Mercurial Mercurial > hg > lexing / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
a simple proof of big0
authorChristian Urban <urbanc@in.tum.de>
Mon, 29 Jul 2019 20:20:32 +0100
changeset 334 cc26b029a866
parent 333 e0903f6fb4f7
child 335 f5ab2f02d148
a simple proof of big0
thys/BitCoded.thy file | annotate | diff | comparison | revisions 
--- 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 \<circ> fuse bs1) as1 = map (fuse bs1) (map (bder c) as1)"
+  apply(induct as1)
+   apply(auto)
+  using bder_fuse by blast
+  
+
 lemma big0:
-  assumes as1p: "\<exists>as1'. map (fuse bs1) as1 = as1'" 
-      and as2p: "\<exists>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: "\<exists>as1'. map (fuse bs1) as1 = as1'" 
-      and as2p: "\<exists>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:
lexing