Library conseqsound

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 conseq_rule_sound_aux : forall p sd I r ri q q´, (q ==> q´) ->
            forall C o aop O,
        {[p, sd , I, r, ri, lift q]} ||- (C, o) <_msim (aop, O ) ->
        {[p, sd , I, r, ri, lift q´]} ||- (C, o) <_msim (aop, O ).

Lemma conseq_rule_sound :
  forall Spec sd I r ri p´ p q q´ s,
    (p´ ==> p) -> (q ==> q´) ->
    RuleSem Spec sd I r ri p s q ->
    RuleSem Spec sd I r ri p´ s q´.

Lemma conseq_rule_r_sound_aux :
  forall p sd I r ri ri´ q r´, (forall v,r v==> r´ v) ->
                            ri ==> ri´ ->
                            forall C o aop O,
                              {[p, sd, I, r, ri, q]} ||- (C, o) <_msim (aop, O ) ->
                              {[p, sd, I, r´, ri´, q]} ||- (C, o) <_msim (aop, O ).

Lemma conseq_rule_r_sound : forall Spec sd I r r´ ri ri´ p q s,
                               (forall v,r v ==> r´ v) ->
                               ri ==> ri´ ->
                               RuleSem Spec sd I r ri p s q ->
                              RuleSem Spec sd I r´ ri´ p s q.

Lemma absconseq_rule_sound_aux : forall p sd I r ri q q´, (absimp´ q q´) ->
            forall C o aop O,
        {[p, sd , I, r, ri, lift q]} ||- (C, o) <_msim (aop, O ) ->
        {[p, sd, I, r, ri, lift q´]} ||- (C, o) <_msim (aop, O ).

Lemma hmstepstar_seq :
  forall s1 O x s2 s1´,
    hmstepstar s1 O s1´ x ->
    hmstepstar (s1;; s2) O (s1´;; s2) x.

Lemma absinfersound :
  forall p q, absinfer p q -> absimp p q.

Lemma absimp_imp :
  forall p q, absimp p q -> absimp´ p q.

Lemma abscsq_rule_sound : forall Spec sd I r ri p´ p q q´ s ,
                             absinfer p´ p -> absinfer q q´ ->
                                RuleSem Spec sd I r ri p s q ->
                                 RuleSem Spec sd I r ri p´ s q´.