--- a/thys/Sulzmann.thy	Sat Jun 24 18:50:26 2017 +0100
+++ b/thys/Sulzmann.thy	Sun Jun 25 12:44:01 2017 +0100
@@ -1431,185 +1431,169 @@
   assumes "s \<in> r \<rightarrow> v1" 
   shows "\<not>(\<exists>v2 \<in> CPT r s. v2 :\<sqsubset>val v1)"
 using assms
-apply(induct)
-apply(auto)[1]
-apply(simp add: CPT_def)
-apply(simp add: val_ord_ex_def)
-apply(erule exE)
-apply(simp add: val_ord_def)
-apply(auto simp add: pflat_len_simps)[1]
-using Prf_CPrf Prf_elims(4) apply blast
-(* CHAR *)
-apply(auto)[1]
-apply(simp add: CPT_def)
-apply(simp add: val_ord_ex_def)
-apply(clarify)
-apply(erule CPrf.cases)
-apply(simp_all)
-apply(simp add: val_ord_def)
-(* ALT *)
-apply(auto)[1]
-apply(simp add: CPT_def)
-apply(clarify)
-apply(erule CPrf.cases)
-apply(simp_all)
-apply(simp add: val_ord_ex_def)
-apply(clarify)
-apply(case_tac p)
-apply(simp)
-apply(simp add: val_ord_def)
-apply(auto)[1]
-apply(auto simp add: pflat_len_simps)[1]
-using Posix1(2) apply auto[1]
-apply(clarify)
-using val_ord_ALTE apply blast
-apply(simp add: val_ord_ex_def)
-apply(clarify)
-apply(simp add: val_ord_def)
-apply(auto simp add: pflat_len_simps)[1]
-using Posix1(2) apply auto[1]
-apply (metis (mono_tags, lifting) One_nat_def Pos_empty Sulzmann.lexordp_simps(3) Un_iff inlen_bigger less_minus_one_simps(1) mem_Collect_eq not_less pflat_len_simps(3) pflat_len_simps(6) pflat_len_simps(7) zero_less_one)
-(* ALT RIGHT case *)
+by (metis Posix_val_ord_stronger less_irrefl val_ord_def 
+    val_ord_ex1_def val_ord_ex_def val_ord_ex_trans)
+
+(*
+lemma CPrf_Stars:
+  assumes "\<forall>v \<in> set vs. \<Turnstile> v : r"
+  shows "\<Turnstile> Stars vs : STAR r"
+using assms
+apply(induct vs) 
+apply(auto intro: CPrf.intros)
+a
+
+lemma L_flat_CPrf:
+  assumes "s \<in> L r" 
+  shows "\<exists>v. \<Turnstile> v : r \<and> flat v = s"
+using assms
+apply(induct r arbitrary: s)
+apply(auto simp add: Sequ_def intro: CPrf.intros)
+using CPrf.intros(1) flat.simps(5) apply blast
+using CPrf.intros(2) flat.simps(3) apply blast
+using CPrf.intros(3) flat.simps(4) apply blast
+apply(subgoal_tac "\<exists>vs::val list. concat (map flat vs) = s \<and> (\<forall>v \<in> set vs. \<Turnstile> v : r)")
 apply(auto)[1]
-apply(simp add: CPT_def)
-apply(clarify)
-apply(erule CPrf.cases)
-apply(simp_all)
-apply(simp add: val_ord_ex_def)
-apply(clarify)
-apply (simp add: L_flat_Prf1 Prf_CPrf)
-apply(simp add: val_ord_ex_def)
-apply(clarify)
-apply(case_tac p)
-apply (simp add: Posix1(2) pflat_len_simps(7) val_ord_def)
-using val_ord_ALTE2 apply blast
-(* SEQ case *)
-apply(clarify)
-apply(simp add: CPT_def)
-apply(clarify)
-apply(erule CPrf.cases)
-apply(simp_all)
-apply(drule_tac r="r1a" in val_ord_SEQ)
-apply(simp)
-using Posix1(2) apply auto[1]
-apply (simp add: Prf_CPrf)
-apply (simp add: Posix1a)
-apply(auto)[1]
-apply(subgoal_tac "length (flat v1a) \<le> length s1")
-prefer 2
-apply (metis L_flat_Prf1 Prf_CPrf append_eq_append_conv_if append_eq_conv_conj drop_eq_Nil)
-apply(subst (asm) append_eq_append_conv_if)
-apply(simp)
-apply (metis (mono_tags, lifting) CPT_def Posix_CPT le_less_linear mem_Collect_eq take_all val_ord_ex_trans val_ord_shorterI)
-using Posix1(2) apply auto[1]
-(* STAR case *)
-apply(clarify)
-apply(simp add: CPT_def)
-apply(clarify)
-apply(erule CPrf.cases)
-apply(simp_all)
-apply (simp add: Posix1(2))
-apply(subgoal_tac "length (flat va) \<le> length s1")
-prefer 2
-apply (metis L.simps(6) L_flat_Prf1 Prf_CPrf append_eq_append_conv_if append_eq_conv_conj drop_eq_Nil flat_Stars)
-apply(subst (asm) append_eq_append_conv_if)
+apply(rule_tac x="Stars vs" in exI)
 apply(simp)
 (* HERE *)
-apply(case_tac "flat va = s1")
-prefer 2
-apply(subgoal_tac "v :\<sqsubset>val va")
+apply (simp add: Prf_Stars)
+apply(drule Star_string)
+apply(auto)
+apply(rule Star_val)
+apply(auto)
+done
+*)
+
+definition PT :: "rexp \<Rightarrow> string \<Rightarrow> val set"
+where "PT r s \<equiv> {v. flat v = s \<and> \<turnstile> v : r}"
+
+lemma val_ord_Posix:
+  assumes "v1 \<in> CPT r s" "\<not>(\<exists>v2 \<in> PT r s. v2 :\<sqsubset>val v1)"
+  shows "s \<in> r \<rightarrow> v1" 
+using assms
+apply(induct r arbitrary: s v1)
+apply(auto simp add: CPT_def PT_def)[1]
+apply(erule CPrf.cases)
+apply(simp_all)
+(* ONE *)
+apply(auto simp add: CPT_def)[1]
+apply(erule CPrf.cases)
+apply(simp_all)
+apply(rule Posix.intros)
+(* CHAR *)
+apply(auto simp add: CPT_def)[1]
+apply(erule CPrf.cases)
+apply(simp_all)
+apply(rule Posix.intros)
 prefer 2
