equal
deleted
inserted
replaced
724 assumes "LV r s \<noteq> {}" |
724 assumes "LV r s \<noteq> {}" |
725 shows " \<exists>!vmin \<in> LV r s. \<forall>v \<in> LV r s. vmin :\<sqsubseteq>val v" |
725 shows " \<exists>!vmin \<in> LV r s. \<forall>v \<in> LV r s. vmin :\<sqsubseteq>val v" |
726 using Least_existence[OF assms] assms |
726 using Least_existence[OF assms] assms |
727 using PosOrdeq_antisym by blast |
727 using PosOrdeq_antisym by blast |
728 |
728 |
729 |
729 lemma Least_existence2: |
730 |
730 assumes "LV r s \<noteq> {}" |
|
731 shows " \<exists>!vmin \<in> LV r s. lexer r s = Some vmin \<and> (\<forall>v \<in> LV r s. vmin :\<sqsubseteq>val v)" |
|
732 using Least_existence[OF assms] assms |
|
733 using PosOrdeq_antisym |
|
734 using PosOrd_Posix PosOrd_ex_eq2 lexer_correctness(1) by auto |
731 |
735 |
732 |
736 |
733 lemma Least_existence1_pre: |
737 lemma Least_existence1_pre: |
734 assumes "LV r s \<noteq> {}" |
738 assumes "LV r s \<noteq> {}" |
735 shows " \<exists>!vmin \<in> LV r s. \<forall>v \<in> (LV r s \<union> {v'. flat v' \<sqsubset>spre s}). vmin :\<sqsubseteq>val v" |
739 shows " \<exists>!vmin \<in> LV r s. \<forall>v \<in> (LV r s \<union> {v'. flat v' \<sqsubset>spre s}). vmin :\<sqsubseteq>val v" |