3   imports Main 

     3   imports Spec 

     7 section {* Sequential Composition of Languages *}

     7 section {* The Lexer Functions by Sulzmann and Lu  *}

     8 

     9 definition

    10   Sequ :: "string set \<Rightarrow> string set \<Rightarrow> string set" ("_ ;; _" [100,100] 100)

    11 where 

    12   "A ;; B = {s1 @ s2 | s1 s2. s1 \<in> A \<and> s2 \<in> B}"

    13 

    14 text {* Two Simple Properties about Sequential Composition *}

    15 

    16 lemma Sequ_empty_string [simp]:

    17   shows "A ;; {[]} = A"

    18   and   "{[]} ;; A = A"

    19 by (simp_all add: Sequ_def)

    20 

    21 lemma Sequ_empty [simp]:

    22   shows "A ;; {} = {}"

    23   and   "{} ;; A = {}"

    24 by (simp_all add: Sequ_def)

    25 

    26 

    27 section {* Semantic Derivative (Left Quotient) of Languages *}

    28 

    29 definition

    30   Der :: "char \<Rightarrow> string set \<Rightarrow> string set"

    31 where

    32   "Der c A \<equiv> {s. c # s \<in> A}"

    33 

    34 definition

    35   Ders :: "string \<Rightarrow> string set \<Rightarrow> string set"

    36 where

    37   "Ders s A \<equiv> {s'. s @ s' \<in> A}"

    38 

    39 lemma Der_null [simp]:

    40   shows "Der c {} = {}"

    41 unfolding Der_def

    42 by auto

    43 

    44 lemma Der_empty [simp]:

    45   shows "Der c {[]} = {}"

    46 unfolding Der_def

    47 by auto

    48 

    49 lemma Der_char [simp]:

    50   shows "Der c {[d]} = (if c = d then {[]} else {})"

    51 unfolding Der_def

    52 by auto

    53 

    54 lemma Der_union [simp]:

    55   shows "Der c (A \<union> B) = Der c A \<union> Der c B"

    56 unfolding Der_def

    57 by auto

    58 

    59 lemma Der_Sequ [simp]:

    60   shows "Der c (A ;; B) = (Der c A) ;; B \<union> (if [] \<in> A then Der c B else {})"

    61 unfolding Der_def Sequ_def

    62 by (auto simp add: Cons_eq_append_conv)

    63 

    64 

    65 section {* Kleene Star for Languages *}

    66 

    67 inductive_set

    68   Star :: "string set \<Rightarrow> string set" ("_\<star>" [101] 102)

    69   for A :: "string set"

    70 where

    71   start[intro]: "[] \<in> A\<star>"

    72 | step[intro]:  "\<lbrakk>s1 \<in> A; s2 \<in> A\<star>\<rbrakk> \<Longrightarrow> s1 @ s2 \<in> A\<star>"

    73 

    74 (* Arden's lemma *)

    75 

    76 lemma Star_cases:

    77   shows "A\<star> = {[]} \<union> A ;; A\<star>"

    78 unfolding Sequ_def

    79 by (auto) (metis Star.simps)

    80 

    81 lemma Star_decomp: 

    82   assumes "c # x \<in> A\<star>" 

    83   shows "\<exists>s1 s2. x = s1 @ s2 \<and> c # s1 \<in> A \<and> s2 \<in> A\<star>"

    84 using assms

    85 by (induct x\<equiv>"c # x" rule: Star.induct) 

    86    (auto simp add: append_eq_Cons_conv)

    87 

    88 lemma Star_Der_Sequ: 

    89   shows "Der c (A\<star>) \<subseteq> (Der c A) ;; A\<star>"

    90 unfolding Der_def

    91 apply(rule subsetI)

    92 apply(simp)

    93 unfolding Sequ_def

    94 apply(simp)

    95 by(auto simp add: Sequ_def Star_decomp)

    96 

    97 

    98 lemma Der_star [simp]:

    99   shows "Der c (A\<star>) = (Der c A) ;; A\<star>"

   100 proof -    

   101   have "Der c (A\<star>) = Der c ({[]} \<union> A ;; A\<star>)"  

   102     by (simp only: Star_cases[symmetric])

   103   also have "... = Der c (A ;; A\<star>)"

   104     by (simp only: Der_union Der_empty) (simp)

   105   also have "... = (Der c A) ;; A\<star> \<union> (if [] \<in> A then Der c (A\<star>) else {})"

   106     by simp

   107   also have "... =  (Der c A) ;; A\<star>"

   108     using Star_Der_Sequ by auto

   109   finally show "Der c (A\<star>) = (Der c A) ;; A\<star>" .

   110 qed

   111 

   112 

   113 section {* Regular Expressions *}

   114 

   115 datatype rexp =

   116   ZERO

   117 | ONE

   118 | CHAR char

   119 | SEQ rexp rexp

   120 | ALT rexp rexp

   121 | STAR rexp

   122 

   123 section {* Semantics of Regular Expressions *}

   124  

   125 fun

   126   L :: "rexp \<Rightarrow> string set"

   127 where

   128   "L (ZERO) = {}"

   129 | "L (ONE) = {[]}"

   130 | "L (CHAR c) = {[c]}"

   131 | "L (SEQ r1 r2) = (L r1) ;; (L r2)"

   132 | "L (ALT r1 r2) = (L r1) \<union> (L r2)"

   133 | "L (STAR r) = (L r)\<star>"

   134 

   135 

   136 section {* Nullable, Derivatives *}

   137 

   138 fun

   139  nullable :: "rexp \<Rightarrow> bool"

   140 where

   141   "nullable (ZERO) = False"

   142 | "nullable (ONE) = True"

   143 | "nullable (CHAR c) = False"

   144 | "nullable (ALT r1 r2) = (nullable r1 \<or> nullable r2)"

   145 | "nullable (SEQ r1 r2) = (nullable r1 \<and> nullable r2)"

   146 | "nullable (STAR r) = True"

   147 

   148 

   149 fun

   150  der :: "char \<Rightarrow> rexp \<Rightarrow> rexp"

   151 where

   152   "der c (ZERO) = ZERO"

   153 | "der c (ONE) = ZERO"

   154 | "der c (CHAR d) = (if c = d then ONE else ZERO)"

   155 | "der c (ALT r1 r2) = ALT (der c r1) (der c r2)"

   156 | "der c (SEQ r1 r2) = 

   157      (if nullable r1

   158       then ALT (SEQ (der c r1) r2) (der c r2)

   159       else SEQ (der c r1) r2)"

   160 | "der c (STAR r) = SEQ (der c r) (STAR r)"

   161 

   162 fun 

   163  ders :: "string \<Rightarrow> rexp \<Rightarrow> rexp"

   164 where

   165   "ders [] r = r"

   166 | "ders (c # s) r = ders s (der c r)"

   167 

   168 

   169 lemma nullable_correctness:

   170   shows "nullable r  \<longleftrightarrow> [] \<in> (L r)"

   171 by (induct r) (auto simp add: Sequ_def) 

   172 

   173 lemma der_correctness:

   174   shows "L (der c r) = Der c (L r)"

   175 by (induct r) (simp_all add: nullable_correctness)

   176 

   177 lemma ders_correctness:

   178   shows "L (ders s r) = Ders s (L r)"

   179 apply(induct s arbitrary: r)

   180 apply(simp_all add: Ders_def der_correctness Der_def)

   181 done

   182 

   183 

   184 section {* Lemmas about ders *}

   185 

   186 lemma ders_ZERO:

   187   shows "ders s (ZERO) = ZERO"

   188 apply(induct s)

   189 apply(simp_all)

   190 done

   191 

   192 lemma ders_ONE:

   193   shows "ders s (ONE) = (if s = [] then ONE else ZERO)"

   194 apply(induct s)

   195 apply(simp_all add: ders_ZERO)

   196 done

   197 

   198 lemma ders_CHAR:

   199   shows "ders s (CHAR c) = 

   200            (if s = [c] then ONE else 

   201            (if s = [] then (CHAR c) else ZERO))"

   202 apply(induct s)

   203 apply(simp_all add: ders_ZERO ders_ONE)

   204 done

   205 

   206 lemma  ders_ALT:

   207   shows "ders s (ALT r1 r2) = ALT (ders s r1) (ders s r2)"

   208 apply(induct s arbitrary: r1 r2)

   209 apply(simp_all)

   210 done

   211 

   212 section {* Values *}

   213 

   214 datatype val = 

   215   Void

   216 | Char char

   217 | Seq val val

   218 | Right val

   219 | Left val

   220 | Stars "val list"

   221 

   222 

   223 section {* The string behind a value *}

   224 

   225 fun 

   226   flat :: "val \<Rightarrow> string"

   227 where

   228   "flat (Void) = []"

   229 | "flat (Char c) = [c]"

   230 | "flat (Left v) = flat v"

   231 | "flat (Right v) = flat v"

   232 | "flat (Seq v1 v2) = (flat v1) @ (flat v2)"

   233 | "flat (Stars []) = []"

   234 | "flat (Stars (v#vs)) = (flat v) @ (flat (Stars vs))" 

   235 

   236 lemma flat_Stars [simp]:

   237  "flat (Stars vs) = concat (map flat vs)"

   238 by (induct vs) (auto)

   239 

   240 

   241 section {* Relation between values and regular expressions *}

   242 

   243 inductive 

   244   Prf :: "val \<Rightarrow> rexp \<Rightarrow> bool" ("\<turnstile> _ : _" [100, 100] 100)

   245 where

   246  "\<lbrakk>\<turnstile> v1 : r1; \<turnstile> v2 : r2\<rbrakk> \<Longrightarrow> \<turnstile> Seq v1 v2 : SEQ r1 r2"

   247 | "\<turnstile> v1 : r1 \<Longrightarrow> \<turnstile> Left v1 : ALT r1 r2"

   248 | "\<turnstile> v2 : r2 \<Longrightarrow> \<turnstile> Right v2 : ALT r1 r2"

   249 | "\<turnstile> Void : ONE"

   250 | "\<turnstile> Char c : CHAR c"

   251 | "\<forall>v \<in> set vs. \<turnstile> v : r \<Longrightarrow> \<turnstile> Stars vs : STAR r"

   252 

   253 inductive_cases Prf_elims:

   254   "\<turnstile> v : ZERO"

   255   "\<turnstile> v : SEQ r1 r2"

   256   "\<turnstile> v : ALT r1 r2"

   257   "\<turnstile> v : ONE"

   258   "\<turnstile> v : CHAR c"

   259   "\<turnstile> vs : STAR r"

   260 

   261 lemma Star_concat:

   262   assumes "\<forall>s \<in> set ss. s \<in> A"  

   263   shows "concat ss \<in> A\<star>"

   264 using assms by (induct ss) (auto)

   265 

   266 

   267 lemma Prf_flat_L:

   268   assumes "\<turnstile> v : r" shows "flat v \<in> L r"

   269 using assms

   270 by (induct v r rule: Prf.induct)

   271    (auto simp add: Sequ_def Star_concat)

   272 

   273 lemma Prf_Stars_append:

   274   assumes "\<turnstile> Stars vs1 : STAR r" "\<turnstile> Stars vs2 : STAR r"

   275   shows "\<turnstile> Stars (vs1 @ vs2) : STAR r"

   276 using assms

   277 by (auto intro!: Prf.intros elim!: Prf_elims)

   278 

   279 lemma Star_string:

   280   assumes "s \<in> A\<star>"

   281   shows "\<exists>ss. concat ss = s \<and> (\<forall>s \<in> set ss. s \<in> A)"

   282 using assms

   283 apply(induct rule: Star.induct)

   284 apply(auto)

   285 apply(rule_tac x="[]" in exI)

   286 apply(simp)

   287 apply(rule_tac x="s1#ss" in exI)

   288 apply(simp)

   289 done

   290 

   291 lemma Star_val:

   292   assumes "\<forall>s\<in>set ss. \<exists>v. s = flat v \<and> \<turnstile> v : r"

   293   shows "\<exists>vs. concat (map flat vs) = concat ss \<and> (\<forall>v\<in>set vs. \<turnstile> v : r)"

   294 using assms

   295 apply(induct ss)

   296 apply(auto)

   297 apply (metis empty_iff list.set(1))

   298 by (metis concat.simps(2) list.simps(9) set_ConsD)

   299 

   300 

   301 lemma L_flat_Prf1:

   302   assumes "\<turnstile> v : r" 

   303   shows "flat v \<in> L r"

   304 using assms

   305 by (induct) (auto simp add: Sequ_def Star_concat)

   306 

   307 lemma L_flat_Prf2:

   308   assumes "s \<in> L r" 

   309   shows "\<exists>v. \<turnstile> v : r \<and> flat v = s"

   310 using assms

   311 proof(induct r arbitrary: s)

   312   case (STAR r s)

   313   have IH: "\<And>s. s \<in> L r \<Longrightarrow> \<exists>v. \<turnstile> v : r \<and> flat v = s" by fact

   314   have "s \<in> L (STAR r)" by fact

   315   then obtain ss where "concat ss = s" "\<forall>s \<in> set ss. s \<in> L r"

   316   using Star_string by auto

   317   then obtain vs where "concat (map flat vs) = s" "\<forall>v\<in>set vs. \<turnstile> v : r"

   318   using IH Star_val by blast

   319   then show "\<exists>v. \<turnstile> v : STAR r \<and> flat v = s"

   320   using Prf.intros(6) flat_Stars by blast

   321 next 

   322   case (SEQ r1 r2 s)

   323   then show "\<exists>v. \<turnstile> v : SEQ r1 r2 \<and> flat v = s"

   324   unfolding Sequ_def L.simps by (fastforce intro: Prf.intros)

   325 next

   326   case (ALT r1 r2 s)

   327   then show "\<exists>v. \<turnstile> v : ALT r1 r2 \<and> flat v = s"

   328   unfolding L.simps by (fastforce intro: Prf.intros)

   329 qed (auto intro: Prf.intros)

   330 

   331 lemma L_flat_Prf:

   332   "L(r) = {flat v | v. \<turnstile> v : r}"

   333 using L_flat_Prf1 L_flat_Prf2 by blast

   334 

   335 (*

   336 lemma Star_values_exists:

   337   assumes "s \<in> (L r)\<star>"

   338   shows "\<exists>vs. concat (map flat vs) = s \<and> \<turnstile> Stars vs : STAR r"

   339 using assms

   340 apply(drule_tac Star_string)

   341 apply(auto)

   342 by (metis L_flat_Prf2 Prf.intros(6) Star_val)

   343 *)

   344 

   345 

   346 section {* Sulzmann and Lu functions *}

   366 

    27 fun 

   367 section {* Mkeps, injval *}

    28   lexer :: "rexp \<Rightarrow> string \<Rightarrow> val option"

    29 where

    30   "lexer r [] = (if nullable r then Some(mkeps r) else None)"

    31 | "lexer r (c#s) = (case (lexer (der c r) s) of  

    32                     None \<Rightarrow> None

    33                   | Some(v) \<Rightarrow> Some(injval r c v))"

    34 

    35 

    36 

    37 section {* Mkeps, Injval Properties *}

   399 

    68 text {*

   400 

    69   Mkeps and injval produce, or preserve, Posix values.

   401 section {* Our Alternative Posix definition *}

    70 *}

   402 

   403 inductive 

   404   Posix :: "string \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<in> _ \<rightarrow> _" [100, 100, 100] 100)

   405 where

   406   Posix_ONE: "[] \<in> ONE \<rightarrow> Void"

   407 | Posix_CHAR: "[c] \<in> (CHAR c) \<rightarrow> (Char c)"

   408 | Posix_ALT1: "s \<in> r1 \<rightarrow> v \<Longrightarrow> s \<in> (ALT r1 r2) \<rightarrow> (Left v)"

   409 | Posix_ALT2: "\<lbrakk>s \<in> r2 \<rightarrow> v; s \<notin> L(r1)\<rbrakk> \<Longrightarrow> s \<in> (ALT r1 r2) \<rightarrow> (Right v)"

   410 | Posix_SEQ: "\<lbrakk>s1 \<in> r1 \<rightarrow> v1; s2 \<in> r2 \<rightarrow> v2;

   411     \<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> 

   412     (s1 @ s2) \<in> (SEQ r1 r2) \<rightarrow> (Seq v1 v2)"

   413 | Posix_STAR1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> STAR r \<rightarrow> Stars vs; flat v \<noteq> [];

   414     \<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>

   415     \<Longrightarrow> (s1 @ s2) \<in> STAR r \<rightarrow> Stars (v # vs)"

   416 | Posix_STAR2: "[] \<in> STAR r \<rightarrow> Stars []"

   417 

   418 inductive_cases Posix_elims:

   419   "s \<in> ZERO \<rightarrow> v"

   420   "s \<in> ONE \<rightarrow> v"

   421   "s \<in> CHAR c \<rightarrow> v"

   422   "s \<in> ALT r1 r2 \<rightarrow> v"

   423   "s \<in> SEQ r1 r2 \<rightarrow> v"

   424   "s \<in> STAR r \<rightarrow> v"

   425 

   426 lemma Posix1:

   427   assumes "s \<in> r \<rightarrow> v"

   428   shows "s \<in> L r" "flat v = s"

   429 using assms

   430 by (induct s r v rule: Posix.induct)

   431    (auto simp add: Sequ_def)

   432 

   433 

   434 lemma Posix1a:

   435   assumes "s \<in> r \<rightarrow> v"

   436   shows "\<turnstile> v : r"

   437 using assms

   438 apply(induct s r v rule: Posix.induct)

   439 apply(auto intro!: Prf.intros elim!: Prf_elims)

   440 done

   441 

   672 section {* The Lexer by Sulzmann and Lu  *}

   233 section {* Lexer Correctness *}

   673 

   674 fun 

   675   lexer :: "rexp \<Rightarrow> string \<Rightarrow> val option"

   676 where

   677   "lexer r [] = (if nullable r then Some(mkeps r) else None)"

   678 | "lexer r (c#s) = (case (lexer (der c r) s) of  

   679                     None \<Rightarrow> None

   680                   | Some(v) \<Rightarrow> Some(injval r c v))"