# HG changeset patch # User krauss # Date 1312278777 -7200 # Node ID 88bd7d74a2c172390512f25b1353e73e7996f6fb # Parent 5cfc1c36ae97dd30c7841e07e7f06b0a5092f7eb moved recursion combinator to HOL/Library/Wfrec.thy -- it is so fundamental and well-known that it should survive recdef diff -r 5cfc1c36ae97 -r 88bd7d74a2c1 src/HOL/Induct/Sexp.thy --- 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" diff -r 5cfc1c36ae97 -r 88bd7d74a2c1 src/HOL/IsaMakefile --- 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 \ diff -r 5cfc1c36ae97 -r 88bd7d74a2c1 src/HOL/Library/Library.thy --- 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 diff -r 5cfc1c36ae97 -r 88bd7d74a2c1 src/HOL/Library/Old_Recdef.thy --- 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 \ 'a \ bool) \ (('a \ 'b) \ 'a \ 'b) \ 'a \ 'b" - -definition wf_wfrec' :: "('a \ 'a \ bool) \ (('a \ 'b) \ 'a \ 'b) \ 'a \ 'b" where -[nitpick_simp]: "wf_wfrec' R F x = F (cut (wf_wfrec R F) R x) x" - -definition wfrec' :: "('a \ 'a \ bool) \ (('a \ 'b) \ 'a \ 'b) \ 'a \ 'b" where -"wfrec' R F x \ 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 diff -r 5cfc1c36ae97 -r 88bd7d74a2c1 src/HOL/Library/Wfrec.thy --- /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 \ 'a \ bool) \ (('a \ 'b) \ 'a \ 'b) \ 'a \ 'b" + +definition wf_wfrec' :: "('a \ 'a \ bool) \ (('a \ 'b) \ 'a \ 'b) \ 'a \ 'b" where +[nitpick_simp]: "wf_wfrec' R F x = F (cut (wf_wfrec R F) R x) x" + +definition wfrec' :: "('a \ 'a \ bool) \ (('a \ 'b) \ 'a \ 'b) \ 'a \ 'b" where +"wfrec' R F x \ 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 diff -r 5cfc1c36ae97 -r 88bd7d74a2c1 src/HOL/MicroJava/J/TypeRel.thy --- 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" diff -r 5cfc1c36ae97 -r 88bd7d74a2c1 src/HOL/Tools/TFL/rules.ML --- 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 =