feat(HOTG) major upgrade: move concepts to semantical HOL basis

HOTG/Arithmetics/SAddition.thy → HOTG/Arithmetics/HOTG_Addition.thy

@@ -1,10 +1,10 @@
 \<^marker>\<open>creator "Linghan Fang"\<close>
 \<^marker>\<open>creator "Kevin Kappelmann"\<close>
-section \<open>Generalised Addition\<close>
-theory SAddition
+subsection \<open>Generalised Addition\<close>
+theory HOTG_Addition
   imports
-    SLess_Than
-    Ordinals_Base
+    HOTG_Less_Than
+    HOTG_Ordinals_Base
 begin
 
 unbundle
@@ -25,7 +25,7 @@ unbundle
   no_HOL_ascii_syntax
 
 lemma add_eq_bin_union_repl_add: "X + Y = X \<union> {X + y | y \<in> Y}"
-  unfolding add_def by (simp add: transrec_eq)
+  unfolding add_def supply transrec_eq[uhint] by (urule refl)
 
 text \<open>The lift operation from \<^cite>\<open>kirby_set_arithemtics\<close>.\<close>
 
@@ -38,7 +38,7 @@ lemma lift_eq_repl_add: "lift X Y = {X + y | y \<in> Y}"
   using lift_eq_image_add by simp
 
 lemma add_eq_bin_union_lift: "X + Y = X \<union> lift X Y"
-  unfolding lift_eq_image_add by (subst add_eq_bin_union_repl_add) simp
+  unfolding lift_eq_image_add by (urule add_eq_bin_union_repl_add)
 
 corollary lift_subset_add: "lift X Y \<subseteq> X + Y"
   using add_eq_bin_union_lift by auto
@@ -195,11 +195,11 @@ proof (rule injectiveI)
     case (mem Y)
     {
       fix U V u assume uvassms: "U \<in> {Y, Z}" "V \<in> {Y, Z}" "U \<noteq> V" "u \<in> U"
-      with mem have "X + u \<in> lift X V" by (auto simp: lift_eq_repl_add)
+      with mem have "X + u \<in> lift X V" by (auto simp: lift_eq_repl_add mem_insert_iff)
       then obtain v where "v \<in> V" "X + u = X + v" using lift_eq_repl_add by auto
       then have "X \<union> lift X u  = X \<union> lift X v" by (simp add: add_eq_bin_union_lift)
       with disjoint_lift_self_right have "lift X u = lift X v" by blast
-      with uvassms \<open>v \<in> V\<close> mem.IH have "u \<in> V" by auto
+      with uvassms \<open>v \<in> V\<close> mem.IH have "u \<in> V" by (auto simp: mem_insert_iff)
     }
     then show ?case by blast
   qed
@@ -236,17 +236,17 @@ corollary add_mem_add_iff_mem_right [iff]: "X + Y \<in> X + Z \<longleftrightarr
 
 text \<open>We next prove some monotonicity lemmas for @{term lift} and @{term "(+)"}.\<close>
 
-lemma mono_lift: "((\<subseteq>) \<Rrightarrow>\<^sub>m (\<subseteq>)) (lift X)"
-  by (intro dep_mono_wrt_relI) (auto simp: lift_eq_repl_add)
+lemma mono_lift: "((\<subseteq>) \<Rightarrow> (\<subseteq>)) (lift X)"
+  by (intro mono_wrt_relI) (auto simp: lift_eq_repl_add)
 
 lemma subset_if_lift_subset_lift: "lift X Y \<subseteq> lift X Z \<Longrightarrow> Y \<subseteq> Z"
   by (auto simp: lift_eq_repl_add)
 
 corollary lift_subset_lift_iff_subset: "lift X Y \<subseteq> lift X Z \<longleftrightarrow> Y \<subseteq> Z"
   using subset_if_lift_subset_lift mono_lift[of X] by (auto del: subsetI)
 
-lemma mono_add: "((\<subseteq>) \<Rrightarrow>\<^sub>m (\<subseteq>)) ((+) X)"
-proof (rule dep_mono_wrt_relI)
+lemma mono_add: "((\<subseteq>) \<Rightarrow> (\<subseteq>)) ((+) X)"
+proof (rule mono_wrt_relI)
   fix Y Z assume "Y \<subseteq> Z"
   then have "lift X Y \<subseteq> lift X Z" by (simp only: lift_subset_lift_iff_subset)
   then show "X + Y \<subseteq> X + Z" by (auto simp: add_eq_bin_union_lift)
@@ -356,3 +356,4 @@ lemma lt_if_add_lt: "X + Y < Z \<Longrightarrow> X < Z"
 
 
 end
+

HOTG/Arithmetics/SArithmetics.thy → HOTG/Arithmetics/HOTG_Arithmetics.thy

@@ -1,9 +1,10 @@
 \<^marker>\<open>creator "Kevin Kappelmann"\<close>
 section \<open>Arithmetics\<close>
-theory SArithmetics
+theory HOTG_Arithmetics
   imports
