--- a/ChengsongTanPhdThesis/Chapters/Finite.tex Tue Jun 28 21:07:42 2022 +0100
+++ b/ChengsongTanPhdThesis/Chapters/Finite.tex Wed Jun 29 12:38:05 2022 +0100
@@ -852,13 +852,49 @@
The reason why we take the trouble of defining
two separate list rewriting definitions $\frewrite$ and $\grewrite$
is that sometimes $\grewrites$ is slightly too powerful
-that it renders certain equivalence to break after derivative:
-
-$\rsimp{(\rsimpalts \; (\map \; (\_ \backslash x) \; (\rdistinct{(\rflts \; (\map \; (\rsimp{} \; \circ \; (\lambda r. \rderssimp{r}{xs}))))}{\varnothing})))} \neq
- \rsimp{(\rsimpalts \; (\rdistinct{(\map \; (\_ \backslash x) \; (\rflts \; (\map \; (\rsimp{} \; \circ \; (\lambda r. \rderssimp{r}{xs})))) ) }{\varnothing})} $
+for proving equivalence.
+For example, when proving the closed-form for the alternative regular expression,
+one of the rewriting steps would be:
+\begin{lemma}
+ $\sum (\rDistinct \; (\map \; (\_ \backslash x) \; (\rflts \; rs)) \; \varnothing) \sequal
+ \sum (\rDistinct \; (\rflts \; (\map \; (\_ \backslash x) \; rs)) \; \varnothing)
+ $
+\end{lemma}
+\noindent
+Proving this is by first showing
+\begin{lemma}
+ $\map \; (\_ \backslash x) \; (\rflts \; rs) \frewrites
+\rflts \; (\map \; (\_ \backslash x) \; rs)$
+\end{lemma}
+\noindent
+and then using lemma
+\begin{lemma}\label{frewritesSimpeq}
+ If $rs_1 \frewrites rs_2 $, then $\sum (\rDistinct \; rs_1 \; \varnothing) \sequal
+ \sum (\rDistinct \; rs_2 \; {})$.
+\end{lemma}
+. But this trick will not work for $\grewrites$:
+\begin{center}
+$\map \; (\_ \backslash x) \; (\rDistinct \; rs \; rset) \grewrites \rDistinct \; (\map \;
+(\_ \backslash x) \; rs) \; (\map \; (\_ \backslash x) \; rset)$
+\end{center}
+\noindent
+does \emph{not} hold.
+
+%this is for closed form for alts section, talk about that later------------------------------
+\begin{comment}
+\begin{center}
+$\rsimp{(\rsimpalts \; (\map \; (\_ \backslash x) \; (\rdistinct{(\rflts \; (\map \; (\rsimp{} \; \circ \; (\lambda r. \rderssimp{r}{xs}))))}{\varnothing})))} =
+\rsimp{(\rsimpalts \; (\rdistinct{(\map \; (\_ \backslash x) \; (\rflts \; (\map \; (\rsimp{} \; \circ \; (\lambda r. \rderssimp{r}{xs})))) ) }{\varnothing}))} $
+\end{center}
+
+\noindent
+This is not possible to prove
+
+\end{comment}
+%this is for closed form for alts section, talk about that later------------------------------
And we define an "grewrite" relation that works on lists:
\begin{center}
\begin{tabular}{lcl}
@@ -1321,14 +1357,10 @@
There are a few key steps, one of these steps is
-\[
-rsimp (rsimp\_ALTs (map (rder x) (rdistinct (rflts (map (rsimp \circ (\lambda r. rders\_simp r xs)) rs)) {})))
-= rsimp (rsimp\_ALTs (rdistinct (map (rder x) (rflts (map (rsimp \circ (\lambda r. rders\_simp r xs)) rs))) {}))
-\]
+
One might want to prove this by something a simple statement like:
-$map (rder x) (rdistinct rs rset) = rdistinct (map (rder x) rs) (rder x) ` rset)$.
For this to hold we want the $\textit{distinct}$ function to pick up
the elements before and after derivatives correctly:
--- a/ChengsongTanPhdThesis/Chapters/Introduction.tex Tue Jun 28 21:07:42 2022 +0100
+++ b/ChengsongTanPhdThesis/Chapters/Introduction.tex Wed Jun 29 12:38:05 2022 +0100
@@ -31,6 +31,7 @@
\newcommand{\ONE}{\mbox{\bf 1}}
\newcommand{\AALTS}[2]{\oplus {\scriptstyle #1}\, #2}
\newcommand{\rdistinct}[2]{\textit{rdistinct} \;\; #1 \;\; #2}
+\def\rDistinct{\textit{rdistinct}}
\newcommand\hflat[1]{\llparenthesis #1 \rrparenthesis_*}
\newcommand\hflataux[1]{\llparenthesis #1 \rrparenthesis_*'}
\newcommand\createdByStar[1]{\textit{createdByStar}(#1)}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/thys3/BasicIdentities.thy Wed Jun 29 12:38:05 2022 +0100
@@ -0,0 +1,630 @@
+theory BasicIdentities
+ imports "RfltsRdistinctProps"
+begin
+
+
+
+lemma rder_rsimp_ALTs_commute:
+ shows " (rder x (rsimp_ALTs rs)) = rsimp_ALTs (map (rder x) rs)"
+ apply(induct rs)
+ apply simp
+ apply(case_tac rs)
+ apply simp
+ apply auto
+ done
+
+
+
+lemma rsimp_aalts_smaller:
+ shows "rsize (rsimp_ALTs rs) \<le> rsize (RALTS rs)"
+ apply(induct rs)
+ apply simp
+ apply simp
+ apply(case_tac "rs = []")
+ apply simp
+ apply(subgoal_tac "\<exists>rsp ap. rs = ap # rsp")
+ apply(erule exE)+
+ apply simp
+ apply simp
+ by(meson neq_Nil_conv)
+
+
+
+
+
+lemma rSEQ_mono:
+ shows "rsize (rsimp_SEQ r1 r2) \<le>rsize (RSEQ r1 r2)"
+ apply auto
+ apply(induct r1)
+ apply auto
+ 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 r2)
+ apply simp_all
+ done
+
+lemma ralts_cap_mono:
+ shows "rsize (RALTS rs) \<le> Suc (rsizes rs)"
+ by simp
+
+
+
+
+lemma rflts_mono:
+ shows "rsizes (rflts rs) \<le> rsizes rs"
+ apply(induct rs)
+ apply simp
+ apply(case_tac "a = RZERO")
+ apply simp
+ apply(case_tac "\<exists>rs1. a = RALTS rs1")
+ apply(erule exE)
+ apply simp
+ apply(subgoal_tac "rflts (a # rs) = a # (rflts rs)")
+ prefer 2
+
+ using rflts_def_idiot apply blast
+ apply simp
+ done
+
+lemma rdistinct_smaller:
+ shows "rsizes (rdistinct rs ss) \<le> rsizes rs"
+ apply (induct rs arbitrary: ss)
+ apply simp
+ by (simp add: trans_le_add2)
+
+
+lemma rsimp_alts_mono :
+ shows "\<And>x. (\<And>xa. xa \<in> set x \<Longrightarrow> rsize (rsimp xa) \<le> rsize xa) \<Longrightarrow>
+ rsize (rsimp_ALTs (rdistinct (rflts (map rsimp x)) {})) \<le> Suc (rsizes x)"
+ apply(subgoal_tac "rsize (rsimp_ALTs (rdistinct (rflts (map rsimp x)) {} ))
+ \<le> rsize (RALTS (rdistinct (rflts (map rsimp x)) {} ))")
+ prefer 2
+ using rsimp_aalts_smaller apply auto[1]
+ apply(subgoal_tac "rsize (RALTS (rdistinct (rflts (map rsimp x)) {})) \<le>Suc (rsizes (rdistinct (rflts (map rsimp x)) {}))")
+ prefer 2
+ using ralts_cap_mono apply blast
+ apply(subgoal_tac "rsizes (rdistinct (rflts (map rsimp x)) {}) \<le> rsizes (rflts (map rsimp x))")
+ prefer 2
+ using rdistinct_smaller apply presburger
+ apply(subgoal_tac "rsizes (rflts (map rsimp x)) \<le> rsizes (map rsimp x)")
+ prefer 2
+ using rflts_mono apply blast
+ apply(subgoal_tac "rsizes (map rsimp x) \<le> rsizes x")
+ prefer 2
+
+ apply (simp add: sum_list_mono)
+ by linarith
+
+
+
+
+
+lemma rsimp_mono:
+ shows "rsize (rsimp r) \<le> rsize r"
+ apply(induct r)
+ apply simp_all
+ apply(subgoal_tac "rsize (rsimp_SEQ (rsimp r1) (rsimp r2)) \<le> rsize (RSEQ (rsimp r1) (rsimp r2))")
+ apply force
+ using rSEQ_mono
+ apply presburger
+ using rsimp_alts_mono by auto
+
+lemma idiot:
+ shows "rsimp_SEQ RONE r = r"
+ apply(case_tac r)
+ apply simp_all
+ done
+
+
+
+
+
+lemma idiot2:
+ shows " \<lbrakk>r1 \<noteq> RZERO; r1 \<noteq> RONE;r2 \<noteq> RZERO\<rbrakk>
+ \<Longrightarrow> rsimp_SEQ r1 r2 = RSEQ r1 r2"
+ apply(case_tac r1)
+ 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 r2)
+ apply simp_all
+ done
+
+lemma rders__onechar:
+ shows " (rders_simp r [c]) = (rsimp (rders r [c]))"
+ by simp
+
+lemma rders_append:
+ "rders c (s1 @ s2) = rders (rders c s1) s2"
+ apply(induct s1 arbitrary: c s2)
+ apply(simp_all)
+ done
+
+lemma rders_simp_append:
+ "rders_simp c (s1 @ s2) = rders_simp (rders_simp c s1) s2"
+ apply(induct s1 arbitrary: c s2)
+ apply(simp_all)
+ done
+
+
+lemma rders_simp_one_char:
+ shows "rders_simp r [c] = rsimp (rder c r)"
+ apply auto
+ done
+
+
+
+
+
+lemma k0a:
+ shows "rflts [RALTS rs] = rs"
+ apply(simp)
+ done
+
+lemma bbbbs:
+ assumes "good r" "r = RALTS rs"
+ shows "rsimp_ALTs (rflts [r]) = RALTS rs"
+ using assms
+ by (metis good.simps(4) good.simps(5) k0a rsimp_ALTs.elims)
+
+lemma bbbbs1:
+ shows "nonalt r \<or> (\<exists> rs. r = RALTS rs)"
+ by (meson nonalt.elims(3))
+
+
+
+lemma good0:
+ assumes "rs \<noteq> Nil" "\<forall>r \<in> set rs. nonalt r" "distinct rs"
+ shows "good (rsimp_ALTs rs) \<longleftrightarrow> (\<forall>r \<in> set rs. good r)"
+ using assms
+ apply(induct rs rule: rsimp_ALTs.induct)
+ apply(auto)
+ done
+
+lemma flts1:
+ assumes "good r"
+ shows "rflts [r] \<noteq> []"
+ using assms
+ apply(induct r)
+ apply(simp_all)
+ using good.simps(4) by blast
+
+lemma flts2:
+ assumes "good r"
+ shows "\<forall>r' \<in> set (rflts [r]). good r' \<and> nonalt r'"
+ using assms
+ apply(induct r)
+ apply(simp)
+ apply(simp)
+ apply(simp)
+ prefer 2
+ apply(simp)
+ apply(auto)[1]
+
+ apply (metis flts1 good.simps(5) good.simps(6) k0a neq_Nil_conv)
+ apply (metis flts1 good.simps(5) good.simps(6) k0a neq_Nil_conv)
+ apply fastforce
+ apply(simp)
+ done
+
+
+
+lemma flts3:
+ assumes "\<forall>r \<in> set rs. good r \<or> r = RZERO"
+ shows "\<forall>r \<in> set (rflts rs). good r"
+ using assms
+ apply(induct rs rule: rflts.induct)
+ apply(simp_all)
+ by (metis UnE flts2 k0a)
+
+
+lemma k0:
+ shows "rflts (r # rs1) = rflts [r] @ rflts rs1"
+ apply(induct r arbitrary: rs1)
+ apply(auto)
+ done
+
+
+lemma good_SEQ:
+ assumes "r1 \<noteq> RZERO" "r2 \<noteq> RZERO" " r1 \<noteq> RONE"
+ shows "good (RSEQ 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 rsize0:
+ shows "0 < rsize r"
+ apply(induct r)
+ apply(auto)
+ done
+
+
+
+
+
+
+
+
+
+
+
+lemma nn1qq:
+ assumes "nonnested (RALTS rs)"
+ shows "\<nexists> rs1. RALTS rs1 \<in> set rs"
+ using assms
+ apply(induct rs rule: rflts.induct)
+ apply(auto)
+ done
+
+
+
+lemma n0:
+ shows "nonnested (RALTS rs) \<longleftrightarrow> (\<forall>r \<in> set rs. nonalt r)"
+ apply(induct rs )
+ apply(auto)
+ apply (metis list.set_intros(1) nn1qq nonalt.elims(3))
+ apply (metis nonalt.elims(2) nonnested.simps(3) nonnested.simps(4) nonnested.simps(5) nonnested.simps(6) nonnested.simps(7))
+ using bbbbs1 apply fastforce
+ by (metis bbbbs1 list.set_intros(2) nn1qq)
+
+
+
+
+lemma nn1c:
+ assumes "\<forall>r \<in> set rs. nonnested r"
+ shows "\<forall>r \<in> set (rflts rs). nonalt r"
+ using assms
+ apply(induct rs rule: rflts.induct)
+ apply(auto)
+ using n0 by blast
+
+lemma nn1bb:
+ assumes "\<forall>r \<in> set rs. nonalt r"
+ shows "nonnested (rsimp_ALTs rs)"
+ using assms
+ apply(induct rs rule: rsimp_ALTs.induct)
+ apply(auto)
+ using nonalt.simps(1) nonnested.elims(3) apply blast
+ using n0 by auto
+
+lemma bsimp_ASEQ0:
+ shows "rsimp_SEQ r1 RZERO = RZERO"
+ apply(induct r1)
+ apply(auto)
+ done
+
+lemma nn1b:
+ shows "nonnested (rsimp r)"
+ apply(induct r)
+ apply(simp_all)
+ apply(case_tac "rsimp r1 = RZERO")
+ apply(simp)
+ apply(case_tac "rsimp r2 = RZERO")
+ apply(simp)
+ apply(subst bsimp_ASEQ0)
+ apply(simp)
+ apply(case_tac "\<exists>bs. rsimp r1 = RONE")
+ apply(auto)[1]
+ using idiot apply fastforce
+ using idiot2 nonnested.simps(11) apply presburger
+ by (metis (mono_tags, lifting) Diff_empty image_iff list.set_map nn1bb nn1c rdistinct_set_equality1)
+
+lemma nonalt_flts_rd:
+ shows "\<lbrakk>xa \<in> set (rdistinct (rflts (map rsimp rs)) {})\<rbrakk>
+ \<Longrightarrow> nonalt xa"
+ by (metis Diff_empty ex_map_conv nn1b nn1c rdistinct_set_equality1)
+
+
+
+
+lemma bsimp_ASEQ2:
+ shows "rsimp_SEQ RONE r2 = r2"
+ apply(induct r2)
+ apply(auto)
+ done
+
+lemma elem_smaller_than_set:
+ shows "xa \<in> set list \<Longrightarrow> rsize xa < Suc (rsizes list)"
+ apply(induct list)
+ apply simp
+ by (metis image_eqI le_imp_less_Suc list.set_map member_le_sum_list)
+
+lemma rsimp_list_mono:
+ shows "rsizes (map rsimp rs) \<le> rsizes rs"
+ apply(induct rs)
+ apply simp+
+ by (simp add: add_mono_thms_linordered_semiring(1) rsimp_mono)
+
+
+(*says anything coming out of simp+flts+db will be good*)
+lemma good2_obv_simplified:
+ shows " \<lbrakk>\<forall>y. rsize y < Suc (rsizes rs) \<longrightarrow> good (rsimp y) \<or> rsimp y = RZERO;
+ xa \<in> set (rdistinct (rflts (map rsimp rs)) {})\<rbrakk> \<Longrightarrow> good xa"
+ apply(subgoal_tac " \<forall>xa' \<in> set (map rsimp rs). good xa' \<or> xa' = RZERO")
+ prefer 2
+ apply (simp add: elem_smaller_than_set)
+ by (metis Diff_empty flts3 rdistinct_set_equality1)
+
+
+
+
+lemma good1:
+ shows "good (rsimp a) \<or> rsimp a = RZERO"
+ apply(induct a taking: rsize rule: measure_induct)
+ apply(case_tac x)
+ apply(simp)
+ apply(simp)
+ apply(simp)
+ prefer 3
+ apply(simp)
+ prefer 2
+ apply(simp only:)
+ apply simp
+ apply (smt (verit, ccfv_threshold) add_mono_thms_linordered_semiring(1) elem_smaller_than_set good0 good2_obv_simplified le_eq_less_or_eq nonalt_flts_rd order_less_trans plus_1_eq_Suc rdistinct_does_the_job rdistinct_smaller rflts_mono rsimp_ALTs.simps(1) rsimp_list_mono)
+ apply simp
+ apply(subgoal_tac "good (rsimp x41) \<or> rsimp x41 = RZERO")
+ apply(subgoal_tac "good (rsimp x42) \<or> rsimp x42 = RZERO")
+ apply(case_tac "rsimp x41 = RZERO")
+ apply simp
+ apply(case_tac "rsimp x42 = RZERO")
+ apply simp
+ using bsimp_ASEQ0 apply blast
+ apply(subgoal_tac "good (rsimp x41)")
+ apply(subgoal_tac "good (rsimp x42)")
+ apply simp
+ apply (metis bsimp_ASEQ2 good_SEQ idiot2)
+ apply blast
+ apply fastforce
+ using less_add_Suc2 apply blast
+ using less_iff_Suc_add by blast
+
+lemma RL_rnullable:
+ shows "rnullable r = ([] \<in> RL r)"
+ apply(induct r)
+ apply(auto simp add: Sequ_def)
+ done
+
+lemma RL_rder:
+ shows "RL (rder c r) = Der c (RL r)"
+ apply(induct r)
+ apply(auto simp add: Sequ_def Der_def)
+ apply (metis append_Cons)
+ using RL_rnullable apply blast
+ apply (metis append_eq_Cons_conv)
+ apply (metis append_Cons)
+ apply (metis RL_rnullable append_eq_Cons_conv)
+ apply (metis Star.step append_Cons)
+ using Star_decomp by auto
+
+
+
+
+lemma RL_rsimp_RSEQ:
+ shows "RL (rsimp_SEQ r1 r2) = (RL r1 ;; RL r2)"
+ apply(induct r1 r2 rule: rsimp_SEQ.induct)
+ apply(simp_all)
+ done
+
+
+
+lemma RL_rsimp_RALTS:
+ shows "RL (rsimp_ALTs rs) = (\<Union> (set (map RL rs)))"
+ apply(induct rs rule: rsimp_ALTs.induct)
+ apply(simp_all)
+ done
+
+lemma RL_rsimp_rdistinct:
+ shows "(\<Union> (set (map RL (rdistinct rs {})))) = (\<Union> (set (map RL rs)))"
+ apply(auto)
+ apply (metis Diff_iff rdistinct_set_equality1)
+ by (metis Diff_empty rdistinct_set_equality1)
+
+lemma RL_rsimp_rflts:
+ shows "(\<Union> (set (map RL (rflts rs)))) = (\<Union> (set (map RL rs)))"
+ apply(induct rs rule: rflts.induct)
+ apply(simp_all)
+ done
+
+lemma RL_rsimp:
+ shows "RL r = RL (rsimp r)"
+ apply(induct r rule: rsimp.induct)
+ apply(auto simp add: Sequ_def RL_rsimp_RSEQ)
+ using RL_rsimp_RALTS RL_rsimp_rdistinct RL_rsimp_rflts apply auto[1]
+ by (smt (verit, del_insts) RL_rsimp_RALTS RL_rsimp_rdistinct RL_rsimp_rflts UN_E image_iff list.set_map)
+
+
+
+lemma der_simp_nullability:
+ shows "rnullable r = rnullable (rsimp r)"
+ using RL_rnullable RL_rsimp by auto
+
+
+lemma qqq1:
+ shows "RZERO \<notin> set (rflts (map rsimp rs))"
+ by (metis ex_map_conv flts3 good.simps(1) good1)
+
+
+
+
+
+lemma flts_single1:
+ assumes "nonalt r" "nonazero r"
+ shows "rflts [r] = [r]"
+ using assms
+ apply(induct r)
+ apply(auto)
+ done
+
+lemma nonalt0_flts_keeps:
+ shows "(a \<noteq> RZERO) \<and> (\<forall>rs. a \<noteq> RALTS rs) \<Longrightarrow> rflts (a # xs) = a # rflts xs"
+ apply(case_tac a)
+ apply simp+
+ done
+
+
+lemma nonalt0_fltseq:
+ shows "\<forall>r \<in> set rs. r \<noteq> RZERO \<and> nonalt r \<Longrightarrow> rflts rs = rs"
+ apply(induct rs)
+ apply simp
+ apply(case_tac "a = RZERO")
+ apply fastforce
+ apply(case_tac "\<exists>rs1. a = RALTS rs1")
+ apply(erule exE)
+ apply simp+
+ using nonalt0_flts_keeps by presburger
+
+
+
+
+lemma goodalts_nonalt:
+ shows "good (RALTS rs) \<Longrightarrow> rflts rs = rs"
+ apply(induct x == "RALTS rs" arbitrary: rs rule: good.induct)
+ apply simp
+
+ using good.simps(5) apply blast
+ apply simp
+ apply(case_tac "r1 = RZERO")
+ using good.simps(1) apply force
+ apply(case_tac "r2 = RZERO")
+ using good.simps(1) apply force
+ apply(subgoal_tac "rflts (r1 # r2 # rs) = r1 # r2 # rflts rs")
+ prefer 2
+ apply (metis nonalt.simps(1) rflts_def_idiot)
+ apply(subgoal_tac "\<forall>r \<in> set rs. r \<noteq> RZERO \<and> nonalt r")
+ apply(subgoal_tac "rflts rs = rs")
+ apply presburger
+ using nonalt0_fltseq apply presburger
+ using good.simps(1) by blast
+
+
+
+
+
+lemma test:
+ assumes "good r"
+ shows "rsimp r = r"
+
+ using assms
+ apply(induct rule: good.induct)
+ apply simp
+ apply simp
+ apply simp
+ apply simp
+ apply simp
+ apply(subgoal_tac "distinct (r1 # r2 # rs)")
+ prefer 2
+ using good.simps(6) apply blast
+ apply(subgoal_tac "rflts (r1 # r2 # rs ) = r1 # r2 # rs")
+ prefer 2
+ using goodalts_nonalt apply blast
+
+ apply(subgoal_tac "r1 \<noteq> r2")
+ prefer 2
+ apply (meson distinct_length_2_or_more)
+ apply(subgoal_tac "r1 \<notin> set rs")
+ apply(subgoal_tac "r2 \<notin> set rs")
+ apply(subgoal_tac "\<forall>r \<in> set rs. rsimp r = r")
+ apply(subgoal_tac "map rsimp rs = rs")
+ apply simp
+ apply(subgoal_tac "\<forall>r \<in> {r1, r2}. r \<notin> set rs")
+ apply (metis distinct_not_exist rdistinct_on_distinct)
+
+ apply blast
+ apply (meson map_idI)
+ apply (metis good.simps(6) insert_iff list.simps(15))
+
+ apply (meson distinct.simps(2))
+ apply (simp add: distinct_length_2_or_more)
+ apply simp+
+ done
+
+
+
+lemma rsimp_idem:
+ shows "rsimp (rsimp r) = rsimp r"
+ using test good1
+ by force
+
+corollary rsimp_inner_idem4:
+ shows "rsimp r = RALTS rs \<Longrightarrow> rflts rs = rs"
+ by (metis good1 goodalts_nonalt rrexp.simps(12))
+
+
+corollary head_one_more_simp:
+ shows "map rsimp (r # rs) = map rsimp (( rsimp r) # rs)"
+ by (simp add: rsimp_idem)
+
+
+
+
+lemma basic_regex_property1:
+ shows "rnullable r \<Longrightarrow> rsimp r \<noteq> RZERO"
+ apply(induct r rule: rsimp.induct)
+ apply(auto)
+ apply (metis idiot idiot2 rrexp.distinct(5))
+ by (metis der_simp_nullability rnullable.simps(1) rnullable.simps(4) rsimp.simps(2))
+
+
+
+lemma no_alt_short_list_after_simp:
+ shows "RALTS rs = rsimp r \<Longrightarrow> rsimp_ALTs rs = RALTS rs"
+ by (metis bbbbs good1 k0a rrexp.simps(12))
+
+
+lemma no_further_dB_after_simp:
+ shows "RALTS rs = rsimp r \<Longrightarrow> rdistinct rs {} = rs"
+ apply(subgoal_tac "good (RALTS rs)")
+ apply(subgoal_tac "distinct rs")
+ using rdistinct_on_distinct apply blast
+ apply (metis distinct.simps(1) distinct.simps(2) empty_iff good.simps(6) list.exhaust set_empty2)
+ using good1 by fastforce
+
+
+lemma idem_after_simp1:
+ shows "rsimp_ALTs (rdistinct (rflts [rsimp aa]) {}) = rsimp aa"
+ apply(case_tac "rsimp aa")
+ apply simp+
+ apply (metis no_alt_short_list_after_simp no_further_dB_after_simp)
+ by simp
+
+
+
+
+
+(*equalities with rsimp *)
+lemma identity_wwo0:
+ shows "rsimp (rsimp_ALTs (RZERO # rs)) = rsimp (rsimp_ALTs rs)"
+ by (metis idem_after_simp1 list.exhaust list.simps(8) list.simps(9) rflts.simps(2) rsimp.simps(2) rsimp.simps(3) rsimp_ALTs.simps(1) rsimp_ALTs.simps(2) rsimp_ALTs.simps(3))
+
+
+
+
+
+
+
+(*some basic facts about rsimp*)
+
+unused_thms
+
+
+end
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/thys3/Blexer.thy Wed Jun 29 12:38:05 2022 +0100
@@ -0,0 +1,454 @@
+
+theory Blexer
+ imports "Lexer" "PDerivs"
+begin
+
+section \<open>Bit-Encodings\<close>
+
+datatype bit = Z | S
+
+fun code :: "val \<Rightarrow> bit list"
+where
+ "code Void = []"
+| "code (Char c) = []"
+| "code (Left v) = Z # (code v)"
+| "code (Right v) = S # (code v)"
+| "code (Seq v1 v2) = (code v1) @ (code v2)"
+| "code (Stars []) = [S]"
+| "code (Stars (v # vs)) = (Z # code v) @ code (Stars vs)"
+
+
+fun
+ Stars_add :: "val \<Rightarrow> val \<Rightarrow> val"
+where
+ "Stars_add v (Stars vs) = Stars (v # vs)"
+
+function
+ decode' :: "bit list \<Rightarrow> rexp \<Rightarrow> (val * bit list)"
+where
+ "decode' bs ZERO = (undefined, bs)"
+| "decode' bs ONE = (Void, bs)"
+| "decode' bs (CH d) = (Char d, bs)"
+| "decode' [] (ALT r1 r2) = (Void, [])"
+| "decode' (Z # bs) (ALT r1 r2) = (let (v, bs') = decode' bs r1 in (Left v, bs'))"
+| "decode' (S # bs) (ALT r1 r2) = (let (v, bs') = decode' bs r2 in (Right v, bs'))"
+| "decode' bs (SEQ r1 r2) = (let (v1, bs') = decode' bs r1 in
+ let (v2, bs'') = decode' bs' r2 in (Seq v1 v2, bs''))"
+| "decode' [] (STAR r) = (Void, [])"
+| "decode' (S # bs) (STAR r) = (Stars [], bs)"
+| "decode' (Z # bs) (STAR r) = (let (v, bs') = decode' bs r in
+ let (vs, bs'') = decode' bs' (STAR r)
+ in (Stars_add v vs, bs''))"
+by pat_completeness auto
+
+lemma decode'_smaller:
+ assumes "decode'_dom (bs, r)"
+ shows "length (snd (decode' bs r)) \<le> length bs"
+using assms
+apply(induct bs r)
+apply(auto simp add: decode'.psimps split: prod.split)
+using dual_order.trans apply blast
+by (meson dual_order.trans le_SucI)
+
+termination "decode'"
+apply(relation "inv_image (measure(%cs. size cs) <*lex*> measure(%s. size s)) (%(ds,r). (r,ds))")
+apply(auto dest!: decode'_smaller)
+by (metis less_Suc_eq_le snd_conv)
+
+definition
+ decode :: "bit list \<Rightarrow> rexp \<Rightarrow> val option"
+where
+ "decode ds r \<equiv> (let (v, ds') = decode' ds r
+ in (if ds' = [] then Some v else None))"
+
+lemma decode'_code_Stars:
+ assumes "\<forall>v\<in>set vs. \<Turnstile> v : r \<and> (\<forall>x. decode' (code v @ x) r = (v, x)) \<and> flat v \<noteq> []"
+ shows "decode' (code (Stars vs) @ ds) (STAR r) = (Stars vs, ds)"
+ using assms
+ apply(induct vs)
+ apply(auto)
+ done
+
+lemma decode'_code:
+ assumes "\<Turnstile> v : r"
+ shows "decode' ((code v) @ ds) r = (v, ds)"
+using assms
+ apply(induct v r arbitrary: ds)
+ apply(auto)
+ using decode'_code_Stars by blast
+
+lemma decode_code:
+ assumes "\<Turnstile> v : r"
+ shows "decode (code v) r = Some v"
+ using assms unfolding decode_def
+ by (smt append_Nil2 decode'_code old.prod.case)
+
+
+section {* Annotated Regular Expressions *}
+
+datatype arexp =
+ AZERO
+| AONE "bit list"
+| ACHAR "bit list" char
+| ASEQ "bit list" arexp arexp
+| AALTs "bit list" "arexp list"
+| ASTAR "bit list" arexp
+
+abbreviation
+ "AALT bs r1 r2 \<equiv> AALTs bs [r1, r2]"
+
+fun asize :: "arexp \<Rightarrow> nat" where
+ "asize AZERO = 1"
+| "asize (AONE cs) = 1"
+| "asize (ACHAR cs c) = 1"
+| "asize (AALTs cs rs) = Suc (sum_list (map asize rs))"
+| "asize (ASEQ cs r1 r2) = Suc (asize r1 + asize r2)"
+| "asize (ASTAR cs r) = Suc (asize r)"
+
+fun
+ erase :: "arexp \<Rightarrow> rexp"
+where
+ "erase AZERO = ZERO"
+| "erase (AONE _) = ONE"
+| "erase (ACHAR _ c) = CH c"
+| "erase (AALTs _ []) = ZERO"
+| "erase (AALTs _ [r]) = (erase r)"
+| "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 fuse :: "bit list \<Rightarrow> arexp \<Rightarrow> arexp" where
+ "fuse bs AZERO = AZERO"
+| "fuse bs (AONE cs) = AONE (bs @ cs)"
+| "fuse bs (ACHAR cs c) = ACHAR (bs @ cs) c"
+| "fuse bs (AALTs cs rs) = AALTs (bs @ cs) rs"
+| "fuse bs (ASEQ cs r1 r2) = ASEQ (bs @ cs) r1 r2"
+| "fuse bs (ASTAR cs r) = ASTAR (bs @ cs) r"
+
+lemma fuse_append:
+ shows "fuse (bs1 @ bs2) r = fuse bs1 (fuse bs2 r)"
+ apply(induct r)
+ apply(auto)
+ done
+
+
+fun intern :: "rexp \<Rightarrow> arexp" where
+ "intern ZERO = AZERO"
+| "intern ONE = AONE []"
+| "intern (CH c) = ACHAR [] c"
+| "intern (ALT r1 r2) = AALT [] (fuse [Z] (intern r1))
+ (fuse [S] (intern r2))"
+| "intern (SEQ r1 r2) = ASEQ [] (intern r1) (intern r2)"
+| "intern (STAR r) = ASTAR [] (intern r)"
+
+
+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"
+| "retrieve (ASTAR bs r) (Stars []) = bs @ [S]"
+| "retrieve (ASTAR bs r) (Stars (v#vs)) =
+ bs @ [Z] @ retrieve r v @ retrieve (ASTAR [] r) (Stars vs)"
+
+
+
+fun
+ bnullable :: "arexp \<Rightarrow> bool"
+where
+ "bnullable (AZERO) = False"
+| "bnullable (AONE bs) = True"
+| "bnullable (ACHAR bs c) = False"
+| "bnullable (AALTs bs rs) = (\<exists>r \<in> set rs. bnullable r)"
+| "bnullable (ASEQ bs r1 r2) = (bnullable r1 \<and> bnullable r2)"
+| "bnullable (ASTAR bs r) = True"
+
+abbreviation
+ bnullables :: "arexp list \<Rightarrow> bool"
+where
+ "bnullables rs \<equiv> (\<exists>r \<in> set rs. bnullable r)"
+
+fun
+ bmkeps :: "arexp \<Rightarrow> bit list" and
+ bmkepss :: "arexp list \<Rightarrow> bit list"
+where
+ "bmkeps(AONE bs) = bs"
+| "bmkeps(ASEQ bs r1 r2) = bs @ (bmkeps r1) @ (bmkeps r2)"
+| "bmkeps(AALTs bs rs) = bs @ (bmkepss rs)"
+| "bmkeps(ASTAR bs r) = bs @ [S]"
+| "bmkepss (r # rs) = (if bnullable(r) then (bmkeps r) else (bmkepss rs))"
+
+lemma bmkepss1:
+ assumes "\<not> bnullables rs1"
+ shows "bmkepss (rs1 @ rs2) = bmkepss rs2"
+ using assms
+ by (induct rs1) (auto)
+
+lemma bmkepss2:
+ assumes "bnullables rs1"
+ shows "bmkepss (rs1 @ rs2) = bmkepss rs1"
+ using assms
+ by (induct rs1) (auto)
+
+
+fun
+ bder :: "char \<Rightarrow> arexp \<Rightarrow> arexp"
+where
+ "bder c (AZERO) = AZERO"
+| "bder c (AONE bs) = AZERO"
+| "bder c (ACHAR bs d) = (if c = d then AONE bs else AZERO)"
+| "bder c (AALTs bs rs) = AALTs bs (map (bder c) rs)"
+| "bder c (ASEQ bs r1 r2) =
+ (if bnullable r1
+ then AALT bs (ASEQ [] (bder c r1) r2) (fuse (bmkeps r1) (bder c r2))
+ else ASEQ bs (bder c r1) r2)"
+| "bder c (ASTAR bs r) = ASEQ (bs @ [Z]) (bder c r) (ASTAR [] r)"
+
+
+fun
+ bders :: "arexp \<Rightarrow> string \<Rightarrow> arexp"
+where
+ "bders r [] = r"
+| "bders r (c#s) = bders (bder c r) s"
+
+lemma bders_append:
+ "bders c (s1 @ s2) = bders (bders c s1) s2"
+ apply(induct s1 arbitrary: c s2)
+ apply(simp_all)
+ done
+
+lemma bnullable_correctness:
+ shows "nullable (erase r) = bnullable r"
+ apply(induct r rule: erase.induct)
+ apply(simp_all)
+ done
+
+lemma erase_fuse:
+ shows "erase (fuse bs r) = erase r"
+ apply(induct r rule: erase.induct)
+ apply(simp_all)
+ done
+
+lemma erase_intern [simp]:
+ shows "erase (intern r) = r"
+ apply(induct r)
+ apply(simp_all add: erase_fuse)
+ done
+
+lemma erase_bder [simp]:
+ shows "erase (bder a r) = der a (erase r)"
+ apply(induct r rule: erase.induct)
+ apply(simp_all add: erase_fuse bnullable_correctness)
+ done
+
+lemma erase_bders [simp]:
+ shows "erase (bders r s) = ders s (erase r)"
+ apply(induct s arbitrary: r )
+ apply(simp_all)
+ done
+
+lemma bnullable_fuse:
+ shows "bnullable (fuse bs r) = bnullable r"
+ apply(induct r arbitrary: bs)
+ apply(auto)
+ done
+
+lemma retrieve_encode_STARS:
+ assumes "\<forall>v\<in>set vs. \<Turnstile> v : r \<and> code v = retrieve (intern r) v"
+ shows "code (Stars vs) = retrieve (ASTAR [] (intern r)) (Stars vs)"
+ using assms
+ apply(induct vs)
+ apply(simp_all)
+ done
+
+lemma retrieve_fuse2:
+ assumes "\<Turnstile> v : (erase r)"
+ shows "retrieve (fuse bs r) v = bs @ retrieve r v"
+ using assms
+ apply(induct r arbitrary: v bs)
+ apply(auto elim: Prf_elims)[4]
+ apply(case_tac x2a)
+ apply(simp)
+ using Prf_elims(1) apply blast
+ apply(case_tac x2a)
+ apply(simp)
+ apply(simp)
+ apply(case_tac list)
+ apply(simp)
+ apply(simp)
+ apply (smt (verit, best) Prf_elims(3) append_assoc retrieve.simps(4) retrieve.simps(5))
+ apply(simp)
+ using retrieve_encode_STARS
+ apply(auto elim!: Prf_elims)[1]
+ apply(case_tac vs)
+ apply(simp)
+ apply(simp)
+ done
+
+lemma retrieve_fuse:
+ assumes "\<Turnstile> v : r"
+ shows "retrieve (fuse bs (intern r)) v = bs @ retrieve (intern r) v"
+ using assms
+ by (simp_all add: retrieve_fuse2)
+
+
+lemma retrieve_code:
+ assumes "\<Turnstile> v : r"
+ shows "code v = retrieve (intern r) v"
+ using assms
+ apply(induct v r )
+ apply(simp_all add: retrieve_fuse retrieve_encode_STARS)
+ done
+
+
+lemma retrieve_AALTs_bnullable1:
+ assumes "bnullable r"
+ shows "retrieve (AALTs bs (r # rs)) (mkeps (erase (AALTs bs (r # rs))))
+ = bs @ retrieve r (mkeps (erase r))"
+ using assms
+ apply(case_tac rs)
+ apply(auto simp add: bnullable_correctness)
+ done
+
+lemma retrieve_AALTs_bnullable2:
+ assumes "\<not>bnullable r" "bnullables rs"
+ shows "retrieve (AALTs bs (r # rs)) (mkeps (erase (AALTs bs (r # rs))))
+ = retrieve (AALTs bs rs) (mkeps (erase (AALTs bs rs)))"
+ using assms
+ apply(induct rs arbitrary: r bs)
+ apply(auto)
+ using bnullable_correctness apply blast
+ apply(case_tac rs)
+ apply(auto)
+ using bnullable_correctness apply blast
+ apply(case_tac rs)
+ apply(auto)
+ done
+
+lemma bmkeps_retrieve_AALTs:
+ assumes "\<forall>r \<in> set rs. bnullable r \<longrightarrow> bmkeps r = retrieve r (mkeps (erase r))"
+ "bnullables rs"
+ shows "bs @ bmkepss rs = retrieve (AALTs bs rs) (mkeps (erase (AALTs bs rs)))"
+ using assms
+ apply(induct rs arbitrary: bs)
+ apply(auto)
+ using retrieve_AALTs_bnullable1 apply presburger
+ apply (metis retrieve_AALTs_bnullable2)
+ apply (simp add: retrieve_AALTs_bnullable1)
+ by (metis retrieve_AALTs_bnullable2)
+
+
+lemma bmkeps_retrieve:
+ assumes "bnullable r"
+ shows "bmkeps r = retrieve r (mkeps (erase r))"
+ using assms
+ apply(induct r)
+ apply(auto)
+ using bmkeps_retrieve_AALTs by auto
+
+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 rule: erase.induct)
+ using Prf_elims(1) apply auto[1]
+ using Prf_elims(1) apply auto[1]
+ apply(auto)[1]
+ apply (metis Prf_elims(4) injval.simps(1) retrieve.simps(1) retrieve.simps(2))
+ using Prf_elims(1) apply blast
+ (* AALTs case *)
+ 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)
+ using Prf_elims(3) apply fastforce
+ (* ASEQ case *)
+ apply(simp)
+ apply(case_tac "nullable (erase r1)")
+ apply(simp)
+ apply(erule Prf_elims)
+ using Prf_elims(2) bnullable_correctness apply force
+ apply (simp add: bmkeps_retrieve bnullable_correctness retrieve_fuse2)
+ apply (simp add: bmkeps_retrieve bnullable_correctness retrieve_fuse2)
+ using Prf_elims(2) apply force
+ (* ASTAR case *)
+ apply(rename_tac bs r v)
+ apply(simp)
+ apply(erule Prf_elims)
+ apply(clarify)
+ apply(erule Prf_elims)
+ apply(clarify)
+ by (simp add: retrieve_fuse2)
+
+
+lemma MAIN_decode:
+ assumes "\<Turnstile> v : ders s r"
+ shows "Some (flex r id s v) = decode (retrieve (bders (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 (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 (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 (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)
+ 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 blexer where
+ "blexer r s \<equiv> if bnullable (bders (intern r) s) then
+ decode (bmkeps (bders (intern r) s)) r else None"
+
+lemma blexer_correctness:
+ shows "blexer r s = lexer r s"
+proof -
+ { define bds where "bds \<equiv> bders (intern r) s"
+ define ds where "ds \<equiv> ders s r"
+ assume asm: "nullable ds"
+ have era: "erase bds = ds"
+ unfolding ds_def bds_def by simp
+ have mke: "\<Turnstile> mkeps ds : ds"
+ using asm by (simp add: mkeps_nullable)
+ have "decode (bmkeps bds) r = decode (retrieve bds (mkeps ds)) r"
+ using bmkeps_retrieve
+ using asm era
+ using bnullable_correctness by force
+ also have "... = Some (flex r id s (mkeps ds))"
+ using mke by (simp_all add: MAIN_decode ds_def bds_def)
+ finally have "decode (bmkeps bds) r = Some (flex r id s (mkeps ds))"
+ unfolding bds_def ds_def .
+ }
+ then show "blexer r s = lexer r s"
+ unfolding blexer_def lexer_flex
+ by (auto simp add: bnullable_correctness[symmetric])
+qed
+
+
+unused_thms
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/thys3/ClosedFormsBounds.thy Wed Jun 29 12:38:05 2022 +0100
@@ -0,0 +1,448 @@
+
+theory ClosedFormsBounds
+ imports "GeneralRegexBound" "ClosedForms"
+begin
+lemma alts_ders_lambda_shape_ders:
+ shows "\<forall>r \<in> set (map (\<lambda>r. rders_simp r ( s)) rs ). \<exists>r1 \<in> set rs. r = rders_simp r1 s"
+ by (simp add: image_iff)
+
+lemma rlist_bound:
+ assumes "\<forall>r \<in> set rs. rsize r \<le> N"
+ shows "rsizes rs \<le> N * (length rs)"
+ using assms
+ apply(induct rs)
+ apply simp
+ by simp
+
+lemma alts_closed_form_bounded:
+ assumes "\<forall>r \<in> set rs. \<forall>s. rsize (rders_simp r s) \<le> N"
+ shows "rsize (rders_simp (RALTS rs) s) \<le> max (Suc (N * (length rs))) (rsize (RALTS rs))"
+proof (cases s)
+ case Nil
+ then show "rsize (rders_simp (RALTS rs) s) \<le> max (Suc (N * length rs)) (rsize (RALTS rs))"
+ by simp
+next
+ case (Cons a s)
+
+ from assms have "\<forall>r \<in> set (map (\<lambda>r. rders_simp r (a # s)) rs ). rsize r \<le> N"
+ by (metis alts_ders_lambda_shape_ders)
+ then have a: "rsizes (map (\<lambda>r. rders_simp r (a # s)) rs ) \<le> N * (length rs)"
+ by (metis length_map rlist_bound)
+
+ have "rsize (rders_simp (RALTS rs) (a # s))
+ = rsize (rsimp (RALTS (map (\<lambda>r. rders_simp r (a # s)) rs)))"
+ by (metis alts_closed_form_variant list.distinct(1))
+ also have "... \<le> rsize (RALTS (map (\<lambda>r. rders_simp r (a # s)) rs))"
+ using rsimp_mono by blast
+ also have "... = Suc (rsizes (map (\<lambda>r. rders_simp r (a # s)) rs))"
+ by simp
+ also have "... \<le> Suc (N * (length rs))"
+ using a by blast
+ finally have "rsize (rders_simp (RALTS rs) (a # s)) \<le> max (Suc (N * length rs)) (rsize (RALTS rs))"
+ by auto
+ then show ?thesis using local.Cons by simp
+qed
+
+lemma alts_simp_ineq_unfold:
+ shows "rsize (rsimp (RALTS rs)) \<le> Suc (rsizes (rdistinct (rflts (map rsimp rs)) {}))"
+ using rsimp_aalts_smaller by auto
+
+
+lemma rdistinct_mono_list:
+ shows "rsizes (rdistinct (x5 @ rs) rset) \<le> rsizes x5 + rsizes (rdistinct rs ((set x5 ) \<union> rset))"
+ apply(induct x5 arbitrary: rs rset)
+ apply simp
+ apply(case_tac "a \<in> rset")
+ apply simp
+ apply (simp add: add.assoc insert_absorb trans_le_add2)
+ apply simp
+ by (metis Un_insert_right)
+
+
+lemma flts_size_reduction_alts:
+ assumes a: "\<And>noalts_set alts_set corr_set.
+ (\<forall>r\<in>noalts_set. \<forall>xs. r \<noteq> RALTS xs) \<and>
+ (\<forall>a\<in>alts_set. \<exists>xs. a = RALTS xs \<and> set xs \<subseteq> corr_set) \<Longrightarrow>
+ Suc (rsizes (rdistinct (rflts rs) (noalts_set \<union> corr_set)))
+ \<le> Suc (rsizes (rdistinct rs (insert RZERO (noalts_set \<union> alts_set))))"
+ and b: "\<forall>r\<in>noalts_set. \<forall>xs. r \<noteq> RALTS xs"
+ and c: "\<forall>a\<in>alts_set. \<exists>xs. a = RALTS xs \<and> set xs \<subseteq> corr_set"
+ and d: "a = RALTS x5"
+ shows "rsizes (rdistinct (rflts (a # rs)) (noalts_set \<union> corr_set))
+ \<le> rsizes (rdistinct (a # rs) (insert RZERO (noalts_set \<union> alts_set)))"
+
+ apply(case_tac "a \<in> alts_set")
+ using a b c d
+ apply simp
+ apply(subgoal_tac "set x5 \<subseteq> corr_set")
+ apply(subst rdistinct_concat)
+ apply auto[1]
+ apply presburger
+ apply fastforce
+ using a b c d
+ apply (subgoal_tac "a \<notin> noalts_set")
+ prefer 2
+ apply blast
+ apply simp
+ apply(subgoal_tac "rsizes (rdistinct (x5 @ rflts rs) (noalts_set \<union> corr_set))
+ \<le> rsizes x5 + rsizes (rdistinct (rflts rs) ((set x5) \<union> (noalts_set \<union> corr_set)))")
+ prefer 2
+ using rdistinct_mono_list apply presburger
+ apply(subgoal_tac "insert (RALTS x5) (noalts_set \<union> alts_set) = noalts_set \<union> (insert (RALTS x5) alts_set)")
+ apply(simp only:)
+ apply(subgoal_tac "rsizes x5 + rsizes (rdistinct (rflts rs) (noalts_set \<union> (corr_set \<union> (set x5)))) \<le>
+ rsizes x5 + rsizes (rdistinct rs (insert RZERO (noalts_set \<union> insert (RALTS x5) alts_set)))")
+
+ apply (simp add: Un_left_commute inf_sup_aci(5))
+ apply(subgoal_tac "rsizes (rdistinct (rflts rs) (noalts_set \<union> (corr_set \<union> set x5))) \<le>
+ rsizes (rdistinct rs (insert RZERO (noalts_set \<union> insert (RALTS x5) alts_set)))")
+ apply linarith
+ apply(subgoal_tac "\<forall>r \<in> insert (RALTS x5) alts_set. \<exists>xs1.( r = RALTS xs1 \<and> set xs1 \<subseteq> corr_set \<union> set x5)")
+ apply presburger
+ apply (meson insert_iff sup.cobounded2 sup.coboundedI1)
+ by blast
+
+
+lemma flts_vs_nflts1:
+ assumes "\<forall>r \<in> noalts_set. \<forall>xs. r \<noteq> RALTS xs"
+ and "\<forall>a \<in> alts_set. (\<exists>xs. a = RALTS xs \<and> set xs \<subseteq> corr_set)"
+ shows "rsizes (rdistinct (rflts rs) (noalts_set \<union> corr_set))
+ \<le> rsizes (rdistinct rs (insert RZERO (noalts_set \<union> alts_set)))"
+ using assms
+ apply(induct rs arbitrary: noalts_set alts_set corr_set)
+ apply simp
+ apply(case_tac a)
+ apply(case_tac "RZERO \<in> noalts_set")
+ apply simp
+ apply(subgoal_tac "RZERO \<notin> alts_set")
+ apply simp
+ apply fastforce
+ apply(case_tac "RONE \<in> noalts_set")
+ apply simp
+ apply(subgoal_tac "RONE \<notin> alts_set")
+ prefer 2
+ apply fastforce
+ apply(case_tac "RONE \<in> corr_set")
+ apply(subgoal_tac "rflts (a # rs) = RONE # rflts rs")
+ apply(simp only:)
+ apply(subgoal_tac "rdistinct (RONE # rflts rs) (noalts_set \<union> corr_set) =
+ rdistinct (rflts rs) (noalts_set \<union> corr_set)")
+ apply(simp only:)
+ apply(subgoal_tac "rdistinct (RONE # rs) (insert RZERO (noalts_set \<union> alts_set)) =
+ RONE # (rdistinct rs (insert RONE (insert RZERO (noalts_set \<union> alts_set)))) ")
+ apply(simp only:)
+ apply(subgoal_tac "rdistinct (rflts rs) (noalts_set \<union> corr_set) =
+ rdistinct (rflts rs) (insert RONE (noalts_set \<union> corr_set))")
+ apply (simp only:)
+ apply(subgoal_tac "insert RONE (noalts_set \<union> corr_set) = (insert RONE noalts_set) \<union> corr_set")
+ apply(simp only:)
+ apply(subgoal_tac "insert RONE (insert RZERO (noalts_set \<union> alts_set)) =
+ insert RZERO ((insert RONE noalts_set) \<union> alts_set)")
+ apply(simp only:)
+ apply(subgoal_tac "rsizes (rdistinct rs (insert RZERO (insert RONE noalts_set \<union> alts_set)))
+ \<le> rsizes (RONE # rdistinct rs (insert RZERO (insert RONE noalts_set \<union> alts_set)))")
+ apply (smt (verit, best) dual_order.trans insert_iff rrexp.distinct(15))
+ apply (metis (no_types, opaque_lifting) le_add_same_cancel2 list.simps(9) sum_list.Cons zero_le)
+ apply fastforce
+ apply fastforce
+ apply (metis Un_iff insert_absorb)
+ apply (metis UnE insertE insert_is_Un rdistinct.simps(2) rrexp.distinct(1))
+ apply (meson UnCI rdistinct.simps(2))
+ using rflts.simps(4) apply presburger
+ apply simp
+ apply(subgoal_tac "insert RONE (noalts_set \<union> corr_set) = (insert RONE noalts_set) \<union> corr_set")
+ apply(simp only:)
+ apply (metis Un_insert_left insertE rrexp.distinct(15))
+ apply fastforce
+ apply(case_tac "a \<in> noalts_set")
+ apply simp
+ apply(subgoal_tac "a \<notin> alts_set")
+ prefer 2
+ apply blast
+ apply(case_tac "a \<in> corr_set")
+ apply(subgoal_tac "noalts_set \<union> corr_set = insert a ( noalts_set \<union> corr_set)")
+ prefer 2
+ apply fastforce
+ apply(simp only:)
+ apply(subgoal_tac "rsizes (rdistinct (a # rs) (insert RZERO ((insert a noalts_set) \<union> alts_set))) \<le>
+ rsizes (rdistinct (a # rs) (insert RZERO (noalts_set \<union> alts_set)))")
+
+ apply(subgoal_tac "rsizes (rdistinct (rflts (a # rs)) ((insert a noalts_set) \<union> corr_set)) \<le>
+ rsizes (rdistinct (a # rs) (insert RZERO ((insert a noalts_set) \<union> alts_set)))")
+ apply fastforce
+ apply simp
+ apply(subgoal_tac "(insert a (noalts_set \<union> alts_set)) = (insert a noalts_set) \<union> alts_set")
+ apply(simp only:)
+ apply(subgoal_tac "noalts_set \<union> corr_set = (insert a noalts_set) \<union> corr_set")
+ apply(simp only:)
+ apply (metis insertE rrexp.distinct(21))
+ apply blast
+
+ apply fastforce
+ apply force
+ apply simp
+ apply (metis Un_insert_left insert_iff rrexp.distinct(21))
+ apply(case_tac "a \<in> noalts_set")
+ apply simp
+ apply(subgoal_tac "a \<notin> alts_set")
+ prefer 2
+ apply blast
+ apply(case_tac "a \<in> corr_set")
+ apply(subgoal_tac "noalts_set \<union> corr_set = insert a ( noalts_set \<union> corr_set)")
+ prefer 2
+ apply fastforce
+ apply(simp only:)
+ apply(subgoal_tac "rsizes (rdistinct (a # rs) (insert RZERO ((insert a noalts_set) \<union> alts_set))) \<le>
+ rsizes (rdistinct (a # rs) (insert RZERO (noalts_set \<union> alts_set)))")
+
+ apply(subgoal_tac "rsizes (rdistinct (rflts (a # rs)) ((insert a noalts_set) \<union> corr_set)) \<le>
+ rsizes (rdistinct (a # rs) (insert RZERO ((insert a noalts_set) \<union> alts_set)))")
+ apply fastforce
+ apply simp
+ apply(subgoal_tac "(insert a (noalts_set \<union> alts_set)) = (insert a noalts_set) \<union> alts_set")
+ apply(simp only:)
+ apply(subgoal_tac "noalts_set \<union> corr_set = (insert a noalts_set) \<union> corr_set")
+ apply(simp only:)
+
+
+ apply (metis insertE rrexp.distinct(25))
+ apply blast
+ apply fastforce
+ apply force
+ apply simp
+
+ apply (metis Un_insert_left insertE rrexp.distinct(25))
+
+ using Suc_le_mono flts_size_reduction_alts apply presburger
+ apply(case_tac "a \<in> noalts_set")
+ apply simp
+ apply(subgoal_tac "a \<notin> alts_set")
+ prefer 2
+ apply blast
+ apply(case_tac "a \<in> corr_set")
+ apply(subgoal_tac "noalts_set \<union> corr_set = insert a ( noalts_set \<union> corr_set)")
+ prefer 2
+ apply fastforce
+ apply(simp only:)
+ apply(subgoal_tac "rsizes (rdistinct (a # rs) (insert RZERO ((insert a noalts_set) \<union> alts_set))) \<le>
+ rsizes (rdistinct (a # rs) (insert RZERO (noalts_set \<union> alts_set)))")
+
+ apply(subgoal_tac "rsizes (rdistinct (rflts (a # rs)) ((insert a noalts_set) \<union> corr_set)) \<le>
+ rsizes (rdistinct (a # rs) (insert RZERO ((insert a noalts_set) \<union> alts_set)))")
+ apply fastforce
+ apply simp
+ apply(subgoal_tac "(insert a (noalts_set \<union> alts_set)) = (insert a noalts_set) \<union> alts_set")
+ apply(simp only:)
+ apply(subgoal_tac "noalts_set \<union> corr_set = (insert a noalts_set) \<union> corr_set")
+ apply(simp only:)
+ apply (metis insertE rrexp.distinct(29))
+
+ apply blast
+
+ apply fastforce
+ apply force
+ apply simp
+ apply (metis Un_insert_left insert_iff rrexp.distinct(29))
+ done
+
+
+lemma flts_vs_nflts:
+ assumes "\<forall>r \<in> noalts_set. \<forall>xs. r \<noteq> RALTS xs"
+ and "\<forall>a \<in> alts_set. (\<exists>xs. a = RALTS xs \<and> set xs \<subseteq> corr_set)"
+ shows "rsizes (rdistinct (rflts rs) (noalts_set \<union> corr_set))
+ \<le> rsizes (rdistinct rs (insert RZERO (noalts_set \<union> alts_set)))"
+ by (simp add: assms flts_vs_nflts1)
+
+lemma distinct_simp_ineq_general:
+ assumes "rsimp ` no_simp = has_simp" "finite no_simp"
+ shows "rsizes (rdistinct (map rsimp rs) has_simp) \<le> rsizes (rdistinct rs no_simp)"
+ using assms
+ apply(induct rs no_simp arbitrary: has_simp rule: rdistinct.induct)
+ apply simp
+ apply(auto)
+ using add_le_mono rsimp_mono by presburger
+
+lemma larger_acc_smaller_distinct_res0:
+ assumes "ss \<subseteq> SS"
+ shows "rsizes (rdistinct rs SS) \<le> rsizes (rdistinct rs ss)"
+ using assms
+ apply(induct rs arbitrary: ss SS)
+ apply simp
+ by (metis distinct_early_app1 rdistinct_smaller)
+
+lemma without_flts_ineq:
+ shows "rsizes (rdistinct (rflts rs) {}) \<le> rsizes (rdistinct rs {})"
+proof -
+ have "rsizes (rdistinct (rflts rs) {}) \<le> rsizes (rdistinct rs (insert RZERO {}))"
+ by (metis empty_iff flts_vs_nflts sup_bot_left)
+ also have "... \<le> rsizes (rdistinct rs {})"
+ by (simp add: larger_acc_smaller_distinct_res0)
+ finally show ?thesis
+ by blast
+qed
+
+
+lemma distinct_simp_ineq:
+ shows "rsizes (rdistinct (map rsimp rs) {}) \<le> rsizes (rdistinct rs {})"
+ using distinct_simp_ineq_general by blast
+
+
+lemma alts_simp_control:
+ shows "rsize (rsimp (RALTS rs)) \<le> Suc (rsizes (rdistinct rs {}))"
+proof -
+ have "rsize (rsimp (RALTS rs)) \<le> Suc (rsizes (rdistinct (rflts (map rsimp rs)) {}))"
+ using alts_simp_ineq_unfold by auto
+ moreover have "\<dots> \<le> Suc (rsizes (rdistinct (map rsimp rs) {}))"
+ using without_flts_ineq by blast
+ ultimately show "rsize (rsimp (RALTS rs)) \<le> Suc (rsizes (rdistinct rs {}))"
+ by (meson Suc_le_mono distinct_simp_ineq le_trans)
+qed
+
+
+lemma larger_acc_smaller_distinct_res:
+ shows "rsizes (rdistinct rs (insert a ss)) \<le> rsizes (rdistinct rs ss)"
+ by (simp add: larger_acc_smaller_distinct_res0 subset_insertI)
+
+lemma triangle_inequality_distinct:
+ shows "rsizes (rdistinct (a # rs) ss) \<le> rsize a + rsizes (rdistinct rs ss)"
+ apply(case_tac "a \<in> ss")
+ apply simp
+ by (simp add: larger_acc_smaller_distinct_res)
+
+
+lemma distinct_list_size_len_bounded:
+ assumes "\<forall>r \<in> set rs. rsize r \<le> N" "length rs \<le> lrs"
+ shows "rsizes rs \<le> lrs * N "
+ using assms
+ by (metis rlist_bound dual_order.trans mult.commute mult_le_mono1)
+
+
+
+lemma rdistinct_same_set:
+ shows "r \<in> set rs \<longleftrightarrow> r \<in> set (rdistinct rs {})"
+ apply(induct rs)
+ apply simp
+ by (metis rdistinct_set_equality)
+
+(* distinct_list_rexp_up_to_certain_size_bouded_by_set_enumerating_up_to_that_size *)
+lemma distinct_list_rexp_upto:
+ assumes "\<forall>r\<in> set rs. (rsize r) \<le> N"
+ shows "rsizes (rdistinct rs {}) \<le> (card (sizeNregex N)) * N"
+
+ apply(subgoal_tac "distinct (rdistinct rs {})")
+ prefer 2
+ using rdistinct_does_the_job apply blast
+ apply(subgoal_tac "length (rdistinct rs {}) \<le> card (sizeNregex N)")
+ apply(rule distinct_list_size_len_bounded)
+ using assms
+ apply (meson rdistinct_same_set)
+ apply blast
+ apply(subgoal_tac "\<forall>r \<in> set (rdistinct rs {}). rsize r \<le> N")
+ prefer 2
+ using assms
+ apply (meson rdistinct_same_set)
+ apply(subgoal_tac "length (rdistinct rs {}) = card (set (rdistinct rs {}))")
+ prefer 2
+ apply (simp add: distinct_card)
+ apply(simp)
+ by (metis card_mono finite_size_n mem_Collect_eq sizeNregex_def subsetI)
+
+
+lemma star_control_bounded:
+ assumes "\<forall>s. rsize (rders_simp r s) \<le> N"
+ shows "rsizes (rdistinct (map (\<lambda>s1. RSEQ (rders_simp r s1) (RSTAR r)) (star_updates s r [[c]])) {})
+ \<le> (card (sizeNregex (Suc (N + rsize (RSTAR r))))) * (Suc (N + rsize (RSTAR r)))"
+ by (smt (verit) add_Suc_shift add_mono_thms_linordered_semiring(3) assms distinct_list_rexp_upto image_iff list.set_map plus_nat.simps(2) rsize.simps(5))
+
+
+lemma star_closed_form_bounded:
+ assumes "\<forall>s. rsize (rders_simp r s) \<le> N"
+ shows "rsize (rders_simp (RSTAR r) s) \<le>
+ max ((Suc (card (sizeNregex (Suc (N + rsize (RSTAR r))))) * (Suc (N + rsize (RSTAR r))))) (rsize (RSTAR r))"
+proof(cases s)
+ case Nil
+ then show "rsize (rders_simp (RSTAR r) s)
+ \<le> max (Suc (card (sizeNregex (Suc (N + rsize (RSTAR r))))) * Suc (N + rsize (RSTAR r))) (rsize (RSTAR r))"
+ by simp
+next
+ case (Cons a list)
+ then have "rsize (rders_simp (RSTAR r) s) =
+ rsize (rsimp (RALTS ((map (\<lambda>s1. RSEQ (rders_simp r s1) (RSTAR r)) (star_updates list r [[a]])))))"
+ using star_closed_form by fastforce
+ also have "... \<le> Suc (rsizes (rdistinct (map (\<lambda>s1. RSEQ (rders_simp r s1) (RSTAR r)) (star_updates list r [[a]])) {}))"
+ using alts_simp_control by blast
+ also have "... \<le> Suc (card (sizeNregex (Suc (N + rsize (RSTAR r))))) * (Suc (N + rsize (RSTAR r)))"
+ using star_control_bounded[OF assms] by (metis add_mono le_add1 mult_Suc plus_1_eq_Suc)
+ also have "... \<le> max (Suc (card (sizeNregex (Suc (N + rsize (RSTAR r))))) * Suc (N + rsize (RSTAR r))) (rsize (RSTAR r))"
+ by simp
+ finally show ?thesis by simp
+qed
+
+
+lemma seq_estimate_bounded:
+ assumes "\<forall>s. rsize (rders_simp r1 s) \<le> N1"
+ and "\<forall>s. rsize (rders_simp r2 s) \<le> N2"
+ shows
+ "rsizes (rdistinct (RSEQ (rders_simp r1 s) r2 # map (rders_simp r2) (vsuf s r1)) {})
+ \<le> (Suc (N1 + (rsize r2)) + (N2 * card (sizeNregex N2)))"
+proof -
+ have a: "rsizes (rdistinct (map (rders_simp r2) (vsuf s r1)) {}) \<le> N2 * card (sizeNregex N2)"
+ by (metis assms(2) distinct_list_rexp_upto ex_map_conv mult.commute)
+
+ have "rsizes (rdistinct (RSEQ (rders_simp r1 s) r2 # map (rders_simp r2) (vsuf s r1)) {}) \<le>
+ rsize (RSEQ (rders_simp r1 s) r2) + rsizes (rdistinct (map (rders_simp r2) (vsuf s r1)) {})"
+ using triangle_inequality_distinct by blast
+ also have "... \<le> rsize (RSEQ (rders_simp r1 s) r2) + N2 * card (sizeNregex N2)"
+ by (simp add: a)
+ also have "... \<le> Suc (N1 + (rsize r2) + N2 * card (sizeNregex N2))"
+ by (simp add: assms(1))
+ finally show ?thesis
+ by force
+qed
+
+
+lemma seq_closed_form_bounded2:
+ assumes "\<forall>s. rsize (rders_simp r1 s) \<le> N1"
+ and "\<forall>s. rsize (rders_simp r2 s) \<le> N2"
+shows "rsize (rders_simp (RSEQ r1 r2) s)
+ \<le> max (2 + N1 + (rsize r2) + (N2 * card (sizeNregex N2))) (rsize (RSEQ r1 r2))"
+proof(cases s)
+ case Nil
+ then show "rsize (rders_simp (RSEQ r1 r2) s)
+ \<le> max (2 + N1 + (rsize r2) + (N2 * card (sizeNregex N2))) (rsize (RSEQ r1 r2))"
+ by simp
+next
+ case (Cons a list)
+ then have "rsize (rders_simp (RSEQ r1 r2) s) =
+ rsize (rsimp (RALTS ((RSEQ (rders_simp r1 s) r2) # (map (rders_simp r2) (vsuf s r1)))))"
+ using seq_closed_form_variant by (metis list.distinct(1))
+ also have "... \<le> Suc (rsizes (rdistinct (RSEQ (rders_simp r1 s) r2 # map (rders_simp r2) (vsuf s r1)) {}))"
+ using alts_simp_control by blast
+ also have "... \<le> 2 + N1 + (rsize r2) + (N2 * card (sizeNregex N2))"
+ using seq_estimate_bounded[OF assms] by auto
+ ultimately show "rsize (rders_simp (RSEQ r1 r2) s)
+ \<le> max (2 + N1 + (rsize r2) + N2 * card (sizeNregex N2)) (rsize (RSEQ r1 r2))"
+ by auto
+qed
+
+
+lemma rders_simp_bounded:
+ shows "\<exists>N. \<forall>s. rsize (rders_simp r s) \<le> N"
+ apply(induct r)
+ apply(rule_tac x = "Suc 0 " in exI)
+ using three_easy_cases0 apply force
+ using three_easy_cases1 apply blast
+ using three_easy_casesC apply blast
+ apply(erule exE)+
+ apply(rule exI)
+ apply(rule allI)
+ apply(rule seq_closed_form_bounded2)
+ apply(assumption)
+ apply(assumption)
+ apply (metis alts_closed_form_bounded size_list_estimation')
+ using star_closed_form_bounded by blast
+
+
+unused_thms
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/thys3/FBound.thy Wed Jun 29 12:38:05 2022 +0100
@@ -0,0 +1,180 @@
+
+theory FBound
+ imports "BlexerSimp" "ClosedFormsBounds"
+begin
+
+fun distinctBy :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b set \<Rightarrow> 'a list"
+ where
+ "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)))"
+
+fun rerase :: "arexp \<Rightarrow> rrexp"
+where
+ "rerase AZERO = RZERO"
+| "rerase (AONE _) = RONE"
+| "rerase (ACHAR _ c) = RCHAR c"
+| "rerase (AALTs bs rs) = RALTS (map rerase rs)"
+| "rerase (ASEQ _ r1 r2) = RSEQ (rerase r1) (rerase r2)"
+| "rerase (ASTAR _ r) = RSTAR (rerase r)"
+
+lemma eq1_rerase:
+ shows "x ~1 y \<longleftrightarrow> (rerase x) = (rerase y)"
+ apply(induct x y rule: eq1.induct)
+ apply(auto)
+ done
+
+
+lemma distinctBy_distinctWith:
+ shows "distinctBy xs f (f ` acc) = distinctWith xs (\<lambda>x y. f x = f y) acc"
+ apply(induct xs arbitrary: acc)
+ apply(auto)
+ by (metis image_insert)
+
+lemma distinctBy_distinctWith2:
+ shows "distinctBy xs rerase {} = distinctWith xs eq1 {}"
+ apply(subst distinctBy_distinctWith[of _ _ "{}", simplified])
+ using eq1_rerase by presburger
+
+lemma asize_rsize:
+ shows "rsize (rerase r) = asize r"
+ apply(induct r rule: rerase.induct)
+ apply(auto)
+ apply (metis (mono_tags, lifting) comp_apply map_eq_conv)
+ done
+
+lemma rerase_fuse:
+ shows "rerase (fuse bs r) = rerase r"
+ apply(induct r)
+ apply simp+
+ done
+
+lemma rerase_bsimp_ASEQ:
+ shows "rerase (bsimp_ASEQ x1 a1 a2) = rsimp_SEQ (rerase a1) (rerase a2)"
+ apply(induct x1 a1 a2 rule: bsimp_ASEQ.induct)
+ apply(auto)
+ done
+
+lemma rerase_bsimp_AALTs:
+ shows "rerase (bsimp_AALTs bs rs) = rsimp_ALTs (map rerase rs)"
+ apply(induct bs rs rule: bsimp_AALTs.induct)
+ apply(auto simp add: rerase_fuse)
+ done
+
+fun anonalt :: "arexp \<Rightarrow> bool"
+ where
+ "anonalt (AALTs bs2 rs) = False"
+| "anonalt r = True"
+
+
+fun agood :: "arexp \<Rightarrow> bool" where
+ "agood AZERO = False"
+| "agood (AONE cs) = True"
+| "agood (ACHAR cs c) = True"
+| "agood (AALTs cs []) = False"
+| "agood (AALTs cs [r]) = False"
+| "agood (AALTs cs (r1#r2#rs)) = (distinct (map rerase (r1 # r2 # rs)) \<and>(\<forall>r' \<in> set (r1#r2#rs). agood r' \<and> anonalt r'))"
+| "agood (ASEQ _ AZERO _) = False"
+| "agood (ASEQ _ (AONE _) _) = False"
+| "agood (ASEQ _ _ AZERO) = False"
+| "agood (ASEQ cs r1 r2) = (agood r1 \<and> agood r2)"
+| "agood (ASTAR cs r) = True"
+
+
+fun anonnested :: "arexp \<Rightarrow> bool"
+ where
+ "anonnested (AALTs bs2 []) = True"
+| "anonnested (AALTs bs2 ((AALTs bs1 rs1) # rs2)) = False"
+| "anonnested (AALTs bs2 (r # rs2)) = anonnested (AALTs bs2 rs2)"
+| "anonnested r = True"
+
+
+lemma asize0:
+ shows "0 < asize r"
+ apply(induct r)
+ apply(auto)
+ done
+
+lemma rnullable:
+ shows "rnullable (rerase r) = bnullable r"
+ apply(induct r rule: rerase.induct)
+ apply(auto)
+ done
+
+lemma rder_bder_rerase:
+ shows "rder c (rerase r ) = rerase (bder c r)"
+ apply (induct r)
+ apply (auto)
+ using rerase_fuse apply presburger
+ using rnullable apply blast
+ using rnullable by blast
+
+lemma rerase_map_bsimp:
+ assumes "\<And> r. r \<in> set rs \<Longrightarrow> rerase (bsimp r) = (rsimp \<circ> rerase) r"
+ shows "map rerase (map bsimp rs) = map (rsimp \<circ> rerase) rs"
+ using assms
+ apply(induct rs)
+ by simp_all
+
+
+lemma rerase_flts:
+ shows "map rerase (flts rs) = rflts (map rerase rs)"
+ apply(induct rs rule: flts.induct)
+ apply(auto simp add: rerase_fuse)
+ done
+
+lemma rerase_dB:
+ shows "map rerase (distinctBy rs rerase acc) = rdistinct (map rerase rs) acc"
+ apply(induct rs arbitrary: acc)
+ apply simp+
+ done
+
+lemma rerase_earlier_later_same:
+ assumes " \<And>r. r \<in> set rs \<Longrightarrow> rerase (bsimp r) = rsimp (rerase r)"
+ shows " (map rerase (distinctBy (flts (map bsimp rs)) rerase {})) =
+ (rdistinct (rflts (map (rsimp \<circ> rerase) rs)) {})"
+ apply(subst rerase_dB)
+ apply(subst rerase_flts)
+ apply(subst rerase_map_bsimp)
+ apply auto
+ using assms
+ apply simp
+ done
+
+lemma bsimp_rerase:
+ shows "rerase (bsimp a) = rsimp (rerase a)"
+ apply(induct a rule: bsimp.induct)
+ apply(auto)
+ using rerase_bsimp_ASEQ apply presburger
+ using distinctBy_distinctWith2 rerase_bsimp_AALTs rerase_earlier_later_same by fastforce
+
+lemma rders_simp_size:
+ shows "rders_simp (rerase r) s = rerase (bders_simp r s)"
+ apply(induct s rule: rev_induct)
+ apply simp
+ by (simp add: bders_simp_append rder_bder_rerase rders_simp_append bsimp_rerase)
+
+
+corollary aders_simp_finiteness:
+ assumes "\<exists>N. \<forall>s. rsize (rders_simp (rerase r) s) \<le> N"
+ shows " \<exists>N. \<forall>s. asize (bders_simp r s) \<le> N"
+proof -
+ from assms obtain N where "\<forall>s. rsize (rders_simp (rerase r) s) \<le> N"
+ by blast
+ then have "\<forall>s. rsize (rerase (bders_simp r s)) \<le> N"
+ by (simp add: rders_simp_size)
+ then have "\<forall>s. asize (bders_simp r s) \<le> N"
+ by (simp add: asize_rsize)
+ then show "\<exists>N. \<forall>s. asize (bders_simp r s) \<le> N" by blast
+qed
+
+theorem annotated_size_bound:
+ shows "\<exists>N. \<forall>s. asize (bders_simp r s) \<le> N"
+ apply(insert aders_simp_finiteness)
+ by (simp add: rders_simp_bounded)
+
+
+unused_thms
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/thys3/GeneralRegexBound.thy Wed Jun 29 12:38:05 2022 +0100
@@ -0,0 +1,212 @@
+theory GeneralRegexBound
+ imports "BasicIdentities"
+begin
+
+lemma size_geq1:
+ shows "rsize r \<ge> 1"
+ by (induct r) auto
+
+definition RSEQ_set where
+ "RSEQ_set A n \<equiv> {RSEQ r1 r2 | r1 r2. r1 \<in> A \<and> r2 \<in> A \<and> rsize r1 + rsize r2 \<le> n}"
+
+definition RSEQ_set_cartesian where
+ "RSEQ_set_cartesian A = {RSEQ r1 r2 | r1 r2. r1 \<in> A \<and> r2 \<in> A}"
+
+definition RALT_set where
+ "RALT_set A n \<equiv> {RALTS rs | rs. set rs \<subseteq> A \<and> rsizes rs \<le> n}"
+
+definition RALTs_set where
+ "RALTs_set A n \<equiv> {RALTS rs | rs. \<forall>r \<in> set rs. r \<in> A \<and> rsizes rs \<le> n}"
+
+definition
+ "sizeNregex N \<equiv> {r. rsize r \<le> N}"
+
+
+lemma sizenregex_induct1:
+ "sizeNregex (Suc n) = (({RZERO, RONE} \<union> {RCHAR c| c. True})
+ \<union> (RSTAR ` sizeNregex n)
+ \<union> (RSEQ_set (sizeNregex n) n)
+ \<union> (RALTs_set (sizeNregex n) n))"
+ apply(auto)
+ apply(case_tac x)
+ apply(auto simp add: RSEQ_set_def)
+ using sizeNregex_def apply force
+ using sizeNregex_def apply auto[1]
+ apply (simp add: sizeNregex_def)
+ apply (simp add: sizeNregex_def)
+ apply (simp add: RALTs_set_def)
+ apply (metis imageI list.set_map member_le_sum_list order_trans)
+ apply (simp add: sizeNregex_def)
+ apply (simp add: sizeNregex_def)
+ apply (simp add: sizeNregex_def)
+ using sizeNregex_def apply force
+ apply (simp add: sizeNregex_def)
+ apply (simp add: sizeNregex_def)
+ apply (simp add: RALTs_set_def)
+ apply(simp add: sizeNregex_def)
+ apply(auto)
+ using ex_in_conv by fastforce
+
+lemma s4:
+ "RSEQ_set A n \<subseteq> RSEQ_set_cartesian A"
+ using RSEQ_set_cartesian_def RSEQ_set_def by fastforce
+
+lemma s5:
+ assumes "finite A"
+ shows "finite (RSEQ_set_cartesian A)"
+ using assms
+ apply(subgoal_tac "RSEQ_set_cartesian A = (\<lambda>(x1, x2). RSEQ x1 x2) ` (A \<times> A)")
+ apply simp
+ unfolding RSEQ_set_cartesian_def
+ apply(auto)
+ done
+
+
+definition RALTs_set_length
+ where
+ "RALTs_set_length A n l \<equiv> {RALTS rs | rs. \<forall>r \<in> set rs. r \<in> A \<and> rsizes rs \<le> n \<and> length rs \<le> l}"
+
+
+definition RALTs_set_length2
+ where
+ "RALTs_set_length2 A l \<equiv> {RALTS rs | rs. \<forall>r \<in> set rs. r \<in> A \<and> length rs \<le> l}"
+
+definition set_length2
+ where
+ "set_length2 A l \<equiv> {rs. \<forall>r \<in> set rs. r \<in> A \<and> length rs \<le> l}"
+
+
+lemma r000:
+ shows "RALTs_set_length A n l \<subseteq> RALTs_set_length2 A l"
+ apply(auto simp add: RALTs_set_length2_def RALTs_set_length_def)
+ done
+
+
+lemma r02:
+ shows "set_length2 A 0 \<subseteq> {[]}"
+ apply(auto simp add: set_length2_def)
+ apply(case_tac x)
+ apply(auto)
+ done
+
+lemma r03:
+ shows "set_length2 A (Suc n) \<subseteq>
+ {[]} \<union> (\<lambda>(h, t). h # t) ` (A \<times> (set_length2 A n))"
+ apply(auto simp add: set_length2_def)
+ apply(case_tac x)
+ apply(auto)
+ done
+
+lemma r1:
+ assumes "finite A"
+ shows "finite (set_length2 A n)"
+ using assms
+ apply(induct n)
+ apply(rule finite_subset)
+ apply(rule r02)
+ apply(simp)
+ apply(rule finite_subset)
+ apply(rule r03)
+ apply(simp)
+ done
+
+lemma size_sum_more_than_len:
+ shows "rsizes rs \<ge> length rs"
+ apply(induct rs)
+ apply simp
+ apply simp
+ apply(subgoal_tac "rsize a \<ge> 1")
+ apply linarith
+ using size_geq1 by auto
+
+
+lemma sum_list_len:
+ shows "rsizes rs \<le> n \<Longrightarrow> length rs \<le> n"
+ by (meson order.trans size_sum_more_than_len)
+
+
+lemma t2:
+ shows "RALTs_set A n \<subseteq> RALTs_set_length A n n"
+ unfolding RALTs_set_length_def RALTs_set_def
+ apply(auto)
+ using sum_list_len by blast
+
+lemma s8_aux:
+ assumes "finite A"
+ shows "finite (RALTs_set_length A n n)"
+proof -
+ have "finite A" by fact
+ then have "finite (set_length2 A n)"
+ by (simp add: r1)
+ moreover have "(RALTS ` (set_length2 A n)) = RALTs_set_length2 A n"
+ unfolding RALTs_set_length2_def set_length2_def
+ by (auto)
+ ultimately have "finite (RALTs_set_length2 A n)"
+ by (metis finite_imageI)
+ then show ?thesis
+ by (metis infinite_super r000)
+qed
+
+lemma char_finite:
+ shows "finite {RCHAR c |c. True}"
+ apply simp
+ apply(subgoal_tac "finite (RCHAR ` (UNIV::char set))")
+ prefer 2
+ apply simp
+ by (simp add: full_SetCompr_eq)
+
+
+lemma finite_size_n:
+ shows "finite (sizeNregex n)"
+ apply(induct n)
+ apply(simp add: sizeNregex_def)
+ apply (metis (mono_tags, lifting) not_finite_existsD not_one_le_zero size_geq1)
+ apply(subst sizenregex_induct1)
+ apply(simp only: finite_Un)
+ apply(rule conjI)+
+ apply(simp)
+
+ using char_finite apply blast
+ apply(simp)
+ apply(rule finite_subset)
+ apply(rule s4)
+ apply(rule s5)
+ apply(simp)
+ apply(rule finite_subset)
+ apply(rule t2)
+ apply(rule s8_aux)
+ apply(simp)
+ done
+
+lemma three_easy_cases0:
+ shows "rsize (rders_simp RZERO s) \<le> Suc 0"
+ apply(induct s)
+ apply simp
+ apply simp
+ done
+
+
+lemma three_easy_cases1:
+ shows "rsize (rders_simp RONE s) \<le> Suc 0"
+ apply(induct s)
+ apply simp
+ apply simp
+ using three_easy_cases0 by auto
+
+
+lemma three_easy_casesC:
+ shows "rsize (rders_simp (RCHAR c) s) \<le> Suc 0"
+ apply(induct s)
+ apply simp
+ apply simp
+ apply(case_tac " a = c")
+ using three_easy_cases1 apply blast
+ apply simp
+ using three_easy_cases0 by force
+
+
+unused_thms
+
+
+end
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/thys3/HarderProps.thy Wed Jun 29 12:38:05 2022 +0100
@@ -0,0 +1,289 @@
+theory HarderProps imports BasicIdentities
+begin
+
+
+
+
+lemma spawn_simp_rsimpalts:
+ shows "rsimp (rsimp_ALTs rs) = rsimp (rsimp_ALTs (map rsimp rs))"
+ apply(cases rs)
+ apply simp
+ apply(case_tac list)
+ apply simp
+ apply(subst rsimp_idem[symmetric])
+ apply simp
+ apply(subgoal_tac "rsimp_ALTs rs = RALTS rs")
+ apply(simp only:)
+ apply(subgoal_tac "rsimp_ALTs (map rsimp rs) = RALTS (map rsimp rs)")
+ apply(simp only:)
+ prefer 2
+ apply simp
+ prefer 2
+ using rsimp_ALTs.simps(3) apply presburger
+ apply auto
+ apply(subst rsimp_idem)+
+ by (metis comp_apply rsimp_idem)
+
+
+
+
+lemma good1_rsimpalts:
+ shows "rsimp r = RALTS rs \<Longrightarrow> rsimp_ALTs rs = RALTS rs"
+ by (metis no_alt_short_list_after_simp)
+
+
+
+
+lemma good1_flatten:
+ shows "\<lbrakk> rsimp r = (RALTS rs1)\<rbrakk>
+ \<Longrightarrow> rflts (rsimp_ALTs rs1 # map rsimp rsb) = rflts (rs1 @ map rsimp rsb)"
+ apply(subst good1_rsimpalts)
+ apply simp+
+ apply(subgoal_tac "rflts (rs1 @ map rsimp rsb) = rs1 @ rflts (map rsimp rsb)")
+ apply simp
+ using flts_append rsimp_inner_idem4 by presburger
+
+
+lemma flatten_rsimpalts:
+ shows "rflts (rsimp_ALTs (rdistinct (rflts (map rsimp rsa)) {}) # map rsimp rsb) =
+ rflts ( (rdistinct (rflts (map rsimp rsa)) {}) @ map rsimp rsb)"
+ apply(case_tac "map rsimp rsa")
+ apply simp
+ apply(case_tac "list")
+ apply simp
+ apply(case_tac a)
+ apply simp+
+ apply(rename_tac rs1)
+ apply (metis good1_flatten map_eq_Cons_D no_further_dB_after_simp)
+
+ apply simp
+
+ apply(subgoal_tac "\<forall>r \<in> set( rflts (map rsimp rsa)). good r")
+ apply(case_tac "rdistinct (rflts (map rsimp rsa)) {}")
+ apply simp
+ apply(case_tac "listb")
+ apply simp+
+ apply (metis Cons_eq_appendI good1_flatten rflts.simps(3) rsimp.simps(2) rsimp_ALTs.simps(3))
+ by (metis (mono_tags, lifting) flts3 good1 image_iff list.set_map)
+
+
+
+
+
+
+lemma simp_flatten:
+ shows "rsimp (RALTS ((RALTS rsa) # rsb)) = rsimp (RALTS (rsa @ rsb))"
+ apply simp
+ apply(subst flatten_rsimpalts)
+ apply(simp add: flts_append)
+ by (metis Diff_empty distinct_once_enough flts_append nonalt0_fltseq nonalt_flts_rd qqq1 rdistinct_set_equality1)
+
+
+
+
+
+lemma simp_flatten_aux0:
+ shows "rsimp (RALTS rs) = rsimp (RALTS (map rsimp rs))"
+ apply(induct rs)
+ apply simp+
+ by (metis (mono_tags, opaque_lifting) comp_eq_dest_lhs map_eq_conv rsimp_idem)
+
+
+
+
+
+
+lemma good_singleton:
+ shows "good a \<and> nonalt a \<Longrightarrow> rflts [a] = [a]"
+ using good.simps(1) k0b by blast
+
+
+
+
+
+lemma good_flatten_aux_aux1:
+ shows "\<lbrakk> size rs \<ge>2;
+\<forall>r \<in> set rs. good r \<and> r \<noteq> RZERO \<and> nonalt r; \<forall>r \<in> set rsb. good r \<and> r \<noteq> RZERO \<and> nonalt r \<rbrakk>
+ \<Longrightarrow> rdistinct (rs @ rsb) rset =
+ rdistinct (rflts [rsimp_ALTs (rdistinct rs {})] @ rsb) rset"
+ apply(induct rs arbitrary: rset)
+ apply simp
+ apply(case_tac "a \<in> rset")
+ apply simp
+ apply(case_tac "rdistinct rs {a}")
+ apply simp
+ apply(subst good_singleton)
+ apply force
+ apply simp
+ apply (meson all_that_same_elem)
+ apply(subgoal_tac "rflts [rsimp_ALTs (a # rdistinct rs {a})] = a # rdistinct rs {a} ")
+ prefer 2
+ using k0a rsimp_ALTs.simps(3) apply presburger
+ apply(simp only:)
+ apply(subgoal_tac "rdistinct (rs @ rsb) rset = rdistinct ((rdistinct (a # rs) {}) @ rsb) rset ")
+ apply (metis insert_absorb insert_is_Un insert_not_empty rdistinct.simps(2))
+ apply (meson distinct_eq_interesting1)
+ apply simp
+ apply(case_tac "rdistinct rs {a}")
+ prefer 2
+ apply(subgoal_tac "rsimp_ALTs (a # rdistinct rs {a}) = RALTS (a # rdistinct rs {a})")
+ apply(simp only:)
+ apply(subgoal_tac "a # rdistinct (rs @ rsb) (insert a rset) =
+ rdistinct (rflts [RALTS (a # rdistinct rs {a})] @ rsb) rset")
+ apply simp
+ apply (metis append_Cons distinct_early_app empty_iff insert_is_Un k0a rdistinct.simps(2))
+ using rsimp_ALTs.simps(3) apply presburger
+ by (metis Un_insert_left append_Cons distinct_early_app empty_iff good_singleton rdistinct.simps(2) rsimp_ALTs.simps(2) sup_bot_left)
+
+
+
+
+
+lemma good_flatten_aux_aux:
+ shows "\<lbrakk>\<exists>a aa lista list. rs = a # list \<and> list = aa # lista;
+\<forall>r \<in> set rs. good r \<and> r \<noteq> RZERO \<and> nonalt r; \<forall>r \<in> set rsb. good r \<and> r \<noteq> RZERO \<and> nonalt r \<rbrakk>
+ \<Longrightarrow> rdistinct (rs @ rsb) rset =
+ rdistinct (rflts [rsimp_ALTs (rdistinct rs {})] @ rsb) rset"
+ apply(erule exE)+
+ apply(subgoal_tac "size rs \<ge> 2")
+ apply (metis good_flatten_aux_aux1)
+ by (simp add: Suc_leI length_Cons less_add_Suc1)
+
+
+
+lemma good_flatten_aux:
+ shows " \<lbrakk>\<forall>r\<in>set rs. good r \<or> r = RZERO; \<forall>r\<in>set rsa . good r \<or> r = RZERO;
+ \<forall>r\<in>set rsb. good r \<or> r = RZERO;
+ rsimp (RALTS (rsa @ rs @ rsb)) = rsimp_ALTs (rdistinct (rflts (rsa @ rs @ rsb)) {});
+ rsimp (RALTS (rsa @ [RALTS rs] @ rsb)) =
+ rsimp_ALTs (rdistinct (rflts (rsa @ [rsimp (RALTS rs)] @ rsb)) {});
+ map rsimp rsa = rsa;
+ map rsimp rsb = rsb;
+ map rsimp rs = rs;
+ rdistinct (rflts rsa @ rflts rs @ rflts rsb) {} =
+ rdistinct (rflts rsa) {} @ rdistinct (rflts rs @ rflts rsb) (set (rflts rsa));
+ rdistinct (rflts rsa @ rflts [rsimp (RALTS rs)] @ rflts rsb) {} =
+ rdistinct (rflts rsa) {} @ rdistinct (rflts [rsimp (RALTS rs)] @ rflts rsb) (set (rflts rsa))\<rbrakk>
+ \<Longrightarrow> rdistinct (rflts rs @ rflts rsb) rset =
+ rdistinct (rflts [rsimp (RALTS rs)] @ rflts rsb) rset"
+ apply simp
+ apply(case_tac "rflts rs ")
+ apply simp
+ apply(case_tac "list")
+ apply simp
+ apply(case_tac "a \<in> rset")
+ apply simp
+ apply (metis append.left_neutral append_Cons equals0D k0b list.set_intros(1) nonalt_flts_rd qqq1 rdistinct.simps(2))
+ apply simp
+ apply (metis Un_insert_left append_Cons append_Nil ex_in_conv flts_single1 insertI1 list.simps(15) nonalt_flts_rd nonazero.elims(3) qqq1 rdistinct.simps(2) sup_bot_left)
+ apply(subgoal_tac "\<forall>r \<in> set (rflts rs). good r \<and> r \<noteq> RZERO \<and> nonalt r")
+ prefer 2
+ apply (metis Diff_empty flts3 nonalt_flts_rd qqq1 rdistinct_set_equality1)
+ apply(subgoal_tac "\<forall>r \<in> set (rflts rsb). good r \<and> r \<noteq> RZERO \<and> nonalt r")
+ prefer 2
+ apply (metis Diff_empty flts3 good.simps(1) nonalt_flts_rd rdistinct_set_equality1)
+ by (smt (verit, ccfv_threshold) good_flatten_aux_aux)
+
+
+
+
+lemma good_flatten_middle:
+ shows "\<lbrakk>\<forall>r \<in> set rs. good r \<or> r = RZERO;
+ \<forall>r \<in> set rsa. good r \<or> r = RZERO;
+ \<forall>r \<in> set rsb. good r \<or> r = RZERO\<rbrakk> \<Longrightarrow>
+rsimp (RALTS (rsa @ rs @ rsb)) =
+rsimp (RALTS (rsa @ [RALTS rs] @ rsb))"
+ apply(subgoal_tac "rsimp (RALTS (rsa @ rs @ rsb)) = rsimp_ALTs (rdistinct (rflts (map rsimp rsa @
+map rsimp rs @ map rsimp rsb)) {})")
+ prefer 2
+ apply simp
+ apply(simp only:)
+ apply(subgoal_tac "rsimp (RALTS (rsa @ [RALTS rs] @ rsb)) = rsimp_ALTs (rdistinct (rflts (map rsimp rsa @
+[rsimp (RALTS rs)] @ map rsimp rsb)) {})")
+ prefer 2
+ apply simp
+ apply(simp only:)
+ apply(subgoal_tac "map rsimp rsa = rsa")
+ prefer 2
+ apply (metis map_idI rsimp.simps(3) test)
+ apply(simp only:)
+ apply(subgoal_tac "map rsimp rsb = rsb")
+ prefer 2
+ apply (metis map_idI rsimp.simps(3) test)
+ apply(simp only:)
+ apply(subst flts_append)+
+ apply(subgoal_tac "map rsimp rs = rs")
+ apply(simp only:)
+ prefer 2
+ apply (metis map_idI rsimp.simps(3) test)
+ apply(subgoal_tac "rdistinct (rflts rsa @ rflts rs @ rflts rsb) {} =
+rdistinct (rflts rsa) {} @ rdistinct (rflts rs @ rflts rsb) (set (rflts rsa))")
+ apply(simp only:)
+ prefer 2
+ using rdistinct_concat_general apply blast
+ apply(subgoal_tac "rdistinct (rflts rsa @ rflts [rsimp (RALTS rs)] @ rflts rsb) {} =
+rdistinct (rflts rsa) {} @ rdistinct (rflts [rsimp (RALTS rs)] @ rflts rsb) (set (rflts rsa))")
+ apply(simp only:)
+ prefer 2
+ using rdistinct_concat_general apply blast
+ apply(subgoal_tac "rdistinct (rflts rs @ rflts rsb) (set (rflts rsa)) =
+ rdistinct (rflts [rsimp (RALTS rs)] @ rflts rsb) (set (rflts rsa))")
+ apply presburger
+ using good_flatten_aux by blast
+
+
+
+lemma simp_flatten3:
+ shows "rsimp (RALTS (rsa @ [RALTS rs ] @ rsb)) = rsimp (RALTS (rsa @ rs @ rsb))"
+ apply(subgoal_tac "rsimp (RALTS (rsa @ [RALTS rs] @ rsb)) =
+ rsimp (RALTS (map rsimp rsa @ [rsimp (RALTS rs)] @ map rsimp rsb)) ")
+ prefer 2
+ apply (metis append.left_neutral append_Cons list.simps(9) map_append simp_flatten_aux0)
+ apply (simp only:)
+ apply(subgoal_tac "rsimp (RALTS (rsa @ rs @ rsb)) =
+rsimp (RALTS (map rsimp rsa @ map rsimp rs @ map rsimp rsb))")
+ prefer 2
+ apply (metis map_append simp_flatten_aux0)
+ apply(simp only:)
+ apply(subgoal_tac "rsimp (RALTS (map rsimp rsa @ map rsimp rs @ map rsimp rsb)) =
+ rsimp (RALTS (map rsimp rsa @ [RALTS (map rsimp rs)] @ map rsimp rsb))")
+
+ apply (metis (no_types, lifting) head_one_more_simp map_append simp_flatten_aux0)
+ apply(subgoal_tac "\<forall>r \<in> set (map rsimp rsa). good r \<or> r = RZERO")
+ apply(subgoal_tac "\<forall>r \<in> set (map rsimp rs). good r \<or> r = RZERO")
+ apply(subgoal_tac "\<forall>r \<in> set (map rsimp rsb). good r \<or> r = RZERO")
+
+ using good_flatten_middle apply presburger
+ apply (simp add: good1)
+ apply (simp add: good1)
+ apply (simp add: good1)
+ done
+
+
+lemma simp_removes_duplicate1:
+ shows " a \<in> set rsa \<Longrightarrow> rsimp (RALTS (rsa @ [a])) = rsimp (RALTS (rsa))"
+and " rsimp (RALTS (a1 # rsa @ [a1])) = rsimp (RALTS (a1 # rsa))"
+ apply(induct rsa arbitrary: a1)
+ apply simp
+ apply simp
+ prefer 2
+ apply(case_tac "a = aa")
+ apply simp
+ apply simp
+ apply (metis Cons_eq_appendI Cons_eq_map_conv distinct_removes_duplicate_flts list.set_intros(2))
+ apply (metis append_Cons append_Nil distinct_removes_duplicate_flts list.set_intros(1) list.simps(8) list.simps(9))
+ by (metis (mono_tags, lifting) append_Cons distinct_removes_duplicate_flts list.set_intros(1) list.simps(8) list.simps(9) map_append rsimp.simps(2))
+
+lemma simp_removes_duplicate2:
+ shows "a \<in> set rsa \<Longrightarrow> rsimp (RALTS (rsa @ [a] @ rsb)) = rsimp (RALTS (rsa @ rsb))"
+ apply(induct rsb arbitrary: rsa)
+ apply simp
+ using distinct_removes_duplicate_flts apply auto[1]
+ by (metis append.assoc head_one_more_simp rsimp.simps(2) simp_flatten simp_removes_duplicate1(1))
+
+lemma simp_removes_duplicate3:
+ shows "a \<in> set rsa \<Longrightarrow> rsimp (RALTS (rsa @ a # rsb)) = rsimp (RALTS (rsa @ rsb))"
+ using simp_removes_duplicate2 by auto
+
+
+end
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/thys3/Lexer.thy Wed Jun 29 12:38:05 2022 +0100
@@ -0,0 +1,417 @@
+
+theory Lexer
+ imports PosixSpec
+begin
+
+section {* The Lexer Functions by Sulzmann and Lu (without simplification) *}
+
+fun
+ mkeps :: "rexp \<Rightarrow> val"
+where
+ "mkeps(ONE) = Void"
+| "mkeps(SEQ r1 r2) = Seq (mkeps r1) (mkeps r2)"
+| "mkeps(ALT r1 r2) = (if nullable(r1) then Left (mkeps r1) else Right (mkeps r2))"
+| "mkeps(STAR r) = Stars []"
+
+fun injval :: "rexp \<Rightarrow> char \<Rightarrow> val \<Rightarrow> val"
+where
+ "injval (CH d) c Void = Char d"
+| "injval (ALT r1 r2) c (Left v1) = Left(injval r1 c v1)"
+| "injval (ALT r1 r2) c (Right v2) = Right(injval r2 c v2)"
+| "injval (SEQ r1 r2) c (Seq v1 v2) = Seq (injval r1 c v1) v2"
+| "injval (SEQ r1 r2) c (Left (Seq v1 v2)) = Seq (injval r1 c v1) v2"
+| "injval (SEQ r1 r2) c (Right v2) = Seq (mkeps r1) (injval r2 c v2)"
+| "injval (STAR r) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)"
+
+fun
+ lexer :: "rexp \<Rightarrow> string \<Rightarrow> val option"
+where
+ "lexer r [] = (if nullable r then Some(mkeps r) else None)"
+| "lexer r (c#s) = (case (lexer (der c r) s) of
+ None \<Rightarrow> None
+ | Some(v) \<Rightarrow> Some(injval r c v))"
+
+
+
+section {* Mkeps, Injval Properties *}
+
+lemma mkeps_nullable:
+ assumes "nullable(r)"
+ shows "\<Turnstile> mkeps r : r"
+using assms
+by (induct rule: nullable.induct)
+ (auto intro: Prf.intros)
+
+lemma mkeps_flat:
+ assumes "nullable(r)"
+ shows "flat (mkeps r) = []"
+using assms
+by (induct rule: nullable.induct) (auto)
+
+lemma Prf_injval_flat:
+ assumes "\<Turnstile> v : der c r"
+ shows "flat (injval r c v) = c # (flat v)"
+using assms
+apply(induct c r arbitrary: v rule: der.induct)
+apply(auto elim!: Prf_elims intro: mkeps_flat split: if_splits)
+done
+
+lemma Prf_injval:
+ assumes "\<Turnstile> v : der c r"
+ shows "\<Turnstile> (injval r c v) : r"
+using assms
+apply(induct r arbitrary: c v rule: rexp.induct)
+apply(auto intro!: Prf.intros mkeps_nullable elim!: Prf_elims split: if_splits)
+apply(simp add: Prf_injval_flat)
+done
+
+
+
+text {*
+ Mkeps and injval produce, or preserve, Posix values.
+*}
+
+lemma Posix_mkeps:
+ assumes "nullable r"
+ shows "[] \<in> r \<rightarrow> mkeps r"
+using assms
+apply(induct r rule: nullable.induct)
+apply(auto intro: Posix.intros simp add: nullable_correctness Sequ_def)
+apply(subst append.simps(1)[symmetric])
+apply(rule Posix.intros)
+apply(auto)
+done
+
+lemma Posix_injval:
+ assumes "s \<in> (der c r) \<rightarrow> v"
+ shows "(c # s) \<in> r \<rightarrow> (injval r c v)"
+using assms
+proof(induct r arbitrary: s v rule: rexp.induct)
+ case ZERO
+ have "s \<in> der c ZERO \<rightarrow> v" by fact
+ then have "s \<in> ZERO \<rightarrow> v" by simp
+ then have "False" by cases
+ then show "(c # s) \<in> ZERO \<rightarrow> (injval ZERO c v)" by simp
+next
+ case ONE
+ have "s \<in> der c ONE \<rightarrow> v" by fact
+ then have "s \<in> ZERO \<rightarrow> v" by simp
+ then have "False" by cases
+ then show "(c # s) \<in> ONE \<rightarrow> (injval ONE c v)" by simp
+next
+ case (CH d)
+ consider (eq) "c = d" | (ineq) "c \<noteq> d" by blast
+ then show "(c # s) \<in> (CH d) \<rightarrow> (injval (CH d) c v)"
+ proof (cases)
+ case eq
+ have "s \<in> der c (CH d) \<rightarrow> v" by fact
+ then have "s \<in> ONE \<rightarrow> v" using eq by simp
+ then have eqs: "s = [] \<and> v = Void" by cases simp
+ show "(c # s) \<in> CH d \<rightarrow> injval (CH d) c v" using eq eqs
+ by (auto intro: Posix.intros)
+ next
+ case ineq
+ have "s \<in> der c (CH d) \<rightarrow> v" by fact
+ then have "s \<in> ZERO \<rightarrow> v" using ineq by simp
+ then have "False" by cases
+ then show "(c # s) \<in> CH d \<rightarrow> injval (CH d) c v" by simp
+ qed
+next
+ case (ALT r1 r2)
+ have IH1: "\<And>s v. s \<in> der c r1 \<rightarrow> v \<Longrightarrow> (c # s) \<in> r1 \<rightarrow> injval r1 c v" by fact
+ have IH2: "\<And>s v. s \<in> der c r2 \<rightarrow> v \<Longrightarrow> (c # s) \<in> r2 \<rightarrow> injval r2 c v" by fact
+ have "s \<in> der c (ALT r1 r2) \<rightarrow> v" by fact
+ then have "s \<in> ALT (der c r1) (der c r2) \<rightarrow> v" by simp
+ then consider (left) v' where "v = Left v'" "s \<in> der c r1 \<rightarrow> v'"
+ | (right) v' where "v = Right v'" "s \<notin> L (der c r1)" "s \<in> der c r2 \<rightarrow> v'"
+ by cases auto
+ then show "(c # s) \<in> ALT r1 r2 \<rightarrow> injval (ALT r1 r2) c v"
+ proof (cases)
+ case left
+ have "s \<in> der c r1 \<rightarrow> v'" by fact
+ then have "(c # s) \<in> r1 \<rightarrow> injval r1 c v'" using IH1 by simp
+ then have "(c # s) \<in> ALT r1 r2 \<rightarrow> injval (ALT r1 r2) c (Left v')" by (auto intro: Posix.intros)
+ then show "(c # s) \<in> ALT r1 r2 \<rightarrow> injval (ALT r1 r2) c v" using left by simp
+ next
+ case right
+ have "s \<notin> L (der c r1)" by fact
+ then have "c # s \<notin> L r1" by (simp add: der_correctness Der_def)
+ moreover
+ have "s \<in> der c r2 \<rightarrow> v'" by fact
+ then have "(c # s) \<in> r2 \<rightarrow> injval r2 c v'" using IH2 by simp
+ ultimately have "(c # s) \<in> ALT r1 r2 \<rightarrow> injval (ALT r1 r2) c (Right v')"
+ by (auto intro: Posix.intros)
+ then show "(c # s) \<in> ALT r1 r2 \<rightarrow> injval (ALT r1 r2) c v" using right by simp
+ qed
+next
+ case (SEQ r1 r2)
+ have IH1: "\<And>s v. s \<in> der c r1 \<rightarrow> v \<Longrightarrow> (c # s) \<in> r1 \<rightarrow> injval r1 c v" by fact
+ have IH2: "\<And>s v. s \<in> der c r2 \<rightarrow> v \<Longrightarrow> (c # s) \<in> r2 \<rightarrow> injval r2 c v" by fact
+ have "s \<in> der c (SEQ r1 r2) \<rightarrow> v" by fact
+ then consider
+ (left_nullable) v1 v2 s1 s2 where
+ "v = Left (Seq v1 v2)" "s = s1 @ s2"
+ "s1 \<in> der c r1 \<rightarrow> v1" "s2 \<in> r2 \<rightarrow> v2" "nullable r1"
+ "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L (der c r1) \<and> s\<^sub>4 \<in> L r2)"
+ | (right_nullable) v1 s1 s2 where
+ "v = Right v1" "s = s1 @ s2"
+ "s \<in> der c r2 \<rightarrow> v1" "nullable r1" "s1 @ s2 \<notin> L (SEQ (der c r1) r2)"
+ | (not_nullable) v1 v2 s1 s2 where
+ "v = Seq v1 v2" "s = s1 @ s2"
+ "s1 \<in> der c r1 \<rightarrow> v1" "s2 \<in> r2 \<rightarrow> v2" "\<not>nullable r1"
+ "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L (der c r1) \<and> s\<^sub>4 \<in> L r2)"
+ by (force split: if_splits elim!: Posix_elims simp add: Sequ_def der_correctness Der_def)
+ then show "(c # s) \<in> SEQ r1 r2 \<rightarrow> injval (SEQ r1 r2) c v"
+ proof (cases)
+ case left_nullable
+ have "s1 \<in> der c r1 \<rightarrow> v1" by fact
+ then have "(c # s1) \<in> r1 \<rightarrow> injval r1 c v1" using IH1 by simp
+ moreover
+ have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L (der c r1) \<and> s\<^sub>4 \<in> L r2)" by fact
+ then have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (c # s1) @ s\<^sub>3 \<in> L r1 \<and> s\<^sub>4 \<in> L r2)" by (simp add: der_correctness Der_def)
+ ultimately have "((c # s1) @ s2) \<in> SEQ r1 r2 \<rightarrow> Seq (injval r1 c v1) v2" using left_nullable by (rule_tac Posix.intros)
+ then show "(c # s) \<in> SEQ r1 r2 \<rightarrow> injval (SEQ r1 r2) c v" using left_nullable by simp
+ next
+ case right_nullable
+ have "nullable r1" by fact
+ then have "[] \<in> r1 \<rightarrow> (mkeps r1)" by (rule Posix_mkeps)
+ moreover
+ have "s \<in> der c r2 \<rightarrow> v1" by fact
+ then have "(c # s) \<in> r2 \<rightarrow> (injval r2 c v1)" using IH2 by simp
+ moreover
+ have "s1 @ s2 \<notin> L (SEQ (der c r1) r2)" by fact
+ then have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = c # s \<and> [] @ s\<^sub>3 \<in> L r1 \<and> s\<^sub>4 \<in> L r2)" using right_nullable
+ by(auto simp add: der_correctness Der_def append_eq_Cons_conv Sequ_def)
+ ultimately have "([] @ (c # s)) \<in> SEQ r1 r2 \<rightarrow> Seq (mkeps r1) (injval r2 c v1)"
+ by(rule Posix.intros)
+ then show "(c # s) \<in> SEQ r1 r2 \<rightarrow> injval (SEQ r1 r2) c v" using right_nullable by simp
+ next
+ case not_nullable
+ have "s1 \<in> der c r1 \<rightarrow> v1" by fact
+ then have "(c # s1) \<in> r1 \<rightarrow> injval r1 c v1" using IH1 by simp
+ moreover
+ have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L (der c r1) \<and> s\<^sub>4 \<in> L r2)" by fact
+ then have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (c # s1) @ s\<^sub>3 \<in> L r1 \<and> s\<^sub>4 \<in> L r2)" by (simp add: der_correctness Der_def)
+ ultimately have "((c # s1) @ s2) \<in> SEQ r1 r2 \<rightarrow> Seq (injval r1 c v1) v2" using not_nullable
+ by (rule_tac Posix.intros) (simp_all)
+ then show "(c # s) \<in> SEQ r1 r2 \<rightarrow> injval (SEQ r1 r2) c v" using not_nullable by simp
+ qed
+next
+ case (STAR r)
+ have IH: "\<And>s v. s \<in> der c r \<rightarrow> v \<Longrightarrow> (c # s) \<in> r \<rightarrow> injval r c v" by fact
+ have "s \<in> der c (STAR r) \<rightarrow> v" by fact
+ then consider
+ (cons) v1 vs s1 s2 where
+ "v = Seq v1 (Stars vs)" "s = s1 @ s2"
+ "s1 \<in> der c r \<rightarrow> v1" "s2 \<in> (STAR r) \<rightarrow> (Stars vs)"
+ "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L (der c r) \<and> s\<^sub>4 \<in> L (STAR r))"
+ apply(auto elim!: Posix_elims(1-5) simp add: der_correctness Der_def intro: Posix.intros)
+ apply(rotate_tac 3)
+ apply(erule_tac Posix_elims(6))
+ apply (simp add: Posix.intros(6))
+ using Posix.intros(7) by blast
+ then show "(c # s) \<in> STAR r \<rightarrow> injval (STAR r) c v"
+ proof (cases)
+ case cons
+ have "s1 \<in> der c r \<rightarrow> v1" by fact
+ then have "(c # s1) \<in> r \<rightarrow> injval r c v1" using IH by simp
+ moreover
+ have "s2 \<in> STAR r \<rightarrow> Stars vs" by fact
+ moreover
+ have "(c # s1) \<in> r \<rightarrow> injval r c v1" by fact
+ then have "flat (injval r c v1) = (c # s1)" by (rule Posix1)
+ then have "flat (injval r c v1) \<noteq> []" by simp
+ moreover
+ have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L (der c r) \<and> s\<^sub>4 \<in> L (STAR r))" by fact
+ then have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (c # s1) @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (STAR r))"
+ by (simp add: der_correctness Der_def)
+ ultimately
+ have "((c # s1) @ s2) \<in> STAR r \<rightarrow> Stars (injval r c v1 # vs)" by (rule Posix.intros)
+ then show "(c # s) \<in> STAR r \<rightarrow> injval (STAR r) c v" using cons by(simp)
+ qed
+qed
+
+
+section {* Lexer Correctness *}
+
+
+lemma lexer_correct_None:
+ shows "s \<notin> L r \<longleftrightarrow> lexer r s = None"
+ apply(induct s arbitrary: r)
+ apply(simp)
+ apply(simp add: nullable_correctness)
+ apply(simp)
+ apply(drule_tac x="der a r" in meta_spec)
+ apply(auto)
+ apply(auto simp add: der_correctness Der_def)
+done
+
+lemma lexer_correct_Some:
+ shows "s \<in> L r \<longleftrightarrow> (\<exists>v. lexer r s = Some(v) \<and> s \<in> r \<rightarrow> v)"
+ apply(induct s arbitrary : r)
+ apply(simp only: lexer.simps)
+ apply(simp)
+ apply(simp add: nullable_correctness Posix_mkeps)
+ apply(drule_tac x="der a r" in meta_spec)
+ apply(simp (no_asm_use) add: der_correctness Der_def del: lexer.simps)
+ apply(simp del: lexer.simps)
+ apply(simp only: lexer.simps)
+ apply(case_tac "lexer (der a r) s = None")
+ apply(auto)[1]
+ apply(simp)
+ apply(erule exE)
+ apply(simp)
+ apply(rule iffI)
+ apply(simp add: Posix_injval)
+ apply(simp add: Posix1(1))
+done
+
+lemma lexer_correctness:
+ shows "(lexer r s = Some v) \<longleftrightarrow> s \<in> r \<rightarrow> v"
+ and "(lexer r s = None) \<longleftrightarrow> \<not>(\<exists>v. s \<in> r \<rightarrow> v)"
+using Posix1(1) Posix_determ lexer_correct_None lexer_correct_Some apply fastforce
+using Posix1(1) lexer_correct_None lexer_correct_Some by blast
+
+
+subsection {* A slight reformulation of the lexer algorithm using stacked functions*}
+
+fun flex :: "rexp \<Rightarrow> (val \<Rightarrow> val) => string \<Rightarrow> (val \<Rightarrow> val)"
+ where
+ "flex r f [] = f"
+| "flex r f (c#s) = flex (der c r) (\<lambda>v. f (injval r c v)) s"
+
+lemma flex_fun_apply:
+ shows "g (flex r f s v) = flex r (g o f) s v"
+ apply(induct s arbitrary: g f r v)
+ apply(simp_all add: comp_def)
+ by meson
+
+lemma flex_fun_apply2:
+ shows "g (flex r id s v) = flex r g s v"
+ by (simp add: flex_fun_apply)
+
+
+lemma flex_append:
+ shows "flex r f (s1 @ s2) = flex (ders s1 r) (flex r f s1) s2"
+ apply(induct s1 arbitrary: s2 r f)
+ apply(simp_all)
+ done
+
+lemma lexer_flex:
+ shows "lexer r s = (if nullable (ders s r)
+ then Some(flex r id s (mkeps (ders s r))) else None)"
+ apply(induct s arbitrary: r)
+ apply(simp_all add: flex_fun_apply)
+ done
+
+lemma Posix_flex:
+ assumes "s2 \<in> (ders s1 r) \<rightarrow> v"
+ shows "(s1 @ s2) \<in> r \<rightarrow> flex r id s1 v"
+ using assms
+ apply(induct s1 arbitrary: r v s2)
+ apply(simp)
+ apply(simp)
+ apply(drule_tac x="der a r" in meta_spec)
+ apply(drule_tac x="v" in meta_spec)
+ apply(drule_tac x="s2" in meta_spec)
+ apply(simp)
+ using Posix_injval
+ apply(drule_tac Posix_injval)
+ apply(subst (asm) (5) flex_fun_apply)
+ apply(simp)
+ done
+
+lemma injval_inj:
+ assumes "\<Turnstile> a : (der c r)" "\<Turnstile> v : (der c r)" "injval r c a = injval r c v"
+ shows "a = v"
+ using assms
+ apply(induct r arbitrary: a c v)
+ apply(auto)
+ using Prf_elims(1) apply blast
+ using Prf_elims(1) apply blast
+ apply(case_tac "c = x")
+ apply(auto)
+ using Prf_elims(4) apply auto[1]
+ using Prf_elims(1) apply blast
+ prefer 2
+ apply (smt Prf_elims(3) injval.simps(2) injval.simps(3) val.distinct(25) val.inject(3) val.inject(4))
+ apply(case_tac "nullable r1")
+ apply(auto)
+ apply(erule Prf_elims)
+ apply(erule Prf_elims)
+ apply(erule Prf_elims)
+ apply(erule Prf_elims)
+ apply(auto)
+ apply (metis Prf_injval_flat list.distinct(1) mkeps_flat)
+ apply(erule Prf_elims)
+ apply(erule Prf_elims)
+ apply(auto)
+ using Prf_injval_flat mkeps_flat apply fastforce
+ apply(erule Prf_elims)
+ apply(erule Prf_elims)
+ apply(auto)
+ apply(erule Prf_elims)
+ apply(erule Prf_elims)
+ apply(auto)
+ apply (smt Prf_elims(6) injval.simps(7) list.inject val.inject(5))
+ by (smt Prf_elims(6) injval.simps(7) list.inject val.inject(5))
+
+
+
+lemma uu:
+ assumes "(c # s) \<in> r \<rightarrow> injval r c v" "\<Turnstile> v : (der c r)"
+ shows "s \<in> der c r \<rightarrow> v"
+ using assms
+ apply -
+ apply(subgoal_tac "lexer r (c # s) = Some (injval r c v)")
+ prefer 2
+ using lexer_correctness(1) apply blast
+ apply(simp add: )
+ apply(case_tac "lexer (der c r) s")
+ apply(simp)
+ apply(simp)
+ apply(case_tac "s \<in> der c r \<rightarrow> a")
+ prefer 2
+ apply (simp add: lexer_correctness(1))
+ apply(subgoal_tac "\<Turnstile> a : (der c r)")
+ prefer 2
+ using Posix_Prf apply blast
+ using injval_inj by blast
+
+
+lemma Posix_flex2:
+ assumes "(s1 @ s2) \<in> r \<rightarrow> flex r id s1 v" "\<Turnstile> v : ders s1 r"
+ shows "s2 \<in> (ders s1 r) \<rightarrow> v"
+ using assms
+ apply(induct s1 arbitrary: r v s2 rule: rev_induct)
+ apply(simp)
+ apply(simp)
+ apply(drule_tac x="r" in meta_spec)
+ apply(drule_tac x="injval (ders xs r) x v" in meta_spec)
+ apply(drule_tac x="x#s2" in meta_spec)
+ apply(simp add: flex_append ders_append)
+ using Prf_injval uu by blast
+
+lemma Posix_flex3:
+ assumes "s1 \<in> r \<rightarrow> flex r id s1 v" "\<Turnstile> v : ders s1 r"
+ shows "[] \<in> (ders s1 r) \<rightarrow> v"
+ using assms
+ by (simp add: Posix_flex2)
+
+lemma flex_injval:
+ shows "flex (der a r) (injval r a) s v = injval r a (flex (der a r) id s v)"
+ by (simp add: flex_fun_apply)
+
+lemma Prf_flex:
+ assumes "\<Turnstile> v : ders s r"
+ shows "\<Turnstile> flex r id s v : r"
+ using assms
+ apply(induct s arbitrary: v r)
+ apply(simp)
+ apply(simp)
+ by (simp add: Prf_injval flex_injval)
+
+
+unused_thms
+
+end
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/thys3/LexerSimp.thy Wed Jun 29 12:38:05 2022 +0100
@@ -0,0 +1,246 @@
+theory LexerSimp
+ imports "Lexer"
+begin
+
+section {* Lexer including some simplifications *}
+
+
+fun F_RIGHT where
+ "F_RIGHT f v = Right (f v)"
+
+fun F_LEFT where
+ "F_LEFT f v = Left (f v)"
+
+fun F_ALT where
+ "F_ALT f\<^sub>1 f\<^sub>2 (Right v) = Right (f\<^sub>2 v)"
+| "F_ALT f\<^sub>1 f\<^sub>2 (Left v) = Left (f\<^sub>1 v)"
+| "F_ALT f1 f2 v = v"
+
+
+fun F_SEQ1 where
+ "F_SEQ1 f\<^sub>1 f\<^sub>2 v = Seq (f\<^sub>1 Void) (f\<^sub>2 v)"
+
+fun F_SEQ2 where
+ "F_SEQ2 f\<^sub>1 f\<^sub>2 v = Seq (f\<^sub>1 v) (f\<^sub>2 Void)"
+
+fun F_SEQ where
+ "F_SEQ f\<^sub>1 f\<^sub>2 (Seq v\<^sub>1 v\<^sub>2) = Seq (f\<^sub>1 v\<^sub>1) (f\<^sub>2 v\<^sub>2)"
+| "F_SEQ f1 f2 v = v"
+
+fun simp_ALT where
+ "simp_ALT (ZERO, f\<^sub>1) (r\<^sub>2, f\<^sub>2) = (r\<^sub>2, F_RIGHT f\<^sub>2)"
+| "simp_ALT (r\<^sub>1, f\<^sub>1) (ZERO, f\<^sub>2) = (r\<^sub>1, F_LEFT f\<^sub>1)"
+| "simp_ALT (r\<^sub>1, f\<^sub>1) (r\<^sub>2, f\<^sub>2) = (ALT r\<^sub>1 r\<^sub>2, F_ALT f\<^sub>1 f\<^sub>2)"
+
+
+fun simp_SEQ where
+ "simp_SEQ (ONE, f\<^sub>1) (r\<^sub>2, f\<^sub>2) = (r\<^sub>2, F_SEQ1 f\<^sub>1 f\<^sub>2)"
+| "simp_SEQ (r\<^sub>1, f\<^sub>1) (ONE, f\<^sub>2) = (r\<^sub>1, F_SEQ2 f\<^sub>1 f\<^sub>2)"
+| "simp_SEQ (ZERO, f\<^sub>1) (r\<^sub>2, f\<^sub>2) = (ZERO, undefined)"
+| "simp_SEQ (r\<^sub>1, f\<^sub>1) (ZERO, f\<^sub>2) = (ZERO, undefined)"
+| "simp_SEQ (r\<^sub>1, f\<^sub>1) (r\<^sub>2, f\<^sub>2) = (SEQ r\<^sub>1 r\<^sub>2, F_SEQ f\<^sub>1 f\<^sub>2)"
+
+lemma simp_SEQ_simps[simp]:
+ "simp_SEQ p1 p2 = (if (fst p1 = ONE) then (fst p2, F_SEQ1 (snd p1) (snd p2))
+ else (if (fst p2 = ONE) then (fst p1, F_SEQ2 (snd p1) (snd p2))
+ else (if (fst p1 = ZERO) then (ZERO, undefined)
+ else (if (fst p2 = ZERO) then (ZERO, undefined)
+ else (SEQ (fst p1) (fst p2), F_SEQ (snd p1) (snd p2))))))"
+by (induct p1 p2 rule: simp_SEQ.induct) (auto)
+
+lemma simp_ALT_simps[simp]:
+ "simp_ALT p1 p2 = (if (fst p1 = ZERO) then (fst p2, F_RIGHT (snd p2))
+ else (if (fst p2 = ZERO) then (fst p1, F_LEFT (snd p1))
+ else (ALT (fst p1) (fst p2), F_ALT (snd p1) (snd p2))))"
+by (induct p1 p2 rule: simp_ALT.induct) (auto)
+
+fun
+ simp :: "rexp \<Rightarrow> rexp * (val \<Rightarrow> val)"
+where
+ "simp (ALT r1 r2) = simp_ALT (simp r1) (simp r2)"
+| "simp (SEQ r1 r2) = simp_SEQ (simp r1) (simp r2)"
+| "simp r = (r, id)"
+
+fun
+ slexer :: "rexp \<Rightarrow> string \<Rightarrow> val option"
+where
+ "slexer r [] = (if nullable r then Some(mkeps r) else None)"
+| "slexer r (c#s) = (let (rs, fr) = simp (der c r) in
+ (case (slexer rs s) of
+ None \<Rightarrow> None
+ | Some(v) \<Rightarrow> Some(injval r c (fr v))))"
+
+
+lemma slexer_better_simp:
+ "slexer r (c#s) = (case (slexer (fst (simp (der c r))) s) of
+ None \<Rightarrow> None
+ | Some(v) \<Rightarrow> Some(injval r c ((snd (simp (der c r))) v)))"
+by (auto split: prod.split option.split)
+
+
+lemma L_fst_simp:
+ shows "L(r) = L(fst (simp r))"
+by (induct r) (auto)
+
+lemma Posix_simp:
+ assumes "s \<in> (fst (simp r)) \<rightarrow> v"
+ shows "s \<in> r \<rightarrow> ((snd (simp r)) v)"
+using assms
+proof(induct r arbitrary: s v rule: rexp.induct)
+ case (ALT r1 r2 s v)
+ have IH1: "\<And>s v. s \<in> fst (simp r1) \<rightarrow> v \<Longrightarrow> s \<in> r1 \<rightarrow> snd (simp r1) v" by fact
+ have IH2: "\<And>s v. s \<in> fst (simp r2) \<rightarrow> v \<Longrightarrow> s \<in> r2 \<rightarrow> snd (simp r2) v" by fact
+ have as: "s \<in> fst (simp (ALT r1 r2)) \<rightarrow> v" by fact
+ consider (ZERO_ZERO) "fst (simp r1) = ZERO" "fst (simp r2) = ZERO"
+ | (ZERO_NZERO) "fst (simp r1) = ZERO" "fst (simp r2) \<noteq> ZERO"
+ | (NZERO_ZERO) "fst (simp r1) \<noteq> ZERO" "fst (simp r2) = ZERO"
+ | (NZERO_NZERO) "fst (simp r1) \<noteq> ZERO" "fst (simp r2) \<noteq> ZERO" by auto
+ then show "s \<in> ALT r1 r2 \<rightarrow> snd (simp (ALT r1 r2)) v"
+ proof(cases)
+ case (ZERO_ZERO)
+ with as have "s \<in> ZERO \<rightarrow> v" by simp
+ then show "s \<in> ALT r1 r2 \<rightarrow> snd (simp (ALT r1 r2)) v" by (rule Posix_elims(1))
+ next
+ case (ZERO_NZERO)
+ with as have "s \<in> fst (simp r2) \<rightarrow> v" by simp
+ with IH2 have "s \<in> r2 \<rightarrow> snd (simp r2) v" by simp
+ moreover
+ from ZERO_NZERO have "fst (simp r1) = ZERO" by simp
+ then have "L (fst (simp r1)) = {}" by simp
+ then have "L r1 = {}" using L_fst_simp by simp
+ then have "s \<notin> L r1" by simp
+ ultimately have "s \<in> ALT r1 r2 \<rightarrow> Right (snd (simp r2) v)" by (rule Posix_ALT2)
+ then show "s \<in> ALT r1 r2 \<rightarrow> snd (simp (ALT r1 r2)) v"
+ using ZERO_NZERO by simp
+ next
+ case (NZERO_ZERO)
+ with as have "s \<in> fst (simp r1) \<rightarrow> v" by simp
+ with IH1 have "s \<in> r1 \<rightarrow> snd (simp r1) v" by simp
+ then have "s \<in> ALT r1 r2 \<rightarrow> Left (snd (simp r1) v)" by (rule Posix_ALT1)
+ then show "s \<in> ALT r1 r2 \<rightarrow> snd (simp (ALT r1 r2)) v" using NZERO_ZERO by simp
+ next
+ case (NZERO_NZERO)
+ with as have "s \<in> ALT (fst (simp r1)) (fst (simp r2)) \<rightarrow> v" by simp
+ then consider (Left) v1 where "v = Left v1" "s \<in> (fst (simp r1)) \<rightarrow> v1"
+ | (Right) v2 where "v = Right v2" "s \<in> (fst (simp r2)) \<rightarrow> v2" "s \<notin> L (fst (simp r1))"
+ by (erule_tac Posix_elims(4))
+ then show "s \<in> ALT r1 r2 \<rightarrow> snd (simp (ALT r1 r2)) v"
+ proof(cases)
+ case (Left)
+ then have "v = Left v1" "s \<in> r1 \<rightarrow> (snd (simp r1) v1)" using IH1 by simp_all
+ then show "s \<in> ALT r1 r2 \<rightarrow> snd (simp (ALT r1 r2)) v" using NZERO_NZERO
+ by (simp_all add: Posix_ALT1)
+ next
+ case (Right)
+ then have "v = Right v2" "s \<in> r2 \<rightarrow> (snd (simp r2) v2)" "s \<notin> L r1" using IH2 L_fst_simp by simp_all
+ then show "s \<in> ALT r1 r2 \<rightarrow> snd (simp (ALT r1 r2)) v" using NZERO_NZERO
+ by (simp_all add: Posix_ALT2)
+ qed
+ qed
+next
+ case (SEQ r1 r2 s v)
+ have IH1: "\<And>s v. s \<in> fst (simp r1) \<rightarrow> v \<Longrightarrow> s \<in> r1 \<rightarrow> snd (simp r1) v" by fact
+ have IH2: "\<And>s v. s \<in> fst (simp r2) \<rightarrow> v \<Longrightarrow> s \<in> r2 \<rightarrow> snd (simp r2) v" by fact
+ have as: "s \<in> fst (simp (SEQ r1 r2)) \<rightarrow> v" by fact
+ consider (ONE_ONE) "fst (simp r1) = ONE" "fst (simp r2) = ONE"
+ | (ONE_NONE) "fst (simp r1) = ONE" "fst (simp r2) \<noteq> ONE"
+ | (NONE_ONE) "fst (simp r1) \<noteq> ONE" "fst (simp r2) = ONE"
+ | (NONE_NONE) "fst (simp r1) \<noteq> ONE" "fst (simp r2) \<noteq> ONE"
+ by auto
+ then show "s \<in> SEQ r1 r2 \<rightarrow> snd (simp (SEQ r1 r2)) v"
+ proof(cases)
+ case (ONE_ONE)
+ with as have b: "s \<in> ONE \<rightarrow> v" by simp
+ from b have "s \<in> r1 \<rightarrow> snd (simp r1) v" using IH1 ONE_ONE by simp
+ moreover
+ from b have c: "s = []" "v = Void" using Posix_elims(2) by auto
+ moreover
+ have "[] \<in> ONE \<rightarrow> Void" by (simp add: Posix_ONE)
+ then have "[] \<in> fst (simp r2) \<rightarrow> Void" using ONE_ONE by simp
+ then have "[] \<in> r2 \<rightarrow> snd (simp r2) Void" using IH2 by simp
+ ultimately have "([] @ []) \<in> SEQ r1 r2 \<rightarrow> Seq (snd (simp r1) Void) (snd (simp r2) Void)"
+ using Posix_SEQ by blast
+ then show "s \<in> SEQ r1 r2 \<rightarrow> snd (simp (SEQ r1 r2)) v" using c ONE_ONE by simp
+ next
+ case (ONE_NONE)
+ with as have b: "s \<in> fst (simp r2) \<rightarrow> v" by simp
+ from b have "s \<in> r2 \<rightarrow> snd (simp r2) v" using IH2 ONE_NONE by simp
+ moreover
+ have "[] \<in> ONE \<rightarrow> Void" by (simp add: Posix_ONE)
+ then have "[] \<in> fst (simp r1) \<rightarrow> Void" using ONE_NONE by simp
+ then have "[] \<in> r1 \<rightarrow> snd (simp r1) Void" using IH1 by simp
+ moreover
+ from ONE_NONE(1) have "L (fst (simp r1)) = {[]}" by simp
+ then have "L r1 = {[]}" by (simp add: L_fst_simp[symmetric])
+ ultimately have "([] @ s) \<in> SEQ r1 r2 \<rightarrow> Seq (snd (simp r1) Void) (snd (simp r2) v)"
+ by(rule_tac Posix_SEQ) auto
+ then show "s \<in> SEQ r1 r2 \<rightarrow> snd (simp (SEQ r1 r2)) v" using ONE_NONE by simp
+ next
+ case (NONE_ONE)
+ with as have "s \<in> fst (simp r1) \<rightarrow> v" by simp
+ with IH1 have "s \<in> r1 \<rightarrow> snd (simp r1) v" by simp
+ moreover
+ have "[] \<in> ONE \<rightarrow> Void" by (simp add: Posix_ONE)
+ then have "[] \<in> fst (simp r2) \<rightarrow> Void" using NONE_ONE by simp
+ then have "[] \<in> r2 \<rightarrow> snd (simp r2) Void" using IH2 by simp
+ ultimately have "(s @ []) \<in> SEQ r1 r2 \<rightarrow> Seq (snd (simp r1) v) (snd (simp r2) Void)"
+ by(rule_tac Posix_SEQ) auto
+ then show "s \<in> SEQ r1 r2 \<rightarrow> snd (simp (SEQ r1 r2)) v" using NONE_ONE by simp
+ next
+ case (NONE_NONE)
+ from as have 00: "fst (simp r1) \<noteq> ZERO" "fst (simp r2) \<noteq> ZERO"
+ apply(auto)
+ apply(smt Posix_elims(1) fst_conv)
+ by (smt NONE_NONE(2) Posix_elims(1) fstI)
+ with NONE_NONE as have "s \<in> SEQ (fst (simp r1)) (fst (simp r2)) \<rightarrow> v" by simp
+ then obtain s1 s2 v1 v2 where eqs: "s = s1 @ s2" "v = Seq v1 v2"
+ "s1 \<in> (fst (simp r1)) \<rightarrow> v1" "s2 \<in> (fst (simp r2)) \<rightarrow> v2"
+ "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L r1 \<and> s\<^sub>4 \<in> L r2)"
+ by (erule_tac Posix_elims(5)) (auto simp add: L_fst_simp[symmetric])
+ then have "s1 \<in> r1 \<rightarrow> (snd (simp r1) v1)" "s2 \<in> r2 \<rightarrow> (snd (simp r2) v2)"
+ using IH1 IH2 by auto
+ then show "s \<in> SEQ r1 r2 \<rightarrow> snd (simp (SEQ r1 r2)) v" using eqs NONE_NONE 00
+ by(auto intro: Posix_SEQ)
+ qed
+qed (simp_all)
+
+
+lemma slexer_correctness:
+ shows "slexer r s = lexer r s"
+proof(induct s arbitrary: r)
+ case Nil
+ show "slexer r [] = lexer r []" by simp
+next
+ case (Cons c s r)
+ have IH: "\<And>r. slexer r s = lexer r s" by fact
+ show "slexer r (c # s) = lexer r (c # s)"
+ proof (cases "s \<in> L (der c r)")
+ case True
+ assume a1: "s \<in> L (der c r)"
+ then obtain v1 where a2: "lexer (der c r) s = Some v1" "s \<in> der c r \<rightarrow> v1"
+ using lexer_correct_Some by auto
+ from a1 have "s \<in> L (fst (simp (der c r)))" using L_fst_simp[symmetric] by simp
+ then obtain v2 where a3: "lexer (fst (simp (der c r))) s = Some v2" "s \<in> (fst (simp (der c r))) \<rightarrow> v2"
+ using lexer_correct_Some by auto
+ then have a4: "slexer (fst (simp (der c r))) s = Some v2" using IH by simp
+ from a3(2) have "s \<in> der c r \<rightarrow> (snd (simp (der c r))) v2" using Posix_simp by simp
+ with a2(2) have "v1 = (snd (simp (der c r))) v2" using Posix_determ by simp
+ with a2(1) a4 show "slexer r (c # s) = lexer r (c # s)" by (auto split: prod.split)
+ next
+ case False
+ assume b1: "s \<notin> L (der c r)"
+ then have "lexer (der c r) s = None" using lexer_correct_None by simp
+ moreover
+ from b1 have "s \<notin> L (fst (simp (der c r)))" using L_fst_simp[symmetric] by simp
+ then have "lexer (fst (simp (der c r))) s = None" using lexer_correct_None by simp
+ then have "slexer (fst (simp (der c r))) s = None" using IH by simp
+ ultimately show "slexer r (c # s) = lexer r (c # s)"
+ by (simp del: slexer.simps add: slexer_better_simp)
+ qed
+ qed
+
+
+unused_thms
+
+
+end
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/thys3/PDerivs.thy Wed Jun 29 12:38:05 2022 +0100
@@ -0,0 +1,603 @@
+
+theory PDerivs
+ imports PosixSpec
+begin
+
+
+
+abbreviation
+ "SEQs rs r \<equiv> (\<Union>r' \<in> rs. {SEQ r' r})"
+
+lemma SEQs_eq_image:
+ "SEQs rs r = (\<lambda>r'. SEQ r' r) ` rs"
+ by auto
+
+fun
+ pder :: "char \<Rightarrow> rexp \<Rightarrow> rexp set"
+where
+ "pder c ZERO = {}"
+| "pder c ONE = {}"
+| "pder c (CH d) = (if c = d then {ONE} else {})"
+| "pder c (ALT r1 r2) = (pder c r1) \<union> (pder c r2)"
+| "pder c (SEQ r1 r2) =
+ (if nullable r1 then SEQs (pder c r1) r2 \<union> pder c r2 else SEQs (pder c r1) r2)"
+| "pder c (STAR r) = SEQs (pder c r) (STAR r)"
+
+fun
+ pders :: "char list \<Rightarrow> rexp \<Rightarrow> rexp set"
+where
+ "pders [] r = {r}"
+| "pders (c # s) r = \<Union> (pders s ` pder c r)"
+
+abbreviation
+ pder_set :: "char \<Rightarrow> rexp set \<Rightarrow> rexp set"
+where
+ "pder_set c rs \<equiv> \<Union> (pder c ` rs)"
+
+abbreviation
+ pders_set :: "char list \<Rightarrow> rexp set \<Rightarrow> rexp set"
+where
+ "pders_set s rs \<equiv> \<Union> (pders s ` rs)"
+
+lemma pders_append:
+ "pders (s1 @ s2) r = \<Union> (pders s2 ` pders s1 r)"
+by (induct s1 arbitrary: r) (simp_all)
+
+lemma pders_snoc:
+ shows "pders (s @ [c]) r = pder_set c (pders s r)"
+by (simp add: pders_append)
+
+lemma pders_simps [simp]:
+ shows "pders s ZERO = (if s = [] then {ZERO} else {})"
+ and "pders s ONE = (if s = [] then {ONE} else {})"
+ and "pders s (ALT r1 r2) = (if s = [] then {ALT r1 r2} else (pders s r1) \<union> (pders s r2))"
+by (induct s) (simp_all)
+
+lemma pders_CHAR:
+ shows "pders s (CH c) \<subseteq> {CH c, ONE}"
+by (induct s) (simp_all)
+
+subsection \<open>Relating left-quotients and partial derivatives\<close>
+
+lemma Sequ_UNION_distrib:
+shows "A ;; \<Union>(M ` I) = \<Union>((\<lambda>i. A ;; M i) ` I)"
+and "\<Union>(M ` I) ;; A = \<Union>((\<lambda>i. M i ;; A) ` I)"
+by (auto simp add: Sequ_def)
+
+
+lemma Der_pder:
+ shows "Der c (L r) = \<Union> (L ` pder c r)"
+by (induct r) (simp_all add: nullable_correctness Sequ_UNION_distrib)
+
+lemma Ders_pders:
+ shows "Ders s (L r) = \<Union> (L ` pders s r)"
+proof (induct s arbitrary: r)
+ case (Cons c s)
+ have ih: "\<And>r. Ders s (L r) = \<Union> (L ` pders s r)" by fact
+ have "Ders (c # s) (L r) = Ders s (Der c (L r))" by (simp add: Ders_def Der_def)
+ also have "\<dots> = Ders s (\<Union> (L ` pder c r))" by (simp add: Der_pder)
+ also have "\<dots> = (\<Union>A\<in>(L ` (pder c r)). (Ders s A))"
+ by (auto simp add: Ders_def)
+ also have "\<dots> = \<Union> (L ` (pders_set s (pder c r)))"
+ using ih by auto
+ also have "\<dots> = \<Union> (L ` (pders (c # s) r))" by simp
+ finally show "Ders (c # s) (L r) = \<Union> (L ` pders (c # s) r)" .
+qed (simp add: Ders_def)
+
+subsection \<open>Relating derivatives and partial derivatives\<close>
+
+lemma der_pder:
+ shows "\<Union> (L ` (pder c r)) = L (der c r)"
+unfolding der_correctness Der_pder by simp
+
+lemma ders_pders:
+ shows "\<Union> (L ` (pders s r)) = L (ders s r)"
+unfolding der_correctness ders_correctness Ders_pders by simp
+
+
+subsection \<open>Finiteness property of partial derivatives\<close>
+
+definition
+ pders_Set :: "string set \<Rightarrow> rexp \<Rightarrow> rexp set"
+where
+ "pders_Set A r \<equiv> \<Union>x \<in> A. pders x r"
+
+lemma pders_Set_subsetI:
+ assumes "\<And>s. s \<in> A \<Longrightarrow> pders s r \<subseteq> C"
+ shows "pders_Set A r \<subseteq> C"
+using assms unfolding pders_Set_def by (rule UN_least)
+
+lemma pders_Set_union:
+ shows "pders_Set (A \<union> B) r = (pders_Set A r \<union> pders_Set B r)"
+by (simp add: pders_Set_def)
+
+lemma pders_Set_subset:
+ shows "A \<subseteq> B \<Longrightarrow> pders_Set A r \<subseteq> pders_Set B r"
+by (auto simp add: pders_Set_def)
+
+definition
+ "UNIV1 \<equiv> UNIV - {[]}"
+
+lemma pders_Set_ZERO [simp]:
+ shows "pders_Set UNIV1 ZERO = {}"
+unfolding UNIV1_def pders_Set_def by auto
+
+lemma pders_Set_ONE [simp]:
+ shows "pders_Set UNIV1 ONE = {}"
+unfolding UNIV1_def pders_Set_def by (auto split: if_splits)
+
+lemma pders_Set_CHAR [simp]:
+ shows "pders_Set UNIV1 (CH c) = {ONE}"
+unfolding UNIV1_def pders_Set_def
+apply(auto)
+apply(frule rev_subsetD)
+apply(rule pders_CHAR)
+apply(simp)
+apply(case_tac xa)
+apply(auto split: if_splits)
+done
+
+lemma pders_Set_ALT [simp]:
+ shows "pders_Set UNIV1 (ALT r1 r2) = pders_Set UNIV1 r1 \<union> pders_Set UNIV1 r2"
+unfolding UNIV1_def pders_Set_def by auto
+
+
+text \<open>Non-empty suffixes of a string (needed for the cases of @{const SEQ} and @{const STAR} below)\<close>
+
+definition
+ "PSuf s \<equiv> {v. v \<noteq> [] \<and> (\<exists>u. u @ v = s)}"
+
+lemma PSuf_snoc:
+ shows "PSuf (s @ [c]) = (PSuf s) ;; {[c]} \<union> {[c]}"
+unfolding PSuf_def Sequ_def
+by (auto simp add: append_eq_append_conv2 append_eq_Cons_conv)
+
+lemma PSuf_Union:
+ shows "(\<Union>v \<in> PSuf s ;; {[c]}. f v) = (\<Union>v \<in> PSuf s. f (v @ [c]))"
+by (auto simp add: Sequ_def)
+
+lemma pders_Set_snoc:
+ shows "pders_Set (PSuf s ;; {[c]}) r = (pder_set c (pders_Set (PSuf s) r))"
+unfolding pders_Set_def
+by (simp add: PSuf_Union pders_snoc)
+
+lemma pders_SEQ:
+ shows "pders s (SEQ r1 r2) \<subseteq> SEQs (pders s r1) r2 \<union> (pders_Set (PSuf s) r2)"
+proof (induct s rule: rev_induct)
+ case (snoc c s)
+ have ih: "pders s (SEQ r1 r2) \<subseteq> SEQs (pders s r1) r2 \<union> (pders_Set (PSuf s) r2)"
+ by fact
+ have "pders (s @ [c]) (SEQ r1 r2) = pder_set c (pders s (SEQ r1 r2))"
+ by (simp add: pders_snoc)
+ also have "\<dots> \<subseteq> pder_set c (SEQs (pders s r1) r2 \<union> (pders_Set (PSuf s) r2))"
+ using ih by fastforce
+ also have "\<dots> = pder_set c (SEQs (pders s r1) r2) \<union> pder_set c (pders_Set (PSuf s) r2)"
+ by (simp)
+ also have "\<dots> = pder_set c (SEQs (pders s r1) r2) \<union> pders_Set (PSuf s ;; {[c]}) r2"
+ by (simp add: pders_Set_snoc)
+ also
+ have "\<dots> \<subseteq> pder_set c (SEQs (pders s r1) r2) \<union> pder c r2 \<union> pders_Set (PSuf s ;; {[c]}) r2"
+ by auto
+ also
+ have "\<dots> \<subseteq> SEQs (pder_set c (pders s r1)) r2 \<union> pder c r2 \<union> pders_Set (PSuf s ;; {[c]}) r2"
+ by (auto simp add: if_splits)
+ also have "\<dots> = SEQs (pders (s @ [c]) r1) r2 \<union> pder c r2 \<union> pders_Set (PSuf s ;; {[c]}) r2"
+ by (simp add: pders_snoc)
+ also have "\<dots> \<subseteq> SEQs (pders (s @ [c]) r1) r2 \<union> pders_Set (PSuf (s @ [c])) r2"
+ unfolding pders_Set_def by (auto simp add: PSuf_snoc)
+ finally show ?case .
+qed (simp)
+
+lemma pders_Set_SEQ_aux1:
+ assumes a: "s \<in> UNIV1"
+ shows "pders_Set (PSuf s) r \<subseteq> pders_Set UNIV1 r"
+using a unfolding UNIV1_def PSuf_def pders_Set_def by auto
+
+lemma pders_Set_SEQ_aux2:
+ assumes a: "s \<in> UNIV1"
+ shows "SEQs (pders s r1) r2 \<subseteq> SEQs (pders_Set UNIV1 r1) r2"
+using a unfolding pders_Set_def by auto
+
+lemma pders_Set_SEQ:
+ shows "pders_Set UNIV1 (SEQ r1 r2) \<subseteq> SEQs (pders_Set UNIV1 r1) r2 \<union> pders_Set UNIV1 r2"
+apply(rule pders_Set_subsetI)
+apply(rule subset_trans)
+apply(rule pders_SEQ)
+using pders_Set_SEQ_aux1 pders_Set_SEQ_aux2
+apply auto
+apply blast
+done
+
+lemma pders_STAR:
+ assumes a: "s \<noteq> []"
+ shows "pders s (STAR r) \<subseteq> SEQs (pders_Set (PSuf s) r) (STAR r)"
+using a
+proof (induct s rule: rev_induct)
+ case (snoc c s)
+ have ih: "s \<noteq> [] \<Longrightarrow> pders s (STAR r) \<subseteq> SEQs (pders_Set (PSuf s) r) (STAR r)" by fact
+ { assume asm: "s \<noteq> []"
+ have "pders (s @ [c]) (STAR r) = pder_set c (pders s (STAR r))" by (simp add: pders_snoc)
+ also have "\<dots> \<subseteq> pder_set c (SEQs (pders_Set (PSuf s) r) (STAR r))"
+ using ih[OF asm] by fast
+ also have "\<dots> \<subseteq> SEQs (pder_set c (pders_Set (PSuf s) r)) (STAR r) \<union> pder c (STAR r)"
+ by (auto split: if_splits)
+ also have "\<dots> \<subseteq> SEQs (pders_Set (PSuf (s @ [c])) r) (STAR r) \<union> (SEQs (pder c r) (STAR r))"
+ by (simp only: PSuf_snoc pders_Set_snoc pders_Set_union)
+ (auto simp add: pders_Set_def)
+ also have "\<dots> = SEQs (pders_Set (PSuf (s @ [c])) r) (STAR r)"
+ by (auto simp add: PSuf_snoc PSuf_Union pders_snoc pders_Set_def)
+ finally have ?case .
+ }
+ moreover
+ { assume asm: "s = []"
+ then have ?case by (auto simp add: pders_Set_def pders_snoc PSuf_def)
+ }
+ ultimately show ?case by blast
+qed (simp)
+
+lemma pders_Set_STAR:
+ shows "pders_Set UNIV1 (STAR r) \<subseteq> SEQs (pders_Set UNIV1 r) (STAR r)"
+apply(rule pders_Set_subsetI)
+apply(rule subset_trans)
+apply(rule pders_STAR)
+apply(simp add: UNIV1_def)
+apply(simp add: UNIV1_def PSuf_def)
+apply(auto simp add: pders_Set_def)
+done
+
+lemma finite_SEQs [simp]:
+ assumes a: "finite A"
+ shows "finite (SEQs A r)"
+using a by auto
+
+
+lemma finite_pders_Set_UNIV1:
+ shows "finite (pders_Set UNIV1 r)"
+apply(induct r)
+apply(simp_all add:
+ finite_subset[OF pders_Set_SEQ]
+ finite_subset[OF pders_Set_STAR])
+done
+
+lemma pders_Set_UNIV:
+ shows "pders_Set UNIV r = pders [] r \<union> pders_Set UNIV1 r"
+unfolding UNIV1_def pders_Set_def
+by blast
+
+lemma finite_pders_Set_UNIV:
+ shows "finite (pders_Set UNIV r)"
+unfolding pders_Set_UNIV
+by (simp add: finite_pders_Set_UNIV1)
+
+lemma finite_pders_set:
+ shows "finite (pders_Set A r)"
+by (metis finite_pders_Set_UNIV pders_Set_subset rev_finite_subset subset_UNIV)
+
+
+text \<open>The following relationship between the alphabetic width of regular expressions
+(called \<open>awidth\<close> below) and the number of partial derivatives was proved
+by Antimirov~\cite{Antimirov95} and formalized by Max Haslbeck.\<close>
+
+fun awidth :: "rexp \<Rightarrow> nat" where
+"awidth ZERO = 0" |
+"awidth ONE = 0" |
+"awidth (CH a) = 1" |
+"awidth (ALT r1 r2) = awidth r1 + awidth r2" |
+"awidth (SEQ r1 r2) = awidth r1 + awidth r2" |
+"awidth (STAR r1) = awidth r1"
+
+lemma card_SEQs_pders_Set_le:
+ shows "card (SEQs (pders_Set A r) s) \<le> card (pders_Set A r)"
+ using finite_pders_set
+ unfolding SEQs_eq_image
+ by (rule card_image_le)
+
+lemma card_pders_set_UNIV1_le_awidth:
+ shows "card (pders_Set UNIV1 r) \<le> awidth r"
+proof (induction r)
+ case (ALT r1 r2)
+ have "card (pders_Set UNIV1 (ALT r1 r2)) = card (pders_Set UNIV1 r1 \<union> pders_Set UNIV1 r2)" by simp
+ also have "\<dots> \<le> card (pders_Set UNIV1 r1) + card (pders_Set UNIV1 r2)"
+ by(simp add: card_Un_le)
+ also have "\<dots> \<le> awidth (ALT r1 r2)" using ALT.IH by simp
+ finally show ?case .
+next
+ case (SEQ r1 r2)
+ have "card (pders_Set UNIV1 (SEQ r1 r2)) \<le> card (SEQs (pders_Set UNIV1 r1) r2 \<union> pders_Set UNIV1 r2)"
+ by (simp add: card_mono finite_pders_set pders_Set_SEQ)
+ also have "\<dots> \<le> card (SEQs (pders_Set UNIV1 r1) r2) + card (pders_Set UNIV1 r2)"
+ by (simp add: card_Un_le)
+ also have "\<dots> \<le> card (pders_Set UNIV1 r1) + card (pders_Set UNIV1 r2)"
+ by (simp add: card_SEQs_pders_Set_le)
+ also have "\<dots> \<le> awidth (SEQ r1 r2)" using SEQ.IH by simp
+ finally show ?case .
+next
+ case (STAR r)
+ have "card (pders_Set UNIV1 (STAR r)) \<le> card (SEQs (pders_Set UNIV1 r) (STAR r))"
+ by (simp add: card_mono finite_pders_set pders_Set_STAR)
+ also have "\<dots> \<le> card (pders_Set UNIV1 r)" by (rule card_SEQs_pders_Set_le)
+ also have "\<dots> \<le> awidth (STAR r)" by (simp add: STAR.IH)
+ finally show ?case .
+qed (auto)
+
+text\<open>Antimirov's Theorem 3.4:\<close>
+
+theorem card_pders_set_UNIV_le_awidth:
+ shows "card (pders_Set UNIV r) \<le> awidth r + 1"
+proof -
+ have "card (insert r (pders_Set UNIV1 r)) \<le> Suc (card (pders_Set UNIV1 r))"
+ by(auto simp: card_insert_if[OF finite_pders_Set_UNIV1])
+ also have "\<dots> \<le> Suc (awidth r)" by(simp add: card_pders_set_UNIV1_le_awidth)
+ finally show ?thesis by(simp add: pders_Set_UNIV)
+qed
+
+text\<open>Antimirov's Corollary 3.5:\<close>
+(*W stands for word set*)
+corollary card_pders_set_le_awidth:
+ shows "card (pders_Set W r) \<le> awidth r + 1"
+proof -
+ have "card (pders_Set W r) \<le> card (pders_Set UNIV r)"
+ by (simp add: card_mono finite_pders_set pders_Set_subset)
+ also have "... \<le> awidth r + 1"
+ by (rule card_pders_set_UNIV_le_awidth)
+ finally show "card (pders_Set W r) \<le> awidth r + 1" by simp
+qed
+
+(* other result by antimirov *)
+
+lemma card_pders_awidth:
+ shows "card (pders s r) \<le> awidth r + 1"
+proof -
+ have "pders s r \<subseteq> pders_Set UNIV r"
+ using pders_Set_def by auto
+ then have "card (pders s r) \<le> card (pders_Set UNIV r)"
+ by (simp add: card_mono finite_pders_set)
+ then show "card (pders s r) \<le> awidth r + 1"
+ using card_pders_set_le_awidth order_trans by blast
+qed
+
+
+
+
+
+fun subs :: "rexp \<Rightarrow> rexp set" where
+"subs ZERO = {ZERO}" |
+"subs ONE = {ONE}" |
+"subs (CH a) = {CH a, ONE}" |
+"subs (ALT r1 r2) = (subs r1 \<union> subs r2 \<union> {ALT r1 r2})" |
+"subs (SEQ r1 r2) = (subs r1 \<union> subs r2 \<union> {SEQ r1 r2} \<union> SEQs (subs r1) r2)" |
+"subs (STAR r1) = (subs r1 \<union> {STAR r1} \<union> SEQs (subs r1) (STAR r1))"
+
+lemma subs_finite:
+ shows "finite (subs r)"
+ apply(induct r)
+ apply(simp_all)
+ done
+
+
+
+lemma pders_subs:
+ shows "pders s r \<subseteq> subs r"
+ apply(induct r arbitrary: s)
+ 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
+(* STAR case *)
+ apply(case_tac s)
+ apply(simp)
+ apply(rule subset_trans)
+ thm pders_STAR
+ apply(rule pders_STAR)
+ apply(simp)
+ apply(auto simp add: pders_Set_def)[1]
+ apply(simp)
+ apply(rule conjI)
+ apply blast
+apply(auto simp add: pders_Set_def)[1]
+ done
+
+fun size2 :: "rexp \<Rightarrow> nat" where
+ "size2 ZERO = 1" |
+ "size2 ONE = 1" |
+ "size2 (CH c) = 1" |
+ "size2 (ALT r1 r2) = Suc (size2 r1 + size2 r2)" |
+ "size2 (SEQ r1 r2) = Suc (size2 r1 + size2 r2)" |
+ "size2 (STAR r1) = Suc (size2 r1)"
+
+
+lemma size_rexp:
+ fixes r :: rexp
+ shows "1 \<le> size2 r"
+ apply(induct r)
+ apply(simp)
+ apply(simp_all)
+ done
+
+lemma subs_size2:
+ shows "\<forall>r1 \<in> subs r. size2 r1 \<le> Suc (size2 r * size2 r)"
+ apply(induct r)
+ 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)
+ apply(rule le_trans)
+ apply(assumption)
+ apply(simp)
+ using size_rexp
+ apply(simp)
+ done
+
+lemma awidth_size:
+ shows "awidth r \<le> size2 r"
+ apply(induct r)
+ apply(simp_all)
+ done
+
+lemma Sum1:
+ fixes A B :: "nat set"
+ assumes "A \<subseteq> B" "finite A" "finite B"
+ shows "\<Sum>A \<le> \<Sum>B"
+ using assms
+ by (simp add: sum_mono2)
+
+lemma Sum2:
+ fixes A :: "rexp set"
+ and f g :: "rexp \<Rightarrow> nat"
+ assumes "finite A" "\<forall>x \<in> A. f x \<le> g x"
+ shows "sum f A \<le> sum g A"
+ using assms
+ apply(induct A)
+ apply(auto)
+ done
+
+
+
+
+
+lemma pders_max_size:
+ shows "(sum size2 (pders s r)) \<le> (Suc (size2 r)) ^ 3"
+proof -
+ have "(sum size2 (pders s r)) \<le> sum (\<lambda>_. Suc (size2 r * size2 r)) (pders s r)"
+ apply(rule_tac Sum2)
+ apply (meson pders_subs rev_finite_subset subs_finite)
+ using pders_subs subs_size2 by blast
+ also have "... \<le> (Suc (size2 r * size2 r)) * (sum (\<lambda>_. 1) (pders s r))"
+ by simp
+ also have "... \<le> (Suc (size2 r * size2 r)) * card (pders s r)"
+ by simp
+ also have "... \<le> (Suc (size2 r * size2 r)) * (Suc (awidth r))"
+ using Suc_eq_plus1 card_pders_awidth mult_le_mono2 by presburger
+ also have "... \<le> (Suc (size2 r * size2 r)) * (Suc (size2 r))"
+ using Suc_le_mono awidth_size mult_le_mono2 by presburger
+ also have "... \<le> (Suc (size2 r)) ^ 3"
+ by (smt One_nat_def Suc_1 Suc_mult_le_cancel1 Suc_n_not_le_n antisym_conv le_Suc_eq mult.commute nat_le_linear numeral_3_eq_3 power2_eq_square power2_le_imp_le power_Suc size_rexp)
+ finally show ?thesis .
+qed
+
+lemma pders_Set_max_size:
+ shows "(sum size2 (pders_Set A r)) \<le> (Suc (size2 r)) ^ 3"
+proof -
+ have "(sum size2 (pders_Set A r)) \<le> sum (\<lambda>_. Suc (size2 r * size2 r)) (pders_Set A r)"
+ apply(rule_tac Sum2)
+ apply (simp add: finite_pders_set)
+ by (meson pders_Set_subsetI pders_subs subs_size2 subsetD)
+ also have "... \<le> (Suc (size2 r * size2 r)) * (sum (\<lambda>_. 1) (pders_Set A r))"
+ by simp
+ also have "... \<le> (Suc (size2 r * size2 r)) * card (pders_Set A r)"
+ by simp
+ also have "... \<le> (Suc (size2 r * size2 r)) * (Suc (awidth r))"
+ using Suc_eq_plus1 card_pders_set_le_awidth mult_le_mono2 by presburger
+ also have "... \<le> (Suc (size2 r * size2 r)) * (Suc (size2 r))"
+ using Suc_le_mono awidth_size mult_le_mono2 by presburger
+ also have "... \<le> (Suc (size2 r)) ^ 3"
+ by (smt One_nat_def Suc_1 Suc_mult_le_cancel1 Suc_n_not_le_n antisym_conv le_Suc_eq mult.commute nat_le_linear numeral_3_eq_3 power2_eq_square power2_le_imp_le power_Suc size_rexp)
+ finally show ?thesis .
+qed
+
+fun height :: "rexp \<Rightarrow> nat" where
+ "height ZERO = 1" |
+ "height ONE = 1" |
+ "height (CH c) = 1" |
+ "height (ALT r1 r2) = Suc (max (height r1) (height r2))" |
+ "height (SEQ r1 r2) = Suc (max (height r1) (height r2))" |
+ "height (STAR r1) = Suc (height r1)"
+
+lemma height_size2:
+ shows "height r \<le> size2 r"
+ apply(induct r)
+ apply(simp_all)
+ done
+
+lemma height_rexp:
+ fixes r :: rexp
+ shows "1 \<le> height r"
+ apply(induct r)
+ apply(simp_all)
+ done
+
+lemma subs_height:
+ shows "\<forall>r1 \<in> subs r. height r1 \<le> Suc (height r)"
+ apply(induct r)
+ apply(auto)+
+ done
+
+fun lin_concat :: "(char \<times> rexp) \<Rightarrow> rexp \<Rightarrow> (char \<times> rexp)" (infixl "[.]" 91)
+ where
+"(c, ZERO) [.] t = (c, ZERO)"
+| "(c, ONE) [.] t = (c, t)"
+| "(c, p) [.] t = (c, SEQ p t)"
+
+
+fun circle_concat :: "(char \<times> rexp ) set \<Rightarrow> rexp \<Rightarrow> (char \<times> rexp) set" ( infixl "\<circle>" 90)
+ where
+"l \<circle> ZERO = {}"
+| "l \<circle> ONE = l"
+| "l \<circle> t = ( (\<lambda>p. p [.] t) ` l ) "
+
+
+
+fun linear_form :: "rexp \<Rightarrow>( char \<times> rexp ) set"
+ where
+ "linear_form ZERO = {}"
+| "linear_form ONE = {}"
+| "linear_form (CH c) = {(c, ONE)}"
+| "linear_form (ALT r1 r2) = (linear_form) r1 \<union> (linear_form r2)"
+| "linear_form (SEQ r1 r2) = (if (nullable r1) then (linear_form r1) \<circle> r2 \<union> linear_form r2 else (linear_form r1) \<circle> r2) "
+| "linear_form (STAR r ) = (linear_form r) \<circle> (STAR r)"
+
+
+value "linear_form (SEQ (STAR (CH x)) (STAR (ALT (SEQ (CH x) (CH x)) (CH y) )) )"
+
+
+value "linear_form (STAR (ALT (SEQ (CH x) (CH x)) (CH y) )) "
+
+fun pdero :: "char \<Rightarrow> rexp \<Rightarrow> rexp set"
+ where
+"pdero c t = \<Union> ((\<lambda>(d, p). if d = c then {p} else {}) ` (linear_form t) )"
+
+fun pderso :: "char list \<Rightarrow> rexp \<Rightarrow> rexp set"
+ where
+ "pderso [] r = {r}"
+| "pderso (c # s) r = \<Union> ( pderso s ` (pdero c r) )"
+
+lemma pdero_result:
+ shows "pdero c (STAR (ALT (CH c) (SEQ (CH c) (CH c)))) = {SEQ (CH c)(STAR (ALT (CH c) (SEQ (CH c) (CH c)))),(STAR (ALT (CH c) (SEQ (CH c) (CH c))))}"
+ apply(simp)
+ by auto
+
+fun concatLen :: "rexp \<Rightarrow> nat" where
+"concatLen ZERO = 0" |
+"concatLen ONE = 0" |
+"concatLen (CH c) = 0" |
+"concatLen (SEQ v1 v2) = Suc (max (concatLen v1) (concatLen v2))" |
+" concatLen (ALT v1 v2) = max (concatLen v1) (concatLen v2)" |
+" concatLen (STAR v) = Suc (concatLen v)"
+
+
+
+end
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/thys3/Positions.thy Wed Jun 29 12:38:05 2022 +0100
@@ -0,0 +1,773 @@
+
+theory Positions
+ imports PosixSpec Lexer
+begin
+
+chapter \<open>An alternative definition for POSIX values\<close>
+
+section \<open>Positions in Values\<close>
+
+fun
+ at :: "val \<Rightarrow> nat list \<Rightarrow> val"
+where
+ "at v [] = v"
+| "at (Left v) (0#ps)= at v ps"
+| "at (Right v) (Suc 0#ps)= at v ps"
+| "at (Seq v1 v2) (0#ps)= at v1 ps"
+| "at (Seq v1 v2) (Suc 0#ps)= at v2 ps"
+| "at (Stars vs) (n#ps)= at (nth vs n) ps"
+
+
+
+fun Pos :: "val \<Rightarrow> (nat list) set"
+where
+ "Pos (Void) = {[]}"
+| "Pos (Char c) = {[]}"
+| "Pos (Left v) = {[]} \<union> {0#ps | ps. ps \<in> Pos v}"
+| "Pos (Right v) = {[]} \<union> {1#ps | ps. ps \<in> Pos v}"
+| "Pos (Seq v1 v2) = {[]} \<union> {0#ps | ps. ps \<in> Pos v1} \<union> {1#ps | ps. ps \<in> Pos v2}"
+| "Pos (Stars []) = {[]}"
+| "Pos (Stars (v#vs)) = {[]} \<union> {0#ps | ps. ps \<in> Pos v} \<union> {Suc n#ps | n ps. n#ps \<in> Pos (Stars vs)}"
+
+
+lemma Pos_stars:
+ "Pos (Stars vs) = {[]} \<union> (\<Union>n < length vs. {n#ps | ps. ps \<in> Pos (vs ! n)})"
+apply(induct vs)
+apply(auto simp add: insert_ident less_Suc_eq_0_disj)
+done
+
+lemma Pos_empty:
+ shows "[] \<in> Pos v"
+by (induct v rule: Pos.induct)(auto)
+
+
+abbreviation
+ "intlen vs \<equiv> int (length vs)"
+
+
+definition pflat_len :: "val \<Rightarrow> nat list => int"
+where
+ "pflat_len v p \<equiv> (if p \<in> Pos v then intlen (flat (at v p)) else -1)"
+
+lemma pflat_len_simps:
+ shows "pflat_len (Seq v1 v2) (0#p) = pflat_len v1 p"
+ and "pflat_len (Seq v1 v2) (Suc 0#p) = pflat_len v2 p"
+ and "pflat_len (Left v) (0#p) = pflat_len v p"
+ and "pflat_len (Left v) (Suc 0#p) = -1"
+ and "pflat_len (Right v) (Suc 0#p) = pflat_len v p"
+ and "pflat_len (Right v) (0#p) = -1"
+ and "pflat_len (Stars (v#vs)) (Suc n#p) = pflat_len (Stars vs) (n#p)"
+ and "pflat_len (Stars (v#vs)) (0#p) = pflat_len v p"
+ and "pflat_len v [] = intlen (flat v)"
+by (auto simp add: pflat_len_def Pos_empty)
+
+lemma pflat_len_Stars_simps:
+ assumes "n < length vs"
+ shows "pflat_len (Stars vs) (n#p) = pflat_len (vs!n) p"
+using assms
+apply(induct vs arbitrary: n p)
+apply(auto simp add: less_Suc_eq_0_disj pflat_len_simps)
+done
+
+lemma pflat_len_outside:
+ assumes "p \<notin> Pos v1"
+ shows "pflat_len v1 p = -1 "
+using assms by (simp add: pflat_len_def)
+
+
+
+section \<open>Orderings\<close>
+
+
+definition prefix_list:: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" ("_ \<sqsubseteq>pre _" [60,59] 60)
+where
+ "ps1 \<sqsubseteq>pre ps2 \<equiv> \<exists>ps'. ps1 @ps' = ps2"
+
+definition sprefix_list:: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" ("_ \<sqsubset>spre _" [60,59] 60)
+where
+ "ps1 \<sqsubset>spre ps2 \<equiv> ps1 \<sqsubseteq>pre ps2 \<and> ps1 \<noteq> ps2"
+
+inductive lex_list :: "nat list \<Rightarrow> nat list \<Rightarrow> bool" ("_ \<sqsubset>lex _" [60,59] 60)
+where
+ "[] \<sqsubset>lex (p#ps)"
+| "ps1 \<sqsubset>lex ps2 \<Longrightarrow> (p#ps1) \<sqsubset>lex (p#ps2)"
+| "p1 < p2 \<Longrightarrow> (p1#ps1) \<sqsubset>lex (p2#ps2)"
+
+lemma lex_irrfl:
+ fixes ps1 ps2 :: "nat list"
+ assumes "ps1 \<sqsubset>lex ps2"
+ shows "ps1 \<noteq> ps2"
+using assms
+by(induct rule: lex_list.induct)(auto)
+
+lemma lex_simps [simp]:
+ fixes xs ys :: "nat list"
+ shows "[] \<sqsubset>lex ys \<longleftrightarrow> ys \<noteq> []"
+ and "xs \<sqsubset>lex [] \<longleftrightarrow> False"
+ and "(x # xs) \<sqsubset>lex (y # ys) \<longleftrightarrow> (x < y \<or> (x = y \<and> xs \<sqsubset>lex ys))"
+by (auto simp add: neq_Nil_conv elim: lex_list.cases intro: lex_list.intros)
+
+lemma lex_trans:
+ fixes ps1 ps2 ps3 :: "nat list"
+ assumes "ps1 \<sqsubset>lex ps2" "ps2 \<sqsubset>lex ps3"
+ shows "ps1 \<sqsubset>lex ps3"
+using assms
+by (induct arbitrary: ps3 rule: lex_list.induct)
+ (auto elim: lex_list.cases)
+
+
+lemma lex_trichotomous:
+ fixes p q :: "nat list"
+ shows "p = q \<or> p \<sqsubset>lex q \<or> q \<sqsubset>lex p"
+apply(induct p arbitrary: q)
+apply(auto elim: lex_list.cases)
+apply(case_tac q)
+apply(auto)
+done
+
+
+
+
+section \<open>POSIX Ordering of Values According to Okui \& Suzuki\<close>
+
+
+definition PosOrd:: "val \<Rightarrow> nat list \<Rightarrow> val \<Rightarrow> bool" ("_ \<sqsubset>val _ _" [60, 60, 59] 60)
+where
+ "v1 \<sqsubset>val p v2 \<equiv> pflat_len v1 p > pflat_len v2 p \<and>
+ (\<forall>q \<in> Pos v1 \<union> Pos v2. q \<sqsubset>lex p \<longrightarrow> pflat_len v1 q = pflat_len v2 q)"
+
+lemma PosOrd_def2:
+ shows "v1 \<sqsubset>val p v2 \<longleftrightarrow>
+ pflat_len v1 p > pflat_len v2 p \<and>
+ (\<forall>q \<in> Pos v1. q \<sqsubset>lex p \<longrightarrow> pflat_len v1 q = pflat_len v2 q) \<and>
+ (\<forall>q \<in> Pos v2. q \<sqsubset>lex p \<longrightarrow> pflat_len v1 q = pflat_len v2 q)"
+unfolding PosOrd_def
+apply(auto)
+done
+
+
+definition PosOrd_ex:: "val \<Rightarrow> val \<Rightarrow> bool" ("_ :\<sqsubset>val _" [60, 59] 60)
+where
+ "v1 :\<sqsubset>val v2 \<equiv> \<exists>p. v1 \<sqsubset>val p v2"
+
+definition PosOrd_ex_eq:: "val \<Rightarrow> val \<Rightarrow> bool" ("_ :\<sqsubseteq>val _" [60, 59] 60)
+where
+ "v1 :\<sqsubseteq>val v2 \<equiv> v1 :\<sqsubset>val v2 \<or> v1 = v2"
+
+
+lemma PosOrd_trans:
+ assumes "v1 :\<sqsubset>val v2" "v2 :\<sqsubset>val v3"
+ shows "v1 :\<sqsubset>val v3"
+proof -
+ from assms obtain p p'
+ where as: "v1 \<sqsubset>val p v2" "v2 \<sqsubset>val p' v3" unfolding PosOrd_ex_def by blast
+ then have pos: "p \<in> Pos v1" "p' \<in> Pos v2" unfolding PosOrd_def pflat_len_def
+ by (smt not_int_zless_negative)+
+ have "p = p' \<or> p \<sqsubset>lex p' \<or> p' \<sqsubset>lex p"
+ by (rule lex_trichotomous)
+ moreover
+ { assume "p = p'"
+ with as have "v1 \<sqsubset>val p v3" unfolding PosOrd_def pflat_len_def
+ by (smt Un_iff)
+ then have " v1 :\<sqsubset>val v3" unfolding PosOrd_ex_def by blast
+ }
+ moreover
+ { assume "p \<sqsubset>lex p'"
+ with as have "v1 \<sqsubset>val p v3" unfolding PosOrd_def pflat_len_def
+ by (smt Un_iff lex_trans)
+ then have " v1 :\<sqsubset>val v3" unfolding PosOrd_ex_def by blast
+ }
+ moreover
+ { assume "p' \<sqsubset>lex p"
+ with as have "v1 \<sqsubset>val p' v3" unfolding PosOrd_def
+ by (smt Un_iff lex_trans pflat_len_def)
+ then have "v1 :\<sqsubset>val v3" unfolding PosOrd_ex_def by blast
+ }
+ ultimately show "v1 :\<sqsubset>val v3" by blast
+qed
+
+lemma PosOrd_irrefl:
+ assumes "v :\<sqsubset>val v"
+ shows "False"
+using assms unfolding PosOrd_ex_def PosOrd_def
+by auto
+
+lemma PosOrd_assym:
+ assumes "v1 :\<sqsubset>val v2"
+ shows "\<not>(v2 :\<sqsubset>val v1)"
+using assms
+using PosOrd_irrefl PosOrd_trans by blast
+
+(*
+ :\<sqsubseteq>val and :\<sqsubset>val are partial orders.
+*)
+
+lemma PosOrd_ordering:
+ shows "ordering (\<lambda>v1 v2. v1 :\<sqsubseteq>val v2) (\<lambda> v1 v2. v1 :\<sqsubset>val v2)"
+unfolding ordering_def PosOrd_ex_eq_def
+apply(auto)
+using PosOrd_trans partial_preordering_def apply blast
+using PosOrd_assym ordering_axioms_def by blast
+
+lemma PosOrd_order:
+ shows "class.order (\<lambda>v1 v2. v1 :\<sqsubseteq>val v2) (\<lambda> v1 v2. v1 :\<sqsubset>val v2)"
+using PosOrd_ordering
+apply(simp add: class.order_def class.preorder_def class.order_axioms_def)
+ by (metis (full_types) PosOrd_ex_eq_def PosOrd_irrefl PosOrd_trans)
+
+
+lemma PosOrd_ex_eq2:
+ shows "v1 :\<sqsubset>val v2 \<longleftrightarrow> (v1 :\<sqsubseteq>val v2 \<and> v1 \<noteq> v2)"
+ using PosOrd_ordering
+ using PosOrd_ex_eq_def PosOrd_irrefl by blast
+
+lemma PosOrdeq_trans:
+ assumes "v1 :\<sqsubseteq>val v2" "v2 :\<sqsubseteq>val v3"
+ shows "v1 :\<sqsubseteq>val v3"
+using assms PosOrd_ordering
+ unfolding ordering_def
+ by (metis partial_preordering.trans)
+
+lemma PosOrdeq_antisym:
+ assumes "v1 :\<sqsubseteq>val v2" "v2 :\<sqsubseteq>val v1"
+ shows "v1 = v2"
+using assms PosOrd_ordering
+ unfolding ordering_def
+ by (simp add: ordering_axioms_def)
+
+lemma PosOrdeq_refl:
+ shows "v :\<sqsubseteq>val v"
+unfolding PosOrd_ex_eq_def
+by auto
+
+
+lemma PosOrd_shorterE:
+ assumes "v1 :\<sqsubset>val v2"
+ shows "length (flat v2) \<le> length (flat v1)"
+using assms unfolding PosOrd_ex_def PosOrd_def
+apply(auto)
+apply(case_tac p)
+apply(simp add: pflat_len_simps)
+apply(drule_tac x="[]" in bspec)
+apply(simp add: Pos_empty)
+apply(simp add: pflat_len_simps)
+done
+
+lemma PosOrd_shorterI:
+ assumes "length (flat v2) < length (flat v1)"
+ shows "v1 :\<sqsubset>val v2"
+unfolding PosOrd_ex_def PosOrd_def pflat_len_def
+using assms Pos_empty by force
+
+lemma PosOrd_spreI:
+ assumes "flat v' \<sqsubset>spre flat v"
+ shows "v :\<sqsubset>val v'"
+using assms
+apply(rule_tac PosOrd_shorterI)
+unfolding prefix_list_def sprefix_list_def
+by (metis append_Nil2 append_eq_conv_conj drop_all le_less_linear)
+
+lemma pflat_len_inside:
+ assumes "pflat_len v2 p < pflat_len v1 p"
+ shows "p \<in> Pos v1"
+using assms
+unfolding pflat_len_def
+by (auto split: if_splits)
+
+
+lemma PosOrd_Left_Right:
+ assumes "flat v1 = flat v2"
+ shows "Left v1 :\<sqsubset>val Right v2"
+unfolding PosOrd_ex_def
+apply(rule_tac x="[0]" in exI)
+apply(auto simp add: PosOrd_def pflat_len_simps assms)
+done
+
+lemma PosOrd_LeftE:
+ assumes "Left v1 :\<sqsubset>val Left v2" "flat v1 = flat v2"
+ shows "v1 :\<sqsubset>val v2"
+using assms
+unfolding PosOrd_ex_def PosOrd_def2
+apply(auto simp add: pflat_len_simps)
+apply(frule pflat_len_inside)
+apply(auto simp add: pflat_len_simps)
+by (metis lex_simps(3) pflat_len_simps(3))
+
+lemma PosOrd_LeftI:
+ assumes "v1 :\<sqsubset>val v2" "flat v1 = flat v2"
+ shows "Left v1 :\<sqsubset>val Left v2"
+using assms
+unfolding PosOrd_ex_def PosOrd_def2
+apply(auto simp add: pflat_len_simps)
+by (metis less_numeral_extra(3) lex_simps(3) pflat_len_simps(3))
+
+lemma PosOrd_Left_eq:
+ assumes "flat v1 = flat v2"
+ shows "Left v1 :\<sqsubset>val Left v2 \<longleftrightarrow> v1 :\<sqsubset>val v2"
+using assms PosOrd_LeftE PosOrd_LeftI
+by blast
+
+
+lemma PosOrd_RightE:
+ assumes "Right v1 :\<sqsubset>val Right v2" "flat v1 = flat v2"
+ shows "v1 :\<sqsubset>val v2"
+using assms
+unfolding PosOrd_ex_def PosOrd_def2
+apply(auto simp add: pflat_len_simps)
+apply(frule pflat_len_inside)
+apply(auto simp add: pflat_len_simps)
+by (metis lex_simps(3) pflat_len_simps(5))
+
+lemma PosOrd_RightI:
+ assumes "v1 :\<sqsubset>val v2" "flat v1 = flat v2"
+ shows "Right v1 :\<sqsubset>val Right v2"
+using assms
+unfolding PosOrd_ex_def PosOrd_def2
+apply(auto simp add: pflat_len_simps)
+by (metis lex_simps(3) nat_neq_iff pflat_len_simps(5))
+
+
+lemma PosOrd_Right_eq:
+ assumes "flat v1 = flat v2"
+ shows "Right v1 :\<sqsubset>val Right v2 \<longleftrightarrow> v1 :\<sqsubset>val v2"
+using assms PosOrd_RightE PosOrd_RightI
+by blast
+
+
+lemma PosOrd_SeqI1:
+ assumes "v1 :\<sqsubset>val w1" "flat (Seq v1 v2) = flat (Seq w1 w2)"
+ shows "Seq v1 v2 :\<sqsubset>val Seq w1 w2"
+using assms(1)
+apply(subst (asm) PosOrd_ex_def)
+apply(subst (asm) PosOrd_def)
+apply(clarify)
+apply(subst PosOrd_ex_def)
+apply(rule_tac x="0#p" in exI)
+apply(subst PosOrd_def)
+apply(rule conjI)
+apply(simp add: pflat_len_simps)
+apply(rule ballI)
+apply(rule impI)
+apply(simp only: Pos.simps)
+apply(auto)[1]
+apply(simp add: pflat_len_simps)
+apply(auto simp add: pflat_len_simps)
+using assms(2)
+apply(simp)
+apply(metis length_append of_nat_add)
+done
+
+lemma PosOrd_SeqI2:
+ assumes "v2 :\<sqsubset>val w2" "flat v2 = flat w2"
+ shows "Seq v v2 :\<sqsubset>val Seq v w2"
+using assms(1)
+apply(subst (asm) PosOrd_ex_def)
+apply(subst (asm) PosOrd_def)
+apply(clarify)
+apply(subst PosOrd_ex_def)
+apply(rule_tac x="Suc 0#p" in exI)
+apply(subst PosOrd_def)
+apply(rule conjI)
+apply(simp add: pflat_len_simps)
+apply(rule ballI)
+apply(rule impI)
+apply(simp only: Pos.simps)
+apply(auto)[1]
+apply(simp add: pflat_len_simps)
+using assms(2)
+apply(simp)
+apply(auto simp add: pflat_len_simps)
+done
+
+lemma PosOrd_Seq_eq:
+ assumes "flat v2 = flat w2"
+ shows "(Seq v v2) :\<sqsubset>val (Seq v w2) \<longleftrightarrow> v2 :\<sqsubset>val w2"
+using assms
+apply(auto)
+prefer 2
+apply(simp add: PosOrd_SeqI2)
+apply(simp add: PosOrd_ex_def)
+apply(auto)
+apply(case_tac p)
+apply(simp add: PosOrd_def pflat_len_simps)
+apply(case_tac a)
+apply(simp add: PosOrd_def pflat_len_simps)
+apply(clarify)
+apply(case_tac nat)
+prefer 2
+apply(simp add: PosOrd_def pflat_len_simps pflat_len_outside)
+apply(rule_tac x="list" in exI)
+apply(auto simp add: PosOrd_def2 pflat_len_simps)
+apply(smt Collect_disj_eq lex_list.intros(2) mem_Collect_eq pflat_len_simps(2))
+apply(smt Collect_disj_eq lex_list.intros(2) mem_Collect_eq pflat_len_simps(2))
+done
+
+
+
+lemma PosOrd_StarsI:
+ assumes "v1 :\<sqsubset>val v2" "flats (v1#vs1) = flats (v2#vs2)"
+ shows "Stars (v1#vs1) :\<sqsubset>val Stars (v2#vs2)"
+using assms(1)
+apply(subst (asm) PosOrd_ex_def)
+apply(subst (asm) PosOrd_def)
+apply(clarify)
+apply(subst PosOrd_ex_def)
+apply(subst PosOrd_def)
+apply(rule_tac x="0#p" in exI)
+apply(simp add: pflat_len_Stars_simps pflat_len_simps)
+using assms(2)
+apply(simp add: pflat_len_simps)
+apply(auto simp add: pflat_len_Stars_simps pflat_len_simps)
+by (metis length_append of_nat_add)
+
+lemma PosOrd_StarsI2:
+ assumes "Stars vs1 :\<sqsubset>val Stars vs2" "flats vs1 = flats vs2"
+ shows "Stars (v#vs1) :\<sqsubset>val Stars (v#vs2)"
+using assms(1)
+apply(subst (asm) PosOrd_ex_def)
+apply(subst (asm) PosOrd_def)
+apply(clarify)
+apply(subst PosOrd_ex_def)
+apply(subst PosOrd_def)
+apply(case_tac p)
+apply(simp add: pflat_len_simps)
+apply(rule_tac x="Suc a#list" in exI)
+apply(auto simp add: pflat_len_Stars_simps pflat_len_simps assms(2))
+done
+
+lemma PosOrd_Stars_appendI:
+ assumes "Stars vs1 :\<sqsubset>val Stars vs2" "flat (Stars vs1) = flat (Stars vs2)"
+ shows "Stars (vs @ vs1) :\<sqsubset>val Stars (vs @ vs2)"
+using assms
+apply(induct vs)
+apply(simp)
+apply(simp add: PosOrd_StarsI2)
+done
+
+lemma PosOrd_StarsE2:
+ assumes "Stars (v # vs1) :\<sqsubset>val Stars (v # vs2)"
+ shows "Stars vs1 :\<sqsubset>val Stars vs2"
+using assms
+apply(subst (asm) PosOrd_ex_def)
+apply(erule exE)
+apply(case_tac p)
+apply(simp)
+apply(simp add: PosOrd_def pflat_len_simps)
+apply(subst PosOrd_ex_def)
+apply(rule_tac x="[]" in exI)
+apply(simp add: PosOrd_def pflat_len_simps Pos_empty)
+apply(simp)
+apply(case_tac a)
+apply(clarify)
+apply(auto simp add: pflat_len_simps PosOrd_def pflat_len_def split: if_splits)[1]
+apply(clarify)
+apply(simp add: PosOrd_ex_def)
+apply(rule_tac x="nat#list" in exI)
+apply(auto simp add: PosOrd_def pflat_len_simps)[1]
+apply(case_tac q)
+apply(simp add: PosOrd_def pflat_len_simps)
+apply(clarify)
+apply(drule_tac x="Suc a # lista" in bspec)
+apply(simp)
+apply(auto simp add: PosOrd_def pflat_len_simps)[1]
+apply(case_tac q)
+apply(simp add: PosOrd_def pflat_len_simps)
+apply(clarify)
+apply(drule_tac x="Suc a # lista" in bspec)
+apply(simp)
+apply(auto simp add: PosOrd_def pflat_len_simps)[1]
+done
+
+lemma PosOrd_Stars_appendE:
+ assumes "Stars (vs @ vs1) :\<sqsubset>val Stars (vs @ vs2)"
+ shows "Stars vs1 :\<sqsubset>val Stars vs2"
+using assms
+apply(induct vs)
+apply(simp)
+apply(simp add: PosOrd_StarsE2)
+done
+
+lemma PosOrd_Stars_append_eq:
+ assumes "flats vs1 = flats vs2"
+ shows "Stars (vs @ vs1) :\<sqsubset>val Stars (vs @ vs2) \<longleftrightarrow> Stars vs1 :\<sqsubset>val Stars vs2"
+using assms
+apply(rule_tac iffI)
+apply(erule PosOrd_Stars_appendE)
+apply(rule PosOrd_Stars_appendI)
+apply(auto)
+done
+
+lemma PosOrd_almost_trichotomous:
+ shows "v1 :\<sqsubset>val v2 \<or> v2 :\<sqsubset>val v1 \<or> (length (flat v1) = length (flat v2))"
+apply(auto simp add: PosOrd_ex_def)
+apply(auto simp add: PosOrd_def)
+apply(rule_tac x="[]" in exI)
+apply(auto simp add: Pos_empty pflat_len_simps)
+apply(drule_tac x="[]" in spec)
+apply(auto simp add: Pos_empty pflat_len_simps)
+done
+
+
+
+section \<open>The Posix Value is smaller than any other Value\<close>
+
+
+lemma Posix_PosOrd:
+ assumes "s \<in> r \<rightarrow> v1" "v2 \<in> LV r s"
+ shows "v1 :\<sqsubseteq>val v2"
+using assms
+proof (induct arbitrary: v2 rule: Posix.induct)
+ case (Posix_ONE v)
+ have "v \<in> LV ONE []" by fact
+ then have "v = Void"
+ by (simp add: LV_simps)
+ then show "Void :\<sqsubseteq>val v"
+ by (simp add: PosOrd_ex_eq_def)
+next
+ case (Posix_CH c v)
+ have "v \<in> LV (CH c) [c]" by fact
+ then have "v = Char c"
+ by (simp add: LV_simps)
+ then show "Char c :\<sqsubseteq>val v"
+ by (simp add: PosOrd_ex_eq_def)
+next
+ case (Posix_ALT1 s r1 v r2 v2)
+ have as1: "s \<in> r1 \<rightarrow> v" by fact
+ have IH: "\<And>v2. v2 \<in> LV r1 s \<Longrightarrow> v :\<sqsubseteq>val v2" by fact
+ have "v2 \<in> LV (ALT r1 r2) s" by fact
+ then have "\<Turnstile> v2 : ALT r1 r2" "flat v2 = s"
+ by(auto simp add: LV_def prefix_list_def)
+ then consider
+ (Left) v3 where "v2 = Left v3" "\<Turnstile> v3 : r1" "flat v3 = s"
+ | (Right) v3 where "v2 = Right v3" "\<Turnstile> v3 : r2" "flat v3 = s"
+ by (auto elim: Prf.cases)
+ then show "Left v :\<sqsubseteq>val v2"
+ proof(cases)
+ case (Left v3)
+ have "v3 \<in> LV r1 s" using Left(2,3)
+ by (auto simp add: LV_def prefix_list_def)
+ with IH have "v :\<sqsubseteq>val v3" by simp
+ moreover
+ have "flat v3 = flat v" using as1 Left(3)
+ by (simp add: Posix1(2))
+ ultimately have "Left v :\<sqsubseteq>val Left v3"
+ by (simp add: PosOrd_ex_eq_def PosOrd_Left_eq)
+ then show "Left v :\<sqsubseteq>val v2" unfolding Left .
+ next
+ case (Right v3)
+ have "flat v3 = flat v" using as1 Right(3)
+ by (simp add: Posix1(2))
+ then have "Left v :\<sqsubseteq>val Right v3"
+ unfolding PosOrd_ex_eq_def
+ by (simp add: PosOrd_Left_Right)
+ then show "Left v :\<sqsubseteq>val v2" unfolding Right .
+ qed
+next
+ case (Posix_ALT2 s r2 v r1 v2)
+ have as1: "s \<in> r2 \<rightarrow> v" by fact
+ have as2: "s \<notin> L r1" by fact
+ have IH: "\<And>v2. v2 \<in> LV r2 s \<Longrightarrow> v :\<sqsubseteq>val v2" by fact
+ have "v2 \<in> LV (ALT r1 r2) s" by fact
+ then have "\<Turnstile> v2 : ALT r1 r2" "flat v2 = s"
+ by(auto simp add: LV_def prefix_list_def)
+ then consider
+ (Left) v3 where "v2 = Left v3" "\<Turnstile> v3 : r1" "flat v3 = s"
+ | (Right) v3 where "v2 = Right v3" "\<Turnstile> v3 : r2" "flat v3 = s"
+ by (auto elim: Prf.cases)
+ then show "Right v :\<sqsubseteq>val v2"
+ proof (cases)
+ case (Right v3)
+ have "v3 \<in> LV r2 s" using Right(2,3)
+ by (auto simp add: LV_def prefix_list_def)
+ with IH have "v :\<sqsubseteq>val v3" by simp
+ moreover
+ have "flat v3 = flat v" using as1 Right(3)
+ by (simp add: Posix1(2))
+ ultimately have "Right v :\<sqsubseteq>val Right v3"
+ by (auto simp add: PosOrd_ex_eq_def PosOrd_RightI)
+ then show "Right v :\<sqsubseteq>val v2" unfolding Right .
+ next
+ case (Left v3)
+ have "v3 \<in> LV r1 s" using Left(2,3) as2
+ by (auto simp add: LV_def prefix_list_def)
+ then have "flat v3 = flat v \<and> \<Turnstile> v3 : r1" using as1 Left(3)
+ by (simp add: Posix1(2) LV_def)
+ then have "False" using as1 as2 Left
+ by (auto simp add: Posix1(2) L_flat_Prf1)
+ then show "Right v :\<sqsubseteq>val v2" by simp
+ qed
+next
+ case (Posix_SEQ s1 r1 v1 s2 r2 v2 v3)
+ have "s1 \<in> r1 \<rightarrow> v1" "s2 \<in> r2 \<rightarrow> v2" by fact+
+ then have as1: "s1 = flat v1" "s2 = flat v2" by (simp_all add: Posix1(2))
+ have IH1: "\<And>v3. v3 \<in> LV r1 s1 \<Longrightarrow> v1 :\<sqsubseteq>val v3" by fact
+ have IH2: "\<And>v3. v3 \<in> LV r2 s2 \<Longrightarrow> v2 :\<sqsubseteq>val v3" by fact
+ have cond: "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L r1 \<and> s\<^sub>4 \<in> L r2)" by fact
+ have "v3 \<in> LV (SEQ r1 r2) (s1 @ s2)" by fact
+ then obtain v3a v3b where eqs:
+ "v3 = Seq v3a v3b" "\<Turnstile> v3a : r1" "\<Turnstile> v3b : r2"
+ "flat v3a @ flat v3b = s1 @ s2"
+ by (force simp add: prefix_list_def LV_def elim: Prf.cases)
+ with cond have "flat v3a \<sqsubseteq>pre s1" unfolding prefix_list_def
+ by (smt L_flat_Prf1 append_eq_append_conv2 append_self_conv)
+ then have "flat v3a \<sqsubset>spre s1 \<or> (flat v3a = s1 \<and> flat v3b = s2)" using eqs
+ by (simp add: sprefix_list_def append_eq_conv_conj)
+ then have q2: "v1 :\<sqsubset>val v3a \<or> (flat v3a = s1 \<and> flat v3b = s2)"
+ using PosOrd_spreI as1(1) eqs by blast
+ then have "v1 :\<sqsubset>val v3a \<or> (v3a \<in> LV r1 s1 \<and> v3b \<in> LV r2 s2)" using eqs(2,3)
+ by (auto simp add: LV_def)
+ then have "v1 :\<sqsubset>val v3a \<or> (v1 :\<sqsubseteq>val v3a \<and> v2 :\<sqsubseteq>val v3b)" using IH1 IH2 by blast
+ then have "Seq v1 v2 :\<sqsubseteq>val Seq v3a v3b" using eqs q2 as1
+ unfolding PosOrd_ex_eq_def by (auto simp add: PosOrd_SeqI1 PosOrd_Seq_eq)
+ then show "Seq v1 v2 :\<sqsubseteq>val v3" unfolding eqs by blast
+next
+ case (Posix_STAR1 s1 r v s2 vs v3)
+ have "s1 \<in> r \<rightarrow> v" "s2 \<in> STAR r \<rightarrow> Stars vs" by fact+
+ then have as1: "s1 = flat v" "s2 = flat (Stars vs)" by (auto dest: Posix1(2))
+ have IH1: "\<And>v3. v3 \<in> LV r s1 \<Longrightarrow> v :\<sqsubseteq>val v3" by fact
+ have IH2: "\<And>v3. v3 \<in> LV (STAR r) s2 \<Longrightarrow> Stars vs :\<sqsubseteq>val v3" by fact
+ have cond: "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (STAR r))" by fact
+ have cond2: "flat v \<noteq> []" by fact
+ have "v3 \<in> LV (STAR r) (s1 @ s2)" by fact
+ then consider
+ (NonEmpty) v3a vs3 where "v3 = Stars (v3a # vs3)"
+ "\<Turnstile> v3a : r" "\<Turnstile> Stars vs3 : STAR r"
+ "flat (Stars (v3a # vs3)) = s1 @ s2"
+ | (Empty) "v3 = Stars []"
+ unfolding LV_def
+ apply(auto)
+ apply(erule Prf.cases)
+ apply(auto)
+ apply(case_tac vs)
+ apply(auto intro: Prf.intros)
+ done
+ then show "Stars (v # vs) :\<sqsubseteq>val v3"
+ proof (cases)
+ case (NonEmpty v3a vs3)
+ have "flat (Stars (v3a # vs3)) = s1 @ s2" using NonEmpty(4) .
+ with cond have "flat v3a \<sqsubseteq>pre s1" using NonEmpty(2,3)
+ unfolding prefix_list_def
+ by (smt L_flat_Prf1 append_Nil2 append_eq_append_conv2 flat.simps(7))
+ then have "flat v3a \<sqsubset>spre s1 \<or> (flat v3a = s1 \<and> flat (Stars vs3) = s2)" using NonEmpty(4)
+ by (simp add: sprefix_list_def append_eq_conv_conj)
+ then have q2: "v :\<sqsubset>val v3a \<or> (flat v3a = s1 \<and> flat (Stars vs3) = s2)"
+ using PosOrd_spreI as1(1) NonEmpty(4) by blast
+ then have "v :\<sqsubset>val v3a \<or> (v3a \<in> LV r s1 \<and> Stars vs3 \<in> LV (STAR r) s2)"
+ using NonEmpty(2,3) by (auto simp add: LV_def)
+ then have "v :\<sqsubset>val v3a \<or> (v :\<sqsubseteq>val v3a \<and> Stars vs :\<sqsubseteq>val Stars vs3)" using IH1 IH2 by blast
+ then have "v :\<sqsubset>val v3a \<or> (v = v3a \<and> Stars vs :\<sqsubseteq>val Stars vs3)"
+ unfolding PosOrd_ex_eq_def by auto
+ then have "Stars (v # vs) :\<sqsubseteq>val Stars (v3a # vs3)" using NonEmpty(4) q2 as1
+ unfolding PosOrd_ex_eq_def
+ using PosOrd_StarsI PosOrd_StarsI2 by auto
+ then show "Stars (v # vs) :\<sqsubseteq>val v3" unfolding NonEmpty by blast
+ next
+ case Empty
+ have "v3 = Stars []" by fact
+ then show "Stars (v # vs) :\<sqsubseteq>val v3"
+ unfolding PosOrd_ex_eq_def using cond2
+ by (simp add: PosOrd_shorterI)
+ qed
+next
+ case (Posix_STAR2 r v2)
+ have "v2 \<in> LV (STAR r) []" by fact
+ then have "v2 = Stars []"
+ unfolding LV_def by (auto elim: Prf.cases)
+ then show "Stars [] :\<sqsubseteq>val v2"
+ by (simp add: PosOrd_ex_eq_def)
+qed
+
+
+lemma Posix_PosOrd_reverse:
+ assumes "s \<in> r \<rightarrow> v1"
+ shows "\<not>(\<exists>v2 \<in> LV r s. v2 :\<sqsubset>val v1)"
+using assms
+by (metis Posix_PosOrd less_irrefl PosOrd_def
+ PosOrd_ex_eq_def PosOrd_ex_def PosOrd_trans)
+
+lemma PosOrd_Posix:
+ assumes "v1 \<in> LV r s" "\<forall>v\<^sub>2 \<in> LV r s. \<not> v\<^sub>2 :\<sqsubset>val v1"
+ shows "s \<in> r \<rightarrow> v1"
+proof -
+ have "s \<in> L r" using assms(1) unfolding LV_def
+ using L_flat_Prf1 by blast
+ then obtain vposix where vp: "s \<in> r \<rightarrow> vposix"
+ using lexer_correct_Some by blast
+ with assms(1) have "vposix :\<sqsubseteq>val v1" by (simp add: Posix_PosOrd)
+ then have "vposix = v1 \<or> vposix :\<sqsubset>val v1" unfolding PosOrd_ex_eq2 by auto
+ moreover
+ { assume "vposix :\<sqsubset>val v1"
+ moreover
+ have "vposix \<in> LV r s" using vp
+ using Posix_LV by blast
+ ultimately have "False" using assms(2) by blast
+ }
+ ultimately show "s \<in> r \<rightarrow> v1" using vp by blast
+qed
+
+lemma Least_existence:
+ assumes "LV r s \<noteq> {}"
+ shows " \<exists>vmin \<in> LV r s. \<forall>v \<in> LV r s. vmin :\<sqsubseteq>val v"
+proof -
+ from assms
+ obtain vposix where "s \<in> r \<rightarrow> vposix"
+ unfolding LV_def
+ using L_flat_Prf1 lexer_correct_Some by blast
+ then have "\<forall>v \<in> LV r s. vposix :\<sqsubseteq>val v"
+ by (simp add: Posix_PosOrd)
+ then show "\<exists>vmin \<in> LV r s. \<forall>v \<in> LV r s. vmin :\<sqsubseteq>val v"
+ using Posix_LV \<open>s \<in> r \<rightarrow> vposix\<close> by blast
+qed
+
+lemma Least_existence1:
+ assumes "LV r s \<noteq> {}"
+ shows " \<exists>!vmin \<in> LV r s. \<forall>v \<in> LV r s. vmin :\<sqsubseteq>val v"
+using Least_existence[OF assms] assms
+using PosOrdeq_antisym by blast
+
+lemma Least_existence2:
+ assumes "LV r s \<noteq> {}"
+ shows " \<exists>!vmin \<in> LV r s. lexer r s = Some vmin \<and> (\<forall>v \<in> LV r s. vmin :\<sqsubseteq>val v)"
+using Least_existence[OF assms] assms
+using PosOrdeq_antisym
+ using PosOrd_Posix PosOrd_ex_eq2 lexer_correctness(1) by auto
+
+
+lemma Least_existence1_pre:
+ assumes "LV r s \<noteq> {}"
+ shows " \<exists>!vmin \<in> LV r s. \<forall>v \<in> (LV r s \<union> {v'. flat v' \<sqsubset>spre s}). vmin :\<sqsubseteq>val v"
+using Least_existence[OF assms] assms
+apply -
+apply(erule bexE)
+apply(rule_tac a="vmin" in ex1I)
+apply(auto)[1]
+apply (metis PosOrd_Posix PosOrd_ex_eq2 PosOrd_spreI PosOrdeq_antisym Posix1(2))
+apply(auto)[1]
+apply(simp add: PosOrdeq_antisym)
+done
+
+lemma
+ shows "partial_order_on UNIV {(v1, v2). v1 :\<sqsubseteq>val v2}"
+apply(simp add: partial_order_on_def)
+apply(simp add: preorder_on_def refl_on_def)
+apply(simp add: PosOrdeq_refl)
+apply(auto)
+apply(rule transI)
+apply(auto intro: PosOrdeq_trans)[1]
+apply(rule antisymI)
+apply(simp add: PosOrdeq_antisym)
+done
+
+lemma
+ "wf {(v1, v2). v1 :\<sqsubset>val v2 \<and> v1 \<in> LV r s \<and> v2 \<in> LV r s}"
+apply(rule finite_acyclic_wf)
+prefer 2
+apply(simp add: acyclic_def)
+apply(induct_tac rule: trancl.induct)
+apply(auto)[1]
+oops
+
+
+unused_thms
+
+end
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/thys3/PosixSpec.thy Wed Jun 29 12:38:05 2022 +0100
@@ -0,0 +1,380 @@
+
+theory PosixSpec
+ imports RegLangs
+begin
+
+section \<open>"Plain" Values\<close>
+
+datatype val =
+ Void
+| Char char
+| Seq val val
+| Right val
+| Left val
+| Stars "val list"
+
+
+section \<open>The string behind a value\<close>
+
+fun
+ flat :: "val \<Rightarrow> string"
+where
+ "flat (Void) = []"
+| "flat (Char c) = [c]"
+| "flat (Left v) = flat v"
+| "flat (Right v) = flat v"
+| "flat (Seq v1 v2) = (flat v1) @ (flat v2)"
+| "flat (Stars []) = []"
+| "flat (Stars (v#vs)) = (flat v) @ (flat (Stars vs))"
+
+abbreviation
+ "flats vs \<equiv> concat (map flat vs)"
+
+lemma flat_Stars [simp]:
+ "flat (Stars vs) = flats vs"
+by (induct vs) (auto)
+
+
+section \<open>Lexical Values\<close>
+
+inductive
+ Prf :: "val \<Rightarrow> rexp \<Rightarrow> bool" ("\<Turnstile> _ : _" [100, 100] 100)
+where
+ "\<lbrakk>\<Turnstile> v1 : r1; \<Turnstile> v2 : r2\<rbrakk> \<Longrightarrow> \<Turnstile> Seq v1 v2 : SEQ r1 r2"
+| "\<Turnstile> v1 : r1 \<Longrightarrow> \<Turnstile> Left v1 : ALT r1 r2"
+| "\<Turnstile> v2 : r2 \<Longrightarrow> \<Turnstile> Right v2 : ALT r1 r2"
+| "\<Turnstile> Void : ONE"
+| "\<Turnstile> Char c : CH c"
+| "\<forall>v \<in> set vs. \<Turnstile> v : r \<and> flat v \<noteq> [] \<Longrightarrow> \<Turnstile> Stars vs : STAR r"
+
+inductive_cases Prf_elims:
+ "\<Turnstile> v : ZERO"
+ "\<Turnstile> v : SEQ r1 r2"
+ "\<Turnstile> v : ALT r1 r2"
+ "\<Turnstile> v : ONE"
+ "\<Turnstile> v : CH c"
+ "\<Turnstile> vs : STAR r"
+
+lemma Prf_Stars_appendE:
+ assumes "\<Turnstile> Stars (vs1 @ vs2) : STAR r"
+ shows "\<Turnstile> Stars vs1 : STAR r \<and> \<Turnstile> Stars vs2 : STAR r"
+using assms
+by (auto intro: Prf.intros elim!: Prf_elims)
+
+
+lemma flats_Prf_value:
+ assumes "\<forall>s\<in>set ss. \<exists>v. s = flat v \<and> \<Turnstile> v : r"
+ shows "\<exists>vs. flats vs = concat ss \<and> (\<forall>v\<in>set vs. \<Turnstile> v : r \<and> flat v \<noteq> [])"
+using assms
+apply(induct ss)
+apply(auto)
+apply(rule_tac x="[]" in exI)
+apply(simp)
+apply(case_tac "flat v = []")
+apply(rule_tac x="vs" in exI)
+apply(simp)
+apply(rule_tac x="v#vs" in exI)
+apply(simp)
+done
+
+
+lemma L_flat_Prf1:
+ assumes "\<Turnstile> v : r"
+ shows "flat v \<in> L r"
+using assms
+by (induct) (auto simp add: Sequ_def Star_concat)
+
+lemma L_flat_Prf2:
+ assumes "s \<in> L r"
+ shows "\<exists>v. \<Turnstile> v : r \<and> flat v = s"
+using assms
+proof(induct r arbitrary: s)
+ case (STAR r s)
+ have IH: "\<And>s. s \<in> L r \<Longrightarrow> \<exists>v. \<Turnstile> v : r \<and> flat v = s" by fact
+ have "s \<in> L (STAR r)" by fact
+ then obtain ss where "concat ss = s" "\<forall>s \<in> set ss. s \<in> L r \<and> s \<noteq> []"
+ using Star_split by auto
+ then obtain vs where "flats vs = s" "\<forall>v\<in>set vs. \<Turnstile> v : r \<and> flat v \<noteq> []"
+ using IH flats_Prf_value by metis
+ then show "\<exists>v. \<Turnstile> v : STAR r \<and> flat v = s"
+ using Prf.intros(6) flat_Stars by blast
+next
+ case (SEQ r1 r2 s)
+ then show "\<exists>v. \<Turnstile> v : SEQ r1 r2 \<and> flat v = s"
+ unfolding Sequ_def L.simps by (fastforce intro: Prf.intros)
+next
+ case (ALT r1 r2 s)
+ then show "\<exists>v. \<Turnstile> v : ALT r1 r2 \<and> flat v = s"
+ unfolding L.simps by (fastforce intro: Prf.intros)
+qed (auto intro: Prf.intros)
+
+
+lemma L_flat_Prf:
+ shows "L(r) = {flat v | v. \<Turnstile> v : r}"
+using L_flat_Prf1 L_flat_Prf2 by blast
+
+
+
+section \<open>Sets of Lexical Values\<close>
+
+text \<open>
+ Shows that lexical values are finite for a given regex and string.
+\<close>
+
+definition
+ LV :: "rexp \<Rightarrow> string \<Rightarrow> val set"
+where "LV r s \<equiv> {v. \<Turnstile> v : r \<and> flat v = s}"
+
+lemma LV_simps:
+ shows "LV ZERO s = {}"
+ and "LV ONE s = (if s = [] then {Void} else {})"
+ and "LV (CH c) s = (if s = [c] then {Char c} else {})"
+ and "LV (ALT r1 r2) s = Left ` LV r1 s \<union> Right ` LV r2 s"
+unfolding LV_def
+by (auto intro: Prf.intros elim: Prf.cases)
+
+
+abbreviation
+ "Prefixes s \<equiv> {s'. prefix s' s}"
+
+abbreviation
+ "Suffixes s \<equiv> {s'. suffix s' s}"
+
+abbreviation
+ "SSuffixes s \<equiv> {s'. strict_suffix s' s}"
+
+lemma Suffixes_cons [simp]:
+ shows "Suffixes (c # s) = Suffixes s \<union> {c # s}"
+by (auto simp add: suffix_def Cons_eq_append_conv)
+
+
+lemma finite_Suffixes:
+ shows "finite (Suffixes s)"
+by (induct s) (simp_all)
+
+lemma finite_SSuffixes:
+ shows "finite (SSuffixes s)"
+proof -
+ have "SSuffixes s \<subseteq> Suffixes s"
+ unfolding strict_suffix_def suffix_def by auto
+ then show "finite (SSuffixes s)"
+ using finite_Suffixes finite_subset by blast
+qed
+
+lemma finite_Prefixes:
+ shows "finite (Prefixes s)"
+proof -
+ have "finite (Suffixes (rev s))"
+ by (rule finite_Suffixes)
+ then have "finite (rev ` Suffixes (rev s))" by simp
+ moreover
+ have "rev ` (Suffixes (rev s)) = Prefixes s"
+ unfolding suffix_def prefix_def image_def
+ by (auto)(metis rev_append rev_rev_ident)+
+ ultimately show "finite (Prefixes s)" by simp
+qed
+
+lemma LV_STAR_finite:
+ assumes "\<forall>s. finite (LV r s)"
+ shows "finite (LV (STAR r) s)"
+proof(induct s rule: length_induct)
+ fix s::"char list"
+ assume "\<forall>s'. length s' < length s \<longrightarrow> finite (LV (STAR r) s')"
+ then have IH: "\<forall>s' \<in> SSuffixes s. finite (LV (STAR r) s')"
+ by (force simp add: strict_suffix_def suffix_def)
+ define f where "f \<equiv> \<lambda>(v, vs). Stars (v # vs)"
+ define S1 where "S1 \<equiv> \<Union>s' \<in> Prefixes s. LV r s'"
+ define S2 where "S2 \<equiv> \<Union>s2 \<in> SSuffixes s. Stars -` (LV (STAR r) s2)"
+ have "finite S1" using assms
+ unfolding S1_def by (simp_all add: finite_Prefixes)
+ moreover
+ with IH have "finite S2" unfolding S2_def
+ by (auto simp add: finite_SSuffixes inj_on_def finite_vimageI)
+ ultimately
+ have "finite ({Stars []} \<union> f ` (S1 \<times> S2))" by simp
+ moreover
+ have "LV (STAR r) s \<subseteq> {Stars []} \<union> f ` (S1 \<times> S2)"
+ unfolding S1_def S2_def f_def
+ unfolding LV_def image_def prefix_def strict_suffix_def
+ apply(auto)
+ apply(case_tac x)
+ apply(auto elim: Prf_elims)
+ apply(erule Prf_elims)
+ apply(auto)
+ apply(case_tac vs)
+ apply(auto intro: Prf.intros)
+ apply(rule exI)
+ apply(rule conjI)
+ apply(rule_tac x="flat a" in exI)
+ apply(rule conjI)
+ apply(rule_tac x="flats list" in exI)
+ apply(simp)
+ apply(blast)
+ apply(simp add: suffix_def)
+ using Prf.intros(6) by blast
+ ultimately
+ show "finite (LV (STAR r) s)" by (simp add: finite_subset)
+qed
+
+
+lemma LV_finite:
+ shows "finite (LV r s)"
+proof(induct r arbitrary: s)
+ case (ZERO s)
+ show "finite (LV ZERO s)" by (simp add: LV_simps)
+next
+ case (ONE s)
+ show "finite (LV ONE s)" by (simp add: LV_simps)
+next
+ case (CH c s)
+ show "finite (LV (CH c) s)" by (simp add: LV_simps)
+next
+ case (ALT r1 r2 s)
+ then show "finite (LV (ALT r1 r2) s)" by (simp add: LV_simps)
+next
+ case (SEQ r1 r2 s)
+ define f where "f \<equiv> \<lambda>(v1, v2). Seq v1 v2"
+ define S1 where "S1 \<equiv> \<Union>s' \<in> Prefixes s. LV r1 s'"
+ define S2 where "S2 \<equiv> \<Union>s' \<in> Suffixes s. LV r2 s'"
+ have IHs: "\<And>s. finite (LV r1 s)" "\<And>s. finite (LV r2 s)" by fact+
+ then have "finite S1" "finite S2" unfolding S1_def S2_def
+ by (simp_all add: finite_Prefixes finite_Suffixes)
+ moreover
+ have "LV (SEQ r1 r2) s \<subseteq> f ` (S1 \<times> S2)"
+ unfolding f_def S1_def S2_def
+ unfolding LV_def image_def prefix_def suffix_def
+ apply (auto elim!: Prf_elims)
+ by (metis (mono_tags, lifting) mem_Collect_eq)
+ ultimately
+ show "finite (LV (SEQ r1 r2) s)"
+ by (simp add: finite_subset)
+next
+ case (STAR r s)
+ then show "finite (LV (STAR r) s)" by (simp add: LV_STAR_finite)
+qed
+
+
+
+section \<open>Our inductive POSIX Definition\<close>
+
+inductive
+ Posix :: "string \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<in> _ \<rightarrow> _" [100, 100, 100] 100)
+where
+ Posix_ONE: "[] \<in> ONE \<rightarrow> Void"
+| Posix_CH: "[c] \<in> (CH c) \<rightarrow> (Char c)"
+| Posix_ALT1: "s \<in> r1 \<rightarrow> v \<Longrightarrow> s \<in> (ALT r1 r2) \<rightarrow> (Left v)"
+| Posix_ALT2: "\<lbrakk>s \<in> r2 \<rightarrow> v; s \<notin> L(r1)\<rbrakk> \<Longrightarrow> s \<in> (ALT r1 r2) \<rightarrow> (Right v)"
+| Posix_SEQ: "\<lbrakk>s1 \<in> r1 \<rightarrow> v1; s2 \<in> r2 \<rightarrow> v2;
+ \<not>(\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (s1 @ s\<^sub>3) \<in> L r1 \<and> s\<^sub>4 \<in> L r2)\<rbrakk> \<Longrightarrow>
+ (s1 @ s2) \<in> (SEQ r1 r2) \<rightarrow> (Seq v1 v2)"
+| Posix_STAR1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> STAR r \<rightarrow> Stars vs; flat v \<noteq> [];
+ \<not>(\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (s1 @ s\<^sub>3) \<in> L r \<and> s\<^sub>4 \<in> L (STAR r))\<rbrakk>
+ \<Longrightarrow> (s1 @ s2) \<in> STAR r \<rightarrow> Stars (v # vs)"
+| Posix_STAR2: "[] \<in> STAR r \<rightarrow> Stars []"
+
+inductive_cases Posix_elims:
+ "s \<in> ZERO \<rightarrow> v"
+ "s \<in> ONE \<rightarrow> v"
+ "s \<in> CH c \<rightarrow> v"
+ "s \<in> ALT r1 r2 \<rightarrow> v"
+ "s \<in> SEQ r1 r2 \<rightarrow> v"
+ "s \<in> STAR r \<rightarrow> v"
+
+lemma Posix1:
+ assumes "s \<in> r \<rightarrow> v"
+ shows "s \<in> L r" "flat v = s"
+using assms
+ by(induct s r v rule: Posix.induct)
+ (auto simp add: Sequ_def)
+
+text \<open>
+ For a give value and string, our Posix definition
+ determines a unique value.
+\<close>
+
+lemma Posix_determ:
+ assumes "s \<in> r \<rightarrow> v1" "s \<in> r \<rightarrow> v2"
+ shows "v1 = v2"
+using assms
+proof (induct s r v1 arbitrary: v2 rule: Posix.induct)
+ case (Posix_ONE v2)
+ have "[] \<in> ONE \<rightarrow> v2" by fact
+ then show "Void = v2" by cases auto
+next
+ case (Posix_CH c v2)
+ have "[c] \<in> CH c \<rightarrow> v2" by fact
+ then show "Char c = v2" by cases auto
+next
+ case (Posix_ALT1 s r1 v r2 v2)
+ have "s \<in> ALT r1 r2 \<rightarrow> v2" by fact
+ moreover
+ have "s \<in> r1 \<rightarrow> v" by fact
+ then have "s \<in> L r1" by (simp add: Posix1)
+ ultimately obtain v' where eq: "v2 = Left v'" "s \<in> r1 \<rightarrow> v'" by cases auto
+ moreover
+ have IH: "\<And>v2. s \<in> r1 \<rightarrow> v2 \<Longrightarrow> v = v2" by fact
+ ultimately have "v = v'" by simp
+ then show "Left v = v2" using eq by simp
+next
+ case (Posix_ALT2 s r2 v r1 v2)
+ have "s \<in> ALT r1 r2 \<rightarrow> v2" by fact
+ moreover
+ have "s \<notin> L r1" by fact
+ ultimately obtain v' where eq: "v2 = Right v'" "s \<in> r2 \<rightarrow> v'"
+ by cases (auto simp add: Posix1)
+ moreover
+ have IH: "\<And>v2. s \<in> r2 \<rightarrow> v2 \<Longrightarrow> v = v2" by fact
+ ultimately have "v = v'" by simp
+ then show "Right v = v2" using eq by simp
+next
+ case (Posix_SEQ s1 r1 v1 s2 r2 v2 v')
+ have "(s1 @ s2) \<in> SEQ r1 r2 \<rightarrow> v'"
+ "s1 \<in> r1 \<rightarrow> v1" "s2 \<in> r2 \<rightarrow> v2"
+ "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L r1 \<and> s\<^sub>4 \<in> L r2)" by fact+
+ then obtain v1' v2' where "v' = Seq v1' v2'" "s1 \<in> r1 \<rightarrow> v1'" "s2 \<in> r2 \<rightarrow> v2'"
+ apply(cases) apply (auto simp add: append_eq_append_conv2)
+ using Posix1(1) by fastforce+
+ moreover
+ have IHs: "\<And>v1'. s1 \<in> r1 \<rightarrow> v1' \<Longrightarrow> v1 = v1'"
+ "\<And>v2'. s2 \<in> r2 \<rightarrow> v2' \<Longrightarrow> v2 = v2'" by fact+
+ ultimately show "Seq v1 v2 = v'" by simp
+next
+ case (Posix_STAR1 s1 r v s2 vs v2)
+ have "(s1 @ s2) \<in> STAR r \<rightarrow> v2"
+ "s1 \<in> r \<rightarrow> v" "s2 \<in> STAR r \<rightarrow> Stars vs" "flat v \<noteq> []"
+ "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (STAR r))" by fact+
+ then obtain v' vs' where "v2 = Stars (v' # vs')" "s1 \<in> r \<rightarrow> v'" "s2 \<in> (STAR r) \<rightarrow> (Stars vs')"
+ apply(cases) apply (auto simp add: append_eq_append_conv2)
+ using Posix1(1) apply fastforce
+ apply (metis Posix1(1) Posix_STAR1.hyps(6) append_Nil append_Nil2)
+ using Posix1(2) by blast
+ moreover
+ have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2"
+ "\<And>v2. s2 \<in> STAR r \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+
+ ultimately show "Stars (v # vs) = v2" by auto
+next
+ case (Posix_STAR2 r v2)
+ have "[] \<in> STAR r \<rightarrow> v2" by fact
+ then show "Stars [] = v2" by cases (auto simp add: Posix1)
+qed
+
+
+text \<open>
+ Our POSIX values are lexical values.
+\<close>
+
+lemma Posix_LV:
+ assumes "s \<in> r \<rightarrow> v"
+ shows "v \<in> LV r s"
+ using assms unfolding LV_def
+ apply(induct rule: Posix.induct)
+ apply(auto simp add: intro!: Prf.intros elim!: Prf_elims)
+ done
+
+lemma Posix_Prf:
+ assumes "s \<in> r \<rightarrow> v"
+ shows "\<Turnstile> v : r"
+ using assms Posix_LV LV_def
+ by simp
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/thys3/RegLangs.thy Wed Jun 29 12:38:05 2022 +0100
@@ -0,0 +1,237 @@
+
+theory RegLangs
+ imports Main "HOL-Library.Sublist"
+begin
+
+section \<open>Sequential Composition of Languages\<close>
+
+definition
+ Sequ :: "string set \<Rightarrow> string set \<Rightarrow> string set" ("_ ;; _" [100,100] 100)
+where
+ "A ;; B = {s1 @ s2 | s1 s2. s1 \<in> A \<and> s2 \<in> B}"
+
+text \<open>Two Simple Properties about Sequential Composition\<close>
+
+lemma Sequ_empty_string [simp]:
+ shows "A ;; {[]} = A"
+ and "{[]} ;; A = A"
+by (simp_all add: Sequ_def)
+
+lemma Sequ_empty [simp]:
+ shows "A ;; {} = {}"
+ and "{} ;; A = {}"
+ by (simp_all add: Sequ_def)
+
+
+section \<open>Semantic Derivative (Left Quotient) of Languages\<close>
+
+definition
+ Der :: "char \<Rightarrow> string set \<Rightarrow> string set"
+where
+ "Der c A \<equiv> {s. c # s \<in> A}"
+
+definition
+ Ders :: "string \<Rightarrow> string set \<Rightarrow> string set"
+where
+ "Ders s A \<equiv> {s'. s @ s' \<in> A}"
+
+lemma Der_null [simp]:
+ shows "Der c {} = {}"
+unfolding Der_def
+by auto
+
+lemma Der_empty [simp]:
+ shows "Der c {[]} = {}"
+unfolding Der_def
+by auto
+
+lemma Der_char [simp]:
+ shows "Der c {[d]} = (if c = d then {[]} else {})"
+unfolding Der_def
+by auto
+
+lemma Der_union [simp]:
+ shows "Der c (A \<union> B) = Der c A \<union> Der c B"
+unfolding Der_def
+by auto
+
+lemma Der_Sequ [simp]:
+ shows "Der c (A ;; B) = (Der c A) ;; B \<union> (if [] \<in> A then Der c B else {})"
+unfolding Der_def Sequ_def
+by (auto simp add: Cons_eq_append_conv)
+
+
+section \<open>Kleene Star for Languages\<close>
+
+inductive_set
+ Star :: "string set \<Rightarrow> string set" ("_\<star>" [101] 102)
+ for A :: "string set"
+where
+ start[intro]: "[] \<in> A\<star>"
+| step[intro]: "\<lbrakk>s1 \<in> A; s2 \<in> A\<star>\<rbrakk> \<Longrightarrow> s1 @ s2 \<in> A\<star>"
+
+(* Arden's lemma *)
+
+lemma Star_cases:
+ shows "A\<star> = {[]} \<union> A ;; A\<star>"
+unfolding Sequ_def
+by (auto) (metis Star.simps)
+
+lemma Star_decomp:
+ assumes "c # x \<in> A\<star>"
+ shows "\<exists>s1 s2. x = s1 @ s2 \<and> c # s1 \<in> A \<and> s2 \<in> A\<star>"
+using assms
+by (induct x\<equiv>"c # x" rule: Star.induct)
+ (auto simp add: append_eq_Cons_conv)
+
+lemma Star_Der_Sequ:
+ shows "Der c (A\<star>) \<subseteq> (Der c A) ;; A\<star>"
+unfolding Der_def Sequ_def
+by(auto simp add: Star_decomp)
+
+
+lemma Der_star[simp]:
+ shows "Der c (A\<star>) = (Der c A) ;; A\<star>"
+proof -
+ have "Der c (A\<star>) = Der c ({[]} \<union> A ;; A\<star>)"
+ by (simp only: Star_cases[symmetric])
+ also have "... = Der c (A ;; A\<star>)"
+ by (simp only: Der_union Der_empty) (simp)
+ also have "... = (Der c A) ;; A\<star> \<union> (if [] \<in> A then Der c (A\<star>) else {})"
+ by simp
+ also have "... = (Der c A) ;; A\<star>"
+ using Star_Der_Sequ by auto
+ finally show "Der c (A\<star>) = (Der c A) ;; A\<star>" .
+qed
+
+lemma Star_concat:
+ assumes "\<forall>s \<in> set ss. s \<in> A"
+ shows "concat ss \<in> A\<star>"
+using assms by (induct ss) (auto)
+
+lemma Star_split:
+ assumes "s \<in> A\<star>"
+ shows "\<exists>ss. concat ss = s \<and> (\<forall>s \<in> set ss. s \<in> A \<and> s \<noteq> [])"
+using assms
+ apply(induct rule: Star.induct)
+ using concat.simps(1) apply fastforce
+ apply(clarify)
+ by (metis append_Nil concat.simps(2) set_ConsD)
+
+
+
+section \<open>Regular Expressions\<close>
+
+datatype rexp =
+ ZERO
+| ONE
+| CH char
+| SEQ rexp rexp
+| ALT rexp rexp
+| STAR rexp
+
+section \<open>Semantics of Regular Expressions\<close>
+
+fun
+ L :: "rexp \<Rightarrow> string set"
+where
+ "L (ZERO) = {}"
+| "L (ONE) = {[]}"
+| "L (CH c) = {[c]}"
+| "L (SEQ r1 r2) = (L r1) ;; (L r2)"
+| "L (ALT r1 r2) = (L r1) \<union> (L r2)"
+| "L (STAR r) = (L r)\<star>"
+
+
+section \<open>Nullable, Derivatives\<close>
+
+fun
+ nullable :: "rexp \<Rightarrow> bool"
+where
+ "nullable (ZERO) = False"
+| "nullable (ONE) = True"
+| "nullable (CH c) = False"
+| "nullable (ALT r1 r2) = (nullable r1 \<or> nullable r2)"
+| "nullable (SEQ r1 r2) = (nullable r1 \<and> nullable r2)"
+| "nullable (STAR r) = True"
+
+
+fun
+ der :: "char \<Rightarrow> rexp \<Rightarrow> rexp"
+where
+ "der c (ZERO) = ZERO"
+| "der c (ONE) = ZERO"
+| "der c (CH d) = (if c = d then ONE else ZERO)"
+| "der c (ALT r1 r2) = ALT (der c r1) (der c r2)"
+| "der c (SEQ r1 r2) =
+ (if nullable r1
+ then ALT (SEQ (der c r1) r2) (der c r2)
+ else SEQ (der c r1) r2)"
+| "der c (STAR r) = SEQ (der c r) (STAR r)"
+
+fun
+ ders :: "string \<Rightarrow> rexp \<Rightarrow> rexp"
+where
+ "ders [] r = r"
+| "ders (c # s) r = ders s (der c r)"
+
+
+lemma nullable_correctness:
+ shows "nullable r \<longleftrightarrow> [] \<in> (L r)"
+by (induct r) (auto simp add: Sequ_def)
+
+lemma der_correctness:
+ shows "L (der c r) = Der c (L r)"
+by (induct r) (simp_all add: nullable_correctness)
+
+lemma ders_correctness:
+ shows "L (ders s r) = Ders s (L r)"
+ by (induct s arbitrary: r)
+ (simp_all add: Ders_def der_correctness Der_def)
+
+lemma ders_append:
+ shows "ders (s1 @ s2) r = ders s2 (ders s1 r)"
+ by (induct s1 arbitrary: s2 r) (auto)
+
+lemma ders_snoc:
+ shows "ders (s @ [c]) r = der c (ders s r)"
+ by (simp add: ders_append)
+
+
+(*
+datatype ctxt =
+ SeqC rexp bool
+ | AltCL rexp
+ | AltCH rexp
+ | StarC rexp
+
+function
+ down :: "char \<Rightarrow> rexp \<Rightarrow> ctxt list \<Rightarrow> rexp * ctxt list"
+and up :: "char \<Rightarrow> rexp \<Rightarrow> ctxt list \<Rightarrow> rexp * ctxt list"
+where
+ "down c (SEQ r1 r2) ctxts =
+ (if (nullable r1) then down c r1 (SeqC r2 True # ctxts)
+ else down c r1 (SeqC r2 False # ctxts))"
+| "down c (CH d) ctxts =
+ (if c = d then up c ONE ctxts else up c ZERO ctxts)"
+| "down c ONE ctxts = up c ZERO ctxts"
+| "down c ZERO ctxts = up c ZERO ctxts"
+| "down c (ALT r1 r2) ctxts = down c r1 (AltCH r2 # ctxts)"
+| "down c (STAR r1) ctxts = down c r1 (StarC r1 # ctxts)"
+| "up c r [] = (r, [])"
+| "up c r (SeqC r2 False # ctxts) = up c (SEQ r r2) ctxts"
+| "up c r (SeqC r2 True # ctxts) = down c r2 (AltCL (SEQ r r2) # ctxts)"
+| "up c r (AltCL r1 # ctxts) = up c (ALT r1 r) ctxts"
+| "up c r (AltCH r2 # ctxts) = down c r2 (AltCL r # ctxts)"
+| "up c r (StarC r1 # ctxts) = up c (SEQ r (STAR r1)) ctxts"
+ apply(pat_completeness)
+ apply(auto)
+ done
+
+termination
+ sorry
+
+*)
+
+
+end
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/thys3/RfltsRdistinctProps.thy Wed Jun 29 12:38:05 2022 +0100
@@ -0,0 +1,355 @@
+theory RfltsRdistinctProps imports "Rsimp"
+begin
+
+
+
+lemma all_that_same_elem:
+ shows "\<lbrakk> a \<in> rset; rdistinct rs {a} = []\<rbrakk>
+ \<Longrightarrow> rdistinct (rs @ rsb) rset = rdistinct rsb rset"
+ apply(induct rs)
+ apply simp
+ apply(subgoal_tac "aa = a")
+ apply simp
+ by (metis empty_iff insert_iff list.discI rdistinct.simps(2))
+
+
+lemma rdistinct1:
+ assumes "a \<in> acc"
+ shows "a \<notin> set (rdistinct rs acc)"
+ using assms
+ apply(induct rs arbitrary: acc a)
+ apply(auto)
+ done
+
+
+lemma rdistinct_does_the_job:
+ shows "distinct (rdistinct rs s)"
+ apply(induct rs s rule: rdistinct.induct)
+ apply(auto simp add: rdistinct1)
+ done
+
+
+
+lemma rdistinct_concat:
+ assumes "set rs \<subseteq> rset"
+ shows "rdistinct (rs @ rsa) rset = rdistinct rsa rset"
+ using assms
+ apply(induct rs)
+ apply simp+
+ done
+
+lemma distinct_not_exist:
+ assumes "a \<notin> set rs"
+ shows "rdistinct rs rset = rdistinct rs (insert a rset)"
+ using assms
+ apply(induct rs arbitrary: rset)
+ apply(auto)
+ done
+
+lemma rdistinct_on_distinct:
+ shows "distinct rs \<Longrightarrow> rdistinct rs {} = rs"
+ apply(induct rs)
+ apply simp
+ using distinct_not_exist by fastforce
+
+lemma distinct_rdistinct_append:
+ assumes "distinct rs1" "\<forall>r \<in> set rs1. r \<notin> acc"
+ shows "rdistinct (rs1 @ rsa) acc = rs1 @ (rdistinct rsa (acc \<union> set rs1))"
+ using assms
+ apply(induct rs1 arbitrary: rsa acc)
+ apply(auto)[1]
+ apply(auto)[1]
+ apply(drule_tac x="rsa" in meta_spec)
+ apply(drule_tac x="{a} \<union> acc" in meta_spec)
+ apply(simp)
+ apply(drule meta_mp)
+ apply(auto)[1]
+ apply(simp)
+ done
+
+
+lemma rdistinct_set_equality1:
+ shows "set (rdistinct rs acc) = set rs - acc"
+ apply(induct rs acc rule: rdistinct.induct)
+ apply(auto)
+ done
+
+
+lemma rdistinct_set_equality:
+ shows "set (rdistinct rs {}) = set rs"
+ by (simp add: rdistinct_set_equality1)
+
+
+
+lemma distinct_removes_last:
+ shows "\<lbrakk>a \<in> set as\<rbrakk>
+ \<Longrightarrow> rdistinct as rset = rdistinct (as @ [a]) rset"
+and "rdistinct (ab # as @ [ab]) rset1 = rdistinct (ab # as) rset1"
+ apply(induct as arbitrary: rset ab rset1 a)
+ apply simp
+ apply simp
+ apply(case_tac "aa \<in> rset")
+ apply(case_tac "a = aa")
+ apply (metis append_Cons)
+ apply simp
+ apply(case_tac "a \<in> set as")
+ apply (metis append_Cons rdistinct.simps(2) set_ConsD)
+ apply(case_tac "a = aa")
+ prefer 2
+ apply simp
+ apply (metis append_Cons)
+ apply(case_tac "ab \<in> rset1")
+ prefer 2
+ apply(subgoal_tac "rdistinct (ab # (a # as) @ [ab]) rset1 =
+ ab # (rdistinct ((a # as) @ [ab]) (insert ab rset1))")
+ prefer 2
+ apply force
+ apply(simp only:)
+ apply(subgoal_tac "rdistinct (ab # a # as) rset1 = ab # (rdistinct (a # as) (insert ab rset1))")
+ apply(simp only:)
+ apply(subgoal_tac "rdistinct ((a # as) @ [ab]) (insert ab rset1) = rdistinct (a # as) (insert ab rset1)")
+ apply blast
+ apply(case_tac "a \<in> insert ab rset1")
+ apply simp
+ apply (metis insertI1)
+ apply simp
+ apply (meson insertI1)
+ apply simp
+ apply(subgoal_tac "rdistinct ((a # as) @ [ab]) rset1 = rdistinct (a # as) rset1")
+ apply simp
+ by (metis append_Cons insert_iff insert_is_Un rdistinct.simps(2))
+
+
+lemma distinct_removes_middle:
+ shows "\<lbrakk>a \<in> set as\<rbrakk>
+ \<Longrightarrow> rdistinct (as @ as2) rset = rdistinct (as @ [a] @ as2) rset"
+and "rdistinct (ab # as @ [ab] @ as3) rset1 = rdistinct (ab # as @ as3) rset1"
+ apply(induct as arbitrary: rset rset1 ab as2 as3 a)
+ apply simp
+ apply simp
+ apply(case_tac "a \<in> rset")
+ apply simp
+ apply metis
+ apply simp
+ apply (metis insertI1)
+ apply(case_tac "a = ab")
+ apply simp
+ apply(case_tac "ab \<in> rset")
+ apply simp
+ apply presburger
+ apply (meson insertI1)
+ apply(case_tac "a \<in> rset")
+ apply (metis (no_types, opaque_lifting) Un_insert_left append_Cons insert_iff rdistinct.simps(2) sup_bot_left)
+ apply(case_tac "ab \<in> rset")
+ apply simp
+ apply (meson insert_iff)
+ apply simp
+ by (metis insertI1)
+
+
+lemma k0b:
+ assumes "nonalt r" "r \<noteq> RZERO"
+ shows "rflts [r] = [r]"
+ using assms
+ apply(case_tac r)
+ apply(simp_all)
+ done
+
+lemma rflts_def_idiot:
+ shows "\<lbrakk> a \<noteq> RZERO; \<nexists>rs1. a = RALTS rs1\<rbrakk> \<Longrightarrow> rflts (a # rs) = a # rflts rs"
+ apply(case_tac a)
+ apply simp_all
+ done
+
+lemma flts_middle0:
+ shows "rflts (rsa @ RZERO # rsb) = rflts (rsa @ rsb)"
+ apply(induct rsa)
+ apply simp
+ by (metis append_Cons rflts.simps(2) rflts.simps(3) rflts_def_idiot)
+
+
+lemma flts_removes0:
+ shows " rflts (rs @ [RZERO]) =
+ rflts rs"
+ apply(induct rs)
+ apply simp
+ by (metis append_Cons rflts.simps(2) rflts.simps(3) rflts_def_idiot)
+
+lemma rflts_spills_last:
+ shows "rflts (rs1 @ [RALTS rs]) = rflts rs1 @ rs"
+ apply (induct rs1 rule: rflts.induct)
+ apply(auto)
+ done
+
+lemma flts_keeps1:
+ shows "rflts (rs @ [RONE]) = rflts rs @ [RONE]"
+ apply (induct rs rule: rflts.induct)
+ apply(auto)
+ done
+
+lemma flts_keeps_others:
+ shows "\<lbrakk>a \<noteq> RZERO; \<nexists>rs1. a = RALTS rs1\<rbrakk> \<Longrightarrow>rflts (rs @ [a]) = rflts rs @ [a]"
+ apply(induct rs rule: rflts.induct)
+ apply(auto)
+ by (meson k0b nonalt.elims(3))
+
+lemma spilled_alts_contained:
+ shows "\<lbrakk>a = RALTS rs ; a \<in> set rs1\<rbrakk> \<Longrightarrow> \<forall>r \<in> set rs. r \<in> set (rflts rs1)"
+ apply(induct rs1)
+ apply simp
+ apply(case_tac "a = aa")
+ apply simp
+ apply(subgoal_tac " a \<in> set rs1")
+ prefer 2
+ apply (meson set_ConsD)
+ apply(case_tac aa)
+ using rflts.simps(2) apply presburger
+ apply fastforce
+ apply fastforce
+ apply fastforce
+ apply fastforce
+ by fastforce
+
+
+lemma rflts_def_idiot2:
+ shows "\<lbrakk>a \<noteq> RZERO; \<nexists>rs1. a = RALTS rs1; a \<in> set rs\<rbrakk> \<Longrightarrow> a \<in> set (rflts rs)"
+ apply(induct rs rule: rflts.induct)
+ apply(auto)
+ done
+
+lemma flts_append:
+ shows "rflts (rs1 @ rs2) = rflts rs1 @ rflts rs2"
+ apply(induct rs1)
+ apply simp
+ apply(case_tac a)
+ apply simp+
+ done
+lemma distinct_removes_middle3:
+ shows "\<lbrakk>a \<in> set as\<rbrakk>
+ \<Longrightarrow> rdistinct (as @ a #as2) rset = rdistinct (as @ as2) rset"
+ using distinct_removes_middle(1) by fastforce
+
+
+lemma distinct_removes_list:
+ shows "\<lbrakk> \<forall>r \<in> set rs. r \<in> set as\<rbrakk> \<Longrightarrow> rdistinct (as @ rs) {} = rdistinct as {}"
+ apply(induct rs)
+ apply simp+
+ apply(subgoal_tac "rdistinct (as @ a # rs) {} = rdistinct (as @ rs) {}")
+ prefer 2
+ apply (metis append_Cons append_Nil distinct_removes_middle(1))
+ by presburger
+
+lemma last_elem_out:
+ shows "\<lbrakk>x \<notin> set xs; x \<notin> rset \<rbrakk> \<Longrightarrow> rdistinct (xs @ [x]) rset = rdistinct xs rset @ [x]"
+ apply(induct xs arbitrary: rset)
+ apply simp+
+ done
+
+
+lemma rdistinct_concat_general:
+ shows "rdistinct (rs1 @ rs2) {} = (rdistinct rs1 {}) @ (rdistinct rs2 (set rs1))"
+ apply(induct rs1 arbitrary: rs2 rule: rev_induct)
+ apply simp
+ apply(drule_tac x = "x # rs2" in meta_spec)
+ apply simp
+ apply(case_tac "x \<in> set xs")
+ apply simp
+
+ apply (simp add: distinct_removes_middle3 insert_absorb)
+ apply simp
+ by (simp add: last_elem_out)
+
+
+
+
+lemma distinct_once_enough:
+ shows "rdistinct (rs @ rsa) {} = rdistinct (rdistinct rs {} @ rsa) {}"
+ apply(subgoal_tac "distinct (rdistinct rs {})")
+ apply(subgoal_tac
+" rdistinct (rdistinct rs {} @ rsa) {} = rdistinct rs {} @ (rdistinct rsa (set rs))")
+ apply(simp only:)
+ using rdistinct_concat_general apply blast
+ apply (simp add: distinct_rdistinct_append rdistinct_set_equality1)
+ by (simp add: rdistinct_does_the_job)
+
+
+
+
+lemma distinct_removes_duplicate_flts:
+ shows " a \<in> set rsa
+ \<Longrightarrow> rdistinct (rflts (map rsimp rsa @ [rsimp a])) {} =
+ rdistinct (rflts (map rsimp rsa)) {}"
+ apply(subgoal_tac "rsimp a \<in> set (map rsimp rsa)")
+ prefer 2
+ apply simp
+ apply(induct "rsimp a")
+ apply simp
+ using flts_removes0 apply presburger
+ apply(subgoal_tac " rdistinct (rflts (map rsimp rsa @ [rsimp a])) {} =
+ rdistinct (rflts (map rsimp rsa @ [RONE])) {}")
+ apply (simp only:)
+ apply(subst flts_keeps1)
+ apply (metis distinct_removes_last(1) rflts_def_idiot2 rrexp.simps(20) rrexp.simps(6))
+ apply presburger
+ apply(subgoal_tac " rdistinct (rflts (map rsimp rsa @ [rsimp a])) {} =
+ rdistinct ((rflts (map rsimp rsa)) @ [RCHAR x]) {}")
+ apply (simp only:)
+ prefer 2
+ apply (metis flts_keeps_others rrexp.distinct(21) rrexp.distinct(3))
+ apply (metis distinct_removes_last(1) rflts_def_idiot2 rrexp.distinct(21) rrexp.distinct(3))
+
+ apply (metis distinct_removes_last(1) flts_keeps_others rflts_def_idiot2 rrexp.distinct(25) rrexp.distinct(5))
+ prefer 2
+ apply (metis distinct_removes_last(1) flts_keeps_others flts_removes0 rflts_def_idiot2 rrexp.distinct(29))
+ apply(subgoal_tac "rflts (map rsimp rsa @ [rsimp a]) = rflts (map rsimp rsa) @ x")
+ prefer 2
+ apply (simp add: rflts_spills_last)
+ apply(subgoal_tac "\<forall> r \<in> set x. r \<in> set (rflts (map rsimp rsa))")
+ prefer 2
+ apply (metis (mono_tags, lifting) image_iff image_set spilled_alts_contained)
+ apply (metis rflts_spills_last)
+ by (metis distinct_removes_list spilled_alts_contained)
+
+
+
+
+
+lemma distinct_early_app1:
+ shows "rset1 \<subseteq> rset \<Longrightarrow> rdistinct rs rset = rdistinct (rdistinct rs rset1) rset"
+ apply(induct rs arbitrary: rset rset1)
+ apply simp
+ apply simp
+ apply(case_tac "a \<in> rset1")
+ apply simp
+ apply(case_tac "a \<in> rset")
+ apply simp+
+
+ apply blast
+ apply(case_tac "a \<in> rset1")
+ apply simp+
+ apply(case_tac "a \<in> rset")
+ apply simp
+ apply (metis insert_subsetI)
+ apply simp
+ by (meson insert_mono)
+
+
+lemma distinct_early_app:
+ shows " rdistinct (rs @ rsb) rset = rdistinct (rdistinct rs {} @ rsb) rset"
+ apply(induct rsb)
+ apply simp
+ using distinct_early_app1 apply blast
+ by (metis distinct_early_app1 distinct_once_enough empty_subsetI)
+
+
+lemma distinct_eq_interesting1:
+ shows "a \<in> rset \<Longrightarrow> rdistinct (rs @ rsb) rset = rdistinct (rdistinct (a # rs) {} @ rsb) rset"
+ apply(subgoal_tac "rdistinct (rdistinct (a # rs) {} @ rsb) rset = rdistinct (rdistinct rs {} @ rsb) rset")
+ apply(simp only:)
+ using distinct_early_app apply blast
+ by (metis append_Cons distinct_early_app rdistinct.simps(2))
+
+
+
+
+end
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/thys3/Rsimp.thy Wed Jun 29 12:38:05 2022 +0100
@@ -0,0 +1,171 @@
+theory Rsimp imports "Lexer"
+begin
+
+datatype rrexp =
+ RZERO
+| RONE
+| RCHAR char
+| RSEQ rrexp rrexp
+| RALTS "rrexp list"
+| RSTAR rrexp
+
+abbreviation
+ "RALT r1 r2 \<equiv> RALTS [r1, r2]"
+
+
+fun
+ RL :: "rrexp \<Rightarrow> string set"
+where
+ "RL (RZERO) = {}"
+| "RL (RONE) = {[]}"
+| "RL (RCHAR c) = {[c]}"
+| "RL (RSEQ r1 r2) = (RL r1) ;; (RL r2)"
+| "RL (RALTS rs) = (\<Union> (set (map RL rs)))"
+| "RL (RSTAR r) = (RL r)\<star>"
+
+
+
+fun
+ rnullable :: "rrexp \<Rightarrow> bool"
+where
+ "rnullable (RZERO) = False"
+| "rnullable (RONE) = True"
+| "rnullable (RCHAR c) = False"
+| "rnullable (RALTS rs) = (\<exists>r \<in> set rs. rnullable r)"
+| "rnullable (RSEQ r1 r2) = (rnullable r1 \<and> rnullable r2)"
+| "rnullable (RSTAR r) = True"
+
+
+fun
+ rder :: "char \<Rightarrow> rrexp \<Rightarrow> rrexp"
+where
+ "rder c (RZERO) = RZERO"
+| "rder c (RONE) = RZERO"
+| "rder c (RCHAR d) = (if c = d then RONE else RZERO)"
+| "rder c (RALTS rs) = RALTS (map (rder c) rs)"
+| "rder c (RSEQ r1 r2) =
+ (if rnullable r1
+ then RALT (RSEQ (rder c r1) r2) (rder c r2)
+ else RSEQ (rder c r1) r2)"
+| "rder c (RSTAR r) = RSEQ (rder c r) (RSTAR r)"
+
+
+fun
+ rders :: "rrexp \<Rightarrow> string \<Rightarrow> rrexp"
+where
+ "rders r [] = r"
+| "rders r (c#s) = rders (rder c r) s"
+
+fun rdistinct :: "'a list \<Rightarrow>'a set \<Rightarrow> 'a list"
+ where
+ "rdistinct [] acc = []"
+| "rdistinct (x#xs) acc =
+ (if x \<in> acc then rdistinct xs acc
+ else x # (rdistinct xs ({x} \<union> acc)))"
+
+
+fun rflts :: "rrexp list \<Rightarrow> rrexp list"
+ where
+ "rflts [] = []"
+| "rflts (RZERO # rs) = rflts rs"
+| "rflts ((RALTS rs1) # rs) = rs1 @ rflts rs"
+| "rflts (r1 # rs) = r1 # rflts rs"
+
+fun nonalt :: "rrexp \<Rightarrow> bool"
+ where
+ "nonalt (RALTS rs) = False"
+| "nonalt r = True"
+
+fun rsimp_ALTs :: " rrexp list \<Rightarrow> rrexp"
+ where
+ "rsimp_ALTs [] = RZERO"
+| "rsimp_ALTs [r] = r"
+| "rsimp_ALTs rs = RALTS rs"
+
+fun rsimp_SEQ :: " rrexp \<Rightarrow> rrexp \<Rightarrow> rrexp"
+ where
+ "rsimp_SEQ RZERO _ = RZERO"
+| "rsimp_SEQ _ RZERO = RZERO"
+| "rsimp_SEQ RONE r2 = r2"
+| "rsimp_SEQ r1 r2 = RSEQ r1 r2"
+
+
+fun rsimp :: "rrexp \<Rightarrow> rrexp"
+ where
+ "rsimp (RSEQ r1 r2) = rsimp_SEQ (rsimp r1) (rsimp r2)"
+| "rsimp (RALTS rs) = rsimp_ALTs (rdistinct (rflts (map rsimp rs)) {}) "
+| "rsimp r = r"
+
+
+fun
+ rders_simp :: "rrexp \<Rightarrow> string \<Rightarrow> rrexp"
+where
+ "rders_simp r [] = r"
+| "rders_simp r (c#s) = rders_simp (rsimp (rder c r)) s"
+
+fun rsize :: "rrexp \<Rightarrow> nat" where
+ "rsize RZERO = 1"
+| "rsize (RONE) = 1"
+| "rsize (RCHAR c) = 1"
+| "rsize (RALTS rs) = Suc (sum_list (map rsize rs))"
+| "rsize (RSEQ r1 r2) = Suc (rsize r1 + rsize r2)"
+| "rsize (RSTAR r) = Suc (rsize r)"
+
+abbreviation rsizes where
+ "rsizes rs \<equiv> sum_list (map rsize rs)"
+
+fun nonnested :: "rrexp \<Rightarrow> bool"
+ where
+ "nonnested (RALTS []) = True"
+| "nonnested (RALTS ((RALTS rs1) # rs2)) = False"
+| "nonnested (RALTS (r # rs2)) = nonnested (RALTS rs2)"
+| "nonnested r = True"
+
+
+fun good :: "rrexp \<Rightarrow> bool" where
+ "good RZERO = False"
+| "good (RONE) = True"
+| "good (RCHAR c) = True"
+| "good (RALTS []) = False"
+| "good (RALTS [r]) = False"
+| "good (RALTS (r1 # r2 # rs)) =
+ ((distinct ( (r1 # r2 # rs))) \<and>
+ (\<forall>r' \<in> set (r1 # r2 # rs). good r' \<and> nonalt r'))"
+| "good (RSEQ RZERO _) = False"
+| "good (RSEQ RONE _) = False"
+| "good (RSEQ _ RZERO) = False"
+| "good (RSEQ r1 r2) = (good r1 \<and> good r2)"
+| "good (RSTAR r) = True"
+
+fun nonazero :: "rrexp \<Rightarrow> bool"
+ where
+ "nonazero RZERO = False"
+| "nonazero r = True"
+
+
+
+
+
+
+lemma basic_rsimp_SEQ_property1:
+ shows "rsimp_SEQ RONE r = r"
+ apply(induct r)
+ apply simp+
+ done
+
+
+lemma basic_rsimp_SEQ_property3:
+ shows "rsimp_SEQ r RZERO = RZERO"
+ using rsimp_SEQ.elims by blast
+
+
+lemma rsimpalts_conscons:
+ shows "rsimp_ALTs (r1 # rsa @ r2 # rsb) = RALTS (r1 # rsa @ r2 # rsb)"
+ by (metis Nil_is_append_conv list.exhaust rsimp_ALTs.simps(3))
+
+lemma rsimp_alts_equal:
+ shows "rsimp_ALTs (rsa @ a # rsb @ a # rsc) = RALTS (rsa @ a # rsb @ a # rsc) "
+ by (metis append_Cons append_Nil neq_Nil_conv rsimpalts_conscons)
+
+
+end
\ No newline at end of file