Library whilesound

Require Import include.
Require Import memory.
Require Import memdata.
Require Import language.
Require Import opsem.
Require Import assertion.
Require Import simulation.
Require Import lemmasforseplog.
Require Import inferules.
Require Import tacticsforseplog.
Require Import includeLib.
Require Import baseTac.
Require Import auxdef.

Lemma while_sim_aux :
forall FSpec sd I r ri asrt tp e s, (asrt ==> EX v, Rv e@tp==v) ->
      forall C c ke ks ks´ o aop O ,
        (C = (c , (ke,ks))) ->
        ((C = (SKIP,(kenil,kstop)) /\ ks´=kstop/\ (o,O,aop) |= asrt //\\ Aisfalse e) \/
        (ks´ = kseq (swhile e s) kstop /\
            ({[FSpec, sd, I, r, ri, lift asrt]} ||- (C, o) <_msim (aop, O))) \/
        (C = nilcont (swhile e s) /\ ks´ = kstop /\
                (o,O,aop) |= asrt) \/
        (ks´ = (kwhile e s kstop) /\ ks =kstop /\
              (o,O,aop) |= EX v, Rv e@tp==v /\
             estepstar (cure e) kenil (get_smem o) c ke (get_smem o)/\
                ({[FSpec, sd, I, r, ri, lift asrt ]} ||- (C, o) <_msim (aop, O)))) ->
            (forall (o : taskst) (O : osabst) (aop : absop),
               (o, O, aop) |= asrt ->
                {[FSpec, sd, I, r, ri, lift asrt ]} ||- (
                (cure e, (kenil, kstop)), o) <_msim (aop, O ))->
             (forall (o : taskst) (O : osabst) (aop : absop),
               (o, O, aop) |= asrt //\\ Aistrue e ->
                {[FSpec, sd, I, r, ri, lift asrt]} ||- (
                nilcont s, o) <_msim (aop, O )) ->
              {[FSpec, sd, I, r, ri, lift (asrt //\\ Aisfalse e)]} ||-
   ((c, (ke, ks ## ks´)), o) <_msim (aop, O ).

Lemma while_rule_sound : forall Spec sd I r ri p e s tp,
                           ( p ==> EX v , Rv e @ tp == v) ->
                  RuleSem Spec sd I r ri ( p //\\ (Aistrue e)) s p ->
                   RuleSem Spec sd I r ri p (swhile e s) (p //\\ (Aisfalse e)) .