diff -r 06aa99b54423 -r fedc16924b76 thys/BitCoded2.thy
--- a/thys/BitCoded2.thy	Wed Sep 18 16:35:57 2019 +0100
+++ b/thys/BitCoded2.thy	Sat Oct 24 12:13:39 2020 +0100
@@ -170,7 +170,7 @@
 | "intern (ALT r1 r2) = AALT [] (fuse [Z] (intern r1)) 
                                 (fuse [S]  (intern r2))"
 | "intern (SEQ r1 r2) = ASEQ [] (intern r1) (intern r2)"
-| "intern (STAR r) = ASTAR [] (intern r)"
+| "intern (STAR r) = ASTAR [S] (intern r)"
 
 
 fun retrieve :: "arexp \<Rightarrow> val \<Rightarrow> bit list" where
@@ -203,7 +203,7 @@
 | "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]"
+| "bmkeps(ASTAR bs r) = bs"
 
 
 fun
@@ -217,7 +217,15 @@
      (if bnullable r1
       then AALT bs (ASEQ [] (bder c r1) r2) (fuse (bmkeps r1) (bder c r2))
       else ASEQ bs (bder c r1) r2)"
-| "bder c (ASTAR bs r) = ASEQ bs (fuse [Z] (bder c r)) (ASTAR [] r)"
+| "bder c (ASTAR bs r) = ASEQ (butlast bs) (fuse [Z] (bder c r)) (ASTAR [S] r)"
+
+
+
+lemma bder_fuse:
+  "fuse bs (bder c r) = bder c (fuse bs r)"
+  apply(induct r arbitrary: bs)
+  apply(simp_all)
+  done
 
 
 fun 
@@ -301,14 +309,6 @@
   by (simp_all add: retrieve_fuse2)
 
 
-lemma retrieve_code:
-  assumes "\<Turnstile> v : r"
-  shows "code v = retrieve (intern r) v"
-  using assms
-  apply(induct v r )
-  apply(simp_all add: retrieve_fuse retrieve_encode_STARS)
-  done
-
 lemma r:
   assumes "bnullable (AALTs bs (a # rs))"
   shows "bnullable a \<or> (\<not> bnullable a \<and> bnullable (AALTs bs rs))"
@@ -410,148 +410,6 @@
   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(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 rule: erase.induct)
-         apply(simp)
-         apply(erule Prf_elims)
-        apply(simp)
-        apply(erule Prf_elims) 
-        apply(simp)
-      apply(case_tac "c = ca")
-       apply(simp)
-       apply(erule Prf_elims)
-       apply(simp)
-      apply(simp)
-       apply(erule Prf_elims)
-  apply(simp)
-      apply(erule Prf_elims)
-     apply(simp)
-    apply(simp)
-  apply(rename_tac "r\<^sub>1" "r\<^sub>2" rs v)
-    apply(erule Prf_elims)
-     apply(simp)
-    apply(simp)
-    apply(case_tac rs)
-     apply(simp)
-    apply(simp)
-  apply (smt Prf_elims(3) injval.simps(2) injval.simps(3) retrieve.simps(4) retrieve.simps(5) same_append_eq)
-   apply(simp)
-   apply(case_tac "nullable (erase r1)")
-    apply(simp)
-  apply(erule Prf_elims)
-     apply(subgoal_tac "bnullable r1")
-  prefer 2
-  using bnullable_correctness apply blast
-    apply(simp)
-     apply(erule Prf_elims)
-     apply(simp)
-   apply(subgoal_tac "bnullable r1")
-  prefer 2
-  using bnullable_correctness apply blast
-    apply(simp)
-    apply(simp add: retrieve_fuse2)
-    apply(simp add: bmkeps_retrieve)
-   apply(simp)
-   apply(erule Prf_elims)
-   apply(simp)
-  using bnullable_correctness apply blast
-  apply(rename_tac bs r v)
-  apply(simp)
-  apply(erule Prf_elims)
-     apply(clarify)
-  apply(erule Prf_elims)
-  apply(clarify)
-  apply(subst injval.simps)
-  apply(simp del: retrieve.simps)
-  apply(subst retrieve.simps)
-  apply(subst retrieve.simps)
-  apply(simp)
-  apply(simp add: retrieve_fuse2)
-  done
-  
-
-
-lemma MAIN_decode:
-  assumes "\<Turnstile> v : ders s r"
-  shows "Some (flex r id s v) = decode (retrieve (bders (intern r) s) v) r"
-  using assms
-proof (induct s arbitrary: v rule: rev_induct)
-  case Nil
-  have "\<Turnstile> v : ders [] r" by fact
-  then have "\<Turnstile> v : r" by simp
-  then have "Some v = decode (retrieve (intern r) v) r"
-    using decode_code retrieve_code by auto
-  then show "Some (flex r id [] v) = decode (retrieve (bders (intern r) []) v) r"
-    by simp
-next
-  case (snoc c s v)
-  have IH: "\<And>v. \<Turnstile> v : ders s r \<Longrightarrow> 
-     Some (flex r id s v) = decode (retrieve (bders (intern r) s) v) r" by fact
-  have asm: "\<Turnstile> v : ders (s @ [c]) r" by fact
-  then have asm2: "\<Turnstile> injval (ders s r) c v : ders s r" 
-    by (simp add: Prf_injval ders_append)
-  have "Some (flex r id (s @ [c]) v) = Some (flex r id s (injval (ders s r) c v))"
-    by (simp add: flex_append)
-  also have "... = decode (retrieve (bders (intern r) s) (injval (ders s r) c v)) r"
-    using asm2 IH by simp
-  also have "... = decode (retrieve (bder c (bders (intern r) s)) v) r"
-    using asm by (simp_all add: bder_retrieve ders_append)
-  finally show "Some (flex r id (s @ [c]) v) = 
-                 decode (retrieve (bders (intern r) (s @ [c])) v) r" by (simp add: bders_append)
-qed
-
-
-definition blex where
- "blex a s \<equiv> if bnullable (bders a s) then Some (bmkeps (bders a s)) else None"
-
-
-
-definition blexer where
- "blexer r s \<equiv> if bnullable (bders (intern r) s) then 
-                decode (bmkeps (bders (intern r) s)) r else None"
-
-lemma blexer_correctness:
-  shows "blexer r s = lexer r s"
-proof -
-  { define bds where "bds \<equiv> bders (intern r) s"
-    define ds  where "ds \<equiv> ders s r"
-    assume asm: "nullable ds"
-    have era: "erase bds = ds" 
-      unfolding ds_def bds_def by simp
-    have mke: "\<Turnstile> mkeps ds : ds"
-      using asm by (simp add: mkeps_nullable)
-    have "decode (bmkeps bds) r = decode (retrieve bds (mkeps ds)) r"
-      using bmkeps_retrieve
-      using asm era by (simp add: bmkeps_retrieve)
-    also have "... =  Some (flex r id s (mkeps ds))"
-      using mke by (simp_all add: MAIN_decode ds_def bds_def)
-    finally have "decode (bmkeps bds) r = Some (flex r id s (mkeps ds))" 
-      unfolding bds_def ds_def .
-  }
-  then show "blexer r s = lexer r s"
-    unfolding blexer_def lexer_flex
-    apply(subst bnullable_correctness[symmetric])
-    apply(simp)
-    done
-qed
 
 lemma asize0:
   shows "0 < asize r"
@@ -565,24 +423,27 @@
   apply(auto)
   done
 
-lemma bder_fuse:
-  shows "bder c (fuse bs a) = fuse bs (bder c a)"
-  apply(induct a arbitrary: bs c)
-  apply(simp_all)
-  done
-
-lemma bders_fuse:
-  shows "bders (fuse bs a) s = fuse bs (bders a s)"
-  apply(induct s arbitrary: bs a)
-   apply(simp_all)
-  by (simp add: bder_fuse)
-
-
-lemma map_bder_fuse:
-  shows "map (bder c \<circ> fuse bs1) as1 = map (fuse bs1) (map (bder c) as1)"
-  apply(induct as1)
-  apply(auto simp add: bder_fuse)
-  done
+lemma TESTTEST:
+  shows "bder c (intern r) = intern (der c r)"
+  apply(induct r)
+       apply(simp)
+      apply(simp)
+     apply(simp)
+    prefer 2
+    apply(simp)  
+    apply (simp add: bder_fuse[symmetric])
+  prefer 3
+   apply(simp only: intern.simps)
+   apply(simp only: der.simps)
+   apply(simp only: intern.simps)
+    apply(simp only: bder.simps)
+  apply(simp)
+   apply(simp only: intern.simps)
+   prefer 2
+   apply(simp)
+   prefer 2
+   apply(simp)
+  apply(auto)
 
 
 fun nonnested :: "arexp \<Rightarrow> bool"
