# HG changeset patch
# User krauss
# Date 1313048481 -7200
# Node ID 24bb6b4e873f42cf52203a274d5e1c03e96beffb
# Parent  74b3751ea271a0b898072967dadd0ed127012376
removed obsolete recdef-related examples

diff -r 74b3751ea271 -r 24bb6b4e873f src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Thu Aug 11 09:15:45 2011 +0200
+++ b/src/HOL/IsaMakefile	Thu Aug 11 09:41:21 2011 +0200
@@ -1052,7 +1052,6 @@
   ex/Gauge_Integration.thy ex/Groebner_Examples.thy ex/Guess.thy	\
   ex/HarmonicSeries.thy ex/Hebrew.thy ex/Hex_Bin_Examples.thy		\
   ex/Higher_Order_Logic.thy ex/Iff_Oracle.thy ex/Induction_Schema.thy	\
-  ex/InductiveInvariant.thy ex/InductiveInvariant_examples.thy		\
   ex/Interpretation_with_Defs.thy ex/Intuitionistic.thy ex/Lagrange.thy	\
   ex/List_to_Set_Comprehension_Examples.thy ex/LocaleTest2.thy		\
   ex/MT.thy ex/MergeSort.thy ex/Meson_Test.thy ex/MonoidGroup.thy	\
@@ -1060,7 +1059,7 @@
   ex/Numeral.thy ex/PER.thy ex/PresburgerEx.thy ex/Primrec.thy		\
   ex/Quickcheck_Examples.thy ex/Quickcheck_Lattice_Examples.thy		\
   ex/Quickcheck_Narrowing_Examples.thy  				\
-  ex/Quicksort.thy ex/ROOT.ML ex/Recdefs.thy ex/Records.thy		\
+  ex/Quicksort.thy ex/ROOT.ML ex/Records.thy		\
   ex/ReflectionEx.thy ex/Refute_Examples.thy ex/SAT_Examples.thy	\
   ex/SVC_Oracle.thy ex/Serbian.thy ex/Set_Algebras.thy			\
   ex/sledgehammer_tactics.ML ex/Sqrt.thy				\
diff -r 74b3751ea271 -r 24bb6b4e873f src/HOL/ex/InductiveInvariant.thy
--- a/src/HOL/ex/InductiveInvariant.thy	Thu Aug 11 09:15:45 2011 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,95 +0,0 @@
-(*
-    Author:     Sava Krsti\'{c} and John Matthews
-*)
-
-header {* Some of the results in Inductive Invariants for Nested Recursion *}
-
-theory InductiveInvariant imports "~~/src/HOL/Library/Old_Recdef" 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
diff -r 74b3751ea271 -r 24bb6b4e873f src/HOL/ex/InductiveInvariant_examples.thy
--- a/src/HOL/ex/InductiveInvariant_examples.thy	Thu Aug 11 09:15:45 2011 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,130 +0,0 @@
-(*
-    Author:     Sava Krsti\'{c} and John Matthews
-*)
-
-header {* Example use if an inductive invariant to solve termination conditions *}
-
-theory InductiveInvariant_examples imports InductiveInvariant  begin
-
-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)
-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)
-
-end
diff -r 74b3751ea271 -r 24bb6b4e873f src/HOL/ex/ROOT.ML
--- a/src/HOL/ex/ROOT.ML	Thu Aug 11 09:15:45 2011 +0200
+++ b/src/HOL/ex/ROOT.ML	Thu Aug 11 09:41:21 2011 +0200
@@ -22,10 +22,8 @@
   "Abstract_NAT",
   "Guess",
   "Binary",
-  "Recdefs",
   "Fundefs",
   "Induction_Schema",
-  "InductiveInvariant_examples",
   "LocaleTest2",
   "Records",
   "While_Combinator_Example",
diff -r 74b3751ea271 -r 24bb6b4e873f src/HOL/ex/Recdefs.thy
--- a/src/HOL/ex/Recdefs.thy	Thu Aug 11 09:15:45 2011 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,144 +0,0 @@
-(*  Title:      HOL/ex/Recdefs.thy
-    Author:     Konrad Slind and Lawrence C Paulson
-    Copyright   1996  University of Cambridge
-
-Examples of recdef definitions.  Most, but not all, are handled automatically.
-*)
-
-header {* Examples of recdef definitions *}
-
-theory Recdefs imports "~~/src/HOL/Library/Old_Recdef" begin
-
-consts fact :: "nat => nat"
-recdef fact  less_than
-  "fact x = (if x = 0 then 1 else x * fact (x - 1))"
-
-consts Fact :: "nat => nat"
-recdef Fact  less_than
-  "Fact 0 = 1"
-  "Fact (Suc x) = Fact x * Suc x"
-
-consts fib :: "int => int"
-recdef fib  "measure nat"
-  eqn:  "fib n = (if n < 1 then 0
-                  else if n=1 then 1
-                  else fib(n - 2) + fib(n - 1))";
-
-lemma "fib 7 = 13"
-by simp
-
-
-consts map2 :: "('a => 'b => 'c) * 'a list * 'b list => 'c list"
-recdef map2  "measure(\<lambda>(f, l1, l2). size l1)"
-  "map2 (f, [], [])  = []"
-  "map2 (f, h # t, []) = []"
-  "map2 (f, h1 # t1, h2 # t2) = f h1 h2 # map2 (f, t1, t2)"
-
-consts finiteRchain :: "('a => 'a => bool) * 'a list => bool"
-recdef finiteRchain  "measure (\<lambda>(R, l). size l)"
-  "finiteRchain(R,  []) = True"
-  "finiteRchain(R, [x]) = True"
-  "finiteRchain(R, x # y # rst) = (R x y \<and> finiteRchain (R, y # rst))"
-
-text {* Not handled automatically: too complicated. *}
-consts variant :: "nat * nat list => nat"
-recdef (permissive) variant "measure (\<lambda>(n,ns). size (filter (\<lambda>y. n \<le> y) ns))"
-  "variant (x, L) = (if x \<in> set L then variant (Suc x, L) else x)"
-
-consts gcd :: "nat * nat => nat"
-recdef gcd  "measure (\<lambda>(x, y). x + y)"
-  "gcd (0, y) = y"
-  "gcd (Suc x, 0) = Suc x"
-  "gcd (Suc x, Suc y) =
-    (if y \<le> x then gcd (x - y, Suc y) else gcd (Suc x, y - x))"
-
-
-text {*
-  \medskip The silly @{term g} function: example of nested recursion.
-  Not handled automatically.  In fact, @{term g} is the zero constant
-  function.
- *}
-
-consts g :: "nat => nat"
-recdef (permissive) g  less_than
-  "g 0 = 0"
-  "g (Suc x) = g (g x)"
-
-lemma g_terminates: "g x < Suc x"
-  apply (induct x rule: g.induct)
-   apply (auto simp add: g.simps)
-  done
-
-lemma g_zero: "g x = 0"
-  apply (induct x rule: g.induct)
-   apply (simp_all add: g.simps g_terminates)
-  done
-
-
-consts Div :: "nat * nat => nat * nat"
-recdef Div  "measure fst"
-  "Div (0, x) = (0, 0)"
-  "Div (Suc x, y) =
-    (let (q, r) = Div (x, y)
-    in if y \<le> Suc r then (Suc q, 0) else (q, Suc r))"
-
-text {*
-  \medskip Not handled automatically.  Should be the predecessor
-  function, but there is an unnecessary "looping" recursive call in
-  @{text "k 1"}.
-*}
-
-consts k :: "nat => nat"
-
-recdef (permissive) k  less_than
-  "k 0 = 0"
-  "k (Suc n) =
-   (let x = k 1
-    in if False then k (Suc 1) else n)"
-
-consts part :: "('a => bool) * 'a list * 'a list * 'a list => 'a list * 'a list"
-recdef part  "measure (\<lambda>(P, l, l1, l2). size l)"
-  "part (P, [], l1, l2) = (l1, l2)"
-  "part (P, h # rst, l1, l2) =
-    (if P h then part (P, rst, h # l1, l2)
-    else part (P, rst, l1, h # l2))"
-
-consts fqsort :: "('a => 'a => bool) * 'a list => 'a list"
-recdef (permissive) fqsort  "measure (size o snd)"
-  "fqsort (ord, []) = []"
-  "fqsort (ord, x # rst) =
-  (let (less, more) = part ((\<lambda>y. ord y x), rst, ([], []))
-  in fqsort (ord, less) @ [x] @ fqsort (ord, more))"
-
-text {*
-  \medskip Silly example which demonstrates the occasional need for
-  additional congruence rules (here: @{thm [source] map_cong}).  If
-  the congruence rule is removed, an unprovable termination condition
-  is generated!  Termination not proved automatically.  TFL requires
-  @{term [source] "\<lambda>x. mapf x"} instead of @{term [source] mapf}.
-*}
-
-consts mapf :: "nat => nat list"
-recdef mapf  "measure (\<lambda>m. m)"
-  "mapf 0 = []"
-  "mapf (Suc n) = concat (map (\<lambda>x. mapf x) (replicate n n))"
-  (hints cong: map_cong)
-
-(* This used to be an example where recdef_tc etc is needed,
-   but now termination is proved outright
-recdef_tc mapf_tc: mapf
-  apply (rule allI)
-  apply (case_tac "n = 0")
-   apply simp_all
-  done
-
-text {* Removing the termination condition from the generated thms: *}
-
-lemma "mapf (Suc n) = concat (map mapf (replicate n n))"
-  apply (simp add: mapf.simps mapf_tc)
-  done
-
-lemmas mapf_induct = mapf.induct [OF mapf_tc]
-*)
-
-end