Theory Positions3
theory Positions3
imports Lexer3 LexicalVals3
begin
section ‹An alternative definition for POSIX values by Okui \& Suzuki›
section ‹Positions in Values›
fun
at :: "'a val ⇒ nat list ⇒ 'a val"
where
"at v [] = v"
| "at (Left v) (0#ps)= at v ps"
| "at (Right v) (Suc 0#ps)= at v ps"
| "at (Seq v1 v2) (0#ps)= at v1 ps"
| "at (Seq v1 v2) (Suc 0#ps)= at v2 ps"
| "at (Stars vs) (n#ps) = at (nth vs n) ps"
| "at (Recv l v) ps = at v ps"
fun Pos :: "'a val ⇒ (nat list) set"
where
"Pos (Void) = {[]}"
| "Pos (Atm c) = {[]}"
| "Pos (Left v) = {[]} ∪ {0#ps | ps. ps ∈ Pos v}"
| "Pos (Right v) = {[]} ∪ {1#ps | ps. ps ∈ Pos v}"
| "Pos (Seq v1 v2) = {[]} ∪ {0#ps | ps. ps ∈ Pos v1} ∪ {1#ps | ps. ps ∈ Pos v2}"
| "Pos (Stars []) = {[]}"
| "Pos (Stars (v#vs)) = {[]} ∪ {0#ps | ps. ps ∈ Pos v} ∪ {Suc n#ps | n ps. n#ps ∈ Pos (Stars vs)}"
| "Pos (Recv l v) = {[]} ∪ {ps . ps ∈ Pos v}"
lemma Pos_stars:
"Pos (Stars vs) = {[]} ∪ (⋃n < length vs. {n#ps | ps. ps ∈ Pos (vs ! n)})"
apply(induct vs)
apply(auto simp add: insert_ident less_Suc_eq_0_disj)
done
lemma Pos_empty:
shows "[] ∈ Pos v"
by (induct v rule: Pos.induct)(auto)
abbreviation
"intlen vs ≡ int (length vs)"
definition pflat_len :: "'a val ⇒ nat list => int"
where
"pflat_len v p ≡ (if p ∈ Pos v then intlen (flat (at v p)) else -1)"
lemma pflat_len_simps:
shows "pflat_len (Seq v1 v2) (0#p) = pflat_len v1 p"
and "pflat_len (Seq v1 v2) (Suc 0#p) = pflat_len v2 p"
and "pflat_len (Left v) (0#p) = pflat_len v p"
and "pflat_len (Left v) (Suc 0#p) = -1"
and "pflat_len (Right v) (Suc 0#p) = pflat_len v p"
and "pflat_len (Right v) (0#p) = -1"
and "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"
and "pflat_len (Recv l v) p = pflat_len v p"
and "pflat_len v [] = intlen (flat v)"
apply (auto simp add: pflat_len_def Pos_empty)
by (metis at.simps(7) neq_Nil_conv)
lemma pflat_len_Stars_simps:
assumes "n < length vs"
shows "pflat_len (Stars vs) (n#p) = pflat_len (vs!n) p"
using assms
apply(induct vs arbitrary: n p)
apply(auto simp add: less_Suc_eq_0_disj pflat_len_simps)
done
lemma pflat_len_outside:
assumes "p ∉ Pos v1"
shows "pflat_len v1 p = -1 "
using assms by (simp add: pflat_len_def)
section ‹Orderings›
definition prefix_list:: "'a list ⇒ 'a list ⇒ bool" (‹_ ⊑pre _› [60,59] 60)
where
"ps1 ⊑pre ps2 ≡ ∃ps'. ps1 @ps' = ps2"
definition sprefix_list:: "'a list ⇒ 'a list ⇒ bool" (‹_ ⊏spre _› [60,59] 60)
where
"ps1 ⊏spre ps2 ≡ ps1 ⊑pre ps2 ∧ ps1 ≠ ps2"
inductive lex_list :: "nat list ⇒ nat list ⇒ bool" (‹_ ⊏lex _› [60,59] 60)
where
"[] ⊏lex (p#ps)"
| "ps1 ⊏lex ps2 ⟹ (p#ps1) ⊏lex (p#ps2)"
| "p1 < p2 ⟹ (p1#ps1) ⊏lex (p2#ps2)"
lemma lex_irrfl:
fixes ps1 ps2 :: "nat list"
assumes "ps1 ⊏lex ps2"
shows "ps1 ≠ ps2"
using assms
by(induct rule: lex_list.induct)(auto)
lemma lex_simps [simp]:
fixes xs ys :: "nat list"
shows "[] ⊏lex ys ⟷ ys ≠ []"
and "xs ⊏lex [] ⟷ False"
and "(x # xs) ⊏lex (y # ys) ⟷ (x < y ∨ (x = y ∧ xs ⊏lex ys))"
by (auto simp add: neq_Nil_conv elim: lex_list.cases intro: lex_list.intros)
lemma lex_trans:
fixes ps1 ps2 ps3 :: "nat list"
assumes "ps1 ⊏lex ps2" "ps2 ⊏lex ps3"
shows "ps1 ⊏lex ps3"
using assms
by (induct arbitrary: ps3 rule: lex_list.induct)
(auto elim: lex_list.cases)
lemma lex_trichotomous:
fixes p q :: "nat list"
shows "p = q ∨ p ⊏lex q ∨ q ⊏lex p"
apply(induct p arbitrary: q)
apply(auto elim: lex_list.cases)
apply(case_tac q)
apply(auto)
done
section ‹POSIX Ordering of Values According to Okui \& Suzuki›
definition PosOrd:: "'a val ⇒ nat list ⇒ 'a val ⇒ bool" (‹_ ⊏val _ _› [60, 60, 59] 60)
where
"v1 ⊏val p v2 ≡ pflat_len v1 p > pflat_len v2 p ∧
(∀q ∈ Pos v1 ∪ Pos v2. q ⊏lex p ⟶ pflat_len v1 q = pflat_len v2 q)"
lemma PosOrd_def2:
shows "v1 ⊏val p v2 ⟷
pflat_len v1 p > pflat_len v2 p ∧
(∀q ∈ Pos v1. q ⊏lex p ⟶ pflat_len v1 q = pflat_len v2 q) ∧
(∀q ∈ Pos v2. q ⊏lex p ⟶ pflat_len v1 q = pflat_len v2 q)"
unfolding PosOrd_def
apply(auto)
done
definition PosOrd_ex:: "'a val ⇒ 'a val ⇒ bool" (‹_ :⊏val _› [60, 59] 60)
where
"v1 :⊏val v2 ≡ ∃p. v1 ⊏val p v2"
definition PosOrd_ex_eq:: "'a val ⇒ 'a val ⇒ bool" (‹_ :⊑val _› [60, 59] 60)
where
"v1 :⊑val v2 ≡ v1 :⊏val v2 ∨ v1 = v2"
lemma PosOrd_trans:
assumes "v1 :⊏val v2" "v2 :⊏val v3"
shows "v1 :⊏val v3"
proof -
from assms obtain p p'
where as: "v1 ⊏val p v2" "v2 ⊏val p' v3" unfolding PosOrd_ex_def by blast
then have pos: "p ∈ Pos v1" "p' ∈ Pos v2" unfolding PosOrd_def pflat_len_def
by (smt not_int_zless_negative)+
have "p = p' ∨ p ⊏lex p' ∨ p' ⊏lex p"
by (rule lex_trichotomous)
moreover
{ assume "p = p'"
with as have "v1 ⊏val p v3" unfolding PosOrd_def pflat_len_def
by (smt Un_iff)
then have " v1 :⊏val v3" unfolding PosOrd_ex_def by blast
}
moreover
{ assume "p ⊏lex p'"
with as have "v1 ⊏val p v3" unfolding PosOrd_def pflat_len_def
by (smt Un_iff lex_trans)
then have " v1 :⊏val v3" unfolding PosOrd_ex_def by blast
}
moreover
{ assume "p' ⊏lex p"
with as have "v1 ⊏val p' v3" unfolding PosOrd_def
by (smt Un_iff lex_trans pflat_len_def)
then have "v1 :⊏val v3" unfolding PosOrd_ex_def by blast
}
ultimately show "v1 :⊏val v3" by blast
qed
lemma PosOrd_irrefl:
assumes "v :⊏val v"
shows "False"
using assms unfolding PosOrd_ex_def PosOrd_def
by auto
lemma PosOrd_assym:
assumes "v1 :⊏val v2"
shows "¬(v2 :⊏val v1)"
using assms
using PosOrd_irrefl PosOrd_trans by blast
lemma PosOrd_ordering:
shows "ordering (λv1 v2. v1 :⊑val v2) (λ v1 v2. v1 :⊏val v2)"
unfolding ordering_def PosOrd_ex_eq_def
apply(auto)
using PosOrd_trans partial_preordering_def apply blast
using PosOrd_assym ordering_axioms_def by blast
lemma PosOrd_order:
shows "class.order (λv1 v2. v1 :⊑val v2) (λ v1 v2. v1 :⊏val v2)"
using PosOrd_ordering
apply(simp add: class.order_def class.preorder_def class.order_axioms_def)
by (smt (verit) PosOrd_ex_eq_def PosOrd_irrefl PosOrd_trans)
lemma PosOrd_ex_eq2:
shows "v1 :⊏val v2 ⟷ (v1 :⊑val v2 ∧ v1 ≠ v2)"
using PosOrd_ordering
using PosOrd_ex_eq_def PosOrd_irrefl by blast
lemma PosOrdeq_trans:
assumes "v1 :⊑val v2" "v2 :⊑val v3"
shows "v1 :⊑val v3"
using assms PosOrd_ordering
unfolding ordering_def
by (metis partial_preordering.trans)
lemma PosOrdeq_antisym:
assumes "v1 :⊑val v2" "v2 :⊑val v1"
shows "v1 = v2"
using assms PosOrd_ordering
by (metis ordering.eq_iff)
lemma PosOrdeq_refl:
shows "v :⊑val v"
unfolding PosOrd_ex_eq_def
by auto
lemma PosOrd_shorterE:
assumes "v1 :⊏val v2"
shows "length (flat v2) ≤ length (flat v1)"
using assms unfolding PosOrd_ex_def PosOrd_def
apply(auto)
apply(case_tac p)
apply(simp add: pflat_len_simps)
apply(drule_tac x="[]" in bspec)
apply(simp add: Pos_empty)
apply(simp add: pflat_len_simps)
done
lemma PosOrd_shorterI:
assumes "length (flat v2) < length (flat v1)"
shows "v1 :⊏val v2"
unfolding PosOrd_ex_def PosOrd_def pflat_len_def
using assms Pos_empty by force
lemma PosOrd_spreI:
assumes "flat v' ⊏spre flat v"
shows "v :⊏val v'"
using assms
apply(rule_tac PosOrd_shorterI)
unfolding prefix_list_def sprefix_list_def
by (metis append_Nil2 append_eq_conv_conj drop_all le_less_linear)
lemma pflat_len_inside:
assumes "pflat_len v2 p < pflat_len v1 p"
shows "p ∈ Pos v1"
using assms
unfolding pflat_len_def
by (auto split: if_splits)
lemma PosOrd_Rec_eq:
assumes "flat v1 = flat v2"
shows "Recv l v1 :⊏val Recv l v2 ⟷ v1 :⊏val v2"
unfolding PosOrd_ex_def PosOrd_def2
using assms
apply(auto)
apply (simp add: pflat_len_simps(10))
apply (metis pflat_len_simps(9))
by (metis pflat_len_simps(10) pflat_len_simps(9))
lemma PosOrd_Left_Right:
assumes "flat v1 = flat v2"
shows "Left v1 :⊏val Right v2"
unfolding PosOrd_ex_def
apply(rule_tac x="[0]" in exI)
apply(auto simp add: PosOrd_def pflat_len_simps assms)
done
lemma PosOrd_LeftE:
assumes "Left v1 :⊏val Left v2" "flat v1 = flat v2"
shows "v1 :⊏val v2"
using assms
unfolding PosOrd_ex_def PosOrd_def2
apply(auto simp add: pflat_len_simps)
apply(frule pflat_len_inside)
apply(auto simp add: pflat_len_simps)
by (metis lex_simps(3) pflat_len_simps(3))
lemma PosOrd_LeftI:
assumes "v1 :⊏val v2" "flat v1 = flat v2"
shows "Left v1 :⊏val Left v2"
using assms
unfolding PosOrd_ex_def PosOrd_def2
apply(auto simp add: pflat_len_simps)
by (metis less_numeral_extra(3) lex_simps(3) pflat_len_simps(3))
lemma PosOrd_Left_eq:
assumes "flat v1 = flat v2"
shows "Left v1 :⊏val Left v2 ⟷ v1 :⊏val v2"
using assms PosOrd_LeftE PosOrd_LeftI
by blast
lemma PosOrd_RightE:
assumes "Right v1 :⊏val Right v2" "flat v1 = flat v2"
shows "v1 :⊏val v2"
using assms
unfolding PosOrd_ex_def PosOrd_def2
apply(auto simp add: pflat_len_simps)
apply(frule pflat_len_inside)
apply(auto simp add: pflat_len_simps)
by (metis lex_simps(3) pflat_len_simps(5))
lemma PosOrd_RightI:
assumes "v1 :⊏val v2" "flat v1 = flat v2"
shows "Right v1 :⊏val Right v2"
using assms
unfolding PosOrd_ex_def PosOrd_def2
apply(auto simp add: pflat_len_simps)
by (metis lex_simps(3) nat_neq_iff pflat_len_simps(5))
lemma PosOrd_Right_eq:
assumes "flat v1 = flat v2"
shows "Right v1 :⊏val Right v2 ⟷ v1 :⊏val v2"
using assms PosOrd_RightE PosOrd_RightI
by blast
lemma PosOrd_SeqI1:
assumes "v1 :⊏val w1" "flat (Seq v1 v2) = flat (Seq w1 w2)"
shows "Seq v1 v2 :⊏val Seq w1 w2"
using assms(1)
apply(subst (asm) PosOrd_ex_def)
apply(subst (asm) PosOrd_def)
apply(clarify)
apply(subst PosOrd_ex_def)
apply(rule_tac x="0#p" in exI)
apply(subst PosOrd_def)
apply(rule conjI)
apply(simp add: pflat_len_simps)
apply(rule ballI)
apply(rule impI)
apply(simp only: Pos.simps)
apply(auto)[1]
apply(simp add: pflat_len_simps)
apply(auto simp add: pflat_len_simps)
using assms(2)
apply(simp)
apply(metis length_append of_nat_add)
done
lemma PosOrd_SeqI2:
assumes "v2 :⊏val w2" "flat v2 = flat w2"
shows "Seq v v2 :⊏val Seq v w2"
using assms(1)
apply(subst (asm) PosOrd_ex_def)
apply(subst (asm) PosOrd_def)
apply(clarify)
apply(subst PosOrd_ex_def)
apply(rule_tac x="Suc 0#p" in exI)
apply(subst PosOrd_def)
apply(rule conjI)
apply(simp add: pflat_len_simps)
apply(rule ballI)
apply(rule impI)
apply(simp only: Pos.simps)
apply(auto)[1]
apply(simp add: pflat_len_simps)
using assms(2)
apply(simp)
apply(auto simp add: pflat_len_simps)
done
lemma PosOrd_Seq_eq:
assumes "flat v2 = flat w2"
shows "(Seq v v2) :⊏val (Seq v w2) ⟷ v2 :⊏val w2"
using assms
apply(auto)
prefer 2
apply(simp add: PosOrd_SeqI2)
apply(simp add: PosOrd_ex_def)
apply(auto)
apply(case_tac p)
apply(simp add: PosOrd_def pflat_len_simps)
apply(case_tac a)
apply(simp add: PosOrd_def pflat_len_simps)
apply(clarify)
apply(case_tac nat)
prefer 2
apply(simp add: PosOrd_def pflat_len_simps pflat_len_outside)
apply(rule_tac x="list" in exI)
apply(auto simp add: PosOrd_def2 pflat_len_simps)
apply(smt Collect_disj_eq lex_list.intros(2) mem_Collect_eq pflat_len_simps(2))
apply(smt Collect_disj_eq lex_list.intros(2) mem_Collect_eq pflat_len_simps(2))
done
lemma PosOrd_StarsI:
assumes "v1 :⊏val v2" "flats (v1#vs1) = flats (v2#vs2)"
shows "Stars (v1#vs1) :⊏val Stars (v2#vs2)"
using assms(1)
apply(subst (asm) PosOrd_ex_def)
apply(subst (asm) PosOrd_def)
apply(clarify)
apply(subst PosOrd_ex_def)
apply(subst PosOrd_def)
apply(rule_tac x="0#p" in exI)
apply(simp add: pflat_len_Stars_simps pflat_len_simps)
using assms(2)
apply(simp add: pflat_len_simps)
apply(auto simp add: pflat_len_Stars_simps pflat_len_simps)
by (metis length_append of_nat_add)
lemma PosOrd_StarsI2:
assumes "Stars vs1 :⊏val Stars vs2" "flats vs1 = flats vs2"
shows "Stars (v#vs1) :⊏val Stars (v#vs2)"
using assms(1)
apply(subst (asm) PosOrd_ex_def)
apply(subst (asm) PosOrd_def)
apply(clarify)
apply(subst PosOrd_ex_def)
apply(subst PosOrd_def)
apply(case_tac p)
apply(simp add: pflat_len_simps)
apply(rule_tac x="Suc a#list" in exI)
apply(auto simp add: pflat_len_Stars_simps pflat_len_simps assms(2))
done
lemma PosOrd_Stars_appendI:
assumes "Stars vs1 :⊏val Stars vs2" "flat (Stars vs1) = flat (Stars vs2)"
shows "Stars (vs @ vs1) :⊏val Stars (vs @ vs2)"
using assms
apply(induct vs)
apply(simp)
apply(simp add: PosOrd_StarsI2)
done
lemma PosOrd_StarsE2:
assumes "Stars (v # vs1) :⊏val Stars (v # vs2)"
shows "Stars vs1 :⊏val Stars vs2"
using assms
apply(subst (asm) PosOrd_ex_def)
apply(erule exE)
apply(case_tac p)
apply(simp)
apply(simp add: PosOrd_def pflat_len_simps)
apply(subst PosOrd_ex_def)
apply(rule_tac x="[]" in exI)
apply(simp add: PosOrd_def pflat_len_simps Pos_empty)
apply(simp)
apply(case_tac a)
apply(clarify)
apply(auto simp add: pflat_len_simps PosOrd_def pflat_len_def split: if_splits)[1]
apply(clarify)
apply(simp add: PosOrd_ex_def)
apply(rule_tac x="nat#list" in exI)
apply(auto simp add: PosOrd_def pflat_len_simps)[1]
apply(case_tac q)
apply(simp add: PosOrd_def pflat_len_simps)
apply(clarify)
apply(drule_tac x="Suc a # lista" in bspec)
apply(simp)
apply(auto simp add: PosOrd_def pflat_len_simps)[1]
apply(case_tac q)
apply(simp add: PosOrd_def pflat_len_simps)
apply(clarify)
apply(drule_tac x="Suc a # lista" in bspec)
apply(simp)
apply(auto simp add: PosOrd_def pflat_len_simps)[1]
done
lemma PosOrd_Stars_appendE:
assumes "Stars (vs @ vs1) :⊏val Stars (vs @ vs2)"
shows "Stars vs1 :⊏val Stars vs2"
using assms
apply(induct vs)
apply(simp)
apply(simp add: PosOrd_StarsE2)
done
lemma PosOrd_Stars_append_eq:
assumes "flats vs1 = flats vs2"
shows "Stars (vs @ vs1) :⊏val Stars (vs @ vs2) ⟷ Stars vs1 :⊏val Stars vs2"
using assms
apply(rule_tac iffI)
apply(erule PosOrd_Stars_appendE)
apply(rule PosOrd_Stars_appendI)
apply(auto)
done
lemma PosOrd_Stars_equalsI:
assumes "flats vs1 = flats vs2" "length vs1 = length vs2"
and "list_all2 (λv1 v2. v1 :⊑val v2) vs1 vs2"
shows "Stars vs1 :⊑val Stars vs2"
using assms(3) assms(2,1)
apply(induct rule: list_all2_induct)
apply (simp add: PosOrdeq_refl)
apply(case_tac "Stars (x # xs) = Stars (y # ys)")
apply (simp add: PosOrdeq_refl)
apply(case_tac "x = y")
apply(subgoal_tac "Stars xs :⊏val Stars ys")
apply (simp add: PosOrd_StarsI2 PosOrd_ex_eq_def)
apply (simp add: PosOrd_ex_eq2)
by (meson PosOrd_StarsI PosOrd_ex_eq_def)
lemma PosOrd_almost_trichotomous:
shows "v1 :⊏val v2 ∨ v2 :⊏val v1 ∨ (length (flat v1) = length (flat v2))"
apply(auto simp add: PosOrd_ex_def)
apply(auto simp add: PosOrd_def)
apply(rule_tac x="[]" in exI)
apply(auto simp add: Pos_empty pflat_len_simps)
apply(drule_tac x="[]" in spec)
apply(auto simp add: Pos_empty pflat_len_simps)
done
section ‹The Posix Value is smaller than any other lexical value›
lemma Posix_PosOrd:
assumes "s ∈ r → v1" "v2 ∈ LV r s"
shows "v1 :⊑val v2"
using assms
proof (induct arbitrary: v2 rule: Posix.induct)
case (Posix_One v)
have "v ∈ LV One []" by fact
then have "v = Void"
by (simp add: LV_simps)
then show "Void :⊑val v"
by (simp add: PosOrd_ex_eq_def)
next
case (Posix_Atom c v)
have "v ∈ LV (Atom c) [c]" by fact
then have "v = Atm c"
by (simp add: LV_simps)
then show "Atm c :⊑val v"
by (simp add: PosOrd_ex_eq_def)
next
case (Posix_Plus1 s r1 v r2 v2)
have as1: "s ∈ r1 → v" by fact
have IH: "⋀v2. v2 ∈ LV r1 s ⟹ v :⊑val v2" by fact
have "v2 ∈ LV (Plus r1 r2) s" by fact
then have "⊢ v2 : Plus r1 r2" "flat v2 = s"
by(auto simp add: LV_def prefix_list_def)
then consider
(Left) v3 where "v2 = Left v3" "⊢ v3 : r1" "flat v3 = s"
| (Right) v3 where "v2 = Right v3" "⊢ v3 : r2" "flat v3 = s"
by (auto elim: Prf.cases)
then show "Left v :⊑val v2"
proof(cases)
case (Left v3)
have "v3 ∈ LV r1 s" using Left(2,3)
by (auto simp add: LV_def prefix_list_def)
with IH have "v :⊑val v3" by simp
moreover
have "flat v3 = flat v" using as1 Left(3)
by (simp add: Posix1(2))
ultimately have "Left v :⊑val Left v3"
by (simp add: PosOrd_ex_eq_def PosOrd_Left_eq)
then show "Left v :⊑val v2" unfolding Left .
next
case (Right v3)
have "flat v3 = flat v" using as1 Right(3)
by (simp add: Posix1(2))
then have "Left v :⊑val Right v3"
unfolding PosOrd_ex_eq_def
by (simp add: PosOrd_Left_Right)
then show "Left v :⊑val v2" unfolding Right .
qed
next
case (Posix_Plus2 s r2 v r1 v2)
have as1: "s ∈ r2 → v" by fact
have as2: "s ∉ lang r1" by fact
have IH: "⋀v2. v2 ∈ LV r2 s ⟹ v :⊑val v2" by fact
have "v2 ∈ LV (Plus r1 r2) s" by fact
then have "⊢ v2 : Plus r1 r2" "flat v2 = s"
by(auto simp add: LV_def prefix_list_def)
then consider
(Left) v3 where "v2 = Left v3" "⊢ v3 : r1" "flat v3 = s"
| (Right) v3 where "v2 = Right v3" "⊢ v3 : r2" "flat v3 = s"
by (auto elim: Prf.cases)
then show "Right v :⊑val v2"
proof (cases)
case (Right v3)
have "v3 ∈ LV r2 s" using Right(2,3)
by (auto simp add: LV_def prefix_list_def)
with IH have "v :⊑val v3" by simp
moreover
have "flat v3 = flat v" using as1 Right(3)
by (simp add: Posix1(2))
ultimately have "Right v :⊑val Right v3"
by (auto simp add: PosOrd_ex_eq_def PosOrd_RightI)
then show "Right v :⊑val v2" unfolding Right .
next
case (Left v3)
have "v3 ∈ LV r1 s" using Left(2,3) as2
by (auto simp add: LV_def prefix_list_def)
then have "flat v3 = flat v ∧ ⊢ v3 : r1" using as1 Left(3)
by (simp add: Posix1(2) LV_def)
then have "False" using as1 as2 Left
using Prf_flat_lang by blast
then show "Right v :⊑val v2" by simp
qed
next
case (Posix_Times s1 r1 v1 s2 r2 v2 v3)
have "s1 ∈ r1 → v1" "s2 ∈ r2 → v2" by fact+
then have as1: "s1 = flat v1" "s2 = flat v2" by (simp_all add: Posix1(2))
have IH1: "⋀v3. v3 ∈ LV r1 s1 ⟹ v1 :⊑val v3" by fact
have IH2: "⋀v3. v3 ∈ LV r2 s2 ⟹ v2 :⊑val v3" by fact
have cond: "¬ (∃s⇩3 s⇩4. s⇩3 ≠ [] ∧ s⇩3 @ s⇩4 = s2 ∧ s1 @ s⇩3 ∈ lang r1 ∧ s⇩4 ∈ lang r2)" by fact
have "v3 ∈ LV (Times r1 r2) (s1 @ s2)" by fact
then obtain v3a v3b where eqs:
"v3 = Seq v3a v3b" "⊢ v3a : r1" "⊢ v3b : r2"
"flat v3a @ flat v3b = s1 @ s2"
by (force simp add: prefix_list_def LV_def elim: Prf.cases)
with cond have "flat v3a ⊑pre s1" unfolding prefix_list_def
by (smt Prf_flat_lang append_eq_append_conv2 append_self_conv)
then have "flat v3a ⊏spre s1 ∨ (flat v3a = s1 ∧ flat v3b = s2)" using eqs
by (simp add: sprefix_list_def append_eq_conv_conj)
then have q2: "v1 :⊏val v3a ∨ (flat v3a = s1 ∧ flat v3b = s2)"
using PosOrd_spreI as1(1) eqs by blast
then have "v1 :⊏val v3a ∨ (v3a ∈ LV r1 s1 ∧ v3b ∈ LV r2 s2)" using eqs(2,3)
by (auto simp add: LV_def)
then have "v1 :⊏val v3a ∨ (v1 :⊑val v3a ∧ v2 :⊑val v3b)" using IH1 IH2 by blast
then have "Seq v1 v2 :⊑val Seq v3a v3b" using eqs q2 as1
unfolding PosOrd_ex_eq_def by (auto simp add: PosOrd_SeqI1 PosOrd_Seq_eq)
then show "Seq v1 v2 :⊑val v3" unfolding eqs by blast
next
case (Posix_Star1 s1 r v s2 vs v3)
have "s1 ∈ r → v" "s2 ∈ Star r → Stars vs" by fact+
then have as1: "s1 = flat v" "s2 = flat (Stars vs)" by (auto dest: Posix1(2))
have IH1: "⋀v3. v3 ∈ LV r s1 ⟹ v :⊑val v3" by fact
have IH2: "⋀v3. v3 ∈ LV (Star r) s2 ⟹ Stars vs :⊑val v3" by fact
have cond: "¬ (∃s⇩3 s⇩4. s⇩3 ≠ [] ∧ s⇩3 @ s⇩4 = s2 ∧ s1 @ s⇩3 ∈ lang r ∧ s⇩4 ∈ lang (Star r))" by fact
have cond2: "flat v ≠ []" by fact
have "v3 ∈ LV (Star r) (s1 @ s2)" by fact
then consider
(NonEmpty) v3a vs3 where "v3 = Stars (v3a # vs3)"
"⊢ v3a : r" "⊢ Stars vs3 : Star r"
"flat (Stars (v3a # vs3)) = s1 @ s2"
| (Empty) "v3 = Stars []"
unfolding LV_def
apply(auto)
apply(erule Prf_elims)
by (metis NonEmpty Prf.intros(6) list.set_intros(1) list.set_intros(2) neq_Nil_conv)
then show "Stars (v # vs) :⊑val v3"
proof (cases)
case (NonEmpty v3a vs3)
have "flat (Stars (v3a # vs3)) = s1 @ s2" using NonEmpty(4) .
with cond have "flat v3a ⊑pre s1" using NonEmpty(2,3)
unfolding prefix_list_def
by (smt Prf_flat_lang append_Nil2 append_eq_append_conv2 flat.simps(7))
then have "flat v3a ⊏spre s1 ∨ (flat v3a = s1 ∧ flat (Stars vs3) = s2)" using NonEmpty(4)
by (simp add: sprefix_list_def append_eq_conv_conj)
then have q2: "v :⊏val v3a ∨ (flat v3a = s1 ∧ flat (Stars vs3) = s2)"
using PosOrd_spreI as1(1) NonEmpty(4) by blast
then have "v :⊏val v3a ∨ (v3a ∈ LV r s1 ∧ Stars vs3 ∈ LV (Star r) s2)"
using NonEmpty(2,3) by (auto simp add: LV_def)
then have "v :⊏val v3a ∨ (v :⊑val v3a ∧ Stars vs :⊑val Stars vs3)" using IH1 IH2 by blast
then have "v :⊏val v3a ∨ (v = v3a ∧ Stars vs :⊑val Stars vs3)"
unfolding PosOrd_ex_eq_def by auto
then have "Stars (v # vs) :⊑val Stars (v3a # vs3)" using NonEmpty(4) q2 as1
unfolding PosOrd_ex_eq_def
using PosOrd_StarsI PosOrd_StarsI2
by (metis flat.simps(7) flat_Stars val.inject(5))
then show "Stars (v # vs) :⊑val v3" unfolding NonEmpty by blast
next
case Empty
have "v3 = Stars []" by fact
then show "Stars (v # vs) :⊑val v3"
unfolding PosOrd_ex_eq_def using cond2
by (simp add: PosOrd_shorterI)
qed
next
case (Posix_Star2 r v2)
have "v2 ∈ LV (Star r) []" by fact
then have "v2 = Stars []"
unfolding LV_def by (auto elim: Prf.cases)
then show "Stars [] :⊑val v2"
by (simp add: PosOrd_ex_eq_def)
next
case (Posix_NTimes2 vs r n v2)
have IH: "∀v∈set vs. [] ∈ r → v ∧ (∀x. x ∈ LV r [] ⟶ v :⊑val x)" by fact
then have "flats vs = []"
by (metis Posix.Posix_NTimes2 Posix1(2) flat_Stars)
have "v2 ∈ LV (NTimes r n) []" by fact
then obtain vs' where eq: "v2 = Stars vs'" and "length vs' = n" and as: "∀v ∈ set vs'. v ∈ LV r [] ∧ flat v = []"
unfolding LV_def by (auto elim!: Prf_elims)
then have "Stars vs :⊑val Stars vs'"
apply(rule_tac PosOrd_Stars_equalsI)
apply (simp add: ‹flats vs = []›)
using Posix_NTimes2.hyps(2) apply blast
using IH apply(simp add: list_all2_iff)
apply(auto)
using Posix_NTimes2.hyps(2) apply blast
by (meson in_set_zipE)
then show "Stars vs :⊑val v2" using eq by simp
next
case (Posix_NTimes1 s1 r v s2 n vs)
have "s1 ∈ r → v" "s2 ∈ NTimes r n → Stars vs" by fact+
then have as1: "s1 = flat v" "s2 = flat (Stars vs)" by (auto dest: Posix1(2))
have IH1: "⋀v3. v3 ∈ LV r s1 ⟹ v :⊑val v3" by fact
have IH2: "⋀v3. v3 ∈ LV (NTimes r n) s2 ⟹ Stars vs :⊑val v3" by fact
have cond: "¬ (∃s⇩3 s⇩4. s⇩3 ≠ [] ∧ s⇩3 @ s⇩4 = s2 ∧ s1 @ s⇩3 ∈ lang r ∧ s⇩4 ∈ lang (NTimes r n))" by fact
have cond2: "flat v ≠ []" by fact
have "v2 ∈ LV (NTimes r (n + 1)) (s1 @ s2)" by fact
then consider
(NonEmpty) v3a vs3 where "v2 = Stars (v3a # vs3)"
"⊢ v3a : r" "⊢ Stars vs3 : NTimes r n"
"flat (Stars (v3a # vs3)) = s1 @ s2"
| (Empty) "v2 = Stars []"
unfolding LV_def
apply(auto)
apply(erule Prf_elims)
apply(case_tac vs1)
apply(simp add: as1(1) cond2 flats_empty)
apply(simp)
using Prf.simps apply fastforce
done
then show "Stars (v # vs) :⊑val v2"
proof (cases)
case (NonEmpty v3a vs3)
have "flat (Stars (v3a # vs3)) = s1 @ s2" using NonEmpty(4) .
with cond have "flat v3a ⊑pre s1" using NonEmpty(2,3)
unfolding prefix_list_def
by (smt Prf_flat_lang append_Nil2 append_eq_append_conv2 flat.simps(7))
then have "flat v3a ⊏spre s1 ∨ (flat v3a = s1 ∧ flat (Stars vs3) = s2)" using NonEmpty(4)
by (simp add: sprefix_list_def append_eq_conv_conj)
then have q2: "v :⊏val v3a ∨ (flat v3a = s1 ∧ flat (Stars vs3) = s2)"
using PosOrd_spreI as1(1) NonEmpty(4) by blast
then have "v :⊏val v3a ∨ (v3a ∈ LV r s1 ∧ Stars vs3 ∈ LV (NTimes r n) s2)"
using NonEmpty(2,3) by (auto simp add: LV_def)
then have "v :⊏val v3a ∨ (v :⊑val v3a ∧ Stars vs :⊑val Stars vs3)" using IH1 IH2 by blast
then have "v :⊏val v3a ∨ (v = v3a ∧ Stars vs :⊑val Stars vs3)"
unfolding PosOrd_ex_eq_def by auto
then have "Stars (v # vs) :⊑val Stars (v3a # vs3)" using NonEmpty(4) q2 as1
unfolding PosOrd_ex_eq_def
using PosOrd_StarsI PosOrd_StarsI2
by (metis flat.simps(7) flat_Stars val.inject(5))
then show "Stars (v # vs) :⊑val v2" unfolding NonEmpty by blast
next
case Empty
have "v2 = Stars []" by fact
then show "Stars (v # vs) :⊑val v2"
unfolding PosOrd_ex_eq_def using cond2
by (simp add: PosOrd_shorterI)
qed
next
case (Posix_Upto1 s1 r v s2 n vs v3)
have "s1 ∈ r → v" "s2 ∈ Upto r n → Stars vs" by fact+
then have as1: "s1 = flat v" "s2 = flat (Stars vs)" by (auto dest: Posix1(2))
have IH1: "⋀v3. v3 ∈ LV r s1 ⟹ v :⊑val v3" by fact
have IH2: "⋀v3. v3 ∈ LV (Upto r n) s2 ⟹ Stars vs :⊑val v3" by fact
have cond: "¬ (∃s⇩3 s⇩4. s⇩3 ≠ [] ∧ s⇩3 @ s⇩4 = s2 ∧ s1 @ s⇩3 ∈ lang r ∧ s⇩4 ∈ lang (Upto r n))" by fact
have cond2: "flat v ≠ []" by fact
have "v3 ∈ LV (Upto r (n + 1)) (s1 @ s2)" by fact
then consider
(NonEmpty) v3a vs3 where "v3 = Stars (v3a # vs3)"
"⊢ v3a : r" "⊢ Stars vs3 : Upto r n"
"flat (Stars (v3a # vs3)) = s1 @ s2"
| (Empty) "v3 = Stars []"
unfolding LV_def
apply(auto)
apply(erule Prf_elims)
apply(case_tac vs)
apply(auto)
by (simp add: Prf.intros(8))
then show "Stars (v # vs) :⊑val v3"
proof (cases)
case (NonEmpty v3a vs3)
have "flat (Stars (v3a # vs3)) = s1 @ s2" using NonEmpty(4) .
with cond have "flat v3a ⊑pre s1" using NonEmpty(2,3)
unfolding prefix_list_def
by (smt Prf_flat_lang append_Nil2 append_eq_append_conv2 flat.simps(7))
then have "flat v3a ⊏spre s1 ∨ (flat v3a = s1 ∧ flat (Stars vs3) = s2)" using NonEmpty(4)
by (simp add: sprefix_list_def append_eq_conv_conj)
then have q2: "v :⊏val v3a ∨ (flat v3a = s1 ∧ flat (Stars vs3) = s2)"
using PosOrd_spreI as1(1) NonEmpty(4) by blast
then have "v :⊏val v3a ∨ (v3a ∈ LV r s1 ∧ Stars vs3 ∈ LV (Upto r n) s2)"
using NonEmpty(2,3)
by (auto simp add: LV_def)
then have "v :⊏val v3a ∨ (v :⊑val v3a ∧ Stars vs :⊑val Stars vs3)" using IH1 IH2 by blast
then have "v :⊏val v3a ∨ (v = v3a ∧ Stars vs :⊑val Stars vs3)"
unfolding PosOrd_ex_eq_def by auto
then have "Stars (v # vs) :⊑val Stars (v3a # vs3)" using NonEmpty(4) q2 as1
unfolding PosOrd_ex_eq_def
using PosOrd_StarsI PosOrd_StarsI2
by (metis flat.simps(7) flat_Stars val.inject(5))
then show "Stars (v # vs) :⊑val v3" unfolding NonEmpty by blast
next
case Empty
have "v3 = Stars []" by fact
then show "Stars (v # vs) :⊑val v3"
unfolding PosOrd_ex_eq_def using cond2
by (simp add: PosOrd_shorterI)
qed
next
case (Posix_Upto2 r n v2)
have "v2 ∈ LV (Upto r n) []" by fact
then have "v2 = Stars []"
unfolding LV_def by (auto elim: Prf.cases)
then show "Stars [] :⊑val v2"
by (simp add: PosOrd_ex_eq_def)
next
case (Posix_From2 vs r n)
then show "Stars vs :⊑val v2"
apply(simp add: LV_def)
apply(auto)
apply(erule Prf_elims)
apply(auto)
apply(rule PosOrd_Stars_equalsI)
apply (metis Posix1(2) flats_empty)
apply(simp)
apply(auto simp add: list_all2_iff)
apply (meson set_zip_leftD set_zip_rightD)
done
next
case (Posix_From1 s1 r v s2 n vs v3)
have "s1 ∈ r → v" "s2 ∈ From r (n - 1) → Stars vs" by fact+
then have as1: "s1 = flat v" "s2 = flats vs" by (auto dest: Posix1(2))
have IH1: "⋀v3. v3 ∈ LV r s1 ⟹ v :⊑val v3" by fact
have IH2: "⋀v3. v3 ∈ LV (From r (n - 1)) s2 ⟹ Stars vs :⊑val v3" by fact
have cond: "¬ (∃s⇩3 s⇩4. s⇩3 ≠ [] ∧ s⇩3 @ s⇩4 = s2 ∧ s1 @ s⇩3 ∈ lang r ∧ s⇩4 ∈ lang (From r (n - 1)))" by fact
have cond2: "flat v ≠ []" by fact
have "v3 ∈ LV (From r n) (s1 @ s2)" by fact
then consider
(NonEmpty) v3a vs3 where "v3 = Stars (v3a # vs3)"
"⊢ v3a : r" "⊢ Stars vs3 : From r (n - 1)"
"flats (v3a # vs3) = s1 @ s2"
| (Empty) "v3 = Stars []"
unfolding LV_def
apply(auto)
apply(erule Prf.cases)
apply(auto)
apply(case_tac vs1)
apply(auto intro: Prf.intros)
apply(case_tac vs2)
apply(auto intro: Prf.intros)
apply (simp add: as1(1) cond2 flats_empty)
apply (simp add: Prf.intros)
apply(case_tac vs)
apply(auto)
by (metis Posix_From1.hyps(6) Prf.intros(10) Suc_le_eq Suc_pred less_Suc_eq_le)
then show "Stars (v # vs) :⊑val v3"
proof (cases)
case (NonEmpty v3a vs3)
have "flats (v3a # vs3) = s1 @ s2" using NonEmpty(4) .
with cond have "flat v3a ⊑pre s1" using NonEmpty(2,3)
unfolding prefix_list_def
by (smt (z3) Prf_flat_lang append.right_neutral append_eq_append_conv2 flat.simps(7) flat_Stars)
then have "flat v3a ⊏spre s1 ∨ (flat v3a = s1 ∧ flat (Stars vs3) = s2)" using NonEmpty(4)
by (simp add: sprefix_list_def append_eq_conv_conj)
then have q2: "v :⊏val v3a ∨ (flat v3a = s1 ∧ flat (Stars vs3) = s2)"
using PosOrd_spreI as1(1) NonEmpty(4) by blast
then have "v :⊏val v3a ∨ (v3a ∈ LV r s1 ∧ Stars vs3 ∈ LV (From r (n - 1)) s2)"
using NonEmpty(2,3) by (auto simp add: LV_def)
then have "v :⊏val v3a ∨ (v :⊑val v3a ∧ Stars vs :⊑val Stars vs3)" using IH1 IH2 by blast
then have "v :⊏val v3a ∨ (v = v3a ∧ Stars vs :⊑val Stars vs3)"
unfolding PosOrd_ex_eq_def by auto
then have "Stars (v # vs) :⊑val Stars (v3a # vs3)" using NonEmpty(4) q2 as1
unfolding PosOrd_ex_eq_def
by (metis PosOrd_StarsI PosOrd_StarsI2 flat.simps(7) flat_Stars val.inject(5))
then show "Stars (v # vs) :⊑val v3" unfolding NonEmpty by blast
next
case Empty
have "v3 = Stars []" by fact
then show "Stars (v # vs) :⊑val v3"
unfolding PosOrd_ex_eq_def using cond2
by (simp add: PosOrd_shorterI)
qed
next
case (Posix_From3 s1 r v s2 vs v3)
have "s1 ∈ r → v" "s2 ∈ Star r → Stars vs" by fact+
then have as1: "s1 = flat v" "s2 = flat (Stars vs)" by (auto dest: Posix1(2))
have IH1: "⋀v3. v3 ∈ LV r s1 ⟹ v :⊑val v3" by fact
have IH2: "⋀v3. v3 ∈ LV (Star r) s2 ⟹ Stars vs :⊑val v3" by fact
have cond: "¬ (∃s⇩3 s⇩4. s⇩3 ≠ [] ∧ s⇩3 @ s⇩4 = s2 ∧ s1 @ s⇩3 ∈ lang r ∧ s⇩4 ∈ lang (Star r))" by fact
have cond2: "flat v ≠ []" by fact
have "v3 ∈ LV (From r 0) (s1 @ s2)" by fact
then consider
(NonEmpty) v3a vs3 where "v3 = Stars (v3a # vs3)"
"⊢ v3a : r" "⊢ Stars vs3 : Star r"
"flat (Stars (v3a # vs3)) = s1 @ s2"
| (Empty) "v3 = Stars []"
unfolding LV_def
apply(auto)
apply(erule Prf.cases)
apply(auto)
apply(case_tac vs)
apply(auto intro: Prf.intros)
done
then show "Stars (v # vs) :⊑val v3"
proof (cases)
case (NonEmpty v3a vs3)
have "flat (Stars (v3a # vs3)) = s1 @ s2" using NonEmpty(4) .
with cond have "flat v3a ⊑pre s1" using NonEmpty(2,3)
unfolding prefix_list_def
by (smt (z3) Prf_flat_lang append.right_neutral append_eq_append_conv2 flat.simps(7))
then have "flat v3a ⊏spre s1 ∨ (flat v3a = s1 ∧ flat (Stars vs3) = s2)" using NonEmpty(4)
by (simp add: sprefix_list_def append_eq_conv_conj)
then have q2: "v :⊏val v3a ∨ (flat v3a = s1 ∧ flat (Stars vs3) = s2)"
using PosOrd_spreI as1(1) NonEmpty(4) by blast
then have "v :⊏val v3a ∨ (v3a ∈ LV r s1 ∧ Stars vs3 ∈ LV (Star r) s2)"
using NonEmpty(2,3) by (auto simp add: LV_def)
then have "v :⊏val v3a ∨ (v :⊑val v3a ∧ Stars vs :⊑val Stars vs3)" using IH1 IH2 by blast
then have "v :⊏val v3a ∨ (v = v3a ∧ Stars vs :⊑val Stars vs3)"
unfolding PosOrd_ex_eq_def by auto
then have "Stars (v # vs) :⊑val Stars (v3a # vs3)" using NonEmpty(4) q2 as1
unfolding PosOrd_ex_eq_def
by (metis PosOrd_StarsI PosOrd_StarsI2 flat.simps(7) flat_Stars val.inject(5))
then show "Stars (v # vs) :⊑val v3" unfolding NonEmpty by blast
next
case Empty
have "v3 = Stars []" by fact
then show "Stars (v # vs) :⊑val v3"
unfolding PosOrd_ex_eq_def using cond2
by (simp add: PosOrd_shorterI)
qed
next
case (Posix_Rec s r v l v2)
then show "Recv l v :⊑val v2"
by (smt (verit, del_insts) LV_def LV_simps(6) PosOrd_Rec_eq PosOrd_ex_eq_def Posix1(2) mem_Collect_eq)
next
case (Posix_Cset c cs v)
have "v ∈ LV (Charset cs) [c]" by fact
then have "v = Atm c ∨ False"
apply(case_tac "c ∈ cs")
by(auto simp add: LV_simps)
then show "Atm c :⊑val v"
by (simp add: PosOrd_ex_eq_def)
qed
lemma Posix_PosOrd_reverse:
assumes "s ∈ r → v1"
shows "¬(∃v2 ∈ LV r s. v2 :⊏val v1)"
using assms
by (metis Posix_PosOrd less_irrefl PosOrd_def
PosOrd_ex_eq_def PosOrd_ex_def PosOrd_trans)
lemma PosOrd_Posix:
assumes "v1 ∈ LV r s" "∀v⇩2 ∈ LV r s. ¬ v⇩2 :⊏val v1"
shows "s ∈ r → v1"
proof -
have "s ∈ lang r" using assms(1) unfolding LV_def
using Prf_flat_lang by blast
then obtain vposix where vp: "s ∈ r → vposix"
using lexer_correct_Some by blast
with assms(1) have "vposix :⊑val v1" by (simp add: Posix_PosOrd)
then have "vposix = v1 ∨ vposix :⊏val v1" unfolding PosOrd_ex_eq2 by auto
moreover
{ assume "vposix :⊏val v1"
moreover
have "vposix ∈ LV r s" using vp
using Posix_LV by blast
ultimately have "False" using assms(2) by blast
}
ultimately show "s ∈ r → v1" using vp by blast
qed
lemma Least_existence:
assumes "LV r s ≠ {}"
shows " ∃vmin ∈ LV r s. ∀v ∈ LV r s. vmin :⊑val v"
proof -
from assms
obtain vposix where "s ∈ r → vposix"
unfolding LV_def
using Prf_flat_lang lexer_correct_Some by blast
then have "∀v ∈ LV r s. vposix :⊑val v"
by (simp add: Posix_PosOrd)
then show "∃vmin ∈ LV r s. ∀v ∈ LV r s. vmin :⊑val v"
using Posix_LV ‹s ∈ r → vposix› by blast
qed
lemma Least_existence1:
assumes "LV r s ≠ {}"
shows " ∃! v⇩m⇩i⇩n ∈ LV r s. ∀v ∈ LV r s. v⇩m⇩i⇩n :⊑val v"
using Least_existence[OF assms] assms
using PosOrdeq_antisym by blast
lemma Least_existence2:
assumes "LV r s ≠ {}"
shows " ∃!vmin ∈ LV r s. lexer r s = Some vmin ∧ (∀v ∈ LV r s. vmin :⊑val v)"
using Least_existence[OF assms] assms
using PosOrdeq_antisym
using PosOrd_Posix PosOrd_ex_eq2 lexer_correctness(1)
by (metis (mono_tags, lifting))
lemma Least_existence1_pre:
assumes "LV r s ≠ {}"
shows " ∃!vmin ∈ LV r s. ∀v ∈ (LV r s ∪ {v'. flat v' ⊏spre s}). vmin :⊑val v"
using Least_existence[OF assms] assms
apply -
apply(erule bexE)
apply(rule_tac a="vmin" in ex1I)
apply(auto)[1]
apply (metis PosOrd_Posix PosOrd_ex_eq2 PosOrd_spreI PosOrdeq_antisym Posix1(2))
apply(auto)[1]
apply(simp add: PosOrdeq_antisym)
done
lemma PosOrd_partial:
shows "partial_order_on UNIV {(v1, v2). v1 :⊑val v2}"
apply(simp add: partial_order_on_def)
apply(simp add: preorder_on_def refl_on_def)
apply(simp add: PosOrdeq_refl)
apply(auto)
apply(rule transI)
apply(auto intro: PosOrdeq_trans)[1]
apply(rule antisymI)
apply(simp add: PosOrdeq_antisym)
done
lemma PosOrd_wf:
shows "wf {(v1, v2). v1 :⊏val v2 ∧ v1 ∈ LV r s ∧ v2 ∈ LV r s}"
proof -
have "finite {(v1, v2). v1 ∈ LV r s ∧ v2 ∈ LV r s}"
by (simp add: LV_finite)
moreover
have "{(v1, v2). v1 :⊏val v2 ∧ v1 ∈ LV r s ∧ v2 ∈ LV r s} ⊆ {(v1, v2). v1 ∈ LV r s ∧ v2 ∈ LV r s}"
by auto
ultimately have "finite {(v1, v2). v1 :⊏val v2 ∧ v1 ∈ LV r s ∧ v2 ∈ LV r s}"
using finite_subset by blast
moreover
have "acyclicP (λv1 v2. v1 :⊏val v2 ∧ v1 ∈ LV r s ∧ v2 ∈ LV r s)"
unfolding acyclic_def
by (smt (verit, ccfv_threshold) PosOrd_irrefl PosOrd_trans tranclp_trans_induct tranclp_unfold)
ultimately show "wf {(v1, v2). v1 :⊏val v2 ∧ v1 ∈ LV r s ∧ v2 ∈ LV r s}"
using finite_acyclic_wf by blast
qed
unused_thms
end