Theory Checker

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

section ‹Proof Checker›

unbundle MFOTL_syntax

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

begin

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

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

subsection ‹Checker Soundness›

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

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

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

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

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

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

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

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

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

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

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

lemmas compatible_vals_extensible = compatible_extensible[unfolded compatible_alt]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

subsection ‹Executable Variant of the Checker›

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

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