theory KHeap_R

lemma map_to_ctes_upd_cte:
  "\<lbrakk> s p = Some (KOCTE cte'); is_aligned p cte_level_bits;
     {p + 1..p + mask cte_level_bits} \<inter> dom s = {} \<rbrakk> \<Longrightarrow>
     map_to_ctes (s (p \<mapsto> (KOCTE cte))) = ((map_to_ctes s) (p \<mapsto> cte))" apply (rule ext) apply (simp    add: map_to_ctes_def Let_def dom_fun_upd2
           split del: if_split del: dom_fun_upd) apply (case_tac "x = p") apply (simp add: objBits_simps' cte_level_bits_def mask_def field_simps) apply (case_tac "(x && ~~ mask (objBitsKO (KOTCB undefined))) = p") apply clarsimp apply (simp del: dom_fun_upd split del: if_split cong: if_cong
              add: dom_fun_upd2 field_simps objBits_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s p = Some (KOCTE cte'); is_aligned p cte_level_bits; {p + 1..p + mask cte_level_bits} \<inter> dom s = {}\<rbrakk> \<Longrightarrow> map_to_ctes (s(p \<mapsto> KOCTE cte)) = (map_to_ctes s)(p \<mapsto> cte) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>s p = Some (KOCTE cte'); is_aligned p cte_level_bits; {p + 1..p + mask cte_level_bits} \<inter> dom s = {}\<rbrakk> \<Longrightarrow> map_to_ctes (s(p \<mapsto> KOCTE cte)) x = ((map_to_ctes s)(p \<mapsto> cte)) x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>s p = Some (KOCTE cte'); is_aligned p cte_level_bits; {p + 1..p + mask cte_level_bits} \<inter> dom s = {}\<rbrakk> \<Longrightarrow> (if (\<exists>ctea. (if x = p then Some (KOCTE cte) else s x) = Some (KOCTE ctea)) \<and> is_aligned x (objBitsKO (KOCTE undefined)) \<and> {x + 1..x + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom s = {} then case if x = p then Some (KOCTE cte) else s x of Some (KOCTE x) \<Rightarrow> Some x else if (\<exists>tcb. (if x && ~~ mask (objBitsKO (KOTCB undefined)) = p then Some (KOCTE cte) else s (x && ~~ mask (objBitsKO (KOTCB undefined)))) = Some (KOTCB tcb)) \<and> {(x && ~~ mask (objBitsKO (KOTCB undefined))) + 1..(x && ~~ mask (objBitsKO (KOTCB undefined))) + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom s = {} then case if x && ~~ mask (objBitsKO (KOTCB undefined)) = p then Some (KOCTE cte) else s (x && ~~ mask (objBitsKO (KOTCB undefined))) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (x - (x && ~~ mask (objBitsKO (KOTCB undefined))))) else None) = (if x = p then Some cte else if (\<exists>cte. s x = Some (KOCTE cte)) \<and> is_aligned x (objBitsKO (KOCTE undefined)) \<and> {x + 1..x + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom s = {} then case s x of Some (KOCTE x) \<Rightarrow> Some x else if (\<exists>tcb. s (x && ~~ mask (objBitsKO (KOTCB undefined))) = Some (KOTCB tcb)) \<and> {(x && ~~ mask (objBitsKO (KOTCB undefined))) + 1..(x && ~~ mask (objBitsKO (KOTCB undefined))) + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom s = {} then case s (x && ~~ mask (objBitsKO (KOTCB undefined))) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (x - (x && ~~ mask (objBitsKO (KOTCB undefined))))) else None) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>s p = Some (KOCTE cte'); is_aligned p cte_level_bits; {p + 1..p + mask cte_level_bits} \<inter> dom s = {}; x = p\<rbrakk> \<Longrightarrow> (if (\<exists>ctea. (if x = p then Some (KOCTE cte) else s x) = Some (KOCTE ctea)) \<and> is_aligned x (objBitsKO (KOCTE undefined)) \<and> {x + 1..x + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom s = {} then case if x = p then Some (KOCTE cte) else s x of Some (KOCTE x) \<Rightarrow> Some x else if (\<exists>tcb. (if x && ~~ mask (objBitsKO (KOTCB undefined)) = p then Some (KOCTE cte) else s (x && ~~ mask (objBitsKO (KOTCB undefined)))) = Some (KOTCB tcb)) \<and> {(x && ~~ mask (objBitsKO (KOTCB undefined))) + 1..(x && ~~ mask (objBitsKO (KOTCB undefined))) + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom s = {} then case if x && ~~ mask (objBitsKO (KOTCB undefined)) = p then Some (KOCTE cte) else s (x && ~~ mask (objBitsKO (KOTCB undefined))) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (x - (x && ~~ mask (objBitsKO (KOTCB undefined))))) else None) = (if x = p then Some cte else if (\<exists>cte. s x = Some (KOCTE cte)) \<and> is_aligned x (objBitsKO (KOCTE undefined)) \<and> {x + 1..x + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom s = {} then case s x of Some (KOCTE x) \<Rightarrow> Some x else if (\<exists>tcb. s (x && ~~ mask (objBitsKO (KOTCB undefined))) = Some (KOTCB tcb)) \<and> {(x && ~~ mask (objBitsKO (KOTCB undefined))) + 1..(x && ~~ mask (objBitsKO (KOTCB undefined))) + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom s = {} then case s (x && ~~ mask (objBitsKO (KOTCB undefined))) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (x - (x && ~~ mask (objBitsKO (KOTCB undefined))))) else None)
 2. \<And>x. \<lbrakk>s p = Some (KOCTE cte'); is_aligned p cte_level_bits; {p + 1..p + mask cte_level_bits} \<inter> dom s = {}; x \<noteq> p\<rbrakk> \<Longrightarrow> (if (\<exists>ctea. (if x = p then Some (KOCTE cte) else s x) = Some (KOCTE ctea)) \<and> is_aligned x (objBitsKO (KOCTE undefined)) \<and> {x + 1..x + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom s = {} then case if x = p then Some (KOCTE cte) else s x of Some (KOCTE x) \<Rightarrow> Some x else if (\<exists>tcb. (if x && ~~ mask (objBitsKO (KOTCB undefined)) = p then Some (KOCTE cte) else s (x && ~~ mask (objBitsKO (KOTCB undefined)))) = Some (KOTCB tcb)) \<and> {(x && ~~ mask (objBitsKO (KOTCB undefined))) + 1..(x && ~~ mask (objBitsKO (KOTCB undefined))) + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom s = {} then case if x && ~~ mask (objBitsKO (KOTCB undefined)) = p then Some (KOCTE cte) else s (x && ~~ mask (objBitsKO (KOTCB undefined))) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (x - (x && ~~ mask (objBitsKO (KOTCB undefined))))) else None) = (if x = p then Some cte else if (\<exists>cte. s x = Some (KOCTE cte)) \<and> is_aligned x (objBitsKO (KOCTE undefined)) \<and> {x + 1..x + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom s = {} then case s x of Some (KOCTE x) \<Rightarrow> Some x else if (\<exists>tcb. s (x && ~~ mask (objBitsKO (KOTCB undefined))) = Some (KOTCB tcb)) \<and> {(x && ~~ mask (objBitsKO (KOTCB undefined))) + 1..(x && ~~ mask (objBitsKO (KOTCB undefined))) + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom s = {} then case s (x && ~~ mask (objBitsKO (KOTCB undefined))) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (x - (x && ~~ mask (objBitsKO (KOTCB undefined))))) else None) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>s p = Some (KOCTE cte'); is_aligned p cte_level_bits; {p + 1..p + mask cte_level_bits} \<inter> dom s = {}; x \<noteq> p\<rbrakk> \<Longrightarrow> (if (\<exists>ctea. (if x = p then Some (KOCTE cte) else s x) = Some (KOCTE ctea)) \<and> is_aligned x (objBitsKO (KOCTE undefined)) \<and> {x + 1..x + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom s = {} then case if x = p then Some (KOCTE cte) else s x of Some (KOCTE x) \<Rightarrow> Some x else if (\<exists>tcb. (if x && ~~ mask (objBitsKO (KOTCB undefined)) = p then Some (KOCTE cte) else s (x && ~~ mask (objBitsKO (KOTCB undefined)))) = Some (KOTCB tcb)) \<and> {(x && ~~ mask (objBitsKO (KOTCB undefined))) + 1..(x && ~~ mask (objBitsKO (KOTCB undefined))) + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom s = {} then case if x && ~~ mask (objBitsKO (KOTCB undefined)) = p then Some (KOCTE cte) else s (x && ~~ mask (objBitsKO (KOTCB undefined))) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (x - (x && ~~ mask (objBitsKO (KOTCB undefined))))) else None) = (if x = p then Some cte else if (\<exists>cte. s x = Some (KOCTE cte)) \<and> is_aligned x (objBitsKO (KOCTE undefined)) \<and> {x + 1..x + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom s = {} then case s x of Some (KOCTE x) \<Rightarrow> Some x else if (\<exists>tcb. s (x && ~~ mask (objBitsKO (KOTCB undefined))) = Some (KOTCB tcb)) \<and> {(x && ~~ mask (objBitsKO (KOTCB undefined))) + 1..(x && ~~ mask (objBitsKO (KOTCB undefined))) + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom s = {} then case s (x && ~~ mask (objBitsKO (KOTCB undefined))) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (x - (x && ~~ mask (objBitsKO (KOTCB undefined))))) else None) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>s p = Some (KOCTE cte'); is_aligned p cte_level_bits; {p + 1..p + mask cte_level_bits} \<inter> dom s = {}; x \<noteq> p; x && ~~ mask (objBitsKO (KOTCB undefined)) = p\<rbrakk> \<Longrightarrow> (if (\<exists>ctea. (if x = p then Some (KOCTE cte) else s x) = Some (KOCTE ctea)) \<and> is_aligned x (objBitsKO (KOCTE undefined)) \<and> {x + 1..x + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom s = {} then case if x = p then Some (KOCTE cte) else s x of Some (KOCTE x) \<Rightarrow> Some x else if (\<exists>tcb. (if x && ~~ mask (objBitsKO (KOTCB undefined)) = p then Some (KOCTE cte) else s (x && ~~ mask (objBitsKO (KOTCB undefined)))) = Some (KOTCB tcb)) \<and> {(x && ~~ mask (objBitsKO (KOTCB undefined))) + 1..(x && ~~ mask (objBitsKO (KOTCB undefined))) + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom s = {} then case if x && ~~ mask (objBitsKO (KOTCB undefined)) = p then Some (KOCTE cte) else s (x && ~~ mask (objBitsKO (KOTCB undefined))) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (x - (x && ~~ mask (objBitsKO (KOTCB undefined))))) else None) = (if x = p then Some cte else if (\<exists>cte. s x = Some (KOCTE cte)) \<and> is_aligned x (objBitsKO (KOCTE undefined)) \<and> {x + 1..x + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom s = {} then case s x of Some (KOCTE x) \<Rightarrow> Some x else if (\<exists>tcb. s (x && ~~ mask (objBitsKO (KOTCB undefined))) = Some (KOTCB tcb)) \<and> {(x && ~~ mask (objBitsKO (KOTCB undefined))) + 1..(x && ~~ mask (objBitsKO (KOTCB undefined))) + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom s = {} then case s (x && ~~ mask (objBitsKO (KOTCB undefined))) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (x - (x && ~~ mask (objBitsKO (KOTCB undefined))))) else None)
 2. \<And>x. \<lbrakk>s p = Some (KOCTE cte'); is_aligned p cte_level_bits; {p + 1..p + mask cte_level_bits} \<inter> dom s = {}; x \<noteq> p; x && ~~ mask (objBitsKO (KOTCB undefined)) \<noteq> p\<rbrakk> \<Longrightarrow> (if (\<exists>ctea. (if x = p then Some (KOCTE cte) else s x) = Some (KOCTE ctea)) \<and> is_aligned x (objBitsKO (KOCTE undefined)) \<and> {x + 1..x + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom s = {} then case if x = p then Some (KOCTE cte) else s x of Some (KOCTE x) \<Rightarrow> Some x else if (\<exists>tcb. (if x && ~~ mask (objBitsKO (KOTCB undefined)) = p then Some (KOCTE cte) else s (x && ~~ mask (objBitsKO (KOTCB undefined)))) = Some (KOTCB tcb)) \<and> {(x && ~~ mask (objBitsKO (KOTCB undefined))) + 1..(x && ~~ mask (objBitsKO (KOTCB undefined))) + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom s = {} then case if x && ~~ mask (objBitsKO (KOTCB undefined)) = p then Some (KOCTE cte) else s (x && ~~ mask (objBitsKO (KOTCB undefined))) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (x - (x && ~~ mask (objBitsKO (KOTCB undefined))))) else None) = (if x = p then Some cte else if (\<exists>cte. s x = Some (KOCTE cte)) \<and> is_aligned x (objBitsKO (KOCTE undefined)) \<and> {x + 1..x + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom s = {} then case s x of Some (KOCTE x) \<Rightarrow> Some x else if (\<exists>tcb. s (x && ~~ mask (objBitsKO (KOTCB undefined))) = Some (KOTCB tcb)) \<and> {(x && ~~ mask (objBitsKO (KOTCB undefined))) + 1..(x && ~~ mask (objBitsKO (KOTCB undefined))) + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom s = {} then case s (x && ~~ mask (objBitsKO (KOTCB undefined))) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (x - (x && ~~ mask (objBitsKO (KOTCB undefined))))) else None) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>s p = Some (KOCTE cte'); is_aligned p cte_level_bits; {p + 1..p + mask cte_level_bits} \<inter> dom s = {}; x \<noteq> p; x && ~~ mask (objBitsKO (KOTCB undefined)) \<noteq> p\<rbrakk> \<Longrightarrow> (if (\<exists>ctea. (if x = p then Some (KOCTE cte) else s x) = Some (KOCTE ctea)) \<and> is_aligned x (objBitsKO (KOCTE undefined)) \<and> {x + 1..x + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom s = {} then case if x = p then Some (KOCTE cte) else s x of Some (KOCTE x) \<Rightarrow> Some x else if (\<exists>tcb. (if x && ~~ mask (objBitsKO (KOTCB undefined)) = p then Some (KOCTE cte) else s (x && ~~ mask (objBitsKO (KOTCB undefined)))) = Some (KOTCB tcb)) \<and> {(x && ~~ mask (objBitsKO (KOTCB undefined))) + 1..(x && ~~ mask (objBitsKO (KOTCB undefined))) + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom s = {} then case if x && ~~ mask (objBitsKO (KOTCB undefined)) = p then Some (KOCTE cte) else s (x && ~~ mask (objBitsKO (KOTCB undefined))) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (x - (x && ~~ mask (objBitsKO (KOTCB undefined))))) else None) = (if x = p then Some cte else if (\<exists>cte. s x = Some (KOCTE cte)) \<and> is_aligned x (objBitsKO (KOCTE undefined)) \<and> {x + 1..x + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom s = {} then case s x of Some (KOCTE x) \<Rightarrow> Some x else if (\<exists>tcb. s (x && ~~ mask (objBitsKO (KOTCB undefined))) = Some (KOTCB tcb)) \<and> {(x && ~~ mask (objBitsKO (KOTCB undefined))) + 1..(x && ~~ mask (objBitsKO (KOTCB undefined))) + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom s = {} then case s (x && ~~ mask (objBitsKO (KOTCB undefined))) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (x - (x && ~~ mask (objBitsKO (KOTCB undefined))))) else None) proof (prove)
goal:
No subgoals!