theory StateRelation

lemma pspace_relation_absD:
  "\<lbrakk> ab x = Some y; pspace_relation ab con \<rbrakk>
      \<Longrightarrow> \<forall>(x', P) \<in> obj_relation_cuts y x. \<exists>z. con x' = Some z \<and> P y z" apply (clarsimp simp add: pspace_relation_def) apply (drule bspec, erule domI) apply simp apply (drule(1) bspec) apply (subgoal_tac "a \<in> pspace_dom ab") apply clarsimp apply (simp(no_asm) add: pspace_dom_def) apply (rule rev_bexI, erule domI) apply (simp add: image_def rev_bexI) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ab x = Some y; pspace_relation ab con\<rbrakk> \<Longrightarrow> \<forall>(x', P)\<in>obj_relation_cuts y x. \<exists>z. con x' = Some z \<and> P y z proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>ab x = Some y; (a, b) \<in> obj_relation_cuts y x; pspace_dom ab = dom con; \<forall>x\<in>dom ab. \<forall>xa\<in>obj_relation_cuts (the (ab x)) x. case xa of (y, P) \<Rightarrow> P (the (ab x)) (the (con y))\<rbrakk> \<Longrightarrow> \<exists>z. con a = Some z \<and> b y z proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>ab x = Some y; (a, b) \<in> obj_relation_cuts y x; pspace_dom ab = dom con; \<forall>xa\<in>obj_relation_cuts (the (ab x)) x. case xa of (y, P) \<Rightarrow> P (the (ab x)) (the (con y))\<rbrakk> \<Longrightarrow> \<exists>z. con a = Some z \<and> b y z proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>ab x = Some y; (a, b) \<in> obj_relation_cuts y x; pspace_dom ab = dom con; \<forall>x\<in>obj_relation_cuts y x. case x of (ya, P) \<Rightarrow> P y (the (con ya))\<rbrakk> \<Longrightarrow> \<exists>z. con a = Some z \<and> b y z proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>ab x = Some y; (a, b) \<in> obj_relation_cuts y x; pspace_dom ab = dom con; case (a, b) of (ya, P) \<Rightarrow> P y (the (con ya))\<rbrakk> \<Longrightarrow> \<exists>z. con a = Some z \<and> b y z proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>ab x = Some y; (a, b) \<in> obj_relation_cuts y x; pspace_dom ab = dom con; case (a, b) of (ya, P) \<Rightarrow> P y (the (con ya)); a \<in> pspace_dom ab\<rbrakk> \<Longrightarrow> \<exists>z. con a = Some z \<and> b y z
 2. \<And>a b. \<lbrakk>ab x = Some y; (a, b) \<in> obj_relation_cuts y x; pspace_dom ab = dom con; case (a, b) of (ya, P) \<Rightarrow> P y (the (con ya))\<rbrakk> \<Longrightarrow> a \<in> pspace_dom ab proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>ab x = Some y; (a, b) \<in> obj_relation_cuts y x; pspace_dom ab = dom con; case (a, b) of (ya, P) \<Rightarrow> P y (the (con ya))\<rbrakk> \<Longrightarrow> a \<in> pspace_dom ab proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>ab x = Some y; (a, b) \<in> obj_relation_cuts y x; pspace_dom ab = dom con; case (a, b) of (ya, P) \<Rightarrow> P y (the (con ya))\<rbrakk> \<Longrightarrow> \<exists>x\<in>dom ab. a \<in> fst ` obj_relation_cuts (the (ab x)) x proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>ab x = Some y; (a, b) \<in> obj_relation_cuts y x; pspace_dom ab = dom con; case (a, b) of (ya, P) \<Rightarrow> P y (the (con ya))\<rbrakk> \<Longrightarrow> a \<in> fst ` obj_relation_cuts (the (ab x)) x proof (prove)
goal:
No subgoals!