Require Import Facts States ICSemantics.
Set Implicit Arguments.
Unset Strict Implicit.

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).
Proof.
  move⇒ x /wp_det[f[y[sx/=[m dm]]]]. ∃ m. apply: wp_mono x sx.
    by move⇒ g x [<-<-].
Qed.

Lemma wp_cons_continuous (D Q : NPred state) s :
  wp (sup D .: Q) s <<= sup (fun m ⇒ wp (D m .: Q) s).
Proof.
  move⇒ x sx. apply: wp_continuous. by apply: wp_mono x sx ⇒ -[].
Qed.

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.
Proof.
  apply: fix_fixk. move⇒ D _. exact: wp_cons_continuous. exact: wp_cons_mono.
Qed.

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.
Proof.
  split=>/=; apply: wp_mono x ⇒ -[]//= x; by rewrite wp_fix_kleene.
Qed.

End ICContinuity.