--- 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: