--- a/thys/BitCoded.thy Mon Aug 19 16:24:28 2019 +0100
+++ b/thys/BitCoded.thy Tue Aug 20 23:42:28 2019 +0200
@@ -567,6 +567,9 @@
| "flts ((AALTs bs rs1) # rs) = (map (fuse bs) rs1) @ flts rs"
| "flts (r1 # rs) = r1 # flts rs"
+
+
+
fun li :: "bit list \<Rightarrow> arexp list \<Rightarrow> arexp"
where
"li _ [] = AZERO"
@@ -574,6 +577,8 @@
| "li bs as = AALTs bs as"
+
+
fun bsimp_ASEQ :: "bit list \<Rightarrow> arexp \<Rightarrow> arexp \<Rightarrow> arexp"
where
"bsimp_ASEQ _ AZERO _ = AZERO"
@@ -1083,6 +1088,8 @@
apply(auto)
done
+
+
lemma rt:
shows "sum_list (map asize (flts (map bsimp rs))) \<le> sum_list (map asize rs)"
apply(induct rs)
@@ -1783,6 +1790,56 @@
apply(simp_all)
done
+
+fun flts2 :: "char \<Rightarrow> arexp list \<Rightarrow> arexp list"
+ where
+ "flts2 _ [] = []"
+| "flts2 c (AZERO # rs) = flts2 c rs"
+| "flts2 c (AONE _ # rs) = flts2 c rs"
+| "flts2 c (ACHAR bs d # rs) = (if c = d then (ACHAR bs d # flts2 c rs) else flts2 c rs)"
+| "flts2 c ((AALTs bs rs1) # rs) = (map (fuse bs) rs1) @ flts2 c rs"
+| "flts2 c (ASEQ bs r1 r2 # rs) = (if (bnullable(r1) \<and> r2 = AZERO) then
+ flts2 c rs
+ else ASEQ bs r1 r2 # flts2 c rs)"
+| "flts2 c (r1 # rs) = r1 # flts2 c rs"
+
+lemma flts2_k0:
+ shows "flts2 c (r # rs1) = flts2 c [r] @ flts2 c rs1"
+ apply(induct r arbitrary: c rs1)
+ apply(auto)
+ done
+
+lemma flts2_k00:
+ shows "flts2 c (rs1 @ rs2) = flts2 c rs1 @ flts2 c rs2"
+ apply(induct rs1 arbitrary: rs2 c)
+ apply(auto)
+ by (metis append.assoc flts2_k0)
+
+
+lemma
+ shows "flts (map (bder c) rs) = (map (bder c) (flts2 c rs))"
+ apply(induct c rs rule: flts2.induct)
+ apply(simp)
+ apply(simp)
+ apply(simp)
+ apply(simp)
+ apply(simp)
+ apply(auto simp add: bder_fuse)[1]
+ defer
+ apply(simp)
+ apply(simp del: flts2.simps)
+ apply(rule conjI)
+ prefer 2
+ apply(auto)[1]
+ apply(rule impI)
+ apply(subst flts2_k0)
+ apply(subst map_append)
+ apply(subst flts2.simps)
+ apply(simp only: flts2.simps)
+ apply(auto)
+
+
+
lemma XXX2_helper:
assumes "\<forall>y. asize y < Suc (sum_list (map asize rs)) \<longrightarrow> good y \<longrightarrow> bsimp y = y"
"\<forall>r'\<in>set rs. good r' \<and> nonalt r'"
@@ -2390,130 +2447,13 @@
apply(auto)
done
-lemma
- assumes "\<forall>y. asize y < Suc (sum_list (map asize x52)) \<longrightarrow> asize (bsimp y) = asize y \<longrightarrow> bsimp y \<noteq> AZERO \<longrightarrow> bsimp y = y"
- "asize (bsimp_AALTs x51 (flts (map bsimp x52))) = Suc (sum_list (map asize x52))"
- "bsimp_AALTs x51 (flts (map bsimp x52)) \<noteq> AZERO"
- shows "bsimp_AALTs x51 (flts (map bsimp x52)) = AALTs x51 x52"
- using assms
- apply(induct x52 arbitrary: x51)
- apply(simp)
- oops
-
-
-lemma
- assumes "asize (bsimp a) = asize a" "bsimp a \<noteq> AZERO"
- shows "bsimp a = a"
- using assms
- apply(induct a taking: asize rule: measure_induct)
- apply(case_tac x)
- apply(simp_all)
- apply(case_tac "(bsimp x42) = AZERO")
- apply(simp add: asize0)
- apply(case_tac "(bsimp x43) = AZERO")
- apply(simp add: asize0)
- apply (metis bsimp_ASEQ0)
- apply(case_tac "\<exists>bs. (bsimp x42) = AONE bs")
- apply(auto)[1]
- apply (metis b1 bsimp_size fuse_size less_add_Suc2 not_less)
- apply (metis Suc_inject add.commute asize.simps(5) bsimp_ASEQ1 bsimp_size leD le_neq_implies_less less_add_Suc2 less_add_eq_less)
- (* ALT case *)
- apply(frule iii)
- apply(case_tac x52)
- apply(simp)
- apply(simp)
- apply(subst k0)
- apply(subst (asm) k0)
- apply(subst (asm) (2) k0)
- apply(subst (asm) (3) k0)
- apply(case_tac "(bsimp a) = AZERO")
- apply(simp)
- apply (metis (no_types, lifting) Suc_le_lessD asize0 bsimp_AALTs_size le_less_trans less_add_same_cancel2 not_less_eq rt)
- apply(simp)
- apply(case_tac "nonalt (bsimp a)")
- prefer 2
- apply(drule_tac x="AALTs x51 (bsimp a # list)" in spec)
- apply(drule mp)
- apply (metis asize.simps(4) bsimp.simps(2) bsimp_AALTs_size3 k0 less_not_refl list.set_intros(1) list.simps(9) sum_list.Cons)
- apply(drule mp)
- apply(simp)
- apply (metis asize.simps(4) bsimp.simps(2) bsimp_AALTs_size3 k0 lessI list.set_intros(1) list.simps(9) not_less_eq sum_list.Cons)
- apply(drule mp)
- apply(simp)
- using bsimp_idem apply auto[1]
- apply(simp add: bsimp_idem)
- apply (metis append.left_neutral append_Cons asize.simps(4) bsimp.simps(2) bsimp_AALTs_size3 k00 less_not_refl list.set_intros(1) list.simps(9) sum_list.Cons)
- apply (metis bsimp.simps(2) bsimp_idem k0 list.simps(9) nn1b nonalt.elims(3) nonnested.simps(2))
- apply(subgoal_tac "flts [bsimp a] = [bsimp a]")
- prefer 2
- using k0b apply blast
- apply(clarify)
- apply(simp only:)
- apply(simp)
- apply(case_tac "flts (map bsimp list) = Nil")
- apply (metis bsimp_AALTs1 bsimp_size fuse_size less_add_Suc1 not_less)
- apply (subgoal_tac "bsimp_AALTs x51 (bsimp a # flts (map bsimp list)) = AALTs x51 (bsimp a # flts (map bsimp list))")
- prefer 2
- apply (metis bsimp_AALTs.simps(3) neq_Nil_conv)
- apply(auto)
- apply (metis add.commute bsimp_size leD le_neq_implies_less less_add_Suc1 less_add_eq_less rt)
- oops
-
-
-
-
-lemma OOO:
- 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 "a = AZERO")
- apply(simp)
- apply(case_tac "list")
- apply(simp)
- apply(simp)
- apply(case_tac "bsimp a = AZERO")
- apply(simp)
- apply(case_tac "list")
- apply(simp)
- apply(simp add: bsimp_fuse[symmetric])
- apply(simp)
- apply(case_tac "nonalt (bsimp a)")
- apply(case_tac list)
- apply(simp)
- apply(subst k0b)
- apply(simp)
- apply(simp)
- apply(simp add: bsimp_fuse)
- apply(simp)
- apply(subgoal_tac "asize (bsimp a) < asize a \<or> asize (bsimp a) = asize a")
- prefer 2
- using bsimp_size le_neq_implies_less apply blast
- apply(erule disjE)
- apply(drule_tac x="(bsimp a) # list" in spec)
- apply(drule mp)
- apply(simp)
- apply(simp)
- apply (metis bsimp.simps(2) bsimp_AALTs.elims bsimp_AALTs.simps(2) bsimp_fuse bsimp_idem list.distinct(1) list.inject list.simps(9))
- apply(subgoal_tac "\<exists>bs rs. bsimp a = AALTs bs rs \<and> rs \<noteq> Nil \<and> length rs > 1")
- prefer 2
- apply (metis bbbbs1 bsimp.simps(2) bsimp_AALTs.simps(1) bsimp_idem flts.simps(1) good.simps(5) good1 length_0_conv length_Suc_conv less_one list.simps(8) nat_neq_iff not_less_eq)
- apply(auto)
- oops
-
-
-lemma
- assumes "rs = [AALTs bsa [AONE bsb, AONE bsb]]"
- shows "bsimp (bsimp_AALTs bs rs) = bsimp_AALTs bs (flts (map bsimp rs))"
- using assms
- apply(simp)
- oops
-
-
+lemma CT1_SEQ:
+ shows "bsimp (ASEQ bs a1 a2) = bsimp (ASEQ bs (bsimp a1) (bsimp a2))"
+ apply(simp add: bsimp_idem)
+ done
lemma CT1:
- shows "bsimp (AALTs bs as) = bsimp(AALTs bs (map bsimp as))"
+ shows "bsimp (AALTs bs as) = bsimp (AALTs bs (map bsimp as))"
apply(induct as arbitrary: bs)
apply(simp)
apply(simp)
@@ -2523,6 +2463,21 @@
shows "bsimp (AALT bs a1 a2) = bsimp(AALT bs (bsimp a1) (bsimp a2))"
by (metis CT1 list.simps(8) list.simps(9))
+lemma WWW2:
+ shows "bsimp (bsimp_AALTs bs1 (flts (map bsimp as1))) =
+ bsimp_AALTs bs1 (flts (map bsimp as1))"
+ by (metis bsimp.simps(2) bsimp_idem)
+
+lemma CT1b:
+ shows "bsimp (bsimp_AALTs bs as) = bsimp (bsimp_AALTs bs (map bsimp as))"
+ apply(induct bs as rule: bsimp_AALTs.induct)
+ apply(auto simp add: bsimp_idem)
+ apply (simp add: bsimp_fuse bsimp_idem)
+ by (metis bsimp_idem comp_apply)
+
+
+
+
(* CT *)
lemma CTU:
@@ -2531,7 +2486,7 @@
apply(auto)
done
-
+find_theorems "bder _ (bsimp_AALTs _ _)"
lemma CTa:
assumes "\<forall>r \<in> set as. nonalt r \<and> r \<noteq> AZERO"
@@ -2574,15 +2529,6 @@
-
-lemma
- shows "bsimp (AALT bs (AALTs bs1 (map (bder c) as1)) (AALTs bs2 (map (bder c) as2)))
- = bsimp (AALTs bs ((map (fuse bs1) (map (bder c) as1)) @
- (map (fuse bs2) (map (bder c) as2))))"
- apply(subst bsimp_idem[symmetric])
- apply(simp)
- oops
-
lemma CT_exp:
assumes "\<forall>a \<in> set as. bsimp (bder c (bsimp a)) = bsimp (bder c a)"
shows "map bsimp (map (bder c) as) = map bsimp (map (bder c) (map bsimp as))"
@@ -2641,10 +2587,6 @@
using flts2 good1 apply fastforce
by (smt ex_map_conv list.simps(9) nn1b nn1c)
-lemma WWW2:
- shows "bsimp (bsimp_AALTs bs1 (flts (map bsimp as1))) =
- bsimp_AALTs bs1 (flts (map bsimp as1))"
- by (metis bsimp.simps(2) bsimp_idem)
lemma WWW3:
shows "flts [bsimp_AALTs bs1 (flts (map bsimp as1))] =
@@ -3019,12 +2961,17 @@
apply(simp)
prefer 3
apply(simp)
+ (* SEQ case *)
+ apply(simp only:)
+ apply(subst CT1_SEQ)
+ apply(simp only: bsimp.simps)
+
(* AALT case *)
prefer 2
apply(simp only:)
apply(case_tac "\<exists>a1 a2. x52 = [a1, a2]")
apply(clarify)
- apply(simp del: bsimp.simps)
+ apply(simp del: bsimp.simps)
apply(subst (2) CT1)
apply(simp del: bsimp.simps)
apply(rule_tac t="bsimp (bder c a1)" and s="bsimp (bder c (bsimp a1))" in subst)
@@ -3032,6 +2979,21 @@
apply(rule_tac t="bsimp (bder c a2)" and s="bsimp (bder c (bsimp a2))" in subst)
apply(simp del: bsimp.simps)
apply(subst CT1a[symmetric])
+ (* \<rightarrow> *)
+ apply(rule_tac t="AALT x51 (bder c (bsimp a1)) (bder c (bsimp a2))"
+ and s="bder c (AALT x51 (bsimp a1) (bsimp a2))" in subst)
+ apply(simp)
+ apply(subst bsimp.simps)
+ apply(simp del: bsimp.simps bder.simps)
+
+ apply(subst bder_bsimp_AALTs)
+ apply(subst bsimp.simps)
+ apply(subst WWW2[symmetric])
+ apply(subst bsimp_AALTs_qq)
+ defer
+ apply(subst bsimp.simps)
+
+ (* <- *)
apply(subst bsimp.simps)
apply(simp del: bsimp.simps)
(*bsimp_AALTs x51 (map (bder c) (flts [a1, a2])) =
@@ -3046,7 +3008,7 @@
apply(simp del: bsimp.simps)
apply(subst big0)
apply(simp add: WWW4)
- apply (metis One_nat_def Suc_eq_plus1 Suc_lessI arexp.distinct(7) bsimp.simps(2) bsimp_AALTs.simps(1) bsimp_idem flts.simps(1) length_append length_greater_0_conv length_map not_add_less2 not_less_eq)
+ apply (m etis One_nat_def Suc_eq_plus1 Suc_lessI arexp.distinct(7) bsimp.simps(2) bsimp_AALTs.simps(1) bsimp_idem flts.simps(1) length_append length_greater_0_conv length_map not_add_less2 not_less_eq)
oops
lemma XXX2a_long_without_good: