# 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 == \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) - +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 == \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 \ 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: "\k. n = Suc (Suc (2*k)) ==> g_even n = 3" -apply (rule_tac D="{n. \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: "\k. n = 2*k + 4 ==> g_even n = g_even (g_even (n - 2) - 1)" -apply (subgoal_tac "(\k. n - 2 = 2*k + 2) & (\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: "\k. n = Suc (Suc (2*k)) ==> g_even n = 3" +apply (rule_tac D="{n. \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: "\k. n = 2*k + 4 ==> g_even n = g_even (g_even (n - 2) - 1)" +apply (subgoal_tac "(\k. n - 2 = 2*k + 2) & (\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