theory CSpace_I

lemma distinct_zombies_copyMasterE:
  "\<lbrakk> distinct_zombies m; m x = Some cte;
          capClass (cteCap cte') = PhysicalClass
             \<Longrightarrow> capMasterCap (cteCap cte) = capMasterCap (cteCap cte');
          isZombie (cteCap cte') \<Longrightarrow> x = y \<rbrakk>
       \<Longrightarrow> distinct_zombies (m (y \<mapsto> cte'))" apply (erule(1) distinct_zombies_copyE, simp_all) apply (rule master_eqI, rule isCap_Master, simp) apply (drule_tac f=isUntypedCap in arg_cong) apply (simp add: isCap_Master) apply (drule_tac f=isArchPageCap in arg_cong) apply (simp add: isCap_Master) apply (rule master_eqI, rule capBits_Master, simp) apply clarsimp apply (drule_tac f=capClass in arg_cong, simp add: capClass_Master) apply (drule_tac f=capUntypedPtr in arg_cong, simp add: capUntyped_Master) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_zombies m; m x = Some cte; capClass (cteCap cte') = PhysicalClass \<Longrightarrow> capMasterCap (cteCap cte) = capMasterCap (cteCap cte'); isZombie (cteCap cte') \<Longrightarrow> x = y\<rbrakk> \<Longrightarrow> distinct_zombies (m(y \<mapsto> cte')) proof (prove)
goal (6 subgoals):
 1. \<lbrakk>m x = Some cte; capMasterCap (cteCap cte) = capMasterCap (cteCap cte'); isZombie (cteCap cte') \<Longrightarrow> x = y; capClass (cteCap cte') = PhysicalClass\<rbrakk> \<Longrightarrow> isZombie (cteCap cte) = isZombie (cteCap cte')
 2. \<lbrakk>m x = Some cte; capMasterCap (cteCap cte) = capMasterCap (cteCap cte'); isZombie (cteCap cte') \<Longrightarrow> x = y; capClass (cteCap cte') = PhysicalClass; isUntypedCap (cteCap cte)\<rbrakk> \<Longrightarrow> isUntypedCap (cteCap cte')
 3. \<lbrakk>m x = Some cte; capMasterCap (cteCap cte) = capMasterCap (cteCap cte'); isZombie (cteCap cte') \<Longrightarrow> x = y; capClass (cteCap cte') = PhysicalClass; isArchPageCap (cteCap cte)\<rbrakk> \<Longrightarrow> isArchPageCap (cteCap cte')
 4. \<lbrakk>m x = Some cte; capMasterCap (cteCap cte) = capMasterCap (cteCap cte'); isZombie (cteCap cte') \<Longrightarrow> x = y; capClass (cteCap cte') = PhysicalClass\<rbrakk> \<Longrightarrow> capBits (cteCap cte') = capBits (cteCap cte)
 5. \<lbrakk>m x = Some cte; capClass (cteCap cte') = PhysicalClass \<Longrightarrow> capMasterCap (cteCap cte) = capMasterCap (cteCap cte'); isZombie (cteCap cte') \<Longrightarrow> x = y\<rbrakk> \<Longrightarrow> capClass (cteCap cte') = PhysicalClass \<longrightarrow> capClass (cteCap cte) = PhysicalClass
 6. \<lbrakk>m x = Some cte; capMasterCap (cteCap cte) = capMasterCap (cteCap cte'); isZombie (cteCap cte') \<Longrightarrow> x = y; capClass (cteCap cte') = PhysicalClass\<rbrakk> \<Longrightarrow> global.capUntypedPtr (cteCap cte') = global.capUntypedPtr (cteCap cte) proof (prove)
goal (5 subgoals):
 1. \<lbrakk>m x = Some cte; capMasterCap (cteCap cte) = capMasterCap (cteCap cte'); isZombie (cteCap cte') \<Longrightarrow> x = y; capClass (cteCap cte') = PhysicalClass; isUntypedCap (cteCap cte)\<rbrakk> \<Longrightarrow> isUntypedCap (cteCap cte')
 2. \<lbrakk>m x = Some cte; capMasterCap (cteCap cte) = capMasterCap (cteCap cte'); isZombie (cteCap cte') \<Longrightarrow> x = y; capClass (cteCap cte') = PhysicalClass; isArchPageCap (cteCap cte)\<rbrakk> \<Longrightarrow> isArchPageCap (cteCap cte')
 3. \<lbrakk>m x = Some cte; capMasterCap (cteCap cte) = capMasterCap (cteCap cte'); isZombie (cteCap cte') \<Longrightarrow> x = y; capClass (cteCap cte') = PhysicalClass\<rbrakk> \<Longrightarrow> capBits (cteCap cte') = capBits (cteCap cte)
 4. \<lbrakk>m x = Some cte; capClass (cteCap cte') = PhysicalClass \<Longrightarrow> capMasterCap (cteCap cte) = capMasterCap (cteCap cte'); isZombie (cteCap cte') \<Longrightarrow> x = y\<rbrakk> \<Longrightarrow> capClass (cteCap cte') = PhysicalClass \<longrightarrow> capClass (cteCap cte) = PhysicalClass
 5. \<lbrakk>m x = Some cte; capMasterCap (cteCap cte) = capMasterCap (cteCap cte'); isZombie (cteCap cte') \<Longrightarrow> x = y; capClass (cteCap cte') = PhysicalClass\<rbrakk> \<Longrightarrow> global.capUntypedPtr (cteCap cte') = global.capUntypedPtr (cteCap cte) proof (prove)
goal (5 subgoals):
 1. \<lbrakk>m x = Some cte; isZombie (cteCap cte') \<Longrightarrow> x = y; capClass (cteCap cte') = PhysicalClass; isUntypedCap (cteCap cte); isUntypedCap (capMasterCap (cteCap cte)) = isUntypedCap (capMasterCap (cteCap cte'))\<rbrakk> \<Longrightarrow> isUntypedCap (cteCap cte')
 2. \<lbrakk>m x = Some cte; capMasterCap (cteCap cte) = capMasterCap (cteCap cte'); isZombie (cteCap cte') \<Longrightarrow> x = y; capClass (cteCap cte') = PhysicalClass; isArchPageCap (cteCap cte)\<rbrakk> \<Longrightarrow> isArchPageCap (cteCap cte')
 3. \<lbrakk>m x = Some cte; capMasterCap (cteCap cte) = capMasterCap (cteCap cte'); isZombie (cteCap cte') \<Longrightarrow> x = y; capClass (cteCap cte') = PhysicalClass\<rbrakk> \<Longrightarrow> capBits (cteCap cte') = capBits (cteCap cte)
 4. \<lbrakk>m x = Some cte; capClass (cteCap cte') = PhysicalClass \<Longrightarrow> capMasterCap (cteCap cte) = capMasterCap (cteCap cte'); isZombie (cteCap cte') \<Longrightarrow> x = y\<rbrakk> \<Longrightarrow> capClass (cteCap cte') = PhysicalClass \<longrightarrow> capClass (cteCap cte) = PhysicalClass
 5. \<lbrakk>m x = Some cte; capMasterCap (cteCap cte) = capMasterCap (cteCap cte'); isZombie (cteCap cte') \<Longrightarrow> x = y; capClass (cteCap cte') = PhysicalClass\<rbrakk> \<Longrightarrow> global.capUntypedPtr (cteCap cte') = global.capUntypedPtr (cteCap cte) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>m x = Some cte; capMasterCap (cteCap cte) = capMasterCap (cteCap cte'); isZombie (cteCap cte') \<Longrightarrow> x = y; capClass (cteCap cte') = PhysicalClass; isArchPageCap (cteCap cte)\<rbrakk> \<Longrightarrow> isArchPageCap (cteCap cte')
 2. \<lbrakk>m x = Some cte; capMasterCap (cteCap cte) = capMasterCap (cteCap cte'); isZombie (cteCap cte') \<Longrightarrow> x = y; capClass (cteCap cte') = PhysicalClass\<rbrakk> \<Longrightarrow> capBits (cteCap cte') = capBits (cteCap cte)
 3. \<lbrakk>m x = Some cte; capClass (cteCap cte') = PhysicalClass \<Longrightarrow> capMasterCap (cteCap cte) = capMasterCap (cteCap cte'); isZombie (cteCap cte') \<Longrightarrow> x = y\<rbrakk> \<Longrightarrow> capClass (cteCap cte') = PhysicalClass \<longrightarrow> capClass (cteCap cte) = PhysicalClass
 4. \<lbrakk>m x = Some cte; capMasterCap (cteCap cte) = capMasterCap (cteCap cte'); isZombie (cteCap cte') \<Longrightarrow> x = y; capClass (cteCap cte') = PhysicalClass\<rbrakk> \<Longrightarrow> global.capUntypedPtr (cteCap cte') = global.capUntypedPtr (cteCap cte) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>m x = Some cte; isZombie (cteCap cte') \<Longrightarrow> x = y; capClass (cteCap cte') = PhysicalClass; isArchPageCap (cteCap cte); isArchPageCap (capMasterCap (cteCap cte)) = isArchPageCap (capMasterCap (cteCap cte'))\<rbrakk> \<Longrightarrow> isArchPageCap (cteCap cte')
 2. \<lbrakk>m x = Some cte; capMasterCap (cteCap cte) = capMasterCap (cteCap cte'); isZombie (cteCap cte') \<Longrightarrow> x = y; capClass (cteCap cte') = PhysicalClass\<rbrakk> \<Longrightarrow> capBits (cteCap cte') = capBits (cteCap cte)
 3. \<lbrakk>m x = Some cte; capClass (cteCap cte') = PhysicalClass \<Longrightarrow> capMasterCap (cteCap cte) = capMasterCap (cteCap cte'); isZombie (cteCap cte') \<Longrightarrow> x = y\<rbrakk> \<Longrightarrow> capClass (cteCap cte') = PhysicalClass \<longrightarrow> capClass (cteCap cte) = PhysicalClass
 4. \<lbrakk>m x = Some cte; capMasterCap (cteCap cte) = capMasterCap (cteCap cte'); isZombie (cteCap cte') \<Longrightarrow> x = y; capClass (cteCap cte') = PhysicalClass\<rbrakk> \<Longrightarrow> global.capUntypedPtr (cteCap cte') = global.capUntypedPtr (cteCap cte) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>m x = Some cte; capMasterCap (cteCap cte) = capMasterCap (cteCap cte'); isZombie (cteCap cte') \<Longrightarrow> x = y; capClass (cteCap cte') = PhysicalClass\<rbrakk> \<Longrightarrow> capBits (cteCap cte') = capBits (cteCap cte)
 2. \<lbrakk>m x = Some cte; capClass (cteCap cte') = PhysicalClass \<Longrightarrow> capMasterCap (cteCap cte) = capMasterCap (cteCap cte'); isZombie (cteCap cte') \<Longrightarrow> x = y\<rbrakk> \<Longrightarrow> capClass (cteCap cte') = PhysicalClass \<longrightarrow> capClass (cteCap cte) = PhysicalClass
 3. \<lbrakk>m x = Some cte; capMasterCap (cteCap cte) = capMasterCap (cteCap cte'); isZombie (cteCap cte') \<Longrightarrow> x = y; capClass (cteCap cte') = PhysicalClass\<rbrakk> \<Longrightarrow> global.capUntypedPtr (cteCap cte') = global.capUntypedPtr (cteCap cte) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m x = Some cte; capClass (cteCap cte') = PhysicalClass \<Longrightarrow> capMasterCap (cteCap cte) = capMasterCap (cteCap cte'); isZombie (cteCap cte') \<Longrightarrow> x = y\<rbrakk> \<Longrightarrow> capClass (cteCap cte') = PhysicalClass \<longrightarrow> capClass (cteCap cte) = PhysicalClass
 2. \<lbrakk>m x = Some cte; capMasterCap (cteCap cte) = capMasterCap (cteCap cte'); isZombie (cteCap cte') \<Longrightarrow> x = y; capClass (cteCap cte') = PhysicalClass\<rbrakk> \<Longrightarrow> global.capUntypedPtr (cteCap cte') = global.capUntypedPtr (cteCap cte) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m x = Some cte; capMasterCap (cteCap cte) = capMasterCap (cteCap cte'); isZombie (cteCap cte') \<Longrightarrow> x = y; capClass (cteCap cte') = PhysicalClass\<rbrakk> \<Longrightarrow> capClass (cteCap cte) = PhysicalClass
 2. \<lbrakk>m x = Some cte; capMasterCap (cteCap cte) = capMasterCap (cteCap cte'); isZombie (cteCap cte') \<Longrightarrow> x = y; capClass (cteCap cte') = PhysicalClass\<rbrakk> \<Longrightarrow> global.capUntypedPtr (cteCap cte') = global.capUntypedPtr (cteCap cte) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m x = Some cte; capMasterCap (cteCap cte) = capMasterCap (cteCap cte'); isZombie (cteCap cte') \<Longrightarrow> x = y; capClass (cteCap cte') = PhysicalClass\<rbrakk> \<Longrightarrow> global.capUntypedPtr (cteCap cte') = global.capUntypedPtr (cteCap cte) proof (prove)
goal:
No subgoals!