# HG changeset patch # User traytel # Date 1656338058 -7200 # Node ID 22d1c5f2b9f4ae08d2b66f9062adbee5b8e83eef # Parent 7a6301d0119906f7d25e2b59f86e6d1e4b9b8748 strict bounds for BNFs (by Jan van Brügge) diff -r 7a6301d01199 -r 22d1c5f2b9f4 src/Doc/Datatypes/Datatypes.thy --- a/src/Doc/Datatypes/Datatypes.thy Sat Jun 25 09:50:40 2022 +0000 +++ b/src/Doc/Datatypes/Datatypes.thy Mon Jun 27 15:54:18 2022 +0200 @@ -2855,7 +2855,7 @@ bnf "('d, 'a) fn" map: map_fn sets: set_fn - bd: "natLeq +c |UNIV :: 'd set|" + bd: "card_suc (natLeq +c |UNIV :: 'd set| )" rel: rel_fn pred: pred_fn proof - @@ -2875,22 +2875,24 @@ show "set_fn \ map_fn f = (`) f \ set_fn" by transfer (auto simp add: comp_def) next - show "card_order (natLeq +c |UNIV :: 'd set| )" - apply (rule card_order_csum) - apply (rule natLeq_card_order) - by (rule card_of_card_order_on) + show "card_order (card_suc (natLeq +c |UNIV :: 'd set| ))" + by (rule card_order_card_suc_natLeq_UNIV) next - show "cinfinite (natLeq +c |UNIV :: 'd set| )" - apply (rule cinfinite_csum) - apply (rule disjI1) - by (rule natLeq_cinfinite) + show "cinfinite (card_suc (natLeq +c |UNIV :: 'd set| ))" + by (rule cinfinite_card_suc_natLeq_UNIV) + next + show "regularCard (card_suc (natLeq +c |UNIV :: 'd set| ))" + by (rule regularCard_card_suc_natLeq_UNIV) next fix F :: "('d, 'a) fn" have "|set_fn F| \o |UNIV :: 'd set|" (is "_ \o ?U") by transfer (rule card_of_image) also have "?U \o natLeq +c ?U" by (rule ordLeq_csum2) (rule card_of_Card_order) - finally show "|set_fn F| \o natLeq +c |UNIV :: 'd set|" . + finally have "|set_fn F| \o natLeq +c |UNIV :: 'd set|" . + then show "|set_fn F| 'b \ bool" and S :: "'b \ 'c \ bool" show "rel_fn R OO rel_fn S \ rel_fn (R OO S)" diff -r 7a6301d01199 -r 22d1c5f2b9f4 src/HOL/BNF_Cardinal_Arithmetic.thy --- a/src/HOL/BNF_Cardinal_Arithmetic.thy Sat Jun 25 09:50:40 2022 +0000 +++ b/src/HOL/BNF_Cardinal_Arithmetic.thy Mon Jun 27 15:54:18 2022 +0200 @@ -103,6 +103,9 @@ lemma natLeq_cinfinite: "cinfinite natLeq" unfolding cinfinite_def Field_natLeq by (rule infinite_UNIV_nat) +lemma natLeq_Cinfinite: "Cinfinite natLeq" + using natLeq_cinfinite natLeq_Card_order by simp + lemma natLeq_ordLeq_cinfinite: assumes inf: "Cinfinite r" shows "natLeq \o r" @@ -126,6 +129,21 @@ lemma cinfinite_mono: "\r1 \o r2; cinfinite r1\ \ cinfinite r2" unfolding cinfinite_def by (auto dest: card_of_ordLeq_infinite[OF card_of_mono2]) +lemma regularCard_ordIso: +assumes "k =o k'" and "Cinfinite k" and "regularCard k" +shows "regularCard k'" +proof- + have "stable k" using assms cinfinite_def regularCard_stable by blast + hence "stable k'" using assms stable_ordIso1 ordIso_symmetric by blast + thus ?thesis using assms cinfinite_def stable_regularCard + using Cinfinite_cong by blast +qed + +corollary card_of_UNION_ordLess_infinite_Field_regularCard: +assumes ST: "regularCard r" and INF: "Cinfinite r" and + LEQ_I: "|I| i \ I. |A i| i \ I. A i| Binary sum\ @@ -222,7 +240,6 @@ lemma Un_csum: "|A \ B| \o |A| +c |B|" using ordLeq_ordIso_trans[OF card_of_Un_Plus_ordLeq Plus_csum] by blast - subsection \One\ definition cone where @@ -359,6 +376,76 @@ lemma csum_absorb1: "\Cinfinite r2; r1 \o r2\ \ r2 +c r1 =o r2" by (rule csum_absorb1') auto +lemma csum_absorb2: "\Cinfinite r2 ; r1 \o r2\ \ r1 +c r2 =o r2" + using ordIso_transitive csum_com csum_absorb1 by blast + +lemma regularCard_csum: + assumes "Cinfinite r" "Cinfinite s" "regularCard r" "regularCard s" + shows "regularCard (r +c s)" +proof (cases "r \o s") + case True + then show ?thesis using regularCard_ordIso[of s] csum_absorb2'[THEN ordIso_symmetric] assms by auto +next + case False + have "Well_order s" "Well_order r" using assms card_order_on_well_order_on by auto + then have "s \o r" using not_ordLeq_iff_ordLess False ordLess_imp_ordLeq by auto + then show ?thesis using regularCard_ordIso[of r] csum_absorb1'[THEN ordIso_symmetric] assms by auto +qed + +lemma csum_mono_strict: + assumes Card_order: "Card_order r" "Card_order q" + and Cinfinite: "Cinfinite r'" "Cinfinite q'" + and less: "r o q") + case True + then have "r +c q =o q" using csum_absorb2 inner by blast + then show ?thesis + using ordIso_ordLess_trans ordLess_ordLeq_trans less Cinfinite ordLeq_csum2 by blast + next + case False + then have "q \o r" using not_ordLeq_iff_ordLess Well_order ordLess_imp_ordLeq by blast + then have "r +c q =o r" using csum_absorb1 outer by blast + then show ?thesis + using ordIso_ordLess_trans ordLess_ordLeq_trans less Cinfinite ordLeq_csum1 by blast + qed + next + case False + then have "Cfinite q" using Card_order cinfinite_def cfinite_def by blast + then have "q \o r" using finite_ordLess_infinite cfinite_def cinfinite_def outer + Well_order ordLess_imp_ordLeq by blast + then have "r +c q =o r" by (rule csum_absorb1[OF outer]) + then show ?thesis using ordIso_ordLess_trans ordLess_ordLeq_trans less ordLeq_csum1 Cinfinite by blast + qed + next + case False + then have outer: "Cfinite r" using Card_order cinfinite_def cfinite_def by blast + then show ?thesis + proof (cases "Cinfinite q") + case True + then have "r \o q" using finite_ordLess_infinite cinfinite_def cfinite_def outer Well_order + ordLess_imp_ordLeq by blast + then have "r +c q =o q" by (rule csum_absorb2[OF True]) + then show ?thesis using ordIso_ordLess_trans ordLess_ordLeq_trans less ordLeq_csum2 Cinfinite by blast + next + case False + then have "Cfinite q" using Card_order cinfinite_def cfinite_def by blast + then have "Cfinite (r +c q)" using Cfinite_csum outer by blast + moreover have "Cinfinite (r' +c q')" using Cinfinite_csum1 Cinfinite by blast + ultimately show ?thesis using Cfinite_ordLess_Cinfinite by blast + qed + qed +qed subsection \Exponentiation\ @@ -568,6 +655,14 @@ "\ctwo \o q; Cinfinite r\ \ Cinfinite (q ^c r)" by (simp add: cinfinite_cexp Card_order_cexp) +lemma card_order_cexp: + assumes "card_order r1" "card_order r2" + shows "card_order (r1 ^c r2)" +proof - + have "Field r1 = UNIV" "Field r2 = UNIV" using assms card_order_on_Card_order by auto + thus ?thesis unfolding cexp_def Func_def using card_of_card_order_on by simp +qed + lemma ctwo_ordLess_natLeq: "ctwo |A| \o r; |B| \o r; Cinfinite r\ \ |A \ B| \o r" by (auto simp add: cinfinite_def card_of_Un_ordLeq_infinite_Field) +lemma Un_Cinfinite_bound_strict: "\|A| \ |A \ B| |I| \o r; \i \ I. |A i| \o r; Cinfinite r\ \ |\i \ I. A i| \o r" by (auto simp add: card_of_UNION_ordLeq_infinite_Field cinfinite_def) @@ -606,6 +704,30 @@ by (blast intro: card_of_Times_ordLeq_infinite_Field) qed +lemma cprod_infinite2': "\Cnotzero r1; Cinfinite r2; r1 \o r2\ \ r1 *c r2 =o r2" + unfolding ordIso_iff_ordLeq + by (intro conjI cprod_cinfinite_bound ordLeq_cprod2 ordLeq_refl) + (auto dest!: ordIso_imp_ordLeq not_ordLeq_ordLess simp: czero_def Card_order_empty) + +lemma regularCard_cprod: + assumes "Cinfinite r" "Cinfinite s" "regularCard r" "regularCard s" + shows "regularCard (r *c s)" +proof (cases "r \o s") + case True + show ?thesis + apply (rule regularCard_ordIso[of s]) + apply (rule ordIso_symmetric[OF cprod_infinite2']) + using assms True Cinfinite_Cnotzero by auto +next + case False + have "Well_order r" "Well_order s" using assms card_order_on_well_order_on by auto + then have 1: "s \o r" using not_ordLeq_iff_ordLess ordLess_imp_ordLeq False by blast + show ?thesis + apply (rule regularCard_ordIso[of r]) + apply (rule ordIso_symmetric[OF cprod_infinite1']) + using assms 1 Cinfinite_Cnotzero by auto +qed + lemma cprod_csum_cexp: "r1 *c r2 \o (r1 +c r2) ^c ctwo" unfolding cprod_def csum_def cexp_def ctwo_def Field_card_of @@ -692,4 +814,27 @@ shows "\i \ Field (cardSuc r). B \ As i" using cardSuc_UNION assms unfolding cinfinite_def by blast +lemma Cinfinite_card_suc: "\ Cinfinite r ; card_order r \ \ Cinfinite (card_suc r)" + using Cinfinite_cong[OF cardSuc_ordIso_card_suc Cinfinite_cardSuc] . + +lemma regularCard_cardSuc: "Cinfinite k \ regularCard (cardSuc k)" + by (rule infinite_cardSuc_regularCard) (auto simp: cinfinite_def) + +lemma regular_card_suc: "card_order r \ Cinfinite r \ regularCard (card_suc r)" + using cardSuc_ordIso_card_suc Cinfinite_cardSuc regularCard_cardSuc regularCard_ordIso + by blast + +(* card_suc (natLeq +c |UNIV| ) *) + +lemma card_order_card_suc_natLeq_UNIV: "card_order (card_suc (natLeq +c |UNIV :: 'a set| ))" + using card_order_card_suc card_order_csum natLeq_card_order card_of_card_order_on by blast + +lemma cinfinite_card_suc_natLeq_UNIV: "cinfinite (card_suc (natLeq +c |UNIV :: 'a set| ))" + using Cinfinite_card_suc card_order_csum natLeq_card_order card_of_card_order_on natLeq_Cinfinite + Cinfinite_csum1 by blast + +lemma regularCard_card_suc_natLeq_UNIV: "regularCard (card_suc (natLeq +c |UNIV :: 'a set| ))" + using regular_card_suc card_order_csum natLeq_card_order card_of_card_order_on Cinfinite_csum1 + natLeq_Cinfinite by blast + end diff -r 7a6301d01199 -r 22d1c5f2b9f4 src/HOL/BNF_Cardinal_Order_Relation.thy --- a/src/HOL/BNF_Cardinal_Order_Relation.thy Sat Jun 25 09:50:40 2022 +0000 +++ b/src/HOL/BNF_Cardinal_Order_Relation.thy Mon Jun 27 15:54:18 2022 +0200 @@ -1,6 +1,7 @@ (* Title: HOL/BNF_Cardinal_Order_Relation.thy Author: Andrei Popescu, TU Muenchen - Copyright 2012 + Author: Jan van Brügge, TU Muenchen + Copyright 2012, 2022 Cardinal-order relations as needed by bounded natural functors. *) @@ -1425,6 +1426,66 @@ thus ?thesis by (simp only: card_of_cardSuc_finite) qed +lemma Field_cardSuc_not_empty: +assumes "Card_order r" +shows "Field (cardSuc r) \ {}" +proof + assume "Field(cardSuc r) = {}" + then have "|Field(cardSuc r)| \o r" using assms Card_order_empty[of r] by auto + then have "cardSuc r \o r" using assms card_of_Field_ordIso + cardSuc_Card_order ordIso_symmetric ordIso_ordLeq_trans by blast + then show False using cardSuc_greater not_ordLess_ordLeq assms by blast +qed + +typedef 'a suc = "Field (cardSuc |UNIV :: 'a set| )" + using Field_cardSuc_not_empty card_of_Card_order by blast + +definition card_suc :: "'a rel \ 'a suc rel" where + "card_suc \ \_. map_prod Abs_suc Abs_suc ` cardSuc |UNIV :: 'a set|" + +lemma Field_card_suc: "Field (card_suc r) = UNIV" +proof - + let ?r = "cardSuc |UNIV|" + let ?ar = "\x. Abs_suc (Rep_suc x)" + have 1: "\P. (\x\Field ?r. P x) = (\x. P (Rep_suc x))" using Rep_suc_induct Rep_suc by blast + have 2: "\P. (\x\Field ?r. P x) = (\x. P (Rep_suc x))" using Rep_suc_cases Rep_suc by blast + have 3: "\A a b. (a, b) \ A \ (Abs_suc a, Abs_suc b) \ map_prod Abs_suc Abs_suc ` A" unfolding map_prod_def by auto + have "\x\Field ?r. (\b\Field ?r. (x, b) \ ?r) \ (\a\Field ?r. (a, x) \ ?r)" + unfolding Field_def Range.simps Domain.simps Un_iff by blast + then have "\x. (\b. (Rep_suc x, Rep_suc b) \ ?r) \ (\a. (Rep_suc a, Rep_suc x) \ ?r)" unfolding 1 2 . + then have "\x. (\b. (?ar x, ?ar b) \ map_prod Abs_suc Abs_suc ` ?r) \ (\a. (?ar a, ?ar x) \ map_prod Abs_suc Abs_suc ` ?r)" using 3 by fast + then have "\x. (\b. (x, b) \ card_suc r) \ (\a. (a, x) \ card_suc r)" unfolding card_suc_def Rep_suc_inverse . + then show ?thesis unfolding Field_def Domain.simps Range.simps set_eq_iff Un_iff eqTrueI[OF UNIV_I] ex_simps simp_thms . +qed + +lemma card_suc_alt: "card_suc r = dir_image (cardSuc |UNIV :: 'a set| ) Abs_suc" + unfolding card_suc_def dir_image_def by auto + +lemma cardSuc_Well_order: "Card_order r \ Well_order(cardSuc r)" + using cardSuc_Card_order unfolding card_order_on_def by blast + +lemma cardSuc_ordIso_card_suc: + assumes "card_order r" + shows "cardSuc r =o card_suc (r :: 'a rel)" +proof - + have "cardSuc (r :: 'a rel) =o cardSuc |UNIV :: 'a set|" + using cardSuc_invar_ordIso[THEN iffD2, OF _ card_of_Card_order card_of_unique[OF assms]] assms + by (simp add: card_order_on_Card_order) + also have "cardSuc |UNIV :: 'a set| =o card_suc (r :: 'a rel)" + unfolding card_suc_alt + by (rule dir_image_ordIso) (simp_all add: inj_on_def Abs_suc_inject cardSuc_Well_order card_of_Card_order) + finally show ?thesis . +qed + +lemma Card_order_card_suc: "card_order r \ Card_order (card_suc r)" + using cardSuc_Card_order[THEN Card_order_ordIso2[OF _ cardSuc_ordIso_card_suc]] card_order_on_Card_order by blast + +lemma card_order_card_suc: "card_order r \ card_order (card_suc r)" + using Card_order_card_suc arg_cong2[OF Field_card_suc refl, of "card_order_on"] by blast + +lemma card_suc_greater: "card_order r \ r finite C" and LESS1: "|A| finite C" and + LESS1: "|A| B| finite (Field r)" and r: "Card_order r" and + LESS1: "|A| |?C| =o r" using r card_of_Field_ordIso + ordIso_symmetric by blast + hence "|A| Regular cardinals\ @@ -1689,4 +1771,228 @@ thus ?thesis using card_of_ordIso by blast qed +subsection \Regular vs. stable cardinals\ + +definition stable :: "'a rel \ bool" +where +"stable r \ \(A::'a set) (F :: 'a \ 'a set). + |A| (\a \ A. |F a| |SIGMA a : A. F a| finite (Field r)" and reg: "regularCard r" + shows "stable r" + unfolding stable_def proof safe + fix A :: "'a set" and F :: "'a \ 'a set" assume A: "|A| a\A. |F a| o |Sigma A F|" + hence "|Field r| \o |Sigma A F|" using card_of_Field_ordIso[OF cr] ordIso_ordLeq_trans by blast + moreover have Fi: "Field r \ {}" using ir by auto + ultimately have "\f. f ` Sigma A F = Field r" using card_of_ordLeq2[OF Fi] by blast + then obtain f where f: "f ` Sigma A F = Field r" by blast + have r: "wo_rel r" using cr unfolding card_order_on_def wo_rel_def by auto + {fix a assume a: "a \ A" + define L where "L = {(a,u) | u. u \ F a}" + have fL: "f ` L \ Field r" using f a unfolding L_def by auto + have "|L| =o |F a|" unfolding L_def card_of_ordIso[symmetric] + apply(rule exI[of _ snd]) unfolding bij_betw_def inj_on_def by (auto simp: image_def) + hence "|L| cofinal (f ` L) r" using reg fL unfolding regularCard_def + apply simp + apply (drule not_ordLess_ordIso) + by auto + then obtain k where k: "k \ Field r" and "\ l \ L. \ (f l \ k \ (k, f l) \ r)" + unfolding cofinal_def image_def by auto + hence "\ k \ Field r. \ l \ L. (f l, k) \ r" + using wo_rel.in_notinI[OF r _ _ \k \ Field r\] fL unfolding image_subset_iff by fast + hence "\ k \ Field r. \ u \ F a. (f (a,u), k) \ r" unfolding L_def by auto + } + then have x: "\a. a\A \ \k. k \ Field r \ (\u\F a. (f (a, u), k) \ r)" by blast + obtain gg where "\a. a\A \ gg a = (SOME k. k \ Field r \ (\u\F a. (f (a, u), k) \ r))" by simp + then have gg: "\a\A. \u\F a. (f (a, u), gg a) \ r" using someI_ex[OF x] by auto + obtain j0 where j0: "j0 \ Field r" using Fi by auto + define g where [abs_def]: "g a = (if F a \ {} then gg a else j0)" for a + have g: "\ a \ A. \ u \ F a. (f (a,u),g a) \ r" using gg unfolding g_def by auto + hence 1: "Field r \ (\a \ A. under r (g a))" + using f[symmetric] unfolding under_def image_def by auto + have gA: "g ` A \ Field r" using gg j0 unfolding Field_def g_def by auto + moreover have "cofinal (g ` A) r" unfolding cofinal_def proof safe + fix i assume "i \ Field r" + then obtain j where ij: "(i,j) \ r" "i \ j" using cr ir infinite_Card_order_limit by fast + hence "j \ Field r" using card_order_on_def cr well_order_on_domain by fast + then obtain a where a: "a \ A" and j: "(j, g a) \ r" using 1 unfolding under_def by auto + hence "(i, g a) \ r" using ij wo_rel.TRANS[OF r] unfolding trans_def by blast + moreover have "i \ g a" + using ij j r unfolding wo_rel_def unfolding well_order_on_def linear_order_on_def + partial_order_on_def antisym_def by auto + ultimately show "\j\g ` A. i \ j \ (i, j) \ r" using a by auto + qed + ultimately have "|g ` A| =o r" using reg unfolding regularCard_def by auto + moreover have "|g ` A| \o |A|" using card_of_image by blast + ultimately have False using A using not_ordLess_ordIso ordLeq_ordLess_trans by blast + } + thus "|Sigma A F| finite (Field r)" and st: "stable r" +shows "regularCard r" +unfolding regularCard_def proof safe + fix K assume K: "K \ Field r" and cof: "cofinal K r" + have "|K| \o r" using K card_of_Field_ordIso card_of_mono1 cr ordLeq_ordIso_trans by blast + moreover + {assume Kr: "|K| a. a \ Field r \ \b. b \ K \ a \ b \ (a, b) \ r" using cof unfolding cofinal_def by blast + then obtain f where "\a. a \ Field r \ f a = (SOME b. b \ K \ a \ b \ (a, b) \ r)" by simp + then have "\a\Field r. f a \ K \ a \ f a \ (a, f a) \ r" using someI_ex[OF x] by simp + hence "Field r \ (\a \ K. underS r a)" unfolding underS_def by auto + hence "r \o |\a \ K. underS r a|" + using cr Card_order_iff_ordLeq_card_of card_of_mono1 ordLeq_transitive by blast + also have "|\a \ K. underS r a| \o |SIGMA a: K. underS r a|" by (rule card_of_UNION_Sigma) + also + {have "\ a \ K. |underS r a| B < Field r. |A| =o |B| \ |B| |A| =o p \ p |Field p| B < Field r. |A| =o |B| \ |B| B < Field r. |A| =o |B| \ |B| i \ I. |A i| =o |B i|" +shows "|SIGMA i : I. A i| =o |SIGMA i : I. B i|" +using assms by (auto simp add: card_of_Sigma_mono1 ordIso_iff_ordLeq) + +lemma card_of_Sigma_cong2: +assumes "bij_betw f (I::'i set) (J::'j set)" +shows "|SIGMA i : I. (A::'j \ 'a set) (f i)| =o |SIGMA j : J. A j|" +proof- + let ?LEFT = "SIGMA i : I. A (f i)" + let ?RIGHT = "SIGMA j : J. A j" + obtain u where u_def: "u = (\(i::'i,a::'a). (f i,a))" by blast + have "bij_betw u ?LEFT ?RIGHT" + using assms unfolding u_def bij_betw_def inj_on_def by auto + thus ?thesis using card_of_ordIso by blast +qed + +lemma card_of_Sigma_cong: +assumes BIJ: "bij_betw f I J" and + ISO: "\j \ J. |A j| =o |B j|" +shows "|SIGMA i : I. A (f i)| =o |SIGMA j : J. B j|" +proof- + have "\i \ I. |A(f i)| =o |B(f i)|" + using ISO BIJ unfolding bij_betw_def by blast + hence "|SIGMA i : I. A (f i)| =o |SIGMA i : I. B (f i)|" by (rule card_of_Sigma_cong1) + moreover have "|SIGMA i : I. B (f i)| =o |SIGMA j : J. B j|" + using BIJ card_of_Sigma_cong2 by blast + ultimately show ?thesis using ordIso_transitive by blast +qed + +(* Note that below the types of A and F are now unconstrained: *) +lemma stable_elim: +assumes ST: "stable r" and A_LESS: "|A| a. a \ A \ |F a| |A'| A" + hence "\B'. B' \ Field r \ |F a| =o |B'| \ |B'| a \ A. F' a \ Field r \ |F a| =o |F' a| \ |F' a| a B'. B' \ Field r \ |F a| =o |B'| \ |B'| a \ A. F' a \ Field r \ |F' a| a \ A. |F' a| =o |F a|" using temp ordIso_symmetric by auto + (* *) + have "\a' \ A'. F'(G a') \ Field r \ |F'(G a')| 'a set" + assume "|A| a\A. |F a| (\a \ A. finite(F a))" + by (auto simp add: finite_iff_ordLess_natLeq) + hence "finite(Sigma A F)" by (simp only: finite_SigmaI[of A F]) + thus "|Sigma A F | 'b set" + assume "|A| a \ A. |F a| (\a \ A. |F a| a. a \ A \ |F a| a \ A. F a| a \ A. F a| \o |SIGMA a : A. F a|" + using card_of_UNION_Sigma by blast + thus ?thesis using assms stable_elim ordLeq_ordLess_trans by blast +qed + +corollary card_of_UNION_ordLess_infinite: +assumes INF: "stable |B|" and + LEQ_I: "|I| i \ I. |A i| i \ I. A i| i \ I. |A i| i \ I. A i| |?B| =o r" using r card_of_Field_ordIso + ordIso_symmetric by blast + hence "|I| i \ I. |A i| i \ I. A i| _. {}) \ f = image g \ (\_. {})" by (rule ext) simp +lemma Cinfinite_gt_empty: "Cinfinite r \ |{}| image (image f) = image f \ Union" by (rule ext) (auto simp only: comp_apply) lemma in_Union_o_assoc: "x \ (Union \ gset \ gmap) A \ x \ (Union \ (gset \ gmap)) A" by (unfold comp_assoc) +lemma regularCard_UNION_bound: + assumes "Cinfinite r" "regularCard r" and "|I| i. i \ I \ |A i| i\I. A i| x. |fset x| x. |gset x| (fset ` gset x)| (fset ` gset x)| (fset ` gset x)| o fbd" using not_ordLess_iff_ordLeq False by blast + then have "|gset x| (fset ` gset x)| x. |fset x| \o fbd" and @@ -75,6 +106,9 @@ lemma comp_set_bd_Union_o_collect: "|\(\((\f. f x) ` X))| \o hbd \ |(Union \ collect X) x| \o hbd" by (unfold comp_apply collect_def) simp +lemma comp_set_bd_Union_o_collect_strict: "|\(\((\f. f x) ` X))| |(Union \ collect X) x| P = Q" by blast @@ -91,7 +125,7 @@ lemma type_copy_map_cong0: "M (g x) = N (h x) \ (f \ M \ g) x = (f \ N \ h) x" by auto -lemma type_copy_set_bd: "(\y. |S y| \o bd) \ |(S \ Rep) x| \o bd" +lemma type_copy_set_bd: "(\y. |S y| |(S \ Rep) x| vimage2p f g R = vimage2p f g S" @@ -152,7 +186,7 @@ map: "id :: 'a \ 'a" bd: natLeq rel: "(=) :: 'a \ 'a \ bool" - by (auto simp add: natLeq_card_order natLeq_cinfinite) + by (auto simp add: natLeq_card_order natLeq_cinfinite regularCard_natLeq) definition id_bnf :: "'a \ 'a" where "id_bnf \ (\x. x)" @@ -167,8 +201,8 @@ rel: "id_bnf :: ('a \ 'b \ bool) \ 'a \ 'b \ bool" pred: "id_bnf :: ('a \ bool) \ 'a \ bool" unfolding id_bnf_def - apply (auto simp: Grp_def fun_eq_iff relcompp.simps natLeq_card_order natLeq_cinfinite) - apply (rule ordLess_imp_ordLeq[OF finite_ordLess_infinite[OF _ natLeq_Well_order]]) + apply (auto simp: Grp_def fun_eq_iff relcompp.simps natLeq_card_order natLeq_cinfinite regularCard_natLeq) + apply (rule finite_ordLess_infinite[OF _ natLeq_Well_order]) apply (auto simp add: Field_card_of Field_natLeq card_of_well_order_on)[3] done diff -r 7a6301d01199 -r 22d1c5f2b9f4 src/HOL/BNF_Greatest_Fixpoint.thy --- a/src/HOL/BNF_Greatest_Fixpoint.thy Sat Jun 25 09:50:40 2022 +0000 +++ b/src/HOL/BNF_Greatest_Fixpoint.thy Mon Jun 27 15:54:18 2022 +0200 @@ -281,6 +281,24 @@ thus "univ f X \ B" using x PRES by simp qed +lemma card_suc_ordLess_imp_ordLeq: + assumes ORD: "Card_order r" "Card_order r'" "card_order r'" + and LESS: "r o r'" +proof - + have "Card_order (card_suc r')" by (rule Card_order_card_suc[OF ORD(3)]) + then have "cardSuc r \o card_suc r'" using cardSuc_least ORD LESS by blast + then have "cardSuc r \o cardSuc r'" using cardSuc_ordIso_card_suc ordIso_symmetric + ordLeq_ordIso_trans ORD(3) by blast + then show ?thesis using cardSuc_mono_ordLeq ORD by blast +qed + +lemma natLeq_ordLess_cinfinite: "\Cinfinite r; card_order r\ \ natLeq Cinfinite r'; card_order r'; r \ card_suc r'\ \ natLeq Tools/BNF/bnf_gfp_util.ML\ ML_file \Tools/BNF/bnf_gfp_tactics.ML\ ML_file \Tools/BNF/bnf_gfp.ML\ diff -r 7a6301d01199 -r 22d1c5f2b9f4 src/HOL/BNF_Wellorder_Constructions.thy --- a/src/HOL/BNF_Wellorder_Constructions.thy Sat Jun 25 09:50:40 2022 +0000 +++ b/src/HOL/BNF_Wellorder_Constructions.thy Mon Jun 27 15:54:18 2022 +0200 @@ -561,6 +561,10 @@ "r \ r' \o r" using ordLess_ordLeq_trans ordLess_irreflexive by blast +lemma not_ordLeq_ordLess: +"r \o r' \ \ r' r' \o r" diff -r 7a6301d01199 -r 22d1c5f2b9f4 src/HOL/BNF_Wellorder_Relation.thy --- a/src/HOL/BNF_Wellorder_Relation.thy Sat Jun 25 09:50:40 2022 +0000 +++ b/src/HOL/BNF_Wellorder_Relation.thy Mon Jun 27 15:54:18 2022 +0200 @@ -190,6 +190,9 @@ using assms ANTISYM unfolding antisym_def using TOTALS unfolding max2_def by auto +lemma in_notinI: +assumes "(j,i) \ r \ j = i" and "i \ Field r" and "j \ Field r" +shows "(i,j) \ r" using assms max2_def max2_greater_among by fastforce subsubsection \Existence and uniqueness for isMinim and well-definedness of minim\ diff -r 7a6301d01199 -r 22d1c5f2b9f4 src/HOL/Basic_BNFs.thy --- a/src/HOL/Basic_BNFs.thy Sat Jun 25 09:50:40 2022 +0000 +++ b/src/HOL/Basic_BNFs.thy Mon Jun 27 15:54:18 2022 +0200 @@ -2,7 +2,8 @@ Author: Dmitriy Traytel, TU Muenchen Author: Andrei Popescu, TU Muenchen Author: Jasmin Blanchette, TU Muenchen - Copyright 2012 + Author: Jan van Brügge + Copyright 2012, 2022 Registration of basic types as bounded natural functors. *) @@ -77,15 +78,15 @@ next show "cinfinite natLeq" by (rule natLeq_cinfinite) next + show "regularCard natLeq" by (rule regularCard_natLeq) +next fix x :: "'o + 'p" - show "|setl x| \o natLeq" - apply (rule ordLess_imp_ordLeq) + show "|setl x| o natLeq" - apply (rule ordLess_imp_ordLeq) + show "|setr x| o natLeq" - by (rule ordLess_imp_ordLeq) (simp add: finite_iff_ordLess_natLeq[symmetric]) + show "regularCard natLeq" by (rule regularCard_natLeq) next fix x - show "|{snd x}| \o natLeq" - by (rule ordLess_imp_ordLeq) (simp add: finite_iff_ordLess_natLeq[symmetric]) + show "|{fst x}| rel_prod (R1 OO S1) (R2 OO S2)" by auto @@ -190,7 +193,7 @@ bnf "'a \ 'b" map: "(\)" sets: range - bd: "natLeq +c |UNIV :: 'a set|" + bd: "card_suc (natLeq +c |UNIV::'a set|)" rel: "rel_fun (=)" pred: "pred_fun (\_. True)" proof @@ -206,20 +209,38 @@ fix f show "range \ (\) f = (`) f \ range" by (auto simp add: fun_eq_iff) next - show "card_order (natLeq +c |UNIV| )" (is "_ (_ +c ?U)") - apply (rule card_order_csum) - apply (rule natLeq_card_order) - by (rule card_of_card_order_on) -(* *) - show "cinfinite (natLeq +c ?U)" - apply (rule cinfinite_csum) + show "card_order (card_suc (natLeq +c |UNIV|))" + apply (rule card_order_card_suc) + apply (rule card_order_csum) + apply (rule natLeq_card_order) + by (rule card_of_card_order_on) +next + have "Cinfinite (card_suc (natLeq +c |UNIV| ))" + apply (rule Cinfinite_card_suc) + apply (rule Cinfinite_csum) + apply (rule disjI1) + apply (rule natLeq_Cinfinite) + apply (rule card_order_csum) + apply (rule natLeq_card_order) + by (rule card_of_card_order_on) + then show "cinfinite (card_suc (natLeq +c |UNIV|))" by blast +next + show "regularCard (card_suc (natLeq +c |UNIV|))" + apply (rule regular_card_suc) + apply (rule card_order_csum) + apply (rule natLeq_card_order) + apply (rule card_of_card_order_on) + apply (rule Cinfinite_csum) apply (rule disjI1) - by (rule natLeq_cinfinite) + by (rule natLeq_Cinfinite) next fix f :: "'d => 'a" have "|range f| \o | (UNIV::'d set) |" (is "_ \o ?U") by (rule card_of_image) - also have "?U \o natLeq +c ?U" by (rule ordLeq_csum2) (rule card_of_Card_order) - finally show "|range f| \o natLeq +c ?U" . + then have 1: "|range f| \o natLeq +c ?U" using ordLeq_transitive ordLeq_csum2 card_of_Card_order by blast + have "natLeq +c ?U rel_fun (=) (R OO S)" by (auto simp: rel_fun_def) diff -r 7a6301d01199 -r 22d1c5f2b9f4 src/HOL/Cardinals/Bounded_Set.thy --- a/src/HOL/Cardinals/Bounded_Set.thy Sat Jun 25 09:50:40 2022 +0000 +++ b/src/HOL/Cardinals/Bounded_Set.thy Mon Jun 27 15:54:18 2022 +0200 @@ -74,7 +74,7 @@ bnf "'a set['k]" map: map_bset sets: set_bset - bd: "natLeq +c |UNIV :: 'k set|" + bd: "card_suc (natLeq +c |UNIV :: 'k set| )" wits: bempty rel: rel_bset proof - @@ -91,8 +91,10 @@ show "set_bset \ map_bset f = (`) f \ set_bset" by (rule ext, transfer) auto next fix X :: "'a set['k]" - show "|set_bset X| \o natLeq +c |UNIV :: 'k set|" - by transfer (blast dest: ordLess_imp_ordLeq) + have "|set_bset X| rel_bset (R OO S)" @@ -107,7 +109,8 @@ fix x assume "x \ set_bset bempty" then show False by transfer simp -qed (simp_all add: card_order_csum natLeq_card_order cinfinite_csum natLeq_cinfinite) +qed (simp_all add: card_order_card_suc_natLeq_UNIV cinfinite_card_suc_natLeq_UNIV + regularCard_card_suc_natLeq_UNIV) lemma map_bset_bempty[simp]: "map_bset f bempty = bempty" diff -r 7a6301d01199 -r 22d1c5f2b9f4 src/HOL/Cardinals/Cardinal_Order_Relation.thy --- a/src/HOL/Cardinals/Cardinal_Order_Relation.thy Sat Jun 25 09:50:40 2022 +0000 +++ b/src/HOL/Cardinals/Cardinal_Order_Relation.thy Mon Jun 27 15:54:18 2022 +0200 @@ -91,22 +91,6 @@ lemma card_of_unique2: "\card_order_on B r; bij_betw f A B\ \ r =o |A|" using card_of_ordIso card_of_unique ordIso_equivalence by blast -lemma internalize_card_of_ordLess: -"( |A| B < Field r. |A| =o |B| \ |B| |A| =o p \ p |Field p| B < Field r. |A| =o |B| \ |B| B < Field r. |A| =o |B| \ |B| B < C. |A| =o |B| \ |B| i. Field(p i)" "\ j. Field(r j)"] by metis -lemma card_of_Sigma_cong1: -assumes "\i \ I. |A i| =o |B i|" -shows "|SIGMA i : I. A i| =o |SIGMA i : I. B i|" -using assms by (auto simp add: card_of_Sigma_mono1 ordIso_iff_ordLeq) - -lemma card_of_Sigma_cong2: -assumes "bij_betw f (I::'i set) (J::'j set)" -shows "|SIGMA i : I. (A::'j \ 'a set) (f i)| =o |SIGMA j : J. A j|" -proof- - let ?LEFT = "SIGMA i : I. A (f i)" - let ?RIGHT = "SIGMA j : J. A j" - obtain u where u_def: "u = (\(i::'i,a::'a). (f i,a))" by blast - have "bij_betw u ?LEFT ?RIGHT" - using assms unfolding u_def bij_betw_def inj_on_def by auto - thus ?thesis using card_of_ordIso by blast -qed - -lemma card_of_Sigma_cong: -assumes BIJ: "bij_betw f I J" and - ISO: "\j \ J. |A j| =o |B j|" -shows "|SIGMA i : I. A (f i)| =o |SIGMA j : J. B j|" -proof- - have "\i \ I. |A(f i)| =o |B(f i)|" - using ISO BIJ unfolding bij_betw_def by blast - hence "|SIGMA i : I. A (f i)| =o |SIGMA i : I. B (f i)|" by (rule card_of_Sigma_cong1) - moreover have "|SIGMA i : I. B (f i)| =o |SIGMA j : J. B j|" - using BIJ card_of_Sigma_cong2 by blast - ultimately show ?thesis using ordIso_transitive by blast -qed - lemma ordIso_Sigma_cong1: assumes "\i \ I. p i =o r i" shows "|SIGMA i : I. Field(p i)| =o |SIGMA i : I. Field(r i)|" @@ -1656,62 +1610,6 @@ subsection \Regular vs. stable cardinals\ -definition stable :: "'a rel \ bool" -where -"stable r \ \(A::'a set) (F :: 'a \ 'a set). - |A| (\a \ A. |F a| |SIGMA a : A. F a| finite (Field r)" and reg: "regularCard r" -shows "stable r" -unfolding stable_def proof safe - fix A :: "'a set" and F :: "'a \ 'a set" assume A: "|A| a\A. |F a| o |Sigma A F|" - hence "|Field r| \o |Sigma A F|" using card_of_Field_ordIso[OF cr] - by (metis Field_card_of card_of_cong ordLeq_iff_ordLess_or_ordIso ordLeq_ordLess_trans) - moreover have Fi: "Field r \ {}" using ir by auto - ultimately obtain f where f: "f ` Sigma A F = Field r" using card_of_ordLeq2 by metis - have r: "wo_rel r" using cr unfolding card_order_on_def wo_rel_def by auto - {fix a assume a: "a \ A" - define L where "L = {(a,u) | u. u \ F a}" - have fL: "f ` L \ Field r" using f a unfolding L_def by auto - have "|L| =o |F a|" unfolding L_def card_of_ordIso[symmetric] - apply(rule exI[of _ snd]) unfolding bij_betw_def inj_on_def by (auto simp: image_def) - hence "|L| cofinal (f ` L) r" using reg fL unfolding regularCard_def by (metis not_ordLess_ordIso) - then obtain k where k: "k \ Field r" and "\ l \ L. \ (f l \ k \ (k, f l) \ r)" - unfolding cofinal_def image_def by auto - hence "\ k \ Field r. \ l \ L. (f l, k) \ r" using r by (metis fL image_subset_iff wo_rel.in_notinI) - hence "\ k \ Field r. \ u \ F a. (f (a,u), k) \ r" unfolding L_def by auto - } - then obtain gg where gg: "\ a \ A. \ u \ F a. (f (a,u), gg a) \ r" by metis - obtain j0 where j0: "j0 \ Field r" using Fi by auto - define g where [abs_def]: "g a = (if F a \ {} then gg a else j0)" for a - have g: "\ a \ A. \ u \ F a. (f (a,u),g a) \ r" using gg unfolding g_def by auto - hence 1: "Field r \ (\a \ A. under r (g a))" - using f[symmetric] unfolding under_def image_def by auto - have gA: "g ` A \ Field r" using gg j0 unfolding Field_def g_def by auto - moreover have "cofinal (g ` A) r" unfolding cofinal_def proof safe - fix i assume "i \ Field r" - then obtain j where ij: "(i,j) \ r" "i \ j" using cr ir by (metis infinite_Card_order_limit) - hence "j \ Field r" by (metis card_order_on_def cr well_order_on_domain) - then obtain a where a: "a \ A" and j: "(j, g a) \ r" using 1 unfolding under_def by auto - hence "(i, g a) \ r" using ij wo_rel.TRANS[OF r] unfolding trans_def by blast - moreover have "i \ g a" - using ij j r unfolding wo_rel_def unfolding well_order_on_def linear_order_on_def - partial_order_on_def antisym_def by auto - ultimately show "\j\g ` A. i \ j \ (i, j) \ r" using a by auto - qed - ultimately have "|g ` A| =o r" using reg unfolding regularCard_def by auto - moreover have "|g ` A| \o |A|" by (metis card_of_image) - ultimately have False using A by (metis not_ordLess_ordIso ordLeq_ordLess_trans) - } - thus "|Sigma A F| finite (Field r)" and st: "stable r" shows "regularCard r" @@ -1736,36 +1634,6 @@ ultimately show "|K| =o r" by (metis ordLeq_iff_ordLess_or_ordIso) qed -(* Note that below the types of A and F are now unconstrained: *) -lemma stable_elim: -assumes ST: "stable r" and A_LESS: "|A| a. a \ A \ |F a| |A'| A" - hence "\B'. B' \ Field r \ |F a| =o |B'| \ |B'| a \ A. F' a \ Field r \ |F a| =o |F' a| \ |F' a| a B'. B' \ Field r \ |F a| =o |B'| \ |B'| a \ A. F' a \ Field r \ |F' a| a \ A. |F' a| =o |F a|" using temp ordIso_symmetric by auto - (* *) - have "\a' \ A'. F'(G a') \ Field r \ |F'(G a')| 'a set" @@ -1786,16 +1654,6 @@ using infinite_cardSuc_regularCard regularCard_stable by (metis CARD INF cardSuc_Card_order cardSuc_finite) -lemma stable_UNION: -assumes ST: "stable r" and A_LESS: "|A| a. a \ A \ |F a| a \ A. F a| a \ A. F a| \o |SIGMA a : A. F a|" - using card_of_UNION_Sigma by blast - thus ?thesis using assms stable_elim ordLeq_ordLess_trans by blast -qed - lemma stable_ordIso1: assumes ST: "stable r" and ISO: "r' =o r" shows "stable r'" diff -r 7a6301d01199 -r 22d1c5f2b9f4 src/HOL/Cardinals/Fun_More.thy --- a/src/HOL/Cardinals/Fun_More.thy Sat Jun 25 09:50:40 2022 +0000 +++ b/src/HOL/Cardinals/Fun_More.thy Mon Jun 27 15:54:18 2022 +0200 @@ -38,12 +38,6 @@ qed (* unused *) -(*1*)lemma bij_betw_ball: -assumes BIJ: "bij_betw f A B" -shows "(\b \ B. phi b) = (\a \ A. phi(f a))" -using assms unfolding bij_betw_def inj_on_def by blast - -(* unused *) (*1*)lemma bij_betw_diff_singl: assumes BIJ: "bij_betw f A A'" and IN: "a \ A" shows "bij_betw f (A - {a}) (A' - {f a})" diff -r 7a6301d01199 -r 22d1c5f2b9f4 src/HOL/Cardinals/Wellorder_Constructions.thy --- a/src/HOL/Cardinals/Wellorder_Constructions.thy Sat Jun 25 09:50:40 2022 +0000 +++ b/src/HOL/Cardinals/Wellorder_Constructions.thy Mon Jun 27 15:54:18 2022 +0200 @@ -511,10 +511,6 @@ ultimately show "a = b" using TOTALS A a b unfolding underS_def by auto qed -lemma in_notinI: -assumes "(j,i) \ r \ j = i" and "i \ Field r" and "j \ Field r" -shows "(i,j) \ r" by (metis assms max2_def max2_greater_among) - lemma ofilter_init_seg_of: assumes "ofilter F" shows "Restr r F initial_segment_of r" diff -r 7a6301d01199 -r 22d1c5f2b9f4 src/HOL/Fun.thy --- a/src/HOL/Fun.thy Sat Jun 25 09:50:40 2022 +0000 +++ b/src/HOL/Fun.thy Mon Jun 27 15:54:18 2022 +0200 @@ -457,6 +457,9 @@ lemma bij_betw_subset: "bij_betw f A A' \ B \ A \ f ` B = B' \ bij_betw f B B'" by (auto simp add: bij_betw_def inj_on_def) +lemma bij_betw_ball: "bij_betw f A B \ (\b \ B. phi b) = (\a \ A. phi (f a))" + unfolding bij_betw_def inj_on_def by blast + lemma bij_pointE: assumes "bij f" obtains x where "y = f x" and "\x'. y = f x' \ x' = x" diff -r 7a6301d01199 -r 22d1c5f2b9f4 src/HOL/Library/Countable_Set_Type.thy --- a/src/HOL/Library/Countable_Set_Type.thy Sat Jun 25 09:50:40 2022 +0000 +++ b/src/HOL/Library/Countable_Set_Type.thy Mon Jun 27 15:54:18 2022 +0200 @@ -593,7 +593,7 @@ bnf "'a cset" map: cimage sets: rcset - bd: natLeq + bd: "card_suc natLeq" wits: "cempty" rel: rel_cset proof - @@ -606,12 +606,18 @@ next fix f show "rcset \ cimage f = (`) f \ rcset" including cset.lifting by transfer' fastforce next - show "card_order natLeq" by (rule natLeq_card_order) + show "card_order (card_suc natLeq)" by (rule card_order_card_suc[OF natLeq_card_order]) +next + show "cinfinite (card_suc natLeq)" using Cinfinite_card_suc[OF natLeq_Cinfinite natLeq_card_order] + by simp next - show "cinfinite natLeq" by (rule natLeq_cinfinite) + show "regularCard (card_suc natLeq)" using natLeq_card_order natLeq_Cinfinite + by (rule regular_card_suc) next - fix C show "|rcset C| \o natLeq" - including cset.lifting by transfer (unfold countable_card_le_natLeq) + fix C + have "|rcset C| \o natLeq" including cset.lifting by transfer (unfold countable_card_le_natLeq) + then show "|rcset C| rel_cset (R OO S)" diff -r 7a6301d01199 -r 22d1c5f2b9f4 src/HOL/Library/FSet.thy --- a/src/HOL/Library/FSet.thy Sat Jun 25 09:50:40 2022 +0000 +++ b/src/HOL/Library/FSet.thy Mon Jun 27 15:54:18 2022 +0200 @@ -1167,8 +1167,9 @@ apply transfer apply force apply transfer' apply force apply (rule natLeq_card_order) - apply (rule natLeq_cinfinite) - apply transfer apply (metis ordLess_imp_ordLeq finite_iff_ordLess_natLeq) + apply (rule natLeq_cinfinite) + apply (rule regularCard_natLeq) + apply transfer apply (metis finite_iff_ordLess_natLeq) apply (fastforce simp: rel_fset_alt) apply (simp add: Grp_def relcompp.simps conversep.simps fun_eq_iff rel_fset_alt rel_fset_aux[unfolded OO_Grp_alt]) diff -r 7a6301d01199 -r 22d1c5f2b9f4 src/HOL/Library/Multiset.thy --- a/src/HOL/Library/Multiset.thy Sat Jun 25 09:50:40 2022 +0000 +++ b/src/HOL/Library/Multiset.thy Mon Jun 27 15:54:18 2022 +0200 @@ -4088,9 +4088,11 @@ by (rule natLeq_card_order) show "BNF_Cardinal_Arithmetic.cinfinite natLeq" by (rule natLeq_cinfinite) - show "ordLeq3 (card_of (set_mset X)) natLeq" for X + show "regularCard natLeq" + by (rule regularCard_natLeq) + show "ordLess2 (card_of (set_mset X)) natLeq" for X by transfer - (auto intro!: ordLess_imp_ordLeq simp: finite_iff_ordLess_natLeq[symmetric]) + (auto simp: finite_iff_ordLess_natLeq[symmetric]) show "rel_mset R OO rel_mset S \ rel_mset (R OO S)" for R S unfolding rel_mset_def[abs_def] OO_def apply clarify diff -r 7a6301d01199 -r 22d1c5f2b9f4 src/HOL/Library/Uprod.thy --- a/src/HOL/Library/Uprod.thy Sat Jun 25 09:50:40 2022 +0000 +++ b/src/HOL/Library/Uprod.thy Mon Jun 27 15:54:18 2022 +0200 @@ -128,8 +128,9 @@ show "set_uprod \ map_uprod f = (`) f \ set_uprod" for f :: "'a \ 'b" by transfer auto show "card_order natLeq" by(rule natLeq_card_order) show "BNF_Cardinal_Arithmetic.cinfinite natLeq" by(rule natLeq_cinfinite) - show "ordLeq3 (card_of (set_uprod x)) natLeq" for x :: "'a uprod" - by (auto simp flip: finite_iff_ordLess_natLeq intro: ordLess_imp_ordLeq) + show "regularCard natLeq" by(rule regularCard_natLeq) + show "ordLess2 (card_of (set_uprod x)) natLeq" for x :: "'a uprod" + by (auto simp flip: finite_iff_ordLess_natLeq) show "rel_uprod R OO rel_uprod S \ rel_uprod (R OO S)" for R :: "'a \ 'b \ bool" and S :: "'b \ 'c \ bool" by(rule predicate2I)(transfer; auto) show "rel_uprod R = (\x y. \z. set_uprod z \ {(x, y). R x y} \ map_uprod fst z = x \ map_uprod snd z = y)" diff -r 7a6301d01199 -r 22d1c5f2b9f4 src/HOL/Probability/Probability_Mass_Function.thy --- a/src/HOL/Probability/Probability_Mass_Function.thy Sat Jun 25 09:50:40 2022 +0000 +++ b/src/HOL/Probability/Probability_Mass_Function.thy Mon Jun 27 15:54:18 2022 +0200 @@ -1355,7 +1355,7 @@ by auto qed -bnf pmf: "'a pmf" map: map_pmf sets: set_pmf bd : "natLeq" rel: rel_pmf +bnf pmf: "'a pmf" map: map_pmf sets: set_pmf bd : "card_suc natLeq" rel: rel_pmf proof - show "map_pmf id = id" by (rule map_pmf_id) show "\f g. map_pmf (f \ g) = map_pmf f \ map_pmf g" by (rule map_pmf_compose) @@ -1365,14 +1365,20 @@ show "\f::'a \ 'b. set_pmf \ map_pmf f = (`) f \ set_pmf" by (rule pmf_set_map) - show "(card_of (set_pmf p), natLeq) \ ordLeq" for p :: "'s pmf" + show "card_order (card_suc natLeq)" using natLeq_card_order by (rule card_order_card_suc) + show "BNF_Cardinal_Arithmetic.cinfinite (card_suc natLeq)" + using natLeq_Cinfinite natLeq_card_order Cinfinite_card_suc by blast + show "regularCard (card_suc natLeq)" using natLeq_card_order natLeq_Cinfinite + by (rule regular_card_suc) + + show "(card_of (set_pmf p), card_suc natLeq) \ ordLess" for p :: "'s pmf" proof - have "(card_of (set_pmf p), card_of (UNIV :: nat set)) \ ordLeq" by (rule card_of_ordLeqI[where f="to_nat_on (set_pmf p)"]) (auto intro: countable_set_pmf) also have "(card_of (UNIV :: nat set), natLeq) \ ordLeq" by (metis Field_natLeq card_of_least natLeq_Well_order) - finally show ?thesis . + finally show ?thesis using card_suc_greater natLeq_card_order ordLeq_ordLess_trans by blast qed show "\R. rel_pmf R = (\x y. \z. set_pmf z \ {(x, y). R x y} \ @@ -1413,7 +1419,7 @@ then show ?thesis by(auto simp add: le_fun_def) qed -qed (fact natLeq_card_order natLeq_cinfinite)+ +qed lemma map_pmf_idI: "(\x. x \ set_pmf p \ f x = x) \ map_pmf f p = p" by(simp cong: pmf.map_cong) diff -r 7a6301d01199 -r 22d1c5f2b9f4 src/HOL/Tools/BNF/bnf_comp.ML --- a/src/HOL/Tools/BNF/bnf_comp.ML Sat Jun 25 09:50:40 2022 +0000 +++ b/src/HOL/Tools/BNF/bnf_comp.ML Mon Jun 27 15:54:18 2022 +0200 @@ -298,6 +298,10 @@ fun bd_cinfinite_tac ctxt = mk_comp_bd_cinfinite_tac ctxt (bd_cinfinite_of_bnf inner) (bd_cinfinite_of_bnf outer); + fun bd_regularCard_tac ctxt = + mk_comp_bd_regularCard_tac ctxt (map bd_regularCard_of_bnf inners) (bd_regularCard_of_bnf outer) + (map bd_Cinfinite_of_bnf inners) (bd_Cinfinite_of_bnf outer); + val set_alt_thms = if Config.get lthy quick_and_dirty then [] @@ -320,15 +324,23 @@ let val outer_set_bds = set_bd_of_bnf outer; val inner_set_bdss = map set_bd_of_bnf inners; - val inner_bd_Card_orders = map bd_Card_order_of_bnf inners; + val inner_bd_Cinfinites = map bd_Cinfinite_of_bnf inners; + val inner_bd_regularCards = map bd_regularCard_of_bnf inners; fun single_set_bd_thm i j = - @{thm comp_single_set_bd} OF [nth inner_bd_Card_orders j, nth (nth inner_set_bdss j) i, + @{thm comp_single_set_bd_strict} OF [nth inner_bd_Cinfinites j, nth inner_bd_regularCards j, + bd_Cinfinite_of_bnf outer, bd_regularCard_of_bnf outer, nth (nth inner_set_bdss j) i, nth outer_set_bds j] + fun single_bd_Cinfinite i = @{thm Cinfinite_cprod2} OF [ + @{thm Cinfinite_Cnotzero} OF [bd_Cinfinite_of_bnf outer], + nth inner_bd_Cinfinites i + ] val single_set_bd_thmss = map ((fn f => map f (0 upto olive - 1)) o single_set_bd_thm) (0 upto ilive - 1); + val Gbd_Fbd_Cinfinites = map single_bd_Cinfinite (0 upto length inners - 1) in @{map 3} (fn set'_eq_set => fn set_alt => fn single_set_bds => fn ctxt => - mk_comp_set_bd_tac ctxt set'_eq_set bd_ordIso_natLeq_thm_opt set_alt single_set_bds) + mk_comp_set_bd_tac ctxt set'_eq_set bd_ordIso_natLeq_thm_opt set_alt single_set_bds + Gbd_Fbd_Cinfinites) set'_eq_sets set_alt_thms single_set_bd_thmss end; @@ -371,7 +383,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 le_rel_OO_tac rel_OO_Grp_tac pred_set_tac; + bd_cinfinite_tac bd_regularCard_tac set_bd_tacs le_rel_OO_tac rel_OO_Grp_tac pred_set_tac; val outer_wits = mk_wits_of_bnf (replicate onwits oDs) (replicate onwits CAs) outer; @@ -454,6 +466,7 @@ val set_map0_tacs = map (fn thm => fn ctxt => rtac ctxt thm 1) (drop n (set_map0_of_bnf bnf)); fun bd_card_order_tac ctxt = rtac ctxt (bd_card_order_of_bnf bnf) 1; fun bd_cinfinite_tac ctxt = rtac ctxt (bd_cinfinite_of_bnf bnf) 1; + fun bd_regularCard_tac ctxt = rtac ctxt (bd_regularCard_of_bnf bnf) 1; val set_bd_tacs = map (fn thm => fn ctxt => rtac ctxt thm 1) (drop n (set_bd_of_bnf bnf)); val in_alt_thm = @@ -488,7 +501,7 @@ fun pred_set_tac ctxt = mk_simple_pred_set_tac ctxt (pred_set_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 le_rel_OO_tac rel_OO_Grp_tac pred_set_tac; + bd_cinfinite_tac bd_regularCard_tac set_bd_tacs le_rel_OO_tac rel_OO_Grp_tac pred_set_tac; val bnf_wits = mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf; @@ -563,11 +576,12 @@ map (fn thm => fn ctxt => rtac ctxt thm 1) (set_map0_of_bnf bnf); fun bd_card_order_tac ctxt = rtac ctxt (bd_card_order_of_bnf bnf) 1; fun bd_cinfinite_tac ctxt = rtac ctxt (bd_cinfinite_of_bnf bnf) 1; + fun bd_regularCard_tac ctxt = rtac ctxt (bd_regularCard_of_bnf bnf) 1; val set_bd_tacs = if Config.get lthy quick_and_dirty then replicate (n + live) (K all_tac) else - replicate n (fn ctxt => mk_lift_set_bd_tac ctxt (bd_Card_order_of_bnf bnf)) @ + replicate n (fn ctxt => mk_lift_set_bd_tac ctxt (bd_Cinfinite_of_bnf bnf)) @ (map (fn thm => fn ctxt => rtac ctxt thm 1) (set_bd_of_bnf bnf)); val in_alt_thm = @@ -587,7 +601,7 @@ fun pred_set_tac ctxt = mk_simple_pred_set_tac ctxt (pred_set_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 le_rel_OO_tac rel_OO_Grp_tac pred_set_tac; + bd_cinfinite_tac bd_regularCard_tac set_bd_tacs le_rel_OO_tac rel_OO_Grp_tac pred_set_tac; val wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf); @@ -655,6 +669,7 @@ val set_map0_tacs = permute (map (fn thm => fn ctxt => rtac ctxt thm 1) (set_map0_of_bnf bnf)); fun bd_card_order_tac ctxt = rtac ctxt (bd_card_order_of_bnf bnf) 1; fun bd_cinfinite_tac ctxt = rtac ctxt (bd_cinfinite_of_bnf bnf) 1; + fun bd_regularCard_tac ctxt = rtac ctxt (bd_regularCard_of_bnf bnf) 1; val set_bd_tacs = permute (map (fn thm => fn ctxt => rtac ctxt thm 1) (set_bd_of_bnf bnf)); val in_alt_thm = @@ -675,7 +690,7 @@ fun pred_set_tac ctxt = mk_simple_pred_set_tac ctxt (pred_set_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 le_rel_OO_tac rel_OO_Grp_tac pred_set_tac; + bd_cinfinite_tac bd_regularCard_tac set_bd_tacs le_rel_OO_tac rel_OO_Grp_tac pred_set_tac; val wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf); @@ -887,9 +902,9 @@ maybe_typedef false (bdT_bind, params, NoSyn) (HOLogic.mk_UNIV bd_repT) NONE (fn ctxt => EVERY' [rtac ctxt exI, rtac ctxt UNIV_I] 1) lthy; - val (bnf_bd', bd_ordIso, bd_card_order, bd_cinfinite) = + val (bnf_bd', bd_ordIso, bd_card_order, bd_cinfinite, bd_regularCard) = if bdT = bd_repT then (bnf_bd, bd_Card_order_of_bnf bnf RS @{thm ordIso_refl}, - bd_card_order_of_bnf bnf, bd_cinfinite_of_bnf bnf) + bd_card_order_of_bnf bnf, bd_cinfinite_of_bnf bnf, bd_regularCard_of_bnf bnf) else let val bnf_bd' = mk_dir_image bnf_bd (Const (Abs_bd_name, bd_repT --> bdT)); @@ -902,8 +917,10 @@ @{thm card_order_dir_image} OF [Abs_bdT_bij, bd_card_order_of_bnf bnf]; val bd_cinfinite = (@{thm Cinfinite_cong} OF [bd_ordIso, bd_Cinfinite_of_bnf bnf]) RS conjunct1; + val bd_regularCard = @{thm regularCard_ordIso} OF [bd_ordIso, bd_Cinfinite_of_bnf bnf, + bd_regularCard_of_bnf bnf]; in - (bnf_bd', bd_ordIso, bd_card_order, bd_cinfinite) + (bnf_bd', bd_ordIso, bd_card_order, bd_cinfinite, bd_regularCard) end; fun map_id0_tac ctxt = @@ -916,7 +933,7 @@ etac ctxt (o_apply RS equalityD2 RS set_mp)]) (1 upto live)) 1; fun set_map0_tac thm ctxt = rtac ctxt (@{thm type_copy_set_map0} OF [type_definition, thm]) 1; - val set_bd_tacs = map (fn thm => fn ctxt => rtac ctxt (@{thm ordLeq_ordIso_trans} OF + val set_bd_tacs = map (fn thm => fn ctxt => rtac ctxt (@{thm ordLess_ordIso_trans} OF [thm, bd_ordIso] RS @{thm type_copy_set_bd}) 1) (set_bd_of_bnf bnf); fun le_rel_OO_tac ctxt = rtac ctxt (le_rel_OO_of_bnf bnf RS @{thm vimage2p_relcompp_mono}) 1; @@ -936,7 +953,7 @@ val tacs = zip_axioms map_id0_tac map_comp0_tac map_cong0_tac (map set_map0_tac (set_map0_of_bnf bnf)) (fn ctxt => rtac ctxt bd_card_order 1) (fn ctxt => rtac ctxt bd_cinfinite 1) - set_bd_tacs le_rel_OO_tac rel_OO_Grp_tac pred_set_tac; + (fn ctxt => rtac ctxt bd_regularCard 1) set_bd_tacs le_rel_OO_tac rel_OO_Grp_tac pred_set_tac; val bnf_wits = map (fn (I, t) => fold Term.absdummy (map (nth As) I) diff -r 7a6301d01199 -r 22d1c5f2b9f4 src/HOL/Tools/BNF/bnf_comp_tactics.ML --- a/src/HOL/Tools/BNF/bnf_comp_tactics.ML Sat Jun 25 09:50:40 2022 +0000 +++ b/src/HOL/Tools/BNF/bnf_comp_tactics.ML Mon Jun 27 15:54:18 2022 +0200 @@ -10,12 +10,13 @@ sig val mk_comp_bd_card_order_tac: Proof.context -> thm list -> thm -> tactic val mk_comp_bd_cinfinite_tac: Proof.context -> thm -> thm -> tactic + val mk_comp_bd_regularCard_tac: Proof.context -> thm list -> thm -> thm list -> thm -> tactic val mk_comp_in_alt_tac: Proof.context -> thm list -> tactic val mk_comp_map_comp0_tac: Proof.context -> thm -> thm -> thm list -> tactic val mk_comp_map_cong0_tac: Proof.context -> thm list -> thm list -> thm -> thm list -> tactic val mk_comp_map_id0_tac: Proof.context -> thm -> thm -> thm list -> tactic val mk_comp_set_alt_tac: Proof.context -> thm -> tactic - val mk_comp_set_bd_tac: Proof.context -> thm -> thm option -> thm -> thm list -> tactic + val mk_comp_set_bd_tac: Proof.context -> thm -> thm option -> thm -> thm list -> thm list -> tactic val mk_comp_set_map0_tac: Proof.context -> thm -> thm -> thm -> thm -> thm list -> tactic val mk_comp_wit_tac: Proof.context -> thm list -> thm list -> thm -> thm list -> tactic @@ -126,25 +127,58 @@ rtac ctxt Fbd_cinfinite) THEN' rtac ctxt Gbd_cinfinite) 1; -fun mk_comp_set_bd_tac ctxt set'_eq_set bd_ordIso_natLeq_opt comp_set_alt Gset_Fset_bds = +fun mk_comp_bd_regularCard_tac ctxt Fbd_regularCards Gbd_regularCard Fbd_Cinfinites Gbd_Cinfinite = + rtac ctxt @{thm regularCard_natLeq} 1 ORELSE + EVERY1 [ + rtac ctxt @{thm regularCard_cprod}, + TRY o rtac ctxt @{thm Cinfinite_csum1}, + resolve_tac ctxt Fbd_Cinfinites, + rtac ctxt Gbd_Cinfinite, + REPEAT_DETERM o EVERY' [ + rtac ctxt @{thm regularCard_csum}, + resolve_tac ctxt Fbd_Cinfinites, + TRY o rtac ctxt @{thm Cinfinite_csum1}, + resolve_tac ctxt Fbd_Cinfinites, + resolve_tac ctxt Fbd_regularCards + ], + resolve_tac ctxt Fbd_regularCards, + rtac ctxt Gbd_regularCard + ]; + +fun mk_comp_set_bd_tac ctxt set'_eq_set bd_ordIso_natLeq_opt comp_set_alt Gset_Fset_bds Gbd_Fbd_Cinfinites = let val (bds, last_bd) = split_last Gset_Fset_bds; - fun gen_before bd = - rtac ctxt ctrans THEN' rtac ctxt @{thm Un_csum} THEN' - rtac ctxt ctrans THEN' rtac ctxt @{thm csum_mono} THEN' - rtac ctxt bd; - fun gen_after _ = rtac ctxt @{thm ordIso_imp_ordLeq} THEN' rtac ctxt @{thm cprod_csum_distrib1}; + fun gen_before bd = EVERY' [ + rtac ctxt @{thm ordLeq_ordLess_trans}, + rtac ctxt @{thm Un_csum}, + rtac ctxt @{thm csum_mono_strict}, + rtac ctxt @{thm card_of_Card_order}, + rtac ctxt @{thm card_of_Card_order}, + resolve_tac ctxt Gbd_Fbd_Cinfinites, + defer_tac, + rtac ctxt bd + ]; in (case bd_ordIso_natLeq_opt of - SOME thm => rtac ctxt (thm RSN (2, @{thm ordLeq_ordIso_trans})) 1 + SOME thm => rtac ctxt (thm RSN (2, @{thm ordLess_ordIso_trans})) 1 | NONE => all_tac) THEN unfold_thms_tac ctxt [set'_eq_set, comp_set_alt] THEN - rtac ctxt @{thm comp_set_bd_Union_o_collect} 1 THEN + rtac ctxt @{thm comp_set_bd_Union_o_collect_strict} 1 THEN unfold_thms_tac ctxt @{thms Union_image_insert Union_image_empty Union_Un_distrib o_apply} THEN - (rtac ctxt ctrans THEN' - WRAP' gen_before gen_after bds (rtac ctxt last_bd) THEN' - rtac ctxt @{thm ordIso_imp_ordLeq} THEN' - rtac ctxt @{thm cprod_com}) 1 + EVERY1 [ + rtac ctxt @{thm ordLess_ordLeq_trans}, + WRAP' gen_before (K (K all_tac)) bds (rtac ctxt last_bd), + rtac ctxt @{thm ordIso_imp_ordLeq}, + REPEAT_DETERM_N (length Gset_Fset_bds - 1) o EVERY' [ + rtac ctxt @{thm ordIso_transitive}, + REPEAT_DETERM o (rtac ctxt @{thm cprod_csum_distrib1} ORELSE' rtac ctxt @{thm csum_cong2}) + ], + rtac ctxt @{thm cprod_com}, + REPEAT_DETERM o EVERY' [ + TRY o rtac ctxt @{thm Cinfinite_csum1}, + resolve_tac ctxt Gbd_Fbd_Cinfinites + ] + ] end; val comp_in_alt_thms = @{thms o_apply collect_def image_insert image_empty Union_insert UN_insert @@ -204,8 +238,8 @@ fun empty_natural_tac ctxt = rtac ctxt @{thm empty_natural} 1; -fun mk_lift_set_bd_tac ctxt bd_Card_order = - (rtac ctxt @{thm Card_order_empty} THEN' rtac ctxt bd_Card_order) 1; +fun mk_lift_set_bd_tac ctxt bd_Cinfinite = + (rtac ctxt @{thm Cinfinite_gt_empty} THEN' rtac ctxt bd_Cinfinite) 1; fun lift_in_alt_tac ctxt = ((rtac ctxt @{thm Collect_cong} THEN' rtac ctxt iffI) 1 THEN diff -r 7a6301d01199 -r 22d1c5f2b9f4 src/HOL/Tools/BNF/bnf_def.ML --- a/src/HOL/Tools/BNF/bnf_def.ML Sat Jun 25 09:50:40 2022 +0000 +++ b/src/HOL/Tools/BNF/bnf_def.ML Mon Jun 27 15:54:18 2022 +0200 @@ -2,7 +2,8 @@ Author: Dmitriy Traytel, TU Muenchen Author: Jasmin Blanchette, TU Muenchen Author: Martin Desharnais, TU Muenchen - Copyright 2012, 2013, 2014 + Author: Jan van Brügge, TU Muenchen + Copyright 2012, 2013, 2014, 2022 Definition of bounded natural functors. *) @@ -57,6 +58,7 @@ val bd_Cnotzero_of_bnf: bnf -> thm val bd_card_order_of_bnf: bnf -> thm val bd_cinfinite_of_bnf: bnf -> thm + val bd_regularCard_of_bnf: bnf -> thm val collect_set_map_of_bnf: bnf -> thm val in_bd_of_bnf: bnf -> thm val in_cong_of_bnf: bnf -> thm @@ -135,7 +137,7 @@ val minimize_wits: (''a list * 'b) list -> (''a list * 'b) list val wits_of_bnf: bnf -> nonemptiness_witness list - val zip_axioms: 'a -> 'a -> 'a -> 'a list -> 'a -> 'a -> 'a list -> 'a -> 'a -> 'a -> 'a list + val zip_axioms: 'a -> 'a -> 'a -> 'a list -> 'a -> 'a -> 'a -> 'a list -> 'a -> 'a -> 'a -> 'a list datatype inline_policy = Dont_Inline | Hardly_Inline | Smart_Inline | Do_Inline datatype fact_policy = Dont_Note | Note_Some | Note_All @@ -198,15 +200,16 @@ set_map0: thm list, bd_card_order: thm, bd_cinfinite: thm, + bd_regularCard: thm, set_bd: thm list, le_rel_OO: thm, rel_OO_Grp: thm, pred_set: thm }; -fun mk_axioms' (((((((((id, comp), cong), map), c_o), cinf), set_bd), le_rel_OO), rel), pred) = +fun mk_axioms' ((((((((((id, comp), cong), map), c_o), cinf), creg), set_bd), le_rel_OO), rel), pred) = {map_id0 = id, map_comp0 = comp, map_cong0 = cong, set_map0 = map, bd_card_order = c_o, - bd_cinfinite = cinf, set_bd = set_bd, le_rel_OO = le_rel_OO, rel_OO_Grp = rel, pred_set = pred}; + bd_cinfinite = cinf, bd_regularCard = creg, set_bd = set_bd, le_rel_OO = le_rel_OO, rel_OO_Grp = rel, pred_set = pred}; fun dest_cons [] = raise List.Empty | dest_cons (x :: xs) = (x, xs); @@ -219,23 +222,25 @@ ||>> chop n ||>> dest_cons ||>> dest_cons + ||>> dest_cons ||>> chop n ||>> dest_cons ||>> dest_cons ||> the_single |> mk_axioms'; -fun zip_axioms mid mcomp mcong smap bdco bdinf sbd le_rel_OO rel pred = - [mid, mcomp, mcong] @ smap @ [bdco, bdinf] @ sbd @ [le_rel_OO, rel, pred]; +fun zip_axioms mid mcomp mcong smap bdco bdinf bdreg sbd le_rel_OO rel pred = + [mid, mcomp, mcong] @ smap @ [bdco, bdinf, bdreg] @ sbd @ [le_rel_OO, rel, pred]; -fun map_axioms f {map_id0, map_comp0, map_cong0, set_map0, bd_card_order, bd_cinfinite, set_bd, - le_rel_OO, rel_OO_Grp, pred_set} = +fun map_axioms f {map_id0, map_comp0, map_cong0, set_map0, bd_card_order, bd_cinfinite, + bd_regularCard, set_bd, le_rel_OO, rel_OO_Grp, pred_set} = {map_id0 = f map_id0, map_comp0 = f map_comp0, map_cong0 = f map_cong0, set_map0 = map f set_map0, bd_card_order = f bd_card_order, bd_cinfinite = f bd_cinfinite, + bd_regularCard = f bd_regularCard, set_bd = map f set_bd, le_rel_OO = f le_rel_OO, rel_OO_Grp = f rel_OO_Grp, @@ -576,6 +581,7 @@ val bd_Cnotzero_of_bnf = #bd_Cnotzero o #facts o rep_bnf; val bd_card_order_of_bnf = #bd_card_order o #axioms o rep_bnf; val bd_cinfinite_of_bnf = #bd_cinfinite o #axioms o rep_bnf; +val bd_regularCard_of_bnf = #bd_regularCard o #axioms o rep_bnf; val collect_set_map_of_bnf = Lazy.force o #collect_set_map o #facts o rep_bnf; val in_bd_of_bnf = Lazy.force o #in_bd o #facts o rep_bnf; val in_cong_of_bnf = Lazy.force o #in_cong o #facts o rep_bnf; @@ -835,6 +841,7 @@ val bd_CnotzeroN = "bd_Cnotzero"; val bd_card_orderN = "bd_card_order"; val bd_cinfiniteN = "bd_cinfinite"; +val bd_regularCardN = "bd_regularCard"; val collect_set_mapN = "collect_set_map"; val in_bdN = "in_bd"; val in_monoN = "in_mono"; @@ -912,6 +919,7 @@ val notes = [(bd_card_orderN, [#bd_card_order axioms]), (bd_cinfiniteN, [#bd_cinfinite axioms]), + (bd_regularCardN, [#bd_regularCard axioms]), (bd_Card_orderN, [#bd_Card_order facts]), (bd_CinfiniteN, [#bd_Cinfinite facts]), (bd_CnotzeroN, [#bd_Cnotzero facts]), @@ -1404,10 +1412,12 @@ val cinfinite_bd_goal = HOLogic.mk_Trueprop (mk_cinfinite bnf_bd_As); + val regularCard_bd_goal = HOLogic.mk_Trueprop (mk_regularCard bnf_bd_As); + val set_bds_goal = let fun mk_goal set = - Logic.all x (HOLogic.mk_Trueprop (mk_ordLeq (mk_card_of (set $ x)) bnf_bd_As)); + Logic.all x (HOLogic.mk_Trueprop (mk_ordLess (mk_card_of (set $ x)) bnf_bd_As)); in map mk_goal bnf_sets_As end; @@ -1427,7 +1437,7 @@ Term.list_comb (mk_pred_spec Ds As', Ps))); 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 le_rel_OO_goal rel_OO_Grp_goal pred_set_goal; + card_order_bd_goal cinfinite_bd_goal regularCard_bd_goal set_bds_goal le_rel_OO_goal rel_OO_Grp_goal pred_set_goal; val mk_wit_goals = mk_wit_goals bs zs bnf_sets_As; fun triv_wit_tac ctxt = mk_trivial_wit_tac ctxt bnf_wit_defs; @@ -1562,11 +1572,12 @@ val in_bd_goal = fold_rev Logic.all As (HOLogic.mk_Trueprop (mk_ordLeq (mk_card_of (mk_in As bnf_sets_As CA')) bd)); + val weak_set_bds = map (fn thm => @{thm ordLess_imp_ordLeq} OF [thm]) (#set_bd axioms); in Goal.prove_sorry lthy [] [] in_bd_goal (fn {context = ctxt, prems = _} => mk_in_bd_tac ctxt live surj_imp_ordLeq_inst (Lazy.force map_comp) (Lazy.force map_id) (#map_cong0 axioms) - (map Lazy.force set_map) (#set_bd axioms) (#bd_card_order axioms) + (map Lazy.force set_map) weak_set_bds (#bd_card_order axioms) bd_Card_order bd_Cinfinite bd_Cnotzero) |> Thm.close_derivation \<^here> end; @@ -2028,11 +2039,11 @@ val facts = mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_map in_bd in_cong in_mono in_rel inj_map inj_map_strong map_comp map_cong map_cong_simp map_cong_pred map_id - map_ident0 map_ident map_ident_strong map_transfer rel_eq rel_flip set_map rel_cong0 - rel_cong rel_cong_simp rel_map rel_mono rel_mono_strong0 rel_mono_strong set_transfer - rel_Grp rel_conversep rel_OO rel_refl rel_refl_strong rel_reflp rel_symp rel_transp - rel_transfer rel_eq_onp pred_transfer pred_True pred_map pred_rel pred_mono_strong0 - pred_mono_strong pred_mono pred_cong0 pred_cong pred_cong_simp; + map_ident0 map_ident map_ident_strong map_transfer rel_eq rel_flip set_map rel_cong0 rel_cong + rel_cong_simp rel_map rel_mono rel_mono_strong0 rel_mono_strong set_transfer rel_Grp rel_conversep + rel_OO rel_refl rel_refl_strong rel_reflp rel_symp rel_transp rel_transfer rel_eq_onp + pred_transfer pred_True pred_map pred_rel pred_mono_strong0 pred_mono_strong pred_mono + pred_cong0 pred_cong pred_cong_simp; val wits = map2 mk_witness bnf_wits wit_thms; diff -r 7a6301d01199 -r 22d1c5f2b9f4 src/HOL/Tools/BNF/bnf_fp_util.ML --- a/src/HOL/Tools/BNF/bnf_fp_util.ML Sat Jun 25 09:50:40 2022 +0000 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Mon Jun 27 15:54:18 2022 +0200 @@ -188,6 +188,7 @@ val mk_sum_Cinfinite: thm list -> thm val mk_sum_card_order: thm list -> thm + val mk_sum_Cinfinite_regularCard: (thm * thm) list -> thm * thm val force_typ: Proof.context -> typ -> term -> term @@ -548,6 +549,14 @@ fun mk_sum_card_order [thm] = thm | mk_sum_card_order (thm :: thms) = @{thm card_order_csum} OF [thm, mk_sum_card_order thms]; +fun mk_sum_Cinfinite_regularCard [x] = x + | mk_sum_Cinfinite_regularCard ((cinf, thm) :: thms) = + let val (cinf_sum, thm_sum) = mk_sum_Cinfinite_regularCard thms + in ( + @{thm Cinfinite_csum_weak} OF [cinf, cinf_sum], + @{thm regularCard_csum} OF [cinf, cinf_sum, thm, thm_sum] + ) end; + fun mk_xtor_rel_co_induct_thm fp pre_rels pre_phis rels phis xs ys xtors xtor's tac lthy = let val pre_relphis = map (fn rel => Term.list_comb (rel, phis @ pre_phis)) pre_rels; diff -r 7a6301d01199 -r 22d1c5f2b9f4 src/HOL/Tools/BNF/bnf_gfp.ML --- a/src/HOL/Tools/BNF/bnf_gfp.ML Sat Jun 25 09:50:40 2022 +0000 +++ b/src/HOL/Tools/BNF/bnf_gfp.ML Mon Jun 27 15:54:18 2022 +0200 @@ -2,7 +2,8 @@ Author: Dmitriy Traytel, TU Muenchen Author: Andrei Popescu, TU Muenchen Author: Jasmin Blanchette, TU Muenchen - Copyright 2012 + Author: Jan van Brügge, TU Muenchen + Copyright 2012, 2022 Codatatype construction. *) @@ -181,6 +182,7 @@ val bd_Card_order = hd bd_Card_orders; val bd_Cinfinites = map bd_Cinfinite_of_bnf bnfs; val bd_Cinfinite = hd bd_Cinfinites; + val bd_regularCards = map bd_regularCard_of_bnf bnfs; val in_monos = map in_mono_of_bnf bnfs; val map_comp0s = map map_comp0_of_bnf bnfs; val sym_map_comps = map mk_sym map_comp0s; @@ -745,8 +747,7 @@ (* bounds *) - val (lthy, sbd, sbdT, - sbd_card_order, sbd_Cinfinite, sbd_Card_order, set_sbdss) = + val (lthy, sbd', sbdT', sbd_card_order', sbd_Cinfinite', sbd_Card_order', set_sbdss') = if n = 1 then (lthy, sum_bd, sum_bdT, bd_card_order, bd_Cinfinite, bd_Card_order, set_bdss) else @@ -785,19 +786,30 @@ val sum_card_order = mk_sum_card_order bd_card_orders; val sbd_ordIso = @{thm ssubst_Pair_rhs} OF - [@{thm dir_image} OF [Abs_sbdT_inj, sum_Card_order], sbd_def]; + [@{thm dir_image} OF [Abs_sbdT_inj, sum_Card_order], + sbd_def + ]; val sbd_card_order = @{thm iffD2[OF arg_cong[of _ _ card_order]]} OF [sbd_def, @{thm card_order_dir_image} OF [Abs_sbdT_bij, sum_card_order]]; val sbd_Cinfinite = @{thm Cinfinite_cong} OF [sbd_ordIso, sum_Cinfinite]; - val sbd_Card_order = sbd_Cinfinite RS conjunct2; + val sbd_Card_order = conjunct2 OF [sbd_Cinfinite]; fun mk_set_sbd i bd_Card_order bds = - map (fn thm => @{thm ordLeq_ordIso_trans} OF - [bd_Card_order RS mk_ordLeq_csum n i thm, sbd_ordIso]) bds; + map (fn thm => @{thm ordLess_ordIso_trans} OF + [mk_ordLess_csum n i thm OF [bd_Card_order], sbd_ordIso]) bds; val set_sbdss = @{map 3} mk_set_sbd ks bd_Card_orders set_bdss; in (lthy, sbd, sbdT, sbd_card_order, sbd_Cinfinite, sbd_Card_order, set_sbdss) end; + val sbd = mk_card_suc sbd'; + val sbdT = fst (dest_relT (fastype_of sbd)); + val sbd_card_order = @{thm card_order_card_suc} OF [sbd_card_order']; + val sbd_Cinfinite = @{thm Cinfinite_card_suc} OF [sbd_Cinfinite', sbd_card_order']; + val sbd_Card_order = @{thm Card_order_card_suc} OF [sbd_card_order']; + val sbd_regularCard = @{thm regular_card_suc} OF [sbd_card_order', sbd_Cinfinite']; + val set_sbdss = map (map (fn thm => @{thm ordLess_transitive} OF [ + thm, @{thm card_suc_greater} OF [sbd_card_order'] + ])) set_sbdss'; val sbdTs = replicate n sbdT; val sum_sbdT = mk_sumTN sbdTs; @@ -978,7 +990,7 @@ mk_fromCard (nth (nth setssAs (i - 1)) (m + i' - 1) $ (s $ x)) sbd; fun mk_to_sbd_thmss thm = map (map (fn set_sbd => - thm OF [set_sbd, sbd_Card_order]) o drop m) set_sbdss; + thm OF [@{thm ordLess_imp_ordLeq} OF [set_sbd], sbd_Card_order]) o drop m) set_sbdss; val to_sbd_inj_thmss = mk_to_sbd_thmss @{thm toCard_inj}; val from_to_sbd_thmss = mk_to_sbd_thmss @{thm fromCard_toCard}; @@ -2075,7 +2087,7 @@ val col_bd_thmss = let - fun mk_col_bd z col bd = mk_ordLeq (mk_card_of (col $ z)) bd; + fun mk_col_bd z col bd = mk_ordLess (mk_card_of (col $ z)) bd; fun mk_goal bds cols = list_all_free Jzs (Library.foldr1 HOLogic.mk_conj (@{map 3} mk_col_bd Jzs cols bds)); @@ -2090,7 +2102,7 @@ Variable.add_free_names lthy goal [] |> (fn vars => Goal.prove_sorry lthy vars [] (HOLogic.mk_Trueprop goal) (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jbd_defs THEN - mk_col_bd_tac ctxt m j cts rec_0s rec_Sucs sbd_Card_order sbd_Cinfinite set_sbdss)) + mk_col_bd_tac ctxt m j cts rec_0s rec_Sucs sbd_regularCard sbd_Cinfinite set_sbdss)) |> Thm.close_derivation \<^here>) ls goals ctss col_0ss' col_Sucss'; in @@ -2468,14 +2480,20 @@ val Jbd_card_orders = map (fn def => Local_Defs.fold lthy [def] sbd_card_order) Jbd_defs; val Jbd_Cinfinites = map (fn def => Local_Defs.fold lthy [def] sbd_Cinfinite) Jbd_defs; + val Jbd_regularCards = map (fn def => Local_Defs.fold lthy [def] sbd_regularCard) Jbd_defs; + + val Jbd_natLeq_ordLess_thms = map (fn def => @{thm natLeq_ordLess_cinfinite'} OF [ + sbd_Cinfinite', sbd_card_order', def + ]) Jbd_defs; val bd_co_tacs = map (fn thm => fn ctxt => rtac ctxt thm 1) Jbd_card_orders; val bd_cinf_tacs = map (fn thm => fn ctxt => rtac ctxt (thm RS conjunct1) 1) Jbd_Cinfinites; + val bd_reg_tacs = map (fn thm => fn ctxt => rtac ctxt thm 1) Jbd_regularCards; val set_bd_tacss = - map2 (fn Cinf => map (fn col => fn ctxt => - unfold_thms_tac ctxt Jset_defs THEN mk_set_bd_tac ctxt Cinf col)) - Jbd_Cinfinites (transpose col_bd_thmss); + @{map 4} (fn Cinf => fn Creg => fn thm => map (fn col => fn ctxt => + unfold_thms_tac ctxt Jset_defs THEN mk_set_bd_tac ctxt Cinf Creg thm col)) + Jbd_Cinfinites Jbd_regularCards Jbd_natLeq_ordLess_thms (transpose col_bd_thmss); val le_rel_OO_tacs = map (fn i => fn ctxt => rtac ctxt (le_Jrel_OO_thm RS mk_conjunctN n i) 1) ks; @@ -2484,8 +2502,8 @@ val pred_set_tacs = map (fn def => fn ctxt => rtac ctxt def 1) Jpred_unabs_defs; - val tacss = @{map 10} 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 pred_set_tacs; + val tacss = @{map 11} zip_axioms map_id0_tacs map_comp0_tacs map_cong0_tacs set_map0_tacss + bd_co_tacs bd_cinf_tacs bd_reg_tacs set_bd_tacss le_rel_OO_tacs rel_OO_Grp_tacs pred_set_tacs; fun wit_tac thms ctxt = mk_wit_tac ctxt n dtor_ctor_thms (flat dtor_Jset_thmss) (maps wit_thms_of_bnf bnfs) thms; diff -r 7a6301d01199 -r 22d1c5f2b9f4 src/HOL/Tools/BNF/bnf_gfp_tactics.ML --- a/src/HOL/Tools/BNF/bnf_gfp_tactics.ML Sat Jun 25 09:50:40 2022 +0000 +++ b/src/HOL/Tools/BNF/bnf_gfp_tactics.ML Mon Jun 27 15:54:18 2022 +0200 @@ -76,7 +76,7 @@ val mk_sbis_lsbis_tac: Proof.context -> thm list -> thm -> thm -> tactic val mk_set_Lev_tac: Proof.context -> cterm option list -> thm list -> thm list -> thm list -> thm list -> thm list list -> tactic - val mk_set_bd_tac: Proof.context -> thm -> thm -> tactic + val mk_set_bd_tac: Proof.context -> thm -> thm -> thm -> thm -> tactic val mk_set_Jset_incl_Jset_tac: Proof.context -> int -> 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 @@ -881,28 +881,31 @@ EVERY' (map (rtac ctxt) [@{thm ext}, o_apply RS trans, sym, o_apply RS trans, @{thm image_UN} RS trans, refl RS @{thm SUP_cong}, col_natural]) 1; -fun mk_col_bd_tac ctxt m j cts rec_0s rec_Sucs sbd_Card_order sbd_Cinfinite set_sbdss = +fun mk_col_bd_tac ctxt m j cts rec_0s rec_Sucs sbd_regularCard sbd_Cinfinite set_sbdss = let val n = length rec_0s; in EVERY' [rtac ctxt (Thm.instantiate' [] cts nat_induct), REPEAT_DETERM o rtac ctxt allI, - CONJ_WRAP' (fn rec_0 => EVERY' (map (rtac ctxt) [ordIso_ordLeq_trans, - @{thm card_of_ordIso_subst}, rec_0, @{thm Card_order_empty}, sbd_Card_order])) rec_0s, + CONJ_WRAP' (fn rec_0 => EVERY' (map (rtac ctxt) [@{thm ordIso_ordLess_trans}, + @{thm card_of_ordIso_subst}, rec_0, @{thm Cinfinite_gt_empty}, sbd_Cinfinite])) rec_0s, REPEAT_DETERM o rtac ctxt allI, CONJ_WRAP' (fn (rec_Suc, set_sbds) => EVERY' - [rtac ctxt ordIso_ordLeq_trans, rtac ctxt @{thm card_of_ordIso_subst}, rtac ctxt rec_Suc, - rtac ctxt (sbd_Cinfinite RSN (3, @{thm Un_Cinfinite_bound})), rtac ctxt (nth set_sbds (j - 1)), - REPEAT_DETERM_N (n - 1) o rtac ctxt (sbd_Cinfinite RSN (3, @{thm Un_Cinfinite_bound})), - EVERY' (map2 (fn i => fn set_sbd => EVERY' [rtac ctxt @{thm UNION_Cinfinite_bound}, - rtac ctxt set_sbd, rtac ctxt ballI, REPEAT_DETERM o etac ctxt allE, - etac ctxt (mk_conjunctN n i), rtac ctxt sbd_Cinfinite]) (1 upto n) (drop m set_sbds))]) + [rtac ctxt @{thm ordIso_ordLess_trans}, rtac ctxt @{thm card_of_ordIso_subst}, + rtac ctxt rec_Suc, rtac ctxt (sbd_Cinfinite RSN (3, @{thm Un_Cinfinite_bound_strict})), + rtac ctxt (nth set_sbds (j - 1)), + REPEAT_DETERM_N (n - 1) o rtac ctxt (sbd_Cinfinite RSN (3, @{thm Un_Cinfinite_bound_strict})), + EVERY' (map2 (fn i => fn set_sbd => EVERY' [ + rtac ctxt (@{thm card_of_UNION_ordLess_infinite_Field_regularCard} OF [sbd_regularCard, + sbd_Cinfinite]), rtac ctxt set_sbd, rtac ctxt ballI, REPEAT_DETERM o etac ctxt allE, + etac ctxt (mk_conjunctN n i)]) (1 upto n) (drop m set_sbds))]) (rec_Sucs ~~ set_sbdss)] 1 end; -fun mk_set_bd_tac ctxt sbd_Cinfinite col_bd = - EVERY' (map (rtac ctxt) [@{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_set_bd_tac ctxt sbd_Cinfinite sbd_regularCard natLeq_ordLess_bd col_bd = + EVERY' (map (rtac ctxt) [@{thm card_of_UNION_ordLess_infinite_Field_regularCard} OF [ + sbd_regularCard, sbd_Cinfinite], @{thm ordIso_ordLess_trans}, @{thm card_of_nat}, + natLeq_ordLess_bd, ballI, col_bd]) 1; fun mk_le_rel_OO_tac ctxt coinduct rel_Jrels le_rel_OOs = EVERY' (rtac ctxt coinduct :: map2 (fn rel_Jrel => fn le_rel_OO => diff -r 7a6301d01199 -r 22d1c5f2b9f4 src/HOL/Tools/BNF/bnf_gfp_util.ML --- a/src/HOL/Tools/BNF/bnf_gfp_util.ML Sat Jun 25 09:50:40 2022 +0000 +++ b/src/HOL/Tools/BNF/bnf_gfp_util.ML Mon Jun 27 15:54:18 2022 +0200 @@ -1,6 +1,7 @@ (* Title: HOL/Tools/BNF/bnf_gfp_util.ML Author: Dmitriy Traytel, TU Muenchen - Copyright 2012 + Author: Jan van Brügge, TU Muenchen + Copyright 2012, 2022 Library for the codatatype construction. *) @@ -31,6 +32,7 @@ val mk_toCard: term -> term -> term val mk_undefined: typ -> term val mk_univ: term -> term + val mk_card_suc: term -> term val mk_specN: int -> thm -> thm @@ -141,6 +143,12 @@ fun mk_undefined T = Const (\<^const_name>\undefined\, T); +fun mk_card_suc t = + let + val T = fst (dest_relT (fastype_of t)) + val T' = Type (\<^type_name>\suc\, [T]) + in Const (\<^const_name>\card_suc\, mk_relT (T, T) --> mk_relT (T', T')) $ t end; + fun mk_rec_nat Zero Suc = let val T = fastype_of Zero; in Const (\<^const_name>\old.rec_nat\, T --> fastype_of Suc --> HOLogic.natT --> T) $ Zero $ Suc end; diff -r 7a6301d01199 -r 22d1c5f2b9f4 src/HOL/Tools/BNF/bnf_lfp.ML --- a/src/HOL/Tools/BNF/bnf_lfp.ML Sat Jun 25 09:50:40 2022 +0000 +++ b/src/HOL/Tools/BNF/bnf_lfp.ML Mon Jun 27 15:54:18 2022 +0200 @@ -1,7 +1,8 @@ (* Title: HOL/Tools/BNF/bnf_lfp.ML Author: Dmitriy Traytel, TU Muenchen Author: Andrei Popescu, TU Muenchen - Copyright 2012 + Author: Jan van Brügge, TU Muenchen + Copyright 2012, 2022 Datatype construction. *) @@ -133,6 +134,7 @@ val bd0_card_orders = map bd_card_order_of_bnf bnfs; val bd0_Card_orders = map bd_Card_order_of_bnf bnfs; val bd0_Cinfinites = map bd_Cinfinite_of_bnf bnfs; + val bd0_regularCards = map bd_regularCard_of_bnf bnfs; val set_bd0ss = map set_bd_of_bnf bnfs; val bd_Card_order = @{thm Card_order_csum}; @@ -142,7 +144,7 @@ val bd_Cinfinite = hd bd_Cinfinites; val set_bdss = map2 (fn set_bd0s => fn bd0_Card_order => - map (fn thm => ctrans OF [thm, bd0_Card_order RS @{thm ordLeq_csum1}]) set_bd0s) + map (fn thm => @{thm ordLess_ordLeq_trans} OF [thm, bd0_Card_order RS @{thm ordLeq_csum1}]) set_bd0s) set_bd0ss bd0_Card_orders; val in_bds = map in_bd_of_bnf bnfs; val sym_map_comps = map (fn bnf => map_comp0_of_bnf bnf RS sym) bnfs; @@ -491,8 +493,8 @@ val sbd_Card_order = sbd_Cinfinite RS conjunct2; fun mk_set_sbd i bd_Card_order bds = - map (fn thm => @{thm ordLeq_ordIso_trans} OF - [bd_Card_order RS mk_ordLeq_csum n i thm, sbd_ordIso]) bds; + map (fn thm => @{thm ordLess_ordIso_trans} OF + [bd_Card_order RS mk_ordLess_csum n i thm, sbd_ordIso]) bds; val set_sbdss = @{map 3} mk_set_sbd ks bd_Card_orders set_bdss; fun mk_in_bd_sum i Co Cnz bd = @@ -690,6 +692,7 @@ val (alg_min_alg_thm, card_of_min_alg_thms, least_min_alg_thms, mor_incl_min_alg_thm) = let + val set_sbdss_weak = map (map (fn thm => @{thm ordLess_imp_ordLeq} OF [thm])) set_sbdss; val alg_min_alg = let val goal = HOLogic.mk_Trueprop (mk_alg min_algs ss); @@ -697,7 +700,7 @@ in Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} => mk_alg_min_alg_tac ctxt m alg_def min_alg_defs - suc_bd_limit_thm sbd_Cinfinite set_sbdss min_algs_thms min_algs_mono_thms) + suc_bd_limit_thm sbd_Cinfinite set_sbdss_weak min_algs_thms min_algs_mono_thms) |> Thm.close_derivation \<^here> end; @@ -1372,9 +1375,9 @@ ctors (0 upto n - 1) witss end; - val (lthy, sbd0, sbd0_card_order, sbd0_Cinfinite, set_sbd0ss) = + val (lthy, sbd0, sbd0_card_order, sbd0_Cinfinite, sbd0_regularCard, set_sbd0ss) = if n = 1 - then (lthy, hd bd0s, hd bd0_card_orders, hd bd0_Cinfinites, set_bd0ss) + then (lthy, hd bd0s, hd bd0_card_orders, hd bd0_Cinfinites, hd bd0_regularCards, set_bd0ss) else let val sum_bd0 = Library.foldr1 (uncurry mk_csum) bd0s; @@ -1411,7 +1414,8 @@ val Abs_sbd0T_inj = mk_Abs_inj_thm (#Abs_inject sbd0T_loc_info); val Abs_sbd0T_bij = mk_Abs_bij_thm lthy Abs_sbd0T_inj (#Abs_cases sbd0T_loc_info); - val sum_Cinfinite = mk_sum_Cinfinite bd0_Cinfinites; + val (sum_Cinfinite, sum_regularCard) = + mk_sum_Cinfinite_regularCard (bd0_Cinfinites ~~ bd0_regularCards); val sum_Card_order = sum_Cinfinite RS conjunct2; val sum_card_order = mk_sum_card_order bd0_card_orders; @@ -1422,12 +1426,15 @@ val sbd0_card_order = @{thm iffD2[OF arg_cong[of _ _ card_order]]} OF [sbd0_def, @{thm card_order_dir_image} OF [Abs_sbd0T_bij, sum_card_order]]; + val sbd0_regularCard = @{thm regularCard_ordIso} OF + [sbd0_ordIso, sum_Cinfinite, sum_regularCard]; + fun mk_set_sbd0 i bd0_Card_order bd0s = - map (fn thm => @{thm ordLeq_ordIso_trans} OF - [bd0_Card_order RS mk_ordLeq_csum n i thm, sbd0_ordIso]) bd0s; + map (fn thm => @{thm ordLess_ordIso_trans} OF + [bd0_Card_order RS mk_ordLess_csum n i thm, sbd0_ordIso]) bd0s; val set_sbd0ss = @{map 3} mk_set_sbd0 ks bd0_Card_orders set_bd0ss; in - (lthy, sbd0, sbd0_card_order, sbd0_Cinfinite, set_sbd0ss) + (lthy, sbd0, sbd0_card_order, sbd0_Cinfinite, sbd0_regularCard, set_sbd0ss) end; val (Ibnf_consts, lthy) = @@ -1605,7 +1612,7 @@ val Iset_bd_thmss = let - fun mk_set_bd z bd set = mk_ordLeq (mk_card_of (set $ z)) bd; + fun mk_set_bd z bd set = mk_ordLess (mk_card_of (set $ z)) bd; fun mk_cphi z set = Thm.cterm_of lthy (Term.absfree (dest_Free z) (mk_set_bd z sbd0 set)); @@ -1619,7 +1626,8 @@ HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (@{map 3} mk_set_bd Izs Ibds sets))) Isetss_by_range; - fun mk_tac ctxt induct = mk_set_bd_tac ctxt m (rtac ctxt induct) sbd0_Cinfinite set_sbd0ss; + fun mk_tac ctxt induct = mk_set_bd_tac ctxt m (rtac ctxt induct) sbd0_Cinfinite + sbd0_regularCard set_sbd0ss; val thms = @{map 4} (fn goal => fn ctor_sets => fn induct => fn i => Variable.add_free_names lthy goal [] @@ -1736,6 +1744,8 @@ unfold_thms_tac ctxt Ibd_defs THEN rtac ctxt sbd0_card_order 1); val bd_cinf_tacs = replicate n (fn ctxt => unfold_thms_tac ctxt Ibd_defs THEN rtac ctxt (sbd0_Cinfinite RS conjunct1) 1); + val bd_reg_tacs = replicate n (fn ctxt => + unfold_thms_tac ctxt Ibd_defs THEN rtac ctxt sbd0_regularCard 1); val set_bd_tacss = map (map (fn thm => fn ctxt => rtac ctxt thm 1)) (transpose Iset_bd_thmss); val le_rel_OO_tacs = map (fn i => fn ctxt => (rtac ctxt @{thm predicate2I} THEN' etac ctxt (le_Irel_OO_thm RS mk_conjunctN n i RS mp)) 1) ks; @@ -1744,8 +1754,8 @@ val pred_set_tacs = map (fn def => fn ctxt => rtac ctxt def 1) Ipred_unabs_defs; - val tacss = @{map 10} 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 pred_set_tacs; + val tacss = @{map 11} zip_axioms map_id0_tacs map_comp0_tacs map_cong0_tacs set_map0_tacss + bd_co_tacs bd_cinf_tacs bd_reg_tacs set_bd_tacss le_rel_OO_tacs rel_OO_Grp_tacs pred_set_tacs; fun wit_tac ctxt = unfold_thms_tac ctxt (flat Iwit_defss) THEN mk_wit_tac ctxt n (flat ctor_Iset_thmss) (maps wit_thms_of_bnf bnfs); diff -r 7a6301d01199 -r 22d1c5f2b9f4 src/HOL/Tools/BNF/bnf_lfp_tactics.ML --- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML Sat Jun 25 09:50:40 2022 +0000 +++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML Mon Jun 27 15:54:18 2022 +0200 @@ -1,7 +1,8 @@ (* Title: HOL/Tools/BNF/bnf_lfp_tactics.ML Author: Dmitriy Traytel, TU Muenchen Author: Andrei Popescu, TU Muenchen - Copyright 2012 + Author: Jan van Brügge, TU Muenchen + Copyright 2012, 2022 Tactics for the datatype construction. *) @@ -65,8 +66,8 @@ thm list -> tactic val mk_rec_tac: Proof.context -> thm list -> thm -> thm list -> tactic val mk_rec_unique_mor_tac: Proof.context -> thm list -> thm list -> thm -> tactic - val mk_set_bd_tac: Proof.context -> int -> (int -> tactic) -> thm -> thm list list -> thm list -> - int -> tactic + val mk_set_bd_tac: Proof.context -> int -> (int -> tactic) -> thm -> thm -> thm list list -> + thm list -> int -> tactic val mk_set_nat_tac: Proof.context -> int -> (int -> tactic) -> thm list list -> thm list -> cterm list -> thm list -> int -> tactic val mk_set_map0_tac: Proof.context -> thm -> tactic @@ -563,17 +564,22 @@ (induct_tac THEN' EVERY' (@{map 4} mk_set_nat csets ctor_maps ctor_sets set_mapss)) 1 end; -fun mk_set_bd_tac ctxt m induct_tac bd_Cinfinite set_bdss ctor_sets i = +fun mk_set_bd_tac ctxt m induct_tac bd_Cinfinite bd_regularCard set_bdss ctor_sets i = let val n = length ctor_sets; - fun useIH set_bd = EVERY' [rtac ctxt @{thm UNION_Cinfinite_bound}, rtac ctxt set_bd, rtac ctxt ballI, - Goal.assume_rule_tac ctxt, rtac ctxt bd_Cinfinite]; + fun useIH set_bd = EVERY' [ + rtac ctxt (@{thm card_of_UNION_ordLess_infinite_Field_regularCard} OF [ + bd_regularCard, bd_Cinfinite, set_bd + ]), + rtac ctxt ballI, + Goal.assume_rule_tac ctxt + ]; fun mk_set_nat ctor_set set_bds = - EVERY' [rtac ctxt @{thm ordIso_ordLeq_trans}, rtac ctxt @{thm card_of_ordIso_subst}, rtac ctxt ctor_set, - rtac ctxt (bd_Cinfinite RSN (3, @{thm Un_Cinfinite_bound})), rtac ctxt (nth set_bds (i - 1)), - REPEAT_DETERM_N (n - 1) o rtac ctxt (bd_Cinfinite RSN (3, @{thm Un_Cinfinite_bound})), + EVERY' [rtac ctxt @{thm ordIso_ordLess_trans}, rtac ctxt @{thm card_of_ordIso_subst}, rtac ctxt ctor_set, + rtac ctxt (bd_Cinfinite RSN (3, @{thm Un_Cinfinite_bound_strict})), rtac ctxt (nth set_bds (i - 1)), + REPEAT_DETERM_N (n - 1) o rtac ctxt (bd_Cinfinite RSN (3, @{thm Un_Cinfinite_bound_strict})), EVERY' (map useIH (drop m set_bds))]; in (induct_tac THEN' EVERY' (map2 mk_set_nat ctor_sets set_bdss)) 1 diff -r 7a6301d01199 -r 22d1c5f2b9f4 src/HOL/Tools/BNF/bnf_lift.ML --- a/src/HOL/Tools/BNF/bnf_lift.ML Sat Jun 25 09:50:40 2022 +0000 +++ b/src/HOL/Tools/BNF/bnf_lift.ML Mon Jun 27 15:54:18 2022 +0200 @@ -614,6 +614,8 @@ fun cinfinite_bd_tac ctxt = HEADGOAL (rtac ctxt (bd_cinfinite_of_bnf bnf_F)); + fun regularCard_bd_tac ctxt = HEADGOAL (rtac ctxt (bd_regularCard_of_bnf bnf_F)); + val set_bds_tac = map (fn set_bd => fn ctxt => HEADGOAL (EVERY' [SELECT_GOAL (unfold_thms_tac ctxt [o_apply]), rtac ctxt set_bd])) @@ -670,7 +672,7 @@ wit_thms)); val tactics = [map_id0_tac, map_comp0_tac, map_cong0_tac] @ set_map0s_tac @ - [card_order_bd_tac, cinfinite_bd_tac] @ set_bds_tac @ + [card_order_bd_tac, cinfinite_bd_tac, regularCard_bd_tac] @ set_bds_tac @ [le_rel_OO_tac, rel_OO_Grp_tac, pred_set_tac]; val (bnf_G, lthy) = bnf_def Dont_Inline (user_policy Note_Some) true I @@ -1105,6 +1107,7 @@ (* auxiliary lemmas *) val bd_card_order = bd_card_order_of_bnf bnf_F; val bd_cinfinite = bd_cinfinite_of_bnf bnf_F; + val bd_regularCard = bd_regularCard_of_bnf bnf_F; val in_rel = in_rel_of_bnf bnf_F; val map_F_comp = map_comp_of_bnf bnf_F; val map_F_comp0 = map_comp0_of_bnf bnf_F; @@ -1798,11 +1801,14 @@ (* bd_cinfinite: BNF_Cardinal_Arithmetic.cinfinite bd_F *) fun bd_cinfinite_tac ctxt = HEADGOAL (rtac ctxt bd_cinfinite); - (*target: ordLeq3 (card_of (set_F' (rep_G x_))) bd_F*) + (* bd_regularCard: regularCard bd_F *) + fun bd_regularCard_tac ctxt = HEADGOAL (rtac ctxt bd_regularCard); + + (*target: ordLess2 (card_of (set_F' (rep_G x_))) bd_F*) fun mk_set_G_bd_tac thms set_bd_thm ctxt = EVERY [Local_Defs.fold_tac ctxt [#set_F'_def thms], unfold_thms_tac ctxt [o_apply], - HEADGOAL (rtac ctxt (@{thm ordLeq_transitive} OF + HEADGOAL (rtac ctxt (@{thm ordLeq_ordLess_trans} OF [@{thm card_of_mono1} OF [#set_F'_subset thms], set_bd_thm]))]; (* rel_compp: rel_G R OO rel_G S \ rel_G (R OO S) *) @@ -1859,7 +1865,7 @@ val tactics = map_G_id0_tac :: map_G_comp0_tac :: map_G_cong_tac :: map mk_set_G_map0_G_tac set_F'_thmss @ - bd_card_order_tac :: bd_cinfinite_tac :: + bd_card_order_tac :: bd_cinfinite_tac :: bd_regularCard_tac :: map2 mk_set_G_bd_tac set_F'_thmss set_bd_thms @ rel_compp_tac :: rel_compp_Grp_tac :: [pred_G_set_G_tac]; diff -r 7a6301d01199 -r 22d1c5f2b9f4 src/HOL/Tools/BNF/bnf_util.ML --- a/src/HOL/Tools/BNF/bnf_util.ML Sat Jun 25 09:50:40 2022 +0000 +++ b/src/HOL/Tools/BNF/bnf_util.ML Mon Jun 27 15:54:18 2022 +0200 @@ -53,6 +53,7 @@ val mk_card_order: term -> term val mk_cexp: term -> term -> term val mk_cinfinite: term -> term + val mk_regularCard: term -> term val mk_collect: term list -> typ -> term val mk_converse: term -> term val mk_conversep: term -> term @@ -66,6 +67,7 @@ val mk_inj: term -> term val mk_leq: term -> term -> term val mk_ordLeq: term -> term -> term + val mk_ordLess: term -> term -> term val mk_rel_comp: term * term -> term val mk_rel_compp: term * term -> term val mk_vimage2p: term -> term -> term @@ -95,6 +97,7 @@ val mk_nthI: int -> int -> thm val mk_nth_conv: int -> int -> thm val mk_ordLeq_csum: int -> int -> thm -> thm + val mk_ordLess_csum: int -> int -> thm -> thm val mk_pointful: Proof.context -> thm -> thm val mk_rel_funDN: int -> thm -> thm val mk_rel_funDN_rotated: int -> thm -> thm @@ -313,10 +316,16 @@ fun mk_cinfinite bd = Const (\<^const_name>\cinfinite\, fastype_of bd --> HOLogic.boolT) $ bd; +fun mk_regularCard bd = Const (\<^const_name>\regularCard\, fastype_of bd --> HOLogic.boolT) $ bd; + fun mk_ordLeq t1 t2 = HOLogic.mk_mem (HOLogic.mk_prod (t1, t2), Const (\<^const_name>\ordLeq\, mk_relT (fastype_of t1, fastype_of t2))); +fun mk_ordLess t1 t2 = + HOLogic.mk_mem (HOLogic.mk_prod (t1, t2), + Const (\<^const_name>\ordLess\, mk_relT (fastype_of t1, fastype_of t2))); + fun mk_card_of A = let val AT = fastype_of A; @@ -439,6 +448,12 @@ | mk_ordLeq_csum n m thm = @{thm ordLeq_transitive} OF [mk_ordLeq_csum (n - 1) (m - 1) thm, @{thm ordLeq_csum2[OF Card_order_csum]}]; +fun mk_ordLess_csum 1 1 thm = thm + | mk_ordLess_csum _ 1 thm = @{thm ordLess_ordLeq_trans} OF [thm, @{thm ordLeq_csum1}] + | mk_ordLess_csum 2 2 thm = @{thm ordLess_ordLeq_trans} OF [thm, @{thm ordLeq_csum2}] + | mk_ordLess_csum n m thm = @{thm ordLess_ordLeq_trans} OF + [mk_ordLess_csum (n - 1) (m - 1) thm, @{thm ordLeq_csum2[OF Card_order_csum]}]; + fun mk_rel_funDN n = funpow n (fn thm => thm RS rel_funD); val mk_rel_funDN_rotated = rotate_prems ~1 oo mk_rel_funDN;