theory EquivValidTutorial

lemma precond_get_return_desk:
  "\<lbrace>|\<top>\<top>|, (\<lambda>s. desk s = c)\<rbrace>
     do
       s \<leftarrow> get;
       return (desk s)
     od
   \<lbrace>|\<top>\<top>|\<rbrace>" apply(clarsimp simp:equiv_valid_def2)
  \<comment> \<open> We want to use the fact that \<open>desk\<close> contains \<open>c\<close> initially for both runs.
    So we give it here. \<close> apply(rule_tac P="(\<lambda>s. desk s = c)" and P'="(\<lambda>s. desk s = c)" in equiv_valid_2_bind_pre) apply(wp add:return_ev2) apply(clarsimp simp:equiv_valid_def2 equiv_valid_2_def)
      \<comment> \<open> No need to guess anything. \<close> apply(force simp add:get_def)
     \<comment> \<open> Use \<open>wp\<close> tactic to discharge the two Hoare triples; see Lib.WPTutorial for more info. \<close> apply wp apply wp apply force apply force done

(* 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_rv_inv (\<lambda>_ _. True) (\<lambda>_ _. True) ?R' (\<lambda>s. desk s = c) get
 3. \<lbrace>?S\<rbrace> get \<lbrace>?Q\<rbrace>
 4. \<lbrace>?S'\<rbrace> get \<lbrace>?Q'\<rbrace>
 5. \<And>s. desk s = c \<Longrightarrow> desk s = c \<and> ?S s
 6. \<And>s. desk s = c \<Longrightarrow> desk s = c \<and> ?S' s proof (prove)
goal (5 subgoals):
 1. equiv_valid_rv_inv (\<lambda>_ _. True) (\<lambda>_ _. True) (\<lambda>rv rv'. desk rv = desk rv') (\<lambda>s. desk s = c) get
 2. \<lbrace>?S\<rbrace> get \<lbrace>?Q\<rbrace>
 3. \<lbrace>?S'\<rbrace> get \<lbrace>?Q'\<rbrace>
 4. \<And>s. desk s = c \<Longrightarrow> desk s = c \<and> ?S s
 5. \<And>s. desk s = c \<Longrightarrow> desk s = c \<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); desk t = desk s; c = desk s\<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> desk s = c \<and> ?S s
 5. \<And>s. desk s = c \<Longrightarrow> desk s = c \<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> desk s = c \<and> ?S s
 4. \<And>s. desk s = c \<Longrightarrow> desk s = c \<and> ?S' s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?S'\<rbrace> get \<lbrace>?Q'\<rbrace>
 2. \<And>s. desk s = c \<Longrightarrow> desk s = c \<and> K ?P27 s
 3. \<And>s. desk s = c \<Longrightarrow> desk s = c \<and> ?S' s proof (prove)
goal (2 subgoals):
 1. \<And>s. desk s = c \<Longrightarrow> desk s = c \<and> K ?P27 s
 2. \<And>s. desk s = c \<Longrightarrow> desk s = c \<and> K ?P30 s proof (prove)
goal (1 subgoal):
 1. \<And>s. desk s = c \<Longrightarrow> desk s = c \<and> K ?P30 s proof (prove)
goal:
No subgoals!