(* Title: HOL/BNF_Wellorder_Relation.thy Author: Andrei Popescu, TU Muenchen Copyright 2012 Well-order relations as needed by bounded natural functors. *) header {* 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}, @{text "max2"}, and the minimum {\em of a set}, @{text "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 @{text "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 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 show ?thesis proof(simp add: isMinim_def, rule exI[of _ b], auto) show "b \ B" using * by simp next fix b' 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 {assume "b' = b" hence "(b,b') \ r" using ** REFL by (auto simp add: refl_on_def) } moreover {assume "b' \ b \ (b',b) \ r" hence "(b,b') \ r" using ** TOTAL by (auto simp add: total_on_def) } ultimately show "(b,b') \ r" by blast qed 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(unfold ofilter_def under_def, auto simp add: Field_def) fix aa x assume "(aa,a) \ r" "(x,aa) \ r" thus "(x,a) \ r" using TRANS trans_def[of r] by blast qed lemma underS_ofilter: "ofilter (underS a)" proof(unfold ofilter_def underS_def under_def, auto simp add: Field_def) 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 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, simp) 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(unfold underS_def, auto simp add: 4) 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 } thus "(x,?a) \ r" by blast qed next show "underS ?a \ A" proof(unfold underS_def, auto) fix x assume **: "x \ ?a" and ***: "(x,?a) \ r" hence 11: "x \ Field r" using Field_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] ** *** by auto } thus "x \ A" by blast qed qed ultimately have ?One using 2 by blast thus ?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