lexing: comparison thys2/SizeBound.thy

equal deleted inserted replaced

-:320f923c77b9
+:98362002c818
 | "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)"
 fun nonalt :: "arexp \<Rightarrow> bool"
 where
 "nonalt (AALTs bs2 rs) = False"
 | "nonalt r = True"
-fun good :: "arexp \<Rightarrow> bool" where
-"good AZERO = False"
-| "good (AONE cs) = True"
-| "good (ACHAR cs c) = True"
-| "good (AALTs cs []) = False"
-| "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"
 fun fuse :: "bit list \<Rightarrow> arexp \<Rightarrow> arexp" where
 "fuse bs AZERO = AZERO"
 | "fuse bs (AONE cs) = AONE (bs @ cs)"
 lemma erase_fuse:
 shows "erase (fuse bs r) = erase r"
 apply(induct r rule: erase.induct)
 apply(simp_all)
 done
-thm Posix.induct
 lemma erase_intern [simp]:
 shows "erase (intern r) = r"
 apply(induct r)
 apply(simp_all add: erase_fuse)
 "distinctBy [] f acc = []"
 | "distinctBy (x#xs) f acc =
 (if (f x) \<in> acc then distinctBy xs f acc
 else x # (distinctBy xs f ({f x} \<union> acc)))"
+lemma dB_single_step:
+shows "distinctBy (a#rs) f {} = a # distinctBy rs f {f a}"
+by simp
 fun flts :: "arexp list \<Rightarrow> arexp list"
 where
 "flts [] = []"
 | "flts (AZERO # rs) = flts rs"
 | "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"
-| "li bs [a] = fuse bs a"
-| "li bs as = AALTs bs as"
 fun bsimp_ASEQ :: "bit list \<Rightarrow> arexp \<Rightarrow> arexp \<Rightarrow> arexp"
 where
 "bsimp_ASEQ _ AZERO _ = AZERO"
 | "bsimp_ASEQ _ _ AZERO = AZERO"
 | "bsimp_ASEQ bs1 (AONE bs2) r2 = fuse (bs1 @ bs2) r2"
 fun bsimp :: "arexp \<Rightarrow> arexp"
 where
 "bsimp (ASEQ bs1 r1 r2) = bsimp_ASEQ bs1 (bsimp r1) (bsimp r2)"
-| "bsimp (AALTs bs1 rs) = bsimp_AALTs bs1 (distinctBy  (flts (map bsimp rs)) erase {} ) "
+| "bsimp (AALTs bs1 rs) = bsimp_AALTs bs1 (distinctBy (flts (map bsimp rs)) erase {}) "
 | "bsimp r = r"
 fun
 bders_simp :: "arexp \<Rightarrow> string \<Rightarrow> arexp"
 where
 "bders_simp r [] = r"
 | "bders_simp r (c # s) = bders_simp (bsimp (bder c r)) s"
 definition blexer_simp where
 "blexer_simp r s \<equiv> if bnullable (bders_simp (intern r) s) then
 decode (bmkeps (bders_simp (intern r) s)) r else None"
 export_code bders_simp in Scala module_name Example
 lemma bders_simp_append:
 shows "bders_simp r (s1 @ s2) = bders_simp (bders_simp r s1) s2"
 apply(induct s1 arbitrary: r s2)
-apply(simp)
+apply(simp_all)
-apply(simp)
+done
-done
 lemma L_bsimp_ASEQ:
 "L (SEQ (erase r1) (erase r2)) = L (erase (bsimp_ASEQ bs r1 r2))"
 apply(induct bs r1 r2 rule: bsimp_ASEQ.induct)
 apply(simp_all)
 apply(auto simp add: Sequ_def)[1]
 apply(subst L_bsimp_ASEQ[symmetric])
 apply(auto simp add: Sequ_def)[1]
 apply(subst (asm)  L_bsimp_ASEQ[symmetric])
 apply(auto simp add: Sequ_def)[1]
 apply(simp)
 apply(subst L_bsimp_AALTs[symmetric])
 defer
 apply(simp)
 apply(subst (2)L_erase_AALTs)
 apply(subst L_erase_dB)
 apply(subst L_erase_flts)
 apply(auto)
 apply (simp add: L_erase_AALTs)
 using L_erase_AALTs by blast
 lemma bsimp_ASEQ0:
 shows "bsimp_ASEQ bs r1 AZERO = AZERO"
 apply(induct r1)
 apply(auto)
 done
 lemma bsimp_ASEQ1:
 assumes "r1 \<noteq> AZERO" "r2 \<noteq> AZERO" "\<forall>bs. r1 \<noteq> AONE bs"
 shows "bsimp_ASEQ bs r1 r2 = ASEQ bs r1 r2"
 using assms
 apply(induct bs r1 r2 rule: bsimp_ASEQ.induct)
 lemma L_bders_simp:
 shows "L (erase (bders_simp r s)) = L (erase (bders r s))"
 apply(induct s arbitrary: r rule: rev_induct)
 apply(simp)
 apply(simp)
 apply(simp add: ders_append)
 apply(simp add: bders_simp_append)
 apply(simp add: L_bsimp_erase[symmetric])
 by (simp add: der_correctness)
 apply(induct rs arbitrary: rs1 bs)
 apply(simp)
 apply(simp)
 by (metis append_assoc in_set_conv_decomp r1 r2)
-lemma qq3:
-shows "bnullable (AALTs bs rs) = (\<exists>r \<in> set rs. bnullable r)"
-apply(induct rs arbitrary: bs)
-apply(simp)
-apply(simp)
-done
-fun nonnested :: "arexp \<Rightarrow> bool"
-where
-"nonnested (AALTs bs2 []) = True"
-| "nonnested (AALTs bs2 ((AALTs bs1 rs1) # rs2)) = False"
-| "nonnested (AALTs bs2 (r # rs2)) = nonnested (AALTs bs2 rs2)"
-| "nonnested r = True"
 lemma flts_append:
 shows "flts (xs1 @ xs2) = flts xs1 @ flts xs2"
 by (induct xs1  arbitrary: xs2  rule: flts.induct)(auto)
 apply(drule contextrewrites2)
 apply auto
 done
-corollary srewrites_alt1: "rs1 s\<leadsto>* rs2 \<Longrightarrow> AALTs bs rs1 \<leadsto>* AALTs bs rs2"
+corollary srewrites_alt1:
+assumes "rs1 s\<leadsto>* rs2"
+shows "AALTs bs rs1 \<leadsto>* AALTs bs rs2"
+using assms
 by (metis append.left_neutral srewrites_alt)
-lemma star_seq:  "r1 \<leadsto>* r2 \<Longrightarrow> ASEQ bs r1 r3 \<leadsto>* ASEQ bs r2 r3"
+lemma star_seq:
-apply(induct r1 r2 arbitrary: r3 rule: rrewrites.induct)
+assumes "r1 \<leadsto>* r2"
-apply(rule rs1)
+shows "ASEQ bs r1 r3 \<leadsto>* ASEQ bs r2 r3"
-apply(erule rrewrites.cases)
+using assms
-apply(simp)
+apply(induct r1 r2 arbitrary: r3 rule: rrewrites.induct)
-apply(rule r_in_rstar)
+apply(auto intro: rrewrite.intros)
-apply(rule rrewrite.intros(4))
+done
-apply simp
-apply(rule rs2)
+lemma star_seq2:
-apply(assumption)
+assumes "r3 \<leadsto>* r4"
-apply(rule rrewrite.intros(4))
+shows "ASEQ bs r1 r3 \<leadsto>* ASEQ bs r1 r4"
-by assumption
+using assms
+apply(induct r3 r4 arbitrary: r1 rule: rrewrites.induct)
-lemma star_seq2:  "r3 \<leadsto>* r4 \<Longrightarrow> ASEQ bs r1 r3 \<leadsto>* ASEQ bs r1 r4"
+apply(auto intro: rrewrite.intros)
-apply(induct r3 r4 arbitrary: r1 rule: rrewrites.induct)
+done
-apply auto
-using rrewrite.intros(5) by blast
+lemma continuous_rewrite:
+assumes "r1 \<leadsto>* AZERO"
+shows "ASEQ bs1 r1 r2 \<leadsto>* AZERO"
-lemma continuous_rewrite: "\<lbrakk>r1 \<leadsto>* AZERO\<rbrakk> \<Longrightarrow> ASEQ bs1 r1 r2 \<leadsto>* AZERO"
+using assms
 apply(induction ra\<equiv>"r1" rb\<equiv>"AZERO" arbitrary: bs1 r1 r2 rule: rrewrites.induct)
-apply (simp add: r_in_rstar rrewrite.intros(1))
+apply(auto intro: rrewrite.intros r_in_rstar star_seq)
+by (meson rrewrite.intros(1) rs2 star_seq)
-by (meson rrewrite.intros(1) rrewrites.intros(2) star_seq)
+lemma bsimp_aalts_simpcases:
-lemma bsimp_aalts_simpcases: "AONE bs \<leadsto>* (bsimp (AONE bs))"  "AZERO \<leadsto>* bsimp AZERO" "ACHAR bs c \<leadsto>* (bsimp (ACHAR bs c))"
+shows "AONE bs \<leadsto>* bsimp (AONE bs)"
-apply (simp add: rrewrites.intros(1))
+and   "AZERO \<leadsto>* bsimp AZERO"
-apply (simp add: rrewrites.intros(1))
+and   "ACHAR bs c \<leadsto>* bsimp (ACHAR bs c)"
-by (simp add: rrewrites.intros(1))
+by (simp_all)
 lemma trivialbsimpsrewrites: "\<lbrakk>\<And>x. x \<in> set rs \<Longrightarrow> x \<leadsto>* f x \<rbrakk> \<Longrightarrow> rs s\<leadsto>* (map f rs)"
 apply(induction rs)
 apply simp
 where
 fs1: "[] f\<leadsto>* []"
 |fs2: "\<lbrakk>rs f\<leadsto>* rs'\<rbrakk> \<Longrightarrow> (AZERO#rs) f\<leadsto>* rs'"
 |fs3: "\<lbrakk>rs f\<leadsto>* rs'\<rbrakk> \<Longrightarrow> ((AALTs bs rs1) # rs) f\<leadsto>* ((map (fuse bs) rs1) @ rs')"
 |fs4: "\<lbrakk>rs f\<leadsto>* rs';nonalt r; nonazero r\<rbrakk> \<Longrightarrow> (r#rs) f\<leadsto>* (r#rs')"
 lemma flts_prepend: "\<lbrakk>nonalt a; nonazero a\<rbrakk> \<Longrightarrow> flts (a#rs) = a # (flts rs)"
 by (metis append_Cons append_Nil flts_single1 flts_append)
 thm nonalt.elims
 apply blast
 using bbbbs1 apply blast
-apply(simp add: nonalt.simps)+
+apply(simp)+
 apply (meson nonazero.elims(3))
 by (meson fs4 nonalt.elims(3) nonazero.elims(3))
-lemma rrewrite0away: "AALTs bs ( AZERO # rsb) \<leadsto> AALTs bs rsb"
+lemma rrewrite0away: "AALTs bs (AZERO # rsb) \<leadsto> AALTs bs rsb"
 by (metis append_Nil rrewrite.intros(7))
 lemma frewritesaalts:"rs f\<leadsto>* rs' \<Longrightarrow> (AALTs bs (rs1@rs)) \<leadsto>* (AALTs bs (rs1@rs'))"
 apply(induct rs rs' arbitrary: bs rs1 rule:frewrites.induct)
 apply(case_tac "\<exists>bs2 rs2. a = AALTs bs2 rs2")
 apply(erule exE)+
-apply(simp add: flts.simps)
+apply(simp)
 prefer 2
 apply(subst flts_prepend)
 apply (meson nonalt.elims(3))
 lemma threelistsappend: "rsa@a#rsb = (rsa@[a])@rsb"
 apply auto
 done
-fun distinctByAcc :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b set \<Rightarrow> 'b set"
-where
-"distinctByAcc [] f acc = acc"
-| "distinctByAcc (x#xs) f acc =
-(if (f x) \<in> acc then distinctByAcc xs f acc
-else  (distinctByAcc xs f ({f x} \<union> acc)))"
-lemma dB_single_step: "distinctBy (a#rs) f {} = a # distinctBy rs f {f a}"
-apply simp
-done
 lemma somewhereInside: "r \<in> set rs \<Longrightarrow> \<exists>rs1 rs2. rs = rs1@[r]@rs2"
 using split_list by fastforce
 lemma somewhereMapInside: "f r \<in> f ` set rs \<Longrightarrow> \<exists>rs1 rs2 a. rs = rs1@[a]@rs2 \<and> f a = f r"
-lemma bsimp_rewrite: " (rrewrites r ( bsimp r))"
+lemma bsimp_rewrite:
+shows "r \<leadsto>* bsimp r"
 apply(induction r rule: bsimp.induct)
 apply simp
 apply(case_tac "bsimp r1 = AZERO")
 apply simp
 using continuous_rewrite apply blast
 lemma nomember_bnullable: "\<lbrakk> \<not> (\<exists>r0\<in>set rs1. bnullable r0); \<not> bnullable r; \<not> (\<exists>r0\<in>set rs2. bnullable r0)\<rbrakk>
 \<Longrightarrow> \<not>bnullable (AALTs bs (rs1 @ [r] @ rs2))"
-using nonbnullable_lists_concat qq3 by presburger
+using bnullable.simps(4) nonbnullable_lists_concat by presburger
 lemma bnullable_segment: " bnullable (AALTs bs (rs1@[r]@rs2)) \<Longrightarrow> bnullable (AALTs bs rs1) \<or> bnullable (AALTs bs rs2) \<or> bnullable r"
 apply(case_tac "\<exists>r0\<in>set rs1.  bnullable r0")
+using r2 apply blast
-using qq3 apply blast
 apply(case_tac "bnullable r")
 apply blast
 apply(case_tac "\<exists>r0\<in>set rs2.  bnullable r0")
 lemma third_segment_bmkeps:  "\<lbrakk>bnullable (AALTs bs (rs1@rs2@rs3)); \<not>bnullable (AALTs bs rs1); \<not>bnullable (AALTs bs rs2)\<rbrakk> \<Longrightarrow>
 bmkeps (AALTs bs (rs1@rs2@rs3) ) = bmkeps (AALTs bs rs3)"
 apply(subgoal_tac "bnullable (AALTs bs rs3)")
 apply(subgoal_tac "\<forall>r \<in> set (rs1@rs2). \<not>bnullable r")
 apply(subgoal_tac "bmkeps (AALTs bs (rs1@rs2@rs3)) = bmkeps (AALTs bs ((rs1@rs2)@rs3) )")
-apply (metis qq2 qq3)
+apply (metis bnullable.simps(4) qq2)
 apply (metis append.assoc)
 apply (metis append.assoc in_set_conv_decomp r2 third_segment_bnullable)
 using r2 apply blast
 apply (metis list.set_intros(1))
-apply (smt (verit, ccfv_threshold) append_eq_append_conv2 list.set_intros(1) qq2 qq3 rewrite_nullable rrewrite.intros(8) self_append_conv2 spillbmkepslistr)
+apply (smt (verit, ccfv_threshold) append_eq_append_conv2 list.set_intros(1) qq2 bnullable.simps(4) rewrite_nullable rrewrite.intros(8) self_append_conv2 spillbmkepslistr)
 thm qq1
 apply(subgoal_tac "bmkeps  (AALTs bs (rsa @ AALTs bs1 rs1 # rsb)) = bmkeps (AALTs bs rsb) ")
 prefer 2
 using bnullable.simps(1) apply blast
 apply (simp add: b2)
-by (smt (z3) Un_iff bnullable_correctness erase.simps(5) qq1 qq2 qq3 set_append)
+by (smt (z3) Un_iff bnullable_correctness erase.simps(5) qq1 qq2 bnullable.simps(4) set_append)
 lemma rewrites_bmkeps:
 assumes "r1 \<leadsto>* r2" "bnullable r1"
 shows "bmkeps r1 = bmkeps r2"
 using assms
 using rrewrite.intros(13) by auto
-lemma rewrites_fuse:  "r2 \<leadsto>* r2' \<Longrightarrow>  (fuse bs1 r2) \<leadsto>*  (fuse bs1 r2')"
+lemma rewrites_fuse:
-apply(induction r2 r2' arbitrary: bs1 rule: rrewrites.induct)
+assumes "r2 \<leadsto>* r2'"
-apply simp
+shows "fuse bs1 r2 \<leadsto>* fuse bs1 r2'"
-by (meson real_trans rewrite_fuse)
+using assms
+apply(induction r2 r2' arbitrary: bs1 rule: rrewrites.induct)
-lemma  bder_fuse_list: " map (bder c \<circ> fuse bs1) rs1 = map (fuse bs1 \<circ> bder c) rs1"
+apply(auto intro: rewrite_fuse real_trans)
-apply(induction rs1)
+done
-apply simp
-by (simp add: bder_fuse)
+lemma  bder_fuse_list:
+shows "map (bder c \<circ> fuse bs1) rs1 = map (fuse bs1 \<circ> bder c) rs1"
+apply(induction rs1)
+apply(simp_all add: bder_fuse)
+done
 lemma rewrite_der_altmiddle: "bder c (AALTs bs (rsa @ AALTs bs1 rs1 # rsb)) \<leadsto>* bder c (AALTs bs (rsa @ map (fuse bs1) rs1 @ rsb))"
 apply simp
 apply(simp add: bder_fuse_list)

changeset 374	98362002c818
parent 373	320f923c77b9
child 375	f83271c585d2