theory CSpace1_R

lemma pspace_relation_update_ctes:
  assumes ps: "pspace_relation s s'"
    and octe: "s' z = Some (KOCTE octe)"
    and  s'': "\<And>x. s'' x = (case (s x) of None \<Rightarrow> None | Some ko \<Rightarrow>
                    (case ko of CNode sz cs \<Rightarrow>
                          Some (CNode sz (\<lambda>y. if y \<in> dom cs \<and> cte_map (x, y) = z
                                              then Some cap else cs y))
                                    | _ \<Rightarrow> Some ko))"
     and rel: "cap_relation cap (cteCap cte')"
       shows  "pspace_relation s'' (s'(z \<mapsto> KOCTE cte'))" proof - have funny_update_no_dom:
    "\<And>fun P v. dom (\<lambda>y. if y \<in> dom fun \<and> P y then Some v else fun y)
      = dom fun" by (rule set_eqI, simp add: domIff) have funny_update_well_formed_cnode:
    "\<And>sz fun P v.
      well_formed_cnode_n sz (\<lambda>y. if y \<in> dom fun \<and> P y then Some v else fun y)
      = well_formed_cnode_n sz fun" by (simp add: well_formed_cnode_n_def funny_update_no_dom) have obj_relation_cuts1:
  "\<And>ko x. obj_relation_cuts (the (case ko of CNode sz cs \<Rightarrow>
                                       Some (CNode sz (\<lambda>y. if y \<in> dom cs \<and> cte_map (x, y) = z
                                                           then Some cap else cs y))
                                    | _ \<Rightarrow> Some ko)) x
             = obj_relation_cuts ko x" by (simp split: Structures_A.kernel_object.split
               add: funny_update_well_formed_cnode funny_update_no_dom) have domEq[simp]:
    "dom s'' = dom s" using s'' apply (intro set_eqI) apply (simp add: domIff split: option.split Structures_A.kernel_object.split) done have obj_relation_cuts2:
  "\<And>x. x \<in> dom s'' \<Longrightarrow> obj_relation_cuts (the (s'' x)) x = obj_relation_cuts (the (s x)) x" using s'' by (clarsimp simp add: obj_relation_cuts1 dest!: domD) show ?thesis using ps octe apply (clarsimp simp add: pspace_relation_def dom_fun_upd2
                    simp del: dom_fun_upd split del: if_split) apply (rule conjI) apply (erule subst[where t="dom s'"]) apply (simp add: pspace_dom_def obj_relation_cuts2) apply (simp add: obj_relation_cuts2) apply (rule ballI, drule(1) bspec)+ apply clarsimp apply (intro conjI impI) apply (simp add: s'') apply (rule obj_relation_cutsE, assumption+, simp_all split: if_split_asm)[1] apply (clarsimp simp: cte_relation_def rel) apply (rule obj_relation_cutsE, assumption+, simp_all add: s'') apply (clarsimp simp: cte_relation_def) apply (clarsimp simp: is_other_obj_relation_type other_obj_relation_def
                   split: Structures_A.kernel_object.split_asm) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pspace_relation s'' (s'(z \<mapsto> KOCTE cte')) proof (state)
goal (1 subgoal):
 1. pspace_relation s'' (s'(z \<mapsto> KOCTE cte')) proof (prove)
goal (1 subgoal):
 1. \<And>fun P v. dom (\<lambda>y. if y \<in> dom fun \<and> P y then Some v else fun y) = dom fun proof (state)
this:
dom (\<lambda>y. if y \<in> dom ?fun \<and> ?P y then Some ?v else ?fun y) = dom ?fun

goal (1 subgoal):
 1. pspace_relation s'' (s'(z \<mapsto> KOCTE cte')) proof (prove)
goal (1 subgoal):
 1. \<And>sz fun P v. well_formed_cnode_n sz (\<lambda>y. if y \<in> dom fun \<and> P y then Some v else fun y) = well_formed_cnode_n sz fun proof (state)
this:
well_formed_cnode_n ?sz1 (\<lambda>y. if y \<in> dom ?fun1 \<and> ?P1 y then Some ?v1 else ?fun1 y) = well_formed_cnode_n ?sz1 ?fun1

goal (1 subgoal):
 1. pspace_relation s'' (s'(z \<mapsto> KOCTE cte')) proof (prove)
