theory UserOp_IF

lemma spec_equiv_valid_inv_gets:
  assumes proj_retain: "\<And>t. \<lbrakk> P st; P t; I st t; A st t \<rbrakk> \<Longrightarrow> proj (f st) = proj (f t)"
  and spec_eqv_valid: "spec_equiv_valid_inv st I A P (g (proj (f st)))"
  shows "spec_equiv_valid_inv st I A P (do r \<leftarrow> gets f; g (proj r) od)" apply (clarsimp simp: spec_equiv_valid_def equiv_valid_2_def gets_def get_def bind_def return_def) apply (frule (3) proj_retain) apply (cut_tac spec_eqv_valid) apply (clarsimp simp: spec_equiv_valid_def equiv_valid_2_def gets_def get_def bind_def return_def) apply (drule spec)+ apply (erule impE) apply fastforce apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. spec_equiv_valid_inv st I A P (do r <- gets f;
g (proj r)
od) proof (prove)
goal (1 subgoal):
 1. \<And>t a b aa ba. \<lbrakk>(a, b) \<in> fst (g (proj (f st)) st); (aa, ba) \<in> fst (g (proj (f t)) t); P st; P t; I st t; A st t\<rbrakk> \<Longrightarrow> a = aa \<and> I b ba \<and> A b ba proof (prove)
goal (1 subgoal):
 1. \<And>t a b aa ba. \<lbrakk>(a, b) \<in> fst (g (proj (f st)) st); (aa, ba) \<in> fst (g (proj (f t)) t); P st; P t; I st t; A st t; proj (f st) = proj (f t)\<rbrakk> \<Longrightarrow> a = aa \<and> I b ba \<and> A b ba proof (prove)
goal (1 subgoal):
 1. \<And>t a b aa ba. \<lbrakk>(a, b) \<in> fst (g (proj (f st)) st); (aa, ba) \<in> fst (g (proj (f t)) t); P st; P t; I st t; A st t; proj (f st) = proj (f t); spec_equiv_valid_inv st I A P (g (proj (f st)))\<rbrakk> \<Longrightarrow> a = aa \<and> I b ba \<and> A b ba proof (prove)
goal (1 subgoal):
 1. \<And>t a b aa ba. \<lbrakk>(a, b) \<in> fst (g (proj (f t)) st); (aa, ba) \<in> fst (g (proj (f t)) t); P st; P t; I st t; A st t; proj (f st) = proj (f t); \<forall>ta. P ta \<and> I st ta \<and> A st ta \<longrightarrow> (\<forall>x\<in>fst (g (proj (f t)) st). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst (g (proj (f t)) ta). case x of (rvb, t') \<Rightarrow> rva = rvb \<and> I s' t' \<and> A s' t')\<rbrakk> \<Longrightarrow> a = aa \<and> I b ba \<and> A b ba proof (prove)
goal (1 subgoal):
 1. \<And>t a b aa ba. \<lbrakk>(a, b) \<in> fst (g (proj (f t)) st); (aa, ba) \<in> fst (g (proj (f t)) t); P st; P t; I st t; A st t; proj (f st) = proj (f t); P (?t35 t a b aa ba) \<and> I st (?t35 t a b aa ba) \<and> A st (?t35 t a b aa ba) \<longrightarrow> (\<forall>x\<in>fst (g (proj (f t)) st). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst (g (proj (f t)) (?t35 t a b aa ba)). case x of (rvb, t') \<Rightarrow> rva = rvb \<and> I s' t' \<and> A s' t')\<rbrakk> \<Longrightarrow> a = aa \<and> I b ba \<and> A b ba proof (prove)
goal (2 subgoals):
 1. \<And>t a b aa ba. \<lbrakk>(a, b) \<in> fst (g (proj (f t)) st); (aa, ba) \<in> fst (g (proj (f t)) t); P st; P t; I st t; A st t; proj (f st) = proj (f t)\<rbrakk> \<Longrightarrow> P (?t35 t a b aa ba) \<and> I st (?t35 t a b aa ba) \<and> A st (?t35 t a b aa ba)
 2. \<And>t a b aa ba. \<lbrakk>(a, b) \<in> fst (g (proj (f t)) st); (aa, ba) \<in> fst (g (proj (f t)) t); P st; P t; I st t; A st t; proj (f st) = proj (f t); \<forall>x\<in>fst (g (proj (f t)) st). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst (g (proj (f t)) (?t35 t a b aa ba)). case x of (rvb, t') \<Rightarrow> rva = rvb \<and> I s' t' \<and> A s' t'\<rbrakk> \<Longrightarrow> a = aa \<and> I b ba \<and> A b ba proof (prove)
goal (1 subgoal):
 1. \<And>t a b aa ba. \<lbrakk>(a, b) \<in> fst (g (proj (f t)) st); (aa, ba) \<in> fst (g (proj (f t)) t); P st; P t; I st t; A st t; proj (f st) = proj (f t); \<forall>x\<in>fst (g (proj (f t)) st). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst (g (proj (f t)) t). case x of (rvb, t') \<Rightarrow> rva = rvb \<and> I s' t' \<and> A s' t'\<rbrakk> \<Longrightarrow> a = aa \<and> I b ba \<and> A b ba proof (prove)
goal:
No subgoals!