
diff -r 8b0b414e71b0 -r 3b8e3a156200 thys/BitCoded.thy
--- a/thys/BitCoded.thy	Wed Feb 20 00:00:30 2019 +0000
+++ b/thys/BitCoded.thy	Sat Feb 23 21:52:06 2019 +0000
@@ -120,6 +120,7 @@
 fun retrieve :: "arexp \<Rightarrow> val \<Rightarrow> bit list" where
   "retrieve (AONE bs) Void = bs"
 | "retrieve (ACHAR bs c) (Char d) = bs"
+| "retrieve (AALTs bs [r]) v = bs @ retrieve r v" 
 | "retrieve (AALTs bs (r#rs)) (Left v) = bs @ retrieve r v"
 | "retrieve (AALTs bs (r#rs)) (Right v) = bs @ retrieve (AALTs [] rs) v"
 | "retrieve (ASEQ bs r1 r2) (Seq v1 v2) = bs @ retrieve r1 v1 @ retrieve r2 v2"
@@ -135,7 +136,7 @@
 | "erase (ACHAR _ c) = CHAR c"
 | "erase (AALTs _ []) = ZERO"
 | "erase (AALTs _ [r]) = (erase r)"
-| "erase (AALTs _ (r#rs)) = ALT (erase r) (erase (AALTs [] rs))"
+| "erase (AALTs bs (r#rs)) = ALT (erase r) (erase (AALTs bs rs))"
 | "erase (ASEQ _ r1 r2) = SEQ (erase r1) (erase r2)"
 | "erase (ASTAR _ r) = STAR (erase r)"
 
@@ -154,6 +155,7 @@
 where
   "bmkeps(AONE bs) = bs"
 | "bmkeps(ASEQ bs r1 r2) = bs @ (bmkeps r1) @ (bmkeps r2)"
+| "bmkeps(AALTs bs [r]) = bs @ (bmkeps r)"
 | "bmkeps(AALTs bs (r#rs)) = (if bnullable(r) then bs @ (bmkeps r) else (bmkeps (AALTs bs rs)))"
 | "bmkeps(ASTAR bs r) = bs @ [S]"
 
@@ -226,9 +228,25 @@
   assumes "\<Turnstile> v : (erase r)"
   shows "retrieve (fuse bs r) v = bs @ retrieve r v"
   using assms
-  apply(induct r arbitrary: v bs rule: erase.induct)
-         apply(auto elim: Prf_elims)[1]
-  sorry
+  apply(induct r arbitrary: v bs)
+         apply(auto elim: Prf_elims)[4]
+   defer
+  using retrieve_encode_STARS
+   apply(auto elim!: Prf_elims)[1]
+   apply(case_tac vs)
+    apply(simp)
+   apply(simp)
+  (* AALTs  case *)
+  apply(simp)
+  apply(case_tac x2a)
+   apply(simp)
+   apply(auto elim!: Prf_elims)[1]
+  apply(simp)
+   apply(case_tac list)
+   apply(simp)
+  apply(auto)
+  apply(auto elim!: Prf_elims)[1]
+  done
 
 lemma retrieve_fuse:
   assumes "\<Turnstile> v : r"
@@ -243,24 +261,135 @@
   using assms
   apply(induct v r )
   apply(simp_all add: retrieve_fuse retrieve_encode_STARS)
-  sorry
+  done
+
+lemma r:
+  assumes "bnullable (AALTs bs (a # rs))"
+  shows "bnullable a \<or> (\<not> bnullable a \<and> bnullable (AALTs bs rs))"
+  using assms
+  apply(induct rs)
+   apply(auto)
+  done
+
+lemma r0:
+  assumes "bnullable a" 
+  shows  "bmkeps (AALTs bs (a # rs)) = bs @ (bmkeps a)"
+  using assms
+  by (metis bmkeps.simps(3) bmkeps.simps(4) list.exhaust)
+
+lemma r1:
+  assumes "\<not> bnullable a" "bnullable (AALTs bs rs)"
+  shows  "bmkeps (AALTs bs (a # rs)) = bmkeps (AALTs bs rs)"
+  using assms
+  apply(induct rs)
+   apply(auto)
+  done
+
+lemma r2:
+  assumes "x \<in> set rs" "bnullable x"
+  shows "bnullable (AALTs bs rs)"
+  using assms
+  apply(induct rs)
+   apply(auto)
+  done
 
