Impressum Checker.thy

(*<*)
theory Checker
  imports Proof_System Proof_Object Regex_Checker "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
    (\<top>, STT i) ==> True
  | (r † ts, SPred i s ts') ==>
    (r = s ∧ ts = ts' ∧ (r, v\<lbrakk>ts\<rbrakk>) ∈ Γ σ i)
  | (x \<approx> 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))
  | (\<triangleleft> I r, SMatchP rsp) ==>
    (let (j, i) = rs_at s_at rsp in j ≤ i ∧ mem (τ σ i - τ σ j) I ∧ rs_check (s_check v) s_at r rsp)
  | (\<triangleright> I r, SMatchF rsp) ==>
    (let (i, j) = rs_at s_at rsp in i ≤ j ∧ mem (τ σ j - τ σ i) I ∧ rs_check (s_check v) s_at r rsp)
  | ( _ , _) ==> False)"
| "v_check v f p = (case (f, p) of
    (\<bottom>, VFF i) ==> True
  | (r † ts, VPred i pred ts') ==>
    (r = pred ∧ ts = ts' ∧ (r, v\<lbrakk>ts\<rbrakk>) ∉ Γ σ i)
  | (x \<approx> 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))
  | (\<triangleleft> I r, VMatchPOut i) ==> τ σ i < τ σ 0 + left I
  | (\<triangleleft> I r, VMatchP i rvps) ==>
    (let j = ETP σ (case right I of ∞ ==> 0 | enat n ==> τ σ i - n)
    in τ σ i ≥ τ σ 0 + left I ∧ map (fst ∘ rv_at v_at) rvps = [j ..< Suc (LTP_p σ i I)] ∧
    (∀rvp ∈ set rvps. rv_check (v_check v) v_at r rvp ∧ snd (rv_at v_at rvp) = i))
  | (\<triangleright> I r, VMatchF i rvps) ==>
    (let j = LTP σ (case right I of ∞ ==> 0 | enat n ==> τ σ i + n)
    in map (snd ∘ rv_at v_at) rvps = [ETP_f σ i I ..< Suc j] ∧ right I ≠ ∞ ∧
    (∀rvp ∈ set rvps. rv_check (v_check v) v_at r rvp ∧ fst (rv_at v_at rvp) = i))
  | ( _ , _) ==> 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 (SMatchP rsp)
  then show ?case
    by (cases φ) (auto intro: SAT_VIO.SMatchP dest!: rs_check_sound[rotated, where sat="SAT σ v"])
next
  case (SMatchF rsp)
  then show ?case
    by (cases φ) (auto intro: SAT_VIO.SMatchF dest!: rs_check_sound[rotated, where sat="SAT σ v"])
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)
next
  case (VMatchPOut i rvps)
  then show ?case by (cases φ) (auto intro: SAT_VIO.VMatchPOut)
next
  case (VMatchP i rvps)
  then show ?case
  proof (cases φ)
    case (MatchP I r)
    then have vio: "∧rvp. rvp ∈ set rvps ==> Regex_Proof_System.VIO (VIO σ v) (fst (rv_at v_at rvp)) (snd (rv_at v_at rvp)) r"
      using rv_check_sound[of r _ "v_check v" "VIO σ v" v_at] VMatchP MatchP
      by (auto simp: Let_def)
    { fix k
      define j where j_def: "j ≡ ETP σ (case right I of ∞ ==> 0 | enat n ==> τ σ i - n)"
      assume k_def: "k ≥ j ∧ k ≤ i ∧ k ≤ LTP σ (τ σ i - left I)"
      from VMatchP MatchP j_def have map: "set (map (fst ∘ rv_at v_at) rvps) = set [j ..< Suc (LTP_p σ i I)]"
        by (auto simp: Let_def)
      then have kset: "k ∈ set ([j ..< Suc (LTP_p σ i I)])" using k_def j_def by auto
      then obtain rvp where rvp: "rvp ∈ set rvps" "fst (rv_at v_at rvp) = k"
        using k_def kset map
        by (auto simp: i_LTP_tau set_eq_iff image_iff dest: spec[of _ k] simp del: upt.simps)
      then have "Regex_Proof_System.VIO (VIO σ v) k i r" using VMatchP MatchP vio[of rvp]
        by (auto simp: Let_def)
      } note * = this
    then show ?thesis using VMatchP MatchP
      by (auto simp: i_ETP_tau intro!: SAT_VIO.VMatchP split: enat.splits)
  qed(auto intro: SAT_VIO.intros)
