theory Retype_R

lemma pspace_dom_upd:
  assumes      orth: "set as \<inter> dom ps = {}"
  shows "pspace_dom (foldr (\<lambda>p ps. ps(p \<mapsto> ko)) as ps) =
       pspace_dom ps \<union> (\<Union>x \<in> set as. fst ` obj_relation_cuts ko x)" using orth apply (subst foldr_upd_app_if) apply (rule set_eqI, simp add: pspace_dom_def) apply (rule iffI) apply (clarsimp split: if_split_asm) apply (rule rev_bexI, erule domI) apply (fastforce simp: image_def) apply (erule disjE) apply clarsimp apply (rule rev_bexI) apply (clarsimp simp: domIff) apply (erule exI) apply clarsimp apply (intro conjI impI) apply (drule equals0D, erule notE, erule IntI, erule domI) apply (fastforce simp: image_def) apply clarsimp apply (rule rev_bexI) apply (clarsimp simp: domIff) apply (erule(1) notE) apply clarsimp apply (fastforce simp: image_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pspace_dom (foldr (\<lambda>p ps. ps(p \<mapsto> ko)) as ps) = pspace_dom ps \<union> (\<Union>x\<in>set as. fst ` obj_relation_cuts ko x) proof (prove)
using this:
set as \<inter> dom ps = {}

goal (1 subgoal):
 1. pspace_dom (foldr (\<lambda>p ps. ps(p \<mapsto> ko)) as ps) = pspace_dom ps \<union> (\<Union>x\<in>set as. fst ` obj_relation_cuts ko x) proof (prove)
goal (1 subgoal):
 1. set as \<inter> dom ps = {} \<Longrightarrow> pspace_dom (\<lambda>x. if x \<in> set as then Some ko else ps x) = pspace_dom ps \<union> (\<Union>x\<in>set as. fst ` obj_relation_cuts ko x) proof (prove)
goal (1 subgoal):
 1. \<And>x. set as \<inter> dom ps = {} \<Longrightarrow> (\<exists>xa\<in>dom (\<lambda>x. if x \<in> set as then Some ko else ps x). (xa \<in> set as \<longrightarrow> x \<in> fst ` obj_relation_cuts ko xa) \<and> (xa \<notin> set as \<longrightarrow> x \<in> fst ` obj_relation_cuts (the (ps xa)) xa)) = ((\<exists>xa\<in>dom ps. x \<in> fst ` obj_relation_cuts (the (ps xa)) xa) \<or> (\<exists>xa\<in>set as. x \<in> fst ` obj_relation_cuts ko xa)) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>set as \<inter> dom ps = {}; \<exists>xa\<in>dom (\<lambda>x. if x \<in> set as then Some ko else ps x). (xa \<in> set as \<longrightarrow> x \<in> fst ` obj_relation_cuts ko xa) \<and> (xa \<notin> set as \<longrightarrow> x \<in> fst ` obj_relation_cuts (the (ps xa)) xa)\<rbrakk> \<Longrightarrow> (\<exists>xa\<in>dom ps. x \<in> fst ` obj_relation_cuts (the (ps xa)) xa) \<or> (\<exists>xa\<in>set as. x \<in> fst ` obj_relation_cuts ko xa)
 2. \<And>x. \<lbrakk>set as \<inter> dom ps = {}; (\<exists>xa\<in>dom ps. x \<in> fst ` obj_relation_cuts (the (ps xa)) xa) \<or> (\<exists>xa\<in>set as. x \<in> fst ` obj_relation_cuts ko xa)\<rbrakk> \<Longrightarrow> \<exists>xa\<in>dom (\<lambda>x. if x \<in> set as then Some ko else ps x). (xa \<in> set as \<longrightarrow> x \<in> fst ` obj_relation_cuts ko xa) \<and> (xa \<notin> set as \<longrightarrow> x \<in> fst ` obj_relation_cuts (the (ps xa)) xa) proof (prove)
