theory Retype_C

lemma ptr_retyps_out:
  fixes p :: "'a :: mem_type ptr"
  shows "x \<notin> {ptr_val p..+n * size_of TYPE('a)} \<Longrightarrow> ptr_retyps n p td x = td x" proof (induct n arbitrary: p) case 0 thus ?case by simp next case (Suc m) have ih: "ptr_retyps m (CTypesDefs.ptr_add p 1) td x = td x" proof (rule Suc.hyps) from Suc.prems show "x \<notin> {ptr_val (CTypesDefs.ptr_add p 1)..+m * size_of TYPE('a)}" apply (rule contrapos_nn) apply (erule subsetD [rotated]) apply (simp add: CTypesDefs.ptr_add_def) apply (rule intvl_sub_offset) apply (simp add: unat_of_nat) done qed from Suc.prems have "x \<notin> {ptr_val p..+size_of TYPE('a)}" apply (rule contrapos_nn) apply (erule subsetD [rotated]) apply (rule intvl_start_le) apply simp done thus ?case by (simp add: ptr_retyp_d ih) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<notin> {ptr_val p..+n * size_of TYPE('a)} \<Longrightarrow> ptr_retyps n p td x = td x proof (state)
goal (2 subgoals):
 1. \<And>p. x \<notin> {ptr_val p..+0 * size_of TYPE('a)} \<Longrightarrow> ptr_retyps 0 p td x = td x
 2. \<And>n p. \<lbrakk>\<And>p. x \<notin> {ptr_val p..+n * size_of TYPE('a)} \<Longrightarrow> ptr_retyps n p td x = td x; x \<notin> {ptr_val p..+Suc n * size_of TYPE('a)}\<rbrakk> \<Longrightarrow> ptr_retyps (Suc n) p td x = td x proof (state)
this:
x \<notin> {ptr_val p..+0 * size_of TYPE('a)}

goal (2 subgoals):
 1. \<And>p. x \<notin> {ptr_val p..+0 * size_of TYPE('a)} \<Longrightarrow> ptr_retyps 0 p td x = td x
 2. \<And>n p. \<lbrakk>\<And>p. x \<notin> {ptr_val p..+n * size_of TYPE('a)} \<Longrightarrow> ptr_retyps n p td x = td x; x \<notin> {ptr_val p..+Suc n * size_of TYPE('a)}\<rbrakk> \<Longrightarrow> ptr_retyps (Suc n) p td x = td x proof (prove)
using this:
x \<notin> {ptr_val p..+0 * size_of TYPE('a)}

goal (1 subgoal):
 1. ptr_retyps 0 p td x = td x proof (state)
this:
ptr_retyps 0 p td x = td x

goal (1 subgoal):
 1. \<And>n p. \<lbrakk>\<And>p. x \<notin> {ptr_val p..+n * size_of TYPE('a)} \<Longrightarrow> ptr_retyps n p td x = td x; x \<notin> {ptr_val p..+Suc n * size_of TYPE('a)}\<rbrakk> \<Longrightarrow> ptr_retyps (Suc n) p td x = td x proof (state)
goal (1 subgoal):
 1. \<And>n p. \<lbrakk>\<And>p. x \<notin> {ptr_val p..+n * size_of TYPE('a)} \<Longrightarrow> ptr_retyps n p td x = td x; x \<notin> {ptr_val p..+Suc n * size_of TYPE('a)}\<rbrakk> \<Longrightarrow> ptr_retyps (Suc n) p td x = td x proof (state)
this:
x \<notin> {ptr_val ?p2..+m * size_of TYPE('a)} \<Longrightarrow> ptr_retyps m ?p2 td x = td x
x \<notin> {ptr_val p..+Suc m * size_of TYPE('a)}

goal (1 subgoal):
 1. \<And>n p. \<lbrakk>\<And>p. x \<notin> {ptr_val p..+n * size_of TYPE('a)} \<Longrightarrow> ptr_retyps n p td x = td x; x \<notin> {ptr_val p..+Suc n * size_of TYPE('a)}\<rbrakk> \<Longrightarrow> ptr_retyps (Suc n) p td x = td x proof (prove)
goal (1 subgoal):
 1. ptr_retyps m (p +\<^sub>p 1) td x = td x proof (state)
goal (1 subgoal):
 1. x \<notin> {ptr_val (p +\<^sub>p 1)..+m * size_of TYPE('a)} proof (chain)
picking this:
x \<notin> {ptr_val p..+Suc m * size_of TYPE('a)} proof (prove)
using this:
x \<notin> {ptr_val p..+Suc m * size_of TYPE('a)}

goal (1 subgoal):
 1. x \<notin> {ptr_val (p +\<^sub>p 1)..+m * size_of TYPE('a)} proof (prove)
goal (1 subgoal):
 1. x \<in> {ptr_val (p +\<^sub>p 1)..+m * size_of TYPE('a)} \<Longrightarrow> x \<in> {ptr_val p..+Suc m * size_of TYPE('a)} proof (prove)
goal (1 subgoal):
 1. {ptr_val (p +\<^sub>p 1)..+m * size_of TYPE('a)} \<subseteq> {ptr_val p..+Suc m * size_of TYPE('a)} proof (prove)
goal (1 subgoal):
 1. {ptr_val p + word_of_nat (size_of TYPE('a))..+m * size_of TYPE('a)} \<subseteq> {ptr_val p..+size_of TYPE('a) + m * size_of TYPE('a)} proof (prove)
goal (1 subgoal):
 1. unat (word_of_nat (size_of TYPE('a))) + m * size_of TYPE('a) \<le> size_of TYPE('a) + m * size_of TYPE('a) proof (prove)
goal:
No subgoals! proof (state)
this:
x \<notin> {ptr_val (p +\<^sub>p 1)..+m * size_of TYPE('a)}

goal:
No subgoals! proof (state)
this:
ptr_retyps m (p +\<^sub>p 1) td x = td x

goal (1 subgoal):
 1. \<And>n p. \<lbrakk>\<And>p. x \<notin> {ptr_val p..+n * size_of TYPE('a)} \<Longrightarrow> ptr_retyps n p td x = td x; x \<notin> {ptr_val p..+Suc n * size_of TYPE('a)}\<rbrakk> \<Longrightarrow> ptr_retyps (Suc n) p td x = td x proof (chain)
picking this:
x \<notin> {ptr_val p..+Suc m * size_of TYPE('a)} proof (prove)
using this:
x \<notin> {ptr_val p..+Suc m * size_of TYPE('a)}

goal (1 subgoal):
 1. x \<notin> ptr_span p proof (prove)
goal (1 subgoal):
 1. x \<in> ptr_span p \<Longrightarrow> x \<in> {ptr_val p..+Suc m * size_of TYPE('a)} proof (prove)
goal (1 subgoal):
 1. ptr_span p \<subseteq> {ptr_val p..+Suc m * size_of TYPE('a)} proof (prove)
goal (1 subgoal):
 1. size_of TYPE('a) \<le> Suc m * size_of TYPE('a) proof (prove)
goal:
No subgoals! proof (state)
this:
x \<notin> ptr_span p

goal (1 subgoal):
 1. \<And>n p. \<lbrakk>\<And>p. x \<notin> {ptr_val p..+n * size_of TYPE('a)} \<Longrightarrow> ptr_retyps n p td x = td x; x \<notin> {ptr_val p..+Suc n * size_of TYPE('a)}\<rbrakk> \<Longrightarrow> ptr_retyps (Suc n) p td x = td x proof (prove)
using this:
x \<notin> ptr_span p

goal (1 subgoal):
 1. ptr_retyps (Suc m) p td x = td x proof (state)
this:
ptr_retyps (Suc m) p td x = td x

goal:
No subgoals!