-apply (metis Posix1(2) le_less_linear take_all val_ord_shorterI)
-apply(rotate_tac 3)
-apply(simp add: val_ord_ex_def)
-apply(clarify)
-apply(case_tac p)
-apply(simp add: val_ord_def pflat_len_simps)
-apply (smt Posix1(2) append_take_drop_id flat_Stars intlen_append)
+(* ALT *)
+apply(auto simp add: CPT_def PT_def)[1]
+apply(erule CPrf.cases)
+apply(simp_all)
+apply(rule Posix.intros)
+apply(drule_tac x="flat v1a" in meta_spec)
+apply(drule_tac x="v1a" in meta_spec)
+apply(drule meta_mp)
+apply(simp)
+apply(drule meta_mp)
+apply(auto)[1]
+apply(drule_tac x="Left v2" in spec)
+apply(simp)
+apply(drule mp)
+apply(rule Prf.intros)
 apply(simp)
-prefer 2
+apply (meson val_ord_ALTI val_ord_ex_def)
+apply(assumption)
+(* ALT Right *)
+apply(auto simp add: CPT_def)[1]
+apply(rule Posix.intros)
+apply(rotate_tac 1)
+apply(drule_tac x="flat v2" in meta_spec)
+apply(drule_tac x="v2" in meta_spec)
+apply(drule meta_mp)
 apply(simp)
-apply(drule_tac x="va" in spec)
+apply(drule meta_mp)
+apply(auto)[1]
+apply(drule_tac x="Right v2a" in spec)
+apply(simp)
+apply(drule mp)
+apply(rule Prf.intros)
 apply(simp)
 apply(subst (asm) (2) val_ord_ex_def)
-apply(subst (asm) (2) val_ord_ex_def)
+apply(erule exE)
+apply(drule val_ord_ALTI2)
+apply(assumption)
+apply(auto simp add: val_ord_ex_def)[1]
+apply(assumption)
+apply(auto)[1]
+apply(subgoal_tac "\<exists>v2'. flat v2' = flat v2 \<and> \<turnstile> v2' : r1a")
 apply(clarify)
