(* Title: HOL/Cardinals/Wellorder_Relation.thy Author: Andrei Popescu, TU Muenchen Copyright 2012 Well-order relations. *) section ‹Well-Order Relations› theory Wellorder_Relation imports Wellfounded_More begin context wo_rel begin subsection ‹Auxiliaries› lemma PREORD: "Preorder r" using WELL order_on_defs[of _ r] by auto lemma PARORD: "Partial_order r" using WELL order_on_defs[of _ r] by auto lemma cases_Total2: "⋀ phi a b. ⟦{a,b} ≤ Field r; ((a,b) ∈ r - Id ⟹ phi a b); ((b,a) ∈ r - Id ⟹ phi a b); (a = b ⟹ phi a b)⟧ ⟹ phi a b" using TOTALS by auto subsection ‹Well-founded induction and recursion adapted to non-strict well-order relations› lemma worec_unique_fixpoint: assumes ADM: "adm_wo H" and fp: "f = H f" shows "f = worec H" proof- have "adm_wf (r - Id) H" unfolding adm_wf_def 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 . qed subsubsection ‹Properties of max2› lemma max2_iff: assumes "a ∈ Field r" and "b ∈ Field r" shows "((max2 a b, c) ∈ r) = ((a,c) ∈ r ∧ (b,c) ∈ r)" proof assume "(max2 a b, c) ∈ r" thus "(a,c) ∈ r ∧ (b,c) ∈ r" using assms max2_greater[of a b] TRANS trans_def[of r] by blast next assume "(a,c) ∈ r ∧ (b,c) ∈ r" thus "(max2 a b, c) ∈ r" using assms max2_among[of a b] by auto qed subsubsection ‹Properties of minim› lemma minim_Under: "⟦B ≤ Field r; B ≠ {}⟧ ⟹ minim B ∈ Under B" by(auto simp add: Under_def minim_inField minim_least) lemma equals_minim_Under: "⟦B ≤ Field r; a ∈ B; a ∈ Under B⟧ ⟹ a = minim B" by(auto simp add: Under_def equals_minim) lemma minim_iff_In_Under: assumes SUB: "B ≤ Field r" and NE: "B ≠ {}" shows "(a = minim B) = (a ∈ B ∧ a ∈ Under B)" proof assume "a = minim B" thus "a ∈ B ∧ a ∈ Under B" using assms minim_in minim_Under by simp next assume "a ∈ B ∧ a ∈ Under B" thus "a = minim B" using assms equals_minim_Under by simp qed lemma minim_Under_under: assumes NE: "A ≠ {}" and SUB: "A ≤ Field r" shows "Under A = under (minim A)" proof- (* Preliminary facts *) have 1: "minim A ∈ A" using assms minim_in by auto have 2: "∀x ∈ A. (minim A, x) ∈ r" using assms minim_least by auto (* Main proof *) have "Under A ≤ under (minim A)" proof fix x assume "x ∈ Under A" with 1 Under_def[of r] have "(x,minim A) ∈ r" by auto thus "x ∈ under(minim A)" unfolding under_def by simp qed (* *) moreover (* *) have "under (minim A) ≤ Under A" proof fix x assume "x ∈ under(minim A)" hence 11: "(x,minim A) ∈ r" unfolding under_def by simp hence "x ∈ Field r" unfolding Field_def by auto moreover {fix a assume "a ∈ A" with 2 have "(minim A, a) ∈ r" by simp with 11 have "(x,a) ∈ r" using TRANS trans_def[of r] by blast } ultimately show "x ∈ Under A" by (unfold Under_def, auto) qed (* *) ultimately show ?thesis by blast qed lemma minim_UnderS_underS: assumes NE: "A ≠ {}" and SUB: "A ≤ Field r" shows "UnderS A = underS (minim A)" proof- (* Preliminary facts *) have 1: "minim A ∈ A" using assms minim_in by auto have 2: "∀x ∈ A. (minim A, x) ∈ r" using assms minim_least by auto (* Main proof *) have "UnderS A ≤ underS (minim A)" proof fix x assume "x ∈ UnderS A" 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 (* *) moreover (* *) have "underS (minim A) ≤ UnderS A" proof fix x assume "x ∈ underS(minim A)" hence 11: "x ≠ minim A ∧ (x,minim A) ∈ r" unfolding underS_def by simp hence "x ∈ Field r" unfolding Field_def by auto moreover {fix a assume "a ∈ A" with 2 have 3: "(minim A, a) ∈ r" by simp with 11 have "(x,a) ∈ r" using TRANS trans_def[of r] by blast moreover have "x ≠ a" proof assume "x = a" with 11 3 ANTISYM antisym_def[of r] show False by auto qed ultimately have "x ≠ a ∧ (x,a) ∈ r" by simp } ultimately show "x ∈ UnderS A" by (unfold UnderS_def, auto) qed (* *) ultimately show ?thesis by blast qed subsubsection ‹Properties of supr› lemma supr_Above: assumes SUB: "B ≤ Field r" and ABOVE: "Above B ≠ {}" shows "supr B ∈ Above B" proof(unfold supr_def) have "Above B ≤ Field r" using Above_Field[of r] by auto thus "minim (Above B) ∈ Above B" using assms by (simp add: minim_in) qed lemma supr_greater: assumes SUB: "B ≤ Field r" and ABOVE: "Above B ≠ {}" and IN: "b ∈ B" shows "(b, supr B) ∈ r" proof- from assms supr_Above have "supr B ∈ Above B" by simp with IN Above_def[of r] show ?thesis by simp qed lemma supr_least_Above: assumes SUB: "B ≤ Field r" and ABOVE: "a ∈ Above B" shows "(supr B, a) ∈ r" proof(unfold supr_def) have "Above B ≤ Field r" using Above_Field[of r] by auto thus "(minim (Above B), a) ∈ r" using assms minim_least by simp qed lemma supr_least: "⟦B ≤ Field r; a ∈ Field r; (⋀ b. b ∈ B ⟹ (b,a) ∈ r)⟧ ⟹ (supr B, a) ∈ r" by(auto simp add: supr_least_Above Above_def) lemma equals_supr_Above: assumes SUB: "B ≤ Field r" and ABV: "a ∈ Above B" and MINIM: "⋀ a'. a' ∈ Above B ⟹ (a,a') ∈ r" shows "a = supr B" proof(unfold supr_def) have "Above B ≤ Field r" using Above_Field[of r] by auto thus "a = minim (Above B)" using assms equals_minim by simp qed lemma equals_supr: assumes SUB: "B ≤ Field r" and IN: "a ∈ Field r" and ABV: "⋀ b. b ∈ B ⟹ (b,a) ∈ r" and MINIM: "⋀ a'. ⟦ a' ∈ Field r; ⋀ b. b ∈ B ⟹ (b,a') ∈ r⟧ ⟹ (a,a') ∈ r" shows "a = supr B" proof- have "a ∈ Above B" unfolding Above_def using ABV IN by simp moreover have "⋀ a'. a' ∈ Above B ⟹ (a,a') ∈ r" unfolding Above_def using MINIM by simp ultimately show ?thesis using equals_supr_Above SUB by auto qed lemma supr_inField: assumes "B ≤ Field r" and "Above B ≠ {}" shows "supr B ∈ Field r" proof- have "supr B ∈ Above B" using supr_Above assms by simp thus ?thesis using assms Above_Field[of r] by auto qed lemma supr_above_Above: assumes SUB: "B ≤ Field r" and ABOVE: "Above B ≠ {}" shows "Above B = above (supr B)" proof(unfold Above_def above_def, auto) fix a assume "a ∈ Field r" "∀b ∈ B. (b,a) ∈ r" with supr_least assms show "(supr B, a) ∈ r" by auto next fix b assume "(supr B, b) ∈ r" thus "b ∈ Field r" using REFL refl_on_def[of _ r] by auto next fix a b assume 1: "(supr B, b) ∈ r" and 2: "a ∈ B" with assms supr_greater have "(a,supr B) ∈ r" by auto thus "(a,b) ∈ r" using 1 TRANS trans_def[of r] by blast qed lemma supr_under: assumes IN: "a ∈ Field r" shows "a = supr (under a)" proof- have "under a ≤ Field r" using under_Field[of r] by auto moreover have "under a ≠ {}" using IN Refl_under_in[of r] REFL by auto moreover have "a ∈ Above (under a)" 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) fix a' assume "∀aa. (aa, a) ∈ r ⟶ (aa, a') ∈ r" hence "(a,a) ∈ r ⟶ (a,a') ∈ r" by blast moreover have "(a,a) ∈ r" using REFL IN by (auto simp add: refl_on_def) ultimately show "(a, a') ∈ r" by (rule mp) qed ultimately show ?thesis using equals_supr_Above by auto qed subsubsection ‹Properties of successor› lemma suc_least: "⟦B ≤ Field r; a ∈ Field r; (⋀ b. b ∈ B ⟹ a ≠ b ∧ (b,a) ∈ r)⟧ ⟹ (suc B, a) ∈ r" by(auto simp add: suc_least_AboveS AboveS_def) lemma equals_suc: assumes SUB: "B ≤ Field r" and IN: "a ∈ Field r" and ABVS: "⋀ b. b ∈ B ⟹ a ≠ b ∧ (b,a) ∈ r" and MINIM: "⋀ a'. ⟦a' ∈ Field r; ⋀ b. b ∈ B ⟹ a' ≠ b ∧ (b,a') ∈ r⟧ ⟹ (a,a') ∈ r" shows "a = suc B" proof- have "a ∈ AboveS B" unfolding AboveS_def using ABVS IN by simp moreover have "⋀ a'. a' ∈ AboveS B ⟹ (a,a') ∈ r" unfolding AboveS_def using MINIM by simp ultimately show ?thesis using equals_suc_AboveS SUB by auto qed lemma suc_above_AboveS: assumes SUB: "B ≤ Field r" and ABOVE: "AboveS B ≠ {}" shows "AboveS B = above (suc B)" proof(unfold AboveS_def above_def, auto) fix a assume "a ∈ Field r" "∀b ∈ B. a ≠ b ∧ (b,a) ∈ r" with suc_least assms show "(suc B,a) ∈ r" by auto next fix b assume "(suc B, b) ∈ r" thus "b ∈ Field r" using REFL refl_on_def[of _ r] by auto next fix a b assume 1: "(suc B, b) ∈ r" and 2: "a ∈ B" with assms suc_greater[of B a] have "(a,suc B) ∈ r" by auto thus "(a,b) ∈ r" using 1 TRANS trans_def[of r] by blast next fix a assume 1: "(suc B, a) ∈ r" and 2: "a ∈ B" with assms suc_greater[of B a] have "(a,suc B) ∈ r" by auto moreover have "suc B ∈ Field r" using assms suc_inField by simp ultimately have "a = suc B" using 1 2 SUB ANTISYM antisym_def[of r] by auto thus False using assms suc_greater[of B a] 2 by auto qed lemma suc_singl_pred: assumes IN: "a ∈ Field r" and ABOVE_NE: "aboveS a ≠ {}" and REL: "(a',suc {a}) ∈ r" and DIFF: "a' ≠ suc {a}" shows "a' = a ∨ (a',a) ∈ r" proof- have *: "suc {a} ∈ Field r ∧ a' ∈ Field r" 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) moreover {assume "(a,a') ∈ r" with ** * assms WELL suc_least[of "{a}" a'] have "(suc {a},a') ∈ r" by auto with REL DIFF * ANTISYM antisym_def[of r] have False by simp } ultimately have "(a',a) ∈ r" by blast } thus ?thesis by blast qed lemma under_underS_suc: assumes IN: "a ∈ Field r" and ABV: "aboveS a ≠ {}" shows "underS (suc {a}) = under a" proof- have 1: "AboveS {a} ≠ {}" 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 (* *) have "underS (suc {a}) ≤ under a" proof(unfold underS_def under_def, auto) fix x assume *: "x ≠ suc {a}" and **: "(x,suc {a}) ∈ r" with suc_singl_pred[of a x] IN ABV have "x = a ∨ (x,a) ∈ r" by auto with REFL refl_on_def[of _ r] IN show "(x,a) ∈ r" by auto qed (* *) moreover (* *) have "under a ≤ underS (suc {a})" proof(unfold underS_def under_def, auto) assume "(suc {a}, a) ∈ r" with 2 ANTISYM antisym_def[of r] show False by auto next fix x assume *: "(x,a) ∈ r" with 2 TRANS trans_def[of r] show "(x,suc {a}) ∈ r" by blast (* blast is often better than auto/auto for transitivity-like properties *) qed (* *) ultimately show ?thesis by blast qed subsubsection ‹Properties of order filters› lemma ofilter_Under[simp]: assumes "A ≤ Field r" shows "ofilter(Under A)" proof(unfold ofilter_def, auto) fix x assume "x ∈ Under A" thus "x ∈ Field r" 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[of r] by auto qed lemma ofilter_UnderS[simp]: assumes "A ≤ Field r" shows "ofilter(UnderS A)" proof(unfold ofilter_def, auto) fix x assume "x ∈ UnderS A" thus "x ∈ Field r" 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[of r] by auto qed lemma ofilter_Int[simp]: "⟦ofilter A; ofilter B⟧ ⟹ ofilter(A Int B)" unfolding ofilter_def by blast lemma ofilter_Un[simp]: "⟦ofilter A; ofilter B⟧ ⟹ ofilter(A ∪ B)" unfolding ofilter_def by blast lemma ofilter_INTER: "⟦I ≠ {}; ⋀ i. i ∈ I ⟹ ofilter(A i)⟧ ⟹ ofilter (⋂i ∈ I. A i)" unfolding ofilter_def by blast lemma ofilter_Inter: "⟦S ≠ {}; ⋀ A. A ∈ S ⟹ ofilter A⟧ ⟹ ofilter (⋂S)" unfolding ofilter_def by blast lemma ofilter_Union: "(⋀ A. A ∈ S ⟹ ofilter A) ⟹ ofilter (⋃S)" unfolding ofilter_def by blast lemma ofilter_under_Union: "ofilter A ⟹ A = ⋃{under a| a. a ∈ A}" using ofilter_under_UNION [of A] by auto subsubsection ‹Other properties› lemma Trans_Under_regressive: assumes NE: "A ≠ {}" and SUB: "A ≤ Field r" shows "Under(Under A) ≤ Under A" proof let ?a = "minim A" (* Preliminary facts *) have 1: "minim A ∈ Under A" using assms minim_Under by auto have 2: "∀y ∈ A. (minim A, y) ∈ r" using assms minim_least by auto (* Main proof *) fix x assume "x ∈ Under(Under A)" with 1 have 1: "(x,minim A) ∈ r" using Under_def[of r] by auto with Field_def have "x ∈ Field r" by fastforce moreover {fix y assume *: "y ∈ A" hence "(x,y) ∈ r" using 1 2 TRANS trans_def[of r] by blast with Field_def have "(x,y) ∈ r" by auto } ultimately show "x ∈ Under A" unfolding Under_def by auto qed lemma ofilter_suc_Field: assumes OF: "ofilter A" and NE: "A ≠ Field r" shows "ofilter (A ∪ {suc A})" proof- (* Preliminary facts *) have 1: "A ≤ Field r" using OF ofilter_def by auto hence 2: "AboveS A ≠ {}" using ofilter_AboveS_Field NE OF by blast from 1 2 suc_inField have 3: "suc A ∈ Field r" by auto (* Main proof *) show ?thesis proof(unfold ofilter_def, auto simp add: 1 3) fix a x assume "a ∈ A" "x ∈ under a" "x ∉ A" with OF ofilter_def have False by auto thus "x = suc A" by simp next fix x assume *: "x ∈ under (suc A)" and **: "x ∉ A" hence "x ∈ Field r" using under_def Field_def by fastforce with ** have "x ∈ AboveS A" using ofilter_AboveS_Field[of A] OF by auto hence "(suc A,x) ∈ r" using suc_least_AboveS by auto moreover 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 qed (* FIXME: needed? *) declare minim_in[simp] minim_inField[simp] minim_least[simp] under_ofilter[simp] underS_ofilter[simp] Field_ofilter[simp] end abbreviation "worec ≡ wo_rel.worec" abbreviation "adm_wo ≡ wo_rel.adm_wo" abbreviation "isMinim ≡ wo_rel.isMinim" abbreviation "minim ≡ wo_rel.minim" abbreviation "max2 ≡ wo_rel.max2" abbreviation "supr ≡ wo_rel.supr" abbreviation "suc ≡ wo_rel.suc" end