# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1423483990 0
# Node ID a6bb0152ccc2470b8ee881906a9ffe9872d146f2
# Parent  2cdbab0378617cadadeec9a564ce789335d4439f
updated some rules

diff -r 2cdbab037861 -r a6bb0152ccc2 progs/scala/re.scala
--- a/progs/scala/re.scala	Sat Jan 31 18:21:03 2015 +0000
+++ b/progs/scala/re.scala	Mon Feb 09 12:13:10 2015 +0000
@@ -43,6 +43,27 @@
   def $ (r: Rexp) = RECD(s, r)
 }
 
+def pretty(r: Rexp) : String = r match {
+  case NULL => "0"
+  case EMPTY => "e"
+  case CHAR(c) => c.toString 
+  case ALT(r1, r2) => "(" ++ pretty(r1) ++ " | " + pretty(r2) ++ ")"
+  case SEQ(r1, r2) => pretty(r1) ++ pretty(r2)
+  case STAR(r) => "(" ++ pretty(r) ++ ")*"
+  case RECD(x, r) => "(" ++ x ++ " : " ++ pretty(r) ++ ")"
+}
+
+def vpretty(v: Val) : String = v match {
+  case Void => "()"
+  case Chr(c) => c.toString
+  case Left(v) => "Left(" ++ vpretty(v) ++ ")"
+  case Right(v) => "Right(" ++ vpretty(v) ++ ")"
+  case Sequ(v1, v2) => vpretty(v1) ++ " ~ " ++ vpretty(v2)
+  case Stars(vs) => vs.flatMap(vpretty).mkString("[", ",", "]")
+  case Rec(x, v) => "(" ++ x ++ ":" ++ vpretty(v) ++ ")"
+}
+
+
 // size of a regular expressions - for testing purposes 
 def size(r: Rexp) : Int = r match {
   case NULL => 1
@@ -59,7 +80,8 @@
   case NULL => Set()
   case EMPTY => Set(Void)
   case CHAR(c) => Set(Chr(c))
-  case ALT(r1, r2) => values(r1) ++ values(r2)
+  case ALT(r1, r2) => (for (v1 <- values(r1)) yield Left(v1)) ++ 
+                      (for (v2 <- values(r2)) yield Right(v2))
   case SEQ(r1, r2) => for (v1 <- values(r1); v2 <- values(r2)) yield Sequ(v1, v2)
   case STAR(r) => Set(Void) ++ values(r)   // to do more would cause the set to be infinite
   case RECD(_, r) => values(r)
@@ -271,6 +293,18 @@
 println(values(r2).mkString("\n"))
 println(values(r2).toList.map(flatten).mkString("\n"))
 
+//Some experiments
+//================
+
+val reg0 = ("" | "a") ~ ("ab" | "b")
+val reg1 = der('a', reg0)
+val reg2 = der('b', reg1)
+println(List(reg0, reg1, reg2).map(pretty).mkString("\n"))
+println(lexing(reg0, "ab"))
+
+val val0 = values(reg0)
+val val1 = values(reg1)
+val val2 = values(reg2)
 
 
 // Two Simple Tests
diff -r 2cdbab037861 -r a6bb0152ccc2 thys/Re1.thy
--- a/thys/Re1.thy	Sat Jan 31 18:21:03 2015 +0000
+++ b/thys/Re1.thy	Mon Feb 09 12:13:10 2015 +0000
@@ -42,6 +42,20 @@
 | "L (SEQ r1 r2) = (L r1) ;; (L r2)"
 | "L (ALT r1 r2) = (L r1) \<union> (L r2)"
 
+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
 
 section {* Values *}
 
@@ -52,16 +66,6 @@
 | Right val
 | Left val
 
-section {* Relation between values and regular expressions *}
-
-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"
-
 section {* The string behind a value *}
 
 fun flat :: "val \<Rightarrow> string"
@@ -80,6 +84,44 @@
 | "flats(Right v) = flats(v)"
 | "flats(Seq v1 v2) = (flats v1) @ (flats v2)"
 
+
+section {* Relation between values and regular expressions *}
+
+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 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
+
+text {*
+  The value mkeps returns is always the correct POSIX
+  value.
+*}
+
 lemma Prf_flat_L:
   assumes "\<turnstile> v : r" shows "flat v \<in> L r"
 using assms
@@ -108,8 +150,8 @@
 
 inductive ValOrd :: "val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<succ>_ _" [100, 100, 100] 100)
 where
