theory Detype_R

lemma mdb_parent:
  "ctes_of s \<turnstile> x \<rightarrow> y \<Longrightarrow> ctes' \<turnstile> x \<rightarrow> y" apply (erule subtree.induct) apply (frule(1) mdb_src, frule(1) mdb_dest) apply (rule subtree.direct_parent) apply (simp add: next_unfold' tree_to_ctes) apply assumption apply (simp add: parentOf_def tree_to_ctes) apply (frule(1) mdb_src, frule(1) mdb_dest) apply (erule subtree.trans_parent) apply (simp add: next_unfold' tree_to_ctes) apply assumption apply (frule mdb_parent_notrange) apply (simp add: parentOf_def tree_to_ctes) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ctes_of s \<turnstile> x \<rightarrow> y \<Longrightarrow> ctes' \<turnstile> x \<rightarrow> y proof (prove)
goal (2 subgoals):
 1. \<And>c'. \<lbrakk>ctes_of s \<turnstile> x \<leadsto> c'; c' \<noteq> 0; ctes_of s \<turnstile> x parentOf c'\<rbrakk> \<Longrightarrow> ctes' \<turnstile> x \<rightarrow> c'
 2. \<And>c' c''. \<lbrakk>ctes_of s \<turnstile> x \<rightarrow> c'; ctes' \<turnstile> x \<rightarrow> c'; ctes_of s \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; ctes_of s \<turnstile> x parentOf c''\<rbrakk> \<Longrightarrow> ctes' \<turnstile> x \<rightarrow> c'' proof (prove)
goal (2 subgoals):
 1. \<And>c'. \<lbrakk>ctes_of s \<turnstile> x \<leadsto> c'; c' \<noteq> 0; ctes_of s \<turnstile> x parentOf c'; x \<notin> base_bits; c' \<notin> base_bits\<rbrakk> \<Longrightarrow> ctes' \<turnstile> x \<rightarrow> c'
 2. \<And>c' c''. \<lbrakk>ctes_of s \<turnstile> x \<rightarrow> c'; ctes' \<turnstile> x \<rightarrow> c'; ctes_of s \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; ctes_of s \<turnstile> x parentOf c''\<rbrakk> \<Longrightarrow> ctes' \<turnstile> x \<rightarrow> c'' proof (prove)
goal (4 subgoals):
 1. \<And>c'. \<lbrakk>ctes_of s \<turnstile> x \<leadsto> c'; c' \<noteq> 0; ctes_of s \<turnstile> x parentOf c'; x \<notin> base_bits; c' \<notin> base_bits\<rbrakk> \<Longrightarrow> ctes' \<turnstile> x \<leadsto> c'
 2. \<And>c'. \<lbrakk>ctes_of s \<turnstile> x \<leadsto> c'; c' \<noteq> 0; ctes_of s \<turnstile> x parentOf c'; x \<notin> base_bits; c' \<notin> base_bits\<rbrakk> \<Longrightarrow> c' \<noteq> 0
 3. \<And>c'. \<lbrakk>ctes_of s \<turnstile> x \<leadsto> c'; c' \<noteq> 0; ctes_of s \<turnstile> x parentOf c'; x \<notin> base_bits; c' \<notin> base_bits\<rbrakk> \<Longrightarrow> ctes' \<turnstile> x parentOf c'
 4. \<And>c' c''. \<lbrakk>ctes_of s \<turnstile> x \<rightarrow> c'; ctes' \<turnstile> x \<rightarrow> c'; ctes_of s \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; ctes_of s \<turnstile> x parentOf c''\<rbrakk> \<Longrightarrow> ctes' \<turnstile> x \<rightarrow> c'' proof (prove)
goal (3 subgoals):
 1. \<And>c'. \<lbrakk>ctes_of s \<turnstile> x \<leadsto> c'; c' \<noteq> 0; ctes_of s \<turnstile> x parentOf c'; x \<notin> base_bits; c' \<notin> base_bits\<rbrakk> \<Longrightarrow> c' \<noteq> 0
 2. \<And>c'. \<lbrakk>ctes_of s \<turnstile> x \<leadsto> c'; c' \<noteq> 0; ctes_of s \<turnstile> x parentOf c'; x \<notin> base_bits; c' \<notin> base_bits\<rbrakk> \<Longrightarrow> ctes' \<turnstile> x parentOf c'
 3. \<And>c' c''. \<lbrakk>ctes_of s \<turnstile> x \<rightarrow> c'; ctes' \<turnstile> x \<rightarrow> c'; ctes_of s \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; ctes_of s \<turnstile> x parentOf c''\<rbrakk> \<Longrightarrow> ctes' \<turnstile> x \<rightarrow> c'' proof (prove)
