diff -r 26202889f829 -r a8bcb5a0f9b9 thys/Re.thy
--- a/thys/Re.thy	Thu Dec 17 14:16:24 2015 +0000
+++ b/thys/Re.thy	Fri Dec 18 00:37:35 2015 +0000
@@ -391,6 +391,56 @@
 | "mkeps(SEQ r1 r2) = Seq (mkeps r1) (mkeps r2)"
 | "mkeps(ALT r1 r2) = (if nullable(r1) then Left (mkeps r1) else Right (mkeps r2))"
 
+section {* Derivatives *}
+
+fun
+ der :: "char \<Rightarrow> rexp \<Rightarrow> rexp"
+where
+  "der c (NULL) = NULL"
+| "der c (EMPTY) = NULL"
+| "der c (CHAR c') = (if c = c' then EMPTY else NULL)"
+| "der c (ALT r1 r2) = ALT (der c r1) (der c r2)"
+| "der c (SEQ r1 r2) = 
+     (if nullable r1
+      then ALT (SEQ (der c r1) r2) (der c r2)
+      else SEQ (der c r1) r2)"
+
+fun 
+ ders :: "string \<Rightarrow> rexp \<Rightarrow> rexp"
+where
+  "ders [] r = r"
+| "ders (c # s) r = ders s (der c r)"
+
+
+section {* Injection function *}
+
+fun injval :: "rexp \<Rightarrow> char \<Rightarrow> val \<Rightarrow> val"
+where
+  "injval (EMPTY) c Void = Char c"
+| "injval (CHAR d) c Void = Char d"
+| "injval (CHAR d) c (Char c') = Seq (Char d) (Char c')"
+| "injval (ALT r1 r2) c (Left v1) = Left(injval r1 c v1)"
+| "injval (ALT r1 r2) c (Right v2) = Right(injval r2 c v2)"
+| "injval (SEQ r1 r2) c (Char c') = Seq (Char c) (Char c')"
+| "injval (SEQ r1 r2) c (Seq v1 v2) = Seq (injval r1 c v1) v2"
+| "injval (SEQ r1 r2) c (Left (Seq v1 v2)) = Seq (injval r1 c v1) v2"
+| "injval (SEQ r1 r2) c (Right v2) = Seq (mkeps r1) (injval r2 c v2)"
+
+
+section {* Projection function *}
+
+fun projval :: "rexp \<Rightarrow> char \<Rightarrow> val \<Rightarrow> val"
+where
+  "projval (CHAR d) c _ = Void"
+| "projval (ALT r1 r2) c (Left v1) = Left (projval r1 c v1)"
+| "projval (ALT r1 r2) c (Right v2) = Right (projval r2 c v2)"
+| "projval (SEQ r1 r2) c (Seq v1 v2) = 
+     (if flat v1 = [] then Right(projval r2 c v2) 
+      else if nullable r1 then Left (Seq (projval r1 c v1) v2)
+                          else Seq (projval r1 c v1) v2)"
+
+
+
 lemma mkeps_nullable:
   assumes "nullable(r)" 
   shows "\<turnstile> mkeps r : r"
@@ -407,10 +457,306 @@
 apply(auto)
 done
 