-apply(simp)
-apply(drule_tac x="Stars vsa" in spec)
-apply(simp)
-apply(case_tac p)
+apply(drule_tac x="Left v2'" in spec)
 apply(simp)
-apply (metis Posix1(2) flat.simps(7) flat_Stars less_irrefl pflat_len_simps(7) val_ord_def)
-apply(clarify)
-apply(case_tac a)
+apply(drule mp)
+apply(rule Prf.intros)
+apply(assumption)
+apply(simp add: val_ord_ex_def)
+apply(subst (asm) (3) val_ord_def)
 apply(simp)
-apply(subst (asm) val_ord_ex_def)
-apply(simp)
-apply(subst (asm) (2) val_ord_def)
-apply(clarify)
-apply(simp add: pflat_len_Stars_simps)
 apply(simp add: pflat_len_simps)
-prefer 3
-proof -
-  fix s1 :: "char list" and v :: val and s2 :: "char list" and vs :: "val list" and va :: val and ra :: rexp and vsa :: "val list" and p :: "nat list" and pa :: "nat list" and a :: nat and list :: "nat list"
-  assume a1: "length (flat va) \<le> length s1"
-  assume a2: "s1 \<in> ra \<rightarrow> v"
-  assume a3: "s2 \<in> STAR ra \<rightarrow> Stars vs"
-  assume a4: "Stars (va # vsa) \<sqsubset>val a # list Stars (v # vs)"
-  assume a5: "v \<sqsubset>val pa va"
-  assume a6: "flat va = take (length (flat va)) s1"
-  assume a7: "concat (map flat vsa) = drop (length (flat va)) s1 @ s2"
-  assume "p = a # list"
-  obtain nns :: "val \<Rightarrow> val \<Rightarrow> nat list" where
-    f8: "(\<forall>v va. \<not> v :\<sqsubset>val va \<or> v \<sqsubset>val nns v va va) \<and> (\<forall>v va. (\<forall>ns. \<not> v \<sqsubset>val ns va) \<or> v :\<sqsubset>val va)"
-    using val_ord_ex_def by moura
-  then have "Stars (v # vs) :\<sqsubset>val Stars (va # vsa)"
-    using a7 a6 a5 a3 a2 a1 by (metis Posix1(2) append_eq_append_conv_if flat.simps(7) flat_Stars val_ord_STARI)
-  then show False
-    using f8 a4 by (meson less_irrefl val_ord_def val_ord_ex_trans)
-next
-  fix v :: val and vs :: "val list" and va :: val and ra :: rexp and vsa :: "val list" and list :: "nat list"
-  assume a1: "intlen (flat va @ concat (map flat vsa)) = intlen (flat v @ concat (map flat vs)) \<and> (\<forall>q\<in>{0 # ps |ps. ps \<in> Pos va} \<union> {Suc n # ps |n ps. n # ps \<in> Pos (Stars vsa)} \<union> ({0 # ps |ps. ps \<in> Pos v} \<union> {Suc n # ps |n ps. n # ps \<in> Pos (Stars vs)}). q \<sqsubset>lex 0 # list \<longrightarrow> pflat_len (Stars (va # vsa)) q = pflat_len (Stars (v # vs)) q)"
-  assume a2: "pflat_len v list < pflat_len va list"
-  assume a3: "list \<in> Pos va"
-  assume a4: "\<forall>p. \<not> va \<sqsubset>val p v"
-  have f5: "\<And>ns. pflat_len (Stars (v # vs)) ns = pflat_len (Stars (va # vsa)) ns \<or> \<not> ns \<sqsubset>lex 0 # list \<or> (\<forall>nsa. ns \<noteq> 0 # nsa \<or> nsa \<notin> Pos v)"
-    using a1 by fastforce
-  have "\<And>ns. pflat_len (Stars (v # vs)) ns = pflat_len (Stars (va # vsa)) ns \<or> \<not> ns \<sqsubset>lex 0 # list \<or> (\<forall>nsa. ns \<noteq> 0 # nsa \<or> nsa \<notin> Pos va)"
-    using a1 by fastforce
-  then show False
-    using f5 a4 a3 a2 by (metis (no_types) Sulzmann.lexordp_simps(3) Un_iff pflat_len_Stars_simps2(2) val_ord_def)
-next
-  fix v abd vs and va and ra and vsa and p a and list and nat
-  assume "flat va \<in> ra \<rightarrow> v"
-         "concat (map flat vsa) \<in> STAR ra \<rightarrow> Stars vs" "flat v \<noteq> []"
-         "\<forall>s\<^sub>3. flat va @ s\<^sub>3 \<in> L ra \<longrightarrow> s\<^sub>3 = [] \<or> (\<forall>s\<^sub>4. s\<^sub>3 @ s\<^sub>4 = concat (map flat vsa) \<longrightarrow> s\<^sub>4 \<notin> L ra\<star>)"
-         "\<Turnstile> va : ra" "flat va \<noteq> []"
-         "\<Turnstile> Stars vsa : STAR ra" 
-         "\<forall>p. \<not> va \<sqsubset>val p v" "Stars (va # vsa) \<sqsubset>val a # list Stars (v # vs)" 
-         "\<not> Stars vsa :\<sqsubset>val Stars vs" "a = Suc nat"
-  then show "False"
-  apply -
-  apply(subst (asm) val_ord_ex_def)
-  apply(simp)
-  apply(drule STAR_val_ord)
-  using Posix1(2) apply auto[1]
-  apply blast
-  done
-next
-  fix r
-  show " \<forall>v2\<in>CPT (STAR r) []. \<not> v2 :\<sqsubset>val Stars []"
-  apply -
-  apply(rule ballI)    
-  apply(simp add: CPT_def)
-  apply(auto)
-  apply(erule CPrf.cases)
-  apply(simp_all)
-  apply(simp add: val_ord_ex_def)
-  apply(clarify)
-  apply(simp add: val_ord_def)
-  done
-qed  
+apply(drule_tac x="[0]" in spec)
+apply(simp add: pflat_len_simps Pos_empty)
+apply(drule mp)
+apply (smt inlen_bigger)
+apply(erule disjE)
+apply blast
+apply auto[1]
+apply (meson L_flat_Prf2)
+(* SEQ *)
+apply(auto simp add: CPT_def)[1]
+apply(erule CPrf.cases)
+apply(simp_all)
+apply(rule Posix.intros)
+apply(drule_tac x="flat v1a" in meta_spec)
+apply(drule_tac x="v1a" in meta_spec)
+apply(drule meta_mp)
+apply(simp)
+apply(drule meta_mp)
+apply(auto)[1]
+apply(auto simp add: PT_def)[1]
+apply(drule_tac x="Seq v2a v2" in spec)
+apply(simp)
+apply(drule mp)
+apply (simp add: Prf.intros(1) Prf_CPrf)
+using val_ord_SEQI val_ord_ex_def apply fastforce
+apply(assumption)
+apply(rotate_tac 1)
+apply(drule_tac x="flat v2" in meta_spec)
+apply(drule_tac x="v2" in meta_spec)
+apply(simp)
+apply(auto)[1]
+apply(drule meta_mp)
+apply(auto)[1]
+apply(auto simp add: PT_def)[1]
+apply(drule_tac x="Seq v1a v2a" in spec)
+apply(simp)
+apply(drule mp)
+apply (simp add: Prf.intros(1) Prf_CPrf)
+apply (meson val_ord_SEQI2 val_ord_ex_def)
+apply(assumption)
+(* SEQ side condition *)
+apply(auto simp add: PT_def)
+apply(subgoal_tac "\<exists>vA. flat vA = flat v1a @ s\<^sub>3 \<and> \<turnstile> vA : r1a")
+prefer 2
+apply (meson L_flat_Prf2)
+apply(subgoal_tac "\<exists>vB. flat vB = s\<^sub>4 \<and> \<turnstile> vB : r2a")
+prefer 2
+apply (meson L_flat_Prf2)
+apply(clarify)
+apply(drule_tac x="Seq vA vB" in spec)
+apply(simp)
+apply(drule mp)
+apply (simp add: Prf.intros(1))
+apply(subst (asm) (3) val_ord_ex_def)
+apply (metis append_Nil2 append_assoc append_eq_conv_conj flat.simps(5) length_append not_add_less1 not_less_iff_gr_or_eq val_ord_SEQI val_ord_ex_def val_ord_shorterI)
+(* STAR *)
 
 
 definition Minval :: "rexp \<Rightarrow> string \<Rightarrow> val \<Rightarrow> bool"