--- a/thys/ReStar.thy Wed Mar 09 10:33:26 2016 +0000
+++ b/thys/ReStar.thy Thu Mar 10 23:43:04 2016 +0000
@@ -157,9 +157,7 @@
lemma der_correctness:
shows "L (der c r) = Der c (L r)"
-apply(induct r)
-apply(simp_all add: nullable_correctness)
-done
+by (induct r) (simp_all add: nullable_correctness)
section {* Values *}
@@ -206,11 +204,15 @@
| "\<turnstile> Stars [] : STAR r"
| "\<lbrakk>\<turnstile> v : r; \<turnstile> Stars vs : STAR r\<rbrakk> \<Longrightarrow> \<turnstile> Stars (v # vs) : STAR r"
-lemma not_nullable_flat:
- assumes "\<turnstile> v : r" "\<not> nullable r"
- shows "flat v \<noteq> []"
-using assms
-by (induct) (auto)
+inductive_cases Prf_elims:
+ "\<turnstile> v : ZERO"
+ "\<turnstile> v : SEQ r1 r2"
+ "\<turnstile> v : ALT r1 r2"
+ "\<turnstile> v : ONE"
+ "\<turnstile> v : CHAR c"
+(* "\<turnstile> vs : STAR r"*)
+
+
lemma Prf_flat_L:
assumes "\<turnstile> v : r" shows "flat v \<in> L r"
@@ -239,6 +241,7 @@
apply(simp)
done
+
lemma Star_val:
assumes "\<forall>s\<in>set ss. \<exists>v. s = flat v \<and> \<turnstile> v : r"
shows "\<exists>vs. concat (map flat vs) = concat ss \<and> (\<forall>v\<in>set vs. \<turnstile> v : r)"
@@ -258,8 +261,7 @@
apply (metis Prf.intros(1) flat.simps(5))
apply (metis Prf.intros(2) flat.simps(3))
apply (metis Prf.intros(3) flat.simps(4))
-apply(erule Prf.cases)
-apply(auto)
+apply(auto elim!: Prf_elims)
apply(subgoal_tac "\<exists>vs::val list. concat (map flat vs) = x \<and> (\<forall>v \<in> set vs. \<turnstile> v : r)")
apply(auto)[1]
apply(rule_tac x="Stars vs" in exI)
@@ -304,13 +306,6 @@
None \<Rightarrow> None
| Some(v) \<Rightarrow> Some(injval r c v))"
-fun
- matcher2 :: "rexp \<Rightarrow> string \<Rightarrow> val"
-where
- "matcher2 r [] = mkeps r"
-| "matcher2 r (c#s) = injval r c (matcher2 (der c r) s)"
-
-
section {* Mkeps, injval *}
@@ -318,67 +313,23 @@
assumes "nullable(r)"
shows "\<turnstile> mkeps r : r"
using assms
-apply(induct rule: nullable.induct)
-apply(auto intro: Prf.intros)
-done
+by (induct rule: nullable.induct)
+ (auto intro: Prf.intros)
lemma mkeps_flat:
assumes "nullable(r)"
shows "flat (mkeps r) = []"
using assms
-apply(induct rule: nullable.induct)
-apply(auto)
-done
+by (induct rule: nullable.induct) (auto)
+
lemma Prf_injval:
assumes "\<turnstile> v : der c r"
shows "\<turnstile> (injval r c v) : r"
using assms
apply(induct r arbitrary: c v rule: rexp.induct)
-apply(simp_all)
-(* ZERO *)
-apply(erule Prf.cases)
-apply(simp_all)[7]
-(* ONE *)
-apply(erule Prf.cases)
-apply(simp_all)[7]
-(* CHAR *)
-apply(case_tac "c = x")
-apply(simp)
-apply(erule Prf.cases)
-apply(simp_all)[7]
-apply(rule Prf.intros(5))
-apply(simp)
-apply(erule Prf.cases)
-apply(simp_all)[7]
-(* SEQ *)
-apply(case_tac "nullable x1")
-apply(simp)
-apply(erule Prf.cases)
-apply(simp_all)[7]
-apply(auto)[1]
-apply(erule Prf.cases)
-apply(simp_all)[7]
-apply(auto)[1]
-apply(rule Prf.intros)
-apply(auto)[2]
-apply (metis Prf.intros(1) mkeps_nullable)
-apply(simp)
-apply(erule Prf.cases)
-apply(simp_all)[7]
-apply(auto)[1]
-apply(rule Prf.intros)
-apply(auto)[2]
-(* ALT *)
-apply(erule Prf.cases)
-apply(simp_all)[7]
-apply(clarify)
-apply (metis Prf.intros(2))
-apply (metis Prf.intros(3))
+apply(auto intro!: Prf.intros mkeps_nullable elim!: Prf_elims split: if_splits)
(* STAR *)
-apply(erule Prf.cases)
-apply(simp_all)[7]
-apply(clarify)
apply(rotate_tac 2)
apply(erule Prf.cases)
apply(simp_all)[7]
@@ -479,6 +430,15 @@
apply(auto)
done
+inductive_cases PMatch_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"
+
+thm PMatch_elims
+
lemma PMatch_determ:
assumes "s \<in> r \<rightarrow> v1" "s \<in> r \<rightarrow> v2"
shows "v1 = v2"
@@ -560,7 +520,8 @@
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)
+ 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
@@ -612,9 +573,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)"
- 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
+ by (force split: if_splits elim!: PMatch_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
@@ -659,11 +618,9 @@
"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(auto elim!: PMatch_elims(1-4) simp add: der_correctness Der_def intro: PMatch.intros)
+ apply(rotate_tac 3)
+ apply(erule_tac PMatch_elims(5))
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"
@@ -777,25 +734,6 @@
apply(simp)
using PMatch1(1) by auto
-lemma lex_correct5:
- assumes "s \<in> L r"
- shows "s \<in> r \<rightarrow> (matcher2 r s)"
-using assms
-apply(induct s arbitrary: r)
-apply(simp)
-apply (metis PMatch_mkeps nullable_correctness)
-apply(simp)
-apply(rule PMatch2_roy_version)
-apply(drule_tac x="der a r" in meta_spec)
-apply(drule meta_mp)
-apply(simp add: der_correctness Der_def)
-apply(auto)
-done
-
-lemma
- "matcher2 (ALT (CHAR a) (ALT (CHAR b) (SEQ (CHAR a) (CHAR b)))) [a,b] = Right (Right (Seq (Char a) (Char b)))"
-apply(simp)
-done
fun F_RIGHT where
"F_RIGHT f v = Right (f v)"