feat(*) fine-tuning

HOTG/Arithmetics/HOTG_Multiplication.thy

@@ -3,8 +3,9 @@
 subsection \<open>Generalised Multiplication\<close>
 theory HOTG_Multiplication
   imports
-    HOTG_Addition HOTG_Additive_Order
-begin                 
+    HOTG_Addition
+    HOTG_Additively_Divides
+begin
 
 paragraph \<open>Summary\<close>
 text \<open>Translation of generalised set multiplication for sets from \<^cite>\<open>kirby_set_arithemtics\<close>
@@ -153,41 +154,37 @@ qed simp
 
 paragraph\<open>Lemma 4.6 from \<^cite>\<open>kirby_set_arithemtics\<close>\<close>
 
-text\<open>The next lemma is rather complex and remains incomplete as of now. A complete proof
-can be found in \<^cite>\<open>kirby_set_arithemtics\<close> and
-\<^url>\<open>https://foss.heptapod.net/isa-afp/afp-devel/-/blob/06458dfa40c7b4aaaeb855a37ae77993cb4c8c18/thys/ZFC_in_HOL/Kirby.thy#L992\<close>.\<close>
-
-lemma zero_if_multi_eq_multi_add_aux:
+lemma mul_eq_mul_add_ltE:
   assumes "A * X = A * Y + B" "0 < B" "B < A"
   obtains u f where "A * Y = A * u + f" "0 < f" "f < A" "u < X"
 proof -
   define \<phi> where "\<phi> x \<longleftrightarrow> (\<exists>r. 0 < r \<and> r < A \<and> A * x = A * Y + r)" for x
-  have "\<phi> X" using \<phi>_def assms by auto
-  then obtain X' where "\<phi> X'" "X' \<le> X" and X'_min: "\<And>x. x < X' \<Longrightarrow> \<not> \<phi> x" 
-    using minimal_satisfier_le by auto
-  from \<open>\<phi> X'\<close> obtain B' where "0 < B'" "B' < A" "A * X' = A * Y + B'" using \<phi>_def by auto
+  from assms have "\<phi> X" unfolding \<phi>_def by auto
+  then obtain X' where "\<phi> X'" "X' \<le> X" and X'_min: "\<And>x. x < X' \<Longrightarrow> \<not> \<phi> x"
+    using le_minimal_set_witnessE by auto
+  from \<open>\<phi> X'\<close> obtain B' where "0 < B'" "B' < A" "A * X' = A * Y + B'" unfolding \<phi>_def by auto
   then have "A * Y < A * X'" by auto
   then obtain p where "p \<in> A * X'" "A * Y \<le> p" by (auto elim: lt_mem_leE)
