diff -r 1dfc08ca43da -r fe177dfc4697 thys/Re.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/thys/Re.thy	Mon Sep 08 14:06:15 2014 +0100
@@ -0,0 +1,1711 @@
+theory Matcher3simple
+  imports "Main" 
+begin
+
+section {* Sequential Composition of Sets *}
+
+definition
+  Sequ :: "string set \<Rightarrow> string set \<Rightarrow> string set" ("_ ;; _" [100,100] 100)
+where 
+  "A ;; B = {s1 @ s2 | s1 s2. s1 \<in> A \<and> s2 \<in> B}"
+
+text {* Two Simple Properties about Sequential Composition *}
+
+lemma seq_empty [simp]:
+  shows "A ;; {[]} = A"
+  and   "{[]} ;; A = A"
+by (simp_all add: Sequ_def)
+
+lemma seq_null [simp]:
+  shows "A ;; {} = {}"
+  and   "{} ;; A = {}"
+by (simp_all add: Sequ_def)
+
+section {* Regular Expressions *}
+
+datatype rexp =
+  NULL
+| EMPTY
+| CHAR char
+| SEQ rexp rexp
+| ALT rexp rexp
+
+section {* Semantics of Regular Expressions *}
+ 
+fun
+  L :: "rexp \<Rightarrow> string set"
+where
+  "L (NULL) = {}"
+| "L (EMPTY) = {[]}"
+| "L (CHAR c) = {[c]}"
+| "L (SEQ r1 r2) = (L r1) ;; (L r2)"
+| "L (ALT r1 r2) = (L r1) \<union> (L r2)"
+
+datatype val = 
+  Void
+| Char char
+| Seq val val
+| Right val
+| Left val
+
+inductive Prf :: "val \<Rightarrow> rexp \<Rightarrow> bool" ("\<turnstile> _ : _" [100, 100] 100)
+where
+ "\<lbrakk>\<turnstile> v1 : r1; \<turnstile> v2 : r2\<rbrakk> \<Longrightarrow> \<turnstile> Seq v1 v2 : SEQ r1 r2"
+| "\<turnstile> v1 : r1 \<Longrightarrow> \<turnstile> Left v1 : ALT r1 r2"
+| "\<turnstile> v2 : r2 \<Longrightarrow> \<turnstile> Right v2 : ALT r1 r2"
+| "\<turnstile> Void : EMPTY"
+| "\<turnstile> Char c : CHAR c"
+
+fun flat :: "val \<Rightarrow> string"
+where
+  "flat(Void) = []"
+| "flat(Char c) = [c]"
+| "flat(Left v) = flat(v)"
+| "flat(Right v) = flat(v)"
+| "flat(Seq v1 v2) = flat(v1) @ flat(v2)"
+
+datatype tree = 
+  Leaf string
+| Branch tree tree
+
+fun flats :: "val \<Rightarrow> tree"
+where
+  "flats(Void) = Leaf []"
+| "flats(Char c) = Leaf [c]"
+| "flats(Left v) = flats(v)"
+| "flats(Right v) = flats(v)"
+| "flats(Seq v1 v2) = Branch (flats v1) (flats v2)"
+
+fun flatten :: "tree \<Rightarrow> string"
+where
+  "flatten (Leaf s) = s"
+| "flatten (Branch t1 t2) = flatten t1 @ flatten t2" 
+
+lemma flats_flat:
+  shows "flat v1 = flatten (flats v1)"
+apply(induct v1)
+apply(simp_all)
+done
+
+lemma Prf_flat_L:
+  assumes "\<turnstile> v : r" shows "flat v \<in> L r"
+using assms
+apply(induct)
+apply(auto simp add: Sequ_def)
+done
+
+lemma L_flat_Prf:
+  "L(r) = {flat v | v. \<turnstile> v : r}"
+apply(induct r)
+apply(auto dest: Prf_flat_L simp add: Sequ_def)
+apply (metis Prf.intros(4) flat.simps(1))
+apply (metis Prf.intros(5) flat.simps(2))
+apply (metis Prf.intros(1) flat.simps(5))
+apply (metis Prf.intros(2) flat.simps(3))
+apply (metis Prf.intros(3) flat.simps(4))
+by (smt Prf.cases flat.simps(3) flat.simps(4) rexp.distinct(13) rexp.distinct(17) rexp.distinct(19) rexp.inject(3))
+
+inductive ValOrd :: "val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<succ>_ _" [100, 100, 100] 100)
+where
+  "\<lbrakk>v1 \<succ>r1 v1'; v2 \<succ>r2 v2'\<rbrakk> \<Longrightarrow> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1' v2')" 
+| "length (flat v1) \<ge> length (flat v2) \<Longrightarrow> (Left v1) \<succ>(ALT r1 r2) (Right v2)"
+| "length (flat v2) > length (flat v1) \<Longrightarrow> (Right v2) \<succ>(ALT r1 r2) (Left v1)"
+| "v2 \<succ>r2 v2' \<Longrightarrow> (Right v2) \<succ>(ALT r1 r2) (Right v2')"
+| "v1 \<succ>r1 v1' \<Longrightarrow> (Left v1) \<succ>(ALT r1 r2) (Left v1')"
+| "Void \<succ>EMPTY Void"
+| "(Char c) \<succ>(CHAR c) (Char c)"
+
+lemma
+  assumes "r = SEQ (ALT EMPTY EMPTY) (ALT EMPTY (CHAR c))"
+  shows "(Seq (Left Void) (Right (Char c))) \<succ>r (Seq (Left Void) (Left Void))"
+using assms
+apply(simp)
+apply(rule ValOrd.intros)
+apply(rule ValOrd.intros)
+apply(rule ValOrd.intros)
+apply(rule ValOrd.intros)
+apply(simp)
+done
+
+
+definition POSIX :: "val \<Rightarrow> rexp \<Rightarrow> bool" 
+where
+  "POSIX v r \<equiv> (\<forall>v'. (\<turnstile> v' : r \<and> flats v = flats v') \<longrightarrow> v \<succ>r v')"
+
+lemma POSIX:
+  assumes "r = SEQ (ALT EMPTY EMPTY) (ALT EMPTY (CHAR c))"
+  shows "POSIX (Seq (Left Void) (Right (Char c))) r"
+apply(simp add: POSIX_def assms)
+apply(auto)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(rule ValOrd.intros)
+apply (smt POSIX_def Prf.cases Prf.simps ValOrd.intros(2) ValOrd.intros(5) ValOrd.intros(6) flats.simps(1) flats.simps(3) rexp.distinct(11) rexp.distinct(13) rexp.distinct(17) rexp.distinct(19) rexp.distinct(9) rexp.inject(3) val.distinct(19) val.inject(3))
+by (smt Prf.simps ValOrd.intros(4) ValOrd.intros(7) flats.simps(1) flats.simps(3) list.distinct(1) rexp.distinct(11) rexp.distinct(13) rexp.distinct(15) rexp.distinct(17) rexp.distinct(19) rexp.distinct(9) rexp.inject(1) rexp.inject(3) tree.inject(1))
+
+
+lemma Exists_POSIX: "\<exists>v. POSIX v r"
+apply(induct r)
+apply(auto simp add: POSIX_def)
+apply(rule exI)
+apply(auto)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply (smt Prf.simps ValOrd.intros(6) rexp.distinct(11) rexp.distinct(13) rexp.distinct(9))
+apply(rule exI)
+apply(auto)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(rule ValOrd.intros)
+apply(rule exI)
+apply(auto)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(rule ValOrd.intros)
+apply(auto)[2]
+apply(rule_tac x="Left v" in exI)
+apply(auto)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(rule ValOrd.intros)
+apply(auto)[1]
+apply(auto)
+apply(rule ValOrd.intros)
+by (metis flats_flat order_refl)
+
+
+lemma POSIX_SEQ:
+  assumes "POSIX (Seq v1 v2) (SEQ r1 r2)" "\<turnstile> v1 : r1" "\<turnstile> v2 : r2"
+  shows "POSIX v1 r1 \<and> POSIX v2 r2"
+using assms
+unfolding POSIX_def
+apply(auto)
+apply(drule_tac x="Seq v' v2" in spec)
+apply(simp)
+apply (smt Prf.intros(1) ValOrd.simps assms(3) rexp.inject(2) val.distinct(15) val.distinct(17) val.distinct(3) val.distinct(9) val.inject(2))
+apply(drule_tac x="Seq v1 v'" in spec)
+apply(simp)
+by (smt Prf.intros(1) ValOrd.simps rexp.inject(2) val.distinct(15) val.distinct(17) val.distinct(3) val.distinct(9) val.inject(2))
+
+lemma POSIX_SEQ_I:
+  assumes "POSIX v1 r1" "POSIX v2 r2" 
+  shows "POSIX (Seq v1 v2) (SEQ r1 r2)" 
+using assms
+unfolding POSIX_def
+apply(auto)
+apply(rotate_tac 4)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(auto)[1]
+apply(rule ValOrd.intros)
+apply(auto)
+done
+
+lemma POSIX_ALT:
+  assumes "POSIX (Left v1) (ALT r1 r2)"
+  shows "POSIX v1 r1"
+using assms
+unfolding POSIX_def
+apply(auto)
+apply(drule_tac x="Left v'" in spec)
+apply(simp)
+apply(drule mp)
+apply(rule Prf.intros)
+apply(auto)
+apply(erule ValOrd.cases)
+apply(simp_all)[7]
+done
+
+lemma POSIX_ALT1a:
+  assumes "POSIX (Right v2) (ALT r1 r2)"
+  shows "POSIX v2 r2"
+using assms
+unfolding POSIX_def
+apply(auto)
+apply(drule_tac x="Right v'" in spec)
+apply(simp)
+apply(drule mp)
+apply(rule Prf.intros)
+apply(auto)
+apply(erule ValOrd.cases)
+apply(simp_all)[7]
+done
+
+lemma POSIX_ALT1b:
+  assumes "POSIX (Right v2) (ALT r1 r2)"
+  shows "(\<forall>v'. (\<turnstile> v' : r2 \<and> flats v' = flats v2) \<longrightarrow> v2 \<succ>r2 v')"
+using assms
+apply(drule_tac POSIX_ALT1a)
+unfolding POSIX_def
+apply(auto)
+done
+
+lemma POSIX_ALT_I1:
+  assumes "POSIX v1 r1" 
+  shows "POSIX (Left v1) (ALT r1 r2)"
+using assms
+unfolding POSIX_def
+apply(auto)
+apply(rotate_tac 3)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(auto)
+apply(rule ValOrd.intros)
+apply(auto)
+apply(rule ValOrd.intros)
+by (metis flats_flat order_refl)
+
+lemma POSIX_ALT_I2:
+  assumes "POSIX v2 r2" "\<forall>v'. \<turnstile> v' : r1 \<longrightarrow> length (flat v2) > length (flat v')"
+  shows "POSIX (Right v2) (ALT r1 r2)"
+using assms
+unfolding POSIX_def
+apply(auto)
+apply(rotate_tac 3)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(auto)
+prefer 2
+apply(rule ValOrd.intros)
+apply metis
+apply(rule ValOrd.intros)
+apply(auto)
+done
+
+lemma ValOrd_refl:
+  assumes "\<turnstile> v : r"
+  shows "v \<succ>r v"
+using assms
+apply(induct)
+apply(auto intro: ValOrd.intros)
+done
+
+lemma ValOrd_length:
+  assumes "v1 \<succ>r v2" shows "length (flat v1) \<ge> length (flat v2)"
+using assms
+apply(induct)
+apply(auto)
+done
+
+section {* The Matcher *}
+
+fun
+ nullable :: "rexp \<Rightarrow> bool"
+where
+  "nullable (NULL) = False"
+| "nullable (EMPTY) = True"
+| "nullable (CHAR c) = False"
+| "nullable (ALT r1 r2) = (nullable r1 \<or> nullable r2)"
+| "nullable (SEQ r1 r2) = (nullable r1 \<and> nullable r2)"
+
+lemma nullable_correctness:
+  shows "nullable r  \<longleftrightarrow> [] \<in> (L r)"
+apply (induct r) 
+apply(auto simp add: Sequ_def) 
+done
+
+fun mkeps :: "rexp \<Rightarrow> val"
+where
+  "mkeps(EMPTY) = Void"
+| "mkeps(SEQ r1 r2) = Seq (mkeps r1) (mkeps r2)"
+| "mkeps(ALT r1 r2) = (if nullable(r1) then Left (mkeps r1) else Right (mkeps r2))"
+
+lemma mkeps_nullable:
+  assumes "nullable(r)" shows "\<turnstile> mkeps r : r"
+using assms
+apply(induct rule: nullable.induct)
+apply(auto intro: Prf.intros)
+done
+
+lemma mkeps_flat:
+  assumes "nullable(r)" shows "flat (mkeps r) = []"
+using assms
+apply(induct rule: nullable.induct)
+apply(auto)
+done
+
+
+lemma mkeps_flats:
+  assumes "nullable(r)" shows "flatten (flats (mkeps r)) = []"
+using assms
+apply(induct rule: nullable.induct)
+apply(auto)
+done
+
+lemma mkeps_POSIX:
+  assumes "nullable r"
+  shows "POSIX (mkeps r) r"
+using assms
+apply(induct r)
+apply(auto)
+apply(simp add: POSIX_def)
+apply(auto)[1]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply (metis ValOrd.intros(6))
+apply(simp add: POSIX_def)
+apply(auto)[1]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(auto)
+apply (metis ValOrd.intros(1) append_is_Nil_conv mkeps_flat)
+apply(simp add: POSIX_def)
+apply(auto)[1]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(auto)
+apply (metis ValOrd.intros(5))
+apply(rule ValOrd.intros(2))
+apply(simp add: mkeps_flat)
+apply(simp add: flats_flat)
+apply (metis mkeps_flats)
+apply(simp add: POSIX_def)
+apply(auto)[1]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(auto)
+apply (metis ValOrd.intros(5))
+apply (smt ValOrd.intros(2) flats_flat)
+apply(simp add: POSIX_def)
+apply(auto)[1]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply (metis Prf_flat_L flats_flat mkeps_flats nullable_correctness)
+by (metis ValOrd.intros(4))
+
+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)"
+
+fun injval :: "rexp \<Rightarrow> char \<Rightarrow> val \<Rightarrow> val"
+where
+  "injval (CHAR d) c Void = Char d"
+| "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 (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)"
+
+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 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(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(erule Prf.cases)
+apply(simp_all)[5]
+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
+
+fun head where
+  "head [] = None"
+| "head (x#xs) = Some x"
+
+lemma head1:
+  assumes "head (xs @ ys) = Some x"
+  shows "(head xs = Some x) \<or> (xs = [] \<and> head ys = Some x)"
+using assms
+apply(induct xs)
+apply(auto)
+done
+
+lemma head2:
+  assumes "head (xs @ ys) = None"
+  shows "(head xs = None) \<and> (head ys = None)"
+using assms
+apply(induct xs)
+apply(auto)
+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)[5]
+apply(auto)[1]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(auto)[1]
+apply (metis mkeps_flat)
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+done
+
+
+lemma proj_inj_id:
+  assumes "\<turnstile> v : der c r" 
+  shows "projval r c (injval r c v) = v"
+using assms
+apply(induct r arbitrary: c v rule: rexp.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 = char")
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+defer
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(simp)
+apply(case_tac "nullable rexp1")
+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 list.distinct(1) v4)
+apply(auto)[1]
+apply (metis mkeps_flat)
+apply(auto)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(auto)[1]
+apply(simp add: v4)
+done
+
+lemma Le_2a: "(head (flat v) = None) = (flat v = [])"
+apply(induct v)
+apply(simp_all)
+apply (metis Nil_is_append_conv head.elims option.distinct(1))
+done
+
+lemma v5:
+  assumes "\<turnstile> v : der c r" "POSIX v (der c r)"
+  shows "POSIX (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(simp)
+apply(case_tac "c = c'")
+apply(auto simp add: POSIX_def)[1]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply (metis ValOrd.intros(7))
+apply(erule Prf.cases)
+apply(simp_all)[5]
+prefer 2
+apply(simp)
+apply(case_tac "nullable r1")
+apply(simp)
+defer
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(auto)[1]
+apply(drule POSIX_SEQ)
+apply(assumption)
+apply(assumption)
+apply(auto)[1]
+apply(rule POSIX_SEQ_I)
+apply metis
+apply(simp)
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(auto)[1]
+apply(drule POSIX_ALT)
+apply(rule POSIX_ALT_I1)
+apply metis
+defer
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(auto)
+apply(rotate_tac 5)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(auto)[1]
+apply(drule POSIX_ALT)
+apply(drule POSIX_SEQ)
+apply(simp)
+apply(simp)
+apply(rule POSIX_SEQ_I)
+apply metis
+apply(simp)
+apply(drule POSIX_ALT1a)
+apply(rule POSIX_SEQ_I)
+apply (metis mkeps_POSIX)
+apply(metis)
+apply(frule POSIX_ALT1a)
+apply(rotate_tac 1)
+apply(drule_tac x="v2" in meta_spec)
+apply(simp)
+apply(rule POSIX_ALT_I2)
+apply(simp)
+apply(frule POSIX_ALT1a)
+apply(auto)
+apply(subst v4)
+apply(simp)
+apply(simp)
+apply(case_tac "\<exists>r. v2 \<succ>r v'")
+apply (metis ValOrd_length le_neq_implies_less less_Suc_eq)
+apply(auto)[1]
+apply(frule_tac x="der c r2" in spec)
+apply(subgoal_tac "\<not>(Right v2 \<succ>(ALT (der c r1) (der c r2)) Right v')")
+prefer 2
+apply(rule notI)
+apply(erule ValOrd.cases)
+apply(simp_all)[7]
+apply(subst (asm) (1) POSIX_def)
+apply(simp)
+apply(subgoal_tac "(\<not> \<turnstile> Right v' : ALT (der c r1) (der c r2)) \<or> (flats v2 \<noteq> flats v')")
+prefer 2
+apply (metis flats.simps(4))
+apply(simp)
+apply(auto)[1]
+apply(subst v4)
+apply(simp)
+apply(simp)
+apply(case_tac "v2 \<succ>r1 v'")
+apply (metis ValOrd_length le_neq_implies_less less_Suc_eq)
+apply(
+
+apply(drule_tac x="projval (ALT r1 r2) c v'" in spec)
+apply(drule mp)
+apply(auto)
+apply(frule POSIX_ALT1b)
+apply(auto)
+apply(subst v4)
+apply(simp)
+apply(simp)
+apply(simp add: flats_flat)
+apply(rotate_tac 1)
+apply(drule_tac x="v2" in meta_spec)
+apply(simp)
+apply(rule POSIX_ALT_I2)
+apply(simp)
+apply(auto)[1]
+apply(subst v4)
+apply(simp)
+defer
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(auto)
+apply(rotate_tac 5)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(auto)[1]
+apply(drule POSIX_ALT)
+apply(drule POSIX_SEQ)
+apply(simp)
+apply(simp)
+apply(rule POSIX_SEQ_I)
+apply metis
+apply(simp)
+apply(drule POSIX_ALT1a)
+apply(rule POSIX_SEQ_I)
+apply (metis mkeps_POSIX)
+apply metis
+apply(drule_tac x="projval r1 c v'" in meta_spec)
+apply(drule meta_mp)
+defer
+apply(drule meta_mp)
+defer
+apply(subst (asm) (1) POSIX_def)
+apply(simp)
+
+
+
+lemma inj_proj_id:
+  assumes "\<turnstile> v : r" "POSIX v r" "head (flat v) = Some c"  
+  shows "injval r c (projval r c v) = v"
+using assms
+apply(induct v r arbitrary: rule: Prf.induct)
+apply(simp)
+apply(auto)[1]
+
+apply(simp)
+apply(frule POSIX_head)
+apply(assumption)
+apply(simp)
+apply(drule meta_mp)
+
+apply(frule POSIX_E1)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(frule POSIX_E1)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(frule POSIX_E1)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(frule POSIX_E1)
+defer
+apply(frule POSIX_E1)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(auto)[1]
+
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(simp)
+apply(case_tac "c = char")
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+
+
+lemma POSIX_head:
+  assumes "POSIX (Stars (v#vs)) (STAR r)" "head (flat v @ flat (Stars vs)) = Some c"
+  shows "head (flat v) = Some c"
+using assms
+apply(rule_tac ccontr)
+apply(frule POSIX_E1)
+apply(drule Le_1)
+apply(assumption)
+apply(auto)[1]
+apply(auto simp add: POSIX_def)
+apply(drule_tac x="Stars (v'#vs')" in spec)
+apply(simp)
+apply(simp add: ValOrd_eq_def)
+apply(auto)
+apply(erule ValOrd.cases)
+apply(simp_all)
+apply(auto)
+using Le_2
+
+by (metis Le_2 Le_2a head1)
+
+
+lemma inj_proj_id:
+  assumes "\<turnstile> v : r" "POSIX v r" "head (flat v) = Some c"  
+  shows "injval r c (projval r c v) = v"
+using assms
+apply(induct r arbitrary: rule: Prf.induct)
+apply(simp)
+apply(simp)
+apply(frule POSIX_head)
+apply(assumption)
+apply(simp)
+apply(drule meta_mp)
+
+apply(frule POSIX_E1)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(frule POSIX_E1)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(frule POSIX_E1)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(frule POSIX_E1)
+defer
+apply(frule POSIX_E1)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(auto)[1]
+
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(simp)
+apply(case_tac "c = char")
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+defer
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(auto)[1]
+apply(rotate_tac 2)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(case_tac "nullable rexp1")
+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(simp add: v4)
+apply(auto)[1]
+apply(simp add: v2a)
+apply(simp only: der.simps)
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(auto)[1]
+apply(simp add: v4)
+done
+
+
+
+lemma STAR_obtain:
+  assumes "\<turnstile> v : STAR r"
+  obtains vs where "\<turnstile> Stars vs : STAR r" and "v = Stars vs"
+using assms
+by (smt Prf.cases rexp.distinct(17) rexp.distinct(23) rexp.distinct(27) rexp.distinct(29))
+
+fun first :: "val \<Rightarrow> char option"
+where
+  "first Void = None"
+| "first (Char c) = Some c"
+| "first (Seq v1 v2) = (if (\<exists>c. first v1 = Some c) then first v1 else first v2)"
+| "first (Right v) = first v"
+| "first (Left v) = first v"
+| "first (Stars []) = None"
+| "first (Stars (v#vs)) =  (if (\<exists>c. first v = Some c) then first v else first (Stars vs))"   
+
+lemma flat: 
+  shows "flat v = [] \<longleftrightarrow> first v = None"
+  and "flat (Stars vs) = [] \<longleftrightarrow> first (Stars vs) = None"
+apply(induct v and vs)
+apply(auto)
+done
+
+lemma first: 
+  shows "first v = Some c \<Longrightarrow> head (flat v @ ys) = Some c"
+apply(induct arbitrary: ys rule: first.induct)
+apply(auto split: if_splits simp add: flat[symmetric])
+done
+
+
+
+lemma v5:
+  assumes "POSIX v r" "head (flat v) = Some c" 
+  shows "\<turnstile> projval r c v : der c r"
+using assms
+apply(induct r arbitrary: c v rule: rexp.induct)
+prefer 6
+apply(frule POSIX_E1)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(rule Prf.intros)
+apply(drule_tac x="c" in meta_spec)
+apply(drule_tac x="va" in meta_spec)
+apply(drule meta_mp)
+apply(simp add: POSIX_def)
+apply(auto)[1]
+apply(drule_tac x="Stars (v'#vs)" in spec)
+apply(simp)
+apply(drule mp)
+apply (metis Prf.intros(2))
+apply(simp add: ValOrd_eq_def)
+apply(erule disjE)
+apply(simp)
+apply(erule ValOrd.cases)
+apply(simp_all)[10]
+apply(drule_tac meta_mp)
+apply(drule head1)
+apply(auto)[1]
+apply(simp add: POSIX_def)
+apply(auto)[1]
+apply(drule_tac x="Stars (va#vs)" in spec)
+apply(simp)
+prefer 6
+apply(simp)
+apply(auto split: if_splits)[1]
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(rule Prf.intros)
+apply metis
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(auto split: if_splits)[1]
+apply(rule Prf.intros)
+apply(auto split: if_splits)[1]
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(auto)
+apply(case_tac "char = c")
+apply(simp)
+apply(rule Prf.intros)
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[
+
+
+lemma uu:
+  assumes ih: "\<And>v c. \<lbrakk>head (flat v) = Some c\<rbrakk> \<Longrightarrow> \<turnstile> projval rexp c v : der c rexp"
+  assumes "\<turnstile> Stars vs : STAR rexp"
+  and "first (Stars (v#vs)) = Some c"
+  shows "\<turnstile> projval rexp c v : der c rexp"
+using assms(2,3)
+apply(induct vs)
+apply(simp_all)
+apply(auto split: if_splits)
+apply (metis first head1 ih)
+apply (metis first head1 ih)
+
+apply(auto)
+
+lemma v5:
+  assumes "\<turnstile> v : r" "head (flat v) = Some c" 
+  shows "\<turnstile> projval r c v : der c r"
+using assms
+apply(induct r arbitrary: v c rule: rexp.induct)
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(case_tac "char = c")
+apply(simp)
+apply(rule Prf.intros)
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+prefer 3
+proof -
+  fix rexp v c vs
+  assume ih: "\<And>v c. \<lbrakk>\<turnstile> v : rexp; head (flat v) = Some c\<rbrakk> \<Longrightarrow> \<turnstile> projval rexp c v : der c rexp"
+  assume a: "head (flat (Stars vs)) = Some c"
+  assume b: "\<turnstile> Stars vs : STAR rexp"
+  have c: "first (Stars vs) = Some c \<Longrightarrow> \<turnstile> (hd vs) : rexp \<Longrightarrow> \<turnstile> projval rexp c (hd vs) : der c rexp"
+    using b
+    apply(induct arbitrary: rule: Prf.induct) 
+    apply(simp_all)
+    apply(case_tac "\<exists>c. first v = Some c")
+    apply(auto)[1]
+    apply(rule ih)
+    apply(simp)
+    apply (metis append_Nil2 first)
+    apply(auto)[1]
+    apply(simp)
+    apply(auto split: if_splits)[1]
+apply (metis append_Nil2 first ih)
+    apply(drule_tac x="v" in meta_spec)
+    apply(simp)
+    apply(rotate_tac 1)
+    apply(erule Prf.cases)
+    apply(simp_all)[7]
+    apply(drule_tac x="v" in meta_spec)
+    apply(simp)
+    using a
+    apply(rotate_tac 1)
+    apply(erule Prf.cases)
+    apply(simp_all)[7]
+
+
+apply (metis (full_types) Prf.cases Prf.simps a b flat.simps(6) head.simps(1) list.distinct(1) list.inject option.distinct(1) rexp.distinct(17) rexp.distinct(23) rexp.distinct(27) rexp.distinct(29) val.distinct(17) val.distinct(27) val.distinct(29) val.inject(5))
+    
+    apply(auto)[1]
+    apply(case_tac "\<exists>c. first a = Some c")
+    apply(auto)[1]
+    apply(rule ih)
+    apply(simp)
+apply (metis append_Nil2 first ih)
+    apply(auto)[1]
+    apply(case_tac "\<exists>c. first a = Some c")
+    apply(auto)[1]
+    apply(rule ih)
+    apply(simp)
+    apply(auto)[1]
+    
+    apply(erule Prf.cases)
+    apply(simp_all)[7]
+apply (metis append_Nil2 first)
+    apply(simp)
+    apply(simp add: )
+    apply(simp add: flat)
+    apply(erule Prf.cases)
+    apply(simp_all)[7]
+    apply(rule Prf.intros)
+      *)
+  show "\<turnstile> projval (STAR rexp) c (Stars vs) : SEQ (der c rexp) (STAR rexp)"
+    using b a
+    apply -
+    apply(erule Prf.cases)
+    apply(simp_all)[7]
+    apply(drule head1)
+    apply(auto)
+    apply(rule Prf.intros)
+    apply(rule ih)
+    apply(simp_all)[3]
+    using k
+    apply -
+    apply(rule Prf.intros)
+    apply(auto)
+
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(rule Prf.intros)
+defer
+apply(rotate_tac 1)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(drule_tac meta_mp)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(rule ih)
+apply(case_tac vs)
+apply(simp)
+apply(simp)
+apply(rotate_tac 3)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(auto)[1]
+apply (metis Prf.intros(1) Prf.intros(3))
+apply(simp)
+
+apply(drule head1)
+apply(auto)[1]
+apply (metis Prf.intros(3))
+
+
+apply (metis Prf.intros)
+apply(case_tac "nullable r1")
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(auto)[1]
+apply (metis Prf.intros(5))
+apply (metis Prf.intros(3) Prf.intros(4) head1)
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(auto)[1]
+apply (metis nullable_correctness v1)
+apply(drule head1)
+apply(auto)[1]
+apply (metis Prf.intros(3))
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(auto)[1]
+apply(drule head1)
+apply(auto)[1]
+apply(rule Prf.intros)
+apply(auto)
+apply(rule Prf.intros)
+apply(auto)
+apply(rotate_tac 2)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(auto)
+apply(drule head1)
+apply(auto)
+apply(rule Prf.intros)
+apply(auto)
+apply(rule Prf.intros)
+apply(auto)
+
+defer
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(auto)[1]
+apply(rule Prf.intros)
+apply(auto)
+apply(drule head1)
+apply(auto)[1]
+defer
+apply(rotate_tac 3)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(auto)
+apply(drule head1)
+apply(auto)[1]
+
+apply(simp)
+apply(rule Prf.intros)
+apply(auto)
+apply(drule_tac x="v" in meta_spec)
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(auto)[1]
+apply(drule head1)
+apply(auto)[1]
+apply(rule Prf.intros)
+apply(auto)
+apply(drule meta_mp)
+apply(rule Prf.intros)
+apply(auto)
+
+apply(simp)
+apply (metis Prf.intros(3) head1)
+
+defer
+apply(simp)
+apply(drule_tac head1)
+apply(auto)[1]
+apply(rule Prf.intros)
+apply(rule Prf.intros)
+apply(simp)
+apply(simp)
+apply(rule Prf.intros)
+apply(simp)
+apply(simp)
+apply(rule Prf.intros)
+apply(simp)
+apply (metis nullable_correctness v1)
+apply(simp)
+apply(rule Prf.intros)
+apply(simp)
+apply(simp)
+apply(rule Prf.intros)
+apply(simp)
+apply(simp)
+apply(simp)
+apply(rule Prf.intros)
+apply(drule_tac head1)
+apply(auto)[1]
+apply (metis Prf.intros(3))
+apply(rotate_tac 2)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(auto)[1]
+apply(rule Prf.intros)
+defer
+apply(drule_tac x="c" in meta_spec)
+apply(simp)
+apply(rotate_tac 6)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(auto)[1]
+apply(rule Prf.intros)
+apply(auto)[2]
+apply(drule v1)
+apply(simp)
+apply(rule Prf.intros)
+apply(simp add: nullable_correctness[symmetric])
+apply(rotate_tac 1)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(auto)[1]
+apply(drule head1)
+apply(auto)[1]
+apply(rule Prf.intros)
+apply(simp)
+apply(simp)
+apply(simp)
+
+lemma inj_proj_id:
+  assumes "\<turnstile> v : r" "head (flat v) = Some c" 
+  shows "injval r c (projval r c v) = v"
+using assms
+apply(induct arbitrary: c rule: Prf.induct)
+apply(simp)
+apply(simp)
+apply(drule head1)
+apply(auto)[1]
+apply(rotate_tac 2)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(auto)[1]
+apply(drule head1)
+apply(auto)[1]
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(simp)
+apply(case_tac "ca = c'")
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+defer
+apply(simp)
+apply(case_tac "nullable r1")
+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(rotate_tac 2)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(simp)
+apply(case_tac "nullable rexp1")
+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(simp add: v4)
+apply(auto)[1]
+apply(simp add: v2a)
+apply(simp only: der.simps)
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(auto)[1]
+apply(simp add: v4)
+done
+
+
+
+lemma POSIX_I:
+  assumes "\<turnstile> v : r" "\<And>v'.  \<turnstile> v' : r \<Longrightarrow> flat v = flat v' \<Longrightarrow> v \<succeq>r v'"
+  shows "POSIX v r"
+using assms
+unfolding POSIX_def
+apply(auto)
+done
+
+lemma DISJ:
+  "(\<not> A \<Longrightarrow> B) \<Longrightarrow> A \<or> B"
+by metis
+
+lemma DISJ2:
+  "\<not>(A \<and> B) \<longleftrightarrow> \<not>A \<or> \<not>B"
+by metis
+ 
+lemma APP: "xs @ [] = xs" by simp
+
+lemma v5:
+  assumes "POSIX v (der c r)"
+  shows "POSIX (injval r c v) r"
+using assms
+apply(induct arbitrary: v rule: der.induct)
+apply(simp)
+apply(auto simp add: POSIX_def)[1]
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(auto simp add: POSIX_def)[1]
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(case_tac "c = c'")
+apply(auto simp add: POSIX_def)[1]
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(rule Prf.intros)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(simp add: ValOrd_eq_def)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(simp)
+apply(auto simp add: POSIX_def)[1]
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(erule Prf.cases)
+apply(simp_all)[7]
+prefer 3
+apply(simp)
+apply(frule POSIX_E1)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(auto)[1]
+apply(drule_tac x="v1" in meta_spec)
+apply(drule meta_mp)
+apply(rule POSIX_I)
+apply(simp)
+apply(simp add: POSIX_def)
+apply(auto)[1]
+apply(drule_tac x="Seq v' v2" in spec)
+apply(simp)
+apply(drule mp)
+apply (metis Prf.intros(3))
+apply(simp add: ValOrd_eq_def)
+apply(erule disjE)
+apply(simp)
+apply(erule ValOrd.cases)
+apply(simp_all)[10]
+apply(subgoal_tac "\<exists>vs2. v2 = Stars vs2")
+prefer 2
+apply(rotate_tac 2)
+apply(erule Prf.cases)
+apply(auto)[7]
+apply(erule exE)
+apply(clarify)
+apply(simp only: injval.simps)
+apply(case_tac "POSIX (Stars (injval r c v1 # vs2)) (STAR r)")
+apply(simp)
+apply(subgoal_tac "\<exists>v'' vs''. Stars (v''#vs'')  \<succ>(STAR r) Stars (injval r c v1 # vs2)")
+apply(erule exE)+
+apply(erule ValOrd.cases)
+apply(simp_all)[8]
+apply(auto)[1]
+apply(subst (asm) (2) POSIX_def)
+
+
+prefer 2
+apply(subst (asm) (3) POSIX_def)
+apply(simp)
+apply(drule mp)
+apply (metis Prf.intros(2) v3)
+apply(erule exE)
+apply(auto)[1]
+
+apply
+apply(subgoal_tac "\<turnstile> Stars (injval r c v1 # vs2) : STAR r")
+apply(simp)
+apply(case_tac "flat () = []")
+
+apply(rule POSIX_I)
+apply (metis POSIX_E1 der.simps(6) v3)
+apply(rotate_tac 2)
+apply(erule Prf.cases)
+defer
+defer
+apply(simp_all)[5]
+prefer 4
+apply(clarify)
+apply(simp only: v4 flat.simps injval.simps)
+prefer 4
+apply(clarify)
+apply(simp only: v4 APP flat.simps injval.simps)
+prefer 2
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(clarify)
+
+
+apply(simp add: ValOrd_eq_def)
+apply(subst (asm) POSIX_def)
+apply(erule conjE)
+apply(drule_tac x="va" in spec)
+apply(simp)
+apply(simp add: v4)
+apply(simp add: ValOrd_eq_def)
+apply(simp)
+apply(rule disjI2)
+apply(rule ValOrd.intros)
+apply(rotate_tac 2)
+apply(subst (asm) POSIX_def)
+apply(simp)
+apply(auto)[1]
+apply(drule_tac x="v" in spec)
+apply(simp)
+apply(drule mp)
+prefer 2
+apply(simp add: ValOrd_eq_def)
+apply(auto)[1]
+
+apply(case_tac "injval rb c v1 = v \<and> [] = vs")
+apply(simp)
+apply(simp only: DISJ2)
+apply(rule disjI2)
+apply(erule disjE)
+
+
+apply(auto)[1]
+apply (metis list.distinct(1) v4)
+apply(auto)[1]
+apply(simp add: ValOrd_eq_def)
+apply(rule DISJ)
+apply(simp only: DISJ2)
+apply(erule disjE)
+apply(rule ValOrd.intros)
+apply(subst (asm) POSIX_def)
+apply(auto)[1]
+
+apply (metis list.distinct(1) v4)
+apply(subst (asm) POSIX_def)
+apply(auto)[1]
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(rotate_tac 3)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(auto)[1]
+apply (metis list.distinct(1) v4)
+apply (metis list.distinct(1) v4)
+apply(clarify)
+apply(rotate_tac 3)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+prefer 2
+apply(clarify)
+apply(simp add: ValOrd_eq_def)
+apply(drule_tac x="Stars (v#vs)" in spec)
+apply(drule mp)
+apply(auto)[1]
+
+apply(simp add: ValOrd_eq_def)
+
+apply (metis POSIX_E1 der.simps(6) list.distinct(1) v4)
+apply(rotate_tac 3)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+
+apply(simp)
+apply(case_tac v2)
+apply(simp)
+apply(simp (no_asm) POSIX_def)
+apply(auto)[1]
+apply(auto)[1]
+ 
+
+apply (metis POSIX_E der.simps(6) v3)
+
+apply(rule Prf.intros)
+apply(drule_tac x="v1" in meta_spec)
+apply(drule meta_mp)
+prefer 2
+
+apply(subgoal_tac "POSIX v1 (der c r)")
+prefer 2
+apply(simp add: POSIX_def)
+apply(auto)[1]
+apply(simp add: ValOrd_eq_def)
+apply(auto)[1]
+
+
+lemma v5:
+  assumes "\<turnstile> v : der c r" "POSIX v (der c r)"
+  shows "POSIX (injval r c v) r"
+using assms
+apply(induct arbitrary: v rule: der.induct)
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(simp)
+apply(case_tac "c = c'")
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(simp add: POSIX_def)
+apply(auto)[1]
+apply(rule Prf.intros)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(simp add: ValOrd_eq_def)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+prefer 3
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(auto)[1]
+apply(case_tac "flat (Seq v1 v2) \<noteq> []")
+apply(subgoal_tac "POSIX v1 (der c r)")
+prefer 2
+apply(simp add: POSIX_def)
+apply(auto)[1]
+
+
+apply(drule_tac x="v1" in meta_spec)
+apply(simp)
+apply(simp (no_asm) add: POSIX_def)
+apply(auto)[1]
+apply(rule v3)
+apply (metis Prf.intros(3) der.simps(6))
+apply(rotate_tac 1)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(simp add: ValOrd_eq_def)
+apply(rule disjI2)
+apply(rotate_tac 1)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(rule ValOrd.intros)
+apply(simp)
+apply (metis list.distinct(1) v4)
+apply(rule ValOrd.intros)
+apply(simp add: POSIX_def)
+apply(auto)[1]
+apply(rotate_tac 3)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(simp add: ValOrd_eq_def)
+apply(drule_tac x="v" in spec)
+apply(simp)
+apply(auto)[1]
+apply(simp)
+
+apply(simp add: POSIX_def)
+apply(auto)[1]
+apply(
+
+apply(rotate_tac 1)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply (metis list.distinct(1) v4)
+apply(rotate_tac 8)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply (metis POSIX_def ValOrd.intros(9) ValOrd_eq_def)
+apply(simp add: ValOrd_eq_def)
+apply(simp)
+
+apply(simp add: ValOrd_eq_def)
+apply(simp add: POSIX_def)
+apply(auto)[1]
+
+
+apply(simp)
+apply(simp add: ValOrd_eq_def)
+apply(simp add: POSIX_def)
+apply(erule conjE)+
+apply(drule_tac x="Seq v1 v2" in spec)
+apply(simp)
+
+
+
+apply(rotate_tac 2)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(auto)[1]
+apply(simp add: POSIX_def)
+apply(auto)[1]
+apply(rule Prf.intros)
+apply(rule v3)
+apply(simp)
+apply(rotate_tac 5)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(auto)[1]
+apply(rotate_tac 4)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(auto)[1]
+apply(simp add: ValOrd_eq_def)
+
+apply(simp)
+
+
+prefer 2
+apply(auto)[1]
+apply(subgoal_tac "POSIX v2 (der c r2)")
+apply(rotate_tac 1)
+apply(drule_tac x="v2" in meta_spec)
+apply(simp)
+apply(subgoal_tac "\<turnstile> Right (injval r2 c v2) : (ALT r1 r2)") 
+prefer 2
+apply (metis Prf.intros(5) v3)
+apply(simp (no_asm) add: POSIX_def)
+apply(auto)[1]
+apply(rotate_tac 6)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+prefer 2
+apply(auto)[1]
+apply(simp add: ValOrd_eq_def)
+apply (metis POSIX_def ValOrd.intros(5) ValOrd_eq_def)
+apply(auto)[1]
+apply(simp add: ValOrd_eq_def)
+
+
+section {* Correctness Proof of the Matcher *}
+
+
+section {* Left-Quotient of a Set *}
+
+fun
+ zeroable :: "rexp \<Rightarrow> bool"
+where
+  "zeroable (NULL) = True"
+| "zeroable (EMPTY) = False"
+| "zeroable (CHAR c) = False"
+| "zeroable (ALT r1 r2) = (zeroable r1 \<and> zeroable r2)"
+| "zeroable (SEQ r1 r2) = (zeroable r1 \<or> zeroable r2)"
+| "zeroable (STAR r) = False"
+
+
+lemma zeroable_correctness:
+  shows "zeroable r  \<longleftrightarrow>  (L r = {})"
+apply(induct r)
+apply(auto simp add: Seq_def)[6]
+done
+
+section {* Left-Quotient of a Set *}
+
+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 Seq_def
+by (auto simp add: Cons_eq_append_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 Seq_def Der_def
+    by (auto dest: star_decomp)
+  finally show "Der c (A\<star>) = (Der c A) ;; A\<star>" .
+qed
+
+
+lemma der_correctness:
+  shows "L (der c r) = Der c (L r)"
+by (induct r) 
+   (simp_all add: nullable_correctness)
+
+lemma matcher_correctness:
+  shows "matcher r s \<longleftrightarrow> s \<in> L r"
+by (induct s arbitrary: r)
+   (simp_all add: nullable_correctness der_correctness Der_def)
+
+section {* Examples *}
+
+definition 
+  "CHRA \<equiv> CHAR (CHR ''a'')"
+
+definition 
+  "ALT1 \<equiv> ALT CHRA EMPTY"
+
+definition 
+  "SEQ3 \<equiv> SEQ (SEQ ALT1 ALT1) ALT1"
+
+value "matcher SEQ3 ''aaa''"
+
+value "matcher NULL []"
+value "matcher (CHAR (CHR ''a'')) [CHR ''a'']"
+value "matcher (CHAR a) [a,a]"
+value "matcher (STAR (CHAR a)) []"
+value "matcher (STAR (CHAR a))  [a,a]"
+value "matcher (SEQ (CHAR (CHR ''a'')) (SEQ (STAR (CHAR (CHR ''b''))) (CHAR (CHR ''c'')))) ''abbbbc''"
+value "matcher (SEQ (CHAR (CHR ''a'')) (SEQ (STAR (CHAR (CHR ''b''))) (CHAR (CHR ''c'')))) ''abbcbbc''"
+
+section {* Incorrect Matcher - fun-definition rejected *}
+
+fun
+  match :: "rexp list \<Rightarrow> string \<Rightarrow> bool"
+where
+  "match [] [] = True"
+| "match [] (c # s) = False"
+| "match (NULL # rs) s = False"  
+| "match (EMPTY # rs) s = match rs s"
+| "match (CHAR c # rs) [] = False"
+| "match (CHAR c # rs) (d # s) = (if c = d then match rs s else False)"         
+| "match (ALT r1 r2 # rs) s = (match (r1 # rs) s \<or> match (r2 # rs) s)" 
+| "match (SEQ r1 r2 # rs) s = match (r1 # r2 # rs) s"
+| "match (STAR r # rs) s = (match rs s \<or> match (r # (STAR r) # rs) s)"
+
+
+end    
\ No newline at end of file