--- a/thys/ReStar.thy Mon Mar 07 03:23:28 2016 +0000
+++ b/thys/ReStar.thy Mon Mar 07 18:56:41 2016 +0000
@@ -582,131 +582,158 @@
apply(clarify)
by (metis PMatch1(2))
-
-
-
(* a proof that does not need proj *)
lemma PMatch2_roy_version:
assumes "s \<in> (der c r) \<rightarrow> v"
shows "(c#s) \<in> r \<rightarrow> (injval r c v)"
using assms
-apply(induct r arbitrary: s v c rule: rexp.induct)
-apply(auto)
-(* ZERO case *)
-apply(erule PMatch.cases)
-apply(simp_all)[7]
-(* ONE case *)
-apply(erule PMatch.cases)
-apply(simp_all)[7]
-(* CHAR case *)
-apply(case_tac "c = x")
-apply(simp)
-apply(erule PMatch.cases)
-apply(simp_all)[7]
-apply (metis PMatch.intros(2))
-apply(simp)
-apply(erule PMatch.cases)
-apply(simp_all)[7]
-(* ALT case *)
-prefer 2
-apply(erule PMatch.cases)
-apply(simp_all)[7]
-apply (metis PMatch.intros(3))
-apply(clarify)
-apply(rule PMatch.intros)
-apply metis
-apply(simp add: der_correctness Der_def)
-(* SEQ case *)
-apply(case_tac "nullable x1")
-apply(simp)
-prefer 2
-(* not-nullbale case *)
-apply(simp)
-apply(erule PMatch.cases)
-apply(simp_all)[7]
-apply(clarify)
-apply(subst append.simps(2)[symmetric])
-apply(rule PMatch.intros)
-apply metis
-apply metis
-apply(auto)[1]
-apply(simp add: der_correctness Der_def)
-apply(auto)[1]
-(* nullable case *)
-apply(erule PMatch.cases)
-apply(simp_all)[7]
-(* left case *)
-apply(clarify)
-apply(erule PMatch.cases)
-apply(simp_all)[4]
-prefer 2
-apply(clarify)
-prefer 2
-apply(clarify)
-apply(clarify)
-apply(simp (no_asm))
-apply(subst append.simps(2)[symmetric])
-apply(rule PMatch.intros)
-apply metis
-apply metis
-apply(erule contrapos_nn)
-apply(erule exE)+
-apply(auto)[1]
-apply(simp add: der_correctness Der_def)
-apply metis
-(* right interesting case *)
-apply(clarify)
-apply(subst append.simps(1)[symmetric])
-apply(rule PMatch.intros)
-apply (metis PMatch_mkeps)
-apply metis
-apply(rule notI)
-apply(clarify)
-apply(simp)
-apply(simp add: der_correctness)
-apply(simp only: Der_def Sequ_def)
-apply(simp)
-apply (metis Cons_eq_append_conv)
-(* Stars case *)
-apply(erule PMatch.cases)
-apply(simp_all)[7]
-apply(clarify)
-apply(rotate_tac 2)
-apply(frule_tac PMatch1)
-apply(erule PMatch.cases)
-apply(simp_all)[7]
-apply(subst append.simps(2)[symmetric])
-apply(rule PMatch.intros)
-apply metis
-apply(auto)[1]
-apply(rule PMatch.intros)
-apply(simp)
-apply(simp)
-apply(simp)
-apply (metis L.simps(6))
-apply(subst Prf_injval_flat)
-apply (metis PMatch1)
-apply(simp)
-apply(auto)[1]
-apply(drule_tac x="s\<^sub>3" in spec)
-apply(drule mp)
-defer
-apply metis
-apply(clarify)
-apply(drule_tac x="s1" in meta_spec)
-apply(drule_tac x="v1" in meta_spec)
-apply(drule_tac x="c" in meta_spec)
-apply(simp)
-apply(rotate_tac 2)
-apply(drule PMatch.intros(6))
-apply(rule PMatch.intros(7))
-(* HERE *)
-apply (metis PMatch1(1) list.distinct(1) Prf_injval_flat)
-apply (metis Nil_is_append_conv)
-apply(simp)
-apply(subst der_correctness)
-apply(simp add: Der_def)
-done
+proof(induct r arbitrary: s v rule: rexp.induct)
+ case ZERO
+ have "s \<in> der c ZERO \<rightarrow> v" by fact
+ then have "s \<in> ZERO \<rightarrow> v" by simp
+ then have "False" by cases
+ then show "(c#s) \<in> ZERO \<rightarrow> (injval ZERO c v)" by simp
+next
+ case ONE
+ have "s \<in> der c ONE \<rightarrow> v" by fact
+ then have "s \<in> ZERO \<rightarrow> v" by simp
+ then have "False" by cases
+ then show "(c#s) \<in> ONE \<rightarrow> (injval ONE c v)" by simp
+next
+ case (CHAR d)
+ consider (eq) "c = d" | (ineq) "c \<noteq> d" by blast
+ then show "(c#s) \<in> (CHAR d) \<rightarrow> (injval (CHAR d) c v)"
+ proof (cases)
+ case eq
+ have "s \<in> der c (CHAR d) \<rightarrow> v" by fact
+ 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)
+ next
+ case ineq
+ have "s \<in> der c (CHAR d) \<rightarrow> v" by fact
+ then have "s \<in> ZERO \<rightarrow> v" using ineq by simp
+ then have "False" by cases
+ then show "(c # s) \<in> CHAR d \<rightarrow> injval (CHAR d) c v" by simp
+ qed
+next
+ case (ALT r1 r2)
+ have IH1: "\<And>s v. s \<in> der c r1 \<rightarrow> v \<Longrightarrow> (c # s) \<in> r1 \<rightarrow> injval r1 c v" by fact
+ have IH2: "\<And>s v. s \<in> der c r2 \<rightarrow> v \<Longrightarrow> (c # s) \<in> r2 \<rightarrow> injval r2 c v" by fact
+ have "s \<in> der c (ALT r1 r2) \<rightarrow> v" by fact
+ then have "s \<in> ALT (der c r1) (der c r2) \<rightarrow> v" by simp
+ then consider (left) v' where "v = Left v'" "s \<in> der c r1 \<rightarrow> v'"
+ | (right) v' where "v = Right v'" "s \<notin> L (der c r1)" "s \<in> der c r2 \<rightarrow> v'"
+ by cases auto
+ then show "(c # s) \<in> ALT r1 r2 \<rightarrow> injval (ALT r1 r2) c v"
+ proof (cases)
+ 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 show "(c # s) \<in> ALT r1 r2 \<rightarrow> injval (ALT r1 r2) c v" using left by simp
+ next
+ case right
+ have "s \<notin> L (der c r1)" by fact
+ then have "c # s \<notin> L r1" by (simp add: der_correctness Der_def)
+ moreover
+ 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)
+ then show "(c # s) \<in> ALT r1 r2 \<rightarrow> injval (ALT r1 r2) c v" using right by simp
+ qed
+next
+ case (SEQ r1 r2)
+ have IH1: "\<And>s v. s \<in> der c r1 \<rightarrow> v \<Longrightarrow> (c # s) \<in> r1 \<rightarrow> injval r1 c v" by fact
+ have IH2: "\<And>s v. s \<in> der c r2 \<rightarrow> v \<Longrightarrow> (c # s) \<in> r2 \<rightarrow> injval r2 c v" by fact
+ have "s \<in> der c (SEQ r1 r2) \<rightarrow> v" by fact
+ then consider
+ (left_nullable) v1 v2 s1 s2 where
+ "v = Left (Seq v1 v2)" "s = s1 @ s2"
+ "s1 \<in> der c r1 \<rightarrow> v1" "s2 \<in> r2 \<rightarrow> v2" "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)"
+ | (right_nullable) v1 s1 s2 where
+ "v = Right v1" "s = s1 @ s2"
+ "s \<in> der c r2 \<rightarrow> v1" "nullable r1" "s1 @ s2 \<notin> L (SEQ (der c r1) r2)"
+ | (not_nullable) v1 v2 s1 s2 where
+ "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)"
+ apply(auto split: if_splits simp add: Sequ_def) apply(erule PMatch.cases)
+ apply(auto elim: PMatch.cases simp add: Sequ_def der_correctness Der_def)
+ by fastforce
+ then show "(c # s) \<in> SEQ r1 r2 \<rightarrow> injval (SEQ r1 r2) c v"
+ proof (cases)
+ case left_nullable
+ have "s1 \<in> der c r1 \<rightarrow> v1" by fact
+ then have "(c # s1) \<in> r1 \<rightarrow> injval r1 c v1" using IH1 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 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)
+ 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)
+ 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
+ moreover
+ have "s1 @ s2 \<notin> L (SEQ (der c r1) r2)" by fact
+ 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)
+ then show "(c # s) \<in> SEQ r1 r2 \<rightarrow> injval (SEQ r1 r2) c v" using right_nullable by simp
+ next
+ case not_nullable
+ have "s1 \<in> der c r1 \<rightarrow> v1" by fact
+ then have "(c # s1) \<in> r1 \<rightarrow> injval r1 c v1" using IH1 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 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)
+ then show "(c # s) \<in> SEQ r1 r2 \<rightarrow> injval (SEQ r1 r2) c v" using not_nullable by simp
+ qed
+next
+ case (STAR r)
+ have IH: "\<And>s v. s \<in> der c r \<rightarrow> v \<Longrightarrow> (c # s) \<in> r \<rightarrow> injval r c v" by fact
+ have "s \<in> der c (STAR r) \<rightarrow> v" by fact
+ then consider
+ (cons) v1 vs s1 s2 where
+ "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(erule_tac PMatch.cases)
+ apply(auto)
+ apply(rotate_tac 4)
+ apply(erule_tac PMatch.cases)
+ apply(auto)
+ apply (simp add: PMatch.intros(6))
+ using PMatch.intros(7) by blast
+ then show "(c # s) \<in> STAR r \<rightarrow> injval (STAR r) c v"
+ proof (cases)
+ case cons
+ have "s1 \<in> der c r \<rightarrow> v1" by fact
+ then have "(c # s1) \<in> r \<rightarrow> injval r c v1" using IH by simp
+ moreover
+ 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) \<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)
+ then show "(c # s) \<in> STAR r \<rightarrow> injval (STAR r) c v" using cons by(simp)
+ qed
+qed
lemma lex_correct1:
assumes "s \<notin> L r"