theory Sep_Tactic_Examples

lemma invoke_cnode_rotate2_wp_old:
  "(dest) \<noteq> (rnd) \<Longrightarrow>
  \<lbrace><dest \<mapsto>c cap1 \<and>* src \<mapsto>c cap2 \<and>*
    rnd \<mapsto>c - \<and>* R>\<rbrace>
     invoke_cnode (RotateCall cap1 cap2 dest src rnd)
  \<lbrace>\<lambda>_. <dest \<mapsto>c NullCap \<and>* src \<mapsto>c cap1 \<and>*
    rnd \<mapsto>c cap2 \<and>* R>\<rbrace>" including no_pre apply (clarsimp simp: invoke_cnode_def) apply (wp) apply (rule hoare_strengthen_post) apply (rule move_cap_wp) apply (sep_solve ) apply (rule hoare_chain) apply (rule move_cap_wp) apply (sep_select_asm 2, sep_select_asm 3) apply (sep_solve) apply (sep_solve) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dest \<noteq> rnd \<Longrightarrow> \<lbrace>cdl.lift (dest \<mapsto>c cap1 \<and>* src \<mapsto>c cap2 \<and>* rnd \<mapsto>c - \<and>* R)\<rbrace> invoke_cnode (RotateCall cap1 cap2 dest src rnd) \<lbrace>\<lambda>_. cdl.lift (dest \<mapsto>c NullCap \<and>* src \<mapsto>c cap1 \<and>* rnd \<mapsto>c cap2 \<and>* R)\<rbrace> proof (prove)
goal (1 subgoal):
 1. dest \<noteq> rnd \<Longrightarrow> \<lbrace>cdl.lift (dest \<mapsto>c cap1 \<and>* src \<mapsto>c cap2 \<and>* rnd \<mapsto>c - \<and>* R)\<rbrace> invoke_cnode (RotateCall cap1 cap2 dest src rnd) \<lbrace>\<lambda>_. cdl.lift (dest \<mapsto>c NullCap \<and>* src \<mapsto>c cap1 \<and>* rnd \<mapsto>c cap2 \<and>* R)\<rbrace> proof (prove)
goal (1 subgoal):
 1. dest \<noteq> rnd \<Longrightarrow> \<lbrace>cdl.lift (dest \<mapsto>c cap1 \<and>* src \<mapsto>c cap2 \<and>* rnd \<mapsto>c - \<and>* R)\<rbrace> liftE (do y <- move_cap cap2 src rnd;
move_cap cap1 dest src
od) \<lbrace>\<lambda>_. cdl.lift (dest \<mapsto>c NullCap \<and>* src \<mapsto>c cap1 \<and>* rnd \<mapsto>c cap2 \<and>* R)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>y. dest \<noteq> rnd \<Longrightarrow> \<lbrace>?B4 y\<rbrace> move_cap cap1 dest src \<lbrace>\<lambda>_. cdl.lift (dest \<mapsto>c NullCap \<and>* src \<mapsto>c cap1 \<and>* rnd \<mapsto>c cap2 \<and>* R)\<rbrace>
 2. dest \<noteq> rnd \<Longrightarrow> \<lbrace>cdl.lift (dest \<mapsto>c cap1 \<and>* src \<mapsto>c cap2 \<and>* rnd \<mapsto>c - \<and>* R)\<rbrace> move_cap cap2 src rnd \<lbrace>?B4\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>y. dest \<noteq> rnd \<Longrightarrow> \<lbrace>?B4 y\<rbrace> move_cap cap1 dest src \<lbrace>?Q5 y\<rbrace>
 2. \<And>y rv s. \<lbrakk>dest \<noteq> rnd; ?Q5 y rv s\<rbrakk> \<Longrightarrow> cdl.lift (dest \<mapsto>c NullCap \<and>* src \<mapsto>c cap1 \<and>* rnd \<mapsto>c cap2 \<and>* R) s
 3. dest \<noteq> rnd \<Longrightarrow> \<lbrace>cdl.lift (dest \<mapsto>c cap1 \<and>* src \<mapsto>c cap2 \<and>* rnd \<mapsto>c - \<and>* R)\<rbrace> move_cap cap2 src rnd \<lbrace>?B4\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>y rv s. \<lbrakk>dest \<noteq> rnd; cdl.lift (src \<mapsto>c cap1 \<and>* dest \<mapsto>c NullCap \<and>* ?R8 y) s\<rbrakk> \<Longrightarrow> cdl.lift (dest \<mapsto>c NullCap \<and>* src \<mapsto>c cap1 \<and>* rnd \<mapsto>c cap2 \<and>* R) s
 2. dest \<noteq> rnd \<Longrightarrow> \<lbrace>cdl.lift (dest \<mapsto>c cap1 \<and>* src \<mapsto>c cap2 \<and>* rnd \<mapsto>c - \<and>* R)\<rbrace> move_cap cap2 src rnd \<lbrace>\<lambda>y. cdl.lift (src \<mapsto>c - \<and>* dest \<mapsto>c ?cap8 y \<and>* ?R8 y)\<rbrace> proof (prove)