goal (1 subgoal):
 1. \<And>ko x. obj_relation_cuts (the (case ko of CNode sz cs \<Rightarrow> Some (CNode sz (\<lambda>y. if y \<in> dom cs \<and> cte_map (x, y) = z then Some cap else cs y)) | _ \<Rightarrow> Some ko)) x = obj_relation_cuts ko x proof (state)
this:
obj_relation_cuts (the (case ?ko1 of CNode sz cs \<Rightarrow> Some (CNode sz (\<lambda>y. if y \<in> dom cs \<and> cte_map (?x1, y) = z then Some cap else cs y)) | _ \<Rightarrow> Some ?ko1)) ?x1 = obj_relation_cuts ?ko1 ?x1

goal (1 subgoal):
 1. pspace_relation s'' (s'(z \<mapsto> KOCTE cte')) proof (prove)
goal (1 subgoal):
 1. dom s'' = dom s proof (prove)
using this:
s'' ?x = (case s ?x of None \<Rightarrow> None | Some ko \<Rightarrow> case ko of CNode sz cs \<Rightarrow> Some (CNode sz (\<lambda>y. if y \<in> dom cs \<and> cte_map (?x, y) = z then Some cap else cs y)) | _ \<Rightarrow> Some ko)

goal (1 subgoal):
 1. dom s'' = dom s proof (prove)
goal (1 subgoal):
 1. \<And>x. (\<And>x. s'' x = (case s x of None \<Rightarrow> None | Some ko \<Rightarrow> case ko of CNode sz cs \<Rightarrow> Some (CNode sz (\<lambda>y. if y \<in> dom cs \<and> cte_map (x, y) = z then Some cap else cs y)) | _ \<Rightarrow> Some ko)) \<Longrightarrow> (x \<in> dom s'') = (x \<in> dom s) proof (prove)
goal:
No subgoals! proof (state)
this:
dom s'' = dom s

goal (1 subgoal):
 1. pspace_relation s'' (s'(z \<mapsto> KOCTE cte')) proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> dom s'' \<Longrightarrow> obj_relation_cuts (the (s'' x)) x = obj_relation_cuts (the (s x)) x proof (prove)
using this:
s'' ?x = (case s ?x of None \<Rightarrow> None | Some ko \<Rightarrow> case ko of CNode sz cs \<Rightarrow> Some (CNode sz (\<lambda>y. if y \<in> dom cs \<and> cte_map (?x, y) = z then Some cap else cs y)) | _ \<Rightarrow> Some ko)

goal (1 subgoal):
 1. \<And>x. x \<in> dom s'' \<Longrightarrow> obj_relation_cuts (the (s'' x)) x = obj_relation_cuts (the (s x)) x proof (state)
this:
?x1 \<in> dom s'' \<Longrightarrow> obj_relation_cuts (the (s'' ?x1)) ?x1 = obj_relation_cuts (the (s ?x1)) ?x1

goal (1 subgoal):
 1. pspace_relation s'' (s'(z \<mapsto> KOCTE cte')) proof (prove)
goal (1 subgoal):
 1. pspace_relation s'' (s'(z \<mapsto> KOCTE cte')) proof (prove)
using this:
pspace_relation s s'
s' z = Some (KOCTE octe)

