Theory rg_cond

(*
Created by Yongwang Zhao (zhaoyw@buaa.edu.cn)
School of Computer Science & Engineering, Beihang University, China
*)

theory rg_cond
imports mem_spec invariant (*"../picore-lib/picore_lemma"*)
begin

section ‹Rely-guarantee condition of events›

subsection ‹defs of rely-guarantee conditions›
definition lvars_nochange :: "Thread ⇒ State ⇒ State ⇒ bool"
where "lvars_nochange t r s ≡
    i r t = i s t ∧ j r t = j s t ∧ ret r t = ret s t
    ∧ endt r t = endt s t ∧ rf r t = rf s t ∧ tmout r t = tmout s t
    ∧ lsizes r t = lsizes s t ∧ alloc_l r t = alloc_l s t ∧ free_l r t = free_l s t
    ∧ from_l r t = from_l s t ∧ blk r t = blk s t ∧ nodev r t = nodev s t
    ∧ bn r t = bn s t ∧ lbn r t = lbn s t ∧ lsz r t = lsz s t ∧ block2 r t = block2 s t
    ∧ free_block_r r t = free_block_r s t ∧ alloc_lsize_r r t = alloc_lsize_r s t ∧ lvl r t = lvl s t ∧ bb r t = bb s t
    ∧ block_pt r t = block_pt s t ∧ th r t = th s t ∧ need_resched r t = need_resched s t
    ∧ mempoolalloc_ret r t = mempoolalloc_ret s t
    ∧ freeing_node r t = freeing_node s t ∧ allocating_node r t = allocating_node s t"

definition lvars_nochange_rel :: "Thread ⇒ (State × State) set"
where "lvars_nochange_rel t ≡ {(s,r). lvars_nochange t s r}"

definition lvars_nochange_4all :: "(State × State) set"
where "lvars_nochange_4all ≡ {(s,r). ∀t. lvars_nochange t s r}"

definition lvars_nochange1 :: "Thread ⇒ State ⇒ State ⇒ bool"
where "lvars_nochange1 t r s ≡ freeing_node r t = freeing_node s t ∧ allocating_node r t = allocating_node s t"

definition lvars_nochange1_rel :: "Thread ⇒ (State × State) set"
where "lvars_nochange1_rel t ≡ {(s,r). lvars_nochange1 t s r}"

definition lvars_nochange1_4all :: "(State × State) set"
where "lvars_nochange1_4all ≡ {(s,r). ∀t. lvars_nochange1 t s r}"

lemma lvars_nochange_trans:
"lvars_nochange t x y ⟹ lvars_nochange t y z ⟹ lvars_nochange t x z"
apply(simp add:lvars_nochange_def)
done

lemma lvars_nochange_sym:
"lvars_nochange t x y ⟹ lvars_nochange t y x"
apply(simp add:lvars_nochange_def)
done

lemma lvars_nochange_refl:
"lvars_nochange t x x"
apply(simp add:lvars_nochange_def)
done

lemma lvars_nc_nc1: "lvars_nochange t r s ⟹ lvars_nochange1 t r s"
  unfolding lvars_nochange_def lvars_nochange1_def by simp

lemma lv_noch_all1: "(s,r)∈lvars_nochange_4all
      ⟹ (s,r)∈lvars_nochange_rel t ∧ (∀t'. t' ≠ t ⟶ (s,r)∈lvars_nochange_rel t')"
  unfolding lvars_nochange_4all_def lvars_nochange_rel_def by auto

lemma lv_noch_all2: "(s,r)∈lvars_nochange_rel t ∧ (∀t'. t' ≠ t ⟶ lvars_nochange t' s r)
        ⟹ (s,r)∈lvars_nochange_4all"
  unfolding lvars_nochange_4all_def lvars_nochange_rel_def by auto

definition gvars_nochange :: "State ⇒ State ⇒ bool"
where "gvars_nochange s r ≡ cur r = cur s ∧ tick r = tick s ∧ thd_state r = thd_state s
                          ∧ mem_pools r = mem_pools s ∧ mem_pool_info r = mem_pool_info s"

definition gvars_nochange_rel :: "(State × State) set"
where "gvars_nochange_rel ≡ {(s,r). gvars_nochange s r}"

definition gvars_conf :: "State ⇒ State ⇒ bool"
where "gvars_conf s r ≡
  mem_pools r = mem_pools s
    ∧ (∀p. buf (mem_pool_info s p) = buf (mem_pool_info r p)
          ∧ max_sz (mem_pool_info s p) = max_sz (mem_pool_info r p)
          ∧ n_max (mem_pool_info s p) = n_max (mem_pool_info r p)
          ∧ n_levels (mem_pool_info s p) = n_levels (mem_pool_info r p)
          ∧ length (levels (mem_pool_info s p)) = length (levels (mem_pool_info r p))
          ∧ (∀i. length (bits (levels (mem_pool_info s p) ! i))
                   = length (bits (levels (mem_pool_info r p) ! i))) )"

definition gvars_conf_stable :: "(State × State) set"
where "gvars_conf_stable ≡ {(s,r). gvars_conf s r}"

definition inv_sta_rely :: "(State × State) set"
where "inv_sta_rely ≡ {(s,r). inv s ⟶ inv r}"

definition inv_sta_guar :: "(State × State) set"
where "inv_sta_guar ≡ {(s,r). inv s ⟶ inv r}"


lemma glnochange_inv0:
  "(a, b) ∈ lvars_nochange1_4all ⟹ cur a = cur b ⟹
     thd_state a = thd_state b ⟹ mem_pools a = mem_pools b ⟹
     mem_pool_info a = mem_pool_info b ⟹ inv a ⟹ inv b"
  apply(simp add:lvars_nochange1_4all_def lvars_nochange1_def inv_def)
  apply(rule conjI) apply(simp add:inv_cur_def)
    apply(rule conjI) apply(simp add:inv_thd_waitq_def) apply auto[1]
    apply(rule conjI) apply(simp add:inv_mempool_info_def)
    apply(rule conjI) apply(simp add:inv_bitmap_freelist_def)
    apply(rule conjI) apply(simp add:inv_bitmap_def)
    apply(rule conjI) apply(simp add: inv_aux_vars_def mem_block_addr_valid_def)
    apply(rule conjI) apply(simp add:inv_bitmap0_def)
    apply(rule conjI) apply(simp add:inv_bitmapn_def)
    apply(simp add:inv_bitmap_not4free_def)
done

lemma glnochange_inv1:
  "(a, b) ∈ lvars_nochange_4all ⟹ cur a = cur b ⟹
     thd_state a = thd_state b ⟹ mem_pools a = mem_pools b ⟹
     mem_pool_info a = mem_pool_info b ⟹ inv a ⟹ inv b"
  apply(simp add:lvars_nochange_4all_def lvars_nochange_def)
  using glnochange_inv0
  apply(simp add:lvars_nochange1_4all_def lvars_nochange1_def)
  by metis

lemma glnochange_inv:
  "inv a ⟹ ∀t'. t' ≠ t1 ⟶ lvars_nochange t' a b
      ⟹ gvars_nochange a b ⟹ lvars_nochange t1 a b ⟹ inv b"
  apply(subgoal_tac "(a, b) ∈ lvars_nochange_4all")
    apply(simp add: gvars_nochange_def)
    using glnochange_inv1 apply auto
  using lv_noch_all2[of a b t1] apply auto[1]
  by(simp add: lvars_nochange_rel_def)

definition Schedule_rely :: "(State × State) set"
where "Schedule_rely ≡ {(s,r). inv s ⟶ inv r} ∪ Id"

definition Schedule_guar :: "(State × State) set"
where "Schedule_guar ≡
  (⌦‹(*⦃(ºcur ≠ Some t ⟶
          (ºcur ≠ None ⟶ ªthd_state = (ºthd_state (the (ºcur) := READY))(t := RUNNING) ∧ ªcur = Some t)
        ∧ (ºcur = None ⟶ ªthd_state = ºthd_state (t := RUNNING)) ∧ ªcur = Some t)
    ∧ (ºcur = Some t ⟶ ªthd_state = ºthd_state ∧ ºcur = ªcur) ⦄*)›
   {(s,r). inv s ⟶ inv r}
   ∩ ⦃ºtick = ªtick ∧ ºmem_pools = ªmem_pools ∧ ºmem_pool_info = ªmem_pool_info⦄
   ∩ (⋂t. lvars_nochange_rel t)) ∪ Id"

definition
  "Schedule_RGCond t ≡ ⦇ PiCore_Validity.rgformula.Com = Schedule t, Pre = {s. inv s}, Rely = Schedule_rely, Guar = Schedule_guar, Post = {s. inv s} ⦈"

definition Tick_rely :: "(State × State) set"
where "Tick_rely ≡ ⦃ºtick = ªtick⦄ ∪ Id"

definition Tick_guar :: "(State × State) set"
where "Tick_guar ≡ (⦃ªtick = ºtick + 1 ∧ ºcur = ªcur ∧ ºthd_state = ªthd_state
                      ∧ ºmem_pools = ªmem_pools ∧ ºmem_pool_info = ªmem_pool_info⦄
                      ∩ (⋂t. lvars_nochange_rel t)) ∪ Id"

