3195 assumes "(c # s1) \<in> L r" |
3265 assumes "(c # s1) \<in> L r" |
3196 shows "bders (bder c (intern r)) s1 >> code (PX r (c # s1)) \<longleftrightarrow> |
3266 shows "bders (bder c (intern r)) s1 >> code (PX r (c # s1)) \<longleftrightarrow> |
3197 bder c (intern r) >> code (PX r (c # s1))" |
3267 bder c (intern r) >> code (PX r (c # s1))" |
3198 using PX2b PX3 assms by force |
3268 using PX2b PX3 assms by force |
3199 |
3269 |
3200 |
3270 |
3201 |
3271 lemma FC_id: |
3202 |
3272 shows "FC r [] v = retrieve r v" |
3203 |
3273 by (simp add: FC_def) |
3204 |
3274 |
3205 definition EQ where |
3275 lemma FC_char: |
3206 "EQ a1 a2 \<equiv> (\<forall>bs. a1 >> bs \<longleftrightarrow> a2 >> bs)" |
3276 shows "FC r [c] v = retrieve r (injval (erase r) c v)" |
3207 |
3277 by (simp add: FC_def) |
3208 lemma EQ1: |
3278 |
3209 assumes "EQ (intern r1) (intern r2)" |
3279 lemma FC_char2: |
3210 "bders (intern r1) s >> code (PX r1 s)" |
3280 assumes "\<Turnstile> v : der c (erase r)" |
3211 "s \<in> L r1" "s \<in> L r2" |
3281 shows "FC r [c] v = FC (bder c r) [] v" |
3212 shows "bders (intern r2) s >> code (PX r1 s)" |
3282 using assms |
3213 using assms unfolding EQ_def |
3283 by (simp add: FC_char FC_id bder_retrieve) |
3214 thm PX_bders_iff |
3284 |
3215 apply(subst (asm) PX_bders_iff) |
3285 |
3216 apply(assumption) |
3286 lemma FC_bders_iff: |
3217 apply(subgoal_tac "intern r2 >> code (PX r1 s)") |
3287 assumes "\<Turnstile> v : ders s (erase r)" |
3218 prefer 2 |
3288 shows "bders r s >> FC r s v \<longleftrightarrow> r >> FC r s v" |
3219 apply(auto) |
3289 unfolding FC_def |
|
3290 by (simp add: assms contains8_iff) |
|
3291 |
|
3292 |
|
3293 lemma FC_bder_iff: |
|
3294 assumes "\<Turnstile> v : der c (erase r)" |
|
3295 shows "bder c r >> FC r [c] v \<longleftrightarrow> r >> FC r [c] v" |
|
3296 apply(subst FC_bders_iff[symmetric]) |
|
3297 apply(simp add: assms) |
|
3298 apply(simp) |
|
3299 done |
|
3300 |
|
3301 lemma FC_bnullable0: |
|
3302 assumes "bnullable r" |
|
3303 shows "FC r [] (mkeps (erase r)) = FC (bsimp r) [] (mkeps (erase (bsimp r)))" |
|
3304 unfolding FC_def |
|
3305 by (simp add: L0 assms) |
|
3306 |
|
3307 |
|
3308 lemma FC_nullable2: |
|
3309 assumes "bnullable (bders a s)" |
|
3310 shows "FC (bsimp a) s (mkeps (erase (bders (bsimp a) s))) = |
|
3311 FC (bders (bsimp a) s) [] (mkeps (erase (bders (bsimp a) s)))" |
|
3312 unfolding FC_def |
|
3313 using L02_bders assms by auto |
|
3314 |
|
3315 lemma FC_nullable3: |
|
3316 assumes "bnullable (bders a s)" |
|
3317 shows "FC a s (mkeps (erase (bders a s))) = |
|
3318 FC (bders a s) [] (mkeps (erase (bders a s)))" |
|
3319 unfolding FC_def |
|
3320 using LA assms bnullable_correctness mkeps_nullable by fastforce |
|
3321 |
|
3322 |
|
3323 lemma FE_contains0: |
|
3324 assumes "bnullable r" |
|
3325 shows "r >> FE r []" |
|
3326 by (simp add: FE_def assms bnullable_correctness contains6 mkeps_nullable) |
|
3327 |
|
3328 lemma FE_contains1: |
|
3329 assumes "bnullable (bders r s)" |
|
3330 shows "r >> FE r s" |
|
3331 by (metis FE_def Prf_flex assms bnullable_correctness contains6 erase_bders mkeps_nullable) |
|
3332 |
|
3333 lemma FE_bnullable0: |
|
3334 assumes "bnullable r" |
|
3335 shows "FE r [] = FE (bsimp r) []" |
|
3336 unfolding FE_def |
|
3337 by (simp add: L0 assms) |
|
3338 |
|
3339 |
|
3340 lemma FE_nullable1: |
|
3341 assumes "bnullable (bders r s)" |
|
3342 shows "FE r s = FE (bders r s) []" |
|
3343 unfolding FE_def |
|
3344 using LA assms bnullable_correctness mkeps_nullable by fastforce |
|
3345 |
|
3346 lemma FE_contains2: |
|
3347 assumes "bnullable (bders r s)" |
|
3348 shows "r >> FE (bders r s) []" |
|
3349 by (metis FE_contains1 FE_nullable1 assms) |
|
3350 |
|
3351 lemma FE_contains3: |
|
3352 assumes "bnullable (bder c r)" |
|
3353 shows "r >> FE (bsimp (bder c r)) []" |
|
3354 by (metis FE_def L0 assms bder_retrieve bders.simps(1) bnullable_correctness contains7a erase_bder erase_bders flex.simps(1) id_apply mkeps_nullable) |
|
3355 |
|
3356 lemma FE_contains4: |
|
3357 assumes "bnullable (bders r s)" |
|
3358 shows "r >> FE (bsimp (bders r s)) []" |
|
3359 using FE_bnullable0 FE_contains2 assms by auto |
|
3360 |
|
3361 |
|
3362 (* |
|
3363 lemma FE_bnullable2: |
|
3364 assumes "bnullable (bder c r)" |
|
3365 shows "FE r [c] = FE (bsimp r) [c]" |
|
3366 unfolding FE_def |
|
3367 apply(simp) |
|
3368 using L0 |
|
3369 |
|
3370 apply(subst FE_nullable1) |
|
3371 using assms apply(simp) |
|
3372 apply(subst FE_bnullable0) |
|
3373 using assms apply(simp) |
|
3374 unfolding FE_def |
|
3375 apply(simp) |
|
3376 apply(subst L0) |
|
3377 using assms apply(simp) |
|
3378 apply(subst bder_retrieve[symmetric]) |
|
3379 using LLLL(1) L_erase_bder_simp assms bnullable_correctness mkeps_nullable nullable_correctness apply b last |
|
3380 apply(simp) |
|
3381 find_theorems "retrieve _ (injval _ _ _)" |
|
3382 find_theorems "retrieve (bsimp _) _" |
|
3383 |
|
3384 lemma FE_nullable3: |
|
3385 assumes "bnullable (bders a s)" |
|
3386 shows "FE (bsimp a) s = FE a s" |
|
3387 |
|
3388 unfolding FE_def |
|
3389 using LA assms bnullable_correctness mkeps_nullable by fas tforce |
|
3390 *) |
|
3391 |
|
3392 |
|
3393 lemma FC4: |
|
3394 assumes "\<Turnstile> v : ders s (erase a)" |
|
3395 shows "FC a s v = FC (bders a s) [] v" |
|
3396 unfolding FC_def by (simp add: LA assms) |
|
3397 |
|
3398 lemma FC5: |
|
3399 assumes "nullable (erase a)" |
|
3400 shows "FC a [] (mkeps (erase a)) = FC (bsimp a) [] (mkeps (erase (bsimp a)))" |
|
3401 unfolding FC_def |
|
3402 using L0 assms bnullable_correctness by auto |
|
3403 |
|
3404 |
|
3405 lemma FC6: |
|
3406 assumes "nullable (erase (bders a s))" |
|
3407 shows "FC (bsimp a) s (mkeps (erase (bders (bsimp a) s))) = FC a s (mkeps (erase (bders a s)))" |
|
3408 apply(subst (2) FC4) |
|
3409 using assms mkeps_nullable apply auto[1] |
|
3410 apply(subst FC_nullable2) |
|
3411 using assms bnullable_correctness apply blast |
|
3412 oops |
|
3413 (* |
|
3414 lemma FC_bnullable: |
|
3415 assumes "bnullable (bders r s)" |
|
3416 shows "FC r s (mkeps (erase r)) = FC (bsimp r) s (mkeps (erase (bsimp r)))" |
|
3417 using assms |
|
3418 unfolding FC_def |
|
3419 using L0 L0a bder_retrieve L02_bders L04 |
|
3420 |
|
3421 apply(induct s arbitrary: r) |
|
3422 apply(simp add: FC_id) |
|
3423 apply (simp add: L0 assms) |
|
3424 apply(simp add: bders_append) |
|
3425 apply(drule_tac x="bder a r" in meta_spec) |
|
3426 apply(drule meta_mp) |
|
3427 apply(simp) |
|
3428 |
|
3429 apply(subst bder_retrieve[symmetric]) |
|
3430 apply(simp) |
|
3431 *) |
|
3432 |
|
3433 |
|
3434 lemma FC_bnullable: |
|
3435 assumes "bnullable (bders r s)" |
|
3436 shows "FC r s (mkeps (ders s (erase r))) = FC (bsimp r) s (mkeps (ders s (erase (bsimp r))))" |
|
3437 unfolding FC_def |
|
3438 oops |
|
3439 |
|
3440 lemma AA0: |
|
3441 assumes "bnullable (bders r s)" |
|
3442 assumes "bders r s >> FC r s (mkeps (erase (bders r s)))" |
|
3443 shows "bders (bsimp r) s >> FC (bsimp r) s (mkeps (erase (bders (bsimp r) s)))" |
|
3444 using assms |
|
3445 apply(subst (asm) FC_bders_iff) |
|
3446 apply(simp) |
|
3447 using bnullable_correctness mkeps_nullable apply fastforce |
|
3448 apply(subst FC_bders_iff) |
|
3449 apply(simp) |
|
3450 apply (metis LLLL(1) bnullable_correctness ders_correctness erase_bders mkeps_nullable nullable_correctness) |
|
3451 apply(simp add: PPP1_eq) |
|
3452 unfolding FC_def |
|
3453 find_theorems "retrieve (bsimp _) _" |
|
3454 using contains7b |
|
3455 oops |
3220 |
3456 |
3221 |
3457 |
3222 lemma AA1: |
3458 lemma AA1: |
3223 assumes "[c] \<in> L r" |
3459 |
3224 assumes "bder c (intern r) >> code (PX r [c])" |
3460 assumes "\<Turnstile> v : der c (erase r)" "\<Turnstile> v : der c (erase (bsimp r))" |
3225 shows "bder c (bsimp (intern r)) >> code (PX r [c])" |
3461 assumes "bder c r >> FC r [c] v" |
3226 using assms |
3462 shows "bder c (bsimp r) >> FC (bsimp r) [c] v" |
3227 |
3463 using assms |
3228 apply(induct a arbitrary: c bs1 bs2 rs) |
3464 apply(subst (asm) FC_bder_iff) |
3229 apply(auto elim: contains.cases) |
3465 apply(rule assms) |
3230 apply(case_tac "c = x2a") |
3466 apply(subst FC_bder_iff) |
3231 apply(simp) |
3467 apply(rule assms) |
3232 apply(case_tac rs) |
3468 apply(simp add: PPP1_eq) |
3233 apply(auto) |
3469 unfolding FC_def |
3234 using contains0 apply fastforce |
3470 find_theorems "retrieve (bsimp _) _" |
3235 apply(case_tac list) |
3471 using contains7b |
3236 apply(auto) |
3472 oops |
3237 |
3473 |
3238 prefer 2 |
3474 |
3239 apply(erule contains.cases) |
|
3240 apply(auto) |
|
3241 |
|
3242 |
|
3243 |
|
3244 lemma TEST: |
|
3245 assumes "bder c a >> bs" |
|
3246 shows "bder c (bsimp a) >> bs" |
|
3247 using assms |
|
3248 apply(induct a arbitrary: c bs) |
|
3249 apply(auto elim: contains.cases) |
|
3250 prefer 2 |
|
3251 apply(erule contains.cases) |
|
3252 apply(auto) |
|
3253 |
|
3254 |
|
3255 |
|
3256 |
|
3257 |
|
3258 lemma PX_bder_simp_iff: |
3475 lemma PX_bder_simp_iff: |
3259 assumes "\<Turnstile> v: ders (s1 @ s2) r" |
3476 assumes "\<Turnstile> v: ders (s1 @ s2) r" |
3260 shows "bders (bsimp (bders (intern r) s1)) s2 >> code (PV r (s1 @ s2) v) \<longleftrightarrow> |
3477 shows "bders (bsimp (bders (intern r) s1)) s2 >> code (PV r (s1 @ s2) v) \<longleftrightarrow> |
3261 bders (intern r) s1 >> code (PV r (s1 @ s2) v)" |
3478 bders (intern r) s1 >> code (PV r (s1 @ s2) v)" |
3262 using assms |
3479 using assms |
3267 apply(drule_tac x="s1 @ [a]" in meta_spec) |
3484 apply(drule_tac x="s1 @ [a]" in meta_spec) |
3268 apply(drule_tac x="v" in meta_spec) |
3485 apply(drule_tac x="v" in meta_spec) |
3269 apply(simp) |
3486 apply(simp) |
3270 apply(simp add: bders_append) |
3487 apply(simp add: bders_append) |
3271 apply(subst (asm) PV_bder_IFF) |
3488 apply(subst (asm) PV_bder_IFF) |
3272 |
3489 oops |
3273 definition EXs where |
3490 |
3274 "EXs a s \<equiv> \<forall>v \<in> \<lbrace>= v : ders s (erase a). |
3491 lemma in1: |
|
3492 assumes "AALTs bsX rsX \<in> set rs" |
|
3493 shows "\<forall>r \<in> set rsX. fuse bsX r \<in> set (flts rs)" |
|
3494 using assms |
|
3495 apply(induct rs arbitrary: bsX rsX) |
|
3496 apply(auto) |
|
3497 by (metis append_assoc in_set_conv_decomp k0) |
|
3498 |
|
3499 lemma in2a: |
|
3500 assumes "nonnested (bsimp r)" "\<not>nonalt(bsimp r)" |
|
3501 shows "(\<exists>bsX rsX. r = AALTs bsX rsX) \<or> (\<exists>bsX rX1 rX2. r = ASEQ bsX rX1 rX2 \<and> bnullable rX1)" |
|
3502 using assms |
|
3503 apply(induct r) |
|
3504 apply(auto) |
|
3505 by (metis arexp.distinct(25) b3 bnullable.simps(2) bsimp_ASEQ.simps(1) bsimp_ASEQ0 bsimp_ASEQ1 nonalt.elims(3) nonalt.simps(2)) |
|
3506 |
|
3507 |
|
3508 lemma in2: |
|
3509 assumes "bder c r >> bs2" and |
|
3510 "AALTs bsX rsX = bsimp r" and |
|
3511 "XX \<in> set rsX" "nonnested (bsimp r)" |
|
3512 shows "bder c (fuse bsX XX) >> bs2" |
|
3513 sorry |
|
3514 |
|
3515 |
|
3516 lemma |
|
3517 assumes "bder c a >> bs" |
|
3518 shows "bder c (bsimp a) >> bs" |
|
3519 using assms |
|
3520 apply(induct a arbitrary: c bs) |
|
3521 apply(auto elim: contains.cases) |
|
3522 apply(case_tac "bnullable a1") |
|
3523 apply(simp) |
|
3524 prefer 2 |
|
3525 apply(simp) |
|
3526 apply(erule contains.cases) |
|
3527 apply(auto) |
|
3528 apply(case_tac "(bsimp a1) = AZERO") |
|
3529 apply(simp) |
|
3530 apply (metis append_Nil2 contains0 contains49 fuse.simps(1)) |
|
3531 apply(case_tac "(bsimp a2a) = AZERO") |
|
3532 apply(simp) |
|
3533 apply (metis bder.simps(1) bsimp.simps(1) bsimp_ASEQ0 contains.intros(3) contains55) |
|
3534 apply(case_tac "\<exists>bsX. (bsimp a1) = AONE bsX") |
|
3535 apply(auto)[1] |
|
3536 using b3 apply fastforce |
|
3537 apply(subst bsimp_ASEQ1) |
|
3538 apply(auto)[3] |
|
3539 apply(simp) |
|
3540 apply(subgoal_tac "\<not> bnullable (bsimp a1)") |
|
3541 prefer 2 |
|
3542 using b3 apply blast |
|
3543 apply(simp) |
|
3544 apply (simp add: contains.intros(3) contains55) |
|
3545 (* SEQ nullable case *) |
|
3546 apply(erule contains.cases) |
|
3547 apply(auto) |
|
3548 apply(erule contains.cases) |
|
3549 apply(auto) |
|
3550 apply(case_tac "(bsimp a1) = AZERO") |
|
3551 apply(simp) |
|
3552 apply (metis append_Nil2 contains0 contains49 fuse.simps(1)) |
|
3553 apply(case_tac "(bsimp a2a) = AZERO") |
|
3554 apply(simp) |
|
3555 apply (metis bder.simps(1) bsimp.simps(1) bsimp_ASEQ0 contains.intros(3) contains55) |
|
3556 apply(case_tac "\<exists>bsX. (bsimp a1) = AONE bsX") |
|
3557 apply(auto)[1] |
|
3558 using contains.simps apply blast |
|
3559 apply(subst bsimp_ASEQ1) |
|
3560 apply(auto)[3] |
|
3561 apply(simp) |
|
3562 apply(subgoal_tac "bnullable (bsimp a1)") |
|
3563 prefer 2 |
|
3564 using b3 apply blast |
|
3565 apply(simp) |
|
3566 apply (metis contains.intros(3) contains.intros(4) contains55 self_append_conv2) |
|
3567 apply(erule contains.cases) |
|
3568 apply(auto) |
|
3569 apply(case_tac "(bsimp a1) = AZERO") |
|
3570 apply(simp) |
|
3571 using b3 apply force |
|
3572 apply(case_tac "(bsimp a2) = AZERO") |
|
3573 apply(simp) |
|
3574 apply (metis bder.simps(1) bsimp_ASEQ0 bsimp_ASEQ_fuse contains0 contains49 f_cont1) |
|
3575 apply(case_tac "\<exists>bsX. (bsimp a1) = AONE bsX") |
|
3576 apply(auto)[1] |
|
3577 apply (metis append_assoc bder_fuse bmkeps.simps(1) bmkeps_simp bsimp_ASEQ2 contains0 contains49 f_cont1) |
|
3578 apply(subst bsimp_ASEQ1) |
|
3579 apply(auto)[3] |
|
3580 apply(simp) |
|
3581 apply(subgoal_tac "bnullable (bsimp a1)") |
|
3582 prefer 2 |
|
3583 using b3 apply blast |
|
3584 apply(simp) |
|
3585 apply (metis bmkeps_simp contains.intros(4) contains.intros(5) contains0 contains49 f_cont1) |
|
3586 apply(erule contains.cases) |
|
3587 apply(auto) |
|
3588 (* ALT case *) |
|
3589 apply(drule contains59) |
|
3590 apply(auto) |
|
3591 apply(subst bder_bsimp_AALTs) |
|
3592 apply(rule contains61a) |
|
3593 apply(auto) |
|
3594 apply(subgoal_tac "bsimp r \<in> set (map bsimp x2a)") |
|
3595 prefer 2 |
|
3596 apply simp |
|
3597 apply(case_tac "bsimp r = AZERO") |
|
3598 apply (metis Nil_is_append_conv bder.simps(1) bsimp_AALTs.elims bsimp_AALTs.simps(2) contains49 contains61 f_cont2 list.distinct(1) split_list_last) |
|
3599 apply(subgoal_tac "nonnested (bsimp r)") |
|
3600 prefer 2 |
|
3601 using nn1b apply blast |
|
3602 apply(case_tac "nonalt (bsimp r)") |
|
3603 apply(rule_tac x="bsimp r" in bexI) |
|
3604 apply (metis contains0 contains49 f_cont1) |
|
3605 apply (metis append_Cons flts_append in_set_conv_decomp k0 k0b) |
|
3606 (* AALTS case *) |
|
3607 apply(subgoal_tac "\<exists>rsX bsX. (bsimp r) = AALTs bsX rsX \<and> (\<forall>r \<in> set rsX. nonalt r)") |
|
3608 prefer 2 |
|
3609 apply (metis n0 nonalt.elims(3)) |
|
3610 apply(auto) |
|
3611 apply(subgoal_tac "bsimp r \<in> set (map bsimp x2a)") |
|
3612 prefer 2 |
|
3613 apply (metis imageI list.set_map) |
|
3614 apply(simp) |
|
3615 apply(simp add: image_def) |
|
3616 apply(erule bexE) |
|
3617 apply(subgoal_tac "AALTs bsX rsX \<in> set (map bsimp x2a)") |
|
3618 prefer 2 |
|
3619 apply simp |
|
3620 apply(drule in1) |
|
3621 apply(subgoal_tac "rsX \<noteq> []") |
|
3622 prefer 2 |
|
3623 apply (metis arexp.distinct(7) good.simps(4) good1) |
|
3624 apply(subgoal_tac "\<exists>XX. XX \<in> set rsX") |
|
3625 prefer 2 |
|
3626 using neq_Nil_conv apply fastforce |
|
3627 apply(erule exE) |
|
3628 apply(rule_tac x="fuse bsX XX" in bexI) |
|
3629 prefer 2 |
|
3630 apply blast |
|
3631 apply(frule f_cont1) |
|
3632 apply(auto) |
|
3633 apply(rule contains0) |
|
3634 apply(drule contains49) |
|
3635 by (simp add: in2) |
|
3636 |
|
3637 lemma CONTAINS1: |
|
3638 assumes "a >> bs" |
|
3639 shows "a >>2 bs" |
|
3640 using assms |
|
3641 apply(induct a bs) |
|
3642 apply(auto intro: contains2.intros) |
|
3643 done |
|
3644 |
|
3645 lemma CONTAINS2: |
|
3646 assumes "a >>2 bs" |
|
3647 shows "a >> bs" |
|
3648 using assms |
|
3649 apply(induct a bs) |
|
3650 apply(auto intro: contains.intros) |
|
3651 using contains55 by auto |
|
3652 |
|
3653 lemma CONTAINS2_IFF: |
|
3654 shows "a >> bs \<longleftrightarrow> a >>2 bs" |
|
3655 using CONTAINS1 CONTAINS2 by blast |
|
3656 |
|
3657 lemma |
|
3658 assumes "bders (intern r) s >>2 bs" |
|
3659 shows "bders_simp (intern r) s >>2 bs" |
|
3660 using assms |
|
3661 apply(induct s arbitrary: r bs) |
|
3662 apply(simp) |
|
3663 apply(simp) |
|
3664 oops |
|
3665 |
3275 |
3666 |
3276 lemma |
3667 lemma |
3277 assumes "s \<in> L r" |
3668 assumes "s \<in> L r" |
3278 shows "(bders_simp (intern r) s >> code (PX r s)) \<longleftrightarrow> ((intern r) >> code (PX r s))" |
3669 shows "(bders_simp (intern r) s >> code (PX r s)) \<longleftrightarrow> ((intern r) >> code (PX r s))" |
3279 using assms |
3670 using assms |
3407 apply (simp add: contains2 mkeps_nullable nullable_correctness) |
3755 apply (simp add: contains2 mkeps_nullable nullable_correctness) |
3408 apply(simp add: bders_simp_append flex_append) |
3756 apply(simp add: bders_simp_append flex_append) |
3409 apply(simp add: PPP1_eq) |
3757 apply(simp add: PPP1_eq) |
3410 apply(rule Etrans) |
3758 apply(rule Etrans) |
3411 apply(rule_tac v="flex r id xs (mkeps (ders (xs @ [x]) r))" in contains7) |
3759 apply(rule_tac v="flex r id xs (mkeps (ders (xs @ [x]) r))" in contains7) |
3412 |
3760 oops |
3413 |
3761 |
3414 |
3762 |
3415 thm L07XX PPP0b erase_intern |
3763 thm L07XX PPP0b erase_intern |
3416 |
3764 |
3417 find_theorems "retrieve (bders _ _) _" |
3765 find_theorems "retrieve (bders _ _) _" |
3418 find_theorems "_ >> retrieve _ _" |
3766 find_theorems "_ >> retrieve _ _" |
3419 find_theorems "bder _ _ >> _" |
3767 find_theorems "bder _ _ >> _" |
3420 |
3768 |
3421 |
|
3422 proof - |
|
3423 from assms have "\<Turnstile> v : erase (bder c r)" by simp |
|
3424 then have "bder c r >> retrieve (bder c r) v" |
|
3425 by (simp add: contains6) |
|
3426 moreover have "retrieve (bder c r) v = retrieve r (injval (erase r) c v)" |
|
3427 using assms bder_retrieve by blast |
|
3428 ultimately have "bder c r >> code (injval (erase r) c v)" |
|
3429 apply - |
|
3430 apply(subst retrieve_code_bder) |
|
3431 apply(simp add: assms) |
|
3432 oops |
|
3433 |
|
3434 find_theorems "code _ = retrieve _ _" |
|
3435 find_theorems "_ >> retrieve _ _" |
|
3436 find_theorems "bder _ _ >> _" |
|
3437 |
|
3438 lemma |
|
3439 assumes "s \<in> r \<rightarrow> v" "s = [c1, c2]" |
|
3440 shows "bders_simp (intern r) s >> bs \<longleftrightarrow> bders (intern r) s >> bs" |
|
3441 using assms |
|
3442 apply(simp add: PPP1_eq) |
|
3443 |
|
3444 |
|
3445 |
|
3446 lemma PPP10: |
|
3447 assumes "s \<in> r \<rightarrow> v" |
|
3448 shows "bders_simp (intern r) s >> retrieve (intern r) v \<longleftrightarrow> bders (intern r) s >> retrieve (intern r) v" |
|
3449 using assms |
|
3450 apply(induct s arbitrary: r v rule: rev_induct) |
|
3451 apply(auto) |
|
3452 apply(simp_all add: PPP1_eq bders_append bders_simp_append) |
|
3453 |
|
3454 find_theorems "bder _ _ >> _" |
|
3455 |
|
3456 lemma |
|
3457 shows "bder |
|
3458 |
|
3459 |
|
3460 find_theorems "bsimp _ >> _" |
|
3461 |
|
3462 fun get where |
|
3463 "get (Some v) = v" |
|
3464 |
|
3465 |
|
3466 lemma decode9: |
|
3467 assumes "decode' bs (STAR r) = (v, bsX)" "bs \<noteq> []" |
|
3468 shows "\<exists>vs. v = Stars vs" |
|
3469 using assms |
|
3470 apply(induct bs\<equiv>"bs" r\<equiv>"STAR r" arbitrary: bs r v bsX rule: decode'.induct) |
|
3471 apply(auto) |
|
3472 apply(case_tac "decode' ds r") |
|
3473 apply(auto) |
|
3474 apply(case_tac "decode' b (STAR r)") |
|
3475 apply(auto) |
|
3476 apply(case_tac aa) |
|
3477 apply(auto) |
|
3478 done |
|
3479 |
|
3480 lemma decode10_Stars: |
|
3481 assumes "decode' bs (STAR r) = (Stars vs, bs1)" "\<Turnstile> Stars vs : (STAR r)" "vs \<noteq> []" |
|
3482 shows "decode' (bs @ bsX) (STAR r) = (Stars vs, bs1 @ bsX)" |
|
3483 using assms |
|
3484 apply(induct vs arbitrary: bs r bs1 bsX) |
|
3485 apply(auto elim!: Prf_elims) |
|
3486 apply(case_tac vs) |
|
3487 apply(auto) |
|
3488 apply(case_tac bs) |
|
3489 apply(auto) |
|
3490 apply(case_tac aa) |
|
3491 apply(auto) |
|
3492 apply(case_tac "decode' list r") |
|
3493 apply(auto) |
|
3494 apply(case_tac "decode' b (STAR r)") |
|
3495 apply(auto) |
|
3496 apply(case_tac "decode' (list @ bsX) r") |
|
3497 apply(auto) |
|
3498 apply(case_tac "decode' ba (STAR r)") |
|
3499 apply(auto) |
|
3500 apply(case_tac ba) |
|
3501 apply(auto) |
|
3502 oops |
|
3503 |
|
3504 lemma decode10: |
|
3505 assumes "decode' bs r = (v, bs1)" "\<Turnstile> v : r" |
|
3506 shows "decode' (bs @ bsX) r = (v, bs1 @ bsX)" |
|
3507 using assms |
|
3508 apply(induct bs r arbitrary: v bs1 bsX rule: decode'.induct) |
|
3509 apply(auto elim: Prf_elims)[7] |
|
3510 apply(case_tac "decode' ds r1") |
|
3511 apply(auto)[3] |
|
3512 apply(case_tac "decode' (ds @ bsX) r1") |
|
3513 apply(auto)[3] |
|
3514 apply(auto elim: Prf_elims)[4] |
|
3515 apply(case_tac "decode' ds r2") |
|
3516 apply(auto)[1] |
|
3517 apply(case_tac "decode' (ds @ bsX) r2") |
|
3518 apply(auto)[1] |
|
3519 apply(auto elim: Prf_elims)[2] |
|
3520 apply(case_tac "decode' ds r1") |
|
3521 apply(auto)[1] |
|
3522 apply(case_tac "decode' b r2") |
|
3523 apply(auto)[1] |
|
3524 apply(auto elim: Prf_elims)[1] |
|
3525 apply(auto elim: Prf_elims)[1] |
|
3526 apply(auto elim: Prf_elims)[1] |
|
3527 apply(erule Prf_elims) |
|
3528 (* STAR case *) |
|
3529 apply(auto) |
|
3530 apply(case_tac "decode' ds r") |
|
3531 apply(auto) |
|
3532 apply(case_tac "decode' b (STAR r)") |
|
3533 apply(auto) |
|
3534 apply(case_tac aa) |
|
3535 apply(auto) |
|
3536 apply(case_tac "decode' (b @ bsX) (STAR r)") |
|
3537 apply(auto) |
|
3538 oops |
|
3539 |
|
3540 |
|
3541 lemma contains100: |
|
3542 assumes "(intern r) >> bs" |
|
3543 shows "\<exists>v bsV. decode' bs r = (v, bsV) \<and> \<Turnstile> v : r" |
|
3544 using assms |
|
3545 apply(induct r arbitrary: bs) |
|
3546 apply(auto) |
|
3547 apply(erule contains.cases) |
|
3548 apply(auto) |
|
3549 apply(erule contains.cases) |
|
3550 apply(auto intro: Prf.intros) |
|
3551 apply(erule contains.cases) |
|
3552 apply(auto) |
|
3553 apply(drule_tac x="bs1" in meta_spec) |
|
3554 apply(drule_tac x="bs2" in meta_spec) |
|
3555 apply(auto)[1] |
|
3556 apply(rule_tac x="Seq v va" in exI) |
|
3557 apply(auto) |
|
3558 apply(case_tac "decode' (bs1 @ bs2) r1") |
|
3559 apply(auto) |
|
3560 apply(case_tac "decode' b r2") |
|
3561 apply(auto) |
|
3562 oops |
|
3563 |
|
3564 lemma contains101: |
|
3565 assumes "(intern r) >> code v" |
|
3566 shows "\<Turnstile> v : r" |
|
3567 using assms |
|
3568 apply(induct r arbitrary: v) |
|
3569 apply(auto elim: contains.cases) |
|
3570 apply(erule contains.cases) |
|
3571 apply(auto) |
|
3572 apply(case_tac v) |
|
3573 apply(auto intro: Prf.intros) |
|
3574 apply(erule contains.cases) |
|
3575 apply(auto) |
|
3576 apply(case_tac v) |
|
3577 apply(auto intro: Prf.intros) |
|
3578 |
|
3579 (* |
|
3580 using contains.simps apply blast |
|
3581 apply(erule contains.cases) |
|
3582 apply(auto) |
|
3583 using L1 Posix_ONE Prf.intros(4) apply force |
|
3584 apply(erule contains.cases) |
|
3585 apply(auto) |
|
3586 apply (metis Prf.intros(5) code.simps(2) decode_code get.simps) |
|
3587 apply(erule contains.cases) |
|
3588 apply(auto) |
|
3589 prefer 2 |
|
3590 apply(erule contains.cases) |
|
3591 apply(auto) |
|
3592 apply(frule f_cont1) |
|
3593 apply(auto) |
|
3594 apply(case_tac "decode' bs2 r1") |
|
3595 apply(auto) |
|
3596 apply(rule Prf.intros) |
|
3597 apply (metis Cons_eq_append_conv contains49 f_cont1 fst_conv list.inject self_append_conv2) |
|
3598 apply(erule contains.cases) |
|
3599 apply(auto) |
|
3600 apply(frule f_cont1) |
|
3601 apply(auto) |
|
3602 apply(case_tac "decode' bs2 r2") |
|
3603 apply(auto) |
|
3604 apply(rule Prf.intros) |
|
3605 apply (metis (full_types) append_Cons contains49 append_Nil fst_conv) |
|
3606 apply(erule contains.cases) |
|
3607 apply(auto) |
|
3608 apply(case_tac "decode' (bs1 @ bs2) r1") |
|
3609 apply(auto) |
|
3610 apply(case_tac "decode' b r2") |
|
3611 apply(auto) |
|
3612 apply(rule Prf.intros) |
|
3613 |
|
3614 apply (metis fst_conv) |
|
3615 apply(subgoal_tac "b = bs2 @ bsX") |
|
3616 apply(auto) |
|
3617 apply (metis fst_conv) |
|
3618 apply(subgoal_tac "decode' (bs1 @ bs2 @ bsX) r1 = (a, bs2 @ bsX)") |
|
3619 apply simp |
|
3620 *) |
|
3621 |
|
3622 |
|
3623 apply(case_tac ba) |
|
3624 apply(auto) |
|
3625 apply(drule meta_spec) |
|
3626 apply(drule meta_mp) |
|
3627 apply(assumption) |
|
3628 prefer 2 |
|
3629 |
|
3630 |
|
3631 apply(case_tac v) |
|
3632 apply(auto) |
|
3633 |
|
3634 |
|
3635 |
|
3636 find_theorems "bder _ _ >> _" |
|
3637 |
|
3638 lemma PPP0_isar: |
|
3639 assumes "bders r s >> code v" |
|
3640 shows "bders_simp r s >> code v" |
|
3641 using assms |
|
3642 apply(induct s arbitrary: r v) |
|
3643 apply(simp) |
|
3644 apply(auto) |
|
3645 apply(drule_tac x="bsimp (bder a r)" in meta_spec) |
|
3646 apply(drule_tac x="v" in meta_spec) |
|
3647 apply(drule_tac meta_mp) |
|
3648 |
|
3649 prefer 2 |
|
3650 apply(simp) |
|
3651 |
|
3652 using bnullable_correctness nullable_correctness apply fastforce |
|
3653 apply(simp add: bders_append) |
|
3654 |
|
3655 |
|
3656 |
|
3657 |
|
3658 |
|
3659 lemma PPP0_isar: |
|
3660 assumes "s \<in> r \<rightarrow> v" |
|
3661 shows "(bders (intern r) s) >> code v" |
|
3662 proof - |
|
3663 from assms have a1: "\<Turnstile> v : r" using Posix_Prf by simp |
|
3664 |
|
3665 from assms have "s \<in> L r" using Posix1(1) by auto |
|
3666 then have "[] \<in> L (ders s r)" by (simp add: ders_correctness Ders_def) |
|
3667 then have a2: "\<Turnstile> mkeps (ders s r) : ders s r" |
|
3668 by (simp add: mkeps_nullable nullable_correctness) |
|
3669 |
|
3670 have "retrieve (bders (intern r) s) (mkeps (ders s r)) = |
|
3671 retrieve (intern r) (flex r id s (mkeps (ders s r)))" using a2 LA by simp |
|
3672 also have "... = retrieve (intern r) v" |
|
3673 using LB assms by auto |
|
3674 also have "... = code v" using a1 by (simp add: retrieve_code) |
|
3675 finally have "retrieve (bders (intern r) s) (mkeps (ders s r)) = code v" by simp |
|
3676 moreover |
|
3677 have "\<Turnstile> mkeps (ders s r) : erase (bders (intern r) s)" using a2 by simp |
|
3678 then have "bders (intern r) s >> retrieve (bders (intern r) s) (mkeps (ders s r))" |
|
3679 by (rule contains6) |
|
3680 ultimately |
|
3681 show "(bders (intern r) s) >> code v" by simp |
|
3682 qed |
|
3683 |
|
3684 |
|
3685 |
|
3686 |
|
3687 |
|
3688 |
|
3689 |
|
3690 |
|
3691 |
|
3692 lemma A0: |
|
3693 assumes "r \<in> set (flts rs)" |
|
3694 shows "r \<in> set rs" |
|
3695 using assms |
|
3696 apply(induct rs arbitrary: r rule: flts.induct) |
|
3697 apply(auto) |
|
3698 oops |
|
3699 |
|
3700 lemma A1: |
|
3701 assumes "r \<in> set (flts (map (bder c) (flts rs)))" "\<forall>r \<in> set rs. nonnested r \<and> good r" |
|
3702 shows "r \<in> set (flts (map (bder c) rs))" |
|
3703 using assms |
|
3704 apply(induct rs arbitrary: r c rule: flts.induct) |
|
3705 apply(auto) |
|
3706 apply(subst (asm) map_bder_fuse) |
|
3707 apply(simp add: flts_append) |
|
3708 apply(auto) |
|
3709 apply(auto simp add: comp_def) |
|
3710 apply(subgoal_tac "\<forall>r \<in> set rs1. nonalt r \<and> good r") |
|
3711 prefer 2 |
|
3712 apply (metis Nil_is_append_conv good.simps(5) good.simps(6) in_set_conv_decomp neq_Nil_conv) |
|
3713 apply(case_tac rs1) |
|
3714 apply(auto) |
|
3715 apply(subst (asm) k0) |
|
3716 apply(auto) |
|
3717 |
|
3718 oops |
|
3719 |
|
3720 |
|
3721 lemma bsimp_comm2: |
|
3722 assumes "bder c a >> bs" |
|
3723 shows "bder c (bsimp a) >> bs" |
|
3724 using assms |
|
3725 apply(induct a arbitrary: bs c taking: "asize" rule: measure_induct) |
|
3726 apply(case_tac x) |
|
3727 apply(auto) |
|
3728 prefer 2 |
|
3729 apply(erule contains.cases) |
|
3730 apply(auto) |
|
3731 apply(subst bder_bsimp_AALTs) |
|
3732 apply(rule contains61a) |
|
3733 apply(rule bexI) |
|
3734 apply(rule contains0) |
|
3735 apply(assumption) |
|
3736 |
|
3737 |
|
3738 lemma bsimp_comm: |
|
3739 assumes "bder c (bsimp a) >> bs" |
|
3740 shows "bsimp (bder c a) >> bs" |
|
3741 using assms |
|
3742 apply(induct a arbitrary: bs c taking: "asize" rule: measure_induct) |
|
3743 apply(case_tac x) |
|
3744 apply(auto) |
|
3745 prefer 4 |
|
3746 apply(erule contains.cases) |
|
3747 apply(auto) |
|
3748 using contains.intros(3) contains55 apply fastforce |
|
3749 prefer 3 |
|
3750 apply(subst (asm) bder_bsimp_AALTs) |
|
3751 apply(drule contains61b) |
|
3752 apply(auto) |
|
3753 apply(rule contains61a) |
|
3754 apply(rule bexI) |
|
3755 apply(assumption) |
|
3756 apply(rule_tac t="set (flts (map (bsimp \<circ> bder c) x52))" |
|
3757 and s="set (flts (map (bder c \<circ> bsimp) x52))" in subst) |
|
3758 prefer 2 |
|
3759 find_theorems "map (_ \<circ> _) _ = _" |
|
3760 apply(simp add: comp_def) |
|
3761 |
|
3762 |
|
3763 find_theorems "bder _ (bsimp_AALTs _ _) = _" |
|
3764 apply(drule contains_SEQ1) |
|
3765 apply(auto)[1] |
|
3766 apply(rule contains.intros) |
|
3767 prefer 2 |
|
3768 apply(assumption) |
|
3769 |
|
3770 |
|
3771 apply(case_tac "bnullable x42") |
|
3772 apply(simp) |
|
3773 prefer 2 |
|
3774 apply(simp) |
|
3775 apply(case_tac "bsimp x42 = AZERO") |
|
3776 apply (me tis L_erase_bder_simp bder.simps(1) bsimp.simps(3) bsimp_ASEQ.simps(1) good.simps(1) good1a xxx_bder2) |
|
3777 apply(case_tac "bsimp x43 = AZERO") |
|
3778 apply (simp add: bsimp_ASEQ0) |
|
3779 apply(case_tac "\<exists>bs1. bsimp x42 = AONE bs1") |
|
3780 using b3 apply force |
|
3781 apply(subst bsimp_ASEQ1) |
|
3782 apply(auto)[3] |
|
3783 apply(auto)[1] |
|
3784 using b3 apply blast |
|
3785 apply(case_tac "bsimp (bder c x42) = AZERO") |
|
3786 apply(simp) |
|
3787 using contains.simps apply blast |
|
3788 apply(case_tac "\<exists>bs2. bsimp (bder c x42) = AONE bs2") |
|
3789 apply(auto)[1] |
|
3790 apply(subst (asm) bsimp_ASEQ2) |
|
3791 apply(subgoal_tac "\<exists>bsX. bs = x41 @ bs2 @ bsX") |
|
3792 apply(auto)[1] |
|
3793 apply(rule contains.intros) |
|
3794 apply (simp add: contains.intros(1)) |
|
3795 apply (metis append_assoc contains49) |
|
3796 using append_assoc f_cont1 apply blast |
|
3797 apply(subst (asm) bsimp_ASEQ1) |
|
3798 apply(auto)[3] |
|
3799 apply(erule contains.cases) |
|
3800 apply(auto) |
|
3801 using contains.intros(3) less_add_Suc1 apply blast |
|
3802 apply(case_tac "bsimp x42 = AZERO") |
|
3803 using b3 apply force |
|
3804 apply(case_tac "bsimp x43 = AZERO") |
|
3805 apply (metis LLLL(1) L_erase_bder_simp bder.simps(1) bsimp_AALTs.simps(1) bsimp_ASEQ0 bsimp_fuse flts.simps(1) flts.simps(2) fuse.simps(1) good.simps(1) good1a xxx_bder2) |
|
3806 apply(case_tac "\<exists>bs1. bsimp x42 = AONE bs1") |
|
3807 apply(auto)[1] |
|
3808 apply(subst bsimp_ASEQ2) |
|
3809 apply(drule_tac x="fuse (x41 @ bs1) x43" in spec) |
|
3810 apply(drule mp) |
|
3811 apply (simp add: asize_fuse) |
|
3812 apply(drule_tac x="bs" in spec) |
|
3813 apply(drule_tac x="c" in spec) |
|
3814 apply(drule mp) |
|
3815 prefer 2 |
|
3816 apply (simp add: bsimp_fuse) |
|
3817 apply(subst (asm) k0) |
|
3818 apply(subgoal_tac "\<exists>bsX. bs = x41 @ bsX") |
|
3819 prefer 2 |
|
3820 using f_cont2 apply blast |
|
3821 apply(clarify) |
|
3822 apply(drule contains62) |
|
3823 apply(auto)[1] |
|
3824 apply(case_tac "bsimp (bder c x42) = AZERO") |
|
3825 apply (metis append_is_Nil_conv bsimp_ASEQ.simps(1) contains61 flts.simps(1) flts.simps(2) in_set_conv_decomp list.distinct(1)) |
|
3826 apply(case_tac "\<exists>bsX. bsimp (bder c x42) = AONE bsX") |
|
3827 apply(clarify) |
|
3828 apply (simp add: L_erase_bder_simp xxx_bder2) |
|
3829 using L_erase_bder_simp xxx_bder2 apply auto[1] |
|
3830 apply(drule contains65) |
|
3831 apply(auto)[1] |
|
3832 apply (simp add: bder_fuse bmkeps_simp bsimp_fuse fuse_append) |
|
3833 apply(subst bsimp_ASEQ1) |
|
3834 apply(auto)[3] |
|
3835 apply(auto)[1] |
|
3836 apply(case_tac "bsimp (bder c x42) = AZERO") |
|
3837 apply(simp add: bsimp_ASEQ0) |
|
3838 apply(drule contains65) |
|
3839 apply(auto)[1] |
|
3840 apply (metis asize_fuse bder_fuse bmkeps_simp bsimp_fuse contains.intros(4) contains.intros(5) contains49 f_cont1 less_add_Suc2) |
|
3841 |
|
3842 apply(frule f_cont1) |
|
3843 apply(auto) |
|
3844 |
|
3845 apply(case_tac "\<exists>bsX. bsimp (bder c x42) = AONE bsX") |
|
3846 apply(auto)[1] |
|
3847 apply(subst (asm) bsimp_ASEQ2) |
|
3848 apply(auto) |
|
3849 apply(drule contains65) |
|
3850 apply(auto)[1] |
|
3851 apply(frule f_cont1) |
|
3852 apply(auto) |
|
3853 apply(rule contains.intros) |
|
3854 apply (metis (no_types, lifting) append_Nil2 append_eq_append_conv2 contains.intros(1) contains.intros(3) contains49 f_cont1 less_add_Suc1 same_append_eq) |
|
3855 apply(frule f_cont1) |
|
3856 apply(auto) |
|
3857 apply(rule contains.intros) |
|
3858 apply(drule contains49) |
|
3859 apply(subst (asm) bsimp_fuse[symmetric]) |
|
3860 apply(frule f_cont1) |
|
3861 apply(auto) |
|
3862 apply(subst (3) append_Nil[symmetric]) |
|
3863 apply(rule contains.intros) |
|
3864 apply(drule contains49) |
|
3865 |
|
3866 prefer 2 |
|
3867 |
|
3868 apply(simp) |
|
3869 find_theorems "fuse _ _ >> _" |
|
3870 |
|
3871 |
|
3872 apply(erule contains.cases) |
|
3873 apply(auto) |
|
3874 |
|
3875 |
|
3876 |
|
3877 |
|
3878 |
|
3879 |
|
3880 |
|
3881 |
|
3882 |
|
3883 thm bder_retrieve |
|
3884 find_theorems "_ >> retrieve _ _" |
|
3885 |
|
3886 lemma TEST: |
|
3887 assumes "\<Turnstile> v : ders s (erase r)" |
|
3888 shows "bders r s >> retrieve r (flex (erase r) id s v)" |
|
3889 using assms |
|
3890 apply(induct s arbitrary: v r rule: rev_induct) |
|
3891 apply(simp) |
|
3892 apply (simp add: contains6) |
|
3893 apply(simp add: bders_append ders_append) |
|
3894 apply(rule Etrans) |
|
3895 apply(rule contains7) |
|
3896 apply(simp) |
|
3897 by (metis LA bder_retrieve bders_snoc ders_snoc erase_bders) |
|
3898 |
|
3899 |
|
3900 lemma TEST1: |
|
3901 assumes "bder c r >> retrieve r (injval (erase r) c v)" |
|
3902 shows "r >> retrieve r v" |
|
3903 oops |
|
3904 |
|
3905 lemma TEST2: |
|
3906 assumes "bders (intern r) s >> retrieve (intern r) (flex r id s (mkeps (ders s r)))" "s = [c1, c2]" |
|
3907 shows "bders_simp (intern r) s >> retrieve (intern r) (flex r id s (mkeps (ders s r)))" |
|
3908 using assms |
|
3909 apply(simp) |
|
3910 |
|
3911 |
|
3912 apply(induct s arbitrary: r rule: rev_induct) |
|
3913 apply(simp) |
|
3914 apply(simp add: bders_simp_append ders_append flex_append bders_append) |
|
3915 apply(rule contains55) |
|
3916 |
|
3917 apply(drule_tac x="bsimp (bder a r)" in meta_spec) |
|
3918 thm L02_bders |
|
3919 apply(subst L02_bders) |
|
3920 find_theorems "retrieve (bsimp _) _ = _" |
|
3921 apply(drule_tac "" in Etrans) |
|
3922 |
|
3923 lemma TEST2: |
|
3924 assumes "bders r s >> retrieve r (flex (erase r) id s (mkeps (ders s (erase r))))" |
|
3925 shows "bders_simp r s >> retrieve r (flex (erase r) id s (mkeps (ders s (erase r))))" |
|
3926 using assms |
|
3927 apply(induct s arbitrary: r rule: rev_induct) |
|
3928 apply(simp) |
|
3929 apply(simp add: bders_simp_append ders_append flex_append bders_append) |
|
3930 apply(subgoal_tac "bder x (bders r xs) >> retrieve r (flex (erase r) id xs (injval (ders xs (erase r)) x (mkeps (ders xs (erase r)))))") |
|
3931 find_theorems "bders _ _ >> _" |
|
3932 apply(drule_tac x="bsimp (bder a r)" in meta_spec) |
|
3933 thm L02_bders |
|
3934 apply(subst L02_bders) |
|
3935 find_theorems "retrieve (bsimp _) _ = _" |
|
3936 apply(drule_tac "" in Etrans) |
|
3937 apply(rule contains55) |
|
3938 apply(rule Etrans) |
|
3939 apply(rule contains7) |
|
3940 apply(subgoal_tac "\<Turnstile> v : der x (erase (bders_simp r xs))") |
|
3941 apply(assumption) |
|
3942 prefer 2 |
|
3943 |
|
3944 |
|
3945 apply(simp) |
|
3946 by (m etis LA bder_retrieve bders_snoc ders_snoc erase_bders) |
|
3947 |
|
3948 |
|
3949 |
|
3950 |
|
3951 lemma PPP0A: |
|
3952 assumes "s \<in> L (r)" |
|
3953 shows "(bders (intern r) s) >> code (flex r id s (mkeps (ders s r)))" |
|
3954 using assms |
|
3955 by (metis L07XX PPP0 erase_intern) |
|
3956 |
|
3957 |
|
3958 |
|
3959 |
|
3960 lemma PPP1: |
|
3961 assumes "bder c (intern r) >> code v" "\<Turnstile> v : der c r" |
|
3962 shows "(intern r) >> code (injval r c v)" |
|
3963 using assms |
|
3964 by (simp add: Prf_injval contains2) |
|
3965 |
|
3966 |
|
3967 (* |
|
3968 lemma PPP1: |
|
3969 assumes "bder c r >> code v" "\<Turnstile> v : der c (erase r)" |
|
3970 shows "r >> code (injval (erase r) c v)" |
|
3971 using assms contains7[OF assms(2)] retrieve_code[OF assms(2)] |
|
3972 find_theorems "bder _ _ >> _" |
|
3973 by (simp add: Prf_injval contains2) |
|
3974 *) |
|
3975 |
3769 |
3976 lemma PPP3: |
3770 lemma PPP3: |
3977 assumes "\<Turnstile> v : ders s (erase a)" |
3771 assumes "\<Turnstile> v : ders s (erase a)" |
3978 shows "bders a s >> retrieve a (flex (erase a) id s v)" |
3772 shows "bders a s >> retrieve a (flex (erase a) id s v)" |
3979 using LA[OF assms] contains6 erase_bders assms by metis |
3773 using LA[OF assms] contains6 erase_bders assms by metis |
3980 |
3774 |
3981 |
3775 |
3982 find_theorems "bder _ _ >> _" |
3776 find_theorems "bder _ _ >> _" |
3983 |
3777 |
3984 lemma QQQ0: |
|
3985 assumes "bder c a >> code v" |
|
3986 shows "a >> code (injval (erase a) c v)" |
|
3987 using assms |
|
3988 apply(induct a arbitrary: c v) |
|
3989 apply(auto) |
|
3990 using contains.simps apply blast |
|
3991 using contains.simps apply blast |
|
3992 apply(case_tac "c = x2a") |
|
3993 apply(simp) |
|
3994 apply(erule contains.cases) |
|
3995 apply(auto) |
|
3996 |
|
3997 |
|
3998 lemma PPP4: |
|
3999 assumes "bders (intern a) [c1, c2] >> bs" |
|
4000 shows "bders_simp (intern a) [c1, c2] >> bs" |
|
4001 using assms |
|
4002 apply(simp) |
|
4003 apply(rule contains55) |
|
4004 |
|
4005 find_theorems "bder _ _ >> _" |
|
4006 |
|
4007 |
|
4008 apply(induct s arbitrary: a v rule: rev_induct) |
|
4009 apply(simp) |
|
4010 apply (simp add: contains6) |
|
4011 apply(simp add: bders_append bders_simp_append ders_append flex_append) |
|
4012 (*apply(rule contains55)*) |
|
4013 apply(drule Prf_injval) |
|
4014 apply(drule_tac x="a" in meta_spec) |
|
4015 apply(drule_tac x="injval (ders xs (erase a)) x v" in meta_spec) |
|
4016 apply(drule meta_mp) |
|
4017 apply(assumption) |
|
4018 |
|
4019 apply(thin_tac "\<Turnstile> injval (ders xs (erase a)) x v : ders xs (erase a)") |
|
4020 |
|
4021 apply(thin_tac "bders a xs >> retrieve a (flex (erase a) id xs (injval (ders xs (erase a)) x v))") |
|
4022 |
|
4023 apply(rule Etrans) |
|
4024 apply(rule contains7) |
|
4025 |
|
4026 lemma PPP4: |
|
4027 assumes "bders a s >> code v" "\<Turnstile> v : ders s (erase a)" |
|
4028 shows "bders_simp a s >> code v" |
|
4029 using assms |
|
4030 apply(induct s arbitrary: a v rule: rev_induct) |
|
4031 apply(simp) |
|
4032 apply(simp add: bders_append bders_simp_append ders_append) |
|
4033 apply(rule contains55) |
|
4034 find_theorems "bder _ _ >> _" |
|
4035 |
|
4036 |
|
4037 lemma PPP0: |
|
4038 assumes "s \<in> L (r)" |
|
4039 shows "(bders (intern r) s) >> code (flex r id s (mkeps (ders s r)))" |
|
4040 using assms |
|
4041 apply(induct s arbitrary: r rule: rev_induct) |
|
4042 apply(simp) |
|
4043 apply (simp add: contains2 mkeps_nullable nullable_correctness) |
|
4044 apply(simp add: bders_simp_append flex_append) |
|
4045 apply(rule contains55) |
|
4046 apply(rule Etrans) |
|
4047 apply(rule contains7) |
|
4048 defer |
|
4049 |
|
4050 find_theorems "_ >> _" |
|
4051 apply(drule_tac x="der a r" in meta_spec) |
|
4052 apply(drule meta_mp) |
|
4053 find_theorems "bder _ _ >> _" |
|
4054 apply(subgoal_tac "s \<in> L(der a r)") |
|
4055 prefer 2 |
|
4056 |
|
4057 apply (simp add: Posix_Prf contains2) |
|
4058 apply(simp add: bders_simp_append) |
|
4059 apply(rule contains55) |
|
4060 apply(frule PPP0) |
|
4061 apply(simp add: bders_append) |
|
4062 using Posix_injval contains7 |
|
4063 apply(subgoal_tac "retrieve r (injval (erase r) x v)") |
|
4064 find_theorems "bders _ _ >> _" |
|
4065 |
|
4066 |
|
4067 |
|
4068 lemma PPP1: |
|
4069 assumes "\<Turnstile> v : ders s r" |
|
4070 shows "bders (intern r) s >> code v" |
|
4071 using assms |
|
4072 apply(induct s arbitrary: r v rule: rev_induct) |
|
4073 apply(simp) |
|
4074 apply (simp add: Posix_Prf contains2) |
|
4075 apply(simp add: bders_append ders_append flex_append) |
|
4076 apply(frule Prf_injval) |
|
4077 apply(drule meta_spec) |
|
4078 apply(drule meta_spec) |
|
4079 apply(drule meta_mp) |
|
4080 apply(assumption) |
|
4081 apply(subst retrieve_code) |
|
4082 apply(assumption) |
|
4083 apply(subst (asm) retrieve_code) |
|
4084 apply(assumption) |
|
4085 |
|
4086 using contains7 contains7a contains6 retrieve_code |
|
4087 apply(rule contains7) |
|
4088 |
|
4089 find_theorems "bder _ _ >> _" |
|
4090 find_theorems "code _ = _" |
|
4091 find_theorems "\<Turnstile> _ : der _ _" |
|
4092 |
|
4093 |
|
4094 |
|
4095 find_theorems "_ >> (code _)" |
|
4096 apply(induct s arbitrary: a bs rule: rev_induct) |
|
4097 apply(simp) |
|
4098 apply(simp add: bders_simp_append bders_append) |
|
4099 apply(rule contains55) |
|
4100 find_theorems "bder _ _ >> _" |
|
4101 apply(drule_tac x="bder a aa" in meta_spec) |
|
4102 apply(drule_tac x="bs" in meta_spec) |
|
4103 apply(simp) |
|
4104 apply(rule contains55) |
|
4105 find_theorems "bsimp _ >> _" |
|
4106 |
|
4107 lemma XXX4: |
|
4108 assumes "good a" |
|
4109 shows "bders_simp a s = bsimp (bders a s)" |
|
4110 using assms |
|
4111 apply(induct s arbitrary: a rule: rev_induct) |
|
4112 apply(simp) |
|
4113 apply (simp add: test2) |
|
4114 apply(simp add: bders_append bders_simp_append) |
|
4115 oops |
|
4116 |
|
4117 |
|
4118 lemma MAINMAIN: |
|
4119 "blexer r s = blexer_simp r s" |
|
4120 apply(induct s arbitrary: r) |
|
4121 apply(simp add: blexer_def blexer_simp_def) |
|
4122 apply(simp add: blexer_def blexer_simp_def del: bders.simps bders_simp.simps) |
|
4123 apply(auto simp del: bders.simps bders_simp.simps) |
|
4124 prefer 2 |
|
4125 apply (metis b4 bders.simps(2) bders_simp.simps(2)) |
|
4126 prefer 2 |
|
4127 apply (metis b4 bders.simps(2)) |
|
4128 apply(subst bmkeps_simp) |
|
4129 apply(simp) |
|
4130 apply(case_tac s) |
|
4131 apply(simp only: bders.simps) |
|
4132 apply(subst bders_simp.simps) |
|
4133 apply(simp) |
|
4134 oops |
|
4135 |
|
4136 |
3778 |
4137 lemma |
3779 lemma |
4138 fixes n :: nat |
3780 fixes n :: nat |
4139 shows "(\<Sum>i \<in> {0..n}. i) = n * (n + 1) div 2" |
3781 shows "(\<Sum>i \<in> {0..n}. i) = n * (n + 1) div 2" |
4140 apply(induct n) |
3782 apply(induct n) |