author  wenzelm 
Mon, 07 Dec 2015 10:38:04 +0100  
changeset 61799  4cf66f21b764 
parent 60758  d8d85a8172b5 
child 63561  fba08009ff3e 
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 

58 

60758  59 
subsection\<open>Orders on the field\<close> 
26273  60 

30198  61 
abbreviation "Refl r \<equiv> refl_on (Field r) r" 
26295  62 

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

64 

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

26273  66 

26295  67 
abbreviation "Total r \<equiv> total_on (Field r) r" 
68 

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

70 

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

72 

26273  73 

74 
lemma subset_Image_Image_iff: 

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

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

48750  77 
unfolding preorder_on_def refl_on_def Image_def 
78 
apply (simp add: subset_eq) 

79 
unfolding trans_def by fast 

26273  80 

81 
lemma subset_Image1_Image1_iff: 

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

83 
by(simp add:subset_Image_Image_iff) 

84 

85 
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

86 
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

87 
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

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

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

90 
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

91 
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

92 
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

93 
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

94 
qed fast 
26273  95 

96 
lemma Partial_order_eq_Image1_Image1_iff: 

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

26295  98 
by(auto simp:order_on_defs Refl_antisym_eq_Image1_Image1_iff) 
99 

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

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

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

104 
proof(auto) 

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

54482  106 
then obtain b and c where "b \<noteq> c \<and> (b,c) \<in> r" using NID by auto 
52182  107 
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

108 

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

111 
using * 1 by auto 

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

113 
by (simp add: total_on_def) 

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

115 
qed 

116 

26295  117 

60758  118 
subsection\<open>Orders on a type\<close> 
26295  119 

120 
abbreviation "strict_linear_order \<equiv> strict_linear_order_on UNIV" 

121 

122 
abbreviation "linear_order \<equiv> linear_order_on UNIV" 

123 

54551  124 
abbreviation "well_order \<equiv> well_order_on UNIV" 
26273  125 

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

126 

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

128 

60758  129 
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

130 
to orderlike relations, i.e., to reflexive and/or transitive and/or symmetric and/or 
60758  131 
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

132 

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

133 

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

135 

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

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

137 
"\<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

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

139 

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

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

141 
"\<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

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

143 

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

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

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

146 
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

147 

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

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

149 
"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

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

151 

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

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

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

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

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

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

157 
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

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

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

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

161 
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

162 
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

163 
((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

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

165 
hence "a = c \<and> a = d" using SUB by blast 
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 
hence "r \<le> {(a,a)}" by auto 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

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

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

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

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

172 

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

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

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

175 
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

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

177 
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

178 

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

179 

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

181 

60758  182 
text\<open>Here we define upper (``above") and lower (``below") bounds operators. 
61799  183 
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

184 
at the names of some operators indicates that the bounds are strict  e.g., 
61799  185 
\<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

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

188 

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

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

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

191 

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

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

193 
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

194 

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

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

196 
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

197 

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

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

199 
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

200 

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

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

202 
where "above r a \<equiv> {b. (a,b) \<in> r}" 
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 aboveS::"'a rel \<Rightarrow> 'a \<Rightarrow> 'a set" 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

205 
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

206 

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

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

208 
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

209 

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

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

211 
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

212 

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

215 

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

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

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

219 

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

220 
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

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

222 

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

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

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

225 

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

226 
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

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

228 

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

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

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

231 

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

232 
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

233 
by(auto simp add: AboveS_def underS_def) 
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 Refl_under_underS: 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

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

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

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

239 
using assms refl_on_def[of _ r] by fastforce 
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 underS_empty: "a \<notin> Field r \<Longrightarrow> underS r a = {}" 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

242 
by (auto simp: Field_def underS_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 under_Field: "under r a \<le> Field r" 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

245 
by(unfold under_def Field_def, auto) 
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 underS_Field: "underS r a \<le> Field r" 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

248 
by(unfold underS_def Field_def, auto) 
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 underS_Field2: 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

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

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

253 

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

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

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

256 
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

257 

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

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

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

260 

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

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

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

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

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

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

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

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

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

269 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

283 

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

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

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

286 
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

287 
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

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

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

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

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

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

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

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

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

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

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

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

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

300 
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

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

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

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

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

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

306 
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

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

308 

55027  309 

60758  310 
subsection \<open>Variations on WellFounded Relations\<close> 
55027  311 

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

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

316 
\item variations of wellfounded induction; 

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

318 
\end{itemize} 

60758  319 
\<close> 
55027  320 

321 

60758  322 
subsubsection \<open>Characterizations of wellfoundedness\<close> 
55027  323 

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

55027  326 

327 
lemma trans_wf_iff: 

328 
assumes "trans r" 

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

330 
proof 

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

332 
{assume *: "wf r" 

333 
{fix a 

334 
have "wf(R a)" 

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

336 
} 

337 
} 

338 
(* *) 

339 
moreover 

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

341 
have "wf r" 

342 
proof(unfold wf_def, clarify) 

343 
fix phi a 

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

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

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

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

348 
unfolding wf_def by blast 

349 
moreover 

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

351 
proof(auto simp add: chi_def R_def) 

352 
fix b 

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

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

355 
using assms trans_def[of r] by blast 

356 
thus "phi b" using ** by blast 

357 
qed 

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

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

360 
qed 

361 
} 

362 
ultimately show ?thesis using R_def by blast 

363 
qed 

364 

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

368 
lemma wf_eq_minimal2: 

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

370 
proof 

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

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

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

374 
(rule wfI_min, fast) 

375 
(* *) 

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

377 
proof 

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

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

380 
next 

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

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

383 
proof(clarify) 

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

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

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

387 
proof(cases "B = {}") 

388 
assume Case1: "B = {}" 

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

390 
using ** Case1 unfolding B_def by blast 

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

392 
thus ?thesis using 1 by blast 

393 
next 

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

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

396 
using Case2 1 * by blast 

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

398 
proof(clarify) 

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

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

401 
thus False using 2 ** by blast 

402 
qed 

403 
thus ?thesis using 2 unfolding B_def by blast 

404 
qed 

405 
qed 

406 
qed 

407 
finally show ?thesis by blast 

408 
qed 

409 

410 

60758  411 
subsubsection \<open>Characterizations of wellfoundedness\<close> 
55027  412 

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

417 
lemma Linear_order_wf_diff_Id: 

418 
assumes LI: "Linear_order r" 

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

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

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

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

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

424 
moreover 

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

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

427 
unfolding order_on_defs using Case1 Total_subset_Id by auto 

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

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

430 
} 

431 
ultimately show ?thesis by blast 

432 
next 

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

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

435 
unfolding order_on_defs by blast 

436 
show ?thesis 

437 
proof 

438 
assume *: "wf(r  Id)" 

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

440 
proof(clarify) 

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

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

443 
using 1 * unfolding wf_eq_minimal2 by simp 

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

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

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

447 
qed 

448 
next 

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

450 
show "wf(r  Id)" 

451 
proof(unfold wf_eq_minimal2, clarify) 

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

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

454 
using 1 * by simp 

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

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

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

458 
qed 

459 
qed 

460 
qed 

461 

462 
corollary Linear_order_Well_order_iff: 

463 
assumes "Linear_order r" 

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

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

466 

26273  467 
end 