Theory Checker
theory Checker
imports Prelim Proof_System Proof_Object "HOL-Library.Simps_Case_Conv"
begin
section ‹Proof Checker›
unbundle MFOTL_notation
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, v❙⟦ts❙⟧) ∈ Γ σ 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, v❙⟦ts❙⟧) ∉ Γ σ 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