--- a/thys/BitCoded.thy Fri May 10 17:23:28 2019 +0100
+++ b/thys/BitCoded.thy Tue May 14 21:43:11 2019 +0100
@@ -106,6 +106,34 @@
| "asize (ASEQ cs r1 r2) = Suc (asize r1 + asize r2)"
| "asize (ASTAR cs r) = Suc (asize r)"
+fun
+ erase :: "arexp \<Rightarrow> rexp"
+where
+ "erase AZERO = ZERO"
+| "erase (AONE _) = ONE"
+| "erase (ACHAR _ c) = CHAR c"
+| "erase (AALTs _ []) = ZERO"
+| "erase (AALTs _ [r]) = (erase r)"
+| "erase (AALTs bs (r#rs)) = ALT (erase r) (erase (AALTs bs rs))"
+| "erase (ASEQ _ r1 r2) = SEQ (erase r1) (erase r2)"
+| "erase (ASTAR _ r) = STAR (erase r)"
+
+fun nonalt :: "arexp \<Rightarrow> bool"
+ where
+ "nonalt (AALTs bs2 rs) = False"
+| "nonalt r = True"
+
+
+fun good :: "arexp \<Rightarrow> bool" where
+ "good AZERO = False"
+| "good (AONE cs) = True"
+| "good (ACHAR cs c) = True"
+| "good (AALTs cs []) = False"
+| "good (AALTs cs (r#rs)) = (\<forall>r' \<in> set (r#rs). good r')"
+| "good (ASEQ cs r1 r2) = (good r1 \<and> good r2)"
+| "good (ASTAR cs r) = True"
+
+
fun fuse :: "bit list \<Rightarrow> arexp \<Rightarrow> arexp" where
@@ -144,17 +172,7 @@
| "retrieve (ASTAR bs r) (Stars (v#vs)) =
bs @ [Z] @ retrieve r v @ retrieve (ASTAR [] r) (Stars vs)"
-fun
- erase :: "arexp \<Rightarrow> rexp"
-where
- "erase AZERO = ZERO"
-| "erase (AONE _) = ONE"
-| "erase (ACHAR _ c) = CHAR c"
-| "erase (AALTs _ []) = ZERO"
-| "erase (AALTs _ [r]) = (erase r)"
-| "erase (AALTs bs (r#rs)) = ALT (erase r) (erase (AALTs bs rs))"
-| "erase (ASEQ _ r1 r2) = SEQ (erase r1) (erase r2)"
-| "erase (ASTAR _ r) = STAR (erase r)"
+
fun
bnullable :: "arexp \<Rightarrow> bool"
@@ -559,6 +577,10 @@
| "bsimp (AALTs bs1 rs) = bsimp_AALTs bs1 (flts (map bsimp rs))"
| "bsimp r = r"
+value "good (AALTs [] [AALTs [] [AONE []]])"
+value "bsimp (AALTs [] [AONE [], AALTs [] [AONE []]])"
+
+
fun
bders_simp :: "arexp \<Rightarrow> string \<Rightarrow> arexp"
where
@@ -570,9 +592,6 @@
decode (bmkeps (bders_simp (intern r) s)) r else None"
-
-
-
lemma asize0:
shows "0 < asize r"
apply(induct r)
@@ -611,7 +630,8 @@
apply(induct rs rule: bsimp_AALTs.induct)
apply(auto simp add: fuse_size)
done
-
+
+
lemma bsimp_size:
shows "asize (bsimp r) \<le> asize r"
apply(induct r)
@@ -624,10 +644,13 @@
apply(rule flts_size)
by (simp add: sum_list_mono)
-fun nonalt :: "arexp \<Rightarrow> bool"
- where
- "nonalt (AALTs bs2 rs) = False"
-| "nonalt r = True"
+lemma bsimp_asize0:
+ shows "(\<Sum>x\<leftarrow>rs. asize (bsimp x)) \<le> sum_list (map asize rs)"
+ apply(induct rs)
+ apply(auto)
+ by (simp add: add_mono bsimp_size)
+
+
@@ -1057,8 +1080,241 @@
apply(simp_all)
done
+lemma good_fuse:
+ shows "good (fuse bs r) = good r"
+ apply(induct r)
+ apply(auto)
+ apply (metis arexp.distinct(25) arexp.distinct(7) arexp.inject(4) good.elims(3) good.simps(4) good.simps(5))
+ by (metis good.simps(4) good.simps(5) neq_Nil_conv)
+
+lemma good0:
+ assumes "rs \<noteq> Nil"
+ shows "good (bsimp_AALTs bs rs) \<longleftrightarrow> (\<forall>r \<in> set rs. good r)"
+ using assms
+ apply(induct bs rs rule: bsimp_AALTs.induct)
+ apply(auto simp add: good_fuse)
+ done
+
+lemma good0a:
+ assumes "flts (map bsimp rs) \<noteq> Nil"
+ shows "good (bsimp (AALTs bs rs)) \<longleftrightarrow> (\<forall>r \<in> set (flts (map bsimp rs)). good r)"
+ using assms
+ apply(simp)
+ apply(rule good0)
+ apply(simp)
+ done
+
+lemma flts0:
+ assumes "r \<noteq> AZERO" "nonalt r"
+ shows "flts [r] \<noteq> []"
+ using assms
+ apply(induct r)
+ apply(simp_all)
+ done
+
+lemma flts1:
+ assumes "good r"
+ shows "flts [r] \<noteq> []"
+ using assms
+ apply(induct r)
+ apply(simp_all)
+ apply(case_tac x2a)
+ apply(simp)
+ apply(simp)
+ done
+
+lemma flts2:
+ assumes "good r"
+ shows "\<forall>r' \<in> set (flts [r]). good r'"
+ using assms
+ apply(induct r)
+ apply(simp)
+ apply(simp)
+ apply(simp)
+ prefer 2
+ apply(simp)
+ apply(auto)[1]
+ apply (metis good.simps(5) good_fuse in_set_insert insert_Nil list.exhaust)
+ prefer 2
+ apply(simp)
+ by fastforce
+
+lemma flts3a:
+ assumes "good r"
+ shows "good (AALTs bs (flts [r]))"
+ using assms
+ by (metis flts1 flts2 good.simps(5) neq_Nil_conv)
+
+
+lemma flts3:
+ assumes "\<forall>r \<in> set rs. good r \<or> r = AZERO"
+ shows "\<forall>r \<in> set (flts rs). good r"
+ using assms
+ apply(induct rs arbitrary: rule: flts.induct)
+ apply(simp_all)
+ by (metis UnE flts2 k0a set_map)
+
+lemma flts3b:
+ assumes "\<exists>r\<in>set rs. good r"
+ shows "flts rs \<noteq> []"
+ using assms
+ apply(induct rs arbitrary: rule: flts.induct)
+ apply(simp)
+ apply(simp)
+ apply(simp)
+ apply(auto)
+ done
+
+lemma flts4:
+ assumes "bsimp_AALTs bs (flts rs) = AZERO"
+ shows "\<forall>r \<in> set rs. \<not> good r"
+ using assms
+ apply(induct rs arbitrary: bs rule: flts.induct)
+ apply(auto)
+ defer
+ apply (metis (no_types, lifting) Nil_is_append_conv append_self_conv2 bsimp_AALTs.elims butlast.simps(2) butlast_append flts3b nonalt.simps(1) nonalt.simps(2))
+ apply (metis arexp.distinct(7) bsimp_AALTs.elims flts2 good.simps(1) good.simps(2) good0 k0b list.distinct(1) list.inject nonalt.simps(3))
+ apply (metis arexp.distinct(3) arexp.distinct(7) bsimp_AALTs.elims fuse.simps(3) list.distinct(1) list.inject)
+ apply (metis arexp.distinct(7) bsimp_AALTs.elims good.simps(1) good.simps(6) good_fuse list.distinct(1) list.inject)
+ apply (metis arexp.distinct(7) bsimp_AALTs.elims list.distinct(1) list.inject)
+ apply (metis arexp.distinct(7) bsimp_AALTs.simps(2) bsimp_AALTs.simps(3) flts.simps(1) flts.simps(2) flts1 good.simps(7) good_fuse neq_Nil_conv)
+ by (metis (no_types, lifting) Nil_is_append_conv append_Nil2 arexp.distinct(7) bsimp_AALTs.elims butlast.simps(2) butlast_append flts1 flts2 good.simps(1) good0 k0a)
+
+lemma flts_nil:
+ assumes "\<forall>y. asize y < Suc (sum_list (map asize rs)) \<longrightarrow>
+ good (bsimp y) \<or> bsimp y = AZERO"
+ and "\<forall>r\<in>set rs. \<not> good (bsimp r)"
+ shows "flts (map bsimp rs) = []"
+ using assms
+ apply(induct rs)
+ apply(simp)
+ apply(simp)
+ apply(subst k0)
+ apply(simp)
+ by force
+
+
+lemma good1:
+ shows "good (bsimp a) \<or> bsimp a = AZERO"
+ apply(induct a taking: asize rule: measure_induct)
+ apply(case_tac x)
+ apply(simp)
+ apply(simp)
+ apply(simp)
+ prefer 3
+ apply(simp)
+ prefer 2
+ apply(simp only:)
+ apply(case_tac "x52")
+ apply(simp)
+ apply(simp only: good0a)
+ apply(frule_tac x="a" in spec)
+ apply(drule mp)
+ apply(simp)
+ apply(erule disjE)
+ prefer 2
+ apply(simp)
+ apply(frule_tac x="AALTs x51 list" in spec)
+ apply(drule mp)
+ apply(simp add: asize0)
+ apply(auto)[1]
+ apply(frule_tac x="AALTs x51 list" in spec)
+ apply(drule mp)
+ apply(simp add: asize0)
+ apply(erule disjE)
+ apply(rule disjI1)
+ apply(simp add: good0)
+ apply(subst good0)
+ apply (metis Nil_is_append_conv flts1 k0)
+ apply(simp)
+ apply(subst k0)
+ apply(simp)
+ apply(auto)[1]
+ using flts2 apply blast
+ apply (metis good0 in_set_member member_rec(2))
+ apply(simp)
+ apply(rule disjI1)
+ apply(drule flts4)
+ apply(subst k0)
+ apply(subst good0)
+ apply (metis append_is_Nil_conv flts1 k0)
+ apply(auto)[1]
+ using flts2 apply blast
+ apply (metis add.commute add_lessD1 flts_nil list.distinct(1) list.set_cases not_less_eq)
+ (* SEQ case *)
+ apply(simp)
+ apply(case_tac "bsimp x42 = AZERO")
+ apply(simp)
+ apply(case_tac "bsimp x43 = AZERO")
+ apply(simp)
+ apply(subst (2) bsimp_ASEQ0)
+ apply(simp)
+ apply(case_tac "\<exists>bs. bsimp x42 = AONE bs")
+ apply(auto)[1]
+ apply(subst bsimp_ASEQ2)
+ using good_fuse apply force
+ apply(subst bsimp_ASEQ1)
+ apply(auto)
+ using less_add_Suc1 apply blast
+ using less_add_Suc2 by blast
+
+lemma flts_append:
+ "flts (xs1 @ xs2) = flts xs1 @ flts xs2"
+ apply(induct xs1 arbitrary: xs2 rule: rev_induct)
+ apply(auto)
+ apply(case_tac xs)
+ apply(auto)
+ apply(case_tac x)
+ apply(auto)
+ apply(case_tac x)
+ apply(auto)
+ done
+
+lemma g1:
+ assumes "good (bsimp_AALTs bs rs)"
+ shows "bsimp_AALTs bs rs = AALTs bs rs \<or> (\<exists>r. rs = [r] \<and> bsimp_AALTs bs [r] = fuse bs r)"
+using assms
+ apply(induct rs arbitrary: bs)
+ apply(simp)
+ apply(case_tac rs)
+ apply(simp only:)
+ apply(simp)
+ apply(case_tac list)
+ apply(simp)
+ by simp
+
lemma flts_idem:
- assumes "\<forall>r \<in> set rs. bsimp (bsimp r) = bsimp r"
+ assumes "\<forall>y. asize y < Suc (sum_list (map asize rs)) \<longrightarrow>
+ bsimp (bsimp y) = bsimp y"
+ shows "map bsimp (flts (map bsimp rs)) = flts (map bsimp rs)"
+ using assms
+ apply(induct rs)
+ apply(simp)
+ apply(simp)
+ apply(subst k0)
+ apply(subst (2) k0)
+ apply(simp add: flts_append)
+ using good1
+ apply -
+ apply(drule_tac x="a" in meta_spec)
+ apply(erule disjE)
+ prefer 2
+ apply(simp)
+ using flts.simps
+ apply(case_tac a)
+ apply(simp_all)
+ defer
+ apply(drule g1)
+ apply(erule disjE)
+ apply(simp)
+ defer
+ apply(auto)[1]
+
+
+
+lemma flts_idem:
+ assumes "\<forall>y. asize y < Suc (sum_list (map asize rs)) \<longrightarrow>
+ bsimp (bsimp y) = bsimp y"
shows "flts (map bsimp (flts (map bsimp rs))) = flts (map bsimp rs)"
using assms
apply(induct rs)
@@ -1066,6 +1322,31 @@
apply(simp)
apply(subst k0)
apply(subst (2) k0)
+ apply(simp add: flts_append)
+ using good1
+ apply -
+ apply(drule_tac x="a" in meta_spec)
+ apply(erule disjE)
+ prefer 2
+ apply(simp)
+ using flts.simps
+ apply(case_tac a)
+ apply(simp_all)
+ defer
+ apply(drule g1)
+ apply(erule disjE)
+ apply(simp)
+ defer
+ apply(auto)[1]
+
+ apply(subst g1)
+ apply(simp)
+ apply(simp)
+ apply (me tis (full_types) arexp.inject(4) bsimp_AALTs.simps(2) flts3a fuse_empty g1 list.distinct(1))
+
+
+
+
apply(case_tac "bsimp a = AZERO")
apply(simp)
apply(case_tac "nonalt (bsimp a)")
@@ -1093,91 +1374,6 @@
apply(simp_all)
oops
-lemma bsimp_AALTs_idem:
- (*assumes "\<forall>r \<in> set rs. bsimp (bsimp r) = bsimp r \<and> nonalt (bsimp r)" *)
- (*assumes "\<forall>r \<in> set rs. bsimp (bsimp r) = bsimp r" *)
- shows "bsimp (bsimp_AALTs bs rs) = bsimp_AALTs bs (flts (map bsimp rs))"
- apply(induct rs arbitrary: bs taking: "\<lambda>rs. sum_list (map asize rs)" rule: measure_induct)
- apply(case_tac x)
- apply(simp)
- apply(simp)
- apply(case_tac "\<exists>bs' rs'. a = AALTs bs' rs'")
- apply(clarify)
- apply(case_tac list)
- apply(simp)
- apply(simp)
-
- apply(drule_tac x="flts (rs' @ list)" in spec)
- apply(erule impE)
- prefer 2
- apply(case_tac a)
- apply(simp)
- apply(case_tac list)
- apply(simp)
- apply(simp)
- apply(case_tac list)
- apply(simp)
- apply(simp)
- apply(case_tac list)
- apply(simp)
- apply(simp)
- prefer 3
- apply(case_tac list)
- apply(simp)
- apply(simp)
- apply(case_tac list)
- apply(simp)
-
-
- apply(simp)
-
- apply(case_tac "flts (map bsimp list)")
- apply(simp)
- apply(simp)
-
-
-
- prefer 2
- apply(simp)
-
- apply(subst k0)
- apply(subst (2) k0)
-
- apply(case_tac a)
- apply(simp_all)
-
- prefer 2
- apply(simp)
- apply(case_tac r)
- apply(auto)
- apply(case_tac "bsimp x42 = AZERO")
- apply(simp)
- apply(case_tac "bsimp x43 = AZERO")
- apply(simp)
- apply(subst bsimp_ASEQ0)
- apply(subst bsimp_ASEQ0)
- apply(simp)
- apply(case_tac "\<exists>bs. bsimp x42 = AONE bs")
- apply(auto)[1]
- apply(subst bsimp_ASEQ2)
- apply(subst bsimp_ASEQ2)
- prefer 2
- apply(subst bsimp_ASEQ1)
- apply(auto)
- apply(subst bsimp_ASEQ1)
- apply(auto)
- apply(subst (asm) bsimp_ASEQ2)
- apply(subst (asm) bsimp_ASEQ2)
- using flts_fuse bsimp_fuse bsimp_fuse_AALTs bsimp_fuse_AALTs2 bsimp_AALTs.simps flts.simps
-
- apply(case_tac x43)
- apply(simp_all)
- prefer 3
- oops
-
-lemma ww:
- shows "bsimp_AALTs bs [r] = fuse bs r"
- by simp
lemma flts_0:
assumes "nonnested (AALTs bs rs)"
@@ -1194,15 +1390,17 @@
apply(rule ballI)
apply(simp)
done
+
+lemma flts_0a:
+ assumes "nonnested (AALTs bs rs)"
+ shows "AZERO \<notin> set (flts rs)"
+ using assms
+ using flts_0 by blast
-lemma q1:
+lemma qqq1:
shows "AZERO \<notin> set (flts (map bsimp rs))"
- apply(induct rs)
- apply(simp)
- apply(simp)
- apply(case_tac rs)
- apply(simp)
-
+ by (metis ex_map_conv flts3 good.simps(1) good1)
+
lemma cc:
assumes "bsimp (fuse bs' r) = (AALTs bs rs)"
shows "\<forall>r \<in> set rs. r \<noteq> AZERO"
@@ -1290,7 +1488,7 @@
apply(case_tac "\<exists>bs'. bsimp r1 = AONE bs'")
apply(auto)
apply (simp add: bsimp_ASEQ2)
- using bsimp_fuse apply fastforce
+ using bsimp_fuse apply fast force
apply (simp add: bsimp_ASEQ1)
@@ -1340,6 +1538,13 @@
apply(subst bsimp_AALTs_qq)
apply(auto)[1]
apply(simp)
+ apply(subst k0)
+ apply(simp)
+ apply(simp add: flts_append)
+ apply(subst (2) k0)
+
+ apply(simp add: flts_append)
+
prefer 2
apply(subgoal_tac "length (flts (bsimp a # map bsimp list)) = 0 \<or>
length (flts (bsimp a # map bsimp list)) = 1")
@@ -2300,17 +2505,6 @@
apply(simp)
oops
-lemma flts_append:
- "flts (xs1 @ xs2) = flts xs1 @ flts xs2"
- apply(induct xs1 arbitrary: xs2 rule: rev_induct)
- apply(auto)
- apply(case_tac xs)
- apply(auto)
- apply(case_tac x)
- apply(auto)
- apply(case_tac x)
- apply(auto)
- done
lemma flts_bsimp:
"flts (map bsimp rs) = map bsimp (flts rs)"