--- a/thys/Sulzmann.thy	Sun Jun 25 12:44:01 2017 +0100
+++ b/thys/Sulzmann.thy	Mon Jun 26 17:43:28 2017 +0100
@@ -569,6 +569,19 @@
 apply (simp add: intlen_length)
 apply(simp)
 done
+
+lemma val_ord_spre:
+  assumes "(flat v') \<sqsubset>spre (flat v)"
+  shows "v :\<sqsubset>val v'" 
+using assms(1)
+apply(rule_tac val_ord_shorterI)
+apply(simp add: sprefix_list_def prefix_list_def)
+apply(auto)
+apply(case_tac ps')
+apply(auto)
+by (metis append_eq_conv_conj drop_all le_less_linear neq_Nil_conv)
+
+
 lemma val_ord_ALTI:
   assumes "v \<sqsubset>val p v'" "flat v = flat v'"
   shows "(Left v) \<sqsubset>val (0#p) (Left v')" 
@@ -1434,40 +1447,234 @@
 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"
+thm Posix.intros(6)
+
+inductive Prop :: "rexp \<Rightarrow> val list \<Rightarrow> bool"
+where
+  "Prop r []"
+| "\<lbrakk>Prop r vs; 
+    \<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = concat (map flat vs) \<and> flat v @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (STAR r))\<rbrakk> 
+   \<Longrightarrow> Prop r (v # vs)"
+
+lemma STAR_val_ord_ex:
+  assumes "Stars (v # vs1) :\<sqsubset>val Stars (v # vs2)"
+  shows "Stars vs1 :\<sqsubset>val Stars vs2"
 using assms
-apply(induct vs) 
-apply(auto intro: CPrf.intros)
-a
+apply(subst (asm) val_ord_ex_def)
+apply(erule exE)
+apply(case_tac p)
+apply(simp)
+apply(simp add: val_ord_def pflat_len_simps intlen_append)
+apply(subst val_ord_ex_def)
+apply(rule_tac x="[]" in exI)
+apply(simp add: val_ord_def pflat_len_simps Pos_empty)
+apply(simp)
+apply(case_tac a)
+apply(clarify)
+prefer 2
+using STAR_val_ord val_ord_ex_def apply blast
+apply(auto simp add: pflat_len_Stars_simps2 val_ord_def pflat_len_def)[1]
+done
 
-lemma L_flat_CPrf:
-  assumes "s \<in> L r" 
-  shows "\<exists>v. \<Turnstile> v : r \<and> flat v = s"
+lemma STAR_val_ord_exI:
+  assumes "Stars vs1 :\<sqsubset>val Stars vs2" "flat (Stars vs1) = flat (Stars vs2)"
+  shows "Stars (vs @ vs1) :\<sqsubset>val Stars (vs @ vs2)"
 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(rule_tac x="Stars vs" in exI)
+apply(induct vs)
+apply(simp)
+apply(simp)
+apply(simp add: val_ord_ex_def)
+apply(erule exE)
+apply(case_tac p)
+apply(simp)
+apply(rule_tac x="[]" in exI)
+apply(simp add: val_ord_def)
+apply(auto simp add: pflat_len_simps intlen_append)[1]
+apply(simp)
+apply(rule_tac x="Suc aa#list" in exI)
+apply(rule val_ord_STARI2)
+apply(simp)
 apply(simp)
-(* HERE *)
-apply (simp add: Prf_Stars)
-apply(drule Star_string)
-apply(auto)
-apply(rule Star_val)
+done
+
+lemma STAR_val_ord_ex_append:
+  assumes "Stars (vs @ vs1) :\<sqsubset>val Stars (vs @ vs2)"
+  shows "Stars vs1 :\<sqsubset>val Stars vs2"
+using assms
+apply(induct vs)
+apply(simp)
+apply(simp)
+apply(drule STAR_val_ord_ex)
+apply(simp)
+done
+
+lemma STAR_val_ord_ex_append_eq:
+  assumes "flat (Stars vs1) = flat (Stars vs2)"
+  shows "Stars (vs @ vs1) :\<sqsubset>val Stars (vs @ vs2) \<longleftrightarrow> Stars vs1 :\<sqsubset>val Stars vs2"
+using assms
+apply(rule_tac iffI)
+apply(erule STAR_val_ord_ex_append)
+apply(rule STAR_val_ord_exI)
 apply(auto)
 done
-*)
+
+lemma Posix_STARI:
+  assumes "\<forall>v \<in> set vs. flat v \<noteq> [] \<and> (flat v) \<in> r \<rightarrow> v" "Prop r vs"
+  shows "flat (Stars vs) \<in> STAR r \<rightarrow> Stars vs"
+using assms
+apply(induct vs arbitrary: r)
+apply(simp)
+apply(rule Posix.intros)
+apply(simp)
+apply(rule Posix.intros)
+apply(simp)
+apply(auto)[1]
+apply(erule Prop.cases)
+apply(simp)
+apply(simp)
+apply(simp)
+apply(erule Prop.cases)
+apply(simp)
+apply(auto)[1]
+done
+
+lemma CPrf_stars:
+  assumes "\<Turnstile> Stars vs : STAR r"
+  shows "\<forall>v \<in> set vs. flat v \<noteq> [] \<and> \<Turnstile> v : r"
+using assms
+apply(induct vs)
+apply(auto)
+apply(erule CPrf.cases)
+apply(simp_all)
+apply(erule CPrf.cases)
+apply(simp_all)
+apply(erule CPrf.cases)
+apply(simp_all)
+apply(erule CPrf.cases)
+apply(simp_all)
+done
 
 definition PT :: "rexp \<Rightarrow> string \<Rightarrow> val set"
 where "PT r s \<equiv> {v. flat v = s \<and> \<turnstile> v : r}"
 
