# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1422522340 0
# Node ID 38cde0214ad52359e189c4bd277736f9111a78db
# Parent  d67149236738e51f2c1fccd9834f8bd8f3d5ec6b
added some lemmas, attempted others

diff -r d67149236738 -r 38cde0214ad5 thys/Re1.thy
--- a/thys/Re1.thy	Mon Jan 26 16:01:58 2015 +0000
+++ b/thys/Re1.thy	Thu Jan 29 09:05:40 2015 +0000
@@ -117,6 +117,7 @@
 | "Void \<succ>EMPTY Void"
 | "(Char c) \<succ>(CHAR c) (Char c)"
 
+
 section {* The ordering is reflexive *}
 
 lemma ValOrd_refl:
@@ -357,8 +358,6 @@
 
 
 
-
-
 section {* The Matcher *}
 
 fun
@@ -630,8 +629,37 @@
 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 behin the injection value is an added c
+  The string behind the injection value is an added c
 *}
 
 lemma v4:
@@ -671,6 +699,331 @@
 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 t: "(c#xs = c#ys) \<Longrightarrow> xs = ys"
+by (metis list.sel(3))
+
+lemma Prf_proj:
+  assumes "v1 \<succ>r v2" "\<turnstile> v1 : r" "\<turnstile> v2 : r" "\<exists>s. (flat v1) = c # s" "\<exists>s. (flat v2) = c # s"
+  shows "(projval r c v1) \<succ>(der c r) (projval r c v2)"
+using assms
+apply(induct arbitrary: v1 v2 rule: der.induct)
+apply(simp)
+apply(erule ValOrd.cases)
+apply(simp_all)[8]
+apply(erule ValOrd.cases)
+apply(simp_all)[8]
+apply(case_tac "c = c'")
+apply(simp)
+apply (metis ValOrd.intros(7))
+apply(erule ValOrd.cases)
+apply(simp_all)[8]
+apply(simp)
+apply(erule ValOrd.cases)
+apply(simp_all)[8]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(clarify)
+apply(rule ValOrd.intros)
+apply(subst v4_proj2)
+apply(simp)
+apply(simp)
+apply(subst v4_proj2)
+apply(simp)
+apply(simp)
+apply(simp)
+apply(clarify)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(clarify)
+apply(rule ValOrd.intros)
+apply(subst v4_proj2)
+apply(simp)
+apply(simp)
+apply(subst v4_proj2)
+apply(simp)
+apply(simp)
+apply(simp)
+apply(clarify)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(clarify)
+apply(rule ValOrd.intros)
+apply metis
+apply(clarify)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(clarify)
+apply(rule ValOrd.intros)
+apply metis
+apply(clarify)
+apply(simp)
+apply(auto)
+defer
+apply(erule ValOrd.cases)
+apply(simp_all)[8]
+apply(auto)[1]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(clarify)
+apply(simp)
+apply (metis Prf_flat_L nullable_correctness)
+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(simp)
+apply(auto)[1]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(clarify)
+apply (metis Prf_flat_L nullable_correctness)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(clarify)
+apply (metis Prf_flat_L nullable_correctness)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(clarify)
+apply (metis Prf_flat_L nullable_correctness)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(clarify)
+apply(rule ValOrd.intros(2))
+apply (metis append_Cons list.inject neq_Nil_conv)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(clarify)
+apply(auto)
+apply(erule ValOrd.cases)
+apply(simp_all)[8]
+apply(auto)[1]
+apply(rule ValOrd.intros)
+apply metis
+apply(clarify)
+apply(rule ValOrd.intros)
+
+apply(rule ValOrd.intros)
+apply(simp)
+apply(simp)
+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)
+defer
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(clarify)
+apply(simp add: append_eq_Cons_conv)
+apply(clarify)
+apply(rule ValOrd.intros)
+apply(simp)
+apply(subst v4_proj2)
+apply(simp)
+apply(simp)
+apply(subst v4_proj2)
+apply(simp)
+apply(simp)
+
+apply(simp)
+
+apply (metis Prf_flat_L nullable_correctness)
+
+
+
+
+apply(rule ValOrd.intros(2))
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(simp)
+apply(erule ValOrd.cases)
+apply(simp_all)[8]
+apply(clarify)
+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(simp)
+
+lemma Prf_inj:
+  assumes "v1 \<succ>(der c r) v2" "\<turnstile> v1 : der c r" "\<turnstile> v2 : der c r"
+  shows "(injval r c v1) \<succ>r (injval r c v2)"
+using assms
+apply(induct arbitrary: v1 v2 rule: der.induct)
+apply(simp)
+apply(erule ValOrd.cases)
+apply(simp_all)[8]
+apply(erule ValOrd.cases)
+apply(simp_all)[8]
+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]
+apply(simp)
+apply(erule ValOrd.cases)
+apply(simp_all)[8]
+apply(rule ValOrd.intros)
+apply(subst v4)
+apply(clarify)
+apply(rotate_tac 3)
+apply(erule Prf.cases)
+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(subst v4)
+apply(clarify)
+apply(rotate_tac 3)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(subst v4)
+apply(clarify)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+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]
+apply(simp)
+apply(case_tac "nullable r1")
+defer
+apply(simp)
+apply(erule ValOrd.cases)
+apply(simp_all)[8]
+apply(clarify)
+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(simp)
+apply(rule ValOrd.intros(2))
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(simp)
+apply(erule ValOrd.cases)
+apply(simp_all)[8]
+apply(clarify)
+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(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(rotate_tac 1)
+apply(drule meta_mp)
+apply(rule
+
+lemma POSIX_der:
+  assumes "POSIX v (der c r)" "\<turnstile> v : der c r"
+  shows "POSIX (injval r c v) r"
+using assms
+unfolding POSIX_def
+apply(auto)
+apply(subst (asm) v4)
+apply(assumption)
+apply(drule_tac x="projval r c v'" in spec)
+apply(drule mp)
+apply(auto)
+apply(rule v3_proj)
+apply(simp)
+apply(rule_tac x="flat v" in exI)
+apply(simp)
+apply(rule_tac c="c" in  t)
+apply(simp)
+apply(subst v4_proj)
+apply(simp)
+apply(rule_tac x="flat v" in exI)
+apply(simp)
+apply(simp)
+apply(simp add: Cons_eq_append_conv)
+apply(auto)[1]
+
 text {*
   Injection followed by projection is the identity.
 *}
@@ -754,7 +1107,7 @@
 apply(simp)
 apply (metis ValOrd_refl)
 apply(simp add: POSIX3_def)
-
+oops
 
 lemma "\<exists>v. POSIX v r"
 apply(induct r)
@@ -817,12 +1170,15 @@
   shows "POSIX (injval r c v) r"
 using assms
 apply(induct arbitrary: v rule: der.induct)
+(* NULL case *)
 apply(simp)
 apply(erule Prf.cases)
 apply(simp_all)[5]
+(* EMPTY case *)
 apply(simp)
 apply(erule Prf.cases)
 apply(simp_all)[5]
+(* CHAR case *)
 apply(simp)
 apply(case_tac "c = c'")
 apply(auto simp add: POSIX_def)[1]
@@ -830,8 +1186,8 @@
 apply(simp_all)[5]
 apply(erule Prf.cases)
 apply(simp_all)[5]
-using ValOrd.simps apply blast
-apply(auto)
+apply(rule ValOrd.intros)
+apply(auto)[1]
 apply(erule Prf.cases)
 apply(simp_all)[5]
 (* base cases done *)
@@ -840,6 +1196,30 @@
 apply(simp_all)[5]
 using POSIX_ALT POSIX_ALT_I1 apply blast
 apply(clarify)
+apply(simp)
+apply(rule POSIX_ALT_I2)
+apply(drule POSIX_ALT1a)
+apply metis
+apply(auto)[1]
+apply(subst v4)
+apply(assumption)
+apply(simp)
+apply(drule POSIX_ALT1a)
+apply(rotate_tac 1)
+apply(drule_tac x="v2" in meta_spec)
+apply(simp)
+
+apply(rotate_tac 4)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(rule ValOrd.intros)
+apply(simp)
+apply(subst (asm) v4)
+apply(assumption)
+apply(clarify)
+thm POSIX_ALT1a POSIX_ALT1b POSIX_ALT_I2
+apply(subst (asm) v4)
+apply(auto simp add: POSIX_def)[1]
 apply(subgoal_tac "POSIX v2 (der c r2)")
 prefer 2
 apply(auto simp add: POSIX_def)[1]
@@ -853,7 +1233,6 @@
 apply(subgoal_tac "\<turnstile> Right (injval r2 c v2) : (ALT r1 r2)")
 prefer 2
 apply (metis Prf.intros(3) v3)
-
 apply auto[1]
 apply(subst v4)
 apply(auto)[2]