next
  case (VMatchF i rvps)  then show ?case
  proof (cases φ)
    case (MatchF I r)
    then have vio: "∧rvp. rvp ∈ set rvps ==> Regex_Proof_System.VIO (VIO σ v) (fst (rv_at v_at rvp)) (snd (rv_at v_at rvp)) r"
      using rv_check_sound[of r _ "v_check v" "VIO σ v" v_at] VMatchF MatchF
      by (auto simp: Let_def)
    { fix k
      define j where j_def: "j ≡ LTP σ (case right I of ∞ ==> 0 | enat n ==> τ σ i + n)"
      assume k_def: "k ≤ j ∧ k ≥ i ∧ k ≥ ETP σ (τ σ i + left I)"
      from VMatchF MatchF j_def have map: "set (map (snd ∘ rv_at v_at) rvps) = set [ETP_f σ i I ..< Suc j]"
        by (auto simp: Let_def)
      then have kset: "k ∈ set ([ETP_f σ i I ..< Suc j])" using k_def j_def by auto
      then obtain rvp where rvp: "rvp ∈ set rvps" "snd (rv_at v_at rvp) = k"
        using k_def kset map
        by (auto simp: i_LTP_tau set_eq_iff image_iff dest: spec[of _ k] simp del: upt.simps)
      then have "Regex_Proof_System.VIO (VIO σ v) i k r" using VMatchF MatchF vio[of rvp]
        by (auto simp: Let_def)
      } note * = this
    then show ?thesis using VMatchF MatchF
      by (auto simp: Let_def intro!: SAT_VIO.VMatchF)
  qed(auto intro: SAT_VIO.intros)
qed

definition "compatible X vs v ⟷ (∀x∈X. 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_vals_Union_eq:
  "compatible_vals (∪x∈X. Y x) vs = (∩x ∈ X. compatible_vals (Y x) 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' ∧ (∀x∈X. 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 "∀tX∈set 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: "∀tX∈set 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: "∀tX∈set 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 "∀tX∈set 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 ‹∀tX∈set 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 "∀tX∈set 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 ‹∀tX∈set 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 (vs\<lbrace>ts\<rbrace>) ==>
  ∃v∈compatible_vals (fv (r † ts)) vs. cs = v\<lbrakk>ts\<rbrakk>"
proof (induct ts arbitrary: cs vs)
  case (Cons t ts)
  show ?case
  proof(cases t)
    case (Var x)
    let ?Ts = "vs\<lbrace>ts\<rbrace>"
    have "vs\<lbrace>(t # ts)\<rbrace> = (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 = v\<lbrakk>ts\<rbrakk>"
        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 = v\<lbrakk>ts\<rbrakk>"
          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 (vs{t}) = t"
  by (cases t; clarsimp)

lemma mk_values_complete: "cs = v\<lbrakk>ts\<rbrakk> ==>
  v ∈ compatible_vals (fv (r † ts)) vs ==>
  cs ∈ mk_values (vs\<lbrace>ts\<rbrace>)"