-  "\<lbrakk>v1 = v1'; v2 \<succ>r2 v2'\<rbrakk> \<Longrightarrow> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1' v2')" 
-| "v1  \<succ>r1 v1' \<Longrightarrow> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1' v2')" 
+  "v2 \<succ>r2 v2' \<Longrightarrow> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1 v2')" 
+| "\<lbrakk>v1 \<succ>r1 v1'; v1 \<noteq> v1'\<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')"
@@ -128,38 +170,32 @@
 apply(auto intro: ValOrd.intros)
 done
 
-lemma ValOrd_flats:
-  assumes "v1 \<succ>r v2"
-  shows "hd (flats v2) = hd (flats v1)"
-using assms
-apply(induct)
-apply(auto)
-oops
-
-
 section {* Posix definition *}
 
 definition POSIX :: "val \<Rightarrow> rexp \<Rightarrow> bool" 
 where
-  "POSIX v r \<equiv> (\<forall>v'. (\<turnstile> v' : r \<and> flat v = flat v') \<longrightarrow> v \<succ>r v')"
+  "POSIX v r \<equiv> (\<turnstile> v : r \<and> (\<forall>v'. (\<turnstile> v' : r \<and> flat v = flat v') \<longrightarrow> v \<succ>r v'))"
 
 (*
 an alternative definition: might cause problems
 with theorem mkeps_POSIX
 *)
 
+(*
 definition POSIX2 :: "val \<Rightarrow> rexp \<Rightarrow> bool" 
 where
   "POSIX2 v r \<equiv> \<turnstile> v : r \<and> (\<forall>v'. \<turnstile> v' : r \<longrightarrow> v \<succ>r v')"
+*)
 
+(*
 definition POSIX3 :: "val \<Rightarrow> rexp \<Rightarrow> bool" 
 where
   "POSIX3 v r \<equiv> \<turnstile> v : r \<and> (\<forall>v'. (\<turnstile> v' : r \<and> length (flat v') \<le> length(flat v)) \<longrightarrow> v \<succ>r v')"
-
+*)
 
-lemma POSIX_SEQ:
+lemma POSIX_SEQ1:
   assumes "POSIX (Seq v1 v2) (SEQ r1 r2)" "\<turnstile> v1 : r1" "\<turnstile> v2 : r2"
-  shows "POSIX v1 r1 \<and> POSIX v2 r2"
+  shows "POSIX v1 r1"
 using assms
 unfolding POSIX_def
 apply(auto)
@@ -172,7 +208,14 @@
 apply(erule ValOrd.cases)
 apply(simp_all)
 apply(clarify)
-defer
+by (metis ValOrd_refl)
+
+lemma POSIX_SEQ2:
+  assumes "POSIX (Seq v1 v2) (SEQ r1 r2)" "\<turnstile> v1 : r1" "\<turnstile> v2 : r2" 
+  shows "POSIX v2 r2"
+using assms
+unfolding POSIX_def
+apply(auto)
 apply(drule_tac x="Seq v1 v'" in spec)
 apply(simp)
 apply(erule impE)
@@ -181,38 +224,7 @@
 apply(simp)
 apply(erule ValOrd.cases)
 apply(simp_all)
-apply(clarify)
-oops (*not true*)
-
-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 2)
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(auto)[1]
-apply(rule ValOrd.intros)
-oops (* maybe also not true *)
-
-lemma POSIX3_SEQ_I:
-  assumes "POSIX3 v1 r1" "POSIX3 v2 r2" 
-  shows "POSIX3 (Seq v1 v2) (SEQ r1 r2)" 
-using assms
-unfolding POSIX3_def
-apply(auto)
-apply (metis Prf.intros(1))
-apply(rotate_tac 4)
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(auto)[1]
-apply(case_tac "v1 = v1a")
-apply(auto)
-apply (metis ValOrd.intros(1))
-apply (rule ValOrd.intros(2))
-oops
+done
 
 lemma POSIX_ALT2:
   assumes "POSIX (Left v1) (ALT r1 r2)"
