diff -r e0903f6fb4f7 -r cc26b029a866 thys/BitCoded.thy --- a/thys/BitCoded.thy Mon Jul 29 16:54:56 2019 +0100 +++ b/thys/BitCoded.thy Mon Jul 29 20:20:32 2019 +0100 @@ -2641,143 +2641,29 @@ 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))] = + flts (map bsimp (map (fuse bs1) as1))" + by (metis CT0 YY flts_nonalt flts_nothing qqq1) + +lemma WWW4: + shows "map (bder c \ fuse bs1) as1 = map (fuse bs1) (map (bder c) as1)" + apply(induct as1) + apply(auto) + using bder_fuse by blast + + lemma big0: - assumes as1p: "\as1'. map (fuse bs1) as1 = as1'" - and as2p: "\as2'. map (fuse bs2) as2 = as2'" shows "bsimp (AALT x51 (AALTs bs1 as1) (AALTs bs2 as2)) = bsimp (AALTs x51 ((map (fuse bs1) as1) @ (map (fuse bs2) as2)))" - apply - - apply(subst CT1a) - apply(subst (2) bsimp.simps) - apply(subst (2) bsimp.simps) - apply(subst (2) bsimp_idem[symmetric]) - apply(subst (2) bsimp.simps) - using as1p as2p - apply - - apply(erule exE)+ - apply(simp del: bsimp.simps) - apply(simp only: flts_append) - apply(case_tac "flts (map bsimp as1)") - apply(subgoal_tac "flts (map bsimp as1') = []") - prefer 2 - using YY apply auto[1] - apply(simp only:) - apply(simp del: bsimp_AALTs.simps bsimp.simps) - apply(subst bsimp_AALTs.simps) - apply(case_tac "flts (map bsimp as2)") - apply(subgoal_tac "flts (map bsimp as2') = []") - prefer 2 - using YY apply auto[1] - apply(simp) - apply(case_tac list) - apply(simp) - apply(subgoal_tac "flts (map bsimp as2') = map (fuse bs2) [a]") - prefer 2 - using YY apply blast - apply(simp) - apply(subgoal_tac "nonalt a") - prefer 2 - apply (simp add: flts_nonalt) - apply(subgoal_tac "nonalt (fuse bs2 a)") - prefer 2 - using nn11a apply blast - apply (metis bsimp.simps(2) bsimp_AALTs.simps(2) bsimp_AALTs1 bsimp_idem) - apply(simp only:) - apply(subgoal_tac "bsimp_AALTs bs2 (a # aa # lista) = AALTs bs2 (a # aa # lista)") - prefer 2 - using bsimp_AALTs.simps(3) apply blast - apply(simp only:) - apply(subgoal_tac "flts (map bsimp as2') = map (fuse bs2)(a # aa # lista) ") - prefer 2 - using YY apply blast - apply(simp only:) - apply(subst (1) bsimp_idem[symmetric]) - apply(simp) - apply (metis arexp.distinct(7) bbbbs bsimp.simps(2) bsimp_AALTs.simps(3) bsimp_idem good1 list.simps(9) map_map) - (* HERE TODAY *) - - - sorry -(* - - - using as1 apply auto[1] - apply(case_tac list) - apply(simp) - apply (metis as1 bsimp.simps(2) bsimp_AALTs.simps(2) bsimp_AALTs_size3 bsimp_size list.set_intros(1) n0 nn11a nn_flts nonalt.simps(1) not_less) - apply(simp only:) - apply(subgoal_tac "flts (map bsimp as1') = map (fuse bs1) (a # aa # lista)") - prefer 2 - apply (metis CTa arexp.distinct(7) as1 bsimp.simps(2) bsimp_AALTs.simps(3) flts2 good.simps(1) good1 k0a map_idI test2) - apply(simp only:) - apply(simp only: bsimp_AALTs.simps) - apply(simp del: bsimp_AALTs.simps bsimp.simps) - apply(subst bsimp_AALTs.simps) - apply(case_tac "flts (map bsimp as2)") - apply(simp) - using as2 apply auto[1] - apply(case_tac listb) - apply(simp) - apply (metis as2 bsimp.simps(2) bsimp_AALTs.simps(2) bsimp_AALTs_size3 bsimp_size list.set_intros(1) n0 nn11a nn_flts nonalt.simps(1) not_less) - apply(simp only:) - apply(simp only: bsimp_AALTs.simps) - apply(subgoal_tac "flts (map bsimp as2') = map (fuse bs2) (ab # ac # listc)") - prefer 2 - apply (metis arexp.distinct(7) as2 bsimp.simps(2) bsimp_AALTs.simps(3) flts2 flts_qq good1 k0a test2) - apply(simp only:) - apply(simp del: bsimp.simps) - by (smt append_Cons bsimp.simps(2) bsimp_AALTs.simps(3) bsimp_idem k0 k0a list.simps(8) list.simps(9)) -*) + by (smt WWW3 bsimp.simps(2) k0 k00 list.simps(8) list.simps(9) map_append) -(* -lemma big: - assumes as1: "(AALTs bs1 as1) = bsimp (AALTs bs1 as1)" - and as2: "(AALTs bs2 as2) = bsimp (AALTs bs2 as2)" - and as1p: "\as1'. map (fuse bs1) as1 = as1'" - and as2p: "\as2'. map (fuse bs2) as2 = as2'" - shows "bsimp (AALT x51 (AALTs bs1 as1) (AALTs bs2 as2)) = - bsimp (AALTs x51 ((map (fuse bs1) as1) @ (map (fuse bs2) as2)))" - apply - - apply(subst as1) - apply(subst as2) - apply(subst (2) bsimp.simps) - apply(subst (2) bsimp.simps) - apply(subst (2) bsimp_idem[symmetric]) - apply(subst (2) bsimp.simps) - using as1p as2p - apply - - apply(erule exE)+ - apply(simp del: bsimp.simps) - apply(simp only: flts_append) - apply(case_tac "flts (map bsimp as1)") - apply(simp) - using as1 apply auto[1] - apply(case_tac list) - apply(simp) - apply (metis as1 bsimp.simps(2) bsimp_AALTs.simps(2) bsimp_AALTs_size3 bsimp_size list.set_intros(1) n0 nn11a nn_flts nonalt.simps(1) not_less) - apply(simp only:) - apply(subgoal_tac "flts (map bsimp as1') = map (fuse bs1) (a # aa # lista)") - prefer 2 - apply (metis CTa arexp.distinct(7) as1 bsimp.simps(2) bsimp_AALTs.simps(3) flts2 good.simps(1) good1 k0a map_idI test2) - apply(simp only:) - apply(simp only: bsimp_AALTs.simps) - apply(simp del: bsimp_AALTs.simps bsimp.simps) - apply(subst bsimp_AALTs.simps) - apply(case_tac "flts (map bsimp as2)") - apply(simp) - using as2 apply auto[1] - apply(case_tac listb) - apply(simp) - apply (metis as2 bsimp.simps(2) bsimp_AALTs.simps(2) bsimp_AALTs_size3 bsimp_size list.set_intros(1) n0 nn11a nn_flts nonalt.simps(1) not_less) - apply(simp only:) - apply(simp only: bsimp_AALTs.simps) - apply(subgoal_tac "flts (map bsimp as2') = map (fuse bs2) (ab # ac # listc)") - prefer 2 - apply (metis arexp.distinct(7) as2 bsimp.simps(2) bsimp_AALTs.simps(3) flts2 flts_qq good1 k0a test2) - apply(simp only:) - apply(simp del: bsimp.simps) - by (smt append_Cons bsimp.simps(2) bsimp_AALTs.simps(3) bsimp_idem k0 k0a list.simps(8) list.simps(9)) -*) + lemma XXX2a_long_without_good: shows "bsimp (bder c (bsimp a)) = bsimp (bder c a)" @@ -2811,13 +2697,8 @@ prefer 2 apply(simp del: bsimp.simps) apply(subst big0) - prefer 2 - apply(blast) - prefer 2 - apply(blast) - prefer 2 - - + 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) oops lemma XXX2a_long_without_good: