theory EquivValidTutorial

lemma desk_equiv_no_longer_needed:
  "\<lbrace>|desk_equivalence|, \<top>\<rbrace>
       do reveal_desk_to_window;
          modify (\<lambda>r. r\<lparr>desk := inbox r\<rparr>)
       od
   \<lbrace>|window_equivalence|\<rbrace>"
  \<comment> \<open> Use \<open>pre_ev\<close> to weaken the precondition of the \<open>equiv_valid\<close> statement. \<close> apply(rule pre_ev)
   \<comment> \<open> Use \<open>bind_ev_general\<close> to split the goal into \<open>equiv_valid\<close> statements for
       each of the two \<open>modify\<close> commands. It will ask us to prove them in reverse order. \<close> apply(rule bind_ev_general)
     \<comment> \<open> Prove \<open>equiv_valid\<close> for \<open>desk := inbox\<close> manually. \<close> apply clarsimp apply(rule modify_ev'')
     \<comment> \<open> The \<open>force\<close> tactic has enough information here to figure out that
         the intermediate equivalence \<open>B\<close> needs to be \<open>window_equivalence\<close>. \<close> apply(force simp:window_equivalence_def desk_equivalence_def)
    \<comment> \<open> This happens to be the post-equivalence for the \<open>equiv_valid\<close> lemma
        we just proved for \<open>window := desk\<close>, so we can reuse that lemma here. \<close> using reveal_desk_equiv_to_window_equiv unfolding window_equivalence_def apply force apply wp apply force done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid (\<lambda>_ _. True) desk_equivalence window_equivalence (\<lambda>_. True) (do reveal_desk_to_window;
modify (\<lambda>r. r\<lparr>desk := inbox r\<rparr>)
od) proof (prove)
goal (2 subgoals):
 1. equiv_valid (\<lambda>_ _. True) desk_equivalence window_equivalence ?Q (do reveal_desk_to_window;
modify (\<lambda>r. r\<lparr>desk := inbox r\<rparr>)
od)
 2. \<And>s. True \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>rv. equiv_valid (\<lambda>_ _. True) ?B3 window_equivalence (?Q3 rv) (K_bind (modify (\<lambda>r. r\<lparr>desk := inbox r\<rparr>)) rv)
 2. equiv_valid (\<lambda>_ _. True) desk_equivalence ?B3 ?P'3 reveal_desk_to_window
 3. \<lbrace>?P''3\<rbrace> reveal_desk_to_window \<lbrace>?Q3\<rbrace>
 4. \<And>s. True \<Longrightarrow> ?P'3 s \<and> ?P''3 s proof (prove)
goal (4 subgoals):
 1. equiv_valid (\<lambda>_ _. True) ?B3 window_equivalence (?Q3 ()) (modify (\<lambda>r. r\<lparr>desk := inbox r\<rparr>))
 2. equiv_valid (\<lambda>_ _. True) desk_equivalence ?B3 ?P'3 reveal_desk_to_window
 3. \<lbrace>?P''3\<rbrace> reveal_desk_to_window \<lbrace>?Q3\<rbrace>
 4. \<And>s. True \<Longrightarrow> ?P'3 s \<and> ?P''3 s proof (prove)
goal (4 subgoals):
 1. \<And>s t. \<lbrakk>True; ?B3 s t; ?Q3 () s; ?Q3 () t\<rbrakk> \<Longrightarrow> True \<and> window_equivalence (s\<lparr>desk := inbox s\<rparr>) (t\<lparr>desk := inbox t\<rparr>)
 2. equiv_valid (\<lambda>_ _. True) desk_equivalence ?B3 ?P'3 reveal_desk_to_window
 3. \<lbrace>?P''3\<rbrace> reveal_desk_to_window \<lbrace>?Q3\<rbrace>
 4. \<And>s. True \<Longrightarrow> ?P'3 s \<and> ?P''3 s proof (prove)
goal (3 subgoals):
 1. equiv_valid (\<lambda>_ _. True) desk_equivalence (\<lambda>s t. window s = window t) ?P'3 reveal_desk_to_window
 2. \<lbrace>?P''3\<rbrace> reveal_desk_to_window \<lbrace>?Q3\<rbrace>
 3. \<And>s. True \<Longrightarrow> ?P'3 s \<and> ?P''3 s proof (prove)
using this:
equiv_valid (\<lambda>_ _. True) desk_equivalence window_equivalence (\<lambda>_. True) reveal_desk_to_window

goal (3 subgoals):
 1. equiv_valid (\<lambda>_ _. True) desk_equivalence (\<lambda>s t. window s = window t) ?P'3 reveal_desk_to_window
 2. \<lbrace>?P''3\<rbrace> reveal_desk_to_window \<lbrace>?Q3\<rbrace>
 3. \<And>s. True \<Longrightarrow> ?P'3 s \<and> ?P''3 s proof (prove)
using this:
equiv_valid (\<lambda>_ _. True) desk_equivalence (\<lambda>r1 r2. window r1 = window r2) (\<lambda>_. True) reveal_desk_to_window

goal (3 subgoals):
 1. equiv_valid (\<lambda>_ _. True) desk_equivalence (\<lambda>s t. window s = window t) ?P'3 reveal_desk_to_window
 2. \<lbrace>?P''3\<rbrace> reveal_desk_to_window \<lbrace>?Q3\<rbrace>
 3. \<And>s. True \<Longrightarrow> ?P'3 s \<and> ?P''3 s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P''3\<rbrace> reveal_desk_to_window \<lbrace>?Q3\<rbrace>
 2. \<And>s. True \<Longrightarrow> True \<and> ?P''3 s proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> True \<and> K ?P19 s proof (prove)
goal:
No subgoals!