--- a/thys2/SizeBoundStrong.thy Tue Mar 08 00:50:40 2022 +0000
+++ b/thys2/SizeBoundStrong.thy Wed Mar 09 17:33:08 2022 +0000
@@ -942,21 +942,14 @@
fun pAKC_aux :: "arexp list \<Rightarrow> arexp \<Rightarrow> rexp \<Rightarrow> arexp"
where
-"pAKC_aux rsa r ctx = (if (L (SEQ (erase r) ctx)) \<subseteq> (L (erase (AALTs [] rsa))) then AZERO else
- case r of (ASEQ bs r1 r2) \<Rightarrow> pAKC_aux rsa r1 (SEQ (erase r1) ctx) |
- (AALTs bs rs) \<Rightarrow> AALTs bs (map (\<lambda>r. pAKC_aux rsa r ctx) rs) |
+"pAKC_aux rsa r ctx = (if (L (SEQ (erase r) ( ctx) )) \<subseteq> (L (erase (AALTs [] rsa))) then AZERO else
+ case r of (ASEQ bs r1 r2) \<Rightarrow>
+ bsimp_ASEQ bs (pAKC_aux rsa r1 (SEQ (erase r1) ( ctx) )) r2 |
+ (AALTs bs rs) \<Rightarrow>
+ bsimp_AALTs bs (flts (map (\<lambda>r. pAKC_aux rsa r ( ctx) ) rs)) |
r \<Rightarrow> r
)"
-|"pAKC_aux rsa (ASEQ bs1 a1 a2) ctx = (if (L (SEQ (SEQ (erase a1) (erase a2)) ctx)) \<subseteq>
- L (erase (AALTs [] rsa))
- then AZERO
- else (pAKC_aux rsa a1 (ASEQ bs1 a2 ctx)))"
-| "pAKC_aux rsa (AALTs bs1 rs1) ctx = ctx "
-
-fun pruneAwayKnownComponents :: "arexp list \<Rightarrow> arexp \<Rightarrow> arexp" where
-"pruneAwayKnownComponents rsa (ASEQ bs r1 r2) = (pAKC_aux rsa r1 r2)"
-
inductive
@@ -974,7 +967,7 @@
| "AALTs bs [] \<leadsto> AZERO"
| "AALTs bs [r] \<leadsto> fuse bs r"
| "erase a1 = erase a2 \<Longrightarrow> AALTs bs (rsa@[a1]@rsb@[a2]@rsc) \<leadsto> AALTs bs (rsa@[a1]@rsb@rsc)"
-| "pruneAwayKnownComponents rsa a2 = a2' \<Longrightarrow> AALTs bs (rsa @ [a2] @ rsb) \<leadsto> AALTs bs (rsa @ [a2'] @ rsb)"
+| "pAKC_aux rsa a2 ONE = a2' \<Longrightarrow> AALTs bs (rsa @ [a2] @ rsb) \<leadsto> AALTs bs (rsa @ [a2'] @ rsb)"
inductive