(* Title: HOL/Cardinals/Wellorder_Relation.thy
Author: Andrei Popescu, TU Muenchen
Copyright 2012
Well-order relations.
*)
section \<open>Well-Order Relations\<close>
theory Wellorder_Relation
imports Wellfounded_More
begin
context wo_rel
begin
subsection \<open>Auxiliaries\<close>
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) \<in> r - Id \<Longrightarrow> phi a b); (a = b \<Longrightarrow> phi a b)\<rbrakk>
\<Longrightarrow> phi a b"
using TOTALS by auto
subsection \<open>Well-founded induction and recursion adapted to non-strict well-order relations\<close>
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 \<open>Properties of max2\<close>
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 \<open>Properties of minim\<close>
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\
\<Longrightarrow> 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 \<open>Properties of supr\<close>
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)\
\<Longrightarrow> (supr B, a) \<in> 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 \<open>Properties of successor\<close>
lemma suc_least:
"\B \ Field r; a \ Field r; (\ b. b \ B \ a \ b \ (b,a) \ r)\
\<Longrightarrow> (suc B, a) \<in> 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 \<open>Properties of order filters\<close>
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 \<open>Other properties\<close>
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
¤ Dauer der Verarbeitung: 0.8 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