goal (1 subgoal):
 1. pspace_relation s'' (s'(z \<mapsto> KOCTE cte')) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s' z = Some (KOCTE octe); pspace_dom s = dom s'; \<forall>x\<in>dom s. \<forall>xa\<in>obj_relation_cuts (the (s x)) x. case xa of (y, P) \<Rightarrow> P (the (s x)) (the (s' y))\<rbrakk> \<Longrightarrow> pspace_dom s'' = dom s' \<and> (\<forall>x\<in>dom s. \<forall>xa\<in>obj_relation_cuts (the (s'' x)) x. case xa of (y, P) \<Rightarrow> P (the (s'' x)) (the (if y = z then Some (KOCTE cte') else s' y))) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>s' z = Some (KOCTE octe); pspace_dom s = dom s'; \<forall>x\<in>dom s. \<forall>xa\<in>obj_relation_cuts (the (s x)) x. case xa of (y, P) \<Rightarrow> P (the (s x)) (the (s' y))\<rbrakk> \<Longrightarrow> pspace_dom s'' = dom s'
 2. \<lbrakk>s' z = Some (KOCTE octe); pspace_dom s = dom s'; \<forall>x\<in>dom s. \<forall>xa\<in>obj_relation_cuts (the (s x)) x. case xa of (y, P) \<Rightarrow> P (the (s x)) (the (s' y))\<rbrakk> \<Longrightarrow> \<forall>x\<in>dom s. \<forall>xa\<in>obj_relation_cuts (the (s'' x)) x. case xa of (y, P) \<Rightarrow> P (the (s'' x)) (the (if y = z then Some (KOCTE cte') else s' y)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>s' z = Some (KOCTE octe); \<forall>x\<in>dom s. \<forall>xa\<in>obj_relation_cuts (the (s x)) x. case xa of (y, P) \<Rightarrow> P (the (s x)) (the (s' y))\<rbrakk> \<Longrightarrow> pspace_dom s'' = pspace_dom s
 2. \<lbrakk>s' z = Some (KOCTE octe); pspace_dom s = dom s'; \<forall>x\<in>dom s. \<forall>xa\<in>obj_relation_cuts (the (s x)) x. case xa of (y, P) \<Rightarrow> P (the (s x)) (the (s' y))\<rbrakk> \<Longrightarrow> \<forall>x\<in>dom s. \<forall>xa\<in>obj_relation_cuts (the (s'' x)) x. case xa of (y, P) \<Rightarrow> P (the (s'' x)) (the (if y = z then Some (KOCTE cte') else s' y)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s' z = Some (KOCTE octe); pspace_dom s = dom s'; \<forall>x\<in>dom s. \<forall>xa\<in>obj_relation_cuts (the (s x)) x. case xa of (y, P) \<Rightarrow> P (the (s x)) (the (s' y))\<rbrakk> \<Longrightarrow> \<forall>x\<in>dom s. \<forall>xa\<in>obj_relation_cuts (the (s'' x)) x. case xa of (y, P) \<Rightarrow> P (the (s'' x)) (the (if y = z then Some (KOCTE cte') else s' y)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s' z = Some (KOCTE octe); pspace_dom s = dom s'; \<forall>x\<in>dom s. \<forall>xa\<in>obj_relation_cuts (the (s x)) x. case xa of (y, P) \<Rightarrow> P (the (s x)) (the (s' y))\<rbrakk> \<Longrightarrow> \<forall>x\<in>dom s. \<forall>xa\<in>obj_relation_cuts (the (s x)) x. case xa of (y, P) \<Rightarrow> P (the (s'' x)) (the (if y = z then Some (KOCTE cte') else s' y)) proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>s' z = Some (KOCTE octe); pspace_dom s = dom s'; x \<in> dom s; xa \<in> obj_relation_cuts (the (s x)) x; case xa of (y, P) \<Rightarrow> P (the (s x)) (the (s' y))\<rbrakk> \<Longrightarrow> case xa of (y, P) \<Rightarrow> P (the (s'' x)) (the (if y = z then Some (KOCTE cte') else s' y)) proof (prove)
goal (1 subgoal):
 1. \<And>x a b y. \<lbrakk>s' z = Some (KOCTE octe); pspace_dom s = dom s'; (a, b) \<in> obj_relation_cuts y x; b y (the (s' a)); s x = Some y\<rbrakk> \<Longrightarrow> (a = z \<longrightarrow> b (the (s'' x)) (KOCTE cte')) \<and> (a \<noteq> z \<longrightarrow> b (the (s'' x)) (the (s' a))) proof (prove)
goal (2 subgoals):
 1. \<And>x a b y. \<lbrakk>s' z = Some (KOCTE octe); pspace_dom s = dom s'; (a, b) \<in> obj_relation_cuts y x; b y (the (s' a)); s x = Some y; a = z\<rbrakk> \<Longrightarrow> b (the (s'' x)) (KOCTE cte')
 2. \<And>x a b y. \<lbrakk>s' z = Some (KOCTE octe); pspace_dom s = dom s'; (a, b) \<in> obj_relation_cuts y x; b y (the (s' a)); s x = Some y; a \<noteq> z\<rbrakk> \<Longrightarrow> b (the (s'' x)) (the (s' a)) proof (prove)
goal (2 subgoals):
 1. \<And>x a b y. \<lbrakk>s' z = Some (KOCTE octe); pspace_dom s = dom s'; (z, b) \<in> obj_relation_cuts y x; b y (KOCTE octe); s x = Some y; a = z\<rbrakk> \<Longrightarrow> b (the (case y of CNode sz cs \<Rightarrow> Some (CNode sz (\<lambda>y. if y \<in> dom cs \<and> cte_map (x, y) = z then Some cap else cs y)) | _ \<Rightarrow> Some y)) (KOCTE cte')
 2. \<And>x a b y. \<lbrakk>s' z = Some (KOCTE octe); pspace_dom s = dom s'; (a, b) \<in> obj_relation_cuts y x; b y (the (s' a)); s x = Some y; a \<noteq> z\<rbrakk> \<Longrightarrow> b (the (s'' x)) (the (s' a)) proof (prove)
goal (2 subgoals):
 1. \<And>x a b y sz cs za capa cte. \<lbrakk>s' (cte_map (x, za)) = Some (KOCTE cte); pspace_dom s = dom s'; \<exists>y. cte_map (x, za) = cte_map (x, y) \<and> b = cte_relation y \<and> y \<in> dom cs; b (CNode sz cs) (KOCTE cte); s x = Some (CNode sz cs); a = cte_map (x, za); y = CNode sz cs; well_formed_cnode_n sz cs; z = cte_map (x, za); octe = cte; cs za = Some capa; cap_relation capa (cteCap cte)\<rbrakk> \<Longrightarrow> b (CNode sz (\<lambda>y. if y \<in> dom cs \<and> cte_map (x, y) = cte_map (x, za) then Some cap else cs y)) (KOCTE cte')
 2. \<And>x a b y. \<lbrakk>s' z = Some (KOCTE octe); pspace_dom s = dom s'; (a, b) \<in> obj_relation_cuts y x; b y (the (s' a)); s x = Some y; a \<noteq> z\<rbrakk> \<Longrightarrow> b (the (s'' x)) (the (s' a)) proof (prove)
goal (1 subgoal):
 1. \<And>x a b y. \<lbrakk>s' z = Some (KOCTE octe); pspace_dom s = dom s'; (a, b) \<in> obj_relation_cuts y x; b y (the (s' a)); s x = Some y; a \<noteq> z\<rbrakk> \<Longrightarrow> b (the (s'' x)) (the (s' a)) proof (prove)
goal (2 subgoals):
 1. \<And>x a b y sz cs za capa cte. \<lbrakk>s' z = Some (KOCTE octe); pspace_dom s = dom s'; \<exists>y. cte_map (x, za) = cte_map (x, y) \<and> b = cte_relation y \<and> y \<in> dom cs; b (CNode sz cs) (KOCTE cte); s x = Some (CNode sz cs); cte_map (x, za) \<noteq> z; y = CNode sz cs; well_formed_cnode_n sz cs; a = cte_map (x, za); the (s' (cte_map (x, za))) = KOCTE cte; cs za = Some capa; cap_relation capa (cteCap cte)\<rbrakk> \<Longrightarrow> b (CNode sz (\<lambda>y. if y \<in> dom cs \<and> cte_map (x, y) = z then Some cap else cs y)) (KOCTE cte)
 2. \<And>x a b y. \<lbrakk>s' z = Some (KOCTE octe); pspace_dom s = dom s'; (x, b) \<in> obj_relation_cuts y x; b y (the (s' x)); s x = Some y; x \<noteq> z; a = x; other_obj_relation y (the (s' x)); is_other_obj_relation_type (a_type y)\<rbrakk> \<Longrightarrow> b (the (case y of CNode sz cs \<Rightarrow> Some (CNode sz (\<lambda>y. if y \<in> dom cs \<and> cte_map (x, y) = z then Some cap else cs y)) | _ \<Rightarrow> Some y)) (the (s' x)) proof (prove)
goal (1 subgoal):
 1. \<And>x a b y. \<lbrakk>s' z = Some (KOCTE octe); pspace_dom s = dom s'; (x, b) \<in> obj_relation_cuts y x; b y (the (s' x)); s x = Some y; x \<noteq> z; a = x; other_obj_relation y (the (s' x)); is_other_obj_relation_type (a_type y)\<rbrakk> \<Longrightarrow> b (the (case y of CNode sz cs \<Rightarrow> Some (CNode sz (\<lambda>y. if y \<in> dom cs \<and> cte_map (x, y) = z then Some cap else cs y)) | _ \<Rightarrow> Some y)) (the (s' x)) proof (prove)
goal:
No subgoals! proof (state)
this:
pspace_relation s'' (s'(z \<mapsto> KOCTE cte'))

goal:
No subgoals!