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 62 a6bb0152ccc2
parent 56 5bc72d6d633d
child 63 498171d2379a
equal deleted inserted replaced
60:2cdbab037861 62:a6bb0152ccc2 
    40 | "L (EMPTY) = {[]}"
 
    40 | "L (EMPTY) = {[]}"
 
    41 | "L (CHAR c) = {[c]}"
 
    41 | "L (CHAR c) = {[c]}"
 
    42 | "L (SEQ r1 r2) = (L r1) ;; (L r2)"
 
    42 | "L (SEQ r1 r2) = (L r1) ;; (L r2)"
 
    43 | "L (ALT r1 r2) = (L r1) \<union> (L r2)"
 
    43 | "L (ALT r1 r2) = (L r1) \<union> (L r2)"
 
    44 
    44 
       
    45 fun
 
       
    46  nullable :: "rexp \<Rightarrow> bool"
 
       
    47 where
 
       
    48   "nullable (NULL) = False"
 
       
    49 | "nullable (EMPTY) = True"
 
       
    50 | "nullable (CHAR c) = False"
 
       
    51 | "nullable (ALT r1 r2) = (nullable r1 \<or> nullable r2)"
 
       
    52 | "nullable (SEQ r1 r2) = (nullable r1 \<and> nullable r2)"
 
       
    53 
       
    54 lemma nullable_correctness:
 
       
    55   shows "nullable r  \<longleftrightarrow> [] \<in> (L r)"
 
       
    56 apply (induct r) 
       
    57 apply(auto simp add: Sequ_def) 
       
    58 done
 
    45 
    59 
    46 section {* Values *}
 
    60 section {* Values *}
 
    47 
    61 
    48 datatype val = 
    62 datatype val = 
    49   Void
 
    63   Void
 
    50 | Char char
 
    64 | Char char
 
    51 | Seq val val
 
    65 | Seq val val
 
    52 | Right val
 
    66 | Right val
 
    53 | Left val
 
    67 | Left val
 
       
    68 
       
    69 section {* The string behind a value *}
 
       
    70 
       
    71 fun flat :: "val \<Rightarrow> string"
 
       
    72 where
 
       
    73   "flat(Void) = []"
 
       
    74 | "flat(Char c) = [c]"
 
       
    75 | "flat(Left v) = flat(v)"
 
       
    76 | "flat(Right v) = flat(v)"
 
       
    77 | "flat(Seq v1 v2) = flat(v1) @ flat(v2)"
 
       
    78 
       
    79 fun flats :: "val \<Rightarrow> string list"
 
       
    80 where
 
       
    81   "flats(Void) = [[]]"
 
       
    82 | "flats(Char c) = [[c]]"
 
       
    83 | "flats(Left v) = flats(v)"
 
       
    84 | "flats(Right v) = flats(v)"
 
       
    85 | "flats(Seq v1 v2) = (flats v1) @ (flats v2)"
 
       
    86 
    54 
    87 
    55 section {* Relation between values and regular expressions *}
 
    88 section {* Relation between values and regular expressions *}
 
    56 
    89 
    57 inductive Prf :: "val \<Rightarrow> rexp \<Rightarrow> bool" ("\<turnstile> _ : _" [100, 100] 100)
 
    90 inductive Prf :: "val \<Rightarrow> rexp \<Rightarrow> bool" ("\<turnstile> _ : _" [100, 100] 100)
 
    58 where
 
    91 where
 
    60 | "\<turnstile> v1 : r1 \<Longrightarrow> \<turnstile> Left v1 : ALT r1 r2"
 
    93 | "\<turnstile> v1 : r1 \<Longrightarrow> \<turnstile> Left v1 : ALT r1 r2"
 
    61 | "\<turnstile> v2 : r2 \<Longrightarrow> \<turnstile> Right v2 : ALT r1 r2"
 
    94 | "\<turnstile> v2 : r2 \<Longrightarrow> \<turnstile> Right v2 : ALT r1 r2"
 
    62 | "\<turnstile> Void : EMPTY"
 
    95 | "\<turnstile> Void : EMPTY"
 
    63 | "\<turnstile> Char c : CHAR c"
 
    96 | "\<turnstile> Char c : CHAR c"
 
    64 
    97 
    65 section {* The string behind a value *}
 
    98 fun mkeps :: "rexp \<Rightarrow> val"
 
    66 
       
    67 fun flat :: "val \<Rightarrow> string"
 
       
    68 where
 
    99 where
 
    69   "flat(Void) = []"
 
   100   "mkeps(EMPTY) = Void"
 
    70 | "flat(Char c) = [c]"
 
   101 | "mkeps(SEQ r1 r2) = Seq (mkeps r1) (mkeps r2)"
 
    71 | "flat(Left v) = flat(v)"
 
   102 | "mkeps(ALT r1 r2) = (if nullable(r1) then Left (mkeps r1) else Right (mkeps r2))"
 
    72 | "flat(Right v) = flat(v)"
 
   103 
    73 | "flat(Seq v1 v2) = flat(v1) @ flat(v2)"
 
   104 lemma mkeps_nullable:
 
    74 
   105   assumes "nullable(r)" shows "\<turnstile> mkeps r : r"
 
    75 fun flats :: "val \<Rightarrow> string list"
 
   106 using assms
 
    76 where
 
   107 apply(induct rule: nullable.induct)
 
    77   "flats(Void) = [[]]"
 
   108 apply(auto intro: Prf.intros)
 
    78 | "flats(Char c) = [[c]]"
 
   109 done
 
    79 | "flats(Left v) = flats(v)"
 
   110 
    80 | "flats(Right v) = flats(v)"
 
   111 
    81 | "flats(Seq v1 v2) = (flats v1) @ (flats v2)"
 
   112 
       
   113 lemma mkeps_flat:
 
       
   114   assumes "nullable(r)" shows "flat (mkeps r) = []"
 
       
   115 using assms
 
       
   116 apply(induct rule: nullable.induct)
 
       
   117 apply(auto)
 
       
   118 done
 
       
   119 
       
   120 text {*
 
       
   121   The value mkeps returns is always the correct POSIX
 
       
   122   value.
 
       
   123 *}
 
    82 
   124 
    83 lemma Prf_flat_L:
 
   125 lemma Prf_flat_L:
 
    84   assumes "\<turnstile> v : r" shows "flat v \<in> L r"
 
   126   assumes "\<turnstile> v : r" shows "flat v \<in> L r"
 
    85 using assms
 
   127 using assms
 
    86 apply(induct)
 
   128 apply(induct)
 
   106 
   148 
   107 section {* Ordering of values *}
 
   149 section {* Ordering of values *}
 
   108 
   150 
   109 inductive ValOrd :: "val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<succ>_ _" [100, 100, 100] 100)
 
   151 inductive ValOrd :: "val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<succ>_ _" [100, 100, 100] 100)
 
   110 where
 
   152 where
 
   111   "\<lbrakk>v1 = v1'; v2 \<succ>r2 v2'\<rbrakk> \<Longrightarrow> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1' v2')" 
   153   "v2 \<succ>r2 v2' \<Longrightarrow> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1 v2')" 
   112 | "v1  \<succ>r1 v1' \<Longrightarrow> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1' v2')" 
   154 | "\<lbrakk>v1 \<succ>r1 v1'; v1 \<noteq> v1'\<rbrakk> \<Longrightarrow> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1' v2')" 
   113 | "length (flat v1) \<ge> length (flat v2) \<Longrightarrow> (Left v1) \<succ>(ALT r1 r2) (Right v2)"
 
   155 | "length (flat v1) \<ge> length (flat v2) \<Longrightarrow> (Left v1) \<succ>(ALT r1 r2) (Right v2)"
 
   114 | "length (flat v2) > length (flat v1) \<Longrightarrow> (Right v2) \<succ>(ALT r1 r2) (Left v1)"
 
   156 | "length (flat v2) > length (flat v1) \<Longrightarrow> (Right v2) \<succ>(ALT r1 r2) (Left v1)"
 
   115 | "v2 \<succ>r2 v2' \<Longrightarrow> (Right v2) \<succ>(ALT r1 r2) (Right v2')"
 
   157 | "v2 \<succ>r2 v2' \<Longrightarrow> (Right v2) \<succ>(ALT r1 r2) (Right v2')"
 
   116 | "v1 \<succ>r1 v1' \<Longrightarrow> (Left v1) \<succ>(ALT r1 r2) (Left v1')"
 
   158 | "v1 \<succ>r1 v1' \<Longrightarrow> (Left v1) \<succ>(ALT r1 r2) (Left v1')"
 
   117 | "Void \<succ>EMPTY Void"
 
   159 | "Void \<succ>EMPTY Void"
 
   126 using assms
 
   168 using assms
 
   127 apply(induct)
 
   169 apply(induct)
 
   128 apply(auto intro: ValOrd.intros)
 
   170 apply(auto intro: ValOrd.intros)
 
   129 done
 
   171 done
 
   130 
   172 
   131 lemma ValOrd_flats:
 
       
   132   assumes "v1 \<succ>r v2"
 
       
   133   shows "hd (flats v2) = hd (flats v1)"
 
       
   134 using assms
 
       
   135 apply(induct)
 
       
   136 apply(auto)
 
       
   137 oops
 
       
   138 
       
   139 
       
   140 section {* Posix definition *}
 
   173 section {* Posix definition *}
 
   141 
   174 
   142 definition POSIX :: "val \<Rightarrow> rexp \<Rightarrow> bool" 
   175 definition POSIX :: "val \<Rightarrow> rexp \<Rightarrow> bool" 
   143 where
 
   176 where
 
   144   "POSIX v r \<equiv> (\<forall>v'. (\<turnstile> v' : r \<and> flat v = flat v') \<longrightarrow> v \<succ>r v')"
 
   177   "POSIX v r \<equiv> (\<turnstile> v : r \<and> (\<forall>v'. (\<turnstile> v' : r \<and> flat v = flat v') \<longrightarrow> v \<succ>r v'))"
 
   145 
   178 
   146 (*
 
   179 (*
 
   147 an alternative definition: might cause problems
 
   180 an alternative definition: might cause problems
 
   148 with theorem mkeps_POSIX
 
   181 with theorem mkeps_POSIX
 
   149 *)
 
   182 *)
 
   150 
   183 
       
   184 (*
 
   151 definition POSIX2 :: "val \<Rightarrow> rexp \<Rightarrow> bool" 
   185 definition POSIX2 :: "val \<Rightarrow> rexp \<Rightarrow> bool" 
   152 where
 
   186 where
 
   153   "POSIX2 v r \<equiv> \<turnstile> v : r \<and> (\<forall>v'. \<turnstile> v' : r \<longrightarrow> v \<succ>r v')"
 
   187   "POSIX2 v r \<equiv> \<turnstile> v : r \<and> (\<forall>v'. \<turnstile> v' : r \<longrightarrow> v \<succ>r v')"
 
   154 
   188 *)
 
       
   189 
       
   190 (*
 
   155 definition POSIX3 :: "val \<Rightarrow> rexp \<Rightarrow> bool" 
   191 definition POSIX3 :: "val \<Rightarrow> rexp \<Rightarrow> bool" 
   156 where
 
   192 where
 
   157   "POSIX3 v r \<equiv> \<turnstile> v : r \<and> (\<forall>v'. (\<turnstile> v' : r \<and> length (flat v') \<le> length(flat v)) \<longrightarrow> v \<succ>r v')"
 
   193   "POSIX3 v r \<equiv> \<turnstile> v : r \<and> (\<forall>v'. (\<turnstile> v' : r \<and> length (flat v') \<le> length(flat v)) \<longrightarrow> v \<succ>r v')"
 
   158 
   194 *)
 
   159 
   195 
   160 lemma POSIX_SEQ:
 
   196 lemma POSIX_SEQ1:
 
   161   assumes "POSIX (Seq v1 v2) (SEQ r1 r2)" "\<turnstile> v1 : r1" "\<turnstile> v2 : r2"
 
   197   assumes "POSIX (Seq v1 v2) (SEQ r1 r2)" "\<turnstile> v1 : r1" "\<turnstile> v2 : r2"
 
   162   shows "POSIX v1 r1 \<and> POSIX v2 r2"
 
   198   shows "POSIX v1 r1"
 
   163 using assms
 
   199 using assms
 
   164 unfolding POSIX_def
 
   200 unfolding POSIX_def
 
   165 apply(auto)
 
   201 apply(auto)
 
   166 apply(drule_tac x="Seq v' v2" in spec)
 
   202 apply(drule_tac x="Seq v' v2" in spec)
 
   167 apply(simp)
 
   203 apply(simp)
 
   170 apply(simp)
 
   206 apply(simp)
 
   171 apply(simp)
 
   207 apply(simp)
 
   172 apply(erule ValOrd.cases)
 
   208 apply(erule ValOrd.cases)
 
   173 apply(simp_all)
 
   209 apply(simp_all)
 
   174 apply(clarify)
 
   210 apply(clarify)
 
   175 defer
 
   211 by (metis ValOrd_refl)
 
       
   212 
       
   213 lemma POSIX_SEQ2:
 
       
   214   assumes "POSIX (Seq v1 v2) (SEQ r1 r2)" "\<turnstile> v1 : r1" "\<turnstile> v2 : r2" 
       
   215   shows "POSIX v2 r2"
 
       
   216 using assms
 
       
   217 unfolding POSIX_def
 
       
   218 apply(auto)
 
   176 apply(drule_tac x="Seq v1 v'" in spec)
 
   219 apply(drule_tac x="Seq v1 v'" in spec)
 
   177 apply(simp)
 
   220 apply(simp)
 
   178 apply(erule impE)
 
   221 apply(erule impE)
 
   179 apply(rule Prf.intros)
 
   222 apply(rule Prf.intros)
 
   180 apply(simp)
 
   223 apply(simp)
 
   181 apply(simp)
 
   224 apply(simp)
 
   182 apply(erule ValOrd.cases)
 
   225 apply(erule ValOrd.cases)
 
   183 apply(simp_all)
 
   226 apply(simp_all)
 
   184 apply(clarify)
 
   227 done
 
   185 oops (*not true*)
 
       
   186 
       
   187 lemma POSIX_SEQ_I:
 
       
   188   assumes "POSIX v1 r1" "POSIX v2 r2" 
       
   189   shows "POSIX (Seq v1 v2) (SEQ r1 r2)" 
       
   190 using assms
 
       
   191 unfolding POSIX_def
 
       
   192 apply(auto)
 
       
   193 apply(rotate_tac 2)
 
       
   194 apply(erule Prf.cases)
 
       
   195 apply(simp_all)[5]
 
       
   196 apply(auto)[1]
 
       
   197 apply(rule ValOrd.intros)
 
       
   198 oops (* maybe also not true *)
 
       
   199 
       
   200 lemma POSIX3_SEQ_I:
 
       
   201   assumes "POSIX3 v1 r1" "POSIX3 v2 r2" 
       
   202   shows "POSIX3 (Seq v1 v2) (SEQ r1 r2)" 
       
   203 using assms
 
       
   204 unfolding POSIX3_def
 
       
   205 apply(auto)
 
       
   206 apply (metis Prf.intros(1))
 
       
   207 apply(rotate_tac 4)
 
       
   208 apply(erule Prf.cases)
 
       
   209 apply(simp_all)[5]
 
       
   210 apply(auto)[1]
 
       
   211 apply(case_tac "v1 = v1a")
 
       
   212 apply(auto)
 
       
   213 apply (metis ValOrd.intros(1))
 
       
   214 apply (rule ValOrd.intros(2))
 
       
   215 oops
 
       
   216 
   228 
   217 lemma POSIX_ALT2:
 
   229 lemma POSIX_ALT2:
 
   218   assumes "POSIX (Left v1) (ALT r1 r2)"
 
   230   assumes "POSIX (Left v1) (ALT r1 r2)"
 
   219   shows "POSIX v1 r1"
 
   231   shows "POSIX v1 r1"
 
   220 using assms
 
   232 using assms
 
   221 unfolding POSIX_def
 
   233 unfolding POSIX_def
 
   222 apply(auto)
 
   234 apply(auto)
 
       
   235 apply(erule Prf.cases)
 
       
   236 apply(simp_all)[5]
 
   223 apply(drule_tac x="Left v'" in spec)
 
   237 apply(drule_tac x="Left v'" in spec)
 
   224 apply(simp)
 
   238 apply(simp)
 
   225 apply(drule mp)
 
   239 apply(drule mp)
 
   226 apply(rule Prf.intros)
 
   240 apply(rule Prf.intros)
 
   227 apply(auto)
 
   241 apply(auto)
 
   228 apply(erule ValOrd.cases)
 
   242 apply(erule ValOrd.cases)
 
   229 apply(simp_all)
 
   243 apply(simp_all)
 
   230 done
 
   244 done
 
   231 
       
   232 lemma POSIX2_ALT:
 
       
   233   assumes "POSIX2 (Left v1) (ALT r1 r2)"
 
       
   234   shows "POSIX2 v1 r1"
 
       
   235 using assms
 
       
   236 unfolding POSIX2_def
 
       
   237 apply(auto)
 
       
   238 oops
 
       
   239 
       
   240 lemma POSIX_ALT:
 
       
   241   assumes "POSIX (Left v1) (ALT r1 r2)"
 
       
   242   shows "POSIX v1 r1"
 
       
   243 using assms
 
       
   244 unfolding POSIX_def
 
       
   245 apply(auto)
 
       
   246 apply(drule_tac x="Left v'" in spec)
 
       
   247 apply(simp)
 
       
   248 apply(drule mp)
 
       
   249 apply(rule Prf.intros)
 
       
   250 apply(auto)
 
       
   251 apply(erule ValOrd.cases)
 
       
   252 apply(simp_all)
 
       
   253 done
 
       
   254 
       
   255 lemma POSIX2_ALT:
 
       
   256   assumes "POSIX2 (Left v1) (ALT r1 r2)"
 
       
   257   shows "POSIX2 v1 r1"
 
       
   258 using assms
 
       
   259 apply(simp add: POSIX2_def)
 
       
   260 apply(auto)
 
       
   261 apply(erule Prf.cases)
 
       
   262 apply(simp_all)[5]
 
       
   263 apply(drule_tac x="Left v'" in spec)
 
       
   264 apply(drule mp)
 
       
   265 apply(rule Prf.intros)
 
       
   266 apply(auto)
 
       
   267 apply(erule ValOrd.cases)
 
       
   268 apply(simp_all)
 
       
   269 done
 
       
   270 
       
   271 
   245 
   272 lemma POSIX_ALT1a:
 
   246 lemma POSIX_ALT1a:
 
   273   assumes "POSIX (Right v2) (ALT r1 r2)"
 
   247   assumes "POSIX (Right v2) (ALT r1 r2)"
 
   274   shows "POSIX v2 r2"
 
   248   shows "POSIX v2 r2"
 
   275 using assms
 
   249 using assms
 
   276 unfolding POSIX_def
 
   250 unfolding POSIX_def
 
   277 apply(auto)
 
   251 apply(auto)
 
       
   252 apply(erule Prf.cases)
 
       
   253 apply(simp_all)[5]
 
   278 apply(drule_tac x="Right v'" in spec)
 
   254 apply(drule_tac x="Right v'" in spec)
 
   279 apply(simp)
 
   255 apply(simp)
 
   280 apply(drule mp)
 
   256 apply(drule mp)
 
   281 apply(rule Prf.intros)
 
   257 apply(rule Prf.intros)
 
   282 apply(auto)
 
   258 apply(auto)
 
   283 apply(erule ValOrd.cases)
 
   259 apply(erule ValOrd.cases)
 
   284 apply(simp_all)
 
   260 apply(simp_all)
 
   285 done
 
   261 done
 
   286 
       
   287 lemma POSIX2_ALT1a:
 
       
   288   assumes "POSIX2 (Right v2) (ALT r1 r2)"
 
       
   289   shows "POSIX2 v2 r2"
 
       
   290 using assms
 
       
   291 unfolding POSIX2_def
 
       
   292 apply(auto)
 
       
   293 apply(erule Prf.cases)
 
       
   294 apply(simp_all)[5]
 
       
   295 apply(drule_tac x="Right v'" in spec)
 
       
   296 apply(drule mp)
 
       
   297 apply(rule Prf.intros)
 
       
   298 apply(auto)
 
       
   299 apply(erule ValOrd.cases)
 
       
   300 apply(simp_all)
 
       
   301 done
 
       
   302 
       
   303 
   262 
   304 lemma POSIX_ALT1b:
 
   263 lemma POSIX_ALT1b:
 
   305   assumes "POSIX (Right v2) (ALT r1 r2)"
 
   264   assumes "POSIX (Right v2) (ALT r1 r2)"
 
   306   shows "(\<forall>v'. (\<turnstile> v' : r2 \<and> flat v' = flat v2) \<longrightarrow> v2 \<succ>r2 v')"
 
   265   shows "(\<forall>v'. (\<turnstile> v' : r2 \<and> flat v' = flat v2) \<longrightarrow> v2 \<succ>r2 v')"
 
   307 using assms
 
   266 using assms
 
   314   assumes "POSIX v1 r1" 
   273   assumes "POSIX v1 r1" 
   315   shows "POSIX (Left v1) (ALT r1 r2)"
 
   274   shows "POSIX (Left v1) (ALT r1 r2)"
 
   316 using assms
 
   275 using assms
 
   317 unfolding POSIX_def
 
   276 unfolding POSIX_def
 
   318 apply(auto)
 
   277 apply(auto)
 
   319 apply(rotate_tac 3)
 
   278 apply (metis Prf.intros(2))
 
       
   279 apply(rotate_tac 2)
 
   320 apply(erule Prf.cases)
 
   280 apply(erule Prf.cases)
 
   321 apply(simp_all)[5]
 
   281 apply(simp_all)[5]
 
   322 apply(auto)
 
   282 apply(auto)
 
   323 apply(rule ValOrd.intros)
 
   283 apply(rule ValOrd.intros)
 
   324 apply(auto)
 
   284 apply(auto)
 
   325 apply(rule ValOrd.intros)
 
   285 apply(rule ValOrd.intros)
 
   326 by simp
 
   286 by simp
 
   327 
   287 
   328 lemma POSIX2_ALT_I1:
 
       
   329   assumes "POSIX2 v1 r1" 
       
   330   shows "POSIX2 (Left v1) (ALT r1 r2)"
 
       
   331 using assms
 
       
   332 unfolding POSIX2_def
 
       
   333 apply(auto)
 
       
   334 apply(rule Prf.intros)
 
       
   335 apply(simp)
 
       
   336 apply(rotate_tac 2)
 
       
   337 apply(erule Prf.cases)
 
       
   338 apply(simp_all)[5]
 
       
   339 apply(auto)
 
       
   340 apply(rule ValOrd.intros)
 
       
   341 apply(auto)
 
       
   342 apply(rule ValOrd.intros)
 
       
   343 oops
 
       
   344 
   288 
   345 lemma POSIX_ALT_I2:
 
   289 lemma POSIX_ALT_I2:
 
   346   assumes "POSIX v2 r2" "\<forall>v'. \<turnstile> v' : r1 \<longrightarrow> length (flat v2) > length (flat v')"
 
   290   assumes "POSIX v2 r2" "\<forall>v'. \<turnstile> v' : r1 \<longrightarrow> length (flat v2) > length (flat v')"
 
   347   shows "POSIX (Right v2) (ALT r1 r2)"
 
   291   shows "POSIX (Right v2) (ALT r1 r2)"
 
   348 using assms
 
   292 using assms
 
   349 unfolding POSIX_def
 
   293 unfolding POSIX_def
 
   350 apply(auto)
 
   294 apply(auto)
 
       
   295 apply (metis Prf.intros)
 
   351 apply(rotate_tac 3)
 
   296 apply(rotate_tac 3)
 
   352 apply(erule Prf.cases)
 
   297 apply(erule Prf.cases)
 
   353 apply(simp_all)[5]
 
   298 apply(simp_all)[5]
 
   354 apply(auto)
 
   299 apply(auto)
 
   355 apply(rule ValOrd.intros)
 
   300 apply(rule ValOrd.intros)
 
   356 apply metis
 
   301 apply metis
 
   357 done
 
   302 done
 
   358 
       
   359 
       
   360 
       
   361 section {* The Matcher *}
 
       
   362 
       
   363 fun
 
       
   364  nullable :: "rexp \<Rightarrow> bool"
 
       
   365 where
 
       
   366   "nullable (NULL) = False"
 
       
   367 | "nullable (EMPTY) = True"
 
       
   368 | "nullable (CHAR c) = False"
 
       
   369 | "nullable (ALT r1 r2) = (nullable r1 \<or> nullable r2)"
 
       
   370 | "nullable (SEQ r1 r2) = (nullable r1 \<and> nullable r2)"
 
       
   371 
       
   372 lemma nullable_correctness:
 
       
   373   shows "nullable r  \<longleftrightarrow> [] \<in> (L r)"
 
       
   374 apply (induct r) 
       
   375 apply(auto simp add: Sequ_def) 
       
   376 done
 
       
   377 
       
   378 fun mkeps :: "rexp \<Rightarrow> val"
 
       
   379 where
 
       
   380   "mkeps(EMPTY) = Void"
 
       
   381 | "mkeps(SEQ r1 r2) = Seq (mkeps r1) (mkeps r2)"
 
       
   382 | "mkeps(ALT r1 r2) = (if nullable(r1) then Left (mkeps r1) else Right (mkeps r2))"
 
       
   383 
       
   384 lemma mkeps_nullable:
 
       
   385   assumes "nullable(r)" shows "\<turnstile> mkeps r : r"
 
       
   386 using assms
 
       
   387 apply(induct rule: nullable.induct)
 
       
   388 apply(auto intro: Prf.intros)
 
       
   389 done
 
       
   390 
       
   391 lemma mkeps_flat:
 
       
   392   assumes "nullable(r)" shows "flat (mkeps r) = []"
 
       
   393 using assms
 
       
   394 apply(induct rule: nullable.induct)
 
       
   395 apply(auto)
 
       
   396 done
 
       
   397 
       
   398 text {*
 
       
   399   The value mkeps returns is always the correct POSIX
 
       
   400   value.
 
       
   401 *}
 
       
   402 
       
   403 lemma mkeps_POSIX2:
 
       
   404   assumes "nullable r"
 
       
   405   shows "POSIX2 (mkeps r) r"
 
       
   406 using assms
 
       
   407 apply(induct r)
 
       
   408 apply(auto)[1]
 
       
   409 apply(simp add: POSIX2_def)
 
       
   410 oops
 
       
   411 
       
   412 lemma mkeps_POSIX3:
 
       
   413   assumes "nullable r"
 
       
   414   shows "POSIX3 (mkeps r) r"
 
       
   415 using assms
 
       
   416 apply(induct r)
 
       
   417 apply(auto)[1]
 
       
   418 apply(simp add: POSIX3_def)
 
       
   419 apply(auto)[1]
 
       
   420 apply (metis Prf.intros(4))
 
       
   421 apply(erule Prf.cases)
 
       
   422 apply(simp_all)[5]
 
       
   423 apply (metis ValOrd.intros)
 
       
   424 apply(simp add: POSIX3_def)
 
       
   425 apply(auto)[1]
 
       
   426 apply(simp add: POSIX3_def)
 
       
   427 apply(auto)[1]
 
       
   428 apply (metis mkeps.simps(2) mkeps_nullable nullable.simps(5))
 
       
   429 apply(rotate_tac 6)
 
       
   430 apply(erule Prf.cases)
 
       
   431 apply(simp_all)[5]
 
       
   432 apply (metis ValOrd.intros(2) add_leE gen_length_code(1) gen_length_def mkeps_flat)
 
       
   433 apply(auto)
 
       
   434 apply(simp add: POSIX3_def)
 
       
   435 apply(auto)
 
       
   436 apply (metis Prf.intros(2))
 
       
   437 apply(rotate_tac 4)
 
       
   438 apply(erule Prf.cases)
 
       
   439 apply(simp_all)[5]
 
       
   440 apply (metis ValOrd.intros(6))
 
       
   441 apply(auto)[1]
 
       
   442 apply (metis ValOrd.intros(3))
 
       
   443 apply(simp add: POSIX3_def)
 
       
   444 apply(auto)
 
       
   445 apply (metis Prf.intros(2))
 
       
   446 apply(rotate_tac 6)
 
       
   447 apply(erule Prf.cases)
 
       
   448 apply(simp_all)[5]
 
       
   449 apply (metis ValOrd.intros(6))
 
       
   450 apply (metis ValOrd.intros(3))
 
       
   451 apply(simp add: POSIX3_def)
 
       
   452 apply(auto)
 
       
   453 apply (metis Prf.intros(3))
 
       
   454 apply(rotate_tac 5)
 
       
   455 apply(erule Prf.cases)
 
       
   456 apply(simp_all)[5]
 
       
   457 apply (metis Prf_flat_L drop_0 drop_all list.size(3) mkeps_flat nullable_correctness)
 
       
   458 by (metis ValOrd.intros(5))
 
       
   459 
       
   460 
   303 
   461 lemma mkeps_POSIX:
 
   304 lemma mkeps_POSIX:
 
   462   assumes "nullable r"
 
   305   assumes "nullable r"
 
   463   shows "POSIX (mkeps r) r"
 
   306   shows "POSIX (mkeps r) r"
 
   464 using assms
 
   307 using assms
 
   465 apply(induct r)
 
   308 apply(induct r)
 
   466 apply(auto)[1]
 
   309 apply(auto)[1]
 
   467 apply(simp add: POSIX_def)
 
   310 apply(simp add: POSIX_def)
 
   468 apply(auto)[1]
 
   311 apply(auto)[1]
 
       
   312 apply (metis Prf.intros(4))
 
   469 apply(erule Prf.cases)
 
   313 apply(erule Prf.cases)
 
   470 apply(simp_all)[5]
 
   314 apply(simp_all)[5]
 
   471 apply (metis ValOrd.intros)
 
   315 apply (metis ValOrd.intros)
 
   472 apply(simp add: POSIX_def)
 
   316 apply(simp add: POSIX_def)
 
   473 apply(auto)[1]
 
   317 apply(auto)[1]
 
   474 apply(simp add: POSIX_def)
 
   318 apply(simp add: POSIX_def)
 
   475 apply(auto)[1]
 
   319 apply(auto)[1]
 
   476 apply(erule Prf.cases)
 
   320 apply (metis mkeps.simps(2) mkeps_nullable nullable.simps(5))
 
   477 apply(simp_all)[5]
 
       
   478 apply(auto)
 
       
   479 apply (simp add: ValOrd.intros(2) mkeps_flat)
 
       
   480 apply(simp add: POSIX_def)
 
       
   481 apply(auto)[1]
 
       
   482 apply(erule Prf.cases)
 
       
   483 apply(simp_all)[5]
 
       
   484 apply(auto)
 
       
   485 apply (simp add: ValOrd.intros(6))
 
       
   486 apply (simp add: ValOrd.intros(3))
 
       
   487 apply(simp add: POSIX_def)
 
       
   488 apply(auto)[1]
 
       
   489 apply(erule Prf.cases)
 
       
   490 apply(simp_all)[5]
 
       
   491 apply(auto)
 
       
   492 apply (simp add: ValOrd.intros(6))
 
       
   493 apply (simp add: ValOrd.intros(3))
 
       
   494 apply(simp add: POSIX_def)
 
       
   495 apply(auto)[1]
 
       
   496 apply(erule Prf.cases)
 
       
   497 apply(simp_all)[5]
 
       
   498 apply(auto)
 
       
   499 apply (metis Prf_flat_L mkeps_flat nullable_correctness)
 
       
   500 by (simp add: ValOrd.intros(5))
 
       
   501 
       
   502 
       
   503 lemma mkeps_POSIX2:
 
       
   504   assumes "nullable r"
 
       
   505   shows "POSIX2 (mkeps r) r"
 
       
   506 using assms
 
       
   507 apply(induct r)
 
       
   508 apply(simp)
 
       
   509 apply(simp)
 
       
   510 apply(simp add: POSIX2_def)
 
       
   511 apply(rule conjI)
 
       
   512 apply(rule Prf.intros)
 
       
   513 apply(auto)[1]
 
       
   514 apply(erule Prf.cases)
 
       
   515 apply(simp_all)[5]
 
       
   516 apply(rule ValOrd.intros)
 
       
   517 apply(simp)
 
       
   518 apply(simp)
 
       
   519 apply(simp add: POSIX2_def)
 
       
   520 apply(rule conjI)
 
       
   521 apply(rule Prf.intros)
 
       
   522 apply(simp add: mkeps_nullable)
 
       
   523 apply(simp add: mkeps_nullable)
 
       
   524 apply(auto)[1]
 
       
   525 apply(rotate_tac 6)
 
   321 apply(rotate_tac 6)
 
   526 apply(erule Prf.cases)
 
   322 apply(erule Prf.cases)
 
   527 apply(simp_all)[5]
 
   323 apply(simp_all)[5]
 
   528 apply(rule ValOrd.intros(2))
 
   324 apply (simp add: mkeps_flat)
 
   529 apply(simp)
 
   325 apply(case_tac "mkeps r1a = v1")
 
   530 apply(simp only: nullable.simps)
 
   326 apply(simp)
 
       
   327 apply (metis ValOrd.intros(1))
 
       
   328 apply (rule ValOrd.intros(2))
 
       
   329 apply metis
 
       
   330 apply(simp)
 
       
   331 apply(simp)
 
   531 apply(erule disjE)
 
   332 apply(erule disjE)
 
   532 apply(simp)
 
   333 apply(simp)
 
   533 thm POSIX2_ALT1a
 
   334 apply (metis POSIX_ALT_I1)
 
   534 apply(rule POSIX2_ALT)
 
   335 apply(auto)
 
   535 apply(simp add: POSIX2_def)
 
   336 apply (metis POSIX_ALT_I1)
 
   536 apply(rule conjI)
 
   337 apply(simp add: POSIX_def)
 
   537 apply(rule Prf.intros)
 
   338 apply(auto)[1]
 
   538 apply(simp add: mkeps_nullable)
 
   339 apply (metis Prf.intros(3))
 
   539 oops
 
   340 apply(rotate_tac 5)
 
       
   341 apply(erule Prf.cases)
 
       
   342 apply(simp_all)[5]
 
       
   343 apply(simp add: mkeps_flat)
 
       
   344 apply(auto)[1]
 
       
   345 apply (metis Prf_flat_L nullable_correctness)
 
       
   346 apply(rule ValOrd.intros)
 
       
   347 by metis
 
   540 
   348 
   541 
   349 
   542 section {* Derivatives *}
 
   350 section {* Derivatives *}
 
   543 
   351 
   544 fun
 
   352 fun
 
   722 by (metis list.inject v4_proj)
 
   530 by (metis list.inject v4_proj)
 
   723 
   531 
   724 lemma t: "(c#xs = c#ys) \<Longrightarrow> xs = ys"
 
   532 lemma t: "(c#xs = c#ys) \<Longrightarrow> xs = ys"
 
   725 by (metis list.sel(3))
 
   533 by (metis list.sel(3))
 
   726 
   534 
       
   535 lemma t2: "(xs = ys) \<Longrightarrow> (c#xs) = (c#ys)"
 
       
   536 by (metis)
 
       
   537 
       
   538 fun zeroable where
 
       
   539   "zeroable NULL = True"
 
       
   540 | "zeroable EMPTY = False"
 
       
   541 | "zeroable (CHAR c) = False"
 
       
   542 | "zeroable (ALT r1 r2) = (zeroable r1 \<and> zeroable r2)"
 
       
   543 | "zeroable (SEQ r1 r2) = (zeroable r1 \<or> zeroable r2)"
 
       
   544 
       
   545 lemma "\<not>(nullable r) \<Longrightarrow> \<not>(\<exists>v. \<turnstile> v : r \<and> flat v = [])"
 
       
   546 by (metis Prf_flat_L nullable_correctness)
 
       
   547 
   727 lemma Prf_inj:
 
   548 lemma Prf_inj:
 
   728   assumes "v1 \<succ>(der c r) v2" "\<turnstile> v1 : der c r" "\<turnstile> v2 : der c r"
 
   549   assumes "v1 \<succ>(der c r) v2" "\<turnstile> v1 : der c r" "\<turnstile> v2 : der c r" (*"flat v1 = flat v2"*)
 
   729   shows "(injval r c v1) \<succ>r (injval r c v2)"
 
   550   shows "(injval r c v1) \<succ>r (injval r c v2)"
 
   730 using assms
 
   551 using assms
 
   731 apply(induct arbitrary: v1 v2 rule: der.induct)
 
   552 apply(induct arbitrary: v1 v2 rule: der.induct)
 
   732 (* NULL case *)
 
   553 (* NULL case *)
 
   733 apply(simp)
 
   554 apply(simp)
 
   760 apply(rotate_tac 2)
 
   581 apply(rotate_tac 2)
 
   761 apply(erule Prf.cases)
 
   582 apply(erule Prf.cases)
 
   762 apply(simp_all)[5]
 
   583 apply(simp_all)[5]
 
   763 apply(simp)
 
   584 apply(simp)
 
   764 apply(rule ValOrd.intros)
 
   585 apply(rule ValOrd.intros)
 
       
   586 apply(clarify)
 
       
   587 apply(rotate_tac 3)
 
       
   588 apply(erule Prf.cases)
 
       
   589 apply(simp_all)[5]
 
       
   590 apply(clarify)
 
       
   591 apply(erule Prf.cases)
 
       
   592 apply(simp_all)[5]
 
       
   593 apply(clarify)
 
   765 apply(subst v4)
 
   594 apply(subst v4)
 
   766 apply(clarify)
 
   595 apply(simp)
 
       
   596 apply(subst v4)
 
       
   597 apply(simp)
 
       
   598 apply(simp)
 
       
   599 apply(rule ValOrd.intros)
 
       
   600 apply(clarify)
 
       
   601 apply(erule Prf.cases)
 
       
   602 apply(simp_all)[5]
 
       
   603 apply(erule Prf.cases)
 
       
   604 apply(simp_all)[5]
 
       
   605 apply(rule ValOrd.intros)
 
       
   606 apply(clarify)
 
       
   607 apply(erule Prf.cases)
 
       
   608 apply(simp_all)[5]
 
       
   609 apply(erule Prf.cases)
 
       
   610 apply(simp_all)[5]
 
       
   611 (* SEQ case*)
 
       
   612 apply(simp)
 
       
   613 apply(case_tac "nullable r1")
 
       
   614 apply(simp)
 
       
   615 defer
 
       
   616 apply(simp)
 
       
   617 apply(erule Prf.cases)
 
       
   618 apply(simp_all)[5]
 
       
   619 apply(erule Prf.cases)
 
       
   620 apply(simp_all)[5]
 
       
   621 apply(clarify)
 
       
   622 apply(erule ValOrd.cases)
 
       
   623 apply(simp_all)[8]
 
       
   624 apply(clarify)
 
       
   625 apply(rule ValOrd.intros)
 
       
   626 apply(simp)
 
       
   627 apply(clarify)
 
       
   628 apply(rule ValOrd.intros(2))
 
       
   629 apply metis
 
       
   630 
       
   631 apply(erule Prf.cases)
 
       
   632 apply(simp_all)[5]
 
       
   633 apply(erule Prf.cases)
 
       
   634 apply(simp_all)[5]
 
       
   635 apply(clarify)
 
       
   636 defer
 
       
   637 apply(erule ValOrd.cases)
 
       
   638 apply(simp_all del: injval.simps)[8]
 
       
   639 apply(simp)
 
       
   640 apply(clarify)
 
       
   641 apply(simp)
 
       
   642 apply(erule Prf.cases)
 
       
   643 apply(simp_all)[5]
 
       
   644 apply(erule Prf.cases)
 
       
   645 apply(simp_all)[5]
 
       
   646 apply(clarify)
 
       
   647 apply(erule Prf.cases)
 
       
   648 apply(simp_all)[5]
 
       
   649 apply(clarify)
 
       
   650 apply(rule ValOrd.intros(2))
 
       
   651 
       
   652 
       
   653 lemma POSIX_ex: "\<turnstile> v : r \<Longrightarrow> \<exists>v. POSIX v r"
 
       
   654 apply(induct r arbitrary: v)
 
       
   655 apply(erule Prf.cases)
 
       
   656 apply(simp_all)[5]
 
       
   657 apply(erule Prf.cases)
 
       
   658 apply(simp_all)[5]
 
       
   659 apply(rule_tac x="Void" in exI)
 
       
   660 apply(simp add: POSIX_def)
 
       
   661 apply(auto)[1]
 
       
   662 apply (metis Prf.intros(4))
 
       
   663 apply(erule Prf.cases)
 
       
   664 apply(simp_all)[5]
 
       
   665 apply (metis ValOrd.intros(7))
 
       
   666 apply(erule Prf.cases)
 
       
   667 apply(simp_all)[5]
 
       
   668 apply(rule_tac x="Char c" in exI)
 
       
   669 apply(simp add: POSIX_def)
 
       
   670 apply(auto)[1]
 
       
   671 apply (metis Prf.intros(5))
 
       
   672 apply(erule Prf.cases)
 
       
   673 apply(simp_all)[5]
 
       
   674 apply (metis ValOrd.intros(8))
 
       
   675 apply(erule Prf.cases)
 
       
   676 apply(simp_all)[5]
 
       
   677 apply(auto)[1]
 
       
   678 apply(drule_tac x="v1" in meta_spec)
 
       
   679 apply(drule_tac x="v2" in meta_spec)
 
       
   680 apply(auto)[1]
 
       
   681 defer
 
       
   682 apply(erule Prf.cases)
 
       
   683 apply(simp_all)[5]
 
       
   684 apply(auto)[1]
 
       
   685 apply (metis POSIX_ALT_I1)
 
       
   686 apply (metis POSIX_ALT_I1 POSIX_ALT_I2)
 
       
   687 apply(case_tac "nullable r1a")
 
       
   688 apply(rule_tac x="Seq (mkeps r1a) va" in exI)
 
       
   689 apply(auto simp add: POSIX_def)[1]
 
       
   690 apply (metis Prf.intros(1) mkeps_nullable)
 
       
   691 apply(simp add: mkeps_flat)
 
       
   692 apply(rotate_tac 7)
 
       
   693 apply(erule Prf.cases)
 
       
   694 apply(simp_all)[5]
 
       
   695 apply(case_tac "mkeps r1 = v1a")
 
       
   696 apply(simp)
 
       
   697 apply (rule ValOrd.intros(1))
 
       
   698 apply (metis append_Nil mkeps_flat)
 
       
   699 apply (rule ValOrd.intros(2))
 
       
   700 apply(drule mkeps_POSIX)
 
       
   701 apply(simp add: POSIX_def)
 
       
   702 
       
   703 apply metis
 
       
   704 apply(simp)
 
       
   705 apply(simp)
 
       
   706 apply(erule disjE)
 
       
   707 apply(simp)
 
       
   708 
       
   709 apply(drule_tac x="v2" in spec)
 
       
   710 
       
   711 lemma POSIX_ex2: "\<turnstile> v : r \<Longrightarrow> \<exists>v. POSIX v r \<and> \<turnstile> v : r"
 
       
   712 apply(induct r arbitrary: v)
 
       
   713 apply(erule Prf.cases)
 
       
   714 apply(simp_all)[5]
 
       
   715 apply(erule Prf.cases)
 
       
   716 apply(simp_all)[5]
 
       
   717 apply(rule_tac x="Void" in exI)
 
       
   718 apply(simp add: POSIX_def)
 
       
   719 apply(auto)[1]
 
       
   720 apply(erule Prf.cases)
 
       
   721 apply(simp_all)[5]
 
       
   722 apply (metis ValOrd.intros(7))
 
       
   723 apply (metis Prf.intros(4))
 
       
   724 apply(erule Prf.cases)
 
       
   725 apply(simp_all)[5]
 
       
   726 apply(rule_tac x="Char c" in exI)
 
       
   727 apply(simp add: POSIX_def)
 
       
   728 apply(auto)[1]
 
       
   729 apply(erule Prf.cases)
 
       
   730 apply(simp_all)[5]
 
       
   731 apply (metis ValOrd.intros(8))
 
       
   732 apply (metis Prf.intros(5))
 
       
   733 apply(erule Prf.cases)
 
       
   734 apply(simp_all)[5]
 
       
   735 apply(auto)[1]
 
       
   736 apply(drule_tac x="v1" in meta_spec)
 
       
   737 apply(drule_tac x="v2" in meta_spec)
 
       
   738 apply(auto)[1]
 
       
   739 apply(simp add: POSIX_def)
 
       
   740 apply(auto)[1]
 
       
   741 apply(rule ccontr)
 
       
   742 apply(simp)
 
       
   743 apply(drule_tac x="Seq v va" in spec)
 
       
   744 apply(drule mp)
 
       
   745 defer
 
       
   746 apply (metis Prf.intros(1))
 
       
   747 
       
   748 
       
   749 oops
 
       
   750 
       
   751 lemma POSIX_ALT_cases:
 
       
   752   assumes "\<turnstile> v : (ALT r1 r2)" "POSIX v (ALT r1 r2)"
 
       
   753   shows "(\<exists>v1. v = Left v1 \<and> POSIX v1 r1) \<or> (\<exists>v2. v = Right v2 \<and> POSIX v2 r2)"
 
       
   754 using assms
 
       
   755 apply(erule_tac Prf.cases)
 
       
   756 apply(simp_all)
 
       
   757 unfolding POSIX_def
 
       
   758 apply(auto)
 
       
   759 apply (metis POSIX_ALT2 POSIX_def assms(2))
 
       
   760 by (metis POSIX_ALT1b assms(2))
 
       
   761 
       
   762 lemma POSIX_ALT_cases2:
 
       
   763   assumes "POSIX v (ALT r1 r2)" "\<turnstile> v : (ALT r1 r2)" 
       
   764   shows "(\<exists>v1. v = Left v1 \<and> POSIX v1 r1) \<or> (\<exists>v2. v = Right v2 \<and> POSIX v2 r2)"
 
       
   765 using assms POSIX_ALT_cases by auto
 
       
   766 
       
   767 lemma Prf_flat_empty:
 
       
   768   assumes "\<turnstile> v : r" "flat v = []"
 
       
   769   shows "nullable r"
 
       
   770 using assms
 
       
   771 apply(induct)
 
       
   772 apply(auto)
 
       
   773 done
 
       
   774 
       
   775 lemma POSIX_proj:
 
       
   776   assumes "POSIX v r" "\<turnstile> v : r" "\<exists>s. flat v = c#s"
 
       
   777   shows "POSIX (projval r c v) (der c r)"
 
       
   778 using assms
 
       
   779 apply(induct r c v arbitrary: rule: projval.induct)
 
       
   780 defer
 
       
   781 defer
 
       
   782 defer
 
       
   783 defer
 
       
   784 apply(erule Prf.cases)
 
       
   785 apply(simp_all)[5]
 
       
   786 apply(erule Prf.cases)
 
       
   787 apply(simp_all)[5]
 
       
   788 apply(erule Prf.cases)
 
       
   789 apply(simp_all)[5]
 
       
   790 apply(erule Prf.cases)
 
       
   791 apply(simp_all)[5]
 
       
   792 apply(erule Prf.cases)
 
       
   793 apply(simp_all)[5]
 
       
   794 apply(erule Prf.cases)
 
       
   795 apply(simp_all)[5]
 
       
   796 apply(erule Prf.cases)
 
       
   797 apply(simp_all)[5]
 
       
   798 apply(erule Prf.cases)
 
       
   799 apply(simp_all)[5]
 
       
   800 apply(erule Prf.cases)
 
       
   801 apply(simp_all)[5]
 
       
   802 apply(erule Prf.cases)
 
       
   803 apply(simp_all)[5]
 
       
   804 apply(simp add: POSIX_def)
 
       
   805 apply(auto)[1]
 
       
   806 apply(erule Prf.cases)
 
       
   807 apply(simp_all)[5]
 
       
   808 apply (metis ValOrd.intros(7))
 
       
   809 apply(erule_tac [!] exE)
 
       
   810 prefer 3
 
       
   811 apply(frule POSIX_SEQ1)
 
       
   812 apply(erule Prf.cases)
 
       
   813 apply(simp_all)[5]
 
       
   814 apply(erule Prf.cases)
 
       
   815 apply(simp_all)[5]
 
       
   816 apply(case_tac "flat v1 = []")
 
       
   817 apply(subgoal_tac "nullable r1")
 
       
   818 apply(simp)
 
       
   819 prefer 2
 
       
   820 apply(rule_tac v="v1" in Prf_flat_empty)
 
       
   821 apply(erule Prf.cases)
 
       
   822 apply(simp_all)[5]
 
       
   823 apply(simp)
 
       
   824 apply(frule POSIX_SEQ2)
 
       
   825 apply(erule Prf.cases)
 
       
   826 apply(simp_all)[5]
 
       
   827 apply(erule Prf.cases)
 
       
   828 apply(simp_all)[5]
 
       
   829 apply(simp)
 
       
   830 apply(drule meta_mp)
 
       
   831 apply(erule Prf.cases)
 
       
   832 apply(simp_all)[5]
 
       
   833 apply(rule ccontr)
 
       
   834 apply(subgoal_tac "\<turnstile> val.Right (projval r2 c v2) : (ALT (SEQ (der c r1) r2) (der c r2))")
 
       
   835 apply(rotate_tac 11)
 
       
   836 apply(frule POSIX_ex)
 
       
   837 apply(erule exE)
 
       
   838 apply(drule POSIX_ALT_cases2)
 
       
   839 apply(erule Prf.cases)
 
       
   840 apply(simp_all)[5]
 
       
   841 apply(drule v3_proj)
 
       
   842 apply(simp)
 
       
   843 apply(simp)
 
       
   844 apply(drule POSIX_ex)
 
       
   845 apply(erule exE)
 
       
   846 apply(frule POSIX_ALT_cases2)
 
       
   847 apply(simp)
 
       
   848 apply(simp)
 
       
   849 apply(erule 
       
   850 prefer 2
 
       
   851 apply(case_tac "nullable r1")
 
       
   852 prefer 2
 
       
   853 apply(simp)
 
       
   854 apply(rotate_tac 1)
 
       
   855 apply(drule meta_mp)
 
       
   856 apply(rule POSIX_SEQ1)
 
       
   857 apply(assumption)
 
       
   858 apply(erule Prf.cases)
 
       
   859 apply(simp_all)[5]
 
       
   860 apply(erule Prf.cases)
 
       
   861 apply(simp_all)[5]
 
       
   862 apply(rotate_tac 7)
 
       
   863 apply(drule meta_mp)
 
       
   864 apply(erule Prf.cases)
 
       
   865 apply(simp_all)[5]
 
       
   866 apply(rotate_tac 7)
 
       
   867 apply(drule meta_mp)
 
       
   868 apply (metis Cons_eq_append_conv)
 
       
   869 
       
   870 
       
   871 apply(erule Prf.cases)
 
       
   872 apply(simp_all)[5]
 
       
   873 apply(simp add: POSIX_def)
 
       
   874 apply(simp)
 
       
   875 apply(simp)
 
       
   876 apply(simp_all)[5]
 
       
   877 apply(simp add: POSIX_def)
 
       
   878 
       
   879 
       
   880 lemma POSIX_proj:
 
       
   881   assumes "POSIX v r" "\<turnstile> v : r" "\<exists>s. flat v = c#s"
 
       
   882   shows "POSIX (projval r c v) (der c r)"
 
       
   883 using assms
 
       
   884 apply(induct r arbitrary: c v rule: rexp.induct)
 
       
   885 apply(erule Prf.cases)
 
       
   886 apply(simp_all)[5]
 
       
   887 apply(erule Prf.cases)
 
       
   888 apply(simp_all)[5]
 
       
   889 apply(erule Prf.cases)
 
       
   890 apply(simp_all)[5]
 
       
   891 apply(simp add: POSIX_def)
 
       
   892 apply(auto)[1]
 
       
   893 apply(erule Prf.cases)
 
       
   894 apply(simp_all)[5]
 
       
   895 apply (metis ValOrd.intros(7))
 
       
   896 
       
   897 apply(erule Prf.cases)
 
       
   898 apply(simp_all)[5]
 
       
   899 apply(erule Prf.cases)
 
       
   900 apply(simp_all)[5]
 
       
   901 apply(erule Prf.cases)
 
       
   902 apply(simp_all)[5]
 
       
   903 apply(erule Prf.cases)
 
       
   904 apply(simp_all)[5]
 
       
   905 apply(erule Prf.cases)
 
       
   906 apply(simp_all)[5]
 
       
   907 apply(erule Prf.cases)
 
       
   908 apply(simp_all)[5]
 
       
   909 apply(simp add: POSIX_def)
 
       
   910 apply(auto)[1]
 
       
   911 apply(erule Prf.cases)
 
       
   912 apply(simp_all)[5]
 
       
   913 apply (metis ValOrd.intros(7))
 
       
   914 apply(erule_tac [!] exE)
 
       
   915 prefer 3
 
       
   916 apply(frule POSIX_SEQ1)
 
       
   917 apply(erule Prf.cases)
 
       
   918 apply(simp_all)[5]
 
       
   919 apply(erule Prf.cases)
 
       
   920 apply(simp_all)[5]
 
       
   921 apply(case_tac "flat v1 = []")
 
       
   922 apply(subgoal_tac "nullable r1")
 
       
   923 apply(simp)
 
       
   924 prefer 2
 
       
   925 apply(rule_tac v="v1" in Prf_flat_empty)
 
       
   926 apply(erule Prf.cases)
 
       
   927 apply(simp_all)[5]
 
       
   928 
       
   929 
       
   930 lemma POSIX_proj:
 
       
   931   assumes "POSIX v r" "\<turnstile> v : r" "\<exists>s. flat v = c#s"
 
       
   932   shows "POSIX (projval r c v) (der c r)"
 
       
   933 using assms
 
       
   934 apply(induct r c v arbitrary: rule: projval.induct)
 
       
   935 defer
 
       
   936 defer
 
       
   937 defer
 
       
   938 defer
 
       
   939 apply(erule Prf.cases)
 
       
   940 apply(simp_all)[5]
 
       
   941 apply(erule Prf.cases)
 
       
   942 apply(simp_all)[5]
 
       
   943 apply(erule Prf.cases)
 
       
   944 apply(simp_all)[5]
 
       
   945 apply(erule Prf.cases)
 
       
   946 apply(simp_all)[5]
 
       
   947 apply(erule Prf.cases)
 
       
   948 apply(simp_all)[5]
 
       
   949 apply(erule Prf.cases)
 
       
   950 apply(simp_all)[5]
 
       
   951 apply(erule Prf.cases)
 
       
   952 apply(simp_all)[5]
 
       
   953 apply(erule Prf.cases)
 
       
   954 apply(simp_all)[5]
 
       
   955 apply(erule Prf.cases)
 
       
   956 apply(simp_all)[5]
 
       
   957 apply(erule Prf.cases)
 
       
   958 apply(simp_all)[5]
 
       
   959 apply(simp add: POSIX_def)
 
       
   960 apply(auto)[1]
 
       
   961 apply(erule Prf.cases)
 
       
   962 apply(simp_all)[5]
 
       
   963 apply (metis ValOrd.intros(7))
 
       
   964 apply(erule_tac [!] exE)
 
       
   965 prefer 3
 
       
   966 apply(frule POSIX_SEQ1)
 
       
   967 apply(erule Prf.cases)
 
       
   968 apply(simp_all)[5]
 
       
   969 apply(erule Prf.cases)
 
       
   970 apply(simp_all)[5]
 
       
   971 apply(case_tac "flat v1 = []")
 
       
   972 apply(subgoal_tac "nullable r1")
 
       
   973 apply(simp)
 
       
   974 prefer 2
 
       
   975 apply(rule_tac v="v1" in Prf_flat_empty)
 
       
   976 apply(erule Prf.cases)
 
       
   977 apply(simp_all)[5]
 
       
   978 apply(simp)
 
       
   979 apply(rule ccontr)
 
       
   980 apply(drule v3_proj)
 
       
   981 apply(simp)
 
       
   982 apply(simp)
 
       
   983 apply(drule POSIX_ex)
 
       
   984 apply(erule exE)
 
       
   985 apply(frule POSIX_ALT_cases2)
 
       
   986 apply(simp)
 
       
   987 apply(simp)
 
       
   988 apply(erule 
       
   989 prefer 2
 
       
   990 apply(case_tac "nullable r1")
 
       
   991 prefer 2
 
       
   992 apply(simp)
 
       
   993 apply(rotate_tac 1)
 
       
   994 apply(drule meta_mp)
 
       
   995 apply(rule POSIX_SEQ1)
 
       
   996 apply(assumption)
 
       
   997 apply(erule Prf.cases)
 
       
   998 apply(simp_all)[5]
 
       
   999 apply(erule Prf.cases)
 
       
  1000 apply(simp_all)[5]
 
       
  1001 apply(rotate_tac 7)
 
       
  1002 apply(drule meta_mp)
 
       
  1003 apply(erule Prf.cases)
 
       
  1004 apply(simp_all)[5]
 
       
  1005 apply(rotate_tac 7)
 
       
  1006 apply(drule meta_mp)
 
       
  1007 apply (metis Cons_eq_append_conv)
 
       
  1008 
       
  1009 
       
  1010 apply(erule Prf.cases)
 
       
  1011 apply(simp_all)[5]
 
       
  1012 apply(simp add: POSIX_def)
 
       
  1013 apply(simp)
 
       
  1014 apply(simp)
 
       
  1015 apply(simp_all)[5]
 
       
  1016 apply(simp add: POSIX_def)
 
       
  1017 
       
  1018 done
 
       
  1019 (* NULL case *)
 
       
  1020 apply(simp add: POSIX_def)
 
       
  1021 apply(auto)[1]
 
       
  1022 apply(erule Prf.cases)
 
       
  1023 apply(simp_all)[5]
 
       
  1024 apply(erule Prf.cases)
 
       
  1025 apply(simp_all)[5]
 
       
  1026 apply (metis ValOrd.intros(7))
 
       
  1027 apply(rotate_tac 4)
 
       
  1028 apply(erule Prf.cases)
 
       
  1029 apply(simp_all)[5]
 
       
  1030 apply(simp)
 
       
  1031 prefer 2
 
       
  1032 apply(simp)
 
       
  1033 apply(frule POSIX_ALT1a)
 
       
  1034 apply(drule meta_mp)
 
       
  1035 apply(simp)
 
       
  1036 apply(drule meta_mp)
 
       
  1037 apply(erule Prf.cases)
 
       
  1038 apply(simp_all)[5]
 
       
  1039 apply(rule POSIX_ALT_I2)
 
       
  1040 apply(assumption)
 
       
  1041 apply(auto)[1]
 
       
  1042 
       
  1043 thm v4_proj2
 
       
  1044 prefer 2
 
       
  1045 apply(subst (asm) (13) POSIX_def)
 
       
  1046 
       
  1047 apply(drule_tac x="projval v2" in spec)
 
       
  1048 apply(auto)[1]
 
       
  1049 apply(drule mp)
 
       
  1050 apply(rule conjI)
 
       
  1051 apply(simp)
 
       
  1052 apply(simp)
 
       
  1053 
       
  1054 apply(erule Prf.cases)
 
       
  1055 apply(simp_all)[5]
 
       
  1056 apply(erule Prf.cases)
 
       
  1057 apply(simp_all)[5]
 
       
  1058 prefer 2
 
       
  1059 apply(clarify)
 
       
  1060 apply(subst (asm) (2) POSIX_def)
 
       
  1061 
       
  1062 apply (metis ValOrd.intros(5))
 
       
  1063 apply(clarify)
 
       
  1064 apply(simp)
 
   767 apply(rotate_tac 3)
 
  1065 apply(rotate_tac 3)
 
   768 apply(erule Prf.cases)
 
  1066 apply(drule_tac c="c" in t2)
 
   769 apply(simp_all)[5]
 
  1067 apply(subst (asm) v4_proj)
 
       
  1068 apply(simp)
 
       
  1069 apply(simp)
 
       
  1070 thm contrapos_np contrapos_nn
 
       
  1071 apply(erule contrapos_np)
 
       
  1072 apply(rule ValOrd.intros)
 
       
  1073 apply(subst  v4_proj2)
 
       
  1074 apply(simp)
 
       
  1075 apply(simp)
 
       
  1076 apply(subgoal_tac "\<not>(length (flat v1) < length (flat (projval r2a c v2a)))")
 
       
  1077 prefer 2
 
       
  1078 apply(erule contrapos_nn)
 
       
  1079 apply (metis nat_less_le v4_proj2)
 
       
  1080 apply(simp)
 
       
  1081 
       
  1082 apply(blast)
 
       
  1083 thm contrapos_nn
 
       
  1084 
       
  1085 apply(simp add: POSIX_def)
 
       
  1086 apply(auto)[1]
 
       
  1087 apply(erule Prf.cases)
 
       
  1088 apply(simp_all)[5]
 
       
  1089 apply(erule Prf.cases)
 
       
  1090 apply(simp_all)[5]
 
       
  1091 apply(clarify)
 
       
  1092 apply(rule ValOrd.intros)
 
       
  1093 apply(drule meta_mp)
 
       
  1094 apply(auto)[1]
 
       
  1095 apply (metis POSIX_ALT2 POSIX_def flat.simps(3))
 
       
  1096 apply metis
 
       
  1097 apply(clarify)
 
       
  1098 apply(rule ValOrd.intros)
 
       
  1099 apply(simp)
 
       
  1100 apply(simp add: POSIX_def)
 
       
  1101 apply(auto)[1]
 
       
  1102 apply(erule Prf.cases)
 
       
  1103 apply(simp_all)[5]
 
       
  1104 apply(erule Prf.cases)
 
       
  1105 apply(simp_all)[5]
 
       
  1106 apply(clarify)
 
       
  1107 apply(rule ValOrd.intros)
 
       
  1108 apply(simp)
 
       
  1109 
       
  1110 apply(drule meta_mp)
 
       
  1111 apply(auto)[1]
 
       
  1112 apply (metis POSIX_ALT2 POSIX_def flat.simps(3))
 
       
  1113 apply metis
 
       
  1114 apply(clarify)
 
       
  1115 apply(rule ValOrd.intros)
 
       
  1116 apply(simp)
 
       
  1117 
       
  1118 
       
  1119 done
 
       
  1120 (* EMPTY case *)
 
       
  1121 apply(simp add: POSIX_def)
 
       
  1122 apply(auto)[1]
 
       
  1123 apply(rotate_tac 3)
 
       
  1124 apply(erule Prf.cases)
 
       
  1125 apply(simp_all)[5]
 
       
  1126 apply(drule_tac c="c" in t2)
 
       
  1127 apply(subst (asm) v4_proj)
 
       
  1128 apply(auto)[2]
 
       
  1129 
       
  1130 apply(erule ValOrd.cases)
 
       
  1131 apply(simp_all)[8]
 
       
  1132 (* CHAR case *)
 
       
  1133 apply(case_tac "c = c'")
 
       
  1134 apply(simp)
 
       
  1135 apply(erule ValOrd.cases)
 
       
  1136 apply(simp_all)[8]
 
       
  1137 apply(rule ValOrd.intros)
 
       
  1138 apply(simp)
 
       
  1139 apply(erule ValOrd.cases)
 
       
  1140 apply(simp_all)[8]
 
       
  1141 (* ALT case *)
 
       
  1142 
       
  1143 
       
  1144 unfolding POSIX_def
 
       
  1145 apply(auto)
 
       
  1146 thm v4
 
       
  1147 
       
  1148 lemma Prf_inj:
 
       
  1149   assumes "v1 \<succ>(der c r) v2" "\<turnstile> v1 : der c r" "\<turnstile> v2 : der c r" "flat v1 = flat v2"
 
       
  1150   shows "(injval r c v1) \<succ>r (injval r c v2)"
 
       
  1151 using assms
 
       
  1152 apply(induct arbitrary: v1 v2 rule: der.induct)
 
       
  1153 (* NULL case *)
 
       
  1154 apply(simp)
 
       
  1155 apply(erule ValOrd.cases)
 
       
  1156 apply(simp_all)[8]
 
       
  1157 (* EMPTY case *)
 
       
  1158 apply(erule ValOrd.cases)
 
       
  1159 apply(simp_all)[8]
 
       
  1160 (* CHAR case *)
 
       
  1161 apply(case_tac "c = c'")
 
       
  1162 apply(simp)
 
       
  1163 apply(erule ValOrd.cases)
 
       
  1164 apply(simp_all)[8]
 
       
  1165 apply(rule ValOrd.intros)
 
       
  1166 apply(simp)
 
       
  1167 apply(erule ValOrd.cases)
 
       
  1168 apply(simp_all)[8]
 
       
  1169 (* ALT case *)
 
       
  1170 apply(simp)
 
       
  1171 apply(erule ValOrd.cases)
 
       
  1172 apply(simp_all)[8]
 
       
  1173 apply(rule ValOrd.intros)
 
   770 apply(subst v4)
 
  1174 apply(subst v4)
 
   771 apply(clarify)
 
  1175 apply(clarify)
 
   772 apply(erule Prf.cases)
 
  1176 apply(rotate_tac 3)
 
   773 apply(simp_all)[5]
 
  1177 apply(erule Prf.cases)
 
   774 apply(simp)
 
  1178 apply(simp_all)[5]
 
   775 apply(rule ValOrd.intros)
 
  1179 apply(subst v4)
 
   776 apply(clarify)
 
  1180 apply(clarify)
 
   777 apply(erule Prf.cases)
 
  1181 apply(rotate_tac 2)
 
   778 apply(simp_all)[5]
 
  1182 apply(erule Prf.cases)
 
       
  1183 apply(simp_all)[5]
 
       
  1184 apply(simp)
 
       
  1185 apply(rule ValOrd.intros)
 
       
  1186 apply(clarify)
 
       
  1187 apply(rotate_tac 3)
 
       
  1188 apply(erule Prf.cases)
 
       
  1189 apply(simp_all)[5]
 
       
  1190 apply(clarify)
 
   779 apply(erule Prf.cases)
 
  1191 apply(erule Prf.cases)
 
   780 apply(simp_all)[5]
 
  1192 apply(simp_all)[5]
 
   781 apply(rule ValOrd.intros)
 
  1193 apply(rule ValOrd.intros)
 
   782 apply(clarify)
 
  1194 apply(clarify)
 
   783 apply(erule Prf.cases)
 
  1195 apply(erule Prf.cases)
 
   803 apply(rule ValOrd.intros(2))
 
  1215 apply(rule ValOrd.intros(2))
 
   804 apply(erule Prf.cases)
 
  1216 apply(erule Prf.cases)
 
   805 apply(simp_all)[5]
 
  1217 apply(simp_all)[5]
 
   806 apply(erule Prf.cases)
 
  1218 apply(erule Prf.cases)
 
   807 apply(simp_all)[5]
 
  1219 apply(simp_all)[5]
 
       
  1220 apply(clarify)
 
       
  1221 defer
 
       
  1222 apply(simp)
 
       
  1223 apply(erule ValOrd.cases)
 
       
  1224 apply(simp_all del: injval.simps)[8]
 
       
  1225 apply(simp)
 
       
  1226 apply(clarify)
 
       
  1227 apply(simp)
 
       
  1228 apply(erule Prf.cases)
 
       
  1229 apply(simp_all)[5]
 
       
  1230 apply(erule Prf.cases)
 
       
  1231 apply(simp_all)[5]
 
       
  1232 apply(clarify)
 
       
  1233 apply(erule Prf.cases)
 
       
  1234 apply(simp_all)[5]
 
       
  1235 apply(clarify)
 
       
  1236 apply(rule ValOrd.intros(2))
 
       
  1237 
       
  1238 
       
  1239 
       
  1240 
       
  1241 done
 
       
  1242 
       
  1243 
       
  1244 txt {*
 
       
  1245 done
 
   808 (* nullable case - unfinished *)
 
  1246 (* nullable case - unfinished *)
 
   809 apply(simp)
 
  1247 apply(simp)
 
   810 apply(erule ValOrd.cases)
 
  1248 apply(erule ValOrd.cases)
 
   811 apply(simp_all)[8]
 
  1249 apply(simp_all del: injval.simps)[8]
 
   812 apply(clarify)
 
  1250 apply(simp)
 
   813 apply(simp)
 
  1251 apply(clarify)
 
   814 apply(erule Prf.cases)
 
  1252 apply(simp)
 
   815 apply(simp_all)[5]
 
  1253 apply(erule Prf.cases)
 
   816 apply(erule Prf.cases)
 
  1254 apply(simp_all)[5]
 
   817 apply(simp_all)[5]
 
  1255 apply(erule Prf.cases)
 
   818 apply(clarify)
 
  1256 apply(simp_all)[5]
 
   819 apply(erule Prf.cases)
 
  1257 apply(clarify)
 
   820 apply(simp_all)[5]
 
  1258 apply(erule Prf.cases)
 
   821 apply(clarify)
 
  1259 apply(simp_all)[5]
 
   822 apply(simp)
 
  1260 apply(clarify)
 
   823 apply(case_tac "injval r1 c v1 = mkeps r1") 
  1261 apply(simp)
 
   824 apply(rule ValOrd.intros(1))
 
       
   825 apply(simp)
 
       
   826 apply (metis impossible_Cons le_add2 list.size(3) mkeps_flat monoid_add_class.add.right_neutral v4)
 
       
   827 apply(rule ValOrd.intros(2))
 
  1262 apply(rule ValOrd.intros(2))
 
   828 apply(drule_tac x="proj r1 c" in spec)
 
  1263 oops
 
       
  1264 *}
 
   829 oops
 
  1265 oops
 
   830 
  1266 
   831 lemma POSIX_der:
 
  1267 lemma POSIX_der:
 
   832   assumes "POSIX v (der c r)" "\<turnstile> v : der c r"
 
  1268   assumes "POSIX v (der c r)" "\<turnstile> v : der c r"
 
   833   shows "POSIX (injval r c v) r"
 
  1269   shows "POSIX (injval r c v) r"
lexing