goal (2 subgoals):
 1. \<And>xa y a b. \<lbrakk>set as \<inter> dom ps = {}; ps xa = Some y; xa \<notin> set as; \<forall>x\<in>set as. a \<notin> fst ` obj_relation_cuts ko x; (a, b) \<in> obj_relation_cuts y xa\<rbrakk> \<Longrightarrow> \<exists>x\<in>dom ps. a \<in> fst ` obj_relation_cuts (the (ps x)) x
 2. \<And>x. \<lbrakk>set as \<inter> dom ps = {}; (\<exists>xa\<in>dom ps. x \<in> fst ` obj_relation_cuts (the (ps xa)) xa) \<or> (\<exists>xa\<in>set as. x \<in> fst ` obj_relation_cuts ko xa)\<rbrakk> \<Longrightarrow> \<exists>xa\<in>dom (\<lambda>x. if x \<in> set as then Some ko else ps x). (xa \<in> set as \<longrightarrow> x \<in> fst ` obj_relation_cuts ko xa) \<and> (xa \<notin> set as \<longrightarrow> x \<in> fst ` obj_relation_cuts (the (ps xa)) xa) proof (prove)
goal (2 subgoals):
 1. \<And>xa y a b. \<lbrakk>set as \<inter> dom ps = {}; ps xa = Some y; xa \<notin> set as; \<forall>x\<in>set as. a \<notin> fst ` obj_relation_cuts ko x; (a, b) \<in> obj_relation_cuts y xa\<rbrakk> \<Longrightarrow> a \<in> fst ` obj_relation_cuts (the (ps xa)) xa
 2. \<And>x. \<lbrakk>set as \<inter> dom ps = {}; (\<exists>xa\<in>dom ps. x \<in> fst ` obj_relation_cuts (the (ps xa)) xa) \<or> (\<exists>xa\<in>set as. x \<in> fst ` obj_relation_cuts ko xa)\<rbrakk> \<Longrightarrow> \<exists>xa\<in>dom (\<lambda>x. if x \<in> set as then Some ko else ps x). (xa \<in> set as \<longrightarrow> x \<in> fst ` obj_relation_cuts ko xa) \<and> (xa \<notin> set as \<longrightarrow> x \<in> fst ` obj_relation_cuts (the (ps xa)) xa) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>set as \<inter> dom ps = {}; (\<exists>xa\<in>dom ps. x \<in> fst ` obj_relation_cuts (the (ps xa)) xa) \<or> (\<exists>xa\<in>set as. x \<in> fst ` obj_relation_cuts ko xa)\<rbrakk> \<Longrightarrow> \<exists>xa\<in>dom (\<lambda>x. if x \<in> set as then Some ko else ps x). (xa \<in> set as \<longrightarrow> x \<in> fst ` obj_relation_cuts ko xa) \<and> (xa \<notin> set as \<longrightarrow> x \<in> fst ` obj_relation_cuts (the (ps xa)) xa) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>set as \<inter> dom ps = {}; \<exists>xa\<in>dom ps. x \<in> fst ` obj_relation_cuts (the (ps xa)) xa\<rbrakk> \<Longrightarrow> \<exists>xa\<in>dom (\<lambda>x. if x \<in> set as then Some ko else ps x). (xa \<in> set as \<longrightarrow> x \<in> fst ` obj_relation_cuts ko xa) \<and> (xa \<notin> set as \<longrightarrow> x \<in> fst ` obj_relation_cuts (the (ps xa)) xa)
 2. \<And>x. \<lbrakk>set as \<inter> dom ps = {}; \<exists>xa\<in>set as. x \<in> fst ` obj_relation_cuts ko xa\<rbrakk> \<Longrightarrow> \<exists>xa\<in>dom (\<lambda>x. if x \<in> set as then Some ko else ps x). (xa \<in> set as \<longrightarrow> x \<in> fst ` obj_relation_cuts ko xa) \<and> (xa \<notin> set as \<longrightarrow> x \<in> fst ` obj_relation_cuts (the (ps xa)) xa) proof (prove)
goal (2 subgoals):
 1. \<And>xa a b y. \<lbrakk>set as \<inter> dom ps = {}; (a, b) \<in> obj_relation_cuts y xa; ps xa = Some y\<rbrakk> \<Longrightarrow> \<exists>x\<in>dom (\<lambda>x. if x \<in> set as then Some ko else ps x). (x \<in> set as \<longrightarrow> a \<in> fst ` obj_relation_cuts ko x) \<and> (x \<notin> set as \<longrightarrow> a \<in> fst ` obj_relation_cuts (the (ps x)) x)
 2. \<And>x. \<lbrakk>set as \<inter> dom ps = {}; \<exists>xa\<in>set as. x \<in> fst ` obj_relation_cuts ko xa\<rbrakk> \<Longrightarrow> \<exists>xa\<in>dom (\<lambda>x. if x \<in> set as then Some ko else ps x). (xa \<in> set as \<longrightarrow> x \<in> fst ` obj_relation_cuts ko xa) \<and> (xa \<notin> set as \<longrightarrow> x \<in> fst ` obj_relation_cuts (the (ps xa)) xa) proof (prove)
goal (3 subgoals):
 1. \<And>xa a b y. \<lbrakk>set as \<inter> dom ps = {}; (a, b) \<in> obj_relation_cuts y xa; ps xa = Some y\<rbrakk> \<Longrightarrow> ?x61 xa a b y \<in> dom (\<lambda>x. if x \<in> set as then Some ko else ps x)
 2. \<And>xa a b y. \<lbrakk>set as \<inter> dom ps = {}; (a, b) \<in> obj_relation_cuts y xa; ps xa = Some y\<rbrakk> \<Longrightarrow> (?x61 xa a b y \<in> set as \<longrightarrow> a \<in> fst ` obj_relation_cuts ko (?x61 xa a b y)) \<and> (?x61 xa a b y \<notin> set as \<longrightarrow> a \<in> fst ` obj_relation_cuts (the (ps (?x61 xa a b y))) (?x61 xa a b y))
 3. \<And>x. \<lbrakk>set as \<inter> dom ps = {}; \<exists>xa\<in>set as. x \<in> fst ` obj_relation_cuts ko xa\<rbrakk> \<Longrightarrow> \<exists>xa\<in>dom (\<lambda>x. if x \<in> set as then Some ko else ps x). (xa \<in> set as \<longrightarrow> x \<in> fst ` obj_relation_cuts ko xa) \<and> (xa \<notin> set as \<longrightarrow> x \<in> fst ` obj_relation_cuts (the (ps xa)) xa) proof (prove)
goal (3 subgoals):
 1. \<And>xa a b y. \<lbrakk>set as \<inter> dom ps = {}; (a, b) \<in> obj_relation_cuts y xa; ps xa = Some y; ?x69 xa a b y \<notin> set as\<rbrakk> \<Longrightarrow> \<exists>ya. ps (?x69 xa a b y) = Some ya
 2. \<And>xa a b y. \<lbrakk>set as \<inter> dom ps = {}; (a, b) \<in> obj_relation_cuts y xa; ps xa = Some y\<rbrakk> \<Longrightarrow> (?x69 xa a b y \<in> set as \<longrightarrow> a \<in> fst ` obj_relation_cuts ko (?x69 xa a b y)) \<and> (?x69 xa a b y \<notin> set as \<longrightarrow> a \<in> fst ` obj_relation_cuts (the (ps (?x69 xa a b y))) (?x69 xa a b y))
 3. \<And>x. \<lbrakk>set as \<inter> dom ps = {}; \<exists>xa\<in>set as. x \<in> fst ` obj_relation_cuts ko xa\<rbrakk> \<Longrightarrow> \<exists>xa\<in>dom (\<lambda>x. if x \<in> set as then Some ko else ps x). (xa \<in> set as \<longrightarrow> x \<in> fst ` obj_relation_cuts ko xa) \<and> (xa \<notin> set as \<longrightarrow> x \<in> fst ` obj_relation_cuts (the (ps xa)) xa) proof (prove)
goal (2 subgoals):
 1. \<And>xa a b y. \<lbrakk>set as \<inter> dom ps = {}; (a, b) \<in> obj_relation_cuts y xa; ps xa = Some y\<rbrakk> \<Longrightarrow> (xa \<in> set as \<longrightarrow> a \<in> fst ` obj_relation_cuts ko xa) \<and> (xa \<notin> set as \<longrightarrow> a \<in> fst ` obj_relation_cuts (the (ps xa)) xa)
 2. \<And>x. \<lbrakk>set as \<inter> dom ps = {}; \<exists>xa\<in>set as. x \<in> fst ` obj_relation_cuts ko xa\<rbrakk> \<Longrightarrow> \<exists>xa\<in>dom (\<lambda>x. if x \<in> set as then Some ko else ps x). (xa \<in> set as \<longrightarrow> x \<in> fst ` obj_relation_cuts ko xa) \<and> (xa \<notin> set as \<longrightarrow> x \<in> fst ` obj_relation_cuts (the (ps xa)) xa) proof (prove)
goal (2 subgoals):
 1. \<And>xa a b y. \<lbrakk>set as \<inter> dom ps = {}; (a, b) \<in> obj_relation_cuts y xa; ps xa = Some y\<rbrakk> \<Longrightarrow> (xa \<in> set as \<longrightarrow> a \<in> fst ` obj_relation_cuts ko xa) \<and> (xa \<notin> set as \<longrightarrow> a \<in> fst ` obj_relation_cuts y xa)
 2. \<And>x. \<lbrakk>set as \<inter> dom ps = {}; \<exists>xa\<in>set as. x \<in> fst ` obj_relation_cuts ko xa\<rbrakk> \<Longrightarrow> \<exists>xa\<in>dom (\<lambda>x. if x \<in> set as then Some ko else ps x). (xa \<in> set as \<longrightarrow> x \<in> fst ` obj_relation_cuts ko xa) \<and> (xa \<notin> set as \<longrightarrow> x \<in> fst ` obj_relation_cuts (the (ps xa)) xa) proof (prove)
goal (3 subgoals):
 1. \<And>xa a b y. \<lbrakk>set as \<inter> dom ps = {}; (a, b) \<in> obj_relation_cuts y xa; ps xa = Some y; xa \<in> set as\<rbrakk> \<Longrightarrow> a \<in> fst ` obj_relation_cuts ko xa
 2. \<And>xa a b y. \<lbrakk>set as \<inter> dom ps = {}; (a, b) \<in> obj_relation_cuts y xa; ps xa = Some y; xa \<notin> set as\<rbrakk> \<Longrightarrow> a \<in> fst ` obj_relation_cuts y xa
 3. \<And>x. \<lbrakk>set as \<inter> dom ps = {}; \<exists>xa\<in>set as. x \<in> fst ` obj_relation_cuts ko xa\<rbrakk> \<Longrightarrow> \<exists>xa\<in>dom (\<lambda>x. if x \<in> set as then Some ko else ps x). (xa \<in> set as \<longrightarrow> x \<in> fst ` obj_relation_cuts ko xa) \<and> (xa \<notin> set as \<longrightarrow> x \<in> fst ` obj_relation_cuts (the (ps xa)) xa) proof (prove)
goal (2 subgoals):
 1. \<And>xa a b y. \<lbrakk>set as \<inter> dom ps = {}; (a, b) \<in> obj_relation_cuts y xa; ps xa = Some y; xa \<notin> set as\<rbrakk> \<Longrightarrow> a \<in> fst ` obj_relation_cuts y xa
 2. \<And>x. \<lbrakk>set as \<inter> dom ps = {}; \<exists>xa\<in>set as. x \<in> fst ` obj_relation_cuts ko xa\<rbrakk> \<Longrightarrow> \<exists>xa\<in>dom (\<lambda>x. if x \<in> set as then Some ko else ps x). (xa \<in> set as \<longrightarrow> x \<in> fst ` obj_relation_cuts ko xa) \<and> (xa \<notin> set as \<longrightarrow> x \<in> fst ` obj_relation_cuts (the (ps xa)) xa) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>set as \<inter> dom ps = {}; \<exists>xa\<in>set as. x \<in> fst ` obj_relation_cuts ko xa\<rbrakk> \<Longrightarrow> \<exists>xa\<in>dom (\<lambda>x. if x \<in> set as then Some ko else ps x). (xa \<in> set as \<longrightarrow> x \<in> fst ` obj_relation_cuts ko xa) \<and> (xa \<notin> set as \<longrightarrow> x \<in> fst ` obj_relation_cuts (the (ps xa)) xa) proof (prove)
goal (1 subgoal):
 1. \<And>xa a b. \<lbrakk>set as \<inter> dom ps = {}; xa \<in> set as; (a, b) \<in> obj_relation_cuts ko xa\<rbrakk> \<Longrightarrow> \<exists>x\<in>dom (\<lambda>x. if x \<in> set as then Some ko else ps x). (x \<in> set as \<longrightarrow> a \<in> fst ` obj_relation_cuts ko x) \<and> (x \<notin> set as \<longrightarrow> a \<in> fst ` obj_relation_cuts (the (ps x)) x) proof (prove)
goal (2 subgoals):
 1. \<And>xa a b. \<lbrakk>set as \<inter> dom ps = {}; xa \<in> set as; (a, b) \<in> obj_relation_cuts ko xa\<rbrakk> \<Longrightarrow> ?x102 xa a b \<in> dom (\<lambda>x. if x \<in> set as then Some ko else ps x)
 2. \<And>xa a b. \<lbrakk>set as \<inter> dom ps = {}; xa \<in> set as; (a, b) \<in> obj_relation_cuts ko xa\<rbrakk> \<Longrightarrow> (?x102 xa a b \<in> set as \<longrightarrow> a \<in> fst ` obj_relation_cuts ko (?x102 xa a b)) \<and> (?x102 xa a b \<notin> set as \<longrightarrow> a \<in> fst ` obj_relation_cuts (the (ps (?x102 xa a b))) (?x102 xa a b)) proof (prove)
goal (2 subgoals):
 1. \<And>xa a b. \<lbrakk>set as \<inter> dom ps = {}; xa \<in> set as; (a, b) \<in> obj_relation_cuts ko xa; ?x110 xa a b \<notin> set as\<rbrakk> \<Longrightarrow> \<exists>y. ps (?x110 xa a b) = Some y
 2. \<And>xa a b. \<lbrakk>set as \<inter> dom ps = {}; xa \<in> set as; (a, b) \<in> obj_relation_cuts ko xa\<rbrakk> \<Longrightarrow> (?x110 xa a b \<in> set as \<longrightarrow> a \<in> fst ` obj_relation_cuts ko (?x110 xa a b)) \<and> (?x110 xa a b \<notin> set as \<longrightarrow> a \<in> fst ` obj_relation_cuts (the (ps (?x110 xa a b))) (?x110 xa a b)) proof (prove)
goal (1 subgoal):
 1. \<And>xa a b. \<lbrakk>set as \<inter> dom ps = {}; xa \<in> set as; (a, b) \<in> obj_relation_cuts ko xa\<rbrakk> \<Longrightarrow> (xa \<in> set as \<longrightarrow> a \<in> fst ` obj_relation_cuts ko xa) \<and> (xa \<notin> set as \<longrightarrow> a \<in> fst ` obj_relation_cuts (the (ps xa)) xa) proof (prove)
goal (1 subgoal):
 1. \<And>xa a b. \<lbrakk>set as \<inter> dom ps = {}; xa \<in> set as; (a, b) \<in> obj_relation_cuts ko xa\<rbrakk> \<Longrightarrow> a \<in> fst ` obj_relation_cuts ko xa proof (prove)
goal:
No subgoals!