| author | Christian Urban <urbanc@in.tum.de> |
| Thu, 29 Jun 2017 17:57:41 +0100 | |
| changeset 256 | 146b4817aebd |
| parent 255 | 222ed43892ea |
| child 257 | 9deaff82e0c5 |
| 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 |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
3 |
imports "Lexer" |
|
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 |
|
| 254 | 6 |
|
7 |
section {* Position in values *}
|
|
8 |
||
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
9 |
fun |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
10 |
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
|
11 |
where |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
12 |
"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
|
13 |
| "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
|
14 |
| "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
|
15 |
| "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
|
16 |
| "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
|
17 |
| "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
|
18 |
|
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
19 |
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
|
20 |
where |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
21 |
"Pos (Void) = {[]}"
|
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
22 |
| "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
|
23 |
| "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
|
24 |
| "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
|
25 |
| "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
|
26 |
| "Pos (Stars []) = {[]}"
|
| 251 | 27 |
| "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
|
28 |
|
| 253 | 29 |
lemma Pos_stars: |
30 |
"Pos (Stars vs) = {[]} \<union> (\<Union>n < length vs. {n#ps | ps. ps \<in> Pos (vs ! n)})"
|
|
31 |
apply(induct vs) |
|
32 |
apply(simp) |
|
33 |
apply(simp) |
|
34 |
apply(simp add: insert_ident) |
|
35 |
apply(rule subset_antisym) |
|
36 |
apply(auto) |
|
37 |
apply(auto)[1] |
|
38 |
using less_Suc_eq_0_disj by auto |
|
39 |
||
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
40 |
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
|
41 |
shows "[] \<in> Pos v" |
| 251 | 42 |
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
|
43 |
|
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
44 |
fun intlen :: "'a list \<Rightarrow> int" |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
45 |
where |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
46 |
"intlen [] = 0" |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
47 |
| "intlen (x#xs) = 1 + intlen xs" |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
48 |
|
| 255 | 49 |
lemma intlen_bigger: |
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
50 |
shows "0 \<le> intlen xs" |
| 251 | 51 |
by (induct xs)(auto) |
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
52 |
|
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
53 |
lemma intlen_append: |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
54 |
shows "intlen (xs @ ys) = intlen xs + intlen ys" |
| 251 | 55 |
by (induct xs arbitrary: ys) (auto) |
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
56 |
|
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
57 |
lemma intlen_length: |
| 256 | 58 |
shows "intlen xs < intlen ys \<longleftrightarrow> length xs < length ys" |
59 |
apply(induct xs arbitrary: ys) |
|
60 |
apply(auto) |
|
61 |
apply(case_tac ys) |
|
62 |
apply(simp_all) |
|
63 |
apply (smt intlen_bigger) |
|
64 |
(* HERE *) |
|
65 |
oops |
|
66 |
||
67 |
||
68 |
lemma intlen_length: |
|
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
69 |
assumes "length xs < length ys" |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
70 |
shows "intlen xs < intlen ys" |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
71 |
using assms |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
72 |
apply(induct xs arbitrary: ys) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
73 |
apply(auto) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
74 |
apply(case_tac ys) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
75 |
apply(simp_all) |
| 255 | 76 |
apply (smt intlen_bigger) |
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
77 |
by (smt Suc_lessE intlen.simps(2) length_Suc_conv) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
78 |
|
| 255 | 79 |
lemma length_intlen: |
80 |
assumes "intlen xs < intlen ys" |
|
81 |
shows "length xs < length ys" |
|
82 |
using assms |
|
83 |
apply(induct xs arbitrary: ys) |
|
84 |
apply(auto) |
|
85 |
apply(case_tac ys) |
|
86 |
apply(simp_all) |
|
87 |
by (smt intlen_bigger) |
|
88 |
||
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
89 |
|
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
90 |
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
|
91 |
where |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
92 |
"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
|
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 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
|
95 |
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
|
96 |
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
|
97 |
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
|
98 |
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
|
99 |
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
|
100 |
and "pflat_len (Right v) (0#p) = -1" |
| 251 | 101 |
and "pflat_len (Stars (v#vs)) (Suc n#p) = pflat_len (Stars vs) (n#p)" |
102 |
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
|
103 |
and "pflat_len v [] = intlen (flat v)" |
| 251 | 104 |
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
|
105 |
|
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
106 |
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
|
107 |
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
|
108 |
shows "pflat_len (Stars vs) (n#p) = pflat_len (vs!n) p" |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
109 |
using assms |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
110 |
apply(induct vs arbitrary: n p) |
| 251 | 111 |
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
|
112 |
done |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
113 |
|
| 254 | 114 |
lemma outside_lemma: |
115 |
assumes "p \<notin> Pos v1 \<union> Pos v2" |
|
116 |
shows "pflat_len v1 p = pflat_len v2 p" |
|
117 |
using assms by (auto simp add: pflat_len_def) |
|
| 252 | 118 |
|
119 |
||
120 |
section {* Orderings *}
|
|
121 |
||
122 |
||
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
123 |
definition prefix_list:: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" ("_ \<sqsubseteq>pre _")
|
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
124 |
where |
| 252 | 125 |
"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
|
126 |
|
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
127 |
definition sprefix_list:: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" ("_ \<sqsubset>spre _")
|
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
128 |
where |
| 252 | 129 |
"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
|
130 |
|
| 251 | 131 |
inductive lex_list :: "nat list \<Rightarrow> nat list \<Rightarrow> bool" ("_ \<sqsubset>lex _")
|
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
132 |
where |
| 252 | 133 |
"[] \<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
|
134 |
| "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
|
135 |
| "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
|
136 |
|
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
137 |
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
|
138 |
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
|
139 |
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
|
140 |
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
|
141 |
using assms |
| 251 | 142 |
apply(induct rule: lex_list.induct) |
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
143 |
apply(auto) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
144 |
done |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
145 |
|
| 251 | 146 |
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
|
147 |
fixes xs ys :: "nat list" |
| 251 | 148 |
shows "[] \<sqsubset>lex ys \<longleftrightarrow> ys \<noteq> []" |
149 |
and "xs \<sqsubset>lex [] \<longleftrightarrow> False" |
|
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
150 |
and "(x # xs) \<sqsubset>lex (y # ys) \<longleftrightarrow> (x < y \<or> (\<not> y < x \<and> xs \<sqsubset>lex ys))" |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
151 |
apply - |
| 251 | 152 |
apply (metis lex_irrfl lex_list.intros(1) list.exhaust) |
153 |
using lex_list.cases apply blast |
|
154 |
using lex_list.cases lex_list.intros(2) lex_list.intros(3) not_less_iff_gr_or_eq by fastforce |
|
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
155 |
|
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
156 |
|
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
157 |
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
|
158 |
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
|
159 |
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
|
160 |
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
|
161 |
using assms |
| 251 | 162 |
apply(induct arbitrary: ps3 rule: lex_list.induct) |
163 |
apply(erule 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
|
164 |
apply(simp_all) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
165 |
apply(rotate_tac 2) |
| 251 | 166 |
apply(erule 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
|
167 |
apply(simp_all) |
| 251 | 168 |
apply(erule 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
|
169 |
apply(simp_all) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
170 |
done |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
171 |
|
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
172 |
|
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
173 |
lemma trichotomous: |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
174 |
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
|
175 |
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
|
176 |
apply(induct p arbitrary: q) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
177 |
apply(auto) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
178 |
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
|
179 |
apply(auto) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
180 |
done |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
181 |
|
| 254 | 182 |
|
183 |
||
184 |
||
185 |
section {* Ordering of values according to Okui & Suzuki *}
|
|
186 |
||
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
187 |
|
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
188 |
definition val_ord:: "val \<Rightarrow> nat list \<Rightarrow> val \<Rightarrow> bool" ("_ \<sqsubset>val _ _")
|
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
189 |
where |
| 254 | 190 |
"v1 \<sqsubset>val p v2 \<equiv> (p \<in> Pos v1 \<and> |
191 |
pflat_len v1 p > pflat_len v2 p \<and> |
|
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
192 |
(\<forall>q \<in> Pos v1 \<union> Pos v2. q \<sqsubset>lex p \<longrightarrow> pflat_len v1 q = pflat_len v2 q))" |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
193 |
|
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
194 |
|
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
195 |
definition val_ord_ex:: "val \<Rightarrow> val \<Rightarrow> bool" ("_ :\<sqsubset>val _")
|
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
196 |
where |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
197 |
"v1 :\<sqsubset>val v2 \<equiv> (\<exists>p. v1 \<sqsubset>val p v2)" |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
198 |
|
| 256 | 199 |
|
200 |
||
201 |
||
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
202 |
definition val_ord_ex1:: "val \<Rightarrow> val \<Rightarrow> bool" ("_ :\<sqsubseteq>val _")
|
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
203 |
where |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
204 |
"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
|
205 |
|
| 255 | 206 |
lemma val_ord_shorterE: |
207 |
assumes "v1 :\<sqsubset>val v2" |
|
208 |
shows "length (flat v2) \<le> length (flat v1)" |
|
209 |
using assms |
|
210 |
apply(auto simp add: val_ord_ex_def val_ord_def) |
|
211 |
apply(case_tac p) |
|
212 |
apply(simp add: pflat_len_simps) |
|
213 |
apply(drule length_intlen) |
|
214 |
apply(simp) |
|
215 |
apply(drule_tac x="[]" in bspec) |
|
216 |
apply(simp add: Pos_empty) |
|
217 |
apply(simp add: pflat_len_simps) |
|
218 |
by (metis intlen_length le_less less_irrefl linear) |
|
219 |
||
220 |
||
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
221 |
lemma val_ord_shorterI: |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
222 |
assumes "length (flat v') < length (flat v)" |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
223 |
shows "v :\<sqsubset>val v'" |
| 251 | 224 |
using assms |
225 |
unfolding val_ord_ex_def |
|
226 |
by (metis Pos_empty intlen_length lex_simps(2) pflat_len_simps(9) val_ord_def) |
|
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
227 |
|
| 251 | 228 |
lemma val_ord_spreI: |
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
229 |
assumes "(flat v') \<sqsubset>spre (flat v)" |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
230 |
shows "v :\<sqsubset>val v'" |
| 251 | 231 |
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
|
232 |
apply(rule_tac val_ord_shorterI) |
| 251 | 233 |
by (metis append_eq_conv_conj le_less_linear prefix_list_def sprefix_list_def take_all) |
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
234 |
|
| 254 | 235 |
|
| 256 | 236 |
|
| 251 | 237 |
lemma val_ord_LeftI: |
238 |
assumes "v :\<sqsubset>val v'" "flat v = flat v'" |
|
239 |
shows "(Left v) :\<sqsubset>val (Left v')" |
|
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
240 |
using assms(1) |
| 251 | 241 |
unfolding val_ord_ex_def |
242 |
apply(auto) |
|
243 |
apply(rule_tac x="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
|
244 |
using assms(2) |
| 251 | 245 |
apply(auto simp add: val_ord_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
|
246 |
done |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
247 |
|
| 251 | 248 |
lemma val_ord_RightI: |
249 |
assumes "v :\<sqsubset>val v'" "flat v = flat v'" |
|
250 |
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
|
251 |
using assms(1) |
| 251 | 252 |
unfolding val_ord_ex_def |
253 |
apply(auto) |
|
254 |
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
|
255 |
using assms(2) |
| 251 | 256 |
apply(auto simp add: val_ord_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
|
257 |
done |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
258 |
|
| 252 | 259 |
lemma val_ord_LeftE: |
260 |
assumes "(Left v1) :\<sqsubset>val (Left v2)" |
|
261 |
shows "v1 :\<sqsubset>val v2" |
|
262 |
using assms |
|
263 |
apply(simp add: val_ord_ex_def) |
|
264 |
apply(erule exE) |
|
265 |
apply(case_tac "p = []") |
|
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
266 |
apply(simp add: val_ord_def) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
267 |
apply(auto simp add: pflat_len_simps) |
| 252 | 268 |
apply(rule_tac x="[]" in exI) |
269 |
apply(simp add: Pos_empty pflat_len_simps) |
|
270 |
apply(auto simp add: pflat_len_simps val_ord_def) |
|
271 |
apply(rule_tac x="ps" in exI) |
|
272 |
apply(auto) |
|
273 |
apply(drule_tac x="0#q" in bspec) |
|
274 |
apply(simp) |
|
275 |
apply(simp add: pflat_len_simps) |
|
276 |
apply(drule_tac x="0#q" in bspec) |
|
277 |
apply(simp) |
|
278 |
apply(simp add: pflat_len_simps) |
|
279 |
done |
|
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
280 |
|
| 252 | 281 |
lemma val_ord_RightE: |
282 |
assumes "(Right v1) :\<sqsubset>val (Right v2)" |
|
283 |
shows "v1 :\<sqsubset>val v2" |
|
284 |
using assms |
|
285 |
apply(simp add: val_ord_ex_def) |
|
286 |
apply(erule exE) |
|
287 |
apply(case_tac "p = []") |
|
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
288 |
apply(simp add: val_ord_def) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
289 |
apply(auto simp add: pflat_len_simps) |
| 252 | 290 |
apply(rule_tac x="[]" in exI) |
291 |
apply(simp add: Pos_empty pflat_len_simps) |
|
292 |
apply(auto simp add: pflat_len_simps val_ord_def) |
|
293 |
apply(rule_tac x="ps" in exI) |
|
294 |
apply(auto) |
|
295 |
apply(drule_tac x="Suc 0#q" in bspec) |
|
296 |
apply(simp) |
|
297 |
apply(simp add: pflat_len_simps) |
|
298 |
apply(drule_tac x="Suc 0#q" in bspec) |
|
299 |
apply(simp) |
|
300 |
apply(simp add: pflat_len_simps) |
|
301 |
done |
|
302 |
||
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
303 |
|
| 252 | 304 |
lemma val_ord_SeqI1: |
305 |
assumes "v1 :\<sqsubset>val v1'" "flat (Seq v1 v2) = flat (Seq v1' v2')" |
|
306 |
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
|
307 |
using assms(1) |
| 252 | 308 |
apply(subst (asm) val_ord_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
|
309 |
apply(subst (asm) val_ord_def) |
| 252 | 310 |
apply(clarify) |
311 |
apply(subst val_ord_ex_def) |
|
312 |
apply(rule_tac x="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
|
313 |
apply(subst val_ord_def) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
314 |
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
|
315 |
apply(simp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
316 |
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
|
317 |
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
|
318 |
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
|
319 |
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
|
320 |
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
|
321 |
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
|
322 |
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
|
323 |
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
|
324 |
apply(simp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
325 |
apply(auto simp add: pflat_len_simps)[2] |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
326 |
done |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
327 |
|
| 252 | 328 |
lemma val_ord_SeqI2: |
329 |
assumes "v2 :\<sqsubset>val v2'" "flat v2 = flat v2'" |
|
330 |
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
|
331 |
using assms(1) |
| 252 | 332 |
apply(subst (asm) val_ord_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
|
333 |
apply(subst (asm) val_ord_def) |
| 252 | 334 |
apply(clarify) |
335 |
apply(subst val_ord_ex_def) |
|
336 |
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
|
337 |
apply(subst val_ord_def) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
338 |
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
|
339 |
apply(simp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
340 |
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
|
341 |
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
|
342 |
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
|
343 |
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
|
344 |
apply(simp only: Pos.simps) |
| 252 | 345 |
apply(auto)[1] |
346 |
apply(simp add: pflat_len_simps) |
|
347 |
using assms(2) |
|
348 |
apply(simp) |
|
349 |
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
|
350 |
done |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
351 |
|
| 254 | 352 |
lemma val_ord_SeqE: |
353 |
assumes "(Seq v1 v2) :\<sqsubset>val (Seq v1' v2')" |
|
354 |
shows "v1 :\<sqsubset>val v1' \<or> v2 :\<sqsubset>val v2'" |
|
355 |
using assms |
|
356 |
apply(simp add: val_ord_ex_def) |
|
357 |
apply(erule exE) |
|
358 |
apply(case_tac p) |
|
359 |
apply(simp add: val_ord_def) |
|
360 |
apply(auto simp add: pflat_len_simps intlen_append)[1] |
|
361 |
apply(rule_tac x="[]" in exI) |
|
362 |
apply(drule_tac x="[]" in spec) |
|
363 |
apply(simp add: Pos_empty pflat_len_simps) |
|
364 |
apply(case_tac a) |
|
365 |
apply(rule disjI1) |
|
366 |
apply(simp add: val_ord_def) |
|
367 |
apply(auto simp add: pflat_len_simps intlen_append)[1] |
|
368 |
apply(rule_tac x="list" in exI) |
|
369 |
apply(simp) |
|
370 |
apply(rule ballI) |
|
371 |
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
|
372 |
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
|
373 |
apply(simp) |
| 254 | 374 |
apply(simp add: pflat_len_simps) |
375 |
apply(case_tac nat) |
|
376 |
apply(rule disjI2) |
|
377 |
apply(simp add: val_ord_def) |
|
378 |
apply(auto simp add: pflat_len_simps intlen_append) |
|
379 |
apply(rule_tac x="list" in exI) |
|
380 |
apply(simp add: Pos_empty) |
|
381 |
apply(rule ballI) |
|
382 |
apply(rule impI) |
|
383 |
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
|
384 |
apply(simp) |
| 254 | 385 |
apply(simp add: pflat_len_simps) |
386 |
apply(simp add: val_ord_def) |
|
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
387 |
done |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
388 |
|
| 254 | 389 |
lemma val_ord_StarsI: |
390 |
assumes "v1 :\<sqsubset>val v2" "flat (Stars (v1#vs1)) = flat (Stars (v2#vs2))" |
|
391 |
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
|
392 |
using assms(1) |
| 254 | 393 |
apply(subst (asm) val_ord_ex_def) |
394 |
apply(subst (asm) val_ord_def) |
|
395 |
apply(clarify) |
|
396 |
apply(subst val_ord_ex_def) |
|
397 |
apply(subst val_ord_def) |
|
398 |
apply(rule_tac x="0#p" in exI) |
|
399 |
apply(simp add: pflat_len_Stars_simps pflat_len_simps) |
|
400 |
using assms(2) |
|
401 |
apply(simp add: pflat_len_simps intlen_append) |
|
402 |
apply(auto simp add: pflat_len_Stars_simps 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
|
403 |
done |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
404 |
|
| 254 | 405 |
lemma val_ord_StarsI2: |
406 |
assumes "(Stars vs1) :\<sqsubset>val (Stars vs2)" "flat (Stars vs1) = flat (Stars vs2)" |
|
407 |
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
|
408 |
using assms(1) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
409 |
apply(subst (asm) val_ord_ex_def) |
| 254 | 410 |
apply(subst (asm) val_ord_def) |
411 |
apply(clarify) |
|
412 |
apply(subst val_ord_ex_def) |
|
413 |
apply(subst val_ord_def) |
|
414 |
apply(case_tac p) |
|
415 |
apply(simp add: pflat_len_simps) |
|
416 |
apply(rule_tac x="[]" in exI) |
|
417 |
apply(simp add: pflat_len_Stars_simps pflat_len_simps intlen_append) |
|
418 |
apply(rule_tac x="Suc a#list" in exI) |
|
419 |
apply(simp add: pflat_len_Stars_simps pflat_len_simps) |
|
420 |
using assms(2) |
|
421 |
apply(simp add: pflat_len_simps intlen_append) |
|
422 |
apply(auto simp add: pflat_len_Stars_simps pflat_len_simps) |
|
423 |
done |
|
424 |
||
425 |
lemma val_ord_Stars_appendI: |
|
426 |
assumes "Stars vs1 :\<sqsubset>val Stars vs2" "flat (Stars vs1) = flat (Stars vs2)" |
|
427 |
shows "Stars (vs @ vs1) :\<sqsubset>val Stars (vs @ vs2)" |
|
428 |
using assms |
|
429 |
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
|
430 |
apply(simp) |
| 254 | 431 |
apply(simp add: val_ord_StarsI2) |
432 |
done |
|
433 |
||
434 |
lemma val_ord_StarsE2: |
|
435 |
assumes "Stars (v # vs1) :\<sqsubset>val Stars (v # vs2)" |
|
436 |
shows "Stars vs1 :\<sqsubset>val Stars vs2" |
|
437 |
using assms |
|
438 |
apply(subst (asm) val_ord_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
|
439 |
apply(erule exE) |
| 254 | 440 |
apply(case_tac p) |
441 |
apply(simp) |
|
442 |
apply(simp add: val_ord_def pflat_len_simps intlen_append) |
|
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
443 |
apply(subst val_ord_ex_def) |
| 254 | 444 |
apply(rule_tac x="[]" in exI) |
445 |
apply(simp add: val_ord_def pflat_len_simps Pos_empty) |
|
446 |
apply(simp) |
|
447 |
apply(case_tac a) |
|
448 |
apply(clarify) |
|
449 |
apply(auto simp add: pflat_len_simps val_ord_def pflat_len_def)[1] |
|
450 |
apply(clarify) |
|
451 |
apply(simp add: val_ord_ex_def) |
|
452 |
apply(rule_tac x="nat#list" in exI) |
|
453 |
apply(auto simp add: val_ord_def pflat_len_simps intlen_append)[1] |
|
454 |
apply(case_tac q) |
|
455 |
apply(simp add: val_ord_def pflat_len_simps intlen_append) |
|
456 |
apply(clarify) |
|
457 |
apply(drule_tac x="Suc a # lista" in bspec) |
|
458 |
apply(simp) |
|
459 |
apply(auto simp add: val_ord_def pflat_len_simps intlen_append)[1] |
|
460 |
apply(case_tac q) |
|
461 |
apply(simp add: val_ord_def pflat_len_simps intlen_append) |
|
462 |
apply(clarify) |
|
463 |
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
|
464 |
apply(simp) |
| 254 | 465 |
apply(auto simp add: val_ord_def pflat_len_simps intlen_append)[1] |
466 |
done |
|
467 |
||
468 |
lemma val_ord_Stars_appendE: |
|
469 |
assumes "Stars (vs @ vs1) :\<sqsubset>val Stars (vs @ vs2)" |
|
470 |
shows "Stars vs1 :\<sqsubset>val Stars vs2" |
|
471 |
using assms |
|
472 |
apply(induct vs) |
|
473 |
apply(simp) |
|
474 |
apply(simp add: val_ord_StarsE2) |
|
475 |
done |
|
476 |
||
477 |
lemma val_ord_Stars_append_eq: |
|
478 |
assumes "flat (Stars vs1) = flat (Stars vs2)" |
|
479 |
shows "Stars (vs @ vs1) :\<sqsubset>val Stars (vs @ vs2) \<longleftrightarrow> Stars vs1 :\<sqsubset>val Stars vs2" |
|
480 |
using assms |
|
481 |
apply(rule_tac iffI) |
|
482 |
apply(erule val_ord_Stars_appendE) |
|
483 |
apply(rule val_ord_Stars_appendI) |
|
484 |
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
|
485 |
done |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
486 |
|
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
487 |
|
| 254 | 488 |
lemma val_ord_trans: |
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
489 |
assumes "v1 :\<sqsubset>val v2" "v2 :\<sqsubset>val v3" |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
490 |
shows "v1 :\<sqsubset>val v3" |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
491 |
using assms |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
492 |
unfolding val_ord_ex_def |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
493 |
apply(clarify) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
494 |
apply(subgoal_tac "p = pa \<or> p \<sqsubset>lex pa \<or> pa \<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
|
495 |
prefer 2 |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
496 |
apply(rule trichotomous) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
497 |
apply(erule disjE) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
498 |
apply(simp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
499 |
apply(rule_tac x="pa" in exI) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
500 |
apply(subst val_ord_def) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
501 |
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
|
502 |
apply(simp add: val_ord_def) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
503 |
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
|
504 |
apply(simp add: val_ord_def) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
505 |
apply(simp add: val_ord_def) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
506 |
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
|
507 |
using outside_lemma apply blast |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
508 |
apply(simp add: val_ord_def) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
509 |
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
|
510 |
using outside_lemma apply force |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
511 |
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
|
512 |
apply(simp add: val_ord_def) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
513 |
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
|
514 |
apply (metis (no_types, hide_lams) lex_trans outside_lemma) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
515 |
apply(simp add: val_ord_def) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
516 |
apply(auto)[1] |
| 255 | 517 |
by (smt intlen_bigger lex_trans outside_lemma pflat_len_def) |
| 254 | 518 |
|
| 256 | 519 |
lemma val_ord_irrefl: |
520 |
assumes "v :\<sqsubset>val v" |
|
521 |
shows "False" |
|
522 |
using assms |
|
523 |
by(auto simp add: val_ord_ex_def val_ord_def) |
|
524 |
||
525 |
lemma val_ord_almost_trichotomous: |
|
526 |
shows "v1 :\<sqsubset>val v2 \<or> v2 :\<sqsubset>val v1 \<or> (intlen (flat v1) = intlen (flat v2))" |
|
527 |
apply(auto simp add: val_ord_ex_def) |
|
528 |
apply(auto simp add: val_ord_def) |
|
529 |
apply(rule_tac x="[]" in exI) |
|
530 |
apply(auto simp add: Pos_empty pflat_len_simps) |
|
531 |
apply(drule_tac x="[]" in spec) |
|
532 |
apply(auto simp add: Pos_empty pflat_len_simps) |
|
533 |
done |
|
534 |
||
535 |
lemma WW1: |
|
536 |
assumes "v1 :\<sqsubset>val v2" "v2 :\<sqsubset>val v1" |
|
537 |
shows "False" |
|
538 |
using assms |
|
539 |
apply(auto simp add: val_ord_ex_def val_ord_def) |
|
540 |
using assms(1) assms(2) val_ord_irrefl val_ord_trans by blast |
|
541 |
||
542 |
lemma WW2: |
|
543 |
assumes "\<not>(v1 :\<sqsubset>val v2)" |
|
544 |
shows "v1 = v2 \<or> v2 :\<sqsubset>val v1" |
|
545 |
using assms |
|
546 |
oops |
|
547 |
||
548 |
lemma val_ord_SeqE2: |
|
549 |
assumes "(Seq v1 v2) :\<sqsubset>val (Seq v1' v2')" |
|
550 |
shows "v1 :\<sqsubset>val v1' \<or> (v1 = v1' \<and> v2 :\<sqsubset>val v2')" |
|
551 |
using assms |
|
552 |
apply(frule_tac val_ord_SeqE) |
|
553 |
apply(erule disjE) |
|
554 |
apply(simp) |
|
555 |
apply(auto) |
|
556 |
apply(case_tac "v1 :\<sqsubset>val v1'") |
|
557 |
apply(simp) |
|
558 |
apply(auto simp add: val_ord_ex_def) |
|
559 |
apply(case_tac "v1 = v1'") |
|
560 |
apply(simp) |
|
561 |
oops |
|
| 254 | 562 |
|
563 |
section {* CPT and CPTpre *}
|
|
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
564 |
|
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
565 |
|
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
566 |
inductive |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
567 |
CPrf :: "val \<Rightarrow> rexp \<Rightarrow> bool" ("\<Turnstile> _ : _" [100, 100] 100)
|
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
568 |
where |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
569 |
"\<lbrakk>\<Turnstile> v1 : r1; \<Turnstile> v2 : r2\<rbrakk> \<Longrightarrow> \<Turnstile> Seq v1 v2 : SEQ r1 r2" |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
570 |
| "\<Turnstile> v1 : r1 \<Longrightarrow> \<Turnstile> Left v1 : ALT r1 r2" |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
571 |
| "\<Turnstile> v2 : r2 \<Longrightarrow> \<Turnstile> Right v2 : ALT r1 r2" |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
572 |
| "\<Turnstile> Void : ONE" |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
573 |
| "\<Turnstile> Char c : CHAR c" |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
574 |
| "\<Turnstile> Stars [] : STAR r" |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
575 |
| "\<lbrakk>\<Turnstile> v : r; flat v \<noteq> []; \<Turnstile> Stars vs : STAR r\<rbrakk> \<Longrightarrow> \<Turnstile> Stars (v # vs) : STAR r" |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
576 |
|
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
577 |
lemma Prf_CPrf: |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
578 |
assumes "\<Turnstile> v : r" |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
579 |
shows "\<turnstile> v : r" |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
580 |
using assms |
| 254 | 581 |
by (induct) (auto intro: Prf.intros) |
582 |
||
| 256 | 583 |
lemma pflat_len_equal_iff: |
584 |
assumes "\<Turnstile> v1 : r" "\<Turnstile> v2 : r" |
|
585 |
and "\<forall>p. pflat_len v1 p = pflat_len v2 p" |
|
586 |
shows "v1 = v2" |
|
587 |
using assms |
|
588 |
apply(induct v1 r arbitrary: v2 rule: CPrf.induct) |
|
589 |
apply(rotate_tac 4) |
|
590 |
apply(erule CPrf.cases) |
|
591 |
apply(simp_all)[7] |
|
592 |
apply (metis pflat_len_simps(1) pflat_len_simps(2)) |
|
593 |
apply(rotate_tac 2) |
|
594 |
apply(erule CPrf.cases) |
|
595 |
apply(simp_all)[7] |
|
596 |
apply (metis pflat_len_simps(3)) |
|
597 |
apply (metis intlen.simps(1) intlen_length length_greater_0_conv list.size(3) neg_0_le_iff_le not_less not_less_iff_gr_or_eq not_one_le_zero pflat_len_simps(3) pflat_len_simps(6) pflat_len_simps(9)) |
|
598 |
apply(rotate_tac 2) |
|
599 |
apply(erule CPrf.cases) |
|
600 |
apply(simp_all)[7] |
|
601 |
apply (metis intlen.simps(1) intlen_length length_greater_0_conv list.size(3) neg_0_le_iff_le not_less not_less_iff_gr_or_eq not_one_le_zero pflat_len_simps(3) pflat_len_simps(6) pflat_len_simps(9)) |
|
602 |
apply (metis pflat_len_simps(5)) |
|
603 |
apply(erule CPrf.cases) |
|
604 |
apply(simp_all)[7] |
|
605 |
apply(erule CPrf.cases) |
|
606 |
apply(simp_all)[7] |
|
607 |
apply(erule CPrf.cases) |
|
608 |
apply(simp_all)[7] |
|
609 |
apply (metis append_Cons flat.simps(6) flat.simps(7) intlen_length length_greater_0_conv neq_Nil_conv not_less_iff_gr_or_eq pflat_len_simps(9)) |
|
610 |
apply(rotate_tac 5) |
|
611 |
apply(erule CPrf.cases) |
|
612 |
apply(simp_all)[7] |
|
613 |
apply (metis append_Cons flat.simps(6) flat.simps(7) intlen_length length_greater_0_conv list.distinct(1) list.exhaust not_less_iff_gr_or_eq pflat_len_simps(9)) |
|
614 |
apply(auto) |
|
615 |
apply (metis pflat_len_simps(8)) |
|
616 |
apply(subgoal_tac "v = va") |
|
617 |
prefer 2 |
|
618 |
apply (metis pflat_len_simps(8)) |
|
619 |
apply(simp) |
|
620 |
apply(rotate_tac 3) |
|
621 |
apply(drule_tac x="Stars vsa" in meta_spec) |
|
622 |
apply(simp) |
|
623 |
apply(drule_tac meta_mp) |
|
624 |
apply(rule allI) |
|
625 |
apply(case_tac p) |
|
626 |
apply(simp add: pflat_len_simps) |
|
627 |
apply(drule_tac x="[]" in spec) |
|
628 |
apply(simp add: pflat_len_simps intlen_append) |
|
629 |
apply(drule_tac x="Suc a#list" in spec) |
|
630 |
apply(simp add: pflat_len_simps intlen_append) |
|
631 |
apply(simp) |
|
632 |
done |
|
633 |
||
634 |
lemma val_ord_trichotomous_stronger: |
|
635 |
assumes "\<Turnstile> v1 : r" "\<Turnstile> v2 : r" |
|
636 |
shows "v1 :\<sqsubset>val v2 \<or> v2 :\<sqsubset>val v1 \<or> (v1 = v2)" |
|
637 |
oops |
|
638 |
||
| 254 | 639 |
lemma CPrf_stars: |
640 |
assumes "\<Turnstile> Stars vs : STAR r" |
|
641 |
shows "\<forall>v \<in> set vs. flat v \<noteq> [] \<and> \<Turnstile> v : r" |
|
642 |
using assms |
|
643 |
apply(induct vs) |
|
644 |
apply(auto) |
|
645 |
apply(erule CPrf.cases) |
|
646 |
apply(simp_all) |
|
647 |
apply(erule CPrf.cases) |
|
648 |
apply(simp_all) |
|
649 |
apply(erule CPrf.cases) |
|
650 |
apply(simp_all) |
|
651 |
apply(erule CPrf.cases) |
|
652 |
apply(simp_all) |
|
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
653 |
done |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
654 |
|
| 254 | 655 |
lemma CPrf_Stars_appendE: |
656 |
assumes "\<Turnstile> Stars (vs1 @ vs2) : STAR r" |
|
657 |
shows "\<Turnstile> Stars vs1 : STAR r \<and> \<Turnstile> Stars vs2 : STAR r" |
|
658 |
using assms |
|
659 |
apply(induct vs1 arbitrary: vs2) |
|
660 |
apply(auto intro: CPrf.intros)[1] |
|
661 |
apply(erule CPrf.cases) |
|
662 |
apply(simp_all) |
|
663 |
apply(auto intro: CPrf.intros) |
|
664 |
done |
|
665 |
||
666 |
definition PT :: "rexp \<Rightarrow> string \<Rightarrow> val set" |
|
667 |
where "PT r s \<equiv> {v. flat v = s \<and> \<turnstile> v : r}"
|
|
668 |
||
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
669 |
definition |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
670 |
"CPT r s = {v. flat v = s \<and> \<Turnstile> v : r}"
|
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
671 |
|
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
672 |
definition |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
673 |
"CPTpre r s = {v. \<exists>s'. flat v @ s' = s \<and> \<Turnstile> v : r}"
|
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
674 |
|
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
675 |
lemma CPT_CPTpre_subset: |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
676 |
shows "CPT r s \<subseteq> CPTpre r s" |
| 254 | 677 |
by(auto simp add: CPT_def CPTpre_def) |
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
678 |
|
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
679 |
lemma CPTpre_subsets: |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
680 |
"CPTpre ZERO s = {}"
|
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
681 |
"CPTpre ONE s \<subseteq> {Void}"
|
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
682 |
"CPTpre (CHAR c) s \<subseteq> {Char c}"
|
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
683 |
"CPTpre (ALT r1 r2) s \<subseteq> Left ` CPTpre r1 s \<union> Right ` CPTpre r2 s" |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
684 |
"CPTpre (SEQ r1 r2) s \<subseteq> {Seq v1 v2 | v1 v2. v1 \<in> CPTpre r1 s \<and> v2 \<in> CPTpre r2 (drop (length (flat v1)) s)}"
|
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
685 |
"CPTpre (STAR r) s \<subseteq> {Stars []} \<union>
|
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
686 |
{Stars (v#vs) | v vs. v \<in> CPTpre r s \<and> flat v \<noteq> [] \<and> Stars vs \<in> CPTpre (STAR r) (drop (length (flat v)) s)}"
|
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
687 |
"CPTpre (STAR r) [] = {Stars []}"
|
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
688 |
apply(auto simp add: CPTpre_def) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
689 |
apply(erule CPrf.cases) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
690 |
apply(simp_all) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
691 |
apply(erule CPrf.cases) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
692 |
apply(simp_all) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
693 |
apply(erule CPrf.cases) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
694 |
apply(simp_all) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
695 |
apply(erule CPrf.cases) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
696 |
apply(simp_all) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
697 |
apply(erule CPrf.cases) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
698 |
apply(simp_all) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
699 |
apply(erule CPrf.cases) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
700 |
apply(simp_all) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
701 |
apply(erule CPrf.cases) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
702 |
apply(simp_all) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
703 |
apply(rule CPrf.intros) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
704 |
done |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
705 |
|
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
706 |
|
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
707 |
lemma CPTpre_simps: |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
708 |
shows "CPTpre ONE s = {Void}"
|
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
709 |
and "CPTpre (CHAR c) (d#s) = (if c = d then {Char c} else {})"
|
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
710 |
and "CPTpre (ALT r1 r2) s = Left ` CPTpre r1 s \<union> Right ` CPTpre r2 s" |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
711 |
and "CPTpre (SEQ r1 r2) s = |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
712 |
{Seq v1 v2 | v1 v2. v1 \<in> CPTpre r1 s \<and> v2 \<in> CPTpre r2 (drop (length (flat v1)) s)}"
|
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
713 |
apply - |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
714 |
apply(rule subset_antisym) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
715 |
apply(rule CPTpre_subsets) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
716 |
apply(auto simp add: CPTpre_def intro: "CPrf.intros")[1] |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
717 |
apply(case_tac "c = d") |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
718 |
apply(simp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
719 |
apply(rule subset_antisym) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
720 |
apply(rule CPTpre_subsets) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
721 |
apply(auto simp add: CPTpre_def intro: CPrf.intros)[1] |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
722 |
apply(simp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
723 |
apply(auto simp add: CPTpre_def intro: CPrf.intros)[1] |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
724 |
apply(erule CPrf.cases) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
725 |
apply(simp_all) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
726 |
apply(rule subset_antisym) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
727 |
apply(rule CPTpre_subsets) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
728 |
apply(auto simp add: CPTpre_def intro: CPrf.intros)[1] |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
729 |
apply(rule subset_antisym) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
730 |
apply(rule CPTpre_subsets) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
731 |
apply(auto simp add: CPTpre_def intro: CPrf.intros)[1] |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
732 |
done |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
733 |
|
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
734 |
lemma CPT_simps: |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
735 |
shows "CPT ONE s = (if s = [] then {Void} else {})"
|
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
736 |
and "CPT (CHAR c) [d] = (if c = d then {Char c} else {})"
|
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
737 |
and "CPT (ALT r1 r2) s = Left ` CPT r1 s \<union> Right ` CPT r2 s" |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
738 |
and "CPT (SEQ r1 r2) s = |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
739 |
{Seq v1 v2 | v1 v2 s1 s2. s1 @ s2 = s \<and> v1 \<in> CPT r1 s1 \<and> v2 \<in> CPT r2 s2}"
|
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
740 |
apply - |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
741 |
apply(rule subset_antisym) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
742 |
apply(auto simp add: CPT_def)[1] |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
743 |
apply(erule CPrf.cases) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
744 |
apply(simp_all)[7] |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
745 |
apply(erule CPrf.cases) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
746 |
apply(simp_all)[7] |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
747 |
apply(auto simp add: CPT_def intro: CPrf.intros)[1] |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
748 |
apply(auto simp add: CPT_def intro: CPrf.intros)[1] |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
749 |
apply(erule CPrf.cases) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
750 |
apply(simp_all)[7] |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
751 |
apply(erule CPrf.cases) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
752 |
apply(simp_all)[7] |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
753 |
apply(auto simp add: CPT_def image_def intro: CPrf.intros)[1] |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
754 |
apply(erule CPrf.cases) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
755 |
apply(simp_all)[7] |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
756 |
apply(clarify) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
757 |
apply blast |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
758 |
apply(auto simp add: CPT_def image_def intro: CPrf.intros)[1] |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
759 |
apply(erule CPrf.cases) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
760 |
apply(simp_all)[7] |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
761 |
done |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
762 |
|
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
763 |
lemma test: |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
764 |
assumes "finite A" |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
765 |
shows "finite {vs. Stars vs \<in> A}"
|
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
766 |
using assms |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
767 |
apply(induct A) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
768 |
apply(simp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
769 |
apply(auto) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
770 |
apply(case_tac x) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
771 |
apply(simp_all) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
772 |
done |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
773 |
|
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
774 |
lemma CPTpre_STAR_finite: |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
775 |
assumes "\<And>s. finite (CPTpre r s)" |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
776 |
shows "finite (CPTpre (STAR r) s)" |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
777 |
apply(induct s rule: length_induct) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
778 |
apply(case_tac xs) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
779 |
apply(simp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
780 |
apply(simp add: CPTpre_subsets) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
781 |
apply(rule finite_subset) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
782 |
apply(rule CPTpre_subsets) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
783 |
apply(simp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
784 |
apply(rule_tac B="(\<lambda>(v, vs). Stars (v#vs)) ` {(v, vs). v \<in> CPTpre r (a#list) \<and> flat v \<noteq> [] \<and> Stars vs \<in> CPTpre (STAR r) (drop (length (flat v)) (a#list))}" in finite_subset)
|
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
785 |
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
|
786 |
apply(rule finite_imageI) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
787 |
apply(simp add: Collect_case_prod_Sigma) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
788 |
apply(rule finite_SigmaI) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
789 |
apply(rule assms) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
790 |
apply(case_tac "flat v = []") |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
791 |
apply(simp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
792 |
apply(drule_tac x="drop (length (flat v)) (a # list)" in spec) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
793 |
apply(simp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
794 |
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
|
795 |
apply(rule test) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
796 |
apply(simp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
797 |
done |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
798 |
|
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
799 |
lemma CPTpre_finite: |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
800 |
shows "finite (CPTpre r s)" |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
801 |
apply(induct r arbitrary: s) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
802 |
apply(simp add: CPTpre_subsets) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
803 |
apply(rule finite_subset) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
804 |
apply(rule CPTpre_subsets) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
805 |
apply(simp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
806 |
apply(rule finite_subset) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
807 |
apply(rule CPTpre_subsets) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
808 |
apply(simp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
809 |
apply(rule finite_subset) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
810 |
apply(rule CPTpre_subsets) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
811 |
apply(rule_tac B="(\<lambda>(v1, v2). Seq v1 v2) ` {(v1, v2). v1 \<in> CPTpre r1 s \<and> v2 \<in> CPTpre r2 (drop (length (flat v1)) s)}" in finite_subset)
|
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
812 |
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
|
813 |
apply(rule finite_imageI) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
814 |
apply(simp add: Collect_case_prod_Sigma) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
815 |
apply(rule finite_subset) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
816 |
apply(rule CPTpre_subsets) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
817 |
apply(simp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
818 |
by (simp add: CPTpre_STAR_finite) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
819 |
|
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
820 |
|
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
821 |
lemma CPT_finite: |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
822 |
shows "finite (CPT r s)" |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
823 |
apply(rule finite_subset) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
824 |
apply(rule CPT_CPTpre_subset) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
825 |
apply(rule CPTpre_finite) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
826 |
done |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
827 |
|
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
828 |
lemma Posix_CPT: |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
829 |
assumes "s \<in> r \<rightarrow> v" |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
830 |
shows "v \<in> CPT r s" |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
831 |
using assms |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
832 |
apply(induct rule: Posix.induct) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
833 |
apply(simp add: CPT_def) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
834 |
apply(rule CPrf.intros) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
835 |
apply(simp add: CPT_def) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
836 |
apply(rule CPrf.intros) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
837 |
apply(simp add: CPT_def) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
838 |
apply(rule CPrf.intros) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
839 |
apply(simp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
840 |
apply(simp add: CPT_def) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
841 |
apply(rule CPrf.intros) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
842 |
apply(simp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
843 |
apply(simp add: CPT_def) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
844 |
apply(rule CPrf.intros) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
845 |
apply(simp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
846 |
apply(simp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
847 |
apply(simp add: CPT_def) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
848 |
apply(rule CPrf.intros) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
849 |
apply(simp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
850 |
apply(simp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
851 |
apply(simp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
852 |
apply(simp add: CPT_def) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
853 |
apply(rule CPrf.intros) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
854 |
done |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
855 |
|
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
856 |
lemma Posix_val_ord: |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
857 |
assumes "s \<in> r \<rightarrow> v1" "v2 \<in> CPTpre r s" |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
858 |
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
|
859 |
using assms |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
860 |
apply(induct arbitrary: v2 rule: Posix.induct) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
861 |
apply(simp add: CPTpre_def) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
862 |
apply(clarify) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
863 |
apply(erule CPrf.cases) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
864 |
apply(simp_all) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
865 |
apply(simp add: val_ord_ex1_def) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
866 |
apply(simp add: CPTpre_def) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
867 |
apply(clarify) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
868 |
apply(erule CPrf.cases) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
869 |
apply(simp_all) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
870 |
apply(simp add: val_ord_ex1_def) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
871 |
(* ALT1 *) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
872 |
prefer 3 |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
873 |
(* SEQ case *) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
874 |
apply(subst (asm) (3) CPTpre_def) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
875 |
apply(clarify) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
876 |
apply(erule CPrf.cases) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
877 |
apply(simp_all) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
878 |
apply(case_tac "s' = []") |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
879 |
apply(simp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
880 |
prefer 2 |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
881 |
apply(simp add: val_ord_ex1_def) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
882 |
apply(clarify) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
883 |
apply(simp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
884 |
apply(simp add: val_ord_ex_def) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
885 |
apply(simp (no_asm) add: val_ord_def) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
886 |
apply(rule_tac x="[]" in exI) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
887 |
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
|
888 |
apply(rule intlen_length) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
889 |
apply (metis Posix1(2) append_assoc append_eq_conv_conj drop_eq_Nil not_le) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
890 |
apply(subgoal_tac "length (flat v1a) \<le> length s1") |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
891 |
prefer 2 |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
892 |
apply (metis L_flat_Prf1 Prf_CPrf append_eq_append_conv_if append_take_drop_id drop_eq_Nil) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
893 |
apply(subst (asm) append_eq_append_conv_if) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
894 |
apply(simp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
895 |
apply(clarify) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
896 |
apply(drule_tac x="v1a" in meta_spec) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
897 |
apply(drule meta_mp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
898 |
apply(auto simp add: CPTpre_def)[1] |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
899 |
using append_eq_conv_conj apply blast |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
900 |
apply(subst (asm) (2)val_ord_ex1_def) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
901 |
apply(erule disjE) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
902 |
apply(subst val_ord_ex1_def) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
903 |
apply(rule disjI1) |
| 252 | 904 |
apply(rule val_ord_SeqI1) |
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
905 |
apply(simp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
906 |
apply(simp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
907 |
apply (metis Posix1(2) append_assoc append_take_drop_id) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
908 |
apply(simp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
909 |
apply(drule_tac x="v2b" in meta_spec) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
910 |
apply(drule meta_mp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
911 |
apply(auto simp add: CPTpre_def)[1] |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
912 |
apply (simp add: Posix1(2)) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
913 |
apply(subst (asm) val_ord_ex1_def) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
914 |
apply(erule disjE) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
915 |
apply(subst val_ord_ex1_def) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
916 |
apply(rule disjI1) |
| 252 | 917 |
apply(rule val_ord_SeqI2) |
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
918 |
apply(simp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
919 |
apply (simp add: Posix1(2)) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
920 |
apply(subst val_ord_ex1_def) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
921 |
apply(simp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
922 |
(* ALT *) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
923 |
apply(subst (asm) (2) CPTpre_def) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
924 |
apply(clarify) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
925 |
apply(erule CPrf.cases) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
926 |
apply(simp_all) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
927 |
apply(clarify) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
928 |
apply(case_tac "s' = []") |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
929 |
apply(simp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
930 |
apply(drule_tac x="v1" in meta_spec) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
931 |
apply(drule meta_mp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
932 |
apply(auto simp add: CPTpre_def)[1] |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
933 |
apply(subst (asm) val_ord_ex1_def) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
934 |
apply(erule disjE) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
935 |
apply(subst (asm) val_ord_ex_def) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
936 |
apply(erule exE) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
937 |
apply(subst val_ord_ex1_def) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
938 |
apply(rule disjI1) |
| 251 | 939 |
apply(rule val_ord_LeftI) |
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
940 |
apply(subst val_ord_ex_def) |
| 251 | 941 |
apply(auto)[1] |
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
942 |
using Posix1(2) apply blast |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
943 |
using val_ord_ex1_def apply blast |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
944 |
apply(subst val_ord_ex1_def) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
945 |
apply(rule disjI1) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
946 |
apply (simp add: Posix1(2) val_ord_shorterI) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
947 |
apply(subst val_ord_ex1_def) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
948 |
apply(rule disjI1) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
949 |
apply(case_tac "s' = []") |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
950 |
apply(simp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
951 |
apply(subst val_ord_ex_def) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
952 |
apply(rule_tac x="[0]" in exI) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
953 |
apply(subst val_ord_def) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
954 |
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
|
955 |
apply(simp add: Pos_empty) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
956 |
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
|
957 |
apply(simp add: pflat_len_simps) |
| 255 | 958 |
apply (smt intlen_bigger) |
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
959 |
apply(simp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
960 |
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
|
961 |
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
|
962 |
using Posix1(2) 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
|
963 |
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
|
964 |
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
|
965 |
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
|
966 |
using Posix1(2) 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
|
967 |
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
|
968 |
apply(rule val_ord_shorterI) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
969 |
apply(simp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
970 |
apply (simp add: Posix1(2)) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
971 |
(* ALT RIGHT *) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
972 |
apply(subst (asm) (2) CPTpre_def) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
973 |
apply(clarify) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
974 |
apply(erule CPrf.cases) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
975 |
apply(simp_all) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
976 |
apply(clarify) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
977 |
apply(case_tac "s' = []") |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
978 |
apply(simp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
979 |
apply (simp add: L_flat_Prf1 Prf_CPrf) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
980 |
apply(subst val_ord_ex1_def) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
981 |
apply(rule disjI1) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
982 |
apply(rule val_ord_shorterI) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
983 |
apply(simp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
984 |
apply (simp add: Posix1(2)) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
985 |
apply(case_tac "s' = []") |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
986 |
apply(simp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
987 |
apply(drule_tac x="v2a" in meta_spec) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
988 |
apply(drule meta_mp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
989 |
apply(auto simp add: CPTpre_def)[1] |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
990 |
apply(subst (asm) val_ord_ex1_def) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
991 |
apply(erule disjE) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
992 |
apply(subst val_ord_ex1_def) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
993 |
apply(rule disjI1) |
| 251 | 994 |
apply(rule val_ord_RightI) |
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
995 |
apply(simp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
996 |
using Posix1(2) apply blast |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
997 |
apply (simp add: val_ord_ex1_def) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
998 |
apply(subst val_ord_ex1_def) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
999 |
apply(rule disjI1) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1000 |
apply(rule val_ord_shorterI) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1001 |
apply(simp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1002 |
apply (simp add: Posix1(2)) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1003 |
(* STAR empty case *) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1004 |
prefer 2 |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1005 |
apply(subst (asm) CPTpre_def) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1006 |
apply(clarify) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1007 |
apply(erule CPrf.cases) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1008 |
apply(simp_all) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1009 |
apply(clarify) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1010 |
apply (simp add: val_ord_ex1_def) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1011 |
(* STAR non-empty case *) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1012 |
apply(subst (asm) (3) CPTpre_def) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1013 |
apply(clarify) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1014 |
apply(erule CPrf.cases) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1015 |
apply(simp_all) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1016 |
apply(clarify) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1017 |
apply (simp add: val_ord_ex1_def) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1018 |
apply(rule val_ord_shorterI) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1019 |
apply(simp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1020 |
apply(case_tac "s' = []") |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1021 |
apply(simp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1022 |
prefer 2 |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1023 |
apply (simp add: val_ord_ex1_def) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1024 |
apply(rule disjI1) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1025 |
apply(rule val_ord_shorterI) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1026 |
apply(simp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1027 |
apply (metis Posix1(2) append_assoc append_eq_conv_conj drop_all flat.simps(7) flat_Stars length_append not_less) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1028 |
apply(drule_tac x="va" in meta_spec) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1029 |
apply(drule meta_mp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1030 |
apply(auto simp add: CPTpre_def)[1] |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1031 |
apply (smt L.simps(6) L_flat_Prf1 Prf_CPrf append_eq_append_conv2 flat_Stars self_append_conv) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1032 |
apply (subst (asm) (2) val_ord_ex1_def) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1033 |
apply(erule disjE) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1034 |
prefer 2 |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1035 |
apply(simp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1036 |
apply(drule_tac x="Stars vsa" in meta_spec) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1037 |
apply(drule meta_mp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1038 |
apply(auto simp add: CPTpre_def)[1] |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1039 |
apply (simp add: Posix1(2)) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1040 |
apply (subst (asm) val_ord_ex1_def) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1041 |
apply(erule disjE) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1042 |
apply (subst val_ord_ex1_def) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1043 |
apply(rule disjI1) |
| 253 | 1044 |
apply(rule val_ord_StarsI2) |
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1045 |
apply(simp) |
| 253 | 1046 |
using Posix1(2) apply force |
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1047 |
apply(simp add: val_ord_ex1_def) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1048 |
apply (subst val_ord_ex1_def) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1049 |
apply(rule disjI1) |
| 253 | 1050 |
apply(rule val_ord_StarsI) |
1051 |
apply(simp) |
|
1052 |
apply(simp add: Posix1) |
|
1053 |
using Posix1(2) by force |
|
1054 |
||
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1055 |
|
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1056 |
lemma Posix_val_ord_stronger: |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1057 |
assumes "s \<in> r \<rightarrow> v1" "v2 \<in> CPT r s" |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1058 |
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
|
1059 |
using assms |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1060 |
apply(rule_tac Posix_val_ord) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1061 |
apply(assumption) |
| 254 | 1062 |
using CPT_CPTpre_subset by auto |
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1063 |
|
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1064 |
|
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1065 |
lemma Posix_val_ord_reverse: |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1066 |
assumes "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
|
1067 |
shows "\<not>(\<exists>v2 \<in> CPT r s. v2 :\<sqsubset>val v1)" |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1068 |
using assms |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1069 |
by (metis Posix_val_ord_stronger less_irrefl val_ord_def |
| 254 | 1070 |
val_ord_ex1_def val_ord_ex_def val_ord_trans) |
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1071 |
|
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1072 |
|
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1073 |
lemma val_ord_Posix_Stars: |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1074 |
assumes "(Stars vs) \<in> CPT (STAR r) (flat (Stars vs))" "\<forall>v \<in> set vs. flat v \<in> r \<rightarrow> v" |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1075 |
and "\<not>(\<exists>vs2 \<in> PT (STAR r) (flat (Stars vs)). vs2 :\<sqsubset>val (Stars vs))" |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1076 |
shows "(flat (Stars vs)) \<in> (STAR r) \<rightarrow> Stars vs" |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1077 |
using assms |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1078 |
apply(induct vs) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1079 |
apply(simp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1080 |
apply(rule Posix.intros) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1081 |
apply(simp (no_asm)) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1082 |
apply(rule Posix.intros) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1083 |
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
|
1084 |
apply(auto simp add: CPT_def PT_def)[1] |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1085 |
defer |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1086 |
apply(simp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1087 |
apply(drule meta_mp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1088 |
apply(auto simp add: CPT_def PT_def)[1] |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1089 |
apply(erule CPrf.cases) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1090 |
apply(simp_all) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1091 |
apply(drule meta_mp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1092 |
apply(auto simp add: CPT_def PT_def)[1] |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1093 |
apply(erule Prf.cases) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1094 |
apply(simp_all) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1095 |
apply (metis CPrf_stars Cons_eq_map_conv Posix_CPT Posix_STAR2 Posix_val_ord_reverse list.exhaust list.set_intros(2) map_idI val.distinct(25)) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1096 |
apply(clarify) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1097 |
apply(drule_tac x="Stars (a#v#vsa)" in spec) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1098 |
apply(simp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1099 |
apply(drule mp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1100 |
apply (meson CPrf_stars Prf.intros(7) Prf_CPrf list.set_intros(1)) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1101 |
apply(subst (asm) (2) val_ord_ex_def) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1102 |
apply(simp) |
| 253 | 1103 |
apply (metis flat.simps(7) flat_Stars val_ord_StarsI2 val_ord_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
|
1104 |
apply(auto simp add: CPT_def PT_def)[1] |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1105 |
using CPrf_stars 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
|
1106 |
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
|
1107 |
apply(auto simp add: CPT_def PT_def)[1] |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1108 |
apply(subgoal_tac "\<exists>vA. flat vA = flat a @ s\<^sub>3 \<and> \<turnstile> vA : r") |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1109 |
prefer 2 |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1110 |
apply (meson L_flat_Prf2) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1111 |
apply(subgoal_tac "\<exists>vB. flat (Stars vB) = s\<^sub>4 \<and> \<turnstile> (Stars vB) : (STAR r)") |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1112 |
apply(clarify) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1113 |
apply(drule_tac x="Stars (vA # vB)" in spec) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1114 |
apply(simp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1115 |
apply(drule mp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1116 |
using Prf.intros(7) apply blast |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1117 |
apply(subst (asm) (2) val_ord_ex_def) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1118 |
apply(simp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1119 |
prefer 2 |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1120 |
apply(simp) |
| 254 | 1121 |
using Star_values_exists apply blast |
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1122 |
prefer 2 |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1123 |
apply(drule meta_mp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1124 |
apply(erule CPrf.cases) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1125 |
apply(simp_all) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1126 |
apply(drule meta_mp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1127 |
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
|
1128 |
prefer 2 |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1129 |
apply(simp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1130 |
apply(erule CPrf.cases) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1131 |
apply(simp_all) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1132 |
apply(clarify) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1133 |
apply(rotate_tac 3) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1134 |
apply(erule Prf.cases) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1135 |
apply(simp_all) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1136 |
apply (metis CPrf_stars intlen.cases less_irrefl list.set_intros(1) val_ord_def val_ord_ex_def) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1137 |
apply(drule_tac x="Stars (v#va#vsb)" in spec) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1138 |
apply(drule mp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1139 |
apply (simp add: Posix1a Prf.intros(7)) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1140 |
apply(simp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1141 |
apply(subst (asm) (2) val_ord_ex_def) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1142 |
apply(simp) |
| 253 | 1143 |
apply (metis flat.simps(7) flat_Stars val_ord_StarsI2 val_ord_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
|
1144 |
proof - |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1145 |
fix a :: val and vsa :: "val list" and s\<^sub>3 :: "char list" and vA :: val and vB :: "val list" |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1146 |
assume a1: "s\<^sub>3 \<noteq> []" |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1147 |
assume a2: "s\<^sub>3 @ concat (map flat vB) = concat (map flat vsa)" |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1148 |
assume a3: "flat vA = flat a @ s\<^sub>3" |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1149 |
assume a4: "\<forall>p. \<not> Stars (vA # vB) \<sqsubset>val p Stars (a # vsa)" |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1150 |
have f5: "\<And>n cs. drop n (cs::char list) = [] \<or> n < length cs" |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1151 |
by (meson drop_eq_Nil not_less) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1152 |
have f6: "\<not> length (flat vA) \<le> length (flat a)" |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1153 |
using a3 a1 by simp |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1154 |
have "flat (Stars (a # vsa)) = flat (Stars (vA # vB))" |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1155 |
using a3 a2 by simp |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1156 |
then show False |
| 253 | 1157 |
using f6 f5 a4 by (metis (full_types) drop_eq_Nil val_ord_StarsI val_ord_ex_def val_ord_shorterI) |
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1158 |
qed |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1159 |
|
| 254 | 1160 |
|
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1161 |
|
| 254 | 1162 |
|
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1163 |
|
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1164 |
lemma val_ord_Posix: |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1165 |
assumes "v1 \<in> CPT r s" "\<not>(\<exists>v2 \<in> PT r s. v2 :\<sqsubset>val v1)" |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1166 |
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
|
1167 |
using assms |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1168 |
apply(induct r arbitrary: s v1) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1169 |
apply(auto simp add: CPT_def PT_def)[1] |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1170 |
apply(erule CPrf.cases) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1171 |
apply(simp_all) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1172 |
(* ONE *) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1173 |
apply(auto simp add: CPT_def)[1] |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1174 |
apply(erule CPrf.cases) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1175 |
apply(simp_all) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1176 |
apply(rule Posix.intros) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1177 |
(* CHAR *) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1178 |
apply(auto simp add: CPT_def)[1] |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1179 |
apply(erule CPrf.cases) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1180 |
apply(simp_all) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1181 |
apply(rule Posix.intros) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1182 |
prefer 2 |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1183 |
(* ALT *) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1184 |
apply(auto simp add: CPT_def PT_def)[1] |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1185 |
apply(erule CPrf.cases) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1186 |
apply(simp_all) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1187 |
apply(rule Posix.intros) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1188 |
apply(drule_tac x="flat v1a" in meta_spec) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1189 |
apply(drule_tac x="v1a" in meta_spec) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1190 |
apply(drule meta_mp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1191 |
apply(simp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1192 |
apply(drule meta_mp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1193 |
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
|
1194 |
apply(drule_tac x="Left v2" in spec) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1195 |
apply(simp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1196 |
apply(drule mp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1197 |
apply(rule Prf.intros) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1198 |
apply(simp) |
| 251 | 1199 |
apply (meson val_ord_LeftI) |
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1200 |
apply(assumption) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1201 |
(* ALT Right *) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1202 |
apply(auto simp add: CPT_def)[1] |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1203 |
apply(rule Posix.intros) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1204 |
apply(rotate_tac 1) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1205 |
apply(drule_tac x="flat v2" in meta_spec) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1206 |
apply(drule_tac x="v2" in meta_spec) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1207 |
apply(drule meta_mp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1208 |
apply(simp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1209 |
apply(drule meta_mp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1210 |
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
|
1211 |
apply(drule_tac x="Right v2a" in spec) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1212 |
apply(simp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1213 |
apply(drule mp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1214 |
apply(rule Prf.intros) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1215 |
apply(simp) |
| 251 | 1216 |
apply(drule val_ord_RightI) |
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1217 |
apply(assumption) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1218 |
apply(auto simp add: val_ord_ex_def)[1] |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1219 |
apply(assumption) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1220 |
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
|
1221 |
apply(subgoal_tac "\<exists>v2'. flat v2' = flat v2 \<and> \<turnstile> v2' : r1a") |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1222 |
apply(clarify) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1223 |
apply(drule_tac x="Left v2'" in spec) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1224 |
apply(simp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1225 |
apply(drule mp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1226 |
apply(rule Prf.intros) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1227 |
apply(assumption) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1228 |
apply(simp add: val_ord_ex_def) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1229 |
apply(subst (asm) (3) val_ord_def) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1230 |
apply(simp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1231 |
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
|
1232 |
apply(drule_tac x="[0]" in spec) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1233 |
apply(simp add: pflat_len_simps Pos_empty) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1234 |
apply(drule mp) |
| 255 | 1235 |
apply (smt intlen_bigger) |
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1236 |
apply(erule disjE) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1237 |
apply blast |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1238 |
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
|
1239 |
apply (meson L_flat_Prf2) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1240 |
(* SEQ *) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1241 |
apply(auto simp add: CPT_def)[1] |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1242 |
apply(erule CPrf.cases) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1243 |
apply(simp_all) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1244 |
apply(rule Posix.intros) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1245 |
apply(drule_tac x="flat v1a" in meta_spec) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1246 |
apply(drule_tac x="v1a" in meta_spec) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1247 |
apply(drule meta_mp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1248 |
apply(simp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1249 |
apply(drule meta_mp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1250 |
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
|
1251 |
apply(auto simp add: PT_def)[1] |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1252 |
apply(drule_tac x="Seq v2a v2" in spec) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1253 |
apply(simp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1254 |
apply(drule mp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1255 |
apply (simp add: Prf.intros(1) Prf_CPrf) |
| 252 | 1256 |
using val_ord_SeqI1 apply fastforce |
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1257 |
apply(assumption) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1258 |
apply(rotate_tac 1) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1259 |
apply(drule_tac x="flat v2" in meta_spec) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1260 |
apply(drule_tac x="v2" in meta_spec) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1261 |
apply(simp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1262 |
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
|
1263 |
apply(drule meta_mp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1264 |
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
|
1265 |
apply(auto simp add: PT_def)[1] |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1266 |
apply(drule_tac x="Seq v1a v2a" in spec) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1267 |
apply(simp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1268 |
apply(drule mp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1269 |
apply (simp add: Prf.intros(1) Prf_CPrf) |
| 252 | 1270 |
apply (meson val_ord_SeqI2) |
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1271 |
apply(assumption) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1272 |
(* SEQ side condition *) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1273 |
apply(auto simp add: PT_def) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1274 |
apply(subgoal_tac "\<exists>vA. flat vA = flat v1a @ s\<^sub>3 \<and> \<turnstile> vA : r1a") |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1275 |
prefer 2 |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1276 |
apply (meson L_flat_Prf2) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1277 |
apply(subgoal_tac "\<exists>vB. flat vB = s\<^sub>4 \<and> \<turnstile> vB : r2a") |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1278 |
prefer 2 |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1279 |
apply (meson L_flat_Prf2) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1280 |
apply(clarify) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1281 |
apply(drule_tac x="Seq vA vB" in spec) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1282 |
apply(simp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1283 |
apply(drule mp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1284 |
apply (simp add: Prf.intros(1)) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1285 |
apply(subst (asm) (3) val_ord_ex_def) |
| 252 | 1286 |
apply (metis append_Nil2 append_assoc append_eq_conv_conj flat.simps(5) length_append not_add_less1 not_less_iff_gr_or_eq val_ord_SeqI1 val_ord_ex_def val_ord_shorterI) |
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1287 |
(* STAR *) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1288 |
apply(auto simp add: CPT_def)[1] |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1289 |
apply(erule CPrf.cases) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1290 |
apply(simp_all)[6] |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1291 |
using Posix_STAR2 apply blast |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1292 |
apply(clarify) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1293 |
apply(rule val_ord_Posix_Stars) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1294 |
apply(auto simp add: CPT_def)[1] |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1295 |
apply (simp add: CPrf.intros(7)) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1296 |
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
|
1297 |
apply(drule_tac x="flat v" in meta_spec) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1298 |
apply(drule_tac x="v" in meta_spec) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1299 |
apply(simp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1300 |
apply(drule meta_mp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1301 |
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
|
1302 |
apply(drule_tac x="Stars (v2#vs)" in spec) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1303 |
apply(simp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1304 |
apply(drule mp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1305 |
using Prf.intros(7) Prf_CPrf apply blast |
| 253 | 1306 |
apply(simp add: val_ord_StarsI) |
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1307 |
apply(assumption) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1308 |
apply(drule_tac x="flat va" in meta_spec) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1309 |
apply(drule_tac x="va" in meta_spec) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1310 |
apply(simp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1311 |
apply(drule meta_mp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1312 |
using CPrf_stars apply blast |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1313 |
apply(drule meta_mp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1314 |
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
|
1315 |
apply(subgoal_tac "\<exists>pre post. vs = pre @ [va] @ post") |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1316 |
prefer 2 |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1317 |
apply (metis append_Cons append_Nil in_set_conv_decomp_first) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1318 |
apply(clarify) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1319 |
apply(drule_tac x="Stars (v#(pre @ [v2] @ post))" in spec) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1320 |
apply(simp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1321 |
apply(drule mp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1322 |
apply(rule Prf.intros) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1323 |
apply (simp add: Prf_CPrf) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1324 |
apply(rule Prf_Stars_append) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1325 |
apply(drule CPrf_Stars_appendE) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1326 |
apply(auto simp add: Prf_CPrf)[1] |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1327 |
apply (metis CPrf_Stars_appendE CPrf_stars Prf_CPrf Prf_Stars list.set_intros(2) set_ConsD) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1328 |
apply(subgoal_tac "\<not> Stars ([v] @ pre @ v2 # post) :\<sqsubset>val Stars ([v] @ pre @ va # post)") |
| 254 | 1329 |
apply(subst (asm) val_ord_Stars_append_eq) |
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1330 |
apply(simp) |
| 254 | 1331 |
apply(subst (asm) val_ord_Stars_append_eq) |
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1332 |
apply(simp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1333 |
prefer 2 |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1334 |
apply(simp) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1335 |
prefer 2 |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1336 |
apply(simp) |
| 253 | 1337 |
apply (simp add: val_ord_StarsI) |
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1338 |
apply(auto simp add: PT_def) |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1339 |
done |
|
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1340 |
|
| 249 | 1341 |
unused_thms |
1342 |
||
|
248
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1343 |
end |