--- a/thys/BitCoded2.thy Mon Aug 19 16:24:28 2019 +0100
+++ b/thys/BitCoded2.thy Tue Aug 20 23:42:28 2019 +0200
@@ -641,6 +641,19 @@
| "bsimp (AALTs bs1 rs) = bsimp_AALTs bs1 (flts (map bsimp rs))"
| "bsimp r = r"
+
+inductive contains2 :: "arexp \<Rightarrow> bit list \<Rightarrow> bool" ("_ >>2 _" [51, 50] 50)
+ where
+ "AONE bs >>2 bs"
+| "ACHAR bs c >>2 bs"
+| "\<lbrakk>a1 >>2 bs1; a2 >>2 bs2\<rbrakk> \<Longrightarrow> ASEQ bs a1 a2 >>2 bs @ bs1 @ bs2"
+| "r >>2 bs1 \<Longrightarrow> AALTs bs (r#rs) >>2 bs @ bs1"
+| "AALTs bs rs >>2 bs @ bs1 \<Longrightarrow> AALTs bs (r#rs) >>2 bs @ bs1"
+| "ASTAR bs r >>2 bs @ [S]"
+| "\<lbrakk>r >>2 bs1; ASTAR [] r >>2 bs2\<rbrakk> \<Longrightarrow> ASTAR bs r >>2 bs @ Z # bs1 @ bs2"
+| "r >>2 bs \<Longrightarrow> (bsimp r) >>2 bs"
+
+
inductive contains :: "arexp \<Rightarrow> bit list \<Rightarrow> bool" ("_ >> _" [51, 50] 50)
where
"AONE bs >> bs"
@@ -678,6 +691,9 @@
done
+
+
+
lemma contains2:
assumes "\<Turnstile> v : r"
shows "(intern r) >> code v"
@@ -798,6 +814,7 @@
using contains2[OF assms] retrieve_code[OF assms]
by (simp)
+
lemma contains6:
assumes "\<Turnstile> v : (erase r)"
shows "r >> retrieve r v"
@@ -844,6 +861,37 @@
apply(simp)
done
+lemma contains7b:
+ assumes "\<Turnstile> v : ders s (erase r)"
+ shows "(bders r s) >> retrieve r (flex (erase r) id s v)"
+ using assms
+ apply(induct s arbitrary: r v)
+ apply(simp)
+ apply (simp add: contains6)
+ apply(simp add: bders_append flex_append ders_append)
+ apply(drule_tac x="bder a r" in meta_spec)
+ apply(drule meta_spec)
+ apply(drule meta_mp)
+ apply(simp)
+ apply(simp)
+ apply(subst (asm) bder_retrieve)
+ defer
+ apply (simp add: flex_injval)
+ by (simp add: Prf_flex)
+
+lemma contains7_iff:
+ assumes "\<Turnstile> v : der c (erase r)"
+ shows "(bder c r) >> retrieve r (injval (erase r) c v) \<longleftrightarrow>
+ r >> retrieve r (injval (erase r) c v)"
+ by (simp add: assms contains7 contains7a)
+
+lemma contains8_iff:
+ assumes "\<Turnstile> v : ders s (erase r)"
+ shows "(bders r s) >> retrieve r (flex (erase r) id s v) \<longleftrightarrow>
+ r >> retrieve r (flex (erase r) id s v)"
+ using Prf_flex assms contains6 contains7b by blast
+
+
fun
bders_simp :: "arexp \<Rightarrow> string \<Rightarrow> arexp"
where
@@ -1826,13 +1874,13 @@
apply(auto)
apply(erule contains.cases)
apply(auto)
- apply (metis append.left_neutral contains.intros(4) contains.intros(5) contains0 fuse.simps(2))
+ 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 append.left_neutral contains.intros(4) contains.intros(5) contains0 fuse.simps(2))
+ apply (metis contains.intros(4) contains.intros(5) contains0 fuse.simps(2))
apply(erule contains.cases)
apply(auto)
apply(erule contains.cases)
@@ -2354,7 +2402,7 @@
lemma L0:
assumes "bnullable a"
shows "retrieve (bsimp a) (mkeps (erase (bsimp a))) = retrieve a (mkeps (erase a))"
- using assms
+ using assms b3 bmkeps_retrieve bmkeps_simp bnullable_correctness
by (metis b3 bmkeps_retrieve bmkeps_simp bnullable_correctness)
thm bmkeps_retrieve
@@ -3013,8 +3061,6 @@
apply(simp)
done
-thm LA LB
-
lemma contains70:
assumes "s \<in> L(r)"
shows "bders (intern r) s >> code (flex r id s (mkeps (ders s r)))"
@@ -3024,6 +3070,17 @@
+
+
+
+
+
+
+definition FC where
+ "FC a s v = retrieve a (flex (erase a) id s v)"
+
+definition FE where
+ "FE a s = retrieve a (flex (erase a) id s (mkeps (ders s (erase a))))"
definition PV where
"PV r s v = flex r id s v"
@@ -3031,6 +3088,18 @@
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)
+
+lemma FE_PX_code:
+ assumes "s \<in> L r"
+ shows "FE (intern r) s = code (PX r s)"
+ unfolding FE_def PX_def PV_def
+ using assms
+ by (metis L07XX Posix_Prf erase_intern retrieve_code)
+
+
lemma PV_id[simp]:
shows "PV r [] v = v"
by (simp add: PV_def)
@@ -3129,6 +3198,7 @@
using assms
using PX_def PV_def contains70 by auto
+
lemma PV_bders_iff:
assumes "\<Turnstile> v : ders s r"
shows "bders (intern r) s >> code (PV r s v) \<longleftrightarrow> (intern r) >> code (PV r s v)"
@@ -3197,64 +3267,211 @@
bder c (intern r) >> code (PX r (c # s1))"
using PX2b PX3 assms by force
+
+lemma FC_id:
+ shows "FC r [] v = retrieve r v"
+ by (simp add: FC_def)
+
+lemma FC_char:
+ shows "FC r [c] v = retrieve r (injval (erase r) c v)"
+ by (simp add: FC_def)
+
+lemma FC_char2:
+ assumes "\<Turnstile> v : der c (erase r)"
+ shows "FC r [c] v = FC (bder c r) [] v"
+ using assms
+ by (simp add: FC_char FC_id bder_retrieve)
-
+
+lemma FC_bders_iff:
+ assumes "\<Turnstile> v : ders s (erase r)"
+ shows "bders r s >> FC r s v \<longleftrightarrow> r >> FC r s v"
+ unfolding FC_def
+ by (simp add: assms contains8_iff)
+
+
+lemma FC_bder_iff:
+ assumes "\<Turnstile> v : der c (erase r)"
+ shows "bder c r >> FC r [c] v \<longleftrightarrow> r >> FC r [c] v"
+ apply(subst FC_bders_iff[symmetric])
+ apply(simp add: assms)
+ apply(simp)
+ done
+
+lemma FC_bnullable0:
+ assumes "bnullable r"
+ shows "FC r [] (mkeps (erase r)) = FC (bsimp r) [] (mkeps (erase (bsimp r)))"
+ unfolding FC_def
+ by (simp add: L0 assms)
+
+
+lemma FC_nullable2:
+ assumes "bnullable (bders a s)"
+ shows "FC (bsimp a) s (mkeps (erase (bders (bsimp a) s))) =
+ FC (bders (bsimp a) s) [] (mkeps (erase (bders (bsimp a) s)))"
+ unfolding FC_def
+ using L02_bders assms by auto
+
+lemma FC_nullable3:
+ assumes "bnullable (bders a s)"
+ shows "FC a s (mkeps (erase (bders a s))) =
+ FC (bders a s) [] (mkeps (erase (bders a s)))"
+ unfolding FC_def
+ using LA assms bnullable_correctness mkeps_nullable by fastforce
+
+
+lemma FE_contains0:
+ assumes "bnullable r"
+ shows "r >> FE r []"
+ by (simp add: FE_def assms bnullable_correctness contains6 mkeps_nullable)
+
+lemma FE_contains1:
+ assumes "bnullable (bders r s)"
+ shows "r >> FE r s"
+ by (metis FE_def Prf_flex assms bnullable_correctness contains6 erase_bders mkeps_nullable)
+
+lemma FE_bnullable0:
+ assumes "bnullable r"
+ shows "FE r [] = FE (bsimp r) []"
+ unfolding FE_def
+ by (simp add: L0 assms)
+
+
+lemma FE_nullable1:
+ assumes "bnullable (bders r s)"
+ shows "FE r s = FE (bders r s) []"
+ unfolding FE_def
+ using LA assms bnullable_correctness mkeps_nullable by fastforce
+
+lemma FE_contains2:
+ assumes "bnullable (bders r s)"
+ shows "r >> FE (bders r s) []"
+ by (metis FE_contains1 FE_nullable1 assms)
+
+lemma FE_contains3:
+ assumes "bnullable (bder c r)"
+ shows "r >> FE (bsimp (bder c r)) []"
+ by (metis FE_def L0 assms bder_retrieve bders.simps(1) bnullable_correctness contains7a erase_bder erase_bders flex.simps(1) id_apply mkeps_nullable)
+
+lemma FE_contains4:
+ assumes "bnullable (bders r s)"
+ shows "r >> FE (bsimp (bders r s)) []"
+ using FE_bnullable0 FE_contains2 assms by auto
-
-definition EQ where
- "EQ a1 a2 \<equiv> (\<forall>bs. a1 >> bs \<longleftrightarrow> a2 >> bs)"
-
-lemma EQ1:
- assumes "EQ (intern r1) (intern r2)"
- "bders (intern r1) s >> code (PX r1 s)"
- "s \<in> L r1" "s \<in> L r2"
- shows "bders (intern r2) s >> code (PX r1 s)"
- using assms unfolding EQ_def
- thm PX_bders_iff
- apply(subst (asm) PX_bders_iff)
- apply(assumption)
- apply(subgoal_tac "intern r2 >> code (PX r1 s)")
- prefer 2
- apply(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"
+ unfolding FC_def by (simp add: LA assms)
+
+lemma FC5:
+ assumes "nullable (erase a)"
+ shows "FC a [] (mkeps (erase a)) = FC (bsimp a) [] (mkeps (erase (bsimp a)))"
+ unfolding FC_def
+ 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 "[c] \<in> L r"
- assumes "bder c (intern r) >> code (PX r [c])"
- shows "bder c (bsimp (intern r)) >> code (PX r [c])"
- using assms
-
- apply(induct a arbitrary: c bs1 bs2 rs)
- apply(auto elim: contains.cases)
- apply(case_tac "c = x2a")
- apply(simp)
- apply(case_tac rs)
- apply(auto)
- using contains0 apply fastforce
- apply(case_tac list)
- apply(auto)
- prefer 2
- apply(erule contains.cases)
- apply(auto)
-
-
-
-lemma TEST:
- assumes "bder c a >> bs"
- shows "bder c (bsimp a) >> bs"
+ 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(induct a arbitrary: c bs)
- apply(auto elim: contains.cases)
- prefer 2
- apply(erule contains.cases)
- apply(auto)
+ 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>
@@ -3269,9 +3486,183 @@
apply(simp)
apply(simp add: bders_append)
apply(subst (asm) PV_bder_IFF)
-
-definition EXs where
- "EXs a s \<equiv> \<forall>v \<in> \<lbrace>= v : ders s (erase a).
+ oops
+
+lemma in1:
+ assumes "AALTs bsX rsX \<in> set rs"
+ shows "\<forall>r \<in> set rsX. fuse bsX r \<in> set (flts rs)"
+ using assms
+ apply(induct rs arbitrary: bsX rsX)
+ apply(auto)
+ by (metis append_assoc in_set_conv_decomp k0)
+
+lemma in2a:
+ assumes "nonnested (bsimp r)" "\<not>nonalt(bsimp r)"
+ shows "(\<exists>bsX rsX. r = AALTs bsX rsX) \<or> (\<exists>bsX rX1 rX2. r = ASEQ bsX rX1 rX2 \<and> bnullable rX1)"
+ using assms
+ apply(induct r)
+ apply(auto)
+ by (metis arexp.distinct(25) b3 bnullable.simps(2) bsimp_ASEQ.simps(1) bsimp_ASEQ0 bsimp_ASEQ1 nonalt.elims(3) nonalt.simps(2))
+
+
+lemma in2:
+ assumes "bder c r >> bs2" and
+ "AALTs bsX rsX = bsimp r" and
+ "XX \<in> set rsX" "nonnested (bsimp r)"
+ shows "bder c (fuse bsX XX) >> bs2"
+ sorry
+
+
+lemma
+ assumes "bder c a >> bs"
+ shows "bder c (bsimp a) >> bs"
+ using assms
+ apply(induct a arbitrary: c bs)
+ apply(auto elim: contains.cases)
+ apply(case_tac "bnullable a1")
+ apply(simp)
+ prefer 2
+ apply(simp)
+ apply(erule contains.cases)
+ apply(auto)
+ apply(case_tac "(bsimp a1) = AZERO")
+ apply(simp)
+ apply (metis append_Nil2 contains0 contains49 fuse.simps(1))
+ apply(case_tac "(bsimp a2a) = AZERO")
+ apply(simp)
+ apply (metis bder.simps(1) bsimp.simps(1) bsimp_ASEQ0 contains.intros(3) contains55)
+ apply(case_tac "\<exists>bsX. (bsimp a1) = AONE bsX")
+ apply(auto)[1]
+ using b3 apply fastforce
+ apply(subst bsimp_ASEQ1)
+ apply(auto)[3]
+ apply(simp)
+ apply(subgoal_tac "\<not> bnullable (bsimp a1)")
+ prefer 2
+ using b3 apply blast
+ apply(simp)
+ apply (simp add: contains.intros(3) contains55)
+ (* SEQ nullable case *)
+ apply(erule contains.cases)
+ apply(auto)
+ apply(erule contains.cases)
+ apply(auto)
+ apply(case_tac "(bsimp a1) = AZERO")
+ apply(simp)
+ apply (metis append_Nil2 contains0 contains49 fuse.simps(1))
+ apply(case_tac "(bsimp a2a) = AZERO")
+ apply(simp)
+ apply (metis bder.simps(1) bsimp.simps(1) bsimp_ASEQ0 contains.intros(3) contains55)
+ apply(case_tac "\<exists>bsX. (bsimp a1) = AONE bsX")
+ apply(auto)[1]
+ using contains.simps apply blast
+ apply(subst bsimp_ASEQ1)
+ apply(auto)[3]
+ apply(simp)
+ apply(subgoal_tac "bnullable (bsimp a1)")
+ prefer 2
+ using b3 apply blast
+ apply(simp)
+ apply (metis contains.intros(3) contains.intros(4) contains55 self_append_conv2)
+ apply(erule contains.cases)
+ apply(auto)
+ apply(case_tac "(bsimp a1) = AZERO")
+ apply(simp)
+ using b3 apply force
+ apply(case_tac "(bsimp a2) = AZERO")
+ apply(simp)
+ apply (metis bder.simps(1) bsimp_ASEQ0 bsimp_ASEQ_fuse contains0 contains49 f_cont1)
+ apply(case_tac "\<exists>bsX. (bsimp a1) = AONE bsX")
+ apply(auto)[1]
+ apply (metis append_assoc bder_fuse bmkeps.simps(1) bmkeps_simp bsimp_ASEQ2 contains0 contains49 f_cont1)
+ apply(subst bsimp_ASEQ1)
+ apply(auto)[3]
+ apply(simp)
+ apply(subgoal_tac "bnullable (bsimp a1)")
+ prefer 2
+ using b3 apply blast
+ apply(simp)
+ apply (metis bmkeps_simp contains.intros(4) contains.intros(5) contains0 contains49 f_cont1)
+ apply(erule contains.cases)
+ apply(auto)
+ (* ALT case *)
+ apply(drule contains59)
+ apply(auto)
+ apply(subst bder_bsimp_AALTs)
+ apply(rule contains61a)
+ apply(auto)
+ apply(subgoal_tac "bsimp r \<in> set (map bsimp x2a)")
+ prefer 2
+ apply simp
+ apply(case_tac "bsimp r = AZERO")
+ apply (metis Nil_is_append_conv bder.simps(1) bsimp_AALTs.elims bsimp_AALTs.simps(2) contains49 contains61 f_cont2 list.distinct(1) split_list_last)
+ apply(subgoal_tac "nonnested (bsimp r)")
+ prefer 2
+ using nn1b apply blast
+ apply(case_tac "nonalt (bsimp r)")
+ apply(rule_tac x="bsimp r" in bexI)
+ apply (metis contains0 contains49 f_cont1)
+ apply (metis append_Cons flts_append in_set_conv_decomp k0 k0b)
+ (* AALTS case *)
+ apply(subgoal_tac "\<exists>rsX bsX. (bsimp r) = AALTs bsX rsX \<and> (\<forall>r \<in> set rsX. nonalt r)")
+ prefer 2
+ apply (metis n0 nonalt.elims(3))
+ apply(auto)
+ apply(subgoal_tac "bsimp r \<in> set (map bsimp x2a)")
+ prefer 2
+ apply (metis imageI list.set_map)
+ apply(simp)
+ apply(simp add: image_def)
+ apply(erule bexE)
+ apply(subgoal_tac "AALTs bsX rsX \<in> set (map bsimp x2a)")
+ prefer 2
+ apply simp
+ apply(drule in1)
+ apply(subgoal_tac "rsX \<noteq> []")
+ prefer 2
+ apply (metis arexp.distinct(7) good.simps(4) good1)
+ apply(subgoal_tac "\<exists>XX. XX \<in> set rsX")
+ prefer 2
+ using neq_Nil_conv apply fastforce
+ apply(erule exE)
+ apply(rule_tac x="fuse bsX XX" in bexI)
+ prefer 2
+ apply blast
+ apply(frule f_cont1)
+ apply(auto)
+ apply(rule contains0)
+ apply(drule contains49)
+ by (simp add: in2)
+
+lemma CONTAINS1:
+ assumes "a >> bs"
+ shows "a >>2 bs"
+ using assms
+ apply(induct a bs)
+ apply(auto intro: contains2.intros)
+ done
+
+lemma CONTAINS2:
+ assumes "a >>2 bs"
+ shows "a >> bs"
+ 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
+
+lemma
+ assumes "bders (intern r) s >>2 bs"
+ shows "bders_simp (intern r) s >>2 bs"
+ using assms
+ apply(induct s arbitrary: r bs)
+ apply(simp)
+ apply(simp)
+ oops
+
lemma
assumes "s \<in> L r"
@@ -3286,7 +3677,7 @@
find_theorems "retrieve (bders _ _) _"
find_theorems "_ >> retrieve _ _"
find_theorems "bsimp _ >> _"
-
+ oops
lemma PX4a:
@@ -3311,49 +3702,6 @@
find_theorems "bder _ _ >> _"
-
-lemma PV6:
- assumes "s @[c] \<in> L r"
- shows"bder s1 (bders (intern r) s2) >> code (PX r (c # s))"
- apply(subst PX_bders_iff)
- apply(rule contains7)
- apply(simp)
- apply(rule assms)
- apply(subst retrieve_code)
-
- apply(simp add: PV_def)
- apply(simp)
- apply(drule_tac x="r" in meta_spec)
- apply(drule_tac x="s1 @ [a]" in meta_spec)
- apply(simp add: bders_append)
- apply(subst PV_cons)
- apply(drule_tac x="injval r a v" in meta_spec)
- apply(drule meta_mp)
-
-
-lemma PV8:
- assumes "(s1 @ s2) \<in> L r"
- shows "bders (bders_simp (intern r) s1) s2 >> code (PX r (s1 @ s2))"
- using assms
- apply(induct s1 arbitrary: r s2 rule: rev_induct)
- apply(simp add: PX3)
- apply(simp)
- apply(simp add: bders_simp_append)
- apply(drule_tac x="r" in meta_spec)
- apply(drule_tac x="x # s2" in meta_spec)
- apply(simp add: bders_simp_append)
- apply(rule iffI)
- defer
-
- apply(simp add: PX_append)
- apply(simp add: bders_append)
-
-lemma PV6:
- assumes "\<Turnstile> v : ders s r"
- shows "bders (intern r) s >> code (PV r s v)"
- using assms
- by (simp add: PV_def contains6 retrieve_code_bders)
-
lemma OO0_PX:
assumes "s \<in> L r"
shows "bders (intern r) s >> code (PX r s)"
@@ -3395,7 +3743,7 @@
apply(rule Etrans)
thm contains7
apply(rule contains7)
-
+ oops
lemma contains70:
@@ -3409,7 +3757,7 @@
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
@@ -3419,560 +3767,6 @@
find_theorems "bder _ _ >> _"
-proof -
- from assms have "\<Turnstile> v : erase (bder c r)" by simp
- then have "bder c r >> retrieve (bder c r) v"
- by (simp add: contains6)
- moreover have "retrieve (bder c r) v = retrieve r (injval (erase r) c v)"
- using assms bder_retrieve by blast
- ultimately have "bder c r >> code (injval (erase r) c v)"
- apply -
- apply(subst retrieve_code_bder)
- apply(simp add: assms)
- oops
-
-find_theorems "code _ = retrieve _ _"
-find_theorems "_ >> retrieve _ _"
-find_theorems "bder _ _ >> _"
-
-lemma
- assumes "s \<in> r \<rightarrow> v" "s = [c1, c2]"
- shows "bders_simp (intern r) s >> bs \<longleftrightarrow> bders (intern r) s >> bs"
- using assms
- apply(simp add: PPP1_eq)
-
-
-
-lemma PPP10:
- assumes "s \<in> r \<rightarrow> v"
- shows "bders_simp (intern r) s >> retrieve (intern r) v \<longleftrightarrow> bders (intern r) s >> retrieve (intern r) v"
- using assms
- apply(induct s arbitrary: r v rule: rev_induct)
- apply(auto)
- apply(simp_all add: PPP1_eq bders_append bders_simp_append)
-
- find_theorems "bder _ _ >> _"
-
-lemma
- shows "bder
-
-
-find_theorems "bsimp _ >> _"
-
-fun get where
- "get (Some v) = v"
-
-
-lemma decode9:
- assumes "decode' bs (STAR r) = (v, bsX)" "bs \<noteq> []"
- shows "\<exists>vs. v = Stars vs"
- using assms
- apply(induct bs\<equiv>"bs" r\<equiv>"STAR r" arbitrary: bs r v bsX rule: decode'.induct)
- apply(auto)
- apply(case_tac "decode' ds r")
- apply(auto)
- apply(case_tac "decode' b (STAR r)")
- apply(auto)
- apply(case_tac aa)
- apply(auto)
- done
-
-lemma decode10_Stars:
- assumes "decode' bs (STAR r) = (Stars vs, bs1)" "\<Turnstile> Stars vs : (STAR r)" "vs \<noteq> []"
- shows "decode' (bs @ bsX) (STAR r) = (Stars vs, bs1 @ bsX)"
- using assms
- apply(induct vs arbitrary: bs r bs1 bsX)
- apply(auto elim!: Prf_elims)
- apply(case_tac vs)
- apply(auto)
- apply(case_tac bs)
- apply(auto)
- apply(case_tac aa)
- apply(auto)
- apply(case_tac "decode' list r")
- apply(auto)
- apply(case_tac "decode' b (STAR r)")
- apply(auto)
- apply(case_tac "decode' (list @ bsX) r")
- apply(auto)
- apply(case_tac "decode' ba (STAR r)")
- apply(auto)
- apply(case_tac ba)
- apply(auto)
- oops
-
-lemma decode10:
- assumes "decode' bs r = (v, bs1)" "\<Turnstile> v : r"
- shows "decode' (bs @ bsX) r = (v, bs1 @ bsX)"
- using assms
- apply(induct bs r arbitrary: v bs1 bsX rule: decode'.induct)
- apply(auto elim: Prf_elims)[7]
- apply(case_tac "decode' ds r1")
- apply(auto)[3]
- apply(case_tac "decode' (ds @ bsX) r1")
- apply(auto)[3]
- apply(auto elim: Prf_elims)[4]
- apply(case_tac "decode' ds r2")
- apply(auto)[1]
- apply(case_tac "decode' (ds @ bsX) r2")
- apply(auto)[1]
- apply(auto elim: Prf_elims)[2]
- apply(case_tac "decode' ds r1")
- apply(auto)[1]
- apply(case_tac "decode' b r2")
- apply(auto)[1]
- apply(auto elim: Prf_elims)[1]
- apply(auto elim: Prf_elims)[1]
- apply(auto elim: Prf_elims)[1]
- apply(erule Prf_elims)
-(* STAR case *)
- apply(auto)
- apply(case_tac "decode' ds r")
- apply(auto)
- apply(case_tac "decode' b (STAR r)")
- apply(auto)
- apply(case_tac aa)
- apply(auto)
- apply(case_tac "decode' (b @ bsX) (STAR r)")
- apply(auto)
- oops
-
-
-lemma contains100:
- assumes "(intern r) >> bs"
- shows "\<exists>v bsV. decode' bs r = (v, bsV) \<and> \<Turnstile> v : r"
- using assms
- apply(induct r arbitrary: bs)
- apply(auto)
-apply(erule contains.cases)
- apply(auto)
- apply(erule contains.cases)
- apply(auto intro: Prf.intros)
-apply(erule contains.cases)
- apply(auto)
- apply(drule_tac x="bs1" in meta_spec)
- apply(drule_tac x="bs2" in meta_spec)
- apply(auto)[1]
- apply(rule_tac x="Seq v va" in exI)
- apply(auto)
- apply(case_tac "decode' (bs1 @ bs2) r1")
- apply(auto)
- apply(case_tac "decode' b r2")
- apply(auto)
- oops
-
-lemma contains101:
- assumes "(intern r) >> code v"
- shows "\<Turnstile> v : r"
- using assms
- apply(induct r arbitrary: v)
- apply(auto elim: contains.cases)
- apply(erule contains.cases)
- apply(auto)
- apply(case_tac v)
- apply(auto intro: Prf.intros)
- apply(erule contains.cases)
- apply(auto)
- apply(case_tac v)
- apply(auto intro: Prf.intros)
-
-(*
- using contains.simps apply blast
- apply(erule contains.cases)
- apply(auto)
- using L1 Posix_ONE Prf.intros(4) apply force
- apply(erule contains.cases)
- apply(auto)
- apply (metis Prf.intros(5) code.simps(2) decode_code get.simps)
- apply(erule contains.cases)
- apply(auto)
- prefer 2
- apply(erule contains.cases)
- apply(auto)
- apply(frule f_cont1)
- apply(auto)
- apply(case_tac "decode' bs2 r1")
- apply(auto)
- apply(rule Prf.intros)
- apply (metis Cons_eq_append_conv contains49 f_cont1 fst_conv list.inject self_append_conv2)
- apply(erule contains.cases)
- apply(auto)
- apply(frule f_cont1)
- apply(auto)
- apply(case_tac "decode' bs2 r2")
- apply(auto)
- apply(rule Prf.intros)
- apply (metis (full_types) append_Cons contains49 append_Nil fst_conv)
- apply(erule contains.cases)
- apply(auto)
- apply(case_tac "decode' (bs1 @ bs2) r1")
- apply(auto)
- apply(case_tac "decode' b r2")
- apply(auto)
- apply(rule Prf.intros)
-
- apply (metis fst_conv)
- apply(subgoal_tac "b = bs2 @ bsX")
- apply(auto)
- apply (metis fst_conv)
- apply(subgoal_tac "decode' (bs1 @ bs2 @ bsX) r1 = (a, bs2 @ bsX)")
- apply simp
-*)
-
-
- apply(case_tac ba)
- apply(auto)
- apply(drule meta_spec)
- apply(drule meta_mp)
- apply(assumption)
- prefer 2
-
-
- apply(case_tac v)
- apply(auto)
-
-
-
-find_theorems "bder _ _ >> _"
-
-lemma PPP0_isar:
- assumes "bders r s >> code v"
- shows "bders_simp r s >> code v"
- using assms
- apply(induct s arbitrary: r v)
- apply(simp)
- apply(auto)
- apply(drule_tac x="bsimp (bder a r)" in meta_spec)
- apply(drule_tac x="v" in meta_spec)
- apply(drule_tac meta_mp)
-
- prefer 2
- apply(simp)
-
- using bnullable_correctness nullable_correctness apply fastforce
- apply(simp add: bders_append)
-
-
-
-
-
-lemma PPP0_isar:
- assumes "s \<in> r \<rightarrow> v"
- shows "(bders (intern r) s) >> code v"
-proof -
- from assms have a1: "\<Turnstile> v : r" using Posix_Prf by simp
-
- from assms have "s \<in> L r" using Posix1(1) by auto
- then have "[] \<in> L (ders s r)" by (simp add: ders_correctness Ders_def)
- then have a2: "\<Turnstile> mkeps (ders s r) : ders s r"
- by (simp add: mkeps_nullable nullable_correctness)
-
- have "retrieve (bders (intern r) s) (mkeps (ders s r)) =
- retrieve (intern r) (flex r id s (mkeps (ders s r)))" using a2 LA by simp
- also have "... = retrieve (intern r) v"
- using LB assms by auto
- also have "... = code v" using a1 by (simp add: retrieve_code)
- finally have "retrieve (bders (intern r) s) (mkeps (ders s r)) = code v" by simp
- moreover
- have "\<Turnstile> mkeps (ders s r) : erase (bders (intern r) s)" using a2 by simp
- then have "bders (intern r) s >> retrieve (bders (intern r) s) (mkeps (ders s r))"
- by (rule contains6)
- ultimately
- show "(bders (intern r) s) >> code v" by simp
-qed
-
-
-
-
-
-
-
-
-
-lemma A0:
- assumes "r \<in> set (flts rs)"
- shows "r \<in> set rs"
- using assms
- apply(induct rs arbitrary: r rule: flts.induct)
- apply(auto)
- oops
-
-lemma A1:
- assumes "r \<in> set (flts (map (bder c) (flts rs)))" "\<forall>r \<in> set rs. nonnested r \<and> good r"
- shows "r \<in> set (flts (map (bder c) rs))"
- using assms
- apply(induct rs arbitrary: r c rule: flts.induct)
- apply(auto)
- apply(subst (asm) map_bder_fuse)
- apply(simp add: flts_append)
- apply(auto)
- apply(auto simp add: comp_def)
- apply(subgoal_tac "\<forall>r \<in> set rs1. nonalt r \<and> good r")
- prefer 2
- apply (metis Nil_is_append_conv good.simps(5) good.simps(6) in_set_conv_decomp neq_Nil_conv)
- apply(case_tac rs1)
- apply(auto)
- apply(subst (asm) k0)
- apply(auto)
-
- oops
-
-
-lemma bsimp_comm2:
- assumes "bder c a >> bs"
- shows "bder c (bsimp a) >> bs"
- using assms
- apply(induct a arbitrary: bs c taking: "asize" rule: measure_induct)
- apply(case_tac x)
- apply(auto)
- prefer 2
- apply(erule contains.cases)
- apply(auto)
- apply(subst bder_bsimp_AALTs)
- apply(rule contains61a)
- apply(rule bexI)
- apply(rule contains0)
- apply(assumption)
-
-
-lemma bsimp_comm:
- assumes "bder c (bsimp a) >> bs"
- shows "bsimp (bder c a) >> bs"
- using assms
- apply(induct a arbitrary: bs c taking: "asize" rule: measure_induct)
- apply(case_tac x)
- apply(auto)
- prefer 4
- apply(erule contains.cases)
- apply(auto)
- using contains.intros(3) contains55 apply fastforce
- prefer 3
- apply(subst (asm) bder_bsimp_AALTs)
- apply(drule contains61b)
- apply(auto)
- apply(rule contains61a)
- apply(rule bexI)
- apply(assumption)
- apply(rule_tac t="set (flts (map (bsimp \<circ> bder c) x52))"
- and s="set (flts (map (bder c \<circ> bsimp) x52))" in subst)
- prefer 2
- find_theorems "map (_ \<circ> _) _ = _"
- apply(simp add: comp_def)
-
-
- find_theorems "bder _ (bsimp_AALTs _ _) = _"
- apply(drule contains_SEQ1)
- apply(auto)[1]
- apply(rule contains.intros)
- prefer 2
- apply(assumption)
-
-
- apply(case_tac "bnullable x42")
- apply(simp)
- prefer 2
- apply(simp)
- apply(case_tac "bsimp x42 = AZERO")
- apply (me tis L_erase_bder_simp bder.simps(1) bsimp.simps(3) bsimp_ASEQ.simps(1) good.simps(1) good1a xxx_bder2)
- apply(case_tac "bsimp x43 = AZERO")
- apply (simp add: bsimp_ASEQ0)
- apply(case_tac "\<exists>bs1. bsimp x42 = AONE bs1")
- using b3 apply force
- apply(subst bsimp_ASEQ1)
- apply(auto)[3]
- apply(auto)[1]
- using b3 apply blast
- apply(case_tac "bsimp (bder c x42) = AZERO")
- apply(simp)
- using contains.simps apply blast
- apply(case_tac "\<exists>bs2. bsimp (bder c x42) = AONE bs2")
- apply(auto)[1]
- apply(subst (asm) bsimp_ASEQ2)
- apply(subgoal_tac "\<exists>bsX. bs = x41 @ bs2 @ bsX")
- apply(auto)[1]
- apply(rule contains.intros)
- apply (simp add: contains.intros(1))
- apply (metis append_assoc contains49)
- using append_assoc f_cont1 apply blast
- apply(subst (asm) bsimp_ASEQ1)
- apply(auto)[3]
- apply(erule contains.cases)
- apply(auto)
- using contains.intros(3) less_add_Suc1 apply blast
- apply(case_tac "bsimp x42 = AZERO")
- using b3 apply force
- apply(case_tac "bsimp x43 = AZERO")
- apply (metis LLLL(1) L_erase_bder_simp bder.simps(1) bsimp_AALTs.simps(1) bsimp_ASEQ0 bsimp_fuse flts.simps(1) flts.simps(2) fuse.simps(1) good.simps(1) good1a xxx_bder2)
- apply(case_tac "\<exists>bs1. bsimp x42 = AONE bs1")
- apply(auto)[1]
- apply(subst bsimp_ASEQ2)
- apply(drule_tac x="fuse (x41 @ bs1) x43" in spec)
- apply(drule mp)
- apply (simp add: asize_fuse)
- apply(drule_tac x="bs" in spec)
- apply(drule_tac x="c" in spec)
- apply(drule mp)
- prefer 2
- apply (simp add: bsimp_fuse)
- apply(subst (asm) k0)
- apply(subgoal_tac "\<exists>bsX. bs = x41 @ bsX")
- prefer 2
- using f_cont2 apply blast
- apply(clarify)
- apply(drule contains62)
- apply(auto)[1]
- apply(case_tac "bsimp (bder c x42) = AZERO")
- apply (metis append_is_Nil_conv bsimp_ASEQ.simps(1) contains61 flts.simps(1) flts.simps(2) in_set_conv_decomp list.distinct(1))
- apply(case_tac "\<exists>bsX. bsimp (bder c x42) = AONE bsX")
- apply(clarify)
- apply (simp add: L_erase_bder_simp xxx_bder2)
- using L_erase_bder_simp xxx_bder2 apply auto[1]
- apply(drule contains65)
- apply(auto)[1]
- apply (simp add: bder_fuse bmkeps_simp bsimp_fuse fuse_append)
- apply(subst bsimp_ASEQ1)
- apply(auto)[3]
- apply(auto)[1]
- apply(case_tac "bsimp (bder c x42) = AZERO")
- apply(simp add: bsimp_ASEQ0)
- apply(drule contains65)
- apply(auto)[1]
- apply (metis asize_fuse bder_fuse bmkeps_simp bsimp_fuse contains.intros(4) contains.intros(5) contains49 f_cont1 less_add_Suc2)
-
- apply(frule f_cont1)
- apply(auto)
-
- apply(case_tac "\<exists>bsX. bsimp (bder c x42) = AONE bsX")
- apply(auto)[1]
- apply(subst (asm) bsimp_ASEQ2)
- apply(auto)
- apply(drule contains65)
- apply(auto)[1]
- apply(frule f_cont1)
- apply(auto)
- apply(rule contains.intros)
- apply (metis (no_types, lifting) append_Nil2 append_eq_append_conv2 contains.intros(1) contains.intros(3) contains49 f_cont1 less_add_Suc1 same_append_eq)
- apply(frule f_cont1)
- apply(auto)
- apply(rule contains.intros)
- apply(drule contains49)
- apply(subst (asm) bsimp_fuse[symmetric])
- apply(frule f_cont1)
- apply(auto)
- apply(subst (3) append_Nil[symmetric])
- apply(rule contains.intros)
- apply(drule contains49)
-
- prefer 2
-
- apply(simp)
- find_theorems "fuse _ _ >> _"
-
-
- apply(erule contains.cases)
- apply(auto)
-
-
-
-
-
-
-
-
-
-thm bder_retrieve
-find_theorems "_ >> retrieve _ _"
-
-lemma TEST:
- assumes "\<Turnstile> v : ders s (erase r)"
- shows "bders r s >> retrieve r (flex (erase r) id s v)"
- using assms
- apply(induct s arbitrary: v r rule: rev_induct)
- apply(simp)
- apply (simp add: contains6)
- apply(simp add: bders_append ders_append)
- apply(rule Etrans)
- apply(rule contains7)
- apply(simp)
- by (metis LA bder_retrieve bders_snoc ders_snoc erase_bders)
-
-
-lemma TEST1:
- assumes "bder c r >> retrieve r (injval (erase r) c v)"
- shows "r >> retrieve r v"
- oops
-
-lemma TEST2:
- assumes "bders (intern r) s >> retrieve (intern r) (flex r id s (mkeps (ders s r)))" "s = [c1, c2]"
- shows "bders_simp (intern r) s >> retrieve (intern r) (flex r id s (mkeps (ders s r)))"
- using assms
- apply(simp)
-
-
- apply(induct s arbitrary: r rule: rev_induct)
- apply(simp)
- apply(simp add: bders_simp_append ders_append flex_append bders_append)
- apply(rule contains55)
-
- apply(drule_tac x="bsimp (bder a r)" in meta_spec)
- thm L02_bders
- apply(subst L02_bders)
- find_theorems "retrieve (bsimp _) _ = _"
- apply(drule_tac "" in Etrans)
-
-lemma TEST2:
- assumes "bders r s >> retrieve r (flex (erase r) id s (mkeps (ders s (erase r))))"
- shows "bders_simp r s >> retrieve r (flex (erase r) id s (mkeps (ders s (erase r))))"
- using assms
- apply(induct s arbitrary: r rule: rev_induct)
- apply(simp)
- apply(simp add: bders_simp_append ders_append flex_append bders_append)
- apply(subgoal_tac "bder x (bders r xs) >> retrieve r (flex (erase r) id xs (injval (ders xs (erase r)) x (mkeps (ders xs (erase r)))))")
- find_theorems "bders _ _ >> _"
- apply(drule_tac x="bsimp (bder a r)" in meta_spec)
- thm L02_bders
- apply(subst L02_bders)
- find_theorems "retrieve (bsimp _) _ = _"
- apply(drule_tac "" in Etrans)
- apply(rule contains55)
- apply(rule Etrans)
- apply(rule contains7)
- apply(subgoal_tac "\<Turnstile> v : der x (erase (bders_simp r xs))")
- apply(assumption)
- prefer 2
-
-
- apply(simp)
- by (m etis LA bder_retrieve bders_snoc ders_snoc erase_bders)
-
-
-
-
-lemma PPP0A:
- assumes "s \<in> L (r)"
- shows "(bders (intern r) s) >> code (flex r id s (mkeps (ders s r)))"
- using assms
- by (metis L07XX PPP0 erase_intern)
-
-
-
-
-lemma PPP1:
- assumes "bder c (intern r) >> code v" "\<Turnstile> v : der c r"
- shows "(intern r) >> code (injval r c v)"
- using assms
- by (simp add: Prf_injval contains2)
-
-
-(*
-lemma PPP1:
- assumes "bder c r >> code v" "\<Turnstile> v : der c (erase r)"
- shows "r >> code (injval (erase r) c v)"
- using assms contains7[OF assms(2)] retrieve_code[OF assms(2)]
- find_theorems "bder _ _ >> _"
- by (simp add: Prf_injval contains2)
-*)
-
lemma PPP3:
assumes "\<Turnstile> v : ders s (erase a)"
shows "bders a s >> retrieve a (flex (erase a) id s v)"
@@ -3981,158 +3775,6 @@
find_theorems "bder _ _ >> _"
-lemma QQQ0:
- assumes "bder c a >> code v"
- shows "a >> code (injval (erase a) c v)"
- using assms
- apply(induct a arbitrary: c v)
- apply(auto)
- using contains.simps apply blast
- using contains.simps apply blast
- apply(case_tac "c = x2a")
- apply(simp)
- apply(erule contains.cases)
- apply(auto)
-
-
-lemma PPP4:
- assumes "bders (intern a) [c1, c2] >> bs"
- shows "bders_simp (intern a) [c1, c2] >> bs"
- using assms
- apply(simp)
- apply(rule contains55)
-
- find_theorems "bder _ _ >> _"
-
-
- apply(induct s arbitrary: a v rule: rev_induct)
- apply(simp)
- apply (simp add: contains6)
- apply(simp add: bders_append bders_simp_append ders_append flex_append)
- (*apply(rule contains55)*)
- apply(drule Prf_injval)
- apply(drule_tac x="a" in meta_spec)
- apply(drule_tac x="injval (ders xs (erase a)) x v" in meta_spec)
- apply(drule meta_mp)
- apply(assumption)
-
- apply(thin_tac "\<Turnstile> injval (ders xs (erase a)) x v : ders xs (erase a)")
-
- apply(thin_tac "bders a xs >> retrieve a (flex (erase a) id xs (injval (ders xs (erase a)) x v))")
-
- apply(rule Etrans)
- apply(rule contains7)
-
-lemma PPP4:
- assumes "bders a s >> code v" "\<Turnstile> v : ders s (erase a)"
- shows "bders_simp a s >> code v"
- using assms
- apply(induct s arbitrary: a v rule: rev_induct)
- apply(simp)
- apply(simp add: bders_append bders_simp_append ders_append)
- apply(rule contains55)
- find_theorems "bder _ _ >> _"
-
-
-lemma PPP0:
- assumes "s \<in> L (r)"
- shows "(bders (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(rule contains55)
- apply(rule Etrans)
- apply(rule contains7)
- defer
-
- find_theorems "_ >> _"
- apply(drule_tac x="der a r" in meta_spec)
- apply(drule meta_mp)
- find_theorems "bder _ _ >> _"
- apply(subgoal_tac "s \<in> L(der a r)")
- prefer 2
-
- apply (simp add: Posix_Prf contains2)
- apply(simp add: bders_simp_append)
- apply(rule contains55)
- apply(frule PPP0)
- apply(simp add: bders_append)
- using Posix_injval contains7
- apply(subgoal_tac "retrieve r (injval (erase r) x v)")
- find_theorems "bders _ _ >> _"
-
-
-
-lemma PPP1:
- assumes "\<Turnstile> v : ders s r"
- shows "bders (intern r) s >> code v"
- using assms
- apply(induct s arbitrary: r v rule: rev_induct)
- apply(simp)
- apply (simp add: Posix_Prf contains2)
- apply(simp add: bders_append ders_append flex_append)
- apply(frule Prf_injval)
- apply(drule meta_spec)
- apply(drule meta_spec)
- apply(drule meta_mp)
- apply(assumption)
- apply(subst retrieve_code)
- apply(assumption)
- apply(subst (asm) retrieve_code)
- apply(assumption)
-
- using contains7 contains7a contains6 retrieve_code
- apply(rule contains7)
-
- find_theorems "bder _ _ >> _"
- find_theorems "code _ = _"
- find_theorems "\<Turnstile> _ : der _ _"
-
-
-
- find_theorems "_ >> (code _)"
- apply(induct s arbitrary: a bs rule: rev_induct)
- apply(simp)
- apply(simp add: bders_simp_append bders_append)
- apply(rule contains55)
- find_theorems "bder _ _ >> _"
- apply(drule_tac x="bder a aa" in meta_spec)
- apply(drule_tac x="bs" in meta_spec)
- apply(simp)
- apply(rule contains55)
- find_theorems "bsimp _ >> _"
-
-lemma XXX4:
- assumes "good a"
- shows "bders_simp a s = bsimp (bders a s)"
- using assms
- apply(induct s arbitrary: a rule: rev_induct)
- apply(simp)
- apply (simp add: test2)
- apply(simp add: bders_append bders_simp_append)
- oops
-
-
-lemma MAINMAIN:
- "blexer r s = blexer_simp r s"
- apply(induct s arbitrary: r)
- apply(simp add: blexer_def blexer_simp_def)
- apply(simp add: blexer_def blexer_simp_def del: bders.simps bders_simp.simps)
- apply(auto simp del: bders.simps bders_simp.simps)
- prefer 2
- apply (metis b4 bders.simps(2) bders_simp.simps(2))
- prefer 2
- apply (metis b4 bders.simps(2))
- apply(subst bmkeps_simp)
- apply(simp)
- apply(case_tac s)
- apply(simp only: bders.simps)
- apply(subst bders_simp.simps)
- apply(simp)
- oops
-
lemma
fixes n :: nat