499 also have "... = decode (retrieve (bder c (bders (intern r) s)) v) r" |
499 also have "... = decode (retrieve (bder c (bders (intern r) s)) v) r" |
500 using asm by (simp_all add: bder_retrieve ders_append) |
500 using asm by (simp_all add: bder_retrieve ders_append) |
501 finally show "Some (flex r id (s @ [c]) v) = |
501 finally show "Some (flex r id (s @ [c]) v) = |
502 decode (retrieve (bders (intern r) (s @ [c])) v) r" by (simp add: bders_append) |
502 decode (retrieve (bders (intern r) (s @ [c])) v) r" by (simp add: bders_append) |
503 qed |
503 qed |
|
504 |
|
505 corollary main_decode1_horribly_wrong: |
|
506 assumes "\<Turnstile> v : ders s r" |
|
507 shows "Some(v) = decode (retrieve (bders (intern r) s) v) r" |
|
508 using assms |
|
509 proof (induct s arbitrary: v rule: rev_induct) |
|
510 case Nil |
|
511 have "\<Turnstile> v : ders [] r" by fact |
|
512 then have "\<Turnstile> v: r" by simp |
|
513 then have "Some v = decode (retrieve (intern r) v) r" |
|
514 using decode_code retrieve_code by force |
|
515 then show "Some (v) = decode (retrieve (bders (intern r) []) v) r" |
|
516 by simp |
|
517 next |
|
518 case (snoc c s v) |
|
519 have IH: "\<And>v. \<Turnstile> v : ders s r \<Longrightarrow> |
|
520 Some ( v) = decode (retrieve (bders (intern r) s) v ) r" by fact |
|
521 have asm: "\<Turnstile> v: ders (s @ [c]) r" by fact |
|
522 then have asm2: "\<Turnstile> injval (ders s r) c v : ders s r" |
|
523 using Prf_injval ders_snoc by force |
|
524 then have injv: "Some (injval (ders s r) c v) = |
|
525 decode (retrieve (bders (intern r) s) (injval (ders s r) c v)) r" |
|
526 by (simp add: IH asm2) |
|
527 oops |
|
528 |
504 |
529 |
505 |
530 |
506 definition blex where |
531 definition blex where |
507 "blex a s \<equiv> if bnullable (bders a s) then Some (bmkeps (bders a s)) else None" |
532 "blex a s \<equiv> if bnullable (bders a s) then Some (bmkeps (bders a s)) else None" |
508 |
533 |
590 | \<open>collect erasedR2 ((SEQ r1 r2) # rs) = |
615 | \<open>collect erasedR2 ((SEQ r1 r2) # rs) = |
591 (if r2 = erasedR2 then r1 # (collect erasedR2 rs) else collect erasedR2 rs)\<close> |
616 (if r2 = erasedR2 then r1 # (collect erasedR2 rs) else collect erasedR2 rs)\<close> |
592 | \<open>collect erasedR2 (r # rs) = collect erasedR2 rs\<close> |
617 | \<open>collect erasedR2 (r # rs) = collect erasedR2 rs\<close> |
593 |
618 |
594 |
619 |
595 fun pruneRexp where |
620 fun pruneRexp :: "arexp \<Rightarrow> rexp list \<Rightarrow> arexp" |
|
621 where |
596 "pruneRexp (ASEQ bs r1 r2) allowableTerms = |
622 "pruneRexp (ASEQ bs r1 r2) allowableTerms = |
597 (let termsTruncated = (collect (erase r2) allowableTerms) in |
623 (let termsTruncated = (collect (erase r2) allowableTerms) in |
598 (let pruned = pruneRexp r1 termsTruncated in |
624 (let pruned = pruneRexp r1 termsTruncated in |
599 (bsimp_ASEQ1 bs pruned r2)))" |
625 (bsimp_ASEQ bs pruned r2)))" |
600 | \<open>pruneRexp (AALTs bs rs) allowableTerms = |
626 | \<open>pruneRexp (AALTs bs rs) allowableTerms = |
601 (let rsp = (filter (\<lambda>r. r \<noteq> AZERO) (map (\<lambda>r. pruneRexp r allowableTerms) rs) ) in bsimp_AALTs bs rsp ) |
627 (let rsp = (filter (\<lambda>r. r \<noteq> AZERO) (map (\<lambda>r. pruneRexp r allowableTerms) rs) ) in bsimp_AALTs bs rsp ) |
602 \<close> |
628 \<close> |
603 | \<open>pruneRexp r allowableTerms = (if (erase r) \<in> (set allowableTerms) then r else AZERO)\<close> |
629 | \<open>pruneRexp r allowableTerms = (if (erase r) \<in> (set allowableTerms) then r else AZERO)\<close> |
604 |
630 |
605 |
|
606 fun oneSimp :: \<open>rexp \<Rightarrow> rexp\<close> where |
631 fun oneSimp :: \<open>rexp \<Rightarrow> rexp\<close> where |
607 \<open> oneSimp (SEQ ONE r) = r \<close> |
632 \<open> oneSimp (SEQ ONE r) = r \<close> |
608 | \<open> oneSimp (SEQ r1 r2) = SEQ (oneSimp r1) r2 \<close> |
633 | \<open> oneSimp (SEQ r1 r2) = SEQ (oneSimp r1) r2 \<close> |
609 | \<open> oneSimp r = r \<close> |
634 | \<open> oneSimp r = r \<close> |
610 |
635 |
615 |
640 |
616 fun addToAcc :: "arexp \<Rightarrow> rexp list \<Rightarrow> rexp list" |
641 fun addToAcc :: "arexp \<Rightarrow> rexp list \<Rightarrow> rexp list" |
617 where |
642 where |
618 \<open>addToAcc r acc = filter (\<lambda>r1. oneSimp r1 \<notin> set acc) (breakIntoTerms (erase r)) \<close> |
643 \<open>addToAcc r acc = filter (\<lambda>r1. oneSimp r1 \<notin> set acc) (breakIntoTerms (erase r)) \<close> |
619 |
644 |
|
645 |
|
646 (*newSubRexps: terms that are new--have not existed in acc before*) |
620 fun dBStrong :: "arexp list \<Rightarrow> rexp list \<Rightarrow> arexp list" |
647 fun dBStrong :: "arexp list \<Rightarrow> rexp list \<Rightarrow> arexp list" |
621 where |
648 where |
622 "dBStrong [] acc = []" |
649 "dBStrong [] acc = []" |
623 | "dBStrong (r # rs) acc = (if (erase r) \<in> (set acc) then dBStrong rs acc |
650 | "dBStrong (r # rs) acc = (if (erase r) \<in> (set acc) then dBStrong rs acc |
624 else let newSubRexps = (addToAcc r acc) in |
651 else let newSubRexps = (addToAcc r acc) in |
625 (case (pruneRexp r newSubRexps) of |
652 (case (pruneRexp r newSubRexps) of |
626 AZERO \<Rightarrow> dBStrong rs (newSubRexps @ acc) | |
653 AZERO \<Rightarrow> dBStrong rs (map oneSimp newSubRexps @ acc) | |
627 r1 \<Rightarrow> r1 # (dBStrong rs (newSubRexps @ acc)) |
654 r1 \<Rightarrow> r1 # (dBStrong rs (map oneSimp newSubRexps @ acc)) |
628 ) |
655 ) |
629 ) |
656 ) |
630 " |
657 " |
631 |
658 |
632 |
659 |