--- a/thys/BitCoded.thy Thu Apr 11 17:37:00 2019 +0100
+++ b/thys/BitCoded.thy Fri May 10 11:56:37 2019 +0100
@@ -400,13 +400,65 @@
shows "retrieve (bder c r) v = retrieve r (injval (erase r) c v)"
using assms
apply(induct r arbitrary: v rule: erase.induct)
- apply(auto elim!: Prf_elims simp add: retrieve_fuse2 bnullable_correctness bmkeps_retrieve)
- apply(case_tac va)
+ apply(simp)
+ apply(erule Prf_elims)
+ apply(simp)
+ apply(erule Prf_elims)
+ apply(simp)
+ apply(case_tac "c = ca")
+ apply(simp)
+ apply(erule Prf_elims)
+ apply(simp)
+ apply(simp)
+ apply(erule Prf_elims)
+ apply(simp)
+ apply(erule Prf_elims)
+ apply(simp)
+ apply(simp)
+ apply(rename_tac "r\<^sub>1" "r\<^sub>2" rs v)
+ apply(erule Prf_elims)
+ apply(simp)
+ apply(simp)
+ apply(case_tac rs)
+ apply(simp)
+ apply(simp)
+ apply (smt Prf_elims(3) injval.simps(2) injval.simps(3) retrieve.simps(4) retrieve.simps(5) same_append_eq)
apply(simp)
- apply(auto)
- by (smt Prf_elims(3) injval.simps(2) injval.simps(3) retrieve.simps(4) retrieve.simps(5) same_append_eq)
+ apply(case_tac "nullable (erase r1)")
+ apply(simp)
+ apply(erule Prf_elims)
+ apply(subgoal_tac "bnullable r1")
+ prefer 2
+ using bnullable_correctness apply blast
+ apply(simp)
+ apply(erule Prf_elims)
+ apply(simp)
+ apply(subgoal_tac "bnullable r1")
+ prefer 2
+ using bnullable_correctness apply blast
+ apply(simp)
+ apply(simp add: retrieve_fuse2)
+ apply(simp add: bmkeps_retrieve)
+ apply(simp)
+ apply(erule Prf_elims)
+ apply(simp)
+ using bnullable_correctness apply blast
+ apply(rename_tac bs r v)
+ apply(simp)
+ apply(erule Prf_elims)
+ apply(clarify)
+ apply(erule Prf_elims)
+ apply(clarify)
+ apply(subst injval.simps)
+ apply(simp del: retrieve.simps)
+ apply(subst retrieve.simps)
+ apply(subst retrieve.simps)
+ apply(simp)
+ apply(simp add: retrieve_fuse2)
+ done
+
lemma MAIN_decode:
assumes "\<Turnstile> v : ders s r"
shows "Some (flex r id s v) = decode (retrieve (bders (intern r) s) v) r"
@@ -425,18 +477,23 @@
Some (flex r id s v) = decode (retrieve (bders (intern r) s) v) r" by fact
have asm: "\<Turnstile> v : ders (s @ [c]) r" by fact
then have asm2: "\<Turnstile> injval (ders s r) c v : ders s r"
- by(simp add: Prf_injval ders_append)
+ by (simp add: Prf_injval ders_append)
have "Some (flex r id (s @ [c]) v) = Some (flex r id s (injval (ders s r) c v))"
by (simp add: flex_append)
also have "... = decode (retrieve (bders (intern r) s) (injval (ders s r) c v)) r"
using asm2 IH by simp
also have "... = decode (retrieve (bder c (bders (intern r) s)) v) r"
- using asm by(simp_all add: bder_retrieve ders_append)
+ using asm by (simp_all add: bder_retrieve ders_append)
finally show "Some (flex r id (s @ [c]) v) =
decode (retrieve (bders (intern r) (s @ [c])) v) r" by (simp add: bders_append)
qed
+definition blex where
+ "blex a s \<equiv> if bnullable (bders a s) then Some (bmkeps (bders a s)) else None"
+
+
+
definition blexer where
"blexer r s \<equiv> if bnullable (bders (intern r) s) then
decode (bmkeps (bders (intern r) s)) r else None"
@@ -513,6 +570,9 @@
decode (bmkeps (bders_simp (intern r) s)) r else None"
+
+
+
lemma asize0:
shows "0 < asize r"
apply(induct r)
@@ -964,6 +1024,20 @@
apply(auto)
by (metis (mono_tags, hide_lams) imageE nn1c set_map)
+lemma nn1d:
+ assumes "bsimp r = AALTs bs rs"
+ shows "\<forall>r1 \<in> set rs. \<forall> bs. r1 \<noteq> AALTs bs rs2"
+ using nn1b assms
+ by (metis nn1qq)
+
+lemma nn_flts:
+ assumes "nonnested (AALTs bs rs)"
+ shows "\<forall>r \<in> set (flts rs). nonalt r"
+ using assms
+ apply(induct rs arbitrary: bs rule: flts.induct)
+ apply(auto)
+ done
+
lemma rt:
shows "sum_list (map asize (flts (map bsimp rs))) \<le> sum_list (map asize rs)"
apply(induct rs)
@@ -973,6 +1047,16 @@
apply(simp)
by (smt add_le_cancel_right add_mono bsimp_size flts.simps(1) flts_size k0 le_iff_add list.simps(9) map_append sum_list.Cons sum_list.append trans_le_add1)
+lemma bsimp_AALTs_qq:
+ assumes "1 < length rs"
+ shows "bsimp_AALTs bs rs = AALTs bs rs"
+ using assms
+ apply(case_tac rs)
+ apply(simp)
+ apply(case_tac list)
+ apply(simp_all)
+ done
+
lemma flts_idem:
assumes "\<forall>r \<in> set rs. bsimp (bsimp r) = bsimp r"
shows "flts (map bsimp (flts (map bsimp rs))) = flts (map bsimp rs)"
@@ -1007,7 +1091,7 @@
apply(simp)
apply(case_tac a)
apply(simp_all)
- sorry
+ oops
lemma bsimp_AALTs_idem:
(*assumes "\<forall>r \<in> set rs. bsimp (bsimp r) = bsimp r \<and> nonalt (bsimp r)" *)
@@ -1091,6 +1175,149 @@
prefer 3
oops
+lemma ww:
+ shows "bsimp_AALTs bs [r] = fuse bs r"
+ by simp
+
+lemma flts_0:
+ assumes "nonnested (AALTs bs rs)"
+ shows "\<forall>r \<in> set (flts rs). r \<noteq> AZERO"
+ using assms
+ apply(induct rs arbitrary: bs rule: flts.induct)
+ apply(simp)
+ apply(simp)
+ defer
+ apply(simp)
+ apply(simp)
+ apply(simp)
+apply(simp)
+ apply(rule ballI)
+ apply(simp)
+ done
+
+lemma q1:
+ shows "AZERO \<notin> set (flts (map bsimp rs))"
+ apply(induct rs)
+ apply(simp)
+ apply(simp)
+ apply(case_tac rs)
+ apply(simp)
+
+lemma cc:
+ assumes "bsimp (fuse bs' r) = (AALTs bs rs)"
+ shows "\<forall>r \<in> set rs. r \<noteq> AZERO"
+ using assms
+ apply(induct r arbitrary: rs bs bs' rule: bsimp.induct)
+ apply(simp)
+ apply(case_tac "bsimp r1 = AZERO")
+ apply simp
+ apply(case_tac "bsimp r2 = AZERO")
+ apply(simp)
+ apply(case_tac "\<exists>bs'. bsimp r1 = AONE bs'")
+ apply(auto)[1]
+ apply (simp add: bsimp_ASEQ0)
+ apply(case_tac "\<exists>bs'. bsimp r1 = AONE bs'")
+ apply(auto)[2]
+ apply (simp add: bsimp_ASEQ2)
+ using bsimp_fuse apply fastforce
+ apply (simp add: bsimp_ASEQ1)
+ prefer 2
+ apply(simp)
+ defer
+ apply(simp)
+ apply(simp)
+ apply(simp)
+ (* AALT case *)
+ apply(simp only: fuse.simps)
+ apply(simp)
+ apply(case_tac "flts (map bsimp rs)")
+ apply(simp)
+ apply(simp)
+ apply(case_tac list)
+ apply(simp)
+ apply(case_tac a)
+ apply(simp_all)
+ apply(auto)
+ apply (metis ex_map_conv list.set_intros(1) nn1b nn1c nonalt.simps(1))
+ apply(case_tac rs)
+ apply(simp)
+ apply(simp)
+ apply(case_tac list)
+ apply(simp)
+
+
+ apply(subgoal_tac "\<forall>r \<in> set (flts (map bsimp rs)). r \<noteq> AZERO")
+ prefer 2
+ apply(rule_tac bs="bs' @ bs1" in flts_0)
+
+
+ thm bsimp_AALTs_qq
+ apply(case_tac "1 < length rs")
+ apply(drule_tac bsimp_AALTs_qq)
+ apply(subgoal_tac "nonnested (AALTs bs rsa)")
+ prefer 2
+ apply (metis nn1b)
+ apply(rule ballI)
+ apply(simp)
+ apply(drule_tac x="r" in meta_spec)
+ apply(simp)
+ (* HERE *)
+ apply(drule flts_0)
+
+
+
+ apply(simp)
+
+
+
+
+ apply(subst
+
+ apply (sm t arexp.distinct(15) arexp.distinct(21) arexp.distinct(25) arexp.distinct(29) arexp.inject(4) b1 fuse.elims)
+
+ prefer 2
+
+
+ apply(induct r arbitrary: rs bs bs' rule: bsimp.induct)
+ apply(auto)
+ apply(case_tac "bsimp r1 = AZERO")
+ apply simp
+ apply(case_tac "bsimp r2 = AZERO")
+ apply(simp)
+ apply(case_tac "\<exists>bs'. bsimp r1 = AONE bs'")
+ apply(auto)
+ apply (simp add: bsimp_ASEQ0)
+ apply(case_tac "\<exists>bs'. bsimp r1 = AONE bs'")
+ apply(auto)
+ apply (simp add: bsimp_ASEQ2)
+ using bsimp_fuse apply fastforce
+ apply (simp add: bsimp_ASEQ1)
+
+
+
+ apply(subst
+
+ apply (sm t arexp.distinct(15) arexp.distinct(21) arexp.distinct(25) arexp.distinct(29) arexp.inject(4) b1 fuse.elims)
+
+ prefer 2
+
+
+
+lemma ww1:
+ assumes "flts [r1] = [r2]" "r1 \<noteq> AZERO"
+ shows "r1 = r2"
+ using assms
+ apply(case_tac r1)
+ apply(simp)
+ apply(simp)
+ apply(simp)
+ apply(simp)
+ prefer 2
+ apply(simp)
+ apply(simp)
+ apply(auto)
+ oops
+
lemma bsimp_idem:
shows "bsimp (bsimp r) = bsimp r"
apply(induct r taking: "asize" rule: measure_induct)
@@ -1104,8 +1331,87 @@
apply (simp add: bsimp_ASEQ_idem)
apply(clarify)
apply(case_tac x52)
+ apply(simp)
+ (* AALT case where rs is of the form _ # _ *)
+ apply(clarify)
apply(simp)
- apply(simp)
+ apply(case_tac "length (flts (bsimp a # map bsimp list)) \<le> 1")
+ prefer 2
+ apply(subst bsimp_AALTs_qq)
+ apply(auto)[1]
+ apply(simp)
+ prefer 2
+ apply(subgoal_tac "length (flts (bsimp a # map bsimp list)) = 0 \<or>
+ length (flts (bsimp a # map bsimp list)) = 1")
+ prefer 2
+ apply(auto)[1]
+ using le_SucE apply blast
+ apply(erule disjE)
+ apply(simp)
+ apply(simp)
+ apply(subst k0)
+ apply(subst (2) k0)
+ apply(subst (asm) k0)
+ apply(simp)
+ apply(subgoal_tac "length (flts [bsimp a]) = 1 \<or>
+ length (flts (map bsimp list)) = 1")
+ prefer 2
+ apply linarith
+ apply(erule disjE)
+ apply(simp)
+ prefer 2
+ apply(simp)
+ apply(drule_tac x="AALTs x51 list" in spec)
+ apply(drule mp)
+ apply(simp)
+ using asize0 apply blast
+ apply(simp)
+ apply(frule_tac x="a" in spec)
+ apply(drule mp)
+ apply(simp)
+ apply(subgoal_tac "\<exists>r. flts [bsimp a] = [r]")
+ prefer 2
+ apply (simp add: length_Suc_conv)
+ apply(clarify)
+ apply(simp only: )
+ apply(case_tac "bsimp a = AZERO")
+ apply simp
+ apply(case_tac "\<exists>bs rs. bsimp a = AALTs bs rs")
+ apply(clarify)
+ apply(simp)
+ apply(drule_tac x="AALTs bs rs" in spec)
+ apply(drule mp)
+ apply(simp)
+ apply (metis asize.simps(4) bsimp_size lessI less_le_trans trans_less_add1)
+ apply(simp)
+
+ apply(subst ww)
+ apply(subst ww)
+ apply(frule_tac x="fuse x51 r" in spec)
+ apply(drule mp)
+ apply(simp)
+ apply (smt add.commute add_le_cancel_right fuse_size le_add2 le_trans list.map(1) list.simps(9) not_less not_less_eq rt sum_list.Cons)
+ apply(case_tac "bsimp a = AZERO")
+ apply simp
+ apply(case_tac "\<exists>bs rs. bsimp a = AALTs bs rs")
+ apply(clarify)
+
+ defer
+
+ apply(
+ apply(case_tac a)
+ apply(simp_all)
+ apply(subgoal_tac "\<exists>r. flts [bsimp a] = [r]")
+ prefer 2
+ apply (simp add: length_Suc_conv)
+ apply auto[1]
+ apply(case_tac
+ apply(clarify)
+
+ defer
+ apply(auto)[1]
+
+
apply(subst k0)
apply(subst (2) k0)
apply(case_tac "bsimp a = AZERO")
@@ -1480,7 +1786,7 @@
defer
apply(subst bsimp_ASEQ1)
- using L_bsimp_erase L_flat_Prf1 L_flat_Prf2 apply fastforce
+ using L_bsimp_erase L_flat_Prf1 L_flat_Prf2 apply fast force
using L_bsimp_erase L_
lemma retrieve_XXX:
@@ -1744,7 +2050,7 @@
apply(auto elim!: Prf_elims)[1]
apply(case_tac "(bsimp (fuse [Z] (bder c r))) = AZERO")
apply(simp)
- apply (metis L_bsimp_erase L_flat_Prf1 L_flat_Prf2 Prf_elims(1) erase.simps(1) erase_bder erase_fuse)
+ apply (met is L_bsimp_erase L_flat_Prf1 L_flat_Prf2 Prf_elims(1) erase.simps(1) erase_bder erase_fuse)
apply(case_tac "\<exists>bs. bsimp (fuse [Z] (bder c r)) = AONE bs")
apply(clarify)
apply(subgoal_tac "L (der c (erase r)) = {[]}")
@@ -1960,7 +2266,7 @@
apply(subst blexer_def)
apply(subgoal_tac "bnullable (bders (intern r) (a # s))")
prefer 2
- apply (metis Posix_injval blexer_correctness blexer_def lexer_correctness(2))
+ apply (me tis Posix_injval blexer_correctness blexer_def lexer_correctness(2))
apply(simp)
@@ -1992,6 +2298,198 @@
apply(simp)
apply(subst bnullable_correctness[symmetric])
apply(simp)
+ oops
+
+lemma flts_append:
+ "flts (xs1 @ xs2) = flts xs1 @ flts xs2"
+ apply(induct xs1 arbitrary: xs2 rule: rev_induct)
+ apply(auto)
+ apply(case_tac xs)
+ apply(auto)
+ apply(case_tac x)
+ apply(auto)
+ apply(case_tac x)
+ apply(auto)
+ done
+
+lemma flts_bsimp:
+ "flts (map bsimp rs) = map bsimp (flts rs)"
+apply(induct rs taking: size rule: measure_induct)
+ apply(case_tac x)
+ apply(simp)
+ apply(simp)
+ apply(induct rs rule: flts.induct)
+ apply(simp)
+ apply(simp)
+ defer
+ apply(simp)
+ apply(simp)
+ defer
+ apply(simp)
+ apply(subst List.list.map(2))
+ apply(simp only: flts.simps)
+ apply(subst k0)
+ apply(subst map_append)
+ apply(simp only:)
+ apply(simp del: bsimp.simps)
+ apply(case_tac rs1)
+ apply(simp)
+ apply(simp)
+ apply(case_tac list)
+ apply(simp_all)
+ thm map
+ apply(subst map.simps)
+ apply(auto)
+ defer
+ apply(case_tac "(bsimp va) = AZERO")
+ apply(simp)
+
+ using b3 apply for ce
+ apply(case_tac "(bsimp a2) = AZERO")
+ apply(simp)
+ apply (me tis bder.simps(1) bsimp.simps(3) bsimp_AALTs.simps(1) bsimp_ASEQ0 bsimp_fuse flts.simps(1) flts.simps(2) fuse.simps(1))
+ apply(case_tac "\<exists>bs. (bsimp a1) = AONE bs")
+ apply(clarify)
+ apply(simp)
+
+
+lemma XXX:
+ shows "bsimp (bsimp a) = bsimp a"
+ sorry
+
+lemma bder_fuse:
+ shows "bder c (fuse bs a) = fuse bs (bder c a)"
+ apply(induct a arbitrary: bs c)
+ apply(simp_all)
+ done
+
+lemma XXX2:
+ shows "bsimp (bder c (bsimp a)) = bsimp (bder c a)"
+ apply(induct a arbitrary: c)
+ apply(simp)
+ apply(simp)
+ apply(simp)
+ prefer 3
+ apply(simp)
+ apply(auto)[1]
+ 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.simps(3) bsimp_AALTs.simps(1) bsimp_ASEQ0 bsimp_fuse flts.simps(1) flts.simps(2) fuse.simps(1))
+ apply(case_tac "\<exists>bs. (bsimp a1) = AONE bs")
+ apply(clarify)
+ apply(simp)
+ apply(subst bsimp_ASEQ2)
+ apply(subgoal_tac "bmkeps a1 = bs")
+ prefer 2
+ apply (simp add: bmkeps_simp)
+ apply(simp)
+ apply(subst (1) bsimp_fuse[symmetric])
+ defer
+ apply(subst bsimp_ASEQ1)
+ apply(simp)
+ apply(simp)
+ apply(simp)
+ apply(auto)[1]
+ apply (metis XXX bmkeps_simp bsimp_fuse)
+ using b3 apply blast
+ apply (smt XXX b3 bder.simps(1) bder.simps(5) bnullable.simps(2) bsimp.simps(1) bsimp_ASEQ.simps(1) bsimp_ASEQ0 bsimp_ASEQ1)
+ apply(simp)
+ prefer 2
+ apply(subst bder_fuse)
+ apply(subst bsimp_fuse[symmetric])
+ apply(simp)
+ sorry
+
+
+thm bsimp_AALTs.simps
+thm bsimp.simps
+thm flts.simps
+
+lemma XXX3:
+ "bsimp (bders (bsimp r) s) = bsimp (bders r s)"
+ apply(induct s arbitrary: r rule: rev_induct)
+ apply(simp)
+ apply (simp add: XXX)
+ apply(simp add: bders_append)
+ apply(subst (2) XXX2[symmetric])
+ apply(subst XXX2[symmetric])
+ apply(drule_tac x="r" in meta_spec)
+ apply(simp)
+ done
+
+lemma XXX4:
+ "bders_simp (bsimp r) s = bsimp (bders r s)"
+ apply(induct s arbitrary: r)
+ apply(simp)
+ apply(simp)
+ by (metis XXX2)
+
+
+lemma
+ assumes "bnullable (bder c r)" "bnullable (bder c (bsimp r))"
+ shows "bmkeps (bder c r) = bmkeps (bder c (bsimp r))"
+ using assms
+ apply(induct r arbitrary: c)
+ apply(simp)
+ apply(simp)
+ apply(simp)
+ prefer 3
+ apply(simp)
+ apply(auto)[1]
+ apply(case_tac "(bsimp r1) = AZERO")
+ apply(simp)
+ apply(case_tac "(bsimp r2) = AZERO")
+ apply(simp)
+ apply (simp add: bsimp_ASEQ0)
+ apply(case_tac "\<exists>bs. (bsimp r1) = AONE bs")
+ apply(clarify)
+ apply(simp)
+ apply(subgoal_tac "bnullable r1")
+ prefer 2
+ using b3 apply force
+ apply(simp)
+ apply(simp add: bsimp_ASEQ2)
+ prefer 2
+
+
+
+ apply(subst bsimp_ASEQ2)
+
+
+
+
+
+
+lemma
+ assumes "bnullable (bders a (s1 @ s2))" "bnullable (bders (bsimp (bders a s1)) s2)"
+ shows "bmkeps (bders a (s1 @ s2)) = bmkeps (bders (bsimp (bders a s1)) s2)"
+ using assms
+ apply(induct s2 arbitrary: a s1)
+ apply(simp)
+ using bmkeps_simp apply blast
+ apply(simp add: bders_append)
+ apply(drule_tac x="aa" in meta_spec)
+ apply(drule_tac x="s1 @ [a]" in meta_spec)
+ apply(drule meta_mp)
+ apply(simp add: bders_append)
+ apply(simp add: bders_append)
+ apply(drule meta_mp)
+ apply (metis b4 bders.simps(2) bders_simp.simps(2))
+ apply(simp)
+
+ apply (met is b4 bders.simps(2) bders_simp.simps(2))
+
+
+
+ using b3 apply blast
+ using b3 apply auto[1]
+ apply(auto simp add: blex_def)
+ prefer 3
+
+