29 | EMPTY

    29 | EMPTY

    30 | CHAR char

    30 | CHAR char

    31 | SEQ rexp rexp

    31 | SEQ rexp rexp

    32 | ALT rexp rexp

    32 | ALT rexp rexp

    33 

    33 

    34 section {* Semantics of Regular Expressions *}

    39 section {* Semantics of Regular Expressions *}

    35  

    40  

    36 fun

    41 fun

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

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

    38 where

    43 where

    48   "nullable (NULL) = False"

    53   "nullable (NULL) = False"

    49 | "nullable (EMPTY) = True"

    54 | "nullable (EMPTY) = True"

    50 | "nullable (CHAR c) = False"

    55 | "nullable (CHAR c) = False"

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

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

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

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

    53 

    74 

    54 value "L(CHAR c)"

    75 value "L(CHAR c)"

    55 value "L(SEQ(CHAR c)(CHAR b))"

    76 value "L(SEQ(CHAR c)(CHAR b))"

    56 

    77 

    57 lemma nullable_correctness:

    78 lemma nullable_correctness:

    67 | Char char

    88 | Char char

    68 | Seq val val

    89 | Seq val val

    69 | Right val

    90 | Right val

    70 | Left val

    91 | Left val

    71 

    92 

    72 section {* The string behind a value *}

    99 section {* The string behind a value *}

    73 

   100 

    74 fun flat :: "val \<Rightarrow> string"

   101 fun flat :: "val \<Rightarrow> string"

    75 where

   102 where

    76   "flat(Void) = []"

   103   "flat(Void) = []"

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

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

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

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

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

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

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

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

    81 

   108 

    82 fun head :: "val \<Rightarrow> string"

   125 fun head :: "val \<Rightarrow> string"

    83 where

   126 where

    84   "head(Void) = []"

   127   "head(Void) = []"

    85 | "head(Char c) = [c]"

   128 | "head(Char c) = [c]"

    86 | "head(Left v) = head(v)"

   129 | "head(Left v) = head(v)"

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

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

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

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

   107 | "\<turnstile> Void : EMPTY"

   150 | "\<turnstile> Void : EMPTY"

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

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

   109 

   152 

   110 fun mkeps :: "rexp \<Rightarrow> val"

   158 fun mkeps :: "rexp \<Rightarrow> val"

   111 where

   159 where

   112   "mkeps(EMPTY) = Void"

   160   "mkeps(EMPTY) = Void"

   113 | "mkeps(SEQ r1 r2) = Seq (mkeps r1) (mkeps r2)"

   161 | "mkeps(SEQ r1 r2) = Seq (mkeps r1) (mkeps r2)"

   114 | "mkeps(ALT r1 r2) = (if nullable(r1) then Left (mkeps r1) else Right (mkeps r2))"

   162 | "mkeps(ALT r1 r2) = (if nullable(r1) then Left (mkeps r1) else Right (mkeps r2))"

   127   assumes "nullable(r)" shows "flat (mkeps r) = []"

   175   assumes "nullable(r)" shows "flat (mkeps r) = []"

   128 using assms

   176 using assms

   129 apply(induct rule: nullable.induct)

   177 apply(induct rule: nullable.induct)

   130 apply(auto)

   178 apply(auto)

   131 done

   179 done

   132 

   189 

   133 text {*

   190 text {*

   134   The value mkeps returns is always the correct POSIX

   191   The value mkeps returns is always the correct POSIX

   135   value.

   192   value.

   136 *}

   193 *}

   140 

   197 

   141 

   198 

   142 lemma Prf_flat_L:

   199 lemma Prf_flat_L:

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

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

   144 using assms

   201 using assms

   146 apply(auto simp add: Sequ_def)

   203 apply(auto simp add: Sequ_def)

   147 done

   204 done

   148 

   205 

   149 lemma L_flat_Prf:

   206 lemma L_flat_Prf:

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

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

   174 | "v2 \<succ>r2 v2' \<Longrightarrow> (Right v2) \<succ>(ALT r1 r2) (Right v2')"

   231 | "v2 \<succ>r2 v2' \<Longrightarrow> (Right v2) \<succ>(ALT r1 r2) (Right v2')"

   175 | "v1 \<succ>r1 v1' \<Longrightarrow> (Left v1) \<succ>(ALT r1 r2) (Left v1')"

   232 | "v1 \<succ>r1 v1' \<Longrightarrow> (Left v1) \<succ>(ALT r1 r2) (Left v1')"

   176 | "Void \<succ>EMPTY Void"

   233 | "Void \<succ>EMPTY Void"

   177 | "(Char c) \<succ>(CHAR c) (Char c)"

   234 | "(Char c) \<succ>(CHAR c) (Char c)"

   178 

   235 

   179 

   263 

   180 section {* The ordering is reflexive *}

   264 section {* The ordering is reflexive *}

   181 

   265 

   182 lemma ValOrd_refl:

   266 lemma ValOrd_refl:

   183   assumes "\<turnstile> v : r"

   267   assumes "\<turnstile> v : r"

   539 apply(simp_all)[5]

   623 apply(simp_all)[5]

   540 apply(simp)

   624 apply(simp)

   541 apply(case_tac "nullable r1")

   625 apply(case_tac "nullable r1")

   542 apply(simp)

   626 apply(simp)

   543 apply(erule Prf.cases)

   627 apply(erule Prf.cases)

   548 apply(auto)[1]

   634 apply(auto)[1]

   549 apply (metis mkeps_flat)

   635 apply (metis mkeps_flat)

   550 apply(simp)

   636 apply(simp)

   551 apply(erule Prf.cases)

   637 apply(erule Prf.cases)

   552 apply(simp_all)[5]

   638 apply(simp_all)[5]

   553 done

   639 done

   554 

   675 

   555 lemma v4_proj:

   676 lemma v4_proj:

   556   assumes "\<turnstile> v : r" and "\<exists>s. (flat v) = c # s"

   677   assumes "\<turnstile> v : r" and "\<exists>s. (flat v) = c # s"

   557   shows "c # flat (projval r c v) = flat v"

   678   shows "c # flat (projval r c v) = flat v"

   558 using assms

   679 using assms

   680 apply(simp_all)[5]

   801 apply(simp_all)[5]

   681 apply(auto)[1]

   802 apply(auto)[1]

   682 apply(simp add: v4)

   803 apply(simp add: v4)

   683 done

   804 done

   684 

   805 

   740 lemma LeftRight:

   806 lemma LeftRight:

   741   assumes "(Left v1) \<succ>(der c (ALT r1 r2)) (Right v2)"

   807   assumes "(Left v1) \<succ>(der c (ALT r1 r2)) (Right v2)"

   742   and "\<turnstile> v1 : der c r1" "\<turnstile> v2 : der c r2" 

   808   and "\<turnstile> v1 : der c r1" "\<turnstile> v2 : der c r2" 

   743   shows "(injval (ALT r1 r2) c (Left v1)) \<succ>(ALT r1 r2) (injval (ALT r1 r2) c (Right v2))"

   809   shows "(injval (ALT r1 r2) c (Left v1)) \<succ>(ALT r1 r2) (injval (ALT r1 r2) c (Right v2))"

   744 using assms

   810 using assms

   818 prefer 2

   884 prefer 2

   819 apply (metis list.distinct(1) mkeps_flat v4)

   885 apply (metis list.distinct(1) mkeps_flat v4)

   820 by (metis h)

   886 by (metis h)

   821 

   887 

   822 lemma Prf_inj_test:

   888 lemma Prf_inj_test:

   826 

   969 

   827 lemma Prf_inj:

   970 lemma Prf_inj:

   828   assumes "v1 \<succ>(der c r) v2" "\<turnstile> v1 : der c r" "\<turnstile> v2 : der c r" (*"flat v1 = flat v2"*)

   971   assumes "v1 \<succ>(der c r) v2" "\<turnstile> v1 : der c r" "\<turnstile> v2 : der c r" (*"flat v1 = flat v2"*)

   829   shows "(injval r c v1) \<succ>r (injval r c v2)"

   972   shows "(injval r c v1) \<succ>r (injval r c v2)"

   830 using assms

   973 using assms

   832 (* NULL case *)

   975 (* NULL case *)

   833 apply(simp)

   976 apply(simp)

   834 apply(erule ValOrd.cases)

   977 apply(erule ValOrd.cases)

   835 apply(simp_all)[8]

   978 apply(simp_all)[8]

   836 (* EMPTY case *)

   979 (* EMPTY case *)

   968 prefer 2

  1111 prefer 2

   969 thm mkeps_flat v4

  1112 thm mkeps_flat v4

   970 apply (metis list.distinct(1) mkeps_flat v4)

  1113 apply (metis list.distinct(1) mkeps_flat v4)

   971 oops

  1114 oops

   972 

  1115 

   973 lemma POSIX_der:

  1117 lemma POSIX_der:

   974   assumes "POSIX v (der c r)" "\<turnstile> v : der c r"

  1118   assumes "POSIX v (der c r)" "\<turnstile> v : der c r"

   975   shows "POSIX (injval r c v) r"

  1119   shows "POSIX (injval r c v) r"

   976 using assms

  1120 using assms

   977 unfolding POSIX_def

  1121 unfolding POSIX_def

   978 apply(auto)

  1122 apply(auto)

   979 thm v3

  1123 thm v3

   981 thm v4

  1125 thm v4

   982 apply(subst (asm) v4)

  1126 apply(subst (asm) v4)

   983 apply(assumption)

  1127 apply(assumption)

   984 apply(drule_tac x="projval r c v'" in spec)

  1128 apply(drule_tac x="projval r c v'" in spec)

   985 apply(drule mp)

  1129 apply(drule mp)

   996 apply(subst v4_proj)

  1140 apply(subst v4_proj)

   997 apply(simp)

  1141 apply(simp)

   998 apply(rule_tac x="flat v" in exI)

  1142 apply(rule_tac x="flat v" in exI)

   999 apply(simp)

  1143 apply(simp)

  1000 apply(simp)

  1144 apply(simp)

  1005 apply(rule_tac c="c" in  t)

  1262 apply(rule_tac c="c" in  t)

  1006 apply(simp)

  1263 apply(simp)

  1007 thm v4_proj

  1264 thm v4_proj

  1008 apply(subst v4_proj)

  1265 apply(subst v4_proj)

  1009 apply(simp)

  1266 apply(simp)

  1010 apply(rule_tac x="flat v" in exI)

  1267 apply(rule_tac x="flat v" in exI)

  1011 apply(simp)

  1268 apply(simp)

  1012 apply(simp)

  1269 apply(simp)

  1017 

  1271 

  1018 

  1272 

  1019 lemma POSIX_ex: "\<turnstile> v : r \<Longrightarrow> \<exists>v. POSIX v r"

  1273 lemma POSIX_ex: "\<turnstile> v : r \<Longrightarrow> \<exists>v. POSIX v r"

  1020 apply(induct r arbitrary: v)

  1274 apply(induct r arbitrary: v)

  1021 apply(erule Prf.cases)

  1275 apply(erule Prf.cases)