1.1 --- a/src/HOL/IsaMakefile Thu Aug 11 09:15:45 2011 +0200
1.2 +++ b/src/HOL/IsaMakefile Thu Aug 11 09:41:21 2011 +0200
1.3 @@ -1052,7 +1052,6 @@
1.4 ex/Gauge_Integration.thy ex/Groebner_Examples.thy ex/Guess.thy \
1.5 ex/HarmonicSeries.thy ex/Hebrew.thy ex/Hex_Bin_Examples.thy \
1.6 ex/Higher_Order_Logic.thy ex/Iff_Oracle.thy ex/Induction_Schema.thy \
1.7 - ex/InductiveInvariant.thy ex/InductiveInvariant_examples.thy \
1.8 ex/Interpretation_with_Defs.thy ex/Intuitionistic.thy ex/Lagrange.thy \
1.9 ex/List_to_Set_Comprehension_Examples.thy ex/LocaleTest2.thy \
1.10 ex/MT.thy ex/MergeSort.thy ex/Meson_Test.thy ex/MonoidGroup.thy \
1.11 @@ -1060,7 +1059,7 @@
1.12 ex/Numeral.thy ex/PER.thy ex/PresburgerEx.thy ex/Primrec.thy \
1.13 ex/Quickcheck_Examples.thy ex/Quickcheck_Lattice_Examples.thy \
1.14 ex/Quickcheck_Narrowing_Examples.thy \
1.15 - ex/Quicksort.thy ex/ROOT.ML ex/Recdefs.thy ex/Records.thy \
1.16 + ex/Quicksort.thy ex/ROOT.ML ex/Records.thy \
1.17 ex/ReflectionEx.thy ex/Refute_Examples.thy ex/SAT_Examples.thy \
1.18 ex/SVC_Oracle.thy ex/Serbian.thy ex/Set_Algebras.thy \
1.19 ex/sledgehammer_tactics.ML ex/Sqrt.thy \
2.1 --- a/src/HOL/ex/InductiveInvariant.thy Thu Aug 11 09:15:45 2011 +0200
2.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
2.3 @@ -1,95 +0,0 @@
2.4 -(*
2.5 - Author: Sava Krsti\'{c} and John Matthews
2.6 -*)
2.7 -
2.8 -header {* Some of the results in Inductive Invariants for Nested Recursion *}
2.9 -
2.10 -theory InductiveInvariant imports "~~/src/HOL/Library/Old_Recdef" begin
2.11 -
2.12 -text {* A formalization of some of the results in \emph{Inductive
2.13 - Invariants for Nested Recursion}, by Sava Krsti\'{c} and John
2.14 - Matthews. Appears in the proceedings of TPHOLs 2003, LNCS
2.15 - vol. 2758, pp. 253-269. *}
2.16 -
2.17 -
2.18 -text "S is an inductive invariant of the functional F with respect to the wellfounded relation r."
2.19 -
2.20 -definition
2.21 - indinv :: "('a * 'a) set => ('a => 'b => bool) => (('a => 'b) => ('a => 'b)) => bool" where
2.22 - "indinv r S F = (\<forall>f x. (\<forall>y. (y,x) : r --> S y (f y)) --> S x (F f x))"
2.23 -
2.24 -
2.25 -text "S is an inductive invariant of the functional F on set D with respect to the wellfounded relation r."
2.26 -
2.27 -definition
2.28 - indinv_on :: "('a * 'a) set => 'a set => ('a => 'b => bool) => (('a => 'b) => ('a => 'b)) => bool" where
2.29 - "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))"
2.30 -
2.31 -
2.32 -text "The key theorem, corresponding to theorem 1 of the paper. All other results
2.33 - in this theory are proved using instances of this theorem, and theorems
2.34 - derived from this theorem."
2.35 -
2.36 -theorem indinv_wfrec:
2.37 - assumes wf: "wf r" and
2.38 - inv: "indinv r S F"
2.39 - shows "S x (wfrec r F x)"
2.40 - using wf
2.41 -proof (induct x)
2.42 - fix x
2.43 - assume IHYP: "!!y. (y,x) \<in> r \<Longrightarrow> S y (wfrec r F y)"
2.44 - then have "!!y. (y,x) \<in> r \<Longrightarrow> S y (cut (wfrec r F) r x y)" by (simp add: tfl_cut_apply)
2.45 - with inv have "S x (F (cut (wfrec r F) r x) x)" by (unfold indinv_def, blast)
2.46 - thus "S x (wfrec r F x)" using wf by (simp add: wfrec)
2.47 -qed
2.48 -
2.49 -theorem indinv_on_wfrec:
2.50 - assumes WF: "wf r" and
2.51 - INV: "indinv_on r D S F" and
2.52 - D: "x\<in>D"
2.53 - shows "S x (wfrec r F x)"
2.54 -apply (insert INV D indinv_wfrec [OF WF, of "% x y. x\<in>D --> S x y"])
2.55 -by (simp add: indinv_on_def indinv_def)
2.56 -
2.57 -theorem ind_fixpoint_on_lemma:
2.58 - assumes WF: "wf r" and
2.59 - 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)
2.60 - --> S x (wfrec r F x) & F f x = wfrec r F x" and
2.61 - D: "x\<in>D"
2.62 - shows "F (wfrec r F) x = wfrec r F x & S x (wfrec r F x)"
2.63 -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])
2.64 - show "indinv_on r D (%a b. F (wfrec r F) a = b & wfrec r F a = b & S a b) F"
2.65 - proof (unfold indinv_on_def, clarify)
2.66 - fix f x
2.67 - 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)"
2.68 - assume D': "x\<in>D"
2.69 - from A1 INV [THEN spec, of f, THEN bspec, OF D']
2.70 - have "S x (wfrec r F x)" and
2.71 - "F f x = wfrec r F x" by auto
2.72 - moreover
2.73 - from A1 have "\<forall>y\<in>D. (y, x) \<in> r --> S y (wfrec r F y)" by auto
2.74 - with D' INV [THEN spec, of "wfrec r F", simplified]
2.75 - have "F (wfrec r F) x = wfrec r F x" by blast
2.76 - ultimately show "F (wfrec r F) x = F f x & wfrec r F x = F f x & S x (F f x)" by auto
2.77 - qed
2.78 -qed
2.79 -
2.80 -theorem ind_fixpoint_lemma:
2.81 - assumes WF: "wf r" and
2.82 - INV: "\<forall>f x. (\<forall>y. (y,x) \<in> r --> S y (wfrec r F y) & f y = wfrec r F y)
2.83 - --> S x (wfrec r F x) & F f x = wfrec r F x"
2.84 - shows "F (wfrec r F) x = wfrec r F x & S x (wfrec r F x)"
2.85 -apply (rule ind_fixpoint_on_lemma [OF WF _ UNIV_I, simplified])
2.86 -by (rule INV)
2.87 -
2.88 -theorem tfl_indinv_wfrec:
2.89 -"[| f == wfrec r F; wf r; indinv r S F |]
2.90 - ==> S x (f x)"
2.91 -by (simp add: indinv_wfrec)
2.92 -
2.93 -theorem tfl_indinv_on_wfrec:
2.94 -"[| f == wfrec r F; wf r; indinv_on r D S F; x\<in>D |]
2.95 - ==> S x (f x)"
2.96 -by (simp add: indinv_on_wfrec)
2.97 -
2.98 -end
3.1 --- a/src/HOL/ex/InductiveInvariant_examples.thy Thu Aug 11 09:15:45 2011 +0200
3.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
3.3 @@ -1,130 +0,0 @@
3.4 -(*
3.5 - Author: Sava Krsti\'{c} and John Matthews
3.6 -*)
3.7 -
3.8 -header {* Example use if an inductive invariant to solve termination conditions *}
3.9 -
3.10 -theory InductiveInvariant_examples imports InductiveInvariant begin
3.11 -
3.12 -text "A simple example showing how to use an inductive invariant
3.13 - to solve termination conditions generated by recdef on
3.14 - nested recursive function definitions."
3.15 -
3.16 -consts g :: "nat => nat"
3.17 -
3.18 -recdef (permissive) g "less_than"
3.19 - "g 0 = 0"
3.20 - "g (Suc n) = g (g n)"
3.21 -
3.22 -text "We can prove the unsolved termination condition for
3.23 - g by showing it is an inductive invariant."
3.24 -
3.25 -recdef_tc g_tc[simp]: g
3.26 -apply (rule allI)
3.27 -apply (rule_tac x=n in tfl_indinv_wfrec [OF g_def])
3.28 -apply (auto simp add: indinv_def split: nat.split)
3.29 -apply (frule_tac x=nat in spec)
3.30 -apply (drule_tac x="f nat" in spec)
3.31 -by auto
3.32 -
3.33 -
3.34 -text "This declaration invokes Isabelle's simplifier to
3.35 - remove any termination conditions before adding
3.36 - g's rules to the simpset."
3.37 -declare g.simps [simplified, simp]
3.38 -
3.39 -
3.40 -text "This is an example where the termination condition generated
3.41 - by recdef is not itself an inductive invariant."
3.42 -
3.43 -consts g' :: "nat => nat"
3.44 -recdef (permissive) g' "less_than"
3.45 - "g' 0 = 0"
3.46 - "g' (Suc n) = g' n + g' (g' n)"
3.47 -
3.48 -thm g'.simps
3.49 -
3.50 -
3.51 -text "The strengthened inductive invariant is as follows
3.52 - (this invariant also works for the first example above):"
3.53 -
3.54 -lemma g'_inv: "g' n = 0"
3.55 -thm tfl_indinv_wfrec [OF g'_def]
3.56 -apply (rule_tac x=n in tfl_indinv_wfrec [OF g'_def])
3.57 -by (auto simp add: indinv_def split: nat.split)
3.58 -
3.59 -recdef_tc g'_tc[simp]: g'
3.60 -by (simp add: g'_inv)
3.61 -
3.62 -text "Now we can remove the termination condition from
3.63 - the rules for g' ."
3.64 -thm g'.simps [simplified]
3.65 -
3.66 -
3.67 -text {* Sometimes a recursive definition is partial, that is, it
3.68 - is only meant to be invoked on "good" inputs. As a contrived
3.69 - example, we will define a new version of g that is only
3.70 - well defined for even inputs greater than zero. *}
3.71 -
3.72 -consts g_even :: "nat => nat"
3.73 -recdef (permissive) g_even "less_than"
3.74 - "g_even (Suc (Suc 0)) = 3"
3.75 - "g_even n = g_even (g_even (n - 2) - 1)"
3.76 -
3.77 -
3.78 -text "We can prove a conditional version of the unsolved termination
3.79 - condition for @{term g_even} by proving a stronger inductive invariant."
3.80 -
3.81 -lemma g_even_indinv: "\<exists>k. n = Suc (Suc (2*k)) ==> g_even n = 3"
3.82 -apply (rule_tac D="{n. \<exists>k. n = Suc (Suc (2*k))}" and x=n in tfl_indinv_on_wfrec [OF g_even_def])
3.83 -apply (auto simp add: indinv_on_def split: nat.split)
3.84 -by (case_tac ka, auto)
3.85 -
3.86 -
3.87 -text "Now we can prove that the second recursion equation for @{term g_even}
3.88 - holds, provided that n is an even number greater than two."
3.89 -
3.90 -theorem g_even_n: "\<exists>k. n = 2*k + 4 ==> g_even n = g_even (g_even (n - 2) - 1)"
3.91 -apply (subgoal_tac "(\<exists>k. n - 2 = 2*k + 2) & (\<exists>k. n = 2*k + 2)")
3.92 -by (auto simp add: g_even_indinv, arith)
3.93 -
3.94 -
3.95 -text "McCarthy's ninety-one function. This function requires a
3.96 - non-standard measure to prove termination."
3.97 -
3.98 -consts ninety_one :: "nat => nat"
3.99 -recdef (permissive) ninety_one "measure (%n. 101 - n)"
3.100 - "ninety_one x = (if 100 < x
3.101 - then x - 10
3.102 - else (ninety_one (ninety_one (x+11))))"
3.103 -
3.104 -text "To discharge the termination condition, we will prove
3.105 - a strengthened inductive invariant:
3.106 - S x y == x < y + 11"
3.107 -
3.108 -lemma ninety_one_inv: "n < ninety_one n + 11"
3.109 -apply (rule_tac x=n in tfl_indinv_wfrec [OF ninety_one_def])
3.110 -apply force
3.111 -apply (auto simp add: indinv_def)
3.112 -apply (frule_tac x="x+11" in spec)
3.113 -apply (frule_tac x="f (x + 11)" in spec)
3.114 -by arith
3.115 -
3.116 -text "Proving the termination condition using the
3.117 - strengthened inductive invariant."
3.118 -
3.119 -recdef_tc ninety_one_tc[rule_format]: ninety_one
3.120 -apply clarify
3.121 -by (cut_tac n="x+11" in ninety_one_inv, arith)
3.122 -
3.123 -text "Now we can remove the termination condition from
3.124 - the simplification rule for @{term ninety_one}."
3.125 -
3.126 -theorem def_ninety_one:
3.127 -"ninety_one x = (if 100 < x
3.128 - then x - 10
3.129 - else ninety_one (ninety_one (x+11)))"
3.130 -by (subst ninety_one.simps,
3.131 - simp add: ninety_one_tc)
3.132 -
3.133 -end
4.1 --- a/src/HOL/ex/ROOT.ML Thu Aug 11 09:15:45 2011 +0200
4.2 +++ b/src/HOL/ex/ROOT.ML Thu Aug 11 09:41:21 2011 +0200
4.3 @@ -22,10 +22,8 @@
4.4 "Abstract_NAT",
4.5 "Guess",
4.6 "Binary",
4.7 - "Recdefs",
4.8 "Fundefs",
4.9 "Induction_Schema",
4.10 - "InductiveInvariant_examples",
4.11 "LocaleTest2",
4.12 "Records",
4.13 "While_Combinator_Example",
5.1 --- a/src/HOL/ex/Recdefs.thy Thu Aug 11 09:15:45 2011 +0200
5.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
5.3 @@ -1,144 +0,0 @@
5.4 -(* Title: HOL/ex/Recdefs.thy
5.5 - Author: Konrad Slind and Lawrence C Paulson
5.6 - Copyright 1996 University of Cambridge
5.7 -
5.8 -Examples of recdef definitions. Most, but not all, are handled automatically.
5.9 -*)
5.10 -
5.11 -header {* Examples of recdef definitions *}
5.12 -
5.13 -theory Recdefs imports "~~/src/HOL/Library/Old_Recdef" begin
5.14 -
5.15 -consts fact :: "nat => nat"
5.16 -recdef fact less_than
5.17 - "fact x = (if x = 0 then 1 else x * fact (x - 1))"
5.18 -
5.19 -consts Fact :: "nat => nat"
5.20 -recdef Fact less_than
5.21 - "Fact 0 = 1"
5.22 - "Fact (Suc x) = Fact x * Suc x"
5.23 -
5.24 -consts fib :: "int => int"
5.25 -recdef fib "measure nat"
5.26 - eqn: "fib n = (if n < 1 then 0
5.27 - else if n=1 then 1
5.28 - else fib(n - 2) + fib(n - 1))";
5.29 -
5.30 -lemma "fib 7 = 13"
5.31 -by simp
5.32 -
5.33 -
5.34 -consts map2 :: "('a => 'b => 'c) * 'a list * 'b list => 'c list"
5.35 -recdef map2 "measure(\<lambda>(f, l1, l2). size l1)"
5.36 - "map2 (f, [], []) = []"
5.37 - "map2 (f, h # t, []) = []"
5.38 - "map2 (f, h1 # t1, h2 # t2) = f h1 h2 # map2 (f, t1, t2)"
5.39 -
5.40 -consts finiteRchain :: "('a => 'a => bool) * 'a list => bool"
5.41 -recdef finiteRchain "measure (\<lambda>(R, l). size l)"
5.42 - "finiteRchain(R, []) = True"
5.43 - "finiteRchain(R, [x]) = True"
5.44 - "finiteRchain(R, x # y # rst) = (R x y \<and> finiteRchain (R, y # rst))"
5.45 -
5.46 -text {* Not handled automatically: too complicated. *}
5.47 -consts variant :: "nat * nat list => nat"
5.48 -recdef (permissive) variant "measure (\<lambda>(n,ns). size (filter (\<lambda>y. n \<le> y) ns))"
5.49 - "variant (x, L) = (if x \<in> set L then variant (Suc x, L) else x)"
5.50 -
5.51 -consts gcd :: "nat * nat => nat"
5.52 -recdef gcd "measure (\<lambda>(x, y). x + y)"
5.53 - "gcd (0, y) = y"
5.54 - "gcd (Suc x, 0) = Suc x"
5.55 - "gcd (Suc x, Suc y) =
5.56 - (if y \<le> x then gcd (x - y, Suc y) else gcd (Suc x, y - x))"
5.57 -
5.58 -
5.59 -text {*
5.60 - \medskip The silly @{term g} function: example of nested recursion.
5.61 - Not handled automatically. In fact, @{term g} is the zero constant
5.62 - function.
5.63 - *}
5.64 -
5.65 -consts g :: "nat => nat"
5.66 -recdef (permissive) g less_than
5.67 - "g 0 = 0"
5.68 - "g (Suc x) = g (g x)"
5.69 -
5.70 -lemma g_terminates: "g x < Suc x"
5.71 - apply (induct x rule: g.induct)
5.72 - apply (auto simp add: g.simps)
5.73 - done
5.74 -
5.75 -lemma g_zero: "g x = 0"
5.76 - apply (induct x rule: g.induct)
5.77 - apply (simp_all add: g.simps g_terminates)
5.78 - done
5.79 -
5.80 -
5.81 -consts Div :: "nat * nat => nat * nat"
5.82 -recdef Div "measure fst"
5.83 - "Div (0, x) = (0, 0)"
5.84 - "Div (Suc x, y) =
5.85 - (let (q, r) = Div (x, y)
5.86 - in if y \<le> Suc r then (Suc q, 0) else (q, Suc r))"
5.87 -
5.88 -text {*
5.89 - \medskip Not handled automatically. Should be the predecessor
5.90 - function, but there is an unnecessary "looping" recursive call in
5.91 - @{text "k 1"}.
5.92 -*}
5.93 -
5.94 -consts k :: "nat => nat"
5.95 -
5.96 -recdef (permissive) k less_than
5.97 - "k 0 = 0"
5.98 - "k (Suc n) =
5.99 - (let x = k 1
5.100 - in if False then k (Suc 1) else n)"
5.101 -
5.102 -consts part :: "('a => bool) * 'a list * 'a list * 'a list => 'a list * 'a list"
5.103 -recdef part "measure (\<lambda>(P, l, l1, l2). size l)"
5.104 - "part (P, [], l1, l2) = (l1, l2)"
5.105 - "part (P, h # rst, l1, l2) =
5.106 - (if P h then part (P, rst, h # l1, l2)
5.107 - else part (P, rst, l1, h # l2))"
5.108 -
5.109 -consts fqsort :: "('a => 'a => bool) * 'a list => 'a list"
5.110 -recdef (permissive) fqsort "measure (size o snd)"
5.111 - "fqsort (ord, []) = []"
5.112 - "fqsort (ord, x # rst) =
5.113 - (let (less, more) = part ((\<lambda>y. ord y x), rst, ([], []))
5.114 - in fqsort (ord, less) @ [x] @ fqsort (ord, more))"
5.115 -
5.116 -text {*
5.117 - \medskip Silly example which demonstrates the occasional need for
5.118 - additional congruence rules (here: @{thm [source] map_cong}). If
5.119 - the congruence rule is removed, an unprovable termination condition
5.120 - is generated! Termination not proved automatically. TFL requires
5.121 - @{term [source] "\<lambda>x. mapf x"} instead of @{term [source] mapf}.
5.122 -*}
5.123 -
5.124 -consts mapf :: "nat => nat list"
5.125 -recdef mapf "measure (\<lambda>m. m)"
5.126 - "mapf 0 = []"
5.127 - "mapf (Suc n) = concat (map (\<lambda>x. mapf x) (replicate n n))"
5.128 - (hints cong: map_cong)
5.129 -
5.130 -(* This used to be an example where recdef_tc etc is needed,
5.131 - but now termination is proved outright
5.132 -recdef_tc mapf_tc: mapf
5.133 - apply (rule allI)
5.134 - apply (case_tac "n = 0")
5.135 - apply simp_all
5.136 - done
5.137 -
5.138 -text {* Removing the termination condition from the generated thms: *}
5.139 -
5.140 -lemma "mapf (Suc n) = concat (map mapf (replicate n n))"
5.141 - apply (simp add: mapf.simps mapf_tc)
5.142 - done
5.143 -
5.144 -lemmas mapf_induct = mapf.induct [OF mapf_tc]
5.145 -*)
5.146 -
5.147 -end