--- a/thys/Sulzmann.thy	Fri Jun 23 00:27:53 2017 +0100
+++ b/thys/Sulzmann.thy	Sat Jun 24 18:50:26 2017 +0100
@@ -164,6 +164,13 @@
 by (metis diff_Suc_1 less_Suc_eq_0_disj nth_Cons')
 
 
+lemma pflat_len_Stars_simps2:
+  shows "pflat_len (Stars (v#vs)) (Suc n # p) = pflat_len (Stars vs) (n#p)"
+  and   "pflat_len (Stars (v#vs)) (0 # p) = pflat_len v p"
+using assms 
+apply(simp_all add: pflat_len_def)
+done
+
 lemma Two_to_Three_aux:
   assumes "p \<in> Pos v1 \<union> Pos v2" "pflat_len v1 p = pflat_len v2 p"
   shows "p \<in> Pos v1 \<inter> Pos v2"
@@ -562,9 +569,6 @@
 apply (simp add: intlen_length)
 apply(simp)
 done
-
-
-
 lemma val_ord_ALTI:
   assumes "v \<sqsubset>val p v'" "flat v = flat v'"
   shows "(Left v) \<sqsubset>val (0#p) (Left v')" 
@@ -605,6 +609,24 @@
 apply(auto simp add: pflat_len_simps)[2]
 done
 
+lemma val_ord_ALTE:
+  assumes "(Left v1) \<sqsubset>val (p # ps) (Left v2)"
+  shows "p = 0 \<and> v1 \<sqsubset>val ps v2"
+using assms(1)
+apply(simp add: val_ord_def)
+apply(auto simp add: pflat_len_simps)
+apply (metis (no_types, hide_lams) assms lex_lists.intros(2) outside_lemma pflat_len_simps(3) val_ord_def)
+by (metis (no_types, hide_lams) assms lex_lists.intros(2) outside_lemma pflat_len_simps(3) val_ord_def)
+
+lemma val_ord_ALTE2:
+  assumes "(Right v1) \<sqsubset>val (p # ps) (Right v2)"
+  shows "p = 1 \<and> v1 \<sqsubset>val ps v2"
+using assms(1)
+apply(simp add: val_ord_def)
+apply(auto simp add: pflat_len_simps)
+apply (metis (no_types, hide_lams) assms lex_lists.intros(2) outside_lemma pflat_len_simps(5) val_ord_def)
+by (metis (no_types, hide_lams) assms lex_lists.intros(2) outside_lemma pflat_len_simps(5) val_ord_def)
+
 lemma val_ord_STARI:
   assumes "v1 \<sqsubset>val p v2" "flat (Stars (v1#vs1)) = flat (Stars (v2#vs2))"
   shows "(Stars (v1#vs1)) \<sqsubset>val (0#p) (Stars (v2#vs2))" 
@@ -832,6 +854,7 @@
 apply(simp add: pflat_len_simps)
 done
 
+
 lemma val_ord_ex_trans:
   assumes "v1 :\<sqsubset>val v2" "v2 :\<sqsubset>val v3"
   shows "v1 :\<sqsubset>val v3"
@@ -1061,50 +1084,6 @@
 
 
 
-lemma CPTpre_test:
-  assumes "s \<in> r \<rightarrow> v"
-  shows "\<not>(\<exists>v' \<in> CPT r s. v :\<sqsubset>val v')"
-using assms
-apply(induct r arbitrary: s v rule: rexp.induct)
-apply(erule Posix.cases)
-apply(simp_all)
-apply(erule Posix.cases)
-apply(simp_all)
-apply(simp add: CPT_simps)
-apply(simp add: val_ord_def val_ord_ex_def)
-apply(erule Posix.cases)
-apply(simp_all)
-apply(simp add: CPT_simps)
-apply (simp add: val_ord_def val_ord_ex_def)
-(* SEQ *)
-apply(rule ballI)
-apply(erule Posix.cases)
-apply(simp_all)
-apply(clarify)
-apply(subst (asm) CPT_simps)
-apply(simp)
-apply(clarify)
-thm val_ord_SEQ
-apply(drule_tac ?r="r1" in val_ord_SEQ)
-apply(simp)
-apply (simp add: CPT_def Posix1(2))
-apply (simp add: Posix1a)
-apply (simp add: CPT_def Posix1a)
-using Prf_CPrf apply auto[1]
-apply(erule disjE)
-apply(drule_tac x="s1" in meta_spec)
-apply(drule_tac x="v1" in meta_spec)
-apply(simp)
-apply(drule_tac x="v1a" in bspec)
-apply(subgoal_tac "s1 = s1a")
-apply(simp)
-apply(auto simp add: append_eq_append_conv2)[1]
-apply (metis (mono_tags, lifting) CPT_def L_flat_Prf1 Prf_CPrf append_Nil append_Nil2 mem_Collect_eq)
-apply(simp add: CPT_def)
-apply(auto)[1]
-oops
-
-
 lemma test: 
   assumes "finite A"
   shows "finite {vs. Stars vs \<in> A}"
@@ -1414,6 +1393,225 @@
 apply(simp add: CPTpre_def CPT_def)
 done
 
+
+lemma STAR_val_ord:
+  assumes "Stars (v1 # vs1) \<sqsubset>val (Suc p # ps) Stars (v2 # vs2)" "flat v1 = flat v2"
+  shows "(Stars vs1) \<sqsubset>val (p # ps) (Stars vs2)"
+using assms(1,2)
+apply -
+apply(simp(no_asm)  add: val_ord_def)
+apply(rule conjI)
+apply(simp add: val_ord_def)
+apply(rule conjI)
+apply(simp add: val_ord_def)
+apply(auto simp add: pflat_len_simps pflat_len_Stars_simps2)[1]
+apply(rule ballI)
+apply(rule impI)
+apply(simp add: val_ord_def pflat_len_simps pflat_len_Stars_simps2 intlen_append)
+apply(clarify)
+apply(case_tac q)
+apply(simp add: val_ord_def pflat_len_simps pflat_len_Stars_simps2 intlen_append)
+apply(clarify)
+apply(erule disjE)
+prefer 2
+apply(drule_tac x="Suc a # list" in bspec)
+apply(simp)
+apply(drule mp)
+apply(simp)
+apply(simp add: val_ord_def pflat_len_simps pflat_len_Stars_simps2 intlen_append)
+apply(drule_tac x="Suc a # list" in bspec)
+apply(simp)
+apply(drule mp)
+apply(simp)
+apply(simp add: val_ord_def pflat_len_simps pflat_len_Stars_simps2 intlen_append)
+done
+
+
+lemma Posix_val_ord_reverse:
+  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 *)
+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(simp)
+(* HERE *)
+apply(case_tac "flat va = s1")
+prefer 2
+apply(subgoal_tac "v :\<sqsubset>val va")
+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)
+apply(simp)
+prefer 2
+apply(simp)
+apply(drule_tac x="va" in spec)
+apply(simp)
+apply(subst (asm) (2) val_ord_ex_def)
+apply(subst (asm) (2) val_ord_ex_def)
+apply(clarify)
+apply(simp)
+apply(drule_tac x="Stars vsa" in spec)
+apply(simp)
+apply(case_tac p)
+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(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  
+
+
 definition Minval :: "rexp \<Rightarrow> string \<Rightarrow> val \<Rightarrow> bool"
   where
   "Minval r s v \<equiv> \<Turnstile> v : r \<and> flat v = s \<and> (\<forall>v' \<in> CPT r s. v :\<sqsubset>val v' \<or> v = v')"