--- a/thys/BitCoded.thy Mon Aug 19 16:24:28 2019 +0100
+++ b/thys/BitCoded.thy Tue Aug 20 23:42:28 2019 +0200
@@ -567,6 +567,9 @@
| "flts ((AALTs bs rs1) # rs) = (map (fuse bs) rs1) @ flts rs"
| "flts (r1 # rs) = r1 # flts rs"
+
+
+
fun li :: "bit list \<Rightarrow> arexp list \<Rightarrow> arexp"
where
"li _ [] = AZERO"
@@ -574,6 +577,8 @@
| "li bs as = AALTs bs as"
+
+
fun bsimp_ASEQ :: "bit list \<Rightarrow> arexp \<Rightarrow> arexp \<Rightarrow> arexp"
where
"bsimp_ASEQ _ AZERO _ = AZERO"
@@ -1083,6 +1088,8 @@
apply(auto)
done
+
+
lemma rt:
shows "sum_list (map asize (flts (map bsimp rs))) \<le> sum_list (map asize rs)"
apply(induct rs)
@@ -1783,6 +1790,56 @@
apply(simp_all)
done
+
+fun flts2 :: "char \<Rightarrow> arexp list \<Rightarrow> arexp list"
+ where
+ "flts2 _ [] = []"
+| "flts2 c (AZERO # rs) = flts2 c rs"
+| "flts2 c (AONE _ # rs) = flts2 c rs"
+| "flts2 c (ACHAR bs d # rs) = (if c = d then (ACHAR bs d # flts2 c rs) else flts2 c rs)"
+| "flts2 c ((AALTs bs rs1) # rs) = (map (fuse bs) rs1) @ flts2 c rs"
+| "flts2 c (ASEQ bs r1 r2 # rs) = (if (bnullable(r1) \<and> r2 = AZERO) then
+ flts2 c rs
+ else ASEQ bs r1 r2 # flts2 c rs)"
+| "flts2 c (r1 # rs) = r1 # flts2 c rs"
+
+lemma flts2_k0:
+ shows "flts2 c (r # rs1) = flts2 c [r] @ flts2 c rs1"
+ apply(induct r arbitrary: c rs1)
+ apply(auto)
+ done
+
+lemma flts2_k00:
+ shows "flts2 c (rs1 @ rs2) = flts2 c rs1 @ flts2 c rs2"
+ apply(induct rs1 arbitrary: rs2 c)
+ apply(auto)
+ by (metis append.assoc flts2_k0)
+
+
+lemma
+ shows "flts (map (bder c) rs) = (map (bder c) (flts2 c rs))"
+ apply(induct c rs rule: flts2.induct)
+ apply(simp)
+ apply(simp)
+ apply(simp)
+ apply(simp)
+ apply(simp)
+ apply(auto simp add: bder_fuse)[1]
+ defer
+ apply(simp)
+ apply(simp del: flts2.simps)
+ apply(rule conjI)
+ prefer 2
+ apply(auto)[1]
+ apply(rule impI)
+ apply(subst flts2_k0)
+ apply(subst map_append)
+ apply(subst flts2.simps)
+ apply(simp only: flts2.simps)
+ apply(auto)
+
+
+
lemma XXX2_helper:
assumes "\<forall>y. asize y < Suc (sum_list (map asize rs)) \<longrightarrow> good y \<longrightarrow> bsimp y = y"
"\<forall>r'\<in>set rs. good r' \<and> nonalt r'"
@@ -2390,130 +2447,13 @@
apply(auto)
done
-lemma
- assumes "\<forall>y. asize y < Suc (sum_list (map asize x52)) \<longrightarrow> asize (bsimp y) = asize y \<longrightarrow> bsimp y \<noteq> AZERO \<longrightarrow> bsimp y = y"
- "asize (bsimp_AALTs x51 (flts (map bsimp x52))) = Suc (sum_list (map asize x52))"
- "bsimp_AALTs x51 (flts (map bsimp x52)) \<noteq> AZERO"
- shows "bsimp_AALTs x51 (flts (map bsimp x52)) = AALTs x51 x52"
- using assms
- apply(induct x52 arbitrary: x51)
- apply(simp)
- oops
-
-
-lemma
- assumes "asize (bsimp a) = asize a" "bsimp a \<noteq> AZERO"
- shows "bsimp a = a"
- using assms
- apply(induct a taking: asize rule: measure_induct)
- apply(case_tac x)
- apply(simp_all)
- apply(case_tac "(bsimp x42) = AZERO")
- apply(simp add: asize0)
- apply(case_tac "(bsimp x43) = AZERO")
- apply(simp add: asize0)
- apply (metis bsimp_ASEQ0)
- apply(case_tac "\<exists>bs. (bsimp x42) = AONE bs")
- apply(auto)[1]
- apply (metis b1 bsimp_size fuse_size less_add_Suc2 not_less)
- apply (metis Suc_inject add.commute asize.simps(5) bsimp_ASEQ1 bsimp_size leD le_neq_implies_less less_add_Suc2 less_add_eq_less)
- (* ALT case *)
- apply(frule iii)
- apply(case_tac x52)
- apply(simp)
- apply(simp)
- apply(subst k0)
- apply(subst (asm) k0)
- apply(subst (asm) (2) k0)
- apply(subst (asm) (3) k0)
- apply(case_tac "(bsimp a) = AZERO")
- apply(simp)
- apply (metis (no_types, lifting) Suc_le_lessD asize0 bsimp_AALTs_size le_less_trans less_add_same_cancel2 not_less_eq rt)
- apply(simp)
- apply(case_tac "nonalt (bsimp a)")
- prefer 2
- apply(drule_tac x="AALTs x51 (bsimp a # list)" in spec)
- apply(drule mp)
- apply (metis asize.simps(4) bsimp.simps(2) bsimp_AALTs_size3 k0 less_not_refl list.set_intros(1) list.simps(9) sum_list.Cons)
- apply(drule mp)
- apply(simp)
- apply (metis asize.simps(4) bsimp.simps(2) bsimp_AALTs_size3 k0 lessI list.set_intros(1) list.simps(9) not_less_eq sum_list.Cons)
- apply(drule mp)
- apply(simp)
- using bsimp_idem apply auto[1]
- apply(simp add: bsimp_idem)
- apply (metis append.left_neutral append_Cons asize.simps(4) bsimp.simps(2) bsimp_AALTs_size3 k00 less_not_refl list.set_intros(1) list.simps(9) sum_list.Cons)
- apply (metis bsimp.simps(2) bsimp_idem k0 list.simps(9) nn1b nonalt.elims(3) nonnested.simps(2))
- apply(subgoal_tac "flts [bsimp a] = [bsimp a]")
- prefer 2
- using k0b apply blast
- apply(clarify)
- apply(simp only:)
- apply(simp)
- apply(case_tac "flts (map bsimp list) = Nil")
- apply (metis bsimp_AALTs1 bsimp_size fuse_size less_add_Suc1 not_less)
- apply (subgoal_tac "bsimp_AALTs x51 (bsimp a # flts (map bsimp list)) = AALTs x51 (bsimp a # flts (map bsimp list))")
- prefer 2
- apply (metis bsimp_AALTs.simps(3) neq_Nil_conv)
- apply(auto)
- apply (metis add.commute bsimp_size leD le_neq_implies_less less_add_Suc1 less_add_eq_less rt)
- oops
-
-
-
-
-lemma OOO:
- shows "bsimp (bsimp_AALTs bs rs) = bsimp_AALTs bs (flts (map bsimp rs))"
- apply(induct rs arbitrary: bs taking: "\<lambda>rs. sum_list (map asize rs)" rule: measure_induct)
- apply(case_tac x)
- apply(simp)
- apply(simp)
- apply(case_tac "a = AZERO")
- apply(simp)
- apply(case_tac "list")
- apply(simp)
- apply(simp)
- apply(case_tac "bsimp a = AZERO")
- apply(simp)
- apply(case_tac "list")
- apply(simp)
- apply(simp add: bsimp_fuse[symmetric])
- apply(simp)
- apply(case_tac "nonalt (bsimp a)")
- apply(case_tac list)
- apply(simp)
- apply(subst k0b)
- apply(simp)
- apply(simp)
- apply(simp add: bsimp_fuse)
- apply(simp)
- apply(subgoal_tac "asize (bsimp a) < asize a \<or> asize (bsimp a) = asize a")
- prefer 2
- using bsimp_size le_neq_implies_less apply blast
- apply(erule disjE)
- apply(drule_tac x="(bsimp a) # list" in spec)
- apply(drule mp)
- apply(simp)
- apply(simp)
- apply (metis bsimp.simps(2) bsimp_AALTs.elims bsimp_AALTs.simps(2) bsimp_fuse bsimp_idem list.distinct(1) list.inject list.simps(9))
- apply(subgoal_tac "\<exists>bs rs. bsimp a = AALTs bs rs \<and> rs \<noteq> Nil \<and> length rs > 1")
- prefer 2
- apply (metis bbbbs1 bsimp.simps(2) bsimp_AALTs.simps(1) bsimp_idem flts.simps(1) good.simps(5) good1 length_0_conv length_Suc_conv less_one list.simps(8) nat_neq_iff not_less_eq)
- apply(auto)
- oops
-
-
-lemma
- assumes "rs = [AALTs bsa [AONE bsb, AONE bsb]]"
- shows "bsimp (bsimp_AALTs bs rs) = bsimp_AALTs bs (flts (map bsimp rs))"
- using assms
- apply(simp)
- oops
-
-
+lemma CT1_SEQ:
+ shows "bsimp (ASEQ bs a1 a2) = bsimp (ASEQ bs (bsimp a1) (bsimp a2))"
+ apply(simp add: bsimp_idem)
+ done
lemma CT1:
- shows "bsimp (AALTs bs as) = bsimp(AALTs bs (map bsimp as))"
+ shows "bsimp (AALTs bs as) = bsimp (AALTs bs (map bsimp as))"
apply(induct as arbitrary: bs)
apply(simp)
apply(simp)
@@ -2523,6 +2463,21 @@
shows "bsimp (AALT bs a1 a2) = bsimp(AALT bs (bsimp a1) (bsimp a2))"
by (metis CT1 list.simps(8) list.simps(9))
+lemma WWW2:
+ shows "bsimp (bsimp_AALTs bs1 (flts (map bsimp as1))) =
+ bsimp_AALTs bs1 (flts (map bsimp as1))"
+ by (metis bsimp.simps(2) bsimp_idem)
+
+lemma CT1b:
+ shows "bsimp (bsimp_AALTs bs as) = bsimp (bsimp_AALTs bs (map bsimp as))"
+ apply(induct bs as rule: bsimp_AALTs.induct)
+ apply(auto simp add: bsimp_idem)
+ apply (simp add: bsimp_fuse bsimp_idem)
+ by (metis bsimp_idem comp_apply)
+
+
+
+
(* CT *)
lemma CTU:
@@ -2531,7 +2486,7 @@
apply(auto)
done
-
+find_theorems "bder _ (bsimp_AALTs _ _)"
lemma CTa:
assumes "\<forall>r \<in> set as. nonalt r \<and> r \<noteq> AZERO"
@@ -2574,15 +2529,6 @@
-
-lemma
- shows "bsimp (AALT bs (AALTs bs1 (map (bder c) as1)) (AALTs bs2 (map (bder c) as2)))
- = bsimp (AALTs bs ((map (fuse bs1) (map (bder c) as1)) @
- (map (fuse bs2) (map (bder c) as2))))"
- apply(subst bsimp_idem[symmetric])
- apply(simp)
- oops
-
lemma CT_exp:
assumes "\<forall>a \<in> set as. bsimp (bder c (bsimp a)) = bsimp (bder c a)"
shows "map bsimp (map (bder c) as) = map bsimp (map (bder c) (map bsimp as))"
@@ -2641,10 +2587,6 @@
using flts2 good1 apply fastforce
by (smt ex_map_conv list.simps(9) nn1b nn1c)
-lemma WWW2:
- shows "bsimp (bsimp_AALTs bs1 (flts (map bsimp as1))) =
- bsimp_AALTs bs1 (flts (map bsimp as1))"
- by (metis bsimp.simps(2) bsimp_idem)
lemma WWW3:
shows "flts [bsimp_AALTs bs1 (flts (map bsimp as1))] =
@@ -3019,12 +2961,17 @@
apply(simp)
prefer 3
apply(simp)
+ (* SEQ case *)
+ apply(simp only:)
+ apply(subst CT1_SEQ)
+ apply(simp only: bsimp.simps)
+
(* AALT case *)
prefer 2
apply(simp only:)
apply(case_tac "\<exists>a1 a2. x52 = [a1, a2]")
apply(clarify)
- apply(simp del: bsimp.simps)
+ apply(simp del: bsimp.simps)
apply(subst (2) CT1)
apply(simp del: bsimp.simps)
apply(rule_tac t="bsimp (bder c a1)" and s="bsimp (bder c (bsimp a1))" in subst)
@@ -3032,6 +2979,21 @@
apply(rule_tac t="bsimp (bder c a2)" and s="bsimp (bder c (bsimp a2))" in subst)
apply(simp del: bsimp.simps)
apply(subst CT1a[symmetric])
+ (* \<rightarrow> *)
+ apply(rule_tac t="AALT x51 (bder c (bsimp a1)) (bder c (bsimp a2))"
+ and s="bder c (AALT x51 (bsimp a1) (bsimp a2))" in subst)
+ apply(simp)
+ apply(subst bsimp.simps)
+ apply(simp del: bsimp.simps bder.simps)
+
+ apply(subst bder_bsimp_AALTs)
+ apply(subst bsimp.simps)
+ apply(subst WWW2[symmetric])
+ apply(subst bsimp_AALTs_qq)
+ defer
+ apply(subst bsimp.simps)
+
+ (* <- *)
apply(subst bsimp.simps)
apply(simp del: bsimp.simps)
(*bsimp_AALTs x51 (map (bder c) (flts [a1, a2])) =
@@ -3046,7 +3008,7 @@
apply(simp del: bsimp.simps)
apply(subst big0)
apply(simp add: WWW4)
- apply (metis One_nat_def Suc_eq_plus1 Suc_lessI arexp.distinct(7) bsimp.simps(2) bsimp_AALTs.simps(1) bsimp_idem flts.simps(1) length_append length_greater_0_conv length_map not_add_less2 not_less_eq)
+ apply (m etis One_nat_def Suc_eq_plus1 Suc_lessI arexp.distinct(7) bsimp.simps(2) bsimp_AALTs.simps(1) bsimp_idem flts.simps(1) length_append length_greater_0_conv length_map not_add_less2 not_less_eq)
oops
lemma XXX2a_long_without_good:
--- 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
--- a/thys/Lexer.thy Mon Aug 19 16:24:28 2019 +0100
+++ b/thys/Lexer.thy Tue Aug 20 23:42:28 2019 +0200
@@ -286,6 +286,11 @@
apply(simp_all add: comp_def)
by meson
+lemma flex_fun_apply2:
+ shows "g (flex r id s v) = flex r g s v"
+ by (simp add: flex_fun_apply)
+
+
lemma flex_append:
shows "flex r f (s1 @ s2) = flex (ders s1 r) (flex r f s1) s2"
apply(induct s1 arbitrary: s2 r f)
@@ -397,7 +402,14 @@
shows "flex (der a r) (injval r a) s v = injval r a (flex (der a r) id s v)"
by (simp add: flex_fun_apply)
-
-
+lemma Prf_flex:
+ assumes "\<Turnstile> v : ders s r"
+ shows "\<Turnstile> flex r id s v : r"
+ using assms
+ apply(induct s arbitrary: v r)
+ apply(simp)
+ apply(simp)
+ by (simp add: Prf_injval flex_injval)
+
end
\ No newline at end of file