equal
deleted
inserted
replaced
92 |
92 |
93 fun notZero :: "arexp \<Rightarrow> bool" where |
93 fun notZero :: "arexp \<Rightarrow> bool" where |
94 "notZero AZERO = True" |
94 "notZero AZERO = True" |
95 | "notZero _ = False" |
95 | "notZero _ = False" |
96 |
96 |
|
97 fun tset :: "arexp list \<Rightarrow> rexp set" where |
|
98 "tset rs = set (concat (map turnIntoTerms (map erase rs)))" |
|
99 |
|
100 |
97 fun prune6 :: "rexp set \<Rightarrow> arexp \<Rightarrow> rexp list \<Rightarrow> arexp" where |
101 fun prune6 :: "rexp set \<Rightarrow> arexp \<Rightarrow> rexp list \<Rightarrow> arexp" where |
98 "prune6 acc a ctx = (if (ABIncludedByC a ctx acc attachCtx rs1_subseteq_rs2) then AZERO else |
102 "prune6 acc a ctx = (if (ABIncludedByC a ctx acc attachCtx rs1_subseteq_rs2) then AZERO else |
99 (case a of (ASEQ bs r1 r2) \<Rightarrow> bsimp_ASEQ bs (prune6 acc r1 (erase r2 # ctx)) r2 |
103 (case a of (ASEQ bs r1 r2) \<Rightarrow> bsimp_ASEQ bs (prune6 acc r1 (erase r2 # ctx)) r2 |
100 | AALTs bs rs0 \<Rightarrow> bsimp_AALTs bs (filter notZero (map (\<lambda>r.(prune6 acc r ctx)) rs0))) )" |
104 | AALTs bs rs0 \<Rightarrow> bsimp_AALTs bs (filter notZero (map (\<lambda>r.(prune6 acc r ctx)) rs0))) )" |
101 |
105 |
|
106 abbreviation |
|
107 "p acc r \<equiv> prune6 (set (concat (map turnIntoTerms (map erase acc)) ) ) r Nil" |
102 |
108 |
103 |
109 |
104 fun dB6 :: "arexp list \<Rightarrow> rexp set \<Rightarrow> arexp list" where |
110 fun dB6 :: "arexp list \<Rightarrow> rexp set \<Rightarrow> arexp list" where |
105 "dB6 [] acc = []" |
111 "dB6 [] acc = []" |
106 | "dB6 (a # as) acc = (if (erase a \<in> acc) then (dB6 as acc) |
112 | "dB6 (a # as) acc = (if (erase a \<in> acc) then (dB6 as acc) |
273 apply (simp add: rs_in_rstar) |
279 apply (simp add: rs_in_rstar) |
274 apply(subgoal_tac "L (erase a) \<subseteq> L (erase x)") |
280 apply(subgoal_tac "L (erase a) \<subseteq> L (erase x)") |
275 using ss6 apply presburger |
281 using ss6 apply presburger |
276 by simp |
282 by simp |
277 |
283 |
|
284 |
|
285 |
278 lemma ss6_realistic: |
286 lemma ss6_realistic: |
279 shows "(rs1 @ rs2) s\<leadsto>* (rs1 @ dB6 rs2 (set (concat (map turnIntoTerms (map erase rs1)))))" |
287 shows "(rs1 @ rs2) s\<leadsto>* (rs1 @ dB6 rs2 (tset rs1))" |
280 apply(induct rs2 arbitrary: rs1) |
288 apply(induct rs2 arbitrary: rs1) |
281 apply simp |
289 apply simp |
282 apply(rename_tac cc cc') |
290 apply(rename_tac cc' cc) |
283 |
291 apply(subgoal_tac "(cc @ a # cc') s\<leadsto>* (cc @ a # dB6 cc' (tset (cc @ [a])))") |
284 |
292 prefer 2 |
|
293 apply (metis append.assoc append.left_neutral append_Cons) |
|
294 apply(subgoal_tac "(cc @ a # dB6 cc' (tset (cc @ [a]))) s\<leadsto>* (cc @ (p cc a) # dB6 cc' (tset (cc @ [a])))") |
285 sorry |
295 sorry |
286 |
296 |
287 |
297 |
288 lemma ss6_stronger_aux: |
298 lemma ss6_stronger_aux: |
289 shows "(rs1 @ rs2) s\<leadsto>* (rs1 @ dB6 rs2 (set (map erase rs1)))" |
299 shows "(rs1 @ rs2) s\<leadsto>* (rs1 @ dB6 rs2 (set (map erase rs1)))" |