src/HOL/ex/InductiveInvariant.thy

no longer declare .psimps rules as [simp].

This regularly caused confusion (e.g., they show up in simp traces
when the regular simp rules are disabled). In the few places where the
rules are used, explicitly mentioning them actually clarifies the
proof text.

(*
    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."

definition
  indinv :: "('a * 'a) set => ('a => 'b => bool) => (('a => 'b) => ('a => 'b)) => bool" where
  "indinv r S F = (\<forall>f x. (\<forall>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."

definition
  indinv_on :: "('a * 'a) set => 'a set => ('a => 'b => bool) => (('a => 'b) => ('a => 'b)) => bool" where
  "indinv_on r D S F = (\<forall>f. \<forall>x\<in>D. (\<forall>y\<in>D. (y,x) \<in> 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)"
  using wf
proof (induct x)
  fix x
  assume  IHYP: "!!y. (y,x) \<in> r \<Longrightarrow> S y (wfrec r F y)"
  then have     "!!y. (y,x) \<in> r \<Longrightarrow> 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\<in>D"
  shows        "S x (wfrec r F x)"
apply (insert INV D indinv_wfrec [OF WF, of "% x y. x\<in>D --> S x y"])
by (simp add: indinv_on_def indinv_def)

theorem ind_fixpoint_on_lemma:
  assumes WF:  "wf r" and
         INV: "\<forall>f. \<forall>x\<in>D. (\<forall>y\<in>D. (y,x) \<in> 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\<in>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: "\<forall>y\<in>D. (y, x) \<in> r --> F (wfrec r F) y = f y & wfrec r F y = f y & S y (f y)"
    assume D': "x\<in>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 "\<forall>y\<in>D. (y, x) \<in> 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: "\<forall>f x. (\<forall>y. (y,x) \<in> 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\<in>D |]
 ==> S x (f x)"
by (simp add: indinv_on_wfrec)

end