-text {*
-  The value mkeps returns is always the correct POSIX
-  value.
-*}
+lemma v3:
+  assumes "\<turnstile> v : der c r" 
+  shows "\<turnstile> (injval r c v) : r"
+using assms
+apply(induct arbitrary: v rule: der.induct)
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(case_tac "c = c'")
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply (metis Prf.intros(5))
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply (metis Prf.intros(2))
+apply (metis Prf.intros(3))
+apply(simp)
+apply(case_tac "nullable r1")
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(auto)[1]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(auto)[1]
+apply (metis Prf.intros(1))
+apply(auto)[1]
+apply (metis Prf.intros(1) mkeps_nullable)
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(auto)[1]
+apply(rule Prf.intros)
+apply(auto)[2]
+done
+
+lemma v3_proj:
+  assumes "\<turnstile> v : r" and "\<exists>s. (flat v) = c # s"
+  shows "\<turnstile> (projval r c v) : der c r"
+using assms
+apply(induct rule: Prf.induct)
+prefer 4
+apply(simp)
+prefer 4
+apply(simp)
+apply (metis Prf.intros(4))
+prefer 2
+apply(simp)
+apply (metis Prf.intros(2))
+prefer 2
+apply(simp)
+apply (metis Prf.intros(3))
+apply(auto)
+apply(rule Prf.intros)
+apply(simp)
+apply (metis Prf_flat_L nullable_correctness)
+apply(rule Prf.intros)
+apply(rule Prf.intros)
+apply (metis Cons_eq_append_conv)
+apply(simp)
+apply(rule Prf.intros)
+apply (metis Cons_eq_append_conv)
+apply(simp)
+done
+
+lemma v4:
+  assumes "\<turnstile> v : der c r" 
+  shows "flat (injval r c v) = c # (flat v)"
+using assms
+apply(induct arbitrary: v rule: der.induct)
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(simp)
+apply(case_tac "c = c'")
+apply(simp)
+apply(auto)[1]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(simp)
+apply(case_tac "nullable r1")
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all (no_asm_use))[5]
+apply(auto)[1]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(clarify)
+apply(simp only: injval.simps flat.simps)
+apply(auto)[1]
+apply (metis mkeps_flat)
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+done
+
+lemma v4_proj:
+  assumes "\<turnstile> v : r" and "\<exists>s. (flat v) = c # s"
+  shows "c # flat (projval r c v) = flat v"
+using assms
+apply(induct rule: Prf.induct)
+prefer 4
+apply(simp)
+prefer 4
+apply(simp)
+prefer 2
+apply(simp)
+prefer 2
+apply(simp)
+apply(auto)
+by (metis Cons_eq_append_conv)
+
+lemma v4_proj2:
+  assumes "\<turnstile> v : r" and "(flat v) = c # s"
+  shows "flat (projval r c v) = s"
+using assms
+by (metis list.inject v4_proj)
+
+
+section {* Alternative Posix definition *}
+
+inductive 
+  PMatch :: "string \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<in> _ \<rightarrow> _" [100, 100, 100] 100)
+where
+  "[] \<in> EMPTY \<rightarrow> Void"
+| "[c] \<in> (CHAR c) \<rightarrow> (Char c)"
+| "s \<in> r1 \<rightarrow> v \<Longrightarrow> s \<in> (ALT r1 r2) \<rightarrow> (Left v)"
+| "\<lbrakk>s \<in> r2 \<rightarrow> v; s \<notin> L(r1)\<rbrakk> \<Longrightarrow> s \<in> (ALT r1 r2) \<rightarrow> (Right v)"
+| "\<lbrakk>s1 \<in> r1 \<rightarrow> v1; s2 \<in> r2 \<rightarrow> v2;
+    \<not>(\<exists>s3 s4. s3 \<noteq> [] \<and> s3 @ s4 = s2 \<and> (s1 @ s2) \<in> L r1 \<and> s4 \<in> L r2)\<rbrakk> \<Longrightarrow> 
+    (s1 @ s2) \<in> (SEQ r1 r2) \<rightarrow> (Seq v1 v2)"
+
+lemma PMatch_mkeps:
+  assumes "nullable r"
+  shows " [] \<in> r \<rightarrow> mkeps r"
+using assms
+apply(induct r)
+apply(auto)
+apply (metis PMatch.intros(1))
+apply(subst append.simps(1)[symmetric])
+apply (rule PMatch.intros)
+apply(simp)
+apply(simp)
+apply(auto)[1]
+apply (rule PMatch.intros)
+apply(simp)
+apply (rule PMatch.intros)
+apply(simp)
+apply (rule PMatch.intros)
+apply(simp)
+by (metis nullable_correctness)
+
+
+lemma PMatch1:
+  assumes "s \<in> r \<rightarrow> v"
+  shows "\<turnstile> v : r" "flat v = s"
+using assms
+apply(induct s r v rule: PMatch.induct)
+apply(auto)
+apply (metis Prf.intros(4))
+apply (metis Prf.intros(5))
+apply (metis Prf.intros(2))
+apply (metis Prf.intros(3))
+apply (metis Prf.intros(1))
+by (metis Prf.intros(1))
+
+lemma PMAtch2:
+  assumes "s \<in> (der c r) \<rightarrow> v"
+  shows "(c#s) \<in> r \<rightarrow> (injval r c v)"
+using assms
+apply(induct c r arbitrary: s v rule: der.induct)
+apply(auto)
+apply(erule PMatch.cases)
+apply(simp_all)[5]
+apply(erule PMatch.cases)
+apply(simp_all)[5]
+apply(case_tac "c = c'")
+apply(simp)
+apply(erule PMatch.cases)
+apply(simp_all)[5]
+apply (metis PMatch.intros(2))
+apply(simp)
+apply(erule PMatch.cases)
+apply(simp_all)[5]
+apply(erule PMatch.cases)
+apply(simp_all)[5]
+apply (metis PMatch.intros(3))
+apply(clarify)
+apply(rule PMatch.intros)
+apply metis
+apply(simp add: L_flat_Prf)
+apply(auto)[1]
+thm v3_proj
+apply(frule_tac c="c" in v3_proj)
+apply metis
+apply(drule_tac x="projval r1 c v" in spec)
+apply(drule mp)
+apply (metis v4_proj2)
+apply(simp)
+apply(case_tac "nullable r1")
+apply(simp)
+defer
+apply(simp)
+apply(erule PMatch.cases)
+apply(simp_all)[5]
+apply(clarify)
+apply(subst append.simps(2)[symmetric])
+apply(rule PMatch.intros)
+apply metis
+apply metis
+apply(auto)[1]
+apply(simp add: L_flat_Prf)
+apply(auto)[1]
+apply(frule_tac c="c" in v3_proj)
+apply metis
+apply(drule_tac x="projval r1 c v" in spec)
+apply(drule mp)
+apply (metis v4_proj2)
+apply(simp)
+(* nullable case *)
+apply(erule PMatch.cases)
+apply(simp_all)[5]
+apply(clarify)
+apply(erule PMatch.cases)
+apply(simp_all)[5]
+apply(clarify)
+apply(subst append.simps(2)[symmetric])
+apply(rule PMatch.intros)
+apply metis
+apply metis
+apply(auto)[1]
+apply(simp add: L_flat_Prf)
+apply(auto)[1]
+apply(frule_tac c="c" in v3_proj)
+apply metis
+apply(drule_tac x="projval r1 c v" in spec)
+apply(drule mp)
+apply (metis v4_proj2)
+apply(simp)
+(* interesting case *)
+apply(clarify)
+apply(simp)
+thm L.simps
+apply(subst (asm) L.simps(4)[symmetric])
+apply(simp only: L_flat_Prf)
+apply(simp)
+apply(subst append.simps(1)[symmetric])
+apply(rule PMatch.intros)
+apply (metis PMatch_mkeps)
+apply metis
+apply(auto)
+apply(simp only: L_flat_Prf)
+apply(simp)
+apply(auto)
+apply(drule_tac x="projval r1 c v" in spec)
+apply(drule mp)
+apply (metis v4_proj2)
+apply(rotate_tac 1)
+apply(drule_tac x="sa" in meta_spec)
+apply(drule_tac x="va" in meta_spec)
+apply(simp)
+apply(rotate_tac 2)
+apply(drule_tac x="sa" in meta_spec)
+apply(drule_tac x="projval r1 c v" in meta_spec)
+apply(drule meta_mp)
+apply(frule_tac c="c" in v3_proj)
+apply metis
+
+apply(frule PMatch1(1))
+apply(drule PMatch1(2))
+apply(clarify)
+apply(subst (asm) (2) not_def)
+apply(drule mp)
+thm v3_proj
+apply(rule v3_proj)
+apply(rule conjI)
+apply (metis v4_proj2)
+apply (metis v3_proj)
+v3_proj
+
+
+
+
 
 section {* Sulzmann's Ordering of values *}
 
@@ -752,196 +1098,17 @@
 by simp
 
 
-section {* Derivatives *}
-
-fun
- der :: "char \<Rightarrow> rexp \<Rightarrow> rexp"
-where
-  "der c (NULL) = NULL"
-| "der c (EMPTY) = NULL"
-| "der c (CHAR c') = (if c = c' then EMPTY else NULL)"
-| "der c (ALT r1 r2) = ALT (der c r1) (der c r2)"
-| "der c (SEQ r1 r2) = 
-     (if nullable r1
-      then ALT (SEQ (der c r1) r2) (der c r2)
-      else SEQ (der c r1) r2)"
-
-fun 
- ders :: "string \<Rightarrow> rexp \<Rightarrow> rexp"
-where
-  "ders [] r = r"
-| "ders (c # s) r = ders s (der c r)"
-
-
-section {* Injection function *}
-
-fun injval :: "rexp \<Rightarrow> char \<Rightarrow> val \<Rightarrow> val"
-where
-  "injval (EMPTY) c Void = Char c"
-| "injval (CHAR d) c Void = Char d"
-| "injval (CHAR d) c (Char c') = Seq (Char d) (Char c')"
-| "injval (ALT r1 r2) c (Left v1) = Left(injval r1 c v1)"
-| "injval (ALT r1 r2) c (Right v2) = Right(injval r2 c v2)"
-| "injval (SEQ r1 r2) c (Char c') = Seq (Char c) (Char c')"
-| "injval (SEQ r1 r2) c (Seq v1 v2) = Seq (injval r1 c v1) v2"
-| "injval (SEQ r1 r2) c (Left (Seq v1 v2)) = Seq (injval r1 c v1) v2"
-| "injval (SEQ r1 r2) c (Right v2) = Seq (mkeps r1) (injval r2 c v2)"
-
-
-section {* Projection function *}
-
-fun projval :: "rexp \<Rightarrow> char \<Rightarrow> val \<Rightarrow> val"
-where
-  "projval (CHAR d) c _ = Void"
-| "projval (ALT r1 r2) c (Left v1) = Left (projval r1 c v1)"
-| "projval (ALT r1 r2) c (Right v2) = Right (projval r2 c v2)"
-| "projval (SEQ r1 r2) c (Seq v1 v2) = 
-     (if flat v1 = [] then Right(projval r2 c v2) 
-      else if nullable r1 then Left (Seq (projval r1 c v1) v2)
-                          else Seq (projval r1 c v1) v2)"
 
 text {*
   Injection value is related to r
 *}
 
-lemma v3:
-  assumes "\<turnstile> v : der c r" 
-  shows "\<turnstile> (injval r c v) : r"
-using assms
-apply(induct arbitrary: v rule: der.induct)
-apply(simp)
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(simp)
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(case_tac "c = c'")
-apply(simp)
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply (metis Prf.intros(5))
-apply(simp)
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(simp)
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply (metis Prf.intros(2))
-apply (metis Prf.intros(3))
-apply(simp)
-apply(case_tac "nullable r1")
-apply(simp)
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(auto)[1]
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(auto)[1]
-apply (metis Prf.intros(1))
-apply(auto)[1]
-apply (metis Prf.intros(1) mkeps_nullable)
-apply(simp)
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(auto)[1]
-apply(rule Prf.intros)
-apply(auto)[2]
-done
 
-lemma v3_proj:
-  assumes "\<turnstile> v : r" and "\<exists>s. (flat v) = c # s"
-  shows "\<turnstile> (projval r c v) : der c r"
-using assms
-apply(induct rule: Prf.induct)
-prefer 4
-apply(simp)
-prefer 4
-apply(simp)
-apply (metis Prf.intros(4))
-prefer 2
-apply(simp)
-apply (metis Prf.intros(2))
-prefer 2
-apply(simp)
-apply (metis Prf.intros(3))
-apply(auto)
-apply(rule Prf.intros)
-apply(simp)
-apply (metis Prf_flat_L nullable_correctness)
-apply(rule Prf.intros)
-apply(rule Prf.intros)
-apply (metis Cons_eq_append_conv)
-apply(simp)
-apply(rule Prf.intros)
-apply (metis Cons_eq_append_conv)
-apply(simp)
-done
 
 text {*
   The string behind the injection value is an added c
 *}
 
-lemma v4:
-  assumes "\<turnstile> v : der c r" 
-  shows "flat (injval r c v) = c # (flat v)"
-using assms
-apply(induct arbitrary: v rule: der.induct)
-apply(simp)
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(simp)
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(simp)
-apply(case_tac "c = c'")
-apply(simp)
-apply(auto)[1]
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(simp)
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(simp)
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(simp)
-apply(case_tac "nullable r1")
-apply(simp)
-apply(erule Prf.cases)
-apply(simp_all (no_asm_use))[5]
-apply(auto)[1]
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(clarify)
-apply(simp only: injval.simps flat.simps)
-apply(auto)[1]
-apply (metis mkeps_flat)
-apply(simp)
-apply(erule Prf.cases)
-apply(simp_all)[5]
-done
-
-lemma v4_proj:
-  assumes "\<turnstile> v : r" and "\<exists>s. (flat v) = c # s"
-  shows "c # flat (projval r c v) = flat v"
-using assms
-apply(induct rule: Prf.induct)
-prefer 4
-apply(simp)
-prefer 4
-apply(simp)
-prefer 2
-apply(simp)
-prefer 2
-apply(simp)
-apply(auto)
-by (metis Cons_eq_append_conv)
-
-lemma v4_proj2:
-  assumes "\<turnstile> v : r" and "(flat v) = c # s"
-  shows "flat (projval r c v) = s"
-using assms
-by (metis list.inject v4_proj)
 
 lemma injval_inj: "inj_on (injval r c) {v. \<turnstile> v : der c r}"
 apply(induct c r rule: der.induct)