thys/Re.thy
changeset 6 87618dae0e04
parent 5 fe177dfc4697
child 7 b409ecf47f64
equal deleted inserted replaced
5:fe177dfc4697 6:87618dae0e04
    62 | "flat(Char c) = [c]"
    62 | "flat(Char c) = [c]"
    63 | "flat(Left v) = flat(v)"
    63 | "flat(Left v) = flat(v)"
    64 | "flat(Right v) = flat(v)"
    64 | "flat(Right v) = flat(v)"
    65 | "flat(Seq v1 v2) = flat(v1) @ flat(v2)"
    65 | "flat(Seq v1 v2) = flat(v1) @ flat(v2)"
    66 
    66 
       
    67 (* not actually in the paper *)
    67 datatype tree = 
    68 datatype tree = 
    68   Leaf string
    69   Leaf string
    69 | Branch tree tree
    70 | Branch tree tree
    70 
    71 
    71 fun flats :: "val \<Rightarrow> tree"
    72 fun flats :: "val \<Rightarrow> tree"
   101 apply (metis Prf.intros(4) flat.simps(1))
   102 apply (metis Prf.intros(4) flat.simps(1))
   102 apply (metis Prf.intros(5) flat.simps(2))
   103 apply (metis Prf.intros(5) flat.simps(2))
   103 apply (metis Prf.intros(1) flat.simps(5))
   104 apply (metis Prf.intros(1) flat.simps(5))
   104 apply (metis Prf.intros(2) flat.simps(3))
   105 apply (metis Prf.intros(2) flat.simps(3))
   105 apply (metis Prf.intros(3) flat.simps(4))
   106 apply (metis Prf.intros(3) flat.simps(4))
   106 by (smt Prf.cases flat.simps(3) flat.simps(4) rexp.distinct(13) rexp.distinct(17) rexp.distinct(19) rexp.inject(3))
   107 sorry
       
   108 
       
   109 (*by (smt Prf.cases flat.simps(3) flat.simps(4) rexp.distinct(13) rexp.distinct(17) rexp.distinct(19) rexp.inject(3))*)
   107 
   110 
   108 inductive ValOrd :: "val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<succ>_ _" [100, 100, 100] 100)
   111 inductive ValOrd :: "val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<succ>_ _" [100, 100, 100] 100)
   109 where
   112 where
   110   "\<lbrakk>v1 \<succ>r1 v1'; v2 \<succ>r2 v2'\<rbrakk> \<Longrightarrow> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1' v2')" 
   113   "\<lbrakk>v1 = v1'; v2 \<succ>r2 v2'\<rbrakk> \<Longrightarrow> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1' v2')" 
       
   114 | "v1  \<succ>r1 v1' \<Longrightarrow> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1' v2')" 
   111 | "length (flat v1) \<ge> length (flat v2) \<Longrightarrow> (Left v1) \<succ>(ALT r1 r2) (Right v2)"
   115 | "length (flat v1) \<ge> length (flat v2) \<Longrightarrow> (Left v1) \<succ>(ALT r1 r2) (Right v2)"
   112 | "length (flat v2) > length (flat v1) \<Longrightarrow> (Right v2) \<succ>(ALT r1 r2) (Left v1)"
   116 | "length (flat v2) > length (flat v1) \<Longrightarrow> (Right v2) \<succ>(ALT r1 r2) (Left v1)"
   113 | "v2 \<succ>r2 v2' \<Longrightarrow> (Right v2) \<succ>(ALT r1 r2) (Right v2')"
   117 | "v2 \<succ>r2 v2' \<Longrightarrow> (Right v2) \<succ>(ALT r1 r2) (Right v2')"
   114 | "v1 \<succ>r1 v1' \<Longrightarrow> (Left v1) \<succ>(ALT r1 r2) (Left v1')"
   118 | "v1 \<succ>r1 v1' \<Longrightarrow> (Left v1) \<succ>(ALT r1 r2) (Left v1')"
   115 | "Void \<succ>EMPTY Void"
   119 | "Void \<succ>EMPTY Void"
   116 | "(Char c) \<succ>(CHAR c) (Char c)"
   120 | "(Char c) \<succ>(CHAR c) (Char c)"
   117 
   121 
       
   122 (*
   118 lemma
   123 lemma
   119   assumes "r = SEQ (ALT EMPTY EMPTY) (ALT EMPTY (CHAR c))"
   124   assumes "r = SEQ (ALT EMPTY EMPTY) (ALT EMPTY (CHAR c))"
   120   shows "(Seq (Left Void) (Right (Char c))) \<succ>r (Seq (Left Void) (Left Void))"
   125   shows "(Seq (Left Void) (Right (Char c))) \<succ>r (Seq (Left Void) (Left Void))"
   121 using assms
   126 using assms
   122 apply(simp)
   127 apply(simp)
   124 apply(rule ValOrd.intros)
   129 apply(rule ValOrd.intros)
   125 apply(rule ValOrd.intros)
   130 apply(rule ValOrd.intros)
   126 apply(rule ValOrd.intros)
   131 apply(rule ValOrd.intros)
   127 apply(simp)
   132 apply(simp)
   128 done
   133 done
   129 
   134 *)
   130 
   135 
   131 definition POSIX :: "val \<Rightarrow> rexp \<Rightarrow> bool" 
   136 definition POSIX :: "val \<Rightarrow> rexp \<Rightarrow> bool" 
   132 where
   137 where
   133   "POSIX v r \<equiv> (\<forall>v'. (\<turnstile> v' : r \<and> flats v = flats v') \<longrightarrow> v \<succ>r v')"
   138   "POSIX v r \<equiv> (\<forall>v'. (\<turnstile> v' : r \<and> flat v = flat v') \<longrightarrow> v \<succ>r v')"
   134 
   139 
   135 lemma POSIX:
   140 (*
   136   assumes "r = SEQ (ALT EMPTY EMPTY) (ALT EMPTY (CHAR c))"
       
   137   shows "POSIX (Seq (Left Void) (Right (Char c))) r"
       
   138 apply(simp add: POSIX_def assms)
       
   139 apply(auto)
       
   140 apply(erule Prf.cases)
       
   141 apply(simp_all)
       
   142 apply(rule ValOrd.intros)
       
   143 apply (smt POSIX_def Prf.cases Prf.simps ValOrd.intros(2) ValOrd.intros(5) ValOrd.intros(6) flats.simps(1) flats.simps(3) rexp.distinct(11) rexp.distinct(13) rexp.distinct(17) rexp.distinct(19) rexp.distinct(9) rexp.inject(3) val.distinct(19) val.inject(3))
       
   144 by (smt Prf.simps ValOrd.intros(4) ValOrd.intros(7) flats.simps(1) flats.simps(3) list.distinct(1) rexp.distinct(11) rexp.distinct(13) rexp.distinct(15) rexp.distinct(17) rexp.distinct(19) rexp.distinct(9) rexp.inject(1) rexp.inject(3) tree.inject(1))
       
   145 
       
   146 
       
   147 lemma Exists_POSIX: "\<exists>v. POSIX v r"
       
   148 apply(induct r)
       
   149 apply(auto simp add: POSIX_def)
       
   150 apply(rule exI)
       
   151 apply(auto)
       
   152 apply(erule Prf.cases)
       
   153 apply(simp_all)[5]
       
   154 apply (smt Prf.simps ValOrd.intros(6) rexp.distinct(11) rexp.distinct(13) rexp.distinct(9))
       
   155 apply(rule exI)
       
   156 apply(auto)
       
   157 apply(erule Prf.cases)
       
   158 apply(simp_all)[5]
       
   159 apply(rule ValOrd.intros)
       
   160 apply(rule exI)
       
   161 apply(auto)
       
   162 apply(erule Prf.cases)
       
   163 apply(simp_all)[5]
       
   164 apply(rule ValOrd.intros)
       
   165 apply(auto)[2]
       
   166 apply(rule_tac x="Left v" in exI)
       
   167 apply(auto)
       
   168 apply(erule Prf.cases)
       
   169 apply(simp_all)[5]
       
   170 apply(rule ValOrd.intros)
       
   171 apply(auto)[1]
       
   172 apply(auto)
       
   173 apply(rule ValOrd.intros)
       
   174 by (metis flats_flat order_refl)
       
   175 
       
   176 
       
   177 lemma POSIX_SEQ:
   141 lemma POSIX_SEQ:
   178   assumes "POSIX (Seq v1 v2) (SEQ r1 r2)" "\<turnstile> v1 : r1" "\<turnstile> v2 : r2"
   142   assumes "POSIX (Seq v1 v2) (SEQ r1 r2)" "\<turnstile> v1 : r1" "\<turnstile> v2 : r2"
   179   shows "POSIX v1 r1 \<and> POSIX v2 r2"
   143   shows "POSIX v1 r1 \<and> POSIX v2 r2"
   180 using assms
   144 using assms
   181 unfolding POSIX_def
   145 unfolding POSIX_def
   184 apply(simp)
   148 apply(simp)
   185 apply (smt Prf.intros(1) ValOrd.simps assms(3) rexp.inject(2) val.distinct(15) val.distinct(17) val.distinct(3) val.distinct(9) val.inject(2))
   149 apply (smt Prf.intros(1) ValOrd.simps assms(3) rexp.inject(2) val.distinct(15) val.distinct(17) val.distinct(3) val.distinct(9) val.inject(2))
   186 apply(drule_tac x="Seq v1 v'" in spec)
   150 apply(drule_tac x="Seq v1 v'" in spec)
   187 apply(simp)
   151 apply(simp)
   188 by (smt Prf.intros(1) ValOrd.simps rexp.inject(2) val.distinct(15) val.distinct(17) val.distinct(3) val.distinct(9) val.inject(2))
   152 by (smt Prf.intros(1) ValOrd.simps rexp.inject(2) val.distinct(15) val.distinct(17) val.distinct(3) val.distinct(9) val.inject(2))
   189 
   153 *)
       
   154 
       
   155 (*
   190 lemma POSIX_SEQ_I:
   156 lemma POSIX_SEQ_I:
   191   assumes "POSIX v1 r1" "POSIX v2 r2" 
   157   assumes "POSIX v1 r1" "POSIX v2 r2" 
   192   shows "POSIX (Seq v1 v2) (SEQ r1 r2)" 
   158   shows "POSIX (Seq v1 v2) (SEQ r1 r2)" 
   193 using assms
   159 using assms
   194 unfolding POSIX_def
   160 unfolding POSIX_def
   269 apply(rule ValOrd.intros)
   235 apply(rule ValOrd.intros)
   270 apply metis
   236 apply metis
   271 apply(rule ValOrd.intros)
   237 apply(rule ValOrd.intros)
   272 apply(auto)
   238 apply(auto)
   273 done
   239 done
       
   240 *)
   274 
   241 
   275 lemma ValOrd_refl:
   242 lemma ValOrd_refl:
   276   assumes "\<turnstile> v : r"
   243   assumes "\<turnstile> v : r"
   277   shows "v \<succ>r v"
   244   shows "v \<succ>r v"
   278 using assms
   245 using assms
   279 apply(induct)
   246 apply(induct)
   280 apply(auto intro: ValOrd.intros)
   247 apply(auto intro: ValOrd.intros)
   281 done
   248 done
   282 
   249 
       
   250 (*
   283 lemma ValOrd_length:
   251 lemma ValOrd_length:
   284   assumes "v1 \<succ>r v2" shows "length (flat v1) \<ge> length (flat v2)"
   252   assumes "v1 \<succ>r v2" shows "length (flat v1) \<ge> length (flat v2)"
   285 using assms
   253 using assms
   286 apply(induct)
   254 apply(induct)
   287 apply(auto)
   255 apply(auto)
   288 done
   256 done
       
   257 *)
   289 
   258 
   290 section {* The Matcher *}
   259 section {* The Matcher *}
   291 
   260 
   292 fun
   261 fun
   293  nullable :: "rexp \<Rightarrow> bool"
   262  nullable :: "rexp \<Rightarrow> bool"
   335 lemma mkeps_POSIX:
   304 lemma mkeps_POSIX:
   336   assumes "nullable r"
   305   assumes "nullable r"
   337   shows "POSIX (mkeps r) r"
   306   shows "POSIX (mkeps r) r"
   338 using assms
   307 using assms
   339 apply(induct r)
   308 apply(induct r)
   340 apply(auto)
   309 apply(auto)[1]
   341 apply(simp add: POSIX_def)
   310 apply(simp add: POSIX_def)
   342 apply(auto)[1]
   311 apply(auto)[1]
   343 apply(erule Prf.cases)
   312 apply(erule Prf.cases)
   344 apply(simp_all)[5]
   313 apply(simp_all)[5]
   345 apply (metis ValOrd.intros(6))
   314 apply (metis ValOrd.intros)
   346 apply(simp add: POSIX_def)
   315 apply(simp add: POSIX_def)
   347 apply(auto)[1]
   316 apply(auto)[1]
   348 apply(erule Prf.cases)
   317 sorry
   349 apply(simp_all)[5]
   318 
   350 apply(auto)
       
   351 apply (metis ValOrd.intros(1) append_is_Nil_conv mkeps_flat)
       
   352 apply(simp add: POSIX_def)
       
   353 apply(auto)[1]
       
   354 apply(erule Prf.cases)
       
   355 apply(simp_all)[5]
       
   356 apply(auto)
       
   357 apply (metis ValOrd.intros(5))
       
   358 apply(rule ValOrd.intros(2))
       
   359 apply(simp add: mkeps_flat)
       
   360 apply(simp add: flats_flat)
       
   361 apply (metis mkeps_flats)
       
   362 apply(simp add: POSIX_def)
       
   363 apply(auto)[1]
       
   364 apply(erule Prf.cases)
       
   365 apply(simp_all)[5]
       
   366 apply(auto)
       
   367 apply (metis ValOrd.intros(5))
       
   368 apply (smt ValOrd.intros(2) flats_flat)
       
   369 apply(simp add: POSIX_def)
       
   370 apply(auto)[1]
       
   371 apply(erule Prf.cases)
       
   372 apply(simp_all)[5]
       
   373 apply (metis Prf_flat_L flats_flat mkeps_flats nullable_correctness)
       
   374 by (metis ValOrd.intros(4))
       
   375 
   319 
   376 fun
   320 fun
   377  der :: "char \<Rightarrow> rexp \<Rightarrow> rexp"
   321  der :: "char \<Rightarrow> rexp \<Rightarrow> rexp"
   378 where
   322 where
   379   "der c (NULL) = NULL"
   323   "der c (NULL) = NULL"
   554 apply(induct v)
   498 apply(induct v)
   555 apply(simp_all)
   499 apply(simp_all)
   556 apply (metis Nil_is_append_conv head.elims option.distinct(1))
   500 apply (metis Nil_is_append_conv head.elims option.distinct(1))
   557 done
   501 done
   558 
   502 
       
   503 (* HERE *)
   559 lemma v5:
   504 lemma v5:
   560   assumes "\<turnstile> v : der c r" "POSIX v (der c r)"
   505   assumes "\<turnstile> v : der c r" "POSIX v (der c r)"
   561   shows "POSIX (injval r c v) r"
   506   shows "POSIX (injval r c v) r"
   562 using assms
   507 using assms
       
   508 apply(induct r)
       
   509 apply(simp (no_asm) only: POSIX_def)
       
   510 apply(rule allI)
       
   511 apply(rule impI)
       
   512 apply(simp)
       
   513 apply(erule Prf.cases)
       
   514 apply(simp_all)[5]
   563 apply(induct arbitrary: v rule: der.induct)
   515 apply(induct arbitrary: v rule: der.induct)
   564 apply(simp)
   516 apply(simp)
   565 apply(erule Prf.cases)
   517 apply(erule Prf.cases)
   566 apply(simp_all)[5]
   518 apply(simp_all)[5]
   567 apply(simp)
   519 apply(simp)