author  blanchet 
Fri, 17 Jan 2014 10:02:49 +0100  
changeset 55026  258fa7b5a621 
parent 54552  5d57cbec0f0f 
child 55027  a74ea6d75571 
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 

6 
header {* Orders as Relations *} 

7 

8 
theory Order_Relation 

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

9 
imports Wellfounded 
26273  10 
begin 
11 

26295  12 
subsection{* Orders on a set *} 
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 

59 
subsection{* Orders on the field *} 

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 

118 
subsection{* Orders on a type *} 

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 

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

127 
subsection {* Orderlike relations *} 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

128 

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

129 
text{* In this subsection, we develop basic concepts and results pertaining 
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 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

131 
total relations. We also further define upper and lower bounds operators. *} 
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 

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

134 
subsubsection {* Auxiliaries *} 
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 

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

180 
subsubsection {* The upper and lower bounds operators *} 
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 
text{* Here we define upper (``above") and lower (``below") bounds operators. 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

183 
We think of @{text "r"} as a {\em nonstrict} relation. The suffix ``S" 
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., 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

185 
@{text "underS a"} is the set of all strict lower bounds of @{text "a"} (w.r.t. @{text "r"}). 
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 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

187 
than on individual elements. *} 
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 

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

213 
text{* Note: In the definitions of @{text "Above[S]"} and @{text "Under[S]"}, 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

214 
we bounded comprehension by @{text "Field r"} in order to properly cover 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

215 
the case of @{text "A"} being empty. *} 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

216 

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

217 
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

218 
by(auto simp add: underS_def under_def) 
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_notIn: "a \<notin> underS r a" 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

221 
by(simp add: underS_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 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

224 
by(simp add: refl_on_def under_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 AboveS_disjoint: "A Int (AboveS r A) = {}" 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

227 
by(auto simp add: AboveS_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 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

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

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

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

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

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

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

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

245 
by(unfold underS_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_Field2: 
258fa7b5a621
folded 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54552
diff
changeset

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

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

250 

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

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

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

253 
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

254 

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

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

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

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

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

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

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

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

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

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

266 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

280 

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

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

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

283 
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

284 
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

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

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

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

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

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

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

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

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

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

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

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

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

297 
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

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

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

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

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

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

303 
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

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

305 

26273  306 
end 