theory Untyped_R

lemma site_no_parent_n:
  "n \<turnstile> site \<rightarrow> p = False" using parent valid_badges apply clarsimp apply (erule subtree.induct) prefer 2 apply simp apply (clarsimp simp: parentOf_def mdb_next_unfold new_site_def n) apply (cases "mdbNext parent_node = site") apply (subgoal_tac "m \<turnstile> parent \<leadsto> site") apply simp apply (subst mdb_next_unfold) apply (simp add: parent) apply clarsimp apply (erule notE[rotated], erule(1) next_not_parent[unfolded new_site_def]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n \<turnstile> site \<rightarrow> p = False proof (prove)
using this:
m parent = Some (CTE parent_cap parent_node)
valid_badges m

goal (1 subgoal):
 1. n \<turnstile> site \<rightarrow> p = False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m parent = Some (CTE parent_cap parent_node); valid_badges m; n \<turnstile> site \<rightarrow> p\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>c'. \<lbrakk>m parent = Some (CTE parent_cap parent_node); valid_badges m; n \<turnstile> site \<leadsto> c'; c' \<noteq> 0; n \<turnstile> site parentOf c'\<rbrakk> \<Longrightarrow> False
 2. \<And>c' c''. \<lbrakk>m parent = Some (CTE parent_cap parent_node); valid_badges m; n \<turnstile> site \<rightarrow> c'; False; n \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; n \<turnstile> site parentOf c''\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>c' c''. \<lbrakk>m parent = Some (CTE parent_cap parent_node); valid_badges m; n \<turnstile> site \<rightarrow> c'; False; n \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; n \<turnstile> site parentOf c''\<rbrakk> \<Longrightarrow> False
 2. \<And>c'. \<lbrakk>m parent = Some (CTE parent_cap parent_node); valid_badges m; n \<turnstile> site \<leadsto> c'; c' \<noteq> 0; n \<turnstile> site parentOf c'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>c'. \<lbrakk>m parent = Some (CTE parent_cap parent_node); valid_badges m; n \<turnstile> site \<leadsto> c'; c' \<noteq> 0; n \<turnstile> site parentOf c'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>cte. \<lbrakk>m parent = Some (CTE parent_cap parent_node); valid_badges m; mdbNext parent_node \<noteq> 0; (if mdbNext parent_node = site then Some (CTE c' (MDB (mdbNext parent_node) parent True True)) else m (mdbNext parent_node)) = Some cte; isMDBParentOf (CTE c' (MDB (mdbNext parent_node) parent True True)) cte\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>cte. \<lbrakk>m parent = Some (CTE parent_cap parent_node); valid_badges m; mdbNext parent_node \<noteq> 0; (if mdbNext parent_node = site then Some (CTE c' (MDB (mdbNext parent_node) parent True True)) else m (mdbNext parent_node)) = Some cte; isMDBParentOf (CTE c' (MDB (mdbNext parent_node) parent True True)) cte; mdbNext parent_node = site\<rbrakk> \<Longrightarrow> False
 2. \<And>cte. \<lbrakk>m parent = Some (CTE parent_cap parent_node); valid_badges m; mdbNext parent_node \<noteq> 0; (if mdbNext parent_node = site then Some (CTE c' (MDB (mdbNext parent_node) parent True True)) else m (mdbNext parent_node)) = Some cte; isMDBParentOf (CTE c' (MDB (mdbNext parent_node) parent True True)) cte; mdbNext parent_node \<noteq> site\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>cte. \<lbrakk>m parent = Some (CTE parent_cap parent_node); valid_badges m; mdbNext parent_node \<noteq> 0; (if mdbNext parent_node = site then Some (CTE c' (MDB (mdbNext parent_node) parent True True)) else m (mdbNext parent_node)) = Some cte; isMDBParentOf (CTE c' (MDB (mdbNext parent_node) parent True True)) cte; mdbNext parent_node = site; m \<turnstile> parent \<leadsto> site\<rbrakk> \<Longrightarrow> False
 2. \<And>cte. \<lbrakk>m parent = Some (CTE parent_cap parent_node); valid_badges m; mdbNext parent_node \<noteq> 0; (if mdbNext parent_node = site then Some (CTE c' (MDB (mdbNext parent_node) parent True True)) else m (mdbNext parent_node)) = Some cte; isMDBParentOf (CTE c' (MDB (mdbNext parent_node) parent True True)) cte; mdbNext parent_node = site\<rbrakk> \<Longrightarrow> m \<turnstile> parent \<leadsto> site
 3. \<And>cte. \<lbrakk>m parent = Some (CTE parent_cap parent_node); valid_badges m; mdbNext parent_node \<noteq> 0; (if mdbNext parent_node = site then Some (CTE c' (MDB (mdbNext parent_node) parent True True)) else m (mdbNext parent_node)) = Some cte; isMDBParentOf (CTE c' (MDB (mdbNext parent_node) parent True True)) cte; mdbNext parent_node \<noteq> site\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>cte. \<lbrakk>m parent = Some (CTE parent_cap parent_node); valid_badges m; mdbNext parent_node \<noteq> 0; (if mdbNext parent_node = site then Some (CTE c' (MDB (mdbNext parent_node) parent True True)) else m (mdbNext parent_node)) = Some cte; isMDBParentOf (CTE c' (MDB (mdbNext parent_node) parent True True)) cte; mdbNext parent_node = site\<rbrakk> \<Longrightarrow> m \<turnstile> parent \<leadsto> site
 2. \<And>cte. \<lbrakk>m parent = Some (CTE parent_cap parent_node); valid_badges m; mdbNext parent_node \<noteq> 0; (if mdbNext parent_node = site then Some (CTE c' (MDB (mdbNext parent_node) parent True True)) else m (mdbNext parent_node)) = Some cte; isMDBParentOf (CTE c' (MDB (mdbNext parent_node) parent True True)) cte; mdbNext parent_node \<noteq> site\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>cte. \<lbrakk>m parent = Some (CTE parent_cap parent_node); valid_badges m; mdbNext parent_node \<noteq> 0; (if mdbNext parent_node = site then Some (CTE c' (MDB (mdbNext parent_node) parent True True)) else m (mdbNext parent_node)) = Some cte; isMDBParentOf (CTE c' (MDB (mdbNext parent_node) parent True True)) cte; mdbNext parent_node = site\<rbrakk> \<Longrightarrow> \<exists>z. m parent = Some z \<and> site = mdbNext (cteMDBNode z)
 2. \<And>cte. \<lbrakk>m parent = Some (CTE parent_cap parent_node); valid_badges m; mdbNext parent_node \<noteq> 0; (if mdbNext parent_node = site then Some (CTE c' (MDB (mdbNext parent_node) parent True True)) else m (mdbNext parent_node)) = Some cte; isMDBParentOf (CTE c' (MDB (mdbNext parent_node) parent True True)) cte; mdbNext parent_node \<noteq> site\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>cte. \<lbrakk>m parent = Some (CTE parent_cap parent_node); valid_badges m; mdbNext parent_node \<noteq> 0; (if mdbNext parent_node = site then Some (CTE c' (MDB (mdbNext parent_node) parent True True)) else m (mdbNext parent_node)) = Some cte; isMDBParentOf (CTE c' (MDB (mdbNext parent_node) parent True True)) cte; mdbNext parent_node \<noteq> site\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>cte. \<lbrakk>m parent = Some (CTE parent_cap parent_node); valid_badges m; mdbNext parent_node \<noteq> 0; m (mdbNext parent_node) = Some cte; isMDBParentOf (CTE c' (MDB (mdbNext parent_node) parent True True)) cte; mdbNext parent_node \<noteq> site\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!