| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/Archive-of-Formal-Proofs/thys/MFOTL_Checker/ (Archive of formal Proofs Version 2026-5©) Datei vom 31.4.2026 mit Größe 165 kB |
|
Quelle Checker.thy Sprache: Isabelle |
|||||||||||||||||||||||||
|
(*<*) 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 ( | (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) | (\<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) | ( _ , _) → 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 ( | (∀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 simps_of_case v_check_simps[simp]: v_check.simps[unfolded prod.case] (splits: formula 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 p 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 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 (L 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 p 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) ..< 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_a 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 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_a 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 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' ∧ ( 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_valu 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 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 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 in else if list_all (λtX. Max (set (positions tXs tX)) < Max (set (positions (map fst then {p} × mk_values tXs ⊆ X else (if finite X then False else Code.abort STR ''subset on infinite subset'' (λ 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 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_va 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 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 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\<lbr 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\<rbr 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 | "check_values vs (v x # ts) (u # us) (Some v) = (if u ∈ vs x ∧ (v x = Some u ∨ | "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 shows "check_values vs ts ((λx. case f x of None → v x | Some y → y)\<lbrakk>ts\<rbrak 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 → 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 des 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_con 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 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!: spe 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 = | (φ ⟶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 | (φ ⟷F ψ, SIffVV vp1 vp2) → v_check_exec vs φ vp1 ∧ v_check_exec vs ψ vp2 ∧ v_at vp1 | (∃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 := | (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_ex | (\<triangleright> I r, SMatchF rsp) → (let (i, j) = rs_at s_at rsp in i ≤ j ∧ mem (τ σ j - τ σ i) I ∧ rs_check (s_check_ex | ( _ , _) → 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 = | (φ ∧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 = | (φ ⟷F ψ, VIffSV sp1 vp2) → s_check_exec vs φ sp1 ∧ v_check_exec vs ψ vp2 ∧ s_at sp1 | (φ ⟷F ψ, VIffVS vp1 sp2) → v_check_exec vs φ vp1 ∧ s_check_exec vs ψ sp2 ∧ v_at vp1 | (∃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 := | (∀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) = | (\<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) = | ( _ , _) → 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] (spli simps_of_case v_check_exec_simps[simp]: v_check_exec.simps[unfolded prod.case] (spli 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 unfolding compatible_vals_def by auto lemma fun_upd_in_compatible_vals: "v ∈ compatible_vals (A - {x}) vs ==> v(x := t) unfolding compatible_vals_def by auto lemma fun_upd_in_compatible_vals_in: "v ∈ compatible_vals (A - {x}) vs ==> t ∈ vs unfolding compatible_vals_def by auto lemma fun_upd_in_compatible_vals_notin: "x ∉ A ==> v ∈ compatible_vals A vs ==> v( 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_va 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_va 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_va next case φ2 then show ?case by (metis (mono_tags, lifting) 2 IntE Un_upper2 compatible_vals_extensible compatible_va 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_va next case φ2 then show ?case by (metis (mono_tags, lifting) 1 IntE Un_upper2 compatible_vals_extensible compatible_va 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_va 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_va 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_va 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_va 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_va next case φ2 then show ?case by (metis (mono_tags, lifting) 2 IntE Un_upper2 compatible_vals_extensible compatible_va 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_va next case φ2 then show ?case by (metis (mono_tags, lifting) 1 IntE Un_upper2 compatible_vals_extensible compatible_va 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_va next case φ2 then show ?case by (metis (mono_tags, lifting) 1 IntE Un_upper2 compatible_vals_extensible compatible_va 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_va next case φ2 then show ?case by (metis (mono_tags, lifting) 2 IntE Un_upper2 compatible_vals_extensible compatible_va 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_va next case φ2 then show ?case by (metis (mono_tags, lifting) 2 IntE Un_upper2 compatible_vals_extensible compatible_va 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_c 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 compatib 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 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_up 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 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_up 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_c 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 compatib } 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 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_va 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_va 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 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_va 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_va qed next case (VSinceInf i j vps) show ?thesis unfolding VSinceInf v_check_exec_simps v_check_simps fv.simps ball_conj_distrib ball_s 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_va 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 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_va 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_va 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 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_va 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_va qed next case (VUntilInf i j vps) show ?thesis unfolding VUntilInf v_check_exec_simps v_check_simps fv.simps ball_conj_distrib ball_s 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_va 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_con 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_con 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_con 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_con 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 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 | "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 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)[ro 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)[ro 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 f 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\<rbra 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)) - by (auto 0 3 simp: AD_def max_opt_def not_none_fb_LRTP le_max_iff_disj Bex_def split: optio lemma AD_simps_regex[simp]: "future_bounded (\<triangleleft> I r) ==> regex.atms r ≠ {} ==> AD (\<triangleleft "future_bounded (\<triangleright> I r) ==> regex.atms r ≠ {} ==> AD (\<trianglerig unfolding AD_def by (auto 0 6 simp: Let_def collect_alt regex.pred_set image_image Ball_def not_none_fb_LRT 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_s 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_ 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)) Until(2)[of "LTP_f σ i (the_enat (right I))" "LTP_f σ j (the_enat (right I))"] Until( 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 (LRT 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 (LR 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[o 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 re 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 re 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 | assump 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 | assump 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 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, 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, 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 \<phi> I \<psi>) { fix vp :: "('n, 'd) vproof" define l and u where "l = v_at vp" and "u = LTP_f \<sigma> i (the_enat (right I))" assume *: "vp \<in> 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 \<sigma> i I ..< Suc u]" then have "length vps = Suc u - ETP_f \<sigma> i I" by (auto dest!: arg_cong[where f=length]) with j eq have "l \<le> LTP_f \<sigma> i (the_enat (right I))" by (auto simp: l_def u_def dest!: arg_cong[where f="\<lambda>xs. nth xs j"] simp del: upt.simps split: if_splits) with Until hyps(2,3) have "\<forall>x\<in>fv \<psi>. v x = v' x \<or> v x \<notin> AD \<psi> l \<and> v' x \<notin> AD 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 "\<forall>rvp \<in> set rvps. \<forall>vp' \<in> vpatms rvp. v_at vp' \<le> 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 Matc 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 "\<forall>rvp \<in> set rvps. \<forall>vp' \<in> vpatms rvp. v_at vp' \<le> LTP_f \<sigma> (v_ 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 Matc 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' \<in> vpatms rvp" "\<not> v_at vp' by (auto simp: in_set_conv_nth) moreover from vp' hyps(1) have "v_check v f vp \<Longrightarrow> v_at vp' \<le> LTP_f \<sigma> (v_at 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="\<lambda>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 \<open>Checker Completeness\<close> lemma part_hd_tabulate: "distinct xs \<Longrightarrow> part_hd (tabulate xs f z) = (case xs of [ by (transfer, auto split: list.splits) lemma s_at_tabulate: assumes "\<forall>z. s_at (mypick z) = i" and "mypart = tabulate (sorted_list_of_set (AD \<phi> i)) mypick (mypick (SOME z. z \<notin> AD \<ph shows "\<forall>(sub, vp) \<in> SubsVals mypart. s_at vp = i" using assms by (transfer, auto) lemma v_at_tabulate: assumes "\<forall>z. v_at (mypick z) = i" and "mypart = tabulate (sorted_list_of_set (AD \<phi> i)) mypick (mypick (SOME z. z \<notin> AD \<ph shows "\<forall>(sub, vp) \<in> SubsVals mypart. v_at vp = i" using assms by (transfer, auto) lemma s_check_tabulate: assumes "future_bounded \<phi>" and "\<forall>z. s_at (mypick z) = i" and "\<forall>z. s_check (v(x:=z)) \<phi> (mypick z)" and "mypart = tabulate (sorted_list_of_set (AD \<phi> i)) mypick (mypick (SOME z. z \<notin> AD \<ph shows "\<forall>(sub, vp) \<in> SubsVals mypart. \<forall>z \<in> sub. s_check (v(x := z)) \<phi> vp" using assms proof (transfer fixing: \<sigma> \<phi> mypick i v x, goal_cases 1) case (1 mypart) { fix z assume s_at_assm: "\<forall>z. s_at (mypick z) = i" and s_check_assm: "\<forall>z. s_check (v(x := z)) \<phi> (mypick z)" and fb_assm: "future_bounded \<phi>" and z_notin_AD: "z \<notin> (AD \<phi> i)" have s_at_mypick: "s_at (mypick (SOME z. z \<notin> AD \<phi> i)) = i" using s_at_assm by simp have s_check_mypick: "Checker.s_check \<sigma> (v(x := SOME z. z \<notin> AD \<phi> i)) \<phi> (mypick using s_check_assm by simp have "s_check (v(x := z)) \<phi> (mypick (SOME z. z \<notin> AD \<phi> i))" using z_notin_AD by (subst check_AD_cong(1)[of \<phi> "v(x := z)" "v(x := (SOME z. z \<notin> Checker.AD \<sigma> \<phi> (auto simp add: someI[of "\<lambda>z. z \<notin> AD \<phi> i" z] s_check_mypick fb_assm split: if_sp } with 1 show ?case by auto qed lemma v_check_tabulate: assumes "future_bounded \<phi>" and "\<forall>z. v_at (mypick z) = i" and "\<forall>z. v_check (v(x:=z)) \<phi> (mypick z)" and "mypart = tabulate (sorted_list_of_set (AD \<phi> i)) mypick (mypick (SOME z. z \<notin> AD \<ph shows "\<forall>(sub, vp) \<in> SubsVals mypart. \<forall>z \<in> sub. v_check (v(x := z)) \<phi> vp" using assms proof (transfer fixing: \<sigma> \<phi> mypick i v x, goal_cases 1) case (1 mypart) { fix z assume v_at_assm: "\<forall>z. v_at (mypick z) = i" and v_check_assm: "\<forall>z. v_check (v(x := z)) \<phi> (mypick z)" and fb_assm: "future_bounded \<phi>" and z_notin_AD: "z \<notin> (AD \<phi> i)" have v_at_mypick: "v_at (mypick (SOME z. z \<notin> AD \<phi> i)) = i" using v_at_assm by simp have v_check_mypick: "Checker.v_check \<sigma> (v(x := SOME z. z \<notin> AD \<phi> i)) \<phi> (mypick using v_check_assm by simp have "v_check (v(x := z)) \<phi> (mypick (SOME z. z \<notin> AD \<phi> i))" using z_notin_AD by (subst check_AD_cong(2)[of \<phi> "v(x := z)" "v(x := (SOME z. z \<notin> Checker.AD \<sigma> \<phi> (auto simp add: someI[of "\<lambda>z. z \<notin> AD \<phi> i" z] v_check_mypick fb_assm split: if_sp } with 1 show ?case by auto qed lemma s_at_part_hd_tabulate: assumes "future_bounded \<phi>" and "\<forall>z. s_at (f z) = i" and "mypart = tabulate (sorted_list_of_set (AD \<phi> i)) f (f (SOME z. z \<notin> AD \<phi> 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 \<phi>" and "\<forall>z. v_at (f z) = i" and "mypart = tabulate (sorted_list_of_set (AD \<phi> i)) f (f (SOME z. z \<notin> AD \<phi> i))" shows "v_at (part_hd mypart) = i" using assms by (simp add: part_hd_tabulate split: list.splits) lemma check_completeness_aux: "(SAT \<sigma> v i \<phi> \<longrightarrow> future_bounded \<phi> \<longrightarrow> (\<exists>sp. s_at (VIO \<sigma> v i \<phi> \<longrightarrow> future_bounded \<phi> \<longrightarrow> (\<exists>vp. v_at v proof (induct v i \<phi> 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 \<phi>) then show ?case by (auto intro: exI[of _ "SNeg _"]) next case (VNeg v i \<phi>) then show ?case by (auto intro: exI[of _ "VNeg _"]) next case (SOrL v i \<phi> \<psi>) then show ?case by (auto intro: exI[of _ "SOrL _"]) next case (SOrR v i \<psi> \<phi>) then show ?case by (auto intro: exI[of _ "SOrR _"]) next case (VOr v i \<phi> \<psi>) then show ?case by (auto 0 3 intro: exI[of _ "VOr _ _"]) next case (SAnd v i \<phi> \<psi>) then show ?case by (auto 0 3 intro: exI[of _ "SAnd _ _"]) next case (VAndL v i \<phi> \<psi>) then show ?case by (auto intro: exI[of _ "VAndL _"]) next case (VAndR v i \<psi> \<phi>) then show ?case by (auto intro: exI[of _ "VAndR _"]) next case (SImpL v i \<phi> \<psi>) then show ?case by (auto intro: exI[of _ "SImpL _"]) next case (SImpR v i \<psi> \<phi>) then show ?case by (auto intro: exI[of _ "SImpR _"]) next case (VImp v i \<phi> \<psi>) then show ?case by (auto 0 3 intro: exI[of _ "VImp _ _"]) next case (SIffSS v i \<phi> \<psi>) then show ?case by (auto 0 3 intro: exI[of _ "SIffSS _ _"]) next case (SIffVV v i \<phi> \<psi>) then show ?case by (auto 0 3 intro: exI[of _ "SIffVV _ _"]) next case (VIffSV v i \<phi> \<psi>) then show ?case by (auto 0 3 intro: exI[of _ "VIffSV _ _"]) next case (VIffVS v i \<phi> \<psi>) then show ?case by (auto 0 3 intro: exI[of _ "VIffVS _ _"]) next case (SExists v x i \<phi>) then show ?case by (auto 0 3 simp: fun_upd_def intro: exI[of _ "SExists x _ _"]) next case (VExists v x i \<phi>) show ?case proof assume "future_bounded (\<exists>\<^sub>Fx. \<phi>)" then have fb: "future_bounded \<phi>" by simp obtain mypick where mypick_def: "v_at (mypick z) = i \<and> v_check (v(x:=z)) \<phi> (mypick z)" fo using VExists fb by metis define mypart where "mypart = tabulate (sorted_list_of_set (AD \<phi> i)) mypick (mypick (SOME have mypick_at: "\<forall>z. v_at (mypick z) = i" by (simp add: mypick_def) have mypick_v_check: "\<forall>z. v_check (v(x:=z)) \<phi> (mypick z)" by (simp add: mypick_def) have mypick_v_check2: "\<forall>z. v_check (v(x := (SOME z. z \<notin> AD \<phi> i))) \<phi> (mypick (S 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 (\<exists>\<^sub>Fx. \<phi>) (VExists x mypart)" using v_at_tabulate[of mypick i _ \<phi>, 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 "\<exists>vp. v_at vp = i \<and> v_check v (\<exists>\<^sub>Fx. \<phi>) vp" using v_at_myp v_check_myp by blast qed next case (SForall v x i \<phi>) show ?case proof assume "future_bounded (\<forall>\<^sub>Fx. \<phi>)" then have fb: "future_bounded \<phi>" by simp obtain mypick where mypick_def: "s_at (mypick z) = i \<and> s_check (v(x:=z)) \<phi> (mypick z)" fo using SForall fb by metis define mypart where "mypart = tabulate (sorted_list_of_set (AD \<phi> i)) mypick (mypick (SOME have mypick_at: "\<forall>z. s_at (mypick z) = i" by (simp add: mypick_def) have mypick_s_check: "\<forall>z. s_check (v(x:=z)) \<phi> (mypick z)" by (simp add: mypick_def) have mypick_s_check2: "\<forall>z. s_check (v(x := (SOME z. z \<notin> AD \<phi> i))) \<phi> (mypick (S 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 (\<forall>\<^sub>Fx. \<phi>) (SForall x mypart)" using s_at_tabulate[of mypick i _ \<phi>, 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 "\<exists>sp. s_at sp = i \<and> s_check v (\<forall>\<^sub>Fx. \<phi>) sp" using s_at_myp s_check_myp by blast qed next case (VForall v x i \<phi>) then show ?case by (auto 0 3 simp: fun_upd_def intro: exI[of _ "VForall x _ _"]) next case (SPrev i I v \<phi>) then show ?case by (force intro: exI[of _ "SPrev _"]) next case (VPrev i v \<phi> I) then show ?case by (force intro: exI[of _ "VPrev _"]) next case (VPrevZ i v I \<phi>) then show ?case by (auto intro!: exI[of _ "VPrevZ"]) next case (VPrevOutL i I v \<phi>) then show ?case by (auto intro!: exI[of _ "VPrevOutL i"]) next case (VPrevOutR i I v \<phi>) then show ?case by (auto intro!: exI[of _ "VPrevOutR i"]) next case (SNext i I v \<phi>) then show ?case by (force simp: Let_def intro: exI[of _ "SNext _"]) next case (VNext v i \<phi> I) then show ?case by (force simp: Let_def intro: exI[of _ "VNext _"]) next case (VNextOutL i I v \<phi>) then show ?case by (auto intro!: exI[of _ "VNextOutL i"]) next case (VNextOutR i I v \<phi>) then show ?case by (auto intro!: exI[of _ "VNextOutR i"]) next case (SOnce j i I v \<phi>) then show ?case by (auto simp: Let_def intro: exI[of _ "SOnce i _"]) next case (VOnceOut i I v \<phi>) then show ?case by (auto intro!: exI[of _ "VOnceOut i"]) next case (VOnce j I i v \<phi>) show ?case proof assume "future_bounded (\<^bold>P I \<phi>)" then have fb: "future_bounded \<phi>" by simp obtain mypick where mypick_def: "\<forall>k \<in> {j .. LTP_p \<sigma> i I}. v_at (mypick k) = k \<and> v_ using VOnce fb by metis then obtain vps where vps_def: "map (v_at) vps = [j ..< Suc (LTP_p \<sigma> i I)] \<and> (\<forall>vp \<in> by atomize_elim (auto intro!: trans[OF list.map_cong list.map_id] exI[of _ "map mypick ([j . then have "v_at (VOnce i j vps) = i \<and> v_check v (\<^bold>P I \<phi>) (VOnce i j vps)" using VOnce by auto then show "\<exists>vp. v_at vp = i \<and> v_check v (\<^bold>P I \<phi>) vp" by blast qed next case (SEventually j i I v \<phi>) then show ?case by (auto simp: Let_def intro: exI[of _ "SEventually i _"]) next case (VEventually I i v \<phi>) show ?case proof assume fb_eventually: "future_bounded (\<^bold>F I \<phi>)" then have fb: "future_bounded \<phi>" 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 \<sigma> (\<tau> \<sigma> i + b)" obtain mypick where mypick_def: "\<forall>k \<in> {ETP_f \<sigma> i I .. j}. v_at (mypick k) = k \<and> v_ 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 \<sigma> i I ..< Suc j] \<and> (\<forall>vp \<in> se by atomize_elim (auto intro!: trans[OF list.map_cong list.map_id] exI[of _ "map mypick ([ET then have "v_at (VEventually i j vps) = i \<and> v_check v (\<^bold>F I \<phi>) (VEventually i j vps)" using VEventually b_def j_def by simp then show "\<exists>vp. v_at vp = i \<and> v_check v (\<^bold>F I \<phi>) vp" by blast qed next case (SHistorically j I i v \<phi>) show ?case proof assume fb_historically: "future_bounded (\<^bold>H I \<phi>)" then have fb: "future_bounded \<phi>" by simp obtain mypick where mypick_def: "\<forall>k \<in> {j .. LTP_p \<sigma> i I}. s_at (mypick k) = k \<and> s_ using SHistorically fb by metis then obtain sps where sps_def: "map (s_at) sps = [j ..< Suc (LTP_p \<sigma> i I)] \<and> (\<forall>sp \<in> by atomize_elim (auto intro!: trans[OF list.map_cong list.map_id] exI[of _ "map mypick ([j . then have "s_at (SHistorically i j sps) = i \<and> s_check v (\<^bold>H I \<phi>) (SHistorically i j sps using SHistorically by auto then show "\<exists>sp. s_at sp = i \<and> s_check v (\<^bold>H I \<phi>) sp" by blast qed next case (SHistoricallyOut i I v \<phi>) then show ?case by (auto intro!: exI[of _ "SHistoricallyOut i"]) next case (VHistorically j i I v \<phi>) then show ?case by (auto simp: Let_def intro: exI[of _ "VHistorically i _"]) next case (SAlways I i v \<phi>) show ?case proof assume fb_always: "future_bounded (\<^bold>G I \<phi>)" then have fb: "future_bounded \<phi>" 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 \<sigma> (\<tau> \<sigma> i + b)" obtain mypick where mypick_def: "\<forall>k \<in> {ETP_f \<sigma> i I .. j}. s_at (mypick k) = k \<and> s_ 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 \<sigma> i I ..< Suc j] \<and> (\<forall>sp \<in> se by atomize_elim (auto intro!: trans[OF list.map_cong list.map_id] exI[of _ "map mypick ([ET then have "s_at (SAlways i j sps) = i \<and> s_check v (\<^bold>G I \<phi>) (SAlways i j sps)" using SAlways b_def j_def by simp then show "\<exists>sp. s_at sp = i \<and> s_check v (\<^bold>G I \<phi>) sp" by blast qed next case (VAlways j i I v \<phi>) then show ?case by (auto simp: Let_def intro: exI[of _ "VAlways i _"]) next case (SSince j i I v \<psi> \<phi>) show ?case proof assume fb_since: "future_bounded (\<phi> \<^bold>S I \<psi>)" then have fb: "future_bounded \<phi>" "future_bounded \<psi>" by simp_all obtain sp2 where sp2_def: "s_at sp2 = j \<and> s_check v \<psi> sp2" using SSince fb_since by auto { assume "Suc j > i" then have "s_at (SSince sp2 []) = i \<and> s_check v (\<phi> \<^bold>S I \<psi>) (SSince sp2 [])" using sp2_def SSince by auto then have "\<exists>sp. s_at sp = i \<and> s_check v (\<phi> \<^bold>S I \<psi>) 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_chec 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 sp1 by atomize_elim (auto intro!: trans[OF list.map_cong list.map_id] exI[of _ "map mypick ([ 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_che 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 ∈ by atomize_elim (auto intro!: trans[OF list.map_cong list.map_id] exI[of _ "map mypick ([ 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_che 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 ∈ by atomize_elim (auto intro!: trans[OF list.map_cong list.map_id] exI[of _ "map mypick ([ 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 φ (my 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_che by atomize_elim (auto intro!: trans[OF list.map_cong list.map_id] exI[of _ "map mypick ([ 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_che 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 ∈ se by atomize_elim (auto intro!: trans[OF list.map_cong list.map_id] exI[of _ "map mypick ([ 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_che 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 ∈ se by atomize_elim (auto intro!: trans[OF list.map_cong list.map_id] exI[of _ "map mypick ([ 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 (afe 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 yto xIf"VacPu ") next case (VMatchP k I ) { ix assume fb: "regeexport_ ope seaPoeCd nHsel 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 VMa (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 (\◃ 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 VMa (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) = ( if "j ∈ ?J" for j by metis with fb have "∃vp. v_at vp = i ∧ v_check v (\▹ 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 ( 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 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 _ _ _ _ compatibl case (compatible v) from compatible(2-) compatible(1)[THEN bspec, of "v(x := d)"] compatible(1)[THEN b 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) ex "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_completen then show ?thesis by (intro exI[of _ "Leaf (Inl sp)"]) (auto simp: vars_order.intros p_check_def p_a 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_completen then show ?thesis by (intro exI[of _ "Leaf (Inr vp)"]) (auto simp: vars_order.intros p_check_def p_a 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 (p 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_p 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_a unbundle no MFOTL_syntax (*<*) end (*>*)
¤ Dauer der Verarbeitung: 0.249 Sekunden (vorverarbeitet am 2026-11-04) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||||||||||||
2026-11-01