diff -r f46ebc84408d -r f16019b11179 thys/Positions.thy
--- a/thys/Positions.thy	Fri Aug 25 23:54:10 2017 +0200
+++ b/thys/Positions.thy	Sun Aug 27 00:03:31 2017 +0300
@@ -739,249 +739,24 @@
 by (metis Posix_PosOrd less_irrefl PosOrd_def 
     PosOrd_ex_eq_def PosOrd_ex_def PosOrd_trans)
 
-
-
-lemma PosOrd_Posix_Stars:
-  assumes "\<forall>v \<in> set vs. flat v \<in> r \<rightarrow> v \<and> flat v \<noteq> []"
-  and "\<not>(\<exists>vs2 \<in> LV (STAR r) (flat (Stars vs)). vs2 :\<sqsubset>val (Stars vs))"
-  shows "(flat (Stars vs)) \<in> (STAR r) \<rightarrow> Stars vs" 
-using assms
-proof(induct vs)
-  case Nil
-  show "flat (Stars []) \<in> STAR r \<rightarrow> Stars []"
-    by(simp add: Posix.intros)
-next
-  case (Cons v vs)
-  have IH: "\<lbrakk>\<forall>v\<in>set vs. flat v \<in> r \<rightarrow> v \<and> flat v \<noteq> []; 
-             \<not> (\<exists>vs2\<in>LV (STAR r) (flat (Stars vs)). vs2 :\<sqsubset>val Stars vs)\<rbrakk>
-             \<Longrightarrow> flat (Stars vs) \<in> STAR r \<rightarrow> Stars vs" by fact
-  have as2: "\<forall>v\<in>set (v # vs). flat v \<in> r \<rightarrow> v \<and> flat v \<noteq> []" by fact
-  have as3: "\<not> (\<exists>vs2\<in>LV (STAR r) (flat (Stars (v # vs))). vs2 :\<sqsubset>val Stars (v # vs))" by fact
-  have "flat v \<in> r \<rightarrow> v" "flat v \<noteq> []" using as2 by auto
-  moreover
-  have  "flat (Stars vs) \<in> STAR r \<rightarrow> Stars vs" 
-    proof (rule IH)
-      show "\<forall>v\<in>set vs. flat v \<in> r \<rightarrow> v \<and> flat v \<noteq> []" using as2 by simp
-    next 
-      show "\<not> (\<exists>vs2\<in>LV (STAR r) (flat (Stars vs)). vs2 :\<sqsubset>val Stars vs)" using as3
-        apply(auto)
-        apply(subst (asm) (2) LV_def)
-        apply(auto)
-        apply(erule Prf.cases)
-        apply(simp_all)
-        apply(drule_tac x="Stars (v # vs)" in bspec)
-        apply(simp add: LV_def)
-        using Posix_LV Prf.intros(6) calculation
-        apply(rule_tac Prf.intros)
-        apply(simp add:)
-        prefer 2
-        apply (simp add: PosOrd_StarsI2)
-        apply(drule Posix_LV) 
-        apply(simp add: LV_def)
-        done
-    qed
-  moreover
-  have "flat v \<noteq> []" using as2 by simp
-  moreover
-  have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = flat (Stars vs) \<and> flat v @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (STAR r))" 
-   using as3
-   apply(auto)
-   apply(drule L_flat_Prf2)
-   apply(erule exE)
-   apply(simp only: L.simps[symmetric])
-   apply(drule L_flat_Prf2)
-   apply(erule exE)
-   apply(clarify)
-   apply(rotate_tac 5)
-   apply(erule Prf.cases)
-   apply(simp_all)
-   apply(clarify)
-   apply(drule_tac x="Stars (va#vs)" in bspec)
-   apply(auto simp add: LV_def)[1]   
-   apply(rule Prf.intros)
-   apply(simp)
-   by (simp add: PosOrd_StarsI PosOrd_shorterI)
-  ultimately show "flat (Stars (v # vs)) \<in> STAR r \<rightarrow> Stars (v # vs)"
-  by (simp add: Posix.intros)
-qed
-
-
-
-section {* The Smallest Value is indeed the Posix Value *}
-
 lemma PosOrd_Posix:
   assumes "v1 \<in> LV r s" "\<forall>v\<^sub>2 \<in> LV r s. \<not> v\<^sub>2 :\<sqsubset>val v1"
   shows "s \<in> r \<rightarrow> v1" 
