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