
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 \<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)




