# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1410190573 -3600
# Node ID 87618dae0e047700d5e0cb6129fb680ebde5e027
# Parent  fe177dfc46971a0ccaee48000d9f0d01aaf2fc8e
getting back the original version by Sulzmann

diff -r fe177dfc4697 -r 87618dae0e04 thys/Re.thy
--- a/thys/Re.thy	Mon Sep 08 14:06:15 2014 +0100
+++ b/thys/Re.thy	Mon Sep 08 16:36:13 2014 +0100
@@ -64,6 +64,7 @@
 | "flat(Right v) = flat(v)"
 | "flat(Seq v1 v2) = flat(v1) @ flat(v2)"
 
+(* not actually in the paper *)
 datatype tree = 
   Leaf string
 | Branch tree tree
@@ -103,11 +104,14 @@
 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))
+sorry
+
+(*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')" 
+  "\<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')" 
 | "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')"
@@ -115,6 +119,7 @@
 | "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))"
@@ -126,54 +131,13 @@
 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))
-
+  "POSIX v r \<equiv> (\<forall>v'. (\<turnstile> v' : r \<and> flat v = flat v') \<longrightarrow> v \<succ>r v')"
 
-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"
@@ -186,7 +150,9 @@
 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)" 
@@ -271,6 +237,7 @@
 apply(rule ValOrd.intros)
 apply(auto)
 done
+*)
 
 lemma ValOrd_refl:
   assumes "\<turnstile> v : r"
@@ -280,12 +247,14 @@
 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 *}
 
@@ -337,41 +306,16 @@
   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 (metis ValOrd.intros)
 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))
+sorry
+
 
 fun
  der :: "char \<Rightarrow> rexp \<Rightarrow> rexp"
@@ -556,10 +500,18 @@
 apply (metis Nil_is_append_conv head.elims option.distinct(1))
 done
 
+(* HERE *)
 lemma v5:
   assumes "\<turnstile> v : der c r" "POSIX v (der c r)"
   shows "POSIX (injval r c v) r"
 using assms
+apply(induct r)
+apply(simp (no_asm) only: POSIX_def)
+apply(rule allI)
+apply(rule impI)
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[5]
 apply(induct arbitrary: v rule: der.induct)
 apply(simp)
 apply(erule Prf.cases)