Up to index of Isabelle/HOL/Free-Groups
theory Wellorder_Relation_Base(* Title: HOL/Cardinals/Wellorder_Relation_Base.thy
Author: Andrei Popescu, TU Muenchen
Copyright 2012
Well-order relations (base).
*)
header {* Well-Order Relations (Base) *}
theory Wellorder_Relation_Base
imports Wellfounded_More_Base
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 = 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 *)
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 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)"
definition ofilter :: "'a set => bool"
where
"ofilter A ≡ (A ≤ Field r) ∧ (∀a ∈ A. under a ≤ 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 WF wf_eq_minimal[of "r - Id"] NE Id_def obtain b where
*: "b ∈ B ∧ (∀b'. b' ≠ b ∧ (b',b) ∈ r --> b' ∉ B)" by force
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 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 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 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 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 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 by auto
moreover
have "a ∈ AboveS (underS a)"
using in_AboveS_underS IN by auto
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 auto
{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 blast
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[of A] 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 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_Under:
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 assms by auto
next
fix a x
assume "a ∈ Under A" and "x ∈ under a"
thus "x ∈ Under A"
using TRANS under_Under_trans by auto
qed
lemma ofilter_UnderS:
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 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 by auto
qed
lemma ofilter_Int: "[|ofilter A; ofilter B|] ==> ofilter(A Int B)"
unfolding ofilter_def by blast
lemma ofilter_Un: "[|ofilter A; ofilter B|] ==> ofilter(A ∪ B)"
unfolding ofilter_def by blast
lemma ofilter_UNION:
"(!! i. i ∈ I ==> ofilter(A i)) ==> ofilter (\<Union> i ∈ I. A i)"
unfolding ofilter_def by blast
lemma ofilter_under_UNION:
assumes "ofilter A"
shows "A = (\<Union> a ∈ A. under a)"
proof
have "∀a ∈ A. under a ≤ A"
using assms ofilter_def by auto
thus "(\<Union> a ∈ A. under a) ≤ A" by blast
next
have "∀a ∈ A. a ∈ under a"
using REFL Refl_under_in assms ofilter_def by blast
thus "A ≤ (\<Union> 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 TRANS ANTISYM 1 2
have "A ≤ B" by auto
hence ?thesis by auto
}
moreover
{assume "(b,a) ∈ r"
with underS_incr 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 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 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 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