1.1 --- a/src/HOL/Induct/Sexp.thy	Tue Aug 02 10:36:50 2011 +0200
     1.2 +++ b/src/HOL/Induct/Sexp.thy	Tue Aug 02 11:52:57 2011 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4  structures by hand.
     1.5  *)
     1.6  
     1.7 -theory Sexp imports Main "~~/src/HOL/Library/Old_Recdef" begin
     1.8 +theory Sexp imports Main "~~/src/HOL/Library/Wfrec" begin
     1.9  
    1.10  type_synonym 'a item = "'a Datatype.item"
    1.11  abbreviation "Leaf == Datatype.Leaf"

     2.1 --- a/src/HOL/IsaMakefile	Tue Aug 02 10:36:50 2011 +0200
     2.2 +++ b/src/HOL/IsaMakefile	Tue Aug 02 11:52:57 2011 +0200
     2.3 @@ -473,7 +473,7 @@
     2.4    Library/Sum_of_Squares/sos_wrapper.ML					\
     2.5    Library/Sum_of_Squares/sum_of_squares.ML				\
     2.6    Library/Transitive_Closure_Table.thy Library/Univ_Poly.thy		\
     2.7 -  Library/While_Combinator.thy Library/Zorn.thy				\
     2.8 +  Library/Wfrec.thy Library/While_Combinator.thy Library/Zorn.thy	\
     2.9    $(SRC)/Tools/adhoc_overloading.ML Library/positivstellensatz.ML	\
    2.10    Library/reflection.ML Library/reify_data.ML				\
    2.11    Library/document/root.bib Library/document/root.tex			\

     3.1 --- a/src/HOL/Library/Library.thy	Tue Aug 02 10:36:50 2011 +0200
     3.2 +++ b/src/HOL/Library/Library.thy	Tue Aug 02 11:52:57 2011 +0200
     3.3 @@ -61,6 +61,7 @@
     3.4    Sum_of_Squares
     3.5    Transitive_Closure_Table
     3.6    Univ_Poly
     3.7 +  Wfrec
     3.8    While_Combinator
     3.9    Zorn
    3.10  begin

     4.1 --- a/src/HOL/Library/Old_Recdef.thy	Tue Aug 02 10:36:50 2011 +0200
     4.2 +++ b/src/HOL/Library/Old_Recdef.thy	Tue Aug 02 11:52:57 2011 +0200
     4.3 @@ -5,7 +5,7 @@
     4.4  header {* TFL: recursive function definitions *}
     4.5  
     4.6  theory Old_Recdef
     4.7 -imports Main
     4.8 +imports Wfrec
     4.9  uses
    4.10    ("~~/src/HOL/Tools/TFL/casesplit.ML")
    4.11    ("~~/src/HOL/Tools/TFL/utils.ML")
    4.12 @@ -19,95 +19,6 @@
    4.13    ("~~/src/HOL/Tools/recdef.ML")
    4.14  begin
    4.15  
    4.16 -inductive
    4.17 -  wfrec_rel :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b => bool"
    4.18 -  for R :: "('a * 'a) set"
    4.19 -  and F :: "('a => 'b) => 'a => 'b"
    4.20 -where
    4.21 -  wfrecI: "ALL z. (z, x) : R --> wfrec_rel R F z (g z) ==>
    4.22 -            wfrec_rel R F x (F g x)"
    4.23 -
    4.24 -definition
    4.25 -  cut        :: "('a => 'b) => ('a * 'a)set => 'a => 'a => 'b" where
    4.26 -  "cut f r x == (%y. if (y,x):r then f y else undefined)"
    4.27 -
    4.28 -definition
    4.29 -  adm_wf :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => bool" where
    4.30 -  "adm_wf R F == ALL f g x.
    4.31 -     (ALL z. (z, x) : R --> f z = g z) --> F f x = F g x"
    4.32 -
    4.33 -definition
    4.34 -  wfrec :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b" where
    4.35 -  "wfrec R F == %x. THE y. wfrec_rel R (%f x. F (cut f R x) x) x y"
    4.36 -
    4.37 -subsection{*Well-Founded Recursion*}
    4.38 -
    4.39 -text{*cut*}
    4.40 -
    4.41 -lemma cuts_eq: "(cut f r x = cut g r x) = (ALL y. (y,x):r --> f(y)=g(y))"
    4.42 -by (simp add: fun_eq_iff cut_def)
    4.43 -
    4.44 -lemma cut_apply: "(x,a):r ==> (cut f r a)(x) = f(x)"
    4.45 -by (simp add: cut_def)
    4.46 -
    4.47 -text{*Inductive characterization of wfrec combinator; for details see:
    4.48 -John Harrison, "Inductive definitions: automation and application"*}
    4.49 -
    4.50 -lemma wfrec_unique: "[| adm_wf R F; wf R |] ==> EX! y. wfrec_rel R F x y"
    4.51 -apply (simp add: adm_wf_def)
    4.52 -apply (erule_tac a=x in wf_induct)
    4.53 -apply (rule ex1I)
    4.54 -apply (rule_tac g = "%x. THE y. wfrec_rel R F x y" in wfrec_rel.wfrecI)
    4.55 -apply (fast dest!: theI')
    4.56 -apply (erule wfrec_rel.cases, simp)
    4.57 -apply (erule allE, erule allE, erule allE, erule mp)
    4.58 -apply (fast intro: the_equality [symmetric])
    4.59 -done
    4.60 -
    4.61 -lemma adm_lemma: "adm_wf R (%f x. F (cut f R x) x)"
    4.62 -apply (simp add: adm_wf_def)
    4.63 -apply (intro strip)
    4.64 -apply (rule cuts_eq [THEN iffD2, THEN subst], assumption)
    4.65 -apply (rule refl)
    4.66 -done
    4.67 -
    4.68 -lemma wfrec: "wf(r) ==> wfrec r H a = H (cut (wfrec r H) r a) a"
    4.69 -apply (simp add: wfrec_def)
    4.70 -apply (rule adm_lemma [THEN wfrec_unique, THEN the1_equality], assumption)
    4.71 -apply (rule wfrec_rel.wfrecI)
    4.72 -apply (intro strip)
    4.73 -apply (erule adm_lemma [THEN wfrec_unique, THEN theI'])
    4.74 -done
    4.75 -
    4.76 -
    4.77 -text{** This form avoids giant explosions in proofs.  NOTE USE OF ==*}
    4.78 -lemma def_wfrec: "[| f==wfrec r H;  wf(r) |] ==> f(a) = H (cut f r a) a"
    4.79 -apply auto
    4.80 -apply (blast intro: wfrec)
    4.81 -done
    4.82 -
    4.83 -
    4.84 -subsection {* Nitpick setup *}
    4.85 -
    4.86 -axiomatization wf_wfrec :: "('a \<times> 'a \<Rightarrow> bool) \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
    4.87 -
    4.88 -definition wf_wfrec' :: "('a \<times> 'a \<Rightarrow> bool) \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
    4.89 -[nitpick_simp]: "wf_wfrec' R F x = F (cut (wf_wfrec R F) R x) x"
    4.90 -
    4.91 -definition wfrec' ::  "('a \<times> 'a \<Rightarrow> bool) \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
    4.92 -"wfrec' R F x \<equiv> if wf R then wf_wfrec' R F x
    4.93 -                else THE y. wfrec_rel R (%f x. F (cut f R x) x) x y"
    4.94 -
    4.95 -setup {*
    4.96 -  Nitpick_HOL.register_ersatz_global
    4.97 -    [(@{const_name wf_wfrec}, @{const_name wf_wfrec'}),
    4.98 -     (@{const_name wfrec}, @{const_name wfrec'})]
    4.99 -*}
   4.100 -
   4.101 -hide_const (open) wf_wfrec wf_wfrec' wfrec'
   4.102 -hide_fact (open) wf_wfrec'_def wfrec'_def
   4.103 -
   4.104 -
   4.105  subsection {* Lemmas for TFL *}
   4.106  
   4.107  lemma tfl_wf_induct: "ALL R. wf R -->  
   4.108 @@ -163,31 +74,7 @@
   4.109  use "~~/src/HOL/Tools/recdef.ML"
   4.110  setup Recdef.setup
   4.111  
   4.112 -text {*Wellfoundedness of @{text same_fst}*}
   4.113 -
   4.114 -definition
   4.115 - same_fst :: "('a => bool) => ('a => ('b * 'b)set) => (('a*'b)*('a*'b))set"
   4.116 -where
   4.117 -    "same_fst P R == {((x',y'),(x,y)) . x'=x & P x & (y',y) : R x}"
   4.118 -   --{*For @{text rec_def} declarations where the first n parameters
   4.119 -       stay unchanged in the recursive call. *}
   4.120 -
   4.121 -lemma same_fstI [intro!]:
   4.122 -     "[| P x; (y',y) : R x |] ==> ((x,y'),(x,y)) : same_fst P R"
   4.123 -by (simp add: same_fst_def)
   4.124 -
   4.125 -lemma wf_same_fst:
   4.126 -  assumes prem: "(!!x. P x ==> wf(R x))"
   4.127 -  shows "wf(same_fst P R)"
   4.128 -apply (simp cong del: imp_cong add: wf_def same_fst_def)
   4.129 -apply (intro strip)
   4.130 -apply (rename_tac a b)
   4.131 -apply (case_tac "wf (R a)")
   4.132 - apply (erule_tac a = b in wf_induct, blast)
   4.133 -apply (blast intro: prem)
   4.134 -done
   4.135 -
   4.136 -text {*Rule setup*}
   4.137 +subsection {* Rule setup *}
   4.138  
   4.139  lemmas [recdef_simp] =
   4.140    inv_image_def

     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Library/Wfrec.thy	Tue Aug 02 11:52:57 2011 +0200
     5.3 @@ -0,0 +1,121 @@
     5.4 +(*  Title:      HOL/Library/Wfrec.thy
     5.5 +    Author:     Tobias Nipkow
     5.6 +    Author:     Lawrence C Paulson
     5.7 +    Author:     Konrad Slind
     5.8 +*)
     5.9 +
    5.10 +header {* Well-Founded Recursion Combinator *}
    5.11 +
    5.12 +theory Wfrec
    5.13 +imports Main
    5.14 +begin
    5.15 +
    5.16 +inductive
    5.17 +  wfrec_rel :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b => bool"
    5.18 +  for R :: "('a * 'a) set"
    5.19 +  and F :: "('a => 'b) => 'a => 'b"
    5.20 +where
    5.21 +  wfrecI: "ALL z. (z, x) : R --> wfrec_rel R F z (g z) ==>
    5.22 +            wfrec_rel R F x (F g x)"
    5.23 +
    5.24 +definition
    5.25 +  cut        :: "('a => 'b) => ('a * 'a)set => 'a => 'a => 'b" where
    5.26 +  "cut f r x == (%y. if (y,x):r then f y else undefined)"
    5.27 +
    5.28 +definition
    5.29 +  adm_wf :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => bool" where
    5.30 +  "adm_wf R F == ALL f g x.
    5.31 +     (ALL z. (z, x) : R --> f z = g z) --> F f x = F g x"
    5.32 +
    5.33 +definition
    5.34 +  wfrec :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b" where
    5.35 +  "wfrec R F == %x. THE y. wfrec_rel R (%f x. F (cut f R x) x) x y"
    5.36 +
    5.37 +lemma cuts_eq: "(cut f r x = cut g r x) = (ALL y. (y,x):r --> f(y)=g(y))"
    5.38 +by (simp add: fun_eq_iff cut_def)
    5.39 +
    5.40 +lemma cut_apply: "(x,a):r ==> (cut f r a)(x) = f(x)"
    5.41 +by (simp add: cut_def)
    5.42 +
    5.43 +text{*Inductive characterization of wfrec combinator; for details see:
    5.44 +John Harrison, "Inductive definitions: automation and application"*}
    5.45 +
    5.46 +lemma wfrec_unique: "[| adm_wf R F; wf R |] ==> EX! y. wfrec_rel R F x y"
    5.47 +apply (simp add: adm_wf_def)
    5.48 +apply (erule_tac a=x in wf_induct)
    5.49 +apply (rule ex1I)
    5.50 +apply (rule_tac g = "%x. THE y. wfrec_rel R F x y" in wfrec_rel.wfrecI)
    5.51 +apply (fast dest!: theI')
    5.52 +apply (erule wfrec_rel.cases, simp)
    5.53 +apply (erule allE, erule allE, erule allE, erule mp)
    5.54 +apply (fast intro: the_equality [symmetric])
    5.55 +done
    5.56 +
    5.57 +lemma adm_lemma: "adm_wf R (%f x. F (cut f R x) x)"
    5.58 +apply (simp add: adm_wf_def)
    5.59 +apply (intro strip)
    5.60 +apply (rule cuts_eq [THEN iffD2, THEN subst], assumption)
    5.61 +apply (rule refl)
    5.62 +done
    5.63 +
    5.64 +lemma wfrec: "wf(r) ==> wfrec r H a = H (cut (wfrec r H) r a) a"
    5.65 +apply (simp add: wfrec_def)
    5.66 +apply (rule adm_lemma [THEN wfrec_unique, THEN the1_equality], assumption)
    5.67 +apply (rule wfrec_rel.wfrecI)
    5.68 +apply (intro strip)
    5.69 +apply (erule adm_lemma [THEN wfrec_unique, THEN theI'])
    5.70 +done
    5.71 +
    5.72 +
    5.73 +text{** This form avoids giant explosions in proofs.  NOTE USE OF ==*}
    5.74 +lemma def_wfrec: "[| f==wfrec r H;  wf(r) |] ==> f(a) = H (cut f r a) a"
    5.75 +apply auto
    5.76 +apply (blast intro: wfrec)
    5.77 +done
    5.78 +
    5.79 +
    5.80 +subsection {* Nitpick setup *}
    5.81 +
    5.82 +axiomatization wf_wfrec :: "('a \<times> 'a \<Rightarrow> bool) \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
    5.83 +
    5.84 +definition wf_wfrec' :: "('a \<times> 'a \<Rightarrow> bool) \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
    5.85 +[nitpick_simp]: "wf_wfrec' R F x = F (cut (wf_wfrec R F) R x) x"
    5.86 +
    5.87 +definition wfrec' ::  "('a \<times> 'a \<Rightarrow> bool) \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
    5.88 +"wfrec' R F x \<equiv> if wf R then wf_wfrec' R F x
    5.89 +                else THE y. wfrec_rel R (%f x. F (cut f R x) x) x y"
    5.90 +
    5.91 +setup {*
    5.92 +  Nitpick_HOL.register_ersatz_global
    5.93 +    [(@{const_name wf_wfrec}, @{const_name wf_wfrec'}),
    5.94 +     (@{const_name wfrec}, @{const_name wfrec'})]
    5.95 +*}
    5.96 +
    5.97 +hide_const (open) wf_wfrec wf_wfrec' wfrec'
    5.98 +hide_fact (open) wf_wfrec'_def wfrec'_def
    5.99 +
   5.100 +subsection {* Wellfoundedness of @{text same_fst} *}
   5.101 +
   5.102 +definition
   5.103 + same_fst :: "('a => bool) => ('a => ('b * 'b)set) => (('a*'b)*('a*'b))set"
   5.104 +where
   5.105 +    "same_fst P R == {((x',y'),(x,y)) . x'=x & P x & (y',y) : R x}"
   5.106 +   --{*For @{text rec_def} declarations where the first n parameters
   5.107 +       stay unchanged in the recursive call. *}
   5.108 +
   5.109 +lemma same_fstI [intro!]:
   5.110 +     "[| P x; (y',y) : R x |] ==> ((x,y'),(x,y)) : same_fst P R"
   5.111 +by (simp add: same_fst_def)
   5.112 +
   5.113 +lemma wf_same_fst:
   5.114 +  assumes prem: "(!!x. P x ==> wf(R x))"
   5.115 +  shows "wf(same_fst P R)"
   5.116 +apply (simp cong del: imp_cong add: wf_def same_fst_def)
   5.117 +apply (intro strip)
   5.118 +apply (rename_tac a b)
   5.119 +apply (case_tac "wf (R a)")
   5.120 + apply (erule_tac a = b in wf_induct, blast)
   5.121 +apply (blast intro: prem)
   5.122 +done
   5.123 +
   5.124 +end

     6.1 --- a/src/HOL/MicroJava/J/TypeRel.thy	Tue Aug 02 10:36:50 2011 +0200
     6.2 +++ b/src/HOL/MicroJava/J/TypeRel.thy	Tue Aug 02 11:52:57 2011 +0200
     6.3 @@ -4,7 +4,7 @@
     6.4  
     6.5  header {* \isaheader{Relations between Java Types} *}
     6.6  
     6.7 -theory TypeRel imports Decl "~~/src/HOL/Library/Old_Recdef" begin
     6.8 +theory TypeRel imports Decl "~~/src/HOL/Library/Wfrec" begin
     6.9  
    6.10  -- "direct subclass, cf. 8.1.3"
    6.11  

     7.1 --- a/src/HOL/Tools/TFL/rules.ML	Tue Aug 02 10:36:50 2011 +0200
     7.2 +++ b/src/HOL/Tools/TFL/rules.ML	Tue Aug 02 11:52:57 2011 +0200
     7.3 @@ -445,7 +445,7 @@
     7.4  fun is_cong thm =
     7.5    case (Thm.prop_of thm)
     7.6       of (Const("==>",_)$(Const(@{const_name Trueprop},_)$ _) $
     7.7 -         (Const("==",_) $ (Const (@{const_name Old_Recdef.cut},_) $ f $ R $ a $ x) $ _)) => false
     7.8 +         (Const("==",_) $ (Const (@{const_name Wfrec.cut},_) $ f $ R $ a $ x) $ _)) => false
     7.9        | _ => true;
    7.10  
    7.11  
    7.12 @@ -645,7 +645,7 @@
    7.13    end;
    7.14  
    7.15  fun restricted t = is_some (USyntax.find_term
    7.16 -                            (fn (Const(@{const_name Old_Recdef.cut},_)) =>true | _ => false)
    7.17 +                            (fn (Const(@{const_name Wfrec.cut},_)) =>true | _ => false)
    7.18                              t)
    7.19  
    7.20  fun CONTEXT_REWRITE_RULE (func, G, cut_lemma, congs) th =