moved recdef package to HOL/Library/Old_Recdef.thy
authorkrauss
Tue Aug 02 10:36:50 2011 +0200 (2011-08-02)
changeset 440135cfc1c36ae97
parent 44012 8c1dfd6c2262
child 44014 88bd7d74a2c1
moved recdef package to HOL/Library/Old_Recdef.thy
src/HOL/Bali/Basis.thy
src/HOL/Bali/Decl.thy
src/HOL/Decision_Procs/Cooper.thy
src/HOL/Decision_Procs/Ferrack.thy
src/HOL/Decision_Procs/MIR.thy
src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
src/HOL/Induct/Sexp.thy
src/HOL/IsaMakefile
src/HOL/Library/Library.thy
src/HOL/Library/More_List.thy
src/HOL/Library/Old_Recdef.thy
src/HOL/List.thy
src/HOL/MicroJava/J/TypeRel.thy
src/HOL/NanoJava/TypeRel.thy
src/HOL/Nitpick.thy
src/HOL/Recdef.thy
src/HOL/Subst/Unify.thy
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Tools/TFL/rules.ML
src/HOL/Tools/recdef.ML
src/HOL/ex/InductiveInvariant.thy
src/HOL/ex/Recdefs.thy
     1.1 --- a/src/HOL/Bali/Basis.thy	Tue Aug 02 10:03:14 2011 +0200
     1.2 +++ b/src/HOL/Bali/Basis.thy	Tue Aug 02 10:36:50 2011 +0200
     1.3 @@ -3,7 +3,7 @@
     1.4  *)
     1.5  header {* Definitions extending HOL as logical basis of Bali *}
     1.6  
     1.7 -theory Basis imports Main begin
     1.8 +theory Basis imports Main "~~/src/HOL/Library/Old_Recdef" begin
     1.9  
    1.10  
    1.11  section "misc"
     2.1 --- a/src/HOL/Bali/Decl.thy	Tue Aug 02 10:03:14 2011 +0200
     2.2 +++ b/src/HOL/Bali/Decl.thy	Tue Aug 02 10:36:50 2011 +0200
     2.3 @@ -5,7 +5,8 @@
     2.4  *}
     2.5  
     2.6  theory Decl
     2.7 -imports Term Table (** order is significant, because of clash for "var" **)
     2.8 +imports Term Table
     2.9 +  (** order is significant, because of clash for "var" **)
    2.10  begin
    2.11  
    2.12  text {*
     3.1 --- a/src/HOL/Decision_Procs/Cooper.thy	Tue Aug 02 10:03:14 2011 +0200
     3.2 +++ b/src/HOL/Decision_Procs/Cooper.thy	Tue Aug 02 10:36:50 2011 +0200
     3.3 @@ -3,7 +3,7 @@
     3.4  *)
     3.5  
     3.6  theory Cooper
     3.7 -imports Complex_Main "~~/src/HOL/Library/Efficient_Nat"
     3.8 +imports Complex_Main "~~/src/HOL/Library/Efficient_Nat" "~~/src/HOL/Library/Old_Recdef"
     3.9  uses ("cooper_tac.ML")
    3.10  begin
    3.11  
     4.1 --- a/src/HOL/Decision_Procs/Ferrack.thy	Tue Aug 02 10:03:14 2011 +0200
     4.2 +++ b/src/HOL/Decision_Procs/Ferrack.thy	Tue Aug 02 10:36:50 2011 +0200
     4.3 @@ -4,7 +4,7 @@
     4.4  
     4.5  theory Ferrack
     4.6  imports Complex_Main Dense_Linear_Order DP_Library
     4.7 -  "~~/src/HOL/Library/Efficient_Nat"
     4.8 +  "~~/src/HOL/Library/Efficient_Nat" "~~/src/HOL/Library/Old_Recdef"
     4.9  uses ("ferrack_tac.ML")
    4.10  begin
    4.11  
     5.1 --- a/src/HOL/Decision_Procs/MIR.thy	Tue Aug 02 10:03:14 2011 +0200
     5.2 +++ b/src/HOL/Decision_Procs/MIR.thy	Tue Aug 02 10:36:50 2011 +0200
     5.3 @@ -4,7 +4,7 @@
     5.4  
     5.5  theory MIR
     5.6  imports Complex_Main Dense_Linear_Order DP_Library
     5.7 -  "~~/src/HOL/Library/Efficient_Nat"
     5.8 +  "~~/src/HOL/Library/Efficient_Nat" "~~/src/HOL/Library/Old_Recdef"
     5.9  uses ("mir_tac.ML")
    5.10  begin
    5.11  
     6.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Tue Aug 02 10:03:14 2011 +0200
     6.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Tue Aug 02 10:36:50 2011 +0200
     6.3 @@ -6,7 +6,7 @@
     6.4  
     6.5  theory Parametric_Ferrante_Rackoff
     6.6  imports Reflected_Multivariate_Polynomial Dense_Linear_Order DP_Library
     6.7 -  "~~/src/HOL/Library/Efficient_Nat"
     6.8 +  "~~/src/HOL/Library/Efficient_Nat" "~~/src/HOL/Library/Old_Recdef"
     6.9  begin
    6.10  
    6.11  subsection {* Terms *}
     7.1 --- a/src/HOL/Induct/Sexp.thy	Tue Aug 02 10:03:14 2011 +0200
     7.2 +++ b/src/HOL/Induct/Sexp.thy	Tue Aug 02 10:36:50 2011 +0200
     7.3 @@ -6,7 +6,7 @@
     7.4  structures by hand.
     7.5  *)
     7.6  
     7.7 -theory Sexp imports Main begin
     7.8 +theory Sexp imports Main "~~/src/HOL/Library/Old_Recdef" begin
     7.9  
    7.10  type_synonym 'a item = "'a Datatype.item"
    7.11  abbreviation "Leaf == Datatype.Leaf"
     8.1 --- a/src/HOL/IsaMakefile	Tue Aug 02 10:03:14 2011 +0200
     8.2 +++ b/src/HOL/IsaMakefile	Tue Aug 02 10:36:50 2011 +0200
     8.3 @@ -292,7 +292,6 @@
     8.4    Quotient.thy \
     8.5    Random.thy \
     8.6    Random_Sequence.thy \
     8.7 -  Recdef.thy \
     8.8    Record.thy \
     8.9    Refute.thy \
    8.10    Semiring_Normalization.thy \
    8.11 @@ -359,7 +358,6 @@
    8.12    Tools/Quotient/quotient_tacs.ML \
    8.13    Tools/Quotient/quotient_term.ML \
    8.14    Tools/Quotient/quotient_typ.ML \
    8.15 -  Tools/recdef.ML \
    8.16    Tools/record.ML \
    8.17    Tools/semiring_normalizer.ML \
    8.18    Tools/Sledgehammer/async_manager.ML \
    8.19 @@ -389,15 +387,6 @@
    8.20    Tools/string_code.ML \
    8.21    Tools/string_syntax.ML \
    8.22    Tools/transfer.ML \
    8.23 -  Tools/TFL/casesplit.ML \
    8.24 -  Tools/TFL/dcterm.ML \
    8.25 -  Tools/TFL/post.ML \
    8.26 -  Tools/TFL/rules.ML \
    8.27 -  Tools/TFL/tfl.ML \
    8.28 -  Tools/TFL/thms.ML \
    8.29 -  Tools/TFL/thry.ML \
    8.30 -  Tools/TFL/usyntax.ML \
    8.31 -  Tools/TFL/utils.ML
    8.32  
    8.33  $(OUT)/HOL-Main: main.ML $(MAIN_DEPENDENCIES)
    8.34  	@$(ISABELLE_TOOL) usedir -b -f main.ML -g true $(OUT)/Pure HOL-Main
    8.35 @@ -464,7 +453,8 @@
    8.36    Library/List_lexord.thy Library/Mapping.thy Library/Monad_Syntax.thy	\
    8.37    Library/More_List.thy Library/More_Set.thy Library/Multiset.thy	\
    8.38    Library/Nat_Bijection.thy Library/Nested_Environment.thy		\
    8.39 -  Library/Numeral_Type.thy Library/OptionalSugar.thy			\
    8.40 +  Library/Numeral_Type.thy Library/Old_Recdef.thy 			\
    8.41 +  Library/OptionalSugar.thy						\
    8.42    Library/Order_Relation.thy Library/Permutation.thy			\
    8.43    Library/Permutations.thy Library/Poly_Deriv.thy			\
    8.44    Library/Polynomial.thy Library/Predicate_Compile_Quickcheck.thy	\
    8.45 @@ -486,7 +476,11 @@
    8.46    Library/While_Combinator.thy Library/Zorn.thy				\
    8.47    $(SRC)/Tools/adhoc_overloading.ML Library/positivstellensatz.ML	\
    8.48    Library/reflection.ML Library/reify_data.ML				\
    8.49 -  Library/document/root.bib Library/document/root.tex
    8.50 +  Library/document/root.bib Library/document/root.tex			\
    8.51 +  Tools/TFL/casesplit.ML Tools/TFL/dcterm.ML Tools/TFL/post.ML		\
    8.52 +  Tools/TFL/rules.ML Tools/TFL/tfl.ML Tools/TFL/thms.ML			\
    8.53 +  Tools/TFL/thry.ML Tools/TFL/usyntax.ML Tools/TFL/utils.ML		\
    8.54 +  Tools/recdef.ML
    8.55  	@cd Library; $(ISABELLE_TOOL) usedir -b $(OUT)/HOL HOL-Library
    8.56  
    8.57  
     9.1 --- a/src/HOL/Library/Library.thy	Tue Aug 02 10:03:14 2011 +0200
     9.2 +++ b/src/HOL/Library/Library.thy	Tue Aug 02 10:36:50 2011 +0200
     9.3 @@ -39,6 +39,7 @@
     9.4    Multiset
     9.5    Nested_Environment
     9.6    Numeral_Type
     9.7 +  Old_Recdef
     9.8    OptionalSugar
     9.9    Option_ord
    9.10    Permutation
    10.1 --- a/src/HOL/Library/More_List.thy	Tue Aug 02 10:03:14 2011 +0200
    10.2 +++ b/src/HOL/Library/More_List.thy	Tue Aug 02 10:36:50 2011 +0200
    10.3 @@ -35,7 +35,7 @@
    10.4    "fold f (rev xs) = foldr f xs"
    10.5    by (simp add: foldr_fold_rev)
    10.6    
    10.7 -lemma fold_cong [fundef_cong, recdef_cong]:
    10.8 +lemma fold_cong [fundef_cong]:
    10.9    "a = b \<Longrightarrow> xs = ys \<Longrightarrow> (\<And>x. x \<in> set xs \<Longrightarrow> f x = g x)
   10.10      \<Longrightarrow> fold f xs a = fold g ys b"
   10.11    by (induct ys arbitrary: a b xs) simp_all
    11.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.2 +++ b/src/HOL/Library/Old_Recdef.thy	Tue Aug 02 10:36:50 2011 +0200
    11.3 @@ -0,0 +1,214 @@
    11.4 +(*  Title:      HOL/Library/Old_Recdef.thy
    11.5 +    Author:     Konrad Slind and Markus Wenzel, TU Muenchen
    11.6 +*)
    11.7 +
    11.8 +header {* TFL: recursive function definitions *}
    11.9 +
   11.10 +theory Old_Recdef
   11.11 +imports Main
   11.12 +uses
   11.13 +  ("~~/src/HOL/Tools/TFL/casesplit.ML")
   11.14 +  ("~~/src/HOL/Tools/TFL/utils.ML")
   11.15 +  ("~~/src/HOL/Tools/TFL/usyntax.ML")
   11.16 +  ("~~/src/HOL/Tools/TFL/dcterm.ML")
   11.17 +  ("~~/src/HOL/Tools/TFL/thms.ML")
   11.18 +  ("~~/src/HOL/Tools/TFL/rules.ML")
   11.19 +  ("~~/src/HOL/Tools/TFL/thry.ML")
   11.20 +  ("~~/src/HOL/Tools/TFL/tfl.ML")
   11.21 +  ("~~/src/HOL/Tools/TFL/post.ML")
   11.22 +  ("~~/src/HOL/Tools/recdef.ML")
   11.23 +begin
   11.24 +
   11.25 +inductive
   11.26 +  wfrec_rel :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b => bool"
   11.27 +  for R :: "('a * 'a) set"
   11.28 +  and F :: "('a => 'b) => 'a => 'b"
   11.29 +where
   11.30 +  wfrecI: "ALL z. (z, x) : R --> wfrec_rel R F z (g z) ==>
   11.31 +            wfrec_rel R F x (F g x)"
   11.32 +
   11.33 +definition
   11.34 +  cut        :: "('a => 'b) => ('a * 'a)set => 'a => 'a => 'b" where
   11.35 +  "cut f r x == (%y. if (y,x):r then f y else undefined)"
   11.36 +
   11.37 +definition
   11.38 +  adm_wf :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => bool" where
   11.39 +  "adm_wf R F == ALL f g x.
   11.40 +     (ALL z. (z, x) : R --> f z = g z) --> F f x = F g x"
   11.41 +
   11.42 +definition
   11.43 +  wfrec :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b" where
   11.44 +  "wfrec R F == %x. THE y. wfrec_rel R (%f x. F (cut f R x) x) x y"
   11.45 +
   11.46 +subsection{*Well-Founded Recursion*}
   11.47 +
   11.48 +text{*cut*}
   11.49 +
   11.50 +lemma cuts_eq: "(cut f r x = cut g r x) = (ALL y. (y,x):r --> f(y)=g(y))"
   11.51 +by (simp add: fun_eq_iff cut_def)
   11.52 +
   11.53 +lemma cut_apply: "(x,a):r ==> (cut f r a)(x) = f(x)"
   11.54 +by (simp add: cut_def)
   11.55 +
   11.56 +text{*Inductive characterization of wfrec combinator; for details see:
   11.57 +John Harrison, "Inductive definitions: automation and application"*}
   11.58 +
   11.59 +lemma wfrec_unique: "[| adm_wf R F; wf R |] ==> EX! y. wfrec_rel R F x y"
   11.60 +apply (simp add: adm_wf_def)
   11.61 +apply (erule_tac a=x in wf_induct)
   11.62 +apply (rule ex1I)
   11.63 +apply (rule_tac g = "%x. THE y. wfrec_rel R F x y" in wfrec_rel.wfrecI)
   11.64 +apply (fast dest!: theI')
   11.65 +apply (erule wfrec_rel.cases, simp)
   11.66 +apply (erule allE, erule allE, erule allE, erule mp)
   11.67 +apply (fast intro: the_equality [symmetric])
   11.68 +done
   11.69 +
   11.70 +lemma adm_lemma: "adm_wf R (%f x. F (cut f R x) x)"
   11.71 +apply (simp add: adm_wf_def)
   11.72 +apply (intro strip)
   11.73 +apply (rule cuts_eq [THEN iffD2, THEN subst], assumption)
   11.74 +apply (rule refl)
   11.75 +done
   11.76 +
   11.77 +lemma wfrec: "wf(r) ==> wfrec r H a = H (cut (wfrec r H) r a) a"
   11.78 +apply (simp add: wfrec_def)
   11.79 +apply (rule adm_lemma [THEN wfrec_unique, THEN the1_equality], assumption)
   11.80 +apply (rule wfrec_rel.wfrecI)
   11.81 +apply (intro strip)
   11.82 +apply (erule adm_lemma [THEN wfrec_unique, THEN theI'])
   11.83 +done
   11.84 +
   11.85 +
   11.86 +text{** This form avoids giant explosions in proofs.  NOTE USE OF ==*}
   11.87 +lemma def_wfrec: "[| f==wfrec r H;  wf(r) |] ==> f(a) = H (cut f r a) a"
   11.88 +apply auto
   11.89 +apply (blast intro: wfrec)
   11.90 +done
   11.91 +
   11.92 +
   11.93 +subsection {* Nitpick setup *}
   11.94 +
   11.95 +axiomatization wf_wfrec :: "('a \<times> 'a \<Rightarrow> bool) \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
   11.96 +
   11.97 +definition wf_wfrec' :: "('a \<times> 'a \<Rightarrow> bool) \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
   11.98 +[nitpick_simp]: "wf_wfrec' R F x = F (cut (wf_wfrec R F) R x) x"
   11.99 +
  11.100 +definition wfrec' ::  "('a \<times> 'a \<Rightarrow> bool) \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
  11.101 +"wfrec' R F x \<equiv> if wf R then wf_wfrec' R F x
  11.102 +                else THE y. wfrec_rel R (%f x. F (cut f R x) x) x y"
  11.103 +
  11.104 +setup {*
  11.105 +  Nitpick_HOL.register_ersatz_global
  11.106 +    [(@{const_name wf_wfrec}, @{const_name wf_wfrec'}),
  11.107 +     (@{const_name wfrec}, @{const_name wfrec'})]
  11.108 +*}
  11.109 +
  11.110 +hide_const (open) wf_wfrec wf_wfrec' wfrec'
  11.111 +hide_fact (open) wf_wfrec'_def wfrec'_def
  11.112 +
  11.113 +
  11.114 +subsection {* Lemmas for TFL *}
  11.115 +
  11.116 +lemma tfl_wf_induct: "ALL R. wf R -->  
  11.117 +       (ALL P. (ALL x. (ALL y. (y,x):R --> P y) --> P x) --> (ALL x. P x))"
  11.118 +apply clarify
  11.119 +apply (rule_tac r = R and P = P and a = x in wf_induct, assumption, blast)
  11.120 +done
  11.121 +
  11.122 +lemma tfl_cut_apply: "ALL f R. (x,a):R --> (cut f R a)(x) = f(x)"
  11.123 +apply clarify
  11.124 +apply (rule cut_apply, assumption)
  11.125 +done
  11.126 +
  11.127 +lemma tfl_wfrec:
  11.128 +     "ALL M R f. (f=wfrec R M) --> wf R --> (ALL x. f x = M (cut f R x) x)"
  11.129 +apply clarify
  11.130 +apply (erule wfrec)
  11.131 +done
  11.132 +
  11.133 +lemma tfl_eq_True: "(x = True) --> x"
  11.134 +  by blast
  11.135 +
  11.136 +lemma tfl_rev_eq_mp: "(x = y) --> y --> x";
  11.137 +  by blast
  11.138 +
  11.139 +lemma tfl_simp_thm: "(x --> y) --> (x = x') --> (x' --> y)"
  11.140 +  by blast
  11.141 +
  11.142 +lemma tfl_P_imp_P_iff_True: "P ==> P = True"
  11.143 +  by blast
  11.144 +
  11.145 +lemma tfl_imp_trans: "(A --> B) ==> (B --> C) ==> (A --> C)"
  11.146 +  by blast
  11.147 +
  11.148 +lemma tfl_disj_assoc: "(a \<or> b) \<or> c == a \<or> (b \<or> c)"
  11.149 +  by simp
  11.150 +
  11.151 +lemma tfl_disjE: "P \<or> Q ==> P --> R ==> Q --> R ==> R"
  11.152 +  by blast
  11.153 +
  11.154 +lemma tfl_exE: "\<exists>x. P x ==> \<forall>x. P x --> Q ==> Q"
  11.155 +  by blast
  11.156 +
  11.157 +use "~~/src/HOL/Tools/TFL/casesplit.ML"
  11.158 +use "~~/src/HOL/Tools/TFL/utils.ML"
  11.159 +use "~~/src/HOL/Tools/TFL/usyntax.ML"
  11.160 +use "~~/src/HOL/Tools/TFL/dcterm.ML"
  11.161 +use "~~/src/HOL/Tools/TFL/thms.ML"
  11.162 +use "~~/src/HOL/Tools/TFL/rules.ML"
  11.163 +use "~~/src/HOL/Tools/TFL/thry.ML"
  11.164 +use "~~/src/HOL/Tools/TFL/tfl.ML"
  11.165 +use "~~/src/HOL/Tools/TFL/post.ML"
  11.166 +use "~~/src/HOL/Tools/recdef.ML"
  11.167 +setup Recdef.setup
  11.168 +
  11.169 +text {*Wellfoundedness of @{text same_fst}*}
  11.170 +
  11.171 +definition
  11.172 + same_fst :: "('a => bool) => ('a => ('b * 'b)set) => (('a*'b)*('a*'b))set"
  11.173 +where
  11.174 +    "same_fst P R == {((x',y'),(x,y)) . x'=x & P x & (y',y) : R x}"
  11.175 +   --{*For @{text rec_def} declarations where the first n parameters
  11.176 +       stay unchanged in the recursive call. *}
  11.177 +
  11.178 +lemma same_fstI [intro!]:
  11.179 +     "[| P x; (y',y) : R x |] ==> ((x,y'),(x,y)) : same_fst P R"
  11.180 +by (simp add: same_fst_def)
  11.181 +
  11.182 +lemma wf_same_fst:
  11.183 +  assumes prem: "(!!x. P x ==> wf(R x))"
  11.184 +  shows "wf(same_fst P R)"
  11.185 +apply (simp cong del: imp_cong add: wf_def same_fst_def)
  11.186 +apply (intro strip)
  11.187 +apply (rename_tac a b)
  11.188 +apply (case_tac "wf (R a)")
  11.189 + apply (erule_tac a = b in wf_induct, blast)
  11.190 +apply (blast intro: prem)
  11.191 +done
  11.192 +
  11.193 +text {*Rule setup*}
  11.194 +
  11.195 +lemmas [recdef_simp] =
  11.196 +  inv_image_def
  11.197 +  measure_def
  11.198 +  lex_prod_def
  11.199 +  same_fst_def
  11.200 +  less_Suc_eq [THEN iffD2]
  11.201 +
  11.202 +lemmas [recdef_cong] =
  11.203 +  if_cong let_cong image_cong INT_cong UN_cong bex_cong ball_cong imp_cong
  11.204 +  map_cong filter_cong takeWhile_cong dropWhile_cong foldl_cong foldr_cong 
  11.205 +
  11.206 +lemmas [recdef_wf] =
  11.207 +  wf_trancl
  11.208 +  wf_less_than
  11.209 +  wf_lex_prod
  11.210 +  wf_inv_image
  11.211 +  wf_measure
  11.212 +  wf_measures
  11.213 +  wf_pred_nat
  11.214 +  wf_same_fst
  11.215 +  wf_empty
  11.216 +
  11.217 +end
    12.1 --- a/src/HOL/List.thy	Tue Aug 02 10:03:14 2011 +0200
    12.2 +++ b/src/HOL/List.thy	Tue Aug 02 10:36:50 2011 +0200
    12.3 @@ -5,7 +5,7 @@
    12.4  header {* The datatype of finite lists *}
    12.5  
    12.6  theory List
    12.7 -imports Plain Presburger Recdef Code_Numeral Quotient ATP
    12.8 +imports Plain Presburger Code_Numeral Quotient ATP
    12.9  uses
   12.10    ("Tools/list_code.ML")
   12.11    ("Tools/list_to_set_comprehension.ML")
   12.12 @@ -800,7 +800,7 @@
   12.13  lemma map_eq_conv[simp]: "(map f xs = map g xs) = (!x : set xs. f x = g x)"
   12.14  by (induct xs) auto
   12.15  
   12.16 -lemma map_cong [fundef_cong, recdef_cong]:
   12.17 +lemma map_cong [fundef_cong]:
   12.18    "xs = ys \<Longrightarrow> (\<And>x. x \<in> set ys \<Longrightarrow> f x = g x) \<Longrightarrow> map f xs = map g ys"
   12.19    by simp
   12.20  
   12.21 @@ -1237,7 +1237,7 @@
   12.22    (\<exists>us vs. ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs)"
   12.23  by(auto dest:Cons_eq_filterD)
   12.24  
   12.25 -lemma filter_cong[fundef_cong, recdef_cong]:
   12.26 +lemma filter_cong[fundef_cong]:
   12.27   "xs = ys \<Longrightarrow> (\<And>x. x \<in> set ys \<Longrightarrow> P x = Q x) \<Longrightarrow> filter P xs = filter Q ys"
   12.28  apply simp
   12.29  apply(erule thin_rl)
   12.30 @@ -2003,12 +2003,12 @@
   12.31  apply(auto)
   12.32  done
   12.33  
   12.34 -lemma takeWhile_cong [fundef_cong, recdef_cong]:
   12.35 +lemma takeWhile_cong [fundef_cong]:
   12.36    "[| l = k; !!x. x : set l ==> P x = Q x |] 
   12.37    ==> takeWhile P l = takeWhile Q k"
   12.38  by (induct k arbitrary: l) (simp_all)
   12.39  
   12.40 -lemma dropWhile_cong [fundef_cong, recdef_cong]:
   12.41 +lemma dropWhile_cong [fundef_cong]:
   12.42    "[| l = k; !!x. x : set l ==> P x = Q x |] 
   12.43    ==> dropWhile P l = dropWhile Q k"
   12.44  by (induct k arbitrary: l, simp_all)
   12.45 @@ -2349,12 +2349,12 @@
   12.46    shows "foldl (\<lambda>s x. f x s) (h s) xs = h (foldl (\<lambda>s x. g x s) s xs)"
   12.47    by (rule sym, insert assms, induct xs arbitrary: s) (simp_all add: fun_eq_iff)
   12.48  
   12.49 -lemma foldl_cong [fundef_cong, recdef_cong]:
   12.50 +lemma foldl_cong [fundef_cong]:
   12.51    "[| a = b; l = k; !!a x. x : set l ==> f a x = g a x |] 
   12.52    ==> foldl f a l = foldl g b k"
   12.53  by (induct k arbitrary: a b l) simp_all
   12.54  
   12.55 -lemma foldr_cong [fundef_cong, recdef_cong]:
   12.56 +lemma foldr_cong [fundef_cong]:
   12.57    "[| a = b; l = k; !!a x. x : set l ==> f x a = g x a |] 
   12.58    ==> foldr f l a = foldr g k b"
   12.59  by (induct k arbitrary: a b l) simp_all
   12.60 @@ -4586,7 +4586,7 @@
   12.61  definition
   12.62    "measures fs = inv_image (lex less_than) (%a. map (%f. f a) fs)"
   12.63  
   12.64 -lemma wf_measures[recdef_wf, simp]: "wf (measures fs)"
   12.65 +lemma wf_measures[simp]: "wf (measures fs)"
   12.66  unfolding measures_def
   12.67  by blast
   12.68  
    13.1 --- a/src/HOL/MicroJava/J/TypeRel.thy	Tue Aug 02 10:03:14 2011 +0200
    13.2 +++ b/src/HOL/MicroJava/J/TypeRel.thy	Tue Aug 02 10:36:50 2011 +0200
    13.3 @@ -4,7 +4,7 @@
    13.4  
    13.5  header {* \isaheader{Relations between Java Types} *}
    13.6  
    13.7 -theory TypeRel imports Decl begin
    13.8 +theory TypeRel imports Decl "~~/src/HOL/Library/Old_Recdef" begin
    13.9  
   13.10  -- "direct subclass, cf. 8.1.3"
   13.11  
    14.1 --- a/src/HOL/NanoJava/TypeRel.thy	Tue Aug 02 10:03:14 2011 +0200
    14.2 +++ b/src/HOL/NanoJava/TypeRel.thy	Tue Aug 02 10:36:50 2011 +0200
    14.3 @@ -4,7 +4,7 @@
    14.4  
    14.5  header "Type relations"
    14.6  
    14.7 -theory TypeRel imports Decl begin
    14.8 +theory TypeRel imports Decl "~~/src/HOL/Library/Old_Recdef" begin
    14.9  
   14.10  consts
   14.11    subcls1 :: "(cname \<times> cname) set"  --{* subclass *}
    15.1 --- a/src/HOL/Nitpick.thy	Tue Aug 02 10:03:14 2011 +0200
    15.2 +++ b/src/HOL/Nitpick.thy	Tue Aug 02 10:36:50 2011 +0200
    15.3 @@ -82,15 +82,6 @@
    15.4  definition wf' :: "('a \<times> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
    15.5  "wf' r \<equiv> acyclic r \<and> (finite r \<or> unknown)"
    15.6  
    15.7 -axiomatization wf_wfrec :: "('a \<times> 'a \<Rightarrow> bool) \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
    15.8 -
    15.9 -definition wf_wfrec' :: "('a \<times> 'a \<Rightarrow> bool) \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
   15.10 -[nitpick_simp]: "wf_wfrec' R F x = F (Recdef.cut (wf_wfrec R F) R x) x"
   15.11 -
   15.12 -definition wfrec' ::  "('a \<times> 'a \<Rightarrow> bool) \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
   15.13 -"wfrec' R F x \<equiv> if wf R then wf_wfrec' R F x
   15.14 -                else THE y. wfrec_rel R (%f x. F (Recdef.cut f R x) x) x y"
   15.15 -
   15.16  definition card' :: "('a \<Rightarrow> bool) \<Rightarrow> nat" where
   15.17  "card' A \<equiv> if finite A then length (SOME xs. set xs = A \<and> distinct xs) else 0"
   15.18  
   15.19 @@ -238,14 +229,14 @@
   15.20  setup {* Nitpick_Isar.setup *}
   15.21  
   15.22  hide_const (open) unknown is_unknown bisim bisim_iterator_max Quot safe_The
   15.23 -    FunBox PairBox Word prod refl' wf' wf_wfrec wf_wfrec' wfrec' card' setsum'
   15.24 +    FunBox PairBox Word prod refl' wf' card' setsum'
   15.25      fold_graph' nat_gcd nat_lcm int_gcd int_lcm Frac Abs_Frac Rep_Frac zero_frac
   15.26      one_frac num denom norm_frac frac plus_frac times_frac uminus_frac
   15.27      number_of_frac inverse_frac less_frac less_eq_frac of_frac
   15.28  hide_type (open) iota bisim_iterator fun_box pair_box unsigned_bit signed_bit
   15.29      word
   15.30  hide_fact (open) Ex1_unfold rtrancl_unfold rtranclp_unfold tranclp_unfold
   15.31 -    prod_def refl'_def wf'_def wf_wfrec'_def wfrec'_def card'_def setsum'_def
   15.32 +    prod_def refl'_def wf'_def card'_def setsum'_def
   15.33      fold_graph'_def The_psimp Eps_psimp unit_case_unfold nat_case_unfold
   15.34      list_size_simp nat_gcd_def nat_lcm_def int_gcd_def int_lcm_def Frac_def
   15.35      zero_frac_def one_frac_def num_def denom_def norm_frac_def frac_def
    16.1 --- a/src/HOL/Recdef.thy	Tue Aug 02 10:03:14 2011 +0200
    16.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    16.3 @@ -1,189 +0,0 @@
    16.4 -(*  Title:      HOL/Recdef.thy
    16.5 -    Author:     Konrad Slind and Markus Wenzel, TU Muenchen
    16.6 -*)
    16.7 -
    16.8 -header {* TFL: recursive function definitions *}
    16.9 -
   16.10 -theory Recdef
   16.11 -imports Plain Hilbert_Choice
   16.12 -uses
   16.13 -  ("Tools/TFL/casesplit.ML")
   16.14 -  ("Tools/TFL/utils.ML")
   16.15 -  ("Tools/TFL/usyntax.ML")
   16.16 -  ("Tools/TFL/dcterm.ML")
   16.17 -  ("Tools/TFL/thms.ML")
   16.18 -  ("Tools/TFL/rules.ML")
   16.19 -  ("Tools/TFL/thry.ML")
   16.20 -  ("Tools/TFL/tfl.ML")
   16.21 -  ("Tools/TFL/post.ML")
   16.22 -  ("Tools/recdef.ML")
   16.23 -begin
   16.24 -
   16.25 -inductive
   16.26 -  wfrec_rel :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b => bool"
   16.27 -  for R :: "('a * 'a) set"
   16.28 -  and F :: "('a => 'b) => 'a => 'b"
   16.29 -where
   16.30 -  wfrecI: "ALL z. (z, x) : R --> wfrec_rel R F z (g z) ==>
   16.31 -            wfrec_rel R F x (F g x)"
   16.32 -
   16.33 -definition
   16.34 -  cut        :: "('a => 'b) => ('a * 'a)set => 'a => 'a => 'b" where
   16.35 -  "cut f r x == (%y. if (y,x):r then f y else undefined)"
   16.36 -
   16.37 -definition
   16.38 -  adm_wf :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => bool" where
   16.39 -  "adm_wf R F == ALL f g x.
   16.40 -     (ALL z. (z, x) : R --> f z = g z) --> F f x = F g x"
   16.41 -
   16.42 -definition
   16.43 -  wfrec :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b" where
   16.44 -  "wfrec R F == %x. THE y. wfrec_rel R (%f x. F (cut f R x) x) x y"
   16.45 -
   16.46 -subsection{*Well-Founded Recursion*}
   16.47 -
   16.48 -text{*cut*}
   16.49 -
   16.50 -lemma cuts_eq: "(cut f r x = cut g r x) = (ALL y. (y,x):r --> f(y)=g(y))"
   16.51 -by (simp add: fun_eq_iff cut_def)
   16.52 -
   16.53 -lemma cut_apply: "(x,a):r ==> (cut f r a)(x) = f(x)"
   16.54 -by (simp add: cut_def)
   16.55 -
   16.56 -text{*Inductive characterization of wfrec combinator; for details see:
   16.57 -John Harrison, "Inductive definitions: automation and application"*}
   16.58 -
   16.59 -lemma wfrec_unique: "[| adm_wf R F; wf R |] ==> EX! y. wfrec_rel R F x y"
   16.60 -apply (simp add: adm_wf_def)
   16.61 -apply (erule_tac a=x in wf_induct)
   16.62 -apply (rule ex1I)
   16.63 -apply (rule_tac g = "%x. THE y. wfrec_rel R F x y" in wfrec_rel.wfrecI)
   16.64 -apply (fast dest!: theI')
   16.65 -apply (erule wfrec_rel.cases, simp)
   16.66 -apply (erule allE, erule allE, erule allE, erule mp)
   16.67 -apply (fast intro: the_equality [symmetric])
   16.68 -done
   16.69 -
   16.70 -lemma adm_lemma: "adm_wf R (%f x. F (cut f R x) x)"
   16.71 -apply (simp add: adm_wf_def)
   16.72 -apply (intro strip)
   16.73 -apply (rule cuts_eq [THEN iffD2, THEN subst], assumption)
   16.74 -apply (rule refl)
   16.75 -done
   16.76 -
   16.77 -lemma wfrec: "wf(r) ==> wfrec r H a = H (cut (wfrec r H) r a) a"
   16.78 -apply (simp add: wfrec_def)
   16.79 -apply (rule adm_lemma [THEN wfrec_unique, THEN the1_equality], assumption)
   16.80 -apply (rule wfrec_rel.wfrecI)
   16.81 -apply (intro strip)
   16.82 -apply (erule adm_lemma [THEN wfrec_unique, THEN theI'])
   16.83 -done
   16.84 -
   16.85 -
   16.86 -text{** This form avoids giant explosions in proofs.  NOTE USE OF ==*}
   16.87 -lemma def_wfrec: "[| f==wfrec r H;  wf(r) |] ==> f(a) = H (cut f r a) a"
   16.88 -apply auto
   16.89 -apply (blast intro: wfrec)
   16.90 -done
   16.91 -
   16.92 -
   16.93 -lemma tfl_wf_induct: "ALL R. wf R -->  
   16.94 -       (ALL P. (ALL x. (ALL y. (y,x):R --> P y) --> P x) --> (ALL x. P x))"
   16.95 -apply clarify
   16.96 -apply (rule_tac r = R and P = P and a = x in wf_induct, assumption, blast)
   16.97 -done
   16.98 -
   16.99 -lemma tfl_cut_apply: "ALL f R. (x,a):R --> (cut f R a)(x) = f(x)"
  16.100 -apply clarify
  16.101 -apply (rule cut_apply, assumption)
  16.102 -done
  16.103 -
  16.104 -lemma tfl_wfrec:
  16.105 -     "ALL M R f. (f=wfrec R M) --> wf R --> (ALL x. f x = M (cut f R x) x)"
  16.106 -apply clarify
  16.107 -apply (erule wfrec)
  16.108 -done
  16.109 -
  16.110 -lemma tfl_eq_True: "(x = True) --> x"
  16.111 -  by blast
  16.112 -
  16.113 -lemma tfl_rev_eq_mp: "(x = y) --> y --> x";
  16.114 -  by blast
  16.115 -
  16.116 -lemma tfl_simp_thm: "(x --> y) --> (x = x') --> (x' --> y)"
  16.117 -  by blast
  16.118 -
  16.119 -lemma tfl_P_imp_P_iff_True: "P ==> P = True"
  16.120 -  by blast
  16.121 -
  16.122 -lemma tfl_imp_trans: "(A --> B) ==> (B --> C) ==> (A --> C)"
  16.123 -  by blast
  16.124 -
  16.125 -lemma tfl_disj_assoc: "(a \<or> b) \<or> c == a \<or> (b \<or> c)"
  16.126 -  by simp
  16.127 -
  16.128 -lemma tfl_disjE: "P \<or> Q ==> P --> R ==> Q --> R ==> R"
  16.129 -  by blast
  16.130 -
  16.131 -lemma tfl_exE: "\<exists>x. P x ==> \<forall>x. P x --> Q ==> Q"
  16.132 -  by blast
  16.133 -
  16.134 -use "Tools/TFL/casesplit.ML"
  16.135 -use "Tools/TFL/utils.ML"
  16.136 -use "Tools/TFL/usyntax.ML"
  16.137 -use "Tools/TFL/dcterm.ML"
  16.138 -use "Tools/TFL/thms.ML"
  16.139 -use "Tools/TFL/rules.ML"
  16.140 -use "Tools/TFL/thry.ML"
  16.141 -use "Tools/TFL/tfl.ML"
  16.142 -use "Tools/TFL/post.ML"
  16.143 -use "Tools/recdef.ML"
  16.144 -setup Recdef.setup
  16.145 -
  16.146 -text {*Wellfoundedness of @{text same_fst}*}
  16.147 -
  16.148 -definition
  16.149 - same_fst :: "('a => bool) => ('a => ('b * 'b)set) => (('a*'b)*('a*'b))set"
  16.150 -where
  16.151 -    "same_fst P R == {((x',y'),(x,y)) . x'=x & P x & (y',y) : R x}"
  16.152 -   --{*For @{text rec_def} declarations where the first n parameters
  16.153 -       stay unchanged in the recursive call. *}
  16.154 -
  16.155 -lemma same_fstI [intro!]:
  16.156 -     "[| P x; (y',y) : R x |] ==> ((x,y'),(x,y)) : same_fst P R"
  16.157 -by (simp add: same_fst_def)
  16.158 -
  16.159 -lemma wf_same_fst:
  16.160 -  assumes prem: "(!!x. P x ==> wf(R x))"
  16.161 -  shows "wf(same_fst P R)"
  16.162 -apply (simp cong del: imp_cong add: wf_def same_fst_def)
  16.163 -apply (intro strip)
  16.164 -apply (rename_tac a b)
  16.165 -apply (case_tac "wf (R a)")
  16.166 - apply (erule_tac a = b in wf_induct, blast)
  16.167 -apply (blast intro: prem)
  16.168 -done
  16.169 -
  16.170 -text {*Rule setup*}
  16.171 -
  16.172 -lemmas [recdef_simp] =
  16.173 -  inv_image_def
  16.174 -  measure_def
  16.175 -  lex_prod_def
  16.176 -  same_fst_def
  16.177 -  less_Suc_eq [THEN iffD2]
  16.178 -
  16.179 -lemmas [recdef_cong] =
  16.180 -  if_cong let_cong image_cong INT_cong UN_cong bex_cong ball_cong imp_cong
  16.181 -
  16.182 -lemmas [recdef_wf] =
  16.183 -  wf_trancl
  16.184 -  wf_less_than
  16.185 -  wf_lex_prod
  16.186 -  wf_inv_image
  16.187 -  wf_measure
  16.188 -  wf_pred_nat
  16.189 -  wf_same_fst
  16.190 -  wf_empty
  16.191 -
  16.192 -end
    17.1 --- a/src/HOL/Subst/Unify.thy	Tue Aug 02 10:03:14 2011 +0200
    17.2 +++ b/src/HOL/Subst/Unify.thy	Tue Aug 02 10:36:50 2011 +0200
    17.3 @@ -6,7 +6,7 @@
    17.4  header {* Unification Algorithm *}
    17.5  
    17.6  theory Unify
    17.7 -imports Unifier
    17.8 +imports Unifier "~~/src/HOL/Library/Old_Recdef"
    17.9  begin
   17.10  
   17.11  subsection {* Substitution and Unification in Higher-Order Logic. *}
    18.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Aug 02 10:03:14 2011 +0200
    18.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Aug 02 10:36:50 2011 +0200
    18.3 @@ -1779,7 +1779,7 @@
    18.4                                     "too many nested definitions (" ^
    18.5                                     string_of_int depth ^ ") while expanding " ^
    18.6                                     quote s)
    18.7 -                else if s = @{const_name wfrec'} then
    18.8 +                else if s = "Old_Recdef.wfrec'" (* FIXME unchecked! *) then
    18.9                    (do_term (depth + 1) Ts (s_betapplys Ts (def, ts)), [])
   18.10                  else if not unfold andalso
   18.11                       size_of_term def > def_inline_threshold () then
   18.12 @@ -1873,9 +1873,7 @@
   18.13    [(@{const_name card}, @{const_name card'}),
   18.14     (@{const_name setsum}, @{const_name setsum'}),
   18.15     (@{const_name fold_graph}, @{const_name fold_graph'}),
   18.16 -   (@{const_name wf}, @{const_name wf'}),
   18.17 -   (@{const_name wf_wfrec}, @{const_name wf_wfrec'}),
   18.18 -   (@{const_name wfrec}, @{const_name wfrec'})]
   18.19 +   (@{const_name wf}, @{const_name wf'})]
   18.20  
   18.21  fun ersatz_table ctxt =
   18.22   (basic_ersatz_table @ #ersatz_table (Data.get (Context.Proof ctxt)))
    19.1 --- a/src/HOL/Tools/TFL/rules.ML	Tue Aug 02 10:03:14 2011 +0200
    19.2 +++ b/src/HOL/Tools/TFL/rules.ML	Tue Aug 02 10:36:50 2011 +0200
    19.3 @@ -445,7 +445,7 @@
    19.4  fun is_cong thm =
    19.5    case (Thm.prop_of thm)
    19.6       of (Const("==>",_)$(Const(@{const_name Trueprop},_)$ _) $
    19.7 -         (Const("==",_) $ (Const (@{const_name Recdef.cut},_) $ f $ R $ a $ x) $ _)) => false
    19.8 +         (Const("==",_) $ (Const (@{const_name Old_Recdef.cut},_) $ f $ R $ a $ x) $ _)) => false
    19.9        | _ => true;
   19.10  
   19.11  
   19.12 @@ -645,7 +645,7 @@
   19.13    end;
   19.14  
   19.15  fun restricted t = is_some (USyntax.find_term
   19.16 -                            (fn (Const(@{const_name Recdef.cut},_)) =>true | _ => false)
   19.17 +                            (fn (Const(@{const_name Old_Recdef.cut},_)) =>true | _ => false)
   19.18                              t)
   19.19  
   19.20  fun CONTEXT_REWRITE_RULE (func, G, cut_lemma, congs) th =
    20.1 --- a/src/HOL/Tools/recdef.ML	Tue Aug 02 10:03:14 2011 +0200
    20.2 +++ b/src/HOL/Tools/recdef.ML	Tue Aug 02 10:36:50 2011 +0200
    20.3 @@ -182,7 +182,7 @@
    20.4  
    20.5  (** add_recdef(_i) **)
    20.6  
    20.7 -fun requires_recdef thy = Theory.requires thy "Recdef" "recursive functions";
    20.8 +fun requires_recdef thy = Theory.requires thy "Old_Recdef" "recursive functions";
    20.9  
   20.10  fun gen_add_recdef tfl_fn prep_att prep_hints not_permissive raw_name R eq_srcs hints thy =
   20.11    let
    21.1 --- a/src/HOL/ex/InductiveInvariant.thy	Tue Aug 02 10:03:14 2011 +0200
    21.2 +++ b/src/HOL/ex/InductiveInvariant.thy	Tue Aug 02 10:36:50 2011 +0200
    21.3 @@ -4,7 +4,7 @@
    21.4  
    21.5  header {* Some of the results in Inductive Invariants for Nested Recursion *}
    21.6  
    21.7 -theory InductiveInvariant imports Main begin
    21.8 +theory InductiveInvariant imports "~~/src/HOL/Library/Old_Recdef" begin
    21.9  
   21.10  text {* A formalization of some of the results in \emph{Inductive
   21.11    Invariants for Nested Recursion}, by Sava Krsti\'{c} and John
    22.1 --- a/src/HOL/ex/Recdefs.thy	Tue Aug 02 10:03:14 2011 +0200
    22.2 +++ b/src/HOL/ex/Recdefs.thy	Tue Aug 02 10:36:50 2011 +0200
    22.3 @@ -7,7 +7,7 @@
    22.4  
    22.5  header {* Examples of recdef definitions *}
    22.6  
    22.7 -theory Recdefs imports Main begin
    22.8 +theory Recdefs imports "~~/src/HOL/Library/Old_Recdef" begin
    22.9  
   22.10  consts fact :: "nat => nat"
   22.11  recdef fact  less_than