--- 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)