feat(HOTG) tuning of well-founded recursion theories

HOTG/Arithmetics/HOTG_Addition.thy

@@ -3,7 +3,6 @@
 subsection \<open>Generalised Addition\<close>
 theory HOTG_Addition
   imports
-    HOTG_Less_Than
     HOTG_Ordinals_Base
     HOTG_Transfinite_Recursion
 begin
@@ -17,7 +16,7 @@ text \<open>Translation of generalised set addition from \<^cite>\<open>kirby_se
 \<^cite>\<open>ZFC_in_HOL_AFP\<close>. Note that general set addition is associative and
 monotone and injective in the second argument, but it is not commutative (not proven here).\<close>
 
-definition "add X \<equiv> transrec (\<lambda>addX Y. X \<union> image addX Y)"
+definition "add X \<equiv> transfrec (\<lambda>addX Y. X \<union> image addX Y)"
 
 bundle hotg_add_syntax begin notation add (infixl "+" 65) end
 bundle no_hotg_add_syntax begin no_notation add (infixl "+" 65) end
@@ -26,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 supply transrec_eq[uhint] by (urule refl)
+  unfolding add_def supply transfrec_eq[uhint] by (urule refl)
 
 text \<open>The lift operation from \<^cite>\<open>kirby_set_arithemtics\<close>.\<close>
 

HOTG/Arithmetics/HOTG_Arithmetics_Cardinal_Arithmetics.thy

@@ -6,6 +6,7 @@ theory HOTG_Arithmetics_Cardinal_Arithmetics
     HOTG_Cardinals_Addition
     HOTG_Cardinals_Multiplication
     HOTG_Addition
+    HOTG_Functions_Injective
     HOTG_Multiplication
 begin
 
@@ -23,53 +24,36 @@ 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)
 
-text\<open>A similar theorem shows that set multiplication is compatible with cardinality multiplication.\<close>
+text\<open>The next theorems show that set multiplication is compatible with cardinality multiplication.\<close>
 