-    SAddition
-    SMultiplication
+    HOTG_Addition
+    HOTG_Multiplication
+    HOTG_Arithmetics_Cardinal_Arithmetics
 begin
 
 

HOTG/Arithmetics/HOTG_Arithmetics_Cardinal_Arithmetics.thy

@@ -0,0 +1,32 @@
+\<^marker>\<open>creator "Linghan Fang"\<close>
+\<^marker>\<open>creator "Kevin Kappelmann"\<close>
+subsection \<open>Compatibility of Set Arithmetics and Cardinal Arithmetics\<close>
+theory HOTG_Arithmetics_Cardinal_Arithmetics
+  imports
+    HOTG_Cardinals_Addition
+    HOTG_Addition
+begin
+
+unbundle no_HOL_groups_syntax
+
+lemma cardinality_lift_eq_cardinality_right [simp]: "|lift X Y| = |Y|"
+proof (intro cardinality_eq_if_equipollent equipollentI)
+  let ?f = "\<lambda>z. (THE y : Y. z = X + y)"
+  let ?g = "((+) X)"
+  from injective_on_if_inverse_on show "bijection_on (lift X Y) Y ?f ?g"
+    by (urule bijection_onI dep_mono_wrt_predI where chained = insert)+
+    (auto intro: pred_btheI[of "\<lambda>x. x \<in> Y"] simp: lift_eq_repl_add mem_of_eq)
+qed
+
+text\<open>The next theorem shows that set addition is compatible with cardinality addition.\<close>
+
+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)
+
+text\<open>A similar theorem shows that set multiplication is compatible with cardinality multiplication,
+but it is not proven here. See
+\<^url>\<open>https://foss.heptapod.net/isa-afp/afp-devel/-/blob/06458dfa40c7b4aaaeb855a37ae77993cb4c8c18/thys/ZFC_in_HOL/Kirby.thy#L1431\<close>.\<close>
+
+end
+

HOTG/Arithmetics/SMultiplication.thy → HOTG/Arithmetics/HOTG_Multiplication.thy

@@ -1,9 +1,9 @@
 \<^marker>\<open>creator "Linghan Fang"\<close>
 \<^marker>\<open>creator "Kevin Kappelmann"\<close>
-section \<open>Generalised Multiplication\<close>
-theory SMultiplication
+subsection \<open>Generalised Multiplication\<close>
+theory HOTG_Multiplication
   imports
-    SAddition
+    HOTG_Addition
 begin
 
 paragraph \<open>Summary\<close>
@@ -18,7 +18,7 @@ bundle no_hotg_mul_syntax begin no_notation mul (infixl "*" 70) end
 unbundle hotg_mul_syntax
 
 lemma mul_eq_idx_union_lift_mul: "X * Y = (\<Union>y \<in> Y. lift (X * y) X)"
-  by (simp add: mul_def transrec_eq)
+  unfolding mul_def by (urule transrec_eq)
 
 corollary mul_eq_idx_union_repl_mul_add: "X * Y = (\<Union>y \<in> Y. {X * y + x | x \<in> X})"
   using mul_eq_idx_union_lift_mul[of X Y] lift_eq_repl_add by simp
@@ -178,19 +178,23 @@ next
   next
     case False
     then show ?thesis sorry
-        qed
-      qed
+  qed
+qed
 
 paragraph\<open>Lemma 4.7 from \<^cite>\<open>kirby_set_arithemtics\<close>\<close>
 
 text\<open>For the next missing proofs, see
 \<^url>\<open>https://foss.heptapod.net/isa-afp/afp-devel/-/blob/06458dfa40c7b4aaaeb855a37ae77993cb4c8c18/thys/ZFC_in_HOL/Kirby.thy#L1166\<close>.\<close>
 
-lemma subset_if_mul_add_subset_mul_add: assumes "R < A" "S < A" "A * X + R \<subseteq> A * Y + S"
+(* lemma subset_if_mul_add_subset_mul_add_if_lt:
+  assumes "R < A" "S < A"
+  and "A * X + R \<subseteq> A * Y + S"
   shows "X \<subseteq> Y"
-  sorry
+  sorry *)
 
-lemma eq_if_mul_add_eq_mul_add: assumes "R < A" "S < A" "A * X + R = A * Y + S"
+lemma eq_if_mul_add_eq_mul_add_if_lt:
+  assumes "R < A" "S < A"
+  and "A * X + R = A * Y + S"
   shows "X = Y" "R = S"
   sorry
 
@@ -205,7 +209,7 @@ proof (rule eqI)
   from asm obtain rr where RR: "x = A * Y + rr" "rr \<in> mem_trans_closure A"
     using lift_eq_repl_add by auto
   with R have "A * X + r = A * Y + rr" "r < A" "rr < A" by (auto simp: lt_iff_mem_trans_closure)
-  then have "X = Y" "r = rr" using eq_if_mul_add_eq_mul_add[of r _ rr X _] by auto
+  then have "X = Y" "r = rr" using eq_if_mul_add_eq_mul_add_if_lt[of r _ rr X _] by auto
   then show "x \<in> 0" by (simp add: assms)
 qed simp