theory Sep_Tactic_Examples

lemma move_cap_wp_old:
 "\<lbrace><dest \<mapsto>c - \<and>* src \<mapsto>c cap \<and>* R>\<rbrace>
    move_cap cap' src dest
  \<lbrace>\<lambda>_. <dest \<mapsto>c cap'  \<and>* src \<mapsto>c NullCap \<and>* R>\<rbrace>" including no_pre apply (simp add: move_cap_def) apply (wp swap_parents_wp) apply (rule hoare_strengthen_post) apply (rule set_cap_wp) apply (sep_select 2) apply (sep_solve) apply (rule hoare_chain) apply (rule insert_cap_orphan_wp) apply (sep_solve) apply (sep_solve) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cdl.lift (dest \<mapsto>c - \<and>* src \<mapsto>c cap \<and>* R)\<rbrace> move_cap cap' src dest \<lbrace>\<lambda>_. cdl.lift (dest \<mapsto>c cap' \<and>* src \<mapsto>c NullCap \<and>* R)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>cdl.lift (dest \<mapsto>c - \<and>* src \<mapsto>c cap \<and>* R)\<rbrace> move_cap cap' src dest \<lbrace>\<lambda>_. cdl.lift (dest \<mapsto>c cap' \<and>* src \<mapsto>c NullCap \<and>* R)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>cdl.lift (dest \<mapsto>c - \<and>* src \<mapsto>c cap \<and>* R)\<rbrace> do y <- insert_cap_orphan cap' dest;
y <- set_cap src NullCap;
swap_parents src dest
od \<lbrace>\<lambda>_. cdl.lift (dest \<mapsto>c cap' \<and>* src \<mapsto>c NullCap \<and>* R)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrace>?B y\<rbrace> set_cap src NullCap \<lbrace>\<lambda>ya. cdl.lift (dest \<mapsto>c cap' \<and>* src \<mapsto>c NullCap \<and>* R)\<rbrace>
 2. \<lbrace>cdl.lift (dest \<mapsto>c - \<and>* src \<mapsto>c cap \<and>* R)\<rbrace> insert_cap_orphan cap' dest \<lbrace>?B\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>y. \<lbrace>?B y\<rbrace> set_cap src NullCap \<lbrace>?Q3 y\<rbrace>
 2. \<And>y rv s. ?Q3 y rv s \<Longrightarrow> cdl.lift (dest \<mapsto>c cap' \<and>* src \<mapsto>c NullCap \<and>* R) s
 3. \<lbrace>cdl.lift (dest \<mapsto>c - \<and>* src \<mapsto>c cap \<and>* R)\<rbrace> insert_cap_orphan cap' dest \<lbrace>?B\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>y rv s. cdl.lift (src \<mapsto>c NullCap \<and>* ?R6 y) s \<Longrightarrow> cdl.lift (dest \<mapsto>c cap' \<and>* src \<mapsto>c NullCap \<and>* R) s
 2. \<lbrace>cdl.lift (dest \<mapsto>c - \<and>* src \<mapsto>c cap \<and>* R)\<rbrace> insert_cap_orphan cap' dest \<lbrace>\<lambda>y. cdl.lift (src \<mapsto>c - \<and>* ?R6 y)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>y rv s. cdl.lift (src \<mapsto>c NullCap \<and>* ?R6 y) s \<Longrightarrow> cdl.lift (src \<mapsto>c NullCap \<and>* dest \<mapsto>c cap' \<and>* R) s
 2. \<lbrace>cdl.lift (dest \<mapsto>c - \<and>* src \<mapsto>c cap \<and>* R)\<rbrace> insert_cap_orphan cap' dest \<lbrace>\<lambda>y. cdl.lift (src \<mapsto>c - \<and>* ?R6 y)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>cdl.lift (dest \<mapsto>c - \<and>* src \<mapsto>c cap \<and>* R)\<rbrace> insert_cap_orphan cap' dest \<lbrace>\<lambda>y. cdl.lift (src \<mapsto>c - \<and>* dest \<mapsto>c cap' \<and>* R)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrace>?P10\<rbrace> insert_cap_orphan cap' dest \<lbrace>?Q10\<rbrace>
 2. \<And>s. cdl.lift (dest \<mapsto>c - \<and>* src \<mapsto>c cap \<and>* R) s \<Longrightarrow> ?P10 s
 3. \<And>rv s. ?Q10 rv s \<Longrightarrow> cdl.lift (src \<mapsto>c - \<and>* dest \<mapsto>c cap' \<and>* R) s proof (prove)
goal (2 subgoals):
 1. \<And>s. cdl.lift (dest \<mapsto>c - \<and>* src \<mapsto>c cap \<and>* R) s \<Longrightarrow> cdl.lift (dest \<mapsto>c - \<and>* ?R14) s
 2. \<And>rv s. cdl.lift (dest \<mapsto>c cap' \<and>* ?R14) s \<Longrightarrow> cdl.lift (src \<mapsto>c - \<and>* dest \<mapsto>c cap' \<and>* R) s proof (prove)
goal (1 subgoal):
 1. \<And>rv s. cdl.lift (dest \<mapsto>c cap' \<and>* src \<mapsto>c cap \<and>* R) s \<Longrightarrow> cdl.lift (src \<mapsto>c - \<and>* dest \<mapsto>c cap' \<and>* R) s proof (prove)
goal:
No subgoals!