theory SR_lemmas_C

lemma cap_get_tag_ZombieCap:
  assumes cr: "ccap_relation cap cap'"
  shows "(cap_get_tag cap' = scast cap_zombie_cap) =
  (cap =
   (if isZombieTCB_C (capZombieType_CL (cap_zombie_cap_lift cap'))
     then capability.Zombie (capZombieID_CL (cap_zombie_cap_lift cap') && ~~ mask 5) ZombieTCB
           (unat (capZombieID_CL (cap_zombie_cap_lift cap') && mask 5))
     else let radix = unat (capZombieType_CL (cap_zombie_cap_lift cap'))
          in capability.Zombie (capZombieID_CL (cap_zombie_cap_lift cap') && ~~ mask (radix + 1))
              (ZombieCNode radix)
              (unat (capZombieID_CL (cap_zombie_cap_lift cap') && mask (radix + 1)))))" using cr apply - apply (rule iffI) apply (erule ccap_relationE) apply (clarsimp simp add: cap_lifts cap_to_H_def) apply (simp add: cap_get_tag_isCap isCap_simps Let_def
            split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap) = (cap = (if isZombieTCB_C (capZombieType_CL (cap_zombie_cap_lift cap')) then capability.Zombie (capZombieID_CL (cap_zombie_cap_lift cap') && ~~ mask 5) ZombieTCB (unat (capZombieID_CL (cap_zombie_cap_lift cap') && mask 5)) else let radix = unat (capZombieType_CL (cap_zombie_cap_lift cap')) in capability.Zombie (capZombieID_CL (cap_zombie_cap_lift cap') && ~~ mask (radix + 1)) (ZombieCNode radix) (unat (capZombieID_CL (cap_zombie_cap_lift cap') && mask (radix + 1))))) proof (prove)
using this:
ccap_relation cap cap'

goal (1 subgoal):
 1. (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap) = (cap = (if isZombieTCB_C (capZombieType_CL (cap_zombie_cap_lift cap')) then capability.Zombie (capZombieID_CL (cap_zombie_cap_lift cap') && ~~ mask 5) ZombieTCB (unat (capZombieID_CL (cap_zombie_cap_lift cap') && mask 5)) else let radix = unat (capZombieType_CL (cap_zombie_cap_lift cap')) in capability.Zombie (capZombieID_CL (cap_zombie_cap_lift cap') && ~~ mask (radix + 1)) (ZombieCNode radix) (unat (capZombieID_CL (cap_zombie_cap_lift cap') && mask (radix + 1))))) proof (prove)
goal (1 subgoal):
 1. ccap_relation cap cap' \<Longrightarrow> (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap) = (cap = (if isZombieTCB_C (capZombieType_CL (cap_zombie_cap_lift cap')) then capability.Zombie (capZombieID_CL (cap_zombie_cap_lift cap') && ~~ mask 5) ZombieTCB (unat (capZombieID_CL (cap_zombie_cap_lift cap') && mask 5)) else let radix = unat (capZombieType_CL (cap_zombie_cap_lift cap')) in capability.Zombie (capZombieID_CL (cap_zombie_cap_lift cap') && ~~ mask (radix + 1)) (ZombieCNode radix) (unat (capZombieID_CL (cap_zombie_cap_lift cap') && mask (radix + 1))))) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ccap_relation cap cap'; cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap\<rbrakk> \<Longrightarrow> cap = (if isZombieTCB_C (capZombieType_CL (cap_zombie_cap_lift cap')) then capability.Zombie (capZombieID_CL (cap_zombie_cap_lift cap') && ~~ mask 5) ZombieTCB (unat (capZombieID_CL (cap_zombie_cap_lift cap') && mask 5)) else let radix = unat (capZombieType_CL (cap_zombie_cap_lift cap')) in capability.Zombie (capZombieID_CL (cap_zombie_cap_lift cap') && ~~ mask (radix + 1)) (ZombieCNode radix) (unat (capZombieID_CL (cap_zombie_cap_lift cap') && mask (radix + 1))))
 2. \<lbrakk>ccap_relation cap cap'; cap = (if isZombieTCB_C (capZombieType_CL (cap_zombie_cap_lift cap')) then capability.Zombie (capZombieID_CL (cap_zombie_cap_lift cap') && ~~ mask 5) ZombieTCB (unat (capZombieID_CL (cap_zombie_cap_lift cap') && mask 5)) else let radix = unat (capZombieType_CL (cap_zombie_cap_lift cap')) in capability.Zombie (capZombieID_CL (cap_zombie_cap_lift cap') && ~~ mask (radix + 1)) (ZombieCNode radix) (unat (capZombieID_CL (cap_zombie_cap_lift cap') && mask (radix + 1))))\<rbrakk> \<Longrightarrow> cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap proof (prove)
goal (2 subgoals):
 1. \<And>vl. \<lbrakk>cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap; cap_lift cap' = Some vl; cap = cap_to_H vl; c_valid_cap cap'\<rbrakk> \<Longrightarrow> cap = (if isZombieTCB_C (capZombieType_CL (cap_zombie_cap_lift cap')) then capability.Zombie (capZombieID_CL (cap_zombie_cap_lift cap') && ~~ mask 5) ZombieTCB (unat (capZombieID_CL (cap_zombie_cap_lift cap') && mask 5)) else let radix = unat (capZombieType_CL (cap_zombie_cap_lift cap')) in capability.Zombie (capZombieID_CL (cap_zombie_cap_lift cap') && ~~ mask (radix + 1)) (ZombieCNode radix) (unat (capZombieID_CL (cap_zombie_cap_lift cap') && mask (radix + 1))))
 2. \<lbrakk>ccap_relation cap cap'; cap = (if isZombieTCB_C (capZombieType_CL (cap_zombie_cap_lift cap')) then capability.Zombie (capZombieID_CL (cap_zombie_cap_lift cap') && ~~ mask 5) ZombieTCB (unat (capZombieID_CL (cap_zombie_cap_lift cap') && mask 5)) else let radix = unat (capZombieType_CL (cap_zombie_cap_lift cap')) in capability.Zombie (capZombieID_CL (cap_zombie_cap_lift cap') && ~~ mask (radix + 1)) (ZombieCNode radix) (unat (capZombieID_CL (cap_zombie_cap_lift cap') && mask (radix + 1))))\<rbrakk> \<Longrightarrow> cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ccap_relation cap cap'; cap = (if isZombieTCB_C (capZombieType_CL (cap_zombie_cap_lift cap')) then capability.Zombie (capZombieID_CL (cap_zombie_cap_lift cap') && ~~ mask 5) ZombieTCB (unat (capZombieID_CL (cap_zombie_cap_lift cap') && mask 5)) else let radix = unat (capZombieType_CL (cap_zombie_cap_lift cap')) in capability.Zombie (capZombieID_CL (cap_zombie_cap_lift cap') && ~~ mask (radix + 1)) (ZombieCNode radix) (unat (capZombieID_CL (cap_zombie_cap_lift cap') && mask (radix + 1))))\<rbrakk> \<Longrightarrow> cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap proof (prove)
goal:
No subgoals!