# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1673798285 0
# Node ID f70d431b5016de2a6487c88b908573cb9a0162d4
# Parent  f552cf789a8dc574d8b632c779f6d5da5493873e
One messy, messy proof

diff -r f552cf789a8d -r f70d431b5016 src/HOL/Basic_BNFs.thy
--- a/src/HOL/Basic_BNFs.thy	Sat Jan 14 21:42:08 2023 +0000
+++ b/src/HOL/Basic_BNFs.thy	Sun Jan 15 15:58:05 2023 +0000
@@ -130,7 +130,7 @@
 
 lemma rel_prod_conv:
   "rel_prod R1 R2 = (\<lambda>(a, b) (c, d). R1 a c \<and> R2 b d)"
-  by (rule ext, rule ext) auto
+  by force
 
 definition
   pred_fun :: "('a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
@@ -198,27 +198,22 @@
 
 lemma regularCard_bd_fun: "regularCard (natLeq +c card_suc ( |UNIV| ))"
   (is "regularCard (_ +c card_suc ?U)")
-  apply (cases "Cinfinite ?U")
-   apply (rule regularCard_csum)
-      apply (rule natLeq_Cinfinite)
-     apply (rule Cinfinite_card_suc)
-      apply assumption
-     apply (rule card_of_card_order_on)
-    apply (rule regularCard_natLeq)
-   apply (rule regularCard_card_suc)
-    apply (rule card_of_card_order_on)
-   apply assumption
-  apply (rule regularCard_ordIso[of natLeq])
-    apply (rule csum_absorb1[THEN ordIso_symmetric])
-     apply (rule natLeq_Cinfinite)
-    apply (rule card_suc_least)
-      apply (rule card_of_card_order_on)
-     apply (rule natLeq_Card_order)
-    apply (subst finite_iff_ordLess_natLeq[symmetric])
-    apply (simp add: cinfinite_def Field_card_of card_of_card_order_on)
-   apply (rule natLeq_Cinfinite)
-  apply (rule regularCard_natLeq)
-  done
+proof (cases "Cinfinite ?U")
+  case True
+  then show ?thesis 
+    by (intro regularCard_csum natLeq_Cinfinite Cinfinite_card_suc 
+              card_of_card_order_on regularCard_natLeq regularCard_card_suc)
+next
+  case False
+  then have "card_suc ?U \<le>o natLeq"
+    unfolding cinfinite_def Field_card_of
+    by (intro card_suc_least; 
+        simp add: natLeq_Card_order card_of_card_order_on flip: finite_iff_ordLess_natLeq)
+  then have "natLeq =o natLeq +c card_suc ?U"
+    using natLeq_Cinfinite csum_absorb1 ordIso_symmetric by blast
+  then show ?thesis 
+    by (intro regularCard_ordIso[OF _ natLeq_Cinfinite regularCard_natLeq])
+qed
 
 lemma ordLess_bd_fun: "|UNIV::'a set| <o natLeq +c card_suc ( |UNIV::'a set| )"
   (is "_ <o (_ +c card_suc (?U :: 'a rel))")