|
365
|
1 |
|
|
|
2 |
theory Positions
|
|
|
3 |
imports "Spec" "Lexer"
|
|
|
4 |
begin
|
|
|
5 |
|
|
|
6 |
chapter \<open>An alternative definition for POSIX values\<close>
|
|
|
7 |
|
|
|
8 |
section \<open>Positions in Values\<close>
|
|
|
9 |
|
|
|
10 |
fun
|
|
|
11 |
at :: "val \<Rightarrow> nat list \<Rightarrow> val"
|
|
|
12 |
where
|
|
|
13 |
"at v [] = v"
|
|
|
14 |
| "at (Left v) (0#ps)= at v ps"
|
|
|
15 |
| "at (Right v) (Suc 0#ps)= at v ps"
|
|
|
16 |
| "at (Seq v1 v2) (0#ps)= at v1 ps"
|
|
|
17 |
| "at (Seq v1 v2) (Suc 0#ps)= at v2 ps"
|
|
|
18 |
| "at (Stars vs) (n#ps)= at (nth vs n) ps"
|
|
|
19 |
|
|
|
20 |
|
|
|
21 |
|
|
|
22 |
fun Pos :: "val \<Rightarrow> (nat list) set"
|
|
|
23 |
where
|
|
|
24 |
"Pos (Void) = {[]}"
|
|
|
25 |
| "Pos (Char c) = {[]}"
|
|
|
26 |
| "Pos (Left v) = {[]} \<union> {0#ps | ps. ps \<in> Pos v}"
|
|
|
27 |
| "Pos (Right v) = {[]} \<union> {1#ps | ps. ps \<in> Pos v}"
|
|
|
28 |
| "Pos (Seq v1 v2) = {[]} \<union> {0#ps | ps. ps \<in> Pos v1} \<union> {1#ps | ps. ps \<in> Pos v2}"
|
|
|
29 |
| "Pos (Stars []) = {[]}"
|
|
|
30 |
| "Pos (Stars (v#vs)) = {[]} \<union> {0#ps | ps. ps \<in> Pos v} \<union> {Suc n#ps | n ps. n#ps \<in> Pos (Stars vs)}"
|
|
|
31 |
|
|
|
32 |
|
|
|
33 |
lemma Pos_stars:
|
|
|
34 |
"Pos (Stars vs) = {[]} \<union> (\<Union>n < length vs. {n#ps | ps. ps \<in> Pos (vs ! n)})"
|
|
|
35 |
apply(induct vs)
|
|
|
36 |
apply(auto simp add: insert_ident less_Suc_eq_0_disj)
|
|
|
37 |
done
|
|
|
38 |
|
|
|
39 |
lemma Pos_empty:
|
|
|
40 |
shows "[] \<in> Pos v"
|
|
|
41 |
by (induct v rule: Pos.induct)(auto)
|
|
|
42 |
|
|
|
43 |
|
|
|
44 |
abbreviation
|
|
|
45 |
"intlen vs \<equiv> int (length vs)"
|
|
|
46 |
|
|
|
47 |
|
|
|
48 |
definition pflat_len :: "val \<Rightarrow> nat list => int"
|
|
|
49 |
where
|
|
|
50 |
"pflat_len v p \<equiv> (if p \<in> Pos v then intlen (flat (at v p)) else -1)"
|
|
|
51 |
|
|
|
52 |
lemma pflat_len_simps:
|
|
|
53 |
shows "pflat_len (Seq v1 v2) (0#p) = pflat_len v1 p"
|
|
|
54 |
and "pflat_len (Seq v1 v2) (Suc 0#p) = pflat_len v2 p"
|
|
|
55 |
and "pflat_len (Left v) (0#p) = pflat_len v p"
|
|
|
56 |
and "pflat_len (Left v) (Suc 0#p) = -1"
|
|
|
57 |
and "pflat_len (Right v) (Suc 0#p) = pflat_len v p"
|
|
|
58 |
and "pflat_len (Right v) (0#p) = -1"
|
|
|
59 |
and "pflat_len (Stars (v#vs)) (Suc n#p) = pflat_len (Stars vs) (n#p)"
|
|
|
60 |
and "pflat_len (Stars (v#vs)) (0#p) = pflat_len v p"
|
|
|
61 |
and "pflat_len v [] = intlen (flat v)"
|
|
|
62 |
by (auto simp add: pflat_len_def Pos_empty)
|
|
|
63 |
|
|
|
64 |
lemma pflat_len_Stars_simps:
|
|
|
65 |
assumes "n < length vs"
|
|
|
66 |
shows "pflat_len (Stars vs) (n#p) = pflat_len (vs!n) p"
|
|
|
67 |
using assms
|
|
|
68 |
apply(induct vs arbitrary: n p)
|
|
|
69 |
apply(auto simp add: less_Suc_eq_0_disj pflat_len_simps)
|
|
|
70 |
done
|
|
|
71 |
|
|
|
72 |
lemma pflat_len_outside:
|
|
|
73 |
assumes "p \<notin> Pos v1"
|
|
|
74 |
shows "pflat_len v1 p = -1 "
|
|
|
75 |
using assms by (simp add: pflat_len_def)
|
|
|
76 |
|
|
|
77 |
|
|
|
78 |
|
|
|
79 |
section \<open>Orderings\<close>
|
|
|
80 |
|
|
|
81 |
|
|
|
82 |
definition prefix_list:: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" ("_ \<sqsubseteq>pre _" [60,59] 60)
|
|
|
83 |
where
|
|
|
84 |
"ps1 \<sqsubseteq>pre ps2 \<equiv> \<exists>ps'. ps1 @ps' = ps2"
|
|
|
85 |
|
|
|
86 |
definition sprefix_list:: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" ("_ \<sqsubset>spre _" [60,59] 60)
|
|
|
87 |
where
|
|
|
88 |
"ps1 \<sqsubset>spre ps2 \<equiv> ps1 \<sqsubseteq>pre ps2 \<and> ps1 \<noteq> ps2"
|
|
|
89 |
|
|
|
90 |
inductive lex_list :: "nat list \<Rightarrow> nat list \<Rightarrow> bool" ("_ \<sqsubset>lex _" [60,59] 60)
|
|
|
91 |
where
|
|
|
92 |
"[] \<sqsubset>lex (p#ps)"
|
|
|
93 |
| "ps1 \<sqsubset>lex ps2 \<Longrightarrow> (p#ps1) \<sqsubset>lex (p#ps2)"
|
|
|
94 |
| "p1 < p2 \<Longrightarrow> (p1#ps1) \<sqsubset>lex (p2#ps2)"
|
|
|
95 |
|
|
|
96 |
lemma lex_irrfl:
|
|
|
97 |
fixes ps1 ps2 :: "nat list"
|
|
|
98 |
assumes "ps1 \<sqsubset>lex ps2"
|
|
|
99 |
shows "ps1 \<noteq> ps2"
|
|
|
100 |
using assms
|
|
|
101 |
by(induct rule: lex_list.induct)(auto)
|
|
|
102 |
|
|
|
103 |
lemma lex_simps [simp]:
|
|
|
104 |
fixes xs ys :: "nat list"
|
|
|
105 |
shows "[] \<sqsubset>lex ys \<longleftrightarrow> ys \<noteq> []"
|
|
|
106 |
and "xs \<sqsubset>lex [] \<longleftrightarrow> False"
|
|
|
107 |
and "(x # xs) \<sqsubset>lex (y # ys) \<longleftrightarrow> (x < y \<or> (x = y \<and> xs \<sqsubset>lex ys))"
|
|
|
108 |
by (auto simp add: neq_Nil_conv elim: lex_list.cases intro: lex_list.intros)
|
|
|
109 |
|
|
|
110 |
lemma lex_trans:
|
|
|
111 |
fixes ps1 ps2 ps3 :: "nat list"
|
|
|
112 |
assumes "ps1 \<sqsubset>lex ps2" "ps2 \<sqsubset>lex ps3"
|
|
|
113 |
shows "ps1 \<sqsubset>lex ps3"
|
|
|
114 |
using assms
|
|
|
115 |
by (induct arbitrary: ps3 rule: lex_list.induct)
|
|
|
116 |
(auto elim: lex_list.cases)
|
|
|
117 |
|
|
|
118 |
|
|
|
119 |
lemma lex_trichotomous:
|
|
|
120 |
fixes p q :: "nat list"
|
|
|
121 |
shows "p = q \<or> p \<sqsubset>lex q \<or> q \<sqsubset>lex p"
|
|
|
122 |
apply(induct p arbitrary: q)
|
|
|
123 |
apply(auto elim: lex_list.cases)
|
|
|
124 |
apply(case_tac q)
|
|
|
125 |
apply(auto)
|
|
|
126 |
done
|
|
|
127 |
|
|
|
128 |
|
|
|
129 |
|
|
|
130 |
|
|
|
131 |
section \<open>POSIX Ordering of Values According to Okui \& Suzuki\<close>
|
|
|
132 |
|
|
|
133 |
|
|
|
134 |
definition PosOrd:: "val \<Rightarrow> nat list \<Rightarrow> val \<Rightarrow> bool" ("_ \<sqsubset>val _ _" [60, 60, 59] 60)
|
|
|
135 |
where
|
|
|
136 |
"v1 \<sqsubset>val p v2 \<equiv> pflat_len v1 p > pflat_len v2 p \<and>
|
|
|
137 |
(\<forall>q \<in> Pos v1 \<union> Pos v2. q \<sqsubset>lex p \<longrightarrow> pflat_len v1 q = pflat_len v2 q)"
|
|
|
138 |
|
|
|
139 |
lemma PosOrd_def2:
|
|
|
140 |
shows "v1 \<sqsubset>val p v2 \<longleftrightarrow>
|
|
|
141 |
pflat_len v1 p > pflat_len v2 p \<and>
|
|
|
142 |
(\<forall>q \<in> Pos v1. q \<sqsubset>lex p \<longrightarrow> pflat_len v1 q = pflat_len v2 q) \<and>
|
|
|
143 |
(\<forall>q \<in> Pos v2. q \<sqsubset>lex p \<longrightarrow> pflat_len v1 q = pflat_len v2 q)"
|
|
|
144 |
unfolding PosOrd_def
|
|
|
145 |
apply(auto)
|
|
|
146 |
done
|
|
|
147 |
|
|
|
148 |
|
|
|
149 |
definition PosOrd_ex:: "val \<Rightarrow> val \<Rightarrow> bool" ("_ :\<sqsubset>val _" [60, 59] 60)
|
|
|
150 |
where
|
|
|
151 |
"v1 :\<sqsubset>val v2 \<equiv> \<exists>p. v1 \<sqsubset>val p v2"
|
|
|
152 |
|
|
|
153 |
definition PosOrd_ex_eq:: "val \<Rightarrow> val \<Rightarrow> bool" ("_ :\<sqsubseteq>val _" [60, 59] 60)
|
|
|
154 |
where
|
|
|
155 |
"v1 :\<sqsubseteq>val v2 \<equiv> v1 :\<sqsubset>val v2 \<or> v1 = v2"
|
|
|
156 |
|
|
|
157 |
|
|
|
158 |
lemma PosOrd_trans:
|
|
|
159 |
assumes "v1 :\<sqsubset>val v2" "v2 :\<sqsubset>val v3"
|
|
|
160 |
shows "v1 :\<sqsubset>val v3"
|
|
|
161 |
proof -
|
|
|
162 |
from assms obtain p p'
|
|
|
163 |
where as: "v1 \<sqsubset>val p v2" "v2 \<sqsubset>val p' v3" unfolding PosOrd_ex_def by blast
|
|
|
164 |
then have pos: "p \<in> Pos v1" "p' \<in> Pos v2" unfolding PosOrd_def pflat_len_def
|
|
|
165 |
by (smt not_int_zless_negative)+
|
|
|
166 |
have "p = p' \<or> p \<sqsubset>lex p' \<or> p' \<sqsubset>lex p"
|
|
|
167 |
by (rule lex_trichotomous)
|
|
|
168 |
moreover
|
|
|
169 |
{ assume "p = p'"
|
|
|
170 |
with as have "v1 \<sqsubset>val p v3" unfolding PosOrd_def pflat_len_def
|
|
|
171 |
by (smt Un_iff)
|
|
|
172 |
then have " v1 :\<sqsubset>val v3" unfolding PosOrd_ex_def by blast
|
|
|
173 |
}
|
|
|
174 |
moreover
|
|
|
175 |
{ assume "p \<sqsubset>lex p'"
|
|
|
176 |
with as have "v1 \<sqsubset>val p v3" unfolding PosOrd_def pflat_len_def
|
|
|
177 |
by (smt Un_iff lex_trans)
|
|
|
178 |
then have " v1 :\<sqsubset>val v3" unfolding PosOrd_ex_def by blast
|
|
|
179 |
}
|
|
|
180 |
moreover
|
|
|
181 |
{ assume "p' \<sqsubset>lex p"
|
|
|
182 |
with as have "v1 \<sqsubset>val p' v3" unfolding PosOrd_def
|
|
|
183 |
by (smt Un_iff lex_trans pflat_len_def)
|
|
|
184 |
then have "v1 :\<sqsubset>val v3" unfolding PosOrd_ex_def by blast
|
|
|
185 |
}
|
|
|
186 |
ultimately show "v1 :\<sqsubset>val v3" by blast
|
|
|
187 |
qed
|
|
|
188 |
|
|
|
189 |
lemma PosOrd_irrefl:
|
|
|
190 |
assumes "v :\<sqsubset>val v"
|
|
|
191 |
shows "False"
|
|
|
192 |
using assms unfolding PosOrd_ex_def PosOrd_def
|
|
|
193 |
by auto
|
|
|
194 |
|
|
|
195 |
lemma PosOrd_assym:
|
|
|
196 |
assumes "v1 :\<sqsubset>val v2"
|
|
|
197 |
shows "\<not>(v2 :\<sqsubset>val v1)"
|
|
|
198 |
using assms
|
|
|
199 |
using PosOrd_irrefl PosOrd_trans by blast
|
|
|
200 |
|
|
|
201 |
(*
|
|
|
202 |
:\<sqsubseteq>val and :\<sqsubset>val are partial orders.
|
|
|
203 |
*)
|
|
|
204 |
|
|
|
205 |
lemma PosOrd_ordering:
|
|
|
206 |
shows "ordering (\<lambda>v1 v2. v1 :\<sqsubseteq>val v2) (\<lambda> v1 v2. v1 :\<sqsubset>val v2)"
|
|
|
207 |
unfolding ordering_def PosOrd_ex_eq_def
|
|
|
208 |
apply(auto)
|
|
|
209 |
using PosOrd_irrefl apply blast
|
|
|
210 |
using PosOrd_assym apply blast
|
|
|
211 |
using PosOrd_trans by blast
|
|
|
212 |
|
|
|
213 |
lemma PosOrd_order:
|
|
|
214 |
shows "class.order (\<lambda>v1 v2. v1 :\<sqsubseteq>val v2) (\<lambda> v1 v2. v1 :\<sqsubset>val v2)"
|
|
|
215 |
using PosOrd_ordering
|
|
|
216 |
apply(simp add: class.order_def class.preorder_def class.order_axioms_def)
|
|
|
217 |
unfolding ordering_def
|
|
|
218 |
by blast
|
|
|
219 |
|
|
|
220 |
|
|
|
221 |
lemma PosOrd_ex_eq2:
|
|
|
222 |
shows "v1 :\<sqsubset>val v2 \<longleftrightarrow> (v1 :\<sqsubseteq>val v2 \<and> v1 \<noteq> v2)"
|
|
|
223 |
using PosOrd_ordering
|
|
|
224 |
unfolding ordering_def
|
|
|
225 |
by auto
|
|
|
226 |
|
|
|
227 |
lemma PosOrdeq_trans:
|
|
|
228 |
assumes "v1 :\<sqsubseteq>val v2" "v2 :\<sqsubseteq>val v3"
|
|
|
229 |
shows "v1 :\<sqsubseteq>val v3"
|
|
|
230 |
using assms PosOrd_ordering
|
|
|
231 |
unfolding ordering_def
|
|
|
232 |
by blast
|
|
|
233 |
|
|
|
234 |
lemma PosOrdeq_antisym:
|
|
|
235 |
assumes "v1 :\<sqsubseteq>val v2" "v2 :\<sqsubseteq>val v1"
|
|
|
236 |
shows "v1 = v2"
|
|
|
237 |
using assms PosOrd_ordering
|
|
|
238 |
unfolding ordering_def
|
|
|
239 |
by blast
|
|
|
240 |
|
|
|
241 |
lemma PosOrdeq_refl:
|
|
|
242 |
shows "v :\<sqsubseteq>val v"
|
|
|
243 |
unfolding PosOrd_ex_eq_def
|
|
|
244 |
by auto
|
|
|
245 |
|
|
|
246 |
|
|
|
247 |
lemma PosOrd_shorterE:
|
|
|
248 |
assumes "v1 :\<sqsubset>val v2"
|
|
|
249 |
shows "length (flat v2) \<le> length (flat v1)"
|
|
|
250 |
using assms unfolding PosOrd_ex_def PosOrd_def
|
|
|
251 |
apply(auto)
|
|
|
252 |
apply(case_tac p)
|
|
|
253 |
apply(simp add: pflat_len_simps)
|
|
|
254 |
apply(drule_tac x="[]" in bspec)
|
|
|
255 |
apply(simp add: Pos_empty)
|
|
|
256 |
apply(simp add: pflat_len_simps)
|
|
|
257 |
done
|
|
|
258 |
|
|
|
259 |
lemma PosOrd_shorterI:
|
|
|
260 |
assumes "length (flat v2) < length (flat v1)"
|
|
|
261 |
shows "v1 :\<sqsubset>val v2"
|
|
|
262 |
unfolding PosOrd_ex_def PosOrd_def pflat_len_def
|
|
|
263 |
using assms Pos_empty by force
|
|
|
264 |
|
|
|
265 |
lemma PosOrd_spreI:
|
|
|
266 |
assumes "flat v' \<sqsubset>spre flat v"
|
|
|
267 |
shows "v :\<sqsubset>val v'"
|
|
|
268 |
using assms
|
|
|
269 |
apply(rule_tac PosOrd_shorterI)
|
|
|
270 |
unfolding prefix_list_def sprefix_list_def
|
|
|
271 |
by (metis append_Nil2 append_eq_conv_conj drop_all le_less_linear)
|
|
|
272 |
|
|
|
273 |
lemma pflat_len_inside:
|
|
|
274 |
assumes "pflat_len v2 p < pflat_len v1 p"
|
|
|
275 |
shows "p \<in> Pos v1"
|
|
|
276 |
using assms
|
|
|
277 |
unfolding pflat_len_def
|
|
|
278 |
by (auto split: if_splits)
|
|
|
279 |
|
|
|
280 |
|
|
|
281 |
lemma PosOrd_Left_Right:
|
|
|
282 |
assumes "flat v1 = flat v2"
|
|
|
283 |
shows "Left v1 :\<sqsubset>val Right v2"
|
|
|
284 |
unfolding PosOrd_ex_def
|
|
|
285 |
apply(rule_tac x="[0]" in exI)
|
|
|
286 |
apply(auto simp add: PosOrd_def pflat_len_simps assms)
|
|
|
287 |
done
|
|
|
288 |
|
|
|
289 |
lemma PosOrd_LeftE:
|
|
|
290 |
assumes "Left v1 :\<sqsubset>val Left v2" "flat v1 = flat v2"
|
|
|
291 |
shows "v1 :\<sqsubset>val v2"
|
|
|
292 |
using assms
|
|
|
293 |
unfolding PosOrd_ex_def PosOrd_def2
|
|
|
294 |
apply(auto simp add: pflat_len_simps)
|
|
|
295 |
apply(frule pflat_len_inside)
|
|
|
296 |
apply(auto simp add: pflat_len_simps)
|
|
|
297 |
by (metis lex_simps(3) pflat_len_simps(3))
|
|
|
298 |
|
|
|
299 |
lemma PosOrd_LeftI:
|
|
|
300 |
assumes "v1 :\<sqsubset>val v2" "flat v1 = flat v2"
|
|
|
301 |
shows "Left v1 :\<sqsubset>val Left v2"
|
|
|
302 |
using assms
|
|
|
303 |
unfolding PosOrd_ex_def PosOrd_def2
|
|
|
304 |
apply(auto simp add: pflat_len_simps)
|
|
|
305 |
by (metis less_numeral_extra(3) lex_simps(3) pflat_len_simps(3))
|
|
|
306 |
|
|
|
307 |
lemma PosOrd_Left_eq:
|
|
|
308 |
assumes "flat v1 = flat v2"
|
|
|
309 |
shows "Left v1 :\<sqsubset>val Left v2 \<longleftrightarrow> v1 :\<sqsubset>val v2"
|
|
|
310 |
using assms PosOrd_LeftE PosOrd_LeftI
|
|
|
311 |
by blast
|
|
|
312 |
|
|
|
313 |
|
|
|
314 |
lemma PosOrd_RightE:
|
|
|
315 |
assumes "Right v1 :\<sqsubset>val Right v2" "flat v1 = flat v2"
|
|
|
316 |
shows "v1 :\<sqsubset>val v2"
|
|
|
317 |
using assms
|
|
|
318 |
unfolding PosOrd_ex_def PosOrd_def2
|
|
|
319 |
apply(auto simp add: pflat_len_simps)
|
|
|
320 |
apply(frule pflat_len_inside)
|
|
|
321 |
apply(auto simp add: pflat_len_simps)
|
|
|
322 |
by (metis lex_simps(3) pflat_len_simps(5))
|
|
|
323 |
|
|
|
324 |
lemma PosOrd_RightI:
|
|
|
325 |
assumes "v1 :\<sqsubset>val v2" "flat v1 = flat v2"
|
|
|
326 |
shows "Right v1 :\<sqsubset>val Right v2"
|
|
|
327 |
using assms
|
|
|
328 |
unfolding PosOrd_ex_def PosOrd_def2
|
|
|
329 |
apply(auto simp add: pflat_len_simps)
|
|
|
330 |
by (metis lex_simps(3) nat_neq_iff pflat_len_simps(5))
|
|
|
331 |
|
|
|
332 |
|
|
|
333 |
lemma PosOrd_Right_eq:
|
|
|
334 |
assumes "flat v1 = flat v2"
|
|
|
335 |
shows "Right v1 :\<sqsubset>val Right v2 \<longleftrightarrow> v1 :\<sqsubset>val v2"
|
|
|
336 |
using assms PosOrd_RightE PosOrd_RightI
|
|
|
337 |
by blast
|
|
|
338 |
|
|
|
339 |
|
|
|
340 |
lemma PosOrd_SeqI1:
|
|
|
341 |
assumes "v1 :\<sqsubset>val w1" "flat (Seq v1 v2) = flat (Seq w1 w2)"
|
|
|
342 |
shows "Seq v1 v2 :\<sqsubset>val Seq w1 w2"
|
|
|
343 |
using assms(1)
|
|
|
344 |
apply(subst (asm) PosOrd_ex_def)
|
|
|
345 |
apply(subst (asm) PosOrd_def)
|
|
|
346 |
apply(clarify)
|
|
|
347 |
apply(subst PosOrd_ex_def)
|
|
|
348 |
apply(rule_tac x="0#p" in exI)
|
|
|
349 |
apply(subst PosOrd_def)
|
|
|
350 |
apply(rule conjI)
|
|
|
351 |
apply(simp add: pflat_len_simps)
|
|
|
352 |
apply(rule ballI)
|
|
|
353 |
apply(rule impI)
|
|
|
354 |
apply(simp only: Pos.simps)
|
|
|
355 |
apply(auto)[1]
|
|
|
356 |
apply(simp add: pflat_len_simps)
|
|
|
357 |
apply(auto simp add: pflat_len_simps)
|
|
|
358 |
using assms(2)
|
|
|
359 |
apply(simp)
|
|
|
360 |
apply(metis length_append of_nat_add)
|
|
|
361 |
done
|
|
|
362 |
|
|
|
363 |
lemma PosOrd_SeqI2:
|
|
|
364 |
assumes "v2 :\<sqsubset>val w2" "flat v2 = flat w2"
|
|
|
365 |
shows "Seq v v2 :\<sqsubset>val Seq v w2"
|
|
|
366 |
using assms(1)
|
|
|
367 |
apply(subst (asm) PosOrd_ex_def)
|
|
|
368 |
apply(subst (asm) PosOrd_def)
|
|
|
369 |
apply(clarify)
|
|
|
370 |
apply(subst PosOrd_ex_def)
|
|
|
371 |
apply(rule_tac x="Suc 0#p" in exI)
|
|
|
372 |
apply(subst PosOrd_def)
|
|
|
373 |
apply(rule conjI)
|
|
|
374 |
apply(simp add: pflat_len_simps)
|
|
|
375 |
apply(rule ballI)
|
|
|
376 |
apply(rule impI)
|
|
|
377 |
apply(simp only: Pos.simps)
|
|
|
378 |
apply(auto)[1]
|
|
|
379 |
apply(simp add: pflat_len_simps)
|
|
|
380 |
using assms(2)
|
|
|
381 |
apply(simp)
|
|
|
382 |
apply(auto simp add: pflat_len_simps)
|
|
|
383 |
done
|
|
|
384 |
|
|
|
385 |
lemma PosOrd_Seq_eq:
|
|
|
386 |
assumes "flat v2 = flat w2"
|
|
|
387 |
shows "(Seq v v2) :\<sqsubset>val (Seq v w2) \<longleftrightarrow> v2 :\<sqsubset>val w2"
|
|
|
388 |
using assms
|
|
|
389 |
apply(auto)
|
|
|
390 |
prefer 2
|
|
|
391 |
apply(simp add: PosOrd_SeqI2)
|
|
|
392 |
apply(simp add: PosOrd_ex_def)
|
|
|
393 |
apply(auto)
|
|
|
394 |
apply(case_tac p)
|
|
|
395 |
apply(simp add: PosOrd_def pflat_len_simps)
|
|
|
396 |
apply(case_tac a)
|
|
|
397 |
apply(simp add: PosOrd_def pflat_len_simps)
|
|
|
398 |
apply(clarify)
|
|
|
399 |
apply(case_tac nat)
|
|
|
400 |
prefer 2
|
|
|
401 |
apply(simp add: PosOrd_def pflat_len_simps pflat_len_outside)
|
|
|
402 |
apply(rule_tac x="list" in exI)
|
|
|
403 |
apply(auto simp add: PosOrd_def2 pflat_len_simps)
|
|
|
404 |
apply(smt Collect_disj_eq lex_list.intros(2) mem_Collect_eq pflat_len_simps(2))
|
|
|
405 |
apply(smt Collect_disj_eq lex_list.intros(2) mem_Collect_eq pflat_len_simps(2))
|
|
|
406 |
done
|
|
|
407 |
|
|
|
408 |
|
|
|
409 |
|
|
|
410 |
lemma PosOrd_StarsI:
|
|
|
411 |
assumes "v1 :\<sqsubset>val v2" "flats (v1#vs1) = flats (v2#vs2)"
|
|
|
412 |
shows "Stars (v1#vs1) :\<sqsubset>val Stars (v2#vs2)"
|
|
|
413 |
using assms(1)
|
|
|
414 |
apply(subst (asm) PosOrd_ex_def)
|
|
|
415 |
apply(subst (asm) PosOrd_def)
|
|
|
416 |
apply(clarify)
|
|
|
417 |
apply(subst PosOrd_ex_def)
|
|
|
418 |
apply(subst PosOrd_def)
|
|
|
419 |
apply(rule_tac x="0#p" in exI)
|
|
|
420 |
apply(simp add: pflat_len_Stars_simps pflat_len_simps)
|
|
|
421 |
using assms(2)
|
|
|
422 |
apply(simp add: pflat_len_simps)
|
|
|
423 |
apply(auto simp add: pflat_len_Stars_simps pflat_len_simps)
|
|
|
424 |
by (metis length_append of_nat_add)
|
|
|
425 |
|
|
|
426 |
lemma PosOrd_StarsI2:
|
|
|
427 |
assumes "Stars vs1 :\<sqsubset>val Stars vs2" "flats vs1 = flats vs2"
|
|
|
428 |
shows "Stars (v#vs1) :\<sqsubset>val Stars (v#vs2)"
|
|
|
429 |
using assms(1)
|
|
|
430 |
apply(subst (asm) PosOrd_ex_def)
|
|
|
431 |
apply(subst (asm) PosOrd_def)
|
|
|
432 |
apply(clarify)
|
|
|
433 |
apply(subst PosOrd_ex_def)
|
|
|
434 |
apply(subst PosOrd_def)
|
|
|
435 |
apply(case_tac p)
|
|
|
436 |
apply(simp add: pflat_len_simps)
|
|
|
437 |
apply(rule_tac x="Suc a#list" in exI)
|
|
|
438 |
apply(auto simp add: pflat_len_Stars_simps pflat_len_simps assms(2))
|
|
|
439 |
done
|
|
|
440 |
|
|
|
441 |
lemma PosOrd_Stars_appendI:
|
|
|
442 |
assumes "Stars vs1 :\<sqsubset>val Stars vs2" "flat (Stars vs1) = flat (Stars vs2)"
|
|
|
443 |
shows "Stars (vs @ vs1) :\<sqsubset>val Stars (vs @ vs2)"
|
|
|
444 |
using assms
|
|
|
445 |
apply(induct vs)
|
|
|
446 |
apply(simp)
|
|
|
447 |
apply(simp add: PosOrd_StarsI2)
|
|
|
448 |
done
|
|
|
449 |
|
|
|
450 |
lemma PosOrd_StarsE2:
|
|
|
451 |
assumes "Stars (v # vs1) :\<sqsubset>val Stars (v # vs2)"
|
|
|
452 |
shows "Stars vs1 :\<sqsubset>val Stars vs2"
|
|
|
453 |
using assms
|
|
|
454 |
apply(subst (asm) PosOrd_ex_def)
|
|
|
455 |
apply(erule exE)
|
|
|
456 |
apply(case_tac p)
|
|
|
457 |
apply(simp)
|
|
|
458 |
apply(simp add: PosOrd_def pflat_len_simps)
|
|
|
459 |
apply(subst PosOrd_ex_def)
|
|
|
460 |
apply(rule_tac x="[]" in exI)
|
|
|
461 |
apply(simp add: PosOrd_def pflat_len_simps Pos_empty)
|
|
|
462 |
apply(simp)
|
|
|
463 |
apply(case_tac a)
|
|
|
464 |
apply(clarify)
|
|
|
465 |
apply(auto simp add: pflat_len_simps PosOrd_def pflat_len_def split: if_splits)[1]
|
|
|
466 |
apply(clarify)
|
|
|
467 |
apply(simp add: PosOrd_ex_def)
|
|
|
468 |
apply(rule_tac x="nat#list" in exI)
|
|
|
469 |
apply(auto simp add: PosOrd_def pflat_len_simps)[1]
|
|
|
470 |
apply(case_tac q)
|
|
|
471 |
apply(simp add: PosOrd_def pflat_len_simps)
|
|
|
472 |
apply(clarify)
|
|
|
473 |
apply(drule_tac x="Suc a # lista" in bspec)
|
|
|
474 |
apply(simp)
|
|
|
475 |
apply(auto simp add: PosOrd_def pflat_len_simps)[1]
|
|
|
476 |
apply(case_tac q)
|
|
|
477 |
apply(simp add: PosOrd_def pflat_len_simps)
|
|
|
478 |
apply(clarify)
|
|
|
479 |
apply(drule_tac x="Suc a # lista" in bspec)
|
|
|
480 |
apply(simp)
|
|
|
481 |
apply(auto simp add: PosOrd_def pflat_len_simps)[1]
|
|
|
482 |
done
|
|
|
483 |
|
|
|
484 |
lemma PosOrd_Stars_appendE:
|
|
|
485 |
assumes "Stars (vs @ vs1) :\<sqsubset>val Stars (vs @ vs2)"
|
|
|
486 |
shows "Stars vs1 :\<sqsubset>val Stars vs2"
|
|
|
487 |
using assms
|
|
|
488 |
apply(induct vs)
|
|
|
489 |
apply(simp)
|
|
|
490 |
apply(simp add: PosOrd_StarsE2)
|
|
|
491 |
done
|
|
|
492 |
|
|
|
493 |
lemma PosOrd_Stars_append_eq:
|
|
|
494 |
assumes "flats vs1 = flats vs2"
|
|
|
495 |
shows "Stars (vs @ vs1) :\<sqsubset>val Stars (vs @ vs2) \<longleftrightarrow> Stars vs1 :\<sqsubset>val Stars vs2"
|
|
|
496 |
using assms
|
|
|
497 |
apply(rule_tac iffI)
|
|
|
498 |
apply(erule PosOrd_Stars_appendE)
|
|
|
499 |
apply(rule PosOrd_Stars_appendI)
|
|
|
500 |
apply(auto)
|
|
|
501 |
done
|
|
|
502 |
|
|
|
503 |
lemma PosOrd_almost_trichotomous:
|
|
|
504 |
shows "v1 :\<sqsubset>val v2 \<or> v2 :\<sqsubset>val v1 \<or> (length (flat v1) = length (flat v2))"
|
|
|
505 |
apply(auto simp add: PosOrd_ex_def)
|
|
|
506 |
apply(auto simp add: PosOrd_def)
|
|
|
507 |
apply(rule_tac x="[]" in exI)
|
|
|
508 |
apply(auto simp add: Pos_empty pflat_len_simps)
|
|
|
509 |
apply(drule_tac x="[]" in spec)
|
|
|
510 |
apply(auto simp add: Pos_empty pflat_len_simps)
|
|
|
511 |
done
|
|
|
512 |
|
|
|
513 |
|
|
|
514 |
|
|
|
515 |
section \<open>The Posix Value is smaller than any other Value\<close>
|
|
|
516 |
|
|
|
517 |
|
|
|
518 |
lemma Posix_PosOrd:
|
|
|
519 |
assumes "s \<in> r \<rightarrow> v1" "v2 \<in> LV r s"
|
|
|
520 |
shows "v1 :\<sqsubseteq>val v2"
|
|
|
521 |
using assms
|
|
|
522 |
proof (induct arbitrary: v2 rule: Posix.induct)
|
|
|
523 |
case (Posix_ONE v)
|
|
|
524 |
have "v \<in> LV ONE []" by fact
|
|
|
525 |
then have "v = Void"
|
|
|
526 |
by (simp add: LV_simps)
|
|
|
527 |
then show "Void :\<sqsubseteq>val v"
|
|
|
528 |
by (simp add: PosOrd_ex_eq_def)
|
|
|
529 |
next
|
|
|
530 |
case (Posix_CH c v)
|
|
|
531 |
have "v \<in> LV (CH c) [c]" by fact
|
|
|
532 |
then have "v = Char c"
|
|
|
533 |
by (simp add: LV_simps)
|
|
|
534 |
then show "Char c :\<sqsubseteq>val v"
|
|
|
535 |
by (simp add: PosOrd_ex_eq_def)
|
|
|
536 |
next
|
|
|
537 |
case (Posix_ALT1 s r1 v r2 v2)
|
|
|
538 |
have as1: "s \<in> r1 \<rightarrow> v" by fact
|
|
|
539 |
have IH: "\<And>v2. v2 \<in> LV r1 s \<Longrightarrow> v :\<sqsubseteq>val v2" by fact
|
|
|
540 |
have "v2 \<in> LV (ALT r1 r2) s" by fact
|
|
|
541 |
then have "\<Turnstile> v2 : ALT r1 r2" "flat v2 = s"
|
|
|
542 |
by(auto simp add: LV_def prefix_list_def)
|
|
|
543 |
then consider
|
|
|
544 |
(Left) v3 where "v2 = Left v3" "\<Turnstile> v3 : r1" "flat v3 = s"
|
|
|
545 |
| (Right) v3 where "v2 = Right v3" "\<Turnstile> v3 : r2" "flat v3 = s"
|
|
|
546 |
by (auto elim: Prf.cases)
|
|
|
547 |
then show "Left v :\<sqsubseteq>val v2"
|
|
|
548 |
proof(cases)
|
|
|
549 |
case (Left v3)
|
|
|
550 |
have "v3 \<in> LV r1 s" using Left(2,3)
|
|
|
551 |
by (auto simp add: LV_def prefix_list_def)
|
|
|
552 |
with IH have "v :\<sqsubseteq>val v3" by simp
|
|
|
553 |
moreover
|
|
|
554 |
have "flat v3 = flat v" using as1 Left(3)
|
|
|
555 |
by (simp add: Posix1(2))
|
|
|
556 |
ultimately have "Left v :\<sqsubseteq>val Left v3"
|
|
|
557 |
by (simp add: PosOrd_ex_eq_def PosOrd_Left_eq)
|
|
|
558 |
then show "Left v :\<sqsubseteq>val v2" unfolding Left .
|
|
|
559 |
next
|
|
|
560 |
case (Right v3)
|
|
|
561 |
have "flat v3 = flat v" using as1 Right(3)
|
|
|
562 |
by (simp add: Posix1(2))
|
|
|
563 |
then have "Left v :\<sqsubseteq>val Right v3"
|
|
|
564 |
unfolding PosOrd_ex_eq_def
|
|
|
565 |
by (simp add: PosOrd_Left_Right)
|
|
|
566 |
then show "Left v :\<sqsubseteq>val v2" unfolding Right .
|
|
|
567 |
qed
|
|
|
568 |
next
|
|
|
569 |
case (Posix_ALT2 s r2 v r1 v2)
|
|
|
570 |
have as1: "s \<in> r2 \<rightarrow> v" by fact
|
|
|
571 |
have as2: "s \<notin> L r1" by fact
|
|
|
572 |
have IH: "\<And>v2. v2 \<in> LV r2 s \<Longrightarrow> v :\<sqsubseteq>val v2" by fact
|
|
|
573 |
have "v2 \<in> LV (ALT r1 r2) s" by fact
|
|
|
574 |
then have "\<Turnstile> v2 : ALT r1 r2" "flat v2 = s"
|
|
|
575 |
by(auto simp add: LV_def prefix_list_def)
|
|
|
576 |
then consider
|
|
|
577 |
(Left) v3 where "v2 = Left v3" "\<Turnstile> v3 : r1" "flat v3 = s"
|
|
|
578 |
| (Right) v3 where "v2 = Right v3" "\<Turnstile> v3 : r2" "flat v3 = s"
|
|
|
579 |
by (auto elim: Prf.cases)
|
|
|
580 |
then show "Right v :\<sqsubseteq>val v2"
|
|
|
581 |
proof (cases)
|
|
|
582 |
case (Right v3)
|
|
|
583 |
have "v3 \<in> LV r2 s" using Right(2,3)
|
|
|
584 |
by (auto simp add: LV_def prefix_list_def)
|
|
|
585 |
with IH have "v :\<sqsubseteq>val v3" by simp
|
|
|
586 |
moreover
|
|
|
587 |
have "flat v3 = flat v" using as1 Right(3)
|
|
|
588 |
by (simp add: Posix1(2))
|
|
|
589 |
ultimately have "Right v :\<sqsubseteq>val Right v3"
|
|
|
590 |
by (auto simp add: PosOrd_ex_eq_def PosOrd_RightI)
|
|
|
591 |
then show "Right v :\<sqsubseteq>val v2" unfolding Right .
|
|
|
592 |
next
|
|
|
593 |
case (Left v3)
|
|
|
594 |
have "v3 \<in> LV r1 s" using Left(2,3) as2
|
|
|
595 |
by (auto simp add: LV_def prefix_list_def)
|
|
|
596 |
then have "flat v3 = flat v \<and> \<Turnstile> v3 : r1" using as1 Left(3)
|
|
|
597 |
by (simp add: Posix1(2) LV_def)
|
|
|
598 |
then have "False" using as1 as2 Left
|
|
|
599 |
by (auto simp add: Posix1(2) L_flat_Prf1)
|
|
|
600 |
then show "Right v :\<sqsubseteq>val v2" by simp
|
|
|
601 |
qed
|
|
|
602 |
next
|
|
|
603 |
case (Posix_SEQ s1 r1 v1 s2 r2 v2 v3)
|
|
|
604 |
have "s1 \<in> r1 \<rightarrow> v1" "s2 \<in> r2 \<rightarrow> v2" by fact+
|
|
|
605 |
then have as1: "s1 = flat v1" "s2 = flat v2" by (simp_all add: Posix1(2))
|
|
|
606 |
have IH1: "\<And>v3. v3 \<in> LV r1 s1 \<Longrightarrow> v1 :\<sqsubseteq>val v3" by fact
|
|
|
607 |
have IH2: "\<And>v3. v3 \<in> LV r2 s2 \<Longrightarrow> v2 :\<sqsubseteq>val v3" by fact
|
|
|
608 |
have cond: "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L r1 \<and> s\<^sub>4 \<in> L r2)" by fact
|
|
|
609 |
have "v3 \<in> LV (SEQ r1 r2) (s1 @ s2)" by fact
|
|
|
610 |
then obtain v3a v3b where eqs:
|
|
|
611 |
"v3 = Seq v3a v3b" "\<Turnstile> v3a : r1" "\<Turnstile> v3b : r2"
|
|
|
612 |
"flat v3a @ flat v3b = s1 @ s2"
|
|
|
613 |
by (force simp add: prefix_list_def LV_def elim: Prf.cases)
|
|
|
614 |
with cond have "flat v3a \<sqsubseteq>pre s1" unfolding prefix_list_def
|
|
|
615 |
by (smt L_flat_Prf1 append_eq_append_conv2 append_self_conv)
|
|
|
616 |
then have "flat v3a \<sqsubset>spre s1 \<or> (flat v3a = s1 \<and> flat v3b = s2)" using eqs
|
|
|
617 |
by (simp add: sprefix_list_def append_eq_conv_conj)
|
|
|
618 |
then have q2: "v1 :\<sqsubset>val v3a \<or> (flat v3a = s1 \<and> flat v3b = s2)"
|
|
|
619 |
using PosOrd_spreI as1(1) eqs by blast
|
|
|
620 |
then have "v1 :\<sqsubset>val v3a \<or> (v3a \<in> LV r1 s1 \<and> v3b \<in> LV r2 s2)" using eqs(2,3)
|
|
|
621 |
by (auto simp add: LV_def)
|
|
|
622 |
then have "v1 :\<sqsubset>val v3a \<or> (v1 :\<sqsubseteq>val v3a \<and> v2 :\<sqsubseteq>val v3b)" using IH1 IH2 by blast
|
|
|
623 |
then have "Seq v1 v2 :\<sqsubseteq>val Seq v3a v3b" using eqs q2 as1
|
|
|
624 |
unfolding PosOrd_ex_eq_def by (auto simp add: PosOrd_SeqI1 PosOrd_Seq_eq)
|
|
|
625 |
then show "Seq v1 v2 :\<sqsubseteq>val v3" unfolding eqs by blast
|
|
|
626 |
next
|
|
|
627 |
case (Posix_STAR1 s1 r v s2 vs v3)
|
|
|
628 |
have "s1 \<in> r \<rightarrow> v" "s2 \<in> STAR r \<rightarrow> Stars vs" by fact+
|
|
|
629 |
then have as1: "s1 = flat v" "s2 = flat (Stars vs)" by (auto dest: Posix1(2))
|
|
|
630 |
have IH1: "\<And>v3. v3 \<in> LV r s1 \<Longrightarrow> v :\<sqsubseteq>val v3" by fact
|
|
|
631 |
have IH2: "\<And>v3. v3 \<in> LV (STAR r) s2 \<Longrightarrow> Stars vs :\<sqsubseteq>val v3" by fact
|
|
|
632 |
have cond: "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (STAR r))" by fact
|
|
|
633 |
have cond2: "flat v \<noteq> []" by fact
|
|
|
634 |
have "v3 \<in> LV (STAR r) (s1 @ s2)" by fact
|
|
|
635 |
then consider
|
|
|
636 |
(NonEmpty) v3a vs3 where "v3 = Stars (v3a # vs3)"
|
|
|
637 |
"\<Turnstile> v3a : r" "\<Turnstile> Stars vs3 : STAR r"
|
|
|
638 |
"flat (Stars (v3a # vs3)) = s1 @ s2"
|
|
|
639 |
| (Empty) "v3 = Stars []"
|
|
|
640 |
unfolding LV_def
|
|
|
641 |
apply(auto)
|
|
|
642 |
apply(erule Prf.cases)
|
|
|
643 |
apply(auto)
|
|
|
644 |
apply(case_tac vs)
|
|
|
645 |
apply(auto intro: Prf.intros)
|
|
|
646 |
done
|
|
|
647 |
then show "Stars (v # vs) :\<sqsubseteq>val v3"
|
|
|
648 |
proof (cases)
|
|
|
649 |
case (NonEmpty v3a vs3)
|
|
|
650 |
have "flat (Stars (v3a # vs3)) = s1 @ s2" using NonEmpty(4) .
|
|
|
651 |
with cond have "flat v3a \<sqsubseteq>pre s1" using NonEmpty(2,3)
|
|
|
652 |
unfolding prefix_list_def
|
|
|
653 |
by (smt L_flat_Prf1 append_Nil2 append_eq_append_conv2 flat.simps(7))
|
|
|
654 |
then have "flat v3a \<sqsubset>spre s1 \<or> (flat v3a = s1 \<and> flat (Stars vs3) = s2)" using NonEmpty(4)
|
|
|
655 |
by (simp add: sprefix_list_def append_eq_conv_conj)
|
|
|
656 |
then have q2: "v :\<sqsubset>val v3a \<or> (flat v3a = s1 \<and> flat (Stars vs3) = s2)"
|
|
|
657 |
using PosOrd_spreI as1(1) NonEmpty(4) by blast
|
|
|
658 |
then have "v :\<sqsubset>val v3a \<or> (v3a \<in> LV r s1 \<and> Stars vs3 \<in> LV (STAR r) s2)"
|
|
|
659 |
using NonEmpty(2,3) by (auto simp add: LV_def)
|
|
|
660 |
then have "v :\<sqsubset>val v3a \<or> (v :\<sqsubseteq>val v3a \<and> Stars vs :\<sqsubseteq>val Stars vs3)" using IH1 IH2 by blast
|
|
|
661 |
then have "v :\<sqsubset>val v3a \<or> (v = v3a \<and> Stars vs :\<sqsubseteq>val Stars vs3)"
|
|
|
662 |
unfolding PosOrd_ex_eq_def by auto
|
|
|
663 |
then have "Stars (v # vs) :\<sqsubseteq>val Stars (v3a # vs3)" using NonEmpty(4) q2 as1
|
|
|
664 |
unfolding PosOrd_ex_eq_def
|
|
|
665 |
using PosOrd_StarsI PosOrd_StarsI2 by auto
|
|
|
666 |
then show "Stars (v # vs) :\<sqsubseteq>val v3" unfolding NonEmpty by blast
|
|
|
667 |
next
|
|
|
668 |
case Empty
|
|
|
669 |
have "v3 = Stars []" by fact
|
|
|
670 |
then show "Stars (v # vs) :\<sqsubseteq>val v3"
|
|
|
671 |
unfolding PosOrd_ex_eq_def using cond2
|
|
|
672 |
by (simp add: PosOrd_shorterI)
|
|
|
673 |
qed
|
|
|
674 |
next
|
|
|
675 |
case (Posix_STAR2 r v2)
|
|
|
676 |
have "v2 \<in> LV (STAR r) []" by fact
|
|
|
677 |
then have "v2 = Stars []"
|
|
|
678 |
unfolding LV_def by (auto elim: Prf.cases)
|
|
|
679 |
then show "Stars [] :\<sqsubseteq>val v2"
|
|
|
680 |
by (simp add: PosOrd_ex_eq_def)
|
|
|
681 |
qed
|
|
|
682 |
|
|
|
683 |
|
|
|
684 |
lemma Posix_PosOrd_reverse:
|
|
|
685 |
assumes "s \<in> r \<rightarrow> v1"
|
|
|
686 |
shows "\<not>(\<exists>v2 \<in> LV r s. v2 :\<sqsubset>val v1)"
|
|
|
687 |
using assms
|
|
|
688 |
by (metis Posix_PosOrd less_irrefl PosOrd_def
|
|
|
689 |
PosOrd_ex_eq_def PosOrd_ex_def PosOrd_trans)
|
|
|
690 |
|
|
|
691 |
lemma PosOrd_Posix:
|
|
|
692 |
assumes "v1 \<in> LV r s" "\<forall>v\<^sub>2 \<in> LV r s. \<not> v\<^sub>2 :\<sqsubset>val v1"
|
|
|
693 |
shows "s \<in> r \<rightarrow> v1"
|
|
|
694 |
proof -
|
|
|
695 |
have "s \<in> L r" using assms(1) unfolding LV_def
|
|
|
696 |
using L_flat_Prf1 by blast
|
|
|
697 |
then obtain vposix where vp: "s \<in> r \<rightarrow> vposix"
|
|
|
698 |
using lexer_correct_Some by blast
|
|
|
699 |
with assms(1) have "vposix :\<sqsubseteq>val v1" by (simp add: Posix_PosOrd)
|
|
|
700 |
then have "vposix = v1 \<or> vposix :\<sqsubset>val v1" unfolding PosOrd_ex_eq2 by auto
|
|
|
701 |
moreover
|
|
|
702 |
{ assume "vposix :\<sqsubset>val v1"
|
|
|
703 |
moreover
|
|
|
704 |
have "vposix \<in> LV r s" using vp
|
|
|
705 |
using Posix_LV by blast
|
|
|
706 |
ultimately have "False" using assms(2) by blast
|
|
|
707 |
}
|
|
|
708 |
ultimately show "s \<in> r \<rightarrow> v1" using vp by blast
|
|
|
709 |
qed
|
|
|
710 |
|
|
|
711 |
lemma Least_existence:
|
|
|
712 |
assumes "LV r s \<noteq> {}"
|
|
|
713 |
shows " \<exists>vmin \<in> LV r s. \<forall>v \<in> LV r s. vmin :\<sqsubseteq>val v"
|
|
|
714 |
proof -
|
|
|
715 |
from assms
|
|
|
716 |
obtain vposix where "s \<in> r \<rightarrow> vposix"
|
|
|
717 |
unfolding LV_def
|
|
|
718 |
using L_flat_Prf1 lexer_correct_Some by blast
|
|
|
719 |
then have "\<forall>v \<in> LV r s. vposix :\<sqsubseteq>val v"
|
|
|
720 |
by (simp add: Posix_PosOrd)
|
|
|
721 |
then show "\<exists>vmin \<in> LV r s. \<forall>v \<in> LV r s. vmin :\<sqsubseteq>val v"
|
|
|
722 |
using Posix_LV \<open>s \<in> r \<rightarrow> vposix\<close> by blast
|
|
|
723 |
qed
|
|
|
724 |
|
|
|
725 |
lemma Least_existence1:
|
|
|
726 |
assumes "LV r s \<noteq> {}"
|
|
|
727 |
shows " \<exists>!vmin \<in> LV r s. \<forall>v \<in> LV r s. vmin :\<sqsubseteq>val v"
|
|
|
728 |
using Least_existence[OF assms] assms
|
|
|
729 |
using PosOrdeq_antisym by blast
|
|
|
730 |
|
|
|
731 |
lemma Least_existence2:
|
|
|
732 |
assumes "LV r s \<noteq> {}"
|
|
|
733 |
shows " \<exists>!vmin \<in> LV r s. lexer r s = Some vmin \<and> (\<forall>v \<in> LV r s. vmin :\<sqsubseteq>val v)"
|
|
|
734 |
using Least_existence[OF assms] assms
|
|
|
735 |
using PosOrdeq_antisym
|
|
|
736 |
using PosOrd_Posix PosOrd_ex_eq2 lexer_correctness(1) by auto
|
|
|
737 |
|
|
|
738 |
|
|
|
739 |
lemma Least_existence1_pre:
|
|
|
740 |
assumes "LV r s \<noteq> {}"
|
|
|
741 |
shows " \<exists>!vmin \<in> LV r s. \<forall>v \<in> (LV r s \<union> {v'. flat v' \<sqsubset>spre s}). vmin :\<sqsubseteq>val v"
|
|
|
742 |
using Least_existence[OF assms] assms
|
|
|
743 |
apply -
|
|
|
744 |
apply(erule bexE)
|
|
|
745 |
apply(rule_tac a="vmin" in ex1I)
|
|
|
746 |
apply(auto)[1]
|
|
|
747 |
apply (metis PosOrd_Posix PosOrd_ex_eq2 PosOrd_spreI PosOrdeq_antisym Posix1(2))
|
|
|
748 |
apply(auto)[1]
|
|
|
749 |
apply(simp add: PosOrdeq_antisym)
|
|
|
750 |
done
|
|
|
751 |
|
|
|
752 |
lemma
|
|
|
753 |
shows "partial_order_on UNIV {(v1, v2). v1 :\<sqsubseteq>val v2}"
|
|
|
754 |
apply(simp add: partial_order_on_def)
|
|
|
755 |
apply(simp add: preorder_on_def refl_on_def)
|
|
|
756 |
apply(simp add: PosOrdeq_refl)
|
|
|
757 |
apply(auto)
|
|
|
758 |
apply(rule transI)
|
|
|
759 |
apply(auto intro: PosOrdeq_trans)[1]
|
|
|
760 |
apply(rule antisymI)
|
|
|
761 |
apply(simp add: PosOrdeq_antisym)
|
|
|
762 |
done
|
|
|
763 |
|
|
|
764 |
lemma
|
|
|
765 |
"wf {(v1, v2). v1 :\<sqsubset>val v2 \<and> v1 \<in> LV r s \<and> v2 \<in> LV r s}"
|
|
|
766 |
apply(rule finite_acyclic_wf)
|
|
|
767 |
prefer 2
|
|
|
768 |
apply(simp add: acyclic_def)
|
|
|
769 |
apply(induct_tac rule: trancl.induct)
|
|
|
770 |
apply(auto)[1]
|
|
|
771 |
oops
|
|
|
772 |
|
|
|
773 |
|
|
|
774 |
unused_thms
|
|
|
775 |
|
|
|
776 |
end |