Library switchsound

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 switch_rule_sound´ :
  forall Spec sd I r ri x s,
    (SWINV I) ==> (SWPRE sd x) ->
    RuleSem Spec sd I r ri ((SWINV I) //\\ <|spec_seq sched s|>)
            (sprim (switch x)) ((SWINV I) //\\ <|s|>).

Lemma switch_rule_sound : forall Spec sd I r ri x P is cs s,
                            P ==>
                            SWINV I ** Ais is ** Acs cs //\\ <|spec_seq sched s|>->
                            P ==> (SWPRE sd x) ->
                            RuleSem Spec sd I r ri ( P )
                                    (sprim (switch x)) ((SWINV I ** Ais is ** Acs cs) //\\ <|s|>).