Theory memory_management_inv

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

theory memory_management_inv
  imports memory_manage_sys
begin

section ‹ invariant verification ›


theorem "invariant_presv_pares Γ inv (λk. rgformula.Com (Memory_manage_system_Spec k)) {s0} sys_rely"
  apply(rule invariant_theorem[where G="sys_guar" and pst = UNIV])
    using mem_sys_sat apply fast
    apply(simp add:sys_rely_def PiCore_Hoare.stable_def)
     apply(simp add:sys_guar_def)
    apply(subst stable_equiv)
    apply(rule stable_un_R) apply(rule stable_un_R)
      using tick_guar_stb_inv apply(simp add:stable_def)
      using sched_guar_stb_inv apply(simp add:stable_def)
      apply(rule stable_un_S) apply clarify apply(rule stable_un_R)
        using alloc_guar_stb_inv alloc_free_eq_guar apply(simp add:stable_def)
        using alloc_guar_stb_inv apply(simp add:stable_def)
    using s0_inv apply simp
done

end