# HG changeset patch
# User krauss
# Date 1312274210 -7200
# Node ID 5cfc1c36ae97dd30c7841e07e7f06b0a5092f7eb
# Parent  8c1dfd6c226215328a09e4fdc783049f4af50e42
moved recdef package to HOL/Library/Old_Recdef.thy

diff -r 8c1dfd6c2262 -r 5cfc1c36ae97 src/HOL/Bali/Basis.thy
--- a/src/HOL/Bali/Basis.thy	Tue Aug 02 10:03:14 2011 +0200
+++ b/src/HOL/Bali/Basis.thy	Tue Aug 02 10:36:50 2011 +0200
@@ -3,7 +3,7 @@
 *)
 header {* Definitions extending HOL as logical basis of Bali *}
 
-theory Basis imports Main begin
+theory Basis imports Main "~~/src/HOL/Library/Old_Recdef" begin
 
 
 section "misc"
diff -r 8c1dfd6c2262 -r 5cfc1c36ae97 src/HOL/Bali/Decl.thy
--- a/src/HOL/Bali/Decl.thy	Tue Aug 02 10:03:14 2011 +0200
+++ b/src/HOL/Bali/Decl.thy	Tue Aug 02 10:36:50 2011 +0200
@@ -5,7 +5,8 @@
 *}
 
 theory Decl
-imports Term Table (** order is significant, because of clash for "var" **)
+imports Term Table
+  (** order is significant, because of clash for "var" **)
 begin
 
 text {*
diff -r 8c1dfd6c2262 -r 5cfc1c36ae97 src/HOL/Decision_Procs/Cooper.thy
--- a/src/HOL/Decision_Procs/Cooper.thy	Tue Aug 02 10:03:14 2011 +0200
+++ b/src/HOL/Decision_Procs/Cooper.thy	Tue Aug 02 10:36:50 2011 +0200
@@ -3,7 +3,7 @@
 *)
 
 theory Cooper
-imports Complex_Main "~~/src/HOL/Library/Efficient_Nat"
+imports Complex_Main "~~/src/HOL/Library/Efficient_Nat" "~~/src/HOL/Library/Old_Recdef"
 uses ("cooper_tac.ML")
 begin
 
diff -r 8c1dfd6c2262 -r 5cfc1c36ae97 src/HOL/Decision_Procs/Ferrack.thy
--- a/src/HOL/Decision_Procs/Ferrack.thy	Tue Aug 02 10:03:14 2011 +0200
+++ b/src/HOL/Decision_Procs/Ferrack.thy	Tue Aug 02 10:36:50 2011 +0200
@@ -4,7 +4,7 @@
 
 theory Ferrack
 imports Complex_Main Dense_Linear_Order DP_Library
-  "~~/src/HOL/Library/Efficient_Nat"
+  "~~/src/HOL/Library/Efficient_Nat" "~~/src/HOL/Library/Old_Recdef"
 uses ("ferrack_tac.ML")
 begin
 
diff -r 8c1dfd6c2262 -r 5cfc1c36ae97 src/HOL/Decision_Procs/MIR.thy
--- a/src/HOL/Decision_Procs/MIR.thy	Tue Aug 02 10:03:14 2011 +0200
+++ b/src/HOL/Decision_Procs/MIR.thy	Tue Aug 02 10:36:50 2011 +0200
@@ -4,7 +4,7 @@
 
 theory MIR
 imports Complex_Main Dense_Linear_Order DP_Library
-  "~~/src/HOL/Library/Efficient_Nat"
+  "~~/src/HOL/Library/Efficient_Nat" "~~/src/HOL/Library/Old_Recdef"
 uses ("mir_tac.ML")
 begin
 
diff -r 8c1dfd6c2262 -r 5cfc1c36ae97 src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Tue Aug 02 10:03:14 2011 +0200
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Tue Aug 02 10:36:50 2011 +0200
@@ -6,7 +6,7 @@
 
 theory Parametric_Ferrante_Rackoff
 imports Reflected_Multivariate_Polynomial Dense_Linear_Order DP_Library
-  "~~/src/HOL/Library/Efficient_Nat"
+  "~~/src/HOL/Library/Efficient_Nat" "~~/src/HOL/Library/Old_Recdef"
 begin
 
 subsection {* Terms *}
