--- a/thys/ReStar.thy Fri Mar 11 10:43:44 2016 +0000
+++ b/thys/ReStar.thy Fri Mar 11 13:53:53 2016 +0000
@@ -340,7 +340,7 @@
section {* Our Alternative Posix definition *}
inductive
- PMatch :: "string \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<in> _ \<rightarrow> _" [100, 100, 100] 100)
+ Posix :: "string \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<in> _ \<rightarrow> _" [100, 100, 100] 100)
where
"[] \<in> ONE \<rightarrow> Void"
| "[c] \<in> (CHAR c) \<rightarrow> (Char c)"
@@ -354,75 +354,75 @@
\<Longrightarrow> (s1 @ s2) \<in> STAR r \<rightarrow> Stars (v # vs)"
| "[] \<in> STAR r \<rightarrow> Stars []"
-inductive_cases PMatch_elims:
+inductive_cases Posix_elims:
"s \<in> ONE \<rightarrow> v"
"s \<in> CHAR c \<rightarrow> v"
"s \<in> ALT r1 r2 \<rightarrow> v"
"s \<in> SEQ r1 r2 \<rightarrow> v"
"s \<in> STAR r \<rightarrow> v"
-lemma PMatch1:
+lemma Posix1:
assumes "s \<in> r \<rightarrow> v"
shows "s \<in> L r" "flat v = s"
using assms
-by (induct s r v rule: PMatch.induct)
+by (induct s r v rule: Posix.induct)
(auto simp add: Sequ_def)
-lemma PMatch1a:
+lemma Posix1a:
assumes "s \<in> r \<rightarrow> v"
shows "\<turnstile> v : r"
using assms
-apply(induct s r v rule: PMatch.induct)
+apply(induct s r v rule: Posix.induct)
apply(auto intro: Prf.intros)
done
-lemma PMatch_mkeps:
+lemma Posix_mkeps:
assumes "nullable r"
shows "[] \<in> r \<rightarrow> mkeps r"
using assms
apply(induct r)
-apply(auto intro: PMatch.intros simp add: nullable_correctness Sequ_def)
+apply(auto intro: Posix.intros simp add: nullable_correctness Sequ_def)
apply(subst append.simps(1)[symmetric])
-apply(rule PMatch.intros)
+apply(rule Posix.intros)
apply(auto)
done
-lemma PMatch_determ:
+lemma Posix_determ:
assumes "s \<in> r \<rightarrow> v1" "s \<in> r \<rightarrow> v2"
shows "v1 = v2"
using assms
-apply(induct s r v1 arbitrary: v2 rule: PMatch.induct)
-apply(erule PMatch.cases)
+apply(induct s r v1 arbitrary: v2 rule: Posix.induct)
+apply(erule Posix.cases)
apply(simp_all)[7]
-apply(erule PMatch.cases)
+apply(erule Posix.cases)
apply(simp_all)[7]
apply(rotate_tac 2)
-apply(erule PMatch.cases)
+apply(erule Posix.cases)
apply(simp_all (no_asm_use))[7]
apply(clarify)
apply(force)
apply(clarify)
-apply(drule PMatch1(1))
+apply(drule Posix1(1))
apply(simp)
apply(rotate_tac 3)
-apply(erule PMatch.cases)
+apply(erule Posix.cases)
apply(simp_all (no_asm_use))[7]
-apply(drule PMatch1(1))+
+apply(drule Posix1(1))+
apply(simp)
apply(simp)
apply(rotate_tac 5)
-apply(erule PMatch.cases)
+apply(erule Posix.cases)
apply(simp_all (no_asm_use))[7]
apply(clarify)
apply(subgoal_tac "s1 = s1a")
apply(blast)
apply(simp add: append_eq_append_conv2)
apply(clarify)
-apply (metis PMatch1(1) append_self_conv)
+apply (metis Posix1(1) append_self_conv)
apply(rotate_tac 6)
-apply(erule PMatch.cases)
+apply(erule Posix.cases)
apply(simp_all (no_asm_use))[7]
apply(clarify)
apply(subgoal_tac "s1 = s1a")
@@ -430,22 +430,22 @@
apply(blast)
apply(simp (no_asm_use) add: append_eq_append_conv2)
apply(clarify)
-apply (metis L.simps(6) PMatch1(1) append_self_conv)
+apply (metis L.simps(6) Posix1(1) append_self_conv)
apply(clarify)
apply(rotate_tac 2)
-apply(erule PMatch.cases)
+apply(erule Posix.cases)
apply(simp_all (no_asm_use))[7]
-using PMatch1(2) apply auto[1]
-using PMatch1(2) apply blast
-apply(erule PMatch.cases)
+using Posix1(2) apply auto[1]
+using Posix1(2) apply blast
+apply(erule Posix.cases)
apply(simp_all (no_asm_use))[7]
apply(clarify)
-apply (simp add: PMatch1(2))
+apply (simp add: Posix1(2))
apply(simp)
done
(* a proof that does not need proj *)
-lemma PMatch2_roy_version:
+lemma Posix2_roy_version:
assumes "s \<in> (der c r) \<rightarrow> v"
shows "(c # s) \<in> r \<rightarrow> (injval r c v)"
using assms
@@ -471,7 +471,7 @@
then have "s \<in> ONE \<rightarrow> v" using eq by simp
then have eqs: "s = [] \<and> v = Void" by cases simp
show "(c # s) \<in> CHAR d \<rightarrow> injval (CHAR d) c v" using eq eqs
- by (auto intro: PMatch.intros)
+ by (auto intro: Posix.intros)
next
case ineq
have "s \<in> der c (CHAR d) \<rightarrow> v" by fact
@@ -493,7 +493,7 @@
case left
have "s \<in> der c r1 \<rightarrow> v'" by fact
then have "(c # s) \<in> r1 \<rightarrow> injval r1 c v'" using IH1 by simp
- then have "(c # s) \<in> ALT r1 r2 \<rightarrow> injval (ALT r1 r2) c (Left v')" by (auto intro: PMatch.intros)
+ then have "(c # s) \<in> ALT r1 r2 \<rightarrow> injval (ALT r1 r2) c (Left v')" by (auto intro: Posix.intros)
then show "(c # s) \<in> ALT r1 r2 \<rightarrow> injval (ALT r1 r2) c v" using left by simp
next
case right
@@ -503,7 +503,7 @@
have "s \<in> der c r2 \<rightarrow> v'" by fact
then have "(c # s) \<in> r2 \<rightarrow> injval r2 c v'" using IH2 by simp
ultimately have "(c # s) \<in> ALT r1 r2 \<rightarrow> injval (ALT r1 r2) c (Right v')"
- by (auto intro: PMatch.intros)
+ by (auto intro: Posix.intros)
then show "(c # s) \<in> ALT r1 r2 \<rightarrow> injval (ALT r1 r2) c v" using right by simp
qed
next
@@ -523,7 +523,7 @@
"v = Seq v1 v2" "s = s1 @ s2"
"s1 \<in> der c r1 \<rightarrow> v1" "s2 \<in> r2 \<rightarrow> v2" "\<not>nullable r1"
"\<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 (der c r1) \<and> s\<^sub>4 \<in> L r2)"
- by (force split: if_splits elim!: PMatch_elims simp add: Sequ_def der_correctness Der_def)
+ by (force split: if_splits elim!: Posix_elims simp add: Sequ_def der_correctness Der_def)
then show "(c # s) \<in> SEQ r1 r2 \<rightarrow> injval (SEQ r1 r2) c v"
proof (cases)
case left_nullable
@@ -532,12 +532,12 @@
moreover
have "\<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 (der c r1) \<and> s\<^sub>4 \<in> L r2)" by fact
then have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (c # s1) @ s\<^sub>3 \<in> L r1 \<and> s\<^sub>4 \<in> L r2)" by (simp add: der_correctness Der_def)
- ultimately have "((c # s1) @ s2) \<in> SEQ r1 r2 \<rightarrow> Seq (injval r1 c v1) v2" using left_nullable by (rule_tac PMatch.intros)
+ ultimately have "((c # s1) @ s2) \<in> SEQ r1 r2 \<rightarrow> Seq (injval r1 c v1) v2" using left_nullable by (rule_tac Posix.intros)
then show "(c # s) \<in> SEQ r1 r2 \<rightarrow> injval (SEQ r1 r2) c v" using left_nullable by simp
next
case right_nullable
have "nullable r1" by fact
- then have "[] \<in> r1 \<rightarrow> (mkeps r1)" by (rule PMatch_mkeps)
+ then have "[] \<in> r1 \<rightarrow> (mkeps r1)" by (rule Posix_mkeps)
moreover
have "s \<in> der c r2 \<rightarrow> v1" by fact
then have "(c # s) \<in> r2 \<rightarrow> (injval r2 c v1)" using IH2 by simp
@@ -546,7 +546,7 @@
then have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = c # s \<and> [] @ s\<^sub>3 \<in> L r1 \<and> s\<^sub>4 \<in> L r2)" using right_nullable
by(auto simp add: der_correctness Der_def append_eq_Cons_conv Sequ_def)
ultimately have "([] @ (c # s)) \<in> SEQ r1 r2 \<rightarrow> Seq (mkeps r1) (injval r2 c v1)"
- by(rule PMatch.intros)
+ by(rule Posix.intros)
then show "(c # s) \<in> SEQ r1 r2 \<rightarrow> injval (SEQ r1 r2) c v" using right_nullable by simp
next
case not_nullable
@@ -556,7 +556,7 @@
have "\<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 (der c r1) \<and> s\<^sub>4 \<in> L r2)" by fact
then have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (c # s1) @ s\<^sub>3 \<in> L r1 \<and> s\<^sub>4 \<in> L r2)" by (simp add: der_correctness Der_def)
ultimately have "((c # s1) @ s2) \<in> SEQ r1 r2 \<rightarrow> Seq (injval r1 c v1) v2" using not_nullable
- by (rule_tac PMatch.intros) (simp_all)
+ by (rule_tac Posix.intros) (simp_all)
then show "(c # s) \<in> SEQ r1 r2 \<rightarrow> injval (SEQ r1 r2) c v" using not_nullable by simp
qed
next
@@ -568,11 +568,11 @@
"v = Seq v1 (Stars vs)" "s = s1 @ s2"
"s1 \<in> der c r \<rightarrow> v1" "s2 \<in> (STAR r) \<rightarrow> (Stars vs)"
"\<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 (der c r) \<and> s\<^sub>4 \<in> L (STAR r))"
- apply(auto elim!: PMatch_elims(1-4) simp add: der_correctness Der_def intro: PMatch.intros)
+ apply(auto elim!: Posix_elims(1-4) simp add: der_correctness Der_def intro: Posix.intros)
apply(rotate_tac 3)
- apply(erule_tac PMatch_elims(5))
- apply (simp add: PMatch.intros(6))
- using PMatch.intros(7) by blast
+ apply(erule_tac Posix_elims(5))
+ apply (simp add: Posix.intros(6))
+ using Posix.intros(7) by blast
then show "(c # s) \<in> STAR r \<rightarrow> injval (STAR r) c v"
proof (cases)
case cons
@@ -582,14 +582,14 @@
have "s2 \<in> STAR r \<rightarrow> Stars vs" by fact
moreover
have "(c # s1) \<in> r \<rightarrow> injval r c v1" by fact
- then have "flat (injval r c v1) = (c # s1)" by (rule PMatch1)
+ then have "flat (injval r c v1) = (c # s1)" by (rule Posix1)
then have "flat (injval r c v1) \<noteq> []" by simp
moreover
have "\<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 (der c r) \<and> s\<^sub>4 \<in> L (STAR r))" by fact
then have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (c # s1) @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (STAR r))"
by (simp add: der_correctness Der_def)
ultimately
- have "((c # s1) @ s2) \<in> STAR r \<rightarrow> Stars (injval r c v1 # vs)" by (rule PMatch.intros)
+ have "((c # s1) @ s2) \<in> STAR r \<rightarrow> Stars (injval r c v1 # vs)" by (rule Posix.intros)
then show "(c # s) \<in> STAR r \<rightarrow> injval (STAR r) c v" using cons by(simp)
qed
qed
@@ -647,22 +647,22 @@
using assms
apply(induct s arbitrary: r)
apply(simp)
-apply (metis PMatch_mkeps nullable_correctness)
+apply (metis Posix_mkeps nullable_correctness)
apply(drule_tac x="der a r" in meta_spec)
apply(drule meta_mp)
apply(simp add: der_correctness Der_def)
apply(auto)
-by (metis PMatch2_roy_version)
+by (metis Posix2_roy_version)
lemma lex_correct3a:
shows "s \<in> L r \<longleftrightarrow> (\<exists>v. lexer r s = Some(v) \<and> s \<in> r \<rightarrow> v)"
using assms
apply(induct s arbitrary: r)
apply(simp)
-apply (metis PMatch_mkeps nullable_correctness)
+apply (metis Posix_mkeps nullable_correctness)
apply(drule_tac x="der a r" in meta_spec)
apply(auto)
-apply(metis PMatch2_roy_version)
+apply(metis Posix2_roy_version)
apply(simp add: der_correctness Der_def)
using lex_correct1a
apply fastforce
@@ -674,7 +674,7 @@
using assms
apply(induct s arbitrary: r)
apply(simp)
-apply (metis PMatch_mkeps nullable_correctness)
+apply (metis Posix_mkeps nullable_correctness)
apply(drule_tac x="der a r" in meta_spec)
apply(simp add: der_correctness Der_def)
apply(case_tac "lexer (der a r) s = None")
@@ -683,9 +683,9 @@
apply(clarify)
apply(rule iffI)
apply(auto)
-apply(rule PMatch2_roy_version)
+apply(rule Posix2_roy_version)
apply(simp)
-using PMatch1(1) by auto
+using Posix1(1) by auto
section {* Lexer including simplifications *}