goal (1 subgoal):
 1. dest \<noteq> rnd \<Longrightarrow> \<lbrace>cdl.lift (dest \<mapsto>c cap1 \<and>* src \<mapsto>c cap2 \<and>* rnd \<mapsto>c - \<and>* R)\<rbrace> move_cap cap2 src rnd \<lbrace>\<lambda>y. cdl.lift (src \<mapsto>c - \<and>* dest \<mapsto>c ?cap8 y \<and>* rnd \<mapsto>c cap2 \<and>* R)\<rbrace> proof (prove)
goal (3 subgoals):
 1. dest \<noteq> rnd \<Longrightarrow> \<lbrace>?P21\<rbrace> move_cap cap2 src rnd \<lbrace>?Q21\<rbrace>
 2. \<And>s. \<lbrakk>dest \<noteq> rnd; cdl.lift (dest \<mapsto>c cap1 \<and>* src \<mapsto>c cap2 \<and>* rnd \<mapsto>c - \<and>* R) s\<rbrakk> \<Longrightarrow> ?P21 s
 3. \<And>rv s. \<lbrakk>dest \<noteq> rnd; ?Q21 rv s\<rbrakk> \<Longrightarrow> cdl.lift (src \<mapsto>c - \<and>* dest \<mapsto>c ?cap8 rv \<and>* rnd \<mapsto>c cap2 \<and>* R) s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>dest \<noteq> rnd; cdl.lift (dest \<mapsto>c cap1 \<and>* src \<mapsto>c cap2 \<and>* rnd \<mapsto>c - \<and>* R) s\<rbrakk> \<Longrightarrow> cdl.lift (rnd \<mapsto>c - \<and>* src \<mapsto>c ?cap25 \<and>* ?R25) s
 2. \<And>rv s. \<lbrakk>dest \<noteq> rnd; cdl.lift (rnd \<mapsto>c cap2 \<and>* src \<mapsto>c NullCap \<and>* ?R25) s\<rbrakk> \<Longrightarrow> cdl.lift (src \<mapsto>c - \<and>* dest \<mapsto>c ?cap8 rv \<and>* rnd \<mapsto>c cap2 \<and>* R) s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>dest \<noteq> rnd; cdl.lift (rnd \<mapsto>c - \<and>* src \<mapsto>c cap2 \<and>* dest \<mapsto>c cap1 \<and>* R) s\<rbrakk> \<Longrightarrow> cdl.lift (rnd \<mapsto>c - \<and>* src \<mapsto>c ?cap25 \<and>* ?R25) s
 2. \<And>rv s. \<lbrakk>dest \<noteq> rnd; cdl.lift (rnd \<mapsto>c cap2 \<and>* src \<mapsto>c NullCap \<and>* ?R25) s\<rbrakk> \<Longrightarrow> cdl.lift (src \<mapsto>c - \<and>* dest \<mapsto>c ?cap8 rv \<and>* rnd \<mapsto>c cap2 \<and>* R) s proof (prove)
goal (1 subgoal):
 1. \<And>rv s. \<lbrakk>dest \<noteq> rnd; cdl.lift (rnd \<mapsto>c cap2 \<and>* src \<mapsto>c NullCap \<and>* dest \<mapsto>c cap1 \<and>* R) s\<rbrakk> \<Longrightarrow> cdl.lift (src \<mapsto>c - \<and>* dest \<mapsto>c ?cap8 rv \<and>* rnd \<mapsto>c cap2 \<and>* R) s proof (prove)
goal:
No subgoals!