proof (induct ts arbitrary: v cs vs)
  case (Cons t ts)
  then obtain a as
    where a_def: "a = v[t]"
      and as_def: "as = v\<lbrakk>ts\<rbrakk>"
      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 (vs\<lbrace>ts\<rbrace>)"
    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 (vs\<lbrace>ts\<rbrace>)) (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 (vs\<lbrace>ts\<rbrace>))"
        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 (vs\<lbrace>ts\<rbrace>) ⊆ - Γ σ 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 (vs\<lbrace>ts\<rbrace>) =
   {cs. ∃v∈compatible_vals (∪(fv_trm ` set ts)) vs. cs = v\<lbrakk>ts\<rbrakk>}"
  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)\<lbrakk>ts\<rbrakk>) (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)\<lbrakk>ts\<rbrakk>)
        (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:
  "∀v∈compatible_vals (∪ (fv_trm ` set ts) - dom f) vs. us ≠ (λx. case f x of None ==> v x | Some y ==> y)\<lbrakk>ts\<rbrakk> ==>
  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
    (\<top>, STT i) ==> True
  | (r † ts, SPred i s ts') ==>
    (r = s ∧ ts = ts' ∧ mk_values_subset r (vs\<lbrace>ts\<rbrace>) (Γ σ i))
  | (x \<approx> 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))
  | (\<triangleleft> I r, SMatchP rsp) ==>
    (let (j, i) = rs_at s_at rsp in j ≤ i ∧ mem (τ σ i - τ σ j) I ∧ rs_check (s_check_exec vs) s_at r rsp)
  | (\<triangleright> I r, SMatchF rsp) ==>
    (let (i, j) = rs_at s_at rsp in i ≤ j ∧ mem (τ σ j - τ σ i) I ∧ rs_check (s_check_exec vs) s_at r rsp)
  | ( _ , _) ==> False)"
| "v_check_exec vs f p = (case (f, p) of
    (\<bottom>, VFF i) ==> True
  | (r † ts, VPred i pred ts') ==>
    (r = pred ∧ ts = ts' ∧ mk_values_subset_Compl r vs ts i)
  | (x \<approx> 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))
  | (\<triangleleft> I r, VMatchPOut i) ==> τ σ i < τ σ 0 + left I
  | (\<triangleleft> I r, VMatchP i rvps) ==>
    (let j = ETP σ (case right I of ∞ ==> 0 | enat n ==> τ σ i - n)
    in τ σ i ≥ τ σ 0 + left I ∧ map (fst ∘ rv_at v_at) rvps = [j ..< Suc (LTP_p σ i I)] ∧
    (∀rvp ∈ set rvps. rv_check (v_check_exec vs) v_at r rvp ∧ snd (rv_at v_at rvp) = i))
  | (\<triangleright> I r, VMatchF i rvps) ==>
    (let j = LTP σ (case right I of ∞ ==> 0 | enat n ==> τ σ i + n)
    in map (snd ∘ rv_at v_at) rvps = [ETP_f σ i I ..< Suc j] ∧ right I ≠ ∞ ∧
    (∀rvp ∈ set rvps. rv_check (v_check_exec vs) v_at r rvp ∧ fst (rv_at v_at rvp) = i))
  | ( _ , _) ==> False)"

declare s_check_exec.simps[simp del] v_check_exec.simps[simp del]
simps_of_case s_check_exec_simps[simp]: s_check_exec.simps[unfolded prod.case] (splits: formula.split sproof.split)
simps_of_case v_check_exec_simps[simp]: 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
  }
