diff -r 44914e2724b7 -r 6c71db65bdec thys/BitCoded.thy --- 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 \ AZERO) " + "\(\ a01 a02 x02. ( (a1 = ASEQ x02 a01 a02) \ 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] \ 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 " \ 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 \ AZERO) " + "\(\ a01 a02 x02. ( (a1 = ASEQ x02 a01 a02) \ bnullable(a01) ) )" +" (bder c a2 \ AZERO)" + "\(\ a11 a12 x12. ( (a2 = ASEQ x12 a11 a12) \ 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 "\bs1 as1. bsimp a1 = AALTs bs1 as1") apply(case_tac "\bs2 as2. bsimp a2 = AALTs bs2 as2") apply(clarify)