@@ -220,6 +232,8 @@
 using assms
 unfolding POSIX_def
 apply(auto)
+apply(erule Prf.cases)
+apply(simp_all)[5]
 apply(drule_tac x="Left v'" in spec)
 apply(simp)
 apply(drule mp)
@@ -229,52 +243,14 @@
 apply(simp_all)
 done
 
-lemma POSIX2_ALT:
-  assumes "POSIX2 (Left v1) (ALT r1 r2)"
-  shows "POSIX2 v1 r1"
-using assms
-unfolding POSIX2_def
-apply(auto)
-oops
-
-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)
-done
-
-lemma POSIX2_ALT:
-  assumes "POSIX2 (Left v1) (ALT r1 r2)"
-  shows "POSIX2 v1 r1"
-using assms
-apply(simp add: POSIX2_def)
-apply(auto)
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(drule_tac x="Left v'" in spec)
-apply(drule mp)
-apply(rule Prf.intros)
-apply(auto)
-apply(erule ValOrd.cases)
-apply(simp_all)
-done
-
-
 lemma POSIX_ALT1a:
   assumes "POSIX (Right v2) (ALT r1 r2)"
   shows "POSIX v2 r2"
 using assms
 unfolding POSIX_def
 apply(auto)
+apply(erule Prf.cases)
+apply(simp_all)[5]
 apply(drule_tac x="Right v'" in spec)
 apply(simp)
 apply(drule mp)
@@ -284,23 +260,6 @@
 apply(simp_all)
 done
 
-lemma POSIX2_ALT1a:
-  assumes "POSIX2 (Right v2) (ALT r1 r2)"
-  shows "POSIX2 v2 r2"
-using assms
-unfolding POSIX2_def
-apply(auto)
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(drule_tac x="Right v'" in spec)
-apply(drule mp)
-apply(rule Prf.intros)
-apply(auto)
-apply(erule ValOrd.cases)
-apply(simp_all)
-done
-
-
 lemma POSIX_ALT1b:
   assumes "POSIX (Right v2) (ALT r1 r2)"
   shows "(\<forall>v'. (\<turnstile> v' : r2 \<and> flat v' = flat v2) \<longrightarrow> v2 \<succ>r2 v')"
@@ -316,7 +275,8 @@
 using assms
 unfolding POSIX_def
 apply(auto)
-apply(rotate_tac 3)
+apply (metis Prf.intros(2))
+apply(rotate_tac 2)
 apply(erule Prf.cases)
 apply(simp_all)[5]
 apply(auto)
@@ -325,22 +285,6 @@
 apply(rule ValOrd.intros)
 by simp
 
-lemma POSIX2_ALT_I1:
-  assumes "POSIX2 v1 r1" 
-  shows "POSIX2 (Left v1) (ALT r1 r2)"
-using assms
-unfolding POSIX2_def
-apply(auto)
-apply(rule Prf.intros)
-apply(simp)
-apply(rotate_tac 2)
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(auto)
-apply(rule ValOrd.intros)
-apply(auto)
-apply(rule ValOrd.intros)
-oops
 
 lemma POSIX_ALT_I2:
   assumes "POSIX v2 r2" "\<forall>v'. \<turnstile> v' : r1 \<longrightarrow> length (flat v2) > length (flat v')"
@@ -348,6 +292,7 @@
 using assms
 unfolding POSIX_def
 apply(auto)
+apply (metis Prf.intros)
 apply(rotate_tac 3)
 apply(erule Prf.cases)
 apply(simp_all)[5]
@@ -356,108 +301,6 @@
 apply metis
 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
