theory ArchCNodeInv_AI

lemma weak_derived_table_cap_ref [CNodeInv_AI_assms]:
  "weak_derived c c' \<Longrightarrow> table_cap_ref c = table_cap_ref c'" apply (clarsimp simp: weak_derived_def copy_of_def
                 same_object_as_def2
          split: if_split_asm) apply (elim disjE,simp_all add:is_cap_simps) apply (elim disjE,simp_all) apply clarsimp apply (frule vs_cap_ref_master[OF sym],simp+) apply (drule vs_cap_ref_eq_imp_table_cap_ref_eq') apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. weak_derived c c' \<Longrightarrow> table_cap_ref c = table_cap_ref c' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_untyped_cap c'; c' = c \<and> cap_asid c = cap_asid c' \<and> cap_asid_base c = cap_asid_base c' \<and> cap_vptr c = cap_vptr c' \<or> c' = c\<rbrakk> \<Longrightarrow> table_cap_ref c = table_cap_ref c'
 2. \<lbrakk>\<not> is_untyped_cap c'; cap_master_cap c' = cap_master_cap c \<and> c' \<noteq> NullCap \<and> \<not> is_zombie c' \<and> (is_arch_cap c' \<longrightarrow> (case the_arch_cap c' of PageCap d x rs sz v \<Rightarrow> x \<le> x + 2 ^ pageBitsForSize sz - 1 | _ \<Rightarrow> True)) \<and> is_reply_cap c' = is_reply_cap c \<and> is_master_reply_cap c' = is_master_reply_cap c \<and> cap_asid c = cap_asid c' \<and> cap_asid_base c = cap_asid_base c' \<and> cap_vptr c = cap_vptr c' \<or> c' = c\<rbrakk> \<Longrightarrow> table_cap_ref c = table_cap_ref c' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>dev r bits f. c' \<noteq> UntypedCap dev r bits f; cap_master_cap c' = cap_master_cap c \<and> c' \<noteq> NullCap \<and> (\<forall>r b n. c' \<noteq> Zombie r b n) \<and> ((\<exists>a. c' = ArchObjectCap a) \<longrightarrow> (case the_arch_cap c' of PageCap d x rs sz v \<Rightarrow> x \<le> x + 2 ^ pageBitsForSize sz - 1 | _ \<Rightarrow> True)) \<and> (\<exists>x R. c' = ReplyCap x False R) = (\<exists>x R. c = ReplyCap x False R) \<and> (\<exists>x R. c' = ReplyCap x True R) = (\<exists>x R. c = ReplyCap x True R) \<and> cap_asid c = cap_asid c' \<and> cap_asid_base c = cap_asid_base c' \<and> cap_vptr c = cap_vptr c' \<or> c' = c\<rbrakk> \<Longrightarrow> table_cap_ref c = table_cap_ref c' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>dev r bits f. c' \<noteq> UntypedCap dev r bits f; cap_master_cap c' = cap_master_cap c \<and> c' \<noteq> NullCap \<and> (\<forall>r b n. c' \<noteq> Zombie r b n) \<and> ((\<exists>a. c' = ArchObjectCap a) \<longrightarrow> (case the_arch_cap c' of PageCap d x rs sz v \<Rightarrow> x \<le> x + 2 ^ pageBitsForSize sz - 1 | _ \<Rightarrow> True)) \<and> (\<exists>x R. c' = ReplyCap x False R) = (\<exists>x R. c = ReplyCap x False R) \<and> (\<exists>x R. c' = ReplyCap x True R) = (\<exists>x R. c = ReplyCap x True R) \<and> cap_asid c = cap_asid c' \<and> cap_asid_base c = cap_asid_base c' \<and> cap_vptr c = cap_vptr c'\<rbrakk> \<Longrightarrow> table_cap_ref c = table_cap_ref c' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>dev r bits f. c' \<noteq> UntypedCap dev r bits f; cap_master_cap c' = cap_master_cap c; c' \<noteq> NullCap; \<forall>r b n. c' \<noteq> Zombie r b n; (\<exists>a. c' = ArchObjectCap a) \<longrightarrow> (case the_arch_cap c' of PageCap d x rs sz v \<Rightarrow> x \<le> x + 2 ^ pageBitsForSize sz - 1 | _ \<Rightarrow> True); (\<exists>x R. c' = ReplyCap x False R) = (\<exists>x R. c = ReplyCap x False R); (\<exists>x R. c' = ReplyCap x True R) = (\<exists>x R. c = ReplyCap x True R); cap_asid c = cap_asid c'; cap_asid_base c = cap_asid_base c'; cap_vptr c = cap_vptr c'\<rbrakk> \<Longrightarrow> table_cap_ref c = table_cap_ref c' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>dev r bits f. c' \<noteq> UntypedCap dev r bits f; cap_master_cap c' = cap_master_cap c; c' \<noteq> NullCap; \<forall>r b n. c' \<noteq> Zombie r b n; (\<exists>a. c' = ArchObjectCap a) \<longrightarrow> (case the_arch_cap c' of PageCap d x rs sz v \<Rightarrow> x \<le> x + 2 ^ pageBitsForSize sz - 1 | _ \<Rightarrow> True); (\<exists>x R. c' = ReplyCap x False R) = (\<exists>x R. c = ReplyCap x False R); (\<exists>x R. c' = ReplyCap x True R) = (\<exists>x R. c = ReplyCap x True R); cap_asid c = cap_asid c'; cap_asid_base c = cap_asid_base c'; cap_vptr c = cap_vptr c'; vs_cap_ref c = vs_cap_ref c'\<rbrakk> \<Longrightarrow> table_cap_ref c = table_cap_ref c' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>dev r bits f. c' \<noteq> UntypedCap dev r bits f; c' \<noteq> NullCap; \<forall>r b n. c' \<noteq> Zombie r b n; (\<exists>a. c' = ArchObjectCap a) \<longrightarrow> (case the_arch_cap c' of PageCap d x rs sz v \<Rightarrow> x \<le> x + 2 ^ pageBitsForSize sz - 1 | _ \<Rightarrow> True); (\<exists>x R. c' = ReplyCap x False R) = (\<exists>x R. c = ReplyCap x False R); (\<exists>x R. c' = ReplyCap x True R) = (\<exists>x R. c = ReplyCap x True R); cap_asid c = cap_asid c'; cap_asid_base c = cap_asid_base c'; cap_vptr c = cap_vptr c'; vs_cap_ref c = vs_cap_ref c'\<rbrakk> \<Longrightarrow> vs_cap_ref c' = vs_cap_ref c
 2. \<lbrakk>\<forall>dev r bits f. c' \<noteq> UntypedCap dev r bits f; c' \<noteq> NullCap; \<forall>r b n. c' \<noteq> Zombie r b n; (\<exists>a. c' = ArchObjectCap a) \<longrightarrow> (case the_arch_cap c' of PageCap d x rs sz v \<Rightarrow> x \<le> x + 2 ^ pageBitsForSize sz - 1 | _ \<Rightarrow> True); (\<exists>x R. c' = ReplyCap x False R) = (\<exists>x R. c = ReplyCap x False R); (\<exists>x R. c' = ReplyCap x True R) = (\<exists>x R. c = ReplyCap x True R); cap_asid c = cap_asid c'; cap_asid_base c = cap_asid_base c'; cap_vptr c = cap_vptr c'; vs_cap_ref c = vs_cap_ref c'; table_cap_ref c' = table_cap_ref c\<rbrakk> \<Longrightarrow> table_cap_ref c = table_cap_ref c' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>dev r bits f. c' \<noteq> UntypedCap dev r bits f; c' \<noteq> NullCap; \<forall>r b n. c' \<noteq> Zombie r b n; (\<exists>a. c' = ArchObjectCap a) \<longrightarrow> (case the_arch_cap c' of PageCap d x rs sz v \<Rightarrow> x \<le> x + 2 ^ pageBitsForSize sz - 1 | _ \<Rightarrow> True); (\<exists>x R. c' = ReplyCap x False R) = (\<exists>x R. c = ReplyCap x False R); (\<exists>x R. c' = ReplyCap x True R) = (\<exists>x R. c = ReplyCap x True R); cap_asid c = cap_asid c'; cap_asid_base c = cap_asid_base c'; cap_vptr c = cap_vptr c'; vs_cap_ref c = vs_cap_ref c'; table_cap_ref c' = table_cap_ref c\<rbrakk> \<Longrightarrow> table_cap_ref c = table_cap_ref c' proof (prove)
goal:
No subgoals!