definition Tick_RGCond
  where "Tick_RGCond ≡ ⦇ PiCore_Validity.rgformula.Com = Tick,
          Pre = ⦃True⦄, Rely = Tick_rely, Guar = Tick_guar, Post = ⦃True⦄ ⦈"

abbreviation alloc_blk_valid :: "State ⇒ mempool_ref ⇒ nat ⇒ nat ⇒ mem_ref ⇒ bool"
where "alloc_blk_valid s p lv bnum blkaddr
        ≡ (blkaddr = buf (mem_pool_info s p) + bnum * ((max_sz (mem_pool_info s p)) div (4 ^ lv))
            ∧ bnum < n_max (mem_pool_info s p) * (4 ^ lv))"

abbreviation alloc_memblk_data_valid :: "State ⇒ mempool_ref ⇒ Mem_block ⇒ bool"
where "alloc_memblk_data_valid s p mb ≡ alloc_blk_valid s p (level mb) (block mb) (data mb)"

definition alloc_memblk_valid :: "State ⇒ mempool_ref ⇒ nat ⇒ Mem_block ⇒ bool"
where "alloc_memblk_valid s p sz mb ≡
        p = pool mb ∧ p ∈ mem_pools s
         ∧ sz ≤ (max_sz (mem_pool_info s p)) div (4 ^ (level mb)) ⌦‹(* block size of level mb + 1 < sz ≤ block size of level mb *)›
         ∧ (level mb < n_levels (mem_pool_info s p) - 1 ⟶ sz > (max_sz (mem_pool_info s p)) div (4 ^ (level mb + 1)))
         ∧ alloc_memblk_data_valid s p mb" (* (data mb = buf (mem_pool_info s p) + (block mb) * ((max_sz (mem_pool_info s p)) div (4 ^ (level mb))))" *)
         (* mem ref of allocated block should be the address of block id in the level *)
         (*∧ (bits (levels (mem_pool_info s p) ! (level mb))) ! (block mb) = ALLOCATED"*)
          (* flag bit should be ALLOCATED, we remove the condition since
            other threads may free the block after allocating and before service returning *)

abbreviation Mem_pool_alloc_pre :: "Thread ⇒ State set"
where "Mem_pool_alloc_pre t ≡ {s. inv s ∧ allocating_node s t = None ∧ freeing_node s t = None}"

definition Mem_pool_alloc_rely :: "Thread ⇒ (State × State) set"
where "Mem_pool_alloc_rely t ≡
   ((lvars_nochange_rel t ∩ gvars_conf_stable
    ∩ {(s,r). inv s ⟶ inv r}
    ∩ {(s,r).(cur s = Some t ⟶ mem_pool_info s = mem_pool_info r
                  ∧ (∀t'. t' ≠ t ⟶ lvars_nochange t' s r))}) ∪ Id)"

definition Mem_pool_alloc_guar :: "Thread ⇒ (State × State) set"
where "Mem_pool_alloc_guar t ≡
        ((gvars_conf_stable ∩
          {(s,r). (cur s ≠ Some t ⟶ gvars_nochange s r ∧ lvars_nochange t s r)
                  ∧ (cur s = Some t ⟶ inv s ⟶ inv r)
                  ∧ (∀t'. t' ≠ t ⟶ lvars_nochange t' s r) }
          ∩ ⦃ºtick = ªtick⦄) ∪ Id)"

definition Mem_pool_alloc_post :: "Thread ⇒ mempool_ref ⇒ nat ⇒ int ⇒ State set"
where "Mem_pool_alloc_post t p sz timeout ≡
  {s. inv s ∧ allocating_node s t = None ∧ freeing_node s t = None
      ∧ (timeout = FOREVER ⟶ (ret s t = ESIZEERR ∧ mempoolalloc_ret s t = None
                              ∨ ret s t = OK ∧ (∃mblk. mempoolalloc_ret s t = Some mblk ∧ alloc_memblk_valid s p sz mblk)))
      ∧ (timeout = NOWAIT ⟶ ((ret s t = ENOMEM ∨ ret s t = ESIZEERR) ∧ mempoolalloc_ret s t = None)
                              ∨ (ret s t = OK ∧ (∃mblk. mempoolalloc_ret s t = Some mblk ∧ alloc_memblk_valid s p sz mblk)))
      ∧ (timeout > 0 ⟶ ((ret s t = ETIMEOUT ∨ ret s t = ESIZEERR) ∧ mempoolalloc_ret s t = None)
                         ∨ (ret s t = OK ∧ (∃mblk. mempoolalloc_ret s t = Some mblk ∧ alloc_memblk_valid s p sz mblk)))}"

definition Mem_pool_alloc_RGCond
  where "Mem_pool_alloc_RGCond t p sz timeout ≡
⦇ PiCore_Validity.rgformula.Com = Mem_pool_alloc t p sz timeout,
          Pre = Mem_pool_alloc_pre t,
              Rely = Mem_pool_alloc_rely t,
              Guar = Mem_pool_alloc_guar t,
              Post = Mem_pool_alloc_post t p sz timeout ⦈"

abbreviation Mem_pool_free_pre :: "Thread ⇒ State set"
where "Mem_pool_free_pre t ≡ {s. inv s ∧ allocating_node s t = None ∧ freeing_node s t = None}"

definition Mem_pool_free_rely :: "Thread ⇒ (State × State) set"
where "Mem_pool_free_rely t ≡
   ((lvars_nochange_rel t ∩ gvars_conf_stable
    ∩ {(s,r). inv s ⟶ inv r}
    ∩ {(s,r).(cur s = Some t ⟶ mem_pool_info s = mem_pool_info r
                  ∧ (∀t'. t' ≠ t ⟶ lvars_nochange t' s r))}) ∪ Id)"

definition Mem_pool_free_guar :: "Thread ⇒ (State × State) set"
where "Mem_pool_free_guar t ≡
        ((gvars_conf_stable ∩
          {(s,r). (cur s ≠ Some t ⟶ gvars_nochange s r ∧ lvars_nochange t s r)
                  ∧ (cur s = Some t ⟶ inv s ⟶ inv r)
                  ∧ (∀t'. t' ≠ t ⟶ lvars_nochange t' s r) }
          ∩ ⦃ºtick = ªtick⦄) ∪ Id)"

definition Mem_pool_free_post :: "Thread ⇒ State set"
where "Mem_pool_free_post t ≡ {s. inv s ∧ allocating_node s t = None ∧ freeing_node s t = None}"


definition Mem_pool_free_RGCond
  where "Mem_pool_free_RGCond t b ≡
          ⦇ PiCore_Validity.rgformula.Com = Mem_pool_free t b,
              Pre = Mem_pool_free_pre t,
              Rely = Mem_pool_free_rely t,
              Guar = Mem_pool_free_guar t,
              Post = Mem_pool_free_post t ⦈"

subsection ‹stability, subset relations of rely-guarantee conditions›

lemma stable_inv_free_rely:
  "(s,r)∈Mem_pool_free_rely t ⟹ inv s ⟹ inv r"
  apply (simp add:Mem_pool_free_rely_def)
  apply(case_tac "cur s = Some t") apply simp
    apply(subgoal_tac "(s, r) ∈ lvars_nochange_4all")
      apply(simp add:lvars_nochange_4all_def lvars_nochange_def)
      apply(simp add:inv_def) unfolding gvars_conf_stable_def gvars_conf_def
      apply(rule conjI) apply(simp add:inv_cur_def) apply auto[1] apply metis
        apply(simp add:lvars_nochange_4all_def lvars_nochange_rel_def)
        apply auto[1] apply(simp add:lvars_nochange_def)
        apply auto
done

lemma stable_inv_free_rely1: "stable ⦃´inv⦄ (Mem_pool_free_rely t)"
  using stable_inv_free_rely unfolding stable_def by auto

lemma stable_inv_alloc_rely:
  "(s,r)∈Mem_pool_alloc_rely t ⟹ inv s ⟹ inv r"
  apply(subgoal_tac "Mem_pool_alloc_rely t = Mem_pool_free_rely t")
  using stable_inv_free_rely apply simp
  by (simp add:Mem_pool_alloc_rely_def Mem_pool_free_rely_def)

lemma stable_inv_alloc_rely1: "stable ⦃´inv⦄ (Mem_pool_alloc_rely t)"
  using stable_inv_alloc_rely unfolding stable_def by auto

lemma stable_inv_sched_rely:
  "(s,r)∈Schedule_rely ⟹ inv s ⟹ inv r"
  apply (simp add:Schedule_rely_def) by auto

lemma stable_inv_sched_rely1: "stable ⦃´inv⦄ Schedule_rely"
  using stable_inv_sched_rely unfolding stable_def by auto

lemma free_guar_stb_inv: "stable ⦃´inv⦄ (Mem_pool_free_guar t)"
proof -
{
  fix x
  assume a0: "inv x"
  {
    fix y
    assume b0: "(x,y)∈Mem_pool_free_guar t"
    hence "(x,y)∈ {(s,r). (cur s ≠ Some t ⟶ gvars_nochange s r ∧ lvars_nochange t s r)
                  ∧ (cur s = Some t ⟶ inv s ⟶ inv r)
                  ∧ (∀t'. t' ≠ t ⟶ lvars_nochange t' s r)}"
      unfolding Mem_pool_free_guar_def gvars_nochange_def lvars_nochange_def by auto
    hence "(cur x ≠ Some t ⟶ gvars_nochange x y ∧ lvars_nochange t x y)
            ∧ (cur x = Some t ⟶ inv x ⟶ inv y)
            ∧ (∀t'. t' ≠ t ⟶ lvars_nochange t' x y)" by simp
    hence "inv y"
      apply(case_tac "cur x ≠ Some t")
        apply (simp add: gvars_nochange_def lvars_nochange_def) using a0 apply clarify
        apply(simp add:inv_def)
        apply(rule conjI) apply(simp add:inv_cur_def)
        apply(rule conjI) apply(simp add:inv_thd_waitq_def) apply metis
        apply(rule conjI) apply(simp add:inv_mempool_info_def)
        apply(rule conjI) using inv_bitmap_freelist_def apply metis
        apply(rule conjI) apply(simp add:inv_bitmap_def)
        apply(rule conjI) apply(simp add:inv_aux_vars_def)
          apply(rule conjI) apply metis
          apply(rule conjI) apply(simp add:mem_block_addr_valid_def) apply metis
          apply(rule conjI) apply metis
          apply(rule conjI) apply(simp add:mem_block_addr_valid_def) apply metis
          apply(rule conjI) apply metis
          apply(rule conjI) apply metis
          apply metis
        apply(rule conjI) apply(simp add:inv_bitmap0_def)
        apply(rule conjI) apply(simp add:inv_bitmapn_def)
        apply(simp add:inv_bitmap_not4free_def)
      using a0 by auto
  }
}
then show ?thesis by (simp add:stable_def)
qed

lemma alloc_guar_stb_inv: "stable ⦃´inv⦄ (Mem_pool_alloc_guar t)"
  apply(subgoal_tac "Mem_pool_alloc_guar t = Mem_pool_free_guar t")
  using free_guar_stb_inv apply simp
  by (simp add:Mem_pool_alloc_guar_def Mem_pool_free_guar_def)

lemma sched_guar_stb_inv:
  "(s,r)∈Schedule_guar ⟹ inv s ⟹ inv r"
  apply(simp add:Schedule_guar_def)
  apply(erule disjE) by auto

lemma tick_guar_stb_inv:
  "(s,r)∈Tick_guar ⟹ inv s ⟹ inv r"
  apply(simp add:Tick_guar_def) apply(erule disjE)
    using glnochange_inv0 lvars_nc_nc1
    unfolding lvars_nochange1_4all_def lvars_nochange_rel_def apply auto[1] apply blast
  by auto

lemma stable_equiv: ‹PiCore_Hoare.stable = RG_Hoare.stable›
  by (unfold PiCore_Hoare.stable_def RG_Hoare.stable_def) auto

lemma mem_pool_alloc_pre_stb: "stable (Mem_pool_alloc_pre t) (Mem_pool_alloc_rely t)"
  apply(rule subst[where t="⦃´inv ∧ ´allocating_node t = None ∧ ´freeing_node t = None⦄"
        and s="⦃´inv⦄ ∩ ⦃´allocating_node t = None ∧ ´freeing_node t = None⦄"])
    apply auto[1]
  apply(rule stable_int2) apply (simp add: stable_inv_alloc_rely1)
  apply(simp add:stable_def Mem_pool_alloc_rely_def gvars_conf_stable_def lvars_nochange_rel_def lvars_nochange_def)
done

lemma mp_alloc_post_stb: "stable (Mem_pool_alloc_post t p sz timeout) (Mem_pool_alloc_rely t)"
  apply(simp add:stable_def) apply(rule allI) apply(rule impI) apply(rule allI) apply(rule impI)
  apply(simp add:Mem_pool_alloc_rely_def Mem_pool_alloc_post_def)
  apply(rule conjI)
    apply(simp add:gvars_conf_stable_def) unfolding gvars_conf_def apply metis
    apply(simp add:lvars_nochange_rel_def lvars_nochange_def)
    apply(case_tac "x = y")
      apply simp apply clarify
      apply(simp add:alloc_memblk_valid_def gvars_conf_def gvars_conf_stable_def)
done

lemma mem_pool_free_pre_stb: "stable (Mem_pool_free_pre t) (Mem_pool_free_rely t)"
  apply(rule subst[where t="⦃´inv ∧ ´allocating_node t = None ∧ ´freeing_node t = None⦄"
        and s="⦃´inv⦄ ∩ ⦃´allocating_node t = None ∧ ´freeing_node t = None⦄"])
    apply auto[1]
  apply(rule stable_int2) apply (simp add: stable_inv_free_rely1)
  apply(simp add:stable_def Mem_pool_free_rely_def gvars_conf_stable_def lvars_nochange_rel_def lvars_nochange_def)

done

lemma mem_pool_free_post_stb: "stable (Mem_pool_free_post t) (Mem_pool_free_rely t)"
  using mem_pool_free_pre_stb apply(simp add:Mem_pool_free_post_def)
done

lemma allocguar_in_allocrely: "t1 ≠ t2 ⟹ Mem_pool_alloc_guar t1 ⊆ Mem_pool_alloc_rely t2"
  apply clarify
  proof -
    fix a b
    assume p0: "t1 ≠ t2"
      and  p1: "(a, b) ∈ Mem_pool_alloc_guar t1"
    hence p2: "(a, b) ∈ gvars_conf_stable
                  ∧ (cur a ≠ Some t1 ⟶ gvars_nochange a b ∧ lvars_nochange t1 a b)
                  ∧ (cur a = Some t1 ⟶ inv a ⟶ inv b)
                  ∧ (∀t'. t' ≠ t1 ⟶ lvars_nochange t' a b)
                  ∧ tick a = tick b ∨ a = b"
      unfolding Mem_pool_alloc_guar_def by auto

    from p0 p2 have
      "(a, b) ∈ lvars_nochange_rel t2 ∧ (a, b) ∈ gvars_conf_stable
        ∧ (inv a ⟶ inv b)
        ∧ (cur a = Some t2 ⟶  mem_pool_info a = mem_pool_info b
                ∧ (∀t'. t' ≠ t2 ⟶ lvars_nochange t' a b))
        ∨ a = b"
      apply clarify
      apply(rule conjI) apply(simp add:lvars_nochange_rel_def)
      apply(rule conjI) apply simp
      apply(rule conjI) apply clarify using glnochange_inv apply auto[1]
      apply clarify
      apply(rule conjI) apply(simp add:gvars_nochange_def)
      by auto

    thus "(a, b) ∈ Mem_pool_alloc_rely t2" unfolding Mem_pool_alloc_rely_def by simp
  qed

lemma schedguar_in_allocrely: "Schedule_guar ⊆ Mem_pool_alloc_rely t2"
apply clarify
proof -
  fix a b
  assume p0: "(a, b) ∈ Schedule_guar"
  hence p1: "(inv a ⟶ inv b) ∧ tick a = tick b ∧ mem_pools a = mem_pools b ∧ mem_pool_info a = mem_pool_info b
            ∧ (a,b)∈(⋂t. lvars_nochange_rel t) ∨ a = b"
    by(simp add:Schedule_guar_def)

  hence "(a, b) ∈ lvars_nochange_rel t2 ∧ (a, b) ∈ gvars_conf_stable
        ∧ (inv a ⟶ inv b)
        ∧ (cur a = Some t2 ⟶  mem_pool_info a = mem_pool_info b
                ∧ (∀t'. t' ≠ t2 ⟶ lvars_nochange t' a b))
        ∨ a = b"
      apply clarify
      apply(rule conjI) apply(simp add:lvars_nochange_rel_def)
      apply(rule conjI) apply(simp add:gvars_conf_stable_def gvars_conf_def)
      apply(rule conjI) apply clarify apply clarify
      by(simp add:lvars_nochange_rel_def)

  thus "(a, b) ∈ Mem_pool_alloc_rely t2" by(simp add:Mem_pool_alloc_rely_def)
qed

lemma schedguar_in_tickrely: "Schedule_guar ⊆ Tick_rely"
  apply(simp add:Schedule_guar_def Tick_rely_def)
  by auto

lemma allocguar_in_tickrely: "Mem_pool_alloc_guar t ⊆ Tick_rely"
  apply(simp add:Mem_pool_alloc_guar_def Tick_rely_def)
  by auto

lemma tickguar_in_allocrely: "Tick_guar ⊆ Mem_pool_alloc_rely t"
  apply clarify
  proof -
  fix a b
  assume p0: "(a, b) ∈ Tick_guar"
  hence p1: "tick b = tick a + 1 ∧ cur a = cur b ∧ thd_state a = thd_state b
            ∧ mem_pools a = mem_pools b ∧ mem_pool_info a = mem_pool_info b
            ∧ (a,b)∈(⋂t. lvars_nochange_rel t) ∨ a = b"
    by(simp add:Tick_guar_def)

  hence "(a, b) ∈ lvars_nochange_rel t ∧ (a, b) ∈ gvars_conf_stable
        ∧ (inv a ⟶ inv b)
        ∧ (cur a = Some t ⟶  mem_pool_info a = mem_pool_info b
                ∧ (∀t'. t' ≠ t ⟶ lvars_nochange t' a b))
        ∨ a = b"
      apply clarify
      apply(rule conjI) apply(simp add:lvars_nochange_rel_def)
      apply(rule conjI) apply(simp add:gvars_conf_stable_def gvars_conf_def)
      apply(rule conjI) using glnochange_inv0 lvars_nc_nc1 unfolding lvars_nochange_rel_def lvars_nochange1_4all_def
        apply auto[1] apply blast
      by auto

  thus "(a, b) ∈ Mem_pool_alloc_rely t" by(simp add:Mem_pool_alloc_rely_def)
qed

lemma allocguar_in_schedrely: "Mem_pool_alloc_guar t ⊆ Schedule_rely"
  apply(simp add:Mem_pool_alloc_guar_def Schedule_rely_def)
  apply clarify
  apply(case_tac "cur a = Some t")
    apply simp
    apply clarify
    using glnochange_inv by auto

lemma tickguar_in_schedrely: "Tick_guar ⊆ Schedule_rely"
  apply clarify
  proof -
    fix a b
    assume p0: "(a, b) ∈ Tick_guar"
    thus "(a, b) ∈ Schedule_rely"
      apply(simp add:Tick_guar_def Schedule_rely_def) apply auto
      using glnochange_inv1 by(simp add:lvars_nochange_4all_def lvars_nochange_rel_def)
  qed


end