+lemma exists:
+  assumes "s \<in> (L r)\<star>"
+  shows "\<exists>vs. concat (map flat vs) = s \<and> \<turnstile> Stars vs : STAR r"
+using assms
+apply(drule_tac Star_string)
+apply(auto)
+by (metis L_flat_Prf2 Prf_Stars Star_val)
+
+
+lemma val_ord_Posix_Stars:
+  assumes "(Stars vs) \<in> CPT (STAR r) (flat (Stars vs))" "\<forall>v \<in> set vs. flat v \<in> r \<rightarrow> v"
+  and "\<not>(\<exists>vs2 \<in> PT (STAR r) (flat (Stars vs)). vs2 :\<sqsubset>val (Stars vs))"
+  shows "(flat (Stars vs)) \<in> (STAR r) \<rightarrow> Stars vs" 
+using assms
+apply(induct vs)
+apply(simp)
+apply(rule Posix.intros)
+apply(simp (no_asm))
+apply(rule Posix.intros)
+apply(auto)[1]
+apply(auto simp add: CPT_def PT_def)[1]
+defer
+apply(simp)
+apply(drule meta_mp)
+apply(auto simp add: CPT_def PT_def)[1]
+apply(erule CPrf.cases)
+apply(simp_all)
+apply(drule meta_mp)
+apply(auto simp add: CPT_def PT_def)[1]
+apply(erule Prf.cases)
+apply(simp_all)
+apply (metis CPrf_stars Cons_eq_map_conv Posix_CPT Posix_STAR2 Posix_val_ord_reverse list.exhaust list.set_intros(2) map_idI val.distinct(25))
+apply(clarify)
+apply(drule_tac x="Stars (a#v#vsa)" in spec)
+apply(simp)
+apply(drule mp)
+apply (meson CPrf_stars Prf.intros(7) Prf_CPrf list.set_intros(1))
+apply(subst (asm) (2) val_ord_ex_def)
+apply(simp)
+apply (metis flat.simps(7) flat_Stars intlen.cases not_less_iff_gr_or_eq pflat_len_simps(7) val_ord_STARI2 val_ord_def val_ord_ex_def)
+apply(auto simp add: CPT_def PT_def)[1]
+using CPrf_stars apply auto[1]
+apply(auto)[1]
+apply(auto simp add: CPT_def PT_def)[1]
+apply(subgoal_tac "\<exists>vA. flat vA = flat a @ s\<^sub>3 \<and> \<turnstile> vA : r")
+prefer 2
+apply (meson L_flat_Prf2)
+apply(subgoal_tac "\<exists>vB. flat (Stars vB) = s\<^sub>4 \<and> \<turnstile> (Stars vB) : (STAR r)")
+apply(clarify)
+apply(drule_tac x="Stars (vA # vB)" in spec)
+apply(simp)
+apply(drule mp)
+using Prf.intros(7) apply blast
+apply(subst (asm) (2) val_ord_ex_def)
+apply(simp)
+prefer 2
+apply(simp)
+using exists apply blast
+prefer 2
+apply(drule meta_mp)
+apply(erule CPrf.cases)
+apply(simp_all)
+apply(drule meta_mp)
+apply(auto)[1]
+prefer 2
+apply(simp)
+apply(erule CPrf.cases)
+apply(simp_all)
+apply(clarify)
+apply(rotate_tac 3)
+apply(erule Prf.cases)
+apply(simp_all)
+apply (metis CPrf_stars intlen.cases less_irrefl list.set_intros(1) val_ord_def val_ord_ex_def)
+apply(drule_tac x="Stars (v#va#vsb)" in spec)
+apply(drule mp)
+apply (simp add: Posix1a Prf.intros(7))
+apply(simp)
+apply(subst (asm) (2) val_ord_ex_def)
+apply(simp)
+apply (metis flat.simps(7) flat_Stars intlen.cases not_less_iff_gr_or_eq pflat_len_simps(7) val_ord_STARI2 val_ord_def val_ord_ex_def)
+proof -
+  fix a :: val and vsa :: "val list" and s\<^sub>3 :: "char list" and vA :: val and vB :: "val list"
+  assume a1: "s\<^sub>3 \<noteq> []"
+  assume a2: "s\<^sub>3 @ concat (map flat vB) = concat (map flat vsa)"
+  assume a3: "flat vA = flat a @ s\<^sub>3"
+  assume a4: "\<forall>p. \<not> Stars (vA # vB) \<sqsubset>val p Stars (a # vsa)"
+  have f5: "\<And>n cs. drop n (cs::char list) = [] \<or> n < length cs"
+    by (meson drop_eq_Nil not_less)
+  have f6: "\<not> length (flat vA) \<le> length (flat a)"
+    using a3 a1 by simp
+  have "flat (Stars (a # vsa)) = flat (Stars (vA # vB))"
+    using a3 a2 by simp
+  then show False
+    using f6 f5 a4 by (metis (full_types) drop_eq_Nil val_ord_STARI val_ord_ex_def val_ord_shorterI)
+qed
+
+lemma Prf_Stars_append:
+  assumes "\<turnstile> Stars vs1 : STAR r" "\<turnstile> Stars vs2 : STAR r"
+  shows "\<turnstile> Stars (vs1 @ vs2) : STAR r"
+using assms
+apply(induct vs1 arbitrary: vs2)
+apply(auto intro: Prf.intros)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(auto intro: Prf.intros)
+done
+
+lemma CPrf_Stars_appendE:
+  assumes "\<Turnstile> Stars (vs1 @ vs2) : STAR r"
+  shows "\<Turnstile> Stars vs1 : STAR r \<and> \<Turnstile> Stars vs2 : STAR r" 
+using assms
+apply(induct vs1 arbitrary: vs2)
+apply(auto intro: CPrf.intros)[1]
+apply(erule CPrf.cases)
+apply(simp_all)
+apply(auto intro: CPrf.intros)
+done
+
 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" 
