# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1454946683 0
# Node ID 8b919b3d753ebd2ce0f90df31df28b57543fc700
# Parent  f76c250906d51bf0315c6bebf2c2ba309cd7deca
strengthened PMatch to get determ

diff -r f76c250906d5 -r 8b919b3d753e thys/Paper/Paper.thy
--- a/thys/Paper/Paper.thy	Mon Feb 08 11:54:48 2016 +0000
+++ b/thys/Paper/Paper.thy	Mon Feb 08 15:51:23 2016 +0000
@@ -176,7 +176,7 @@
   @{thm[mode=Rule] PMatch.intros(3)[of "s" "r\<^sub>1" "v" "r\<^sub>2"]}\qquad
   @{thm[mode=Rule] PMatch.intros(4)[of "s" "r\<^sub>2" "v" "r\<^sub>1"]}\medskip\\
   \multicolumn{1}{p{5cm}}{@{thm[mode=Rule] PMatch.intros(5)[of "s\<^sub>1" "r\<^sub>1" "v\<^sub>1" "s\<^sub>2" "r\<^sub>2" "v\<^sub>2"]}}\medskip\\
-  @{thm[mode=Rule] PMatch.intros(6)[of "s\<^sub>1" "r" "v" "s\<^sub>2" "vs"]} \qquad
+  @{thm[mode=Rule] PMatch.intros(6)[of "s\<^sub>1" "r" "v" "s\<^sub>2" "vs"]}\medskip\\
   @{thm[mode=Axiom] PMatch.intros(7)}\medskip\\
   \end{tabular}
   \end{center}
@@ -249,6 +249,9 @@
 
   @{thm[mode=IfThen] PMatch1N}
 
+  @{thm[mode=IfThen] PMatch_determ(1)[of "s" "r" "v\<^sub>1" "v\<^sub>2"]}
+
+  \medskip
   \noindent
   This is the main theorem that lets us prove that the algorithm is correct according to
   @{term "s \<in> r \<rightarrow> v"}:
diff -r f76c250906d5 -r 8b919b3d753e thys/ReStar.thy
--- a/thys/ReStar.thy	Mon Feb 08 11:54:48 2016 +0000
+++ b/thys/ReStar.thy	Mon Feb 08 15:51:23 2016 +0000
@@ -27,6 +27,37 @@
   and   "{} ;; A = {}"
 by (simp_all add: Sequ_def)
 
+definition
+  Der :: "char \<Rightarrow> string set \<Rightarrow> string set"
+where
+  "Der c A \<equiv> {s. [c] @ s \<in> A}"
+
+lemma Der_null [simp]:
+  shows "Der c {} = {}"
+unfolding Der_def
+by auto
+
+lemma Der_empty [simp]:
+  shows "Der c {[]} = {}"
+unfolding Der_def
+by auto
+
+lemma Der_char [simp]:
+  shows "Der c {[d]} = (if c = d then {[]} else {})"
+unfolding Der_def
+by auto
+
+lemma Der_union [simp]:
+  shows "Der c (A \<union> B) = Der c A \<union> Der c B"
+unfolding Der_def
+by auto
+
+lemma Der_seq [simp]:
+  shows "Der c (A ;; B) = (Der c A) ;; B \<union> (if [] \<in> A then Der c B else {})"
+unfolding Der_def Sequ_def
+apply (auto simp add: Cons_eq_append_conv)
+done
+
 lemma seq_image:
   assumes "\<forall>s1 s2. f (s1 @ s2) = (f s1) @ (f s2)"
   shows "f ` (A ;; B) = (f ` A) ;; (f ` B)"
@@ -49,6 +80,12 @@
   start[intro]: "[] \<in> A\<star>"
 | step[intro]:  "\<lbrakk>s1 \<in> A; s2 \<in> A\<star>\<rbrakk> \<Longrightarrow> s1 @ s2 \<in> A\<star>"
 
+lemma star_cases:
+  shows "A\<star> = {[]} \<union> A ;; A\<star>"
+unfolding Sequ_def
+by (auto) (metis Star.simps)
+
+
 fun 
   pow :: "string set \<Rightarrow> nat \<Rightarrow> string set" ("_ \<up> _" [100,100] 100)
 where
@@ -115,6 +152,23 @@
 by (induct x\<equiv>"c # x" rule: Star.induct) 
    (auto simp add: append_eq_Cons_conv)
 
