Properties of the denotation-based condition interpretation

DenoteBasedInterp F reads a condition captured under a runtime factory over F by its evaluation to true, so on such conditions it agrees with evaluation to true (evalInterp_holds_iff_denoteBasedInterp). A condition captured under another factory is read by an arbitrary predicate of the world, so DenoteBasedInterp F is stable under an event-argument relation only for conditions captured over F (denoteBasedInterp_stableUnder), and a trace relation stated under evaluation to true carries over to it only for traces whose events are captured over F (weakensAssumes_denoteBasedInterp).

Key theorems: evalInterp_holds_iff_denoteBasedInterp, denoteBasedInterp_stableUnder, weakensAssumes_denoteBasedInterp.

theorem Core.Logic.evalInterp_holds_iff_denoteBasedInterp {F : Lambda.Factory CoreLParams} (w : (DenoteBasedInterp F).World) (c : Imperative.EventArg Expression) (hc : c.factory.factory = F) : Imperative.BigStep.evalInterp.holds () c ↔ (DenoteBasedInterp F).holds w c

For a condition captured under a runtime factory over F, reading it under its own runtime factory (Imperative.BigStep.evalInterp) agrees with DenoteBasedInterp F in every world.

theorem Core.Logic.denoteBasedInterp_stableUnder {F : Lambda.Factory CoreLParams} {R : Imperative.EventArg Expression → Imperative.EventArg Expression → Prop} (hstable : Imperative.BigStep.evalInterp.StableUnder R) (hfac : ∀ {a b : Imperative.EventArg Expression}, R a b → b.factory = a.factory) : (DenoteBasedInterp F).StableUnder fun (a b : Imperative.EventArg Expression) => R a b ∧ a.factory.factory = F

DenoteBasedInterp F is stable on conditions captured over F. For an event-argument relation R keeping the factory, under which evaluation to true is stable: related conditions whose source is captured under a runtime factory over F hold alike under DenoteBasedInterp F.

theorem Core.Logic.weakensAssumes_denoteBasedInterp {F : Lambda.Factory CoreLParams} {s t : Imperative.Trace Expression} (h : Imperative.Trace.WeakensAssumes Imperative.BigStep.evalInterp s t) (hs : ∀ (ev : Imperative.Event Expression), ev ∈ s → ev.condition.factory.factory = F) (ht : ∀ (ev : Imperative.Event Expression), ev ∈ t → ev.condition.factory.factory = F) : Imperative.Trace.WeakensAssumes (DenoteBasedInterp F) s t

Weakened assumptions under evaluation are weakened assumptions under the denotation, for traces whose events are all captured under runtime factories over F.