Commit 64d01de4 authored by Lawrence Paulson's avatar Lawrence Paulson
Browse files

Stylistic tweaks, which I hope are improvements :-)

parent bf041f4c01bf
......@@ -26,8 +26,7 @@ proof -
have "small D" "D \<subseteq> ON"
using assms down elts_subset_ON [of \<beta>] by auto
then have \<phi>_less_iff: "\<And>\<gamma> \<delta>. \<lbrakk>\<gamma> \<in> elts (tp D); \<delta> \<in> elts (tp D)\<rbrakk> \<Longrightarrow> \<phi> \<gamma> < \<phi> \<delta> \<longleftrightarrow> \<gamma> < \<delta>"
using ordermap_mono_less [of _ _ VWF D] bij_betw_apply [OF bij_\<phi>] VWF_iff_Ord_less \<phi>_cancel_right trans_VWF wf_VWF
by (metis ON_imp_Ord Ord_linear2 less_V_def order.asym)
by (metis ON_imp_Ord Ord_linear2 \<phi>_def inv_into_ordermap inv_ordermap_VWF_mono_le leD less_V_def)
obtain \<alpha>s where "List.set \<alpha>s \<subseteq> ON" and "\<omega>_dec \<alpha>s" and tpD_eq: "tp D = \<omega>_sum \<alpha>s"
using Ord_ordertype \<omega>_nf_exists by blast \<comment> \<open>Cantor normal form of the ordertype\<close>
have ord [simp]: "Ord (\<alpha>s ! k)" "Ord (\<omega>_sum (take k \<alpha>s))" if "k < length \<alpha>s" for k
......@@ -225,7 +224,8 @@ qed
text \<open>The ``remark'' of Erdős and E. C. Milner, Canad. Math. Bull. Vol. 17 (2), 1974\<close>
proposition indecomposable_imp_Ex_less_sets:
assumes indec: "indecomposable \<alpha>" and "\<alpha> > 1" and A: "tp A = \<alpha>" "small A" "A \<subseteq> ON"
assumes indec: "indecomposable \<alpha>" and "\<alpha> > 1"
and A: "tp A = \<alpha>" "small A" "A \<subseteq> ON"
and "x \<in> A" and A1: "tp A1 = \<alpha>" "A1 \<subseteq> A"
obtains A2 where "tp A2 = \<alpha>" "A2 \<subseteq> A1" "{x} \<lless> A2"
proof -
......@@ -244,12 +244,15 @@ proof -
then have "Ord \<gamma>"
using Ord_in_Ord \<open>Ord \<alpha>\<close> by blast
define B where "B \<equiv> \<phi> ` (elts (succ \<gamma>))"
have B: "{y \<in> A. ordermap A VWF y \<le> ordermap A VWF x} \<subseteq> B"
apply (clarsimp simp add: B_def \<gamma>_def image_iff \<phi>_def)
by (metis Ord_linear Ord_ordermap OrdmemD bij_betw_inv_into_left bij_om leD)
show thesis
proof
have "small A1"
by (meson \<open>small A\<close> A1 smaller_than_small)
then have "tp (A1 - B) \<le> tp A1"
unfolding B_def by (auto intro!: ordertype_VWF_mono del: vsubsetI)
by (simp add: ordertype_VWF_mono)
moreover have "tp (A1 - B) \<ge> \<alpha>"
proof -
have "\<not> (\<alpha> \<le> tp B)"
......@@ -265,34 +268,20 @@ proof -
using \<gamma> Limit_def \<open>Limit \<alpha>\<close> by blast
with A sub show "\<phi> u < \<phi> v"
if "u \<in> elts (succ \<gamma>)" and "v \<in> elts (succ \<gamma>)" and "u < v" for u v
by (metis ON_imp_Ord Ord_not_le \<open>A \<subseteq> ON\<close> \<open>small A\<close> \<phi>_def bij_\<phi> bij_betw_apply inv_ordermap_VWF_mono_le leD subsetD that)
by (metis ON_imp_Ord Ord_linear2 \<phi>_def inv_into_ordermap inv_ordermap_VWF_mono_le leD subset_iff that)
show "\<not> \<alpha> \<le> tp (elts (succ \<gamma>))"
by (metis Limit_def Ord_succ \<gamma> \<open>Limit \<alpha>\<close> \<open>Ord \<gamma>\<close> mem_not_refl ordertype_eq_Ord vsubsetD)
qed auto
then show ?thesis
using indecomposable_ordertype_ge [OF indec, of A1 B] \<open>small A1\<close> A1
by (auto simp: B_def)
using indecomposable_ordertype_ge [OF indec, of A1 B] \<open>small A1\<close> A1 by (auto simp: B_def)
qed
ultimately show "tp (A1 - B) = \<alpha>"
using A1 by blast
show "{x} \<lless> (A1 - B)"
proof (clarsimp simp: less_sets_def B_def simp del: elts_succ)
fix y
assume "y \<in> A1" and y: "y \<notin> \<phi> ` elts (succ \<gamma>)"
obtain "Ord x" "Ord y"
using \<open>A \<subseteq> ON\<close> \<open>x \<in> A\<close> \<open>y \<in> A1\<close> A1 by auto
have "y \<in> \<phi> ` elts (succ \<gamma>)" if "y \<in> elts (succ x)"
proof -
have "ordermap A VWF y \<in> elts (ZFC_in_HOL.succ (ordermap A VWF x))"
using A1
by (metis insert_iff ordermap_mono subset_iff that wf_VWF OrdmemD VWF_iff_Ord_less \<open>Ord x\<close> \<open>Ord y\<close> \<open>small A\<close> \<open>y \<in> A1\<close> elts_succ)
then show ?thesis
using that A1 unfolding \<gamma>_def
by (metis \<open>y \<in> A1\<close> \<phi>_def bij_betw_inv_into_left bij_om imageI subsetD)
qed
then show "x < y"
by (meson Ord_linear2 Ord_mem_iff_lt Ord_succ \<open>Ord x\<close> \<open>Ord y\<close> y succ_le_iff)
qed
have "{x} \<lless> (A - B)"
using assms B
apply (clarsimp simp: less_sets_def \<phi>_def subset_iff)
by (metis Ord_not_le VWF_iff_Ord_less less_V_def order_refl ordermap_mono_less trans_VWF wf_VWF)
with \<open>A1 \<subseteq> A\<close> show "{x} \<lless> (A1 - B)" by auto
qed auto
qed
......@@ -1242,7 +1231,7 @@ qed
theorem Erdos_Milner:
assumes \<nu>: "\<nu> \<in> elts \<omega>1"
shows "partn_lst_VWF (\<omega>\<up>(1 + \<nu> * ord_of_nat n)) [ord_of_nat (2^n), \<omega>\<up>(1+\<nu>)] 2"
shows "partn_lst_VWF (\<omega>\<up>(1 + \<nu> * n)) [ord_of_nat (2^n), \<omega>\<up>(1+\<nu>)] 2"
proof (induction n)
case 0
then show ?case
......
......@@ -1623,7 +1623,7 @@ proof (subst ordertype_eq_iff)
assume "f p < f q"
with \<section> assms have "(u, x) \<in> r \<or> u=x \<and> (v, y) \<in> s"
apply (simp add: f_def)
by (metis Ord_add Ord_add_mult_iff Ord_mem_iff_lt Ord_mult Ord_ordermap converse_ordermap_mono
by (metis Ord_add Ord_add_mult_iff Ord_mem_iff_lt Ord_mult wf_Ord_ordermap converse_ordermap_mono
ordermap_eq_iff ordermap_in_ordertype wf_Ord_ordertype)
then show "(p,q) \<in> (r <*lex*> s)"
by (simp add: \<section>)
......@@ -1642,7 +1642,7 @@ proof (subst ordertype_eq_iff)
assume "p = (a, b)" and "q = (a', b')"
then have "?\<beta> * ordermap A r a + ordermap B s b < ?\<beta> * ordermap A r a'"
using ux assms \<section>
by (metis Ord_mult Ord_ordermap OrdmemD Pair_inject add_mult_less ordermap_in_ordertype ordermap_mono wf_Ord_ordertype)
by (metis Ord_mult wf_Ord_ordermap OrdmemD Pair_inject add_mult_less ordermap_in_ordertype ordermap_mono wf_Ord_ordertype)
also have "\<dots> \<le> ?\<beta> * ordermap A r a' + ordermap B s b'"
by simp
finally show "?\<beta> * ordermap A r a + ordermap B s b < ?\<beta> * ordermap A r a' + ordermap B s b'" .
......
......@@ -909,7 +909,7 @@ lemma ordermap: "wf r \<Longrightarrow> ordermap A r a = set (ordermap A r ` {y
unfolding ordermap_def
by (auto simp: wfrec_fixpoint adm_wf_def)
lemma Ord_ordermap [iff]: assumes "wf r" "trans r" shows "Ord (ordermap A r x)"
lemma wf_Ord_ordermap [iff]: assumes "wf r" "trans r" shows "Ord (ordermap A r x)"
using \<open>wf r\<close>
proof (induction x rule: wf_induct_rule)
case (less u)
......@@ -942,7 +942,7 @@ proof -
if "y = ordermap A r x" "x \<in> A" "small (ordermap A r ` A)" for x y
using that by (auto simp: less_eq_V_def ordermap [OF \<open>wf r\<close>, of A x])
moreover have "z \<le> y" if "y \<in> ordermap A r ` A" "z \<in> elts y" for y z
by (metis Ord_ordermap OrdmemD assms imageE order.strict_implies_order that)
by (metis wf_Ord_ordermap OrdmemD assms imageE order.strict_implies_order that)
ultimately show ?thesis
unfolding ordertype_def Ord_def Transset_def by simp
qed
......@@ -950,6 +950,9 @@ qed
lemma Ord_ordertype [simp]: "Ord(ordertype A VWF)"
using wf_Ord_ordertype by blast
lemma Ord_ordermap [simp]: "Ord (ordermap A VWF x)"
by blast
lemma ordertype_singleton [simp]:
assumes "wf r"
shows "ordertype {x} r = 1"
......@@ -1075,7 +1078,7 @@ proof -
case (less x)
have "ordermap X r z < ordermap Y r x" if "z \<in> X" and zx: "(z,x) \<in> r" for z
using less [OF zx] assms
by (meson Ord_linear2 OrdmemD Ord_ordermap ordermap_mono in_mono leD that(1) vsubsetD zx)
by (meson Ord_linear2 OrdmemD wf_Ord_ordermap ordermap_mono in_mono leD that(1) vsubsetD zx)
then show ?case
by (auto simp add: ordermap [of _ X x] \<open>small X\<close> Ord_mem_iff_lt set_image_le_iff less_eq_V_def r)
qed
......@@ -1211,7 +1214,7 @@ proof (rule ordertype_inc_eq)
by (meson assms smaller_than_small)
show "(ordermap A r x, ordermap A r y) \<in> VWF"
if "x \<in> X" "y \<in> X" "(x, y) \<in> r" for x y
by (meson that Ord_ordermap VWF_iff_Ord_less assms ordermap_mono_less subsetD)
by (meson that wf_Ord_ordermap VWF_iff_Ord_less assms ordermap_mono_less subsetD)
qed (use assms in auto)
lemma ordertype_map_image:
......@@ -1268,7 +1271,7 @@ proof
moreover have "ordermap A r x \<in> ordermap B s ` B"
by (meson L \<open>x \<in> A\<close> \<open>small A\<close> in_mono ordermap_in_ordertype ordermap_surj vsubsetD)
moreover have "ordermap A r x < ordermap A r y"
using * r s by (metis (no_types) Ord_ordermap OrdmemD \<open>(x, y) \<in> r\<close> \<open>x \<in> A\<close> \<open>small A\<close> ordermap_mono)
using * r s by (metis (no_types) wf_Ord_ordermap OrdmemD \<open>(x, y) \<in> r\<close> \<open>x \<in> A\<close> \<open>small A\<close> ordermap_mono)
ultimately show "(f x, f y) \<in> s"
using \<dagger> s by (metis assms(7) f_inv_into_f inv_into_into less_asym ordermap_mono_less total_on_def)
qed
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment