kings-crown/FVELER_Isabelle huggingface dataset:
theory Abstract_Separation_D

lemma clean_slots_map_add_comm:
  "cmps_a \<inter> cmps_b = {}
  \<Longrightarrow> clean_slots slots_a cmps_a ++ clean_slots slots_b cmps_b =
      clean_slots slots_b cmps_b ++ clean_slots slots_a cmps_a" apply (clarsimp simp: clean_slots_def) apply (drule the_set_inter_empty) apply (erule map_add_restrict_comm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cmps_a \<inter> cmps_b = {} \<Longrightarrow> clean_slots slots_a cmps_a ++ clean_slots slots_b cmps_b = clean_slots slots_b cmps_b ++ clean_slots slots_a cmps_a proof (prove)
goal (1 subgoal):
 1. cmps_a \<inter> cmps_b = {} \<Longrightarrow> slots_a |` the_set cmps_a ++ slots_b |` the_set cmps_b = slots_b |` the_set cmps_b ++ slots_a |` the_set cmps_a proof (prove)
goal (1 subgoal):
 1. the_set cmps_a \<inter> the_set cmps_b = {} \<Longrightarrow> slots_a |` the_set cmps_a ++ slots_b |` the_set cmps_b = slots_b |` the_set cmps_b ++ slots_a |` the_set cmps_a proof (prove)
goal:
No subgoals!
theory Abstract_Separation_D

lemma object_clean_all:
  "object_type obj_a = object_type obj_b \<Longrightarrow> object_clean obj_b {} = object_clean obj_a {}" apply (clarsimp simp: object_clean_def object_clean_slots_def clean_slots_def the_set_def) apply (rule_tac cmps'1="{}" and obj'1="obj_a" in trans [OF update_slots_object_clean_fields], fastforce+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. object_type obj_a = object_type obj_b \<Longrightarrow> object_clean obj_b {} = object_clean obj_a {} proof (prove)
goal (1 subgoal):
 1. object_type obj_a = object_type obj_b \<Longrightarrow> update_slots (\<lambda>x. None) (object_clean_fields obj_b {}) = update_slots (\<lambda>x. None) (object_clean_fields obj_a {}) proof (prove)
goal:
No subgoals!
theory Abstract_Separation_D

lemma add_to_slots_comm:
  "\<lbrakk>object_slots y_obj \<bottom> object_slots z_obj; update_slots Map.empty y_obj = update_slots Map.empty z_obj \<rbrakk>
  \<Longrightarrow> add_to_slots (object_slots z_obj) y_obj = add_to_slots (object_slots y_obj) z_obj" by (fastforce simp: add_to_slots_def update_slots_def object_slots_def
                     cdl_tcb.splits cdl_cnode.splits
              dest!: map_add_com
              split: cdl_object.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>object_slots y_obj \<bottom> object_slots z_obj; update_slots (\<lambda>x. None) y_obj = update_slots (\<lambda>x. None) z_obj\<rbrakk> \<Longrightarrow> Abstract_Separation_D.add_to_slots (object_slots z_obj) y_obj = Abstract_Separation_D.add_to_slots (object_slots y_obj) z_obj
theory Abstract_Separation_D

lemma cdl_heap_add_none2:
  "cdl_heap_add x y obj_id = None \<Longrightarrow> (sep_heap y) obj_id = None" by (clarsimp simp: cdl_heap_add_def Let_unfold split:option.splits if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cdl_heap_add x y obj_id = None \<Longrightarrow> sep_heap y obj_id = None
theory Abstract_Separation_D

lemma object_type_object_addL:
  "object_type obj = object_type obj'
  \<Longrightarrow> object_type (object_add obj obj' cmp cmp') = object_type obj" by (clarsimp simp: object_add_def Let_unfold)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. object_type obj = object_type obj' \<Longrightarrow> object_type (object_add obj obj' cmp cmp') = object_type obj
theory Abstract_Separation_D

lemma object_type_object_addR:
  "object_type obj = object_type obj'
  \<Longrightarrow> object_type (object_add obj obj' cmp cmp') = object_type obj'" by (clarsimp simp: object_add_def Let_unfold)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. object_type obj = object_type obj' \<Longrightarrow> object_type (object_add obj obj' cmp cmp') = object_type obj'
theory Abstract_Separation_D

lemma sep_state_add_disjL:
  "\<lbrakk>sep_state_disj y z; sep_state_disj x (sep_state_add y z)\<rbrakk> \<Longrightarrow> sep_state_disj x y" apply (clarsimp simp: sep_state_disj_def sep_state_add_def) apply (rename_tac obj_id) apply (clarsimp simp: not_conflicting_objects_def) apply (erule_tac x=obj_id in allE)+ apply (fastforce simp: cdl_heap_add_def cdl_ghost_state_add_def object_type_object_addR
                 split: option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sep_state_disj y z; sep_state_disj x (sep_state_add y z)\<rbrakk> \<Longrightarrow> sep_state_disj x y proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>All (not_conflicting_objects y z); All (not_conflicting_objects x (SepState (cdl_heap_add y z) (cdl_ghost_state_add y z)))\<rbrakk> \<Longrightarrow> not_conflicting_objects x y xa proof (prove)
goal (1 subgoal):
 1. \<And>obj_id. \<lbrakk>All (not_conflicting_objects y z); All (not_conflicting_objects x (SepState (cdl_heap_add y z) (cdl_ghost_state_add y z)))\<rbrakk> \<Longrightarrow> not_conflicting_objects x y obj_id proof (prove)
goal (1 subgoal):
 1. \<And>obj_id. \<lbrakk>\<forall>obj_id. case sep_heap y obj_id of None \<Rightarrow> True | Some o1 \<Rightarrow> case sep_heap z obj_id of None \<Rightarrow> True | Some o2 \<Rightarrow> object_type o1 = object_type o2 \<and> sep_ghost_state y obj_id \<inter> sep_ghost_state z obj_id = {}; \<forall>obj_id. case sep_heap x obj_id of None \<Rightarrow> True | Some o1 \<Rightarrow> case cdl_heap_add y z obj_id of None \<Rightarrow> True | Some o2 \<Rightarrow> object_type o1 = object_type o2 \<and> sep_ghost_state x obj_id \<inter> cdl_ghost_state_add y z obj_id = {}\<rbrakk> \<Longrightarrow> case sep_heap x obj_id of None \<Rightarrow> True | Some o1 \<Rightarrow> case sep_heap y obj_id of None \<Rightarrow> True | Some o2 \<Rightarrow> object_type o1 = object_type o2 \<and> sep_ghost_state x obj_id \<inter> sep_ghost_state y obj_id = {} proof (prove)
goal (1 subgoal):
 1. \<And>obj_id. \<lbrakk>case sep_heap y obj_id of None \<Rightarrow> True | Some o1 \<Rightarrow> case sep_heap z obj_id of None \<Rightarrow> True | Some o2 \<Rightarrow> object_type o1 = object_type o2 \<and> sep_ghost_state y obj_id \<inter> sep_ghost_state z obj_id = {}; case sep_heap x obj_id of None \<Rightarrow> True | Some o1 \<Rightarrow> case cdl_heap_add y z obj_id of None \<Rightarrow> True | Some o2 \<Rightarrow> object_type o1 = object_type o2 \<and> sep_ghost_state x obj_id \<inter> cdl_ghost_state_add y z obj_id = {}\<rbrakk> \<Longrightarrow> case sep_heap x obj_id of None \<Rightarrow> True | Some o1 \<Rightarrow> case sep_heap y obj_id of None \<Rightarrow> True | Some o2 \<Rightarrow> object_type o1 = object_type o2 \<and> sep_ghost_state x obj_id \<inter> sep_ghost_state y obj_id = {} proof (prove)
goal:
No subgoals!
theory Abstract_Separation_D

lemma sep_state_add_disjR:
  "\<lbrakk>sep_state_disj y z; sep_state_disj x (sep_state_add y z)\<rbrakk> \<Longrightarrow> sep_state_disj x z" apply (clarsimp simp: sep_state_disj_def sep_state_add_def) apply (rename_tac obj_id) apply (clarsimp simp: not_conflicting_objects_def) apply (erule_tac x=obj_id in allE)+ apply (fastforce simp: cdl_heap_add_def cdl_ghost_state_add_def object_type_object_addR
                 split: option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sep_state_disj y z; sep_state_disj x (sep_state_add y z)\<rbrakk> \<Longrightarrow> sep_state_disj x z proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>All (not_conflicting_objects y z); All (not_conflicting_objects x (SepState (cdl_heap_add y z) (cdl_ghost_state_add y z)))\<rbrakk> \<Longrightarrow> not_conflicting_objects x z xa proof (prove)
goal (1 subgoal):
 1. \<And>obj_id. \<lbrakk>All (not_conflicting_objects y z); All (not_conflicting_objects x (SepState (cdl_heap_add y z) (cdl_ghost_state_add y z)))\<rbrakk> \<Longrightarrow> not_conflicting_objects x z obj_id proof (prove)
goal (1 subgoal):
 1. \<And>obj_id. \<lbrakk>\<forall>obj_id. case sep_heap y obj_id of None \<Rightarrow> True | Some o1 \<Rightarrow> case sep_heap z obj_id of None \<Rightarrow> True | Some o2 \<Rightarrow> object_type o1 = object_type o2 \<and> sep_ghost_state y obj_id \<inter> sep_ghost_state z obj_id = {}; \<forall>obj_id. case sep_heap x obj_id of None \<Rightarrow> True | Some o1 \<Rightarrow> case cdl_heap_add y z obj_id of None \<Rightarrow> True | Some o2 \<Rightarrow> object_type o1 = object_type o2 \<and> sep_ghost_state x obj_id \<inter> cdl_ghost_state_add y z obj_id = {}\<rbrakk> \<Longrightarrow> case sep_heap x obj_id of None \<Rightarrow> True | Some o1 \<Rightarrow> case sep_heap z obj_id of None \<Rightarrow> True | Some o2 \<Rightarrow> object_type o1 = object_type o2 \<and> sep_ghost_state x obj_id \<inter> sep_ghost_state z obj_id = {} proof (prove)
goal (1 subgoal):
 1. \<And>obj_id. \<lbrakk>case sep_heap y obj_id of None \<Rightarrow> True | Some o1 \<Rightarrow> case sep_heap z obj_id of None \<Rightarrow> True | Some o2 \<Rightarrow> object_type o1 = object_type o2 \<and> sep_ghost_state y obj_id \<inter> sep_ghost_state z obj_id = {}; case sep_heap x obj_id of None \<Rightarrow> True | Some o1 \<Rightarrow> case cdl_heap_add y z obj_id of None \<Rightarrow> True | Some o2 \<Rightarrow> object_type o1 = object_type o2 \<and> sep_ghost_state x obj_id \<inter> cdl_ghost_state_add y z obj_id = {}\<rbrakk> \<Longrightarrow> case sep_heap x obj_id of None \<Rightarrow> True | Some o1 \<Rightarrow> case sep_heap z obj_id of None \<Rightarrow> True | Some o2 \<Rightarrow> object_type o1 = object_type o2 \<and> sep_ghost_state x obj_id \<inter> sep_ghost_state z obj_id = {} proof (prove)
goal:
No subgoals!
theory Separation_D

lemma sep_map_general_def2:
  "sep_map_general p obj gs s =
   (dom (sep_heap s) = {p} \<and> ko_at obj p (sep_heap s) \<and> sep_ghost_state s p = gs)" apply (clarsimp simp: sep_map_general_def object_at_def) apply (rule) apply clarsimp apply (clarsimp simp: fun_upd_def) apply (rule ext) apply (fastforce simp: dom_def split:if_split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sep_map_general p obj gs s = (dom (sep_heap s) = {p} \<and> ko_at obj p (sep_heap s) \<and> sep_ghost_state s p = gs) proof (prove)
goal (1 subgoal):
 1. (sep_heap s = [p \<mapsto> obj] \<and> sep_ghost_state s p = gs) = (dom (sep_heap s) = {p} \<and> sep_heap s p = Some obj \<and> sep_ghost_state s p = gs) proof (prove)
goal (2 subgoals):
 1. sep_heap s = [p \<mapsto> obj] \<and> sep_ghost_state s p = gs \<Longrightarrow> dom (sep_heap s) = {p} \<and> sep_heap s p = Some obj \<and> sep_ghost_state s p = gs
 2. dom (sep_heap s) = {p} \<and> sep_heap s p = Some obj \<and> sep_ghost_state s p = gs \<Longrightarrow> sep_heap s = [p \<mapsto> obj] \<and> sep_ghost_state s p = gs proof (prove)
goal (1 subgoal):
 1. dom (sep_heap s) = {p} \<and> sep_heap s p = Some obj \<and> sep_ghost_state s p = gs \<Longrightarrow> sep_heap s = [p \<mapsto> obj] \<and> sep_ghost_state s p = gs proof (prove)
goal (1 subgoal):
 1. \<lbrakk>dom (sep_heap s) = {p}; sep_heap s p = Some obj; gs = sep_ghost_state s p\<rbrakk> \<Longrightarrow> sep_heap s = (\<lambda>x. if x = p then Some obj else None) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>dom (sep_heap s) = {p}; sep_heap s p = Some obj; gs = sep_ghost_state s p\<rbrakk> \<Longrightarrow> sep_heap s x = (if x = p then Some obj else None) proof (prove)
goal:
No subgoals!
theory EquivValidTutorial

lemma "equiv_valid I \<top>\<top> \<top>\<top> P f = equiv_valid \<top>\<top> I I P f" unfolding equiv_valid_def2 equiv_valid_2_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv I (\<lambda>_ _. True) P f = equiv_valid_inv (\<lambda>_ _. True) I P f proof (prove)
goal (1 subgoal):
 1. (\<forall>s t. P s \<and> P t \<and> I s t \<and> True \<longrightarrow> (\<forall>(rva, s')\<in>fst (f s). \<forall>(rvb, t')\<in>fst (f t). rva = rvb \<and> I s' t' \<and> True)) = (\<forall>s t. P s \<and> P t \<and> True \<and> I s t \<longrightarrow> (\<forall>(rva, s')\<in>fst (f s). \<forall>(rvb, t')\<in>fst (f t). rva = rvb \<and> True \<and> I s' t'))
theory EquivValidTutorial

lemma "equiv_valid_inv I A P f" unfolding equiv_valid_def2 oops
\<comment> \<open>Generalised to allow specifying equivalence R on return values.\<close>

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv I A P f proof (prove)
goal (1 subgoal):
 1. equiv_valid_rv_inv I A (=) P f
theory EquivValidTutorial

lemma "equiv_valid_rv I A B R P f" unfolding equiv_valid_2_def oops

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_rv I A B R P f proof (prove)
goal (1 subgoal):
 1. \<forall>s t. P s \<and> P t \<and> I s t \<and> A s t \<longrightarrow> (\<forall>(rva, s')\<in>fst (f s). \<forall>(rvb, t')\<in>fst (f t). R rva rvb \<and> I s' t' \<and> B s' t')
theory EquivValidTutorial

lemma "equiv_valid_2 I A B R P P' f f'" unfolding equiv_valid_2_def oops

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_2 I A B R P P' f f' proof (prove)
goal (1 subgoal):
 1. \<forall>s t. P s \<and> P' t \<and> I s t \<and> A s t \<longrightarrow> (\<forall>(rva, s')\<in>fst (f s). \<forall>(rvb, t')\<in>fst (f' t). R rva rvb \<and> I s' t' \<and> B s' t')
theory EquivValidTutorial

lemma "gets desk = do document \<leftarrow> gets desk; return document od" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. gets desk = gets desk >>= return
theory EquivValidTutorial

lemma gets_desk_return_leak:
  \<comment> \<open> No restrictions on pre-equivalence, precondition, or post-equivalence. \<close>
  "\<lbrace>|\<top>\<top>|, \<top>\<rbrace> gets desk \<lbrace>|\<top>\<top>|\<rbrace>" find_theorems intro
  \<comment> \<open> There happens to be an applicable \<open>gets\<close> rule for \<open>equiv_valid_inv\<close>. \<close> thm gets_ev'' apply(rule gets_ev'')
  \<comment> \<open> \<open>equiv_valid\<close> requires the return value to be the same in both runs.
     As expected, we are stuck, as we don't know that the contents of \<open>desk\<close>
     were initially the same for both runs. \<close> nitpick oops

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (\<lambda>_ _. True) (\<lambda>_ _. True) (\<lambda>_. True) (gets desk) proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (\<lambda>_ _. True) (\<lambda>_ _. True) (\<lambda>_. True) (gets desk) proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (\<lambda>_ _. True) (\<lambda>_ _. True) (\<lambda>_. True) (gets desk) proof (prove)
goal (1 subgoal):
 1. \<forall>s t. True \<and> True \<and> True \<and> True \<longrightarrow> desk s = desk t proof (prove)
goal (1 subgoal):
 1. \<forall>s t. True \<and> True \<and> True \<and> True \<longrightarrow> desk s = desk t
theory EquivValidTutorial

lemma gets_desk_equiv_return:
  \<comment> \<open> Pre-equivalence (and post-equivalence):
      The value of \<open>desk\<close> is equal initially (and finally) for both runs. \<close>
  "\<lbrace>|desk_equivalence|, \<top>\<rbrace>
     gets desk
   \<lbrace>|desk_equivalence|\<rbrace>" find_theorems intro apply(rule gets_ev'') unfolding desk_equivalence_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (\<lambda>_ _. True) desk_equivalence (\<lambda>_. True) (gets desk) proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (\<lambda>_ _. True) desk_equivalence (\<lambda>_. True) (gets desk) proof (prove)
goal (1 subgoal):
 1. \<forall>s t. True \<and> desk_equivalence s t \<and> True \<and> True \<longrightarrow> desk s = desk t proof (prove)
goal (1 subgoal):
 1. \<forall>s t. True \<and> desk s = desk t \<and> True \<and> True \<longrightarrow> desk s = desk t
theory EquivValidTutorial

lemma "\<lbrace>|\<top>\<top>|, \<top>\<rbrace> f \<lbrace>|\<top>\<top>|\<rbrace> = equiv_valid_rv \<top>\<top> \<top>\<top> \<top>\<top> (=) \<top> f" by (simp add:equiv_valid_def2) \<comment> \<open> Try replacing the \<open>(=)\<close> here. \<close>

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (\<lambda>_ _. True) (\<lambda>_ _. True) (\<lambda>_. True) f = equiv_valid_rv_inv (\<lambda>_ _. True) (\<lambda>_ _. True) (=) (\<lambda>_. True) f
theory EquivValidTutorial

lemma reveal_desk_window_leak:
  \<comment> \<open> Pre-equivalence and post-equivalence:
      The value of \<open>window\<close> is equal initially and finally for both runs. \<close>
  "\<lbrace>|window_equivalence|, \<top>\<rbrace>
     reveal_desk_to_window
   \<lbrace>|window_equivalence|\<rbrace>" unfolding reveal_desk_to_window_def
  \<comment> \<open> We find an applicable \<open>modify\<close> rule for \<open>equiv_valid_inv\<close>. \<close> find_theorems intro apply(rule modify_ev'')
  \<comment> \<open> Applying it, we see that it demands that \<open>window_equivalence\<close> holds
      between the final states of both runs. \<close> unfolding window_equivalence_def apply clarsimp
  \<comment> \<open> We should not expect to be able to prove this, because we have
      said nothing about the initial value of desk in these runs. \<close> oops

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (\<lambda>_ _. True) window_equivalence (\<lambda>_. True) reveal_desk_to_window proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (\<lambda>_ _. True) window_equivalence (\<lambda>_. True) (modify (\<lambda>s. s\<lparr>window := desk s\<rparr>)) proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (\<lambda>_ _. True) window_equivalence (\<lambda>_. True) (modify (\<lambda>s. s\<lparr>window := desk s\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s t. \<lbrakk>True; window_equivalence s t; True; True\<rbrakk> \<Longrightarrow> True \<and> window_equivalence (s\<lparr>window := desk s\<rparr>) (t\<lparr>window := desk t\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s t. \<lbrakk>True; window s = window t; True; True\<rbrakk> \<Longrightarrow> True \<and> window (s\<lparr>window := desk s\<rparr>) = window (t\<lparr>window := desk t\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s t. window s = window t \<Longrightarrow> desk s = desk t
theory EquivValidTutorial

lemma reveal_desk_equiv_window_equiv:
  "\<lbrace>|desk_equivalence and window_equivalence|, \<top>\<rbrace>
     reveal_desk_to_window
   \<lbrace>|desk_equivalence and window_equivalence|\<rbrace>" unfolding reveal_desk_to_window_def apply(rule modify_ev'') unfolding desk_equivalence_def window_equivalence_def by clarsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (\<lambda>_ _. True) (desk_equivalence and window_equivalence) (\<lambda>_. True) reveal_desk_to_window proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (\<lambda>_ _. True) (desk_equivalence and window_equivalence) (\<lambda>_. True) (modify (\<lambda>s. s\<lparr>window := desk s\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s t. \<lbrakk>True; (desk_equivalence and window_equivalence) s t; True; True\<rbrakk> \<Longrightarrow> True \<and> (desk_equivalence and window_equivalence) (s\<lparr>window := desk s\<rparr>) (t\<lparr>window := desk t\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s t. \<lbrakk>True; ((\<lambda>r1 r2. desk r1 = desk r2) and (\<lambda>r1 r2. window r1 = window r2)) s t; True; True\<rbrakk> \<Longrightarrow> True \<and> ((\<lambda>r1 r2. desk r1 = desk r2) and (\<lambda>r1 r2. window r1 = window r2)) (s\<lparr>window := desk s\<rparr>) (t\<lparr>window := desk t\<rparr>)
theory EquivValidTutorial

lemma gets_desk_equiv_return_using_wp:
  "\<lbrace>|desk_equivalence|, \<top>\<rbrace>
     gets desk
   \<lbrace>|desk_equivalence|\<rbrace>"
  \<comment> \<open> Use \<open>pre_ev\<close> to weaken the precondition of the \<open>equiv_valid\<close> statement
       and make the \<open>wp\<close> method applicable. \<close> apply(rule pre_ev) apply wp unfolding desk_equivalence_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (\<lambda>_ _. True) desk_equivalence (\<lambda>_. True) (gets desk) proof (prove)
goal (2 subgoals):
 1. equiv_valid_inv (\<lambda>_ _. True) desk_equivalence ?Q (gets desk)
 2. \<And>s. True \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> \<forall>s t. True \<and> desk_equivalence s t \<longrightarrow> desk s = desk t proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> \<forall>s t. True \<and> desk s = desk t \<longrightarrow> desk s = desk t
theory EquivValidTutorial

lemma reveal_desk_equiv_window_equiv_using_wp:
  "\<lbrace>|desk_equivalence and window_equivalence|, \<top>\<rbrace>
     reveal_desk_to_window
   \<lbrace>|desk_equivalence and window_equivalence|\<rbrace>" unfolding reveal_desk_to_window_def apply(rule pre_ev) apply(wp add:modify_ev) unfolding desk_equivalence_def window_equivalence_def by clarsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (\<lambda>_ _. True) (desk_equivalence and window_equivalence) (\<lambda>_. True) reveal_desk_to_window proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (\<lambda>_ _. True) (desk_equivalence and window_equivalence) (\<lambda>_. True) (modify (\<lambda>s. s\<lparr>window := desk s\<rparr>)) proof (prove)
goal (2 subgoals):
 1. equiv_valid_inv (\<lambda>_ _. True) (desk_equivalence and window_equivalence) ?Q (modify (\<lambda>s. s\<lparr>window := desk s\<rparr>))
 2. \<And>s. True \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> \<forall>s t. True \<and> (desk_equivalence and window_equivalence) s t \<longrightarrow> True \<and> (desk_equivalence and window_equivalence) (s\<lparr>window := desk s\<rparr>) (t\<lparr>window := desk t\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> \<forall>s t. True \<and> ((\<lambda>r1 r2. desk r1 = desk r2) and (\<lambda>r1 r2. window r1 = window r2)) s t \<longrightarrow> True \<and> ((\<lambda>r1 r2. desk r1 = desk r2) and (\<lambda>r1 r2. window r1 = window r2)) (s\<lparr>window := desk s\<rparr>) (t\<lparr>window := desk t\<rparr>)
theory EquivValidTutorial

lemma example_precond_desk_return:
  \<comment> \<open> Precondition: The value of desk is some fixed value \<open>c\<close>.
      \<open>equiv_valid\<close> then assumes that this precondition applies to both runs. \<close>
  "\<lbrace>|\<top>\<top>|, (\<lambda>s. desk s = c)\<rbrace>
     gets desk
   \<lbrace>|\<top>\<top>|\<rbrace>" apply(wp del:gets_ev add:gets_ev'') by force

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (\<lambda>_ _. True) (\<lambda>_ _. True) (\<lambda>s. desk s = c) (gets desk) proof (prove)
goal (1 subgoal):
 1. \<forall>s t. True \<and> True \<and> desk s = c \<and> desk t = c \<longrightarrow> desk s = desk t
theory EquivValidTutorial

lemma reveal_const_desk_preserves_window_equiv:
  \<comment> \<open> Precondition: Desk initially has a fixed constant \<open>c\<close>.
      \<open>equiv_valid\<close> then assumes that this precondition applies to both runs. \<close>
  "\<lbrace>|window_equivalence|, (\<lambda>s. desk s = c)\<rbrace>
     reveal_desk_to_window
   \<lbrace>|window_equivalence|\<rbrace>" unfolding reveal_desk_to_window_def apply(wp add:modify_ev'') unfolding window_equivalence_def by clarsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (\<lambda>_ _. True) window_equivalence (\<lambda>s. desk s = c) reveal_desk_to_window proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (\<lambda>_ _. True) window_equivalence (\<lambda>s. desk s = c) (modify (\<lambda>s. s\<lparr>window := desk s\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s t. \<lbrakk>True; window_equivalence s t; desk s = c; desk t = c\<rbrakk> \<Longrightarrow> window_equivalence (s\<lparr>window := desk s\<rparr>) (t\<lparr>window := desk t\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s t. \<lbrakk>True; window s = window t; desk s = c; desk t = c\<rbrakk> \<Longrightarrow> window (s\<lparr>window := desk s\<rparr>) = window (t\<lparr>window := desk t\<rparr>)