-lemma bijection_onto_image_if_injective_on:
-  assumes "\<And>x x'. x \<in> X \<Longrightarrow> x' \<in> X \<Longrightarrow> f x = f x' \<Longrightarrow> x = x'"
-  shows "\<exists>g. (bijection_on X (image f X) f g)"
-proof
-  define P where "P y x \<longleftrightarrow> x \<in> X \<and> f x = y" for y x
-  let ?g = "\<lambda>y. THE x. P y x"
-  have inv: "?g y \<in> X \<and> f (?g y) = y" if "y \<in> image f X" for y
-  proof -
-    from that obtain x where hx: "P y x" using P_def image_def by auto
-    moreover from this have "x = x'" if "P y x'" for x' using P_def that assms by auto
-    ultimately have "P y (?g y)" using theI[of "P y"] by blast
-    then show ?thesis using P_def by auto
-  qed 
-  have inv': "?g (f x) = x" if "x \<in> X" for x
-  proof -
-    have "?g (f x) \<in> X \<and> f (?g (f x)) = f x" using that inv image_def by auto
-    then show ?thesis using assms that by auto
-  qed
-  show "bijection_on X (image f X) f ?g" by (urule bijection_onI) (auto simp: inv')
-qed
-
-theorem cardinality_mul_eq_cardinal_mul_cardinality: "|X * Y| = |X| \<otimes> |Y|"
+theorem cardinality_mul_eq_cardinal_pair: "|X * Y| = |X \<times> Y|"
 proof -
-  define f :: "set \<Rightarrow> set" where "f = (\<lambda>\<langle>x, y\<rangle>. X * y + x)"
-  have "p\<^sub>1 = p\<^sub>2" if "p\<^sub>1 \<in> X \<times> Y" "p\<^sub>2 \<in> X \<times> Y" "f p\<^sub>1 = f p\<^sub>2" for p\<^sub>1 p\<^sub>2
-  proof -
-    from that obtain x\<^sub>1 y\<^sub>1 where "x\<^sub>1 \<in> X" "y\<^sub>1 \<in> Y" "p\<^sub>1 = \<langle>x\<^sub>1, y\<^sub>1\<rangle>" by auto
-    moreover from that obtain x\<^sub>2 y\<^sub>2 where "x\<^sub>2 \<in> X" "y\<^sub>2 \<in> Y" "p\<^sub>2 = \<langle>x\<^sub>2, y\<^sub>2\<rangle>" by auto 
+  define f :: "set \<Rightarrow> set" where "f \<equiv> \<lambda>\<langle>x, y\<rangle>. X * y + x"
+  have "injective_on (X \<times> Y :: set) f"
+  proof (urule injective_onI)
+    fix p\<^sub>1 p\<^sub>2 presume asms: "p\<^sub>1 \<in> X \<times> Y" "p\<^sub>2 \<in> X \<times> Y" "f p\<^sub>1 = f p\<^sub>2"
+    then obtain x\<^sub>1 y\<^sub>1 where "x\<^sub>1 \<in> X" "y\<^sub>1 \<in> Y" "p\<^sub>1 = \<langle>x\<^sub>1, y\<^sub>1\<rangle>" by auto
+    moreover from asms obtain x\<^sub>2 y\<^sub>2 where "x\<^sub>2 \<in> X" "y\<^sub>2 \<in> Y" "p\<^sub>2 = \<langle>x\<^sub>2, y\<^sub>2\<rangle>" by auto
     ultimately have "X * y\<^sub>1 + x\<^sub>1 = X * y\<^sub>2 + x\<^sub>2" using f_def \<open>f p\<^sub>1 = f p\<^sub>2\<close> by auto
     moreover have "x\<^sub>1 < X \<and> x\<^sub>2 < X" using \<open>x\<^sub>1 \<in> X\<close> \<open>x\<^sub>2 \<in> X\<close> lt_if_mem by auto
     ultimately have "x\<^sub>1 = x\<^sub>2 \<and> y\<^sub>1 = y\<^sub>2" using eq_if_mul_add_eq_mul_add_if_lt by blast
-    then show ?thesis 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
-  then have "\<exists>g. (bijection_on (X \<times> Y) (image f (X \<times> Y)) f g)"
-    using bijection_onto_image_if_injective_on by blast
+    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
-  moreover have "image f (X \<times> Y) = X * Y" 
+  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 have "|X \<times> Y| = |X * Y|" using cardinality_eq_if_equipollent by auto
-  then show ?thesis using cardinality_mul_cardinality_eq_cardinality_cartprod by auto
+  ultimately show ?thesis using cardinality_eq_if_equipollent by auto
 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
+
 end
 

HOTG/Arithmetics/HOTG_Multiplication.thy

@@ -5,8 +5,8 @@ theory HOTG_Multiplication
   imports
     HOTG_Addition
     HOTG_Additively_Divides
-    HOTG_Ranks
     HOTG_Ordinals_Max
+    HOTG_Ranks
 begin
 
 unbundle no_HOL_groups_syntax
@@ -16,14 +16,14 @@ text \<open>Translation of generalised set multiplication for sets from \<^cite>
 and \<^cite>\<open>ZFC_in_HOL_AFP\<close>. Note that general set multiplication is associative,
 but it is not commutative (not proven here).\<close>
 
-definition "mul X \<equiv> transrec (\<lambda>mulX Y. \<Union>(image (\<lambda>y. lift (mulX y) X) Y))"
+definition "mul X \<equiv> transfrec (\<lambda>mulX Y. \<Union>(image (\<lambda>y. lift (mulX y) X) Y))"
 
 bundle hotg_mul_syntax begin notation mul (infixl "*" 70) end
 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)"
