author  Andreas Lochbihler 
Fri, 29 Jul 2016 09:49:23 +0200  
changeset 63561  fba08009ff3e 
parent 61799  4cf66f21b764 
child 63563  0bcd79da075b 
permissions  rwrr 
54552
5d57cbec0f0f
moving 'Order_Relation' to 'HOL' (since it's a BNF dependency)
blanchet
parents:
54551
diff
changeset

1 
(* Title: HOL/Order_Relation.thy 
5d57cbec0f0f
moving 'Order_Relation' to 'HOL' (since it's a BNF dependency)
blanchet
parents:
54551
diff
changeset

2 
Author: Tobias Nipkow 
55026
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

3 
Author: Andrei Popescu, TU Muenchen 
54552
5d57cbec0f0f
moving 'Order_Relation' to 'HOL' (since it's a BNF dependency)
blanchet
parents:
54551
diff
changeset

4 
*) 
26273  5 

60758  6 
section \<open>Orders as Relations\<close> 
26273  7 

8 
theory Order_Relation 

55027  9 
imports Wfrec 
26273  10 
begin 
11 

60758  12 
subsection\<open>Orders on a set\<close> 
26295  13 

30198  14 
definition "preorder_on A r \<equiv> refl_on A r \<and> trans r" 
26295  15 

16 
definition "partial_order_on A r \<equiv> preorder_on A r \<and> antisym r" 

26273  17 

26295  18 
definition "linear_order_on A r \<equiv> partial_order_on A r \<and> total_on A r" 
19 

20 
definition "strict_linear_order_on A r \<equiv> trans r \<and> irrefl r \<and> total_on A r" 

21 

22 
definition "well_order_on A r \<equiv> linear_order_on A r \<and> wf(r  Id)" 

26273  23 

26295  24 
lemmas order_on_defs = 
25 
preorder_on_def partial_order_on_def linear_order_on_def 

26 
strict_linear_order_on_def well_order_on_def 

27 

26273  28 

26295  29 
lemma preorder_on_empty[simp]: "preorder_on {} {}" 
30 
by(simp add:preorder_on_def trans_def) 

31 

32 
lemma partial_order_on_empty[simp]: "partial_order_on {} {}" 

33 
by(simp add:partial_order_on_def) 

26273  34 

26295  35 
lemma lnear_order_on_empty[simp]: "linear_order_on {} {}" 
36 
by(simp add:linear_order_on_def) 

37 

38 
lemma well_order_on_empty[simp]: "well_order_on {} {}" 

39 
by(simp add:well_order_on_def) 

40 

26273  41 

26295  42 
lemma preorder_on_converse[simp]: "preorder_on A (r^1) = preorder_on A r" 
43 
by (simp add:preorder_on_def) 

44 

45 
lemma partial_order_on_converse[simp]: 

46 
"partial_order_on A (r^1) = partial_order_on A r" 

47 
by (simp add: partial_order_on_def) 

26273  48 

26295  49 
lemma linear_order_on_converse[simp]: 
50 
"linear_order_on A (r^1) = linear_order_on A r" 

51 
by (simp add: linear_order_on_def) 

52 

26273  53 

26295  54 
lemma strict_linear_order_on_diff_Id: 
55 
"linear_order_on A r \<Longrightarrow> strict_linear_order_on A (rId)" 

56 
by(simp add: order_on_defs trans_diff_Id) 

57 

63561
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
61799
diff
changeset

58 
lemma linear_order_on_singleton [iff]: "linear_order_on {x} {(x, x)}" 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
61799
diff
changeset

59 
unfolding order_on_defs by simp 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
61799
diff
changeset

60 

fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
61799
diff
changeset

61 
lemma linear_order_on_acyclic: 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
61799
diff
changeset

62 
assumes "linear_order_on A r" 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
61799
diff
changeset

63 
shows "acyclic (r  Id)" 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
61799
diff
changeset

64 
using strict_linear_order_on_diff_Id[OF assms] 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
61799
diff
changeset

65 
by(auto simp add: acyclic_irrefl strict_linear_order_on_def) 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
61799
diff
changeset

66 

fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
61799
diff
changeset

67 
lemma linear_order_on_well_order_on: 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
61799
diff
changeset

68 
assumes "finite r" 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
61799
diff
changeset

69 
shows "linear_order_on A r \<longleftrightarrow> well_order_on A r" 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
61799
diff
changeset

70 
unfolding well_order_on_def 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
61799
diff
changeset

71 
using assms finite_acyclic_wf[OF _ linear_order_on_acyclic, of r] by blast 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
61799
diff
changeset

72 

26295  73 

60758  74 
subsection\<open>Orders on the field\<close> 
26273  75 

30198  76 
abbreviation "Refl r \<equiv> refl_on (Field r) r" 
26295  77 

78 
abbreviation "Preorder r \<equiv> preorder_on (Field r) r" 

79 

80 
abbreviation "Partial_order r \<equiv> partial_order_on (Field r) r" 

26273  81 

26295  82 
abbreviation "Total r \<equiv> total_on (Field r) r" 
83 

84 
abbreviation "Linear_order r \<equiv> linear_order_on (Field r) r" 

85 

86 
abbreviation "Well_order r \<equiv> well_order_on (Field r) r" 

87 

26273  88 

89 
lemma subset_Image_Image_iff: 

90 
"\<lbrakk> Preorder r; A \<subseteq> Field r; B \<subseteq> Field r\<rbrakk> \<Longrightarrow> 

91 
r `` A \<subseteq> r `` B \<longleftrightarrow> (\<forall>a\<in>A.\<exists>b\<in>B. (b,a):r)" 

48750  92 
unfolding preorder_on_def refl_on_def Image_def 
93 
apply (simp add: subset_eq) 

94 
unfolding trans_def by fast 

26273  95 

96 
lemma subset_Image1_Image1_iff: 

97 
"\<lbrakk> Preorder r; a : Field r; b : Field r\<rbrakk> \<Longrightarrow> r `` {a} \<subseteq> r `` {b} \<longleftrightarrow> (b,a):r" 

98 
by(simp add:subset_Image_Image_iff) 

99 

100 
lemma Refl_antisym_eq_Image1_Image1_iff: 

54552
5d57cbec0f0f
moving 'Order_Relation' to 'HOL' (since it's a BNF dependency)
blanchet
parents:
54551
diff
changeset

101 
assumes r: "Refl r" and as: "antisym r" and abf: "a \<in> Field r" "b \<in> Field r" 
5d57cbec0f0f
moving 'Order_Relation' to 'HOL' (since it's a BNF dependency)
blanchet
parents:
54551
diff
changeset

102 
shows "r `` {a} = r `` {b} \<longleftrightarrow> a = b" 
5d57cbec0f0f
moving 'Order_Relation' to 'HOL' (since it's a BNF dependency)
blanchet
parents:
54551
diff
changeset

103 
proof 
5d57cbec0f0f
moving 'Order_Relation' to 'HOL' (since it's a BNF dependency)
blanchet
parents:
54551
diff
changeset

104 
assume "r `` {a} = r `` {b}" 
5d57cbec0f0f
moving 'Order_Relation' to 'HOL' (since it's a BNF dependency)
blanchet
parents:
54551
diff
changeset

105 
hence e: "\<And>x. (a, x) \<in> r \<longleftrightarrow> (b, x) \<in> r" by (simp add: set_eq_iff) 
5d57cbec0f0f
moving 'Order_Relation' to 'HOL' (since it's a BNF dependency)
blanchet
parents:
54551
diff
changeset

106 
have "(a, a) \<in> r" "(b, b) \<in> r" using r abf by (simp_all add: refl_on_def) 
5d57cbec0f0f
moving 'Order_Relation' to 'HOL' (since it's a BNF dependency)
blanchet
parents:
54551
diff
changeset

107 
hence "(a, b) \<in> r" "(b, a) \<in> r" using e[of a] e[of b] by simp_all 
5d57cbec0f0f
moving 'Order_Relation' to 'HOL' (since it's a BNF dependency)
blanchet
parents:
54551
diff
changeset

108 
thus "a = b" using as[unfolded antisym_def] by blast 
5d57cbec0f0f
moving 'Order_Relation' to 'HOL' (since it's a BNF dependency)
blanchet
parents:
54551
diff
changeset

109 
qed fast 
26273  110 

111 
lemma Partial_order_eq_Image1_Image1_iff: 

112 
"\<lbrakk>Partial_order r; a:Field r; b:Field r\<rbrakk> \<Longrightarrow> r `` {a} = r `` {b} \<longleftrightarrow> a=b" 

26295  113 
by(auto simp:order_on_defs Refl_antisym_eq_Image1_Image1_iff) 
114 

52182  115 
lemma Total_Id_Field: 
116 
assumes TOT: "Total r" and NID: "\<not> (r <= Id)" 

117 
shows "Field r = Field(r  Id)" 

118 
using mono_Field[of "r  Id" r] Diff_subset[of r Id] 

119 
proof(auto) 

120 
have "r \<noteq> {}" using NID by fast 

54482  121 
then obtain b and c where "b \<noteq> c \<and> (b,c) \<in> r" using NID by auto 
52182  122 
hence 1: "b \<noteq> c \<and> {b,c} \<le> Field r" by (auto simp: Field_def) 
54552
5d57cbec0f0f
moving 'Order_Relation' to 'HOL' (since it's a BNF dependency)
blanchet
parents:
54551
diff
changeset

123 

52182  124 
fix a assume *: "a \<in> Field r" 
125 
obtain d where 2: "d \<in> Field r" and 3: "d \<noteq> a" 

126 
using * 1 by auto 

127 
hence "(a,d) \<in> r \<or> (d,a) \<in> r" using * TOT 

128 
by (simp add: total_on_def) 

129 
thus "a \<in> Field(r  Id)" using 3 unfolding Field_def by blast 

130 
qed 

131 

26295  132 

60758  133 
subsection\<open>Orders on a type\<close> 
26295  134 

135 
abbreviation "strict_linear_order \<equiv> strict_linear_order_on UNIV" 

136 

137 
abbreviation "linear_order \<equiv> linear_order_on UNIV" 

138 

54551  139 
abbreviation "well_order \<equiv> well_order_on UNIV" 
26273  140 

55026
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

141 

60758  142 
subsection \<open>Orderlike relations\<close> 
55026
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

143 

60758  144 
text\<open>In this subsection, we develop basic concepts and results pertaining 
55026
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

145 
to orderlike relations, i.e., to reflexive and/or transitive and/or symmetric and/or 
60758  146 
total relations. We also further define upper and lower bounds operators.\<close> 
55026
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

147 

258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

148 

60758  149 
subsubsection \<open>Auxiliaries\<close> 
55026
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

150 

258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

151 
lemma refl_on_domain: 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

152 
"\<lbrakk>refl_on A r; (a,b) : r\<rbrakk> \<Longrightarrow> a \<in> A \<and> b \<in> A" 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

153 
by(auto simp add: refl_on_def) 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

154 

258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

155 
corollary well_order_on_domain: 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

156 
"\<lbrakk>well_order_on A r; (a,b) \<in> r\<rbrakk> \<Longrightarrow> a \<in> A \<and> b \<in> A" 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

157 
by (auto simp add: refl_on_domain order_on_defs) 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

158 

258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

159 
lemma well_order_on_Field: 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

160 
"well_order_on A r \<Longrightarrow> A = Field r" 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

161 
by(auto simp add: refl_on_def Field_def order_on_defs) 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

162 

258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

163 
lemma well_order_on_Well_order: 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

164 
"well_order_on A r \<Longrightarrow> A = Field r \<and> Well_order r" 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

165 
using well_order_on_Field by auto 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

166 

258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

167 
lemma Total_subset_Id: 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

168 
assumes TOT: "Total r" and SUB: "r \<le> Id" 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

169 
shows "r = {} \<or> (\<exists>a. r = {(a,a)})" 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

170 
proof 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

171 
{assume "r \<noteq> {}" 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

172 
then obtain a b where 1: "(a,b) \<in> r" by fast 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

173 
hence "a = b" using SUB by blast 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

174 
hence 2: "(a,a) \<in> r" using 1 by simp 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

175 
{fix c d assume "(c,d) \<in> r" 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

176 
hence "{a,c,d} \<le> Field r" using 1 unfolding Field_def by blast 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

177 
hence "((a,c) \<in> r \<or> (c,a) \<in> r \<or> a = c) \<and> 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

178 
((a,d) \<in> r \<or> (d,a) \<in> r \<or> a = d)" 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

179 
using TOT unfolding total_on_def by blast 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

180 
hence "a = c \<and> a = d" using SUB by blast 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

181 
} 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

182 
hence "r \<le> {(a,a)}" by auto 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

183 
with 2 have "\<exists>a. r = {(a,a)}" by blast 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

184 
} 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

185 
thus ?thesis by blast 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

186 
qed 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

187 

258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

188 
lemma Linear_order_in_diff_Id: 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

189 
assumes LI: "Linear_order r" and 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

190 
IN1: "a \<in> Field r" and IN2: "b \<in> Field r" 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

191 
shows "((a,b) \<in> r) = ((b,a) \<notin> r  Id)" 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

192 
using assms unfolding order_on_defs total_on_def antisym_def Id_def refl_on_def by force 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

193 

258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

194 

60758  195 
subsubsection \<open>The upper and lower bounds operators\<close> 
55026
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

196 

60758  197 
text\<open>Here we define upper (``above") and lower (``below") bounds operators. 
61799  198 
We think of \<open>r\<close> as a {\em nonstrict} relation. The suffix ``S" 
55026
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

199 
at the names of some operators indicates that the bounds are strict  e.g., 
61799  200 
\<open>underS a\<close> is the set of all strict lower bounds of \<open>a\<close> (w.r.t. \<open>r\<close>). 
55026
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

201 
Capitalization of the first letter in the name reminds that the operator acts on sets, rather 
60758  202 
than on individual elements.\<close> 
55026
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

203 

258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

204 
definition under::"'a rel \<Rightarrow> 'a \<Rightarrow> 'a set" 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

205 
where "under r a \<equiv> {b. (b,a) \<in> r}" 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

206 

258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

207 
definition underS::"'a rel \<Rightarrow> 'a \<Rightarrow> 'a set" 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

208 
where "underS r a \<equiv> {b. b \<noteq> a \<and> (b,a) \<in> r}" 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

209 

258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

210 
definition Under::"'a rel \<Rightarrow> 'a set \<Rightarrow> 'a set" 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

211 
where "Under r A \<equiv> {b \<in> Field r. \<forall>a \<in> A. (b,a) \<in> r}" 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

212 

258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

213 
definition UnderS::"'a rel \<Rightarrow> 'a set \<Rightarrow> 'a set" 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

214 
where "UnderS r A \<equiv> {b \<in> Field r. \<forall>a \<in> A. b \<noteq> a \<and> (b,a) \<in> r}" 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

215 

258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

216 
definition above::"'a rel \<Rightarrow> 'a \<Rightarrow> 'a set" 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

217 
where "above r a \<equiv> {b. (a,b) \<in> r}" 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

218 

258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

219 
definition aboveS::"'a rel \<Rightarrow> 'a \<Rightarrow> 'a set" 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

220 
where "aboveS r a \<equiv> {b. b \<noteq> a \<and> (a,b) \<in> r}" 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

221 

258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

222 
definition Above::"'a rel \<Rightarrow> 'a set \<Rightarrow> 'a set" 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

223 
where "Above r A \<equiv> {b \<in> Field r. \<forall>a \<in> A. (a,b) \<in> r}" 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

224 

258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

225 
definition AboveS::"'a rel \<Rightarrow> 'a set \<Rightarrow> 'a set" 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

226 
where "AboveS r A \<equiv> {b \<in> Field r. \<forall>a \<in> A. b \<noteq> a \<and> (a,b) \<in> r}" 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

227 

55173  228 
definition ofilter :: "'a rel \<Rightarrow> 'a set \<Rightarrow> bool" 
229 
where "ofilter r A \<equiv> (A \<le> Field r) \<and> (\<forall>a \<in> A. under r a \<le> A)" 

230 

61799  231 
text\<open>Note: In the definitions of \<open>Above[S]\<close> and \<open>Under[S]\<close>, 
232 
we bounded comprehension by \<open>Field r\<close> in order to properly cover 

233 
the case of \<open>A\<close> being empty.\<close> 

55026
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

234 

258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

235 
lemma underS_subset_under: "underS r a \<le> under r a" 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

236 
by(auto simp add: underS_def under_def) 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

237 

258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

238 
lemma underS_notIn: "a \<notin> underS r a" 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

239 
by(simp add: underS_def) 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

240 

258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

241 
lemma Refl_under_in: "\<lbrakk>Refl r; a \<in> Field r\<rbrakk> \<Longrightarrow> a \<in> under r a" 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

242 
by(simp add: refl_on_def under_def) 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

243 

258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

244 
lemma AboveS_disjoint: "A Int (AboveS r A) = {}" 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

245 
by(auto simp add: AboveS_def) 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

246 

258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

247 
lemma in_AboveS_underS: "a \<in> Field r \<Longrightarrow> a \<in> AboveS r (underS r a)" 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

248 
by(auto simp add: AboveS_def underS_def) 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

249 

258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

250 
lemma Refl_under_underS: 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

251 
assumes "Refl r" "a \<in> Field r" 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

252 
shows "under r a = underS r a \<union> {a}" 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

253 
unfolding under_def underS_def 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

254 
using assms refl_on_def[of _ r] by fastforce 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

255 

258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

256 
lemma underS_empty: "a \<notin> Field r \<Longrightarrow> underS r a = {}" 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

257 
by (auto simp: Field_def underS_def) 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

258 

258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

259 
lemma under_Field: "under r a \<le> Field r" 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

260 
by(unfold under_def Field_def, auto) 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

261 

258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

262 
lemma underS_Field: "underS r a \<le> Field r" 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

263 
by(unfold underS_def Field_def, auto) 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

264 

258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

265 
lemma underS_Field2: 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

266 
"a \<in> Field r \<Longrightarrow> underS r a < Field r" 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

267 
using underS_notIn underS_Field by fast 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

268 

258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

269 
lemma underS_Field3: 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

270 
"Field r \<noteq> {} \<Longrightarrow> underS r a < Field r" 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

271 
by(cases "a \<in> Field r", simp add: underS_Field2, auto simp add: underS_empty) 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

272 

258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

273 
lemma AboveS_Field: "AboveS r A \<le> Field r" 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

274 
by(unfold AboveS_def Field_def, auto) 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

275 

258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

276 
lemma under_incr: 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

277 
assumes TRANS: "trans r" and REL: "(a,b) \<in> r" 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

278 
shows "under r a \<le> under r b" 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

279 
proof(unfold under_def, auto) 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

280 
fix x assume "(x,a) \<in> r" 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

281 
with REL TRANS trans_def[of r] 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

282 
show "(x,b) \<in> r" by blast 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

283 
qed 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

284 

258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

285 
lemma underS_incr: 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

286 
assumes TRANS: "trans r" and ANTISYM: "antisym r" and 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

287 
REL: "(a,b) \<in> r" 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

288 
shows "underS r a \<le> underS r b" 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

289 
proof(unfold underS_def, auto) 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

290 
assume *: "b \<noteq> a" and **: "(b,a) \<in> r" 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

291 
with ANTISYM antisym_def[of r] REL 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

292 
show False by blast 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

293 
next 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

294 
fix x assume "x \<noteq> a" "(x,a) \<in> r" 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

295 
with REL TRANS trans_def[of r] 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

296 
show "(x,b) \<in> r" by blast 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

297 
qed 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

298 

258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

299 
lemma underS_incl_iff: 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

300 
assumes LO: "Linear_order r" and 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

301 
INa: "a \<in> Field r" and INb: "b \<in> Field r" 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

302 
shows "(underS r a \<le> underS r b) = ((a,b) \<in> r)" 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

303 
proof 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

304 
assume "(a,b) \<in> r" 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

305 
thus "underS r a \<le> underS r b" using LO 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

306 
by (simp add: order_on_defs underS_incr) 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

307 
next 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

308 
assume *: "underS r a \<le> underS r b" 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

309 
{assume "a = b" 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

310 
hence "(a,b) \<in> r" using assms 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

311 
by (simp add: order_on_defs refl_on_def) 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

312 
} 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

313 
moreover 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

314 
{assume "a \<noteq> b \<and> (b,a) \<in> r" 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

315 
hence "b \<in> underS r a" unfolding underS_def by blast 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

316 
hence "b \<in> underS r b" using * by blast 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

317 
hence False by (simp add: underS_notIn) 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

318 
} 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

319 
ultimately 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

320 
show "(a,b) \<in> r" using assms 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

321 
order_on_defs[of "Field r" r] total_on_def[of "Field r" r] by blast 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

322 
qed 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

323 

63561
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
61799
diff
changeset

324 
lemma finite_Linear_order_induct[consumes 3, case_names step]: 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
61799
diff
changeset

325 
assumes "Linear_order r" 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
61799
diff
changeset

326 
and "x \<in> Field r" 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
61799
diff
changeset

327 
and "finite r" 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
61799
diff
changeset

328 
and step: "\<And>x. \<lbrakk>x \<in> Field r; \<And>y. y \<in> aboveS r x \<Longrightarrow> P y\<rbrakk> \<Longrightarrow> P x" 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
61799
diff
changeset

329 
shows "P x" 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
61799
diff
changeset

330 
using assms(2) 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
61799
diff
changeset

331 
proof(induct rule: wf_induct[of "r\<inverse>  Id"]) 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
61799
diff
changeset

332 
from assms(1,3) show "wf (r\<inverse>  Id)" 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
61799
diff
changeset

333 
using linear_order_on_well_order_on linear_order_on_converse 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
61799
diff
changeset

334 
unfolding well_order_on_def by blast 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
61799
diff
changeset

335 
next 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
61799
diff
changeset

336 
case (2 x) then show ?case 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
61799
diff
changeset

337 
by  (rule step; auto simp: aboveS_def intro: FieldI2) 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
61799
diff
changeset

338 
qed 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
61799
diff
changeset

339 

55027  340 

60758  341 
subsection \<open>Variations on WellFounded Relations\<close> 
55027  342 

60758  343 
text \<open> 
55027  344 
This subsection contains some variations of the results from @{theory Wellfounded}: 
345 
\begin{itemize} 

346 
\item means for slightly more direct definitions by wellfounded recursion; 

347 
\item variations of wellfounded induction; 

348 
\item means for proving a linear order to be a wellorder. 

349 
\end{itemize} 

60758  350 
\<close> 
55027  351 

352 

60758  353 
subsubsection \<open>Characterizations of wellfoundedness\<close> 
55027  354 

60758  355 
text \<open>A transitive relation is wellfounded iff it is ``locally'' wellfounded, 
356 
i.e., iff its restriction to the lower bounds of of any element is wellfounded.\<close> 

55027  357 

358 
lemma trans_wf_iff: 

359 
assumes "trans r" 

360 
shows "wf r = (\<forall>a. wf(r Int (r^1``{a} \<times> r^1``{a})))" 

361 
proof 

362 
obtain R where R_def: "R = (\<lambda> a. r Int (r^1``{a} \<times> r^1``{a}))" by blast 

363 
{assume *: "wf r" 

364 
{fix a 

365 
have "wf(R a)" 

366 
using * R_def wf_subset[of r "R a"] by auto 

367 
} 

368 
} 

369 
(* *) 

370 
moreover 

371 
{assume *: "\<forall>a. wf(R a)" 

372 
have "wf r" 

373 
proof(unfold wf_def, clarify) 

374 
fix phi a 

375 
assume **: "\<forall>a. (\<forall>b. (b,a) \<in> r \<longrightarrow> phi b) \<longrightarrow> phi a" 

376 
obtain chi where chi_def: "chi = (\<lambda>b. (b,a) \<in> r \<longrightarrow> phi b)" by blast 

377 
with * have "wf (R a)" by auto 

378 
hence "(\<forall>b. (\<forall>c. (c,b) \<in> R a \<longrightarrow> chi c) \<longrightarrow> chi b) \<longrightarrow> (\<forall>b. chi b)" 

379 
unfolding wf_def by blast 

380 
moreover 

381 
have "\<forall>b. (\<forall>c. (c,b) \<in> R a \<longrightarrow> chi c) \<longrightarrow> chi b" 

382 
proof(auto simp add: chi_def R_def) 

383 
fix b 

384 
assume 1: "(b,a) \<in> r" and 2: "\<forall>c. (c, b) \<in> r \<and> (c, a) \<in> r \<longrightarrow> phi c" 

385 
hence "\<forall>c. (c, b) \<in> r \<longrightarrow> phi c" 

386 
using assms trans_def[of r] by blast 

387 
thus "phi b" using ** by blast 

388 
qed 

389 
ultimately have "\<forall>b. chi b" by (rule mp) 

390 
with ** chi_def show "phi a" by blast 

391 
qed 

392 
} 

393 
ultimately show ?thesis using R_def by blast 

394 
qed 

395 

61799  396 
text \<open>The next lemma is a variation of \<open>wf_eq_minimal\<close> from Wellfounded, 
60758  397 
allowing one to assume the set included in the field.\<close> 
55027  398 

399 
lemma wf_eq_minimal2: 

400 
"wf r = (\<forall>A. A <= Field r \<and> A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. \<not> (a',a) \<in> r))" 

401 
proof 

402 
let ?phi = "\<lambda> A. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. \<not> (a',a) \<in> r)" 

403 
have "wf r = (\<forall>A. ?phi A)" 

404 
by (auto simp: ex_in_conv [THEN sym], erule wfE_min, assumption, blast) 

405 
(rule wfI_min, fast) 

406 
(* *) 

407 
also have "(\<forall>A. ?phi A) = (\<forall>B \<le> Field r. ?phi B)" 

408 
proof 

409 
assume "\<forall>A. ?phi A" 

410 
thus "\<forall>B \<le> Field r. ?phi B" by simp 

411 
next 

412 
assume *: "\<forall>B \<le> Field r. ?phi B" 

413 
show "\<forall>A. ?phi A" 

414 
proof(clarify) 

415 
fix A::"'a set" assume **: "A \<noteq> {}" 

416 
obtain B where B_def: "B = A Int (Field r)" by blast 

417 
show "\<exists>a \<in> A. \<forall>a' \<in> A. (a',a) \<notin> r" 

418 
proof(cases "B = {}") 

419 
assume Case1: "B = {}" 

420 
obtain a where 1: "a \<in> A \<and> a \<notin> Field r" 

421 
using ** Case1 unfolding B_def by blast 

422 
hence "\<forall>a' \<in> A. (a',a) \<notin> r" using 1 unfolding Field_def by blast 

423 
thus ?thesis using 1 by blast 

424 
next 

425 
assume Case2: "B \<noteq> {}" have 1: "B \<le> Field r" unfolding B_def by blast 

426 
obtain a where 2: "a \<in> B \<and> (\<forall>a' \<in> B. (a',a) \<notin> r)" 

427 
using Case2 1 * by blast 

428 
have "\<forall>a' \<in> A. (a',a) \<notin> r" 

429 
proof(clarify) 

430 
fix a' assume "a' \<in> A" and **: "(a',a) \<in> r" 

431 
hence "a' \<in> B" unfolding B_def Field_def by blast 

432 
thus False using 2 ** by blast 

433 
qed 

434 
thus ?thesis using 2 unfolding B_def by blast 

435 
qed 

436 
qed 

437 
qed 

438 
finally show ?thesis by blast 

439 
qed 

440 

441 

60758  442 
subsubsection \<open>Characterizations of wellfoundedness\<close> 
55027  443 

60758  444 
text \<open>The next lemma and its corollary enable one to prove that 
55027  445 
a linear order is a wellorder in a way which is more standard than 
60758  446 
via wellfoundedness of the strict version of the relation.\<close> 
55027  447 

448 
lemma Linear_order_wf_diff_Id: 

449 
assumes LI: "Linear_order r" 

450 
shows "wf(r  Id) = (\<forall>A \<le> Field r. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r))" 

451 
proof(cases "r \<le> Id") 

452 
assume Case1: "r \<le> Id" 

453 
hence temp: "r  Id = {}" by blast 

454 
hence "wf(r  Id)" by (simp add: temp) 

455 
moreover 

456 
{fix A assume *: "A \<le> Field r" and **: "A \<noteq> {}" 

457 
obtain a where 1: "r = {} \<or> r = {(a,a)}" using LI 

458 
unfolding order_on_defs using Case1 Total_subset_Id by auto 

459 
hence "A = {a} \<and> r = {(a,a)}" using * ** unfolding Field_def by blast 

460 
hence "\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r" using 1 by blast 

461 
} 

462 
ultimately show ?thesis by blast 

463 
next 

464 
assume Case2: "\<not> r \<le> Id" 

465 
hence 1: "Field r = Field(r  Id)" using Total_Id_Field LI 

466 
unfolding order_on_defs by blast 

467 
show ?thesis 

468 
proof 

469 
assume *: "wf(r  Id)" 

470 
show "\<forall>A \<le> Field r. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r)" 

471 
proof(clarify) 

472 
fix A assume **: "A \<le> Field r" and ***: "A \<noteq> {}" 

473 
hence "\<exists>a \<in> A. \<forall>a' \<in> A. (a',a) \<notin> r  Id" 

474 
using 1 * unfolding wf_eq_minimal2 by simp 

475 
moreover have "\<forall>a \<in> A. \<forall>a' \<in> A. ((a,a') \<in> r) = ((a',a) \<notin> r  Id)" 

476 
using Linear_order_in_diff_Id[of r] ** LI by blast 

477 
ultimately show "\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r" by blast 

478 
qed 

479 
next 

480 
assume *: "\<forall>A \<le> Field r. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r)" 

481 
show "wf(r  Id)" 

482 
proof(unfold wf_eq_minimal2, clarify) 

483 
fix A assume **: "A \<le> Field(r  Id)" and ***: "A \<noteq> {}" 

484 
hence "\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r" 

485 
using 1 * by simp 

486 
moreover have "\<forall>a \<in> A. \<forall>a' \<in> A. ((a,a') \<in> r) = ((a',a) \<notin> r  Id)" 

487 
using Linear_order_in_diff_Id[of r] ** LI mono_Field[of "r  Id" r] by blast 

488 
ultimately show "\<exists>a \<in> A. \<forall>a' \<in> A. (a',a) \<notin> r  Id" by blast 

489 
qed 

490 
qed 

491 
qed 

492 

493 
corollary Linear_order_Well_order_iff: 

494 
assumes "Linear_order r" 

495 
shows "Well_order r = (\<forall>A \<le> Field r. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r))" 

496 
using assms unfolding well_order_on_def using Linear_order_wf_diff_Id[of r] by blast 

497 

26273  498 
end 