feat(HOTG) clean up transitive closures and move general stuff to AFP

HOTG/Arithmetics/HOTG_Arithmetics_Cardinal_Arithmetics.thy

@@ -3,10 +3,10 @@
 subsection \<open>Compatibility of Set Arithmetics and Cardinal Arithmetics\<close>
 theory HOTG_Arithmetics_Cardinal_Arithmetics
   imports
+    HOTG_Bounded_Definite_Description
     HOTG_Cardinals_Addition
     HOTG_Cardinals_Multiplication
     HOTG_Addition
-    HOTG_Functions_Injective
     HOTG_Multiplication
 begin
 
@@ -24,14 +24,15 @@ qed
 
 text\<open>The next theorem shows that set addition is compatible with cardinality addition.\<close>
 
-(*TODO: cardinalities on rhs can be removed*)
-theorem cardinality_add_eq_cardinal_add_cardinality: "|X + Y| = |X| \<oplus> |Y|"
-  using disjoint_lift_self_right by (auto simp add:
-  cardinality_bin_union_eq_cardinal_add_cardinality_if_disjoint add_eq_bin_union_lift)
+theorem cardinality_add_eq_cardinal_add: "|X + Y| = X \<oplus> Y"
+  unfolding add_eq_bin_union_lift
+  by (subst cardinality_bin_union_eq_cardinal_add_if_disjoint[OF disjoint_lift_self_right],
+    subst cardinality_cardinal_add_eq_cardinal_add[symmetric])
+  (simp add: cardinality_lift_eq_cardinality_right)
 
 text\<open>The next theorems show that set multiplication is compatible with cardinality multiplication.\<close>
 
-theorem cardinality_mul_eq_cardinal_pair: "|X * Y| = |X \<times> Y|"
+lemma mul_equipollent_pair: "X * Y \<approx> X \<times> Y"
 proof -
   define f :: "set \<Rightarrow> set" where "f \<equiv> \<lambda>\<langle>x, y\<rangle>. X * y + x"
   have "injective_on (X \<times> Y :: set) f"
@@ -45,15 +46,15 @@ proof -
     then show "p\<^sub>1 = p\<^sub>2" using \<open>p\<^sub>1 = \<langle>x\<^sub>1, y\<^sub>1\<rangle>\<close> \<open>p\<^sub>2 = \<langle>x\<^sub>2, y\<^sub>2\<rangle>\<close> by auto
   qed auto
   then obtain g where "bijection_on (X \<times> Y) (image f (X \<times> Y)) f g"
-    using bijection_on_image_if_injective_on by blast
-  then have "X \<times> Y \<approx> image f (X \<times> Y)" using equipollentI by blast
+    using bijection_on_image_the_inverse_on_if_injective_on by blast
   moreover have "image f (X \<times> Y) = X * Y"
-    unfolding mul_eq_idx_union_repl_mul_add[of X Y] f_def by force
-  ultimately show ?thesis using cardinality_eq_if_equipollent by auto
+    unfolding mul_eq_idx_union_repl_mul_add[of X Y] f_def by fastforce
+  ultimately show ?thesis by (intro equipollentI) fastforce
 qed
 
 theorem cardinality_mul_eq_cardinal_mul: "|X * Y| = X \<otimes> Y"
-  using cardinality_mul_eq_cardinal_pair cardinal_mul_eq_cardinality_pair by simp
+  unfolding cardinal_mul_eq_cardinality_pair
+  by (intro cardinality_eq_if_equipollent mul_equipollent_pair)
 
 end
 

HOTG/Binary_Relations/HOTG_Binary_Relations.thy

@@ -3,8 +3,6 @@ theory HOTG_Binary_Relations
   imports
     HOTG_Binary_Relation_Properties
     HOTG_Transfinite_Recursion
-    Wellfounded_Recursion
-    Binary_Relations_Transitive_Closure
     HOTG_Binary_Relation_Functions
     HOTG_Binary_Relations_Agree
     HOTG_Binary_Relations_Base

HOTG/Binary_Relations/HOTG_Binary_Relations_Extend.thy

@@ -69,6 +69,10 @@ lemma has_inverse_on_set_iff_has_inverse_on_pred_uhint [iff]:
   "has_inverse_on_set A f y \<longleftrightarrow> has_inverse_on (mem_of A) f y"
   by simp
 