@@ -671,6 +532,8 @@
 | "ASTAR bs r >> bs @ [S]"
 | "\<lbrakk>r >> bs1; ASTAR [] r >> bs2\<rbrakk> \<Longrightarrow> ASTAR bs r >> bs @ Z # bs1 @ bs2"
 
+
+
 lemma contains0:
   assumes "a >> bs"
   shows "(fuse bs1 a) >> bs1 @ bs"
@@ -899,6 +762,8 @@
   using Prf_flex assms contains6 contains7b by blast
 
 
+
+
 fun 
   bders_simp :: "arexp \<Rightarrow> string \<Rightarrow> arexp"
 where
@@ -2060,6 +1925,14 @@
    apply(auto)
   using contains0 by blast
 
+lemma test1:
+  shows "AALT [] (ACHAR [Z] c) (ACHAR [S] c) >> [S]"
+  by (metis contains.intros(2) contains.intros(4) contains.intros(5) self_append_conv2)
+
+lemma test1a:
+  shows "bsimp (AALT [] (ACHAR [Z] c) (ACHAR [S] c)) = AALT [] (ACHAR [Z] c) (ACHAR [S] c)"
+  apply(simp)
+  done
 
 lemma q3a:
   assumes "\<exists>r \<in> set rs. bnullable r"
@@ -3039,6 +2912,14 @@
   shows "bsimp r >> bs \<longleftrightarrow> r >> bs"
   using contains55 contains55a by blast
 
+
+definition "SET a \<equiv> {bs . a >> bs}"
+
+lemma "SET(bsimp a) \<subseteq> SET(a)"
+  unfolding SET_def
+  apply(auto simp add: PPP1_eq)
+  done
+
 lemma retrieve_code_bder:
   assumes "\<Turnstile> v : der c r"
   shows "code (injval r c v) = retrieve (bder c (intern r)) v"
@@ -3078,8 +2959,15 @@
 
 
 
+lemma PPP:
+  assumes "\<Turnstile> v : r"
+  shows "intern r >> (retrieve (intern r) v)"
+  using assms
+  using contains5 by blast
   
   
+ 
+  
   
   
 
@@ -3963,36 +3851,20 @@
 (* HERE *)
 
 lemma PX:
-  assumes "s \<in> L r" 
-  shows "bders (intern r) s >> code (PX r s) \<Longrightarrow> bders (bsimp (intern r)) s >> code (PX r s)"
-  
-  using FC_def contains7b
-  using assms by me tis
-
-
-
-  
-  apply(simp)
-  (*using FC_bders_iff2[of _ _ "[b]", simplified]*)
-  apply(subst (asm) FC_bders_iff2[of _ _ "[b]", simplified])
-  apply(simp)
-  apply(subst (asm) FC_bder_iff)
+  assumes "s \<in> L r" "bders (intern r) s >> code (PX r s)"
+  shows "bders (bsimp (intern r)) s >> code (PX r s)"
+  using assms
+  apply(induct s arbitrary: r rule: rev_induct)
    apply(simp)
-  apply(drule bder_simp_contains)
-  using FC_bder_iff FC_bders_iff2 FC_bders_iff
-  apply(subst (asm) FC_bder_iff[symmetric])
-   apply(subst FC_bder_iff)
-    using FC_bder_iff
-  
-  
-  apply (simp add: bder_simp_contains)
-
-lemma bder_simp_contains_IFF2:
-  assumes "bders r s >> bs"
-  shows ""
-  using assms
-  apply(induct s arbitrary: r bs rule: rev_induct)
-   apply(simp)
+   apply (simp add: PPP1_eq)
+  apply (simp add: bders_append bders_simp_append)
+  thm PX_bder_iff PX_bders_iff
+  apply(subst (asm) PX_bder_iff)
+   apply(assumption)
+  apply(subst (asm) (2) PX_bders_iff)
+  find_theorems "_ >> code (PX _ _)"
+  find_theorems "PX _ _ = _"
+  find_theorems "(intern _) >> _"
   apply (simp add: contains55)  
   apply (simp add: bders_append bders_simp_append)
    apply (simp add: PPP1_eq)