theory Retype_DP

lemma set_cap_opt_cap_sep_imp:
  assumes asid:
    "\<And>c c'. reset_cap_asid c = reset_cap_asid c' \<Longrightarrow> P (Some c) = P (Some c')"
  shows
    "\<lbrace>\<lambda>s. cdl.lift (ptr \<mapsto>c c \<and>* cref \<mapsto>c - \<and>* sep_true) s \<and> P (Some c)\<rbrace>
    set_cap cref cap
    \<lbrace>\<lambda>rv s. P (opt_cap ptr s)\<rbrace>" apply (rule hoare_name_pre_state) apply (rule hoare_pre) apply (rule hoare_post_imp[OF _ set_cap_wp]) prefer 2 apply clarsimp apply sep_solve apply clarsimp apply (sep_select_asm 2) apply (drule opt_cap_sep_imp)+ apply (clarsimp dest!: asid) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cdl.lift (ptr \<mapsto>c c \<and>* cref \<mapsto>c - \<and>* (\<lambda>s. True)) s \<and> P (Some c)\<rbrace> set_cap cref cap \<lbrace>\<lambda>rv s. P (opt_cap ptr s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. cdl.lift (ptr \<mapsto>c c \<and>* cref \<mapsto>c - \<and>* (\<lambda>s. True)) s \<and> P (Some c) \<Longrightarrow> \<lbrace>(=) s\<rbrace> set_cap cref cap \<lbrace>\<lambda>rv s. P (opt_cap ptr s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. cdl.lift (ptr \<mapsto>c c \<and>* cref \<mapsto>c - \<and>* (\<lambda>s. True)) s \<and> P (Some c) \<Longrightarrow> \<lbrace>?Q2 s\<rbrace> set_cap cref cap \<lbrace>\<lambda>rv s. P (opt_cap ptr s)\<rbrace>
 2. \<And>s sa. \<lbrakk>cdl.lift (ptr \<mapsto>c c \<and>* cref \<mapsto>c - \<and>* (\<lambda>s. True)) s \<and> P (Some c); s = sa\<rbrakk> \<Longrightarrow> ?Q2 s sa proof (prove)
goal (2 subgoals):
 1. \<And>s rv sa. \<lbrakk>cdl.lift (ptr \<mapsto>c c \<and>* cref \<mapsto>c - \<and>* (\<lambda>s. True)) s \<and> P (Some c); cdl.lift (cref \<mapsto>c cap \<and>* ?R6 s) sa\<rbrakk> \<Longrightarrow> P (opt_cap ptr sa)
 2. \<And>s sa. \<lbrakk>cdl.lift (ptr \<mapsto>c c \<and>* cref \<mapsto>c - \<and>* (\<lambda>s. True)) s \<and> P (Some c); s = sa\<rbrakk> \<Longrightarrow> cdl.lift (cref \<mapsto>c - \<and>* ?R6 s) sa proof (prove)
goal (2 subgoals):
 1. \<And>s sa. \<lbrakk>cdl.lift (ptr \<mapsto>c c \<and>* cref \<mapsto>c - \<and>* (\<lambda>s. True)) s \<and> P (Some c); s = sa\<rbrakk> \<Longrightarrow> cdl.lift (cref \<mapsto>c - \<and>* ?R6 s) sa
 2. \<And>s rv sa. \<lbrakk>cdl.lift (ptr \<mapsto>c c \<and>* cref \<mapsto>c - \<and>* (\<lambda>s. True)) s \<and> P (Some c); cdl.lift (cref \<mapsto>c cap \<and>* ?R6 s) sa\<rbrakk> \<Longrightarrow> P (opt_cap ptr sa) proof (prove)
goal (2 subgoals):
 1. \<And>sa. \<lbrakk>cdl.lift (ptr \<mapsto>c c \<and>* cref \<mapsto>c - \<and>* (\<lambda>s. True)) sa; P (Some c)\<rbrakk> \<Longrightarrow> cdl.lift (cref \<mapsto>c - \<and>* ?R6 sa) sa
 2. \<And>s rv sa. \<lbrakk>cdl.lift (ptr \<mapsto>c c \<and>* cref \<mapsto>c - \<and>* (\<lambda>s. True)) s \<and> P (Some c); cdl.lift (cref \<mapsto>c cap \<and>* ?R6 s) sa\<rbrakk> \<Longrightarrow> P (opt_cap ptr sa) proof (prove)
goal (1 subgoal):
 1. \<And>s rv sa. \<lbrakk>cdl.lift (ptr \<mapsto>c c \<and>* cref \<mapsto>c - \<and>* (\<lambda>s. True)) s \<and> P (Some c); cdl.lift (cref \<mapsto>c cap \<and>* ptr \<mapsto>c c \<and>* (\<lambda>s. True)) sa\<rbrakk> \<Longrightarrow> P (opt_cap ptr sa) proof (prove)
goal (1 subgoal):
 1. \<And>s sa. \<lbrakk>cdl.lift (cref \<mapsto>c cap \<and>* ptr \<mapsto>c c \<and>* (\<lambda>s. True)) sa; cdl.lift (ptr \<mapsto>c c \<and>* cref \<mapsto>c - \<and>* (\<lambda>s. True)) s; P (Some c)\<rbrakk> \<Longrightarrow> P (opt_cap ptr sa) proof (prove)
goal (1 subgoal):
 1. \<And>s sa. \<lbrakk>cdl.lift (ptr \<mapsto>c c \<and>* cref \<mapsto>c - \<and>* (\<lambda>s. True)) s; P (Some c); cdl.lift (ptr \<mapsto>c c \<and>* cref \<mapsto>c cap \<and>* (\<lambda>s. True)) sa\<rbrakk> \<Longrightarrow> P (opt_cap ptr sa) proof (prove)
goal (1 subgoal):
 1. \<And>s sa. \<lbrakk>P (Some c); \<exists>cap'. opt_cap ptr s = Some cap' \<and> reset_cap_asid cap' = reset_cap_asid c; \<exists>cap'. opt_cap ptr sa = Some cap' \<and> reset_cap_asid cap' = reset_cap_asid c\<rbrakk> \<Longrightarrow> P (opt_cap ptr sa) proof (prove)
goal:
No subgoals!