+lemma mem_of_repl_eq_has_inverse_on [simp, set_to_HOL_simp]:
+  "mem_of (repl A f) = has_inverse_on A f"
+  by (intro ext) auto
+
 context
   notes set_to_HOL_simp[simp]
 begin

HOTG/Binary_Relations/HOTG_Binary_Relations_Pow.thy

@@ -2,7 +2,9 @@
 \<^marker>\<open>creator "Niklas Krofta"\<close>
 subsection \<open>Power of Relations\<close>
 theory HOTG_Binary_Relations_Pow
-  imports HOTG_Transfinite_Recursion
+  imports
+    HOTG_Transfinite_Recursion
+    Transport.Binary_Relations_Transitive_Closure
 begin
 
 paragraph \<open>Summary\<close>
@@ -31,4 +33,5 @@ lemma rel_powE:
   obtains (rel) "R x y" | (step) m z where "m \<in> n" "rel_pow R m x z" "R z y"
   using assms unfolding rel_pow_iff[where ?n=n] by blast
 
+
 end

HOTG/Cardinals/HOTG_Cardinals_Addition.thy

@@ -14,7 +14,7 @@ text \<open>Cardinal addition is the cardinality of the disjoint union of two se
 We show that cardinal addition is commutative and associative.
 We also derive the connection between set addition and cardinal addition.\<close>
 
-definition "cardinal_add \<kappa> \<mu> \<equiv> |\<kappa> \<Coprod> \<mu>|"
+definition "cardinal_add X Y \<equiv> |X \<Coprod> Y|"
 
 bundle hotg_cardinal_add_syntax begin notation cardinal_add (infixl "\<oplus>" 65) end
 bundle no_hotg_cardinal_add_syntax begin no_notation cardinal_add (infixl "\<oplus>" 65) end
@@ -29,7 +29,7 @@ lemma coprod_equipollent_self_commute: "X \<Coprod> Y \<approx> Y \<Coprod> X"
 
 lemma cardinal_add_comm: "X \<oplus> Y = Y \<oplus> X"
   unfolding cardinal_add_eq_cardinality_coprod
-  by (intro cardinality_eq_if_equipollent cardinality_eq_if_equipollent coprod_equipollent_self_commute)
+  by (intro cardinality_eq_if_equipollent coprod_equipollent_self_commute)
 
 lemma empty_coprod_equipollent_self: "{} \<Coprod> X \<approx> X"
   by (intro equipollentI[where ?f="coprod_rec inr id" and ?g="inr"])
@@ -70,16 +70,9 @@ qed
 corollary cardinality_coprod_equipollent_coprod [iff]: "|X| \<Coprod> |Y| \<approx> X \<Coprod> Y"
   using coprod_equipollent_if_equipollent by auto
 
-lemma bin_union_equipollent_coprod_if_disjoint:
-  assumes "disjoint X Y"
-  shows "X \<union> Y \<approx> X \<Coprod> Y"
-proof -
-  let ?l = "\<lambda>z. if z \<in> X then inl z else inr z"
-  let ?r = "coprod_rec id id"
-  from assms have "bijection_on (mem_of (X \<union> Y)) (mem_of (X \<Coprod> Y)) ?l ?r"
-    by (intro bijection_onI mono_wrt_predI inverse_onI) auto
-  then show ?thesis by blast
-qed
+corollary cardinality_cardinal_add_eq_cardinal_add [simp]: "|X| \<oplus> |Y| = X \<oplus> Y"
+  unfolding cardinal_add_eq_cardinality_coprod
+  by (intro cardinality_eq_if_equipollent cardinality_coprod_equipollent_coprod)
 
 lemma cardinal_add_assoc: "(X \<oplus> Y) \<oplus> Z = X \<oplus> (Y \<oplus> Z)"
 proof -
@@ -93,16 +86,21 @@ proof -
     by (auto intro: cardinality_eq_if_equipollent simp: cardinal_add_eq_cardinality_coprod)
 qed
 
-lemma cardinality_bin_union_eq_cardinal_add_cardinality_if_disjoint:
+lemma bin_union_equipollent_coprod_if_disjoint:
   assumes "disjoint X Y"
-  shows "|X \<union> Y| = |X| \<oplus> |Y|"
+  shows "X \<union> Y \<approx> X \<Coprod> Y"
 proof -
-  from assms have "X \<union> Y \<approx> X \<Coprod> Y" by (intro bin_union_equipollent_coprod_if_disjoint) auto
-  also have "... \<approx> |X| \<Coprod> |Y|" using cardinality_coprod_equipollent_coprod symmetric_equipollent
-    by (blast dest: symmetricD)
-  finally have "X \<union> Y \<approx> |X| \<Coprod> |Y|" .
-  with cardinality_eq_if_equipollent have "|X \<union> Y| = ||X| \<Coprod> |Y||" by auto
-  with cardinal_add_eq_cardinality_coprod show ?thesis by auto
+  let ?l = "\<lambda>z. if z \<in> X then inl z else inr z"
+  let ?r = "coprod_rec id id"
+  from assms have "bijection_on (mem_of (X \<union> Y)) (mem_of (X \<Coprod> Y)) ?l ?r"
+    by (intro bijection_onI mono_wrt_predI inverse_onI) auto
+  then show ?thesis by blast
 qed
 
+corollary cardinality_bin_union_eq_cardinal_add_if_disjoint:
+  assumes "disjoint X Y"
+  shows "|X \<union> Y| = X \<oplus> Y"
+  unfolding cardinal_add_eq_cardinality_coprod using assms
+  by (intro cardinality_eq_if_equipollent bin_union_equipollent_coprod_if_disjoint)
+
 end

HOTG/Cardinals/HOTG_Cardinals_Base.thy

@@ -3,7 +3,7 @@
 section \<open>Cardinals\<close>
 theory HOTG_Cardinals_Base
   imports
-    HOTG_Bounded_Definite_Description
+    Transport.Binary_Relations_Least
     HOTG_Equipollence
     HOTG_Ordinals_Base
 begin
@@ -17,17 +17,19 @@ The cardinality of a set \<open>X\<close> is the smallest ordinal number \<open>
 exists a bijection between \<open>X\<close> and \<open>\<alpha>\<close>.
 Further details can be found in \<^url>\<open>https://en.wikipedia.org/wiki/Cardinal_number\<close>.\<close>
 
-definition "least_wrt_rel R (P :: set \<Rightarrow> bool) = (THE x : P. \<forall>y : P. R x y)"
-
-text\<open>Cardinality is defined as in \<^cite>\<open>ZFC_in_HOL_AFP\<close>,
-\<^url>\<open>https://foss.heptapod.net/isa-afp/afp-devel/-/blob/06458dfa40c7b4aaaeb855a37ae77993cb4c8c18/thys/ZFC_in_HOL/ZFC_Cardinals.thy#L1785\<close>.\<close>
-
 definition "cardinality (X :: set) \<equiv> least_wrt_rel (\<subseteq>) (ordinal \<sqinter> ((\<approx>) X))"
 
 bundle hotg_cardinality_syntax begin notation cardinality ("|_|") end
 bundle no_hotg_cardinality_syntax begin no_notation cardinality ("|_|") end
 unbundle hotg_cardinality_syntax
 
+lemma cardinality_eq_if_equipollent_if_subset_if_ordinal:
+  assumes "ordinal Y"
+  and "\<And>Y'. ordinal Y' \<Longrightarrow> X \<approx> Y' \<Longrightarrow> Y \<subseteq> Y'"
+  and "X \<approx> Y"
+  shows "|X| = Y"
+  unfolding cardinality_def using assms by (intro least_wrt_rel_eq_if_antisymmetric_onI) auto
+
 lemma cardinality_eq_if_equipollent:
   assumes "X \<approx> Y"
   shows "|X| = |Y|"
@@ -44,5 +46,7 @@ lemma cardinality_equipollent_self [iff]: "|X| \<approx> X"
 lemma cardinality_cardinality_eq_cardinality [simp]: "||X|| = |X|"
   by (intro cardinality_eq_if_equipollent cardinality_equipollent_self)
 
+lemma cardinality_zero_eq_zero [simp]: "|0| = 0"
+  by (intro cardinality_eq_if_equipollent_if_subset_if_ordinal) auto
 
 end