@@ -1594,61 +1801,64 @@
 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"
-  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')"   
-
-lemma 
-  assumes "s \<in> L(r)"
-  shows "\<exists>v. Minval r s v"
-using assms
-apply(induct r arbitrary: s)
-apply(simp)
-apply(simp)
-apply(rule_tac x="Void" in exI)
-apply(simp add: Minval_def)
-apply(rule conjI)
-apply (simp add: CPrf.intros(4))
-apply(clarify)
-apply(simp add: CPT_def)
-apply(auto)[1]
+apply(auto simp add: CPT_def)[1]
 apply(erule CPrf.cases)
-apply(simp_all)
-apply(rule_tac x="Char x" in exI)
-apply(simp add: Minval_def)
-apply(rule conjI)
-apply (simp add: CPrf.intros)
+apply(simp_all)[6]
+using Posix_STAR2 apply blast
 apply(clarify)
-apply(simp add: CPT_def)
+apply(rule val_ord_Posix_Stars)
+apply(auto simp add: CPT_def)[1]
+apply (simp add: CPrf.intros(7))
+apply(auto)[1]
+apply(drule_tac x="flat v" in meta_spec)
+apply(drule_tac x="v" in meta_spec)
+apply(simp)
+apply(drule meta_mp)
 apply(auto)[1]
