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/ReStar.thy
changeset 95 a33d3040bf7e
parent 94 5b01f7c233f8
child 97 38696f516c6b
equal deleted inserted replaced
94:5b01f7c233f8 95:a33d3040bf7e 
   538   "Values (NULL) s = {}"
 
   538   "Values (NULL) s = {}"
 
   539   "Values (EMPTY) s = {Void}"
 
   539   "Values (EMPTY) s = {Void}"
 
   540   "Values (CHAR c) s = (if [c] \<sqsubseteq> s then {Char c} else {})" 
   540   "Values (CHAR c) s = (if [c] \<sqsubseteq> s then {Char c} else {})" 
   541   "Values (ALT r1 r2) s = {Left v | v. v \<in> Values r1 s} \<union> {Right v | v. v \<in> Values r2 s}"
 
   541   "Values (ALT r1 r2) s = {Left v | v. v \<in> Values r1 s} \<union> {Right v | v. v \<in> Values r2 s}"
 
   542   "Values (SEQ r1 r2) s = {Seq v1 v2 | v1 v2. v1 \<in> Values r1 s \<and> v2 \<in> Values r2 (rest v1 s)}"
 
   542   "Values (SEQ r1 r2) s = {Seq v1 v2 | v1 v2. v1 \<in> Values r1 s \<and> v2 \<in> Values r2 (rest v1 s)}"
 
   543   "Values (STAR r) s = {Star []} \<union> {Star (v # vs) | v vs. v \<in> Values r s \<and> 
   543   "Values (STAR r) s = 
   544                                                                Star vs \<in> Values (STAR r) (rest v s)}"
 
   544       {Star []} \<union> {Star (v # vs) | v vs. v \<in> Values r s \<and> Star vs \<in> Values (STAR r) (rest v s)}"
 
   545 unfolding Values_def
 
   545 unfolding Values_def
 
   546 apply(auto)
 
   546 apply(auto)
 
   547 (*NULL*)
 
   547 (*NULL*)
 
   548 apply(erule Prf.cases)
 
   548 apply(erule Prf.cases)
 
   549 apply(simp_all)[7]
 
   549 apply(simp_all)[7]
 
   587   "NValues (NULL) s = {}"
 
   587   "NValues (NULL) s = {}"
 
   588   "NValues (EMPTY) s = {Void}"
 
   588   "NValues (EMPTY) s = {Void}"
 
   589   "NValues (CHAR c) s = (if [c] \<sqsubseteq> s then {Char c} else {})" 
   589   "NValues (CHAR c) s = (if [c] \<sqsubseteq> s then {Char c} else {})" 
   590   "NValues (ALT r1 r2) s = {Left v | v. v \<in> NValues r1 s} \<union> {Right v | v. v \<in> NValues r2 s}"
 
   590   "NValues (ALT r1 r2) s = {Left v | v. v \<in> NValues r1 s} \<union> {Right v | v. v \<in> NValues r2 s}"
 
   591   "NValues (SEQ r1 r2) s = {Seq v1 v2 | v1 v2. v1 \<in> NValues r1 s \<and> v2 \<in> NValues r2 (rest v1 s)}"
 
   591   "NValues (SEQ r1 r2) s = {Seq v1 v2 | v1 v2. v1 \<in> NValues r1 s \<and> v2 \<in> NValues r2 (rest v1 s)}"
 
   592   "NValues (STAR r) s = {Star []} \<union> {Star (v # vs) | v vs. v \<in> NValues r s \<and> flat v \<noteq> [] \<and> 
   592   "NValues (STAR r) s = 
   593                                                                Star vs \<in> NValues (STAR r) (rest v s)}"
 
   593   {Star []} \<union> {Star (v # vs) | v vs. v \<in> NValues r s \<and> flat v \<noteq> [] \<and>  Star vs \<in> NValues (STAR r) (rest v s)}"
 
   594 unfolding NValues_def
 
   594 unfolding NValues_def
 
   595 apply(auto)
 
   595 apply(auto)
 
   596 (*NULL*)
 
   596 (*NULL*)
 
   597 apply(erule NPrf.cases)
 
   597 apply(erule NPrf.cases)
 
   598 apply(simp_all)[7]
 
   598 apply(simp_all)[7]
 
  1215 apply(simp)
 
  1215 apply(simp)
 
  1216 done
 
  1216 done
 
  1217 
  1217 
  1218 lemma lex_correct4:
 
  1218 lemma lex_correct4:
 
  1219   assumes "s \<in> L r"
 
  1219   assumes "s \<in> L r"
 
       
  1220   shows "\<exists>v. lex r s = Some(v) \<and> \<Turnstile> v : r \<and> flat v = s"
 
       
  1221 using lex_correct3[OF assms]
 
       
  1222 apply(auto)
 
       
  1223 apply (metis PMatch1N)
 
       
  1224 by (metis PMatch1(2))
 
       
  1225 
       
  1226 
       
  1227 lemma lex_correct5:
 
       
  1228   assumes "s \<in> L r"
 
  1220   shows "s \<in> r \<rightarrow> (lex2 r s)"
 
  1229   shows "s \<in> r \<rightarrow> (lex2 r s)"
 
  1221 using assms
 
  1230 using assms
 
  1222 apply(induct s arbitrary: r)
 
  1231 apply(induct s arbitrary: r)
 
  1223 apply(simp)
 
  1232 apply(simp)
 
  1224 apply (metis PMatch_mkeps nullable_correctness)
 
  1233 apply (metis PMatch_mkeps nullable_correctness)
 
  1241 
  1250 
  1242 section {* Sulzmann's Ordering of values *}
 
  1251 section {* Sulzmann's Ordering of values *}
 
  1243 
  1252 
  1244 thm PMatch.intros
 
  1253 thm PMatch.intros
 
  1245 
  1254 
       
  1255 (*
 
  1246 inductive ValOrd :: "string \<Rightarrow> val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<turnstile> _ \<succ>_ _" [100, 100, 100, 100] 100)
 
  1256 inductive ValOrd :: "string \<Rightarrow> val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<turnstile> _ \<succ>_ _" [100, 100, 100, 100] 100)
 
  1247 where
 
  1257 where
 
  1248   "\<lbrakk>s2 \<turnstile> v2 \<succ>r2 v2'; flat v1 = s1\<rbrakk> \<Longrightarrow> (s1 @ s2) \<turnstile> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1 v2')" 
  1258   "\<lbrakk>s2 \<turnstile> v2 \<succ>r2 v2'; flat v1 = s1\<rbrakk> \<Longrightarrow> (s1 @ s2) \<turnstile> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1 v2')" 
  1249 | "\<lbrakk>s1 \<turnstile> v1 \<succ>r1 v1'; v1 \<noteq> v1'\<rbrakk> \<Longrightarrow> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1' v2')" 
  1259 | "\<lbrakk>s1 \<turnstile> v1 \<succ>r1 v1'; v1 \<noteq> v1'\<rbrakk> \<Longrightarrow> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1' v2')" 
  1250 | "\<lbrakk>flat v1 \<sqsubseteq> s; flat v2 \<sqsubseteq> flat v1\<rbrakk> \<Longrightarrow> s \<turnstile> (Left v1) \<succ>(ALT r1 r2) (Right v2)"
 
  1260 | "\<lbrakk>flat v1 \<sqsubseteq> s; flat v2 \<sqsubseteq> flat v1\<rbrakk> \<Longrightarrow> s \<turnstile> (Left v1) \<succ>(ALT r1 r2) (Right v2)"
 
  1251 | "\<lbrakk>flat v2 \<sqsubseteq> s; flat v1 \<sqsubset>  flat v2\<rbrakk> \<Longrightarrow> s \<turnstile> (Right v2) \<succ>(ALT r1 r2) (Left v1)"
 
  1261 | "\<lbrakk>flat v2 \<sqsubseteq> s; flat v1 \<sqsubset>  flat v2\<rbrakk> \<Longrightarrow> s \<turnstile> (Right v2) \<succ>(ALT r1 r2) (Left v1)"
 
  1252 | "s \<turnstile> v2 \<succ>r2 v2' \<Longrightarrow> s \<turnstile> (Right v2) \<succ>(ALT r1 r2) (Right v2')"
 
  1262 | "s \<turnstile> v2 \<succ>r2 v2' \<Longrightarrow> s \<turnstile> (Right v2) \<succ>(ALT r1 r2) (Right v2')"
 
  1253 | "s \<turnstile> v1 \<succ>r1 v1' \<Longrightarrow> s \<turnstile> (Left v1) \<succ>(ALT r1 r2) (Left v1')"
 
  1263 | "s \<turnstile> v1 \<succ>r1 v1' \<Longrightarrow> s \<turnstile> (Left v1) \<succ>(ALT r1 r2) (Left v1')"
 
  1254 | "s \<turnstile> Void \<succ>EMPTY Void"
 
  1264 | "s \<turnstile> Void \<succ>EMPTY Void"
 
  1255 | "(c#s) \<turnstile> (Char c) \<succ>(CHAR c) (Char c)"
 
  1265 | "(c#s) \<turnstile> (Char c) \<succ>(CHAR c) (Char c)"
 
  1256 
  1266 *)
 
  1257 
  1267 
  1258 inductive ValOrd :: "val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<succ>_ _" [100, 100, 100] 100)
 
  1268 inductive ValOrd :: "val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<succ>_ _" [100, 100, 100] 100)
 
  1259 where
 
  1269 where
 
  1260   "v2 \<succ>r2 v2' \<Longrightarrow> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1 v2')" 
  1270   "v2 \<succ>r2 v2' \<Longrightarrow> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1 v2')" 
  1261 | "\<lbrakk>v1 \<succ>r1 v1'; v1 \<noteq> v1'\<rbrakk> \<Longrightarrow> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1' v2')" 
  1271 | "\<lbrakk>v1 \<succ>r1 v1'; v1 \<noteq> v1'\<rbrakk> \<Longrightarrow> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1' v2')" 
  1263 | "length (flat v2) > length (flat v1) \<Longrightarrow> (Right v2) \<succ>(ALT r1 r2) (Left v1)"
 
  1273 | "length (flat v2) > length (flat v1) \<Longrightarrow> (Right v2) \<succ>(ALT r1 r2) (Left v1)"
 
  1264 | "v2 \<succ>r2 v2' \<Longrightarrow> (Right v2) \<succ>(ALT r1 r2) (Right v2')"
 
  1274 | "v2 \<succ>r2 v2' \<Longrightarrow> (Right v2) \<succ>(ALT r1 r2) (Right v2')"
 
  1265 | "v1 \<succ>r1 v1' \<Longrightarrow> (Left v1) \<succ>(ALT r1 r2) (Left v1')"
 
  1275 | "v1 \<succ>r1 v1' \<Longrightarrow> (Left v1) \<succ>(ALT r1 r2) (Left v1')"
 
  1266 | "Void \<succ>EMPTY Void"
 
  1276 | "Void \<succ>EMPTY Void"
 
  1267 | "(Char c) \<succ>(CHAR c) (Char c)"
 
  1277 | "(Char c) \<succ>(CHAR c) (Char c)"
 
       
  1278 | "flat (Star (v # vs)) = [] \<Longrightarrow> (Star []) \<succ>(STAR r) (Star (v # vs))"
 
       
  1279 | "flat (Star (v # vs)) \<noteq> [] \<Longrightarrow> (Star (v # vs)) \<succ>(STAR r) (Star [])"
 
       
  1280 | "v1 \<succ>r v2 \<Longrightarrow> (Star (v1 # vs1)) \<succ>(STAR r) (Star (v2 # vs2))"
 
       
  1281 | "(Star vs1) \<succ>(STAR r) (Star vs2) \<Longrightarrow> (Star (v # vs1)) \<succ>(STAR r) (Star (v # vs2))"
 
       
  1282 | "(Star []) \<succ>(STAR r) (Star [])"
 
       
  1283 
       
  1284 (*
 
  1268 
  1285 
  1269 lemma ValOrd_PMatch:
 
  1286 lemma ValOrd_PMatch:
 
  1270   assumes "s \<in> r \<rightarrow> v1" "\<turnstile> v2 : r" "flat v2  \<sqsubseteq> s"
 
  1287   assumes "s \<in> r \<rightarrow> v1" "\<turnstile> v2 : r" "flat v2  \<sqsubseteq> s"
 
  1271   shows "v1 \<succ>r v2"
 
  1288   shows "v1 \<succ>r v2"
 
  1272 using assms
 
  1289 using assms
 
  1273 apply(induct r arbitrary: s v1 v2 rule: rexp.induct)
 
  1290 apply(induct r arbitrary: s v1 v2 rule: rexp.induct)
 
  1274 apply(erule Prf.cases)
 
  1291 apply(erule Prf.cases)
 
  1275 apply(simp_all)[5]
 
  1292 apply(simp_all)[7]
 
  1276 apply(erule Prf.cases)
 
  1293 apply(erule Prf.cases)
 
  1277 apply(simp_all)[5]
 
  1294 apply(simp_all)[7]
 
  1278 apply(erule PMatch.cases)
 
  1295 apply(erule PMatch.cases)
 
  1279 apply(simp_all)[5]
 
  1296 apply(simp_all)[7]
 
  1280 apply (metis ValOrd.intros(7))
 
  1297 apply (metis ValOrd.intros(7))
 
  1281 apply(erule Prf.cases)
 
  1298 apply(erule Prf.cases)
 
  1282 apply(simp_all)[5]
 
  1299 apply(simp_all)[7]
 
  1283 apply(erule PMatch.cases)
 
  1300 apply(erule PMatch.cases)
 
  1284 apply(simp_all)[5]
 
  1301 apply(simp_all)[7]
 
  1285 apply (metis ValOrd.intros(8))
 
  1302 apply (metis ValOrd.intros(8))
 
  1286 defer
 
  1303 defer
 
  1287 apply(erule Prf.cases)
 
  1304 apply(erule Prf.cases)
 
  1288 apply(simp_all)[5]
 
  1305 apply(simp_all)[7]
 
  1289 apply(erule PMatch.cases)
 
  1306 apply(erule PMatch.cases)
 
  1290 apply(simp_all)[5]
 
  1307 apply(simp_all)[7]
 
  1291 apply (metis ValOrd.intros(6))
 
  1308 apply (metis ValOrd.intros(6))
 
  1292 apply (metis PMatch1(2) Prf_flat_L ValOrd.intros(4) length_sprefix sprefix_def)
 
  1309 apply (metis PMatch1(2) Prf_flat_L ValOrd.intros(4) length_sprefix sprefix_def)
 
  1293 apply(clarify)
 
  1310 apply(clarify)
 
  1294 apply(erule PMatch.cases)
 
  1311 apply(erule PMatch.cases)
 
  1295 apply(simp_all)[5]
 
  1312 apply(simp_all)[7]
 
  1296 apply (metis PMatch1(2) ValOrd.intros(3) length_sprefix less_imp_le_nat order_refl sprefix_def)
 
  1313 apply (metis PMatch1(2) ValOrd.intros(3) length_sprefix less_imp_le_nat order_refl sprefix_def)
 
  1297 apply(clarify)
 
  1314 apply(clarify)
 
  1298 apply (metis ValOrd.intros(5))
 
  1315 apply (metis ValOrd.intros(5))
 
       
  1316 (* Star case *)
 
       
  1317 apply(erule Prf.cases)
 
       
  1318 apply(simp_all)[7]
 
       
  1319 apply(erule PMatch.cases)
 
       
  1320 apply(simp_all)
 
       
  1321 apply (metis Nil_is_append_conv ValOrd.intros(10) flat.simps(7))
 
       
  1322 apply (metis ValOrd.intros(13))
 
       
  1323 apply(clarify)
 
       
  1324 apply(erule PMatch.cases)
 
       
  1325 apply(simp_all)
 
       
  1326 prefer 2
 
       
  1327 apply(rule ValOrd.intros)
 
       
  1328 apply(simp add: prefix_def)
 
       
  1329 apply(rule ValOrd.intros)
 
       
  1330 apply(drule_tac x="s1" in meta_spec)
 
       
  1331 apply(drule_tac x="va" in meta_spec)
 
       
  1332 apply(drule_tac x="v" in meta_spec)
 
       
  1333 apply(drule_tac meta_mp)
 
       
  1334 apply(simp)
 
       
  1335 apply(drule_tac meta_mp)
 
       
  1336 apply(simp)
 
       
  1337 apply(drule_tac meta_mp)
 
       
  1338 apply(simp add: prefix_def)
 
       
  1339 apply(auto)[1]
 
       
  1340 prefer 3
 
  1299 (* Seq case *)
 
  1341 (* Seq case *)
 
  1300 apply(erule Prf.cases)
 
  1342 apply(erule Prf.cases)
 
  1301 apply(simp_all)[5]
 
  1343 apply(simp_all)[5]
 
  1302 apply(auto)
 
  1344 apply(auto)
 
  1303 apply(erule PMatch.cases)
 
  1345 apply(erule PMatch.cases)
 
  2869 apply(case_tac "c = c'")
 
  2911 apply(case_tac "c = c'")
 
  2870 apply(auto simp add: POSIX_def)[1]
 
  2912 apply(auto simp add: POSIX_def)[1]
 
  2871 apply(erule Prf.cases)
 
  2913 apply(erule Prf.cases)
 
  2872 apply(simp_all)[5]
 
  2914 apply(simp_all)[5]
 
  2873 oops
 
  2915 oops
 
       
  2916 *)
 
       
  2917 
       
  2918 end
lexing