699 shows "bders_simp r (s1 @ s2) = bders_simp (bders_simp r s1) s2" |
699 shows "bders_simp r (s1 @ s2) = bders_simp (bders_simp r s1) s2" |
700 apply(induct s1 arbitrary: r s2) |
700 apply(induct s1 arbitrary: r s2) |
701 apply(simp_all) |
701 apply(simp_all) |
702 done |
702 done |
703 |
703 |
|
704 lemma bdersStrong_append: |
|
705 shows "bdersStrong r (s1 @ s2) = bdersStrong (bdersStrong r s1) s2" |
|
706 apply(induct s1 arbitrary: r) |
|
707 apply simp+ |
|
708 done |
|
709 |
|
710 |
704 lemma L_bsimp_ASEQ: |
711 lemma L_bsimp_ASEQ: |
705 "L (SEQ (erase r1) (erase r2)) = L (erase (bsimp_ASEQ bs r1 r2))" |
712 "L (SEQ (erase r1) (erase r2)) = L (erase (bsimp_ASEQ bs r1 r2))" |
706 apply(induct bs r1 r2 rule: bsimp_ASEQ.induct) |
713 apply(induct bs r1 r2 rule: bsimp_ASEQ.induct) |
707 apply(simp_all) |
714 apply(simp_all) |
708 by (metis erase_fuse fuse.simps(4)) |
715 by (metis erase_fuse fuse.simps(4)) |
709 |
716 |
|
717 |
|
718 |
710 lemma L_bsimp_AALTs: |
719 lemma L_bsimp_AALTs: |
711 "L (erase (AALTs bs rs)) = L (erase (bsimp_AALTs bs rs))" |
720 "L (erase (AALTs bs rs)) = L (erase (bsimp_AALTs bs rs))" |
712 apply(induct bs rs rule: bsimp_AALTs.induct) |
721 apply(induct bs rs rule: bsimp_AALTs.induct) |
713 apply(simp_all add: erase_fuse) |
722 apply(simp_all add: erase_fuse) |
714 done |
723 done |
|
724 |
715 |
725 |
716 lemma L_erase_AALTs: |
726 lemma L_erase_AALTs: |
717 shows "L (erase (AALTs bs rs)) = \<Union> (L ` erase ` (set rs))" |
727 shows "L (erase (AALTs bs rs)) = \<Union> (L ` erase ` (set rs))" |
718 apply(induct rs) |
728 apply(induct rs) |
719 apply(simp) |
729 apply(simp) |
969 |
979 |
970 fun pAKC_aux :: "arexp list \<Rightarrow> arexp \<Rightarrow> rexp \<Rightarrow> arexp" |
980 fun pAKC_aux :: "arexp list \<Rightarrow> arexp \<Rightarrow> rexp \<Rightarrow> arexp" |
971 where |
981 where |
972 "pAKC_aux rsa r ctx = (if (L (SEQ (erase r) ( ctx) )) \<subseteq> (L (erase (AALTs [] rsa))) then AZERO else |
982 "pAKC_aux rsa r ctx = (if (L (SEQ (erase r) ( ctx) )) \<subseteq> (L (erase (AALTs [] rsa))) then AZERO else |
973 case r of (ASEQ bs r1 r2) \<Rightarrow> |
983 case r of (ASEQ bs r1 r2) \<Rightarrow> |
974 bsimp_ASEQ bs (pAKC_aux rsa r1 (SEQ (erase r1) ( ctx) )) r2 | |
984 bsimp_ASEQ bs (pAKC_aux rsa r1 (SEQ (erase r2) ( ctx) )) r2 | |
975 (AALTs bs rs) \<Rightarrow> |
985 (AALTs bs rs) \<Rightarrow> |
976 bsimp_AALTs bs (flts (map (\<lambda>r. pAKC_aux rsa r ( ctx) ) rs)) | |
986 bsimp_AALTs bs (filter (\<lambda>r. r \<noteq> AZERO) (map (\<lambda>r. pAKC_aux rsa r ( ctx) ) rs) ) | |
977 r \<Rightarrow> r |
987 r \<Rightarrow> r |
978 )" |
988 )" |
979 |
989 |
980 |
990 |
981 |
|
982 inductive |
991 inductive |
983 rrewrite:: "arexp \<Rightarrow> arexp \<Rightarrow> bool" ("_ \<leadsto> _" [99, 99] 99) |
992 rrewrite:: "arexp \<Rightarrow> arexp \<Rightarrow> bool" ("_ \<leadsto> _" [99, 99] 99) |
984 where |
993 where |
985 "ASEQ bs AZERO r2 \<leadsto> AZERO" |
994 "pAKC_aux rsa a2 ONE = a2' \<Longrightarrow> AALTs bs (rsa @ [a2] @ rsb) \<leadsto> AALTs bs (rsa @ [a2'] @ rsb)" |
|
995 |
|
996 | "ASEQ bs AZERO r2 \<leadsto> AZERO" |
986 | "ASEQ bs r1 AZERO \<leadsto> AZERO" |
997 | "ASEQ bs r1 AZERO \<leadsto> AZERO" |
987 | "ASEQ bs1 (AONE bs2) r \<leadsto> fuse (bs1@bs2) r" |
998 | "ASEQ bs1 (AONE bs2) r \<leadsto> fuse (bs1@bs2) r" |
988 | "r1 \<leadsto> r2 \<Longrightarrow> ASEQ bs r1 r3 \<leadsto> ASEQ bs r2 r3" |
999 | "r1 \<leadsto> r2 \<Longrightarrow> ASEQ bs r1 r3 \<leadsto> ASEQ bs r2 r3" |
989 | "r3 \<leadsto> r4 \<Longrightarrow> ASEQ bs r1 r3 \<leadsto> ASEQ bs r1 r4" |
1000 | "r3 \<leadsto> r4 \<Longrightarrow> ASEQ bs r1 r3 \<leadsto> ASEQ bs r1 r4" |
990 | "r \<leadsto> r' \<Longrightarrow> (AALTs bs (rs1 @ [r] @ rs2)) \<leadsto> (AALTs bs (rs1 @ [r'] @ rs2))" |
1001 | "r \<leadsto> r' \<Longrightarrow> (AALTs bs (rs1 @ [r] @ rs2)) \<leadsto> (AALTs bs (rs1 @ [r'] @ rs2))" |
992 | "AALTs bs (rsa@ [AZERO] @ rsb) \<leadsto> AALTs bs (rsa @ rsb)" |
1003 | "AALTs bs (rsa@ [AZERO] @ rsb) \<leadsto> AALTs bs (rsa @ rsb)" |
993 | "AALTs bs (rsa@ [AALTs bs1 rs1] @ rsb) \<leadsto> AALTs bs (rsa@(map (fuse bs1) rs1)@rsb)" |
1004 | "AALTs bs (rsa@ [AALTs bs1 rs1] @ rsb) \<leadsto> AALTs bs (rsa@(map (fuse bs1) rs1)@rsb)" |
994 | "AALTs bs [] \<leadsto> AZERO" |
1005 | "AALTs bs [] \<leadsto> AZERO" |
995 | "AALTs bs [r] \<leadsto> fuse bs r" |
1006 | "AALTs bs [r] \<leadsto> fuse bs r" |
996 | "erase a1 = erase a2 \<Longrightarrow> AALTs bs (rsa@[a1]@rsb@[a2]@rsc) \<leadsto> AALTs bs (rsa@[a1]@rsb@rsc)" |
1007 | "erase a1 = erase a2 \<Longrightarrow> AALTs bs (rsa@[a1]@rsb@[a2]@rsc) \<leadsto> AALTs bs (rsa@[a1]@rsb@rsc)" |
997 | "pAKC_aux rsa a2 ONE = a2' \<Longrightarrow> AALTs bs (rsa @ [a2] @ rsb) \<leadsto> AALTs bs (rsa @ [a2'] @ rsb)" |
|
998 |
1008 |
999 |
1009 |
1000 inductive |
1010 inductive |
1001 rrewrites:: "arexp \<Rightarrow> arexp \<Rightarrow> bool" ("_ \<leadsto>* _" [100, 100] 100) |
1011 rrewrites:: "arexp \<Rightarrow> arexp \<Rightarrow> bool" ("_ \<leadsto>* _" [100, 100] 100) |
1002 where |
1012 where |
1038 |
1048 |
1039 |
1049 |
1040 lemma contextrewrites1: "r \<leadsto>* r' \<Longrightarrow> (AALTs bs (r#rs)) \<leadsto>* (AALTs bs (r'#rs))" |
1050 lemma contextrewrites1: "r \<leadsto>* r' \<Longrightarrow> (AALTs bs (r#rs)) \<leadsto>* (AALTs bs (r'#rs))" |
1041 apply(induct r r' rule: rrewrites.induct) |
1051 apply(induct r r' rule: rrewrites.induct) |
1042 apply simp |
1052 apply simp |
1043 by (metis append_Cons append_Nil rrewrite.intros(6) rs2) |
1053 |
|
1054 oops |
1044 |
1055 |
1045 |
1056 |
1046 lemma contextrewrites2: "r \<leadsto>* r' \<Longrightarrow> (AALTs bs (rs1@[r]@rs)) \<leadsto>* (AALTs bs (rs1@[r']@rs))" |
1057 lemma contextrewrites2: "r \<leadsto>* r' \<Longrightarrow> (AALTs bs (rs1@[r]@rs)) \<leadsto>* (AALTs bs (rs1@[r']@rs))" |
1047 apply(induct r r' rule: rrewrites.induct) |
1058 apply(induct r r' rule: rrewrites.induct) |
1048 apply simp |
1059 apply simp |
1049 using rrewrite.intros(6) by blast |
1060 using rrewrite.intros(6) |
|
1061 oops |
1050 |
1062 |
1051 |
1063 |
1052 |
1064 |
1053 lemma srewrites_alt: "rs1 s\<leadsto>* rs2 \<Longrightarrow> (AALTs bs (rs@rs1)) \<leadsto>* (AALTs bs (rs@rs2))" |
1065 lemma srewrites_alt: "rs1 s\<leadsto>* rs2 \<Longrightarrow> (AALTs bs (rs@rs1)) \<leadsto>* (AALTs bs (rs@rs2))" |
1054 |
1066 |