theory ADT_IF

lemma hoare_add_postE:
  "\<lbrakk> \<lbrace>S\<rbrace> f \<lbrace>\<lambda>_. S'\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. S' s \<longrightarrow> Q r s\<rbrace>, \<lbrace>\<lambda>r s. S' s \<longrightarrow> E r s\<rbrace> \<rbrakk>
     \<Longrightarrow> \<lbrace>P and S\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" apply (clarsimp simp: validE_def) apply (rule hoare_add_post) apply assumption apply simp apply (rule hoare_strengthen_post) apply (rule hoare_pre) apply (assumption, simp, fastforce split: sum.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>S\<rbrace> f \<lbrace>\<lambda>_. S'\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. S' s \<longrightarrow> Q r s\<rbrace>, \<lbrace>\<lambda>r s. S' s \<longrightarrow> E r s\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P and S\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>S\<rbrace> f \<lbrace>\<lambda>_. S'\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> S' s \<longrightarrow> E e s | Inr r \<Rightarrow> S' s \<longrightarrow> Q r s\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P and S\<rbrace> f \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> E e s | Inr r \<Rightarrow> Q r s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<lbrace>S\<rbrace> f \<lbrace>\<lambda>_. S'\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> S' s \<longrightarrow> E e s | Inr r \<Rightarrow> S' s \<longrightarrow> Q r s\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>?P'2\<rbrace> f \<lbrace>?Q'2\<rbrace>
 2. \<And>s. \<lbrakk>\<lbrace>S\<rbrace> f \<lbrace>\<lambda>_. S'\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> S' s \<longrightarrow> E e s | Inr r \<Rightarrow> S' s \<longrightarrow> Q r s\<rbrace>; (P and S) s\<rbrakk> \<Longrightarrow> ?P'2 s
 3. \<lbrakk>\<lbrace>S\<rbrace> f \<lbrace>\<lambda>_. S'\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> S' s \<longrightarrow> E e s | Inr r \<Rightarrow> S' s \<longrightarrow> Q r s\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P and S\<rbrace> f \<lbrace>\<lambda>rv s. ?Q'2 rv s \<longrightarrow> (case rv of Inl e \<Rightarrow> E e s | Inr r \<Rightarrow> Q r s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<lbrace>S\<rbrace> f \<lbrace>\<lambda>_. S'\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> S' s \<longrightarrow> E e s | Inr r \<Rightarrow> S' s \<longrightarrow> Q r s\<rbrace>; (P and S) s\<rbrakk> \<Longrightarrow> S s
 2. \<lbrakk>\<lbrace>S\<rbrace> f \<lbrace>\<lambda>_. S'\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> S' s \<longrightarrow> E e s | Inr r \<Rightarrow> S' s \<longrightarrow> Q r s\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P and S\<rbrace> f \<lbrace>\<lambda>rv s. S' s \<longrightarrow> (case rv of Inl e \<Rightarrow> E e s | Inr r \<Rightarrow> Q r s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>S\<rbrace> f \<lbrace>\<lambda>_. S'\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> S' s \<longrightarrow> E e s | Inr r \<Rightarrow> S' s \<longrightarrow> Q r s\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P and S\<rbrace> f \<lbrace>\<lambda>rv s. S' s \<longrightarrow> (case rv of Inl e \<Rightarrow> E e s | Inr r \<Rightarrow> Q r s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<lbrace>S\<rbrace> f \<lbrace>\<lambda>_. S'\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> S' s \<longrightarrow> E e s | Inr r \<Rightarrow> S' s \<longrightarrow> Q r s\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P and S\<rbrace> f \<lbrace>?Q6\<rbrace>
 2. \<And>rv s. \<lbrakk>\<lbrace>S\<rbrace> f \<lbrace>\<lambda>_. S'\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> S' s \<longrightarrow> E e s | Inr r \<Rightarrow> S' s \<longrightarrow> Q r s\<rbrace>; ?Q6 rv s\<rbrakk> \<Longrightarrow> S' s \<longrightarrow> (case rv of Inl e \<Rightarrow> E e s | Inr r \<Rightarrow> Q r s) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<lbrace>S\<rbrace> f \<lbrace>\<lambda>_. S'\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> S' s \<longrightarrow> E e s | Inr r \<Rightarrow> S' s \<longrightarrow> Q r s\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>?Q9\<rbrace> f \<lbrace>?Q6\<rbrace>
 2. \<And>s. \<lbrakk>\<lbrace>S\<rbrace> f \<lbrace>\<lambda>_. S'\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> S' s \<longrightarrow> E e s | Inr r \<Rightarrow> S' s \<longrightarrow> Q r s\<rbrace>; (P and S) s\<rbrakk> \<Longrightarrow> ?Q9 s
 3. \<And>rv s. \<lbrakk>\<lbrace>S\<rbrace> f \<lbrace>\<lambda>_. S'\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> S' s \<longrightarrow> E e s | Inr r \<Rightarrow> S' s \<longrightarrow> Q r s\<rbrace>; ?Q6 rv s\<rbrakk> \<Longrightarrow> S' s \<longrightarrow> (case rv of Inl e \<Rightarrow> E e s | Inr r \<Rightarrow> Q r s) proof (prove)
goal:
No subgoals!