equal
deleted
inserted
replaced
940 apply(simp_all) |
940 apply(simp_all) |
941 done |
941 done |
942 |
942 |
943 fun pAKC_aux :: "arexp list \<Rightarrow> arexp \<Rightarrow> rexp \<Rightarrow> arexp" |
943 fun pAKC_aux :: "arexp list \<Rightarrow> arexp \<Rightarrow> rexp \<Rightarrow> arexp" |
944 where |
944 where |
945 "pAKC_aux rsa r ctx = (if (L (SEQ (erase r) ctx)) \<subseteq> (L (erase (AALTs [] rsa))) then AZERO else |
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) | |
946 case r of (ASEQ bs r1 r2) \<Rightarrow> |
947 (AALTs bs rs) \<Rightarrow> AALTs bs (map (\<lambda>r. pAKC_aux rsa r ctx) rs) | |
947 bsimp_ASEQ bs (pAKC_aux rsa r1 (SEQ (erase r1) ( ctx) )) r2 | |
|
948 (AALTs bs rs) \<Rightarrow> |
|
949 bsimp_AALTs bs (flts (map (\<lambda>r. pAKC_aux rsa r ( ctx) ) rs)) | |
948 r \<Rightarrow> r |
950 r \<Rightarrow> r |
949 )" |
951 )" |
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)" |
|
959 |
952 |
960 |
953 |
961 |
954 |
962 inductive |
955 inductive |
963 rrewrite:: "arexp \<Rightarrow> arexp \<Rightarrow> bool" ("_ \<leadsto> _" [99, 99] 99) |
956 rrewrite:: "arexp \<Rightarrow> arexp \<Rightarrow> bool" ("_ \<leadsto> _" [99, 99] 99) |
972 | "AALTs bs (rsa@ [AZERO] @ rsb) \<leadsto> AALTs bs (rsa @ rsb)" |
965 | "AALTs bs (rsa@ [AZERO] @ rsb) \<leadsto> AALTs bs (rsa @ rsb)" |
973 | "AALTs bs (rsa@ [AALTs bs1 rs1] @ rsb) \<leadsto> AALTs bs (rsa@(map (fuse bs1) rs1)@rsb)" |
966 | "AALTs bs (rsa@ [AALTs bs1 rs1] @ rsb) \<leadsto> AALTs bs (rsa@(map (fuse bs1) rs1)@rsb)" |
974 | "AALTs bs [] \<leadsto> AZERO" |
967 | "AALTs bs [] \<leadsto> AZERO" |
975 | "AALTs bs [r] \<leadsto> fuse bs r" |
968 | "AALTs bs [r] \<leadsto> fuse bs r" |
976 | "erase a1 = erase a2 \<Longrightarrow> AALTs bs (rsa@[a1]@rsb@[a2]@rsc) \<leadsto> AALTs bs (rsa@[a1]@rsb@rsc)" |
969 | "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)" |
970 | "pAKC_aux rsa a2 ONE = a2' \<Longrightarrow> AALTs bs (rsa @ [a2] @ rsb) \<leadsto> AALTs bs (rsa @ [a2'] @ rsb)" |
978 |
971 |
979 |
972 |
980 inductive |
973 inductive |
981 rrewrites:: "arexp \<Rightarrow> arexp \<Rightarrow> bool" ("_ \<leadsto>* _" [100, 100] 100) |
974 rrewrites:: "arexp \<Rightarrow> arexp \<Rightarrow> bool" ("_ \<leadsto>* _" [100, 100] 100) |
982 where |
975 where |