-  from \<open>p \<in> A * X'\<close> obtain u c where "u \<in> X'" "c \<in> A" "p = A * u + c" 
+  from \<open>p \<in> A * X'\<close> obtain u c where "u \<in> X'" "c \<in> A" "p = A * u + c"
     using mul_eq_idx_union_repl_mul_add[of A X'] by auto
   have "A * u \<noteq> A * Y"
   proof
     assume "A * u = A * Y"
     moreover have "lift (A * u) A \<subseteq> A * X'" using \<open>u \<in> X'\<close> mul_eq_idx_union_lift_mul by fast
     ultimately have "lift (A * Y) A \<subseteq> A * X'" by auto
-    then have "lift (A * Y) A \<subseteq> A * Y \<union> lift (A * Y) B'" 
+    then have "lift (A * Y) A \<subseteq> A * Y \<union> lift (A * Y) B'"
       using \<open>A * X' = A * Y + B'\<close> add_eq_bin_union_lift by blast
     then have "lift (A * Y) A \<subseteq> lift (A * Y) B'"
       using disjoint_lift_self_right disjoint_iff_all_not_mem by blast
     then have "A \<subseteq> B'" using subset_if_lift_subset_lift by blast
     then show "False" using \<open>B' < A\<close> not_subset_if_lt by blast
   qed
   from \<open>A * Y \<le> p\<close> have "p \<notin> A * Y" using lt_if_mem not_lt_if_le by auto
-  then have "p \<in> lift (A * Y) B'" 
+  then have "p \<in> lift (A * Y) B'"
     using \<open>p \<in> A * X'\<close> \<open>A * X' = A * Y + B'\<close> add_eq_bin_union_lift by auto
   then obtain d where "d \<in> B'" "p = A * Y + d" using lift_eq_repl_add by auto
-  then consider "A * Y \<unlhd> A * u" | "A * u \<unlhd> A * Y" 
-    using \<open>p = A * u + c\<close> additively_divides_if_sums_equal by blast 
+  then consider "A * Y \<unlhd> A * u" | "A * u \<unlhd> A * Y"
+    using \<open>p = A * u + c\<close> additively_divides_or_additively_divides_if_add_eq_add by blast
   then show ?thesis
   proof cases
     case 1
@@ -198,36 +195,34 @@ proof -
     also have "d < A" using \<open>d \<in> B'\<close> lt_if_mem \<open>B' < A\<close> lt_trans by blast
     finally have "e < A" using lt_if_le_if_lt by auto
     have "e \<noteq> 0" using \<open>A * u = A * Y + e\<close> add_zero_eq_self \<open>A * u \<noteq> A * Y\<close> by force
-    then have "\<phi> u" using \<phi>_def \<open>e < A\<close> \<open>A * u = A * Y + e\<close> by blast
+    then have "\<phi> u" using \<open>e < A\<close> \<open>A * u = A * Y + e\<close> unfolding \<phi>_def by blast
     then have "False" using X'_min \<open>u \<in> X'\<close> lt_if_mem by auto
     then show ?thesis by blast
   next
     case 2
-    then obtain f where "A * Y = A * u + f" by (auto elim!: additively_dividesE) 
+    then obtain f where "A * Y = A * u + f" by fast
     then have "A * u + f + d = A * u + c" using \<open>p = A * Y + d\<close> \<open>p = A * u + c\<close> by auto
     then have "f + d = c" using add_assoc add_eq_add_if_eq_right by auto
-    then have "f < A" using le_self_add \<open>c \<in> A\<close> lt_if_mem_if_le by auto
+    then have "f < A" using \<open>c \<in> A\<close> lt_if_mem_if_le by auto
     have "f \<noteq> 0" using \<open>A * Y = A * u + f\<close> add_zero_eq_self \<open>A * u \<noteq> A * Y\<close> by force
     have "u < X" using \<open>u \<in> X'\<close> lt_if_mem \<open>X' \<le> X\<close> lt_if_le_if_lt by blast
     then show ?thesis using that \<open>A * Y = A * u + f\<close> \<open>f \<noteq> 0\<close> \<open>f < A\<close> \<open>u < X\<close> by auto
   qed
 qed
 
-lemma zero_if_multi_eq_multi_add:
+lemma eq_zero_if_lt_if_mul_eq_mul_add:
   assumes "A * X = A * Y + B" "B < A"
   shows "B = 0"
-  using assms 
+using assms
 proof (induction X arbitrary: Y B rule: lt_induct)
-  case (step X)
-  show ?case
+  case (step X) show ?case
   proof (rule ccontr)
     assume "B \<noteq> 0"
     then have "0 < B" by auto
-    from zero_if_multi_eq_multi_add_aux[OF step(2) \<open>0 < B\<close> \<open>B < A\<close>] obtain u f where 
-      "A * Y = A * u + f" "0 < f" "f < A" "u < X" by auto
-    from zero_if_multi_eq_multi_add_aux[OF this(1, 2, 3)] obtain v g where
-      "A * u = A * v + g" "0 < g" "g < A" "v < Y" by auto
-    then have "g = 0" using step.IH \<open>u < X\<close> by auto
+    with mul_eq_mul_add_ltE step obtain u f where "A * Y = A * u + f" "0 < f" "f < A" "u < X"
+      by blast
+    with mul_eq_mul_add_ltE obtain v g where "A * u = A * v + g" "0 < g" "g < A" "v < Y" by blast
+    with step.IH have "g = 0" using \<open>u < X\<close> by auto
     then show "False" using \<open>0 < g\<close> by auto
   qed
 qed

HOTG/Mem_Transitive_Closure/HOTG_Mem_Transitive_Closure.thy

@@ -83,11 +83,11 @@ proof (induction Y)
     by (cases "Y = {}") (auto simp add: mem_trans_closure_eq_bin_union_idx_union[of Y])
 qed
 
-lemma mem_trans_closures_subset_if_subset:
+lemma mem_trans_closure_subset_mem_trans_closure_if_subset:
   assumes "Y \<subseteq> X"
   shows "mem_trans_closure Y \<subseteq> mem_trans_closure X"
-    using mem_trans_closure_le_if_le_if_mem_trans_closed[OF mem_trans_closed_mem_trans_closure]
-    subset_mem_trans_closure_self[of X] assms by blast
+  using assms subset_mem_trans_closure_self mem_trans_closed_mem_trans_closure
+  by (intro mem_trans_closure_le_if_le_if_mem_trans_closed) auto
 
 lemma mem_trans_closure_eq_self_if_mem_trans_closed [simp]:
   assumes "mem_trans_closed X"

HOTG/Orders/HOTG_Additive_Order.thy → HOTG/Orders/HOTG_Additively_Divides.thy

@@ -1,25 +1,29 @@
-theory HOTG_Additive_Order
-  imports HOTG_Addition
+\<^marker>\<open>creator "Niklas Krofta"\<close>
+theory HOTG_Additively_Divides
+  imports
+    HOTG_Addition
+    Transport.Functions_Base
 begin
 
-definition additively_divides :: "set \<Rightarrow> set \<Rightarrow> bool" where
-"additively_divides x y \<longleftrightarrow> (\<exists>d. x + d = y)"
+unbundle no_HOL_groups_syntax
 
-bundle hotg_additive_order_syntax begin notation additively_divides (infix "\<unlhd>" 50) end
-bundle no_hotg_additive_order_syntax begin no_notation additively_divides (infix "\<unlhd>" 50) end
-unbundle hotg_additive_order_syntax
+definition "additively_divides x y \<equiv> has_inverse ((+) x) y"
 
-lemma additively_dividesI[intro]:
+bundle hotg_additively_divides_syntax begin notation additively_divides (infix "\<unlhd>" 50) end
+bundle no_hotg_additively_divides_syntax begin no_notation additively_divides (infix "\<unlhd>" 50) end
+unbundle hotg_additively_divides_syntax
+
+lemma additively_dividesI [intro]:
   assumes "x + d = y"
   shows "x \<unlhd> y"
   unfolding additively_divides_def using assms by auto
 
-lemma additively_dividesE[elim]:
+lemma additively_dividesE [elim]:
   assumes "x \<unlhd> y"
   obtains d where "x + d = y"
   using assms unfolding additively_divides_def by auto
 
-lemma subset_if_additively_divides: "x \<unlhd> y \<Longrightarrow> x \<subseteq> y" 
+lemma subset_if_additively_divides: "x \<unlhd> y \<Longrightarrow> x \<subseteq> y"
   using add_eq_bin_union_lift by force
 
 lemma le_if_additively_divides: "x \<unlhd> y \<Longrightarrow> x \<le> y"
@@ -31,7 +35,7 @@ lemma reflexive_additively_divides: "reflexive (\<unlhd>)"
 lemma antisymmetric_additively_divides: "antisymmetric (\<unlhd>)"
   using subset_if_additively_divides by auto
 
-lemma additively_divides_trans[trans]: "x \<unlhd> y \<Longrightarrow> y \<unlhd> z \<Longrightarrow> x \<unlhd> z"
+lemma additively_divides_trans [trans]: "x \<unlhd> y \<Longrightarrow> y \<unlhd> z \<Longrightarrow> x \<unlhd> z"
   using add_assoc by force
 
 corollary transitive_additively_divides: "transitive (\<unlhd>)"
@@ -40,41 +44,36 @@ corollary transitive_additively_divides: "transitive (\<unlhd>)"
 corollary preorder_additively_divides: "preorder (\<unlhd>)"
   using reflexive_additively_divides transitive_additively_divides by blast
 
-corollary additively_divides_partial_order: "partial_order (\<unlhd>)"
+corollary partial_order_additively_divides: "partial_order (\<unlhd>)"
   using preorder_additively_divides antisymmetric_additively_divides by auto
 
-lemma additively_divides_if_sums_equal:
+lemma additively_divides_or_additively_divides_if_add_eq_add:
   assumes "a + b = c + d"
   shows "a \<unlhd> c \<or> c \<unlhd> a"
 proof (rule ccontr)
-  assume ac_incomparable: "\<not> (a \<unlhd> c \<or> c \<unlhd> a)"
+  assume ac_incomparable: "\<not>(a \<unlhd> c \<or> c \<unlhd> a)"
   have "\<forall>z. a + x \<noteq> c + z" for x
   proof (induction x rule: mem_induction)
-    case (mem x)
-    show ?case
+    case (mem x) show ?case
     proof (cases "x = 0")
-      case True
-      then show ?thesis using ac_incomparable by auto
-    next
-      case False
-      show ?thesis
+      case False show ?thesis
       proof (rule ccontr)
-        assume "\<not> (\<forall>z. a + x \<noteq> c + z)"
+        assume "\<not>(\<forall>z. a + x \<noteq> c + z)"
         then obtain z where hz: "a + x = c + z" by auto
-        then have "z \<noteq> 0" using add_zero_eq_self ac_incomparable by auto
+        with ac_incomparable have "z \<noteq> 0" by auto
         from \<open>x \<noteq> 0\<close> obtain v where "v \<in> x" by auto
-        then have "a + v \<in> c + z" unfolding hz[symmetric] using add_eq_bin_union_repl_add[of a x] by auto
+        then have "a + v \<in> c + z" using hz add_eq_bin_union_repl_add[where ?Y=x] by auto
         then consider (c) "a + v \<in> c" | (\<lambda>) "a + v \<in> lift c z" unfolding add_eq_bin_union_lift by auto
         then show "False"
-        proof (cases)
-          case c                             
+        proof cases
+          case c
           have "lift c z \<subseteq> lift a x"
           proof (rule ccontr)
-            assume "\<not> lift c z \<subseteq> lift a x"
+            assume "\<not>(lift c z \<subseteq> lift a x)"
             then have "\<exists>z' : lift c z.  z' \<in> a" using hz unfolding add_eq_bin_union_lift by auto
             then obtain w where "c + w \<in> a" using lift_eq_repl_add by auto
             then have "c + w \<in> a + v" using add_eq_bin_union_lift by auto
-            moreover have "a + v \<in> c + w" using add_eq_bin_union_lift[of c w] using c by auto
+            moreover from c have "a + v \<in> c + w" using add_eq_bin_union_lift[where ?Y=w] by auto
             ultimately show "False" using not_mem_if_mem by auto
           qed
           moreover from mem have "lift a x \<inter> lift c z = 0" for z using lift_eq_repl_add by auto
@@ -85,9 +84,15 @@ proof (rule ccontr)
           then show "False" using lift_eq_repl_add mem.IH \<open>v \<in> x\<close> by auto
         qed
       qed
-    qed
+    qed (use ac_incomparable in auto)
   qed
-  then show "False" using assms by auto
+  with assms show "False" by auto
 qed
 
+lemma additively_divides_if_add_eq_addE:
+  assumes "a + b = c + d"
+  obtains (left_divides) "a \<unlhd> c" | (right_divides) "c \<unlhd> a"
+  using assms additively_divides_or_additively_divides_if_add_eq_add by blast
+
+
 end

HOTG/Orders/HOTG_Less_Than.thy

@@ -42,6 +42,16 @@ lemma mem_trans_closure_if_lt:
   shows "X \<in> mem_trans_closure Y"
   using assms unfolding lt_iff_mem_trans_closure by simp
 
+lemma not_subset_if_lt:
+  assumes "A < B"
+  shows "\<not>(B \<subseteq> A)"
+proof
+  assume "B \<subseteq> A"
+  with mem_trans_closure_if_lt have "A \<in> mem_trans_closure A"
+    using mem_trans_closure_subset_mem_trans_closure_if_subset assms by blast
+  then show "False" using not_mem_mem_trans_closure_self by blast
+qed
+
 corollary mem_if_lt_if_mem_trans_closed: "mem_trans_closed S \<Longrightarrow> X < S \<Longrightarrow> X \<in> S"
   using mem_trans_closure_if_lt mem_trans_closure_le_if_le_if_mem_trans_closed by blast
 
@@ -183,58 +193,49 @@ local_setup \<open>
   }
 \<close>
 
