--- a/src/HOL/BNF_Wellorder_Relation.thy Tue Jan 21 16:56:34 2014 +0100
+++ b/src/HOL/BNF_Wellorder_Relation.thy Wed Jan 22 09:45:30 2014 +0100
@@ -11,13 +11,11 @@
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"
@@ -40,49 +38,39 @@
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: "\<forall>a \<in> Field r. \<forall>b \<in> Field r. (a,b) \<in> r \<or> (b,a) \<in> 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:
"\<And> phi a b. \<lbrakk>{a,b} <= Field r; ((a,b) \<in> r \<Longrightarrow> phi a b); ((b,a) \<in> r \<Longrightarrow> phi a b)\<rbrakk>
\<Longrightarrow> phi a b"
using TOTALS by auto
-
lemma cases_Total3:
"\<And> phi a b. \<lbrakk>{a,b} \<le> Field r; ((a,b) \<in> r - Id \<or> (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 {* Well-founded induction and recursion adapted to non-strict well-order relations *}
-
+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.
@@ -90,7 +78,6 @@
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: "\<And>x. \<forall>y. y \<noteq> x \<and> (y, x) \<in> r \<longrightarrow> P y \<Longrightarrow> P x"
shows "P a"
@@ -100,19 +87,16 @@
thus "P a" using WF wf_induct[of "r - Id" P a] by blast
qed
-
definition
worec :: "(('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
where
"worec F \<equiv> wfrec (r - Id) F"
-
definition
adm_wo :: "(('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> bool"
where
"adm_wo H \<equiv> \<forall>f g x. (\<forall>y \<in> underS x. f y = g y) \<longrightarrow> H f x = H g x"
-
lemma worec_fixpoint:
assumes ADM: "adm_wo H"
shows "worec H = H (worec H)"
@@ -127,8 +111,7 @@
qed
-subsection {* The notions of maximum, minimum, supremum, successor and order filter *}
-
+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
@@ -141,18 +124,15 @@
meaningful for sets for which strict upper bounds exist.
Order filters for well-orders are also known as ``initial segments". *}
-
definition max2 :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
where "max2 a b \<equiv> if (a,b) \<in> r then b else a"
-
definition isMinim :: "'a set \<Rightarrow> 'a \<Rightarrow> bool"
where "isMinim A b \<equiv> b \<in> A \<and> (\<forall>a \<in> A. (b,a) \<in> r)"
definition minim :: "'a set \<Rightarrow> 'a"
where "minim A \<equiv> THE b. isMinim A b"
-
definition supr :: "'a set \<Rightarrow> 'a"
where "supr A \<equiv> minim (Above A)"
@@ -166,7 +146,6 @@
subsubsection {* Properties of max2 *}
-
lemma max2_greater_among:
assumes "a \<in> Field r" and "b \<in> Field r"
shows "(a, max2 a b) \<in> r \<and> (b, max2 a b) \<in> r \<and> max2 a b \<in> {a,b}"
@@ -191,26 +170,22 @@
total_on_def[of "Field r" r] by blast
qed
-
lemma max2_greater:
assumes "a \<in> Field r" and "b \<in> Field r"
shows "(a, max2 a b) \<in> r \<and> (b, max2 a b) \<in> r"
using assms by (auto simp add: max2_greater_among)
-
lemma max2_among:
assumes "a \<in> Field r" and "b \<in> Field r"
shows "max2 a b \<in> {a, b}"
using assms max2_greater_among[of a b] by simp
-
lemma max2_equals1:
assumes "a \<in> Field r" and "b \<in> Field r"
shows "(max2 a b = a) = ((b,a) \<in> r)"
using assms ANTISYM unfolding antisym_def using TOTALS
by(auto simp add: max2_def max2_among)
-
lemma max2_equals2:
assumes "a \<in> Field r" and "b \<in> Field r"
shows "(max2 a b = b) = ((a,b) \<in> r)"
@@ -220,7 +195,6 @@
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'"
@@ -240,7 +214,6 @@
show ?thesis using ANTISYM antisym_def[of r] by blast
qed
-
lemma Well_order_isMinim_exists:
assumes SUB: "B \<le> Field r" and NE: "B \<noteq> {}"
shows "\<exists>b. isMinim B b"
@@ -269,7 +242,6 @@
qed
qed
-
lemma minim_isMinim:
assumes SUB: "B \<le> Field r" and NE: "B \<noteq> {}"
shows "isMinim B (minim B)"
@@ -284,10 +256,8 @@
unfolding minim_def using theI[of ?phi b] by blast
qed
-
subsubsection{* Properties of minim *}
-
lemma minim_in:
assumes "B \<le> Field r" and "B \<noteq> {}"
shows "minim B \<in> B"
@@ -297,7 +267,6 @@
thus ?thesis by (simp add: isMinim_def)
qed
-
lemma minim_inField:
assumes "B \<le> Field r" and "B \<noteq> {}"
shows "minim B \<in> Field r"
@@ -306,7 +275,6 @@
thus ?thesis using assms by blast
qed
-
lemma minim_least:
assumes SUB: "B \<le> Field r" and IN: "b \<in> B"
shows "(minim B, b) \<in> r"
@@ -316,7 +284,6 @@
thus ?thesis by (auto simp add: isMinim_def IN)
qed
-
lemma equals_minim:
assumes SUB: "B \<le> Field r" and IN: "a \<in> B" and
LEAST: "\<And> b. b \<in> B \<Longrightarrow> (a,b) \<in> r"
@@ -329,10 +296,8 @@
using isMinim_unique by auto
qed
-
subsubsection{* Properties of successor *}
-
lemma suc_AboveS:
assumes SUB: "B \<le> Field r" and ABOVES: "AboveS B \<noteq> {}"
shows "suc B \<in> AboveS B"
@@ -343,7 +308,6 @@
using assms by (simp add: minim_in)
qed
-
lemma suc_greater:
assumes SUB: "B \<le> Field r" and ABOVES: "AboveS B \<noteq> {}" and
IN: "b \<in> B"
@@ -354,7 +318,6 @@
with IN AboveS_def[of r] show ?thesis by simp
qed
-
lemma suc_least_AboveS:
assumes ABOVES: "a \<in> AboveS B"
shows "(suc B,a) \<in> r"
@@ -365,7 +328,6 @@
using assms minim_least by simp
qed
-
lemma suc_inField:
assumes "B \<le> Field r" and "AboveS B \<noteq> {}"
shows "suc B \<in> Field r"
@@ -375,7 +337,6 @@
using assms AboveS_Field[of r] by auto
qed
-
lemma equals_suc_AboveS:
assumes SUB: "B \<le> Field r" and ABV: "a \<in> AboveS B" and
MINIM: "\<And> a'. a' \<in> AboveS B \<Longrightarrow> (a,a') \<in> r"
@@ -388,7 +349,6 @@
by simp
qed
-
lemma suc_underS:
assumes IN: "a \<in> Field r"
shows "a = suc (underS a)"
@@ -432,7 +392,6 @@
subsubsection {* Properties of order filters *}
-
lemma under_ofilter:
"ofilter (under a)"
proof(unfold ofilter_def under_def, auto simp add: Field_def)
@@ -442,7 +401,6 @@
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)
@@ -456,12 +414,10 @@
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 = ((\<exists>a \<in> Field r. A = underS a) \<or> (A = Field r))"
proof
@@ -523,12 +479,10 @@
qed
qed
-
lemma ofilter_UNION:
"(\<And> i. i \<in> I \<Longrightarrow> ofilter(A i)) \<Longrightarrow> ofilter (\<Union> i \<in> I. A i)"
unfolding ofilter_def by blast
-
lemma ofilter_under_UNION:
assumes "ofilter A"
shows "A = (\<Union> a \<in> A. under a)"
@@ -542,10 +496,8 @@
thus "A \<le> (\<Union> a \<in> A. under a)" by blast
qed
-
subsubsection{* Other properties *}
-
lemma ofilter_linord:
assumes OF1: "ofilter A" and OF2: "ofilter B"
shows "A \<le> B \<or> B \<le> A"
@@ -587,7 +539,6 @@
qed
qed
-
lemma ofilter_AboveS_Field:
assumes "ofilter A"
shows "A \<union> (AboveS A) = Field r"
@@ -614,7 +565,6 @@
thus "Field r \<le> A \<union> (AboveS A)" by blast
qed
-
lemma suc_ofilter_in:
assumes OF: "ofilter A" and ABOVE_NE: "AboveS A \<noteq> {}" and
REL: "(b,suc A) \<in> r" and DIFF: "b \<noteq> suc A"
@@ -633,10 +583,6 @@
thus ?thesis by blast
qed
-
-
end (* context wo_rel *)
-
-
end