diff -r 8c1dfd6c2262 -r 5cfc1c36ae97 src/HOL/Induct/Sexp.thy
--- a/src/HOL/Induct/Sexp.thy	Tue Aug 02 10:03:14 2011 +0200
+++ b/src/HOL/Induct/Sexp.thy	Tue Aug 02 10:36:50 2011 +0200
@@ -6,7 +6,7 @@
 structures by hand.
 *)
 
-theory Sexp imports Main begin
+theory Sexp imports Main "~~/src/HOL/Library/Old_Recdef" begin
 
 type_synonym 'a item = "'a Datatype.item"
 abbreviation "Leaf == Datatype.Leaf"
diff -r 8c1dfd6c2262 -r 5cfc1c36ae97 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Tue Aug 02 10:03:14 2011 +0200
+++ b/src/HOL/IsaMakefile	Tue Aug 02 10:36:50 2011 +0200
@@ -292,7 +292,6 @@
   Quotient.thy \
   Random.thy \
   Random_Sequence.thy \
-  Recdef.thy \
   Record.thy \
   Refute.thy \
   Semiring_Normalization.thy \
@@ -359,7 +358,6 @@
   Tools/Quotient/quotient_tacs.ML \
   Tools/Quotient/quotient_term.ML \
   Tools/Quotient/quotient_typ.ML \
-  Tools/recdef.ML \
   Tools/record.ML \
   Tools/semiring_normalizer.ML \
   Tools/Sledgehammer/async_manager.ML \
@@ -389,15 +387,6 @@
   Tools/string_code.ML \
   Tools/string_syntax.ML \
   Tools/transfer.ML \
-  Tools/TFL/casesplit.ML \
-  Tools/TFL/dcterm.ML \
-  Tools/TFL/post.ML \
-  Tools/TFL/rules.ML \
-  Tools/TFL/tfl.ML \
-  Tools/TFL/thms.ML \
-  Tools/TFL/thry.ML \
-  Tools/TFL/usyntax.ML \
-  Tools/TFL/utils.ML
 
 $(OUT)/HOL-Main: main.ML $(MAIN_DEPENDENCIES)
 	@$(ISABELLE_TOOL) usedir -b -f main.ML -g true $(OUT)/Pure HOL-Main
@@ -464,7 +453,8 @@
   Library/List_lexord.thy Library/Mapping.thy Library/Monad_Syntax.thy	\
   Library/More_List.thy Library/More_Set.thy Library/Multiset.thy	\
   Library/Nat_Bijection.thy Library/Nested_Environment.thy		\
-  Library/Numeral_Type.thy Library/OptionalSugar.thy			\
+  Library/Numeral_Type.thy Library/Old_Recdef.thy 			\
+  Library/OptionalSugar.thy						\
   Library/Order_Relation.thy Library/Permutation.thy			\
   Library/Permutations.thy Library/Poly_Deriv.thy			\
   Library/Polynomial.thy Library/Predicate_Compile_Quickcheck.thy	\
@@ -486,7 +476,11 @@
   Library/While_Combinator.thy Library/Zorn.thy				\
   $(SRC)/Tools/adhoc_overloading.ML Library/positivstellensatz.ML	\
   Library/reflection.ML Library/reify_data.ML				\
-  Library/document/root.bib Library/document/root.tex
+  Library/document/root.bib Library/document/root.tex			\
+  Tools/TFL/casesplit.ML Tools/TFL/dcterm.ML Tools/TFL/post.ML		\
+  Tools/TFL/rules.ML Tools/TFL/tfl.ML Tools/TFL/thms.ML			\
+  Tools/TFL/thry.ML Tools/TFL/usyntax.ML Tools/TFL/utils.ML		\
+  Tools/recdef.ML
 	@cd Library; $(ISABELLE_TOOL) usedir -b $(OUT)/HOL HOL-Library
 
 
diff -r 8c1dfd6c2262 -r 5cfc1c36ae97 src/HOL/Library/Library.thy
--- a/src/HOL/Library/Library.thy	Tue Aug 02 10:03:14 2011 +0200
+++ b/src/HOL/Library/Library.thy	Tue Aug 02 10:36:50 2011 +0200
@@ -39,6 +39,7 @@
   Multiset
   Nested_Environment
   Numeral_Type