-apply(erule CPrf.cases)
-apply(simp_all)
+apply(drule_tac x="Stars (v2#vs)" in spec)
+apply(simp)
+apply(drule mp)
+using Prf.intros(7) Prf_CPrf apply blast
+apply(subst (asm) (2) val_ord_ex_def)
+apply(simp)
+using val_ord_STARI val_ord_ex_def apply fastforce
+apply(assumption)
+apply(drule_tac x="flat va" in meta_spec)
+apply(drule_tac x="va" in meta_spec)
+apply(simp)
+apply(drule meta_mp)
+using CPrf_stars apply blast
+apply(drule meta_mp)
+apply(auto)[1]
+apply(subgoal_tac "\<exists>pre post. vs = pre @ [va] @ post")
 prefer 2
-apply(auto)[1]
-apply(drule_tac x="s" in meta_spec) 
-apply(simp)
+apply (metis append_Cons append_Nil in_set_conv_decomp_first)
 apply(clarify)
-apply(rule_tac x="Left x" in exI)
-apply(simp (no_asm) add: Minval_def)
-apply(rule conjI)
-apply (simp add: CPrf.intros(2) Minval_def)
-apply(rule conjI)
-apply(simp add: Minval_def)
-apply(clarify)
-apply(simp add: CPT_def)
-apply(auto)[1]
-apply(erule CPrf.cases)
-apply(simp_all)
+apply(drule_tac x="Stars (v#(pre @ [v2] @ post))" in spec)
+apply(simp)
+apply(drule mp)
+apply(rule Prf.intros)
+apply (simp add: Prf_CPrf)
+apply(rule Prf_Stars_append)
+apply(drule CPrf_Stars_appendE)
+apply(auto simp add: Prf_CPrf)[1]
+apply (metis CPrf_Stars_appendE CPrf_stars Prf_CPrf Prf_Stars list.set_intros(2) set_ConsD)
+apply(subgoal_tac "\<not> Stars ([v] @ pre @ v2 # post) :\<sqsubset>val Stars ([v] @ pre @ va # post)")
+apply(subst (asm) STAR_val_ord_ex_append_eq)
+apply(simp)
+apply(subst (asm) STAR_val_ord_ex_append_eq)
+apply(simp)
+prefer 2
+apply(simp)
+prefer 2
+apply(simp)
 apply(simp add: val_ord_ex_def)
-apply(simp only: val_ord_def)
-oops
-
-lemma
-  "wf {(v1, v2). v1 \<in> CPT r s \<and> v2 \<in> CPT r s \<and> (v1 :\<sqsubset>val v2)}"
-apply(rule wfI)
-oops
+apply(erule exE)
+apply(rotate_tac 6)
+apply(drule_tac x="0#p" in spec)
+apply (simp add: val_ord_STARI)
+apply(auto simp add: PT_def)
+done
 
 inductive ValOrd :: "val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<preceq>_ _" [100, 100, 100] 100)
 where
@@ -1662,10 +1872,12 @@
 | K2: "flat (Stars (v # vs)) \<noteq> [] \<Longrightarrow> (Stars (v # vs)) \<preceq>(STAR r) (Stars [])"
 | K3: "v1 \<preceq>r v2 \<Longrightarrow> (Stars (v1 # vs1)) \<preceq>(STAR r) (Stars (v2 # vs2))"
 | K4: "(Stars vs1) \<preceq>(STAR r) (Stars vs2) \<Longrightarrow> (Stars (v # vs1)) \<preceq>(STAR r) (Stars (v # vs2))"
-| MY1: "Void \<preceq>ONE Void" 
+(*| MY1: "Void \<preceq>ONE Void" 
 | MY2: "(Char c) \<preceq>(CHAR c) (Char c)" 
 | MY3: "(Stars []) \<preceq>(STAR r) (Stars [])" 
+*)
 
+(*
 lemma ValOrd_refl: 
   assumes "\<turnstile> v : r" 
   shows "v \<preceq>r v"
@@ -1683,12 +1895,132 @@
 apply(rule ValOrd.intros)
 apply(simp)
 done
+*)
+
+lemma ValOrd_irrefl: 
+  assumes "\<turnstile> v : r"  "v \<preceq>r v" 
+  shows "False"
+using assms
+apply(induct v r rule: Prf.induct)
+apply(erule ValOrd.cases)
+apply(simp_all)
+apply(erule ValOrd.cases)
+apply(simp_all)
+apply(erule ValOrd.cases)
+apply(simp_all)
+apply(erule ValOrd.cases)
+apply(simp_all)
+apply(erule ValOrd.cases)
+apply(simp_all)
+apply(erule ValOrd.cases)
+apply(simp_all)
+apply(erule ValOrd.cases)
+apply(simp_all)
+done
+
+lemma prefix_sprefix:
+  shows "xs \<sqsubseteq>pre ys \<longleftrightarrow> (xs = ys \<or> xs \<sqsubset>spre ys)"
+apply(auto simp add: sprefix_list_def prefix_list_def)
+done
+
+
 
 lemma Posix_CPT2:
