(* Title: HOL/BNF_Wellorder_Relation.thy Author: Andrei Popescu, TU Muenchen Copyright 2012 Well-order relations as needed by bounded natural functors. *) section ‹Well-Order Relations as Needed by Bounded Natural Functors› theory BNF_Wellorder_Relation imports Order_Relation begin text‹In this section, we develop basic concepts and results pertaining to well-order relations. Note that we consider well-order relations as {\em non-strict relations}, i.e., as containing the diagonals of their fields.› locale wo_rel = fixes r :: "'a rel" assumes WELL: "Well_order r" begin text‹The following context encompasses all this section. In other words, for the whole section, we consider a fixed well-order relation \<^term>‹r›.› (* context wo_rel *) abbreviation under where "under ≡ Order_Relation.under r" abbreviation underS where "underS ≡ Order_Relation.underS r" abbreviation Under where "Under ≡ Order_Relation.Under r" abbreviation UnderS where "UnderS ≡ Order_Relation.UnderS r" abbreviation above where "above ≡ Order_Relation.above r" abbreviation aboveS where "aboveS ≡ Order_Relation.aboveS r" abbreviation Above where "Above ≡ Order_Relation.Above r" abbreviation AboveS where "AboveS ≡ Order_Relation.AboveS r" abbreviation ofilter where "ofilter ≡ Order_Relation.ofilter r" lemmas ofilter_def = Order_Relation.ofilter_def[of r] subsection ‹Auxiliaries› lemma REFL: "Refl r" using WELL order_on_defs[of _ r] by auto lemma TRANS: "trans r" using WELL order_on_defs[of _ r] by auto lemma ANTISYM: "antisym r" using WELL order_on_defs[of _ r] by auto lemma TOTAL: "Total r" using WELL order_on_defs[of _ r] by auto lemma TOTALS: "∀a ∈ Field r. ∀b ∈ Field r. (a,b) ∈ r ∨ (b,a) ∈ r" using REFL TOTAL refl_on_def[of _ r] total_on_def[of _ r] by force lemma LIN: "Linear_order r" using WELL well_order_on_def[of _ r] by auto lemma WF: "wf (r - Id)" using WELL well_order_on_def[of _ r] by auto lemma cases_Total: "⋀ phi a b. ⟦{a,b} <= Field r; ((a,b) ∈ r ⟹ phi a b); ((b,a) ∈ r ⟹ phi a b)⟧ ⟹ phi a b" using TOTALS by auto lemma cases_Total3: "⋀ phi a b. ⟦{a,b} ≤ Field r; ((a,b) ∈ r - Id ∨ (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› text‹Here we provide induction and recursion principles specific to {\em non-strict} well-order relations. Although minor variations of those for well-founded relations, they will be useful for doing away with the tediousness of having to take out the diagonal each time in order to switch to a well-founded relation.› lemma well_order_induct: assumes IND: "⋀x. ∀y. y ≠ x ∧ (y, x) ∈ r ⟶ P y ⟹ P x" shows "P a" proof- have "⋀x. ∀y. (y, x) ∈ r - Id ⟶ P y ⟹ P x" using IND by blast thus "P a" using WF wf_induct[of "r - Id" P a] by blast qed definition worec :: "(('a ⇒ 'b) ⇒ 'a ⇒ 'b) ⇒ 'a ⇒ 'b" where "worec F ≡ wfrec (r - Id) F" definition adm_wo :: "(('a ⇒ 'b) ⇒ 'a ⇒ 'b) ⇒ bool" where "adm_wo H ≡ ∀f g x. (∀y ∈ underS x. f y = g y) ⟶ H f x = H g x" lemma worec_fixpoint: assumes ADM: "adm_wo H" shows "worec H = H (worec H)" proof- let ?rS = "r - Id" have "adm_wf (r - Id) H" unfolding adm_wf_def 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 . qed subsection ‹The notions of maximum, minimum, supremum, successor and order filter› text‹ We define the successor {\em of a set}, and not of an element (the latter is of course a particular case). Also, we define the maximum {\em of two elements}, ‹max2›, and the minimum {\em of a set}, ‹minim› -- we chose these variants since we consider them the most useful for well-orders. The minimum is defined in terms of the auxiliary relational operator ‹isMinim›. Then, supremum and successor are defined in terms of minimum as expected. The minimum is only meaningful for non-empty sets, and the successor is only meaningful for sets for which strict upper bounds exist. Order filters for well-orders are also known as ``initial segments".› definition max2 :: "'a ⇒ 'a ⇒ 'a" where "max2 a b ≡ if (a,b) ∈ r then b else a" definition isMinim :: "'a set ⇒ 'a ⇒ bool" where "isMinim A b ≡ b ∈ A ∧ (∀a ∈ A. (b,a) ∈ r)" definition minim :: "'a set ⇒ 'a" where "minim A ≡ THE b. isMinim A b" definition supr :: "'a set ⇒ 'a" where "supr A ≡ minim (Above A)" definition suc :: "'a set ⇒ 'a" where "suc A ≡ minim (AboveS A)" subsubsection ‹Properties of max2› lemma max2_greater_among: assumes "a ∈ Field r" and "b ∈ Field r" shows "(a, max2 a b) ∈ r ∧ (b, max2 a b) ∈ r ∧ max2 a b ∈ {a,b}" proof- {assume "(a,b) ∈ r" hence ?thesis using max2_def assms REFL refl_on_def by (auto simp add: refl_on_def) } moreover {assume "a = b" hence "(a,b) ∈ r" using REFL assms by (auto simp add: refl_on_def) } moreover {assume *: "a ≠ b ∧ (b,a) ∈ r" hence "(a,b) ∉ r" using ANTISYM by (auto simp add: antisym_def) hence ?thesis using * max2_def assms REFL refl_on_def by (auto simp add: refl_on_def) } ultimately show ?thesis using assms TOTAL total_on_def[of "Field r" r] by blast qed lemma max2_greater: assumes "a ∈ Field r" and "b ∈ Field r" shows "(a, max2 a b) ∈ r ∧ (b, max2 a b) ∈ r" using assms by (auto simp add: max2_greater_among) lemma max2_among: assumes "a ∈ Field r" and "b ∈ Field r" shows "max2 a b ∈ {a, b}" using assms max2_greater_among[of a b] by simp lemma max2_equals1: assumes "a ∈ Field r" and "b ∈ Field r" shows "(max2 a b = a) = ((b,a) ∈ r)" using assms ANTISYM unfolding antisym_def using TOTALS by(auto simp add: max2_def max2_among) lemma max2_equals2: assumes "a ∈ Field r" and "b ∈ Field r" shows "(max2 a b = b) = ((a,b) ∈ r)" using assms ANTISYM unfolding antisym_def using TOTALS unfolding max2_def by auto lemma in_notinI: assumes "(j,i) ∉ r ∨ j = i" and "i ∈ Field r" and "j ∈ Field r" shows "(i,j) ∈ r" using assms max2_def max2_greater_among by fastforce subsubsection ‹Existence and uniqueness for isMinim and well-definedness of minim› lemma isMinim_unique: assumes MINIM: "isMinim B a" and MINIM': "isMinim B a'" shows "a = a'" proof- {have "a ∈ B" using MINIM isMinim_def by simp hence "(a',a) ∈ r" using MINIM' isMinim_def by simp } moreover {have "a' ∈ B" using MINIM' isMinim_def by simp hence "(a,a') ∈ r" using MINIM isMinim_def by simp } ultimately show ?thesis using ANTISYM antisym_def[of r] by blast qed lemma Well_order_isMinim_exists: assumes SUB: "B ≤ Field r" and NE: "B ≠ {}" shows "∃b. isMinim B b" proof- from spec[OF WF[unfolded wf_eq_minimal[of "r - Id"]], of B] NE obtain b where *: "b ∈ B ∧ (∀b'. b' ≠ b ∧ (b',b) ∈ r ⟶ b' ∉ B)" by auto have "∀b'. b' ∈ B ⟶ (b, b') ∈ r" proof fix b' show "b' ∈ B ⟶ (b, b') ∈ r" proof assume As: "b' ∈ B" hence **: "b ∈ Field r ∧ b' ∈ Field r" using As SUB * by auto from As * have "b' = b ∨ (b',b) ∉ r" by auto moreover have "b' = b ⟹ (b, b') ∈ r" using ** REFL by (auto simp add: refl_on_def) moreover have "b' ≠ b ∧ (b',b) ∉ r ⟹ (b,b') ∈ r" using ** TOTAL by (auto simp add: total_on_def) ultimately show "(b,b') ∈ r" by blast qed qed then have "isMinim B b" unfolding isMinim_def using * by auto then show ?thesis by auto qed lemma minim_isMinim: assumes SUB: "B ≤ Field r" and NE: "B ≠ {}" shows "isMinim B (minim B)" proof- let ?phi = "(λ b. isMinim B b)" from assms Well_order_isMinim_exists obtain b where *: "?phi b" by blast moreover have "⋀ b'. ?phi b' ⟹ b' = b" using isMinim_unique * by auto ultimately show ?thesis unfolding minim_def using theI[of ?phi b] by blast qed subsubsection‹Properties of minim› lemma minim_in: assumes "B ≤ Field r" and "B ≠ {}" shows "minim B ∈ B" proof- from minim_isMinim[of B] assms have "isMinim B (minim B)" by simp thus ?thesis by (simp add: isMinim_def) qed lemma minim_inField: assumes "B ≤ Field r" and "B ≠ {}" shows "minim B ∈ Field r" proof- have "minim B ∈ B" using assms by (simp add: minim_in) thus ?thesis using assms by blast qed lemma minim_least: assumes SUB: "B ≤ Field r" and IN: "b ∈ B" shows "(minim B, b) ∈ r" proof- from minim_isMinim[of B] assms have "isMinim B (minim B)" by auto thus ?thesis by (auto simp add: isMinim_def IN) qed lemma equals_minim: assumes SUB: "B ≤ Field r" and IN: "a ∈ B" and LEAST: "⋀ b. b ∈ B ⟹ (a,b) ∈ r" shows "a = minim B" proof- from minim_isMinim[of B] assms have "isMinim B (minim B)" by auto moreover have "isMinim B a" using IN LEAST isMinim_def by auto ultimately show ?thesis using isMinim_unique by auto qed subsubsection‹Properties of successor› lemma suc_AboveS: assumes SUB: "B ≤ Field r" and ABOVES: "AboveS B ≠ {}" shows "suc B ∈ AboveS B" proof(unfold suc_def) have "AboveS B ≤ Field r" using AboveS_Field[of r] by auto thus "minim (AboveS B) ∈ AboveS B" using assms by (simp add: minim_in) qed lemma suc_greater: assumes SUB: "B ≤ Field r" and ABOVES: "AboveS B ≠ {}" and IN: "b ∈ B" shows "suc B ≠ b ∧ (b,suc B) ∈ r" proof- from assms suc_AboveS have "suc B ∈ AboveS B" by simp with IN AboveS_def[of r] show ?thesis by simp qed lemma suc_least_AboveS: assumes ABOVES: "a ∈ AboveS B" shows "(suc B,a) ∈ r" proof(unfold suc_def) have "AboveS B ≤ Field r" using AboveS_Field[of r] by auto thus "(minim (AboveS B),a) ∈ r" using assms minim_least by simp qed lemma suc_inField: assumes "B ≤ Field r" and "AboveS B ≠ {}" shows "suc B ∈ Field r" proof- have "suc B ∈ AboveS B" using suc_AboveS assms by simp thus ?thesis using assms AboveS_Field[of r] by auto qed lemma equals_suc_AboveS: assumes SUB: "B ≤ Field r" and ABV: "a ∈ AboveS B" and MINIM: "⋀ a'. a' ∈ AboveS B ⟹ (a,a') ∈ r" shows "a = suc B" proof(unfold suc_def) have "AboveS B ≤ Field r" using AboveS_Field[of r B] by auto thus "a = minim (AboveS B)" using assms equals_minim by simp qed lemma suc_underS: assumes IN: "a ∈ Field r" shows "a = suc (underS a)" proof- have "underS a ≤ Field r" using underS_Field[of r] by auto moreover have "a ∈ AboveS (underS a)" 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 fast {assume "(a,a') ∉ r" hence "a' = a ∨ (a',a) ∈ r" using TOTAL IN ** by (auto simp add: total_on_def) moreover {assume "a' = a" hence "(a,a') ∈ r" using REFL IN ** by (auto simp add: refl_on_def) } moreover {assume "a' ≠ a ∧ (a',a) ∈ r" hence "a' ∈ underS a" unfolding underS_def by simp hence "a' ∉ AboveS (underS a)" using AboveS_disjoint by fast with * have False by simp } ultimately have "(a,a') ∈ r" by blast } thus "(a, a') ∈ r" by blast qed ultimately show ?thesis using equals_suc_AboveS by auto qed subsubsection ‹Properties of order filters› lemma under_ofilter: "ofilter (under a)" proof - have "⋀aa x. (aa, a) ∈ r ⟹ (x, aa) ∈ r ⟹ (x, a) ∈ r" proof - fix aa x assume "(aa,a) ∈ r" "(x,aa) ∈ r" then show "(x,a) ∈ r" using TRANS trans_def[of r] by blast qed then show ?thesis unfolding ofilter_def under_def by (auto simp add: Field_def) qed lemma underS_ofilter: "ofilter (underS a)" unfolding ofilter_def underS_def under_def proof safe fix aa assume "(a, aa) ∈ r" "(aa, a) ∈ r" and DIFF: "aa ≠ a" thus False using ANTISYM antisym_def[of r] by blast next fix aa x assume "(aa,a) ∈ r" "aa ≠ a" "(x,aa) ∈ r" thus "(x,a) ∈ r" using TRANS trans_def[of r] by blast next fix x assume "x ≠ a" and "(x, a) ∈ r" then show "x ∈ Field r" unfolding Field_def by auto qed lemma Field_ofilter: "ofilter (Field r)" by(unfold ofilter_def under_def, auto simp add: Field_def) lemma ofilter_underS_Field: "ofilter A = ((∃a ∈ Field r. A = underS a) ∨ (A = Field r))" proof assume "(∃a∈Field r. A = underS a) ∨ A = Field r" thus "ofilter A" by (auto simp: underS_ofilter Field_ofilter) next assume *: "ofilter A" let ?One = "(∃a∈Field r. A = underS a)" let ?Two = "(A = Field r)" show "?One ∨ ?Two" proof(cases ?Two) let ?B = "(Field r) - A" let ?a = "minim ?B" assume "A ≠ Field r" moreover have "A ≤ Field r" using * ofilter_def by simp ultimately have 1: "?B ≠ {}" by blast hence 2: "?a ∈ Field r" using minim_inField[of ?B] by blast have 3: "?a ∈ ?B" using minim_in[of ?B] 1 by blast hence 4: "?a ∉ A" by blast have 5: "A ≤ Field r" using * ofilter_def by auto (* *) moreover have "A = underS ?a" proof show "A ≤ underS ?a" proof fix x assume **: "x ∈ A" hence 11: "x ∈ Field r" using 5 by auto have 12: "x ≠ ?a" using 4 ** by auto have 13: "under x ≤ A" using * ofilter_def ** by auto {assume "(x,?a) ∉ r" 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[of r] by auto hence "?a ∈ A" using ** 13 by blast with 4 have False by simp } then have "(x,?a) ∈ r" by blast thus "x ∈ underS ?a" unfolding underS_def by (auto simp add: 12) qed next show "underS ?a ≤ A" proof fix x assume **: "x ∈ underS ?a" hence 11: "x ∈ Field r" using Field_def unfolding underS_def by fastforce {assume "x ∉ A" hence "x ∈ ?B" using 11 by auto hence "(?a,x) ∈ r" using 3 minim_least[of ?B x] by blast hence False using ANTISYM antisym_def[of r] ** unfolding underS_def by auto } thus "x ∈ A" by blast qed qed ultimately have ?One using 2 by blast thus ?thesis by simp next assume "A = Field r" then show ?thesis by simp qed qed lemma ofilter_UNION: "(⋀ i. i ∈ I ⟹ ofilter(A i)) ⟹ ofilter (⋃i ∈ I. A i)" unfolding ofilter_def by blast lemma ofilter_under_UNION: assumes "ofilter A" shows "A = (⋃a ∈ A. under a)" proof have "∀a ∈ A. under a ≤ A" using assms ofilter_def by auto thus "(⋃a ∈ A. under a) ≤ A" by blast next have "∀a ∈ A. a ∈ under a" using REFL Refl_under_in[of r] assms ofilter_def[of A] by blast thus "A ≤ (⋃a ∈ A. under a)" by blast qed subsubsection‹Other properties› lemma ofilter_linord: assumes OF1: "ofilter A" and OF2: "ofilter B" shows "A ≤ B ∨ B ≤ A" proof(cases "A = Field r") assume Case1: "A = Field r" hence "B ≤ A" using OF2 ofilter_def by auto thus ?thesis by simp next assume Case2: "A ≠ Field r" with ofilter_underS_Field OF1 obtain a where 1: "a ∈ Field r ∧ A = underS a" by auto show ?thesis proof(cases "B = Field r") assume Case21: "B = Field r" hence "A ≤ B" using OF1 ofilter_def by auto thus ?thesis by simp next assume Case22: "B ≠ Field r" with ofilter_underS_Field OF2 obtain b where 2: "b ∈ Field r ∧ B = underS b" by auto have "a = b ∨ (a,b) ∈ r ∨ (b,a) ∈ r" using 1 2 TOTAL total_on_def[of _ r] by auto moreover {assume "a = b" with 1 2 have ?thesis by auto } moreover {assume "(a,b) ∈ r" 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[of r] TRANS ANTISYM 1 2 have "B ≤ A" by auto hence ?thesis by auto } ultimately show ?thesis by blast qed qed lemma ofilter_AboveS_Field: assumes "ofilter A" shows "A ∪ (AboveS A) = Field r" proof show "A ∪ (AboveS A) ≤ Field r" 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" with ** have 1: "y ≠ x" by auto {assume "(y,x) ∉ r" moreover 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[of r] have "x ∈ A" by auto with ** have False by contradiction } hence "(y,x) ∈ r" by blast with 1 have "y ≠ x ∧ (y,x) ∈ r" by auto } with * have "x ∈ AboveS A" unfolding AboveS_def by auto } thus "Field r ≤ A ∪ (AboveS A)" by blast qed lemma suc_ofilter_in: assumes OF: "ofilter A" and ABOVE_NE: "AboveS A ≠ {}" and REL: "(b,suc A) ∈ r" and DIFF: "b ≠ suc A" shows "b ∈ A" proof- have *: "suc A ∈ Field r ∧ b ∈ Field r" 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 hence "(suc A, b) ∈ r" using suc_least_AboveS by auto hence False using REL DIFF ANTISYM * by (auto simp add: antisym_def) } thus ?thesis by blast qed end (* context wo_rel *) end