theory Finalise_R

lemma nullcaps_n: "valid_nullcaps n" proof - from valid have "valid_nullcaps m" .. thus ?thesis apply (clarsimp simp: valid_nullcaps_def nullMDBNode_def nullPointer_def) apply (frule n_cap) apply (frule n_next) apply (frule n_badged) apply (frule n_revokable) apply (drule n_prev) apply (case_tac n) apply (insert slot) apply (fastforce split: if_split_asm) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_nullcaps n proof (state)
goal (1 subgoal):
 1. valid_nullcaps n proof (chain)
picking this:
valid_mdb_ctes m proof (prove)
using this:
valid_mdb_ctes m

goal (1 subgoal):
 1. valid_nullcaps m proof (state)
this:
valid_nullcaps m

goal (1 subgoal):
 1. valid_nullcaps n proof (prove)
using this:
valid_nullcaps m

goal (1 subgoal):
 1. valid_nullcaps n proof (prove)
goal (1 subgoal):
 1. \<And>p na. \<lbrakk>\<forall>p n. m p = Some (CTE capability.NullCap n) \<longrightarrow> n = MDB 0 0 False False; n p = Some (CTE capability.NullCap na)\<rbrakk> \<Longrightarrow> na = MDB 0 0 False False proof (prove)
goal (1 subgoal):
 1. \<And>p na. \<lbrakk>\<forall>p n. m p = Some (CTE capability.NullCap n) \<longrightarrow> n = MDB 0 0 False False; n p = Some (CTE capability.NullCap na); \<exists>cap' node'. m p = Some (CTE cap' node') \<and> (if p = slot then capability.NullCap = capability.NullCap else cap' = capability.NullCap)\<rbrakk> \<Longrightarrow> na = MDB 0 0 False False proof (prove)
goal (1 subgoal):
 1. \<And>p na. \<lbrakk>\<forall>p n. m p = Some (CTE capability.NullCap n) \<longrightarrow> n = MDB 0 0 False False; n p = Some (CTE capability.NullCap na); \<exists>cap' node'. m p = Some (CTE cap' node') \<and> (if p = slot then capability.NullCap = capability.NullCap else cap' = capability.NullCap); \<exists>cap' node'. m p = Some (CTE cap' node') \<and> (if p = slot then mdbNext na = 0 else if p = mdbPrev s_node then mdbNext na = mdbNext s_node else mdbNext na = mdbNext node')\<rbrakk> \<Longrightarrow> na = MDB 0 0 False False proof (prove)
goal (1 subgoal):
 1. \<And>p na. \<lbrakk>\<forall>p n. m p = Some (CTE capability.NullCap n) \<longrightarrow> n = MDB 0 0 False False; n p = Some (CTE capability.NullCap na); \<exists>cap' node'. m p = Some (CTE cap' node') \<and> (if p = slot then capability.NullCap = capability.NullCap else cap' = capability.NullCap); \<exists>cap' node'. m p = Some (CTE cap' node') \<and> (if p = slot then mdbNext na = 0 else if p = mdbPrev s_node then mdbNext na = mdbNext s_node else mdbNext na = mdbNext node'); \<exists>cap' node'. m p = Some (CTE cap' node') \<and> (if p = slot then \<not> mdbFirstBadged na else if p = mdbNext s_node then mdbFirstBadged na = (mdbFirstBadged node' \<or> mdbFirstBadged s_node) else mdbFirstBadged na = mdbFirstBadged node')\<rbrakk> \<Longrightarrow> na = MDB 0 0 False False proof (prove)
goal (1 subgoal):
 1. \<And>p na. \<lbrakk>\<forall>p n. m p = Some (CTE capability.NullCap n) \<longrightarrow> n = MDB 0 0 False False; n p = Some (CTE capability.NullCap na); \<exists>cap' node'. m p = Some (CTE cap' node') \<and> (if p = slot then capability.NullCap = capability.NullCap else cap' = capability.NullCap); \<exists>cap' node'. m p = Some (CTE cap' node') \<and> (if p = slot then mdbNext na = 0 else if p = mdbPrev s_node then mdbNext na = mdbNext s_node else mdbNext na = mdbNext node'); \<exists>cap' node'. m p = Some (CTE cap' node') \<and> (if p = slot then \<not> mdbFirstBadged na else if p = mdbNext s_node then mdbFirstBadged na = (mdbFirstBadged node' \<or> mdbFirstBadged s_node) else mdbFirstBadged na = mdbFirstBadged node'); \<exists>cap' node'. m p = Some (CTE cap' node') \<and> (if p = slot then \<not> mdbRevocable na else mdbRevocable na = mdbRevocable node')\<rbrakk> \<Longrightarrow> na = MDB 0 0 False False proof (prove)
goal (1 subgoal):
 1. \<And>p n. \<lbrakk>\<forall>p n. m p = Some (CTE capability.NullCap n) \<longrightarrow> n = MDB 0 0 False False; \<exists>cap' node'. m p = Some (CTE cap' node') \<and> (if p = slot then capability.NullCap = capability.NullCap else cap' = capability.NullCap); \<exists>cap' node'. m p = Some (CTE cap' node') \<and> (if p = slot then mdbNext n = 0 else if p = mdbPrev s_node then mdbNext n = mdbNext s_node else mdbNext n = mdbNext node'); \<exists>cap' node'. m p = Some (CTE cap' node') \<and> (if p = slot then \<not> mdbFirstBadged n else if p = mdbNext s_node then mdbFirstBadged n = (mdbFirstBadged node' \<or> mdbFirstBadged s_node) else mdbFirstBadged n = mdbFirstBadged node'); \<exists>cap' node'. m p = Some (CTE cap' node') \<and> (if p = slot then \<not> mdbRevocable n else mdbRevocable n = mdbRevocable node'); \<exists>cap' node'. m p = Some (CTE cap' node') \<and> (if p = slot then mdbPrev n = 0 else if p = mdbNext s_node then mdbPrev n = mdbPrev s_node else mdbPrev n = mdbPrev node')\<rbrakk> \<Longrightarrow> n = MDB 0 0 False False proof (prove)
goal (1 subgoal):
 1. \<And>p n x1 x2 x3 x4. \<lbrakk>\<forall>p n. m p = Some (CTE capability.NullCap n) \<longrightarrow> n = MDB 0 0 False False; \<exists>cap' node'. m p = Some (CTE cap' node') \<and> (if p = slot then capability.NullCap = capability.NullCap else cap' = capability.NullCap); \<exists>cap' node'. m p = Some (CTE cap' node') \<and> (if p = slot then mdbNext n = 0 else if p = mdbPrev s_node then mdbNext n = mdbNext s_node else mdbNext n = mdbNext node'); \<exists>cap' node'. m p = Some (CTE cap' node') \<and> (if p = slot then \<not> mdbFirstBadged n else if p = mdbNext s_node then mdbFirstBadged n = (mdbFirstBadged node' \<or> mdbFirstBadged s_node) else mdbFirstBadged n = mdbFirstBadged node'); \<exists>cap' node'. m p = Some (CTE cap' node') \<and> (if p = slot then \<not> mdbRevocable n else mdbRevocable n = mdbRevocable node'); \<exists>cap' node'. m p = Some (CTE cap' node') \<and> (if p = slot then mdbPrev n = 0 else if p = mdbNext s_node then mdbPrev n = mdbPrev s_node else mdbPrev n = mdbPrev node'); n = MDB x1 x2 x3 x4\<rbrakk> \<Longrightarrow> n = MDB 0 0 False False proof (prove)
goal (1 subgoal):
 1. \<And>p n x1 x2 x3 x4. \<lbrakk>\<forall>p n. m p = Some (CTE capability.NullCap n) \<longrightarrow> n = MDB 0 0 False False; \<exists>cap' node'. m p = Some (CTE cap' node') \<and> (if p = slot then capability.NullCap = capability.NullCap else cap' = capability.NullCap); \<exists>cap' node'. m p = Some (CTE cap' node') \<and> (if p = slot then mdbNext n = 0 else if p = mdbPrev s_node then mdbNext n = mdbNext s_node else mdbNext n = mdbNext node'); \<exists>cap' node'. m p = Some (CTE cap' node') \<and> (if p = slot then \<not> mdbFirstBadged n else if p = mdbNext s_node then mdbFirstBadged n = (mdbFirstBadged node' \<or> mdbFirstBadged s_node) else mdbFirstBadged n = mdbFirstBadged node'); \<exists>cap' node'. m p = Some (CTE cap' node') \<and> (if p = slot then \<not> mdbRevocable n else mdbRevocable n = mdbRevocable node'); \<exists>cap' node'. m p = Some (CTE cap' node') \<and> (if p = slot then mdbPrev n = 0 else if p = mdbNext s_node then mdbPrev n = mdbPrev s_node else mdbPrev n = mdbPrev node'); n = MDB x1 x2 x3 x4; m slot = Some (CTE s_cap s_node)\<rbrakk> \<Longrightarrow> n = MDB 0 0 False False proof (prove)
goal:
No subgoals! proof (state)
this:
valid_nullcaps n

goal:
No subgoals!