Library joinmemLib

Require Import include.
Require Import memory.
Require Import memdata.
Require Import language.
Require Import opsem.
Require Import assertion.
Require Import baseTac.
Require Import simulation.

Lemma Mem_minus_disj : forall M m, MemMod.disj (MemMod.minus M m) m.

Lemma join_minus_r : forall m1 m2 m3 M,
  MemMod.join m1 m2 (MemMod.minus M m3) ->
  exists mx, MemMod.join m2 m3 mx.

Lemma taskst_join_merge : forall o o1 M1 M2 o´, joinmem o M1 o1 ->
     joinmem o1 M2 o´ -> exists M3, MemMod.join M1 M2 M3 /\ joinmem o M3 o´.

Lemma join_intro_l: forall G E M isr aux M´ o, joinmem (G, E , M, isr, aux) M´ o -> exists M1, MemMod.join M M´ M1 /\ o = (G,E,M1,isr,aux).

Lemma join_intro_r : forall G E M isr aux M´ o, joinmem o M´ (G, E , M, isr, aux) -> exists M1, MemMod.join M1 M´ M /\ o = (G,E,M1,isr,aux).

Lemma Mem_join_disj : forall M1 M2 M, MemMod.join M1 M2 M -> MemMod.disj M1 M2.

Lemma join_mjoin_intro_intro: forall G E M1 isr aux M2 M3 M o,
                        joinmem (G,E,M1,isr,aux) M o ->
                        MemMod.join M2 M3 M
                    -> exists M´, joinmem (G,E,M´,isr,aux) M2 o /\ MemMod.join M1 M3 M´.

Lemma join_frame_dis : forall o1 M o1´ Ms o0 Mf o2,
                          joinmem o1 M o1´ ->
                          joinmem o1´ Ms o0 ->
                          joinmem o0 Mf o2 ->
                          exists o M´, joinmem o1 Ms o /\
                          joinmem o M´ o2 /\ joinmem o M o0 /\ MemMod.join M Mf M´.

Lemma join_sub_inv: forall o1 M o1´ Ms Os ab I, joinmem o1 M o1´ ->
                       (substaskst o1´ Ms, Os, ab) |= INV I ->
                     (substaskst o1 Ms, Os, ab) |= INV I.

Lemma join_sub_inv_rev: forall o1 M o1´ Ms Os ab I, joinmem o1 M o1´ ->
                       (substaskst o1 Ms, Os, ab) |= INV I ->
                     (substaskst o1´ Ms, Os, ab) |= INV I.

Lemma join_inject: forall o1 M1 o2 M o3 M0 Mf , joinmem o2 M o3 ->
                                          joinmem o1 M1 o2 ->
                                          MemMod.join M0 Mf M ->
                            exists o2´ o1´ , joinmem o2´ Mf o3 /\joinmem o1´ M1 o2´
                                          /\ joinmem o1 M0 o1´.

Lemma joinmem_get_disj : forall o M o´,joinmem o M o´ -> MemMod.disj (get_mem (get_smem o)) M.

Lemma join_memj_intro : forall o M o´ M1 M2, joinmem o M o´ -> MemMod.join M1 M2 M ->
          exists o1 , joinmem o1 M2 o´ /\ joinmem o M1 o1.

Lemma join_disj_disj : forall o M o´ Ms,
                     joinmem o M o´ -> MemMod.disj (get_mem (get_smem o´)) Ms ->
                             MemMod.disj (get_mem (get_smem o)) Ms.

Lemma join_join_intro : forall o M o´ M´ o´´ ,joinmem o M o´ -> joinmem o´ M´ o´´ ->
         exists M1, joinmem o M1 o´´/\ MemMod.join M M´ M1.

Lemma join_swinv_prop : forall o M o´ Mc aop O I, joinmem o M o´ ->
                        (substaskst o Mc, O, aop) |= SWINV I
                         -> (substaskst o´ Mc, O, aop) |= SWINV I.

 Lemma join_swinv_prop_rev : forall o M o´ Mc aop O I, joinmem o M o´ ->
                        (substaskst o´ Mc, O, aop) |= SWINV I
                         -> (substaskst o Mc, O, aop) |= SWINV I.

 Lemma join_join_intro´ : forall o M o´ M´ o´´, joinmem o M o´ -> joinmem o´ M´ o´´ -> exists o1, joinmem o M´ o1/\ joinmem o1 M o´´.

Lemma env_join_get: forall x l tp E1 E1´ E E2,
                    EnvMod.join (EnvMod.sig x (l, tp)) E1 E1´ ->
                    EnvMod.join E E1´ E2 ->
                EnvMod.get E2 x = Some (l, tp) .

Lemma ListSet_set_In_cons_elim :
  forall {t:Type} (a b:t) x,
    ListSet.set_In a (b::x) -> a = b \/ ListSet.set_In a x.

Lemma ListSet_set_In_cons_intro :
  forall {t:Type} (a b:t) x,
    a = b \/ ListSet.set_In a x -> ListSet.set_In a (b::x).

Lemma join_eq_dom_env: forall x l tp E1 E1´ dd,
           EnvMod.join (EnvMod.sig x (l, tp)) E1 E1´ ->
          eq_dom_env E1 (getlenvdom dd) ->
          eq_dom_env E1´ ((x,tp)::(getlenvdom dd)).

Lemma join_join_getgenv : forall o o´ M1 M2 G E M isr aux,
                    joinmem o M1 o´ -> joinmem o´ M2 (G,E,M,isr,aux) -> get_genv (get_smem o) = G.

Lemma join_join_getlenv : forall o o´ M1 M2 G E M isr aux,
                    joinmem o M1 o´ -> joinmem o´ M2 (G,E,M,isr,aux) -> get_lenv (get_smem o) = E.

Lemma join_eqenv : forall o M o´, joinmem o M o´ -> eqenv o o´.

Lemma eqenv_trans : forall o o´ o´´, eqenv o o´ -> eqenv o´ o´´ -> eqenv o o´´.

Lemma eqenv_comm: forall o o´, eqenv o o´ -> eqenv o´ o.

Lemma joinmem_eqg : forall o M o´, joinmem o M o´ -> get_genv (get_smem o) = get_genv (get_smem o´).