# HG changeset patch
# User paulson
# Date 1112164421 -7200
# Node ID 57c437b705219849de6670e6550b247930896618
# Parent  8408a06590a644176e2e9953ed183ac07f399a01
converted from DOS to UNIX format

diff -r 8408a06590a6 -r 57c437b70521 src/HOL/ex/InductiveInvariant.thy
--- a/src/HOL/ex/InductiveInvariant.thy	Tue Mar 29 12:30:48 2005 +0200
+++ b/src/HOL/ex/InductiveInvariant.thy	Wed Mar 30 08:33:41 2005 +0200
@@ -1,89 +1,89 @@
-theory InductiveInvariant = Main:
-
-(** Authors: Sava Krsti\'{c} and John Matthews **)
-(**    Date: Sep 12, 2003                      **)
-
-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 == \<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."
-
-constdefs indinv_on :: "('a * 'a) set => 'a set => ('a => 'b => bool) => (('a => 'b) => ('a => 'b)) => bool"
-         "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)"
-proof (induct_tac x rule: wf_induct [OF WF])
-  fix x
-  assume  IHYP: "\<forall>y. (y,x) \<in> r --> S y (wfrec r F y)"
-  then have     "\<forall>y. (y,x) \<in> 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\<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)
-
+theory InductiveInvariant = Main:
+
+(** Authors: Sava Krsti\'{c} and John Matthews **)
+(**    Date: Sep 12, 2003                      **)
+
+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 == \<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."
+
+constdefs indinv_on :: "('a * 'a) set => 'a set => ('a => 'b => bool) => (('a => 'b) => ('a => 'b)) => bool"
+         "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)"
+proof (induct_tac x rule: wf_induct [OF WF])
+  fix x
+  assume  IHYP: "\<forall>y. (y,x) \<in> r --> S y (wfrec r F y)"
+  then have     "\<forall>y. (y,x) \<in> 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\<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
\ No newline at end of file
diff -r 8408a06590a6 -r 57c437b70521 src/HOL/ex/InductiveInvariant_examples.thy
--- a/src/HOL/ex/InductiveInvariant_examples.thy	Tue Mar 29 12:30:48 2005 +0200
+++ b/src/HOL/ex/InductiveInvariant_examples.thy	Wed Mar 30 08:33:41 2005 +0200
@@ -1,127 +1,127 @@
-theory InductiveInvariant_examples = InductiveInvariant :
-
-(** Authors: Sava Krsti\'{c} and John Matthews **)
-(**    Date: Oct 17, 2003                      **)
-
-text "A simple example showing how to use an inductive invariant
-      to solve termination conditions generated by recdef on
-      nested recursive function definitions."
-
-consts g :: "nat => nat"
-
-recdef (permissive) g "less_than"
-  "g 0 = 0"
-  "g (Suc n) = g (g n)"
-
-text "We can prove the unsolved termination condition for
-      g by showing it is an inductive invariant."
-
-recdef_tc g_tc[simp]: g
-apply (rule allI)
-apply (rule_tac x=n in tfl_indinv_wfrec [OF g_def])
-apply (auto simp add: indinv_def split: nat.split)
-apply (frule_tac x=nat in spec)
-apply (drule_tac x="f nat" in spec)
-by auto
-
-
-text "This declaration invokes Isabelle's simplifier to
-      remove any termination conditions before adding
-      g's rules to the simpset."
-declare g.simps [simplified, simp]
-
-
-text "This is an example where the termination condition generated
-      by recdef is not itself an inductive invariant."
-
-consts g' :: "nat => nat"
-recdef (permissive) g' "less_than"
-  "g' 0 = 0"
-  "g' (Suc n) = g' n + g' (g' n)"
-
-thm g'.simps
-
-
-text "The strengthened inductive invariant is as follows
-      (this invariant also works for the first example above):"
-
-lemma g'_inv: "g' n = 0"
-thm tfl_indinv_wfrec [OF g'_def]
-apply (rule_tac x=n in tfl_indinv_wfrec [OF g'_def])
-by (auto simp add: indinv_def split: nat.split)
-
-recdef_tc g'_tc[simp]: g'
-by (simp add: g'_inv)
-
-text "Now we can remove the termination condition from
-      the rules for g' ."
-thm g'.simps [simplified]
-
-
-text {* Sometimes a recursive definition is partial, that is, it
-        is only meant to be invoked on "good" inputs. As a contrived
-        example, we will define a new version of g that is only
-        well defined for even inputs greater than zero. *}
-
-consts g_even :: "nat => nat"
-recdef (permissive) g_even "less_than"
-  "g_even (Suc (Suc 0)) = 3"
-  "g_even n = g_even (g_even (n - 2) - 1)"
-
-
-text "We can prove a conditional version of the unsolved termination
-      condition for @{term g_even} by proving a stronger inductive invariant."
-
-lemma g_even_indinv: "\<exists>k. n = Suc (Suc (2*k)) ==> g_even n = 3"
-apply (rule_tac D="{n. \<exists>k. n = Suc (Suc (2*k))}" and x=n in tfl_indinv_on_wfrec [OF g_even_def])
-apply (auto simp add: indinv_on_def split: nat.split)
-by (case_tac ka, auto)
-
-
-text "Now we can prove that the second recursion equation for @{term g_even}
-      holds, provided that n is an even number greater than two."
-
-theorem g_even_n: "\<exists>k. n = 2*k + 4 ==> g_even n = g_even (g_even (n - 2) - 1)"
-apply (subgoal_tac "(\<exists>k. n - 2 = 2*k + 2) & (\<exists>k. n = 2*k + 2)")
-by (auto simp add: g_even_indinv, arith)
-
-
-text "McCarthy's ninety-one function. This function requires a
-      non-standard measure to prove termination."
-
-consts ninety_one :: "nat => nat"
-recdef (permissive) ninety_one "measure (%n. 101 - n)"
-  "ninety_one x = (if 100 < x
-                     then x - 10
-                     else (ninety_one (ninety_one (x+11))))"
-
-text "To discharge the termination condition, we will prove
-      a strengthened inductive invariant:
-         S x y == x < y + 11"
-
-lemma ninety_one_inv: "n < ninety_one n + 11"
-apply (rule_tac x=n in tfl_indinv_wfrec [OF ninety_one_def])
-apply force
-apply (auto simp add: indinv_def measure_def inv_image_def)
-apply (frule_tac x="x+11" in spec)
-apply (frule_tac x="f (x + 11)" in spec)
-by arith
-
-text "Proving the termination condition using the
-      strengthened inductive invariant."
-
-recdef_tc ninety_one_tc[rule_format]: ninety_one
-apply clarify
-by (cut_tac n="x+11" in ninety_one_inv, arith)
-
-text "Now we can remove the termination condition from
-      the simplification rule for @{term ninety_one}."
-
-theorem def_ninety_one:
-"ninety_one x = (if 100 < x
-                   then x - 10
-                   else ninety_one (ninety_one (x+11)))"
-by (subst ninety_one.simps,
-    simp add: ninety_one_tc measure_def inv_image_def)
-
+theory InductiveInvariant_examples = InductiveInvariant :
+
+(** Authors: Sava Krsti\'{c} and John Matthews **)
+(**    Date: Oct 17, 2003                      **)
+
+text "A simple example showing how to use an inductive invariant
+      to solve termination conditions generated by recdef on
+      nested recursive function definitions."
+
+consts g :: "nat => nat"
+
+recdef (permissive) g "less_than"
+  "g 0 = 0"
+  "g (Suc n) = g (g n)"
+
+text "We can prove the unsolved termination condition for
+      g by showing it is an inductive invariant."
+
+recdef_tc g_tc[simp]: g
+apply (rule allI)
+apply (rule_tac x=n in tfl_indinv_wfrec [OF g_def])
+apply (auto simp add: indinv_def split: nat.split)
+apply (frule_tac x=nat in spec)
+apply (drule_tac x="f nat" in spec)
+by auto
+
+
+text "This declaration invokes Isabelle's simplifier to
+      remove any termination conditions before adding
+      g's rules to the simpset."
+declare g.simps [simplified, simp]
+
+
+text "This is an example where the termination condition generated
+      by recdef is not itself an inductive invariant."
+
+consts g' :: "nat => nat"
+recdef (permissive) g' "less_than"
+  "g' 0 = 0"
+  "g' (Suc n) = g' n + g' (g' n)"
+
+thm g'.simps
+
+
+text "The strengthened inductive invariant is as follows
+      (this invariant also works for the first example above):"
+
+lemma g'_inv: "g' n = 0"
+thm tfl_indinv_wfrec [OF g'_def]
+apply (rule_tac x=n in tfl_indinv_wfrec [OF g'_def])
+by (auto simp add: indinv_def split: nat.split)
+
+recdef_tc g'_tc[simp]: g'
+by (simp add: g'_inv)
+
+text "Now we can remove the termination condition from
+      the rules for g' ."
+thm g'.simps [simplified]
+
+
+text {* Sometimes a recursive definition is partial, that is, it
+        is only meant to be invoked on "good" inputs. As a contrived
+        example, we will define a new version of g that is only
+        well defined for even inputs greater than zero. *}
+
+consts g_even :: "nat => nat"
+recdef (permissive) g_even "less_than"
+  "g_even (Suc (Suc 0)) = 3"
+  "g_even n = g_even (g_even (n - 2) - 1)"
+
+
+text "We can prove a conditional version of the unsolved termination
+      condition for @{term g_even} by proving a stronger inductive invariant."
+
+lemma g_even_indinv: "\<exists>k. n = Suc (Suc (2*k)) ==> g_even n = 3"
+apply (rule_tac D="{n. \<exists>k. n = Suc (Suc (2*k))}" and x=n in tfl_indinv_on_wfrec [OF g_even_def])
+apply (auto simp add: indinv_on_def split: nat.split)
+by (case_tac ka, auto)
+
+
+text "Now we can prove that the second recursion equation for @{term g_even}
+      holds, provided that n is an even number greater than two."
+
+theorem g_even_n: "\<exists>k. n = 2*k + 4 ==> g_even n = g_even (g_even (n - 2) - 1)"
+apply (subgoal_tac "(\<exists>k. n - 2 = 2*k + 2) & (\<exists>k. n = 2*k + 2)")
+by (auto simp add: g_even_indinv, arith)
+
+
+text "McCarthy's ninety-one function. This function requires a
+      non-standard measure to prove termination."
+
+consts ninety_one :: "nat => nat"
+recdef (permissive) ninety_one "measure (%n. 101 - n)"
+  "ninety_one x = (if 100 < x
+                     then x - 10
+                     else (ninety_one (ninety_one (x+11))))"
+
+text "To discharge the termination condition, we will prove
+      a strengthened inductive invariant:
+         S x y == x < y + 11"
+
+lemma ninety_one_inv: "n < ninety_one n + 11"
+apply (rule_tac x=n in tfl_indinv_wfrec [OF ninety_one_def])
+apply force
+apply (auto simp add: indinv_def measure_def inv_image_def)
+apply (frule_tac x="x+11" in spec)
+apply (frule_tac x="f (x + 11)" in spec)
+by arith
+
+text "Proving the termination condition using the
+      strengthened inductive invariant."
+
+recdef_tc ninety_one_tc[rule_format]: ninety_one
+apply clarify
+by (cut_tac n="x+11" in ninety_one_inv, arith)
+
+text "Now we can remove the termination condition from
+      the simplification rule for @{term ninety_one}."
+
+theorem def_ninety_one:
+"ninety_one x = (if 100 < x
+                   then x - 10
+                   else ninety_one (ninety_one (x+11)))"
+by (subst ninety_one.simps,
+    simp add: ninety_one_tc measure_def inv_image_def)
+
 end
\ No newline at end of file