# HG changeset patch # User traytel # Date 1387361020 -3600 # Node ID af71b753c45979d93faaea4e9317f0d2ed9dbcb4 # Parent fac0c76bbda265c9e2527f4e41aa7a4315dcd3a2 express weak pullback property of bnfs only in terms of the relator diff -r fac0c76bbda2 -r af71b753c459 src/HOL/BNF/BNF.thy --- a/src/HOL/BNF/BNF.thy Fri Dec 20 21:09:01 2013 +0100 +++ b/src/HOL/BNF/BNF.thy Wed Dec 18 11:03:40 2013 +0100 @@ -14,7 +14,7 @@ begin hide_const (open) image2 image2p vimage2p Gr Grp collect fsts snds setl setr - convol thePull pick_middlep fstOp sndOp csquare inver - image2 relImage relInvImage prefCl PrefCl Succ Shift shift + convol pick_middlep fstOp sndOp csquare inver relImage relInvImage + prefCl PrefCl Succ Shift shift end diff -r fac0c76bbda2 -r af71b753c459 src/HOL/BNF/BNF_Comp.thy --- a/src/HOL/BNF/BNF_Comp.thy Fri Dec 20 21:09:01 2013 +0100 +++ b/src/HOL/BNF/BNF_Comp.thy Wed Dec 18 11:03:40 2013 +0100 @@ -11,9 +11,6 @@ imports Basic_BNFs begin -lemma wpull_id: "wpull UNIV B1 B2 id id id id" -unfolding wpull_def by simp - lemma empty_natural: "(\_. {}) o f = image g o (\_. {})" by (rule ext) simp diff -r fac0c76bbda2 -r af71b753c459 src/HOL/BNF/BNF_Def.thy --- a/src/HOL/BNF/BNF_Def.thy Fri Dec 20 21:09:01 2013 +0100 +++ b/src/HOL/BNF/BNF_Def.thy Wed Dec 18 11:03:40 2013 +0100 @@ -39,56 +39,13 @@ definition csquare where "csquare A f1 f2 p1 p2 \ (\ a \ A. f1 (p1 a) = f2 (p2 a))" -(* 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 blast -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 - lemma eq_alt: "op = = Grp UNIV id" unfolding Grp_def by auto lemma leq_conversepI: "R = op = \ R \ R^--1" by auto -lemma eq_OOI: "R = op = \ R = R OO R" +lemma leq_OOI: "R = op = \ R \ R OO R" by auto lemma OO_Grp_alt: "(Grp A f)^--1 OO Grp A g = (\x y. \z. z \ A \ f z = x \ g z = y)" @@ -142,11 +99,6 @@ "csquare (Collect (split (P OO Q))) snd fst (fstOp P Q) (sndOp P Q)" unfolding csquare_def fstOp_def sndOp_def using pick_middlep by simp -lemma wppull_fstOp_sndOp: -shows "wppull (Collect (split (P OO Q))) (Collect (split P)) (Collect (split Q)) - snd fst fst snd (fstOp P Q) (sndOp P Q)" -using pick_middlep unfolding wppull_def fstOp_def sndOp_def relcompp.simps by auto - lemma snd_fst_flip: "snd xy = (fst o (%(x, y). (y, x))) xy" by (simp split: prod.split) diff -r fac0c76bbda2 -r af71b753c459 src/HOL/BNF/BNF_GFP.thy --- a/src/HOL/BNF/BNF_GFP.thy Fri Dec 20 21:09:01 2013 +0100 +++ b/src/HOL/BNF/BNF_GFP.thy Wed Dec 18 11:03:40 2013 +0100 @@ -254,29 +254,6 @@ "\|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 where -"pickWP A p1 p2 b1 b2 \ SOME a. a \ A \ p1 a = b1 \ p2 a = b2" - -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. a \ A \ p1 a = b1 \ p2 a = b2" -using assms unfolding wpull_def by blast - -lemma pickWP_raw: -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" -unfolding pickWP_def using assms someI_ex[OF pickWP_pred] by fastforce - -lemmas pickWP = - pickWP_raw[THEN conjunct1] - pickWP_raw[THEN conjunct2, THEN conjunct1] - pickWP_raw[THEN conjunct2, THEN conjunct2] - lemma Inl_Field_csum: "a \ Field r \ Inl a \ Field (r +c s)" unfolding Field_card_of csum_def by auto diff -r fac0c76bbda2 -r af71b753c459 src/HOL/BNF/BNF_LFP.thy --- a/src/HOL/BNF/BNF_LFP.thy Fri Dec 20 21:09:01 2013 +0100 +++ b/src/HOL/BNF/BNF_LFP.thy Wed Dec 18 11:03:40 2013 +0100 @@ -224,6 +224,10 @@ shows "PROP P x y" by (rule `(\x y. PROP P x y)`) +lemma nchotomy_relcomppE: + "\\y. \x. y = f x; (r OO s) a c; (\b. r a (f b) \ s (f b) c \ P)\ \ P" + by (metis relcompp.cases) + lemma vimage2p_fun_rel: "(fun_rel (vimage2p f g R) R) f g" unfolding fun_rel_def vimage2p_def by auto diff -r fac0c76bbda2 -r af71b753c459 src/HOL/BNF/BNF_Util.thy --- a/src/HOL/BNF/BNF_Util.thy Fri Dec 20 21:09:01 2013 +0100 +++ b/src/HOL/BNF/BNF_Util.thy Wed Dec 18 11:03:40 2013 +0100 @@ -17,17 +17,6 @@ definition collect where "collect F x = (\f \ F. f x)" -(* Weak pullbacks: *) -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))" - -(* 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))" - lemma fstI: "x = (y, z) \ fst x = y" by simp diff -r fac0c76bbda2 -r af71b753c459 src/HOL/BNF/Basic_BNFs.thy --- a/src/HOL/BNF/Basic_BNFs.thy Fri Dec 20 21:09:01 2013 +0100 +++ b/src/HOL/BNF/Basic_BNFs.thy Wed Dec 18 11:03:40 2013 +0100 @@ -17,9 +17,6 @@ Main begin -lemma wpull_Grp_def: "wpull A B1 B2 f1 f2 p1 p2 \ Grp B1 f1 OO (Grp B2 f2)\\ \ (Grp A p1)\\ OO Grp A p2" - unfolding wpull_def Grp_def by auto - bnf ID: 'a map: "id :: ('a \ 'b) \ 'a \ 'b" sets: "\x. {x}" @@ -34,7 +31,7 @@ map: "id :: 'a \ 'a" bd: "natLeq +c |UNIV :: 'a set|" rel: "op = :: 'a \ 'a \ bool" -by (auto simp add: wpull_Grp_def Grp_def +by (auto simp add: Grp_def card_order_csum natLeq_card_order card_of_card_order_on cinfinite_csum natLeq_cinfinite) @@ -93,47 +90,9 @@ apply (rule finite_iff_ordLess_natLeq[THEN iffD1]) by (simp add: setr_def split: sum.split) next - fix A1 A2 B11 B12 B21 B22 f11 f12 f21 f22 p11 p12 p21 p22 - assume "wpull A1 B11 B21 f11 f21 p11 p21" "wpull A2 B12 B22 f12 f22 p12 p22" - hence - pull1: "\b1 b2. \b1 \ B11; b2 \ B21; f11 b1 = f21 b2\ \ \a \ A1. p11 a = b1 \ p21 a = b2" - and pull2: "\b1 b2. \b1 \ B12; b2 \ B22; f12 b1 = f22 b2\ \ \a \ A2. p12 a = b1 \ p22 a = b2" - unfolding wpull_def by blast+ - show "wpull {x. setl x \ A1 \ setr x \ A2} - {x. setl x \ B11 \ setr x \ B12} {x. setl x \ B21 \ setr x \ B22} - (sum_map f11 f12) (sum_map f21 f22) (sum_map p11 p12) (sum_map p21 p22)" - (is "wpull ?in ?in1 ?in2 ?mapf1 ?mapf2 ?mapp1 ?mapp2") - proof (unfold wpull_def) - { fix B1 B2 - assume *: "B1 \ ?in1" "B2 \ ?in2" "?mapf1 B1 = ?mapf2 B2" - have "\A \ ?in. ?mapp1 A = B1 \ ?mapp2 A = B2" - proof (cases B1) - case (Inl b1) - { fix b2 assume "B2 = Inr b2" - with Inl *(3) have False by simp - } then obtain b2 where Inl': "B2 = Inl b2" by (cases B2) (simp, blast) - with Inl * have "b1 \ B11" "b2 \ B21" "f11 b1 = f21 b2" - by (simp add: setl_def)+ - with pull1 obtain a where "a \ A1" "p11 a = b1" "p21 a = b2" by blast+ - with Inl Inl' have "Inl a \ ?in" "?mapp1 (Inl a) = B1 \ ?mapp2 (Inl a) = B2" - by (simp add: sum_set_defs)+ - thus ?thesis by blast - next - case (Inr b1) - { fix b2 assume "B2 = Inl b2" - with Inr *(3) have False by simp - } then obtain b2 where Inr': "B2 = Inr b2" by (cases B2) (simp, blast) - with Inr * have "b1 \ B12" "b2 \ B22" "f12 b1 = f22 b2" - by (simp add: sum_set_defs)+ - with pull2 obtain a where "a \ A2" "p12 a = b1" "p22 a = b2" by blast+ - with Inr Inr' have "Inr a \ ?in" "?mapp1 (Inr a) = B1 \ ?mapp2 (Inr a) = B2" - by (simp add: sum_set_defs)+ - thus ?thesis by blast - qed - } - thus "\B1 B2. B1 \ ?in1 \ B2 \ ?in2 \ ?mapf1 B1 = ?mapf2 B2 \ - (\A \ ?in. ?mapp1 A = B1 \ ?mapp2 A = B2)" by fastforce - qed + fix R1 R2 S1 S2 + show "sum_rel R1 R2 OO sum_rel S1 S2 \ sum_rel (R1 OO S1) (R2 OO S2)" + by (auto simp: sum_rel_def split: sum.splits) next fix R S show "sum_rel R S = @@ -187,12 +146,8 @@ show "|{snd x}| \o natLeq" by (metis ordLess_imp_ordLeq finite_iff_ordLess_natLeq finite.emptyI finite_insert) next - fix A1 A2 B11 B12 B21 B22 f11 f12 f21 f22 p11 p12 p21 p22 - assume "wpull A1 B11 B21 f11 f21 p11 p21" "wpull A2 B12 B22 f12 f22 p12 p22" - thus "wpull {x. {fst x} \ A1 \ {snd x} \ A2} - {x. {fst x} \ B11 \ {snd x} \ B12} {x. {fst x} \ B21 \ {snd x} \ B22} - (map_pair f11 f12) (map_pair f21 f22) (map_pair p11 p12) (map_pair p21 p22)" - unfolding wpull_def by simp fast + fix R1 R2 S1 S2 + show "prod_rel R1 R2 OO prod_rel S1 S2 \ prod_rel (R1 OO S1) (R2 OO S2)" by auto next fix R S show "prod_rel R S = @@ -202,26 +157,6 @@ by auto qed -(* Categorical version of pullback: *) -lemma wpull_cat: -assumes p: "wpull A B1 B2 f1 f2 p1 p2" -and c: "f1 o q1 = f2 o q2" -and r: "range q1 \ B1" "range q2 \ B2" -obtains h where "range h \ A \ q1 = p1 o h \ q2 = p2 o h" -proof- - have *: "\d. \a \ A. p1 a = q1 d & p2 a = q2 d" - proof safe - fix d - have "f1 (q1 d) = f2 (q2 d)" using c unfolding comp_def[abs_def] by (rule fun_cong) - moreover - have "q1 d : B1" "q2 d : B2" using r unfolding image_def by auto - ultimately show "\a \ A. p1 a = q1 d \ p2 a = q2 d" - using p unfolding wpull_def by auto - qed - then obtain h where "!! d. h d \ A & p1 (h d) = q1 d & p2 (h d) = q2 d" by metis - thus ?thesis using that by fastforce -qed - bnf "'a \ 'b" map: "op \" sets: range @@ -255,16 +190,8 @@ also have "?U \o natLeq +c ?U" by (rule ordLeq_csum2) (rule card_of_Card_order) finally show "|range f| \o natLeq +c ?U" . next - fix A B1 B2 f1 f2 p1 p2 assume p: "wpull A B1 B2 f1 f2 p1 p2" - show "wpull {h. range h \ A} {g1. range g1 \ B1} {g2. range g2 \ B2} - (op \ f1) (op \ f2) (op \ p1) (op \ p2)" - unfolding wpull_def - proof safe - fix g1 g2 assume r: "range g1 \ B1" "range g2 \ B2" - and c: "f1 \ g1 = f2 \ g2" - show "\h \ {h. range h \ A}. p1 \ h = g1 \ p2 \ h = g2" - using wpull_cat[OF p c r] by simp metis - qed + fix R S + show "fun_rel op = R OO fun_rel op = S \ fun_rel op = (R OO S)" by (auto simp: fun_rel_def) next fix R show "fun_rel op = R = diff -r fac0c76bbda2 -r af71b753c459 src/HOL/BNF/Countable_Set_Type.thy --- a/src/HOL/BNF/Countable_Set_Type.thy Fri Dec 20 21:09:01 2013 +0100 +++ b/src/HOL/BNF/Countable_Set_Type.thy Wed Dec 18 11:03:40 2013 +0100 @@ -176,31 +176,9 @@ next fix C show "|rcset C| \o natLeq" by transfer (unfold countable_card_le_natLeq) next - fix A B1 B2 f1 f2 p1 p2 - assume wp: "wpull A B1 B2 f1 f2 p1 p2" - show "wpull {x. rcset x \ A} {x. rcset x \ B1} {x. rcset x \ B2} - (cimage f1) (cimage f2) (cimage p1) (cimage p2)" - unfolding wpull_def proof safe - fix y1 y2 - assume Y1: "rcset y1 \ B1" and Y2: "rcset y2 \ B2" - assume "cimage f1 y1 = cimage f2 y2" - hence EQ: "f1 ` (rcset y1) = f2 ` (rcset y2)" by transfer - with Y1 Y2 obtain X where X: "X \ A" - and Y1: "p1 ` X = rcset y1" and Y2: "p2 ` X = rcset y2" - using wpull_image[OF wp] unfolding wpull_def Pow_def Bex_def mem_Collect_eq - by (auto elim!: allE[of _ "rcset y1"] allE[of _ "rcset y2"]) - have "\ y1' \ rcset y1. \ x. x \ X \ y1' = p1 x" using Y1 by auto - then obtain q1 where q1: "\ y1' \ rcset y1. q1 y1' \ X \ y1' = p1 (q1 y1')" by metis - have "\ y2' \ rcset y2. \ x. x \ X \ y2' = p2 x" using Y2 by auto - then obtain q2 where q2: "\ y2' \ rcset y2. q2 y2' \ X \ y2' = p2 (q2 y2')" by metis - def X' \ "q1 ` (rcset y1) \ q2 ` (rcset y2)" - have X': "X' \ A" and Y1: "p1 ` X' = rcset y1" and Y2: "p2 ` X' = rcset y2" - using X Y1 Y2 q1 q2 unfolding X'_def by fast+ - have fX': "countable X'" unfolding X'_def by simp - then obtain x where X'eq: "X' = rcset x" by transfer blast - show "\x\{x. rcset x \ A}. cimage p1 x = y1 \ cimage p2 x = y2" - using X' Y1 Y2 unfolding X'eq by (intro bexI[of _ "x"]) (transfer, auto) - qed + fix R S + show "cset_rel R OO cset_rel S \ cset_rel (R OO S)" + unfolding cset_rel_def[abs_def] by fast next fix R show "cset_rel R = diff -r fac0c76bbda2 -r af71b753c459 src/HOL/BNF/More_BNFs.thy --- a/src/HOL/BNF/More_BNFs.thy Fri Dec 20 21:09:01 2013 +0100 +++ b/src/HOL/BNF/More_BNFs.thy Wed Dec 18 11:03:40 2013 +0100 @@ -50,18 +50,9 @@ show "|Option.set x| \o natLeq" by (cases x) (simp_all add: ordLess_imp_ordLeq finite_iff_ordLess_natLeq[symmetric]) next - fix A B1 B2 f1 f2 p1 p2 - assume wpull: "wpull A B1 B2 f1 f2 p1 p2" - show "wpull {x. Option.set x \ A} {x. Option.set x \ B1} {x. Option.set x \ B2} - (Option.map f1) (Option.map f2) (Option.map p1) (Option.map p2)" - (is "wpull ?A ?B1 ?B2 ?f1 ?f2 ?p1 ?p2") - unfolding wpull_def - proof (intro strip, elim conjE) - fix b1 b2 - assume "b1 \ ?B1" "b2 \ ?B2" "?f1 b1 = ?f2 b2" - thus "\a \ ?A. ?p1 a = b1 \ ?p2 a = b2" using wpull - unfolding wpull_def by (cases b2) (auto 4 5) - qed + fix R S + show "option_rel R OO option_rel S \ option_rel (R OO S)" + by (auto simp: option_rel_def split: option.splits) next fix z assume "z \ Option.set None" @@ -76,28 +67,6 @@ split: option.splits) qed -lemma wpull_map: - assumes "wpull A B1 B2 f1 f2 p1 p2" - shows "wpull {x. set x \ A} {x. set x \ B1} {x. set x \ B2} (map f1) (map f2) (map p1) (map p2)" - (is "wpull ?A ?B1 ?B2 _ _ _ _") -proof (unfold wpull_def) - { fix as bs assume *: "as \ ?B1" "bs \ ?B2" "map f1 as = map f2 bs" - hence "length as = length bs" by (metis length_map) - hence "\zs \ ?A. map p1 zs = as \ map p2 zs = bs" using * - proof (induct as bs rule: list_induct2) - case (Cons a as b bs) - hence "a \ B1" "b \ B2" "f1 a = f2 b" by auto - with assms obtain z where "z \ A" "p1 z = a" "p2 z = b" unfolding wpull_def by blast - moreover - from Cons obtain zs where "zs \ ?A" "map p1 zs = as" "map p2 zs = bs" by auto - ultimately have "z # zs \ ?A" "map p1 (z # zs) = a # as \ map p2 (z # zs) = b # bs" by auto - thus ?case by (rule_tac x = "z # zs" in bexI) - qed simp - } - thus "\as bs. as \ ?B1 \ bs \ ?B2 \ map f1 as = map f2 bs \ - (\zs \ ?A. map p1 zs = as \ map p2 zs = bs)" by blast -qed - bnf "'a list" map: map sets: set @@ -125,50 +94,21 @@ show "|set x| \o natLeq" by (metis List.finite_set finite_iff_ordLess_natLeq ordLess_imp_ordLeq) next + fix R S + show "list_all2 R OO list_all2 S \ list_all2 (R OO S)" + by (metis list_all2_OO order_refl) +next fix R show "list_all2 R = (Grp {x. set x \ {(x, y). R x y}} (map fst))\\ OO Grp {x. set x \ {(x, y). R x y}} (map snd)" unfolding list_all2_def[abs_def] Grp_def fun_eq_iff relcompp.simps conversep.simps by (force simp: zip_map_fst_snd) -qed (simp add: wpull_map)+ +qed simp_all (* Finite sets *) -lemma wpull_image: - assumes "wpull A B1 B2 f1 f2 p1 p2" - shows "wpull (Pow A) (Pow B1) (Pow B2) (image f1) (image f2) (image p1) (image p2)" -unfolding wpull_def Pow_def Bex_def mem_Collect_eq proof clarify - fix Y1 Y2 assume Y1: "Y1 \ B1" and Y2: "Y2 \ B2" and EQ: "f1 ` Y1 = f2 ` Y2" - def X \ "{a \ A. p1 a \ Y1 \ p2 a \ Y2}" - show "\X\A. p1 ` X = Y1 \ p2 ` X = Y2" - proof (rule exI[of _ X], intro conjI) - show "p1 ` X = Y1" - proof - show "Y1 \ p1 ` X" - proof safe - fix y1 assume y1: "y1 \ Y1" - then obtain y2 where y2: "y2 \ Y2" and eq: "f1 y1 = f2 y2" using EQ by auto - then obtain x where "x \ A" and "p1 x = y1" and "p2 x = y2" - using assms y1 Y1 Y2 unfolding wpull_def by blast - thus "y1 \ p1 ` X" unfolding X_def using y1 y2 by auto - qed - qed(unfold X_def, auto) - show "p2 ` X = Y2" - proof - show "Y2 \ p2 ` X" - proof safe - fix y2 assume y2: "y2 \ Y2" - then obtain y1 where y1: "y1 \ Y1" and eq: "f1 y1 = f2 y2" using EQ by force - then obtain x where "x \ A" and "p1 x = y1" and "p2 x = y2" - using assms y2 Y1 Y2 unfolding wpull_def by blast - thus "y2 \ p2 ` X" unfolding X_def using y1 y2 by auto - qed - qed(unfold X_def, auto) - qed(unfold X_def, auto) -qed - context includes fset.lifting begin @@ -206,31 +146,6 @@ by (transfer, clarsimp, metis fst_conv) qed -lemma wpull_fimage: - assumes "wpull A B1 B2 f1 f2 p1 p2" - shows "wpull {x. fset x \ A} {x. fset x \ B1} {x. fset x \ B2} - (fimage f1) (fimage f2) (fimage p1) (fimage p2)" -unfolding wpull_def Pow_def Bex_def mem_Collect_eq proof clarify - fix y1 y2 - assume Y1: "fset y1 \ B1" and Y2: "fset y2 \ B2" - assume "fimage f1 y1 = fimage f2 y2" - hence EQ: "f1 ` (fset y1) = f2 ` (fset y2)" by transfer simp - with Y1 Y2 obtain X where X: "X \ A" and Y1: "p1 ` X = fset y1" and Y2: "p2 ` X = fset y2" - using wpull_image[OF assms] unfolding wpull_def Pow_def - by (auto elim!: allE[of _ "fset y1"] allE[of _ "fset y2"]) - have "\ y1' \ fset y1. \ x. x \ X \ y1' = p1 x" using Y1 by auto - then obtain q1 where q1: "\ y1' \ fset y1. q1 y1' \ X \ y1' = p1 (q1 y1')" by metis - have "\ y2' \ fset y2. \ x. x \ X \ y2' = p2 x" using Y2 by auto - then obtain q2 where q2: "\ y2' \ fset y2. q2 y2' \ X \ y2' = p2 (q2 y2')" by metis - def X' \ "q1 ` (fset y1) \ q2 ` (fset y2)" - have X': "X' \ A" and Y1: "p1 ` X' = fset y1" and Y2: "p2 ` X' = fset y2" - using X Y1 Y2 q1 q2 unfolding X'_def by auto - have fX': "finite X'" unfolding X'_def by transfer simp - then obtain x where X'eq: "X' = fset x" by transfer simp - show "\x. fset x \ A \ fimage p1 x = y1 \ fimage p2 x = y2" - using X' Y1 Y2 by (auto simp: X'eq intro!: exI[of _ "x"]) (transfer, blast)+ -qed - bnf "'a fset" map: fimage sets: fset @@ -245,7 +160,7 @@ apply (rule natLeq_card_order) apply (rule natLeq_cinfinite) apply transfer apply (metis ordLess_imp_ordLeq finite_iff_ordLess_natLeq) - apply (erule wpull_fimage) + apply (fastforce simp: fset_rel_alt) apply (simp add: Grp_def relcompp.simps conversep.simps fun_eq_iff fset_rel_alt fset_rel_aux) apply transfer apply simp done @@ -550,6 +465,62 @@ show ?thesis unfolding A using finite_cartesian_product[OF assms] by auto qed +(* Weak pullbacks: *) +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))" + +(* 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 blast +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_fstOp_sndOp: +shows "wppull (Collect (split (P OO Q))) (Collect (split P)) (Collect (split Q)) + snd fst fst snd (fstOp P Q) (sndOp P Q)" +using pick_middlep unfolding wppull_def fstOp_def sndOp_def relcompp.simps by auto + lemma wpull_mmap: fixes A :: "'a set" and B1 :: "'b1 set" and B2 :: "'b2 set" assumes wp: "wpull A B1 B2 f1 f2 p1 p2" @@ -781,18 +752,33 @@ by transfer (auto intro!: ordLess_imp_ordLeq simp: finite_iff_ordLess_natLeq[symmetric] multiset_def) +lemma wppull_mmap: + assumes "wppull A B1 B2 f1 f2 e1 e2 p1 p2" + shows "wppull {M. set_of M \ A} {N1. set_of N1 \ B1} {N2. set_of N2 \ B2} + (mmap f1) (mmap f2) (mmap e1) (mmap e2) (mmap p1) (mmap p2)" +proof - + from assms obtain j where j: "\a'\thePull B1 B2 f1 f2. + j a' \ A \ e1 (p1 (j a')) = e1 (fst a') \ e2 (p2 (j a')) = e2 (snd a')" + by (blast dest: wppull_thePull) + then show ?thesis + by (intro wpull_wppull[OF wpull_mmap[OF wpull_thePull], of _ _ _ _ "mmap j"]) + (auto simp: o_eq_dest_lhs[OF mmap_comp[symmetric]] o_eq_dest[OF set_of_mmap] + intro!: mmap_cong simp del: mem_set_of_iff simp: mem_set_of_iff[symmetric]) +qed + bnf "'a multiset" map: mmap sets: set_of bd: natLeq wits: "{#}" by (auto simp add: mmap_id0 mmap_comp set_of_mmap natLeq_card_order natLeq_cinfinite set_of_bd - intro: mmap_cong wpull_mmap) + Grp_def relcompp.simps intro: mmap_cong) + (metis wppull_mmap[OF wppull_fstOp_sndOp, unfolded wppull_def + o_eq_dest_lhs[OF mmap_comp[symmetric]] fstOp_def sndOp_def o_def, simplified]) inductive rel_multiset' where -Zero: "rel_multiset' R {#} {#}" -| -Plus: "\R a b; rel_multiset' R M N\ \ rel_multiset' R (M + {#a#}) (N + {#b#})" + Zero[intro]: "rel_multiset' R {#} {#}" +| Plus[intro]: "\R a b; rel_multiset' R M N\ \ rel_multiset' R (M + {#a#}) (N + {#b#})" lemma map_multiset_Zero_iff[simp]: "mmap f M = {#} \ M = {#}" by (metis image_is_empty multiset.set_map set_of_eq_empty_iff) @@ -998,8 +984,6 @@ (* Advanced relator customization *) (* Set vs. sum relators: *) -(* FIXME: All such facts should be declared as simps: *) -declare sum_rel_simps[simp] lemma set_rel_sum_rel[simp]: "set_rel (sum_rel \ \) A1 A2 \ diff -r fac0c76bbda2 -r af71b753c459 src/HOL/BNF/Tools/bnf_comp.ML --- a/src/HOL/BNF/Tools/bnf_comp.ML Fri Dec 20 21:09:01 2013 +0100 +++ b/src/HOL/BNF/Tools/bnf_comp.ML Wed Dec 18 11:03:40 2013 +0100 @@ -214,8 +214,8 @@ |> Thm.close_derivation end; - fun map_wpull_tac _ = - mk_map_wpull_tac in_alt_thm (map map_wpull_of_bnf inners) (map_wpull_of_bnf outer); + fun le_rel_OO_tac _ = mk_le_rel_OO_tac (le_rel_OO_of_bnf outer) (rel_mono_of_bnf outer) + (map le_rel_OO_of_bnf inners); fun rel_OO_Grp_tac _ = let @@ -234,7 +234,7 @@ end; val tacs = zip_axioms map_id0_tac map_comp0_tac map_cong0_tac set_map0_tacs bd_card_order_tac - bd_cinfinite_tac set_bd_tacs map_wpull_tac rel_OO_Grp_tac; + bd_cinfinite_tac set_bd_tacs le_rel_OO_tac rel_OO_Grp_tac; val outer_wits = mk_wits_of_bnf (replicate onwits oDs) (replicate onwits CAs) outer; @@ -322,7 +322,9 @@ Goal.prove_sorry lthy [] [] goal (K kill_in_alt_tac) |> Thm.close_derivation end; - fun map_wpull_tac _ = mk_map_wpull_tac in_alt_thm [] (map_wpull_of_bnf bnf); + fun le_rel_OO_tac {context = ctxt, prems = _} = + EVERY' [rtac @{thm ord_le_eq_trans}, rtac (le_rel_OO_of_bnf bnf)] 1 THEN + unfold_thms_tac ctxt @{thms eq_OO} THEN rtac refl 1; fun rel_OO_Grp_tac _ = let @@ -340,7 +342,7 @@ end; val tacs = zip_axioms map_id0_tac map_comp0_tac map_cong0_tac set_map0_tacs bd_card_order_tac - bd_cinfinite_tac set_bd_tacs map_wpull_tac rel_OO_Grp_tac; + bd_cinfinite_tac set_bd_tacs le_rel_OO_tac rel_OO_Grp_tac; val bnf_wits = mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf; @@ -420,12 +422,12 @@ Goal.prove_sorry lthy [] [] goal (K lift_in_alt_tac) |> Thm.close_derivation end; - fun map_wpull_tac _ = mk_map_wpull_tac in_alt_thm [] (map_wpull_of_bnf bnf); + fun le_rel_OO_tac _ = rtac (le_rel_OO_of_bnf bnf) 1; fun rel_OO_Grp_tac _ = mk_simple_rel_OO_Grp_tac (rel_OO_Grp_of_bnf bnf) in_alt_thm; val tacs = zip_axioms map_id0_tac map_comp0_tac map_cong0_tac set_map0_tacs bd_card_order_tac - bd_cinfinite_tac set_bd_tacs map_wpull_tac rel_OO_Grp_tac; + bd_cinfinite_tac set_bd_tacs le_rel_OO_tac rel_OO_Grp_tac; val wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf); @@ -493,12 +495,12 @@ |> Thm.close_derivation end; - fun map_wpull_tac _ = mk_map_wpull_tac in_alt_thm [] (map_wpull_of_bnf bnf); + fun le_rel_OO_tac _ = rtac (le_rel_OO_of_bnf bnf) 1; fun rel_OO_Grp_tac _ = mk_simple_rel_OO_Grp_tac (rel_OO_Grp_of_bnf bnf) in_alt_thm; val tacs = zip_axioms map_id0_tac map_comp0_tac map_cong0_tac set_map0_tacs bd_card_order_tac - bd_cinfinite_tac set_bd_tacs map_wpull_tac rel_OO_Grp_tac; + bd_cinfinite_tac set_bd_tacs le_rel_OO_tac rel_OO_Grp_tac; val wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf); @@ -633,7 +635,7 @@ val tacs = zip_axioms (mk_tac (map_id0_of_bnf bnf)) (mk_tac (map_comp0_of_bnf bnf)) (mk_tac (map_cong0_of_bnf bnf)) (map mk_tac (set_map0_of_bnf bnf)) (K (rtac bd_card_order 1)) (K (rtac bd_cinfinite 1)) (map mk_tac set_bds) - (mk_tac (map_wpull_of_bnf bnf)) + (mk_tac (le_rel_OO_of_bnf bnf)) (mk_tac (rel_OO_Grp_of_bnf bnf)); val bnf_wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf); diff -r fac0c76bbda2 -r af71b753c459 src/HOL/BNF/Tools/bnf_comp_tactics.ML --- a/src/HOL/BNF/Tools/bnf_comp_tactics.ML Fri Dec 20 21:09:01 2013 +0100 +++ b/src/HOL/BNF/Tools/bnf_comp_tactics.ML Wed Dec 18 11:03:40 2013 +0100 @@ -31,7 +31,7 @@ val mk_permute_in_alt_tac: ''a list -> ''a list -> tactic - val mk_map_wpull_tac: thm -> thm list -> thm -> tactic + val mk_le_rel_OO_tac: thm -> thm -> thm list -> tactic val mk_simple_rel_OO_Grp_tac: thm -> thm -> tactic val mk_simple_wit_tac: thm list -> tactic end; @@ -241,10 +241,8 @@ mk_rotate_eq_tac (rtac refl) trans @{thm conj_assoc} @{thm conj_commute} @{thm conj_cong} dest src) 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_le_rel_OO_tac outer_le_rel_OO outer_rel_mono inner_le_rel_OOs = + EVERY' (map rtac (@{thm order_trans} :: outer_le_rel_OO :: outer_rel_mono :: inner_le_rel_OOs)) 1; fun mk_simple_rel_OO_Grp_tac rel_OO_Grp in_alt_thm = rtac (trans OF [rel_OO_Grp, in_alt_thm RS @{thm OO_Grp_cong} RS sym]) 1; diff -r fac0c76bbda2 -r af71b753c459 src/HOL/BNF/Tools/bnf_def.ML --- a/src/HOL/BNF/Tools/bnf_def.ML Fri Dec 20 21:09:01 2013 +0100 +++ b/src/HOL/BNF/Tools/bnf_def.ML Wed Dec 18 11:03:40 2013 +0100 @@ -58,8 +58,7 @@ val map_id0_of_bnf: bnf -> thm val map_id_of_bnf: bnf -> thm val map_transfer_of_bnf: bnf -> thm - val map_wppull_of_bnf: bnf -> thm - val map_wpull_of_bnf: bnf -> thm + val le_rel_OO_of_bnf: bnf -> thm val rel_def_of_bnf: bnf -> thm val rel_Grp_of_bnf: bnf -> thm val rel_OO_of_bnf: bnf -> thm @@ -110,6 +109,18 @@ ((thm list -> thm list list) -> thm list list -> Proof.context -> bnf * local_theory) * local_theory * thm list + val define_bnf_consts: const_policy -> fact_policy -> typ list option -> + binding -> binding -> binding list -> + (((((binding * typ) * term) * term list) * term) * term list) * term option -> local_theory -> + ((typ list * typ list * typ list * typ) * + (term * term list * term * (int list * term) list * term) * + (thm * thm list * thm * thm list * thm) * + ((typ list -> typ list -> typ list -> term) * + (typ list -> typ list -> term -> term) * + (typ list -> typ list -> typ -> typ) * + (typ list -> typ list -> typ list -> term) * + (typ list -> typ list -> typ list -> term))) * local_theory + val bnf_def: const_policy -> (Proof.context -> fact_policy) -> (binding -> binding) -> ({prems: thm list, context: Proof.context} -> tactic) list -> ({prems: thm list, context: Proof.context} -> tactic) -> typ list option -> binding -> @@ -135,13 +146,13 @@ bd_card_order: thm, bd_cinfinite: thm, set_bd: thm list, - map_wpull: thm, + le_rel_OO: thm, rel_OO_Grp: thm }; -fun mk_axioms' ((((((((id, comp), cong), map), c_o), cinf), set_bd), wpull), rel) = +fun mk_axioms' ((((((((id, comp), cong), map), c_o), cinf), set_bd), le_rel_OO), rel) = {map_id0 = id, map_comp0 = comp, map_cong0 = cong, set_map0 = map, bd_card_order = c_o, - bd_cinfinite = cinf, set_bd = set_bd, map_wpull = wpull, rel_OO_Grp = rel}; + bd_cinfinite = cinf, set_bd = set_bd, le_rel_OO = le_rel_OO, rel_OO_Grp = rel}; fun dest_cons [] = raise List.Empty | dest_cons (x :: xs) = (x, xs); @@ -159,16 +170,16 @@ ||> the_single |> mk_axioms'; -fun zip_axioms mid mcomp mcong smap bdco bdinf sbd wpull rel = - [mid, mcomp, mcong] @ smap @ [bdco, bdinf] @ sbd @ [wpull, rel]; +fun zip_axioms mid mcomp mcong smap bdco bdinf sbd le_rel_OO rel = + [mid, mcomp, mcong] @ smap @ [bdco, bdinf] @ sbd @ [le_rel_OO, rel]; fun dest_axioms {map_id0, map_comp0, map_cong0, set_map0, bd_card_order, bd_cinfinite, set_bd, - map_wpull, rel_OO_Grp} = - zip_axioms map_id0 map_comp0 map_cong0 set_map0 bd_card_order bd_cinfinite set_bd map_wpull + le_rel_OO, rel_OO_Grp} = + zip_axioms map_id0 map_comp0 map_cong0 set_map0 bd_card_order bd_cinfinite set_bd le_rel_OO rel_OO_Grp; fun map_axioms f {map_id0, map_comp0, map_cong0, set_map0, bd_card_order, bd_cinfinite, set_bd, - map_wpull, rel_OO_Grp} = + le_rel_OO, rel_OO_Grp} = {map_id0 = f map_id0, map_comp0 = f map_comp0, map_cong0 = f map_cong0, @@ -176,7 +187,7 @@ bd_card_order = f bd_card_order, bd_cinfinite = f bd_cinfinite, set_bd = map f set_bd, - map_wpull = f map_wpull, + le_rel_OO = f le_rel_OO, rel_OO_Grp = f rel_OO_Grp}; val morph_axioms = map_axioms o Morphism.thm; @@ -207,7 +218,6 @@ map_cong: thm lazy, map_id: thm lazy, map_transfer: thm lazy, - map_wppull: thm lazy, rel_eq: thm lazy, rel_flip: thm lazy, set_map: thm lazy list, @@ -220,7 +230,7 @@ }; fun mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_map in_bd in_cong in_mono in_rel - map_comp map_cong map_id map_transfer map_wppull rel_eq rel_flip set_map rel_cong rel_mono + map_comp map_cong map_id map_transfer rel_eq rel_flip set_map rel_cong rel_mono rel_mono_strong rel_Grp rel_conversep rel_OO = { bd_Card_order = bd_Card_order, bd_Cinfinite = bd_Cinfinite, @@ -234,7 +244,6 @@ map_cong = map_cong, map_id = map_id, map_transfer = map_transfer, - map_wppull = map_wppull, rel_eq = rel_eq, rel_flip = rel_flip, set_map = set_map, @@ -258,7 +267,6 @@ map_cong, map_id, map_transfer, - map_wppull, rel_eq, rel_flip, set_map, @@ -280,7 +288,6 @@ map_cong = Lazy.map f map_cong, map_id = Lazy.map f map_id, map_transfer = Lazy.map f map_transfer, - map_wppull = Lazy.map f map_wppull, rel_eq = Lazy.map f rel_eq, rel_flip = Lazy.map f rel_flip, set_map = map (Lazy.map f) set_map, @@ -402,8 +409,7 @@ val map_cong0_of_bnf = #map_cong0 o #axioms o rep_bnf; val map_cong_of_bnf = Lazy.force o #map_cong o #facts o rep_bnf; val map_transfer_of_bnf = Lazy.force o #map_transfer o #facts o rep_bnf; -val map_wppull_of_bnf = Lazy.force o #map_wppull o #facts o rep_bnf; -val map_wpull_of_bnf = #map_wpull o #axioms o rep_bnf; +val le_rel_OO_of_bnf = #le_rel_OO o #axioms o rep_bnf; val rel_def_of_bnf = #rel_def o #defs o rep_bnf; val rel_eq_of_bnf = Lazy.force o #rel_eq o #facts o rep_bnf; val rel_flip_of_bnf = Lazy.force o #rel_flip o #facts o rep_bnf; @@ -569,7 +575,6 @@ val map_cong0N = "map_cong0"; val map_congN = "map_cong"; val map_transferN = "map_transfer"; -val map_wpullN = "map_wpull"; val rel_eqN = "rel_eq"; val rel_flipN = "rel_flip"; val set_map0N = "set_map0"; @@ -618,7 +623,6 @@ (map_comp0N, [#map_comp0 axioms]), (map_id0N, [#map_id0 axioms]), (map_transferN, [Lazy.force (#map_transfer facts)]), - (map_wpullN, [#map_wpull axioms]), (rel_mono_strongN, [Lazy.force (#rel_mono_strong facts)]), (set_map0N, #set_map0 axioms), (set_bdN, #set_bd axioms)] @ @@ -660,30 +664,10 @@ (* Define new BNFs *) -fun prepare_def const_policy mk_fact_policy qualify prep_typ prep_term Ds_opt map_b rel_b set_bs - ((((((raw_bnf_b, raw_bnf_T), raw_map), raw_sets), raw_bd), raw_wits), raw_rel_opt) - no_defs_lthy = +fun define_bnf_consts const_policy fact_policy Ds_opt map_b rel_b set_bs + ((((((bnf_b, T_rhs), map_rhs), set_rhss), bd_rhs), wit_rhss), rel_rhs_opt) no_defs_lthy = let - val fact_policy = mk_fact_policy no_defs_lthy; - val bnf_b = qualify raw_bnf_b; - val live = length raw_sets; - - val T_rhs = prep_typ no_defs_lthy raw_bnf_T; - val map_rhs = prep_term no_defs_lthy raw_map; - val set_rhss = map (prep_term no_defs_lthy) raw_sets; - val bd_rhs = prep_term no_defs_lthy raw_bd; - - fun err T = - error ("Trying to register the type " ^ quote (Syntax.string_of_typ no_defs_lthy T) ^ - " as unnamed BNF"); - - val (bnf_b, key) = - if Binding.eq_name (bnf_b, Binding.empty) then - (case T_rhs of - Type (C, Ts) => if forall (can dest_TFree) Ts - then (Binding.qualified_name C, C) else err T_rhs - | T => err T) - else (bnf_b, Local_Theory.full_name no_defs_lthy bnf_b); + val live = length set_rhss; val def_qualify = Binding.conceal o Binding.qualify false (Binding.name_of bnf_b); @@ -736,6 +720,7 @@ val phi = Proof_Context.export_morphism lthy_old lthy; + val bnf_map_def = Morphism.thm phi raw_map_def; val bnf_set_defs = map (Morphism.thm phi) raw_set_defs; val bnf_bd_def = Morphism.thm phi raw_bd_def; @@ -744,57 +729,162 @@ (*TODO: handle errors*) (*simple shape analysis of a map function*) - val ((alphas, betas), (CA, _)) = + val ((alphas, betas), (Calpha, _)) = fastype_of bnf_map |> strip_typeN live |>> map_split dest_funT ||> dest_funT handle TYPE _ => error "Bad map function"; - val CA_params = map TVar (Term.add_tvarsT CA []); + val Calpha_params = map TVar (Term.add_tvarsT Calpha []); val bnf_T = Morphism.typ phi T_rhs; val bad_args = Term.add_tfreesT bnf_T []; val _ = if null bad_args then () else error ("Locally fixed type arguments " ^ commas_quote (map (Syntax.string_of_typ no_defs_lthy o TFree) bad_args)); - val bnf_sets = map2 (normalize_set CA_params) alphas (map (Morphism.term phi) bnf_set_terms); + val bnf_sets = + map2 (normalize_set Calpha_params) alphas (map (Morphism.term phi) bnf_set_terms); val bnf_bd = - Term.subst_TVars (Term.add_tvar_namesT bnf_T [] ~~ CA_params) (Morphism.term phi bnf_bd_term); + Term.subst_TVars (Term.add_tvar_namesT bnf_T [] ~~ Calpha_params) + (Morphism.term phi bnf_bd_term); (*TODO: assert Ds = (TVars of bnf_map) \ (alphas @ betas) as sets*) val deads = (case Ds_opt of NONE => subtract (op =) (alphas @ betas) (map TVar (Term.add_tvars bnf_map [])) | SOME Ds => map (Morphism.typ phi) Ds); - val dead = length deads; (*TODO: further checks of type of bnf_map*) (*TODO: check types of bnf_sets*) (*TODO: check type of bnf_bd*) (*TODO: check type of bnf_rel*) - val ((((((((((As', Bs'), Cs), Ds), B1Ts), B2Ts), domTs), ranTs), ranTs'), ranTs''), - (Ts, T)) = lthy + fun mk_bnf_map Ds As' Bs' = + Term.subst_atomic_types ((deads ~~ Ds) @ (alphas ~~ As') @ (betas ~~ Bs')) bnf_map; + fun mk_bnf_t Ds As' = Term.subst_atomic_types ((deads ~~ Ds) @ (alphas ~~ As')); + fun mk_bnf_T Ds As' = Term.typ_subst_atomic ((deads ~~ Ds) @ (alphas ~~ As')); + + val (((As, Bs), Ds), names_lthy) = lthy + |> mk_TFrees live + ||>> mk_TFrees live + ||>> mk_TFrees (length deads); + val RTs = map2 (curry HOLogic.mk_prodT) As Bs; + val pred2RTs = map2 mk_pred2T As Bs; + val (Rs, Rs') = names_lthy |> mk_Frees' "R" pred2RTs |> fst + val CA = mk_bnf_T Ds As Calpha; + val CR = mk_bnf_T Ds RTs Calpha; + val setRs = + map3 (fn R => fn T => fn U => + HOLogic.Collect_const (HOLogic.mk_prodT (T, U)) $ HOLogic.mk_split R) Rs As Bs; + + (*Grp (in (Collect (split R1) .. Collect (split Rn))) (map fst .. fst)^--1 OO + Grp (in (Collect (split R1) .. Collect (split Rn))) (map snd .. snd)*) + val OO_Grp = + let + val map1 = Term.list_comb (mk_bnf_map Ds RTs As, map fst_const RTs); + val map2 = Term.list_comb (mk_bnf_map Ds RTs Bs, map snd_const RTs); + val bnf_in = mk_in setRs (map (mk_bnf_t Ds RTs) bnf_sets) CR; + in + mk_rel_compp (mk_conversep (mk_Grp bnf_in map1), mk_Grp bnf_in map2) + |> fold_rev Term.absfree Rs' + end; + + val rel_rhs = the_default OO_Grp rel_rhs_opt; + + val rel_bind_def = + (fn () => def_qualify (if Binding.is_empty rel_b then mk_prefix_binding relN else rel_b), + rel_rhs); + + val wit_rhss = + if null wit_rhss then + [fold_rev Term.absdummy As (Term.list_comb (mk_bnf_map Ds As As, + map2 (fn T => fn i => Term.absdummy T (Bound i)) As (live downto 1)) $ + Const (@{const_name undefined}, CA))] + else wit_rhss; + val nwits = length wit_rhss; + val wit_binds_defs = + let + val bs = if nwits = 1 then [fn () => def_qualify (mk_prefix_binding witN)] + else map (fn i => fn () => def_qualify (mk_prefix_binding (mk_witN i))) (1 upto nwits); + in bs ~~ wit_rhss end; + + val (((bnf_rel_term, raw_rel_def), (bnf_wit_terms, raw_wit_defs)), (lthy, lthy_old)) = + lthy + |> maybe_define (is_some rel_rhs_opt) rel_bind_def + ||>> apfst split_list o fold_map (maybe_define (not (null wit_rhss))) wit_binds_defs + ||> `(maybe_restore lthy); + + val phi = Proof_Context.export_morphism lthy_old lthy; + val bnf_rel_def = Morphism.thm phi raw_rel_def; + val bnf_rel = Morphism.term phi bnf_rel_term; + fun mk_bnf_rel Ds As' Bs' = + normalize_rel lthy (map2 mk_pred2T As' Bs') (mk_bnf_T Ds As' Calpha) (mk_bnf_T Ds Bs' Calpha) + bnf_rel; + + val bnf_wit_defs = map (Morphism.thm phi) raw_wit_defs; + val bnf_wits = + map (normalize_wit Calpha_params Calpha alphas o Morphism.term phi) bnf_wit_terms; + + fun mk_OO_Grp Ds' As' Bs' = + Term.subst_atomic_types ((Ds ~~ Ds') @ (As ~~ As') @ (Bs ~~ Bs')) OO_Grp; + in + (((alphas, betas, deads, Calpha), + (bnf_map, bnf_sets, bnf_bd, bnf_wits, bnf_rel), + (bnf_map_def, bnf_set_defs, bnf_bd_def, bnf_wit_defs, bnf_rel_def), + (mk_bnf_map, mk_bnf_t, mk_bnf_T, mk_bnf_rel, mk_OO_Grp)), lthy) + end; + +fun prepare_def const_policy mk_fact_policy qualify prep_typ prep_term Ds_opt map_b rel_b set_bs + ((((((raw_bnf_b, raw_bnf_T), raw_map), raw_sets), raw_bd), raw_wits), raw_rel_opt) + no_defs_lthy = + let + val fact_policy = mk_fact_policy no_defs_lthy; + val bnf_b = qualify raw_bnf_b; + val live = length raw_sets; + + val T_rhs = prep_typ no_defs_lthy raw_bnf_T; + val map_rhs = prep_term no_defs_lthy raw_map; + val set_rhss = map (prep_term no_defs_lthy) raw_sets; + val bd_rhs = prep_term no_defs_lthy raw_bd; + val wit_rhss = map (prep_term no_defs_lthy) raw_wits; + val rel_rhs_opt = Option.map (prep_term no_defs_lthy) raw_rel_opt; + + fun err T = + error ("Trying to register the type " ^ quote (Syntax.string_of_typ no_defs_lthy T) ^ + " as unnamed BNF"); + + val (bnf_b, key) = + if Binding.eq_name (bnf_b, Binding.empty) then + (case T_rhs of + Type (C, Ts) => if forall (can dest_TFree) Ts + then (Binding.qualified_name C, C) else err T_rhs + | T => err T) + else (bnf_b, Local_Theory.full_name no_defs_lthy bnf_b); + + val (((alphas, betas, deads, Calpha), + (bnf_map, bnf_sets, bnf_bd, bnf_wits, bnf_rel), + (bnf_map_def, bnf_set_defs, bnf_bd_def, bnf_wit_defs, bnf_rel_def), + (mk_bnf_map_Ds, mk_bnf_t_Ds, mk_bnf_T_Ds, _, mk_OO_Grp)), lthy) = + define_bnf_consts const_policy fact_policy Ds_opt map_b rel_b set_bs + ((((((bnf_b, T_rhs), map_rhs), set_rhss), bd_rhs), wit_rhss), rel_rhs_opt) no_defs_lthy; + + val dead = length deads; + + val ((((((As', Bs'), Cs), Ds), B1Ts), B2Ts), (Ts, T)) = lthy |> mk_TFrees live ||>> mk_TFrees live ||>> mk_TFrees live ||>> mk_TFrees dead ||>> mk_TFrees live ||>> mk_TFrees live - ||>> mk_TFrees live - ||>> mk_TFrees live - ||>> mk_TFrees live - ||>> mk_TFrees live ||> fst o mk_TFrees 1 ||> the_single ||> `(replicate live); - fun mk_bnf_map As' Bs' = - Term.subst_atomic_types ((deads ~~ Ds) @ (alphas ~~ As') @ (betas ~~ Bs')) bnf_map; - fun mk_bnf_t As' = Term.subst_atomic_types ((deads ~~ Ds) @ (alphas ~~ As')); - fun mk_bnf_T As' = Term.typ_subst_atomic ((deads ~~ Ds) @ (alphas ~~ As')); + val mk_bnf_map = mk_bnf_map_Ds Ds; + val mk_bnf_t = mk_bnf_t_Ds Ds; + val mk_bnf_T = mk_bnf_T_Ds Ds; - val RTs = map HOLogic.mk_prodT (As' ~~ Bs'); val pred2RTs = map2 mk_pred2T As' Bs'; val pred2RTsAsCs = map2 mk_pred2T As' Cs; val pred2RTsBsCs = map2 mk_pred2T Bs' Cs; @@ -803,12 +893,11 @@ val transfer_domRTs = map2 mk_pred2T As' B1Ts; val transfer_ranRTs = map2 mk_pred2T Bs' B2Ts; - val CA' = mk_bnf_T As' CA; - val CB' = mk_bnf_T Bs' CA; - val CC' = mk_bnf_T Cs CA; - val CRs' = mk_bnf_T RTs CA; - val CB1 = mk_bnf_T B1Ts CA; - val CB2 = mk_bnf_T B2Ts CA; + val CA' = mk_bnf_T As' Calpha; + val CB' = mk_bnf_T Bs' Calpha; + val CC' = mk_bnf_T Cs Calpha; + val CB1 = mk_bnf_T B1Ts Calpha; + val CB2 = mk_bnf_T B2Ts Calpha; val bnf_map_AsAs = mk_bnf_map As' As'; val bnf_map_AsBs = mk_bnf_map As' Bs'; @@ -817,10 +906,11 @@ val bnf_sets_As = map (mk_bnf_t As') bnf_sets; val bnf_sets_Bs = map (mk_bnf_t Bs') bnf_sets; val bnf_bd_As = mk_bnf_t As' bnf_bd; + fun mk_bnf_rel RTs CA CB = normalize_rel lthy RTs CA CB bnf_rel; val pre_names_lthy = lthy; - val ((((((((((((((((((((((((fs, gs), hs), x), y), zs), ys), As), - As_copy), Xs), B1s), B2s), f1s), f2s), e1s), e2s), p1s), p2s), bs), (Rs, Rs')), Rs_copy), Ss), + val (((((((((((((((fs, gs), hs), x), y), zs), ys), As), + As_copy), bs), Rs), Rs_copy), Ss), transfer_domRs), transfer_ranRs), names_lthy) = pre_names_lthy |> mk_Frees "f" (map2 (curry op -->) As' Bs') ||>> mk_Frees "g" (map2 (curry op -->) Bs' Cs) @@ -831,17 +921,8 @@ ||>> mk_Frees "y" Bs' ||>> mk_Frees "A" (map HOLogic.mk_setT As') ||>> mk_Frees "A" (map HOLogic.mk_setT As') - ||>> mk_Frees "A" (map HOLogic.mk_setT domTs) - ||>> mk_Frees "B1" (map HOLogic.mk_setT B1Ts) - ||>> mk_Frees "B2" (map HOLogic.mk_setT B2Ts) - ||>> mk_Frees "f1" (map2 (curry op -->) B1Ts ranTs) - ||>> mk_Frees "f2" (map2 (curry op -->) B2Ts ranTs) - ||>> mk_Frees "e1" (map2 (curry op -->) B1Ts ranTs') - ||>> mk_Frees "e2" (map2 (curry op -->) B2Ts ranTs'') - ||>> mk_Frees "p1" (map2 (curry op -->) domTs B1Ts) - ||>> mk_Frees "p2" (map2 (curry op -->) domTs B2Ts) ||>> mk_Frees "b" As' - ||>> mk_Frees' "R" pred2RTs + ||>> mk_Frees "R" pred2RTs ||>> mk_Frees "R" pred2RTs ||>> mk_Frees "S" pred2RTsBsCs ||>> mk_Frees "R" transfer_domRTs @@ -850,59 +931,8 @@ val fs_copy = map2 (retype_free o fastype_of) fs gs; val x_copy = retype_free CA' y; - val setRs = - map3 (fn R => fn T => fn U => - HOLogic.Collect_const (HOLogic.mk_prodT (T, U)) $ HOLogic.mk_split R) Rs As' Bs'; - - (*Grp (in (Collect (split R1) .. Collect (split Rn))) (map fst .. fst)^--1 OO - Grp (in (Collect (split R1) .. Collect (split Rn))) (map snd .. snd)*) - val OO_Grp = - let - val map1 = Term.list_comb (mk_bnf_map RTs As', map fst_const RTs); - val map2 = Term.list_comb (mk_bnf_map RTs Bs', map snd_const RTs); - val bnf_in = mk_in setRs (map (mk_bnf_t RTs) bnf_sets) CRs'; - in - mk_rel_compp (mk_conversep (mk_Grp bnf_in map1), mk_Grp bnf_in map2) - end; - - val rel_rhs = (case raw_rel_opt of - NONE => fold_rev Term.absfree Rs' OO_Grp - | SOME raw_rel => prep_term no_defs_lthy raw_rel); - - val rel_bind_def = - (fn () => def_qualify (if Binding.is_empty rel_b then mk_prefix_binding relN else rel_b), - rel_rhs); - - val wit_rhss = - if null raw_wits then - [fold_rev Term.absdummy As' (Term.list_comb (bnf_map_AsAs, - map2 (fn T => fn i => Term.absdummy T (Bound i)) As' (live downto 1)) $ - Const (@{const_name undefined}, CA'))] - else map (prep_term no_defs_lthy) raw_wits; - val nwits = length wit_rhss; - val wit_binds_defs = - let - val bs = if nwits = 1 then [fn () => def_qualify (mk_prefix_binding witN)] - else map (fn i => fn () => def_qualify (mk_prefix_binding (mk_witN i))) (1 upto nwits); - in bs ~~ wit_rhss end; - - val (((bnf_rel_term, raw_rel_def), (bnf_wit_terms, raw_wit_defs)), (lthy, lthy_old)) = - lthy - |> maybe_define (is_some raw_rel_opt) rel_bind_def - ||>> apfst split_list o fold_map (maybe_define (not (null raw_wits))) wit_binds_defs - ||> `(maybe_restore lthy); - - val phi = Proof_Context.export_morphism lthy_old lthy; - val bnf_rel_def = Morphism.thm phi raw_rel_def; - val bnf_rel = Morphism.term phi bnf_rel_term; - - fun mk_bnf_rel RTs CA' CB' = normalize_rel lthy RTs CA' CB' bnf_rel; - val rel = mk_bnf_rel pred2RTs CA' CB'; val relAsAs = mk_bnf_rel self_pred2RTs CA' CA'; - - val bnf_wit_defs = map (Morphism.thm phi) raw_wit_defs; - val bnf_wits = map (normalize_wit CA_params CA alphas o Morphism.term phi) bnf_wit_terms; val bnf_wit_As = map (apsnd (mk_bnf_t As')) bnf_wits; val map_id0_goal = @@ -959,31 +989,18 @@ map mk_goal bnf_sets_As end; - val map_wpull_goal = - let - val prems = map HOLogic.mk_Trueprop - (map8 mk_wpull Xs B1s B2s f1s f2s (replicate live NONE) p1s p2s); - val CX = mk_bnf_T domTs CA; - val bnf_sets_CX = map2 (normalize_set (map (mk_bnf_T domTs) CA_params)) domTs bnf_sets; - val bnf_sets_CB1 = map2 (normalize_set (map (mk_bnf_T B1Ts) CA_params)) B1Ts bnf_sets; - val bnf_sets_CB2 = map2 (normalize_set (map (mk_bnf_T B2Ts) CA_params)) B2Ts bnf_sets; - val bnf_map_app_f1 = Term.list_comb (mk_bnf_map B1Ts ranTs, f1s); - val bnf_map_app_f2 = Term.list_comb (mk_bnf_map B2Ts ranTs, f2s); - val bnf_map_app_p1 = Term.list_comb (mk_bnf_map domTs B1Ts, p1s); - val bnf_map_app_p2 = Term.list_comb (mk_bnf_map domTs B2Ts, p2s); + val relAsCs = mk_bnf_rel pred2RTsAsCs CA' CC'; + val relBsCs = mk_bnf_rel pred2RTsBsCs CB' CC'; + val rel_OO_lhs = Term.list_comb (relAsCs, map2 (curry mk_rel_compp) Rs Ss); + val rel_OO_rhs = mk_rel_compp (Term.list_comb (rel, Rs), Term.list_comb (relBsCs, Ss)); + val le_rel_OO_goal = + fold_rev Logic.all (Rs @ Ss) (HOLogic.mk_Trueprop (mk_leq rel_OO_rhs rel_OO_lhs)); - val map_wpull = mk_wpull (mk_in Xs bnf_sets_CX CX) - (mk_in B1s bnf_sets_CB1 CB1) (mk_in B2s bnf_sets_CB2 CB2) - bnf_map_app_f1 bnf_map_app_f2 NONE bnf_map_app_p1 bnf_map_app_p2; - in - fold_rev Logic.all (Xs @ B1s @ B2s @ f1s @ f2s @ p1s @ p2s) - (Logic.list_implies (prems, HOLogic.mk_Trueprop map_wpull)) - end; - - val rel_OO_Grp_goal = fold_rev Logic.all Rs (mk_Trueprop_eq (Term.list_comb (rel, Rs), OO_Grp)); + val rel_OO_Grp_goal = fold_rev Logic.all Rs (mk_Trueprop_eq (Term.list_comb (rel, Rs), + Term.list_comb (mk_OO_Grp Ds As' Bs', Rs))); val goals = zip_axioms map_id0_goal map_comp0_goal map_cong0_goal set_map0s_goal - card_order_bd_goal cinfinite_bd_goal set_bds_goal map_wpull_goal rel_OO_Grp_goal; + card_order_bd_goal cinfinite_bd_goal set_bds_goal le_rel_OO_goal rel_OO_Grp_goal; fun mk_wit_goals (I, wit) = let @@ -1018,7 +1035,7 @@ fun mk_collect_set_map () = let - val defT = mk_bnf_T Ts CA --> HOLogic.mk_setT T; + val defT = mk_bnf_T Ts Calpha --> HOLogic.mk_setT T; val collect_map = HOLogic.mk_comp (mk_collect (map (mk_bnf_t Ts) bnf_sets) defT, Term.list_comb (mk_bnf_map As' Ts, hs)); @@ -1090,12 +1107,12 @@ let val bdT = fst (dest_relT (fastype_of bnf_bd_As)); val bdTs = replicate live bdT; - val bd_bnfT = mk_bnf_T bdTs CA; + val bd_bnfT = mk_bnf_T bdTs Calpha; val surj_imp_ordLeq_inst = (if live = 0 then TrueI else let val ranTs = map (fn AT => mk_sumT (AT, HOLogic.unitT)) As'; val funTs = map (fn T => bdT --> T) ranTs; - val ran_bnfT = mk_bnf_T ranTs CA; + val ran_bnfT = mk_bnf_T ranTs Calpha; val (revTs, Ts) = `rev (bd_bnfT :: funTs); val cTs = map (SOME o certifyT lthy) [ran_bnfT, Library.foldr1 HOLogic.mk_prodT Ts]; val tinst = fold (fn T => fn t => HOLogic.mk_split (Term.absdummy T t)) (tl revTs) @@ -1123,42 +1140,6 @@ val in_bd = Lazy.lazy mk_in_bd; - fun mk_map_wppull () = - let - val prems = if live = 0 then [] else - [HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj - (map8 mk_wpull Xs B1s B2s f1s f2s (map SOME (e1s ~~ e2s)) p1s p2s))]; - val CX = mk_bnf_T domTs CA; - val bnf_sets_CX = - map2 (normalize_set (map (mk_bnf_T domTs) CA_params)) domTs bnf_sets; - val bnf_sets_CB1 = - map2 (normalize_set (map (mk_bnf_T B1Ts) CA_params)) B1Ts bnf_sets; - val bnf_sets_CB2 = - map2 (normalize_set (map (mk_bnf_T B2Ts) CA_params)) B2Ts bnf_sets; - val bnf_map_app_f1 = Term.list_comb (mk_bnf_map B1Ts ranTs, f1s); - val bnf_map_app_f2 = Term.list_comb (mk_bnf_map B2Ts ranTs, f2s); - val bnf_map_app_e1 = Term.list_comb (mk_bnf_map B1Ts ranTs', e1s); - val bnf_map_app_e2 = Term.list_comb (mk_bnf_map B2Ts ranTs'', e2s); - val bnf_map_app_p1 = Term.list_comb (mk_bnf_map domTs B1Ts, p1s); - val bnf_map_app_p2 = Term.list_comb (mk_bnf_map domTs B2Ts, p2s); - - val concl = mk_wpull (mk_in Xs bnf_sets_CX CX) - (mk_in B1s bnf_sets_CB1 CB1) (mk_in B2s bnf_sets_CB2 CB2) - bnf_map_app_f1 bnf_map_app_f2 (SOME (bnf_map_app_e1, bnf_map_app_e2)) - bnf_map_app_p1 bnf_map_app_p2; - - val goal = - fold_rev Logic.all (Xs @ B1s @ B2s @ f1s @ f2s @ e1s @ e2s @ p1s @ p2s) - (Logic.list_implies (prems, HOLogic.mk_Trueprop concl)) - in - Goal.prove_sorry lthy [] [] goal - (fn _ => mk_map_wppull_tac (#map_id0 axioms) (#map_cong0 axioms) - (#map_wpull axioms) (Lazy.force map_comp) (map Lazy.force set_map)) - |> Thm.close_derivation - end; - - val map_wppull = Lazy.lazy mk_map_wppull; - val rel_OO_Grp = #rel_OO_Grp axioms; val rel_OO_Grps = no_refl [rel_OO_Grp]; @@ -1234,18 +1215,12 @@ val rel_conversep = Lazy.lazy mk_rel_conversep; fun mk_rel_OO () = - let - val relAsCs = mk_bnf_rel pred2RTsAsCs CA' CC'; - val relBsCs = mk_bnf_rel pred2RTsBsCs CB' CC'; - val lhs = Term.list_comb (relAsCs, map2 (curry mk_rel_compp) Rs Ss); - val rhs = mk_rel_compp (Term.list_comb (rel, Rs), Term.list_comb (relBsCs, Ss)); - val goal = fold_rev Logic.all (Rs @ Ss) (mk_Trueprop_eq (lhs, rhs)); - in - Goal.prove_sorry lthy [] [] goal - (mk_rel_OO_tac rel_OO_Grps (Lazy.force rel_eq) (#map_cong0 axioms) - (Lazy.force map_wppull) (Lazy.force map_comp) (map Lazy.force set_map)) - |> Thm.close_derivation - end; + Goal.prove_sorry lthy [] [] + (fold_rev Logic.all (Rs @ Ss) (HOLogic.mk_Trueprop (mk_leq rel_OO_lhs rel_OO_rhs))) + (mk_rel_OO_le_tac rel_OO_Grps (Lazy.force rel_eq) (#map_cong0 axioms) + (Lazy.force map_comp) (map Lazy.force set_map)) + |> Thm.close_derivation + |> (fn thm => @{thm antisym} OF [thm, #le_rel_OO axioms]); val rel_OO = Lazy.lazy mk_rel_OO; @@ -1305,7 +1280,7 @@ val defs = mk_defs bnf_map_def bnf_set_defs bnf_rel_def; val facts = mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_map in_bd in_cong - in_mono in_rel map_comp map_cong map_id map_transfer map_wppull rel_eq rel_flip set_map + in_mono in_rel map_comp map_cong map_id map_transfer rel_eq rel_flip set_map rel_cong rel_mono rel_mono_strong rel_Grp rel_conversep rel_OO; val wits = map2 mk_witness bnf_wits wit_thms; @@ -1313,8 +1288,8 @@ val bnf_rel = Term.subst_atomic_types ((Ds ~~ deads) @ (As' ~~ alphas) @ (Bs' ~~ betas)) rel; - val bnf = mk_bnf bnf_b CA live alphas betas dead deads bnf_map bnf_sets bnf_bd axioms defs - facts wits bnf_rel; + val bnf = mk_bnf bnf_b Calpha live alphas betas dead deads bnf_map bnf_sets bnf_bd axioms + defs facts wits bnf_rel; in (bnf, lthy |> note_bnf_thms fact_policy qualify bnf_b bnf) end; @@ -1336,7 +1311,8 @@ K (TRYALL Goal.conjunction_tac) THEN' (case triv_tac_opt of SOME tac => tac set_maps - | NONE => mk_unfold_thms_then_tac lthy one_step_defs wit_tac); + | NONE => fn {context = ctxt, prems} => + unfold_thms_tac ctxt one_step_defs THEN wit_tac {context = ctxt, prems = prems}); val wit_goals = map Logic.mk_conjunction_balanced wit_goalss; fun mk_wit_thms set_maps = Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced wit_goals) (mk_wits_tac set_maps) @@ -1345,7 +1321,8 @@ |> map (map (Thm.close_derivation o Thm.forall_elim_vars 0)); in map2 (Thm.close_derivation oo Goal.prove_sorry lthy [] []) - goals (map (mk_unfold_thms_then_tac lthy one_step_defs) tacs) + goals (map (fn tac => fn {context = ctxt, prems} => + unfold_thms_tac ctxt one_step_defs THEN tac {context = ctxt, prems = prems}) tacs) |> (fn thms => after_qed mk_wit_thms (map single thms) lthy) end) oo prepare_def const_policy fact_policy qualify (K I) (K I) Ds map_b rel_b set_bs; diff -r fac0c76bbda2 -r af71b753c459 src/HOL/BNF/Tools/bnf_def_tactics.ML --- a/src/HOL/BNF/Tools/bnf_def_tactics.ML Fri Dec 20 21:09:01 2013 +0100 +++ b/src/HOL/BNF/Tools/bnf_def_tactics.ML Wed Dec 18 11:03:40 2013 +0100 @@ -13,13 +13,12 @@ val mk_map_comp: thm -> thm val mk_map_cong_tac: Proof.context -> thm -> tactic val mk_in_mono_tac: int -> tactic - val mk_map_wppull_tac: thm -> thm -> thm -> thm -> thm list -> tactic val mk_set_map: thm -> thm val mk_rel_Grp_tac: thm list -> thm -> thm -> thm -> thm -> thm list -> {prems: thm list, context: Proof.context} -> tactic val mk_rel_eq_tac: int -> thm -> thm -> thm -> tactic - val mk_rel_OO_tac: thm list -> thm -> thm -> thm -> thm -> thm list -> + val mk_rel_OO_le_tac: thm list -> thm -> thm -> thm -> thm list -> {prems: thm list, context: Proof.context} -> tactic val mk_rel_conversep_tac: thm -> thm -> tactic val mk_rel_conversep_le_tac: thm list -> thm -> thm -> thm -> thm list -> @@ -68,22 +67,6 @@ rtac set_map0) set_map0s) THEN' rtac @{thm image_empty}) 1; -fun mk_map_wppull_tac map_id0 map_cong0 map_wpull map_comp set_maps = - if null set_maps then - EVERY' [rtac @{thm wppull_id}, rtac map_wpull, rtac map_id0, rtac map_id0] 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 ord_eq_le_trans), - rtac @{thm image_subsetI}, rtac conjunct1, etac bspec, etac set_mp, atac]) - set_maps, - CONJ_WRAP' (fn thm => EVERY' [rtac (map_comp RS trans), rtac (map_comp RS trans), - rtac (map_comp RS trans RS sym), rtac map_cong0, - REPEAT_DETERM_N (length set_maps) 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_Grp_tac rel_OO_Grps map_id0 map_cong0 map_id map_comp set_maps {context = ctxt, prems = _} = let @@ -163,7 +146,7 @@ rtac le_conversep, rtac @{thm iffD2[OF conversep_mono]}, rtac rel_mono, REPEAT_DETERM o rtac @{thm eq_refl[OF sym[OF conversep_conversep]]}] 1; -fun mk_rel_OO_tac rel_OO_Grps rel_eq map_cong0 map_wppull map_comp set_maps +fun mk_rel_OO_le_tac rel_OO_Grps rel_eq map_cong0 map_comp set_maps {context = ctxt, prems = _} = let val n = length set_maps; @@ -171,13 +154,13 @@ CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS ord_eq_le_trans), rtac @{thm image_subsetI}, rtac nthO_in, etac set_mp, atac]) set_maps; val rel_OO_Grps_tac = if null rel_OO_Grps then K all_tac - else rtac (hd rel_OO_Grps RS trans) THEN' + else rtac (hd rel_OO_Grps RS ord_eq_le_trans) THEN' rtac (@{thm arg_cong2[of _ _ _ _ "op OO"]} OF (replicate 2 (hd rel_OO_Grps RS sym)) RSN - (2, trans)); + (2, ord_le_eq_trans)); in - if null set_maps then rtac (rel_eq RS @{thm eq_OOI}) 1 + if null set_maps then rtac (rel_eq RS @{thm leq_OOI}) 1 else - EVERY' [rel_OO_Grps_tac, rtac @{thm antisym}, rtac @{thm predicate2I}, + EVERY' [rel_OO_Grps_tac, rtac @{thm predicate2I}, REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm GrpE}, @{thm relcomppE}, @{thm conversepE}], hyp_subst_tac ctxt, @@ -197,18 +180,7 @@ in_tac @{thm sndOp_in}, rtac @{thm GrpI}, rtac trans, rtac map_comp, rtac sym, rtac map_cong0, REPEAT_DETERM_N n o rtac @{thm snd_sndOp}, - in_tac @{thm sndOp_in}, - rtac @{thm predicate2I}, - REPEAT_DETERM o eresolve_tac [@{thm relcomppE}, @{thm conversepE}, @{thm GrpE}], - hyp_subst_tac ctxt, - rtac allE, rtac subst, rtac @{thm wppull_def}, rtac map_wppull, - CONJ_WRAP' (K (rtac @{thm wppull_fstOp_sndOp})) set_maps, - etac allE, etac impE, etac conjI, etac conjI, etac sym, - REPEAT_DETERM o eresolve_tac [bexE, conjE], - rtac @{thm relcomppI}, rtac @{thm conversepI}, - EVERY' (map (fn thm => EVERY' [rtac @{thm GrpI}, rtac trans, - rtac trans, rtac map_cong0, REPEAT_DETERM_N n o rtac thm, - rtac (map_comp RS sym), atac, atac]) [@{thm fst_fstOp}, @{thm snd_sndOp}])] 1 + in_tac @{thm sndOp_in}] 1 end; fun mk_rel_mono_strong_tac in_rel set_maps {context = ctxt, prems = _} = diff -r fac0c76bbda2 -r af71b753c459 src/HOL/BNF/Tools/bnf_gfp.ML --- a/src/HOL/BNF/Tools/bnf_gfp.ML Fri Dec 20 21:09:01 2013 +0100 +++ b/src/HOL/BNF/Tools/bnf_gfp.ML Wed Dec 18 11:03:40 2013 +0100 @@ -85,16 +85,13 @@ val passives = map fst (subtract (op = o apsnd TFree) deads resBs); (* tvars *) - val ((((((((passiveAs, activeAs), passiveBs), activeBs), passiveCs), activeCs), passiveXs), - passiveYs), idxT) = names_lthy + val ((((((passiveAs, activeAs), passiveBs), activeBs), passiveCs), activeCs), idxT) = names_lthy |> variant_tfrees passives ||>> mk_TFrees n ||>> variant_tfrees passives ||>> mk_TFrees n ||>> mk_TFrees m ||>> mk_TFrees n - ||>> mk_TFrees m - ||>> mk_TFrees m ||> fst o mk_TFrees 1 ||> the_single; @@ -168,14 +165,15 @@ val hrecTs = map fastype_of Zeros; val hsetTs = map (fn hrecT => Library.foldr (op -->) (sTs, HOLogic.natT --> hrecT)) hrecTs; - val ((((((((((((((((((((((((((((((((((zs, zs'), zs_copy), zs_copy2), - z's), As), Bs), Bs_copy), B's), B''s), ss), sum_ss), s's), s''s), fs), fs_copy), + val (((((((((((((((((((((((((((((((((((zs, zs'), zs_copy), zs_copy2), z's), (ys, ys')), + As), Bs), Bs_copy), B's), B''s), ss), sum_ss), s's), s''s), fs), fs_copy), self_fs), gs), all_gs), xFs), yFs), yFs_copy), RFs), (Rtuple, Rtuple')), (hrecs, hrecs')), (nat, nat')), Rs), Rs_copy), R's), sRs), (idx, idx')), Idx), Ris), Kss), names_lthy) = lthy |> mk_Frees' "b" activeAs ||>> mk_Frees "b" activeAs ||>> mk_Frees "b" activeAs ||>> mk_Frees "b" activeBs + ||>> mk_Frees' "y" passiveAs ||>> mk_Frees "A" ATs ||>> mk_Frees "B" BTs ||>> mk_Frees "B" BTs @@ -230,7 +228,6 @@ val map_cong0s = map map_cong0_of_bnf bnfs; val map_id0s = map map_id0_of_bnf bnfs; val map_ids = map map_id_of_bnf bnfs; - val map_wpulls = map map_wpull_of_bnf bnfs; val set_bdss = map set_bd_of_bnf bnfs; val set_mapss = map set_map_of_bnf bnfs; val rel_congs = map rel_cong_of_bnf bnfs; @@ -667,25 +664,6 @@ val set_hset_thmss' = transpose set_hset_thmss; val set_hset_hset_thmsss' = transpose (map transpose set_hset_hset_thmsss); - val set_incl_hin_thmss = - let - fun mk_set_incl_hin s x hsets1 set hsets2 T = - fold_rev Logic.all (x :: ss @ As) - (Logic.list_implies - (map2 (fn hset => fn A => HOLogic.mk_Trueprop (mk_leq (hset $ x) A)) hsets1 As, - HOLogic.mk_Trueprop (mk_leq (set $ (s $ x)) (mk_in As hsets2 T)))); - - val set_incl_hin_goalss = - map4 (fn s => fn x => fn sets => fn hsets => - map3 (mk_set_incl_hin s x hsets) (drop m sets) hsetssAs activeAs) - ss zs setssAs hsetssAs; - in - map2 (map2 (fn goal => fn thms => - Goal.prove_sorry lthy [] [] goal (K (mk_set_incl_hin_tac thms)) - |> Thm.close_derivation)) - set_incl_hin_goalss set_hset_incl_hset_thmsss - end; - val hset_minimal_thms = let fun mk_passive_prem set s x K = @@ -1648,7 +1626,6 @@ val Ts = map (fn name => Type (name, params')) T_names; fun mk_Ts passive = map (Term.typ_subst_atomic (passiveAs ~~ passive)) Ts; val Ts' = mk_Ts passiveBs; - val Ts'' = mk_Ts passiveCs; val Rep_Ts = map2 (fn info => fn T => Const (#Rep_name info, T --> treeQT)) T_glob_infos Ts; val Abs_Ts = map2 (fn info => fn T => Const (#Abs_name info, treeQT --> T)) T_glob_infos Ts; @@ -1679,21 +1656,21 @@ val corec_Inls = map (Term.subst_atomic_types (activeBs ~~ Ts)) Inls; val corec_UNIVs = map2 (HOLogic.mk_UNIV oo curry mk_sumT) Ts activeAs; - val ((((((((((((((Jzs, Jzs'), (Jz's, Jz's')), Jzs_copy), Jz's_copy), Jzs1), Jzs2), Jpairs), - FJzs), TRs), unfold_fs), unfold_fs_copy), corec_ss), phis), names_lthy) = names_lthy + val (((((((((((((Jzs, Jzs'), Jz's), Jzs_copy), Jz's_copy), Jzs1), Jzs2), + FJzs), TRs), unfold_fs), corec_ss), phis), dtor_set_induct_phiss), + names_lthy) = names_lthy |> mk_Frees' "z" Ts - ||>> mk_Frees' "y" Ts' + ||>> mk_Frees "y" Ts' ||>> mk_Frees "z'" Ts ||>> mk_Frees "y'" Ts' ||>> mk_Frees "z1" Ts ||>> mk_Frees "z2" Ts - ||>> mk_Frees "j" (map2 (curry HOLogic.mk_prodT) Ts Ts') ||>> mk_Frees "x" prodFTs ||>> mk_Frees "r" (map (mk_relT o `I) Ts) ||>> mk_Frees "f" unfold_fTs - ||>> mk_Frees "g" unfold_fTs ||>> mk_Frees "s" corec_sTs - ||>> mk_Frees "P" (map2 mk_pred2T Ts Ts); + ||>> mk_Frees "P" (map2 mk_pred2T Ts Ts) + ||>> mk_Freess "P" (map (fn A => map (mk_pred2T A) Ts) passiveAs); fun dtor_bind i = nth external_bs (i - 1) |> Binding.prefix_name (dtorN ^ "_"); val dtor_name = Binding.name_of o dtor_bind; @@ -1812,25 +1789,6 @@ |> Thm.close_derivation) end; - val unique_mor_thms = - let - val prems = [HOLogic.mk_Trueprop (mk_coalg passive_UNIVs Bs ss), HOLogic.mk_Trueprop - (HOLogic.mk_conj (mk_mor Bs ss UNIVs dtors unfold_fs, - mk_mor Bs ss UNIVs dtors unfold_fs_copy))]; - fun mk_fun_eq B f g z = HOLogic.mk_imp - (HOLogic.mk_mem (z, B), HOLogic.mk_eq (f $ z, g $ z)); - val unique = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj - (map4 mk_fun_eq Bs unfold_fs unfold_fs_copy zs)); - - val unique_mor = Goal.prove_sorry lthy [] [] - (fold_rev Logic.all (Bs @ ss @ unfold_fs @ unfold_fs_copy @ zs) - (Logic.list_implies (prems, unique))) - (K (mk_unique_mor_tac raw_coind_thms bis_image2_thm)) - |> Thm.close_derivation; - in - map (fn thm => conjI RSN (2, thm RS mp)) (split_conj_thm unique_mor) - end; - val (unfold_unique_mor_thms, unfold_unique_mor_thm) = let val prem = HOLogic.mk_Trueprop (mk_mor active_UNIVs ss UNIVs dtors unfold_fs); @@ -2086,6 +2044,59 @@ val timer = time (timer "coinduction"); + val setss_by_bnf = map (fn i => map2 (mk_hset dtors i) ls passiveAs) ks; + val setss_by_range = transpose setss_by_bnf; + + val (hset_dtor_incl_thmss, hset_hset_dtor_incl_thmsss, dtor_hset_induct_thms) = + let + fun tinst_of dtor = + map (SOME o certify lthy) (dtor :: remove (op =) dtor dtors); + fun tinst_of' dtor = case tinst_of dtor of t :: ts => t :: NONE :: ts; + val Tinst = map (pairself (certifyT lthy)) + (map Logic.varifyT_global (deads @ allAs) ~~ (deads @ passiveAs @ Ts)); + val set_incl_thmss = + map2 (fn dtor => map (singleton (Proof_Context.export names_lthy lthy) o + Drule.instantiate' [] (tinst_of' dtor) o + Thm.instantiate (Tinst, []) o Drule.zero_var_indexes)) + dtors set_incl_hset_thmss; + + val tinst = splice (map (SOME o certify lthy) dtors) (replicate n NONE) + val set_minimal_thms = + map (Drule.instantiate' [] tinst o Thm.instantiate (Tinst, []) o + Drule.zero_var_indexes) + hset_minimal_thms; + + val set_set_incl_thmsss = + map2 (fn dtor => map (map (singleton (Proof_Context.export names_lthy lthy) o + Drule.instantiate' [] (NONE :: tinst_of' dtor) o + Thm.instantiate (Tinst, []) o Drule.zero_var_indexes))) + dtors set_hset_incl_hset_thmsss; + + val set_set_incl_thmsss' = transpose (map transpose set_set_incl_thmsss); + + val incls = + maps (map (fn thm => thm RS @{thm subset_Collect_iff})) set_incl_thmss @ + @{thms subset_Collect_iff[OF subset_refl]}; + + fun mk_induct_tinst phis jsets y y' = + map4 (fn phi => fn jset => fn Jz => fn Jz' => + SOME (certify lthy (Term.absfree Jz' (HOLogic.mk_Collect (fst y', snd y', + HOLogic.mk_conj (HOLogic.mk_mem (y, jset $ Jz), phi $ y $ Jz)))))) + phis jsets Jzs Jzs'; + val dtor_set_induct_thms = + map6 (fn set_minimal => fn set_set_inclss => fn jsets => fn y => fn y' => fn phis => + ((set_minimal + |> Drule.instantiate' [] (mk_induct_tinst phis jsets y y') + |> unfold_thms lthy incls) OF + (replicate n ballI @ + maps (map (fn thm => thm RS @{thm subset_CollectI})) set_set_inclss)) + |> singleton (Proof_Context.export names_lthy lthy) + |> rule_by_tactic lthy (ALLGOALS (TRY o etac asm_rl))) + set_minimal_thms set_set_incl_thmsss' setss_by_range ys ys' dtor_set_induct_phiss + in + (set_incl_thmss, set_set_incl_thmsss, dtor_set_induct_thms) + end; + fun mk_dtor_map_DEADID_thm dtor_inject map_id0 = trans OF [iffD2 OF [dtor_inject, id_apply], map_id0 RS sym]; @@ -2093,60 +2104,49 @@ trans OF [rel_eq_of_bnf bnf RS @{thm predicate2_eqD}, dtor_inject] RS sym; val JphiTs = map2 mk_pred2T passiveAs passiveBs; + val Jpsi1Ts = map2 mk_pred2T passiveAs passiveCs; + val Jpsi2Ts = map2 mk_pred2T passiveCs passiveBs; val prodTsTs' = map2 (curry HOLogic.mk_prodT) Ts Ts'; val fstsTsTs' = map fst_const prodTsTs'; val sndsTsTs' = map snd_const prodTsTs'; val activephiTs = map2 mk_pred2T activeAs activeBs; val activeJphiTs = map2 mk_pred2T Ts Ts'; - val (((Jphis, activephis), activeJphis), names_lthy) = names_lthy + val (((((Jphis, Jpsi1s), Jpsi2s), activephis), activeJphis), names_lthy) = names_lthy |> mk_Frees "R" JphiTs + ||>> mk_Frees "R" Jpsi1Ts + ||>> mk_Frees "Q" Jpsi2Ts ||>> mk_Frees "S" activephiTs ||>> mk_Frees "JR" activeJphiTs; val rels = map2 (fn Ds => mk_rel_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs; val in_rels = map in_rel_of_bnf bnfs; + fun mk_Jrel_DEADID_coinduct_thm () = + mk_rel_xtor_co_induct_thm Greatest_FP rels activeJphis (map HOLogic.eq_const Ts) Jphis + Jzs Jz's dtors dtor's (fn {context = ctxt, prems} => + (unfold_thms_tac ctxt @{thms le_fun_def le_bool_def all_simps(1,2)[symmetric]} THEN + REPEAT_DETERM (rtac allI 1) THEN rtac (dtor_coinduct_thm OF prems) 1)) lthy; + (*register new codatatypes as BNFs*) - val (timer, Jbnfs, (folded_dtor_map_o_thms, folded_dtor_map_thms), folded_dtor_set_thmss', - dtor_set_induct_thms, dtor_Jrel_thms, Jbnf_notes, lthy) = + val (timer, Jbnfs, (dtor_Jmap_o_thms, dtor_Jmap_thms), dtor_Jset_thmss', + dtor_Jrel_thms, Jrel_coinduct_thm, Jbnf_notes, lthy) = if m = 0 then (timer, replicate n DEADID_bnf, map_split (`(mk_pointfree lthy)) (map2 mk_dtor_map_DEADID_thm dtor_inject_thms map_ids), - replicate n [], [], map2 mk_dtor_Jrel_DEADID_thm dtor_inject_thms bnfs, [], lthy) + replicate n [], map2 mk_dtor_Jrel_DEADID_thm dtor_inject_thms bnfs, + mk_Jrel_DEADID_coinduct_thm (), [], lthy) else let val fTs = map2 (curry op -->) passiveAs passiveBs; val gTs = map2 (curry op -->) passiveBs passiveCs; - val f1Ts = map2 (curry op -->) passiveAs passiveYs; - val f2Ts = map2 (curry op -->) passiveBs passiveYs; - val p1Ts = map2 (curry op -->) passiveXs passiveAs; - val p2Ts = map2 (curry op -->) passiveXs passiveBs; - val pTs = map2 (curry op -->) passiveXs passiveCs; val uTs = map2 (curry op -->) Ts Ts'; - val B1Ts = map HOLogic.mk_setT passiveAs; - val B2Ts = map HOLogic.mk_setT passiveBs; - val AXTs = map HOLogic.mk_setT passiveXs; - val XTs = mk_Ts passiveXs; - val YTs = mk_Ts passiveYs; - - val ((((((((((((((((((fs, fs'), fs_copy), gs), us), - (Jys, Jys')), (Jys_copy, Jys'_copy)), dtor_set_induct_phiss), - B1s), B2s), AXs), f1s), f2s), p1s), p2s), ps), (ys, ys')), (ys_copy, ys'_copy)), - names_lthy) = names_lthy + + val ((((((((fs, fs'), fs_copy), gs), us), (Jys, Jys')), (Jys_copy, Jys'_copy)), + (ys_copy, ys'_copy)), names_lthy) = names_lthy |> mk_Frees' "f" fTs ||>> mk_Frees "f" fTs ||>> mk_Frees "g" gTs ||>> mk_Frees "u" uTs ||>> mk_Frees' "b" Ts' ||>> mk_Frees' "b" Ts' - ||>> mk_Freess "P" (map (fn A => map (mk_pred2T A) Ts) passiveAs) - ||>> mk_Frees "B1" B1Ts - ||>> mk_Frees "B2" B2Ts - ||>> mk_Frees "A" AXTs - ||>> mk_Frees "f1" f1Ts - ||>> mk_Frees "f2" f2Ts - ||>> mk_Frees "p1" p1Ts - ||>> mk_Frees "p2" p2Ts - ||>> mk_Frees "p" pTs - ||>> mk_Frees' "y" passiveAs ||>> mk_Frees' "y" passiveAs; val map_FTFT's = map2 (fn Ds => @@ -2160,382 +2160,11 @@ HOLogic.mk_comp (mk_Fmap mk_const fs Ts Fmap, dtor)) dtors (mk_maps Ts mk_T)); val mk_map_id = mk_map HOLogic.id_const I; val mk_mapsAB = mk_maps passiveAs passiveBs; - val mk_mapsBC = mk_maps passiveBs passiveCs; - val mk_mapsAC = mk_maps passiveAs passiveCs; - val mk_mapsAY = mk_maps passiveAs passiveYs; - val mk_mapsBY = mk_maps passiveBs passiveYs; - val mk_mapsXA = mk_maps passiveXs passiveAs; - val mk_mapsXB = mk_maps passiveXs passiveBs; - val mk_mapsXC = mk_maps passiveXs passiveCs; val fs_maps = map (mk_map_id Ts fs Ts' dtors mk_mapsAB) ks; - val fs_copy_maps = map (mk_map_id Ts fs_copy Ts' dtors mk_mapsAB) ks; - val gs_maps = map (mk_map_id Ts' gs Ts'' dtor's mk_mapsBC) ks; - val fgs_maps = - map (mk_map_id Ts (map2 (curry HOLogic.mk_comp) gs fs) Ts'' dtors mk_mapsAC) ks; - val Xdtors = mk_dtors passiveXs; - val UNIV's = map HOLogic.mk_UNIV Ts'; - val CUNIVs = map HOLogic.mk_UNIV passiveCs; - val UNIV''s = map HOLogic.mk_UNIV Ts''; - val dtor''s = mk_dtors passiveCs; - val f1s_maps = map (mk_map_id Ts f1s YTs dtors mk_mapsAY) ks; - val f2s_maps = map (mk_map_id Ts' f2s YTs dtor's mk_mapsBY) ks; - val pid_maps = map (mk_map_id XTs ps Ts'' Xdtors mk_mapsXC) ks; - val pfst_Fmaps = - map (mk_Fmap fst_const p1s prodTsTs') (mk_mapsXA prodTsTs' (fst o HOLogic.dest_prodT)); - val psnd_Fmaps = - map (mk_Fmap snd_const p2s prodTsTs') (mk_mapsXB prodTsTs' (snd o HOLogic.dest_prodT)); - val p1id_Fmaps = map (mk_Fmap HOLogic.id_const p1s prodTsTs') (mk_mapsXA prodTsTs' I); - val p2id_Fmaps = map (mk_Fmap HOLogic.id_const p2s prodTsTs') (mk_mapsXB prodTsTs' I); - val pid_Fmaps = map (mk_Fmap HOLogic.id_const ps prodTsTs') (mk_mapsXC prodTsTs' I); - - val (dtor_map_thms, map_thms) = - let - fun mk_goal fs_map map dtor dtor' = fold_rev Logic.all fs - (mk_Trueprop_eq (HOLogic.mk_comp (dtor', fs_map), - HOLogic.mk_comp (Term.list_comb (map, fs @ fs_maps), dtor))); - val goals = map4 mk_goal fs_maps map_FTFT's dtors dtor's; - val cTs = map (SOME o certifyT lthy) FTs'; - val maps = - map5 (fn goal => fn cT => fn unfold => fn map_comp => fn map_cong0 => - Goal.prove_sorry lthy [] [] goal - (K (mk_map_tac m n cT unfold map_comp map_cong0)) - |> Thm.close_derivation) - goals cTs dtor_unfold_thms map_comps map_cong0s; - in - map_split (fn thm => (thm RS @{thm comp_eq_dest}, thm)) maps - end; - - val map_comp0_thms = - let - val goal = fold_rev Logic.all (fs @ gs) - (HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj - (map3 (fn fmap => fn gmap => fn fgmap => - HOLogic.mk_eq (HOLogic.mk_comp (gmap, fmap), fgmap)) - fs_maps gs_maps fgs_maps))) - in - split_conj_thm (Goal.prove_sorry lthy [] [] goal - (K (mk_map_comp0_tac m n map_thms map_comp0s map_cong0s dtor_unfold_unique_thm)) - |> Thm.close_derivation) - end; - - val dtor_map_unique_thm = - let - fun mk_prem u map dtor dtor' = - mk_Trueprop_eq (HOLogic.mk_comp (dtor', u), - HOLogic.mk_comp (Term.list_comb (map, fs @ us), dtor)); - val prems = map4 mk_prem us map_FTFT's dtors dtor's; - val goal = - HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj - (map2 (curry HOLogic.mk_eq) us fs_maps)); - in - Goal.prove_sorry lthy [] [] - (fold_rev Logic.all (us @ fs) (Logic.list_implies (prems, goal))) - (mk_dtor_map_unique_tac dtor_unfold_unique_thm sym_map_comps) - |> Thm.close_derivation - end; - - val timer = time (timer "map functions for the new codatatypes"); - - val setss_by_bnf = map (fn i => map2 (mk_hset dtors i) ls passiveAs) ks; - val setss_by_bnf' = map (fn i => map2 (mk_hset dtor's i) ls passiveBs) ks; - val setss_by_range = transpose setss_by_bnf; - - val dtor_set_thmss = - let - fun mk_simp_goal relate pas_set act_sets sets dtor z set = - relate (set $ z, mk_union (pas_set $ (dtor $ z), - Library.foldl1 mk_union - (map2 (fn X => mk_UNION (X $ (dtor $ z))) act_sets sets))); - fun mk_goals eq = - map2 (fn i => fn sets => - map4 (fn Fsets => - mk_simp_goal eq (nth Fsets (i - 1)) (drop m Fsets) sets) - FTs_setss dtors Jzs sets) - ls setss_by_range; - - val le_goals = map - (fold_rev Logic.all Jzs o HOLogic.mk_Trueprop o Library.foldr1 HOLogic.mk_conj) - (mk_goals (uncurry mk_leq)); - val set_le_thmss = map split_conj_thm - (map4 (fn goal => fn hset_minimal => fn set_hsets => fn set_hset_hsetss => - Goal.prove_sorry lthy [] [] goal - (K (mk_set_le_tac n hset_minimal set_hsets set_hset_hsetss)) - |> Thm.close_derivation) - le_goals hset_minimal_thms set_hset_thmss' set_hset_hset_thmsss'); - - val simp_goalss = map (map2 (fn z => fn goal => - Logic.all z (HOLogic.mk_Trueprop goal)) Jzs) - (mk_goals HOLogic.mk_eq); - in - map4 (map4 (fn goal => fn set_le => fn set_incl_hset => fn set_hset_incl_hsets => - Goal.prove_sorry lthy [] [] goal - (K (mk_dtor_set_tac n set_le set_incl_hset set_hset_incl_hsets)) - |> Thm.close_derivation)) - simp_goalss set_le_thmss set_incl_hset_thmss' set_hset_incl_hset_thmsss' - end; - - val timer = time (timer "set functions for the new codatatypes"); - - val colss = map2 (fn j => fn T => - map (fn i => mk_hset_rec dtors nat i j T) ks) ls passiveAs; - val colss' = map2 (fn j => fn T => - map (fn i => mk_hset_rec dtor's nat i j T) ks) ls passiveBs; - val Xcolss = map2 (fn j => fn T => - map (fn i => mk_hset_rec Xdtors nat i j T) ks) ls passiveXs; - - val col_natural_thmss = - let - fun mk_col_natural f map z col col' = - HOLogic.mk_eq (mk_image f $ (col $ z), col' $ (map $ z)); - - fun mk_goal f cols cols' = list_all_free Jzs (Library.foldr1 HOLogic.mk_conj - (map4 (mk_col_natural f) fs_maps Jzs cols cols')); - - val goals = map3 mk_goal fs colss colss'; - - val ctss = - map (fn phi => map (SOME o certify lthy) [Term.absfree nat' phi, nat]) goals; - - val thms = - map4 (fn goal => fn cts => fn rec_0s => fn rec_Sucs => - singleton (Proof_Context.export names_lthy lthy) - (Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal) - (mk_col_natural_tac cts rec_0s rec_Sucs dtor_map_thms set_mapss)) - |> Thm.close_derivation) - goals ctss hset_rec_0ss' hset_rec_Sucss'; - in - map (split_conj_thm o mk_specN n) thms - end; - - val col_bd_thmss = - let - fun mk_col_bd z col = mk_ordLeq (mk_card_of (col $ z)) sbd; - - fun mk_goal cols = list_all_free Jzs (Library.foldr1 HOLogic.mk_conj - (map2 mk_col_bd Jzs cols)); - - val goals = map mk_goal colss; - - val ctss = - map (fn phi => map (SOME o certify lthy) [Term.absfree nat' phi, nat]) goals; - - val thms = - map5 (fn j => fn goal => fn cts => fn rec_0s => fn rec_Sucs => - singleton (Proof_Context.export names_lthy lthy) - (Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal) - (K (mk_col_bd_tac m j cts rec_0s rec_Sucs - sbd_Card_order sbd_Cinfinite set_sbdss))) - |> Thm.close_derivation) - ls goals ctss hset_rec_0ss' hset_rec_Sucss'; - in - map (split_conj_thm o mk_specN n) thms - end; - - val map_cong0_thms = - let - val cTs = map (SOME o certifyT lthy o - Term.typ_subst_atomic (passiveAs ~~ passiveBs) o TFree) coinduct_params; - - fun mk_prem z set f g y y' = - mk_Ball (set $ z) (Term.absfree y' (HOLogic.mk_eq (f $ y, g $ y))); - - fun mk_prems sets z = - Library.foldr1 HOLogic.mk_conj (map5 (mk_prem z) sets fs fs_copy ys ys') - - fun mk_map_cong0 sets z fmap gmap = - HOLogic.mk_imp (mk_prems sets z, HOLogic.mk_eq (fmap $ z, gmap $ z)); - - fun mk_coind_body sets (x, T) z fmap gmap y y_copy = - HOLogic.mk_conj - (HOLogic.mk_mem (z, HOLogic.mk_Collect (x, T, mk_prems sets z)), - HOLogic.mk_conj (HOLogic.mk_eq (y, fmap $ z), - HOLogic.mk_eq (y_copy, gmap $ z))) - - fun mk_cphi sets (z' as (x, T)) z fmap gmap y' y y'_copy y_copy = - HOLogic.mk_exists (x, T, mk_coind_body sets z' z fmap gmap y y_copy) - |> Term.absfree y'_copy - |> Term.absfree y' - |> certify lthy; - - val cphis = - map9 mk_cphi setss_by_bnf Jzs' Jzs fs_maps fs_copy_maps Jys' Jys Jys'_copy Jys_copy; - - val coinduct = Drule.instantiate' cTs (map SOME cphis) dtor_map_coinduct_thm; - - val goal = - HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj - (map4 mk_map_cong0 setss_by_bnf Jzs fs_maps fs_copy_maps)); - - val thm = singleton (Proof_Context.export names_lthy lthy) - (Goal.prove_sorry lthy [] [] goal - (K (mk_mcong_tac lthy m (rtac coinduct) map_comps dtor_map_thms map_cong0s set_mapss - set_hset_thmss set_hset_hset_thmsss))) - |> Thm.close_derivation - in - split_conj_thm thm - end; - - val B1_ins = map2 (mk_in B1s) setss_by_bnf Ts; - val B2_ins = map2 (mk_in B2s) setss_by_bnf' Ts'; - val thePulls = map4 mk_thePull B1_ins B2_ins f1s_maps f2s_maps; - val thePullTs = passiveXs @ map2 (curry HOLogic.mk_prodT) Ts Ts'; - val thePull_ins = map2 (mk_in (AXs @ thePulls)) (mk_setss thePullTs) (mk_FTs thePullTs); - val pickFs = map5 mk_pickWP thePull_ins pfst_Fmaps psnd_Fmaps - (map2 (curry op $) dtors Jzs) (map2 (curry op $) dtor's Jz's); - val pickF_ss = map3 (fn pickF => fn z => fn z' => - HOLogic.mk_split (Term.absfree z (Term.absfree z' pickF))) pickFs Jzs' Jz's'; - val picks = map (mk_unfold XTs pickF_ss) ks; - - val wpull_prem = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj - (map8 mk_wpull AXs B1s B2s f1s f2s (replicate m NONE) p1s p2s)); - - val map_eq_thms = map2 (fn simp => fn diff => box_equals OF [diff RS iffD2, simp, simp]) - dtor_map_thms dtor_inject_thms; - val map_wpull_thms = map (fn thm => thm OF - (replicate m asm_rl @ replicate n @{thm wpull_thePull})) map_wpulls; - val pickWP_assms_tacs = - map3 mk_pickWP_assms_tac set_incl_hset_thmss set_incl_hin_thmss map_eq_thms; - - val coalg_thePull_thm = - let - val coalg = HOLogic.mk_Trueprop - (mk_coalg CUNIVs thePulls (map2 (curry HOLogic.mk_comp) pid_Fmaps pickF_ss)); - val goal = fold_rev Logic.all (AXs @ B1s @ B2s @ f1s @ f2s @ p1s @ p2s @ ps) - (Logic.mk_implies (wpull_prem, coalg)); - in - Goal.prove_sorry lthy [] [] goal (mk_coalg_thePull_tac m coalg_def map_wpull_thms - set_mapss pickWP_assms_tacs) - |> Thm.close_derivation - end; - - val (mor_thePull_fst_thm, mor_thePull_snd_thm, mor_thePull_pick_thm) = - let - val mor_fst = HOLogic.mk_Trueprop - (mk_mor thePulls (map2 (curry HOLogic.mk_comp) p1id_Fmaps pickF_ss) - UNIVs dtors fstsTsTs'); - val mor_snd = HOLogic.mk_Trueprop - (mk_mor thePulls (map2 (curry HOLogic.mk_comp) p2id_Fmaps pickF_ss) - UNIV's dtor's sndsTsTs'); - val mor_pick = HOLogic.mk_Trueprop - (mk_mor thePulls (map2 (curry HOLogic.mk_comp) pid_Fmaps pickF_ss) - UNIV''s dtor''s (map2 (curry HOLogic.mk_comp) pid_maps picks)); - - val fst_goal = fold_rev Logic.all (AXs @ B1s @ B2s @ f1s @ f2s @ p1s @ p2s) - (Logic.mk_implies (wpull_prem, mor_fst)); - val snd_goal = fold_rev Logic.all (AXs @ B1s @ B2s @ f1s @ f2s @ p1s @ p2s) - (Logic.mk_implies (wpull_prem, mor_snd)); - val pick_goal = fold_rev Logic.all (AXs @ B1s @ B2s @ f1s @ f2s @ p1s @ p2s @ ps) - (Logic.mk_implies (wpull_prem, mor_pick)); - in - (Goal.prove_sorry lthy [] [] fst_goal (mk_mor_thePull_fst_tac m mor_def map_wpull_thms - map_comps pickWP_assms_tacs) |> Thm.close_derivation, - Goal.prove_sorry lthy [] [] snd_goal (mk_mor_thePull_snd_tac m mor_def map_wpull_thms - map_comps pickWP_assms_tacs) |> Thm.close_derivation, - Goal.prove_sorry lthy [] [] pick_goal (mk_mor_thePull_pick_tac mor_def dtor_unfold_thms - map_comps) |> Thm.close_derivation) - end; - - val pick_col_thmss = - let - fun mk_conjunct AX Jpair pick thePull col = - HOLogic.mk_imp (HOLogic.mk_mem (Jpair, thePull), mk_leq (col $ (pick $ Jpair)) AX); - - fun mk_concl AX cols = - list_all_free Jpairs (Library.foldr1 HOLogic.mk_conj - (map4 (mk_conjunct AX) Jpairs picks thePulls cols)); - - val concls = map2 mk_concl AXs Xcolss; - - val ctss = - map (fn phi => map (SOME o certify lthy) [Term.absfree nat' phi, nat]) concls; - - val goals = - map (fn concl => Logic.mk_implies (wpull_prem, HOLogic.mk_Trueprop concl)) concls; - - val thms = - map5 (fn j => fn goal => fn cts => fn rec_0s => fn rec_Sucs => - singleton (Proof_Context.export names_lthy lthy) (Goal.prove_sorry lthy [] [] goal - (mk_pick_col_tac m j cts rec_0s rec_Sucs dtor_unfold_thms set_mapss - map_wpull_thms pickWP_assms_tacs)) - |> Thm.close_derivation) - ls goals ctss hset_rec_0ss' hset_rec_Sucss'; - in - map (map (fn thm => thm RS mp) o split_conj_thm o mk_specN n) thms - end; - - val timer = time (timer "helpers for BNF properties"); - - val map_id0_tacs = - map2 (K oo mk_map_id0_tac map_thms) dtor_unfold_unique_thms unfold_dtor_thms; - val map_comp0_tacs = map (fn thm => K (rtac (thm RS sym) 1)) map_comp0_thms; - val map_cong0_tacs = map (mk_map_cong0_tac m) map_cong0_thms; - val set_nat_tacss = - map2 (map2 (K oo mk_set_map0_tac)) hset_defss (transpose col_natural_thmss); - - val bd_co_tacs = replicate n (K (rtac sbd_card_order 1)); - val bd_cinf_tacs = replicate n (K (rtac (sbd_Cinfinite RS conjunct1) 1)); - - val set_bd_tacss = - map2 (map2 (K oo mk_set_bd_tac sbd_Cinfinite)) hset_defss (transpose col_bd_thmss); - - val map_wpull_tacs = - map3 (K ooo mk_wpull_tac m coalg_thePull_thm mor_thePull_fst_thm mor_thePull_snd_thm - mor_thePull_pick_thm) unique_mor_thms (transpose pick_col_thmss) hset_defss; - - val rel_OO_Grp_tacs = replicate n (K (rtac refl 1)); - - val tacss = map9 zip_axioms map_id0_tacs map_comp0_tacs map_cong0_tacs set_nat_tacss - bd_co_tacs bd_cinf_tacs set_bd_tacss map_wpull_tacs rel_OO_Grp_tacs; - - val (hset_dtor_incl_thmss, hset_hset_dtor_incl_thmsss, dtor_hset_induct_thms) = - let - fun tinst_of dtor = - map (SOME o certify lthy) (dtor :: remove (op =) dtor dtors); - fun tinst_of' dtor = case tinst_of dtor of t :: ts => t :: NONE :: ts; - val Tinst = map (pairself (certifyT lthy)) - (map Logic.varifyT_global (deads @ allAs) ~~ (deads @ passiveAs @ Ts)); - val set_incl_thmss = - map2 (fn dtor => map (singleton (Proof_Context.export names_lthy lthy) o - Drule.instantiate' [] (tinst_of' dtor) o - Thm.instantiate (Tinst, []) o Drule.zero_var_indexes)) - dtors set_incl_hset_thmss; - - val tinst = splice (map (SOME o certify lthy) dtors) (replicate n NONE) - val set_minimal_thms = - map (Drule.instantiate' [] tinst o Thm.instantiate (Tinst, []) o - Drule.zero_var_indexes) - hset_minimal_thms; - - val set_set_incl_thmsss = - map2 (fn dtor => map (map (singleton (Proof_Context.export names_lthy lthy) o - Drule.instantiate' [] (NONE :: tinst_of' dtor) o - Thm.instantiate (Tinst, []) o Drule.zero_var_indexes))) - dtors set_hset_incl_hset_thmsss; - - val set_set_incl_thmsss' = transpose (map transpose set_set_incl_thmsss); - - val incls = - maps (map (fn thm => thm RS @{thm subset_Collect_iff})) set_incl_thmss @ - @{thms subset_Collect_iff[OF subset_refl]}; - - fun mk_induct_tinst phis jsets y y' = - map4 (fn phi => fn jset => fn Jz => fn Jz' => - SOME (certify lthy (Term.absfree Jz' (HOLogic.mk_Collect (fst y', snd y', - HOLogic.mk_conj (HOLogic.mk_mem (y, jset $ Jz), phi $ y $ Jz)))))) - phis jsets Jzs Jzs'; - val dtor_set_induct_thms = - map6 (fn set_minimal => fn set_set_inclss => fn jsets => fn y => fn y' => fn phis => - ((set_minimal - |> Drule.instantiate' [] (mk_induct_tinst phis jsets y y') - |> unfold_thms lthy incls) OF - (replicate n ballI @ - maps (map (fn thm => thm RS @{thm subset_CollectI})) set_set_inclss)) - |> singleton (Proof_Context.export names_lthy lthy) - |> rule_by_tactic lthy (ALLGOALS (TRY o etac asm_rl))) - set_minimal_thms set_set_incl_thmsss' setss_by_range ys ys' dtor_set_induct_phiss - in - (set_incl_thmss, set_set_incl_thmsss, dtor_set_induct_thms) - end; + + val set_bss = + map (flat o map2 (fn B => fn b => + if member (op =) resDs (TFree B) then [] else [b]) resBs) set_bss0; fun close_wit I wit = (I, fold_rev Term.absfree (map (nth ys') I) wit); @@ -2622,6 +2251,14 @@ val coind_witss = maps (map (mk_coind_wits o prepare_args)) nonredundant_coind_wit_argsss; + val witss = map2 (fn Ds => fn bnf => mk_wits_of_bnf + (replicate (nwits_of_bnf bnf) Ds) + (replicate (nwits_of_bnf bnf) (passiveAs @ Ts)) bnf) Dss bnfs; + + val ctor_witss = + map (map (uncurry close_wit o tree_to_ctor_wit ys ctors witss o snd o snd) o + filter_out (fst o snd)) wit_treess; + fun mk_coind_wit_thms ((I, dummys), (wits, wit_thms)) = let fun mk_goal sets y y_copy y'_copy j = @@ -2653,57 +2290,253 @@ val coind_wit_thms = maps mk_coind_wit_thms coind_witss; - val witss = map2 (fn Ds => fn bnf => mk_wits_of_bnf - (replicate (nwits_of_bnf bnf) Ds) - (replicate (nwits_of_bnf bnf) (passiveAs @ Ts)) bnf) Dss bnfs; - - val ctor_witss = - map (map (uncurry close_wit o tree_to_ctor_wit ys ctors witss o snd o snd) o - filter_out (fst o snd)) wit_treess; - - val all_witss = + val (wit_thmss, all_witss) = fold (fn ((i, wit), thms) => fn witss => nth_map i (fn (thms', wits) => (thms @ thms', wit :: wits)) witss) coind_wit_thms (map (pair []) ctor_witss) - |> map (apsnd (map snd o minimize_wits)); - - val wit_tac = mk_wit_tac n dtor_ctor_thms (flat dtor_set_thmss) (maps wit_thms_of_bnf bnfs); - - val set_bss = - map (flat o map2 (fn B => fn b => - if member (op =) resDs (TFree B) then [] else [b]) resBs) set_bss0; - - val (Jbnfs, lthy) = - fold_map9 (fn tacs => fn b => fn map_b => fn rel_b => fn set_bs => fn mapx => fn sets => - fn T => fn (thms, wits) => fn lthy => - bnf_def Dont_Inline (user_policy Note_Some) I tacs (wit_tac thms) (SOME deads) map_b - rel_b set_bs - ((((((b, T), fold_rev Term.absfree fs' mapx), sets), sbd), wits), NONE) lthy - |> register_bnf (Local_Theory.full_name lthy b)) - tacss bs map_bs rel_bs set_bss fs_maps setss_by_bnf Ts all_witss lthy; - - val fold_maps = fold_thms lthy (map (fn bnf => - mk_unabs_def m (map_def_of_bnf bnf RS meta_eq_to_obj_eq)) Jbnfs); - - val fold_sets = fold_thms lthy (maps (fn bnf => - map (fn thm => thm RS meta_eq_to_obj_eq) (set_defs_of_bnf bnf)) Jbnfs); - - val timer = time (timer "registered new codatatypes as BNFs"); - - val dtor_set_incl_thmss = map (map fold_sets) hset_dtor_incl_thmss; - val dtor_set_set_incl_thmsss = map (map (map fold_sets)) hset_hset_dtor_incl_thmsss; - val dtor_set_induct_thms = map fold_sets dtor_hset_induct_thms; - - val Jrels = map (mk_rel_of_bnf deads passiveAs passiveBs) Jbnfs; - - val Jrelphis = map (fn Jrel => Term.list_comb (Jrel, Jphis)) Jrels; + |> map (apsnd (map snd o minimize_wits)) + |> split_list; + + val (Jbnf_consts, lthy) = + fold_map8 (fn b => fn map_b => fn rel_b => fn set_bs => fn mapx => fn sets => fn wits => + fn T => fn lthy => + define_bnf_consts Dont_Inline (user_policy Note_Some lthy) (SOME deads) + map_b rel_b set_bs + ((((((b, T), fold_rev Term.absfree fs' mapx), sets), sbd), wits), NONE) lthy) + bs map_bs rel_bs set_bss fs_maps setss_by_bnf all_witss Ts lthy; + + val (_, Jconsts, Jconst_defs, mk_Jconsts) = split_list4 Jbnf_consts; + val (_, Jsetss, Jbds_Ds, Jwitss_Ds, _) = split_list5 Jconsts; + val (Jmap_defs, Jset_defss, Jbd_defs, Jwit_defss, Jrel_defs) = split_list5 Jconst_defs; + val (mk_Jmaps_Ds, mk_Jt_Ds, _, mk_Jrels_Ds, _) = split_list5 mk_Jconsts; + + val Jrel_unabs_defs = map (fn def => mk_unabs_def m (def RS meta_eq_to_obj_eq)) Jrel_defs; + val Jset_defs = flat Jset_defss; + val Jset_unabs_defs = map (fn def => def RS meta_eq_to_obj_eq RS fun_cong) Jset_defs; + + fun mk_Jmaps As Bs = map (fn mk => mk deads As Bs) mk_Jmaps_Ds; + fun mk_Jsetss As = map2 (fn mk => fn Jsets => map (mk deads As) Jsets) mk_Jt_Ds Jsetss; + val Jbds = map2 (fn mk => mk deads passiveAs) mk_Jt_Ds Jbds_Ds; + val Jwitss = + map2 (fn mk => fn Jwits => map (mk deads passiveAs o snd) Jwits) mk_Jt_Ds Jwitss_Ds; + fun mk_Jrels As Bs = map (fn mk => mk deads As Bs) mk_Jrels_Ds; + + val Jmaps = mk_Jmaps passiveAs passiveBs; + val fs_Jmaps = map (fn m => Term.list_comb (m, fs)) Jmaps; + val fs_copy_Jmaps = map (fn m => Term.list_comb (m, fs_copy)) Jmaps; + val gs_Jmaps = map (fn m => Term.list_comb (m, gs)) (mk_Jmaps passiveBs passiveCs); + val fgs_Jmaps = map (fn m => Term.list_comb (m, map2 (curry HOLogic.mk_comp) gs fs)) + (mk_Jmaps passiveAs passiveCs); + val (Jsetss_by_range, Jsetss_by_bnf) = `transpose (mk_Jsetss passiveAs); + + val timer = time (timer "bnf constants for the new datatypes"); + + val (dtor_Jmap_thms, Jmap_thms) = + let + fun mk_goal fs_Jmap map dtor dtor' = fold_rev Logic.all fs + (mk_Trueprop_eq (HOLogic.mk_comp (dtor', fs_Jmap), + HOLogic.mk_comp (Term.list_comb (map, fs @ fs_Jmaps), dtor))); + val goals = map4 mk_goal fs_Jmaps map_FTFT's dtors dtor's; + val cTs = map (SOME o certifyT lthy) FTs'; + val maps = + map5 (fn goal => fn cT => fn unfold => fn map_comp => fn map_cong0 => + Goal.prove_sorry lthy [] [] goal + (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jmap_defs THEN + mk_map_tac m n cT unfold map_comp map_cong0) + |> Thm.close_derivation) + goals cTs dtor_unfold_thms map_comps map_cong0s; + in + map_split (fn thm => (thm RS @{thm comp_eq_dest}, thm)) maps + end; + + val dtor_Jmap_unique_thm = + let + fun mk_prem u map dtor dtor' = + mk_Trueprop_eq (HOLogic.mk_comp (dtor', u), + HOLogic.mk_comp (Term.list_comb (map, fs @ us), dtor)); + val prems = map4 mk_prem us map_FTFT's dtors dtor's; + val goal = + HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj + (map2 (curry HOLogic.mk_eq) us fs_Jmaps)); + in + Goal.prove_sorry lthy [] [] + (fold_rev Logic.all (us @ fs) (Logic.list_implies (prems, goal))) + (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jmap_defs THEN + mk_dtor_map_unique_tac dtor_unfold_unique_thm sym_map_comps ctxt) + |> Thm.close_derivation + end; + + val Jmap_comp0_thms = + let + val goal = fold_rev Logic.all (fs @ gs) + (HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj + (map3 (fn fmap => fn gmap => fn fgmap => + HOLogic.mk_eq (HOLogic.mk_comp (gmap, fmap), fgmap)) + fs_Jmaps gs_Jmaps fgs_Jmaps))) + in + split_conj_thm (Goal.prove_sorry lthy [] [] goal + (K (mk_map_comp0_tac Jmap_thms map_comp0s dtor_Jmap_unique_thm)) + |> Thm.close_derivation) + end; + + val timer = time (timer "map functions for the new codatatypes"); + + val (dtor_Jset_thmss', dtor_Jset_thmss) = + let + fun mk_simp_goal relate pas_set act_sets sets dtor z set = + relate (set $ z, mk_union (pas_set $ (dtor $ z), + Library.foldl1 mk_union + (map2 (fn X => mk_UNION (X $ (dtor $ z))) act_sets sets))); + fun mk_goals eq = + map2 (fn i => fn sets => + map4 (fn Fsets => + mk_simp_goal eq (nth Fsets (i - 1)) (drop m Fsets) sets) + FTs_setss dtors Jzs sets) + ls Jsetss_by_range; + + val le_goals = map + (fold_rev Logic.all Jzs o HOLogic.mk_Trueprop o Library.foldr1 HOLogic.mk_conj) + (mk_goals (uncurry mk_leq)); + val set_le_thmss = map split_conj_thm + (map4 (fn goal => fn hset_minimal => fn set_hsets => fn set_hset_hsetss => + Goal.prove_sorry lthy [] [] goal + (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jset_defs THEN + mk_set_le_tac n hset_minimal set_hsets set_hset_hsetss) + |> Thm.close_derivation) + le_goals hset_minimal_thms set_hset_thmss' set_hset_hset_thmsss'); + + val ge_goalss = map (map2 (fn z => fn goal => + Logic.all z (HOLogic.mk_Trueprop goal)) Jzs) + (mk_goals (uncurry mk_leq o swap)); + val set_ge_thmss = + map3 (map3 (fn goal => fn set_incl_hset => fn set_hset_incl_hsets => + Goal.prove_sorry lthy [] [] goal + (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jset_defs THEN + mk_set_ge_tac n set_incl_hset set_hset_incl_hsets) + |> Thm.close_derivation)) + ge_goalss set_incl_hset_thmss' set_hset_incl_hset_thmsss' + in + map2 (map2 (fn le => fn ge => equalityI OF [le, ge])) set_le_thmss set_ge_thmss + |> `transpose + end; + + val timer = time (timer "set functions for the new codatatypes"); + + val colss = map2 (fn j => fn T => + map (fn i => mk_hset_rec dtors nat i j T) ks) ls passiveAs; + val colss' = map2 (fn j => fn T => + map (fn i => mk_hset_rec dtor's nat i j T) ks) ls passiveBs; + + val col_natural_thmss = + let + fun mk_col_natural f map z col col' = + HOLogic.mk_eq (mk_image f $ (col $ z), col' $ (map $ z)); + + fun mk_goal f cols cols' = list_all_free Jzs (Library.foldr1 HOLogic.mk_conj + (map4 (mk_col_natural f) fs_Jmaps Jzs cols cols')); + + val goals = map3 mk_goal fs colss colss'; + + val ctss = + map (fn phi => map (SOME o certify lthy) [Term.absfree nat' phi, nat]) goals; + + val thms = + map4 (fn goal => fn cts => fn rec_0s => fn rec_Sucs => + singleton (Proof_Context.export names_lthy lthy) + (Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal) + (mk_col_natural_tac cts rec_0s rec_Sucs dtor_Jmap_thms set_mapss)) + |> Thm.close_derivation) + goals ctss hset_rec_0ss' hset_rec_Sucss'; + in + map (split_conj_thm o mk_specN n) thms + end; + + val col_bd_thmss = + let + fun mk_col_bd z col bd = mk_ordLeq (mk_card_of (col $ z)) bd; + + fun mk_goal bds cols = list_all_free Jzs (Library.foldr1 HOLogic.mk_conj + (map3 mk_col_bd Jzs cols bds)); + + val goals = map (mk_goal Jbds) colss; + + val ctss = map (fn phi => map (SOME o certify lthy) [Term.absfree nat' phi, nat]) + (map (mk_goal (replicate n sbd)) colss); + + val thms = + map5 (fn j => fn goal => fn cts => fn rec_0s => fn rec_Sucs => + singleton (Proof_Context.export names_lthy lthy) + (Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal) + (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jbd_defs THEN + mk_col_bd_tac m j cts rec_0s rec_Sucs sbd_Card_order sbd_Cinfinite set_sbdss)) + |> Thm.close_derivation) + ls goals ctss hset_rec_0ss' hset_rec_Sucss'; + in + map (split_conj_thm o mk_specN n) thms + end; + + val map_cong0_thms = + let + val cTs = map (SOME o certifyT lthy o + Term.typ_subst_atomic (passiveAs ~~ passiveBs) o TFree) coinduct_params; + + fun mk_prem z set f g y y' = + mk_Ball (set $ z) (Term.absfree y' (HOLogic.mk_eq (f $ y, g $ y))); + + fun mk_prems sets z = + Library.foldr1 HOLogic.mk_conj (map5 (mk_prem z) sets fs fs_copy ys ys') + + fun mk_map_cong0 sets z fmap gmap = + HOLogic.mk_imp (mk_prems sets z, HOLogic.mk_eq (fmap $ z, gmap $ z)); + + fun mk_coind_body sets (x, T) z fmap gmap y y_copy = + HOLogic.mk_conj + (HOLogic.mk_mem (z, HOLogic.mk_Collect (x, T, mk_prems sets z)), + HOLogic.mk_conj (HOLogic.mk_eq (y, fmap $ z), + HOLogic.mk_eq (y_copy, gmap $ z))) + + fun mk_cphi sets (z' as (x, T)) z fmap gmap y' y y'_copy y_copy = + HOLogic.mk_exists (x, T, mk_coind_body sets z' z fmap gmap y y_copy) + |> Term.absfree y'_copy + |> Term.absfree y' + |> certify lthy; + + val cphis = map9 mk_cphi + Jsetss_by_bnf Jzs' Jzs fs_Jmaps fs_copy_Jmaps Jys' Jys Jys'_copy Jys_copy; + + val coinduct = unfold_thms lthy Jset_defs + (Drule.instantiate' cTs (map SOME cphis) dtor_map_coinduct_thm); + + val goal = + HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj + (map4 mk_map_cong0 Jsetss_by_bnf Jzs fs_Jmaps fs_copy_Jmaps)); + + val thm = singleton (Proof_Context.export names_lthy lthy) + (Goal.prove_sorry lthy [] [] goal + (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jset_defs THEN + mk_mcong_tac lthy m (rtac coinduct) map_comps dtor_Jmap_thms map_cong0s + set_mapss set_hset_thmss set_hset_hset_thmsss)) + |> Thm.close_derivation + in + split_conj_thm thm + end; + + val in_Jrels = map (fn def => trans OF [def, @{thm OO_Grp_alt}] RS @{thm predicate2_eqD}) + Jrel_unabs_defs; + + val fold_Jsets = fold_thms lthy Jset_unabs_defs; + val dtor_Jset_incl_thmss = map (map fold_Jsets) hset_dtor_incl_thmss; + val dtor_set_Jset_incl_thmsss = map (map (map fold_Jsets)) hset_hset_dtor_incl_thmsss; + val dtor_Jset_induct_thms = map fold_Jsets dtor_hset_induct_thms; + val Jwit_thmss = map (map fold_Jsets) wit_thmss; + + val Jrels = mk_Jrels passiveAs passiveBs; + val Jrelphis = map (fn rel => Term.list_comb (rel, Jphis)) Jrels; val relphis = map (fn rel => Term.list_comb (rel, Jphis @ Jrelphis)) rels; - val in_Jrels = map in_rel_of_bnf Jbnfs; - - val folded_dtor_map_thms = map fold_maps dtor_map_thms; - val folded_dtor_map_o_thms = map fold_maps map_thms; - val folded_dtor_set_thmss = map (map fold_sets) dtor_set_thmss; - val folded_dtor_set_thmss' = transpose folded_dtor_set_thmss; + val Jrelpsi1s = map (fn rel => Term.list_comb (rel, Jpsi1s)) (mk_Jrels passiveAs passiveCs); + val Jrelpsi2s = map (fn rel => Term.list_comb (rel, Jpsi2s)) (mk_Jrels passiveCs passiveBs); + val Jrelpsi12s = map (fn rel => + Term.list_comb (rel, map2 (curry mk_rel_compp) Jpsi1s Jpsi2s)) Jrels; val dtor_Jrel_thms = let @@ -2718,43 +2551,11 @@ (K (mk_dtor_rel_tac lthy in_Jrels i in_rel map_comp0 map_cong0 dtor_map dtor_sets dtor_inject dtor_ctor set_map0s dtor_set_incls dtor_set_set_inclss)) |> Thm.close_derivation) - ks goals in_rels map_comps map_cong0s folded_dtor_map_thms folded_dtor_set_thmss' - dtor_inject_thms dtor_ctor_thms set_mapss dtor_set_incl_thmss - dtor_set_set_incl_thmsss + ks goals in_rels map_comps map_cong0s dtor_Jmap_thms dtor_Jset_thmss' + dtor_inject_thms dtor_ctor_thms set_mapss dtor_Jset_incl_thmss + dtor_set_Jset_incl_thmsss end; - val timer = time (timer "additional properties"); - - val ls' = if m = 1 then [0] else ls; - - val Jbnf_common_notes = - [(dtor_map_uniqueN, [fold_maps dtor_map_unique_thm])] @ - map2 (fn i => fn thm => (mk_dtor_set_inductN i, [thm])) ls' dtor_set_induct_thms - |> map (fn (thmN, thms) => - ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])); - - val Jbnf_notes = - [(dtor_mapN, map single folded_dtor_map_thms), - (dtor_relN, map single dtor_Jrel_thms), - (dtor_set_inclN, dtor_set_incl_thmss), - (dtor_set_set_inclN, map flat dtor_set_set_incl_thmsss)] @ - map2 (fn i => fn thms => (mk_dtor_setN i, map single thms)) ls' folded_dtor_set_thmss - |> maps (fn (thmN, thmss) => - map2 (fn b => fn thms => - ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])) - bs thmss) - in - (timer, Jbnfs, (folded_dtor_map_o_thms, folded_dtor_map_thms), folded_dtor_set_thmss', - dtor_set_induct_thms, dtor_Jrel_thms, Jbnf_common_notes @ Jbnf_notes, lthy) - end; - - val dtor_unfold_o_map_thms = mk_xtor_un_fold_o_map_thms Greatest_FP false m - dtor_unfold_unique_thm folded_dtor_map_o_thms (map (mk_pointfree lthy) dtor_unfold_thms) - sym_map_comps map_cong0s; - val dtor_corec_o_map_thms = mk_xtor_un_fold_o_map_thms Greatest_FP true m - dtor_corec_unique_thm folded_dtor_map_o_thms (map (mk_pointfree lthy) dtor_corec_thms) - sym_map_comps map_cong0s; - val passiveABs = map2 (curry HOLogic.mk_prodT) passiveAs passiveBs; val zip_ranTs = passiveABs @ prodTsTs'; val allJphis = Jphis @ activeJphis; @@ -2773,19 +2574,17 @@ val all_fsts = fstABs @ fstsTsTs'; val map_all_fsts = map2 (fn Ds => fn bnf => Term.list_comb (mk_map_of_bnf Ds zip_ranTs (passiveAs @ Ts) bnf, all_fsts)) Dss bnfs; - val Jmap_fsts = map2 (fn bnf => fn T => if m = 0 then HOLogic.id_const T - else Term.list_comb (mk_map_of_bnf deads passiveABs passiveAs bnf, fstABs)) Jbnfs Ts; + val Jmap_fsts = map2 (fn map => fn T => if m = 0 then HOLogic.id_const T + else Term.list_comb (map, fstABs)) (mk_Jmaps passiveABs passiveAs) Ts; val sndABs = map snd_const passiveABs; val all_snds = sndABs @ sndsTsTs'; val map_all_snds = map2 (fn Ds => fn bnf => Term.list_comb (mk_map_of_bnf Ds zip_ranTs (passiveBs @ Ts') bnf, all_snds)) Dss bnfs; - val Jmap_snds = map2 (fn bnf => fn T => if m = 0 then HOLogic.id_const T - else Term.list_comb (mk_map_of_bnf deads passiveABs passiveBs bnf, sndABs)) Jbnfs Ts; + val Jmap_snds = map2 (fn map => fn T => if m = 0 then HOLogic.id_const T + else Term.list_comb (map, sndABs)) (mk_Jmaps passiveABs passiveBs) Ts; val zip_unfolds = map (mk_unfold zip_zTs (map HOLogic.mk_split zips)) ks; - val zip_setss = map (mk_sets_of_bnf (replicate m deads) (replicate m passiveABs)) Jbnfs - |> transpose; - val in_Jrels = map in_rel_of_bnf Jbnfs; + val zip_setss = mk_Jsetss passiveABs |> transpose; val Jrel_coinduct_tac = let @@ -2813,7 +2612,7 @@ (map6 (mk_helper_coind_concl false) activeJphis Jzs Jz's_copy Jz's Jmap_snds zip_unfolds)); val helper_coind_tac = mk_rel_coinduct_coind_tac m dtor_map_coinduct_thm ks map_comps - map_cong0s map_arg_cong_thms set_mapss dtor_unfold_thms folded_dtor_map_thms; + map_cong0s map_arg_cong_thms set_mapss dtor_unfold_thms dtor_Jmap_thms; fun mk_helper_coind_thms vars concl = Goal.prove_sorry lthy [] [] (fold_rev Logic.all (Jphis @ activeJphis @ vars @ zips) @@ -2845,22 +2644,111 @@ (mk_rel_coinduct_ind_tac m ks dtor_unfold_thms set_mapss j set_induct) |> Thm.close_derivation |> split_conj_thm) - mk_helper_ind_concls ls dtor_set_induct_thms + mk_helper_ind_concls ls dtor_Jset_induct_thms |> transpose; in mk_rel_coinduct_tac in_rels in_Jrels helper_ind_thmss helper_coind1_thms helper_coind2_thms end; - - val Jrels = if m = 0 then map HOLogic.eq_const Ts - else map (mk_rel_of_bnf deads passiveAs passiveBs) Jbnfs; + val Jrel_coinduct_thm = mk_rel_xtor_co_induct_thm Greatest_FP rels activeJphis Jrels Jphis Jzs Jz's dtors dtor's Jrel_coinduct_tac lthy; + val le_Jrel_OO_thm = + let + fun mk_le_Jrel_OO Jrelpsi1 Jrelpsi2 Jrelpsi12 = + mk_leq (mk_rel_compp (Jrelpsi1, Jrelpsi2)) Jrelpsi12; + val goals = map3 mk_le_Jrel_OO Jrelpsi1s Jrelpsi2s Jrelpsi12s; + + val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj goals); + in + singleton (Proof_Context.export names_lthy lthy) + (Goal.prove_sorry lthy [] [] goal + (K (mk_le_rel_OO_tac Jrel_coinduct_thm dtor_Jrel_thms rel_OOs))) + |> Thm.close_derivation + end; + + val timer = time (timer "helpers for BNF properties"); + + val map_id0_tacs = + map2 (K oo mk_map_id0_tac Jmap_thms) dtor_unfold_unique_thms unfold_dtor_thms; + val map_comp0_tacs = map (fn thm => K (rtac (thm RS sym) 1)) Jmap_comp0_thms; + val map_cong0_tacs = map (mk_map_cong0_tac m) map_cong0_thms; + val set_nat_tacss = + map2 (map2 (fn def => fn col => fn {context = ctxt, prems = _} => + unfold_thms_tac ctxt Jset_defs THEN mk_set_map0_tac def col)) + hset_defss (transpose col_natural_thmss); + + val Jbd_card_orders = map (fn def => fold_thms lthy [def] sbd_card_order) Jbd_defs; + val Jbd_Cinfinites = map (fn def => fold_thms lthy [def] sbd_Cinfinite) Jbd_defs; + + val bd_co_tacs = map (fn thm => K (rtac thm 1)) Jbd_card_orders; + val bd_cinf_tacs = map (fn thm => K (rtac (thm RS conjunct1) 1)) Jbd_Cinfinites; + + val set_bd_tacss = + map3 (fn Cinf => map2 (fn def => fn col => fn {context = ctxt, prems = _} => + unfold_thms_tac ctxt Jset_defs THEN mk_set_bd_tac Cinf def col)) + Jbd_Cinfinites hset_defss (transpose col_bd_thmss); + + val le_rel_OO_tacs = map (fn i => K (rtac (le_Jrel_OO_thm RS mk_conjunctN n i) 1)) ks; + + val rel_OO_Grp_tacs = map (fn def => K (rtac def 1)) Jrel_unabs_defs; + + val tacss = map9 zip_axioms map_id0_tacs map_comp0_tacs map_cong0_tacs set_nat_tacss + bd_co_tacs bd_cinf_tacs set_bd_tacss le_rel_OO_tacs rel_OO_Grp_tacs; + + fun wit_tac thms {context = ctxt, prems = _} = unfold_thms_tac ctxt (flat Jwit_defss) THEN + mk_wit_tac n dtor_ctor_thms (flat dtor_Jset_thmss) (maps wit_thms_of_bnf bnfs) thms ctxt; + + val (Jbnfs, lthy) = + fold_map6 (fn tacs => fn map_b => fn rel_b => fn set_bs => fn Jwit_thms => fn consts => + fn lthy => + bnf_def Do_Inline (user_policy Note_Some) I tacs (wit_tac Jwit_thms) (SOME deads) + map_b rel_b set_bs consts lthy + |> register_bnf (Local_Theory.full_name lthy b)) + tacss map_bs rel_bs set_bss Jwit_thmss + ((((((bs ~~ Ts) ~~ Jmaps) ~~ Jsetss_by_bnf) ~~ Jbds) ~~ Jwitss) ~~ map SOME Jrels) + lthy; + + val timer = time (timer "registered new codatatypes as BNFs"); + + val ls' = if m = 1 then [0] else ls; + + val Jbnf_common_notes = + [(dtor_map_uniqueN, [dtor_Jmap_unique_thm])] @ + map2 (fn i => fn thm => (mk_dtor_set_inductN i, [thm])) ls' dtor_Jset_induct_thms + |> map (fn (thmN, thms) => + ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])); + + val Jbnf_notes = + [(dtor_mapN, map single dtor_Jmap_thms), + (dtor_relN, map single dtor_Jrel_thms), + (dtor_set_inclN, dtor_Jset_incl_thmss), + (dtor_set_set_inclN, map flat dtor_set_Jset_incl_thmsss)] @ + map2 (fn i => fn thms => (mk_dtor_setN i, map single thms)) ls' dtor_Jset_thmss + |> maps (fn (thmN, thmss) => + map2 (fn b => fn thms => + ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])) + bs thmss) + in + (timer, Jbnfs, (Jmap_thms, dtor_Jmap_thms), dtor_Jset_thmss', + dtor_Jrel_thms, Jrel_coinduct_thm, Jbnf_common_notes @ Jbnf_notes, lthy) + end; + + val dtor_unfold_o_Jmap_thms = mk_xtor_un_fold_o_map_thms Greatest_FP false m + dtor_unfold_unique_thm dtor_Jmap_o_thms (map (mk_pointfree lthy) dtor_unfold_thms) + sym_map_comps map_cong0s; + val dtor_corec_o_Jmap_thms = mk_xtor_un_fold_o_map_thms Greatest_FP true m + dtor_corec_unique_thm dtor_Jmap_o_thms (map (mk_pointfree lthy) dtor_corec_thms) + sym_map_comps map_cong0s; + val rels = map2 (fn Ds => mk_rel_of_bnf Ds allAs allBs') Dss bnfs; + val dtor_unfold_transfer_thms = - mk_un_fold_transfer_thms Greatest_FP rels activephis Jrels Jphis + mk_un_fold_transfer_thms Greatest_FP rels activephis + (if m = 0 then map HOLogic.eq_const Ts + else map (mk_rel_of_bnf deads passiveAs passiveBs) Jbnfs) Jphis (mk_unfolds passiveAs activeAs) (mk_unfolds passiveBs activeBs) (mk_unfold_transfer_tac m Jrel_coinduct_thm (map map_transfer_of_bnf bnfs) dtor_unfold_thms) @@ -2887,8 +2775,8 @@ (dtor_unfoldN, dtor_unfold_thms), (dtor_unfold_uniqueN, dtor_unfold_unique_thms), (dtor_corec_uniqueN, dtor_corec_unique_thms), - (dtor_unfold_o_mapN, dtor_unfold_o_map_thms), - (dtor_corec_o_mapN, dtor_corec_o_map_thms)] + (dtor_unfold_o_mapN, dtor_unfold_o_Jmap_thms), + (dtor_corec_o_mapN, dtor_corec_o_Jmap_thms)] |> map (apsnd (map single)) |> maps (fn (thmN, thmss) => map2 (fn b => fn thms => @@ -2905,10 +2793,10 @@ xtor_co_induct = dtor_coinduct_thm, dtor_ctors = dtor_ctor_thms, ctor_dtors = ctor_dtor_thms, ctor_injects = ctor_inject_thms, dtor_injects = dtor_inject_thms, - xtor_map_thms = folded_dtor_map_thms, xtor_set_thmss = folded_dtor_set_thmss', + xtor_map_thms = dtor_Jmap_thms, xtor_set_thmss = dtor_Jset_thmss', xtor_rel_thms = dtor_Jrel_thms, xtor_co_iter_thmss = transpose [dtor_unfold_thms, dtor_corec_thms], - xtor_co_iter_o_map_thmss = transpose [dtor_unfold_o_map_thms, dtor_corec_o_map_thms], + xtor_co_iter_o_map_thmss = transpose [dtor_unfold_o_Jmap_thms, dtor_corec_o_Jmap_thms], rel_xtor_co_induct_thm = Jrel_coinduct_thm}, lthy |> Local_Theory.notes (maybe_conceal_notes (common_notes @ notes @ Jbnf_notes)) |> snd) end; diff -r fac0c76bbda2 -r af71b753c459 src/HOL/BNF/Tools/bnf_gfp_tactics.ML --- a/src/HOL/BNF/Tools/bnf_gfp_tactics.ML Fri Dec 20 21:09:01 2013 +0100 +++ b/src/HOL/BNF/Tools/bnf_gfp_tactics.ML Wed Dec 18 11:03:40 2013 +0100 @@ -23,8 +23,6 @@ val mk_coalg_final_tac: int -> thm -> thm list -> thm list -> thm list list -> thm list list -> tactic val mk_coalg_set_tac: thm -> tactic - val mk_coalg_thePull_tac: int -> thm -> thm list -> thm list list -> (int -> tactic) list -> - {prems: 'a, context: Proof.context} -> tactic val mk_coind_wit_tac: thm -> thm list -> thm list -> thm list -> {prems: 'a, context: Proof.context} -> tactic val mk_col_bd_tac: int -> int -> cterm option list -> thm list -> thm list -> thm -> thm -> @@ -37,7 +35,6 @@ val mk_corec_unique_mor_tac: thm list -> thm list -> thm -> {prems: 'a, context: Proof.context} -> tactic val mk_dtor_map_coinduct_tac: int -> int list -> thm -> thm -> tactic - val mk_dtor_set_tac: int -> thm -> thm -> thm list -> tactic val mk_dtor_coinduct_tac: int -> thm -> thm -> thm list -> tactic val mk_dtor_rel_tac: Proof.context -> thm list -> int -> thm -> thm -> thm -> thm -> thm list -> thm -> thm -> thm list -> thm list -> thm list list -> tactic @@ -50,12 +47,12 @@ val mk_incl_lsbis_tac: int -> int -> thm -> tactic val mk_length_Lev'_tac: thm -> tactic val mk_length_Lev_tac: Proof.context -> cterm option list -> thm list -> thm list -> tactic - val mk_map_comp0_tac: int -> int -> thm list -> thm list -> thm list -> thm -> tactic + val mk_map_comp0_tac: thm list -> thm list -> thm -> tactic val mk_mcong_tac: Proof.context -> int -> (int -> tactic) -> thm list -> thm list -> thm list -> thm list list -> thm list list -> thm list list list -> tactic val mk_map_id0_tac: thm list -> thm -> thm -> tactic val mk_map_tac: int -> int -> ctyp option -> thm -> thm -> thm -> tactic - val mk_dtor_map_unique_tac: thm -> thm list -> {prems: 'a, context: Proof.context} -> tactic + val mk_dtor_map_unique_tac: thm -> thm list -> Proof.context -> tactic val mk_mor_Abs_tac: thm list -> thm list -> {prems: 'a, context: Proof.context} -> tactic val mk_mor_Rep_tac: int -> thm list -> thm list -> thm list -> thm list list -> thm list -> thm list -> {prems: 'a, context: Proof.context} -> tactic @@ -73,19 +70,9 @@ val mk_mor_incl_tac: thm -> thm list -> tactic val mk_mor_str_tac: 'a list -> thm -> tactic val mk_mor_sum_case_tac: 'a list -> thm -> tactic - val mk_mor_thePull_fst_tac: int -> thm -> thm list -> thm list -> (int -> tactic) list -> - {prems: thm list, context: Proof.context} -> tactic - val mk_mor_thePull_snd_tac: int -> thm -> thm list -> thm list -> (int -> tactic) list -> - {prems: thm list, context: Proof.context} -> tactic - val mk_mor_thePull_pick_tac: thm -> thm list -> thm list -> - {prems: 'a, context: Proof.context} -> tactic val mk_mor_unfold_tac: int -> thm -> thm list -> thm list -> thm list -> thm list -> thm list -> thm list -> tactic val mk_prefCl_Lev_tac: Proof.context -> cterm option list -> thm list -> thm list -> tactic - val mk_pickWP_assms_tac: thm list -> thm list -> thm -> (int -> tactic) - val mk_pick_col_tac: int -> int -> cterm option list -> thm list -> thm list -> thm list -> - thm list list -> thm list -> (int -> tactic) list -> {prems: 'a, context: Proof.context} -> - tactic val mk_raw_coind_tac: thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm list -> thm list -> thm list -> thm -> thm list -> tactic val mk_rel_coinduct_tac: thm list -> thm list -> thm list list -> thm list -> thm list -> @@ -102,8 +89,8 @@ val mk_set_hset_incl_hset_tac: int -> thm list -> thm -> int -> tactic val mk_set_image_Lev_tac: Proof.context -> cterm option list -> thm list -> thm list -> thm list -> thm list -> thm list list -> thm list list -> tactic - val mk_set_incl_hin_tac: thm list -> tactic val mk_set_incl_hset_tac: thm -> thm -> tactic + val mk_set_ge_tac: int -> thm -> thm list -> tactic val mk_set_le_tac: int -> thm -> thm list -> thm list list -> tactic val mk_set_map0_tac: thm -> thm -> tactic val mk_set_rv_Lev_tac: Proof.context -> int -> cterm option list -> thm list -> thm list -> @@ -111,10 +98,8 @@ val mk_unfold_unique_mor_tac: thm list -> thm -> thm -> thm list -> tactic val mk_unfold_transfer_tac: int -> thm -> thm list -> thm list -> {prems: thm list, context: Proof.context} -> tactic - val mk_unique_mor_tac: thm list -> thm -> tactic - val mk_wit_tac: int -> thm list -> thm list -> thm list -> thm list -> - {prems: 'a, context: Proof.context} -> tactic - val mk_wpull_tac: int -> thm -> thm -> thm -> thm -> thm -> thm list -> thm list -> tactic + val mk_wit_tac: int -> thm list -> thm list -> thm list -> thm list -> Proof.context -> tactic + val mk_le_rel_OO_tac: thm -> thm list -> thm list -> tactic end; structure BNF_GFP_Tactics : BNF_GFP_TACTICS = @@ -206,11 +191,6 @@ mk_UnIN n i] @ [etac @{thm UN_I}, atac]) 1; -fun mk_set_incl_hin_tac incls = - if null incls then rtac subset_UNIV 1 - else EVERY' [rtac subsetI, rtac CollectI, - CONJ_WRAP' (fn incl => EVERY' [rtac subset_trans, etac incl, atac]) incls] 1; - fun mk_hset_rec_minimal_tac m cts rec_0s rec_Sucs {context = ctxt, prems = _} = EVERY' [rtac (Drule.instantiate' [] cts nat_induct), REPEAT_DETERM o rtac allI, @@ -940,12 +920,6 @@ (Rep_injects ~~ (equiv_LSBISs ~~ (incl_lsbiss ~~ lsbis_incls)))] 1 end; -fun mk_unique_mor_tac raw_coinds bis = - CONJ_WRAP' (fn raw_coind => - EVERY' [rtac impI, rtac (bis RS raw_coind RS set_mp RS @{thm IdD}), atac, - etac conjunct1, atac, etac conjunct2, rtac @{thm image2_eqI}, rtac refl, rtac refl, atac]) - raw_coinds 1; - fun mk_unfold_unique_mor_tac raw_coinds bis mor unfold_defs = CONJ_WRAP' (fn (raw_coind, unfold_def) => EVERY' [rtac ext, etac (bis RS raw_coind RS set_mp RS @{thm IdD}), rtac mor, @@ -1023,8 +997,8 @@ EVERY' (map (fn thm => EVERY' [etac @{thm UN_E}, etac thm, atac]) set_hset_hsets)]) (1 upto n) set_hsets set_hset_hsetss)] 1; -fun mk_dtor_set_tac n set_le set_incl_hset set_hset_incl_hsets = - EVERY' [rtac equalityI, rtac set_le, rtac @{thm Un_least}, rtac set_incl_hset, +fun mk_set_ge_tac n set_incl_hset set_hset_incl_hsets = + EVERY' [rtac @{thm Un_least}, rtac set_incl_hset, REPEAT_DETERM_N (n - 1) o rtac @{thm Un_least}, EVERY' (map (fn thm => rtac @{thm UN_least} THEN' etac thm) set_hset_incl_hsets)] 1; @@ -1032,20 +1006,15 @@ EVERY' [rtac (unfold_unique RS trans), EVERY' (map (rtac o mk_sym) maps), rtac unfold_dtor] 1; -fun mk_map_comp0_tac m n maps map_comp0s map_cong0s unfold_unique = - EVERY' [rtac unfold_unique, - EVERY' (map3 (fn map_thm => fn map_comp0 => fn map_cong0 => +fun mk_map_comp0_tac maps map_comp0s map_unique = + EVERY' [rtac map_unique, + EVERY' (map2 (fn map_thm => fn map_comp0 => EVERY' (map rtac - ([@{thm o_assoc} RS trans, - @{thm arg_cong2[of _ _ _ _ "op o"]} OF [map_comp0 RS sym, refl] RS trans, - @{thm o_assoc} RS trans RS sym, + [@{thm o_assoc} RS trans, @{thm arg_cong2[of _ _ _ _ "op o"]} OF [map_thm, refl] RS trans, @{thm o_assoc} RS sym RS trans, map_thm RS arg_cong RS trans, @{thm o_assoc} RS trans, - @{thm arg_cong2[of _ _ _ _ "op o"]} OF [map_comp0 RS sym, refl] RS trans, - ext, o_apply RS trans, o_apply RS trans RS sym, map_cong0] @ - replicate m (@{thm id_o} RS fun_cong) @ - replicate n (@{thm o_id} RS fun_cong)))) - maps map_comp0s map_cong0s)] 1; + @{thm arg_cong2[of _ _ _ _ "op o"]} OF [map_comp0 RS sym, refl]])) + maps map_comp0s)] 1; fun mk_mcong_tac ctxt m coinduct_tac map_comps dtor_maps map_cong0s set_map0ss set_hsetss set_hset_hsetsss = @@ -1082,7 +1051,7 @@ rtac conjI, rtac refl, rtac refl]) ks]) 1 end -fun mk_dtor_map_unique_tac unfold_unique sym_map_comps {context = ctxt, prems = _} = +fun mk_dtor_map_unique_tac unfold_unique sym_map_comps ctxt = rtac unfold_unique 1 THEN unfold_thms_tac ctxt (sym_map_comps @ @{thms o_assoc id_o o_id}) THEN ALLGOALS (etac sym); @@ -1135,128 +1104,16 @@ @{thm UNION_Cinfinite_bound}, ordIso_ordLeq_trans, @{thm card_of_nat}, @{thm natLeq_ordLeq_cinfinite}, sbd_Cinfinite, ballI, col_bd, sbd_Cinfinite]) 1; -fun mk_pickWP_assms_tac set_incl_hsets set_incl_hins map_eq = - let - val m = length set_incl_hsets; - in - EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac CollectI, - EVERY' (map (fn thm => rtac conjI THEN' etac (thm RS @{thm subset_trans})) set_incl_hsets), - CONJ_WRAP' (fn thm => rtac thm THEN' REPEAT_DETERM_N m o atac) set_incl_hins, - REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac CollectI, - EVERY' (map (fn thm => rtac conjI THEN' etac (thm RS @{thm subset_trans})) set_incl_hsets), - CONJ_WRAP' (fn thm => rtac thm THEN' REPEAT_DETERM_N m o atac) set_incl_hins, - REPEAT_DETERM o eresolve_tac [CollectE, conjE], etac map_eq] - end; - -fun mk_coalg_thePull_tac m coalg_def map_wpulls set_map0ss pickWP_assms_tacs - {context = ctxt, prems = _} = - unfold_thms_tac ctxt [coalg_def] THEN - CONJ_WRAP' (fn (map_wpull, (pickWP_assms_tac, set_map0s)) => - EVERY' [rtac ballI, dtac @{thm set_mp[OF equalityD1[OF thePull_def]]}, - REPEAT_DETERM o eresolve_tac [CollectE, @{thm prod_caseE}], - hyp_subst_tac ctxt, rtac rev_mp, rtac (map_wpull RS @{thm pickWP(1)}), - EVERY' (map (etac o mk_conjunctN m) (1 upto m)), - pickWP_assms_tac, - SELECT_GOAL (unfold_thms_tac ctxt @{thms o_apply prod.cases}), rtac impI, - REPEAT_DETERM o eresolve_tac [CollectE, conjE], - rtac CollectI, - REPEAT_DETERM_N m o (rtac conjI THEN' rtac subset_UNIV), - CONJ_WRAP' (fn set_map0 => - EVERY' [rtac ord_eq_le_trans, rtac trans, rtac set_map0, - rtac trans_fun_cong_image_id_id_apply, atac]) - (drop m set_map0s)]) - (map_wpulls ~~ (pickWP_assms_tacs ~~ set_map0ss)) 1; - -fun mk_mor_thePull_nth_tac conv pick m mor_def map_wpulls map_comp0s pickWP_assms_tacs - {context = ctxt, prems = _: thm list} = - let - val n = length map_comp0s; - in - unfold_thms_tac ctxt [mor_def] THEN - EVERY' [rtac conjI, - CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) (1 upto n), - CONJ_WRAP' (fn (map_wpull, (pickWP_assms_tac, map_comp0)) => - EVERY' [rtac ballI, dtac @{thm set_mp[OF equalityD1[OF thePull_def]]}, - REPEAT_DETERM o eresolve_tac [CollectE, @{thm prod_caseE}, conjE], - hyp_subst_tac ctxt, - SELECT_GOAL (unfold_thms_tac ctxt @{thms o_apply prod.cases}), - rtac (map_comp0 RS trans), - SELECT_GOAL (unfold_thms_tac ctxt (conv :: @{thms o_id id_o})), - rtac (map_wpull RS pick), REPEAT_DETERM_N m o atac, - pickWP_assms_tac]) - (map_wpulls ~~ (pickWP_assms_tacs ~~ map_comp0s))] 1 - end; - -val mk_mor_thePull_fst_tac = mk_mor_thePull_nth_tac @{thm fst_conv} @{thm pickWP(2)}; -val mk_mor_thePull_snd_tac = mk_mor_thePull_nth_tac @{thm snd_conv} @{thm pickWP(3)}; +fun mk_le_rel_OO_tac coinduct rel_Jrels rel_OOs = + EVERY' (rtac coinduct :: map2 (fn rel_Jrel => fn rel_OO => + let val Jrel_imp_rel = rel_Jrel RS iffD1; + in + EVERY' [rtac (rel_OO RS sym RS @{thm eq_refl} RS @{thm predicate2D}), etac @{thm relcomppE}, + rtac @{thm relcomppI}, etac Jrel_imp_rel, etac Jrel_imp_rel] + end) + rel_Jrels rel_OOs) 1; -fun mk_mor_thePull_pick_tac mor_def unfolds map_comp0s {context = ctxt, prems = _} = - unfold_thms_tac ctxt [mor_def, @{thm thePull_def}] THEN rtac conjI 1 THEN - CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) unfolds 1 THEN - CONJ_WRAP' (fn (unfold, map_comp0) => - EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, @{thm prod_caseE}, conjE], - hyp_subst_tac ctxt, - SELECT_GOAL (unfold_thms_tac ctxt (unfold :: map_comp0 :: @{thms comp_def id_def})), - rtac refl]) - (unfolds ~~ map_comp0s) 1; - -fun mk_pick_col_tac m j cts rec_0s rec_Sucs unfolds set_map0ss map_wpulls pickWP_assms_tacs - {context = ctxt, prems = _} = - let - val n = length rec_0s; - val ks = n downto 1; - in - EVERY' [rtac (Drule.instantiate' [] cts nat_induct), - REPEAT_DETERM o rtac allI, - CONJ_WRAP' (fn thm => EVERY' - [rtac impI, rtac ord_eq_le_trans, rtac thm, rtac @{thm empty_subsetI}]) rec_0s, - REPEAT_DETERM o rtac allI, - CONJ_WRAP' (fn (rec_Suc, ((unfold, set_map0s), (map_wpull, pickWP_assms_tac))) => - EVERY' [rtac impI, dtac @{thm set_mp[OF equalityD1[OF thePull_def]]}, - REPEAT_DETERM o eresolve_tac [CollectE, @{thm prod_caseE}], - hyp_subst_tac ctxt, rtac rev_mp, rtac (map_wpull RS @{thm pickWP(1)}), - EVERY' (map (etac o mk_conjunctN m) (1 upto m)), - pickWP_assms_tac, - rtac impI, REPEAT_DETERM o eresolve_tac [CollectE, conjE], - rtac ord_eq_le_trans, rtac rec_Suc, - rtac @{thm Un_least}, - SELECT_GOAL (unfold_thms_tac ctxt [unfold, nth set_map0s (j - 1), - @{thm prod.cases}]), - etac ord_eq_le_trans_trans_fun_cong_image_id_id_apply, - CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least})) (fn (i, set_map0) => - EVERY' [rtac @{thm UN_least}, - SELECT_GOAL (unfold_thms_tac ctxt [unfold, set_map0, @{thm prod.cases}]), - etac imageE, hyp_subst_tac ctxt, REPEAT_DETERM o etac allE, - dtac (mk_conjunctN n i), etac mp, etac set_mp, atac]) - (ks ~~ rev (drop m set_map0s))]) - (rec_Sucs ~~ ((unfolds ~~ set_map0ss) ~~ (map_wpulls ~~ pickWP_assms_tacs)))] 1 - end; - -fun mk_wpull_tac m coalg_thePull mor_thePull_fst mor_thePull_snd mor_thePull_pick - mor_unique pick_cols hset_defs = - EVERY' [rtac (@{thm wpull_def} RS iffD2), REPEAT_DETERM o rtac allI, rtac impI, - REPEAT_DETERM o etac conjE, rtac bexI, rtac conjI, - rtac box_equals, rtac mor_unique, - rtac coalg_thePull, REPEAT_DETERM_N (m - 1) o etac conjI, atac, - rtac mor_thePull_pick, REPEAT_DETERM_N (m - 1) o etac conjI, atac, - rtac mor_thePull_fst, REPEAT_DETERM_N (m - 1) o etac conjI, atac, - rtac @{thm set_mp[OF equalityD2[OF thePull_def]]}, rtac CollectI, - rtac @{thm prod_caseI}, etac conjI, etac conjI, atac, rtac o_apply, rtac @{thm fst_conv}, - rtac box_equals, rtac mor_unique, - rtac coalg_thePull, REPEAT_DETERM_N (m - 1) o etac conjI, atac, - rtac mor_thePull_pick, REPEAT_DETERM_N (m - 1) o etac conjI, atac, - rtac mor_thePull_snd, REPEAT_DETERM_N (m - 1) o etac conjI, atac, - rtac @{thm set_mp[OF equalityD2[OF thePull_def]]}, rtac CollectI, - rtac @{thm prod_caseI}, etac conjI, etac conjI, atac, rtac o_apply, rtac @{thm snd_conv}, - rtac CollectI, - CONJ_WRAP' (fn (pick, def) => - EVERY' [rtac (def RS ord_eq_le_trans), rtac @{thm UN_least}, - rtac pick, REPEAT_DETERM_N (m - 1) o etac conjI, atac, - rtac @{thm set_mp[OF equalityD2[OF thePull_def]]}, rtac CollectI, - rtac @{thm prod_caseI}, etac conjI, etac conjI, atac]) - (pick_cols ~~ hset_defs)] 1; - -fun mk_wit_tac n dtor_ctors dtor_set wit coind_wits {context = ctxt, prems = _} = +fun mk_wit_tac n dtor_ctors dtor_set wit coind_wits ctxt = ALLGOALS (TRY o (eresolve_tac coind_wits THEN' rtac refl)) THEN REPEAT_DETERM (atac 1 ORELSE EVERY' [dtac set_rev_mp, rtac equalityD1, resolve_tac dtor_set, diff -r fac0c76bbda2 -r af71b753c459 src/HOL/BNF/Tools/bnf_gfp_util.ML --- a/src/HOL/BNF/Tools/bnf_gfp_util.ML Fri Dec 20 21:09:01 2013 +0100 +++ b/src/HOL/BNF/Tools/bnf_gfp_util.ML Wed Dec 18 11:03:40 2013 +0100 @@ -24,14 +24,12 @@ val mk_fromCard: term -> term -> term val mk_list_rec: term -> term -> term val mk_nat_rec: term -> term -> term - val mk_pickWP: term -> term -> term -> term -> term -> term val mk_prefCl: term -> term val mk_prefixeq: term -> term -> term val mk_proj: term -> term val mk_quotient: term -> term -> term val mk_shift: term -> term -> term val mk_size: term -> term - val mk_thePull: term -> term -> term -> term -> term val mk_toCard: term -> term -> term val mk_undefined: typ -> term val mk_univ: term -> term @@ -160,29 +158,6 @@ Const (@{const_name list_rec}, T --> consT --> HOLogic.listT U --> T) $ Nil $ Cons end; -fun mk_thePull B1 B2 f1 f2 = - let - val fT1 = fastype_of f1; - val fT2 = fastype_of f2; - val BT1 = domain_type fT1; - val BT2 = domain_type fT2; - in - Const (@{const_name thePull}, HOLogic.mk_setT BT1 --> HOLogic.mk_setT BT2 --> fT1 --> fT2 --> - mk_relT (BT1, BT2)) $ B1 $ B2 $ f1 $ f2 - end; - -fun mk_pickWP A f1 f2 b1 b2 = - let - val fT1 = fastype_of f1; - val fT2 = fastype_of f2; - val AT = domain_type fT1; - val BT1 = range_type fT1; - val BT2 = range_type fT2; - in - Const (@{const_name pickWP}, HOLogic.mk_setT AT --> fT1 --> fT2 --> BT1 --> BT2 --> AT) $ - A $ f1 $ f2 $ b1 $ b2 - end; - fun mk_InN_not_InM 1 _ = @{thm Inl_not_Inr} | mk_InN_not_InM n m = if n > m then mk_InN_not_InM m n RS @{thm not_sym} diff -r fac0c76bbda2 -r af71b753c459 src/HOL/BNF/Tools/bnf_lfp.ML --- a/src/HOL/BNF/Tools/bnf_lfp.ML Fri Dec 20 21:09:01 2013 +0100 +++ b/src/HOL/BNF/Tools/bnf_lfp.ML Wed Dec 18 11:03:40 2013 +0100 @@ -55,15 +55,15 @@ val passives = map fst (subtract (op = o apsnd TFree) deads resBs); (* tvars *) - val ((((((passiveAs, activeAs), passiveBs), activeBs), activeCs), passiveXs), passiveYs) = + val (((((passiveAs, activeAs), passiveBs), activeBs), passiveCs), activeCs) = names_lthy |> variant_tfrees passives ||>> mk_TFrees n ||>> variant_tfrees passives ||>> mk_TFrees n + ||>> variant_tfrees passives ||>> mk_TFrees n - ||>> mk_TFrees m - ||> fst o mk_TFrees m; + |> fst; val allAs = passiveAs @ activeAs; val allBs' = passiveBs @ activeBs; @@ -174,8 +174,9 @@ val map_cong0s = map map_cong0_of_bnf bnfs; val map_id0s = map map_id0_of_bnf bnfs; val map_ids = map map_id_of_bnf bnfs; - val map_wpulls = map map_wpull_of_bnf bnfs; val set_mapss = map set_map_of_bnf bnfs; + val rel_mono_strongs = map rel_mono_strong_of_bnf bnfs; + val rel_OOs = map rel_OO_of_bnf bnfs; val timer = time (timer "Extracted terms & thms"); @@ -1402,16 +1403,20 @@ trans OF [ctor_inject, rel_eq_of_bnf bnf RS @{thm predicate2_eqD} RS sym]; val IphiTs = map2 mk_pred2T passiveAs passiveBs; + val Ipsi1Ts = map2 mk_pred2T passiveAs passiveCs; + val Ipsi2Ts = map2 mk_pred2T passiveCs passiveBs; val activephiTs = map2 mk_pred2T activeAs activeBs; val activeIphiTs = map2 mk_pred2T Ts Ts'; - val (((Iphis, activephis), activeIphis), names_lthy) = names_lthy + val (((((Iphis, Ipsi1s), Ipsi2s), activephis), activeIphis), names_lthy) = names_lthy |> mk_Frees "R" IphiTs + ||>> mk_Frees "R" Ipsi1Ts + ||>> mk_Frees "Q" Ipsi2Ts ||>> mk_Frees "S" activephiTs ||>> mk_Frees "IR" activeIphiTs; val rels = map2 (fn Ds => mk_rel_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs; (*register new datatypes as BNFs*) - val (timer, Ibnfs, (folded_ctor_map_o_thms, folded_ctor_map_thms), folded_ctor_set_thmss', + val (timer, Ibnfs, (ctor_Imap_o_thms, ctor_Imap_thms), ctor_Iset_thmss', ctor_Irel_thms, Ibnf_notes, lthy) = if m = 0 then (timer, replicate n DEADID_bnf, @@ -1419,31 +1424,13 @@ replicate n [], map2 mk_ctor_Irel_DEADID_thm ctor_inject_thms bnfs, [], lthy) else let val fTs = map2 (curry op -->) passiveAs passiveBs; - val f1Ts = map2 (curry op -->) passiveAs passiveYs; - val f2Ts = map2 (curry op -->) passiveBs passiveYs; - val p1Ts = map2 (curry op -->) passiveXs passiveAs; - val p2Ts = map2 (curry op -->) passiveXs passiveBs; val uTs = map2 (curry op -->) Ts Ts'; - val B1Ts = map HOLogic.mk_setT passiveAs; - val B2Ts = map HOLogic.mk_setT passiveBs; - val AXTs = map HOLogic.mk_setT passiveXs; - val XTs = mk_Ts passiveXs; - val YTs = mk_Ts passiveYs; - val (((((((((((((fs, fs'), fs_copy), us), - B1s), B2s), AXs), (xs, xs')), f1s), f2s), p1s), p2s), (ys, ys')), + val (((((fs, fs'), fs_copy), us), (ys, ys')), names_lthy) = names_lthy |> mk_Frees' "f" fTs ||>> mk_Frees "f" fTs ||>> mk_Frees "u" uTs - ||>> mk_Frees "B1" B1Ts - ||>> mk_Frees "B2" B2Ts - ||>> mk_Frees "A" AXTs - ||>> mk_Frees' "x" XTs - ||>> mk_Frees "f1" f1Ts - ||>> mk_Frees "f2" f2Ts - ||>> mk_Frees "p1" p1Ts - ||>> mk_Frees "p2" p2Ts ||>> mk_Frees' "y" passiveAs; val map_FTFT's = map2 (fn Ds => @@ -1456,51 +1443,9 @@ mk_fold Ts (map2 (mk_map_fold_arg fs Ts') ctors (mk_maps Ts')); val pmapsABT' = mk_passive_maps passiveAs passiveBs; val fs_maps = map (mk_map Ts fs Ts' ctor's pmapsABT') ks; - val fs_copy_maps = map (mk_map Ts fs_copy Ts' ctor's pmapsABT') ks; - val Yctors = mk_ctors passiveYs; - val f1s_maps = map (mk_map Ts f1s YTs Yctors (mk_passive_maps passiveAs passiveYs)) ks; - val f2s_maps = map (mk_map Ts' f2s YTs Yctors (mk_passive_maps passiveBs passiveYs)) ks; - val p1s_maps = map (mk_map XTs p1s Ts ctors (mk_passive_maps passiveXs passiveAs)) ks; - val p2s_maps = map (mk_map XTs p2s Ts' ctor's (mk_passive_maps passiveXs passiveBs)) ks; - - val (ctor_map_thms, ctor_map_o_thms) = - let - fun mk_goal fs_map map ctor ctor' = fold_rev Logic.all fs - (mk_Trueprop_eq (HOLogic.mk_comp (fs_map, ctor), - HOLogic.mk_comp (ctor', Term.list_comb (map, fs @ fs_maps)))); - val goals = map4 mk_goal fs_maps map_FTFT's ctors ctor's; - val maps = - map4 (fn goal => fn foldx => fn map_comp_id => fn map_cong0 => - Goal.prove_sorry lthy [] [] goal (K (mk_map_tac m n foldx map_comp_id map_cong0)) - |> Thm.close_derivation) - goals ctor_fold_thms map_comp_id_thms map_cong0s; - in - `(map (fn thm => thm RS @{thm comp_eq_dest})) maps - end; - - val (ctor_map_unique_thms, ctor_map_unique_thm) = - let - fun mk_prem u map ctor ctor' = - mk_Trueprop_eq (HOLogic.mk_comp (u, ctor), - HOLogic.mk_comp (ctor', Term.list_comb (map, fs @ us))); - val prems = map4 mk_prem us map_FTFT's ctors ctor's; - val goal = - HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj - (map2 (curry HOLogic.mk_eq) us fs_maps)); - val unique = Goal.prove_sorry lthy [] [] - (fold_rev Logic.all (us @ fs) (Logic.list_implies (prems, goal))) - (mk_ctor_map_unique_tac ctor_fold_unique_thm sym_map_comps) - |> Thm.close_derivation; - in - `split_conj_thm unique - end; - - val timer = time (timer "map functions for the new datatypes"); val ls = 1 upto m; val setsss = map (mk_setss o mk_set_Ts) passiveAs; - val map_setss = map (fn T => map2 (fn Ds => - mk_map_of_bnf Ds (passiveAs @ Ts) (mk_set_Ts T)) Dss bnfs) passiveAs; fun mk_col l T z z' sets = let @@ -1515,198 +1460,9 @@ val setss_by_range = map (fn cols => map (mk_fold Ts cols) ks) colss; val setss_by_bnf = transpose setss_by_range; - val ctor_set_thmss = - let - fun mk_goal sets ctor set col map = - mk_Trueprop_eq (HOLogic.mk_comp (set, ctor), - HOLogic.mk_comp (col, Term.list_comb (map, passive_ids @ sets))); - val goalss = - map3 (fn sets => map4 (mk_goal sets) ctors sets) setss_by_range colss map_setss; - val setss = map (map2 (fn foldx => fn goal => - Goal.prove_sorry lthy [] [] goal (K (mk_set_tac foldx)) |> Thm.close_derivation) - ctor_fold_thms) goalss; - - fun mk_simp_goal pas_set act_sets sets ctor z set = - Logic.all z (mk_Trueprop_eq (set $ (ctor $ z), - mk_union (pas_set $ z, - Library.foldl1 mk_union (map2 (fn X => mk_UNION (X $ z)) act_sets sets)))); - val simp_goalss = - map2 (fn i => fn sets => - map4 (fn Fsets => mk_simp_goal (nth Fsets (i - 1)) (drop m Fsets) sets) - FTs_setss ctors xFs sets) - ls setss_by_range; - - val ctor_setss = map3 (fn i => map3 (fn set_nats => fn goal => fn set => - Goal.prove_sorry lthy [] [] goal - (K (mk_ctor_set_tac set (nth set_nats (i - 1)) (drop m set_nats))) - |> Thm.close_derivation) - set_mapss) ls simp_goalss setss; - in - ctor_setss - end; - - fun mk_set_thms ctor_set = (@{thm xt1(3)} OF [ctor_set, @{thm Un_upper1}]) :: - map (fn i => (@{thm xt1(3)} OF [ctor_set, @{thm Un_upper2}]) RS - (mk_Un_upper n i RS subset_trans) RSN - (2, @{thm UN_upper} RS subset_trans)) - (1 upto n); - val Fset_set_thmsss = transpose (map (map mk_set_thms) ctor_set_thmss); - - val timer = time (timer "set functions for the new datatypes"); - - val cxs = map (SOME o certify lthy) Izs; - val setss_by_bnf' = - map (map (Term.subst_atomic_types (passiveAs ~~ passiveBs))) setss_by_bnf; - val setss_by_range' = transpose setss_by_bnf'; - - val set_map0_thmss = - let - fun mk_set_map0 f map z set set' = - HOLogic.mk_eq (mk_image f $ (set $ z), set' $ (map $ z)); - - fun mk_cphi f map z set set' = certify lthy - (Term.absfree (dest_Free z) (mk_set_map0 f map z set set')); - - val csetss = map (map (certify lthy)) setss_by_range'; - - val cphiss = map3 (fn f => fn sets => fn sets' => - (map4 (mk_cphi f) fs_maps Izs sets sets')) fs setss_by_range setss_by_range'; - - val inducts = map (fn cphis => - Drule.instantiate' cTs (map SOME cphis @ cxs) ctor_induct_thm) cphiss; - - val goals = - map3 (fn f => fn sets => fn sets' => - HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj - (map4 (mk_set_map0 f) fs_maps Izs sets sets'))) - fs setss_by_range setss_by_range'; - - fun mk_tac induct = mk_set_nat_tac m (rtac induct) set_mapss ctor_map_thms; - val thms = - map5 (fn goal => fn csets => fn ctor_sets => fn induct => fn i => - singleton (Proof_Context.export names_lthy lthy) - (Goal.prove_sorry lthy [] [] goal (mk_tac induct csets ctor_sets i)) - |> Thm.close_derivation) - goals csetss ctor_set_thmss inducts ls; - in - map split_conj_thm thms - end; - - val set_bd_thmss = - let - fun mk_set_bd z set = mk_ordLeq (mk_card_of (set $ z)) sum_bd; - - fun mk_cphi z set = certify lthy (Term.absfree (dest_Free z) (mk_set_bd z set)); - - val cphiss = map (map2 mk_cphi Izs) setss_by_range; - - val inducts = map (fn cphis => - Drule.instantiate' cTs (map SOME cphis @ cxs) ctor_induct_thm) cphiss; - - val goals = - map (fn sets => - HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj - (map2 mk_set_bd Izs sets))) setss_by_range; - - fun mk_tac induct = mk_set_bd_tac m (rtac induct) sum_Cinfinite set_bd_sumss; - val thms = - map4 (fn goal => fn ctor_sets => fn induct => fn i => - singleton (Proof_Context.export names_lthy lthy) - (Goal.prove_sorry lthy [] [] goal (mk_tac induct ctor_sets i)) - |> Thm.close_derivation) - goals ctor_set_thmss inducts ls; - in - map split_conj_thm thms - end; - - val map_cong0_thms = - let - fun mk_prem z set f g y y' = - mk_Ball (set $ z) (Term.absfree y' (HOLogic.mk_eq (f $ y, g $ y))); - - fun mk_map_cong0 sets z fmap gmap = - HOLogic.mk_imp - (Library.foldr1 HOLogic.mk_conj (map5 (mk_prem z) sets fs fs_copy ys ys'), - HOLogic.mk_eq (fmap $ z, gmap $ z)); - - fun mk_cphi sets z fmap gmap = - certify lthy (Term.absfree (dest_Free z) (mk_map_cong0 sets z fmap gmap)); - - val cphis = map4 mk_cphi setss_by_bnf Izs fs_maps fs_copy_maps; - - val induct = Drule.instantiate' cTs (map SOME cphis @ cxs) ctor_induct_thm; - - val goal = - HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj - (map4 mk_map_cong0 setss_by_bnf Izs fs_maps fs_copy_maps)); - - val thm = singleton (Proof_Context.export names_lthy lthy) - (Goal.prove_sorry lthy [] [] goal - (mk_mcong_tac (rtac induct) Fset_set_thmsss map_cong0s ctor_map_thms)) - |> Thm.close_derivation; - in - split_conj_thm thm - end; - - val Xsetss = map (map (Term.subst_atomic_types (passiveAs ~~ passiveXs))) setss_by_bnf; - - val map_wpull_thms = - let - val cTs = map (SOME o certifyT lthy o TFree) induct2_params; - val cxs = map (SOME o certify lthy) (splice Izs1 Izs2); - - fun mk_prem z1 z2 sets1 sets2 map1 map2 = - HOLogic.mk_conj - (HOLogic.mk_mem (z1, mk_in B1s sets1 (fastype_of z1)), - HOLogic.mk_conj - (HOLogic.mk_mem (z2, mk_in B2s sets2 (fastype_of z2)), - HOLogic.mk_eq (map1 $ z1, map2 $ z2))); - - val prems = map6 mk_prem Izs1 Izs2 setss_by_bnf setss_by_bnf' f1s_maps f2s_maps; - - fun mk_concl z1 z2 sets map1 map2 T x x' = - mk_Bex (mk_in AXs sets T) (Term.absfree x' - (HOLogic.mk_conj (HOLogic.mk_eq (map1 $ x, z1), HOLogic.mk_eq (map2 $ x, z2)))); - - val concls = map8 mk_concl Izs1 Izs2 Xsetss p1s_maps p2s_maps XTs xs xs'; - - val goals = map2 (curry HOLogic.mk_imp) prems concls; - - fun mk_cphi z1 z2 goal = certify lthy (Term.absfree z1 (Term.absfree z2 goal)); - - val cphis = map3 mk_cphi Izs1' Izs2' goals; - - val induct = Drule.instantiate' cTs (map SOME cphis @ cxs) ctor_induct2_thm; - - val goal = Logic.list_implies (map HOLogic.mk_Trueprop - (map8 mk_wpull AXs B1s B2s f1s f2s (replicate m NONE) p1s p2s), - HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj goals)); - - val thm = singleton (Proof_Context.export names_lthy lthy) - (Goal.prove_sorry lthy [] [] goal - (K (mk_lfp_map_wpull_tac lthy m (rtac induct) map_wpulls ctor_map_thms - (transpose ctor_set_thmss) Fset_set_thmsss ctor_inject_thms))) - |> Thm.close_derivation; - in - split_conj_thm thm - end; - - val timer = time (timer "helpers for BNF properties"); - - val map_id0_tacs = map (K o mk_map_id0_tac map_id0s) ctor_map_unique_thms; - val map_comp0_tacs = - map2 (K oo mk_map_comp0_tac map_comps ctor_map_thms) ctor_map_unique_thms ks; - val map_cong0_tacs = map (mk_map_cong0_tac m) map_cong0_thms; - val set_nat_tacss = map (map (K o mk_set_map0_tac)) (transpose set_map0_thmss); - val bd_co_tacs = replicate n (K (mk_bd_card_order_tac bd_card_orders)); - val bd_cinf_tacs = replicate n (K (rtac (sum_Cinfinite RS conjunct1) 1)); - val set_bd_tacss = map (map (fn thm => K (rtac thm 1))) (transpose set_bd_thmss); - val map_wpull_tacs = map (K o mk_wpull_tac) map_wpull_thms; - - val rel_OO_Grp_tacs = replicate n (K (rtac refl 1)); - - val tacss = map9 zip_axioms map_id0_tacs map_comp0_tacs map_cong0_tacs set_nat_tacss - bd_co_tacs bd_cinf_tacs set_bd_tacss map_wpull_tacs rel_OO_Grp_tacs; + val set_bss = + map (flat o map2 (fn B => fn b => + if member (op =) resDs (TFree B) then [] else [b]) resBs) set_bss0; val ctor_witss = let @@ -1733,45 +1489,227 @@ ctors (0 upto n - 1) witss end; - fun wit_tac {context = ctxt, prems = _} = - mk_wit_tac ctxt n (flat ctor_set_thmss) (maps wit_thms_of_bnf bnfs); - - val set_bss = - map (flat o map2 (fn B => fn b => - if member (op =) resDs (TFree B) then [] else [b]) resBs) set_bss0; - - val (Ibnfs, lthy) = - fold_map9 (fn tacs => fn b => fn map_b => fn rel_b => fn set_bs => fn mapx => fn sets => - fn T => fn wits => fn lthy => - bnf_def Dont_Inline (user_policy Note_Some) I tacs wit_tac (SOME deads) + val (Ibnf_consts, lthy) = + fold_map8 (fn b => fn map_b => fn rel_b => fn set_bs => fn mapx => fn sets => fn wits => + fn T => fn lthy => + define_bnf_consts Dont_Inline (user_policy Note_Some lthy) (SOME deads) map_b rel_b set_bs - ((((((b, T), fold_rev Term.absfree fs' mapx), sets), sum_bd), wits), NONE) - lthy - |> register_bnf (Local_Theory.full_name lthy b)) - tacss bs map_bs rel_bs set_bss fs_maps setss_by_bnf Ts ctor_witss lthy; + ((((((b, T), fold_rev Term.absfree fs' mapx), sets), sum_bd), wits), NONE) lthy) + bs map_bs rel_bs set_bss fs_maps setss_by_bnf ctor_witss Ts lthy; + + val (_, Iconsts, Iconst_defs, mk_Iconsts) = split_list4 Ibnf_consts; + val (_, Isetss, Ibds_Ds, Iwitss_Ds, _) = split_list5 Iconsts; + val (Imap_defs, Iset_defss, Ibd_defs, Iwit_defss, Irel_defs) = split_list5 Iconst_defs; + val (mk_Imaps_Ds, mk_It_Ds, _, mk_Irels_Ds, _) = split_list5 mk_Iconsts; + + val Irel_unabs_defs = map (fn def => mk_unabs_def m (def RS meta_eq_to_obj_eq)) Irel_defs; + val Iset_defs = flat Iset_defss; + + fun mk_Imaps As Bs = map (fn mk => mk deads As Bs) mk_Imaps_Ds; + fun mk_Isetss As = map2 (fn mk => fn Isets => map (mk deads As) Isets) mk_It_Ds Isetss; + val Ibds = map2 (fn mk => mk deads passiveAs) mk_It_Ds Ibds_Ds; + val Iwitss = + map2 (fn mk => fn Iwits => map (mk deads passiveAs o snd) Iwits) mk_It_Ds Iwitss_Ds; + fun mk_Irels As Bs = map (fn mk => mk deads As Bs) mk_Irels_Ds; + + val Imaps = mk_Imaps passiveAs passiveBs; + val fs_Imaps = map (fn m => Term.list_comb (m, fs)) Imaps; + val fs_copy_Imaps = map (fn m => Term.list_comb (m, fs_copy)) Imaps; + val (Isetss_by_range, Isetss_by_bnf) = `transpose (mk_Isetss passiveAs); + + val map_setss = map (fn T => map2 (fn Ds => + mk_map_of_bnf Ds (passiveAs @ Ts) (mk_set_Ts T)) Dss bnfs) passiveAs; + + val timer = time (timer "bnf constants for the new datatypes"); + + val (ctor_Imap_thms, ctor_Imap_o_thms) = + let + fun mk_goal fs_map map ctor ctor' = fold_rev Logic.all fs + (mk_Trueprop_eq (HOLogic.mk_comp (fs_map, ctor), + HOLogic.mk_comp (ctor', Term.list_comb (map, fs @ fs_Imaps)))); + val goals = map4 mk_goal fs_Imaps map_FTFT's ctors ctor's; + val maps = + map4 (fn goal => fn foldx => fn map_comp_id => fn map_cong0 => + Goal.prove_sorry lthy [] [] goal + (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Imap_defs THEN + mk_map_tac m n foldx map_comp_id map_cong0) + |> Thm.close_derivation) + goals ctor_fold_thms map_comp_id_thms map_cong0s; + in + `(map (fn thm => thm RS @{thm comp_eq_dest})) maps + end; - val fold_maps = fold_thms lthy (map (fn bnf => - mk_unabs_def m (map_def_of_bnf bnf RS meta_eq_to_obj_eq)) Ibnfs); + val (ctor_Imap_unique_thms, ctor_Imap_unique_thm) = + let + fun mk_prem u map ctor ctor' = + mk_Trueprop_eq (HOLogic.mk_comp (u, ctor), + HOLogic.mk_comp (ctor', Term.list_comb (map, fs @ us))); + val prems = map4 mk_prem us map_FTFT's ctors ctor's; + val goal = + HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj + (map2 (curry HOLogic.mk_eq) us fs_Imaps)); + val unique = Goal.prove_sorry lthy [] [] + (fold_rev Logic.all (us @ fs) (Logic.list_implies (prems, goal))) + (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Imap_defs THEN + mk_ctor_map_unique_tac ctor_fold_unique_thm sym_map_comps ctxt) + |> Thm.close_derivation; + in + `split_conj_thm unique + end; + + val timer = time (timer "map functions for the new datatypes"); + + val ctor_Iset_thmss = + let + fun mk_goal sets ctor set col map = + mk_Trueprop_eq (HOLogic.mk_comp (set, ctor), + HOLogic.mk_comp (col, Term.list_comb (map, passive_ids @ sets))); + val goalss = + map3 (fn sets => map4 (mk_goal sets) ctors sets) Isetss_by_range colss map_setss; + val setss = map (map2 (fn foldx => fn goal => + Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} => + unfold_thms_tac ctxt Iset_defs THEN mk_set_tac foldx) + |> Thm.close_derivation) + ctor_fold_thms) goalss; + + fun mk_simp_goal pas_set act_sets sets ctor z set = + Logic.all z (mk_Trueprop_eq (set $ (ctor $ z), + mk_union (pas_set $ z, + Library.foldl1 mk_union (map2 (fn X => mk_UNION (X $ z)) act_sets sets)))); + val simp_goalss = + map2 (fn i => fn sets => + map4 (fn Fsets => mk_simp_goal (nth Fsets (i - 1)) (drop m Fsets) sets) + FTs_setss ctors xFs sets) + ls Isetss_by_range; + + val ctor_setss = map3 (fn i => map3 (fn set_nats => fn goal => fn set => + Goal.prove_sorry lthy [] [] goal + (K (mk_ctor_set_tac set (nth set_nats (i - 1)) (drop m set_nats))) + |> Thm.close_derivation) + set_mapss) ls simp_goalss setss; + in + ctor_setss + end; - val fold_sets = fold_thms lthy (maps (fn bnf => - map (fn thm => thm RS meta_eq_to_obj_eq) (set_defs_of_bnf bnf)) Ibnfs); + fun mk_set_thms ctor_set = (@{thm xt1(3)} OF [ctor_set, @{thm Un_upper1}]) :: + map (fn i => (@{thm xt1(3)} OF [ctor_set, @{thm Un_upper2}]) RS + (mk_Un_upper n i RS subset_trans) RSN + (2, @{thm UN_upper} RS subset_trans)) + (1 upto n); + val set_Iset_thmsss = transpose (map (map mk_set_thms) ctor_Iset_thmss); + + val timer = time (timer "set functions for the new datatypes"); + + val cxs = map (SOME o certify lthy) Izs; + val Isetss_by_range' = + map (map (Term.subst_atomic_types (passiveAs ~~ passiveBs))) Isetss_by_range; + + val Iset_Imap0_thmss = + let + fun mk_set_map0 f map z set set' = + HOLogic.mk_eq (mk_image f $ (set $ z), set' $ (map $ z)); + + fun mk_cphi f map z set set' = certify lthy + (Term.absfree (dest_Free z) (mk_set_map0 f map z set set')); + + val csetss = map (map (certify lthy)) Isetss_by_range'; + + val cphiss = map3 (fn f => fn sets => fn sets' => + (map4 (mk_cphi f) fs_Imaps Izs sets sets')) fs Isetss_by_range Isetss_by_range'; - val timer = time (timer "registered new datatypes as BNFs"); + val inducts = map (fn cphis => + Drule.instantiate' cTs (map SOME cphis @ cxs) ctor_induct_thm) cphiss; + + val goals = + map3 (fn f => fn sets => fn sets' => + HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj + (map4 (mk_set_map0 f) fs_Imaps Izs sets sets'))) + fs Isetss_by_range Isetss_by_range'; + + fun mk_tac induct = mk_set_nat_tac m (rtac induct) set_mapss ctor_Imap_thms; + val thms = + map5 (fn goal => fn csets => fn ctor_sets => fn induct => fn i => + singleton (Proof_Context.export names_lthy lthy) + (Goal.prove_sorry lthy [] [] goal (mk_tac induct csets ctor_sets i)) + |> Thm.close_derivation) + goals csetss ctor_Iset_thmss inducts ls; + in + map split_conj_thm thms + end; + + val Iset_bd_thmss = + let + fun mk_set_bd z bd set = mk_ordLeq (mk_card_of (set $ z)) bd; + + fun mk_cphi z set = certify lthy (Term.absfree (dest_Free z) (mk_set_bd z sum_bd set)); - val Irels = map (mk_rel_of_bnf deads passiveAs passiveBs) Ibnfs; + val cphiss = map (map2 mk_cphi Izs) Isetss_by_range; + + val inducts = map (fn cphis => + Drule.instantiate' cTs (map SOME cphis @ cxs) ctor_induct_thm) cphiss; + + val goals = + map (fn sets => + HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj + (map3 mk_set_bd Izs Ibds sets))) Isetss_by_range; + + fun mk_tac induct = mk_set_bd_tac m (rtac induct) sum_Cinfinite set_bd_sumss; + val thms = + map4 (fn goal => fn ctor_sets => fn induct => fn i => + singleton (Proof_Context.export names_lthy lthy) + (Goal.prove_sorry lthy [] [] goal + (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Ibd_defs THEN + mk_tac induct ctor_sets i ctxt)) + |> Thm.close_derivation) + goals ctor_Iset_thmss inducts ls; + in + map split_conj_thm thms + end; - val Irelphis = map (fn Irel => Term.list_comb (Irel, Iphis)) Irels; - val relphis = map (fn rel => Term.list_comb (rel, Iphis @ Irelphis)) rels; + val Imap_cong0_thms = + let + fun mk_prem z set f g y y' = + mk_Ball (set $ z) (Term.absfree y' (HOLogic.mk_eq (f $ y, g $ y))); + + fun mk_map_cong0 sets z fmap gmap = + HOLogic.mk_imp + (Library.foldr1 HOLogic.mk_conj (map5 (mk_prem z) sets fs fs_copy ys ys'), + HOLogic.mk_eq (fmap $ z, gmap $ z)); + + fun mk_cphi sets z fmap gmap = + certify lthy (Term.absfree (dest_Free z) (mk_map_cong0 sets z fmap gmap)); + + val cphis = map4 mk_cphi Isetss_by_bnf Izs fs_Imaps fs_copy_Imaps; + + val induct = Drule.instantiate' cTs (map SOME cphis @ cxs) ctor_induct_thm; + + val goal = + HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj + (map4 mk_map_cong0 Isetss_by_bnf Izs fs_Imaps fs_copy_Imaps)); + + val thm = singleton (Proof_Context.export names_lthy lthy) + (Goal.prove_sorry lthy [] [] goal + (mk_mcong_tac (rtac induct) set_Iset_thmsss map_cong0s ctor_Imap_thms)) + |> Thm.close_derivation; + in + split_conj_thm thm + end; val in_rels = map in_rel_of_bnf bnfs; - val in_Irels = map in_rel_of_bnf Ibnfs; + val in_Irels = map (fn def => trans OF [def, @{thm OO_Grp_alt}] RS @{thm predicate2_eqD}) + Irel_unabs_defs; + + val ctor_Iset_incl_thmss = map (map hd) set_Iset_thmsss; + val ctor_set_Iset_incl_thmsss = map (transpose o map tl) set_Iset_thmsss; + val ctor_Iset_thmss' = transpose ctor_Iset_thmss; - val ctor_set_incl_thmss = map (map (fold_sets o hd)) Fset_set_thmsss; - val ctor_set_set_incl_thmsss = map (transpose o map (map fold_sets o tl)) Fset_set_thmsss; - val folded_ctor_map_thms = map fold_maps ctor_map_thms; - val folded_ctor_map_o_thms = map fold_maps ctor_map_o_thms; - val folded_ctor_set_thmss = map (map fold_sets) ctor_set_thmss; - val folded_ctor_set_thmss' = transpose folded_ctor_set_thmss; + val Irels = mk_Irels passiveAs passiveBs; + val Irelphis = map (fn rel => Term.list_comb (rel, Iphis)) Irels; + val relphis = map (fn rel => Term.list_comb (rel, Iphis @ Irelphis)) rels; + val Irelpsi1s = map (fn rel => Term.list_comb (rel, Ipsi1s)) (mk_Irels passiveAs passiveCs); + val Irelpsi2s = map (fn rel => Term.list_comb (rel, Ipsi2s)) (mk_Irels passiveCs passiveBs); + val Irelpsi12s = map (fn rel => + Term.list_comb (rel, map2 (curry mk_rel_compp) Ipsi1s Ipsi2s)) Irels; val ctor_Irel_thms = let @@ -1786,46 +1724,99 @@ (K (mk_ctor_rel_tac lthy in_Irels i in_rel map_comp0 map_cong0 ctor_map ctor_sets ctor_inject ctor_dtor set_map0s ctor_set_incls ctor_set_set_inclss)) |> Thm.close_derivation) - ks goals in_rels map_comps map_cong0s folded_ctor_map_thms folded_ctor_set_thmss' - ctor_inject_thms ctor_dtor_thms set_mapss ctor_set_incl_thmss - ctor_set_set_incl_thmsss + ks goals in_rels map_comps map_cong0s ctor_Imap_thms ctor_Iset_thmss' + ctor_inject_thms ctor_dtor_thms set_mapss ctor_Iset_incl_thmss + ctor_set_Iset_incl_thmsss + end; + + val le_Irel_OO_thm = + let + fun mk_le_Irel_OO Irelpsi1 Irelpsi2 Irelpsi12 Iz1 Iz2 = + HOLogic.mk_imp (mk_rel_compp (Irelpsi1, Irelpsi2) $ Iz1 $ Iz2, + Irelpsi12 $ Iz1 $ Iz2); + val goals = map5 mk_le_Irel_OO Irelpsi1s Irelpsi2s Irelpsi12s Izs1 Izs2; + + val cTs = map (SOME o certifyT lthy o TFree) induct2_params; + val cxs = map (SOME o certify lthy) (splice Izs1 Izs2); + fun mk_cphi z1 z2 goal = SOME (certify lthy (Term.absfree z1 (Term.absfree z2 goal))); + val cphis = map3 mk_cphi Izs1' Izs2' goals; + val induct = Drule.instantiate' cTs (cphis @ cxs) ctor_induct2_thm; + + val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj goals); + in + singleton (Proof_Context.export names_lthy lthy) + (Goal.prove_sorry lthy [] [] goal + (mk_le_rel_OO_tac m induct ctor_nchotomy_thms ctor_Irel_thms rel_mono_strongs + rel_OOs)) + |> Thm.close_derivation end; - val timer = time (timer "additional properties"); + val timer = time (timer "helpers for BNF properties"); + + val map_id0_tacs = map (K o mk_map_id0_tac map_id0s) ctor_Imap_unique_thms; + val map_comp0_tacs = + map2 (K oo mk_map_comp0_tac map_comps ctor_Imap_thms) ctor_Imap_unique_thms ks; + val map_cong0_tacs = map (mk_map_cong0_tac m) Imap_cong0_thms; + val set_map0_tacss = map (map (K o mk_set_map0_tac)) (transpose Iset_Imap0_thmss); + val bd_co_tacs = replicate n (fn {context = ctxt, prems = _} => + unfold_thms_tac ctxt Ibd_defs THEN mk_bd_card_order_tac bd_card_orders); + val bd_cinf_tacs = replicate n (fn {context = ctxt, prems = _} => + unfold_thms_tac ctxt Ibd_defs THEN rtac (sum_Cinfinite RS conjunct1) 1); + val set_bd_tacss = map (map (fn thm => K (rtac thm 1))) (transpose Iset_bd_thmss); + val le_rel_OO_tacs = map (fn i => + K ((rtac @{thm predicate2I} THEN' etac (le_Irel_OO_thm RS mk_conjunctN n i RS mp)) 1)) ks; + + val rel_OO_Grp_tacs = map (fn def => K (rtac def 1)) Irel_unabs_defs; + + val tacss = map9 zip_axioms map_id0_tacs map_comp0_tacs map_cong0_tacs set_map0_tacss + bd_co_tacs bd_cinf_tacs set_bd_tacss le_rel_OO_tacs rel_OO_Grp_tacs; + + fun wit_tac {context = ctxt, prems = _} = unfold_thms_tac ctxt (flat Iwit_defss) THEN + mk_wit_tac ctxt n (flat ctor_Iset_thmss) (maps wit_thms_of_bnf bnfs); + + val (Ibnfs, lthy) = + fold_map5 (fn tacs => fn map_b => fn rel_b => fn set_bs => fn consts => fn lthy => + bnf_def Do_Inline (user_policy Note_Some) I tacs wit_tac (SOME deads) + map_b rel_b set_bs consts lthy + |> register_bnf (Local_Theory.full_name lthy b)) + tacss map_bs rel_bs set_bss + ((((((bs ~~ Ts) ~~ Imaps) ~~ Isetss_by_bnf) ~~ Ibds) ~~ Iwitss) ~~ map SOME Irels) + lthy; + + val timer = time (timer "registered new datatypes as BNFs"); val ls' = if m = 1 then [0] else ls val Ibnf_common_notes = - [(ctor_map_uniqueN, [fold_maps ctor_map_unique_thm])] + [(ctor_map_uniqueN, [ctor_Imap_unique_thm])] |> map (fn (thmN, thms) => ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])); val Ibnf_notes = - [(ctor_mapN, map single folded_ctor_map_thms), + [(ctor_mapN, map single ctor_Imap_thms), (ctor_relN, map single ctor_Irel_thms), - (ctor_set_inclN, ctor_set_incl_thmss), - (ctor_set_set_inclN, map flat ctor_set_set_incl_thmsss)] @ - map2 (fn i => fn thms => (mk_ctor_setN i, map single thms)) ls' folded_ctor_set_thmss + (ctor_set_inclN, ctor_Iset_incl_thmss), + (ctor_set_set_inclN, map flat ctor_set_Iset_incl_thmsss)] @ + map2 (fn i => fn thms => (mk_ctor_setN i, map single thms)) ls' ctor_Iset_thmss |> maps (fn (thmN, thmss) => map2 (fn b => fn thms => ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])) bs thmss) in - (timer, Ibnfs, (folded_ctor_map_o_thms, folded_ctor_map_thms), folded_ctor_set_thmss', + (timer, Ibnfs, (ctor_Imap_o_thms, ctor_Imap_thms), ctor_Iset_thmss', ctor_Irel_thms, Ibnf_common_notes @ Ibnf_notes, lthy) end; - val ctor_fold_o_map_thms = mk_xtor_un_fold_o_map_thms Least_FP false m ctor_fold_unique_thm - folded_ctor_map_o_thms (map (mk_pointfree lthy) ctor_fold_thms) sym_map_comps map_cong0s; - val ctor_rec_o_map_thms = mk_xtor_un_fold_o_map_thms Least_FP true m ctor_rec_unique_thm - folded_ctor_map_o_thms (map (mk_pointfree lthy) ctor_rec_thms) sym_map_comps map_cong0s; + val ctor_fold_o_Imap_thms = mk_xtor_un_fold_o_map_thms Least_FP false m ctor_fold_unique_thm + ctor_Imap_o_thms (map (mk_pointfree lthy) ctor_fold_thms) sym_map_comps map_cong0s; + val ctor_rec_o_Imap_thms = mk_xtor_un_fold_o_map_thms Least_FP true m ctor_rec_unique_thm + ctor_Imap_o_thms (map (mk_pointfree lthy) ctor_rec_thms) sym_map_comps map_cong0s; val Irels = if m = 0 then map HOLogic.eq_const Ts else map (mk_rel_of_bnf deads passiveAs passiveBs) Ibnfs; val Irel_induct_thm = mk_rel_xtor_co_induct_thm Least_FP rels activeIphis Irels Iphis xFs yFs ctors ctor's - (mk_rel_induct_tac m ctor_induct2_thm ks ctor_Irel_thms (map rel_mono_strong_of_bnf bnfs)) - lthy; + (mk_rel_induct_tac m ctor_induct2_thm ks ctor_Irel_thms rel_mono_strongs) lthy; val rels = map2 (fn Ds => mk_rel_of_bnf Ds allAs allBs') Dss bnfs; val ctor_fold_transfer_thms = @@ -1850,8 +1841,8 @@ (ctor_foldN, ctor_fold_thms), (ctor_fold_uniqueN, ctor_fold_unique_thms), (ctor_rec_uniqueN, ctor_rec_unique_thms), - (ctor_fold_o_mapN, ctor_fold_o_map_thms), - (ctor_rec_o_mapN, ctor_rec_o_map_thms), + (ctor_fold_o_mapN, ctor_fold_o_Imap_thms), + (ctor_rec_o_mapN, ctor_rec_o_Imap_thms), (ctor_injectN, ctor_inject_thms), (ctor_recN, ctor_rec_thms), (dtor_ctorN, dtor_ctor_thms), @@ -1871,10 +1862,10 @@ ({Ts = Ts, bnfs = Ibnfs, ctors = ctors, dtors = dtors, xtor_co_iterss = transpose [folds, recs], xtor_co_induct = ctor_induct_thm, dtor_ctors = dtor_ctor_thms, ctor_dtors = ctor_dtor_thms, ctor_injects = ctor_inject_thms, dtor_injects = dtor_inject_thms, - xtor_map_thms = folded_ctor_map_thms, xtor_set_thmss = folded_ctor_set_thmss', + xtor_map_thms = ctor_Imap_thms, xtor_set_thmss = ctor_Iset_thmss', xtor_rel_thms = ctor_Irel_thms, xtor_co_iter_thmss = transpose [ctor_fold_thms, ctor_rec_thms], - xtor_co_iter_o_map_thmss = transpose [ctor_fold_o_map_thms, ctor_rec_o_map_thms], + xtor_co_iter_o_map_thmss = transpose [ctor_fold_o_Imap_thms, ctor_rec_o_Imap_thms], rel_xtor_co_induct_thm = Irel_induct_thm}, lthy |> Local_Theory.notes (maybe_conceal_notes (common_notes @ notes @ Ibnf_notes)) |> snd) end; diff -r fac0c76bbda2 -r af71b753c459 src/HOL/BNF/Tools/bnf_lfp_tactics.ML --- a/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Fri Dec 20 21:09:01 2013 +0100 +++ b/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Wed Dec 18 11:03:40 2013 +0100 @@ -37,12 +37,12 @@ val mk_fold_transfer_tac: int -> thm -> thm list -> thm list -> {prems: thm list, context: Proof.context} -> tactic val mk_least_min_alg_tac: thm -> thm -> tactic - val mk_lfp_map_wpull_tac: Proof.context -> int -> (int -> tactic) -> thm list -> thm list -> - thm list list -> thm list list list -> thm list -> tactic + val mk_le_rel_OO_tac: int -> thm -> thm list -> thm list -> thm list -> thm list -> + {prems: 'a, context: Proof.context} -> tactic val mk_map_comp0_tac: thm list -> thm list -> thm -> int -> tactic val mk_map_id0_tac: thm list -> thm -> tactic val mk_map_tac: int -> int -> thm -> thm -> thm -> tactic - val mk_ctor_map_unique_tac: thm -> thm list -> {prems: thm list, context: Proof.context} -> tactic + val mk_ctor_map_unique_tac: thm -> thm list -> Proof.context -> tactic val mk_mcong_tac: (int -> tactic) -> thm list list list -> thm list -> thm list -> {prems: 'a, context: Proof.context} -> tactic val mk_min_algs_card_of_tac: ctyp -> cterm -> int -> thm -> thm list -> thm list -> thm -> thm -> @@ -69,13 +69,12 @@ val mk_rec_unique_mor_tac: thm list -> thm list -> thm -> {prems: 'a, context: Proof.context} -> tactic val mk_set_bd_tac: int -> (int -> tactic) -> thm -> thm list list -> thm list -> int -> - {prems: 'a, context: Proof.context} -> tactic + Proof.context -> tactic val mk_set_nat_tac: int -> (int -> tactic) -> thm list list -> thm list -> cterm list -> thm list -> int -> {prems: 'a, context: Proof.context} -> tactic val mk_set_map0_tac: thm -> tactic val mk_set_tac: thm -> tactic val mk_wit_tac: Proof.context -> int -> thm list -> thm list -> tactic - val mk_wpull_tac: thm -> tactic end; structure BNF_LFP_Tactics : BNF_LFP_TACTICS = @@ -584,7 +583,7 @@ REPEAT_DETERM_N n o (EVERY' (map rtac [trans, o_apply, id_apply])), rtac sym, rtac o_apply] 1; -fun mk_ctor_map_unique_tac fold_unique sym_map_comps {context = ctxt, prems = _} = +fun mk_ctor_map_unique_tac fold_unique sym_map_comps ctxt = rtac fold_unique 1 THEN unfold_thms_tac ctxt (sym_map_comps @ @{thms o_assoc[symmetric] id_o o_id}) THEN ALLGOALS atac; @@ -624,7 +623,7 @@ (induct_tac THEN' EVERY' (map4 mk_set_nat csets ctor_maps ctor_sets set_mapss)) 1 end; -fun mk_set_bd_tac m induct_tac bd_Cinfinite set_bdss ctor_sets i {context = ctxt, prems = _} = +fun mk_set_bd_tac m induct_tac bd_Cinfinite set_bdss ctor_sets i ctxt = let val n = length ctor_sets; @@ -658,49 +657,18 @@ (induct_tac THEN' EVERY' (map3 mk_map_cong0 ctor_maps map_cong0s set_setsss)) 1 end; -fun mk_lfp_map_wpull_tac ctxt m induct_tac wpulls ctor_maps ctor_setss set_setsss ctor_injects = - let - val n = length wpulls; - val ks = 1 upto n; - val ls = 1 upto m; - - fun use_pass_asm thm = rtac conjI THEN' etac (thm RS subset_trans); - fun use_act_asm thm = etac (thm RS subset_trans) THEN' atac; - - fun useIH set_sets i = EVERY' [rtac ssubst, rtac @{thm wpull_def}, - REPEAT_DETERM_N m o etac thin_rl, select_prem_tac n (dtac asm_rl) i, - rtac allI, rtac allI, rtac impI, REPEAT_DETERM o etac conjE, - REPEAT_DETERM o dtac @{thm meta_spec}, - dtac meta_mp, atac, - dtac meta_mp, atac, etac mp, - rtac conjI, rtac CollectI, CONJ_WRAP' use_act_asm set_sets, - rtac conjI, rtac CollectI, CONJ_WRAP' use_act_asm set_sets, - atac]; - - fun mk_subset thm = EVERY' [rtac ord_eq_le_trans, rtac thm, rtac @{thm Un_least}, atac, - REPEAT_DETERM_N (n - 1) o rtac @{thm Un_least}, - REPEAT_DETERM_N n o - EVERY' [rtac @{thm UN_least}, rtac CollectE, etac set_rev_mp, atac, - REPEAT_DETERM o etac conjE, atac]]; - - fun mk_wpull wpull ctor_map ctor_sets set_setss ctor_inject = - EVERY' [rtac impI, REPEAT_DETERM o eresolve_tac [CollectE, conjE], - rtac rev_mp, rtac wpull, - EVERY' (map (fn i => REPEAT_DETERM_N (i - 1) o etac thin_rl THEN' atac) ls), - EVERY' (map2 useIH (transpose (map tl set_setss)) ks), - rtac impI, REPEAT_DETERM_N (m + n) o etac thin_rl, - dtac @{thm subst[OF wpull_def, of "%x. x"]}, etac allE, etac allE, etac impE, - rtac conjI, rtac CollectI, EVERY' (map (use_pass_asm o hd) set_setss), - CONJ_WRAP' (K (rtac subset_refl)) ks, - rtac conjI, rtac CollectI, EVERY' (map (use_pass_asm o hd) set_setss), - CONJ_WRAP' (K (rtac subset_refl)) ks, - rtac subst, rtac ctor_inject, rtac trans, rtac sym, rtac ctor_map, - rtac trans, atac, rtac ctor_map, REPEAT_DETERM o eresolve_tac [CollectE, conjE, bexE], - hyp_subst_tac ctxt, rtac bexI, rtac conjI, rtac ctor_map, rtac ctor_map, rtac CollectI, - CONJ_WRAP' mk_subset ctor_sets]; - in - (induct_tac THEN' EVERY' (map5 mk_wpull wpulls ctor_maps ctor_setss set_setsss ctor_injects)) 1 - end; +fun mk_le_rel_OO_tac m induct ctor_nchotomys ctor_Irels rel_mono_strongs rel_OOs + {context = ctxt, prems = _} = + EVERY' (rtac induct :: + map4 (fn nchotomy => fn Irel => fn rel_mono => fn rel_OO => + EVERY' [rtac impI, etac (nchotomy RS @{thm nchotomy_relcomppE}), + REPEAT_DETERM_N 2 o dtac (Irel RS iffD1), rtac (Irel RS iffD2), + rtac rel_mono, rtac (rel_OO RS @{thm predicate2_eqD} RS iffD2), + rtac @{thm relcomppI}, atac, atac, + REPEAT_DETERM_N m o EVERY' [rtac ballI, rtac ballI, rtac impI, atac], + REPEAT_DETERM_N (length rel_OOs) o + EVERY' [rtac ballI, rtac ballI, Goal.assume_rule_tac ctxt]]) + ctor_nchotomys ctor_Irels rel_mono_strongs rel_OOs) 1; (* BNF tactics *) @@ -730,10 +698,6 @@ fun mk_bd_card_order_tac bd_card_orders = CONJ_WRAP_GEN' (rtac @{thm card_order_csum}) rtac bd_card_orders 1; -fun mk_wpull_tac wpull = - EVERY' [rtac ssubst, rtac @{thm wpull_def}, rtac allI, rtac allI, - rtac wpull, REPEAT_DETERM o atac] 1; - fun mk_wit_tac ctxt n ctor_set wit = REPEAT_DETERM (atac 1 ORELSE EVERY' [dtac set_rev_mp, rtac equalityD1, resolve_tac ctor_set, diff -r fac0c76bbda2 -r af71b753c459 src/HOL/BNF/Tools/bnf_tactics.ML --- a/src/HOL/BNF/Tools/bnf_tactics.ML Fri Dec 20 21:09:01 2013 +0100 +++ b/src/HOL/BNF/Tools/bnf_tactics.ML Wed Dec 18 11:03:40 2013 +0100 @@ -11,7 +11,6 @@ include CTR_SUGAR_GENERAL_TACTICS val fo_rtac: thm -> Proof.context -> int -> tactic - val mk_unfold_thms_then_tac: Proof.context -> thm list -> ('a -> tactic) -> 'a -> tactic val mk_flatten_assoc_tac: (int -> tactic) -> thm -> thm -> thm -> tactic val mk_rotate_eq_tac: (int -> tactic) -> thm -> thm -> thm -> thm -> ''a list -> ''a list -> @@ -45,8 +44,6 @@ rtac (Drule.instantiate_normalize insts thm) 1 end); -fun mk_unfold_thms_then_tac ctxt defs tac x = unfold_thms_tac ctxt defs THEN tac x; - (*transforms f (g x) = h (k x) into f o g = h o k using first order matches for f, g, h, and k*) fun mk_pointfree ctxt thm = thm |> Thm.prop_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq diff -r fac0c76bbda2 -r af71b753c459 src/HOL/BNF/Tools/bnf_util.ML --- a/src/HOL/BNF/Tools/bnf_util.ML Fri Dec 20 21:09:01 2013 +0100 +++ b/src/HOL/BNF/Tools/bnf_util.ML Wed Dec 18 11:03:40 2013 +0100 @@ -45,6 +45,7 @@ 'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list -> 'i list -> 'j -> 'k list * 'j val split_list4: ('a * 'b * 'c * 'd) list -> 'a list * 'b list * 'c list * 'd list + val split_list5: ('a * 'b * 'c * 'd * 'e) list -> 'a list * 'b list * 'c list * 'd list * 'e list val find_indices: ('b * 'a -> bool) -> 'a list -> 'b list -> int list val mk_TFreess: int list -> Proof.context -> typ list list * Proof.context @@ -98,7 +99,6 @@ val mk_ordLeq: term -> term -> term val mk_rel_comp: term * term -> term val mk_rel_compp: term * term -> term - val mk_wpull: term -> term -> term -> term -> term -> (term * term) option -> term -> term -> term (*parameterized terms*) val mk_nthN: int -> term -> int -> term @@ -252,6 +252,11 @@ let val (xs1, xs2, xs3, xs4) = split_list4 xs; in (x1 :: xs1, x2 :: xs2, x3 :: xs3, x4 :: xs4) end; +fun split_list5 [] = ([], [], [], [], []) + | split_list5 ((x1, x2, x3, x4, x5) :: xs) = + let val (xs1, xs2, xs3, xs4, xs5) = split_list5 xs; + in (x1 :: xs1, x2 :: xs2, x3 :: xs3, x4 :: xs4, x5 :: xs5) end; + val parse_binding_colon = parse_binding --| @{keyword ":"}; val parse_opt_binding_colon = Scan.optional parse_binding_colon Binding.empty; @@ -460,39 +465,6 @@ else HOLogic.mk_UNIV T end; -fun mk_wpull A B1 B2 f1 f2 pseudo p1 p2 = - let - val AT = fastype_of A; - val BT1 = fastype_of B1; - val BT2 = fastype_of B2; - val FT1 = fastype_of f1; - val FT2 = fastype_of f2; - val PT1 = fastype_of p1; - val PT2 = fastype_of p2; - val T1 = HOLogic.dest_setT BT1; - val T2 = HOLogic.dest_setT BT2; - val domP = domain_type PT1; - val ranF = range_type FT1; - val _ = if is_some pseudo orelse - (HOLogic.dest_setT AT = domP andalso - domain_type FT1 = T1 andalso - domain_type FT2 = T2 andalso - domain_type PT2 = domP andalso - range_type PT1 = T1 andalso - range_type PT2 = T2 andalso - range_type FT2 = ranF) - then () else raise TYPE ("mk_wpull", [BT1, BT2, FT1, FT2, PT1, PT2], []); - in - (case pseudo of - NONE => Const (@{const_name wpull}, - AT --> BT1 --> BT2 --> FT1 --> FT2 --> PT1 --> PT2 --> HOLogic.boolT) $ - A $ B1 $ B2 $ f1 $ f2 $ p1 $ p2 - | SOME (e1, e2) => Const (@{const_name wppull}, - AT --> BT1 --> BT2 --> FT1 --> FT2 --> fastype_of e1 --> fastype_of e2 --> - PT1 --> PT2 --> HOLogic.boolT) $ - A $ B1 $ B2 $ f1 $ f2 $ e1 $ e2 $ p1 $ p2) - end; - fun mk_leq t1 t2 = Const (@{const_name less_eq}, (fastype_of t1) --> (fastype_of t2) --> HOLogic.boolT) $ t1 $ t2;