theory Retype_DP

lemma validE_def2:
  "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace> =
  \<lbrace>P\<rbrace> f \<lbrace>\<lambda>v s. (\<forall>e. v = Inl e \<longrightarrow> E e s) \<and> (\<forall>r. v = Inr r \<longrightarrow> Q r s)\<rbrace>" apply (clarsimp simp:validE_def valid_def) apply (rule iffI) apply clarsimp apply (drule_tac x = s in spec) apply fastforce apply clarsimp apply (drule_tac x = s in spec) apply clarsimp apply (drule_tac x = "(a,b)" in bspec) apply simp apply clarsimp apply (case_tac a) apply clarsimp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace> = \<lbrace>P\<rbrace> f \<lbrace>\<lambda>v s. (\<forall>e. v = Inl e \<longrightarrow> E e s) \<and> (\<forall>r. v = Inr r \<longrightarrow> Q r s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. (\<forall>s. P s \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (Inl e, s') \<Rightarrow> E e s' | (Inr ra, s') \<Rightarrow> Q ra s')) = (\<forall>s. P s \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (r, s') \<Rightarrow> (\<forall>e. r = Inl e \<longrightarrow> E e s') \<and> (\<forall>ra. r = Inr ra \<longrightarrow> Q ra s'))) proof (prove)
goal (2 subgoals):
 1. \<forall>s. P s \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (Inl e, s') \<Rightarrow> E e s' | (Inr ra, s') \<Rightarrow> Q ra s') \<Longrightarrow> \<forall>s. P s \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (r, s') \<Rightarrow> (\<forall>e. r = Inl e \<longrightarrow> E e s') \<and> (\<forall>ra. r = Inr ra \<longrightarrow> Q ra s'))
 2. \<forall>s. P s \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (r, s') \<Rightarrow> (\<forall>e. r = Inl e \<longrightarrow> E e s') \<and> (\<forall>ra. r = Inr ra \<longrightarrow> Q ra s')) \<Longrightarrow> \<forall>s. P s \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (Inl e, s') \<Rightarrow> E e s' | (Inr ra, s') \<Rightarrow> Q ra s') proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<lbrakk>\<forall>s. P s \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (Inl e, s') \<Rightarrow> E e s' | (Inr ra, s') \<Rightarrow> Q ra s'); P s; (a, b) \<in> fst (f s)\<rbrakk> \<Longrightarrow> (\<forall>e. a = Inl e \<longrightarrow> E e b) \<and> (\<forall>r. a = Inr r \<longrightarrow> Q r b)
 2. \<forall>s. P s \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (r, s') \<Rightarrow> (\<forall>e. r = Inl e \<longrightarrow> E e s') \<and> (\<forall>ra. r = Inr ra \<longrightarrow> Q ra s')) \<Longrightarrow> \<forall>s. P s \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (Inl e, s') \<Rightarrow> E e s' | (Inr ra, s') \<Rightarrow> Q ra s') proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<lbrakk>P s; (a, b) \<in> fst (f s); P s \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (Inl e, s') \<Rightarrow> E e s' | (Inr ra, s') \<Rightarrow> Q ra s')\<rbrakk> \<Longrightarrow> (\<forall>e. a = Inl e \<longrightarrow> E e b) \<and> (\<forall>r. a = Inr r \<longrightarrow> Q r b)
 2. \<forall>s. P s \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (r, s') \<Rightarrow> (\<forall>e. r = Inl e \<longrightarrow> E e s') \<and> (\<forall>ra. r = Inr ra \<longrightarrow> Q ra s')) \<Longrightarrow> \<forall>s. P s \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (Inl e, s') \<Rightarrow> E e s' | (Inr ra, s') \<Rightarrow> Q ra s') proof (prove)
goal (1 subgoal):
 1. \<forall>s. P s \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (r, s') \<Rightarrow> (\<forall>e. r = Inl e \<longrightarrow> E e s') \<and> (\<forall>ra. r = Inr ra \<longrightarrow> Q ra s')) \<Longrightarrow> \<forall>s. P s \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (Inl e, s') \<Rightarrow> E e s' | (Inr ra, s') \<Rightarrow> Q ra s') proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>\<forall>s. P s \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (r, s') \<Rightarrow> (\<forall>e. r = Inl e \<longrightarrow> E e s') \<and> (\<forall>ra. r = Inr ra \<longrightarrow> Q ra s')); P s; (a, b) \<in> fst (f s)\<rbrakk> \<Longrightarrow> case a of Inl e \<Rightarrow> E e b | Inr r \<Rightarrow> Q r b proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>P s; (a, b) \<in> fst (f s); P s \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (r, s') \<Rightarrow> (\<forall>e. r = Inl e \<longrightarrow> E e s') \<and> (\<forall>ra. r = Inr ra \<longrightarrow> Q ra s'))\<rbrakk> \<Longrightarrow> case a of Inl e \<Rightarrow> E e b | Inr r \<Rightarrow> Q r b proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>P s; (a, b) \<in> fst (f s); \<forall>x\<in>fst (f s). case x of (r, s') \<Rightarrow> (\<forall>e. r = Inl e \<longrightarrow> E e s') \<and> (\<forall>ra. r = Inr ra \<longrightarrow> Q ra s')\<rbrakk> \<Longrightarrow> case a of Inl e \<Rightarrow> E e b | Inr r \<Rightarrow> Q r b proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<lbrakk>P s; (a, b) \<in> fst (f s)\<rbrakk> \<Longrightarrow> (a, b) \<in> fst (f s)
 2. \<And>s a b. \<lbrakk>P s; (a, b) \<in> fst (f s); case (a, b) of (r, s') \<Rightarrow> (\<forall>e. r = Inl e \<longrightarrow> E e s') \<and> (\<forall>ra. r = Inr ra \<longrightarrow> Q ra s')\<rbrakk> \<Longrightarrow> case a of Inl e \<Rightarrow> E e b | Inr r \<Rightarrow> Q r b proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>P s; (a, b) \<in> fst (f s); case (a, b) of (r, s') \<Rightarrow> (\<forall>e. r = Inl e \<longrightarrow> E e s') \<and> (\<forall>ra. r = Inr ra \<longrightarrow> Q ra s')\<rbrakk> \<Longrightarrow> case a of Inl e \<Rightarrow> E e b | Inr r \<Rightarrow> Q r b proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>P s; (a, b) \<in> fst (f s); \<forall>e. a = Inl e \<longrightarrow> E e b; \<forall>r. a = Inr r \<longrightarrow> Q r b\<rbrakk> \<Longrightarrow> case a of Inl e \<Rightarrow> E e b | Inr r \<Rightarrow> Q r b proof (prove)
goal (2 subgoals):
 1. \<And>s a b aa. \<lbrakk>P s; (a, b) \<in> fst (f s); \<forall>e. a = Inl e \<longrightarrow> E e b; \<forall>r. a = Inr r \<longrightarrow> Q r b; a = Inl aa\<rbrakk> \<Longrightarrow> case a of Inl e \<Rightarrow> E e b | Inr r \<Rightarrow> Q r b
 2. \<And>s a b ba. \<lbrakk>P s; (a, b) \<in> fst (f s); \<forall>e. a = Inl e \<longrightarrow> E e b; \<forall>r. a = Inr r \<longrightarrow> Q r b; a = Inr ba\<rbrakk> \<Longrightarrow> case a of Inl e \<Rightarrow> E e b | Inr r \<Rightarrow> Q r b proof (prove)
goal:
No subgoals!