Theory Checker

(*<*)
theory Checker
  imports Prelim Proof_System Proof_Object "HOL-Library.Simps_Case_Conv"
begin
(*>*)

section ‹Proof Checker›

unbundle MFOTL_syntax

context fixes σ :: "('n, 'd :: {default, linorder}) trace"

begin

fun s_check :: "('n, 'd) env  ('n, 'd) formula  ('n, 'd) sproof  bool"
and v_check :: "('n, 'd) env  ('n, 'd) formula  ('n, 'd) vproof  bool" where
  "s_check v f p = (case (f, p) of
    (, STT i)  True
  | (r  ts, SPred i s ts') 
    (r = s  ts = ts'  (r, vts)  Γ σ i)
  | (x  c, SEq_Const i x' c') 
    (c = c'  x = x'  v x = c)
  | (¬F φ, SNeg vp)  v_check v φ vp
  | (φ F ψ, SOrL sp1)  s_check v φ sp1
  | (φ F ψ, SOrR sp2)  s_check v ψ sp2
  | (φ F ψ, SAnd sp1 sp2)  s_check v φ sp1  s_check v ψ sp2  s_at sp1 = s_at sp2
  | (φ F ψ, SImpL vp1)  v_check v φ vp1
  | (φ F ψ, SImpR sp2)  s_check v ψ sp2
  | (φ F ψ, SIffSS sp1 sp2)  s_check v φ sp1  s_check v ψ sp2  s_at sp1 = s_at sp2
  | (φ F ψ, SIffVV vp1 vp2)  v_check v φ vp1  v_check v ψ vp2  v_at vp1 = v_at vp2
  | (Fx.  φ, SExists y val sp)  (x = y  s_check (v (x := val)) φ sp)
  | (Fx.  φ, SForall y sp_part)  (let i = s_at (part_hd sp_part)
      in x = y  ((sub, sp)  SubsVals sp_part. s_at sp = i  (z  sub. s_check (v (x := z)) φ sp)))
  | (Y I φ, SPrev sp) 
    (let j = s_at sp; i = s_at (SPrev sp) in
    i = j+1  mem (Δ σ i) I  s_check v φ sp)
  | (X I φ, SNext sp) 
    (let j = s_at sp; i = s_at (SNext sp) in
    j = i+1  mem (Δ σ j) I  s_check v φ sp)
  | (P I φ, SOnce i sp) 
    (let j = s_at sp in
    j  i  mem (τ σ i - τ σ j) I  s_check v φ sp)
  | (F I φ, SEventually i sp) 
    (let j = s_at sp in
    j  i  mem (τ σ j - τ σ i) I  s_check v φ sp)
  | (H I φ, SHistoricallyOut i) 
    τ σ i < τ σ 0 + left I
  | (H I φ, SHistorically i li sps) 
    (li = (case right I of   0 | enat b  ETP σ (τ σ i - b))
     τ σ 0 + left I  τ σ i
     map s_at sps = [li ..< (LTP_p σ i I) + 1]
     (sp  set sps. s_check v φ sp))
  | (G I φ, SAlways i hi sps) 
    (hi = (case right I of enat b  LTP_f σ i b)
     right I  
     map s_at sps = [(ETP_f σ i I) ..< hi + 1]
     (sp  set sps. s_check v φ sp))
  | (φ S I ψ, SSince sp2 sp1s) 
    (let i = s_at (SSince sp2 sp1s); j = s_at sp2 in
    j  i  mem (τ σ i - τ σ j) I
     map s_at sp1s = [j+1 ..< i+1]
     s_check v ψ sp2
     (sp1  set sp1s. s_check v φ sp1))
  | (φ U I ψ, SUntil sp1s sp2) 
    (let i = s_at (SUntil sp1s sp2); j = s_at sp2 in
    j  i  mem (τ σ j - τ σ i) I
     map s_at sp1s = [i ..< j]  s_check v ψ sp2
     (sp1  set sp1s. s_check v φ sp1))
  | ( _ , _)  False)"
| "v_check v f p = (case (f, p) of
    (, VFF i)  True
  | (r  ts, VPred i pred ts') 
    (r = pred  ts = ts'  (r, vts)  Γ σ i)
  | (x  c, VEq_Const i x' c') 
    (c = c'  x = x'  v x  c)
  | (¬F φ, VNeg sp)  s_check v φ sp
  | (φ F ψ, VOr vp1 vp2)  v_check v φ vp1  v_check v ψ vp2  v_at vp1 = v_at vp2
  | (φ F ψ, VAndL vp1)  v_check v φ vp1
  | (φ F ψ, VAndR vp2)  v_check v ψ vp2
  | (φ F ψ, VImp sp1 vp2)  s_check v φ sp1  v_check v ψ vp2  s_at sp1 = v_at vp2
  | (φ F ψ, VIffSV sp1 vp2)  s_check v φ sp1  v_check v ψ vp2  s_at sp1 = v_at vp2
  | (φ F ψ, VIffVS vp1 sp2)  v_check v φ vp1  s_check v ψ sp2  v_at vp1 = s_at sp2
  | (Fx.  φ, VExists y vp_part)  (let i = v_at (part_hd vp_part)
      in x = y  ((sub, vp)  SubsVals vp_part. v_at vp = i  (z  sub. v_check (v (x := z)) φ vp)))
  | (Fx.  φ, VForall y val vp)  (x = y  v_check (v (x := val)) φ vp)
  | (Y I φ, VPrev vp) 
    (let j = v_at vp; i = v_at (VPrev vp) in
    i = j+1  v_check v φ vp)
  | (Y I φ, VPrevZ)  True
  | (Y I φ, VPrevOutL i) 
    i > 0  Δ σ i < left I
  | (Y I φ, VPrevOutR i) 
    i > 0  enat (Δ σ i) > right I
  | (X I φ, VNext vp) 
    (let j = v_at vp; i = v_at (VNext vp) in
    j = i+1  v_check v φ vp)
  | (X I φ, VNextOutL i) 
    Δ σ (i+1) < left I
  | (X I φ, VNextOutR i) 
    enat (Δ σ (i+1)) > right I
  | (P I φ, VOnceOut i) 
    τ σ i < τ σ 0 + left I
  | (P I φ, VOnce i li vps) 
    (li = (case right I of   0 | enat b  ETP_p σ i b)
     τ σ 0 + left I  τ σ i
     map v_at vps = [li ..< (LTP_p σ i I) + 1]
     (vp  set vps. v_check v φ vp))
  | (F I φ, VEventually i hi vps) 
    (hi = (case right I of enat b  LTP_f σ i b)  right I  
     map v_at vps = [(ETP_f σ i I) ..< hi + 1]
     (vp  set vps. v_check v φ vp))
  | (H I φ, VHistorically i vp) 
    (let j = v_at vp in
    j  i  mem (τ σ i - τ σ j) I  v_check v φ vp)
  | (G I φ, VAlways i vp) 
    (let j = v_at vp
    in j  i  mem (τ σ j - τ σ i) I  v_check v φ vp)
  | (φ S I ψ, VSinceOut i) 
    τ σ i < τ σ 0 + left I
  | (φ S I ψ, VSince i vp1 vp2s) 
    (let j = v_at vp1 in
    (case right I of   True | enat b  ETP_p σ i b  j)  j  i
     τ σ 0 + left I  τ σ i
     map v_at vp2s = [j ..< (LTP_p σ i I) + 1]  v_check v φ vp1
     (vp2  set vp2s. v_check v ψ vp2))
  | (φ S I ψ, VSinceInf i li vp2s) 
    (li = (case right I of   0 | enat b  ETP_p σ i b)
     τ σ 0 + left I  τ σ i
     map v_at vp2s = [li ..< (LTP_p σ i I) + 1]
     (vp2  set vp2s. v_check v ψ vp2))
  | (φ U I ψ, VUntil i vp2s vp1) 
    (let j = v_at vp1 in
    (case right I of   True | enat b  j < LTP_f σ i b)  i  j
     map v_at vp2s = [ETP_f σ i I ..< j + 1]  v_check v φ vp1
     (vp2  set vp2s. v_check v ψ vp2))
  | (φ U I ψ, VUntilInf i hi vp2s) 
    (hi = (case right I of enat b  LTP_f σ i b)  right I  
     map v_at vp2s = [ETP_f σ i I ..< hi + 1]
     (vp2  set vp2s. v_check v ψ vp2))
  | ( _ , _)  False)"

declare s_check.simps[simp del] v_check.simps[simp del]
simps_of_case s_check_simps[simp]: s_check.simps[unfolded prod.case] (splits: formula.split sproof.split)
simps_of_case v_check_simps[simp]: v_check.simps[unfolded prod.case] (splits: formula.split vproof.split)

subsection ‹Checker Soundness›

lemma check_soundness:
  "s_check v φ sp  SAT σ v (s_at sp) φ"
  "v_check v φ vp  VIO σ v (v_at vp) φ"
proof (induction sp and vp arbitrary: v φ and v φ)
  case STT
  then show ?case by (cases φ) (auto intro: SAT_VIO.STT)
next
  case SPred
  then show ?case by (cases φ) (auto intro: SAT_VIO.SPred)
next
  case SEq_Const
  then show ?case by (cases φ) (auto intro: SAT_VIO.SEq_Const)
next
  case SNeg
  then show ?case by (cases φ) (auto intro: SAT_VIO.SNeg)
next
  case SAnd
  then show ?case by (cases φ) (auto intro: SAT_VIO.SAnd)
next
  case SOrL
  then show ?case by (cases φ) (auto intro: SAT_VIO.SOrL)
next
  case SOrR
  then show ?case by (cases φ) (auto intro: SAT_VIO.SOrR)
next
  case SImpR
  then show ?case by (cases φ) (auto intro: SAT_VIO.SImpR)
next
  case SImpL
  then show ?case by (cases φ) (auto intro: SAT_VIO.SImpL)
next
  case SIffSS
  then show ?case by (cases φ) (auto intro: SAT_VIO.SIffSS)
next
  case SIffVV
  then show ?case by (cases φ) (auto intro: SAT_VIO.SIffVV)
next
  case (SExists x z sp)
  with SExists(1)[of "v(x := z)"] show ?case
    by (cases φ) (auto intro: SAT_VIO.SExists)
next
  case (SForall x part)
  then show ?case
  proof (cases φ)
    case (Forall y ψ)
    show ?thesis unfolding Forall
    proof (intro SAT_VIO.SForall allI)
      fix z
      let ?sp = "lookup_part part z"
      from lookup_part_SubsVals[of z part] obtain D where "z  D" "(D, ?sp)  SubsVals part"
        by blast
      with SForall(2-) Forall have "s_check (v(y := z)) ψ ?sp" "s_at ?sp = s_at (SForall x part)"
        by auto
      then show "SAT σ (v(y := z)) (s_at (SForall x part)) ψ"
        by (auto simp del: fun_upd_apply dest!: SForall(1)[rotated])
    qed
  qed auto
next
  case (SSince spsi sps)
  then show ?case
  proof (cases φ)
    case (Since φ I ψ)
    show ?thesis
      using SSince(3)
      unfolding Since
    proof (intro SAT_VIO.SSince[of "s_at spsi"], goal_cases le mem SATψ SATφ)
      case (SATφ k)
      then show ?case
        by (cases "k  s_at (hd sps)")
          (auto 0 3 simp: Let_def elim: map_setE[of _ _ _ k] intro: SSince(2) dest!: sym[of "s_at _" "Suc (s_at _)"])
    qed (auto simp: Let_def intro: SSince(1))
  qed auto
next
  case (SOnce i sp)
  then show ?case
  proof (cases φ)
    case (Once I φ)
    show ?thesis
      using SOnce
      unfolding Once
      by (intro SAT_VIO.SOnce[of "s_at sp"]) (auto simp: Let_def)
  qed auto
next
  case (SEventually i sp)
  then show ?case
  proof (cases φ)
    case (Eventually I φ)
    show ?thesis
      using SEventually
      unfolding Eventually
      by (intro SAT_VIO.SEventually[of _ "s_at sp"]) (auto simp: Let_def)
  qed auto
next
  case SHistoricallyOut
  then show ?case by (cases φ) (auto intro: SAT_VIO.SHistoricallyOut)
next
  case (SHistorically i li sps)
  then show ?case
  proof (cases φ)
    case (Historically I φ)
    {fix k
      define j where j_def: "j  case right I of   0 | enat n  ETP σ (τ  σ i - n)"
      assume k_def: "k  j  k  i  k  LTP σ (τ σ i - left I)"
      from SHistorically Historically j_def have map: "set (map s_at sps) = set [j ..< Suc (LTP_p σ i I)]"
        by (auto simp: Let_def)
      then have kset: "k  set ([j ..< Suc (LTP_p σ i I)])" using j_def k_def by auto
      then obtain x where x: "x  set sps"  "s_at x = k" using k_def map
        unfolding set_map set_eq_iff image_iff
        by metis
      then have "SAT σ v k φ" using SHistorically unfolding Historically
        by (auto simp: Let_def)
    } note * = this
    show ?thesis
      using SHistorically *
      unfolding Historically
      by (auto simp: Let_def intro!: SAT_VIO.SHistorically)
  qed (auto intro: SAT_VIO.intros)
next
  case (SAlways i hi sps)
  then show ?case
  proof (cases φ)
    case (Always I φ)
    obtain n where n_def: "right I = enat n"
      using SAlways
      by (auto simp: Always split: enat.splits)
    {fix k
      define j where j_def: "j  LTP σ (τ σ i + n)"
      assume k_def: "k  j  k  i  k  ETP σ (τ σ i + left I)"
      from SAlways Always j_def have map: "set (map s_at sps) = set [(ETP_f σ i I) ..< Suc j]"
        by (auto simp: Let_def n_def)
      then have kset: "k  set ([(ETP_f σ i I) ..< Suc j])" using k_def j_def by auto
      then obtain x where x: "x  set sps" "s_at x = k" using k_def map
        unfolding set_map set_eq_iff image_iff
        by metis
      then have "SAT σ v k φ" using SAlways unfolding Always
        by (auto simp: Let_def n_def)
    } note * = this
    then show ?thesis
      using SAlways
      unfolding Always
      by (auto simp: Let_def n_def intro: SAT_VIO.SAlways split: if_splits enat.splits)
  qed(auto intro: SAT_VIO.intros)
next
  case (SUntil sps spsi)
  then show ?case
  proof (cases φ)
    case (Until φ I ψ)
    show ?thesis
      using SUntil(3)
      unfolding Until
    proof (intro SAT_VIO.SUntil[of _ "s_at spsi"], goal_cases le mem SATψ SATφ)
      case (SATφ k)
      then show ?case
        by (cases "k  s_at (hd sps)")
          (auto 0 3 simp: Let_def elim: map_setE[of _ _ _ k] intro: SUntil(1))
    qed (auto simp: Let_def intro: SUntil(2))
  qed auto
next
  case (SNext sp)
  then show ?case by (cases φ) (auto simp add: Let_def SAT_VIO.SNext)
next
  case (SPrev sp)
  then show ?case by (cases φ) (auto simp add: Let_def SAT_VIO.SPrev)
next
  case VFF
  then show ?case by (cases φ) (auto intro: SAT_VIO.VFF)
next
  case VPred
  then show ?case by (cases φ) (auto intro: SAT_VIO.VPred)
next
  case VEq_Const
  then show ?case by (cases φ) (auto intro: SAT_VIO.VEq_Const)
next
  case VNeg
  then show ?case by (cases φ) (auto intro: SAT_VIO.VNeg)
next
  case VOr
  then show ?case by (cases φ) (auto intro: SAT_VIO.VOr)
next
  case VAndL
  then show ?case by (cases φ) (auto intro: SAT_VIO.VAndL)
next
  case VAndR
  then show ?case by (cases φ) (auto intro: SAT_VIO.VAndR)
next
  case VImp
  then show ?case by (cases φ) (auto intro: SAT_VIO.VImp)
next
  case VIffSV
  then show ?case by (cases φ) (auto intro: SAT_VIO.VIffSV)
next
  case VIffVS
  then show ?case by (cases φ) (auto intro: SAT_VIO.VIffVS)
next
  case (VExists x part)
  then show ?case
  proof (cases φ)
    case (Exists y ψ)
    show ?thesis unfolding Exists
    proof (intro SAT_VIO.VExists allI)
      fix z
      let ?vp = "lookup_part part z"
      from lookup_part_SubsVals[of z part] obtain D where "z  D" "(D, ?vp)  SubsVals part"
        by blast
      with VExists(2-) Exists have "v_check (v(y := z)) ψ ?vp" "v_at ?vp = v_at (VExists x part)"
        by auto
      then show "VIO σ (v(y := z)) (v_at (VExists x part)) ψ"
        by (auto simp del: fun_upd_apply dest!: VExists(1)[rotated])
    qed
  qed auto
next
  case (VForall x z vp)
  with VForall(1)[of "v(x := z)"] show ?case
    by (cases φ) (auto intro: SAT_VIO.VForall)
next
  case VOnceOut
  then show ?case by (cases φ) (auto intro: SAT_VIO.VOnceOut)
next
  case (VOnce i li vps)
  then show ?case
  proof (cases φ)
    case (Once I φ)
    {fix k
      define j where j_def: "j  case right I of   0 | enat n  ETP σ (τ σ i - n)"
      assume k_def: "k  j  k  i  k  LTP σ (τ σ i - left I)"
      from VOnce Once j_def have map: "set (map v_at vps) = set [j ..< Suc (LTP_p σ i I)]"
        by (auto simp: Let_def)
      then have kset: "k  set ([j ..< Suc (LTP_p σ i I)])" using j_def k_def by auto
      then obtain x where x: "x  set vps"  "v_at x = k" using k_def map
        unfolding set_map set_eq_iff image_iff
        by metis
      then have "VIO σ v k φ" using VOnce unfolding Once
        by (auto simp: Let_def)
    } note * = this
    show ?thesis
      using VOnce *
      unfolding Once
      by (auto simp: Let_def intro!: SAT_VIO.VOnce)
  qed (auto intro: SAT_VIO.intros)
next
  case (VEventually i hi vps)
  then show ?case
  proof (cases φ)
    case (Eventually I φ)
    obtain n where n_def: "right I = enat n"
      using VEventually
      by (auto simp: Eventually split: enat.splits)
    {fix k
      define j where j_def: "j  LTP σ (τ σ i + n)"
      assume k_def: "k  j  k  i  k  ETP σ (τ σ i + left I)"
      from VEventually Eventually j_def have map: "set (map v_at vps) = set [(ETP_f σ i I) ..< Suc j]"
        by (auto simp: Let_def n_def)
      then have kset: "k  set ([(ETP_f σ i I) ..< Suc j])" using k_def j_def by auto
      then obtain x where x: "x  set vps" "v_at x = k" using k_def map
        unfolding set_map set_eq_iff image_iff
        by metis
      then have "VIO σ v k φ" using VEventually unfolding Eventually
        by (auto simp: Let_def n_def)
    } note * = this
    then show ?thesis
      using VEventually
      unfolding Eventually
      by (auto simp: Let_def n_def intro: SAT_VIO.VEventually split: if_splits enat.splits)
  qed(auto intro: SAT_VIO.intros)
next
  case (VHistorically i vp)
  then show ?case
  proof (cases φ)
    case (Historically I φ)
    show ?thesis
      using VHistorically
      unfolding Historically
      by (intro SAT_VIO.VHistorically[of "v_at vp"]) (auto simp: Let_def)
  qed auto
next
  case (VAlways i vp)
  then show ?case
  proof (cases φ)
    case (Always I φ)
    show ?thesis
      using VAlways
      unfolding Always
      by (intro SAT_VIO.VAlways[of _ "v_at vp"]) (auto simp: Let_def)
  qed auto
next
  case VNext
  then show ?case by (cases φ) (auto intro: SAT_VIO.VNext)
next
  case VNextOutR
  then show ?case by (cases φ) (auto intro: SAT_VIO.VNextOutR)
next
  case VNextOutL
  then show ?case by (cases φ) (auto intro: SAT_VIO.VNextOutL)
next
  case VPrev
  then show ?case by (cases φ) (auto intro: SAT_VIO.VPrev)
next
  case VPrevOutR
  then show ?case by (cases φ) (auto intro: SAT_VIO.VPrevOutR)
next
  case VPrevOutL
  then show ?case by (cases φ) (auto intro: SAT_VIO.VPrevOutL)
next
  case VPrevZ
  then show ?case by (cases φ) (auto intro: SAT_VIO.VPrevZ)
next
  case VSinceOut
  then show ?case by (cases φ) (auto intro: SAT_VIO.VSinceOut)
next
  case (VSince i vp vps)
  then show ?case
  proof (cases φ)
    case (Since φ I ψ)
    {fix k
      assume k_def: "k  v_at vp  k  i  k  LTP σ (τ σ i - left I)"
      from VSince Since have map: "set (map v_at vps) = set ([(v_at vp) ..< Suc (LTP_p σ i I)])"
        by (auto simp: Let_def)
      then have kset: "k  set ([(v_at vp) ..< Suc (LTP_p σ i I)])" using k_def by auto
      then obtain x where x: "x  set vps" "v_at x = k" using k_def map kset
        unfolding set_map set_eq_iff image_iff
        by metis
      then have "VIO σ v k ψ" using VSince unfolding Since
        by (auto simp: Let_def)
    } note * = this
    show ?thesis
      using VSince *
      unfolding Since
      by (auto simp: Let_def split: enat.splits if_splits
          intro!: SAT_VIO.VSince[of _ i "v_at vp"])
  qed (auto intro: SAT_VIO.intros)
next
  case (VUntil i vps vp)
  then show ?case
  proof (cases φ)
    case (Until φ I ψ)
    {fix k
      assume k_def: "k  v_at vp  k  i  k  ETP σ (τ σ i + left I)"
      from VUntil Until have map: "set (map v_at vps) = set [(ETP_f σ i I) ..< Suc (v_at vp)]"
        by (auto simp: Let_def)
      then have kset: "k  set ([(ETP_f σ i I) ..< Suc (v_at vp)])" using k_def by auto
      then obtain x where x: "x  set vps" "v_at x = k" using k_def map kset
        unfolding set_map set_eq_iff image_iff
        by metis
      then have "VIO σ v k ψ" using VUntil unfolding Until
        by (auto simp: Let_def)
    } note * = this
    then show ?thesis
      using VUntil
      unfolding Until
      by (auto simp: Let_def split: enat.splits if_splits
          intro!: SAT_VIO.VUntil)
  qed(auto intro: SAT_VIO.intros)
next
  case (VSinceInf i li vps)
  then show ?case
  proof (cases φ)
    case (Since φ I ψ)
    {fix k
      define j where j_def: "j  case right I of   0 | enat n  ETP σ (τ σ i - n)"
      assume k_def: "k  j  k  i  k  LTP σ (τ σ i - left I)"
      from VSinceInf Since j_def have map: "set (map v_at vps) = set [j ..< Suc (LTP_p σ i I)]"
        by (auto simp: Let_def)
      then have kset: "k  set ([j ..< Suc (LTP_p σ i I)])" using j_def k_def by auto
      then obtain x where x: "x  set vps"  "v_at x = k" using k_def map
        unfolding set_map set_eq_iff image_iff
        by metis
      then have "VIO σ v k ψ" using VSinceInf unfolding Since
        by (auto simp: Let_def)
    } note * = this
    show ?thesis
      using VSinceInf *
      unfolding Since
      by (auto simp: Let_def intro!: SAT_VIO.VSinceInf)
  qed (auto intro: SAT_VIO.intros)
next
  case (VUntilInf i hi vps)
  then show ?case
  proof (cases φ)
    case (Until φ I ψ)
    obtain n where n_def: "right I = enat n"
      using VUntilInf
      by (auto simp: Until split: enat.splits)
    {fix k
      define j where j_def: "j  LTP σ (τ σ i + n)"
      assume k_def: "k  j  k  i  k  ETP σ (τ σ i + left I)"
      from VUntilInf Until j_def have map: "set (map v_at vps) = set [(ETP_f σ i I) ..< Suc j]"
        by (auto simp: Let_def n_def)
      then have kset: "k  set ([(ETP_f σ i I) ..< Suc j])" using k_def j_def by auto
      then obtain x where x: "x  set vps" "v_at x = k" using k_def map
        unfolding set_map set_eq_iff image_iff
        by metis
      then have "VIO σ v k ψ" using VUntilInf unfolding Until
        by (auto simp: Let_def n_def)
    } note * = this
    then show ?thesis
      using VUntilInf
      unfolding Until
      by (auto simp: Let_def n_def intro: SAT_VIO.VUntilInf split: if_splits enat.splits)
  qed(auto intro: SAT_VIO.intros)
qed

definition "compatible X vs v  (xX. v x  vs x)"

definition "compatible_vals X vs = {v. x  X. v x  vs x}"

lemma compatible_alt:
  "compatible X vs v  v  compatible_vals X vs"
  by (auto simp: compatible_def compatible_vals_def)

lemma compatible_empty_iff: "compatible {} vs v  True"
  by (auto simp: compatible_def)

lemma compatible_vals_empty_eq: "compatible_vals {} vs = UNIV"
  by (auto simp: compatible_vals_def)

lemma compatible_union_iff:
  "compatible (X  Y) vs v  compatible X vs v  compatible Y vs v"
  by (auto simp: compatible_def)

lemma compatible_vals_union_eq:
  "compatible_vals (X  Y) vs = compatible_vals X vs  compatible_vals Y vs"
  by (auto simp: compatible_vals_def)

lemma compatible_antimono:
  "compatible X vs v  Y  X  compatible Y vs v"
  by (auto simp: compatible_def)

lemma compatible_vals_antimono:
  "Y  X  compatible_vals X vs  compatible_vals Y vs"
  by (auto simp: compatible_vals_def)

lemma compatible_extensible:
  "(x. vs x  {})  compatible X vs v  X  Y  v'. compatible Y vs v'  (xX. v x = v' x)"
  using some_in_eq[of "vs _"] by (auto simp: override_on_def compatible_def
      intro: exI[where x="override_on v (λx. SOME y. y  vs x) (Y-X)"])

lemmas compatible_vals_extensible = compatible_extensible[unfolded compatible_alt]

primrec mk_values :: "(('n, 'd) trm × 'a set) list  'a list set"
  where "mk_values [] = {[]}"
  | "mk_values (T # Ts) = (case T of
      (v x, X) 
        let terms = map fst Ts in
        if v x  set terms then
          let fst_pos = hd (positions terms (v x)) in (λxs. (xs ! fst_pos) # xs) ` (mk_values Ts)
        else set_Cons X (mk_values Ts)
    | (c a, X)  set_Cons X (mk_values Ts))"

lemma mk_values_nempty:
  "{}  set (map snd tXs)  mk_values tXs  {}"
  by (induct tXs)
    (auto simp: set_Cons_def image_iff split: trm.splits if_splits)

lemma mk_values_not_Nil:
  "{}  set (map snd tXs)  tXs  []  vs  mk_values tXs  vs  []"
  by (induct tXs)
    (auto simp: set_Cons_def image_iff split: trm.splits if_splits)

lemma mk_values_nth_cong: "v x  set (map fst tXs) 
  n  set (positions (map fst tXs) (v x)) 
  m  set (positions (map fst tXs) (v x)) 
  vs  mk_values tXs 
  vs ! n = vs ! m"
proof (induct tXs arbitrary: n m vs x)
  case (Cons tX tXs)
  show ?case
  proof (cases n)
    case 0
    then show ?thesis
    proof (cases m)
      case (Suc m')
      with 0 show ?thesis
        using Cons(2-) Cons.hyps(1)[of x m' _ "tl vs"] positions_eq_nil_iff[of "map fst tXs" "trm.Var x"]
        by (fastforce split: if_splits simp: in_set_conv_nth
            Let_def nth_Cons' gr0_conv_Suc neq_Nil_conv)
    qed simp
  next
    case n: (Suc n')
    then show ?thesis
    proof (cases m)
      case 0
      with n show ?thesis
        using Cons(2-) Cons.hyps(1)[of x _ n' "tl vs"] positions_eq_nil_iff[of "map fst tXs" "trm.Var x"]
        by (fastforce split: if_splits simp: in_set_conv_nth
            Let_def nth_Cons' gr0_conv_Suc neq_Nil_conv)
    next
      case (Suc m')
      with n show ?thesis
        using Cons(1)[of x n' m' "tl vs"] Cons(2-)
        by (fastforce simp: set_Cons_def set_positions_eq split: trm.splits if_splits)
    qed
  qed
qed simp

definition "mk_values_subset p tXs X
   (let (fintXs, inftXs) = partition (λtX. finite (snd tX)) tXs in
  if inftXs = [] then {p} × mk_values tXs  X
  else let inf_dups = filter (λtX. (fst tX)  set (map fst fintXs)) inftXs in
    if inf_dups = [] then (if finite X then False else Code.abort STR ''subset on infinite subset'' (λ_. {p} × mk_values tXs  X))
    else if list_all (λtX. Max (set (positions tXs tX)) < Max (set (positions (map fst tXs) (fst tX)))) inf_dups
      then {p} × mk_values tXs  X
      else (if finite X then False else Code.abort STR ''subset on infinite subset'' (λ_. {p} × mk_values tXs  X)))"

lemma mk_values_nemptyI: "tX  set tXs. snd tX  {}  mk_values tXs  {}"
  by (induct tXs)
    (auto simp: Let_def set_Cons_eq split: prod.splits trm.splits)

lemma infinite_mk_values1: "tX  set tXs. snd tX  {}  tY  set tXs 
  Y. (fst tY, Y)  set tXs  infinite Y  infinite (mk_values tXs)"
proof (induct tXs arbitrary: tY)
  case (Cons tX tXs)
  show ?case
    unfolding Let_def image_iff mk_values.simps split_beta
      trm.split[of infinite] if_split[of infinite]
  proof (safe, goal_cases var_in var_out const)
    case (var_in x)
    hence "tXset tXs. snd tX  {}"
      by (simp add: Cons.prems(1))
    moreover have "Z. (trm.Var x, Z)  set tXs  infinite Z"
      using Cons.prems(2,3) var_in
      by (cases "tY  set tXs"; clarsimp)
        (metis (no_types, lifting) Cons.hyps Cons.prems(1)
          finite_imageD inj_on_def list.inject list.set_intros(2))
    ultimately have "infinite (mk_values tXs)"
      using Cons.hyps var_in
      by auto
    moreover have "inj (λxs. xs ! hd (positions (map fst tXs) (trm.Var x)) # xs)"
      by (clarsimp simp: inj_on_def)
    ultimately show ?case
      using var_in(3) finite_imageD inj_on_subset
      by fastforce
  next
    case (var_out x)
    hence "infinite (snd tX)"
      using Cons
      by (metis infinite_set_ConsI(2) insert_iff list.simps(15) prod.collapse)
    moreover have "mk_values tXs  {}"
      using Cons.prems
      by (auto intro!: mk_values_nemptyI)
    then show ?case
      using Cons var_out infinite_set_ConsI(1)[OF mk_values tXs  {} infinite (snd tX)]
      by auto
  next
    case (const c)
    hence "infinite (snd tX)"
      using Cons
      by (metis infinite_set_ConsI(2) insert_iff list.simps(15) prod.collapse)
    moreover have "mk_values tXs  {}"
      using Cons.prems
      by (auto intro!: mk_values_nemptyI)
    then show ?case
      using Cons const infinite_set_ConsI(1)[OF mk_values tXs  {} infinite (snd tX)]
      by auto
  qed
qed simp

lemma infinite_mk_values2: "tXset tXs. snd tX  {} 
  tY  set tXs  infinite (snd tY) 
  Max (set (positions tXs tY))  Max (set (positions (map fst tXs) (fst tY))) 
  infinite (mk_values tXs)"
proof (induct tXs arbitrary: tY)
  case (Cons tX tXs)
  hence obs1: "tXset tXs. snd tX  {}"
    by (simp add: Cons.prems(1))
  note IH = Cons.hyps[OF obs1 _ infinite (snd tY)]
  have obs2: "tY  set tXs 
    Max (set (positions (map fst tXs) (fst tY)))  Max (set (positions tXs tY))"
    using Cons.prems(4) unfolding list.map
    by (metis Max_set_positions_Cons_tl Suc_le_mono positions_eq_nil_iff set_empty2 subset_empty subset_positions_map_fst)
  show ?case
    unfolding Let_def image_iff mk_values.simps split_beta
      trm.split[of infinite] if_split[of infinite]
  proof (safe, goal_cases var_in var_out const)
    case (var_in x)
    then show ?case
    proof (cases "tY  set tXs")
      case True
      hence "infinite ((λXs. Xs ! hd (positions (map fst tXs) (trm.Var x)) # Xs) ` mk_values tXs)"
        using IH[OF True obs2[OF True]] finite_imageD inj_on_def by blast
      then show "False"
        using var_in by blast
    next
      case False
      have "Max (set (positions (map fst (tX # tXs)) (fst tY)))
      = Suc (Max (set (positions (map fst tXs) (fst tY))))"
        using Cons.prems var_in
        by (simp only: list.map(2))
          (subst Max_set_positions_Cons_tl; force simp: image_iff)
      moreover have "tY  set tXs  Max (set (positions (tX # tXs) tY)) = (0::nat)"
        using Cons.prems Max_set_positions_Cons_hd by fastforce
      ultimately show "False"
        using Cons.prems(4) False
        by linarith
    qed
  next
    case (var_out x)
    then show ?case
    proof (cases "tY  set tXs")
      case True
      hence "infinite (mk_values tXs)"
        using IH obs2 by blast
      hence "infinite (set_Cons (snd tX) (mk_values tXs))"
        by (metis Cons.prems(1) infinite_set_ConsI(2) list.set_intros(1))
      then show "False"
        using var_out by blast
    next
      case False
      hence "snd tY = snd tX" and "infinite (snd tX)"
        using var_out Cons.prems
        by auto
      hence "infinite (set_Cons (snd tX) (mk_values tXs))"
        by (simp add: infinite_set_ConsI(1) mk_values_nemptyI obs1)
      then show "False"
        using var_out by blast
    qed
  next
    case (const c)
    then show ?case
    proof (cases "tY  set tXs")
      case True
      hence "infinite (mk_values tXs)"
        using IH obs2 by blast
      hence "infinite (set_Cons (snd tX) (mk_values tXs))"
        by (metis Cons.prems(1) infinite_set_ConsI(2) list.set_intros(1))
      then show "False"
        using const by blast
    next
      case False
      hence "infinite (set_Cons (snd tX) (mk_values tXs))"
        using const Cons.prems
        by (simp add: infinite_set_ConsI(1) mk_values_nemptyI obs1)
      then show "False"
        using const by blast
    qed
  qed
qed simp

lemma mk_values_subset_iff: "tX  set tXs. snd tX  {} 
   mk_values_subset p tXs X  {p} × mk_values tXs  X"
  unfolding mk_values_subset_def image_iff Let_def comp_def split_beta if_split_eq1
    partition_filter1 partition_filter2 o_def set_map set_filter filter_filter bex_simps
proof safe
  assume "tXset tXs. snd tX  {}" and "finite X"
    and filter1: "filter (λxy. infinite (snd xy)  (ab. (ab  set tXs  finite (snd ab))  fst xy = fst ab)) tXs = []"
    and filter2: "filter (λx. infinite (snd x)) tXs  []"
  then obtain tY where "tY  set tXs" and "infinite (snd tY)"
    by (meson filter_False)
  moreover have "Y. (fst tY, Y)  set tXs  infinite Y"
    using filter1 calculation
    by (auto simp: filter_empty_conv)
  ultimately have "infinite (mk_values tXs)"
    using infinite_mk_values1[OF tXset tXs. snd tX  {}]
    by auto
  hence "infinite ({p} × mk_values tXs)"
    using finite_cartesian_productD2 by auto
  thus "{p} × mk_values tXs  X  False"
    using finite X
    by (simp add: finite_subset)
next
  assume "tXset tXs. snd tX  {}"
    and "finite X"
    and ex_dupl_inf: "¬ list_all (λtX. Max (set (positions tXs tX))
    < Max (set (positions (map fst tXs) (fst tX))))
        (filter (λxy. infinite (snd xy)  (ab. (ab  set tXs  finite (snd ab))  fst xy = fst ab)) tXs)"
    and filter: "filter (λx. infinite (snd x)) tXs  []"
  then obtain tY and Z where "tY  set tXs"
    and "infinite (snd tY)"
    and "(fst tY, Z)  set tXs"
    and "finite Z"
    and "Max (set (positions tXs tY))  Max (set (positions (map fst tXs) (fst tY)))"
    by (auto simp: list_all_iff)
  hence "infinite (mk_values tXs)"
    using infinite_mk_values2[OF tXset tXs. snd tX  {} tY  set tXs]
    by auto
  hence "infinite ({p} × mk_values tXs)"
    using finite_cartesian_productD2 by auto
  thus "{p} × mk_values tXs  X  False"
    using finite X
    by (simp add: finite_subset)
qed auto

lemma mk_values_sound: "cs  mk_values (vsts) 
  vcompatible_vals (fv (r  ts)) vs. cs = vts"
proof (induct ts arbitrary: cs vs)
  case (Cons t ts)
  show ?case
  proof(cases t)
    case (Var x)
    let ?Ts = "vsts"
    have "vs(t # ts) = (v x, vs x) # ?Ts"
      using Var by (simp add: eval_trms_set_def)
    show ?thesis
    proof (cases "v x  set ts")
      case True
      then obtain n where n_in: "n  set (positions ts (v x))"
        and nth_n: "ts ! n = v x"
        by (meson fst_pos_in_positions nth_fst_pos)
      hence n_in': "n  set (positions (map fst ?Ts) (v x))"
        by (induct ts arbitrary: n)
          (auto simp: eval_trms_set_def split: if_splits)
      have key: "v x  set (map fst ?Ts)"
        using True by (induct ts)
          (auto simp: eval_trms_set_def)
      then obtain a as
        where as_head: "as ! (hd (positions (map fst ?Ts) (v x))) = a"
          and as_tail: "as  mk_values ?Ts"
          and as_shape: "cs = a # as"
        using Cons(2)
        by (clarsimp simp add: eval_trms_set_def Var image_iff)
      obtain v where v_hyps: "v  compatible_vals (fv (r  ts)) vs"
        "as = vts"
        using Cons(1)[OF as_tail] by blast
      hence as'_nth: "as ! n = v x"
        using nth_n positions_length[OF n_in]
        by (simp add: eval_trms_def)
      have evals_neq_Nil: "?Ts  []"
        using key by auto
      moreover have "positions (map fst ?Ts) (v x)  []"
        using positions_eq_nil_iff[of "map fst ?Ts" "v x"] key
        by fastforce
      ultimately have as_hyp: "a = as ! n"
        using mk_values_nth_cong[OF key hd_in_set n_in' as_tail] as_head  by blast
      thus ?thesis
        using Var as_shape True v_hyps as'_nth
        by (auto simp: compatible_vals_def eval_trms_def intro!: exI[of _ v])
    next
      case False
      hence *: "v x  set (map fst ?Ts)"
      proof (induct ts arbitrary: x)
        case (Cons a ts)
        then show ?case
          by (cases a) (auto simp: eval_trms_set_def)
      qed (simp add: eval_trms_set_def)
      from Cons(2) False show ?thesis
        unfolding set_Cons_def eval_trms_set_def Let_def list.simps Var
          *[THEN eq_False[THEN iffD2], unfolded eval_trms_set_def] if_False
          mk_values.simps eval_trm_set.simps prod.case trm.case mem_Collect_eq
      proof (elim exE conjE, goal_cases)
        case (1 a as)
        with Cons(1)[of as vs] obtain v where "v  compatible_vals (fv (r  ts)) vs" "as = vts"
          by (auto simp: eval_trms_set_def)
        with 1 show ?case
          by (auto simp: eval_trms_set_def eval_trms_def compatible_vals_def in_fv_trm_conv
            intro!: exI[of _ "v(x := a)"] eval_trm_fv_cong)
      qed
    qed
  next
    case (Const c)
    then show ?thesis
      using Cons(1)[of _ vs] Cons(2)
      by (auto simp: eval_trms_set_def set_Cons_def
          eval_trms_def compatible_def)
  qed
qed (simp add: eval_trms_set_def eval_trms_def compatible_vals_def)

lemma fst_eval_trm_set[simp]:
  "fst (vst) = t"
  by (cases t; clarsimp)

lemma mk_values_complete: "cs = vts 
  v  compatible_vals (fv (r  ts)) vs 
  cs  mk_values (vsts)"
proof (induct ts arbitrary: v cs vs)
  case (Cons t ts)
  then obtain a as
    where a_def: "a = vt"
      and as_def: "as = vts"
      and cs_cons: "cs = a # as"
    by (auto simp: eval_trms_def)
  have compat_v_vs: "v  compatible_vals (fv (r  ts)) vs"
    using Cons.prems
    by (auto simp: compatible_vals_def)
  hence mk_values_ts: "as  mk_values (vsts)"
    using Cons.hyps[OF as_def]
    unfolding eval_trms_set_def by blast
  show ?case
  proof (cases "t")
    case (Var x)
    then show ?thesis
    proof (cases "v x  set ts")
      case True
      then obtain n
        where n_head: "n = hd (positions ts (v x))"
          and n_in: "n  set (positions ts (v x))"
          and nth_n: "ts ! n = v x"
        by (simp_all add: hd_positions_eq_fst_pos nth_fst_pos fst_pos_in_positions)
      hence n_in': "n = hd (positions (map fst (vsts)) (v x))"
        by (clarsimp simp: eval_trms_set_def o_def)
      moreover have "as ! n = a"
        using a_def as_def nth_n Var n_in True positions_length
        by (fastforce simp: eval_trms_def)
      moreover have "v x  set (map fst (vsts))"
        using True by (induct ts)
          (auto simp: eval_trms_set_def)
      ultimately show ?thesis
        using mk_values_ts cs_cons
        by (clarsimp simp: eval_trms_set_def Var image_iff)
    next
      case False
      then show ?thesis
        using Var cs_cons mk_values_ts Cons.prems a_def
        by (clarsimp simp: eval_trms_set_def image_iff
            set_Cons_def compatible_vals_def split: trm.splits)
    qed
  next
    case (Const a)
    then show ?thesis
      using cs_cons mk_values_ts Cons.prems a_def
      by (clarsimp simp: eval_trms_set_def image_iff
          set_Cons_def compatible_vals_def split: trm.splits)
  qed
qed (simp add: compatible_vals_def
    eval_trms_set_def eval_trms_def)

definition "mk_values_subset_Compl r vs ts i = ({r} × mk_values (vsts)  - Γ σ i)"

fun check_values where
  "check_values _ _ _ None = None"
| "check_values vs (c c # ts) (u # us) f = (if c = u then check_values vs ts us f else None)"
| "check_values vs (v x # ts) (u # us) (Some v) = (if u  vs x  (v x = Some u  v x = None) then check_values vs ts us (Some (v(x  u))) else None)"
| "check_values vs [] [] f = f"
| "check_values _ _ _ _ = None"

lemma mk_values_alt:
  "mk_values (vsts) =
   {cs. vcompatible_vals ((fv_trm ` set ts)) vs. cs = vts}"
  by (auto dest!: mk_values_sound intro: mk_values_complete)

lemma check_values_neq_NoneI:
  assumes "v  compatible_vals ( (fv_trm ` set ts) - dom f) vs" "x y. f x = Some y  y  vs x"
  shows "check_values vs ts ((λx. case f x of None  v x | Some y  y)ts) (Some f)  None"
  using assms
proof (induct ts arbitrary: f)
  case (Cons t ts)
  then show ?case
  proof (cases t)
    case (Var x)
    show ?thesis
    proof (cases "f x")
      case None
      with Cons(2) Var have v_in[simp]: "v x  vs x"
        by (auto simp: compatible_vals_def)
      from Cons(2) have "v  compatible_vals ( (fv_trm ` set ts) - dom (f(x  v x))) vs"
        by (auto simp: compatible_vals_def)
      then have "check_values vs ts
        ((λz. case (f(x  v x)) z of None  v z | Some y  y)ts)
        (Some (f(x  v x)))  None"
        using Cons(3) None Var
        by (intro Cons(1)) (auto simp: compatible_vals_def split: if_splits)
      then show ?thesis
        by (elim eq_neq_eq_imp_neq[OF _ _ refl, rotated])
          (auto simp add: eval_trms_def compatible_vals_def Var None split: if_splits option.splits
            intro!: arg_cong2[of _ _ _ _ "check_values vs ts"] eval_trm_fv_cong)
    next
      case (Some y)
      with Cons(1)[of f] Cons(2-) Var fun_upd_triv[of f x] show ?thesis
        by (auto simp: domI eval_trms_def compatible_vals_def split: option.splits)
    qed
  next
    case (Const c)
    with Cons show ?thesis
      by (auto simp: eval_trms_def compatible_vals_def split: option.splits)
  qed
qed (simp add: eval_trms_def)

lemma check_values_eq_NoneI:
  "vcompatible_vals ( (fv_trm ` set ts) - dom f) vs. us  (λx. case f x of None  v x | Some y  y)ts 
  check_values vs ts us (Some f) = None"
proof (induct vs ts us "Some f" arbitrary: f rule: check_values.induct)
  case (3 vs x ts u us v)
  show ?case
    unfolding check_values.simps if_split_eq1 simp_thms
  proof (intro impI 3(1), safe, goal_cases)
    case (1 v')
    with 3(2) show ?case
      by (auto simp: insert_dom domI eval_trms_def intro!: eval_trm_fv_cong split: if_splits dest!: bspec[of _ _ "v'"])
  next
    case (2 v')
    with 3(2) show ?case
      by (auto simp: insert_dom domI compatible_vals_def eval_trms_def intro!: eval_trm_fv_cong split: if_splits option.splits dest!: spec[of _ "v'(x := u)"])
  qed
qed (auto simp: compatible_vals_def eval_trms_def)

lemma mk_values_subset_Compl_code[code]:
  "mk_values_subset_Compl r vs ts i = ((q, us)  Γ σ i. q  r  check_values vs ts us (Some Map.empty) = None)"
  unfolding mk_values_subset_Compl_def eval_trms_set_def[symmetric] mk_values_alt
proof (safe, goal_cases)
  case (1 _ us y)
  then show ?case
    by (auto simp: subset_eq check_values_eq_NoneI[where f=Map.empty, simplified] dest!: spec[of _ us])
qed (auto simp: subset_eq  dest!: check_values_neq_NoneI[where f=Map.empty, simplified])

subsection ‹Executable Variant of the Checker›

fun s_check_exec :: "('n, 'd) envset  ('n, 'd) formula  ('n, 'd) sproof  bool"
and v_check_exec :: "('n, 'd) envset  ('n, 'd) formula  ('n, 'd) vproof  bool" where
  "s_check_exec vs f p = (case (f, p) of
    (, STT i)  True
  | (r  ts, SPred i s ts') 
    (r = s  ts = ts'  mk_values_subset r (vsts) (Γ σ i))
  | (x  c, SEq_Const i x' c') 
    (c = c'  x = x'  vs x = {c})
  | (¬F φ, SNeg vp)  v_check_exec vs φ vp
  | (φ F ψ, SOrL sp1)  s_check_exec vs φ sp1
  | (φ F ψ, SOrR sp2)  s_check_exec vs ψ sp2
  | (φ F ψ, SAnd sp1 sp2)  s_check_exec vs φ sp1  s_check_exec vs ψ sp2  s_at sp1 = s_at sp2
  | (φ F ψ, SImpL vp1)  v_check_exec vs φ vp1
  | (φ F ψ, SImpR sp2)  s_check_exec vs ψ sp2
  | (φ F ψ, SIffSS sp1 sp2)  s_check_exec vs φ sp1  s_check_exec vs ψ sp2  s_at sp1 = s_at sp2
  | (φ F ψ, SIffVV vp1 vp2)  v_check_exec vs φ vp1  v_check_exec vs ψ vp2  v_at vp1 = v_at vp2
  | (Fx.  φ, SExists y val sp)  (x = y  s_check_exec (vs (x := {val})) φ sp)
  | (Fx.  φ, SForall y sp_part)  (let i = s_at (part_hd sp_part)
      in x = y  ((sub, sp)  SubsVals sp_part. s_at sp = i  s_check_exec (vs (x := sub)) φ sp))
  | (Y I φ, SPrev sp) 
    (let j = s_at sp; i = s_at (SPrev sp) in
    i = j+1  mem (Δ σ i) I  s_check_exec vs φ sp)
  | (X I φ, SNext sp) 
    (let j = s_at sp; i = s_at (SNext sp) in
    j = i+1  mem (Δ σ j) I  s_check_exec vs φ sp)
  | (P I φ, SOnce i sp) 
    (let j = s_at sp in
    j  i  mem (τ σ i - τ σ j) I  s_check_exec vs φ sp)
  | (F I φ, SEventually i sp) 
    (let j = s_at sp in
    j  i  mem (τ σ j - τ σ i) I  s_check_exec vs φ sp)
  | (H I φ, SHistoricallyOut i) 
    τ σ i < τ σ 0 + left I
  | (H I φ, SHistorically i li sps) 
    (li = (case right I of   0 | enat b  ETP σ (τ σ i - b))
     τ σ 0 + left I  τ σ i
     map s_at sps = [li ..< (LTP_p σ i I) + 1]
     (sp  set sps. s_check_exec vs φ sp))
  | (G I φ, SAlways i hi sps) 
    (hi = (case right I of enat b  LTP_f σ i b)
     right I  
     map s_at sps = [(ETP_f σ i I) ..< hi + 1]
     (sp  set sps. s_check_exec vs φ sp))
  | (φ S I ψ, SSince sp2 sp1s) 
    (let i = s_at (SSince sp2 sp1s); j = s_at sp2 in
    j  i  mem (τ σ i - τ σ j) I
     map s_at sp1s = [j+1 ..< i+1]
     s_check_exec vs ψ sp2
     (sp1  set sp1s. s_check_exec vs φ sp1))
  | (φ U I ψ, SUntil sp1s sp2) 
    (let i = s_at (SUntil sp1s sp2); j = s_at sp2 in
    j  i  mem (τ σ j - τ σ i) I
     map s_at sp1s = [i ..< j]  s_check_exec vs ψ sp2
     (sp1  set sp1s. s_check_exec vs φ sp1))
  | ( _ , _)  False)"
| "v_check_exec vs f p = (case (f, p) of
    (, VFF i)  True
  | (r  ts, VPred i pred ts') 
    (r = pred  ts = ts'  mk_values_subset_Compl r vs ts i)
  | (x  c, VEq_Const i x' c') 
    (c = c'  x = x'  c  vs x)
  | (¬F φ, VNeg sp)  s_check_exec vs φ sp
  | (φ F ψ, VOr vp1 vp2)  v_check_exec vs φ vp1  v_check_exec vs ψ vp2  v_at vp1 = v_at vp2
  | (φ F ψ, VAndL vp1)  v_check_exec vs φ vp1
  | (φ F ψ, VAndR vp2)  v_check_exec vs ψ vp2
  | (φ F ψ, VImp sp1 vp2)  s_check_exec vs φ sp1  v_check_exec vs ψ vp2  s_at sp1 = v_at vp2
  | (φ F ψ, VIffSV sp1 vp2)  s_check_exec vs φ sp1  v_check_exec vs ψ vp2  s_at sp1 = v_at vp2
  | (φ F ψ, VIffVS vp1 sp2)  v_check_exec vs φ vp1  s_check_exec vs ψ sp2  v_at vp1 = s_at sp2
  | (Fx.  φ, VExists y vp_part)  (let i = v_at (part_hd vp_part)
      in x = y  ((sub, vp)  SubsVals vp_part. v_at vp = i  v_check_exec (vs (x := sub)) φ vp))
  | (Fx.  φ, VForall y val vp)  (x = y  v_check_exec (vs (x := {val})) φ vp)
  | (Y I φ, VPrev vp) 
    (let j = v_at vp; i = v_at (VPrev vp) in
    i = j+1  v_check_exec vs φ vp)
  | (Y I φ, VPrevZ)  True
  | (Y I φ, VPrevOutL i) 
    i > 0  Δ σ i < left I
  | (Y I φ, VPrevOutR i) 
    i > 0  enat (Δ σ i) > right I
  | (X I φ, VNext vp) 
    (let j = v_at vp; i = v_at (VNext vp) in
    j = i+1  v_check_exec vs φ vp)
  | (X I φ, VNextOutL i) 
    Δ σ (i+1) < left I
  | (X I φ, VNextOutR i) 
    enat (Δ σ (i+1)) > right I
  | (P I φ, VOnceOut i) 
    τ σ i < τ σ 0 + left I
  | (P I φ, VOnce i li vps) 
    (li = (case right I of   0 | enat b  ETP_p σ i b)
     τ σ 0 + left I  τ σ i
     map v_at vps = [li ..< (LTP_p σ i I) + 1]
     (vp  set vps. v_check_exec vs φ vp))
  | (F I φ, VEventually i hi vps) 
    (hi = (case right I of enat b  LTP_f σ i b)  right I  
     map v_at vps = [(ETP_f σ i I) ..< hi + 1]
     (vp  set vps. v_check_exec vs φ vp))
  | (H I φ, VHistorically i vp) 
    (let j = v_at vp in
    j  i  mem (τ σ i - τ σ j) I  v_check_exec vs φ vp)
  | (G I φ, VAlways i vp) 
    (let j = v_at vp
    in j  i  mem (τ σ j - τ σ i) I  v_check_exec vs φ vp)
  | (φ S I ψ, VSinceOut i) 
    τ σ i < τ σ 0 + left I
  | (φ S I ψ, VSince i vp1 vp2s) 
    (let j = v_at vp1 in
    (case right I of   True | enat b  ETP_p σ i b  j)  j  i
     τ σ 0 + left I  τ σ i
     map v_at vp2s = [j ..< (LTP_p σ i I) + 1]  v_check_exec vs φ vp1
     (vp2  set vp2s. v_check_exec vs ψ vp2))
  | (φ S I ψ, VSinceInf i li vp2s) 
    (li = (case right I of   0 | enat b  ETP_p σ i b)
     τ σ 0 + left I  τ σ i
     map v_at vp2s = [li ..< (LTP_p σ i I) + 1]
     (vp2  set vp2s. v_check_exec vs ψ vp2))
  | (φ U I ψ, VUntil i vp2s vp1) 
    (let j = v_at vp1 in
    (case right I of   True | enat b  j < LTP_f σ i b)  i  j
     map v_at vp2s = [ETP_f σ i I ..< j + 1]  v_check_exec vs φ vp1
     (vp2  set vp2s. v_check_exec vs ψ vp2))
  | (φ U I ψ, VUntilInf i hi vp2s) 
    (hi = (case right I of enat b  LTP_f σ i b)  right I  
     map v_at vp2s = [ETP_f σ i I ..< hi + 1]
     (vp2  set vp2s. v_check_exec vs ψ vp2))
  | ( _ , _)  False)"

declare s_check_exec.simps[simp del] v_check_exec.simps[simp del]
simps_of_case s_check_exec_simps[simp, code]: s_check_exec.simps[unfolded prod.case] (splits: formula.split sproof.split)
simps_of_case v_check_exec_simps[simp, code]: v_check_exec.simps[unfolded prod.case] (splits: formula.split vproof.split)


lemma check_fv_cong:
  assumes "x  fv φ. v x = v' x"
  shows "s_check v φ sp  s_check v' φ sp" "v_check v φ vp  v_check v' φ vp"
  using assms
proof (induct φ arbitrary: v v' sp vp)
  case TT
  {
    case 1
    then show ?case
      by (cases sp) auto
  next
    case 2
    then show ?case
      by (cases vp) auto
  }
next
  case FF
  {
    case 1
    then show ?case
      by (cases sp) auto
  next
    case 2
    then show ?case
      by (cases vp) auto
  }
next
  case (Pred p ts)
  {
    case 1
    with Pred show ?case using eval_trms_fv_cong[of ts v v']
      by (cases sp) auto
  next
    case 2
    with Pred show ?case using eval_trms_fv_cong[of ts v v']
      by (cases vp) auto
  }
  case (Eq_Const x c)
  {
    case 1
    then show ?case
      by (cases sp) auto
  next
    case 2
    then show ?case
      by (cases vp) auto
  }
next
  case (Neg φ)
  {
    case 1
    with Neg[of v v'] show ?case
      by (cases sp) auto
  next
    case 2
    with Neg[of v v'] show ?case
      by (cases vp) auto
  }
next
  case (Or φ1 φ2)
  {
    case 1
    with Or[of v v'] show ?case
      by (cases sp) auto
  next
    case 2
    with Or[of v v'] show ?case
      by (cases vp) auto
  }
next
  case (And φ1 φ2)
  {
    case 1
    with And[of v v'] show ?case
      by (cases sp) auto
  next
    case 2
    with And[of v v'] show ?case
      by (cases vp) auto
  }
next
  case (Imp φ1 φ2)
  {
    case 1
    with Imp[of v v'] show ?case
      by (cases sp) auto
  next
    case 2
    with Imp[of v v'] show ?case
      by (cases vp) auto
  }
next
  case (Iff φ1 φ2)
  {
    case 1
    with Iff[of v v'] show ?case
      by (cases sp) auto
  next
    case 2
    with Iff[of v v'] show ?case
      by (cases vp) auto
  }
next
  case (Exists x φ)
  {
    case 1
    with Exists[of "v(x := z)" "v'(x := z)" for z] show ?case
      by (cases sp) (auto simp: fun_upd_def)
  next
    case 2
    with Exists[of "v(x := z)" "v'(x := z)" for z] show ?case
      by (cases vp) (auto simp: fun_upd_def)
  }
next
  case (Forall x φ)
  {
    case 1
    with Forall[of "v(x := z)" "v'(x := z)" for z] show ?case
      by (cases sp) (auto simp: fun_upd_def)
  next
    case 2
    with Forall[of "v(x := z)" "v'(x := z)" for z] show ?case
      by (cases vp) (auto simp: fun_upd_def)
  }
next
  case (Prev I φ)
  {
    case 1
    with Prev[of v v'] show ?case
      by (cases sp) auto
  next
    case 2
    with Prev[of v v'] show ?case
      by (cases vp) auto
  }
next
  case (Next I φ)
  {
    case 1
    with Next[of v v'] show ?case
      by (cases sp) auto
  next
    case 2
    with Next[of v v'] show ?case
      by (cases vp) auto
  }
next
  case (Once I φ)
  {
    case 1
    with Once[of v v'] show ?case
      by (cases sp) auto
  next
    case 2
    with Once[of v v'] show ?case
      by (cases vp) auto
  }
next
  case (Historically I φ)
  {
    case 1
    with Historically[of v v'] show ?case
      by (cases sp) auto
  next
    case 2
    with Historically[of v v'] show ?case
      by (cases vp) auto
  }
next
  case (Eventually I φ)
  {
    case 1
    with Eventually[of v v'] show ?case
      by (cases sp) auto
  next
    case 2
    with Eventually[of v v'] show ?case
      by (cases vp) auto
  }
next
  case (Always I φ)
  {
    case 1
    with Always[of v v'] show ?case
      by (cases sp) auto
  next
    case 2
    with Always[of v v'] show ?case
      by (cases vp) auto
  }
next
  case (Since φ1 I φ2)
  {
    case 1
    with Since[of v v'] show ?case
      by (cases sp) auto
  next
    case 2
    with Since[of v v'] show ?case
      by (cases vp) auto
  }
next
  case (Until φ1 I φ2)
  {
    case 1
    with Until[of v v'] show ?case
      by (cases sp) auto
  next
    case 2
    with Until[of v v'] show ?case
      by (cases vp) auto
  }
qed

lemma s_check_fun_upd_notin[simp]:
  "x  fv φ  s_check (v(x := t)) φ sp = s_check v φ sp"
  by (rule check_fv_cong) auto
lemma v_check_fun_upd_notin[simp]:
  "x  fv φ  v_check (v(x := t)) φ sp = v_check v φ sp"
  by (rule check_fv_cong) auto

lemma SubsVals_nonempty: "(X, t)  SubsVals part  X  {}"
  by transfer (auto simp: partition_on_def image_iff)

lemma compatible_vals_nonemptyI: "x. vs x  {}  compatible_vals A vs  {}"
  by (auto simp: compatible_vals_def intro!: bchoice)

lemma compatible_vals_fun_upd: "compatible_vals A (vs(x := X)) =
  (if x  A then {v  compatible_vals (A - {x}) vs. v x  X} else compatible_vals A vs)"
  unfolding compatible_vals_def
  by auto

lemma fun_upd_in_compatible_vals: "v  compatible_vals (A - {x}) vs  v(x := t)  compatible_vals (A - {x}) vs"
  unfolding compatible_vals_def
  by auto

lemma fun_upd_in_compatible_vals_in: "v  compatible_vals (A - {x}) vs  t  vs x  v(x := t)  compatible_vals A vs"
  unfolding compatible_vals_def
  by auto

lemma fun_upd_in_compatible_vals_notin: "x  A  v  compatible_vals A vs  v(x := t)  compatible_vals A vs"
  unfolding compatible_vals_def
  by auto

lemma check_exec_check:
  assumes "x. vs x  {}"
  shows "s_check_exec vs φ sp  (v  compatible_vals (fv φ) vs. s_check v φ sp)"
    and "v_check_exec vs φ vp  (v  compatible_vals (fv φ) vs. v_check v φ vp)"
  using assms
proof (induct φ arbitrary: vs sp vp)
  case TT
  {
    case 1
    then show ?case using compatible_vals_nonemptyI
      by (cases sp)
        auto
  next
    case 2
    then show ?case using compatible_vals_nonemptyI
      by auto
  }
next
  case FF
  {
    case 1
    then show ?case using compatible_vals_nonemptyI
      by (cases sp)
        auto
  next
    case 2
    then show ?case using compatible_vals_nonemptyI
      by (cases vp)
        auto
  }
next
  case (Pred p ts)
  {
    case 1
    have obs: "tXset (vsts). snd tX  {}"
      using x. vs x  {}
    proof (induct ts)
      case (Cons a ts)
      then show ?case
        by (cases a) (auto simp: eval_trms_set_def)
    qed (auto simp: eval_trms_set_def)
    show ?case
      using 1 compatible_vals_nonemptyI[OF 1]
        mk_values_complete[OF refl, of _ p ts vs] mk_values_sound[of _ vs ts p]
      by (cases sp)
        (auto 6 0 simp: mk_values_subset_iff[OF obs] simp del: fv.simps)
  next
    case 2
    then show ?case using compatible_vals_nonemptyI[OF 2]
        mk_values_complete[OF refl, of _ p ts vs] mk_values_sound[of _ vs ts p]
      by (cases vp)
        (auto 6 0 simp: mk_values_subset_Compl_def eval_trms_set_def simp del: fv.simps)
  }
next
  case (Eq_Const x c)
  {
    case 1
    then show ?case
      by (cases sp) (auto simp: compatible_vals_def)
  next
    case 2
    then show ?case
      by (cases vp) (auto simp: compatible_vals_def)
  }
next
  case (Neg φ)
  {
    case 1
    then show ?case
      using Neg.hyps(2) compatible_vals_nonemptyI[OF 1]
      by (cases sp) auto
  next
    case 2
    then show ?case
      using Neg.hyps(1) compatible_vals_nonemptyI[OF 2]
      by (cases vp) auto
  }
next
  case (Or φ1 φ2)
  {
    case 1
    with compatible_vals_nonemptyI[OF 1, of "fv φ1  fv φ2"] show ?case
    proof (cases sp)
      case (SOrL sp')
      from check_fv_cong(1)[of φ1 _ _ sp'] show ?thesis
        unfolding SOrL s_check_exec_simps s_check_simps fv.simps Or(1)[OF 1, of sp']
        by (metis (mono_tags, lifting) 1 IntE Un_upper1 compatible_vals_extensible compatible_vals_union_eq)
    next
      case (SOrR sp')
      from check_fv_cong(1)[of φ2 _ _ sp'] show ?thesis
        unfolding SOrR s_check_exec_simps s_check_simps fv.simps Or(3)[OF 1, of sp']
        by (metis (mono_tags, lifting) 1 IntE Un_upper2 compatible_vals_extensible compatible_vals_union_eq)
    qed (auto simp: compatible_vals_union_eq)
  next
    case 2
    with compatible_vals_nonemptyI[OF 2, of "fv φ1  fv φ2"] show ?case
    proof (cases vp)
      case (VOr vp1 vp2)
      from check_fv_cong(2)[of φ1 _ _ vp1] check_fv_cong(2)[of φ2 _ _ vp2] show ?thesis
        unfolding VOr v_check_exec_simps v_check_simps fv.simps ball_conj_distrib
          Or(2)[OF 2, of vp1]  Or(4)[OF 2, of vp2]
          ball_triv_nonempty[OF compatible_vals_nonemptyI[OF 2, of "fv φ1  fv φ2"]]
      proof (intro arg_cong2[of _ _ _ _ "(∧)"] refl, goal_cases φ1 φ2)
        case φ1
        then show ?case
          by (metis (mono_tags, lifting) 2 IntE Un_upper1 compatible_vals_extensible compatible_vals_union_eq)
      next
        case φ2
        then show ?case
          by (metis (mono_tags, lifting) 2 IntE Un_upper2 compatible_vals_extensible compatible_vals_union_eq)
      qed
    qed (auto simp: compatible_vals_union_eq)
  }
next
  case (And φ1 φ2)
  {
    case 1
    with compatible_vals_nonemptyI[OF 1, of "fv φ1  fv φ2"] show ?case
    proof (cases sp)
      case (SAnd sp1 sp2)
      from check_fv_cong(1)[of φ1 _ _ sp1] check_fv_cong(1)[of φ2 _ _ sp2] show ?thesis
        unfolding SAnd s_check_exec_simps s_check_simps fv.simps ball_conj_distrib
          And(1)[OF 1, of sp1] And(3)[OF 1, of sp2]
          ball_triv_nonempty[OF compatible_vals_nonemptyI[OF 1, of "fv φ1  fv φ2"]]
      proof (intro arg_cong2[of _ _ _ _ "(∧)"] refl, goal_cases φ1 φ2)
        case φ1
        then show ?case
          by (metis (mono_tags, lifting) 1 IntE Un_upper1 compatible_vals_extensible compatible_vals_union_eq)
      next
        case φ2
        then show ?case
          by (metis (mono_tags, lifting) 1 IntE Un_upper2 compatible_vals_extensible compatible_vals_union_eq)
      qed
    qed (auto simp: compatible_vals_union_eq)
  next
    case 2
    with compatible_vals_nonemptyI[OF 2, of "fv φ1  fv φ2"] show ?case
    proof (cases vp)
      case (VAndL vp')
      from check_fv_cong(2)[of φ1 _ _ vp'] show ?thesis
        unfolding VAndL v_check_exec_simps v_check_simps fv.simps And(2)[OF 2, of vp']
        by (metis (mono_tags, lifting) 2 IntE Un_upper1 compatible_vals_extensible compatible_vals_union_eq)
    next
      case (VAndR vp')
      from check_fv_cong(2)[of φ2 _ _ vp'] show ?thesis
        unfolding VAndR v_check_exec_simps v_check_simps fv.simps And(4)[OF 2, of vp']
        by (metis (mono_tags, lifting) 2 IntE Un_upper2 compatible_vals_extensible compatible_vals_union_eq)
    qed (auto simp: compatible_vals_union_eq)
  }
next
  case (Imp φ1 φ2)
  {
    case 1
    with compatible_vals_nonemptyI[OF 1, of "fv φ1  fv φ2"] show ?case
    proof (cases sp)
      case (SImpL vp')
      from check_fv_cong(2)[of φ1 _ _ vp'] show ?thesis
        unfolding SImpL s_check_exec_simps s_check_simps fv.simps Imp(2)[OF 1, of vp']
        by (metis (mono_tags, lifting) 1 IntE Un_upper1 compatible_vals_extensible compatible_vals_union_eq)
    next
      case (SImpR sp')
      from check_fv_cong(1)[of φ2 _ _ sp'] show ?thesis
        unfolding SImpR s_check_exec_simps s_check_simps fv.simps Imp(3)[OF 1, of sp']
        by (metis (mono_tags, lifting) 1 IntE Un_upper2 compatible_vals_extensible compatible_vals_union_eq)
    qed (auto simp: compatible_vals_union_eq)
  next
    case 2
    with compatible_vals_nonemptyI[OF 2, of "fv φ1  fv φ2"] show ?case
    proof (cases vp)
      case (VImp sp1 vp2)
      from check_fv_cong(1)[of φ1 _ _ sp1] check_fv_cong(2)[of φ2 _ _ vp2] show ?thesis
        unfolding VImp v_check_exec_simps v_check_simps fv.simps ball_conj_distrib
          Imp(1)[OF 2, of sp1] Imp(4)[OF 2, of vp2]
          ball_triv_nonempty[OF compatible_vals_nonemptyI[OF 2, of "fv φ1  fv φ2"]]
      proof (intro arg_cong2[of _ _ _ _ "(∧)"] refl, goal_cases φ1 φ2)
        case φ1
        then show ?case
          by (metis (mono_tags, lifting) 2 IntE Un_upper1 compatible_vals_extensible compatible_vals_union_eq)
      next
        case φ2
        then show ?case
          by (metis (mono_tags, lifting) 2 IntE Un_upper2 compatible_vals_extensible compatible_vals_union_eq)
      qed
    qed (auto simp: compatible_vals_union_eq)
  }
next
  case (Iff φ1 φ2)
  {
    case 1
    with compatible_vals_nonemptyI[OF 1, of "fv φ1  fv φ2"] show ?case
    proof (cases sp)
      case (SIffSS sp1 sp2)
      from check_fv_cong(1)[of φ1 _ _ sp1] check_fv_cong(1)[of φ2 _ _ sp2] show ?thesis
        unfolding SIffSS s_check_exec_simps s_check_simps fv.simps ball_conj_distrib
          Iff(1)[OF 1, of sp1] Iff(3)[OF 1, of sp2]
          ball_triv_nonempty[OF compatible_vals_nonemptyI[OF 1, of "fv φ1  fv φ2"]]
      proof (intro arg_cong2[of _ _ _ _ "(∧)"] refl, goal_cases φ1 φ2)
        case φ1
        then show ?case
          by (metis (mono_tags, lifting) 1 IntE Un_upper1 compatible_vals_extensible compatible_vals_union_eq)
      next
        case φ2
        then show ?case
          by (metis (mono_tags, lifting) 1 IntE Un_upper2 compatible_vals_extensible compatible_vals_union_eq)
      qed
    next
      case (SIffVV vp1 vp2)
      from check_fv_cong(2)[of φ1 _ _ vp1] check_fv_cong(2)[of φ2 _ _ vp2] show ?thesis
        unfolding SIffVV s_check_exec_simps s_check_simps fv.simps ball_conj_distrib
          Iff(2)[OF 1, of vp1] Iff(4)[OF 1, of vp2]
          ball_triv_nonempty[OF compatible_vals_nonemptyI[OF 1, of "fv φ1  fv φ2"]]
      proof (intro arg_cong2[of _ _ _ _ "(∧)"] refl, goal_cases φ1 φ2)
        case φ1
        then show ?case
          by (metis (mono_tags, lifting) 1 IntE Un_upper1 compatible_vals_extensible compatible_vals_union_eq)
      next
        case φ2
        then show ?case
          by (metis (mono_tags, lifting) 1 IntE Un_upper2 compatible_vals_extensible compatible_vals_union_eq)
      qed
    qed (auto simp: compatible_vals_union_eq)
  next
    case 2
    with compatible_vals_nonemptyI[OF 2, of "fv φ1  fv φ2"] show ?case
    proof (cases vp)
      case (VIffSV sp1 vp2)
      from check_fv_cong(1)[of φ1 _ _ sp1] check_fv_cong(2)[of φ2 _ _ vp2] show ?thesis
        unfolding VIffSV v_check_exec_simps v_check_simps fv.simps ball_conj_distrib
          Iff(1)[OF 2, of sp1] Iff(4)[OF 2, of vp2]
          ball_triv_nonempty[OF compatible_vals_nonemptyI[OF 2, of "fv φ1  fv φ2"]]
      proof (intro arg_cong2[of _ _ _ _ "(∧)"] refl, goal_cases φ1 φ2)
        case φ1
        then show ?case
          by (metis (mono_tags, lifting) 2 IntE Un_upper1 compatible_vals_extensible compatible_vals_union_eq)
      next
        case φ2
        then show ?case
          by (metis (mono_tags, lifting) 2 IntE Un_upper2 compatible_vals_extensible compatible_vals_union_eq)
      qed
    next
      case (VIffVS vp1 sp2)
      from check_fv_cong(2)[of φ1 _ _ vp1] check_fv_cong(1)[of φ2 _ _ sp2] show ?thesis
        unfolding VIffVS v_check_exec_simps v_check_simps fv.simps ball_conj_distrib
          Iff(2)[OF 2, of vp1] Iff(3)[OF 2, of sp2]
          ball_triv_nonempty[OF compatible_vals_nonemptyI[OF 2, of "fv φ1  fv φ2"]]
      proof (intro arg_cong2[of _ _ _ _ "(∧)"] refl, goal_cases φ1 φ2)
        case φ1
        then show ?case
          by (metis (mono_tags, lifting) 2 IntE Un_upper1 compatible_vals_extensible compatible_vals_union_eq)
      next
        case φ2
        then show ?case
          by (metis (mono_tags, lifting) 2 IntE Un_upper2 compatible_vals_extensible compatible_vals_union_eq)
      qed
    qed (auto simp: compatible_vals_union_eq)
  }
next
  case (Exists x φ)
  {
    case 1
    then have "(vs(x := Z)) y  {}" if "Z  {}" for Z y
      using that by auto
    with 1 have IH:
      "s_check_exec (vs(x := {z})) φ sp = (vcompatible_vals (fv φ) (vs(x := {z})). s_check v φ sp)"
      for z sp
      by (intro Exists;
          auto simp: compatible_vals_fun_upd fun_upd_same
          simp del: fun_upd_apply intro: fun_upd_in_compatible_vals)
    from 1 show ?case
      using compatible_vals_nonemptyI[OF 1, of "fv φ - {x}"]
      by (cases sp) (auto simp: SubsVals_nonempty IH fun_upd_in_compatible_vals_notin compatible_vals_fun_upd)
  next
    case 2
    then have "(vs(x := Z)) y  {}" if "Z  {}" for Z y
      using that by auto
    with 2 have IH:
      "Z  {}  v_check_exec (vs(x := Z)) φ vp = (vcompatible_vals (fv φ) (vs(x := Z)). v_check v φ vp)"
      for Z vp
      by (intro Exists;
          auto simp: compatible_vals_fun_upd fun_upd_same
          simp del: fun_upd_apply intro: fun_upd_in_compatible_vals)
    show ?case
      using compatible_vals_nonemptyI[OF 2, of "fv φ - {x}"]
      by (cases vp)
        (auto simp: SubsVals_nonempty IH[OF SubsVals_nonempty]
          fun_upd_in_compatible_vals fun_upd_in_compatible_vals_notin compatible_vals_fun_upd
          ball_conj_distrib 2[simplified] split: prod.splits if_splits |
          drule bspec, assumption)+
  }
next
  case (Forall x φ)
  {
    case 1
    then have "(vs(x := Z)) y  {}" if "Z  {}" for Z y
      using that by auto
    with 1 have IH:
      "Z  {}  s_check_exec (vs(x := Z)) φ sp = (vcompatible_vals (fv φ) (vs(x := Z)). s_check v φ sp)"
      for Z sp
      by (intro Forall;
          auto simp: compatible_vals_fun_upd fun_upd_same
          simp del: fun_upd_apply intro: fun_upd_in_compatible_vals)
    show ?case
      using compatible_vals_nonemptyI[OF 1, of "fv φ - {x}"]
      by (cases sp)
        (auto simp: SubsVals_nonempty IH[OF SubsVals_nonempty]
          fun_upd_in_compatible_vals fun_upd_in_compatible_vals_notin compatible_vals_fun_upd
          ball_conj_distrib 1[simplified] split: prod.splits if_splits |
          drule bspec, assumption)+
  next
    case 2
    then have "(vs(x := Z)) y  {}" if "Z  {}" for Z y
      using that by auto
    with 2 have IH:
      "v_check_exec (vs(x := {z})) φ vp = (vcompatible_vals (fv φ) (vs(x := {z})). v_check v φ vp)"
      for z vp
      by (intro Forall;
          auto simp: compatible_vals_fun_upd fun_upd_same
          simp del: fun_upd_apply intro: fun_upd_in_compatible_vals)
    from 2 show ?case
      using compatible_vals_nonemptyI[OF 2, of "fv φ - {x}"]
      by (cases vp) (auto simp: SubsVals_nonempty IH fun_upd_in_compatible_vals_notin compatible_vals_fun_upd)
  }
next
  case (Prev I φ)
  {
    case 1
    with Prev[of vs] show ?case
      using compatible_vals_nonemptyI[OF 1, of "fv φ"]
      by (cases sp) auto
  next
    case 2
    with Prev[of vs] show ?case
      using compatible_vals_nonemptyI[OF 2, of "fv φ"]
      by (cases vp) auto
  }
next
  case (Next I φ)
  {
    case 1
    with Next[of vs] show ?case
      using compatible_vals_nonemptyI[OF 1, of "fv φ"]
      by (cases sp) (auto simp: Let_def)
  next
    case 2
    with Next[of vs] show ?case
      using compatible_vals_nonemptyI[OF 2, of "fv φ"]
      by (cases vp) auto
  }
next
  case (Once I φ)
  {
    case 1
    with Once[of vs] show ?case
      using compatible_vals_nonemptyI[OF 1, of "fv φ"]
      by (cases sp) (auto simp: Let_def)
  next
    case 2
    with Once[of vs] show ?case
      using compatible_vals_nonemptyI[OF 2, of "fv φ"]
      by (cases vp) auto
  }
next
  case (Historically I φ)
  {
    case 1
    with Historically[of vs] show ?case
      using compatible_vals_nonemptyI[OF 1, of "fv φ"]
      by (cases sp) auto
  next
    case 2
    with Historically[of vs] show ?case
      using compatible_vals_nonemptyI[OF 2, of "fv φ"]
      by (cases vp) (auto simp: Let_def)
  }
next
  case (Eventually I φ)
  {
    case 1
    with Eventually[of vs] show ?case
      using compatible_vals_nonemptyI[OF 1, of "fv φ"]
      by (cases sp) (auto simp: Let_def)
  next
    case 2
    with Eventually[of vs] show ?case
      using compatible_vals_nonemptyI[OF 2, of "fv φ"]
      by (cases vp) auto
  }
next
  case (Always I φ)
  {
    case 1
    with Always[of vs] show ?case
      using compatible_vals_nonemptyI[OF 1, of "fv φ"]
      by (cases sp) auto
  next
    case 2
    with Always[of vs] show ?case
      using compatible_vals_nonemptyI[OF 2, of "fv φ"]
      by (cases vp) (auto simp: Let_def)
  }
next
  case (Since φ1 I φ2)
  {
    case 1
    with compatible_vals_nonemptyI[OF 1, of "fv φ1  fv φ2"] show ?case
    proof (cases sp)
      case (SSince sp' sps)
      from check_fv_cong(1)[of φ2 _ _ sp'] show ?thesis
        unfolding SSince s_check_exec_simps s_check_simps fv.simps ball_conj_distrib ball_swap[of _ "set sps"]
          Since(1)[OF 1] Since(3)[OF 1, of sp'] Let_def
          ball_triv_nonempty[OF compatible_vals_nonemptyI[OF 1, of "fv φ1  fv φ2"]]
      proof (intro arg_cong2[of _ _ _ _ "(∧)"] ball_cong[of "set sps", OF refl] refl, goal_cases φ2 φ1)
        case φ2
        then show ?case
          by (metis (mono_tags, lifting) 1 IntE Un_upper2 compatible_vals_extensible compatible_vals_union_eq)
      next
        case (φ1 sp)
        then show ?case using check_fv_cong(1)[of φ1 _ _ sp]
          by (metis (mono_tags, lifting) 1 IntE Un_upper1 compatible_vals_extensible compatible_vals_union_eq)
      qed
    qed (auto simp: compatible_vals_union_eq)
  next
    case 2
    with compatible_vals_nonemptyI[OF 2, of "fv φ1  fv φ2"] show ?case
    proof (cases vp)
      case (VSince i vp' vps)
      from check_fv_cong(2)[of φ1 _ _ vp'] show ?thesis
        unfolding VSince v_check_exec_simps v_check_simps fv.simps ball_conj_distrib ball_swap[of _ "set vps"]
          Since(2)[OF 2, of vp'] Since(4)[OF 2] Let_def
          ball_triv_nonempty[OF compatible_vals_nonemptyI[OF 2, of "fv φ1  fv φ2"]]
      proof (intro arg_cong2[of _ _ _ _ "(∧)"] ball_cong[of "set vps", OF refl] refl, goal_cases φ1 φ2)
        case φ1
        then show ?case
          by (metis (mono_tags, lifting) 2 IntE Un_upper2 compatible_vals_extensible compatible_vals_union_eq)
      next
        case (φ2 vp)
        then show ?case using check_fv_cong(2)[of φ2 _ _ vp]
          by (metis (mono_tags, lifting) 2 IntE Un_upper1 compatible_vals_extensible compatible_vals_union_eq)
      qed
    next
      case (VSinceInf i j vps)
      show ?thesis
        unfolding VSinceInf v_check_exec_simps v_check_simps fv.simps ball_conj_distrib ball_swap[of _ "set vps"]
          Since(4)[OF 2] Let_def
          ball_triv_nonempty[OF compatible_vals_nonemptyI[OF 2, of "fv φ1  fv φ2"]]
      proof (intro arg_cong2[of _ _ _ _ "(∧)"] ball_cong[of "set vps", OF refl] refl, goal_cases φ2)
        case (φ2 vp)
        then show ?case using check_fv_cong(2)[of φ2 _ _ vp]
          by (metis (mono_tags, lifting) 2 IntE Un_upper1 compatible_vals_extensible compatible_vals_union_eq)
      qed
    qed (auto simp: compatible_vals_union_eq)
  }
next
  case (Until φ1 I φ2)
  {
    case 1
    with compatible_vals_nonemptyI[OF 1, of "fv φ1  fv φ2"] show ?case
    proof (cases sp)
      case (SUntil sps sp')
      from check_fv_cong(1)[of φ2 _ _ sp'] show ?thesis
        unfolding SUntil s_check_exec_simps s_check_simps fv.simps ball_conj_distrib ball_swap[of _ "set sps"]
          Until(1)[OF 1] Until(3)[OF 1, of sp'] Let_def
          ball_triv_nonempty[OF compatible_vals_nonemptyI[OF 1, of "fv φ1  fv φ2"]]
      proof (intro arg_cong2[of _ _ _ _ "(∧)"] ball_cong[of "set sps", OF refl] refl, goal_cases φ2 φ1)
        case φ2
        then show ?case
          by (metis (mono_tags, lifting) 1 IntE Un_upper2 compatible_vals_extensible compatible_vals_union_eq)
      next
        case (φ1 sp)
        then show ?case using check_fv_cong(1)[of φ1 _ _ sp]
          by (metis (mono_tags, lifting) 1 IntE Un_upper1 compatible_vals_extensible compatible_vals_union_eq)
      qed
    qed (auto simp: compatible_vals_union_eq)
  next
    case 2
    with compatible_vals_nonemptyI[OF 2, of "fv φ1  fv φ2"] show ?case
    proof (cases vp)
      case (VUntil i vps vp')
      from check_fv_cong(2)[of φ1 _ _ vp'] show ?thesis
        unfolding VUntil v_check_exec_simps v_check_simps fv.simps ball_conj_distrib ball_swap[of _ "set vps"]
          Until(2)[OF 2, of vp'] Until(4)[OF 2] Let_def
          ball_triv_nonempty[OF compatible_vals_nonemptyI[OF 2, of "fv φ1  fv φ2"]]
      proof (intro arg_cong2[of _ _ _ _ "(∧)"] ball_cong[of "set vps", OF refl] refl, goal_cases φ1 φ2)
        case φ1
        then show ?case
          by (metis (mono_tags, lifting) 2 IntE Un_upper2 compatible_vals_extensible compatible_vals_union_eq)
      next
        case (φ2 vp)
        then show ?case using check_fv_cong(2)[of φ2 _ _ vp]
          by (metis (mono_tags, lifting) 2 IntE Un_upper1 compatible_vals_extensible compatible_vals_union_eq)
      qed
    next
      case (VUntilInf i j vps)
      show ?thesis
        unfolding VUntilInf v_check_exec_simps v_check_simps fv.simps ball_conj_distrib ball_swap[of _ "set vps"]
          Until(4)[OF 2] Let_def
          ball_triv_nonempty[OF compatible_vals_nonemptyI[OF 2, of "fv φ1  fv φ2"]]
      proof (intro arg_cong2[of _ _ _ _ "(∧)"] ball_cong[of "set vps", OF refl] refl, goal_cases φ2)
        case (φ2 vp)
        then show ?case using check_fv_cong(2)[of φ2 _ _ vp]
          by (metis (mono_tags, lifting) 2 IntE Un_upper1 compatible_vals_extensible compatible_vals_union_eq)
      qed
    qed (auto simp: compatible_vals_union_eq)
  }
qed

lemma s_check_code[code]: "s_check v φ sp = s_check_exec (λx. {v x}) φ sp"
  by (subst check_exec_check)
    (auto simp: compatible_vals_def elim: check_fv_cong[THEN iffD2, rotated])

lemma v_check_code[code]: "v_check v φ vp = v_check_exec (λx. {v x}) φ vp"
  by (subst check_exec_check)
    (auto simp: compatible_vals_def elim: check_fv_cong[THEN iffD2, rotated])

subsection ‹Latest Relevant Time-Point›

fun LRTP :: "('n, 'd) formula  nat  nat option" where
  "LRTP  i = Some i"
| "LRTP  i = Some i"
| "LRTP (_  _) i = Some i"
| "LRTP (_  _) i = Some i"
| "LRTP (¬F φ) i = LRTP φ i"
| "LRTP (φ F ψ) i = max_opt (LRTP φ i) (LRTP ψ i)"
| "LRTP (φ F ψ) i = max_opt (LRTP φ i) (LRTP ψ i)"
| "LRTP (φ F ψ) i = max_opt (LRTP φ i) (LRTP ψ i)"
| "LRTP (φ F ψ) i = max_opt (LRTP φ i) (LRTP ψ i)"
| "LRTP (F_. φ) i = LRTP φ i"
| "LRTP (F_. φ) i = LRTP φ i"
| "LRTP (Y I φ) i = LRTP φ (i-1)"
| "LRTP (X I φ) i = LRTP φ (i+1)"
| "LRTP (P I φ) i = LRTP φ (LTP_p_safe σ i I)"
| "LRTP (H I φ) i = LRTP φ (LTP_p_safe σ i I)"
| "LRTP (F I φ) i = (case right I of   None | enat b  LRTP φ (LTP_f σ i b))"
| "LRTP (G I φ) i = (case right I of   None | enat b  LRTP φ (LTP_f σ i b))" 
| "LRTP (φ S I ψ) i = max_opt (LRTP φ i) (LRTP ψ (LTP_p_safe σ i I))"
| "LRTP (φ U I ψ) i = (case right I of   None | enat b  max_opt (LRTP φ ((LTP_f σ i b)-1)) (LRTP ψ (LTP_f σ i b)))"

lemma fb_LRTP: 
  assumes "future_bounded φ"
  shows "¬ Option.is_none (LRTP φ i)"
  using assms
  by (induction φ i rule: LRTP.induct) 
    (auto simp add: max_opt_def Option.is_none_def)

lemma not_none_fb_LRTP:
  assumes "future_bounded φ"
  shows "LRTP φ i  None"
  using assms fb_LRTP by (auto simp add: Option.is_none_def)

lemma is_some_fb_LRTP:
  assumes "future_bounded φ"
  shows "j. LRTP φ i = Some j"
  using assms fb_LRTP by (auto simp add: Option.is_none_def)

lemma enat_trans[simp]: "enat i  enat j  enat j  enat k  enat i  enat k"
  by auto

subsection ‹Active Domain›

definition AD :: "('n, 'd) formula  nat  'd set"
  where "AD φ i = consts φ  ( k  the (LRTP φ i).  (set ` snd ` Γ σ k))"

lemma val_in_AD_iff:
  "x  fv φ  v x  AD φ i  v x  consts φ 
  (r ts k. k  the (LRTP φ i)  (r, vts)  Γ σ k  x   (set (map fv_trm ts)))"
  unfolding AD_def Un_iff UN_iff Bex_def atMost_iff set_map
    ex_comm[of "P :: _  nat  _" for P] ex_simps image_iff
proof (safe intro!: arg_cong[of _ _ "λx. _  x"] ex_cong, unfold snd_conv, goal_cases LR RL)
  case (LR i _ r ds)
  then show ?case
    by (intro exI[of _ r] conjI
        exI[of _ "map (λd. if v x = d then (v x) else c d) ds"])
      (auto simp: eval_trms_def o_def map_idI)
next
  case (RL i r ts t)
  then show ?case
    by (intro exI[of _ "vts"] conjI)
      (auto simp: eval_trms_def image_iff in_fv_trm_conv intro!: bexI[of _ t])
qed

lemma val_notin_AD_iff:
  "x  fv φ  v x  AD φ i  v x  consts φ 
    (r ts k. k  the (LRTP φ i)  x   (set (map fv_trm ts))  (r, vts)  Γ σ k)"
  using val_in_AD_iff by blast

lemma finite_values: "finite ( (set ` snd ` Γ σ k))"
  by (transfer, auto simp add: sfinite_def)

lemma finite_tps: "future_bounded φ  finite ( k < the (LRTP φ i). {k})"
  using fb_LRTP[of φ] finite_enat_bounded
  by simp

lemma finite_AD [simp]: "future_bounded φ  finite (AD φ i)"
  using finite_tps finite_values
  by (simp add: AD_def enat_def)

lemma finite_AD_UNIV:
  assumes "future_bounded φ" and "AD φ i = (UNIV:: 'd set)"
  shows "finite (UNIV::'d set)"
proof -
  have "finite (AD φ i)"
    using finite_AD[of φ i, OF assms(1)] by simp
  then show ?thesis
    using assms(2) by simp
qed

subsection ‹Congruence Modulo Active Domain›

lemma AD_simps[simp]:
  "AD (¬F φ) i = AD φ i"
  "future_bounded (φ F ψ)  AD (φ F ψ) i = AD φ i  AD ψ i"
  "future_bounded (φ F ψ)  AD (φ F ψ) i = AD φ i  AD ψ i"
  "future_bounded (φ F ψ)  AD (φ F ψ) i = AD φ i  AD ψ i"
  "future_bounded (φ F ψ)  AD (φ F ψ) i = AD φ i  AD ψ i"
  "AD (Fx.  φ) i = AD φ i"
  "AD (Fx.  φ) i = AD φ i"
  "AD (Y I φ) i = AD φ (i - 1)"
  "AD (X I φ) i = AD φ (i + 1)"
  "future_bounded (F I φ)  AD (F I φ) i = AD φ (LTP_f σ i (the_enat (right I)))"
  "future_bounded (G I φ)  AD (G I φ) i = AD φ (LTP_f σ i (the_enat (right I)))"
  "AD (P I φ) i = AD φ (LTP_p_safe σ i I)"
  "AD (H I φ) i = AD φ (LTP_p_safe σ i I)"
  "future_bounded (φ S I ψ)  AD (φ S I ψ) i = AD φ i  AD ψ (LTP_p_safe σ i I)"
  "future_bounded (φ U I ψ)  AD (φ U I ψ) i = AD φ (LTP_f σ i (the_enat (right I)) - 1)  AD ψ (LTP_f σ i (the_enat (right I)))"
  by (auto 0 3 simp: AD_def max_opt_def not_none_fb_LRTP le_max_iff_disj Bex_def split: option.splits)


lemma LTP_p_mono: "i  j  LTP_p_safe σ i I  LTP_p_safe σ j I"
  unfolding LTP_p_safe_def
  by (smt (verit, ccfv_threshold) τ_mono bot_nat_0.extremum diff_le_mono order.trans i_LTP_tau le_cases3 min.bounded_iff)

lemma LTP_f_mono:
  assumes "i  j"
  shows"LTP_f σ i b  LTP_f σ j b"
  unfolding LTP_def
proof (rule Max_mono)
  show "finite {i. τ σ i  τ σ j + b}"
    unfolding finite_nat_set_iff_bounded_le
    by (metis i_le_LTPi_add le_Suc_ex mem_Collect_eq)
qed (auto simp: assms intro!: exI[of _ i] elim: order_trans)

lemma LRTP_mono: "future_bounded φ  i  j  the (LRTP φ i)  the (LRTP φ j)"
proof (induct φ arbitrary: i j)
  case (Or φ1 φ2)
  from Or(1,2)[of i j] Or(3-) show ?case
    by (auto simp: max_opt_def not_none_fb_LRTP split: option.splits)
next
  case (And φ1 φ2)
  from And(1,2)[of i j] And(3-) show ?case
    by (auto simp: max_opt_def not_none_fb_LRTP split: option.splits)
next
  case (Imp φ1 φ2)
  from Imp(1,2)[of i j] Imp(3-) show ?case
    by (auto simp: max_opt_def not_none_fb_LRTP split: option.splits)
next
  case (Iff φ1 φ2)
  from Iff(1,2)[of i j] Iff(3-) show ?case
    by (auto simp: max_opt_def not_none_fb_LRTP split: option.splits)
next
  case (Since φ1 I φ2)
  from Since(1)[OF _ Since(4)] Since(2)[of "LTP_p_safe σ i I" "LTP_p_safe σ j I"] Since(3-)
  show ?case
    by (auto simp: max_opt_def not_none_fb_LRTP LTP_p_mono split: option.splits)
next
  case (Until φ1 I φ2)
  from Until(1)[of "LTP_f σ i (the_enat (right I)) - 1" "LTP_f σ j (the_enat (right I)) - 1"]
    Until(2)[of "LTP_f σ i (the_enat (right I))" "LTP_f σ j (the_enat (right I))"] Until(3-)
  show ?case
    by (auto simp: max_opt_def not_none_fb_LRTP LTP_f_mono diff_le_mono split: option.splits)
qed (auto simp: LTP_p_mono LTP_f_mono)

lemma AD_mono: "future_bounded φ  i  j  AD φ i  AD φ j"
  by (auto 0 3 simp: AD_def Bex_def intro: LRTP_mono elim!: order_trans)

lemma LTP_p_safe_le[simp]: "LTP_p_safe σ i I  i"
  by (auto simp: LTP_p_safe_def)

lemma check_AD_cong:
  assumes "future_bounded φ"
    and "(x  fv φ. v x = v' x  (v x  AD φ i  v' x  AD φ i))"
  shows "(s_at sp = i  s_check v φ sp  s_check v' φ sp)"
    "(v_at vp = i  v_check v φ vp  v_check v' φ vp)"
  using assms
proof (induction v φ sp and v φ vp arbitrary: i v' and i v' rule: s_check_v_check.induct)
  case (1 v f sp)
  note IH = 1(1-23)[OF refl] and hyps = 1(24-26)
  show ?case
  proof (cases sp)
    case (SPred j r ts)
    then show ?thesis
    proof (cases f)
      case (Pred q us)
      with SPred hyps show ?thesis
        using eval_trms_fv_cong[of ts v v']
        by (force simp: val_notin_AD_iff dest!: spec[of _ i] spec[of _ r] spec[of _ ts])
    qed auto
  next
    case (SEq_Const j r ts)
    with hyps show ?thesis
      by (cases f) (auto simp: val_notin_AD_iff)
  next
    case (SNeg vp')
    then show ?thesis
      using IH(1)[of _ _ _ v'] hyps
      by (cases f) auto
  next
    case (SOrL sp')
    then show ?thesis
      using IH(2)[of _ _ _ _ v'] hyps
      by (cases f) auto
  next
    case (SOrR sp')
    then show ?thesis
      using IH(3)[of _ _ _ _ v'] hyps
      by (cases f) auto
  next
    case (SAnd sp1 sp2)
    then show ?thesis
      using IH(4,5)[of _ _ _ _ _ v'] hyps
      by (cases f) (auto 7 0)+
  next
    case (SImpL vp')
    then show ?thesis
      using IH(6)[of _ _ _ _ v'] hyps
      by (cases f) auto
  next
    case (SImpR sp')
    then show ?thesis
      using IH(7)[of _ _ _ _ v'] hyps
      by (cases f) auto
  next
    case (SIffSS sp1 sp2)
    then show ?thesis
      using IH(8,9)[of _ _ _ _ _ v'] hyps
      by (cases f) (auto 7 0)+
  next
    case (SIffVV vp1 vp2)
    then show ?thesis
      using IH(10,11)[of _ _ _ _ _ v'] hyps
      by (cases f) (auto 7 0)+
  next
    case (SExists x z sp')
    then show ?thesis
      using IH(12)[of x _ x z sp' i "v'(x := z)"] hyps
      by (cases f) (auto simp add: fun_upd_def)
  next
    case (SForall x part)
    then show ?thesis
      using IH(13)[of x _ x part _ _ D _ z _ "v'(x := z)" for D z, OF _ _ _ _  refl _ refl] hyps
      by (cases f) (auto simp add: fun_upd_def)
  next
    case (SPrev sp')
    then show ?thesis
      using IH(14)[of _ _ _ _ _ _ v'] hyps
      by (cases f) auto
  next
    case (SNext sp')
    then show ?thesis
      using IH(15)[of _ _ _ _ _ _ v'] hyps
      by (cases f) (auto simp add: Let_def)
  next
    case (SOnce j sp')
    then show ?thesis
    proof (cases f)
      case (Once I φ)
      { fix k
        assume k: "k  i" "τ σ i - left I  τ σ k"
        then have "τ σ i - left I  τ σ 0"
          by (meson τ_mono le0 order_trans)
        with k have "k  LTP_p_safe σ i I"
          unfolding LTP_p_safe_def by (auto simp: i_LTP_tau)
        with Once hyps(2,3) have "xfv φ. v x = v' x  v x  AD φ k  v' x  AD φ k"
          by (auto dest!: bspec dest: AD_mono[THEN set_mp, rotated -1])
      }
      with Once SOnce show ?thesis
        using IH(16)[OF Once SOnce refl refl, of v'] hyps(1,2)
        by (auto simp: Let_def le_diff_conv2)
    qed auto
  next
    case (SHistorically j k sps)
    then show ?thesis
    proof (cases f)
      case (Historically I φ)
      { fix sp :: "('n, 'd) sproof"
        define l and u where "l = s_at sp" and "u = LTP_p σ i I"
        assume *: "sp  set sps" "τ σ 0 + left I  τ σ i"
        then have u_def: "u = LTP_p_safe σ i I"
          by (auto simp: LTP_p_safe_def u_def)
        from *(1) obtain j where j: "sp = sps ! j" "j < length sps"
          unfolding in_set_conv_nth by auto
        moreover
        assume eq: "map s_at sps = [k ..< Suc u]"
        then have len: "length sps = Suc u - k"
          by (auto dest!: arg_cong[where f=length])
        moreover
        have "s_at (sps ! j) = k + j"
          using arg_cong[where f="λxs. nth xs j", OF eq] j len *(2)
          by (auto simp: nth_append)
        ultimately have "l  u"
          unfolding l_def by auto
        with Historically hyps(2,3) have "xfv φ. v x = v' x  v x  AD φ l  v' x  AD φ l"
          by (auto simp: u_def dest!: bspec dest: AD_mono[THEN set_mp, rotated -1])
      }
      with Historically SHistorically show ?thesis
        using IH(17)[OF Historically SHistorically _ refl, of _ v'] hyps(1,2)
        by auto
    qed auto
  next
    case (SEventually j sp')
    then show ?thesis
    proof (cases f)
      case (Eventually I φ)
      { fix k
        assume "τ σ k  the_enat (right I) + τ σ i"
        then have "k  LTP_f σ i (the_enat (right I))"
          by (metis add.commute i_le_LTPi_add le_add_diff_inverse)
        with Eventually hyps(2,3) have "xfv φ. v x = v' x  v x  AD φ k  v' x  AD φ k"
          by (auto dest!: bspec dest: AD_mono[THEN set_mp, rotated -1])
      }
      with Eventually SEventually show ?thesis
        using IH(18)[OF Eventually SEventually refl refl, of v'] hyps(1,2)
        by (auto simp: Let_def)
    qed auto
  next
    case (SAlways j k sps)
    then show ?thesis
    proof (cases f)
      case (Always I φ)
      { fix sp :: "('n, 'd) sproof"
        define l and u where "l = s_at sp" and "u = LTP_f σ i (the_enat (right I))"
        assume *: "sp  set sps"
        then obtain j where j: "sp = sps ! j" "j < length sps"
          unfolding in_set_conv_nth by auto
        assume eq: "map s_at sps = [ETP_f σ i I ..< Suc u]"
        then have "length sps = Suc u - ETP_f σ i I"
          by (auto dest!: arg_cong[where f=length])
        with j eq have "l  LTP_f σ i (the_enat (right I))"
          by (auto simp: l_def u_def dest!: arg_cong[where f="λxs. nth xs j"]
              simp del: upt.simps split: if_splits)
        with Always hyps(2,3) have "xfv φ. v x = v' x  v x  AD φ l  v' x  AD φ l"
          by (auto dest!: bspec dest: AD_mono[THEN set_mp, rotated -1])
      }
      with Always SAlways show ?thesis
        using IH(19)[OF Always SAlways _ refl, of _ v'] hyps(1,2)
        by auto
    qed auto
  next
    case (SSince sp' sps)
    then show ?thesis
    proof (cases f)
      case (Since φ I ψ)
      { fix sp :: "('n, 'd) sproof"
        define l where "l = s_at sp"
        assume *: "sp  set sps"
        from *(1) obtain j where j: "sp = sps ! j" "j < length sps"
          unfolding in_set_conv_nth by auto
        moreover
        assume eq: "map s_at sps = [Suc (s_at sp')  ..< Suc i]"
        then have len: "length sps = i - s_at sp'"
          by (auto dest!: arg_cong[where f=length])
        moreover
        have "s_at (sps ! j) = Suc (s_at sp') + j"
          using arg_cong[where f="λxs. nth xs j", OF eq] j len
          by (auto simp: nth_append)
        ultimately have "l  i"
          unfolding l_def by auto
        with Since hyps(2,3) have "xfv φ. v x = v' x  v x  AD φ l  v' x  AD φ l"
          by (auto simp: dest!: bspec dest: AD_mono[THEN set_mp, rotated -1])
      }
      moreover
      { fix k
        assume k: "k  i" "τ σ i - left I  τ σ k"
        then have "τ σ i - left I  τ σ 0"
          by (meson τ_mono le0 order_trans)
        with k have "k  LTP_p_safe σ i I"
          unfolding LTP_p_safe_def by (auto simp: i_LTP_tau)
        with Since hyps(2,3) have "xfv ψ. v x = v' x  v x  AD ψ k  v' x  AD ψ k"
          by (auto dest!: bspec dest: AD_mono[THEN set_mp, rotated -1])
      }
      ultimately show ?thesis
        using Since SSince IH(20)[OF Since SSince refl refl refl, of v'] IH(21)[OF Since SSince refl refl _ refl, of _ v'] hyps(1,2)
        by (auto simp: Let_def le_diff_conv2 simp del: upt.simps)
    qed auto
  next
    case (SUntil sps sp')
    then show ?thesis
    proof (cases f)
      case (Until φ I ψ)
      { fix sp :: "('n, 'd) sproof"
        define l where "l = s_at sp"
        assume *: "sp  set sps"
        from *(1) obtain j where j: "sp = sps ! j" "j < length sps"
          unfolding in_set_conv_nth by auto
        moreover
        assume "δ σ (s_at sp') i  the_enat (right I)"
        then have "s_at sp'  LTP_f σ i (the_enat (right I))"
          by (metis add.commute i_le_LTPi_add le_add_diff_inverse le_diff_conv)
        moreover
        assume eq: "map s_at sps = [i ..< s_at sp']"
        then have len: "length sps = s_at sp' - i"
          by (auto dest!: arg_cong[where f=length])
        moreover
        have "s_at (sps ! j) = i + j"
          using arg_cong[where f="λxs. nth xs j", OF eq] j len
          by (auto simp: nth_append)
        ultimately have "l  LTP_f σ i (the_enat (right I)) - 1"
          unfolding l_def by auto
        with Until hyps(2,3) have "xfv φ. v x = v' x  v x  AD φ l  v' x  AD φ l"
          by (auto simp: dest!: bspec dest: AD_mono[THEN set_mp, rotated -1])
      }
      moreover
      { fix k
        assume "τ σ k  the_enat (right I) + τ σ i"
        then have "k  LTP_f σ i (the_enat (right I))"
          by (metis add.commute i_le_LTPi_add le_add_diff_inverse)
        with Until hyps(2,3) have "xfv ψ. v x = v' x  v x  AD ψ k  v' x  AD ψ k"
          by (auto dest!: bspec dest: AD_mono[THEN set_mp, rotated -1])
      }
      ultimately show ?thesis
        using Until SUntil IH(22)[OF Until SUntil refl refl refl, of v'] IH(23)[OF Until SUntil refl refl _ refl, of _ v'] hyps(1,2)
        by (auto simp: Let_def le_diff_conv2 simp del: upt.simps)
    qed auto
  qed (cases f; simp_all)+
next
  case (2 v f vp)
  note IH = 2(1-25)[OF refl] and hyps = 2(26-28)
  show ?case
  proof (cases vp)
    case (VPred j r ts)
    then show ?thesis
    proof (cases f)
      case (Pred q us)
      with VPred hyps show ?thesis
        using eval_trms_fv_cong[of ts v v']
        by (force simp: val_notin_AD_iff dest!: spec[of _ i] spec[of _ r] spec[of _ ts])
    qed auto
  next
    case (VEq_Const j r ts)
    with hyps show ?thesis
      by (cases f) (auto simp: val_notin_AD_iff)
  next
    case (VNeg sp')
    then show ?thesis
      using IH(1)[of _ _ _ v'] hyps
      by (cases f) auto
  next
    case (VOr vp1 vp2)
    then show ?thesis
      using IH(2,3)[of _ _ _ _ _ v'] hyps
      by (cases f) (auto 7 0)+
  next
    case (VAndL vp')
    then show ?thesis
      using IH(4)[of _ _ _ _ v'] hyps
      by (cases f) auto
  next
    case (VAndR vp')
    then show ?thesis
      using IH(5)[of _ _ _ _ v'] hyps
      by (cases f) auto
  next
    case (VImp sp1 vp2)
    then show ?thesis
      using IH(6,7)[of _ _ _ _ _ v'] hyps
      by (cases f) (auto 7 0)+
  next
    case (VIffSV sp1 vp2)
    then show ?thesis
      using IH(8,9)[of _ _ _ _ _ v'] hyps
      by (cases f) (auto 7 0)+
  next
    case (VIffVS vp1 sp2)
    then show ?thesis
      using IH(10,11)[of _ _ _ _ _ v'] hyps
      by (cases f) (auto 7 0)+
  next
    case (VExists x part)
    then show ?thesis
      using IH(12)[of x _ x part _ _ D _ z _ "v'(x := z)" for D z, OF _ _ _ _  refl _ refl] hyps
      by (cases f) (auto simp add: fun_upd_def)
  next
    case (VForall x z vp')
    then show ?thesis
      using IH(13)[of x _ x z vp' i "v'(x := z)"] hyps
      by (cases f) (auto simp add: fun_upd_def)
  next
    case (VPrev vp')
    then show ?thesis
      using IH(14)[of _ _ _ _ _ _ v'] hyps
      by (cases f) auto
  next
    case (VNext vp')
    then show ?thesis
      using IH(15)[of _ _ _ _ _ _ v'] hyps
      by (cases f) auto
  next
    case (VOnce j k vps)
    then show ?thesis
    proof (cases f)
      case (Once I φ)
      { fix vp :: "('n, 'd) vproof"
        define l and u where "l = v_at vp" and "u = LTP_p σ i I"
        assume *: "vp  set vps" "τ σ 0 + left I  τ σ i"
        then have u_def: "u = LTP_p_safe σ i I"
          by (auto simp: LTP_p_safe_def u_def)
        from *(1) obtain j where j: "vp = vps ! j" "j < length vps"
          unfolding in_set_conv_nth by auto
        moreover
        assume eq: "map v_at vps = [k ..< Suc u]"
        then have len: "length vps = Suc u - k"
          by (auto dest!: arg_cong[where f=length])
        moreover
        have "v_at (vps ! j) = k + j"
          using arg_cong[where f="λxs. nth xs j", OF eq] j len *(2)
          by (auto simp: nth_append)
        ultimately have "l  u"
          unfolding l_def by auto
        with Once hyps(2,3) have "xfv φ. v x = v' x  v x  AD φ l  v' x  AD φ l"
          by (auto simp: u_def dest!: bspec dest: AD_mono[THEN set_mp, rotated -1])
      }
      with Once VOnce show ?thesis
        using IH(16)[OF Once VOnce _ refl, of _ v'] hyps(1,2)
        by auto
    qed auto
  next
    case (VHistorically j vp')
    then show ?thesis
    proof (cases f)
      case (Historically I φ)
      { fix k
        assume k: "k  i" "τ σ i - left I  τ σ k"
        then have "τ σ i - left I  τ σ 0"
          by (meson τ_mono le0 order_trans)
        with k have "k  LTP_p_safe σ i I"
          unfolding LTP_p_safe_def by (auto simp: i_LTP_tau)
        with Historically hyps(2,3) have "xfv φ. v x = v' x  v x  AD φ k  v' x  AD φ k"
          by (auto dest!: bspec dest: AD_mono[THEN set_mp, rotated -1])
      }
      with Historically VHistorically show ?thesis
        using IH(17)[OF Historically VHistorically refl refl, of v'] hyps(1,2)
        by (auto simp: Let_def le_diff_conv2)
    qed auto
  next
    case (VEventually j k vps)
    then show ?thesis
    proof (cases f)
      case (Eventually I φ)
      { fix vp :: "('n, 'd) vproof"
        define l and u where "l = v_at vp" and "u = LTP_f σ i (the_enat (right I))"
        assume *: "vp  set vps"
        then obtain j where j: "vp = vps ! j" "j < length vps"
          unfolding in_set_conv_nth by auto
        assume eq: "map v_at vps = [ETP_f σ i I ..< Suc u]"
        then have "length vps = Suc u - ETP_f σ i I"
          by (auto dest!: arg_cong[where f=length])
        with j eq have "l  LTP_f σ i (the_enat (right I))"
          by (auto simp: l_def u_def dest!: arg_cong[where f="λxs. nth xs j"]
              simp del: upt.simps split: if_splits)
        with Eventually hyps(2,3) have "xfv φ. v x = v' x  v x  AD φ l  v' x  AD φ l"
          by (auto dest!: bspec dest: AD_mono[THEN set_mp, rotated -1])
      }
      with Eventually VEventually show ?thesis
        using IH(18)[OF Eventually VEventually _ refl, of _ v'] hyps(1,2)
        by auto
    qed auto
  next
    case (VAlways j vp')
    then show ?thesis
    proof (cases f)
      case (Always I φ)
      { fix k
        assume "τ σ k  the_enat (right I) + τ σ i"
        then have "k  LTP_f σ i (the_enat (right I))"
          by (metis add.commute i_le_LTPi_add le_add_diff_inverse)
        with Always hyps(2,3) have "xfv φ. v x = v' x  v x  AD φ k  v' x  AD φ k"
          by (auto dest!: bspec dest: AD_mono[THEN set_mp, rotated -1])
      }
      with Always VAlways show ?thesis
        using IH(19)[OF Always VAlways refl refl, of v'] hyps(1,2)
        by (auto simp: Let_def)
    qed auto
  next
    case (VSince j vp' vps)
    then show ?thesis
    proof (cases f)
      case (Since φ I ψ)
      { fix sp :: "('n, 'd) vproof"
        define l and u where "l = v_at sp" and "u = LTP_p σ i I"
        assume *: "sp  set vps" "τ σ 0 + left I  τ σ i"
        then have u_def: "u = LTP_p_safe σ i I"
          by (auto simp: LTP_p_safe_def u_def)
        from *(1) obtain j where j: "sp = vps ! j" "j < length vps"
          unfolding in_set_conv_nth by auto
        moreover
        assume eq: "map v_at vps = [v_at vp'  ..< Suc u]"
        then have len: "length vps = Suc u - v_at vp'"
          by (auto dest!: arg_cong[where f=length])
        moreover
        have "v_at (vps ! j) = v_at vp' + j"
          using arg_cong[where f="λxs. nth xs j", OF eq] j len
          by (auto simp: nth_append)
        ultimately have "l  u"
          unfolding l_def by auto
        with Since hyps(2,3) have "xfv ψ. v x = v' x  v x  AD ψ l  v' x  AD ψ l"
          by (auto simp: u_def dest!: bspec dest: AD_mono[THEN set_mp, rotated -1])
      }
      moreover
      { fix k
        assume k: "k  i"
        with Since hyps(2,3) have "xfv φ. v x = v' x  v x  AD φ k  v' x  AD φ k"
          by (auto dest!: bspec dest: AD_mono[THEN set_mp, rotated -1])
      }
      ultimately show ?thesis
        using Since VSince IH(20)[OF Since VSince refl refl, of v'] IH(21)[OF Since VSince refl _ refl, of _ v'] hyps(1,2)
        by (auto simp: Let_def le_diff_conv2 simp del: upt.simps)
    qed auto
  next
    case (VSinceInf j k vps)
    then show ?thesis
    proof (cases f)
      case (Since φ I ψ)
      { fix vp :: "('n, 'd) vproof"
        define l and u where "l = v_at vp" and "u = LTP_p σ i I"
        assume *: "vp  set vps" "τ σ 0 + left I  τ σ i"
        then have u_def: "u = LTP_p_safe σ i I"
          by (auto simp: LTP_p_safe_def u_def)
        from *(1) obtain j where j: "vp = vps ! j" "j < length vps"
          unfolding in_set_conv_nth by auto
        moreover
        assume eq: "map v_at vps = [k ..< Suc u]"
        then have len: "length vps = Suc u - k"
          by (auto dest!: arg_cong[where f=length])
        moreover
        have "v_at (vps ! j) = k + j"
          using arg_cong[where f="λxs. nth xs j", OF eq] j len *(2)
          by (auto simp: nth_append)
        ultimately have "l  u"
          unfolding l_def by auto
        with Since hyps(2,3) have "xfv ψ. v x = v' x  v x  AD ψ l  v' x  AD ψ l"
          by (auto simp: u_def dest!: bspec dest: AD_mono[THEN set_mp, rotated -1])
      }
      with Since VSinceInf show ?thesis
        using IH(22)[OF Since VSinceInf _ refl, of _ v'] hyps(1,2)
        by auto
    qed auto
  next
    case (VUntil j vps vp')
    then show ?thesis
    proof (cases f)
      case (Until φ I ψ)
      { fix sp :: "('n, 'd) vproof"
        define l and u where "l = v_at sp" and "u = v_at vp'"
        assume *: "sp  set vps" "v_at vp'  LTP_f σ i (the_enat (right I))"
        from *(1) obtain j where j: "sp = vps ! j" "j < length vps"
          unfolding in_set_conv_nth by auto
        moreover
        assume eq: "map v_at vps = [ETP_f σ i I ..< Suc u]"
        then have "length vps = Suc u - ETP_f σ i I"
          by (auto dest!: arg_cong[where f=length])
        with j eq *(2) have "l  LTP_f σ i (the_enat (right I))"
          by (auto simp: l_def u_def dest!: arg_cong[where f="λxs. nth xs j"]
              simp del: upt.simps split: if_splits)
        with Until hyps(2,3) have "xfv ψ. v x = v' x  v x  AD ψ l  v' x  AD ψ l"
          by (auto dest!: bspec dest: AD_mono[THEN set_mp, rotated -1])
      }
      moreover
      { fix k
        assume "k < LTP_f σ i (the_enat (right I))"
        then have "k  LTP_f σ i (the_enat (right I)) - 1"
          by linarith
        with Until hyps(2,3) have "xfv φ. v x = v' x  v x  AD φ k  v' x  AD φ k"
          by (auto dest!: bspec dest: AD_mono[THEN set_mp, rotated -1])
      }
      ultimately show ?thesis
        using Until VUntil IH(23)[OF Until VUntil refl refl, of v'] IH(24)[OF Until VUntil refl _ refl, of _ v'] hyps(1,2)
        by (auto simp: Let_def le_diff_conv2 simp del: upt.simps)
    qed auto
  next
    case (VUntilInf j k vps)
    then show ?thesis
    proof (cases f)
      case (Until φ I ψ)
      { fix vp :: "('n, 'd) vproof"
        define l and u where "l = v_at vp" and "u = LTP_f σ i (the_enat (right I))"
        assume *: "vp  set vps"
        then obtain j where j: "vp = vps ! j" "j < length vps"
          unfolding in_set_conv_nth by auto
        assume eq: "map v_at vps = [ETP_f σ i I ..< Suc u]"
        then have "length vps = Suc u - ETP_f σ i I"
          by (auto dest!: arg_cong[where f=length])
        with j eq have "l  LTP_f σ i (the_enat (right I))"
          by (auto simp: l_def u_def dest!: arg_cong[where f="λxs. nth xs j"]
              simp del: upt.simps split: if_splits)
        with Until hyps(2,3) have "xfv ψ. v x = v' x  v x  AD ψ l  v' x  AD ψ l"
          by (auto dest!: bspec dest: AD_mono[THEN set_mp, rotated -1])
      }
      with Until VUntilInf show ?thesis
        using IH(25)[OF Until VUntilInf _ refl, of _ v'] hyps(1,2)
        by auto
    qed auto
  qed (cases f; simp_all)+
qed

subsection ‹Checker Completeness›

lemma part_hd_tabulate: "distinct xs  part_hd (tabulate xs f z) = (case xs of []  z | (x # _)  (if set xs = UNIV then f x else z))"
  by (transfer, auto split: list.splits)

lemma s_at_tabulate:
  assumes "z. s_at (mypick z) = i"
    and "mypart = tabulate (sorted_list_of_set (AD φ i)) mypick (mypick (SOME z. z  AD φ i))"
  shows "(sub, vp)  SubsVals mypart. s_at vp = i"
  using assms by (transfer, auto)

lemma v_at_tabulate:
  assumes "z. v_at (mypick z) = i"
    and "mypart = tabulate (sorted_list_of_set (AD φ i)) mypick (mypick (SOME z. z  AD φ i))"
  shows "(sub, vp)  SubsVals mypart. v_at vp = i"
  using assms by (transfer, auto)

lemma s_check_tabulate:
  assumes "future_bounded φ"
    and "z. s_at (mypick z) = i"
    and "z. s_check (v(x:=z)) φ (mypick z)"
    and "mypart = tabulate (sorted_list_of_set (AD φ i)) mypick (mypick (SOME z. z  AD φ i))"
  shows "(sub, vp)  SubsVals mypart. z  sub. s_check (v(x := z)) φ vp"
  using assms
proof (transfer fixing: σ φ mypick i v x, goal_cases 1)
  case (1 mypart)
  { fix z
    assume s_at_assm: "z. s_at (mypick z) = i"
      and s_check_assm: "z. s_check (v(x := z)) φ (mypick z)"
      and fb_assm: "future_bounded φ"
      and z_notin_AD: "z  (AD φ i)"
    have s_at_mypick: "s_at (mypick (SOME z. z  local.AD φ i)) = i"
      using s_at_assm by simp
    have s_check_mypick: "Checker.s_check σ (v(x := SOME z. z  AD φ i)) φ (mypick (SOME z. z  AD φ i))"
      using s_check_assm by simp
    have "s_check (v(x := z)) φ (mypick (SOME z. z  AD φ i))"
      using z_notin_AD
      by (subst check_AD_cong(1)[of φ "v(x := z)" "v(x := (SOME z. z  Checker.AD σ φ i))" i "mypick (SOME z. z  AD φ i)", OF fb_assm _ s_at_mypick])
        (auto simp add: someI[of "λz. z  AD φ i" z] s_check_mypick fb_assm split: if_splits)
  }
  with 1 show ?case
    by auto
qed

lemma v_check_tabulate:
  assumes "future_bounded φ"
    and "z. v_at (mypick z) = i"
    and "z. v_check (v(x:=z)) φ (mypick z)"
    and "mypart = tabulate (sorted_list_of_set (AD φ i)) mypick (mypick (SOME z. z  AD φ i))"
  shows "(sub, vp)  SubsVals mypart. z  sub. v_check (v(x := z)) φ vp"
  using assms
proof (transfer fixing: σ φ mypick i v x, goal_cases 1)
  case (1 mypart)
  { fix z
    assume v_at_assm: "z. v_at (mypick z) = i"
      and v_check_assm: "z. v_check (v(x := z)) φ (mypick z)"
      and fb_assm: "future_bounded φ"
      and z_notin_AD: "z  (AD φ i)"
    have v_at_mypick: "v_at (mypick (SOME z. z  local.AD φ i)) = i"
      using v_at_assm by simp
    have v_check_mypick: "Checker.v_check σ (v(x := SOME z. z  AD φ i)) φ (mypick (SOME z. z  AD φ i))"
      using v_check_assm by simp
    have "v_check (v(x := z)) φ (mypick (SOME z. z  AD φ i))"
      using z_notin_AD
      by (subst check_AD_cong(2)[of φ "v(x := z)" "v(x := (SOME z. z  Checker.AD σ φ i))" i "mypick (SOME z. z  AD φ i)", OF fb_assm _ v_at_mypick])
        (auto simp add: someI[of "λz. z  AD φ i" z] v_check_mypick fb_assm split: if_splits)
  }
  with 1 show ?case
    by auto
qed

lemma s_at_part_hd_tabulate:
  assumes "future_bounded φ"
    and "z. s_at (f z) = i"
    and "mypart = tabulate (sorted_list_of_set (AD φ i)) f (f (SOME z. z  AD φ i))"
  shows "s_at (part_hd mypart) = i"
  using assms by (simp add: part_hd_tabulate split: list.splits)

lemma v_at_part_hd_tabulate:
  assumes "future_bounded φ"
    and "z. v_at (f z) = i"
    and "mypart = tabulate (sorted_list_of_set (AD φ i)) f (f (SOME z. z  AD φ i))"
  shows "v_at (part_hd mypart) = i"
  using assms by (simp add: part_hd_tabulate split: list.splits)

lemma check_completeness_aux:
  "(SAT σ v i φ  future_bounded φ  (sp. s_at sp = i  s_check v φ sp)) 
   (VIO σ v i φ  future_bounded φ  (vp. v_at vp = i  v_check v φ vp))"
proof (induct v i φ rule: SAT_VIO.induct)
  case (STT v i)
  then show ?case
    by (auto intro!: exI[of _ "STT i"])
next
  case (VFF v i)
  then show ?case
    by (auto intro!: exI[of _ "VFF i"])
next
  case (SPred r v ts i)
  then show ?case
    by (auto intro!: exI[of _ "SPred i r ts"])
next
  case (VPred r v ts i)
  then show ?case
    by (auto intro!: exI[of _ "VPred i r ts"])
next
  case (SEq_Const v x c i)
  then show ?case
    by (auto intro!: exI[of _ "SEq_Const i x c"])
next
  case (VEq_Const v x c i)
  then show ?case
    by (auto intro!: exI[of _ "VEq_Const i x c"])
next
  case (SNeg v i φ)
  then show ?case
    by (auto intro: exI[of _ "SNeg _"])
next
  case (VNeg v i φ)
  then show ?case
    by (auto intro: exI[of _ "VNeg _"])
next
  case (SOrL v i φ ψ)
  then show ?case
    by (auto intro: exI[of _ "SOrL _"])
next
  case (SOrR v i ψ φ)
  then show ?case
    by (auto intro: exI[of _ "SOrR _"])
next
  case (VOr v i φ ψ)
  then show ?case
    by (auto 0 3 intro: exI[of _ "VOr _ _"])
next
  case (SAnd v i φ ψ)
  then show ?case
    by (auto 0 3 intro: exI[of _ "SAnd _ _"])
next
  case (VAndL v i φ ψ)
  then show ?case
    by (auto intro: exI[of _ "VAndL _"])
next
  case (VAndR v i ψ φ)
  then show ?case
    by (auto intro: exI[of _ "VAndR _"])
next
  case (SImpL v i φ ψ)
  then show ?case
    by (auto intro: exI[of _ "SImpL _"])
next
  case (SImpR v i ψ φ)
  then show ?case
    by (auto intro: exI[of _ "SImpR _"])
next
  case (VImp v i φ ψ)
  then show ?case
    by (auto 0 3 intro: exI[of _ "VImp _ _"])
next
  case (SIffSS v i φ ψ)
  then show ?case
    by (auto 0 3 intro: exI[of _ "SIffSS _ _"])
next
  case (SIffVV v i φ ψ)
  then show ?case
    by (auto 0 3 intro: exI[of _ "SIffVV _ _"])
next
  case (VIffSV v i φ ψ)
  then show ?case
    by (auto 0 3 intro: exI[of _ "VIffSV _ _"])
next
  case (VIffVS v i φ ψ)
  then show ?case
    by (auto 0 3 intro: exI[of _ "VIffVS _ _"])
next
  case (SExists v x i φ)
  then show ?case
    by (auto 0 3 simp: fun_upd_def intro: exI[of _ "SExists x _ _"])
next
  case (VExists v x i φ)
  show ?case
  proof
    assume "future_bounded (Fx.  φ)"
    then have fb: "future_bounded φ"
      by simp
    obtain mypick where mypick_def: "v_at (mypick z) = i  v_check (v(x:=z)) φ (mypick z)" for z
      using VExists fb by metis
    define mypart where "mypart = tabulate (sorted_list_of_set (AD φ i)) mypick (mypick (SOME z. z  (AD φ i)))"
    have mypick_at: "z. v_at (mypick z) = i"
      by (simp add: mypick_def)
    have mypick_v_check: "z. v_check (v(x:=z)) φ (mypick z)"
      by (simp add: mypick_def)
    have mypick_v_check2: "z. v_check (v(x := (SOME z. z  AD φ i))) φ (mypick (SOME z. z  AD φ i))"
      by (simp add: mypick_def)
    have v_at_myp: "v_at (VExists x mypart) = i"
      using v_at_part_hd_tabulate[OF fb, of mypick i]
      by (simp add: mypart_def mypick_def)
    have v_check_myp: "v_check v (Fx.  φ) (VExists x mypart)"
      using v_at_tabulate[of mypick i _ φ, OF mypick_at]
        v_check_tabulate[OF fb mypick_at mypick_v_check]
      by (auto simp add: mypart_def v_at_part_hd_tabulate[OF fb mypick_at])
    show "vp. v_at vp = i  v_check v (Fx.  φ) vp"
      using v_at_myp v_check_myp by blast
  qed
next
  case (SForall v x i φ)
  show ?case
  proof
    assume "future_bounded (Fx.  φ)"
    then have fb: "future_bounded φ"
      by simp
    obtain mypick where mypick_def: "s_at (mypick z) = i  s_check (v(x:=z)) φ (mypick z)" for z
      using SForall fb by metis
    define mypart where "mypart = tabulate (sorted_list_of_set (AD φ i)) mypick (mypick (SOME z. z  (AD φ i)))"
    have mypick_at: "z. s_at (mypick z) = i"
      by (simp add: mypick_def)
    have mypick_s_check: "z. s_check (v(x:=z)) φ (mypick z)"
      by (simp add: mypick_def)
    have mypick_s_check2: "z. s_check (v(x := (SOME z. z  AD φ i))) φ (mypick (SOME z. z  AD φ i))"
      by (simp add: mypick_def)
    have s_at_myp: "s_at (SForall x mypart) = i"
      using s_at_part_hd_tabulate[OF fb, of mypick i]
      by (simp add: mypart_def mypick_def)
    have s_check_myp: "s_check v (Fx.  φ) (SForall x mypart)"
      using s_at_tabulate[of mypick i _ φ, OF mypick_at]
        s_check_tabulate[OF fb mypick_at mypick_s_check]
      by (auto simp add: mypart_def s_at_part_hd_tabulate[OF fb mypick_at])
    show "sp. s_at sp = i  s_check v (Fx.  φ) sp"
      using s_at_myp s_check_myp by blast
  qed
next
  case (VForall v x i φ)
  then show ?case
    by (auto 0 3 simp: fun_upd_def intro: exI[of _ "VForall x _ _"])
next
  case (SPrev i I v φ)
  then show ?case
    by (force intro: exI[of _ "SPrev _"])
next
  case (VPrev i v φ I)
  then show ?case
    by (force intro: exI[of _ "VPrev _"])
next
  case (VPrevZ i v I φ)
  then show ?case
    by (auto intro!: exI[of _ "VPrevZ"])
next
  case (VPrevOutL i I v φ)
  then show ?case
    by (auto intro!: exI[of _ "VPrevOutL i"])
next
  case (VPrevOutR i I v φ)
  then show ?case
    by (auto intro!: exI[of _ "VPrevOutR i"])
next
  case (SNext i I v φ)
  then show ?case
    by (force simp: Let_def intro: exI[of _ "SNext _"])
next
  case (VNext v i φ I)
  then show ?case
    by (force simp: Let_def intro: exI[of _ "VNext _"])
next
  case (VNextOutL i I v φ)
  then show ?case
    by (auto intro!: exI[of _ "VNextOutL i"])
next
  case (VNextOutR i I v φ)
  then show ?case
    by (auto intro!: exI[of _ "VNextOutR i"])
next
  case (SOnce j i I v φ)
  then show ?case
    by (auto simp: Let_def intro: exI[of _ "SOnce i _"])
next
  case (VOnceOut i I v φ)
  then show ?case
    by (auto intro!: exI[of _ "VOnceOut i"])
next
  case (VOnce j I i v φ)
  show ?case
  proof
    assume "future_bounded (P I φ)"
    then have fb: "future_bounded φ"
      by simp
    obtain mypick where mypick_def: "k  {j .. LTP_p σ i I}. v_at (mypick k) = k  v_check v φ (mypick k)"
      using VOnce fb by metis
    then obtain vps where vps_def: "map (v_at) vps = [j ..< Suc (LTP_p σ i I)]  (vp  set vps. v_check v φ vp)"
      by atomize_elim (auto intro!: trans[OF list.map_cong list.map_id] exI[of _ "map mypick ([j ..< Suc (LTP_p σ i I)])"])
    then have "v_at (VOnce i j vps) = i  v_check v (P I φ) (VOnce i j vps)"
      using VOnce by auto
    then show "vp. v_at vp = i  v_check v (P I φ) vp"
      by blast
  qed
next
  case (SEventually j i I v φ)
  then show ?case
    by (auto simp: Let_def intro: exI[of _ "SEventually i _"])
next
  case (VEventually I i v φ)
  show ?case
  proof
    assume fb_eventually: "future_bounded (F I φ)"
    then have fb: "future_bounded φ"
      by simp
    obtain b where b_def: "right I = enat b"
      using fb_eventually by (atomize_elim, cases "right I") auto
    define j where j_def: "j = LTP σ (τ σ i + b)"
    obtain mypick where mypick_def: "k  {ETP_f σ i I .. j}. v_at (mypick k) = k  v_check v φ (mypick k)"
      using VEventually fb_eventually unfolding b_def j_def enat.simps
      by atomize_elim (rule bchoice, simp)
    then obtain vps where vps_def: "map (v_at) vps = [ETP_f σ i I ..< Suc j]  (vp  set vps. v_check v φ vp)"
      by atomize_elim (auto intro!: trans[OF list.map_cong list.map_id] exI[of _ "map mypick ([ETP_f σ i I ..< Suc j])"])
    then have "v_at (VEventually i j vps) = i  v_check v (F I φ) (VEventually i j vps)"
      using VEventually b_def j_def by simp
    then show "vp. v_at vp = i  v_check v (F I φ) vp"
      by blast
  qed
next
  case (SHistorically j I i v φ)
  show ?case
  proof
    assume fb_historically: "future_bounded (H I φ)"
    then have fb: "future_bounded φ"
      by simp
    obtain mypick where mypick_def: "k  {j .. LTP_p σ i I}. s_at (mypick k) = k  s_check v φ (mypick k)"
      using SHistorically fb by metis
    then obtain sps where sps_def: "map (s_at) sps = [j ..< Suc (LTP_p σ i I)]  (sp  set sps. s_check v φ sp)"
      by atomize_elim (auto intro!: trans[OF list.map_cong list.map_id] exI[of _ "map mypick ([j ..< Suc (LTP_p σ i I)])"])
    then have "s_at (SHistorically i j sps) = i  s_check v (H I φ) (SHistorically i j sps)"
      using SHistorically by auto
    then show "sp. s_at sp = i  s_check v (H I φ) sp"
      by blast
  qed
next
  case (SHistoricallyOut i I v φ)
  then show ?case
    by (auto intro!: exI[of _ "SHistoricallyOut i"])
next
  case (VHistorically j i I v φ)
  then show ?case
    by (auto simp: Let_def intro: exI[of _ "VHistorically i _"])
next
  case (SAlways I i v φ)
  show ?case
  proof
    assume fb_always: "future_bounded (G I φ)"
    then have fb: "future_bounded φ"
      by simp
    obtain b where b_def: "right I = enat b"
      using fb_always by (atomize_elim, cases "right I") auto
    define j where j_def: "j = LTP σ (τ σ i + b)"
    obtain mypick where mypick_def: "k  {ETP_f σ i I .. j}. s_at (mypick k) = k  s_check v φ (mypick k)"
      using SAlways fb_always unfolding b_def j_def enat.simps
      by atomize_elim (rule bchoice, simp)
    then obtain sps where sps_def: "map (s_at) sps = [ETP_f σ i I ..< Suc j]  (sp  set sps. s_check v φ sp)"
      by atomize_elim (auto intro!: trans[OF list.map_cong list.map_id] exI[of _ "map mypick ([ETP_f σ i I ..< Suc j])"])
    then have "s_at (SAlways i j sps) = i  s_check v (G I φ) (SAlways i j sps)"
      using SAlways b_def j_def by simp
    then show "sp. s_at sp = i  s_check v (G I φ) sp"
      by blast
  qed
next
  case (VAlways j i I v φ)
  then show ?case
    by (auto simp: Let_def intro: exI[of _ "VAlways i _"])
next
  case (SSince j i I v ψ φ)
  show ?case
  proof
    assume fb_since: "future_bounded (φ S I ψ)"
    then have fb: "future_bounded φ" "future_bounded ψ"
      by simp_all
    obtain sp2 where sp2_def: "s_at sp2 = j  s_check v ψ sp2"
      using SSince fb_since by auto
    {
      assume "Suc j > i"
      then have "s_at (SSince sp2 []) = i  s_check v (φ S I ψ) (SSince sp2 [])"
        using sp2_def SSince by auto
      then have "sp. s_at sp = i  s_check v (φ S I ψ) sp"
        by blast
    }
    moreover
    {
      assume sucj_leq_i: "Suc j  i"
      obtain mypick where mypick_def: "k  {Suc j ..< Suc i}. s_at (mypick k) = k  s_check v φ (mypick k)"
        using SSince fb_since by atomize_elim (rule bchoice, simp)
      then obtain sp1s where sp1s_def: "map (s_at) sp1s = [Suc j ..< Suc i]  (sp  set sp1s. s_check v φ sp)"
        by atomize_elim (auto intro!: trans[OF list.map_cong list.map_id] exI[of _ "map mypick ([Suc j ..< Suc i])"])
      then have "sp1s  []"
        using sucj_leq_i by auto
      then have "s_at (SSince sp2 sp1s) = i  s_check v (φ S I ψ) (SSince sp2 sp1s)"
        using SSince sucj_leq_i fb sp2_def sp1s_def
        by (clarsimp simp add:
          Cons_eq_upt_conv append_eq_Cons_conv map_eq_append_conv
          split: list.splits) auto
      then have "sp. s_at sp = i  s_check v (φ S I ψ) sp"
        by blast
    }
    ultimately show "sp. s_at sp = i  s_check v (φ S I ψ) sp"
      using not_less by blast
  qed
next
  case (VSinceOut i I v φ ψ)
  then show ?case
    by (auto intro!: exI[of _ "VSinceOut i"])
next
  case (VSince I i j v φ ψ)
  show ?case
  proof
    assume fb_since: "future_bounded (φ S I ψ)"
    then have fb: "future_bounded φ" "future_bounded ψ"
      by simp_all
    obtain vp1 where vp1_def: "v_at vp1 = j  v_check v φ vp1"
      using fb_since VSince by auto
    obtain mypick where mypick_def: "k  {j .. LTP_p σ i I}. v_at (mypick k) = k  v_check v ψ (mypick k)"
      using VSince fb_since by atomize_elim (rule bchoice, simp)
    then obtain vp2s where vp2s_def: "map (v_at) vp2s = [j ..< Suc (LTP_p σ i I)]  (vp  set vp2s. v_check v ψ vp)"
      by atomize_elim (auto intro!: trans[OF list.map_cong list.map_id] exI[of _ "map mypick ([j ..< Suc (LTP_p σ i I)])"])
    then have "v_at (VSince i vp1 vp2s) = i  v_check v (φ S I ψ) (VSince i vp1 vp2s)"
      using vp1_def VSince by auto
    then show "vp. v_at vp = i  v_check v (φ S I ψ) vp"
      by blast
  qed
next
  case (VSinceInf j I i v ψ φ)
  show ?case
  proof
    assume fb_since: "future_bounded (φ S I ψ)"
    then have fb: "future_bounded φ" "future_bounded ψ"
      by simp_all
    obtain mypick where mypick_def: "k  {j .. LTP_p σ i I}. v_at (mypick k) = k  v_check v ψ (mypick k)"
      using VSinceInf fb_since by atomize_elim (rule bchoice, simp)
    then obtain vp2s where vp2s_def: "map (v_at) vp2s = [j ..< Suc (LTP_p σ i I)]  (vp  set vp2s. v_check v ψ vp)"
      by atomize_elim (auto intro!: trans[OF list.map_cong list.map_id] exI[of _ "map mypick ([j ..< Suc (LTP_p σ i I)])"])
    then have "v_at (VSinceInf i j vp2s) = i  v_check v (φ S I ψ) (VSinceInf i j vp2s)"
      using VSinceInf by auto
    then show "vp. v_at vp = i  v_check v (φ S I ψ) vp"
      by blast
  qed
next
  case (SUntil j i I v ψ φ)
  show ?case
  proof
    assume fb_until: "future_bounded (φ U I ψ)"
    then have fb: "future_bounded φ" "future_bounded ψ"
      by simp_all
    obtain sp2 where sp2_def: "s_at sp2 = j  s_check v ψ sp2"
      using fb SUntil by blast
    {
      assume "i  j"
      then have "s_at (SUntil [] sp2) = i  s_check v (φ U I ψ) (SUntil [] sp2)"
        using sp2_def SUntil by auto
      then have "sp. s_at sp = i  s_check v (φ U I ψ) sp"
        by blast
    }
    moreover
    {
      assume i_l_j: "i < j"
      obtain mypick where mypick_def: "k  {i ..< j}. s_at (mypick k) = k  s_check v φ (mypick k)"
        using SUntil fb_until by atomize_elim (rule bchoice, simp)
      then obtain sp1s where sp1s_def: "map (s_at) sp1s = [i ..< j]  (sp  set sp1s. s_check v φ sp)"
        by atomize_elim (auto intro!: trans[OF list.map_cong list.map_id] exI[of _ "map mypick ([i ..< j])"])
      then have "s_at (SUntil sp1s sp2) = i  s_check v (φ U I ψ) (SUntil sp1s sp2)"
        using SUntil fb_until sp2_def sp1s_def i_l_j
        by (clarsimp simp add: append_eq_Cons_conv map_eq_append_conv split: list.splits)
          (auto simp: Cons_eq_upt_conv dest!: upt_eq_Nil_conv[THEN iffD1, OF sym])
      then have "sp. s_at sp = i  s_check v (φ U I ψ) sp"
        by blast
    }
    ultimately show "sp. s_at sp = i  s_check v (φ U I ψ) sp"
      using not_less by blast
  qed
next
  case (VUntil I j i v φ ψ)
  show ?case
  proof
    assume fb_until: "future_bounded (φ U I ψ)"
    then have fb: "future_bounded φ" "future_bounded ψ"
      by simp_all
    obtain vp1 where vp1_def: "v_at vp1 = j  v_check v φ vp1"
      using VUntil fb_until by auto
    obtain mypick where mypick_def: "k  {ETP_f σ i I .. j}. v_at (mypick k) = k  v_check v ψ (mypick k)"
      using VUntil fb_until by atomize_elim (rule bchoice, simp)
    then obtain vp2s where vp2s_def: "map (v_at) vp2s = [ETP_f σ i I ..< Suc j]  (vp  set vp2s. v_check v ψ vp)"
      by atomize_elim (auto intro!: trans[OF list.map_cong list.map_id] exI[of _ "map mypick ([ETP_f σ i I ..< Suc j])"])
    then have "v_at (VUntil i vp2s vp1) = i  v_check v (φ U I ψ) (VUntil i vp2s vp1)"
      using VUntil fb_until vp1_def by simp
    then show "vp. v_at vp = i  v_check v (φ U I ψ) vp"
      by blast
  qed
next
  case (VUntilInf I i v ψ φ)
  show ?case
  proof
    assume fb_until: "future_bounded (φ U I ψ)"
    then have fb: "future_bounded φ" "future_bounded ψ"
      by simp_all
    obtain b where b_def: "right I = enat b"
      using fb_until by (atomize_elim, cases "right I") auto
    define j where j_def: "j = LTP σ (τ σ i + b)"
    obtain mypick where mypick_def: "k  {ETP_f σ i I .. j}. v_at (mypick k) = k  v_check v ψ (mypick k)"
      using VUntilInf fb_until unfolding b_def j_def by atomize_elim (rule bchoice, simp)
    then obtain vp2s where vp2s_def: "map (v_at) vp2s = [ETP_f σ i I ..< Suc j]  (vp  set vp2s. v_check v ψ vp)"
      by atomize_elim (auto intro!: trans[OF list.map_cong list.map_id] exI[of _ "map mypick ([ETP_f σ i I ..< Suc j])"])
    then have "v_at (VUntilInf i j vp2s) = i  v_check v (φ U I ψ) (VUntilInf i j vp2s)"
      using VUntilInf b_def j_def by simp
    then show "vp. v_at vp = i  v_check v (φ U I ψ) vp"
      by blast
  qed
qed

lemmas check_completeness =
  conjunct1[OF check_completeness_aux, rule_format]
  conjunct2[OF check_completeness_aux, rule_format]

definition "p_check v φ p = (case p of Inl sp  s_check v φ sp | Inr vp  v_check v φ vp)"
definition "p_check_exec vs φ p = (case p of Inl sp  s_check_exec vs φ sp | Inr vp  v_check_exec vs φ vp)"

definition valid :: "('n, 'd) envset  nat  ('n, 'd) formula  ('n, 'd) proof  bool" where
  "valid vs i φ p =
    (case p of
      Inl p  s_check_exec vs φ p  s_at p = i
    | Inr p  v_check_exec vs φ p  v_at p = i)"

end

subsection ‹Lifting the Checker to PDTs›

fun check_one where
  "check_one σ v φ (Leaf p) = p_check σ v φ p"
| "check_one σ v φ (Node x part) = check_one σ v φ (lookup_part part (v x))"

fun check_all_aux where
  "check_all_aux σ vs φ (Leaf p) = p_check_exec σ vs φ p"
| "check_all_aux σ vs φ (Node x part) = ((D, e)  set (subsvals part). check_all_aux σ (vs(x := D)) φ e)"

fun collect_paths_aux where
  "collect_paths_aux DS σ vs φ (Leaf p) = (if p_check_exec σ vs φ p then {} else rev ` DS)"
| "collect_paths_aux DS σ vs φ (Node x part) = ((D, e)  set (subsvals part). collect_paths_aux (Cons D ` DS) σ (vs(x := D)) φ e)"

lemma check_one_cong: "xfv φ  vars e. v x = v' x  check_one σ v φ e = check_one σ v' φ e"
proof (induct e arbitrary: v v')
  case (Leaf x)
  then show ?case
    by (auto simp: p_check_def check_fv_cong split: sum.splits)
next
  case (Node x part)
  from Node(2) have *: "v x = v' x"
    by simp
  from Node(2) show ?case
    unfolding check_one.simps *
    by (intro Node(1)) auto
qed

lemma check_all_aux_check_one: "x. vs x  {}  distinct_paths e  (x  vars e. vs x = UNIV) 
  check_all_aux σ vs φ e  (v  compatible_vals (fv φ) vs. check_one σ v φ e)"
proof (induct e arbitrary: vs)
  case (Node x part)
  show ?case
    unfolding check_all_aux.simps check_one.simps split_beta
  proof (safe, unfold fst_conv snd_conv, goal_cases LR RL)
    case (LR v)
    from Node(2-) fst_lookup[of "v x" part] LR(1)[rule_format, OF lookup_subsvals[of _ "v x"]] LR(2) show ?case
      by (subst (asm) Node(1))
         (auto 0 3 simp: compatible_vals_fun_upd dest!: bspec[of _ _ v]
            elim!: compatible_vals_antimono[THEN set_mp, rotated])
  next
    case (RL D e)
    from RL(2) obtain d where "d  D"
      by transfer (force simp: partition_on_def image_iff)
    with RL show ?case
      using Node(2-) lookup_subsvals[of part d] lookup_part_Vals[of part d]
        lookup_part_from_subvals[of D e part d]
    proof (intro Node(1)[THEN iffD2, OF _ _ _ _ ballI], goal_cases _ _ _ _ compatible)
      case (compatible v)
      from compatible(2-) compatible(1)[THEN bspec, of "v(x := d)"] compatible(1)[THEN bspec, of v]
      show ?case
        using lookup_part_from_subvals[of D e part "v x"]
          fun_upd_in_compatible_vals_in[of v "fv φ" x vs "v x"]
          check_one_cong[THEN iffD1, rotated -1, of σ "v(x := d)" φ e v, simplified]
        by (auto simp: compatible_vals_fun_upd fun_upd_apply[of _ _ _ x]
          fun_upd_in_compatible_vals_notin split: if_splits
          simp del: fun_upd_apply)
    qed auto
  qed
qed (auto simp: p_check_exec_def p_check_def check_exec_check split: sum.splits)

definition check_all :: "('n, 'd :: {default, linorder}) trace  ('n, 'd) formula  ('n, 'd) expl  bool" where
  "check_all σ φ e = (distinct_paths e  check_all_aux σ (λ_. UNIV) φ e)"

lemma check_one_alt: "check_one σ v φ e = p_check σ v φ (eval_pdt v e)"
  by (induct e) auto

lemma check_all_alt: "check_all σ φ e = (distinct_paths e  (v. p_check σ v φ (eval_pdt v e)))"
  unfolding check_all_def
  by (rule conj_cong[OF refl], subst check_all_aux_check_one)
    (auto simp: compatible_vals_def check_one_alt)

fun pdt_at where
  "pdt_at i (Leaf l) = (p_at l = i)"
| "pdt_at i (Node x part) = (pdt  Vals part. pdt_at i pdt)"

lemma pdt_at_p_at_eval_pdt: "pdt_at i e  p_at (eval_pdt v e) = i"
  by (induct e) auto

lemma check_all_completeness_aux:
  fixes φ :: "('n, 'd :: {default, linorder}) formula"
  shows "set vs  fv φ  future_bounded φ  distinct vs 
  e. pdt_at i e  vars_order vs e  (v. (x. x  set vs  v x = w x)  p_check σ v φ (eval_pdt v e))"
proof (induct vs arbitrary: w)
  case Nil
  then show ?case
  proof (cases "sat σ w i φ")
    case True
    then have "SAT σ w i φ" by (rule completeness)
    with Nil obtain sp where "s_at sp = i" "s_check σ w φ sp" by (blast dest: check_completeness)
    then show ?thesis
      by (intro exI[of _ "Leaf (Inl sp)"]) (auto simp: vars_order.intros p_check_def p_at_def)
  next
    case False
    then have "VIO σ w i φ" by (rule completeness)
    with Nil obtain vp where "v_at vp = i" "v_check σ w φ vp" by (blast dest: check_completeness)
    then show ?thesis
      by (intro exI[of _ "Leaf (Inr vp)"]) (auto simp: vars_order.intros p_check_def p_at_def)
  qed
next
  case (Cons x vs)
  define eq :: "('n  'd)  ('n  'd)  bool" where "eq = rel_fun (eq_onp (λx. x  set vs)) (=)"
  from Cons have "w. e. pdt_at i e  vars_order vs e 
    (v. (x. x  set vs  v x = w x)  p_check σ v φ (eval_pdt v e))" by simp
  then obtain pick :: "'d  ('n, 'd) expl" where pick: "pdt_at i (pick a)" "vars_order vs (pick a)" and
    eq_pick: "v. eq v (w(x := a))  p_check σ v φ (eval_pdt v (pick a))" for a
    unfolding eq_def rel_fun_def eq_onp_def choice_iff
  proof (atomize_elim, elim exE, goal_cases pick_val)
    case (pick_val f)
    then show ?case
      by (auto intro!: exI[of _ "λa. f (w(x := a))"])
  qed
  let ?a = "SOME z. z  AD σ φ i"
  let ?AD = "sorted_list_of_set (AD σ φ i)"
  show ?case
  proof (intro exI[of _ "Node x (tabulate ?AD pick (pick ?a))"] conjI allI impI,
    goal_cases pdt_at vars_order p_check)
    case (p_check w')
    have "w' x  AD σ φ i  ?a  AD σ φ i"
      by (metis some_eq_imp)
    moreover have "eq (w'(x := ?a)) (w(x := ?a))"
      using p_check by (auto simp: eq_def rel_fun_def eq_onp_def)
    moreover have "eq w' (w(x := w' x))"
      using p_check by (auto simp: eq_def rel_fun_def eq_onp_def)
    ultimately show ?case
      using pick Cons(2-) eq_pick[of w' "w' x"] eq_pick[of "w'(x := ?a)" ?a]
        pdt_at_p_at_eval_pdt[of "i" "pick ?a" w'] eval_pdt_fun_upd[of vs "pick ?a" x w' ?a]
      by (auto simp: p_check_def p_at_def
        elim!: check_AD_cong[THEN iffD1, rotated -1, of _ _ _ _ _ i]
        split: if_splits sum.splits sum.splits)
  qed (use Cons(2-) pick in simp_all add: vars_order.intros)
qed

lemma check_all_completeness:
  fixes φ :: "('n, 'd :: {default, linorder}) formula"
  assumes "future_bounded φ"
  shows "e. pdt_at i e  check_all σ φ e"
proof -
  obtain vs where vs[simp]: "distinct vs" "set vs = fv φ"
    by (meson finite_distinct_list finite_fv)
  have s: "s_check σ v φ sp"
    if "vars_order vs e"
    and "v. (sp. eval_pdt v e = Inl sp  (x. x  fv φ  v x  undefined)  s_check σ v φ sp) 
             (vp. eval_pdt v e = Inr vp  (x. x  fv φ  v x  undefined)  v_check σ v φ vp)"
    and "eval_pdt v e = Inl sp" for e v sp
    using that eval_pdt_cong[of e v "λx. if x  fv φ then v x else undefined"]
      check_fv_cong[of φ v "λx. if x  fv φ then v x else undefined"]
    by (auto dest!: spec[of _ sp] vars_order_vars simp: subset_eq)
  have v: "v_check σ v φ vp"
    if "vars_order vs e"
    and "v. (sp. eval_pdt v e = Inl sp  (x. x  fv φ  v x  undefined)  s_check σ v φ sp) 
             (vp. eval_pdt v e = Inr vp  (x. x  fv φ  v x  undefined)  v_check σ v φ vp)"
    and "eval_pdt v e = Inr vp" for e v vp
    using that eval_pdt_cong[of e v "λx. if x  fv φ then v x else undefined"]
      check_fv_cong[of φ v "λx. if x  fv φ then v x else undefined"]
    by (auto dest!: spec[of _ vp] vars_order_vars simp: subset_eq)
  show ?thesis
    using check_all_completeness_aux[of vs φ i "λ_. undefined" σ] assms
    unfolding check_all_alt p_check_def
    by (auto elim!: exI [where P = "λx. _ x  _ x" , OF conjI] simp: vars_order_distinct_paths split: sum.splits intro: s v)
qed

lemma check_all_soundness_aux: "check_all σ φ e  p = eval_pdt v e  isl p  sat σ v (p_at p) φ"
  unfolding check_all_alt
  by (auto simp: isl_def p_check_def p_at_def dest!: spec[of _ v]
    dest: check_soundness soundness split: sum.splits)

lemma check_all_soundness: "check_all σ φ e  pdt_at i e  isl (eval_pdt v e)  sat σ v i φ"
  by (drule check_all_soundness_aux[OF _ refl, of _ _ _ v]) (auto simp: pdt_at_p_at_eval_pdt)

unbundle no MFOTL_syntax

(*<*)
end
(*>*)