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