next
  case (MatchP I r)
  {
    case 1
    with MatchP[of _ v v'] show ?case
      by (cases sp) (auto simp: collect_alt elim!: rs_check_cong[THEN iffD1, rotated -1])
  next
    case 2
    with MatchP[of _ v v'] show ?case
      by (cases vp) (auto simp: collect_alt Let_def elim!: rv_check_cong[THEN iffD1, rotated -1])
  }
next
  case (MatchF I r)
  {
    case 1
    with MatchF[of _ v v'] show ?case
      by (cases sp) (auto simp: collect_alt elim!: rs_check_cong[THEN iffD1, rotated -1])
  next
    case 2
    with MatchF[of _ v v'] show ?case
      by (cases vp) (auto simp: collect_alt Let_def elim!: rv_check_cong[THEN iffD1, rotated -1])
  }
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: "∀tX∈set (vs\<lbrace>ts\<rbrace>). 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 = (∀v∈compatible_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 = (∀v∈compatible_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 = (∀v∈compatible_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 = (∀v∈compatible_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)
  }
next
  case (MatchP I r)
  {
    case 1
    with compatible_vals_nonemptyI[OF 1, of "Regex.collect fv r"] show ?case
    proof (cases sp)
      case (SMatchP rsp)
      show ?thesis
        unfolding SMatchP s_check_exec_simps s_check_simps fv.simps Let_def split_beta ball_conj_distrib
          ball_triv_nonempty[OF compatible_vals_nonemptyI[OF 1, of "Regex.collect fv r"]]
        unfolding collect_alt compatible_vals_Union_eq
        by (intro conj_cong refl
          rs_check_exec_rs_check compatible_vals_nonemptyI 1
          compatible_vals_union_eq compatible_vals_Union_eq
          compatible_vals_extensible check_fv_cong(1) MatchP(1)[OF _ 1])
    qed auto
  next
    case 2
    with compatible_vals_nonemptyI[OF 2, of "Regex.collect fv r"] show ?case
    proof (cases vp)
      case (VMatchP i rvps)
      show ?thesis
        unfolding VMatchP v_check_exec_simps v_check_simps fv.simps Let_def split_beta ball_conj_distrib
          ball_triv_nonempty[OF compatible_vals_nonemptyI[OF 2, of "Regex.collect fv r"]]
        unfolding collect_alt compatible_vals_Union_eq ball_swap[of _ "set rvps"]
        by (intro conj_cong refl ball_cong
          rv_check_exec_rv_check compatible_vals_nonemptyI 2
          compatible_vals_union_eq compatible_vals_Union_eq
          compatible_vals_extensible check_fv_cong(2) MatchP(2)[OF _ 2])
    qed auto
  }
next
  case (MatchF I r)
  {
    case 1
    with compatible_vals_nonemptyI[OF 1, of "Regex.collect fv r"] show ?case
    proof (cases sp)
      case (SMatchF rsp)
      show ?thesis
        unfolding SMatchF s_check_exec_simps s_check_simps fv.simps Let_def split_beta ball_conj_distrib
          ball_triv_nonempty[OF compatible_vals_nonemptyI[OF 1, of "Regex.collect fv r"]]
        unfolding collect_alt compatible_vals_Union_eq
        by (intro arg_cong2[of _ _ _ _ "(∧)"] refl
          rs_check_exec_rs_check compatible_vals_nonemptyI 1
          compatible_vals_union_eq compatible_vals_Union_eq
          compatible_vals_extensible check_fv_cong(1) MatchF(1)[OF _ 1])
    qed auto
  next
    case 2
    with compatible_vals_nonemptyI[OF 2, of "Regex.collect fv r"] show ?case
    proof (cases vp)
      case (VMatchF i rvps)
      show ?thesis
        unfolding VMatchF v_check_exec_simps v_check_simps fv.simps Let_def split_beta ball_conj_distrib
          ball_triv_nonempty[OF compatible_vals_nonemptyI[OF 2, of "Regex.collect fv r"]]
        unfolding collect_alt compatible_vals_Union_eq ball_swap[of _ "set rvps"]
        by (intro conj_cong refl ball_cong
          rv_check_exec_rv_check compatible_vals_nonemptyI 2
          compatible_vals_union_eq compatible_vals_Union_eq
          compatible_vals_extensible check_fv_cong(2) MatchF(2)[OF _ 2])
    qed auto
  }
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 rLRTP :: "('a ==> nat ==> nat option) ==> 'a Regex.regex ==> nat ==> nat option" where
  "rLRTP LRTP (Regex.Skip n) i = Some i"
| "rLRTP LRTP (Regex.Test x) i = LRTP x i"
| "rLRTP LRTP (Regex.Plus r s) i = max_opt (rLRTP LRTP r i) (rLRTP LRTP s i)"
| "rLRTP LRTP (Regex.Times r s) i = max_opt (rLRTP LRTP r i) (rLRTP LRTP s i)"
| "rLRTP LRTP (Regex.Star r) i = rLRTP LRTP r i"

lemma rLRTP_cong[fundef_cong]: 
  "(∧x. x ∈ regex.atms r ==> LRTP x i = LRTP' x i) ==> rLRTP LRTP r i = rLRTP LRTP' r i"
  by (induct r) auto

lemma fb_rLRTP: 
  assumes "∀φ ∈ regex.atms r. future_bounded φ ∧ ¬ Option.is_none (LRTP φ i)"
  shows "¬ Option.is_none (rLRTP LRTP r i)"
  using assms by (induct r) (auto simp: max_opt_def Option.is_none_def)

fun LRTP :: "('n, 'd) formula ==> nat ==> nat option" where
  "LRTP \<top> i = Some i"
| "LRTP \<bottom> i = Some i"
| "LRTP (_ † _) i = Some i"
| "LRTP (_ \<approx> _) 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)))"
| "LRTP (\<triangleleft> I r) i =
    (let X = (λφ. LRTP φ i) ` regex.atms r in
    if X = {} then Some i else if None ∈ X then None else Some (Max (the ` X)))"
| "LRTP (\<triangleright> I r) i = (case right I of ∞ ==> None | enat b ==>
    let X = (λφ. LRTP φ (LTP_f σ i b)) ` regex.atms r in
    if X = {} then Some (LTP_f σ i b) else if None ∈ X then None else Some (Max (the ` X)))"