+lemma Der_star [simp]:
+  shows "Der c (A\<star>) = (Der c A) ;; A\<star>"
+proof -    
+  have "Der c (A\<star>) = Der c ({[]} \<union> A ;; A\<star>)"
+    
+    by (simp only: star_cases[symmetric])
+  also have "... = Der c (A ;; A\<star>)"
+    by (simp only: Der_union Der_empty) (simp)
+  also have "... = (Der c A) ;; A\<star> \<union> (if [] \<in> A then Der c (A\<star>) else {})"
+    by simp
+  also have "... =  (Der c A) ;; A\<star>"
+    unfolding Sequ_def Der_def
+    by (auto dest: star_decomp)
+  finally show "Der c (A\<star>) = (Der c A) ;; A\<star>" .
+qed
+
+
 
 section {* Regular Expressions *}
 
@@ -154,6 +208,8 @@
 apply(auto simp add: Sequ_def) 
 done
 
+
+
 section {* Values *}
 
 datatype val = 
@@ -747,6 +803,12 @@
 | "ders (c # s) r = ders s (der c r)"
 
 
+lemma der_correctness:
+  shows "L (der c r) = Der c (L r)"
+apply(induct r) 
+apply(simp_all add: nullable_correctness)
+done
+
 section {* Injection function *}
 
 fun injval :: "rexp \<Rightarrow> char \<Rightarrow> val \<Rightarrow> val"
@@ -978,7 +1040,8 @@
 | "\<lbrakk>s1 \<in> r1 \<rightarrow> v1; s2 \<in> r2 \<rightarrow> v2;
     \<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 r1 \<and> s\<^sub>4 \<in> L r2)\<rbrakk> \<Longrightarrow> 
     (s1 @ s2) \<in> (SEQ r1 r2) \<rightarrow> (Seq v1 v2)"
