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)

    74 

    69 

    75 lemma Der_union [simp]:

    70 lemma Der_union [simp]:

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

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

    77 unfolding Der_def

    72 unfolding Der_def

    78 by auto

    73 by auto

   220 | UPNTIMES rexp nat

   215 | UPNTIMES rexp nat

   221 | NTIMES rexp nat

   216 | NTIMES rexp nat

   222 | FROMNTIMES rexp nat

   217 | FROMNTIMES rexp nat

   223 | NMTIMES rexp nat nat

   218 | NMTIMES rexp nat nat

   224 | PLUS rexp

   219 | PLUS rexp

   229 

   220 

   230 section {* Semantics of Regular Expressions *}

   221 section {* Semantics of Regular Expressions *}

   231  

   222  

   232 fun

   223 fun

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

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

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

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

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

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

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

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

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

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

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

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

   250 

   237 

   251 section {* Nullable, Derivatives *}

   238 section {* Nullable, Derivatives *}

   252 

   239 

   253 fun

   240 fun

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

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

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

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

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

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

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

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

   265 | "nullable (NMTIMES r n m) = (if m < n then False else (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))"

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

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

   272 

   254 

   273 fun

   255 fun

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

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

   275 where

   257 where

   276   "der c (ZERO) = ZERO"

   258   "der c (ZERO) = ZERO"

   292      (if m < n then ZERO 

   274      (if m < n then ZERO 

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

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

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

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

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

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

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

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

   302 

   279 

   303 fun 

   280 fun 

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

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

   305 where

   282 where

   306   "ders [] r = r"

   283   "ders [] r = r"

   351 apply(case_tac "n \<le> m")

   328 apply(case_tac "n \<le> m")

   352 prefer 2

   329 prefer 2

   353 apply(simp only: der.simps if_True)

   330 apply(simp only: der.simps if_True)

   354 apply(simp only: L.simps)

   331 apply(simp only: L.simps)

   355 apply(simp)

   332 apply(simp)

   357 apply(subst (asm) Sequ_UNION[symmetric])

   334 apply(subst (asm) Sequ_UNION[symmetric])

   358 apply(subst (asm) test[symmetric])

   335 apply(subst (asm) test[symmetric])

   359 apply(auto simp add: Der_UNION)[1]

   336 apply(auto simp add: Der_UNION)[1]

   360 apply(auto simp add: Der_UNION)[1]

   337 apply(auto simp add: Der_UNION)[1]

   361 apply(subst Sequ_UNION[symmetric])

   338 apply(subst Sequ_UNION[symmetric])

   376 apply(simp add: Der_UNION)

   353 apply(simp add: Der_UNION)

   377 apply(erule_tac bexE)

   354 apply(erule_tac bexE)

   378 apply(case_tac xa)

   355 apply(case_tac xa)

   379 apply(simp)

   356 apply(simp)

   380 apply(simp)

   357 apply(simp)

   382 apply(auto simp add: Sequ_def Der_def)[1]

   359 apply(auto simp add: Sequ_def Der_def)[1]

   383 using Star_def apply auto[1]

   360 using Star_def apply auto[1]

   384 apply(case_tac "[] \<in> L r")

   361 apply(case_tac "[] \<in> L r")

   395 

   364 

   396 lemma ders_correctness:

   365 lemma ders_correctness:

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

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

   398 apply(induct s arbitrary: r)

   367 apply(induct s arbitrary: r)

   399 apply(simp_all add: Ders_def der_correctness Der_def)

   368 apply(simp_all add: Ders_def der_correctness Der_def)

   431 | Char char

   400 | Char char

   432 | Seq val val

   401 | Seq val val

   433 | Right val

   402 | Right val

   434 | Left val

   403 | Left val

   435 | Stars "val list"

   404 | Stars "val list"

   440 

   406 

   441 section {* The string behind a value *}

   407 section {* The string behind a value *}

   442 

   408 

   443 fun 

   409 fun 

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

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

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

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

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

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

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

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

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

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

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

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

   457 

   419 

   458 lemma flat_Stars [simp]:

   420 lemma flat_Stars [simp]:

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

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

   460 by (induct vs) (auto)

   422 by (induct vs) (auto)

   461 

   423 

   462 lemma Star_Pow:

   490 lemma Star_Pow:

   463   assumes "s \<in> A \<up> n"

   491   assumes "s \<in> A \<up> n"

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

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

   465 using assms

   493 using assms

   466 apply(induct n arbitrary: s)

   494 apply(induct n arbitrary: s)

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

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

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

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

   477 using assms

   505 using assms

   478 apply(auto simp add: Star_def)

   506 apply(auto simp add: Star_def)

   479 using Star_Pow by blast

   507 using Star_Pow by blast

   480 

   592 

   481 

   593 

   482 section {* Sulzmann and Lu functions *}

   594 section {* Sulzmann and Lu functions *}

   483 

   595 

   484 fun 

   596 fun 

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

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

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

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

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

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

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

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

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

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

   499 

   608 

   500 

   609 

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

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

   502 where

   611 where

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

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

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

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

   511 | "injval (NTIMES 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)"

   512 | "injval (FROMNTIMES 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)"

   513 | "injval (NMTIMES r n m) 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)"

   514 | "injval (PLUS r) 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)"

   517 

   624 

   518 section {* Mkeps, injval *}

   625 section {* Mkeps, injval *}

   519 

   634 

   520 lemma mkeps_flat:

   635 lemma mkeps_flat:

   521   assumes "nullable(r)" 

   636   assumes "nullable(r)" 

   522   shows "flat (mkeps r) = []"

   637   shows "flat (mkeps r) = []"

   523 using assms

   638 using assms

   570 

   643 

   571 lemma Prf_injval:

   644 lemma Prf_injval:

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

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

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

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

   574 using assms

   647 using assms

   645 apply(rotate_tac 2)

   718 apply(rotate_tac 2)

   646 apply(erule Prf.cases)

   719 apply(erule Prf.cases)

   647 apply(simp_all)

   720 apply(simp_all)

   648 apply(auto)

   721 apply(auto)

   649 using Prf.intros apply auto[1]

   722 using Prf.intros apply auto[1]

   662 

   758 

   663 

   759 

   664 section {* Our Alternative Posix definition *}

   760 section {* Our Alternative Posix definition *}

   665 

   761 

   666 inductive 

   762 inductive 

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

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

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

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

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

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

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

   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>

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

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

   700 

   795 

   701 inductive_cases Posix_elims:

   796 inductive_cases Posix_elims:

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

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

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

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

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

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

   829 apply(rotate_tac 3)

   924 apply(rotate_tac 3)

   830 apply(erule Prf.cases)

   925 apply(erule Prf.cases)

   831 apply(simp_all)

   926 apply(simp_all)

   832 apply(rule Prf.intros)

   927 apply(rule Prf.intros)

   833 apply(auto)

   928 apply(auto)

   837 

   930 

   838 

   931 

   839 lemma  Posix_NTIMES_mkeps:

   932 lemma  Posix_NTIMES_mkeps:

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

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

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

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

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

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

  1087   moreover

  1180   moreover

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

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

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

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

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

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

  1102 qed

  1184 qed

  1103 

  1185 

  1104 lemma NTIMES_Stars:

  1186 lemma NTIMES_Stars:

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

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

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

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

  1521   using PLUS.hyps apply auto[1]

  1603   using PLUS.hyps apply auto[1]

  1522   apply(rule Posix.intros)

  1604   apply(rule Posix.intros)

  1523   apply(simp)

  1605   apply(simp)

  1524   apply(simp)

  1606   apply(simp)

  1525   done  

  1607   done  

  1537 qed

  1608 qed

  1538 

  1609 

  1539 

  1610 

  1540 

  1611 

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

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