--- a/thys/BitCoded2.thy Mon Sep 09 09:37:33 2019 +0100
+++ b/thys/BitCoded2.thy Thu Sep 12 18:06:01 2019 +0100
@@ -3503,166 +3503,6 @@
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 [simp]:
- shows "size (fuse bs r) = size r"
- by (induct r) (auto)
-
-fun AALTs_subs where
- "AALTs_subs (AZERO) = {}"
-| "AALTs_subs (AONE bs) = {AONE bs}"
-| "AALTs_subs (ACHAR bs c) = {ACHAR bs c}"
-| "AALTs_subs (ASEQ bs r1 r2) = {ASEQ bs r1 r2}"
-| "AALTs_subs (ASTAR bs r) = {ASTAR bs r}"
-| "AALTs_subs (AALTs bs []) = {}"
-| "AALTs_subs (AALTs bs (r#rs)) = AALTs_subs (fuse bs r) \<union> AALTs_subs (AALTs bs rs)"
-
-lemma nonalt_10:
- assumes "nonalt r" "r \<noteq> AZERO"
- shows "r \<in> AALTs_subs r"
- using assms
- apply(induct r)
- apply(auto)
- done
-
-lemma flt_fuse:
- shows "flts (map (fuse bs) rs) = map (fuse bs) (flts rs)"
- apply(induct rs arbitrary: bs rule: flts.induct)
- apply(auto)
- by (simp add: fuse_append)
-
-lemma AALTs_subs_fuse:
- shows "AALTs_subs (fuse bs r) = (fuse bs) ` (AALTs_subs r)"
- apply(induct r arbitrary: bs rule: AALTs_subs.induct)
- apply(auto)
- apply (simp add: fuse_append)
- apply blast
- by (simp add: fuse_append)
-
-lemma AALTs_subs_fuse2:
- shows "AALTs_subs (AALTs bs rs) = AALTs_subs (AALTs [] (map (fuse bs) rs))"
- apply(induct rs arbitrary: bs)
- apply(auto)
- apply (auto simp add: fuse_empty)
- done
-
-lemma fuse_map:
- shows "map (fuse (bs1 @ bs2)) rs = map (fuse bs1) (map (fuse bs2) rs)"
- apply(induct rs)
- apply(auto)
- using fuse_append by blast
-
-
-
-lemma contains59_2:
- assumes "AALTs bs rs >> bs2"
- shows "\<exists>r\<in>AALTs_subs (AALTs bs rs). r >> bs2"
- using assms
- apply(induct rs arbitrary: bs bs2 taking: "\<lambda>rs. sum_list (map asize rs)" rule: measure_induct)
- apply(case_tac x)
- apply(auto)
- using contains59 apply force
- apply(erule contains.cases)
- apply(auto)
- apply(case_tac "r = AZERO")
- apply(simp)
- apply (metis bsimp_AALTs.simps(1) contains61 empty_iff empty_set)
- apply(case_tac "nonalt r")
- apply (metis UnCI bsimp_AALTs.simps(1) contains0 contains61 empty_iff empty_set nn11a nonalt_10)
- apply(subgoal_tac "\<exists>bsX rsX. r = AALTs bsX rsX")
- prefer 2
- using bbbbs1 apply blast
- apply(auto)
- apply (metis UnCI contains0 fuse.simps(4) less_add_Suc1)
- apply(drule_tac x="rs" in spec)
- apply(drule mp)
- apply(simp add: asize0)
- apply(drule_tac x="bsa" in spec)
- apply(drule_tac x="bsa @ bs1" in spec)
- apply(auto)
- done
-
-lemma TEMPLATE_contains61a:
- assumes "\<exists>r \<in> set rs. (fuse bs r) >> bs2"
- shows "bsimp_AALTs bs rs >> bs2"
- using assms
- apply(induct rs arbitrary: bs2 bs)
- apply(auto)
- apply (metis bsimp_AALTs.elims contains60 list.distinct(1) list.inject list.set_intros(1))
- by (metis append_Cons append_Nil contains50 f_cont2)
-
-
-
-
-lemma H1:
- assumes "r >> bs2" "r \<in> AALTs_subs a"
- shows "a >> bs2"
- using assms
- apply(induct a arbitrary: r bs2 rule: AALTs_subs.induct)
- apply(auto)
- apply (simp add: contains60)
- by (simp add: contains59 contains60)
-
-lemma H3:
- assumes "a >> bs"
- shows "\<exists>r \<in> AALTs_subs a. r >> bs"
- using assms
- apply(induct a bs)
- apply(auto intro: contains.intros)
- using contains.intros(4) contains59_2 by fastforce
-
-lemma H4:
- shows "AALTs_subs (AALTs bs rs1) \<subseteq> AALTs_subs (AALTs bs (rs1 @ rs2))"
- apply(induct rs1)
- apply(auto)
- done
-
-lemma H5:
- shows "AALTs_subs (AALTs bs rs2) \<subseteq> AALTs_subs (AALTs bs (rs1 @ rs2))"
- apply(induct rs1)
- apply(auto)
- done
-
-lemma H7:
- shows "AALTs_subs (AALTs bs (rs1 @ rs2)) = AALTs_subs (AALTs bs rs1) \<union> AALTs_subs (AALTs bs rs2)"
- apply(induct rs1)
- apply(auto)
- done
-
-lemma H6:
- shows "AALTs_subs (AALTs bs (flts rs)) = AALTs_subs (AALTs bs rs)"
- apply(induct rs arbitrary: bs rule: flts.induct)
- apply(auto)
- apply (metis AALTs_subs_fuse2 H7 Un_iff fuse_map)
- apply (metis AALTs_subs_fuse2 H7 UnCI fuse_map)
- by (simp add: H7)
-
-
-lemma H2:
- assumes "r >> bs2" "r \<in> AALTs_subs (AALTs bs rs)"
- shows "r \<in> AALTs_subs (AALTs bs (flts rs))"
- using assms
- apply(induct rs arbitrary: r bs bs2 rule: flts.induct)
- apply(auto)
- apply (metis AALTs_subs_fuse2 H4 fuse_map in_mono)
- using H7 by blast
-
-lemma H00:
- shows " (\<Union> (AALTs_subs ` (set (map (bder c o fuse bs) rs)))) \<subseteq> ((bder c) ` (AALTs_subs (AALTs bs rs)))"
- apply(induct rs arbitrary: bs c)
- apply(auto simp add: image_def)
-
-
-
-lemma contains61a_2:
- assumes "\<exists>r\<in>AALTs_subs (AALTs bs rs). r >> bs2"
- shows "bsimp_AALTs bs rs >> bs2"
- using assms
- apply(induct rs arbitrary: bs2 bs)
- apply(auto)
- apply (simp add: H1 TEMPLATE_contains61a)
- by (metis append_Cons append_Nil contains50 f_cont2)
lemma in2:
@@ -3670,11 +3510,8 @@
"AALTs bsX rsX = bsimp r" and
"XX \<in> set rsX" "nonnested (bsimp r)"
shows "bder c (fuse bsX XX) >> bs2"
- using assms
- apply(induct r arbitrary: c bs2 bsX rsX XX)
- apply(auto)
- prefer 2
- oops
+
+ sorry
lemma
@@ -3750,22 +3587,6 @@
apply(erule contains.cases)
apply(auto)
(* ALT case *)
- apply(drule contains59_2)
- apply(auto)
- apply(subst bder_bsimp_AALTs)
- thm contains61a_2 contains61a
- apply(rule contains61a_2)
- apply(case_tac x2a)
- apply(simp)
- apply(simp)
- apply(auto)
-
-
-
-(* HERE HERE *)
-
-(* old *)
-(*
apply(drule contains59)
apply(auto)
apply(subst bder_bsimp_AALTs)
@@ -3801,21 +3622,7 @@
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)
-*)
-
+ by (metis contains0 contains49 f_cont1 in2 list.exhaust list.set_intros(1))
lemma CONTAINS1:
assumes "a >> bs"