-  assumes "v1 \<preceq>r v2" "flat v1 = flat v2"
-  shows "v2 :\<sqsubset>val v1 \<or> v1 = v2" 
+  assumes "v1 \<preceq>r v2" "flat v2 \<sqsubseteq>pre flat v1"
+  shows "v1 :\<sqsubset>val v2" 
 using assms
-apply(induct r arbitrary: v1 v2 rule: rexp.induct)
+apply(induct v1 r v2 arbitrary: rule: ValOrd.induct)
+prefer 3
+apply(simp)
+apply(auto simp add: prefix_sprefix)[1]
+apply(rule val_ord_spre)
+apply(simp)
+prefer 3
+apply(simp)
+apply(auto simp add: prefix_sprefix)[1]
+apply(auto simp add: val_ord_ex_def)[1]
+apply(rule_tac x="[0]" in exI)
+apply(auto simp add: val_ord_def Pos_empty pflat_len_simps)[1]
+apply (smt inlen_bigger)
+apply(rule val_ord_spre)
+apply(simp)
+prefer 3
+apply(simp)
+apply(auto simp add: prefix_sprefix)[1]
+using val_ord_ALTI2 val_ord_ex_def apply fastforce
+apply(rule val_ord_spre)
+apply(simp)
+prefer 3
+apply(simp)
+apply(auto simp add: prefix_sprefix)[1]
+using val_ord_ALTI val_ord_ex_def apply fastforce
+apply(rule val_ord_spre)
+apply(simp)
+(* SEQ case *)
+apply(simp)
+apply(auto simp add: prefix_sprefix)[1]
+apply(auto simp add: append_eq_append_conv2)[1]
+apply(case_tac "us = []")
+apply(simp)
+apply(auto simp add: val_ord_ex1_def)[1]
+apply (metis flat.simps(5) val_ord_SEQI val_ord_ex_def)
+apply(simp)
+prefer 2
+apply(case_tac "us = []")
+apply(simp)
+apply (metis flat.simps(5) val_ord_SEQI val_ord_ex_def)
+apply(drule meta_mp)
+apply(rule disjI2)
+apply (metis append_self_conv prefix_list_def sprefix_list_def)
+apply(auto simp add: val_ord_ex_def)[1]
+apply (metis append_assoc flat.simps(5) val_ord_SEQI)
+
+apply(sugoal_ tac "")
+thm val_ord_SEQI
+apply(rule val_ord_SEQI)
+thm val_ord_SEQI
+prefer 2
+apply(case_tac "us
+apply(case_tac "v1 = v1'")
+apply(simp)
+
+apply(auto simp add: val_ord_ex1_def)[1]
+apply(auto simp add: val_ord_ex_def)[1]
+apply(rule_tac x="[0]" in exI)
+
+prefer 2
+apply(rule val_ord_spre)
+apply(simp)
+prefer 3
+apply(simp)
+using val_ord_ex1_def val_ord_spre apply auto[1]
+
+apply(erule disjE)
+prefer 2
+apply(subst val_ord_ex1_def)
+apply(rule disjI1)
+apply(rule val_ord_spre)
+apply(simp)
+apply(simp)
+apply(simp add: append_eq_append_conv2)
+apply(auto)[1]
+apply(case_tac "us = []")
+apply(simp)
+apply(drule meta_mp)
+apply(auto simp add: prefix_sprefix)[1]
+apply(subst (asm) val_ord_ex1_def)
+apply(erule disjE)
+apply(subst val_ord_ex1_def)
+apply(rule disjI1)
+apply (metis flat.simps(5) val_ord_SEQI val_ord_ex_def)
+apply(clarify)
+prefer 2
+apply(subgoal_tac "flat v1' \<sqsubset>spre flat v1")
+prefer 2
+apply (simp add: prefix_list_def sprefix_list_def)
+apply(drule val_ord_spre)
+apply(auto)[1]
+apply(rule val_ord_sprefixI)
 apply(erule ValOrd.cases)
 apply(simp_all)
 apply(erule ValOrd.cases)