| author | Christian Urban <urbanc@in.tum.de> |
| Fri, 18 Aug 2017 14:51:29 +0100 | |
| changeset 268 | 6746f5e1f1f8 |
| parent 267 | 32b222d77fa0 |
| child 269 | 12772d537b71 |
| permissions | -rw-r--r-- |
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1 |
|
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
2 |
theory Positions |
| 268 | 3 |
imports "Spec" "Lexer" |
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
4 |
begin |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
5 |
|
|
265
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
6 |
section {* Positions in Values *}
|
| 254 | 7 |
|
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
8 |
fun |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
9 |
at :: "val \<Rightarrow> nat list \<Rightarrow> val" |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
10 |
where |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
11 |
"at v [] = v" |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
12 |
| "at (Left v) (0#ps)= at v ps" |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
13 |
| "at (Right v) (Suc 0#ps)= at v ps" |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
14 |
| "at (Seq v1 v2) (0#ps)= at v1 ps" |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
15 |
| "at (Seq v1 v2) (Suc 0#ps)= at v2 ps" |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
16 |
| "at (Stars vs) (n#ps)= at (nth vs n) ps" |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
17 |
|
|
265
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
18 |
|
|
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
19 |
|
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
20 |
fun Pos :: "val \<Rightarrow> (nat list) set" |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
21 |
where |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
22 |
"Pos (Void) = {[]}"
|
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
23 |
| "Pos (Char c) = {[]}"
|
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
24 |
| "Pos (Left v) = {[]} \<union> {0#ps | ps. ps \<in> Pos v}"
|
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
25 |
| "Pos (Right v) = {[]} \<union> {1#ps | ps. ps \<in> Pos v}"
|
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
26 |
| "Pos (Seq v1 v2) = {[]} \<union> {0#ps | ps. ps \<in> Pos v1} \<union> {1#ps | ps. ps \<in> Pos v2}"
|
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
27 |
| "Pos (Stars []) = {[]}"
|
| 251 | 28 |
| "Pos (Stars (v#vs)) = {[]} \<union> {0#ps | ps. ps \<in> Pos v} \<union> {Suc n#ps | n ps. n#ps \<in> Pos (Stars vs)}"
|
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
29 |
|
|
265
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
30 |
|
| 253 | 31 |
lemma Pos_stars: |
32 |
"Pos (Stars vs) = {[]} \<union> (\<Union>n < length vs. {n#ps | ps. ps \<in> Pos (vs ! n)})"
|
|
33 |
apply(induct vs) |
|
| 267 | 34 |
apply(auto simp add: insert_ident less_Suc_eq_0_disj) |
35 |
done |
|
| 253 | 36 |
|
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
37 |
lemma Pos_empty: |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
38 |
shows "[] \<in> Pos v" |
| 251 | 39 |
by (induct v rule: Pos.induct)(auto) |
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
40 |
|
| 268 | 41 |
abbreviation |
42 |
"intlen vs \<equiv> int (length vs)" |
|
| 267 | 43 |
|
| 255 | 44 |
|
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
45 |
definition pflat_len :: "val \<Rightarrow> nat list => int" |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
46 |
where |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
47 |
"pflat_len v p \<equiv> (if p \<in> Pos v then intlen (flat (at v p)) else -1)" |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
48 |
|
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
49 |
lemma pflat_len_simps: |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
50 |
shows "pflat_len (Seq v1 v2) (0#p) = pflat_len v1 p" |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
51 |
and "pflat_len (Seq v1 v2) (Suc 0#p) = pflat_len v2 p" |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
52 |
and "pflat_len (Left v) (0#p) = pflat_len v p" |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
53 |
and "pflat_len (Left v) (Suc 0#p) = -1" |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
54 |
and "pflat_len (Right v) (Suc 0#p) = pflat_len v p" |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
55 |
and "pflat_len (Right v) (0#p) = -1" |
| 251 | 56 |
and "pflat_len (Stars (v#vs)) (Suc n#p) = pflat_len (Stars vs) (n#p)" |
57 |
and "pflat_len (Stars (v#vs)) (0#p) = pflat_len v p" |
|
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
58 |
and "pflat_len v [] = intlen (flat v)" |
| 251 | 59 |
by (auto simp add: pflat_len_def Pos_empty) |
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
60 |
|
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
61 |
lemma pflat_len_Stars_simps: |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
62 |
assumes "n < length vs" |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
63 |
shows "pflat_len (Stars vs) (n#p) = pflat_len (vs!n) p" |
| 267 | 64 |
using assms |
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
65 |
apply(induct vs arbitrary: n p) |
| 251 | 66 |
apply(auto simp add: less_Suc_eq_0_disj pflat_len_simps) |
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
67 |
done |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
68 |
|
|
265
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
69 |
lemma pflat_len_outside: |
|
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
70 |
assumes "p \<notin> Pos v1" |
|
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
71 |
shows "pflat_len v1 p = -1 " |
| 267 | 72 |
using assms by (simp add: pflat_len_def) |
73 |
||
| 252 | 74 |
|
75 |
||
76 |
section {* Orderings *}
|
|
77 |
||
78 |
||
| 257 | 79 |
definition prefix_list:: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" ("_ \<sqsubseteq>pre _" [60,59] 60)
|
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
80 |
where |
| 252 | 81 |
"ps1 \<sqsubseteq>pre ps2 \<equiv> \<exists>ps'. ps1 @ps' = ps2" |
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
82 |
|
| 257 | 83 |
definition sprefix_list:: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" ("_ \<sqsubset>spre _" [60,59] 60)
|
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
84 |
where |
| 252 | 85 |
"ps1 \<sqsubset>spre ps2 \<equiv> ps1 \<sqsubseteq>pre ps2 \<and> ps1 \<noteq> ps2" |
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
86 |
|
| 257 | 87 |
inductive lex_list :: "nat list \<Rightarrow> nat list \<Rightarrow> bool" ("_ \<sqsubset>lex _" [60,59] 60)
|
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
88 |
where |
| 252 | 89 |
"[] \<sqsubset>lex (p#ps)" |
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
90 |
| "ps1 \<sqsubset>lex ps2 \<Longrightarrow> (p#ps1) \<sqsubset>lex (p#ps2)" |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
91 |
| "p1 < p2 \<Longrightarrow> (p1#ps1) \<sqsubset>lex (p2#ps2)" |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
92 |
|
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
93 |
lemma lex_irrfl: |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
94 |
fixes ps1 ps2 :: "nat list" |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
95 |
assumes "ps1 \<sqsubset>lex ps2" |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
96 |
shows "ps1 \<noteq> ps2" |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
97 |
using assms |
| 257 | 98 |
by(induct rule: lex_list.induct)(auto) |
99 |
||
| 251 | 100 |
lemma lex_simps [simp]: |
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
101 |
fixes xs ys :: "nat list" |
| 251 | 102 |
shows "[] \<sqsubset>lex ys \<longleftrightarrow> ys \<noteq> []" |
103 |
and "xs \<sqsubset>lex [] \<longleftrightarrow> False" |
|
|
265
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
104 |
and "(x # xs) \<sqsubset>lex (y # ys) \<longleftrightarrow> (x < y \<or> (x = y \<and> xs \<sqsubset>lex ys))" |
|
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
105 |
by (auto simp add: neq_Nil_conv elim: lex_list.cases intro: lex_list.intros) |
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
106 |
|
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
107 |
lemma lex_trans: |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
108 |
fixes ps1 ps2 ps3 :: "nat list" |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
109 |
assumes "ps1 \<sqsubset>lex ps2" "ps2 \<sqsubset>lex ps3" |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
110 |
shows "ps1 \<sqsubset>lex ps3" |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
111 |
using assms |
| 264 | 112 |
by (induct arbitrary: ps3 rule: lex_list.induct) |
113 |
(auto elim: lex_list.cases) |
|
114 |
||
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
115 |
|
| 257 | 116 |
lemma lex_trichotomous: |
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
117 |
fixes p q :: "nat list" |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
118 |
shows "p = q \<or> p \<sqsubset>lex q \<or> q \<sqsubset>lex p" |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
119 |
apply(induct p arbitrary: q) |
|
265
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
120 |
apply(auto elim: lex_list.cases) |
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
121 |
apply(case_tac q) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
122 |
apply(auto) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
123 |
done |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
124 |
|
| 254 | 125 |
|
126 |
||
127 |
||
|
265
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
128 |
section {* POSIX Ordering of Values According to Okui & Suzuki *}
|
| 254 | 129 |
|
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
130 |
|
| 261 | 131 |
definition PosOrd:: "val \<Rightarrow> nat list \<Rightarrow> val \<Rightarrow> bool" ("_ \<sqsubset>val _ _" [60, 60, 59] 60)
|
132 |
where |
|
| 264 | 133 |
"v1 \<sqsubset>val p v2 \<equiv> pflat_len v1 p > pflat_len v2 p \<and> |
134 |
(\<forall>q \<in> Pos v1 \<union> Pos v2. q \<sqsubset>lex p \<longrightarrow> pflat_len v1 q = pflat_len v2 q)" |
|
135 |
||
|
265
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
136 |
|
| 261 | 137 |
|
138 |
definition PosOrd_ex:: "val \<Rightarrow> val \<Rightarrow> bool" ("_ :\<sqsubset>val _" [60, 59] 60)
|
|
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
139 |
where |
|
265
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
140 |
"v1 :\<sqsubset>val v2 \<equiv> \<exists>p. v1 \<sqsubset>val p v2" |
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
141 |
|
|
265
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
142 |
definition PosOrd_ex_eq:: "val \<Rightarrow> val \<Rightarrow> bool" ("_ :\<sqsubseteq>val _" [60, 59] 60)
|
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
143 |
where |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
144 |
"v1 :\<sqsubseteq>val v2 \<equiv> v1 :\<sqsubset>val v2 \<or> v1 = v2" |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
145 |
|
|
265
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
146 |
|
| 268 | 147 |
lemma PosOrd_trans: |
148 |
assumes "v1 :\<sqsubset>val v2" "v2 :\<sqsubset>val v3" |
|
149 |
shows "v1 :\<sqsubset>val v3" |
|
150 |
proof - |
|
151 |
from assms obtain p p' |
|
152 |
where as: "v1 \<sqsubset>val p v2" "v2 \<sqsubset>val p' v3" unfolding PosOrd_ex_def by blast |
|
153 |
then have pos: "p \<in> Pos v1" "p' \<in> Pos v2" unfolding PosOrd_def pflat_len_def |
|
154 |
by (smt not_int_zless_negative)+ |
|
155 |
have "p = p' \<or> p \<sqsubset>lex p' \<or> p' \<sqsubset>lex p" |
|
156 |
by (rule lex_trichotomous) |
|
157 |
moreover |
|
158 |
{ assume "p = p'"
|
|
159 |
with as have "v1 \<sqsubset>val p v3" unfolding PosOrd_def pflat_len_def |
|
160 |
by (smt Un_iff) |
|
161 |
then have " v1 :\<sqsubset>val v3" unfolding PosOrd_ex_def by blast |
|
162 |
} |
|
163 |
moreover |
|
164 |
{ assume "p \<sqsubset>lex p'"
|
|
165 |
with as have "v1 \<sqsubset>val p v3" unfolding PosOrd_def pflat_len_def |
|
166 |
by (smt Un_iff lex_trans) |
|
167 |
then have " v1 :\<sqsubset>val v3" unfolding PosOrd_ex_def by blast |
|
168 |
} |
|
169 |
moreover |
|
170 |
{ assume "p' \<sqsubset>lex p"
|
|
171 |
with as have "v1 \<sqsubset>val p' v3" unfolding PosOrd_def |
|
172 |
by (smt Un_iff lex_trans pflat_len_def) |
|
173 |
then have "v1 :\<sqsubset>val v3" unfolding PosOrd_ex_def by blast |
|
174 |
} |
|
175 |
ultimately show "v1 :\<sqsubset>val v3" by blast |
|
176 |
qed |
|
177 |
||
178 |
lemma PosOrd_irrefl: |
|
179 |
assumes "v :\<sqsubset>val v" |
|
180 |
shows "False" |
|
181 |
using assms unfolding PosOrd_ex_def PosOrd_def |
|
182 |
by auto |
|
183 |
||
184 |
lemma PosOrd_assym: |
|
185 |
assumes "v1 :\<sqsubset>val v2" |
|
186 |
shows "\<not>(v2 :\<sqsubset>val v1)" |
|
187 |
using assms |
|
188 |
using PosOrd_irrefl PosOrd_trans by blast |
|
189 |
||
190 |
text {*
|
|
191 |
:\<sqsubseteq>val and :\<sqsubset>val are partial orders. |
|
192 |
*} |
|
193 |
||
194 |
lemma PosOrd_ordering: |
|
195 |
shows "ordering (\<lambda>v1 v2. v1 :\<sqsubseteq>val v2) (\<lambda> v1 v2. v1 :\<sqsubset>val v2)" |
|
196 |
unfolding ordering_def PosOrd_ex_eq_def |
|
197 |
apply(auto) |
|
198 |
using PosOrd_irrefl apply blast |
|
199 |
using PosOrd_assym apply blast |
|
200 |
using PosOrd_trans by blast |
|
201 |
||
202 |
lemma PosOrd_order: |
|
203 |
shows "class.order (\<lambda>v1 v2. v1 :\<sqsubseteq>val v2) (\<lambda> v1 v2. v1 :\<sqsubset>val v2)" |
|
204 |
using PosOrd_ordering |
|
205 |
apply(simp add: class.order_def class.preorder_def class.order_axioms_def) |
|
206 |
unfolding ordering_def |
|
207 |
by blast |
|
208 |
||
209 |
||
210 |
lemma PosOrd_ex_eq2: |
|
211 |
shows "v1 :\<sqsubset>val v2 \<longleftrightarrow> (v1 :\<sqsubseteq>val v2 \<and> v1 \<noteq> v2)" |
|
212 |
using PosOrd_ordering |
|
213 |
unfolding ordering_def |
|
214 |
by auto |
|
215 |
||
216 |
lemma PosOrdeq_trans: |
|
217 |
assumes "v1 :\<sqsubseteq>val v2" "v2 :\<sqsubseteq>val v3" |
|
218 |
shows "v1 :\<sqsubseteq>val v3" |
|
219 |
using assms PosOrd_ordering |
|
220 |
unfolding ordering_def |
|
221 |
by blast |
|
222 |
||
223 |
lemma PosOrdeq_antisym: |
|
224 |
assumes "v1 :\<sqsubseteq>val v2" "v2 :\<sqsubseteq>val v1" |
|
225 |
shows "v1 = v2" |
|
226 |
using assms PosOrd_ordering |
|
227 |
unfolding ordering_def |
|
228 |
by blast |
|
229 |
||
230 |
lemma PosOrdeq_refl: |
|
231 |
shows "v :\<sqsubseteq>val v" |
|
232 |
unfolding PosOrd_ex_eq_def |
|
233 |
by auto |
|
234 |
||
235 |
||
236 |
||
237 |
||
| 261 | 238 |
lemma PosOrd_shorterE: |
| 255 | 239 |
assumes "v1 :\<sqsubset>val v2" |
240 |
shows "length (flat v2) \<le> length (flat v1)" |
|
| 267 | 241 |
using assms unfolding PosOrd_ex_def PosOrd_def |
| 268 | 242 |
apply(auto simp add: pflat_len_def split: if_splits) |
| 267 | 243 |
apply (metis Pos_empty Un_iff at.simps(1) eq_iff lex_simps(1) nat_less_le) |
244 |
by (metis Pos_empty UnI2 at.simps(1) lex_simps(2) lex_trichotomous linear) |
|
| 255 | 245 |
|
| 261 | 246 |
lemma PosOrd_shorterI: |
|
265
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
247 |
assumes "length (flat v2) < length (flat v1)" |
| 268 | 248 |
shows "v1 :\<sqsubset>val v2" |
249 |
unfolding PosOrd_ex_def PosOrd_def pflat_len_def |
|
250 |
using assms Pos_empty by force |
|
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
251 |
|
| 261 | 252 |
lemma PosOrd_spreI: |
|
265
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
253 |
assumes "flat v' \<sqsubset>spre flat v" |
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
254 |
shows "v :\<sqsubset>val v'" |
| 251 | 255 |
using assms |
| 261 | 256 |
apply(rule_tac PosOrd_shorterI) |
| 268 | 257 |
unfolding prefix_list_def sprefix_list_def |
258 |
by (metis append_Nil2 append_eq_conv_conj drop_all le_less_linear) |
|
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
259 |
|
|
265
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
260 |
|
| 261 | 261 |
lemma PosOrd_Left_Right: |
262 |
assumes "flat v1 = flat v2" |
|
263 |
shows "Left v1 :\<sqsubset>val Right v2" |
|
264 |
unfolding PosOrd_ex_def |
|
265 |
apply(rule_tac x="[0]" in exI) |
|
|
265
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
266 |
using assms |
| 268 | 267 |
apply(auto simp add: PosOrd_def pflat_len_simps) |
| 261 | 268 |
done |
| 256 | 269 |
|
|
265
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
270 |
lemma PosOrd_Left_eq: |
|
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
271 |
assumes "flat v = flat v'" |
|
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
272 |
shows "Left v :\<sqsubset>val Left v' \<longleftrightarrow> v :\<sqsubset>val v'" |
|
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
273 |
using assms |
| 261 | 274 |
unfolding PosOrd_ex_def |
| 251 | 275 |
apply(auto) |
|
265
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
276 |
apply(case_tac p) |
|
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
277 |
apply(simp add: PosOrd_def pflat_len_simps) |
|
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
278 |
apply(case_tac a) |
|
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
279 |
apply(simp add: PosOrd_def pflat_len_simps) |
|
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
280 |
apply(rule_tac x="list" in exI) |
|
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
281 |
apply(auto simp add: PosOrd_def pflat_len_simps)[1] |
|
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
282 |
apply (smt Un_def lex_list.intros(2) mem_Collect_eq pflat_len_simps(3)) |
|
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
283 |
apply (smt Collect_disj_eq lex_list.intros(2) mem_Collect_eq pflat_len_simps(3)) |
|
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
284 |
apply(auto simp add: PosOrd_def pflat_len_outside)[1] |
| 251 | 285 |
apply(rule_tac x="0#p" in exI) |
| 261 | 286 |
apply(auto simp add: PosOrd_def pflat_len_simps) |
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
287 |
done |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
288 |
|
|
265
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
289 |
|
| 261 | 290 |
lemma PosOrd_RightI: |
| 251 | 291 |
assumes "v :\<sqsubset>val v'" "flat v = flat v'" |
| 268 | 292 |
shows "Right v :\<sqsubset>val Right v'" |
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
293 |
using assms(1) |
| 261 | 294 |
unfolding PosOrd_ex_def |
| 251 | 295 |
apply(auto) |
296 |
apply(rule_tac x="Suc 0#p" in exI) |
|
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
297 |
using assms(2) |
| 261 | 298 |
apply(auto simp add: PosOrd_def pflat_len_simps) |
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
299 |
done |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
300 |
|
| 261 | 301 |
lemma PosOrd_RightE: |
| 268 | 302 |
assumes "Right v1 :\<sqsubset>val Right v2" |
| 252 | 303 |
shows "v1 :\<sqsubset>val v2" |
304 |
using assms |
|
| 261 | 305 |
apply(simp add: PosOrd_ex_def) |
| 252 | 306 |
apply(erule exE) |
| 264 | 307 |
apply(case_tac p) |
| 261 | 308 |
apply(simp add: PosOrd_def) |
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
309 |
apply(auto simp add: pflat_len_simps) |
| 252 | 310 |
apply(rule_tac x="[]" in exI) |
311 |
apply(simp add: Pos_empty pflat_len_simps) |
|
| 264 | 312 |
apply(case_tac a) |
313 |
apply(simp add: pflat_len_def PosOrd_def) |
|
314 |
apply(case_tac nat) |
|
315 |
prefer 2 |
|
316 |
apply(simp add: pflat_len_def PosOrd_def) |
|
| 261 | 317 |
apply(auto simp add: pflat_len_simps PosOrd_def) |
| 264 | 318 |
apply(rule_tac x="list" in exI) |
| 252 | 319 |
apply(auto) |
320 |
apply(drule_tac x="Suc 0#q" in bspec) |
|
321 |
apply(simp) |
|
322 |
apply(simp add: pflat_len_simps) |
|
323 |
apply(drule_tac x="Suc 0#q" in bspec) |
|
324 |
apply(simp) |
|
325 |
apply(simp add: pflat_len_simps) |
|
326 |
done |
|
327 |
||
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
328 |
|
| 261 | 329 |
lemma PosOrd_SeqI1: |
| 252 | 330 |
assumes "v1 :\<sqsubset>val v1'" "flat (Seq v1 v2) = flat (Seq v1' v2')" |
| 268 | 331 |
shows "Seq v1 v2 :\<sqsubset>val Seq v1' v2'" |
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
332 |
using assms(1) |
| 261 | 333 |
apply(subst (asm) PosOrd_ex_def) |
334 |
apply(subst (asm) PosOrd_def) |
|
| 252 | 335 |
apply(clarify) |
| 261 | 336 |
apply(subst PosOrd_ex_def) |
| 252 | 337 |
apply(rule_tac x="0#p" in exI) |
| 261 | 338 |
apply(subst PosOrd_def) |
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
339 |
apply(rule conjI) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
340 |
apply(simp add: pflat_len_simps) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
341 |
apply(rule ballI) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
342 |
apply(rule impI) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
343 |
apply(simp only: Pos.simps) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
344 |
apply(auto)[1] |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
345 |
apply(simp add: pflat_len_simps) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
346 |
using assms(2) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
347 |
apply(simp) |
| 268 | 348 |
apply(auto simp add: pflat_len_simps) |
349 |
by (metis length_append of_nat_add) |
|
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
350 |
|
| 261 | 351 |
lemma PosOrd_SeqI2: |
| 252 | 352 |
assumes "v2 :\<sqsubset>val v2'" "flat v2 = flat v2'" |
| 268 | 353 |
shows "Seq v v2 :\<sqsubset>val Seq v v2'" |
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
354 |
using assms(1) |
| 261 | 355 |
apply(subst (asm) PosOrd_ex_def) |
356 |
apply(subst (asm) PosOrd_def) |
|
| 252 | 357 |
apply(clarify) |
| 261 | 358 |
apply(subst PosOrd_ex_def) |
| 252 | 359 |
apply(rule_tac x="Suc 0#p" in exI) |
| 261 | 360 |
apply(subst PosOrd_def) |
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
361 |
apply(rule conjI) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
362 |
apply(simp add: pflat_len_simps) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
363 |
apply(rule ballI) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
364 |
apply(rule impI) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
365 |
apply(simp only: Pos.simps) |
| 252 | 366 |
apply(auto)[1] |
367 |
apply(simp add: pflat_len_simps) |
|
368 |
using assms(2) |
|
369 |
apply(simp) |
|
370 |
apply(auto simp add: pflat_len_simps) |
|
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
371 |
done |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
372 |
|
| 261 | 373 |
lemma PosOrd_SeqE: |
| 268 | 374 |
assumes "Seq v1 v2 :\<sqsubset>val Seq v1' v2'" |
| 254 | 375 |
shows "v1 :\<sqsubset>val v1' \<or> v2 :\<sqsubset>val v2'" |
376 |
using assms |
|
| 261 | 377 |
apply(simp add: PosOrd_ex_def) |
| 254 | 378 |
apply(erule exE) |
379 |
apply(case_tac p) |
|
| 261 | 380 |
apply(simp add: PosOrd_def) |
| 268 | 381 |
apply(auto simp add: pflat_len_simps)[1] |
| 254 | 382 |
apply(rule_tac x="[]" in exI) |
383 |
apply(drule_tac x="[]" in spec) |
|
384 |
apply(simp add: Pos_empty pflat_len_simps) |
|
385 |
apply(case_tac a) |
|
386 |
apply(rule disjI1) |
|
| 261 | 387 |
apply(simp add: PosOrd_def) |
| 268 | 388 |
apply(auto simp add: pflat_len_simps)[1] |
| 254 | 389 |
apply(rule_tac x="list" in exI) |
390 |
apply(simp) |
|
391 |
apply(rule ballI) |
|
392 |
apply(rule impI) |
|
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
393 |
apply(drule_tac x="0#q" in bspec) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
394 |
apply(simp) |
| 254 | 395 |
apply(simp add: pflat_len_simps) |
396 |
apply(case_tac nat) |
|
397 |
apply(rule disjI2) |
|
| 261 | 398 |
apply(simp add: PosOrd_def) |
| 268 | 399 |
apply(auto simp add: pflat_len_simps) |
| 254 | 400 |
apply(rule_tac x="list" in exI) |
401 |
apply(simp add: Pos_empty) |
|
402 |
apply(rule ballI) |
|
403 |
apply(rule impI) |
|
| 264 | 404 |
apply(auto)[1] |
| 254 | 405 |
apply(drule_tac x="Suc 0#q" in bspec) |
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
406 |
apply(simp) |
| 254 | 407 |
apply(simp add: pflat_len_simps) |
| 264 | 408 |
apply(drule_tac x="Suc 0#q" in bspec) |
409 |
apply(simp) |
|
410 |
apply(simp add: pflat_len_simps) |
|
411 |
apply(simp add: PosOrd_def pflat_len_def) |
|
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
412 |
done |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
413 |
|
| 261 | 414 |
lemma PosOrd_StarsI: |
| 268 | 415 |
assumes "v1 :\<sqsubset>val v2" "flats (v1#vs1) = flats (v2#vs2)" |
416 |
shows "Stars (v1#vs1) :\<sqsubset>val Stars (v2#vs2)" |
|
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
417 |
using assms(1) |
| 261 | 418 |
apply(subst (asm) PosOrd_ex_def) |
419 |
apply(subst (asm) PosOrd_def) |
|
| 254 | 420 |
apply(clarify) |
| 261 | 421 |
apply(subst PosOrd_ex_def) |
422 |
apply(subst PosOrd_def) |
|
| 254 | 423 |
apply(rule_tac x="0#p" in exI) |
424 |
apply(simp add: pflat_len_Stars_simps pflat_len_simps) |
|
425 |
using assms(2) |
|
| 268 | 426 |
apply(simp add: pflat_len_simps) |
| 254 | 427 |
apply(auto simp add: pflat_len_Stars_simps pflat_len_simps) |
| 268 | 428 |
by (metis length_append of_nat_add) |
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
429 |
|
| 261 | 430 |
lemma PosOrd_StarsI2: |
| 268 | 431 |
assumes "Stars vs1 :\<sqsubset>val Stars vs2" "flats vs1 = flats vs2" |
432 |
shows "Stars (v#vs1) :\<sqsubset>val Stars (v#vs2)" |
|
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
433 |
using assms(1) |
| 261 | 434 |
apply(subst (asm) PosOrd_ex_def) |
435 |
apply(subst (asm) PosOrd_def) |
|
| 254 | 436 |
apply(clarify) |
| 261 | 437 |
apply(subst PosOrd_ex_def) |
438 |
apply(subst PosOrd_def) |
|
| 254 | 439 |
apply(case_tac p) |
440 |
apply(simp add: pflat_len_simps) |
|
441 |
apply(rule_tac x="Suc a#list" in exI) |
|
| 268 | 442 |
apply(auto simp add: pflat_len_Stars_simps pflat_len_simps assms(2)) |
| 254 | 443 |
done |
444 |
||
| 261 | 445 |
lemma PosOrd_Stars_appendI: |
| 254 | 446 |
assumes "Stars vs1 :\<sqsubset>val Stars vs2" "flat (Stars vs1) = flat (Stars vs2)" |
447 |
shows "Stars (vs @ vs1) :\<sqsubset>val Stars (vs @ vs2)" |
|
448 |
using assms |
|
449 |
apply(induct vs) |
|
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
450 |
apply(simp) |
| 261 | 451 |
apply(simp add: PosOrd_StarsI2) |
| 254 | 452 |
done |
453 |
||
| 261 | 454 |
lemma PosOrd_StarsE2: |
| 254 | 455 |
assumes "Stars (v # vs1) :\<sqsubset>val Stars (v # vs2)" |
456 |
shows "Stars vs1 :\<sqsubset>val Stars vs2" |
|
457 |
using assms |
|
| 261 | 458 |
apply(subst (asm) PosOrd_ex_def) |
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
459 |
apply(erule exE) |
| 254 | 460 |
apply(case_tac p) |
461 |
apply(simp) |
|
| 268 | 462 |
apply(simp add: PosOrd_def pflat_len_simps) |
| 261 | 463 |
apply(subst PosOrd_ex_def) |
| 254 | 464 |
apply(rule_tac x="[]" in exI) |
| 261 | 465 |
apply(simp add: PosOrd_def pflat_len_simps Pos_empty) |
| 254 | 466 |
apply(simp) |
467 |
apply(case_tac a) |
|
468 |
apply(clarify) |
|
| 264 | 469 |
apply(auto simp add: pflat_len_simps PosOrd_def pflat_len_def split: if_splits)[1] |
| 254 | 470 |
apply(clarify) |
| 261 | 471 |
apply(simp add: PosOrd_ex_def) |
| 254 | 472 |
apply(rule_tac x="nat#list" in exI) |
| 268 | 473 |
apply(auto simp add: PosOrd_def pflat_len_simps)[1] |
| 254 | 474 |
apply(case_tac q) |
| 268 | 475 |
apply(simp add: PosOrd_def pflat_len_simps) |
| 254 | 476 |
apply(clarify) |
477 |
apply(drule_tac x="Suc a # lista" in bspec) |
|
478 |
apply(simp) |
|
| 268 | 479 |
apply(auto simp add: PosOrd_def pflat_len_simps)[1] |
| 254 | 480 |
apply(case_tac q) |
| 268 | 481 |
apply(simp add: PosOrd_def pflat_len_simps) |
| 254 | 482 |
apply(clarify) |
483 |
apply(drule_tac x="Suc a # lista" in bspec) |
|
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
484 |
apply(simp) |
| 268 | 485 |
apply(auto simp add: PosOrd_def pflat_len_simps)[1] |
| 254 | 486 |
done |
487 |
||
| 261 | 488 |
lemma PosOrd_Stars_appendE: |
| 254 | 489 |
assumes "Stars (vs @ vs1) :\<sqsubset>val Stars (vs @ vs2)" |
490 |
shows "Stars vs1 :\<sqsubset>val Stars vs2" |
|
491 |
using assms |
|
492 |
apply(induct vs) |
|
493 |
apply(simp) |
|
| 261 | 494 |
apply(simp add: PosOrd_StarsE2) |
| 254 | 495 |
done |
496 |
||
| 261 | 497 |
lemma PosOrd_Stars_append_eq: |
| 254 | 498 |
assumes "flat (Stars vs1) = flat (Stars vs2)" |
499 |
shows "Stars (vs @ vs1) :\<sqsubset>val Stars (vs @ vs2) \<longleftrightarrow> Stars vs1 :\<sqsubset>val Stars vs2" |
|
500 |
using assms |
|
501 |
apply(rule_tac iffI) |
|
| 261 | 502 |
apply(erule PosOrd_Stars_appendE) |
503 |
apply(rule PosOrd_Stars_appendI) |
|
| 254 | 504 |
apply(auto) |
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
505 |
done |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
506 |
|
| 261 | 507 |
lemma PosOrd_almost_trichotomous: |
| 256 | 508 |
shows "v1 :\<sqsubset>val v2 \<or> v2 :\<sqsubset>val v1 \<or> (intlen (flat v1) = intlen (flat v2))" |
| 261 | 509 |
apply(auto simp add: PosOrd_ex_def) |
510 |
apply(auto simp add: PosOrd_def) |
|
| 256 | 511 |
apply(rule_tac x="[]" in exI) |
512 |
apply(auto simp add: Pos_empty pflat_len_simps) |
|
513 |
apply(drule_tac x="[]" in spec) |
|
514 |
apply(auto simp add: Pos_empty pflat_len_simps) |
|
515 |
done |
|
516 |
||
517 |
||
| 261 | 518 |
lemma PosOrd_SeqE2: |
|
265
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
519 |
assumes "(Seq v1 v2) :\<sqsubset>val (Seq v1' v2')" "flat (Seq v1 v2) = flat (Seq v1' v2')" |
|
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
520 |
shows "v1 :\<sqsubset>val v1' \<or> (intlen (flat v1) = intlen (flat v1') \<and> v2 :\<sqsubset>val v2')" |
| 256 | 521 |
using assms |
| 261 | 522 |
apply(frule_tac PosOrd_SeqE) |
| 256 | 523 |
apply(erule disjE) |
524 |
apply(simp) |
|
525 |
apply(case_tac "v1 :\<sqsubset>val v1'") |
|
526 |
apply(simp) |
|
|
265
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
527 |
apply(rule disjI2) |
|
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
528 |
apply(rule conjI) |
|
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
529 |
prefer 2 |
|
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
530 |
apply(simp) |
|
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
531 |
apply(auto) |
| 261 | 532 |
apply(auto simp add: PosOrd_ex_def) |
|
265
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
533 |
apply(auto simp add: PosOrd_def pflat_len_simps) |
|
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
534 |
apply(case_tac p) |
|
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
535 |
apply(auto simp add: PosOrd_def pflat_len_simps) |
|
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
536 |
apply(case_tac a) |
|
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
537 |
apply(auto simp add: PosOrd_def pflat_len_simps) |
| 268 | 538 |
apply (metis PosOrd_SeqI1 PosOrd_def PosOrd_ex_def PosOrd_shorterI PosOrd_assym assms less_linear) |
539 |
by (metis PosOrd_SeqI1 PosOrd_almost_trichotomous PosOrd_def PosOrd_ex_def PosOrd_assym assms of_nat_eq_iff) |
|
|
265
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
540 |
|
|
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
541 |
lemma PosOrd_SeqE4: |
|
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
542 |
assumes "(Seq v1 v2) :\<sqsubset>val (Seq v1' v2')" "flat (Seq v1 v2) = flat (Seq v1' v2')" |
|
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
543 |
shows "v1 :\<sqsubset>val v1' \<or> (flat v1 = flat v1' \<and> v2 :\<sqsubset>val v2')" |
|
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
544 |
using assms |
|
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
545 |
apply(frule_tac PosOrd_SeqE) |
|
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
546 |
apply(erule disjE) |
| 256 | 547 |
apply(simp) |
|
265
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
548 |
apply(case_tac "v1 :\<sqsubset>val v1'") |
|
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
549 |
apply(simp) |
|
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
550 |
apply(rule disjI2) |
|
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
551 |
apply(rule conjI) |
|
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
552 |
prefer 2 |
|
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
553 |
apply(simp) |
|
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
554 |
apply(auto) |
|
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
555 |
apply(case_tac "length (flat v1') < length (flat v1)") |
|
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
556 |
using PosOrd_shorterI apply blast |
| 268 | 557 |
by (metis PosOrd_SeqI1 PosOrd_shorterI PosOrd_assym antisym_conv3 append_eq_append_conv assms(2)) |
|
265
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
558 |
|
| 254 | 559 |
|
| 267 | 560 |
|
| 261 | 561 |
section {* The Posix Value is smaller than any other Value *}
|
562 |
||
| 262 | 563 |
|
| 261 | 564 |
lemma Posix_PosOrd: |
| 268 | 565 |
assumes "s \<in> r \<rightarrow> v1" "v2 \<in> LV r s" |
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
566 |
shows "v1 :\<sqsubseteq>val v2" |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
567 |
using assms |
| 261 | 568 |
proof (induct arbitrary: v2 rule: Posix.induct) |
569 |
case (Posix_ONE v) |
|
| 268 | 570 |
have "v \<in> LV ONE []" by fact |
| 262 | 571 |
then have "v = Void" |
| 268 | 572 |
by (simp add: LV_simps) |
| 261 | 573 |
then show "Void :\<sqsubseteq>val v" |
|
265
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
574 |
by (simp add: PosOrd_ex_eq_def) |
| 261 | 575 |
next |
576 |
case (Posix_CHAR c v) |
|
| 268 | 577 |
have "v \<in> LV (CHAR c) [c]" by fact |
| 262 | 578 |
then have "v = Char c" |
| 268 | 579 |
by (simp add: LV_simps) |
| 261 | 580 |
then show "Char c :\<sqsubseteq>val v" |
|
265
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
581 |
by (simp add: PosOrd_ex_eq_def) |
| 261 | 582 |
next |
583 |
case (Posix_ALT1 s r1 v r2 v2) |
|
584 |
have as1: "s \<in> r1 \<rightarrow> v" by fact |
|
| 268 | 585 |
have IH: "\<And>v2. v2 \<in> LV r1 s \<Longrightarrow> v :\<sqsubseteq>val v2" by fact |
586 |
have "v2 \<in> LV (ALT r1 r2) s" by fact |
|
| 262 | 587 |
then have "\<Turnstile> v2 : ALT r1 r2" "flat v2 = s" |
| 268 | 588 |
by(auto simp add: LV_def prefix_list_def) |
| 261 | 589 |
then consider |
| 262 | 590 |
(Left) v3 where "v2 = Left v3" "\<Turnstile> v3 : r1" "flat v3 = s" |
591 |
| (Right) v3 where "v2 = Right v3" "\<Turnstile> v3 : r2" "flat v3 = s" |
|
| 268 | 592 |
by (auto elim: Prf.cases) |
| 261 | 593 |
then show "Left v :\<sqsubseteq>val v2" |
594 |
proof(cases) |
|
595 |
case (Left v3) |
|
| 268 | 596 |
have "v3 \<in> LV r1 s" using Left(2,3) |
597 |
by (auto simp add: LV_def prefix_list_def) |
|
| 261 | 598 |
with IH have "v :\<sqsubseteq>val v3" by simp |
599 |
moreover |
|
| 262 | 600 |
have "flat v3 = flat v" using as1 Left(3) |
601 |
by (simp add: Posix1(2)) |
|
| 261 | 602 |
ultimately have "Left v :\<sqsubseteq>val Left v3" |
|
265
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
603 |
by (simp add: PosOrd_ex_eq_def PosOrd_Left_eq) |
| 261 | 604 |
then show "Left v :\<sqsubseteq>val v2" unfolding Left . |
605 |
next |
|
606 |
case (Right v3) |
|
| 262 | 607 |
have "flat v3 = flat v" using as1 Right(3) |
608 |
by (simp add: Posix1(2)) |
|
| 268 | 609 |
then have "Left v :\<sqsubseteq>val Right v3" |
610 |
unfolding PosOrd_ex_eq_def |
|
611 |
by (simp add: PosOrd_Left_Right) |
|
| 261 | 612 |
then show "Left v :\<sqsubseteq>val v2" unfolding Right . |
613 |
qed |
|
614 |
next |
|
615 |
case (Posix_ALT2 s r2 v r1 v2) |
|
616 |
have as1: "s \<in> r2 \<rightarrow> v" by fact |
|
617 |
have as2: "s \<notin> L r1" by fact |
|
| 268 | 618 |
have IH: "\<And>v2. v2 \<in> LV r2 s \<Longrightarrow> v :\<sqsubseteq>val v2" by fact |
619 |
have "v2 \<in> LV (ALT r1 r2) s" by fact |
|
| 262 | 620 |
then have "\<Turnstile> v2 : ALT r1 r2" "flat v2 = s" |
| 268 | 621 |
by(auto simp add: LV_def prefix_list_def) |
| 261 | 622 |
then consider |
| 262 | 623 |
(Left) v3 where "v2 = Left v3" "\<Turnstile> v3 : r1" "flat v3 = s" |
624 |
| (Right) v3 where "v2 = Right v3" "\<Turnstile> v3 : r2" "flat v3 = s" |
|
| 268 | 625 |
by (auto elim: Prf.cases) |
| 261 | 626 |
then show "Right v :\<sqsubseteq>val v2" |
627 |
proof (cases) |
|
628 |
case (Right v3) |
|
| 268 | 629 |
have "v3 \<in> LV r2 s" using Right(2,3) |
630 |
by (auto simp add: LV_def prefix_list_def) |
|
| 261 | 631 |
with IH have "v :\<sqsubseteq>val v3" by simp |
632 |
moreover |
|
| 262 | 633 |
have "flat v3 = flat v" using as1 Right(3) |
634 |
by (simp add: Posix1(2)) |
|
| 261 | 635 |
ultimately have "Right v :\<sqsubseteq>val Right v3" |
|
265
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
636 |
by (auto simp add: PosOrd_ex_eq_def PosOrd_RightI) |
| 261 | 637 |
then show "Right v :\<sqsubseteq>val v2" unfolding Right . |
638 |
next |
|
639 |
case (Left v3) |
|
| 268 | 640 |
have "v3 \<in> LV r1 s" using Left(2,3) as2 |
641 |
by (auto simp add: LV_def prefix_list_def) |
|
| 262 | 642 |
then have "flat v3 = flat v \<and> \<Turnstile> v3 : r1" using as1 Left(3) |
| 268 | 643 |
by (simp add: Posix1(2) LV_def) |
| 262 | 644 |
then have "False" using as1 as2 Left |
| 268 | 645 |
by (auto simp add: Posix1(2) L_flat_Prf1) |
| 262 | 646 |
then show "Right v :\<sqsubseteq>val v2" by simp |
| 261 | 647 |
qed |
648 |
next |
|
649 |
case (Posix_SEQ s1 r1 v1 s2 r2 v2 v3) |
|
| 264 | 650 |
have "s1 \<in> r1 \<rightarrow> v1" "s2 \<in> r2 \<rightarrow> v2" by fact+ |
651 |
then have as1: "s1 = flat v1" "s2 = flat v2" by (simp_all add: Posix1(2)) |
|
| 268 | 652 |
have IH1: "\<And>v3. v3 \<in> LV r1 s1 \<Longrightarrow> v1 :\<sqsubseteq>val v3" by fact |
653 |
have IH2: "\<And>v3. v3 \<in> LV r2 s2 \<Longrightarrow> v2 :\<sqsubseteq>val v3" by fact |
|
| 261 | 654 |
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 |
| 268 | 655 |
have "v3 \<in> LV (SEQ r1 r2) (s1 @ s2)" by fact |
| 261 | 656 |
then obtain v3a v3b where eqs: |
657 |
"v3 = Seq v3a v3b" "\<Turnstile> v3a : r1" "\<Turnstile> v3b : r2" |
|
| 262 | 658 |
"flat v3a @ flat v3b = s1 @ s2" |
| 268 | 659 |
by (force simp add: prefix_list_def LV_def elim: Prf.cases) |
| 262 | 660 |
with cond have "flat v3a \<sqsubseteq>pre s1" unfolding prefix_list_def |
| 268 | 661 |
by (smt L_flat_Prf1 append_eq_append_conv2 append_self_conv) |
| 262 | 662 |
then have "flat v3a \<sqsubset>spre s1 \<or> (flat v3a = s1 \<and> flat v3b = s2)" using eqs |
663 |
by (simp add: sprefix_list_def append_eq_conv_conj) |
|
664 |
then have q2: "v1 :\<sqsubset>val v3a \<or> (flat v3a = s1 \<and> flat v3b = s2)" |
|
| 264 | 665 |
using PosOrd_spreI as1(1) eqs by blast |
| 268 | 666 |
then have "v1 :\<sqsubset>val v3a \<or> (v3a \<in> LV r1 s1 \<and> v3b \<in> LV r2 s2)" using eqs(2,3) |
667 |
by (auto simp add: LV_def) |
|
| 262 | 668 |
then have "v1 :\<sqsubset>val v3a \<or> (v1 :\<sqsubseteq>val v3a \<and> v2 :\<sqsubseteq>val v3b)" using IH1 IH2 by blast |
669 |
then have "Seq v1 v2 :\<sqsubseteq>val Seq v3a v3b" using eqs q2 as1 |
|
|
265
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
670 |
unfolding PosOrd_ex_eq_def by (auto simp add: PosOrd_SeqI1 PosOrd_SeqI2) |
| 262 | 671 |
then show "Seq v1 v2 :\<sqsubseteq>val v3" unfolding eqs by blast |
| 261 | 672 |
next |
673 |
case (Posix_STAR1 s1 r v s2 vs v3) |
|
| 264 | 674 |
have "s1 \<in> r \<rightarrow> v" "s2 \<in> STAR r \<rightarrow> Stars vs" by fact+ |
675 |
then have as1: "s1 = flat v" "s2 = flat (Stars vs)" by (auto dest: Posix1(2)) |
|
| 268 | 676 |
have IH1: "\<And>v3. v3 \<in> LV r s1 \<Longrightarrow> v :\<sqsubseteq>val v3" by fact |
677 |
have IH2: "\<And>v3. v3 \<in> LV (STAR r) s2 \<Longrightarrow> Stars vs :\<sqsubseteq>val v3" by fact |
|
| 261 | 678 |
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 |
679 |
have cond2: "flat v \<noteq> []" by fact |
|
| 268 | 680 |
have "v3 \<in> LV (STAR r) (s1 @ s2)" by fact |
|
265
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
681 |
then consider |
|
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
682 |
(NonEmpty) v3a vs3 where "v3 = Stars (v3a # vs3)" |
|
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
683 |
"\<Turnstile> v3a : r" "\<Turnstile> Stars vs3 : STAR r" |
| 262 | 684 |
"flat (Stars (v3a # vs3)) = s1 @ s2" |
| 261 | 685 |
| (Empty) "v3 = Stars []" |
| 268 | 686 |
unfolding LV_def |
|
265
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
687 |
apply(auto) |
| 268 | 688 |
apply(erule Prf.cases) |
|
265
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
689 |
apply(simp_all) |
|
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
690 |
apply(auto)[1] |
|
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
691 |
apply(case_tac vs) |
|
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
692 |
apply(auto) |
| 268 | 693 |
using Prf.intros(6) by blast |
694 |
then show "Stars (v # vs) :\<sqsubseteq>val v3" |
|
| 261 | 695 |
proof (cases) |
696 |
case (NonEmpty v3a vs3) |
|
| 262 | 697 |
have "flat (Stars (v3a # vs3)) = s1 @ s2" using NonEmpty(4) . |
698 |
with cond have "flat v3a \<sqsubseteq>pre s1" using NonEmpty(2,3) |
|
699 |
unfolding prefix_list_def |
|
| 268 | 700 |
by (smt L_flat_Prf1 append_Nil2 append_eq_append_conv2 flat.simps(7)) |
| 262 | 701 |
then have "flat v3a \<sqsubset>spre s1 \<or> (flat v3a = s1 \<and> flat (Stars vs3) = s2)" using NonEmpty(4) |
702 |
by (simp add: sprefix_list_def append_eq_conv_conj) |
|
703 |
then have q2: "v :\<sqsubset>val v3a \<or> (flat v3a = s1 \<and> flat (Stars vs3) = s2)" |
|
| 264 | 704 |
using PosOrd_spreI as1(1) NonEmpty(4) by blast |
| 268 | 705 |
then have "v :\<sqsubset>val v3a \<or> (v3a \<in> LV r s1 \<and> Stars vs3 \<in> LV (STAR r) s2)" |
706 |
using NonEmpty(2,3) by (auto simp add: LV_def) |
|
| 264 | 707 |
then have "v :\<sqsubset>val v3a \<or> (v :\<sqsubseteq>val v3a \<and> Stars vs :\<sqsubseteq>val Stars vs3)" using IH1 IH2 by blast |
708 |
then have "v :\<sqsubset>val v3a \<or> (v = v3a \<and> Stars vs :\<sqsubseteq>val Stars vs3)" |
|
|
265
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
709 |
unfolding PosOrd_ex_eq_def by auto |
| 262 | 710 |
then have "Stars (v # vs) :\<sqsubseteq>val Stars (v3a # vs3)" using NonEmpty(4) q2 as1 |
|
265
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
711 |
unfolding PosOrd_ex_eq_def |
| 268 | 712 |
using PosOrd_StarsI PosOrd_StarsI2 by auto |
| 262 | 713 |
then show "Stars (v # vs) :\<sqsubseteq>val v3" unfolding NonEmpty by blast |
| 261 | 714 |
next |
715 |
case Empty |
|
716 |
have "v3 = Stars []" by fact |
|
717 |
then show "Stars (v # vs) :\<sqsubseteq>val v3" |
|
|
265
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
718 |
unfolding PosOrd_ex_eq_def using cond2 |
| 261 | 719 |
by (simp add: PosOrd_shorterI) |
720 |
qed |
|
721 |
next |
|
722 |
case (Posix_STAR2 r v2) |
|
| 268 | 723 |
have "v2 \<in> LV (STAR r) []" by fact |
| 262 | 724 |
then have "v2 = Stars []" |
| 268 | 725 |
unfolding LV_def by (auto elim: Prf.cases) |
| 261 | 726 |
then show "Stars [] :\<sqsubseteq>val v2" |
|
265
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
727 |
by (simp add: PosOrd_ex_eq_def) |
| 261 | 728 |
qed |
| 253 | 729 |
|
| 263 | 730 |
|
| 261 | 731 |
lemma Posix_PosOrd_reverse: |
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
732 |
assumes "s \<in> r \<rightarrow> v1" |
| 268 | 733 |
shows "\<not>(\<exists>v2 \<in> LV r s. v2 :\<sqsubset>val v1)" |
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
734 |
using assms |
| 267 | 735 |
by (metis Posix_PosOrd less_irrefl PosOrd_def |
|
265
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
736 |
PosOrd_ex_eq_def PosOrd_ex_def PosOrd_trans) |
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
737 |
|
|
265
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
738 |
|
|
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
739 |
|
|
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
740 |
lemma PosOrd_Posix_Stars: |
|
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
741 |
assumes "\<forall>v \<in> set vs. flat v \<in> r \<rightarrow> v \<and> flat v \<noteq> []" |
| 267 | 742 |
and "\<not>(\<exists>vs2 \<in> LV (STAR r) (flat (Stars vs)). vs2 :\<sqsubset>val (Stars vs))" |
|
265
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
743 |
shows "(flat (Stars vs)) \<in> (STAR r) \<rightarrow> Stars vs" |
|
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
744 |
using assms |
|
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
745 |
proof(induct vs) |
|
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
746 |
case Nil |
|
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
747 |
show "flat (Stars []) \<in> STAR r \<rightarrow> Stars []" |
|
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
748 |
by(simp add: Posix.intros) |
|
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
749 |
next |
|
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
750 |
case (Cons v vs) |
|
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
751 |
have IH: "\<lbrakk>\<forall>v\<in>set vs. flat v \<in> r \<rightarrow> v \<and> flat v \<noteq> []; |
| 267 | 752 |
\<not> (\<exists>vs2\<in>LV (STAR r) (flat (Stars vs)). vs2 :\<sqsubset>val Stars vs)\<rbrakk> |
|
265
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
753 |
\<Longrightarrow> flat (Stars vs) \<in> STAR r \<rightarrow> Stars vs" by fact |
|
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
754 |
have as2: "\<forall>v\<in>set (v # vs). flat v \<in> r \<rightarrow> v \<and> flat v \<noteq> []" by fact |
| 267 | 755 |
have as3: "\<not> (\<exists>vs2\<in>LV (STAR r) (flat (Stars (v # vs))). vs2 :\<sqsubset>val Stars (v # vs))" by fact |
| 268 | 756 |
have "flat v \<in> r \<rightarrow> v" "flat v \<noteq> []" using as2 by auto |
|
265
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
757 |
moreover |
|
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
758 |
have "flat (Stars vs) \<in> STAR r \<rightarrow> Stars vs" |
|
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
759 |
proof (rule IH) |
|
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
760 |
show "\<forall>v\<in>set vs. flat v \<in> r \<rightarrow> v \<and> flat v \<noteq> []" using as2 by simp |
|
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
761 |
next |
| 267 | 762 |
show "\<not> (\<exists>vs2\<in>LV (STAR r) (flat (Stars vs)). vs2 :\<sqsubset>val Stars vs)" using as3 |
|
265
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
763 |
apply(auto) |
| 267 | 764 |
apply(subst (asm) (2) LV_def) |
|
265
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
765 |
apply(auto) |
|
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
766 |
apply(erule Prf.cases) |
|
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
767 |
apply(simp_all) |
|
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
768 |
apply(drule_tac x="Stars (v # vs)" in bspec) |
| 268 | 769 |
apply(simp add: LV_def) |
770 |
using Posix_LV Prf.intros(6) calculation |
|
|
265
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
771 |
apply(rule_tac Prf.intros) |
|
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
772 |
apply(simp add:) |
| 268 | 773 |
prefer 2 |
|
265
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
774 |
apply (simp add: PosOrd_StarsI2) |
| 268 | 775 |
apply(drule Posix_LV) |
776 |
apply(simp add: LV_def) |
|
|
265
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
777 |
done |
|
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
778 |
qed |
|
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
779 |
moreover |
|
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
780 |
have "flat v \<noteq> []" using as2 by simp |
|
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
781 |
moreover |
|
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
782 |
have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = flat (Stars vs) \<and> flat v @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (STAR r))" |
|
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
783 |
using as3 |
|
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
784 |
apply(auto) |
|
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
785 |
apply(drule L_flat_Prf2) |
|
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
786 |
apply(erule exE) |
|
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
787 |
apply(simp only: L.simps[symmetric]) |
|
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
788 |
apply(drule L_flat_Prf2) |
|
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
789 |
apply(erule exE) |
|
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
790 |
apply(clarify) |
|
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
791 |
apply(rotate_tac 5) |
|
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
792 |
apply(erule Prf.cases) |
|
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
793 |
apply(simp_all) |
|
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
794 |
apply(clarify) |
|
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
795 |
apply(drule_tac x="Stars (va#vs)" in bspec) |
| 267 | 796 |
apply(auto simp add: LV_def)[1] |
|
265
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
797 |
apply(rule Prf.intros) |
|
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
798 |
apply(simp) |
|
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
799 |
by (simp add: PosOrd_StarsI PosOrd_shorterI) |
|
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
800 |
ultimately show "flat (Stars (v # vs)) \<in> STAR r \<rightarrow> Stars (v # vs)" |
|
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
801 |
by (simp add: Posix.intros) |
|
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
802 |
qed |
|
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
803 |
|
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
804 |
|
| 254 | 805 |
|
| 261 | 806 |
section {* The Smallest Value is indeed the Posix Value *}
|
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
807 |
|
| 261 | 808 |
lemma PosOrd_Posix: |
| 268 | 809 |
assumes "v1 \<in> LV r s" "\<forall>v\<^sub>2 \<in> LV r s. \<not> v\<^sub>2 :\<sqsubset>val v1" |
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
810 |
shows "s \<in> r \<rightarrow> v1" |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
811 |
using assms |
| 261 | 812 |
proof(induct r arbitrary: s v1) |
813 |
case (ZERO s v1) |
|
| 268 | 814 |
have "v1 \<in> LV ZERO s" by fact |
815 |
then show "s \<in> ZERO \<rightarrow> v1" unfolding LV_def |
|
816 |
by (auto elim: Prf.cases) |
|
| 261 | 817 |
next |
818 |
case (ONE s v1) |
|
| 268 | 819 |
have "v1 \<in> LV ONE s" by fact |
820 |
then show "s \<in> ONE \<rightarrow> v1" unfolding LV_def |
|
821 |
by(auto elim!: Prf.cases intro: Posix.intros) |
|
| 261 | 822 |
next |
823 |
case (CHAR c s v1) |
|
| 268 | 824 |
have "v1 \<in> LV (CHAR c) s" by fact |
825 |
then show "s \<in> CHAR c \<rightarrow> v1" unfolding LV_def |
|
826 |
by (auto elim!: Prf.cases intro: Posix.intros) |
|
| 261 | 827 |
next |
828 |
case (ALT r1 r2 s v1) |
|
| 268 | 829 |
have IH1: "\<And>s v1. \<lbrakk>v1 \<in> LV r1 s; \<forall>v2 \<in> LV r1 s. \<not> v2 :\<sqsubset>val v1\<rbrakk> \<Longrightarrow> s \<in> r1 \<rightarrow> v1" by fact |
830 |
have IH2: "\<And>s v1. \<lbrakk>v1 \<in> LV r2 s; \<forall>v2 \<in> LV r2 s. \<not> v2 :\<sqsubset>val v1\<rbrakk> \<Longrightarrow> s \<in> r2 \<rightarrow> v1" by fact |
|
| 267 | 831 |
have as1: "\<forall>v2\<in>LV (ALT r1 r2) s. \<not> v2 :\<sqsubset>val v1" by fact |
| 268 | 832 |
have as2: "v1 \<in> LV (ALT r1 r2) s" by fact |
| 261 | 833 |
then consider |
834 |
(Left) v1' where |
|
835 |
"v1 = Left v1'" "s = flat v1'" |
|
| 268 | 836 |
"v1' \<in> LV r1 s" |
| 261 | 837 |
| (Right) v1' where |
838 |
"v1 = Right v1'" "s = flat v1'" |
|
| 268 | 839 |
"v1' \<in> LV r2 s" |
840 |
unfolding LV_def by (auto elim: Prf.cases) |
|
| 261 | 841 |
then show "s \<in> ALT r1 r2 \<rightarrow> v1" |
842 |
proof (cases) |
|
843 |
case (Left v1') |
|
| 268 | 844 |
have "v1' \<in> LV r1 s" using as2 |
845 |
unfolding LV_def Left by (auto elim: Prf.cases) |
|
| 261 | 846 |
moreover |
| 267 | 847 |
have "\<forall>v2 \<in> LV r1 s. \<not> v2 :\<sqsubset>val v1'" using as1 |
848 |
unfolding LV_def Left using Prf.intros(2) PosOrd_Left_eq by force |
|
| 261 | 849 |
ultimately have "s \<in> r1 \<rightarrow> v1'" using IH1 by simp |
850 |
then have "s \<in> ALT r1 r2 \<rightarrow> Left v1'" by (rule Posix.intros) |
|
851 |
then show "s \<in> ALT r1 r2 \<rightarrow> v1" using Left by simp |
|
852 |
next |
|
853 |
case (Right v1') |
|
| 268 | 854 |
have "v1' \<in> LV r2 s" using as2 |
855 |
unfolding LV_def Right by (auto elim: Prf.cases) |
|
| 261 | 856 |
moreover |
| 267 | 857 |
have "\<forall>v2 \<in> LV r2 s. \<not> v2 :\<sqsubset>val v1'" using as1 |
858 |
unfolding LV_def Right using Prf.intros(3) PosOrd_RightI by force |
|
| 261 | 859 |
ultimately have "s \<in> r2 \<rightarrow> v1'" using IH2 by simp |
860 |
moreover |
|
861 |
{ assume "s \<in> L r1"
|
|
| 267 | 862 |
then obtain v' where "v' \<in> LV r1 s" |
863 |
unfolding LV_def using L_flat_Prf2 by blast |
|
864 |
then have "Left v' \<in> LV (ALT r1 r2) s" |
|
865 |
unfolding LV_def by (auto intro: Prf.intros) |
|
| 261 | 866 |
with as1 have "\<not> (Left v' :\<sqsubset>val Right v1') \<and> (flat v' = s)" |
| 268 | 867 |
unfolding LV_def Right |
868 |
by (auto) |
|
| 261 | 869 |
then have False using PosOrd_Left_Right Right by blast |
870 |
} |
|
871 |
then have "s \<notin> L r1" by rule |
|
872 |
ultimately have "s \<in> ALT r1 r2 \<rightarrow> Right v1'" by (rule Posix.intros) |
|
873 |
then show "s \<in> ALT r1 r2 \<rightarrow> v1" using Right by simp |
|
874 |
qed |
|
875 |
next |
|
876 |
case (SEQ r1 r2 s v1) |
|
| 268 | 877 |
have IH1: "\<And>s v1. \<lbrakk>v1 \<in> LV r1 s; \<forall>v2 \<in> LV r1 s. \<not> v2 :\<sqsubset>val v1\<rbrakk> \<Longrightarrow> s \<in> r1 \<rightarrow> v1" by fact |
878 |
have IH2: "\<And>s v1. \<lbrakk>v1 \<in> LV r2 s; \<forall>v2 \<in> LV r2 s. \<not> v2 :\<sqsubset>val v1\<rbrakk> \<Longrightarrow> s \<in> r2 \<rightarrow> v1" by fact |
|
| 267 | 879 |
have as1: "\<forall>v2\<in>LV (SEQ r1 r2) s. \<not> v2 :\<sqsubset>val v1" by fact |
| 268 | 880 |
have as2: "v1 \<in> LV (SEQ r1 r2) s" by fact |
| 261 | 881 |
then obtain |
882 |
v1a v1b where eqs: |
|
883 |
"v1 = Seq v1a v1b" "s = flat v1a @ flat v1b" |
|
| 268 | 884 |
"v1a \<in> LV r1 (flat v1a)" "v1b \<in> LV r2 (flat v1b)" |
885 |
unfolding LV_def by(auto elim: Prf.cases) |
|
| 267 | 886 |
have "\<forall>v2 \<in> LV r1 (flat v1a). \<not> v2 :\<sqsubset>val v1a" |
| 261 | 887 |
proof |
888 |
fix v2 |
|
| 267 | 889 |
assume "v2 \<in> LV r1 (flat v1a)" |
890 |
with eqs(2,4) have "Seq v2 v1b \<in> LV (SEQ r1 r2) s" |
|
| 268 | 891 |
by (simp add: LV_def Prf.intros(1)) |
| 261 | 892 |
with as1 have "\<not> Seq v2 v1b :\<sqsubset>val Seq v1a v1b \<and> flat (Seq v2 v1b) = flat (Seq v1a v1b)" |
| 267 | 893 |
using eqs by (simp add: LV_def) |
| 261 | 894 |
then show "\<not> v2 :\<sqsubset>val v1a" |
895 |
using PosOrd_SeqI1 by blast |
|
896 |
qed |
|
897 |
then have "flat v1a \<in> r1 \<rightarrow> v1a" using IH1 eqs by simp |
|
898 |
moreover |
|
| 267 | 899 |
have "\<forall>v2 \<in> LV r2 (flat v1b). \<not> v2 :\<sqsubset>val v1b" |
| 261 | 900 |
proof |
901 |
fix v2 |
|
| 267 | 902 |
assume "v2 \<in> LV r2 (flat v1b)" |
903 |
with eqs(2,3,4) have "Seq v1a v2 \<in> LV (SEQ r1 r2) s" |
|
| 268 | 904 |
by (simp add: LV_def Prf.intros) |
| 261 | 905 |
with as1 have "\<not> Seq v1a v2 :\<sqsubset>val Seq v1a v1b \<and> flat v2 = flat v1b" |
| 267 | 906 |
using eqs by (simp add: LV_def) |
| 261 | 907 |
then show "\<not> v2 :\<sqsubset>val v1b" |
908 |
using PosOrd_SeqI2 by auto |
|
909 |
qed |
|
910 |
then have "flat v1b \<in> r2 \<rightarrow> v1b" using IH2 eqs by simp |
|
911 |
moreover |
|
912 |
have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = flat v1b \<and> flat v1a @ s\<^sub>3 \<in> L r1 \<and> s\<^sub>4 \<in> L r2)" |
|
913 |
proof |
|
914 |
assume "\<exists>s3 s4. s3 \<noteq> [] \<and> s3 @ s4 = flat v1b \<and> flat v1a @ s3 \<in> L r1 \<and> s4 \<in> L r2" |
|
915 |
then obtain s3 s4 where q1: "s3 \<noteq> [] \<and> s3 @ s4 = flat v1b \<and> flat v1a @ s3 \<in> L r1 \<and> s4 \<in> L r2" by blast |
|
| 268 | 916 |
then obtain vA vB where q2: "flat vA = flat v1a @ s3" "\<Turnstile> vA : r1" "flat vB = s4" "\<Turnstile> vB : r2" |
| 261 | 917 |
using L_flat_Prf2 by blast |
| 267 | 918 |
then have "Seq vA vB \<in> LV (SEQ r1 r2) s" unfolding eqs using q1 |
| 268 | 919 |
by (auto simp add: LV_def intro!: Prf.intros) |
| 261 | 920 |
with as1 have "\<not> Seq vA vB :\<sqsubset>val Seq v1a v1b" unfolding eqs by auto |
921 |
then have "\<not> vA :\<sqsubset>val v1a \<and> length (flat vA) > length (flat v1a)" using q1 q2 PosOrd_SeqI1 by auto |
|
922 |
then show "False" |
|
923 |
using PosOrd_shorterI by blast |
|
924 |
qed |
|
925 |
ultimately |
|
926 |
show "s \<in> SEQ r1 r2 \<rightarrow> v1" unfolding eqs |
|
927 |
by (rule Posix.intros) |
|
928 |
next |
|
929 |
case (STAR r s v1) |
|
| 268 | 930 |
have IH: "\<And>s v1. \<lbrakk>v1 \<in> LV r s; \<forall>v2\<in>LV r s. \<not> v2 :\<sqsubset>val v1\<rbrakk> \<Longrightarrow> s \<in> r \<rightarrow> v1" by fact |
| 267 | 931 |
have as1: "\<forall>v2\<in>LV (STAR r) s. \<not> v2 :\<sqsubset>val v1" by fact |
| 268 | 932 |
have as2: "v1 \<in> LV (STAR r) s" by fact |
| 261 | 933 |
then obtain |
934 |
vs where eqs: |
|
935 |
"v1 = Stars vs" "s = flat (Stars vs)" |
|
| 268 | 936 |
"\<forall>v \<in> set vs. v \<in> LV r (flat v)" |
937 |
unfolding LV_def by (auto elim: Prf.cases) |
|
|
265
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
938 |
have "\<forall>v\<in>set vs. flat v \<in> r \<rightarrow> v \<and> flat v \<noteq> []" |
| 261 | 939 |
proof |
940 |
fix v |
|
941 |
assume a: "v \<in> set vs" |
|
942 |
then obtain pre post where e: "vs = pre @ [v] @ post" |
|
943 |
by (metis append_Cons append_Nil in_set_conv_decomp_first) |
|
| 267 | 944 |
then have q: "\<forall>v2\<in>LV (STAR r) s. \<not> v2 :\<sqsubset>val Stars (pre @ [v] @ post)" |
| 261 | 945 |
using as1 unfolding eqs by simp |
| 267 | 946 |
have "\<forall>v2\<in>LV r (flat v). \<not> v2 :\<sqsubset>val v" unfolding eqs |
| 261 | 947 |
proof (rule ballI, rule notI) |
948 |
fix v2 |
|
949 |
assume w: "v2 :\<sqsubset>val v" |
|
| 267 | 950 |
assume "v2 \<in> LV r (flat v)" |
951 |
then have "Stars (pre @ [v2] @ post) \<in> LV (STAR r) s" |
|
| 261 | 952 |
using as2 unfolding e eqs |
| 268 | 953 |
apply(auto simp add: LV_def intro!: Prf.intros elim: Prf_elims dest: Prf_Stars_appendE) |
954 |
apply(auto dest!: Prf_Stars_appendE elim: Prf.cases) |
|
955 |
done |
|
| 261 | 956 |
then have "\<not> Stars (pre @ [v2] @ post) :\<sqsubset>val Stars (pre @ [v] @ post)" |
957 |
using q by simp |
|
958 |
with w show "False" |
|
| 267 | 959 |
using LV_def \<open>v2 \<in> LV r (flat v)\<close> append_Cons flat.simps(7) mem_Collect_eq |
| 261 | 960 |
PosOrd_StarsI PosOrd_Stars_appendI by auto |
961 |
qed |
|
962 |
with IH |
|
| 268 | 963 |
show "flat v \<in> r \<rightarrow> v \<and> flat v \<noteq> []" using a as2 unfolding eqs LV_def |
964 |
by (auto elim: Prf.cases) |
|
| 261 | 965 |
qed |
966 |
moreover |
|
| 267 | 967 |
have "\<not> (\<exists>vs2\<in>LV (STAR r) (flat (Stars vs)). vs2 :\<sqsubset>val Stars vs)" |
| 261 | 968 |
proof |
| 267 | 969 |
assume "\<exists>vs2 \<in> LV (STAR r) (flat (Stars vs)). vs2 :\<sqsubset>val Stars vs" |
| 268 | 970 |
then obtain vs2 where "\<Turnstile> Stars vs2 : STAR r" "flat (Stars vs2) = flat (Stars vs)" |
| 261 | 971 |
"Stars vs2 :\<sqsubset>val Stars vs" |
| 268 | 972 |
unfolding LV_def by (force elim: Prf_elims intro: Prf.intros) |
| 261 | 973 |
then show "False" using as1 unfolding eqs |
| 268 | 974 |
by (auto simp add: LV_def) |
| 261 | 975 |
qed |
|
265
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
976 |
ultimately have "flat (Stars vs) \<in> STAR r \<rightarrow> Stars vs" |
|
d36be1e356c0
changed definitions of PRF
Christian Urban <urbanc@in.tum.de>
parents:
264
diff
changeset
|
977 |
thm PosOrd_Posix_Stars |
| 261 | 978 |
by (rule PosOrd_Posix_Stars) |
979 |
then show "s \<in> STAR r \<rightarrow> v1" unfolding eqs . |
|
980 |
qed |
|
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
981 |
|
| 268 | 982 |
lemma Least_existence: |
983 |
assumes "LV r s \<noteq> {}"
|
|
984 |
shows " \<exists>vmin \<in> LV r s. \<forall>v \<in> LV r s. vmin :\<sqsubseteq>val v" |
|
985 |
proof - |
|
986 |
from assms |
|
987 |
obtain vposix where "s \<in> r \<rightarrow> vposix" |
|
988 |
unfolding LV_def |
|
989 |
using L_flat_Prf1 lexer_correct_Some by blast |
|
990 |
then have "\<forall>v \<in> LV r s. vposix :\<sqsubseteq>val v" |
|
991 |
by (simp add: Posix_PosOrd) |
|
992 |
then show "\<exists>vmin \<in> LV r s. \<forall>v \<in> LV r s. vmin :\<sqsubseteq>val v" |
|
993 |
using Posix_LV \<open>s \<in> r \<rightarrow> vposix\<close> by blast |
|
994 |
qed |
|
995 |
||
996 |
lemma Least_existence1: |
|
997 |
assumes "LV r s \<noteq> {}"
|
|
998 |
shows " \<exists>!vmin \<in> LV r s. \<forall>v \<in> (LV r s \<union> {v'. flat v' \<sqsubset>spre s}). vmin :\<sqsubseteq>val v"
|
|
999 |
using Least_existence[OF assms] assms |
|
1000 |
apply - |
|
1001 |
apply(erule bexE) |
|
1002 |
apply(rule_tac a="vmin" in ex1I) |
|
1003 |
apply(auto)[1] |
|
1004 |
apply (metis PosOrd_Posix PosOrd_ex_eq2 PosOrd_spreI PosOrdeq_antisym Posix1(2)) |
|
1005 |
apply(auto)[1] |
|
1006 |
apply(simp add: PosOrdeq_antisym) |
|
1007 |
done |
|
1008 |
||
1009 |
lemma |
|
1010 |
shows "partial_order_on UNIV {(v1, v2). v1 :\<sqsubseteq>val v2}"
|
|
1011 |
apply(simp add: partial_order_on_def) |
|
1012 |
apply(simp add: preorder_on_def refl_on_def) |
|
1013 |
apply(simp add: PosOrdeq_refl) |
|
1014 |
apply(auto) |
|
1015 |
apply(rule transI) |
|
1016 |
apply(auto intro: PosOrdeq_trans)[1] |
|
1017 |
apply(rule antisymI) |
|
1018 |
apply(simp add: PosOrdeq_antisym) |
|
1019 |
done |
|
1020 |
||
1021 |
lemma |
|
1022 |
"wf {(v1, v2). v1 :\<sqsubset>val v2 \<and> v1 \<in> LV r s \<and> v2 \<in> LV r s}"
|
|
1023 |
apply(rule finite_acyclic_wf) |
|
1024 |
prefer 2 |
|
1025 |
apply(simp add: acyclic_def) |
|
1026 |
apply(induct_tac rule: trancl.induct) |
|
1027 |
apply(auto)[1] |
|
1028 |
oops |
|
1029 |
||
1030 |
||
| 249 | 1031 |
unused_thms |
1032 |
||
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1033 |
end |