moved recursion combinator to HOL/Library/Wfrec.thy -- it is so fundamental and well-known that it should survive recdef
--- a/src/HOL/Induct/Sexp.thy Tue Aug 02 10:36:50 2011 +0200
+++ b/src/HOL/Induct/Sexp.thy Tue Aug 02 11:52:57 2011 +0200
@@ -6,7 +6,7 @@
structures by hand.
*)
-theory Sexp imports Main "~~/src/HOL/Library/Old_Recdef" begin
+theory Sexp imports Main "~~/src/HOL/Library/Wfrec" begin
type_synonym 'a item = "'a Datatype.item"
abbreviation "Leaf == Datatype.Leaf"
--- a/src/HOL/IsaMakefile Tue Aug 02 10:36:50 2011 +0200
+++ b/src/HOL/IsaMakefile Tue Aug 02 11:52:57 2011 +0200
@@ -473,7 +473,7 @@
Library/Sum_of_Squares/sos_wrapper.ML \
Library/Sum_of_Squares/sum_of_squares.ML \
Library/Transitive_Closure_Table.thy Library/Univ_Poly.thy \
- Library/While_Combinator.thy Library/Zorn.thy \
+ Library/Wfrec.thy 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 \
--- a/src/HOL/Library/Library.thy Tue Aug 02 10:36:50 2011 +0200
+++ b/src/HOL/Library/Library.thy Tue Aug 02 11:52:57 2011 +0200
@@ -61,6 +61,7 @@
Sum_of_Squares
Transitive_Closure_Table
Univ_Poly
+ Wfrec
While_Combinator
Zorn
begin
--- a/src/HOL/Library/Old_Recdef.thy Tue Aug 02 10:36:50 2011 +0200
+++ b/src/HOL/Library/Old_Recdef.thy Tue Aug 02 11:52:57 2011 +0200
@@ -5,7 +5,7 @@
header {* TFL: recursive function definitions *}
theory Old_Recdef
-imports Main
+imports Wfrec
uses
("~~/src/HOL/Tools/TFL/casesplit.ML")
("~~/src/HOL/Tools/TFL/utils.ML")
@@ -19,95 +19,6 @@
("~~/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 -->
@@ -163,31 +74,7 @@
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*}
+subsection {* Rule setup *}
lemmas [recdef_simp] =
inv_image_def
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Wfrec.thy Tue Aug 02 11:52:57 2011 +0200
@@ -0,0 +1,121 @@
+(* Title: HOL/Library/Wfrec.thy
+ Author: Tobias Nipkow
+ Author: Lawrence C Paulson
+ Author: Konrad Slind
+*)
+
+header {* Well-Founded Recursion Combinator *}
+
+theory Wfrec
+imports Main
+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"
+
+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 {* 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
+
+end
--- a/src/HOL/MicroJava/J/TypeRel.thy Tue Aug 02 10:36:50 2011 +0200
+++ b/src/HOL/MicroJava/J/TypeRel.thy Tue Aug 02 11:52:57 2011 +0200
@@ -4,7 +4,7 @@
header {* \isaheader{Relations between Java Types} *}
-theory TypeRel imports Decl "~~/src/HOL/Library/Old_Recdef" begin
+theory TypeRel imports Decl "~~/src/HOL/Library/Wfrec" begin
-- "direct subclass, cf. 8.1.3"
--- a/src/HOL/Tools/TFL/rules.ML Tue Aug 02 10:36:50 2011 +0200
+++ b/src/HOL/Tools/TFL/rules.ML Tue Aug 02 11:52:57 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 Old_Recdef.cut},_) $ f $ R $ a $ x) $ _)) => false
+ (Const("==",_) $ (Const (@{const_name Wfrec.cut},_) $ f $ R $ a $ x) $ _)) => false
| _ => true;
@@ -645,7 +645,7 @@
end;
fun restricted t = is_some (USyntax.find_term
- (fn (Const(@{const_name Old_Recdef.cut},_)) =>true | _ => false)
+ (fn (Const(@{const_name Wfrec.cut},_)) =>true | _ => false)
t)
fun CONTEXT_REWRITE_RULE (func, G, cut_lemma, congs) th =