64 

    64 

    65 lemma Der_Sequ [simp]:

    65 lemma Der_Sequ [simp]:

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

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

    67 unfolding Der_def Sequ_def

    67 unfolding Der_def Sequ_def

    68 by (auto simp add: Cons_eq_append_conv)

    68 by (auto simp add: Cons_eq_append_conv)

    69 

    74 

    70 lemma Der_union [simp]:

    75 lemma Der_union [simp]:

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

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

    72 unfolding Der_def

    77 unfolding Der_def

    73 by auto

    78 by auto

   215 | UPNTIMES rexp nat

   220 | UPNTIMES rexp nat

   216 | NTIMES rexp nat

   221 | NTIMES rexp nat

   217 | FROMNTIMES rexp nat

   222 | FROMNTIMES rexp nat

   218 | NMTIMES rexp nat nat

   223 | NMTIMES rexp nat nat

   219 | PLUS rexp

   224 | PLUS rexp

   220 

   226 

   221 section {* Semantics of Regular Expressions *}

   227 section {* Semantics of Regular Expressions *}

   222  

   228  

   223 fun

   229 fun

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

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

   232 | "L (UPNTIMES r n) = (\<Union>i\<in> {..n} . (L r) \<up> i)"

   238 | "L (UPNTIMES r n) = (\<Union>i\<in> {..n} . (L r) \<up> i)"

   233 | "L (NTIMES r n) = (L r) \<up> n"

   239 | "L (NTIMES r n) = (L r) \<up> n"

   234 | "L (FROMNTIMES r n) = (\<Union>i\<in> {n..} . (L r) \<up> i)"

   240 | "L (FROMNTIMES r n) = (\<Union>i\<in> {n..} . (L r) \<up> i)"

   235 | "L (NMTIMES r n m) = (\<Union>i\<in>{n..m} . (L r) \<up> i)" 

   241 | "L (NMTIMES r n m) = (\<Union>i\<in>{n..m} . (L r) \<up> i)" 

   236 | "L (PLUS r) = (\<Union>i\<in> {1..} . (L r) \<up> i)"

   242 | "L (PLUS r) = (\<Union>i\<in> {1..} . (L r) \<up> i)"

   237 

   244 

   238 section {* Nullable, Derivatives *}

   245 section {* Nullable, Derivatives *}

   239 

   246 

   240 fun

   247 fun

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

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

   249 | "nullable (UPNTIMES r n) = True"

   256 | "nullable (UPNTIMES r n) = True"

   250 | "nullable (NTIMES r n) = (if n = 0 then True else nullable r)"

   257 | "nullable (NTIMES r n) = (if n = 0 then True else nullable r)"

   251 | "nullable (FROMNTIMES r n) = (if n = 0 then True else nullable r)"

   258 | "nullable (FROMNTIMES r n) = (if n = 0 then True else nullable r)"

   252 | "nullable (NMTIMES r n m) = (if m < n then False else (if n = 0 then True else nullable r))"

   259 | "nullable (NMTIMES r n m) = (if m < n then False else (if n = 0 then True else nullable r))"

   253 | "nullable (PLUS r) = (nullable r)"

   260 | "nullable (PLUS r) = (nullable r)"

   254 

   262 

   255 fun

   263 fun

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

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

   257 where

   265 where

   258   "der c (ZERO) = ZERO"

   266   "der c (ZERO) = ZERO"

   274      (if m < n then ZERO 

   282      (if m < n then ZERO 

   275       else (if n = 0 then (if m = 0 then ZERO else 

   283       else (if n = 0 then (if m = 0 then ZERO else 

   276                            SEQ (der c r) (UPNTIMES r (m - 1))) else 

   284                            SEQ (der c r) (UPNTIMES r (m - 1))) else 

   277                            SEQ (der c r) (NMTIMES r (n - 1) (m - 1))))" 

   285                            SEQ (der c r) (NMTIMES r (n - 1) (m - 1))))" 

   278 | "der c (PLUS r) = SEQ (der c r) (STAR r)"

   286 | "der c (PLUS r) = SEQ (der c r) (STAR r)"

   279 

   288 

   280 fun 

   289 fun 

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

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

   282 where

   291 where

   283   "ders [] r = r"

   292   "ders [] r = r"

   400 | Char char

   409 | Char char

   401 | Seq val val

   410 | Seq val val

   402 | Right val

   411 | Right val

   403 | Left val

   412 | Left val

   404 | Stars "val list"

   413 | Stars "val list"

   406 

   415 

   407 section {* The string behind a value *}

   416 section {* The string behind a value *}

   408 

   417 

   409 fun 

   418 fun 

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

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

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

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

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

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

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

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

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

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

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

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

   419 

   429 

   420 lemma flat_Stars [simp]:

   430 lemma flat_Stars [simp]:

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

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

   422 by (induct vs) (auto)

   432 by (induct vs) (auto)

   423 

   433 

   436 | "\<lbrakk>\<forall>v \<in> set vs. \<turnstile> v : r; length vs \<le> n\<rbrakk> \<Longrightarrow> \<turnstile> Stars vs : UPNTIMES r n"

   446 | "\<lbrakk>\<forall>v \<in> set vs. \<turnstile> v : r; length vs \<le> n\<rbrakk> \<Longrightarrow> \<turnstile> Stars vs : UPNTIMES r n"

   437 | "\<lbrakk>\<forall>v \<in> set vs. \<turnstile> v : r; length vs = n\<rbrakk> \<Longrightarrow> \<turnstile> Stars vs : NTIMES r n"

   447 | "\<lbrakk>\<forall>v \<in> set vs. \<turnstile> v : r; length vs = n\<rbrakk> \<Longrightarrow> \<turnstile> Stars vs : NTIMES r n"

   438 | "\<lbrakk>\<forall>v \<in> set vs. \<turnstile> v : r; length vs \<ge> n\<rbrakk> \<Longrightarrow> \<turnstile> Stars vs : FROMNTIMES r n"

   448 | "\<lbrakk>\<forall>v \<in> set vs. \<turnstile> v : r; length vs \<ge> n\<rbrakk> \<Longrightarrow> \<turnstile> Stars vs : FROMNTIMES r n"

   439 | "\<lbrakk>\<forall>v \<in> set vs. \<turnstile> v : r; length vs \<ge> n; length vs \<le> m\<rbrakk> \<Longrightarrow> \<turnstile> Stars vs : NMTIMES r n m"

   449 | "\<lbrakk>\<forall>v \<in> set vs. \<turnstile> v : r; length vs \<ge> n; length vs \<le> m\<rbrakk> \<Longrightarrow> \<turnstile> Stars vs : NMTIMES r n m"

   440 | "\<lbrakk>\<forall>v \<in> set vs. \<turnstile> v : r; length vs \<ge> 1\<rbrakk> \<Longrightarrow> \<turnstile> Stars vs : PLUS r"

   450 | "\<lbrakk>\<forall>v \<in> set vs. \<turnstile> v : r; length vs \<ge> 1\<rbrakk> \<Longrightarrow> \<turnstile> Stars vs : PLUS r"

   441 

   452 

   442 

   453 

   443 inductive_cases Prf_elims:

   454 inductive_cases Prf_elims:

   444   "\<turnstile> v : ZERO"

   455   "\<turnstile> v : ZERO"

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

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

   582 apply(simp)

   593 apply(simp)

   583 apply(rule Prf.intros)

   594 apply(rule Prf.intros)

   584 apply(simp)

   595 apply(simp)

   585 apply(simp)

   596 apply(simp)

   586 using Star_Pow Star_val_length apply blast

   597 using Star_Pow Star_val_length apply blast

   588 

   600 

   589 lemma L_flat_Prf:

   601 lemma L_flat_Prf:

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

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

   591 using Prf_flat_L L_flat_Prf2 by blast

   603 using Prf_flat_L L_flat_Prf2 by blast

   592 

   604 

   603 | "mkeps(UPNTIMES r n) = Stars []"

   615 | "mkeps(UPNTIMES r n) = Stars []"

   604 | "mkeps(NTIMES r n) = Stars (replicate n (mkeps r))"

   616 | "mkeps(NTIMES r n) = Stars (replicate n (mkeps r))"

   605 | "mkeps(FROMNTIMES r n) = Stars (replicate n (mkeps r))"

   617 | "mkeps(FROMNTIMES r n) = Stars (replicate n (mkeps r))"

   606 | "mkeps(NMTIMES r n m) = Stars (replicate n (mkeps r))"

   618 | "mkeps(NMTIMES r n m) = Stars (replicate n (mkeps r))"

   607 | "mkeps(PLUS r) = Stars ([mkeps r])"

   619 | "mkeps(PLUS r) = Stars ([mkeps r])"

   608 

   621 

   609 

   622 

   610 fun injval :: "rexp \<Rightarrow> char \<Rightarrow> val \<Rightarrow> val"

   623 fun injval :: "rexp \<Rightarrow> char \<Rightarrow> val \<Rightarrow> val"

   611 where

   624 where

   612   "injval (CHAR d) c Void = Char d"

   625   "injval (CHAR d) c Void = Char d"

   619 | "injval (UPNTIMES r n) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)"

   632 | "injval (UPNTIMES r n) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)"

   620 | "injval (NTIMES r n) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)"

   633 | "injval (NTIMES r n) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)"

   621 | "injval (FROMNTIMES r n) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)"

   634 | "injval (FROMNTIMES r n) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)"

   622 | "injval (NMTIMES r n m) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)"

   635 | "injval (NMTIMES r n m) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)"

   623 | "injval (PLUS r) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)"

   636 | "injval (PLUS r) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)"

   624 

   638 

   625 section {* Mkeps, injval *}

   639 section {* Mkeps, injval *}

   626 

   648 

   627 lemma mkeps_nullable:

   649 lemma mkeps_nullable:

   628   assumes "nullable(r)" 

   650   assumes "nullable(r)" 

   629   shows "\<turnstile> mkeps r : r"

   651   shows "\<turnstile> mkeps r : r"

   630 using assms

   652 using assms

   631 apply(induct r rule: mkeps.induct) 

   653 apply(induct r rule: mkeps.induct) 

   632 apply(auto intro: Prf.intros)

   654 apply(auto intro: Prf.intros)

   643 

   695 

   644 lemma Prf_injval:

   696 lemma Prf_injval:

   645   assumes "\<turnstile> v : der c r" 

   697   assumes "\<turnstile> v : der c r" 

   646   shows "\<turnstile> (injval r c v) : r"

   698   shows "\<turnstile> (injval r c v) : r"

   647 using assms

   699 using assms

   718 apply(rotate_tac 2)

   770 apply(rotate_tac 2)

   719 apply(erule Prf.cases)

   771 apply(erule Prf.cases)

   720 apply(simp_all)

   772 apply(simp_all)

   721 apply(auto)

   773 apply(auto)

   722 using Prf.intros apply auto[1]

   774 using Prf.intros apply auto[1]

   758 

   787 

   759 

   788 

   760 section {* Our Alternative Posix definition *}

   789 section {* Our Alternative Posix definition *}

   761 

   790 

   762 inductive 

   791 inductive 

   790     \<Longrightarrow> (s1 @ s2) \<in> NMTIMES r (Suc n) (Suc m) \<rightarrow> Stars (v # vs)"

   819     \<Longrightarrow> (s1 @ s2) \<in> NMTIMES r (Suc n) (Suc m) \<rightarrow> Stars (v # vs)"

   791 | Posix_NMTIMES2: "s \<in> UPNTIMES r m \<rightarrow> Stars vs \<Longrightarrow>  s \<in> NMTIMES r 0 m \<rightarrow> Stars vs"

   820 | Posix_NMTIMES2: "s \<in> UPNTIMES r m \<rightarrow> Stars vs \<Longrightarrow>  s \<in> NMTIMES r 0 m \<rightarrow> Stars vs"

   792 | Posix_PLUS1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> STAR r \<rightarrow> Stars vs; flat v = [] \<Longrightarrow> flat (Stars vs) = [];

   821 | Posix_PLUS1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> STAR r \<rightarrow> Stars vs; flat v = [] \<Longrightarrow> flat (Stars vs) = [];

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

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

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

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

   795 

   825 

   796 inductive_cases Posix_elims:

   826 inductive_cases Posix_elims:

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

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

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

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

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

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

   924 apply(rotate_tac 3)

   954 apply(rotate_tac 3)

   925 apply(erule Prf.cases)

   955 apply(erule Prf.cases)

   926 apply(simp_all)

   956 apply(simp_all)

   927 apply(rule Prf.intros)

   957 apply(rule Prf.intros)

   928 apply(auto)

   958 apply(auto)

   930 

   962 

   931 

   963 

   932 lemma  Posix_NTIMES_mkeps:

   964 lemma  Posix_NTIMES_mkeps:

   933   assumes "[] \<in> r \<rightarrow> mkeps r"

   965   assumes "[] \<in> r \<rightarrow> mkeps r"

   934   shows "[] \<in> NTIMES r n \<rightarrow> Stars (replicate n (mkeps r))"

   966   shows "[] \<in> NTIMES r n \<rightarrow> Stars (replicate n (mkeps r))"

  1179   by (metis Posix1(1) Posix_PLUS1.hyps(6) append_self_conv append_self_conv2)

  1211   by (metis Posix1(1) Posix_PLUS1.hyps(6) append_self_conv append_self_conv2)

  1180   moreover

  1212   moreover

  1181   have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2"

  1213   have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2"

  1182             "\<And>v2. s2 \<in> STAR r \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+

  1214             "\<And>v2. s2 \<in> STAR r \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+

  1183   ultimately show "Stars (v # vs) = v2" by auto

  1215   ultimately show "Stars (v # vs) = v2" by auto

  1184 qed

  1227 qed

  1185 

  1228 

  1186 lemma NTIMES_Stars:

  1229 lemma NTIMES_Stars:

  1187  assumes "\<turnstile> v : NTIMES r n"

  1230  assumes "\<turnstile> v : NTIMES r n"

  1188  shows "\<exists>vs. v = Stars vs \<and> (\<forall>v \<in> set vs. \<turnstile> v : r) \<and> length vs = n"

  1231  shows "\<exists>vs. v = Stars vs \<and> (\<forall>v \<in> set vs. \<turnstile> v : r) \<and> length vs = n"

  1603   using PLUS.hyps apply auto[1]

  1646   using PLUS.hyps apply auto[1]

  1604   apply(rule Posix.intros)

  1647   apply(rule Posix.intros)

  1605   apply(simp)

  1648   apply(simp)

  1606   apply(simp)

  1649   apply(simp)

  1607   done  

  1650   done  

  1608 qed

  1662 qed

  1609 

  1663 

  1610 

  1664 

  1611 

  1665 

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

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