409
+ − 1
+ − 2
theory SizeBound5CT
428
+ − 3
imports "Lexer" "PDerivs"
409
+ − 4
begin
+ − 5
+ − 6
section \<open>Bit-Encodings\<close>
+ − 7
+ − 8
datatype bit = Z | S
+ − 9
+ − 10
fun code :: "val \<Rightarrow> bit list"
+ − 11
where
+ − 12
"code Void = []"
+ − 13
| "code (Char c) = []"
+ − 14
| "code (Left v) = Z # (code v)"
+ − 15
| "code (Right v) = S # (code v)"
+ − 16
| "code (Seq v1 v2) = (code v1) @ (code v2)"
+ − 17
| "code (Stars []) = [S]"
+ − 18
| "code (Stars (v # vs)) = (Z # code v) @ code (Stars vs)"
+ − 19
+ − 20
+ − 21
fun
+ − 22
Stars_add :: "val \<Rightarrow> val \<Rightarrow> val"
+ − 23
where
+ − 24
"Stars_add v (Stars vs) = Stars (v # vs)"
+ − 25
+ − 26
function
+ − 27
decode' :: "bit list \<Rightarrow> rexp \<Rightarrow> (val * bit list)"
+ − 28
where
+ − 29
"decode' bs ZERO = (undefined, bs)"
+ − 30
| "decode' bs ONE = (Void, bs)"
+ − 31
| "decode' bs (CH d) = (Char d, bs)"
+ − 32
| "decode' [] (ALT r1 r2) = (Void, [])"
+ − 33
| "decode' (Z # bs) (ALT r1 r2) = (let (v, bs') = decode' bs r1 in (Left v, bs'))"
+ − 34
| "decode' (S # bs) (ALT r1 r2) = (let (v, bs') = decode' bs r2 in (Right v, bs'))"
+ − 35
| "decode' bs (SEQ r1 r2) = (let (v1, bs') = decode' bs r1 in
+ − 36
let (v2, bs'') = decode' bs' r2 in (Seq v1 v2, bs''))"
+ − 37
| "decode' [] (STAR r) = (Void, [])"
+ − 38
| "decode' (S # bs) (STAR r) = (Stars [], bs)"
+ − 39
| "decode' (Z # bs) (STAR r) = (let (v, bs') = decode' bs r in
+ − 40
let (vs, bs'') = decode' bs' (STAR r)
+ − 41
in (Stars_add v vs, bs''))"
+ − 42
by pat_completeness auto
+ − 43
+ − 44
lemma decode'_smaller:
+ − 45
assumes "decode'_dom (bs, r)"
+ − 46
shows "length (snd (decode' bs r)) \<le> length bs"
+ − 47
using assms
+ − 48
apply(induct bs r)
+ − 49
apply(auto simp add: decode'.psimps split: prod.split)
+ − 50
using dual_order.trans apply blast
+ − 51
by (meson dual_order.trans le_SucI)
+ − 52
+ − 53
termination "decode'"
+ − 54
apply(relation "inv_image (measure(%cs. size cs) <*lex*> measure(%s. size s)) (%(ds,r). (r,ds))")
+ − 55
apply(auto dest!: decode'_smaller)
+ − 56
by (metis less_Suc_eq_le snd_conv)
+ − 57
+ − 58
definition
+ − 59
decode :: "bit list \<Rightarrow> rexp \<Rightarrow> val option"
+ − 60
where
+ − 61
"decode ds r \<equiv> (let (v, ds') = decode' ds r
+ − 62
in (if ds' = [] then Some v else None))"
+ − 63
+ − 64
lemma decode'_code_Stars:
+ − 65
assumes "\<forall>v\<in>set vs. \<Turnstile> v : r \<and> (\<forall>x. decode' (code v @ x) r = (v, x)) \<and> flat v \<noteq> []"
+ − 66
shows "decode' (code (Stars vs) @ ds) (STAR r) = (Stars vs, ds)"
+ − 67
using assms
+ − 68
apply(induct vs)
+ − 69
apply(auto)
+ − 70
done
+ − 71
+ − 72
lemma decode'_code:
+ − 73
assumes "\<Turnstile> v : r"
+ − 74
shows "decode' ((code v) @ ds) r = (v, ds)"
+ − 75
using assms
+ − 76
apply(induct v r arbitrary: ds)
+ − 77
apply(auto)
+ − 78
using decode'_code_Stars by blast
+ − 79
+ − 80
lemma decode_code:
+ − 81
assumes "\<Turnstile> v : r"
+ − 82
shows "decode (code v) r = Some v"
+ − 83
using assms unfolding decode_def
+ − 84
by (smt append_Nil2 decode'_code old.prod.case)
+ − 85
+ − 86
+ − 87
section {* Annotated Regular Expressions *}
+ − 88
+ − 89
datatype arexp =
+ − 90
AZERO
+ − 91
| AONE "bit list"
+ − 92
| ACHAR "bit list" char
+ − 93
| ASEQ "bit list" arexp arexp
+ − 94
| AALTs "bit list" "arexp list"
+ − 95
| ASTAR "bit list" arexp
+ − 96
+ − 97
abbreviation
+ − 98
"AALT bs r1 r2 \<equiv> AALTs bs [r1, r2]"
+ − 99
+ − 100
fun asize :: "arexp \<Rightarrow> nat" where
+ − 101
"asize AZERO = 1"
+ − 102
| "asize (AONE cs) = 1"
+ − 103
| "asize (ACHAR cs c) = 1"
+ − 104
| "asize (AALTs cs rs) = Suc (sum_list (map asize rs))"
+ − 105
| "asize (ASEQ cs r1 r2) = Suc (asize r1 + asize r2)"
+ − 106
| "asize (ASTAR cs r) = Suc (asize r)"
+ − 107
+ − 108
fun
+ − 109
erase :: "arexp \<Rightarrow> rexp"
+ − 110
where
+ − 111
"erase AZERO = ZERO"
+ − 112
| "erase (AONE _) = ONE"
+ − 113
| "erase (ACHAR _ c) = CH c"
+ − 114
| "erase (AALTs _ []) = ZERO"
+ − 115
| "erase (AALTs _ [r]) = (erase r)"
+ − 116
| "erase (AALTs bs (r#rs)) = ALT (erase r) (erase (AALTs bs rs))"
+ − 117
| "erase (ASEQ _ r1 r2) = SEQ (erase r1) (erase r2)"
+ − 118
| "erase (ASTAR _ r) = STAR (erase r)"
+ − 119
+ − 120
+ − 121
fun fuse :: "bit list \<Rightarrow> arexp \<Rightarrow> arexp" where
+ − 122
"fuse bs AZERO = AZERO"
+ − 123
| "fuse bs (AONE cs) = AONE (bs @ cs)"
+ − 124
| "fuse bs (ACHAR cs c) = ACHAR (bs @ cs) c"
+ − 125
| "fuse bs (AALTs cs rs) = AALTs (bs @ cs) rs"
+ − 126
| "fuse bs (ASEQ cs r1 r2) = ASEQ (bs @ cs) r1 r2"
+ − 127
| "fuse bs (ASTAR cs r) = ASTAR (bs @ cs) r"
+ − 128
+ − 129
lemma fuse_append:
+ − 130
shows "fuse (bs1 @ bs2) r = fuse bs1 (fuse bs2 r)"
+ − 131
apply(induct r)
+ − 132
apply(auto)
+ − 133
done
+ − 134
+ − 135
+ − 136
fun intern :: "rexp \<Rightarrow> arexp" where
+ − 137
"intern ZERO = AZERO"
+ − 138
| "intern ONE = AONE []"
+ − 139
| "intern (CH c) = ACHAR [] c"
+ − 140
| "intern (ALT r1 r2) = AALT [] (fuse [Z] (intern r1))
+ − 141
(fuse [S] (intern r2))"
+ − 142
| "intern (SEQ r1 r2) = ASEQ [] (intern r1) (intern r2)"
+ − 143
| "intern (STAR r) = ASTAR [] (intern r)"
+ − 144
+ − 145
+ − 146
fun retrieve :: "arexp \<Rightarrow> val \<Rightarrow> bit list" where
+ − 147
"retrieve (AONE bs) Void = bs"
+ − 148
| "retrieve (ACHAR bs c) (Char d) = bs"
+ − 149
| "retrieve (AALTs bs [r]) v = bs @ retrieve r v"
+ − 150
| "retrieve (AALTs bs (r#rs)) (Left v) = bs @ retrieve r v"
+ − 151
| "retrieve (AALTs bs (r#rs)) (Right v) = bs @ retrieve (AALTs [] rs) v"
+ − 152
| "retrieve (ASEQ bs r1 r2) (Seq v1 v2) = bs @ retrieve r1 v1 @ retrieve r2 v2"
+ − 153
| "retrieve (ASTAR bs r) (Stars []) = bs @ [S]"
+ − 154
| "retrieve (ASTAR bs r) (Stars (v#vs)) =
+ − 155
bs @ [Z] @ retrieve r v @ retrieve (ASTAR [] r) (Stars vs)"
+ − 156
+ − 157
+ − 158
+ − 159
fun
+ − 160
bnullable :: "arexp \<Rightarrow> bool"
+ − 161
where
+ − 162
"bnullable (AZERO) = False"
+ − 163
| "bnullable (AONE bs) = True"
+ − 164
| "bnullable (ACHAR bs c) = False"
+ − 165
| "bnullable (AALTs bs rs) = (\<exists>r \<in> set rs. bnullable r)"
+ − 166
| "bnullable (ASEQ bs r1 r2) = (bnullable r1 \<and> bnullable r2)"
+ − 167
| "bnullable (ASTAR bs r) = True"
+ − 168
+ − 169
abbreviation
+ − 170
bnullables :: "arexp list \<Rightarrow> bool"
+ − 171
where
+ − 172
"bnullables rs \<equiv> (\<exists>r \<in> set rs. bnullable r)"
+ − 173
+ − 174
fun
+ − 175
bmkeps :: "arexp \<Rightarrow> bit list" and
+ − 176
bmkepss :: "arexp list \<Rightarrow> bit list"
+ − 177
where
+ − 178
"bmkeps(AONE bs) = bs"
+ − 179
| "bmkeps(ASEQ bs r1 r2) = bs @ (bmkeps r1) @ (bmkeps r2)"
+ − 180
| "bmkeps(AALTs bs rs) = bs @ (bmkepss rs)"
+ − 181
| "bmkeps(ASTAR bs r) = bs @ [S]"
+ − 182
| "bmkepss [] = []"
+ − 183
| "bmkepss (r # rs) = (if bnullable(r) then (bmkeps r) else (bmkepss rs))"
+ − 184
+ − 185
lemma bmkepss1:
+ − 186
assumes "\<not> bnullables rs1"
+ − 187
shows "bmkepss (rs1 @ rs2) = bmkepss rs2"
+ − 188
using assms
+ − 189
by (induct rs1) (auto)
+ − 190
+ − 191
lemma bmkepss2:
+ − 192
assumes "bnullables rs1"
+ − 193
shows "bmkepss (rs1 @ rs2) = bmkepss rs1"
+ − 194
using assms
+ − 195
by (induct rs1) (auto)
+ − 196
+ − 197
+ − 198
fun
+ − 199
bder :: "char \<Rightarrow> arexp \<Rightarrow> arexp"
+ − 200
where
+ − 201
"bder c (AZERO) = AZERO"
+ − 202
| "bder c (AONE bs) = AZERO"
+ − 203
| "bder c (ACHAR bs d) = (if c = d then AONE bs else AZERO)"
+ − 204
| "bder c (AALTs bs rs) = AALTs bs (map (bder c) rs)"
+ − 205
| "bder c (ASEQ bs r1 r2) =
+ − 206
(if bnullable r1
+ − 207
then AALT bs (ASEQ [] (bder c r1) r2) (fuse (bmkeps r1) (bder c r2))
+ − 208
else ASEQ bs (bder c r1) r2)"
+ − 209
| "bder c (ASTAR bs r) = ASEQ bs (fuse [Z] (bder c r)) (ASTAR [] r)"
+ − 210
+ − 211
+ − 212
fun
+ − 213
bders :: "arexp \<Rightarrow> string \<Rightarrow> arexp"
+ − 214
where
+ − 215
"bders r [] = r"
+ − 216
| "bders r (c#s) = bders (bder c r) s"
+ − 217
+ − 218
lemma bders_append:
+ − 219
"bders c (s1 @ s2) = bders (bders c s1) s2"
+ − 220
apply(induct s1 arbitrary: c s2)
+ − 221
apply(simp_all)
+ − 222
done
+ − 223
+ − 224
lemma bnullable_correctness:
+ − 225
shows "nullable (erase r) = bnullable r"
+ − 226
apply(induct r rule: erase.induct)
+ − 227
apply(simp_all)
+ − 228
done
+ − 229
+ − 230
lemma erase_fuse:
+ − 231
shows "erase (fuse bs r) = erase r"
+ − 232
apply(induct r rule: erase.induct)
+ − 233
apply(simp_all)
+ − 234
done
+ − 235
+ − 236
lemma erase_intern [simp]:
+ − 237
shows "erase (intern r) = r"
+ − 238
apply(induct r)
+ − 239
apply(simp_all add: erase_fuse)
+ − 240
done
+ − 241
+ − 242
lemma erase_bder [simp]:
+ − 243
shows "erase (bder a r) = der a (erase r)"
+ − 244
apply(induct r rule: erase.induct)
+ − 245
apply(simp_all add: erase_fuse bnullable_correctness)
+ − 246
done
+ − 247
+ − 248
lemma erase_bders [simp]:
+ − 249
shows "erase (bders r s) = ders s (erase r)"
+ − 250
apply(induct s arbitrary: r )
+ − 251
apply(simp_all)
+ − 252
done
+ − 253
+ − 254
lemma bnullable_fuse:
+ − 255
shows "bnullable (fuse bs r) = bnullable r"
+ − 256
apply(induct r arbitrary: bs)
+ − 257
apply(auto)
+ − 258
done
+ − 259
+ − 260
lemma retrieve_encode_STARS:
+ − 261
assumes "\<forall>v\<in>set vs. \<Turnstile> v : r \<and> code v = retrieve (intern r) v"
+ − 262
shows "code (Stars vs) = retrieve (ASTAR [] (intern r)) (Stars vs)"
+ − 263
using assms
+ − 264
apply(induct vs)
+ − 265
apply(simp_all)
+ − 266
done
+ − 267
+ − 268
lemma retrieve_fuse2:
+ − 269
assumes "\<Turnstile> v : (erase r)"
+ − 270
shows "retrieve (fuse bs r) v = bs @ retrieve r v"
+ − 271
using assms
+ − 272
apply(induct r arbitrary: v bs)
+ − 273
apply(auto elim: Prf_elims)[4]
+ − 274
apply(case_tac x2a)
+ − 275
apply(simp)
+ − 276
using Prf_elims(1) apply blast
+ − 277
apply(case_tac x2a)
+ − 278
apply(simp)
+ − 279
apply(simp)
+ − 280
apply(case_tac list)
+ − 281
apply(simp)
+ − 282
apply(simp)
+ − 283
apply (smt (verit, best) Prf_elims(3) append_assoc retrieve.simps(4) retrieve.simps(5))
+ − 284
apply(simp)
+ − 285
using retrieve_encode_STARS
+ − 286
apply(auto elim!: Prf_elims)[1]
+ − 287
apply(case_tac vs)
+ − 288
apply(simp)
+ − 289
apply(simp)
+ − 290
done
+ − 291
+ − 292
lemma retrieve_fuse:
+ − 293
assumes "\<Turnstile> v : r"
+ − 294
shows "retrieve (fuse bs (intern r)) v = bs @ retrieve (intern r) v"
+ − 295
using assms
+ − 296
by (simp_all add: retrieve_fuse2)
+ − 297
+ − 298
+ − 299
lemma retrieve_code:
+ − 300
assumes "\<Turnstile> v : r"
+ − 301
shows "code v = retrieve (intern r) v"
+ − 302
using assms
+ − 303
apply(induct v r )
+ − 304
apply(simp_all add: retrieve_fuse retrieve_encode_STARS)
+ − 305
done
+ − 306
+ − 307
+ − 308
lemma retrieve_AALTs_bnullable1:
+ − 309
assumes "bnullable r"
+ − 310
shows "retrieve (AALTs bs (r # rs)) (mkeps (erase (AALTs bs (r # rs))))
+ − 311
= bs @ retrieve r (mkeps (erase r))"
+ − 312
using assms
+ − 313
apply(case_tac rs)
+ − 314
apply(auto simp add: bnullable_correctness)
+ − 315
done
+ − 316
+ − 317
lemma retrieve_AALTs_bnullable2:
+ − 318
assumes "\<not>bnullable r" "bnullables rs"
+ − 319
shows "retrieve (AALTs bs (r # rs)) (mkeps (erase (AALTs bs (r # rs))))
+ − 320
= retrieve (AALTs bs rs) (mkeps (erase (AALTs bs rs)))"
+ − 321
using assms
+ − 322
apply(induct rs arbitrary: r bs)
+ − 323
apply(auto)
+ − 324
using bnullable_correctness apply blast
+ − 325
apply(case_tac rs)
+ − 326
apply(auto)
+ − 327
using bnullable_correctness apply blast
+ − 328
apply(case_tac rs)
+ − 329
apply(auto)
+ − 330
done
+ − 331
+ − 332
lemma bmkeps_retrieve_AALTs:
+ − 333
assumes "\<forall>r \<in> set rs. bnullable r \<longrightarrow> bmkeps r = retrieve r (mkeps (erase r))"
+ − 334
"bnullables rs"
+ − 335
shows "bs @ bmkepss rs = retrieve (AALTs bs rs) (mkeps (erase (AALTs bs rs)))"
+ − 336
using assms
+ − 337
apply(induct rs arbitrary: bs)
+ − 338
apply(auto)
+ − 339
using retrieve_AALTs_bnullable1 apply presburger
+ − 340
apply (metis retrieve_AALTs_bnullable2)
+ − 341
apply (simp add: retrieve_AALTs_bnullable1)
+ − 342
by (metis retrieve_AALTs_bnullable2)
+ − 343
+ − 344
+ − 345
lemma bmkeps_retrieve:
+ − 346
assumes "bnullable r"
+ − 347
shows "bmkeps r = retrieve r (mkeps (erase r))"
+ − 348
using assms
+ − 349
apply(induct r)
+ − 350
apply(auto)
+ − 351
using bmkeps_retrieve_AALTs by auto
+ − 352
+ − 353
lemma bder_retrieve:
+ − 354
assumes "\<Turnstile> v : der c (erase r)"
+ − 355
shows "retrieve (bder c r) v = retrieve r (injval (erase r) c v)"
+ − 356
using assms
+ − 357
apply(induct r arbitrary: v rule: erase.induct)
+ − 358
using Prf_elims(1) apply auto[1]
+ − 359
using Prf_elims(1) apply auto[1]
+ − 360
apply(auto)[1]
+ − 361
apply (metis Prf_elims(4) injval.simps(1) retrieve.simps(1) retrieve.simps(2))
+ − 362
using Prf_elims(1) apply blast
+ − 363
(* AALTs case *)
+ − 364
apply(simp)
+ − 365
apply(erule Prf_elims)
+ − 366
apply(simp)
+ − 367
apply(simp)
+ − 368
apply(rename_tac "r\<^sub>1" "r\<^sub>2" rs v)
+ − 369
apply(erule Prf_elims)
+ − 370
apply(simp)
+ − 371
apply(simp)
+ − 372
apply(case_tac rs)
+ − 373
apply(simp)
+ − 374
apply(simp)
+ − 375
using Prf_elims(3) apply fastforce
+ − 376
(* ASEQ case *)
+ − 377
apply(simp)
+ − 378
apply(case_tac "nullable (erase r1)")
+ − 379
apply(simp)
+ − 380
apply(erule Prf_elims)
+ − 381
using Prf_elims(2) bnullable_correctness apply force
+ − 382
apply (simp add: bmkeps_retrieve bnullable_correctness retrieve_fuse2)
+ − 383
apply (simp add: bmkeps_retrieve bnullable_correctness retrieve_fuse2)
+ − 384
using Prf_elims(2) apply force
+ − 385
(* ASTAR case *)
+ − 386
apply(rename_tac bs r v)
+ − 387
apply(simp)
+ − 388
apply(erule Prf_elims)
+ − 389
apply(clarify)
+ − 390
apply(erule Prf_elims)
+ − 391
apply(clarify)
+ − 392
by (simp add: retrieve_fuse2)
+ − 393
+ − 394
+ − 395
lemma MAIN_decode:
+ − 396
assumes "\<Turnstile> v : ders s r"
+ − 397
shows "Some (flex r id s v) = decode (retrieve (bders (intern r) s) v) r"
+ − 398
using assms
+ − 399
proof (induct s arbitrary: v rule: rev_induct)
+ − 400
case Nil
+ − 401
have "\<Turnstile> v : ders [] r" by fact
+ − 402
then have "\<Turnstile> v : r" by simp
+ − 403
then have "Some v = decode (retrieve (intern r) v) r"
+ − 404
using decode_code retrieve_code by auto
+ − 405
then show "Some (flex r id [] v) = decode (retrieve (bders (intern r) []) v) r"
+ − 406
by simp
+ − 407
next
+ − 408
case (snoc c s v)
+ − 409
have IH: "\<And>v. \<Turnstile> v : ders s r \<Longrightarrow>
+ − 410
Some (flex r id s v) = decode (retrieve (bders (intern r) s) v) r" by fact
+ − 411
have asm: "\<Turnstile> v : ders (s @ [c]) r" by fact
+ − 412
then have asm2: "\<Turnstile> injval (ders s r) c v : ders s r"
+ − 413
by (simp add: Prf_injval ders_append)
+ − 414
have "Some (flex r id (s @ [c]) v) = Some (flex r id s (injval (ders s r) c v))"
+ − 415
by (simp add: flex_append)
+ − 416
also have "... = decode (retrieve (bders (intern r) s) (injval (ders s r) c v)) r"
+ − 417
using asm2 IH by simp
+ − 418
also have "... = decode (retrieve (bder c (bders (intern r) s)) v) r"
+ − 419
using asm by (simp_all add: bder_retrieve ders_append)
+ − 420
finally show "Some (flex r id (s @ [c]) v) =
+ − 421
decode (retrieve (bders (intern r) (s @ [c])) v) r" by (simp add: bders_append)
+ − 422
qed
+ − 423
+ − 424
definition blexer where
+ − 425
"blexer r s \<equiv> if bnullable (bders (intern r) s) then
+ − 426
decode (bmkeps (bders (intern r) s)) r else None"
+ − 427
+ − 428
lemma blexer_correctness:
+ − 429
shows "blexer r s = lexer r s"
+ − 430
proof -
+ − 431
{ define bds where "bds \<equiv> bders (intern r) s"
+ − 432
define ds where "ds \<equiv> ders s r"
+ − 433
assume asm: "nullable ds"
+ − 434
have era: "erase bds = ds"
+ − 435
unfolding ds_def bds_def by simp
+ − 436
have mke: "\<Turnstile> mkeps ds : ds"
+ − 437
using asm by (simp add: mkeps_nullable)
+ − 438
have "decode (bmkeps bds) r = decode (retrieve bds (mkeps ds)) r"
+ − 439
using bmkeps_retrieve
+ − 440
using asm era
+ − 441
using bnullable_correctness by force
+ − 442
also have "... = Some (flex r id s (mkeps ds))"
+ − 443
using mke by (simp_all add: MAIN_decode ds_def bds_def)
+ − 444
finally have "decode (bmkeps bds) r = Some (flex r id s (mkeps ds))"
+ − 445
unfolding bds_def ds_def .
+ − 446
}
+ − 447
then show "blexer r s = lexer r s"
+ − 448
unfolding blexer_def lexer_flex
+ − 449
by (auto simp add: bnullable_correctness[symmetric])
+ − 450
qed
+ − 451
+ − 452
+ − 453
fun distinctBy :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b set \<Rightarrow> 'a list"
+ − 454
where
+ − 455
"distinctBy [] f acc = []"
+ − 456
| "distinctBy (x#xs) f acc =
+ − 457
(if (f x) \<in> acc then distinctBy xs f acc
+ − 458
else x # (distinctBy xs f ({f x} \<union> acc)))"
+ − 459
+ − 460
+ − 461
+ − 462
fun flts :: "arexp list \<Rightarrow> arexp list"
+ − 463
where
+ − 464
"flts [] = []"
+ − 465
| "flts (AZERO # rs) = flts rs"
+ − 466
| "flts ((AALTs bs rs1) # rs) = (map (fuse bs) rs1) @ flts rs"
+ − 467
| "flts (r1 # rs) = r1 # flts rs"
+ − 468
+ − 469
+ − 470
+ − 471
fun bsimp_ASEQ :: "bit list \<Rightarrow> arexp \<Rightarrow> arexp \<Rightarrow> arexp"
+ − 472
where
+ − 473
"bsimp_ASEQ _ AZERO _ = AZERO"
+ − 474
| "bsimp_ASEQ _ _ AZERO = AZERO"
+ − 475
| "bsimp_ASEQ bs1 (AONE bs2) r2 = fuse (bs1 @ bs2) r2"
+ − 476
| "bsimp_ASEQ bs1 r1 r2 = ASEQ bs1 r1 r2"
+ − 477
+ − 478
lemma bsimp_ASEQ0[simp]:
+ − 479
shows "bsimp_ASEQ bs r1 AZERO = AZERO"
+ − 480
by (case_tac r1)(simp_all)
+ − 481
+ − 482
lemma bsimp_ASEQ1:
+ − 483
assumes "r1 \<noteq> AZERO" "r2 \<noteq> AZERO" "\<nexists>bs. r1 = AONE bs"
+ − 484
shows "bsimp_ASEQ bs r1 r2 = ASEQ bs r1 r2"
+ − 485
using assms
+ − 486
apply(induct bs r1 r2 rule: bsimp_ASEQ.induct)
+ − 487
apply(auto)
+ − 488
done
+ − 489
+ − 490
lemma bsimp_ASEQ2[simp]:
+ − 491
shows "bsimp_ASEQ bs1 (AONE bs2) r2 = fuse (bs1 @ bs2) r2"
+ − 492
by (case_tac r2) (simp_all)
+ − 493
+ − 494
+ − 495
fun bsimp_AALTs :: "bit list \<Rightarrow> arexp list \<Rightarrow> arexp"
+ − 496
where
+ − 497
"bsimp_AALTs _ [] = AZERO"
+ − 498
| "bsimp_AALTs bs1 [r] = fuse bs1 r"
+ − 499
| "bsimp_AALTs bs1 rs = AALTs bs1 rs"
+ − 500
+ − 501
+ − 502
fun bsimp :: "arexp \<Rightarrow> arexp"
+ − 503
where
+ − 504
"bsimp (ASEQ bs1 r1 r2) = bsimp_ASEQ bs1 (bsimp r1) (bsimp r2)"
+ − 505
| "bsimp (AALTs bs1 rs) = bsimp_AALTs bs1 (distinctBy (flts (map bsimp rs)) erase {}) "
+ − 506
| "bsimp r = r"
+ − 507
+ − 508
+ − 509
fun
+ − 510
bders_simp :: "arexp \<Rightarrow> string \<Rightarrow> arexp"
+ − 511
where
+ − 512
"bders_simp r [] = r"
+ − 513
| "bders_simp r (c # s) = bders_simp (bsimp (bder c r)) s"
+ − 514
+ − 515
definition blexer_simp where
+ − 516
"blexer_simp r s \<equiv> if bnullable (bders_simp (intern r) s) then
+ − 517
decode (bmkeps (bders_simp (intern r) s)) r else None"
+ − 518
+ − 519
+ − 520
+ − 521
lemma bders_simp_append:
+ − 522
shows "bders_simp r (s1 @ s2) = bders_simp (bders_simp r s1) s2"
+ − 523
apply(induct s1 arbitrary: r s2)
+ − 524
apply(simp_all)
+ − 525
done
+ − 526
+ − 527
+ − 528
lemma bmkeps_fuse:
+ − 529
assumes "bnullable r"
+ − 530
shows "bmkeps (fuse bs r) = bs @ bmkeps r"
+ − 531
using assms
+ − 532
by (metis bmkeps_retrieve bnullable_correctness erase_fuse mkeps_nullable retrieve_fuse2)
+ − 533
+ − 534
lemma bmkepss_fuse:
+ − 535
assumes "bnullables rs"
+ − 536
shows "bmkepss (map (fuse bs) rs) = bs @ bmkepss rs"
+ − 537
using assms
+ − 538
apply(induct rs arbitrary: bs)
+ − 539
apply(auto simp add: bmkeps_fuse bnullable_fuse)
+ − 540
done
+ − 541
+ − 542
lemma bder_fuse:
+ − 543
shows "bder c (fuse bs a) = fuse bs (bder c a)"
+ − 544
apply(induct a arbitrary: bs c)
+ − 545
apply(simp_all)
+ − 546
done
+ − 547
+ − 548
+ − 549
+ − 550
+ − 551
inductive
+ − 552
rrewrite:: "arexp \<Rightarrow> arexp \<Rightarrow> bool" ("_ \<leadsto> _" [99, 99] 99)
+ − 553
and
+ − 554
srewrite:: "arexp list \<Rightarrow> arexp list \<Rightarrow> bool" (" _ s\<leadsto> _" [100, 100] 100)
+ − 555
where
+ − 556
bs1: "ASEQ bs AZERO r2 \<leadsto> AZERO"
+ − 557
| bs2: "ASEQ bs r1 AZERO \<leadsto> AZERO"
+ − 558
| bs3: "ASEQ bs1 (AONE bs2) r \<leadsto> fuse (bs1@bs2) r"
+ − 559
| bs4: "r1 \<leadsto> r2 \<Longrightarrow> ASEQ bs r1 r3 \<leadsto> ASEQ bs r2 r3"
+ − 560
| bs5: "r3 \<leadsto> r4 \<Longrightarrow> ASEQ bs r1 r3 \<leadsto> ASEQ bs r1 r4"
+ − 561
| bs6: "AALTs bs [] \<leadsto> AZERO"
+ − 562
| bs7: "AALTs bs [r] \<leadsto> fuse bs r"
+ − 563
| bs8: "rs1 s\<leadsto> rs2 \<Longrightarrow> AALTs bs rs1 \<leadsto> AALTs bs rs2"
+ − 564
(*| ss1: "[] s\<leadsto> []"*)
+ − 565
| ss2: "rs1 s\<leadsto> rs2 \<Longrightarrow> (r # rs1) s\<leadsto> (r # rs2)"
+ − 566
| ss3: "r1 \<leadsto> r2 \<Longrightarrow> (r1 # rs) s\<leadsto> (r2 # rs)"
+ − 567
| ss4: "(AZERO # rs) s\<leadsto> rs"
+ − 568
| ss5: "(AALTs bs1 rs1 # rsb) s\<leadsto> ((map (fuse bs1) rs1) @ rsb)"
+ − 569
| ss6: "erase a1 = erase a2 \<Longrightarrow> (rsa@[a1]@rsb@[a2]@rsc) s\<leadsto> (rsa@[a1]@rsb@rsc)"
+ − 570
+ − 571
+ − 572
inductive
+ − 573
rrewrites:: "arexp \<Rightarrow> arexp \<Rightarrow> bool" ("_ \<leadsto>* _" [100, 100] 100)
+ − 574
where
+ − 575
rs1[intro, simp]:"r \<leadsto>* r"
+ − 576
| rs2[intro]: "\<lbrakk>r1 \<leadsto>* r2; r2 \<leadsto> r3\<rbrakk> \<Longrightarrow> r1 \<leadsto>* r3"
+ − 577
+ − 578
inductive
+ − 579
srewrites:: "arexp list \<Rightarrow> arexp list \<Rightarrow> bool" ("_ s\<leadsto>* _" [100, 100] 100)
+ − 580
where
+ − 581
sss1[intro, simp]:"rs s\<leadsto>* rs"
+ − 582
| sss2[intro]: "\<lbrakk>rs1 s\<leadsto> rs2; rs2 s\<leadsto>* rs3\<rbrakk> \<Longrightarrow> rs1 s\<leadsto>* rs3"
+ − 583
+ − 584
+ − 585
lemma r_in_rstar:
+ − 586
shows "r1 \<leadsto> r2 \<Longrightarrow> r1 \<leadsto>* r2"
+ − 587
using rrewrites.intros(1) rrewrites.intros(2) by blast
+ − 588
+ − 589
lemma rrewrites_trans[trans]:
+ − 590
assumes a1: "r1 \<leadsto>* r2" and a2: "r2 \<leadsto>* r3"
+ − 591
shows "r1 \<leadsto>* r3"
+ − 592
using a2 a1
+ − 593
apply(induct r2 r3 arbitrary: r1 rule: rrewrites.induct)
+ − 594
apply(auto)
+ − 595
done
+ − 596
+ − 597
lemma srewrites_trans[trans]:
+ − 598
assumes a1: "r1 s\<leadsto>* r2" and a2: "r2 s\<leadsto>* r3"
+ − 599
shows "r1 s\<leadsto>* r3"
+ − 600
using a1 a2
+ − 601
apply(induct r1 r2 arbitrary: r3 rule: srewrites.induct)
+ − 602
apply(auto)
+ − 603
done
+ − 604
+ − 605
+ − 606
+ − 607
lemma contextrewrites0:
+ − 608
"rs1 s\<leadsto>* rs2 \<Longrightarrow> AALTs bs rs1 \<leadsto>* AALTs bs rs2"
+ − 609
apply(induct rs1 rs2 rule: srewrites.inducts)
+ − 610
apply simp
+ − 611
using bs8 r_in_rstar rrewrites_trans by blast
+ − 612
+ − 613
lemma contextrewrites1:
+ − 614
"r \<leadsto>* r' \<Longrightarrow> AALTs bs (r # rs) \<leadsto>* AALTs bs (r' # rs)"
+ − 615
apply(induct r r' rule: rrewrites.induct)
+ − 616
apply simp
+ − 617
using bs8 ss3 by blast
+ − 618
+ − 619
lemma srewrite1:
+ − 620
shows "rs1 s\<leadsto> rs2 \<Longrightarrow> (rs @ rs1) s\<leadsto> (rs @ rs2)"
+ − 621
apply(induct rs)
+ − 622
apply(auto)
+ − 623
using ss2 by auto
+ − 624
+ − 625
lemma srewrites1:
+ − 626
shows "rs1 s\<leadsto>* rs2 \<Longrightarrow> (rs @ rs1) s\<leadsto>* (rs @ rs2)"
+ − 627
apply(induct rs1 rs2 rule: srewrites.induct)
+ − 628
apply(auto)
+ − 629
using srewrite1 by blast
+ − 630
+ − 631
lemma srewrite2:
+ − 632
shows "r1 \<leadsto> r2 \<Longrightarrow> True"
+ − 633
and "rs1 s\<leadsto> rs2 \<Longrightarrow> (rs1 @ rs) s\<leadsto>* (rs2 @ rs)"
+ − 634
apply(induct rule: rrewrite_srewrite.inducts)
+ − 635
apply(auto)
+ − 636
apply (metis append_Cons append_Nil srewrites1)
+ − 637
apply(meson srewrites.simps ss3)
+ − 638
apply (meson srewrites.simps ss4)
+ − 639
apply (meson srewrites.simps ss5)
+ − 640
by (metis append_Cons append_Nil srewrites.simps ss6)
+ − 641
+ − 642
+ − 643
lemma srewrites3:
+ − 644
shows "rs1 s\<leadsto>* rs2 \<Longrightarrow> (rs1 @ rs) s\<leadsto>* (rs2 @ rs)"
+ − 645
apply(induct rs1 rs2 arbitrary: rs rule: srewrites.induct)
+ − 646
apply(auto)
+ − 647
by (meson srewrite2(2) srewrites_trans)
+ − 648
+ − 649
(*
+ − 650
lemma srewrites4:
+ − 651
assumes "rs3 s\<leadsto>* rs4" "rs1 s\<leadsto>* rs2"
+ − 652
shows "(rs1 @ rs3) s\<leadsto>* (rs2 @ rs4)"
+ − 653
using assms
+ − 654
apply(induct rs3 rs4 arbitrary: rs1 rs2 rule: srewrites.induct)
+ − 655
apply (simp add: srewrites3)
+ − 656
using srewrite1 by blast
+ − 657
*)
+ − 658
+ − 659
lemma srewrites6:
+ − 660
assumes "r1 \<leadsto>* r2"
+ − 661
shows "[r1] s\<leadsto>* [r2]"
+ − 662
using assms
+ − 663
apply(induct r1 r2 rule: rrewrites.induct)
+ − 664
apply(auto)
+ − 665
by (meson srewrites.simps srewrites_trans ss3)
+ − 666
+ − 667
lemma srewrites7:
+ − 668
assumes "rs3 s\<leadsto>* rs4" "r1 \<leadsto>* r2"
+ − 669
shows "(r1 # rs3) s\<leadsto>* (r2 # rs4)"
+ − 670
using assms
+ − 671
by (smt (verit, del_insts) append.simps srewrites1 srewrites3 srewrites6 srewrites_trans)
+ − 672
+ − 673
lemma ss6_stronger_aux:
+ − 674
shows "(rs1 @ rs2) s\<leadsto>* (rs1 @ distinctBy rs2 erase (set (map erase rs1)))"
+ − 675
apply(induct rs2 arbitrary: rs1)
+ − 676
apply(auto)
+ − 677
apply (smt (verit, best) append.assoc append.right_neutral append_Cons append_Nil split_list srewrite2(2) srewrites_trans ss6)
+ − 678
apply(drule_tac x="rs1 @ [a]" in meta_spec)
+ − 679
apply(simp)
+ − 680
done
+ − 681
+ − 682
lemma ss6_stronger:
+ − 683
shows "rs1 s\<leadsto>* distinctBy rs1 erase {}"
+ − 684
using ss6_stronger_aux[of "[]" _] by auto
+ − 685
+ − 686
lemma rewrite_preserves_fuse:
+ − 687
shows "r2 \<leadsto> r3 \<Longrightarrow> fuse bs r2 \<leadsto> fuse bs r3"
+ − 688
and "rs2 s\<leadsto> rs3 \<Longrightarrow> map (fuse bs) rs2 s\<leadsto> map (fuse bs) rs3"
+ − 689
proof(induct rule: rrewrite_srewrite.inducts)
+ − 690
case (bs3 bs1 bs2 r)
+ − 691
then show "fuse bs (ASEQ bs1 (AONE bs2) r) \<leadsto> fuse bs (fuse (bs1 @ bs2) r)"
+ − 692
by (metis fuse.simps(5) fuse_append rrewrite_srewrite.bs3)
+ − 693
next
+ − 694
case (bs7 bs1 r)
+ − 695
then show "fuse bs (AALTs bs1 [r]) \<leadsto> fuse bs (fuse bs1 r)"
+ − 696
by (metis fuse.simps(4) fuse_append rrewrite_srewrite.bs7)
+ − 697
next
+ − 698
case (ss2 rs1 rs2 r)
+ − 699
then show "map (fuse bs) (r # rs1) s\<leadsto> map (fuse bs) (r # rs2)"
+ − 700
by (simp add: rrewrite_srewrite.ss2)
+ − 701
next
+ − 702
case (ss3 r1 r2 rs)
+ − 703
then show "map (fuse bs) (r1 # rs) s\<leadsto> map (fuse bs) (r2 # rs)"
+ − 704
by (simp add: rrewrite_srewrite.ss3)
+ − 705
next
+ − 706
case (ss5 bs1 rs1 rsb)
+ − 707
have "map (fuse bs) (AALTs bs1 rs1 # rsb) = AALTs (bs @ bs1) rs1 # (map (fuse bs) rsb)" by simp
+ − 708
also have "... s\<leadsto> ((map (fuse (bs @ bs1)) rs1) @ (map (fuse bs) rsb))"
+ − 709
by (simp add: rrewrite_srewrite.ss5)
+ − 710
finally show "map (fuse bs) (AALTs bs1 rs1 # rsb) s\<leadsto> map (fuse bs) (map (fuse bs1) rs1 @ rsb)"
+ − 711
by (simp add: comp_def fuse_append)
+ − 712
next
+ − 713
case (ss6 a1 a2 rsa rsb rsc)
+ − 714
then show "map (fuse bs) (rsa @ [a1] @ rsb @ [a2] @ rsc) s\<leadsto> map (fuse bs) (rsa @ [a1] @ rsb @ rsc)"
+ − 715
apply(simp)
+ − 716
apply(rule rrewrite_srewrite.ss6[simplified])
+ − 717
apply(simp add: erase_fuse)
+ − 718
done
+ − 719
qed (auto intro: rrewrite_srewrite.intros)
+ − 720
+ − 721
lemma rewrites_fuse:
+ − 722
assumes "r1 \<leadsto>* r2"
+ − 723
shows "fuse bs r1 \<leadsto>* fuse bs r2"
+ − 724
using assms
+ − 725
apply(induction r1 r2 arbitrary: bs rule: rrewrites.induct)
+ − 726
apply(auto intro: rewrite_preserves_fuse)
+ − 727
done
+ − 728
+ − 729
+ − 730
lemma star_seq:
+ − 731
assumes "r1 \<leadsto>* r2"
+ − 732
shows "ASEQ bs r1 r3 \<leadsto>* ASEQ bs r2 r3"
+ − 733
using assms
+ − 734
apply(induct r1 r2 arbitrary: r3 rule: rrewrites.induct)
+ − 735
apply(auto intro: rrewrite_srewrite.intros)
+ − 736
done
+ − 737
+ − 738
lemma star_seq2:
+ − 739
assumes "r3 \<leadsto>* r4"
+ − 740
shows "ASEQ bs r1 r3 \<leadsto>* ASEQ bs r1 r4"
+ − 741
using assms
+ − 742
apply(induct r3 r4 arbitrary: r1 rule: rrewrites.induct)
+ − 743
apply(auto intro: rrewrite_srewrite.intros)
+ − 744
done
+ − 745
+ − 746
lemma continuous_rewrite:
+ − 747
assumes "r1 \<leadsto>* AZERO"
+ − 748
shows "ASEQ bs1 r1 r2 \<leadsto>* AZERO"
+ − 749
using assms bs1 star_seq by blast
+ − 750
+ − 751
(*
+ − 752
lemma continuous_rewrite2:
+ − 753
assumes "r1 \<leadsto>* AONE bs"
+ − 754
shows "ASEQ bs1 r1 r2 \<leadsto>* (fuse (bs1 @ bs) r2)"
+ − 755
using assms by (meson bs3 rrewrites.simps star_seq)
+ − 756
*)
+ − 757
+ − 758
lemma bsimp_aalts_simpcases:
+ − 759
shows "AONE bs \<leadsto>* bsimp (AONE bs)"
+ − 760
and "AZERO \<leadsto>* bsimp AZERO"
+ − 761
and "ACHAR bs c \<leadsto>* bsimp (ACHAR bs c)"
+ − 762
by (simp_all)
+ − 763
+ − 764
lemma bsimp_AALTs_rewrites:
+ − 765
shows "AALTs bs1 rs \<leadsto>* bsimp_AALTs bs1 rs"
+ − 766
by (smt (verit) bs6 bs7 bsimp_AALTs.elims rrewrites.simps)
+ − 767
+ − 768
lemma trivialbsimp_srewrites:
+ − 769
assumes "\<And>x. x \<in> set rs \<Longrightarrow> x \<leadsto>* f x"
+ − 770
shows "rs s\<leadsto>* (map f rs)"
+ − 771
using assms
+ − 772
apply(induction rs)
+ − 773
apply(simp_all add: srewrites7)
+ − 774
done
+ − 775
+ − 776
lemma fltsfrewrites: "rs s\<leadsto>* flts rs"
+ − 777
apply(induction rs rule: flts.induct)
+ − 778
apply(auto intro: rrewrite_srewrite.intros)
+ − 779
apply (meson srewrites.simps srewrites1 ss5)
+ − 780
using rs1 srewrites7 apply presburger
+ − 781
using srewrites7 apply force
+ − 782
apply (simp add: srewrites7)
+ − 783
by (simp add: srewrites7)
+ − 784
+ − 785
lemma bnullable0:
+ − 786
shows "r1 \<leadsto> r2 \<Longrightarrow> bnullable r1 = bnullable r2"
+ − 787
and "rs1 s\<leadsto> rs2 \<Longrightarrow> bnullables rs1 = bnullables rs2"
+ − 788
apply(induct rule: rrewrite_srewrite.inducts)
+ − 789
apply(auto simp add: bnullable_fuse)
+ − 790
apply (meson UnCI bnullable_fuse imageI)
+ − 791
by (metis bnullable_correctness)
+ − 792
+ − 793
+ − 794
lemma rewrites_bnullable_eq:
+ − 795
assumes "r1 \<leadsto>* r2"
+ − 796
shows "bnullable r1 = bnullable r2"
+ − 797
using assms
+ − 798
apply(induction r1 r2 rule: rrewrites.induct)
+ − 799
apply simp
+ − 800
using bnullable0(1) by auto
+ − 801
+ − 802
lemma rewrite_bmkeps_aux:
+ − 803
shows "r1 \<leadsto> r2 \<Longrightarrow> bnullable r1 \<Longrightarrow> bmkeps r1 = bmkeps r2"
+ − 804
and "rs1 s\<leadsto> rs2 \<Longrightarrow> bnullables rs1 \<Longrightarrow> bmkepss rs1 = bmkepss rs2"
+ − 805
proof (induct rule: rrewrite_srewrite.inducts)
+ − 806
case (bs3 bs1 bs2 r)
+ − 807
have IH2: "bnullable (ASEQ bs1 (AONE bs2) r)" by fact
+ − 808
then show "bmkeps (ASEQ bs1 (AONE bs2) r) = bmkeps (fuse (bs1 @ bs2) r)"
+ − 809
by (simp add: bmkeps_fuse)
+ − 810
next
+ − 811
case (bs7 bs r)
+ − 812
have IH2: "bnullable (AALTs bs [r])" by fact
+ − 813
then show "bmkeps (AALTs bs [r]) = bmkeps (fuse bs r)"
+ − 814
by (simp add: bmkeps_fuse)
+ − 815
next
+ − 816
case (ss3 r1 r2 rs)
+ − 817
have IH1: "bnullable r1 \<Longrightarrow> bmkeps r1 = bmkeps r2" by fact
+ − 818
have as: "r1 \<leadsto> r2" by fact
+ − 819
from IH1 as show "bmkepss (r1 # rs) = bmkepss (r2 # rs)"
+ − 820
by (simp add: bnullable0)
+ − 821
next
+ − 822
case (ss5 bs1 rs1 rsb)
+ − 823
have "bnullables (AALTs bs1 rs1 # rsb)" by fact
+ − 824
then show "bmkepss (AALTs bs1 rs1 # rsb) = bmkepss (map (fuse bs1) rs1 @ rsb)"
+ − 825
by (simp add: bmkepss1 bmkepss2 bmkepss_fuse bnullable_fuse)
+ − 826
next
+ − 827
case (ss6 a1 a2 rsa rsb rsc)
+ − 828
have as1: "erase a1 = erase a2" by fact
+ − 829
have as3: "bnullables (rsa @ [a1] @ rsb @ [a2] @ rsc)" by fact
+ − 830
show "bmkepss (rsa @ [a1] @ rsb @ [a2] @ rsc) = bmkepss (rsa @ [a1] @ rsb @ rsc)" using as1 as3
+ − 831
by (smt (verit, best) append_Cons bmkeps.simps(3) bmkepss.simps(2) bmkepss1 bmkepss2 bnullable_correctness)
+ − 832
qed (auto)
+ − 833
+ − 834
lemma rewrites_bmkeps:
+ − 835
assumes "r1 \<leadsto>* r2" "bnullable r1"
+ − 836
shows "bmkeps r1 = bmkeps r2"
+ − 837
using assms
+ − 838
proof(induction r1 r2 rule: rrewrites.induct)
+ − 839
case (rs1 r)
+ − 840
then show "bmkeps r = bmkeps r" by simp
+ − 841
next
+ − 842
case (rs2 r1 r2 r3)
+ − 843
then have IH: "bmkeps r1 = bmkeps r2" by simp
+ − 844
have a1: "bnullable r1" by fact
+ − 845
have a2: "r1 \<leadsto>* r2" by fact
+ − 846
have a3: "r2 \<leadsto> r3" by fact
+ − 847
have a4: "bnullable r2" using a1 a2 by (simp add: rewrites_bnullable_eq)
+ − 848
then have "bmkeps r2 = bmkeps r3"
+ − 849
using a3 bnullable0(1) rewrite_bmkeps_aux(1) by blast
+ − 850
then show "bmkeps r1 = bmkeps r3" using IH by simp
+ − 851
qed
+ − 852
+ − 853
+ − 854
lemma rewrites_to_bsimp:
+ − 855
shows "r \<leadsto>* bsimp r"
+ − 856
proof (induction r rule: bsimp.induct)
+ − 857
case (1 bs1 r1 r2)
+ − 858
have IH1: "r1 \<leadsto>* bsimp r1" by fact
+ − 859
have IH2: "r2 \<leadsto>* bsimp r2" by fact
+ − 860
{ assume as: "bsimp r1 = AZERO \<or> bsimp r2 = AZERO"
+ − 861
with IH1 IH2 have "r1 \<leadsto>* AZERO \<or> r2 \<leadsto>* AZERO" by auto
+ − 862
then have "ASEQ bs1 r1 r2 \<leadsto>* AZERO"
+ − 863
by (metis bs2 continuous_rewrite rrewrites.simps star_seq2)
+ − 864
then have "ASEQ bs1 r1 r2 \<leadsto>* bsimp (ASEQ bs1 r1 r2)" using as by auto
+ − 865
}
+ − 866
moreover
+ − 867
{ assume "\<exists>bs. bsimp r1 = AONE bs"
+ − 868
then obtain bs where as: "bsimp r1 = AONE bs" by blast
+ − 869
with IH1 have "r1 \<leadsto>* AONE bs" by simp
+ − 870
then have "ASEQ bs1 r1 r2 \<leadsto>* fuse (bs1 @ bs) r2" using bs3 star_seq by blast
+ − 871
with IH2 have "ASEQ bs1 r1 r2 \<leadsto>* fuse (bs1 @ bs) (bsimp r2)"
+ − 872
using rewrites_fuse by (meson rrewrites_trans)
+ − 873
then have "ASEQ bs1 r1 r2 \<leadsto>* bsimp (ASEQ bs1 (AONE bs) r2)" by simp
+ − 874
then have "ASEQ bs1 r1 r2 \<leadsto>* bsimp (ASEQ bs1 r1 r2)" by (simp add: as)
+ − 875
}
+ − 876
moreover
+ − 877
{ assume as1: "bsimp r1 \<noteq> AZERO" "bsimp r2 \<noteq> AZERO" and as2: "(\<nexists>bs. bsimp r1 = AONE bs)"
+ − 878
then have "bsimp_ASEQ bs1 (bsimp r1) (bsimp r2) = ASEQ bs1 (bsimp r1) (bsimp r2)"
+ − 879
by (simp add: bsimp_ASEQ1)
+ − 880
then have "ASEQ bs1 r1 r2 \<leadsto>* bsimp_ASEQ bs1 (bsimp r1) (bsimp r2)" using as1 as2 IH1 IH2
+ − 881
by (metis rrewrites_trans star_seq star_seq2)
+ − 882
then have "ASEQ bs1 r1 r2 \<leadsto>* bsimp (ASEQ bs1 r1 r2)" by simp
+ − 883
}
+ − 884
ultimately show "ASEQ bs1 r1 r2 \<leadsto>* bsimp (ASEQ bs1 r1 r2)" by blast
+ − 885
next
+ − 886
case (2 bs1 rs)
+ − 887
have IH: "\<And>x. x \<in> set rs \<Longrightarrow> x \<leadsto>* bsimp x" by fact
+ − 888
then have "rs s\<leadsto>* (map bsimp rs)" by (simp add: trivialbsimp_srewrites)
+ − 889
also have "... s\<leadsto>* flts (map bsimp rs)" by (simp add: fltsfrewrites)
+ − 890
also have "... s\<leadsto>* distinctBy (flts (map bsimp rs)) erase {}" by (simp add: ss6_stronger)
+ − 891
finally have "AALTs bs1 rs \<leadsto>* AALTs bs1 (distinctBy (flts (map bsimp rs)) erase {})"
+ − 892
using contextrewrites0 by blast
+ − 893
also have "... \<leadsto>* bsimp_AALTs bs1 (distinctBy (flts (map bsimp rs)) erase {})"
+ − 894
by (simp add: bsimp_AALTs_rewrites)
+ − 895
finally show "AALTs bs1 rs \<leadsto>* bsimp (AALTs bs1 rs)" by simp
+ − 896
qed (simp_all)
+ − 897
+ − 898
+ − 899
lemma to_zero_in_alt:
+ − 900
shows "AALT bs (ASEQ [] AZERO r) r2 \<leadsto> AALT bs AZERO r2"
+ − 901
by (simp add: bs1 bs8 ss3)
+ − 902
+ − 903
+ − 904
+ − 905
lemma bder_fuse_list:
+ − 906
shows "map (bder c \<circ> fuse bs1) rs1 = map (fuse bs1 \<circ> bder c) rs1"
+ − 907
apply(induction rs1)
+ − 908
apply(simp_all add: bder_fuse)
+ − 909
done
+ − 910
+ − 911
lemma rewrite_preserves_bder:
+ − 912
shows "r1 \<leadsto> r2 \<Longrightarrow> bder c r1 \<leadsto>* bder c r2"
+ − 913
and "rs1 s\<leadsto> rs2 \<Longrightarrow> map (bder c) rs1 s\<leadsto>* map (bder c) rs2"
+ − 914
proof(induction rule: rrewrite_srewrite.inducts)
+ − 915
case (bs1 bs r2)
+ − 916
show "bder c (ASEQ bs AZERO r2) \<leadsto>* bder c AZERO"
+ − 917
by (simp add: continuous_rewrite)
+ − 918
next
+ − 919
case (bs2 bs r1)
+ − 920
show "bder c (ASEQ bs r1 AZERO) \<leadsto>* bder c AZERO"
+ − 921
apply(auto)
+ − 922
apply (meson bs6 contextrewrites0 rrewrite_srewrite.bs2 rs2 ss3 ss4 sss1 sss2)
+ − 923
by (simp add: r_in_rstar rrewrite_srewrite.bs2)
+ − 924
next
+ − 925
case (bs3 bs1 bs2 r)
+ − 926
show "bder c (ASEQ bs1 (AONE bs2) r) \<leadsto>* bder c (fuse (bs1 @ bs2) r)"
+ − 927
apply(simp)
+ − 928
by (metis (no_types, lifting) bder_fuse bs8 bs7 fuse_append rrewrites.simps ss4 to_zero_in_alt)
+ − 929
next
+ − 930
case (bs4 r1 r2 bs r3)
+ − 931
have as: "r1 \<leadsto> r2" by fact
+ − 932
have IH: "bder c r1 \<leadsto>* bder c r2" by fact
+ − 933
from as IH show "bder c (ASEQ bs r1 r3) \<leadsto>* bder c (ASEQ bs r2 r3)"
+ − 934
by (metis bder.simps(5) bnullable0(1) contextrewrites1 rewrite_bmkeps_aux(1) star_seq)
+ − 935
next
+ − 936
case (bs5 r3 r4 bs r1)
+ − 937
have as: "r3 \<leadsto> r4" by fact
+ − 938
have IH: "bder c r3 \<leadsto>* bder c r4" by fact
+ − 939
from as IH show "bder c (ASEQ bs r1 r3) \<leadsto>* bder c (ASEQ bs r1 r4)"
+ − 940
apply(simp)
+ − 941
apply(auto)
+ − 942
using contextrewrites0 r_in_rstar rewrites_fuse srewrites6 srewrites7 star_seq2 apply presburger
+ − 943
using star_seq2 by blast
+ − 944
next
+ − 945
case (bs6 bs)
+ − 946
show "bder c (AALTs bs []) \<leadsto>* bder c AZERO"
+ − 947
using rrewrite_srewrite.bs6 by force
+ − 948
next
+ − 949
case (bs7 bs r)
+ − 950
show "bder c (AALTs bs [r]) \<leadsto>* bder c (fuse bs r)"
+ − 951
by (simp add: bder_fuse r_in_rstar rrewrite_srewrite.bs7)
+ − 952
next
+ − 953
case (bs8 rs1 rs2 bs)
+ − 954
have IH1: "map (bder c) rs1 s\<leadsto>* map (bder c) rs2" by fact
+ − 955
then show "bder c (AALTs bs rs1) \<leadsto>* bder c (AALTs bs rs2)"
+ − 956
using contextrewrites0 by force
+ − 957
(*next
+ − 958
case ss1
+ − 959
show "map (bder c) [] s\<leadsto>* map (bder c) []" by simp*)
+ − 960
next
+ − 961
case (ss2 rs1 rs2 r)
+ − 962
have IH1: "map (bder c) rs1 s\<leadsto>* map (bder c) rs2" by fact
+ − 963
then show "map (bder c) (r # rs1) s\<leadsto>* map (bder c) (r # rs2)"
+ − 964
by (simp add: srewrites7)
+ − 965
next
+ − 966
case (ss3 r1 r2 rs)
+ − 967
have IH: "bder c r1 \<leadsto>* bder c r2" by fact
+ − 968
then show "map (bder c) (r1 # rs) s\<leadsto>* map (bder c) (r2 # rs)"
+ − 969
by (simp add: srewrites7)
+ − 970
next
+ − 971
case (ss4 rs)
+ − 972
show "map (bder c) (AZERO # rs) s\<leadsto>* map (bder c) rs"
+ − 973
using rrewrite_srewrite.ss4 by fastforce
+ − 974
next
+ − 975
case (ss5 bs1 rs1 rsb)
+ − 976
show "map (bder c) (AALTs bs1 rs1 # rsb) s\<leadsto>* map (bder c) (map (fuse bs1) rs1 @ rsb)"
+ − 977
apply(simp)
+ − 978
using bder_fuse_list map_map rrewrite_srewrite.ss5 srewrites.simps by blast
+ − 979
next
+ − 980
case (ss6 a1 a2 bs rsa rsb)
+ − 981
have as: "erase a1 = erase a2" by fact
+ − 982
show "map (bder c) (bs @ [a1] @ rsa @ [a2] @ rsb) s\<leadsto>* map (bder c) (bs @ [a1] @ rsa @ rsb)"
+ − 983
apply(simp only: map_append)
+ − 984
by (smt (verit, best) erase_bder list.simps(8) list.simps(9) as rrewrite_srewrite.ss6 srewrites.simps)
+ − 985
qed
+ − 986
+ − 987
lemma rewrites_preserves_bder:
+ − 988
assumes "r1 \<leadsto>* r2"
+ − 989
shows "bder c r1 \<leadsto>* bder c r2"
+ − 990
using assms
+ − 991
apply(induction r1 r2 rule: rrewrites.induct)
+ − 992
apply(simp_all add: rewrite_preserves_bder rrewrites_trans)
+ − 993
done
+ − 994
+ − 995
+ − 996
lemma central:
+ − 997
shows "bders r s \<leadsto>* bders_simp r s"
+ − 998
proof(induct s arbitrary: r rule: rev_induct)
+ − 999
case Nil
+ − 1000
then show "bders r [] \<leadsto>* bders_simp r []" by simp
+ − 1001
next
+ − 1002
case (snoc x xs)
+ − 1003
have IH: "\<And>r. bders r xs \<leadsto>* bders_simp r xs" by fact
+ − 1004
have "bders r (xs @ [x]) = bders (bders r xs) [x]" by (simp add: bders_append)
+ − 1005
also have "... \<leadsto>* bders (bders_simp r xs) [x]" using IH
+ − 1006
by (simp add: rewrites_preserves_bder)
+ − 1007
also have "... \<leadsto>* bders_simp (bders_simp r xs) [x]" using IH
+ − 1008
by (simp add: rewrites_to_bsimp)
+ − 1009
finally show "bders r (xs @ [x]) \<leadsto>* bders_simp r (xs @ [x])"
+ − 1010
by (simp add: bders_simp_append)
+ − 1011
qed
+ − 1012
+ − 1013
lemma main_aux:
+ − 1014
assumes "bnullable (bders r s)"
+ − 1015
shows "bmkeps (bders r s) = bmkeps (bders_simp r s)"
+ − 1016
proof -
+ − 1017
have "bders r s \<leadsto>* bders_simp r s" by (rule central)
+ − 1018
then
+ − 1019
show "bmkeps (bders r s) = bmkeps (bders_simp r s)" using assms
+ − 1020
by (rule rewrites_bmkeps)
+ − 1021
qed
+ − 1022
+ − 1023
+ − 1024
theorem main_blexer_simp:
+ − 1025
shows "blexer r s = blexer_simp r s"
+ − 1026
unfolding blexer_def blexer_simp_def
+ − 1027
by (metis central main_aux rewrites_bnullable_eq)
+ − 1028
+ − 1029
+ − 1030
theorem blexersimp_correctness:
+ − 1031
shows "lexer r s = blexer_simp r s"
+ − 1032
using blexer_correctness main_blexer_simp by simp
+ − 1033
+ − 1034
+ − 1035
(* some tests *)
+ − 1036
+ − 1037
lemma asize_fuse:
+ − 1038
shows "asize (fuse bs r) = asize r"
+ − 1039
apply(induct r arbitrary: bs)
+ − 1040
apply(auto)
+ − 1041
done
+ − 1042
+ − 1043
lemma asize_rewrite2:
+ − 1044
shows "r1 \<leadsto> r2 \<Longrightarrow> asize r1 \<ge> asize r2"
+ − 1045
and "rs1 s\<leadsto> rs2 \<Longrightarrow> (sum_list (map asize rs1)) \<ge> (sum_list (map asize rs2))"
+ − 1046
apply(induct rule: rrewrite_srewrite.inducts)
+ − 1047
apply(auto simp add: asize_fuse comp_def)
+ − 1048
done
+ − 1049
+ − 1050
lemma asize_rrewrites:
+ − 1051
assumes "r1 \<leadsto>* r2"
+ − 1052
shows "asize r1 \<ge> asize r2"
+ − 1053
using assms
+ − 1054
apply(induct rule: rrewrites.induct)
+ − 1055
apply(auto)
+ − 1056
using asize_rewrite2(1) le_trans by blast
+ − 1057
+ − 1058
+ − 1059
+ − 1060
fun asize2 :: "arexp \<Rightarrow> nat" where
+ − 1061
"asize2 AZERO = 1"
+ − 1062
| "asize2 (AONE cs) = 1"
+ − 1063
| "asize2 (ACHAR cs c) = 1"
+ − 1064
| "asize2 (AALTs cs rs) = Suc (Suc (sum_list (map asize2 rs)))"
+ − 1065
| "asize2 (ASEQ cs r1 r2) = Suc (asize2 r1 + asize2 r2)"
+ − 1066
| "asize2 (ASTAR cs r) = Suc (asize2 r)"
+ − 1067
+ − 1068
+ − 1069
lemma asize2_fuse:
+ − 1070
shows "asize2 (fuse bs r) = asize2 r"
+ − 1071
apply(induct r arbitrary: bs)
+ − 1072
apply(auto)
+ − 1073
done
+ − 1074
+ − 1075
lemma asize2_not_zero:
+ − 1076
shows "0 < asize2 r"
+ − 1077
apply(induct r)
+ − 1078
apply(auto)
+ − 1079
done
+ − 1080
+ − 1081
lemma asize_rewrite:
+ − 1082
shows "r1 \<leadsto> r2 \<Longrightarrow> asize2 r1 > asize2 r2"
+ − 1083
and "rs1 s\<leadsto> rs2 \<Longrightarrow> (sum_list (map asize2 rs1)) > (sum_list (map asize2 rs2))"
+ − 1084
apply(induct rule: rrewrite_srewrite.inducts)
+ − 1085
apply(auto simp add: asize2_fuse comp_def)
+ − 1086
apply(simp add: asize2_not_zero)
+ − 1087
done
+ − 1088
+ − 1089
lemma asize2_bsimp_ASEQ:
+ − 1090
shows "asize2 (bsimp_ASEQ bs r1 r2) \<le> Suc (asize2 r1 + asize2 r2)"
+ − 1091
apply(induct bs r1 r2 rule: bsimp_ASEQ.induct)
+ − 1092
apply(auto)
+ − 1093
done
+ − 1094
+ − 1095
lemma asize2_bsimp_AALTs:
+ − 1096
shows "asize2 (bsimp_AALTs bs rs) \<le> Suc (Suc (sum_list (map asize2 rs)))"
+ − 1097
apply(induct bs rs rule: bsimp_AALTs.induct)
+ − 1098
apply(auto simp add: asize2_fuse)
+ − 1099
done
+ − 1100
+ − 1101
lemma distinctBy_asize2:
+ − 1102
shows "sum_list (map asize2 (distinctBy rs f acc)) \<le> sum_list (map asize2 rs)"
+ − 1103
apply(induct rs f acc rule: distinctBy.induct)
+ − 1104
apply(auto)
+ − 1105
done
+ − 1106
+ − 1107
lemma flts_asize2:
+ − 1108
shows "sum_list (map asize2 (flts rs)) \<le> sum_list (map asize2 rs)"
+ − 1109
apply(induct rs rule: flts.induct)
+ − 1110
apply(auto simp add: comp_def asize2_fuse)
+ − 1111
done
+ − 1112
+ − 1113
lemma sumlist_asize2:
+ − 1114
assumes "\<And>x. x \<in> set rs \<Longrightarrow> asize2 (f x) \<le> asize2 x"
+ − 1115
shows "sum_list (map asize2 (map f rs)) \<le> sum_list (map asize2 rs)"
+ − 1116
using assms
+ − 1117
apply(induct rs)
+ − 1118
apply(auto simp add: comp_def)
+ − 1119
by (simp add: add_le_mono)
+ − 1120
+ − 1121
lemma test0:
+ − 1122
assumes "r1 \<leadsto>* r2"
+ − 1123
shows "r1 = r2 \<or> (\<exists>r3. r1 \<leadsto> r3 \<and> r3 \<leadsto>* r2)"
+ − 1124
using assms
+ − 1125
apply(induct r1 r2 rule: rrewrites.induct)
+ − 1126
apply(auto)
+ − 1127
done
+ − 1128
+ − 1129
lemma test2:
+ − 1130
assumes "r1 \<leadsto>* r2"
+ − 1131
shows "asize2 r1 \<ge> asize2 r2"
+ − 1132
using assms
+ − 1133
apply(induct r1 r2 rule: rrewrites.induct)
+ − 1134
apply(auto)
+ − 1135
using asize_rewrite(1) by fastforce
+ − 1136
+ − 1137
+ − 1138
lemma test3:
+ − 1139
shows "r = bsimp r \<or> (asize2 (bsimp r) < asize2 r)"
+ − 1140
proof -
+ − 1141
have "r \<leadsto>* bsimp r"
+ − 1142
by (simp add: rewrites_to_bsimp)
+ − 1143
then have "r = bsimp r \<or> (\<exists>r3. r \<leadsto> r3 \<and> r3 \<leadsto>* bsimp r)"
+ − 1144
using test0 by blast
+ − 1145
then show ?thesis
+ − 1146
by (meson asize_rewrite(1) dual_order.strict_trans2 test2)
+ − 1147
qed
+ − 1148
+ − 1149
lemma test3Q:
+ − 1150
shows "r = bsimp r \<or> (asize (bsimp r) \<le> asize r)"
+ − 1151
proof -
+ − 1152
have "r \<leadsto>* bsimp r"
+ − 1153
by (simp add: rewrites_to_bsimp)
+ − 1154
then have "r = bsimp r \<or> (\<exists>r3. r \<leadsto> r3 \<and> r3 \<leadsto>* bsimp r)"
+ − 1155
using test0 by blast
+ − 1156
then show ?thesis
+ − 1157
using asize_rewrite2(1) asize_rrewrites le_trans by blast
+ − 1158
qed
+ − 1159
+ − 1160
lemma test4:
+ − 1161
shows "asize2 (bsimp (bsimp r)) \<le> asize2 (bsimp r)"
+ − 1162
apply(induct r rule: bsimp.induct)
+ − 1163
apply(auto)
+ − 1164
using rewrites_to_bsimp test2 apply fastforce
+ − 1165
using rewrites_to_bsimp test2 by presburger
+ − 1166
+ − 1167
lemma test4Q:
+ − 1168
shows "asize (bsimp (bsimp r)) \<le> asize (bsimp r)"
+ − 1169
apply(induct r rule: bsimp.induct)
+ − 1170
apply(auto)
+ − 1171
apply (metis order_refl test3Q)
+ − 1172
by (metis le_refl test3Q)
+ − 1173
+ − 1174
+ − 1175
+ − 1176
lemma testb0:
+ − 1177
shows "fuse bs1 (bsimp_ASEQ bs r1 r2) = bsimp_ASEQ (bs1 @ bs) r1 r2"
+ − 1178
apply(induct bs r1 r2 arbitrary: bs1 rule: bsimp_ASEQ.induct)
+ − 1179
apply(auto)
+ − 1180
done
+ − 1181
+ − 1182
lemma testb1:
+ − 1183
shows "fuse bs1 (bsimp_AALTs bs rs) = bsimp_AALTs (bs1 @ bs) rs"
+ − 1184
apply(induct bs rs arbitrary: bs1 rule: bsimp_AALTs.induct)
+ − 1185
apply(auto simp add: fuse_append)
+ − 1186
done
+ − 1187
+ − 1188
lemma testb2:
+ − 1189
shows "bsimp (bsimp_ASEQ bs r1 r2) = bsimp_ASEQ bs (bsimp r1) (bsimp r2)"
+ − 1190
apply(induct bs r1 r2 rule: bsimp_ASEQ.induct)
+ − 1191
apply(auto simp add: testb0 testb1)
+ − 1192
done
+ − 1193
+ − 1194
lemma testb3:
+ − 1195
shows "\<nexists>r'. (bsimp r \<leadsto> r') \<and> asize2 (bsimp r) > asize2 r'"
+ − 1196
apply(induct r rule: bsimp.induct)
+ − 1197
apply(auto)
+ − 1198
defer
+ − 1199
defer
+ − 1200
using rrewrite.cases apply blast
+ − 1201
using rrewrite.cases apply blast
+ − 1202
using rrewrite.cases apply blast
+ − 1203
using rrewrite.cases apply blast
+ − 1204
oops
+ − 1205
+ − 1206
lemma testb4:
+ − 1207
assumes "sum_list (map asize rs1) \<le> sum_list (map asize rs2)"
+ − 1208
shows "asize (bsimp_AALTs bs1 rs1) \<le> Suc (asize (bsimp_AALTs bs1 rs2))"
+ − 1209
using assms
+ − 1210
apply(induct bs1 rs2 arbitrary: rs1 rule: bsimp_AALTs.induct)
+ − 1211
apply(auto)
+ − 1212
apply(case_tac rs1)
+ − 1213
apply(auto)
+ − 1214
using asize2.elims apply auto[1]
+ − 1215
apply (metis One_nat_def Zero_not_Suc asize.elims)
+ − 1216
apply(case_tac rs1)
+ − 1217
apply(auto)
+ − 1218
apply(case_tac list)
+ − 1219
apply(auto)
+ − 1220
using asize_fuse apply force
+ − 1221
apply (simp add: asize_fuse)
+ − 1222
by (smt (verit, ccfv_threshold) One_nat_def add.right_neutral asize.simps(1) asize.simps(4) asize_fuse bsimp_AALTs.elims le_Suc_eq list.map(1) list.map(2) not_less_eq_eq sum_list_simps(1) sum_list_simps(2))
+ − 1223
+ − 1224
lemma flts_asize:
+ − 1225
shows "sum_list (map asize (flts rs)) \<le> sum_list (map asize rs)"
+ − 1226
apply(induct rs rule: flts.induct)
+ − 1227
apply(auto simp add: comp_def asize_fuse)
+ − 1228
done
+ − 1229
+ − 1230
+ − 1231
lemma test5:
+ − 1232
shows "asize2 r \<ge> asize2 (bsimp r)"
+ − 1233
apply(induct r rule: bsimp.induct)
+ − 1234
apply(auto)
+ − 1235
apply (meson Suc_le_mono add_le_mono asize2_bsimp_ASEQ order_trans)
+ − 1236
apply(rule order_trans)
+ − 1237
apply(rule asize2_bsimp_AALTs)
+ − 1238
apply(simp)
+ − 1239
apply(rule order_trans)
+ − 1240
apply(rule distinctBy_asize2)
+ − 1241
apply(rule order_trans)
+ − 1242
apply(rule flts_asize2)
+ − 1243
using sumlist_asize2 by force
+ − 1244
+ − 1245
+ − 1246
fun awidth :: "arexp \<Rightarrow> nat" where
+ − 1247
"awidth AZERO = 1"
+ − 1248
| "awidth (AONE cs) = 1"
+ − 1249
| "awidth (ACHAR cs c) = 1"
+ − 1250
| "awidth (AALTs cs rs) = (sum_list (map awidth rs))"
+ − 1251
| "awidth (ASEQ cs r1 r2) = (awidth r1 + awidth r2)"
+ − 1252
| "awidth (ASTAR cs r) = (awidth r)"
+ − 1253
+ − 1254
+ − 1255
+ − 1256
lemma
+ − 1257
shows "s \<notin> L r \<Longrightarrow> blexer_simp r s = None"
+ − 1258
by (simp add: blexersimp_correctness lexer_correct_None)
+ − 1259
+ − 1260
lemma g1:
+ − 1261
"bders_simp AZERO s = AZERO"
+ − 1262
apply(induct s)
+ − 1263
apply(simp)
+ − 1264
apply(simp)
+ − 1265
done
+ − 1266
+ − 1267
lemma g2:
+ − 1268
"s \<noteq> Nil \<Longrightarrow> bders_simp (AONE bs) s = AZERO"
+ − 1269
apply(induct s)
+ − 1270
apply(simp)
+ − 1271
apply(simp)
+ − 1272
apply(case_tac s)
+ − 1273
apply(simp)
+ − 1274
apply(simp)
+ − 1275
done
+ − 1276
+ − 1277
lemma finite_pder:
+ − 1278
shows "finite (pder c r)"
+ − 1279
apply(induct c r rule: pder.induct)
+ − 1280
apply(auto)
+ − 1281
done
+ − 1282
+ − 1283
+ − 1284
+ − 1285
lemma awidth_fuse:
+ − 1286
shows "awidth (fuse bs r) = awidth r"
+ − 1287
apply(induct r arbitrary: bs)
+ − 1288
apply(auto)
+ − 1289
done
+ − 1290
+ − 1291
lemma pders_SEQs:
+ − 1292
assumes "finite A"
+ − 1293
shows "card (SEQs A (STAR r)) \<le> card A"
+ − 1294
using assms
+ − 1295
by (simp add: SEQs_eq_image card_image_le)
+ − 1296
+ − 1297
lemma binullable_intern:
+ − 1298
shows "bnullable (intern r) = nullable r"
+ − 1299
apply(induct r)
+ − 1300
apply(auto simp add: bnullable_fuse)
+ − 1301
done
+ − 1302
+ − 1303
lemma
+ − 1304
"card (pder c r) \<le> awidth (bder c (intern r))"
+ − 1305
apply(induct c r rule: pder.induct)
+ − 1306
apply(simp)
+ − 1307
apply(simp)
+ − 1308
apply(simp)
+ − 1309
apply(simp)
+ − 1310
apply(rule order_trans)
+ − 1311
apply(rule card_Un_le)
+ − 1312
apply (simp add: awidth_fuse bder_fuse)
+ − 1313
defer
+ − 1314
apply(simp)
+ − 1315
apply(rule order_trans)
+ − 1316
apply(rule pders_SEQs)
+ − 1317
using finite_pder apply presburger
+ − 1318
apply (simp add: awidth_fuse)
+ − 1319
apply(auto)
+ − 1320
apply(rule order_trans)
+ − 1321
apply(rule card_Un_le)
+ − 1322
apply(simp add: awidth_fuse)
+ − 1323
defer
+ − 1324
using binullable_intern apply blast
+ − 1325
using binullable_intern apply blast
+ − 1326
apply (smt (verit, best) SEQs_eq_image add.commute add_Suc_right card_image_le dual_order.trans finite_pder trans_le_add2)
+ − 1327
apply(subgoal_tac "card (SEQs (pder c r1) r2) \<le> card (pder c r1)")
+ − 1328
apply(linarith)
+ − 1329
by (simp add: UNION_singleton_eq_range card_image_le finite_pder)
+ − 1330
+ − 1331
lemma
+ − 1332
"card (pder c r) \<le> asize (bder c (intern r))"
+ − 1333
apply(induct c r rule: pder.induct)
+ − 1334
apply(simp)
+ − 1335
apply(simp)
+ − 1336
apply(simp)
+ − 1337
apply(simp)
+ − 1338
apply (metis add_mono_thms_linordered_semiring(1) asize_fuse bder_fuse card_Un_le le_Suc_eq order_trans)
+ − 1339
defer
+ − 1340
apply(simp)
+ − 1341
apply(rule order_trans)
+ − 1342
apply(rule pders_SEQs)
+ − 1343
using finite_pder apply presburger
+ − 1344
apply (simp add: asize_fuse)
+ − 1345
apply(simp)
+ − 1346
apply(auto)
+ − 1347
apply(rule order_trans)
+ − 1348
apply(rule card_Un_le)
+ − 1349
apply (smt (z3) SEQs_eq_image add.commute add_Suc_right add_mono_thms_linordered_semiring(1) asize_fuse card_image_le dual_order.trans finite_pder le_add1)
+ − 1350
apply(rule order_trans)
+ − 1351
apply(rule card_Un_le)
+ − 1352
using binullable_intern apply blast
+ − 1353
using binullable_intern apply blast
+ − 1354
by (smt (verit, best) SEQs_eq_image add.commute add_Suc_right card_image_le dual_order.trans finite_pder trans_le_add2)
+ − 1355
+ − 1356
lemma
+ − 1357
"card (pder c r) \<le> asize (bsimp (bder c (intern r)))"
+ − 1358
apply(induct c r rule: pder.induct)
+ − 1359
apply(simp)
+ − 1360
apply(simp)
+ − 1361
apply(simp)
+ − 1362
apply(simp)
+ − 1363
apply(rule order_trans)
+ − 1364
apply(rule card_Un_le)
+ − 1365
prefer 3
+ − 1366
apply(simp)
+ − 1367
apply(rule order_trans)
+ − 1368
apply(rule pders_SEQs)
+ − 1369
using finite_pder apply blast
+ − 1370
oops
+ − 1371
+ − 1372
+ − 1373
(* below is the idempotency of bsimp *)
+ − 1374
+ − 1375
lemma bsimp_ASEQ_fuse:
+ − 1376
shows "fuse bs1 (bsimp_ASEQ bs2 r1 r2) = bsimp_ASEQ (bs1 @ bs2) r1 r2"
+ − 1377
apply(induct r1 r2 arbitrary: bs1 bs2 rule: bsimp_ASEQ.induct)
+ − 1378
apply(auto)
+ − 1379
done
+ − 1380
+ − 1381
lemma bsimp_AALTs_fuse:
+ − 1382
assumes "\<forall>r \<in> set rs. fuse bs1 (fuse bs2 r) = fuse (bs1 @ bs2) r"
+ − 1383
shows "fuse bs1 (bsimp_AALTs bs2 rs) = bsimp_AALTs (bs1 @ bs2) rs"
+ − 1384
using assms
+ − 1385
apply(induct bs2 rs arbitrary: bs1 rule: bsimp_AALTs.induct)
+ − 1386
apply(auto)
+ − 1387
done
+ − 1388
+ − 1389
lemma bsimp_fuse:
+ − 1390
shows "fuse bs (bsimp r) = bsimp (fuse bs r)"
+ − 1391
apply(induct r arbitrary: bs)
+ − 1392
apply(simp_all add: bsimp_ASEQ_fuse bsimp_AALTs_fuse fuse_append)
+ − 1393
done
+ − 1394
+ − 1395
lemma bsimp_ASEQ_idem:
+ − 1396
assumes "bsimp (bsimp r1) = bsimp r1" "bsimp (bsimp r2) = bsimp r2"
+ − 1397
shows "bsimp (bsimp_ASEQ x1 (bsimp r1) (bsimp r2)) = bsimp_ASEQ x1 (bsimp r1) (bsimp r2)"
+ − 1398
using assms
+ − 1399
apply(case_tac "bsimp r1 = AZERO")
+ − 1400
apply(simp)
+ − 1401
apply(case_tac "bsimp r2 = AZERO")
+ − 1402
apply(simp)
+ − 1403
apply(case_tac "\<exists>bs. bsimp r1 = AONE bs")
+ − 1404
apply(auto)[1]
+ − 1405
apply (metis bsimp_fuse)
+ − 1406
apply(simp add: bsimp_ASEQ1)
+ − 1407
done
+ − 1408
+ − 1409
lemma bsimp_AALTs_idem:
+ − 1410
assumes "\<forall>r \<in> set rs. bsimp (bsimp r) = bsimp r"
+ − 1411
shows "bsimp (bsimp_AALTs bs rs) = bsimp_AALTs bs (map bsimp rs)"
+ − 1412
using assms
+ − 1413
apply(induct bs rs rule: bsimp_AALTs.induct)
+ − 1414
apply(simp)
+ − 1415
apply(simp)
+ − 1416
using bsimp_fuse apply presburger
+ − 1417
oops
+ − 1418
+ − 1419
lemma bsimp_idem_rev:
+ − 1420
shows "\<nexists>r2. bsimp r1 \<leadsto> r2"
+ − 1421
apply(induct r1 rule: bsimp.induct)
+ − 1422
apply(auto)
+ − 1423
defer
+ − 1424
defer
+ − 1425
using rrewrite.simps apply blast
+ − 1426
using rrewrite.cases apply blast
+ − 1427
using rrewrite.simps apply blast
+ − 1428
using rrewrite.cases apply blast
+ − 1429
apply(case_tac "bsimp r1 = AZERO")
+ − 1430
apply(simp)
+ − 1431
apply(case_tac "bsimp r2 = AZERO")
+ − 1432
apply(simp)
+ − 1433
apply(case_tac "\<exists>bs. bsimp r1 = AONE bs")
+ − 1434
apply(auto)[1]
+ − 1435
prefer 2
+ − 1436
apply (smt (verit, best) arexp.distinct(25) arexp.inject(3) bsimp_ASEQ1 rrewrite.simps)
+ − 1437
defer
+ − 1438
oops
+ − 1439
+ − 1440
lemma bsimp_idem:
+ − 1441
shows "bsimp (bsimp r) = bsimp r"
+ − 1442
apply(induct r rule: bsimp.induct)
+ − 1443
apply(auto)
+ − 1444
using bsimp_ASEQ_idem apply presburger
417
+ − 1445
sorry
+ − 1446
409
+ − 1447
+ − 1448
lemma neg:
+ − 1449
shows " \<not>(\<exists>r2. r1 \<leadsto> r2 \<and> (r2 \<leadsto>* bsimp r1) )"
+ − 1450
apply(rule notI)
+ − 1451
apply(erule exE)
+ − 1452
apply(erule conjE)
+ − 1453
oops
+ − 1454
+ − 1455
+ − 1456
+ − 1457
lemma reduction_always_in_bsimp:
+ − 1458
shows " \<lbrakk> r1 \<leadsto> r2 ; \<not>(r2 \<leadsto>* bsimp r1)\<rbrakk> \<Longrightarrow> False"
+ − 1459
apply(erule rrewrite.cases)
+ − 1460
apply simp
+ − 1461
apply auto
+ − 1462
+ − 1463
oops
+ − 1464
417
+ − 1465
+ − 1466
409
+ − 1467
(*
+ − 1468
AALTs [] [AZERO, AALTs(bs1, [a, b]) ]
+ − 1469
rewrite seq 1: \<leadsto> AALTs [] [ AALTs(bs1, [a, b]) ] \<leadsto>
+ − 1470
fuse [] (AALTs bs1, [a, b])
+ − 1471
rewrite seq 2: \<leadsto> AALTs [] [AZERO, (fuse bs1 a), (fuse bs1 b)]) ]
+ − 1472
+ − 1473
*)
+ − 1474
+ − 1475
lemma normal_bsimp:
+ − 1476
shows "\<nexists>r'. bsimp r \<leadsto> r'"
+ − 1477
oops
+ − 1478
+ − 1479
(*r' size bsimp r > size r'
+ − 1480
r' \<leadsto>* bsimp bsimp r
+ − 1481
size bsimp r > size r' \<ge> size bsimp bsimp r*)
+ − 1482
417
+ − 1483
fun orderedSufAux :: "nat \<Rightarrow> char list \<Rightarrow> char list list"
+ − 1484
where
421
+ − 1485
"orderedSufAux (Suc i) ss = (drop i ss) # (orderedSufAux i ss)"
417
+ − 1486
|"orderedSufAux 0 ss = Nil"
+ − 1487
+ − 1488
fun
+ − 1489
orderedSuf :: "char list \<Rightarrow> char list list"
+ − 1490
where
+ − 1491
"orderedSuf s = orderedSufAux (length s) s"
+ − 1492
421
+ − 1493
fun orderedPrefAux :: "nat \<Rightarrow> char list \<Rightarrow> char list list"
+ − 1494
where
+ − 1495
"orderedPrefAux (Suc i) ss = (take i ss) # (orderedPrefAux i ss)"
+ − 1496
|"orderedPrefAux 0 ss = Nil"
+ − 1497
+ − 1498
+ − 1499
fun orderedPref :: "char list \<Rightarrow> char list list"
+ − 1500
where
+ − 1501
"orderedPref s = orderedPrefAux (length s) s"
+ − 1502
+ − 1503
lemma shape_of_pref_1list:
+ − 1504
shows "orderedPref [c] = [[]]"
417
+ − 1505
apply auto
+ − 1506
done
+ − 1507
421
+ − 1508
lemma shape_of_suf_1list:
+ − 1509
shows "orderedSuf [c] = [[c]]"
+ − 1510
by auto
+ − 1511
+ − 1512
lemma shape_of_suf_2list:
+ − 1513
shows "orderedSuf [c2, c3] = [[c3], [c2,c3]]"
+ − 1514
by auto
+ − 1515
+ − 1516
lemma shape_of_prf_2list:
+ − 1517
shows "orderedPref [c1, c2] = [[c1], []]"
+ − 1518
by auto
+ − 1519
417
+ − 1520
+ − 1521
lemma shape_of_suf_3list:
421
+ − 1522
shows "orderedSuf [c1, c2, c3] = [[c3], [c2, c3], [c1, c2, c3]]"
+ − 1523
by auto
+ − 1524
+ − 1525
lemma throwing_elem_around:
+ − 1526
shows "orderedSuf (s1 @ [a] @ s) = (orderedSuf s) @ (map (\<lambda>s11. s11 @ s) (orderedSuf ( s1 @ [a]) ))"
+ − 1527
and "orderedSuf (s1 @ [a] @ s) = (orderedSuf ([a] @ s) @ (map (\<lambda>s11. s11 @ ([a] @ s))) (orderedSuf s1) )"
+ − 1528
sorry
+ − 1529
+ − 1530
+ − 1531
lemma suf_cons:
+ − 1532
shows "orderedSuf (s1 @ s) = (orderedSuf s) @ (map (\<lambda>s11. s11 @ s) (orderedSuf s1))"
+ − 1533
apply(induct s arbitrary: s1)
+ − 1534
apply simp
+ − 1535
apply(subgoal_tac "s1 @ a # s = (s1 @ [a]) @ s")
+ − 1536
prefer 2
+ − 1537
apply simp
+ − 1538
apply(subgoal_tac "orderedSuf (s1 @ a # s) = orderedSuf ((s1 @ [a]) @ s)")
+ − 1539
prefer 2
+ − 1540
apply presburger
+ − 1541
apply(drule_tac x="s1 @ [a]" in meta_spec)
+ − 1542
sorry
+ − 1543
+ − 1544
+ − 1545
+ − 1546
lemma shape_of_prf_3list:
+ − 1547
shows "orderedPref [c1, c2, c3] = [[c1, c2], [c1], []]"
+ − 1548
by auto
+ − 1549
+ − 1550
fun zip_concat :: "char list list \<Rightarrow> char list list \<Rightarrow> char list list"
+ − 1551
where
+ − 1552
"zip_concat (s1#ss1) (s2#ss2) = (s1@s2) # (zip_concat ss1 ss2)"
+ − 1553
| "zip_concat [] [] = []"
+ − 1554
| "zip_concat [] (s2#ss2) = s2 # (zip_concat [] ss2)"
+ − 1555
| "zip_concat (s1#ss1) [] = s1 # (zip_concat ss1 [])"
+ − 1556
+ − 1557
+ − 1558
+ − 1559
lemma compliment_pref_suf:
+ − 1560
shows "zip_concat (orderedPref s) (orderedSuf s) = replicate (length s) s "
+ − 1561
apply(induct s)
+ − 1562
apply auto[1]
+ − 1563
sorry
+ − 1564
417
+ − 1565
+ − 1566
+ − 1567
+ − 1568
datatype rrexp =
+ − 1569
RZERO
+ − 1570
| RONE
+ − 1571
| RCHAR char
+ − 1572
| RSEQ rrexp rrexp
+ − 1573
| RALTS "rrexp list"
+ − 1574
| RSTAR rrexp
+ − 1575
+ − 1576
abbreviation
+ − 1577
"RALT r1 r2 \<equiv> RALTS [r1, r2]"
+ − 1578
+ − 1579
fun
+ − 1580
rerase :: "arexp \<Rightarrow> rrexp"
+ − 1581
where
+ − 1582
"rerase AZERO = RZERO"
+ − 1583
| "rerase (AONE _) = RONE"
+ − 1584
| "rerase (ACHAR _ c) = RCHAR c"
+ − 1585
| "rerase (AALTs bs rs) = RALTS (map rerase rs)"
+ − 1586
| "rerase (ASEQ _ r1 r2) = RSEQ (rerase r1) (rerase r2)"
+ − 1587
| "rerase (ASTAR _ r) = RSTAR (rerase r)"
+ − 1588
+ − 1589
+ − 1590
+ − 1591
+ − 1592
fun
+ − 1593
rnullable :: "rrexp \<Rightarrow> bool"
+ − 1594
where
+ − 1595
"rnullable (RZERO) = False"
+ − 1596
| "rnullable (RONE ) = True"
+ − 1597
| "rnullable (RCHAR c) = False"
+ − 1598
| "rnullable (RALTS rs) = (\<exists>r \<in> set rs. rnullable r)"
+ − 1599
| "rnullable (RSEQ r1 r2) = (rnullable r1 \<and> rnullable r2)"
+ − 1600
| "rnullable (RSTAR r) = True"
+ − 1601
+ − 1602
+ − 1603
fun
+ − 1604
rder :: "char \<Rightarrow> rrexp \<Rightarrow> rrexp"
+ − 1605
where
+ − 1606
"rder c (RZERO) = RZERO"
+ − 1607
| "rder c (RONE) = RZERO"
+ − 1608
| "rder c (RCHAR d) = (if c = d then RONE else RZERO)"
+ − 1609
| "rder c (RALTS rs) = RALTS (map (rder c) rs)"
+ − 1610
| "rder c (RSEQ r1 r2) =
+ − 1611
(if rnullable r1
+ − 1612
then RALT (RSEQ (rder c r1) r2) (rder c r2)
+ − 1613
else RSEQ (rder c r1) r2)"
+ − 1614
| "rder c (RSTAR r) = RSEQ (rder c r) (RSTAR r)"
+ − 1615
+ − 1616
+ − 1617
fun
+ − 1618
rders :: "rrexp \<Rightarrow> string \<Rightarrow> rrexp"
+ − 1619
where
+ − 1620
"rders r [] = r"
+ − 1621
| "rders r (c#s) = rders (rder c r) s"
+ − 1622
+ − 1623
fun rdistinct :: "'a list \<Rightarrow>'a set \<Rightarrow> 'a list"
+ − 1624
where
+ − 1625
"rdistinct [] acc = []"
+ − 1626
| "rdistinct (x#xs) acc =
+ − 1627
(if x \<in> acc then rdistinct xs acc
+ − 1628
else x # (rdistinct xs ({x} \<union> acc)))"
+ − 1629
+ − 1630
+ − 1631
fun rflts :: "rrexp list \<Rightarrow> rrexp list"
+ − 1632
where
+ − 1633
"rflts [] = []"
+ − 1634
| "rflts (RZERO # rs) = rflts rs"
+ − 1635
| "rflts ((RALTS rs1) # rs) = rs1 @ rflts rs"
+ − 1636
| "rflts (r1 # rs) = r1 # rflts rs"
+ − 1637
+ − 1638
+ − 1639
fun rsimp_ALTs :: " rrexp list \<Rightarrow> rrexp"
+ − 1640
where
+ − 1641
"rsimp_ALTs [] = RZERO"
+ − 1642
| "rsimp_ALTs [r] = r"
+ − 1643
| "rsimp_ALTs rs = RALTS rs"
+ − 1644
+ − 1645
fun rsimp_SEQ :: " rrexp \<Rightarrow> rrexp \<Rightarrow> rrexp"
+ − 1646
where
+ − 1647
"rsimp_SEQ RZERO _ = RZERO"
+ − 1648
| "rsimp_SEQ _ RZERO = RZERO"
+ − 1649
| "rsimp_SEQ RONE r2 = r2"
+ − 1650
| "rsimp_SEQ r1 r2 = RSEQ r1 r2"
+ − 1651
+ − 1652
+ − 1653
fun rsimp :: "rrexp \<Rightarrow> rrexp"
+ − 1654
where
+ − 1655
"rsimp (RSEQ r1 r2) = rsimp_SEQ (rsimp r1) (rsimp r2)"
+ − 1656
| "rsimp (RALTS rs) = rsimp_ALTs (rdistinct (rflts (map rsimp rs)) {}) "
+ − 1657
| "rsimp r = r"
+ − 1658
+ − 1659
+ − 1660
fun
+ − 1661
rders_simp :: "rrexp \<Rightarrow> string \<Rightarrow> rrexp"
+ − 1662
where
+ − 1663
"rders_simp r [] = r"
+ − 1664
| "rders_simp r (c#s) = rders_simp (rsimp (rder c r)) s"
+ − 1665
421
+ − 1666
fun rsize :: "rrexp \<Rightarrow> nat" where
+ − 1667
"rsize RZERO = 1"
+ − 1668
| "rsize (RONE) = 1"
+ − 1669
| "rsize (RCHAR c) = 1"
+ − 1670
| "rsize (RALTS rs) = Suc (sum_list (map rsize rs))"
+ − 1671
| "rsize (RSEQ r1 r2) = Suc (rsize r1 + rsize r2)"
+ − 1672
| "rsize (RSTAR r) = Suc (rsize r)"
+ − 1673
417
+ − 1674
427
+ − 1675
+ − 1676
+ − 1677
lemma rsimp_aalts_smaller:
+ − 1678
shows "rsize (rsimp_ALTs rs) \<le> rsize (RALTS rs)"
+ − 1679
apply(induct rs)
+ − 1680
apply simp
+ − 1681
sorry
+ − 1682
+ − 1683
lemma finite_list_of_ders:
+ − 1684
shows"\<exists>dersset. ( (finite dersset) \<and> (\<forall>s. (rders_simp r s) \<in> dersset) )"
+ − 1685
sorry
+ − 1686
+ − 1687
+ − 1688
417
+ − 1689
lemma rerase_bsimp:
+ − 1690
shows "rerase (bsimp r) = rsimp (rerase r)"
+ − 1691
apply(induct r)
+ − 1692
apply auto
+ − 1693
+ − 1694
+ − 1695
sorry
+ − 1696
421
+ − 1697
417
+ − 1698
lemma rerase_bder:
+ − 1699
shows "rerase (bder c r) = rder c (rerase r)"
+ − 1700
apply(induct r)
+ − 1701
apply auto
+ − 1702
sorry
421
+ − 1703
(*
417
+ − 1704
lemma rders_shape:
421
+ − 1705
shows "s \<noteq> [] \<Longrightarrow> rders_simp (RSEQ r1 r2) s =
417
+ − 1706
rsimp (RALTS ((RSEQ (rders r1 s) r2) #
+ − 1707
(map (rders r2) (orderedSuf s))) )"
421
+ − 1708
apply(induct s arbitrary: r1 r2 rule: rev_induct)
+ − 1709
apply simp
+ − 1710
apply simp
+ − 1711
417
+ − 1712
sorry
421
+ − 1713
*)
+ − 1714
427
+ − 1715
421
+ − 1716
+ − 1717
fun rders_cond_list :: "rrexp \<Rightarrow> bool list \<Rightarrow> char list list \<Rightarrow> rrexp list"
+ − 1718
where
+ − 1719
"rders_cond_list r2 (True # bs) (s # strs) = (rders r2 s) # (rders_cond_list r2 bs strs)"
+ − 1720
| "rders_cond_list r2 (False # bs) (s # strs) = rders_cond_list r2 bs strs"
+ − 1721
| "rders_cond_list r2 [] s = []"
+ − 1722
| "rders_cond_list r2 bs [] = []"
+ − 1723
+ − 1724
fun nullable_bools :: "rrexp \<Rightarrow> char list list \<Rightarrow> bool list"
+ − 1725
where
+ − 1726
"nullable_bools r (s#strs) = (rnullable (rders r s)) # (nullable_bools r strs) "
+ − 1727
|"nullable_bools r [] = []"
417
+ − 1728
427
+ − 1729
thm rsimp_SEQ.simps
+ − 1730
+ − 1731
lemma idiot:
+ − 1732
shows "rsimp_SEQ RONE r = r"
+ − 1733
apply(case_tac r)
+ − 1734
apply simp_all
+ − 1735
done
+ − 1736
+ − 1737
lemma no_dup_after_simp:
+ − 1738
shows "RALTS rs = rsimp r \<Longrightarrow> distinct rs"
+ − 1739
sorry
+ − 1740
+ − 1741
lemma no_further_dB_after_simp:
+ − 1742
shows "RALTS rs = rsimp r \<Longrightarrow> rdistinct rs {} = rs"
+ − 1743
sorry
+ − 1744
+ − 1745
lemma longlist_withstands_rsimp_alts:
+ − 1746
shows "length rs \<ge> 2 \<Longrightarrow> rsimp_ALTs rs = RALTS rs"
+ − 1747
sorry
+ − 1748
+ − 1749
lemma no_alt_short_list_after_simp:
+ − 1750
shows "RALTS rs = rsimp r \<Longrightarrow> rsimp_ALTs rs = RALTS rs"
+ − 1751
sorry
+ − 1752
+ − 1753
lemma idiot2:
+ − 1754
shows " \<lbrakk>r1 \<noteq> RZERO; r1 \<noteq> RONE;r2 \<noteq> RZERO\<rbrakk>
+ − 1755
\<Longrightarrow> rsimp_SEQ r1 r2 = RSEQ r1 r2"
+ − 1756
apply(case_tac r1)
+ − 1757
apply(case_tac r2)
+ − 1758
apply simp_all
+ − 1759
apply(case_tac r2)
+ − 1760
apply simp_all
+ − 1761
apply(case_tac r2)
+ − 1762
apply simp_all
+ − 1763
apply(case_tac r2)
+ − 1764
apply simp_all
+ − 1765
apply(case_tac r2)
+ − 1766
apply simp_all
+ − 1767
done
+ − 1768
+ − 1769
lemma rsimp_aalts_another:
+ − 1770
shows "\<forall>r \<in> (set (map rsimp ((RSEQ (rders r1 s) r2) #
+ − 1771
(rders_cond_list r2 (nullable_bools r1 (orderedPref s)) (orderedSuf s)) )) ). (rsize r) < N "
+ − 1772
sorry
+ − 1773
+ − 1774
+ − 1775
+ − 1776
lemma shape_derssimpseq_onechar:
+ − 1777
shows " rerase (bders_simp r [c]) = rerase (bsimp (bders r [c]))"
+ − 1778
and "rders_simp (RSEQ r1 r2) [c] =
+ − 1779
rsimp (RALTS ((RSEQ (rders r1 [c]) r2) #
+ − 1780
(rders_cond_list r2 (nullable_bools r1 (orderedPref [c])) (orderedSuf [c]))) )"
+ − 1781
apply simp
+ − 1782
apply(simp add: rders.simps)
+ − 1783
apply(case_tac "rsimp (rder c r1) = RZERO")
+ − 1784
apply auto
+ − 1785
apply(case_tac "rsimp (rder c r1) = RONE")
+ − 1786
apply auto
+ − 1787
apply(subgoal_tac "rsimp_SEQ RONE (rsimp r2) = rsimp r2")
+ − 1788
prefer 2
+ − 1789
using idiot
+ − 1790
apply simp
+ − 1791
apply(subgoal_tac "rsimp_SEQ RONE (rsimp r2) = rsimp_ALTs (rdistinct (rflts [rsimp r2]) {})")
+ − 1792
prefer 2
+ − 1793
apply auto
+ − 1794
apply(case_tac "rsimp r2")
+ − 1795
apply auto
+ − 1796
apply(subgoal_tac "rdistinct x5 {} = x5")
+ − 1797
prefer 2
+ − 1798
using no_further_dB_after_simp
+ − 1799
apply metis
+ − 1800
apply(subgoal_tac "rsimp_ALTs (rdistinct x5 {}) = rsimp_ALTs x5")
+ − 1801
prefer 2
+ − 1802
apply fastforce
+ − 1803
apply auto
+ − 1804
apply (metis no_alt_short_list_after_simp)
+ − 1805
apply (case_tac "rsimp r2 = RZERO")
+ − 1806
apply(subgoal_tac "rsimp_SEQ (rsimp (rder c r1)) (rsimp r2) = RZERO")
+ − 1807
prefer 2
+ − 1808
apply(case_tac "rsimp ( rder c r1)")
+ − 1809
apply auto
+ − 1810
apply(subgoal_tac "rsimp_SEQ (rsimp (rder c r1)) (rsimp r2) = RSEQ (rsimp (rder c r1)) (rsimp r2)")
+ − 1811
prefer 2
+ − 1812
apply auto
+ − 1813
apply(metis idiot2)
+ − 1814
done
+ − 1815
+ − 1816
lemma rders__onechar:
+ − 1817
shows " (rders_simp r [c]) = (rsimp (rders r [c]))"
+ − 1818
by simp
+ − 1819
+ − 1820
lemma rders_append:
+ − 1821
"rders c (s1 @ s2) = rders (rders c s1) s2"
+ − 1822
apply(induct s1 arbitrary: c s2)
+ − 1823
apply(simp_all)
+ − 1824
done
+ − 1825
+ − 1826
lemma rders_simp_append:
+ − 1827
"rders_simp c (s1 @ s2) = rders_simp (rders_simp c s1) s2"
+ − 1828
apply(induct s1 arbitrary: c s2)
+ − 1829
apply(simp_all)
+ − 1830
done
+ − 1831
+ − 1832
lemma inside_simp_removal:
+ − 1833
shows " rsimp (rder x (rsimp r)) = rsimp (rder x r)"
417
+ − 1834
427
+ − 1835
sorry
+ − 1836
+ − 1837
lemma set_related_list:
+ − 1838
shows "distinct rs \<Longrightarrow> length rs = card (set rs)"
+ − 1839
by (simp add: distinct_card)
+ − 1840
(*this section deals with the property of distinctBy: creates a list without duplicates*)
+ − 1841
lemma rdistinct_never_added_twice:
+ − 1842
shows "rdistinct (a # rs) {a} = rdistinct rs {a}"
+ − 1843
by force
+ − 1844
+ − 1845
+ − 1846
lemma rdistinct_does_the_job:
+ − 1847
shows "distinct (rdistinct rs s)"
+ − 1848
apply(induct rs arbitrary: s)
+ − 1849
apply simp
+ − 1850
apply simp
+ − 1851
sorry
+ − 1852
+ − 1853
+ − 1854
+ − 1855
+ − 1856
(*this section deals with the property of distinctBy: creates a list without duplicates*)
+ − 1857
+ − 1858
lemma rders_simp_same_simpders:
+ − 1859
shows "s \<noteq> [] \<Longrightarrow> rders_simp r s = rsimp (rders r s)"
+ − 1860
apply(induct s rule: rev_induct)
+ − 1861
apply simp
+ − 1862
apply(case_tac "xs = []")
+ − 1863
apply simp
+ − 1864
apply(simp add: rders_append rders_simp_append)
+ − 1865
using inside_simp_removal by blast
+ − 1866
422
+ − 1867
lemma shape_derssimp_seq:
427
+ − 1868
shows "\<lbrakk>s \<noteq>[] \<rbrakk> \<Longrightarrow> (rders_simp r s) = (rsimp (rders r s))"
421
+ − 1869
and "\<lbrakk>s \<noteq> []\<rbrakk> \<Longrightarrow> rders_simp (RSEQ r1 r2) s =
+ − 1870
rsimp (RALTS ((RSEQ (rders r1 s) r2) #
+ − 1871
(rders_cond_list r2 (nullable_bools r1 (orderedPref s)) (orderedSuf s))) )"
+ − 1872
apply(induct s arbitrary: r r1 r2 rule: rev_induct)
+ − 1873
apply simp
+ − 1874
apply simp
+ − 1875
apply(case_tac "xs = []")
+ − 1876
+ − 1877
apply (simp add: bders_simp_append )
+ − 1878
apply(subgoal_tac "rerase (bsimp (bder x (bders_simp r xs))) = (rsimp (rerase (bder x (bders_simp r xs)))) ")
+ − 1879
prefer 2
+ − 1880
apply (simp add: rerase_bsimp)
+ − 1881
apply(subgoal_tac "(rsimp (rerase (bder x (bders_simp r xs)))) = (rsimp (rder x (rerase (bders_simp r xs))))")
+ − 1882
+ − 1883
apply(subgoal_tac "xs \<noteq> [] \<Longrightarrow> rsimp (rder x (rerase (bders_simp r xs))) = rsimp (rder x (rerase (bsimp (bders r xs))))")
+ − 1884
prefer 2
427
+ − 1885
apply presburger
+ − 1886
apply(case_tac "xs = []")
421
+ − 1887
sorry
417
+ − 1888
427
+ − 1889
422
+ − 1890
lemma shape_derssimp_alts:
427
+ − 1891
shows "s \<noteq> [] \<Longrightarrow> rders_simp (RALTS rs) s = rsimp (RALTS (map (\<lambda>r. rders r s) rs))"
+ − 1892
apply(case_tac "s")
+ − 1893
apply simp
+ − 1894
apply simp
+ − 1895
sorry
428
+ − 1896
(*
+ − 1897
fun rexp_encode :: "rrexp \<Rightarrow> nat"
+ − 1898
where
+ − 1899
"rexp_encode RZERO = 0"
+ − 1900
|"rexp_encode RONE = 1"
+ − 1901
|"rexp_encode (RCHAR c) = 2"
+ − 1902
|"rexp_encode (RSEQ r1 r2) = ( 2 ^ (rexp_encode r1)) "
+ − 1903
*)
+ − 1904
lemma finite_chars:
+ − 1905
shows " \<exists>N. ( (\<forall>r \<in> (set rs). \<exists>c. r = RCHAR c) \<and> (distinct rs) \<longrightarrow> length rs < N)"
+ − 1906
apply(rule_tac x = "Suc 256" in exI)
+ − 1907
sorry
+ − 1908
430
+ − 1909
definition all_chars :: "int \<Rightarrow> char list"
+ − 1910
where "all_chars n = map char_of [0..n]"
428
+ − 1911
+ − 1912
fun rexp_enum :: "nat \<Rightarrow> rrexp list"
+ − 1913
where
+ − 1914
"rexp_enum 0 = []"
430
+ − 1915
|"rexp_enum (Suc 0) = RALTS [] # RZERO # (RONE # (map RCHAR (all_chars 255)))"
+ − 1916
|"rexp_enum (Suc n) = [(RSEQ r1 r2). r1 \<in> set (rexp_enum i) \<and> r2 \<in> set (rexp_enum j) \<and> i + j = n]"
+ − 1917
428
+ − 1918
+ − 1919
lemma finite_sized_rexp_forms_finite_set:
+ − 1920
shows " \<exists>SN. ( \<forall>r.( rsize r < N \<longrightarrow> r \<in> SN)) \<and> (finite SN)"
+ − 1921
apply(induct N)
+ − 1922
apply simp
+ − 1923
apply auto
+ − 1924
(*\<lbrakk>\<forall>r. rsize r < N \<longrightarrow> r \<in> SN; finite SN\<rbrakk> \<Longrightarrow> \<exists>SN. (\<forall>r. rsize r < Suc N \<longrightarrow> r \<in> SN) \<and> finite SN*)
+ − 1925
(* \<And>N. \<exists>SN. (\<forall>r. rsize r < N \<longrightarrow> r \<in> SN) \<and> finite SN \<Longrightarrow> \<exists>SN. (\<forall>r. rsize r < Suc N \<longrightarrow> r \<in> SN) \<and> finite SN*)
+ − 1926
sorry
422
+ − 1927
+ − 1928
421
+ − 1929
lemma finite_size_finite_regx:
428
+ − 1930
shows " \<exists>l. \<forall>rs. ((\<forall>r \<in> (set rs). rsize r < N) \<and> (distinct rs) \<longrightarrow> (length rs) < l) "
430
+ − 1931
sorry
421
+ − 1932
+ − 1933
(*below probably needs proved concurrently*)
+ − 1934
+ − 1935
lemma finite_r1r2_ders_list:
427
+ − 1936
shows "(\<forall>s. rsize (rders_simp r1 s) < N1 \<and> rsize (rders_simp r2 s) < N2)
+ − 1937
\<Longrightarrow> \<exists>l. \<forall>s.
+ − 1938
(length (rdistinct (map rsimp (rders_cond_list r2 (nullable_bools r1 (orderedPref s)) (orderedSuf s))) {}) ) < l "
421
+ − 1939
sorry
+ − 1940
427
+ − 1941
(*
+ − 1942
\<lbrakk>s \<noteq> []\<rbrakk> \<Longrightarrow> rders_simp (RSEQ r1 r2) s =
+ − 1943
rsimp (RALTS ((RSEQ (rders r1 s) r2) #
+ − 1944
(rders_cond_list r2 (nullable_bools r1 (orderedPref s)) (orderedSuf s))) )
+ − 1945
*)
+ − 1946
+ − 1947
lemma finite_width_alt:
+ − 1948
shows "(\<forall>s. rsize (rders_simp r1 s) < N1 \<and> rsize (rders_simp r2 s) < N2)
+ − 1949
\<Longrightarrow> \<exists>N3. \<forall>s. rsize (rsimp (RALTS ((RSEQ (rders r1 s) r2) #
+ − 1950
(rders_cond_list r2 (nullable_bools r1 (orderedPref s)) (orderedSuf s))) )) < N3"
+ − 1951
+ − 1952
sorry
+ − 1953
+ − 1954
+ − 1955
lemma empty_diff:
+ − 1956
shows "s = [] \<Longrightarrow>
+ − 1957
(rsize (rders_simp (RSEQ r1 r2) s)) \<le>
+ − 1958
(max
+ − 1959
(rsize (rsimp (RALTS (RSEQ (rders r1 s) r2 # rders_cond_list r2 (nullable_bools r1 (orderedPref s)) (orderedSuf s)))))
+ − 1960
(Suc (rsize r1 + rsize r2)) ) "
+ − 1961
apply simp
+ − 1962
done
+ − 1963
421
+ − 1964
lemma finite_seq:
+ − 1965
shows "(\<forall>s. rsize (rders_simp r1 s) < N1 \<and> rsize (rders_simp r2 s) < N2)
+ − 1966
\<Longrightarrow> \<exists>N3.\<forall>s.(rsize (rders_simp (RSEQ r1 r2) s)) < N3"
427
+ − 1967
apply(frule finite_width_alt)
+ − 1968
apply(erule exE)
+ − 1969
apply(rule_tac x = "max (N3+2) (Suc (Suc (rsize r1) + (rsize r2)))" in exI)
+ − 1970
apply(rule allI)
+ − 1971
apply(case_tac "s = []")
+ − 1972
prefer 2
+ − 1973
apply (simp add: less_SucI shape_derssimp_seq(2))
+ − 1974
apply (meson less_SucI less_max_iff_disj)
+ − 1975
apply simp
+ − 1976
done
+ − 1977
+ − 1978
+ − 1979
(*For star related error bound*)
+ − 1980
+ − 1981
lemma star_is_a_singleton_list_derc:
+ − 1982
shows " \<exists>Ss. rders_simp (RSTAR r) [c] = rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) Ss)"
+ − 1983
apply simp
+ − 1984
apply(rule_tac x = "[[c]]" in exI)
+ − 1985
apply auto
+ − 1986
done
+ − 1987
+ − 1988
lemma rder_rsimp_ALTs_commute:
+ − 1989
shows " (rder x (rsimp_ALTs rs)) = rsimp_ALTs (map (rder x) rs)"
+ − 1990
apply(induct rs)
+ − 1991
apply simp
+ − 1992
apply(case_tac rs)
+ − 1993
apply simp
+ − 1994
apply auto
+ − 1995
done
+ − 1996
+ − 1997
lemma double_nested_ALTs_under_rsimp:
+ − 1998
shows "rsimp (rsimp_ALTs ((RALTS rs1) # rs)) = rsimp (RALTS (rs1 @ rs))"
+ − 1999
apply(case_tac rs1)
+ − 2000
apply simp
+ − 2001
+ − 2002
apply (metis list.simps(8) list.simps(9) neq_Nil_conv rdistinct.simps(1) rflts.simps(1) rflts.simps(2) rsimp.simps(2) rsimp_ALTs.simps(1) rsimp_ALTs.simps(2) rsimp_ALTs.simps(3))
+ − 2003
apply(case_tac rs)
+ − 2004
apply simp
+ − 2005
apply auto
421
+ − 2006
sorry
+ − 2007
427
+ − 2008
lemma star_seqs_produce_star_seqs:
+ − 2009
shows "rsimp (rsimp_ALTs (map (rder x \<circ> (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r))) Ss))
+ − 2010
= rsimp (rsimp_ALTs (map ( (\<lambda>s1. rder x (rsimp_SEQ (rders_simp r s1) (RSTAR r)))) Ss))"
+ − 2011
by (meson comp_apply)
+ − 2012
+ − 2013
lemma der_seqstar_res:
428
+ − 2014
shows "rder x (RSEQ r1 r2) = RSEQ r3 r4"
427
+ − 2015
+ − 2016
+ − 2017
lemma linearity_of_list_of_star_or_starseqs:
+ − 2018
shows "\<exists>Ssa. rsimp (rder x (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) Ss))) =
+ − 2019
rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) Ssa)"
+ − 2020
apply(simp add: rder_rsimp_ALTs_commute)
+ − 2021
apply(induct Ss)
+ − 2022
apply simp
+ − 2023
apply (metis list.simps(8) rsimp_ALTs.simps(1))
+ − 2024
428
+ − 2025
427
+ − 2026
sorry
+ − 2027
+ − 2028
lemma starder_is_a_list_of_stars_or_starseqs:
+ − 2029
shows "s \<noteq> [] \<Longrightarrow> \<exists>Ss. rders_simp (RSTAR r) s = rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) Ss)"
+ − 2030
apply(induct s rule: rev_induct)
+ − 2031
apply simp
+ − 2032
apply(case_tac "xs = []")
+ − 2033
using star_is_a_singleton_list_derc
+ − 2034
apply(simp)
+ − 2035
apply auto
+ − 2036
apply(simp add: rders_simp_append)
+ − 2037
using linearity_of_list_of_star_or_starseqs by blast
+ − 2038
421
+ − 2039
422
+ − 2040
lemma finite_star:
+ − 2041
shows "(\<forall>s. rsize (rders_simp r0 s) < N0 )
+ − 2042
\<Longrightarrow> \<exists>N3. \<forall>s.(rsize (rders_simp (RSTAR r0) s)) < N3"
427
+ − 2043
422
+ − 2044
sorry
+ − 2045
+ − 2046
+ − 2047
lemma rderssimp_zero:
+ − 2048
shows"rders_simp RZERO s = RZERO"
+ − 2049
apply(induction s)
+ − 2050
apply simp
+ − 2051
by simp
+ − 2052
+ − 2053
lemma rderssimp_one:
+ − 2054
shows"rders_simp RONE (a # s) = RZERO"
+ − 2055
apply(induction s)
+ − 2056
apply simp
+ − 2057
by simp
+ − 2058
+ − 2059
lemma rderssimp_char:
+ − 2060
shows "rders_simp (RCHAR c) s = RONE \<or> rders_simp (RCHAR c) s = RZERO \<or> rders_simp (RCHAR c) s = (RCHAR c)"
+ − 2061
apply auto
+ − 2062
by (metis rder.simps(2) rder.simps(3) rders_simp.elims rders_simp.simps(2) rderssimp_one rsimp.simps(4))
+ − 2063
421
+ − 2064
lemma finite_size_ders:
422
+ − 2065
shows " \<exists>Nr. \<forall>s. rsize (rders_simp r s) < Nr"
+ − 2066
apply(induct r rule: rrexp.induct)
+ − 2067
apply auto
+ − 2068
apply(rule_tac x = "2" in exI)
+ − 2069
using rderssimp_zero rsize.simps(1) apply presburger
+ − 2070
apply(rule_tac x = "2" in exI)
+ − 2071
apply (metis Suc_1 lessI rders_simp.elims rderssimp_one rsize.simps(1) rsize.simps(2))
+ − 2072
apply(rule_tac x = "2" in meta_spec)
+ − 2073
apply (metis lessI rderssimp_char rsize.simps(1) rsize.simps(2) rsize.simps(3))
+ − 2074
+ − 2075
using finite_seq apply blast
+ − 2076
prefer 2
+ − 2077
+ − 2078
apply (simp add: finite_star)
421
+ − 2079
sorry
409
+ − 2080
+ − 2081
+ − 2082
unused_thms
417
+ − 2083
lemma seq_ders_shape:
+ − 2084
shows "E"
+ − 2085
+ − 2086
oops
+ − 2087
+ − 2088
(*rsimp (rders (RSEQ r1 r2) s) =
+ − 2089
rsimp RALT [RSEQ (rders r1 s) r2, rders r2 si, ...]
+ − 2090
where si is the i-th shortest suffix of s such that si \<in> L r2"
+ − 2091
*)
409
+ − 2092
+ − 2093
+ − 2094
inductive aggressive:: "arexp \<Rightarrow> arexp \<Rightarrow> bool" ("_ \<leadsto>? _" [99, 99] 99)
+ − 2095
where
+ − 2096
"ASEQ bs (AALTs bs1 rs) r \<leadsto>? AALTs (bs@bs1) (map (\<lambda>r'. ASEQ [] r' r) rs) "
+ − 2097
+ − 2098
+ − 2099
+ − 2100
end