89
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1
220
+ − 2
theory LexerExt
276
+ − 3
imports SpecExt
89
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 4
begin
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 5
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 6
276
+ − 7
section {* The Lexer Functions by Sulzmann and Lu *}
89
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 8
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 9
fun
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 10
mkeps :: "rexp \<Rightarrow> val"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 11
where
107
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 12
"mkeps(ONE) = Void"
89
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 13
| "mkeps(SEQ r1 r2) = Seq (mkeps r1) (mkeps r2)"
276
+ − 14
| "mkeps(ALT r1 r2) = (if nullable(r1) then Left (mkeps r1) else Right (mkeps r2))"
97
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 15
| "mkeps(STAR r) = Stars []"
220
+ − 16
| "mkeps(UPNTIMES r n) = Stars []"
221
+ − 17
| "mkeps(NTIMES r n) = Stars (replicate n (mkeps r))"
223
+ − 18
| "mkeps(FROMNTIMES r n) = Stars (replicate n (mkeps r))"
227
+ − 19
| "mkeps(NMTIMES r n m) = Stars (replicate n (mkeps r))"
397
+ − 20
| "mkeps(NOT ZERO) = Nt Void"
+ − 21
| "mkeps(NOT (CH _ )) = Nt Void"
+ − 22
| "mkeps(NOT (SEQ r1 r2)) = Seq (mkeps (NOT r1)) (mkeps (NOT r1))"
+ − 23
| "mkeps(NOT (ALT r1 r2)) = (if nullable(r1) then Right (mkeps (NOT r2)) else (mkeps (NOT r1)))"
+ − 24
+ − 25
89
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 26
fun injval :: "rexp \<Rightarrow> char \<Rightarrow> val \<Rightarrow> val"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 27
where
397
+ − 28
"injval (CH d) c Void = Char d"
89
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 29
| "injval (ALT r1 r2) c (Left v1) = Left(injval r1 c v1)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 30
| "injval (ALT r1 r2) c (Right v2) = Right(injval r2 c v2)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 31
| "injval (SEQ r1 r2) c (Seq v1 v2) = Seq (injval r1 c v1) v2"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 32
| "injval (SEQ r1 r2) c (Left (Seq v1 v2)) = Seq (injval r1 c v1) v2"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 33
| "injval (SEQ r1 r2) c (Right v2) = Seq (mkeps r1) (injval r2 c v2)"
97
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 34
| "injval (STAR r) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)"
276
+ − 35
| "injval (NTIMES r n) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)"
+ − 36
| "injval (FROMNTIMES r n) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)"
+ − 37
| "injval (UPNTIMES r n) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)"
+ − 38
| "injval (NMTIMES r n m) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)"
+ − 39
+ − 40
fun
+ − 41
lexer :: "rexp \<Rightarrow> string \<Rightarrow> val option"
+ − 42
where
+ − 43
"lexer r [] = (if nullable r then Some(mkeps r) else None)"
+ − 44
| "lexer r (c#s) = (case (lexer (der c r) s) of
+ − 45
None \<Rightarrow> None
+ − 46
| Some(v) \<Rightarrow> Some(injval r c v))"
107
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 47
276
+ − 48
+ − 49
+ − 50
section {* Mkeps, Injval Properties *}
243
+ − 51
89
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 52
lemma mkeps_flat:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 53
assumes "nullable(r)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 54
shows "flat (mkeps r) = []"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 55
using assms
276
+ − 56
apply(induct rule: nullable.induct)
397
+ − 57
apply(auto)
+ − 58
apply presburger
+ − 59
apply(case_tac r)
+ − 60
apply(auto)
+ − 61
sorry
276
+ − 62
+ − 63
lemma mkeps_nullable:
+ − 64
assumes "nullable(r)"
+ − 65
shows "\<Turnstile> mkeps r : r"
89
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 66
using assms
276
+ − 67
apply(induct rule: nullable.induct)
+ − 68
apply(auto intro: Prf.intros split: if_splits)
+ − 69
using Prf.intros(8) apply force
+ − 70
apply(subst append.simps(1)[symmetric])
+ − 71
apply(rule Prf.intros)
+ − 72
apply(simp)
+ − 73
apply(simp)
+ − 74
apply (simp add: mkeps_flat)
+ − 75
apply(simp)
+ − 76
using Prf.intros(9) apply force
+ − 77
apply(subst append.simps(1)[symmetric])
+ − 78
apply(rule Prf.intros)
+ − 79
apply(simp)
+ − 80
apply(simp)
+ − 81
apply (simp add: mkeps_flat)
+ − 82
apply(simp)
+ − 83
using Prf.intros(11) apply force
+ − 84
apply(subst append.simps(1)[symmetric])
+ − 85
apply(rule Prf.intros)
+ − 86
apply(simp)
+ − 87
apply(simp)
+ − 88
apply (simp add: mkeps_flat)
+ − 89
apply(simp)
+ − 90
apply(simp)
397
+ − 91
sorry
276
+ − 92
89
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 93
243
+ − 94
lemma Prf_injval_flat:
276
+ − 95
assumes "\<Turnstile> v : der c r"
243
+ − 96
shows "flat (injval r c v) = c # (flat v)"
+ − 97
using assms
+ − 98
apply(induct arbitrary: v rule: der.induct)
276
+ − 99
apply(auto elim!: Prf_elims intro: mkeps_flat split: if_splits)
397
+ − 100
sorry
276
+ − 101
+ − 102
lemma Prf_injval:
+ − 103
assumes "\<Turnstile> v : der c r"
+ − 104
shows "\<Turnstile> (injval r c v) : r"
+ − 105
using assms
+ − 106
apply(induct r arbitrary: c v rule: rexp.induct)
+ − 107
apply(auto intro!: Prf.intros mkeps_nullable elim!: Prf_elims split: if_splits)[6]
+ − 108
apply(simp add: Prf_injval_flat)
+ − 109
apply(simp)
+ − 110
apply(case_tac x2)
+ − 111
apply(simp)
+ − 112
apply(erule Prf_elims)
+ − 113
apply(simp)
+ − 114
apply(erule Prf_elims)
+ − 115
apply(simp)
+ − 116
apply(erule Prf_elims)
+ − 117
apply(simp)
+ − 118
using Prf.intros(7) Prf_injval_flat apply auto[1]
+ − 119
apply(simp)
+ − 120
apply(case_tac x2)
+ − 121
apply(simp)
+ − 122
apply(erule Prf_elims)
+ − 123
apply(simp)
+ − 124
apply(erule Prf_elims)
+ − 125
apply(simp)
+ − 126
apply(erule Prf_elims)
+ − 127
apply(simp)
+ − 128
apply(subst append.simps(2)[symmetric])
+ − 129
apply(rule Prf.intros)
+ − 130
apply(simp add: Prf_injval_flat)
+ − 131
apply(simp)
+ − 132
apply(simp)
+ − 133
prefer 2
+ − 134
apply(simp)
+ − 135
apply(case_tac "x3a < x2")
+ − 136
apply(simp)
+ − 137
apply(erule Prf_elims)
+ − 138
apply(simp)
+ − 139
apply(case_tac x2)
+ − 140
apply(simp)
+ − 141
apply(case_tac x3a)
+ − 142
apply(simp)
+ − 143
apply(erule Prf_elims)
+ − 144
apply(simp)
+ − 145
apply(erule Prf_elims)
+ − 146
apply(simp)
+ − 147
apply(erule Prf_elims)
+ − 148
apply(simp)
+ − 149
using Prf.intros(12) Prf_injval_flat apply auto[1]
+ − 150
apply(simp)
+ − 151
apply(erule Prf_elims)
+ − 152
apply(simp)
+ − 153
apply(erule Prf_elims)
+ − 154
apply(simp)
+ − 155
apply(subst append.simps(2)[symmetric])
+ − 156
apply(rule Prf.intros)
+ − 157
apply(simp add: Prf_injval_flat)
+ − 158
apply(simp)
+ − 159
apply(simp)
+ − 160
apply(simp)
+ − 161
apply(simp)
+ − 162
using Prf.intros(12) Prf_injval_flat apply auto[1]
+ − 163
apply(case_tac x2)
+ − 164
apply(simp)
+ − 165
apply(erule Prf_elims)
+ − 166
apply(simp)
+ − 167
apply(erule Prf_elims)
+ − 168
apply(simp_all)
+ − 169
apply (simp add: Prf.intros(10) Prf_injval_flat)
+ − 170
using Prf.intros(10) Prf_injval_flat apply auto[1]
+ − 171
apply(erule Prf_elims)
+ − 172
apply(simp)
+ − 173
apply(erule Prf_elims)
+ − 174
apply(simp_all)
+ − 175
apply(subst append.simps(2)[symmetric])
+ − 176
apply(rule Prf.intros)
+ − 177
apply(simp add: Prf_injval_flat)
+ − 178
apply(simp)
+ − 179
apply(simp)
397
+ − 180
sorry
+ − 181
89
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 182
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 183
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 184
276
+ − 185
text {*
+ − 186
Mkeps and injval produce, or preserve, Posix values.
+ − 187
*}
223
+ − 188
146
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 189
lemma Posix_mkeps:
89
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 190
assumes "nullable r"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 191
shows "[] \<in> r \<rightarrow> mkeps r"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 192
using assms
185
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 193
apply(induct r rule: nullable.induct)
146
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 194
apply(auto intro: Posix.intros simp add: nullable_correctness Sequ_def)
89
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 195
apply(subst append.simps(1)[symmetric])
146
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 196
apply(rule Posix.intros)
397
+ − 197
apply(auto)
+ − 198
apply(case_tac r)
+ − 199
apply(auto)
+ − 200
sorry
276
+ − 201
100
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 202
172
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 203
lemma Posix_injval:
276
+ − 204
assumes "s \<in> (der c r) \<rightarrow> v"
143
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 205
shows "(c # s) \<in> r \<rightarrow> (injval r c v)"
106
489dfa0d7ec9
more cleaning and moving unnessary stuff to the end
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 206
using assms
121
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 207
proof(induct r arbitrary: s v rule: rexp.induct)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 208
case ZERO
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 209
have "s \<in> der c ZERO \<rightarrow> v" by fact
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 210
then have "s \<in> ZERO \<rightarrow> v" by simp
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 211
then have "False" by cases
143
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 212
then show "(c # s) \<in> ZERO \<rightarrow> (injval ZERO c v)" by simp
121
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 213
next
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 214
case ONE
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 215
have "s \<in> der c ONE \<rightarrow> v" by fact
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 216
then have "s \<in> ZERO \<rightarrow> v" by simp
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 217
then have "False" by cases
143
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 218
then show "(c # s) \<in> ONE \<rightarrow> (injval ONE c v)" by simp
121
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 219
next
397
+ − 220
case (CH d)
121
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 221
consider (eq) "c = d" | (ineq) "c \<noteq> d" by blast
397
+ − 222
then show "(c # s) \<in> (CH d) \<rightarrow> (injval (CH d) c v)"
121
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 223
proof (cases)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 224
case eq
397
+ − 225
have "s \<in> der c (CH d) \<rightarrow> v" by fact
121
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 226
then have "s \<in> ONE \<rightarrow> v" using eq by simp
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 227
then have eqs: "s = [] \<and> v = Void" by cases simp
397
+ − 228
show "(c # s) \<in> CH d \<rightarrow> injval (CH d) c v" using eq eqs
146
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 229
by (auto intro: Posix.intros)
121
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 230
next
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 231
case ineq
397
+ − 232
have "s \<in> der c (CH d) \<rightarrow> v" by fact
121
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 233
then have "s \<in> ZERO \<rightarrow> v" using ineq by simp
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 234
then have "False" by cases
397
+ − 235
then show "(c # s) \<in> CH d \<rightarrow> injval (CH d) c v" by simp
121
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 236
qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 237
next
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 238
case (ALT r1 r2)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 239
have IH1: "\<And>s v. s \<in> der c r1 \<rightarrow> v \<Longrightarrow> (c # s) \<in> r1 \<rightarrow> injval r1 c v" by fact
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 240
have IH2: "\<And>s v. s \<in> der c r2 \<rightarrow> v \<Longrightarrow> (c # s) \<in> r2 \<rightarrow> injval r2 c v" by fact
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 241
have "s \<in> der c (ALT r1 r2) \<rightarrow> v" by fact
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 242
then have "s \<in> ALT (der c r1) (der c r2) \<rightarrow> v" by simp
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 243
then consider (left) v' where "v = Left v'" "s \<in> der c r1 \<rightarrow> v'"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 244
| (right) v' where "v = Right v'" "s \<notin> L (der c r1)" "s \<in> der c r2 \<rightarrow> v'"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 245
by cases auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 246
then show "(c # s) \<in> ALT r1 r2 \<rightarrow> injval (ALT r1 r2) c v"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 247
proof (cases)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 248
case left
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 249
have "s \<in> der c r1 \<rightarrow> v'" by fact
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 250
then have "(c # s) \<in> r1 \<rightarrow> injval r1 c v'" using IH1 by simp
146
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 251
then have "(c # s) \<in> ALT r1 r2 \<rightarrow> injval (ALT r1 r2) c (Left v')" by (auto intro: Posix.intros)
121
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 252
then show "(c # s) \<in> ALT r1 r2 \<rightarrow> injval (ALT r1 r2) c v" using left by simp
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 253
next
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 254
case right
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 255
have "s \<notin> L (der c r1)" by fact
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 256
then have "c # s \<notin> L r1" by (simp add: der_correctness Der_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 257
moreover
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 258
have "s \<in> der c r2 \<rightarrow> v'" by fact
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 259
then have "(c # s) \<in> r2 \<rightarrow> injval r2 c v'" using IH2 by simp
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 260
ultimately have "(c # s) \<in> ALT r1 r2 \<rightarrow> injval (ALT r1 r2) c (Right v')"
146
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 261
by (auto intro: Posix.intros)
121
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 262
then show "(c # s) \<in> ALT r1 r2 \<rightarrow> injval (ALT r1 r2) c v" using right by simp
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 263
qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 264
next
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 265
case (SEQ r1 r2)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 266
have IH1: "\<And>s v. s \<in> der c r1 \<rightarrow> v \<Longrightarrow> (c # s) \<in> r1 \<rightarrow> injval r1 c v" by fact
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 267
have IH2: "\<And>s v. s \<in> der c r2 \<rightarrow> v \<Longrightarrow> (c # s) \<in> r2 \<rightarrow> injval r2 c v" by fact
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 268
have "s \<in> der c (SEQ r1 r2) \<rightarrow> v" by fact
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 269
then consider
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 270
(left_nullable) v1 v2 s1 s2 where
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 271
"v = Left (Seq v1 v2)" "s = s1 @ s2"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 272
"s1 \<in> der c r1 \<rightarrow> v1" "s2 \<in> r2 \<rightarrow> v2" "nullable r1"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 273
"\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L (der c r1) \<and> s\<^sub>4 \<in> L r2)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 274
| (right_nullable) v1 s1 s2 where
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 275
"v = Right v1" "s = s1 @ s2"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 276
"s \<in> der c r2 \<rightarrow> v1" "nullable r1" "s1 @ s2 \<notin> L (SEQ (der c r1) r2)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 277
| (not_nullable) v1 v2 s1 s2 where
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 278
"v = Seq v1 v2" "s = s1 @ s2"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 279
"s1 \<in> der c r1 \<rightarrow> v1" "s2 \<in> r2 \<rightarrow> v2" "\<not>nullable r1"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 280
"\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L (der c r1) \<and> s\<^sub>4 \<in> L r2)"
146
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 281
by (force split: if_splits elim!: Posix_elims simp add: Sequ_def der_correctness Der_def)
121
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 282
then show "(c # s) \<in> SEQ r1 r2 \<rightarrow> injval (SEQ r1 r2) c v"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 283
proof (cases)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 284
case left_nullable
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 285
have "s1 \<in> der c r1 \<rightarrow> v1" by fact
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 286
then have "(c # s1) \<in> r1 \<rightarrow> injval r1 c v1" using IH1 by simp
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 287
moreover
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 288
have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L (der c r1) \<and> s\<^sub>4 \<in> L r2)" by fact
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 289
then have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (c # s1) @ s\<^sub>3 \<in> L r1 \<and> s\<^sub>4 \<in> L r2)" by (simp add: der_correctness Der_def)
146
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 290
ultimately have "((c # s1) @ s2) \<in> SEQ r1 r2 \<rightarrow> Seq (injval r1 c v1) v2" using left_nullable by (rule_tac Posix.intros)
121
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 291
then show "(c # s) \<in> SEQ r1 r2 \<rightarrow> injval (SEQ r1 r2) c v" using left_nullable by simp
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 292
next
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 293
case right_nullable
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 294
have "nullable r1" by fact
146
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 295
then have "[] \<in> r1 \<rightarrow> (mkeps r1)" by (rule Posix_mkeps)
121
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 296
moreover
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 297
have "s \<in> der c r2 \<rightarrow> v1" by fact
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 298
then have "(c # s) \<in> r2 \<rightarrow> (injval r2 c v1)" using IH2 by simp
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 299
moreover
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 300
have "s1 @ s2 \<notin> L (SEQ (der c r1) r2)" by fact
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 301
then have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = c # s \<and> [] @ s\<^sub>3 \<in> L r1 \<and> s\<^sub>4 \<in> L r2)" using right_nullable
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 302
by(auto simp add: der_correctness Der_def append_eq_Cons_conv Sequ_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 303
ultimately have "([] @ (c # s)) \<in> SEQ r1 r2 \<rightarrow> Seq (mkeps r1) (injval r2 c v1)"
146
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 304
by(rule Posix.intros)
121
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 305
then show "(c # s) \<in> SEQ r1 r2 \<rightarrow> injval (SEQ r1 r2) c v" using right_nullable by simp
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 306
next
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 307
case not_nullable
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 308
have "s1 \<in> der c r1 \<rightarrow> v1" by fact
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 309
then have "(c # s1) \<in> r1 \<rightarrow> injval r1 c v1" using IH1 by simp
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 310
moreover
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 311
have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L (der c r1) \<and> s\<^sub>4 \<in> L r2)" by fact
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 312
then have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (c # s1) @ s\<^sub>3 \<in> L r1 \<and> s\<^sub>4 \<in> L r2)" by (simp add: der_correctness Der_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 313
ultimately have "((c # s1) @ s2) \<in> SEQ r1 r2 \<rightarrow> Seq (injval r1 c v1) v2" using not_nullable
146
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 314
by (rule_tac Posix.intros) (simp_all)
121
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 315
then show "(c # s) \<in> SEQ r1 r2 \<rightarrow> injval (SEQ r1 r2) c v" using not_nullable by simp
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 316
qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 317
next
276
+ − 318
case (UPNTIMES r n s v)
+ − 319
have IH: "\<And>s v. s \<in> der c r \<rightarrow> v \<Longrightarrow> (c # s) \<in> r \<rightarrow> injval r c v" by fact
+ − 320
have "s \<in> der c (UPNTIMES r n) \<rightarrow> v" by fact
+ − 321
then consider
+ − 322
(cons) v1 vs s1 s2 where
+ − 323
"v = Seq v1 (Stars vs)" "s = s1 @ s2"
+ − 324
"s1 \<in> der c r \<rightarrow> v1" "s2 \<in> (UPNTIMES r (n - 1)) \<rightarrow> (Stars vs)" "0 < n"
+ − 325
"\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L (der c r) \<and> s\<^sub>4 \<in> L (UPNTIMES r (n - 1)))"
+ − 326
(* here *)
+ − 327
apply(auto elim: Posix_elims simp add: der_correctness Der_def intro: Posix.intros split: if_splits)
+ − 328
apply(erule Posix_elims)
+ − 329
apply(simp)
+ − 330
apply(subgoal_tac "\<exists>vss. v2 = Stars vss")
+ − 331
apply(clarify)
+ − 332
apply(drule_tac x="vss" in meta_spec)
+ − 333
apply(drule_tac x="s1" in meta_spec)
+ − 334
apply(drule_tac x="s2" in meta_spec)
+ − 335
apply(simp add: der_correctness Der_def)
+ − 336
apply(erule Posix_elims)
+ − 337
apply(auto)
+ − 338
done
+ − 339
then show "(c # s) \<in> (UPNTIMES r n) \<rightarrow> injval (UPNTIMES r n) c v"
+ − 340
proof (cases)
+ − 341
case cons
+ − 342
have "s1 \<in> der c r \<rightarrow> v1" by fact
+ − 343
then have "(c # s1) \<in> r \<rightarrow> injval r c v1" using IH by simp
+ − 344
moreover
+ − 345
have "s2 \<in> (UPNTIMES r (n - 1)) \<rightarrow> Stars vs" by fact
+ − 346
moreover
+ − 347
have "(c # s1) \<in> r \<rightarrow> injval r c v1" by fact
+ − 348
then have "flat (injval r c v1) = (c # s1)" by (rule Posix1)
+ − 349
then have "flat (injval r c v1) \<noteq> []" by simp
+ − 350
moreover
+ − 351
have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L (der c r) \<and> s\<^sub>4 \<in> L (UPNTIMES r (n - 1)))" by fact
+ − 352
then have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (c # s1) @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (UPNTIMES r (n - 1)))"
+ − 353
by (simp add: der_correctness Der_def)
+ − 354
ultimately
+ − 355
have "((c # s1) @ s2) \<in> UPNTIMES r n \<rightarrow> Stars (injval r c v1 # vs)"
+ − 356
thm Posix.intros
+ − 357
apply (rule_tac Posix.intros)
+ − 358
apply(simp_all)
+ − 359
apply(case_tac n)
+ − 360
apply(simp)
+ − 361
using Posix_elims(1) UPNTIMES.prems apply auto[1]
+ − 362
apply(simp)
+ − 363
done
+ − 364
then show "(c # s) \<in> UPNTIMES r n \<rightarrow> injval (UPNTIMES r n) c v" using cons by(simp)
+ − 365
qed
+ − 366
next
+ − 367
case (STAR r)
121
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 368
have IH: "\<And>s v. s \<in> der c r \<rightarrow> v \<Longrightarrow> (c # s) \<in> r \<rightarrow> injval r c v" by fact
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 369
have "s \<in> der c (STAR r) \<rightarrow> v" by fact
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 370
then consider
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 371
(cons) v1 vs s1 s2 where
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 372
"v = Seq v1 (Stars vs)" "s = s1 @ s2"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 373
"s1 \<in> der c r \<rightarrow> v1" "s2 \<in> (STAR r) \<rightarrow> (Stars vs)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 374
"\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L (der c r) \<and> s\<^sub>4 \<in> L (STAR r))"
149
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 375
apply(auto elim!: Posix_elims(1-5) simp add: der_correctness Der_def intro: Posix.intros)
142
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 376
apply(rotate_tac 3)
149
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 377
apply(erule_tac Posix_elims(6))
146
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 378
apply (simp add: Posix.intros(6))
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 379
using Posix.intros(7) by blast
121
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 380
then show "(c # s) \<in> STAR r \<rightarrow> injval (STAR r) c v"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 381
proof (cases)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 382
case cons
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 383
have "s1 \<in> der c r \<rightarrow> v1" by fact
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 384
then have "(c # s1) \<in> r \<rightarrow> injval r c v1" using IH by simp
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 385
moreover
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 386
have "s2 \<in> STAR r \<rightarrow> Stars vs" by fact
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 387
moreover
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 388
have "(c # s1) \<in> r \<rightarrow> injval r c v1" by fact
146
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 389
then have "flat (injval r c v1) = (c # s1)" by (rule Posix1)
121
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 390
then have "flat (injval r c v1) \<noteq> []" by simp
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 391
moreover
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 392
have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L (der c r) \<and> s\<^sub>4 \<in> L (STAR r))" by fact
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 393
then have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (c # s1) @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (STAR r))"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 394
by (simp add: der_correctness Der_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 395
ultimately
146
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 396
have "((c # s1) @ s2) \<in> STAR r \<rightarrow> Stars (injval r c v1 # vs)" by (rule Posix.intros)
121
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 397
then show "(c # s) \<in> STAR r \<rightarrow> injval (STAR r) c v" using cons by(simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 398
qed
276
+ − 399
next
+ − 400
case (NTIMES r n s v)
+ − 401
have IH: "\<And>s v. s \<in> der c r \<rightarrow> v \<Longrightarrow> (c # s) \<in> r \<rightarrow> injval r c v" by fact
+ − 402
have "s \<in> der c (NTIMES r n) \<rightarrow> v" by fact
220
+ − 403
then consider
276
+ − 404
(cons) v1 vs s1 s2 where
220
+ − 405
"v = Seq v1 (Stars vs)" "s = s1 @ s2"
276
+ − 406
"s1 \<in> der c r \<rightarrow> v1" "s2 \<in> (NTIMES r (n - 1)) \<rightarrow> (Stars vs)" "0 < n"
+ − 407
"\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L (der c r) \<and> s\<^sub>4 \<in> L (NTIMES r (n - 1)))"
+ − 408
apply(auto elim: Posix_elims simp add: der_correctness Der_def intro: Posix.intros split: if_splits)
+ − 409
apply(erule Posix_elims)
+ − 410
apply(simp)
+ − 411
apply(subgoal_tac "\<exists>vss. v2 = Stars vss")
+ − 412
apply(clarify)
+ − 413
apply(drule_tac x="vss" in meta_spec)
+ − 414
apply(drule_tac x="s1" in meta_spec)
+ − 415
apply(drule_tac x="s2" in meta_spec)
+ − 416
apply(simp add: der_correctness Der_def)
+ − 417
apply(erule Posix_elims)
+ − 418
apply(auto)
+ − 419
done
+ − 420
then show "(c # s) \<in> (NTIMES r n) \<rightarrow> injval (NTIMES r n) c v"
220
+ − 421
proof (cases)
+ − 422
case cons
+ − 423
have "s1 \<in> der c r \<rightarrow> v1" by fact
+ − 424
then have "(c # s1) \<in> r \<rightarrow> injval r c v1" using IH by simp
+ − 425
moreover
276
+ − 426
have "s2 \<in> (NTIMES r (n - 1)) \<rightarrow> Stars vs" by fact
220
+ − 427
moreover
+ − 428
have "(c # s1) \<in> r \<rightarrow> injval r c v1" by fact
+ − 429
then have "flat (injval r c v1) = (c # s1)" by (rule Posix1)
+ − 430
then have "flat (injval r c v1) \<noteq> []" by simp
+ − 431
moreover
276
+ − 432
have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L (der c r) \<and> s\<^sub>4 \<in> L (NTIMES r (n - 1)))" by fact
+ − 433
then have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (c # s1) @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (NTIMES r (n - 1)))"
220
+ − 434
by (simp add: der_correctness Der_def)
+ − 435
ultimately
276
+ − 436
have "((c # s1) @ s2) \<in> NTIMES r n \<rightarrow> Stars (injval r c v1 # vs)"
+ − 437
apply (rule_tac Posix.intros)
+ − 438
apply(simp_all)
+ − 439
apply(case_tac n)
+ − 440
apply(simp)
+ − 441
using Posix_elims(1) NTIMES.prems apply auto[1]
+ − 442
apply(simp)
+ − 443
done
221
+ − 444
then show "(c # s) \<in> NTIMES r n \<rightarrow> injval (NTIMES r n) c v" using cons by(simp)
276
+ − 445
qed
+ − 446
next
+ − 447
case (FROMNTIMES r n s v)
223
+ − 448
have IH: "\<And>s v. s \<in> der c r \<rightarrow> v \<Longrightarrow> (c # s) \<in> r \<rightarrow> injval r c v" by fact
+ − 449
have "s \<in> der c (FROMNTIMES r n) \<rightarrow> v" by fact
+ − 450
then consider
276
+ − 451
(cons) v1 vs s1 s2 where
223
+ − 452
"v = Seq v1 (Stars vs)" "s = s1 @ s2"
276
+ − 453
"s1 \<in> der c r \<rightarrow> v1" "s2 \<in> (FROMNTIMES r (n - 1)) \<rightarrow> (Stars vs)" "0 < n"
+ − 454
"\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L (der c r) \<and> s\<^sub>4 \<in> L (FROMNTIMES r (n - 1)))"
277
+ − 455
| (null) v1 vs s1 s2 where
+ − 456
"v = Seq v1 (Stars vs)" "s = s1 @ s2" "s2 \<in> (STAR r) \<rightarrow> (Stars vs)"
+ − 457
"s1 \<in> der c r \<rightarrow> v1" "n = 0"
278
+ − 458
"\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L (der c r) \<and> s\<^sub>4 \<in> L (STAR r))"
276
+ − 459
apply(auto elim: Posix_elims simp add: der_correctness Der_def intro: Posix.intros split: if_splits)
277
+ − 460
prefer 2
276
+ − 461
apply(erule Posix_elims)
+ − 462
apply(simp)
+ − 463
apply(subgoal_tac "\<exists>vss. v2 = Stars vss")
+ − 464
apply(clarify)
+ − 465
apply(drule_tac x="vss" in meta_spec)
+ − 466
apply(drule_tac x="s1" in meta_spec)
+ − 467
apply(drule_tac x="s2" in meta_spec)
+ − 468
apply(simp add: der_correctness Der_def)
277
+ − 469
apply(rotate_tac 5)
276
+ − 470
apply(erule Posix_elims)
+ − 471
apply(auto)[2]
277
+ − 472
apply(erule Posix_elims)
+ − 473
apply(simp)
+ − 474
apply blast
+ − 475
apply(erule Posix_elims)
+ − 476
apply(auto)
+ − 477
apply(auto elim: Posix_elims simp add: der_correctness Der_def intro: Posix.intros split: if_splits)
+ − 478
apply(subgoal_tac "\<exists>vss. v2 = Stars vss")
+ − 479
apply(clarify)
+ − 480
apply simp
+ − 481
apply(rotate_tac 6)
+ − 482
apply(erule Posix_elims)
+ − 483
apply(auto)[2]
+ − 484
done
276
+ − 485
then show "(c # s) \<in> (FROMNTIMES r n) \<rightarrow> injval (FROMNTIMES r n) c v"
223
+ − 486
proof (cases)
+ − 487
case cons
+ − 488
have "s1 \<in> der c r \<rightarrow> v1" by fact
+ − 489
then have "(c # s1) \<in> r \<rightarrow> injval r c v1" using IH by simp
+ − 490
moreover
276
+ − 491
have "s2 \<in> (FROMNTIMES r (n - 1)) \<rightarrow> Stars vs" by fact
223
+ − 492
moreover
276
+ − 493
have "(c # s1) \<in> r \<rightarrow> injval r c v1" by fact
+ − 494
then have "flat (injval r c v1) = (c # s1)" by (rule Posix1)
+ − 495
then have "flat (injval r c v1) \<noteq> []" by simp
+ − 496
moreover
+ − 497
have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L (der c r) \<and> s\<^sub>4 \<in> L (FROMNTIMES r (n - 1)))" by fact
+ − 498
then have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (c # s1) @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (FROMNTIMES r (n - 1)))"
223
+ − 499
by (simp add: der_correctness Der_def)
+ − 500
ultimately
276
+ − 501
have "((c # s1) @ s2) \<in> FROMNTIMES r n \<rightarrow> Stars (injval r c v1 # vs)"
+ − 502
apply (rule_tac Posix.intros)
+ − 503
apply(simp_all)
+ − 504
apply(case_tac n)
+ − 505
apply(simp)
+ − 506
using Posix_elims(1) FROMNTIMES.prems apply auto[1]
+ − 507
using cons(5) apply blast
+ − 508
apply(simp)
+ − 509
done
223
+ − 510
then show "(c # s) \<in> FROMNTIMES r n \<rightarrow> injval (FROMNTIMES r n) c v" using cons by(simp)
276
+ − 511
next
+ − 512
case null
277
+ − 513
have "s1 \<in> der c r \<rightarrow> v1" by fact
+ − 514
then have "(c # s1) \<in> r \<rightarrow> injval r c v1" using IH by simp
+ − 515
moreover
+ − 516
have "s2 \<in> STAR r \<rightarrow> Stars vs" by fact
+ − 517
moreover
+ − 518
have "(c # s1) \<in> r \<rightarrow> injval r c v1" by fact
+ − 519
then have "flat (injval r c v1) = (c # s1)" by (rule Posix1)
276
+ − 520
then have "flat (injval r c v1) \<noteq> []" by simp
277
+ − 521
moreover
+ − 522
moreover
+ − 523
have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L (der c r) \<and> s\<^sub>4 \<in> L (STAR r))" by fact
+ − 524
then have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (c # s1) @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (STAR r))"
+ − 525
by (simp add: der_correctness Der_def)
276
+ − 526
ultimately
277
+ − 527
have "((c # s1) @ s2) \<in> FROMNTIMES r 0 \<rightarrow> Stars (injval r c v1 # vs)"
+ − 528
apply (rule_tac Posix.intros) back
+ − 529
apply(simp_all)
276
+ − 530
done
+ − 531
then show "(c # s) \<in> FROMNTIMES r n \<rightarrow> injval (FROMNTIMES r n) c v" using null
+ − 532
apply(simp)
277
+ − 533
done
276
+ − 534
qed
+ − 535
next
278
+ − 536
case (NMTIMES r n m s v)
+ − 537
have IH: "\<And>s v. s \<in> der c r \<rightarrow> v \<Longrightarrow> (c # s) \<in> r \<rightarrow> injval r c v" by fact
+ − 538
have "s \<in> der c (NMTIMES r n m) \<rightarrow> v" by fact
+ − 539
then consider
+ − 540
(cons) v1 vs s1 s2 where
+ − 541
"v = Seq v1 (Stars vs)" "s = s1 @ s2"
+ − 542
"s1 \<in> der c r \<rightarrow> v1" "s2 \<in> (NMTIMES r (n - 1) (m - 1)) \<rightarrow> (Stars vs)" "0 < n" "n \<le> m"
+ − 543
"\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L (der c r) \<and> s\<^sub>4 \<in> L (NMTIMES r (n - 1) (m - 1)))"
+ − 544
| (null) v1 vs s1 s2 where
+ − 545
"v = Seq v1 (Stars vs)" "s = s1 @ s2" "s2 \<in> (UPNTIMES r (m - 1)) \<rightarrow> (Stars vs)"
+ − 546
"s1 \<in> der c r \<rightarrow> v1" "n = 0" "0 < m"
+ − 547
"\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L (der c r) \<and> s\<^sub>4 \<in> L (UPNTIMES r (m - 1)))"
+ − 548
apply(auto elim: Posix_elims simp add: der_correctness Der_def intro: Posix.intros split: if_splits)
+ − 549
prefer 2
+ − 550
apply(erule Posix_elims)
+ − 551
apply(simp)
+ − 552
apply(subgoal_tac "\<exists>vss. v2 = Stars vss")
+ − 553
apply(clarify)
+ − 554
apply(drule_tac x="vss" in meta_spec)
+ − 555
apply(drule_tac x="s1" in meta_spec)
+ − 556
apply(drule_tac x="s2" in meta_spec)
+ − 557
apply(simp add: der_correctness Der_def)
+ − 558
apply(rotate_tac 5)
+ − 559
apply(erule Posix_elims)
+ − 560
apply(auto)[2]
+ − 561
apply(erule Posix_elims)
+ − 562
apply(simp)
+ − 563
apply blast
+ − 564
+ − 565
apply(erule Posix_elims)
+ − 566
apply(auto)
+ − 567
apply(auto elim: Posix_elims simp add: der_correctness Der_def intro: Posix.intros split: if_splits)
+ − 568
apply(subgoal_tac "\<exists>vss. v2 = Stars vss")
+ − 569
apply(clarify)
+ − 570
apply simp
+ − 571
apply(rotate_tac 6)
+ − 572
apply(erule Posix_elims)
+ − 573
apply(auto)[2]
+ − 574
done
+ − 575
then show "(c # s) \<in> (NMTIMES r n m) \<rightarrow> injval (NMTIMES r n m) c v"
+ − 576
proof (cases)
+ − 577
case cons
+ − 578
have "s1 \<in> der c r \<rightarrow> v1" by fact
+ − 579
then have "(c # s1) \<in> r \<rightarrow> injval r c v1" using IH by simp
+ − 580
moreover
+ − 581
have "s2 \<in> (NMTIMES r (n - 1) (m - 1)) \<rightarrow> Stars vs" by fact
+ − 582
moreover
+ − 583
have "(c # s1) \<in> r \<rightarrow> injval r c v1" by fact
+ − 584
then have "flat (injval r c v1) = (c # s1)" by (rule Posix1)
+ − 585
then have "flat (injval r c v1) \<noteq> []" by simp
+ − 586
moreover
+ − 587
have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L (der c r) \<and> s\<^sub>4 \<in> L (NMTIMES r (n - 1) (m - 1)))" by fact
+ − 588
then have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (c # s1) @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (NMTIMES r (n - 1) (m - 1)))"
+ − 589
by (simp add: der_correctness Der_def)
+ − 590
ultimately
+ − 591
have "((c # s1) @ s2) \<in> NMTIMES r n m \<rightarrow> Stars (injval r c v1 # vs)"
+ − 592
apply (rule_tac Posix.intros)
+ − 593
apply(simp_all)
+ − 594
apply(case_tac n)
+ − 595
apply(simp)
+ − 596
using Posix_elims(1) NMTIMES.prems apply auto[1]
+ − 597
using cons(5) apply blast
+ − 598
apply(simp)
+ − 599
apply(rule cons)
+ − 600
done
+ − 601
then show "(c # s) \<in> NMTIMES r n m \<rightarrow> injval (NMTIMES r n m) c v" using cons by(simp)
+ − 602
next
+ − 603
case null
+ − 604
have "s1 \<in> der c r \<rightarrow> v1" by fact
+ − 605
then have "(c # s1) \<in> r \<rightarrow> injval r c v1" using IH by simp
+ − 606
moreover
+ − 607
have "s2 \<in> UPNTIMES r (m - 1) \<rightarrow> Stars vs" by fact
+ − 608
moreover
+ − 609
have "(c # s1) \<in> r \<rightarrow> injval r c v1" by fact
+ − 610
then have "flat (injval r c v1) = (c # s1)" by (rule Posix1)
+ − 611
then have "flat (injval r c v1) \<noteq> []" by simp
+ − 612
moreover
+ − 613
moreover
+ − 614
have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L (der c r) \<and> s\<^sub>4 \<in> L (UPNTIMES r (m - 1)))" by fact
+ − 615
then have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (c # s1) @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (UPNTIMES r (m - 1)))"
+ − 616
by (simp add: der_correctness Der_def)
+ − 617
ultimately
+ − 618
have "((c # s1) @ s2) \<in> NMTIMES r 0 m \<rightarrow> Stars (injval r c v1 # vs)"
+ − 619
apply (rule_tac Posix.intros) back
+ − 620
apply(simp_all)
+ − 621
apply(rule null)
+ − 622
done
+ − 623
then show "(c # s) \<in> NMTIMES r n m \<rightarrow> injval (NMTIMES r n m) c v" using null
+ − 624
apply(simp)
+ − 625
done
+ − 626
qed
397
+ − 627
next
+ − 628
case (NOT r s v)
+ − 629
then show ?case sorry
121
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 630
qed
106
489dfa0d7ec9
more cleaning and moving unnessary stuff to the end
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 631
276
+ − 632
section {* Lexer Correctness *}
145
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 633
151
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 634
lemma lexer_correct_None:
145
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 635
shows "s \<notin> L r \<longleftrightarrow> lexer r s = None"
120
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 636
apply(induct s arbitrary: r)
143
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 637
apply(simp add: nullable_correctness)
120
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 638
apply(drule_tac x="der a r" in meta_spec)
143
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 639
apply(auto simp add: der_correctness Der_def)
120
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 640
done
106
489dfa0d7ec9
more cleaning and moving unnessary stuff to the end
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 641
151
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 642
lemma lexer_correct_Some:
185
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 643
shows "s \<in> L r \<longleftrightarrow> (\<exists>v. lexer r s = Some(v) \<and> s \<in> r \<rightarrow> v)"
124
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 644
apply(induct s arbitrary: r)
151
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 645
apply(auto simp add: Posix_mkeps nullable_correctness)[1]
124
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 646
apply(drule_tac x="der a r" in meta_spec)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 647
apply(simp add: der_correctness Der_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 648
apply(rule iffI)
172
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 649
apply(auto intro: Posix_injval simp add: Posix1(1))
151
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 650
done
149
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 651
186
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 652
lemma lexer_correctness:
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 653
shows "(lexer r s = Some v) \<longleftrightarrow> s \<in> r \<rightarrow> v"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 654
and "(lexer r s = None) \<longleftrightarrow> \<not>(\<exists>v. s \<in> r \<rightarrow> v)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 655
using Posix1(1) Posix_determ lexer_correct_None lexer_correct_Some apply fastforce
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 656
using Posix1(1) lexer_correct_None lexer_correct_Some by blast
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 657
95
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 658
end