--- a/thys/BitCoded.thy Wed May 15 11:51:52 2019 +0100
+++ b/thys/BitCoded.thy Thu May 23 13:30:09 2019 +0100
@@ -129,7 +129,11 @@
| "good (AONE cs) = True"
| "good (ACHAR cs c) = True"
| "good (AALTs cs []) = False"
-| "good (AALTs cs (r#rs)) = (\<forall>r' \<in> set (r#rs). good r')"
+| "good (AALTs cs [r]) = False"
+| "good (AALTs cs (r1#r2#rs)) = (\<forall>r' \<in> set (r1#r2#rs). good r' \<and> nonalt r')"
+| "good (ASEQ _ AZERO _) = False"
+| "good (ASEQ _ (AONE _) _) = False"
+| "good (ASEQ _ _ AZERO) = False"
| "good (ASEQ cs r1 r2) = (good r1 \<and> good r2)"
| "good (ASTAR cs r) = True"
@@ -1079,13 +1083,40 @@
lemma good_fuse:
shows "good (fuse bs r) = good r"
- apply(induct r)
+ apply(induct r arbitrary: bs)
apply(auto)
- apply (metis arexp.distinct(25) arexp.distinct(7) arexp.inject(4) good.elims(3) good.simps(4) good.simps(5))
- by (metis good.simps(4) good.simps(5) neq_Nil_conv)
+ apply(case_tac r1)
+ apply(simp_all)
+ apply(case_tac r2)
+ apply(simp_all)
+ apply(case_tac r2)
+ apply(simp_all)
+ apply(case_tac r2)
+ apply(simp_all)
+ apply(case_tac r2)
+ apply(simp_all)
+ apply(case_tac r1)
+ apply(simp_all)
+ apply(case_tac r2)
+ apply(simp_all)
+ apply(case_tac r2)
+ apply(simp_all)
+ apply(case_tac r2)
+ apply(simp_all)
+ apply(case_tac r2)
+ apply(simp_all)
+ apply(case_tac x2a)
+ apply(simp_all)
+ apply(case_tac list)
+ apply(simp_all)
+ apply(case_tac x2a)
+ apply(simp_all)
+ apply(case_tac list)
+ apply(simp_all)
+ done
lemma good0:
- assumes "rs \<noteq> Nil"
+ assumes "rs \<noteq> Nil" "\<forall>r \<in> set rs. nonalt r"
shows "good (bsimp_AALTs bs rs) \<longleftrightarrow> (\<forall>r \<in> set rs. good r)"
using assms
apply(induct bs rs rule: bsimp_AALTs.induct)
@@ -1093,12 +1124,17 @@
done
lemma good0a:
- assumes "flts (map bsimp rs) \<noteq> Nil"
+ assumes "flts (map bsimp rs) \<noteq> Nil" "\<forall>r \<in> set (flts (map bsimp rs)). nonalt r"
shows "good (bsimp (AALTs bs rs)) \<longleftrightarrow> (\<forall>r \<in> set (flts (map bsimp rs)). good r)"
using assms
apply(simp)
- apply(rule good0)
+ apply(auto)
+ apply(subst (asm) good0)
apply(simp)
+ apply(auto)
+ apply(subst good0)
+ apply(simp)
+ apply(auto)
done
lemma flts0:
@@ -1122,7 +1158,7 @@
lemma flts2:
assumes "good r"
- shows "\<forall>r' \<in> set (flts [r]). good r'"
+ shows "\<forall>r' \<in> set (flts [r]). good r' \<and> nonalt r'"
using assms
apply(induct r)
apply(simp)
@@ -1131,16 +1167,11 @@
prefer 2
apply(simp)
apply(auto)[1]
- apply (metis good.simps(5) good_fuse in_set_insert insert_Nil list.exhaust)
- prefer 2
- apply(simp)
- by fastforce
-
-lemma flts3a:
- assumes "good r"
- shows "good (AALTs bs (flts [r]))"
- using assms
- by (metis flts1 flts2 good.simps(5) neq_Nil_conv)
+ apply (metis bsimp_AALTs.elims good.simps(4) good.simps(5) good.simps(6) good_fuse)
+ apply (metis bsimp_AALTs.elims good.simps(4) good.simps(5) good.simps(6) nn11a)
+ apply fastforce
+ apply(simp)
+ done
lemma flts3:
@@ -1172,11 +1203,12 @@
apply (metis (no_types, lifting) Nil_is_append_conv append_self_conv2 bsimp_AALTs.elims butlast.simps(2) butlast_append flts3b nonalt.simps(1) nonalt.simps(2))
apply (metis arexp.distinct(7) bsimp_AALTs.elims flts2 good.simps(1) good.simps(2) good0 k0b list.distinct(1) list.inject nonalt.simps(3))
apply (metis arexp.distinct(3) arexp.distinct(7) bsimp_AALTs.elims fuse.simps(3) list.distinct(1) list.inject)
- apply (metis arexp.distinct(7) bsimp_AALTs.elims good.simps(1) good.simps(6) good_fuse list.distinct(1) list.inject)
- apply (metis arexp.distinct(7) bsimp_AALTs.elims list.distinct(1) list.inject)
- apply (metis arexp.distinct(7) bsimp_AALTs.simps(2) bsimp_AALTs.simps(3) flts.simps(1) flts.simps(2) flts1 good.simps(7) good_fuse neq_Nil_conv)
+ apply (metis arexp.distinct(7) bsimp_AALTs.elims good.simps(1) good_fuse list.distinct(1) list.inject)
+ apply (metis arexp.distinct(7) bsimp_AALTs.elims list.distinct(1) list.inject)
+ apply (metis arexp.distinct(7) bsimp_AALTs.elims flts2 good.simps(1) good.simps(33) good0 k0b list.distinct(1) list.inject nonalt.simps(6))
by (metis (no_types, lifting) Nil_is_append_conv append_Nil2 arexp.distinct(7) bsimp_AALTs.elims butlast.simps(2) butlast_append flts1 flts2 good.simps(1) good0 k0a)
+
lemma flts_nil:
assumes "\<forall>y. asize y < Suc (sum_list (map asize rs)) \<longrightarrow>
good (bsimp y) \<or> bsimp y = AZERO"
@@ -1189,7 +1221,40 @@
apply(subst k0)
apply(simp)
by force
+
+lemma flts_nil2:
+ assumes "\<forall>y. asize y < Suc (sum_list (map asize rs)) \<longrightarrow>
+ good (bsimp y) \<or> bsimp y = AZERO"
+ and "bsimp_AALTs bs (flts (map bsimp rs)) = AZERO"
+ shows "flts (map bsimp rs) = []"
+ using assms
+ apply(induct rs arbitrary: bs)
+ apply(simp)
+ apply(simp)
+ apply(subst k0)
+ apply(simp)
+ apply(subst (asm) k0)
+ apply(auto)
+ apply (metis flts.simps(1) flts.simps(2) flts4 k0 less_add_Suc1 list.set_intros(1))
+ by (metis flts.simps(2) flts4 k0 less_add_Suc1 list.set_intros(1))
+
+
+lemma good_SEQ:
+ assumes "r1 \<noteq> AZERO" "r2 \<noteq> AZERO" "\<forall>bs. r1 \<noteq> AONE bs"
+ shows "good (ASEQ bs r1 r2) = (good r1 \<and> good r2)"
+ using assms
+ apply(case_tac r1)
+ apply(simp_all)
+ apply(case_tac r2)
+ apply(simp_all)
+ apply(case_tac r2)
+ apply(simp_all)
+ apply(case_tac r2)
+ apply(simp_all)
+ apply(case_tac r2)
+ apply(simp_all)
+ done
lemma good1:
shows "good (bsimp a) \<or> bsimp a = AZERO"
@@ -1211,7 +1276,7 @@
apply(erule disjE)
prefer 2
apply(simp)
- apply(frule_tac x="AALTs x51 list" in spec)
+ apply(drule_tac x="AALTs x51 list" in spec)
apply(drule mp)
apply(simp add: asize0)
apply(auto)[1]
@@ -1222,22 +1287,42 @@
apply(rule disjI1)
apply(simp add: good0)
apply(subst good0)
- apply (metis Nil_is_append_conv flts1 k0)
+ apply (metis Nil_is_append_conv flts1 k0)
+ apply (metis ex_map_conv list.simps(9) nn1b nn1c)
apply(simp)
apply(subst k0)
apply(simp)
apply(auto)[1]
using flts2 apply blast
- apply (metis good0 in_set_member member_rec(2))
- apply(simp)
- apply(rule disjI1)
- apply(drule flts4)
- apply(subst k0)
- apply(subst good0)
- apply (metis append_is_Nil_conv flts1 k0)
- apply(auto)[1]
+ apply(subst (asm) good0)
+ prefer 3
+ apply(auto)[1]
+ apply auto[1]
+ apply (metis ex_map_conv nn1b nn1c)
+ apply(simp)
+ apply(frule_tac x="a" in spec)
+ apply(drule mp)
+ apply(simp)
+ apply(erule disjE)
+ apply(rule disjI1)
+ apply(subst good0)
+ apply(subst k0)
+ using flts1 apply blast
+ apply(auto)[1]
+ apply (metis (no_types, hide_lams) ex_map_conv list.simps(9) nn1b nn1c)
+ apply(auto)[1]
+ apply(subst (asm) k0)
+ apply(auto)[1]
using flts2 apply blast
- apply (metis add.commute add_lessD1 flts_nil list.distinct(1) list.set_cases not_less_eq)
+ apply(frule_tac x="AALTs x51 list" in spec)
+ apply(drule mp)
+ apply(simp add: asize0)
+ apply(erule disjE)
+ apply(simp)
+ apply(simp)
+ apply (metis add.left_commute flts_nil2 less_add_Suc1 less_imp_Suc_add list.distinct(1) list.set_cases nat.inject)
+ apply(subst (2) k0)
+ apply(simp)
(* SEQ case *)
apply(simp)
apply(case_tac "bsimp x42 = AZERO")
@@ -1252,8 +1337,19 @@
using good_fuse apply force
apply(subst bsimp_ASEQ1)
apply(auto)
- using less_add_Suc1 apply blast
- using less_add_Suc2 by blast
+ apply(subst good_SEQ)
+ apply(simp)
+ apply(simp)
+ apply(simp)
+ using less_add_Suc1 less_add_Suc2 by blast
+
+lemma good1a:
+ assumes "L(erase a) \<noteq> {}"
+ shows "good (bsimp a)"
+ using good1 assms
+ using L_bsimp_erase by force
+
+
lemma flts_append:
"flts (xs1 @ xs2) = flts xs1 @ flts xs2"
@@ -1280,7 +1376,6 @@
apply(simp)
by simp
-
lemma flts_0:
assumes "nonnested (AALTs bs rs)"
shows "\<forall>r \<in> set (flts rs). r \<noteq> AZERO"
@@ -1306,66 +1401,8 @@
lemma qqq1:
shows "AZERO \<notin> set (flts (map bsimp rs))"
by (metis ex_map_conv flts3 good.simps(1) good1)
-
-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)
- oops
-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
-
fun nonazero :: "arexp \<Rightarrow> bool"
where
"nonazero AZERO = False"
@@ -1387,213 +1424,119 @@
apply(auto)
done
+lemma flts_qq:
+ 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'"
+ shows "flts (map bsimp rs) = rs"
+ using assms
+ apply(induct rs)
+ apply(simp)
+ apply(simp)
+ apply(subst k0)
+ apply(subgoal_tac "flts [bsimp a] = [a]")
+ prefer 2
+ apply(drule_tac x="a" in spec)
+ apply(drule mp)
+ apply(simp)
+ apply(auto)[1]
+ using good.simps(1) k0b apply blast
+ apply(auto)[1]
+ done
+
lemma test:
- assumes "good r"
- shows "bsimp (r) = r"
+ assumes "good r"
+ shows "bsimp r = r"
+ using assms
+ apply(induct r taking: "asize" rule: measure_induct)
+ apply(erule good.elims)
+ apply(simp_all)
+ apply(subst k0)
+ apply(subst (2) k0)
+ apply(subst flts_qq)
+ apply(auto)[1]
+ apply(auto)[1]
+ apply (metis append_Cons append_Nil bsimp_AALTs.simps(3) good.simps(1) k0b)
+ apply force+
+ apply (metis (no_types, lifting) add_Suc add_Suc_right asize.simps(5) bsimp.simps(1) bsimp_ASEQ.simps(19) less_add_Suc1 less_add_Suc2)
+ apply (metis add_Suc add_Suc_right arexp.distinct(5) arexp.distinct(7) asize.simps(4) asize.simps(5) bsimp.simps(1) bsimp.simps(2) bsimp_ASEQ1 good.simps(21) good.simps(8) less_add_Suc1 less_add_Suc2)
+ apply force+
+ apply (metis (no_types, lifting) add_Suc add_Suc_right arexp.distinct(5) arexp.distinct(7) asize.simps(4) asize.simps(5) bsimp.simps(1) bsimp.simps(2) bsimp_ASEQ1 good.simps(25) good.simps(8) less_add_Suc1 less_add_Suc2)
+ apply (metis add_Suc add_Suc_right arexp.distinct(7) asize.simps(4) bsimp.simps(2) bsimp_ASEQ1 good.simps(26) good.simps(8) less_add_Suc1 less_add_Suc2)
+ apply force+
+ done
+
+lemma test2:
+ assumes "good r"
+ shows "bsimp r = r"
using assms
- apply(induct r)
- apply(simp_all)
+ apply(induct r taking: "asize" rule: measure_induct)
+ apply(case_tac x)
+ apply(simp_all)
+ defer
+ (* AALT case *)
+ apply(subgoal_tac "1 < length x52")
+ prefer 2
+ apply(case_tac x52)
+ apply(simp)
+ apply(simp)
+ apply(case_tac list)
+ apply(simp)
+ apply(simp)
+ apply(subst bsimp_AALTs_qq)
+ prefer 2
+ apply(subst flts_qq)
+ apply(auto)[1]
+ apply(auto)[1]
+ apply(case_tac x52)
+ apply(simp)
+ apply(simp)
+ apply(case_tac list)
+ apply(simp)
+ apply(simp)
+ apply(auto)[1]
+ apply (metis (no_types, lifting) bsimp_AALTs.elims good.simps(6) length_Cons length_pos_if_in_set list.size(3) nat_neq_iff)
+ apply(simp)
+ apply(case_tac x52)
+ apply(simp)
+ apply(simp)
+ apply(case_tac list)
+ apply(simp)
+ apply(simp)
+ apply(subst k0)
+ apply(simp)
+ apply(subst (2) k0)
+ apply(simp)
+ apply (simp add: Suc_lessI flts1 one_is_add)
+ (* SEQ case *)
+ apply(case_tac "bsimp x42 = AZERO")
+ apply simp
+ apply (metis asize.elims good.simps(10) good.simps(11) good.simps(12) good.simps(2) good.simps(7) good.simps(9) good_SEQ less_add_Suc1)
+ apply(case_tac "\<exists>bs'. bsimp x42 = AONE bs'")
+ apply(auto)[1]
+ defer
+ apply(case_tac "bsimp x43 = AZERO")
+ apply(simp)
+ apply (metis bsimp.elims bsimp.simps(3) good.simps(10) good.simps(11) good.simps(12) good.simps(8) good.simps(9) good_SEQ less_add_Suc2)
+ apply(auto)
+ apply (subst bsimp_ASEQ1)
+ apply(auto)[3]
+ apply(auto)[1]
+ apply (metis bsimp.simps(3) good.simps(2) good_SEQ less_add_Suc1)
+ apply (metis bsimp.simps(3) good.simps(2) good_SEQ less_add_Suc1 less_add_Suc2)
+ apply (subst bsimp_ASEQ2)
+ apply(drule_tac x="x42" in spec)
+ apply(drule mp)
+ apply(simp)
+ apply(drule mp)
+ apply (metis bsimp.elims bsimp.simps(3) good.simps(10) good.simps(11) good.simps(2) good_SEQ)
+ apply(simp)
+ done
lemma bsimp_idem:
shows "bsimp (bsimp r) = bsimp r"
-apply(induct r taking: "asize" rule: measure_induct)
- apply(case_tac x)
- apply(simp)
- apply(simp)
- apply(simp)
- prefer 3
- apply(simp)
- apply(simp)
- 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(case_tac "length (flts (bsimp a # map bsimp list)) \<le> 1")
- prefer 2
- apply(subst bsimp_AALTs_qq)
- apply(auto)[1]
- apply(simp)
- apply(subst k0)
- apply(simp)
- apply(simp add: flts_append)
- apply(subst (2) k0)
- apply(subst (asm) k0)
- apply(simp)
- apply(subgoal_tac "good (bsimp a) \<or> bsimp a = AZERO")
- prefer 2
- using good1 apply blast
- apply(erule disjE)
- prefer 2
- apply(simp)
- apply(drule_tac x="AALTs x51 list" in spec)
- apply(drule mp)
- apply(simp add: asize0)
- apply(simp)
- apply (simp add: bsimp_AALTs_qq)
- apply(case_tac "nonalt (bsimp a)")
- apply(subst flts_single1)
- apply(simp)
- using nonazero.elims(3) apply force
- apply(simp)
- apply(subst k0b)
- apply(simp)
- apply(auto)[1]
- apply(subst k0b)
- apply(simp)
- apply(auto)[1]
- apply(simp)
- (* HERE *)
- apply(subst (asm) flts_single1)
- apply(simp)
- apply(simp)
- using nonazero.elims(3) apply force
- apply(simp)
- apply(subst (2) bsimp_AALTs_qq)
- apply(auto)[1]
- apply(subst bsimp_AALTs_qq)
- apply(auto)[1]
- apply(case_tac list)
- apply(simp)
- 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")
- apply(simp)
- apply(frule_tac x="AALTs x51 (flts (map bsimp list))" in spec)
- apply(drule mp)
- apply(simp)
- apply (meson add_le_cancel_right asize0 le_trans not_le rt trans_le_add2)
- apply(simp)
- apply(subst (asm) flts_idem)
- apply(auto)[1]
- apply(drule_tac x="r" in spec)
- apply (metis add.commute add_lessD1 not_add_less1 not_less_eq sum_list_map_remove1)
- apply(simp)
- apply(subst flts_idem)
- apply(auto)[1]
- apply(drule_tac x="r" in spec)
- apply (metis add.commute add_lessD1 not_add_less1 not_less_eq sum_list_map_remove1)
- apply(simp)
- apply(case_tac "nonalt (bsimp a)")
- apply(subst k0b)
- apply(simp)
- apply(simp)
- apply(subst k0b)
- apply(simp)
- apply(simp)
- apply(auto)[1]
- apply(frule_tac x="AALTs x51 (bsimp a # flts (map bsimp list))" in spec)
- apply(drule mp)
- apply(simp)
- prefer 2
- apply(simp)
- apply(subst (asm) k0)
- apply(subst (asm) flts_idem)
- apply(auto)[1]
- apply (simp add: sum_list_map_remove1)
- apply(subst (asm) k0b)
- apply(simp)
- apply(simp)
- apply(simp)
- apply(subst k0)
- apply(subst flts_idem)
- apply(auto)[1]
- apply (simp add: sum_list_map_remove1)
- apply(subst k0b)
- apply(simp)
- apply(simp)
- apply(simp)
-lemma XX_bder:
- shows "bsimp (bder c (bsimp r)) = (bsimp \<circ> bder c) r"
- apply(induct r)
- apply(simp)
- apply(simp)
- apply(simp)
- prefer 3
- apply(simp)
- prefer 2
- apply(simp)
- apply(case_tac x2a)
- apply(simp)
- apply(simp)
- apply(auto)[1]
+ using test good1
+ by force
lemma q3a:
@@ -1760,360 +1703,6 @@
apply(simp_all)
done
-
-fun extr :: "arexp \<Rightarrow> (bit list) set" where
- "extr (AONE bs) = {bs}"
-| "extr (ACHAR bs c) = {bs}"
-| "extr (AALTs bs (r#rs)) =
- {bs @ bs' | bs'. bs' \<in> extr r} \<union>
- {bs @ bs' | bs'. bs' \<in> extr (AALTs [] rs)}"
-| "extr (ASEQ bs r1 r2) =
- {bs @ bs1 @ bs2 | bs1 bs2. bs1 \<in> extr r1 \<and> bs2 \<in> extr r2}"
-| "extr (ASTAR bs r) = {bs @ [S]} \<union>
- {bs @ [Z] @ bs1 @ bs2 | bs1 bs2. bs1 \<in> extr r \<and> bs2 \<in> extr (ASTAR [] r)}"
-
-
-lemma MAIN_decode:
- assumes "\<Turnstile> v : ders s r"
- shows "Some (flex r id s v) = decode (retrieve (bders_simp (intern r) s) v) r"
- using assms
-proof (induct s arbitrary: v rule: rev_induct)
- case Nil
- have "\<Turnstile> v : ders [] r" by fact
- then have "\<Turnstile> v : r" by simp
- then have "Some v = decode (retrieve (intern r) v) r"
- using decode_code retrieve_code by auto
- then show "Some (flex r id [] v) = decode (retrieve (bders_simp (intern r) []) v) r"
- by simp
-next
- case (snoc c s v)
- have IH: "\<And>v. \<Turnstile> v : ders s r \<Longrightarrow>
- Some (flex r id s v) = decode (retrieve (bders_simp (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)
- 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_simp (intern r) s) (injval (ders s r) c v)) r"
- using asm2 IH by simp
- also have "... = decode (retrieve (bder c (bders_simp (intern r) s)) v) r"
- using asm bder_retrieve ders_append
- apply -
- apply(drule_tac x="v" in meta_spec)
- apply(drule_tac x="c" in meta_spec)
- apply(drule_tac x="bders_simp (intern r) s" in meta_spec)
- apply(drule_tac meta_mp)
- apply(simp add: ders_append)
- defer
- apply(simp)
- oops
-
-fun vsimp :: "arexp \<Rightarrow> val \<Rightarrow> val"
- where
- "vsimp (ASEQ _ (AONE _) r) (Seq v1 v2) = vsimp r v1"
-| "vsimp _ v = v"
-
-lemma fuse_vsimp:
- assumes "\<Turnstile> v : (erase r)"
- shows "vsimp (fuse bs r) v = vsimp r v"
- using assms
- apply(induct r arbitrary: v bs)
- apply(simp_all)
- apply(case_tac "\<exists>bs. r1 = AONE bs")
- apply(auto)
- apply (metis Prf_elims(2) vsimp.simps(1))
- apply(erule Prf_elims)
- apply(auto)
- apply(case_tac r1)
- apply(auto)
- done
-
-
-lemma retrieve_XXX0:
- assumes "\<And>r v. \<lbrakk>r \<in> set rs; \<Turnstile> v : erase r\<rbrakk> \<Longrightarrow>
- \<exists>v'. \<Turnstile> v' : erase (bsimp r) \<and> retrieve (bsimp r) v' = retrieve r v"
- "\<Turnstile> v : erase (AALTs bs rs)"
- shows "\<exists>v'. \<Turnstile> v' : erase (bsimp_AALTs bs (flts (map bsimp rs))) \<and>
- retrieve (bsimp_AALTs bs (flts (map bsimp rs))) v' = retrieve (AALTs bs rs) v"
- using assms
-apply(induct rs arbitrary: bs v taking: size rule: measure_induct)
- apply(case_tac x)
- apply(simp)
- using Prf_elims(1) apply blast
- apply(simp)
- apply(case_tac list)
- apply(simp_all)
- apply(case_tac a)
- apply(simp_all)
- using Prf_elims(1) apply blast
- apply (metis erase.simps(2) fuse.simps(2) retrieve_fuse2)
- using Prf_elims(5) apply force
- apply(erule Prf_elims)
- apply(auto)[1]
-
-
-
-
- apply(simp)
- apply(erule Prf_elims)
- using Prf_elims(1) apply b last
- apply(auto)
- apply (metis append_Ni l2 erase_fuse fuse.simps(4) retrieve_fuse2)
- apply(case_tac rs)
- apply(auto)
-
-
- oops
-
-fun get where
- "get (Some v) = v"
-
-
-lemma retrieve_XXX:
- assumes "\<Turnstile> v : erase r"
- shows "\<Turnstile> get (decode (code v) (erase (bsimp r))) : erase (bsimp r)"
- using assms
-apply(induct r arbitrary: v)
- apply(simp)
- using Prf_elims(1) apply auto[1]
- apply(simp)
- apply (simp add: decode_code)
- apply(simp)
- apply (simp add: decode_code)
- apply(simp)
- apply(erule Prf_elims)
- apply(simp)
- apply(case_tac "r1 = AZERO")
- apply(simp)
- apply (meson Prf_elims(1) Prf_elims(2))
- apply(case_tac "r2 = AZERO")
- apply(simp)
- apply (meson Prf_elims(1) Prf_elims(2))
- apply(case_tac "\<exists>bs. bsimp r1 = AONE bs")
- apply(clarify)
- apply(simp)
- apply(subst bsimp_ASEQ2)
- apply(subst bsimp_ASEQ2)
- apply(simp add: erase_fuse)
- apply(case_tac r1)
- apply(simp_all)
- using Prf_elims(4) apply fastforce
- apply(erule Prf_elims)
- apply(simp)
-
- apply(simp)
-
-
- defer
- apply(subst bsimp_ASEQ1)
- using L_bsimp_erase L_flat_Prf1 L_flat_Prf2 apply fast force
- using L_bsimp_erase L_
-
-lemma retrieve_XXX:
- assumes "\<Turnstile> v : erase r"
- shows "\<Turnstile> (vsimp (bsimp r) v : erase (bsimp r) \<and> retrieve (bsimp r) (vsimp (bsimp r) v) = retrieve r v"
- using assms
- apply(induct r arbitrary: v)
- apply(simp)
- using Prf_elims(1) apply blast
- apply(simp)
- using Prf_elims(4) apply fastforce
- apply(simp)
- apply blast
- apply simp
- apply(case_tac "r1 = AZERO")
- apply(simp)
- apply (meson Prf_elims(1) Prf_elims(2))
- apply(case_tac "r2 = AZERO")
- apply(simp)
- apply (meson Prf_elims(1) Prf_elims(2))
- apply(erule Prf_elims)
- apply(simp)
- apply(case_tac "\<exists>bs. bsimp r1 = AONE bs")
- apply(clarify)
- apply(simp)
- apply(subst bsimp_ASEQ2)
- 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 fastforce
- apply(simp)
- apply(simp)
- apply(drule_tac x="v1" in meta_spec)
- apply(drule_tac x="v2" in meta_spec)
- apply(simp)
- apply(clarify)
- apply(rule_tac x="Seq v' v'a" in exI)
- apply(simp)
- apply (metis Prf.intros(1) Prf_elims(1) bsimp_ASEQ1 erase.simps(1) retrieve.simps(6))
- prefer 3
- apply(drule_tac x="v1" in meta_spec)
- apply(drule_tac x="v2" in meta_spec)
- apply(simp)
- apply(clarify)
- apply(rule_tac x="v'a" in exI)
- apply(subst bsimp_ASEQ2)
- apply (metis Prf_elims(4) append_assoc erase_fuse retrieve.simps(1) retrieve_fuse2)
- prefer 2
- apply(auto)
- apply(case_tac "x2a")
- apply(simp)
- using Prf_elims(1) apply blast
- apply(simp)
- apply(case_tac "list")
- apply(simp)
- sorry
-
-
-lemma retrieve_XXX:
- assumes "\<Turnstile> v : erase r"
- shows "\<exists>v'. \<Turnstile> v' : erase (bsimp r) \<and> retrieve (bsimp r) v' = retrieve r v"
- using assms
- apply(induct r arbitrary: v)
- apply(simp)
- using Prf_elims(1) apply blast
- apply(simp)
- using Prf_elims(4) apply fastforce
- apply(simp)
- apply blast
- apply simp
- apply(case_tac "r1 = AZERO")
- apply(simp)
- apply (meson Prf_elims(1) Prf_elims(2))
- apply(case_tac "r2 = AZERO")
- apply(simp)
- apply (meson Prf_elims(1) Prf_elims(2))
- apply(erule Prf_elims)
- apply(simp)
- apply(case_tac "\<exists>bs. bsimp r1 = AONE bs")
- apply(clarify)
- apply(simp)
- apply(subst bsimp_ASEQ2)
- 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 fastforce
- apply(simp)
- apply(simp)
- apply(drule_tac x="v1" in meta_spec)
- apply(drule_tac x="v2" in meta_spec)
- apply(simp)
- apply(clarify)
- apply(rule_tac x="Seq v' v'a" in exI)
- apply(simp)
- apply (metis Prf.intros(1) Prf_elims(1) bsimp_ASEQ1 erase.simps(1) retrieve.simps(6))
- prefer 3
- apply(drule_tac x="v1" in meta_spec)
- apply(drule_tac x="v2" in meta_spec)
- apply(simp)
- apply(clarify)
- apply(rule_tac x="v'a" in exI)
- apply(subst bsimp_ASEQ2)
- apply (metis Prf_elims(4) append_assoc erase_fuse retrieve.simps(1) retrieve_fuse2)
- prefer 2
- apply(auto)
- apply(case_tac "x2a")
- apply(simp)
- using Prf_elims(1) apply blast
- apply(simp)
- apply(case_tac "list")
- apply(simp)
- sorry
-
-
-lemma TEST:
- assumes "\<Turnstile> v : ders s r"
- shows "\<exists>v'. retrieve (bders (intern r) s) v' = retrieve (bsimp (bders (intern r) s)) v"
- using assms
- apply(induct s arbitrary: r v rule: rev_induct)
- apply(simp)
-
- defer
- apply(simp add: ders_append)
- apply(frule Prf_injval)
- apply(drule_tac x="r" in meta_spec)
- apply(drule_tac x="injval (ders xs r) x v" in meta_spec)
- apply(simp)
- apply(simp add: bders_append)
- apply(subst bder_retrieve)
- apply(simp)
- apply(simp)
- thm bder_retrieve
- thm bmkeps_retrieve
-
-
-lemma bmkeps_simp2:
- assumes "bnullable (bder c r)"
- shows "bmkeps (bder c (bsimp r)) = bmkeps (bder c r)"
- using assms
- apply(induct r)
- apply(simp)
- apply(simp)
- apply(simp)
- prefer 3
- apply(simp)
- apply(simp)
- apply(auto)[1]
- prefer 2
- apply(case_tac "r1 = AZERO")
- apply(simp)
- apply(case_tac "r2 = AZERO")
- apply(simp)
- apply(case_tac "\<exists>bs. (bsimp r1) = AONE bs")
- apply(clarify)
- apply(simp)
- apply(subst bsimp_ASEQ2)
-
- apply(simp add: bmkeps_simp)
- apply(simp add: bders_append)
- apply(drule_tac x="bder a r" in meta_spec)
- apply(simp)
- apply(simp)
- apply(simp)
- prefer 3
- apply(simp)
- prefer 2
- apply(simp)
- apply(case_tac x2a)
- apply(simp)
- apply(simp add: )
- apply(subst k0)
- apply(auto)[1]
- apply(case_tac list)
- apply(simp)
-
-
- apply(case_tac "r1=AZERO")
- apply(simp)
- apply(case_tac "r2=AZERO")
- apply(simp)
- apply(auto)[1]
- apply(case_tac "\<exists>bs. r1=AONE bs")
- apply(simp)
- apply(auto)[1]
- apply(subst bsimp_ASEQ2)
-
-
- prefer 2
- apply(simp)
- apply(subst bmkeps_bder_AALTs)
- apply(case_tac x2a)
- apply(simp)
- apply(simp)
- apply(auto)[1]
- apply(subst bmkeps_bder_AALTs)
-
- apply(case_tac a)
- apply(simp_all)
- apply(auto)[1]
- apply(case_tac list)
- apply(simp)
- apply(simp)
-
- prefer 2
- apply(simp)
-
-
lemma bbs0:
shows "blexer_simp r [] = blexer r []"
apply(simp add: blexer_def blexer_simp_def)
@@ -2130,341 +1719,12 @@
apply(simp)
apply(simp)
done
-
-lemma bbs1:
- shows "blexer_simp r [c1, c2] = blexer r [c1, c2]"
- apply(simp add: blexer_def blexer_simp_def)
- apply(auto)
- defer
- apply (metis L_bsimp_erase bnullable_correctness der_correctness erase_bder lexer.simps(1) lexer_correct_None option.distinct(1))
- apply (metis L_bsimp_erase bnullable_correctness der_correctness erase_bder lexer.simps(1) lexer_correct_None option.distinct(1))
- apply(subst bmkeps_simp[symmetric])
- using b3 apply auto[1]
- apply(subst bmkeps_retrieve)
- using b3 bnullable_correctness apply blast
- apply(subst bder_retrieve)
- using b3 bnullable_correctness mkeps_nullable apply fastforce
- apply(subst bmkeps_retrieve)
- using bnullable_correctness apply blast
- apply(subst bder_retrieve)
- using bnullable_correctness mkeps_nullable apply force
-
- using bder_retrieve bmkeps_simp bmkeps_retrieve
-
-
-
-lemma bsimp_retrieve_bder:
- assumes "\<Turnstile> v : der c (erase r)"
- shows "retrieve (bder c r) v = retrieve (bsimp (bder c r)) v"
- thm bder_retrieve bmkeps_simp
- apply(induct r arbitrary: c v)
- apply(simp)
- apply(simp)
- apply(simp)
- apply(auto)[1]
- apply(case_tac "bsimp (bder c r1) = AZERO")
- apply(simp)
-
- prefer 3
- apply(simp)
- apply(auto elim!: Prf_elims)[1]
- apply(case_tac "(bsimp (fuse [Z] (bder c r))) = AZERO")
- apply(simp)
- 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)) = {[]}")
- prefer 2
- apply (metis L.simps(2) L_bsimp_erase erase.simps(2) erase_bder erase_fuse)
- apply(simp)
-
-
-
- apply(subst bsimp_ASEQ1)
- apply(simp)
- apply(simp)
- apply(auto)[1]
-
- prefer 2
-
lemma oo:
shows "(case (blexer (der c r) s) of None \<Rightarrow> None | Some v \<Rightarrow> Some (injval r c v)) = blexer r (c # s)"
apply(simp add: blexer_correctness)
done
-lemma oo2a:
- assumes "\<forall>r. bmkeps (bders_simp r s) = bmkeps (bders r s)" "c # s \<in> L r"
- "bnullable (bders_simp (bsimp (bder c (intern r))) s)"
- shows "(case (blexer_simp (der c r) s) of None \<Rightarrow> None | Some v \<Rightarrow> Some (injval r c v)) = blexer_simp r (c # s)"
- using assms
- apply(simp add: blexer_simp_def)
- apply(auto split: option.split)
- apply (metis blexer_correctness blexer_def lexer.simps(2) lexer_correct_None option.simps(4))
- prefer 2
- apply (metis L_bders_simp L_bsimp_erase Posix1(1) Posix_mkeps bnullable_correctness ders_correctness erase_bder erase_bders erase_intern lexer.simps(1) lexer_correct_None)
- apply(subst bmkeps_retrieve)
- using L_bders_simp bnullable_correctness nullable_correctness apply blast
-
- thm bder_retrieve
-
-
- apply(subst bder_retrieve[symmetric])
-
-
-
- apply(drule_tac x="bsimp (bder c (intern r))" in spec)
- apply(drule sym)
- apply(simp)
- apply(subst blexer_simp_def)
- apply(case_tac "bnullable (bders_simp (intern (der c r)) s)")
- apply(simp)
- apply(auto split: option.split)
- apply(subst oo)
- apply(simp)
- done
-
-
-
-lemma oo3:
- assumes "\<forall>r. bders r s = bders_simp r s"
- shows "blexer_simp r (s @ [c]) = blexer r (s @ [c])"
- using assms
- apply(simp (no_asm) add: blexer_simp_def)
- apply(auto)
- prefer 2
- apply (metis L_bders_simp blexer_def bnullable_correctness lexer.simps(1) lexer_correct_None option.distinct(1))
- apply(simp add: bders_simp_append)
- apply(subst bmkeps_simp[symmetric])
- using b3 apply auto[1]
- apply(simp add: blexer_def)
- apply(auto)[1]
- prefer 2
- apply (metis (mono_tags, lifting) L_bders_simp Posix_mkeps append.right_neutral bders_simp.simps(1) bders_simp.simps(2) bders_simp_append bnullable_correctness lexer.simps(1) lexer_correct_None lexer_correctness(1) option.distinct(1))
- apply(simp add: bders_append)
- done
-
-lemma oo4:
- assumes "\<forall>r. bmkeps (bders r s) = bmkeps (bders_simp r s)" "bnullable (bder c (bders r s))"
- shows "bmkeps (bders_simp r (s @ [c])) = bmkeps (bders r (s @ [c]))"
- using assms
- apply(simp add: bders_simp_append)
- apply(subst bmkeps_simp[symmetric])
- apply (metis L_bders_simp bnullable_correctness der_correctness erase_bder lexer.simps(1) lexer_correct_None option.distinct(1))
- apply(simp add: bders_append)
- done
-
-lemma oo4:
- shows "blexer_simp r s = blexer r s"
- apply(induct s arbitrary: r rule: rev_induct)
- apply(simp only: blexer_simp_def blexer_def)
- apply(simp)
- apply(simp only: blexer_simp_def blexer_def)
- apply(subgoal_tac "bnullable (bders_simp (intern r) (xs @ [x])) = bnullable (bders (intern r) (xs @ [x]))")
- prefer 2
- apply (simp add: b4)
- apply(simp)
- apply(rule impI)
- apply(simp add: bders_simp_append)
- apply(subst bmkeps_simp[symmetric])
- using b3 apply auto[1]
- apply(subst bmkeps_retrieve)
- using b3 bnullable_correctness apply blast
- apply(subst bder_retrieve)
- using b3 bnullable_correctness mkeps_nullable apply fastforce
- apply(simp add: bders_append)
- apply(subst bmkeps_retrieve)
- using bnullable_correctness apply blast
- apply(subst bder_retrieve)
- using bnullable_correctness mkeps_nullable apply fastforce
- apply(subst erase_bder)
- apply(case_tac "xs \<in> L")
- apply(subst (asm) (2) bmkeps_retrieve)
-
-
- thm bmkeps_retrieve bmkeps_retrieve
- apply(subst bmkeps_retrieve[symmetric])
-
- apply (simp add: bnullable_correctness)
- apply(simp add: bders_simp_append)
-
-
- apply(induct s arbitrary: r rule: rev_induct)
- apply(simp add: blexer_def blexer_simp_def)
- apply(rule oo3)
- apply(simp (no_asm) add: blexer_simp_def)
- apply(auto)
- prefer 2
- apply (metis L_bders_simp blexer_def bnullable_correctness lexer.simps(1) lexer_correct_None option.distinct(1))
- apply(simp add: bders_simp_append)
- apply(subst bmkeps_simp[symmetric])
- using b3 apply auto[1]
- apply(simp add: blexer_def)
- apply(auto)[1]
- prefer 2
- apply (m etis (mono_tags, lifting) L_bders_simp Posix_mkeps append.right_neutral bders_simp.simps(1) bders_simp.simps(2) bders_simp_append bnullable_correctness lexer.simps(1) lexer_correct_None lexer_correctness(1) option.distinct(1))
- apply(simp add: bders_append)
- oops
-
-
-lemma bnullable_simp:
- assumes "s \<in> L (erase r)"
- shows "bmkeps (bders r s) = bmkeps (bders_simp r s)"
- using assms
- apply(induct s arbitrary: r rule: rev_induct)
- apply(simp)
- apply(simp add: bders_append bders_simp_append)
- apply(subst bmkeps_simp[symmetric])
- apply (metis L_bders_simp b3 bders_simp.simps(1) bders_simp.simps(2) bders_simp_append blexer_correctness blexer_def bnullable_correctness erase_bders erase_intern lexer.simps(1) lexer_correct_None lexer_correct_Some lexer_correctness(1))
- apply(subst bmkeps_retrieve)
- apply (metis bders.simps(1) bders.simps(2) bders_append blexer_correctness blexer_def bnullable_correctness erase_bders erase_intern lexer_correct_Some option.distinct(1))
- apply(subst bmkeps_retrieve)
- apply (metis L_bders_simp L_bsimp_erase Posix_mkeps bders_simp.simps(1) bders_simp.simps(2) bders_simp_append blexer_correctness blexer_def bnullable_correctness erase_bders erase_intern lexer.simps(1) lexer_correct_None lexer_correctness(2))
- apply(subst bder_retrieve)
- apply (metis bders.simps(1) bders.simps(2) bders_append blexer_correctness blexer_def bnullable_correctness erase_bder erase_bders erase_intern lexer_correct_Some mkeps_nullable option.distinct(1))
- apply(subst bder_retrieve)
- apply (metis L_bders_simp L_bsimp_erase Posix_mkeps bders_simp.simps(1) bders_simp.simps(2) bders_simp_append blexer_correctness blexer_def bnullable_correctness erase_bder erase_bders erase_intern lexer.simps(1) lexer_correct_None lexer_correctness(2) mkeps_nullable)
-
- apply(drule_tac x="bder a r" in meta_spec)
- apply(drule_tac meta_mp)
- apply (me tis erase_bder lexer.simps(2) lexer_correct_None option.simps(4))
- apply(simp)
- oops
-
-
-lemma
- shows "blexer r s = blexer_simp r s"
- apply(induct s arbitrary: r rule: rev_induct)
- apply(simp add: blexer_def blexer_simp_def)
- apply(case_tac "xs @ [x] \<in> L r")
- defer
- apply(subgoal_tac "blexer (ders xs r) [x] = None")
- prefer 2
- apply(subst blexer_correctness)
- apply(simp (no_asm) add: lexer_correct_None)
- apply(simp add: nullable_correctness)
- apply(simp add: der_correctness ders_correctness)
- apply(simp add: Der_def Ders_def)
-apply(subgoal_tac "blexer r (xs @ [x]) = None")
- prefer 2
- apply (simp add: blexer_correctness)
- using lexer_correct_None apply auto[1]
- apply(simp)
- apply(subgoal_tac "blexer_simp (ders xs r) [x] = None")
- prefer 2
- apply (metis L_bders_simp Posix_injval Posix_mkeps bders.simps(2) blexer_correctness blexer_simp_def bnullable_correctness ders.simps(1) erase_bder erase_bders erase_intern lexer_correct_None lexer_correctness(2))
- apply(subgoal_tac "[] \<notin> L (erase (bders_simp (intern r) (xs @ [x])))")
- prefer 2
- apply(metis L_bders_simp Posix_injval bders.simps(2) blexer_correctness ders.simps(1) ders_append erase_bder erase_bders erase_intern lexer_correct_None lexer_correctness(2))
- using blexer_simp_def bnullable_correctness lexer_correct_None apply auto[1]
-(* case xs @ [x] \<in> L r *)
- apply(subgoal_tac "\<exists>v. blexer (ders xs r) [x] = Some v \<and> [x] \<in> (ders xs r) \<rightarrow> v")
- prefer 2
- using blexer_correctness lexer_correct_Some apply auto[1]
- apply (simp add: Posix_injval Posix_mkeps)
- apply (metis ders.simps(1) ders.simps(2) ders_append lexer_correct_None lexer_flex)
- apply(clarify)
- apply(subgoal_tac "blexer_simp (ders xs r) [x] = Some v")
- prefer 2
- apply(simp add: blexer_simp_def)
- apply(auto)[1]
- apply (metis bders.simps(1) bders.simps(2) blexer_def bmkeps_simp option.simps(3))
- using b3 blexer_def apply fastforce
- apply(subgoal_tac "blexer_simp (ders xs r) [x] = blexer_simp r (xs @ [x])")
- prefer 2
- apply(simp add: blexer_simp_def)
-
- apply(simp)
-
-
-
- apply(simp)
- apply(subst blexer_simp_def)
- apply(simp)
- apply(auto)
- apply(drule_tac x="der a r" in meta_spec)
- apply(subst blexer_def)
- apply(subgoal_tac "bnullable (bders (intern r) (a # s))")
- prefer 2
- apply (me tis Posix_injval blexer_correctness blexer_def lexer_correctness(2))
- apply(simp)
-
-
-
-lemma
- shows "blexer r s = blexer_simp r s"
- apply(induct s arbitrary: r)
- apply(simp add: blexer_def blexer_simp_def)
- apply(case_tac "s \<in> L (der a r)")
- defer
- apply(subgoal_tac "blexer (der a r) s = None")
- prefer 2
- apply (simp add: blexer_correctness lexer_correct_None)
-apply(subgoal_tac "blexer r (a # s) = None")
- prefer 2
- apply (simp add: blexer_correctness)
- apply(simp)
-
- apply(subst blexer_simp_def)
- apply(simp)
- apply(drule_tac x="der a r" in meta_spec)
- apply(subgoal_tac "s \<notin> L(erase (bder a (intern r)))")
- prefer 2
- apply simp
-
- apply(simp only:)
- apply(subst blexer_simp_def)
- apply(subgoal_tac "\<not> bnullable (bders_simp (intern r) (a # s))")
- apply(simp)
- apply(subst bnullable_correctness[symmetric])
- apply(simp)
- oops
-
-
-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)"
@@ -2472,134 +1732,428 @@
apply(simp_all)
done
-lemma XXX2:
+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'"
+ shows "flts (map (bsimp \<circ> bder c) (flts (map bsimp rs))) = flts (map (bsimp \<circ> bder c) rs)"
+ using assms
+ apply(induct rs arbitrary: c)
+ apply(simp)
+ apply(simp)
+ apply(subst k0)
+ apply(simp add: flts_append)
+ apply(subst (2) k0)
+ apply(simp add: flts_append)
+ apply(subgoal_tac "flts [a] = [a]")
+ prefer 2
+ using good.simps(1) k0b apply blast
+ apply(simp)
+ done
+
+lemma bmkeps_good:
+ assumes "good a"
+ shows "bmkeps (bsimp a) = bmkeps a"
+ using assms
+ using test2 by auto
+
+
+lemma xxx_bder:
+ assumes "good r"
+ shows "L (erase r) \<noteq> {}"
+ using assms
+ apply(induct r rule: good.induct)
+ apply(auto simp add: Sequ_def)
+ done
+
+lemma xxx_bder2:
+ assumes "L (erase (bsimp r)) = {}"
+ shows "bsimp r = AZERO"
+ using assms xxx_bder test2 good1
+ by blast
+
+lemma XXX2aa:
+ assumes "good a"
shows "bsimp (bder c (bsimp a)) = bsimp (bder c a)"
- apply(induct a arbitrary: c)
+ using assms
+ by (simp add: test2)
+
+lemma XXX2aa_ders:
+ assumes "good a"
+ shows "bsimp (bders (bsimp a) s) = bsimp (bders a s)"
+ using assms
+ by (simp add: test2)
+
+lemma XXX4a:
+ shows "good (bders_simp (bsimp r) s) \<or> bders_simp (bsimp r) s = AZERO"
+ apply(induct s arbitrary: r rule: rev_induct)
+ apply(simp)
+ apply (simp add: good1)
+ apply(simp add: bders_simp_append)
+ apply (simp add: good1)
+ done
+
+lemma XXX4a_good:
+ assumes "good a"
+ shows "good (bders_simp a s) \<or> bders_simp a s = AZERO"
+ using assms
+ apply(induct s arbitrary: a rule: rev_induct)
+ apply(simp)
+ apply(simp add: bders_simp_append)
+ apply (simp add: good1)
+ done
+
+lemma XXX4a_good_cons:
+ assumes "s \<noteq> []"
+ shows "good (bders_simp a s) \<or> bders_simp a s = AZERO"
+ using assms
+ apply(case_tac s)
+ apply(auto)
+ using XXX4a by blast
+
+lemma XXX4b:
+ assumes "good a" "L (erase (bders_simp a s)) \<noteq> {}"
+ shows "good (bders_simp a s)"
+ using assms
+ apply(induct s arbitrary: a)
+ apply(simp)
+ apply(simp)
+ apply(subgoal_tac "L (erase (bder a aa)) = {} \<or> L (erase (bder a aa)) \<noteq> {}")
+ prefer 2
+ apply(auto)[1]
+ apply(erule disjE)
+ apply(subgoal_tac "bsimp (bder a aa) = AZERO")
+ prefer 2
+ using L_bsimp_erase xxx_bder2 apply auto[1]
+ apply(simp)
+ apply (metis L.simps(1) XXX4a erase.simps(1))
+ apply(drule_tac x="bsimp (bder a aa)" in meta_spec)
+ apply(drule meta_mp)
+ apply simp
+ apply(rule good1a)
+ apply(auto)
+ done
+
+lemma bders_AZERO:
+ shows "bders AZERO s = AZERO"
+ and "bders_simp AZERO s = AZERO"
+ apply (induct s)
+ apply(auto)
+ done
+
+lemma ZZ0:
+ assumes "bsimp a = AALTs bs rs"
+ shows "bsimp (bder c a) = AALTs bs (map (bder c) rs)"
+ using assms
+ apply(induct a arbitrary: rs bs c)
+ apply(simp_all)
+ apply(auto)[1]
+ prefer 2
+ apply (metis arexp.distinct(25) arexp.distinct(7) b3 bnullable.simps(2) bsimp_ASEQ.simps(1) bsimp_ASEQ0 bsimp_ASEQ1)
+ prefer 2
+ oops
+
+
+lemma ZZZ:
+ assumes "\<forall>y. asize y < Suc (sum_list (map asize x52)) \<longrightarrow> bsimp (bder c (bsimp y)) = bsimp (bder c y)"
+ shows "bsimp (bder c (bsimp_AALTs x51 (flts (map bsimp x52)))) = bsimp_AALTs x51 (flts (map (bsimp \<circ> bder c) x52))"
+ using assms
+ apply(induct x52)
+ apply(simp)
+ apply(simp)
+ apply(case_tac "bsimp a = AZERO")
+ apply(simp)
+ apply(subgoal_tac "bsimp (bder c a) = AZERO")
+ prefer 2
+ using less_add_Suc1 apply fastforce
+ apply(simp)
+ apply(case_tac "\<exists>bs rs. bsimp a = AALTs bs rs")
+ apply(clarify)
+ apply(simp)
+ apply(subst k0)
+ apply(case_tac "rs = []")
+ apply(simp)
+ apply(subgoal_tac "bsimp (bder c a) = AALTs bs []")
+ apply(simp)
+ apply (metis arexp.distinct(7) good.simps(4) good1)
+ oops
+
+
+
+
+lemma bders_snoc:
+ "bder c (bders a s) = bders a (s @ [c])"
+ apply(simp add: bders_append)
+ done
+
+lemma
+ assumes "bnullable (bders a s)" "good a"
+ shows "bmkeps (bders_simp a s) = bmkeps (bders a s)"
+ using assms
+ apply(induct s arbitrary: a)
+ apply(simp)
+ apply(simp add: bders_append bders_simp_append)
+ apply(drule_tac x="bsimp (bsimp (bder a aa))" in meta_spec)
+ apply(drule meta_mp)
+ apply (metis b4 bders.simps(2) bders_simp.simps(2) bsimp_idem)
+ apply(subgoal_tac "good (bsimp (bder a aa)) \<or> bsimp (bder a aa) = AZERO")
+ apply(auto simp add: bders_AZERO)
+ prefer 2
+ apply (metis b4 bders.simps(2) bders_AZERO(2) bders_simp.simps(2) bnullable.simps(1))
+ prefer 2
+ using good1 apply auto[1]
+ apply(drule meta_mp)
+ apply (simp add: bsimp_idem)
+ apply (subst (asm) (1) bsimp_idem)
+ apply(simp)
+ apply(subst (asm) (2) bmkeps_simp)
+ apply (metis b4 bders.simps(2) bders_simp.simps(2) bsimp_idem)
+ apply (subst (asm) (1) bsimp_idem)
+ apply(simp)
+ defer
+ oops
+
+
+lemma
+ shows "bmkeps (bders (bders_simp a s2) s1) = bmkeps (bders_simp a (s2 @ s1))"
+ apply(induct s2 arbitrary: a s1)
+ apply(simp)
+ defer
+ apply(simp add: bders_append bders_simp_append)
+ oops
+
+lemma QQ1:
+ shows "bsimp (bders (bsimp a) []) = bders_simp (bsimp a) []"
+ apply(simp)
+ apply(simp add: bsimp_idem)
+ done
+
+lemma QQ2:
+ shows "bsimp (bders (bsimp a) [c]) = bders_simp (bsimp a) [c]"
+ apply(simp)
+ done
+
+lemma QQ3:
+ assumes "good a"
+ shows "bmkeps (bsimp (bders (bsimp a) [c1, c2])) = bmkeps (bders_simp (bsimp a) [c1, c2])"
+ using assms
+ apply(simp)
+
+ oops
+
+lemma QQ4:
+ shows "bmkeps (bsimp (bders (bsimp a) [c1, c2, c3])) = bmkeps (bders_simp (bsimp a) [c1, c2, c3])"
+ apply(simp)
+ oops
+
+lemma QQ3:
+ assumes "good a"
+ shows "bsimp (bders (bders_simp a s2) s1)= bders_simp a (s1 @ s2)"
+ using assms
+ apply(induct s2 arbitrary: a s1)
+ apply(simp)
+ oops
+
+lemma XXX2a_long:
+ assumes "good a"
+ shows "bsimp (bder c (bsimp a)) = bsimp (bder c a)"
+ using assms
+ apply(induct a arbitrary: c taking: asize rule: measure_induct)
+ apply(case_tac x)
apply(simp)
apply(simp)
apply(simp)
prefer 3
apply(simp)
+ apply(simp)
apply(auto)[1]
- apply(case_tac "(bsimp a1) = AZERO")
+apply(case_tac "x42 = AZERO")
+ apply(simp)
+ apply(case_tac "x43 = AZERO")
apply(simp)
+ using test2 apply force
+ apply(case_tac "\<exists>bs. x42 = AONE bs")
+ apply(clarify)
+ apply(simp)
+ apply(subst bsimp_ASEQ1)
+ apply(simp)
using b3 apply force
- apply(case_tac "(bsimp a2) = AZERO")
+ using bsimp_ASEQ0 test2 apply force
+ thm good_SEQ test2
+ apply (simp add: good_SEQ test2)
+ apply (simp add: good_SEQ test2)
+ apply(case_tac "x42 = 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(case_tac "x43 = AZERO")
+ apply(simp)
+ apply (simp add: bsimp_ASEQ0)
+ apply(case_tac "\<exists>bs. x42 = AONE bs")
apply(clarify)
apply(simp)
- apply(subst bsimp_ASEQ2)
- apply(subgoal_tac "bmkeps a1 = bs")
+ apply(subst bsimp_ASEQ1)
+ apply(simp)
+ using bsimp_ASEQ0 test2 apply force
+ apply (simp add: good_SEQ test2)
+ apply (simp add: good_SEQ test2)
+ apply (simp add: good_SEQ test2)
+ (* AALTs case *)
+ apply(simp)
+ using test2 by fastforce
+
+lemma XXX2a_long_without_good:
+ shows "bsimp (bder c (bsimp a)) = bsimp (bder c a)"
+ apply(induct a arbitrary: c taking: asize rule: measure_induct)
+ apply(case_tac x)
+ apply(simp)
+ apply(simp)
+ apply(simp)
+ prefer 3
+ apply(simp)
+ apply(simp)
+ apply(auto)[1]
+apply(case_tac "x42 = AZERO")
+ apply(simp)
+ apply(case_tac "bsimp x43 = AZERO")
+ apply(simp)
+ apply (simp add: bsimp_ASEQ0)
+ apply(subgoal_tac "bsimp (fuse (bmkeps x42) (bder c x43)) = AZERO")
+ apply(simp)
+ apply (metis bder.simps(1) bsimp.simps(3) bsimp_fuse fuse.simps(1) less_add_Suc2)
+ apply(case_tac "\<exists>bs. bsimp x42 = AONE bs")
+ apply(clarify)
+ apply(simp)
+ apply(subst bsimp_ASEQ2)
+ apply(subgoal_tac "bsimp (bder c x42) = AZERO")
+ apply(simp)
+ prefer 2
+ using less_add_Suc1 apply fastforce
+ apply(subgoal_tac "bmkeps x42 = bs")
prefer 2
apply (simp add: bmkeps_simp)
apply(simp)
- apply(subst (1) bsimp_fuse[symmetric])
- defer
- apply(subst bsimp_ASEQ1)
+ apply(case_tac "nonalt (bsimp (bder c x43))")
+ apply (metis bder_fuse bsimp_AALTs.simps(1) bsimp_AALTs.simps(2) bsimp_fuse flts.simps(1) flts.simps(2) fuse.simps(1) fuse_append k0b less_add_Suc2 nn11a)
+ apply(subgoal_tac "nonnested (bsimp (bder c x43))")
+ prefer 2
+ using nn1b apply blast
+ apply(case_tac x43)
+ apply(simp)
+ apply(simp)
+ apply(simp)
+ prefer 3
+ apply(simp)
+ apply (metis arexp.distinct(25) arexp.distinct(7) arexp.distinct(9) bsimp_ASEQ.simps(1) bsimp_ASEQ.simps(11) bsimp_ASEQ1 nn11a nonalt.elims(3) nonalt.simps(6))
+ apply(simp)
+ apply(auto)[1]
+ apply(case_tac "(bsimp (bder c x42a)) = AZERO")
apply(simp)
+
apply(simp)
+
+
+
+ apply(subgoal_tac "(\<exists>bs1 rs1. 1 < length rs1 \<and> bsimp (bder c x43) = AALTs bs1 rs1 ) \<or>
+ (\<exists>bs1 r. bsimp (bder c x43) = fuse bs1 r)")
+ prefer 2
+ apply (metis fuse_empty)
+ apply(erule disjE)
+ prefer 2
+ apply(clarify)
+ apply(simp only:)
+ apply(simp)
+ apply(simp add: fuse_append)
+ apply(subst bder_fuse)
+ apply(subst bsimp_fuse[symmetric])
+ apply(subst bder_fuse)
+ apply(subst bsimp_fuse[symmetric])
+ apply(subgoal_tac "bsimp (bder c (bsimp x43)) = bsimp (bder c x43)")
+ prefer 2
+ using less_add_Suc2 apply blast
+ apply(simp only: )
+ apply(subst bsimp_fuse[symmetric])
+ apply(simp only: )
+
+ apply(simp only: fuse.simps)
apply(simp)
+ apply(case_tac rs1)
+ apply(simp)
+ apply (me tis arexp.distinct(7) fuse.simps(1) good.simps(4) good1 good_fuse)
+ apply(simp)
+ apply(case_tac list)
+ apply(simp)
+ apply (metis arexp.distinct(7) fuse.simps(1) good.simps(5) good1 good_fuse)
+ apply(simp only: bsimp_AALTs.simps map_cons.simps)
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
+
+
+
+ apply(subst bsimp_fuse[symmetric])
+ apply(subgoal_tac "bmkeps x42 = bs")
+ prefer 2
+ apply (simp add: bmkeps_simp)
+
+
+ apply(simp)
+
+ using b3 apply force
+ using bsimp_ASEQ0 test2 apply force
+ thm good_SEQ test2
+ apply (simp add: good_SEQ test2)
+ apply (simp add: good_SEQ test2)
+ apply(case_tac "x42 = AZERO")
+ apply(simp)
+ apply(case_tac "x43 = AZERO")
+ apply(simp)
+ apply (simp add: bsimp_ASEQ0)
+ apply(case_tac "\<exists>bs. x42 = AONE bs")
+ apply(clarify)
+ apply(simp)
+ apply(subst bsimp_ASEQ1)
+ apply(simp)
+ using bsimp_ASEQ0 test2 apply force
+ apply (simp add: good_SEQ test2)
+ apply (simp add: good_SEQ test2)
+ apply (simp add: good_SEQ test2)
+ (* AALTs case *)
+ apply(simp)
+ using test2 by fastforce
-thm bsimp_AALTs.simps
-thm bsimp.simps
-thm flts.simps
-
-lemma XXX3:
- "bsimp (bders (bsimp r) s) = bsimp (bders r s)"
+lemma XXX4ab:
+ shows "good (bders_simp (bsimp r) s) \<or> bders_simp (bsimp r) s = AZERO"
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)
+ apply (simp add: good1)
+ apply(simp add: bders_simp_append)
+ apply (simp add: good1)
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
+ 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(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)
-
-
-
-
+ apply (simp add: test2)
+ apply(simp add: bders_append bders_simp_append)
+ oops
-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)
+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)
- 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(case_tac s)
+ apply(simp only: bders.simps)
+ apply(subst bders_simp.simps)
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
-
-
-
-
+
end
\ No newline at end of file