theory Detype_C

lemma tcb_ptr_to_ctcb_ptr_to_Ptr:
  "tcb_ptr_to_ctcb_ptr ` {p..+b} = Ptr ` {p + ctcb_offset..+b}" apply (simp add:  tcb_ptr_to_ctcb_ptr_comp image_comp [symmetric]) apply (rule equalityI) apply clarsimp apply (rule imageI) apply (drule intvlD) apply clarsimp apply (subgoal_tac "p + ctcb_offset + of_nat k \<in> {p + ctcb_offset..+b}") apply (simp add: field_simps) apply (erule intvlI) apply clarsimp apply (drule intvlD) apply clarsimp apply (rule image_eqI) apply simp apply (erule intvlI) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tcb_ptr_to_ctcb_ptr ` {p..+b} = tcb_Ptr ` {p + ctcb_offset..+b} proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. tcb_Ptr (x + ctcb_offset)) ` {p..+b} = tcb_Ptr ` {p + ctcb_offset..+b} proof (prove)
goal (2 subgoals):
 1. (\<lambda>x. tcb_Ptr (x + ctcb_offset)) ` {p..+b} \<subseteq> tcb_Ptr ` {p + ctcb_offset..+b}
 2. tcb_Ptr ` {p + ctcb_offset..+b} \<subseteq> (\<lambda>x. tcb_Ptr (x + ctcb_offset)) ` {p..+b} proof (prove)
goal (2 subgoals):
 1. \<And>xa. xa \<in> {p..+b} \<Longrightarrow> tcb_Ptr (xa + ctcb_offset) \<in> tcb_Ptr ` {p + ctcb_offset..+b}
 2. tcb_Ptr ` {p + ctcb_offset..+b} \<subseteq> (\<lambda>x. tcb_Ptr (x + ctcb_offset)) ` {p..+b} proof (prove)
goal (2 subgoals):
 1. \<And>xa. xa \<in> {p..+b} \<Longrightarrow> xa + ctcb_offset \<in> {p + ctcb_offset..+b}
 2. tcb_Ptr ` {p + ctcb_offset..+b} \<subseteq> (\<lambda>x. tcb_Ptr (x + ctcb_offset)) ` {p..+b} proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<exists>k. xa = p + word_of_nat k \<and> k < b \<Longrightarrow> xa + ctcb_offset \<in> {p + ctcb_offset..+b}
 2. tcb_Ptr ` {p + ctcb_offset..+b} \<subseteq> (\<lambda>x. tcb_Ptr (x + ctcb_offset)) ` {p..+b} proof (prove)
goal (2 subgoals):
 1. \<And>k. k < b \<Longrightarrow> p + word_of_nat k + ctcb_offset \<in> {p + ctcb_offset..+b}
 2. tcb_Ptr ` {p + ctcb_offset..+b} \<subseteq> (\<lambda>x. tcb_Ptr (x + ctcb_offset)) ` {p..+b} proof (prove)
goal (3 subgoals):
 1. \<And>k. \<lbrakk>k < b; p + ctcb_offset + word_of_nat k \<in> {p + ctcb_offset..+b}\<rbrakk> \<Longrightarrow> p + word_of_nat k + ctcb_offset \<in> {p + ctcb_offset..+b}
 2. \<And>k. k < b \<Longrightarrow> p + ctcb_offset + word_of_nat k \<in> {p + ctcb_offset..+b}
 3. tcb_Ptr ` {p + ctcb_offset..+b} \<subseteq> (\<lambda>x. tcb_Ptr (x + ctcb_offset)) ` {p..+b} proof (prove)
goal (2 subgoals):
 1. \<And>k. k < b \<Longrightarrow> p + ctcb_offset + word_of_nat k \<in> {p + ctcb_offset..+b}
 2. tcb_Ptr ` {p + ctcb_offset..+b} \<subseteq> (\<lambda>x. tcb_Ptr (x + ctcb_offset)) ` {p..+b} proof (prove)
goal (1 subgoal):
 1. tcb_Ptr ` {p + ctcb_offset..+b} \<subseteq> (\<lambda>x. tcb_Ptr (x + ctcb_offset)) ` {p..+b} proof (prove)
goal (1 subgoal):
 1. \<And>xa. xa \<in> {p + ctcb_offset..+b} \<Longrightarrow> tcb_Ptr xa \<in> (\<lambda>x. tcb_Ptr (x + ctcb_offset)) ` {p..+b} proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<exists>k. xa = p + ctcb_offset + word_of_nat k \<and> k < b \<Longrightarrow> tcb_Ptr xa \<in> (\<lambda>x. tcb_Ptr (x + ctcb_offset)) ` {p..+b} proof (prove)
goal (1 subgoal):
 1. \<And>k. k < b \<Longrightarrow> tcb_Ptr (p + ctcb_offset + word_of_nat k) \<in> (\<lambda>x. tcb_Ptr (x + ctcb_offset)) ` {p..+b} proof (prove)
goal (2 subgoals):
 1. \<And>k. k < b \<Longrightarrow> tcb_Ptr (p + ctcb_offset + word_of_nat k) = tcb_Ptr (?x33 k + ctcb_offset)
 2. \<And>k. k < b \<Longrightarrow> ?x33 k \<in> {p..+b} proof (prove)
goal (1 subgoal):
 1. \<And>k. k < b \<Longrightarrow> p + word_of_nat k \<in> {p..+b} proof (prove)
goal:
No subgoals!