Theory VLA_Criterion
section "Equivalent Criteria for Infinite Descent"
text "This subsection concerns two families of alternative criteria that are logically equivalent to
Infinite Descent, and are used as the basis for decision procedures. While these criteria are
already well-established, we provide the first mechanization within the
sloped graph locale, and formal proofs of their soundness and completeness relative to the
locale-level InfiniteDescent predicate."
subsection "Automata-based criteria"
text ‹The first family of criteria reduces Infinite Descent to a language inclusion problem by interpreting (descending) ipaths as words in an \(\omega\)-regular language~\cite{LeeJB01,Brotherston:PhD,Simpson17Fossacs,InfiniteDescent}.
We formalize two approaches for constructing this interpretation, which (following the terminology of~\cite{InfiniteDescent})
we refer to as the `vertex-language' and `slope-language' criteria, respectively.›
subsubsection "Vertex-language Criterion"
theory VLA_Criterion
imports "../Sloped_Graphs"
"../Buchi_Preliminaries"
begin
context Sloped_Graph
begin
abbreviation q⇩0 where "q⇩0 ≡ None"
fun Δ_trans :: "'node ⇒ 'node option ⇒ 'node option set" where
"Δ_trans tr (Some s) = (if edge s tr ∧ {s, tr} ⊆ Node then {Some tr} else {})"|
"Δ_trans tr q⇩0 = (if tr ∈ Node then {Some tr} else {})"
lemma Δ_trans_q⇩0:"l ∈ Node ⟹ Some l ∈ Δ_trans l q⇩0" by auto
lemma Δ_trans_edge:"edge s tr ⟹ {s, tr} ⊆ Node ⟹ (Some tr) ∈ Δ_trans tr (Some s)" by auto
lemma Δ_trans_elim:
assumes "r ∈ Δ_trans x q"
obtains (EdgeCase) "∃q'. q = Some q' ∧ edge q' x ∧ {q', x} ⊆ Node ∧ r = (Some x)"
| (InitCase) "q = q⇩0" "x ∈ Node" "r = (Some x)"
proof -
have "r ∈ Δ_trans x q" using assms by assumption
then consider
(EdgeCase) "∃q'. q = Some q' ∧ edge q' x ∧ {q', x} ⊆ Node ∧ r = (Some x)" |
(InitCase) "q = q⇩0 ∧ x ∈ Node ∧ r = (Some x)"
by(cases q, auto split: if_splits)
then show thesis using that by (cases, auto)
qed
lemma "Δ_trans l s =
{s'. s = q⇩0 ∧ s' = (Some l) ∧ l ∈ Node} ∪
{s' . ∃q'. s = Some q' ∧ s' = (Some l) ∧ edge q' l ∧ {q', l} ⊆ Node}"
by(cases s, auto)
definition Paut⇩V :: "('node, 'node option) nba" where
"Paut⇩V = nba
Node
{q⇩0}
Δ_trans
(λs. the s ∈ Node)"
lemmas Paut⇩V_defs = Paut⇩V_def Δ_trans.simps
lemma Paut⇩V_alpha[simp]:"nba.alphabet Paut⇩V = Node" unfolding Paut⇩V_def by auto
lemma Paut⇩V_accept[simp]:"nba.accepting Paut⇩V = (λs. the s ∈ Node)" unfolding Paut⇩V_def by auto
lemma Paut⇩V_init[simp]: "nba.initial Paut⇩V = {q⇩0}" unfolding Paut⇩V_def by auto
lemma Paut⇩V_initp[intro]:"p ∈ nba.initial Paut⇩V ⟷ p = q⇩0" by auto
lemma Paut⇩V_trans[simp]:"nba.transition Paut⇩V a b = Δ_trans a b" unfolding Paut⇩V_def by auto
lemmas Paut⇩V_trans' = Paut⇩V_trans Δ_trans.simps
lemma Paut⇩V_lang:"NBA.language Paut⇩V = {nd. ipath nd}"
proof(safe)
fix x
show "x ∈ NBA.language Paut⇩V ⟹ local.ipath x"
proof(erule nba.language_elim, unfold ipath_def Paut⇩V_initp Paut⇩V_accept, safe)
fix r p i
assume run:"NBA.run Paut⇩V (x ||| r) q⇩0" and accept:"infs (λs. the s ∈ Node) r"
have "sset x ⊆ Node" using streams_sset[OF nba.run_alphabet[OF run]] by auto
thus "alw (holdsS Node) x" by (simp add: alw_holdsS_iff_snth subsetD)
show "alw (holds2 edge) x"
proof (coinduct rule:alw_coinduct[of "λx. ∃r q. NBA.run Paut⇩V (x ||| r) q"],safe)
fix x'::"'node stream"
fix r'::"'node option stream"
fix q
show "∃r q. NBA.run Paut⇩V (x ||| r) q" using run streams_sset[OF nba.run_alphabet[OF run]] by auto
show "NBA.run Paut⇩V (x' ||| r') q ⟹ holds2 edge x'"
apply(unfold szip_unfold[of x' r'], erule NBA.nba.run_scons_elim[of Paut⇩V], safe)
apply(unfold Paut⇩V_alpha Paut⇩V_trans szip_unfold[of "stl x'"])
apply(erule NBA.nba.run_scons_elim[of Paut⇩V])
by(cases q, auto split: if_splits)
{assume "¬ alw (holds2 edge) (stl x')" "NBA.run Paut⇩V (x' ||| r') q"
then show"∃r q. NBA.run Paut⇩V (stl x' ||| r) q"
by(cases "(x' ||| r')", auto simp: stl_sset subset_iff split: if_splits)}
qed
qed
show "ipath x ⟹ x ∈ NBA.language Paut⇩V"
proof(rule nba.language[of q⇩0 _ x "smap Some x"])
fix x
assume ipath:"ipath x"
hence x1_prop:"Some (shd x) ∈ Δ_trans (shd x) q⇩0" "shd x ∈ Node"
using Δ_trans_q⇩0 alw_holdsS_iff_snth snth_0 ipath sset_ipath by force+
show "q⇩0 ∈ nba.initial Paut⇩V" by auto
define F_valid:: "('node × 'node option) stream ⇒ 'node option ⇒ bool" where
"F_valid ≡ (λr p. ∃r1. r = (r1 ||| smap Some r1) ∧ ipath r1 ∧ Some (shd r1) ∈ Δ_trans (shd r1) p)"
have FF:"F_valid (x ||| smap Some x) q⇩0" using x1_prop ipath by(auto simp: F_valid_def)
thm "nba.run_coinduct"
thus "NBA.run Paut⇩V (x ||| smap Some x) q⇩0"
apply(coinduct rule: nba.run_coinduct[of F_valid])
apply(unfold Paut⇩V_alpha Paut⇩V_trans fst_def snd_def F_valid_def,safe)
subgoal using sset_ipath by auto
subgoal by simp
subgoal for _ _ _ _ r1 apply(intro exI[of _ "stl r1"] conjI, safe)
subgoal by auto
subgoal using ipath_stl by auto
unfolding stream.map_sel(1)
apply(rule Δ_trans_edge)
subgoal unfolding ipath_iff_snth by(erule allE[of _ 0], auto)
subgoal by (metis R_ne insert_subset sset_ipath stream.collapse stream.set) . .
show "infs (nba.accepting Paut⇩V) (q⇩0 ## smap Some x)"
unfolding alw_ev_scons apply(rule infs_all)
using ipath sset_ipath[OF ipath] unfolding ipath_iff_snth
by (auto)
qed
qed
fun Δ_trans' :: "'node ⇒ ('node × 'pos × slope) option ⇒
('node × 'pos × slope) option set" where
"Δ_trans' v' (Some tr) = (case tr of (v, p, s) ⇒ {Some (v', p', s')| p' s'. RR (v, p) (v', p') s'})"|
"Δ_trans' v' q⇩0 = (if v' ∈ Node then {q⇩0} ∪ {Some (v', p', s')| p' s'. p' ∈ PosOf v' ∧ s' = Main} else {})"
fun fsnd where "fsnd (v,p,s) = (v, p)"
lemma q⇩0'_notDecr:"third r = Decr ⟹ ¬ (Some r) ∈ Δ_trans' x q⇩0" by(auto simp: split: if_splits)
lemma Δ_trans_q⇩0'I:"v ∈ Node ⟹ q⇩0 ∈ Δ_trans' v q⇩0" by auto
lemma Δ_trans'_intro:
assumes "v' ∈ Node"
assumes "tr = q⇩0 ⟹ x = q⇩0 ∨ (∃p' s'. x = Some (v', p', s') ∧ p' ∈ PosOf v' ∧ s' = Main)"
assumes "tr ≠ q⇩0 ⟹ (∃ p' s'. x = Some (v', p', s') ∧ RR (fst(the tr), second(the tr)) (v', p') s')"
shows "x ∈ Δ_trans' v' tr"
using assms by (cases tr, auto)
lemma Δ_trans'_elim:
assumes "v' ∈ Δ_trans' v⇩t q"
obtains
(Δ_trans⇩1) "q = q⇩0" "v⇩t ∈ Node" "v' = q⇩0"
| (Δ_trans⇩2) "q = q⇩0" "v⇩t ∈ Node" "∃v'' p' s'. v' = Some (v'', p',s') ∧ p' ∈ PosOf v'' ∧ s' = Main ∧ v⇩t = v''"
| (Δ_trans⇩3) "∃v p s v'' p' s'. q = Some (v, p, s) ∧ v' = Some (v'', p',s') ∧ RR (v, p) (v'', p') s' ∧ v⇩t = v''" "v⇩t ∈ Node"
proof -
from assms consider
(Δ_trans⇩1) "q = q⇩0 ∧ v⇩t ∈ Node ∧ v' = q⇩0"
| (Δ_trans⇩2) "∃v'' p' s'. q = q⇩0 ∧ v⇩t ∈ Node ∧ v' = Some (v'', p',s') ∧ p' ∈ PosOf v'' ∧ s' = Main ∧ v⇩t = v''"
| (Δ_trans⇩3) "∃v p s v'' p' s'. q = Some (v, p, s) ∧ v' = Some (v'', p',s') ∧ RR (v, p) (v'', p') s' ∧ v⇩t = v'' ∧ v⇩t ∈ Node"
using RR_PosOf by(cases q, auto split: if_splits)
then show thesis using that by cases auto
qed
lemma Δ_trans'_elim_q⇩0'_target:
assumes "q⇩0 ∈ Δ_trans' v a"
obtains "q⇩0 = a" "v ∈ Node"
using assms by(cases a,auto split: if_splits)
lemma Δ_trans'_elim_q⇩0':
assumes "v' ∈ Δ_trans' v⇩t q⇩0"
obtains
(Δ_trans⇩1) "v⇩t ∈ Node" "v' = q⇩0"
| (Δ_trans⇩2) "v⇩t ∈ Node" "second (the v') ∈ PosOf (fst (the v'))" "third (the v') = Main" "v⇩t = fst (the v')"
proof -
from assms consider
(Δ_trans⇩1) "v⇩t ∈ Node ∧ v' = q⇩0"
| (Δ_trans⇩2) "v⇩t ∈ Node ∧ second (the v') ∈ PosOf (fst (the v')) ∧ third (the v') = Main ∧ v⇩t = fst (the v')"
using RR_PosOf by(auto split: if_splits)
then show thesis using that by cases auto
qed
lemma q⇩0'_notReachable:"q ≠ q⇩0 ⟹ v' ∈ Δ_trans' v q ⟹ v' ≠ q⇩0" by(cases v', cases q, auto)
lemma Δ_trans'_v_eq:"v' ≠ q⇩0 ⟹ v' ∈ Δ_trans' v q ⟹ fst (the v') = v"
apply(cases v')
subgoal by(cases q, auto)
subgoal by(cases q, auto split: if_splits) .
lemma Δ_trans'_Decr_not_q⇩0:"Some (v, p, Decr) ∈ Δ_trans' vs q ⟹ ∃v' p s. q = Some (v',p,s) ∧ vs = v "
by(cases q, auto split: if_splits)
lemma Δ_trans'_DecrRR:
"v' ≠ None ⟹
fst (the v') ∈ Node ⟹
second (the v') ∈ PosOf (fst (the v')) ⟹
third (the v') = Decr ⟹ v' ∈ Δ_trans' v q ⟹
RR (fst (the q), second (the q)) (fst (the v'), second (the v')) Decr ∧ fst (the v') = v ∧ (fst (the q) ∈ Node ∧ second (the q) ∈ PosOf (fst (the q)) ∧ (third (the q) = Decr ∨ third (the q) = Main))"
apply(cases v')
subgoal by (cases q, auto split:if_splits)
apply(erule Δ_trans'_elim) using RR_PosOf slope.exhaust by (auto,meson slope.exhaust)
lemma Δ_trans'_DecrRR':
"Some (v',p',Decr) ∈ Δ_trans' v q ⟹
v' ∈ Node ⟹ p' ∈ PosOf v' ⟹
RR (fst (the q), second (the q)) (v', p') Decr ∧ v' = v ∧ (fst (the q) ∈ Node ∧ second (the q) ∈ PosOf (fst (the q)))"
using Δ_trans'_DecrRR[of "Some (v',p',Decr)"] by auto
lemma Δ_trans'_ProgDRR:
"q ≠ q⇩0 ⟹
fst (the q) ∈ Node ⟹ second (the q) ∈ PosOf (fst (the q)) ⟹ third (the q) = Decr ⟹
v' ∈ Δ_trans' v q ⟹
RR (fst (the q), second (the q)) (fst (the v'), second (the v')) (third (the v')) ∧ (third (the v') = Main ∨ third (the v') = Decr) ∧ v' ≠ q⇩0"
apply(cases v')
subgoal by( cases q, auto split:if_splits)
apply(erule Δ_trans'_elim) by auto
lemma Δ_trans'_ProgMRR:
"q ≠ q⇩0 ⟹
v' ∈ Δ_trans' v q ⟹
RR (fst (the q), second (the q)) (fst (the v'), second (the v')) (third (the v')) ∧ (third (the v') = Main ∨ third (the v') = Decr) ∧ v' ≠ q⇩0"
apply(cases v')
subgoal by( cases q, auto split:if_splits)
apply(erule Δ_trans'_elim) by auto
lemma Δ_trans'_ProgMRR'_Main:
"x ∈ Node ⟹ y ∈ PosOf x ⟹
Some (x',y',Main) ∈ Δ_trans' x' (Some (x,y,z)) ⟹
RR (x, y) (x', y') Main"
using Δ_trans'_ProgMRR[of "Some (x,y,z)" "Some (x',y',Main)" x'] slope.exhaust by auto
definition Q'_states::"('node × 'pos × slope) option set" where
"Q'_states ≡ {q⇩0} ∪ {Some (v, p, s) |v p s. v ∈ Node ∧ p ∈ PosOf v}"
definition F_valid::"('node × 'pos × slope) option ⇒ bool" where
"F_valid ≡ λs. ∃r1 r2. s = Some (r1, r2, Decr) ∧ r1 ∈ Node ∧ r2 ∈ PosOf r1"
definition Taut⇩V :: "('node, ('node × 'pos × slope) option) nba" where
"Taut⇩V = nba
Node
{q⇩0}
Δ_trans'
F_valid"
lemma RR_red:"(∀n≥Suc 0. RR (r1 !! n, Ps !! n) (stl r1 !! n, stl Ps !! n) (stl Ss !! n)) ⟷
(∀n. RR (stl r1 !! n, stl Ps !! n) (stl(stl r1) !! n, stl(stl Ps) !! n) (stl(stl Ss) !! n))"
apply standard
subgoal by auto
subgoal apply(rule allI)
subgoal for n by(cases n, auto) . .
lemma Taut⇩V_alpha[simp]:"nba.alphabet Taut⇩V = Node" unfolding Taut⇩V_def by auto
lemma Taut⇩V_accept[simp]:"nba.accepting Taut⇩V = (λs. ∃r1 r2. s = Some (r1, r2, Decr) ∧ r1 ∈ Node ∧ r2 ∈ PosOf r1)" unfolding Taut⇩V_def F_valid_def by auto
lemma Taut⇩V_init[simp]: "nba.initial Taut⇩V = {q⇩0}" unfolding Taut⇩V_def by auto
lemma Taut⇩V_initp[intro]:"p ∈ nba.initial Taut⇩V ⟷ p = q⇩0" by auto
lemma Taut⇩V_trans[simp]:"nba.transition Taut⇩V a b = Δ_trans' a b" unfolding Taut⇩V_def by auto
lemmas run_def = nba.run_alt_def_snth fst_nth_zip snd_nth_zip Taut⇩V_trans Taut⇩V_alpha nba.target_alt_def nba.states_alt_def
lemma Taut⇩V_lang:"NBA.language Taut⇩V = {nds. (∃Ps. descentIpath nds Ps) ∧ alw (holdsS Node) nds}"
proof(safe)
fix x
show "x ∈ NBA.language Taut⇩V ⟹ (∃Ps. descentIpath x Ps)"
proof(erule nba.language_elim, unfold Taut⇩V_accept singleton_iff)
fix r p
assume init:"p ∈ nba.initial Taut⇩V" and runs:"NBA.run Taut⇩V (x ||| r) p" and "infs (λs. ∃r1 r2. s = Some (r1, r2, Decr) ∧ r1 ∈ Node ∧ r2 ∈ PosOf r1) (p##r)"
hence p_eq:"p = q⇩0" and run:"NBA.run Taut⇩V (x ||| r) q⇩0" and accept:"infs (λs. ∃r1 r2. s = Some (r1, r2, Decr) ∧ r1 ∈ Node ∧ r2 ∈ PosOf r1) r" by auto
have run':"⋀k. x !! k ∈ Node ∧ r !! k ∈ Δ_trans' (x !! k) (last (q⇩0 # map snd (stake k (x ||| r))))" using run unfolding run_def by auto
have accept_from:"⋀n. ∃k≥n. ∃r1 r2. r !! k = Some (r1, r2, Decr) ∧ r1 ∈ Node ∧ r2 ∈ PosOf r1 ∧ Some (r1, r2, Decr) ∈ Δ_trans' (x !! k) (last (stake k r))"
subgoal for n
using accept unfolding infs_snth
apply-apply(erule allE[of _ "Suc n"], safe)
subgoal for k using runE_Suc'[OF run, of k, unfolded Taut⇩V_trans]
apply-by(rule exI[of _ k], auto simp add: last_stake_i stl_Suc)+ . .
have q⇩0'_Decr:"⋀r1 r2 k j. 0<k ⟹ r !! k = Some (r1, r2, Decr) ⟹ r1 ∈ Node ⟹ r2 ∈ PosOf r1 ⟹ k ≤ j ⟹ r !! j ≠ q⇩0"
subgoal for r1 r2 k j proof(induct "j - k" arbitrary: j)
case 0
then show ?case by auto
next
case (Suc xa)
hence Suc':"⋀ j. 0 < k ⟹ xa = j - k ⟹ k ≤ j ⟹ r !! j ≠ q⇩0" by auto
obtain n where n:"j = Suc n" "xa = n - k" "k ≤ n" using Suc by(cases j,auto)
show ?case
using Suc'[of n,OF Suc(3) n(2,3)] unfolding n
using runE_Suc[OF run, of n]
using q⇩0'_notReachable[of "r !! n" "r !! Suc n"] by auto
qed .
obtain Ps where Ps:"Ps = smap (λr. second (the r)) r" by auto
have x_eq_r:"⋀j. (∃r1 r2 r3. r !! j = Some (r1, r2, r3)) ⟹ x !! j = fst (the (r !! j))"
subgoal for j apply(cases j)
subgoal using runE_0[OF run] by (simp split: if_splits)
apply safe
subgoal for j' r1 r2 r3
using runE_Suc[OF run,of j', unfolded Taut⇩V_trans]
apply-by(erule Δ_trans'_elim, auto) . .
have x_eq_r':"⋀j. (∃r1 r2 r3. stl r !! j = Some (r1, r2, r3)) ⟹ stl x !! j = fst (the (stl r !! j))"
subgoal for j using x_eq_r[of "Suc j"] by auto .
show "∃Ps. descentIpath x Ps"
apply(rule exI[of _ Ps], unfold descentIpath_iff_snth2, intro conjI)
subgoal using accept unfolding infs_snth apply-apply(erule allE[of _ "Suc 0"], safe)
subgoal for k r1 r2 apply(rule exI[of _ k], intro allI impI)
subgoal for j apply(drule Suc_le_lessD)
apply(frule q⇩0'_Decr[of k r1 r2 j], simp_all)
apply(frule x_eq_r)
using runE_Suc'[OF run zero_less_Suc, of j]
Δ_trans'_ProgMRR[of "r !! j" "stl r !! j" "fst (the (stl r !! j))"]
unfolding Ps by auto . .
apply(rule allI)
subgoal for i using accept_from[of "Suc i"] apply-apply(elim exE conjE)
subgoal for k r1 r2 apply(cases k, simp)
subgoal for n
apply(frule Δ_trans'_Decr_not_q⇩0,rule exI[of _ n])
unfolding Ps using x_eq_r[of n] last_take_Suc'[of _ _ r] by auto . . .
qed
next
fix x
show "x ∈ NBA.language Taut⇩V ⟹ alw (holdsS Node) x"
proof(erule nba.language_elim, unfold Taut⇩V_init Taut⇩V_accept singleton_iff)
fix r p
assume "p = q⇩0" and run:"NBA.run Taut⇩V (x ||| r) p"
thus "alw (holdsS Node) x" using streams_sset[OF nba.run_alphabet[OF run]] by (simp add: alw_holdsS_iff_snth subsetD)
qed
next
fix x Ps
assume iDPath:"descentIpath x Ps" and x_node:"alw (holdsS Node) x"
have ev:"ev (alw (holds2 (λ(nd, P) (nd', P'). RR (nd, P) (nd', P') Main ∨ RR (nd, P) (nd', P') Decr))) (x ||| Ps)"and
alw:"alw (ev (holds2 (λ(nd, P) (nd', P'). RR (nd, P) (nd', P') Decr))) (x ||| Ps)"
using iDPath[unfolded descentIpath_def2] by auto
have hh:"⋀x y z i. (stl x!!i, stl y!!i, stl z!!i) ∈sset (x ||| y ||| z)"
by (metis snth_sset snth_szip stream.set_sel(2) szip.sel(2))
define f where "f = (λx' Ps' i. (if RR (x' !! i, Ps' !! i) (stl x' !! i, stl Ps' !! i) Decr then Decr else Main))"
define Ss where "Ss = (λx Ps. Main ## fToStream (f x Ps))"
note Ss_defs = Ss_def f_def fToStream_def
have Ss_i:"⋀k m. m < Suc k ⟹ (Ss (sdrop m x) (sdrop m Ps) !! (Suc k - m)) = f x Ps k" using Suc_diff_le unfolding Ss_defs by auto
obtain m where m:"(⋀n. n≥m ⟹ (holds2 (λ(nd, P) (nd', P'). RR (nd, P) (nd', P') Main ∨ RR (nd, P) (nd', P') Decr)) (sdrop n (x ||| Ps)))"
using ev unfolding ev_alw_iff_sdrop by auto
have alw_dropm:"alw (ev (holds2 (λ(nd, P) (nd', P'). RR (nd, P) (nd', P') Decr))) (sdrop m (x ||| Ps))"
using alw unfolding alw_ev_sdrop by auto
define r where "r = replicate m q⇩0 @- smap Some ((sdrop m x) ||| (sdrop m Ps) ||| (Ss (sdrop m x) (sdrop m Ps)))"
have x_node':"⋀i. x !! i ∈ Node" using x_node unfolding alw_holdsS_iff_snth by auto
have r_eq_q⇩0':"⋀n. Suc n ≤ m ⟷ r!!n = q⇩0"
apply standard unfolding r_def
subgoal using replicate_within_i by auto
subgoal for n apply(rule ccontr, unfold not_le replicate_beyond_i) using x_node'[of "n"] by auto .
have r_neq_q⇩0':"⋀n. Suc n > m ⟷ r!!n = Some (x!!n, Ps !! n, Ss (sdrop m x) (sdrop m Ps) !! (n-m))"
apply standard
subgoal unfolding r_def using replicate_beyond_i by auto
subgoal for n using r_eq_q⇩0'[of n] by auto .
have xn_gr:"⋀n. Suc n > m ⟹ x !! n = fst (the (r !! n))" using r_neq_q⇩0' by auto
have Psn_gr:"⋀n. Suc n > m ⟹ Ps !! n = second (the (r !! n))" using r_neq_q⇩0' by auto
have Ssn_gr:"⋀n. Suc n > m ⟹ third (the (r !! n)) = Ss (sdrop m x) (sdrop m Ps) !! (n-m)" using r_neq_q⇩0' by auto
have m_eq:"⋀k m. Suc k ≤ m ⟹ m < Suc (Suc k) ⟹ m = Suc k" by auto
show "x ∈ NBA.language Taut⇩V"
proof(rule nba.language[of q⇩0 _ _ r], unfold Taut⇩V_accept Taut⇩V_initp, safe)
thm ev_alw_sdrop alw_ev_sdrop
show "NBA.run Taut⇩V (x ||| r) q⇩0"
proof(unfold run_def, intro allI conjI)
fix k
show "x !! k ∈ Node" using x_node' by (metis)
show "r !! k ∈ Δ_trans' (x !! k) (last (q⇩0 # map snd (stake k (x ||| r))))"
proof(induct k)
case 0
then show ?case unfolding r_def apply(cases m)
subgoal using m[of 0] RR_PosOf[of "shd x" "shd Ps" "shd (stl x)" "shd (stl Ps)"]
unfolding Ss_def by (auto)
using Δ_trans_q⇩0'I[of "x!!0", OF x_node'[of 0]] by auto
next
case (Suc k)
then show ?case
unfolding last_stake_szip apply-apply(erule Δ_trans'_elim exE)
subgoal apply(rule Δ_trans'_intro[OF x_node'[of "Suc k"]])
subgoal using le_less_linear[of "Suc (Suc k)" m] apply-apply(erule disjE)
subgoal using r_eq_q⇩0'[of "Suc k"] x_node'[of "Suc k"] by auto
subgoal unfolding r_eq_q⇩0'[symmetric, of k] apply(frule m_eq[of k m], clarify)
using r_neq_q⇩0'[of "Suc k"] m[of "Suc k"] RR_PosOfD Ss_def by auto .
by auto
subgoal apply(rule Δ_trans'_intro[OF x_node'[of "Suc k"]], simp)
using r_neq_q⇩0'[of "Suc k"] r_eq_q⇩0'[of k] Ss_i[of m k]
m[of "k"] xn_gr[of k] xn_gr[of "Suc k"] Psn_gr[of k] Psn_gr[of "Suc k"] Ssn_gr[of "Suc k"]
unfolding f_def by auto
subgoal apply(rule Δ_trans'_intro[OF x_node'[of "Suc k"]], simp)
using r_neq_q⇩0'[of "Suc k"] r_eq_q⇩0'[of k] Ss_i[of m k]
m[of "k"] xn_gr[of k] xn_gr[of "Suc k"] Psn_gr[of k] Psn_gr[of "Suc k"] Ssn_gr[of "Suc k"]
unfolding f_def by auto .
qed
qed
show "infs (λs. ∃r1 r2. s = Some (r1, r2, Decr) ∧ r1 ∈ Node ∧ r2 ∈ PosOf r1) r"
unfolding r_def alw_ev_shift alw_ev_holds_iff_snth
apply(rule allI)
subgoal for i using alw_dropm unfolding alw_ev_holds2_iff_snth case_prod_beta Ss_defs
apply-apply(elim allE[of _ i] exE conjE)
subgoal for j by(frule RR_PosOf,rule exI[of _ "Suc j"], auto) . .
qed
qed
lemma alpha_subseq_PTaut⇩V: "nba.alphabet Paut⇩V ⊆ nba.alphabet Taut⇩V" by simp
lemma Pnode_subseq_rule:"(⋀r. ∀x∈Node. last (map snd r) ≠ Some x ⟹
r ≠ [] ⟹ NBA.path Paut⇩V r None ⟹ last (map snd r) = None) ⟹
(⋃p∈{p. p ∈ nba.initial Paut⇩V}. {last (p # map snd r) |r. NBA.path Paut⇩V r p})
⊆ {r. r = None ∨ (∃x∈Node. r = Some x)}" by auto
lemma Paut⇩V_node_subseq:"NBA.nodes Paut⇩V ⊆ {r. r = None ∨ (∃x∈ Node. r = Some x)}"
unfolding nba.nodes_alt_def nba.reachable_alt_def nba.target_alt_def nba.states_alt_def
apply(rule Pnode_subseq_rule)
subgoal premises p for r using p(3,1-2) apply(induct rule: nba.path.induct)
subgoal by auto
subgoal for a p by (cases p, auto simp: RR_PosOfD' split: if_splits) . .
lemma finite_Nodes_Paut⇩V:"finite (NBA.nodes Paut⇩V)"
apply(rule rev_finite_subset[OF _ Paut⇩V_node_subseq]) using finite_Node_opt by auto
lemma Tnode_subseq_rule:"(⋀r. ∀a. a ∈ Node ⟶ (∀aa. aa ∈ PosOf a ⟶ (∀b. last (map snd r) ≠ Some (a, aa, b))) ⟹
r ≠ [] ⟹ NBA.path Taut⇩V r None ⟹ last (map snd r) = None)
⟹ (⋃p∈{p. p ∈ nba.initial Taut⇩V}. {last (p # map snd r) |r. NBA.path Taut⇩V r p})
⊆ {r. r = None ∨ (∃x∈{(v, p, s) |v p s. v ∈ Node ∧ p ∈ PosOf v}. r = Some x)}" by auto
lemma Taut⇩V_node_subseq:"NBA.nodes Taut⇩V ⊆ {r. r = None ∨ (∃x∈{(v, p, s) |v p s. v ∈ Node ∧ p ∈ PosOf v}. r = Some x)}"
unfolding nba.nodes_alt_def nba.reachable_alt_def nba.target_alt_def nba.states_alt_def
apply(rule Tnode_subseq_rule)
subgoal premises p for r using p(3,1-2) apply(induct rule: nba.path.induct)
subgoal by auto
subgoal for a p by (cases p, auto simp: RR_PosOfD' split: if_splits) . .
lemma set_slope_case:"{(v, p, s) |v p s. v ∈ Node ∧ p ∈ PosOf v} = {(v, p, s) |v p s. v ∈ Node ∧ p ∈ PosOf v ∧ s ∈{Main, Decr}}" by auto
lemma finite_Node_Taut⇩V_gr:"finite ({r. ∃x∈{(v, p, s) |v p s. v ∈ Node ∧ p ∈ PosOf v}. r = Some x}:: ('node × 'pos × slope) option set)"
proof(rule finite_imageI[unfolded image_def, of _ Some], unfold set_slope_case)
define A where "A = {(v, p) | v p. v ∈ Node ∧ p ∈ PosOf v}"
define f::"(('node × 'pos) × slope) ⇒ ('node × 'pos × slope)" where "f = (λ((n, p), s). (n, p, s))"
have A_cart_eq:"A × {Main, Decr} = {(n, p). n ∈ A ∧ p ∈ {Main, Decr}}" by auto
have "A = ⋃ ((λv. {v} × PosOf v) ` Node)"
unfolding A_def by auto
hence "finite A" using Node_finite PosOf_finite by (simp add: finite_UN finite_cartesian_product)
have finiteFull:"finite (A × {Main, Decr})"
using finite_cartesian_product[OF `finite A`, of "{Main, Decr}"] by simp
have S_eq:"{(v, p, s) | v p s. v ∈ Node ∧ p ∈ PosOf v ∧ s ∈ {Main, Decr}} = f ` (A × {Main, Decr})" unfolding A_def f_def case_prod_beta image_def by auto
show "finite {(v, p, s) |v p s. v ∈ Node ∧ p ∈ PosOf v ∧ s ∈ {Main, Decr}}"unfolding S_eq using finite_imageI[OF finiteFull, of f] by auto
qed
lemma finite_Nodes_Taut⇩V:"finite (NBA.nodes Taut⇩V)"
apply(rule rev_finite_subset[OF _ Taut⇩V_node_subseq]) using finite_Node_Taut⇩V_gr by auto
theorem VLA_Criterion:"InfiniteDescent ⟷ NBA.language Paut⇩V ⊆ NBA.language Taut⇩V"
unfolding Taut⇩V_lang Paut⇩V_lang InfiniteDescent_def ipath_def by auto
corollary VLA_Criterion':"InfiniteDescent ⟷ NBA.language Paut⇩V ∩ (NBA.language (complement Taut⇩V)) = {}"
unfolding VLA_Criterion by(rule complement_eq1, simp_all add: finite_Nodes_Taut⇩V)
end
end