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/Spec.thy
changeset 361 8bb064045b4e
parent 359 fedc16924b76
child 365 ec5e4fe4cc70
equal deleted inserted replaced
360:e752d84225ec 361:8bb064045b4e 
     1    
     1    
     2 theory Spec
 
     2 theory Spec
 
     3   imports RegLangs
 
     3   imports RegLangs
 
     4 begin
 
     4 begin
 
     5 
     5 
     6 
     6 section \<open>"Plain" Values\<close>
 
     7 
       
     8 
       
     9 section {* "Plain" Values *}
 
       
    10 
     7 
    11 datatype val = 
     8 datatype val = 
    12   Void
 
     9   Void
 
    13 | Char char
 
    10 | Char char
 
    14 | Seq val val
 
    11 | Seq val val
 
    15 | Right val
 
    12 | Right val
 
    16 | Left val
 
    13 | Left val
 
    17 | Stars "val list"
 
    14 | Stars "val list"
 
    18 
    15 
    19 
    16 
    20 section {* The string behind a value *}
 
    17 section \<open>The string behind a value\<close>
 
    21 
    18 
    22 fun 
    19 fun 
    23   flat :: "val \<Rightarrow> string"
 
    20   flat :: "val \<Rightarrow> string"
 
    24 where
 
    21 where
 
    25   "flat (Void) = []"
 
    22   "flat (Void) = []"
 
    36 lemma flat_Stars [simp]:
 
    33 lemma flat_Stars [simp]:
 
    37  "flat (Stars vs) = flats vs"
 
    34  "flat (Stars vs) = flats vs"
 
    38 by (induct vs) (auto)
 
    35 by (induct vs) (auto)
 
    39 
    36 
    40 
    37 
    41 section {* Lexical Values *}
 
    38 section \<open>Lexical Values\<close>
 
    42 
    39 
    43 inductive 
    40 inductive 
    44   Prf :: "val \<Rightarrow> rexp \<Rightarrow> bool" ("\<Turnstile> _ : _" [100, 100] 100)
 
    41   Prf :: "val \<Rightarrow> rexp \<Rightarrow> bool" ("\<Turnstile> _ : _" [100, 100] 100)
 
    45 where
 
    42 where
 
    46  "\<lbrakk>\<Turnstile> v1 : r1; \<Turnstile> v2 : r2\<rbrakk> \<Longrightarrow> \<Turnstile>  Seq v1 v2 : SEQ r1 r2"
 
    43  "\<lbrakk>\<Turnstile> v1 : r1; \<Turnstile> v2 : r2\<rbrakk> \<Longrightarrow> \<Turnstile>  Seq v1 v2 : SEQ r1 r2"
 
    47 | "\<Turnstile> v1 : r1 \<Longrightarrow> \<Turnstile> Left v1 : ALT r1 r2"
 
    44 | "\<Turnstile> v1 : r1 \<Longrightarrow> \<Turnstile> Left v1 : ALT r1 r2"
 
    48 | "\<Turnstile> v2 : r2 \<Longrightarrow> \<Turnstile> Right v2 : ALT r1 r2"
 
    45 | "\<Turnstile> v2 : r2 \<Longrightarrow> \<Turnstile> Right v2 : ALT r1 r2"
 
    49 | "\<Turnstile> Void : ONE"
 
    46 | "\<Turnstile> Void : ONE"
 
    50 | "\<Turnstile> Char c : CHAR c"
 
    47 | "\<Turnstile> Char c : CH c"
 
    51 | "\<forall>v \<in> set vs. \<Turnstile> v : r \<and> flat v \<noteq> [] \<Longrightarrow> \<Turnstile> Stars vs : STAR r"
 
    48 | "\<forall>v \<in> set vs. \<Turnstile> v : r \<and> flat v \<noteq> [] \<Longrightarrow> \<Turnstile> Stars vs : STAR r"
 
    52 
    49 
    53 inductive_cases Prf_elims:
 
    50 inductive_cases Prf_elims:
 
    54   "\<Turnstile> v : ZERO"
 
    51   "\<Turnstile> v : ZERO"
 
    55   "\<Turnstile> v : SEQ r1 r2"
 
    52   "\<Turnstile> v : SEQ r1 r2"
 
    56   "\<Turnstile> v : ALT r1 r2"
 
    53   "\<Turnstile> v : ALT r1 r2"
 
    57   "\<Turnstile> v : ONE"
 
    54   "\<Turnstile> v : ONE"
 
    58   "\<Turnstile> v : CHAR c"
 
    55   "\<Turnstile> v : CH c"
 
    59   "\<Turnstile> vs : STAR r"
 
    56   "\<Turnstile> vs : STAR r"
 
    60 
    57 
    61 lemma Prf_Stars_appendE:
 
    58 lemma Prf_Stars_appendE:
 
    62   assumes "\<Turnstile> Stars (vs1 @ vs2) : STAR r"
 
    59   assumes "\<Turnstile> Stars (vs1 @ vs2) : STAR r"
 
    63   shows "\<Turnstile> Stars vs1 : STAR r \<and> \<Turnstile> Stars vs2 : STAR r" 
    60   shows "\<Turnstile> Stars vs1 : STAR r \<and> \<Turnstile> Stars vs2 : STAR r" 
   116   shows "L(r) = {flat v | v. \<Turnstile> v : r}"
 
   113   shows "L(r) = {flat v | v. \<Turnstile> v : r}"
 
   117 using L_flat_Prf1 L_flat_Prf2 by blast
 
   114 using L_flat_Prf1 L_flat_Prf2 by blast
 
   118 
   115 
   119 
   116 
   120 
   117 
   121 section {* Sets of Lexical Values *}
 
   118 section \<open>Sets of Lexical Values\<close>
 
   122 
   119 
   123 text {*
 
   120 text \<open>
 
   124   Shows that lexical values are finite for a given regex and string.
 
   121   Shows that lexical values are finite for a given regex and string.
 
   125 *}
 
   122 \<close>
 
   126 
   123 
   127 definition
 
   124 definition
 
   128   LV :: "rexp \<Rightarrow> string \<Rightarrow> val set"
 
   125   LV :: "rexp \<Rightarrow> string \<Rightarrow> val set"
 
   129 where  "LV r s \<equiv> {v. \<Turnstile> v : r \<and> flat v = s}"
 
   126 where  "LV r s \<equiv> {v. \<Turnstile> v : r \<and> flat v = s}"
 
   130 
   127 
   131 lemma LV_simps:
 
   128 lemma LV_simps:
 
   132   shows "LV ZERO s = {}"
 
   129   shows "LV ZERO s = {}"
 
   133   and   "LV ONE s = (if s = [] then {Void} else {})"
 
   130   and   "LV ONE s = (if s = [] then {Void} else {})"
 
   134   and   "LV (CHAR c) s = (if s = [c] then {Char c} else {})"
 
   131   and   "LV (CH c) s = (if s = [c] then {Char c} else {})"
 
   135   and   "LV (ALT r1 r2) s = Left ` LV r1 s \<union> Right ` LV r2 s"
 
   132   and   "LV (ALT r1 r2) s = Left ` LV r1 s \<union> Right ` LV r2 s"
 
   136 unfolding LV_def
 
   133 unfolding LV_def
 
   137 by (auto intro: Prf.intros elim: Prf.cases)
 
   134 by (auto intro: Prf.intros elim: Prf.cases)
 
   138 
   135 
   139 
   136 
   227   show "finite (LV ZERO s)" by (simp add: LV_simps)
 
   224   show "finite (LV ZERO s)" by (simp add: LV_simps)
 
   228 next
 
   225 next
 
   229   case (ONE s)
 
   226   case (ONE s)
 
   230   show "finite (LV ONE s)" by (simp add: LV_simps)
 
   227   show "finite (LV ONE s)" by (simp add: LV_simps)
 
   231 next
 
   228 next
 
   232   case (CHAR c s)
 
   229   case (CH c s)
 
   233   show "finite (LV (CHAR c) s)" by (simp add: LV_simps)
 
   230   show "finite (LV (CH c) s)" by (simp add: LV_simps)
 
   234 next 
   231 next 
   235   case (ALT r1 r2 s)
 
   232   case (ALT r1 r2 s)
 
   236   then show "finite (LV (ALT r1 r2) s)" by (simp add: LV_simps)
 
   233   then show "finite (LV (ALT r1 r2) s)" by (simp add: LV_simps)
 
   237 next 
   234 next 
   238   case (SEQ r1 r2 s)
 
   235   case (SEQ r1 r2 s)
 
   256   then show "finite (LV (STAR r) s)" by (simp add: LV_STAR_finite)
 
   253   then show "finite (LV (STAR r) s)" by (simp add: LV_STAR_finite)
 
   257 qed
 
   254 qed
 
   258 
   255 
   259 
   256 
   260 
   257 
   261 section {* Our inductive POSIX Definition *}
 
   258 section \<open>Our inductive POSIX Definition\<close>
 
   262 
   259 
   263 inductive 
   260 inductive 
   264   Posix :: "string \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<in> _ \<rightarrow> _" [100, 100, 100] 100)
 
   261   Posix :: "string \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<in> _ \<rightarrow> _" [100, 100, 100] 100)
 
   265 where
 
   262 where
 
   266   Posix_ONE: "[] \<in> ONE \<rightarrow> Void"
 
   263   Posix_ONE: "[] \<in> ONE \<rightarrow> Void"
 
   267 | Posix_CHAR: "[c] \<in> (CHAR c) \<rightarrow> (Char c)"
 
   264 | Posix_CH: "[c] \<in> (CH c) \<rightarrow> (Char c)"
 
   268 | Posix_ALT1: "s \<in> r1 \<rightarrow> v \<Longrightarrow> s \<in> (ALT r1 r2) \<rightarrow> (Left v)"
 
   265 | Posix_ALT1: "s \<in> r1 \<rightarrow> v \<Longrightarrow> s \<in> (ALT r1 r2) \<rightarrow> (Left v)"
 
   269 | Posix_ALT2: "\<lbrakk>s \<in> r2 \<rightarrow> v; s \<notin> L(r1)\<rbrakk> \<Longrightarrow> s \<in> (ALT r1 r2) \<rightarrow> (Right v)"
 
   266 | Posix_ALT2: "\<lbrakk>s \<in> r2 \<rightarrow> v; s \<notin> L(r1)\<rbrakk> \<Longrightarrow> s \<in> (ALT r1 r2) \<rightarrow> (Right v)"
 
   270 | Posix_SEQ: "\<lbrakk>s1 \<in> r1 \<rightarrow> v1; s2 \<in> r2 \<rightarrow> v2;
 
   267 | Posix_SEQ: "\<lbrakk>s1 \<in> r1 \<rightarrow> v1; s2 \<in> r2 \<rightarrow> v2;
 
   271     \<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> 
   268     \<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> 
   272     (s1 @ s2) \<in> (SEQ r1 r2) \<rightarrow> (Seq v1 v2)"
 
   269     (s1 @ s2) \<in> (SEQ r1 r2) \<rightarrow> (Seq v1 v2)"
 
   276 | Posix_STAR2: "[] \<in> STAR r \<rightarrow> Stars []"
 
   273 | Posix_STAR2: "[] \<in> STAR r \<rightarrow> Stars []"
 
   277 
   274 
   278 inductive_cases Posix_elims:
 
   275 inductive_cases Posix_elims:
 
   279   "s \<in> ZERO \<rightarrow> v"
 
   276   "s \<in> ZERO \<rightarrow> v"
 
   280   "s \<in> ONE \<rightarrow> v"
 
   277   "s \<in> ONE \<rightarrow> v"
 
   281   "s \<in> CHAR c \<rightarrow> v"
 
   278   "s \<in> CH c \<rightarrow> v"
 
   282   "s \<in> ALT r1 r2 \<rightarrow> v"
 
   279   "s \<in> ALT r1 r2 \<rightarrow> v"
 
   283   "s \<in> SEQ r1 r2 \<rightarrow> v"
 
   280   "s \<in> SEQ r1 r2 \<rightarrow> v"
 
   284   "s \<in> STAR r \<rightarrow> v"
 
   281   "s \<in> STAR r \<rightarrow> v"
 
   285 
   282 
   286 lemma Posix1:
 
   283 lemma Posix1:
 
   287   assumes "s \<in> r \<rightarrow> v"
 
   284   assumes "s \<in> r \<rightarrow> v"
 
   288   shows "s \<in> L r" "flat v = s"
 
   285   shows "s \<in> L r" "flat v = s"
 
   289 using assms
 
   286 using assms
 
   290 by (induct s r v rule: Posix.induct)
 
   287   by(induct s r v rule: Posix.induct)
 
   291    (auto simp add: Sequ_def)
 
   288     (auto simp add: Sequ_def)
 
   292 
   289 
   293 text {*
 
   290 text \<open>
 
   294   For a give value and string, our Posix definition 
   291   For a give value and string, our Posix definition 
   295   determines a unique value.
 
   292   determines a unique value.
 
   296 *}
 
   293 \<close>
 
   297 
   294 
   298 lemma Posix_determ:
 
   295 lemma Posix_determ:
 
   299   assumes "s \<in> r \<rightarrow> v1" "s \<in> r \<rightarrow> v2"
 
   296   assumes "s \<in> r \<rightarrow> v1" "s \<in> r \<rightarrow> v2"
 
   300   shows "v1 = v2"
 
   297   shows "v1 = v2"
 
   301 using assms
 
   298 using assms
 
   302 proof (induct s r v1 arbitrary: v2 rule: Posix.induct)
 
   299 proof (induct s r v1 arbitrary: v2 rule: Posix.induct)
 
   303   case (Posix_ONE v2)
 
   300   case (Posix_ONE v2)
 
   304   have "[] \<in> ONE \<rightarrow> v2" by fact
 
   301   have "[] \<in> ONE \<rightarrow> v2" by fact
 
   305   then show "Void = v2" by cases auto
 
   302   then show "Void = v2" by cases auto
 
   306 next 
   303 next 
   307   case (Posix_CHAR c v2)
 
   304   case (Posix_CH c v2)
 
   308   have "[c] \<in> CHAR c \<rightarrow> v2" by fact
 
   305   have "[c] \<in> CH c \<rightarrow> v2" by fact
 
   309   then show "Char c = v2" by cases auto
 
   306   then show "Char c = v2" by cases auto
 
   310 next 
   307 next 
   311   case (Posix_ALT1 s r1 v r2 v2)
 
   308   case (Posix_ALT1 s r1 v r2 v2)
 
   312   have "s \<in> ALT r1 r2 \<rightarrow> v2" by fact
 
   309   have "s \<in> ALT r1 r2 \<rightarrow> v2" by fact
 
   313   moreover
 
   310   moreover
 
   360   have "[] \<in> STAR r \<rightarrow> v2" by fact
 
   357   have "[] \<in> STAR r \<rightarrow> v2" by fact
 
   361   then show "Stars [] = v2" by cases (auto simp add: Posix1)
 
   358   then show "Stars [] = v2" by cases (auto simp add: Posix1)
 
   362 qed
 
   359 qed
 
   363 
   360 
   364 
   361 
   365 text {*
 
   362 text \<open>
 
   366   Our POSIX values are lexical values.
 
   363   Our POSIX values are lexical values.
 
   367 *}
 
   364 \<close>
 
   368 
   365 
   369 lemma Posix_LV:
 
   366 lemma Posix_LV:
 
   370   assumes "s \<in> r \<rightarrow> v"
 
   367   assumes "s \<in> r \<rightarrow> v"
 
   371   shows "v \<in> LV r s"
 
   368   shows "v \<in> LV r s"
 
   372   using assms unfolding LV_def
 
   369   using assms unfolding LV_def
lexing