--- a/thys/BitCoded.thy Wed Feb 20 00:00:30 2019 +0000
+++ b/thys/BitCoded.thy Sat Feb 23 21:52:06 2019 +0000
@@ -120,6 +120,7 @@
fun retrieve :: "arexp \<Rightarrow> val \<Rightarrow> bit list" where
"retrieve (AONE bs) Void = bs"
| "retrieve (ACHAR bs c) (Char d) = bs"
+| "retrieve (AALTs bs [r]) v = bs @ retrieve r v"
| "retrieve (AALTs bs (r#rs)) (Left v) = bs @ retrieve r v"
| "retrieve (AALTs bs (r#rs)) (Right v) = bs @ retrieve (AALTs [] rs) v"
| "retrieve (ASEQ bs r1 r2) (Seq v1 v2) = bs @ retrieve r1 v1 @ retrieve r2 v2"
@@ -135,7 +136,7 @@
| "erase (ACHAR _ c) = CHAR c"
| "erase (AALTs _ []) = ZERO"
| "erase (AALTs _ [r]) = (erase r)"
-| "erase (AALTs _ (r#rs)) = ALT (erase r) (erase (AALTs [] rs))"
+| "erase (AALTs bs (r#rs)) = ALT (erase r) (erase (AALTs bs rs))"
| "erase (ASEQ _ r1 r2) = SEQ (erase r1) (erase r2)"
| "erase (ASTAR _ r) = STAR (erase r)"
@@ -154,6 +155,7 @@
where
"bmkeps(AONE bs) = bs"
| "bmkeps(ASEQ bs r1 r2) = bs @ (bmkeps r1) @ (bmkeps r2)"
+| "bmkeps(AALTs bs [r]) = bs @ (bmkeps r)"
| "bmkeps(AALTs bs (r#rs)) = (if bnullable(r) then bs @ (bmkeps r) else (bmkeps (AALTs bs rs)))"
| "bmkeps(ASTAR bs r) = bs @ [S]"
@@ -226,9 +228,25 @@
assumes "\<Turnstile> v : (erase r)"
shows "retrieve (fuse bs r) v = bs @ retrieve r v"
using assms
- apply(induct r arbitrary: v bs rule: erase.induct)
- apply(auto elim: Prf_elims)[1]
- sorry
+ apply(induct r arbitrary: v bs)
+ apply(auto elim: Prf_elims)[4]
+ defer
+ using retrieve_encode_STARS
+ apply(auto elim!: Prf_elims)[1]
+ apply(case_tac vs)
+ apply(simp)
+ apply(simp)
+ (* AALTs case *)
+ apply(simp)
+ apply(case_tac x2a)
+ apply(simp)
+ apply(auto elim!: Prf_elims)[1]
+ apply(simp)
+ apply(case_tac list)
+ apply(simp)
+ apply(auto)
+ apply(auto elim!: Prf_elims)[1]
+ done
lemma retrieve_fuse:
assumes "\<Turnstile> v : r"
@@ -243,24 +261,135 @@
using assms
apply(induct v r )
apply(simp_all add: retrieve_fuse retrieve_encode_STARS)
- sorry
+ done
+
+lemma r:
+ assumes "bnullable (AALTs bs (a # rs))"
+ shows "bnullable a \<or> (\<not> bnullable a \<and> bnullable (AALTs bs rs))"
+ using assms
+ apply(induct rs)
+ apply(auto)
+ done
+
+lemma r0:
+ assumes "bnullable a"
+ shows "bmkeps (AALTs bs (a # rs)) = bs @ (bmkeps a)"
+ using assms
+ by (metis bmkeps.simps(3) bmkeps.simps(4) list.exhaust)
+
+lemma r1:
+ assumes "\<not> bnullable a" "bnullable (AALTs bs rs)"
+ shows "bmkeps (AALTs bs (a # rs)) = bmkeps (AALTs bs rs)"
+ using assms
+ apply(induct rs)
+ apply(auto)
+ done
+
+lemma r2:
+ assumes "x \<in> set rs" "bnullable x"
+ shows "bnullable (AALTs bs rs)"
+ using assms
+ apply(induct rs)
+ apply(auto)
+ done
+lemma r3:
+ assumes "\<not> bnullable r"
+ " \<exists> x \<in> set rs. bnullable x"
+ shows "retrieve (AALTs bs rs) (mkeps (erase (AALTs bs rs))) =
+ retrieve (AALTs bs (r # rs)) (mkeps (erase (AALTs bs (r # rs))))"
+ using assms
+ apply(induct rs arbitrary: r bs)
+ apply(auto)[1]
+ apply(auto)
+ using bnullable_correctness apply blast
+ apply(auto simp add: bnullable_correctness mkeps_nullable retrieve_fuse2)
+ apply(subst retrieve_fuse2[symmetric])
+ apply (smt bnullable.simps(4) bnullable_correctness erase.simps(5) erase.simps(6) insert_iff list.exhaust list.set(2) mkeps.simps(3) mkeps_nullable)
+ apply(simp)
+ apply(case_tac "bnullable a")
+ apply (smt append_Nil2 bnullable.simps(4) bnullable_correctness erase.simps(5) erase.simps(6) fuse.simps(4) insert_iff list.exhaust list.set(2) mkeps.simps(3) mkeps_nullable retrieve_fuse2)
+ apply(drule_tac x="a" in meta_spec)
+ apply(drule_tac x="bs" in meta_spec)
+ apply(drule meta_mp)
+ apply(simp)
+ apply(drule meta_mp)
+ apply(auto)
+ apply(subst retrieve_fuse2[symmetric])
+ apply(case_tac rs)
+ apply(simp)
+ apply(auto)[1]
+ apply (simp add: bnullable_correctness)
+ apply (metis append_Nil2 bnullable_correctness erase_fuse fuse.simps(4) list.set_intros(1) mkeps.simps(3) mkeps_nullable nullable.simps(4) r2)
+ apply (simp add: bnullable_correctness)
+ apply (metis append_Nil2 bnullable_correctness erase.simps(6) erase_fuse fuse.simps(4) list.set_intros(2) mkeps.simps(3) mkeps_nullable r2)
+ apply(simp)
+ done
+
+
+lemma t:
+ assumes "\<forall>r \<in> set rs. nullable (erase r) \<longrightarrow> bmkeps r = retrieve r (mkeps (erase r))"
+ "nullable (erase (AALTs bs rs))"
+ shows " bmkeps (AALTs bs rs) = retrieve (AALTs bs rs) (mkeps (erase (AALTs bs rs)))"
+ using assms
+ apply(induct rs arbitrary: bs)
+ apply(simp)
+ apply(auto simp add: bnullable_correctness)
+ apply(case_tac rs)
+ apply(auto simp add: bnullable_correctness)[2]
+ apply(subst r1)
+ apply(simp)
+ apply(rule r2)
+ apply(assumption)
+ apply(simp)
+ apply(drule_tac x="bs" in meta_spec)
+ apply(drule meta_mp)
+ apply(auto)[1]
+ prefer 2
+ apply(case_tac "bnullable a")
+ apply(subst r0)
+ apply blast
+ apply(subgoal_tac "nullable (erase a)")
+ prefer 2
+ using bnullable_correctness apply blast
+ apply (metis (no_types, lifting) erase.simps(5) erase.simps(6) list.exhaust mkeps.simps(3) retrieve.simps(3) retrieve.simps(4))
+ apply(subst r1)
+ apply(simp)
+ using r2 apply blast
+ apply(drule_tac x="bs" in meta_spec)
+ apply(drule meta_mp)
+ apply(auto)[1]
+ apply(simp)
+ using r3 apply blast
+ apply(auto)
+ using r3 by blast
lemma bmkeps_retrieve:
assumes "nullable (erase r)"
shows "bmkeps r = retrieve r (mkeps (erase r))"
using assms
apply(induct r)
- apply(auto simp add: bnullable_correctness)
- sorry
-
+ apply(simp)
+ apply(simp)
+ apply(simp)
+ apply(simp)
+ defer
+ apply(simp)
+ apply(rule t)
+ apply(auto)
+ done
+
lemma bder_retrieve:
assumes "\<Turnstile> v : der c (erase r)"
shows "retrieve (bder c r) v = retrieve r (injval (erase r) c v)"
using assms
- apply(induct r arbitrary: v)
+ apply(induct r arbitrary: v rule: erase.induct)
apply(auto elim!: Prf_elims simp add: retrieve_fuse2 bnullable_correctness bmkeps_retrieve)
- sorry
+ apply(case_tac va)
+ apply(simp)
+ apply(auto)
+ by (smt Prf_elims(3) injval.simps(2) injval.simps(3) retrieve.simps(4) retrieve.simps(5) same_append_eq)
+
lemma MAIN_decode:
assumes "\<Turnstile> v : ders s r"
--- a/thys/PDerivs.thy Wed Feb 20 00:00:30 2019 +0000
+++ b/thys/PDerivs.thy Sat Feb 23 21:52:06 2019 +0000
@@ -358,27 +358,30 @@
apply(simp)
apply(simp)
apply(simp add: pders_CHAR)
+(* SEQ case *)
apply(simp)
apply(rule subset_trans)
apply(rule pders_SEQ)
defer
+(* ALT case *)
apply(simp)
apply(rule impI)
apply(rule conjI)
apply blast
- apply blast
+ apply blast
+(* STAR case *)
apply(case_tac s)
apply(simp)
apply(rule subset_trans)
thm pders_STAR
apply(rule pders_STAR)
apply(simp)
- apply(simp)
- apply (smt UN_I UN_least Un_iff insertCI pders_Set_def subsetCE subsetI)
+ apply(auto simp add: pders_Set_def)[1]
apply(simp)
apply(rule conjI)
- apply blast
- by (metis Un_insert_right le_supI1 pders_Set_subsetI subset_trans sup_ge2)
+ apply blast
+apply(auto simp add: pders_Set_def)[1]
+ done
fun size2 :: "rexp \<Rightarrow> nat" where
"size2 ZERO = 1" |
@@ -403,15 +406,18 @@
apply(simp)
apply(simp)
apply(simp)
+(* SEQ case *)
apply(simp)
apply(auto)[1]
apply (smt Suc_n_not_le_n add.commute distrib_left le_Suc_eq left_add_mult_distrib nat_le_linear trans_le_add1)
apply (smt Suc_le_mono Suc_n_not_le_n le_trans nat_le_linear power2_eq_square power2_sum semiring_normalization_rules(23) trans_le_add2)
apply (smt Groups.add_ac(3) Suc_n_not_le_n distrib_left le_Suc_eq left_add_mult_distrib nat_le_linear trans_le_add1)
+(* ALT case *)
apply(simp)
apply(auto)[1]
apply (smt Groups.add_ac(2) Suc_le_mono Suc_n_not_le_n le_add2 linear order_trans power2_eq_square power2_sum)
apply (smt Groups.add_ac(2) Suc_le_mono Suc_n_not_le_n left_add_mult_distrib linear mult.commute order.trans trans_le_add1)
+(* STAR case *)
apply(auto)[1]
apply(drule_tac x="r'" in bspec)
apply(simp)
--- a/thys/Sulzmann.thy Wed Feb 20 00:00:30 2019 +0000
+++ b/thys/Sulzmann.thy Sat Feb 23 21:52:06 2019 +0000
@@ -247,6 +247,12 @@
shows "bmkeps r = retrieve r (mkeps (erase r))"
using assms
apply(induct r)
+ apply(simp)
+ apply(simp)
+ apply(simp)
+ apply(simp)
+ apply(simp only: bmkeps.simps bnullable_correctness)
+ apply(auto simp only: split: if_split)
apply(auto simp add: bnullable_correctness)
done