Mercurial Mercurial > hg > lexing / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
thys/Re1.thy
changeset 79 ca8f9645db69
parent 78 279d0bc48308
child 81 7ac7782a7318
equal deleted inserted replaced
78:279d0bc48308 79:ca8f9645db69 
    45 | "L (EMPTY) = {[]}"
 
    45 | "L (EMPTY) = {[]}"
 
    46 | "L (CHAR c) = {[c]}"
 
    46 | "L (CHAR c) = {[c]}"
 
    47 | "L (SEQ r1 r2) = (L r1) ;; (L r2)"
 
    47 | "L (SEQ r1 r2) = (L r1) ;; (L r2)"
 
    48 | "L (ALT r1 r2) = (L r1) \<union> (L r2)"
 
    48 | "L (ALT r1 r2) = (L r1) \<union> (L r2)"
 
    49 
    49 
       
    50 fun zeroable where
 
       
    51   "zeroable NULL = True"
 
       
    52 | "zeroable EMPTY = False"
 
       
    53 | "zeroable (CHAR c) = False"
 
       
    54 | "zeroable (ALT r1 r2) = (zeroable r1 \<and> zeroable r2)"
 
       
    55 | "zeroable (SEQ r1 r2) = (zeroable r1 \<or> zeroable r2)"
 
       
    56 
       
    57 lemma L_ALT_cases:
 
       
    58   "L (ALT r1 r2) \<noteq> {} \<Longrightarrow> (L r1 \<noteq> {}) \<or> (L r1 = {} \<and> L r2 \<noteq> {})"
 
       
    59 by(auto)
 
       
    60 
    50 fun
 
    61 fun
 
    51  nullable :: "rexp \<Rightarrow> bool"
 
    62  nullable :: "rexp \<Rightarrow> bool"
 
    52 where
 
    63 where
 
    53   "nullable (NULL) = False"
 
    64   "nullable (NULL) = False"
 
    54 | "nullable (EMPTY) = True"
 
    65 | "nullable (EMPTY) = True"
 
    55 | "nullable (CHAR c) = False"
 
    66 | "nullable (CHAR c) = False"
 
    56 | "nullable (ALT r1 r2) = (nullable r1 \<or> nullable r2)"
 
    67 | "nullable (ALT r1 r2) = (nullable r1 \<or> nullable r2)"
 
    57 | "nullable (SEQ r1 r2) = (nullable r1 \<and> nullable r2)"
 
    68 | "nullable (SEQ r1 r2) = (nullable r1 \<and> nullable r2)"
 
    58 
    69 
    59 fun
 
       
    60  nullable_left :: "rexp \<Rightarrow> bool"
 
       
    61 where
 
       
    62   "nullable_left (NULL) = False"
 
       
    63 | "nullable_left (EMPTY) = True"
 
       
    64 | "nullable_left (CHAR c) = False"
 
       
    65 | "nullable_left (ALT r1 r2) = (nullable_left r1 \<or> nullable_left r2)"
 
       
    66 | "nullable_left (SEQ r1 r2) = nullable_left r1"
 
       
    67 
       
    68 lemma nullable_left:
 
       
    69   "nullable r \<Longrightarrow> nullable_left r"
 
       
    70 apply(induct r)
 
       
    71 apply(auto)
 
       
    72 done
 
       
    73 
       
    74 
       
    75 value "L(CHAR c)"
 
       
    76 value "L(SEQ(CHAR c)(CHAR b))"
 
       
    77 
       
    78 lemma nullable_correctness:
 
    70 lemma nullable_correctness:
 
    79   shows "nullable r  \<longleftrightarrow> [] \<in> (L r)"
 
    71   shows "nullable r  \<longleftrightarrow> [] \<in> (L r)"
 
    80 apply (induct r) 
    72 apply (induct r) 
    81 apply(auto simp add: Sequ_def) 
    73 apply(auto simp add: Sequ_def) 
    82 done
 
    74 done
 
    87   Void
 
    79   Void
 
    88 | Char char
 
    80 | Char char
 
    89 | Seq val val
 
    81 | Seq val val
 
    90 | Right val
 
    82 | Right val
 
    91 | Left val
 
    83 | Left val
 
    92 
       
    93 fun Seqs :: "val \<Rightarrow> val list \<Rightarrow> val"
 
       
    94 where
 
       
    95   "Seqs v [] = v"
 
       
    96 | "Seqs v (v'#vs) = Seq v (Seqs v' vs)"
 
       
    97 
    84 
    98 
    85 
    99 section {* The string behind a value *}
 
    86 section {* The string behind a value *}
 
   100 
    87 
   101 fun flat :: "val \<Rightarrow> string"
 
    88 fun flat :: "val \<Rightarrow> string"
 
   104 | "flat(Char c) = [c]"
 
    91 | "flat(Char c) = [c]"
 
   105 | "flat(Left v) = flat(v)"
 
    92 | "flat(Left v) = flat(v)"
 
   106 | "flat(Right v) = flat(v)"
 
    93 | "flat(Right v) = flat(v)"
 
   107 | "flat(Seq v1 v2) = flat(v1) @ flat(v2)"
 
    94 | "flat(Seq v1 v2) = flat(v1) @ flat(v2)"
 
   108 
    95 
   109 fun flat_left :: "val \<Rightarrow> string"
 
       
   110 where
 
       
   111   "flat_left(Void) = []"
 
       
   112 | "flat_left(Char c) = [c]"
 
       
   113 | "flat_left(Left v) = flat_left(v)"
 
       
   114 | "flat_left(Right v) = flat_left(v)"
 
       
   115 | "flat_left(Seq v1 v2) = flat_left(v1)"
 
       
   116 
       
   117 fun flat_right :: "val \<Rightarrow> string"
 
       
   118 where
 
       
   119   "flat_right(Void) = []"
 
       
   120 | "flat_right(Char c) = [c]"
 
       
   121 | "flat_right(Left v) = flat(v)"
 
       
   122 | "flat_right(Right v) = flat(v)"
 
       
   123 | "flat_right(Seq v1 v2) = flat(v2)"
 
       
   124 
       
   125 fun head :: "val \<Rightarrow> string"
 
       
   126 where
 
       
   127   "head(Void) = []"
 
       
   128 | "head(Char c) = [c]"
 
       
   129 | "head(Left v) = head(v)"
 
       
   130 | "head(Right v) = head(v)"
 
       
   131 | "head(Seq v1 v2) = head v1"
 
       
   132 
       
   133 fun flats :: "val \<Rightarrow> string list"
 
    96 fun flats :: "val \<Rightarrow> string list"
 
   134 where
 
    97 where
 
   135   "flats(Void) = [[]]"
 
    98   "flats(Void) = [[]]"
 
   136 | "flats(Char c) = [[c]]"
 
    99 | "flats(Char c) = [[c]]"
 
   137 | "flats(Left v) = flats(v)"
 
   100 | "flats(Left v) = flats(v)"
 
   140 
   103 
   141 value "flats(Seq(Char c)(Char b))"
 
   104 value "flats(Seq(Char c)(Char b))"
 
   142 
   105 
   143 section {* Relation between values and regular expressions *}
 
   106 section {* Relation between values and regular expressions *}
 
   144 
   107 
       
   108 
   145 inductive Prfs :: "string \<Rightarrow> val \<Rightarrow> rexp \<Rightarrow> bool" ("\<Turnstile>_ _ : _" [100, 100, 100] 100)
 
   109 inductive Prfs :: "string \<Rightarrow> val \<Rightarrow> rexp \<Rightarrow> bool" ("\<Turnstile>_ _ : _" [100, 100, 100] 100)
 
   146 where
 
   110 where
 
   147  "\<lbrakk>\<Turnstile>s1 v1 : r1; \<Turnstile>s2 v2 : r2\<rbrakk> \<Longrightarrow> \<Turnstile>(s1 @ s2) (Seq v1 v2) : SEQ r1 r2"
 
   111  "\<lbrakk>\<Turnstile>s1 v1 : r1; \<Turnstile>s2 v2 : r2\<rbrakk> \<Longrightarrow> \<Turnstile>(s1 @ s2) (Seq v1 v2) : SEQ r1 r2"
 
   148 | "\<Turnstile>s v1 : r1 \<Longrightarrow> \<Turnstile>s (Left v1) : ALT r1 r2"
 
   112 | "\<Turnstile>s v1 : r1 \<Longrightarrow> \<Turnstile>s (Left v1) : ALT r1 r2"
 
   149 | "\<Turnstile>s v2 : r2 \<Longrightarrow> \<Turnstile>s (Right v2) : ALT r1 r2"
 
   113 | "\<Turnstile>s v2 : r2 \<Longrightarrow> \<Turnstile>s (Right v2) : ALT r1 r2"
 
   154   "\<Turnstile>s v : r \<Longrightarrow> flat v = s"
 
   118   "\<Turnstile>s v : r \<Longrightarrow> flat v = s"
 
   155 apply(induct s v r rule: Prfs.induct)
 
   119 apply(induct s v r rule: Prfs.induct)
 
   156 apply(auto)
 
   120 apply(auto)
 
   157 done
 
   121 done
 
   158 
   122 
   159 
       
   160 inductive Prfn :: "nat \<Rightarrow> val \<Rightarrow> rexp \<Rightarrow> bool" ("\<TTurnstile>_ _ : _" [100, 100, 100] 100)
 
   123 inductive Prfn :: "nat \<Rightarrow> val \<Rightarrow> rexp \<Rightarrow> bool" ("\<TTurnstile>_ _ : _" [100, 100, 100] 100)
 
   161 where
 
   124 where
 
   162  "\<lbrakk>\<TTurnstile>n1 v1 : r1; \<TTurnstile>n2 v2 : r2\<rbrakk> \<Longrightarrow> \<TTurnstile>(n1 + n2) (Seq v1 v2) : SEQ r1 r2"
 
   125  "\<lbrakk>\<TTurnstile>n1 v1 : r1; \<TTurnstile>n2 v2 : r2\<rbrakk> \<Longrightarrow> \<TTurnstile>(n1 + n2) (Seq v1 v2) : SEQ r1 r2"
 
   163 | "\<TTurnstile>n v1 : r1 \<Longrightarrow> \<TTurnstile>n (Left v1) : ALT r1 r2"
 
   126 | "\<TTurnstile>n v1 : r1 \<Longrightarrow> \<TTurnstile>n (Left v1) : ALT r1 r2"
 
   164 | "\<TTurnstile>n v2 : r2 \<Longrightarrow> \<TTurnstile>n (Right v2) : ALT r1 r2"
 
   127 | "\<TTurnstile>n v2 : r2 \<Longrightarrow> \<TTurnstile>n (Right v2) : ALT r1 r2"
 
   165 | "\<TTurnstile>0 Void : EMPTY"
 
   128 | "\<TTurnstile>0 Void : EMPTY"
 
   166 | "\<TTurnstile>1 (Char c) : CHAR c"
 
   129 | "\<TTurnstile>1 (Char c) : CHAR c"
 
   167 
   130 
   168 lemma Prfn_flat:
 
   131 lemma Prfn_flat:
 
   169   "\<TTurnstile>n v : r \<Longrightarrow> length(flat v) = n"
 
   132   "\<TTurnstile>n v : r \<Longrightarrow> length (flat v) = n"
 
   170 apply(induct rule: Prfn.induct)
 
   133 apply(induct rule: Prfn.induct)
 
   171 apply(auto)
 
   134 apply(auto)
 
   172 done
 
   135 done
 
   173 
   136 
   174 inductive Prf :: "val \<Rightarrow> rexp \<Rightarrow> bool" ("\<turnstile> _ : _" [100, 100] 100)
 
   137 inductive Prf :: "val \<Rightarrow> rexp \<Rightarrow> bool" ("\<turnstile> _ : _" [100, 100] 100)
 
   236 apply(simp)
 
   199 apply(simp)
 
   237 done
 
   200 done
 
   238 
   201 
   239 lemma mkeps_flat:
 
   202 lemma mkeps_flat:
 
   240   assumes "nullable(r)" shows "flat (mkeps r) = []"
 
   203   assumes "nullable(r)" shows "flat (mkeps r) = []"
 
   241 using assms
 
       
   242 apply(induct rule: nullable.induct)
 
       
   243 apply(auto)
 
       
   244 done
 
       
   245 
       
   246 lemma mkeps_flat_left:
 
       
   247   assumes "nullable(r)" shows "flat_left (mkeps r) = []"
 
       
   248 using assms
 
   204 using assms
 
   249 apply(induct rule: nullable.induct)
 
   205 apply(induct rule: nullable.induct)
 
   250 apply(auto)
 
   206 apply(auto)
 
   251 done
 
   207 done
 
   252 
   208 
   273 apply (metis Prf.intros(3) flat.simps(4))
 
   229 apply (metis Prf.intros(3) flat.simps(4))
 
   274 apply(erule Prf.cases)
 
   230 apply(erule Prf.cases)
 
   275 apply(auto)
 
   231 apply(auto)
 
   276 done
 
   232 done
 
   277 
   233 
   278 definition prefix :: "string \<Rightarrow> string \<Rightarrow> bool" ("_ \<sqsubset> _" [100, 100] 100)
 
   234 
   279 where
 
       
   280   "s1 \<sqsubset> s2 \<equiv> \<exists>s3. s1 @ s3 = s2"
 
       
   281 
   235 
   282 section {* Ordering of values *}
 
   236 section {* Ordering of values *}
 
   283 
   237 
   284 inductive ValOrd :: "val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<succ>_ _" [100, 100, 100] 100)
 
   238 inductive ValOrd :: "val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<succ>_ _" [100, 100, 100] 100)
 
   285 where
 
   239 where
 
   431 apply(erule ValOrd.cases)
 
   385 apply(erule ValOrd.cases)
 
   432 apply(simp_all)[8]
 
   386 apply(simp_all)[8]
 
   433 apply(erule ValOrd.cases)
 
   387 apply(erule ValOrd.cases)
 
   434 apply(simp_all)[8]
 
   388 apply(simp_all)[8]
 
   435 done
 
   389 done
 
       
   390 
       
   391 definition prefix :: "string \<Rightarrow> string \<Rightarrow> bool" ("_ \<sqsubseteq> _" [100, 100] 100)
 
       
   392 where
 
       
   393   "s1 \<sqsubseteq> s2 \<equiv> \<exists>s3. s1 @ s3 = s2"
 
       
   394 
       
   395 
       
   396 lemma
 
       
   397   "L r \<noteq> {} \<longrightarrow> (\<exists>vmax \<in> {v. \<turnstile> v : r}. \<forall>v \<in> {v. \<turnstile> v : r \<and> flat v \<sqsubseteq> flat vmax}. vmax 2\<succ> v)"
 
       
   398 apply(induct r)
 
       
   399 apply(simp)
 
       
   400 apply(rule impI)
 
       
   401 apply(simp)
 
       
   402 apply(rule_tac x="Void" in exI)
 
       
   403 apply(simp)
 
       
   404 apply(rule conjI)
 
       
   405 apply (metis Prf.intros(4))
 
       
   406 apply(rule allI)
 
       
   407 apply(rule impI)
 
       
   408 apply(erule conjE)
 
       
   409 apply(erule Prf.cases)
 
       
   410 apply(simp_all)[5]
 
       
   411 apply (metis ValOrd2.intros(7))
 
       
   412 apply(simp)
 
       
   413 apply(rule_tac x="Char char" in exI)
 
       
   414 apply(simp)
 
       
   415 apply(rule conjI)
 
       
   416 apply (metis Prf.intros)
 
       
   417 apply(rule allI)
 
       
   418 apply(rule impI)
 
       
   419 apply(erule conjE)
 
       
   420 apply(erule Prf.cases)
 
       
   421 apply(simp_all)[5]
 
       
   422 apply (metis ValOrd2.intros(8))
 
       
   423 apply(simp)
 
       
   424 apply(rule impI)
 
       
   425 apply(simp add: Sequ_def)[1]
 
       
   426 apply(erule exE)+
 
       
   427 apply(erule conjE)+
 
       
   428 apply(clarify)
 
       
   429 defer
 
       
   430 apply(rule impI)
 
       
   431 apply(drule L_ALT_cases)
 
       
   432 apply(erule disjE)
 
       
   433 apply(simp)
 
       
   434 apply(erule exE)
 
       
   435 apply(clarify)
 
       
   436 apply(rule_tac x="Left vmax" in exI)
 
       
   437 apply(rule conjI)
 
       
   438 apply (metis Prf.intros(2))
 
       
   439 apply(simp)
 
       
   440 apply(rule allI)
 
       
   441 apply(rule impI)
 
       
   442 apply(erule conjE)
 
       
   443 apply(rotate_tac 4)
 
       
   444 apply(erule Prf.cases)
 
       
   445 apply(simp_all)[5]
 
       
   446 apply (metis ValOrd2.intros(6))
 
       
   447 apply(clarify)
 
       
   448 apply (metis ValOrd2.intros(3) length_append ordered_cancel_comm_monoid_diff_class.le_iff_add prefix_def)
 
       
   449 apply(simp)
 
       
   450 apply(clarify)
 
       
   451 apply(rule_tac x="Right vmax" in exI)
 
       
   452 apply(rule conjI)
 
       
   453 apply (metis Prf.intros(3))
 
       
   454 apply(rule allI)
 
       
   455 apply(rule impI)
 
       
   456 apply(erule conjE)+
 
       
   457 apply(simp)
 
       
   458 apply(rotate_tac 4)
 
       
   459 apply(erule Prf.cases)
 
       
   460 apply(simp_all)[5]
 
       
   461 apply (metis Prf_flat_L empty_iff)
 
       
   462 apply (metis ValOrd2.intros(5))
 
       
   463 apply(drule mp)
 
       
   464 apply (metis empty_iff)
 
       
   465 apply(drule mp)
 
       
   466 apply (metis empty_iff)
 
       
   467 apply(erule exE)+
 
       
   468 apply(erule conjE)+
 
       
   469 apply(rule_tac x="Seq vmax vmaxa" in exI)
 
       
   470 apply(rule conjI)
 
       
   471 apply (metis Prf.intros(1))
 
       
   472 apply(rule allI)
 
       
   473 apply(rule impI)
 
       
   474 apply(erule conjE)+
 
       
   475 apply(simp)
 
       
   476 apply(rotate_tac 6)
 
       
   477 apply(erule Prf.cases)
 
       
   478 apply(simp_all)[5]
 
       
   479 apply(auto)
 
       
   480 apply(case_tac "vmax = v1")
 
       
   481 apply(simp)
 
       
   482 apply (simp add: ValOrd2.intros(1) prefix_def)
 
   436 
   483 
   437 lemma
 
   484 lemma
 
   438   "s \<in> L r \<longrightarrow> (\<exists>vmax \<in> {v. \<turnstile> v : r \<and> flat v = s}. \<forall>v \<in> {v. \<turnstile> v : r \<and> flat v = s}. vmax 2\<succ> v)"
 
   485   "s \<in> L r \<longrightarrow> (\<exists>vmax \<in> {v. \<turnstile> v : r \<and> flat v = s}. \<forall>v \<in> {v. \<turnstile> v : r \<and> flat v = s}. vmax 2\<succ> v)"
 
   439 apply(induct s arbitrary: r rule: length_induct)
 
   486 apply(induct s arbitrary: r rule: length_induct)
 
   440 apply(induct_tac r rule: rexp.induct)
 
   487 apply(induct_tac r rule: rexp.induct)
 
  1628 by (metis list.sel(3))
 
  1675 by (metis list.sel(3))
 
  1629 
  1676 
  1630 lemma t2: "(xs = ys) \<Longrightarrow> (c#xs) = (c#ys)"
 
  1677 lemma t2: "(xs = ys) \<Longrightarrow> (c#xs) = (c#ys)"
 
  1631 by (metis)
 
  1678 by (metis)
 
  1632 
  1679 
  1633 fun zeroable where
 
  1680 
  1634   "zeroable NULL = True"
 
       
  1635 | "zeroable EMPTY = False"
 
       
  1636 | "zeroable (CHAR c) = False"
 
       
  1637 | "zeroable (ALT r1 r2) = (zeroable r1 \<and> zeroable r2)"
 
       
  1638 | "zeroable (SEQ r1 r2) = (zeroable r1 \<or> zeroable r2)"
 
       
  1639 
  1681 
  1640 lemma "\<not>(nullable r) \<Longrightarrow> \<not>(\<exists>v. \<turnstile> v : r \<and> flat v = [])"
 
  1682 lemma "\<not>(nullable r) \<Longrightarrow> \<not>(\<exists>v. \<turnstile> v : r \<and> flat v = [])"
 
  1641 by (metis Prf_flat_L nullable_correctness)
 
  1683 by (metis Prf_flat_L nullable_correctness)
 
  1642 
  1684 
  1643 
  1685
lexing