Library ICContinuity

Continuity of the WP semantics for IC

This is a consequence of determinism. Continuity enables a different characterization of the WP predicate in terms of omega-iteration.
Require Import Facts States ICSemantics.
Set Implicit Arguments.

Module ICContinuity (Sigma : State).
Module ICSem := ICSemantics.ICSemantics Sigma.
Import Sigma.
Export ICSem.

Lemma wp_continuous (D : natNPred state) s :
  wp (sup \o D) s <<= sup (fun mwp (D^~ m) s).

Lemma wp_cons_continuous (D Q : NPred state) s :
  wp (sup D .: Q) s <<= sup (fun mwp (D m .: Q) s).

Definition fix_step n Q s :=
  iter n (fun Pwp (P .: Q) s) bot.

Lemma wp_fix_kleene Q s x :
  Fix (fun Pwp (P .: Q) s) x sup (fun nfix_step n Q s) x.

Corollary wp_defn Q s t x :
  wp Q (Def s t) x wp (sup (fun ifix_step i Q s) .: Q) t x.

End ICContinuity.