--- 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 \<circ> map_fn f = (`) f \<circ> 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| \<le>o |UNIV :: 'd set|" (is "_ \<le>o ?U")
by transfer (rule card_of_image)
also have "?U \<le>o natLeq +c ?U"
by (rule ordLeq_csum2) (rule card_of_Card_order)
- finally show "|set_fn F| \<le>o natLeq +c |UNIV :: 'd set|" .
+ finally have "|set_fn F| \<le>o natLeq +c |UNIV :: 'd set|" .
+ then show "|set_fn F| <o card_suc (natLeq +c |UNIV :: 'd set| )"
+ using ordLeq_ordLess_trans card_suc_greater card_order_csum natLeq_card_order
+ card_of_card_order_on by blast
next
fix R :: "'a \<Rightarrow> 'b \<Rightarrow> bool" and S :: "'b \<Rightarrow> 'c \<Rightarrow> bool"
show "rel_fn R OO rel_fn S \<le> rel_fn (R OO S)"
--- 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 \<le>o r"
@@ -126,6 +129,21 @@
lemma cinfinite_mono: "\<lbrakk>r1 \<le>o r2; cinfinite r1\<rbrakk> \<Longrightarrow> 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| <o r" and LEQ: "\<forall>i \<in> I. |A i| <o r"
+ shows "|\<Union>i \<in> I. A i| <o r"
+ using card_of_UNION_ordLess_infinite_Field regularCard_stable assms cinfinite_def by blast
subsection \<open>Binary sum\<close>
@@ -222,7 +240,6 @@
lemma Un_csum: "|A \<union> B| \<le>o |A| +c |B|"
using ordLeq_ordIso_trans[OF card_of_Un_Plus_ordLeq Plus_csum] by blast
-
subsection \<open>One\<close>
definition cone where
@@ -359,6 +376,76 @@
lemma csum_absorb1: "\<lbrakk>Cinfinite r2; r1 \<le>o r2\<rbrakk> \<Longrightarrow> r2 +c r1 =o r2"
by (rule csum_absorb1') auto
+lemma csum_absorb2: "\<lbrakk>Cinfinite r2 ; r1 \<le>o r2\<rbrakk> \<Longrightarrow> 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 \<le>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 \<le>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 r'" "q <o q'"
+shows "r +c q <o r' +c q'"
+proof -
+ have Well_order: "Well_order r" "Well_order q" "Well_order r'" "Well_order q'"
+ using card_order_on_well_order_on Card_order Cinfinite by auto
+ show ?thesis
+ proof (cases "Cinfinite r")
+ case outer: True
+ then show ?thesis
+ proof (cases "Cinfinite q")
+ case inner: True
+ then show ?thesis
+ proof (cases "r \<le>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 \<le>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 \<le>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 \<le>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 \<open>Exponentiation\<close>
@@ -568,6 +655,14 @@
"\<lbrakk>ctwo \<le>o q; Cinfinite r\<rbrakk> \<Longrightarrow> 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 <o natLeq"
unfolding ctwo_def using finite_UNIV natLeq_cinfinite natLeq_Card_order
by (intro Cfinite_ordLess_Cinfinite) (auto simp: cfinite_def card_of_Card_order)
@@ -583,6 +678,9 @@
lemma Un_Cinfinite_bound: "\<lbrakk>|A| \<le>o r; |B| \<le>o r; Cinfinite r\<rbrakk> \<Longrightarrow> |A \<union> B| \<le>o r"
by (auto simp add: cinfinite_def card_of_Un_ordLeq_infinite_Field)
+lemma Un_Cinfinite_bound_strict: "\<lbrakk>|A| <o r; |B| <o r; Cinfinite r\<rbrakk> \<Longrightarrow> |A \<union> B| <o r"
+by (auto simp add: cinfinite_def card_of_Un_ordLess_infinite_Field)
+
lemma UNION_Cinfinite_bound: "\<lbrakk>|I| \<le>o r; \<forall>i \<in> I. |A i| \<le>o r; Cinfinite r\<rbrakk> \<Longrightarrow> |\<Union>i \<in> I. A i| \<le>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': "\<lbrakk>Cnotzero r1; Cinfinite r2; r1 \<le>o r2\<rbrakk> \<Longrightarrow> 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 \<le>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 \<le>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 \<le>o (r1 +c r2) ^c ctwo"
unfolding cprod_def csum_def cexp_def ctwo_def Field_card_of
@@ -692,4 +814,27 @@
shows "\<exists>i \<in> Field (cardSuc r). B \<le> As i"
using cardSuc_UNION assms unfolding cinfinite_def by blast
+lemma Cinfinite_card_suc: "\<lbrakk> Cinfinite r ; card_order r \<rbrakk> \<Longrightarrow> Cinfinite (card_suc r)"
+ using Cinfinite_cong[OF cardSuc_ordIso_card_suc Cinfinite_cardSuc] .
+
+lemma regularCard_cardSuc: "Cinfinite k \<Longrightarrow> regularCard (cardSuc k)"
+ by (rule infinite_cardSuc_regularCard) (auto simp: cinfinite_def)
+
+lemma regular_card_suc: "card_order r \<Longrightarrow> Cinfinite r \<Longrightarrow> 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
--- 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) \<noteq> {}"
+proof
+ assume "Field(cardSuc r) = {}"
+ then have "|Field(cardSuc r)| \<le>o r" using assms Card_order_empty[of r] by auto
+ then have "cardSuc r \<le>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 \<Rightarrow> 'a suc rel" where
+ "card_suc \<equiv> \<lambda>_. 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 = "\<lambda>x. Abs_suc (Rep_suc x)"
+ have 1: "\<And>P. (\<forall>x\<in>Field ?r. P x) = (\<forall>x. P (Rep_suc x))" using Rep_suc_induct Rep_suc by blast
+ have 2: "\<And>P. (\<exists>x\<in>Field ?r. P x) = (\<exists>x. P (Rep_suc x))" using Rep_suc_cases Rep_suc by blast
+ have 3: "\<And>A a b. (a, b) \<in> A \<Longrightarrow> (Abs_suc a, Abs_suc b) \<in> map_prod Abs_suc Abs_suc ` A" unfolding map_prod_def by auto
+ have "\<forall>x\<in>Field ?r. (\<exists>b\<in>Field ?r. (x, b) \<in> ?r) \<or> (\<exists>a\<in>Field ?r. (a, x) \<in> ?r)"
+ unfolding Field_def Range.simps Domain.simps Un_iff by blast
+ then have "\<forall>x. (\<exists>b. (Rep_suc x, Rep_suc b) \<in> ?r) \<or> (\<exists>a. (Rep_suc a, Rep_suc x) \<in> ?r)" unfolding 1 2 .
+ then have "\<forall>x. (\<exists>b. (?ar x, ?ar b) \<in> map_prod Abs_suc Abs_suc ` ?r) \<or> (\<exists>a. (?ar a, ?ar x) \<in> map_prod Abs_suc Abs_suc ` ?r)" using 3 by fast
+ then have "\<forall>x. (\<exists>b. (x, b) \<in> card_suc r) \<or> (\<exists>a. (a, x) \<in> 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 \<Longrightarrow> 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 \<Longrightarrow> 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 \<Longrightarrow> 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 \<Longrightarrow> r <o card_suc r"
+ using ordLess_ordIso_trans[OF cardSuc_greater cardSuc_ordIso_card_suc] card_order_on_Card_order by blast
+
lemma card_of_Plus_ordLess_infinite:
assumes INF: "\<not>finite C" and
LESS1: "|A| <o |C|" and LESS2: "|B| <o |C|"
@@ -1501,6 +1562,27 @@
using assms card_of_Plus_ordLeq_infinite_Field card_of_Un_Plus_ordLeq
ordLeq_transitive by fast
+lemma card_of_Un_ordLess_infinite:
+assumes INF: "\<not>finite C" and
+ LESS1: "|A| <o |C|" and LESS2: "|B| <o |C|"
+shows "|A \<union> B| <o |C|"
+using assms card_of_Plus_ordLess_infinite card_of_Un_Plus_ordLeq
+ ordLeq_ordLess_trans by blast
+
+lemma card_of_Un_ordLess_infinite_Field:
+assumes INF: "\<not>finite (Field r)" and r: "Card_order r" and
+ LESS1: "|A| <o r" and LESS2: "|B| <o r"
+shows "|A Un B| <o r"
+proof-
+ let ?C = "Field r"
+ have 1: "r =o |?C| \<and> |?C| =o r" using r card_of_Field_ordIso
+ ordIso_symmetric by blast
+ hence "|A| <o |?C|" "|B| <o |?C|"
+ using LESS1 LESS2 ordLess_ordIso_trans by blast+
+ hence "|A Un B| <o |?C|" using INF
+ card_of_Un_ordLess_infinite by blast
+ thus ?thesis using 1 ordLess_ordIso_trans by blast
+qed
subsection \<open>Regular cardinals\<close>
@@ -1689,4 +1771,228 @@
thus ?thesis using card_of_ordIso by blast
qed
+subsection \<open>Regular vs. stable cardinals\<close>
+
+definition stable :: "'a rel \<Rightarrow> bool"
+where
+"stable r \<equiv> \<forall>(A::'a set) (F :: 'a \<Rightarrow> 'a set).
+ |A| <o r \<and> (\<forall>a \<in> A. |F a| <o r)
+ \<longrightarrow> |SIGMA a : A. F a| <o r"
+
+lemma regularCard_stable:
+ assumes cr: "Card_order r" and ir: "\<not>finite (Field r)" and reg: "regularCard r"
+ shows "stable r"
+ unfolding stable_def proof safe
+ fix A :: "'a set" and F :: "'a \<Rightarrow> 'a set" assume A: "|A| <o r" and F: "\<forall>a\<in>A. |F a| <o r"
+ {assume "r \<le>o |Sigma A F|"
+ hence "|Field r| \<le>o |Sigma A F|" using card_of_Field_ordIso[OF cr] ordIso_ordLeq_trans by blast
+ moreover have Fi: "Field r \<noteq> {}" using ir by auto
+ ultimately have "\<exists>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 \<in> A"
+ define L where "L = {(a,u) | u. u \<in> F a}"
+ have fL: "f ` L \<subseteq> 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| <o r" using F a ordIso_ordLess_trans[of "|L|" "|F a|"] unfolding L_def by auto
+ hence "|f ` L| <o r" using ordLeq_ordLess_trans[OF card_of_image, of "L"] unfolding L_def by auto
+ hence "\<not> 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 \<in> Field r" and "\<forall> l \<in> L. \<not> (f l \<noteq> k \<and> (k, f l) \<in> r)"
+ unfolding cofinal_def image_def by auto
+ hence "\<exists> k \<in> Field r. \<forall> l \<in> L. (f l, k) \<in> r"
+ using wo_rel.in_notinI[OF r _ _ \<open>k \<in> Field r\<close>] fL unfolding image_subset_iff by fast
+ hence "\<exists> k \<in> Field r. \<forall> u \<in> F a. (f (a,u), k) \<in> r" unfolding L_def by auto
+ }
+ then have x: "\<And>a. a\<in>A \<Longrightarrow> \<exists>k. k \<in> Field r \<and> (\<forall>u\<in>F a. (f (a, u), k) \<in> r)" by blast
+ obtain gg where "\<And>a. a\<in>A \<Longrightarrow> gg a = (SOME k. k \<in> Field r \<and> (\<forall>u\<in>F a. (f (a, u), k) \<in> r))" by simp
+ then have gg: "\<forall>a\<in>A. \<forall>u\<in>F a. (f (a, u), gg a) \<in> r" using someI_ex[OF x] by auto
+ obtain j0 where j0: "j0 \<in> Field r" using Fi by auto
+ define g where [abs_def]: "g a = (if F a \<noteq> {} then gg a else j0)" for a
+ have g: "\<forall> a \<in> A. \<forall> u \<in> F a. (f (a,u),g a) \<in> r" using gg unfolding g_def by auto
+ hence 1: "Field r \<subseteq> (\<Union>a \<in> A. under r (g a))"
+ using f[symmetric] unfolding under_def image_def by auto
+ have gA: "g ` A \<subseteq> 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 \<in> Field r"
+ then obtain j where ij: "(i,j) \<in> r" "i \<noteq> j" using cr ir infinite_Card_order_limit by fast
+ hence "j \<in> Field r" using card_order_on_def cr well_order_on_domain by fast
+ then obtain a where a: "a \<in> A" and j: "(j, g a) \<in> r" using 1 unfolding under_def by auto
+ hence "(i, g a) \<in> r" using ij wo_rel.TRANS[OF r] unfolding trans_def by blast
+ moreover have "i \<noteq> 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 "\<exists>j\<in>g ` A. i \<noteq> j \<and> (i, j) \<in> r" using a by auto
+ qed
+ ultimately have "|g ` A| =o r" using reg unfolding regularCard_def by auto
+ moreover have "|g ` A| \<le>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| <o r"
+ using cr not_ordLess_iff_ordLeq using card_of_Well_order card_order_on_well_order_on by blast
+qed
+
+lemma stable_regularCard:
+assumes cr: "Card_order r" and ir: "\<not>finite (Field r)" and st: "stable r"
+shows "regularCard r"
+unfolding regularCard_def proof safe
+ fix K assume K: "K \<subseteq> Field r" and cof: "cofinal K r"
+ have "|K| \<le>o r" using K card_of_Field_ordIso card_of_mono1 cr ordLeq_ordIso_trans by blast
+ moreover
+ {assume Kr: "|K| <o r"
+ have x: "\<And>a. a \<in> Field r \<Longrightarrow> \<exists>b. b \<in> K \<and> a \<noteq> b \<and> (a, b) \<in> r" using cof unfolding cofinal_def by blast
+ then obtain f where "\<And>a. a \<in> Field r \<Longrightarrow> f a = (SOME b. b \<in> K \<and> a \<noteq> b \<and> (a, b) \<in> r)" by simp
+ then have "\<forall>a\<in>Field r. f a \<in> K \<and> a \<noteq> f a \<and> (a, f a) \<in> r" using someI_ex[OF x] by simp
+ hence "Field r \<subseteq> (\<Union>a \<in> K. underS r a)" unfolding underS_def by auto
+ hence "r \<le>o |\<Union>a \<in> K. underS r a|"
+ using cr Card_order_iff_ordLeq_card_of card_of_mono1 ordLeq_transitive by blast
+ also have "|\<Union>a \<in> K. underS r a| \<le>o |SIGMA a: K. underS r a|" by (rule card_of_UNION_Sigma)
+ also
+ {have "\<forall> a \<in> K. |underS r a| <o r" using K card_of_underS[OF cr] subsetD by auto
+ hence "|SIGMA a: K. underS r a| <o r" using st Kr unfolding stable_def by auto
+ }
+ finally have "r <o r" .
+ hence False using ordLess_irreflexive by blast
+ }
+ ultimately show "|K| =o r" using ordLeq_iff_ordLess_or_ordIso by blast
+qed
+
+lemma internalize_card_of_ordLess:
+"( |A| <o r) = (\<exists>B < Field r. |A| =o |B| \<and> |B| <o r)"
+proof
+ assume "|A| <o r"
+ then obtain p where 1: "Field p < Field r \<and> |A| =o p \<and> p <o r"
+ using internalize_ordLess[of "|A|" r] by blast
+ hence "Card_order p" using card_of_Card_order Card_order_ordIso2 by blast
+ hence "|Field p| =o p" using card_of_Field_ordIso by blast
+ hence "|A| =o |Field p| \<and> |Field p| <o r"
+ using 1 ordIso_equivalence ordIso_ordLess_trans by blast
+ thus "\<exists>B < Field r. |A| =o |B| \<and> |B| <o r" using 1 by blast
+next
+ assume "\<exists>B < Field r. |A| =o |B| \<and> |B| <o r"
+ thus "|A| <o r" using ordIso_ordLess_trans by blast
+qed
+
+lemma card_of_Sigma_cong1:
+assumes "\<forall>i \<in> 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 \<Rightarrow> '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 = (\<lambda>(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: "\<forall>j \<in> J. |A j| =o |B j|"
+shows "|SIGMA i : I. A (f i)| =o |SIGMA j : J. B j|"
+proof-
+ have "\<forall>i \<in> 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| <o r" and
+ F_LESS: "\<And> a. a \<in> A \<Longrightarrow> |F a| <o r"
+shows "|SIGMA a : A. F a| <o r"
+proof-
+ obtain A' where 1: "A' < Field r \<and> |A'| <o r" and 2: " |A| =o |A'|"
+ using internalize_card_of_ordLess[of A r] A_LESS by blast
+ then obtain G where 3: "bij_betw G A' A"
+ using card_of_ordIso ordIso_symmetric by blast
+ (* *)
+ {fix a assume "a \<in> A"
+ hence "\<exists>B'. B' \<le> Field r \<and> |F a| =o |B'| \<and> |B'| <o r"
+ using internalize_card_of_ordLess[of "F a" r] F_LESS by blast
+ }
+ then obtain F' where
+ temp: "\<forall>a \<in> A. F' a \<le> Field r \<and> |F a| =o |F' a| \<and> |F' a| <o r"
+ using bchoice[of A "\<lambda> a B'. B' \<le> Field r \<and> |F a| =o |B'| \<and> |B'| <o r"] by blast
+ hence 4: "\<forall>a \<in> A. F' a \<le> Field r \<and> |F' a| <o r" by auto
+ have 5: "\<forall>a \<in> A. |F' a| =o |F a|" using temp ordIso_symmetric by auto
+ (* *)
+ have "\<forall>a' \<in> A'. F'(G a') \<le> Field r \<and> |F'(G a')| <o r"
+ using 3 4 bij_betw_ball[of G A' A] by auto
+ hence "|SIGMA a' : A'. F'(G a')| <o r"
+ using ST 1 unfolding stable_def by auto
+ moreover have "|SIGMA a' : A'. F'(G a')| =o |SIGMA a : A. F a|"
+ using card_of_Sigma_cong[of G A' A F' F] 5 3 by blast
+ ultimately show ?thesis using ordIso_symmetric ordIso_ordLess_trans by blast
+qed
+
+lemma stable_natLeq: "stable natLeq"
+proof(unfold stable_def, safe)
+ fix A :: "'a set" and F :: "'a \<Rightarrow> 'a set"
+ assume "|A| <o natLeq" and "\<forall>a\<in>A. |F a| <o natLeq"
+ hence "finite A \<and> (\<forall>a \<in> 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 | <o natLeq"
+ by (auto simp add: finite_iff_ordLess_natLeq)
+qed
+
+corollary regularCard_natLeq: "regularCard natLeq"
+using stable_regularCard[OF natLeq_Card_order _ stable_natLeq] Field_natLeq by simp
+
+lemma stable_ordIso1:
+assumes ST: "stable r" and ISO: "r' =o r"
+shows "stable r'"
+proof(unfold stable_def, auto)
+ fix A::"'b set" and F::"'b \<Rightarrow> 'b set"
+ assume "|A| <o r'" and "\<forall>a \<in> A. |F a| <o r'"
+ hence "( |A| <o r) \<and> (\<forall>a \<in> A. |F a| <o r)"
+ using ISO ordLess_ordIso_trans by blast
+ hence "|SIGMA a : A. F a| <o r" using assms stable_elim by blast
+ thus "|SIGMA a : A. F a| <o r'"
+ using ISO ordIso_symmetric ordLess_ordIso_trans by blast
+qed
+
+lemma stable_UNION:
+assumes ST: "stable r" and A_LESS: "|A| <o r" and
+ F_LESS: "\<And> a. a \<in> A \<Longrightarrow> |F a| <o r"
+shows "|\<Union>a \<in> A. F a| <o r"
+proof-
+ have "|\<Union>a \<in> A. F a| \<le>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| <o |B|" and LEQ: "\<forall>i \<in> I. |A i| <o |B|"
+shows "|\<Union>i \<in> I. A i| <o |B|"
+ using assms stable_UNION by blast
+
+corollary card_of_UNION_ordLess_infinite_Field:
+assumes ST: "stable r" and r: "Card_order r" and
+ LEQ_I: "|I| <o r" and LEQ: "\<forall>i \<in> I. |A i| <o r"
+shows "|\<Union>i \<in> I. A i| <o r"
+proof-
+ let ?B = "Field r"
+ have 1: "r =o |?B| \<and> |?B| =o r" using r card_of_Field_ordIso
+ ordIso_symmetric by blast
+ hence "|I| <o |?B|" "\<forall>i \<in> I. |A i| <o |?B|"
+ using LEQ_I LEQ ordLess_ordIso_trans by blast+
+ moreover have "stable |?B|" using stable_ordIso1 ST 1 by blast
+ ultimately have "|\<Union>i \<in> I. A i| <o |?B|" using LEQ
+ card_of_UNION_ordLess_infinite by blast
+ thus ?thesis using 1 ordLess_ordIso_trans by blast
+qed
+
end
--- a/src/HOL/BNF_Composition.thy Sat Jun 25 09:50:40 2022 +0000
+++ b/src/HOL/BNF_Composition.thy Mon Jun 27 15:54:18 2022 +0200
@@ -1,7 +1,8 @@
(* Title: HOL/BNF_Composition.thy
Author: Dmitriy Traytel, TU Muenchen
Author: Jasmin Blanchette, TU Muenchen
- Copyright 2012, 2013, 2014
+ Author: Jan van Brügge, TU Muenchen
+ Copyright 2012, 2013, 2014, 2022
Composition of bounded natural functors.
*)
@@ -18,12 +19,42 @@
lemma empty_natural: "(\<lambda>_. {}) \<circ> f = image g \<circ> (\<lambda>_. {})"
by (rule ext) simp
+lemma Cinfinite_gt_empty: "Cinfinite r \<Longrightarrow> |{}| <o r"
+ by (simp add: cinfinite_def finite_ordLess_infinite card_of_ordIso_finite Field_card_of card_of_well_order_on emptyI card_order_on_well_order_on)
+
lemma Union_natural: "Union \<circ> image (image f) = image f \<circ> Union"
by (rule ext) (auto simp only: comp_apply)
lemma in_Union_o_assoc: "x \<in> (Union \<circ> gset \<circ> gmap) A \<Longrightarrow> x \<in> (Union \<circ> (gset \<circ> gmap)) A"
by (unfold comp_assoc)
+lemma regularCard_UNION_bound:
+ assumes "Cinfinite r" "regularCard r" and "|I| <o r" "\<And>i. i \<in> I \<Longrightarrow> |A i| <o r"
+ shows "|\<Union>i\<in>I. A i| <o r"
+ using assms cinfinite_def regularCard_stable stable_UNION by blast
+
+lemma comp_single_set_bd_strict:
+ assumes fbd: "Cinfinite fbd" "regularCard fbd" and
+ gbd: "Cinfinite gbd" "regularCard gbd" and
+ fset_bd: "\<And>x. |fset x| <o fbd" and
+ gset_bd: "\<And>x. |gset x| <o gbd"
+ shows "|\<Union>(fset ` gset x)| <o gbd *c fbd"
+proof (cases "fbd <o gbd")
+ case True
+ then have "|fset x| <o gbd" for x using fset_bd ordLess_transitive by blast
+ then have "|\<Union>(fset ` gset x)| <o gbd" using regularCard_UNION_bound[OF gbd gset_bd] by blast
+ then have "|\<Union> (fset ` gset x)| <o fbd *c gbd"
+ using ordLess_ordLeq_trans ordLeq_cprod2 gbd(1) fbd(1) cinfinite_not_czero by blast
+ then show ?thesis using ordLess_ordIso_trans cprod_com by blast
+next
+ case False
+ have "Well_order fbd" "Well_order gbd" using fbd(1) gbd(1) card_order_on_well_order_on by auto
+ then have "gbd \<le>o fbd" using not_ordLess_iff_ordLeq False by blast
+ then have "|gset x| <o fbd" for x using gset_bd ordLess_ordLeq_trans by blast
+ then have "|\<Union>(fset ` gset x)| <o fbd" using regularCard_UNION_bound[OF fbd] fset_bd by blast
+ then show ?thesis using ordLess_ordLeq_trans ordLeq_cprod2 gbd(1) fbd(1) cinfinite_not_czero by blast
+qed
+
lemma comp_single_set_bd:
assumes fbd_Card_order: "Card_order fbd" and
fset_bd: "\<And>x. |fset x| \<le>o fbd" and
@@ -75,6 +106,9 @@
lemma comp_set_bd_Union_o_collect: "|\<Union>(\<Union>((\<lambda>f. f x) ` X))| \<le>o hbd \<Longrightarrow> |(Union \<circ> collect X) x| \<le>o hbd"
by (unfold comp_apply collect_def) simp
+lemma comp_set_bd_Union_o_collect_strict: "|\<Union>(\<Union>((\<lambda>f. f x) ` X))| <o hbd \<Longrightarrow> |(Union \<circ> collect X) x| <o hbd"
+ by (unfold comp_apply collect_def) simp
+
lemma Collect_inj: "Collect P = Collect Q \<Longrightarrow> P = Q"
by blast
@@ -91,7 +125,7 @@
lemma type_copy_map_cong0: "M (g x) = N (h x) \<Longrightarrow> (f \<circ> M \<circ> g) x = (f \<circ> N \<circ> h) x"
by auto
-lemma type_copy_set_bd: "(\<And>y. |S y| \<le>o bd) \<Longrightarrow> |(S \<circ> Rep) x| \<le>o bd"
+lemma type_copy_set_bd: "(\<And>y. |S y| <o bd) \<Longrightarrow> |(S \<circ> Rep) x| <o bd"
by auto
lemma vimage2p_cong: "R = S \<Longrightarrow> vimage2p f g R = vimage2p f g S"
@@ -152,7 +186,7 @@
map: "id :: 'a \<Rightarrow> 'a"
bd: natLeq
rel: "(=) :: 'a \<Rightarrow> 'a \<Rightarrow> 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 \<Rightarrow> 'a" where
"id_bnf \<equiv> (\<lambda>x. x)"
@@ -167,8 +201,8 @@
rel: "id_bnf :: ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
pred: "id_bnf :: ('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 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
--- 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 \<in> 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 card_suc r'"
+shows "r \<le>o r'"
+proof -
+ have "Card_order (card_suc r')" by (rule Card_order_card_suc[OF ORD(3)])
+ then have "cardSuc r \<le>o card_suc r'" using cardSuc_least ORD LESS by blast
+ then have "cardSuc r \<le>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: "\<lbrakk>Cinfinite r; card_order r\<rbrakk> \<Longrightarrow> natLeq <o card_suc r"
+ using natLeq_ordLeq_cinfinite card_suc_greater ordLeq_ordLess_trans by blast
+
+corollary natLeq_ordLess_cinfinite': "\<lbrakk>Cinfinite r'; card_order r'; r \<equiv> card_suc r'\<rbrakk> \<Longrightarrow> natLeq <o r"
+ using natLeq_ordLess_cinfinite by blast
+
ML_file \<open>Tools/BNF/bnf_gfp_util.ML\<close>
ML_file \<open>Tools/BNF/bnf_gfp_tactics.ML\<close>
ML_file \<open>Tools/BNF/bnf_gfp.ML\<close>
--- 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 <o r' \<Longrightarrow> \<not> r' \<le>o r"
using ordLess_ordLeq_trans ordLess_irreflexive by blast
+lemma not_ordLeq_ordLess:
+"r \<le>o r' \<Longrightarrow> \<not> r' <o r"
+using not_ordLess_ordLeq by blast
+
lemma ordLess_or_ordLeq:
assumes WELL: "Well_order r" and WELL': "Well_order r'"
shows "r <o r' \<or> r' \<le>o r"
--- 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) \<notin> r \<or> j = i" and "i \<in> Field r" and "j \<in> Field r"
+shows "(i,j) \<in> r" using assms max2_def max2_greater_among by fastforce
subsubsection \<open>Existence and uniqueness for isMinim and well-definedness of minim\<close>
--- 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| \<le>o natLeq"
- apply (rule ordLess_imp_ordLeq)
+ show "|setl x| <o natLeq"
apply (rule finite_iff_ordLess_natLeq[THEN iffD1])
by (simp add: sum_set_defs(1) split: sum.split)
next
fix x :: "'o + 'p"
- show "|setr x| \<le>o natLeq"
- apply (rule ordLess_imp_ordLeq)
+ show "|setr x| <o natLeq"
apply (rule finite_iff_ordLess_natLeq[THEN iffD1])
by (simp add: sum_set_defs(2) split: sum.split)
next
@@ -168,13 +169,15 @@
next
show "cinfinite natLeq" by (rule natLeq_cinfinite)
next
- fix x
- show "|{fst x}| \<le>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}| \<le>o natLeq"
- by (rule ordLess_imp_ordLeq) (simp add: finite_iff_ordLess_natLeq[symmetric])
+ show "|{fst x}| <o natLeq"
+ by (simp add: finite_iff_ordLess_natLeq[symmetric])
+next
+ fix x
+ show "|{snd x}| <o natLeq"
+ by (simp add: finite_iff_ordLess_natLeq[symmetric])
next
fix R1 R2 S1 S2
show "rel_prod R1 R2 OO rel_prod S1 S2 \<le> rel_prod (R1 OO S1) (R2 OO S2)" by auto
@@ -190,7 +193,7 @@
bnf "'a \<Rightarrow> 'b"
map: "(\<circ>)"
sets: range
- bd: "natLeq +c |UNIV :: 'a set|"
+ bd: "card_suc (natLeq +c |UNIV::'a set|)"
rel: "rel_fun (=)"
pred: "pred_fun (\<lambda>_. True)"
proof
@@ -206,20 +209,38 @@
fix f show "range \<circ> (\<circ>) f = (`) f \<circ> 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| \<le>o | (UNIV::'d set) |" (is "_ \<le>o ?U") by (rule card_of_image)
- also have "?U \<le>o natLeq +c ?U" by (rule ordLeq_csum2) (rule card_of_Card_order)
- finally show "|range f| \<le>o natLeq +c ?U" .
+ then have 1: "|range f| \<le>o natLeq +c ?U" using ordLeq_transitive ordLeq_csum2 card_of_Card_order by blast
+ have "natLeq +c ?U <o card_suc (natLeq +c ?U)" using card_of_card_order_on card_order_csum natLeq_card_order card_suc_greater by blast
+ then have "|range f| <o card_suc (natLeq +c ?U)" by (rule ordLeq_ordLess_trans[OF 1])
+ then show "|range f| <o card_suc (natLeq +c ?U)"
+ using ordLess_ordLeq_trans ordLeq_csum2 card_of_card_order_on Card_order_card_suc by blast
next
fix R S
show "rel_fun (=) R OO rel_fun (=) S \<le> rel_fun (=) (R OO S)" by (auto simp: rel_fun_def)
--- 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 \<circ> map_bset f = (`) f \<circ> set_bset" by (rule ext, transfer) auto
next
fix X :: "'a set['k]"
- show "|set_bset X| \<le>o natLeq +c |UNIV :: 'k set|"
- by transfer (blast dest: ordLess_imp_ordLeq)
+ have "|set_bset X| <o natLeq +c |UNIV :: 'k set|" by transfer blast
+ then show "|set_bset X| <o card_suc (natLeq +c |UNIV :: 'k set| )"
+ using card_suc_greater card_order_csum natLeq_card_order
+ card_of_card_order_on ordLess_transitive by blast
next
fix R S
show "rel_bset R OO rel_bset S \<le> rel_bset (R OO S)"
@@ -107,7 +109,8 @@
fix x
assume "x \<in> 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"
--- 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: "\<lbrakk>card_order_on B r; bij_betw f A B\<rbrakk> \<Longrightarrow> r =o |A|"
using card_of_ordIso card_of_unique ordIso_equivalence by blast
-lemma internalize_card_of_ordLess:
-"( |A| <o r) = (\<exists>B < Field r. |A| =o |B| \<and> |B| <o r)"
-proof
- assume "|A| <o r"
- then obtain p where 1: "Field p < Field r \<and> |A| =o p \<and> p <o r"
- using internalize_ordLess[of "|A|" r] by blast
- hence "Card_order p" using card_of_Card_order Card_order_ordIso2 by blast
- hence "|Field p| =o p" using card_of_Field_ordIso by blast
- hence "|A| =o |Field p| \<and> |Field p| <o r"
- using 1 ordIso_equivalence ordIso_ordLess_trans by blast
- thus "\<exists>B < Field r. |A| =o |B| \<and> |B| <o r" using 1 by blast
-next
- assume "\<exists>B < Field r. |A| =o |B| \<and> |B| <o r"
- thus "|A| <o r" using ordIso_ordLess_trans by blast
-qed
-
lemma internalize_card_of_ordLess2:
"( |A| <o |C| ) = (\<exists>B < C. |A| =o |B| \<and> |B| <o |C| )"
using internalize_card_of_ordLess[of "A" "|C|"] Field_card_of[of C] by auto
@@ -388,36 +372,6 @@
using assms card_of_mono2 card_of_Sigma_mono
[of f I J "\<lambda> i. Field(p i)" "\<lambda> j. Field(r j)"] by metis
-lemma card_of_Sigma_cong1:
-assumes "\<forall>i \<in> 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 \<Rightarrow> '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 = (\<lambda>(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: "\<forall>j \<in> J. |A j| =o |B j|"
-shows "|SIGMA i : I. A (f i)| =o |SIGMA j : J. B j|"
-proof-
- have "\<forall>i \<in> 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 "\<forall>i \<in> 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 \<open>Regular vs. stable cardinals\<close>
-definition stable :: "'a rel \<Rightarrow> bool"
-where
-"stable r \<equiv> \<forall>(A::'a set) (F :: 'a \<Rightarrow> 'a set).
- |A| <o r \<and> (\<forall>a \<in> A. |F a| <o r)
- \<longrightarrow> |SIGMA a : A. F a| <o r"
-
-lemma regularCard_stable:
-assumes cr: "Card_order r" and ir: "\<not>finite (Field r)" and reg: "regularCard r"
-shows "stable r"
-unfolding stable_def proof safe
- fix A :: "'a set" and F :: "'a \<Rightarrow> 'a set" assume A: "|A| <o r" and F: "\<forall>a\<in>A. |F a| <o r"
- {assume "r \<le>o |Sigma A F|"
- hence "|Field r| \<le>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 \<noteq> {}" 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 \<in> A"
- define L where "L = {(a,u) | u. u \<in> F a}"
- have fL: "f ` L \<subseteq> 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| <o r" using F a ordIso_ordLess_trans[of "|L|" "|F a|"] unfolding L_def by auto
- hence "|f ` L| <o r" using ordLeq_ordLess_trans[OF card_of_image, of "L"] unfolding L_def by auto
- hence "\<not> cofinal (f ` L) r" using reg fL unfolding regularCard_def by (metis not_ordLess_ordIso)
- then obtain k where k: "k \<in> Field r" and "\<forall> l \<in> L. \<not> (f l \<noteq> k \<and> (k, f l) \<in> r)"
- unfolding cofinal_def image_def by auto
- hence "\<exists> k \<in> Field r. \<forall> l \<in> L. (f l, k) \<in> r" using r by (metis fL image_subset_iff wo_rel.in_notinI)
- hence "\<exists> k \<in> Field r. \<forall> u \<in> F a. (f (a,u), k) \<in> r" unfolding L_def by auto
- }
- then obtain gg where gg: "\<forall> a \<in> A. \<forall> u \<in> F a. (f (a,u), gg a) \<in> r" by metis
- obtain j0 where j0: "j0 \<in> Field r" using Fi by auto
- define g where [abs_def]: "g a = (if F a \<noteq> {} then gg a else j0)" for a
- have g: "\<forall> a \<in> A. \<forall> u \<in> F a. (f (a,u),g a) \<in> r" using gg unfolding g_def by auto
- hence 1: "Field r \<subseteq> (\<Union>a \<in> A. under r (g a))"
- using f[symmetric] unfolding under_def image_def by auto
- have gA: "g ` A \<subseteq> 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 \<in> Field r"
- then obtain j where ij: "(i,j) \<in> r" "i \<noteq> j" using cr ir by (metis infinite_Card_order_limit)
- hence "j \<in> Field r" by (metis card_order_on_def cr well_order_on_domain)
- then obtain a where a: "a \<in> A" and j: "(j, g a) \<in> r" using 1 unfolding under_def by auto
- hence "(i, g a) \<in> r" using ij wo_rel.TRANS[OF r] unfolding trans_def by blast
- moreover have "i \<noteq> 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 "\<exists>j\<in>g ` A. i \<noteq> j \<and> (i, j) \<in> r" using a by auto
- qed
- ultimately have "|g ` A| =o r" using reg unfolding regularCard_def by auto
- moreover have "|g ` A| \<le>o |A|" by (metis card_of_image)
- ultimately have False using A by (metis not_ordLess_ordIso ordLeq_ordLess_trans)
- }
- thus "|Sigma A F| <o r"
- using cr not_ordLess_iff_ordLeq by (metis card_of_Well_order card_order_on_well_order_on)
-qed
-
lemma stable_regularCard:
assumes cr: "Card_order r" and ir: "\<not>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| <o r" and
- F_LESS: "\<And> a. a \<in> A \<Longrightarrow> |F a| <o r"
-shows "|SIGMA a : A. F a| <o r"
-proof-
- obtain A' where 1: "A' < Field r \<and> |A'| <o r" and 2: " |A| =o |A'|"
- using internalize_card_of_ordLess[of A r] A_LESS by blast
- then obtain G where 3: "bij_betw G A' A"
- using card_of_ordIso ordIso_symmetric by blast
- (* *)
- {fix a assume "a \<in> A"
- hence "\<exists>B'. B' \<le> Field r \<and> |F a| =o |B'| \<and> |B'| <o r"
- using internalize_card_of_ordLess[of "F a" r] F_LESS by blast
- }
- then obtain F' where
- temp: "\<forall>a \<in> A. F' a \<le> Field r \<and> |F a| =o |F' a| \<and> |F' a| <o r"
- using bchoice[of A "\<lambda> a B'. B' \<le> Field r \<and> |F a| =o |B'| \<and> |B'| <o r"] by blast
- hence 4: "\<forall>a \<in> A. F' a \<le> Field r \<and> |F' a| <o r" by auto
- have 5: "\<forall>a \<in> A. |F' a| =o |F a|" using temp ordIso_symmetric by auto
- (* *)
- have "\<forall>a' \<in> A'. F'(G a') \<le> Field r \<and> |F'(G a')| <o r"
- using 3 4 bij_betw_ball[of G A' A] by auto
- hence "|SIGMA a' : A'. F'(G a')| <o r"
- using ST 1 unfolding stable_def by auto
- moreover have "|SIGMA a' : A'. F'(G a')| =o |SIGMA a : A. F a|"
- using card_of_Sigma_cong[of G A' A F' F] 5 3 by blast
- ultimately show ?thesis using ordIso_symmetric ordIso_ordLess_trans by blast
-qed
-
lemma stable_natLeq: "stable natLeq"
proof(unfold stable_def, safe)
fix A :: "'a set" and F :: "'a \<Rightarrow> '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| <o r" and
- F_LESS: "\<And> a. a \<in> A \<Longrightarrow> |F a| <o r"
-shows "|\<Union>a \<in> A. F a| <o r"
-proof-
- have "|\<Union>a \<in> A. F a| \<le>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'"
--- 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 "(\<forall>b \<in> B. phi b) = (\<forall>a \<in> 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 \<in> A"
shows "bij_betw f (A - {a}) (A' - {f a})"
--- 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) \<notin> r \<or> j = i" and "i \<in> Field r" and "j \<in> Field r"
-shows "(i,j) \<in> 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"
--- 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' \<Longrightarrow> B \<subseteq> A \<Longrightarrow> f ` B = B' \<Longrightarrow> bij_betw f B B'"
by (auto simp add: bij_betw_def inj_on_def)
+lemma bij_betw_ball: "bij_betw f A B \<Longrightarrow> (\<forall>b \<in> B. phi b) = (\<forall>a \<in> 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 "\<And>x'. y = f x' \<Longrightarrow> x' = x"
--- 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 \<circ> cimage f = (`) f \<circ> 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| \<le>o natLeq"
- including cset.lifting by transfer (unfold countable_card_le_natLeq)
+ fix C
+ have "|rcset C| \<le>o natLeq" including cset.lifting by transfer (unfold countable_card_le_natLeq)
+ then show "|rcset C| <o card_suc natLeq"
+ using card_suc_greater natLeq_card_order ordLeq_ordLess_trans by blast
next
fix R S
show "rel_cset R OO rel_cset S \<le> rel_cset (R OO S)"
--- 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])
--- 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 \<le> rel_mset (R OO S)" for R S
unfolding rel_mset_def[abs_def] OO_def
apply clarify
--- 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 \<circ> map_uprod f = (`) f \<circ> set_uprod" for f :: "'a \<Rightarrow> '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 \<le> rel_uprod (R OO S)"
for R :: "'a \<Rightarrow> 'b \<Rightarrow> bool" and S :: "'b \<Rightarrow> 'c \<Rightarrow> bool" by(rule predicate2I)(transfer; auto)
show "rel_uprod R = (\<lambda>x y. \<exists>z. set_uprod z \<subseteq> {(x, y). R x y} \<and> map_uprod fst z = x \<and> map_uprod snd z = y)"
--- 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 "\<And>f g. map_pmf (f \<circ> g) = map_pmf f \<circ> map_pmf g" by (rule map_pmf_compose)
@@ -1365,14 +1365,20 @@
show "\<And>f::'a \<Rightarrow> 'b. set_pmf \<circ> map_pmf f = (`) f \<circ> set_pmf"
by (rule pmf_set_map)
- show "(card_of (set_pmf p), natLeq) \<in> 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) \<in> ordLess" for p :: "'s pmf"
proof -
have "(card_of (set_pmf p), card_of (UNIV :: nat set)) \<in> 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) \<in> 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 "\<And>R. rel_pmf R = (\<lambda>x y. \<exists>z. set_pmf z \<subseteq> {(x, y). R x y} \<and>
@@ -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: "(\<And>x. x \<in> set_pmf p \<Longrightarrow> f x = x) \<Longrightarrow> map_pmf f p = p"
by(simp cong: pmf.map_cong)
--- 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)
--- 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
--- 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;
--- 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;
--- 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;
--- 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 =>
--- 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>\<open>undefined\<close>, T);
+fun mk_card_suc t =
+ let
+ val T = fst (dest_relT (fastype_of t))
+ val T' = Type (\<^type_name>\<open>suc\<close>, [T])
+ in Const (\<^const_name>\<open>card_suc\<close>, 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>\<open>old.rec_nat\<close>, T --> fastype_of Suc --> HOLogic.natT --> T) $ Zero $ Suc end;
--- 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);
--- 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
--- 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 \<le> 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];
--- 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>\<open>cinfinite\<close>, fastype_of bd --> HOLogic.boolT) $ bd;
+fun mk_regularCard bd = Const (\<^const_name>\<open>regularCard\<close>, fastype_of bd --> HOLogic.boolT) $ bd;
+
fun mk_ordLeq t1 t2 =
HOLogic.mk_mem (HOLogic.mk_prod (t1, t2),
Const (\<^const_name>\<open>ordLeq\<close>, mk_relT (fastype_of t1, fastype_of t2)));
+fun mk_ordLess t1 t2 =
+ HOLogic.mk_mem (HOLogic.mk_prod (t1, t2),
+ Const (\<^const_name>\<open>ordLess\<close>, 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;