-lemma minimal_satisfier:
+lemma lt_minimal_set_witnessE:
   assumes "P a"
-  obtains m where "P m" "\<And>b. b < m \<Longrightarrow> \<not> P b"
+  obtains m where "P m" "\<And>b. b < m \<Longrightarrow> \<not>(P b)"
 proof -
-  have "\<exists>m. P m \<and> (\<forall>b. b < m \<longrightarrow> \<not> P b)"
+  have "\<exists>m : P. \<forall>b. b < m \<longrightarrow> \<not>(P b)"
   proof (rule ccontr)
-    assume no_minimal: "\<nexists>m. P m \<and> (\<forall>b. b < m \<longrightarrow> \<not> P b)"
-    have "\<forall>x. x \<le> X \<longrightarrow> \<not> P x" for X
+    assume no_minimal: "\<not>(\<exists>m : P. \<forall>b. b < m \<longrightarrow> \<not>(P b))"
+    have "\<forall>x. x \<le> X \<longrightarrow> \<not>(P x)" for X
     proof (induction X rule: mem_induction)
       case (mem X) show ?case
       proof (rule ccontr)
-        assume "\<not> (\<forall>x. x \<le> X \<longrightarrow> \<not> P x)"
+        assume "\<not>(\<forall>x. x \<le> X \<longrightarrow> \<not>(P x))"
         then obtain x where "x \<le> X" "P x" by auto
