theory Detype_R

lemma trancl_next[elim]:
  "\<lbrakk> ctes_of s \<turnstile> x \<leadsto>\<^sup>+ y; x \<notin> base_bits \<rbrakk> \<Longrightarrow> ctes' \<turnstile> x \<leadsto>\<^sup>+ y" apply (erule rev_mp, erule converse_trancl_induct) apply clarsimp apply (rule r_into_trancl) apply (simp add: next_unfold' tree_to_ctes) apply clarsimp apply (rule_tac b=z in trancl_into_trancl2) apply (simp add: next_unfold' tree_to_ctes) apply (case_tac "z = 0") apply (insert no_0)[1] apply (erule tranclE2) apply (simp add: next_unfold') apply (simp add: next_unfold') apply (drule(1) mdb_dest) apply (simp add: next_unfold') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ctes_of s \<turnstile> x \<leadsto>\<^sup>+ y; x \<notin> base_bits\<rbrakk> \<Longrightarrow> ctes' \<turnstile> x \<leadsto>\<^sup>+ y proof (prove)
goal (2 subgoals):
 1. \<And>ya. ctes_of s \<turnstile> ya \<leadsto> y \<Longrightarrow> ya \<notin> base_bits \<longrightarrow> ctes' \<turnstile> ya \<leadsto>\<^sup>+ y
 2. \<And>ya z. \<lbrakk>ctes_of s \<turnstile> ya \<leadsto> z; ctes_of s \<turnstile> z \<leadsto>\<^sup>+ y; z \<notin> base_bits \<longrightarrow> ctes' \<turnstile> z \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> ya \<notin> base_bits \<longrightarrow> ctes' \<turnstile> ya \<leadsto>\<^sup>+ y proof (prove)
goal (2 subgoals):
 1. \<And>ya. \<lbrakk>ctes_of s \<turnstile> ya \<leadsto> y; base \<le> ya \<longrightarrow> \<not> ya \<le> base + (2 ^ bits - 1)\<rbrakk> \<Longrightarrow> ctes' \<turnstile> ya \<leadsto>\<^sup>+ y
 2. \<And>ya z. \<lbrakk>ctes_of s \<turnstile> ya \<leadsto> z; ctes_of s \<turnstile> z \<leadsto>\<^sup>+ y; z \<notin> base_bits \<longrightarrow> ctes' \<turnstile> z \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> ya \<notin> base_bits \<longrightarrow> ctes' \<turnstile> ya \<leadsto>\<^sup>+ y proof (prove)
goal (2 subgoals):
 1. \<And>ya. \<lbrakk>ctes_of s \<turnstile> ya \<leadsto> y; base \<le> ya \<longrightarrow> \<not> ya \<le> base + (2 ^ bits - 1)\<rbrakk> \<Longrightarrow> ctes' \<turnstile> ya \<leadsto> y
 2. \<And>ya z. \<lbrakk>ctes_of s \<turnstile> ya \<leadsto> z; ctes_of s \<turnstile> z \<leadsto>\<^sup>+ y; z \<notin> base_bits \<longrightarrow> ctes' \<turnstile> z \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> ya \<notin> base_bits \<longrightarrow> ctes' \<turnstile> ya \<leadsto>\<^sup>+ y proof (prove)
goal (1 subgoal):
 1. \<And>ya z. \<lbrakk>ctes_of s \<turnstile> ya \<leadsto> z; ctes_of s \<turnstile> z \<leadsto>\<^sup>+ y; z \<notin> base_bits \<longrightarrow> ctes' \<turnstile> z \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> ya \<notin> base_bits \<longrightarrow> ctes' \<turnstile> ya \<leadsto>\<^sup>+ y proof (prove)
goal (1 subgoal):
 1. \<And>ya z. \<lbrakk>ctes_of s \<turnstile> ya \<leadsto> z; ctes_of s \<turnstile> z \<leadsto>\<^sup>+ y; (base \<le> z \<longrightarrow> \<not> z \<le> base + (2 ^ bits - 1)) \<longrightarrow> ctes' \<turnstile> z \<leadsto>\<^sup>+ y; base \<le> ya \<longrightarrow> \<not> ya \<le> base + (2 ^ bits - 1)\<rbrakk> \<Longrightarrow> ctes' \<turnstile> ya \<leadsto>\<^sup>+ y proof (prove)
goal (2 subgoals):
 1. \<And>ya z. \<lbrakk>ctes_of s \<turnstile> ya \<leadsto> z; ctes_of s \<turnstile> z \<leadsto>\<^sup>+ y; (base \<le> z \<longrightarrow> \<not> z \<le> base + (2 ^ bits - 1)) \<longrightarrow> ctes' \<turnstile> z \<leadsto>\<^sup>+ y; base \<le> ya \<longrightarrow> \<not> ya \<le> base + (2 ^ bits - 1)\<rbrakk> \<Longrightarrow> ctes' \<turnstile> ya \<leadsto> z
 2. \<And>ya z. \<lbrakk>ctes_of s \<turnstile> ya \<leadsto> z; ctes_of s \<turnstile> z \<leadsto>\<^sup>+ y; (base \<le> z \<longrightarrow> \<not> z \<le> base + (2 ^ bits - 1)) \<longrightarrow> ctes' \<turnstile> z \<leadsto>\<^sup>+ y; base \<le> ya \<longrightarrow> \<not> ya \<le> base + (2 ^ bits - 1)\<rbrakk> \<Longrightarrow> ctes' \<turnstile> z \<leadsto>\<^sup>+ y proof (prove)
goal (1 subgoal):
 1. \<And>ya z. \<lbrakk>ctes_of s \<turnstile> ya \<leadsto> z; ctes_of s \<turnstile> z \<leadsto>\<^sup>+ y; (base \<le> z \<longrightarrow> \<not> z \<le> base + (2 ^ bits - 1)) \<longrightarrow> ctes' \<turnstile> z \<leadsto>\<^sup>+ y; base \<le> ya \<longrightarrow> \<not> ya \<le> base + (2 ^ bits - 1)\<rbrakk> \<Longrightarrow> ctes' \<turnstile> z \<leadsto>\<^sup>+ y proof (prove)
goal (2 subgoals):
 1. \<And>ya z. \<lbrakk>ctes_of s \<turnstile> ya \<leadsto> z; ctes_of s \<turnstile> z \<leadsto>\<^sup>+ y; (base \<le> z \<longrightarrow> \<not> z \<le> base + (2 ^ bits - 1)) \<longrightarrow> ctes' \<turnstile> z \<leadsto>\<^sup>+ y; base \<le> ya \<longrightarrow> \<not> ya \<le> base + (2 ^ bits - 1); z = 0\<rbrakk> \<Longrightarrow> ctes' \<turnstile> z \<leadsto>\<^sup>+ y
 2. \<And>ya z. \<lbrakk>ctes_of s \<turnstile> ya \<leadsto> z; ctes_of s \<turnstile> z \<leadsto>\<^sup>+ y; (base \<le> z \<longrightarrow> \<not> z \<le> base + (2 ^ bits - 1)) \<longrightarrow> ctes' \<turnstile> z \<leadsto>\<^sup>+ y; base \<le> ya \<longrightarrow> \<not> ya \<le> base + (2 ^ bits - 1); z \<noteq> 0\<rbrakk> \<Longrightarrow> ctes' \<turnstile> z \<leadsto>\<^sup>+ y proof (prove)
goal (2 subgoals):
 1. \<And>ya z. \<lbrakk>ctes_of s \<turnstile> ya \<leadsto> z; ctes_of s \<turnstile> z \<leadsto>\<^sup>+ y; (base \<le> z \<longrightarrow> \<not> z \<le> base + (2 ^ bits - 1)) \<longrightarrow> ctes' \<turnstile> z \<leadsto>\<^sup>+ y; base \<le> ya \<longrightarrow> \<not> ya \<le> base + (2 ^ bits - 1); z = 0; no_0 (ctes_of s)\<rbrakk> \<Longrightarrow> ctes' \<turnstile> z \<leadsto>\<^sup>+ y
 2. \<And>ya z. \<lbrakk>ctes_of s \<turnstile> ya \<leadsto> z; ctes_of s \<turnstile> z \<leadsto>\<^sup>+ y; (base \<le> z \<longrightarrow> \<not> z \<le> base + (2 ^ bits - 1)) \<longrightarrow> ctes' \<turnstile> z \<leadsto>\<^sup>+ y; base \<le> ya \<longrightarrow> \<not> ya \<le> base + (2 ^ bits - 1); z \<noteq> 0\<rbrakk> \<Longrightarrow> ctes' \<turnstile> z \<leadsto>\<^sup>+ y proof (prove)
goal (3 subgoals):
 1. \<And>ya z. \<lbrakk>ctes_of s \<turnstile> ya \<leadsto> z; (base \<le> z \<longrightarrow> \<not> z \<le> base + (2 ^ bits - 1)) \<longrightarrow> ctes' \<turnstile> z \<leadsto>\<^sup>+ y; base \<le> ya \<longrightarrow> \<not> ya \<le> base + (2 ^ bits - 1); z = 0; no_0 (ctes_of s); ctes_of s \<turnstile> z \<leadsto> y\<rbrakk> \<Longrightarrow> ctes' \<turnstile> z \<leadsto>\<^sup>+ y
 2. \<And>ya z c. \<lbrakk>ctes_of s \<turnstile> ya \<leadsto> z; (base \<le> z \<longrightarrow> \<not> z \<le> base + (2 ^ bits - 1)) \<longrightarrow> ctes' \<turnstile> z \<leadsto>\<^sup>+ y; base \<le> ya \<longrightarrow> \<not> ya \<le> base + (2 ^ bits - 1); z = 0; no_0 (ctes_of s); ctes_of s \<turnstile> z \<leadsto> c; ctes_of s \<turnstile> c \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> ctes' \<turnstile> z \<leadsto>\<^sup>+ y
 3. \<And>ya z. \<lbrakk>ctes_of s \<turnstile> ya \<leadsto> z; ctes_of s \<turnstile> z \<leadsto>\<^sup>+ y; (base \<le> z \<longrightarrow> \<not> z \<le> base + (2 ^ bits - 1)) \<longrightarrow> ctes' \<turnstile> z \<leadsto>\<^sup>+ y; base \<le> ya \<longrightarrow> \<not> ya \<le> base + (2 ^ bits - 1); z \<noteq> 0\<rbrakk> \<Longrightarrow> ctes' \<turnstile> z \<leadsto>\<^sup>+ y proof (prove)
goal (2 subgoals):
 1. \<And>ya z c. \<lbrakk>ctes_of s \<turnstile> ya \<leadsto> z; (base \<le> z \<longrightarrow> \<not> z \<le> base + (2 ^ bits - 1)) \<longrightarrow> ctes' \<turnstile> z \<leadsto>\<^sup>+ y; base \<le> ya \<longrightarrow> \<not> ya \<le> base + (2 ^ bits - 1); z = 0; no_0 (ctes_of s); ctes_of s \<turnstile> z \<leadsto> c; ctes_of s \<turnstile> c \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> ctes' \<turnstile> z \<leadsto>\<^sup>+ y
 2. \<And>ya z. \<lbrakk>ctes_of s \<turnstile> ya \<leadsto> z; ctes_of s \<turnstile> z \<leadsto>\<^sup>+ y; (base \<le> z \<longrightarrow> \<not> z \<le> base + (2 ^ bits - 1)) \<longrightarrow> ctes' \<turnstile> z \<leadsto>\<^sup>+ y; base \<le> ya \<longrightarrow> \<not> ya \<le> base + (2 ^ bits - 1); z \<noteq> 0\<rbrakk> \<Longrightarrow> ctes' \<turnstile> z \<leadsto>\<^sup>+ y proof (prove)
goal (1 subgoal):
 1. \<And>ya z. \<lbrakk>ctes_of s \<turnstile> ya \<leadsto> z; ctes_of s \<turnstile> z \<leadsto>\<^sup>+ y; (base \<le> z \<longrightarrow> \<not> z \<le> base + (2 ^ bits - 1)) \<longrightarrow> ctes' \<turnstile> z \<leadsto>\<^sup>+ y; base \<le> ya \<longrightarrow> \<not> ya \<le> base + (2 ^ bits - 1); z \<noteq> 0\<rbrakk> \<Longrightarrow> ctes' \<turnstile> z \<leadsto>\<^sup>+ y proof (prove)
goal (1 subgoal):
 1. \<And>ya z. \<lbrakk>ctes_of s \<turnstile> z \<leadsto>\<^sup>+ y; (base \<le> z \<longrightarrow> \<not> z \<le> base + (2 ^ bits - 1)) \<longrightarrow> ctes' \<turnstile> z \<leadsto>\<^sup>+ y; base \<le> ya \<longrightarrow> \<not> ya \<le> base + (2 ^ bits - 1); z \<noteq> 0; z \<notin> base_bits\<rbrakk> \<Longrightarrow> ctes' \<turnstile> z \<leadsto>\<^sup>+ y proof (prove)
goal:
No subgoals!