--- a/src/Doc/Datatypes/Datatypes.thy Mon Jun 27 15:54:18 2022 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy Mon Jun 27 17:36:26 2022 +0200
@@ -2855,7 +2855,7 @@
bnf "('d, 'a) fn"
map: map_fn
sets: set_fn
- bd: "card_suc (natLeq +c |UNIV :: 'd set| )"
+ bd: "natLeq +c card_suc |UNIV :: 'd set|"
rel: rel_fn
pred: pred_fn
proof -
@@ -2875,24 +2875,23 @@
show "set_fn \<circ> map_fn f = (`) f \<circ> set_fn"
by transfer (auto simp add: comp_def)
next
- show "card_order (card_suc (natLeq +c |UNIV :: 'd set| ))"
- by (rule card_order_card_suc_natLeq_UNIV)
+ show "card_order (natLeq +c card_suc |UNIV :: 'd set| )"
+ by (rule card_order_bd_fun)
next
- show "cinfinite (card_suc (natLeq +c |UNIV :: 'd set| ))"
- by (rule cinfinite_card_suc_natLeq_UNIV)
+ show "cinfinite (natLeq +c card_suc |UNIV :: 'd set| )"
+ by (rule Cinfinite_bd_fun[THEN conjunct1])
next
- show "regularCard (card_suc (natLeq +c |UNIV :: 'd set| ))"
- by (rule regularCard_card_suc_natLeq_UNIV)
+ show "regularCard (natLeq +c card_suc |UNIV :: 'd set| )"
+ by (rule regularCard_bd_fun)
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 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
+ also have "?U <o card_suc ?U"
+ by (simp add: card_of_card_order_on card_suc_greater)
+ also have "card_suc ?U \<le>o natLeq +c card_suc ?U"
+ using Card_order_card_suc card_of_card_order_on ordLeq_csum2 by blast
+ finally show "|set_fn F| <o natLeq +c card_suc |UNIV :: 'd set|" .
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)"