theory EquivValidTutorial

lemma pitfall2_using_bind_ev2:
  "\<lbrace>|\<top>\<top>|, (\<lambda>s. desk s = c)\<rbrace>
     do
       s \<leftarrow> get;
       return (desk s)
     od
   \<lbrace>|\<top>\<top>|\<rbrace>"
  \<comment> \<open> First we need to peel it back to \<open>equiv_valid_2\<close> form, so we can apply its bind rule. \<close> apply(clarsimp simp:equiv_valid_def2) apply(rule equiv_valid_2_bind_pre)
       \<comment> \<open> Here \<open>wp\<close> infers correctly that the equivalence between the
          intermediate return values needs to be \<open>\<lambda>rv rv'. desk rv = desk rv'\<close>,
          i.e. that \<open>desk\<close> has the same value in the state returned by \<open>get\<close> in both runs. \<close> apply(wp add:return_ev2) apply(clarsimp simp:equiv_valid_def spec_equiv_valid_def equiv_valid_2_def)
      \<comment> \<open> The \<open>force\<close> tactic just guesses \<open>False\<close> for the postcondition for both steps. \<close> apply(force simp add:get_def)
     \<comment> \<open> As these next two goals are Hoare triples, we use the \<open>wp\<close> tool, as usual for
         Hoare triples in the seL4 proof base. See Lib.WPTutorial for more information. \<close> apply wp apply wp
   \<comment> \<open> Now we are stuck because \<open>force\<close> guessed \<open>False\<close> as a premise
      to discharge the goal earlier, giving us an unsatisfiable goal here. \<close> oops

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (\<lambda>_ _. True) (\<lambda>_ _. True) (\<lambda>s. desk s = c) (do s <- get;
return (desk s)
od) proof (prove)
goal (1 subgoal):
 1. equiv_valid_rv_inv (\<lambda>_ _. True) (\<lambda>_ _. True) (=) (\<lambda>s. desk s = c) (do s <- get;
return (desk s)
od) proof (prove)
goal (6 subgoals):
 1. \<And>rv rv'. ?R' rv rv' \<Longrightarrow> equiv_valid_2 (\<lambda>_ _. True) (\<lambda>_ _. True) (\<lambda>_ _. True) (=) (?Q rv) (?Q' rv') (return (desk rv)) (return (desk rv'))
 2. equiv_valid_2 (\<lambda>_ _. True) (\<lambda>_ _. True) (\<lambda>_ _. True) ?R' ?P ?P' get get
 3. \<lbrace>?S\<rbrace> get \<lbrace>?Q\<rbrace>
 4. \<lbrace>?S'\<rbrace> get \<lbrace>?Q'\<rbrace>
 5. \<And>s. desk s = c \<Longrightarrow> ?P s \<and> ?S s
 6. \<And>s. desk s = c \<Longrightarrow> ?P' s \<and> ?S' s proof (prove)
goal (5 subgoals):
 1. equiv_valid_2 (\<lambda>_ _. True) (\<lambda>_ _. True) (\<lambda>_ _. True) (\<lambda>rv rv'. desk rv = desk rv') ?P ?P' get get
 2. \<lbrace>?S\<rbrace> get \<lbrace>?Q\<rbrace>
 3. \<lbrace>?S'\<rbrace> get \<lbrace>?Q'\<rbrace>
 4. \<And>s. desk s = c \<Longrightarrow> ?P s \<and> ?S s
 5. \<And>s. desk s = c \<Longrightarrow> ?P' s \<and> ?S' s proof (prove)
goal (5 subgoals):
 1. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (get s); (aa, ba) \<in> fst (get t); ?P s; ?P' t\<rbrakk> \<Longrightarrow> desk a = desk aa
 2. \<lbrace>?S\<rbrace> get \<lbrace>?Q\<rbrace>
 3. \<lbrace>?S'\<rbrace> get \<lbrace>?Q'\<rbrace>
 4. \<And>s. desk s = c \<Longrightarrow> ?P s \<and> ?S s
 5. \<And>s. desk s = c \<Longrightarrow> ?P' s \<and> ?S' s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?S\<rbrace> get \<lbrace>?Q\<rbrace>
 2. \<lbrace>?S'\<rbrace> get \<lbrace>?Q'\<rbrace>
 3. \<And>s. desk s = c \<Longrightarrow> False \<and> ?S s
 4. \<And>s. desk s = c \<Longrightarrow> ?P' s \<and> ?S' s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?S'\<rbrace> get \<lbrace>?Q'\<rbrace>
 2. \<And>s. desk s = c \<Longrightarrow> False \<and> K ?P26 s
 3. \<And>s. desk s = c \<Longrightarrow> ?P' s \<and> ?S' s proof (prove)
goal (2 subgoals):
 1. \<And>s. desk s = c \<Longrightarrow> False \<and> K ?P26 s
 2. \<And>s. desk s = c \<Longrightarrow> ?P' s \<and> K ?P29 s