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 : nat → NPred state) s :
  wp (sup \o D) s <<= sup (fun m ⇒ wp (D^~ m) s).

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

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

Lemma wp_fix_kleene Q s x :
  Fix (fun P ⇒ wp (P .: Q) s) x ↔ sup (fun n ⇒ fix_step n Q s) x.

Corollary wp_defn Q s t x :
  wp Q (Def s t) x ↔ wp (sup (fun i ⇒ fix_step i Q s) .: Q) t x.

End ICContinuity.