lemma fb_LRTP: 
  assumes "future_bounded φ"
  shows "¬ Option.is_none (LRTP φ i)"
  using assms
proof (induction φ i rule: LRTP.induct)
  case (20 I r i)
  from 20(2) show ?case
    by (auto 0 4 simp add: max_opt_def Option.is_none_def Let_def regex.pred_set dest: 20(1)[rotated])
next
  case (21 I r i)
  from 21(2) show ?case
    by (auto 0 4 simp add: max_opt_def Option.is_none_def Let_def regex.pred_set dest: 21(1)[rotated])
qed (auto simp: 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, v\<lbrakk>ts\<rbrakk>) ∈ Γ σ 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 _ "v\<lbrakk>ts\<rbrakk>"] 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, v\<lbrakk>ts\<rbrakk>) ∉ Γ σ 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 AD_simps_regex[simp]:
  "future_bounded (\<triangleleft> I r) ==> regex.atms r ≠ {} ==> AD (\<triangleleft> I r) i = (∪φ ∈ regex.atms r. AD φ i)"
  "future_bounded (\<triangleright> I r) ==> regex.atms r ≠ {} ==> AD (\<triangleright> I r) i = (∪φ ∈ regex.atms r. AD φ (LTP_f σ i (the_enat (right I))))"
  unfolding AD_def
  by (auto 0 6 simp: Let_def collect_alt regex.pred_set image_image Ball_def not_none_fb_LRTP
    dest!: Max_ge_iff[THEN iffD1, rotated -1] sym[of None]
    dest: spec[where P = "λx. x ≤ Max _ ⟶ _ x", THEN mp, OF _ Max_ge_iff[THEN iffD2]] split: if_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_τ_mono:
  assumes "τ σ i ≤ u"
  shows"LTP σ (τ σ i) ≤ LTP σ u"
  using assms unfolding LTP_def
proof (intro Max_mono)
  show "finite {i. τ σ i ≤ u}"
    unfolding finite_nat_set_iff_bounded_le Ball_def mem_Collect_eq
    by (meson τ_mono ex_le_τ nle_le order_trans)
qed auto

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)
next
  case (MatchP I r)
  { assume ne: "regex.atms r ≠ {}" and fb: "∧φ. φ∈regex.atms r ==> future_bounded φ"
    then obtain φ where φ: "φ ∈ regex.atms r" "the (LRTP φ j) = (MAX φ ∈ regex.atms r. the (LRTP φ j))"
      using obtains_MAX[of "regex.atms r" "λφ. the (LRTP φ j)" thesis] by auto
    assume "∀x∈regex.atms r. ∃a∈regex.atms r. ¬ the (LRTP a i) ≤ the (LRTP x j)"
    with φ(1) obtain ψ where ψ: "ψ ∈ regex.atms r" "¬ the (LRTP ψ i) ≤ the (LRTP φ j)"
      by blast
    moreover have "the (LRTP ψ i) ≤ the (LRTP ψ j)"
      using MatchP(1)[OF ψ(1) fb[OF ψ(1)] MatchP(3)] .
    moreover have "the (LRTP ψ j) ≤ the (LRTP φ j)"
      unfolding φ(2) by (subst Max_ge_iff) (auto simp: ne ψ(1))
    ultimately have "False" by auto
  }
  with MatchP(2-) show ?case
    by (force simp: Let_def regex.pred_set not_none_fb_LRTP Max_ge_iff dest!: sym[of None])
