--- a/thys/Re1.thy	Mon May 25 16:09:23 2015 +0100
+++ b/thys/Re1.thy	Mon Jun 08 14:37:19 2015 +0100
@@ -434,111 +434,120 @@
 apply(simp_all)[8]
 done
 
-lemma ValOrd_max:
-  shows "\<exists>v. \<forall>v'. (v' \<succ>r v \<longrightarrow> v = v')" 
-apply(induct r)
-apply(auto)
-apply(rule exI)
-apply(rule allI)
-apply(rule impI)
-apply(erule ValOrd.cases)
-apply(simp_all)[8]
-apply(rule exI)
-apply(rule allI)
-apply(rule impI)
-apply(erule ValOrd.cases)
-apply(simp_all)[8]
-apply(rule exI)
-apply(rule allI)
+lemma
+  "s \<in> L r \<longrightarrow> (\<exists>vmax \<in> {v. \<turnstile> v : r \<and> flat v = s}. \<forall>v \<in> {v. \<turnstile> v : r \<and> flat v = s}. vmax 2\<succ> v)"
+apply(induct s arbitrary: r rule: length_induct)
+apply(induct_tac r rule: rexp.induct)
 apply(rule impI)
-apply(erule ValOrd.cases)
-apply(simp_all)[8]
-apply(rule exI)
-apply(rule allI)
-apply(rule impI)
-apply(erule ValOrd.cases)
-apply(simp_all)[8]
-apply(rule exI)
-apply(rule allI)
+apply(simp)
+apply(simp)
 apply(rule impI)
-apply(erule ValOrd.cases)
-apply(simp_all)[8]
-done
-
-lemma ValOrd_max:
-  assumes "L r \<noteq> {}"
-  shows "\<exists>v. \<turnstile> v : r \<and> (\<forall>v'. ((\<turnstile> v' : r \<and> v' \<succ>r v) \<longrightarrow> v = v'))" 
-using assms
-apply(induct r)
-apply(auto)
-apply(rule exI)
+apply(simp)
+apply(rule_tac x="Void" in exI)
+apply(simp)
 apply(rule conjI)
-apply(rule Prf.intros)
+apply (metis Prf.intros(4))
 apply(rule allI)
 apply(rule impI)
 apply(erule conjE)
-apply(erule ValOrd.cases)
-apply(simp_all)[8]
-apply(rule exI)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply (metis ValOrd2.intros(7))
+apply(simp)
+apply(rule impI)
+apply(rule_tac x="Char char" in exI)
+apply(simp)
 apply(rule conjI)
-apply(rule Prf.intros)
+apply (metis Prf.intros)
+apply(rule allI)
+apply(rule impI)
+apply(erule conjE)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply (metis ValOrd2.intros(8))
+apply(simp)
+apply(rule impI)
+apply(simp add: Sequ_def)[1]
+apply(erule exE)+
+apply(erule conjE)+
+apply(clarify)
+defer
+apply(simp)
+apply(rule conjI)
+apply(rule impI)
+apply(simp)
+apply(erule exE)
+apply(clarify)
+apply(rule_tac x="Left vmax" in exI)
+apply(rule conjI)
+apply (metis Prf.intros(2))
+apply(simp)
 apply(rule allI)
 apply(rule impI)
 apply(erule conjE)
-apply(erule ValOrd.cases)
-apply(simp_all)[8]
-apply(auto simp add: Sequ_def)[1]
-apply(drule meta_mp)
-apply (metis empty_iff)
-apply(drule meta_mp)
-apply (metis empty_iff)
-apply(auto)[1]
-apply(drule_tac x="Seq v va" in spec)
-apply(drule mp)
-apply (metis Prf.intros(1))
-apply(auto)[1]
-apply(erule ValOrd.cases)
-apply(simp_all)[8]
-apply(rotate_tac 6)
+apply(rotate_tac 5)
 apply(erule Prf.cases)
 apply(simp_all)[5]
-apply(rotate_tac 6)
+apply (metis ValOrd2.intros(6))
+apply(clarify)
+apply (metis ValOrd2.intros(3) order_refl)
+apply(rule impI)
+apply(simp)
+apply(erule exE)
+apply(clarify)
+apply(rule_tac x="Right vmax" in exI)
+apply(simp)
+apply(rule conjI)
+apply (metis Prf.intros(3))
+apply(rule allI)
+apply(rule impI)
+apply(erule conjE)+
+apply(rotate_tac 5)
 apply(erule Prf.cases)
 apply(simp_all)[5]
