--- a/thys/BitCoded.thy Tue Jul 30 10:44:12 2019 +0100
+++ b/thys/BitCoded.thy Mon Aug 19 13:33:53 2019 +0100
@@ -2316,7 +2316,7 @@
lemma bder_bsimp_AALTs:
shows "bder c (bsimp_AALTs bs rs) = bsimp_AALTs bs (map (bder c) rs)"
- apply(induct bs rs rule: bsimp_AALTs.induct)
+ apply(induct bs rs rule: bsimp_AALTs.induct)
apply(simp)
apply(simp)
apply (simp add: bder_fuse)
@@ -2663,6 +2663,339 @@
apply(auto)
done
+lemma WWW6:
+ shows "bsimp (bder c (bsimp_AALTs x51 (flts [bsimp a1, bsimp a2]) ) ) =
+ bsimp(bsimp_AALTs x51 (map (bder c) (flts [bsimp a1, bsimp a2]))) "
+ using bder_bsimp_AALTs by auto
+
+lemma WWW7:
+ shows "bsimp (bsimp_AALTs x51 (map (bder c) (flts [bsimp a1, bsimp a2]))) =
+ bsimp(bsimp_AALTs x51 (flts (map (bder c) [bsimp a1, bsimp a2])))"
+ sorry
+
+
+lemma stupid:
+ assumes "a = b"
+ shows "bsimp(a) = bsimp(b)"
+ using assms
+ apply(auto)
+ done
+(*
+proving idea:
+bsimp_AALTs x51 (map (bder c) (flts [a1, a2])) = bsimp_AALTs x51 (map (bder c) (flts [a1]++[a2]))
+= bsimp_AALTs x51 (map (bder c) ((flts [a1])++(flts [a2]))) =
+bsimp_AALTs x51 (map (bder c) (flts [a1]))++(map (bder c) (flts [a2])) = A
+and then want to prove that
+map (bder c) (flts [a]) = flts [bder c a] under the condition
+that a is either a seq with the first elem being not nullable, or a character equal to c,
+or an AALTs, or a star
+Then, A = bsimp_AALTs x51 (flts [bder c a]) ++ (map (bder c) (flts [a2])) = A1
+Using the same condition for a2, we get
+A1 = bsimp_AALTs x51 (flts [bder c a1]) ++ (flts [bder c a2])
+=bsimp_AALTs x51 flts ([bder c a1] ++ [bder c a2])
+=bsimp_AALTs x51 flts ([bder c a1, bder c a2])
+ *)
+lemma manipulate_flts:
+ shows "bsimp_AALTs x51 (map (bder c) (flts [a1, a2])) =
+bsimp_AALTs x51 ((map (bder c) (flts [a1])) @ (map (bder c) (flts [a2])))"
+ by (metis k0 map_append)
+
+lemma go_inside_flts:
+ assumes " (bder c a1 \<noteq> AZERO) "
+ "\<not>(\<exists> a01 a02 x02. ( (a1 = ASEQ x02 a01 a02) \<and> bnullable(a01) ) )"
+shows "map (bder c) (flts [a1]) = flts [bder c a1]"
+ using assms
+ apply -
+ apply(case_tac a1)
+ apply(simp)
+ apply(simp)
+ apply(case_tac "x32 = c")
+ prefer 2
+ apply(simp)
+ apply(simp)
+ apply(simp)
+ apply (simp add: WWW4)
+ apply(simp add: bder_fuse)
+ done
+
+lemma medium010:
+ assumes " (bder c a1 = AZERO) "
+ shows "map (bder c) (flts [a1]) = [AZERO] \<or> map (bder c) (flts [a1]) = []"
+ using assms
+ apply -
+ apply(case_tac a1)
+ apply(simp)
+ apply(simp)
+ apply(simp)
+ apply(simp)
+ apply(simp)
+ apply(simp)
+ done
+
+lemma medium011:
+ assumes " (bder c a1 = AZERO) "
+ shows "flts (map (bder c) [a1, a2]) = flts [bder c a2]"
+ using assms
+ apply -
+ apply(simp)
+ done
+
+lemma medium01central:
+ shows "bsimp(bsimp_AALTs x51 (map (bder c) (flts [a2])) ) = bsimp(bsimp_AALTs x51 (flts [bder c a2]))"
+ sorry
+
+
+lemma plus_bsimp:
+ assumes "bsimp( bsimp a) = bsimp (bsimp b)"
+ shows "bsimp a = bsimp b"
+ using assms
+ apply -
+ by (simp add: bsimp_idem)
+lemma patience_good5:
+ assumes "bsimp r = AALTs x y"
+ shows " \<exists> a aa list. y = a#aa#list"
+ by (metis Nil_is_map_conv arexp.simps(13) assms bsimp_AALTs.elims flts1 good.simps(5) good1 k0a)
+
+
+(*this does not hold actually
+lemma bsimp_equiv0:
+ shows "bsimp(bsimp r) = bsimp(bsimp (AALTs [] [r]))"
+ apply(simp)
+ apply(case_tac "bsimp r")
+ apply(simp)
+ apply(simp)
+ apply(simp)
+ apply(simp)
+ thm good1
+ using good1
+ apply -
+ apply(drule_tac x="r" in meta_spec)
+ apply(erule disjE)
+
+ apply(simp only: bsimp_AALTs.simps)
+ apply(simp only:flts.simps)
+ apply(drule patience_good5)
+ apply(clarify)
+ apply(subst bsimp_AALTs_qq)
+ apply simp
+ prefer 2
+ sorry*)
+
+(*exercise: try multiple ways of proving this*)
+(*this lemma does not hold.........
+lemma bsimp_equiv1:
+ shows "bsimp r = bsimp (AALTs [] [r])"
+ using plus_bsimp
+ apply -
+ using bsimp_equiv0 by blast
+ (*apply(simp)
+ apply(case_tac "bsimp r")
+ apply(simp)
+ apply(simp)
+ apply(simp)
+ apply(simp)
+(*use lemma good1*)
+ thm good1
+ using good1
+ apply -
+ apply(drule_tac x="r" in meta_spec)
+ apply(erule disjE)
+
+ apply(subst flts_single1)
+ apply(simp only: bsimp_AALTs.simps)
+ prefer 2
+
+ thm flts_single1
+
+ find_theorems "flts _ = _"*)
+*)
+lemma bsimp_equiv2:
+ shows "bsimp (AALTs x51 [r]) = bsimp (AALT x51 AZERO r)"
+ sorry
+
+lemma medium_stupid_isabelle:
+ assumes "rs = a # list"
+ shows "bsimp_AALTs x51 (AZERO # rs) = AALTs x51 (AZERO#rs)"
+ using assms
+ apply -
+ apply(simp)
+ done
+(*
+lemma mediumlittle:
+ shows "bsimp(bsimp_AALTs x51 rs) = bsimp(bsimp_AALTs x51 (AZERO # rs))"
+ apply(case_tac rs)
+ apply(simp)
+ apply(case_tac list)
+ apply(subst medium_stupid_isabelle)
+ apply(simp)
+ prefer 2
+ apply simp
+ apply(rule_tac s="a#list" and t="rs" in subst)
+ apply(simp)
+ apply(rule_tac t="list" and s= "[]" in subst)
+ apply(simp)
+ (*dunno what is the rule for x#nil = x*)
+ apply(case_tac a)
+ apply(simp)
+ apply(simp)
+ apply(simp)
+ prefer 3
+ apply simp
+ apply(simp only:bsimp_AALTs.simps)
+
+ apply simp
+ apply(case_tac "bsimp x42")
+ apply(simp)
+ apply simp
+ apply(case_tac "bsimp x43")
+ apply simp
+ apply simp
+ apply simp
+ apply simp
+ apply(simp only:bsimp_ASEQ.simps)
+ using good1
+ apply -
+ apply(drule_tac x="x43" in meta_spec)
+ apply(erule disjE)
+ apply(subst bsimp_AALTs_qq)
+ using patience_good5 apply force
+ apply(simp only:bsimp_AALTs.simps)
+ apply(simp only:fuse.simps)
+ apply(simp only:flts.simps)
+(*OK from here you actually realize this lemma doesnt hold*)
+ apply(simp)
+ apply(simp)
+ apply(rule_tac t="rs" and s="a#list" in subst)
+ apply(simp)
+ apply(rule_tac t="list" and s="[]" in subst)
+ apply(simp)
+ (*apply(simp only:bsimp_AALTs.simps)*)
+ (*apply(simp only:fuse.simps)*)
+ sorry
+*)
+lemma singleton_list_map:
+ shows"map f [a] = [f a]"
+ apply simp
+ done
+lemma map_application2:
+ shows"map f [a,b] = [f a, f b]"
+ apply simp
+ done
+
+(* bsimp (bder c (bsimp_AALTs x51 (flts [bsimp a1, bsimp a2]))) =
+ bsimp (AALT x51 (bder c (bsimp a1)) (bder c (bsimp a2)))*)
+(*This equality does not hold*)
+lemma medium01:
+ assumes " (bder c a1 = AZERO) "
+ shows "bsimp(bsimp_AALTs x51 (map (bder c) (flts [ a1, a2]))) =
+ bsimp(bsimp_AALTs x51 (flts (map (bder c) [ a1, a2])))"
+ apply(subst manipulate_flts)
+ using assms
+ apply -
+ apply(subst medium011)
+ apply(simp)
+ apply(case_tac "map (bder c) (flts [a1]) = []")
+ apply(simp)
+ using medium01central apply blast
+apply(frule medium010)
+ apply(erule disjE)
+ prefer 2
+ apply(simp)
+ apply(simp)
+ apply(case_tac a2)
+ apply simp
+ apply simp
+ apply simp
+ apply(simp only:flts.simps)
+(*HOW do i say here to replace ASEQ ..... back into a2*)
+(*how do i say here to use the definition of map function
+without lemma, of course*)
+(*how do i say here that AZERO#map (bder c) [ASEQ x41 x42 x43]'s list.len >1
+without a lemma, of course*)
+ apply(subst singleton_list_map)
+ apply(simp only: bsimp_AALTs.simps)
+ apply(case_tac "bder c (ASEQ x41 x42 x43)")
+ apply simp
+ apply simp
+ apply simp
+ prefer 3
+ apply simp
+ apply(rule_tac t="bder c (ASEQ x41 x42 x43)"
+and s="ASEQ x41a x42a x43a" in subst)
+ apply simp
+ apply(simp only: flts.simps)
+ apply(simp only: bsimp_AALTs.simps)
+ apply(simp only: fuse.simps)
+ apply(subst (2) bsimp_idem[symmetric])
+ apply(subst (1) bsimp_idem[symmetric])
+ apply(simp only:bsimp.simps)
+ apply(subst map_application2)
+ apply(simp only: bsimp.simps)
+ apply(simp only:flts.simps)
+(*want to happily change between a2 and ASEQ x41 42 43, and eliminate now
+redundant conditions such as map (bder c) (flts [a1]) = [AZERO] *)
+ apply(case_tac "bsimp x42a")
+ apply(simp)
+ apply(case_tac "bsimp x43a")
+ apply(simp)
+ apply(simp)
+ apply(simp)
+ apply(simp)
+ prefer 2
+ apply(simp)
+ apply(rule_tac t="bsimp x43a"
+and s="AALTs x51a x52" in subst)
+ apply simp
+ apply(simp only:bsimp_ASEQ.simps)
+ apply(simp only:fuse.simps)
+ apply(simp only:flts.simps)
+
+ using medium01central mediumlittle by auto
+
+
+
+lemma medium1:
+ assumes " (bder c a1 \<noteq> AZERO) "
+ "\<not>(\<exists> a01 a02 x02. ( (a1 = ASEQ x02 a01 a02) \<and> bnullable(a01) ) )"
+" (bder c a2 \<noteq> AZERO)"
+ "\<not>(\<exists> a11 a12 x12. ( (a2 = ASEQ x12 a11 a12) \<and> bnullable(a11) ) )"
+ shows "bsimp_AALTs x51 (map (bder c) (flts [ a1, a2])) =
+ bsimp_AALTs x51 (flts (map (bder c) [ a1, a2]))"
+ using assms
+ apply -
+ apply(subst manipulate_flts)
+ apply(case_tac "a1")
+ apply(simp)
+ apply(simp)
+ apply(case_tac "x32 = c")
+ prefer 2
+ apply(simp)
+ prefer 2
+ apply(case_tac "bnullable x42")
+ apply(simp)
+ apply(simp)
+
+ apply(case_tac "a2")
+ apply(simp)
+ apply(simp)
+ apply(case_tac "x32 = c")
+ prefer 2
+ apply(simp)
+ apply(simp)
+ apply(case_tac "bnullable x42a")
+ apply(simp)
+ apply(subst go_inside_flts)
+ apply(simp)
+ apply(simp)
+ apply(simp)
+ apply(simp)
+ apply (simp add: WWW4)
+ apply(simp)
+ apply (simp add: WWW4)
+ apply (simp add: go_inside_flts)
+ apply (metis (no_types, lifting) go_inside_flts k0 list.simps(8) list.simps(9))
+ by (smt bder.simps(6) flts.simps(1) flts.simps(6) flts.simps(7) go_inside_flts k0 list.inject list.simps(9))
+
lemma big0:
shows "bsimp (AALT x51 (AALTs bs1 as1) (AALTs bs2 as2)) =
bsimp (AALTs x51 ((map (fuse bs1) as1) @ (map (fuse bs2) as2)))"
@@ -2684,7 +3017,7 @@
apply(simp)
apply(simp)
apply(simp)
- prefer 3
+ prefer 3
apply(simp)
(* AALT case *)
prefer 2
@@ -2701,6 +3034,8 @@
apply(subst CT1a[symmetric])
apply(subst bsimp.simps)
apply(simp del: bsimp.simps)
+(*bsimp_AALTs x51 (map (bder c) (flts [a1, a2])) =
+ bsimp_AALTs x51 (flts (map (bder c) [a1, a2]))*)
apply(case_tac "\<exists>bs1 as1. bsimp a1 = AALTs bs1 as1")
apply(case_tac "\<exists>bs2 as2. bsimp a2 = AALTs bs2 as2")
apply(clarify)