# HG changeset patch # User blanchet # Date 1389901974 -3600 # Node ID 38db7814481d745f0d4d8fe82da57cd6eaf7a187 # Parent eeba3ba734869e2f915dc6721602284c194efb85 get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation' diff -r eeba3ba73486 -r 38db7814481d src/HOL/BNF/BNF_LFP.thy --- a/src/HOL/BNF/BNF_LFP.thy Thu Jan 16 18:52:50 2014 +0100 +++ b/src/HOL/BNF/BNF_LFP.thy Thu Jan 16 20:52:54 2014 +0100 @@ -30,14 +30,14 @@ lemma prop_restrict: "\x \ Z; Z \ {x. x \ X \ P x}\ \ P x" by auto -lemma underS_I: "\i \ j; (i, j) \ R\ \ i \ rel.underS R j" -unfolding rel.underS_def by simp +lemma underS_I: "\i \ j; (i, j) \ R\ \ i \ underS R j" +unfolding underS_def by simp -lemma underS_E: "i \ rel.underS R j \ i \ j \ (i, j) \ R" -unfolding rel.underS_def by simp +lemma underS_E: "i \ underS R j \ i \ j \ (i, j) \ R" +unfolding underS_def by simp -lemma underS_Field: "i \ rel.underS R j \ i \ Field R" -unfolding rel.underS_def Field_def by auto +lemma underS_Field: "i \ underS R j \ i \ Field R" +unfolding underS_def Field_def by auto lemma FieldI2: "(i, j) \ R \ j \ Field R" unfolding Field_def by auto diff -r eeba3ba73486 -r 38db7814481d src/HOL/BNF/Tools/bnf_lfp_util.ML --- a/src/HOL/BNF/Tools/bnf_lfp_util.ML Thu Jan 16 18:52:50 2014 +0100 +++ b/src/HOL/BNF/Tools/bnf_lfp_util.ML Thu Jan 16 20:52:54 2014 +0100 @@ -34,7 +34,7 @@ fun mk_underS r = let val T = fst (dest_relT (fastype_of r)); - in Const (@{const_name rel.underS}, mk_relT (T, T) --> T --> HOLogic.mk_setT T) $ r end; + in Const (@{const_name underS}, mk_relT (T, T) --> T --> HOLogic.mk_setT T) $ r end; fun mk_worec r f = let val (A, AB) = apfst domain_type (dest_funT (fastype_of f)); diff -r eeba3ba73486 -r 38db7814481d src/HOL/Cardinals/Cardinal_Order_Relation.thy --- a/src/HOL/Cardinals/Cardinal_Order_Relation.thy Thu Jan 16 18:52:50 2014 +0100 +++ b/src/HOL/Cardinals/Cardinal_Order_Relation.thy Thu Jan 16 20:52:54 2014 +0100 @@ -1012,11 +1012,11 @@ lemma natLeq_ofilter_less: "ofilter natLeq {0 ..< n}" by(auto simp add: natLeq_wo_rel wo_rel.ofilter_def, - simp add: Field_natLeq, unfold rel.under_def, auto) + simp add: Field_natLeq, unfold under_def, auto) lemma natLeq_ofilter_leq: "ofilter natLeq {0 .. n}" by(auto simp add: natLeq_wo_rel wo_rel.ofilter_def, - simp add: Field_natLeq, unfold rel.under_def, auto) + simp add: Field_natLeq, unfold under_def, auto) lemma natLeq_UNIV_ofilter: "wo_rel.ofilter natLeq UNIV" using natLeq_wo_rel Field_natLeq wo_rel.Field_ofilter[of natLeq] by auto @@ -1047,7 +1047,7 @@ proof(rule iffI) assume "ofilter natLeq A" hence "\m n. n \ A \ m \ n \ m \ A" - by(auto simp add: natLeq_wo_rel wo_rel.ofilter_def rel.under_def) + by(auto simp add: natLeq_wo_rel wo_rel.ofilter_def under_def) thus "A = UNIV \ (\n. A = {0 ..< n})" using closed_nat_set_iff by blast next assume "A = UNIV \ (\n. A = {0 ..< n})" @@ -1056,22 +1056,22 @@ qed lemma natLeq_under_leq: "under natLeq n = {0 .. n}" -unfolding rel.under_def by auto +unfolding under_def by auto lemma natLeq_on_ofilter_less_eq: "n \ m \ wo_rel.ofilter (natLeq_on m) {0 ..< n}" apply (auto simp add: natLeq_on_wo_rel wo_rel.ofilter_def) apply (simp add: Field_natLeq_on) -by (auto simp add: rel.under_def) +by (auto simp add: under_def) lemma natLeq_on_ofilter_iff: "wo_rel.ofilter (natLeq_on m) A = (\n \ m. A = {0 ..< n})" proof(rule iffI) assume *: "wo_rel.ofilter (natLeq_on m) A" hence 1: "A \ {0..n1 n2. n2 \ A \ n1 \ n2 \ n1 \ A" - using * by(fastforce simp add: natLeq_on_wo_rel wo_rel.ofilter_def rel.under_def) + using * by(fastforce simp add: natLeq_on_wo_rel wo_rel.ofilter_def under_def) hence "A = UNIV \ (\n. A = {0 ..< n})" using closed_nat_set_iff by blast thus "\n \ m. A = {0 ..< n}" using 1 atLeastLessThan_less_eq by blast next @@ -1086,7 +1086,7 @@ lemma natLeq_on_ofilter_less: "n < m \ ofilter (natLeq_on m) {0 .. n}" by(auto simp add: natLeq_on_wo_rel wo_rel.ofilter_def, - simp add: Field_natLeq_on, unfold rel.under_def, auto) + simp add: Field_natLeq_on, unfold under_def, auto) lemma natLeq_on_ordLess_natLeq: "natLeq_on n r" shows "under r i \ under r j" -using assms unfolding rel.under_def order_on_defs +using assms unfolding under_def order_on_defs trans_def by blast lemma underS_under: assumes "i \ Field r" shows "underS r i = under r i - {i}" -using assms unfolding rel.underS_def rel.under_def by auto +using assms unfolding underS_def under_def by auto lemma relChain_under: assumes "Well_order r" @@ -1593,7 +1593,7 @@ unfolding p_def apply(rule Refl_Field_Restr2[OF rr]) by auto have of: "ofilter r (Field p)" unfolding wo_rel.ofilter_def[OF 0] proof safe fix a x assume a: "a \ Field p" and "x \ under r a" - hence x: "(x,a) \ r" "x \ Field r" unfolding rel.under_def Field_def by auto + hence x: "(x,a) \ r" "x \ Field r" unfolding under_def Field_def by auto moreover have a: "a \ j" "a \ Field r" "(a,j) \ r" using a jm unfolding fp by auto ultimately have "x \ j" using j jm by (metis 0 wo_rel.max2_def wo_rel.max2_equals1) thus "x \ Field p" using x unfolding fp by auto @@ -1654,7 +1654,7 @@ hence "As (succ r i) \ As j" using rc unfolding relChain_def by auto moreover {have "(i,succ r i) \ r" apply(rule wo_rel.succ_in[OF 0]) - using 1 unfolding rel.aboveS_def by auto + using 1 unfolding aboveS_def by auto hence "As i \ As (succ r i)" using As_s rc rij unfolding relChain_def Field_def by auto } ultimately show False unfolding Asij by auto @@ -1721,13 +1721,13 @@ def g \ "\ a. if F a \ {} then gg a else j0" have g: "\ a \ A. \ u \ F a. (f (a,u),g a) \ r" using gg unfolding g_def by auto hence 1: "Field r \ (\ a \ A. under r (g a))" - using f[symmetric] unfolding rel.under_def image_def by auto + using f[symmetric] unfolding under_def image_def by auto have gA: "g ` A \ Field r" using gg j0 unfolding Field_def g_def by auto moreover have "cofinal (g ` A) r" unfolding cofinal_def proof safe fix i assume "i \ Field r" then obtain j where ij: "(i,j) \ r" "i \ j" using cr ir by (metis infinite_Card_order_limit) - hence "j \ Field r" by (metis card_order_on_def cr rel.well_order_on_domain) - then obtain a where a: "a \ A" and j: "(j, g a) \ r" using 1 unfolding rel.under_def by auto + hence "j \ Field r" by (metis card_order_on_def cr well_order_on_domain) + then obtain a where a: "a \ A" and j: "(j, g a) \ r" using 1 unfolding under_def by auto hence "(i, g a) \ r" using ij wo_rel.TRANS[OF r] unfolding trans_def by blast moreover have "i \ g a" using ij j r unfolding wo_rel_def unfolding well_order_on_def linear_order_on_def @@ -1752,7 +1752,7 @@ {assume Kr: "|K| a \ Field r. f a \ K \ a \ f a \ (a, f a) \ r" using cof unfolding cofinal_def by metis - hence "Field r \ (\ a \ K. underS r a)" unfolding rel.underS_def by auto + hence "Field r \ (\ a \ K. underS r a)" unfolding underS_def by auto hence "r \o |\ a \ K. underS r a|" using cr by (metis Card_order_iff_ordLeq_card_of card_of_mono1 ordLeq_transitive) also have "|\ a \ K. underS r a| \o |SIGMA a: K. underS r a|" by (rule card_of_UNION_Sigma) diff -r eeba3ba73486 -r 38db7814481d src/HOL/Cardinals/Cardinal_Order_Relation_FP.thy --- a/src/HOL/Cardinals/Cardinal_Order_Relation_FP.thy Thu Jan 16 18:52:50 2014 +0100 +++ b/src/HOL/Cardinals/Cardinal_Order_Relation_FP.thy Thu Jan 16 20:52:54 2014 +0100 @@ -59,7 +59,7 @@ lemma card_order_on_Card_order: "card_order_on A r \ A = Field r \ Card_order r" -unfolding card_order_on_def using rel.well_order_on_Field by blast +unfolding card_order_on_def using well_order_on_Field by blast text{* The existence of a cardinal relation on any given set (which will mean @@ -77,7 +77,7 @@ proof- obtain R where R_def: "R = {r. well_order_on A r}" by blast have 1: "R \ {} \ (\r \ R. Well_order r)" - using well_order_on[of A] R_def rel.well_order_on_Well_order by blast + using well_order_on[of A] R_def well_order_on_Well_order by blast hence "\r \ R. \r' \ R. r \o r'" using exists_minim_Well_order[of R] by auto thus ?thesis using R_def unfolding card_order_on_def by auto @@ -98,7 +98,7 @@ proof(unfold card_order_on_def, auto) fix p' assume "well_order_on (Field r') p'" hence 0: "Well_order p' \ Field p' = Field r'" - using rel.well_order_on_Well_order by blast + using well_order_on_Well_order by blast obtain f where 1: "iso r' r f" and 2: "Well_order r \ Well_order r'" using ISO unfolding ordIso_def by auto hence 3: "inj_on f (Field r') \ f ` (Field r') = Field r" @@ -143,7 +143,7 @@ lemma Field_card_of: "Field |A| = A" using card_of_card_order_on[of A] unfolding card_order_on_def -using rel.well_order_on_Field by blast +using well_order_on_Field by blast lemma card_of_Card_order: "Card_order |A|" @@ -273,7 +273,7 @@ obtain f where 1: "well_order_on (Field r) r \ well_order_on (Field r) r \ embed r r' f" using assms unfolding ordLeq_def - by (auto simp add: rel.well_order_on_Well_order) + by (auto simp add: well_order_on_Well_order) hence "inj_on f (Field r) \ f ` (Field r) \ Field r'" by (auto simp add: embed_inj_on embed_Field) thus "|Field r| \o |Field r'|" using card_of_ordLeq by blast @@ -285,7 +285,7 @@ lemma card_of_Field_ordLess: "Well_order r \ |Field r| \o r" -using card_of_least card_of_well_order_on rel.well_order_on_Well_order by blast +using card_of_least card_of_well_order_on well_order_on_Well_order by blast lemma card_of_Field_ordIso: @@ -321,16 +321,16 @@ lemma Card_order_iff_Restr_underS: assumes "Well_order r" -shows "Card_order r = (\a \ Field r. Restr r (rel.underS r a) a \ Field r. Restr r (underS r a) o r" using card_of_least by blast thus ?thesis using assms ordLeq_ordLess_trans by blast qed @@ -937,35 +937,35 @@ lemma Card_order_infinite_not_under: assumes CARD: "Card_order r" and INF: "\finite (Field r)" -shows "\ (\a. Field r = rel.under r a)" +shows "\ (\a. Field r = under r a)" proof(auto) have 0: "Well_order r \ wo_rel r \ Refl r" using CARD unfolding wo_rel_def card_order_on_def order_on_defs by auto - fix a assume *: "Field r = rel.under r a" + fix a assume *: "Field r = under r a" show False proof(cases "a \ Field r") assume Case1: "a \ Field r" - hence "rel.under r a = {}" unfolding Field_def rel.under_def by auto + hence "under r a = {}" unfolding Field_def under_def by auto thus False using INF * by auto next - let ?r' = "Restr r (rel.underS r a)" + let ?r' = "Restr r (underS r a)" assume Case2: "a \ Field r" - hence 1: "rel.under r a = rel.underS r a \ {a} \ a \ rel.underS r a" - using 0 rel.Refl_under_underS rel.underS_notIn by metis - have 2: "wo_rel.ofilter r (rel.underS r a) \ rel.underS r a < Field r" + hence 1: "under r a = underS r a \ {a} \ a \ underS r a" + using 0 Refl_under_underS underS_notIn by metis + have 2: "wo_rel.ofilter r (underS r a) \ underS r a < Field r" using 0 wo_rel.underS_ofilter * 1 Case2 by fast hence "?r' Well_order ?r'" + have "Field ?r' = underS r a \ Well_order ?r'" using 2 0 Field_Restr_ofilter[of r] Well_order_Restr[of r] by blast - ultimately have "|rel.underS r a| f. bij_betw f (rel.under r a) (rel.underS r a)" + {have "\f. bij_betw f (under r a) (underS r a)" using infinite_imp_bij_betw[of "Field r" a] INF * 1 by auto - hence "|rel.under r a| =o |rel.underS r a|" using card_of_ordIso by blast + hence "|under r a| =o |underS r a|" using card_of_ordIso by blast } ultimately show False using not_ordLess_ordIso ordIso_symmetric by blast qed @@ -977,13 +977,13 @@ and a: "a : Field r" shows "EX b : Field r. a \ b \ (a,b) : r" proof- - have "Field r \ rel.under r a" + have "Field r \ under r a" using assms Card_order_infinite_not_under by blast - moreover have "rel.under r a \ Field r" - using rel.under_Field . - ultimately have "rel.under r a < Field r" by blast + moreover have "under r a \ Field r" + using under_Field . + ultimately have "under r a < Field r" by blast then obtain b where 1: "b : Field r \ ~ (b,a) : r" - unfolding rel.under_def by blast + unfolding under_def by blast moreover have ba: "b \ a" using 1 r unfolding card_order_on_def well_order_on_def linear_order_on_def partial_order_on_def preorder_on_def refl_on_def by auto @@ -1036,7 +1036,7 @@ using 7 unfolding bij_betw_def using 6 3 embed_inj_on 4 by auto hence temp2: "wo_rel.ofilter ?r' ?B \ ?B < ?A \ ?A" using 4 wo_rel_def[of ?r'] wo_rel.ofilter_def[of ?r' ?B] by blast - have "\ (\a. Field r = rel.under r a)" + have "\ (\a. Field r = under r a)" using 1 unfolding phi_def using Card_order_infinite_not_under[of r] by auto then obtain A1 where temp3: "wo_rel.ofilter r A1 \ A1 < ?A" and 9: "?B \ A1 \ A1" using temp2 3 bsqr_ofilter[of r ?B] by blast @@ -1332,8 +1332,8 @@ unfolding Field_def by auto -lemma natLeq_underS_less: "rel.underS natLeq n = {x. x < n}" -unfolding rel.underS_def by auto +lemma natLeq_underS_less: "underS natLeq n = {x. x < n}" +unfolding underS_def by auto lemma Restr_natLeq: "Restr natLeq {x. x < n} = natLeq_on n" @@ -1341,7 +1341,7 @@ lemma Restr_natLeq2: -"Restr natLeq (rel.underS natLeq n) = natLeq_on n" +"Restr natLeq (underS natLeq n) = natLeq_on n" by (auto simp add: Restr_natLeq natLeq_underS_less) @@ -1728,7 +1728,7 @@ using r' by (simp add: card_of_Field_ordIso[of ?r']) finally have "|K| \o ?r'" . moreover - {let ?L = "UN j : K. rel.underS ?r' j" + {let ?L = "UN j : K. underS ?r' j" let ?J = "Field r" have rJ: "r =o |?J|" using r_card card_of_Field_ordIso ordIso_symmetric by blast @@ -1736,11 +1736,11 @@ hence "|K| <=o r" using r' card_of_Card_order[of K] by blast hence "|K| \o |?J|" using rJ ordLeq_ordIso_trans by blast moreover - {have "ALL j : K. |rel.underS ?r' j| o r" + hence "ALL j : K. |underS ?r' j| \o r" using r' card_of_Card_order by blast - hence "ALL j : K. |rel.underS ?r' j| \o |?J|" + hence "ALL j : K. |underS ?r' j| \o |?J|" using rJ ordLeq_ordIso_trans by blast } ultimately have "|?L| \o |?J|" @@ -1750,7 +1750,7 @@ moreover { have "Field ?r' \ ?L" - using 2 unfolding rel.underS_def cofinal_def by auto + using 2 unfolding underS_def cofinal_def by auto hence "|Field ?r'| \o |?L|" by (simp add: card_of_mono1) hence "?r' \o |?L|" using 22 ordIso_ordLeq_trans ordIso_symmetric by blast diff -r eeba3ba73486 -r 38db7814481d src/HOL/Cardinals/Constructions_on_Wellorders.thy --- a/src/HOL/Cardinals/Constructions_on_Wellorders.thy Thu Jan 16 18:52:50 2014 +0100 +++ b/src/HOL/Cardinals/Constructions_on_Wellorders.thy Thu Jan 16 20:52:54 2014 +0100 @@ -216,7 +216,7 @@ moreover have "ofilter (r Osum r') (Field r)" using 1 proof(auto simp add: wo_rel_def wo_rel.ofilter_def - Field_Osum rel.under_def) + Field_Osum under_def) fix a b assume 2: "a \ Field r" and 3: "(b,a) \ r Osum r'" moreover {assume "(b,a) \ r'" @@ -251,13 +251,13 @@ then obtain r'' where "well_order_on (f ` A) r''" and 1: "r =o r''" using WELL Well_order_iso_copy by blast hence 2: "Well_order r'' \ Field r'' = (f ` A)" - using rel.well_order_on_Well_order by blast + using well_order_on_Well_order by blast (* *) let ?C = "B - (f ` A)" obtain r''' where "well_order_on ?C r'''" using well_order_on by blast hence 3: "Well_order r''' \ Field r''' = ?C" - using rel.well_order_on_Well_order by blast + using well_order_on_Well_order by blast (* *) let ?r' = "r'' Osum r'''" have "Field r'' Int Field r''' = {}" @@ -479,23 +479,18 @@ have bb: "b \ Field r" using bA unfolding underS_def Field_def by auto assume "\a\A. b \ under a" hence 0: "\a \ A. a \ underS b" using A bA unfolding underS_def - by simp (metis (lifting) bb max2_def max2_greater mem_Collect_eq rel.under_def set_rev_mp) - have "(suc A, b) \ r" apply(rule suc_least[OF A bb]) using 0 unfolding rel.underS_def by auto + by simp (metis (lifting) bb max2_def max2_greater mem_Collect_eq under_def set_rev_mp) + have "(suc A, b) \ r" apply(rule suc_least[OF A bb]) using 0 unfolding underS_def by auto thus False using bA unfolding underS_def by simp (metis ANTISYM antisymD) qed -lemma (in rel) AboveS_underS: -assumes "i \ Field r" -shows "i \ AboveS (underS i)" -using assms unfolding AboveS_def underS_def by auto - lemma (in wo_rel) in_underS_supr: assumes j: "j \ underS i" and i: "i \ A" and A: "A \ Field r" and AA: "Above A \ {}" shows "j \ underS (supr A)" proof- have "(i,supr A) \ r" using supr_greater[OF A AA i] . thus ?thesis using j unfolding underS_def - by simp (metis REFL TRANS max2_def max2_equals1 rel.refl_on_domain transD) + by simp (metis REFL TRANS max2_def max2_equals1 refl_on_domain transD) qed lemma inj_on_Field: @@ -530,7 +525,7 @@ and init: "(R ja, R j) \ init_seg_of" hence jja: "{j,ja} \ Field r" and j: "j \ Field r" and ja: "ja \ Field r" and jjai: "(j,i) \ r" "(ja,i) \ r" - and i: "i \ {j,ja}" unfolding Field_def rel.underS_def by auto + and i: "i \ {j,ja}" unfolding Field_def underS_def by auto have jj: "(j,j) \ r" and jaja: "(ja,ja) \ r" using j ja by (metis in_notinI)+ show "R j initial_segment_of R ja" using jja init jjai i @@ -544,7 +539,7 @@ fix j ja assume jS: "j \ Field r" and jaS: "ja \ Field r" and init: "(R ja, R j) \ init_seg_of" hence jja: "{j,ja} \ Field r" and j: "j \ Field r" and ja: "ja \ Field r" - unfolding Field_def rel.underS_def by auto + unfolding Field_def underS_def by auto have jj: "(j,j) \ r" and jaja: "(ja,ja) \ r" using j ja by (metis in_notinI)+ show "R j initial_segment_of R ja" using jja init @@ -700,8 +695,8 @@ assumes "aboveS i \ {}" shows "(j, succ i) \ r \ (j,i) \ r \ j = succ i" apply safe - apply (metis WELL assms in_notinI rel.well_order_on_domain suc_singl_pred succ_def succ_in_diff) - apply (metis (hide_lams, full_types) REFL TRANS assms max2_def max2_equals1 rel.refl_on_domain succ_in_Field succ_not_in transD) + apply (metis WELL assms in_notinI well_order_on_domain suc_singl_pred succ_def succ_in_diff) + apply (metis (hide_lams, full_types) REFL TRANS assms max2_def max2_equals1 refl_on_domain succ_in_Field succ_not_in transD) apply (metis assms in_notinI succ_in_Field) done @@ -926,7 +921,7 @@ lemma oproj_under: assumes f: "oproj r s f" and a: "a \ under r a'" shows "f a \ under s (f a')" -using oproj_in[OF f] a unfolding rel.under_def by auto +using oproj_in[OF f] a unfolding under_def by auto (* An ordinal is embedded in another whenever it is embedded as an order (not necessarily as initial segment):*) @@ -950,55 +945,55 @@ and IH1a: "\ a1. a1 \ underS r a \ inj_on g (under r a1)" and IH1b: "\ a1. a1 \ underS r a \ g ` under r a1 = under s (g a1)" and IH2: "\ a1. a1 \ underS r a \ g a1 \ under s (f a1)" - unfolding rel.underS_def Field_def bij_betw_def by auto + unfolding underS_def Field_def bij_betw_def by auto have fa: "f a \ Field s" using f[OF a] by auto have g: "g a = suc s (g ` underS r a)" using r.worec_fixpoint[OF adm] unfolding g_def fun_eq_iff by simp have A0: "g ` underS r a \ Field s" - using IH1b by (metis IH2 image_subsetI in_mono rel.under_Field) + using IH1b by (metis IH2 image_subsetI in_mono under_Field) {fix a1 assume a1: "a1 \ underS r a" from IH2[OF this] have "g a1 \ under s (f a1)" . moreover have "f a1 \ underS s (f a)" using f[OF a] a1 by auto - ultimately have "g a1 \ underS s (f a)" by (metis s.ANTISYM s.TRANS rel.under_underS_trans) + ultimately have "g a1 \ underS s (f a)" by (metis s.ANTISYM s.TRANS under_underS_trans) } - hence "f a \ AboveS s (g ` underS r a)" unfolding rel.AboveS_def - using fa by simp (metis (lifting, full_types) mem_Collect_eq rel.underS_def) + hence "f a \ AboveS s (g ` underS r a)" unfolding AboveS_def + using fa by simp (metis (lifting, full_types) mem_Collect_eq underS_def) hence A: "AboveS s (g ` underS r a) \ {}" by auto have B: "\ a1. a1 \ underS r a \ g a1 \ underS s (g a)" unfolding g apply(rule s.suc_underS[OF A0 A]) by auto {fix a1 a2 assume a2: "a2 \ underS r a" and 1: "a1 \ underS r a2" hence a12: "{a1,a2} \ under r a2" and "a1 \ a2" using r.REFL a - unfolding rel.underS_def rel.under_def refl_on_def Field_def by auto + unfolding underS_def under_def refl_on_def Field_def by auto hence "g a1 \ g a2" using IH1a[OF a2] unfolding inj_on_def by auto hence "g a1 \ underS s (g a2)" using IH1b[OF a2] a12 - unfolding rel.underS_def rel.under_def by auto + unfolding underS_def under_def by auto } note C = this have ga: "g a \ Field s" unfolding g using s.suc_inField[OF A0 A] . have aa: "a \ under r a" - using a r.REFL unfolding rel.under_def rel.underS_def refl_on_def by auto + using a r.REFL unfolding under_def underS_def refl_on_def by auto show ?case proof safe show "bij_betw g (under r a) (under s (g a))" unfolding bij_betw_def proof safe show "inj_on g (under r a)" proof(rule r.inj_on_Field) fix a1 a2 assume "a1 \ under r a" and a2: "a2 \ under r a" and a1: "a1 \ underS r a2" hence a22: "a2 \ under r a2" and a12: "a1 \ under r a2" "a1 \ a2" - using a r.REFL unfolding rel.under_def rel.underS_def refl_on_def by auto + using a r.REFL unfolding under_def underS_def refl_on_def by auto show "g a1 \ g a2" proof(cases "a2 = a") case False hence "a2 \ underS r a" - using a2 unfolding rel.underS_def rel.under_def by auto + using a2 unfolding underS_def under_def by auto from IH1a[OF this] show ?thesis using a12 a22 unfolding inj_on_def by auto - qed(insert B a1, unfold rel.underS_def, auto) - qed(unfold rel.under_def Field_def, auto) + qed(insert B a1, unfold underS_def, auto) + qed(unfold under_def Field_def, auto) next fix a1 assume a1: "a1 \ under r a" show "g a1 \ under s (g a)" proof(cases "a1 = a") case True thus ?thesis - using ga s.REFL unfolding refl_on_def rel.under_def by auto + using ga s.REFL unfolding refl_on_def under_def by auto next case False - hence a1: "a1 \ underS r a" using a1 unfolding rel.underS_def rel.under_def by auto - thus ?thesis using B unfolding rel.underS_def rel.under_def by auto + hence a1: "a1 \ underS r a" using a1 unfolding underS_def under_def by auto + thus ?thesis using B unfolding underS_def under_def by auto qed next fix b1 assume b1: "b1 \ under s (g a)" @@ -1007,12 +1002,12 @@ case True thus ?thesis using aa by auto next case False - hence "b1 \ underS s (g a)" using b1 unfolding rel.underS_def rel.under_def by auto + hence "b1 \ underS s (g a)" using b1 unfolding underS_def under_def by auto from s.underS_suc[OF this[unfolded g] A0] obtain a1 where a1: "a1 \ underS r a" and b1: "b1 \ under s (g a1)" by auto obtain a2 where "a2 \ under r a1" and b1: "b1 = g a2" using IH1b[OF a1] b1 by auto hence "a2 \ under r a" using a1 - by (metis r.ANTISYM r.TRANS in_mono rel.underS_subset_under rel.under_underS_trans) + by (metis r.ANTISYM r.TRANS in_mono underS_subset_under under_underS_trans) thus ?thesis using b1 by auto qed qed @@ -1022,9 +1017,9 @@ then obtain a1 where a1: "b1 = g a1" and a1: "a1 \ underS r a" by auto hence "b1 \ underS s (f a)" using a by (metis `\a1. a1 \ underS r a \ g a1 \ underS s (f a)`) - thus "f a \ b1 \ (b1, f a) \ s" unfolding rel.underS_def by auto + thus "f a \ b1 \ (b1, f a) \ s" unfolding underS_def by auto qed(insert fa, auto) - thus "g a \ under s (f a)" unfolding rel.under_def by auto + thus "g a \ under s (f a)" unfolding under_def by auto qed qed } @@ -1046,7 +1041,7 @@ theorem oproj_embed: assumes r: "Well_order r" and s: "Well_order s" and f: "oproj r s f" shows "\ g. embed s r g" -proof (rule embedI[OF s r, of "inv_into (Field r) f"], unfold rel.underS_def, safe) +proof (rule embedI[OF s r, of "inv_into (Field r) f"], unfold underS_def, safe) fix b assume "b \ Field s" thus "inv_into (Field r) f b \ Field r" using oproj_Field2[OF f] by (metis imageI inv_into_into) next diff -r eeba3ba73486 -r 38db7814481d src/HOL/Cardinals/Constructions_on_Wellorders_FP.thy --- a/src/HOL/Cardinals/Constructions_on_Wellorders_FP.thy Thu Jan 16 18:52:50 2014 +0100 +++ b/src/HOL/Cardinals/Constructions_on_Wellorders_FP.thy Thu Jan 16 20:52:54 2014 +0100 @@ -116,12 +116,12 @@ lemma ofilter_Restr_under: assumes WELL: "Well_order r" and OF: "wo_rel.ofilter r A" and IN: "a \ A" -shows "rel.under (Restr r A) a = rel.under r a" +shows "under (Restr r A) a = under r a" using assms wo_rel_def -proof(auto simp add: wo_rel.ofilter_def rel.under_def) +proof(auto simp add: wo_rel.ofilter_def under_def) fix b assume *: "a \ A" and "(b,a) \ r" - hence "b \ rel.under r a \ a \ Field r" - unfolding rel.under_def using Field_def by fastforce + hence "b \ under r a \ a \ Field r" + unfolding under_def using Field_def by fastforce thus "b \ A" using * assms by (auto simp add: wo_rel_def wo_rel.ofilter_def) qed @@ -137,7 +137,7 @@ by (auto simp add: wo_rel_def wo_rel.ofilter_def) next fix a assume "a \ Field (Restr r A)" - thus "bij_betw id (rel.under (Restr r A) a) (rel.under r a)" using assms * + thus "bij_betw id (under (Restr r A) a) (under r a)" using assms * by (simp add: ofilter_Restr_under Field_Restr_ofilter) qed next @@ -148,13 +148,13 @@ {fix a assume "a \ A" hence "a \ Field(Restr r A)" using * assms by (simp add: order_on_defs Refl_Field_Restr2) - hence "bij_betw id (rel.under (Restr r A) a) (rel.under r a)" + hence "bij_betw id (under (Restr r A) a) (under r a)" using * unfolding embed_def by auto - hence "rel.under r a \ rel.under (Restr r A) a" + hence "under r a \ under (Restr r A) a" unfolding bij_betw_def by auto - also have "\ \ Field(Restr r A)" by (simp add: rel.under_Field) + also have "\ \ Field(Restr r A)" by (simp add: under_Field) also have "\ \ A" by (simp add: Field_Restr_subset) - finally have "rel.under r a \ A" . + finally have "under r a \ A" . } thus "wo_rel.ofilter r A" using assms * by (simp add: wo_rel_def wo_rel.ofilter_def) qed @@ -173,13 +173,13 @@ by (simp add: Well_order_Restr wo_rel_def) (* Main proof *) show ?thesis using WellB assms - proof(auto simp add: wo_rel.ofilter_def rel.under_def) + proof(auto simp add: wo_rel.ofilter_def under_def) fix a assume "a \ A" and *: "a \ B" hence "a \ Field r" using OFA Well by (auto simp add: wo_rel.ofilter_def) with * show "a \ Field ?rB" using Field by auto next fix a b assume "a \ A" and "(b,a) \ r" - thus "b \ A" using Well OFA by (auto simp add: wo_rel.ofilter_def rel.under_def) + thus "b \ A" using Well OFA by (auto simp add: wo_rel.ofilter_def under_def) qed qed @@ -312,12 +312,12 @@ assume *: "wo_rel.ofilter r A" "A \ Field r" and **: "wo_rel.ofilter r B" "B \ Field r" and ***: "A < B" then obtain a and b where 0: "a \ Field r \ b \ Field r" and - 1: "A = rel.underS r a \ B = rel.underS r b" + 1: "A = underS r a \ B = underS r b" using Well by (auto simp add: wo_rel.ofilter_underS_Field) hence "a \ b" using *** by auto moreover have "(a,b) \ r" using 0 1 Lo *** - by (auto simp add: rel.underS_incl_iff) + by (auto simp add: underS_incl_iff) moreover have "a = wo_rel.suc r A \ b = wo_rel.suc r B" using Well 0 1 by (simp add: wo_rel.suc_underS) @@ -714,10 +714,10 @@ corollary underS_Restr_ordLess: assumes "Well_order r" and "Field r \ {}" -shows "Restr r (rel.underS r a) a \ Field r. r' =o Restr r (rel.underS r a))" +shows "(r' a \ Field r. r' =o Restr r (underS r a))" proof(auto) - fix a assume *: "a \ Field r" and **: "r' =o Restr r (rel.underS r a)" - hence "Restr r (rel.underS r a) Field r" and **: "r' =o Restr r (underS r a)" + hence "Restr r (underS r a) f ` (Field r') \ Field r" unfolding ordLess_def embedS_def[abs_def] bij_betw_def using embed_inj_on by blast hence "wo_rel.ofilter r (f ` (Field r'))" using embed_Field_ofilter by blast - then obtain a where 3: "a \ Field r" and 4: "rel.underS r a = f ` (Field r')" + then obtain a where 3: "a \ Field r" and 4: "underS r a = f ` (Field r')" using 1 2 by (auto simp add: wo_rel.ofilter_underS_Field wo_rel_def) have "iso r' (Restr r (f ` (Field r'))) f" using embed_implies_iso_Restr 2 assms by blast @@ -791,8 +791,8 @@ using WELL Well_order_Restr by blast ultimately have "r' =o Restr r (f ` (Field r'))" using WELL' unfolding ordIso_def by auto - hence "r' =o Restr r (rel.underS r a)" using 4 by auto - thus "\a \ Field r. r' =o Restr r (rel.underS r a)" using 3 by auto + hence "r' =o Restr r (underS r a)" using 4 by auto + thus "\a \ Field r. r' =o Restr r (underS r a)" using 3 by auto qed @@ -801,13 +801,13 @@ proof assume *: "r' Well_order r'" unfolding ordLess_def by auto - with * obtain a where 1: "a \ Field r" and 2: "r' =o Restr r (rel.underS r a)" + with * obtain a where 1: "a \ Field r" and 2: "r' =o Restr r (underS r a)" using ordLess_iff_ordIso_Restr by blast - let ?p = "Restr r (rel.underS r a)" - have "wo_rel.ofilter r (rel.underS r a)" using 0 + let ?p = "Restr r (underS r a)" + have "wo_rel.ofilter r (underS r a)" using 0 by (simp add: wo_rel_def wo_rel.underS_ofilter) - hence "Field ?p = rel.underS r a" using 0 Field_Restr_ofilter by blast - hence "Field ?p < Field r" using rel.underS_Field2 1 by fast + hence "Field ?p = underS r a" using 0 Field_Restr_ofilter by blast + hence "Field ?p < Field r" using underS_Field2 1 by fast moreover have "?p p. Field p < Field r \ r' =o p \ p o r') = (\a \ Field r. Restr r (rel.underS r a) o r') = (\a \ Field r. Restr r (underS r a) o r'" fix a assume "a \ Field r" - hence "Restr r (rel.underS r a) a \ Field r. Restr r (rel.underS r a) a \ Field r. Restr r (underS r a) Field r \ r' =o Restr r (rel.underS r a)" + then obtain a where "a \ Field r \ r' =o Restr r (underS r a)" using assms ordLess_iff_ordIso_Restr by blast hence False using * not_ordLess_ordIso ordIso_symmetric by blast } @@ -879,14 +879,14 @@ shows "r =o r'" proof- have 0: "Well_order r \ Well_order r' \ Field r = A \ Field r' = A" - using assms rel.well_order_on_Well_order by blast + using assms well_order_on_Well_order by blast moreover have "\r r'. well_order_on A r \ well_order_on A r' \ r \o r' \ r =o r'" proof(clarify) fix r r' assume *: "well_order_on A r" and **: "well_order_on A r'" have 2: "Well_order r \ Well_order r' \ Field r = A \ Field r' = A" - using * ** rel.well_order_on_Well_order by blast + using * ** well_order_on_Well_order by blast assume "r \o r'" then obtain f where 1: "embed r r' f" and "inj_on f A \ f ` A \ A" @@ -1137,7 +1137,7 @@ proof- let ?r' = "dir_image r f" have 1: "A = Field r \ Well_order r" - using WELL rel.well_order_on_Well_order by blast + using WELL well_order_on_Well_order by blast hence 2: "iso r ?r' f" using dir_image_iso using BIJ unfolding bij_betw_def by auto hence "f ` (Field r) = Field ?r'" using 1 iso_iff[of r ?r'] by blast @@ -1576,7 +1576,7 @@ lemma bsqr_ofilter: assumes WELL: "Well_order r" and OF: "wo_rel.ofilter (bsqr r) D" and SUB: "D < Field r \ Field r" and - NE: "\ (\a. Field r = rel.under r a)" + NE: "\ (\a. Field r = under r a)" shows "\A. wo_rel.ofilter r A \ A < Field r \ D \ A \ A" proof- let ?r' = "bsqr r" @@ -1587,17 +1587,17 @@ (* *) have "D < Field ?r'" unfolding Field_bsqr using SUB . with OF obtain a1 and a2 where - "(a1,a2) \ Field ?r'" and 1: "D = rel.underS ?r' (a1,a2)" + "(a1,a2) \ Field ?r'" and 1: "D = underS ?r' (a1,a2)" using Well' wo_rel.ofilter_underS_Field[of ?r' D] by auto hence 2: "{a1,a2} \ Field r" unfolding Field_bsqr by auto let ?m = "wo_rel.max2 r a1 a2" - have "D \ (rel.under r ?m) \ (rel.under r ?m)" + have "D \ (under r ?m) \ (under r ?m)" proof(unfold 1) {fix b1 b2 let ?n = "wo_rel.max2 r b1 b2" - assume "(b1,b2) \ rel.underS ?r' (a1,a2)" + assume "(b1,b2) \ underS ?r' (a1,a2)" hence 3: "((b1,b2),(a1,a2)) \ ?r'" - unfolding rel.underS_def by blast + unfolding underS_def by blast hence "(?n,?m) \ r" using WELL by (simp add: bsqr_max2) moreover {have "(b1,b2) \ Field ?r'" using 3 unfolding Field_def by auto @@ -1607,13 +1607,13 @@ } ultimately have "(b1,?m) \ r \ (b2,?m) \ r" using Trans trans_def[of r] by blast - hence "(b1,b2) \ (rel.under r ?m) \ (rel.under r ?m)" unfolding rel.under_def by simp} - thus "rel.underS ?r' (a1,a2) \ (rel.under r ?m) \ (rel.under r ?m)" by auto + hence "(b1,b2) \ (under r ?m) \ (under r ?m)" unfolding under_def by simp} + thus "underS ?r' (a1,a2) \ (under r ?m) \ (under r ?m)" by auto qed - moreover have "wo_rel.ofilter r (rel.under r ?m)" + moreover have "wo_rel.ofilter r (under r ?m)" using Well by (simp add: wo_rel.under_ofilter) - moreover have "rel.under r ?m < Field r" - using NE rel.under_Field[of r ?m] by blast + moreover have "under r ?m < Field r" + using NE under_Field[of r ?m] by blast ultimately show ?thesis by blast qed diff -r eeba3ba73486 -r 38db7814481d src/HOL/Cardinals/Order_Relation_More.thy --- a/src/HOL/Cardinals/Order_Relation_More.thy Thu Jan 16 18:52:50 2014 +0100 +++ b/src/HOL/Cardinals/Order_Relation_More.thy Thu Jan 16 20:52:54 2014 +0100 @@ -14,66 +14,63 @@ subsection {* The upper and lower bounds operators *} -context rel -begin - -lemma aboveS_subset_above: "aboveS a \ above a" +lemma aboveS_subset_above: "aboveS r a \ above r a" by(auto simp add: aboveS_def above_def) -lemma AboveS_subset_Above: "AboveS A \ Above A" +lemma AboveS_subset_Above: "AboveS r A \ Above r A" by(auto simp add: AboveS_def Above_def) -lemma UnderS_disjoint: "A Int (UnderS A) = {}" +lemma UnderS_disjoint: "A Int (UnderS r A) = {}" by(auto simp add: UnderS_def) -lemma aboveS_notIn: "a \ aboveS a" +lemma aboveS_notIn: "a \ aboveS r a" by(auto simp add: aboveS_def) -lemma Refl_above_in: "\Refl r; a \ Field r\ \ a \ above a" +lemma Refl_above_in: "\Refl r; a \ Field r\ \ a \ above r a" by(auto simp add: refl_on_def above_def) -lemma in_Above_under: "a \ Field r \ a \ Above (under a)" +lemma in_Above_under: "a \ Field r \ a \ Above r (under r a)" by(auto simp add: Above_def under_def) -lemma in_Under_above: "a \ Field r \ a \ Under (above a)" +lemma in_Under_above: "a \ Field r \ a \ Under r (above r a)" by(auto simp add: Under_def above_def) -lemma in_UnderS_aboveS: "a \ Field r \ a \ UnderS (aboveS a)" +lemma in_UnderS_aboveS: "a \ Field r \ a \ UnderS r (aboveS r a)" by(auto simp add: UnderS_def aboveS_def) -lemma UnderS_subset_Under: "UnderS A \ Under A" +lemma UnderS_subset_Under: "UnderS r A \ Under r A" by(auto simp add: UnderS_def Under_def) -lemma subset_Above_Under: "B \ Field r \ B \ Above (Under B)" +lemma subset_Above_Under: "B \ Field r \ B \ Above r (Under r B)" by(auto simp add: Above_def Under_def) -lemma subset_Under_Above: "B \ Field r \ B \ Under (Above B)" +lemma subset_Under_Above: "B \ Field r \ B \ Under r (Above r B)" by(auto simp add: Under_def Above_def) -lemma subset_AboveS_UnderS: "B \ Field r \ B \ AboveS (UnderS B)" +lemma subset_AboveS_UnderS: "B \ Field r \ B \ AboveS r (UnderS r B)" by(auto simp add: AboveS_def UnderS_def) -lemma subset_UnderS_AboveS: "B \ Field r \ B \ UnderS (AboveS B)" +lemma subset_UnderS_AboveS: "B \ Field r \ B \ UnderS r (AboveS r B)" by(auto simp add: UnderS_def AboveS_def) lemma Under_Above_Galois: -"\B \ Field r; C \ Field r\ \ (B \ Above C) = (C \ Under B)" +"\B \ Field r; C \ Field r\ \ (B \ Above r C) = (C \ Under r B)" by(unfold Above_def Under_def, blast) lemma UnderS_AboveS_Galois: -"\B \ Field r; C \ Field r\ \ (B \ AboveS C) = (C \ UnderS B)" +"\B \ Field r; C \ Field r\ \ (B \ AboveS r C) = (C \ UnderS r B)" by(unfold AboveS_def UnderS_def, blast) lemma Refl_above_aboveS: -assumes REFL: "Refl r" and IN: "a \ Field r" -shows "above a = aboveS a \ {a}" + assumes REFL: "Refl r" and IN: "a \ Field r" + shows "above r a = aboveS r a \ {a}" proof(unfold above_def aboveS_def, auto) show "(a,a) \ r" using REFL IN refl_on_def[of _ r] by blast qed lemma Linear_order_under_aboveS_Field: -assumes LIN: "Linear_order r" and IN: "a \ Field r" -shows "Field r = under a \ aboveS a" + assumes LIN: "Linear_order r" and IN: "a \ Field r" + shows "Field r = under r a \ aboveS r a" proof(unfold under_def aboveS_def, auto) assume "a \ Field r" "(a, a) \ r" with LIN IN order_on_defs[of _ r] refl_on_def[of _ r] @@ -96,7 +93,7 @@ lemma Linear_order_underS_above_Field: assumes LIN: "Linear_order r" and IN: "a \ Field r" -shows "Field r = underS a \ above a" +shows "Field r = underS r a \ above r a" proof(unfold underS_def above_def, auto) assume "a \ Field r" "(a, a) \ r" with LIN IN order_on_defs[of _ r] refl_on_def[of _ r] @@ -117,155 +114,155 @@ using LIN order_on_defs[of "Field r" r] refl_on_def[of "Field r" r] by blast qed -lemma under_empty: "a \ Field r \ under a = {}" +lemma under_empty: "a \ Field r \ under r a = {}" unfolding Field_def under_def by auto -lemma Under_Field: "Under A \ Field r" +lemma Under_Field: "Under r A \ Field r" by(unfold Under_def Field_def, auto) -lemma UnderS_Field: "UnderS A \ Field r" +lemma UnderS_Field: "UnderS r A \ Field r" by(unfold UnderS_def Field_def, auto) -lemma above_Field: "above a \ Field r" +lemma above_Field: "above r a \ Field r" by(unfold above_def Field_def, auto) -lemma aboveS_Field: "aboveS a \ Field r" +lemma aboveS_Field: "aboveS r a \ Field r" by(unfold aboveS_def Field_def, auto) -lemma Above_Field: "Above A \ Field r" +lemma Above_Field: "Above r A \ Field r" by(unfold Above_def Field_def, auto) lemma Refl_under_Under: assumes REFL: "Refl r" and NE: "A \ {}" -shows "Under A = (\ a \ A. under a)" +shows "Under r A = (\ a \ A. under r a)" proof - show "Under A \ (\ a \ A. under a)" + show "Under r A \ (\ a \ A. under r a)" by(unfold Under_def under_def, auto) next - show "(\ a \ A. under a) \ Under A" + show "(\ a \ A. under r a) \ Under r A" proof(auto) fix x - assume *: "\xa \ A. x \ under xa" + assume *: "\xa \ A. x \ under r xa" hence "\xa \ A. (x,xa) \ r" by (simp add: under_def) moreover {from NE obtain a where "a \ A" by blast - with * have "x \ under a" by simp + with * have "x \ under r a" by simp hence "x \ Field r" - using under_Field[of a] by auto + using under_Field[of r a] by auto } - ultimately show "x \ Under A" + ultimately show "x \ Under r A" unfolding Under_def by auto qed qed lemma Refl_underS_UnderS: assumes REFL: "Refl r" and NE: "A \ {}" -shows "UnderS A = (\ a \ A. underS a)" +shows "UnderS r A = (\ a \ A. underS r a)" proof - show "UnderS A \ (\ a \ A. underS a)" + show "UnderS r A \ (\ a \ A. underS r a)" by(unfold UnderS_def underS_def, auto) next - show "(\ a \ A. underS a) \ UnderS A" + show "(\ a \ A. underS r a) \ UnderS r A" proof(auto) fix x - assume *: "\xa \ A. x \ underS xa" + assume *: "\xa \ A. x \ underS r xa" hence "\xa \ A. x \ xa \ (x,xa) \ r" by (auto simp add: underS_def) moreover {from NE obtain a where "a \ A" by blast - with * have "x \ underS a" by simp + with * have "x \ underS r a" by simp hence "x \ Field r" - using underS_Field[of a] by auto + using underS_Field[of r a] by auto } - ultimately show "x \ UnderS A" + ultimately show "x \ UnderS r A" unfolding UnderS_def by auto qed qed lemma Refl_above_Above: assumes REFL: "Refl r" and NE: "A \ {}" -shows "Above A = (\ a \ A. above a)" +shows "Above r A = (\ a \ A. above r a)" proof - show "Above A \ (\ a \ A. above a)" + show "Above r A \ (\ a \ A. above r a)" by(unfold Above_def above_def, auto) next - show "(\ a \ A. above a) \ Above A" + show "(\ a \ A. above r a) \ Above r A" proof(auto) fix x - assume *: "\xa \ A. x \ above xa" + assume *: "\xa \ A. x \ above r xa" hence "\xa \ A. (xa,x) \ r" by (simp add: above_def) moreover {from NE obtain a where "a \ A" by blast - with * have "x \ above a" by simp + with * have "x \ above r a" by simp hence "x \ Field r" - using above_Field[of a] by auto + using above_Field[of r a] by auto } - ultimately show "x \ Above A" + ultimately show "x \ Above r A" unfolding Above_def by auto qed qed lemma Refl_aboveS_AboveS: assumes REFL: "Refl r" and NE: "A \ {}" -shows "AboveS A = (\ a \ A. aboveS a)" +shows "AboveS r A = (\ a \ A. aboveS r a)" proof - show "AboveS A \ (\ a \ A. aboveS a)" + show "AboveS r A \ (\ a \ A. aboveS r a)" by(unfold AboveS_def aboveS_def, auto) next - show "(\ a \ A. aboveS a) \ AboveS A" + show "(\ a \ A. aboveS r a) \ AboveS r A" proof(auto) fix x - assume *: "\xa \ A. x \ aboveS xa" + assume *: "\xa \ A. x \ aboveS r xa" hence "\xa \ A. xa \ x \ (xa,x) \ r" by (auto simp add: aboveS_def) moreover {from NE obtain a where "a \ A" by blast - with * have "x \ aboveS a" by simp + with * have "x \ aboveS r a" by simp hence "x \ Field r" - using aboveS_Field[of a] by auto + using aboveS_Field[of r a] by auto } - ultimately show "x \ AboveS A" + ultimately show "x \ AboveS r A" unfolding AboveS_def by auto qed qed -lemma under_Under_singl: "under a = Under {a}" +lemma under_Under_singl: "under r a = Under r {a}" by(unfold Under_def under_def, auto simp add: Field_def) -lemma underS_UnderS_singl: "underS a = UnderS {a}" +lemma underS_UnderS_singl: "underS r a = UnderS r {a}" by(unfold UnderS_def underS_def, auto simp add: Field_def) -lemma above_Above_singl: "above a = Above {a}" +lemma above_Above_singl: "above r a = Above r {a}" by(unfold Above_def above_def, auto simp add: Field_def) -lemma aboveS_AboveS_singl: "aboveS a = AboveS {a}" +lemma aboveS_AboveS_singl: "aboveS r a = AboveS r {a}" by(unfold AboveS_def aboveS_def, auto simp add: Field_def) -lemma Under_decr: "A \ B \ Under B \ Under A" +lemma Under_decr: "A \ B \ Under r B \ Under r A" by(unfold Under_def, auto) -lemma UnderS_decr: "A \ B \ UnderS B \ UnderS A" +lemma UnderS_decr: "A \ B \ UnderS r B \ UnderS r A" by(unfold UnderS_def, auto) -lemma Above_decr: "A \ B \ Above B \ Above A" +lemma Above_decr: "A \ B \ Above r B \ Above r A" by(unfold Above_def, auto) -lemma AboveS_decr: "A \ B \ AboveS B \ AboveS A" +lemma AboveS_decr: "A \ B \ AboveS r B \ AboveS r A" by(unfold AboveS_def, auto) lemma under_incl_iff: assumes TRANS: "trans r" and REFL: "Refl r" and IN: "a \ Field r" -shows "(under a \ under b) = ((a,b) \ r)" +shows "(under r a \ under r b) = ((a,b) \ r)" proof assume "(a,b) \ r" - thus "under a \ under b" using TRANS + thus "under r a \ under r b" using TRANS by (auto simp add: under_incr) next - assume "under a \ under b" + assume "under r a \ under r b" moreover - have "a \ under a" using REFL IN + have "a \ under r a" using REFL IN by (auto simp add: Refl_under_in) ultimately show "(a,b) \ r" by (auto simp add: under_def) @@ -273,7 +270,7 @@ lemma above_decr: assumes TRANS: "trans r" and REL: "(a,b) \ r" -shows "above b \ above a" +shows "above r b \ above r a" proof(unfold above_def, auto) fix x assume "(b,x) \ r" with REL TRANS trans_def[of r] @@ -283,7 +280,7 @@ lemma aboveS_decr: assumes TRANS: "trans r" and ANTISYM: "antisym r" and REL: "(a,b) \ r" -shows "aboveS b \ aboveS a" +shows "aboveS r b \ aboveS r a" proof(unfold aboveS_def, auto) assume *: "a \ b" and **: "(b,a) \ r" with ANTISYM antisym_def[of r] REL @@ -296,11 +293,11 @@ lemma under_trans: assumes TRANS: "trans r" and - IN1: "a \ under b" and IN2: "b \ under c" -shows "a \ under c" + IN1: "a \ under r b" and IN2: "b \ under r c" +shows "a \ under r c" proof- have "(a,b) \ r \ (b,c) \ r" - using IN1 IN2 under_def by auto + using IN1 IN2 under_def by fastforce hence "(a,c) \ r" using TRANS trans_def[of r] by blast thus ?thesis unfolding under_def by simp @@ -308,14 +305,14 @@ lemma under_underS_trans: assumes TRANS: "trans r" and ANTISYM: "antisym r" and - IN1: "a \ under b" and IN2: "b \ underS c" -shows "a \ underS c" + IN1: "a \ under r b" and IN2: "b \ underS r c" +shows "a \ underS r c" proof- have 0: "(a,b) \ r \ (b,c) \ r" - using IN1 IN2 under_def underS_def by auto + using IN1 IN2 under_def underS_def by fastforce hence 1: "(a,c) \ r" using TRANS trans_def[of r] by blast - have 2: "b \ c" using IN2 underS_def by auto + have 2: "b \ c" using IN2 underS_def by force have 3: "a \ c" proof assume "a = c" with 0 2 ANTISYM antisym_def[of r] @@ -326,14 +323,14 @@ lemma underS_under_trans: assumes TRANS: "trans r" and ANTISYM: "antisym r" and - IN1: "a \ underS b" and IN2: "b \ under c" -shows "a \ underS c" + IN1: "a \ underS r b" and IN2: "b \ under r c" +shows "a \ underS r c" proof- have 0: "(a,b) \ r \ (b,c) \ r" - using IN1 IN2 under_def underS_def by auto + using IN1 IN2 under_def underS_def by fast hence 1: "(a,c) \ r" - using TRANS trans_def[of r] by blast - have 2: "a \ b" using IN1 underS_def by auto + using TRANS trans_def[of r] by fast + have 2: "a \ b" using IN1 underS_def by force have 3: "a \ c" proof assume "a = c" with 0 2 ANTISYM antisym_def[of r] @@ -344,21 +341,21 @@ lemma underS_underS_trans: assumes TRANS: "trans r" and ANTISYM: "antisym r" and - IN1: "a \ underS b" and IN2: "b \ underS c" -shows "a \ underS c" + IN1: "a \ underS r b" and IN2: "b \ underS r c" +shows "a \ underS r c" proof- - have "a \ under b" - using IN1 underS_subset_under by auto - with assms under_underS_trans show ?thesis by auto + have "a \ under r b" + using IN1 underS_subset_under by fast + with assms under_underS_trans show ?thesis by fast qed lemma above_trans: assumes TRANS: "trans r" and - IN1: "b \ above a" and IN2: "c \ above b" -shows "c \ above a" + IN1: "b \ above r a" and IN2: "c \ above r b" +shows "c \ above r a" proof- have "(a,b) \ r \ (b,c) \ r" - using IN1 IN2 above_def by auto + using IN1 IN2 above_def by fast hence "(a,c) \ r" using TRANS trans_def[of r] by blast thus ?thesis unfolding above_def by simp @@ -366,14 +363,14 @@ lemma above_aboveS_trans: assumes TRANS: "trans r" and ANTISYM: "antisym r" and - IN1: "b \ above a" and IN2: "c \ aboveS b" -shows "c \ aboveS a" + IN1: "b \ above r a" and IN2: "c \ aboveS r b" +shows "c \ aboveS r a" proof- have 0: "(a,b) \ r \ (b,c) \ r" - using IN1 IN2 above_def aboveS_def by auto + using IN1 IN2 above_def aboveS_def by fast hence 1: "(a,c) \ r" using TRANS trans_def[of r] by blast - have 2: "b \ c" using IN2 aboveS_def by auto + have 2: "b \ c" using IN2 aboveS_def by force have 3: "a \ c" proof assume "a = c" with 0 2 ANTISYM antisym_def[of r] @@ -384,14 +381,14 @@ lemma aboveS_above_trans: assumes TRANS: "trans r" and ANTISYM: "antisym r" and - IN1: "b \ aboveS a" and IN2: "c \ above b" -shows "c \ aboveS a" + IN1: "b \ aboveS r a" and IN2: "c \ above r b" +shows "c \ aboveS r a" proof- have 0: "(a,b) \ r \ (b,c) \ r" - using IN1 IN2 above_def aboveS_def by auto + using IN1 IN2 above_def aboveS_def by fast hence 1: "(a,c) \ r" using TRANS trans_def[of r] by blast - have 2: "a \ b" using IN1 aboveS_def by auto + have 2: "a \ b" using IN1 aboveS_def by force have 3: "a \ c" proof assume "a = c" with 0 2 ANTISYM antisym_def[of r] @@ -402,21 +399,23 @@ lemma aboveS_aboveS_trans: assumes TRANS: "trans r" and ANTISYM: "antisym r" and - IN1: "b \ aboveS a" and IN2: "c \ aboveS b" -shows "c \ aboveS a" + IN1: "b \ aboveS r a" and IN2: "c \ aboveS r b" +shows "c \ aboveS r a" proof- - have "b \ above a" - using IN1 aboveS_subset_above by auto - with assms above_aboveS_trans show ?thesis by auto + have "b \ above r a" + using IN1 aboveS_subset_above by fast + with assms above_aboveS_trans show ?thesis by fast qed lemma under_Under_trans: assumes TRANS: "trans r" and - IN1: "a \ under b" and IN2: "b \ Under C" -shows "a \ Under C" + IN1: "a \ under r b" and IN2: "b \ Under r C" +shows "a \ Under r C" proof- - have "(a,b) \ r \ (\c \ C. (b,c) \ r)" - using IN1 IN2 under_def Under_def by blast + have "b \ {u \ Field r. \x. x \ C \ (u, x) \ r}" + using IN2 Under_def by force + hence "(a,b) \ r \ (\c \ C. (b,c) \ r)" + using IN1 under_def by fast hence "\c \ C. (a,c) \ r" using TRANS trans_def[of r] by blast moreover @@ -427,22 +426,22 @@ lemma underS_Under_trans: assumes TRANS: "trans r" and ANTISYM: "antisym r" and - IN1: "a \ underS b" and IN2: "b \ Under C" -shows "a \ UnderS C" + IN1: "a \ underS r b" and IN2: "b \ Under r C" +shows "a \ UnderS r C" proof- - from IN1 have "a \ under b" - using underS_subset_under[of b] by blast + from IN1 have "a \ under r b" + using underS_subset_under[of r b] by fast with assms under_Under_trans - have "a \ Under C" by auto + have "a \ Under r C" by fast (* *) moreover have "a \ C" proof assume *: "a \ C" have 1: "b \ a \ (a,b) \ r" - using IN1 underS_def[of b] by auto + using IN1 underS_def[of r b] by auto have "\c \ C. (b,c) \ r" - using IN2 Under_def[of C] by auto + using IN2 Under_def[of r C] by auto with * have "(b,a) \ r" by simp with 1 ANTISYM antisym_def[of r] show False by blast @@ -450,53 +449,53 @@ (* *) ultimately show ?thesis unfolding UnderS_def - using Under_def by auto + using Under_def by force qed lemma underS_UnderS_trans: assumes TRANS: "trans r" and ANTISYM: "antisym r" and - IN1: "a \ underS b" and IN2: "b \ UnderS C" -shows "a \ UnderS C" + IN1: "a \ underS r b" and IN2: "b \ UnderS r C" +shows "a \ UnderS r C" proof- - from IN2 have "b \ Under C" - using UnderS_subset_Under[of C] by blast + from IN2 have "b \ Under r C" + using UnderS_subset_Under[of r C] by blast with underS_Under_trans assms - show ?thesis by auto + show ?thesis by force qed lemma above_Above_trans: assumes TRANS: "trans r" and - IN1: "a \ above b" and IN2: "b \ Above C" -shows "a \ Above C" + IN1: "a \ above r b" and IN2: "b \ Above r C" +shows "a \ Above r C" proof- have "(b,a) \ r \ (\c \ C. (c,b) \ r)" - using IN1 IN2 above_def Above_def by auto + using IN1[unfolded above_def] IN2[unfolded Above_def] by simp hence "\c \ C. (c,a) \ r" using TRANS trans_def[of r] by blast moreover - have "a \ Field r" using IN1 Field_def above_def by force + have "a \ Field r" using IN1[unfolded above_def] Field_def by fast ultimately show ?thesis unfolding Above_def by auto qed lemma aboveS_Above_trans: assumes TRANS: "trans r" and ANTISYM: "antisym r" and - IN1: "a \ aboveS b" and IN2: "b \ Above C" -shows "a \ AboveS C" + IN1: "a \ aboveS r b" and IN2: "b \ Above r C" +shows "a \ AboveS r C" proof- - from IN1 have "a \ above b" - using aboveS_subset_above[of b] by blast + from IN1 have "a \ above r b" + using aboveS_subset_above[of r b] by blast with assms above_Above_trans - have "a \ Above C" by auto + have "a \ Above r C" by fast (* *) moreover have "a \ C" proof assume *: "a \ C" have 1: "b \ a \ (b,a) \ r" - using IN1 aboveS_def[of b] by auto + using IN1 aboveS_def[of r b] by auto have "\c \ C. (c,b) \ r" - using IN2 Above_def[of C] by auto + using IN2 Above_def[of r C] by auto with * have "(a,b) \ r" by simp with 1 ANTISYM antisym_def[of r] show False by blast @@ -504,27 +503,27 @@ (* *) ultimately show ?thesis unfolding AboveS_def - using Above_def by auto + using Above_def by force qed lemma above_AboveS_trans: assumes TRANS: "trans r" and ANTISYM: "antisym r" and - IN1: "a \ above b" and IN2: "b \ AboveS C" -shows "a \ AboveS C" + IN1: "a \ above r b" and IN2: "b \ AboveS r C" +shows "a \ AboveS r C" proof- - from IN2 have "b \ Above C" - using AboveS_subset_Above[of C] by blast + from IN2 have "b \ Above r C" + using AboveS_subset_Above[of r C] by blast with assms above_Above_trans - have "a \ Above C" by auto + have "a \ Above r C" by force (* *) moreover have "a \ C" proof assume *: "a \ C" have 1: "(b,a) \ r" - using IN1 above_def[of b] by auto + using IN1 above_def[of r b] by auto have "\c \ C. b \ c \ (c,b) \ r" - using IN2 AboveS_def[of C] by auto + using IN2 AboveS_def[of r C] by auto with * have "b \ a \ (a,b) \ r" by simp with 1 ANTISYM antisym_def[of r] show False by blast @@ -532,38 +531,38 @@ (* *) ultimately show ?thesis unfolding AboveS_def - using Above_def by auto + using Above_def by force qed lemma aboveS_AboveS_trans: assumes TRANS: "trans r" and ANTISYM: "antisym r" and - IN1: "a \ aboveS b" and IN2: "b \ AboveS C" -shows "a \ AboveS C" + IN1: "a \ aboveS r b" and IN2: "b \ AboveS r C" +shows "a \ AboveS r C" proof- - from IN2 have "b \ Above C" - using AboveS_subset_Above[of C] by blast + from IN2 have "b \ Above r C" + using AboveS_subset_Above[of r C] by blast with aboveS_Above_trans assms - show ?thesis by auto + show ?thesis by force qed lemma under_UnderS_trans: assumes TRANS: "trans r" and ANTISYM: "antisym r" and - IN1: "a \ under b" and IN2: "b \ UnderS C" -shows "a \ UnderS C" + IN1: "a \ under r b" and IN2: "b \ UnderS r C" +shows "a \ UnderS r C" proof- - from IN2 have "b \ Under C" - using UnderS_subset_Under[of C] by blast + from IN2 have "b \ Under r C" + using UnderS_subset_Under[of r C] by blast with assms under_Under_trans - have "a \ Under C" by blast + have "a \ Under r C" by force (* *) moreover have "a \ C" proof assume *: "a \ C" have 1: "(a,b) \ r" - using IN1 under_def[of b] by auto + using IN1 under_def[of r b] by auto have "\c \ C. b \ c \ (b,c) \ r" - using IN2 UnderS_def[of C] by blast + using IN2 UnderS_def[of r C] by blast with * have "b \ a \ (b,a) \ r" by blast with 1 ANTISYM antisym_def[of r] show False by blast @@ -573,66 +572,59 @@ show ?thesis unfolding UnderS_def Under_def by fast qed -end (* context rel *) - subsection {* Properties depending on more than one relation *} -abbreviation "under \ rel.under" -abbreviation "underS \ rel.underS" -abbreviation "Under \ rel.Under" -abbreviation "UnderS \ rel.UnderS" -abbreviation "above \ rel.above" -abbreviation "aboveS \ rel.aboveS" -abbreviation "Above \ rel.Above" -abbreviation "AboveS \ rel.AboveS" - lemma under_incr2: "r \ r' \ under r a \ under r' a" -unfolding rel.under_def by blast +unfolding under_def by blast lemma underS_incr2: "r \ r' \ underS r a \ underS r' a" -unfolding rel.underS_def by blast +unfolding underS_def by blast +(* FIXME: r \ r' lemma Under_incr: "r \ r' \ Under r A \ Under r A" -unfolding rel.Under_def by blast +unfolding Under_def by blast lemma UnderS_incr: "r \ r' \ UnderS r A \ UnderS r A" -unfolding rel.UnderS_def by blast +unfolding UnderS_def by blast lemma Under_incr_decr: "\r \ r'; A' \ A\ \ Under r A \ Under r A'" -unfolding rel.Under_def by blast +unfolding Under_def by blast lemma UnderS_incr_decr: "\r \ r'; A' \ A\ \ UnderS r A \ UnderS r A'" -unfolding rel.UnderS_def by blast +unfolding UnderS_def by blast +*) lemma above_incr2: "r \ r' \ above r a \ above r' a" -unfolding rel.above_def by blast +unfolding above_def by blast lemma aboveS_incr2: "r \ r' \ aboveS r a \ aboveS r' a" -unfolding rel.aboveS_def by blast +unfolding aboveS_def by blast +(* FIXME lemma Above_incr: "r \ r' \ Above r A \ Above r A" -unfolding rel.Above_def by blast +unfolding Above_def by blast lemma AboveS_incr: "r \ r' \ AboveS r A \ AboveS r A" -unfolding rel.AboveS_def by blast +unfolding AboveS_def by blast lemma Above_incr_decr: -"\r \ r'; A' \ A\ \ Above r A \ Above r A'" -unfolding rel.Above_def by blast +"\r \ r'; A' \ A\ \ Above r A \ Above r A'" +unfolding Above_def by blast lemma AboveS_incr_decr: -"\r \ r'; A' \ A\ \ AboveS r A \ AboveS r A'" -unfolding rel.AboveS_def by blast +"\r \ r'; A' \ A\ \ AboveS r A \ AboveS r A'" +unfolding AboveS_def by blast +*) end diff -r eeba3ba73486 -r 38db7814481d src/HOL/Cardinals/Order_Relation_More_FP.thy --- a/src/HOL/Cardinals/Order_Relation_More_FP.thy Thu Jan 16 18:52:50 2014 +0100 +++ b/src/HOL/Cardinals/Order_Relation_More_FP.thy Thu Jan 16 20:52:54 2014 +0100 @@ -19,16 +19,6 @@ further define upper and lower bounds operators. *} -locale rel = fixes r :: "'a rel" - -text{* The following context encompasses all this section, except -for its last subsection. In other words, for the rest of this section except its last -subsection, we consider a fixed relation @{text "r"}. *} - -context rel -begin - - subsection {* Auxiliaries *} @@ -39,7 +29,7 @@ corollary well_order_on_domain: "\well_order_on A r; (a,b) \ r\ \ a \ A \ b \ A" -by(simp add: refl_on_domain order_on_defs) +by (auto simp add: refl_on_domain order_on_defs) lemma well_order_on_Field: @@ -49,7 +39,7 @@ lemma well_order_on_Well_order: "well_order_on A r \ A = Field r \ Well_order r" -using well_order_on_Field by simp +using well_order_on_Field by auto lemma Total_subset_Id: @@ -91,103 +81,91 @@ Capitalization of the first letter in the name reminds that the operator acts on sets, rather than on individual elements. *} -definition under::"'a \ 'a set" -where "under a \ {b. (b,a) \ r}" +definition under::"'a rel \ 'a \ 'a set" +where "under r a \ {b. (b,a) \ r}" -definition underS::"'a \ 'a set" -where "underS a \ {b. b \ a \ (b,a) \ r}" +definition underS::"'a rel \ 'a \ 'a set" +where "underS r a \ {b. b \ a \ (b,a) \ r}" -definition Under::"'a set \ 'a set" -where "Under A \ {b \ Field r. \a \ A. (b,a) \ r}" +definition Under::"'a rel \ 'a set \ 'a set" +where "Under r A \ {b \ Field r. \a \ A. (b,a) \ r}" -definition UnderS::"'a set \ 'a set" -where "UnderS A \ {b \ Field r. \a \ A. b \ a \ (b,a) \ r}" +definition UnderS::"'a rel \ 'a set \ 'a set" +where "UnderS r A \ {b \ Field r. \a \ A. b \ a \ (b,a) \ r}" -definition above::"'a \ 'a set" -where "above a \ {b. (a,b) \ r}" +definition above::"'a rel \ 'a \ 'a set" +where "above r a \ {b. (a,b) \ r}" -definition aboveS::"'a \ 'a set" -where "aboveS a \ {b. b \ a \ (a,b) \ r}" +definition aboveS::"'a rel \ 'a \ 'a set" +where "aboveS r a \ {b. b \ a \ (a,b) \ r}" -definition Above::"'a set \ 'a set" -where "Above A \ {b \ Field r. \a \ A. (a,b) \ r}" +definition Above::"'a rel \ 'a set \ 'a set" +where "Above r A \ {b \ Field r. \a \ A. (a,b) \ r}" -definition AboveS::"'a set \ 'a set" -where "AboveS A \ {b \ Field r. \a \ A. b \ a \ (a,b) \ r}" -(* *) +definition AboveS::"'a rel \ 'a set \ 'a set" +where "AboveS r A \ {b \ Field r. \a \ A. b \ a \ (a,b) \ r}" text{* Note: In the definitions of @{text "Above[S]"} and @{text "Under[S]"}, we bounded comprehension by @{text "Field r"} in order to properly cover the case of @{text "A"} being empty. *} - -lemma underS_subset_under: "underS a \ under a" +lemma underS_subset_under: "underS r a \ under r a" by(auto simp add: underS_def under_def) -lemma underS_notIn: "a \ underS a" +lemma underS_notIn: "a \ underS r a" by(simp add: underS_def) -lemma Refl_under_in: "\Refl r; a \ Field r\ \ a \ under a" +lemma Refl_under_in: "\Refl r; a \ Field r\ \ a \ under r a" by(simp add: refl_on_def under_def) -lemma AboveS_disjoint: "A Int (AboveS A) = {}" +lemma AboveS_disjoint: "A Int (AboveS r A) = {}" by(auto simp add: AboveS_def) - -lemma in_AboveS_underS: "a \ Field r \ a \ AboveS (underS a)" +lemma in_AboveS_underS: "a \ Field r \ a \ AboveS r (underS r a)" by(auto simp add: AboveS_def underS_def) - lemma Refl_under_underS: -assumes "Refl r" "a \ Field r" -shows "under a = underS a \ {a}" + assumes "Refl r" "a \ Field r" + shows "under r a = underS r a \ {a}" unfolding under_def underS_def using assms refl_on_def[of _ r] by fastforce - -lemma underS_empty: "a \ Field r \ underS a = {}" +lemma underS_empty: "a \ Field r \ underS r a = {}" by (auto simp: Field_def underS_def) - -lemma under_Field: "under a \ Field r" +lemma under_Field: "under r a \ Field r" by(unfold under_def Field_def, auto) - -lemma underS_Field: "underS a \ Field r" +lemma underS_Field: "underS r a \ Field r" by(unfold underS_def Field_def, auto) - lemma underS_Field2: -"a \ Field r \ underS a < Field r" -using assms underS_notIn underS_Field by blast - +"a \ Field r \ underS r a < Field r" +using underS_notIn underS_Field by fast lemma underS_Field3: -"Field r \ {} \ underS a < Field r" +"Field r \ {} \ underS r a < Field r" by(cases "a \ Field r", simp add: underS_Field2, auto simp add: underS_empty) - -lemma AboveS_Field: "AboveS A \ Field r" +lemma AboveS_Field: "AboveS r A \ Field r" by(unfold AboveS_def Field_def, auto) - lemma under_incr: -assumes TRANS: "trans r" and REL: "(a,b) \ r" -shows "under a \ under b" + assumes TRANS: "trans r" and REL: "(a,b) \ r" + shows "under r a \ under r b" proof(unfold under_def, auto) fix x assume "(x,a) \ r" with REL TRANS trans_def[of r] show "(x,b) \ r" by blast qed - lemma underS_incr: assumes TRANS: "trans r" and ANTISYM: "antisym r" and REL: "(a,b) \ r" -shows "underS a \ underS b" +shows "underS r a \ underS r b" proof(unfold underS_def, auto) assume *: "b \ a" and **: "(b,a) \ r" with ANTISYM antisym_def[of r] REL @@ -198,25 +176,24 @@ show "(x,b) \ r" by blast qed - lemma underS_incl_iff: assumes LO: "Linear_order r" and INa: "a \ Field r" and INb: "b \ Field r" -shows "(underS a \ underS b) = ((a,b) \ r)" +shows "(underS r a \ underS r b) = ((a,b) \ r)" proof assume "(a,b) \ r" - thus "underS a \ underS b" using LO + thus "underS r a \ underS r b" using LO by (simp add: order_on_defs underS_incr) next - assume *: "underS a \ underS b" + assume *: "underS r a \ underS r b" {assume "a = b" hence "(a,b) \ r" using assms by (simp add: order_on_defs refl_on_def) } moreover {assume "a \ b \ (b,a) \ r" - hence "b \ underS a" unfolding underS_def by blast - hence "b \ underS b" using * by blast + hence "b \ underS r a" unfolding underS_def by blast + hence "b \ underS r b" using * by blast hence False by (simp add: underS_notIn) } ultimately @@ -224,7 +201,4 @@ order_on_defs[of "Field r" r] total_on_def[of "Field r" r] by blast qed - -end (* context rel *) - end diff -r eeba3ba73486 -r 38db7814481d src/HOL/Cardinals/Ordinal_Arithmetic.thy --- a/src/HOL/Cardinals/Ordinal_Arithmetic.thy Thu Jan 16 18:52:50 2014 +0100 +++ b/src/HOL/Cardinals/Ordinal_Arithmetic.thy Thu Jan 16 20:52:54 2014 +0100 @@ -148,7 +148,7 @@ have "compat r (r +o r') Inl" unfolding compat_def osum_def by auto moreover have "ofilter (r +o r') (Inl ` Field r)" - unfolding wo_rel.ofilter_def[unfolded wo_rel_def, OF 1] Field_osum rel.under_def + unfolding wo_rel.ofilter_def[unfolded wo_rel_def, OF 1] Field_osum under_def unfolding osum_def Field_def by auto ultimately show ?thesis using assms by (auto simp add: embed_iff_compat_inj_on_ofilter) qed @@ -322,7 +322,7 @@ from r' have "compat r (r *o r') ?f" unfolding compat_def oprod_def by auto moreover from * have "ofilter (r *o r') (?f ` Field r)" - unfolding wo_rel.ofilter_def[unfolded wo_rel_def, OF 1] Field_oprod rel.under_def + unfolding wo_rel.ofilter_def[unfolded wo_rel_def, OF 1] Field_oprod under_def unfolding oprod_def by auto (auto simp: image_iff Field_def) moreover have "inj_on ?f (Field r)" unfolding inj_on_def by auto ultimately show ?thesis using assms by (auto simp add: embed_iff_compat_inj_on_ofilter) @@ -924,11 +924,11 @@ lemma iso_ozero_empty[simp]: "r =o ozero = (r = {})" unfolding ozero_def ordIso_def iso_def[abs_def] embed_def bij_betw_def - by (auto dest: rel.well_order_on_domain) + by (auto dest: well_order_on_domain) lemma ozero_ordLeq: assumes "Well_order r" shows "ozero \o r" -using assms unfolding ozero_def ordLeq_def embed_def[abs_def] rel.under_def by auto +using assms unfolding ozero_def ordLeq_def embed_def[abs_def] under_def by auto definition "oone = {((),())}" @@ -942,10 +942,10 @@ lemma oone_ordIso: "oone =o {(x,x)}" unfolding ordIso_def oone_def well_order_on_def linear_order_on_def partial_order_on_def preorder_on_def total_on_def refl_on_def trans_def antisym_def - by (auto simp: iso_def embed_def bij_betw_def rel.under_def inj_on_def intro!: exI[of _ "\_. x"]) + by (auto simp: iso_def embed_def bij_betw_def under_def inj_on_def intro!: exI[of _ "\_. x"]) lemma osum_ordLeqR: "Well_order r \ Well_order s \ s \o r +o s" - unfolding ordLeq_def2 rel.underS_def + unfolding ordLeq_def2 underS_def by (auto intro!: exI[of _ Inr] osum_Well_order) (auto simp add: osum_def Field_def) lemma osum_congL: @@ -1043,7 +1043,7 @@ unfolding Field_oprod iso_def bij_betw_def inj_on_def by fastforce with f have "bij_betw ?f (Field ?L) (Field ?R)" unfolding Field_oprod iso_def bij_betw_def by (auto intro!: map_pair_surj_on) - moreover from f rel.well_order_on_domain[OF r] have "compat ?L ?R ?f" + moreover from f well_order_on_domain[OF r] have "compat ?L ?R ?f" unfolding iso_iff3[OF r s] compat_def oprod_def bij_betw_def by (auto simp: map_pair_imageI dest: inj_onD) ultimately have "iso ?L ?R ?f" by (subst iso_iff3) (auto intro: oprod_Well_order r s t) @@ -1057,7 +1057,7 @@ assms[unfolded ordIso_def] by auto lemma Field_singleton[simp]: "Field {(z,z)} = {z}" - by (metis rel.well_order_on_Field well_order_on_singleton) + by (metis well_order_on_Field well_order_on_singleton) lemma zero_singleton[simp]: "zero {(z,z)} = z" using wo_rel.zero_in_Field[unfolded wo_rel_def, of "{(z, z)}"] well_order_on_singleton[of z] @@ -1077,7 +1077,7 @@ then obtain x where "x \ Field r" by auto with * have Fr: "Field r = {x}" by auto interpret r: wo_rel r by unfold_locales (rule r) - from Fr r.well_order_on_domain[OF r] refl_onD[OF r.REFL, of x] have r_def: "r = {(x, x)}" by fast + from Fr well_order_on_domain[OF r] refl_onD[OF r.REFL, of x] have r_def: "r = {(x, x)}" by fast interpret wo_rel2 r s by unfold_locales (rule r, rule s) have "bij_betw (\x. ()) (Field ?L) (Field ?R)" unfolding bij_betw_def Field_oexp by (auto simp: r_def FinFunc_singleton) @@ -1138,7 +1138,7 @@ interpret t!: wo_rel t by unfold_locales (rule t) interpret rt!: wo_rel ?R by unfold_locales (rule osum_Well_order[OF r t]) from *(3) have "ofilter ?R (?f ` Field ?L)" - unfolding t.ofilter_def rt.ofilter_def Field_osum image_Un image_image rel.under_def + unfolding t.ofilter_def rt.ofilter_def Field_osum image_Un image_image under_def by (auto simp: osum_def intro!: imageI) (auto simp: Field_def) ultimately have "embed ?L ?R ?f" using embed_iff_compat_inj_on_ofilter[of ?L ?R ?f] by (auto intro: osum_Well_order r s t) @@ -1157,7 +1157,7 @@ let ?f = "sum_map f id" from f have "\a\Field (r +o t). ?f a \ Field (s +o t) \ ?f ` underS (r +o t) a \ underS (s +o t) (?f a)" - unfolding Field_osum rel.underS_def by (fastforce simp: osum_def) + unfolding Field_osum underS_def by (fastforce simp: osum_def) thus ?thesis unfolding ordLeq_def2 by (auto intro: osum_Well_order r s t) qed @@ -1199,13 +1199,13 @@ from *(1) have "inj_on ?f (Field ?L)" unfolding Field_oprod inj_on_def by fastforce moreover from *(2,4) the_inv_into_f_f[OF *(1)] have "compat ?L ?R ?f" unfolding compat_def oprod_def - by auto (metis rel.well_order_on_domain t, metis rel.well_order_on_domain s) + by auto (metis well_order_on_domain t, metis well_order_on_domain s) moreover interpret t!: wo_rel t by unfold_locales (rule t) interpret rt!: wo_rel ?R by unfold_locales (rule oprod_Well_order[OF r t]) from *(3) have "ofilter ?R (?f ` Field ?L)" - unfolding t.ofilter_def rt.ofilter_def Field_oprod rel.under_def - by (auto simp: oprod_def image_iff) (fast | metis r rel.well_order_on_domain)+ + unfolding t.ofilter_def rt.ofilter_def Field_oprod under_def + by (auto simp: oprod_def image_iff) (fast | metis r well_order_on_domain)+ ultimately have "embed ?L ?R ?f" using embed_iff_compat_inj_on_ofilter[of ?L ?R ?f] by (auto intro: oprod_Well_order r s t) moreover @@ -1226,7 +1226,7 @@ let ?f = "map_pair f id" from f have "\a\Field (r *o t). ?f a \ Field (s *o t) \ ?f ` underS (r *o t) a \ underS (s *o t) (?f a)" - unfolding Field_oprod rel.underS_def unfolding map_pair_def oprod_def by auto + unfolding Field_oprod underS_def unfolding map_pair_def oprod_def by auto thus ?thesis unfolding ordLeq_def2 by (auto intro: oprod_Well_order r s t) qed @@ -1269,7 +1269,7 @@ lemma ozero_oexp: "\ (s =o ozero) \ ozero ^o s =o ozero" unfolding oexp_def[OF ozero_Well_order s] FinFunc_def - by simp (metis Func_emp2 bot.extremum_uniqueI emptyE rel.well_order_on_domain s subrelI) + by simp (metis Func_emp2 bot.extremum_uniqueI emptyE well_order_on_domain s subrelI) lemma oone_oexp: "oone ^o s =o oone" (is "?L =o ?R") by (rule oone_ordIso_oexp[OF ordIso_reflexive[OF oone_Well_order] s]) @@ -1326,7 +1326,7 @@ qed moreover from FLR have "ofilter ?R (F ` Field ?L)" - unfolding rexpt.ofilter_def rel.under_def rs.Field_oexp rt.Field_oexp unfolding rt.oexp_def + unfolding rexpt.ofilter_def under_def rs.Field_oexp rt.Field_oexp unfolding rt.oexp_def proof (safe elim!: imageI) fix g h assume gh: "g \ FinFunc r s" "h \ FinFunc r t" "F g \ FinFunc r t" "let m = t.max_fun_diff h (F g) in (h m, F g m) \ r" @@ -1348,7 +1348,7 @@ assume "(t.max_fun_diff h (F g), z) \ t" hence "(z, t.max_fun_diff h (F g)) \ t" using t.in_notinI[of "t.max_fun_diff h (F g)" z] z max_Field by auto - hence "z \ f ` Field s" using *(3) max_f_Field unfolding t.ofilter_def rel.under_def + hence "z \ f ` Field s" using *(3) max_f_Field unfolding t.ofilter_def under_def by fastforce with z show False by blast qed @@ -1356,9 +1356,9 @@ z max_f_Field unfolding F_def by auto } note ** = this with *(3) gh(2) have "h = F (\x. if x \ Field s then h (f x) else undefined)" using invff - unfolding F_def fun_eq_iff FinFunc_def Func_def Let_def t.ofilter_def rel.under_def by auto + unfolding F_def fun_eq_iff FinFunc_def Func_def Let_def t.ofilter_def under_def by auto moreover from gh(2) *(1,3) have "(\x. if x \ Field s then h (f x) else undefined) \ FinFunc r s" - unfolding FinFunc_def Func_def fin_support_def support_def t.ofilter_def rel.under_def + unfolding FinFunc_def Func_def fin_support_def support_def t.ofilter_def under_def by (auto intro: subset_inj_on elim!: finite_imageD[OF finite_subset[rotated]]) ultimately show "?thesis" by (rule image_eqI) qed simp @@ -1396,7 +1396,7 @@ interpret t!: wo_rel t by unfold_locales (rule t) show ?thesis proof (cases "t = {}") - case True thus ?thesis using r s unfolding ordLeq_def2 rel.underS_def by auto + case True thus ?thesis using r s unfolding ordLeq_def2 underS_def by auto next case False thus ?thesis proof (cases "r = {}") @@ -1408,9 +1408,9 @@ hence f_underS: "\a\Field r. f a \ Field s \ f ` underS r a \ underS s (f a)" using embed_in_Field[OF rt.rWELL f] embed_underS2[OF rt.rWELL st.rWELL f] by auto from f `t \ {}` False have *: "Field r \ {}" "Field s \ {}" "Field t \ {}" - unfolding Field_def embed_def rel.under_def bij_betw_def by auto + unfolding Field_def embed_def under_def bij_betw_def by auto with f obtain x where "s.zero = f x" "x \ Field r" unfolding embed_def bij_betw_def - using embed_in_Field[OF r.WELL f] s.zero_under set_mp[OF r.under_Field] by blast + using embed_in_Field[OF r.WELL f] s.zero_under set_mp[OF under_Field[of r]] by blast with f have fz: "f r.zero = s.zero" and inj: "inj_on f (Field r)" and compat: "compat r s f" unfolding embed_iff_compat_inj_on_ofilter[OF r s] compat_def by (fastforce intro: s.leq_zero_imp)+ @@ -1424,11 +1424,11 @@ proof safe fix h assume h_underS: "h \ underS (r ^o t) g" - hence "h \ Field (r ^o t)" unfolding rel.underS_def Field_def by auto + hence "h \ Field (r ^o t)" unfolding underS_def Field_def by auto with fz f_underS have Field_fh: "?f h \ Field (s ^o t)" unfolding st.Field_oexp rt.Field_oexp FinFunc_def Func_def fin_support_def support_def by (auto elim!: finite_subset[rotated]) - from h_underS have "h \ g" and hg: "(h, g) \ rt.oexp" unfolding rel.underS_def by auto + from h_underS have "h \ g" and hg: "(h, g) \ rt.oexp" unfolding underS_def by auto with f inj have neq: "?f h \ ?f g" unfolding fun_eq_iff inj_on_def rt.oexp_def Option.map_def FinFunc_def Func_def Let_def by simp metis @@ -1440,7 +1440,7 @@ with Field_fg Field_fh hg fz f_underS compat neq have "(?f h, ?f g) \ st.oexp" using rt.max_fun_diff[OF `h \ g`] rt.max_fun_diff_in[OF `h \ g`] unfolding st.Field_oexp unfolding rt.oexp_def st.oexp_def Let_def compat_def by auto - ultimately show "?f h \ underS (s ^o t) (?f g)" unfolding rel.underS_def by auto + ultimately show "?f h \ underS (s ^o t) (?f g)" unfolding underS_def by auto qed ultimately have "?f g \ Field (s ^o t) \ ?f ` underS (r ^o t) g \ underS (s ^o t) (?f g)" by blast @@ -1457,11 +1457,11 @@ interpret rs!: wo_rel2 r s by unfold_locales (rule r, rule s) interpret r!: wo_rel r by unfold_locales (rule r) interpret s!: wo_rel s by unfold_locales (rule s) - from assms rel.well_order_on_domain[OF r] obtain x where + from assms well_order_on_domain[OF r] obtain x where x: "x \ Field r" "r.zero \ Field r" "x \ r.zero" - unfolding ordLess_def oone_def embedS_def[abs_def] bij_betw_def embed_def rel.under_def + unfolding ordLess_def oone_def embedS_def[abs_def] bij_betw_def embed_def under_def by (auto simp: image_def) - (metis equals0D insert_not_empty r.under_def r.zero_in_Field rel.under_empty) + (metis (lifting) equals0D mem_Collect_eq r.zero_in_Field singletonI) let ?f = "\a b. if b \ Field s then if b = a then x else r.zero else undefined" from x(3) have SUPP: "\y. y \ Field s \ rs.SUPP (?f y) = {y}" unfolding support_def by auto { fix y assume y: "y \ Field s" @@ -1472,7 +1472,7 @@ proof safe fix z assume "z \ underS s y" - hence z: "z \ y" "(z, y) \ s" "z \ Field s" unfolding rel.underS_def Field_def by auto + hence z: "z \ y" "(z, y) \ s" "z \ Field s" unfolding underS_def Field_def by auto from x(3) y z(1,3) have "?f z \ ?f y" unfolding fun_eq_iff by auto moreover { from x(1,2) have "?f z \ FinFunc r s" "?f y \ FinFunc r s" @@ -1484,7 +1484,7 @@ ultimately have "(?f z, ?f y) \ rs.oexp" using y x(1) unfolding rs.oexp_def Let_def by auto } - ultimately show "?f z \ underS (r ^o s) (?f y)" unfolding rel.underS_def by blast + ultimately show "?f z \ underS (r ^o s) (?f y)" unfolding underS_def by blast qed ultimately have "?f y \ Field (r ^o s) \ ?f ` underS s y \ underS (r ^o s) (?f y)" by blast } diff -r eeba3ba73486 -r 38db7814481d src/HOL/Cardinals/Wellfounded_More_FP.thy --- a/src/HOL/Cardinals/Wellfounded_More_FP.thy Thu Jan 16 18:52:50 2014 +0100 +++ b/src/HOL/Cardinals/Wellfounded_More_FP.thy Thu Jan 16 20:52:54 2014 +0100 @@ -151,7 +151,7 @@ moreover {fix A assume *: "A \ Field r" and **: "A \ {}" obtain a where 1: "r = {} \ r = {(a,a)}" using LI - unfolding order_on_defs using Case1 rel.Total_subset_Id by auto + unfolding order_on_defs using Case1 Total_subset_Id by auto hence "A = {a} \ r = {(a,a)}" using * ** unfolding Field_def by blast hence "\a \ A. \a' \ A. (a,a') \ r" using 1 by blast } @@ -169,7 +169,7 @@ hence "\a \ A. \a' \ A. (a',a) \ r - Id" using 1 * unfolding wf_eq_minimal2 by simp moreover have "\a \ A. \a' \ A. ((a,a') \ r) = ((a',a) \ r - Id)" - using rel.Linear_order_in_diff_Id[of r] ** LI by blast + using Linear_order_in_diff_Id[of r] ** LI by blast ultimately show "\a \ A. \a' \ A. (a,a') \ r" by blast qed next @@ -180,7 +180,7 @@ hence "\a \ A. \a' \ A. (a,a') \ r" using 1 * by simp moreover have "\a \ A. \a' \ A. ((a,a') \ r) = ((a',a) \ r - Id)" - using rel.Linear_order_in_diff_Id[of r] ** LI mono_Field[of "r - Id" r] by blast + using Linear_order_in_diff_Id[of r] ** LI mono_Field[of "r - Id" r] by blast ultimately show "\a \ A. \a' \ A. (a',a) \ r - Id" by blast qed qed diff -r eeba3ba73486 -r 38db7814481d src/HOL/Cardinals/Wellorder_Embedding.thy --- a/src/HOL/Cardinals/Wellorder_Embedding.thy Thu Jan 16 18:52:50 2014 +0100 +++ b/src/HOL/Cardinals/Wellorder_Embedding.thy Thu Jan 16 20:52:54 2014 +0100 @@ -41,7 +41,7 @@ using EMB unfolding embed_def by simp moreover {have "under r a \ Field r" - by (auto simp add: rel.under_Field) + by (auto simp add: under_Field) hence "\ b. b \ under r a \ f b = g b" using EQ by blast } @@ -80,10 +80,10 @@ proof- obtain r where "well_order_on A r" by (fastforce simp add: well_order_on) hence 1: "A = Field r \ Well_order r" - using rel.well_order_on_Well_order by auto + using well_order_on_Well_order by auto obtain r' where 2: "well_order_on A' r'" by (fastforce simp add: well_order_on) hence 2: "A' = Field r' \ Well_order r'" - using rel.well_order_on_Well_order by auto + using well_order_on_Well_order by auto hence "(\f. embed r r' f) \ (\g. embed r' r g)" using 1 2 by (auto simp add: wellorders_totally_ordered) moreover diff -r eeba3ba73486 -r 38db7814481d src/HOL/Cardinals/Wellorder_Embedding_FP.thy --- a/src/HOL/Cardinals/Wellorder_Embedding_FP.thy Thu Jan 16 18:52:50 2014 +0100 +++ b/src/HOL/Cardinals/Wellorder_Embedding_FP.thy Thu Jan 16 20:52:54 2014 +0100 @@ -40,20 +40,20 @@ lemma under_underS_bij_betw: assumes WELL: "Well_order r" and WELL': "Well_order r'" and IN: "a \ Field r" and IN': "f a \ Field r'" and - BIJ: "bij_betw f (rel.underS r a) (rel.underS r' (f a))" -shows "bij_betw f (rel.under r a) (rel.under r' (f a))" + BIJ: "bij_betw f (underS r a) (underS r' (f a))" +shows "bij_betw f (under r a) (under r' (f a))" proof- - have "a \ rel.underS r a \ f a \ rel.underS r' (f a)" - unfolding rel.underS_def by auto + have "a \ underS r a \ f a \ underS r' (f a)" + unfolding underS_def by auto moreover {have "Refl r \ Refl r'" using WELL WELL' by (auto simp add: order_on_defs) - hence "rel.under r a = rel.underS r a \ {a} \ - rel.under r' (f a) = rel.underS r' (f a) \ {f a}" - using IN IN' by(auto simp add: rel.Refl_under_underS) + hence "under r a = underS r a \ {a} \ + under r' (f a) = underS r' (f a) \ {f a}" + using IN IN' by(auto simp add: Refl_under_underS) } ultimately show ?thesis - using BIJ notIn_Un_bij_betw[of a "rel.underS r a" f "rel.underS r' (f a)"] by auto + using BIJ notIn_Un_bij_betw[of a "underS r a" f "underS r' (f a)"] by auto qed @@ -75,7 +75,7 @@ definition embed :: "'a rel \ 'a' rel \ ('a \ 'a') \ bool" where -"embed r r' f \ \a \ Field r. bij_betw f (rel.under r a) (rel.under r' (f a))" +"embed r r' f \ \a \ Field r. bij_betw f (under r a) (under r' (f a))" lemmas embed_defs = embed_def embed_def[abs_def] @@ -133,11 +133,11 @@ using WELL by (auto simp add: wo_rel_def) hence 1: "Refl r" by (auto simp add: wo_rel.REFL) - hence "a \ rel.under r a" using IN rel.Refl_under_in by fastforce - hence "f a \ rel.under r' (f a)" + hence "a \ under r a" using IN Refl_under_in by fastforce + hence "f a \ under r' (f a)" using EMB IN by (auto simp add: embed_def bij_betw_def) thus ?thesis unfolding Field_def - by (auto simp: rel.under_def) + by (auto simp: under_def) qed @@ -147,16 +147,16 @@ shows "embed r r'' (f' o f)" proof(unfold embed_def, auto) fix a assume *: "a \ Field r" - hence "bij_betw f (rel.under r a) (rel.under r' (f a))" + hence "bij_betw f (under r a) (under r' (f a))" using embed_def[of r] EMB by auto moreover {have "f a \ Field r'" using EMB WELL * by (auto simp add: embed_in_Field) - hence "bij_betw f' (rel.under r' (f a)) (rel.under r'' (f' (f a)))" + hence "bij_betw f' (under r' (f a)) (under r'' (f' (f a)))" using embed_def[of r'] EMB' by auto } ultimately - show "bij_betw (f' \ f) (rel.under r a) (rel.under r'' (f'(f a)))" + show "bij_betw (f' \ f) (under r a) (under r'' (f'(f a)))" by(auto simp add: bij_betw_trans) qed @@ -190,14 +190,14 @@ show ?thesis using Well' WELL EMB 0 embed_Field[of r r' f] proof(unfold wo_rel.ofilter_def, auto simp add: image_def) fix a b' - assume *: "a \ A" and **: "b' \ rel.under r' (f a)" + assume *: "a \ A" and **: "b' \ under r' (f a)" hence "a \ Field r" using 0 by auto - hence "bij_betw f (rel.under r a) (rel.under r' (f a))" + hence "bij_betw f (under r a) (under r' (f a))" using * EMB by (auto simp add: embed_def) - hence "f`(rel.under r a) = rel.under r' (f a)" + hence "f`(under r a) = under r' (f a)" by (simp add: bij_betw_def) - with ** image_def[of f "rel.under r a"] obtain b where - 1: "b \ rel.under r a \ b' = f b" by blast + with ** image_def[of f "under r a"] obtain b where + 1: "b \ under r a \ b' = f b" by blast hence "b \ A" using Well * OF by (auto simp add: wo_rel.ofilter_def) with 1 show "\b \ A. b' = f b" by blast @@ -224,14 +224,14 @@ fix a b assume *: "(a,b) \ r" hence 1: "b \ Field r" using Field_def[of r] by blast - have "a \ rel.under r b" - using * rel.under_def[of r] by simp - hence "f a \ rel.under r' (f b)" + have "a \ under r b" + using * under_def[of r] by simp + hence "f a \ under r' (f b)" using EMB embed_def[of r r' f] - bij_betw_def[of f "rel.under r b" "rel.under r' (f b)"] - image_def[of f "rel.under r b"] 1 by auto + bij_betw_def[of f "under r b" "under r' (f b)"] + image_def[of f "under r b"] 1 by auto thus "(f a, f b) \ r'" - by (auto simp add: rel.under_def) + by (auto simp add: under_def) qed @@ -252,16 +252,16 @@ hence 1: "a \ Field r \ b \ Field r" unfolding Field_def by auto {assume "(a,b) \ r" - hence "a \ rel.under r b \ b \ rel.under r b" - using Refl by(auto simp add: rel.under_def refl_on_def) + hence "a \ under r b \ b \ under r b" + using Refl by(auto simp add: under_def refl_on_def) hence "a = b" using EMB 1 *** by (auto simp add: embed_def bij_betw_def inj_on_def) } moreover {assume "(b,a) \ r" - hence "a \ rel.under r a \ b \ rel.under r a" - using Refl by(auto simp add: rel.under_def refl_on_def) + hence "a \ under r a \ b \ under r a" + using Refl by(auto simp add: under_def refl_on_def) hence "a = b" using EMB 1 *** by (auto simp add: embed_def bij_betw_def inj_on_def) @@ -275,19 +275,19 @@ lemma embed_underS: assumes WELL: "Well_order r" and WELL': "Well_order r'" and EMB: "embed r r' f" and IN: "a \ Field r" -shows "bij_betw f (rel.underS r a) (rel.underS r' (f a))" +shows "bij_betw f (underS r a) (underS r' (f a))" proof- - have "bij_betw f (rel.under r a) (rel.under r' (f a))" + have "bij_betw f (under r a) (under r' (f a))" using assms by (auto simp add: embed_def) moreover {have "f a \ Field r'" using assms embed_Field[of r r' f] by auto - hence "rel.under r a = rel.underS r a \ {a} \ - rel.under r' (f a) = rel.underS r' (f a) \ {f a}" - using assms by (auto simp add: order_on_defs rel.Refl_under_underS) + hence "under r a = underS r a \ {a} \ + under r' (f a) = underS r' (f a) \ {f a}" + using assms by (auto simp add: order_on_defs Refl_under_underS) } moreover - {have "a \ rel.underS r a \ f a \ rel.underS r' (f a)" - unfolding rel.underS_def by blast + {have "a \ underS r a \ f a \ underS r' (f a)" + unfolding underS_def by blast } ultimately show ?thesis by (auto simp add: notIn_Un_bij_betw3) @@ -325,20 +325,20 @@ unfolding Field_def by auto have "f a \ f`(Field r)" using **** by auto - hence 2: "rel.under r' (f a) \ f`(Field r)" + hence 2: "under r' (f a) \ f`(Field r)" using Well' *** wo_rel.ofilter_def[of r' "f`(Field r)"] by fastforce (* Main proof *) - show "bij_betw f (rel.under r a) (rel.under r' (f a))" + show "bij_betw f (under r a) (under r' (f a))" proof(unfold bij_betw_def, auto) - show "inj_on f (rel.under r a)" - using * by (metis (no_types) rel.under_Field subset_inj_on) + show "inj_on f (under r a)" + using * by (metis (no_types) under_Field subset_inj_on) next - fix b assume "b \ rel.under r a" - thus "f b \ rel.under r' (f a)" - unfolding rel.under_def using ** + fix b assume "b \ under r a" + thus "f b \ under r' (f a)" + unfolding under_def using ** by (auto simp add: compat_def) next - fix b' assume *****: "b' \ rel.under r' (f a)" + fix b' assume *****: "b' \ under r' (f a)" hence "b' \ f`(Field r)" using 2 by auto with Field_def[of r] obtain b where @@ -349,7 +349,7 @@ with ** 4 have "(f a, b'): r'" by (auto simp add: compat_def) with ***** Antisym' have "f a = b'" - by(auto simp add: rel.under_def antisym_def) + by(auto simp add: under_def antisym_def) with 3 **** 4 * have "a = b" by(auto simp add: inj_on_def) } @@ -361,15 +361,15 @@ ultimately show ?thesis using Total **** 3 by (fastforce simp add: total_on_def) qed - with 4 show "b' \ f`(rel.under r a)" - unfolding rel.under_def by auto + with 4 show "b' \ f`(under r a)" + unfolding under_def by auto qed qed lemma inv_into_ofilter_embed: assumes WELL: "Well_order r" and OF: "wo_rel.ofilter r A" and - BIJ: "\b \ A. bij_betw f (rel.under r b) (rel.under r' (f b))" and + BIJ: "\b \ A. bij_betw f (under r b) (under r' (f b))" and IMAGE: "f ` A = Field r'" shows "embed r' r (inv_into A f)" proof- @@ -390,16 +390,16 @@ using * ** Well OF by (auto simp add: wo_rel.ofilter_def) moreover {assume "(b1,b2) \ r" - hence "b1 \ rel.under r b2 \ b2 \ rel.under r b2" - unfolding rel.under_def using 11 Refl + hence "b1 \ under r b2 \ b2 \ under r b2" + unfolding under_def using 11 Refl by (auto simp add: refl_on_def) hence "b1 = b2" using BIJ * ** *** by (simp add: bij_betw_def inj_on_def) } moreover {assume "(b2,b1) \ r" - hence "b1 \ rel.under r b1 \ b2 \ rel.under r b1" - unfolding rel.under_def using 11 Refl + hence "b1 \ under r b1 \ b2 \ under r b1" + unfolding under_def using 11 Refl by (auto simp add: refl_on_def) hence "b1 = b2" using BIJ * ** *** by (simp add: bij_betw_def inj_on_def) @@ -411,20 +411,20 @@ (* *) let ?f' = "(inv_into A f)" (* *) - have 2: "\b \ A. bij_betw ?f' (rel.under r' (f b)) (rel.under r b)" + have 2: "\b \ A. bij_betw ?f' (under r' (f b)) (under r b)" proof(clarify) fix b assume *: "b \ A" - hence "rel.under r b \ A" + hence "under r b \ A" using Well OF by(auto simp add: wo_rel.ofilter_def) moreover - have "f ` (rel.under r b) = rel.under r' (f b)" + have "f ` (under r b) = under r' (f b)" using * BIJ by (auto simp add: bij_betw_def) ultimately - show "bij_betw ?f' (rel.under r' (f b)) (rel.under r b)" + show "bij_betw ?f' (under r' (f b)) (under r b)" using 1 by (auto simp add: bij_betw_inv_into_subset) qed (* *) - have 3: "\b' \ Field r'. bij_betw ?f' (rel.under r' b') (rel.under r (?f' b'))" + have 3: "\b' \ Field r'. bij_betw ?f' (under r' b') (under r (?f' b'))" proof(clarify) fix b' assume *: "b' \ Field r'" have "b' = f (?f' b')" using * 1 @@ -435,7 +435,7 @@ with 31 have "?f' b' \ A" by auto } ultimately - show "bij_betw ?f' (rel.under r' b') (rel.under r (?f' b'))" + show "bij_betw ?f' (under r' b') (under r (?f' b'))" using 2 by auto qed (* *) @@ -445,10 +445,10 @@ lemma inv_into_underS_embed: assumes WELL: "Well_order r" and - BIJ: "\b \ rel.underS r a. bij_betw f (rel.under r b) (rel.under r' (f b))" and + BIJ: "\b \ underS r a. bij_betw f (under r b) (under r' (f b))" and IN: "a \ Field r" and - IMAGE: "f ` (rel.underS r a) = Field r'" -shows "embed r' r (inv_into (rel.underS r a) f)" + IMAGE: "f ` (underS r a) = Field r'" +shows "embed r' r (inv_into (underS r a) f)" using assms by(auto simp add: wo_rel_def wo_rel.underS_ofilter inv_into_ofilter_embed) @@ -458,7 +458,7 @@ IMAGE: "Field r' \ f ` (Field r)" shows "embed r' r (inv_into (Field r) f)" proof- - have "(\b \ Field r. bij_betw f (rel.under r b) (rel.under r' (f b)))" + have "(\b \ Field r. bij_betw f (under r b) (under r' (f b)))" using EMB by (auto simp add: embed_def) moreover have "f ` (Field r) \ Field r'" @@ -511,101 +511,101 @@ fixes r ::"'a rel" and r'::"'a' rel" and f :: "'a \ 'a'" and a::'a assumes WELL: "Well_order r" and WELL': "Well_order r'" and IN: "a \ Field r" and - IH: "\b \ rel.underS r a. bij_betw f (rel.under r b) (rel.under r' (f b))" and - NOT: "f ` (rel.underS r a) \ Field r'" and SUC: "f a = wo_rel.suc r' (f`(rel.underS r a))" -shows "bij_betw f (rel.under r a) (rel.under r' (f a))" + IH: "\b \ underS r a. bij_betw f (under r b) (under r' (f b))" and + NOT: "f ` (underS r a) \ Field r'" and SUC: "f a = wo_rel.suc r' (f`(underS r a))" +shows "bij_betw f (under r a) (under r' (f a))" proof- (* Preliminary facts *) have Well: "wo_rel r" using WELL unfolding wo_rel_def . hence Refl: "Refl r" using wo_rel.REFL[of r] by auto have Trans: "trans r" using Well wo_rel.TRANS[of r] by auto have Well': "wo_rel r'" using WELL' unfolding wo_rel_def . - have OF: "wo_rel.ofilter r (rel.underS r a)" + have OF: "wo_rel.ofilter r (underS r a)" by (auto simp add: Well wo_rel.underS_ofilter) - hence UN: "rel.underS r a = (\ b \ rel.underS r a. rel.under r b)" - using Well wo_rel.ofilter_under_UNION[of r "rel.underS r a"] by blast - (* Gather facts about elements of rel.underS r a *) - {fix b assume *: "b \ rel.underS r a" - hence t0: "(b,a) \ r \ b \ a" unfolding rel.underS_def by auto + hence UN: "underS r a = (\ b \ underS r a. under r b)" + using Well wo_rel.ofilter_under_UNION[of r "underS r a"] by blast + (* Gather facts about elements of underS r a *) + {fix b assume *: "b \ underS r a" + hence t0: "(b,a) \ r \ b \ a" unfolding underS_def by auto have t1: "b \ Field r" - using * rel.underS_Field[of r a] by auto - have t2: "f`(rel.under r b) = rel.under r' (f b)" + using * underS_Field[of r a] by auto + have t2: "f`(under r b) = under r' (f b)" using IH * by (auto simp add: bij_betw_def) - hence t3: "wo_rel.ofilter r' (f`(rel.under r b))" + hence t3: "wo_rel.ofilter r' (f`(under r b))" using Well' by (auto simp add: wo_rel.under_ofilter) - have "f`(rel.under r b) \ Field r'" - using t2 by (auto simp add: rel.under_Field) + have "f`(under r b) \ Field r'" + using t2 by (auto simp add: under_Field) moreover - have "b \ rel.under r b" - using t1 by(auto simp add: Refl rel.Refl_under_in) + have "b \ under r b" + using t1 by(auto simp add: Refl Refl_under_in) ultimately have t4: "f b \ Field r'" by auto - have "f`(rel.under r b) = rel.under r' (f b) \ - wo_rel.ofilter r' (f`(rel.under r b)) \ + have "f`(under r b) = under r' (f b) \ + wo_rel.ofilter r' (f`(under r b)) \ f b \ Field r'" using t2 t3 t4 by auto } hence bFact: - "\b \ rel.underS r a. f`(rel.under r b) = rel.under r' (f b) \ - wo_rel.ofilter r' (f`(rel.under r b)) \ + "\b \ underS r a. f`(under r b) = under r' (f b) \ + wo_rel.ofilter r' (f`(under r b)) \ f b \ Field r'" by blast (* *) - have subField: "f`(rel.underS r a) \ Field r'" + have subField: "f`(underS r a) \ Field r'" using bFact by blast (* *) - have OF': "wo_rel.ofilter r' (f`(rel.underS r a))" + have OF': "wo_rel.ofilter r' (f`(underS r a))" proof- - have "f`(rel.underS r a) = f`(\ b \ rel.underS r a. rel.under r b)" + have "f`(underS r a) = f`(\ b \ underS r a. under r b)" using UN by auto - also have "\ = (\ b \ rel.underS r a. f`(rel.under r b))" by blast - also have "\ = (\ b \ rel.underS r a. (rel.under r' (f b)))" + also have "\ = (\ b \ underS r a. f`(under r b))" by blast + also have "\ = (\ b \ underS r a. (under r' (f b)))" using bFact by auto finally - have "f`(rel.underS r a) = (\ b \ rel.underS r a. (rel.under r' (f b)))" . + have "f`(underS r a) = (\ b \ underS r a. (under r' (f b)))" . thus ?thesis using Well' bFact - wo_rel.ofilter_UNION[of r' "rel.underS r a" "\ b. rel.under r' (f b)"] by fastforce + wo_rel.ofilter_UNION[of r' "underS r a" "\ b. under r' (f b)"] by fastforce qed (* *) - have "f`(rel.underS r a) \ rel.AboveS r' (f`(rel.underS r a)) = Field r'" + have "f`(underS r a) \ AboveS r' (f`(underS r a)) = Field r'" using Well' OF' by (auto simp add: wo_rel.ofilter_AboveS_Field) - hence NE: "rel.AboveS r' (f`(rel.underS r a)) \ {}" + hence NE: "AboveS r' (f`(underS r a)) \ {}" using subField NOT by blast (* Main proof *) - have INCL1: "f`(rel.underS r a) \ rel.underS r' (f a) " + have INCL1: "f`(underS r a) \ underS r' (f a) " proof(auto) - fix b assume *: "b \ rel.underS r a" + fix b assume *: "b \ underS r a" have "f b \ f a \ (f b, f a) \ r'" using subField Well' SUC NE * - wo_rel.suc_greater[of r' "f`(rel.underS r a)" "f b"] by force - thus "f b \ rel.underS r' (f a)" - unfolding rel.underS_def by simp + wo_rel.suc_greater[of r' "f`(underS r a)" "f b"] by force + thus "f b \ underS r' (f a)" + unfolding underS_def by simp qed (* *) - have INCL2: "rel.underS r' (f a) \ f`(rel.underS r a)" + have INCL2: "underS r' (f a) \ f`(underS r a)" proof - fix b' assume "b' \ rel.underS r' (f a)" + fix b' assume "b' \ underS r' (f a)" hence "b' \ f a \ (b', f a) \ r'" - unfolding rel.underS_def by simp - thus "b' \ f`(rel.underS r a)" + unfolding underS_def by simp + thus "b' \ f`(underS r a)" using Well' SUC NE OF' - wo_rel.suc_ofilter_in[of r' "f ` rel.underS r a" b'] by auto + wo_rel.suc_ofilter_in[of r' "f ` underS r a" b'] by auto qed (* *) - have INJ: "inj_on f (rel.underS r a)" + have INJ: "inj_on f (underS r a)" proof- - have "\b \ rel.underS r a. inj_on f (rel.under r b)" + have "\b \ underS r a. inj_on f (under r b)" using IH by (auto simp add: bij_betw_def) moreover - have "\b. wo_rel.ofilter r (rel.under r b)" + have "\b. wo_rel.ofilter r (under r b)" using Well by (auto simp add: wo_rel.under_ofilter) ultimately show ?thesis using WELL bFact UN - UNION_inj_on_ofilter[of r "rel.underS r a" "\b. rel.under r b" f] + UNION_inj_on_ofilter[of r "underS r a" "\b. under r b" f] by auto qed (* *) - have BIJ: "bij_betw f (rel.underS r a) (rel.underS r' (f a))" + have BIJ: "bij_betw f (underS r a) (underS r' (f a))" unfolding bij_betw_def using INJ INCL1 INCL2 by auto (* *) @@ -622,14 +622,14 @@ f :: "'a \ 'a'" and g :: "'a \ bool" and a::'a assumes WELL: "Well_order r" and WELL': "Well_order r'" and MAIN1: - "\ a. (False \ g`(rel.underS r a) \ f`(rel.underS r a) \ Field r' - \ f a = wo_rel.suc r' (f`(rel.underS r a)) \ g a = True) + "\ a. (False \ g`(underS r a) \ f`(underS r a) \ Field r' + \ f a = wo_rel.suc r' (f`(underS r a)) \ g a = True) \ - (\(False \ (g`(rel.underS r a)) \ f`(rel.underS r a) \ Field r') + (\(False \ (g`(underS r a)) \ f`(underS r a) \ Field r') \ g a = False)" and -MAIN2: "\ a. a \ Field r \ False \ g`(rel.under r a) \ - bij_betw f (rel.under r a) (rel.under r' (f a))" and -Case: "a \ Field r \ False \ g`(rel.under r a)" +MAIN2: "\ a. a \ Field r \ False \ g`(under r a) \ + bij_betw f (under r a) (under r' (f a))" and +Case: "a \ Field r \ False \ g`(under r a)" shows "\f'. embed r' r f'" proof- have Well: "wo_rel r" using WELL unfolding wo_rel_def . @@ -638,13 +638,13 @@ have Antisym: "antisym r" using Well wo_rel.ANTISYM[of r] by auto have Well': "wo_rel r'" using WELL' unfolding wo_rel_def . (* *) - have 0: "rel.under r a = rel.underS r a \ {a}" - using Refl Case by(auto simp add: rel.Refl_under_underS) + have 0: "under r a = underS r a \ {a}" + using Refl Case by(auto simp add: Refl_under_underS) (* *) have 1: "g a = False" proof- {assume "g a \ False" - with 0 Case have "False \ g`(rel.underS r a)" by blast + with 0 Case have "False \ g`(underS r a)" by blast with MAIN1 have "g a = False" by blast} thus ?thesis by blast qed @@ -653,12 +653,12 @@ (* *) have 2: "?A \ {} \ ?A \ Field r" using Case 1 by blast (* *) - have 3: "False \ g`(rel.underS r ?a)" + have 3: "False \ g`(underS r ?a)" proof - assume "False \ g`(rel.underS r ?a)" - then obtain b where "b \ rel.underS r ?a" and 31: "g b = False" by auto + assume "False \ g`(underS r ?a)" + then obtain b where "b \ underS r ?a" and 31: "g b = False" by auto hence 32: "(b,?a) \ r \ b \ ?a" - by (auto simp add: rel.underS_def) + by (auto simp add: underS_def) hence "b \ Field r" unfolding Field_def by auto with 31 have "b \ ?A" by auto hence "(?a,b) \ r" using wo_rel.minim_least 2 Well by fastforce @@ -672,25 +672,25 @@ (* *) have 5: "g ?a = False" using temp by blast (* *) - have 6: "f`(rel.underS r ?a) = Field r'" + have 6: "f`(underS r ?a) = Field r'" using MAIN1[of ?a] 3 5 by blast (* *) - have 7: "\b \ rel.underS r ?a. bij_betw f (rel.under r b) (rel.under r' (f b))" + have 7: "\b \ underS r ?a. bij_betw f (under r b) (under r' (f b))" proof - fix b assume as: "b \ rel.underS r ?a" + fix b assume as: "b \ underS r ?a" moreover - have "wo_rel.ofilter r (rel.underS r ?a)" + have "wo_rel.ofilter r (underS r ?a)" using Well by (auto simp add: wo_rel.underS_ofilter) ultimately - have "False \ g`(rel.under r b)" using 3 Well by (subst (asm) wo_rel.ofilter_def) fast+ + have "False \ g`(under r b)" using 3 Well by (subst (asm) wo_rel.ofilter_def) fast+ moreover have "b \ Field r" - unfolding Field_def using as by (auto simp add: rel.underS_def) + unfolding Field_def using as by (auto simp add: underS_def) ultimately - show "bij_betw f (rel.under r b) (rel.under r' (f b))" + show "bij_betw f (under r b) (under r' (f b))" using MAIN2 by auto qed (* *) - have "embed r' r (inv_into (rel.underS r ?a) f)" + have "embed r' r (inv_into (underS r ?a) f)" using WELL WELL' 7 4 6 inv_into_underS_embed[of r ?a f r'] by auto thus ?thesis unfolding embed_def by blast @@ -709,18 +709,18 @@ have Well': "wo_rel r'" using WELL' unfolding wo_rel_def . (* Main proof *) obtain H where H_def: "H = - (\h a. if False \ (snd o h)`(rel.underS r a) \ (fst o h)`(rel.underS r a) \ Field r' - then (wo_rel.suc r' ((fst o h)`(rel.underS r a)), True) + (\h a. if False \ (snd o h)`(underS r a) \ (fst o h)`(underS r a) \ Field r' + then (wo_rel.suc r' ((fst o h)`(underS r a)), True) else (undefined, False))" by blast have Adm: "wo_rel.adm_wo r H" using Well proof(unfold wo_rel.adm_wo_def, clarify) fix h1::"'a \ 'a' * bool" and h2::"'a \ 'a' * bool" and x - assume "\y\rel.underS r x. h1 y = h2 y" - hence "\y\rel.underS r x. (fst o h1) y = (fst o h2) y \ + assume "\y\underS r x. h1 y = h2 y" + hence "\y\underS r x. (fst o h1) y = (fst o h2) y \ (snd o h1) y = (snd o h2) y" by auto - hence "(fst o h1)`(rel.underS r x) = (fst o h2)`(rel.underS r x) \ - (snd o h1)`(rel.underS r x) = (snd o h2)`(rel.underS r x)" + hence "(fst o h1)`(underS r x) = (fst o h2)`(underS r x) \ + (snd o h1)`(underS r x) = (snd o h2)`(underS r x)" by (auto simp add: image_def) thus "H h1 x = H h2 x" by (simp add: H_def del: not_False_in_image_Ball) qed @@ -729,21 +729,21 @@ where h_def: "h = wo_rel.worec r H" and f_def: "f = fst o h" and g_def: "g = snd o h" by blast obtain test where test_def: - "test = (\ a. False \ (g`(rel.underS r a)) \ f`(rel.underS r a) \ Field r')" by blast + "test = (\ a. False \ (g`(underS r a)) \ f`(underS r a) \ Field r')" by blast (* *) have *: "\ a. h a = H h a" using Adm Well wo_rel.worec_fixpoint[of r H] by (simp add: h_def) have Main1: - "\ a. (test a \ f a = wo_rel.suc r' (f`(rel.underS r a)) \ g a = True) \ + "\ a. (test a \ f a = wo_rel.suc r' (f`(underS r a)) \ g a = True) \ (\(test a) \ g a = False)" proof- (* How can I prove this withou fixing a? *) - fix a show "(test a \ f a = wo_rel.suc r' (f`(rel.underS r a)) \ g a = True) \ + fix a show "(test a \ f a = wo_rel.suc r' (f`(underS r a)) \ g a = True) \ (\(test a) \ g a = False)" using *[of a] test_def f_def g_def H_def by auto qed (* *) - let ?phi = "\ a. a \ Field r \ False \ g`(rel.under r a) \ - bij_betw f (rel.under r a) (rel.under r' (f a))" + let ?phi = "\ a. a \ Field r \ False \ g`(under r a) \ + bij_betw f (under r a) (under r' (f a))" have Main2: "\ a. ?phi a" proof- fix a show "?phi a" @@ -752,46 +752,46 @@ fix a assume IH: "\b. b \ a \ (b,a) \ r \ ?phi b" and *: "a \ Field r" and - **: "False \ g`(rel.under r a)" - have 1: "\b \ rel.underS r a. bij_betw f (rel.under r b) (rel.under r' (f b))" + **: "False \ g`(under r a)" + have 1: "\b \ underS r a. bij_betw f (under r b) (under r' (f b))" proof(clarify) - fix b assume ***: "b \ rel.underS r a" - hence 0: "(b,a) \ r \ b \ a" unfolding rel.underS_def by auto + fix b assume ***: "b \ underS r a" + hence 0: "(b,a) \ r \ b \ a" unfolding underS_def by auto moreover have "b \ Field r" - using *** rel.underS_Field[of r a] by auto - moreover have "False \ g`(rel.under r b)" - using 0 ** Trans rel.under_incr[of r b a] by auto - ultimately show "bij_betw f (rel.under r b) (rel.under r' (f b))" + using *** underS_Field[of r a] by auto + moreover have "False \ g`(under r b)" + using 0 ** Trans under_incr[of r b a] by auto + ultimately show "bij_betw f (under r b) (under r' (f b))" using IH by auto qed (* *) - have 21: "False \ g`(rel.underS r a)" - using ** rel.underS_subset_under[of r a] by auto - have 22: "g`(rel.under r a) \ {True}" using ** by auto - moreover have 23: "a \ rel.under r a" - using Refl * by (auto simp add: rel.Refl_under_in) + have 21: "False \ g`(underS r a)" + using ** underS_subset_under[of r a] by auto + have 22: "g`(under r a) \ {True}" using ** by auto + moreover have 23: "a \ under r a" + using Refl * by (auto simp add: Refl_under_in) ultimately have 24: "g a = True" by blast - have 2: "f`(rel.underS r a) \ Field r'" + have 2: "f`(underS r a) \ Field r'" proof - assume "f`(rel.underS r a) = Field r'" + assume "f`(underS r a) = Field r'" hence "g a = False" using Main1 test_def by blast with 24 show False using ** by blast qed (* *) - have 3: "f a = wo_rel.suc r' (f`(rel.underS r a))" + have 3: "f a = wo_rel.suc r' (f`(underS r a))" using 21 2 Main1 test_def by blast (* *) - show "bij_betw f (rel.under r a) (rel.under r' (f a))" + show "bij_betw f (under r a) (under r' (f a))" using WELL WELL' 1 2 3 * wellorders_totally_ordered_aux[of r r' a f] by auto qed qed (* *) - let ?chi = "(\ a. a \ Field r \ False \ g`(rel.under r a))" + let ?chi = "(\ a. a \ Field r \ False \ g`(under r a))" show ?thesis proof(cases "\a. ?chi a") assume "\ (\a. ?chi a)" - hence "\a \ Field r. bij_betw f (rel.under r a) (rel.under r' (f a))" + hence "\a \ Field r. bij_betw f (under r a) (under r' (f a))" using Main2 by blast thus ?thesis unfolding embed_def by blast next @@ -817,16 +817,16 @@ lemma embed_determined: assumes WELL: "Well_order r" and WELL': "Well_order r'" and EMB: "embed r r' f" and IN: "a \ Field r" -shows "f a = wo_rel.suc r' (f`(rel.underS r a))" +shows "f a = wo_rel.suc r' (f`(underS r a))" proof- - have "bij_betw f (rel.underS r a) (rel.underS r' (f a))" + have "bij_betw f (underS r a) (underS r' (f a))" using assms by (auto simp add: embed_underS) - hence "f`(rel.underS r a) = rel.underS r' (f a)" + hence "f`(underS r a) = underS r' (f a)" by (auto simp add: bij_betw_def) moreover {have "f a \ Field r'" using IN using EMB WELL embed_Field[of r r' f] by auto - hence "f a = wo_rel.suc r' (rel.underS r' (f a))" + hence "f a = wo_rel.suc r' (underS r' (f a))" using WELL' by (auto simp add: wo_rel_def wo_rel.suc_underS) } ultimately show ?thesis by simp @@ -841,9 +841,9 @@ fix a assume IH: "\b. b \ a \ (b,a): r \ b \ Field r \ f b = g b" and *: "a \ Field r" - hence "\b \ rel.underS r a. f b = g b" - unfolding rel.underS_def by (auto simp add: Field_def) - hence "f`(rel.underS r a) = g`(rel.underS r a)" by force + hence "\b \ underS r a. f b = g b" + unfolding underS_def by (auto simp add: Field_def) + hence "f`(underS r a) = g`(underS r a)" by force thus "f a = g a" using assms * embed_determined[of r r' f a] embed_determined[of r r' g a] by auto qed @@ -1083,28 +1083,28 @@ next assume *: "bij_betw f (Field r) (Field r')" and **: "\a\Field r. \b\Field r. ((a, b) \ r) = ((f a, f b) \ r')" - have 1: "\ a. rel.under r a \ Field r \ rel.under r' (f a) \ Field r'" - by (auto simp add: rel.under_Field) + have 1: "\ a. under r a \ Field r \ under r' (f a) \ Field r'" + by (auto simp add: under_Field) have 2: "inj_on f (Field r)" using * by (auto simp add: bij_betw_def) {fix a assume ***: "a \ Field r" - have "bij_betw f (rel.under r a) (rel.under r' (f a))" + have "bij_betw f (under r a) (under r' (f a))" proof(unfold bij_betw_def, auto) - show "inj_on f (rel.under r a)" + show "inj_on f (under r a)" using 1 2 by (metis subset_inj_on) next - fix b assume "b \ rel.under r a" + fix b assume "b \ under r a" hence "a \ Field r \ b \ Field r \ (b,a) \ r" - unfolding rel.under_def by (auto simp add: Field_def Range_def Domain_def) - with 1 ** show "f b \ rel.under r' (f a)" - unfolding rel.under_def by auto + unfolding under_def by (auto simp add: Field_def Range_def Domain_def) + with 1 ** show "f b \ under r' (f a)" + unfolding under_def by auto next - fix b' assume "b' \ rel.under r' (f a)" - hence 3: "(b',f a) \ r'" unfolding rel.under_def by simp + fix b' assume "b' \ under r' (f a)" + hence 3: "(b',f a) \ r'" unfolding under_def by simp hence "b' \ Field r'" unfolding Field_def by auto with * obtain b where "b \ Field r \ f b = b'" unfolding bij_betw_def by force with 3 ** *** - show "b' \ f ` (rel.under r a)" unfolding rel.under_def by blast + show "b' \ f ` (under r a)" unfolding under_def by blast qed } thus "embed r r' f" unfolding embed_def using * by auto diff -r eeba3ba73486 -r 38db7814481d src/HOL/Cardinals/Wellorder_Extension.thy --- a/src/HOL/Cardinals/Wellorder_Extension.thy Thu Jan 16 18:52:50 2014 +0100 +++ b/src/HOL/Cardinals/Wellorder_Extension.thy Thu Jan 16 20:52:54 2014 +0100 @@ -178,7 +178,7 @@ where "p \ w" and wo: "Well_order w" by blast let ?A = "UNIV - Field w" from well_order_on [of ?A] obtain w' where wo': "well_order_on ?A w'" .. - have [simp]: "Field w' = ?A" using rel.well_order_on_Well_order [OF wo'] by simp + have [simp]: "Field w' = ?A" using well_order_on_Well_order [OF wo'] by simp have *: "Field w \ Field w' = {}" by simp let ?w = "w \o w'" have "p \ ?w" using `p \ w` by (auto simp: Osum_def) diff -r eeba3ba73486 -r 38db7814481d src/HOL/Cardinals/Wellorder_Relation.thy --- a/src/HOL/Cardinals/Wellorder_Relation.thy Thu Jan 16 18:52:50 2014 +0100 +++ b/src/HOL/Cardinals/Wellorder_Relation.thy Thu Jan 16 20:52:54 2014 +0100 @@ -37,7 +37,7 @@ proof- have "adm_wf (r - Id) H" unfolding adm_wf_def - using ADM adm_wo_def[of H] underS_def by auto + using ADM adm_wo_def[of H] underS_def[of r] by auto hence "f = wfrec (r - Id) H" using fp WF wfrec_unique_fixpoint[of "r - Id" H] by simp thus ?thesis unfolding worec_def . @@ -97,7 +97,7 @@ have "Under A \ under (minim A)" proof fix x assume "x \ Under A" - with 1 Under_def have "(x,minim A) \ r" by auto + with 1 Under_def[of r] have "(x,minim A) \ r" by auto thus "x \ under(minim A)" unfolding under_def by simp qed (* *) @@ -133,7 +133,7 @@ have "UnderS A \ underS (minim A)" proof fix x assume "x \ UnderS A" - with 1 UnderS_def have "x \ minim A \ (x,minim A) \ r" by auto + with 1 UnderS_def[of r] have "x \ minim A \ (x,minim A) \ r" by auto thus "x \ underS(minim A)" unfolding underS_def by simp qed (* *) @@ -173,7 +173,7 @@ shows "supr B \ Above B" proof(unfold supr_def) have "Above B \ Field r" - using Above_Field by auto + using Above_Field[of r] by auto thus "minim (Above B) \ Above B" using assms by (simp add: minim_in) qed @@ -185,7 +185,7 @@ proof- from assms supr_Above have "supr B \ Above B" by simp - with IN Above_def show ?thesis by simp + with IN Above_def[of r] show ?thesis by simp qed lemma supr_least_Above: @@ -194,7 +194,7 @@ shows "(supr B, a) \ r" proof(unfold supr_def) have "Above B \ Field r" - using Above_Field by auto + using Above_Field[of r] by auto thus "(minim (Above B), a) \ r" using assms minim_least by simp @@ -211,7 +211,7 @@ shows "a = supr B" proof(unfold supr_def) have "Above B \ Field r" - using Above_Field by auto + using Above_Field[of r] by auto thus "a = minim (Above B)" using assms equals_minim by simp qed @@ -236,7 +236,7 @@ shows "supr B \ Field r" proof- have "supr B \ Above B" using supr_Above assms by simp - thus ?thesis using assms Above_Field by auto + thus ?thesis using assms Above_Field[of r] by auto qed lemma supr_above_Above: @@ -264,13 +264,13 @@ shows "a = supr (under a)" proof- have "under a \ Field r" - using under_Field by auto + using under_Field[of r] by auto moreover have "under a \ {}" - using IN Refl_under_in REFL by auto + using IN Refl_under_in[of r] REFL by auto moreover have "a \ Above (under a)" - using in_Above_under IN by auto + using in_Above_under[of _ r] IN by auto moreover have "\a' \ Above (under a). (a,a') \ r" proof(unfold Above_def under_def, auto) @@ -347,7 +347,7 @@ shows "a' = a \ (a',a) \ r" proof- have *: "suc {a} \ Field r \ a' \ Field r" - using WELL REL well_order_on_domain by auto + using WELL REL well_order_on_domain by metis {assume **: "a' \ a" hence "(a,a') \ r \ (a',a) \ r" using TOTAL IN * by (auto simp add: total_on_def) @@ -369,7 +369,7 @@ shows "underS (suc {a}) = under a" proof- have 1: "AboveS {a} \ {}" - using ABV aboveS_AboveS_singl by auto + using ABV aboveS_AboveS_singl[of r] by auto have 2: "a \ suc {a} \ (a,suc {a}) \ r" using suc_greater[of "{a}" a] IN 1 by auto (* *) @@ -408,12 +408,12 @@ proof(unfold ofilter_def, auto) fix x assume "x \ Under A" thus "x \ Field r" - using Under_Field assms by auto + using Under_Field[of r] assms by auto next fix a x assume "a \ Under A" and "x \ under a" thus "x \ Under A" - using TRANS under_Under_trans by auto + using TRANS under_Under_trans[of r] by auto qed lemma ofilter_UnderS[simp]: @@ -422,12 +422,12 @@ proof(unfold ofilter_def, auto) fix x assume "x \ UnderS A" thus "x \ Field r" - using UnderS_Field assms by auto + using UnderS_Field[of r] assms by auto next fix a x assume "a \ UnderS A" and "x \ under a" thus "x \ UnderS A" - using TRANS ANTISYM under_UnderS_trans by auto + using TRANS ANTISYM under_UnderS_trans[of r] by auto qed lemma ofilter_Int[simp]: "\ofilter A; ofilter B\ \ ofilter(A Int B)" @@ -469,7 +469,7 @@ (* Main proof *) fix x assume "x \ Under(Under A)" with 1 have 1: "(x,minim A) \ r" - using Under_def by auto + using Under_def[of r] by auto with Field_def have "x \ Field r" by fastforce moreover {fix y assume *: "y \ A" @@ -506,7 +506,7 @@ hence "(suc A,x) \ r" using suc_least_AboveS by auto moreover - have "(x,suc A) \ r" using * under_def by auto + have "(x,suc A) \ r" using * under_def[of r] by auto ultimately show "x = suc A" using ANTISYM antisym_def[of r] by auto qed diff -r eeba3ba73486 -r 38db7814481d src/HOL/Cardinals/Wellorder_Relation_FP.thy --- a/src/HOL/Cardinals/Wellorder_Relation_FP.thy Thu Jan 16 18:52:50 2014 +0100 +++ b/src/HOL/Cardinals/Wellorder_Relation_FP.thy Thu Jan 16 20:52:54 2014 +0100 @@ -18,7 +18,9 @@ i.e., as containing the diagonals of their fields. *} -locale wo_rel = rel + assumes WELL: "Well_order r" +locale wo_rel = + fixes r :: "'a rel" + assumes WELL: "Well_order r" begin text{* The following context encompasses all this section. In other words, @@ -26,6 +28,15 @@ (* context wo_rel *) +abbreviation under where "under \ Order_Relation_More_FP.under r" +abbreviation underS where "underS \ Order_Relation_More_FP.underS r" +abbreviation Under where "Under \ Order_Relation_More_FP.Under r" +abbreviation UnderS where "UnderS \ Order_Relation_More_FP.UnderS r" +abbreviation above where "above \ Order_Relation_More_FP.above r" +abbreviation aboveS where "aboveS \ Order_Relation_More_FP.aboveS r" +abbreviation Above where "Above \ Order_Relation_More_FP.Above r" +abbreviation AboveS where "AboveS \ Order_Relation_More_FP.AboveS r" + subsection {* Auxiliaries *} @@ -109,7 +120,7 @@ let ?rS = "r - Id" have "adm_wf (r - Id) H" unfolding adm_wf_def - using ADM adm_wo_def[of H] underS_def by auto + using ADM adm_wo_def[of H] underS_def[of r] by auto hence "wfrec ?rS H = H (wfrec ?rS H)" using WF wfrec_fixpoint[of ?rS H] by simp thus ?thesis unfolding worec_def . @@ -327,7 +338,7 @@ shows "suc B \ AboveS B" proof(unfold suc_def) have "AboveS B \ Field r" - using AboveS_Field by auto + using AboveS_Field[of r] by auto thus "minim (AboveS B) \ AboveS B" using assms by (simp add: minim_in) qed @@ -340,7 +351,7 @@ proof- from assms suc_AboveS have "suc B \ AboveS B" by simp - with IN AboveS_def show ?thesis by simp + with IN AboveS_def[of r] show ?thesis by simp qed @@ -349,7 +360,7 @@ shows "(suc B,a) \ r" proof(unfold suc_def) have "AboveS B \ Field r" - using AboveS_Field by auto + using AboveS_Field[of r] by auto thus "(minim (AboveS B),a) \ r" using assms minim_least by simp qed @@ -361,7 +372,7 @@ proof- have "suc B \ AboveS B" using suc_AboveS assms by simp thus ?thesis - using assms AboveS_Field by auto + using assms AboveS_Field[of r] by auto qed @@ -371,7 +382,7 @@ shows "a = suc B" proof(unfold suc_def) have "AboveS B \ Field r" - using AboveS_Field[of B] by auto + using AboveS_Field[of r B] by auto thus "a = minim (AboveS B)" using assms equals_minim by simp @@ -383,17 +394,17 @@ shows "a = suc (underS a)" proof- have "underS a \ Field r" - using underS_Field by auto + using underS_Field[of r] by auto moreover have "a \ AboveS (underS a)" - using in_AboveS_underS IN by auto + using in_AboveS_underS IN by fast moreover have "\a' \ AboveS (underS a). (a,a') \ r" proof(clarify) fix a' assume *: "a' \ AboveS (underS a)" hence **: "a' \ Field r" - using AboveS_Field by auto + using AboveS_Field by fast {assume "(a,a') \ r" hence "a' = a \ (a',a) \ r" using TOTAL IN ** by (auto simp add: total_on_def) @@ -407,7 +418,7 @@ hence "a' \ underS a" unfolding underS_def by simp hence "a' \ AboveS (underS a)" - using AboveS_disjoint by blast + using AboveS_disjoint by fast with * have False by simp } ultimately have "(a,a') \ r" by blast @@ -486,7 +497,7 @@ hence "(?a,x) \ r" using TOTAL total_on_def[of "Field r" r] 2 4 11 12 by auto - hence "?a \ under x" using under_def by auto + hence "?a \ under x" using under_def[of r] by auto hence "?a \ A" using ** 13 by blast with 4 have False by simp } @@ -527,7 +538,7 @@ thus "(\ a \ A. under a) \ A" by blast next have "\a \ A. a \ under a" - using REFL Refl_under_in assms ofilter_def by blast + using REFL Refl_under_in[of r] assms ofilter_def[of A] by blast thus "A \ (\ a \ A. under a)" by blast qed @@ -562,13 +573,13 @@ } moreover {assume "(a,b) \ r" - with underS_incr TRANS ANTISYM 1 2 + with underS_incr[of r] TRANS ANTISYM 1 2 have "A \ B" by auto hence ?thesis by auto } moreover {assume "(b,a) \ r" - with underS_incr TRANS ANTISYM 1 2 + with underS_incr[of r] TRANS ANTISYM 1 2 have "B \ A" by auto hence ?thesis by auto } @@ -582,7 +593,7 @@ shows "A \ (AboveS A) = Field r" proof show "A \ (AboveS A) \ Field r" - using assms ofilter_def AboveS_Field by auto + using assms ofilter_def AboveS_Field[of r] by auto next {fix x assume *: "x \ Field r" and **: "x \ A" {fix y assume ***: "y \ A" @@ -592,7 +603,7 @@ have "y \ Field r" using assms ofilter_def *** by auto ultimately have "(x,y) \ r" using 1 * TOTAL total_on_def[of _ r] by auto - with *** assms ofilter_def under_def have "x \ A" by auto + with *** assms ofilter_def under_def[of r] have "x \ A" by auto with ** have False by contradiction } hence "(y,x) \ r" by blast @@ -610,7 +621,7 @@ shows "b \ A" proof- have *: "suc A \ Field r \ b \ Field r" - using WELL REL well_order_on_domain by auto + using WELL REL well_order_on_domain[of "Field r"] by auto {assume **: "b \ A" hence "b \ AboveS A" using OF * ofilter_AboveS_Field by auto