+apply (metis ValOrd2.intros(8))
+apply(simp)
+apply(rule impI)
+apply(simp add: Sequ_def)[1]
+apply(erule exE)+
+apply(erule conjE)+
 apply(clarify)
-apply metis
-apply(drule meta_mp)
-apply (metis empty_iff)
-apply(auto)[1]
-apply(drule_tac x="Left v" in spec)
-apply(drule mp)
-apply (metis Prf.intros)
-apply(auto)[1]
-apply(rotate_tac 4)
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(erule ValOrd.cases)
-apply(simp_all)[8]
-apply(erule ValOrd.cases)
-apply(simp_all)[8]
-apply(clarify)
-apply(auto)[1]
-oops
+
+
+inductive ValOrd3 :: "val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ 3\<succ>_ _" [100, 100, 100] 100)
+where
+  "\<lbrakk>v2 3\<succ>r2 v2'; \<turnstile> v1 : r1\<rbrakk> \<Longrightarrow> (Seq v1 v2) 3\<succ>(SEQ r1 r2) (Seq v1 v2')" 
+| "\<lbrakk>v1 3\<succ>r1 v1'; v1 \<noteq> v1'; flat v2 = flat v2'; \<turnstile> v2 : r2; \<turnstile> v2' : r2\<rbrakk> 
+      \<Longrightarrow> (Seq v1 v2) 3\<succ>(SEQ r1 r2) (Seq v1' v2')" 
+| "length (flat v1) \<ge> length (flat v2) \<Longrightarrow> (Left v1) 3\<succ>(ALT r1 r2) (Right v2)"
+| "length (flat v2) > length (flat v1) \<Longrightarrow> (Right v2) 3\<succ>(ALT r1 r2) (Left v1)"
+| "v2 3\<succ>r2 v2' \<Longrightarrow> (Right v2) 3\<succ>(ALT r1 r2) (Right v2')"
+| "v1 3\<succ>r1 v1' \<Longrightarrow> (Left v1) 3\<succ>(ALT r1 r2) (Left v1')"
+| "Void 3\<succ>EMPTY Void"
+| "(Char c) 3\<succ>(CHAR c) (Char c)"
+
 
-lemma ValOrd_max2:
-  shows "\<exists>v. \<turnstile> v : r \<and> (\<forall>v'. v \<succ>r v')" 
-using ValOrd_max[where r="r"]
-apply -
-apply(auto)
-apply(rule_tac x="v" in exI)
-apply(auto)
-oops
+lemma "v1 3\<succ>r v2 \<Longrightarrow> v1 \<succ>r v2 \<and> \<turnstile> v1 : r \<and> \<turnstile> v2 : r \<and> flat v1 = flat v2"
+apply(induct rule: ValOrd3.induct)
+prefer 8
+apply(simp)
+apply (metis Prf.intros(5) ValOrd.intros(8))
+prefer 7
+apply(simp)
+apply (metis Prf.intros(4) ValOrd.intros(7))
+apply(simp)
+apply (metis Prf.intros(1) ValOrd.intros(1))
+apply(simp)
+
+
+
 
 lemma ValOrd_trans:
-  assumes "v1 \<succ>r v2" "v2 \<succ>r v3" "\<turnstile> v1 : r" "\<turnstile> v2 : r" "\<turnstile> v3 : r" "flat v1 = flat v2" "flat v2 = flat v3"
+  assumes "v1 \<succ>r v2" "v2 \<succ>r v3" "\<turnstile> v1 : r" "\<turnstile> v2 : r" "\<turnstile> v3 : r" 
+     "flat v1 = flat v2" "flat v2 = flat v3"
   shows "v1 \<succ>r v3"
 using assms
-apply(induct r arbitrary: v1 v2 v3)
+apply(induct r arbitrary: v1 v2 v3 s1 s2 s3)
 apply(erule Prf.cases)
 apply(simp_all)[5]
 apply(erule Prf.cases)
@@ -574,10 +583,89 @@
 apply (rule ValOrd.intros(2))
 prefer 2
 apply(auto)[1]
-prefer 2
+apply metis
+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 ValOrd.cases)
+apply(simp_all)[8]
+apply(erule ValOrd.cases)
+apply(simp_all)[8]
+apply (metis Ord1 Ord3 Prf.intros(2) ValOrd2.intros(6))
+apply(erule ValOrd.cases)
+apply(simp_all)[8]
+apply(erule ValOrd.cases)
+apply(simp_all)[8]
+apply (rule ValOrd.intros)
+apply(clarify)
 oops
 
 
