Merge pull request #4 from kappelmann/nkrofta-master

Tuned PR 3

HOTG/Arithmetics/HOTG_Multiplication.thy

@@ -4,6 +4,7 @@ subsection \<open>Generalised Multiplication\<close>
 theory HOTG_Multiplication
   imports
     HOTG_Addition
+    HOTG_Additively_Divides
 begin
 
 paragraph \<open>Summary\<close>
@@ -153,31 +154,76 @@ 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: assumes "A * X = A * Y + B" "B < A"
-  shows "B = 0"
-proof (cases "A = 0 \<or> X = 0")
-  case True
-  with assms show ?thesis
-  proof (cases "A = 0")
-    case False
-    then have "A * Y + B = 0" using  \<open>A = 0 \<or> X = 0\<close> assms by auto
-    then show ?thesis
-      by (auto simp: add_eq_zero_iff_and_eq_zero[of "A * Y" "B"])
-  qed auto
-next
-  case False
-  then have "A \<noteq> 0" "X \<noteq> 0" by auto
+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
+  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"
+    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'"
+      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'"
+    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_or_additively_divides_if_add_eq_add by blast
   then show ?thesis
-  proof (cases"Y = 0")
-    case True
-    then show ?thesis sorry
+  proof cases
+    case 1
+    then obtain e where "A * u = A * Y + e" by (auto elim!: additively_dividesE)
+    then have "A * Y + d = A * Y + e + c" using \<open>p = A * Y + d\<close> \<open>p = A * u + c\<close> by auto
+    then have "d = e + c" using add_assoc add_eq_add_if_eq_right by auto
+    then have "e \<le> d" using le_self_add by auto
+    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 \<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 False
-    then show ?thesis sorry
+    case 2
+    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 \<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 eq_zero_if_lt_if_mul_eq_mul_add:
+  assumes "A * X = A * Y + B" "B < A"
+  shows "B = 0"
+using assms
+proof (induction X arbitrary: Y B rule: lt_induct)
+  case (step X) show ?case
+  proof (rule ccontr)
+    assume "B \<noteq> 0"
+    then have "0 < B" 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
 
@@ -196,7 +242,22 @@ 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
+proof (induction X rule: lt_induct)
+  case (step X)
+  have "X \<noteq> 0"
+  proof
+    assume "X = 0"
+    then have "A * Y + S < A" sorry
+    show "False" sorry
+  qed
+  {
+    case 1
+    then show ?case sorry
+  next
+    case 2
+    then show ?case sorry
+  }
+qed
 
 lemma bin_inter_lift_mul_mem_trans_closure_lift_mul_mem_trans_closure_eq_zero:
   assumes "X \<noteq> Y"

HOTG/Mem_Transitive_Closure/HOTG_Mem_Transitive_Closure.thy

@@ -83,6 +83,12 @@ proof (induction Y)
     by (cases "Y = {}") (auto simp add: mem_trans_closure_eq_bin_union_idx_union[of Y])
 qed
 
+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 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"
   shows "mem_trans_closure X = X"

HOTG/Orders/HOTG_Additively_Divides.thy

@@ -0,0 +1,98 @@
+\<^marker>\<open>creator "Niklas Krofta"\<close>
+theory HOTG_Additively_Divides
+  imports
+    HOTG_Addition
+    Transport.Functions_Base
+begin
+
+unbundle no_HOL_groups_syntax
+
+definition "additively_divides x y \<equiv> has_inverse ((+) x) y"
+
+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]:
+  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"
+  using add_eq_bin_union_lift by force
+
+lemma le_if_additively_divides: "x \<unlhd> y \<Longrightarrow> x \<le> y"
+  using le_self_add by auto
+
+lemma reflexive_additively_divides: "reflexive (\<unlhd>)"
+  using add_zero_eq_self by blast
+
+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"
+  using add_assoc by force
+
+corollary transitive_additively_divides: "transitive (\<unlhd>)"
+  using additively_divides_trans by auto
+
+corollary preorder_additively_divides: "preorder (\<unlhd>)"
+  using reflexive_additively_divides transitive_additively_divides by blast
+
+corollary partial_order_additively_divides: "partial_order (\<unlhd>)"
+  using preorder_additively_divides antisymmetric_additively_divides by auto
+
+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)"
+  have "\<forall>z. a + x \<noteq> c + z" for x
+  proof (induction x rule: mem_induction)
+    case (mem x) show ?case
+    proof (cases "x = 0")
+      case False show ?thesis
+      proof (rule ccontr)
+        assume "\<not>(\<forall>z. a + x \<noteq> c + z)"
+        then obtain z where hz: "a + x = c + z" 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" 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
+          have "lift c z \<subseteq> lift a x"
+          proof (rule ccontr)
+            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 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
+          ultimately have "lift c z = 0" by auto
+          then show "False" using lift_eq_repl_add \<open>z \<noteq> 0\<close> by auto
+        next
+          case \<lambda>
+          then show "False" using lift_eq_repl_add mem.IH \<open>v \<in> x\<close> by auto
+        qed
+      qed
+    qed (use ac_incomparable in auto)
+  qed
+  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,19 @@ 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
+
 lemma lt_if_lt_if_mem [trans]:
   assumes "x \<in> X"
   and "X < Y"
@@ -180,4 +193,49 @@ local_setup \<open>
   }
 \<close>
 
+lemma lt_minimal_set_witnessE:
+  assumes "P a"
+  obtains m where "P m" "\<And>b. b < m \<Longrightarrow> \<not>(P b)"
+proof -
+  have "\<exists>m : P. \<forall>b. b < m \<longrightarrow> \<not>(P b)"
+  proof (rule ccontr)
+    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))"
+        then obtain x where "x \<le> X" "P x" 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
+        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 le_minimal_set_witnessE:
+  assumes "P a"
+  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
+  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)"
+  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 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,6 +3,7 @@ theory HOTG_Orders
   imports
     HOTG_Less_Than
     HOTG_Well_Orders
+    HOTG_Additively_Divides
 begin
 
 

HOTG/Ordinals/HOTG_Ordinals.thy

@@ -3,6 +3,8 @@
 theory HOTG_Ordinals
   imports
     HOTG_Ordinals_Base
+    HOTG_Ordinals_Max
+    HOTG_Ranks
 begin