Theory VLA_Criterion

(*Certified Infinite Descent Criteria in Isabelle/HOL *)
(*Authors: Jamie Wright, Liron Cohen, Reuben Rowe and Andrei Popescu*)
theory VLA_Criterion
  imports "../Sloped_Graphs"
          "../Buchi_Preliminaries"
begin


context Sloped_Graph 
begin
(*Representing the transitions for the NBA:*)
(**1: In the initial state and can self loop, i.e. Δ(q⇩₀, v) = {q⇩₀} - v can idle **)
(*is a self loop necessary? 
  No, infact it causes the equality to be false... 
      a valid run "NBA.run Paut⇩_V (x ||| r) q⇩₀" 
      doesn't necessarily imply "alw (holds2 edge) x", unless we are guaranteed to transition out of q⇩₀ immediately*)

(**2: Transition into the the graph from q⇩₀ (the path auto has states as vertices, thus the graph is represented 1 for 1, with the addition of q0)**)
(**3: Transition within the graph, using edges (note since q⇩₀ is outside the set of Nodes, we cannot retransition back to q⇩₀)**)

(*Imagine the state transition to look like the graph, where the edges from a state are labelled with the vertex it is visiting*)
(*NB: the parameters of this function are inverted for the nba datatype*)
abbreviation q⇩₀ where "q⇩₀ ≡ None"
(*PATH AUTOMATON*)
fun Δ :: "'node ⇒ 'node option ⇒ 'node option set" where
  "Δ tr (Some s) = (if edge s tr ∧ {s, tr} ⊆ Node then {Some tr} else {})"|
  "Δ tr q⇩₀ = (if tr ∈ Node then {Some tr} else {})"

lemma Δ_q⇩₀:"l ∈ Node ⟹ Some l ∈ Δ l q⇩₀" by auto

lemma Δ_edge:"edge s tr ⟹ {s, tr} ⊆ Node ⟹ (Some tr) ∈ Δ tr (Some s)" by auto

lemma Δ_elim:
  assumes "r ∈ Δ x q"
  obtains (EdgeCase) "∃q'. q = Some q' ∧ edge q' x ∧ {q', x} ⊆ Node ∧ r = (Some x)"
        | (InitCase) "q = q⇩₀" "x ∈ Node" "r = (Some x)"
proof -
  have "r ∈ Δ 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⇩₀ ∧ x ∈ Node ∧ r = (Some x)"
     by(cases q, auto split: if_splits)
  then show thesis using that by (cases, auto)
qed

(*Sanity check with the Δ in the paper, 
  the sets of transitions as before*)
lemma "Δ l s = 
       {s'. s = q⇩₀ ∧ 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⇩₀}
    Δ
    (λs. the s ∈ Node)"

lemmas Paut⇩_V_defs = Paut⇩_V_def Δ.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⇩₀}" unfolding Paut⇩_V_def by auto
lemma Paut⇩_V_initp[intro]:"p ∈ nba.initial Paut⇩_V ⟷ p = q⇩₀" by auto
lemma Paut⇩_V_trans[simp]:"nba.transition Paut⇩_V a b = Δ a b" unfolding Paut⇩_V_def by auto

lemmas Paut⇩_V_trans' = Paut⇩_V_trans Δ.simps


(*The language of the path automaton represents all ipaths*)
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⇩₀" 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⇩₀ _ x "smap Some x"])
    fix x 
    assume ipath:"ipath x"

    hence x1_prop:"Some (shd x) ∈ Δ (shd x) q⇩₀" "shd x ∈ Node" 
      using Δ_q⇩₀ alw_holdsS_iff_snth snth_0 ipath sset_ipath by force+

    show "q⇩₀ ∈ nba.initial Paut⇩_V" by auto

    define F:: "('node × 'node option) stream ⇒ 'node option ⇒ bool" where
      "F ≡ (λr p. ∃r1. r = (r1 ||| smap Some r1) ∧ ipath r1 ∧ Some (shd r1) ∈ Δ (shd r1) p)"

    have FF:"F (x ||| smap Some x) q⇩₀" using x1_prop ipath  by(auto simp: F_def)

    thm "nba.run_coinduct"
    thus "NBA.run Paut⇩_V (x ||| smap Some x) q⇩₀"
      apply(coinduct rule: nba.run_coinduct[of F])
      apply(unfold Paut⇩_V_alpha Paut⇩_V_trans fst_def snd_def F_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 Δ_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⇩₀ ## 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
(*TRACE AUTO*)
fun Δ' :: "'node ⇒ ('node × 'pos × slope) option ⇒ 
                  ('node × 'pos × slope) option set" where
  "Δ' v' (Some tr) = (case tr of (v, p, s) ⇒ {Some (v', p', s')| p' s'. RR (v, p) (v', p') s'})"|
  "Δ' v' q⇩₀ = (if v' ∈ Node then {q⇩₀} ∪ {Some (v', p', s')| p' s'. p' ∈ PosOf v' ∧ s' = Main} else {})"


fun fsnd where "fsnd (v,p,s) = (v, p)"

lemma q⇩₀'_notDecr:"third r = Decr ⟹ ¬ (Some r) ∈ Δ' x q⇩₀" by(auto simp:   split: if_splits)

lemma Δ_q⇩₀'I:"v ∈ Node ⟹ q⇩₀ ∈ Δ' v q⇩₀" by auto 

lemma Δ'_intro:
  assumes "v' ∈ Node"
  assumes "tr = q⇩₀ ⟹ x = q⇩₀  ∨ (∃p' s'. x = Some (v', p', s') ∧ p' ∈ PosOf v' ∧ s' = Main)"
  assumes "tr ≠ q⇩₀ ⟹ (∃ p' s'. x = Some (v', p', s') ∧ RR (fst(the tr), second(the tr)) (v', p') s')"
  shows "x ∈ Δ' v' tr"
  using assms by (cases tr, auto)

lemma Δ'_elim:
  assumes "v' ∈ Δ' v⇩_t q"
  obtains 
    (Δ⇩₁) "q = q⇩₀" "v⇩_t ∈ Node" "v' = q⇩₀"
  | (Δ⇩₂) "q = q⇩₀" "v⇩_t ∈ Node" "∃v'' p' s'. v' = Some (v'', p',s') ∧ p' ∈ PosOf v'' ∧ s' = Main ∧ v⇩_t = v''"
  | (Δ⇩₃) "∃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 
    (Δ⇩₁) "q = q⇩₀ ∧ v⇩_t ∈ Node ∧ v' = q⇩₀" 
  | (Δ⇩₂) "∃v'' p' s'. q = q⇩₀ ∧ v⇩_t ∈ Node ∧ v' = Some (v'', p',s') ∧ p' ∈ PosOf v'' ∧ s' = Main ∧ v⇩_t = v''"
  | (Δ⇩₃) "∃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 Δ'_elim_q⇩₀'_target:
  assumes "q⇩₀ ∈ Δ' v a" 
  obtains "q⇩₀ = a" "v ∈ Node"  
  using assms by(cases a,auto split: if_splits)

lemma Δ'_elim_q⇩₀':
  assumes "v' ∈ Δ' v⇩_t q⇩₀"
  obtains 
    (Δ⇩₁) "v⇩_t ∈ Node" "v' = q⇩₀"
  | (Δ⇩₂) "v⇩_t ∈ Node" "second (the v') ∈ PosOf (fst (the v'))" "third (the v') = Main" "v⇩_t = fst (the v')"
proof -
  from assms consider 
    (Δ⇩₁) "v⇩_t ∈ Node ∧ v' = q⇩₀" 
  | (Δ⇩₂) "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

(*If we transition from a state which is not q⇩₀, then we can never return*)
lemma q⇩₀'_notReachable:"q ≠ q⇩₀ ⟹ v' ∈ Δ' v q ⟹ v' ≠ q⇩₀" by(cases v', cases q, auto)

lemma Δ'_v_eq:"v' ≠ q⇩₀ ⟹ v' ∈ Δ' v q ⟹ fst (the v') = v"
  apply(cases v')
  subgoal by(cases q, auto)
  subgoal by(cases q, auto split: if_splits) .

lemma Δ'_Decr_not_q⇩₀:"Some (v, p, Decr) ∈ Δ' vs q ⟹ ∃v' p s. q = Some (v',p,s) ∧ vs = v "
  by(cases q, auto split: if_splits)

(*If we transition to a state v' which is decreasing, then RR x y Decr*)
lemma Δ'_DecrRR:
              "v' ≠ None ⟹
               fst (the v') ∈ Node ⟹
               second (the v') ∈ PosOf (fst (the v')) ⟹
               third (the v') = Decr ⟹ v' ∈ Δ' 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 Δ'_elim) using  RR_PosOf slope.exhaust by (auto,meson slope.exhaust) 

lemma Δ'_DecrRR':
              "Some (v',p',Decr) ∈ Δ' 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 Δ'_DecrRR[of "Some (v',p',Decr)"] by auto

(*From a decreasing state, we only transition via RR*)
lemma Δ'_ProgDRR:
              "q ≠ q⇩₀ ⟹
               fst (the q) ∈ Node ⟹ second (the q) ∈ PosOf (fst (the q)) ⟹ third (the q) = Decr ⟹ 
               v' ∈ Δ' 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⇩₀"
  apply(cases v')
  subgoal by( cases q, auto split:if_splits)
  apply(erule Δ'_elim) by auto 

lemma Δ'_ProgMRR:
              "q ≠ q⇩₀ ⟹
               v' ∈ Δ' 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⇩₀"
  apply(cases v')
  subgoal by( cases q, auto split:if_splits)
  apply(erule Δ'_elim) by auto 

lemma Δ'_ProgMRR'_Main:
              "x ∈ Node ⟹ y ∈ PosOf x ⟹ 
               Some (x',y',Main) ∈ Δ' x' (Some (x,y,z)) ⟹
               RR (x, y) (x', y') Main"
  using Δ'_ProgMRR[of "Some (x,y,z)" "Some (x',y',Main)" x'] slope.exhaust by auto


(*What the states should be, per the paper:*)
definition Q'::"('node × 'pos × slope) option set" where 
"Q' ≡ {q⇩₀} ∪ {Some (v, p, s) |v p s. v ∈ Node ∧ p ∈ PosOf v}"


definition F::"('node × 'pos × slope) option ⇒ bool" where 
"F ≡ λ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⇩₀}
    Δ'
    F"


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_def by auto
lemma Taut⇩_V_init[simp]: "nba.initial Taut⇩_V = {q⇩₀}" unfolding Taut⇩_V_def by auto
lemma Taut⇩_V_initp[intro]:"p ∈ nba.initial Taut⇩_V ⟷ p = q⇩₀" by auto
lemma Taut⇩_V_trans[simp]:"nba.transition Taut⇩_V a b = Δ' 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
(*The language of the trace automaton accepts all infinite sequences for which some suffix has a decreasing trace*)
(*necessary to include that the nodes are within the set of Nodes, otherwise we cannot transition in Delta *)
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⇩₀" and run:"NBA.run Taut⇩_V (x ||| r) q⇩₀" 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 ∈ Δ' (x !! k) (last (q⇩₀ # 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) ∈ Δ' (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)+ . .

  (*If we reach a point k where Decr occurs, then no future state j with j≥k can be q⇩₀*)
  have q⇩₀'_Decr:"⋀r1 r2 k j. 0<k ⟹ r !! k = Some (r1, r2, Decr) ⟹ r1 ∈ Node ⟹ r2 ∈ PosOf r1 ⟹ k ≤ j ⟹ r !! j ≠ q⇩₀"
    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⇩₀" 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⇩₀'_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 Δ'_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⇩₀'_Decr[of k r1 r2 j], simp_all)
        apply(frule x_eq_r)
        using runE_Suc'[OF run zero_less_Suc, of j] 
              Δ'_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 Δ'_Decr_not_q⇩₀,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⇩₀" 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⇩₀ @- 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⇩₀':"⋀n. Suc n ≤ m ⟷ r!!n = q⇩₀" 
    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⇩₀':"⋀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⇩₀'[of n] by auto .

  have xn_gr:"⋀n. Suc n > m ⟹ x !! n = fst (the (r !! n))" using r_neq_q⇩₀' by auto
  have Psn_gr:"⋀n. Suc n > m ⟹ Ps !! n = second (the (r !! n))" using r_neq_q⇩₀' 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⇩₀' 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⇩₀ _ _ r], unfold Taut⇩_V_accept Taut⇩_V_initp, safe)
    (*can always drop from the stream and preserve these properties*)
    thm ev_alw_sdrop alw_ev_sdrop
    show "NBA.run Taut⇩_V (x ||| r) q⇩₀" 
    proof(unfold run_def, intro allI conjI) 
      fix k 
      show "x !! k ∈ Node" using x_node' by (metis)

      show "r !! k ∈ Δ' (x !! k) (last (q⇩₀ # 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 Δ_q⇩₀'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 Δ'_elim exE)
          (*Δ⇩₁ within q⇩₀ -- q⇩₀ ∈ Δ' (x !! k) q⇩₀ ⟹ r !! Suc k ∈ Δ' (x !! Suc k) q⇩₀*)
          subgoal apply(rule Δ'_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⇩₀'[of "Suc k"] x_node'[of "Suc k"]  by auto 
              subgoal unfolding r_eq_q⇩₀'[symmetric, of k]  apply(frule m_eq[of k m], clarify)
                using r_neq_q⇩₀'[of "Suc k"] m[of "Suc k"] RR_PosOfD Ss_def by auto . 
            by auto
          (*Δ⇩₂ Initialise -- (x !! k,Ps,Main) ∈ Δ' (x !! k) q⇩₀ ⟹ r !! Suc k ∈ Δ' (x !! Suc k) (x !! k,Ps,Main)*)
          subgoal apply(rule Δ'_intro[OF x_node'[of "Suc k"]], simp)
            using r_neq_q⇩₀'[of "Suc k"]  r_eq_q⇩₀'[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 
          (*Δ⇩₃ within Main/Decr trace*)
          subgoal apply(rule Δ'_intro[OF x_node'[of "Suc k"]], simp)
            using r_neq_q⇩₀'[of "Suc k"]  r_eq_q⇩₀'[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
    (*Found the appropriate invariant for this one...*)
    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

(*Trivial auxillary results required*)
lemma alpha_subseq_PTaut⇩_V: "nba.alphabet Paut⇩_V ⊆ nba.alphabet Taut⇩_V" by simp
(*PATH AUTO FINITE NODES*)

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 

(*TRACE AUTO FINITE NODES*)
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 4.1*)
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


(*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(coinduct rule: infs_coinduct
           [of "λss. ∃x y z. 
                ss = smap Some (x ||| y ||| z) ∧ alw (ev (holds2 (λ(nd, P) (nd', P'). RR (nd, P) (nd', P') Decr))) (x ||| y) ∧ 
                (∀i. stl z !! i = Decr ⟷ RR (x!!i, y!!i) (stl x!!i, stl y!!i) Decr)"]) 
      subgoal apply(rule exI3[of _ "sdrop m x" "sdrop m Ps" "Ss (sdrop m x) (sdrop m Ps)"]) 
        using alw_dropm unfolding Ss_defs by (auto simp add: Groups.add_ac(2))
      subgoal for w
        unfolding ev_iff_sdrop apply(elim exE conjE, intro conjI)
        subgoal for x y z apply(drule alwD, elim exE conjE, simp)
          subgoal for m apply(frule RR_PosOf, erule allE[of _ m]) using hh[of x m y z] by(auto) .
        subgoal for x y z 
          apply(rule exI4[of _ 0 "sdrop (Suc 0) x" "sdrop (Suc 0) y" "sdrop (Suc 0) z"])
          apply(intro conjI allI)
          subgoal by auto
          subgoal by auto
          subgoal for i by(erule allE[of _ "Suc i"], simp) . . .*)
end