# HG changeset patch
# User krauss
# Date 1251743684 -7200
# Node ID c33faa2895202ed352e4cf8ba9832fa4a9a9507e
# Parent  eee4fa79398faceda6c9de752ca9c09830726e8a
moved wfrec to Recdef.thy

diff -r eee4fa79398f -r c33faa289520 src/HOL/Recdef.thy
--- a/src/HOL/Recdef.thy	Mon Aug 31 20:32:00 2009 +0200
+++ b/src/HOL/Recdef.thy	Mon Aug 31 20:34:44 2009 +0200
@@ -19,6 +19,65 @@
   ("Tools/recdef.ML")
 begin
 
+inductive
+  wfrec_rel :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b => bool"
+  for R :: "('a * 'a) set"
+  and F :: "('a => 'b) => 'a => 'b"
+where
+  wfrecI: "ALL z. (z, x) : R --> wfrec_rel R F z (g z) ==>
+            wfrec_rel R F x (F g x)"
+
+constdefs
+  cut        :: "('a => 'b) => ('a * 'a)set => 'a => 'a => 'b"
+  "cut f r x == (%y. if (y,x):r then f y else undefined)"
+
+  adm_wf :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => bool"
+  "adm_wf R F == ALL f g x.
+     (ALL z. (z, x) : R --> f z = g z) --> F f x = F g x"
+
+  wfrec :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b"
+  [code del]: "wfrec R F == %x. THE y. wfrec_rel R (%f x. F (cut f R x) x) x y"
+
+subsection{*Well-Founded Recursion*}
+
+text{*cut*}
+
+lemma cuts_eq: "(cut f r x = cut g r x) = (ALL y. (y,x):r --> f(y)=g(y))"
+by (simp add: expand_fun_eq cut_def)
+
+lemma cut_apply: "(x,a):r ==> (cut f r a)(x) = f(x)"
+by (simp add: cut_def)
+
+text{*Inductive characterization of wfrec combinator; for details see:
+John Harrison, "Inductive definitions: automation and application"*}
+
+lemma wfrec_unique: "[| adm_wf R F; wf R |] ==> EX! y. wfrec_rel R F x y"
+apply (simp add: adm_wf_def)
+apply (erule_tac a=x in wf_induct)
+apply (rule ex1I)
+apply (rule_tac g = "%x. THE y. wfrec_rel R F x y" in wfrec_rel.wfrecI)
+apply (fast dest!: theI')
+apply (erule wfrec_rel.cases, simp)
+apply (erule allE, erule allE, erule allE, erule mp)
+apply (fast intro: the_equality [symmetric])
+done
+
+lemma adm_lemma: "adm_wf R (%f x. F (cut f R x) x)"
+apply (simp add: adm_wf_def)
+apply (intro strip)
+apply (rule cuts_eq [THEN iffD2, THEN subst], assumption)
+apply (rule refl)
+done
+
+lemma wfrec: "wf(r) ==> wfrec r H a = H (cut (wfrec r H) r a) a"
+apply (simp add: wfrec_def)
+apply (rule adm_lemma [THEN wfrec_unique, THEN the1_equality], assumption)
+apply (rule wfrec_rel.wfrecI)
+apply (intro strip)
+apply (erule adm_lemma [THEN wfrec_unique, THEN theI'])
+done
+
+
 text{** This form avoids giant explosions in proofs.  NOTE USE OF ==*}
 lemma def_wfrec: "[| f==wfrec r H;  wf(r) |] ==> f(a) = H (cut f r a) a"
 apply auto
diff -r eee4fa79398f -r c33faa289520 src/HOL/Tools/TFL/rules.ML
--- a/src/HOL/Tools/TFL/rules.ML	Mon Aug 31 20:32:00 2009 +0200
+++ b/src/HOL/Tools/TFL/rules.ML	Mon Aug 31 20:34:44 2009 +0200
@@ -456,7 +456,7 @@
 fun is_cong thm =
   case (Thm.prop_of thm)
      of (Const("==>",_)$(Const("Trueprop",_)$ _) $
-         (Const("==",_) $ (Const (@{const_name "Wellfounded.cut"},_) $ f $ R $ a $ x) $ _)) => false
+         (Const("==",_) $ (Const (@{const_name "Recdef.cut"},_) $ f $ R $ a $ x) $ _)) => false
       | _ => true;
 
 
@@ -659,7 +659,7 @@
   end;
 
 fun restricted t = isSome (S.find_term
-                            (fn (Const(@{const_name "Wellfounded.cut"},_)) =>true | _ => false)
+                            (fn (Const(@{const_name "Recdef.cut"},_)) =>true | _ => false)
                             t)
 
 fun CONTEXT_REWRITE_RULE (func, G, cut_lemma, congs) th =
diff -r eee4fa79398f -r c33faa289520 src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Mon Aug 31 20:32:00 2009 +0200
+++ b/src/HOL/Wellfounded.thy	Mon Aug 31 20:34:44 2009 +0200
@@ -13,14 +13,6 @@
 
 subsection {* Basic Definitions *}
 
-inductive
-  wfrec_rel :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b => bool"
-  for R :: "('a * 'a) set"
-  and F :: "('a => 'b) => 'a => 'b"
-where
-  wfrecI: "ALL z. (z, x) : R --> wfrec_rel R F z (g z) ==>
-            wfrec_rel R F x (F g x)"
-
 constdefs
   wf         :: "('a * 'a)set => bool"
   "wf(r) == (!P. (!x. (!y. (y,x):r --> P(y)) --> P(x)) --> (!x. P(x)))"
@@ -31,16 +23,6 @@
   acyclic :: "('a*'a)set => bool"
   "acyclic r == !x. (x,x) ~: r^+"
 
-  cut        :: "('a => 'b) => ('a * 'a)set => 'a => 'a => 'b"
-  "cut f r x == (%y. if (y,x):r then f y else undefined)"
-
-  adm_wf :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => bool"
-  "adm_wf R F == ALL f g x.
-     (ALL z. (z, x) : R --> f z = g z) --> F f x = F g x"
-
-  wfrec :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b"
-  [code del]: "wfrec R F == %x. THE y. wfrec_rel R (%f x. F (cut f R x) x) x y"
-
 abbreviation acyclicP :: "('a => 'a => bool) => bool" where
   "acyclicP r == acyclic {(x, y). r x y}"
 
@@ -425,46 +407,6 @@
 by (blast intro: finite_acyclic_wf wf_acyclic)
 
 
-subsection{*Well-Founded Recursion*}
-
-text{*cut*}
-
-lemma cuts_eq: "(cut f r x = cut g r x) = (ALL y. (y,x):r --> f(y)=g(y))"
-by (simp add: expand_fun_eq cut_def)
-
-lemma cut_apply: "(x,a):r ==> (cut f r a)(x) = f(x)"
-by (simp add: cut_def)
-
-text{*Inductive characterization of wfrec combinator; for details see:  
-John Harrison, "Inductive definitions: automation and application"*}
-
-lemma wfrec_unique: "[| adm_wf R F; wf R |] ==> EX! y. wfrec_rel R F x y"
-apply (simp add: adm_wf_def)
-apply (erule_tac a=x in wf_induct) 
-apply (rule ex1I)
-apply (rule_tac g = "%x. THE y. wfrec_rel R F x y" in wfrec_rel.wfrecI)
-apply (fast dest!: theI')
-apply (erule wfrec_rel.cases, simp)
-apply (erule allE, erule allE, erule allE, erule mp)
-apply (fast intro: the_equality [symmetric])
-done
-
-lemma adm_lemma: "adm_wf R (%f x. F (cut f R x) x)"
-apply (simp add: adm_wf_def)
-apply (intro strip)
-apply (rule cuts_eq [THEN iffD2, THEN subst], assumption)
-apply (rule refl)
-done
-
-lemma wfrec: "wf(r) ==> wfrec r H a = H (cut (wfrec r H) r a) a"
-apply (simp add: wfrec_def)
-apply (rule adm_lemma [THEN wfrec_unique, THEN the1_equality], assumption)
-apply (rule wfrec_rel.wfrecI)
-apply (intro strip)
-apply (erule adm_lemma [THEN wfrec_unique, THEN theI'])
-done
-
-
 subsection {* @{typ nat} is well-founded *}
 
 lemma less_nat_rel: "op < = (\<lambda>m n. n = Suc m)^++"