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