next
  case (MatchF I r)
  let ?j = "LTP_f σ j (the_enat (right I))"
  let ?i = "LTP_f σ i (the_enat (right I))"
  { assume ne: "regex.atms r ≠ {}" and fb: "∧φ. φ∈regex.atms r ==> future_bounded φ"
    then obtain φ where φ: "φ ∈ regex.atms r" "the (LRTP φ ?j) = (MAX φ ∈ regex.atms r. the (LRTP φ ?j))"
      using obtains_MAX[of "regex.atms r" "λφ. the (LRTP φ ?j)" thesis] by auto
    assume "∀x∈regex.atms r. ∃a∈regex.atms r. ¬ the (LRTP a ?i) ≤ the (LRTP x ?j)"
    with φ(1) obtain ψ where ψ: "ψ ∈ regex.atms r" "¬ the (LRTP ψ ?i) ≤ the (LRTP φ ?j)"
      by blast
    moreover have "the (LRTP ψ ?i) ≤ the (LRTP ψ ?j)"
      using MatchF(1)[OF ψ(1) fb[OF ψ(1)] LTP_f_mono[OF MatchF(3)]] .
    moreover have "the (LRTP ψ ?j) ≤ the (LRTP φ ?j)"
      unfolding φ(2) by (subst Max_ge_iff) (auto simp: ne ψ(1))
    ultimately have "False" by auto
  }
  with MatchF(2-) show ?case
    by (auto simp: Let_def regex.pred_set not_none_fb_LRTP Max_ge_iff LTP_f_mono dest!: sym[of None] elim!: meta_mp)
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-25)[OF refl] and hyps = 1(26-28)
  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 "∀x∈fv φ. 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 "∀x∈fv φ. 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 "∀x∈fv φ. 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 "∀x∈fv φ. 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 "∀x∈fv φ. 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 "∀x∈fv ψ. 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 "∀x∈fv φ. 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 "∀x∈fv ψ. 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
  next
    case (SMatchP rsp)
    then show ?thesis
    proof (cases "∀sp' ∈ spatms rsp. s_at sp' ≤ s_at sp")
      case True
      with SMatchP show ?thesis
      proof (cases f)
        case (MatchP I r)
        show ?thesis unfolding SMatchP MatchP s_check_simps Let_def split_beta
        proof ((rule conj_cong refl rs_check_cong IH(24) prod.collapse refl SMatchP MatchP | assumption)+, goal_cases fb AD _)
          case (fb x sp)
          with MatchP hyps show ?case by (auto simp: regex.pred_set collect_alt)
        next
          case (AD x sp)
          with hyps True show ?case unfolding MatchP
            by (subst (asm) (1 2) AD_simps_regex)
               (auto simp: regex.pred_set collect_alt dest!: bspec dest: AD_mono[THEN set_mp, rotated -1])
        qed simp
      qed simp_all
    next
      case False
      with SMatchP show ?thesis
        by (cases f) (auto dest: rs_check_le2[rotated 2])
    qed
  next
    case (SMatchF rsp)
    then show ?thesis
    proof (cases f)
      case (MatchF I r)
      show ?thesis
      proof (cases "∀sp' ∈ spatms rsp. s_at sp' ≤ LTP_f σ (s_at sp) (the_enat (right I))")
        case True
        show ?thesis unfolding SMatchF MatchF s_check_simps Let_def split_beta
        proof ((rule conj_cong refl rs_check_cong IH(25) prod.collapse refl SMatchF MatchF | assumption)+, goal_cases fb AD _)
          case (fb x sp)
          with MatchF hyps show ?case by (auto simp: regex.pred_set collect_alt)
        next
          case (AD x sp)
          with hyps True show ?case unfolding MatchF
            by (subst (asm) (1 2) AD_simps_regex)
              (auto simp: regex.pred_set collect_alt dest!: bspec
                dest: AD_mono[THEN set_mp, rotated -1] order_trans[OF _ i_le_LTPi_add])
        qed simp
      next
        case False
        then obtain sp' where sp': "sp' ∈ spatms rsp" "¬ s_at sp' ≤ LTP_f σ (s_at sp) (the_enat (right I))"
          by auto
        show ?thesis unfolding SMatchF MatchF s_check_simps Let_def split_beta
        proof (intro conj_cong refl iffI, goal_cases LR RL)
          case LR
          have "∀sp ∈ spatms rsp. s_at sp ≤ snd (rs_at s_at rsp)"
            using rs_check_le2[OF _ _ LR(3)] by auto
          with LR(2) sp' hyps(2) show ?case
            using i_le_LTPi_add[of "snd (rs_at s_at rsp)" σ 0]
            unfolding SMatchF MatchF s_at.simps future_bounded.simps
            by (elim notE order_trans) (auto intro!: LTP_τ_mono elim!: order_trans)
        next
          case RL
          have "∀sp ∈ spatms rsp. s_at sp ≤ snd (rs_at s_at rsp)"
            using rs_check_le2[OF _ _ RL(3)] by auto
          with RL(2) sp' hyps(2) show ?case
            using i_le_LTPi_add[of "snd (rs_at s_at rsp)" σ 0]
            unfolding SMatchF MatchF s_at.simps future_bounded.simps
            by (elim notE order_trans) (auto intro!: LTP_τ_mono elim!: order_trans)
        qed
      qed
    qed simp_all
  qed (cases f; simp_all)+