-  unfolding mul_def by (urule transrec_eq)
+  unfolding mul_def by (urule transfrec_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
@@ -233,14 +233,10 @@ 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 eq_if_mul_add_eq_mul_add_if_lt_aux:
   assumes "A * X + R = A * Y + S" "R < A" "S < A"
   assumes IH:
-    "\<And>x y r s. x \<in> X \<Longrightarrow> y \<in> Y \<Longrightarrow> r < A \<Longrightarrow> s < A \<Longrightarrow> 
-    A * x + r = A * y + s \<Longrightarrow> x = y"
+    "\<And>x y r s. x \<in> X \<Longrightarrow> y \<in> Y \<Longrightarrow> r < A \<Longrightarrow> s < A \<Longrightarrow> A * x + r = A * y + s \<Longrightarrow> x = y"
   shows "X \<subseteq> Y"
 proof
   fix u assume "u \<in> X"
@@ -257,7 +253,7 @@ proof
     then show "False" using \<open>S < A\<close> not_subset_if_lt by blast
   qed
   from \<open>R < A\<close> obtain R' where "R' \<in> A" "R \<le> R'" by (auto elim: lt_mem_leE)
-  have "A * u + R' \<in> A * X" 
+  have "A * u + R' \<in> A * X"
     using mul_eq_idx_union_repl_mul_add[of A X] \<open>R' \<in> A\<close> \<open>u \<in> X\<close> by auto
   moreover have "A * X \<subseteq> A * Y \<union> lift (A * Y) S"
     using \<open>A * X + R = A * Y + S\<close> add_eq_bin_union_lift by auto
@@ -290,7 +286,7 @@ proof
     qed
   next
     case 2
-    then obtain v e where "v \<in> Y" "e \<in> A" "A * u + R' = A * v + e" 
+    then obtain v e where "v \<in> Y" "e \<in> A" "A * u + R' = A * v + e"
       using mul_eq_idx_union_repl_mul_add[of A Y] by auto
     then have "u = v" using IH \<open>u \<in> X\<close> \<open>R' \<in> A\<close> lt_if_mem by blast
     then show ?thesis using \<open>v \<in> Y\<close> by blast
@@ -303,30 +299,28 @@ lemma eq_if_mul_add_eq_mul_add_if_lt:
   shows "X = Y \<and> R = S"
 proof -
   let ?\<alpha> = "max_ordinal (rank X) (rank Y)"
-  have "X = Y \<and> R = S" if "ordinal \<alpha>" "rank X \<le> \<alpha>" "rank Y \<le> \<alpha>" for \<alpha> 
-    using that assms
+  have "X = Y \<and> R = S" if "ordinal \<alpha>" "rank X \<le> \<alpha>" "rank Y \<le> \<alpha>" for \<alpha>
+  using that assms
   proof (induction \<alpha> arbitrary: X Y R S rule: ordinal_mem_induct)
     case (step \<alpha>)
     have "\<exists>\<beta>. \<beta> \<in> \<alpha> \<and> rank x \<le> \<beta> \<and> rank y \<le> \<beta>" if "x \<in> X" "y \<in> Y" for x y
     proof
       define \<beta> :: set where "\<beta> = max_ordinal (rank x) (rank y)"
-      have "rank x < \<alpha>" 
+      have "rank x < \<alpha>"
         using \<open>x \<in> X\<close> lt_if_mem rank_lt_rank_if_lt \<open>rank X \<le> \<alpha>\<close> lt_if_lt_if_le by fastforce
       moreover have "rank y < \<alpha>"
         using \<open>y \<in> Y\<close> lt_if_mem rank_lt_rank_if_lt \<open>rank Y \<le> \<alpha>\<close> lt_if_lt_if_le by fastforce
       ultimately have "\<beta> < \<alpha>" using \<beta>_def max_ordinal_lt_if_lt_if_lt by auto
-      then have "\<beta> \<in> \<alpha>" using \<open>ordinal \<alpha>\<close> 
+      then have "\<beta> \<in> \<alpha>" using \<open>ordinal \<alpha>\<close>
         using mem_if_lt_if_mem_trans_closed ordinal_mem_trans_closedE  by auto
-      then show "\<beta> \<in> \<alpha> \<and> rank x \<le> \<beta> \<and> rank y \<le> \<beta>" using \<beta>_def ordinal_rank 
-        le_max_ordinal_left_if_ordinal_if_ordinal le_max_ordinal_right_if_ordinal_if_ordinal by auto 
+      then show "\<beta> \<in> \<alpha> \<and> rank x \<le> \<beta> \<and> rank y \<le> \<beta>" using \<beta>_def ordinal_rank
+        le_max_ordinal_left_if_ordinal_if_ordinal le_max_ordinal_right_if_ordinal_if_ordinal by auto
     qed
-    then have IH': 
-        "\<And>x y r s. x \<in> X \<Longrightarrow> y \<in> Y \<Longrightarrow> r < A \<Longrightarrow> s < A \<Longrightarrow> 
-        A * x + r = A * y + s \<Longrightarrow> x = y \<and> r = s"
+    then have IH':
+      "\<And>x y r s. x \<in> X \<Longrightarrow> y \<in> Y \<Longrightarrow> r < A \<Longrightarrow> s < A \<Longrightarrow> A * x + r = A * y + s \<Longrightarrow> x = y \<and> r = s"
       using step.IH by blast
-    then have "X \<subseteq> Y" 
-      using eq_if_mul_add_eq_mul_add_if_lt_aux step.prems by auto
-    moreover have "Y \<subseteq> X" 
+    then have "X \<subseteq> Y" using eq_if_mul_add_eq_mul_add_if_lt_aux step.prems by auto
+    moreover have "Y \<subseteq> X"
       using eq_if_mul_add_eq_mul_add_if_lt_aux[OF \<open>A * X + R = A * Y + S\<close>[symmetric]]
       using \<open>S < A\<close> \<open>R < A\<close> IH' by force
     ultimately have "X = Y" by auto
@@ -339,8 +333,9 @@ proof -
   ultimately show ?thesis by auto
 qed
 
-corollary eq_if_mul_eq_mul_if_nz:
-  assumes nz: "A \<noteq> 0" and eq: "A * X = A * Y"
+corollary eq_if_mul_eq_mul_if_ne_zero:
+  assumes nz: "A \<noteq> 0"
+  and eq: "A * X = A * Y"
   shows "X = Y"
 proof -
   from eq have "A * X + 0 = A * Y + 0" by auto

HOTG/Binary_Relations/Binary_Relations_Transitive_Closure.thy

@@ -0,0 +1,118 @@
+\<^marker>\<open>creator "Kevin Kappelmann"\<close>
+\<^marker>\<open>creator "Niklas Krofta"\<close>
+subsection \<open>Transitive Closure\<close>
+theory Binary_Relations_Transitive_Closure
+  imports
+    HOTG_Ordinals_Base
+    HOTG_Binary_Relations_Pow
+begin
+
+unbundle no_HOL_order_syntax
+
+(*TODO: could already be defined differently without sets in HOL_Basics library*)
+definition "trans_closure R x y \<equiv> (\<exists>n. rel_pow R n x y)"
+
+lemma trans_closureI [intro]:
+  assumes "rel_pow R n x y"
+  shows "trans_closure R x y"
+  using assms unfolding trans_closure_def by auto
+
+lemma trans_closureE [elim]:
+  assumes "trans_closure R x y"
+  obtains n where "rel_pow R n x y"
+  using assms unfolding trans_closure_def by auto
+
+lemma transitive_trans_closure: "transitive (trans_closure R)"
+proof -
+  have "trans_closure R x z" if "trans_closure R x y" "rel_pow R n y z" for n x y z using that
+  proof (induction n arbitrary: y z rule: mem_induction)
+    case (mem n)
+    consider "R y z" | m u where "m \<in> n" "rel_pow R m y u" "R u z"
+      using \<open>rel_pow R n y z\<close> by (blast elim: rel_powE)
+    then show ?case
+    proof cases
+      case 1
+      from \<open>trans_closure R x y\<close> obtain k where "rel_pow R k x y" by auto
+      from \<open>R y z\<close> have "rel_pow R (succ k) x z"
+        using rel_pow_iff[of R] \<open>rel_pow R k x y\<close> succ_eq_insert_self by blast
+      then show ?thesis by blast
+    next
+      case 2
+      from mem.IH have "trans_closure R x u"
+        using \<open>m \<in> n\<close> \<open>trans_closure R x y\<close> \<open>rel_pow R m y u\<close> by blast
+      then obtain k where "rel_pow R k x u" by auto
+      then have "rel_pow R (succ k) x z"
+        using \<open>R u z\<close> rel_pow_iff[of R] succ_eq_insert_self by blast
+      then show ?thesis by blast
+    qed
+  qed
+  then have "trans_closure R x z" if "trans_closure R x y" "trans_closure R y z" for x y z
+    using that by blast
+  then show ?thesis by fast
+qed
+
+lemma trans_closure_if_rel: "R x y \<Longrightarrow> trans_closure R x y"
+  using rel_pow_if_rel[of R] by fast
+
+lemma trans_closure_cases:
+  assumes "trans_closure R x y"
+  obtains (rel) "R x y" | (step) z where "trans_closure R x z" "R z y"
+  using assms rel_powE[of R] by blast
+
+lemma rel_if_rel_pow_if_le_if_transitive:
+  includes HOL_order_syntax no_hotg_le_syntax
+  assumes "transitive S"
+  and "R \<le> S"
+  and "rel_pow R n x y"
+  shows "S x y"
+using \<open>rel_pow R n x y\<close>
+proof (induction n arbitrary: y rule: mem_induction)
+  case (mem n)
+  show ?case using \<open>rel_pow R n x y\<close>
+  proof (cases rule: rel_powE)
+    case rel
+    then show ?thesis using \<open>R \<le> S\<close> by blast
+  next
+    case (step m z)
+    with mem.IH have "S x z" by blast
+    then show ?thesis using \<open>R z y\<close> \<open>R \<le> S\<close> \<open>transitive S\<close> by blast
+  qed
+qed
+
+corollary rel_if_trans_closure_if_le_if_transitive:
+  includes HOL_order_syntax no_hotg_le_syntax
+  assumes "transitive S"
+  and "R \<le> S"
+  and "trans_closure R x y"
+  shows "S x y"
+  using assms rel_if_rel_pow_if_le_if_transitive by (elim trans_closureE)
+
+text \<open>Note: together,
+@{thm transitive_trans_closure trans_closure_if_rel rel_if_trans_closure_if_le_if_transitive}
+show that @{term "trans_closure R"} satisfies the universal property:
+it is the smallest transitive relation containing @{term R}.\<close>
+
+lemma trans_closure_mem_eq_lt: "trans_closure (\<in>) = (<)"
+proof -
+  have "trans_closure (\<in>) x y \<Longrightarrow> x < y" for x y
+    by (rule rel_if_trans_closure_if_le_if_transitive[where ?R="(\<in>)"])
+    (use transitive_lt lt_if_mem in auto)
+  moreover have "x < y \<Longrightarrow> trans_closure (\<in>) x y" for x y
+  proof (induction y rule: mem_induction)
+    case (mem y)
+    from \<open>x < y\<close> obtain z where "x \<le> z" "z \<in> y" using lt_mem_leE by blast
+    then show ?case
+    proof (cases rule: leE)
+      case lt
+      with \<open>z \<in> y\<close> mem.IH have "trans_closure (\<in>) x z" by blast
+      then show ?thesis using \<open>z \<in> y\<close> transitive_trans_closure[of "(\<in>)"]
+      by (blast dest: trans_closure_if_rel)
+    next
+      case eq
+      then show ?thesis using \<open>z \<in> y\<close> trans_closure_if_rel by auto
+    qed
+  qed
+  ultimately show ?thesis by fastforce
+qed
+
+end

HOTG/Binary_Relations/HOTG_Binary_Relations.thy

@@ -2,10 +2,14 @@
 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_Extend
+    HOTG_Binary_Relations_Pow
 begin
 
 

HOTG/Binary_Relations/HOTG_Binary_Relations_Pow.thy

@@ -0,0 +1,34 @@
+\<^marker>\<open>creator "Kevin Kappelmann"\<close>
+\<^marker>\<open>creator "Niklas Krofta"\<close>
+subsection \<open>Power of Relations\<close>
+theory HOTG_Binary_Relations_Pow
+  imports HOTG_Transfinite_Recursion
+begin
+
+paragraph \<open>Summary\<close>
+text \<open>The n-th composition of a relation with itself:\<close>
+
+definition "rel_pow R = transfrec (\<lambda>r_pow n x y. R x y \<or> (\<exists>m : n. \<exists>z. r_pow m x z \<and> R z y))"
+
+lemma rel_pow_iff: "rel_pow R n x y \<longleftrightarrow> R x y \<or> (\<exists>m : n. \<exists>z. rel_pow R m x z \<and> R z y)"
+  using transfrec_eq[of "\<lambda>r_pow n x y. R x y \<or> (\<exists>m : n. \<exists>z. r_pow m x z \<and> R z y)" n]
+  unfolding rel_pow_def by auto
+
+lemma rel_pow_if_rel:
+  assumes "R x y"
+  shows "rel_pow R n x y"
+  using assms rel_pow_iff by fast
+
+lemma rel_pow_if_rel_if_mem_if_rel_pow:
+  assumes "rel_pow R m x z"
+  and "m \<in> n"
+  and "R z y"
+  shows "rel_pow R n x y"
+  using assms rel_pow_iff by fast
+
+lemma rel_powE:
+  assumes "rel_pow R n x y"
+  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