+lemma  r3:
+  assumes "\<not> bnullable r" 
+          " \<exists> x \<in> set rs. bnullable x"
+  shows "retrieve (AALTs bs rs) (mkeps (erase (AALTs bs rs))) =
+         retrieve (AALTs bs (r # rs)) (mkeps (erase (AALTs bs (r # rs))))"
+  using assms
+  apply(induct rs arbitrary: r bs)
+   apply(auto)[1]
+  apply(auto)
+  using bnullable_correctness apply blast
+    apply(auto simp add: bnullable_correctness mkeps_nullable retrieve_fuse2)
+   apply(subst retrieve_fuse2[symmetric])
+  apply (smt bnullable.simps(4) bnullable_correctness erase.simps(5) erase.simps(6) insert_iff list.exhaust list.set(2) mkeps.simps(3) mkeps_nullable)
+   apply(simp)
+  apply(case_tac "bnullable a")
+  apply (smt append_Nil2 bnullable.simps(4) bnullable_correctness erase.simps(5) erase.simps(6) fuse.simps(4) insert_iff list.exhaust list.set(2) mkeps.simps(3) mkeps_nullable retrieve_fuse2)
+  apply(drule_tac x="a" in meta_spec)
+  apply(drule_tac x="bs" in meta_spec)
+  apply(drule meta_mp)
+   apply(simp)
+  apply(drule meta_mp)
+   apply(auto)
+  apply(subst retrieve_fuse2[symmetric])
+  apply(case_tac rs)
+    apply(simp)
+   apply(auto)[1]
+      apply (simp add: bnullable_correctness)
+  apply (metis append_Nil2 bnullable_correctness erase_fuse fuse.simps(4) list.set_intros(1) mkeps.simps(3) mkeps_nullable nullable.simps(4) r2)
+    apply (simp add: bnullable_correctness)
+  apply (metis append_Nil2 bnullable_correctness erase.simps(6) erase_fuse fuse.simps(4) list.set_intros(2) mkeps.simps(3) mkeps_nullable r2)
+  apply(simp)
+  done
+
+
+lemma t: 
+  assumes "\<forall>r \<in> set rs. nullable (erase r) \<longrightarrow> bmkeps r = retrieve r (mkeps (erase r))" 
+          "nullable (erase (AALTs bs rs))"
+  shows " bmkeps (AALTs bs rs) = retrieve (AALTs bs rs) (mkeps (erase (AALTs bs rs)))"
+  using assms
+  apply(induct rs arbitrary: bs)
+   apply(simp)
+  apply(auto simp add: bnullable_correctness)
+   apply(case_tac rs)
+     apply(auto simp add: bnullable_correctness)[2]
+   apply(subst r1)
+     apply(simp)
+    apply(rule r2)
+     apply(assumption)
+    apply(simp)
+   apply(drule_tac x="bs" in meta_spec)
+   apply(drule meta_mp)
+    apply(auto)[1]
+   prefer 2
+  apply(case_tac "bnullable a")
+    apply(subst r0)
+     apply blast
+    apply(subgoal_tac "nullable (erase a)")
+  prefer 2
+  using bnullable_correctness apply blast
+  apply (metis (no_types, lifting) erase.simps(5) erase.simps(6) list.exhaust mkeps.simps(3) retrieve.simps(3) retrieve.simps(4))
+  apply(subst r1)
+     apply(simp)
+  using r2 apply blast
+  apply(drule_tac x="bs" in meta_spec)
+   apply(drule meta_mp)
+    apply(auto)[1]
+   apply(simp)
+  using r3 apply blast
+  apply(auto)
+  using r3 by blast
 
 lemma bmkeps_retrieve:
   assumes "nullable (erase r)"
   shows "bmkeps r = retrieve r (mkeps (erase r))"
   using assms
   apply(induct r)
-       apply(auto simp add: bnullable_correctness)
-  sorry
-  
+         apply(simp)
+        apply(simp)
+       apply(simp)
+    apply(simp)
+   defer
+   apply(simp)
+  apply(rule t)
+   apply(auto)
+  done
+
 lemma bder_retrieve:
   assumes "\<Turnstile> v : der c (erase r)"
   shows "retrieve (bder c r) v = retrieve r (injval (erase r) c v)"
   using assms
-  apply(induct r arbitrary: v)
+  apply(induct r arbitrary: v rule: erase.induct)
   apply(auto elim!: Prf_elims simp add: retrieve_fuse2 bnullable_correctness bmkeps_retrieve)
-  sorry
+  apply(case_tac va)
+   apply(simp)
+  apply(auto)
+  by (smt Prf_elims(3) injval.simps(2) injval.simps(3) retrieve.simps(4) retrieve.simps(5) same_append_eq)
+  
 
 lemma MAIN_decode:
   assumes "\<Turnstile> v : ders s r"




