From 5454e957676b58de6f239c94e8029f6e586b1931 Mon Sep 17 00:00:00 2001 From: Kevin Kappelmann Date: Wed, 29 May 2024 16:27:38 +0200 Subject: [PATCH] feat(*) fine-tuning --- HOTG/Arithmetics/HOTG_Multiplication.thy | 51 +++++++-------- .../HOTG_Mem_Transitive_Closure.thy | 6 +- ..._Order.thy => HOTG_Additively_Divides.thy} | 65 ++++++++++--------- HOTG/Orders/HOTG_Less_Than.thy | 59 ++++++++--------- HOTG/Orders/HOTG_Orders.thy | 2 +- HOTG/Ordinals/HOTG_Ordinals.thy | 2 +- HOTG/Ordinals/HOTG_Ordinals_Base.thy | 44 ++++++------- HOTG/Ordinals/HOTG_Ordinals_Max.thy | 30 +++++++++ HOTG/Ordinals/HOTG_Ordinals_Min_Max.thy | 27 -------- HOTG/Ordinals/HOTG_Ranks.thy | 14 ++-- 10 files changed, 152 insertions(+), 148 deletions(-) rename HOTG/Orders/{HOTG_Additive_Order.thy => HOTG_Additively_Divides.thy} (59%) create mode 100644 HOTG/Ordinals/HOTG_Ordinals_Max.thy delete mode 100644 HOTG/Ordinals/HOTG_Ordinals_Min_Max.thy diff --git a/HOTG/Arithmetics/HOTG_Multiplication.thy b/HOTG/Arithmetics/HOTG_Multiplication.thy index 23ed81b..c41339b 100644 --- a/HOTG/Arithmetics/HOTG_Multiplication.thy +++ b/HOTG/Arithmetics/HOTG_Multiplication.thy @@ -3,8 +3,9 @@ subsection \Generalised Multiplication\ theory HOTG_Multiplication imports - HOTG_Addition HOTG_Additive_Order -begin + HOTG_Addition + HOTG_Additively_Divides +begin paragraph \Summary\ text \Translation of generalised set multiplication for sets from \<^cite>\kirby_set_arithemtics\ @@ -153,29 +154,25 @@ qed simp paragraph\Lemma 4.6 from \<^cite>\kirby_set_arithemtics\\ -text\The next lemma is rather complex and remains incomplete as of now. A complete proof -can be found in \<^cite>\kirby_set_arithemtics\ and -\<^url>\https://foss.heptapod.net/isa-afp/afp-devel/-/blob/06458dfa40c7b4aaaeb855a37ae77993cb4c8c18/thys/ZFC_in_HOL/Kirby.thy#L992\.\ - -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 \ where "\ x \ (\r. 0 < r \ r < A \ A * x = A * Y + r)" for x - have "\ X" using \_def assms by auto - then obtain X' where "\ X'" "X' \ X" and X'_min: "\x. x < X' \ \ \ x" - using minimal_satisfier_le by auto - from \\ X'\ obtain B' where "0 < B'" "B' < A" "A * X' = A * Y + B'" using \_def by auto + from assms have "\ X" unfolding \_def by auto + then obtain X' where "\ X'" "X' \ X" and X'_min: "\x. x < X' \ \ \ x" + using le_minimal_set_witnessE by auto + from \\ X'\ obtain B' where "0 < B'" "B' < A" "A * X' = A * Y + B'" unfolding \_def by auto then have "A * Y < A * X'" by auto then obtain p where "p \ A * X'" "A * Y \ p" by (auto elim: lt_mem_leE) - from \p \ A * X'\ obtain u c where "u \ X'" "c \ A" "p = A * u + c" + from \p \ A * X'\ obtain u c where "u \ X'" "c \ A" "p = A * u + c" using mul_eq_idx_union_repl_mul_add[of A X'] by auto have "A * u \ A * Y" proof assume "A * u = A * Y" moreover have "lift (A * u) A \ A * X'" using \u \ X'\ mul_eq_idx_union_lift_mul by fast ultimately have "lift (A * Y) A \ A * X'" by auto - then have "lift (A * Y) A \ A * Y \ lift (A * Y) B'" + then have "lift (A * Y) A \ A * Y \ lift (A * Y) B'" using \A * X' = A * Y + B'\ add_eq_bin_union_lift by blast then have "lift (A * Y) A \ lift (A * Y) B'" using disjoint_lift_self_right disjoint_iff_all_not_mem by blast @@ -183,11 +180,11 @@ proof - then show "False" using \B' < A\ not_subset_if_lt by blast qed from \A * Y \ p\ have "p \ A * Y" using lt_if_mem not_lt_if_le by auto - then have "p \ lift (A * Y) B'" + then have "p \ lift (A * Y) B'" using \p \ A * X'\ \A * X' = A * Y + B'\ add_eq_bin_union_lift by auto then obtain d where "d \ B'" "p = A * Y + d" using lift_eq_repl_add by auto - then consider "A * Y \ A * u" | "A * u \ A * Y" - using \p = A * u + c\ additively_divides_if_sums_equal by blast + then consider "A * Y \ A * u" | "A * u \ A * Y" + using \p = A * u + c\ 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 \d \ B'\ lt_if_mem \B' < A\ lt_trans by blast finally have "e < A" using lt_if_le_if_lt by auto have "e \ 0" using \A * u = A * Y + e\ add_zero_eq_self \A * u \ A * Y\ by force - then have "\ u" using \_def \e < A\ \A * u = A * Y + e\ by blast + then have "\ u" using \e < A\ \A * u = A * Y + e\ unfolding \_def by blast then have "False" using X'_min \u \ X'\ 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 \p = A * Y + d\ \p = A * u + c\ 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 \c \ A\ lt_if_mem_if_le by auto + then have "f < A" using \c \ A\ lt_if_mem_if_le by auto have "f \ 0" using \A * Y = A * u + f\ add_zero_eq_self \A * u \ A * Y\ by force have "u < X" using \u \ X'\ lt_if_mem \X' \ X\ lt_if_le_if_lt by blast then show ?thesis using that \A * Y = A * u + f\ \f \ 0\ \f < A\ \u < X\ 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 \ 0" then have "0 < B" by auto - from zero_if_multi_eq_multi_add_aux[OF step(2) \0 < B\ \B < A\] 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 \u < X\ 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 \u < X\ by auto then show "False" using \0 < g\ by auto qed qed diff --git a/HOTG/Mem_Transitive_Closure/HOTG_Mem_Transitive_Closure.thy b/HOTG/Mem_Transitive_Closure/HOTG_Mem_Transitive_Closure.thy index 0b8db03..09ab18e 100644 --- a/HOTG/Mem_Transitive_Closure/HOTG_Mem_Transitive_Closure.thy +++ b/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 \ X" shows "mem_trans_closure Y \ 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" diff --git a/HOTG/Orders/HOTG_Additive_Order.thy b/HOTG/Orders/HOTG_Additively_Divides.thy similarity index 59% rename from HOTG/Orders/HOTG_Additive_Order.thy rename to HOTG/Orders/HOTG_Additively_Divides.thy index 5676929..ece17db 100644 --- a/HOTG/Orders/HOTG_Additive_Order.thy +++ b/HOTG/Orders/HOTG_Additively_Divides.thy @@ -1,25 +1,29 @@ -theory HOTG_Additive_Order - imports HOTG_Addition +\<^marker>\creator "Niklas Krofta"\ +theory HOTG_Additively_Divides + imports + HOTG_Addition + Transport.Functions_Base begin -definition additively_divides :: "set \ set \ bool" where -"additively_divides x y \ (\d. x + d = y)" +unbundle no_HOL_groups_syntax -bundle hotg_additive_order_syntax begin notation additively_divides (infix "\" 50) end -bundle no_hotg_additive_order_syntax begin no_notation additively_divides (infix "\" 50) end -unbundle hotg_additive_order_syntax +definition "additively_divides x y \ has_inverse ((+) x) y" -lemma additively_dividesI[intro]: +bundle hotg_additively_divides_syntax begin notation additively_divides (infix "\" 50) end +bundle no_hotg_additively_divides_syntax begin no_notation additively_divides (infix "\" 50) end +unbundle hotg_additively_divides_syntax + +lemma additively_dividesI [intro]: assumes "x + d = y" shows "x \ y" unfolding additively_divides_def using assms by auto -lemma additively_dividesE[elim]: +lemma additively_dividesE [elim]: assumes "x \ y" obtains d where "x + d = y" using assms unfolding additively_divides_def by auto -lemma subset_if_additively_divides: "x \ y \ x \ y" +lemma subset_if_additively_divides: "x \ y \ x \ y" using add_eq_bin_union_lift by force lemma le_if_additively_divides: "x \ y \ x \ y" @@ -31,7 +35,7 @@ lemma reflexive_additively_divides: "reflexive (\)" lemma antisymmetric_additively_divides: "antisymmetric (\)" using subset_if_additively_divides by auto -lemma additively_divides_trans[trans]: "x \ y \ y \ z \ x \ z" +lemma additively_divides_trans [trans]: "x \ y \ y \ z \ x \ z" using add_assoc by force corollary transitive_additively_divides: "transitive (\)" @@ -40,41 +44,36 @@ corollary transitive_additively_divides: "transitive (\)" corollary preorder_additively_divides: "preorder (\)" using reflexive_additively_divides transitive_additively_divides by blast -corollary additively_divides_partial_order: "partial_order (\)" +corollary partial_order_additively_divides: "partial_order (\)" 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 \ c \ c \ a" proof (rule ccontr) - assume ac_incomparable: "\ (a \ c \ c \ a)" + assume ac_incomparable: "\(a \ c \ c \ a)" have "\z. a + x \ 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 "\ (\z. a + x \ c + z)" + assume "\(\z. a + x \ c + z)" then obtain z where hz: "a + x = c + z" by auto - then have "z \ 0" using add_zero_eq_self ac_incomparable by auto + with ac_incomparable have "z \ 0" by auto from \x \ 0\ obtain v where "v \ x" by auto - then have "a + v \ c + z" unfolding hz[symmetric] using add_eq_bin_union_repl_add[of a x] by auto + then have "a + v \ c + z" using hz add_eq_bin_union_repl_add[where ?Y=x] by auto then consider (c) "a + v \ c" | (\) "a + v \ 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 \ lift a x" proof (rule ccontr) - assume "\ lift c z \ lift a x" + assume "\(lift c z \ lift a x)" then have "\z' : lift c z. z' \ a" using hz unfolding add_eq_bin_union_lift by auto then obtain w where "c + w \ a" using lift_eq_repl_add by auto then have "c + w \ a + v" using add_eq_bin_union_lift by auto - moreover have "a + v \ c + w" using add_eq_bin_union_lift[of c w] using c by auto + moreover from c have "a + v \ 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 \ 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 \v \ x\ 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 \ c" | (right_divides) "c \ a" + using assms additively_divides_or_additively_divides_if_add_eq_add by blast + + end \ No newline at end of file diff --git a/HOTG/Orders/HOTG_Less_Than.thy b/HOTG/Orders/HOTG_Less_Than.thy index 9ab03a9..182741c 100644 --- a/HOTG/Orders/HOTG_Less_Than.thy +++ b/HOTG/Orders/HOTG_Less_Than.thy @@ -42,6 +42,16 @@ lemma mem_trans_closure_if_lt: shows "X \ mem_trans_closure Y" using assms unfolding lt_iff_mem_trans_closure by simp +lemma not_subset_if_lt: + assumes "A < B" + shows "\(B \ A)" +proof + assume "B \ A" + with mem_trans_closure_if_lt have "A \ 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 \ X < S \ X \ S" using mem_trans_closure_if_lt mem_trans_closure_le_if_le_if_mem_trans_closed by blast @@ -183,22 +193,22 @@ local_setup \ } \ -lemma minimal_satisfier: +lemma lt_minimal_set_witnessE: assumes "P a" - obtains m where "P m" "\b. b < m \ \ P b" + obtains m where "P m" "\b. b < m \ \(P b)" proof - - have "\m. P m \ (\b. b < m \ \ P b)" + have "\m : P. \b. b < m \ \(P b)" proof (rule ccontr) - assume no_minimal: "\m. P m \ (\b. b < m \ \ P b)" - have "\x. x \ X \ \ P x" for X + assume no_minimal: "\(\m : P. \b. b < m \ \(P b))" + have "\x. x \ X \ \(P x)" for X proof (induction X rule: mem_induction) case (mem X) show ?case proof (rule ccontr) - assume "\ (\x. x \ X \ \ P x)" + assume "\(\x. x \ X \ \(P x))" then obtain x where "x \ 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 \ X" "y \ z" using lt_if_le_if_lt \x \ X\ lt_mem_leE by blast - then show "False" using mem.IH \P y\ by auto + with mem.IH \P y\ show "False" by auto qed qed then show "False" using \P a\ by auto @@ -206,35 +216,26 @@ proof - 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 \ a" "\b. b < m \ \ P b" + obtains m where "P m" "m \ a" "\b. b < m \ \(P b)" proof - define Q where "Q x \ P x \ x \ a" for x - have "Q a" using assms Q_def by auto - then obtain m where "Q m" "\b. b < m \ \ Q b" using minimal_satisfier by auto - then have "\ 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 \Q m\ Q_def by auto + from assms have "Q a" unfolding Q_def by auto + then obtain m where "Q m" "\b. b < m \ \(Q b)" using lt_minimal_set_witnessE by auto + moreover then have "\(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 "\X. \\x. x < X \ P x\ \ P X" + assumes "\X. \\x. x < X \(P x)\ \(P X)" shows "P X" proof (rule ccontr) - assume "\ P X" - then obtain m where "\ P m" "\y. y < m \ P y" - using minimal_satisfier[where P="\x. \ P x"] by auto - then show "False" using assms by auto -qed - -lemma not_subset_if_lt: - assumes "A < B" - shows "\ B \ A" -proof - assume "B \ A" - then have "A \ 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 "\(P X)" + then obtain m where "\(P m)" "\y. y < m \ P y" + using lt_minimal_set_witnessE[where P="\x. \(P x)"] by auto + with assms show "False" by auto qed end diff --git a/HOTG/Orders/HOTG_Orders.thy b/HOTG/Orders/HOTG_Orders.thy index d2cf6bf..e1be693 100644 --- a/HOTG/Orders/HOTG_Orders.thy +++ b/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 diff --git a/HOTG/Ordinals/HOTG_Ordinals.thy b/HOTG/Ordinals/HOTG_Ordinals.thy index c521a1d..944b649 100644 --- a/HOTG/Ordinals/HOTG_Ordinals.thy +++ b/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 diff --git a/HOTG/Ordinals/HOTG_Ordinals_Base.thy b/HOTG/Ordinals/HOTG_Ordinals_Base.thy index 5d56d70..20da665 100644 --- a/HOTG/Ordinals/HOTG_Ordinals_Base.thy +++ b/HOTG/Ordinals/HOTG_Ordinals_Base.thy @@ -3,9 +3,9 @@ section \Ordinals\ theory HOTG_Ordinals_Base imports + HOTG_Binary_Relations_Connected HOTG_Foundation Transport.HOL_Syntax_Bundles_Groups - HOTG_Binary_Relations_Connected begin paragraph \Summary\ @@ -165,7 +165,7 @@ lemma limit_ordinalE: obtains "ordinal X" "0 \ X" "\x. x \ X \ succ x \ X" using assms unfolding limit_ordinal_def by auto -lemma union_eq_self_if_limit_ordinal: +lemma union_eq_self_if_limit_ordinal: assumes limit: "limit_ordinal X" shows "\X = X" proof @@ -178,8 +178,7 @@ next ultimately show "x \ \X" by blast qed -lemma ordinal_mem_total_order: - shows "ordinal X \ ordinal Y \ X \ Y \ X = Y \ Y \ X" +lemma mem_or_eq_or_mem_if_ordinal_if_ordinal: "ordinal X \ ordinal Y \ X \ Y \ X = Y \ Y \ X" proof (induction X arbitrary: Y rule: ordinal_mem_induct) case step_X: (step X) show ?case using \ordinal Y\ @@ -193,56 +192,57 @@ proof (induction X arbitrary: Y rule: ordinal_mem_induct) then show ?thesis using mem_trans_if_ordinal \ordinal X\ \x \ X\ by auto next case y - have "X = y \ X \ y" using step_Y.IH[OF \y \ Y\] \y \ X\ by auto + have "X = y \ X \ y" using step_Y.IH \y \ Y\ \y \ X\ by auto then show ?thesis using mem_trans_if_ordinal \ordinal Y\ \y \ Y\ by auto - qed (auto) + qed auto qed qed -lemma ordinal_memE: - assumes "ordinal X" and "ordinal Y" +lemma mem_eq_mem_if_ordinalE: + assumes "ordinal X" "ordinal Y" obtains "X \ Y" | "X = Y" | "Y \ X" - using ordinal_mem_total_order assms by (auto del: ordinal_mem_trans_closedE) + using mem_or_eq_or_mem_if_ordinal_if_ordinal assms by (auto del: ordinal_mem_trans_closedE) -lemma membership_connected_ordinals: - shows "connected_on ordinal (\)" - by (auto elim: ordinal_memE del: ordinal_mem_trans_closedE) +lemma connected_on_ordinal_mem: "connected_on ordinal (\)" + by (auto elim: mem_eq_mem_if_ordinalE del: ordinal_mem_trans_closedE) lemma ordinal_cases [cases type: set]: assumes ordinal: "ordinal k" - obtains (0) "k = 0" | (succ) l where "ordinal l" "succ l = k" | (limit) "limit_ordinal k" + obtains (zero) "k = 0" | (succ) l where "ordinal l" "succ l = k" | (limit) "limit_ordinal k" proof (cases "limit_ordinal k") case not_limit: False then show ?thesis proof (cases "0 \ k") case True - then obtain l where hl: "l \ k \ succ l \ k" using not_limit ordinal by (fast intro!: limit_ordinalI) + then obtain l where hl: "l \ k \ succ l \ k" using not_limit ordinal + by (fast intro!: limit_ordinalI) have succ_subset: "succ l \ k" using mem_succE mem_trans_if_ordinal[OF ordinal] hl by blast from hl have "ordinal (succ l)" using ordinal ordinal_succI ordinal_if_mem_if_ordinal by auto - from ordinal_mem_total_order[OF this ordinal] have "succ l = k" using hl succ_subset by auto + from mem_or_eq_or_mem_if_ordinal_if_ordinal[OF this ordinal] have "succ l = k" + using hl succ_subset by auto moreover have "ordinal l" using ordinal_if_mem_if_ordinal ordinal hl by blast ultimately show ?thesis using succ by auto next case False - then have "k = 0" using ordinal_mem_total_order[OF ordinal ordinal_zero] by blast - then show ?thesis using 0 by blast + then have "k = 0" using mem_or_eq_or_mem_if_ordinal_if_ordinal[OF ordinal] by blast + then show ?thesis using zero by blast qed qed text\Standard ordinal induction:\ lemma ordinal_induct [consumes 1, case_names zero succ limit, induct type: set]: - assumes - "ordinal X" and "P 0" and - P_succ: "\X. \ordinal X; P X\ \ P (succ X)" and - P_limit: "\X. \limit_ordinal X; \x. x \ X \ P x\ \ P (\X)" + assumes "ordinal X" + and "P 0" + and P_succ: "\X. \ordinal X; P X\ \ P (succ X)" + and P_limit: "\X. \limit_ordinal X; \x. x \ X \ P x\ \ P (\X)" shows "P X" using \ordinal X\ proof (induction X rule: ordinal_mem_induct) case (step X) then show ?case proof (cases rule: ordinal_cases) - case 0 + case zero with \P 0\ show ?thesis by simp next case (succ l) diff --git a/HOTG/Ordinals/HOTG_Ordinals_Max.thy b/HOTG/Ordinals/HOTG_Ordinals_Max.thy new file mode 100644 index 0000000..d5caa18 --- /dev/null +++ b/HOTG/Ordinals/HOTG_Ordinals_Max.thy @@ -0,0 +1,30 @@ +\<^marker>\creator "Niklas Krofta"\ +theory HOTG_Ordinals_Max + imports + HOTG_Ordinals_Base + HOTG_Less_Than +begin + +unbundle no_HOL_order_syntax + +definition max_ordinal :: "set \ set \ set" where + "max_ordinal A B = (if A \ B then B else A)" + +lemma pred_max_ordinal_if_pred_if_pred: "P A \ P B \ P (max_ordinal A B)" + using max_ordinal_def by auto + +lemma le_max_ordinal_left_if_ordinal_if_ordinal: "ordinal A \ ordinal B \ A \ max_ordinal A B" + using ordinal_memE max_ordinal_def le_if_lt lt_if_mem by auto + +lemma max_ordinal_comm_if_ordinal_if_ordinal: + assumes "ordinal A" "ordinal B" + shows "max_ordinal A B = max_ordinal B A" + using assms ordinal_memE by (auto simp: max_ordinal_def not_mem_if_mem) + +lemma le_max_ordinal_right_if_ordinal_if_ordinal: "ordinal A \ ordinal B \ B \ max_ordinal A B" + using le_max_ordinal_left_if_ordinal_if_ordinal max_ordinal_comm_if_ordinal_if_ordinal by force + +lemma max_ordinal_lt_if_lt_if_lt: "A < C \ B < C \ max_ordinal A B < C" + using max_ordinal_def by auto + +end \ No newline at end of file diff --git a/HOTG/Ordinals/HOTG_Ordinals_Min_Max.thy b/HOTG/Ordinals/HOTG_Ordinals_Min_Max.thy deleted file mode 100644 index 913a065..0000000 --- a/HOTG/Ordinals/HOTG_Ordinals_Min_Max.thy +++ /dev/null @@ -1,27 +0,0 @@ -theory HOTG_Ordinals_Min_Max - imports HOTG_Ordinals_Base HOTG_Less_Than -begin - -unbundle no_HOL_order_syntax - -definition max_ordinal :: "set \ set \ set" where -"max_ordinal A B = (if A \ B then B else A)" - -lemma ordinal_max_ordinal: "ordinal A \ ordinal B \ ordinal (max_ordinal A B)" - using max_ordinal_def by auto - -lemma le_max_ordinal_left: "ordinal A \ ordinal B \ A \ max_ordinal A B" - using ordinal_memE max_ordinal_def le_if_lt lt_if_mem by auto - -lemma max_ordinal_comm: - assumes "ordinal A" and "ordinal B" - shows "max_ordinal A B = max_ordinal B A" - by (cases rule: ordinal_memE[OF assms]) (auto simp: max_ordinal_def not_mem_if_mem) - -lemma le_max_ordinal_right: "ordinal A \ ordinal B \ B \ max_ordinal A B" - using le_max_ordinal_left max_ordinal_comm by force - -lemma max_ordinal_lt: "A < C \ B < C \ max_ordinal A B < C" - using max_ordinal_def by auto - -end \ No newline at end of file diff --git a/HOTG/Ordinals/HOTG_Ranks.thy b/HOTG/Ordinals/HOTG_Ranks.thy index 8b2e368..e32b49b 100644 --- a/HOTG/Ordinals/HOTG_Ranks.thy +++ b/HOTG/Ordinals/HOTG_Ranks.thy @@ -1,3 +1,4 @@ +\<^marker>\creator "Niklas Krofta"\ theory HOTG_Ranks imports HOTG_Ordinals_Base HOTG_Less_Than begin @@ -5,19 +6,18 @@ begin unbundle no_HOL_order_syntax definition rank :: "set \ set" where -"rank = transrec (\rank X. (\x \ X. succ (rank x)))" + "rank = transrec (\rank X. (\x \ X. succ (rank x)))" -lemma rank_eq_idx_union_rank_incr: "rank X = (\x \ X. succ (rank x))" +lemma rank_eq_idx_union_succ_rank: "rank X = (\x \ X. succ (rank x))" unfolding rank_def by (urule transrec_eq) lemma ordinal_rank: "ordinal (rank X)" proof (induction X rule: mem_induction) case (mem X) - then show ?case using rank_eq_idx_union_rank_incr[of X] by (auto intro: ordinal_unionI) + then show ?case using rank_eq_idx_union_succ_rank[of X] by (auto intro: ordinal_unionI) qed -lemma rank_lt_rank_if_lt: - shows "A < B \ rank A < rank B" +lemma rank_lt_rank_if_lt: "A < B \ rank A < rank B" proof (induction B rule: mem_induction) case (mem B) from \A < B\ obtain C where "C \ B" "A \ C" by (auto elim: lt_mem_leE) @@ -25,10 +25,10 @@ proof (induction B rule: mem_induction) proof cases case lt then show ?thesis using mem.IH \C \ B\ le_if_lt by auto - qed (auto) + qed auto moreover have "rank C < rank B" proof - - have "succ (rank C) \ rank B" using rank_eq_idx_union_rank_incr[of B] \C \ B\ by auto + have "succ (rank C) \ rank B" using rank_eq_idx_union_succ_rank[of B] \C \ B\ by auto then show ?thesis using succ_eq_insert_self lt_if_mem by auto qed ultimately show ?case using lt_if_le_if_lt by auto