next
  case (2 v f vp)
  note IH = 2(1-27)[OF refl] and hyps = 2(28-30)
  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 "∀x∈fv φ. 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 "∀x∈fv φ. 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 "∀x∈fv φ. 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 "∀x∈fv φ. 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 "∀x∈fv ψ. 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 "∀x∈fv φ. 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 "∀x∈fv ψ. 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 "∀x∈fv ψ. 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 "∀x∈fv φ. 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 "∀x∈fv ψ. 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
  next
    case (VMatchP i rvps)
    then show ?thesis
    proof (cases "∀rvp ∈ set rvps. ∀vp' ∈ vpatms rvp. v_at vp' ≤ v_at vp")
      case True
      with VMatchP show ?thesis
      proof (cases f)
        case (MatchP I r)
        show ?thesis unfolding VMatchP MatchP v_check_simps Let_def split_beta
        proof ((rule conj_cong ball_cong refl rv_check_cong IH(26) prod.collapse refl VMatchP MatchP | assumption)+, goal_cases fb AD _ _)
          case (fb x sp)
          with MatchP hyps show ?case by (auto simp: regex.pred_set collect_alt)
        next
          case (AD x sp)
          with hyps True show ?case unfolding MatchP
            by (subst (asm) (1 2) AD_simps_regex)
               (auto simp: regex.pred_set collect_alt dest!: bspec dest: AD_mono[THEN set_mp, rotated -1])
        qed simp_all
      qed simp_all
    next
      case False
      with VMatchP show ?thesis
        by (cases f) (auto simp: Let_def dest: rv_check_le2)
    qed
  next
    case (VMatchF ii rvps)
    then show ?thesis
    proof (cases f)
      case (MatchF I r)
      show ?thesis
      proof (cases "∀rvp ∈ set rvps. ∀vp' ∈ vpatms rvp. v_at vp' ≤ LTP_f σ (v_at vp) (the_enat (right I))")
        case True
        show ?thesis unfolding VMatchF MatchF v_check_simps Let_def split_beta
        proof ((rule conj_cong ball_cong refl rv_check_cong IH(27) prod.collapse refl VMatchF MatchF | assumption)+, goal_cases fb AD _ _)
          case (fb x sp)
          with MatchF hyps show ?case by (auto simp: regex.pred_set collect_alt)
        next
          case (AD x sp)
          with hyps True show ?case unfolding MatchF
            by (subst (asm) (1 2) AD_simps_regex)
              (auto simp: regex.pred_set collect_alt dest!: bspec
                dest: AD_mono[THEN set_mp, rotated -1] order_trans[OF _ i_le_LTPi_add])
        qed simp_all
      next
        case False
        then obtain k rvp vp' where vp': "rvp = rvps ! k" "k < length rvps" "vp' ∈ vpatms rvp" "¬ v_at vp' ≤ LTP_f σ (v_at vp) (the_enat (right I))"
          by (auto simp: in_set_conv_nth)
        moreover from vp' hyps(1) have "v_check v f vp ==> v_at vp' ≤ LTP_f σ (v_at vp) (the_enat (right I))" for v
           unfolding  VMatchF MatchF v_at.simps v_check_simps
          using [[linarith_split_limit=15]]
          by (auto simp: Let_def in_set_conv_nth nth_append nth_Cons'
             dest!: rv_check_le2[of _ _ _ _ vp'] bspec[of _ _ rvp]
             dest: arg_cong[where f="λxs. (length xs, nth xs k)"] split: if_splits)
        ultimately show ?thesis by auto
      qed
    qed simp_all
  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 ∉ 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 ∉ 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
next
  case (SMatchP j i I v r)
  then show ?case
    by (safe dest!: rs_check_complete[rotated, where test="s_check v" and testi=s_at])
      (force simp: regex.pred_set intro: exI[of _ "SMatchP _"])+
next
  case (VMatchPOut i I v r)
  then show ?case
    by (auto intro: exI[of _ "VMatchPOut i"])
next
  case (VMatchP k I i v r)
  { fix j
    assume fb: "regex.pred_regex future_bounded r" and j: "j ∈ {k..LTP_p σ i I}"
    then have "j ≤ i"
      by auto
    with j have "∃p. rv_check (v_check v) v_at r p ∧ rv_at v_at p = (j, i)"
      by (rule rv_check_complete[rotated, where test="v_check v" and testi=v_at, OF VMatchP(3)])
        (use fb in ‹auto simp: regex.pred_set›)
  } note * = this
  { assume fb: "regex.pred_regex future_bounded r"
    from *[OF this] obtain f where "rv_check (v_check v) v_at r (f j)" "rv_at v_at (f j) = (j, i)"
      if "j ∈ {k..LTP_p σ i I}" for j by metis
    with VMatchP(1,2) fb have "∃vp. v_at vp = i ∧ v_check v (\<triangleleft> I r) vp"
      by (intro exI[of _ "VMatchP i (map f [k ..< Suc (LTP_p σ i I)])"])
        (auto simp: Let_def o_def intro: map_idI split: enat.splits)
  }
  then show ?case
    by simp
next
  case (SMatchF i j I v r)
  then show ?case
    by (safe dest!: rs_check_complete[rotated, where test="s_check v" and testi=s_at])
      (force simp: regex.pred_set intro: exI[of _ "SMatchF _"])+
next
  case (VMatchF I i v r)
  let ?J = "case right I of enat b ==> {ETP_f σ i I..LTP_f σ i b} | ∞ ==> {ETP_f σ i I..}"
  { fix j
  assume fb: "regex.pred_regex future_bounded r" and j: "j ∈ ?J"
  then have "i ≤ j"
    by (auto split: enat.splits)
  with j have "∃p. rv_check (v_check v) v_at r p ∧ rv_at v_at p = (i, j)"
    by (rule rv_check_complete[rotated, where test="v_check v" and testi=v_at, OF VMatchF(1)])
      (use fb in ‹auto simp: regex.pred_set›)
  } note * = this
  { assume fb: "regex.pred_regex future_bounded r" "right I ≠ ∞"
    from *[OF this(1)] obtain f where "rv_check (v_check v) v_at r (f j)" "rv_at v_at (f j) = (i, j)"
      if "j ∈ ?J" for j by metis
    with fb have "∃vp. v_at vp = i ∧ v_check v (\<triangleright> I r) vp"
      by (intro exI[of _ "VMatchF i (map f [ETP_f σ i I ..< Suc (LTP_f σ i (the_enat (right I)))])"])
        (auto simp: Let_def o_def intro: map_idI split: enat.splits)
  }
  then show ?case
    by simp
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: "∀x∈fv φ ∪ 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
(*>*)