equal
deleted
inserted
replaced
619 |
619 |
620 fun dBStrong :: "arexp list \<Rightarrow> rexp list \<Rightarrow> arexp list" |
620 fun dBStrong :: "arexp list \<Rightarrow> rexp list \<Rightarrow> arexp list" |
621 where |
621 where |
622 "dBStrong [] acc = []" |
622 "dBStrong [] acc = []" |
623 | "dBStrong (r # rs) acc = (if (erase r) \<in> (set acc) then dBStrong rs acc |
623 | "dBStrong (r # rs) acc = (if (erase r) \<in> (set acc) then dBStrong rs acc |
624 else (case (pruneRexp r (addToAcc r acc)) of |
624 else let newSubRexps = (addToAcc r acc) in |
625 AZERO \<Rightarrow> dBStrong rs ((addToAcc r acc) @ acc) | |
625 (case (pruneRexp r newSubRexps) of |
626 r1 \<Rightarrow> r1 # (dBStrong rs ((addToAcc r acc) @ acc)) |
626 AZERO \<Rightarrow> dBStrong rs (newSubRexps @ acc) | |
|
627 r1 \<Rightarrow> r1 # (dBStrong rs (newSubRexps @ acc)) |
627 ) |
628 ) |
628 ) |
629 ) |
629 " |
630 " |
|
631 |
|
632 |
630 fun bsimpStrong :: "arexp \<Rightarrow> arexp " |
633 fun bsimpStrong :: "arexp \<Rightarrow> arexp " |
631 where |
634 where |
632 "bsimpStrong (ASEQ bs1 r1 r2) = bsimp_ASEQ bs1 (bsimpStrong r1) (bsimpStrong r2)" |
635 "bsimpStrong (ASEQ bs1 r1 r2) = bsimp_ASEQ bs1 (bsimpStrong r1) (bsimpStrong r2)" |
633 | "bsimpStrong (AALTs bs1 rs) = bsimp_AALTs bs1 (dBStrong (flts (map bsimpStrong rs)) []) " |
636 | "bsimpStrong (AALTs bs1 rs) = bsimp_AALTs bs1 (dBStrong (flts (map bsimpStrong rs)) []) " |
634 | "bsimpStrong r = r" |
637 | "bsimpStrong r = r" |
935 shows "bder c (fuse bs a) = fuse bs (bder c a)" |
938 shows "bder c (fuse bs a) = fuse bs (bder c a)" |
936 apply(induct a arbitrary: bs c) |
939 apply(induct a arbitrary: bs c) |
937 apply(simp_all) |
940 apply(simp_all) |
938 done |
941 done |
939 |
942 |
|
943 fun pAKC_aux :: "arexp list \<Rightarrow> arexp \<Rightarrow> rexp \<Rightarrow> arexp" |
|
944 where |
|
945 "pAKC_aux rsa r ctx = (if (L (SEQ (erase r) ctx)) \<subseteq> (L (erase (AALTs [] rsa))) then AZERO else |
|
946 case r of (ASEQ bs r1 r2) \<Rightarrow> pAKC_aux rsa r1 (SEQ (erase r1) ctx) | |
|
947 (AALTs bs rs) \<Rightarrow> AALTs bs (map (\<lambda>r. pAKC_aux rsa r ctx) rs) | |
|
948 r \<Rightarrow> r |
|
949 )" |
|
950 |
|
951 |"pAKC_aux rsa (ASEQ bs1 a1 a2) ctx = (if (L (SEQ (SEQ (erase a1) (erase a2)) ctx)) \<subseteq> |
|
952 L (erase (AALTs [] rsa)) |
|
953 then AZERO |
|
954 else (pAKC_aux rsa a1 (ASEQ bs1 a2 ctx)))" |
|
955 | "pAKC_aux rsa (AALTs bs1 rs1) ctx = ctx " |
|
956 |
|
957 fun pruneAwayKnownComponents :: "arexp list \<Rightarrow> arexp \<Rightarrow> arexp" where |
|
958 "pruneAwayKnownComponents rsa (ASEQ bs r1 r2) = (pAKC_aux rsa r1 r2)" |
940 |
959 |
941 |
960 |
942 |
961 |
943 inductive |
962 inductive |
944 rrewrite:: "arexp \<Rightarrow> arexp \<Rightarrow> bool" ("_ \<leadsto> _" [99, 99] 99) |
963 rrewrite:: "arexp \<Rightarrow> arexp \<Rightarrow> bool" ("_ \<leadsto> _" [99, 99] 99) |
953 | "AALTs bs (rsa@ [AZERO] @ rsb) \<leadsto> AALTs bs (rsa @ rsb)" |
972 | "AALTs bs (rsa@ [AZERO] @ rsb) \<leadsto> AALTs bs (rsa @ rsb)" |
954 | "AALTs bs (rsa@ [AALTs bs1 rs1] @ rsb) \<leadsto> AALTs bs (rsa@(map (fuse bs1) rs1)@rsb)" |
973 | "AALTs bs (rsa@ [AALTs bs1 rs1] @ rsb) \<leadsto> AALTs bs (rsa@(map (fuse bs1) rs1)@rsb)" |
955 | "AALTs bs [] \<leadsto> AZERO" |
974 | "AALTs bs [] \<leadsto> AZERO" |
956 | "AALTs bs [r] \<leadsto> fuse bs r" |
975 | "AALTs bs [r] \<leadsto> fuse bs r" |
957 | "erase a1 = erase a2 \<Longrightarrow> AALTs bs (rsa@[a1]@rsb@[a2]@rsc) \<leadsto> AALTs bs (rsa@[a1]@rsb@rsc)" |
976 | "erase a1 = erase a2 \<Longrightarrow> AALTs bs (rsa@[a1]@rsb@[a2]@rsc) \<leadsto> AALTs bs (rsa@[a1]@rsb@rsc)" |
|
977 | "pruneAwayKnownComponents rsa a2 = a2' \<Longrightarrow> AALTs bs (rsa @ [a2] @ rsb) \<leadsto> AALTs bs (rsa @ [a2'] @ rsb)" |
958 |
978 |
959 |
979 |
960 inductive |
980 inductive |
961 rrewrites:: "arexp \<Rightarrow> arexp \<Rightarrow> bool" ("_ \<leadsto>* _" [100, 100] 100) |
981 rrewrites:: "arexp \<Rightarrow> arexp \<Rightarrow> bool" ("_ \<leadsto>* _" [100, 100] 100) |
962 where |
982 where |