+  Old_Recdef
   OptionalSugar
   Option_ord
   Permutation
diff -r 8c1dfd6c2262 -r 5cfc1c36ae97 src/HOL/Library/More_List.thy
--- a/src/HOL/Library/More_List.thy	Tue Aug 02 10:03:14 2011 +0200
+++ b/src/HOL/Library/More_List.thy	Tue Aug 02 10:36:50 2011 +0200
@@ -35,7 +35,7 @@
   "fold f (rev xs) = foldr f xs"
   by (simp add: foldr_fold_rev)
   
-lemma fold_cong [fundef_cong, recdef_cong]:
+lemma fold_cong [fundef_cong]:
   "a = b \<Longrightarrow> xs = ys \<Longrightarrow> (\<And>x. x \<in> set xs \<Longrightarrow> f x = g x)
     \<Longrightarrow> fold f xs a = fold g ys b"
   by (induct ys arbitrary: a b xs) simp_all
diff -r 8c1dfd6c2262 -r 5cfc1c36ae97 src/HOL/Library/Old_Recdef.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Old_Recdef.thy	Tue Aug 02 10:36:50 2011 +0200
@@ -0,0 +1,214 @@
+(*  Title:      HOL/Library/Old_Recdef.thy
+    Author:     Konrad Slind and Markus Wenzel, TU Muenchen
+*)
+
+header {* TFL: recursive function definitions *}
+
+theory Old_Recdef
+imports Main
+uses
+  ("~~/src/HOL/Tools/TFL/casesplit.ML")
+  ("~~/src/HOL/Tools/TFL/utils.ML")
+  ("~~/src/HOL/Tools/TFL/usyntax.ML")
+  ("~~/src/HOL/Tools/TFL/dcterm.ML")
+  ("~~/src/HOL/Tools/TFL/thms.ML")
+  ("~~/src/HOL/Tools/TFL/rules.ML")
+  ("~~/src/HOL/Tools/TFL/thry.ML")
+  ("~~/src/HOL/Tools/TFL/tfl.ML")
+  ("~~/src/HOL/Tools/TFL/post.ML")
+  ("~~/src/HOL/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)"
+
+definition
+  cut        :: "('a => 'b) => ('a * 'a)set => 'a => 'a => 'b" where
+  "cut f r x == (%y. if (y,x):r then f y else undefined)"
+
+definition
+  adm_wf :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => bool" where
+  "adm_wf R F == ALL f g x.
+     (ALL z. (z, x) : R --> f z = g z) --> F f x = F g x"
+
+definition
+  wfrec :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b" where
+  "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: fun_eq_iff 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
+apply (blast intro: wfrec)
+done
+
+
+subsection {* Nitpick setup *}
+
+axiomatization wf_wfrec :: "('a \<times> 'a \<Rightarrow> bool) \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
+
+definition wf_wfrec' :: "('a \<times> 'a \<Rightarrow> bool) \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
+[nitpick_simp]: "wf_wfrec' R F x = F (cut (wf_wfrec R F) R x) x"
+
+definition wfrec' ::  "('a \<times> 'a \<Rightarrow> bool) \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
+"wfrec' R F x \<equiv> if wf R then wf_wfrec' R F x
+                else THE y. wfrec_rel R (%f x. F (cut f R x) x) x y"
+
+setup {*
+  Nitpick_HOL.register_ersatz_global
+    [(@{const_name wf_wfrec}, @{const_name wf_wfrec'}),
+     (@{const_name wfrec}, @{const_name wfrec'})]
+*}
+
+hide_const (open) wf_wfrec wf_wfrec' wfrec'
+hide_fact (open) wf_wfrec'_def wfrec'_def
+
+
+subsection {* Lemmas for TFL *}
+
+lemma tfl_wf_induct: "ALL R. wf R -->  
+       (ALL P. (ALL x. (ALL y. (y,x):R --> P y) --> P x) --> (ALL x. P x))"
+apply clarify
+apply (rule_tac r = R and P = P and a = x in wf_induct, assumption, blast)
+done
+
+lemma tfl_cut_apply: "ALL f R. (x,a):R --> (cut f R a)(x) = f(x)"
+apply clarify
+apply (rule cut_apply, assumption)
+done
+
+lemma tfl_wfrec:
+     "ALL M R f. (f=wfrec R M) --> wf R --> (ALL x. f x = M (cut f R x) x)"
+apply clarify
+apply (erule wfrec)
+done
+
+lemma tfl_eq_True: "(x = True) --> x"
+  by blast
+
+lemma tfl_rev_eq_mp: "(x = y) --> y --> x";
+  by blast
+
+lemma tfl_simp_thm: "(x --> y) --> (x = x') --> (x' --> y)"
+  by blast
+
+lemma tfl_P_imp_P_iff_True: "P ==> P = True"
+  by blast
+
+lemma tfl_imp_trans: "(A --> B) ==> (B --> C) ==> (A --> C)"
+  by blast
+
+lemma tfl_disj_assoc: "(a \<or> b) \<or> c == a \<or> (b \<or> c)"
+  by simp
+
+lemma tfl_disjE: "P \<or> Q ==> P --> R ==> Q --> R ==> R"
+  by blast
+
+lemma tfl_exE: "\<exists>x. P x ==> \<forall>x. P x --> Q ==> Q"
+  by blast
+
+use "~~/src/HOL/Tools/TFL/casesplit.ML"
+use "~~/src/HOL/Tools/TFL/utils.ML"
+use "~~/src/HOL/Tools/TFL/usyntax.ML"
+use "~~/src/HOL/Tools/TFL/dcterm.ML"
+use "~~/src/HOL/Tools/TFL/thms.ML"
+use "~~/src/HOL/Tools/TFL/rules.ML"
+use "~~/src/HOL/Tools/TFL/thry.ML"
+use "~~/src/HOL/Tools/TFL/tfl.ML"
+use "~~/src/HOL/Tools/TFL/post.ML"
+use "~~/src/HOL/Tools/recdef.ML"
+setup Recdef.setup
+
+text {*Wellfoundedness of @{text same_fst}*}
+
+definition
+ same_fst :: "('a => bool) => ('a => ('b * 'b)set) => (('a*'b)*('a*'b))set"
+where
+    "same_fst P R == {((x',y'),(x,y)) . x'=x & P x & (y',y) : R x}"
+   --{*For @{text rec_def} declarations where the first n parameters
+       stay unchanged in the recursive call. *}
+
+lemma same_fstI [intro!]:
+     "[| P x; (y',y) : R x |] ==> ((x,y'),(x,y)) : same_fst P R"
+by (simp add: same_fst_def)
+
+lemma wf_same_fst:
+  assumes prem: "(!!x. P x ==> wf(R x))"
+  shows "wf(same_fst P R)"
+apply (simp cong del: imp_cong add: wf_def same_fst_def)
+apply (intro strip)
+apply (rename_tac a b)
+apply (case_tac "wf (R a)")
+ apply (erule_tac a = b in wf_induct, blast)
+apply (blast intro: prem)
+done
+
+text {*Rule setup*}
+
+lemmas [recdef_simp] =
+  inv_image_def
+  measure_def
+  lex_prod_def
+  same_fst_def
+  less_Suc_eq [THEN iffD2]
+
+lemmas [recdef_cong] =
+  if_cong let_cong image_cong INT_cong UN_cong bex_cong ball_cong imp_cong
+  map_cong filter_cong takeWhile_cong dropWhile_cong foldl_cong foldr_cong 
+
+lemmas [recdef_wf] =
+  wf_trancl
+  wf_less_than
+  wf_lex_prod
+  wf_inv_image
+  wf_measure
+  wf_measures
+  wf_pred_nat
+  wf_same_fst
+  wf_empty
+
+end
diff -r 8c1dfd6c2262 -r 5cfc1c36ae97 src/HOL/List.thy
--- a/src/HOL/List.thy	Tue Aug 02 10:03:14 2011 +0200
+++ b/src/HOL/List.thy	Tue Aug 02 10:36:50 2011 +0200
@@ -5,7 +5,7 @@
 header {* The datatype of finite lists *}
 
 theory List
-imports Plain Presburger Recdef Code_Numeral Quotient ATP
+imports Plain Presburger Code_Numeral Quotient ATP
 uses
   ("Tools/list_code.ML")
   ("Tools/list_to_set_comprehension.ML")
@@ -800,7 +800,7 @@
 lemma map_eq_conv[simp]: "(map f xs = map g xs) = (!x : set xs. f x = g x)"
 by (induct xs) auto
 
-lemma map_cong [fundef_cong, recdef_cong]:
+lemma map_cong [fundef_cong]:
   "xs = ys \<Longrightarrow> (\<And>x. x \<in> set ys \<Longrightarrow> f x = g x) \<Longrightarrow> map f xs = map g ys"
   by simp
 
@@ -1237,7 +1237,7 @@
   (\<exists>us vs. ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs)"
 by(auto dest:Cons_eq_filterD)
 
-lemma filter_cong[fundef_cong, recdef_cong]:
+lemma filter_cong[fundef_cong]:
  "xs = ys \<Longrightarrow> (\<And>x. x \<in> set ys \<Longrightarrow> P x = Q x) \<Longrightarrow> filter P xs = filter Q ys"
 apply simp
 apply(erule thin_rl)
@@ -2003,12 +2003,12 @@
 apply(auto)
 done
 
-lemma takeWhile_cong [fundef_cong, recdef_cong]:
+lemma takeWhile_cong [fundef_cong]:
   "[| l = k; !!x. x : set l ==> P x = Q x |] 
   ==> takeWhile P l = takeWhile Q k"
 by (induct k arbitrary: l) (simp_all)
 
-lemma dropWhile_cong [fundef_cong, recdef_cong]:
+lemma dropWhile_cong [fundef_cong]:
   "[| l = k; !!x. x : set l ==> P x = Q x |] 
   ==> dropWhile P l = dropWhile Q k"
 by (induct k arbitrary: l, simp_all)
@@ -2349,12 +2349,12 @@
   shows "foldl (\<lambda>s x. f x s) (h s) xs = h (foldl (\<lambda>s x. g x s) s xs)"
   by (rule sym, insert assms, induct xs arbitrary: s) (simp_all add: fun_eq_iff)
 
-lemma foldl_cong [fundef_cong, recdef_cong]:
+lemma foldl_cong [fundef_cong]:
   "[| a = b; l = k; !!a x. x : set l ==> f a x = g a x |] 
   ==> foldl f a l = foldl g b k"
 by (induct k arbitrary: a b l) simp_all
 
-lemma foldr_cong [fundef_cong, recdef_cong]:
+lemma foldr_cong [fundef_cong]:
   "[| a = b; l = k; !!a x. x : set l ==> f x a = g x a |] 
   ==> foldr f l a = foldr g k b"
 by (induct k arbitrary: a b l) simp_all
@@ -4586,7 +4586,7 @@
 definition
   "measures fs = inv_image (lex less_than) (%a. map (%f. f a) fs)"
 
-lemma wf_measures[recdef_wf, simp]: "wf (measures fs)"
+lemma wf_measures[simp]: "wf (measures fs)"
 unfolding measures_def
 by blast
 
diff -r 8c1dfd6c2262 -r 5cfc1c36ae97 src/HOL/MicroJava/J/TypeRel.thy
--- a/src/HOL/MicroJava/J/TypeRel.thy	Tue Aug 02 10:03:14 2011 +0200
+++ b/src/HOL/MicroJava/J/TypeRel.thy	Tue Aug 02 10:36:50 2011 +0200
@@ -4,7 +4,7 @@
 
 header {* \isaheader{Relations between Java Types} *}
 
-theory TypeRel imports Decl begin
+theory TypeRel imports Decl "~~/src/HOL/Library/Old_Recdef" begin
 
 -- "direct subclass, cf. 8.1.3"
 
diff -r 8c1dfd6c2262 -r 5cfc1c36ae97 src/HOL/NanoJava/TypeRel.thy
--- a/src/HOL/NanoJava/TypeRel.thy	Tue Aug 02 10:03:14 2011 +0200
+++ b/src/HOL/NanoJava/TypeRel.thy	Tue Aug 02 10:36:50 2011 +0200
@@ -4,7 +4,7 @@
 
 header "Type relations"
 
-theory TypeRel imports Decl begin
+theory TypeRel imports Decl "~~/src/HOL/Library/Old_Recdef" begin
 
 consts
   subcls1 :: "(cname \<times> cname) set"  --{* subclass *}
diff -r 8c1dfd6c2262 -r 5cfc1c36ae97 src/HOL/Nitpick.thy
--- a/src/HOL/Nitpick.thy	Tue Aug 02 10:03:14 2011 +0200
+++ b/src/HOL/Nitpick.thy	Tue Aug 02 10:36:50 2011 +0200
@@ -82,15 +82,6 @@
 definition wf' :: "('a \<times> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
 "wf' r \<equiv> acyclic r \<and> (finite r \<or> unknown)"
 
-axiomatization wf_wfrec :: "('a \<times> 'a \<Rightarrow> bool) \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
-
-definition wf_wfrec' :: "('a \<times> 'a \<Rightarrow> bool) \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
-[nitpick_simp]: "wf_wfrec' R F x = F (Recdef.cut (wf_wfrec R F) R x) x"
-
-definition wfrec' ::  "('a \<times> 'a \<Rightarrow> bool) \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
-"wfrec' R F x \<equiv> if wf R then wf_wfrec' R F x
-                else THE y. wfrec_rel R (%f x. F (Recdef.cut f R x) x) x y"
-
 definition card' :: "('a \<Rightarrow> bool) \<Rightarrow> nat" where
 "card' A \<equiv> if finite A then length (SOME xs. set xs = A \<and> distinct xs) else 0"
 
@@ -238,14 +229,14 @@
 setup {* Nitpick_Isar.setup *}
 
 hide_const (open) unknown is_unknown bisim bisim_iterator_max Quot safe_The
-    FunBox PairBox Word prod refl' wf' wf_wfrec wf_wfrec' wfrec' card' setsum'
+    FunBox PairBox Word prod refl' wf' card' setsum'
     fold_graph' nat_gcd nat_lcm int_gcd int_lcm Frac Abs_Frac Rep_Frac zero_frac
     one_frac num denom norm_frac frac plus_frac times_frac uminus_frac
     number_of_frac inverse_frac less_frac less_eq_frac of_frac
 hide_type (open) iota bisim_iterator fun_box pair_box unsigned_bit signed_bit
     word
 hide_fact (open) Ex1_unfold rtrancl_unfold rtranclp_unfold tranclp_unfold
-    prod_def refl'_def wf'_def wf_wfrec'_def wfrec'_def card'_def setsum'_def
+    prod_def refl'_def wf'_def card'_def setsum'_def
     fold_graph'_def The_psimp Eps_psimp unit_case_unfold nat_case_unfold
     list_size_simp nat_gcd_def nat_lcm_def int_gcd_def int_lcm_def Frac_def
     zero_frac_def one_frac_def num_def denom_def norm_frac_def frac_def
diff -r 8c1dfd6c2262 -r 5cfc1c36ae97 src/HOL/Recdef.thy
--- a/src/HOL/Recdef.thy	Tue Aug 02 10:03:14 2011 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,189 +0,0 @@
-(*  Title:      HOL/Recdef.thy
-    Author:     Konrad Slind and Markus Wenzel, TU Muenchen
-*)
-
-header {* TFL: recursive function definitions *}
-
-theory Recdef
-imports Plain Hilbert_Choice
-uses
-  ("Tools/TFL/casesplit.ML")
-  ("Tools/TFL/utils.ML")
-  ("Tools/TFL/usyntax.ML")
-  ("Tools/TFL/dcterm.ML")
-  ("Tools/TFL/thms.ML")
-  ("Tools/TFL/rules.ML")
-  ("Tools/TFL/thry.ML")
-  ("Tools/TFL/tfl.ML")
-  ("Tools/TFL/post.ML")
-  ("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)"
-
-definition
-  cut        :: "('a => 'b) => ('a * 'a)set => 'a => 'a => 'b" where
-  "cut f r x == (%y. if (y,x):r then f y else undefined)"
-
-definition
-  adm_wf :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => bool" where
-  "adm_wf R F == ALL f g x.
-     (ALL z. (z, x) : R --> f z = g z) --> F f x = F g x"
-
-definition
-  wfrec :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b" where
-  "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: fun_eq_iff 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
-apply (blast intro: wfrec)
-done
-
-
-lemma tfl_wf_induct: "ALL R. wf R -->  
-       (ALL P. (ALL x. (ALL y. (y,x):R --> P y) --> P x) --> (ALL x. P x))"
-apply clarify
-apply (rule_tac r = R and P = P and a = x in wf_induct, assumption, blast)
-done
-
-lemma tfl_cut_apply: "ALL f R. (x,a):R --> (cut f R a)(x) = f(x)"
-apply clarify
-apply (rule cut_apply, assumption)
-done
-
-lemma tfl_wfrec:
-     "ALL M R f. (f=wfrec R M) --> wf R --> (ALL x. f x = M (cut f R x) x)"
-apply clarify
-apply (erule wfrec)
-done
-
-lemma tfl_eq_True: "(x = True) --> x"
-  by blast
-
-lemma tfl_rev_eq_mp: "(x = y) --> y --> x";
-  by blast
-
-lemma tfl_simp_thm: "(x --> y) --> (x = x') --> (x' --> y)"
-  by blast
-
-lemma tfl_P_imp_P_iff_True: "P ==> P = True"
-  by blast
-
-lemma tfl_imp_trans: "(A --> B) ==> (B --> C) ==> (A --> C)"
-  by blast
-
-lemma tfl_disj_assoc: "(a \<or> b) \<or> c == a \<or> (b \<or> c)"
-  by simp
-
-lemma tfl_disjE: "P \<or> Q ==> P --> R ==> Q --> R ==> R"
-  by blast
-
-lemma tfl_exE: "\<exists>x. P x ==> \<forall>x. P x --> Q ==> Q"
-  by blast
-
-use "Tools/TFL/casesplit.ML"
-use "Tools/TFL/utils.ML"
-use "Tools/TFL/usyntax.ML"
-use "Tools/TFL/dcterm.ML"
-use "Tools/TFL/thms.ML"
-use "Tools/TFL/rules.ML"
-use "Tools/TFL/thry.ML"
-use "Tools/TFL/tfl.ML"
-use "Tools/TFL/post.ML"
-use "Tools/recdef.ML"
-setup Recdef.setup
-
-text {*Wellfoundedness of @{text same_fst}*}
-
-definition
- same_fst :: "('a => bool) => ('a => ('b * 'b)set) => (('a*'b)*('a*'b))set"
-where
-    "same_fst P R == {((x',y'),(x,y)) . x'=x & P x & (y',y) : R x}"
-   --{*For @{text rec_def} declarations where the first n parameters
-       stay unchanged in the recursive call. *}
-
-lemma same_fstI [intro!]:
-     "[| P x; (y',y) : R x |] ==> ((x,y'),(x,y)) : same_fst P R"
-by (simp add: same_fst_def)
-
-lemma wf_same_fst:
-  assumes prem: "(!!x. P x ==> wf(R x))"
-  shows "wf(same_fst P R)"
-apply (simp cong del: imp_cong add: wf_def same_fst_def)
-apply (intro strip)
-apply (rename_tac a b)
-apply (case_tac "wf (R a)")
- apply (erule_tac a = b in wf_induct, blast)
-apply (blast intro: prem)
-done
-
-text {*Rule setup*}
-
-lemmas [recdef_simp] =
-  inv_image_def
-  measure_def
-  lex_prod_def
-  same_fst_def
-  less_Suc_eq [THEN iffD2]
-
-lemmas [recdef_cong] =
-  if_cong let_cong image_cong INT_cong UN_cong bex_cong ball_cong imp_cong
-
-lemmas [recdef_wf] =
-  wf_trancl
-  wf_less_than
-  wf_lex_prod
-  wf_inv_image
-  wf_measure
-  wf_pred_nat
-  wf_same_fst
-  wf_empty
-
-end
diff -r 8c1dfd6c2262 -r 5cfc1c36ae97 src/HOL/Subst/Unify.thy
--- a/src/HOL/Subst/Unify.thy	Tue Aug 02 10:03:14 2011 +0200
+++ b/src/HOL/Subst/Unify.thy	Tue Aug 02 10:36:50 2011 +0200
@@ -6,7 +6,7 @@
 header {* Unification Algorithm *}
 
 theory Unify
-imports Unifier
+imports Unifier "~~/src/HOL/Library/Old_Recdef"
 begin
 
 subsection {* Substitution and Unification in Higher-Order Logic. *}
diff -r 8c1dfd6c2262 -r 5cfc1c36ae97 src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Aug 02 10:03:14 2011 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Aug 02 10:36:50 2011 +0200
@@ -1779,7 +1779,7 @@
                                    "too many nested definitions (" ^
                                    string_of_int depth ^ ") while expanding " ^
                                    quote s)
-                else if s = @{const_name wfrec'} then
+                else if s = "Old_Recdef.wfrec'" (* FIXME unchecked! *) then
                   (do_term (depth + 1) Ts (s_betapplys Ts (def, ts)), [])
                 else if not unfold andalso
                      size_of_term def > def_inline_threshold () then
@@ -1873,9 +1873,7 @@
   [(@{const_name card}, @{const_name card'}),
    (@{const_name setsum}, @{const_name setsum'}),
    (@{const_name fold_graph}, @{const_name fold_graph'}),
-   (@{const_name wf}, @{const_name wf'}),
-   (@{const_name wf_wfrec}, @{const_name wf_wfrec'}),
-   (@{const_name wfrec}, @{const_name wfrec'})]
+   (@{const_name wf}, @{const_name wf'})]
 
 fun ersatz_table ctxt =
  (basic_ersatz_table @ #ersatz_table (Data.get (Context.Proof ctxt)))
diff -r 8c1dfd6c2262 -r 5cfc1c36ae97 src/HOL/Tools/TFL/rules.ML
--- a/src/HOL/Tools/TFL/rules.ML	Tue Aug 02 10:03:14 2011 +0200
+++ b/src/HOL/Tools/TFL/rules.ML	Tue Aug 02 10:36:50 2011 +0200
@@ -445,7 +445,7 @@
 fun is_cong thm =
   case (Thm.prop_of thm)
      of (Const("==>",_)$(Const(@{const_name Trueprop},_)$ _) $
-         (Const("==",_) $ (Const (@{const_name Recdef.cut},_) $ f $ R $ a $ x) $ _)) => false
+         (Const("==",_) $ (Const (@{const_name Old_Recdef.cut},_) $ f $ R $ a $ x) $ _)) => false
       | _ => true;
 
 
@@ -645,7 +645,7 @@
   end;
 
 fun restricted t = is_some (USyntax.find_term
-                            (fn (Const(@{const_name Recdef.cut},_)) =>true | _ => false)
+                            (fn (Const(@{const_name Old_Recdef.cut},_)) =>true | _ => false)
                             t)
 
 fun CONTEXT_REWRITE_RULE (func, G, cut_lemma, congs) th =
diff -r 8c1dfd6c2262 -r 5cfc1c36ae97 src/HOL/Tools/recdef.ML
--- a/src/HOL/Tools/recdef.ML	Tue Aug 02 10:03:14 2011 +0200
+++ b/src/HOL/Tools/recdef.ML	Tue Aug 02 10:36:50 2011 +0200
@@ -182,7 +182,7 @@
 
 (** add_recdef(_i) **)
 
-fun requires_recdef thy = Theory.requires thy "Recdef" "recursive functions";
+fun requires_recdef thy = Theory.requires thy "Old_Recdef" "recursive functions";
 
 fun gen_add_recdef tfl_fn prep_att prep_hints not_permissive raw_name R eq_srcs hints thy =
   let
diff -r 8c1dfd6c2262 -r 5cfc1c36ae97 src/HOL/ex/InductiveInvariant.thy
--- a/src/HOL/ex/InductiveInvariant.thy	Tue Aug 02 10:03:14 2011 +0200
+++ b/src/HOL/ex/InductiveInvariant.thy	Tue Aug 02 10:36:50 2011 +0200
@@ -4,7 +4,7 @@
 
 header {* Some of the results in Inductive Invariants for Nested Recursion *}
 
-theory InductiveInvariant imports Main begin
+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
diff -r 8c1dfd6c2262 -r 5cfc1c36ae97 src/HOL/ex/Recdefs.thy
--- a/src/HOL/ex/Recdefs.thy	Tue Aug 02 10:03:14 2011 +0200
+++ b/src/HOL/ex/Recdefs.thy	Tue Aug 02 10:36:50 2011 +0200
@@ -7,7 +7,7 @@
 
 header {* Examples of recdef definitions *}
 
-theory Recdefs imports Main begin
+theory Recdefs imports "~~/src/HOL/Library/Old_Recdef" begin
 
 consts fact :: "nat => nat"
 recdef fact  less_than