583 "bsimp_ASEQ1 _ AZERO _ = AZERO" |
583 "bsimp_ASEQ1 _ AZERO _ = AZERO" |
584 | "bsimp_ASEQ1 bs (AONE bs1) r2 = fuse (bs @ bs1) r2" |
584 | "bsimp_ASEQ1 bs (AONE bs1) r2 = fuse (bs @ bs1) r2" |
585 | "bsimp_ASEQ1 bs r1 r2 = ASEQ bs r1 r2" |
585 | "bsimp_ASEQ1 bs r1 r2 = ASEQ bs r1 r2" |
586 |
586 |
587 |
587 |
588 fun collect where |
588 fun collect :: "rexp \<Rightarrow> rexp list \<Rightarrow> rexp list" where |
589 \<open>collect _ [] = []\<close> |
589 \<open>collect _ [] = []\<close> |
590 | \<open>collect erasedR2 ((SEQ r1 r2) # rs) = (if r2 = erasedR2 then r1 # (collect erasedR2 rs) |
590 | \<open>collect erasedR2 ((SEQ r1 r2) # rs) = |
591 else collect erasedR2 rs)\<close> |
591 (if r2 = erasedR2 then r1 # (collect erasedR2 rs) else collect erasedR2 rs)\<close> |
592 | \<open>collect erasedR2 (r # rs) = collect erasedR2 rs\<close> |
592 | \<open>collect erasedR2 (r # rs) = collect erasedR2 rs\<close> |
593 |
593 |
594 |
594 |
595 fun pruneRexp where |
595 fun pruneRexp where |
596 \<open>pruneRexp (ASEQ bs r1 r2) allowableTerms = |
596 "pruneRexp (ASEQ bs r1 r2) allowableTerms = |
597 ( let termsTruncated = (collect (erase r2) allowableTerms) in (let pruned = pruneRexp r1 termsTruncated in (bsimp_ASEQ1 bs pruned r2)) )\<close> |
597 (let termsTruncated = (collect (erase r2) allowableTerms) in |
598 | \<open>pruneRexp (AALTs bs rs) allowableTerms = (let rsp = (filter (\<lambda>r. r \<noteq> AZERO) (map (\<lambda>r. pruneRexp r allowableTerms) rs) ) in bsimp_AALTs bs rsp ) |
598 (let pruned = pruneRexp r1 termsTruncated in |
|
599 (bsimp_ASEQ1 bs pruned r2)))" |
|
600 | \<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 ) |
599 \<close> |
602 \<close> |
600 | \<open>pruneRexp r allowableTerms = (if (erase r) \<in> (set allowableTerms) then r else AZERO)\<close> |
603 | \<open>pruneRexp r allowableTerms = (if (erase r) \<in> (set allowableTerms) then r else AZERO)\<close> |
601 |
604 |
602 |
605 |
603 fun oneSimp :: \<open>rexp \<Rightarrow> rexp\<close> where |
606 fun oneSimp :: \<open>rexp \<Rightarrow> rexp\<close> where |