goal (2 subgoals):
 1. \<And>c'. \<lbrakk>ctes_of s \<turnstile> x \<leadsto> c'; c' \<noteq> 0; ctes_of s \<turnstile> x parentOf c'; x \<notin> base_bits; c' \<notin> base_bits\<rbrakk> \<Longrightarrow> ctes' \<turnstile> x parentOf c'
 2. \<And>c' c''. \<lbrakk>ctes_of s \<turnstile> x \<rightarrow> c'; ctes' \<turnstile> x \<rightarrow> c'; ctes_of s \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; ctes_of s \<turnstile> x parentOf c''\<rbrakk> \<Longrightarrow> ctes' \<turnstile> x \<rightarrow> c'' proof (prove)
goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>ctes_of s \<turnstile> x \<rightarrow> c'; ctes' \<turnstile> x \<rightarrow> c'; ctes_of s \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; ctes_of s \<turnstile> x parentOf c''\<rbrakk> \<Longrightarrow> ctes' \<turnstile> x \<rightarrow> c'' proof (prove)
goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>ctes_of s \<turnstile> x \<rightarrow> c'; ctes' \<turnstile> x \<rightarrow> c'; ctes_of s \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; ctes_of s \<turnstile> x parentOf c''; c' \<notin> base_bits; c'' \<notin> base_bits\<rbrakk> \<Longrightarrow> ctes' \<turnstile> x \<rightarrow> c'' proof (prove)
goal (3 subgoals):
 1. \<And>c' c''. \<lbrakk>ctes_of s \<turnstile> x \<rightarrow> c'; ctes_of s \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; ctes_of s \<turnstile> x parentOf c''; c' \<notin> base_bits; c'' \<notin> base_bits\<rbrakk> \<Longrightarrow> ctes' \<turnstile> c' \<leadsto> c''
 2. \<And>c' c''. \<lbrakk>ctes_of s \<turnstile> x \<rightarrow> c'; ctes_of s \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; ctes_of s \<turnstile> x parentOf c''; c' \<notin> base_bits; c'' \<notin> base_bits\<rbrakk> \<Longrightarrow> c'' \<noteq> 0
 3. \<And>c' c''. \<lbrakk>ctes_of s \<turnstile> x \<rightarrow> c'; ctes_of s \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; ctes_of s \<turnstile> x parentOf c''; c' \<notin> base_bits; c'' \<notin> base_bits\<rbrakk> \<Longrightarrow> ctes' \<turnstile> x parentOf c'' proof (prove)
goal (2 subgoals):
 1. \<And>c' c''. \<lbrakk>ctes_of s \<turnstile> x \<rightarrow> c'; ctes_of s \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; ctes_of s \<turnstile> x parentOf c''; c' \<notin> base_bits; c'' \<notin> base_bits\<rbrakk> \<Longrightarrow> c'' \<noteq> 0
 2. \<And>c' c''. \<lbrakk>ctes_of s \<turnstile> x \<rightarrow> c'; ctes_of s \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; ctes_of s \<turnstile> x parentOf c''; c' \<notin> base_bits; c'' \<notin> base_bits\<rbrakk> \<Longrightarrow> ctes' \<turnstile> x parentOf c'' proof (prove)
goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>ctes_of s \<turnstile> x \<rightarrow> c'; ctes_of s \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; ctes_of s \<turnstile> x parentOf c''; c' \<notin> base_bits; c'' \<notin> base_bits\<rbrakk> \<Longrightarrow> ctes' \<turnstile> x parentOf c'' proof (prove)
goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>ctes_of s \<turnstile> x \<rightarrow> c'; ctes_of s \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; ctes_of s \<turnstile> x parentOf c''; c' \<notin> base_bits; c'' \<notin> base_bits; x \<notin> base_bits \<and> c' \<notin> base_bits\<rbrakk> \<Longrightarrow> ctes' \<turnstile> x parentOf c'' proof (prove)
goal:
No subgoals!