Library framesound

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.
Require Import conseqsound.

Lemma frame_sim_aux : forall p sd C gamma o o´ O O´ I ri r q frm M Of,
  GoodI I sd ->
   (joinmem o M o´) ->
   (OSAbstMod.join O Of O´) ->
   (~isalloc C /\ ~ isfree C /\ nci C /\ n_dym_com_int_cd C) ->
   (GoodFrm frm /\ sat (substmo (o, O ,gamma) M Of) frm) ->
  ({[p, sd , I, r , ri, lift q]} ||- (C, o) <_msim (gamma, O)) ->
 {[p, sd, I, (fun v => (r v)**frm), ri**frm, lift (q**frm)]} ||- (C, o´) <_msim (gamma, O´).

Lemma frame_rule_all_sound :
  forall Spec sd I r ri p q frm s,
    GoodI I sd ->
    GoodStmt´ s ->
    GoodFrm frm->
    RuleSem Spec sd I r ri p s q ->
    RuleSem Spec sd I (fun v =>(r v) ** frm)
            (ri**frm) (p ** frm) s (q ** frm ) .

Lemma frame_rule_sound:
forall Spec sd I p q frm s aop aop´,
  GoodI I sd ->
  GoodStmt´ s -> GoodFrm frm ->
  RuleSem Spec sd I arfalse Afalse (p //\\ <|aop|>) s (q //\\ <|aop´|>) ->
  RuleSem Spec sd I arfalse Afalse (p ** frm //\\ <|aop|>) s (q ** frm //\\ <|aop´|>) .