src/HOL/Basic_BNFs.thy

 (*  Title:      HOL/Basic_BNFs.thy
     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.
 *)
 
 section \<open>Registration of Basic Types as Bounded Natural Functors\<close>

 next
   show "card_order natLeq" by (rule natLeq_card_order)
 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
   fix R1 R2 S1 S2
   show "rel_sum R1 R2 OO rel_sum S1 S2 \<le> rel_sum (R1 OO S1) (R2 OO S2)"

 next
   show "card_order natLeq" by (rule natLeq_card_order)
 next
   show "cinfinite natLeq" by (rule natLeq_cinfinite)
 next
+  show "regularCard natLeq" by (rule regularCard_natLeq)
+next
   fix x
-  show "|{fst 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}| \<le>o natLeq"
-    by (rule ordLess_imp_ordLeq) (simp add: finite_iff_ordLess_natLeq[symmetric])
+  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
 next
   fix R S

 qed auto
 
 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
   fix f show "id \<circ> f = id f" by simp
 next

   thus "f \<circ> x = g \<circ> x" by auto
 next
   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)
 next
   fix R