365
+ − 1
+ − 2
theory BitCodedCT
+ − 3
imports "Lexer"
+ − 4
begin
+ − 5
+ − 6
section \<open>Bit-Encodings\<close>
+ − 7
+ − 8
datatype bit = Z | S
+ − 9
+ − 10
fun
+ − 11
code :: "val \<Rightarrow> bit list"
+ − 12
where
+ − 13
"code Void = []"
+ − 14
| "code (Char c) = []"
+ − 15
| "code (Left v) = Z # (code v)"
+ − 16
| "code (Right v) = S # (code v)"
+ − 17
| "code (Seq v1 v2) = (code v1) @ (code v2)"
+ − 18
| "code (Stars []) = [S]"
+ − 19
| "code (Stars (v # vs)) = (Z # code v) @ code (Stars vs)"
+ − 20
+ − 21
+ − 22
fun
+ − 23
Stars_add :: "val \<Rightarrow> val \<Rightarrow> val"
+ − 24
where
+ − 25
"Stars_add v (Stars vs) = Stars (v # vs)"
+ − 26
+ − 27
function
+ − 28
decode' :: "bit list \<Rightarrow> rexp \<Rightarrow> (val * bit list)"
+ − 29
where
+ − 30
"decode' ds ZERO = (Void, [])"
+ − 31
| "decode' ds ONE = (Void, ds)"
+ − 32
| "decode' ds (CHAR d) = (Char d, ds)"
+ − 33
| "decode' [] (ALT r1 r2) = (Void, [])"
+ − 34
| "decode' (Z # ds) (ALT r1 r2) = (let (v, ds') = decode' ds r1 in (Left v, ds'))"
+ − 35
| "decode' (S # ds) (ALT r1 r2) = (let (v, ds') = decode' ds r2 in (Right v, ds'))"
+ − 36
| "decode' ds (SEQ r1 r2) = (let (v1, ds') = decode' ds r1 in
+ − 37
let (v2, ds'') = decode' ds' r2 in (Seq v1 v2, ds''))"
+ − 38
| "decode' [] (STAR r) = (Void, [])"
+ − 39
| "decode' (S # ds) (STAR r) = (Stars [], ds)"
+ − 40
| "decode' (Z # ds) (STAR r) = (let (v, ds') = decode' ds r in
+ − 41
let (vs, ds'') = decode' ds' (STAR r)
+ − 42
in (Stars_add v vs, ds''))"
+ − 43
by pat_completeness auto
+ − 44
+ − 45
lemma decode'_smaller:
+ − 46
assumes "decode'_dom (ds, r)"
+ − 47
shows "length (snd (decode' ds r)) \<le> length ds"
+ − 48
using assms
+ − 49
apply(induct ds r)
+ − 50
apply(auto simp add: decode'.psimps split: prod.split)
+ − 51
using dual_order.trans apply blast
+ − 52
by (meson dual_order.trans le_SucI)
+ − 53
+ − 54
termination "decode'"
+ − 55
apply(relation "inv_image (measure(%cs. size cs) <*lex*> measure(%s. size s)) (%(ds,r). (r,ds))")
+ − 56
apply(auto dest!: decode'_smaller)
+ − 57
by (metis less_Suc_eq_le snd_conv)
+ − 58
+ − 59
definition
+ − 60
decode :: "bit list \<Rightarrow> rexp \<Rightarrow> val option"
+ − 61
where
+ − 62
"decode ds r \<equiv> (let (v, ds') = decode' ds r
+ − 63
in (if ds' = [] then Some v else None))"
+ − 64
+ − 65
lemma decode'_code_Stars:
+ − 66
assumes "\<forall>v\<in>set vs. \<Turnstile> v : r \<and> (\<forall>x. decode' (code v @ x) r = (v, x)) \<and> flat v \<noteq> []"
+ − 67
shows "decode' (code (Stars vs) @ ds) (STAR r) = (Stars vs, ds)"
+ − 68
using assms
+ − 69
apply(induct vs)
+ − 70
apply(auto)
+ − 71
done
+ − 72
+ − 73
lemma decode'_code:
+ − 74
assumes "\<Turnstile> v : r"
+ − 75
shows "decode' ((code v) @ ds) r = (v, ds)"
+ − 76
using assms
+ − 77
apply(induct v r arbitrary: ds)
+ − 78
apply(auto)
+ − 79
using decode'_code_Stars by blast
+ − 80
+ − 81
lemma decode_code:
+ − 82
assumes "\<Turnstile> v : r"
+ − 83
shows "decode (code v) r = Some v"
+ − 84
using assms unfolding decode_def
+ − 85
by (smt append_Nil2 decode'_code old.prod.case)
+ − 86
+ − 87
+ − 88
section {* Annotated Regular Expressions *}
+ − 89
+ − 90
datatype arexp =
+ − 91
AZERO
+ − 92
| AONE "bit list"
+ − 93
| ACHAR "bit list" char
+ − 94
| ASEQ "bit list" arexp arexp
+ − 95
| AALTs "bit list" "arexp list"
+ − 96
| ASTAR "bit list" arexp
+ − 97
+ − 98
abbreviation
+ − 99
"AALT bs r1 r2 \<equiv> AALTs bs [r1, r2]"
+ − 100
+ − 101
fun asize :: "arexp \<Rightarrow> nat" where
+ − 102
"asize AZERO = 1"
+ − 103
| "asize (AONE cs) = 1"
+ − 104
| "asize (ACHAR cs c) = 1"
+ − 105
| "asize (AALTs cs rs) = Suc (sum_list (map asize rs))"
+ − 106
| "asize (ASEQ cs r1 r2) = Suc (asize r1 + asize r2)"
+ − 107
| "asize (ASTAR cs r) = Suc (asize r)"
+ − 108
+ − 109
fun
+ − 110
erase :: "arexp \<Rightarrow> rexp"
+ − 111
where
+ − 112
"erase AZERO = ZERO"
+ − 113
| "erase (AONE _) = ONE"
+ − 114
| "erase (ACHAR _ c) = CHAR c"
+ − 115
| "erase (AALTs _ []) = ZERO"
+ − 116
| "erase (AALTs _ [r]) = (erase r)"
+ − 117
| "erase (AALTs bs (r#rs)) = ALT (erase r) (erase (AALTs bs rs))"
+ − 118
| "erase (ASEQ _ r1 r2) = SEQ (erase r1) (erase r2)"
+ − 119
| "erase (ASTAR _ r) = STAR (erase r)"
+ − 120
+ − 121
lemma decode_code_erase:
+ − 122
assumes "\<Turnstile> v : (erase a)"
+ − 123
shows "decode (code v) (erase a) = Some v"
+ − 124
using assms
+ − 125
by (simp add: decode_code)
+ − 126
+ − 127
+ − 128
fun nonalt :: "arexp \<Rightarrow> bool"
+ − 129
where
+ − 130
"nonalt (AALTs bs2 rs) = False"
+ − 131
| "nonalt r = True"
+ − 132
+ − 133
+ − 134
fun good :: "arexp \<Rightarrow> bool" where
+ − 135
"good AZERO = False"
+ − 136
| "good (AONE cs) = True"
+ − 137
| "good (ACHAR cs c) = True"
+ − 138
| "good (AALTs cs []) = False"
+ − 139
| "good (AALTs cs [r]) = False"
+ − 140
| "good (AALTs cs (r1#r2#rs)) = (\<forall>r' \<in> set (r1#r2#rs). good r' \<and> nonalt r')"
+ − 141
| "good (ASEQ _ AZERO _) = False"
+ − 142
| "good (ASEQ _ (AONE _) _) = False"
+ − 143
| "good (ASEQ _ _ AZERO) = False"
+ − 144
| "good (ASEQ cs r1 r2) = (good r1 \<and> good r2)"
+ − 145
| "good (ASTAR cs r) = True"
+ − 146
+ − 147
+ − 148
+ − 149
+ − 150
fun fuse :: "bit list \<Rightarrow> arexp \<Rightarrow> arexp" where
+ − 151
"fuse bs AZERO = AZERO"
+ − 152
| "fuse bs (AONE cs) = AONE (bs @ cs)"
+ − 153
| "fuse bs (ACHAR cs c) = ACHAR (bs @ cs) c"
+ − 154
| "fuse bs (AALTs cs rs) = AALTs (bs @ cs) rs"
+ − 155
| "fuse bs (ASEQ cs r1 r2) = ASEQ (bs @ cs) r1 r2"
+ − 156
| "fuse bs (ASTAR cs r) = ASTAR (bs @ cs) r"
+ − 157
+ − 158
lemma fuse_append:
+ − 159
shows "fuse (bs1 @ bs2) r = fuse bs1 (fuse bs2 r)"
+ − 160
apply(induct r)
+ − 161
apply(auto)
+ − 162
done
+ − 163
+ − 164
+ − 165
fun intern :: "rexp \<Rightarrow> arexp" where
+ − 166
"intern ZERO = AZERO"
+ − 167
| "intern ONE = AONE []"
+ − 168
| "intern (CHAR c) = ACHAR [] c"
+ − 169
| "intern (ALT r1 r2) = AALT [] (fuse [Z] (intern r1))
+ − 170
(fuse [S] (intern r2))"
+ − 171
| "intern (SEQ r1 r2) = ASEQ [] (intern r1) (intern r2)"
+ − 172
| "intern (STAR r) = ASTAR [] (intern r)"
+ − 173
+ − 174
+ − 175
fun retrieve :: "arexp \<Rightarrow> val \<Rightarrow> bit list" where
+ − 176
"retrieve (AONE bs) Void = bs"
+ − 177
| "retrieve (ACHAR bs c) (Char d) = bs"
+ − 178
| "retrieve (AALTs bs [r]) v = bs @ retrieve r v"
+ − 179
| "retrieve (AALTs bs (r#rs)) (Left v) = bs @ retrieve r v"
+ − 180
| "retrieve (AALTs bs (r#rs)) (Right v) = bs @ retrieve (AALTs [] rs) v"
+ − 181
| "retrieve (ASEQ bs r1 r2) (Seq v1 v2) = bs @ retrieve r1 v1 @ retrieve r2 v2"
+ − 182
| "retrieve (ASTAR bs r) (Stars []) = bs @ [S]"
+ − 183
| "retrieve (ASTAR bs r) (Stars (v#vs)) =
+ − 184
bs @ [Z] @ retrieve r v @ retrieve (ASTAR [] r) (Stars vs)"
+ − 185
+ − 186
+ − 187
+ − 188
fun
+ − 189
bnullable :: "arexp \<Rightarrow> bool"
+ − 190
where
+ − 191
"bnullable (AZERO) = False"
+ − 192
| "bnullable (AONE bs) = True"
+ − 193
| "bnullable (ACHAR bs c) = False"
+ − 194
| "bnullable (AALTs bs rs) = (\<exists>r \<in> set rs. bnullable r)"
+ − 195
| "bnullable (ASEQ bs r1 r2) = (bnullable r1 \<and> bnullable r2)"
+ − 196
| "bnullable (ASTAR bs r) = True"
+ − 197
+ − 198
fun
+ − 199
bmkeps :: "arexp \<Rightarrow> bit list"
+ − 200
where
+ − 201
"bmkeps(AONE bs) = bs"
+ − 202
| "bmkeps(ASEQ bs r1 r2) = bs @ (bmkeps r1) @ (bmkeps r2)"
+ − 203
| "bmkeps(AALTs bs [r]) = bs @ (bmkeps r)"
+ − 204
| "bmkeps(AALTs bs (r#rs)) = (if bnullable(r) then bs @ (bmkeps r) else (bmkeps (AALTs bs rs)))"
+ − 205
| "bmkeps(ASTAR bs r) = bs @ [S]"
+ − 206
+ − 207
+ − 208
fun
+ − 209
bder :: "char \<Rightarrow> arexp \<Rightarrow> arexp"
+ − 210
where
+ − 211
"bder c (AZERO) = AZERO"
+ − 212
| "bder c (AONE bs) = AZERO"
+ − 213
| "bder c (ACHAR bs d) = (if c = d then AONE bs else AZERO)"
+ − 214
| "bder c (AALTs bs rs) = AALTs bs (map (bder c) rs)"
+ − 215
| "bder c (ASEQ bs r1 r2) =
+ − 216
(if bnullable r1
+ − 217
then AALT bs (ASEQ [] (bder c r1) r2) (fuse (bmkeps r1) (bder c r2))
+ − 218
else ASEQ bs (bder c r1) r2)"
+ − 219
| "bder c (ASTAR bs r) = ASEQ bs (fuse [Z] (bder c r)) (ASTAR [] r)"
+ − 220
+ − 221
+ − 222
fun
+ − 223
bders :: "arexp \<Rightarrow> string \<Rightarrow> arexp"
+ − 224
where
+ − 225
"bders r [] = r"
+ − 226
| "bders r (c#s) = bders (bder c r) s"
+ − 227
+ − 228
lemma bders_append:
+ − 229
"bders r (s1 @ s2) = bders (bders r s1) s2"
+ − 230
apply(induct s1 arbitrary: r s2)
+ − 231
apply(simp_all)
+ − 232
done
+ − 233
+ − 234
lemma bnullable_correctness:
+ − 235
shows "nullable (erase r) = bnullable r"
+ − 236
apply(induct r rule: erase.induct)
+ − 237
apply(simp_all)
+ − 238
done
+ − 239
+ − 240
lemma erase_fuse:
+ − 241
shows "erase (fuse bs r) = erase r"
+ − 242
apply(induct r rule: erase.induct)
+ − 243
apply(simp_all)
+ − 244
done
+ − 245
+ − 246
lemma erase_intern [simp]:
+ − 247
shows "erase (intern r) = r"
+ − 248
apply(induct r)
+ − 249
apply(simp_all add: erase_fuse)
+ − 250
done
+ − 251
+ − 252
lemma erase_bder [simp]:
+ − 253
shows "erase (bder a r) = der a (erase r)"
+ − 254
apply(induct r rule: erase.induct)
+ − 255
apply(simp_all add: erase_fuse bnullable_correctness)
+ − 256
done
+ − 257
+ − 258
lemma erase_bders [simp]:
+ − 259
shows "erase (bders r s) = ders s (erase r)"
+ − 260
apply(induct s arbitrary: r )
+ − 261
apply(simp_all)
+ − 262
done
+ − 263
+ − 264
lemma retrieve_encode_STARS:
+ − 265
assumes "\<forall>v\<in>set vs. \<Turnstile> v : r \<and> code v = retrieve (intern r) v"
+ − 266
shows "code (Stars vs) = retrieve (ASTAR [] (intern r)) (Stars vs)"
+ − 267
using assms
+ − 268
apply(induct vs)
+ − 269
apply(simp_all)
+ − 270
done
+ − 271
+ − 272
lemma retrieve_fuse2:
+ − 273
assumes "\<Turnstile> v : (erase r)"
+ − 274
shows "retrieve (fuse bs r) v = bs @ retrieve r v"
+ − 275
using assms
+ − 276
apply(induct r arbitrary: v bs)
+ − 277
apply(auto elim: Prf_elims)[4]
+ − 278
defer
+ − 279
using retrieve_encode_STARS
+ − 280
apply(auto elim!: Prf_elims)[1]
+ − 281
apply(case_tac vs)
+ − 282
apply(simp)
+ − 283
apply(simp)
+ − 284
(* AALTs case *)
+ − 285
apply(simp)
+ − 286
apply(case_tac x2a)
+ − 287
apply(simp)
+ − 288
apply(auto elim!: Prf_elims)[1]
+ − 289
apply(simp)
+ − 290
apply(case_tac list)
+ − 291
apply(simp)
+ − 292
apply(auto)
+ − 293
apply(auto elim!: Prf_elims)[1]
+ − 294
done
+ − 295
+ − 296
lemma retrieve_fuse:
+ − 297
assumes "\<Turnstile> v : r"
+ − 298
shows "retrieve (fuse bs (intern r)) v = bs @ retrieve (intern r) v"
+ − 299
using assms
+ − 300
by (simp_all add: retrieve_fuse2)
+ − 301
+ − 302
+ − 303
lemma retrieve_code:
+ − 304
assumes "\<Turnstile> v : r"
+ − 305
shows "code v = retrieve (intern r) v"
+ − 306
using assms
+ − 307
apply(induct v r )
+ − 308
apply(simp_all add: retrieve_fuse retrieve_encode_STARS)
+ − 309
done
+ − 310
+ − 311
lemma r:
+ − 312
assumes "bnullable (AALTs bs (a # rs))"
+ − 313
shows "bnullable a \<or> (\<not> bnullable a \<and> bnullable (AALTs bs rs))"
+ − 314
using assms
+ − 315
apply(induct rs)
+ − 316
apply(auto)
+ − 317
done
+ − 318
+ − 319
lemma r0:
+ − 320
assumes "bnullable a"
+ − 321
shows "bmkeps (AALTs bs (a # rs)) = bs @ (bmkeps a)"
+ − 322
using assms
+ − 323
by (metis bmkeps.simps(3) bmkeps.simps(4) list.exhaust)
+ − 324
+ − 325
lemma r1:
+ − 326
assumes "\<not> bnullable a" "bnullable (AALTs bs rs)"
+ − 327
shows "bmkeps (AALTs bs (a # rs)) = bmkeps (AALTs bs rs)"
+ − 328
using assms
+ − 329
apply(induct rs)
+ − 330
apply(auto)
+ − 331
done
+ − 332
+ − 333
lemma r2:
+ − 334
assumes "x \<in> set rs" "bnullable x"
+ − 335
shows "bnullable (AALTs bs rs)"
+ − 336
using assms
+ − 337
apply(induct rs)
+ − 338
apply(auto)
+ − 339
done
+ − 340
+ − 341
lemma r3:
+ − 342
assumes "\<not> bnullable r"
+ − 343
" \<exists> x \<in> set rs. bnullable x"
+ − 344
shows "retrieve (AALTs bs rs) (mkeps (erase (AALTs bs rs))) =
+ − 345
retrieve (AALTs bs (r # rs)) (mkeps (erase (AALTs bs (r # rs))))"
+ − 346
using assms
+ − 347
apply(induct rs arbitrary: r bs)
+ − 348
apply(auto)[1]
+ − 349
apply(auto)
+ − 350
using bnullable_correctness apply blast
+ − 351
apply(auto simp add: bnullable_correctness mkeps_nullable retrieve_fuse2)
+ − 352
apply(subst retrieve_fuse2[symmetric])
+ − 353
apply (smt bnullable.simps(4) bnullable_correctness erase.simps(5) erase.simps(6) insert_iff list.exhaust list.set(2) mkeps.simps(3) mkeps_nullable)
+ − 354
apply(simp)
+ − 355
apply(case_tac "bnullable a")
+ − 356
apply (smt append_Nil2 bnullable.simps(4) bnullable_correctness erase.simps(5) erase.simps(6) fuse.simps(4) insert_iff list.exhaust list.set(2) mkeps.simps(3) mkeps_nullable retrieve_fuse2)
+ − 357
apply(drule_tac x="a" in meta_spec)
+ − 358
apply(drule_tac x="bs" in meta_spec)
+ − 359
apply(drule meta_mp)
+ − 360
apply(simp)
+ − 361
apply(drule meta_mp)
+ − 362
apply(auto)
+ − 363
apply(subst retrieve_fuse2[symmetric])
+ − 364
apply(case_tac rs)
+ − 365
apply(simp)
+ − 366
apply(auto)[1]
+ − 367
apply (simp add: bnullable_correctness)
+ − 368
apply (metis append_Nil2 bnullable_correctness erase_fuse fuse.simps(4) list.set_intros(1) mkeps.simps(3) mkeps_nullable nullable.simps(4) r2)
+ − 369
apply (simp add: bnullable_correctness)
+ − 370
apply (metis append_Nil2 bnullable_correctness erase.simps(6) erase_fuse fuse.simps(4) list.set_intros(2) mkeps.simps(3) mkeps_nullable r2)
+ − 371
apply(simp)
+ − 372
done
+ − 373
+ − 374
+ − 375
lemma t:
+ − 376
assumes "\<forall>r \<in> set rs. nullable (erase r) \<longrightarrow> bmkeps r = retrieve r (mkeps (erase r))"
+ − 377
"nullable (erase (AALTs bs rs))"
+ − 378
shows " bmkeps (AALTs bs rs) = retrieve (AALTs bs rs) (mkeps (erase (AALTs bs rs)))"
+ − 379
using assms
+ − 380
apply(induct rs arbitrary: bs)
+ − 381
apply(simp)
+ − 382
apply(auto simp add: bnullable_correctness)
+ − 383
apply(case_tac rs)
+ − 384
apply(auto simp add: bnullable_correctness)[2]
+ − 385
apply(subst r1)
+ − 386
apply(simp)
+ − 387
apply(rule r2)
+ − 388
apply(assumption)
+ − 389
apply(simp)
+ − 390
apply(drule_tac x="bs" in meta_spec)
+ − 391
apply(drule meta_mp)
+ − 392
apply(auto)[1]
+ − 393
prefer 2
+ − 394
apply(case_tac "bnullable a")
+ − 395
apply(subst r0)
+ − 396
apply blast
+ − 397
apply(subgoal_tac "nullable (erase a)")
+ − 398
prefer 2
+ − 399
using bnullable_correctness apply blast
+ − 400
apply (metis (no_types, lifting) erase.simps(5) erase.simps(6) list.exhaust mkeps.simps(3) retrieve.simps(3) retrieve.simps(4))
+ − 401
apply(subst r1)
+ − 402
apply(simp)
+ − 403
using r2 apply blast
+ − 404
apply(drule_tac x="bs" in meta_spec)
+ − 405
apply(drule meta_mp)
+ − 406
apply(auto)[1]
+ − 407
apply(simp)
+ − 408
using r3 apply blast
+ − 409
apply(auto)
+ − 410
using r3 by blast
+ − 411
+ − 412
lemma bmkeps_retrieve:
+ − 413
assumes "nullable (erase r)"
+ − 414
shows "bmkeps r = retrieve r (mkeps (erase r))"
+ − 415
using assms
+ − 416
apply(induct r)
+ − 417
apply(simp)
+ − 418
apply(simp)
+ − 419
apply(simp)
+ − 420
apply(simp)
+ − 421
defer
+ − 422
apply(simp)
+ − 423
apply(rule t)
+ − 424
apply(auto)
+ − 425
done
+ − 426
+ − 427
lemma bder_retrieve:
+ − 428
assumes "\<Turnstile> v : der c (erase r)"
+ − 429
shows "retrieve (bder c r) v = retrieve r (injval (erase r) c v)"
+ − 430
using assms
+ − 431
apply(induct r arbitrary: v rule: erase.induct)
+ − 432
apply(simp)
+ − 433
apply(erule Prf_elims)
+ − 434
apply(simp)
+ − 435
apply(erule Prf_elims)
+ − 436
apply(simp)
+ − 437
apply(case_tac "c = ca")
+ − 438
apply(simp)
+ − 439
apply(erule Prf_elims)
+ − 440
apply(simp)
+ − 441
apply(simp)
+ − 442
apply(erule Prf_elims)
+ − 443
apply(simp)
+ − 444
apply(erule Prf_elims)
+ − 445
apply(simp)
+ − 446
apply(simp)
+ − 447
apply(rename_tac "r\<^sub>1" "r\<^sub>2" rs v)
+ − 448
apply(erule Prf_elims)
+ − 449
apply(simp)
+ − 450
apply(simp)
+ − 451
apply(case_tac rs)
+ − 452
apply(simp)
+ − 453
apply(simp)
+ − 454
apply (smt Prf_elims(3) injval.simps(2) injval.simps(3) retrieve.simps(4) retrieve.simps(5) same_append_eq)
+ − 455
apply(simp)
+ − 456
apply(case_tac "nullable (erase r1)")
+ − 457
apply(simp)
+ − 458
apply(erule Prf_elims)
+ − 459
apply(subgoal_tac "bnullable r1")
+ − 460
prefer 2
+ − 461
using bnullable_correctness apply blast
+ − 462
apply(simp)
+ − 463
apply(erule Prf_elims)
+ − 464
apply(simp)
+ − 465
apply(subgoal_tac "bnullable r1")
+ − 466
prefer 2
+ − 467
using bnullable_correctness apply blast
+ − 468
apply(simp)
+ − 469
apply(simp add: retrieve_fuse2)
+ − 470
apply(simp add: bmkeps_retrieve)
+ − 471
apply(simp)
+ − 472
apply(erule Prf_elims)
+ − 473
apply(simp)
+ − 474
using bnullable_correctness apply blast
+ − 475
apply(rename_tac bs r v)
+ − 476
apply(simp)
+ − 477
apply(erule Prf_elims)
+ − 478
apply(clarify)
+ − 479
apply(erule Prf_elims)
+ − 480
apply(clarify)
+ − 481
apply(subst injval.simps)
+ − 482
apply(simp del: retrieve.simps)
+ − 483
apply(subst retrieve.simps)
+ − 484
apply(subst retrieve.simps)
+ − 485
apply(simp)
+ − 486
apply(simp add: retrieve_fuse2)
+ − 487
done
+ − 488
+ − 489
+ − 490
+ − 491
lemma MAIN_decode:
+ − 492
assumes "\<Turnstile> v : ders s r"
+ − 493
shows "Some (flex r id s v) = decode (retrieve (bders (intern r) s) v) r"
+ − 494
using assms
+ − 495
proof (induct s arbitrary: v rule: rev_induct)
+ − 496
case Nil
+ − 497
have "\<Turnstile> v : ders [] r" by fact
+ − 498
then have "\<Turnstile> v : r" by simp
+ − 499
then have "Some v = decode (retrieve (intern r) v) r"
+ − 500
using decode_code retrieve_code by auto
+ − 501
then show "Some (flex r id [] v) = decode (retrieve (bders (intern r) []) v) r"
+ − 502
by simp
+ − 503
next
+ − 504
case (snoc c s v)
+ − 505
have IH: "\<And>v. \<Turnstile> v : ders s r \<Longrightarrow>
+ − 506
Some (flex r id s v) = decode (retrieve (bders (intern r) s) v) r" by fact
+ − 507
have asm: "\<Turnstile> v : ders (s @ [c]) r" by fact
+ − 508
then have asm2: "\<Turnstile> injval (ders s r) c v : ders s r"
+ − 509
by (simp add: Prf_injval ders_append)
+ − 510
have "Some (flex r id (s @ [c]) v) = Some (flex r id s (injval (ders s r) c v))"
+ − 511
by (simp add: flex_append)
+ − 512
also have "... = decode (retrieve (bders (intern r) s) (injval (ders s r) c v)) r"
+ − 513
using asm2 IH by simp
+ − 514
also have "... = decode (retrieve (bder c (bders (intern r) s)) v) r"
+ − 515
using asm by (simp_all add: bder_retrieve ders_append)
+ − 516
finally show "Some (flex r id (s @ [c]) v) =
+ − 517
decode (retrieve (bders (intern r) (s @ [c])) v) r" by (simp add: bders_append)
+ − 518
qed
+ − 519
+ − 520
+ − 521
definition blex where
+ − 522
"blex a s \<equiv> if bnullable (bders a s) then Some (bmkeps (bders a s)) else None"
+ − 523
+ − 524
+ − 525
+ − 526
definition blexer where
+ − 527
"blexer r s \<equiv> if bnullable (bders (intern r) s) then
+ − 528
decode (bmkeps (bders (intern r) s)) r else None"
+ − 529
+ − 530
lemma blexer_correctness:
+ − 531
shows "blexer r s = lexer r s"
+ − 532
proof -
+ − 533
{ define bds where "bds \<equiv> bders (intern r) s"
+ − 534
define ds where "ds \<equiv> ders s r"
+ − 535
assume asm: "nullable ds"
+ − 536
have era: "erase bds = ds"
+ − 537
unfolding ds_def bds_def by simp
+ − 538
have mke: "\<Turnstile> mkeps ds : ds"
+ − 539
using asm by (simp add: mkeps_nullable)
+ − 540
have "decode (bmkeps bds) r = decode (retrieve bds (mkeps ds)) r"
+ − 541
using bmkeps_retrieve
+ − 542
using asm era by (simp add: bmkeps_retrieve)
+ − 543
also have "... = Some (flex r id s (mkeps ds))"
+ − 544
using mke by (simp_all add: MAIN_decode ds_def bds_def)
+ − 545
finally have "decode (bmkeps bds) r = Some (flex r id s (mkeps ds))"
+ − 546
unfolding bds_def ds_def .
+ − 547
}
+ − 548
then show "blexer r s = lexer r s"
+ − 549
unfolding blexer_def lexer_flex
+ − 550
apply(subst bnullable_correctness[symmetric])
+ − 551
apply(simp)
+ − 552
done
+ − 553
qed
+ − 554
+ − 555
+ − 556
fun distinctBy :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b set \<Rightarrow> 'a list"
+ − 557
where
+ − 558
"distinctBy [] f acc = []"
+ − 559
| "distinctBy (x#xs) f acc =
+ − 560
(if (f x) \<in> acc then distinctBy xs f acc
+ − 561
else x # (distinctBy xs f ({f x} \<union> acc)))"
+ − 562
+ − 563
fun flts :: "arexp list \<Rightarrow> arexp list"
+ − 564
where
+ − 565
"flts [] = []"
+ − 566
| "flts (AZERO # rs) = flts rs"
+ − 567
| "flts ((AALTs bs rs1) # rs) = (map (fuse bs) rs1) @ flts rs"
+ − 568
| "flts (r1 # rs) = r1 # flts rs"
+ − 569
+ − 570
+ − 571
+ − 572
+ − 573
fun li :: "bit list \<Rightarrow> arexp list \<Rightarrow> arexp"
+ − 574
where
+ − 575
"li _ [] = AZERO"
+ − 576
| "li bs [a] = fuse bs a"
+ − 577
| "li bs as = AALTs bs as"
+ − 578
+ − 579
+ − 580
+ − 581
+ − 582
fun bsimp_ASEQ :: "bit list \<Rightarrow> arexp \<Rightarrow> arexp \<Rightarrow> arexp"
+ − 583
where
+ − 584
"bsimp_ASEQ _ AZERO _ = AZERO"
+ − 585
| "bsimp_ASEQ _ _ AZERO = AZERO"
+ − 586
| "bsimp_ASEQ bs1 (AONE bs2) r2 = fuse (bs1 @ bs2) r2"
+ − 587
| "bsimp_ASEQ bs1 r1 r2 = ASEQ bs1 r1 r2"
+ − 588
+ − 589
+ − 590
fun bsimp_AALTs :: "bit list \<Rightarrow> arexp list \<Rightarrow> arexp"
+ − 591
where
+ − 592
"bsimp_AALTs _ [] = AZERO"
+ − 593
| "bsimp_AALTs bs1 [r] = fuse bs1 r"
+ − 594
| "bsimp_AALTs bs1 rs = AALTs bs1 rs"
+ − 595
+ − 596
+ − 597
fun bsimp :: "arexp \<Rightarrow> arexp"
+ − 598
where
+ − 599
"bsimp (ASEQ bs1 r1 r2) = bsimp_ASEQ bs1 (bsimp r1) (bsimp r2)"
+ − 600
| "bsimp (AALTs bs1 rs) = bsimp_AALTs bs1 (flts (map bsimp rs))"
+ − 601
| "bsimp r = r"
+ − 602
+ − 603
+ − 604
+ − 605
+ − 606
fun
+ − 607
bders_simp :: "arexp \<Rightarrow> string \<Rightarrow> arexp"
+ − 608
where
+ − 609
"bders_simp r [] = r"
+ − 610
| "bders_simp r (c # s) = bders_simp (bsimp (bder c r)) s"
+ − 611
+ − 612
definition blexer_simp where
+ − 613
"blexer_simp r s \<equiv> if bnullable (bders_simp (intern r) s) then
+ − 614
decode (bmkeps (bders_simp (intern r) s)) r else None"
+ − 615
+ − 616
+ − 617
lemma asize0:
+ − 618
shows "0 < asize r"
+ − 619
apply(induct r)
+ − 620
apply(auto)
+ − 621
done
+ − 622
+ − 623
+ − 624
lemma bders_simp_append:
+ − 625
shows "bders_simp r (s1 @ s2) = bders_simp (bders_simp r s1) s2"
+ − 626
apply(induct s1 arbitrary: r s2)
+ − 627
apply(simp)
+ − 628
apply(simp)
+ − 629
done
+ − 630
+ − 631
lemma bsimp_ASEQ_size:
+ − 632
shows "asize (bsimp_ASEQ bs r1 r2) \<le> Suc (asize r1 + asize r2)"
+ − 633
apply(induct bs r1 r2 rule: bsimp_ASEQ.induct)
+ − 634
apply(auto)
+ − 635
done
+ − 636
+ − 637
lemma fuse_size:
+ − 638
shows "asize (fuse bs r) = asize r"
+ − 639
apply(induct r)
+ − 640
apply(auto)
+ − 641
done
+ − 642
+ − 643
lemma flts_size:
+ − 644
shows "sum_list (map asize (flts rs)) \<le> sum_list (map asize rs)"
+ − 645
apply(induct rs rule: flts.induct)
+ − 646
apply(simp_all)
+ − 647
by (metis (mono_tags, lifting) add_mono comp_apply eq_imp_le fuse_size le_SucI map_eq_conv)
+ − 648
+ − 649
+ − 650
lemma bsimp_AALTs_size:
+ − 651
shows "asize (bsimp_AALTs bs rs) \<le> Suc (sum_list (map asize rs))"
+ − 652
apply(induct rs rule: bsimp_AALTs.induct)
+ − 653
apply(auto simp add: fuse_size)
+ − 654
done
+ − 655
+ − 656
+ − 657
lemma bsimp_size:
+ − 658
shows "asize (bsimp r) \<le> asize r"
+ − 659
apply(induct r)
+ − 660
apply(simp_all)
+ − 661
apply (meson Suc_le_mono add_mono_thms_linordered_semiring(1) bsimp_ASEQ_size le_trans)
+ − 662
apply(rule le_trans)
+ − 663
apply(rule bsimp_AALTs_size)
+ − 664
apply(simp)
+ − 665
apply(rule le_trans)
+ − 666
apply(rule flts_size)
+ − 667
by (simp add: sum_list_mono)
+ − 668
+ − 669
lemma bsimp_asize0:
+ − 670
shows "(\<Sum>x\<leftarrow>rs. asize (bsimp x)) \<le> sum_list (map asize rs)"
+ − 671
apply(induct rs)
+ − 672
apply(auto)
+ − 673
by (simp add: add_mono bsimp_size)
+ − 674
+ − 675
lemma bsimp_AALTs_size2:
+ − 676
assumes "\<forall>r \<in> set rs. nonalt r"
+ − 677
shows "asize (bsimp_AALTs bs rs) \<ge> sum_list (map asize rs)"
+ − 678
using assms
+ − 679
apply(induct rs rule: bsimp_AALTs.induct)
+ − 680
apply(simp_all add: fuse_size)
+ − 681
done
+ − 682
+ − 683
+ − 684
lemma qq:
+ − 685
shows "map (asize \<circ> fuse bs) rs = map asize rs"
+ − 686
apply(induct rs)
+ − 687
apply(auto simp add: fuse_size)
+ − 688
done
+ − 689
+ − 690
lemma flts_size2:
+ − 691
assumes "\<exists>bs rs'. AALTs bs rs' \<in> set rs"
+ − 692
shows "sum_list (map asize (flts rs)) < sum_list (map asize rs)"
+ − 693
using assms
+ − 694
apply(induct rs)
+ − 695
apply(auto simp add: qq)
+ − 696
apply (simp add: flts_size less_Suc_eq_le)
+ − 697
apply(case_tac a)
+ − 698
apply(auto simp add: qq)
+ − 699
prefer 2
+ − 700
apply (simp add: flts_size le_imp_less_Suc)
+ − 701
using less_Suc_eq by auto
+ − 702
+ − 703
lemma bsimp_AALTs_size3:
+ − 704
assumes "\<exists>r \<in> set (map bsimp rs). \<not>nonalt r"
+ − 705
shows "asize (bsimp (AALTs bs rs)) < asize (AALTs bs rs)"
+ − 706
using assms flts_size2
+ − 707
apply -
+ − 708
apply(clarify)
+ − 709
apply(simp)
+ − 710
apply(drule_tac x="map bsimp rs" in meta_spec)
+ − 711
apply(drule meta_mp)
+ − 712
apply (metis list.set_map nonalt.elims(3))
+ − 713
apply(simp)
+ − 714
apply(rule order_class.order.strict_trans1)
+ − 715
apply(rule bsimp_AALTs_size)
+ − 716
apply(simp)
+ − 717
by (smt Suc_leI bsimp_asize0 comp_def le_imp_less_Suc le_trans map_eq_conv not_less_eq)
+ − 718
+ − 719
+ − 720
+ − 721
+ − 722
lemma L_bsimp_ASEQ:
+ − 723
"L (SEQ (erase r1) (erase r2)) = L (erase (bsimp_ASEQ bs r1 r2))"
+ − 724
apply(induct bs r1 r2 rule: bsimp_ASEQ.induct)
+ − 725
apply(simp_all)
+ − 726
by (metis erase_fuse fuse.simps(4))
+ − 727
+ − 728
lemma L_bsimp_AALTs:
+ − 729
"L (erase (AALTs bs rs)) = L (erase (bsimp_AALTs bs rs))"
+ − 730
apply(induct bs rs rule: bsimp_AALTs.induct)
+ − 731
apply(simp_all add: erase_fuse)
+ − 732
done
+ − 733
+ − 734
lemma L_erase_AALTs:
+ − 735
shows "L (erase (AALTs bs rs)) = \<Union> (L ` erase ` (set rs))"
+ − 736
apply(induct rs)
+ − 737
apply(simp)
+ − 738
apply(simp)
+ − 739
apply(case_tac rs)
+ − 740
apply(simp)
+ − 741
apply(simp)
+ − 742
done
+ − 743
+ − 744
lemma L_erase_flts:
+ − 745
shows "\<Union> (L ` erase ` (set (flts rs))) = \<Union> (L ` erase ` (set rs))"
+ − 746
apply(induct rs rule: flts.induct)
+ − 747
apply(simp_all)
+ − 748
apply(auto)
+ − 749
using L_erase_AALTs erase_fuse apply auto[1]
+ − 750
by (simp add: L_erase_AALTs erase_fuse)
+ − 751
+ − 752
+ − 753
lemma L_bsimp_erase:
+ − 754
shows "L (erase r) = L (erase (bsimp r))"
+ − 755
apply(induct r)
+ − 756
apply(simp)
+ − 757
apply(simp)
+ − 758
apply(simp)
+ − 759
apply(auto simp add: Sequ_def)[1]
+ − 760
apply(subst L_bsimp_ASEQ[symmetric])
+ − 761
apply(auto simp add: Sequ_def)[1]
+ − 762
apply(subst (asm) L_bsimp_ASEQ[symmetric])
+ − 763
apply(auto simp add: Sequ_def)[1]
+ − 764
apply(simp)
+ − 765
apply(subst L_bsimp_AALTs[symmetric])
+ − 766
defer
+ − 767
apply(simp)
+ − 768
apply(subst (2)L_erase_AALTs)
+ − 769
apply(subst L_erase_flts)
+ − 770
apply(auto)
+ − 771
apply (simp add: L_erase_AALTs)
+ − 772
using L_erase_AALTs by blast
+ − 773
+ − 774
lemma bsimp_ASEQ0:
+ − 775
shows "bsimp_ASEQ bs r1 AZERO = AZERO"
+ − 776
apply(induct r1)
+ − 777
apply(auto)
+ − 778
done
+ − 779
+ − 780
+ − 781
+ − 782
lemma bsimp_ASEQ1:
+ − 783
assumes "r1 \<noteq> AZERO" "r2 \<noteq> AZERO" "\<forall>bs. r1 \<noteq> AONE bs"
+ − 784
shows "bsimp_ASEQ bs r1 r2 = ASEQ bs r1 r2"
+ − 785
using assms
+ − 786
apply(induct bs r1 r2 rule: bsimp_ASEQ.induct)
+ − 787
apply(auto)
+ − 788
done
+ − 789
+ − 790
lemma bsimp_ASEQ2:
+ − 791
shows "bsimp_ASEQ bs (AONE bs1) r2 = fuse (bs @ bs1) r2"
+ − 792
apply(induct r2)
+ − 793
apply(auto)
+ − 794
done
+ − 795
+ − 796
+ − 797
lemma L_bders_simp:
+ − 798
shows "L (erase (bders_simp r s)) = L (erase (bders r s))"
+ − 799
apply(induct s arbitrary: r rule: rev_induct)
+ − 800
apply(simp)
+ − 801
apply(simp)
+ − 802
apply(simp add: ders_append)
+ − 803
apply(simp add: bders_simp_append)
+ − 804
apply(simp add: L_bsimp_erase[symmetric])
+ − 805
by (simp add: der_correctness)
+ − 806
+ − 807
lemma b1:
+ − 808
"bsimp_ASEQ bs1 (AONE bs) r = fuse (bs1 @ bs) r"
+ − 809
apply(induct r)
+ − 810
apply(auto)
+ − 811
done
+ − 812
+ − 813
lemma b2:
+ − 814
assumes "bnullable r"
+ − 815
shows "bmkeps (fuse bs r) = bs @ bmkeps r"
+ − 816
by (simp add: assms bmkeps_retrieve bnullable_correctness erase_fuse mkeps_nullable retrieve_fuse2)
+ − 817
+ − 818
lemma b3:
+ − 819
shows "bnullable r = bnullable (bsimp r)"
+ − 820
using L_bsimp_erase bnullable_correctness nullable_correctness by auto
+ − 821
+ − 822
+ − 823
lemma b4:
+ − 824
shows "bnullable (bders_simp r s) = bnullable (bders r s)"
+ − 825
by (metis L_bders_simp bnullable_correctness lexer.simps(1) lexer_correct_None option.distinct(1))
+ − 826
+ − 827
lemma q1:
+ − 828
assumes "\<forall>r \<in> set rs. bmkeps(bsimp r) = bmkeps r"
+ − 829
shows "map (\<lambda>r. bmkeps(bsimp r)) rs = map bmkeps rs"
+ − 830
using assms
+ − 831
apply(induct rs)
+ − 832
apply(simp)
+ − 833
apply(simp)
+ − 834
done
+ − 835
+ − 836
lemma q3:
+ − 837
assumes "\<exists>r \<in> set rs. bnullable r"
+ − 838
shows "bmkeps (AALTs bs rs) = bmkeps (bsimp_AALTs bs rs)"
+ − 839
using assms
+ − 840
apply(induct bs rs rule: bsimp_AALTs.induct)
+ − 841
apply(simp)
+ − 842
apply(simp)
+ − 843
apply (simp add: b2)
+ − 844
apply(simp)
+ − 845
done
+ − 846
+ − 847
lemma qq1:
+ − 848
assumes "\<exists>r \<in> set rs. bnullable r"
+ − 849
shows "bmkeps (AALTs bs (rs @ rs1)) = bmkeps (AALTs bs rs)"
+ − 850
using assms
+ − 851
apply(induct rs arbitrary: rs1 bs)
+ − 852
apply(simp)
+ − 853
apply(simp)
+ − 854
by (metis Nil_is_append_conv bmkeps.simps(4) neq_Nil_conv r0 split_list_last)
+ − 855
+ − 856
lemma qq2:
+ − 857
assumes "\<forall>r \<in> set rs. \<not> bnullable r" "\<exists>r \<in> set rs1. bnullable r"
+ − 858
shows "bmkeps (AALTs bs (rs @ rs1)) = bmkeps (AALTs bs rs1)"
+ − 859
using assms
+ − 860
apply(induct rs arbitrary: rs1 bs)
+ − 861
apply(simp)
+ − 862
apply(simp)
+ − 863
by (metis append_assoc in_set_conv_decomp r1 r2)
+ − 864
+ − 865
lemma qq3:
+ − 866
shows "bnullable (AALTs bs rs) = (\<exists>r \<in> set rs. bnullable r)"
+ − 867
apply(induct rs arbitrary: bs)
+ − 868
apply(simp)
+ − 869
apply(simp)
+ − 870
done
+ − 871
+ − 872
lemma fuse_empty:
+ − 873
shows "fuse [] r = r"
+ − 874
apply(induct r)
+ − 875
apply(auto)
+ − 876
done
+ − 877
+ − 878
lemma flts_fuse:
+ − 879
shows "map (fuse bs) (flts rs) = flts (map (fuse bs) rs)"
+ − 880
apply(induct rs arbitrary: bs rule: flts.induct)
+ − 881
apply(auto simp add: fuse_append)
+ − 882
done
+ − 883
+ − 884
lemma bsimp_ASEQ_fuse:
+ − 885
shows "fuse bs1 (bsimp_ASEQ bs2 r1 r2) = bsimp_ASEQ (bs1 @ bs2) r1 r2"
+ − 886
apply(induct r1 r2 arbitrary: bs1 bs2 rule: bsimp_ASEQ.induct)
+ − 887
apply(auto)
+ − 888
done
+ − 889
+ − 890
lemma bsimp_AALTs_fuse:
+ − 891
assumes "\<forall>r \<in> set rs. fuse bs1 (fuse bs2 r) = fuse (bs1 @ bs2) r"
+ − 892
shows "fuse bs1 (bsimp_AALTs bs2 rs) = bsimp_AALTs (bs1 @ bs2) rs"
+ − 893
using assms
+ − 894
apply(induct bs2 rs arbitrary: bs1 rule: bsimp_AALTs.induct)
+ − 895
apply(auto)
+ − 896
done
+ − 897
+ − 898
+ − 899
+ − 900
lemma bsimp_fuse:
+ − 901
shows "fuse bs (bsimp r) = bsimp (fuse bs r)"
+ − 902
apply(induct r arbitrary: bs)
+ − 903
apply(simp)
+ − 904
apply(simp)
+ − 905
apply(simp)
+ − 906
prefer 3
+ − 907
apply(simp)
+ − 908
apply(simp)
+ − 909
apply (simp add: bsimp_ASEQ_fuse)
+ − 910
apply(simp)
+ − 911
by (simp add: bsimp_AALTs_fuse fuse_append)
+ − 912
+ − 913
lemma bsimp_fuse_AALTs:
+ − 914
shows "fuse bs (bsimp (AALTs [] rs)) = bsimp (AALTs bs rs)"
+ − 915
apply(subst bsimp_fuse)
+ − 916
apply(simp)
+ − 917
done
+ − 918
+ − 919
lemma bsimp_fuse_AALTs2:
+ − 920
shows "fuse bs (bsimp_AALTs [] rs) = bsimp_AALTs bs rs"
+ − 921
using bsimp_AALTs_fuse fuse_append by auto
+ − 922
+ − 923
+ − 924
lemma bsimp_ASEQ_idem:
+ − 925
assumes "bsimp (bsimp r1) = bsimp r1" "bsimp (bsimp r2) = bsimp r2"
+ − 926
shows "bsimp (bsimp_ASEQ x1 (bsimp r1) (bsimp r2)) = bsimp_ASEQ x1 (bsimp r1) (bsimp r2)"
+ − 927
using assms
+ − 928
apply(case_tac "bsimp r1 = AZERO")
+ − 929
apply(simp)
+ − 930
apply(case_tac "bsimp r2 = AZERO")
+ − 931
apply(simp)
+ − 932
apply (metis bnullable.elims(2) bnullable.elims(3) bsimp.simps(3) bsimp_ASEQ.simps(2) bsimp_ASEQ.simps(3) bsimp_ASEQ.simps(4) bsimp_ASEQ.simps(5) bsimp_ASEQ.simps(6))
+ − 933
apply(case_tac "\<exists>bs. bsimp r1 = AONE bs")
+ − 934
apply(auto)[1]
+ − 935
apply(subst bsimp_ASEQ2)
+ − 936
apply(subst bsimp_ASEQ2)
+ − 937
apply (metis assms(2) bsimp_fuse)
+ − 938
apply(subst bsimp_ASEQ1)
+ − 939
apply(auto)
+ − 940
done
+ − 941
+ − 942
+ − 943
fun nonnested :: "arexp \<Rightarrow> bool"
+ − 944
where
+ − 945
"nonnested (AALTs bs2 []) = True"
+ − 946
| "nonnested (AALTs bs2 ((AALTs bs1 rs1) # rs2)) = False"
+ − 947
| "nonnested (AALTs bs2 (r # rs2)) = nonnested (AALTs bs2 rs2)"
+ − 948
| "nonnested r = True"
+ − 949
+ − 950
+ − 951
lemma k0:
+ − 952
shows "flts (r # rs1) = flts [r] @ flts rs1"
+ − 953
apply(induct r arbitrary: rs1)
+ − 954
apply(auto)
+ − 955
done
+ − 956
+ − 957
lemma k00:
+ − 958
shows "flts (rs1 @ rs2) = flts rs1 @ flts rs2"
+ − 959
apply(induct rs1 arbitrary: rs2)
+ − 960
apply(auto)
+ − 961
by (metis append.assoc k0)
+ − 962
+ − 963
lemma k0a:
+ − 964
shows "flts [AALTs bs rs] = map (fuse bs) rs"
+ − 965
apply(simp)
+ − 966
done
+ − 967
+ − 968
+ − 969
lemma k0b:
+ − 970
assumes "nonalt r" "r \<noteq> AZERO"
+ − 971
shows "flts [r] = [r]"
+ − 972
using assms
+ − 973
apply(case_tac r)
+ − 974
apply(simp_all)
+ − 975
done
+ − 976
+ − 977
lemma nn1:
+ − 978
assumes "nonnested (AALTs bs rs)"
+ − 979
shows "\<nexists>bs1 rs1. flts rs = [AALTs bs1 rs1]"
+ − 980
using assms
+ − 981
apply(induct rs rule: flts.induct)
+ − 982
apply(auto)
+ − 983
done
+ − 984
+ − 985
lemma nn1q:
+ − 986
assumes "nonnested (AALTs bs rs)"
+ − 987
shows "\<nexists>bs1 rs1. AALTs bs1 rs1 \<in> set (flts rs)"
+ − 988
using assms
+ − 989
apply(induct rs rule: flts.induct)
+ − 990
apply(auto)
+ − 991
done
+ − 992
+ − 993
lemma nn1qq:
+ − 994
assumes "nonnested (AALTs bs rs)"
+ − 995
shows "\<nexists>bs1 rs1. AALTs bs1 rs1 \<in> set rs"
+ − 996
using assms
+ − 997
apply(induct rs rule: flts.induct)
+ − 998
apply(auto)
+ − 999
done
+ − 1000
+ − 1001
lemma nn10:
+ − 1002
assumes "nonnested (AALTs cs rs)"
+ − 1003
shows "nonnested (AALTs (bs @ cs) rs)"
+ − 1004
using assms
+ − 1005
apply(induct rs arbitrary: cs bs)
+ − 1006
apply(simp_all)
+ − 1007
apply(case_tac a)
+ − 1008
apply(simp_all)
+ − 1009
done
+ − 1010
+ − 1011
lemma nn11a:
+ − 1012
assumes "nonalt r"
+ − 1013
shows "nonalt (fuse bs r)"
+ − 1014
using assms
+ − 1015
apply(induct r)
+ − 1016
apply(auto)
+ − 1017
done
+ − 1018
+ − 1019
+ − 1020
lemma nn1a:
+ − 1021
assumes "nonnested r"
+ − 1022
shows "nonnested (fuse bs r)"
+ − 1023
using assms
+ − 1024
apply(induct bs r arbitrary: rule: fuse.induct)
+ − 1025
apply(simp_all add: nn10)
+ − 1026
done
+ − 1027
+ − 1028
lemma n0:
+ − 1029
shows "nonnested (AALTs bs rs) \<longleftrightarrow> (\<forall>r \<in> set rs. nonalt r)"
+ − 1030
apply(induct rs arbitrary: bs)
+ − 1031
apply(auto)
+ − 1032
apply (metis list.set_intros(1) nn1qq nonalt.elims(3))
+ − 1033
apply (metis list.set_intros(2) nn1qq nonalt.elims(3))
+ − 1034
by (metis nonalt.elims(2) nonnested.simps(3) nonnested.simps(4) nonnested.simps(5) nonnested.simps(6) nonnested.simps(7))
+ − 1035
+ − 1036
+ − 1037
+ − 1038
+ − 1039
lemma nn1c:
+ − 1040
assumes "\<forall>r \<in> set rs. nonnested r"
+ − 1041
shows "\<forall>r \<in> set (flts rs). nonalt r"
+ − 1042
using assms
+ − 1043
apply(induct rs rule: flts.induct)
+ − 1044
apply(auto)
+ − 1045
apply(rule nn11a)
+ − 1046
by (metis nn1qq nonalt.elims(3))
+ − 1047
+ − 1048
lemma nn1bb:
+ − 1049
assumes "\<forall>r \<in> set rs. nonalt r"
+ − 1050
shows "nonnested (bsimp_AALTs bs rs)"
+ − 1051
using assms
+ − 1052
apply(induct bs rs rule: bsimp_AALTs.induct)
+ − 1053
apply(auto)
+ − 1054
apply (metis nn11a nonalt.simps(1) nonnested.elims(3))
+ − 1055
using n0 by auto
+ − 1056
+ − 1057
lemma nn1b:
+ − 1058
shows "nonnested (bsimp r)"
+ − 1059
apply(induct r)
+ − 1060
apply(simp_all)
+ − 1061
apply(case_tac "bsimp r1 = AZERO")
+ − 1062
apply(simp)
+ − 1063
apply(case_tac "bsimp r2 = AZERO")
+ − 1064
apply(simp)
+ − 1065
apply(subst bsimp_ASEQ0)
+ − 1066
apply(simp)
+ − 1067
apply(case_tac "\<exists>bs. bsimp r1 = AONE bs")
+ − 1068
apply(auto)[1]
+ − 1069
apply(subst bsimp_ASEQ2)
+ − 1070
apply (simp add: nn1a)
+ − 1071
apply(subst bsimp_ASEQ1)
+ − 1072
apply(auto)
+ − 1073
apply(rule nn1bb)
+ − 1074
apply(auto)
+ − 1075
by (metis (mono_tags, hide_lams) imageE nn1c set_map)
+ − 1076
+ − 1077
lemma nn1d:
+ − 1078
assumes "bsimp r = AALTs bs rs"
+ − 1079
shows "\<forall>r1 \<in> set rs. \<forall> bs. r1 \<noteq> AALTs bs rs2"
+ − 1080
using nn1b assms
+ − 1081
by (metis nn1qq)
+ − 1082
+ − 1083
lemma nn_flts:
+ − 1084
assumes "nonnested (AALTs bs rs)"
+ − 1085
shows "\<forall>r \<in> set (flts rs). nonalt r"
+ − 1086
using assms
+ − 1087
apply(induct rs arbitrary: bs rule: flts.induct)
+ − 1088
apply(auto)
+ − 1089
done
+ − 1090
+ − 1091
+ − 1092
+ − 1093
lemma rt:
+ − 1094
shows "sum_list (map asize (flts (map bsimp rs))) \<le> sum_list (map asize rs)"
+ − 1095
apply(induct rs)
+ − 1096
apply(simp)
+ − 1097
apply(simp)
+ − 1098
apply(subst k0)
+ − 1099
apply(simp)
+ − 1100
by (smt add_le_cancel_right add_mono bsimp_size flts.simps(1) flts_size k0 le_iff_add list.simps(9) map_append sum_list.Cons sum_list.append trans_le_add1)
+ − 1101
+ − 1102
lemma bsimp_AALTs_qq:
+ − 1103
assumes "1 < length rs"
+ − 1104
shows "bsimp_AALTs bs rs = AALTs bs rs"
+ − 1105
using assms
+ − 1106
apply(case_tac rs)
+ − 1107
apply(simp)
+ − 1108
apply(case_tac list)
+ − 1109
apply(simp_all)
+ − 1110
done
+ − 1111
+ − 1112
+ − 1113
lemma bsimp_AALTs1:
+ − 1114
assumes "nonalt r"
+ − 1115
shows "bsimp_AALTs bs (flts [r]) = fuse bs r"
+ − 1116
using assms
+ − 1117
apply(case_tac r)
+ − 1118
apply(simp_all)
+ − 1119
done
+ − 1120
+ − 1121
lemma bbbbs:
+ − 1122
assumes "good r" "r = AALTs bs1 rs"
+ − 1123
shows "bsimp_AALTs bs (flts [r]) = AALTs bs (map (fuse bs1) rs)"
+ − 1124
using assms
+ − 1125
by (metis (no_types, lifting) Nil_is_map_conv append.left_neutral append_butlast_last_id bsimp_AALTs.elims butlast.simps(2) good.simps(4) good.simps(5) k0a map_butlast)
+ − 1126
+ − 1127
lemma bbbbs1:
+ − 1128
shows "nonalt r \<or> (\<exists>bs rs. r = AALTs bs rs)"
+ − 1129
using nonalt.elims(3) by auto
+ − 1130
+ − 1131
+ − 1132
lemma good_fuse:
+ − 1133
shows "good (fuse bs r) = good r"
+ − 1134
apply(induct r arbitrary: bs)
+ − 1135
apply(auto)
+ − 1136
apply(case_tac r1)
+ − 1137
apply(simp_all)
+ − 1138
apply(case_tac r2)
+ − 1139
apply(simp_all)
+ − 1140
apply(case_tac r2)
+ − 1141
apply(simp_all)
+ − 1142
apply(case_tac r2)
+ − 1143
apply(simp_all)
+ − 1144
apply(case_tac r2)
+ − 1145
apply(simp_all)
+ − 1146
apply(case_tac r1)
+ − 1147
apply(simp_all)
+ − 1148
apply(case_tac r2)
+ − 1149
apply(simp_all)
+ − 1150
apply(case_tac r2)
+ − 1151
apply(simp_all)
+ − 1152
apply(case_tac r2)
+ − 1153
apply(simp_all)
+ − 1154
apply(case_tac r2)
+ − 1155
apply(simp_all)
+ − 1156
apply(case_tac x2a)
+ − 1157
apply(simp_all)
+ − 1158
apply(case_tac list)
+ − 1159
apply(simp_all)
+ − 1160
apply(case_tac x2a)
+ − 1161
apply(simp_all)
+ − 1162
apply(case_tac list)
+ − 1163
apply(simp_all)
+ − 1164
done
+ − 1165
+ − 1166
lemma good0:
+ − 1167
assumes "rs \<noteq> Nil" "\<forall>r \<in> set rs. nonalt r"
+ − 1168
shows "good (bsimp_AALTs bs rs) \<longleftrightarrow> (\<forall>r \<in> set rs. good r)"
+ − 1169
using assms
+ − 1170
apply(induct bs rs rule: bsimp_AALTs.induct)
+ − 1171
apply(auto simp add: good_fuse)
+ − 1172
done
+ − 1173
+ − 1174
lemma good0a:
+ − 1175
assumes "flts (map bsimp rs) \<noteq> Nil" "\<forall>r \<in> set (flts (map bsimp rs)). nonalt r"
+ − 1176
shows "good (bsimp (AALTs bs rs)) \<longleftrightarrow> (\<forall>r \<in> set (flts (map bsimp rs)). good r)"
+ − 1177
using assms
+ − 1178
apply(simp)
+ − 1179
apply(auto)
+ − 1180
apply(subst (asm) good0)
+ − 1181
apply(simp)
+ − 1182
apply(auto)
+ − 1183
apply(subst good0)
+ − 1184
apply(simp)
+ − 1185
apply(auto)
+ − 1186
done
+ − 1187
+ − 1188
lemma flts0:
+ − 1189
assumes "r \<noteq> AZERO" "nonalt r"
+ − 1190
shows "flts [r] \<noteq> []"
+ − 1191
using assms
+ − 1192
apply(induct r)
+ − 1193
apply(simp_all)
+ − 1194
done
+ − 1195
+ − 1196
lemma flts1:
+ − 1197
assumes "good r"
+ − 1198
shows "flts [r] \<noteq> []"
+ − 1199
using assms
+ − 1200
apply(induct r)
+ − 1201
apply(simp_all)
+ − 1202
apply(case_tac x2a)
+ − 1203
apply(simp)
+ − 1204
apply(simp)
+ − 1205
done
+ − 1206
+ − 1207
lemma flts2:
+ − 1208
assumes "good r"
+ − 1209
shows "\<forall>r' \<in> set (flts [r]). good r' \<and> nonalt r'"
+ − 1210
using assms
+ − 1211
apply(induct r)
+ − 1212
apply(simp)
+ − 1213
apply(simp)
+ − 1214
apply(simp)
+ − 1215
prefer 2
+ − 1216
apply(simp)
+ − 1217
apply(auto)[1]
+ − 1218
apply (metis bsimp_AALTs.elims good.simps(4) good.simps(5) good.simps(6) good_fuse)
+ − 1219
apply (metis bsimp_AALTs.elims good.simps(4) good.simps(5) good.simps(6) nn11a)
+ − 1220
apply fastforce
+ − 1221
apply(simp)
+ − 1222
done
+ − 1223
+ − 1224
+ − 1225
lemma flts3:
+ − 1226
assumes "\<forall>r \<in> set rs. good r \<or> r = AZERO"
+ − 1227
shows "\<forall>r \<in> set (flts rs). good r"
+ − 1228
using assms
+ − 1229
apply(induct rs arbitrary: rule: flts.induct)
+ − 1230
apply(simp_all)
+ − 1231
by (metis UnE flts2 k0a set_map)
+ − 1232
+ − 1233
lemma flts3b:
+ − 1234
assumes "\<exists>r\<in>set rs. good r"
+ − 1235
shows "flts rs \<noteq> []"
+ − 1236
using assms
+ − 1237
apply(induct rs arbitrary: rule: flts.induct)
+ − 1238
apply(simp)
+ − 1239
apply(simp)
+ − 1240
apply(simp)
+ − 1241
apply(auto)
+ − 1242
done
+ − 1243
+ − 1244
lemma flts4:
+ − 1245
assumes "bsimp_AALTs bs (flts rs) = AZERO"
+ − 1246
shows "\<forall>r \<in> set rs. \<not> good r"
+ − 1247
using assms
+ − 1248
apply(induct rs arbitrary: bs rule: flts.induct)
+ − 1249
apply(auto)
+ − 1250
defer
+ − 1251
apply (metis (no_types, lifting) Nil_is_append_conv append_self_conv2 bsimp_AALTs.elims butlast.simps(2) butlast_append flts3b nonalt.simps(1) nonalt.simps(2))
+ − 1252
apply (metis arexp.distinct(7) bsimp_AALTs.elims flts2 good.simps(1) good.simps(2) good0 k0b list.distinct(1) list.inject nonalt.simps(3))
+ − 1253
apply (metis arexp.distinct(3) arexp.distinct(7) bsimp_AALTs.elims fuse.simps(3) list.distinct(1) list.inject)
+ − 1254
apply (metis arexp.distinct(7) bsimp_AALTs.elims good.simps(1) good_fuse list.distinct(1) list.inject)
+ − 1255
apply (metis arexp.distinct(7) bsimp_AALTs.elims list.distinct(1) list.inject)
+ − 1256
apply (metis arexp.distinct(7) bsimp_AALTs.elims flts2 good.simps(1) good.simps(33) good0 k0b list.distinct(1) list.inject nonalt.simps(6))
+ − 1257
by (metis (no_types, lifting) Nil_is_append_conv append_Nil2 arexp.distinct(7) bsimp_AALTs.elims butlast.simps(2) butlast_append flts1 flts2 good.simps(1) good0 k0a)
+ − 1258
+ − 1259
+ − 1260
lemma flts_nil:
+ − 1261
assumes "\<forall>y. asize y < Suc (sum_list (map asize rs)) \<longrightarrow>
+ − 1262
good (bsimp y) \<or> bsimp y = AZERO"
+ − 1263
and "\<forall>r\<in>set rs. \<not> good (bsimp r)"
+ − 1264
shows "flts (map bsimp rs) = []"
+ − 1265
using assms
+ − 1266
apply(induct rs)
+ − 1267
apply(simp)
+ − 1268
apply(simp)
+ − 1269
apply(subst k0)
+ − 1270
apply(simp)
+ − 1271
by force
+ − 1272
+ − 1273
lemma flts_nil2:
+ − 1274
assumes "\<forall>y. asize y < Suc (sum_list (map asize rs)) \<longrightarrow>
+ − 1275
good (bsimp y) \<or> bsimp y = AZERO"
+ − 1276
and "bsimp_AALTs bs (flts (map bsimp rs)) = AZERO"
+ − 1277
shows "flts (map bsimp rs) = []"
+ − 1278
using assms
+ − 1279
apply(induct rs arbitrary: bs)
+ − 1280
apply(simp)
+ − 1281
apply(simp)
+ − 1282
apply(subst k0)
+ − 1283
apply(simp)
+ − 1284
apply(subst (asm) k0)
+ − 1285
apply(auto)
+ − 1286
apply (metis flts.simps(1) flts.simps(2) flts4 k0 less_add_Suc1 list.set_intros(1))
+ − 1287
by (metis flts.simps(2) flts4 k0 less_add_Suc1 list.set_intros(1))
+ − 1288
+ − 1289
+ − 1290
+ − 1291
lemma good_SEQ:
+ − 1292
assumes "r1 \<noteq> AZERO" "r2 \<noteq> AZERO" "\<forall>bs. r1 \<noteq> AONE bs"
+ − 1293
shows "good (ASEQ bs r1 r2) = (good r1 \<and> good r2)"
+ − 1294
using assms
+ − 1295
apply(case_tac r1)
+ − 1296
apply(simp_all)
+ − 1297
apply(case_tac r2)
+ − 1298
apply(simp_all)
+ − 1299
apply(case_tac r2)
+ − 1300
apply(simp_all)
+ − 1301
apply(case_tac r2)
+ − 1302
apply(simp_all)
+ − 1303
apply(case_tac r2)
+ − 1304
apply(simp_all)
+ − 1305
done
+ − 1306
+ − 1307
lemma good1:
+ − 1308
shows "good (bsimp a) \<or> bsimp a = AZERO"
+ − 1309
apply(induct a taking: asize rule: measure_induct)
+ − 1310
apply(case_tac x)
+ − 1311
apply(simp)
+ − 1312
apply(simp)
+ − 1313
apply(simp)
+ − 1314
prefer 3
+ − 1315
apply(simp)
+ − 1316
prefer 2
+ − 1317
(* AALTs case *)
+ − 1318
apply(simp only:)
+ − 1319
apply(case_tac "x52")
+ − 1320
apply(simp)
+ − 1321
thm good0a
+ − 1322
(* AALTs list at least one - case *)
+ − 1323
apply(simp only: )
+ − 1324
apply(frule_tac x="a" in spec)
+ − 1325
apply(drule mp)
+ − 1326
apply(simp)
+ − 1327
(* either first element is good, or AZERO *)
+ − 1328
apply(erule disjE)
+ − 1329
prefer 2
+ − 1330
apply(simp)
+ − 1331
(* in the AZERO case, the size is smaller *)
+ − 1332
apply(drule_tac x="AALTs x51 list" in spec)
+ − 1333
apply(drule mp)
+ − 1334
apply(simp add: asize0)
+ − 1335
apply(subst (asm) bsimp.simps)
+ − 1336
apply(subst (asm) bsimp.simps)
+ − 1337
apply(assumption)
+ − 1338
(* in the good case *)
+ − 1339
apply(frule_tac x="AALTs x51 list" in spec)
+ − 1340
apply(drule mp)
+ − 1341
apply(simp add: asize0)
+ − 1342
apply(erule disjE)
+ − 1343
apply(rule disjI1)
+ − 1344
apply(simp add: good0)
+ − 1345
apply(subst good0)
+ − 1346
apply (metis Nil_is_append_conv flts1 k0)
+ − 1347
apply (metis ex_map_conv list.simps(9) nn1b nn1c)
+ − 1348
apply(simp)
+ − 1349
apply(subst k0)
+ − 1350
apply(simp)
+ − 1351
apply(auto)[1]
+ − 1352
using flts2 apply blast
+ − 1353
apply(subst (asm) good0)
+ − 1354
prefer 3
+ − 1355
apply(auto)[1]
+ − 1356
apply auto[1]
+ − 1357
apply (metis ex_map_conv nn1b nn1c)
+ − 1358
(* in the AZERO case *)
+ − 1359
apply(simp)
+ − 1360
apply(frule_tac x="a" in spec)
+ − 1361
apply(drule mp)
+ − 1362
apply(simp)
+ − 1363
apply(erule disjE)
+ − 1364
apply(rule disjI1)
+ − 1365
apply(subst good0)
+ − 1366
apply(subst k0)
+ − 1367
using flts1 apply blast
+ − 1368
apply(auto)[1]
+ − 1369
apply (metis (no_types, hide_lams) ex_map_conv list.simps(9) nn1b nn1c)
+ − 1370
apply(auto)[1]
+ − 1371
apply(subst (asm) k0)
+ − 1372
apply(auto)[1]
+ − 1373
using flts2 apply blast
+ − 1374
apply(frule_tac x="AALTs x51 list" in spec)
+ − 1375
apply(drule mp)
+ − 1376
apply(simp add: asize0)
+ − 1377
apply(erule disjE)
+ − 1378
apply(simp)
+ − 1379
apply(simp)
+ − 1380
apply (metis add.left_commute flts_nil2 less_add_Suc1 less_imp_Suc_add list.distinct(1) list.set_cases nat.inject)
+ − 1381
apply(subst (2) k0)
+ − 1382
apply(simp)
+ − 1383
(* SEQ case *)
+ − 1384
apply(simp)
+ − 1385
apply(case_tac "bsimp x42 = AZERO")
+ − 1386
apply(simp)
+ − 1387
apply(case_tac "bsimp x43 = AZERO")
+ − 1388
apply(simp)
+ − 1389
apply(subst (2) bsimp_ASEQ0)
+ − 1390
apply(simp)
+ − 1391
apply(case_tac "\<exists>bs. bsimp x42 = AONE bs")
+ − 1392
apply(auto)[1]
+ − 1393
apply(subst bsimp_ASEQ2)
+ − 1394
using good_fuse apply force
+ − 1395
apply(subst bsimp_ASEQ1)
+ − 1396
apply(auto)
+ − 1397
apply(subst good_SEQ)
+ − 1398
apply(simp)
+ − 1399
apply(simp)
+ − 1400
apply(simp)
+ − 1401
using less_add_Suc1 less_add_Suc2 by blast
+ − 1402
+ − 1403
lemma good1a:
+ − 1404
assumes "L(erase a) \<noteq> {}"
+ − 1405
shows "good (bsimp a)"
+ − 1406
using good1 assms
+ − 1407
using L_bsimp_erase by force
+ − 1408
+ − 1409
+ − 1410
+ − 1411
lemma flts_append:
+ − 1412
"flts (xs1 @ xs2) = flts xs1 @ flts xs2"
+ − 1413
apply(induct xs1 arbitrary: xs2 rule: rev_induct)
+ − 1414
apply(auto)
+ − 1415
apply(case_tac xs)
+ − 1416
apply(auto)
+ − 1417
apply(case_tac x)
+ − 1418
apply(auto)
+ − 1419
apply(case_tac x)
+ − 1420
apply(auto)
+ − 1421
done
+ − 1422
+ − 1423
lemma g1:
+ − 1424
assumes "good (bsimp_AALTs bs rs)"
+ − 1425
shows "bsimp_AALTs bs rs = AALTs bs rs \<or> (\<exists>r. rs = [r] \<and> bsimp_AALTs bs [r] = fuse bs r)"
+ − 1426
using assms
+ − 1427
apply(induct rs arbitrary: bs)
+ − 1428
apply(simp)
+ − 1429
apply(case_tac rs)
+ − 1430
apply(simp only:)
+ − 1431
apply(simp)
+ − 1432
apply(case_tac list)
+ − 1433
apply(simp)
+ − 1434
by simp
+ − 1435
+ − 1436
lemma flts_0:
+ − 1437
assumes "nonnested (AALTs bs rs)"
+ − 1438
shows "\<forall>r \<in> set (flts rs). r \<noteq> AZERO"
+ − 1439
using assms
+ − 1440
apply(induct rs arbitrary: bs rule: flts.induct)
+ − 1441
apply(simp)
+ − 1442
apply(simp)
+ − 1443
defer
+ − 1444
apply(simp)
+ − 1445
apply(simp)
+ − 1446
apply(simp)
+ − 1447
apply(simp)
+ − 1448
apply(rule ballI)
+ − 1449
apply(simp)
+ − 1450
done
+ − 1451
+ − 1452
lemma flts_0a:
+ − 1453
assumes "nonnested (AALTs bs rs)"
+ − 1454
shows "AZERO \<notin> set (flts rs)"
+ − 1455
using assms
+ − 1456
using flts_0 by blast
+ − 1457
+ − 1458
lemma qqq1:
+ − 1459
shows "AZERO \<notin> set (flts (map bsimp rs))"
+ − 1460
by (metis ex_map_conv flts3 good.simps(1) good1)
+ − 1461
+ − 1462
+ − 1463
fun nonazero :: "arexp \<Rightarrow> bool"
+ − 1464
where
+ − 1465
"nonazero AZERO = False"
+ − 1466
| "nonazero r = True"
+ − 1467
+ − 1468
lemma flts_concat:
+ − 1469
shows "flts rs = concat (map (\<lambda>r. flts [r]) rs)"
+ − 1470
apply(induct rs)
+ − 1471
apply(auto)
+ − 1472
apply(subst k0)
+ − 1473
apply(simp)
+ − 1474
done
+ − 1475
+ − 1476
lemma flts_single1:
+ − 1477
assumes "nonalt r" "nonazero r"
+ − 1478
shows "flts [r] = [r]"
+ − 1479
using assms
+ − 1480
apply(induct r)
+ − 1481
apply(auto)
+ − 1482
done
+ − 1483
+ − 1484
lemma flts_qq:
+ − 1485
assumes "\<forall>y. asize y < Suc (sum_list (map asize rs)) \<longrightarrow> good y \<longrightarrow> bsimp y = y"
+ − 1486
"\<forall>r'\<in>set rs. good r' \<and> nonalt r'"
+ − 1487
shows "flts (map bsimp rs) = rs"
+ − 1488
using assms
+ − 1489
apply(induct rs)
+ − 1490
apply(simp)
+ − 1491
apply(simp)
+ − 1492
apply(subst k0)
+ − 1493
apply(subgoal_tac "flts [bsimp a] = [a]")
+ − 1494
prefer 2
+ − 1495
apply(drule_tac x="a" in spec)
+ − 1496
apply(drule mp)
+ − 1497
apply(simp)
+ − 1498
apply(auto)[1]
+ − 1499
using good.simps(1) k0b apply blast
+ − 1500
apply(auto)[1]
+ − 1501
done
+ − 1502
+ − 1503
lemma test:
+ − 1504
assumes "good r"
+ − 1505
shows "bsimp r = r"
+ − 1506
using assms
+ − 1507
apply(induct r taking: "asize" rule: measure_induct)
+ − 1508
apply(erule good.elims)
+ − 1509
apply(simp_all)
+ − 1510
apply(subst k0)
+ − 1511
apply(subst (2) k0)
+ − 1512
apply(subst flts_qq)
+ − 1513
apply(auto)[1]
+ − 1514
apply(auto)[1]
+ − 1515
apply (metis append_Cons append_Nil bsimp_AALTs.simps(3) good.simps(1) k0b)
+ − 1516
apply force+
+ − 1517
apply (metis (no_types, lifting) add_Suc add_Suc_right asize.simps(5) bsimp.simps(1) bsimp_ASEQ.simps(19) less_add_Suc1 less_add_Suc2)
+ − 1518
apply (metis add_Suc add_Suc_right arexp.distinct(5) arexp.distinct(7) asize.simps(4) asize.simps(5) bsimp.simps(1) bsimp.simps(2) bsimp_ASEQ1 good.simps(21) good.simps(8) less_add_Suc1 less_add_Suc2)
+ − 1519
apply force+
+ − 1520
apply (metis (no_types, lifting) add_Suc add_Suc_right arexp.distinct(5) arexp.distinct(7) asize.simps(4) asize.simps(5) bsimp.simps(1) bsimp.simps(2) bsimp_ASEQ1 good.simps(25) good.simps(8) less_add_Suc1 less_add_Suc2)
+ − 1521
apply (metis add_Suc add_Suc_right arexp.distinct(7) asize.simps(4) bsimp.simps(2) bsimp_ASEQ1 good.simps(26) good.simps(8) less_add_Suc1 less_add_Suc2)
+ − 1522
apply force+
+ − 1523
done
+ − 1524
+ − 1525
lemma test2:
+ − 1526
assumes "good r"
+ − 1527
shows "bsimp r = r"
+ − 1528
using assms
+ − 1529
apply(induct r taking: "asize" rule: measure_induct)
+ − 1530
apply(case_tac x)
+ − 1531
apply(simp_all)
+ − 1532
defer
+ − 1533
(* AALT case *)
+ − 1534
apply(subgoal_tac "1 < length x52")
+ − 1535
prefer 2
+ − 1536
apply(case_tac x52)
+ − 1537
apply(simp)
+ − 1538
apply(simp)
+ − 1539
apply(case_tac list)
+ − 1540
apply(simp)
+ − 1541
apply(simp)
+ − 1542
apply(subst bsimp_AALTs_qq)
+ − 1543
prefer 2
+ − 1544
apply(subst flts_qq)
+ − 1545
apply(auto)[1]
+ − 1546
apply(auto)[1]
+ − 1547
apply(case_tac x52)
+ − 1548
apply(simp)
+ − 1549
apply(simp)
+ − 1550
apply(case_tac list)
+ − 1551
apply(simp)
+ − 1552
apply(simp)
+ − 1553
apply(auto)[1]
+ − 1554
apply (metis (no_types, lifting) bsimp_AALTs.elims good.simps(6) length_Cons length_pos_if_in_set list.size(3) nat_neq_iff)
+ − 1555
apply(simp)
+ − 1556
apply(case_tac x52)
+ − 1557
apply(simp)
+ − 1558
apply(simp)
+ − 1559
apply(case_tac list)
+ − 1560
apply(simp)
+ − 1561
apply(simp)
+ − 1562
apply(subst k0)
+ − 1563
apply(simp)
+ − 1564
apply(subst (2) k0)
+ − 1565
apply(simp)
+ − 1566
apply (simp add: Suc_lessI flts1 one_is_add)
+ − 1567
(* SEQ case *)
+ − 1568
apply(case_tac "bsimp x42 = AZERO")
+ − 1569
apply simp
+ − 1570
apply (metis asize.elims good.simps(10) good.simps(11) good.simps(12) good.simps(2) good.simps(7) good.simps(9) good_SEQ less_add_Suc1)
+ − 1571
apply(case_tac "\<exists>bs'. bsimp x42 = AONE bs'")
+ − 1572
apply(auto)[1]
+ − 1573
defer
+ − 1574
apply(case_tac "bsimp x43 = AZERO")
+ − 1575
apply(simp)
+ − 1576
apply (metis bsimp.elims bsimp.simps(3) good.simps(10) good.simps(11) good.simps(12) good.simps(8) good.simps(9) good_SEQ less_add_Suc2)
+ − 1577
apply(auto)
+ − 1578
apply (subst bsimp_ASEQ1)
+ − 1579
apply(auto)[3]
+ − 1580
apply(auto)[1]
+ − 1581
apply (metis bsimp.simps(3) good.simps(2) good_SEQ less_add_Suc1)
+ − 1582
apply (metis bsimp.simps(3) good.simps(2) good_SEQ less_add_Suc1 less_add_Suc2)
+ − 1583
apply (subst bsimp_ASEQ2)
+ − 1584
apply(drule_tac x="x42" in spec)
+ − 1585
apply(drule mp)
+ − 1586
apply(simp)
+ − 1587
apply(drule mp)
+ − 1588
apply (metis bsimp.elims bsimp.simps(3) good.simps(10) good.simps(11) good.simps(2) good_SEQ)
+ − 1589
apply(simp)
+ − 1590
done
+ − 1591
+ − 1592
+ − 1593
lemma bsimp_idem:
+ − 1594
shows "bsimp (bsimp r) = bsimp r"
+ − 1595
using test good1
+ − 1596
by force
+ − 1597
+ − 1598
+ − 1599
lemma q3a:
+ − 1600
assumes "\<exists>r \<in> set rs. bnullable r"
+ − 1601
shows "bmkeps (AALTs bs (map (fuse bs1) rs)) = bmkeps (AALTs (bs@bs1) rs)"
+ − 1602
using assms
+ − 1603
apply(induct rs arbitrary: bs bs1)
+ − 1604
apply(simp)
+ − 1605
apply(simp)
+ − 1606
apply(auto)
+ − 1607
apply (metis append_assoc b2 bnullable_correctness erase_fuse r0)
+ − 1608
apply(case_tac "bnullable a")
+ − 1609
apply (metis append.assoc b2 bnullable_correctness erase_fuse r0)
+ − 1610
apply(case_tac rs)
+ − 1611
apply(simp)
+ − 1612
apply(simp)
+ − 1613
apply(auto)[1]
+ − 1614
apply (metis bnullable_correctness erase_fuse)+
+ − 1615
done
+ − 1616
+ − 1617
lemma qq4:
+ − 1618
assumes "\<exists>x\<in>set list. bnullable x"
+ − 1619
shows "\<exists>x\<in>set (flts list). bnullable x"
+ − 1620
using assms
+ − 1621
apply(induct list rule: flts.induct)
+ − 1622
apply(auto)
+ − 1623
by (metis UnCI bnullable_correctness erase_fuse imageI)
+ − 1624
+ − 1625
+ − 1626
lemma qs3:
+ − 1627
assumes "\<exists>r \<in> set rs. bnullable r"
+ − 1628
shows "bmkeps (AALTs bs rs) = bmkeps (AALTs bs (flts rs))"
+ − 1629
using assms
+ − 1630
apply(induct rs arbitrary: bs taking: size rule: measure_induct)
+ − 1631
apply(case_tac x)
+ − 1632
apply(simp)
+ − 1633
apply(simp)
+ − 1634
apply(case_tac a)
+ − 1635
apply(simp)
+ − 1636
apply (simp add: r1)
+ − 1637
apply(simp)
+ − 1638
apply (simp add: r0)
+ − 1639
apply(simp)
+ − 1640
apply(case_tac "flts list")
+ − 1641
apply(simp)
+ − 1642
apply (metis L_erase_AALTs L_erase_flts L_flat_Prf1 L_flat_Prf2 Prf_elims(1) bnullable_correctness erase.simps(4) mkeps_nullable r2)
+ − 1643
apply(simp)
+ − 1644
apply (simp add: r1)
+ − 1645
prefer 3
+ − 1646
apply(simp)
+ − 1647
apply (simp add: r0)
+ − 1648
prefer 2
+ − 1649
apply(simp)
+ − 1650
apply(case_tac "\<exists>x\<in>set x52. bnullable x")
+ − 1651
apply(case_tac "list")
+ − 1652
apply(simp)
+ − 1653
apply (metis b2 fuse.simps(4) q3a r2)
+ − 1654
apply(erule disjE)
+ − 1655
apply(subst qq1)
+ − 1656
apply(auto)[1]
+ − 1657
apply (metis bnullable_correctness erase_fuse)
+ − 1658
apply(simp)
+ − 1659
apply (metis b2 fuse.simps(4) q3a r2)
+ − 1660
apply(simp)
+ − 1661
apply(auto)[1]
+ − 1662
apply(subst qq1)
+ − 1663
apply (metis bnullable_correctness erase_fuse image_eqI set_map)
+ − 1664
apply (metis b2 fuse.simps(4) q3a r2)
+ − 1665
apply(subst qq1)
+ − 1666
apply (metis bnullable_correctness erase_fuse image_eqI set_map)
+ − 1667
apply (metis b2 fuse.simps(4) q3a r2)
+ − 1668
apply(simp)
+ − 1669
apply(subst qq2)
+ − 1670
apply (metis bnullable_correctness erase_fuse imageE set_map)
+ − 1671
prefer 2
+ − 1672
apply(case_tac "list")
+ − 1673
apply(simp)
+ − 1674
apply(simp)
+ − 1675
apply (simp add: qq4)
+ − 1676
apply(simp)
+ − 1677
apply(auto)
+ − 1678
apply(case_tac list)
+ − 1679
apply(simp)
+ − 1680
apply(simp)
+ − 1681
apply (simp add: r0)
+ − 1682
apply(case_tac "bnullable (ASEQ x41 x42 x43)")
+ − 1683
apply(case_tac list)
+ − 1684
apply(simp)
+ − 1685
apply(simp)
+ − 1686
apply (simp add: r0)
+ − 1687
apply(simp)
+ − 1688
using qq4 r1 r2 by auto
+ − 1689
+ − 1690
+ − 1691
+ − 1692
lemma k1:
+ − 1693
assumes "\<And>x2aa. \<lbrakk>x2aa \<in> set x2a; bnullable x2aa\<rbrakk> \<Longrightarrow> bmkeps x2aa = bmkeps (bsimp x2aa)"
+ − 1694
"\<exists>x\<in>set x2a. bnullable x"
+ − 1695
shows "bmkeps (AALTs x1 (flts x2a)) = bmkeps (AALTs x1 (flts (map bsimp x2a)))"
+ − 1696
using assms
+ − 1697
apply(induct x2a)
+ − 1698
apply fastforce
+ − 1699
apply(simp)
+ − 1700
apply(subst k0)
+ − 1701
apply(subst (2) k0)
+ − 1702
apply(auto)[1]
+ − 1703
apply (metis b3 k0 list.set_intros(1) qs3 r0)
+ − 1704
by (smt b3 imageI insert_iff k0 list.set(2) qq3 qs3 r0 r1 set_map)
+ − 1705
+ − 1706
+ − 1707
+ − 1708
lemma bmkeps_simp:
+ − 1709
assumes "bnullable r"
+ − 1710
shows "bmkeps r = bmkeps (bsimp r)"
+ − 1711
using assms
+ − 1712
apply(induct r)
+ − 1713
apply(simp)
+ − 1714
apply(simp)
+ − 1715
apply(simp)
+ − 1716
apply(simp)
+ − 1717
prefer 3
+ − 1718
apply(simp)
+ − 1719
apply(case_tac "bsimp r1 = AZERO")
+ − 1720
apply(simp)
+ − 1721
apply(auto)[1]
+ − 1722
apply (metis L_bsimp_erase L_flat_Prf1 L_flat_Prf2 Prf_elims(1) bnullable_correctness erase.simps(1) mkeps_nullable)
+ − 1723
apply(case_tac "bsimp r2 = AZERO")
+ − 1724
apply(simp)
+ − 1725
apply(auto)[1]
+ − 1726
apply (metis L_bsimp_erase L_flat_Prf1 L_flat_Prf2 Prf_elims(1) bnullable_correctness erase.simps(1) mkeps_nullable)
+ − 1727
apply(case_tac "\<exists>bs. bsimp r1 = AONE bs")
+ − 1728
apply(auto)[1]
+ − 1729
apply(subst b1)
+ − 1730
apply(subst b2)
+ − 1731
apply(simp add: b3[symmetric])
+ − 1732
apply(simp)
+ − 1733
apply(subgoal_tac "bsimp_ASEQ x1 (bsimp r1) (bsimp r2) = ASEQ x1 (bsimp r1) (bsimp r2)")
+ − 1734
prefer 2
+ − 1735
apply (smt b3 bnullable.elims(2) bsimp_ASEQ.simps(17) bsimp_ASEQ.simps(19) bsimp_ASEQ.simps(20) bsimp_ASEQ.simps(21) bsimp_ASEQ.simps(22) bsimp_ASEQ.simps(24) bsimp_ASEQ.simps(25) bsimp_ASEQ.simps(26) bsimp_ASEQ.simps(27) bsimp_ASEQ.simps(29) bsimp_ASEQ.simps(30) bsimp_ASEQ.simps(31))
+ − 1736
apply(simp)
+ − 1737
apply(simp)
+ − 1738
thm q3
+ − 1739
apply(subst q3[symmetric])
+ − 1740
apply simp
+ − 1741
using b3 qq4 apply auto[1]
+ − 1742
apply(subst qs3)
+ − 1743
apply simp
+ − 1744
using k1 by blast
+ − 1745
+ − 1746
thm bmkeps_retrieve bmkeps_simp bder_retrieve
+ − 1747
+ − 1748
lemma bmkeps_bder_AALTs:
+ − 1749
assumes "\<exists>r \<in> set rs. bnullable (bder c r)"
+ − 1750
shows "bmkeps (bder c (bsimp_AALTs bs rs)) = bmkeps (bsimp_AALTs bs (map (bder c) rs))"
+ − 1751
using assms
+ − 1752
apply(induct rs)
+ − 1753
apply(simp)
+ − 1754
apply(simp)
+ − 1755
apply(auto)
+ − 1756
apply(case_tac rs)
+ − 1757
apply(simp)
+ − 1758
apply (metis (full_types) Prf_injval bder_retrieve bmkeps_retrieve bnullable_correctness erase_bder erase_fuse mkeps_nullable retrieve_fuse2)
+ − 1759
apply(simp)
+ − 1760
apply(case_tac rs)
+ − 1761
apply(simp_all)
+ − 1762
done
+ − 1763
+ − 1764
lemma bbs0:
+ − 1765
shows "blexer_simp r [] = blexer r []"
+ − 1766
apply(simp add: blexer_def blexer_simp_def)
+ − 1767
done
+ − 1768
+ − 1769
lemma bbs1:
+ − 1770
shows "blexer_simp r [c] = blexer r [c]"
+ − 1771
apply(simp add: blexer_def blexer_simp_def)
+ − 1772
apply(auto)
+ − 1773
defer
+ − 1774
using b3 apply auto[1]
+ − 1775
using b3 apply auto[1]
+ − 1776
apply(subst bmkeps_simp[symmetric])
+ − 1777
apply(simp)
+ − 1778
apply(simp)
+ − 1779
done
+ − 1780
+ − 1781
lemma oo:
+ − 1782
shows "(case (blexer (der c r) s) of None \<Rightarrow> None | Some v \<Rightarrow> Some (injval r c v)) = blexer r (c # s)"
+ − 1783
apply(simp add: blexer_correctness)
+ − 1784
done
+ − 1785
+ − 1786
+ − 1787
lemma bder_fuse:
+ − 1788
shows "bder c (fuse bs a) = fuse bs (bder c a)"
+ − 1789
apply(induct a arbitrary: bs c)
+ − 1790
apply(simp_all)
+ − 1791
done
+ − 1792
+ − 1793
+ − 1794
fun flts2 :: "char \<Rightarrow> arexp list \<Rightarrow> arexp list"
+ − 1795
where
+ − 1796
"flts2 _ [] = []"
+ − 1797
| "flts2 c (AZERO # rs) = flts2 c rs"
+ − 1798
| "flts2 c (AONE _ # rs) = flts2 c rs"
+ − 1799
| "flts2 c (ACHAR bs d # rs) = (if c = d then (ACHAR bs d # flts2 c rs) else flts2 c rs)"
+ − 1800
| "flts2 c ((AALTs bs rs1) # rs) = (map (fuse bs) rs1) @ flts2 c rs"
+ − 1801
| "flts2 c (ASEQ bs r1 r2 # rs) = (if (bnullable(r1) \<and> r2 = AZERO) then
+ − 1802
flts2 c rs
+ − 1803
else ASEQ bs r1 r2 # flts2 c rs)"
+ − 1804
| "flts2 c (r1 # rs) = r1 # flts2 c rs"
+ − 1805
+ − 1806
lemma flts2_k0:
+ − 1807
shows "flts2 c (r # rs1) = flts2 c [r] @ flts2 c rs1"
+ − 1808
apply(induct r arbitrary: c rs1)
+ − 1809
apply(auto)
+ − 1810
done
+ − 1811
+ − 1812
lemma flts2_k00:
+ − 1813
shows "flts2 c (rs1 @ rs2) = flts2 c rs1 @ flts2 c rs2"
+ − 1814
apply(induct rs1 arbitrary: rs2 c)
+ − 1815
apply(auto)
+ − 1816
by (metis append.assoc flts2_k0)
+ − 1817
+ − 1818
+ − 1819
lemma
+ − 1820
shows "flts (map (bder c) rs) = (map (bder c) (flts2 c rs))"
+ − 1821
apply(induct c rs rule: flts2.induct)
+ − 1822
apply(simp)
+ − 1823
apply(simp)
+ − 1824
apply(simp)
+ − 1825
apply(simp)
+ − 1826
apply(simp)
+ − 1827
apply(auto simp add: bder_fuse)[1]
+ − 1828
defer
+ − 1829
apply(simp)
+ − 1830
apply(simp del: flts2.simps)
+ − 1831
apply(rule conjI)
+ − 1832
prefer 2
+ − 1833
apply(auto)[1]
+ − 1834
apply(rule impI)
+ − 1835
apply(subst flts2_k0)
+ − 1836
apply(subst map_append)
+ − 1837
apply(subst flts2.simps)
+ − 1838
apply(simp only: flts2.simps)
+ − 1839
apply(auto)
+ − 1840
+ − 1841
+ − 1842
+ − 1843
lemma XXX2_helper:
+ − 1844
assumes "\<forall>y. asize y < Suc (sum_list (map asize rs)) \<longrightarrow> good y \<longrightarrow> bsimp y = y"
+ − 1845
"\<forall>r'\<in>set rs. good r' \<and> nonalt r'"
+ − 1846
shows "flts (map (bsimp \<circ> bder c) (flts (map bsimp rs))) = flts (map (bsimp \<circ> bder c) rs)"
+ − 1847
using assms
+ − 1848
apply(induct rs arbitrary: c)
+ − 1849
apply(simp)
+ − 1850
apply(simp)
+ − 1851
apply(subst k0)
+ − 1852
apply(simp add: flts_append)
+ − 1853
apply(subst (2) k0)
+ − 1854
apply(simp add: flts_append)
+ − 1855
apply(subgoal_tac "flts [a] = [a]")
+ − 1856
prefer 2
+ − 1857
using good.simps(1) k0b apply blast
+ − 1858
apply(simp)
+ − 1859
done
+ − 1860
+ − 1861
lemma bmkeps_good:
+ − 1862
assumes "good a"
+ − 1863
shows "bmkeps (bsimp a) = bmkeps a"
+ − 1864
using assms
+ − 1865
using test2 by auto
+ − 1866
+ − 1867
+ − 1868
lemma xxx_bder:
+ − 1869
assumes "good r"
+ − 1870
shows "L (erase r) \<noteq> {}"
+ − 1871
using assms
+ − 1872
apply(induct r rule: good.induct)
+ − 1873
apply(auto simp add: Sequ_def)
+ − 1874
done
+ − 1875
+ − 1876
lemma xxx_bder2:
+ − 1877
assumes "L (erase (bsimp r)) = {}"
+ − 1878
shows "bsimp r = AZERO"
+ − 1879
using assms xxx_bder test2 good1
+ − 1880
by blast
+ − 1881
+ − 1882
lemma XXX2aa:
+ − 1883
assumes "good a"
+ − 1884
shows "bsimp (bder c (bsimp a)) = bsimp (bder c a)"
+ − 1885
using assms
+ − 1886
by (simp add: test2)
+ − 1887
+ − 1888
lemma XXX2aa_ders:
+ − 1889
assumes "good a"
+ − 1890
shows "bsimp (bders (bsimp a) s) = bsimp (bders a s)"
+ − 1891
using assms
+ − 1892
by (simp add: test2)
+ − 1893
+ − 1894
lemma XXX4a:
+ − 1895
shows "good (bders_simp (bsimp r) s) \<or> bders_simp (bsimp r) s = AZERO"
+ − 1896
apply(induct s arbitrary: r rule: rev_induct)
+ − 1897
apply(simp)
+ − 1898
apply (simp add: good1)
+ − 1899
apply(simp add: bders_simp_append)
+ − 1900
apply (simp add: good1)
+ − 1901
done
+ − 1902
+ − 1903
lemma XXX4a_good:
+ − 1904
assumes "good a"
+ − 1905
shows "good (bders_simp a s) \<or> bders_simp a s = AZERO"
+ − 1906
using assms
+ − 1907
apply(induct s arbitrary: a rule: rev_induct)
+ − 1908
apply(simp)
+ − 1909
apply(simp add: bders_simp_append)
+ − 1910
apply (simp add: good1)
+ − 1911
done
+ − 1912
+ − 1913
lemma XXX4a_good_cons:
+ − 1914
assumes "s \<noteq> []"
+ − 1915
shows "good (bders_simp a s) \<or> bders_simp a s = AZERO"
+ − 1916
using assms
+ − 1917
apply(case_tac s)
+ − 1918
apply(auto)
+ − 1919
using XXX4a by blast
+ − 1920
+ − 1921
lemma XXX4b:
+ − 1922
assumes "good a" "L (erase (bders_simp a s)) \<noteq> {}"
+ − 1923
shows "good (bders_simp a s)"
+ − 1924
using assms
+ − 1925
apply(induct s arbitrary: a)
+ − 1926
apply(simp)
+ − 1927
apply(simp)
+ − 1928
apply(subgoal_tac "L (erase (bder a aa)) = {} \<or> L (erase (bder a aa)) \<noteq> {}")
+ − 1929
prefer 2
+ − 1930
apply(auto)[1]
+ − 1931
apply(erule disjE)
+ − 1932
apply(subgoal_tac "bsimp (bder a aa) = AZERO")
+ − 1933
prefer 2
+ − 1934
using L_bsimp_erase xxx_bder2 apply auto[1]
+ − 1935
apply(simp)
+ − 1936
apply (metis L.simps(1) XXX4a erase.simps(1))
+ − 1937
apply(drule_tac x="bsimp (bder a aa)" in meta_spec)
+ − 1938
apply(drule meta_mp)
+ − 1939
apply simp
+ − 1940
apply(rule good1a)
+ − 1941
apply(auto)
+ − 1942
done
+ − 1943
+ − 1944
lemma bders_AZERO:
+ − 1945
shows "bders AZERO s = AZERO"
+ − 1946
and "bders_simp AZERO s = AZERO"
+ − 1947
apply (induct s)
+ − 1948
apply(auto)
+ − 1949
done
+ − 1950
+ − 1951
lemma LA:
+ − 1952
assumes "\<Turnstile> v : ders s (erase r)"
+ − 1953
shows "retrieve (bders r s) v = retrieve r (flex (erase r) id s v)"
+ − 1954
using assms
+ − 1955
apply(induct s arbitrary: r v rule: rev_induct)
+ − 1956
apply(simp)
+ − 1957
apply(simp add: bders_append ders_append)
+ − 1958
apply(subst bder_retrieve)
+ − 1959
apply(simp)
+ − 1960
apply(drule Prf_injval)
+ − 1961
by (simp add: flex_append)
+ − 1962
+ − 1963
+ − 1964
lemma LB:
+ − 1965
assumes "s \<in> (erase r) \<rightarrow> v"
+ − 1966
shows "retrieve r v = retrieve r (flex (erase r) id s (mkeps (ders s (erase r))))"
+ − 1967
using assms
+ − 1968
apply(induct s arbitrary: r v rule: rev_induct)
+ − 1969
apply(simp)
+ − 1970
apply(subgoal_tac "v = mkeps (erase r)")
+ − 1971
prefer 2
+ − 1972
apply (simp add: Posix1(1) Posix_determ Posix_mkeps nullable_correctness)
+ − 1973
apply(simp)
+ − 1974
apply(simp add: flex_append ders_append)
+ − 1975
by (metis Posix_determ Posix_flex Posix_injval Posix_mkeps ders_snoc lexer_correctness(2) lexer_flex)
+ − 1976
+ − 1977
lemma LB_sym:
+ − 1978
assumes "s \<in> (erase r) \<rightarrow> v"
+ − 1979
shows "retrieve r v = retrieve r (flex (erase r) id s (mkeps (erase (bders r s))))"
+ − 1980
using assms
+ − 1981
by (simp add: LB)
+ − 1982
+ − 1983
+ − 1984
lemma LC:
+ − 1985
assumes "s \<in> (erase r) \<rightarrow> v"
+ − 1986
shows "retrieve r v = retrieve (bders r s) (mkeps (erase (bders r s)))"
+ − 1987
apply(simp)
+ − 1988
by (metis LA LB Posix1(1) assms lexer_correct_None lexer_flex mkeps_nullable)
+ − 1989
+ − 1990
+ − 1991
lemma L0:
+ − 1992
assumes "bnullable a"
+ − 1993
shows "retrieve (bsimp a) (mkeps (erase (bsimp a))) = retrieve a (mkeps (erase a))"
+ − 1994
using assms
+ − 1995
by (metis b3 bmkeps_retrieve bmkeps_simp bnullable_correctness)
+ − 1996
+ − 1997
thm bmkeps_retrieve
+ − 1998
+ − 1999
lemma L0a:
+ − 2000
assumes "s \<in> L(erase a)"
+ − 2001
shows "retrieve (bsimp (bders a s)) (mkeps (erase (bsimp (bders a s)))) =
+ − 2002
retrieve (bders a s) (mkeps (erase (bders a s)))"
+ − 2003
using assms
+ − 2004
by (metis L0 bnullable_correctness erase_bders lexer_correct_None lexer_flex)
+ − 2005
+ − 2006
lemma L0aa:
+ − 2007
assumes "s \<in> L (erase a)"
+ − 2008
shows "[] \<in> erase (bsimp (bders a s)) \<rightarrow> mkeps (erase (bsimp (bders a s)))"
+ − 2009
using assms
+ − 2010
by (metis Posix_mkeps b3 bnullable_correctness erase_bders lexer_correct_None lexer_flex)
+ − 2011
+ − 2012
lemma L0aaa:
+ − 2013
assumes "[c] \<in> L (erase a)"
+ − 2014
shows "[c] \<in> (erase a) \<rightarrow> flex (erase a) id [c] (mkeps (erase (bder c a)))"
+ − 2015
using assms
+ − 2016
by (metis bders.simps(1) bders.simps(2) erase_bders lexer_correct_None lexer_correct_Some lexer_flex option.inject)
+ − 2017
+ − 2018
lemma L0aaaa:
+ − 2019
assumes "[c] \<in> L (erase a)"
+ − 2020
shows "[c] \<in> (erase a) \<rightarrow> flex (erase a) id [c] (mkeps (erase (bders a [c])))"
+ − 2021
using assms
+ − 2022
using L0aaa by auto
+ − 2023
+ − 2024
+ − 2025
lemma L02:
+ − 2026
assumes "bnullable (bder c a)"
+ − 2027
shows "retrieve (bsimp a) (flex (erase (bsimp a)) id [c] (mkeps (erase (bder c (bsimp a))))) =
+ − 2028
retrieve (bder c (bsimp a)) (mkeps (erase (bder c (bsimp a))))"
+ − 2029
using assms
+ − 2030
apply(simp)
+ − 2031
using bder_retrieve L0 bmkeps_simp bmkeps_retrieve L0 LA LB
+ − 2032
apply(subst bder_retrieve[symmetric])
+ − 2033
apply (metis L_bsimp_erase bnullable_correctness der_correctness erase_bder mkeps_nullable nullable_correctness)
+ − 2034
apply(simp)
+ − 2035
done
+ − 2036
+ − 2037
lemma L02_bders:
+ − 2038
assumes "bnullable (bders a s)"
+ − 2039
shows "retrieve (bsimp a) (flex (erase (bsimp a)) id s (mkeps (erase (bders (bsimp a) s)))) =
+ − 2040
retrieve (bders (bsimp a) s) (mkeps (erase (bders (bsimp a) s)))"
+ − 2041
using assms
+ − 2042
by (metis LA L_bsimp_erase bnullable_correctness ders_correctness erase_bders mkeps_nullable nullable_correctness)
+ − 2043
+ − 2044
+ − 2045
+ − 2046
+ − 2047
lemma L03:
+ − 2048
assumes "bnullable (bder c a)"
+ − 2049
shows "retrieve (bder c (bsimp a)) (mkeps (erase (bder c (bsimp a)))) =
+ − 2050
bmkeps (bsimp (bder c (bsimp a)))"
+ − 2051
using assms
+ − 2052
by (metis L0 L_bsimp_erase bmkeps_retrieve bnullable_correctness der_correctness erase_bder nullable_correctness)
+ − 2053
+ − 2054
lemma L04:
+ − 2055
assumes "bnullable (bder c a)"
+ − 2056
shows "retrieve (bder c (bsimp a)) (mkeps (erase (bder c (bsimp a)))) =
+ − 2057
retrieve (bsimp (bder c (bsimp a))) (mkeps (erase (bsimp (bder c (bsimp a)))))"
+ − 2058
using assms
+ − 2059
by (metis L0 L_bsimp_erase bnullable_correctness der_correctness erase_bder nullable_correctness)
+ − 2060
+ − 2061
lemma L05:
+ − 2062
assumes "bnullable (bder c a)"
+ − 2063
shows "retrieve (bder c (bsimp a)) (mkeps (erase (bder c (bsimp a)))) =
+ − 2064
retrieve (bsimp (bder c (bsimp a))) (mkeps (erase (bsimp (bder c (bsimp a)))))"
+ − 2065
using assms
+ − 2066
using L04 by auto
+ − 2067
+ − 2068
lemma L06:
+ − 2069
assumes "bnullable (bder c a)"
+ − 2070
shows "bmkeps (bder c (bsimp a)) = bmkeps (bsimp (bder c (bsimp a)))"
+ − 2071
using assms
+ − 2072
by (metis L03 L_bsimp_erase bmkeps_retrieve bnullable_correctness der_correctness erase_bder nullable_correctness)
+ − 2073
+ − 2074
lemma L07:
+ − 2075
assumes "s \<in> L (erase r)"
+ − 2076
shows "retrieve r (flex (erase r) id s (mkeps (ders s (erase r))))
+ − 2077
= retrieve (bders r s) (mkeps (erase (bders r s)))"
+ − 2078
using assms
+ − 2079
using LB LC lexer_correct_Some by auto
+ − 2080
+ − 2081
lemma LXXX:
+ − 2082
assumes "s \<in> (erase r) \<rightarrow> v" "s \<in> (erase (bsimp r)) \<rightarrow> v'"
+ − 2083
shows "retrieve r v = retrieve (bsimp r) v'"
+ − 2084
using assms
+ − 2085
apply -
+ − 2086
thm LC
+ − 2087
apply(subst LC)
+ − 2088
apply(assumption)
+ − 2089
apply(subst L0[symmetric])
+ − 2090
using bnullable_correctness lexer_correctness(2) lexer_flex apply fastforce
+ − 2091
apply(subst (2) LC)
+ − 2092
apply(assumption)
+ − 2093
apply(subst (2) L0[symmetric])
+ − 2094
using bnullable_correctness lexer_correctness(2) lexer_flex apply fastforce
+ − 2095
+ − 2096
oops
+ − 2097
+ − 2098
+ − 2099
lemma L07a:
+ − 2100
assumes "s \<in> L (erase r)"
+ − 2101
shows "retrieve (bsimp r) (flex (erase (bsimp r)) id s (mkeps (ders s (erase (bsimp r)))))
+ − 2102
= retrieve r (flex (erase r) id s (mkeps (ders s (erase r))))"
+ − 2103
using assms
+ − 2104
apply(induct s arbitrary: r)
+ − 2105
apply(simp)
+ − 2106
using L0a apply force
+ − 2107
apply(drule_tac x="(bder a r)" in meta_spec)
+ − 2108
apply(drule meta_mp)
+ − 2109
apply (metis L_bsimp_erase erase_bder lexer.simps(2) lexer_correct_None option.case(1))
+ − 2110
apply(drule sym)
+ − 2111
apply(simp)
+ − 2112
apply(subst (asm) bder_retrieve)
+ − 2113
apply (metis Posix_Prf Posix_flex Posix_mkeps ders.simps(2) lexer_correct_None lexer_flex)
+ − 2114
apply(simp only: flex_fun_apply)
+ − 2115
apply(simp)
+ − 2116
using L0[no_vars] bder_retrieve[no_vars] LA[no_vars] LC[no_vars] L07[no_vars]
+ − 2117
oops
+ − 2118
+ − 2119
lemma L08:
+ − 2120
assumes "s \<in> L (erase r)"
+ − 2121
shows "retrieve (bders (bsimp r) s) (mkeps (erase (bders (bsimp r) s)))
+ − 2122
= retrieve (bders r s) (mkeps (erase (bders r s)))"
+ − 2123
using assms
+ − 2124
apply(induct s arbitrary: r)
+ − 2125
apply(simp)
+ − 2126
using L0 bnullable_correctness nullable_correctness apply blast
+ − 2127
apply(simp add: bders_append)
+ − 2128
apply(drule_tac x="(bder a (bsimp r))" in meta_spec)
+ − 2129
apply(drule meta_mp)
+ − 2130
apply (metis L_bsimp_erase erase_bder lexer.simps(2) lexer_correct_None option.case(1))
+ − 2131
apply(drule sym)
+ − 2132
apply(simp)
+ − 2133
apply(subst LA)
+ − 2134
apply (metis L0aa L_bsimp_erase Posix1(1) ders.simps(2) ders_correctness erase_bder erase_bders mkeps_nullable nullable_correctness)
+ − 2135
apply(subst LA)
+ − 2136
using lexer_correct_None lexer_flex mkeps_nullable apply force
+ − 2137
+ − 2138
using L0[no_vars] bder_retrieve[no_vars] LA[no_vars] LC[no_vars] L07[no_vars]
+ − 2139
+ − 2140
thm L0[no_vars] bder_retrieve[no_vars] LA[no_vars] LC[no_vars] L07[no_vars]
+ − 2141
oops
+ − 2142
+ − 2143
lemma test:
+ − 2144
assumes "s = [c]"
+ − 2145
shows "retrieve (bders r s) v = XXX" and "YYY = retrieve r (flex (erase r) id s v)"
+ − 2146
using assms
+ − 2147
apply(simp only: bders.simps)
+ − 2148
defer
+ − 2149
using assms
+ − 2150
apply(simp only: flex.simps id_simps)
+ − 2151
using L0[no_vars] bder_retrieve[no_vars] LA[no_vars] LC[no_vars]
+ − 2152
find_theorems "retrieve (bders _ _) _"
+ − 2153
find_theorems "retrieve _ (mkeps _)"
+ − 2154
oops
+ − 2155
+ − 2156
lemma L06X:
+ − 2157
assumes "bnullable (bder c a)"
+ − 2158
shows "bmkeps (bder c (bsimp a)) = bmkeps (bder c a)"
+ − 2159
using assms
+ − 2160
apply(induct a arbitrary: c)
+ − 2161
apply(simp)
+ − 2162
apply(simp)
+ − 2163
apply(simp)
+ − 2164
prefer 3
+ − 2165
apply(simp)
+ − 2166
prefer 2
+ − 2167
apply(simp)
+ − 2168
+ − 2169
defer
+ − 2170
oops
+ − 2171
+ − 2172
lemma L06_2:
+ − 2173
assumes "bnullable (bders a [c,d])"
+ − 2174
shows "bmkeps (bders (bsimp a) [c,d]) = bmkeps (bsimp (bders (bsimp a) [c,d]))"
+ − 2175
using assms
+ − 2176
apply(simp)
+ − 2177
by (metis L_bsimp_erase bmkeps_simp bnullable_correctness der_correctness erase_bder nullable_correctness)
+ − 2178
+ − 2179
lemma L06_bders:
+ − 2180
assumes "bnullable (bders a s)"
+ − 2181
shows "bmkeps (bders (bsimp a) s) = bmkeps (bsimp (bders (bsimp a) s))"
+ − 2182
using assms
+ − 2183
by (metis L_bsimp_erase bmkeps_simp bnullable_correctness ders_correctness erase_bders nullable_correctness)
+ − 2184
+ − 2185
lemma LLLL:
+ − 2186
shows "L (erase a) = L (erase (bsimp a))"
+ − 2187
and "L (erase a) = {flat v | v. \<Turnstile> v: (erase a)}"
+ − 2188
and "L (erase a) = {flat v | v. \<Turnstile> v: (erase (bsimp a))}"
+ − 2189
using L_bsimp_erase apply(blast)
+ − 2190
apply (simp add: L_flat_Prf)
+ − 2191
using L_bsimp_erase L_flat_Prf apply(auto)[1]
+ − 2192
done
+ − 2193
+ − 2194
+ − 2195
+ − 2196
lemma L07XX:
+ − 2197
assumes "s \<in> L (erase a)"
+ − 2198
shows "s \<in> erase a \<rightarrow> flex (erase a) id s (mkeps (ders s (erase a)))"
+ − 2199
using assms
+ − 2200
by (meson lexer_correct_None lexer_correctness(1) lexer_flex)
+ − 2201
+ − 2202
lemma LX0:
+ − 2203
assumes "s \<in> L r"
+ − 2204
shows "decode (bmkeps (bders (intern r) s)) r = Some(flex r id s (mkeps (ders s r)))"
+ − 2205
by (metis assms blexer_correctness blexer_def lexer_correct_None lexer_flex)
+ − 2206
+ − 2207
+ − 2208
lemma L02_bders2:
+ − 2209
assumes "bnullable (bders a s)" "s = [c]"
+ − 2210
shows "retrieve (bders (bsimp a) s) (mkeps (erase (bders (bsimp a) s))) =
+ − 2211
retrieve (bders a s) (mkeps (erase (bders a s)))"
+ − 2212
using assms
+ − 2213
apply(simp)
+ − 2214
+ − 2215
apply(induct s arbitrary: a)
+ − 2216
apply(simp)
+ − 2217
using L0 apply auto[1]
+ − 2218
oops
+ − 2219
+ − 2220
thm bmkeps_retrieve bmkeps_simp Posix_mkeps
+ − 2221
+ − 2222
lemma WQ1:
+ − 2223
assumes "s \<in> L (der c r)"
+ − 2224
shows "s \<in> der c r \<rightarrow> mkeps (ders s (der c r))"
+ − 2225
using assms
+ − 2226
oops
+ − 2227
+ − 2228
lemma L02_bsimp:
+ − 2229
assumes "bnullable (bders a s)"
+ − 2230
shows "retrieve (bsimp a) (flex (erase (bsimp a)) id s (mkeps (erase (bders (bsimp a) s)))) =
+ − 2231
retrieve a (flex (erase a) id s (mkeps (erase (bders a s))))"
+ − 2232
using assms
+ − 2233
apply(induct s arbitrary: a)
+ − 2234
apply(simp)
+ − 2235
apply (simp add: L0)
+ − 2236
apply(simp)
+ − 2237
apply(drule_tac x="bder a aa" in meta_spec)
+ − 2238
apply(simp)
+ − 2239
apply(subst (asm) bder_retrieve)
+ − 2240
using Posix_Prf Posix_flex Posix_mkeps bnullable_correctness apply fastforce
+ − 2241
apply(simp add: flex_fun_apply)
+ − 2242
apply(drule sym)
+ − 2243
apply(simp)
+ − 2244
apply(subst flex_injval)
+ − 2245
apply(subst bder_retrieve[symmetric])
+ − 2246
apply (metis L_bsimp_erase Posix_Prf Posix_flex Posix_mkeps bders.simps(2) bnullable_correctness ders.simps(2) erase_bders lexer_correct_None lexer_flex option.distinct(1))
+ − 2247
apply(simp only: erase_bder[symmetric] erase_bders[symmetric])
+ − 2248
apply(subst LB_sym[symmetric])
+ − 2249
apply(simp)
+ − 2250
oops
+ − 2251
+ − 2252
lemma L1:
+ − 2253
assumes "s \<in> r \<rightarrow> v"
+ − 2254
shows "decode (bmkeps (bders (intern r) s)) r = Some v"
+ − 2255
using assms
+ − 2256
by (metis blexer_correctness blexer_def lexer_correctness(1) option.distinct(1))
+ − 2257
+ − 2258
lemma L2:
+ − 2259
assumes "s \<in> (der c r) \<rightarrow> v"
+ − 2260
shows "decode (bmkeps (bders (intern r) (c # s))) r = Some (injval r c v)"
+ − 2261
using assms
+ − 2262
apply(subst bmkeps_retrieve)
+ − 2263
using Posix1(1) lexer_correct_None lexer_flex apply fastforce
+ − 2264
using MAIN_decode
+ − 2265
apply(subst MAIN_decode[symmetric])
+ − 2266
apply(simp)
+ − 2267
apply (meson Posix1(1) lexer_correct_None lexer_flex mkeps_nullable)
+ − 2268
apply(simp)
+ − 2269
apply(subgoal_tac "v = flex (der c r) id s (mkeps (ders s (der c r)))")
+ − 2270
prefer 2
+ − 2271
apply (metis Posix_determ lexer_correctness(1) lexer_flex option.distinct(1))
+ − 2272
apply(simp)
+ − 2273
apply(subgoal_tac "injval r c (flex (der c r) id s (mkeps (ders s (der c r)))) =
+ − 2274
(flex (der c r) ((\<lambda>v. injval r c v) o id) s (mkeps (ders s (der c r))))")
+ − 2275
apply(simp)
+ − 2276
using flex_fun_apply by blast
+ − 2277
+ − 2278
lemma L3:
+ − 2279
assumes "s2 \<in> (ders s1 r) \<rightarrow> v"
+ − 2280
shows "decode (bmkeps (bders (intern r) (s1 @ s2))) r = Some (flex r id s1 v)"
+ − 2281
using assms
+ − 2282
apply(induct s1 arbitrary: r s2 v rule: rev_induct)
+ − 2283
apply(simp)
+ − 2284
using L1 apply blast
+ − 2285
apply(simp add: ders_append)
+ − 2286
apply(drule_tac x="r" in meta_spec)
+ − 2287
apply(drule_tac x="x # s2" in meta_spec)
+ − 2288
apply(drule_tac x="injval (ders xs r) x v" in meta_spec)
+ − 2289
apply(drule meta_mp)
+ − 2290
defer
+ − 2291
apply(simp)
+ − 2292
apply(simp add: flex_append)
+ − 2293
by (simp add: Posix_injval)
+ − 2294
+ − 2295
+ − 2296
+ − 2297
lemma bders_snoc:
+ − 2298
"bder c (bders a s) = bders a (s @ [c])"
+ − 2299
apply(simp add: bders_append)
+ − 2300
done
+ − 2301
+ − 2302
+ − 2303
lemma QQ1:
+ − 2304
shows "bsimp (bders (bsimp a) []) = bders_simp (bsimp a) []"
+ − 2305
apply(simp)
+ − 2306
apply(simp add: bsimp_idem)
+ − 2307
done
+ − 2308
+ − 2309
lemma QQ2:
+ − 2310
shows "bsimp (bders (bsimp a) [c]) = bders_simp (bsimp a) [c]"
+ − 2311
apply(simp)
+ − 2312
done
+ − 2313
+ − 2314
lemma XXX2a_long:
+ − 2315
assumes "good a"
+ − 2316
shows "bsimp (bder c (bsimp a)) = bsimp (bder c a)"
+ − 2317
using assms
+ − 2318
apply(induct a arbitrary: c taking: asize rule: measure_induct)
+ − 2319
apply(case_tac x)
+ − 2320
apply(simp)
+ − 2321
apply(simp)
+ − 2322
apply(simp)
+ − 2323
prefer 3
+ − 2324
apply(simp)
+ − 2325
apply(simp)
+ − 2326
apply(auto)[1]
+ − 2327
apply(case_tac "x42 = AZERO")
+ − 2328
apply(simp)
+ − 2329
apply(case_tac "x43 = AZERO")
+ − 2330
apply(simp)
+ − 2331
using test2 apply force
+ − 2332
apply(case_tac "\<exists>bs. x42 = AONE bs")
+ − 2333
apply(clarify)
+ − 2334
apply(simp)
+ − 2335
apply(subst bsimp_ASEQ1)
+ − 2336
apply(simp)
+ − 2337
using b3 apply force
+ − 2338
using bsimp_ASEQ0 test2 apply force
+ − 2339
thm good_SEQ test2
+ − 2340
apply (simp add: good_SEQ test2)
+ − 2341
apply (simp add: good_SEQ test2)
+ − 2342
apply(case_tac "x42 = AZERO")
+ − 2343
apply(simp)
+ − 2344
apply(case_tac "x43 = AZERO")
+ − 2345
apply(simp)
+ − 2346
apply (simp add: bsimp_ASEQ0)
+ − 2347
apply(case_tac "\<exists>bs. x42 = AONE bs")
+ − 2348
apply(clarify)
+ − 2349
apply(simp)
+ − 2350
apply(subst bsimp_ASEQ1)
+ − 2351
apply(simp)
+ − 2352
using bsimp_ASEQ0 test2 apply force
+ − 2353
apply (simp add: good_SEQ test2)
+ − 2354
apply (simp add: good_SEQ test2)
+ − 2355
apply (simp add: good_SEQ test2)
+ − 2356
(* AALTs case *)
+ − 2357
apply(simp)
+ − 2358
using test2 by fastforce
+ − 2359
+ − 2360
lemma XXX2a_long_without_good:
+ − 2361
assumes "a = AALTs bs0 [AALTs bs1 [AALTs bs2 [ASTAR [] (AONE bs7), AONE bs6, ASEQ bs3 (ACHAR bs4 d) (AONE bs5)]]]"
+ − 2362
shows "bsimp (bder c (bsimp a)) = bsimp (bder c a)"
+ − 2363
"bsimp (bder c (bsimp a)) = XXX"
+ − 2364
"bsimp (bder c a) = YYY"
+ − 2365
using assms
+ − 2366
apply(simp)
+ − 2367
using assms
+ − 2368
apply(simp)
+ − 2369
prefer 2
+ − 2370
using assms
+ − 2371
apply(simp)
+ − 2372
oops
+ − 2373
+ − 2374
lemma bder_bsimp_AALTs:
+ − 2375
shows "bder c (bsimp_AALTs bs rs) = bsimp_AALTs bs (map (bder c) rs)"
+ − 2376
apply(induct bs rs rule: bsimp_AALTs.induct)
+ − 2377
apply(simp)
+ − 2378
apply(simp)
+ − 2379
apply (simp add: bder_fuse)
+ − 2380
apply(simp)
+ − 2381
done
+ − 2382
+ − 2383
lemma flts_nothing:
+ − 2384
assumes "\<forall>r \<in> set rs. r \<noteq> AZERO" "\<forall>r \<in> set rs. nonalt r"
+ − 2385
shows "flts rs = rs"
+ − 2386
using assms
+ − 2387
apply(induct rs rule: flts.induct)
+ − 2388
apply(auto)
+ − 2389
done
+ − 2390
+ − 2391
lemma flts_flts:
+ − 2392
assumes "\<forall>r \<in> set rs. good r"
+ − 2393
shows "flts (flts rs) = flts rs"
+ − 2394
using assms
+ − 2395
apply(induct rs taking: "\<lambda>rs. sum_list (map asize rs)" rule: measure_induct)
+ − 2396
apply(case_tac x)
+ − 2397
apply(simp)
+ − 2398
apply(simp)
+ − 2399
apply(case_tac a)
+ − 2400
apply(simp_all add: bder_fuse flts_append)
+ − 2401
apply(subgoal_tac "\<forall>r \<in> set x52. r \<noteq> AZERO")
+ − 2402
prefer 2
+ − 2403
apply (metis Nil_is_append_conv bsimp_AALTs.elims good.simps(1) good.simps(5) good0 list.distinct(1) n0 nn1b split_list_last test2)
+ − 2404
apply(subgoal_tac "\<forall>r \<in> set x52. nonalt r")
+ − 2405
prefer 2
+ − 2406
apply (metis n0 nn1b test2)
+ − 2407
by (metis flts_fuse flts_nothing)
+ − 2408
+ − 2409
+ − 2410
lemma PP:
+ − 2411
assumes "bnullable (bders r s)"
+ − 2412
shows "bmkeps (bders (bsimp r) s) = bmkeps (bders r s)"
+ − 2413
using assms
+ − 2414
apply(induct s arbitrary: r)
+ − 2415
apply(simp)
+ − 2416
using bmkeps_simp apply auto[1]
+ − 2417
apply(simp add: bders_append bders_simp_append)
+ − 2418
oops
+ − 2419
+ − 2420
lemma PP:
+ − 2421
assumes "bnullable (bders r s)"
+ − 2422
shows "bmkeps (bders_simp (bsimp r) s) = bmkeps (bders r s)"
+ − 2423
using assms
+ − 2424
apply(induct s arbitrary: r rule: rev_induct)
+ − 2425
apply(simp)
+ − 2426
using bmkeps_simp apply auto[1]
+ − 2427
apply(simp add: bders_append bders_simp_append)
+ − 2428
apply(drule_tac x="bder a (bsimp r)" in meta_spec)
+ − 2429
apply(drule_tac meta_mp)
+ − 2430
defer
+ − 2431
oops
+ − 2432
+ − 2433
+ − 2434
lemma
+ − 2435
assumes "asize (bsimp a) = asize a" "a = AALTs bs [AALTs bs2 [], AZERO, AONE bs3]"
+ − 2436
shows "bsimp a = a"
+ − 2437
using assms
+ − 2438
apply(simp)
+ − 2439
oops
+ − 2440
+ − 2441
+ − 2442
lemma iii:
+ − 2443
assumes "bsimp_AALTs bs rs \<noteq> AZERO"
+ − 2444
shows "rs \<noteq> []"
+ − 2445
using assms
+ − 2446
apply(induct bs rs rule: bsimp_AALTs.induct)
+ − 2447
apply(auto)
+ − 2448
done
+ − 2449
+ − 2450
lemma CT1_SEQ:
+ − 2451
shows "bsimp (ASEQ bs a1 a2) = bsimp (ASEQ bs (bsimp a1) (bsimp a2))"
+ − 2452
apply(simp add: bsimp_idem)
+ − 2453
done
+ − 2454
+ − 2455
lemma CT1:
+ − 2456
shows "bsimp (AALTs bs as) = bsimp (AALTs bs (map bsimp as))"
+ − 2457
apply(induct as arbitrary: bs)
+ − 2458
apply(simp)
+ − 2459
apply(simp)
+ − 2460
by (simp add: bsimp_idem comp_def)
+ − 2461
+ − 2462
lemma CT1a:
+ − 2463
shows "bsimp (AALT bs a1 a2) = bsimp(AALT bs (bsimp a1) (bsimp a2))"
+ − 2464
by (metis CT1 list.simps(8) list.simps(9))
+ − 2465
+ − 2466
lemma WWW2:
+ − 2467
shows "bsimp (bsimp_AALTs bs1 (flts (map bsimp as1))) =
+ − 2468
bsimp_AALTs bs1 (flts (map bsimp as1))"
+ − 2469
by (metis bsimp.simps(2) bsimp_idem)
+ − 2470
+ − 2471
lemma CT1b:
+ − 2472
shows "bsimp (bsimp_AALTs bs as) = bsimp (bsimp_AALTs bs (map bsimp as))"
+ − 2473
apply(induct bs as rule: bsimp_AALTs.induct)
+ − 2474
apply(auto simp add: bsimp_idem)
+ − 2475
apply (simp add: bsimp_fuse bsimp_idem)
+ − 2476
by (metis bsimp_idem comp_apply)
+ − 2477
+ − 2478
+ − 2479
+ − 2480
+ − 2481
(* CT *)
+ − 2482
+ − 2483
lemma CTU:
+ − 2484
shows "bsimp_AALTs bs as = li bs as"
+ − 2485
apply(induct bs as rule: li.induct)
+ − 2486
apply(auto)
+ − 2487
done
+ − 2488
+ − 2489
find_theorems "bder _ (bsimp_AALTs _ _)"
+ − 2490
+ − 2491
lemma CTa:
+ − 2492
assumes "\<forall>r \<in> set as. nonalt r \<and> r \<noteq> AZERO"
+ − 2493
shows "flts as = as"
+ − 2494
using assms
+ − 2495
apply(induct as)
+ − 2496
apply(simp)
+ − 2497
apply(case_tac as)
+ − 2498
apply(simp)
+ − 2499
apply (simp add: k0b)
+ − 2500
using flts_nothing by auto
+ − 2501
+ − 2502
lemma CT0:
+ − 2503
assumes "\<forall>r \<in> set as1. nonalt r \<and> r \<noteq> AZERO"
+ − 2504
shows "flts [bsimp_AALTs bs1 as1] = flts (map (fuse bs1) as1)"
+ − 2505
using assms CTa
+ − 2506
apply(induct as1 arbitrary: bs1)
+ − 2507
apply(simp)
+ − 2508
apply(simp)
+ − 2509
apply(case_tac as1)
+ − 2510
apply(simp)
+ − 2511
apply(simp)
+ − 2512
proof -
+ − 2513
fix a :: arexp and as1a :: "arexp list" and bs1a :: "bit list" and aa :: arexp and list :: "arexp list"
+ − 2514
assume a1: "nonalt a \<and> a \<noteq> AZERO \<and> nonalt aa \<and> aa \<noteq> AZERO \<and> (\<forall>r\<in>set list. nonalt r \<and> r \<noteq> AZERO)"
+ − 2515
assume a2: "\<And>as. \<forall>r\<in>set as. nonalt r \<and> r \<noteq> AZERO \<Longrightarrow> flts as = as"
+ − 2516
assume a3: "as1a = aa # list"
+ − 2517
have "flts [a] = [a]"
+ − 2518
using a1 k0b by blast
+ − 2519
then show "fuse bs1a a # fuse bs1a aa # map (fuse bs1a) list = flts (fuse bs1a a # fuse bs1a aa # map (fuse bs1a) list)"
+ − 2520
using a3 a2 a1 by (metis (no_types) append.left_neutral append_Cons flts_fuse k00 k0b list.simps(9))
+ − 2521
qed
+ − 2522
+ − 2523
+ − 2524
lemma CT01:
+ − 2525
assumes "\<forall>r \<in> set as1. nonalt r \<and> r \<noteq> AZERO" "\<forall>r \<in> set as2. nonalt r \<and> r \<noteq> AZERO"
+ − 2526
shows "flts [bsimp_AALTs bs1 as1, bsimp_AALTs bs2 as2] = flts ((map (fuse bs1) as1) @ (map (fuse bs2) as2))"
+ − 2527
using assms CT0
+ − 2528
by (metis k0 k00)
+ − 2529
+ − 2530
+ − 2531
+ − 2532
lemma CT_exp:
+ − 2533
assumes "\<forall>a \<in> set as. bsimp (bder c (bsimp a)) = bsimp (bder c a)"
+ − 2534
shows "map bsimp (map (bder c) as) = map bsimp (map (bder c) (map bsimp as))"
+ − 2535
using assms
+ − 2536
apply(induct as)
+ − 2537
apply(auto)
+ − 2538
done
+ − 2539
+ − 2540
lemma asize_set:
+ − 2541
assumes "a \<in> set as"
+ − 2542
shows "asize a < Suc (sum_list (map asize as))"
+ − 2543
using assms
+ − 2544
apply(induct as arbitrary: a)
+ − 2545
apply(auto)
+ − 2546
using le_add2 le_less_trans not_less_eq by blast
+ − 2547
+ − 2548
+ − 2549
lemma XXX2a_long_without_good:
+ − 2550
shows "bsimp (bder c (bsimp a)) = bsimp (bder c a)"
+ − 2551
apply(induct a arbitrary: c taking: "\<lambda>a. asize a" rule: measure_induct)
+ − 2552
apply(case_tac x)
+ − 2553
apply(simp)
+ − 2554
apply(simp)
+ − 2555
apply(simp)
+ − 2556
prefer 3
+ − 2557
apply(simp)
+ − 2558
(* AALT case *)
+ − 2559
prefer 2
+ − 2560
apply(simp del: bsimp.simps)
+ − 2561
apply(subst (2) CT1)
+ − 2562
apply(subst CT_exp)
+ − 2563
apply(auto)[1]
+ − 2564
using asize_set apply blast
+ − 2565
apply(subst CT1[symmetric])
+ − 2566
apply(simp)
+ − 2567
oops
+ − 2568
+ − 2569
lemma YY:
+ − 2570
assumes "flts (map bsimp as1) = xs"
+ − 2571
shows "flts (map bsimp (map (fuse bs1) as1)) = map (fuse bs1) xs"
+ − 2572
using assms
+ − 2573
apply(induct as1 arbitrary: bs1 xs)
+ − 2574
apply(simp)
+ − 2575
apply(auto)
+ − 2576
by (metis bsimp_fuse flts_fuse k0 list.simps(9))
+ − 2577
+ − 2578
+ − 2579
lemma flts_nonalt:
+ − 2580
assumes "flts (map bsimp xs) = ys"
+ − 2581
shows "\<forall>y \<in> set ys. nonalt y"
+ − 2582
using assms
+ − 2583
apply(induct xs arbitrary: ys)
+ − 2584
apply(auto)
+ − 2585
apply(case_tac xs)
+ − 2586
apply(auto)
+ − 2587
using flts2 good1 apply fastforce
+ − 2588
by (smt ex_map_conv list.simps(9) nn1b nn1c)
+ − 2589
+ − 2590
+ − 2591
lemma WWW3:
+ − 2592
shows "flts [bsimp_AALTs bs1 (flts (map bsimp as1))] =
+ − 2593
flts (map bsimp (map (fuse bs1) as1))"
+ − 2594
by (metis CT0 YY flts_nonalt flts_nothing qqq1)
+ − 2595
+ − 2596
lemma WWW4:
+ − 2597
shows "map (bder c \<circ> fuse bs1) as1 = map (fuse bs1) (map (bder c) as1)"
+ − 2598
apply(induct as1)
+ − 2599
apply(auto)
+ − 2600
using bder_fuse by blast
+ − 2601
+ − 2602
lemma WWW5:
+ − 2603
shows "map (bsimp \<circ> bder c) as1 = map bsimp (map (bder c) as1)"
+ − 2604
apply(induct as1)
+ − 2605
apply(auto)
+ − 2606
done
+ − 2607
+ − 2608
lemma WWW6:
+ − 2609
shows "bsimp (bder c (bsimp_AALTs x51 (flts [bsimp a1, bsimp a2]) ) ) =
+ − 2610
bsimp(bsimp_AALTs x51 (map (bder c) (flts [bsimp a1, bsimp a2]))) "
+ − 2611
using bder_bsimp_AALTs by auto
+ − 2612
+ − 2613
lemma WWW7:
+ − 2614
shows "bsimp (bsimp_AALTs x51 (map (bder c) (flts [bsimp a1, bsimp a2]))) =
+ − 2615
bsimp(bsimp_AALTs x51 (flts (map (bder c) [bsimp a1, bsimp a2])))"
+ − 2616
sorry
+ − 2617
+ − 2618
+ − 2619
lemma stupid:
+ − 2620
assumes "a = b"
+ − 2621
shows "bsimp(a) = bsimp(b)"
+ − 2622
using assms
+ − 2623
apply(auto)
+ − 2624
done
+ − 2625
(*
+ − 2626
proving idea:
+ − 2627
bsimp_AALTs x51 (map (bder c) (flts [a1, a2])) = bsimp_AALTs x51 (map (bder c) (flts [a1]++[a2]))
+ − 2628
= bsimp_AALTs x51 (map (bder c) ((flts [a1])++(flts [a2]))) =
+ − 2629
bsimp_AALTs x51 (map (bder c) (flts [a1]))++(map (bder c) (flts [a2])) = A
+ − 2630
and then want to prove that
+ − 2631
map (bder c) (flts [a]) = flts [bder c a] under the condition
+ − 2632
that a is either a seq with the first elem being not nullable, or a character equal to c,
+ − 2633
or an AALTs, or a star
+ − 2634
Then, A = bsimp_AALTs x51 (flts [bder c a]) ++ (map (bder c) (flts [a2])) = A1
+ − 2635
Using the same condition for a2, we get
+ − 2636
A1 = bsimp_AALTs x51 (flts [bder c a1]) ++ (flts [bder c a2])
+ − 2637
=bsimp_AALTs x51 flts ([bder c a1] ++ [bder c a2])
+ − 2638
=bsimp_AALTs x51 flts ([bder c a1, bder c a2])
+ − 2639
*)
+ − 2640
lemma manipulate_flts:
+ − 2641
shows "bsimp_AALTs x51 (map (bder c) (flts [a1, a2])) =
+ − 2642
bsimp_AALTs x51 ((map (bder c) (flts [a1])) @ (map (bder c) (flts [a2])))"
+ − 2643
by (metis k0 map_append)
+ − 2644
+ − 2645
lemma go_inside_flts:
+ − 2646
assumes " (bder c a1 \<noteq> AZERO) "
+ − 2647
"\<not>(\<exists> a01 a02 x02. ( (a1 = ASEQ x02 a01 a02) \<and> bnullable(a01) ) )"
+ − 2648
shows "map (bder c) (flts [a1]) = flts [bder c a1]"
+ − 2649
using assms
+ − 2650
apply -
+ − 2651
apply(case_tac a1)
+ − 2652
apply(simp)
+ − 2653
apply(simp)
+ − 2654
apply(case_tac "x32 = c")
+ − 2655
prefer 2
+ − 2656
apply(simp)
+ − 2657
apply(simp)
+ − 2658
apply(simp)
+ − 2659
apply (simp add: WWW4)
+ − 2660
apply(simp add: bder_fuse)
+ − 2661
done
+ − 2662
+ − 2663
lemma medium010:
+ − 2664
assumes " (bder c a1 = AZERO) "
+ − 2665
shows "map (bder c) (flts [a1]) = [AZERO] \<or> map (bder c) (flts [a1]) = []"
+ − 2666
using assms
+ − 2667
apply -
+ − 2668
apply(case_tac a1)
+ − 2669
apply(simp)
+ − 2670
apply(simp)
+ − 2671
apply(simp)
+ − 2672
apply(simp)
+ − 2673
apply(simp)
+ − 2674
apply(simp)
+ − 2675
done
+ − 2676
+ − 2677
lemma medium011:
+ − 2678
assumes " (bder c a1 = AZERO) "
+ − 2679
shows "flts (map (bder c) [a1, a2]) = flts [bder c a2]"
+ − 2680
using assms
+ − 2681
apply -
+ − 2682
apply(simp)
+ − 2683
done
+ − 2684
+ − 2685
lemma medium01central:
+ − 2686
shows "bsimp(bsimp_AALTs x51 (map (bder c) (flts [a2])) ) = bsimp(bsimp_AALTs x51 (flts [bder c a2]))"
+ − 2687
sorry
+ − 2688
+ − 2689
+ − 2690
lemma plus_bsimp:
+ − 2691
assumes "bsimp( bsimp a) = bsimp (bsimp b)"
+ − 2692
shows "bsimp a = bsimp b"
+ − 2693
using assms
+ − 2694
apply -
+ − 2695
by (simp add: bsimp_idem)
+ − 2696
lemma patience_good5:
+ − 2697
assumes "bsimp r = AALTs x y"
+ − 2698
shows " \<exists> a aa list. y = a#aa#list"
+ − 2699
by (metis Nil_is_map_conv arexp.simps(13) assms bsimp_AALTs.elims flts1 good.simps(5) good1 k0a)
+ − 2700
+ − 2701
(*SAD*)
+ − 2702
(*this does not hold actually
+ − 2703
lemma bsimp_equiv0:
+ − 2704
shows "bsimp(bsimp r) = bsimp(bsimp (AALTs [] [r]))"
+ − 2705
apply(simp)
+ − 2706
apply(case_tac "bsimp r")
+ − 2707
apply(simp)
+ − 2708
apply(simp)
+ − 2709
apply(simp)
+ − 2710
apply(simp)
+ − 2711
thm good1
+ − 2712
using good1
+ − 2713
apply -
+ − 2714
apply(drule_tac x="r" in meta_spec)
+ − 2715
apply(erule disjE)
+ − 2716
+ − 2717
apply(simp only: bsimp_AALTs.simps)
+ − 2718
apply(simp only:flts.simps)
+ − 2719
apply(drule patience_good5)
+ − 2720
apply(clarify)
+ − 2721
apply(subst bsimp_AALTs_qq)
+ − 2722
apply simp
+ − 2723
prefer 2
+ − 2724
sorry*)
+ − 2725
+ − 2726
(*exercise: try multiple ways of proving this*)
+ − 2727
(*this lemma does not hold.........
+ − 2728
lemma bsimp_equiv1:
+ − 2729
shows "bsimp r = bsimp (AALTs [] [r])"
+ − 2730
using plus_bsimp
+ − 2731
apply -
+ − 2732
using bsimp_equiv0 by blast
+ − 2733
(*apply(simp)
+ − 2734
apply(case_tac "bsimp r")
+ − 2735
apply(simp)
+ − 2736
apply(simp)
+ − 2737
apply(simp)
+ − 2738
apply(simp)
+ − 2739
(*use lemma good1*)
+ − 2740
thm good1
+ − 2741
using good1
+ − 2742
apply -
+ − 2743
apply(drule_tac x="r" in meta_spec)
+ − 2744
apply(erule disjE)
+ − 2745
+ − 2746
apply(subst flts_single1)
+ − 2747
apply(simp only: bsimp_AALTs.simps)
+ − 2748
prefer 2
+ − 2749
+ − 2750
thm flts_single1
+ − 2751
+ − 2752
find_theorems "flts _ = _"*)
+ − 2753
*)
+ − 2754
lemma bsimp_equiv2:
+ − 2755
shows "bsimp (AALTs x51 [r]) = bsimp (AALT x51 AZERO r)"
+ − 2756
sorry
+ − 2757
+ − 2758
lemma medium_stupid_isabelle:
+ − 2759
assumes "rs = a # list"
+ − 2760
shows "bsimp_AALTs x51 (AZERO # rs) = AALTs x51 (AZERO#rs)"
+ − 2761
using assms
+ − 2762
apply -
+ − 2763
apply(simp)
+ − 2764
done
+ − 2765
(*
+ − 2766
lemma mediumlittle:
+ − 2767
shows "bsimp(bsimp_AALTs x51 rs) = bsimp(bsimp_AALTs x51 (AZERO # rs))"
+ − 2768
apply(case_tac rs)
+ − 2769
apply(simp)
+ − 2770
apply(case_tac list)
+ − 2771
apply(subst medium_stupid_isabelle)
+ − 2772
apply(simp)
+ − 2773
prefer 2
+ − 2774
apply simp
+ − 2775
apply(rule_tac s="a#list" and t="rs" in subst)
+ − 2776
apply(simp)
+ − 2777
apply(rule_tac t="list" and s= "[]" in subst)
+ − 2778
apply(simp)
+ − 2779
(*dunno what is the rule for x#nil = x*)
+ − 2780
apply(case_tac a)
+ − 2781
apply(simp)
+ − 2782
apply(simp)
+ − 2783
apply(simp)
+ − 2784
prefer 3
+ − 2785
apply simp
+ − 2786
apply(simp only:bsimp_AALTs.simps)
+ − 2787
+ − 2788
apply simp
+ − 2789
apply(case_tac "bsimp x42")
+ − 2790
apply(simp)
+ − 2791
apply simp
+ − 2792
apply(case_tac "bsimp x43")
+ − 2793
apply simp
+ − 2794
apply simp
+ − 2795
apply simp
+ − 2796
apply simp
+ − 2797
apply(simp only:bsimp_ASEQ.simps)
+ − 2798
using good1
+ − 2799
apply -
+ − 2800
apply(drule_tac x="x43" in meta_spec)
+ − 2801
apply(erule disjE)
+ − 2802
apply(subst bsimp_AALTs_qq)
+ − 2803
using patience_good5 apply force
+ − 2804
apply(simp only:bsimp_AALTs.simps)
+ − 2805
apply(simp only:fuse.simps)
+ − 2806
apply(simp only:flts.simps)
+ − 2807
(*OK from here you actually realize this lemma doesnt hold*)
+ − 2808
apply(simp)
+ − 2809
apply(simp)
+ − 2810
apply(rule_tac t="rs" and s="a#list" in subst)
+ − 2811
apply(simp)
+ − 2812
apply(rule_tac t="list" and s="[]" in subst)
+ − 2813
apply(simp)
+ − 2814
(*apply(simp only:bsimp_AALTs.simps)*)
+ − 2815
(*apply(simp only:fuse.simps)*)
+ − 2816
sorry
+ − 2817
*)
+ − 2818
lemma singleton_list_map:
+ − 2819
shows"map f [a] = [f a]"
+ − 2820
apply simp
+ − 2821
done
+ − 2822
lemma map_application2:
+ − 2823
shows"map f [a,b] = [f a, f b]"
+ − 2824
apply simp
+ − 2825
done
+ − 2826
(*SAD*)
+ − 2827
(* bsimp (bder c (bsimp_AALTs x51 (flts [bsimp a1, bsimp a2]))) =
+ − 2828
bsimp (AALT x51 (bder c (bsimp a1)) (bder c (bsimp a2)))*)
+ − 2829
(*This equality does not hold*)
+ − 2830
lemma medium01:
+ − 2831
assumes " (bder c a1 = AZERO) "
+ − 2832
shows "bsimp(bsimp_AALTs x51 (map (bder c) (flts [ a1, a2]))) =
+ − 2833
bsimp(bsimp_AALTs x51 (flts (map (bder c) [ a1, a2])))"
+ − 2834
apply(subst manipulate_flts)
+ − 2835
using assms
+ − 2836
apply -
+ − 2837
apply(subst medium011)
+ − 2838
apply(simp)
+ − 2839
apply(case_tac "map (bder c) (flts [a1]) = []")
+ − 2840
apply(simp)
+ − 2841
using medium01central apply blast
+ − 2842
apply(frule medium010)
+ − 2843
apply(erule disjE)
+ − 2844
prefer 2
+ − 2845
apply(simp)
+ − 2846
apply(simp)
+ − 2847
apply(case_tac a2)
+ − 2848
apply simp
+ − 2849
apply simp
+ − 2850
apply simp
+ − 2851
apply(simp only:flts.simps)
+ − 2852
(*HOW do i say here to replace ASEQ ..... back into a2*)
+ − 2853
(*how do i say here to use the definition of map function
+ − 2854
without lemma, of course*)
+ − 2855
(*how do i say here that AZERO#map (bder c) [ASEQ x41 x42 x43]'s list.len >1
+ − 2856
without a lemma, of course*)
+ − 2857
apply(subst singleton_list_map)
+ − 2858
apply(simp only: bsimp_AALTs.simps)
+ − 2859
apply(case_tac "bder c (ASEQ x41 x42 x43)")
+ − 2860
apply simp
+ − 2861
apply simp
+ − 2862
apply simp
+ − 2863
prefer 3
+ − 2864
apply simp
+ − 2865
apply(rule_tac t="bder c (ASEQ x41 x42 x43)"
+ − 2866
and s="ASEQ x41a x42a x43a" in subst)
+ − 2867
apply simp
+ − 2868
apply(simp only: flts.simps)
+ − 2869
apply(simp only: bsimp_AALTs.simps)
+ − 2870
apply(simp only: fuse.simps)
+ − 2871
apply(subst (2) bsimp_idem[symmetric])
+ − 2872
apply(subst (1) bsimp_idem[symmetric])
+ − 2873
apply(simp only:bsimp.simps)
+ − 2874
apply(subst map_application2)
+ − 2875
apply(simp only: bsimp.simps)
+ − 2876
apply(simp only:flts.simps)
+ − 2877
(*want to happily change between a2 and ASEQ x41 42 43, and eliminate now
+ − 2878
redundant conditions such as map (bder c) (flts [a1]) = [AZERO] *)
+ − 2879
apply(case_tac "bsimp x42a")
+ − 2880
apply(simp)
+ − 2881
apply(case_tac "bsimp x43a")
+ − 2882
apply(simp)
+ − 2883
apply(simp)
+ − 2884
apply(simp)
+ − 2885
apply(simp)
+ − 2886
prefer 2
+ − 2887
apply(simp)
+ − 2888
apply(rule_tac t="bsimp x43a"
+ − 2889
and s="AALTs x51a x52" in subst)
+ − 2890
apply simp
+ − 2891
apply(simp only:bsimp_ASEQ.simps)
+ − 2892
apply(simp only:fuse.simps)
+ − 2893
apply(simp only:flts.simps)
+ − 2894
+ − 2895
using medium01central mediumlittle by auto
+ − 2896
+ − 2897
+ − 2898
+ − 2899
lemma medium1:
+ − 2900
assumes " (bder c a1 \<noteq> AZERO) "
+ − 2901
"\<not>(\<exists> a01 a02 x02. ( (a1 = ASEQ x02 a01 a02) \<and> bnullable(a01) ) )"
+ − 2902
" (bder c a2 \<noteq> AZERO)"
+ − 2903
"\<not>(\<exists> a11 a12 x12. ( (a2 = ASEQ x12 a11 a12) \<and> bnullable(a11) ) )"
+ − 2904
shows "bsimp_AALTs x51 (map (bder c) (flts [ a1, a2])) =
+ − 2905
bsimp_AALTs x51 (flts (map (bder c) [ a1, a2]))"
+ − 2906
using assms
+ − 2907
apply -
+ − 2908
apply(subst manipulate_flts)
+ − 2909
apply(case_tac "a1")
+ − 2910
apply(simp)
+ − 2911
apply(simp)
+ − 2912
apply(case_tac "x32 = c")
+ − 2913
prefer 2
+ − 2914
apply(simp)
+ − 2915
prefer 2
+ − 2916
apply(case_tac "bnullable x42")
+ − 2917
apply(simp)
+ − 2918
apply(simp)
+ − 2919
+ − 2920
apply(case_tac "a2")
+ − 2921
apply(simp)
+ − 2922
apply(simp)
+ − 2923
apply(case_tac "x32 = c")
+ − 2924
prefer 2
+ − 2925
apply(simp)
+ − 2926
apply(simp)
+ − 2927
apply(case_tac "bnullable x42a")
+ − 2928
apply(simp)
+ − 2929
apply(subst go_inside_flts)
+ − 2930
apply(simp)
+ − 2931
apply(simp)
+ − 2932
apply(simp)
+ − 2933
apply(simp)
+ − 2934
apply (simp add: WWW4)
+ − 2935
apply(simp)
+ − 2936
apply (simp add: WWW4)
+ − 2937
apply (simp add: go_inside_flts)
+ − 2938
apply (metis (no_types, lifting) go_inside_flts k0 list.simps(8) list.simps(9))
+ − 2939
by (smt bder.simps(6) flts.simps(1) flts.simps(6) flts.simps(7) go_inside_flts k0 list.inject list.simps(9))
+ − 2940
+ − 2941
lemma big0:
+ − 2942
shows "bsimp (AALT x51 (AALTs bs1 as1) (AALTs bs2 as2)) =
+ − 2943
bsimp (AALTs x51 ((map (fuse bs1) as1) @ (map (fuse bs2) as2)))"
+ − 2944
by (smt WWW3 bsimp.simps(2) k0 k00 list.simps(8) list.simps(9) map_append)
+ − 2945
+ − 2946
lemma bignA:
+ − 2947
shows "bsimp (AALTs x51 (AALTs bs1 as1 # as2)) =
+ − 2948
bsimp (AALTs x51 ((map (fuse bs1) as1) @ as2))"
+ − 2949
apply(simp)
+ − 2950
apply(subst k0)
+ − 2951
apply(subst WWW3)
+ − 2952
apply(simp add: flts_append)
+ − 2953
done
+ − 2954
+ − 2955
lemma XXX2a_long_without_good:
+ − 2956
shows "bsimp (bder c (bsimp a)) = bsimp (bder c a)"
+ − 2957
apply(induct a arbitrary: c taking: "\<lambda>a. asize a" rule: measure_induct)
+ − 2958
apply(case_tac x)
+ − 2959
apply(simp)
+ − 2960
apply(simp)
+ − 2961
apply(simp)
+ − 2962
prefer 3
+ − 2963
apply(simp)
+ − 2964
(* SEQ case *)
+ − 2965
apply(simp only:)
+ − 2966
apply(subst CT1_SEQ)
+ − 2967
apply(simp only: bsimp.simps)
+ − 2968
+ − 2969
(* AALT case *)
+ − 2970
prefer 2
+ − 2971
apply(simp only:)
+ − 2972
apply(case_tac "\<exists>a1 a2. x52 = [a1, a2]")
+ − 2973
apply(clarify)
+ − 2974
apply(simp del: bsimp.simps)
+ − 2975
apply(subst (2) CT1)
+ − 2976
apply(simp del: bsimp.simps)
+ − 2977
apply(rule_tac t="bsimp (bder c a1)" and s="bsimp (bder c (bsimp a1))" in subst)
+ − 2978
apply(simp del: bsimp.simps)
+ − 2979
apply(rule_tac t="bsimp (bder c a2)" and s="bsimp (bder c (bsimp a2))" in subst)
+ − 2980
apply(simp del: bsimp.simps)
+ − 2981
apply(subst CT1a[symmetric])
+ − 2982
(* \<rightarrow> *)
+ − 2983
apply(rule_tac t="AALT x51 (bder c (bsimp a1)) (bder c (bsimp a2))"
+ − 2984
and s="bder c (AALT x51 (bsimp a1) (bsimp a2))" in subst)
+ − 2985
apply(simp)
+ − 2986
apply(subst bsimp.simps)
+ − 2987
apply(simp del: bsimp.simps bder.simps)
+ − 2988
+ − 2989
apply(subst bder_bsimp_AALTs)
+ − 2990
apply(subst bsimp.simps)
+ − 2991
apply(subst WWW2[symmetric])
+ − 2992
apply(subst bsimp_AALTs_qq)
+ − 2993
defer
+ − 2994
apply(subst bsimp.simps)
+ − 2995
+ − 2996
(* <- *)
+ − 2997
apply(subst bsimp.simps)
+ − 2998
apply(simp del: bsimp.simps)
+ − 2999
(*bsimp_AALTs x51 (map (bder c) (flts [a1, a2])) =
+ − 3000
bsimp_AALTs x51 (flts (map (bder c) [a1, a2]))*)
+ − 3001
apply(case_tac "\<exists>bs1 as1. bsimp a1 = AALTs bs1 as1")
+ − 3002
apply(case_tac "\<exists>bs2 as2. bsimp a2 = AALTs bs2 as2")
+ − 3003
apply(clarify)
+ − 3004
apply(simp only:)
+ − 3005
apply(simp del: bsimp.simps bder.simps)
+ − 3006
apply(subst bsimp_AALTs_qq)
+ − 3007
prefer 2
+ − 3008
apply(simp del: bsimp.simps)
+ − 3009
apply(subst big0)
+ − 3010
apply(simp add: WWW4)
+ − 3011
apply (m etis One_nat_def Suc_eq_plus1 Suc_lessI arexp.distinct(7) bsimp.simps(2) bsimp_AALTs.simps(1) bsimp_idem flts.simps(1) length_append length_greater_0_conv length_map not_add_less2 not_less_eq)
+ − 3012
oops
+ − 3013
+ − 3014
lemma XXX2a_long_without_good:
+ − 3015
shows "bsimp (bder c (bsimp a)) = bsimp (bder c a)"
+ − 3016
apply(induct a arbitrary: c taking: "\<lambda>a. asize a" rule: measure_induct)
+ − 3017
apply(case_tac x)
+ − 3018
apply(simp)
+ − 3019
apply(simp)
+ − 3020
apply(simp)
+ − 3021
prefer 3
+ − 3022
apply(simp)
+ − 3023
(* AALT case *)
+ − 3024
prefer 2
+ − 3025
apply(subgoal_tac "nonnested (bsimp x)")
+ − 3026
prefer 2
+ − 3027
using nn1b apply blast
+ − 3028
apply(simp only:)
+ − 3029
apply(drule_tac x="AALTs x51 (flts x52)" in spec)
+ − 3030
apply(drule mp)
+ − 3031
defer
+ − 3032
apply(drule_tac x="c" in spec)
+ − 3033
apply(simp)
+ − 3034
apply(rotate_tac 2)
+ − 3035
+ − 3036
apply(drule sym)
+ − 3037
apply(simp)
+ − 3038
+ − 3039
apply(simp only: bder.simps)
+ − 3040
apply(simp only: bsimp.simps)
+ − 3041
apply(subst bder_bsimp_AALTs)
+ − 3042
apply(case_tac x52)
+ − 3043
apply(simp)
+ − 3044
apply(simp)
+ − 3045
apply(case_tac list)
+ − 3046
apply(simp)
+ − 3047
apply(case_tac a)
+ − 3048
apply(simp)
+ − 3049
apply(simp)
+ − 3050
apply(simp)
+ − 3051
defer
+ − 3052
apply(simp)
+ − 3053
+ − 3054
+ − 3055
(* case AALTs list is not empty *)
+ − 3056
apply(simp)
+ − 3057
apply(subst k0)
+ − 3058
apply(subst (2) k0)
+ − 3059
apply(simp)
+ − 3060
apply(case_tac "bsimp a = AZERO")
+ − 3061
apply(subgoal_tac "bsimp (bder c a) = AZERO")
+ − 3062
prefer 2
+ − 3063
using less_iff_Suc_add apply auto[1]
+ − 3064
apply(simp)
+ − 3065
apply(drule_tac x="AALTs x51 list" in spec)
+ − 3066
apply(drule mp)
+ − 3067
apply(simp add: asize0)
+ − 3068
apply(drule_tac x="c" in spec)
+ − 3069
apply(simp add: bder_bsimp_AALTs)
+ − 3070
apply(case_tac "nonalt (bsimp a)")
+ − 3071
prefer 2
+ − 3072
apply(drule_tac x="bsimp (AALTs x51 (a#list))" in spec)
+ − 3073
apply(drule mp)
+ − 3074
apply(rule order_class.order.strict_trans2)
+ − 3075
apply(rule bsimp_AALTs_size3)
+ − 3076
apply(auto)[1]
+ − 3077
apply(simp)
+ − 3078
apply(subst (asm) bsimp_idem)
+ − 3079
apply(drule_tac x="c" in spec)
+ − 3080
apply(simp)
+ − 3081
find_theorems "_ < _ \<Longrightarrow> _ \<le> _ \<Longrightarrow>_ < _"
+ − 3082
apply(rule le_trans)
+ − 3083
apply(subgoal_tac "flts [bsimp a] = [bsimp a]")
+ − 3084
prefer 2
+ − 3085
using k0b apply blast
+ − 3086
apply(simp)
+ − 3087
find_theorems "asize _ < asize _"
+ − 3088
+ − 3089
using bder_bsimp_AALTs
+ − 3090
apply(case_tac list)
+ − 3091
apply(simp)
+ − 3092
sledgeha mmer [timeout=6000]
+ − 3093
+ − 3094
apply(case_tac "\<exists>r \<in> set (map bsimp x52). \<not>nonalt r")
+ − 3095
apply(drule_tac x="bsimp (AALTs x51 x52)" in spec)
+ − 3096
apply(drule mp)
+ − 3097
using bsimp_AALTs_size3 apply blast
+ − 3098
apply(drule_tac x="c" in spec)
+ − 3099
apply(subst (asm) (2) test)
+ − 3100
+ − 3101
apply(case_tac x52)
+ − 3102
apply(simp)
+ − 3103
apply(simp)
+ − 3104
apply(case_tac "bsimp a = AZERO")
+ − 3105
apply(simp)
+ − 3106
apply(subgoal_tac "bsimp (bder c a) = AZERO")
+ − 3107
prefer 2
+ − 3108
apply auto[1]
+ − 3109
apply (metis L.simps(1) L_bsimp_erase der.simps(1) der_correctness erase.simps(1) erase_bder xxx_bder2)
+ − 3110
apply(simp)
+ − 3111
apply(drule_tac x="AALTs x51 list" in spec)
+ − 3112
apply(drule mp)
+ − 3113
apply(simp add: asize0)
+ − 3114
apply(simp)
+ − 3115
apply(case_tac list)
+ − 3116
prefer 2
+ − 3117
apply(simp)
+ − 3118
apply(case_tac "bsimp aa = AZERO")
+ − 3119
apply(simp)
+ − 3120
apply(subgoal_tac "bsimp (bder c aa) = AZERO")
+ − 3121
prefer 2
+ − 3122
apply auto[1]
+ − 3123
apply (metis add.left_commute bder.simps(1) bsimp.simps(3) less_add_Suc1)
+ − 3124
apply(simp)
+ − 3125
apply(drule_tac x="AALTs x51 (a#lista)" in spec)
+ − 3126
apply(drule mp)
+ − 3127
apply(simp add: asize0)
+ − 3128
apply(simp)
+ − 3129
apply (metis flts.simps(2) k0)
+ − 3130
apply(subst k0)
+ − 3131
apply(subst (2) k0)
+ − 3132
+ − 3133
+ − 3134
using less_add_Suc1 apply fastforce
+ − 3135
apply(subst k0)
+ − 3136
+ − 3137
+ − 3138
apply(simp)
+ − 3139
apply(case_tac "bsimp a = AZERO")
+ − 3140
apply(simp)
+ − 3141
apply(subgoal_tac "bsimp (bder c a) = AZERO")
+ − 3142
prefer 2
+ − 3143
apply auto[1]
+ − 3144
apply(simp)
+ − 3145
apply(case_tac "nonalt (bsimp a)")
+ − 3146
apply(subst bsimp_AALTs1)
+ − 3147
apply(simp)
+ − 3148
using less_add_Suc1 apply fastforce
+ − 3149
+ − 3150
apply(subst bsimp_AALTs1)
+ − 3151
+ − 3152
using nn11a apply b last
+ − 3153
+ − 3154
(* SEQ case *)
+ − 3155
apply(clarify)
+ − 3156
apply(subst bsimp.simps)
+ − 3157
apply(simp del: bsimp.simps)
+ − 3158
apply(auto simp del: bsimp.simps)[1]
+ − 3159
apply(subgoal_tac "bsimp x42 \<noteq> AZERO")
+ − 3160
prefer 2
+ − 3161
using b3 apply force
+ − 3162
apply(case_tac "bsimp x43 = AZERO")
+ − 3163
apply(simp)
+ − 3164
apply (simp add: bsimp_ASEQ0)
+ − 3165
apply (metis bder.simps(1) bsimp.simps(3) bsimp_AALTs.simps(1) bsimp_fuse flts.simps(1) flts.simps(2) fuse.simps(1) less_add_Suc2)
+ − 3166
apply(case_tac "\<exists>bs. bsimp x42 = AONE bs")
+ − 3167
apply(clarify)
+ − 3168
apply(simp)
+ − 3169
apply(subst bsimp_ASEQ2)
+ − 3170
apply(subgoal_tac "bsimp (bder c x42) = AZERO")
+ − 3171
prefer 2
+ − 3172
using less_add_Suc1 apply fastforce
+ − 3173
apply(simp)
+ − 3174
apply(frule_tac x="x43" in spec)
+ − 3175
apply(drule mp)
+ − 3176
apply(simp)
+ − 3177
apply(drule_tac x="c" in spec)
+ − 3178
apply(subst bder_fuse)
+ − 3179
apply(subst bsimp_fuse[symmetric])
+ − 3180
apply(simp)
+ − 3181
apply(subgoal_tac "bmkeps x42 = bs")
+ − 3182
prefer 2
+ − 3183
apply (simp add: bmkeps_simp)
+ − 3184
apply(simp)
+ − 3185
apply(subst bsimp_fuse[symmetric])
+ − 3186
apply(case_tac "nonalt (bsimp (bder c x43))")
+ − 3187
apply(subst bsimp_AALTs1)
+ − 3188
using nn11a apply blast
+ − 3189
using fuse_append apply blast
+ − 3190
apply(subgoal_tac "\<exists>bs rs. bsimp (bder c x43) = AALTs bs rs")
+ − 3191
prefer 2
+ − 3192
using bbbbs1 apply blast
+ − 3193
apply(clarify)
+ − 3194
apply(simp)
+ − 3195
apply(case_tac rs)
+ − 3196
apply(simp)
+ − 3197
apply (metis arexp.distinct(7) good.simps(4) good1)
+ − 3198
apply(simp)
+ − 3199
apply(case_tac list)
+ − 3200
apply(simp)
+ − 3201
apply (metis arexp.distinct(7) good.simps(5) good1)
+ − 3202
apply(simp del: bsimp_AALTs.simps)
+ − 3203
apply(simp only: bsimp_AALTs.simps)
+ − 3204
apply(simp)
+ − 3205
+ − 3206
+ − 3207
+ − 3208
+ − 3209
(* HERE *)
+ − 3210
apply(case_tac "x42 = AZERO")
+ − 3211
apply(simp)
+ − 3212
apply(case_tac "bsimp x43 = AZERO")
+ − 3213
apply(simp)
+ − 3214
apply (simp add: bsimp_ASEQ0)
+ − 3215
apply(subgoal_tac "bsimp (fuse (bmkeps x42) (bder c x43)) = AZERO")
+ − 3216
apply(simp)
+ − 3217
apply (met is bder.simps(1) bsimp.simps(3) bsimp_fuse fuse.simps(1) less_add_Suc2)
+ − 3218
apply(case_tac "\<exists>bs. bsimp x42 = AONE bs")
+ − 3219
apply(clarify)
+ − 3220
apply(simp)
+ − 3221
apply(subst bsimp_ASEQ2)
+ − 3222
apply(subgoal_tac "bsimp (bder c x42) = AZERO")
+ − 3223
apply(simp)
+ − 3224
prefer 2
+ − 3225
using less_add_Suc1 apply fastforce
+ − 3226
apply(subgoal_tac "bmkeps x42 = bs")
+ − 3227
prefer 2
+ − 3228
apply (simp add: bmkeps_simp)
+ − 3229
apply(simp)
+ − 3230
apply(case_tac "nonalt (bsimp (bder c x43))")
+ − 3231
apply (metis bder_fuse bsimp_AALTs.simps(1) bsimp_AALTs.simps(2) bsimp_fuse flts.simps(1) flts.simps(2) fuse.simps(1) fuse_append k0b less_add_Suc2 nn11a)
+ − 3232
apply(subgoal_tac "nonnested (bsimp (bder c x43))")
+ − 3233
prefer 2
+ − 3234
using nn1b apply blast
+ − 3235
apply(case_tac x43)
+ − 3236
apply(simp)
+ − 3237
apply(simp)
+ − 3238
apply(simp)
+ − 3239
prefer 3
+ − 3240
apply(simp)
+ − 3241
apply (metis arexp.distinct(25) arexp.distinct(7) arexp.distinct(9) bsimp_ASEQ.simps(1) bsimp_ASEQ.simps(11) bsimp_ASEQ1 nn11a nonalt.elims(3) nonalt.simps(6))
+ − 3242
apply(simp)
+ − 3243
apply(auto)[1]
+ − 3244
apply(case_tac "(bsimp (bder c x42a)) = AZERO")
+ − 3245
apply(simp)
+ − 3246
+ − 3247
apply(simp)
+ − 3248
+ − 3249
+ − 3250
+ − 3251
apply(subgoal_tac "(\<exists>bs1 rs1. 1 < length rs1 \<and> bsimp (bder c x43) = AALTs bs1 rs1 ) \<or>
+ − 3252
(\<exists>bs1 r. bsimp (bder c x43) = fuse bs1 r)")
+ − 3253
prefer 2
+ − 3254
apply (metis fuse_empty)
+ − 3255
apply(erule disjE)
+ − 3256
prefer 2
+ − 3257
apply(clarify)
+ − 3258
apply(simp only:)
+ − 3259
apply(simp)
+ − 3260
apply(simp add: fuse_append)
+ − 3261
apply(subst bder_fuse)
+ − 3262
apply(subst bsimp_fuse[symmetric])
+ − 3263
apply(subst bder_fuse)
+ − 3264
apply(subst bsimp_fuse[symmetric])
+ − 3265
apply(subgoal_tac "bsimp (bder c (bsimp x43)) = bsimp (bder c x43)")
+ − 3266
prefer 2
+ − 3267
using less_add_Suc2 apply bl ast
+ − 3268
apply(simp only: )
+ − 3269
apply(subst bsimp_fuse[symmetric])
+ − 3270
apply(simp only: )
+ − 3271
+ − 3272
apply(simp only: fuse.simps)
+ − 3273
apply(simp)
+ − 3274
apply(case_tac rs1)
+ − 3275
apply(simp)
+ − 3276
apply (me tis arexp.distinct(7) fuse.simps(1) good.simps(4) good1 good_fuse)
+ − 3277
apply(simp)
+ − 3278
apply(case_tac list)
+ − 3279
apply(simp)
+ − 3280
apply (me tis arexp.distinct(7) fuse.simps(1) good.simps(5) good1 good_fuse)
+ − 3281
apply(simp only: bsimp_AALTs.simps map_cons.simps)
+ − 3282
apply(auto)[1]
+ − 3283
+ − 3284
+ − 3285
+ − 3286
apply(subst bsimp_fuse[symmetric])
+ − 3287
apply(subgoal_tac "bmkeps x42 = bs")
+ − 3288
prefer 2
+ − 3289
apply (simp add: bmkeps_simp)
+ − 3290
+ − 3291
+ − 3292
apply(simp)
+ − 3293
+ − 3294
using b3 apply force
+ − 3295
using bsimp_ASEQ0 test2 apply fo rce
+ − 3296
thm good_SEQ test2
+ − 3297
apply (simp add: good_SEQ test2)
+ − 3298
apply (simp add: good_SEQ test2)
+ − 3299
apply(case_tac "x42 = AZERO")
+ − 3300
apply(simp)
+ − 3301
apply(case_tac "x43 = AZERO")
+ − 3302
apply(simp)
+ − 3303
apply (simp add: bsimp_ASEQ0)
+ − 3304
apply(case_tac "\<exists>bs. x42 = AONE bs")
+ − 3305
apply(clarify)
+ − 3306
apply(simp)
+ − 3307
apply(subst bsimp_ASEQ1)
+ − 3308
apply(simp)
+ − 3309
using bsimp_ASEQ0 test2 apply fo rce
+ − 3310
apply (simp add: good_SEQ test2)
+ − 3311
apply (simp add: good_SEQ test2)
+ − 3312
apply (simp add: good_SEQ test2)
+ − 3313
(* AALTs case *)
+ − 3314
apply(simp)
+ − 3315
using test2 by fa st force
+ − 3316
+ − 3317
+ − 3318
lemma XXX4ab:
+ − 3319
shows "good (bders_simp (bsimp r) s) \<or> bders_simp (bsimp r) s = AZERO"
+ − 3320
apply(induct s arbitrary: r rule: rev_induct)
+ − 3321
apply(simp)
+ − 3322
apply (simp add: good1)
+ − 3323
apply(simp add: bders_simp_append)
+ − 3324
apply (simp add: good1)
+ − 3325
done
+ − 3326
+ − 3327
lemma XXX4:
+ − 3328
assumes "good a"
+ − 3329
shows "bders_simp a s = bsimp (bders a s)"
+ − 3330
using assms
+ − 3331
apply(induct s arbitrary: a rule: rev_induct)
+ − 3332
apply(simp)
+ − 3333
apply (simp add: test2)
+ − 3334
apply(simp add: bders_append bders_simp_append)
+ − 3335
oops
+ − 3336
+ − 3337
+ − 3338
lemma MAINMAIN:
+ − 3339
"blexer r s = blexer_simp r s"
+ − 3340
apply(induct s arbitrary: r)
+ − 3341
apply(simp add: blexer_def blexer_simp_def)
+ − 3342
apply(simp add: blexer_def blexer_simp_def del: bders.simps bders_simp.simps)
+ − 3343
apply(auto simp del: bders.simps bders_simp.simps)
+ − 3344
prefer 2
+ − 3345
apply (metis b4 bders.simps(2) bders_simp.simps(2))
+ − 3346
prefer 2
+ − 3347
apply (metis b4 bders.simps(2))
+ − 3348
apply(subst bmkeps_simp)
+ − 3349
apply(simp)
+ − 3350
apply(case_tac s)
+ − 3351
apply(simp only: bders.simps)
+ − 3352
apply(subst bders_simp.simps)
+ − 3353
apply(simp)
+ − 3354
oops
+ − 3355
+ − 3356
+ − 3357
lemma
+ − 3358
fixes n :: nat
+ − 3359
shows "(\<Sum>i \<in> {0..n}. i) = n * (n + 1) div 2"
+ − 3360
apply(induct n)
+ − 3361
apply(simp)
+ − 3362
apply(simp)
+ − 3363
done
+ − 3364
+ − 3365
+ − 3366
+ − 3367
+ − 3368
+ − 3369
end