-        then obtain y where "y < x" "P y" using no_minimal by auto
+        with no_minimal obtain y where "y < x" "P y" by auto
         then obtain z where "z \<in> X" "y \<le> z" using lt_if_le_if_lt \<open>x \<le> X\<close> lt_mem_leE by blast
-        then show "False" using mem.IH \<open>P y\<close> by auto
+        with mem.IH \<open>P y\<close> show "False" by auto
       qed
     qed
     then show "False" using \<open>P a\<close> by auto
   qed
   then show ?thesis using that by blast
 qed
 
-corollary minimal_satisfier_le:
+corollary le_minimal_set_witnessE:
   assumes "P a"
-  obtains m where "P m" "m \<le> a" "\<And>b. b < m \<Longrightarrow> \<not> P b"
+  obtains m where "P m" "m \<le> a" "\<And>b. b < m \<Longrightarrow> \<not>(P b)"
 proof -
   define Q where "Q x \<longleftrightarrow> P x \<and> x \<le> a" for x
-  have "Q a" using assms Q_def by auto
-  then obtain m where "Q m" "\<And>b. b < m \<Longrightarrow> \<not> Q b" using minimal_satisfier by auto
-  then have "\<not> P b" if "b < m" for b using Q_def lt_if_lt_if_le that le_if_lt by auto
-  then show ?thesis using that \<open>Q m\<close> Q_def by auto
+  from assms have "Q a" unfolding Q_def by auto
+  then obtain m where "Q m" "\<And>b. b < m \<Longrightarrow> \<not>(Q b)" using lt_minimal_set_witnessE by auto
+  moreover then have "\<not>(P b)" if "b < m" for b
+    using that lt_if_lt_if_le le_if_lt unfolding Q_def by auto
+  ultimately show ?thesis using that unfolding Q_def by auto
 qed
 
 corollary lt_induct [case_names step]:
