theory Finalise_R

lemma n_badged:
  "n p = Some (CTE cap node) \<Longrightarrow>
  \<exists>cap' node'. m p = Some (CTE cap' node') \<and>
              (if p = slot
               then \<not> mdbFirstBadged node
               else if p = mdbNext s_node
               then mdbFirstBadged node = (mdbFirstBadged node' \<or> mdbFirstBadged s_node)
               else mdbFirstBadged node = mdbFirstBadged node')" apply (subgoal_tac "p \<noteq> 0") prefer 2 apply (insert no_0_n)[1] apply clarsimp apply (cases "p = slot") apply (clarsimp simp: n_def modify_map_if initMDBNode_def split: if_split_asm) apply (cases "p = mdbNext s_node") apply (auto simp: n_def modify_map_if nullMDBNode_def split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n p = Some (CTE cap node) \<Longrightarrow> \<exists>cap' node'. m p = Some (CTE cap' node') \<and> (if p = slot then \<not> mdbFirstBadged node else if p = mdbNext s_node then mdbFirstBadged node = (mdbFirstBadged node' \<or> mdbFirstBadged s_node) else mdbFirstBadged node = mdbFirstBadged node') proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n p = Some (CTE cap node); p \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cap' node'. m p = Some (CTE cap' node') \<and> (if p = slot then \<not> mdbFirstBadged node else if p = mdbNext s_node then mdbFirstBadged node = (mdbFirstBadged node' \<or> mdbFirstBadged s_node) else mdbFirstBadged node = mdbFirstBadged node')
 2. n p = Some (CTE cap node) \<Longrightarrow> p \<noteq> 0 proof (prove)
goal (2 subgoals):
 1. n p = Some (CTE cap node) \<Longrightarrow> p \<noteq> 0
 2. \<lbrakk>n p = Some (CTE cap node); p \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cap' node'. m p = Some (CTE cap' node') \<and> (if p = slot then \<not> mdbFirstBadged node else if p = mdbNext s_node then mdbFirstBadged node = (mdbFirstBadged node' \<or> mdbFirstBadged s_node) else mdbFirstBadged node = mdbFirstBadged node') proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n p = Some (CTE cap node); no_0 n\<rbrakk> \<Longrightarrow> p \<noteq> 0
 2. \<lbrakk>n p = Some (CTE cap node); p \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cap' node'. m p = Some (CTE cap' node') \<and> (if p = slot then \<not> mdbFirstBadged node else if p = mdbNext s_node then mdbFirstBadged node = (mdbFirstBadged node' \<or> mdbFirstBadged s_node) else mdbFirstBadged node = mdbFirstBadged node') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n p = Some (CTE cap node); p \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cap' node'. m p = Some (CTE cap' node') \<and> (if p = slot then \<not> mdbFirstBadged node else if p = mdbNext s_node then mdbFirstBadged node = (mdbFirstBadged node' \<or> mdbFirstBadged s_node) else mdbFirstBadged node = mdbFirstBadged node') proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n p = Some (CTE cap node); p \<noteq> 0; p = slot\<rbrakk> \<Longrightarrow> \<exists>cap' node'. m p = Some (CTE cap' node') \<and> (if p = slot then \<not> mdbFirstBadged node else if p = mdbNext s_node then mdbFirstBadged node = (mdbFirstBadged node' \<or> mdbFirstBadged s_node) else mdbFirstBadged node = mdbFirstBadged node')
 2. \<lbrakk>n p = Some (CTE cap node); p \<noteq> 0; p \<noteq> slot\<rbrakk> \<Longrightarrow> \<exists>cap' node'. m p = Some (CTE cap' node') \<and> (if p = slot then \<not> mdbFirstBadged node else if p = mdbNext s_node then mdbFirstBadged node = (mdbFirstBadged node' \<or> mdbFirstBadged s_node) else mdbFirstBadged node = mdbFirstBadged node') proof (prove)
goal (2 subgoals):
 1. \<And>nodea capa. \<lbrakk>p = slot; m slot = Some (CTE capa nodea); cap = capability.NullCap; node = nullMDBNode; mdbFirstBadged nullMDBNode\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>n p = Some (CTE cap node); p \<noteq> 0; p \<noteq> slot\<rbrakk> \<Longrightarrow> \<exists>cap' node'. m p = Some (CTE cap' node') \<and> (if p = slot then \<not> mdbFirstBadged node else if p = mdbNext s_node then mdbFirstBadged node = (mdbFirstBadged node' \<or> mdbFirstBadged s_node) else mdbFirstBadged node = mdbFirstBadged node') proof (prove)
goal (3 subgoals):
 1. \<And>nodea capa. \<lbrakk>p = slot; m slot = Some (CTE capa nodea); cap = capability.NullCap; node = nullMDBNode; mdbFirstBadged nullMDBNode; p = mdbNext s_node\<rbrakk> \<Longrightarrow> False
 2. \<And>nodea capa. \<lbrakk>p = slot; m slot = Some (CTE capa nodea); cap = capability.NullCap; node = nullMDBNode; mdbFirstBadged nullMDBNode; p \<noteq> mdbNext s_node\<rbrakk> \<Longrightarrow> False
 3. \<lbrakk>n p = Some (CTE cap node); p \<noteq> 0; p \<noteq> slot\<rbrakk> \<Longrightarrow> \<exists>cap' node'. m p = Some (CTE cap' node') \<and> (if p = slot then \<not> mdbFirstBadged node else if p = mdbNext s_node then mdbFirstBadged node = (mdbFirstBadged node' \<or> mdbFirstBadged s_node) else mdbFirstBadged node = mdbFirstBadged node') proof (prove)
goal:
No subgoals!