365
+ − 1
+ − 2
theory Lexer
+ − 3
imports Spec
+ − 4
begin
+ − 5
+ − 6
section {* The Lexer Functions by Sulzmann and Lu (without simplification) *}
+ − 7
+ − 8
fun
+ − 9
mkeps :: "rexp \<Rightarrow> val"
+ − 10
where
+ − 11
"mkeps(ONE) = Void"
+ − 12
| "mkeps(SEQ r1 r2) = Seq (mkeps r1) (mkeps r2)"
+ − 13
| "mkeps(ALT r1 r2) = (if nullable(r1) then Left (mkeps r1) else Right (mkeps r2))"
+ − 14
| "mkeps(STAR r) = Stars []"
+ − 15
+ − 16
fun injval :: "rexp \<Rightarrow> char \<Rightarrow> val \<Rightarrow> val"
+ − 17
where
+ − 18
"injval (CH d) c Void = Char d"
+ − 19
| "injval (ALT r1 r2) c (Left v1) = Left(injval r1 c v1)"
+ − 20
| "injval (ALT r1 r2) c (Right v2) = Right(injval r2 c v2)"
+ − 21
| "injval (SEQ r1 r2) c (Seq v1 v2) = Seq (injval r1 c v1) v2"
+ − 22
| "injval (SEQ r1 r2) c (Left (Seq v1 v2)) = Seq (injval r1 c v1) v2"
+ − 23
| "injval (SEQ r1 r2) c (Right v2) = Seq (mkeps r1) (injval r2 c v2)"
+ − 24
| "injval (STAR r) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)"
+ − 25
+ − 26
fun
+ − 27
lexer :: "rexp \<Rightarrow> string \<Rightarrow> val option"
+ − 28
where
+ − 29
"lexer r [] = (if nullable r then Some(mkeps r) else None)"
+ − 30
| "lexer r (c#s) = (case (lexer (der c r) s) of
+ − 31
None \<Rightarrow> None
+ − 32
| Some(v) \<Rightarrow> Some(injval r c v))"
+ − 33
+ − 34
+ − 35
+ − 36
section {* Mkeps, Injval Properties *}
+ − 37
+ − 38
lemma mkeps_nullable:
+ − 39
assumes "nullable(r)"
+ − 40
shows "\<Turnstile> mkeps r : r"
+ − 41
using assms
+ − 42
by (induct rule: nullable.induct)
+ − 43
(auto intro: Prf.intros)
+ − 44
+ − 45
lemma mkeps_flat:
+ − 46
assumes "nullable(r)"
+ − 47
shows "flat (mkeps r) = []"
+ − 48
using assms
+ − 49
by (induct rule: nullable.induct) (auto)
+ − 50
+ − 51
lemma Prf_injval_flat:
+ − 52
assumes "\<Turnstile> v : der c r"
+ − 53
shows "flat (injval r c v) = c # (flat v)"
+ − 54
using assms
+ − 55
apply(induct c r arbitrary: v rule: der.induct)
+ − 56
apply(auto elim!: Prf_elims intro: mkeps_flat split: if_splits)
+ − 57
done
+ − 58
+ − 59
lemma Prf_injval:
+ − 60
assumes "\<Turnstile> v : der c r"
+ − 61
shows "\<Turnstile> (injval r c v) : r"
+ − 62
using assms
+ − 63
apply(induct r arbitrary: c v rule: rexp.induct)
+ − 64
apply(auto intro!: Prf.intros mkeps_nullable elim!: Prf_elims split: if_splits)
+ − 65
apply(simp add: Prf_injval_flat)
+ − 66
done
+ − 67
+ − 68
+ − 69
+ − 70
text {*
+ − 71
Mkeps and injval produce, or preserve, Posix values.
+ − 72
*}
+ − 73
+ − 74
lemma Posix_mkeps:
+ − 75
assumes "nullable r"
+ − 76
shows "[] \<in> r \<rightarrow> mkeps r"
+ − 77
using assms
+ − 78
apply(induct r rule: nullable.induct)
+ − 79
apply(auto intro: Posix.intros simp add: nullable_correctness Sequ_def)
+ − 80
apply(subst append.simps(1)[symmetric])
+ − 81
apply(rule Posix.intros)
+ − 82
apply(auto)
+ − 83
done
+ − 84
+ − 85
lemma Posix_injval:
+ − 86
assumes "s \<in> (der c r) \<rightarrow> v"
+ − 87
shows "(c # s) \<in> r \<rightarrow> (injval r c v)"
+ − 88
using assms
+ − 89
proof(induct r arbitrary: s v rule: rexp.induct)
+ − 90
case ZERO
+ − 91
have "s \<in> der c ZERO \<rightarrow> v" by fact
+ − 92
then have "s \<in> ZERO \<rightarrow> v" by simp
+ − 93
then have "False" by cases
+ − 94
then show "(c # s) \<in> ZERO \<rightarrow> (injval ZERO c v)" by simp
+ − 95
next
+ − 96
case ONE
+ − 97
have "s \<in> der c ONE \<rightarrow> v" by fact
+ − 98
then have "s \<in> ZERO \<rightarrow> v" by simp
+ − 99
then have "False" by cases
+ − 100
then show "(c # s) \<in> ONE \<rightarrow> (injval ONE c v)" by simp
+ − 101
next
+ − 102
case (CH d)
+ − 103
consider (eq) "c = d" | (ineq) "c \<noteq> d" by blast
+ − 104
then show "(c # s) \<in> (CH d) \<rightarrow> (injval (CH d) c v)"
+ − 105
proof (cases)
+ − 106
case eq
+ − 107
have "s \<in> der c (CH d) \<rightarrow> v" by fact
+ − 108
then have "s \<in> ONE \<rightarrow> v" using eq by simp
+ − 109
then have eqs: "s = [] \<and> v = Void" by cases simp
+ − 110
show "(c # s) \<in> CH d \<rightarrow> injval (CH d) c v" using eq eqs
+ − 111
by (auto intro: Posix.intros)
+ − 112
next
+ − 113
case ineq
+ − 114
have "s \<in> der c (CH d) \<rightarrow> v" by fact
+ − 115
then have "s \<in> ZERO \<rightarrow> v" using ineq by simp
+ − 116
then have "False" by cases
+ − 117
then show "(c # s) \<in> CH d \<rightarrow> injval (CH d) c v" by simp
+ − 118
qed
+ − 119
next
+ − 120
case (ALT r1 r2)
+ − 121
have IH1: "\<And>s v. s \<in> der c r1 \<rightarrow> v \<Longrightarrow> (c # s) \<in> r1 \<rightarrow> injval r1 c v" by fact
+ − 122
have IH2: "\<And>s v. s \<in> der c r2 \<rightarrow> v \<Longrightarrow> (c # s) \<in> r2 \<rightarrow> injval r2 c v" by fact
+ − 123
have "s \<in> der c (ALT r1 r2) \<rightarrow> v" by fact
+ − 124
then have "s \<in> ALT (der c r1) (der c r2) \<rightarrow> v" by simp
+ − 125
then consider (left) v' where "v = Left v'" "s \<in> der c r1 \<rightarrow> v'"
+ − 126
| (right) v' where "v = Right v'" "s \<notin> L (der c r1)" "s \<in> der c r2 \<rightarrow> v'"
+ − 127
by cases auto
+ − 128
then show "(c # s) \<in> ALT r1 r2 \<rightarrow> injval (ALT r1 r2) c v"
+ − 129
proof (cases)
+ − 130
case left
+ − 131
have "s \<in> der c r1 \<rightarrow> v'" by fact
+ − 132
then have "(c # s) \<in> r1 \<rightarrow> injval r1 c v'" using IH1 by simp
+ − 133
then have "(c # s) \<in> ALT r1 r2 \<rightarrow> injval (ALT r1 r2) c (Left v')" by (auto intro: Posix.intros)
+ − 134
then show "(c # s) \<in> ALT r1 r2 \<rightarrow> injval (ALT r1 r2) c v" using left by simp
+ − 135
next
+ − 136
case right
+ − 137
have "s \<notin> L (der c r1)" by fact
+ − 138
then have "c # s \<notin> L r1" by (simp add: der_correctness Der_def)
+ − 139
moreover
+ − 140
have "s \<in> der c r2 \<rightarrow> v'" by fact
+ − 141
then have "(c # s) \<in> r2 \<rightarrow> injval r2 c v'" using IH2 by simp
+ − 142
ultimately have "(c # s) \<in> ALT r1 r2 \<rightarrow> injval (ALT r1 r2) c (Right v')"
+ − 143
by (auto intro: Posix.intros)
+ − 144
then show "(c # s) \<in> ALT r1 r2 \<rightarrow> injval (ALT r1 r2) c v" using right by simp
+ − 145
qed
+ − 146
next
+ − 147
case (SEQ r1 r2)
+ − 148
have IH1: "\<And>s v. s \<in> der c r1 \<rightarrow> v \<Longrightarrow> (c # s) \<in> r1 \<rightarrow> injval r1 c v" by fact
+ − 149
have IH2: "\<And>s v. s \<in> der c r2 \<rightarrow> v \<Longrightarrow> (c # s) \<in> r2 \<rightarrow> injval r2 c v" by fact
+ − 150
have "s \<in> der c (SEQ r1 r2) \<rightarrow> v" by fact
+ − 151
then consider
+ − 152
(left_nullable) v1 v2 s1 s2 where
+ − 153
"v = Left (Seq v1 v2)" "s = s1 @ s2"
+ − 154
"s1 \<in> der c r1 \<rightarrow> v1" "s2 \<in> r2 \<rightarrow> v2" "nullable r1"
+ − 155
"\<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)"
+ − 156
| (right_nullable) v1 s1 s2 where
+ − 157
"v = Right v1" "s = s1 @ s2"
+ − 158
"s \<in> der c r2 \<rightarrow> v1" "nullable r1" "s1 @ s2 \<notin> L (SEQ (der c r1) r2)"
+ − 159
| (not_nullable) v1 v2 s1 s2 where
+ − 160
"v = Seq v1 v2" "s = s1 @ s2"
+ − 161
"s1 \<in> der c r1 \<rightarrow> v1" "s2 \<in> r2 \<rightarrow> v2" "\<not>nullable r1"
+ − 162
"\<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)"
+ − 163
by (force split: if_splits elim!: Posix_elims simp add: Sequ_def der_correctness Der_def)
+ − 164
then show "(c # s) \<in> SEQ r1 r2 \<rightarrow> injval (SEQ r1 r2) c v"
+ − 165
proof (cases)
+ − 166
case left_nullable
+ − 167
have "s1 \<in> der c r1 \<rightarrow> v1" by fact
+ − 168
then have "(c # s1) \<in> r1 \<rightarrow> injval r1 c v1" using IH1 by simp
+ − 169
moreover
+ − 170
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
+ − 171
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)
+ − 172
ultimately have "((c # s1) @ s2) \<in> SEQ r1 r2 \<rightarrow> Seq (injval r1 c v1) v2" using left_nullable by (rule_tac Posix.intros)
+ − 173
then show "(c # s) \<in> SEQ r1 r2 \<rightarrow> injval (SEQ r1 r2) c v" using left_nullable by simp
+ − 174
next
+ − 175
case right_nullable
+ − 176
have "nullable r1" by fact
+ − 177
then have "[] \<in> r1 \<rightarrow> (mkeps r1)" by (rule Posix_mkeps)
+ − 178
moreover
+ − 179
have "s \<in> der c r2 \<rightarrow> v1" by fact
+ − 180
then have "(c # s) \<in> r2 \<rightarrow> (injval r2 c v1)" using IH2 by simp
+ − 181
moreover
+ − 182
have "s1 @ s2 \<notin> L (SEQ (der c r1) r2)" by fact
+ − 183
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
+ − 184
by(auto simp add: der_correctness Der_def append_eq_Cons_conv Sequ_def)
+ − 185
ultimately have "([] @ (c # s)) \<in> SEQ r1 r2 \<rightarrow> Seq (mkeps r1) (injval r2 c v1)"
+ − 186
by(rule Posix.intros)
+ − 187
then show "(c # s) \<in> SEQ r1 r2 \<rightarrow> injval (SEQ r1 r2) c v" using right_nullable by simp
+ − 188
next
+ − 189
case not_nullable
+ − 190
have "s1 \<in> der c r1 \<rightarrow> v1" by fact
+ − 191
then have "(c # s1) \<in> r1 \<rightarrow> injval r1 c v1" using IH1 by simp
+ − 192
moreover
+ − 193
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
+ − 194
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)
+ − 195
ultimately have "((c # s1) @ s2) \<in> SEQ r1 r2 \<rightarrow> Seq (injval r1 c v1) v2" using not_nullable
+ − 196
by (rule_tac Posix.intros) (simp_all)
+ − 197
then show "(c # s) \<in> SEQ r1 r2 \<rightarrow> injval (SEQ r1 r2) c v" using not_nullable by simp
+ − 198
qed
+ − 199
next
+ − 200
case (STAR r)
+ − 201
have IH: "\<And>s v. s \<in> der c r \<rightarrow> v \<Longrightarrow> (c # s) \<in> r \<rightarrow> injval r c v" by fact
+ − 202
have "s \<in> der c (STAR r) \<rightarrow> v" by fact
+ − 203
then consider
+ − 204
(cons) v1 vs s1 s2 where
+ − 205
"v = Seq v1 (Stars vs)" "s = s1 @ s2"
+ − 206
"s1 \<in> der c r \<rightarrow> v1" "s2 \<in> (STAR r) \<rightarrow> (Stars vs)"
+ − 207
"\<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))"
+ − 208
apply(auto elim!: Posix_elims(1-5) simp add: der_correctness Der_def intro: Posix.intros)
+ − 209
apply(rotate_tac 3)
+ − 210
apply(erule_tac Posix_elims(6))
+ − 211
apply (simp add: Posix.intros(6))
+ − 212
using Posix.intros(7) by blast
+ − 213
then show "(c # s) \<in> STAR r \<rightarrow> injval (STAR r) c v"
+ − 214
proof (cases)
+ − 215
case cons
+ − 216
have "s1 \<in> der c r \<rightarrow> v1" by fact
+ − 217
then have "(c # s1) \<in> r \<rightarrow> injval r c v1" using IH by simp
+ − 218
moreover
+ − 219
have "s2 \<in> STAR r \<rightarrow> Stars vs" by fact
+ − 220
moreover
+ − 221
have "(c # s1) \<in> r \<rightarrow> injval r c v1" by fact
+ − 222
then have "flat (injval r c v1) = (c # s1)" by (rule Posix1)
+ − 223
then have "flat (injval r c v1) \<noteq> []" by simp
+ − 224
moreover
+ − 225
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
+ − 226
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))"
+ − 227
by (simp add: der_correctness Der_def)
+ − 228
ultimately
+ − 229
have "((c # s1) @ s2) \<in> STAR r \<rightarrow> Stars (injval r c v1 # vs)" by (rule Posix.intros)
+ − 230
then show "(c # s) \<in> STAR r \<rightarrow> injval (STAR r) c v" using cons by(simp)
+ − 231
qed
+ − 232
qed
+ − 233
+ − 234
+ − 235
section {* Lexer Correctness *}
+ − 236
+ − 237
+ − 238
lemma lexer_correct_None:
+ − 239
shows "s \<notin> L r \<longleftrightarrow> lexer r s = None"
+ − 240
apply(induct s arbitrary: r)
+ − 241
apply(simp)
+ − 242
apply(simp add: nullable_correctness)
+ − 243
apply(simp)
+ − 244
apply(drule_tac x="der a r" in meta_spec)
+ − 245
apply(auto)
+ − 246
apply(auto simp add: der_correctness Der_def)
+ − 247
done
+ − 248
+ − 249
lemma lexer_correct_Some:
+ − 250
shows "s \<in> L r \<longleftrightarrow> (\<exists>v. lexer r s = Some(v) \<and> s \<in> r \<rightarrow> v)"
+ − 251
apply(induct s arbitrary : r)
+ − 252
apply(simp only: lexer.simps)
+ − 253
apply(simp)
+ − 254
apply(simp add: nullable_correctness Posix_mkeps)
+ − 255
apply(drule_tac x="der a r" in meta_spec)
+ − 256
apply(simp (no_asm_use) add: der_correctness Der_def del: lexer.simps)
+ − 257
apply(simp del: lexer.simps)
+ − 258
apply(simp only: lexer.simps)
+ − 259
apply(case_tac "lexer (der a r) s = None")
+ − 260
apply(auto)[1]
+ − 261
apply(simp)
+ − 262
apply(erule exE)
+ − 263
apply(simp)
+ − 264
apply(rule iffI)
+ − 265
apply(simp add: Posix_injval)
+ − 266
apply(simp add: Posix1(1))
+ − 267
done
+ − 268
+ − 269
lemma lexer_correctness:
+ − 270
shows "(lexer r s = Some v) \<longleftrightarrow> s \<in> r \<rightarrow> v"
+ − 271
and "(lexer r s = None) \<longleftrightarrow> \<not>(\<exists>v. s \<in> r \<rightarrow> v)"
+ − 272
using Posix1(1) Posix_determ lexer_correct_None lexer_correct_Some apply fastforce
+ − 273
using Posix1(1) lexer_correct_None lexer_correct_Some by blast
+ − 274
+ − 275
+ − 276
subsection {* A slight reformulation of the lexer algorithm using stacked functions*}
+ − 277
+ − 278
fun flex :: "rexp \<Rightarrow> (val \<Rightarrow> val) => string \<Rightarrow> (val \<Rightarrow> val)"
+ − 279
where
+ − 280
"flex r f [] = f"
+ − 281
| "flex r f (c#s) = flex (der c r) (\<lambda>v. f (injval r c v)) s"
+ − 282
+ − 283
lemma flex_fun_apply:
+ − 284
shows "g (flex r f s v) = flex r (g o f) s v"
+ − 285
apply(induct s arbitrary: g f r v)
+ − 286
apply(simp_all add: comp_def)
+ − 287
by meson
+ − 288
+ − 289
lemma flex_fun_apply2:
+ − 290
shows "g (flex r id s v) = flex r g s v"
+ − 291
by (simp add: flex_fun_apply)
+ − 292
+ − 293
+ − 294
lemma flex_append:
+ − 295
shows "flex r f (s1 @ s2) = flex (ders s1 r) (flex r f s1) s2"
+ − 296
apply(induct s1 arbitrary: s2 r f)
+ − 297
apply(simp_all)
+ − 298
done
+ − 299
+ − 300
lemma lexer_flex:
+ − 301
shows "lexer r s = (if nullable (ders s r)
+ − 302
then Some(flex r id s (mkeps (ders s r))) else None)"
+ − 303
apply(induct s arbitrary: r)
+ − 304
apply(simp_all add: flex_fun_apply)
+ − 305
done
+ − 306
+ − 307
lemma Posix_flex:
+ − 308
assumes "s2 \<in> (ders s1 r) \<rightarrow> v"
+ − 309
shows "(s1 @ s2) \<in> r \<rightarrow> flex r id s1 v"
+ − 310
using assms
+ − 311
apply(induct s1 arbitrary: r v s2)
+ − 312
apply(simp)
+ − 313
apply(simp)
+ − 314
apply(drule_tac x="der a r" in meta_spec)
+ − 315
apply(drule_tac x="v" in meta_spec)
+ − 316
apply(drule_tac x="s2" in meta_spec)
+ − 317
apply(simp)
+ − 318
using Posix_injval
+ − 319
apply(drule_tac Posix_injval)
+ − 320
apply(subst (asm) (5) flex_fun_apply)
+ − 321
apply(simp)
+ − 322
done
+ − 323
+ − 324
lemma injval_inj:
+ − 325
assumes "\<Turnstile> a : (der c r)" "\<Turnstile> v : (der c r)" "injval r c a = injval r c v"
+ − 326
shows "a = v"
+ − 327
using assms
+ − 328
apply(induct r arbitrary: a c v)
+ − 329
apply(auto)
+ − 330
using Prf_elims(1) apply blast
+ − 331
using Prf_elims(1) apply blast
+ − 332
apply(case_tac "c = x")
+ − 333
apply(auto)
+ − 334
using Prf_elims(4) apply auto[1]
+ − 335
using Prf_elims(1) apply blast
+ − 336
prefer 2
+ − 337
apply (smt Prf_elims(3) injval.simps(2) injval.simps(3) val.distinct(25) val.inject(3) val.inject(4))
+ − 338
apply(case_tac "nullable r1")
+ − 339
apply(auto)
+ − 340
apply(erule Prf_elims)
+ − 341
apply(erule Prf_elims)
+ − 342
apply(erule Prf_elims)
+ − 343
apply(erule Prf_elims)
+ − 344
apply(auto)
+ − 345
apply (metis Prf_injval_flat list.distinct(1) mkeps_flat)
+ − 346
apply(erule Prf_elims)
+ − 347
apply(erule Prf_elims)
+ − 348
apply(auto)
+ − 349
using Prf_injval_flat mkeps_flat apply fastforce
+ − 350
apply(erule Prf_elims)
+ − 351
apply(erule Prf_elims)
+ − 352
apply(auto)
+ − 353
apply(erule Prf_elims)
+ − 354
apply(erule Prf_elims)
+ − 355
apply(auto)
+ − 356
apply (smt Prf_elims(6) injval.simps(7) list.inject val.inject(5))
+ − 357
by (smt Prf_elims(6) injval.simps(7) list.inject val.inject(5))
+ − 358
+ − 359
+ − 360
+ − 361
lemma uu:
+ − 362
assumes "(c # s) \<in> r \<rightarrow> injval r c v" "\<Turnstile> v : (der c r)"
+ − 363
shows "s \<in> der c r \<rightarrow> v"
+ − 364
using assms
+ − 365
apply -
+ − 366
apply(subgoal_tac "lexer r (c # s) = Some (injval r c v)")
+ − 367
prefer 2
+ − 368
using lexer_correctness(1) apply blast
+ − 369
apply(simp add: )
+ − 370
apply(case_tac "lexer (der c r) s")
+ − 371
apply(simp)
+ − 372
apply(simp)
+ − 373
apply(case_tac "s \<in> der c r \<rightarrow> a")
+ − 374
prefer 2
+ − 375
apply (simp add: lexer_correctness(1))
+ − 376
apply(subgoal_tac "\<Turnstile> a : (der c r)")
+ − 377
prefer 2
+ − 378
using Posix_Prf apply blast
+ − 379
using injval_inj by blast
+ − 380
+ − 381
+ − 382
lemma Posix_flex2:
+ − 383
assumes "(s1 @ s2) \<in> r \<rightarrow> flex r id s1 v" "\<Turnstile> v : ders s1 r"
+ − 384
shows "s2 \<in> (ders s1 r) \<rightarrow> v"
+ − 385
using assms
+ − 386
apply(induct s1 arbitrary: r v s2 rule: rev_induct)
+ − 387
apply(simp)
+ − 388
apply(simp)
+ − 389
apply(drule_tac x="r" in meta_spec)
+ − 390
apply(drule_tac x="injval (ders xs r) x v" in meta_spec)
+ − 391
apply(drule_tac x="x#s2" in meta_spec)
+ − 392
apply(simp add: flex_append ders_append)
+ − 393
using Prf_injval uu by blast
+ − 394
+ − 395
lemma Posix_flex3:
+ − 396
assumes "s1 \<in> r \<rightarrow> flex r id s1 v" "\<Turnstile> v : ders s1 r"
+ − 397
shows "[] \<in> (ders s1 r) \<rightarrow> v"
+ − 398
using assms
+ − 399
by (simp add: Posix_flex2)
+ − 400
+ − 401
lemma flex_injval:
+ − 402
shows "flex (der a r) (injval r a) s v = injval r a (flex (der a r) id s v)"
+ − 403
by (simp add: flex_fun_apply)
+ − 404
+ − 405
lemma Prf_flex:
+ − 406
assumes "\<Turnstile> v : ders s r"
+ − 407
shows "\<Turnstile> flex r id s v : r"
+ − 408
using assms
+ − 409
apply(induct s arbitrary: v r)
+ − 410
apply(simp)
+ − 411
apply(simp)
+ − 412
by (simp add: Prf_injval flex_injval)
+ − 413
+ − 414
+ − 415
end