-
-text {*
-  The value mkeps returns is always the correct POSIX
-  value.
-*}
-
-lemma mkeps_POSIX2:
-  assumes "nullable r"
-  shows "POSIX2 (mkeps r) r"
-using assms
-apply(induct r)
-apply(auto)[1]
-apply(simp add: POSIX2_def)
-oops
-
-lemma mkeps_POSIX3:
-  assumes "nullable r"
-  shows "POSIX3 (mkeps r) r"
-using assms
-apply(induct r)
-apply(auto)[1]
-apply(simp add: POSIX3_def)
-apply(auto)[1]
-apply (metis Prf.intros(4))
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply (metis ValOrd.intros)
-apply(simp add: POSIX3_def)
-apply(auto)[1]
-apply(simp add: POSIX3_def)
-apply(auto)[1]
-apply (metis mkeps.simps(2) mkeps_nullable nullable.simps(5))
-apply(rotate_tac 6)
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply (metis ValOrd.intros(2) add_leE gen_length_code(1) gen_length_def mkeps_flat)
-apply(auto)
-apply(simp add: POSIX3_def)
-apply(auto)
-apply (metis Prf.intros(2))
-apply(rotate_tac 4)
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply (metis ValOrd.intros(6))
-apply(auto)[1]
-apply (metis ValOrd.intros(3))
-apply(simp add: POSIX3_def)
-apply(auto)
-apply (metis Prf.intros(2))
-apply(rotate_tac 6)
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply (metis ValOrd.intros(6))
-apply (metis ValOrd.intros(3))
-apply(simp add: POSIX3_def)
-apply(auto)
-apply (metis Prf.intros(3))
-apply(rotate_tac 5)
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply (metis Prf_flat_L drop_0 drop_all list.size(3) mkeps_flat nullable_correctness)
-by (metis ValOrd.intros(5))
-
-
 lemma mkeps_POSIX:
   assumes "nullable r"
   shows "POSIX (mkeps r) r"
@@ -466,6 +309,7 @@
 apply(auto)[1]
 apply(simp add: POSIX_def)
 apply(auto)[1]
+apply (metis Prf.intros(4))
 apply(erule Prf.cases)
 apply(simp_all)[5]
 apply (metis ValOrd.intros)
@@ -473,70 +317,34 @@
 apply(auto)[1]
 apply(simp add: POSIX_def)
 apply(auto)[1]
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(auto)
-apply (simp add: ValOrd.intros(2) mkeps_flat)
-apply(simp add: POSIX_def)
-apply(auto)[1]
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(auto)
-apply (simp add: ValOrd.intros(6))
-apply (simp add: ValOrd.intros(3))
-apply(simp add: POSIX_def)
-apply(auto)[1]
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(auto)
-apply (simp add: ValOrd.intros(6))
-apply (simp add: ValOrd.intros(3))
-apply(simp add: POSIX_def)
-apply(auto)[1]
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(auto)
-apply (metis Prf_flat_L mkeps_flat nullable_correctness)
-by (simp add: ValOrd.intros(5))
-
-
-lemma mkeps_POSIX2:
-  assumes "nullable r"
-  shows "POSIX2 (mkeps r) r"
-using assms
-apply(induct r)
-apply(simp)
-apply(simp)
-apply(simp add: POSIX2_def)
-apply(rule conjI)
-apply(rule Prf.intros)
-apply(auto)[1]
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(rule ValOrd.intros)
-apply(simp)
-apply(simp)
-apply(simp add: POSIX2_def)
-apply(rule conjI)
-apply(rule Prf.intros)
-apply(simp add: mkeps_nullable)
-apply(simp add: mkeps_nullable)
-apply(auto)[1]
+apply (metis mkeps.simps(2) mkeps_nullable nullable.simps(5))
 apply(rotate_tac 6)
 apply(erule Prf.cases)
 apply(simp_all)[5]
-apply(rule ValOrd.intros(2))
+apply (simp add: mkeps_flat)
+apply(case_tac "mkeps r1a = v1")
 apply(simp)
-apply(simp only: nullable.simps)
+apply (metis ValOrd.intros(1))
+apply (rule ValOrd.intros(2))
+apply metis
+apply(simp)
+apply(simp)
 apply(erule disjE)
 apply(simp)
-thm POSIX2_ALT1a
-apply(rule POSIX2_ALT)
-apply(simp add: POSIX2_def)
-apply(rule conjI)
-apply(rule Prf.intros)
-apply(simp add: mkeps_nullable)
-oops
+apply (metis POSIX_ALT_I1)
+apply(auto)
+apply (metis POSIX_ALT_I1)
+apply(simp add: POSIX_def)
+apply(auto)[1]
+apply (metis Prf.intros(3))
+apply(rotate_tac 5)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(simp add: mkeps_flat)
+apply(auto)[1]
+apply (metis Prf_flat_L nullable_correctness)
+apply(rule ValOrd.intros)
+by metis
 
 
 section {* Derivatives *}
