# Theory InductiveInvariant

Up to index of Isabelle/HOL/ex

theory InductiveInvariant
imports Main
begin

    (*  ID:         $Id: InductiveInvariant.thy,v 1.4 2005/09/14 20:08:08 wenzelm Exp $
        Author:     Sava Krsti\'{c} and John Matthews
    *)

    header {* Some of the results in Inductive Invariants for Nested Recursion *}

    theory InductiveInvariant imports Main begin

    text {* A formalization of some of the results in \emph{Inductive
      Invariants for Nested Recursion}, by Sava Krsti\'{c} and John
      Matthews.  Appears in the proceedings of TPHOLs 2003, LNCS
      vol. 2758, pp. 253-269. *}

    text "S is an inductive invariant of the functional F with respect to the wellfounded relation r."

    constdefs indinv :: "('a * 'a) set => ('a => 'b => bool) => (('a => 'b) => ('a => 'b)) => bool"
             "indinv r S F == ∀f x. (∀y. (y,x) : r --> S y (f y)) --> S x (F f x)"

    text "S is an inductive invariant of the functional F on set D with respect to the wellfounded relation r."

    constdefs indinv_on :: "('a * 'a) set => 'a set => ('a => 'b => bool) => (('a => 'b) => ('a => 'b)) => bool"
             "indinv_on r D S F == ∀f. ∀x∈D. (∀y∈D. (y,x) ∈ r --> S y (f y)) --> S x (F f x)"

    text "The key theorem, corresponding to theorem 1 of the paper. All other results
          in this theory are proved using instances of this theorem, and theorems
          derived from this theorem."

    theorem indinv_wfrec:
      assumes WF:  "wf r" and
              INV: "indinv r S F"
      shows        "S x (wfrec r F x)"
    proof (induct_tac x rule: wf_induct [OF WF])
      fix x
      assume  IHYP: "∀y. (y,x) ∈ r --> S y (wfrec r F y)"
      then have     "∀y. (y,x) ∈ r --> S y (cut (wfrec r F) r x y)" by (simp add: tfl_cut_apply)
      with INV have "S x (F (cut (wfrec r F) r x) x)" by (unfold indinv_def, blast)
      thus "S x (wfrec r F x)" using WF by (simp add: wfrec)
    qed

    theorem indinv_on_wfrec:
      assumes WF:  "wf r" and
              INV: "indinv_on r D S F" and
              D:   "x∈D"
      shows        "S x (wfrec r F x)"
    apply (insert INV D indinv_wfrec [OF WF, of "% x y. x∈D --> S x y"])
    by (simp add: indinv_on_def indinv_def)

    theorem ind_fixpoint_on_lemma:
      assumes WF:  "wf r" and
             INV: "∀f. ∀x∈D. (∀y∈D. (y,x) ∈ r --> S y (wfrec r F y) & f y = wfrec r F y)
                                   --> S x (wfrec r F x) & F f x = wfrec r F x" and
               D: "x∈D"
      shows "F (wfrec r F) x = wfrec r F x & S x (wfrec r F x)"
    proof (rule indinv_on_wfrec [OF WF _ D, of "% a b. F (wfrec r F) a = b & wfrec r F a = b & S a b" F, simplified])
      show "indinv_on r D (%a b. F (wfrec r F) a = b & wfrec r F a = b & S a b) F"
      proof (unfold indinv_on_def, clarify)
        fix f x
        assume A1: "∀y∈D. (y, x) ∈ r --> F (wfrec r F) y = f y & wfrec r F y = f y & S y (f y)"
        assume D': "x∈D"
        from A1 INV [THEN spec, of f, THEN bspec, OF D']
          have "S x (wfrec r F x)" and
               "F f x = wfrec r F x" by auto
        moreover
        from A1 have "∀y∈D. (y, x) ∈ r --> S y (wfrec r F y)" by auto
        with D' INV [THEN spec, of "wfrec r F", simplified]
          have "F (wfrec r F) x = wfrec r F x" by blast
        ultimately show "F (wfrec r F) x = F f x & wfrec r F x = F f x & S x (F f x)" by auto
      qed
    qed

    theorem ind_fixpoint_lemma:
      assumes WF:  "wf r" and
             INV: "∀f x. (∀y. (y,x) ∈ r --> S y (wfrec r F y) & f y = wfrec r F y)
                             --> S x (wfrec r F x) & F f x = wfrec r F x"
      shows "F (wfrec r F) x = wfrec r F x & S x (wfrec r F x)"
    apply (rule ind_fixpoint_on_lemma [OF WF _ UNIV_I, simplified])
    by (rule INV)

    theorem tfl_indinv_wfrec:
    "[| f == wfrec r F; wf r; indinv r S F |]
     ==> S x (f x)"
    by (simp add: indinv_wfrec)

    theorem tfl_indinv_on_wfrec:
    "[| f == wfrec r F; wf r; indinv_on r D S F; x∈D |]
     ==> S x (f x)"
    by (simp add: indinv_on_wfrec)

    end

theorem indinv_wfrec:

      [| wf r; indinv r S F |] ==> S x (wfrec r F x)

theorem indinv_on_wfrec:

      [| wf r; indinv_on r D S F; x ∈ D |] ==> S x (wfrec r F x)

theorem ind_fixpoint_on_lemma:

      [| wf r;
         ∀f. ∀x∈D. (∀y∈D. (y, x) ∈ r --> S y (wfrec r F y) ∧ f y = wfrec r F y) -->
                   S x (wfrec r F x) ∧ F f x = wfrec r F x;
         x ∈ D |]
      ==> F (wfrec r F) x = wfrec r F x ∧ S x (wfrec r F x)

theorem ind_fixpoint_lemma:

      [| wf r;
         ∀f x. (∀y. (y, x) ∈ r --> S y (wfrec r F y) ∧ f y = wfrec r F y) -->
               S x (wfrec r F x) ∧ F f x = wfrec r F x |]
      ==> F (wfrec r F) x = wfrec r F x ∧ S x (wfrec r F x)

theorem tfl_indinv_wfrec:

      [| f == wfrec r F; wf r; indinv r S F |] ==> S x (f x)

theorem tfl_indinv_on_wfrec:

      [| f == wfrec r F; wf r; indinv_on r D S F; x ∈ D |] ==> S x (f x)