+lemma ValOrd_max:
+  shows "L r \<noteq> {} \<Longrightarrow> \<exists>v. \<turnstile> v : r \<and> (\<forall>v'. (\<turnstile> v' : r \<longrightarrow> v' \<succ>r v \<longrightarrow> v = v'))" 
+using assms
+apply(induct r)
+apply(auto)[3]
+apply(rule_tac x="Void" in exI)
+apply(rule conjI)
+apply (metis Prf.intros(4))
+apply(rule allI)
+apply(rule impI)+
+apply(erule ValOrd.cases)
+apply(simp_all)[8]
+apply(rule_tac x="Char char" in exI)
+apply(rule conjI)
+apply (metis Prf.intros(5))
+apply(rule allI)
+apply(rule impI)+
+apply(erule ValOrd.cases)
+apply(simp_all)[8]
+apply(simp add: L.simps)
+apply(auto simp: Sequ_def)[1]
+apply(drule meta_mp)
+apply (metis empty_iff)
+apply(drule meta_mp)
+apply (metis empty_iff)
+apply(erule exE)+
+apply(rule_tac x="Seq v va" in exI)
+apply(rule conjI)
+apply (metis Prf.intros(1))
+apply(rule allI)
+apply(rule impI)+
+apply(rotate_tac 4)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule ValOrd.cases)
+apply(simp_all)[8]
+apply metis
+apply(simp only: L.simps Lattices.bounded_lattice_bot_class.sup_eq_bot_iff HOL.de_Morgan_conj)
+apply(erule disjE)
+apply(drule meta_mp)
+apply (metis empty_iff)
+apply(erule exE)+
+apply(rule exI)
+apply(rule conjI)
+apply(rule Prf.intros)
+apply(erule conjE)+
+apply(assumption)
+apply(rule allI)
+apply(rule impI)+
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(clarify)
+apply(erule ValOrd.cases)
+apply(simp_all)[8]
+apply(clarify)
+apply(drule meta_mp)
+apply (metis Prf_flat_L empty_iff)
+apply(auto)[1]
+apply(erule ValOrd.cases)
+apply(simp_all)[8]
+apply(clarify)
+oops
 
 section {* Posix definition *}
 
@@ -661,6 +749,7 @@
 apply(drule meta_mp)
 apply (metis empty_iff)
 apply(auto)
+oops
 
 section {* POSIX for some constructors *}
 
@@ -1533,102 +1622,7 @@
 apply(auto)
 apply(frule POSIXs_ALT1a)
 (* HERE *)
-apply(auto)
-apply(rule ccontr)
-apply(simp)
-apply(auto)[1]
-apply(drule POSIXs_ALT1a)
-thm ValOrd2.intros
-
-apply(simp (no_asm) add: POSIXs_def)
-apply(auto)[1]
-apply (metis POSIXs_def 
-der.simps(4) v3s)
-apply(subst (asm) (5) POSIXs_def)
-apply(auto)[1]
-apply(erule Prfs.cases)
-apply(simp_all)[5]
-apply(erule Prfs.cases)
-apply(simp_all)[5]
-apply(auto)[1]
-apply(rule ValOrd2.intros)
-apply(drule_tac x="v1a" in meta_spec)
-apply(drule_tac x="sb" in meta_spec)
-apply(drule_tac meta_mp)
-defer
-apply (metis POSIXs_def)
-apply(auto)[1]
-apply(rule ValOrd2.intros)
-apply(subst v4)
-apply (metis Prfs_Prf)
-apply(simp)
-apply(drule_tac x="Left (injval r1a c v1)" in spec)
-apply(drule mp)
-apply(rule Prfs.intros)
-defer
-apply(erule ValOrd2.cases)
-apply(simp_all)[8] 
-apply(clarify)
-thm v4s
-apply(subst (asm) v4s[of "sb"])
-apply(assumption)
-apply(simp)
-apply(clarify)
-apply(erule Prfs.cases)
-apply(simp_all)[5]
-apply(auto)[1]
-apply(rule ValOrd2.intros)
-apply(subst v4)
-apply (metis Prfs_Prf)
-apply(simp)
-apply(drule_tac x="Right (injval r2a c v2)" in spec)
-apply(drule mp)
-apply(rule Prfs.intros)
-defer
-apply(erule ValOrd2.cases)
-apply(simp_all)[8] 
-apply(clarify)
-apply(subst (asm) v4)
-defer
-apply(simp)
-apply(rule ValOrd2.intros)
-apply (metis POSIXs_ALT1a POSIXs_def Prfs.intros(3))
-apply(case_tac "nullable r1")
-apply(simp (no_asm) add: POSIXs_def)
-apply(auto)[1]
-apply(subst (asm) (6) POSIXs_def)
-apply(auto)[1]
-apply(erule Prfs.cases)
-apply(simp_all)[5]
-apply(clarify)
-defer
-apply (metis Prfs.intros(3) der.simps(5) injval.simps(6) v3s)
-apply(erule Prfs.cases)
-apply(simp_all)[5]
-apply(clarify)
-apply(subst (asm) (6) POSIXs_def)
-apply(auto)[1]
-apply(rotate_tac 7)
-apply(erule Prfs.cases)
-apply(simp_all)[5]
-apply(clarify)
-apply(simp)
-apply(rotate_tac 8)
-apply(erule Prfs.cases)
-apply(simp_all)[5]
-apply(clarify)
-apply(rule ValOrd2.intros(2))
-apply(drule_tac x="v1b" in meta_spec)
-apply(drule_tac x="s1a" in meta_spec)
-apply(drule meta_mp)
-defer
-apply(subst (asm) Cons_eq_append_conv)
-apply(auto)
-defer
-defer
-
-
-thm v4
+oops
 
 lemma t: "(c#xs = c#ys) \<Longrightarrow> xs = ys"
 by (metis list.sel(3))
@@ -1763,6 +1757,139 @@
 oops
 
 lemma Prf_inj_test:
+  assumes "v1 2\<succ> v2" "\<turnstile> v1 : der c r" "\<turnstile> v2 : der c r" 
+  "length (flat v1) = length (flat v2)"
+  shows "(injval r c v1) 2\<succ>  (injval r c v2)"
+using assms
+apply(induct c r arbitrary: v1 v2 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(case_tac "c = c'")
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule ValOrd2.cases)
+apply(simp_all)[8]
+apply(rule ValOrd2.intros)
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+(* ALT case *)
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(auto)[2]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(auto)[2]
+apply(erule ValOrd2.cases)
+apply(simp_all)[8]
+apply(rule ValOrd2.intros)
+apply(auto)[1]
+apply(erule ValOrd2.cases)
+apply(simp_all)[8]
+apply(rule ValOrd2.intros)
+apply(subst v4)
+apply metis
+apply(subst v4)
+apply (metis)
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(auto)[2]
+apply(erule ValOrd2.cases)
+apply(simp_all)[8]
+apply(rule ValOrd2.intros)
+apply(erule ValOrd2.cases)
+apply(simp_all)[8]
+(* 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 ValOrd2.cases)
+apply(simp_all)[8]
+apply(clarify)
+apply(rule ValOrd2.intros)
+apply(simp)
+apply(rule ValOrd2.intros)
+apply(auto)[1]
+
+using injval_inj
+apply(simp add: inj_on_def)
+apply metis
+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(erule Prf.cases)
+apply(simp_all)[5]
+apply(clarify)
+apply(erule ValOrd2.cases)
+apply(simp_all)[8]
+apply(clarify)
+apply(erule ValOrd2.cases)
+apply(simp_all)[8]
+apply(clarify)
+apply (metis ValOrd2.intros(1))
+apply(rule ValOrd2.intros)
+apply metis
+using injval_inj
+apply(simp add: inj_on_def)
+apply metis
+apply(clarify)
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(clarify)
+apply(rule ValOrd2.intros)
+apply(rule Ord1)
+apply(rule h)
+apply(simp)
+apply(simp)
+apply (metis list.distinct(1) mkeps_flat v4)
+apply(clarify)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(clarify)
+apply(rotate_tac 7)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(clarify)
+defer
+apply(clarify)
+apply(erule ValOrd2.cases)
+apply(simp_all)[8]
+apply(clarify)
+apply (metis ValOrd2.intros(1))
+apply(erule ValOrd2.cases)
+apply(simp_all)[8]
+apply(clarify)
+apply(simp)
+apply (rule_tac ValOrd2.intros(2))
+prefer 2
+apply (metis list.distinct(1) mkeps_flat v4)
+
+
+lemma Prf_inj_test:
   assumes "v1 2\<succ> v2" "\<Turnstile>s1 v1 : der c r" "\<Turnstile>s2 v2 : der c r"  
   shows "(injval r c v1) 2\<succ>  (injval r c v2)"
 using assms