-| "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> STAR r \<rightarrow> Stars vs; flat v \<noteq> []\<rbrakk>
+| "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> STAR r \<rightarrow> Stars vs; flat v \<noteq> [];
+    \<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 r \<and> s\<^sub>4 \<in> L (STAR r))\<rbrakk>
     \<Longrightarrow> (s1 @ s2) \<in> STAR r \<rightarrow> Stars (v # vs)"
 | "[] \<in> STAR r \<rightarrow> Stars []"
 
@@ -1036,6 +1099,103 @@
 apply(rule NPrf.intros)
 done
 
+lemma PMatch_determ:
+  shows "\<lbrakk>s \<in> r \<rightarrow> v1; s \<in> r \<rightarrow> v2\<rbrakk> \<Longrightarrow> v1 = v2"
+  and   "\<lbrakk>s \<in> (STAR r) \<rightarrow> Stars vs1; s \<in> (STAR r) \<rightarrow> Stars vs2\<rbrakk> \<Longrightarrow> vs1 = vs2"
+apply(induct v1 and vs1 arbitrary: s r v2 and s r vs2 rule: val.inducts)
+apply(erule PMatch.cases)
+apply(simp_all)[7]
+apply(erule PMatch.cases)
+apply(simp_all)[7]
+apply(erule PMatch.cases)
+apply(simp_all)[7]
+apply(erule PMatch.cases)
+apply(simp_all)[7]
+apply(erule PMatch.cases)
+apply(simp_all)[7]
+apply(erule PMatch.cases)
+apply(simp_all)[7]
+apply(clarify)
+apply(subgoal_tac "s1 = s1a \<and> s2 = s2a")
+apply metis
+apply(rule conjI)
+apply(simp add: append_eq_append_conv2)
+apply(auto)[1]
+apply (metis PMatch1(1) PMatch1(2) Prf_flat_L)
+apply (metis PMatch1(1) PMatch1(2) Prf_flat_L)
+apply(simp add: append_eq_append_conv2)
+apply(auto)[1]
+apply (metis PMatch1(1) PMatch1(2) Prf_flat_L)
+apply (metis PMatch1(1) PMatch1(2) Prf_flat_L)
+apply(erule PMatch.cases)
+apply(simp_all)[7]
+apply(clarify)
+apply(erule PMatch.cases)
+apply(simp_all)[7]
+apply(clarify)
+apply (metis NPrf_flat_L PMatch1(2) PMatch1N)
+apply(erule PMatch.cases)
+apply(simp_all)[7]
+apply(clarify)
+apply(erule PMatch.cases)
+apply(simp_all)[7]
+apply(clarify)
+apply (metis NPrf_flat_L PMatch1(2) PMatch1N)
+(* star case *)
+defer
+apply(erule PMatch.cases)
+apply(simp_all)[7]
+apply(clarify)
+apply(erule PMatch.cases)
+apply(simp_all)[7]
+apply(clarify)
+apply (metis PMatch1(2))
+apply(rotate_tac  3)
+apply(erule PMatch.cases)
+apply(simp_all)[7]
+apply(clarify)
+apply(erule PMatch.cases)
+apply(simp_all)[7]
+apply(clarify)
+apply(subgoal_tac "s1 = s1a \<and> s2 = s2a")
+apply metis
+apply(simp add: append_eq_append_conv2)
+apply(auto)[1]
+apply (metis L.simps(6) PMatch1(1) PMatch1(2) Prf_flat_L)
+apply (metis L.simps(6) PMatch1(1) PMatch1(2) Prf_flat_L)
+apply (metis L.simps(6) PMatch1(1) PMatch1(2) Prf_flat_L)
+apply (metis L.simps(6) PMatch1(1) PMatch1(2) Prf_flat_L)
+apply(erule PMatch.cases)
+apply(simp_all)[7]
+apply(clarify)
+apply (metis PMatch1(2))
+apply(erule PMatch.cases)
+apply(simp_all)[7]
+apply(clarify)
+apply(erule PMatch.cases)
+apply(simp_all)[7]
+apply(clarify)
+apply(subgoal_tac "s1 = s1a \<and> s2 = s2a")
+apply(drule_tac x="s1 @ s2" in meta_spec)
+apply(drule_tac x="rb" in meta_spec)
+apply(drule_tac x="(va#vsa)" in meta_spec)
+apply(simp)
+apply(drule meta_mp)
+apply (metis L.simps(6) PMatch.intros(6))
+apply (metis L.simps(6) PMatch.intros(6))
+apply(simp add: append_eq_append_conv2)
+apply(auto)[1]
+apply (metis L.simps(6) NPrf_flat_L PMatch1(2) PMatch1N)
+apply (metis L.simps(6) NPrf_flat_L PMatch1(2) PMatch1N)
+apply (metis L.simps(6) NPrf_flat_L PMatch1(2) PMatch1N)
+apply (metis L.simps(6) NPrf_flat_L PMatch1(2) PMatch1N)
+apply (metis PMatch1(2))
+apply(erule PMatch.cases)
+apply(simp_all)[7]
+apply(clarify)
+by (metis PMatch1(2))
+
+
 lemma PMatch_Values:
   assumes "s \<in> r \<rightarrow> v"
   shows "v \<in> Values r s"
@@ -1159,14 +1319,29 @@
 apply(simp)
 apply(simp)
 apply(simp)
+apply (metis L.simps(6))
 apply(subst v4)
 apply (metis NPrf_imp_Prf PMatch1N)
 apply(simp)
-apply (metis PMatch.intros(6) PMatch.intros(7) PMatch1(2) append_Nil2 list.discI)
+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(simp)
+apply(rotate_tac 2)
+apply(drule PMatch.intros(6))
+apply(rule PMatch.intros(7))
+apply (metis PMatch1(1) list.distinct(1) v4)
+apply (metis Nil_is_append_conv)
+apply(simp)
+apply(subst der_correctness)
+apply(simp add: Der_def)
 done
 
-
-
 lemma lex_correct1:
   assumes "s \<notin> L r"
   shows "lex r s = None"
@@ -1418,14 +1593,41 @@
 apply(simp_all)
 apply(erule ValOrd.cases)
 apply(simp_all)
+apply(rotate_tac 3)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(clarify)
+apply(erule ValOrd.cases)
+apply(simp_all)
+apply(erule ValOrd.cases)
+apply(simp_all)
+apply(clarify)
+apply(rotate_tac 4)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(clarify)
 apply(erule ValOrd.cases)
 apply(simp_all)
 apply(erule ValOrd.cases)
 apply(simp_all)
+apply(clarify)
+
+
 apply(erule ValOrd.cases)
 apply(simp_all)
-
-
+apply(auto)[1]
+prefer 2
+prefer 3
+apply(auto)[1]
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(clarify)
+apply(rotate_tac 3)
+apply(erule ValOrd.cases)
+apply(simp_all)
+apply(auto)[1]
 oops
 
 
diff -r f76c250906d5 -r 8b919b3d753e thys/paper.pdf
Binary file thys/paper.pdf has changed