365
+ − 1
+ − 2
theory ReTest
+ − 3
imports "Main"
+ − 4
begin
+ − 5
+ − 6
+ − 7
section {* Sequential Composition of Sets *}
+ − 8
+ − 9
definition
+ − 10
Sequ :: "string set \<Rightarrow> string set \<Rightarrow> string set" ("_ ;; _" [100,100] 100)
+ − 11
where
+ − 12
"A ;; B = {s1 @ s2 | s1 s2. s1 \<in> A \<and> s2 \<in> B}"
+ − 13
+ − 14
fun spow where
+ − 15
"spow s 0 = []"
+ − 16
| "spow s (Suc n) = s @ spow s n"
+ − 17
+ − 18
text {* Two Simple Properties about Sequential Composition *}
+ − 19
+ − 20
lemma seq_empty [simp]:
+ − 21
shows "A ;; {[]} = A"
+ − 22
and "{[]} ;; A = A"
+ − 23
by (simp_all add: Sequ_def)
+ − 24
+ − 25
lemma seq_null [simp]:
+ − 26
shows "A ;; {} = {}"
+ − 27
and "{} ;; A = {}"
+ − 28
by (simp_all add: Sequ_def)
+ − 29
+ − 30
definition
+ − 31
Der :: "char \<Rightarrow> string set \<Rightarrow> string set"
+ − 32
where
+ − 33
"Der c A \<equiv> {s. [c] @ s \<in> A}"
+ − 34
+ − 35
definition
+ − 36
Ders :: "string \<Rightarrow> string set \<Rightarrow> string set"
+ − 37
where
+ − 38
"Ders s A \<equiv> {s' | s'. s @ s' \<in> A}"
+ − 39
+ − 40
lemma Der_null [simp]:
+ − 41
shows "Der c {} = {}"
+ − 42
unfolding Der_def
+ − 43
by auto
+ − 44
+ − 45
lemma Der_empty [simp]:
+ − 46
shows "Der c {[]} = {}"
+ − 47
unfolding Der_def
+ − 48
by auto
+ − 49
+ − 50
lemma Der_char [simp]:
+ − 51
shows "Der c {[d]} = (if c = d then {[]} else {})"
+ − 52
unfolding Der_def
+ − 53
by auto
+ − 54
+ − 55
lemma Der_union [simp]:
+ − 56
shows "Der c (A \<union> B) = Der c A \<union> Der c B"
+ − 57
unfolding Der_def
+ − 58
by auto
+ − 59
+ − 60
lemma Der_seq [simp]:
+ − 61
shows "Der c (A ;; B) = (Der c A) ;; B \<union> (if [] \<in> A then Der c B else {})"
+ − 62
unfolding Der_def Sequ_def
+ − 63
apply (auto simp add: Cons_eq_append_conv)
+ − 64
done
+ − 65
+ − 66
lemma seq_image:
+ − 67
assumes "\<forall>s1 s2. f (s1 @ s2) = (f s1) @ (f s2)"
+ − 68
shows "f ` (A ;; B) = (f ` A) ;; (f ` B)"
+ − 69
apply(auto simp add: Sequ_def image_def)
+ − 70
apply(rule_tac x="f s1" in exI)
+ − 71
apply(rule_tac x="f s2" in exI)
+ − 72
using assms
+ − 73
apply(auto)
+ − 74
apply(rule_tac x="xa @ xb" in exI)
+ − 75
using assms
+ − 76
apply(auto)
+ − 77
done
+ − 78
+ − 79
section {* Kleene Star for Sets *}
+ − 80
+ − 81
inductive_set
+ − 82
Star :: "string set \<Rightarrow> string set" ("_\<star>" [101] 102)
+ − 83
for A :: "string set"
+ − 84
where
+ − 85
start[intro]: "[] \<in> A\<star>"
+ − 86
| step[intro]: "\<lbrakk>s1 \<in> A; s2 \<in> A\<star>\<rbrakk> \<Longrightarrow> s1 @ s2 \<in> A\<star>"
+ − 87
+ − 88
lemma star_cases:
+ − 89
shows "A\<star> = {[]} \<union> A ;; A\<star>"
+ − 90
unfolding Sequ_def
+ − 91
by (auto) (metis Star.simps)
+ − 92
+ − 93
+ − 94
fun
+ − 95
pow :: "string set \<Rightarrow> nat \<Rightarrow> string set" ("_ \<up> _" [100,100] 100)
+ − 96
where
+ − 97
"A \<up> 0 = {[]}"
+ − 98
| "A \<up> (Suc n) = A ;; (A \<up> n)"
+ − 99
+ − 100
lemma star1:
+ − 101
shows "s \<in> A\<star> \<Longrightarrow> \<exists>n. s \<in> A \<up> n"
+ − 102
apply(induct rule: Star.induct)
+ − 103
apply (metis pow.simps(1) insertI1)
+ − 104
apply(auto)
+ − 105
apply(rule_tac x="Suc n" in exI)
+ − 106
apply(auto simp add: Sequ_def)
+ − 107
done
+ − 108
+ − 109
lemma star2:
+ − 110
shows "s \<in> A \<up> n \<Longrightarrow> s \<in> A\<star>"
+ − 111
apply(induct n arbitrary: s)
+ − 112
apply (metis pow.simps(1) Star.simps empty_iff insertE)
+ − 113
apply(auto simp add: Sequ_def)
+ − 114
done
+ − 115
+ − 116
lemma star3:
+ − 117
shows "A\<star> = (\<Union>i. A \<up> i)"
+ − 118
using star1 star2
+ − 119
apply(auto)
+ − 120
done
+ − 121
+ − 122
lemma star4:
+ − 123
shows "s \<in> A \<up> n \<Longrightarrow> \<exists>ss. s = concat ss \<and> (\<forall>s' \<in> set ss. s' \<in> A)"
+ − 124
apply(induct n arbitrary: s)
+ − 125
apply(auto simp add: Sequ_def)
+ − 126
apply(rule_tac x="[]" in exI)
+ − 127
apply(auto)
+ − 128
apply(drule_tac x="s2" in meta_spec)
+ − 129
apply(auto)
+ − 130
by (metis concat.simps(2) insertE set_simps(2))
+ − 131
+ − 132
lemma star5:
+ − 133
assumes "f [] = []"
+ − 134
assumes "\<forall>s1 s2. f (s1 @ s2) = (f s1) @ (f s2)"
+ − 135
shows "(f ` A) \<up> n = f ` (A \<up> n)"
+ − 136
apply(induct n)
+ − 137
apply(simp add: assms)
+ − 138
apply(simp)
+ − 139
apply(subst seq_image[OF assms(2)])
+ − 140
apply(simp)
+ − 141
done
+ − 142
+ − 143
lemma star6:
+ − 144
assumes "f [] = []"
+ − 145
assumes "\<forall>s1 s2. f (s1 @ s2) = (f s1) @ (f s2)"
+ − 146
shows "(f ` A)\<star> = f ` (A\<star>)"
+ − 147
apply(simp add: star3)
+ − 148
apply(simp add: image_UN)
+ − 149
apply(subst star5[OF assms])
+ − 150
apply(simp)
+ − 151
done
+ − 152
+ − 153
lemma star_decomp:
+ − 154
assumes a: "c # x \<in> A\<star>"
+ − 155
shows "\<exists>a b. x = a @ b \<and> c # a \<in> A \<and> b \<in> A\<star>"
+ − 156
using a
+ − 157
by (induct x\<equiv>"c # x" rule: Star.induct)
+ − 158
(auto simp add: append_eq_Cons_conv)
+ − 159
+ − 160
lemma Der_star [simp]:
+ − 161
shows "Der c (A\<star>) = (Der c A) ;; A\<star>"
+ − 162
proof -
+ − 163
have "Der c (A\<star>) = Der c ({[]} \<union> A ;; A\<star>)"
+ − 164
+ − 165
by (simp only: star_cases[symmetric])
+ − 166
also have "... = Der c (A ;; A\<star>)"
+ − 167
by (simp only: Der_union Der_empty) (simp)
+ − 168
also have "... = (Der c A) ;; A\<star> \<union> (if [] \<in> A then Der c (A\<star>) else {})"
+ − 169
by simp
+ − 170
also have "... = (Der c A) ;; A\<star>"
+ − 171
unfolding Sequ_def Der_def
+ − 172
by (auto dest: star_decomp)
+ − 173
finally show "Der c (A\<star>) = (Der c A) ;; A\<star>" .
+ − 174
qed
+ − 175
+ − 176
+ − 177
+ − 178
section {* Regular Expressions *}
+ − 179
+ − 180
datatype rexp =
+ − 181
NULL
+ − 182
| EMPTY
+ − 183
| CHAR char
+ − 184
| SEQ rexp rexp
+ − 185
| ALT rexp rexp
+ − 186
| STAR rexp
+ − 187
+ − 188
section {* Semantics of Regular Expressions *}
+ − 189
+ − 190
fun
+ − 191
L :: "rexp \<Rightarrow> string set"
+ − 192
where
+ − 193
"L (NULL) = {}"
+ − 194
| "L (EMPTY) = {[]}"
+ − 195
| "L (CHAR c) = {[c]}"
+ − 196
| "L (SEQ r1 r2) = (L r1) ;; (L r2)"
+ − 197
| "L (ALT r1 r2) = (L r1) \<union> (L r2)"
+ − 198
| "L (STAR r) = (L r)\<star>"
+ − 199
+ − 200
fun
+ − 201
nullable :: "rexp \<Rightarrow> bool"
+ − 202
where
+ − 203
"nullable (NULL) = False"
+ − 204
| "nullable (EMPTY) = True"
+ − 205
| "nullable (CHAR c) = False"
+ − 206
| "nullable (ALT r1 r2) = (nullable r1 \<or> nullable r2)"
+ − 207
| "nullable (SEQ r1 r2) = (nullable r1 \<and> nullable r2)"
+ − 208
| "nullable (STAR r) = True"
+ − 209
+ − 210
lemma nullable_correctness:
+ − 211
shows "nullable r \<longleftrightarrow> [] \<in> (L r)"
+ − 212
apply (induct r)
+ − 213
apply(auto simp add: Sequ_def)
+ − 214
done
+ − 215
+ − 216
+ − 217
+ − 218
section {* Values *}
+ − 219
+ − 220
datatype val =
+ − 221
Void
+ − 222
| Char char
+ − 223
| Seq val val
+ − 224
| Right val
+ − 225
| Left val
+ − 226
| Stars "val list"
+ − 227
+ − 228
section {* The string behind a value *}
+ − 229
+ − 230
fun
+ − 231
flat :: "val \<Rightarrow> string"
+ − 232
where
+ − 233
"flat (Void) = []"
+ − 234
| "flat (Char c) = [c]"
+ − 235
| "flat (Left v) = flat v"
+ − 236
| "flat (Right v) = flat v"
+ − 237
| "flat (Seq v1 v2) = (flat v1) @ (flat v2)"
+ − 238
| "flat (Stars []) = []"
+ − 239
| "flat (Stars (v#vs)) = (flat v) @ (flat (Stars vs))"
+ − 240
+ − 241
lemma [simp]:
+ − 242
"flat (Stars vs) = concat (map flat vs)"
+ − 243
apply(induct vs)
+ − 244
apply(auto)
+ − 245
done
+ − 246
+ − 247
section {* Relation between values and regular expressions *}
+ − 248
+ − 249
inductive
+ − 250
NPrf :: "val \<Rightarrow> rexp \<Rightarrow> bool" ("\<Turnstile> _ : _" [100, 100] 100)
+ − 251
where
+ − 252
"\<lbrakk>\<Turnstile> v1 : r1; \<Turnstile> v2 : r2\<rbrakk> \<Longrightarrow> \<Turnstile> Seq v1 v2 : SEQ r1 r2"
+ − 253
| "\<Turnstile> v1 : r1 \<Longrightarrow> \<Turnstile> Left v1 : ALT r1 r2"
+ − 254
| "\<Turnstile> v2 : r2 \<Longrightarrow> \<Turnstile> Right v2 : ALT r1 r2"
+ − 255
| "\<Turnstile> Void : EMPTY"
+ − 256
| "\<Turnstile> Char c : CHAR c"
+ − 257
| "\<Turnstile> Stars [] : STAR r"
+ − 258
| "\<lbrakk>\<Turnstile> v : r; \<Turnstile> Stars vs : STAR r; flat v \<noteq> []\<rbrakk> \<Longrightarrow> \<Turnstile> Stars (v # vs) : STAR r"
+ − 259
+ − 260
inductive
+ − 261
Prf :: "val \<Rightarrow> rexp \<Rightarrow> bool" ("\<turnstile> _ : _" [100, 100] 100)
+ − 262
where
+ − 263
"\<lbrakk>\<turnstile> v1 : r1; \<turnstile> v2 : r2\<rbrakk> \<Longrightarrow> \<turnstile> Seq v1 v2 : SEQ r1 r2"
+ − 264
| "\<turnstile> v1 : r1 \<Longrightarrow> \<turnstile> Left v1 : ALT r1 r2"
+ − 265
| "\<turnstile> v2 : r2 \<Longrightarrow> \<turnstile> Right v2 : ALT r1 r2"
+ − 266
| "\<turnstile> Void : EMPTY"
+ − 267
| "\<turnstile> Char c : CHAR c"
+ − 268
| "\<turnstile> Stars [] : STAR r"
+ − 269
| "\<lbrakk>\<turnstile> v : r; \<turnstile> Stars vs : STAR r\<rbrakk> \<Longrightarrow> \<turnstile> Stars (v # vs) : STAR r"
+ − 270
+ − 271
lemma NPrf_imp_Prf:
+ − 272
assumes "\<Turnstile> v : r"
+ − 273
shows "\<turnstile> v : r"
+ − 274
using assms
+ − 275
apply(induct)
+ − 276
apply(auto intro: Prf.intros)
+ − 277
done
+ − 278
+ − 279
lemma NPrf_Prf_val:
+ − 280
shows "\<turnstile> v : r \<Longrightarrow> \<exists>v'. flat v' = flat v \<and> \<Turnstile> v' : r"
+ − 281
and "\<turnstile> Stars vs : r \<Longrightarrow> \<exists>vs'. flat (Stars vs') = flat (Stars vs) \<and> \<Turnstile> Stars vs' : r"
+ − 282
using assms
+ − 283
apply(induct v and vs arbitrary: r and r rule: val.inducts)
+ − 284
apply(auto)[1]
+ − 285
apply(erule Prf.cases)
+ − 286
apply(simp_all)[7]
+ − 287
apply(rule_tac x="Void" in exI)
+ − 288
apply(simp)
+ − 289
apply(rule NPrf.intros)
+ − 290
apply(erule Prf.cases)
+ − 291
apply(simp_all)[7]
+ − 292
apply(rule_tac x="Char c" in exI)
+ − 293
apply(simp)
+ − 294
apply(rule NPrf.intros)
+ − 295
apply(erule Prf.cases)
+ − 296
apply(simp_all)[7]
+ − 297
apply(auto)[1]
+ − 298
apply(drule_tac x="r1" in meta_spec)
+ − 299
apply(drule_tac x="r2" in meta_spec)
+ − 300
apply(simp)
+ − 301
apply(auto)[1]
+ − 302
apply(rule_tac x="Seq v' v'a" in exI)
+ − 303
apply(simp)
+ − 304
apply (metis NPrf.intros(1))
+ − 305
apply(erule Prf.cases)
+ − 306
apply(simp_all)[7]
+ − 307
apply(clarify)
+ − 308
apply(drule_tac x="r2" in meta_spec)
+ − 309
apply(simp)
+ − 310
apply(auto)[1]
+ − 311
apply(rule_tac x="Right v'" in exI)
+ − 312
apply(simp)
+ − 313
apply (metis NPrf.intros)
+ − 314
apply(erule Prf.cases)
+ − 315
apply(simp_all)[7]
+ − 316
apply(clarify)
+ − 317
apply(drule_tac x="r1" in meta_spec)
+ − 318
apply(simp)
+ − 319
apply(auto)[1]
+ − 320
apply(rule_tac x="Left v'" in exI)
+ − 321
apply(simp)
+ − 322
apply (metis NPrf.intros)
+ − 323
apply(drule_tac x="r" in meta_spec)
+ − 324
apply(simp)
+ − 325
apply(auto)[1]
+ − 326
apply(rule_tac x="Stars vs'" in exI)
+ − 327
apply(simp)
+ − 328
apply(rule_tac x="[]" in exI)
+ − 329
apply(simp)
+ − 330
apply(erule Prf.cases)
+ − 331
apply(simp_all)[7]
+ − 332
apply (metis NPrf.intros(6))
+ − 333
apply(erule Prf.cases)
+ − 334
apply(simp_all)[7]
+ − 335
apply(auto)[1]
+ − 336
apply(drule_tac x="ra" in meta_spec)
+ − 337
apply(simp)
+ − 338
apply(drule_tac x="STAR ra" in meta_spec)
+ − 339
apply(simp)
+ − 340
apply(auto)
+ − 341
apply(case_tac "flat v = []")
+ − 342
apply(rule_tac x="vs'" in exI)
+ − 343
apply(simp)
+ − 344
apply(rule_tac x="v' # vs'" in exI)
+ − 345
apply(simp)
+ − 346
apply(rule NPrf.intros)
+ − 347
apply(auto)
+ − 348
done
+ − 349
+ − 350
lemma NPrf_Prf:
+ − 351
shows "{flat v | v. \<turnstile> v : r} = {flat v | v. \<Turnstile> v : r}"
+ − 352
apply(auto)
+ − 353
apply (metis NPrf_Prf_val(1))
+ − 354
by (metis NPrf_imp_Prf)
+ − 355
+ − 356
+ − 357
lemma not_nullable_flat:
+ − 358
assumes "\<turnstile> v : r" "\<not>nullable r"
+ − 359
shows "flat v \<noteq> []"
+ − 360
using assms
+ − 361
apply(induct)
+ − 362
apply(auto)
+ − 363
done
+ − 364
+ − 365
lemma Prf_flat_L:
+ − 366
assumes "\<turnstile> v : r" shows "flat v \<in> L r"
+ − 367
using assms
+ − 368
apply(induct v r rule: Prf.induct)
+ − 369
apply(auto simp add: Sequ_def)
+ − 370
done
+ − 371
+ − 372
lemma NPrf_flat_L:
+ − 373
assumes "\<Turnstile> v : r" shows "flat v \<in> L r"
+ − 374
using assms
+ − 375
by (metis NPrf_imp_Prf Prf_flat_L)
+ − 376
+ − 377
lemma Prf_Stars:
+ − 378
assumes "\<forall>v \<in> set vs. \<turnstile> v : r"
+ − 379
shows "\<turnstile> Stars vs : STAR r"
+ − 380
using assms
+ − 381
apply(induct vs)
+ − 382
apply (metis Prf.intros(6))
+ − 383
by (metis Prf.intros(7) insert_iff set_simps(2))
+ − 384
+ − 385
lemma Star_string:
+ − 386
assumes "s \<in> A\<star>"
+ − 387
shows "\<exists>ss. concat ss = s \<and> (\<forall>s \<in> set ss. s \<in> A)"
+ − 388
using assms
+ − 389
apply(induct rule: Star.induct)
+ − 390
apply(auto)
+ − 391
apply(rule_tac x="[]" in exI)
+ − 392
apply(simp)
+ − 393
apply(rule_tac x="s1#ss" in exI)
+ − 394
apply(simp)
+ − 395
done
+ − 396
+ − 397
lemma Star_val:
+ − 398
assumes "\<forall>s\<in>set ss. \<exists>v. s = flat v \<and> \<turnstile> v : r"
+ − 399
shows "\<exists>vs. concat (map flat vs) = concat ss \<and> (\<forall>v\<in>set vs. \<turnstile> v : r)"
+ − 400
using assms
+ − 401
apply(induct ss)
+ − 402
apply(auto)
+ − 403
apply (metis empty_iff list.set(1))
+ − 404
by (metis concat.simps(2) list.simps(9) set_ConsD)
+ − 405
+ − 406
lemma Star_valN:
+ − 407
assumes "\<forall>s\<in>set ss. \<exists>v. s = flat v \<and> \<Turnstile> v : r"
+ − 408
shows "\<exists>vs. concat (map flat vs) = concat ss \<and> (\<forall>v\<in>set vs. \<Turnstile> v : r)"
+ − 409
using assms
+ − 410
apply(induct ss)
+ − 411
apply(auto)
+ − 412
apply (metis empty_iff list.set(1))
+ − 413
by (metis concat.simps(2) list.simps(9) set_ConsD)
+ − 414
+ − 415
lemma L_flat_Prf:
+ − 416
"L(r) = {flat v | v. \<turnstile> v : r}"
+ − 417
apply(induct r)
+ − 418
apply(auto dest: Prf_flat_L simp add: Sequ_def)
+ − 419
apply (metis Prf.intros(4) flat.simps(1))
+ − 420
apply (metis Prf.intros(5) flat.simps(2))
+ − 421
apply (metis Prf.intros(1) flat.simps(5))
+ − 422
apply (metis Prf.intros(2) flat.simps(3))
+ − 423
apply (metis Prf.intros(3) flat.simps(4))
+ − 424
apply(erule Prf.cases)
+ − 425
apply(auto)
+ − 426
apply(subgoal_tac "\<exists>vs::val list. concat (map flat vs) = x \<and> (\<forall>v \<in> set vs. \<turnstile> v : r)")
+ − 427
apply(auto)[1]
+ − 428
apply(rule_tac x="Stars vs" in exI)
+ − 429
apply(simp)
+ − 430
apply(rule Prf_Stars)
+ − 431
apply(simp)
+ − 432
apply(drule Star_string)
+ − 433
apply(auto)
+ − 434
apply(rule Star_val)
+ − 435
apply(simp)
+ − 436
done
+ − 437
+ − 438
lemma L_flat_NPrf:
+ − 439
"L(r) = {flat v | v. \<Turnstile> v : r}"
+ − 440
by (metis L_flat_Prf NPrf_Prf)
+ − 441
+ − 442
text {* nicer proofs by Fahad *}
+ − 443
+ − 444
lemma Prf_Star_flat_L:
+ − 445
assumes "\<turnstile> v : STAR r" shows "flat v \<in> (L r)\<star>"
+ − 446
using assms
+ − 447
apply(induct v r\<equiv>"STAR r" arbitrary: r rule: Prf.induct)
+ − 448
apply(auto)
+ − 449
apply(simp add: star3)
+ − 450
apply(auto)
+ − 451
apply(rule_tac x="Suc x" in exI)
+ − 452
apply(auto simp add: Sequ_def)
+ − 453
apply(rule_tac x="flat v" in exI)
+ − 454
apply(rule_tac x="flat (Stars vs)" in exI)
+ − 455
apply(auto)
+ − 456
by (metis Prf_flat_L)
+ − 457
+ − 458
lemma L_flat_Prf2:
+ − 459
"L(r) = {flat v | v. \<turnstile> v : r}"
+ − 460
apply(induct r)
+ − 461
apply(auto)
+ − 462
using L.simps(1) Prf_flat_L
+ − 463
apply(blast)
+ − 464
using Prf.intros(4)
+ − 465
apply(force)
+ − 466
using L.simps(2) Prf_flat_L
+ − 467
apply(blast)
+ − 468
using Prf.intros(5) apply force
+ − 469
using L.simps(3) Prf_flat_L apply blast
+ − 470
using L_flat_Prf apply auto[1]
+ − 471
apply (smt L.simps(4) Sequ_def mem_Collect_eq)
+ − 472
using Prf_flat_L
+ − 473
apply(fastforce)
+ − 474
apply(metis Prf.intros(2) flat.simps(3))
+ − 475
apply(metis Prf.intros(3) flat.simps(4))
+ − 476
apply(erule Prf.cases)
+ − 477
apply(simp)
+ − 478
apply(simp)
+ − 479
apply(auto)
+ − 480
using L_flat_Prf apply auto[1]
+ − 481
apply (smt Collect_cong L.simps(6) mem_Collect_eq)
+ − 482
using Prf_Star_flat_L
+ − 483
apply(fastforce)
+ − 484
done
+ − 485
+ − 486
+ − 487
section {* Values Sets *}
+ − 488
+ − 489
definition prefix :: "string \<Rightarrow> string \<Rightarrow> bool" ("_ \<sqsubseteq> _" [100, 100] 100)
+ − 490
where
+ − 491
"s1 \<sqsubseteq> s2 \<equiv> \<exists>s3. s1 @ s3 = s2"
+ − 492
+ − 493
definition sprefix :: "string \<Rightarrow> string \<Rightarrow> bool" ("_ \<sqsubset> _" [100, 100] 100)
+ − 494
where
+ − 495
"s1 \<sqsubset> s2 \<equiv> (s1 \<sqsubseteq> s2 \<and> s1 \<noteq> s2)"
+ − 496
+ − 497
lemma length_sprefix:
+ − 498
"s1 \<sqsubset> s2 \<Longrightarrow> length s1 < length s2"
+ − 499
unfolding sprefix_def prefix_def
+ − 500
by (auto)
+ − 501
+ − 502
definition Prefixes :: "string \<Rightarrow> string set" where
+ − 503
"Prefixes s \<equiv> {sp. sp \<sqsubseteq> s}"
+ − 504
+ − 505
definition Suffixes :: "string \<Rightarrow> string set" where
+ − 506
"Suffixes s \<equiv> rev ` (Prefixes (rev s))"
+ − 507
+ − 508
definition SPrefixes :: "string \<Rightarrow> string set" where
+ − 509
"SPrefixes s \<equiv> {sp. sp \<sqsubset> s}"
+ − 510
+ − 511
definition SSuffixes :: "string \<Rightarrow> string set" where
+ − 512
"SSuffixes s \<equiv> rev ` (SPrefixes (rev s))"
+ − 513
+ − 514
lemma Suffixes_in:
+ − 515
"\<exists>s1. s1 @ s2 = s3 \<Longrightarrow> s2 \<in> Suffixes s3"
+ − 516
unfolding Suffixes_def Prefixes_def prefix_def image_def
+ − 517
apply(auto)
+ − 518
by (metis rev_rev_ident)
+ − 519
+ − 520
lemma SSuffixes_in:
+ − 521
"\<exists>s1. s1 \<noteq> [] \<and> s1 @ s2 = s3 \<Longrightarrow> s2 \<in> SSuffixes s3"
+ − 522
unfolding SSuffixes_def Suffixes_def SPrefixes_def Prefixes_def sprefix_def prefix_def image_def
+ − 523
apply(auto)
+ − 524
by (metis append_self_conv rev.simps(1) rev_rev_ident)
+ − 525
+ − 526
lemma Prefixes_Cons:
+ − 527
"Prefixes (c # s) = {[]} \<union> {c # sp | sp. sp \<in> Prefixes s}"
+ − 528
unfolding Prefixes_def prefix_def
+ − 529
apply(auto simp add: append_eq_Cons_conv)
+ − 530
done
+ − 531
+ − 532
lemma finite_Prefixes:
+ − 533
"finite (Prefixes s)"
+ − 534
apply(induct s)
+ − 535
apply(auto simp add: Prefixes_def prefix_def)[1]
+ − 536
apply(simp add: Prefixes_Cons)
+ − 537
done
+ − 538
+ − 539
lemma finite_Suffixes:
+ − 540
"finite (Suffixes s)"
+ − 541
unfolding Suffixes_def
+ − 542
apply(rule finite_imageI)
+ − 543
apply(rule finite_Prefixes)
+ − 544
done
+ − 545
+ − 546
lemma prefix_Cons:
+ − 547
"((c # s1) \<sqsubseteq> (c # s2)) = (s1 \<sqsubseteq> s2)"
+ − 548
apply(auto simp add: prefix_def)
+ − 549
done
+ − 550
+ − 551
lemma prefix_append:
+ − 552
"((s @ s1) \<sqsubseteq> (s @ s2)) = (s1 \<sqsubseteq> s2)"
+ − 553
apply(induct s)
+ − 554
apply(simp)
+ − 555
apply(simp add: prefix_Cons)
+ − 556
done
+ − 557
+ − 558
+ − 559
definition Values :: "rexp \<Rightarrow> string \<Rightarrow> val set" where
+ − 560
"Values r s \<equiv> {v. \<turnstile> v : r \<and> flat v \<sqsubseteq> s}"
+ − 561
+ − 562
definition SValues :: "rexp \<Rightarrow> string \<Rightarrow> val set" where
+ − 563
"SValues r s \<equiv> {v. \<turnstile> v : r \<and> flat v = s}"
+ − 564
+ − 565
+ − 566
definition NValues :: "rexp \<Rightarrow> string \<Rightarrow> val set" where
+ − 567
"NValues r s \<equiv> {v. \<Turnstile> v : r \<and> flat v \<sqsubseteq> s}"
+ − 568
+ − 569
lemma NValues_STAR_Nil:
+ − 570
"NValues (STAR r) [] = {Stars []}"
+ − 571
apply(auto simp add: NValues_def prefix_def)
+ − 572
apply(erule NPrf.cases)
+ − 573
apply(auto)
+ − 574
by (metis NPrf.intros(6))
+ − 575
+ − 576
+ − 577
definition rest :: "val \<Rightarrow> string \<Rightarrow> string" where
+ − 578
"rest v s \<equiv> drop (length (flat v)) s"
+ − 579
+ − 580
lemma rest_Nil:
+ − 581
"rest v [] = []"
+ − 582
apply(simp add: rest_def)
+ − 583
done
+ − 584
+ − 585
lemma rest_Suffixes:
+ − 586
"rest v s \<in> Suffixes s"
+ − 587
unfolding rest_def
+ − 588
by (metis Suffixes_in append_take_drop_id)
+ − 589
+ − 590
lemma rest_SSuffixes:
+ − 591
assumes "flat v \<noteq> []" "s \<noteq> []"
+ − 592
shows "rest v s \<in> SSuffixes s"
+ − 593
using assms
+ − 594
unfolding rest_def
+ − 595
thm SSuffixes_in
+ − 596
apply(rule_tac SSuffixes_in)
+ − 597
apply(rule_tac x="take (length (flat v)) s" in exI)
+ − 598
apply(simp add: sprefix_def)
+ − 599
done
+ − 600
+ − 601
+ − 602
lemma Values_recs:
+ − 603
"Values (NULL) s = {}"
+ − 604
"Values (EMPTY) s = {Void}"
+ − 605
"Values (CHAR c) s = (if [c] \<sqsubseteq> s then {Char c} else {})"
+ − 606
"Values (ALT r1 r2) s = {Left v | v. v \<in> Values r1 s} \<union> {Right v | v. v \<in> Values r2 s}"
+ − 607
"Values (SEQ r1 r2) s = {Seq v1 v2 | v1 v2. v1 \<in> Values r1 s \<and> v2 \<in> Values r2 (rest v1 s)}"
+ − 608
"Values (STAR r) s =
+ − 609
{Stars []} \<union> {Stars (v # vs) | v vs. v \<in> Values r s \<and> Stars vs \<in> Values (STAR r) (rest v s)}"
+ − 610
unfolding Values_def
+ − 611
apply(auto)
+ − 612
(*NULL*)
+ − 613
apply(erule Prf.cases)
+ − 614
apply(simp_all)[7]
+ − 615
(*EMPTY*)
+ − 616
apply(erule Prf.cases)
+ − 617
apply(simp_all)[7]
+ − 618
apply(rule Prf.intros)
+ − 619
apply (metis append_Nil prefix_def)
+ − 620
(*CHAR*)
+ − 621
apply(erule Prf.cases)
+ − 622
apply(simp_all)[7]
+ − 623
apply(rule Prf.intros)
+ − 624
apply(erule Prf.cases)
+ − 625
apply(simp_all)[7]
+ − 626
(*ALT*)
+ − 627
apply(erule Prf.cases)
+ − 628
apply(simp_all)[7]
+ − 629
apply (metis Prf.intros(2))
+ − 630
apply (metis Prf.intros(3))
+ − 631
(*SEQ*)
+ − 632
apply(erule Prf.cases)
+ − 633
apply(simp_all)[7]
+ − 634
apply (simp add: append_eq_conv_conj prefix_def rest_def)
+ − 635
apply (metis Prf.intros(1))
+ − 636
apply (simp add: append_eq_conv_conj prefix_def rest_def)
+ − 637
(*STAR*)
+ − 638
apply(erule Prf.cases)
+ − 639
apply(simp_all)[7]
+ − 640
apply(rule conjI)
+ − 641
apply(simp add: prefix_def)
+ − 642
apply(auto)[1]
+ − 643
apply(simp add: prefix_def)
+ − 644
apply(auto)[1]
+ − 645
apply (metis append_eq_conv_conj rest_def)
+ − 646
apply (metis Prf.intros(6))
+ − 647
apply (metis append_Nil prefix_def)
+ − 648
apply (metis Prf.intros(7))
+ − 649
by (metis append_eq_conv_conj prefix_append prefix_def rest_def)
+ − 650
+ − 651
lemma NValues_recs:
+ − 652
"NValues (NULL) s = {}"
+ − 653
"NValues (EMPTY) s = {Void}"
+ − 654
"NValues (CHAR c) s = (if [c] \<sqsubseteq> s then {Char c} else {})"
+ − 655
"NValues (ALT r1 r2) s = {Left v | v. v \<in> NValues r1 s} \<union> {Right v | v. v \<in> NValues r2 s}"
+ − 656
"NValues (SEQ r1 r2) s = {Seq v1 v2 | v1 v2. v1 \<in> NValues r1 s \<and> v2 \<in> NValues r2 (rest v1 s)}"
+ − 657
"NValues (STAR r) s =
+ − 658
{Stars []} \<union> {Stars (v # vs) | v vs. v \<in> NValues r s \<and> flat v \<noteq> [] \<and> Stars vs \<in> NValues (STAR r) (rest v s)}"
+ − 659
unfolding NValues_def
+ − 660
apply(auto)
+ − 661
(*NULL*)
+ − 662
apply(erule NPrf.cases)
+ − 663
apply(simp_all)[7]
+ − 664
(*EMPTY*)
+ − 665
apply(erule NPrf.cases)
+ − 666
apply(simp_all)[7]
+ − 667
apply(rule NPrf.intros)
+ − 668
apply (metis append_Nil prefix_def)
+ − 669
(*CHAR*)
+ − 670
apply(erule NPrf.cases)
+ − 671
apply(simp_all)[7]
+ − 672
apply(rule NPrf.intros)
+ − 673
apply(erule NPrf.cases)
+ − 674
apply(simp_all)[7]
+ − 675
(*ALT*)
+ − 676
apply(erule NPrf.cases)
+ − 677
apply(simp_all)[7]
+ − 678
apply (metis NPrf.intros(2))
+ − 679
apply (metis NPrf.intros(3))
+ − 680
(*SEQ*)
+ − 681
apply(erule NPrf.cases)
+ − 682
apply(simp_all)[7]
+ − 683
apply (simp add: append_eq_conv_conj prefix_def rest_def)
+ − 684
apply (metis NPrf.intros(1))
+ − 685
apply (simp add: append_eq_conv_conj prefix_def rest_def)
+ − 686
(*STAR*)
+ − 687
apply(erule NPrf.cases)
+ − 688
apply(simp_all)
+ − 689
apply(rule conjI)
+ − 690
apply(simp add: prefix_def)
+ − 691
apply(auto)[1]
+ − 692
apply(simp add: prefix_def)
+ − 693
apply(auto)[1]
+ − 694
apply (metis append_eq_conv_conj rest_def)
+ − 695
apply (metis NPrf.intros(6))
+ − 696
apply (metis append_Nil prefix_def)
+ − 697
apply (metis NPrf.intros(7))
+ − 698
by (metis append_eq_conv_conj prefix_append prefix_def rest_def)
+ − 699
+ − 700
lemma SValues_recs:
+ − 701
"SValues (NULL) s = {}"
+ − 702
"SValues (EMPTY) s = (if s = [] then {Void} else {})"
+ − 703
"SValues (CHAR c) s = (if [c] = s then {Char c} else {})"
+ − 704
"SValues (ALT r1 r2) s = {Left v | v. v \<in> SValues r1 s} \<union> {Right v | v. v \<in> SValues r2 s}"
+ − 705
"SValues (SEQ r1 r2) s = {Seq v1 v2 | v1 v2. \<exists>s1 s2. s = s1 @ s2 \<and> v1 \<in> SValues r1 s1 \<and> v2 \<in> SValues r2 s2}"
+ − 706
"SValues (STAR r) s = (if s = [] then {Stars []} else {}) \<union>
+ − 707
{Stars (v # vs) | v vs. \<exists>s1 s2. s = s1 @ s2 \<and> v \<in> SValues r s1 \<and> Stars vs \<in> SValues (STAR r) s2}"
+ − 708
unfolding SValues_def
+ − 709
apply(auto)
+ − 710
(*NULL*)
+ − 711
apply(erule Prf.cases)
+ − 712
apply(simp_all)[7]
+ − 713
(*EMPTY*)
+ − 714
apply(erule Prf.cases)
+ − 715
apply(simp_all)[7]
+ − 716
apply(rule Prf.intros)
+ − 717
apply(erule Prf.cases)
+ − 718
apply(simp_all)[7]
+ − 719
(*CHAR*)
+ − 720
apply(erule Prf.cases)
+ − 721
apply(simp_all)[7]
+ − 722
apply (metis Prf.intros(5))
+ − 723
apply(erule Prf.cases)
+ − 724
apply(simp_all)[7]
+ − 725
(*ALT*)
+ − 726
apply(erule Prf.cases)
+ − 727
apply(simp_all)[7]
+ − 728
apply metis
+ − 729
apply(erule Prf.intros)
+ − 730
apply(erule Prf.intros)
+ − 731
(* SEQ case *)
+ − 732
apply(erule Prf.cases)
+ − 733
apply(simp_all)[7]
+ − 734
apply (metis Prf.intros(1))
+ − 735
(* STAR case *)
+ − 736
apply(erule Prf.cases)
+ − 737
apply(simp_all)[7]
+ − 738
apply(rule Prf.intros)
+ − 739
apply (metis Prf.intros(7))
+ − 740
apply(erule Prf.cases)
+ − 741
apply(simp_all)[7]
+ − 742
apply (metis Prf.intros(7))
+ − 743
by (metis Prf.intros(7))
+ − 744
+ − 745
lemma finite_image_set2:
+ − 746
"finite {x. P x} \<Longrightarrow> finite {y. Q y} \<Longrightarrow> finite {(x, y) | x y. P x \<and> Q y}"
+ − 747
by (rule finite_subset [where B = "\<Union>x \<in> {x. P x}. \<Union>y \<in> {y. Q y}. {(x, y)}"]) auto
+ − 748
+ − 749
+ − 750
lemma NValues_finite_aux:
+ − 751
"(\<lambda>(r, s). finite (NValues r s)) (r, s)"
+ − 752
apply(rule wf_induct[of "measure size <*lex*> measure length",where P="\<lambda>(r, s). finite (NValues r s)"])
+ − 753
apply (metis wf_lex_prod wf_measure)
+ − 754
apply(auto)
+ − 755
apply(case_tac a)
+ − 756
apply(simp_all)
+ − 757
apply(simp add: NValues_recs)
+ − 758
apply(simp add: NValues_recs)
+ − 759
apply(simp add: NValues_recs)
+ − 760
apply(simp add: NValues_recs)
+ − 761
apply(rule_tac f="\<lambda>(x, y). Seq x y" and
+ − 762
A="{(v1, v2) | v1 v2. v1 \<in> NValues rexp1 b \<and> v2 \<in> NValues rexp2 (rest v1 b)}" in finite_surj)
+ − 763
prefer 2
+ − 764
apply(auto)[1]
+ − 765
apply(rule_tac B="\<Union>sp \<in> Suffixes b. {(v1, v2). v1 \<in> NValues rexp1 b \<and> v2 \<in> NValues rexp2 sp}" in finite_subset)
+ − 766
apply(auto)[1]
+ − 767
apply (metis rest_Suffixes)
+ − 768
apply(rule finite_UN_I)
+ − 769
apply(rule finite_Suffixes)
+ − 770
apply(simp)
+ − 771
apply(simp add: NValues_recs)
+ − 772
apply(clarify)
+ − 773
apply(subst NValues_recs)
+ − 774
apply(simp)
+ − 775
apply(rule_tac f="\<lambda>(v, vs). Stars (v # vs)" and
+ − 776
A="{(v, vs) | v vs. v \<in> NValues rexp b \<and> (flat v \<noteq> [] \<and> Stars vs \<in> NValues (STAR rexp) (rest v b))}" in finite_surj)
+ − 777
prefer 2
+ − 778
apply(auto)[1]
+ − 779
apply(auto)
+ − 780
apply(case_tac b)
+ − 781
apply(simp)
+ − 782
defer
+ − 783
apply(rule_tac B="\<Union>sp \<in> SSuffixes b. {(v, vs) | v vs. v \<in> NValues rexp b \<and> Stars vs \<in> NValues (STAR rexp) sp}" in finite_subset)
+ − 784
apply(auto)[1]
+ − 785
apply(rule_tac x="rest aa (a # list)" in bexI)
+ − 786
apply(simp)
+ − 787
apply (rule rest_SSuffixes)
+ − 788
apply(simp)
+ − 789
apply(simp)
+ − 790
apply(rule finite_UN_I)
+ − 791
defer
+ − 792
apply(frule_tac x="rexp" in spec)
+ − 793
apply(drule_tac x="b" in spec)
+ − 794
apply(drule conjunct1)
+ − 795
apply(drule mp)
+ − 796
apply(simp)
+ − 797
apply(drule_tac x="STAR rexp" in spec)
+ − 798
apply(drule_tac x="sp" in spec)
+ − 799
apply(drule conjunct2)
+ − 800
apply(drule mp)
+ − 801
apply(simp)
+ − 802
apply(simp add: prefix_def SPrefixes_def SSuffixes_def)
+ − 803
apply(auto)[1]
+ − 804
apply (metis length_Cons length_rev length_sprefix rev.simps(2))
+ − 805
apply(simp)
+ − 806
apply(rule finite_cartesian_product)
+ − 807
apply(simp)
+ − 808
apply(rule_tac f="Stars" in finite_imageD)
+ − 809
prefer 2
+ − 810
apply(auto simp add: inj_on_def)[1]
+ − 811
apply (metis finite_subset image_Collect_subsetI)
+ − 812
apply(simp add: rest_Nil)
+ − 813
apply(simp add: NValues_STAR_Nil)
+ − 814
apply(rule_tac B="{(v, vs). v \<in> NValues rexp [] \<and> vs = []}" in finite_subset)
+ − 815
apply(auto)[1]
+ − 816
apply(simp)
+ − 817
apply(rule_tac B="Suffixes b" in finite_subset)
+ − 818
apply(auto simp add: SSuffixes_def Suffixes_def Prefixes_def SPrefixes_def sprefix_def)[1]
+ − 819
by (metis finite_Suffixes)
+ − 820
+ − 821
lemma NValues_finite:
+ − 822
"finite (NValues r s)"
+ − 823
using NValues_finite_aux
+ − 824
apply(simp)
+ − 825
done
+ − 826
+ − 827
section {* Sulzmann functions *}
+ − 828
+ − 829
fun
+ − 830
mkeps :: "rexp \<Rightarrow> val"
+ − 831
where
+ − 832
"mkeps(EMPTY) = Void"
+ − 833
| "mkeps(SEQ r1 r2) = Seq (mkeps r1) (mkeps r2)"
+ − 834
| "mkeps(ALT r1 r2) = (if nullable(r1) then Left (mkeps r1) else Right (mkeps r2))"
+ − 835
| "mkeps(STAR r) = Stars []"
+ − 836
+ − 837
section {* Derivatives *}
+ − 838
+ − 839
fun
+ − 840
der :: "char \<Rightarrow> rexp \<Rightarrow> rexp"
+ − 841
where
+ − 842
"der c (NULL) = NULL"
+ − 843
| "der c (EMPTY) = NULL"
+ − 844
| "der c (CHAR c') = (if c = c' then EMPTY else NULL)"
+ − 845
| "der c (ALT r1 r2) = ALT (der c r1) (der c r2)"
+ − 846
| "der c (SEQ r1 r2) =
+ − 847
(if nullable r1
+ − 848
then ALT (SEQ (der c r1) r2) (der c r2)
+ − 849
else SEQ (der c r1) r2)"
+ − 850
| "der c (STAR r) = SEQ (der c r) (STAR r)"
+ − 851
+ − 852
fun
+ − 853
ders :: "string \<Rightarrow> rexp \<Rightarrow> rexp"
+ − 854
where
+ − 855
"ders [] r = r"
+ − 856
| "ders (c # s) r = ders s (der c r)"
+ − 857
+ − 858
+ − 859
lemma der_correctness:
+ − 860
shows "L (der c r) = Der c (L r)"
+ − 861
apply(induct r)
+ − 862
apply(simp_all add: nullable_correctness)
+ − 863
done
+ − 864
+ − 865
lemma ders_correctness:
+ − 866
shows "L (ders s r) = Ders s (L r)"
+ − 867
apply(induct s arbitrary: r)
+ − 868
apply(simp add: Ders_def)
+ − 869
apply(simp)
+ − 870
apply(subst der_correctness)
+ − 871
apply(simp add: Ders_def Der_def)
+ − 872
done
+ − 873
+ − 874
section {* Injection function *}
+ − 875
+ − 876
fun injval :: "rexp \<Rightarrow> char \<Rightarrow> val \<Rightarrow> val"
+ − 877
where
+ − 878
"injval (CHAR d) c Void = Char d"
+ − 879
| "injval (ALT r1 r2) c (Left v1) = Left(injval r1 c v1)"
+ − 880
| "injval (ALT r1 r2) c (Right v2) = Right(injval r2 c v2)"
+ − 881
| "injval (SEQ r1 r2) c (Seq v1 v2) = Seq (injval r1 c v1) v2"
+ − 882
| "injval (SEQ r1 r2) c (Left (Seq v1 v2)) = Seq (injval r1 c v1) v2"
+ − 883
| "injval (SEQ r1 r2) c (Right v2) = Seq (mkeps r1) (injval r2 c v2)"
+ − 884
| "injval (STAR r) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)"
+ − 885
+ − 886
fun
+ − 887
lex :: "rexp \<Rightarrow> string \<Rightarrow> val option"
+ − 888
where
+ − 889
"lex r [] = (if nullable r then Some(mkeps r) else None)"
+ − 890
| "lex r (c#s) = (case (lex (der c r) s) of
+ − 891
None \<Rightarrow> None
+ − 892
| Some(v) \<Rightarrow> Some(injval r c v))"
+ − 893
+ − 894
fun
+ − 895
lex2 :: "rexp \<Rightarrow> string \<Rightarrow> val"
+ − 896
where
+ − 897
"lex2 r [] = mkeps r"
+ − 898
| "lex2 r (c#s) = injval r c (lex2 (der c r) s)"
+ − 899
+ − 900
+ − 901
section {* Projection function *}
+ − 902
+ − 903
fun projval :: "rexp \<Rightarrow> char \<Rightarrow> val \<Rightarrow> val"
+ − 904
where
+ − 905
"projval (CHAR d) c _ = Void"
+ − 906
| "projval (ALT r1 r2) c (Left v1) = Left (projval r1 c v1)"
+ − 907
| "projval (ALT r1 r2) c (Right v2) = Right (projval r2 c v2)"
+ − 908
| "projval (SEQ r1 r2) c (Seq v1 v2) =
+ − 909
(if flat v1 = [] then Right(projval r2 c v2)
+ − 910
else if nullable r1 then Left (Seq (projval r1 c v1) v2)
+ − 911
else Seq (projval r1 c v1) v2)"
+ − 912
| "projval (STAR r) c (Stars (v # vs)) = Seq (projval r c v) (Stars vs)"
+ − 913
+ − 914
+ − 915
+ − 916
lemma mkeps_nullable:
+ − 917
assumes "nullable(r)"
+ − 918
shows "\<turnstile> mkeps r : r"
+ − 919
using assms
+ − 920
apply(induct rule: nullable.induct)
+ − 921
apply(auto intro: Prf.intros)
+ − 922
done
+ − 923
+ − 924
lemma mkeps_flat:
+ − 925
assumes "nullable(r)"
+ − 926
shows "flat (mkeps r) = []"
+ − 927
using assms
+ − 928
apply(induct rule: nullable.induct)
+ − 929
apply(auto)
+ − 930
done
+ − 931
+ − 932
+ − 933
lemma v3:
+ − 934
assumes "\<turnstile> v : der c r"
+ − 935
shows "\<turnstile> (injval r c v) : r"
+ − 936
using assms
+ − 937
apply(induct arbitrary: v rule: der.induct)
+ − 938
apply(simp)
+ − 939
apply(erule Prf.cases)
+ − 940
apply(simp_all)[7]
+ − 941
apply(simp)
+ − 942
apply(erule Prf.cases)
+ − 943
apply(simp_all)[7]
+ − 944
apply(case_tac "c = c'")
+ − 945
apply(simp)
+ − 946
apply(erule Prf.cases)
+ − 947
apply(simp_all)[7]
+ − 948
apply (metis Prf.intros(5))
+ − 949
apply(simp)
+ − 950
apply(erule Prf.cases)
+ − 951
apply(simp_all)[7]
+ − 952
apply(simp)
+ − 953
apply(erule Prf.cases)
+ − 954
apply(simp_all)[7]
+ − 955
apply (metis Prf.intros(2))
+ − 956
apply (metis Prf.intros(3))
+ − 957
apply(simp)
+ − 958
apply(case_tac "nullable r1")
+ − 959
apply(simp)
+ − 960
apply(erule Prf.cases)
+ − 961
apply(simp_all)[7]
+ − 962
apply(auto)[1]
+ − 963
apply(erule Prf.cases)
+ − 964
apply(simp_all)[7]
+ − 965
apply(auto)[1]
+ − 966
apply (metis Prf.intros(1))
+ − 967
apply(auto)[1]
+ − 968
apply (metis Prf.intros(1) mkeps_nullable)
+ − 969
apply(simp)
+ − 970
apply(erule Prf.cases)
+ − 971
apply(simp_all)[7]
+ − 972
apply(auto)[1]
+ − 973
apply(rule Prf.intros)
+ − 974
apply(auto)[2]
+ − 975
apply(simp)
+ − 976
apply(erule Prf.cases)
+ − 977
apply(simp_all)[7]
+ − 978
apply(clarify)
+ − 979
apply(rotate_tac 2)
+ − 980
apply(erule Prf.cases)
+ − 981
apply(simp_all)[7]
+ − 982
apply(auto)
+ − 983
apply (metis Prf.intros(6) Prf.intros(7))
+ − 984
by (metis Prf.intros(7))
+ − 985
+ − 986
lemma v3_proj:
+ − 987
assumes "\<Turnstile> v : r" and "\<exists>s. (flat v) = c # s"
+ − 988
shows "\<Turnstile> (projval r c v) : der c r"
+ − 989
using assms
+ − 990
apply(induct rule: NPrf.induct)
+ − 991
prefer 4
+ − 992
apply(simp)
+ − 993
prefer 4
+ − 994
apply(simp)
+ − 995
apply (metis NPrf.intros(4))
+ − 996
prefer 2
+ − 997
apply(simp)
+ − 998
apply (metis NPrf.intros(2))
+ − 999
prefer 2
+ − 1000
apply(simp)
+ − 1001
apply (metis NPrf.intros(3))
+ − 1002
apply(auto)
+ − 1003
apply(rule NPrf.intros)
+ − 1004
apply(simp)
+ − 1005
apply (metis NPrf_imp_Prf not_nullable_flat)
+ − 1006
apply(rule NPrf.intros)
+ − 1007
apply(rule NPrf.intros)
+ − 1008
apply (metis Cons_eq_append_conv)
+ − 1009
apply(simp)
+ − 1010
apply(rule NPrf.intros)
+ − 1011
apply (metis Cons_eq_append_conv)
+ − 1012
apply(simp)
+ − 1013
(* Stars case *)
+ − 1014
apply(rule NPrf.intros)
+ − 1015
apply (metis Cons_eq_append_conv)
+ − 1016
apply(auto)
+ − 1017
done
+ − 1018
+ − 1019
lemma v4:
+ − 1020
assumes "\<turnstile> v : der c r"
+ − 1021
shows "flat (injval r c v) = c # (flat v)"
+ − 1022
using assms
+ − 1023
apply(induct arbitrary: v rule: der.induct)
+ − 1024
apply(simp)
+ − 1025
apply(erule Prf.cases)
+ − 1026
apply(simp_all)[7]
+ − 1027
apply(simp)
+ − 1028
apply(erule Prf.cases)
+ − 1029
apply(simp_all)[7]
+ − 1030
apply(simp)
+ − 1031
apply(case_tac "c = c'")
+ − 1032
apply(simp)
+ − 1033
apply(auto)[1]
+ − 1034
apply(erule Prf.cases)
+ − 1035
apply(simp_all)[7]
+ − 1036
apply(simp)
+ − 1037
apply(erule Prf.cases)
+ − 1038
apply(simp_all)[7]
+ − 1039
apply(simp)
+ − 1040
apply(erule Prf.cases)
+ − 1041
apply(simp_all)[7]
+ − 1042
apply(simp)
+ − 1043
apply(case_tac "nullable r1")
+ − 1044
apply(simp)
+ − 1045
apply(erule Prf.cases)
+ − 1046
apply(simp_all (no_asm_use))[7]
+ − 1047
apply(auto)[1]
+ − 1048
apply(erule Prf.cases)
+ − 1049
apply(simp_all)[7]
+ − 1050
apply(clarify)
+ − 1051
apply(simp only: injval.simps flat.simps)
+ − 1052
apply(auto)[1]
+ − 1053
apply (metis mkeps_flat)
+ − 1054
apply(simp)
+ − 1055
apply(erule Prf.cases)
+ − 1056
apply(simp_all)[7]
+ − 1057
apply(simp)
+ − 1058
apply(erule Prf.cases)
+ − 1059
apply(simp_all)[7]
+ − 1060
apply(auto)
+ − 1061
apply(rotate_tac 2)
+ − 1062
apply(erule Prf.cases)
+ − 1063
apply(simp_all)[7]
+ − 1064
done
+ − 1065
+ − 1066
lemma v4_proj:
+ − 1067
assumes "\<Turnstile> v : r" and "\<exists>s. (flat v) = c # s"
+ − 1068
shows "c # flat (projval r c v) = flat v"
+ − 1069
using assms
+ − 1070
apply(induct rule: NPrf.induct)
+ − 1071
prefer 4
+ − 1072
apply(simp)
+ − 1073
prefer 4
+ − 1074
apply(simp)
+ − 1075
prefer 2
+ − 1076
apply(simp)
+ − 1077
prefer 2
+ − 1078
apply(simp)
+ − 1079
apply(auto)
+ − 1080
apply (metis Cons_eq_append_conv)
+ − 1081
apply(simp add: append_eq_Cons_conv)
+ − 1082
apply(auto)
+ − 1083
done
+ − 1084
+ − 1085
lemma v4_proj2:
+ − 1086
assumes "\<Turnstile> v : r" and "(flat v) = c # s"
+ − 1087
shows "flat (projval r c v) = s"
+ − 1088
using assms
+ − 1089
by (metis list.inject v4_proj)
+ − 1090
+ − 1091
+ − 1092
definition
+ − 1093
PC31 :: "string \<Rightarrow> rexp \<Rightarrow> rexp \<Rightarrow> bool"
+ − 1094
where
+ − 1095
"PC31 s r r' \<equiv> s \<notin> L r"
+ − 1096
+ − 1097
definition
+ − 1098
PC41 :: "string \<Rightarrow> string \<Rightarrow> rexp \<Rightarrow> rexp \<Rightarrow> bool"
+ − 1099
where
+ − 1100
"PC41 s s' r r' \<equiv> (\<forall>x. (s @ x \<in> L r \<longrightarrow> s' \<in> {x} ;; L r' \<longrightarrow> x = []))"
+ − 1101
+ − 1102
+ − 1103
lemma
+ − 1104
L1: "\<not>(nullable r1) \<longrightarrow> [] \<in> L r2 \<longrightarrow> PC31 [] r1 r2" and
+ − 1105
L2: "s1 \<in> L(r1) \<longrightarrow> [] \<in> L(r2) \<longrightarrow> PC41 s1 [] r1 r2" and
+ − 1106
L3: "s2 \<in> L(der c r2) \<longrightarrow> PC31 s2 (der c r1) (der c r2) \<longrightarrow> PC31 (c#s2) r1 r2" and
+ − 1107
L4: "s1 \<in> L(der c r1) \<longrightarrow> s2 \<in> L(r2) \<longrightarrow> PC41 s1 s2 (der c r1) r2 \<longrightarrow> PC41 (c#s1) s2 r1 r2" and
+ − 1108
L5: "nullable(r1) \<longrightarrow> s2 \<in> L(der c r2) \<longrightarrow> PC31 s2 (SEQ (der c r1) r2) (der c r2) \<longrightarrow> PC41 [] (c#s2) r1 r2" and
+ − 1109
L6: "s0 \<in> L(der c r0) \<longrightarrow> s \<in> L(STAR r0) \<longrightarrow> PC41 s0 s (der c r0) (STAR r0) \<longrightarrow> PC41 (c#s0) s r0 (STAR r0)" and
+ − 1110
L7: "s' \<in> L(r') \<longrightarrow> s' \<in> L(r) \<longrightarrow> \<not>PC31 s' r r'" and
+ − 1111
L8: "s \<in> L(r) \<longrightarrow> s' \<in> L(r') \<longrightarrow> s @ x \<in> L(r) \<longrightarrow> s' \<in> {x} ;; (L(r') ;; {y}) \<longrightarrow> x \<noteq> [] \<longrightarrow> \<not>PC41 s s' r r'"
+ − 1112
apply(auto simp add: PC31_def PC41_def)[1]
+ − 1113
apply (metis nullable_correctness)
+ − 1114
apply(auto simp add: PC31_def PC41_def)[1]
+ − 1115
apply(simp add: Sequ_def)
+ − 1116
apply(auto simp add: PC31_def PC41_def)[1]
+ − 1117
apply(simp add: der_correctness Der_def)
+ − 1118
apply(auto simp add: PC31_def PC41_def)[1]
+ − 1119
apply(simp add: der_correctness Der_def Sequ_def)
+ − 1120
apply(auto simp add: PC31_def PC41_def)[1]
+ − 1121
apply(simp add: Sequ_def)
+ − 1122
apply(simp add: der_correctness Der_def)
+ − 1123
apply(auto)[1]
+ − 1124
apply (metis append_eq_Cons_conv)
+ − 1125
apply(auto simp add: PC31_def PC41_def)[1]
+ − 1126
apply(simp add: Sequ_def)
+ − 1127
apply(simp add: der_correctness Der_def)
+ − 1128
apply(auto simp add: PC31_def PC41_def)[1]
+ − 1129
apply(rule impI)+
+ − 1130
apply(rule notI)
+ − 1131
(* 8 fails *)
+ − 1132
oops
+ − 1133
+ − 1134
definition
+ − 1135
PC32 :: "string \<Rightarrow> rexp \<Rightarrow> rexp \<Rightarrow> bool"
+ − 1136
where
+ − 1137
"PC32 s r r' \<equiv> \<forall>y. s \<notin> (L r ;; {y})"
+ − 1138
+ − 1139
definition
+ − 1140
PC42 :: "string \<Rightarrow> string \<Rightarrow> rexp \<Rightarrow> rexp \<Rightarrow> bool"
+ − 1141
where
+ − 1142
"PC42 s s' r r' \<equiv> (\<forall>x. (s @ x \<in> L r \<longrightarrow> (\<exists>y. s' \<in> {x} ;; (L r' ;; {y})) \<longrightarrow> x = []))"
+ − 1143
+ − 1144
+ − 1145
lemma
+ − 1146
L1: "\<not>(nullable r1) \<longrightarrow> [] \<in> L r2 \<longrightarrow> PC32 [] r1 r2" and
+ − 1147
L2: "s1 \<in> L(r1) \<longrightarrow> [] \<in> L(r2) \<longrightarrow> PC42 s1 [] r1 r2" and
+ − 1148
L3: "s2 \<in> L(der c r2) \<longrightarrow> PC32 s2 (der c r1) (der c r2) \<longrightarrow> PC32 (c#s2) r1 r2" and
+ − 1149
L4: "s1 \<in> L(der c r1) \<longrightarrow> s2 \<in> L(r2) \<longrightarrow> PC42 s1 s2 (der c r1) r2 \<longrightarrow> PC42 (c#s1) s2 r1 r2" and
+ − 1150
L5: "nullable(r1) \<longrightarrow> s2 \<in> L(der c r2) \<longrightarrow> PC32 s2 (SEQ (der c r1) r2) (der c r2) \<longrightarrow> PC42 [] (c#s2) r1 r2" and
+ − 1151
L6: "s0 \<in> L(der c r0) \<longrightarrow> s \<in> L(STAR r0) \<longrightarrow> PC42 s0 s (der c r0) (STAR r0) \<longrightarrow> PC42 (c#s0) s r0 (STAR r0)" and
+ − 1152
L7: "s' \<in> L(r') \<longrightarrow> s' \<in> L(r) \<longrightarrow> \<not>PC32 s' r r'" and
+ − 1153
L8: "s \<in> L(r) \<longrightarrow> s' \<in> L(r') \<longrightarrow> s @ x \<in> L(r) \<longrightarrow> s' \<in> {x} ;; (L(r') ;; {y}) \<longrightarrow> x \<noteq> [] \<longrightarrow> \<not>PC42 s s' r r'"
+ − 1154
apply(auto simp add: PC32_def PC42_def)[1]
+ − 1155
apply(simp add: Sequ_def)
+ − 1156
apply (metis nullable_correctness)
+ − 1157
apply(auto simp add: PC32_def PC42_def Sequ_def)[1]
+ − 1158
apply(auto simp add: PC32_def PC42_def Sequ_def der_correctness Der_def)[1]
+ − 1159
apply(simp add: Cons_eq_append_conv)
+ − 1160
apply(auto)[1]
+ − 1161
defer
+ − 1162
apply(auto simp add: PC32_def PC42_def Sequ_def der_correctness Der_def)[1]
+ − 1163
apply(auto simp add: PC32_def PC42_def Sequ_def der_correctness Der_def nullable_correctness)[1]
+ − 1164
apply (metis append_Cons append_assoc hd_Cons_tl list.discI list.inject)
+ − 1165
apply(auto simp add: PC32_def PC42_def Sequ_def der_correctness Der_def)[1]
+ − 1166
apply(auto simp add: PC32_def PC42_def Sequ_def der_correctness Der_def)[1]
+ − 1167
apply(auto simp add: PC32_def PC42_def Sequ_def der_correctness Der_def)[1]
+ − 1168
oops
+ − 1169
+ − 1170
definition
+ − 1171
PC33 :: "string \<Rightarrow> rexp \<Rightarrow> rexp \<Rightarrow> bool"
+ − 1172
where
+ − 1173
"PC33 s r r' \<equiv> s \<notin> L r"
+ − 1174
+ − 1175
definition
+ − 1176
PC43 :: "string \<Rightarrow> string \<Rightarrow> rexp \<Rightarrow> rexp \<Rightarrow> bool"
+ − 1177
where
+ − 1178
"PC43 s s' r r' \<equiv> (\<forall>x. (s @ x \<in> L r \<longrightarrow> (\<exists>y. s' \<in> {x} ;; (L r' ;; {y})) \<longrightarrow> x = []))"
+ − 1179
+ − 1180
lemma
+ − 1181
L1: "\<not>(nullable r1) \<longrightarrow> [] \<in> L r2 \<longrightarrow> PC33 [] r1 r2" and
+ − 1182
L2: "s1 \<in> L(r1) \<longrightarrow> [] \<in> L(r2) \<longrightarrow> PC43 s1 [] r1 r2" and
+ − 1183
L3: "s2 \<in> L(der c r2) \<longrightarrow> PC33 s2 (der c r1) (der c r2) \<longrightarrow> PC33 (c#s2) r1 r2" and
+ − 1184
L4: "s1 \<in> L(der c r1) \<longrightarrow> s2 \<in> L(r2) \<longrightarrow> PC43 s1 s2 (der c r1) r2 \<longrightarrow> PC43 (c#s1) s2 r1 r2" and
+ − 1185
L5: "nullable(r1) \<longrightarrow> s2 \<in> L(der c r2) \<longrightarrow> PC33 s2 (SEQ (der c r1) r2) (der c r2) \<longrightarrow> PC43 [] (c#s2) r1 r2" and
+ − 1186
L6: "s0 \<in> L(der c r0) \<longrightarrow> s \<in> L(STAR r0) \<longrightarrow> PC43 s0 s (der c r0) (STAR r0) \<longrightarrow> PC43 (c#s0) s r0 (STAR r0)" and
+ − 1187
L7: "s' \<in> L(r') \<longrightarrow> s' \<in> L(r) \<longrightarrow> \<not>PC33 s' r r'" and
+ − 1188
L8: "s \<in> L(r) \<longrightarrow> s' \<in> L(r') \<longrightarrow> s @ x \<in> L(r) \<longrightarrow> s' \<in> {x} ;; (L(r') ;; {y}) \<longrightarrow> x \<noteq> [] \<longrightarrow> \<not>PC43 s s' r r'"
+ − 1189
apply(auto simp add: PC33_def PC43_def)[1]
+ − 1190
apply (metis nullable_correctness)
+ − 1191
apply(auto simp add: PC33_def PC43_def)[1]
+ − 1192
apply(simp add: Sequ_def)
+ − 1193
apply(auto simp add: PC33_def PC43_def)[1]
+ − 1194
apply(simp add: der_correctness Der_def)
+ − 1195
apply(auto simp add: PC33_def PC43_def)[1]
+ − 1196
apply(simp add: der_correctness Der_def Sequ_def)
+ − 1197
apply metis
+ − 1198
(* 5 *)
+ − 1199
apply(auto simp add: PC33_def PC43_def)[1]
+ − 1200
apply(simp add: Sequ_def)
+ − 1201
apply(simp add: der_correctness Der_def)
+ − 1202
apply(auto)[1]
+ − 1203
defer
+ − 1204
apply(auto simp add: PC33_def PC43_def)[1]
+ − 1205
apply(simp add: Sequ_def)
+ − 1206
apply(simp add: der_correctness Der_def)
+ − 1207
apply metis
+ − 1208
apply(auto simp add: PC33_def PC43_def)[1]
+ − 1209
apply(auto simp add: PC33_def PC43_def)[1]
+ − 1210
(* 5 fails *)
+ − 1211
apply(simp add: Cons_eq_append_conv)
+ − 1212
apply(auto)[1]
+ − 1213
apply(drule_tac x="ys'" in spec)
+ − 1214
apply(simp)
+ − 1215
oops
+ − 1216
+ − 1217
section {* Roy's Definition *}
+ − 1218
+ − 1219
inductive
+ − 1220
Roy :: "val \<Rightarrow> rexp \<Rightarrow> bool" ("\<rhd> _ : _" [100, 100] 100)
+ − 1221
where
+ − 1222
"\<rhd> Void : EMPTY"
+ − 1223
| "\<rhd> Char c : CHAR c"
+ − 1224
| "\<rhd> v : r1 \<Longrightarrow> \<rhd> Left v : ALT r1 r2"
+ − 1225
| "\<lbrakk>\<rhd> v : r2; flat v \<notin> L r1\<rbrakk> \<Longrightarrow> \<rhd> Right v : ALT r1 r2"
+ − 1226
| "\<lbrakk>\<rhd> v1 : r1; \<rhd> v2 : r2; \<not>(\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = flat v2 \<and> (flat v1 @ s\<^sub>3) \<in> L r1 \<and> s\<^sub>4 \<in> L r2)\<rbrakk> \<Longrightarrow>
+ − 1227
\<rhd> Seq v1 v2 : SEQ r1 r2"
+ − 1228
| "\<lbrakk>\<rhd> v : r; \<rhd> Stars vs : STAR r; flat v \<noteq> [];
+ − 1229
\<not>(\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = flat (Stars vs) \<and> (flat v @ s\<^sub>3) \<in> L r \<and> s\<^sub>4 \<in> L (STAR r))\<rbrakk> \<Longrightarrow>
+ − 1230
\<rhd> Stars (v#vs) : STAR r"
+ − 1231
| "\<rhd> Stars [] : STAR r"
+ − 1232
+ − 1233
lemma drop_append:
+ − 1234
assumes "s1 \<sqsubseteq> s2"
+ − 1235
shows "s1 @ drop (length s1) s2 = s2"
+ − 1236
using assms
+ − 1237
apply(simp add: prefix_def)
+ − 1238
apply(auto)
+ − 1239
done
+ − 1240
+ − 1241
lemma royA:
+ − 1242
assumes "\<not>(\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = flat v2 \<and> (flat v1 @ s\<^sub>3) \<in> L r1 \<and> s\<^sub>4 \<in> L r2)"
+ − 1243
shows "\<forall>s. (s \<in> L(ders (flat v1) r1) \<and>
+ − 1244
s \<sqsubseteq> (flat v2) \<and> drop (length s) (flat v2) \<in> L r2 \<longrightarrow> s = [])"
+ − 1245
using assms
+ − 1246
apply -
+ − 1247
apply(rule allI)
+ − 1248
apply(rule impI)
+ − 1249
apply(simp add: ders_correctness)
+ − 1250
apply(simp add: Ders_def)
+ − 1251
thm rest_def
+ − 1252
apply(drule_tac x="s" in spec)
+ − 1253
apply(simp)
+ − 1254
apply(erule disjE)
+ − 1255
apply(simp)
+ − 1256
apply(drule_tac x="drop (length s) (flat v2)" in spec)
+ − 1257
apply(simp add: drop_append)
+ − 1258
done
+ − 1259
+ − 1260
lemma royB:
+ − 1261
assumes "\<forall>s. (s \<in> L(ders (flat v1) r1) \<and>
+ − 1262
s \<sqsubseteq> (flat v2) \<and> drop (length s) (flat v2) \<in> L r2 \<longrightarrow> s = [])"
+ − 1263
shows "\<not>(\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = flat v2 \<and> (flat v1 @ s\<^sub>3) \<in> L r1 \<and> s\<^sub>4 \<in> L r2)"
+ − 1264
using assms
+ − 1265
apply -
+ − 1266
apply(auto simp add: prefix_def ders_correctness Ders_def)
+ − 1267
by (metis append_eq_conv_conj)
+ − 1268
+ − 1269
lemma royC:
+ − 1270
assumes "\<forall>s t. (s \<in> L(ders (flat v1) r1) \<and>
+ − 1271
s \<sqsubseteq> (flat v2 @ t) \<and> drop (length s) (flat v2 @ t) \<in> L r2 \<longrightarrow> s = [])"
+ − 1272
shows "\<not>(\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = flat v2 \<and> (flat v1 @ s\<^sub>3) \<in> L r1 \<and> s\<^sub>4 \<in> L r2)"
+ − 1273
using assms
+ − 1274
apply -
+ − 1275
apply(rule royB)
+ − 1276
apply(rule allI)
+ − 1277
apply(drule_tac x="s" in spec)
+ − 1278
apply(drule_tac x="[]" in spec)
+ − 1279
apply(simp)
+ − 1280
done
+ − 1281
+ − 1282
inductive
+ − 1283
Roy2 :: "val \<Rightarrow> rexp \<Rightarrow> bool" ("2\<rhd> _ : _" [100, 100] 100)
+ − 1284
where
+ − 1285
"2\<rhd> Void : EMPTY"
+ − 1286
| "2\<rhd> Char c : CHAR c"
+ − 1287
| "2\<rhd> v : r1 \<Longrightarrow> 2\<rhd> Left v : ALT r1 r2"
+ − 1288
| "\<lbrakk>2\<rhd> v : r2; \<forall>t. flat v \<notin> (L r1 ;; {t})\<rbrakk> \<Longrightarrow> 2\<rhd> Right v : ALT r1 r2"
+ − 1289
| "\<lbrakk>2\<rhd> v1 : r1; 2\<rhd> v2 : r2;
+ − 1290
\<forall>s. ((flat v1 @ s \<in> L r1) \<and>
+ − 1291
(\<exists>t. s \<sqsubseteq> (flat v2 @ t) \<and> drop (length s) (flat v2) \<in> (L r2 ;; {t}))) \<longrightarrow> s = []\<rbrakk> \<Longrightarrow>
+ − 1292
2\<rhd> Seq v1 v2 : SEQ r1 r2"
+ − 1293
| "\<lbrakk>2\<rhd> v : r; 2\<rhd> Stars vs : STAR r; flat v \<noteq> [];
+ − 1294
\<forall>s. ((flat v @ s \<in> L r) \<and>
+ − 1295
(\<exists>t. s \<sqsubseteq> (flat (Stars vs) @ t) \<and> drop (length s) (flat (Stars vs)) \<in> (L (STAR r) ;; {t}))) \<longrightarrow> s = []\<rbrakk>
+ − 1296
\<Longrightarrow> 2\<rhd> Stars (v#vs) : STAR r"
+ − 1297
| "2\<rhd> Stars [] : STAR r"
+ − 1298
+ − 1299
lemma Roy2_props:
+ − 1300
assumes "2\<rhd> v : r"
+ − 1301
shows "\<turnstile> v : r"
+ − 1302
using assms
+ − 1303
apply(induct)
+ − 1304
apply(auto intro: Prf.intros)
+ − 1305
done
+ − 1306
+ − 1307
lemma Roy_mkeps_nullable:
+ − 1308
assumes "nullable(r)"
+ − 1309
shows "2\<rhd> (mkeps r) : r"
+ − 1310
using assms
+ − 1311
apply(induct rule: nullable.induct)
+ − 1312
apply(auto intro: Roy2.intros)
+ − 1313
apply(rule Roy2.intros)
+ − 1314
apply(simp_all)
+ − 1315
apply(simp add: mkeps_flat)
+ − 1316
apply(simp add: Sequ_def)
+ − 1317
apply (metis nullable_correctness)
+ − 1318
apply(rule Roy2.intros)
+ − 1319
apply(simp_all)
+ − 1320
apply(rule allI)
+ − 1321
apply(rule impI)
+ − 1322
apply(auto simp add: Sequ_def)
+ − 1323
apply(simp add: mkeps_flat)
+ − 1324
apply(auto simp add: prefix_def)
+ − 1325
done
+ − 1326
+ − 1327
section {* Alternative Posix definition *}
+ − 1328
+ − 1329
inductive
+ − 1330
PMatch :: "string \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<in> _ \<rightarrow> _" [100, 100, 100] 100)
+ − 1331
where
+ − 1332
"[] \<in> EMPTY \<rightarrow> Void"
+ − 1333
| "[c] \<in> (CHAR c) \<rightarrow> (Char c)"
+ − 1334
| "s \<in> r1 \<rightarrow> v \<Longrightarrow> s \<in> (ALT r1 r2) \<rightarrow> (Left v)"
+ − 1335
| "\<lbrakk>s \<in> r2 \<rightarrow> v; s \<notin> L(r1)\<rbrakk> \<Longrightarrow> s \<in> (ALT r1 r2) \<rightarrow> (Right v)"
+ − 1336
| "\<lbrakk>s1 \<in> r1 \<rightarrow> v1; s2 \<in> r2 \<rightarrow> v2;
+ − 1337
\<not>(\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (s1 @ s\<^sub>3) \<in> L r1 \<and> s\<^sub>4 \<in> L r2)\<rbrakk> \<Longrightarrow>
+ − 1338
(s1 @ s2) \<in> (SEQ r1 r2) \<rightarrow> (Seq v1 v2)"
+ − 1339
| "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> STAR r \<rightarrow> Stars vs; flat v \<noteq> [];
+ − 1340
\<not>(\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (s1 @ s\<^sub>3) \<in> L r \<and> s\<^sub>4 \<in> L (STAR r))\<rbrakk>
+ − 1341
\<Longrightarrow> (s1 @ s2) \<in> STAR r \<rightarrow> Stars (v # vs)"
+ − 1342
| "[] \<in> STAR r \<rightarrow> Stars []"
+ − 1343
+ − 1344
inductive
+ − 1345
PMatchX :: "string \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("\<turnstile> _ \<in> _ \<rightarrow> _" [100, 100, 100] 100)
+ − 1346
where
+ − 1347
"\<turnstile> s \<in> EMPTY \<rightarrow> Void"
+ − 1348
| "\<turnstile> (c # s) \<in> (CHAR c) \<rightarrow> (Char c)"
+ − 1349
| "\<turnstile> s \<in> r1 \<rightarrow> v \<Longrightarrow> \<turnstile> s \<in> (ALT r1 r2) \<rightarrow> (Left v)"
+ − 1350
| "\<lbrakk>\<turnstile> s \<in> r2 \<rightarrow> v; \<not>(\<exists>s'. s' \<sqsubseteq> s \<and> flat v \<sqsubseteq> s' \<and> s' \<in> L(r1))\<rbrakk> \<Longrightarrow> \<turnstile> s \<in> (ALT r1 r2) \<rightarrow> (Right v)"
+ − 1351
| "\<lbrakk>s1 \<in> r1 \<rightarrow> v1; \<turnstile> s2 \<in> r2 \<rightarrow> v2;
+ − 1352
\<not>(\<exists>s3 s4. s3 \<noteq> [] \<and> (s3 @ s4) \<sqsubseteq> s2 \<and> (s1 @ s3) \<in> L r1 \<and> s4 \<in> L r2)\<rbrakk> \<Longrightarrow>
+ − 1353
\<turnstile> (s1 @ s2) \<in> (SEQ r1 r2) \<rightarrow> (Seq v1 v2)"
+ − 1354
| "\<lbrakk>s1 \<in> r \<rightarrow> v; \<turnstile> s2 \<in> STAR r \<rightarrow> Stars vs; flat v \<noteq> [];
+ − 1355
\<not>(\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> (s\<^sub>3 @ s\<^sub>4) \<sqsubseteq> s2 \<and> (s1 @ s\<^sub>3) \<in> L r \<and> s\<^sub>4 \<in> L (STAR r))\<rbrakk>
+ − 1356
\<Longrightarrow> \<turnstile> (s1 @ s2) \<in> STAR r \<rightarrow> Stars (v # vs)"
+ − 1357
| "\<turnstile> s \<in> STAR r \<rightarrow> Stars []"
+ − 1358
+ − 1359
lemma PMatch1:
+ − 1360
assumes "s \<in> r \<rightarrow> v"
+ − 1361
shows "\<turnstile> v : r" "flat v = s"
+ − 1362
using assms
+ − 1363
apply(induct s r v rule: PMatch.induct)
+ − 1364
apply(auto)
+ − 1365
apply (metis Prf.intros(4))
+ − 1366
apply (metis Prf.intros(5))
+ − 1367
apply (metis Prf.intros(2))
+ − 1368
apply (metis Prf.intros(3))
+ − 1369
apply (metis Prf.intros(1))
+ − 1370
apply (metis Prf.intros(7))
+ − 1371
by (metis Prf.intros(6))
+ − 1372
+ − 1373
+ − 1374
lemma PMatchX1:
+ − 1375
assumes "\<turnstile> s \<in> r \<rightarrow> v"
+ − 1376
shows "\<turnstile> v : r"
+ − 1377
using assms
+ − 1378
apply(induct s r v rule: PMatchX.induct)
+ − 1379
apply(auto simp add: prefix_def intro: Prf.intros)
+ − 1380
apply (metis PMatch1(1) Prf.intros(1))
+ − 1381
by (metis PMatch1(1) Prf.intros(7))
+ − 1382
+ − 1383
+ − 1384
lemma PMatchX:
+ − 1385
assumes "\<turnstile> s \<in> r \<rightarrow> v"
+ − 1386
shows "flat v \<sqsubseteq> s"
+ − 1387
using assms
+ − 1388
apply(induct s r v rule: PMatchX.induct)
+ − 1389
apply(auto simp add: prefix_def PMatch1)
+ − 1390
done
+ − 1391
+ − 1392
lemma PMatchX_PMatch:
+ − 1393
assumes "\<turnstile> s \<in> r \<rightarrow> v" "flat v = s"
+ − 1394
shows "s \<in> r \<rightarrow> v"
+ − 1395
using assms
+ − 1396
apply(induct s r v rule: PMatchX.induct)
+ − 1397
apply(auto intro: PMatch.intros)
+ − 1398
apply(rule PMatch.intros)
+ − 1399
apply(simp)
+ − 1400
apply (metis PMatchX Prefixes_def mem_Collect_eq)
+ − 1401
apply (smt2 PMatch.intros(5) PMatch1(2) PMatchX append_Nil2 append_assoc append_self_conv prefix_def)
+ − 1402
by (metis L.simps(6) PMatch.intros(6) PMatch1(2) append_Nil2 append_eq_conv_conj prefix_def)
+ − 1403
+ − 1404
lemma PMatch_PMatchX:
+ − 1405
assumes "s \<in> r \<rightarrow> v"
+ − 1406
shows "\<turnstile> s \<in> r \<rightarrow> v"
+ − 1407
using assms
+ − 1408
apply(induct s r v arbitrary: s' rule: PMatch.induct)
+ − 1409
apply(auto intro: PMatchX.intros)
+ − 1410
apply(rule PMatchX.intros)
+ − 1411
apply(simp)
+ − 1412
apply(rule notI)
+ − 1413
apply(auto)[1]
+ − 1414
apply (metis PMatch1(2) append_eq_conv_conj length_sprefix less_imp_le_nat prefix_def sprefix_def take_all)
+ − 1415
apply(rule PMatchX.intros)
+ − 1416
apply(simp)
+ − 1417
apply(simp)
+ − 1418
apply(auto)[1]
+ − 1419
oops
+ − 1420
+ − 1421
lemma
+ − 1422
assumes "\<rhd> v : r"
+ − 1423
shows "(flat v) \<in> r \<rightarrow> v"
+ − 1424
using assms
+ − 1425
apply(induct)
+ − 1426
apply(auto intro: PMatch.intros)
+ − 1427
apply(rule PMatch.intros)
+ − 1428
apply(simp)
+ − 1429
apply(simp)
+ − 1430
apply(simp)
+ − 1431
apply(auto)[1]
+ − 1432
done
+ − 1433
+ − 1434
lemma
+ − 1435
assumes "s \<in> r \<rightarrow> v"
+ − 1436
shows "\<rhd> v : r"
+ − 1437
using assms
+ − 1438
apply(induct)
+ − 1439
apply(auto intro: Roy.intros)
+ − 1440
apply (metis PMatch1(2) Roy.intros(4))
+ − 1441
apply (metis PMatch1(2) Roy.intros(5))
+ − 1442
by (metis L.simps(6) PMatch1(2) Roy.intros(6))
+ − 1443
+ − 1444
+ − 1445
lemma PMatch_mkeps:
+ − 1446
assumes "nullable r"
+ − 1447
shows "[] \<in> r \<rightarrow> mkeps r"
+ − 1448
using assms
+ − 1449
apply(induct r)
+ − 1450
apply(auto)
+ − 1451
apply (metis PMatch.intros(1))
+ − 1452
apply(subst append.simps(1)[symmetric])
+ − 1453
apply (rule PMatch.intros)
+ − 1454
apply(simp)
+ − 1455
apply(simp)
+ − 1456
apply(auto)[1]
+ − 1457
apply (rule PMatch.intros)
+ − 1458
apply(simp)
+ − 1459
apply (rule PMatch.intros)
+ − 1460
apply(simp)
+ − 1461
apply (rule PMatch.intros)
+ − 1462
apply(simp)
+ − 1463
apply (metis nullable_correctness)
+ − 1464
apply(metis PMatch.intros(7))
+ − 1465
done
+ − 1466
+ − 1467
+ − 1468
lemma PMatch1N:
+ − 1469
assumes "s \<in> r \<rightarrow> v"
+ − 1470
shows "\<Turnstile> v : r"
+ − 1471
using assms
+ − 1472
apply(induct s r v rule: PMatch.induct)
+ − 1473
apply(auto)
+ − 1474
apply (metis NPrf.intros(4))
+ − 1475
apply (metis NPrf.intros(5))
+ − 1476
apply (metis NPrf.intros(2))
+ − 1477
apply (metis NPrf.intros(3))
+ − 1478
apply (metis NPrf.intros(1))
+ − 1479
apply(rule NPrf.intros)
+ − 1480
apply(simp)
+ − 1481
apply(simp)
+ − 1482
apply(simp)
+ − 1483
apply(rule NPrf.intros)
+ − 1484
done
+ − 1485
+ − 1486
lemma PMatch_determ:
+ − 1487
shows "\<lbrakk>s \<in> r \<rightarrow> v1; s \<in> r \<rightarrow> v2\<rbrakk> \<Longrightarrow> v1 = v2"
+ − 1488
and "\<lbrakk>s \<in> (STAR r) \<rightarrow> Stars vs1; s \<in> (STAR r) \<rightarrow> Stars vs2\<rbrakk> \<Longrightarrow> vs1 = vs2"
+ − 1489
apply(induct v1 and vs1 arbitrary: s r v2 and s r vs2 rule: val.inducts)
+ − 1490
apply(erule PMatch.cases)
+ − 1491
apply(simp_all)[7]
+ − 1492
apply(erule PMatch.cases)
+ − 1493
apply(simp_all)[7]
+ − 1494
apply(erule PMatch.cases)
+ − 1495
apply(simp_all)[7]
+ − 1496
apply(erule PMatch.cases)
+ − 1497
apply(simp_all)[7]
+ − 1498
apply(erule PMatch.cases)
+ − 1499
apply(simp_all)[7]
+ − 1500
apply(erule PMatch.cases)
+ − 1501
apply(simp_all)[7]
+ − 1502
apply(clarify)
+ − 1503
apply(subgoal_tac "s1 = s1a \<and> s2 = s2a")
+ − 1504
apply metis
+ − 1505
apply(rule conjI)
+ − 1506
apply(simp add: append_eq_append_conv2)
+ − 1507
apply(auto)[1]
+ − 1508
apply (metis PMatch1(1) PMatch1(2) Prf_flat_L)
+ − 1509
apply (metis PMatch1(1) PMatch1(2) Prf_flat_L)
+ − 1510
apply(simp add: append_eq_append_conv2)
+ − 1511
apply(auto)[1]
+ − 1512
apply (metis PMatch1(1) PMatch1(2) Prf_flat_L)
+ − 1513
apply (metis PMatch1(1) PMatch1(2) Prf_flat_L)
+ − 1514
apply(erule PMatch.cases)
+ − 1515
apply(simp_all)[7]
+ − 1516
apply(clarify)
+ − 1517
apply(erule PMatch.cases)
+ − 1518
apply(simp_all)[7]
+ − 1519
apply(clarify)
+ − 1520
apply (metis NPrf_flat_L PMatch1(2) PMatch1N)
+ − 1521
apply(erule PMatch.cases)
+ − 1522
apply(simp_all)[7]
+ − 1523
apply(clarify)
+ − 1524
apply(erule PMatch.cases)
+ − 1525
apply(simp_all)[7]
+ − 1526
apply(clarify)
+ − 1527
apply (metis NPrf_flat_L PMatch1(2) PMatch1N)
+ − 1528
(* star case *)
+ − 1529
defer
+ − 1530
apply(erule PMatch.cases)
+ − 1531
apply(simp_all)[7]
+ − 1532
apply(clarify)
+ − 1533
apply(erule PMatch.cases)
+ − 1534
apply(simp_all)[7]
+ − 1535
apply(clarify)
+ − 1536
apply (metis PMatch1(2))
+ − 1537
apply(rotate_tac 3)
+ − 1538
apply(erule PMatch.cases)
+ − 1539
apply(simp_all)[7]
+ − 1540
apply(clarify)
+ − 1541
apply(erule PMatch.cases)
+ − 1542
apply(simp_all)[7]
+ − 1543
apply(clarify)
+ − 1544
apply(subgoal_tac "s1 = s1a \<and> s2 = s2a")
+ − 1545
apply metis
+ − 1546
apply(simp add: append_eq_append_conv2)
+ − 1547
apply(auto)[1]
+ − 1548
apply (metis L.simps(6) PMatch1(1) PMatch1(2) Prf_flat_L)
+ − 1549
apply (metis L.simps(6) PMatch1(1) PMatch1(2) Prf_flat_L)
+ − 1550
apply (metis L.simps(6) PMatch1(1) PMatch1(2) Prf_flat_L)
+ − 1551
apply (metis L.simps(6) PMatch1(1) PMatch1(2) Prf_flat_L)
+ − 1552
apply(erule PMatch.cases)
+ − 1553
apply(simp_all)[7]
+ − 1554
apply(clarify)
+ − 1555
apply (metis PMatch1(2))
+ − 1556
apply(erule PMatch.cases)
+ − 1557
apply(simp_all)[7]
+ − 1558
apply(clarify)
+ − 1559
apply(erule PMatch.cases)
+ − 1560
apply(simp_all)[7]
+ − 1561
apply(clarify)
+ − 1562
apply(subgoal_tac "s1 = s1a \<and> s2 = s2a")
+ − 1563
apply(drule_tac x="s1 @ s2" in meta_spec)
+ − 1564
apply(drule_tac x="rb" in meta_spec)
+ − 1565
apply(drule_tac x="(va#vsa)" in meta_spec)
+ − 1566
apply(simp)
+ − 1567
apply(drule meta_mp)
+ − 1568
apply (metis L.simps(6) PMatch.intros(6))
+ − 1569
apply (metis L.simps(6) PMatch.intros(6))
+ − 1570
apply(simp add: append_eq_append_conv2)
+ − 1571
apply(auto)[1]
+ − 1572
apply (metis L.simps(6) NPrf_flat_L PMatch1(2) PMatch1N)
+ − 1573
apply (metis L.simps(6) NPrf_flat_L PMatch1(2) PMatch1N)
+ − 1574
apply (metis L.simps(6) NPrf_flat_L PMatch1(2) PMatch1N)
+ − 1575
apply (metis L.simps(6) NPrf_flat_L PMatch1(2) PMatch1N)
+ − 1576
apply (metis PMatch1(2))
+ − 1577
apply(erule PMatch.cases)
+ − 1578
apply(simp_all)[7]
+ − 1579
apply(clarify)
+ − 1580
by (metis PMatch1(2))
+ − 1581
+ − 1582
+ − 1583
lemma PMatch_Values:
+ − 1584
assumes "s \<in> r \<rightarrow> v"
+ − 1585
shows "v \<in> Values r s"
+ − 1586
using assms
+ − 1587
apply(simp add: Values_def PMatch1)
+ − 1588
by (metis append_Nil2 prefix_def)
+ − 1589
+ − 1590
lemma PMatch2:
+ − 1591
assumes "s \<in> (der c r) \<rightarrow> v"
+ − 1592
shows "(c#s) \<in> r \<rightarrow> (injval r c v)"
+ − 1593
using assms
+ − 1594
apply(induct c r arbitrary: s v rule: der.induct)
+ − 1595
apply(auto)
+ − 1596
apply(erule PMatch.cases)
+ − 1597
apply(simp_all)[7]
+ − 1598
apply(erule PMatch.cases)
+ − 1599
apply(simp_all)[7]
+ − 1600
apply(case_tac "c = c'")
+ − 1601
apply(simp)
+ − 1602
apply(erule PMatch.cases)
+ − 1603
apply(simp_all)[7]
+ − 1604
apply (metis PMatch.intros(2))
+ − 1605
apply(simp)
+ − 1606
apply(erule PMatch.cases)
+ − 1607
apply(simp_all)[7]
+ − 1608
apply(erule PMatch.cases)
+ − 1609
apply(simp_all)[7]
+ − 1610
apply (metis PMatch.intros(3))
+ − 1611
apply(clarify)
+ − 1612
apply(rule PMatch.intros)
+ − 1613
apply metis
+ − 1614
apply(simp add: L_flat_NPrf)
+ − 1615
apply(auto)[1]
+ − 1616
apply(frule_tac c="c" in v3_proj)
+ − 1617
apply metis
+ − 1618
apply(drule_tac x="projval r1 c v" in spec)
+ − 1619
apply(drule mp)
+ − 1620
apply (metis v4_proj2)
+ − 1621
apply (metis NPrf_imp_Prf)
+ − 1622
(* SEQ case *)
+ − 1623
apply(case_tac "nullable r1")
+ − 1624
apply(simp)
+ − 1625
prefer 2
+ − 1626
apply(simp)
+ − 1627
apply(erule PMatch.cases)
+ − 1628
apply(simp_all)[7]
+ − 1629
apply(clarify)
+ − 1630
apply(subst append.simps(2)[symmetric])
+ − 1631
apply(rule PMatch.intros)
+ − 1632
apply metis
+ − 1633
apply metis
+ − 1634
apply(auto)[1]
+ − 1635
apply(simp add: der_correctness Der_def)
+ − 1636
apply(auto)[1]
+ − 1637
(* nullable case *)
+ − 1638
apply(erule PMatch.cases)
+ − 1639
apply(simp_all)[7]
+ − 1640
apply(clarify)
+ − 1641
apply(erule PMatch.cases)
+ − 1642
apply(simp_all)[4]
+ − 1643
apply(clarify)
+ − 1644
apply(simp (no_asm))
+ − 1645
apply(subst append.simps(2)[symmetric])
+ − 1646
apply(rule PMatch.intros)
+ − 1647
apply metis
+ − 1648
apply metis
+ − 1649
apply(erule contrapos_nn)
+ − 1650
apply(erule exE)+
+ − 1651
apply(auto)[1]
+ − 1652
apply(simp add: L_flat_NPrf)
+ − 1653
apply(auto)[1]
+ − 1654
thm v3_proj
+ − 1655
apply(frule_tac c="c" in v3_proj)
+ − 1656
apply metis
+ − 1657
apply(rule_tac x="s\<^sub>3" in exI)
+ − 1658
apply(simp)
+ − 1659
apply (metis NPrf_imp_Prf v4_proj2)
+ − 1660
apply(simp)
+ − 1661
(* interesting case *)
+ − 1662
apply(clarify)
+ − 1663
apply(clarify)
+ − 1664
apply(simp)
+ − 1665
apply(subst (asm) L.simps(4)[symmetric])
+ − 1666
apply(simp only: L_flat_Prf)
+ − 1667
apply(simp)
+ − 1668
apply(subst append.simps(1)[symmetric])
+ − 1669
apply(rule PMatch.intros)
+ − 1670
apply (metis PMatch_mkeps)
+ − 1671
apply metis
+ − 1672
apply(auto)
+ − 1673
apply(simp only: L_flat_NPrf)
+ − 1674
apply(simp)
+ − 1675
apply(auto)
+ − 1676
apply(drule_tac x="Seq (projval r1 c v) vb" in spec)
+ − 1677
apply(drule mp)
+ − 1678
apply(simp)
+ − 1679
+ − 1680
apply (metis append_Cons butlast_snoc list.sel(1) neq_Nil_conv rotate1.simps(2) v4_proj2)
+ − 1681
apply(subgoal_tac "\<turnstile> projval r1 c v : der c r1")
+ − 1682
apply (metis NPrf_imp_Prf Prf.intros(1))
+ − 1683
apply(rule NPrf_imp_Prf)
+ − 1684
apply(rule v3_proj)
+ − 1685
apply(simp)
+ − 1686
apply (metis Cons_eq_append_conv)
+ − 1687
(* Stars case *)
+ − 1688
apply(erule PMatch.cases)
+ − 1689
apply(simp_all)[7]
+ − 1690
apply(clarify)
+ − 1691
apply(rotate_tac 2)
+ − 1692
apply(frule_tac PMatch1)
+ − 1693
apply(erule PMatch.cases)
+ − 1694
apply(simp_all)[7]
+ − 1695
apply(subst append.simps(2)[symmetric])
+ − 1696
apply(rule PMatch.intros)
+ − 1697
apply metis
+ − 1698
apply(auto)[1]
+ − 1699
apply(rule PMatch.intros)
+ − 1700
apply(simp)
+ − 1701
apply(simp)
+ − 1702
apply(simp)
+ − 1703
apply (metis L.simps(6))
+ − 1704
apply(subst v4)
+ − 1705
apply (metis NPrf_imp_Prf PMatch1N)
+ − 1706
apply(simp)
+ − 1707
apply(auto)[1]
+ − 1708
apply(drule_tac x="s\<^sub>3" in spec)
+ − 1709
apply(drule mp)
+ − 1710
defer
+ − 1711
apply metis
+ − 1712
apply(clarify)
+ − 1713
apply(drule_tac x="s1" in meta_spec)
+ − 1714
apply(drule_tac x="v1" in meta_spec)
+ − 1715
apply(simp)
+ − 1716
apply(rotate_tac 2)
+ − 1717
apply(drule PMatch.intros(6))
+ − 1718
apply(rule PMatch.intros(7))
+ − 1719
apply (metis PMatch1(1) list.distinct(1) v4)
+ − 1720
apply (metis Nil_is_append_conv)
+ − 1721
apply(simp)
+ − 1722
apply(subst der_correctness)
+ − 1723
apply(simp add: Der_def)
+ − 1724
done
+ − 1725
+ − 1726
+ − 1727
+ − 1728
lemma Sequ_single:
+ − 1729
"(A ;; {t}) = {s @ t | s . s \<in> A}"
+ − 1730
apply(simp add: Sequ_def)
+ − 1731
done
+ − 1732
+ − 1733
lemma Sequ_not:
+ − 1734
assumes "\<forall>t. s \<notin> (L(der c r1) ;; {t})" "L r1 \<noteq> {}"
+ − 1735
shows "\<forall>t. c # s \<notin> (L r1 ;; {t})"
+ − 1736
using assms
+ − 1737
apply(simp add: der_correctness)
+ − 1738
apply(simp add: Der_def)
+ − 1739
apply(simp add: Sequ_def)
+ − 1740
apply(rule allI)+
+ − 1741
apply(rule impI)
+ − 1742
apply(simp add: Cons_eq_append_conv)
+ − 1743
apply(auto)
+ − 1744
+ − 1745
oops
+ − 1746
+ − 1747
lemma PMatch_Roy2:
+ − 1748
assumes "2\<rhd> v : (der c r)" "\<exists>s. c # s \<in> L r"
+ − 1749
shows "2\<rhd> (injval r c v) : r"
+ − 1750
using assms
+ − 1751
apply(induct c r arbitrary: v rule: der.induct)
+ − 1752
apply(auto)
+ − 1753
apply(erule Roy2.cases)
+ − 1754
apply(simp_all)
+ − 1755
apply (metis Roy2.intros(2))
+ − 1756
(* alt case *)
+ − 1757
apply(erule Roy2.cases)
+ − 1758
apply(simp_all)
+ − 1759
apply(clarify)
+ − 1760
apply (metis Roy2.intros(3))
+ − 1761
apply(clarify)
+ − 1762
apply(rule Roy2.intros(4))
+ − 1763
apply (metis (full_types) Prf_flat_L Roy2_props v3 v4)
+ − 1764
apply(subgoal_tac "\<forall>t. c # flat va \<notin> L r1 ;; {t}")
+ − 1765
prefer 2
+ − 1766
apply(simp add: der_correctness)
+ − 1767
apply(simp add: Der_def)
+ − 1768
apply(simp add: Sequ_def)
+ − 1769
apply(rule allI)+
+ − 1770
apply(rule impI)
+ − 1771
apply(simp add: Cons_eq_append_conv)
+ − 1772
apply(erule disjE)
+ − 1773
apply(erule conjE)
+ − 1774
prefer 2
+ − 1775
apply metis
+ − 1776
apply(simp)
+ − 1777
apply(drule_tac x="[]" in spec)
+ − 1778
apply(drule_tac x="drop 1 t" in spec)
+ − 1779
apply(clarify)
+ − 1780
apply(simp)
+ − 1781
oops
+ − 1782
+ − 1783
lemma lex_correct1:
+ − 1784
assumes "s \<notin> L r"
+ − 1785
shows "lex r s = None"
+ − 1786
using assms
+ − 1787
apply(induct s arbitrary: r)
+ − 1788
apply(simp)
+ − 1789
apply (metis nullable_correctness)
+ − 1790
apply(auto)
+ − 1791
apply(drule_tac x="der a r" in meta_spec)
+ − 1792
apply(drule meta_mp)
+ − 1793
apply(auto)
+ − 1794
apply(simp add: L_flat_Prf)
+ − 1795
by (metis v3 v4)
+ − 1796
+ − 1797
+ − 1798
lemma lex_correct2:
+ − 1799
assumes "s \<in> L r"
+ − 1800
shows "\<exists>v. lex r s = Some(v) \<and> \<turnstile> v : r \<and> flat v = s"
+ − 1801
using assms
+ − 1802
apply(induct s arbitrary: r)
+ − 1803
apply(simp)
+ − 1804
apply (metis mkeps_flat mkeps_nullable nullable_correctness)
+ − 1805
apply(drule_tac x="der a r" in meta_spec)
+ − 1806
apply(drule meta_mp)
+ − 1807
apply(simp add: L_flat_NPrf)
+ − 1808
apply(auto)
+ − 1809
apply (metis v3_proj v4_proj2)
+ − 1810
apply (metis v3)
+ − 1811
apply(rule v4)
+ − 1812
by metis
+ − 1813
+ − 1814
lemma lex_correct3:
+ − 1815
assumes "s \<in> L r"
+ − 1816
shows "\<exists>v. lex r s = Some(v) \<and> s \<in> r \<rightarrow> v"
+ − 1817
using assms
+ − 1818
apply(induct s arbitrary: r)
+ − 1819
apply(simp)
+ − 1820
apply (metis PMatch_mkeps nullable_correctness)
+ − 1821
apply(drule_tac x="der a r" in meta_spec)
+ − 1822
apply(drule meta_mp)
+ − 1823
apply(simp add: L_flat_NPrf)
+ − 1824
apply(auto)
+ − 1825
apply (metis v3_proj v4_proj2)
+ − 1826
apply(rule PMatch2)
+ − 1827
apply(simp)
+ − 1828
done
+ − 1829
+ − 1830
lemma lex_correct4:
+ − 1831
assumes "s \<in> L r"
+ − 1832
shows "\<exists>v. lex r s = Some(v) \<and> \<Turnstile> v : r \<and> flat v = s"
+ − 1833
using lex_correct3[OF assms]
+ − 1834
apply(auto)
+ − 1835
apply (metis PMatch1N)
+ − 1836
by (metis PMatch1(2))
+ − 1837
+ − 1838
+ − 1839
lemma lex_correct5:
+ − 1840
assumes "s \<in> L r"
+ − 1841
shows "s \<in> r \<rightarrow> (lex2 r s)"
+ − 1842
using assms
+ − 1843
apply(induct s arbitrary: r)
+ − 1844
apply(simp)
+ − 1845
apply (metis PMatch_mkeps nullable_correctness)
+ − 1846
apply(simp)
+ − 1847
apply(rule PMatch2)
+ − 1848
apply(drule_tac x="der a r" in meta_spec)
+ − 1849
apply(drule meta_mp)
+ − 1850
apply(simp add: L_flat_NPrf)
+ − 1851
apply(auto)
+ − 1852
apply (metis v3_proj v4_proj2)
+ − 1853
done
+ − 1854
+ − 1855
lemma
+ − 1856
"lex2 (ALT (CHAR a) (ALT (CHAR b) (SEQ (CHAR a) (CHAR b)))) [a,b] = Right (Right (Seq (Char a) (Char b)))"
+ − 1857
apply(simp)
+ − 1858
done
+ − 1859
+ − 1860
+ − 1861
(* NOT DONE YET *)
+ − 1862
+ − 1863
section {* Sulzmann's Ordering of values *}
+ − 1864
+ − 1865
inductive ValOrd :: "val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<succ>_ _" [100, 100, 100] 100)
+ − 1866
where
+ − 1867
"v2 \<succ>r2 v2' \<Longrightarrow> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1 v2')"
+ − 1868
| "\<lbrakk>v1 \<succ>r1 v1'; v1 \<noteq> v1'\<rbrakk> \<Longrightarrow> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1' v2')"
+ − 1869
| "length (flat v1) \<ge> length (flat v2) \<Longrightarrow> (Left v1) \<succ>(ALT r1 r2) (Right v2)"
+ − 1870
| "length (flat v2) > length (flat v1) \<Longrightarrow> (Right v2) \<succ>(ALT r1 r2) (Left v1)"
+ − 1871
| "v2 \<succ>r2 v2' \<Longrightarrow> (Right v2) \<succ>(ALT r1 r2) (Right v2')"
+ − 1872
| "v1 \<succ>r1 v1' \<Longrightarrow> (Left v1) \<succ>(ALT r1 r2) (Left v1')"
+ − 1873
| "Void \<succ>EMPTY Void"
+ − 1874
| "(Char c) \<succ>(CHAR c) (Char c)"
+ − 1875
| "flat (Stars (v # vs)) = [] \<Longrightarrow> (Stars []) \<succ>(STAR r) (Stars (v # vs))"
+ − 1876
| "flat (Stars (v # vs)) \<noteq> [] \<Longrightarrow> (Stars (v # vs)) \<succ>(STAR r) (Stars [])"
+ − 1877
| "\<lbrakk>v1 \<succ>r v2; v1 \<noteq> v2\<rbrakk> \<Longrightarrow> (Stars (v1 # vs1)) \<succ>(STAR r) (Stars (v2 # vs2))"
+ − 1878
| "(Stars vs1) \<succ>(STAR r) (Stars vs2) \<Longrightarrow> (Stars (v # vs1)) \<succ>(STAR r) (Stars (v # vs2))"
+ − 1879
| "(Stars []) \<succ>(STAR r) (Stars [])"
+ − 1880
+ − 1881
lemma PMatch_ValOrd:
+ − 1882
assumes "s \<in> r \<rightarrow> v" "v' \<in> SValues r s"
+ − 1883
shows "v \<succ>r v'"
+ − 1884
using assms
+ − 1885
apply(induct r arbitrary: v v' s rule: rexp.induct)
+ − 1886
apply(simp add: SValues_recs)
+ − 1887
apply(simp add: SValues_recs)
+ − 1888
apply(erule PMatch.cases)
+ − 1889
apply(simp_all)[7]
+ − 1890
apply (metis ValOrd.intros(7))
+ − 1891
apply(simp add: SValues_recs)
+ − 1892
apply(erule PMatch.cases)
+ − 1893
apply(simp_all)[7]
+ − 1894
apply (metis ValOrd.intros(8) empty_iff singletonD)
+ − 1895
apply(simp add: SValues_recs)
+ − 1896
apply(clarify)
+ − 1897
apply(erule PMatch.cases)
+ − 1898
apply(simp_all)[7]
+ − 1899
apply(clarify)
+ − 1900
apply(case_tac "v1a = v1")
+ − 1901
apply(simp)
+ − 1902
apply(rule ValOrd.intros)
+ − 1903
apply(rotate_tac 1)
+ − 1904
apply(drule_tac x="v2a" in meta_spec)
+ − 1905
apply(rotate_tac 8)
+ − 1906
apply(drule_tac x="v2" in meta_spec)
+ − 1907
apply(drule_tac x="s2a" in meta_spec)
+ − 1908
apply(simp)
+ − 1909
apply(drule_tac meta_mp)
+ − 1910
apply(simp add: SValues_def)
+ − 1911
apply (metis PMatch1(2) same_append_eq)
+ − 1912
apply(simp)
+ − 1913
apply(rule ValOrd.intros)
+ − 1914
apply(drule_tac x="v1a" in meta_spec)
+ − 1915
apply(rotate_tac 8)
+ − 1916
apply(drule_tac x="v1" in meta_spec)
+ − 1917
apply(drule_tac x="s1a" in meta_spec)
+ − 1918
apply(simp)
+ − 1919
apply(drule_tac meta_mp)
+ − 1920
apply(simp add: append_eq_append_conv2)
+ − 1921
apply(auto)[1]
+ − 1922
apply(case_tac "us=[]")
+ − 1923
apply(simp)
+ − 1924
apply(drule_tac x="us" in spec)
+ − 1925
apply(drule mp)
+ − 1926
apply(simp add: SValues_def)
+ − 1927
apply (metis Prf_flat_L)
+ − 1928
apply(erule disjE)
+ − 1929
apply(simp)
+ − 1930
apply(simp)
+ − 1931
apply(simp add: SValues_def)
+ − 1932
apply (metis Prf_flat_L)
+ − 1933
+ − 1934
apply(subst (asm) (2) Values_def)
+ − 1935
apply(simp)
+ − 1936
apply(clarify)
+ − 1937
apply(simp add: rest_def)
+ − 1938
apply(simp add: prefix_def)
+ − 1939
apply(auto)[1]
+ − 1940
apply(simp add: append_eq_append_conv2)
+ − 1941
apply(auto)[1]
+ − 1942
apply(case_tac "us = []")
+ − 1943
apply(simp)
+ − 1944
apply(simp add: Values_def)
+ − 1945
apply (metis append_Nil2 prefix_def)
+ − 1946
apply(drule_tac x="us" in spec)
+ − 1947
apply(simp)
+ − 1948
apply(drule_tac mp)
+ − 1949
+ − 1950
+ − 1951
oops
+ − 1952
(*HERE *)
+ − 1953
+ − 1954
inductive ValOrd2 :: "val \<Rightarrow> string \<Rightarrow> val \<Rightarrow> bool" ("_ 2\<succ>_ _" [100, 100, 100] 100)
+ − 1955
where
+ − 1956
"v2 2\<succ>s v2' \<Longrightarrow> (Seq v1 v2) 2\<succ>(flat v1 @ s) (Seq v1 v2')"
+ − 1957
| "\<lbrakk>v1 2\<succ>s v1'; v1 \<noteq> v1'\<rbrakk> \<Longrightarrow> (Seq v1 v2) 2\<succ>s (Seq v1' v2')"
+ − 1958
| "(flat v2) \<sqsubseteq> (flat v1) \<Longrightarrow> (Left v1) 2\<succ>(flat v1) (Right v2)"
+ − 1959
| "(flat v1) \<sqsubset> (flat v2) \<Longrightarrow> (Right v2) 2\<succ>(flat v2) (Left v1)"
+ − 1960
| "v2 2\<succ>s v2' \<Longrightarrow> (Right v2) 2\<succ>s (Right v2')"
+ − 1961
| "v1 2\<succ>s v1' \<Longrightarrow> (Left v1) 2\<succ>s (Left v1')"
+ − 1962
| "Void 2\<succ>[] Void"
+ − 1963
| "(Char c) 2\<succ>[c] (Char c)"
+ − 1964
| "flat (Stars (v # vs)) = [] \<Longrightarrow> (Stars []) 2\<succ>[] (Stars (v # vs))"
+ − 1965
| "flat (Stars (v # vs)) \<noteq> [] \<Longrightarrow> (Stars (v # vs)) 2\<succ>(flat (Stars (v # vs))) (Stars [])"
+ − 1966
| "\<lbrakk>v1 2\<succ>s v2; v1 \<noteq> v2\<rbrakk> \<Longrightarrow> (Stars (v1 # vs1)) 2\<succ>s (Stars (v2 # vs2))"
+ − 1967
| "(Stars vs1) 2\<succ>s (Stars vs2) \<Longrightarrow> (Stars (v # vs1)) 2\<succ>(flat v @ s) (Stars (v # vs2))"
+ − 1968
| "(Stars []) 2\<succ>[] (Stars [])"
+ − 1969
+ − 1970
lemma ValOrd2_string1:
+ − 1971
assumes "v1 2\<succ>s v2"
+ − 1972
shows "s \<sqsubseteq> flat v1"
+ − 1973
using assms
+ − 1974
apply(induct)
+ − 1975
apply(auto simp add: prefix_def)
+ − 1976
apply (metis append_assoc)
+ − 1977
by (metis append_assoc)
+ − 1978
+ − 1979
+ − 1980
lemma admissibility:
+ − 1981
assumes "s \<in> r \<rightarrow> v" "\<turnstile> v' : r"
+ − 1982
shows "(\<forall>s'. (s' \<in> L(r) \<and> s' \<sqsubseteq> s) \<longrightarrow> v 2\<succ>s' v')"
+ − 1983
using assms
+ − 1984
apply(induct arbitrary: v')
+ − 1985
apply(erule Prf.cases)
+ − 1986
apply(simp_all)[7]
+ − 1987
apply (metis ValOrd2.intros(7))
+ − 1988
apply(erule Prf.cases)
+ − 1989
apply(simp_all)[7]
+ − 1990
apply (metis ValOrd2.intros(8) append_Nil2 prefix_Cons prefix_append prefix_def)
+ − 1991
apply(erule Prf.cases)
+ − 1992
apply(simp_all)[7]
+ − 1993
apply(auto)[1]
+ − 1994
apply (metis ValOrd2.intros(6))
+ − 1995
apply(rule ValOrd2.intros)
+ − 1996
apply(drule_tac x="v1" in meta_spec)
+ − 1997
apply(simp)
+ − 1998
+ − 1999
apply(clarify)
+ − 2000
apply (metis PMatch1(2) ValOrd2.intros(3))
+ − 2001
apply(erule Prf.cases)
+ − 2002
apply(simp_all)[7]
+ − 2003
apply(auto)
+ − 2004
+ − 2005
apply(case_tac "v1 = v1a")
+ − 2006
apply(simp)
+ − 2007
apply(rotate_tac 3)
+ − 2008
apply(drule_tac x="v2a" in meta_spec)
+ − 2009
apply(drule meta_mp)
+ − 2010
apply(simp)
+ − 2011
apply(auto)
+ − 2012
apply(rule_tac x="flat v1a @ s'" in exI)
+ − 2013
apply (metis PMatch1(2) ValOrd2.intros(1) prefix_append)
+ − 2014
apply (metis PMatch1(2) ValOrd2.intros(2) ValOrd2_string1 flat.simps(5))
+ − 2015
prefer 4
+ − 2016
apply(erule Prf.cases)
+ − 2017
apply(simp_all)[7]
+ − 2018
prefer 2
+ − 2019
apply (metis ValOrd2.intros(5))
+ − 2020
+ − 2021
+ − 2022
apply (metis ValOrd.intros(6))
+ − 2023
oops
+ − 2024
+ − 2025
+ − 2026
lemma admissibility:
+ − 2027
assumes "\<turnstile> s \<in> r \<rightarrow> v" "\<turnstile> v' : r"
+ − 2028
shows "v \<succ>r v'"
+ − 2029
using assms
+ − 2030
apply(induct arbitrary: v')
+ − 2031
apply(erule Prf.cases)
+ − 2032
apply(simp_all)[7]
+ − 2033
apply (metis ValOrd.intros(7))
+ − 2034
apply(erule Prf.cases)
+ − 2035
apply(simp_all)[7]
+ − 2036
apply (metis ValOrd.intros(8))
+ − 2037
apply(erule Prf.cases)
+ − 2038
apply(simp_all)[7]
+ − 2039
apply (metis ValOrd.intros(6))
+ − 2040
oops
+ − 2041
+ − 2042
lemma admissibility:
+ − 2043
assumes "2\<rhd> v : r" "\<turnstile> v' : r" "flat v' \<sqsubseteq> flat v"
+ − 2044
shows "v \<succ>r v'"
+ − 2045
using assms
+ − 2046
apply(induct arbitrary: v')
+ − 2047
apply(erule Prf.cases)
+ − 2048
apply(simp_all)[7]
+ − 2049
apply (metis ValOrd.intros(7))
+ − 2050
apply(erule Prf.cases)
+ − 2051
apply(simp_all)[7]
+ − 2052
apply (metis ValOrd.intros(8))
+ − 2053
apply(erule Prf.cases)
+ − 2054
apply(simp_all)[7]
+ − 2055
apply (metis ValOrd.intros(6))
+ − 2056
apply (metis ValOrd.intros(3) length_sprefix less_imp_le_nat order_refl sprefix_def)
+ − 2057
apply(erule Prf.cases)
+ − 2058
apply(simp_all)[7]
+ − 2059
apply (metis Prf_flat_L ValOrd.intros(4) length_sprefix seq_empty(1) sprefix_def)
+ − 2060
apply (metis ValOrd.intros(5))
+ − 2061
oops
+ − 2062
+ − 2063
+ − 2064
lemma admisibility:
+ − 2065
assumes "\<rhd> v : r" "\<turnstile> v' : r"
+ − 2066
shows "v \<succ>r v'"
+ − 2067
using assms
+ − 2068
apply(induct arbitrary: v')
+ − 2069
prefer 5
+ − 2070
apply(drule royA)
+ − 2071
apply(erule Prf.cases)
+ − 2072
apply(simp_all)[7]
+ − 2073
apply(clarify)
+ − 2074
apply(case_tac "v1 = v1a")
+ − 2075
apply(simp)
+ − 2076
apply(rule ValOrd.intros)
+ − 2077
apply metis
+ − 2078
apply (metis ValOrd.intros(2))
+ − 2079
apply(erule Prf.cases)
+ − 2080
apply(simp_all)[7]
+ − 2081
apply (metis ValOrd.intros(7))
+ − 2082
apply(erule Prf.cases)
+ − 2083
apply(simp_all)[7]
+ − 2084
apply (metis ValOrd.intros(8))
+ − 2085
apply(erule Prf.cases)
+ − 2086
apply(simp_all)[7]
+ − 2087
apply (metis ValOrd.intros(6))
+ − 2088
apply(rule ValOrd.intros)
+ − 2089
defer
+ − 2090
apply(erule Prf.cases)
+ − 2091
apply(simp_all)[7]
+ − 2092
apply(clarify)
+ − 2093
apply(rule ValOrd.intros)
+ − 2094
(* seq case goes through *)
+ − 2095
oops
+ − 2096
+ − 2097
+ − 2098
lemma admisibility:
+ − 2099
assumes "\<rhd> v : r" "\<turnstile> v' : r" "flat v' \<sqsubseteq> flat v"
+ − 2100
shows "v \<succ>r v'"
+ − 2101
using assms
+ − 2102
apply(induct arbitrary: v')
+ − 2103
prefer 5
+ − 2104
apply(drule royA)
+ − 2105
apply(erule Prf.cases)
+ − 2106
apply(simp_all)[7]
+ − 2107
apply(clarify)
+ − 2108
apply(case_tac "v1 = v1a")
+ − 2109
apply(simp)
+ − 2110
apply(rule ValOrd.intros)
+ − 2111
apply(subst (asm) (3) prefix_def)
+ − 2112
apply(erule exE)
+ − 2113
apply(simp)
+ − 2114
apply (metis prefix_def)
+ − 2115
(* the unequal case *)
+ − 2116
apply(subgoal_tac "flat v1 \<sqsubset> flat v1a \<or> flat v1a \<sqsubseteq> flat v1")
+ − 2117
prefer 2
+ − 2118
apply(simp add: prefix_def sprefix_def)
+ − 2119
apply (metis append_eq_append_conv2)
+ − 2120
apply(erule disjE)
+ − 2121
(* first case flat v1 \<sqsubset> flat v1a *)
+ − 2122
apply(subst (asm) sprefix_def)
+ − 2123
apply(subst (asm) (5) prefix_def)
+ − 2124
apply(clarify)
+ − 2125
apply(subgoal_tac "(s3 @ flat v2a) \<sqsubseteq> flat v2")
+ − 2126
prefer 2
+ − 2127
apply(simp)
+ − 2128
apply (metis append_assoc prefix_append)
+ − 2129
apply(subgoal_tac "s3 \<noteq> []")
+ − 2130
prefer 2
+ − 2131
apply (metis append_Nil2)
+ − 2132
(* HERE *)
+ − 2133
apply(subst (asm) (5) prefix_def)
+ − 2134
apply(erule exE)
+ − 2135
apply(simp add: ders_correctness Ders_def)
+ − 2136
apply(simp add: prefix_def)
+ − 2137
apply(clarify)
+ − 2138
apply(subst (asm) append_eq_append_conv2)
+ − 2139
apply(erule exE)
+ − 2140
apply(erule disjE)
+ − 2141
apply(clarify)
+ − 2142
oops
+ − 2143
+ − 2144
+ − 2145
+ − 2146
lemma ValOrd_refl:
+ − 2147
assumes "\<turnstile> v : r"
+ − 2148
shows "v \<succ>r v"
+ − 2149
using assms
+ − 2150
apply(induct)
+ − 2151
apply(auto intro: ValOrd.intros)
+ − 2152
done
+ − 2153
+ − 2154
lemma ValOrd_total:
+ − 2155
shows "\<lbrakk>\<turnstile> v1 : r; \<turnstile> v2 : r\<rbrakk> \<Longrightarrow> v1 \<succ>r v2 \<or> v2 \<succ>r v1"
+ − 2156
apply(induct r arbitrary: v1 v2)
+ − 2157
apply(auto)
+ − 2158
apply(erule Prf.cases)
+ − 2159
apply(simp_all)[7]
+ − 2160
apply(erule Prf.cases)
+ − 2161
apply(simp_all)[7]
+ − 2162
apply(erule Prf.cases)
+ − 2163
apply(simp_all)[7]
+ − 2164
apply (metis ValOrd.intros(7))
+ − 2165
apply(erule Prf.cases)
+ − 2166
apply(simp_all)[7]
+ − 2167
apply(erule Prf.cases)
+ − 2168
apply(simp_all)[7]
+ − 2169
apply (metis ValOrd.intros(8))
+ − 2170
apply(erule Prf.cases)
+ − 2171
apply(simp_all)[7]
+ − 2172
apply(erule Prf.cases)
+ − 2173
apply(simp_all)[7]
+ − 2174
apply(clarify)
+ − 2175
apply(case_tac "v1a = v1b")
+ − 2176
apply(simp)
+ − 2177
apply(rule ValOrd.intros(1))
+ − 2178
apply (metis ValOrd.intros(1))
+ − 2179
apply(rule ValOrd.intros(2))
+ − 2180
apply(auto)[2]
+ − 2181
apply(erule contrapos_np)
+ − 2182
apply(rule ValOrd.intros(2))
+ − 2183
apply(auto)
+ − 2184
apply(erule Prf.cases)
+ − 2185
apply(simp_all)[7]
+ − 2186
apply(erule Prf.cases)
+ − 2187
apply(simp_all)[7]
+ − 2188
apply(clarify)
+ − 2189
apply (metis ValOrd.intros(6))
+ − 2190
apply(rule ValOrd.intros)
+ − 2191
apply(erule contrapos_np)
+ − 2192
apply(rule ValOrd.intros)
+ − 2193
apply (metis le_eq_less_or_eq neq_iff)
+ − 2194
apply(erule Prf.cases)
+ − 2195
apply(simp_all)[7]
+ − 2196
apply(rule ValOrd.intros)
+ − 2197
apply(erule contrapos_np)
+ − 2198
apply(rule ValOrd.intros)
+ − 2199
apply (metis le_eq_less_or_eq neq_iff)
+ − 2200
apply(rule ValOrd.intros)
+ − 2201
apply(erule contrapos_np)
+ − 2202
apply(rule ValOrd.intros)
+ − 2203
apply(metis)
+ − 2204
apply(erule Prf.cases)
+ − 2205
apply(simp_all)[7]
+ − 2206
apply(erule Prf.cases)
+ − 2207
apply(simp_all)[7]
+ − 2208
apply(auto)
+ − 2209
apply (metis ValOrd.intros(13))
+ − 2210
apply (metis ValOrd.intros(10) ValOrd.intros(9))
+ − 2211
apply(erule Prf.cases)
+ − 2212
apply(simp_all)[7]
+ − 2213
apply(auto)
+ − 2214
apply (metis ValOrd.intros(10) ValOrd.intros(9))
+ − 2215
apply(case_tac "v = va")
+ − 2216
prefer 2
+ − 2217
apply (metis ValOrd.intros(11))
+ − 2218
apply(simp)
+ − 2219
apply(rule ValOrd.intros(12))
+ − 2220
apply(erule contrapos_np)
+ − 2221
apply(rule ValOrd.intros(12))
+ − 2222
oops
+ − 2223
+ − 2224
lemma Roy_posix:
+ − 2225
assumes "\<rhd> v : r" "\<turnstile> v' : r" "flat v' \<sqsubseteq> flat v"
+ − 2226
shows "v \<succ>r v'"
+ − 2227
using assms
+ − 2228
apply(induct r arbitrary: v v' rule: rexp.induct)
+ − 2229
apply(erule Prf.cases)
+ − 2230
apply(simp_all)[7]
+ − 2231
apply(erule Prf.cases)
+ − 2232
apply(simp_all)[7]
+ − 2233
apply(erule Roy.cases)
+ − 2234
apply(simp_all)
+ − 2235
apply (metis ValOrd.intros(7))
+ − 2236
apply(erule Prf.cases)
+ − 2237
apply(simp_all)[7]
+ − 2238
apply(erule Roy.cases)
+ − 2239
apply(simp_all)
+ − 2240
apply (metis ValOrd.intros(8))
+ − 2241
prefer 2
+ − 2242
apply(erule Prf.cases)
+ − 2243
apply(simp_all)[7]
+ − 2244
apply(erule Roy.cases)
+ − 2245
apply(simp_all)
+ − 2246
apply(clarify)
+ − 2247
apply (metis ValOrd.intros(6))
+ − 2248
apply(clarify)
+ − 2249
apply (metis Prf_flat_L ValOrd.intros(4) length_sprefix sprefix_def)
+ − 2250
apply(erule Roy.cases)
+ − 2251
apply(simp_all)
+ − 2252
apply (metis ValOrd.intros(3) length_sprefix less_imp_le_nat order_refl sprefix_def)
+ − 2253
apply(clarify)
+ − 2254
apply (metis ValOrd.intros(5))
+ − 2255
apply(erule Prf.cases)
+ − 2256
apply(simp_all)[7]
+ − 2257
apply(erule Roy.cases)
+ − 2258
apply(simp_all)
+ − 2259
apply(clarify)
+ − 2260
apply(case_tac "v1a = v1")
+ − 2261
apply(simp)
+ − 2262
apply(rule ValOrd.intros)
+ − 2263
apply (metis prefix_append)
+ − 2264
apply(rule ValOrd.intros)
+ − 2265
prefer 2
+ − 2266
apply(simp)
+ − 2267
apply(simp add: prefix_def)
+ − 2268
apply(auto)[1]
+ − 2269
apply(simp add: append_eq_append_conv2)
+ − 2270
apply(auto)[1]
+ − 2271
apply(drule_tac x="v1a" in meta_spec)
+ − 2272
apply(rotate_tac 9)
+ − 2273
apply(drule_tac x="v1" in meta_spec)
+ − 2274
apply(drule_tac meta_mp)
+ − 2275
apply(simp)
+ − 2276
apply(drule_tac meta_mp)
+ − 2277
apply(simp)
+ − 2278
apply(drule_tac meta_mp)
+ − 2279
apply(simp)
+ − 2280
apply(drule_tac x="us" in spec)
+ − 2281
apply(drule_tac mp)
+ − 2282
apply (metis Prf_flat_L)
+ − 2283
apply(auto)[1]
+ − 2284
oops
+ − 2285
+ − 2286
+ − 2287
lemma ValOrd_anti:
+ − 2288
shows "\<lbrakk>\<turnstile> v1 : r; \<turnstile> v2 : r; v1 \<succ>r v2; v2 \<succ>r v1\<rbrakk> \<Longrightarrow> v1 = v2"
+ − 2289
and "\<lbrakk>\<turnstile> Stars vs1 : r; \<turnstile> Stars vs2 : r; Stars vs1 \<succ>r Stars vs2; Stars vs2 \<succ>r Stars vs1\<rbrakk> \<Longrightarrow> vs1 = vs2"
+ − 2290
apply(induct v1 and vs1 arbitrary: r v2 and r vs2 rule: val.inducts)
+ − 2291
apply(erule Prf.cases)
+ − 2292
apply(simp_all)[7]
+ − 2293
apply(erule Prf.cases)
+ − 2294
apply(simp_all)[7]
+ − 2295
apply(erule Prf.cases)
+ − 2296
apply(simp_all)[7]
+ − 2297
apply(erule Prf.cases)
+ − 2298
apply(simp_all)[7]
+ − 2299
apply(erule Prf.cases)
+ − 2300
apply(simp_all)[7]
+ − 2301
apply(erule Prf.cases)
+ − 2302
apply(simp_all)[7]
+ − 2303
apply(erule ValOrd.cases)
+ − 2304
apply(simp_all)
+ − 2305
apply(erule ValOrd.cases)
+ − 2306
apply(simp_all)
+ − 2307
apply(erule ValOrd.cases)
+ − 2308
apply(simp_all)
+ − 2309
apply(erule Prf.cases)
+ − 2310
apply(simp_all)[7]
+ − 2311
apply(erule Prf.cases)
+ − 2312
apply(simp_all)[7]
+ − 2313
apply(erule ValOrd.cases)
+ − 2314
apply(simp_all)
+ − 2315
apply(erule ValOrd.cases)
+ − 2316
apply(simp_all)
+ − 2317
apply(erule ValOrd.cases)
+ − 2318
apply(simp_all)
+ − 2319
apply(erule ValOrd.cases)
+ − 2320
apply(simp_all)
+ − 2321
apply(erule Prf.cases)
+ − 2322
apply(simp_all)[7]
+ − 2323
apply(erule Prf.cases)
+ − 2324
apply(simp_all)[7]
+ − 2325
apply(erule ValOrd.cases)
+ − 2326
apply(simp_all)
+ − 2327
apply(erule ValOrd.cases)
+ − 2328
apply(simp_all)
+ − 2329
apply(erule ValOrd.cases)
+ − 2330
apply(simp_all)
+ − 2331
apply(erule ValOrd.cases)
+ − 2332
apply(simp_all)
+ − 2333
apply(erule Prf.cases)
+ − 2334
apply(simp_all)[7]
+ − 2335
apply(erule Prf.cases)
+ − 2336
apply(simp_all)[7]
+ − 2337
apply(erule ValOrd.cases)
+ − 2338
apply(simp_all)
+ − 2339
apply(erule ValOrd.cases)
+ − 2340
apply(simp_all)
+ − 2341
apply(erule Prf.cases)
+ − 2342
apply(simp_all)[7]
+ − 2343
apply(erule ValOrd.cases)
+ − 2344
apply(simp_all)
+ − 2345
apply(erule ValOrd.cases)
+ − 2346
apply(simp_all)
+ − 2347
apply(erule ValOrd.cases)
+ − 2348
apply(simp_all)
+ − 2349
apply(erule ValOrd.cases)
+ − 2350
apply(simp_all)
+ − 2351
apply(auto)[1]
+ − 2352
prefer 2
+ − 2353
oops
+ − 2354
+ − 2355
+ − 2356
(*
+ − 2357
+ − 2358
lemma ValOrd_PMatch:
+ − 2359
assumes "s \<in> r \<rightarrow> v1" "\<turnstile> v2 : r" "flat v2 \<sqsubseteq> s"
+ − 2360
shows "v1 \<succ>r v2"
+ − 2361
using assms
+ − 2362
apply(induct r arbitrary: s v1 v2 rule: rexp.induct)
+ − 2363
apply(erule Prf.cases)
+ − 2364
apply(simp_all)[7]
+ − 2365
apply(erule Prf.cases)
+ − 2366
apply(simp_all)[7]
+ − 2367
apply(erule PMatch.cases)
+ − 2368
apply(simp_all)[7]
+ − 2369
apply (metis ValOrd.intros(7))
+ − 2370
apply(erule Prf.cases)
+ − 2371
apply(simp_all)[7]
+ − 2372
apply(erule PMatch.cases)
+ − 2373
apply(simp_all)[7]
+ − 2374
apply (metis ValOrd.intros(8))
+ − 2375
defer
+ − 2376
apply(erule Prf.cases)
+ − 2377
apply(simp_all)[7]
+ − 2378
apply(erule PMatch.cases)
+ − 2379
apply(simp_all)[7]
+ − 2380
apply (metis ValOrd.intros(6))
+ − 2381
apply (metis PMatch1(2) Prf_flat_L ValOrd.intros(4) length_sprefix sprefix_def)
+ − 2382
apply(clarify)
+ − 2383
apply(erule PMatch.cases)
+ − 2384
apply(simp_all)[7]
+ − 2385
apply (metis PMatch1(2) ValOrd.intros(3) length_sprefix less_imp_le_nat order_refl sprefix_def)
+ − 2386
apply(clarify)
+ − 2387
apply (metis ValOrd.intros(5))
+ − 2388
(* Stars case *)
+ − 2389
apply(erule Prf.cases)
+ − 2390
apply(simp_all)[7]
+ − 2391
apply(erule PMatch.cases)
+ − 2392
apply(simp_all)
+ − 2393
apply (metis Nil_is_append_conv ValOrd.intros(10) flat.simps(7))
+ − 2394
apply (metis ValOrd.intros(13))
+ − 2395
apply(clarify)
+ − 2396
apply(erule PMatch.cases)
+ − 2397
apply(simp_all)
+ − 2398
prefer 2
+ − 2399
apply(rule ValOrd.intros)
+ − 2400
apply(simp add: prefix_def)
+ − 2401
apply(rule ValOrd.intros)
+ − 2402
apply(drule_tac x="s1" in meta_spec)
+ − 2403
apply(drule_tac x="va" in meta_spec)
+ − 2404
apply(drule_tac x="v" in meta_spec)
+ − 2405
apply(drule_tac meta_mp)
+ − 2406
apply(simp)
+ − 2407
apply(drule_tac meta_mp)
+ − 2408
apply(simp)
+ − 2409
apply(drule_tac meta_mp)
+ − 2410
apply(simp add: prefix_def)
+ − 2411
apply(auto)[1]
+ − 2412
prefer 3
+ − 2413
(* Seq case *)
+ − 2414
apply(erule Prf.cases)
+ − 2415
apply(simp_all)[5]
+ − 2416
apply(auto)
+ − 2417
apply(erule PMatch.cases)
+ − 2418
apply(simp_all)[5]
+ − 2419
apply(auto)
+ − 2420
apply(case_tac "v1b = v1a")
+ − 2421
apply(auto)
+ − 2422
apply(simp add: prefix_def)
+ − 2423
apply(auto)[1]
+ − 2424
apply (metis PMatch1(2) ValOrd.intros(1) same_append_eq)
+ − 2425
apply(simp add: prefix_def)
+ − 2426
apply(auto)[1]
+ − 2427
apply(simp add: append_eq_append_conv2)
+ − 2428
apply(auto)
+ − 2429
prefer 2
+ − 2430
apply (metis ValOrd.intros(2))
+ − 2431
prefer 2
+ − 2432
apply (metis ValOrd.intros(2))
+ − 2433
apply(case_tac "us = []")
+ − 2434
apply(simp)
+ − 2435
apply (metis ValOrd.intros(2) append_Nil2)
+ − 2436
apply(drule_tac x="us" in spec)
+ − 2437
apply(simp)
+ − 2438
apply(drule_tac mp)
+ − 2439
apply (metis Prf_flat_L)
+ − 2440
apply(drule_tac x="s1 @ us" in meta_spec)
+ − 2441
apply(drule_tac x="v1b" in meta_spec)
+ − 2442
apply(drule_tac x="v1a" in meta_spec)
+ − 2443
apply(drule_tac meta_mp)
+ − 2444
+ − 2445
apply(simp)
+ − 2446
apply(drule_tac meta_mp)
+ − 2447
apply(simp)
+ − 2448
apply(simp)
+ − 2449
apply(simp)
+ − 2450
apply(clarify)
+ − 2451
apply (metis ValOrd.intros(6))
+ − 2452
apply(clarify)
+ − 2453
apply (metis PMatch1(2) ValOrd.intros(3) length_sprefix less_imp_le_nat order_refl sprefix_def)
+ − 2454
apply(erule Prf.cases)
+ − 2455
apply(simp_all)[5]
+ − 2456
apply(clarify)
+ − 2457
apply (metis PMatch1(2) Prf_flat_L ValOrd.intros(4) length_sprefix sprefix_def)
+ − 2458
apply (metis ValOrd.intros(5))
+ − 2459
(* Seq case *)
+ − 2460
apply(erule Prf.cases)
+ − 2461
apply(simp_all)[5]
+ − 2462
apply(auto)
+ − 2463
apply(case_tac "v1 = v1a")
+ − 2464
apply(auto)
+ − 2465
apply(simp add: prefix_def)
+ − 2466
apply(auto)[1]
+ − 2467
apply (metis PMatch1(2) ValOrd.intros(1) same_append_eq)
+ − 2468
apply(simp add: prefix_def)
+ − 2469
apply(auto)[1]
+ − 2470
apply(frule PMatch1)
+ − 2471
apply(frule PMatch1(2)[symmetric])
+ − 2472
apply(clarify)
+ − 2473
apply(simp add: append_eq_append_conv2)
+ − 2474
apply(auto)
+ − 2475
prefer 2
+ − 2476
apply (metis ValOrd.intros(2))
+ − 2477
prefer 2
+ − 2478
apply (metis ValOrd.intros(2))
+ − 2479
apply(case_tac "us = []")
+ − 2480
apply(simp)
+ − 2481
apply (metis ValOrd.intros(2) append_Nil2)
+ − 2482
apply(drule_tac x="us" in spec)
+ − 2483
apply(simp)
+ − 2484
apply(drule mp)
+ − 2485
apply (metis Prf_flat_L)
+ − 2486
apply(drule_tac x="v1a" in meta_spec)
+ − 2487
apply(drule_tac meta_mp)
+ − 2488
apply(simp)
+ − 2489
apply(drule_tac meta_mp)
+ − 2490
apply(simp)
+ − 2491
+ − 2492
lemma ValOrd_PMatch:
+ − 2493
assumes "s \<in> r \<rightarrow> v1" "\<turnstile> v2 : r" "flat v2 \<sqsubseteq> s"
+ − 2494
shows "v1 \<succ>r v2"
+ − 2495
using assms
+ − 2496
apply(induct arbitrary: v2 rule: .induct)
+ − 2497
apply(erule Prf.cases)
+ − 2498
apply(simp_all)[5]
+ − 2499
apply (metis ValOrd.intros(7))
+ − 2500
apply(erule Prf.cases)
+ − 2501
apply(simp_all)[5]
+ − 2502
apply (metis ValOrd.intros(8))
+ − 2503
apply(erule Prf.cases)
+ − 2504
apply(simp_all)[5]
+ − 2505
apply(clarify)
+ − 2506
apply (metis ValOrd.intros(6))
+ − 2507
apply(clarify)
+ − 2508
apply (metis PMatch1(2) ValOrd.intros(3) length_sprefix less_imp_le_nat order_refl sprefix_def)
+ − 2509
apply(erule Prf.cases)
+ − 2510
apply(simp_all)[5]
+ − 2511
apply(clarify)
+ − 2512
apply (metis PMatch1(2) Prf_flat_L ValOrd.intros(4) length_sprefix sprefix_def)
+ − 2513
apply (metis ValOrd.intros(5))
+ − 2514
(* Seq case *)
+ − 2515
apply(erule Prf.cases)
+ − 2516
apply(simp_all)[5]
+ − 2517
apply(auto)
+ − 2518
apply(case_tac "v1 = v1a")
+ − 2519
apply(auto)
+ − 2520
apply(simp add: prefix_def)
+ − 2521
apply(auto)[1]
+ − 2522
apply (metis PMatch1(2) ValOrd.intros(1) same_append_eq)
+ − 2523
apply(simp add: prefix_def)
+ − 2524
apply(auto)[1]
+ − 2525
apply(frule PMatch1)
+ − 2526
apply(frule PMatch1(2)[symmetric])
+ − 2527
apply(clarify)
+ − 2528
apply(simp add: append_eq_append_conv2)
+ − 2529
apply(auto)
+ − 2530
prefer 2
+ − 2531
apply (metis ValOrd.intros(2))
+ − 2532
prefer 2
+ − 2533
apply (metis ValOrd.intros(2))
+ − 2534
apply(case_tac "us = []")
+ − 2535
apply(simp)
+ − 2536
apply (metis ValOrd.intros(2) append_Nil2)
+ − 2537
apply(drule_tac x="us" in spec)
+ − 2538
apply(simp)
+ − 2539
apply(drule mp)
+ − 2540
apply (metis Prf_flat_L)
+ − 2541
apply(drule_tac x="v1a" in meta_spec)
+ − 2542
apply(drule_tac meta_mp)
+ − 2543
apply(simp)
+ − 2544
apply(drule_tac meta_mp)
+ − 2545
apply(simp)
+ − 2546
+ − 2547
apply (metis PMatch1(2) ValOrd.intros(1) same_append_eq)
+ − 2548
apply(rule ValOrd.intros(2))
+ − 2549
apply(auto)
+ − 2550
apply(drule_tac x="v1a" in meta_spec)
+ − 2551
apply(drule_tac meta_mp)
+ − 2552
apply(simp)
+ − 2553
apply(drule_tac meta_mp)
+ − 2554
prefer 2
+ − 2555
apply(simp)
+ − 2556
thm append_eq_append_conv
+ − 2557
apply(simp add: append_eq_append_conv2)
+ − 2558
apply(auto)
+ − 2559
apply (metis Prf_flat_L)
+ − 2560
apply(case_tac "us = []")
+ − 2561
apply(simp)
+ − 2562
apply(drule_tac x="us" in spec)
+ − 2563
apply(drule mp)
+ − 2564
+ − 2565
+ − 2566
inductive ValOrd2 :: "val \<Rightarrow> val \<Rightarrow> bool" ("_ 2\<succ> _" [100, 100] 100)
+ − 2567
where
+ − 2568
"v2 2\<succ> v2' \<Longrightarrow> (Seq v1 v2) 2\<succ> (Seq v1 v2')"
+ − 2569
| "\<lbrakk>v1 2\<succ> v1'; v1 \<noteq> v1'\<rbrakk> \<Longrightarrow> (Seq v1 v2) 2\<succ> (Seq v1' v2')"
+ − 2570
| "length (flat v1) \<ge> length (flat v2) \<Longrightarrow> (Left v1) 2\<succ> (Right v2)"
+ − 2571
| "length (flat v2) > length (flat v1) \<Longrightarrow> (Right v2) 2\<succ> (Left v1)"
+ − 2572
| "v2 2\<succ> v2' \<Longrightarrow> (Right v2) 2\<succ> (Right v2')"
+ − 2573
| "v1 2\<succ> v1' \<Longrightarrow> (Left v1) 2\<succ> (Left v1')"
+ − 2574
| "Void 2\<succ> Void"
+ − 2575
| "(Char c) 2\<succ> (Char c)"
+ − 2576
+ − 2577
lemma Ord1:
+ − 2578
"v1 \<succ>r v2 \<Longrightarrow> v1 2\<succ> v2"
+ − 2579
apply(induct rule: ValOrd.induct)
+ − 2580
apply(auto intro: ValOrd2.intros)
+ − 2581
done
+ − 2582
+ − 2583
lemma Ord2:
+ − 2584
"v1 2\<succ> v2 \<Longrightarrow> \<exists>r. v1 \<succ>r v2"
+ − 2585
apply(induct v1 v2 rule: ValOrd2.induct)
+ − 2586
apply(auto intro: ValOrd.intros)
+ − 2587
done
+ − 2588
+ − 2589
lemma Ord3:
+ − 2590
"\<lbrakk>v1 2\<succ> v2; \<turnstile> v1 : r\<rbrakk> \<Longrightarrow> v1 \<succ>r v2"
+ − 2591
apply(induct v1 v2 arbitrary: r rule: ValOrd2.induct)
+ − 2592
apply(auto intro: ValOrd.intros elim: Prf.cases)
+ − 2593
done
+ − 2594
+ − 2595
section {* Posix definition *}
+ − 2596
+ − 2597
definition POSIX :: "val \<Rightarrow> rexp \<Rightarrow> bool"
+ − 2598
where
+ − 2599
"POSIX v r \<equiv> (\<turnstile> v : r \<and> (\<forall>v'. (\<turnstile> v' : r \<and> flat v' \<sqsubseteq> flat v) \<longrightarrow> v \<succ>r v'))"
+ − 2600
+ − 2601
lemma ValOrd_refl:
+ − 2602
assumes "\<turnstile> v : r"
+ − 2603
shows "v \<succ>r v"
+ − 2604
using assms
+ − 2605
apply(induct)
+ − 2606
apply(auto intro: ValOrd.intros)
+ − 2607
done
+ − 2608
+ − 2609
lemma ValOrd_total:
+ − 2610
shows "\<lbrakk>\<turnstile> v1 : r; \<turnstile> v2 : r\<rbrakk> \<Longrightarrow> v1 \<succ>r v2 \<or> v2 \<succ>r v1"
+ − 2611
apply(induct r arbitrary: v1 v2)
+ − 2612
apply(auto)
+ − 2613
apply(erule Prf.cases)
+ − 2614
apply(simp_all)[5]
+ − 2615
apply(erule Prf.cases)
+ − 2616
apply(simp_all)[5]
+ − 2617
apply(erule Prf.cases)
+ − 2618
apply(simp_all)[5]
+ − 2619
apply (metis ValOrd.intros(7))
+ − 2620
apply(erule Prf.cases)
+ − 2621
apply(simp_all)[5]
+ − 2622
apply(erule Prf.cases)
+ − 2623
apply(simp_all)[5]
+ − 2624
apply (metis ValOrd.intros(8))
+ − 2625
apply(erule Prf.cases)
+ − 2626
apply(simp_all)[5]
+ − 2627
apply(erule Prf.cases)
+ − 2628
apply(simp_all)[5]
+ − 2629
apply(clarify)
+ − 2630
apply(case_tac "v1a = v1b")
+ − 2631
apply(simp)
+ − 2632
apply(rule ValOrd.intros(1))
+ − 2633
apply (metis ValOrd.intros(1))
+ − 2634
apply(rule ValOrd.intros(2))
+ − 2635
apply(auto)[2]
+ − 2636
apply(erule contrapos_np)
+ − 2637
apply(rule ValOrd.intros(2))
+ − 2638
apply(auto)
+ − 2639
apply(erule Prf.cases)
+ − 2640
apply(simp_all)[5]
+ − 2641
apply(erule Prf.cases)
+ − 2642
apply(simp_all)[5]
+ − 2643
apply (metis Ord1 Ord3 Prf.intros(2) ValOrd2.intros(6))
+ − 2644
apply(rule ValOrd.intros)
+ − 2645
apply(erule contrapos_np)
+ − 2646
apply(rule ValOrd.intros)
+ − 2647
apply (metis le_eq_less_or_eq neq_iff)
+ − 2648
apply(erule Prf.cases)
+ − 2649
apply(simp_all)[5]
+ − 2650
apply(rule ValOrd.intros)
+ − 2651
apply(erule contrapos_np)
+ − 2652
apply(rule ValOrd.intros)
+ − 2653
apply (metis le_eq_less_or_eq neq_iff)
+ − 2654
apply(rule ValOrd.intros)
+ − 2655
apply(erule contrapos_np)
+ − 2656
apply(rule ValOrd.intros)
+ − 2657
by metis
+ − 2658
+ − 2659
lemma ValOrd_anti:
+ − 2660
shows "\<lbrakk>\<turnstile> v1 : r; \<turnstile> v2 : r; v1 \<succ>r v2; v2 \<succ>r v1\<rbrakk> \<Longrightarrow> v1 = v2"
+ − 2661
apply(induct r arbitrary: v1 v2)
+ − 2662
apply(erule Prf.cases)
+ − 2663
apply(simp_all)[5]
+ − 2664
apply(erule Prf.cases)
+ − 2665
apply(simp_all)[5]
+ − 2666
apply(erule Prf.cases)
+ − 2667
apply(simp_all)[5]
+ − 2668
apply(erule Prf.cases)
+ − 2669
apply(simp_all)[5]
+ − 2670
apply(erule Prf.cases)
+ − 2671
apply(simp_all)[5]
+ − 2672
apply(erule Prf.cases)
+ − 2673
apply(simp_all)[5]
+ − 2674
apply(erule Prf.cases)
+ − 2675
apply(simp_all)[5]
+ − 2676
apply(erule ValOrd.cases)
+ − 2677
apply(simp_all)[8]
+ − 2678
apply(erule ValOrd.cases)
+ − 2679
apply(simp_all)[8]
+ − 2680
apply(erule ValOrd.cases)
+ − 2681
apply(simp_all)[8]
+ − 2682
apply(erule Prf.cases)
+ − 2683
apply(simp_all)[5]
+ − 2684
apply(erule Prf.cases)
+ − 2685
apply(simp_all)[5]
+ − 2686
apply(erule ValOrd.cases)
+ − 2687
apply(simp_all)[8]
+ − 2688
apply(erule ValOrd.cases)
+ − 2689
apply(simp_all)[8]
+ − 2690
apply(erule ValOrd.cases)
+ − 2691
apply(simp_all)[8]
+ − 2692
apply(erule ValOrd.cases)
+ − 2693
apply(simp_all)[8]
+ − 2694
apply(erule Prf.cases)
+ − 2695
apply(simp_all)[5]
+ − 2696
apply(erule ValOrd.cases)
+ − 2697
apply(simp_all)[8]
+ − 2698
apply(erule ValOrd.cases)
+ − 2699
apply(simp_all)[8]
+ − 2700
apply(erule ValOrd.cases)
+ − 2701
apply(simp_all)[8]
+ − 2702
apply(erule ValOrd.cases)
+ − 2703
apply(simp_all)[8]
+ − 2704
done
+ − 2705
+ − 2706
lemma POSIX_ALT_I1:
+ − 2707
assumes "POSIX v1 r1"
+ − 2708
shows "POSIX (Left v1) (ALT r1 r2)"
+ − 2709
using assms
+ − 2710
unfolding POSIX_def
+ − 2711
apply(auto)
+ − 2712
apply (metis Prf.intros(2))
+ − 2713
apply(rotate_tac 2)
+ − 2714
apply(erule Prf.cases)
+ − 2715
apply(simp_all)[5]
+ − 2716
apply(auto)
+ − 2717
apply(rule ValOrd.intros)
+ − 2718
apply(auto)
+ − 2719
apply(rule ValOrd.intros)
+ − 2720
by (metis le_eq_less_or_eq length_sprefix sprefix_def)
+ − 2721
+ − 2722
lemma POSIX_ALT_I2:
+ − 2723
assumes "POSIX v2 r2" "\<forall>v'. \<turnstile> v' : r1 \<longrightarrow> length (flat v2) > length (flat v')"
+ − 2724
shows "POSIX (Right v2) (ALT r1 r2)"
+ − 2725
using assms
+ − 2726
unfolding POSIX_def
+ − 2727
apply(auto)
+ − 2728
apply (metis Prf.intros)
+ − 2729
apply(rotate_tac 3)
+ − 2730
apply(erule Prf.cases)
+ − 2731
apply(simp_all)[5]
+ − 2732
apply(auto)
+ − 2733
apply(rule ValOrd.intros)
+ − 2734
apply metis
+ − 2735
apply(rule ValOrd.intros)
+ − 2736
apply metis
+ − 2737
done
+ − 2738
+ − 2739
thm PMatch.intros[no_vars]
+ − 2740
+ − 2741
lemma POSIX_PMatch:
+ − 2742
assumes "s \<in> r \<rightarrow> v" "\<turnstile> v' : r"
+ − 2743
shows "length (flat v') \<le> length (flat v)"
+ − 2744
using assms
+ − 2745
apply(induct arbitrary: s v v' rule: rexp.induct)
+ − 2746
apply(erule Prf.cases)
+ − 2747
apply(simp_all)[5]
+ − 2748
apply(erule Prf.cases)
+ − 2749
apply(simp_all)[5]
+ − 2750
apply(erule Prf.cases)
+ − 2751
apply(simp_all)[5]
+ − 2752
apply(erule PMatch.cases)
+ − 2753
apply(simp_all)[5]
+ − 2754
defer
+ − 2755
apply(erule Prf.cases)
+ − 2756
apply(simp_all)[5]
+ − 2757
apply(erule PMatch.cases)
+ − 2758
apply(simp_all)[5]
+ − 2759
apply(clarify)
+ − 2760
apply(simp add: L_flat_Prf)
+ − 2761
+ − 2762
apply(clarify)
+ − 2763
apply (metis ValOrd.intros(8))
+ − 2764
apply (metis POSIX_ALT_I1)
+ − 2765
apply(rule POSIX_ALT_I2)
+ − 2766
apply(simp)
+ − 2767
apply(auto)[1]
+ − 2768
apply(simp add: POSIX_def)
+ − 2769
apply(frule PMatch1(1))
+ − 2770
apply(frule PMatch1(2))
+ − 2771
apply(simp)
+ − 2772
+ − 2773
+ − 2774
lemma POSIX_PMatch:
+ − 2775
assumes "s \<in> r \<rightarrow> v"
+ − 2776
shows "POSIX v r"
+ − 2777
using assms
+ − 2778
apply(induct arbitrary: rule: PMatch.induct)
+ − 2779
apply(auto)
+ − 2780
apply(simp add: POSIX_def)
+ − 2781
apply(auto)[1]
+ − 2782
apply (metis Prf.intros(4))
+ − 2783
apply(erule Prf.cases)
+ − 2784
apply(simp_all)[5]
+ − 2785
apply (metis ValOrd.intros(7))
+ − 2786
apply(simp add: POSIX_def)
+ − 2787
apply(auto)[1]
+ − 2788
apply (metis Prf.intros(5))
+ − 2789
apply(erule Prf.cases)
+ − 2790
apply(simp_all)[5]
+ − 2791
apply (metis ValOrd.intros(8))
+ − 2792
apply (metis POSIX_ALT_I1)
+ − 2793
apply(rule POSIX_ALT_I2)
+ − 2794
apply(simp)
+ − 2795
apply(auto)[1]
+ − 2796
apply(simp add: POSIX_def)
+ − 2797
apply(frule PMatch1(1))
+ − 2798
apply(frule PMatch1(2))
+ − 2799
apply(simp)
+ − 2800
+ − 2801
+ − 2802
+ − 2803
lemma ValOrd_PMatch:
+ − 2804
assumes "s \<in> r \<rightarrow> v1" "\<turnstile> v2 : r" "flat v2 = s"
+ − 2805
shows "v1 \<succ>r v2"
+ − 2806
using assms
+ − 2807
apply(induct arbitrary: v2 rule: PMatch.induct)
+ − 2808
apply(erule Prf.cases)
+ − 2809
apply(simp_all)[5]
+ − 2810
apply (metis ValOrd.intros(7))
+ − 2811
apply(erule Prf.cases)
+ − 2812
apply(simp_all)[5]
+ − 2813
apply (metis ValOrd.intros(8))
+ − 2814
apply(erule Prf.cases)
+ − 2815
apply(simp_all)[5]
+ − 2816
apply(clarify)
+ − 2817
apply (metis ValOrd.intros(6))
+ − 2818
apply(clarify)
+ − 2819
apply (metis PMatch1(2) ValOrd.intros(3) order_refl)
+ − 2820
apply(erule Prf.cases)
+ − 2821
apply(simp_all)[5]
+ − 2822
apply(clarify)
+ − 2823
apply (metis Prf_flat_L)
+ − 2824
apply (metis ValOrd.intros(5))
+ − 2825
(* Seq case *)
+ − 2826
apply(erule Prf.cases)
+ − 2827
apply(simp_all)[5]
+ − 2828
apply(auto)
+ − 2829
apply(case_tac "v1 = v1a")
+ − 2830
apply(auto)
+ − 2831
apply (metis PMatch1(2) ValOrd.intros(1) same_append_eq)
+ − 2832
apply(rule ValOrd.intros(2))
+ − 2833
apply(auto)
+ − 2834
apply(drule_tac x="v1a" in meta_spec)
+ − 2835
apply(drule_tac meta_mp)
+ − 2836
apply(simp)
+ − 2837
apply(drule_tac meta_mp)
+ − 2838
prefer 2
+ − 2839
apply(simp)
+ − 2840
apply(simp add: append_eq_append_conv2)
+ − 2841
apply(auto)
+ − 2842
apply (metis Prf_flat_L)
+ − 2843
apply(case_tac "us = []")
+ − 2844
apply(simp)
+ − 2845
apply(drule_tac x="us" in spec)
+ − 2846
apply(drule mp)
+ − 2847
+ − 2848
thm L_flat_Prf
+ − 2849
apply(simp add: L_flat_Prf)
+ − 2850
thm append_eq_append_conv2
+ − 2851
apply(simp add: append_eq_append_conv2)
+ − 2852
apply(auto)
+ − 2853
apply(drule_tac x="us" in spec)
+ − 2854
apply(drule mp)
+ − 2855
apply metis
+ − 2856
apply (metis append_Nil2)
+ − 2857
apply(case_tac "us = []")
+ − 2858
apply(auto)
+ − 2859
apply(drule_tac x="s2" in spec)
+ − 2860
apply(drule mp)
+ − 2861
+ − 2862
apply(auto)[1]
+ − 2863
apply(drule_tac x="v1a" in meta_spec)
+ − 2864
apply(simp)
+ − 2865
+ − 2866
lemma refl_on_ValOrd:
+ − 2867
"refl_on (Values r s) {(v1, v2). v1 \<succ>r v2 \<and> v1 \<in> Values r s \<and> v2 \<in> Values r s}"
+ − 2868
unfolding refl_on_def
+ − 2869
apply(auto)
+ − 2870
apply(rule ValOrd_refl)
+ − 2871
apply(simp add: Values_def)
+ − 2872
done
+ − 2873
+ − 2874
+ − 2875
section {* Posix definition *}
+ − 2876
+ − 2877
definition POSIX :: "val \<Rightarrow> rexp \<Rightarrow> bool"
+ − 2878
where
+ − 2879
"POSIX v r \<equiv> (\<turnstile> v : r \<and> (\<forall>v'. (\<turnstile> v' : r \<and> flat v = flat v') \<longrightarrow> v \<succ>r v'))"
+ − 2880
+ − 2881
definition POSIX2 :: "val \<Rightarrow> rexp \<Rightarrow> bool"
+ − 2882
where
+ − 2883
"POSIX2 v r \<equiv> (\<turnstile> v : r \<and> (\<forall>v'. (\<turnstile> v' : r \<and> flat v = flat v') \<longrightarrow> v 2\<succ> v'))"
+ − 2884
+ − 2885
lemma "POSIX v r = POSIX2 v r"
+ − 2886
unfolding POSIX_def POSIX2_def
+ − 2887
apply(auto)
+ − 2888
apply(rule Ord1)
+ − 2889
apply(auto)
+ − 2890
apply(rule Ord3)
+ − 2891
apply(auto)
+ − 2892
done
+ − 2893
+ − 2894
section {* POSIX for some constructors *}
+ − 2895
+ − 2896
lemma POSIX_SEQ1:
+ − 2897
assumes "POSIX (Seq v1 v2) (SEQ r1 r2)" "\<turnstile> v1 : r1" "\<turnstile> v2 : r2"
+ − 2898
shows "POSIX v1 r1"
+ − 2899
using assms
+ − 2900
unfolding POSIX_def
+ − 2901
apply(auto)
+ − 2902
apply(drule_tac x="Seq v' v2" in spec)
+ − 2903
apply(simp)
+ − 2904
apply(erule impE)
+ − 2905
apply(rule Prf.intros)
+ − 2906
apply(simp)
+ − 2907
apply(simp)
+ − 2908
apply(erule ValOrd.cases)
+ − 2909
apply(simp_all)
+ − 2910
apply(clarify)
+ − 2911
by (metis ValOrd_refl)
+ − 2912
+ − 2913
lemma POSIX_SEQ2:
+ − 2914
assumes "POSIX (Seq v1 v2) (SEQ r1 r2)" "\<turnstile> v1 : r1" "\<turnstile> v2 : r2"
+ − 2915
shows "POSIX v2 r2"
+ − 2916
using assms
+ − 2917
unfolding POSIX_def
+ − 2918
apply(auto)
+ − 2919
apply(drule_tac x="Seq v1 v'" in spec)
+ − 2920
apply(simp)
+ − 2921
apply(erule impE)
+ − 2922
apply(rule Prf.intros)
+ − 2923
apply(simp)
+ − 2924
apply(simp)
+ − 2925
apply(erule ValOrd.cases)
+ − 2926
apply(simp_all)
+ − 2927
done
+ − 2928
+ − 2929
lemma POSIX_ALT2:
+ − 2930
assumes "POSIX (Left v1) (ALT r1 r2)"
+ − 2931
shows "POSIX v1 r1"
+ − 2932
using assms
+ − 2933
unfolding POSIX_def
+ − 2934
apply(auto)
+ − 2935
apply(erule Prf.cases)
+ − 2936
apply(simp_all)[5]
+ − 2937
apply(drule_tac x="Left v'" in spec)
+ − 2938
apply(simp)
+ − 2939
apply(drule mp)
+ − 2940
apply(rule Prf.intros)
+ − 2941
apply(auto)
+ − 2942
apply(erule ValOrd.cases)
+ − 2943
apply(simp_all)
+ − 2944
done
+ − 2945
+ − 2946
lemma POSIX_ALT1a:
+ − 2947
assumes "POSIX (Right v2) (ALT r1 r2)"
+ − 2948
shows "POSIX v2 r2"
+ − 2949
using assms
+ − 2950
unfolding POSIX_def
+ − 2951
apply(auto)
+ − 2952
apply(erule Prf.cases)
+ − 2953
apply(simp_all)[5]
+ − 2954
apply(drule_tac x="Right v'" in spec)
+ − 2955
apply(simp)
+ − 2956
apply(drule mp)
+ − 2957
apply(rule Prf.intros)
+ − 2958
apply(auto)
+ − 2959
apply(erule ValOrd.cases)
+ − 2960
apply(simp_all)
+ − 2961
done
+ − 2962
+ − 2963
lemma POSIX_ALT1b:
+ − 2964
assumes "POSIX (Right v2) (ALT r1 r2)"
+ − 2965
shows "(\<forall>v'. (\<turnstile> v' : r2 \<and> flat v' = flat v2) \<longrightarrow> v2 \<succ>r2 v')"
+ − 2966
using assms
+ − 2967
apply(drule_tac POSIX_ALT1a)
+ − 2968
unfolding POSIX_def
+ − 2969
apply(auto)
+ − 2970
done
+ − 2971
+ − 2972
lemma POSIX_ALT_I1:
+ − 2973
assumes "POSIX v1 r1"
+ − 2974
shows "POSIX (Left v1) (ALT r1 r2)"
+ − 2975
using assms
+ − 2976
unfolding POSIX_def
+ − 2977
apply(auto)
+ − 2978
apply (metis Prf.intros(2))
+ − 2979
apply(rotate_tac 2)
+ − 2980
apply(erule Prf.cases)
+ − 2981
apply(simp_all)[5]
+ − 2982
apply(auto)
+ − 2983
apply(rule ValOrd.intros)
+ − 2984
apply(auto)
+ − 2985
apply(rule ValOrd.intros)
+ − 2986
by simp
+ − 2987
+ − 2988
lemma POSIX_ALT_I2:
+ − 2989
assumes "POSIX v2 r2" "\<forall>v'. \<turnstile> v' : r1 \<longrightarrow> length (flat v2) > length (flat v')"
+ − 2990
shows "POSIX (Right v2) (ALT r1 r2)"
+ − 2991
using assms
+ − 2992
unfolding POSIX_def
+ − 2993
apply(auto)
+ − 2994
apply (metis Prf.intros)
+ − 2995
apply(rotate_tac 3)
+ − 2996
apply(erule Prf.cases)
+ − 2997
apply(simp_all)[5]
+ − 2998
apply(auto)
+ − 2999
apply(rule ValOrd.intros)
+ − 3000
apply metis
+ − 3001
done
+ − 3002
+ − 3003
lemma mkeps_POSIX:
+ − 3004
assumes "nullable r"
+ − 3005
shows "POSIX (mkeps r) r"
+ − 3006
using assms
+ − 3007
apply(induct r)
+ − 3008
apply(auto)[1]
+ − 3009
apply(simp add: POSIX_def)
+ − 3010
apply(auto)[1]
+ − 3011
apply (metis Prf.intros(4))
+ − 3012
apply(erule Prf.cases)
+ − 3013
apply(simp_all)[5]
+ − 3014
apply (metis ValOrd.intros)
+ − 3015
apply(simp)
+ − 3016
apply(auto)[1]
+ − 3017
apply(simp add: POSIX_def)
+ − 3018
apply(auto)[1]
+ − 3019
apply (metis mkeps.simps(2) mkeps_nullable nullable.simps(5))
+ − 3020
apply(rotate_tac 6)
+ − 3021
apply(erule Prf.cases)
+ − 3022
apply(simp_all)[5]
+ − 3023
apply (simp add: mkeps_flat)
+ − 3024
apply(case_tac "mkeps r1a = v1")
+ − 3025
apply(simp)
+ − 3026
apply (metis ValOrd.intros(1))
+ − 3027
apply (rule ValOrd.intros(2))
+ − 3028
apply metis
+ − 3029
apply(simp)
+ − 3030
(* ALT case *)
+ − 3031
thm mkeps.simps
+ − 3032
apply(simp)
+ − 3033
apply(erule disjE)
+ − 3034
apply(simp)
+ − 3035
apply (metis POSIX_ALT_I1)
+ − 3036
(* *)
+ − 3037
apply(auto)[1]
+ − 3038
thm POSIX_ALT_I1
+ − 3039
apply (metis POSIX_ALT_I1)
+ − 3040
apply(simp (no_asm) add: POSIX_def)
+ − 3041
apply(auto)[1]
+ − 3042
apply(rule Prf.intros(3))
+ − 3043
apply(simp only: POSIX_def)
+ − 3044
apply(rotate_tac 4)
+ − 3045
apply(erule Prf.cases)
+ − 3046
apply(simp_all)[5]
+ − 3047
thm mkeps_flat
+ − 3048
apply(simp add: mkeps_flat)
+ − 3049
apply(auto)[1]
+ − 3050
thm Prf_flat_L nullable_correctness
+ − 3051
apply (metis Prf_flat_L nullable_correctness)
+ − 3052
apply(rule ValOrd.intros)
+ − 3053
apply(subst (asm) POSIX_def)
+ − 3054
apply(clarify)
+ − 3055
apply(drule_tac x="v2" in spec)
+ − 3056
by simp
+ − 3057
+ − 3058
+ − 3059
+ − 3060
text {*
+ − 3061
Injection value is related to r
+ − 3062
*}
+ − 3063
+ − 3064
+ − 3065
+ − 3066
text {*
+ − 3067
The string behind the injection value is an added c
+ − 3068
*}
+ − 3069
+ − 3070
+ − 3071
lemma injval_inj: "inj_on (injval r c) {v. \<turnstile> v : der c r}"
+ − 3072
apply(induct c r rule: der.induct)
+ − 3073
unfolding inj_on_def
+ − 3074
apply(auto)[1]
+ − 3075
apply(erule Prf.cases)
+ − 3076
apply(simp_all)[5]
+ − 3077
apply(auto)[1]
+ − 3078
apply(erule Prf.cases)
+ − 3079
apply(simp_all)[5]
+ − 3080
apply(auto)[1]
+ − 3081
apply(erule Prf.cases)
+ − 3082
apply(simp_all)[5]
+ − 3083
apply(erule Prf.cases)
+ − 3084
apply(simp_all)[5]
+ − 3085
apply(erule Prf.cases)
+ − 3086
apply(simp_all)[5]
+ − 3087
apply(auto)[1]
+ − 3088
apply(erule Prf.cases)
+ − 3089
apply(simp_all)[5]
+ − 3090
apply(erule Prf.cases)
+ − 3091
apply(simp_all)[5]
+ − 3092
apply(erule Prf.cases)
+ − 3093
apply(simp_all)[5]
+ − 3094
apply(auto)[1]
+ − 3095
apply(erule Prf.cases)
+ − 3096
apply(simp_all)[5]
+ − 3097
apply(erule Prf.cases)
+ − 3098
apply(simp_all)[5]
+ − 3099
apply(clarify)
+ − 3100
apply(erule Prf.cases)
+ − 3101
apply(simp_all)[5]
+ − 3102
apply(erule Prf.cases)
+ − 3103
apply(simp_all)[5]
+ − 3104
apply(clarify)
+ − 3105
apply(erule Prf.cases)
+ − 3106
apply(simp_all)[5]
+ − 3107
apply(clarify)
+ − 3108
apply (metis list.distinct(1) mkeps_flat v4)
+ − 3109
apply(erule Prf.cases)
+ − 3110
apply(simp_all)[5]
+ − 3111
apply(clarify)
+ − 3112
apply(rotate_tac 6)
+ − 3113
apply(erule Prf.cases)
+ − 3114
apply(simp_all)[5]
+ − 3115
apply (metis list.distinct(1) mkeps_flat v4)
+ − 3116
apply(erule Prf.cases)
+ − 3117
apply(simp_all)[5]
+ − 3118
apply(erule Prf.cases)
+ − 3119
apply(simp_all)[5]
+ − 3120
done
+ − 3121
+ − 3122
lemma Values_nullable:
+ − 3123
assumes "nullable r1"
+ − 3124
shows "mkeps r1 \<in> Values r1 s"
+ − 3125
using assms
+ − 3126
apply(induct r1 arbitrary: s)
+ − 3127
apply(simp_all)
+ − 3128
apply(simp add: Values_recs)
+ − 3129
apply(simp add: Values_recs)
+ − 3130
apply(simp add: Values_recs)
+ − 3131
apply(auto)[1]
+ − 3132
done
+ − 3133
+ − 3134
lemma Values_injval:
+ − 3135
assumes "v \<in> Values (der c r) s"
+ − 3136
shows "injval r c v \<in> Values r (c#s)"
+ − 3137
using assms
+ − 3138
apply(induct c r arbitrary: v s rule: der.induct)
+ − 3139
apply(simp add: Values_recs)
+ − 3140
apply(simp add: Values_recs)
+ − 3141
apply(case_tac "c = c'")
+ − 3142
apply(simp)
+ − 3143
apply(simp add: Values_recs)
+ − 3144
apply(simp add: prefix_def)
+ − 3145
apply(simp)
+ − 3146
apply(simp add: Values_recs)
+ − 3147
apply(simp)
+ − 3148
apply(simp add: Values_recs)
+ − 3149
apply(auto)[1]
+ − 3150
apply(case_tac "nullable r1")
+ − 3151
apply(simp)
+ − 3152
apply(simp add: Values_recs)
+ − 3153
apply(auto)[1]
+ − 3154
apply(simp add: rest_def)
+ − 3155
apply(subst v4)
+ − 3156
apply(simp add: Values_def)
+ − 3157
apply(simp add: Values_def)
+ − 3158
apply(rule Values_nullable)
+ − 3159
apply(assumption)
+ − 3160
apply(simp add: rest_def)
+ − 3161
apply(subst mkeps_flat)
+ − 3162
apply(assumption)
+ − 3163
apply(simp)
+ − 3164
apply(simp)
+ − 3165
apply(simp add: Values_recs)
+ − 3166
apply(auto)[1]
+ − 3167
apply(simp add: rest_def)
+ − 3168
apply(subst v4)
+ − 3169
apply(simp add: Values_def)
+ − 3170
apply(simp add: Values_def)
+ − 3171
done
+ − 3172
+ − 3173
lemma Values_projval:
+ − 3174
assumes "v \<in> Values r (c#s)" "\<exists>s. flat v = c # s"
+ − 3175
shows "projval r c v \<in> Values (der c r) s"
+ − 3176
using assms
+ − 3177
apply(induct r arbitrary: v s c rule: rexp.induct)
+ − 3178
apply(simp add: Values_recs)
+ − 3179
apply(simp add: Values_recs)
+ − 3180
apply(case_tac "c = char")
+ − 3181
apply(simp)
+ − 3182
apply(simp add: Values_recs)
+ − 3183
apply(simp)
+ − 3184
apply(simp add: Values_recs)
+ − 3185
apply(simp add: prefix_def)
+ − 3186
apply(case_tac "nullable rexp1")
+ − 3187
apply(simp)
+ − 3188
apply(simp add: Values_recs)
+ − 3189
apply(auto)[1]
+ − 3190
apply(simp add: rest_def)
+ − 3191
apply (metis hd_Cons_tl hd_append2 list.sel(1))
+ − 3192
apply(simp add: rest_def)
+ − 3193
apply(simp add: append_eq_Cons_conv)
+ − 3194
apply(auto)[1]
+ − 3195
apply(subst v4_proj2)
+ − 3196
apply(simp add: Values_def)
+ − 3197
apply(assumption)
+ − 3198
apply(simp)
+ − 3199
apply(simp)
+ − 3200
apply(simp add: Values_recs)
+ − 3201
apply(auto)[1]
+ − 3202
apply(auto simp add: Values_def not_nullable_flat)[1]
+ − 3203
apply(simp add: append_eq_Cons_conv)
+ − 3204
apply(auto)[1]
+ − 3205
apply(simp add: append_eq_Cons_conv)
+ − 3206
apply(auto)[1]
+ − 3207
apply(simp add: rest_def)
+ − 3208
apply(subst v4_proj2)
+ − 3209
apply(simp add: Values_def)
+ − 3210
apply(assumption)
+ − 3211
apply(simp)
+ − 3212
apply(simp add: Values_recs)
+ − 3213
apply(auto)[1]
+ − 3214
done
+ − 3215
+ − 3216
+ − 3217
definition "MValue v r s \<equiv> (v \<in> Values r s \<and> (\<forall>v' \<in> Values r s. v 2\<succ> v'))"
+ − 3218
+ − 3219
lemma MValue_ALTE:
+ − 3220
assumes "MValue v (ALT r1 r2) s"
+ − 3221
shows "(\<exists>vl. v = Left vl \<and> MValue vl r1 s \<and> (\<forall>vr \<in> Values r2 s. length (flat vr) \<le> length (flat vl))) \<or>
+ − 3222
(\<exists>vr. v = Right vr \<and> MValue vr r2 s \<and> (\<forall>vl \<in> Values r1 s. length (flat vl) < length (flat vr)))"
+ − 3223
using assms
+ − 3224
apply(simp add: MValue_def)
+ − 3225
apply(simp add: Values_recs)
+ − 3226
apply(auto)
+ − 3227
apply(drule_tac x="Left x" in bspec)
+ − 3228
apply(simp)
+ − 3229
apply(erule ValOrd2.cases)
+ − 3230
apply(simp_all)
+ − 3231
apply(drule_tac x="Right vr" in bspec)
+ − 3232
apply(simp)
+ − 3233
apply(erule ValOrd2.cases)
+ − 3234
apply(simp_all)
+ − 3235
apply(drule_tac x="Right x" in bspec)
+ − 3236
apply(simp)
+ − 3237
apply(erule ValOrd2.cases)
+ − 3238
apply(simp_all)
+ − 3239
apply(drule_tac x="Left vl" in bspec)
+ − 3240
apply(simp)
+ − 3241
apply(erule ValOrd2.cases)
+ − 3242
apply(simp_all)
+ − 3243
done
+ − 3244
+ − 3245
lemma MValue_ALTI1:
+ − 3246
assumes "MValue vl r1 s" "\<forall>vr \<in> Values r2 s. length (flat vr) \<le> length (flat vl)"
+ − 3247
shows "MValue (Left vl) (ALT r1 r2) s"
+ − 3248
using assms
+ − 3249
apply(simp add: MValue_def)
+ − 3250
apply(simp add: Values_recs)
+ − 3251
apply(auto)
+ − 3252
apply(rule ValOrd2.intros)
+ − 3253
apply metis
+ − 3254
apply(rule ValOrd2.intros)
+ − 3255
apply metis
+ − 3256
done
+ − 3257
+ − 3258
lemma MValue_ALTI2:
+ − 3259
assumes "MValue vr r2 s" "\<forall>vl \<in> Values r1 s. length (flat vl) < length (flat vr)"
+ − 3260
shows "MValue (Right vr) (ALT r1 r2) s"
+ − 3261
using assms
+ − 3262
apply(simp add: MValue_def)
+ − 3263
apply(simp add: Values_recs)
+ − 3264
apply(auto)
+ − 3265
apply(rule ValOrd2.intros)
+ − 3266
apply metis
+ − 3267
apply(rule ValOrd2.intros)
+ − 3268
apply metis
+ − 3269
done
+ − 3270
+ − 3271
lemma t: "(c#xs = c#ys) \<Longrightarrow> xs = ys"
+ − 3272
by (metis list.sel(3))
+ − 3273
+ − 3274
lemma t2: "(xs = ys) \<Longrightarrow> (c#xs) = (c#ys)"
+ − 3275
by (metis)
+ − 3276
+ − 3277
lemma "\<not>(nullable r) \<Longrightarrow> \<not>(\<exists>v. \<turnstile> v : r \<and> flat v = [])"
+ − 3278
by (metis Prf_flat_L nullable_correctness)
+ − 3279
+ − 3280
+ − 3281
lemma LeftRight:
+ − 3282
assumes "(Left v1) \<succ>(der c (ALT r1 r2)) (Right v2)"
+ − 3283
and "\<turnstile> v1 : der c r1" "\<turnstile> v2 : der c r2"
+ − 3284
shows "(injval (ALT r1 r2) c (Left v1)) \<succ>(ALT r1 r2) (injval (ALT r1 r2) c (Right v2))"
+ − 3285
using assms
+ − 3286
apply(simp)
+ − 3287
apply(erule ValOrd.cases)
+ − 3288
apply(simp_all)[8]
+ − 3289
apply(rule ValOrd.intros)
+ − 3290
apply(clarify)
+ − 3291
apply(subst v4)
+ − 3292
apply(simp)
+ − 3293
apply(subst v4)
+ − 3294
apply(simp)
+ − 3295
apply(simp)
+ − 3296
done
+ − 3297
+ − 3298
lemma RightLeft:
+ − 3299
assumes "(Right v1) \<succ>(der c (ALT r1 r2)) (Left v2)"
+ − 3300
and "\<turnstile> v1 : der c r2" "\<turnstile> v2 : der c r1"
+ − 3301
shows "(injval (ALT r1 r2) c (Right v1)) \<succ>(ALT r1 r2) (injval (ALT r1 r2) c (Left v2))"
+ − 3302
using assms
+ − 3303
apply(simp)
+ − 3304
apply(erule ValOrd.cases)
+ − 3305
apply(simp_all)[8]
+ − 3306
apply(rule ValOrd.intros)
+ − 3307
apply(clarify)
+ − 3308
apply(subst v4)
+ − 3309
apply(simp)
+ − 3310
apply(subst v4)
+ − 3311
apply(simp)
+ − 3312
apply(simp)
+ − 3313
done
+ − 3314
+ − 3315
lemma h:
+ − 3316
assumes "nullable r1" "\<turnstile> v1 : der c r1"
+ − 3317
shows "injval r1 c v1 \<succ>r1 mkeps r1"
+ − 3318
using assms
+ − 3319
apply(induct r1 arbitrary: v1 rule: der.induct)
+ − 3320
apply(simp)
+ − 3321
apply(simp)
+ − 3322
apply(erule Prf.cases)
+ − 3323
apply(simp_all)[5]
+ − 3324
apply(simp)
+ − 3325
apply(simp)
+ − 3326
apply(erule Prf.cases)
+ − 3327
apply(simp_all)[5]
+ − 3328
apply(clarify)
+ − 3329
apply(auto)[1]
+ − 3330
apply (metis ValOrd.intros(6))
+ − 3331
apply (metis ValOrd.intros(6))
+ − 3332
apply (metis ValOrd.intros(3) le_add2 list.size(3) mkeps_flat monoid_add_class.add.right_neutral)
+ − 3333
apply(auto)[1]
+ − 3334
apply (metis ValOrd.intros(4) length_greater_0_conv list.distinct(1) list.size(3) mkeps_flat v4)
+ − 3335
apply (metis ValOrd.intros(4) length_greater_0_conv list.distinct(1) list.size(3) mkeps_flat v4)
+ − 3336
apply (metis ValOrd.intros(5))
+ − 3337
apply(simp)
+ − 3338
apply(erule Prf.cases)
+ − 3339
apply(simp_all)[5]
+ − 3340
apply(clarify)
+ − 3341
apply(erule Prf.cases)
+ − 3342
apply(simp_all)[5]
+ − 3343
apply(clarify)
+ − 3344
apply (metis ValOrd.intros(2) list.distinct(1) mkeps_flat v4)
+ − 3345
apply(clarify)
+ − 3346
by (metis ValOrd.intros(1))
+ − 3347
+ − 3348
lemma LeftRightSeq:
+ − 3349
assumes "(Left (Seq v1 v2)) \<succ>(der c (SEQ r1 r2)) (Right v3)"
+ − 3350
and "nullable r1" "\<turnstile> v1 : der c r1"
+ − 3351
shows "(injval (SEQ r1 r2) c (Seq v1 v2)) \<succ>(SEQ r1 r2) (injval (SEQ r1 r2) c (Right v2))"
+ − 3352
using assms
+ − 3353
apply(simp)
+ − 3354
apply(erule ValOrd.cases)
+ − 3355
apply(simp_all)[8]
+ − 3356
apply(clarify)
+ − 3357
apply(simp)
+ − 3358
apply(rule ValOrd.intros(2))
+ − 3359
prefer 2
+ − 3360
apply (metis list.distinct(1) mkeps_flat v4)
+ − 3361
by (metis h)
+ − 3362
+ − 3363
lemma rr1:
+ − 3364
assumes "\<turnstile> v : r" "\<not>nullable r"
+ − 3365
shows "flat v \<noteq> []"
+ − 3366
using assms
+ − 3367
by (metis Prf_flat_L nullable_correctness)
+ − 3368
+ − 3369
(* HERE *)
+ − 3370
+ − 3371
lemma Prf_inj_test:
+ − 3372
assumes "v1 \<succ>(der c r) v2"
+ − 3373
"v1 \<in> Values (der c r) s"
+ − 3374
"v2 \<in> Values (der c r) s"
+ − 3375
"injval r c v1 \<in> Values r (c#s)"
+ − 3376
"injval r c v2 \<in> Values r (c#s)"
+ − 3377
shows "(injval r c v1) 2\<succ> (injval r c v2)"
+ − 3378
using assms
+ − 3379
apply(induct c r arbitrary: v1 v2 s rule: der.induct)
+ − 3380
(* NULL case *)
+ − 3381
apply(simp add: Values_recs)
+ − 3382
(* EMPTY case *)
+ − 3383
apply(simp add: Values_recs)
+ − 3384
(* CHAR case *)
+ − 3385
apply(case_tac "c = c'")
+ − 3386
apply(simp)
+ − 3387
apply(simp add: Values_recs)
+ − 3388
apply (metis ValOrd2.intros(8))
+ − 3389
apply(simp add: Values_recs)
+ − 3390
(* ALT case *)
+ − 3391
apply(simp)
+ − 3392
apply(simp add: Values_recs)
+ − 3393
apply(auto)[1]
+ − 3394
apply(erule ValOrd.cases)
+ − 3395
apply(simp_all)[8]
+ − 3396
apply (metis ValOrd2.intros(6))
+ − 3397
apply(erule ValOrd.cases)
+ − 3398
apply(simp_all)[8]
+ − 3399
apply(rule ValOrd2.intros)
+ − 3400
apply(subst v4)
+ − 3401
apply(simp add: Values_def)
+ − 3402
apply(subst v4)
+ − 3403
apply(simp add: Values_def)
+ − 3404
apply(simp)
+ − 3405
apply(erule ValOrd.cases)
+ − 3406
apply(simp_all)[8]
+ − 3407
apply(rule ValOrd2.intros)
+ − 3408
apply(subst v4)
+ − 3409
apply(simp add: Values_def)
+ − 3410
apply(subst v4)
+ − 3411
apply(simp add: Values_def)
+ − 3412
apply(simp)
+ − 3413
apply(erule ValOrd.cases)
+ − 3414
apply(simp_all)[8]
+ − 3415
apply (metis ValOrd2.intros(5))
+ − 3416
(* SEQ case*)
+ − 3417
apply(simp)
+ − 3418
apply(case_tac "nullable r1")
+ − 3419
apply(simp)
+ − 3420
defer
+ − 3421
apply(simp)
+ − 3422
apply(simp add: Values_recs)
+ − 3423
apply(auto)[1]
+ − 3424
apply(erule ValOrd.cases)
+ − 3425
apply(simp_all)[8]
+ − 3426
apply(clarify)
+ − 3427
apply(rule ValOrd2.intros)
+ − 3428
apply(simp)
+ − 3429
apply (metis Ord1)
+ − 3430
apply(clarify)
+ − 3431
apply(rule ValOrd2.intros)
+ − 3432
apply(subgoal_tac "rest v1 (flat v1 @ flat v2) = flat v2")
+ − 3433
apply(simp)
+ − 3434
apply(subgoal_tac "rest (injval r1 c v1) (c # flat v1 @ flat v2) = flat v2")
+ − 3435
apply(simp)
+ − 3436
oops
+ − 3437
+ − 3438
lemma Prf_inj_test:
+ − 3439
assumes "v1 \<succ>(der c r) v2"
+ − 3440
"v1 \<in> Values (der c r) s"
+ − 3441
"v2 \<in> Values (der c r) s"
+ − 3442
"injval r c v1 \<in> Values r (c#s)"
+ − 3443
"injval r c v2 \<in> Values r (c#s)"
+ − 3444
shows "(injval r c v1) 2\<succ> (injval r c v2)"
+ − 3445
using assms
+ − 3446
apply(induct c r arbitrary: v1 v2 s rule: der.induct)
+ − 3447
(* NULL case *)
+ − 3448
apply(simp add: Values_recs)
+ − 3449
(* EMPTY case *)
+ − 3450
apply(simp add: Values_recs)
+ − 3451
(* CHAR case *)
+ − 3452
apply(case_tac "c = c'")
+ − 3453
apply(simp)
+ − 3454
apply(simp add: Values_recs)
+ − 3455
apply (metis ValOrd2.intros(8))
+ − 3456
apply(simp add: Values_recs)
+ − 3457
(* ALT case *)
+ − 3458
apply(simp)
+ − 3459
apply(simp add: Values_recs)
+ − 3460
apply(auto)[1]
+ − 3461
apply(erule ValOrd.cases)
+ − 3462
apply(simp_all)[8]
+ − 3463
apply (metis ValOrd2.intros(6))
+ − 3464
apply(erule ValOrd.cases)
+ − 3465
apply(simp_all)[8]
+ − 3466
apply(rule ValOrd2.intros)
+ − 3467
apply(subst v4)
+ − 3468
apply(simp add: Values_def)
+ − 3469
apply(subst v4)
+ − 3470
apply(simp add: Values_def)
+ − 3471
apply(simp)
+ − 3472
apply(erule ValOrd.cases)
+ − 3473
apply(simp_all)[8]
+ − 3474
apply(rule ValOrd2.intros)
+ − 3475
apply(subst v4)
+ − 3476
apply(simp add: Values_def)
+ − 3477
apply(subst v4)
+ − 3478
apply(simp add: Values_def)
+ − 3479
apply(simp)
+ − 3480
apply(erule ValOrd.cases)
+ − 3481
apply(simp_all)[8]
+ − 3482
apply (metis ValOrd2.intros(5))
+ − 3483
(* SEQ case*)
+ − 3484
apply(simp)
+ − 3485
apply(case_tac "nullable r1")
+ − 3486
apply(simp)
+ − 3487
defer
+ − 3488
apply(simp)
+ − 3489
apply(simp add: Values_recs)
+ − 3490
apply(auto)[1]
+ − 3491
apply(erule ValOrd.cases)
+ − 3492
apply(simp_all)[8]
+ − 3493
apply(clarify)
+ − 3494
apply(rule ValOrd2.intros)
+ − 3495
apply(simp)
+ − 3496
apply (metis Ord1)
+ − 3497
apply(clarify)
+ − 3498
apply(rule ValOrd2.intros)
+ − 3499
apply metis
+ − 3500
using injval_inj
+ − 3501
apply(simp add: Values_def inj_on_def)
+ − 3502
apply metis
+ − 3503
apply(simp add: Values_recs)
+ − 3504
apply(auto)[1]
+ − 3505
apply(erule ValOrd.cases)
+ − 3506
apply(simp_all)[8]
+ − 3507
apply(clarify)
+ − 3508
apply(erule ValOrd.cases)
+ − 3509
apply(simp_all)[8]
+ − 3510
apply(clarify)
+ − 3511
apply (metis Ord1 ValOrd2.intros(1))
+ − 3512
apply(clarify)
+ − 3513
apply(rule ValOrd2.intros(2))
+ − 3514
apply metis
+ − 3515
using injval_inj
+ − 3516
apply(simp add: Values_def inj_on_def)
+ − 3517
apply metis
+ − 3518
apply(erule ValOrd.cases)
+ − 3519
apply(simp_all)[8]
+ − 3520
apply(rule ValOrd2.intros(2))
+ − 3521
thm h
+ − 3522
apply(rule Ord1)
+ − 3523
apply(rule h)
+ − 3524
apply(simp)
+ − 3525
apply(simp add: Values_def)
+ − 3526
apply(simp add: Values_def)
+ − 3527
apply (metis list.distinct(1) mkeps_flat v4)
+ − 3528
apply(erule ValOrd.cases)
+ − 3529
apply(simp_all)[8]
+ − 3530
apply(clarify)
+ − 3531
apply(simp add: Values_def)
+ − 3532
defer
+ − 3533
apply(erule ValOrd.cases)
+ − 3534
apply(simp_all)[8]
+ − 3535
apply(clarify)
+ − 3536
apply(rule ValOrd2.intros(1))
+ − 3537
apply(rotate_tac 1)
+ − 3538
apply(drule_tac x="v2" in meta_spec)
+ − 3539
apply(rotate_tac 8)
+ − 3540
apply(drule_tac x="v2'" in meta_spec)
+ − 3541
apply(rotate_tac 8)
+ − 3542
oops
+ − 3543
+ − 3544
lemma POSIX_der:
+ − 3545
assumes "POSIX v (der c r)" "\<turnstile> v : der c r"
+ − 3546
shows "POSIX (injval r c v) r"
+ − 3547
using assms
+ − 3548
unfolding POSIX_def
+ − 3549
apply(auto)
+ − 3550
thm v3
+ − 3551
apply (erule v3)
+ − 3552
thm v4
+ − 3553
apply(subst (asm) v4)
+ − 3554
apply(assumption)
+ − 3555
apply(drule_tac x="projval r c v'" in spec)
+ − 3556
apply(drule mp)
+ − 3557
apply(rule conjI)
+ − 3558
thm v3_proj
+ − 3559
apply(rule v3_proj)
+ − 3560
apply(simp)
+ − 3561
apply(rule_tac x="flat v" in exI)
+ − 3562
apply(simp)
+ − 3563
thm t
+ − 3564
apply(rule_tac c="c" in t)
+ − 3565
apply(simp)
+ − 3566
thm v4_proj
+ − 3567
apply(subst v4_proj)
+ − 3568
apply(simp)
+ − 3569
apply(rule_tac x="flat v" in exI)
+ − 3570
apply(simp)
+ − 3571
apply(simp)
+ − 3572
oops
+ − 3573
+ − 3574
lemma POSIX_der:
+ − 3575
assumes "POSIX v (der c r)" "\<turnstile> v : der c r"
+ − 3576
shows "POSIX (injval r c v) r"
+ − 3577
using assms
+ − 3578
apply(induct c r arbitrary: v rule: der.induct)
+ − 3579
(* null case*)
+ − 3580
apply(simp add: POSIX_def)
+ − 3581
apply(auto)[1]
+ − 3582
apply(erule Prf.cases)
+ − 3583
apply(simp_all)[5]
+ − 3584
apply(erule Prf.cases)
+ − 3585
apply(simp_all)[5]
+ − 3586
(* empty case *)
+ − 3587
apply(simp add: POSIX_def)
+ − 3588
apply(auto)[1]
+ − 3589
apply(erule Prf.cases)
+ − 3590
apply(simp_all)[5]
+ − 3591
apply(erule Prf.cases)
+ − 3592
apply(simp_all)[5]
+ − 3593
(* char case *)
+ − 3594
apply(simp add: POSIX_def)
+ − 3595
apply(case_tac "c = c'")
+ − 3596
apply(auto)[1]
+ − 3597
apply(erule Prf.cases)
+ − 3598
apply(simp_all)[5]
+ − 3599
apply (metis Prf.intros(5))
+ − 3600
apply(erule Prf.cases)
+ − 3601
apply(simp_all)[5]
+ − 3602
apply(erule Prf.cases)
+ − 3603
apply(simp_all)[5]
+ − 3604
apply (metis ValOrd.intros(8))
+ − 3605
apply(auto)[1]
+ − 3606
apply(erule Prf.cases)
+ − 3607
apply(simp_all)[5]
+ − 3608
apply(erule Prf.cases)
+ − 3609
apply(simp_all)[5]
+ − 3610
(* alt case *)
+ − 3611
apply(erule Prf.cases)
+ − 3612
apply(simp_all)[5]
+ − 3613
apply(clarify)
+ − 3614
apply(simp (no_asm) add: POSIX_def)
+ − 3615
apply(auto)[1]
+ − 3616
apply (metis Prf.intros(2) v3)
+ − 3617
apply(rotate_tac 4)
+ − 3618
apply(erule Prf.cases)
+ − 3619
apply(simp_all)[5]
+ − 3620
apply (metis POSIX_ALT2 POSIX_def ValOrd.intros(6))
+ − 3621
apply (metis ValOrd.intros(3) order_refl)
+ − 3622
apply(simp (no_asm) add: POSIX_def)
+ − 3623
apply(auto)[1]
+ − 3624
apply (metis Prf.intros(3) v3)
+ − 3625
apply(rotate_tac 4)
+ − 3626
apply(erule Prf.cases)
+ − 3627
apply(simp_all)[5]
+ − 3628
defer
+ − 3629
apply (metis POSIX_ALT1a POSIX_def ValOrd.intros(5))
+ − 3630
prefer 2
+ − 3631
apply(subst (asm) (5) POSIX_def)
+ − 3632
apply(auto)[1]
+ − 3633
apply(rotate_tac 5)
+ − 3634
apply(erule Prf.cases)
+ − 3635
apply(simp_all)[5]
+ − 3636
apply(rule ValOrd.intros)
+ − 3637
apply(subst (asm) v4)
+ − 3638
apply(simp)
+ − 3639
apply(drule_tac x="Left (projval r1a c v1)" in spec)
+ − 3640
apply(clarify)
+ − 3641
apply(drule mp)
+ − 3642
apply(rule conjI)
+ − 3643
apply (metis Prf.intros(2) v3_proj)
+ − 3644
apply(simp)
+ − 3645
apply (metis v4_proj2)
+ − 3646
apply(erule ValOrd.cases)
+ − 3647
apply(simp_all)[8]
+ − 3648
apply (metis less_not_refl v4_proj2)
+ − 3649
(* seq case *)
+ − 3650
apply(case_tac "nullable r1")
+ − 3651
defer
+ − 3652
apply(simp add: POSIX_def)
+ − 3653
apply(auto)[1]
+ − 3654
apply(erule Prf.cases)
+ − 3655
apply(simp_all)[5]
+ − 3656
apply (metis Prf.intros(1) v3)
+ − 3657
apply(erule Prf.cases)
+ − 3658
apply(simp_all)[5]
+ − 3659
apply(erule Prf.cases)
+ − 3660
apply(simp_all)[5]
+ − 3661
apply(clarify)
+ − 3662
apply(subst (asm) (3) v4)
+ − 3663
apply(simp)
+ − 3664
apply(simp)
+ − 3665
apply(subgoal_tac "flat v1a \<noteq> []")
+ − 3666
prefer 2
+ − 3667
apply (metis Prf_flat_L nullable_correctness)
+ − 3668
apply(subgoal_tac "\<exists>s. flat v1a = c # s")
+ − 3669
prefer 2
+ − 3670
apply (metis append_eq_Cons_conv)
+ − 3671
apply(auto)[1]
+ − 3672
oops
+ − 3673
+ − 3674
+ − 3675
lemma POSIX_ex: "\<turnstile> v : r \<Longrightarrow> \<exists>v. POSIX v r"
+ − 3676
apply(induct r arbitrary: v)
+ − 3677
apply(erule Prf.cases)
+ − 3678
apply(simp_all)[5]
+ − 3679
apply(erule Prf.cases)
+ − 3680
apply(simp_all)[5]
+ − 3681
apply(rule_tac x="Void" in exI)
+ − 3682
apply(simp add: POSIX_def)
+ − 3683
apply(auto)[1]
+ − 3684
apply (metis Prf.intros(4))
+ − 3685
apply(erule Prf.cases)
+ − 3686
apply(simp_all)[5]
+ − 3687
apply (metis ValOrd.intros(7))
+ − 3688
apply(erule Prf.cases)
+ − 3689
apply(simp_all)[5]
+ − 3690
apply(rule_tac x="Char c" in exI)
+ − 3691
apply(simp add: POSIX_def)
+ − 3692
apply(auto)[1]
+ − 3693
apply (metis Prf.intros(5))
+ − 3694
apply(erule Prf.cases)
+ − 3695
apply(simp_all)[5]
+ − 3696
apply (metis ValOrd.intros(8))
+ − 3697
apply(erule Prf.cases)
+ − 3698
apply(simp_all)[5]
+ − 3699
apply(auto)[1]
+ − 3700
apply(drule_tac x="v1" in meta_spec)
+ − 3701
apply(drule_tac x="v2" in meta_spec)
+ − 3702
apply(auto)[1]
+ − 3703
defer
+ − 3704
apply(erule Prf.cases)
+ − 3705
apply(simp_all)[5]
+ − 3706
apply(auto)[1]
+ − 3707
apply (metis POSIX_ALT_I1)
+ − 3708
apply (metis POSIX_ALT_I1 POSIX_ALT_I2)
+ − 3709
apply(case_tac "nullable r1a")
+ − 3710
apply(rule_tac x="Seq (mkeps r1a) va" in exI)
+ − 3711
apply(auto simp add: POSIX_def)[1]
+ − 3712
apply (metis Prf.intros(1) mkeps_nullable)
+ − 3713
apply(simp add: mkeps_flat)
+ − 3714
apply(rotate_tac 7)
+ − 3715
apply(erule Prf.cases)
+ − 3716
apply(simp_all)[5]
+ − 3717
apply(case_tac "mkeps r1 = v1a")
+ − 3718
apply(simp)
+ − 3719
apply (rule ValOrd.intros(1))
+ − 3720
apply (metis append_Nil mkeps_flat)
+ − 3721
apply (rule ValOrd.intros(2))
+ − 3722
apply(drule mkeps_POSIX)
+ − 3723
apply(simp add: POSIX_def)
+ − 3724
oops
+ − 3725
+ − 3726
lemma POSIX_ex2: "\<turnstile> v : r \<Longrightarrow> \<exists>v. POSIX v r \<and> \<turnstile> v : r"
+ − 3727
apply(induct r arbitrary: v)
+ − 3728
apply(erule Prf.cases)
+ − 3729
apply(simp_all)[5]
+ − 3730
apply(erule Prf.cases)
+ − 3731
apply(simp_all)[5]
+ − 3732
apply(rule_tac x="Void" in exI)
+ − 3733
apply(simp add: POSIX_def)
+ − 3734
apply(auto)[1]
+ − 3735
oops
+ − 3736
+ − 3737
lemma POSIX_ALT_cases:
+ − 3738
assumes "\<turnstile> v : (ALT r1 r2)" "POSIX v (ALT r1 r2)"
+ − 3739
shows "(\<exists>v1. v = Left v1 \<and> POSIX v1 r1) \<or> (\<exists>v2. v = Right v2 \<and> POSIX v2 r2)"
+ − 3740
using assms
+ − 3741
apply(erule_tac Prf.cases)
+ − 3742
apply(simp_all)
+ − 3743
unfolding POSIX_def
+ − 3744
apply(auto)
+ − 3745
apply (metis POSIX_ALT2 POSIX_def assms(2))
+ − 3746
by (metis POSIX_ALT1b assms(2))
+ − 3747
+ − 3748
lemma POSIX_ALT_cases2:
+ − 3749
assumes "POSIX v (ALT r1 r2)" "\<turnstile> v : (ALT r1 r2)"
+ − 3750
shows "(\<exists>v1. v = Left v1 \<and> POSIX v1 r1) \<or> (\<exists>v2. v = Right v2 \<and> POSIX v2 r2)"
+ − 3751
using assms POSIX_ALT_cases by auto
+ − 3752
+ − 3753
lemma Prf_flat_empty:
+ − 3754
assumes "\<turnstile> v : r" "flat v = []"
+ − 3755
shows "nullable r"
+ − 3756
using assms
+ − 3757
apply(induct)
+ − 3758
apply(auto)
+ − 3759
done
+ − 3760
+ − 3761
lemma POSIX_proj:
+ − 3762
assumes "POSIX v r" "\<turnstile> v : r" "\<exists>s. flat v = c#s"
+ − 3763
shows "POSIX (projval r c v) (der c r)"
+ − 3764
using assms
+ − 3765
apply(induct r c v arbitrary: rule: projval.induct)
+ − 3766
defer
+ − 3767
defer
+ − 3768
defer
+ − 3769
defer
+ − 3770
apply(erule Prf.cases)
+ − 3771
apply(simp_all)[5]
+ − 3772
apply(erule Prf.cases)
+ − 3773
apply(simp_all)[5]
+ − 3774
apply(erule Prf.cases)
+ − 3775
apply(simp_all)[5]
+ − 3776
apply(erule Prf.cases)
+ − 3777
apply(simp_all)[5]
+ − 3778
apply(erule Prf.cases)
+ − 3779
apply(simp_all)[5]
+ − 3780
apply(erule Prf.cases)
+ − 3781
apply(simp_all)[5]
+ − 3782
apply(erule Prf.cases)
+ − 3783
apply(simp_all)[5]
+ − 3784
apply(erule Prf.cases)
+ − 3785
apply(simp_all)[5]
+ − 3786
apply(erule Prf.cases)
+ − 3787
apply(simp_all)[5]
+ − 3788
apply(erule Prf.cases)
+ − 3789
apply(simp_all)[5]
+ − 3790
apply(simp add: POSIX_def)
+ − 3791
apply(auto)[1]
+ − 3792
apply(erule Prf.cases)
+ − 3793
apply(simp_all)[5]
+ − 3794
oops
+ − 3795
+ − 3796
lemma POSIX_proj:
+ − 3797
assumes "POSIX v r" "\<turnstile> v : r" "\<exists>s. flat v = c#s"
+ − 3798
shows "POSIX (projval r c v) (der c r)"
+ − 3799
using assms
+ − 3800
apply(induct r arbitrary: c v rule: rexp.induct)
+ − 3801
apply(erule Prf.cases)
+ − 3802
apply(simp_all)[5]
+ − 3803
apply(erule Prf.cases)
+ − 3804
apply(simp_all)[5]
+ − 3805
apply(erule Prf.cases)
+ − 3806
apply(simp_all)[5]
+ − 3807
apply(simp add: POSIX_def)
+ − 3808
apply(auto)[1]
+ − 3809
apply(erule Prf.cases)
+ − 3810
apply(simp_all)[5]
+ − 3811
oops
+ − 3812
+ − 3813
lemma POSIX_proj:
+ − 3814
assumes "POSIX v r" "\<turnstile> v : r" "\<exists>s. flat v = c#s"
+ − 3815
shows "POSIX (projval r c v) (der c r)"
+ − 3816
using assms
+ − 3817
apply(induct r c v arbitrary: rule: projval.induct)
+ − 3818
defer
+ − 3819
defer
+ − 3820
defer
+ − 3821
defer
+ − 3822
apply(erule Prf.cases)
+ − 3823
apply(simp_all)[5]
+ − 3824
apply(erule Prf.cases)
+ − 3825
apply(simp_all)[5]
+ − 3826
apply(erule Prf.cases)
+ − 3827
apply(simp_all)[5]
+ − 3828
apply(erule Prf.cases)
+ − 3829
apply(simp_all)[5]
+ − 3830
apply(erule Prf.cases)
+ − 3831
apply(simp_all)[5]
+ − 3832
apply(erule Prf.cases)
+ − 3833
apply(simp_all)[5]
+ − 3834
apply(erule Prf.cases)
+ − 3835
apply(simp_all)[5]
+ − 3836
apply(erule Prf.cases)
+ − 3837
apply(simp_all)[5]
+ − 3838
apply(erule Prf.cases)
+ − 3839
apply(simp_all)[5]
+ − 3840
apply(erule Prf.cases)
+ − 3841
apply(simp_all)[5]
+ − 3842
apply(simp add: POSIX_def)
+ − 3843
apply(auto)[1]
+ − 3844
apply(erule Prf.cases)
+ − 3845
apply(simp_all)[5]
+ − 3846
oops
+ − 3847
+ − 3848
lemma Prf_inj:
+ − 3849
assumes "v1 \<succ>(der c r) v2" "\<turnstile> v1 : der c r" "\<turnstile> v2 : der c r" "flat v1 = flat v2"
+ − 3850
shows "(injval r c v1) \<succ>r (injval r c v2)"
+ − 3851
using assms
+ − 3852
apply(induct arbitrary: v1 v2 rule: der.induct)
+ − 3853
(* NULL case *)
+ − 3854
apply(simp)
+ − 3855
apply(erule ValOrd.cases)
+ − 3856
apply(simp_all)[8]
+ − 3857
(* EMPTY case *)
+ − 3858
apply(erule ValOrd.cases)
+ − 3859
apply(simp_all)[8]
+ − 3860
(* CHAR case *)
+ − 3861
apply(case_tac "c = c'")
+ − 3862
apply(simp)
+ − 3863
apply(erule ValOrd.cases)
+ − 3864
apply(simp_all)[8]
+ − 3865
apply(rule ValOrd.intros)
+ − 3866
apply(simp)
+ − 3867
apply(erule ValOrd.cases)
+ − 3868
apply(simp_all)[8]
+ − 3869
(* ALT case *)
+ − 3870
apply(simp)
+ − 3871
apply(erule ValOrd.cases)
+ − 3872
apply(simp_all)[8]
+ − 3873
apply(rule ValOrd.intros)
+ − 3874
apply(subst v4)
+ − 3875
apply(clarify)
+ − 3876
apply(rotate_tac 3)
+ − 3877
apply(erule Prf.cases)
+ − 3878
apply(simp_all)[5]
+ − 3879
apply(subst v4)
+ − 3880
apply(clarify)
+ − 3881
apply(rotate_tac 2)
+ − 3882
apply(erule Prf.cases)
+ − 3883
apply(simp_all)[5]
+ − 3884
apply(simp)
+ − 3885
apply(rule ValOrd.intros)
+ − 3886
apply(clarify)
+ − 3887
apply(rotate_tac 3)
+ − 3888
apply(erule Prf.cases)
+ − 3889
apply(simp_all)[5]
+ − 3890
apply(clarify)
+ − 3891
apply(erule Prf.cases)
+ − 3892
apply(simp_all)[5]
+ − 3893
apply(rule ValOrd.intros)
+ − 3894
apply(clarify)
+ − 3895
apply(erule Prf.cases)
+ − 3896
apply(simp_all)[5]
+ − 3897
apply(erule Prf.cases)
+ − 3898
apply(simp_all)[5]
+ − 3899
(* SEQ case*)
+ − 3900
apply(simp)
+ − 3901
apply(case_tac "nullable r1")
+ − 3902
defer
+ − 3903
apply(simp)
+ − 3904
apply(erule ValOrd.cases)
+ − 3905
apply(simp_all)[8]
+ − 3906
apply(clarify)
+ − 3907
apply(erule Prf.cases)
+ − 3908
apply(simp_all)[5]
+ − 3909
apply(erule Prf.cases)
+ − 3910
apply(simp_all)[5]
+ − 3911
apply(clarify)
+ − 3912
apply(rule ValOrd.intros)
+ − 3913
apply(simp)
+ − 3914
oops
+ − 3915
+ − 3916
+ − 3917
text {*
+ − 3918
Injection followed by projection is the identity.
+ − 3919
*}
+ − 3920
+ − 3921
lemma proj_inj_id:
+ − 3922
assumes "\<turnstile> v : der c r"
+ − 3923
shows "projval r c (injval r c v) = v"
+ − 3924
using assms
+ − 3925
apply(induct r arbitrary: c v rule: rexp.induct)
+ − 3926
apply(simp)
+ − 3927
apply(erule Prf.cases)
+ − 3928
apply(simp_all)[5]
+ − 3929
apply(simp)
+ − 3930
apply(erule Prf.cases)
+ − 3931
apply(simp_all)[5]
+ − 3932
apply(simp)
+ − 3933
apply(case_tac "c = char")
+ − 3934
apply(simp)
+ − 3935
apply(erule Prf.cases)
+ − 3936
apply(simp_all)[5]
+ − 3937
apply(simp)
+ − 3938
apply(erule Prf.cases)
+ − 3939
apply(simp_all)[5]
+ − 3940
defer
+ − 3941
apply(simp)
+ − 3942
apply(erule Prf.cases)
+ − 3943
apply(simp_all)[5]
+ − 3944
apply(simp)
+ − 3945
apply(case_tac "nullable rexp1")
+ − 3946
apply(simp)
+ − 3947
apply(erule Prf.cases)
+ − 3948
apply(simp_all)[5]
+ − 3949
apply(auto)[1]
+ − 3950
apply(erule Prf.cases)
+ − 3951
apply(simp_all)[5]
+ − 3952
apply(auto)[1]
+ − 3953
apply (metis list.distinct(1) v4)
+ − 3954
apply(auto)[1]
+ − 3955
apply (metis mkeps_flat)
+ − 3956
apply(auto)
+ − 3957
apply(erule Prf.cases)
+ − 3958
apply(simp_all)[5]
+ − 3959
apply(auto)[1]
+ − 3960
apply(simp add: v4)
+ − 3961
done
+ − 3962
+ − 3963
text {*
+ − 3964
+ − 3965
HERE: Crucial lemma that does not go through in the sequence case.
+ − 3966
+ − 3967
*}
+ − 3968
lemma v5:
+ − 3969
assumes "\<turnstile> v : der c r" "POSIX v (der c r)"
+ − 3970
shows "POSIX (injval r c v) r"
+ − 3971
using assms
+ − 3972
apply(induct arbitrary: v rule: der.induct)
+ − 3973
(* NULL case *)
+ − 3974
apply(simp)
+ − 3975
apply(erule Prf.cases)
+ − 3976
apply(simp_all)[5]
+ − 3977
(* EMPTY case *)
+ − 3978
apply(simp)
+ − 3979
apply(erule Prf.cases)
+ − 3980
apply(simp_all)[5]
+ − 3981
(* CHAR case *)
+ − 3982
apply(simp)
+ − 3983
apply(case_tac "c = c'")
+ − 3984
apply(auto simp add: POSIX_def)[1]
+ − 3985
apply(erule Prf.cases)
+ − 3986
apply(simp_all)[5]
+ − 3987
oops
+ − 3988
*)
+ − 3989
+ − 3990
+ − 3991
end