@@ -724,8 +532,21 @@
 lemma t: "(c#xs = c#ys) \<Longrightarrow> xs = ys"
 by (metis list.sel(3))
 
+lemma t2: "(xs = ys) \<Longrightarrow> (c#xs) = (c#ys)"
+by (metis)
+
+fun zeroable 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)"
+
+lemma "\<not>(nullable r) \<Longrightarrow> \<not>(\<exists>v. \<turnstile> v : r \<and> flat v = [])"
+by (metis Prf_flat_L nullable_correctness)
+
 lemma Prf_inj:
-  assumes "v1 \<succ>(der c r) v2" "\<turnstile> v1 : der c r" "\<turnstile> v2 : der c r"
+  assumes "v1 \<succ>(der c r) v2" "\<turnstile> v1 : der c r" "\<turnstile> v2 : der c r" (*"flat v1 = flat v2"*)
   shows "(injval r c v1) \<succ>r (injval r c v2)"
 using assms
 apply(induct arbitrary: v1 v2 rule: der.induct)
@@ -762,6 +583,594 @@
 apply(simp_all)[5]
 apply(simp)
 apply(rule ValOrd.intros)
+apply(clarify)
+apply(rotate_tac 3)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(clarify)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(clarify)
+apply(subst v4)
+apply(simp)
+apply(subst v4)
+apply(simp)
+apply(simp)
+apply(rule ValOrd.intros)
+apply(clarify)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(rule ValOrd.intros)
+apply(clarify)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+(* SEQ case*)
+apply(simp)
+apply(case_tac "nullable r1")
+apply(simp)
+defer
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(clarify)
+apply(erule ValOrd.cases)
+apply(simp_all)[8]
+apply(clarify)
+apply(rule ValOrd.intros)
+apply(simp)
+apply(clarify)
+apply(rule ValOrd.intros(2))
+apply metis
+
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(clarify)
+defer
+apply(erule ValOrd.cases)
+apply(simp_all del: injval.simps)[8]
+apply(simp)
+apply(clarify)
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(clarify)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(clarify)
+apply(rule ValOrd.intros(2))
+
+
+lemma POSIX_ex: "\<turnstile> v : r \<Longrightarrow> \<exists>v. POSIX v r"
+apply(induct r arbitrary: v)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(rule_tac x="Void" in exI)
+apply(simp add: POSIX_def)
+apply(auto)[1]
+apply (metis Prf.intros(4))
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply (metis ValOrd.intros(7))
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(rule_tac x="Char c" in exI)
+apply(simp add: POSIX_def)
+apply(auto)[1]
+apply (metis Prf.intros(5))
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply (metis ValOrd.intros(8))
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(auto)[1]
+apply(drule_tac x="v1" in meta_spec)
+apply(drule_tac x="v2" in meta_spec)
+apply(auto)[1]
+defer
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(auto)[1]
+apply (metis POSIX_ALT_I1)
+apply (metis POSIX_ALT_I1 POSIX_ALT_I2)
+apply(case_tac "nullable r1a")
+apply(rule_tac x="Seq (mkeps r1a) va" in exI)
+apply(auto simp add: POSIX_def)[1]
+apply (metis Prf.intros(1) mkeps_nullable)
+apply(simp add: mkeps_flat)
+apply(rotate_tac 7)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(case_tac "mkeps r1 = v1a")
+apply(simp)
+apply (rule ValOrd.intros(1))
+apply (metis append_Nil mkeps_flat)
+apply (rule ValOrd.intros(2))
+apply(drule mkeps_POSIX)
+apply(simp add: POSIX_def)
+
+apply metis
+apply(simp)
+apply(simp)
+apply(erule disjE)
+apply(simp)
+
+apply(drule_tac x="v2" in spec)
+
+lemma POSIX_ex2: "\<turnstile> v : r \<Longrightarrow> \<exists>v. POSIX v r \<and> \<turnstile> v : r"
+apply(induct r arbitrary: v)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(rule_tac x="Void" in exI)
+apply(simp add: POSIX_def)
+apply(auto)[1]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply (metis ValOrd.intros(7))
+apply (metis Prf.intros(4))
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(rule_tac x="Char c" in exI)
+apply(simp add: POSIX_def)
+apply(auto)[1]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply (metis ValOrd.intros(8))
+apply (metis Prf.intros(5))
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(auto)[1]
+apply(drule_tac x="v1" in meta_spec)
+apply(drule_tac x="v2" in meta_spec)
+apply(auto)[1]
+apply(simp add: POSIX_def)
+apply(auto)[1]
+apply(rule ccontr)
+apply(simp)
+apply(drule_tac x="Seq v va" in spec)
+apply(drule mp)
+defer
+apply (metis Prf.intros(1))
+
+
+oops
+
+lemma POSIX_ALT_cases:
+  assumes "\<turnstile> v : (ALT r1 r2)" "POSIX v (ALT r1 r2)"
+  shows "(\<exists>v1. v = Left v1 \<and> POSIX v1 r1) \<or> (\<exists>v2. v = Right v2 \<and> POSIX v2 r2)"
+using assms
+apply(erule_tac Prf.cases)
+apply(simp_all)
+unfolding POSIX_def
+apply(auto)
+apply (metis POSIX_ALT2 POSIX_def assms(2))
+by (metis POSIX_ALT1b assms(2))
+
+lemma POSIX_ALT_cases2:
+  assumes "POSIX v (ALT r1 r2)" "\<turnstile> v : (ALT r1 r2)" 
+  shows "(\<exists>v1. v = Left v1 \<and> POSIX v1 r1) \<or> (\<exists>v2. v = Right v2 \<and> POSIX v2 r2)"
+using assms POSIX_ALT_cases by auto
+
+lemma Prf_flat_empty:
+  assumes "\<turnstile> v : r" "flat v = []"
+  shows "nullable r"
+using assms
+apply(induct)
+apply(auto)
+done
+
+lemma POSIX_proj:
+  assumes "POSIX v r" "\<turnstile> v : r" "\<exists>s. flat v = c#s"
+  shows "POSIX (projval r c v) (der c r)"
+using assms
+apply(induct r c v arbitrary: rule: projval.induct)
+defer
+defer
+defer
+defer
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(simp add: POSIX_def)
+apply(auto)[1]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply (metis ValOrd.intros(7))
+apply(erule_tac [!] exE)
+prefer 3
+apply(frule POSIX_SEQ1)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(case_tac "flat v1 = []")
+apply(subgoal_tac "nullable r1")
+apply(simp)
+prefer 2
+apply(rule_tac v="v1" in Prf_flat_empty)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(simp)
+apply(frule POSIX_SEQ2)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(simp)
+apply(drule meta_mp)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(rule ccontr)
+apply(subgoal_tac "\<turnstile> val.Right (projval r2 c v2) : (ALT (SEQ (der c r1) r2) (der c r2))")
+apply(rotate_tac 11)
+apply(frule POSIX_ex)
+apply(erule exE)
+apply(drule POSIX_ALT_cases2)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(drule v3_proj)
+apply(simp)
+apply(simp)
+apply(drule POSIX_ex)
+apply(erule exE)
+apply(frule POSIX_ALT_cases2)
+apply(simp)
+apply(simp)
+apply(erule 
+prefer 2
+apply(case_tac "nullable r1")
+prefer 2
+apply(simp)
+apply(rotate_tac 1)
+apply(drule meta_mp)
+apply(rule POSIX_SEQ1)
+apply(assumption)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(rotate_tac 7)
+apply(drule meta_mp)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(rotate_tac 7)
+apply(drule meta_mp)
+apply (metis Cons_eq_append_conv)
+
+
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(simp add: POSIX_def)
+apply(simp)
+apply(simp)
+apply(simp_all)[5]
+apply(simp add: POSIX_def)
+
+
+lemma POSIX_proj:
+  assumes "POSIX v r" "\<turnstile> v : r" "\<exists>s. flat v = c#s"
+  shows "POSIX (projval r c v) (der c r)"
+using assms
+apply(induct r arbitrary: c v rule: rexp.induct)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(simp add: POSIX_def)
+apply(auto)[1]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply (metis ValOrd.intros(7))
+
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(simp add: POSIX_def)
+apply(auto)[1]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply (metis ValOrd.intros(7))
+apply(erule_tac [!] exE)
+prefer 3
+apply(frule POSIX_SEQ1)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(case_tac "flat v1 = []")
+apply(subgoal_tac "nullable r1")
+apply(simp)
+prefer 2
+apply(rule_tac v="v1" in Prf_flat_empty)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+
+
+lemma POSIX_proj:
+  assumes "POSIX v r" "\<turnstile> v : r" "\<exists>s. flat v = c#s"
+  shows "POSIX (projval r c v) (der c r)"
+using assms
+apply(induct r c v arbitrary: rule: projval.induct)
+defer
+defer
+defer
+defer
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(simp add: POSIX_def)
+apply(auto)[1]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply (metis ValOrd.intros(7))
+apply(erule_tac [!] exE)
+prefer 3
+apply(frule POSIX_SEQ1)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(case_tac "flat v1 = []")
+apply(subgoal_tac "nullable r1")
+apply(simp)
+prefer 2
+apply(rule_tac v="v1" in Prf_flat_empty)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(simp)
+apply(rule ccontr)
+apply(drule v3_proj)
+apply(simp)
+apply(simp)
+apply(drule POSIX_ex)
+apply(erule exE)
+apply(frule POSIX_ALT_cases2)
+apply(simp)
+apply(simp)
+apply(erule 
+prefer 2
+apply(case_tac "nullable r1")
+prefer 2
+apply(simp)
+apply(rotate_tac 1)
+apply(drule meta_mp)
+apply(rule POSIX_SEQ1)
+apply(assumption)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(rotate_tac 7)
+apply(drule meta_mp)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(rotate_tac 7)
+apply(drule meta_mp)
+apply (metis Cons_eq_append_conv)
+
+
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(simp add: POSIX_def)
+apply(simp)
+apply(simp)
+apply(simp_all)[5]
+apply(simp add: POSIX_def)
+
+done
+(* NULL case *)
+apply(simp add: POSIX_def)
+apply(auto)[1]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply (metis ValOrd.intros(7))
+apply(rotate_tac 4)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(simp)
+prefer 2
+apply(simp)
+apply(frule POSIX_ALT1a)
+apply(drule meta_mp)
+apply(simp)
+apply(drule meta_mp)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(rule POSIX_ALT_I2)
+apply(assumption)
+apply(auto)[1]
+
+thm v4_proj2
+prefer 2
+apply(subst (asm) (13) POSIX_def)
+
+apply(drule_tac x="projval v2" in spec)
+apply(auto)[1]
+apply(drule mp)
+apply(rule conjI)
+apply(simp)
+apply(simp)
+
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+prefer 2
+apply(clarify)
+apply(subst (asm) (2) POSIX_def)
+
+apply (metis ValOrd.intros(5))
+apply(clarify)
+apply(simp)
+apply(rotate_tac 3)
+apply(drule_tac c="c" in t2)
+apply(subst (asm) v4_proj)
+apply(simp)
+apply(simp)
+thm contrapos_np contrapos_nn
+apply(erule contrapos_np)
+apply(rule ValOrd.intros)
+apply(subst  v4_proj2)
+apply(simp)
+apply(simp)
+apply(subgoal_tac "\<not>(length (flat v1) < length (flat (projval r2a c v2a)))")
+prefer 2
+apply(erule contrapos_nn)
+apply (metis nat_less_le v4_proj2)
+apply(simp)
+
+apply(blast)
+thm contrapos_nn
+
+apply(simp add: POSIX_def)
+apply(auto)[1]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(clarify)
+apply(rule ValOrd.intros)
+apply(drule meta_mp)
+apply(auto)[1]
+apply (metis POSIX_ALT2 POSIX_def flat.simps(3))
+apply metis
+apply(clarify)
+apply(rule ValOrd.intros)
+apply(simp)
+apply(simp add: POSIX_def)
+apply(auto)[1]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(clarify)
+apply(rule ValOrd.intros)
+apply(simp)
+
+apply(drule meta_mp)
+apply(auto)[1]
+apply (metis POSIX_ALT2 POSIX_def flat.simps(3))
+apply metis
+apply(clarify)
+apply(rule ValOrd.intros)
+apply(simp)
+
+
+done
+(* EMPTY case *)
+apply(simp add: POSIX_def)
+apply(auto)[1]
+apply(rotate_tac 3)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(drule_tac c="c" in t2)
+apply(subst (asm) v4_proj)
+apply(auto)[2]
+
+apply(erule ValOrd.cases)
+apply(simp_all)[8]
+(* CHAR case *)
+apply(case_tac "c = c'")
+apply(simp)
+apply(erule ValOrd.cases)
+apply(simp_all)[8]
+apply(rule ValOrd.intros)
+apply(simp)
+apply(erule ValOrd.cases)
+apply(simp_all)[8]
+(* ALT case *)
+
+
+unfolding POSIX_def
+apply(auto)
+thm v4
+
+lemma Prf_inj:
+  assumes "v1 \<succ>(der c r) v2" "\<turnstile> v1 : der c r" "\<turnstile> v2 : der c r" "flat v1 = flat v2"
+  shows "(injval r c v1) \<succ>r (injval r c v2)"
+using assms
+apply(induct arbitrary: v1 v2 rule: der.induct)
+(* NULL case *)
+apply(simp)
+apply(erule ValOrd.cases)
+apply(simp_all)[8]
+(* EMPTY case *)
+apply(erule ValOrd.cases)
+apply(simp_all)[8]
+(* CHAR case *)
+apply(case_tac "c = c'")
+apply(simp)
+apply(erule ValOrd.cases)
+apply(simp_all)[8]
+apply(rule ValOrd.intros)
+apply(simp)
+apply(erule ValOrd.cases)
+apply(simp_all)[8]
+(* ALT case *)
+apply(simp)
+apply(erule ValOrd.cases)
+apply(simp_all)[8]
+apply(rule ValOrd.intros)
 apply(subst v4)
 apply(clarify)
 apply(rotate_tac 3)
@@ -769,13 +1178,16 @@
 apply(simp_all)[5]
 apply(subst v4)
 apply(clarify)
+apply(rotate_tac 2)
 apply(erule Prf.cases)
 apply(simp_all)[5]
 apply(simp)
 apply(rule ValOrd.intros)
 apply(clarify)
+apply(rotate_tac 3)
 apply(erule Prf.cases)
 apply(simp_all)[5]
+apply(clarify)
 apply(erule Prf.cases)
 apply(simp_all)[5]
 apply(rule ValOrd.intros)
@@ -805,10 +1217,37 @@
 apply(simp_all)[5]
 apply(erule Prf.cases)
 apply(simp_all)[5]
+apply(clarify)
+defer
+apply(simp)
+apply(erule ValOrd.cases)
+apply(simp_all del: injval.simps)[8]
+apply(simp)
+apply(clarify)
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(clarify)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(clarify)
+apply(rule ValOrd.intros(2))
+
+
+
+
+done
+
+
+txt {*
+done
 (* nullable case - unfinished *)
 apply(simp)
 apply(erule ValOrd.cases)
-apply(simp_all)[8]
+apply(simp_all del: injval.simps)[8]
+apply(simp)
 apply(clarify)
 apply(simp)
 apply(erule Prf.cases)
@@ -820,12 +1259,9 @@
 apply(simp_all)[5]
 apply(clarify)
 apply(simp)
-apply(case_tac "injval r1 c v1 = mkeps r1") 
-apply(rule ValOrd.intros(1))
-apply(simp)
-apply (metis impossible_Cons le_add2 list.size(3) mkeps_flat monoid_add_class.add.right_neutral v4)
 apply(rule ValOrd.intros(2))
-apply(drule_tac x="proj r1 c" in spec)
+oops
+*}
 oops
 
 lemma POSIX_der:
diff -r 2cdbab037861 -r a6bb0152ccc2 thys/notes.pdf
Binary file thys/notes.pdf has changed
diff -r 2cdbab037861 -r a6bb0152ccc2 thys/notes.tex
--- a/thys/notes.tex	Sat Jan 31 18:21:03 2015 +0000
+++ b/thys/notes.tex	Mon Feb 09 12:13:10 2015 +0000
@@ -348,5 +348,8 @@
 \end{tabular}
 \end{center}
 
+\subsection*{Problems in the paper proof}
+
+I cannot verify 
 
 \end{document}