# HG changeset patch # User wenzelm # Date 1347385512 -7200 # Node ID 66058a677ddd38c9e758c2c708962a2c27b6df4c # Parent ebe2a5cec4bf031a205c5ddbef9131ee1a49b08b# Parent 64bed36cd8da8d31761f8d9dea7da65314d50832 merged diff -r 64bed36cd8da -r 66058a677ddd src/HOL/Codatatype/BNF_Def.thy --- a/src/HOL/Codatatype/BNF_Def.thy Tue Sep 11 19:43:06 2012 +0200 +++ b/src/HOL/Codatatype/BNF_Def.thy Tue Sep 11 19:45:12 2012 +0200 @@ -8,14 +8,12 @@ header {* Definition of Bounded Natural Functors *} theory BNF_Def -imports BNF_Library +imports BNF_Util keywords - "print_bnfs" :: diag -and + "print_bnfs" :: diag and "bnf_def" :: thy_goal uses - "Tools/bnf_util.ML" - "Tools/bnf_tactics.ML" + "Tools/bnf_def_tactics.ML" "Tools/bnf_def.ML" begin diff -r 64bed36cd8da -r 66058a677ddd src/HOL/Codatatype/BNF_Library.thy --- a/src/HOL/Codatatype/BNF_Library.thy Tue Sep 11 19:43:06 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,849 +0,0 @@ -(* Title: HOL/Codatatype/BNF_Library.thy - Author: Dmitriy Traytel, TU Muenchen - Copyright 2012 - -Library for bounded natural functors. -*) - -header {* Library for Bounded Natural Functors *} - -theory BNF_Library -imports - "../Ordinals_and_Cardinals/Cardinal_Arithmetic" - "~~/src/HOL/Library/Prefix_Order" - Equiv_Relations_More -begin - -lemma iffI_np: "\x \ \ y; \ x \ y\ \ \ x \ y" -by (erule iffI) (erule contrapos_pn) - -lemma all_unit_eq: "(\x. PROP P x) \ PROP P ()" by simp - -lemma all_prod_eq: "(\x. PROP P x) \ (\a b. PROP P (a, b))" by clarsimp - -lemma False_imp_eq: "(False \ P) \ Trueprop True" -by presburger - -lemma case_unit: "(case u of () => f) = f" -by (cases u) (hypsubst, rule unit.cases) - -lemma All_point_1: "(\z. z = b \ phi z) \ Trueprop (phi b)" -by presburger - -lemma subset_Collect_iff: "B \ A \ (B \ {x \ A. P x}) = (\x \ B. P x)" -by blast - -lemma subset_CollectI: "B \ A \ (\x. x \ B \ Q x \ P x) \ ({x \ B. Q x} \ {x \ A. P x})" -by blast - -lemma mem_Collect_eq_split: "{(x, y). (x, y) \ X} = X" -by simp - -lemma image_comp: "image (f o g) = image f o image g" -by (rule ext) (auto simp only: o_apply image_def) - -lemma empty_natural: "(\_. {}) o f = image g o (\_. {})" -by (rule ext) simp - -lemma Union_natural: "Union o image (image f) = image f o Union" -by (rule ext) (auto simp only: o_apply) - -lemma in_Union_o_assoc: "x \ (Union o gset o gmap) A \ x \ (Union o (gset o gmap)) A" -by (unfold o_assoc) - -lemma comp_single_set_bd: - assumes fbd_Card_order: "Card_order fbd" and - fset_bd: "\x. |fset x| \o fbd" and - gset_bd: "\x. |gset x| \o gbd" - shows "|\fset ` gset x| \o gbd *c fbd" -apply (subst sym[OF SUP_def]) -apply (rule ordLeq_transitive) -apply (rule card_of_UNION_Sigma) -apply (subst SIGMA_CSUM) -apply (rule ordLeq_transitive) -apply (rule card_of_Csum_Times') -apply (rule fbd_Card_order) -apply (rule ballI) -apply (rule fset_bd) -apply (rule ordLeq_transitive) -apply (rule cprod_mono1) -apply (rule gset_bd) -apply (rule ordIso_imp_ordLeq) -apply (rule ordIso_refl) -apply (rule Card_order_cprod) -done - -lemma Union_image_insert: "\f ` insert a B = f a \ \f ` B" -by simp - -lemma Union_image_empty: "A \ \f ` {} = A" -by simp - -definition collect where - "collect F x = (\f \ F. f x)" - -lemma collect_o: "collect F o g = collect ((\f. f o g) ` F)" -by (rule ext) (auto simp only: o_apply collect_def) - -lemma image_o_collect: "collect ((\f. image g o f) ` F) = image g o collect F" -by (rule ext) (auto simp add: collect_def) - -lemma conj_subset_def: "A \ {x. P x \ Q x} = (A \ {x. P x} \ A \ {x. Q x})" -by blast - -lemma subset_emptyI: "(\x. x \ A \ False) \ A \ {}" -by blast - -lemma rev_bspec: "a \ A \ \z \ A. P z \ P a" -by simp - -lemma Un_cong: "\A = B; C = D\ \ A \ C = B \ D" -by simp - -lemma UN_image_subset: "\f ` g x \ X = (g x \ {x. f x \ X})" -by blast - -lemma image_Collect_subsetI: - "(\x. P x \ f x \ B) \ f ` {x. P x} \ B" -by blast - -lemma comp_set_bd_Union_o_collect: "|\\(\f. f x) ` X| \o hbd \ |(Union \ collect X) x| \o hbd" -by (unfold o_apply collect_def SUP_def) - -lemma sum_case_comp_Inl: -"sum_case f g \ Inl = f" -unfolding comp_def by simp - -lemma sum_case_expand_Inr: "f o Inl = g \ f x = sum_case g (f o Inr) x" -by (auto split: sum.splits) - -lemma converse_mono: -"R1 ^-1 \ R2 ^-1 \ R1 \ R2" -unfolding converse_def by auto - -lemma converse_shift: -"R1 \ R2 ^-1 \ R1 ^-1 \ R2" -unfolding converse_def by auto - -lemma converse_Times: "(A \ B) ^-1 = B \ A" -by auto - -lemma equiv_triv1: -assumes "equiv A R" and "(a, b) \ R" and "(a, c) \ R" -shows "(b, c) \ R" -using assms unfolding equiv_def sym_def trans_def by blast - -lemma equiv_triv2: -assumes "equiv A R" and "(a, b) \ R" and "(b, c) \ R" -shows "(a, c) \ R" -using assms unfolding equiv_def trans_def by blast - -lemma equiv_proj: - assumes e: "equiv A R" and "z \ R" - shows "(proj R o fst) z = (proj R o snd) z" -proof - - from assms(2) have z: "(fst z, snd z) \ R" by auto - have P: "\x. (fst z, x) \ R \ (snd z, x) \ R" by (erule equiv_triv1[OF e z]) - have "\x. (snd z, x) \ R \ (fst z, x) \ R" by (erule equiv_triv2[OF e z]) - with P show ?thesis unfolding proj_def[abs_def] by auto -qed - - -section{* Weak pullbacks: *} - -definition csquare where -"csquare A f1 f2 p1 p2 \ (\ a \ A. f1 (p1 a) = f2 (p2 a))" - -definition wpull where -"wpull A B1 B2 f1 f2 p1 p2 \ - (\ b1 b2. b1 \ B1 \ b2 \ B2 \ f1 b1 = f2 b2 \ (\ a \ A. p1 a = b1 \ p2 a = b2))" - -lemma wpull_cong: -"\A' = A; B1' = B1; B2' = B2; wpull A B1 B2 f1 f2 p1 p2\ \ wpull A' B1' B2' f1 f2 p1 p2" -by simp - -lemma wpull_id: "wpull UNIV B1 B2 id id id id" -unfolding wpull_def by simp - - -(* Weak pseudo-pullbacks *) - -definition wppull where -"wppull A B1 B2 f1 f2 e1 e2 p1 p2 \ - (\ b1 b2. b1 \ B1 \ b2 \ B2 \ f1 b1 = f2 b2 \ - (\ a \ A. e1 (p1 a) = e1 b1 \ e2 (p2 a) = e2 b2))" - - -(* The pullback of sets *) -definition thePull where -"thePull B1 B2 f1 f2 = {(b1,b2). b1 \ B1 \ b2 \ B2 \ f1 b1 = f2 b2}" - -lemma wpull_thePull: -"wpull (thePull B1 B2 f1 f2) B1 B2 f1 f2 fst snd" -unfolding wpull_def thePull_def by auto - -lemma wppull_thePull: -assumes "wppull A B1 B2 f1 f2 e1 e2 p1 p2" -shows -"\ j. \ a' \ thePull B1 B2 f1 f2. - j a' \ A \ - e1 (p1 (j a')) = e1 (fst a') \ e2 (p2 (j a')) = e2 (snd a')" -(is "\ j. \ a' \ ?A'. ?phi a' (j a')") -proof(rule bchoice[of ?A' ?phi], default) - fix a' assume a': "a' \ ?A'" - hence "fst a' \ B1" unfolding thePull_def by auto - moreover - from a' have "snd a' \ B2" unfolding thePull_def by auto - moreover have "f1 (fst a') = f2 (snd a')" - using a' unfolding csquare_def thePull_def by auto - ultimately show "\ ja'. ?phi a' ja'" - using assms unfolding wppull_def by auto -qed - -lemma wpull_wppull: -assumes wp: "wpull A' B1 B2 f1 f2 p1' p2'" and -1: "\ a' \ A'. j a' \ A \ e1 (p1 (j a')) = e1 (p1' a') \ e2 (p2 (j a')) = e2 (p2' a')" -shows "wppull A B1 B2 f1 f2 e1 e2 p1 p2" -unfolding wppull_def proof safe - fix b1 b2 - assume b1: "b1 \ B1" and b2: "b2 \ B2" and f: "f1 b1 = f2 b2" - then obtain a' where a': "a' \ A'" and b1: "b1 = p1' a'" and b2: "b2 = p2' a'" - using wp unfolding wpull_def by blast - show "\a\A. e1 (p1 a) = e1 b1 \ e2 (p2 a) = e2 b2" - apply(rule bexI[of _ "j a'"]) unfolding b1 b2 using a' 1 by auto -qed - -lemma wppull_id: "\wpull UNIV UNIV UNIV f1 f2 p1 p2; e1 = id; e2 = id\ \ - wppull UNIV UNIV UNIV f1 f2 e1 e2 p1 p2" -by (erule wpull_wppull) auto - - -(* Operators: *) -definition diag where "diag A \ {(a,a) | a. a \ A}" -definition "Gr A f = {(a,f a) | a. a \ A}" -definition image2 where "image2 A f g = {(f a, g a) | a. a \ A}" - -lemma diagI: "x \ A \ (x, x) \ diag A" -unfolding diag_def by simp - -lemma diagE: "(a, b) \ diag A \ a = b" -unfolding diag_def by simp - -lemma diagE': "x \ diag A \ fst x = snd x" -unfolding diag_def by auto - -lemma diag_fst: "x \ diag A \ fst x \ A" -unfolding diag_def by auto - -lemma diag_UNIV: "diag UNIV = Id" -unfolding diag_def by auto - -lemma diag_converse: "diag A = (diag A) ^-1" -unfolding diag_def by auto - -lemma diag_Comp: "diag A = diag A O diag A" -unfolding diag_def by auto - -lemma diag_Gr: "diag A = Gr A id" -unfolding diag_def Gr_def by simp - -lemma diag_UNIV_I: "x = y \ (x, y) \ diag UNIV" -unfolding diag_def by auto - -lemma image2_eqI: "\b = f x; c = g x; x \ A\ \ (b, c) \ image2 A f g" -unfolding image2_def by auto - -lemma Id_def': "Id = {(a,b). a = b}" -by auto - -lemma Id_alt: "Id = Gr UNIV id" -unfolding Gr_def by auto - -lemma Id_subset: "Id \ {(a, b). P a b \ a = b}" -by auto - -lemma IdD: "(a, b) \ Id \ a = b" -by auto - -lemma image2_Gr: "image2 A f g = (Gr A f)^-1 O (Gr A g)" -unfolding image2_def Gr_def by auto - -lemma GrI: "\x \ A; f x = fx\ \ (x, fx) \ Gr A f" -unfolding Gr_def by simp - -lemma GrE: "(x, fx) \ Gr A f \ (x \ A \ f x = fx \ P) \ P" -unfolding Gr_def by simp - -lemma GrD1: "(x, fx) \ Gr A f \ x \ A" -unfolding Gr_def by simp - -lemma GrD2: "(x, fx) \ Gr A f \ f x = fx" -unfolding Gr_def by simp - -lemma Gr_UNIV_id: "f = id \ (Gr UNIV f)^-1 O Gr UNIV f = Gr UNIV f" -unfolding Gr_def by auto - -lemma Gr_fst_snd: "(Gr R fst)^-1 O Gr R snd = R" -unfolding Gr_def by auto - -lemma Gr_mono: "A \ B \ Gr A f \ Gr B f" -unfolding Gr_def by auto - -lemma subst_rel_def: "A = B \ (Gr A f)^-1 O Gr A g = (Gr B f)^-1 O Gr B g" -by simp - -lemma abs_pred_def: "\\x y. (x, y) \ rel = pred x y\ \ rel = Collect (split pred)" -by auto - -lemma Collect_split_cong: "Collect (split pred) = Collect (split pred') \ pred = pred'" -by blast - -lemma pred_def_abs: "rel = Collect (split pred) \ pred = (\x y. (x, y) \ rel)" -by auto - -lemma wpull_Gr: -"wpull (Gr A f) A (f ` A) f id fst snd" -unfolding wpull_def Gr_def by auto - -lemma Gr_incl: "Gr A f \ A <*> B \ f ` A \ B" -unfolding Gr_def by auto - -lemma equiv_Image: "equiv A R \ (\a b. (a, b) \ R \ a \ A \ b \ A \ R `` {a} = R `` {b})" -unfolding equiv_def refl_on_def Image_def by (auto intro: transD symD) - -definition relImage where -"relImage R f \ {(f a1, f a2) | a1 a2. (a1,a2) \ R}" - -definition relInvImage where -"relInvImage A R f \ {(a1, a2) | a1 a2. a1 \ A \ a2 \ A \ (f a1, f a2) \ R}" - -lemma relImage_Gr: -"\R \ A \ A\ \ relImage R f = (Gr A f)^-1 O R O Gr A f" -unfolding relImage_def Gr_def relcomp_def by auto - -lemma relInvImage_Gr: "\R \ B \ B\ \ relInvImage A R f = Gr A f O R O (Gr A f)^-1" -unfolding Gr_def relcomp_def image_def relInvImage_def by auto - -lemma relImage_mono: -"R1 \ R2 \ relImage R1 f \ relImage R2 f" -unfolding relImage_def by auto - -lemma relInvImage_mono: -"R1 \ R2 \ relInvImage A R1 f \ relInvImage A R2 f" -unfolding relInvImage_def by auto - -lemma relInvImage_diag: -"(\a1 a2. f a1 = f a2 \ a1 = a2) \ relInvImage A (diag B) f \ Id" -unfolding relInvImage_def diag_def by auto - -lemma relInvImage_UNIV_relImage: -"R \ relInvImage UNIV (relImage R f) f" -unfolding relInvImage_def relImage_def by auto - -lemma relImage_proj: -assumes "equiv A R" -shows "relImage R (proj R) \ diag (A//R)" -unfolding relImage_def diag_def apply safe -using proj_iff[OF assms] -by (metis assms equiv_Image proj_def proj_preserves) - -lemma relImage_relInvImage: -assumes "R \ f ` A <*> f ` A" -shows "relImage (relInvImage A R f) f = R" -using assms unfolding relImage_def relInvImage_def by fastforce - - -(* Relation composition as a weak pseudo-pullback *) - -(* pick middle *) -definition "pickM P Q a c = (SOME b. (a,b) \ P \ (b,c) \ Q)" - -lemma pickM: -assumes "(a,c) \ P O Q" -shows "(a, pickM P Q a c) \ P \ (pickM P Q a c, c) \ Q" -unfolding pickM_def apply(rule someI_ex) -using assms unfolding relcomp_def by auto - -definition fstO where "fstO P Q ac = (fst ac, pickM P Q (fst ac) (snd ac))" -definition sndO where "sndO P Q ac = (pickM P Q (fst ac) (snd ac), snd ac)" - -lemma fstO_in: "ac \ P O Q \ fstO P Q ac \ P" -by (metis assms fstO_def pickM surjective_pairing) - -lemma fst_fstO: "fst bc = (fst \ fstO P Q) bc" -unfolding comp_def fstO_def by simp - -lemma snd_sndO: "snd bc = (snd \ sndO P Q) bc" -unfolding comp_def sndO_def by simp - -lemma sndO_in: "ac \ P O Q \ sndO P Q ac \ Q" -by (metis assms sndO_def pickM surjective_pairing) - -lemma csquare_fstO_sndO: -"csquare (P O Q) snd fst (fstO P Q) (sndO P Q)" -unfolding csquare_def fstO_def sndO_def using pickM by auto - -lemma wppull_fstO_sndO: -shows "wppull (P O Q) P Q snd fst fst snd (fstO P Q) (sndO P Q)" -using pickM unfolding wppull_def fstO_def sndO_def relcomp_def by auto - -lemma subst_Pair: "P x y \ a = (x, y) \ P (fst a) (snd a)" -by simp - -lemma snd_fst_flip: "snd xy = (fst o (%(x, y). (y, x))) xy" -by (simp split: prod.split) - -lemma fst_snd_flip: "fst xy = (snd o (%(x, y). (y, x))) xy" -by (simp split: prod.split) - -lemma flip_rel: "A \ (R ^-1) \ (%(x, y). (y, x)) ` A \ R" -by auto - -lemma fst_diag_id: "(fst \ (%x. (x, x))) z = id z" -by simp - -lemma snd_diag_id: "(snd \ (%x. (x, x))) z = id z" -by simp - -lemma fst_snd: "\snd x = (y, z)\ \ fst (snd x) = y" -by simp - -lemma snd_snd: "\snd x = (y, z)\ \ snd (snd x) = z" -by simp - -lemma fstI: "x = (y, z) \ fst x = y" -by simp - -lemma sndI: "x = (y, z) \ snd x = z" -by simp - -lemma Collect_restrict: "{x. x \ X \ P x} \ X" -by auto - -lemma Collect_restrict': "{(x, y) | x y. phi x y \ P x y} \ {(x, y) | x y. phi x y}" -by auto - -lemma prop_restrict: "\x \ Z; Z \ {x. x \ X \ P x}\ \ P x" -by auto - -lemma underS_I: "\i \ j; (i, j) \ R\ \ i \ rel.underS R j" -unfolding rel.underS_def by simp - -lemma underS_E: "i \ rel.underS R j \ i \ j \ (i, j) \ R" -unfolding rel.underS_def by simp - -lemma underS_Field: "i \ rel.underS R j \ i \ Field R" -unfolding rel.underS_def Field_def by auto - -lemma FieldI2: "(i, j) \ R \ j \ Field R" -unfolding Field_def by auto - - -subsection {* Convolution product *} - -definition convol ("<_ , _>") where -" \ %a. (f a, g a)" - -lemma fst_convol: -"fst o = f" -apply(rule ext) -unfolding convol_def by simp - -lemma snd_convol: -"snd o = g" -apply(rule ext) -unfolding convol_def by simp - -lemma fst_convol': "fst ( x) = f x" -using fst_convol unfolding convol_def by simp - -lemma snd_convol': "snd ( x) = g x" -using snd_convol unfolding convol_def by simp - -lemma image_convolD: "\(a, b) \ ` X\ \ \x. x \ X \ a = f x \ b = g x" -unfolding convol_def by auto - -lemma convol_expand_snd: "fst o f = g \ = f" -unfolding convol_def by auto - -subsection{* Facts about functions *} - -lemma pointfreeE: "f o g = f' o g' \ f (g x) = f' (g' x)" -unfolding o_def fun_eq_iff by simp - -lemma pointfree_idE: "f o g = id \ f (g x) = x" -unfolding o_def fun_eq_iff by simp - -definition inver where - "inver g f A = (ALL a : A. g (f a) = a)" - -lemma bij_betw_iff_ex: - "bij_betw f A B = (EX g. g ` B = A \ inver g f A \ inver f g B)" (is "?L = ?R") -proof (rule iffI) - assume ?L - hence f: "f ` A = B" and inj_f: "inj_on f A" unfolding bij_betw_def by auto - let ?phi = "% b a. a : A \ f a = b" - have "ALL b : B. EX a. ?phi b a" using f by blast - then obtain g where g: "ALL b : B. g b : A \ f (g b) = b" - using bchoice[of B ?phi] by blast - hence gg: "ALL b : f ` A. g b : A \ f (g b) = b" using f by blast - have gf: "inver g f A" unfolding inver_def by (metis gg imageI inj_f the_inv_into_f_f) - moreover have "g ` B \ A \ inver f g B" using g unfolding inver_def by blast - moreover have "A \ g ` B" - proof safe - fix a assume a: "a : A" - hence "f a : B" using f by auto - moreover have "a = g (f a)" using a gf unfolding inver_def by auto - ultimately show "a : g ` B" by blast - qed - ultimately show ?R by blast -next - assume ?R - then obtain g where g: "g ` B = A \ inver g f A \ inver f g B" by blast - show ?L unfolding bij_betw_def - proof safe - show "inj_on f A" unfolding inj_on_def - proof safe - fix a1 a2 assume a: "a1 : A" "a2 : A" and "f a1 = f a2" - hence "g (f a1) = g (f a2)" by simp - thus "a1 = a2" using a g unfolding inver_def by simp - qed - next - fix a assume "a : A" - then obtain b where b: "b : B" and a: "a = g b" using g by blast - hence "b = f (g b)" using g unfolding inver_def by auto - thus "f a : B" unfolding a using b by simp - next - fix b assume "b : B" - hence "g b : A \ b = f (g b)" using g unfolding inver_def by auto - thus "b : f ` A" by auto - qed -qed - -lemma bijI: "\\x y. (f x = f y) = (x = y); \y. \x. y = f x\ \ bij f" -unfolding bij_def inj_on_def by auto blast - -lemma bij_betw_ex_weakE: - "\bij_betw f A B\ \ \g. g ` B \ A \ inver g f A \ inver f g B" -by (auto simp only: bij_betw_iff_ex) - -lemma inver_surj: "\g ` B \ A; f ` A \ B; inver g f A\ \ g ` B = A" -unfolding inver_def by auto (rule rev_image_eqI, auto) - -lemma inver_mono: "\A \ B; inver f g B\ \ inver f g A" -unfolding inver_def by auto - -lemma inver_pointfree: "inver f g A = (\a \ A. (f o g) a = a)" -unfolding inver_def by simp - -lemma bij_betwE: "bij_betw f A B \ \a\A. f a \ B" -unfolding bij_betw_def by auto - -lemma bij_betw_imageE: "bij_betw f A B \ f ` A = B" -unfolding bij_betw_def by auto - -lemma inverE: "\inver f f' A; x \ A\ \ f (f' x) = x" -unfolding inver_def by auto - -lemma bij_betw_inver1: "bij_betw f A B \ inver (inv_into A f) f A" -unfolding bij_betw_def inver_def by auto - -lemma bij_betw_inver2: "bij_betw f A B \ inver f (inv_into A f) B" -unfolding bij_betw_def inver_def by auto - -lemma bij_betwI: "\bij_betw g B A; inver g f A; inver f g B\ \ bij_betw f A B" -by (metis bij_betw_iff_ex bij_betw_imageE) - -lemma bij_betwI': - "\\x y. \x \ X; y \ X\ \ (f x = f y) = (x = y); - \x. x \ X \ f x \ Y; - \y. y \ Y \ \x \ X. y = f x\ \ bij_betw f X Y" -unfolding bij_betw_def inj_on_def by auto (metis rev_image_eqI) - -lemma o_bij: - assumes gf: "g o f = id" and fg: "f o g = id" - shows "bij f" -unfolding bij_def inj_on_def surj_def proof safe - fix a1 a2 assume "f a1 = f a2" - hence "g ( f a1) = g (f a2)" by simp - thus "a1 = a2" using gf unfolding fun_eq_iff by simp -next - fix b - have "b = f (g b)" - using fg unfolding fun_eq_iff by simp - thus "EX a. b = f a" by blast -qed - -lemma surj_fun_eq: - assumes surj_on: "f ` X = UNIV" and eq_on: "\x \ X. (g1 o f) x = (g2 o f) x" - shows "g1 = g2" -proof (rule ext) - fix y - from surj_on obtain x where "x \ X" and "y = f x" by blast - thus "g1 y = g2 y" using eq_on by simp -qed - -lemma Card_order_wo_rel: "Card_order r \ wo_rel r" -unfolding wo_rel_def card_order_on_def by blast - -lemma Cinfinite_limit: "\x \ Field r; Cinfinite r\ \ - \y \ Field r. x \ y \ (x, y) \ r" -unfolding cinfinite_def by (auto simp add: infinite_Card_order_limit) - -lemma Card_order_trans: - "\Card_order r; x \ y; (x, y) \ r; y \ z; (y, z) \ r\ \ x \ z \ (x, z) \ r" -unfolding card_order_on_def well_order_on_def linear_order_on_def - partial_order_on_def preorder_on_def trans_def antisym_def by blast - -lemma Cinfinite_limit2: - assumes x1: "x1 \ Field r" and x2: "x2 \ Field r" and r: "Cinfinite r" - shows "\y \ Field r. (x1 \ y \ (x1, y) \ r) \ (x2 \ y \ (x2, y) \ r)" -proof - - from r have trans: "trans r" and total: "Total r" and antisym: "antisym r" - unfolding card_order_on_def well_order_on_def linear_order_on_def - partial_order_on_def preorder_on_def by auto - obtain y1 where y1: "y1 \ Field r" "x1 \ y1" "(x1, y1) \ r" - using Cinfinite_limit[OF x1 r] by blast - obtain y2 where y2: "y2 \ Field r" "x2 \ y2" "(x2, y2) \ r" - using Cinfinite_limit[OF x2 r] by blast - show ?thesis - proof (cases "y1 = y2") - case True with y1 y2 show ?thesis by blast - next - case False - with y1(1) y2(1) total have "(y1, y2) \ r \ (y2, y1) \ r" - unfolding total_on_def by auto - thus ?thesis - proof - assume *: "(y1, y2) \ r" - with trans y1(3) have "(x1, y2) \ r" unfolding trans_def by blast - with False y1 y2 * antisym show ?thesis by (cases "x1 = y2") (auto simp: antisym_def) - next - assume *: "(y2, y1) \ r" - with trans y2(3) have "(x2, y1) \ r" unfolding trans_def by blast - with False y1 y2 * antisym show ?thesis by (cases "x2 = y1") (auto simp: antisym_def) - qed - qed -qed - -lemma Cinfinite_limit_finite: "\finite X; X \ Field r; Cinfinite r\ - \ \y \ Field r. \x \ X. (x \ y \ (x, y) \ r)" -proof (induct X rule: finite_induct) - case empty thus ?case unfolding cinfinite_def using ex_in_conv[of "Field r"] finite.emptyI by auto -next - case (insert x X) - then obtain y where y: "y \ Field r" "\x \ X. (x \ y \ (x, y) \ r)" by blast - then obtain z where z: "z \ Field r" "x \ z \ (x, z) \ r" "y \ z \ (y, z) \ r" - using Cinfinite_limit2[OF _ y(1) insert(5), of x] insert(4) by blast - show ?case by (metis Card_order_trans insert(5) insertE y(2) z) -qed - -lemma insert_subsetI: "\x \ A; X \ A\ \ insert x X \ A" -by auto - -(*helps resolution*) -lemma well_order_induct_imp: - "wo_rel r \ (\x. \y. y \ x \ (y, x) \ r \ y \ Field r \ P y \ x \ Field r \ P x) \ - x \ Field r \ P x" -by (erule wo_rel.well_order_induct) - -lemma meta_spec2: - assumes "(\x y. PROP P x y)" - shows "PROP P x y" -by (rule `(\x y. PROP P x y)`) - -(*Extended Sublist*) - -definition prefCl where - "prefCl Kl = (\ kl1 kl2. kl1 \ kl2 \ kl2 \ Kl \ kl1 \ Kl)" -definition PrefCl where - "PrefCl A n = (\kl kl'. kl \ A n \ kl' \ kl \ (\m\n. kl' \ A m))" - -lemma prefCl_UN: - "\\n. PrefCl A n\ \ prefCl (\n. A n)" -unfolding prefCl_def PrefCl_def by fastforce - -definition Succ where "Succ Kl kl = {k . kl @ [k] \ Kl}" -definition Shift where "Shift Kl k = {kl. k # kl \ Kl}" -definition shift where "shift lab k = (\kl. lab (k # kl))" - -lemmas sh_def = Shift_def shift_def - -lemma empty_Shift: "\[] \ Kl; k \ Succ Kl []\ \ [] \ Shift Kl k" -unfolding Shift_def Succ_def by simp - -lemma Shift_clists: "Kl \ Field (clists r) \ Shift Kl k \ Field (clists r)" -unfolding Shift_def clists_def Field_card_of by auto - -lemma Shift_prefCl: "prefCl Kl \ prefCl (Shift Kl k)" -unfolding prefCl_def Shift_def -proof safe - fix kl1 kl2 - assume "\kl1 kl2. kl1 \ kl2 \ kl2 \ Kl \ kl1 \ Kl" - "kl1 \ kl2" "k # kl2 \ Kl" - thus "k # kl1 \ Kl" using Cons_prefix_Cons[of k kl1 k kl2] by blast -qed - -lemma not_in_Shift: "kl \ Shift Kl x \ x # kl \ Kl" -unfolding Shift_def by simp - -lemma prefCl_Succ: "\prefCl Kl; k # kl \ Kl\ \ k \ Succ Kl []" -unfolding Succ_def proof - assume "prefCl Kl" "k # kl \ Kl" - moreover have "k # [] \ k # kl" by auto - ultimately have "k # [] \ Kl" unfolding prefCl_def by blast - thus "[] @ [k] \ Kl" by simp -qed - -lemma SuccD: "k \ Succ Kl kl \ kl @ [k] \ Kl" -unfolding Succ_def by simp - -lemmas SuccE = SuccD[elim_format] - -lemma SuccI: "kl @ [k] \ Kl \ k \ Succ Kl kl" -unfolding Succ_def by simp - -lemma ShiftD: "kl \ Shift Kl k \ k # kl \ Kl" -unfolding Shift_def by simp - -lemma Succ_Shift: "Succ (Shift Kl k) kl = Succ Kl (k # kl)" -unfolding Succ_def Shift_def by auto - -lemma ShiftI: "k # kl \ Kl \ kl \ Shift Kl k" -unfolding Shift_def by simp - -lemma Func_cexp: "|Func A B| =o |B| ^c |A|" -unfolding cexp_def Field_card_of by (simp only: card_of_refl) - -lemma clists_bound: "A \ Field (cpow (clists r)) - {{}} \ |A| \o clists r" -unfolding cpow_def clists_def Field_card_of by (auto simp: card_of_mono1) - -lemma cpow_clists_czero: "\A \ Field (cpow (clists r)) - {{}}; |A| =o czero\ \ False" -unfolding cpow_def clists_def -by (auto simp add: card_of_ordIso_czero_iff_empty[symmetric]) - (erule notE, erule ordIso_transitive, rule czero_ordIso) - -lemma incl_UNION_I: -assumes "i \ I" and "A \ F i" -shows "A \ UNION I F" -using assms by auto - -lemma Nil_clists: "{[]} \ Field (clists r)" -unfolding clists_def Field_card_of by auto - -lemma Cons_clists: - "\x \ Field r; xs \ Field (clists r)\ \ x # xs \ Field (clists r)" -unfolding clists_def Field_card_of by auto - -lemma length_Cons: "length (x#xs) = Suc (length xs)" -by simp - -lemma length_append_singleton: "length (xs @ [x]) = Suc (length xs)" -by simp - -(*injection into the field of a cardinal*) -definition "toCard_pred A r f \ inj_on f A \ f ` A \ Field r \ Card_order r" -definition "toCard A r \ SOME f. toCard_pred A r f" - -lemma ex_toCard_pred: -"\|A| \o r; Card_order r\ \ \ f. toCard_pred A r f" -unfolding toCard_pred_def -using card_of_ordLeq[of A "Field r"] - ordLeq_ordIso_trans[OF _ card_of_unique[of "Field r" r], of "|A|"] -by blast - -lemma toCard_pred_toCard: - "\|A| \o r; Card_order r\ \ toCard_pred A r (toCard A r)" -unfolding toCard_def using someI_ex[OF ex_toCard_pred] . - -lemma toCard_inj: "\|A| \o r; Card_order r; x \ A; y \ A\ \ - toCard A r x = toCard A r y \ x = y" -using toCard_pred_toCard unfolding inj_on_def toCard_pred_def by blast - -lemma toCard: "\|A| \o r; Card_order r; b \ A\ \ toCard A r b \ Field r" -using toCard_pred_toCard unfolding toCard_pred_def by blast - -definition "fromCard A r k \ SOME b. b \ A \ toCard A r b = k" - -lemma fromCard_toCard: -"\|A| \o r; Card_order r; b \ A\ \ fromCard A r (toCard A r b) = b" -unfolding fromCard_def by (rule some_equality) (auto simp add: toCard_inj) - -(* pick according to the weak pullback *) -definition pickWP_pred where -"pickWP_pred A p1 p2 b1 b2 a \ - a \ A \ p1 a = b1 \ p2 a = b2" - -definition pickWP where -"pickWP A p1 p2 b1 b2 \ - SOME a. pickWP_pred A p1 p2 b1 b2 a" - -lemma pickWP_pred: -assumes "wpull A B1 B2 f1 f2 p1 p2" and -"b1 \ B1" and "b2 \ B2" and "f1 b1 = f2 b2" -shows "\ a. pickWP_pred A p1 p2 b1 b2 a" -using assms unfolding wpull_def pickWP_pred_def by blast - -lemma pickWP_pred_pickWP: -assumes "wpull A B1 B2 f1 f2 p1 p2" and -"b1 \ B1" and "b2 \ B2" and "f1 b1 = f2 b2" -shows "pickWP_pred A p1 p2 b1 b2 (pickWP A p1 p2 b1 b2)" -unfolding pickWP_def using assms by(rule someI_ex[OF pickWP_pred]) - -lemma pickWP: -assumes "wpull A B1 B2 f1 f2 p1 p2" and -"b1 \ B1" and "b2 \ B2" and "f1 b1 = f2 b2" -shows "pickWP A p1 p2 b1 b2 \ A" - "p1 (pickWP A p1 p2 b1 b2) = b1" - "p2 (pickWP A p1 p2 b1 b2) = b2" -using assms pickWP_pred_pickWP unfolding pickWP_pred_def by fastforce+ - -lemma ssubst_mem: "\t = s; s \ X\ \ t \ X" by simp - -lemma Inl_Field_csum: "a \ Field r \ Inl a \ Field (r +c s)" -unfolding Field_card_of csum_def by auto - -lemma Inr_Field_csum: "a \ Field s \ Inr a \ Field (r +c s)" -unfolding Field_card_of csum_def by auto - -lemma nat_rec_0: "f = nat_rec f1 (%n rec. f2 n rec) \ f 0 = f1" -by auto - -lemma nat_rec_Suc: "f = nat_rec f1 (%n rec. f2 n rec) \ f (Suc n) = f2 n (f n)" -by auto - -lemma list_rec_Nil: "f = list_rec f1 (%x xs rec. f2 x xs rec) \ f [] = f1" -by auto - -lemma list_rec_Cons: "f = list_rec f1 (%x xs rec. f2 x xs rec) \ f (x # xs) = f2 x xs (f xs)" -by auto - -lemma sum_case_cong: "p = q \ sum_case f g p = sum_case f g q" -by simp - -lemma sum_case_step: - "sum_case (sum_case f' g') g (Inl p) = sum_case f' g' p" - "sum_case f (sum_case f' g') (Inr p) = sum_case f' g' p" -by auto - -lemma one_pointE: "\\x. s = x \ P\ \ P" -by simp - -lemma obj_one_pointE: "\x. s = x \ P \ P" -by blast - -lemma obj_sumE_f: -"\\x. s = f (Inl x) \ P; \x. s = f (Inr x) \ P\ \ \x. s = f x \ P" -by (metis sum.exhaust) - -lemma obj_sumE: "\\x. s = Inl x \ P; \x. s = Inr x \ P\ \ P" -by (cases s) auto - -lemma obj_sum_step: - "\\x. s = f (Inr (Inl x)) \ P; \x. s = f (Inr (Inr x)) \ P\ \ \x. s = f (Inr x) \ P" -by (metis obj_sumE) - -lemma not_arg_cong_Inr: "x \ y \ Inr x \ Inr y" -by simp - -end diff -r 64bed36cd8da -r 66058a677ddd src/HOL/Codatatype/BNF_Util.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Codatatype/BNF_Util.thy Tue Sep 11 19:45:12 2012 +0200 @@ -0,0 +1,859 @@ +(* Title: HOL/Codatatype/BNF_Util.thy + Author: Dmitriy Traytel, TU Muenchen + Author: Jasmin Blanchette, TU Muenchen + Copyright 2012 + +Library for bounded natural functors. +*) + +header {* Library for Bounded Natural Functors *} + +theory BNF_Util +imports + "../Ordinals_and_Cardinals/Cardinal_Arithmetic" + "~~/src/HOL/Library/Prefix_Order" + Equiv_Relations_More +uses + ("Tools/bnf_util.ML") +begin + +lemma iffI_np: "\x \ \ y; \ x \ y\ \ \ x \ y" +by (erule iffI) (erule contrapos_pn) + +lemma all_unit_eq: "(\x. PROP P x) \ PROP P ()" by simp + +lemma all_prod_eq: "(\x. PROP P x) \ (\a b. PROP P (a, b))" by clarsimp + +lemma False_imp_eq: "(False \ P) \ Trueprop True" +by presburger + +lemma case_unit: "(case u of () => f) = f" +by (cases u) (hypsubst, rule unit.cases) + +lemma All_point_1: "(\z. z = b \ phi z) \ Trueprop (phi b)" +by presburger + +lemma subset_Collect_iff: "B \ A \ (B \ {x \ A. P x}) = (\x \ B. P x)" +by blast + +lemma subset_CollectI: "B \ A \ (\x. x \ B \ Q x \ P x) \ ({x \ B. Q x} \ {x \ A. P x})" +by blast + +lemma mem_Collect_eq_split: "{(x, y). (x, y) \ X} = X" +by simp + +lemma image_comp: "image (f o g) = image f o image g" +by (rule ext) (auto simp only: o_apply image_def) + +lemma empty_natural: "(\_. {}) o f = image g o (\_. {})" +by (rule ext) simp + +lemma Union_natural: "Union o image (image f) = image f o Union" +by (rule ext) (auto simp only: o_apply) + +lemma in_Union_o_assoc: "x \ (Union o gset o gmap) A \ x \ (Union o (gset o gmap)) A" +by (unfold o_assoc) + +lemma comp_single_set_bd: + assumes fbd_Card_order: "Card_order fbd" and + fset_bd: "\x. |fset x| \o fbd" and + gset_bd: "\x. |gset x| \o gbd" + shows "|\fset ` gset x| \o gbd *c fbd" +apply (subst sym[OF SUP_def]) +apply (rule ordLeq_transitive) +apply (rule card_of_UNION_Sigma) +apply (subst SIGMA_CSUM) +apply (rule ordLeq_transitive) +apply (rule card_of_Csum_Times') +apply (rule fbd_Card_order) +apply (rule ballI) +apply (rule fset_bd) +apply (rule ordLeq_transitive) +apply (rule cprod_mono1) +apply (rule gset_bd) +apply (rule ordIso_imp_ordLeq) +apply (rule ordIso_refl) +apply (rule Card_order_cprod) +done + +lemma Union_image_insert: "\f ` insert a B = f a \ \f ` B" +by simp + +lemma Union_image_empty: "A \ \f ` {} = A" +by simp + +definition collect where + "collect F x = (\f \ F. f x)" + +lemma collect_o: "collect F o g = collect ((\f. f o g) ` F)" +by (rule ext) (auto simp only: o_apply collect_def) + +lemma image_o_collect: "collect ((\f. image g o f) ` F) = image g o collect F" +by (rule ext) (auto simp add: collect_def) + +lemma conj_subset_def: "A \ {x. P x \ Q x} = (A \ {x. P x} \ A \ {x. Q x})" +by blast + +lemma subset_emptyI: "(\x. x \ A \ False) \ A \ {}" +by blast + +lemma rev_bspec: "a \ A \ \z \ A. P z \ P a" +by simp + +lemma Un_cong: "\A = B; C = D\ \ A \ C = B \ D" +by simp + +lemma UN_image_subset: "\f ` g x \ X = (g x \ {x. f x \ X})" +by blast + +lemma image_Collect_subsetI: + "(\x. P x \ f x \ B) \ f ` {x. P x} \ B" +by blast + +lemma comp_set_bd_Union_o_collect: "|\\(\f. f x) ` X| \o hbd \ |(Union \ collect X) x| \o hbd" +by (unfold o_apply collect_def SUP_def) + +lemma sum_case_comp_Inl: +"sum_case f g \ Inl = f" +unfolding comp_def by simp + +lemma sum_case_expand_Inr: "f o Inl = g \ f x = sum_case g (f o Inr) x" +by (auto split: sum.splits) + +lemma converse_mono: +"R1 ^-1 \ R2 ^-1 \ R1 \ R2" +unfolding converse_def by auto + +lemma converse_shift: +"R1 \ R2 ^-1 \ R1 ^-1 \ R2" +unfolding converse_def by auto + +lemma converse_Times: "(A \ B) ^-1 = B \ A" +by auto + +lemma equiv_triv1: +assumes "equiv A R" and "(a, b) \ R" and "(a, c) \ R" +shows "(b, c) \ R" +using assms unfolding equiv_def sym_def trans_def by blast + +lemma equiv_triv2: +assumes "equiv A R" and "(a, b) \ R" and "(b, c) \ R" +shows "(a, c) \ R" +using assms unfolding equiv_def trans_def by blast + +lemma equiv_proj: + assumes e: "equiv A R" and "z \ R" + shows "(proj R o fst) z = (proj R o snd) z" +proof - + from assms(2) have z: "(fst z, snd z) \ R" by auto + have P: "\x. (fst z, x) \ R \ (snd z, x) \ R" by (erule equiv_triv1[OF e z]) + have "\x. (snd z, x) \ R \ (fst z, x) \ R" by (erule equiv_triv2[OF e z]) + with P show ?thesis unfolding proj_def[abs_def] by auto +qed + + +section{* Weak pullbacks: *} + +definition csquare where +"csquare A f1 f2 p1 p2 \ (\ a \ A. f1 (p1 a) = f2 (p2 a))" + +definition wpull where +"wpull A B1 B2 f1 f2 p1 p2 \ + (\ b1 b2. b1 \ B1 \ b2 \ B2 \ f1 b1 = f2 b2 \ (\ a \ A. p1 a = b1 \ p2 a = b2))" + +lemma wpull_cong: +"\A' = A; B1' = B1; B2' = B2; wpull A B1 B2 f1 f2 p1 p2\ \ wpull A' B1' B2' f1 f2 p1 p2" +by simp + +lemma wpull_id: "wpull UNIV B1 B2 id id id id" +unfolding wpull_def by simp + + +(* Weak pseudo-pullbacks *) + +definition wppull where +"wppull A B1 B2 f1 f2 e1 e2 p1 p2 \ + (\ b1 b2. b1 \ B1 \ b2 \ B2 \ f1 b1 = f2 b2 \ + (\ a \ A. e1 (p1 a) = e1 b1 \ e2 (p2 a) = e2 b2))" + + +(* The pullback of sets *) +definition thePull where +"thePull B1 B2 f1 f2 = {(b1,b2). b1 \ B1 \ b2 \ B2 \ f1 b1 = f2 b2}" + +lemma wpull_thePull: +"wpull (thePull B1 B2 f1 f2) B1 B2 f1 f2 fst snd" +unfolding wpull_def thePull_def by auto + +lemma wppull_thePull: +assumes "wppull A B1 B2 f1 f2 e1 e2 p1 p2" +shows +"\ j. \ a' \ thePull B1 B2 f1 f2. + j a' \ A \ + e1 (p1 (j a')) = e1 (fst a') \ e2 (p2 (j a')) = e2 (snd a')" +(is "\ j. \ a' \ ?A'. ?phi a' (j a')") +proof(rule bchoice[of ?A' ?phi], default) + fix a' assume a': "a' \ ?A'" + hence "fst a' \ B1" unfolding thePull_def by auto + moreover + from a' have "snd a' \ B2" unfolding thePull_def by auto + moreover have "f1 (fst a') = f2 (snd a')" + using a' unfolding csquare_def thePull_def by auto + ultimately show "\ ja'. ?phi a' ja'" + using assms unfolding wppull_def by auto +qed + +lemma wpull_wppull: +assumes wp: "wpull A' B1 B2 f1 f2 p1' p2'" and +1: "\ a' \ A'. j a' \ A \ e1 (p1 (j a')) = e1 (p1' a') \ e2 (p2 (j a')) = e2 (p2' a')" +shows "wppull A B1 B2 f1 f2 e1 e2 p1 p2" +unfolding wppull_def proof safe + fix b1 b2 + assume b1: "b1 \ B1" and b2: "b2 \ B2" and f: "f1 b1 = f2 b2" + then obtain a' where a': "a' \ A'" and b1: "b1 = p1' a'" and b2: "b2 = p2' a'" + using wp unfolding wpull_def by blast + show "\a\A. e1 (p1 a) = e1 b1 \ e2 (p2 a) = e2 b2" + apply(rule bexI[of _ "j a'"]) unfolding b1 b2 using a' 1 by auto +qed + +lemma wppull_id: "\wpull UNIV UNIV UNIV f1 f2 p1 p2; e1 = id; e2 = id\ \ + wppull UNIV UNIV UNIV f1 f2 e1 e2 p1 p2" +by (erule wpull_wppull) auto + + +(* Operators: *) +definition diag where "diag A \ {(a,a) | a. a \ A}" +definition "Gr A f = {(a,f a) | a. a \ A}" +definition image2 where "image2 A f g = {(f a, g a) | a. a \ A}" + +lemma diagI: "x \ A \ (x, x) \ diag A" +unfolding diag_def by simp + +lemma diagE: "(a, b) \ diag A \ a = b" +unfolding diag_def by simp + +lemma diagE': "x \ diag A \ fst x = snd x" +unfolding diag_def by auto + +lemma diag_fst: "x \ diag A \ fst x \ A" +unfolding diag_def by auto + +lemma diag_UNIV: "diag UNIV = Id" +unfolding diag_def by auto + +lemma diag_converse: "diag A = (diag A) ^-1" +unfolding diag_def by auto + +lemma diag_Comp: "diag A = diag A O diag A" +unfolding diag_def by auto + +lemma diag_Gr: "diag A = Gr A id" +unfolding diag_def Gr_def by simp + +lemma diag_UNIV_I: "x = y \ (x, y) \ diag UNIV" +unfolding diag_def by auto + +lemma image2_eqI: "\b = f x; c = g x; x \ A\ \ (b, c) \ image2 A f g" +unfolding image2_def by auto + +lemma Id_def': "Id = {(a,b). a = b}" +by auto + +lemma Id_alt: "Id = Gr UNIV id" +unfolding Gr_def by auto + +lemma Id_subset: "Id \ {(a, b). P a b \ a = b}" +by auto + +lemma IdD: "(a, b) \ Id \ a = b" +by auto + +lemma image2_Gr: "image2 A f g = (Gr A f)^-1 O (Gr A g)" +unfolding image2_def Gr_def by auto + +lemma GrI: "\x \ A; f x = fx\ \ (x, fx) \ Gr A f" +unfolding Gr_def by simp + +lemma GrE: "(x, fx) \ Gr A f \ (x \ A \ f x = fx \ P) \ P" +unfolding Gr_def by simp + +lemma GrD1: "(x, fx) \ Gr A f \ x \ A" +unfolding Gr_def by simp + +lemma GrD2: "(x, fx) \ Gr A f \ f x = fx" +unfolding Gr_def by simp + +lemma Gr_UNIV_id: "f = id \ (Gr UNIV f)^-1 O Gr UNIV f = Gr UNIV f" +unfolding Gr_def by auto + +lemma Gr_fst_snd: "(Gr R fst)^-1 O Gr R snd = R" +unfolding Gr_def by auto + +lemma Gr_mono: "A \ B \ Gr A f \ Gr B f" +unfolding Gr_def by auto + +lemma subst_rel_def: "A = B \ (Gr A f)^-1 O Gr A g = (Gr B f)^-1 O Gr B g" +by simp + +lemma abs_pred_def: "\\x y. (x, y) \ rel = pred x y\ \ rel = Collect (split pred)" +by auto + +lemma Collect_split_cong: "Collect (split pred) = Collect (split pred') \ pred = pred'" +by blast + +lemma pred_def_abs: "rel = Collect (split pred) \ pred = (\x y. (x, y) \ rel)" +by auto + +lemma wpull_Gr: +"wpull (Gr A f) A (f ` A) f id fst snd" +unfolding wpull_def Gr_def by auto + +lemma Gr_incl: "Gr A f \ A <*> B \ f ` A \ B" +unfolding Gr_def by auto + +lemma equiv_Image: "equiv A R \ (\a b. (a, b) \ R \ a \ A \ b \ A \ R `` {a} = R `` {b})" +unfolding equiv_def refl_on_def Image_def by (auto intro: transD symD) + +definition relImage where +"relImage R f \ {(f a1, f a2) | a1 a2. (a1,a2) \ R}" + +definition relInvImage where +"relInvImage A R f \ {(a1, a2) | a1 a2. a1 \ A \ a2 \ A \ (f a1, f a2) \ R}" + +lemma relImage_Gr: +"\R \ A \ A\ \ relImage R f = (Gr A f)^-1 O R O Gr A f" +unfolding relImage_def Gr_def relcomp_def by auto + +lemma relInvImage_Gr: "\R \ B \ B\ \ relInvImage A R f = Gr A f O R O (Gr A f)^-1" +unfolding Gr_def relcomp_def image_def relInvImage_def by auto + +lemma relImage_mono: +"R1 \ R2 \ relImage R1 f \ relImage R2 f" +unfolding relImage_def by auto + +lemma relInvImage_mono: +"R1 \ R2 \ relInvImage A R1 f \ relInvImage A R2 f" +unfolding relInvImage_def by auto + +lemma relInvImage_diag: +"(\a1 a2. f a1 = f a2 \ a1 = a2) \ relInvImage A (diag B) f \ Id" +unfolding relInvImage_def diag_def by auto + +lemma relInvImage_UNIV_relImage: +"R \ relInvImage UNIV (relImage R f) f" +unfolding relInvImage_def relImage_def by auto + +lemma relImage_proj: +assumes "equiv A R" +shows "relImage R (proj R) \ diag (A//R)" +unfolding relImage_def diag_def apply safe +using proj_iff[OF assms] +by (metis assms equiv_Image proj_def proj_preserves) + +lemma relImage_relInvImage: +assumes "R \ f ` A <*> f ` A" +shows "relImage (relInvImage A R f) f = R" +using assms unfolding relImage_def relInvImage_def by fastforce + + +(* Relation composition as a weak pseudo-pullback *) + +(* pick middle *) +definition "pickM P Q a c = (SOME b. (a,b) \ P \ (b,c) \ Q)" + +lemma pickM: +assumes "(a,c) \ P O Q" +shows "(a, pickM P Q a c) \ P \ (pickM P Q a c, c) \ Q" +unfolding pickM_def apply(rule someI_ex) +using assms unfolding relcomp_def by auto + +definition fstO where "fstO P Q ac = (fst ac, pickM P Q (fst ac) (snd ac))" +definition sndO where "sndO P Q ac = (pickM P Q (fst ac) (snd ac), snd ac)" + +lemma fstO_in: "ac \ P O Q \ fstO P Q ac \ P" +by (metis assms fstO_def pickM surjective_pairing) + +lemma fst_fstO: "fst bc = (fst \ fstO P Q) bc" +unfolding comp_def fstO_def by simp + +lemma snd_sndO: "snd bc = (snd \ sndO P Q) bc" +unfolding comp_def sndO_def by simp + +lemma sndO_in: "ac \ P O Q \ sndO P Q ac \ Q" +by (metis assms sndO_def pickM surjective_pairing) + +lemma csquare_fstO_sndO: +"csquare (P O Q) snd fst (fstO P Q) (sndO P Q)" +unfolding csquare_def fstO_def sndO_def using pickM by auto + +lemma wppull_fstO_sndO: +shows "wppull (P O Q) P Q snd fst fst snd (fstO P Q) (sndO P Q)" +using pickM unfolding wppull_def fstO_def sndO_def relcomp_def by auto + +lemma subst_Pair: "P x y \ a = (x, y) \ P (fst a) (snd a)" +by simp + +lemma snd_fst_flip: "snd xy = (fst o (%(x, y). (y, x))) xy" +by (simp split: prod.split) + +lemma fst_snd_flip: "fst xy = (snd o (%(x, y). (y, x))) xy" +by (simp split: prod.split) + +lemma flip_rel: "A \ (R ^-1) \ (%(x, y). (y, x)) ` A \ R" +by auto + +lemma fst_diag_id: "(fst \ (%x. (x, x))) z = id z" +by simp + +lemma snd_diag_id: "(snd \ (%x. (x, x))) z = id z" +by simp + +lemma fst_snd: "\snd x = (y, z)\ \ fst (snd x) = y" +by simp + +lemma snd_snd: "\snd x = (y, z)\ \ snd (snd x) = z" +by simp + +lemma fstI: "x = (y, z) \ fst x = y" +by simp + +lemma sndI: "x = (y, z) \ snd x = z" +by simp + +lemma Collect_restrict: "{x. x \ X \ P x} \ X" +by auto + +lemma Collect_restrict': "{(x, y) | x y. phi x y \ P x y} \ {(x, y) | x y. phi x y}" +by auto + +lemma prop_restrict: "\x \ Z; Z \ {x. x \ X \ P x}\ \ P x" +by auto + +lemma underS_I: "\i \ j; (i, j) \ R\ \ i \ rel.underS R j" +unfolding rel.underS_def by simp + +lemma underS_E: "i \ rel.underS R j \ i \ j \ (i, j) \ R" +unfolding rel.underS_def by simp + +lemma underS_Field: "i \ rel.underS R j \ i \ Field R" +unfolding rel.underS_def Field_def by auto + +lemma FieldI2: "(i, j) \ R \ j \ Field R" +unfolding Field_def by auto + + +subsection {* Convolution product *} + +definition convol ("<_ , _>") where +" \ %a. (f a, g a)" + +lemma fst_convol: +"fst o = f" +apply(rule ext) +unfolding convol_def by simp + +lemma snd_convol: +"snd o = g" +apply(rule ext) +unfolding convol_def by simp + +lemma fst_convol': "fst ( x) = f x" +using fst_convol unfolding convol_def by simp + +lemma snd_convol': "snd ( x) = g x" +using snd_convol unfolding convol_def by simp + +lemma image_convolD: "\(a, b) \ ` X\ \ \x. x \ X \ a = f x \ b = g x" +unfolding convol_def by auto + +lemma convol_expand_snd: "fst o f = g \ = f" +unfolding convol_def by auto + +subsection{* Facts about functions *} + +lemma pointfreeE: "f o g = f' o g' \ f (g x) = f' (g' x)" +unfolding o_def fun_eq_iff by simp + +lemma pointfree_idE: "f o g = id \ f (g x) = x" +unfolding o_def fun_eq_iff by simp + +definition inver where + "inver g f A = (ALL a : A. g (f a) = a)" + +lemma bij_betw_iff_ex: + "bij_betw f A B = (EX g. g ` B = A \ inver g f A \ inver f g B)" (is "?L = ?R") +proof (rule iffI) + assume ?L + hence f: "f ` A = B" and inj_f: "inj_on f A" unfolding bij_betw_def by auto + let ?phi = "% b a. a : A \ f a = b" + have "ALL b : B. EX a. ?phi b a" using f by blast + then obtain g where g: "ALL b : B. g b : A \ f (g b) = b" + using bchoice[of B ?phi] by blast + hence gg: "ALL b : f ` A. g b : A \ f (g b) = b" using f by blast + have gf: "inver g f A" unfolding inver_def by (metis gg imageI inj_f the_inv_into_f_f) + moreover have "g ` B \ A \ inver f g B" using g unfolding inver_def by blast + moreover have "A \ g ` B" + proof safe + fix a assume a: "a : A" + hence "f a : B" using f by auto + moreover have "a = g (f a)" using a gf unfolding inver_def by auto + ultimately show "a : g ` B" by blast + qed + ultimately show ?R by blast +next + assume ?R + then obtain g where g: "g ` B = A \ inver g f A \ inver f g B" by blast + show ?L unfolding bij_betw_def + proof safe + show "inj_on f A" unfolding inj_on_def + proof safe + fix a1 a2 assume a: "a1 : A" "a2 : A" and "f a1 = f a2" + hence "g (f a1) = g (f a2)" by simp + thus "a1 = a2" using a g unfolding inver_def by simp + qed + next + fix a assume "a : A" + then obtain b where b: "b : B" and a: "a = g b" using g by blast + hence "b = f (g b)" using g unfolding inver_def by auto + thus "f a : B" unfolding a using b by simp + next + fix b assume "b : B" + hence "g b : A \ b = f (g b)" using g unfolding inver_def by auto + thus "b : f ` A" by auto + qed +qed + +lemma bijI: "\\x y. (f x = f y) = (x = y); \y. \x. y = f x\ \ bij f" +unfolding bij_def inj_on_def by auto blast + +lemma bij_betw_ex_weakE: + "\bij_betw f A B\ \ \g. g ` B \ A \ inver g f A \ inver f g B" +by (auto simp only: bij_betw_iff_ex) + +lemma inver_surj: "\g ` B \ A; f ` A \ B; inver g f A\ \ g ` B = A" +unfolding inver_def by auto (rule rev_image_eqI, auto) + +lemma inver_mono: "\A \ B; inver f g B\ \ inver f g A" +unfolding inver_def by auto + +lemma inver_pointfree: "inver f g A = (\a \ A. (f o g) a = a)" +unfolding inver_def by simp + +lemma bij_betwE: "bij_betw f A B \ \a\A. f a \ B" +unfolding bij_betw_def by auto + +lemma bij_betw_imageE: "bij_betw f A B \ f ` A = B" +unfolding bij_betw_def by auto + +lemma inverE: "\inver f f' A; x \ A\ \ f (f' x) = x" +unfolding inver_def by auto + +lemma bij_betw_inver1: "bij_betw f A B \ inver (inv_into A f) f A" +unfolding bij_betw_def inver_def by auto + +lemma bij_betw_inver2: "bij_betw f A B \ inver f (inv_into A f) B" +unfolding bij_betw_def inver_def by auto + +lemma bij_betwI: "\bij_betw g B A; inver g f A; inver f g B\ \ bij_betw f A B" +by (metis bij_betw_iff_ex bij_betw_imageE) + +lemma bij_betwI': + "\\x y. \x \ X; y \ X\ \ (f x = f y) = (x = y); + \x. x \ X \ f x \ Y; + \y. y \ Y \ \x \ X. y = f x\ \ bij_betw f X Y" +unfolding bij_betw_def inj_on_def by auto (metis rev_image_eqI) + +lemma o_bij: + assumes gf: "g o f = id" and fg: "f o g = id" + shows "bij f" +unfolding bij_def inj_on_def surj_def proof safe + fix a1 a2 assume "f a1 = f a2" + hence "g ( f a1) = g (f a2)" by simp + thus "a1 = a2" using gf unfolding fun_eq_iff by simp +next + fix b + have "b = f (g b)" + using fg unfolding fun_eq_iff by simp + thus "EX a. b = f a" by blast +qed + +lemma surj_fun_eq: + assumes surj_on: "f ` X = UNIV" and eq_on: "\x \ X. (g1 o f) x = (g2 o f) x" + shows "g1 = g2" +proof (rule ext) + fix y + from surj_on obtain x where "x \ X" and "y = f x" by blast + thus "g1 y = g2 y" using eq_on by simp +qed + +lemma Card_order_wo_rel: "Card_order r \ wo_rel r" +unfolding wo_rel_def card_order_on_def by blast + +lemma Cinfinite_limit: "\x \ Field r; Cinfinite r\ \ + \y \ Field r. x \ y \ (x, y) \ r" +unfolding cinfinite_def by (auto simp add: infinite_Card_order_limit) + +lemma Card_order_trans: + "\Card_order r; x \ y; (x, y) \ r; y \ z; (y, z) \ r\ \ x \ z \ (x, z) \ r" +unfolding card_order_on_def well_order_on_def linear_order_on_def + partial_order_on_def preorder_on_def trans_def antisym_def by blast + +lemma Cinfinite_limit2: + assumes x1: "x1 \ Field r" and x2: "x2 \ Field r" and r: "Cinfinite r" + shows "\y \ Field r. (x1 \ y \ (x1, y) \ r) \ (x2 \ y \ (x2, y) \ r)" +proof - + from r have trans: "trans r" and total: "Total r" and antisym: "antisym r" + unfolding card_order_on_def well_order_on_def linear_order_on_def + partial_order_on_def preorder_on_def by auto + obtain y1 where y1: "y1 \ Field r" "x1 \ y1" "(x1, y1) \ r" + using Cinfinite_limit[OF x1 r] by blast + obtain y2 where y2: "y2 \ Field r" "x2 \ y2" "(x2, y2) \ r" + using Cinfinite_limit[OF x2 r] by blast + show ?thesis + proof (cases "y1 = y2") + case True with y1 y2 show ?thesis by blast + next + case False + with y1(1) y2(1) total have "(y1, y2) \ r \ (y2, y1) \ r" + unfolding total_on_def by auto + thus ?thesis + proof + assume *: "(y1, y2) \ r" + with trans y1(3) have "(x1, y2) \ r" unfolding trans_def by blast + with False y1 y2 * antisym show ?thesis by (cases "x1 = y2") (auto simp: antisym_def) + next + assume *: "(y2, y1) \ r" + with trans y2(3) have "(x2, y1) \ r" unfolding trans_def by blast + with False y1 y2 * antisym show ?thesis by (cases "x2 = y1") (auto simp: antisym_def) + qed + qed +qed + +lemma Cinfinite_limit_finite: "\finite X; X \ Field r; Cinfinite r\ + \ \y \ Field r. \x \ X. (x \ y \ (x, y) \ r)" +proof (induct X rule: finite_induct) + case empty thus ?case unfolding cinfinite_def using ex_in_conv[of "Field r"] finite.emptyI by auto +next + case (insert x X) + then obtain y where y: "y \ Field r" "\x \ X. (x \ y \ (x, y) \ r)" by blast + then obtain z where z: "z \ Field r" "x \ z \ (x, z) \ r" "y \ z \ (y, z) \ r" + using Cinfinite_limit2[OF _ y(1) insert(5), of x] insert(4) by blast + show ?case by (metis Card_order_trans insert(5) insertE y(2) z) +qed + +lemma insert_subsetI: "\x \ A; X \ A\ \ insert x X \ A" +by auto + +(*helps resolution*) +lemma well_order_induct_imp: + "wo_rel r \ (\x. \y. y \ x \ (y, x) \ r \ y \ Field r \ P y \ x \ Field r \ P x) \ + x \ Field r \ P x" +by (erule wo_rel.well_order_induct) + +lemma meta_spec2: + assumes "(\x y. PROP P x y)" + shows "PROP P x y" +by (rule `(\x y. PROP P x y)`) + +(*Extended Sublist*) + +definition prefCl where + "prefCl Kl = (\ kl1 kl2. kl1 \ kl2 \ kl2 \ Kl \ kl1 \ Kl)" +definition PrefCl where + "PrefCl A n = (\kl kl'. kl \ A n \ kl' \ kl \ (\m\n. kl' \ A m))" + +lemma prefCl_UN: + "\\n. PrefCl A n\ \ prefCl (\n. A n)" +unfolding prefCl_def PrefCl_def by fastforce + +definition Succ where "Succ Kl kl = {k . kl @ [k] \ Kl}" +definition Shift where "Shift Kl k = {kl. k # kl \ Kl}" +definition shift where "shift lab k = (\kl. lab (k # kl))" + +lemmas sh_def = Shift_def shift_def + +lemma empty_Shift: "\[] \ Kl; k \ Succ Kl []\ \ [] \ Shift Kl k" +unfolding Shift_def Succ_def by simp + +lemma Shift_clists: "Kl \ Field (clists r) \ Shift Kl k \ Field (clists r)" +unfolding Shift_def clists_def Field_card_of by auto + +lemma Shift_prefCl: "prefCl Kl \ prefCl (Shift Kl k)" +unfolding prefCl_def Shift_def +proof safe + fix kl1 kl2 + assume "\kl1 kl2. kl1 \ kl2 \ kl2 \ Kl \ kl1 \ Kl" + "kl1 \ kl2" "k # kl2 \ Kl" + thus "k # kl1 \ Kl" using Cons_prefix_Cons[of k kl1 k kl2] by blast +qed + +lemma not_in_Shift: "kl \ Shift Kl x \ x # kl \ Kl" +unfolding Shift_def by simp + +lemma prefCl_Succ: "\prefCl Kl; k # kl \ Kl\ \ k \ Succ Kl []" +unfolding Succ_def proof + assume "prefCl Kl" "k # kl \ Kl" + moreover have "k # [] \ k # kl" by auto + ultimately have "k # [] \ Kl" unfolding prefCl_def by blast + thus "[] @ [k] \ Kl" by simp +qed + +lemma SuccD: "k \ Succ Kl kl \ kl @ [k] \ Kl" +unfolding Succ_def by simp + +lemmas SuccE = SuccD[elim_format] + +lemma SuccI: "kl @ [k] \ Kl \ k \ Succ Kl kl" +unfolding Succ_def by simp + +lemma ShiftD: "kl \ Shift Kl k \ k # kl \ Kl" +unfolding Shift_def by simp + +lemma Succ_Shift: "Succ (Shift Kl k) kl = Succ Kl (k # kl)" +unfolding Succ_def Shift_def by auto + +lemma ShiftI: "k # kl \ Kl \ kl \ Shift Kl k" +unfolding Shift_def by simp + +lemma Func_cexp: "|Func A B| =o |B| ^c |A|" +unfolding cexp_def Field_card_of by (simp only: card_of_refl) + +lemma clists_bound: "A \ Field (cpow (clists r)) - {{}} \ |A| \o clists r" +unfolding cpow_def clists_def Field_card_of by (auto simp: card_of_mono1) + +lemma cpow_clists_czero: "\A \ Field (cpow (clists r)) - {{}}; |A| =o czero\ \ False" +unfolding cpow_def clists_def +by (auto simp add: card_of_ordIso_czero_iff_empty[symmetric]) + (erule notE, erule ordIso_transitive, rule czero_ordIso) + +lemma incl_UNION_I: +assumes "i \ I" and "A \ F i" +shows "A \ UNION I F" +using assms by auto + +lemma Nil_clists: "{[]} \ Field (clists r)" +unfolding clists_def Field_card_of by auto + +lemma Cons_clists: + "\x \ Field r; xs \ Field (clists r)\ \ x # xs \ Field (clists r)" +unfolding clists_def Field_card_of by auto + +lemma length_Cons: "length (x#xs) = Suc (length xs)" +by simp + +lemma length_append_singleton: "length (xs @ [x]) = Suc (length xs)" +by simp + +(*injection into the field of a cardinal*) +definition "toCard_pred A r f \ inj_on f A \ f ` A \ Field r \ Card_order r" +definition "toCard A r \ SOME f. toCard_pred A r f" + +lemma ex_toCard_pred: +"\|A| \o r; Card_order r\ \ \ f. toCard_pred A r f" +unfolding toCard_pred_def +using card_of_ordLeq[of A "Field r"] + ordLeq_ordIso_trans[OF _ card_of_unique[of "Field r" r], of "|A|"] +by blast + +lemma toCard_pred_toCard: + "\|A| \o r; Card_order r\ \ toCard_pred A r (toCard A r)" +unfolding toCard_def using someI_ex[OF ex_toCard_pred] . + +lemma toCard_inj: "\|A| \o r; Card_order r; x \ A; y \ A\ \ + toCard A r x = toCard A r y \ x = y" +using toCard_pred_toCard unfolding inj_on_def toCard_pred_def by blast + +lemma toCard: "\|A| \o r; Card_order r; b \ A\ \ toCard A r b \ Field r" +using toCard_pred_toCard unfolding toCard_pred_def by blast + +definition "fromCard A r k \ SOME b. b \ A \ toCard A r b = k" + +lemma fromCard_toCard: +"\|A| \o r; Card_order r; b \ A\ \ fromCard A r (toCard A r b) = b" +unfolding fromCard_def by (rule some_equality) (auto simp add: toCard_inj) + +(* pick according to the weak pullback *) +definition pickWP_pred where +"pickWP_pred A p1 p2 b1 b2 a \ + a \ A \ p1 a = b1 \ p2 a = b2" + +definition pickWP where +"pickWP A p1 p2 b1 b2 \ + SOME a. pickWP_pred A p1 p2 b1 b2 a" + +lemma pickWP_pred: +assumes "wpull A B1 B2 f1 f2 p1 p2" and +"b1 \ B1" and "b2 \ B2" and "f1 b1 = f2 b2" +shows "\ a. pickWP_pred A p1 p2 b1 b2 a" +using assms unfolding wpull_def pickWP_pred_def by blast + +lemma pickWP_pred_pickWP: +assumes "wpull A B1 B2 f1 f2 p1 p2" and +"b1 \ B1" and "b2 \ B2" and "f1 b1 = f2 b2" +shows "pickWP_pred A p1 p2 b1 b2 (pickWP A p1 p2 b1 b2)" +unfolding pickWP_def using assms by(rule someI_ex[OF pickWP_pred]) + +lemma pickWP: +assumes "wpull A B1 B2 f1 f2 p1 p2" and +"b1 \ B1" and "b2 \ B2" and "f1 b1 = f2 b2" +shows "pickWP A p1 p2 b1 b2 \ A" + "p1 (pickWP A p1 p2 b1 b2) = b1" + "p2 (pickWP A p1 p2 b1 b2) = b2" +using assms pickWP_pred_pickWP unfolding pickWP_pred_def by fastforce+ + +lemma ssubst_mem: "\t = s; s \ X\ \ t \ X" by simp + +lemma Inl_Field_csum: "a \ Field r \ Inl a \ Field (r +c s)" +unfolding Field_card_of csum_def by auto + +lemma Inr_Field_csum: "a \ Field s \ Inr a \ Field (r +c s)" +unfolding Field_card_of csum_def by auto + +lemma nat_rec_0: "f = nat_rec f1 (%n rec. f2 n rec) \ f 0 = f1" +by auto + +lemma nat_rec_Suc: "f = nat_rec f1 (%n rec. f2 n rec) \ f (Suc n) = f2 n (f n)" +by auto + +lemma list_rec_Nil: "f = list_rec f1 (%x xs rec. f2 x xs rec) \ f [] = f1" +by auto + +lemma list_rec_Cons: "f = list_rec f1 (%x xs rec. f2 x xs rec) \ f (x # xs) = f2 x xs (f xs)" +by auto + +lemma sum_case_cong: "p = q \ sum_case f g p = sum_case f g q" +by simp + +lemma sum_case_step: + "sum_case (sum_case f' g') g (Inl p) = sum_case f' g' p" + "sum_case f (sum_case f' g') (Inr p) = sum_case f' g' p" +by auto + +lemma one_pointE: "\\x. s = x \ P\ \ P" +by simp + +lemma obj_one_pointE: "\x. s = x \ P \ P" +by blast + +lemma obj_sumE_f: +"\\x. s = f (Inl x) \ P; \x. s = f (Inr x) \ P\ \ \x. s = f x \ P" +by (metis sum.exhaust) + +lemma obj_sumE: "\\x. s = Inl x \ P; \x. s = Inr x \ P\ \ P" +by (cases s) auto + +lemma obj_sum_step: + "\\x. s = f (Inr (Inl x)) \ P; \x. s = f (Inr (Inr x)) \ P\ \ \x. s = f (Inr x) \ P" +by (metis obj_sumE) + +lemma sum_case_if: +"sum_case f g (if p then Inl x else Inr y) = (if p then f x else g y)" +by simp + +lemma not_arg_cong_Inr: "x \ y \ Inr x \ Inr y" +by simp + +ML_file "Tools/bnf_util.ML" +ML_file "Tools/bnf_tactics.ML" + +end diff -r 64bed36cd8da -r 66058a677ddd src/HOL/Codatatype/BNF_Wrap.thy --- a/src/HOL/Codatatype/BNF_Wrap.thy Tue Sep 11 19:43:06 2012 +0200 +++ b/src/HOL/Codatatype/BNF_Wrap.thy Tue Sep 11 19:45:12 2012 +0200 @@ -8,9 +8,10 @@ header {* Wrapping Datatypes *} theory BNF_Wrap -imports BNF_Def +imports BNF_Util keywords - "wrap_data" :: thy_goal + "wrap_data" :: thy_goal and + "no_dests" uses "Tools/bnf_wrap_tactics.ML" "Tools/bnf_wrap.ML" diff -r 64bed36cd8da -r 66058a677ddd src/HOL/Codatatype/Codatatype.thy --- a/src/HOL/Codatatype/Codatatype.thy Tue Sep 11 19:43:06 2012 +0200 +++ b/src/HOL/Codatatype/Codatatype.thy Tue Sep 11 19:45:12 2012 +0200 @@ -10,11 +10,11 @@ header {* The (Co)datatype Package *} theory Codatatype -imports BNF_Wrap BNF_LFP BNF_GFP +imports BNF_LFP BNF_GFP BNF_Wrap keywords - "data" :: thy_decl -and - "codata" :: thy_decl + "data" :: thy_decl and + "codata" :: thy_decl and + "defaults" uses "Tools/bnf_fp_sugar_tactics.ML" "Tools/bnf_fp_sugar.ML" diff -r 64bed36cd8da -r 66058a677ddd src/HOL/Codatatype/Tools/bnf_comp_tactics.ML --- a/src/HOL/Codatatype/Tools/bnf_comp_tactics.ML Tue Sep 11 19:43:06 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_comp_tactics.ML Tue Sep 11 19:45:12 2012 +0200 @@ -33,6 +33,9 @@ val mk_permute_in_alt_tac: ''a list -> ''a list -> tactic val mk_permute_in_bd_tac: ''a list -> ''a list -> thm -> thm -> thm -> tactic + + val mk_map_wpull_tac: thm -> thm list -> thm -> tactic + val mk_simple_wit_tac: thm list -> tactic end; structure BNF_Comp_Tactics : BNF_COMP_TACTICS = @@ -391,4 +394,11 @@ TRY o rtac @{thm csum_Cnotzero2} THEN' rtac @{thm ctwo_Cnotzero}) 1; +fun mk_map_wpull_tac comp_in_alt inner_map_wpulls outer_map_wpull = + (rtac (@{thm wpull_cong} OF (replicate 3 comp_in_alt)) THEN' rtac outer_map_wpull) 1 THEN + WRAP (fn thm => rtac thm 1 THEN REPEAT_DETERM (atac 1)) (K all_tac) inner_map_wpulls all_tac THEN + TRY (REPEAT_DETERM (atac 1 ORELSE rtac @{thm wpull_id} 1)); + +fun mk_simple_wit_tac wit_thms = ALLGOALS (atac ORELSE' eresolve_tac (@{thm emptyE} :: wit_thms)); + end; diff -r 64bed36cd8da -r 66058a677ddd src/HOL/Codatatype/Tools/bnf_def.ML --- a/src/HOL/Codatatype/Tools/bnf_def.ML Tue Sep 11 19:43:06 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_def.ML Tue Sep 11 19:45:12 2012 +0200 @@ -98,7 +98,7 @@ struct open BNF_Util -open BNF_Tactics +open BNF_Def_Tactics type axioms = { map_id: thm, @@ -1182,8 +1182,7 @@ map2 (Thm.close_derivation oo Skip_Proof.prove lthy [] []) goals (map (unfold_defs_tac lthy defs) tacs) |> (fn thms => after_qed (map single thms @ wit_thms) lthy) - end) oo prepare_def const_policy fact_policy qualify - (singleton o Type_Infer_Context.infer_types) Ds; + end) oo prepare_def const_policy fact_policy qualify (K I) Ds; val bnf_def_cmd = (fn (goals, wit_goals, after_qed, lthy, defs) => Proof.unfolding ([[(defs, [])]]) @@ -1222,8 +1221,8 @@ val _ = Outer_Syntax.local_theory_to_proof @{command_spec "bnf_def"} "define a BNF for an existing type" - (((Parse.binding --| Parse.$$$ "=") -- Parse.term -- - (Parse.$$$ "[" |-- Parse.list Parse.term --| Parse.$$$ "]") -- Parse.term -- - (Parse.$$$ "[" |-- Parse.list Parse.term --| Parse.$$$ "]")) >> bnf_def_cmd); + (((Parse.binding --| @{keyword "="}) -- Parse.term -- + (@{keyword "["} |-- Parse.list Parse.term --| @{keyword "]"}) -- Parse.term -- + (@{keyword "["} |-- Parse.list Parse.term --| @{keyword "]"})) >> bnf_def_cmd); end; diff -r 64bed36cd8da -r 66058a677ddd src/HOL/Codatatype/Tools/bnf_def_tactics.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Codatatype/Tools/bnf_def_tactics.ML Tue Sep 11 19:45:12 2012 +0200 @@ -0,0 +1,209 @@ +(* Title: HOL/Codatatype/Tools/bnf_def_tactics.ML + Author: Dmitriy Traytel, TU Muenchen + Author: Jasmin Blanchette, TU Muenchen + Copyright 2012 + +Tactics for definition of bounded natural functors. +*) + +signature BNF_DEF_TACTICS = +sig + val mk_collect_set_natural_tac: Proof.context -> thm list -> tactic + val mk_id': thm -> thm + val mk_comp': thm -> thm + val mk_in_mono_tac: int -> tactic + val mk_map_wppull_tac: thm -> thm -> thm -> thm -> thm list -> tactic + val mk_set_natural': thm -> thm + + val mk_rel_Gr_tac: thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm list -> + {prems: thm list, context: Proof.context} -> tactic + val mk_rel_Id_tac: int -> thm -> thm -> {prems: 'a, context: Proof.context} -> tactic + val mk_rel_O_tac: thm -> thm -> thm -> thm -> thm -> thm list -> + {prems: thm list, context: Proof.context} -> tactic + val mk_in_rel_tac: thm -> int -> {prems: 'b, context: Proof.context} -> tactic + val mk_rel_converse_tac: thm -> tactic + val mk_rel_converse_le_tac: thm -> thm -> thm -> thm -> thm list -> + {prems: thm list, context: Proof.context} -> tactic + val mk_rel_mono_tac: thm -> thm -> {prems: 'a, context: Proof.context} -> tactic +end; + +structure BNF_Def_Tactics : BNF_DEF_TACTICS = +struct + +open BNF_Util +open BNF_Tactics + +val set_mp = @{thm set_mp}; + +fun mk_id' id = mk_trans (fun_cong OF [id]) @{thm id_apply}; +fun mk_comp' comp = @{thm o_eq_dest_lhs} OF [mk_sym comp]; +fun mk_set_natural' set_natural = set_natural RS @{thm pointfreeE}; +fun mk_in_mono_tac n = if n = 0 then rtac @{thm subset_UNIV} 1 + else (rtac subsetI THEN' + rtac CollectI) 1 THEN + REPEAT_DETERM (eresolve_tac [CollectE, conjE] 1) THEN + REPEAT_DETERM_N (n - 1) + ((rtac conjI THEN' etac subset_trans THEN' atac) 1) THEN + (etac subset_trans THEN' atac) 1; + +fun mk_collect_set_natural_tac ctxt set_naturals = + substs_tac ctxt (@{thms collect_o image_insert image_empty} @ set_naturals) 1 THEN rtac refl 1; + +fun mk_map_wppull_tac map_id map_cong map_wpull map_comp set_naturals = + if null set_naturals then + EVERY' [rtac @{thm wppull_id}, rtac map_wpull, rtac map_id, rtac map_id] 1 + else EVERY' [REPEAT_DETERM o etac conjE, REPEAT_DETERM o dtac @{thm wppull_thePull}, + REPEAT_DETERM o etac exE, rtac @{thm wpull_wppull}, rtac map_wpull, + REPEAT_DETERM o rtac @{thm wpull_thePull}, rtac ballI, + REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac conjI, rtac CollectI, + CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}), + rtac @{thm image_subsetI}, rtac conjunct1, etac bspec, etac set_mp, atac]) + set_naturals, + CONJ_WRAP' (fn thm => EVERY' [rtac (map_comp RS trans), rtac (map_comp RS trans), + rtac (map_comp RS trans RS sym), rtac map_cong, + REPEAT_DETERM_N (length set_naturals) o EVERY' [rtac (o_apply RS trans), + rtac (o_apply RS trans RS sym), rtac (o_apply RS trans), rtac thm, + rtac conjunct2, etac bspec, etac set_mp, atac]]) [conjunct1, conjunct2]] 1; + +fun mk_rel_Gr_tac rel_def map_id map_cong map_wpull in_cong map_id' map_comp set_naturals + {context = ctxt, prems = _} = + let + val n = length set_naturals; + in + if null set_naturals then + Local_Defs.unfold_tac ctxt [rel_def] THEN EVERY' [rtac @{thm Gr_UNIV_id}, rtac map_id] 1 + else Local_Defs.unfold_tac ctxt [rel_def, @{thm Gr_def}] THEN + EVERY' [rtac equalityI, rtac subsetI, + REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}], + REPEAT_DETERM o dtac @{thm Pair_eq[THEN subst, of "%x. x"]}, + REPEAT_DETERM o etac conjE, hyp_subst_tac, + rtac CollectI, rtac exI, rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl, + rtac sym, rtac trans, rtac map_comp, rtac map_cong, + REPEAT_DETERM_N n o EVERY' [dtac @{thm set_rev_mp}, atac, + REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac, + rtac (o_apply RS trans), rtac (@{thm fst_conv} RS arg_cong RS trans), + rtac (@{thm snd_conv} RS sym)], + rtac CollectI, + CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}), + rtac @{thm image_subsetI}, dtac @{thm set_rev_mp}, atac, + REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac, + stac @{thm fst_conv}, atac]) set_naturals, + rtac @{thm subrelI}, etac CollectE, REPEAT_DETERM o eresolve_tac [exE, conjE], + REPEAT_DETERM o dtac @{thm Pair_eq[THEN subst, of "%x. x"]}, + REPEAT_DETERM o etac conjE, hyp_subst_tac, + rtac allE, rtac subst, rtac @{thm wpull_def}, rtac map_wpull, + REPEAT_DETERM_N n o rtac @{thm wpull_Gr}, etac allE, etac impE, rtac conjI, atac, + rtac conjI, REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac CollectI, + CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}), + rtac @{thm image_mono}, atac]) set_naturals, + rtac sym, rtac map_id', REPEAT_DETERM o eresolve_tac [bexE, conjE], + rtac @{thm relcompI}, rtac @{thm converseI}, + REPEAT_DETERM_N 2 o EVERY' [rtac CollectI, rtac exI, + rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl, etac sym, + etac @{thm set_rev_mp}, rtac equalityD1, rtac in_cong, + REPEAT_DETERM_N n o rtac @{thm Gr_def}]] 1 + end; + +fun mk_rel_Id_tac n rel_Gr map_id {context = ctxt, prems = _} = + Local_Defs.unfold_tac ctxt [rel_Gr, @{thm Id_alt}] THEN + subst_tac ctxt [map_id] 1 THEN + (if n = 0 then rtac refl 1 + else EVERY' [rtac @{thm arg_cong2[of _ _ _ _ Gr]}, + rtac equalityI, rtac @{thm subset_UNIV}, rtac subsetI, rtac CollectI, + CONJ_WRAP' (K (rtac @{thm subset_UNIV})) (1 upto n), rtac refl] 1); + +fun mk_rel_mono_tac rel_def in_mono {context = ctxt, prems = _} = + Local_Defs.unfold_tac ctxt [rel_def] THEN + EVERY' [rtac @{thm relcomp_mono}, rtac @{thm iffD2[OF converse_mono]}, + rtac @{thm Gr_mono}, rtac in_mono, REPEAT_DETERM o atac, + rtac @{thm Gr_mono}, rtac in_mono, REPEAT_DETERM o atac] 1; + +fun mk_rel_converse_le_tac rel_def rel_Id map_cong map_comp set_naturals + {context = ctxt, prems = _} = + let + val n = length set_naturals; + in + if null set_naturals then + Local_Defs.unfold_tac ctxt [rel_Id] THEN rtac equalityD2 1 THEN rtac @{thm converse_Id} 1 + else Local_Defs.unfold_tac ctxt [rel_def, @{thm Gr_def}] THEN + EVERY' [rtac @{thm subrelI}, + REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}], + REPEAT_DETERM o dtac @{thm Pair_eq[THEN subst, of "%x. x"]}, + REPEAT_DETERM o etac conjE, hyp_subst_tac, rtac @{thm converseI}, + rtac @{thm relcompI}, rtac @{thm converseI}, + EVERY' (map (fn thm => EVERY' [rtac CollectI, rtac exI, + rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl, rtac trans, + rtac map_cong, REPEAT_DETERM_N n o rtac thm, + rtac (map_comp RS sym), rtac CollectI, + CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}), + etac @{thm flip_rel}]) set_naturals]) [@{thm snd_fst_flip}, @{thm fst_snd_flip}])] 1 + end; + +fun mk_rel_converse_tac le_converse = + EVERY' [rtac equalityI, rtac le_converse, rtac @{thm xt1(6)}, rtac @{thm converse_shift}, + rtac le_converse, REPEAT_DETERM o stac @{thm converse_converse}, rtac subset_refl] 1; + +fun mk_rel_O_tac rel_def rel_Id map_cong map_wppull map_comp set_naturals + {context = ctxt, prems = _} = + let + val n = length set_naturals; + fun in_tac nthO_in = rtac CollectI THEN' + CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}), + rtac @{thm image_subsetI}, rtac nthO_in, etac set_mp, atac]) set_naturals; + in + if null set_naturals then Local_Defs.unfold_tac ctxt [rel_Id] THEN rtac (@{thm Id_O_R} RS sym) 1 + else Local_Defs.unfold_tac ctxt [rel_def, @{thm Gr_def}] THEN + EVERY' [rtac equalityI, rtac @{thm subrelI}, + REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}], + REPEAT_DETERM o dtac @{thm Pair_eq[THEN subst, of "%x. x"]}, + REPEAT_DETERM o etac conjE, hyp_subst_tac, + rtac @{thm relcompI}, rtac @{thm relcompI}, rtac @{thm converseI}, + rtac CollectI, rtac exI, rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl, + rtac sym, rtac trans, rtac map_comp, rtac sym, rtac map_cong, + REPEAT_DETERM_N n o rtac @{thm fst_fstO}, + in_tac @{thm fstO_in}, + rtac CollectI, rtac exI, rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl, + rtac sym, rtac trans, rtac map_comp, rtac map_cong, + REPEAT_DETERM_N n o EVERY' [rtac trans, rtac o_apply, rtac ballE, rtac subst, + rtac @{thm csquare_def}, rtac @{thm csquare_fstO_sndO}, atac, etac notE, + etac set_mp, atac], + in_tac @{thm fstO_in}, + rtac @{thm relcompI}, rtac @{thm converseI}, + rtac CollectI, rtac exI, rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl, + rtac sym, rtac trans, rtac map_comp, rtac map_cong, + REPEAT_DETERM_N n o rtac o_apply, + in_tac @{thm sndO_in}, + rtac CollectI, rtac exI, rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl, + rtac sym, rtac trans, rtac map_comp, rtac sym, rtac map_cong, + REPEAT_DETERM_N n o rtac @{thm snd_sndO}, + in_tac @{thm sndO_in}, + rtac @{thm subrelI}, + REPEAT_DETERM o eresolve_tac [CollectE, @{thm relcompE}, @{thm converseE}], + REPEAT_DETERM o eresolve_tac [exE, conjE], + REPEAT_DETERM o dtac @{thm Pair_eq[THEN subst, of "%x. x"]}, + REPEAT_DETERM o etac conjE, hyp_subst_tac, + rtac allE, rtac subst, rtac @{thm wppull_def}, rtac map_wppull, + CONJ_WRAP' (K (rtac @{thm wppull_fstO_sndO})) set_naturals, + etac allE, etac impE, etac conjI, etac conjI, atac, + REPEAT_DETERM o eresolve_tac [bexE, conjE], + rtac @{thm relcompI}, rtac @{thm converseI}, + EVERY' (map (fn thm => EVERY' [rtac CollectI, rtac exI, + rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl, rtac sym, rtac trans, + rtac trans, rtac map_cong, REPEAT_DETERM_N n o rtac thm, + rtac (map_comp RS sym), atac, atac]) [@{thm fst_fstO}, @{thm snd_sndO}])] 1 + end; + +fun mk_in_rel_tac rel_def m {context = ctxt, prems = _} = + let + val ls' = replicate (Int.max (1, m)) (); + in + Local_Defs.unfold_tac ctxt (rel_def :: + @{thms Gr_def converse_unfold relcomp_unfold mem_Collect_eq prod.cases Pair_eq}) THEN + EVERY' [rtac iffI, REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac, rtac exI, + rtac conjI, CONJ_WRAP' (K atac) ls', rtac conjI, rtac refl, rtac refl, + REPEAT_DETERM o eresolve_tac [exE, conjE], rtac exI, rtac conjI, + REPEAT_DETERM_N 2 o EVERY' [rtac exI, rtac conjI, etac @{thm conjI[OF refl sym]}, + CONJ_WRAP' (K atac) ls']] 1 + end; + +end; diff -r 64bed36cd8da -r 66058a677ddd src/HOL/Codatatype/Tools/bnf_fp_sugar.ML --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Tue Sep 11 19:43:06 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Tue Sep 11 19:45:12 2012 +0200 @@ -48,6 +48,8 @@ val lists_bmoc = fold (fn xs => fn t => Term.list_comb (t, xs)) +fun mk_predT T = T --> HOLogic.boolT; + fun mk_id T = Const (@{const_name id}, T --> T); fun mk_tupled_fun x f xs = HOLogic.tupled_lambda x (Term.list_comb (f, xs)); @@ -58,10 +60,9 @@ fun tick v f = Term.lambda v (HOLogic.mk_prod (v, f $ v)); fun tack z_name (c, v) f = - let - val T = fastype_of v; - val z = Free (z_name, mk_sumT (T, fastype_of c)) - in Term.lambda z (mk_sum_case (mk_id T, Term.lambda c (f $ c)) $ z) end; + let val z = Free (z_name, mk_sumT (fastype_of v, fastype_of c)) in + Term.lambda z (mk_sum_case (Term.lambda v v, Term.lambda c (f $ c)) $ z) + end; fun cannot_merge_types () = error "Mutually recursive types must have the same type parameters"; @@ -89,13 +90,17 @@ fun mixfix_of ((_, mx), _) = mx; fun ctr_specs_of (_, ctr_specs) = ctr_specs; -fun disc_of (((disc, _), _), _) = disc; -fun ctr_of (((_, ctr), _), _) = ctr; -fun args_of ((_, args), _) = args; +fun disc_of ((((disc, _), _), _), _) = disc; +fun ctr_of ((((_, ctr), _), _), _) = ctr; +fun args_of (((_, args), _), _) = args; +fun defaults_of ((_, ds), _) = ds; fun ctr_mixfix_of (_, mx) = mx; -fun prepare_datatype prepare_typ lfp specs fake_lthy no_defs_lthy = +fun prepare_datatype prepare_typ prepare_term lfp (no_dests, specs) fake_lthy no_defs_lthy = let + val _ = if not lfp andalso no_dests then error "Cannot define destructor-less codatatypes" + else (); + val constrained_As = map (map (apfst (prepare_typ fake_lthy)) o type_args_constrained_of) specs |> Library.foldr1 (merge_type_args_constrained no_defs_lthy); @@ -132,6 +137,8 @@ val sel_bindersss = map (map (map fst)) ctr_argsss; val fake_ctr_Tsss = map (map (map (prepare_typ fake_lthy o snd))) ctr_argsss; + val raw_sel_defaultsss = map (map defaults_of) ctr_specss; + val rhs_As' = fold (fold (fold Term.add_tfreesT)) fake_ctr_Tsss []; val _ = (case subtract (op =) As' rhs_As' of [] => () @@ -211,12 +218,8 @@ val fp_iter_fun_Ts = fst (split_last (binder_types (fastype_of fp_iter1))); val fp_rec_fun_Ts = fst (split_last (binder_types (fastype_of fp_rec1))); - fun dest_rec_pair (T as Type (@{type_name prod}, Us as [_, U])) = - if member (op =) Cs U then Us else [T] - | dest_rec_pair T = [T]; - val ((iter_only as (gss, _, _), rec_only as (hss, _, _)), - (zs, cs, cpss, coiter_only as ((pgss, cgsss), _), corec_only as ((phss, chsss), _))) = + (zs, cs, cpss, coiter_only as ((pgss, crgsss), _), corec_only as ((phss, cshsss), _))) = if lfp then let val y_Tsss = @@ -228,18 +231,25 @@ lthy |> mk_Freess "f" g_Tss ||>> mk_Freesss "x" y_Tsss; + val yssss = map (map (map single)) ysss; + + fun dest_rec_prodT (T as Type (@{type_name prod}, Us as [_, U])) = + if member (op =) Cs U then Us else [T] + | dest_rec_prodT T = [T]; val z_Tssss = - map3 (fn n => fn ms => map2 (map dest_rec_pair oo dest_tupleT) ms o + map3 (fn n => fn ms => map2 (map dest_rec_prodT oo dest_tupleT) ms o dest_sumTN_balanced n o domain_type) ns mss fp_rec_fun_Ts; val h_Tss = map2 (map2 (fold_rev (curry (op --->)))) z_Tssss Css; val hss = map2 (map2 retype_free) gss h_Tss; - val (zssss, _) = + val zssss_hd = map2 (map2 (map2 (fn y => fn T :: _ => retype_free y T))) ysss z_Tssss; + val (zssss_tl, _) = lthy - |> mk_Freessss "x" z_Tssss; + |> mk_Freessss "y" (map (map (map tl)) z_Tssss); + val zssss = map2 (map2 (map2 cons)) zssss_hd zssss_tl; in - (((gss, g_Tss, map (map (map single)) ysss), (hss, h_Tss, zssss)), + (((gss, g_Tss, yssss), (hss, h_Tss, zssss)), ([], [], [], (([], []), ([], [])), (([], []), ([], [])))) end else @@ -247,49 +257,71 @@ (*avoid "'a itself" arguments in coiterators and corecursors*) val mss' = map (fn [0] => [1] | ms => ms) mss; - val p_Tss = - map2 (fn C => fn n => replicate (Int.max (0, n - 1)) (C --> HOLogic.boolT)) Cs ns; + val p_Tss = map2 (fn n => replicate (Int.max (0, n - 1)) o mk_predT) ns Cs; + + fun zip_predss_getterss qss fss = maps (op @) (qss ~~ fss); - fun zip_preds_getters [] [fs] = fs - | zip_preds_getters (p :: ps) (fs :: fss) = p :: fs @ zip_preds_getters ps fss; + fun zip_preds_predsss_gettersss [] [qss] [fss] = zip_predss_getterss qss fss + | zip_preds_predsss_gettersss (p :: ps) (qss :: qsss) (fss :: fsss) = + p :: zip_predss_getterss qss fss @ zip_preds_predsss_gettersss ps qsss fsss; - fun mk_types fun_Ts = + fun mk_types maybe_dest_sumT fun_Ts = let val f_sum_prod_Ts = map range_type fun_Ts; val f_prod_Tss = map2 dest_sumTN_balanced ns f_sum_prod_Ts; - val f_Tsss = - map3 (fn C => map2 (map (curry (op -->) C) oo dest_tupleT)) Cs mss' f_prod_Tss; - val pf_Tss = map2 zip_preds_getters p_Tss f_Tsss - in (f_sum_prod_Ts, f_Tsss, pf_Tss) end; + val f_Tssss = + map3 (fn C => map2 (map (map (curry (op -->) C) o maybe_dest_sumT) oo dest_tupleT)) + Cs mss' f_prod_Tss; + val q_Tssss = + map (map (map (fn [_] => [] | [_, C] => [mk_predT (domain_type C)]))) f_Tssss; + val pf_Tss = map3 zip_preds_predsss_gettersss p_Tss q_Tssss f_Tssss; + in (q_Tssss, f_sum_prod_Ts, f_Tssss, pf_Tss) end; - val (g_sum_prod_Ts, g_Tsss, pg_Tss) = mk_types fp_iter_fun_Ts; - val (h_sum_prod_Ts, h_Tsss, ph_Tss) = mk_types fp_rec_fun_Ts; + val (r_Tssss, g_sum_prod_Ts, g_Tssss, pg_Tss) = mk_types single fp_iter_fun_Ts; - val ((((Free (z, _), cs), pss), gsss), _) = + val ((((Free (z, _), cs), pss), gssss), _) = lthy |> yield_singleton (mk_Frees "z") dummyT ||>> mk_Frees "a" Cs ||>> mk_Freess "p" p_Tss - ||>> mk_Freesss "g" g_Tsss; + ||>> mk_Freessss "g" g_Tssss; + val rssss = map (map (map (fn [] => []))) r_Tssss; + + fun dest_corec_sumT (T as Type (@{type_name sum}, Us as [_, U])) = + if member (op =) Cs U then Us else [T] + | dest_corec_sumT T = [T]; - val hsss = map2 (map2 (map2 retype_free)) gsss h_Tsss; + val (s_Tssss, h_sum_prod_Ts, h_Tssss, ph_Tss) = mk_types dest_corec_sumT fp_rec_fun_Ts; + + val hssss_hd = map2 (map2 (map2 (fn [g] => fn T :: _ => retype_free g T))) gssss h_Tssss; + val ((sssss, hssss_tl), _) = + lthy + |> mk_Freessss "q" s_Tssss + ||>> mk_Freessss "h" (map (map (map tl)) h_Tssss); + val hssss = map2 (map2 (map2 cons)) hssss_hd hssss_tl; val cpss = map2 (fn c => map (fn p => p $ c)) cs pss; - fun mk_terms fsss = + fun mk_preds_getters_join [] [cf] = cf + | mk_preds_getters_join [cq] [cf, cf'] = + mk_If cq (mk_Inl (fastype_of cf') cf) (mk_Inr (fastype_of cf) cf'); + + fun mk_terms qssss fssss = let - val pfss = map2 zip_preds_getters pss fsss; - val cfsss = map2 (fn c => map (map (fn f => f $ c))) cs fsss - in (pfss, cfsss) end; + val pfss = map3 zip_preds_predsss_gettersss pss qssss fssss; + val cqssss = map2 (fn c => map (map (map (fn f => f $ c)))) cs qssss; + val cfssss = map2 (fn c => map (map (map (fn f => f $ c)))) cs fssss; + val cqfsss = map2 (map2 (map2 mk_preds_getters_join)) cqssss cfssss; + in (pfss, cqfsss) end; in ((([], [], []), ([], [], [])), - ([z], cs, cpss, (mk_terms gsss, (g_sum_prod_Ts, pg_Tss)), - (mk_terms hsss, (h_sum_prod_Ts, ph_Tss)))) + ([z], cs, cpss, (mk_terms rssss gssss, (g_sum_prod_Ts, pg_Tss)), + (mk_terms sssss hssss, (h_sum_prod_Ts, ph_Tss)))) end; - fun pour_some_sugar_on_type (((((((((((((((((b, fpT), C), fld), unf), fp_iter), fp_rec), + fun define_ctrs_case_for_type ((((((((((((((((((b, fpT), C), fld), unf), fp_iter), fp_rec), fld_unf), unf_fld), fld_inject), n), ks), ms), ctr_binders), ctr_mixfixes), ctr_Tss), - disc_binders), sel_binderss) no_defs_lthy = + disc_binders), sel_binderss), raw_sel_defaultss) no_defs_lthy = let val unfT = domain_type (fastype_of fld); val ctr_prod_Ts = map HOLogic.mk_tupleT ctr_Tss; @@ -368,7 +400,7 @@ val tacss = [exhaust_tac] :: inject_tacss @ half_distinct_tacss @ [case_tacs]; - fun some_lfp_sugar ((selss0, discIs, sel_thmss), no_defs_lthy) = + fun define_iter_rec ((selss0, discIs, sel_thmss), no_defs_lthy) = let val fpT_to_C = fpT --> C; @@ -384,11 +416,11 @@ map2 (mk_sum_caseN_balanced oo map2 mk_uncurried2_fun) fss xssss)); in (binder, spec) end; - val iter_likes = + val iter_like_bundles = [(iterN, fp_iter, iter_only), (recN, fp_rec, rec_only)]; - val (binders, specs) = map generate_iter_like iter_likes |> split_list; + val (binders, specs) = map generate_iter_like iter_like_bundles |> split_list; val ((csts, defs), (lthy', lthy)) = no_defs_lthy |> apfst split_list o fold_map2 (fn b => fn spec => @@ -407,31 +439,32 @@ lthy) end; - fun some_gfp_sugar ((selss0, discIs, sel_thmss), no_defs_lthy) = + fun define_coiter_corec ((selss0, discIs, sel_thmss), no_defs_lthy) = let val B_to_fpT = C --> fpT; - fun generate_coiter_like (suf, fp_iter_like, ((pfss, cfsss), (f_sum_prod_Ts, pf_Tss))) = + fun mk_preds_getterss_join c n cps sum_prod_T cqfss = + Term.lambda c (mk_IfN sum_prod_T cps + (map2 (mk_InN_balanced sum_prod_T n) (map HOLogic.mk_tuple cqfss) (1 upto n))); + + fun generate_coiter_like (suf, fp_iter_like, ((pfss, cqfsss), (f_sum_prod_Ts, + pf_Tss))) = let val res_T = fold_rev (curry (op --->)) pf_Tss B_to_fpT; val binder = Binding.suffix_name ("_" ^ suf) b; - fun mk_preds_getters_join c n cps sum_prod_T cfss = - Term.lambda c (mk_IfN sum_prod_T cps - (map2 (mk_InN_balanced sum_prod_T n) (map HOLogic.mk_tuple cfss) (1 upto n))); - val spec = mk_Trueprop_eq (lists_bmoc pfss (Free (Binding.name_of binder, res_T)), Term.list_comb (fp_iter_like, - map5 mk_preds_getters_join cs ns cpss f_sum_prod_Ts cfsss)); + map5 mk_preds_getterss_join cs ns cpss f_sum_prod_Ts cqfsss)); in (binder, spec) end; - val coiter_likes = + val coiter_like_bundles = [(coiterN, fp_iter, coiter_only), (corecN, fp_rec, corec_only)]; - val (binders, specs) = map generate_coiter_like coiter_likes |> split_list; + val (binders, specs) = map generate_coiter_like coiter_like_bundles |> split_list; val ((csts, defs), (lthy', lthy)) = no_defs_lthy |> apfst split_list o fold_map2 (fn b => fn spec => @@ -449,9 +482,16 @@ ((ctrs, selss0, coiter, corec, v, xss, ctr_defs, discIs, sel_thmss, coiter_def, corec_def), lthy) end; + + fun wrap lthy = + let val sel_defaultss = map (map (apsnd (prepare_term lthy))) raw_sel_defaultss in + wrap_datatype tacss (((no_dests, ctrs0), casex0), (disc_binders, (sel_binderss, + sel_defaultss))) lthy + end; + + val define_iter_likes = if lfp then define_iter_rec else define_coiter_corec; in - wrap_datatype tacss ((ctrs0, casex0), (disc_binders, sel_binderss)) lthy' - |> (if lfp then some_lfp_sugar else some_gfp_sugar) + ((wrap, define_iter_likes), lthy') end; val pre_map_defs = map map_def_of_bnf pre_bnfs; @@ -470,7 +510,7 @@ val args = map build_arg TUs; in Term.list_comb (mapx, args) end; - fun pour_more_sugar_on_lfps ((ctrss, _, iters, recs, vs, xsss, ctr_defss, _, _, iter_defs, + fun derive_iter_rec_thms_for_types ((ctrss, _, iters, recs, vs, xsss, ctr_defss, _, _, iter_defs, rec_defs), lthy) = let val xctrss = map2 (map2 (curry Term.list_comb)) ctrss xsss; @@ -491,14 +531,14 @@ ~1 => build_map (build_call fiter_likes maybe_tick) T U | j => maybe_tick (nth vs j) (nth fiter_likes j)); - fun mk_U maybe_prodT = - typ_subst (map2 (fn fpT => fn C => (fpT, maybe_prodT fpT C)) fpTs Cs); + fun mk_U maybe_mk_prodT = + typ_subst (map2 (fn fpT => fn C => (fpT, maybe_mk_prodT fpT C)) fpTs Cs); - fun repair_calls fiter_likes maybe_cons maybe_tick maybe_prodT (x as Free (_, T)) = + fun repair_calls fiter_likes maybe_cons maybe_tick maybe_mk_prodT (x as Free (_, T)) = if member (op =) fpTs T then maybe_cons x [build_call fiter_likes (K I) (T, mk_U (K I) T) $ x] else if exists_subtype (member (op =) fpTs) T then - [build_call fiter_likes maybe_tick (T, mk_U maybe_prodT T) $ x] + [build_call fiter_likes maybe_tick (T, mk_U maybe_mk_prodT T) $ x] else [x]; @@ -514,11 +554,9 @@ val rec_tacss = map2 (map o mk_iter_like_tac pre_map_defs map_ids rec_defs) fp_rec_thms ctr_defss; in - (map2 (map2 (fn goal => fn tac => - Skip_Proof.prove lthy [] [] goal (tac o #context) |> Thm.close_derivation)) + (map2 (map2 (fn goal => fn tac => Skip_Proof.prove lthy [] [] goal (tac o #context))) goal_iterss iter_tacss, - map2 (map2 (fn goal => fn tac => - Skip_Proof.prove lthy [] [] goal (tac o #context) |> Thm.close_derivation)) + map2 (map2 (fn goal => fn tac => Skip_Proof.prove lthy [] [] goal (tac o #context))) goal_recss rec_tacss) end; @@ -533,8 +571,8 @@ lthy |> Local_Theory.notes notes |> snd end; - fun pour_more_sugar_on_gfps ((ctrss, selsss, coiters, corecs, vs, _, ctr_defss, discIss, - sel_thmsss, coiter_defs, corec_defs), lthy) = + fun derive_coiter_corec_thms_for_types ((ctrss, selsss, coiters, corecs, vs, _, ctr_defss, + discIss, sel_thmsss, coiter_defs, corec_defs), lthy) = let val z = the_single zs; @@ -558,23 +596,24 @@ ~1 => build_map (build_call fiter_likes maybe_tack) T U | j => maybe_tack (nth cs j, nth vs j) (nth fiter_likes j)); - fun mk_U maybe_sumT = - typ_subst (map2 (fn C => fn fpT => (maybe_sumT fpT C, fpT)) Cs fpTs); + fun mk_U maybe_mk_sumT = + typ_subst (map2 (fn C => fn fpT => (maybe_mk_sumT fpT C, fpT)) Cs fpTs); - fun repair_calls fiter_likes maybe_sumT maybe_tack - (cf as Free (_, Type (_, [_, T])) $ _) = - if exists_subtype (member (op =) Cs) T then - build_call fiter_likes maybe_tack (T, mk_U maybe_sumT T) $ cf - else - cf; + fun repair_calls fiter_likes maybe_mk_sumT maybe_tack cqf = + let val T = fastype_of cqf in + if exists_subtype (member (op =) Cs) T then + build_call fiter_likes maybe_tack (T, mk_U maybe_mk_sumT T) $ cqf + else + cqf + end; - val cgsss' = map (map (map (repair_calls gcoiters (K I) (K I)))) cgsss; - val chsss' = map (map (map (repair_calls hcorecs (curry mk_sumT) (tack z)))) chsss; + val crgsss' = map (map (map (repair_calls gcoiters (K I) (K I)))) crgsss; + val cshsss' = map (map (map (repair_calls hcorecs (curry mk_sumT) (tack z)))) cshsss; val goal_coiterss = - map8 (map4 oooo mk_goal_coiter_like pgss) cs cpss gcoiters ns kss ctrss mss cgsss'; + map8 (map4 oooo mk_goal_coiter_like pgss) cs cpss gcoiters ns kss ctrss mss crgsss'; val goal_corecss = - map8 (map4 oooo mk_goal_coiter_like phss) cs cpss hcorecs ns kss ctrss mss chsss'; + map8 (map4 oooo mk_goal_coiter_like phss) cs cpss hcorecs ns kss ctrss mss cshsss'; val coiter_tacss = map3 (map oo mk_coiter_like_tac coiter_defs map_ids) fp_iter_thms pre_map_defs @@ -583,9 +622,12 @@ map3 (map oo mk_coiter_like_tac corec_defs map_ids) fp_rec_thms pre_map_defs ctr_defss; in - (map2 (map2 (fn goal => fn tac => Skip_Proof.prove lthy [] [] goal (tac o #context))) + (map2 (map2 (fn goal => fn tac => + Skip_Proof.prove lthy [] [] goal (tac o #context) |> Thm.close_derivation)) goal_coiterss coiter_tacss, - map2 (map2 (fn goal => fn tac => Skip_Proof.prove lthy [] [] goal (tac o #context))) + map2 (map2 (fn goal => fn tac => + Skip_Proof.prove lthy [] [] goal (tac o #context) + |> Local_Defs.unfold lthy @{thms sum_case_if} |> Thm.close_derivation)) goal_corecss corec_tacss) end; @@ -627,12 +669,15 @@ lthy |> Local_Theory.notes notes |> snd end; + fun wrap_types_and_define_iter_likes ((wraps, define_iter_likess), lthy) = + fold_map2 (curry (op o)) define_iter_likess wraps lthy |>> split_list11 + val lthy' = lthy - |> fold_map pour_some_sugar_on_type (bs ~~ fpTs ~~ Cs ~~ flds ~~ unfs ~~ fp_iters ~~ + |> fold_map define_ctrs_case_for_type (bs ~~ fpTs ~~ Cs ~~ flds ~~ unfs ~~ fp_iters ~~ fp_recs ~~ fld_unfs ~~ unf_flds ~~ fld_injects ~~ ns ~~ kss ~~ mss ~~ ctr_binderss ~~ - ctr_mixfixess ~~ ctr_Tsss ~~ disc_binderss ~~ sel_bindersss) - |>> split_list11 - |> (if lfp then pour_more_sugar_on_lfps else pour_more_sugar_on_gfps); + ctr_mixfixess ~~ ctr_Tsss ~~ disc_binderss ~~ sel_bindersss ~~ raw_sel_defaultsss) + |>> split_list |> wrap_types_and_define_iter_likes + |> (if lfp then derive_iter_rec_thms_for_types else derive_coiter_corec_thms_for_types); val timer = time (timer ("Constructors, discriminators, selectors, etc., for the new " ^ (if lfp then "" else "co") ^ "datatype")); @@ -640,7 +685,7 @@ (timer; lthy') end; -fun datatype_cmd info specs lthy = +fun datatype_cmd lfp (bundle as (_, specs)) lthy = let (* TODO: cleaner handling of fake contexts, without "background_theory" *) (*the "perhaps o try" below helps gracefully handles the case where the new type is defined in a @@ -650,26 +695,31 @@ (type_binder_of spec, length (type_args_constrained_of spec), mixfix_of spec)))) specs; val fake_lthy = Proof_Context.background_theory fake_thy lthy; in - prepare_datatype Syntax.read_typ info specs fake_lthy lthy + prepare_datatype Syntax.read_typ Syntax.read_term lfp bundle fake_lthy lthy end; -val parse_opt_binding_colon = Scan.optional (Parse.binding --| Parse.$$$ ":") no_binder +val parse_opt_binding_colon = Scan.optional (Parse.binding --| @{keyword ":"}) no_binder val parse_ctr_arg = - Parse.$$$ "(" |-- parse_opt_binding_colon -- Parse.typ --| Parse.$$$ ")" || + @{keyword "("} |-- parse_opt_binding_colon -- Parse.typ --| @{keyword ")"} || (Parse.typ >> pair no_binder); +val parse_defaults = + @{keyword "("} |-- @{keyword "defaults"} |-- Scan.repeat parse_bound_term --| @{keyword ")"}; + val parse_single_spec = Parse.type_args_constrained -- Parse.binding -- Parse.opt_mixfix -- (@{keyword "="} |-- Parse.enum1 "|" (parse_opt_binding_colon -- Parse.binding -- - Scan.repeat parse_ctr_arg -- Parse.opt_mixfix)); + Scan.repeat parse_ctr_arg -- Scan.optional parse_defaults [] -- Parse.opt_mixfix)); + +val parse_datatype = parse_wrap_options -- Parse.and_list1 parse_single_spec; val _ = Outer_Syntax.local_theory @{command_spec "data"} "define BNF-based inductive datatypes" - (Parse.and_list1 parse_single_spec >> datatype_cmd true); + (parse_datatype >> datatype_cmd true); val _ = Outer_Syntax.local_theory @{command_spec "codata"} "define BNF-based coinductive datatypes" - (Parse.and_list1 parse_single_spec >> datatype_cmd false); + (parse_datatype >> datatype_cmd false); end; diff -r 64bed36cd8da -r 66058a677ddd src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML diff -r 64bed36cd8da -r 66058a677ddd src/HOL/Codatatype/Tools/bnf_fp_util.ML --- a/src/HOL/Codatatype/Tools/bnf_fp_util.ML Tue Sep 11 19:43:06 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_fp_util.ML Tue Sep 11 19:45:12 2012 +0200 @@ -101,6 +101,7 @@ val dest_tupleT: int -> typ -> typ list val mk_Field: term -> term + val mk_If: term -> term -> term -> term val mk_union: term * term -> term val mk_sumEN: int -> thm @@ -258,6 +259,10 @@ val mk_sum_caseN = Library.foldr1 mk_sum_case; val mk_sum_caseN_balanced = Balanced_Tree.make mk_sum_case; +fun mk_If p t f = + let val T = fastype_of t; + in Const (@{const_name If}, HOLogic.boolT --> T --> T --> T) $ p $ t $ f end; + fun mk_Field r = let val T = fst (dest_relT (fastype_of r)); in Const (@{const_name Field}, mk_relT (T, T) --> HOLogic.mk_setT T) $ r end; diff -r 64bed36cd8da -r 66058a677ddd src/HOL/Codatatype/Tools/bnf_gfp.ML --- a/src/HOL/Codatatype/Tools/bnf_gfp.ML Tue Sep 11 19:43:06 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML Tue Sep 11 19:45:12 2012 +0200 @@ -3006,9 +3006,9 @@ end; val _ = - Outer_Syntax.local_theory @{command_spec "codata_raw"} "greatest fixed points for BNF equations" + Outer_Syntax.local_theory @{command_spec "codata_raw"} "greatest fixed points of BNF equations" (Parse.and_list1 - ((Parse.binding --| Parse.$$$ ":") -- (Parse.typ --| Parse.$$$ "=" -- Parse.typ)) >> + ((Parse.binding --| @{keyword ":"}) -- (Parse.typ --| @{keyword "="} -- Parse.typ)) >> (snd oo fp_bnf_cmd bnf_gfp o apsnd split_list o split_list)); end; diff -r 64bed36cd8da -r 66058a677ddd src/HOL/Codatatype/Tools/bnf_gfp_util.ML --- a/src/HOL/Codatatype/Tools/bnf_gfp_util.ML Tue Sep 11 19:43:06 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_gfp_util.ML Tue Sep 11 19:45:12 2012 +0200 @@ -12,7 +12,6 @@ val dest_listT: typ -> typ val mk_Cons: term -> term -> term - val mk_If: term -> term -> term -> term val mk_Shift: term -> term -> term val mk_Succ: term -> term -> term val mk_Times: term * term -> term @@ -122,10 +121,6 @@ fun mk_size t = HOLogic.size_const (fastype_of t) $ t; -fun mk_If p t f = - let val T = fastype_of t; - in Const (@{const_name If}, HOLogic.boolT --> T --> T --> T) $ p $ t $ f end; - fun mk_quotient A R = let val T = fastype_of A; in Const (@{const_name quotient}, T --> fastype_of R --> HOLogic.mk_setT T) $ A $ R end; diff -r 64bed36cd8da -r 66058a677ddd src/HOL/Codatatype/Tools/bnf_lfp.ML --- a/src/HOL/Codatatype/Tools/bnf_lfp.ML Tue Sep 11 19:43:06 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_lfp.ML Tue Sep 11 19:45:12 2012 +0200 @@ -1821,9 +1821,9 @@ end; val _ = - Outer_Syntax.local_theory @{command_spec "data_raw"} "least fixed points for BNF equations" + Outer_Syntax.local_theory @{command_spec "data_raw"} "least fixed points of BNF equations" (Parse.and_list1 - ((Parse.binding --| Parse.$$$ ":") -- (Parse.typ --| Parse.$$$ "=" -- Parse.typ)) >> + ((Parse.binding --| @{keyword ":"}) -- (Parse.typ --| @{keyword "="} -- Parse.typ)) >> (snd oo fp_bnf_cmd bnf_lfp o apsnd split_list o split_list)); end; diff -r 64bed36cd8da -r 66058a677ddd src/HOL/Codatatype/Tools/bnf_tactics.ML --- a/src/HOL/Codatatype/Tools/bnf_tactics.ML Tue Sep 11 19:43:06 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_tactics.ML Tue Sep 11 19:45:12 2012 +0200 @@ -23,30 +23,11 @@ val mk_Abs_bij_thm: Proof.context -> thm -> thm -> thm val mk_Abs_inj_thm: thm -> thm - val mk_Card_order_tac: thm -> tactic - val mk_collect_set_natural_tac: Proof.context -> thm list -> tactic - val mk_id': thm -> thm - val mk_comp': thm -> thm - val mk_in_mono_tac: int -> tactic + val mk_pred_unfold_tac: thm -> thm list -> thm -> {prems: 'a, context: Proof.context} -> tactic + val mk_map_comp_id_tac: thm -> tactic val mk_map_cong_tac: int -> thm -> {prems: 'a, context: Proof.context} -> tactic val mk_map_congL_tac: int -> thm -> thm -> tactic - val mk_map_wppull_tac: thm -> thm -> thm -> thm -> thm list -> tactic - val mk_map_wpull_tac: thm -> thm list -> thm -> tactic - val mk_set_natural': thm -> thm - val mk_simple_wit_tac: thm list -> tactic - - val mk_pred_unfold_tac: thm -> thm list -> thm -> {prems: 'a, context: Proof.context} -> tactic - val mk_rel_Gr_tac: thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm list -> - {prems: thm list, context: Proof.context} -> tactic - val mk_rel_Id_tac: int -> thm -> thm -> {prems: 'a, context: Proof.context} -> tactic - val mk_rel_O_tac: thm -> thm -> thm -> thm -> thm -> thm list -> - {prems: thm list, context: Proof.context} -> tactic - val mk_in_rel_tac: thm -> int -> {prems: 'b, context: Proof.context} -> tactic - val mk_rel_converse_tac: thm -> tactic - val mk_rel_converse_le_tac: thm -> thm -> thm -> thm -> thm list -> - {prems: thm list, context: Proof.context} -> tactic - val mk_rel_mono_tac: thm -> thm -> {prems: 'a, context: Proof.context} -> tactic end; structure BNF_Tactics : BNF_TACTICS = @@ -56,8 +37,6 @@ fun ss_only thms = Simplifier.clear_ss HOL_basic_ss addsimps thms; -val set_mp = @{thm set_mp}; - fun select_prem_tac n tac k = DETERM o (EVERY' [REPEAT_DETERM_N (k - 1) o etac thin_rl, tac, REPEAT_DETERM_N (n - k) o etac thin_rl]); @@ -108,206 +87,22 @@ gen_tac end; -fun mk_Card_order_tac card_order = - (rtac conjE THEN' - rtac @{thm card_order_on_Card_order} THEN' - rtac card_order THEN' - atac) 1; - -fun mk_id' id = mk_trans (fun_cong OF [id]) @{thm id_apply}; -fun mk_comp' comp = @{thm o_eq_dest_lhs} OF [mk_sym comp]; -fun mk_set_natural' set_natural = set_natural RS @{thm pointfreeE}; -fun mk_in_mono_tac n = if n = 0 then rtac @{thm subset_UNIV} 1 - else (rtac subsetI THEN' - rtac CollectI) 1 THEN - REPEAT_DETERM (eresolve_tac [CollectE, conjE] 1) THEN - REPEAT_DETERM_N (n - 1) - ((rtac conjI THEN' etac subset_trans THEN' atac) 1) THEN - (etac subset_trans THEN' atac) 1; - -fun mk_map_wpull_tac comp_in_alt inner_map_wpulls outer_map_wpull = - (rtac (@{thm wpull_cong} OF (replicate 3 comp_in_alt)) THEN' rtac outer_map_wpull) 1 THEN - WRAP (fn thm => rtac thm 1 THEN REPEAT_DETERM (atac 1)) (K all_tac) inner_map_wpulls all_tac THEN - TRY (REPEAT_DETERM (atac 1 ORELSE rtac @{thm wpull_id} 1)); - -fun mk_collect_set_natural_tac ctxt set_naturals = - substs_tac ctxt (@{thms collect_o image_insert image_empty} @ set_naturals) 1 THEN rtac refl 1; - -fun mk_simple_wit_tac wit_thms = ALLGOALS (atac ORELSE' eresolve_tac (@{thm emptyE} :: wit_thms)); +fun mk_pred_unfold_tac pred_def pred_defs rel_unfold {context = ctxt, prems = _} = + Local_Defs.unfold_tac ctxt (@{thm mem_Collect_eq_split} :: pred_def :: pred_defs) THEN + rtac rel_unfold 1; fun mk_map_comp_id_tac map_comp = (rtac trans THEN' rtac map_comp) 1 THEN REPEAT_DETERM (stac @{thm o_id} 1) THEN rtac refl 1; +fun mk_map_cong_tac m map_cong {context = ctxt, prems = _} = + EVERY' [rtac mp, rtac map_cong, + CONJ_WRAP' (K (rtac ballI THEN' Goal.assume_rule_tac ctxt)) (1 upto m)] 1; + fun mk_map_congL_tac passive map_cong map_id' = (rtac trans THEN' rtac map_cong THEN' EVERY' (replicate passive (rtac refl))) 1 THEN REPEAT_DETERM (EVERY' [rtac trans, etac bspec, atac, rtac sym, rtac @{thm id_apply}] 1) THEN rtac map_id' 1; -fun mk_map_wppull_tac map_id map_cong map_wpull map_comp set_naturals = - if null set_naturals then - EVERY' [rtac @{thm wppull_id}, rtac map_wpull, rtac map_id, rtac map_id] 1 - else EVERY' [REPEAT_DETERM o etac conjE, REPEAT_DETERM o dtac @{thm wppull_thePull}, - REPEAT_DETERM o etac exE, rtac @{thm wpull_wppull}, rtac map_wpull, - REPEAT_DETERM o rtac @{thm wpull_thePull}, rtac ballI, - REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac conjI, rtac CollectI, - CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}), - rtac @{thm image_subsetI}, rtac conjunct1, etac bspec, etac set_mp, atac]) - set_naturals, - CONJ_WRAP' (fn thm => EVERY' [rtac (map_comp RS trans), rtac (map_comp RS trans), - rtac (map_comp RS trans RS sym), rtac map_cong, - REPEAT_DETERM_N (length set_naturals) o EVERY' [rtac (o_apply RS trans), - rtac (o_apply RS trans RS sym), rtac (o_apply RS trans), rtac thm, - rtac conjunct2, etac bspec, etac set_mp, atac]]) [conjunct1, conjunct2]] 1; - -fun mk_rel_Gr_tac rel_def map_id map_cong map_wpull in_cong map_id' map_comp set_naturals - {context = ctxt, prems = _} = - let - val n = length set_naturals; - in - if null set_naturals then - Local_Defs.unfold_tac ctxt [rel_def] THEN EVERY' [rtac @{thm Gr_UNIV_id}, rtac map_id] 1 - else Local_Defs.unfold_tac ctxt [rel_def, @{thm Gr_def}] THEN - EVERY' [rtac equalityI, rtac subsetI, - REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}], - REPEAT_DETERM o dtac @{thm Pair_eq[THEN subst, of "%x. x"]}, - REPEAT_DETERM o etac conjE, hyp_subst_tac, - rtac CollectI, rtac exI, rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl, - rtac sym, rtac trans, rtac map_comp, rtac map_cong, - REPEAT_DETERM_N n o EVERY' [dtac @{thm set_rev_mp}, atac, - REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac, - rtac (o_apply RS trans), rtac (@{thm fst_conv} RS arg_cong RS trans), - rtac (@{thm snd_conv} RS sym)], - rtac CollectI, - CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}), - rtac @{thm image_subsetI}, dtac @{thm set_rev_mp}, atac, - REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac, - stac @{thm fst_conv}, atac]) set_naturals, - rtac @{thm subrelI}, etac CollectE, REPEAT_DETERM o eresolve_tac [exE, conjE], - REPEAT_DETERM o dtac @{thm Pair_eq[THEN subst, of "%x. x"]}, - REPEAT_DETERM o etac conjE, hyp_subst_tac, - rtac allE, rtac subst, rtac @{thm wpull_def}, rtac map_wpull, - REPEAT_DETERM_N n o rtac @{thm wpull_Gr}, etac allE, etac impE, rtac conjI, atac, - rtac conjI, REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac CollectI, - CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}), - rtac @{thm image_mono}, atac]) set_naturals, - rtac sym, rtac map_id', REPEAT_DETERM o eresolve_tac [bexE, conjE], - rtac @{thm relcompI}, rtac @{thm converseI}, - REPEAT_DETERM_N 2 o EVERY' [rtac CollectI, rtac exI, - rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl, etac sym, - etac @{thm set_rev_mp}, rtac equalityD1, rtac in_cong, - REPEAT_DETERM_N n o rtac @{thm Gr_def}]] 1 - end; - -fun mk_rel_Id_tac n rel_Gr map_id {context = ctxt, prems = _} = - Local_Defs.unfold_tac ctxt [rel_Gr, @{thm Id_alt}] THEN - subst_tac ctxt [map_id] 1 THEN - (if n = 0 then rtac refl 1 - else EVERY' [rtac @{thm arg_cong2[of _ _ _ _ Gr]}, - rtac equalityI, rtac @{thm subset_UNIV}, rtac subsetI, rtac CollectI, - CONJ_WRAP' (K (rtac @{thm subset_UNIV})) (1 upto n), rtac refl] 1); - -fun mk_rel_mono_tac rel_def in_mono {context = ctxt, prems = _} = - Local_Defs.unfold_tac ctxt [rel_def] THEN - EVERY' [rtac @{thm relcomp_mono}, rtac @{thm iffD2[OF converse_mono]}, - rtac @{thm Gr_mono}, rtac in_mono, REPEAT_DETERM o atac, - rtac @{thm Gr_mono}, rtac in_mono, REPEAT_DETERM o atac] 1; - -fun mk_map_cong_tac m map_cong {context = ctxt, prems = _} = - EVERY' [rtac mp, rtac map_cong, - CONJ_WRAP' (K (rtac ballI THEN' Goal.assume_rule_tac ctxt)) (1 upto m)] 1; - -fun mk_rel_converse_le_tac rel_def rel_Id map_cong map_comp set_naturals - {context = ctxt, prems = _} = - let - val n = length set_naturals; - in - if null set_naturals then - Local_Defs.unfold_tac ctxt [rel_Id] THEN rtac equalityD2 1 THEN rtac @{thm converse_Id} 1 - else Local_Defs.unfold_tac ctxt [rel_def, @{thm Gr_def}] THEN - EVERY' [rtac @{thm subrelI}, - REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}], - REPEAT_DETERM o dtac @{thm Pair_eq[THEN subst, of "%x. x"]}, - REPEAT_DETERM o etac conjE, hyp_subst_tac, rtac @{thm converseI}, - rtac @{thm relcompI}, rtac @{thm converseI}, - EVERY' (map (fn thm => EVERY' [rtac CollectI, rtac exI, - rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl, rtac trans, - rtac map_cong, REPEAT_DETERM_N n o rtac thm, - rtac (map_comp RS sym), rtac CollectI, - CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}), - etac @{thm flip_rel}]) set_naturals]) [@{thm snd_fst_flip}, @{thm fst_snd_flip}])] 1 - end; - -fun mk_rel_converse_tac le_converse = - EVERY' [rtac equalityI, rtac le_converse, rtac @{thm xt1(6)}, rtac @{thm converse_shift}, - rtac le_converse, REPEAT_DETERM o stac @{thm converse_converse}, rtac subset_refl] 1; - -fun mk_rel_O_tac rel_def rel_Id map_cong map_wppull map_comp set_naturals - {context = ctxt, prems = _} = - let - val n = length set_naturals; - fun in_tac nthO_in = rtac CollectI THEN' - CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}), - rtac @{thm image_subsetI}, rtac nthO_in, etac set_mp, atac]) set_naturals; - in - if null set_naturals then Local_Defs.unfold_tac ctxt [rel_Id] THEN rtac (@{thm Id_O_R} RS sym) 1 - else Local_Defs.unfold_tac ctxt [rel_def, @{thm Gr_def}] THEN - EVERY' [rtac equalityI, rtac @{thm subrelI}, - REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}], - REPEAT_DETERM o dtac @{thm Pair_eq[THEN subst, of "%x. x"]}, - REPEAT_DETERM o etac conjE, hyp_subst_tac, - rtac @{thm relcompI}, rtac @{thm relcompI}, rtac @{thm converseI}, - rtac CollectI, rtac exI, rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl, - rtac sym, rtac trans, rtac map_comp, rtac sym, rtac map_cong, - REPEAT_DETERM_N n o rtac @{thm fst_fstO}, - in_tac @{thm fstO_in}, - rtac CollectI, rtac exI, rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl, - rtac sym, rtac trans, rtac map_comp, rtac map_cong, - REPEAT_DETERM_N n o EVERY' [rtac trans, rtac o_apply, rtac ballE, rtac subst, - rtac @{thm csquare_def}, rtac @{thm csquare_fstO_sndO}, atac, etac notE, - etac set_mp, atac], - in_tac @{thm fstO_in}, - rtac @{thm relcompI}, rtac @{thm converseI}, - rtac CollectI, rtac exI, rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl, - rtac sym, rtac trans, rtac map_comp, rtac map_cong, - REPEAT_DETERM_N n o rtac o_apply, - in_tac @{thm sndO_in}, - rtac CollectI, rtac exI, rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl, - rtac sym, rtac trans, rtac map_comp, rtac sym, rtac map_cong, - REPEAT_DETERM_N n o rtac @{thm snd_sndO}, - in_tac @{thm sndO_in}, - rtac @{thm subrelI}, - REPEAT_DETERM o eresolve_tac [CollectE, @{thm relcompE}, @{thm converseE}], - REPEAT_DETERM o eresolve_tac [exE, conjE], - REPEAT_DETERM o dtac @{thm Pair_eq[THEN subst, of "%x. x"]}, - REPEAT_DETERM o etac conjE, hyp_subst_tac, - rtac allE, rtac subst, rtac @{thm wppull_def}, rtac map_wppull, - CONJ_WRAP' (K (rtac @{thm wppull_fstO_sndO})) set_naturals, - etac allE, etac impE, etac conjI, etac conjI, atac, - REPEAT_DETERM o eresolve_tac [bexE, conjE], - rtac @{thm relcompI}, rtac @{thm converseI}, - EVERY' (map (fn thm => EVERY' [rtac CollectI, rtac exI, - rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl, rtac sym, rtac trans, - rtac trans, rtac map_cong, REPEAT_DETERM_N n o rtac thm, - rtac (map_comp RS sym), atac, atac]) [@{thm fst_fstO}, @{thm snd_sndO}])] 1 - end; - -fun mk_in_rel_tac rel_def m {context = ctxt, prems = _} = - let - val ls' = replicate (Int.max (1, m)) (); - in - Local_Defs.unfold_tac ctxt (rel_def :: - @{thms Gr_def converse_unfold relcomp_unfold mem_Collect_eq prod.cases Pair_eq}) THEN - EVERY' [rtac iffI, REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac, rtac exI, - rtac conjI, CONJ_WRAP' (K atac) ls', rtac conjI, rtac refl, rtac refl, - REPEAT_DETERM o eresolve_tac [exE, conjE], rtac exI, rtac conjI, - REPEAT_DETERM_N 2 o EVERY' [rtac exI, rtac conjI, etac @{thm conjI[OF refl sym]}, - CONJ_WRAP' (K atac) ls']] 1 - end; - -fun mk_pred_unfold_tac pred_def pred_defs rel_unfold {context = ctxt, prems = _} = - Local_Defs.unfold_tac ctxt (@{thm mem_Collect_eq_split} :: pred_def :: pred_defs) THEN - rtac rel_unfold 1; - end; diff -r 64bed36cd8da -r 66058a677ddd src/HOL/Codatatype/Tools/bnf_util.ML --- a/src/HOL/Codatatype/Tools/bnf_util.ML Tue Sep 11 19:43:06 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_util.ML Tue Sep 11 19:45:12 2012 +0200 @@ -2,7 +2,7 @@ Author: Dmitriy Traytel, TU Muenchen Copyright 2012 -General library functions. +Library for bounded natural functors. *) signature BNF_UTIL = diff -r 64bed36cd8da -r 66058a677ddd src/HOL/Codatatype/Tools/bnf_wrap.ML --- a/src/HOL/Codatatype/Tools/bnf_wrap.ML Tue Sep 11 19:43:06 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_wrap.ML Tue Sep 11 19:45:12 2012 +0200 @@ -11,8 +11,11 @@ val mk_half_pairss: 'a list -> ('a * 'a) list list val mk_ctr: typ list -> term -> term val wrap_datatype: ({prems: thm list, context: Proof.context} -> tactic) list list -> - (term list * term) * (binding list * binding list list) -> local_theory -> + ((bool * term list) * term) * + (binding list * (binding list list * (binding * term) list list)) -> local_theory -> (term list list * thm list * thm list list) * local_theory + val parse_wrap_options: bool parser + val parse_bound_term: (binding * string) parser end; structure BNF_Wrap : BNF_WRAP = @@ -55,8 +58,7 @@ fun mk_half_pairss ys = mk_half_pairss' [[]] ys; -(* TODO: provide a way to have a different default value, e.g. "tl Nil = Nil" *) -fun mk_undef T Ts = Const (@{const_name undefined}, Ts ---> T); +fun mk_undefined T = Const (@{const_name undefined}, T); fun mk_ctr Ts ctr = let val Type (_, Ts0) = body_type (fastype_of ctr) in @@ -66,27 +68,29 @@ fun eta_expand_case_arg xs f_xs = fold_rev Term.lambda xs f_xs; fun name_of_ctr c = - case head_of c of + (case head_of c of Const (s, _) => s | Free (s, _) => s - | _ => error "Cannot extract name of constructor"; + | _ => error "Cannot extract name of constructor"); -fun prepare_wrap_datatype prep_term ((raw_ctrs, raw_case), (raw_disc_binders, raw_sel_binderss)) - no_defs_lthy = +fun prepare_wrap_datatype prep_term (((no_dests, raw_ctrs), raw_case), + (raw_disc_binders, (raw_sel_binderss, raw_sel_defaultss))) no_defs_lthy = let (* TODO: sanity checks on arguments *) (* TODO: attributes (simp, case_names, etc.) *) (* TODO: case syntax *) (* TODO: integration with function package ("size") *) - val ctrs0 = map (prep_term no_defs_lthy) raw_ctrs; - val case0 = prep_term no_defs_lthy raw_case; - - val n = length ctrs0; + val n = length raw_ctrs; val ks = 1 upto n; val _ = if n > 0 then () else error "No constructors specified"; + val ctrs0 = map (prep_term no_defs_lthy) raw_ctrs; + val case0 = prep_term no_defs_lthy raw_case; + val sel_defaultss = + pad_list [] n (map (map (apsnd (prep_term no_defs_lthy))) raw_sel_defaultss); + val Type (fpT_name, As0) = body_type (fastype_of (hd ctrs0)); val b = Binding.qualified_name fpT_name; @@ -173,81 +177,107 @@ val exist_xs_v_eq_ctrs = map2 (fn xctr => fn xs => list_exists_free xs (HOLogic.mk_eq (v, xctr))) xctrs xss; - fun disc_free b = Free (Binding.name_of b, fpT --> HOLogic.boolT); + val unique_disc_no_def = TrueI; (*arbitrary marker*) + val alternate_disc_no_def = FalseE; (*arbitrary marker*) - fun disc_spec b exist_xs_v_eq_ctr = mk_Trueprop_eq (disc_free b $ v, exist_xs_v_eq_ctr); - - fun alternate_disc_lhs k = + fun alternate_disc_lhs get_disc k = HOLogic.mk_not (case nth disc_binders (k - 1) of NONE => nth exist_xs_v_eq_ctrs (k - 1) - | SOME b => disc_free b $ v); - - fun alternate_disc k = - if n = 2 then Term.lambda v (alternate_disc_lhs (3 - k)) else error "Cannot use \"*\" here" + | SOME b => get_disc b (k - 1) $ v); - fun mk_sel_case_args proto_sels T = - map2 (fn Ts => fn i => - case AList.lookup (op =) proto_sels i of - NONE => mk_undef T Ts - | SOME (xs, x) => fold_rev Term.lambda xs x) ctr_Tss ks; + val (all_sels_distinct, discs, selss, disc_defs, sel_defs, sel_defss, lthy') = + if no_dests then + (true, [], [], [], [], [], no_defs_lthy) + else + let + fun disc_free b = Free (Binding.name_of b, fpT --> HOLogic.boolT); + + fun disc_spec b exist_xs_v_eq_ctr = mk_Trueprop_eq (disc_free b $ v, exist_xs_v_eq_ctr); + + fun alternate_disc k = Term.lambda v (alternate_disc_lhs (K o disc_free) (3 - k)); - fun sel_spec b proto_sels = - let - val _ = - (case duplicates (op =) (map fst proto_sels) of - k :: _ => error ("Duplicate selector name " ^ quote (Binding.name_of b) ^ - " for constructor " ^ quote (Syntax.string_of_term no_defs_lthy (nth ctrs (k - 1)))) - | [] => ()) - val T = - (case distinct (op =) (map (fastype_of o snd o snd) proto_sels) of - [T] => T - | T :: T' :: _ => error ("Inconsistent range type for selector " ^ - quote (Binding.name_of b) ^ ": " ^ quote (Syntax.string_of_typ no_defs_lthy T) ^ - " vs. " ^ quote (Syntax.string_of_typ no_defs_lthy T'))); - in - mk_Trueprop_eq (Free (Binding.name_of b, fpT --> T) $ v, - Term.list_comb (mk_case As T, mk_sel_case_args proto_sels T) $ v) - end; + fun mk_sel_case_args b proto_sels T = + map2 (fn Ts => fn k => + (case AList.lookup (op =) proto_sels k of + NONE => + let val def_T = Ts ---> T in + (case AList.lookup Binding.eq_name (rev (nth sel_defaultss (k - 1))) b of + NONE => mk_undefined def_T + | SOME t => fold_rev (fn T => Term.lambda (Free (Name.uu, T))) Ts + (Term.subst_atomic_types [(fastype_of t, T)] t)) + end + | SOME (xs, x) => fold_rev Term.lambda xs x)) ctr_Tss ks; - val missing_unique_disc_def = TrueI; (*arbitrary marker*) - val missing_alternate_disc_def = FalseE; (*arbitrary marker*) + fun sel_spec b proto_sels = + let + val _ = + (case duplicates (op =) (map fst proto_sels) of + k :: _ => error ("Duplicate selector name " ^ quote (Binding.name_of b) ^ + " for constructor " ^ + quote (Syntax.string_of_term no_defs_lthy (nth ctrs (k - 1)))) + | [] => ()) + val T = + (case distinct (op =) (map (fastype_of o snd o snd) proto_sels) of + [T] => T + | T :: T' :: _ => error ("Inconsistent range type for selector " ^ + quote (Binding.name_of b) ^ ": " ^ quote (Syntax.string_of_typ no_defs_lthy T) ^ + " vs. " ^ quote (Syntax.string_of_typ no_defs_lthy T'))); + in + mk_Trueprop_eq (Free (Binding.name_of b, fpT --> T) $ v, + Term.list_comb (mk_case As T, mk_sel_case_args b proto_sels T) $ v) + end; - val proto_selss = map3 (fn k => fn xs => map (fn x => (k, (xs, x)))) ks xss xss; - val sel_bundles = AList.group Binding.eq_name (flat sel_binderss ~~ flat proto_selss); - val sel_binders = map fst sel_bundles; + val sel_binders = flat sel_binderss; + val uniq_sel_binders = distinct Binding.eq_name sel_binders; + val all_sels_distinct = (length uniq_sel_binders = length sel_binders); + + val sel_binder_index = + if all_sels_distinct then 1 upto length sel_binders + else map (fn b => find_index (curry Binding.eq_name b) uniq_sel_binders) sel_binders; - fun unflat_selss xs = unflat_lookup Binding.eq_name sel_binders xs sel_binderss; + val proto_sels = flat (map3 (fn k => fn xs => map (fn x => (k, (xs, x)))) ks xss xss); + val sel_bundles = + AList.group (op =) (sel_binder_index ~~ proto_sels) + |> sort (int_ord o pairself fst) + |> map snd |> curry (op ~~) uniq_sel_binders; + val sel_binders = map fst sel_bundles; + + fun unflat_selss xs = unflat_lookup Binding.eq_name sel_binders xs sel_binderss; - val (((raw_discs, raw_disc_defs), (raw_sels, raw_sel_defs)), (lthy', lthy)) = - no_defs_lthy - |> apfst split_list o fold_map4 (fn k => fn m => fn exist_xs_v_eq_ctr => - fn NONE => - if n = 1 then pair (Term.lambda v (mk_v_eq_v ()), missing_unique_disc_def) - else if m = 0 then pair (Term.lambda v exist_xs_v_eq_ctr, refl) - else pair (alternate_disc k, missing_alternate_disc_def) - | SOME b => Specification.definition (SOME (b, NONE, NoSyn), - ((Thm.def_binding b, []), disc_spec b exist_xs_v_eq_ctr)) #>> apsnd snd) - ks ms exist_xs_v_eq_ctrs disc_binders - ||>> apfst split_list o fold_map (fn (b, proto_sels) => - Specification.definition (SOME (b, NONE, NoSyn), - ((Thm.def_binding b, []), sel_spec b proto_sels)) #>> apsnd snd) sel_bundles - ||> `Local_Theory.restore; + val (((raw_discs, raw_disc_defs), (raw_sels, raw_sel_defs)), (lthy', lthy)) = + no_defs_lthy + |> apfst split_list o fold_map4 (fn k => fn m => fn exist_xs_v_eq_ctr => + fn NONE => + if n = 1 then pair (Term.lambda v (mk_v_eq_v ()), unique_disc_no_def) + else if m = 0 then pair (Term.lambda v exist_xs_v_eq_ctr, refl) + else pair (alternate_disc k, alternate_disc_no_def) + | SOME b => Specification.definition (SOME (b, NONE, NoSyn), + ((Thm.def_binding b, []), disc_spec b exist_xs_v_eq_ctr)) #>> apsnd snd) + ks ms exist_xs_v_eq_ctrs disc_binders + ||>> apfst split_list o fold_map (fn (b, proto_sels) => + Specification.definition (SOME (b, NONE, NoSyn), + ((Thm.def_binding b, []), sel_spec b proto_sels)) #>> apsnd snd) sel_bundles + ||> `Local_Theory.restore; - (*transforms defined frees into consts (and more)*) - val phi = Proof_Context.export_morphism lthy lthy'; + (*transforms defined frees into consts (and more)*) + val phi = Proof_Context.export_morphism lthy lthy'; - val disc_defs = map (Morphism.thm phi) raw_disc_defs; - val sel_defss = unflat_selss (map (Morphism.thm phi) raw_sel_defs); + val disc_defs = map (Morphism.thm phi) raw_disc_defs; + val sel_defs = map (Morphism.thm phi) raw_sel_defs; + val sel_defss = unflat_selss sel_defs; - val discs0 = map (Morphism.term phi) raw_discs; - val selss0 = unflat_selss (map (Morphism.term phi) raw_sels); + val discs0 = map (Morphism.term phi) raw_discs; + val selss0 = unflat_selss (map (Morphism.term phi) raw_sels); + + fun mk_disc_or_sel Ts c = + Term.subst_atomic_types (snd (Term.dest_Type (domain_type (fastype_of c))) ~~ Ts) c; - fun mk_disc_or_sel Ts c = - Term.subst_atomic_types (snd (Term.dest_Type (domain_type (fastype_of c))) ~~ Ts) c; - - val discs = map (mk_disc_or_sel As) discs0; - val selss = map (map (mk_disc_or_sel As)) selss0; + val discs = map (mk_disc_or_sel As) discs0; + val selss = map (map (mk_disc_or_sel As)) selss0; + in + (all_sels_distinct, discs, selss, disc_defs, sel_defs, sel_defss, lthy') + end; fun mk_imp_p Qs = Logic.list_implies (Qs, HOLogic.mk_Trueprop p); @@ -309,133 +339,163 @@ Skip_Proof.prove lthy [] [] goal (fn _ => mk_nchotomy_tac n exhaust_thm) end; - val sel_thmss = - map2 (fn case_thm => map (fn sel_def => case_thm RS (sel_def RS trans))) case_thms - sel_defss; - - fun mk_unique_disc_def () = - let - val m = the_single ms; - val goal = mk_Trueprop_eq (mk_v_eq_v (), the_single exist_xs_v_eq_ctrs); - in - Skip_Proof.prove lthy [] [] goal (fn _ => mk_unique_disc_def_tac m exhaust_thm') - |> singleton (Proof_Context.export names_lthy lthy) - |> Thm.close_derivation - end; - - fun mk_alternate_disc_def k = - let - val goal = - mk_Trueprop_eq (Morphism.term phi (alternate_disc_lhs (3 - k)), - nth exist_xs_v_eq_ctrs (k - 1)); - in - Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} => - mk_alternate_disc_def_tac ctxt k (nth disc_defs (2 - k)) (nth distinct_thms (2 - k)) - exhaust_thm') - |> singleton (Proof_Context.export names_lthy lthy) - |> Thm.close_derivation - end; - - val has_alternate_disc_def = - exists (fn def => Thm.eq_thm_prop (def, missing_alternate_disc_def)) disc_defs; - - val disc_defs' = - map2 (fn k => fn def => - if Thm.eq_thm_prop (def, missing_unique_disc_def) then mk_unique_disc_def () - else if Thm.eq_thm_prop (def, missing_alternate_disc_def) then mk_alternate_disc_def k - else def) - ks disc_defs; - - val discD_thms = map (fn def => def RS iffD1) disc_defs'; - val discI_thms = - map2 (fn m => fn def => funpow m (fn thm => exI RS thm) (def RS iffD2)) ms disc_defs'; - val not_discI_thms = - map2 (fn m => fn def => funpow m (fn thm => allI RS thm) - (Local_Defs.unfold lthy @{thms not_ex} (def RS @{thm ssubst[of _ _ Not]}))) - ms disc_defs'; - - val (disc_thmss', disc_thmss) = - let - fun mk_thm discI _ [] = refl RS discI - | mk_thm _ not_discI [distinct] = distinct RS not_discI; - fun mk_thms discI not_discI distinctss = map (mk_thm discI not_discI) distinctss; - in - map3 mk_thms discI_thms not_discI_thms distinct_thmsss' |> `transpose - end; - - val disc_thms = flat (map2 (fn true => K [] | false => I) no_discs disc_thmss); - - val disc_exclude_thms = - if has_alternate_disc_def then - [] + val (all_sel_thms, sel_thmss, disc_thms, discI_thms, disc_exclude_thms, disc_exhaust_thms, + collapse_thms, case_eq_thms) = + if no_dests then + ([], [], [], [], [], [], [], []) else let - fun mk_goal [] = [] - | mk_goal [((_, true), (_, true))] = [] - | mk_goal [(((_, disc), _), ((_, disc'), _))] = - [Logic.all v (Logic.mk_implies (HOLogic.mk_Trueprop (betapply (disc, v)), - HOLogic.mk_Trueprop (HOLogic.mk_not (betapply (disc', v)))))]; - fun prove tac goal = Skip_Proof.prove lthy [] [] goal (K tac); + fun make_sel_thm case_thm sel_def = case_thm RS (sel_def RS trans); + + fun has_undefined_rhs thm = + (case snd (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of thm))) of + Const (@{const_name undefined}, _) => true + | _ => false); + + val sel_thmss = map2 (map o make_sel_thm) case_thms sel_defss; + + val all_sel_thms = + (if all_sels_distinct andalso forall null sel_defaultss then + flat sel_thmss + else + map_product (fn s => fn c => make_sel_thm c s) sel_defs case_thms) + |> filter_out has_undefined_rhs; + + fun mk_unique_disc_def () = + let + val m = the_single ms; + val goal = mk_Trueprop_eq (mk_v_eq_v (), the_single exist_xs_v_eq_ctrs); + in + Skip_Proof.prove lthy [] [] goal (fn _ => mk_unique_disc_def_tac m exhaust_thm') + |> singleton (Proof_Context.export names_lthy lthy) + |> Thm.close_derivation + end; - val bundles = ms ~~ discD_thms ~~ discs ~~ no_discs; - val half_pairss = mk_half_pairss bundles; + fun mk_alternate_disc_def k = + let + val goal = + mk_Trueprop_eq (alternate_disc_lhs (K (nth discs)) (3 - k), + nth exist_xs_v_eq_ctrs (k - 1)); + in + Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} => + mk_alternate_disc_def_tac ctxt k (nth disc_defs (2 - k)) + (nth distinct_thms (2 - k)) exhaust_thm') + |> singleton (Proof_Context.export names_lthy lthy) + |> Thm.close_derivation + end; + + val has_alternate_disc_def = + exists (fn def => Thm.eq_thm_prop (def, alternate_disc_no_def)) disc_defs; + + val disc_defs' = + map2 (fn k => fn def => + if Thm.eq_thm_prop (def, unique_disc_no_def) then mk_unique_disc_def () + else if Thm.eq_thm_prop (def, alternate_disc_no_def) then mk_alternate_disc_def k + else def) ks disc_defs; + + val discD_thms = map (fn def => def RS iffD1) disc_defs'; + val discI_thms = + map2 (fn m => fn def => funpow m (fn thm => exI RS thm) (def RS iffD2)) ms + disc_defs'; + val not_discI_thms = + map2 (fn m => fn def => funpow m (fn thm => allI RS thm) + (Local_Defs.unfold lthy @{thms not_ex} (def RS @{thm ssubst[of _ _ Not]}))) + ms disc_defs'; + + val (disc_thmss', disc_thmss) = + let + fun mk_thm discI _ [] = refl RS discI + | mk_thm _ not_discI [distinct] = distinct RS not_discI; + fun mk_thms discI not_discI distinctss = map (mk_thm discI not_discI) distinctss; + in + map3 mk_thms discI_thms not_discI_thms distinct_thmsss' |> `transpose + end; + + val disc_thms = flat (map2 (fn true => K [] | false => I) no_discs disc_thmss); - val goal_halvess = map mk_goal half_pairss; - val half_thmss = - map3 (fn [] => K (K []) | [goal] => fn [((((m, discD), _), _), _)] => fn disc_thm => - [prove (mk_half_disc_exclude_tac m discD disc_thm) goal]) - goal_halvess half_pairss (flat disc_thmss'); + val disc_exclude_thms = + if has_alternate_disc_def then + [] + else + let + fun mk_goal [] = [] + | mk_goal [((_, true), (_, true))] = [] + | mk_goal [(((_, disc), _), ((_, disc'), _))] = + [Logic.all v (Logic.mk_implies (HOLogic.mk_Trueprop (betapply (disc, v)), + HOLogic.mk_Trueprop (HOLogic.mk_not (betapply (disc', v)))))]; + fun prove tac goal = Skip_Proof.prove lthy [] [] goal (K tac); + + val bundles = ms ~~ discD_thms ~~ discs ~~ no_discs; + val half_pairss = mk_half_pairss bundles; + + val goal_halvess = map mk_goal half_pairss; + val half_thmss = + map3 (fn [] => K (K []) | [goal] => fn [((((m, discD), _), _), _)] => + fn disc_thm => [prove (mk_half_disc_exclude_tac m discD disc_thm) goal]) + goal_halvess half_pairss (flat disc_thmss'); + + val goal_other_halvess = map (mk_goal o map swap) half_pairss; + val other_half_thmss = + map2 (map2 (prove o mk_other_half_disc_exclude_tac)) half_thmss + goal_other_halvess; + in + interleave (flat half_thmss) (flat other_half_thmss) + end; - val goal_other_halvess = map (mk_goal o map swap) half_pairss; - val other_half_thmss = - map2 (map2 (prove o mk_other_half_disc_exclude_tac)) half_thmss goal_other_halvess; - in - interleave (flat half_thmss) (flat other_half_thmss) - end; + val disc_exhaust_thms = + if has_alternate_disc_def orelse no_discs_at_all then + [] + else + let + fun mk_prem disc = mk_imp_p [HOLogic.mk_Trueprop (betapply (disc, v))]; + val goal = fold_rev Logic.all [p, v] (mk_imp_p (map mk_prem discs)); + in + [Skip_Proof.prove lthy [] [] goal (fn _ => + mk_disc_exhaust_tac n exhaust_thm discI_thms)] + end; - val disc_exhaust_thms = - if has_alternate_disc_def orelse no_discs_at_all then - [] - else - let - fun mk_prem disc = mk_imp_p [HOLogic.mk_Trueprop (betapply (disc, v))]; - val goal = fold_rev Logic.all [p, v] (mk_imp_p (map mk_prem discs)); + val collapse_thms = + if no_dests then + [] + else + let + fun mk_goal ctr disc sels = + let + val prem = HOLogic.mk_Trueprop (betapply (disc, v)); + val concl = + mk_Trueprop_eq ((null sels ? swap) + (Term.list_comb (ctr, map ap_v sels), v)); + in + if prem aconv concl then NONE + else SOME (Logic.all v (Logic.mk_implies (prem, concl))) + end; + val goals = map3 mk_goal ctrs discs selss; + in + map4 (fn m => fn discD => fn sel_thms => Option.map (fn goal => + Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} => + mk_collapse_tac ctxt m discD sel_thms) + |> perhaps (try (fn thm => refl RS thm)))) ms discD_thms sel_thmss goals + |> map_filter I + end; + + val case_eq_thms = + if no_dests then + [] + else + let + fun mk_body f sels = Term.list_comb (f, map ap_v sels); + val goal = + mk_Trueprop_eq (fcase $ v, mk_IfN B (map ap_v discs) (map2 mk_body fs selss)); + in + [Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} => + mk_case_eq_tac ctxt n exhaust_thm' case_thms disc_thmss' sel_thmss)] + |> Proof_Context.export names_lthy lthy + end; in - [Skip_Proof.prove lthy [] [] goal (fn _ => - mk_disc_exhaust_tac n exhaust_thm discI_thms)] + (all_sel_thms, sel_thmss, disc_thms, discI_thms, disc_exclude_thms, disc_exhaust_thms, + collapse_thms, case_eq_thms) end; - val collapse_thms = - let - fun mk_goal ctr disc sels = - let - val prem = HOLogic.mk_Trueprop (betapply (disc, v)); - val concl = - mk_Trueprop_eq ((null sels ? swap) (Term.list_comb (ctr, map ap_v sels), v)); - in - if prem aconv concl then NONE - else SOME (Logic.all v (Logic.mk_implies (prem, concl))) - end; - val goals = map3 mk_goal ctrs discs selss; - in - map4 (fn m => fn discD => fn sel_thms => Option.map (fn goal => - Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} => - mk_collapse_tac ctxt m discD sel_thms) - |> perhaps (try (fn thm => refl RS thm)))) ms discD_thms sel_thmss goals - |> map_filter I - end; - - val case_eq_thm = - let - fun mk_body f sels = Term.list_comb (f, map ap_v sels); - val goal = - mk_Trueprop_eq (fcase $ v, mk_IfN B (map ap_v discs) (map2 mk_body fs selss)); - in - Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} => - mk_case_eq_tac ctxt n exhaust_thm' case_thms disc_thmss' sel_thmss) - |> singleton (Proof_Context.export names_lthy lthy) - end; - val (case_cong_thm, weak_case_cong_thm) = let fun mk_prem xctr xs f g = @@ -484,7 +544,7 @@ val notes = [(case_congN, [case_cong_thm]), - (case_eqN, [case_eq_thm]), + (case_eqN, case_eq_thms), (casesN, case_thms), (collapseN, collapse_thms), (discsN, disc_thms), @@ -494,7 +554,7 @@ (exhaustN, [exhaust_thm]), (injectN, flat inject_thmss), (nchotomyN, [nchotomy_thm]), - (selsN, flat sel_thmss), + (selsN, all_sel_thms), (splitN, [split_thm]), (split_asmN, [split_asm_thm]), (weak_case_cong_thmsN, [weak_case_cong_thm])] @@ -510,20 +570,29 @@ fun wrap_datatype tacss = (fn (goalss, after_qed, lthy) => map2 (map2 (Skip_Proof.prove lthy [] [])) goalss tacss - |> (fn thms => after_qed thms lthy)) oo - prepare_wrap_datatype (K I) (* FIXME? (singleton o Type_Infer_Context.infer_types) *) + |> (fn thms => after_qed thms lthy)) oo prepare_wrap_datatype (K I); + +fun parse_bracket_list parser = @{keyword "["} |-- Parse.list parser --| @{keyword "]"}; -val parse_bindings = Parse.$$$ "[" |-- Parse.list Parse.binding --| Parse.$$$ "]"; -val parse_bindingss = Parse.$$$ "[" |-- Parse.list parse_bindings --| Parse.$$$ "]"; +val parse_bindings = parse_bracket_list Parse.binding; +val parse_bindingss = parse_bracket_list parse_bindings; + +val parse_bound_term = (Parse.binding --| @{keyword ":"}) -- Parse.term; +val parse_bound_terms = parse_bracket_list parse_bound_term; +val parse_bound_termss = parse_bracket_list parse_bound_terms; val wrap_datatype_cmd = (fn (goalss, after_qed, lthy) => Proof.theorem NONE (snd oo after_qed) (map (map (rpair [])) goalss) lthy) oo prepare_wrap_datatype Syntax.read_term; +val parse_wrap_options = + Scan.optional (@{keyword "("} |-- (@{keyword "no_dests"} >> K true) --| @{keyword ")"}) false; + val _ = Outer_Syntax.local_theory_to_proof @{command_spec "wrap_data"} "wraps an existing datatype" - (((Parse.$$$ "[" |-- Parse.list Parse.term --| Parse.$$$ "]") -- Parse.term -- - Scan.optional (parse_bindings -- Scan.optional parse_bindingss []) ([], [])) + ((parse_wrap_options -- (@{keyword "["} |-- Parse.list Parse.term --| @{keyword "]"}) -- + Parse.term -- Scan.optional (parse_bindings -- Scan.optional (parse_bindingss -- + Scan.optional parse_bound_termss []) ([], [])) ([], ([], []))) >> wrap_datatype_cmd); end;