-  assumes "\<And>X. \<lbrakk>\<And>x. x < X \<Longrightarrow> P x\<rbrakk> \<Longrightarrow> P X"
+  assumes "\<And>X. \<lbrakk>\<And>x. x < X \<Longrightarrow>(P x)\<rbrakk> \<Longrightarrow>(P X)"
   shows "P X"
 proof (rule ccontr)
-  assume "\<not> P X"
-  then obtain m where "\<not> P m" "\<And>y. y < m \<Longrightarrow> P y" 
-    using minimal_satisfier[where P="\<lambda>x. \<not> P x"] by auto
-  then show "False" using assms by auto
-qed
-
-lemma not_subset_if_lt:
-  assumes "A < B"
-  shows "\<not> B \<subseteq> A"
-proof
-  assume "B \<subseteq> A"
-  then have "A \<in> mem_trans_closure A" 
-    using mem_trans_closures_subset_if_subset assms mem_trans_closure_if_lt by blast
-  then show "False" using not_mem_mem_trans_closure_self by blast
+  assume "\<not>(P X)"
+  then obtain m where "\<not>(P m)" "\<And>y. y < m \<Longrightarrow> P y"
+    using lt_minimal_set_witnessE[where P="\<lambda>x. \<not>(P x)"] by auto
+  with assms show "False" by auto
 qed
 
 end

HOTG/Orders/HOTG_Orders.thy

@@ -3,7 +3,7 @@ theory HOTG_Orders
   imports
     HOTG_Less_Than
     HOTG_Well_Orders
-    HOTG_Additive_Order
+    HOTG_Additively_Divides
 begin
 
 

HOTG/Ordinals/HOTG_Ordinals.thy

@@ -3,7 +3,7 @@
 theory HOTG_Ordinals
   imports
     HOTG_Ordinals_Base
-    HOTG_Ordinals_Min_Max
+    HOTG_Ordinals_Max
     HOTG_Ranks
 begin