-using assms
-proof(induct r arbitrary: s v1)
-  case (ZERO s v1)
-  have "v1 \<in> LV ZERO s" by fact
-  then show "s \<in> ZERO \<rightarrow> v1" unfolding LV_def
-    by (auto elim: Prf.cases)
-next 
-  case (ONE s v1)
-  have "v1 \<in> LV ONE s" by fact
-  then have "v1 = Void" "s = []" unfolding LV_def
-    by(auto elim: Prf.cases)
-  then show "s \<in> ONE \<rightarrow> v1" 
-    by(auto intro: Posix.intros)
-next 
-  case (CHAR c s v1)
-  have "v1 \<in> LV (CHAR c) s" by fact
-  then show "s \<in> CHAR c \<rightarrow> v1" unfolding LV_def
-    by (auto elim!: Prf.cases intro: Posix.intros)
-next
-  case (ALT r1 r2 s v1)
-  have IH1: "\<And>s v1. \<lbrakk>v1 \<in> LV r1 s; \<forall>v2 \<in> LV r1 s. \<not> v2 :\<sqsubset>val v1\<rbrakk> \<Longrightarrow> s \<in> r1 \<rightarrow> v1" by fact
-  have IH2: "\<And>s v1. \<lbrakk>v1 \<in> LV r2 s; \<forall>v2 \<in> LV r2 s. \<not> v2 :\<sqsubset>val v1\<rbrakk> \<Longrightarrow> s \<in> r2 \<rightarrow> v1" by fact
-  have as1: "\<forall>v2 \<in> LV (ALT r1 r2) s. \<not> v2 :\<sqsubset>val v1" by fact
-  have as2: "v1 \<in> LV (ALT r1 r2) s" by fact
-  then consider 
-     (Left) v1' where
-        "v1 = Left v1'" "s = flat v1'"
-        "v1' \<in> LV r1 s"
-  |  (Right) v1' where
-        "v1 = Right v1'" "s = flat v1'"
-        "v1' \<in> LV r2 s"
-  unfolding LV_def by (auto elim: Prf.cases)
-  then show "s \<in> ALT r1 r2 \<rightarrow> v1"
-   proof (cases)
-     case (Left v1')
-     have "v1' \<in> LV r1 s" using Left(3) .
-     moreover
-     have "\<forall>v2 \<in> LV r1 s. \<not> v2 :\<sqsubset>val v1'" using as1
-       unfolding Left(1,2) unfolding LV_def 
-       using Prf.intros(2) PosOrd_Left_eq by force  
-     ultimately have "s \<in> r1 \<rightarrow> v1'" using IH1 by simp
-     then have "s \<in> ALT r1 r2 \<rightarrow> Left v1'" by (rule Posix.intros)
-     then show "s \<in> ALT r1 r2 \<rightarrow> v1" using Left by simp
-   next
-     case (Right v1')
-     have "v1' \<in> LV r2 s" using Right(3) .
-     moreover
-     have "\<forall>v2 \<in> LV r2 s. \<not> v2 :\<sqsubset>val v1'" using as1
-       unfolding LV_def Right using Prf.intros(3) PosOrd_RightI by force   
-     ultimately have "s \<in> r2 \<rightarrow> v1'" using IH2 by simp
-     moreover 
-       { assume "s \<in> L r1"
-         then obtain v' where "v' \<in>  LV r1 s"
-            unfolding LV_def using L_flat_Prf2 by blast
-         then have "Left v' \<in>  LV (ALT r1 r2) s" 
-            unfolding LV_def by (auto intro: Prf.intros)
-         with as1 have "\<not> (Left v' :\<sqsubset>val Right v1') \<and> (flat v' = s)" 
-            unfolding LV_def Right 
-            by (auto)
-         then have False using PosOrd_Left_Right Right by blast  
-       }
-     then have "s \<notin> L r1" by rule 
-     ultimately have "s \<in> ALT r1 r2 \<rightarrow> Right v1'" by (rule Posix.intros)
-     then show "s \<in> ALT r1 r2 \<rightarrow> v1" using Right by simp
-  qed
-next 
-  case (SEQ r1 r2 s v1)
-  have IH1: "\<And>s v1. \<lbrakk>v1 \<in> LV r1 s; \<forall>v2 \<in> LV r1 s. \<not> v2 :\<sqsubset>val v1\<rbrakk> \<Longrightarrow> s \<in> r1 \<rightarrow> v1" by fact
-  have IH2: "\<And>s v1. \<lbrakk>v1 \<in> LV r2 s; \<forall>v2 \<in> LV r2 s. \<not> v2 :\<sqsubset>val v1\<rbrakk> \<Longrightarrow> s \<in> r2 \<rightarrow> v1" by fact
-  have as1: "\<forall>v2\<in>LV (SEQ r1 r2) s. \<not> v2 :\<sqsubset>val v1" by fact
-  have as2: "v1 \<in> LV (SEQ r1 r2) s" by fact
-  then obtain 
-    v1a v1b where eqs:
-        "v1 = Seq v1a v1b" "s = flat v1a @ flat v1b"
-        "v1a \<in> LV r1 (flat v1a)" "v1b \<in> LV r2 (flat v1b)" 
-  unfolding LV_def by(auto elim: Prf.cases)
-  have "\<forall>v2 \<in> LV r1 (flat v1a). \<not> v2 :\<sqsubset>val v1a"
-    proof
-      fix v2
-      assume "v2 \<in> LV r1 (flat v1a)"
-      with eqs(2,4) have "Seq v2 v1b \<in> LV (SEQ r1 r2) s"
-         by (simp add: LV_def Prf.intros(1))
-      with as1 have "\<not> Seq v2 v1b :\<sqsubset>val Seq v1a v1b \<and> flat (Seq v2 v1b) = flat (Seq v1a v1b)" 
-         using eqs by (simp add: LV_def) 
-      then show "\<not> v2 :\<sqsubset>val v1a"
-         using PosOrd_SeqI1 by blast
-    qed     
-  then have "flat v1a \<in> r1 \<rightarrow> v1a" using IH1 eqs by simp
+proof -
+  have "s \<in> L r" using assms(1) unfolding LV_def
+    using L_flat_Prf1 by blast 
+  then obtain vposix where vp: "s \<in> r \<rightarrow> vposix"
+    using lexer_correct_Some by blast 
+  with assms(1) have "vposix :\<sqsubseteq>val v1" by (simp add: Posix_PosOrd) 
+  then have "vposix = v1 \<or> vposix :\<sqsubset>val v1" unfolding PosOrd_ex_eq2 by auto
   moreover
-  have "\<forall>v2 \<in> LV r2 (flat v1b). \<not> v2 :\<sqsubset>val v1b"
-    proof 
-      fix v2
-      assume "v2 \<in> LV r2 (flat v1b)"
-      with eqs(2,3,4) have "Seq v1a v2 \<in> LV (SEQ r1 r2) s"
-         by (simp add: LV_def Prf.intros)
-      with as1 have "\<not> Seq v1a v2 :\<sqsubset>val Seq v1a v1b \<and> flat v2 = flat v1b" 
-         using eqs by (simp add: LV_def) 
-      then show "\<not> v2 :\<sqsubset>val v1b"
-         using PosOrd_SeqI2 by auto
-    qed     
-  then have "flat v1b \<in> r2 \<rightarrow> v1b" using IH2 eqs by simp    
-  moreover
-  have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = flat v1b \<and> flat v1a @ s\<^sub>3 \<in> L r1 \<and> s\<^sub>4 \<in> L r2)" 
-  proof
-     assume "\<exists>s3 s4. s3 \<noteq> [] \<and> s3 @ s4 = flat v1b \<and> flat v1a @ s3 \<in> L r1 \<and> s4 \<in> L r2"
-     then obtain s3 s4 where q1: "s3 \<noteq> [] \<and> s3 @ s4 = flat v1b \<and> flat v1a @ s3 \<in> L r1 \<and> s4 \<in> L r2" by blast
-     then obtain vA vB where q2: "flat vA = flat v1a @ s3" "\<Turnstile> vA : r1" "flat vB = s4" "\<Turnstile> vB : r2"
-        using L_flat_Prf2 by blast
-     then have "Seq vA vB \<in> LV (SEQ r1 r2) s" unfolding eqs using q1
-       by (auto simp add: LV_def intro!: Prf.intros)
-     with as1 have "\<not> Seq vA vB :\<sqsubset>val Seq v1a v1b" unfolding eqs by auto
-     then have "\<not> vA :\<sqsubset>val v1a \<and> length (flat vA) > length (flat v1a)" using q1 q2 PosOrd_SeqI1 by auto 
-     then show "False"
-       using PosOrd_shorterI by blast  
-  qed
-  ultimately
-  show "s \<in> SEQ r1 r2 \<rightarrow> v1" unfolding eqs
-    by (rule Posix.intros)
-next
-   case (STAR r s v1)
-   have IH: "\<And>s v1. \<lbrakk>v1 \<in> LV r s; \<forall>v2\<in>LV r s. \<not> v2 :\<sqsubset>val v1\<rbrakk> \<Longrightarrow> s \<in> r \<rightarrow> v1" by fact
-   have as1: "\<forall>v2\<in>LV (STAR r) s. \<not> v2 :\<sqsubset>val v1" by fact
-   have as2: "v1 \<in> LV (STAR r) s" by fact
-   then obtain 
-    vs where eqs:
-        "v1 = Stars vs" "s = flat (Stars vs)"
-        "\<forall>v \<in> set vs. v \<in> LV r (flat v)"
-        unfolding LV_def by (auto elim: Prf.cases)
-   have "\<forall>v\<in>set vs. flat v \<in> r \<rightarrow> v \<and> flat v \<noteq> []" 
-     proof 
-        fix v
-        assume a: "v \<in> set vs"
-        then obtain pre post where e: "vs = pre @ [v] @ post"
-          by (metis append_Cons append_Nil in_set_conv_decomp_first)
-        then have q: "\<forall>v2\<in>LV (STAR r) s. \<not> v2 :\<sqsubset>val Stars (pre @ [v] @ post)" 
-          using as1 unfolding eqs by simp
-        have "\<forall>v2\<in>LV r (flat v). \<not> v2 :\<sqsubset>val v" unfolding eqs 
-          proof (rule ballI, rule notI) 
-             fix v2
-             assume w: "v2 :\<sqsubset>val v"
-             assume "v2 \<in> LV r (flat v)"
-             then have "Stars (pre @ [v2] @ post) \<in> LV (STAR r) s" 
-                 using as2 unfolding e eqs
-                 apply(auto simp add: LV_def intro!: Prf.intros elim: Prf_elims dest: Prf_Stars_appendE)
-                 apply(auto dest!: Prf_Stars_appendE elim: Prf.cases)
-                 done
-             then have  "\<not> Stars (pre @ [v2] @ post) :\<sqsubset>val Stars (pre @ [v] @ post)"
-                using q by simp     
-             with w show "False"
-                using LV_def \<open>v2 \<in> LV r (flat v)\<close> append_Cons flat.simps(7) mem_Collect_eq 
-                PosOrd_StarsI PosOrd_Stars_appendI by auto
-          qed     
-        with IH
-        show "flat v \<in> r \<rightarrow> v \<and> flat v \<noteq> []" using a as2 unfolding eqs LV_def
-        by (auto elim: Prf.cases)
-     qed
-   moreover
-   have "\<not> (\<exists>vs2\<in>LV (STAR r) (flat (Stars vs)). vs2 :\<sqsubset>val Stars vs)" 
-     proof 
-       assume "\<exists>vs2 \<in> LV (STAR r) (flat (Stars vs)). vs2 :\<sqsubset>val Stars vs"
-       then obtain vs2 where "\<Turnstile> Stars vs2 : STAR r" "flat (Stars vs2) = flat (Stars vs)"
-                             "Stars vs2 :\<sqsubset>val Stars vs" 
-         unfolding LV_def by (force elim: Prf_elims intro: Prf.intros)
-       then show "False" using as1 unfolding eqs
-         by (auto simp add: LV_def)
-     qed
-   ultimately have "flat (Stars vs) \<in> STAR r \<rightarrow> Stars vs"
-     thm PosOrd_Posix_Stars
-     by (rule PosOrd_Posix_Stars)
-   then show "s \<in> STAR r \<rightarrow> v1" unfolding eqs .
+    { assume "vposix :\<sqsubset>val v1"
+      moreover
+      have "vposix \<in> LV r s" using vp 
+         using Posix_LV by blast 
+      ultimately have "False" using assms(2) by blast
+    }
+  ultimately show "s \<in> r \<rightarrow> v1" using vp by blast
 qed
 
 lemma Least_existence: