Commit df884836 authored by charguer's avatar charguer

normally2

parent 2ac9d251
......@@ -1261,6 +1261,60 @@ Qed.
(* * Extension: [normally] modality (WORK IN PROGRESS) *)
Module Normally1.
Program Definition normally (H:hprop) :=
fun h => H (h^f,fmap_empty).
Lemma normally_intro : forall H,
normal H ->
H ==> normally H.
Proof using.
introv N. unfolds normal, normally.
intros h M. lets: (>> N M).
skip.
Qed.
(*
Lemma normal_normally : forall H,
normal (normally H).
Proof using.
intros H. unfolds normal, normally. intros h M.
Qed.
*)
Lemma normally_himpl : forall H1 H2,
(H1 ==> H2) ->
normally H1 ==> normally H2.
Proof using.
introv M. unfold normal, normally.
intros h N. hhsimpl~.
Qed.
Lemma normally_hstar : forall H1 H2,
normally H1 \* normally H2 ==> normally (H1 \* H2).
Proof using.
intros. unfold normal, normally. intros h (h1&h2&M1&M2&M3&M4).
(* exists (h1^f \+ h2^f, (fmap_empty:state)).*)
skip.
Qed.
Lemma normally_idempotent1 : forall H,
normally H ==> normally (normally H).
Proof using.
intros. unfolds normal, normally. intros h M. simpl.
(* *)
skip.
Qed.
End Normally1.
(* ---------------------------------------------------------------------- *)
Module Normally2.
Definition normally H :=
Hexists H1 H2, \[normal H1] \* H1 \* \[H1 \* RO H2 ==> H].
......@@ -1306,6 +1360,7 @@ Proof using.
intros. applys normally_intro. applys normal_normally.
Qed.
End Normally2.
(* ---------------------------------------------------------------------- *)
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment