theory Decode_IF

lemma select_ext_ev_bind:
  "(\<And>s t. \<lbrakk>I s t; A s t; a s \<in> S; a t \<in> S\<rbrakk> \<Longrightarrow> a s = a t)
   \<Longrightarrow> (\<And>x. x \<in> S \<Longrightarrow> equiv_valid_inv I A P (g x))
   \<Longrightarrow> equiv_valid_inv I A P ((select_ext a S) >>= (\<lambda>r s :: det_state. g r s))" apply (clarsimp simp: equiv_valid_def2 equiv_valid_2_def select_ext_def
                        bind_def gets_def return_def get_def assert_def fail_def) apply (drule_tac x=s in meta_spec) apply (drule_tac x="a s" in meta_spec) apply (drule_tac x=t in meta_spec) apply simp apply (drule_tac x=s in spec) apply (drule_tac x=t in spec) apply simp apply force done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s t. \<lbrakk>I s t; A s t; a s \<in> S; a t \<in> S\<rbrakk> \<Longrightarrow> a s = a t; \<And>x. x \<in> S \<Longrightarrow> equiv_valid_inv I A P (g x)\<rbrakk> \<Longrightarrow> equiv_valid_inv I A P (select_ext a S >>= g) proof (prove)
goal (1 subgoal):
 1. \<And>s t aa b aaa ba. \<lbrakk>\<And>s t. \<lbrakk>I s t; A s t; a s \<in> S; a t \<in> S\<rbrakk> \<Longrightarrow> a s = a t; \<And>x. x \<in> S \<Longrightarrow> \<forall>s t. P s \<and> P t \<and> I s t \<and> A s t \<longrightarrow> (\<forall>xa\<in>fst (g x s). case xa of (rva, s') \<Rightarrow> \<forall>x\<in>fst (g x t). case x of (rvb, t') \<Rightarrow> rva = rvb \<and> I s' t' \<and> A s' t'); a s \<in> S; a t \<in> S; (aa, b) \<in> fst (g (a s) s); (aaa, ba) \<in> fst (g (a t) t); P s; P t; I s t; A s t\<rbrakk> \<Longrightarrow> aa = aaa \<and> I b ba \<and> A b ba proof (prove)
goal (1 subgoal):
 1. \<And>s t aa b aaa ba. \<lbrakk>\<And>x. x \<in> S \<Longrightarrow> \<forall>s t. P s \<and> P t \<and> I s t \<and> A s t \<longrightarrow> (\<forall>xa\<in>fst (g x s). case xa of (rva, s') \<Rightarrow> \<forall>x\<in>fst (g x t). case x of (rvb, t') \<Rightarrow> rva = rvb \<and> I s' t' \<and> A s' t'); a s \<in> S; a t \<in> S; (aa, b) \<in> fst (g (a s) s); (aaa, ba) \<in> fst (g (a t) t); P s; P t; I s t; A s t; \<And>t. \<lbrakk>I s t; A s t; a s \<in> S; a t \<in> S\<rbrakk> \<Longrightarrow> a s = a t\<rbrakk> \<Longrightarrow> aa = aaa \<and> I b ba \<and> A b ba proof (prove)
goal (1 subgoal):
 1. \<And>s t aa b aaa ba. \<lbrakk>a s \<in> S; a t \<in> S; (aa, b) \<in> fst (g (a s) s); (aaa, ba) \<in> fst (g (a t) t); P s; P t; I s t; A s t; \<And>t. \<lbrakk>I s t; A s t; a s \<in> S; a t \<in> S\<rbrakk> \<Longrightarrow> a s = a t; a s \<in> S \<Longrightarrow> \<forall>sa t. P sa \<and> P t \<and> I sa t \<and> A sa t \<longrightarrow> (\<forall>x\<in>fst (g (a s) sa). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst (g (a s) t). case x of (rvb, t') \<Rightarrow> rva = rvb \<and> I s' t' \<and> A s' t')\<rbrakk> \<Longrightarrow> aa = aaa \<and> I b ba \<and> A b ba proof (prove)
goal (1 subgoal):
 1. \<And>s t aa b aaa ba. \<lbrakk>a s \<in> S; a t \<in> S; (aa, b) \<in> fst (g (a s) s); (aaa, ba) \<in> fst (g (a t) t); P s; P t; I s t; A s t; a s \<in> S \<Longrightarrow> \<forall>sa t. P sa \<and> P t \<and> I sa t \<and> A sa t \<longrightarrow> (\<forall>x\<in>fst (g (a s) sa). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst (g (a s) t). case x of (rvb, t') \<Rightarrow> rva = rvb \<and> I s' t' \<and> A s' t'); \<lbrakk>I s t; A s t; a s \<in> S; a t \<in> S\<rbrakk> \<Longrightarrow> a s = a t\<rbrakk> \<Longrightarrow> aa = aaa \<and> I b ba \<and> A b ba proof (prove)
goal (1 subgoal):
 1. \<And>s t aa b aaa ba. \<lbrakk>a t \<in> S; (aa, b) \<in> fst (g (a t) s); (aaa, ba) \<in> fst (g (a t) t); P s; P t; I s t; A s t; \<forall>s ta. P s \<and> P ta \<and> I s ta \<and> A s ta \<longrightarrow> (\<forall>x\<in>fst (g (a t) s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst (g (a t) ta). case x of (rvb, t') \<Rightarrow> rva = rvb \<and> I s' t' \<and> A s' t'); a s = a t\<rbrakk> \<Longrightarrow> aa = aaa \<and> I b ba \<and> A b ba proof (prove)
goal (1 subgoal):
 1. \<And>s t aa b aaa ba. \<lbrakk>a t \<in> S; (aa, b) \<in> fst (g (a t) s); (aaa, ba) \<in> fst (g (a t) t); P s; P t; I s t; A s t; a s = a t; \<forall>ta. P s \<and> P ta \<and> I s ta \<and> A s ta \<longrightarrow> (\<forall>x\<in>fst (g (a t) s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst (g (a t) ta). case x of (rvb, t') \<Rightarrow> rva = rvb \<and> I s' t' \<and> A s' t')\<rbrakk> \<Longrightarrow> aa = aaa \<and> I b ba \<and> A b ba proof (prove)
goal (1 subgoal):
 1. \<And>s t aa b aaa ba. \<lbrakk>a t \<in> S; (aa, b) \<in> fst (g (a t) s); (aaa, ba) \<in> fst (g (a t) t); P s; P t; I s t; A s t; a s = a t; P s \<and> P t \<and> I s t \<and> A s t \<longrightarrow> (\<forall>x\<in>fst (g (a t) s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst (g (a t) t). case x of (rvb, t') \<Rightarrow> rva = rvb \<and> I s' t' \<and> A s' t')\<rbrakk> \<Longrightarrow> aa = aaa \<and> I b ba \<and> A b ba proof (prove)
goal (1 subgoal):
 1. \<And>s t aa b aaa ba. \<lbrakk>a t \<in> S; (aa, b) \<in> fst (g (a t) s); (aaa, ba) \<in> fst (g (a t) t); P s; P t; I s t; A s t; a s = a t; \<forall>(rva, s')\<in>fst (g (a t) s). \<forall>(rvb, t')\<in>fst (g (a t) t). rva = rvb \<and> I s' t' \<and> A s' t'\<rbrakk> \<Longrightarrow> aa = aaa \<and> I b ba \<and> A b ba proof (prove)
goal:
No subgoals!