--- a/thys/BitCoded2.thy Sat Sep 14 13:25:56 2019 +0100
+++ b/thys/BitCoded2.thy Tue Sep 17 08:42:13 2019 +0100
@@ -566,11 +566,18 @@
done
lemma bder_fuse:
- shows "bder c (fuse bs a) = fuse bs (bder c a)"
+ 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)
@@ -1846,46 +1853,6 @@
by force
-lemma contains_ex1:
- assumes "a = AALTs bs1 [AZERO, AONE bs2]" "a >> bs"
- shows "bsimp a >> bs"
- using assms
- apply(simp)
- apply(erule contains.cases)
- apply(auto)
- using contains.simps apply blast
- apply(erule contains.cases)
- apply(auto)
- using contains0 apply fastforce
- using contains.simps by blast
-
-lemma contains_ex2:
- assumes "a = AALTs bs1 [AZERO, AONE bs2, AALTs bs5 [AONE bs3, AZERO, AONE bs4]]" "a >> bs"
- shows "bsimp a >> bs"
- using assms
- apply(simp)
- apply(erule contains.cases)
- apply(auto)
- using contains.simps apply blast
- apply(erule contains.cases)
- apply(auto)
- using contains3b apply blast
- apply(erule contains.cases)
- apply(auto)
- apply(erule contains.cases)
- apply(auto)
- apply (metis contains.intros(4) contains.intros(5) contains0 fuse.simps(2))
- apply(erule contains.cases)
- apply(auto)
- using contains.simps apply blast
- apply(erule contains.cases)
- apply(auto)
- apply (metis contains.intros(4) contains.intros(5) contains0 fuse.simps(2))
- apply(erule contains.cases)
- apply(auto)
-apply(erule contains.cases)
- apply(auto)
- done
lemma contains48:
assumes "\<And>x2aa bs bs1. \<lbrakk>x2aa \<in> set x2a; fuse bs x2aa >> bs @ bs1\<rbrakk> \<Longrightarrow> x2aa >> bs1"
@@ -1926,6 +1893,39 @@
using contains.intros(7) apply blast
using contains48 by blast
+
+lemma contains50_IFF2:
+ shows "bsimp_AALTs bs [a] >> bs @ bs1 \<longleftrightarrow> fuse bs a >> bs @ bs1"
+ by simp
+
+lemma contains50_IFF3:
+ shows "bsimp_AALTs bs as >> bs @ bs1 \<longleftrightarrow> (\<exists>a \<in> set as. fuse bs a >> bs @ bs1)"
+apply(induct as arbitrary: bs bs1)
+ apply(simp)
+ apply(auto elim: contains.cases simp add: contains0)
+ apply(case_tac as)
+ apply(auto)
+ apply(case_tac list)
+ apply(auto)
+ apply(erule contains.cases)
+ apply(auto)
+ apply (simp add: contains0)
+apply(erule contains.cases)
+ apply(auto)
+ using contains0 apply auto[1]
+ apply(erule contains.cases)
+ apply(auto)
+ apply(erule contains.cases)
+ apply(auto)
+ using contains0 apply blast
+ apply (metis bsimp_AALTs.simps(2) bsimp_AALTs.simps(3) contains.intros(4) contains49 list.exhaust)
+ by (smt bsimp_AALTs.simps(3) contains.intros(4) contains.intros(5) contains49 list.set_cases)
+
+lemma contains50_IFF4:
+ shows "bsimp_AALTs bs as >> bs @ bs1 \<longleftrightarrow> (\<exists>a \<in> set as. a >> bs1)"
+ by (meson contains0 contains49 contains50_IFF3)
+
+
lemma contains50:
assumes "bsimp_AALTs bs rs2 >> bs @ bs1"
shows "bsimp_AALTs bs (rs1 @ rs2) >> bs @ bs1"
@@ -1995,7 +1995,6 @@
apply(simp)
using contains51a by fastforce
-
lemma contains51c:
assumes "AALTs (bs @ bs2) rs >> bs @ bs1"
shows "bsimp_AALTs bs (map (fuse bs2) rs) >> bs @ bs1"
@@ -2642,6 +2641,15 @@
apply(simp)
done
+lemma bders_bsimp_AALTs:
+ shows "bders (bsimp_AALTs bs rs) s = bsimp_AALTs bs (map (\<lambda>a. bders a s) rs)"
+ apply(induct s arbitrary: bs rs rule: rev_induct)
+ apply(simp)
+ apply(simp add: bders_append)
+ apply(simp add: bder_bsimp_AALTs)
+ apply(simp add: comp_def)
+ done
+
lemma flts_nothing:
assumes "\<forall>r \<in> set rs. r \<noteq> AZERO" "\<forall>r \<in> set rs. nonalt r"
shows "flts rs = rs"
@@ -3088,6 +3096,7 @@
definition PX where
"PX r s = PV r s (mkeps (ders s r))"
+
lemma FE_PX:
shows "FE r s = retrieve r (PX (erase r) s)"
unfolding FE_def PX_def PV_def by(simp)
@@ -3298,6 +3307,14 @@
apply(simp)
done
+lemma FC_bders_iff2:
+ assumes "\<Turnstile> v : ders (c # s) (erase r)"
+ shows "bders r (c # s) >> FC r (c # s) v \<longleftrightarrow> bders (bder c r) s >> FC (bder c r) s v"
+ apply(subst FC_bders_iff)
+ using assms apply simp
+ by (metis FC_def assms contains7b contains8_iff ders.simps(2) erase_bder)
+
+
lemma FC_bnullable0:
assumes "bnullable r"
shows "FC r [] (mkeps (erase r)) = FC (bsimp r) [] (mkeps (erase (bsimp r)))"
@@ -3358,38 +3375,6 @@
shows "r >> FE (bsimp (bders r s)) []"
using FE_bnullable0 FE_contains2 assms by auto
-
-(*
-lemma FE_bnullable2:
- assumes "bnullable (bder c r)"
- shows "FE r [c] = FE (bsimp r) [c]"
- unfolding FE_def
- apply(simp)
- using L0
-
- apply(subst FE_nullable1)
- using assms apply(simp)
- apply(subst FE_bnullable0)
- using assms apply(simp)
- unfolding FE_def
- apply(simp)
- apply(subst L0)
- using assms apply(simp)
- apply(subst bder_retrieve[symmetric])
- using LLLL(1) L_erase_bder_simp assms bnullable_correctness mkeps_nullable nullable_correctness apply b last
- apply(simp)
- find_theorems "retrieve _ (injval _ _ _)"
- find_theorems "retrieve (bsimp _) _"
-
- lemma FE_nullable3:
- assumes "bnullable (bders a s)"
- shows "FE (bsimp a) s = FE a s"
-
- unfolding FE_def
- using LA assms bnullable_correctness mkeps_nullable by fas tforce
-*)
-
-
lemma FC4:
assumes "\<Turnstile> v : ders s (erase a)"
shows "FC a s v = FC (bders a s) [] v"
@@ -3402,92 +3387,6 @@
using L0 assms bnullable_correctness by auto
-lemma FC6:
- assumes "nullable (erase (bders a s))"
- shows "FC (bsimp a) s (mkeps (erase (bders (bsimp a) s))) = FC a s (mkeps (erase (bders a s)))"
- apply(subst (2) FC4)
- using assms mkeps_nullable apply auto[1]
- apply(subst FC_nullable2)
- using assms bnullable_correctness apply blast
- oops
-(*
-lemma FC_bnullable:
- assumes "bnullable (bders r s)"
- shows "FC r s (mkeps (erase r)) = FC (bsimp r) s (mkeps (erase (bsimp r)))"
- using assms
- unfolding FC_def
- using L0 L0a bder_retrieve L02_bders L04
-
- apply(induct s arbitrary: r)
- apply(simp add: FC_id)
- apply (simp add: L0 assms)
- apply(simp add: bders_append)
- apply(drule_tac x="bder a r" in meta_spec)
- apply(drule meta_mp)
- apply(simp)
-
- apply(subst bder_retrieve[symmetric])
- apply(simp)
-*)
-
-
-lemma FC_bnullable:
- assumes "bnullable (bders r s)"
- shows "FC r s (mkeps (ders s (erase r))) = FC (bsimp r) s (mkeps (ders s (erase (bsimp r))))"
- unfolding FC_def
- oops
-
-lemma AA0:
- assumes "bnullable (bders r s)"
- assumes "bders r s >> FC r s (mkeps (erase (bders r s)))"
- shows "bders (bsimp r) s >> FC (bsimp r) s (mkeps (erase (bders (bsimp r) s)))"
- using assms
- apply(subst (asm) FC_bders_iff)
- apply(simp)
- using bnullable_correctness mkeps_nullable apply fastforce
- apply(subst FC_bders_iff)
- apply(simp)
- apply (metis LLLL(1) bnullable_correctness ders_correctness erase_bders mkeps_nullable nullable_correctness)
- apply(simp add: PPP1_eq)
- unfolding FC_def
- find_theorems "retrieve (bsimp _) _"
- using contains7b
- oops
-
-
-lemma AA1:
-
- assumes "\<Turnstile> v : der c (erase r)" "\<Turnstile> v : der c (erase (bsimp r))"
- assumes "bder c r >> FC r [c] v"
- shows "bder c (bsimp r) >> FC (bsimp r) [c] v"
- using assms
- apply(subst (asm) FC_bder_iff)
- apply(rule assms)
- apply(subst FC_bder_iff)
- apply(rule assms)
- apply(simp add: PPP1_eq)
- unfolding FC_def
- find_theorems "retrieve (bsimp _) _"
- using contains7b
- oops
-
-
-lemma PX_bder_simp_iff:
- assumes "\<Turnstile> v: ders (s1 @ s2) r"
- shows "bders (bsimp (bders (intern r) s1)) s2 >> code (PV r (s1 @ s2) v) \<longleftrightarrow>
- bders (intern r) s1 >> code (PV r (s1 @ s2) v)"
- using assms
- apply(induct s2 arbitrary: r s1 v)
- apply(simp)
- apply (simp add: PV3 contains55)
- apply(drule_tac x="r" in meta_spec)
- apply(drule_tac x="s1 @ [a]" in meta_spec)
- apply(drule_tac x="v" in meta_spec)
- apply(simp)
- apply(simp add: bders_append)
- apply(subst (asm) PV_bder_IFF)
- oops
-
lemma in1:
assumes "AALTs bsX rsX \<in> set rs"
shows "\<forall>r \<in> set rsX. fuse bsX r \<in> set (flts rs)"
@@ -3644,16 +3543,7 @@
apply (metis AALTs_subs_fuse2 H7 UnCI fuse_map)
by (simp add: H7)
-(*
-lemma H8:
- assumes "AALTs_subs (AALTs bs (flts rs)) = AALTs_subs (AALTs bs rs)"
- shows "AALTs_subs (AALTs bs (flts rs)) = AALTs_subs (AALTs bs rs)"
- apply(induct rs arbitrary: bs rule: flts.induct)
- apply(auto)
- apply (metis AALTs_subs_fuse2 H7 Un_iff fuse_map)
- apply (metis AALTs_subs_fuse2 H7 UnCI fuse_map)
- by (simp add: H7)
-*)
+
lemma H2:
assumes "r >> bs2" "r \<in> AALTs_subs (AALTs bs rs)"
@@ -3729,126 +3619,129 @@
apply (simp add: H1 TEMPLATE_contains61a)
by (metis append_Cons append_Nil contains50 f_cont2)
-lemma HK1:
- assumes "r \<in> AALTs_subs a"
- shows "bsimp r \<in> AALTs_subs (bsimp a)"
- using assms
- apply(induct a arbitrary: r)
- apply(auto)
- apply(case_tac "a1 = AZERO")
- apply(simp)
- oops
-
lemma contains_equiv_def2:
shows " (AALTs bs as >> bs@bs1) \<longleftrightarrow> (\<exists>a\<in>(\<Union> (AALTs_subs ` set as)). a >> bs1)"
by (metis H1 H3 UN_E UN_I contains0 contains49 contains59 contains60)
lemma contains_equiv_def:
- shows " (AALTs bs as >> bs@bs1) \<longleftrightarrow> (\<exists>a\<in>set as. a >> bs1)"
+ shows "(AALTs bs as >> bs@bs1) \<longleftrightarrow> (\<exists>a\<in>set as. a >> bs1)"
by (meson contains0 contains49 contains59 contains60)
-lemma derc_alt00:
- assumes " bder c a >> bs" and "bder c (bsimp a) >> bs"
- shows "bder c (bsimp_AALTs [] (flts [bsimp a])) >> bs"
- using assms
- apply -
+lemma map_fuse2:
+ shows "map (bder c) (map (fuse bs) as) = map (fuse bs) (map (bder c) as)"
+ by (simp add: map_bder_fuse)
+
+lemma map_fuse3:
+ shows "map (\<lambda>a. bders a s) (map (fuse bs) as) = map (fuse bs) (map (\<lambda>a. bders a s) as)"
+ apply(induct s arbitrary: bs as rule: rev_induct)
+ apply(auto simp add: bders_append map_fuse2)
+ using bder_fuse by blast
+
+lemma bders_AALTs:
+ shows "bders (AALTs bs2 as) s = AALTs bs2 (map (\<lambda>a. bders a s) as)"
+ apply(induct s arbitrary: bs2 as rule: rev_induct)
+ apply(auto simp add: bders_append)
+ done
+
+lemma bders_AALTs_contains:
+ shows "bders (AALTs bs2 as) s >> bs2 @ bs \<longleftrightarrow>
+ AALTs bs2 (map (\<lambda>a. bders a s) as) >> bs2 @ bs"
+ apply(induct s arbitrary: bs bs2 as)
+ apply(auto)[1]
+ apply(simp)
+ by (smt comp_apply map_eq_conv)
+
+
+lemma derc_alt00_Urb:
+ shows "bder c (bsimp_AALTs bs2 (flts [bsimp a])) >> bs2 @ bs \<longleftrightarrow>
+ fuse bs2 (bder c (bsimp a)) >> bs2 @ bs"
apply(case_tac "bsimp a")
- prefer 6
- apply(simp)+
- apply(subst bder_bsimp_AALTs)
- by (metis append_Nil contains51c map_bder_fuse map_map)
-
-lemma derc_alt01:
- shows "\<And>a list1 list2.
- \<lbrakk> bder c (bsimp a) >> bs ;
- bder c a >> bs; as = [a] @ list2; flts (map bsimp list1) = [];
- flts (map bsimp list2) \<noteq> []\<rbrakk>
- \<Longrightarrow> bder c (bsimp_AALTs [] (flts [bsimp a] @ flts (map bsimp list2))) >> bs"
- using bder_bsimp_AALTs contains51b derc_alt00 f_cont2 by fastforce
-
-lemma derc_alt10:
- shows "\<And>a list1 list2.
- \<lbrakk> a \<in> set as; bder c (bsimp a) >> bs;
- bder c a >> bs; as = list1 @ [a] @ list2; flts (map bsimp list1) \<noteq> [];
-flts(map bsimp list2) = []\<rbrakk>
- \<Longrightarrow> bder c (bsimp_AALTs []
- (flts (map bsimp list1) @
- flts (map bsimp [a]) @ flts (map bsimp list2))) >> bs"
- apply(subst bder_bsimp_AALTs)
- apply simp
- using bder_bsimp_AALTs contains50 derc_alt00 f_cont2 by fastforce
-
-
-lemma derc_alt:
- assumes "bder c (AALTs [] as) >> bs"
- and "\<forall>a \<in> set as. ((bder c a >> bs) \<longrightarrow> (bder c (bsimp a) >> bs))"
- shows "bder c (bsimp (AALTs [] as)) >> bs"
+ apply(auto)
+ apply(subst (asm) bder_bsimp_AALTs)
+ apply(subst (asm) map_fuse2)
+ using contains60 contains61 contains63 apply blast
+ by (metis bder_bsimp_AALTs contains51c map_bder_fuse map_map)
+
+lemma ders_alt00_Urb:
+ shows "bders (bsimp_AALTs bs2 (flts [bsimp a])) s >> bs2 @ bs \<longleftrightarrow>
+ fuse bs2 (bders (bsimp a) s) >> bs2 @ bs"
+ apply(case_tac "bsimp a")
+ apply (simp add: bders_AZERO(1))
+ using bders_fuse bsimp_AALTs.simps(2) flts.simps(1) flts.simps(4) apply presburger
+ using bders_fuse bsimp_AALTs.simps(2) flts.simps(1) flts.simps(5) apply presburger
+ using bders_fuse bsimp_AALTs.simps(2) flts.simps(1) flts.simps(6) apply presburger
+ prefer 2
+ using bders_fuse bsimp_AALTs.simps(2) flts.simps(1) flts.simps(7) apply presburger
+ apply(auto simp add: bders_bsimp_AALTs)
+ apply(drule contains61)
+ apply(auto simp add: bders_AALTs)
+ apply(rule contains63)
+ apply(rule contains60)
+ apply(auto)
+ using bders_fuse apply auto[1]
+ by (metis contains51c map_fuse3 map_map)
+
+lemma derc_alt00_Urb2a:
+ shows "bder c (bsimp_AALTs bs2 (flts [bsimp a])) >> bs2 @ bs \<longleftrightarrow>
+ bder c (bsimp a) >> bs"
+ using contains0 contains49 derc_alt00_Urb by blast
+
+
+lemma derc_alt00_Urb2:
+ assumes "fuse bs2 (bder c (bsimp a)) >> bs2 @ bs" "a \<in> set as"
+ shows "bder c (bsimp_AALTs bs2 (flts (map bsimp as))) >> bs2 @ bs"
using assms
- apply -
- using contains_equiv_def
- apply -
- apply(simp)
- apply(drule_tac x="[]" in meta_spec)
- apply(drule_tac x="map (bder c) as" in meta_spec)
- apply(drule_tac x="bs" in meta_spec)
-
- apply(simp)
- apply(erule bexE)
apply(subgoal_tac "\<exists>list1 list2. as = list1 @ [a] @ list2")
prefer 2
using split_list_last apply fastforce
apply(erule exE)+
- apply(rule_tac t="as" and s="list1@[a]@list2" in subst)
- apply simp
- (*find_theorems "map _ _ = _"*)
- apply(subst map_append)+
- apply(subst k00)+
- apply(case_tac "flts (map bsimp list1) = Nil")
- apply(case_tac "flts (map bsimp list2) = Nil")
- apply simp
- using derc_alt00 apply blast
- apply simp
- using derc_alt01 apply blast
- apply(case_tac "flts (map bsimp list2) = Nil")
- using derc_alt10 apply blast
- by (smt bder_bsimp_AALTs contains50 contains51b derc_alt00 f_cont2 list.simps(8) list.simps(9) map_append)
-
-
+ apply(simp add: flts_append del: append.simps)
+ using bder_bsimp_AALTs contains50 contains51b derc_alt00_Urb by auto
+
+lemma ders_alt00_Urb2:
+ assumes "fuse bs2 (bders (bsimp a) s) >> bs2 @ bs" "a \<in> set as"
+ shows "bders (bsimp_AALTs bs2 (flts (map bsimp as))) s >> bs2 @ bs"
+ using assms
+ apply(subgoal_tac "\<exists>list1 list2. as = list1 @ [a] @ list2")
+ prefer 2
+ using split_list_last apply fastforce
+ apply(erule exE)+
+ apply(simp add: flts_append del: append.simps)
+ apply(simp add: bders_bsimp_AALTs)
+ apply(rule contains50)
+ apply(rule contains51b)
+ using bders_bsimp_AALTs ders_alt00_Urb by auto
+
+
lemma derc_alt2:
assumes "bder c (AALTs bs2 as) >> bs2 @ bs"
and "\<forall>a \<in> set as. ((bder c a >> bs) \<longrightarrow> (bder c (bsimp a) >> bs))"
shows "bder c (bsimp (AALTs bs2 as)) >> bs2 @ bs"
-proof -
- from assms
- have "bder c (AALTs [] as) >> bs"
- by (metis bder.simps(4) contains_equiv_def self_append_conv2)
- then have "bder c (bsimp (AALTs [] as)) >> bs"
- using assms(2) derc_alt by blast
- then show "bder c (bsimp (AALTs bs2 as)) >> bs2 @ bs"
- by (metis bder_fuse bsimp_fuse_AALTs contains0)
-qed
-
-lemma inA:
- assumes "x \<in> set rs" "bder c (bsimp x) >> bs"
- shows "\<exists>y. y \<in> set (flts (map bsimp rs))"
using assms
- apply(induct rs arbitrary: x c bs)
- apply(auto)
- apply(case_tac "bsimp a = AZERO")
- apply (metis append.left_neutral bder.simps(1) bsimp_AALTs.simps(1) contains61 in_set_conv_decomp neq_Nil_conv)
- apply (metis bsimp_AALTs.simps(1) flts4 good1 list.set_intros(1) neq_Nil_conv)
- by (metis Nil_is_append_conv k0 list.set_intros(1) neq_Nil_conv)
-
-
-lemma inB:
- assumes "a \<noteq> AZERO" "good a"
- shows "AALTs_subs a \<noteq> {}"
+ apply -
+ apply(simp)
+ apply(subst (asm) contains_equiv_def)
+ apply(simp)
+ apply(erule bexE)
+ using contains0 derc_alt00_Urb2 by blast
+
+
+
+lemma ders_alt2:
+ assumes "bders (AALTs bs2 as) s >> bs2 @ bs"
+ and "\<forall>a \<in> set as. ((bders a s >> bs) \<longrightarrow> (bders (bsimp a) s >> bs))"
+ shows "bders (bsimp (AALTs bs2 as)) s >> bs2 @ bs"
using assms
- apply(induct a)
- apply(auto)
- apply(erule good.elims)
- apply(auto)
- by (metis empty_iff good.simps(1) good_fuse nn11a nonalt_10)
+ apply -
+ apply(simp add: bders_AALTs)
+ thm contains_equiv_def
+ apply(subst (asm) contains_equiv_def)
+ apply(simp)
+ apply(erule bexE)
+ using contains0 ders_alt00_Urb2 by blast
+
+
+
lemma bder_simp_contains:
assumes "bder c a >> bs"
@@ -3930,34 +3823,217 @@
apply(rule derc_alt2[simplified])
apply(simp)
by blast
+
-lemma CONTAINS1:
- assumes "a >> bs"
- shows "a >>2 bs"
+
+lemma bder_simp_containsA:
+ assumes "bder c a >> bs"
+ shows "bsimp (bder c (bsimp a)) >> bs"
+ using assms
+ by (simp add: bder_simp_contains contains55)
+
+lemma bder_simp_containsB:
+ assumes "bsimp (bder c a) >> bs"
+ shows "bder c (bsimp a) >> bs"
+ using assms
+ by (simp add: PPP1_eq bder_simp_contains)
+
+lemma bder_simp_contains_IFF:
+ assumes "good a"
+ shows "bsimp (bder c a) >> bs \<longleftrightarrow> bder c (bsimp a) >> bs"
+ using assms
+ by (simp add: PPP1_eq test2)
+
+
+lemma ders_seq:
+ assumes "bders (ASEQ bs a1 a2) s >> bs @ bs2"
+ and "\<And>s bs. bders a1 s >> bs \<Longrightarrow> bders (bsimp a1) s >> bs"
+ "\<And>s bs. bders a2 s >> bs \<Longrightarrow> bders (bsimp a2) s >> bs"
+ shows "bders (ASEQ bs (bsimp a1) (bsimp a2)) s >> bs @ bs2"
+ using assms(1)
+ apply(induct s arbitrary: a1 a2 bs bs2 rule: rev_induct)
+ apply(auto)[1]
+ thm CT1_SEQ PPP1_eq
+ apply (metis CT1_SEQ PPP1_eq)
+ apply(auto simp add: bders_append)
+ apply(drule bder_simp_contains)
+ oops
+
+
+lemma bders_simp_contains:
+ assumes "bders a s >> bs"
+ shows "bders (bsimp a) s >> bs"
+ using assms
+ apply(induct a arbitrary: s bs)
+ apply(auto elim: contains.cases)[4]
+ prefer 2
+ apply(subgoal_tac "\<exists>bsX. bs = x1 @ bsX")
+ prefer 2
+ apply (metis bders_AALTs contains59 f_cont1)
+ apply(clarify)
+ apply(rule ders_alt2)
+ apply(assumption)
+ apply(auto)[1]
+ prefer 2
+ apply simp
+ (* SEQ case *)
+ apply(case_tac "bsimp a1 = AZERO")
+ apply(simp)
+ apply (metis LLLL(1) bders_AZERO(1) bsimp.simps(1) bsimp.simps(3) bsimp_ASEQ.simps(1) contains55 ders_correctness erase_bders good.simps(1) good1a xxx_bder2)
+ apply(case_tac "bsimp a2 = AZERO")
+ apply(simp)
+ apply (metis LLLL(1) bders_AZERO(1) bsimp.simps(1) bsimp.simps(3) bsimp_ASEQ0 contains55 ders_correctness erase_bders good.simps(1) good1a xxx_bder2)
+ apply(case_tac "\<exists>bsX. bsimp a1 = AONE bsX")
+ apply(auto)
+ apply(subst bsimp_ASEQ2)
+ apply(case_tac s)
+ apply(simp)
+ apply (metis b1 bsimp.simps(1) contains55)
+ apply(simp)
+ apply(subgoal_tac "bnullable a1")
+ prefer 2
+ using b3 apply fastforce
+ apply(auto)
+ apply(subst (asm) bders_AALTs)
+ apply(erule contains.cases)
+ apply(auto)
+ prefer 2
+ apply(erule contains.cases)
+ apply(auto)
+ apply(simp add: fuse_append)
+ apply(simp add: bder_fuse bders_fuse)
+apply (metis bders.simps(2) bmkeps.simps(1) bmkeps_simp contains0 contains49 f_cont1)
+ using contains_equiv_def apply auto[1]
+ apply(simp add: bder_fuse bders_fuse fuse_append)
+ apply(rule contains0)
+ oops
+
+
+lemma T0:
+ assumes "s = []"
+ shows "bders (bsimp r) s >> bs \<longleftrightarrow> bders r s >> bs"
+ using assms
+ by (simp add: PPP1_eq test2)
+
+lemma T1:
+ assumes "s = [a]" "bders r s >> bs"
+ shows "bders (bsimp r) s >> bs"
using assms
- apply(induct a bs)
- apply(auto intro: contains2.intros)
- done
-
-lemma CONTAINS2:
- assumes "a >>2 bs"
- shows "a >> bs"
+ apply(simp)
+ by (simp add: bder_simp_contains)
+
+lemma TX:
+ assumes "\<Turnstile> v : ders s (erase r)" "\<Turnstile> v : ders s (erase (bsimp r))"
+ shows "bders r s >> FC r s v \<longleftrightarrow> bders (bsimp r) s >> FC (bsimp r) s v"
+ using FC_def contains7b
+ using assms by metis
+
+lemma mkeps1:
+ assumes "s \<in> L (erase r)"
+ shows "\<Turnstile> mkeps (ders s (erase r)) : ders s (erase r)"
+ using assms
+ by (meson lexer_correct_None lexer_flex mkeps_nullable)
+
+lemma mkeps2:
+ assumes "s \<in> L (erase r)"
+ shows "\<Turnstile> mkeps (ders s (erase (bsimp r))) : ders s (erase (bsimp r))"
+ using assms
+ by (metis LLLL(1) lexer_correct_None lexer_flex mkeps_nullable)
+
+thm FC_def FE_def PX_def PV_def
+
+
+lemma TX2:
+ assumes "s \<in> L (erase r)"
+ shows "bders r s >> FE r s \<longleftrightarrow> bders (bsimp r) s >> FE (bsimp r) s"
+ using assms
+ by (simp add: FE_def contains7b mkeps1 mkeps2)
+
+lemma TX3:
+ assumes "s \<in> L (erase r)"
+ shows "bders r s >> FE r s \<longleftrightarrow> bders (bsimp r) s >> FE (bders (bsimp r) s) []"
using assms
- apply(induct a bs)
- apply(auto intro: contains.intros)
- using contains55 by auto
-
-lemma CONTAINS2_IFF:
- shows "a >> bs \<longleftrightarrow> a >>2 bs"
- using CONTAINS1 CONTAINS2 by blast
+ by (metis FE_PX FE_def L07 LLLL(1) PX_id TX2)
+
+find_theorems "FE _ _ = _"
+find_theorems "FC _ _ _ = _"
+find_theorems "(bder _ _ >> _ _ _ _) = _"
+
+
+(* 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)
+ 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: contains55)
+ apply (simp add: bders_append bders_simp_append)
+ apply (simp add: PPP1_eq)
+ find_theorems "(bder _ _ >> _) = _"
+ apply(rule contains50)
+
+ apply(case_tac "bders a xs = AZERO")
+ apply(simp)
+ apply(subgoal_tac "bders_simp a xs = AZERO")
+ prefer 2
+ apply (metis L_bders_simp XXX4a_good_cons bders.simps(1) bders_simp.simps(1) bsimp.simps(3) good.simps(1) good1a test2 xxx_bder2)
+ apply(simp)
+ apply(case_tac xs)
+ apply(simp)
+ apply (simp add: PPP1_eq)
+ apply(simp)
+ apply(subgoal_tac "good (bders_simp a (aa # list)) \<or> (bders_simp a (aa # list) = AZERO)")
+ apply(auto)
+ apply(subst (asm) bder_simp_contains_IFF)
+ apply(simp)
+
+
lemma
- assumes "bders (intern r) s >>2 bs"
- shows "bders_simp (intern r) s >>2 bs"
+ assumes "s \<in> L (erase r)"
+ shows "bders_simp r s >> bs \<longleftrightarrow> bders r s >> bs"
using assms
apply(induct s arbitrary: r bs)
apply(simp)
+ apply(simp add: bders_append bders_simp_append)
+ apply(rule iffI)
+ apply(drule_tac x="bsimp (bder a r)" in meta_spec)
+ apply(drule_tac x="bs" in meta_spec)
+ apply(drule meta_mp)
+ using L_bsimp_erase lexer_correct_None apply fastforce
apply(simp)
+
+
+ prefer 2
+
+
oops
@@ -4031,32 +4107,6 @@
using OO1a Posix1(1) contains55 by auto
-lemma OO22:
- assumes "[c1, c2] \<in> L r"
- shows "bders_simp (intern r) [c1, c2] >> code (PX r [c1, c2])"
- using assms
- apply(simp)
- apply(rule contains55)
- apply(rule Etrans)
- thm contains7
- apply(rule contains7)
- oops
-
-
-lemma contains70:
- assumes "s \<in> L(r)"
- shows "bders_simp (intern r) s >> code (flex r id s (mkeps (ders s r)))"
- using assms
- apply(induct s arbitrary: r rule: rev_induct)
- apply(simp)
- apply (simp add: contains2 mkeps_nullable nullable_correctness)
- apply(simp add: bders_simp_append flex_append)
- apply(simp add: PPP1_eq)
- apply(rule Etrans)
- apply(rule_tac v="flex r id xs (mkeps (ders (xs @ [x]) r))" in contains7)
- oops
-
-
thm L07XX PPP0b erase_intern
find_theorems "retrieve (bders _ _) _"