theory Nondet_More_VCG

lemma hoare_disj_division:
  "\<lbrakk> P \<or> Q; P \<Longrightarrow> \<lbrace>R\<rbrace> f \<lbrace>S\<rbrace>; Q \<Longrightarrow> \<lbrace>T\<rbrace> f \<lbrace>S\<rbrace> \<rbrakk>
   \<Longrightarrow> \<lbrace>\<lambda>s. (P \<longrightarrow> R s) \<and> (Q \<longrightarrow> T s)\<rbrace> f \<lbrace>S\<rbrace>" apply safe apply (rule hoare_pre_imp) prefer 2 apply simp apply simp apply (rule hoare_pre_imp) prefer 2 apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P \<or> Q; P \<Longrightarrow> \<lbrace>R\<rbrace> f \<lbrace>S\<rbrace>; Q \<Longrightarrow> \<lbrace>T\<rbrace> f \<lbrace>S\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (P \<longrightarrow> R s) \<and> (Q \<longrightarrow> T s)\<rbrace> f \<lbrace>S\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>P \<Longrightarrow> \<lbrace>R\<rbrace> f \<lbrace>S\<rbrace>; Q \<Longrightarrow> \<lbrace>T\<rbrace> f \<lbrace>S\<rbrace>; P\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (P \<longrightarrow> R s) \<and> (Q \<longrightarrow> T s)\<rbrace> f \<lbrace>S\<rbrace>
 2. \<lbrakk>P \<Longrightarrow> \<lbrace>R\<rbrace> f \<lbrace>S\<rbrace>; Q \<Longrightarrow> \<lbrace>T\<rbrace> f \<lbrace>S\<rbrace>; Q\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (P \<longrightarrow> R s) \<and> (Q \<longrightarrow> T s)\<rbrace> f \<lbrace>S\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>P \<Longrightarrow> \<lbrace>R\<rbrace> f \<lbrace>S\<rbrace>; Q \<Longrightarrow> \<lbrace>T\<rbrace> f \<lbrace>S\<rbrace>; P; (P \<longrightarrow> R s) \<and> (Q \<longrightarrow> T s)\<rbrakk> \<Longrightarrow> ?Q1 s
 2. \<lbrakk>P \<Longrightarrow> \<lbrace>R\<rbrace> f \<lbrace>S\<rbrace>; Q \<Longrightarrow> \<lbrace>T\<rbrace> f \<lbrace>S\<rbrace>; P\<rbrakk> \<Longrightarrow> \<lbrace>?Q1\<rbrace> f \<lbrace>S\<rbrace>
 3. \<lbrakk>P \<Longrightarrow> \<lbrace>R\<rbrace> f \<lbrace>S\<rbrace>; Q \<Longrightarrow> \<lbrace>T\<rbrace> f \<lbrace>S\<rbrace>; Q\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (P \<longrightarrow> R s) \<and> (Q \<longrightarrow> T s)\<rbrace> f \<lbrace>S\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrakk>P \<Longrightarrow> \<lbrace>R\<rbrace> f \<lbrace>S\<rbrace>; Q \<Longrightarrow> \<lbrace>T\<rbrace> f \<lbrace>S\<rbrace>; P\<rbrakk> \<Longrightarrow> \<lbrace>?Q1\<rbrace> f \<lbrace>S\<rbrace>
 2. \<And>s. \<lbrakk>P \<Longrightarrow> \<lbrace>R\<rbrace> f \<lbrace>S\<rbrace>; Q \<Longrightarrow> \<lbrace>T\<rbrace> f \<lbrace>S\<rbrace>; P; (P \<longrightarrow> R s) \<and> (Q \<longrightarrow> T s)\<rbrakk> \<Longrightarrow> ?Q1 s
 3. \<lbrakk>P \<Longrightarrow> \<lbrace>R\<rbrace> f \<lbrace>S\<rbrace>; Q \<Longrightarrow> \<lbrace>T\<rbrace> f \<lbrace>S\<rbrace>; Q\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (P \<longrightarrow> R s) \<and> (Q \<longrightarrow> T s)\<rbrace> f \<lbrace>S\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>P \<Longrightarrow> \<lbrace>R\<rbrace> f \<lbrace>S\<rbrace>; Q \<Longrightarrow> \<lbrace>T\<rbrace> f \<lbrace>S\<rbrace>; P; (P \<longrightarrow> R s) \<and> (Q \<longrightarrow> T s)\<rbrakk> \<Longrightarrow> R s
 2. \<lbrakk>P \<Longrightarrow> \<lbrace>R\<rbrace> f \<lbrace>S\<rbrace>; Q \<Longrightarrow> \<lbrace>T\<rbrace> f \<lbrace>S\<rbrace>; Q\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (P \<longrightarrow> R s) \<and> (Q \<longrightarrow> T s)\<rbrace> f \<lbrace>S\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P \<Longrightarrow> \<lbrace>R\<rbrace> f \<lbrace>S\<rbrace>; Q \<Longrightarrow> \<lbrace>T\<rbrace> f \<lbrace>S\<rbrace>; Q\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (P \<longrightarrow> R s) \<and> (Q \<longrightarrow> T s)\<rbrace> f \<lbrace>S\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>P \<Longrightarrow> \<lbrace>R\<rbrace> f \<lbrace>S\<rbrace>; Q \<Longrightarrow> \<lbrace>T\<rbrace> f \<lbrace>S\<rbrace>; Q; (P \<longrightarrow> R s) \<and> (Q \<longrightarrow> T s)\<rbrakk> \<Longrightarrow> ?Q4 s
 2. \<lbrakk>P \<Longrightarrow> \<lbrace>R\<rbrace> f \<lbrace>S\<rbrace>; Q \<Longrightarrow> \<lbrace>T\<rbrace> f \<lbrace>S\<rbrace>; Q\<rbrakk> \<Longrightarrow> \<lbrace>?Q4\<rbrace> f \<lbrace>S\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>P \<Longrightarrow> \<lbrace>R\<rbrace> f \<lbrace>S\<rbrace>; Q \<Longrightarrow> \<lbrace>T\<rbrace> f \<lbrace>S\<rbrace>; Q\<rbrakk> \<Longrightarrow> \<lbrace>?Q4\<rbrace> f \<lbrace>S\<rbrace>
 2. \<And>s. \<lbrakk>P \<Longrightarrow> \<lbrace>R\<rbrace> f \<lbrace>S\<rbrace>; Q \<Longrightarrow> \<lbrace>T\<rbrace> f \<lbrace>S\<rbrace>; Q; (P \<longrightarrow> R s) \<and> (Q \<longrightarrow> T s)\<rbrakk> \<Longrightarrow> ?Q4 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>P \<Longrightarrow> \<lbrace>R\<rbrace> f \<lbrace>S\<rbrace>; Q \<Longrightarrow> \<lbrace>T\<rbrace> f \<lbrace>S\<rbrace>; Q; (P \<longrightarrow> R s) \<and> (Q \<longrightarrow> T s)\<rbrakk> \<Longrightarrow> T s proof (prove)
goal:
No subgoals!