theory Retype_C

lemma h_t_valid_ptr_retyps_gen:
  assumes sz: "nptrs * size_of TYPE('a :: mem_type) < addr_card"
    and gd: "gd p'"
  shows
  "(p' \<in> ((+\<^sub>p) (Ptr p :: 'a ptr) \<circ> int) ` {k. k < nptrs})
    \<Longrightarrow> h_t_valid (ptr_retyps_gen nptrs (Ptr p :: 'a ptr) arr htd) gd p'" using gd sz apply (cases arr, simp_all add: ptr_retyps_gen_def) apply (cases "nptrs = 0") apply simp apply (cut_tac h_t_array_valid_retyp[where p="Ptr p" and htd=htd, OF _ sz], simp_all) apply clarsimp apply (drule_tac k=x in h_t_array_valid_field, simp_all) apply (induct nptrs arbitrary: p htd) apply simp apply clarsimp apply (case_tac x, simp_all add: ptr_retyp_h_t_valid) apply (rule ptr_retyp_disjoint) apply (elim meta_allE, erule meta_mp, rule image_eqI[rotated], simp) apply (simp add: field_simps) apply simp apply (cut_tac p=p and z="size_of TYPE('a)"
    and k="Suc nat * size_of TYPE('a)" in init_intvl_disj) apply (erule order_le_less_trans[rotated]) apply (simp del: mult_Suc) apply (simp add: field_simps Int_ac) apply (erule disjoint_subset[rotated] disjoint_subset2[rotated]) apply (rule intvl_start_le, simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. p' \<in> ((+\<^sub>p) (PTR('a) p) \<circ> int) ` {k. k < nptrs} \<Longrightarrow> ptr_retyps_gen nptrs (PTR('a) p) arr htd,gd \<Turnstile>\<^sub>t p' proof (prove)
using this:
gd p'
nptrs * size_of TYPE('a) < addr_card

goal (1 subgoal):
 1. p' \<in> ((+\<^sub>p) (PTR('a) p) \<circ> int) ` {k. k < nptrs} \<Longrightarrow> ptr_retyps_gen nptrs (PTR('a) p) arr htd,gd \<Turnstile>\<^sub>t p' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p' \<in> (\<lambda>x. PTR('a) (p + word_of_nat x * word_of_nat (size_of TYPE('a)))) ` {k. k < nptrs}; arr; gd p'; nptrs * size_of TYPE('a) < addr_card\<rbrakk> \<Longrightarrow> ptr_arr_retyps nptrs (PTR('a) p) htd,gd \<Turnstile>\<^sub>t p'
 2. \<lbrakk>p' \<in> (\<lambda>x. PTR('a) (p + word_of_nat x * word_of_nat (size_of TYPE('a)))) ` {k. k < nptrs}; \<not> arr; gd p'; nptrs * size_of TYPE('a) < addr_card\<rbrakk> \<Longrightarrow> ptr_retyps nptrs (PTR('a) p) htd,gd \<Turnstile>\<^sub>t p' proof (prove)
goal (3 subgoals):
 1. \<lbrakk>p' \<in> (\<lambda>x. PTR('a) (p + word_of_nat x * word_of_nat (size_of TYPE('a)))) ` {k. k < nptrs}; arr; gd p'; nptrs * size_of TYPE('a) < addr_card; nptrs = 0\<rbrakk> \<Longrightarrow> ptr_arr_retyps nptrs (PTR('a) p) htd,gd \<Turnstile>\<^sub>t p'
 2. \<lbrakk>p' \<in> (\<lambda>x. PTR('a) (p + word_of_nat x * word_of_nat (size_of TYPE('a)))) ` {k. k < nptrs}; arr; gd p'; nptrs * size_of TYPE('a) < addr_card; nptrs \<noteq> 0\<rbrakk> \<Longrightarrow> ptr_arr_retyps nptrs (PTR('a) p) htd,gd \<Turnstile>\<^sub>t p'
 3. \<lbrakk>p' \<in> (\<lambda>x. PTR('a) (p + word_of_nat x * word_of_nat (size_of TYPE('a)))) ` {k. k < nptrs}; \<not> arr; gd p'; nptrs * size_of TYPE('a) < addr_card\<rbrakk> \<Longrightarrow> ptr_retyps nptrs (PTR('a) p) htd,gd \<Turnstile>\<^sub>t p' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p' \<in> (\<lambda>x. PTR('a) (p + word_of_nat x * word_of_nat (size_of TYPE('a)))) ` {k. k < nptrs}; arr; gd p'; nptrs * size_of TYPE('a) < addr_card; nptrs \<noteq> 0\<rbrakk> \<Longrightarrow> ptr_arr_retyps nptrs (PTR('a) p) htd,gd \<Turnstile>\<^sub>t p'
 2. \<lbrakk>p' \<in> (\<lambda>x. PTR('a) (p + word_of_nat x * word_of_nat (size_of TYPE('a)))) ` {k. k < nptrs}; \<not> arr; gd p'; nptrs * size_of TYPE('a) < addr_card\<rbrakk> \<Longrightarrow> ptr_retyps nptrs (PTR('a) p) htd,gd \<Turnstile>\<^sub>t p' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p' \<in> (\<lambda>x. PTR('a) (p + word_of_nat x * word_of_nat (size_of TYPE('a)))) ` {k. k < nptrs}; arr; gd p'; nptrs * size_of TYPE('a) < addr_card; 0 < nptrs; h_t_array_valid (ptr_arr_retyps nptrs (PTR('a) p) htd) (PTR('a) p) nptrs\<rbrakk> \<Longrightarrow> ptr_arr_retyps nptrs (PTR('a) p) htd,gd \<Turnstile>\<^sub>t p'
 2. \<lbrakk>p' \<in> (\<lambda>x. PTR('a) (p + word_of_nat x * word_of_nat (size_of TYPE('a)))) ` {k. k < nptrs}; \<not> arr; gd p'; nptrs * size_of TYPE('a) < addr_card\<rbrakk> \<Longrightarrow> ptr_retyps nptrs (PTR('a) p) htd,gd \<Turnstile>\<^sub>t p' proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>arr; gd (PTR('a) (p + word_of_nat x * word_of_nat (size_of TYPE('a)))); nptrs * size_of TYPE('a) < addr_card; h_t_array_valid (ptr_arr_retyps nptrs (PTR('a) p) htd) (PTR('a) p) nptrs; p' = PTR('a) (p + word_of_nat x * word_of_nat (size_of TYPE('a))); x < nptrs\<rbrakk> \<Longrightarrow> ptr_arr_retyps nptrs (PTR('a) p) htd,gd \<Turnstile>\<^sub>t PTR('a) (p + word_of_nat x * word_of_nat (size_of TYPE('a)))
 2. \<lbrakk>p' \<in> (\<lambda>x. PTR('a) (p + word_of_nat x * word_of_nat (size_of TYPE('a)))) ` {k. k < nptrs}; \<not> arr; gd p'; nptrs * size_of TYPE('a) < addr_card\<rbrakk> \<Longrightarrow> ptr_retyps nptrs (PTR('a) p) htd,gd \<Turnstile>\<^sub>t p' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p' \<in> (\<lambda>x. PTR('a) (p + word_of_nat x * word_of_nat (size_of TYPE('a)))) ` {k. k < nptrs}; \<not> arr; gd p'; nptrs * size_of TYPE('a) < addr_card\<rbrakk> \<Longrightarrow> ptr_retyps nptrs (PTR('a) p) htd,gd \<Turnstile>\<^sub>t p' proof (prove)
goal (2 subgoals):
 1. \<And>p htd. \<lbrakk>p' \<in> (\<lambda>x. PTR('a) (p + word_of_nat x * word_of_nat (size_of TYPE('a)))) ` {k. k < 0}; \<not> arr; gd p'; 0 * size_of TYPE('a) < addr_card\<rbrakk> \<Longrightarrow> ptr_retyps 0 (PTR('a) p) htd,gd \<Turnstile>\<^sub>t p'
 2. \<And>nptrs p htd. \<lbrakk>\<And>p htd. \<lbrakk>p' \<in> (\<lambda>x. PTR('a) (p + word_of_nat x * word_of_nat (size_of TYPE('a)))) ` {k. k < nptrs}; \<not> arr; gd p'; nptrs * size_of TYPE('a) < addr_card\<rbrakk> \<Longrightarrow> ptr_retyps nptrs (PTR('a) p) htd,gd \<Turnstile>\<^sub>t p'; p' \<in> (\<lambda>x. PTR('a) (p + word_of_nat x * word_of_nat (size_of TYPE('a)))) ` {k. k < Suc nptrs}; \<not> arr; gd p'; Suc nptrs * size_of TYPE('a) < addr_card\<rbrakk> \<Longrightarrow> ptr_retyps (Suc nptrs) (PTR('a) p) htd,gd \<Turnstile>\<^sub>t p' proof (prove)
goal (1 subgoal):
 1. \<And>nptrs p htd. \<lbrakk>\<And>p htd. \<lbrakk>p' \<in> (\<lambda>x. PTR('a) (p + word_of_nat x * word_of_nat (size_of TYPE('a)))) ` {k. k < nptrs}; \<not> arr; gd p'; nptrs * size_of TYPE('a) < addr_card\<rbrakk> \<Longrightarrow> ptr_retyps nptrs (PTR('a) p) htd,gd \<Turnstile>\<^sub>t p'; p' \<in> (\<lambda>x. PTR('a) (p + word_of_nat x * word_of_nat (size_of TYPE('a)))) ` {k. k < Suc nptrs}; \<not> arr; gd p'; Suc nptrs * size_of TYPE('a) < addr_card\<rbrakk> \<Longrightarrow> ptr_retyps (Suc nptrs) (PTR('a) p) htd,gd \<Turnstile>\<^sub>t p' proof (prove)
goal (1 subgoal):
 1. \<And>nptrs p htd x. \<lbrakk>\<And>pa htd. PTR('a) (p + word_of_nat x * word_of_nat (size_of TYPE('a))) \<in> (\<lambda>x. PTR('a) (pa + word_of_nat x * word_of_nat (size_of TYPE('a)))) ` {k. k < nptrs} \<Longrightarrow> ptr_retyps nptrs (PTR('a) pa) htd,gd \<Turnstile>\<^sub>t PTR('a) (p + word_of_nat x * word_of_nat (size_of TYPE('a))); \<not> arr; gd (PTR('a) (p + word_of_nat x * word_of_nat (size_of TYPE('a)))); size_of TYPE('a) + nptrs * size_of TYPE('a) < addr_card; p' = PTR('a) (p + word_of_nat x * word_of_nat (size_of TYPE('a))); x < Suc nptrs\<rbrakk> \<Longrightarrow> ptr_retyp (PTR('a) p) (ptr_retyps nptrs (PTR('a) (p + word_of_nat (size_of TYPE('a)))) htd),gd \<Turnstile>\<^sub>t PTR('a) (p + word_of_nat x * word_of_nat (size_of TYPE('a))) proof (prove)
goal (1 subgoal):
 1. \<And>nptrs p htd x nat. \<lbrakk>\<And>pa htd. PTR('a) (p + (1 + word_of_nat nat) * word_of_nat (size_of TYPE('a))) \<in> (\<lambda>x. PTR('a) (pa + word_of_nat x * word_of_nat (size_of TYPE('a)))) ` {k. k < nptrs} \<Longrightarrow> ptr_retyps nptrs (PTR('a) pa) htd,gd \<Turnstile>\<^sub>t PTR('a) (p + (1 + word_of_nat nat) * word_of_nat (size_of TYPE('a))); \<not> arr; gd (PTR('a) (p + (1 + word_of_nat nat) * word_of_nat (size_of TYPE('a)))); size_of TYPE('a) + nptrs * size_of TYPE('a) < addr_card; p' = PTR('a) (p + (1 + word_of_nat nat) * word_of_nat (size_of TYPE('a))); nat < nptrs; x = Suc nat\<rbrakk> \<Longrightarrow> ptr_retyp (PTR('a) p) (ptr_retyps nptrs (PTR('a) (p + word_of_nat (size_of TYPE('a)))) htd),gd \<Turnstile>\<^sub>t PTR('a) (p + (1 + word_of_nat nat) * word_of_nat (size_of TYPE('a))) proof (prove)
goal (2 subgoals):
 1. \<And>nptrs p htd x nat. \<lbrakk>\<And>pa htd. PTR('a) (p + (1 + word_of_nat nat) * word_of_nat (size_of TYPE('a))) \<in> (\<lambda>x. PTR('a) (pa + word_of_nat x * word_of_nat (size_of TYPE('a)))) ` {k. k < nptrs} \<Longrightarrow> ptr_retyps nptrs (PTR('a) pa) htd,gd \<Turnstile>\<^sub>t PTR('a) (p + (1 + word_of_nat nat) * word_of_nat (size_of TYPE('a))); \<not> arr; gd (PTR('a) (p + (1 + word_of_nat nat) * word_of_nat (size_of TYPE('a)))); size_of TYPE('a) + nptrs * size_of TYPE('a) < addr_card; p' = PTR('a) (p + (1 + word_of_nat nat) * word_of_nat (size_of TYPE('a))); nat < nptrs; x = Suc nat\<rbrakk> \<Longrightarrow> ptr_retyps nptrs (PTR('a) (p + word_of_nat (size_of TYPE('a)))) htd,gd \<Turnstile>\<^sub>t PTR('a) (p + (1 + word_of_nat nat) * word_of_nat (size_of TYPE('a)))
 2. \<And>nptrs p htd x nat. \<lbrakk>\<And>pa htd. PTR('a) (p + (1 + word_of_nat nat) * word_of_nat (size_of TYPE('a))) \<in> (\<lambda>x. PTR('a) (pa + word_of_nat x * word_of_nat (size_of TYPE('a)))) ` {k. k < nptrs} \<Longrightarrow> ptr_retyps nptrs (PTR('a) pa) htd,gd \<Turnstile>\<^sub>t PTR('a) (p + (1 + word_of_nat nat) * word_of_nat (size_of TYPE('a))); \<not> arr; gd (PTR('a) (p + (1 + word_of_nat nat) * word_of_nat (size_of TYPE('a)))); size_of TYPE('a) + nptrs * size_of TYPE('a) < addr_card; p' = PTR('a) (p + (1 + word_of_nat nat) * word_of_nat (size_of TYPE('a))); nat < nptrs; x = Suc nat\<rbrakk> \<Longrightarrow> ptr_span (PTR('a) p) \<inter> ptr_span (PTR('a) (p + (1 + word_of_nat nat) * word_of_nat (size_of TYPE('a)))) = {} proof (prove)
goal (2 subgoals):
 1. \<And>nptrs p htd x nat. \<lbrakk>\<not> arr; gd (PTR('a) (p + (1 + word_of_nat nat) * word_of_nat (size_of TYPE('a)))); size_of TYPE('a) + nptrs * size_of TYPE('a) < addr_card; p' = PTR('a) (p + (1 + word_of_nat nat) * word_of_nat (size_of TYPE('a))); nat < nptrs; x = Suc nat\<rbrakk> \<Longrightarrow> PTR('a) (p + (1 + word_of_nat nat) * word_of_nat (size_of TYPE('a))) = PTR('a) (p + word_of_nat (size_of TYPE('a)) + word_of_nat nat * word_of_nat (size_of TYPE('a)))
 2. \<And>nptrs p htd x nat. \<lbrakk>\<And>pa htd. PTR('a) (p + (1 + word_of_nat nat) * word_of_nat (size_of TYPE('a))) \<in> (\<lambda>x. PTR('a) (pa + word_of_nat x * word_of_nat (size_of TYPE('a)))) ` {k. k < nptrs} \<Longrightarrow> ptr_retyps nptrs (PTR('a) pa) htd,gd \<Turnstile>\<^sub>t PTR('a) (p + (1 + word_of_nat nat) * word_of_nat (size_of TYPE('a))); \<not> arr; gd (PTR('a) (p + (1 + word_of_nat nat) * word_of_nat (size_of TYPE('a)))); size_of TYPE('a) + nptrs * size_of TYPE('a) < addr_card; p' = PTR('a) (p + (1 + word_of_nat nat) * word_of_nat (size_of TYPE('a))); nat < nptrs; x = Suc nat\<rbrakk> \<Longrightarrow> ptr_span (PTR('a) p) \<inter> ptr_span (PTR('a) (p + (1 + word_of_nat nat) * word_of_nat (size_of TYPE('a)))) = {} proof (prove)
goal (1 subgoal):
 1. \<And>nptrs p htd x nat. \<lbrakk>\<And>pa htd. PTR('a) (p + (1 + word_of_nat nat) * word_of_nat (size_of TYPE('a))) \<in> (\<lambda>x. PTR('a) (pa + word_of_nat x * word_of_nat (size_of TYPE('a)))) ` {k. k < nptrs} \<Longrightarrow> ptr_retyps nptrs (PTR('a) pa) htd,gd \<Turnstile>\<^sub>t PTR('a) (p + (1 + word_of_nat nat) * word_of_nat (size_of TYPE('a))); \<not> arr; gd (PTR('a) (p + (1 + word_of_nat nat) * word_of_nat (size_of TYPE('a)))); size_of TYPE('a) + nptrs * size_of TYPE('a) < addr_card; p' = PTR('a) (p + (1 + word_of_nat nat) * word_of_nat (size_of TYPE('a))); nat < nptrs; x = Suc nat\<rbrakk> \<Longrightarrow> ptr_span (PTR('a) p) \<inter> ptr_span (PTR('a) (p + (1 + word_of_nat nat) * word_of_nat (size_of TYPE('a)))) = {} proof (prove)
goal (1 subgoal):
 1. \<And>nptrs p x nat. \<lbrakk>\<And>pa htd. PTR('a) (p + (1 + word_of_nat nat) * word_of_nat (size_of TYPE('a))) \<in> (\<lambda>x. PTR('a) (pa + word_of_nat x * word_of_nat (size_of TYPE('a)))) ` {k. k < nptrs} \<Longrightarrow> ptr_retyps nptrs (PTR('a) pa) htd,gd \<Turnstile>\<^sub>t PTR('a) (p + (1 + word_of_nat nat) * word_of_nat (size_of TYPE('a))); \<not> arr; gd (PTR('a) (p + (1 + word_of_nat nat) * word_of_nat (size_of TYPE('a)))); size_of TYPE('a) + nptrs * size_of TYPE('a) < addr_card; p' = PTR('a) (p + (1 + word_of_nat nat) * word_of_nat (size_of TYPE('a))); nat < nptrs; x = Suc nat\<rbrakk> \<Longrightarrow> {p..+size_of TYPE('a)} \<inter> {p + (1 + word_of_nat nat) * word_of_nat (size_of TYPE('a))..+size_of TYPE('a)} = {} proof (prove)
goal (2 subgoals):
 1. \<And>nptrs p x nat. \<lbrakk>\<And>pa htd. PTR('a) (p + (1 + word_of_nat nat) * word_of_nat (size_of TYPE('a))) \<in> (\<lambda>x. PTR('a) (pa + word_of_nat x * word_of_nat (size_of TYPE('a)))) ` {k. k < nptrs} \<Longrightarrow> ptr_retyps nptrs (PTR('a) pa) htd,gd \<Turnstile>\<^sub>t PTR('a) (p + (1 + word_of_nat nat) * word_of_nat (size_of TYPE('a))); \<not> arr; gd (PTR('a) (p + (1 + word_of_nat nat) * word_of_nat (size_of TYPE('a)))); size_of TYPE('a) + nptrs * size_of TYPE('a) < addr_card; p' = PTR('a) (p + (1 + word_of_nat nat) * word_of_nat (size_of TYPE('a))); nat < nptrs; x = Suc nat\<rbrakk> \<Longrightarrow> Suc nat * size_of TYPE('a) + size_of TYPE('a) < addr_card
 2. \<And>nptrs p x nat. \<lbrakk>\<And>pa htd. PTR('a) (p + (1 + word_of_nat nat) * word_of_nat (size_of TYPE('a))) \<in> (\<lambda>x. PTR('a) (pa + word_of_nat x * word_of_nat (size_of TYPE('a)))) ` {k. k < nptrs} \<Longrightarrow> ptr_retyps nptrs (PTR('a) pa) htd,gd \<Turnstile>\<^sub>t PTR('a) (p + (1 + word_of_nat nat) * word_of_nat (size_of TYPE('a))); \<not> arr; gd (PTR('a) (p + (1 + word_of_nat nat) * word_of_nat (size_of TYPE('a)))); size_of TYPE('a) + nptrs * size_of TYPE('a) < addr_card; p' = PTR('a) (p + (1 + word_of_nat nat) * word_of_nat (size_of TYPE('a))); nat < nptrs; x = Suc nat; {p + word_of_nat (Suc nat * size_of TYPE('a))..+size_of TYPE('a)} \<inter> {p..+Suc nat * size_of TYPE('a)} = {}\<rbrakk> \<Longrightarrow> {p..+size_of TYPE('a)} \<inter> {p + (1 + word_of_nat nat) * word_of_nat (size_of TYPE('a))..+size_of TYPE('a)} = {} proof (prove)
goal (2 subgoals):
 1. \<And>nptrs p x nat. \<lbrakk>\<And>pa htd. PTR('a) (p + (1 + word_of_nat nat) * word_of_nat (size_of TYPE('a))) \<in> (\<lambda>x. PTR('a) (pa + word_of_nat x * word_of_nat (size_of TYPE('a)))) ` {k. k < nptrs} \<Longrightarrow> ptr_retyps nptrs (PTR('a) pa) htd,gd \<Turnstile>\<^sub>t PTR('a) (p + (1 + word_of_nat nat) * word_of_nat (size_of TYPE('a))); \<not> arr; gd (PTR('a) (p + (1 + word_of_nat nat) * word_of_nat (size_of TYPE('a)))); p' = PTR('a) (p + (1 + word_of_nat nat) * word_of_nat (size_of TYPE('a))); nat < nptrs; x = Suc nat\<rbrakk> \<Longrightarrow> Suc nat * size_of TYPE('a) + size_of TYPE('a) \<le> size_of TYPE('a) + nptrs * size_of TYPE('a)
 2. \<And>nptrs p x nat. \<lbrakk>\<And>pa htd. PTR('a) (p + (1 + word_of_nat nat) * word_of_nat (size_of TYPE('a))) \<in> (\<lambda>x. PTR('a) (pa + word_of_nat x * word_of_nat (size_of TYPE('a)))) ` {k. k < nptrs} \<Longrightarrow> ptr_retyps nptrs (PTR('a) pa) htd,gd \<Turnstile>\<^sub>t PTR('a) (p + (1 + word_of_nat nat) * word_of_nat (size_of TYPE('a))); \<not> arr; gd (PTR('a) (p + (1 + word_of_nat nat) * word_of_nat (size_of TYPE('a)))); size_of TYPE('a) + nptrs * size_of TYPE('a) < addr_card; p' = PTR('a) (p + (1 + word_of_nat nat) * word_of_nat (size_of TYPE('a))); nat < nptrs; x = Suc nat; {p + word_of_nat (Suc nat * size_of TYPE('a))..+size_of TYPE('a)} \<inter> {p..+Suc nat * size_of TYPE('a)} = {}\<rbrakk> \<Longrightarrow> {p..+size_of TYPE('a)} \<inter> {p + (1 + word_of_nat nat) * word_of_nat (size_of TYPE('a))..+size_of TYPE('a)} = {} proof (prove)
goal (1 subgoal):
 1. \<And>nptrs p x nat. \<lbrakk>\<And>pa htd. PTR('a) (p + (1 + word_of_nat nat) * word_of_nat (size_of TYPE('a))) \<in> (\<lambda>x. PTR('a) (pa + word_of_nat x * word_of_nat (size_of TYPE('a)))) ` {k. k < nptrs} \<Longrightarrow> ptr_retyps nptrs (PTR('a) pa) htd,gd \<Turnstile>\<^sub>t PTR('a) (p + (1 + word_of_nat nat) * word_of_nat (size_of TYPE('a))); \<not> arr; gd (PTR('a) (p + (1 + word_of_nat nat) * word_of_nat (size_of TYPE('a)))); size_of TYPE('a) + nptrs * size_of TYPE('a) < addr_card; p' = PTR('a) (p + (1 + word_of_nat nat) * word_of_nat (size_of TYPE('a))); nat < nptrs; x = Suc nat; {p + word_of_nat (Suc nat * size_of TYPE('a))..+size_of TYPE('a)} \<inter> {p..+Suc nat * size_of TYPE('a)} = {}\<rbrakk> \<Longrightarrow> {p..+size_of TYPE('a)} \<inter> {p + (1 + word_of_nat nat) * word_of_nat (size_of TYPE('a))..+size_of TYPE('a)} = {} proof (prove)
goal (1 subgoal):
 1. \<And>nptrs p x nat. \<lbrakk>\<And>pa htd. PTR('a) (p + (word_of_nat (size_of TYPE('a)) + word_of_nat nat * word_of_nat (size_of TYPE('a)))) \<in> (\<lambda>x. PTR('a) (pa + word_of_nat x * word_of_nat (size_of TYPE('a)))) ` {k. k < nptrs} \<Longrightarrow> ptr_retyps nptrs (PTR('a) pa) htd,gd \<Turnstile>\<^sub>t PTR('a) (p + (word_of_nat (size_of TYPE('a)) + word_of_nat nat * word_of_nat (size_of TYPE('a)))); \<not> arr; gd (PTR('a) (p + (word_of_nat (size_of TYPE('a)) + word_of_nat nat * word_of_nat (size_of TYPE('a))))); size_of TYPE('a) + nptrs * size_of TYPE('a) < addr_card; p' = PTR('a) (p + (word_of_nat (size_of TYPE('a)) + word_of_nat nat * word_of_nat (size_of TYPE('a)))); nat < nptrs; x = Suc nat; {p..+size_of TYPE('a) + nat * size_of TYPE('a)} \<inter> {p + (word_of_nat (size_of TYPE('a)) + word_of_nat nat * word_of_nat (size_of TYPE('a)))..+size_of TYPE('a)} = {}\<rbrakk> \<Longrightarrow> {p..+size_of TYPE('a)} \<inter> {p + (word_of_nat (size_of TYPE('a)) + word_of_nat nat * word_of_nat (size_of TYPE('a)))..+size_of TYPE('a)} = {} proof (prove)
goal (1 subgoal):
 1. \<And>nptrs p x nat. \<lbrakk>\<And>pa htd. PTR('a) (p + (word_of_nat (size_of TYPE('a)) + word_of_nat nat * word_of_nat (size_of TYPE('a)))) \<in> (\<lambda>x. PTR('a) (pa + word_of_nat x * word_of_nat (size_of TYPE('a)))) ` {k. k < nptrs} \<Longrightarrow> ptr_retyps nptrs (PTR('a) pa) htd,gd \<Turnstile>\<^sub>t PTR('a) (p + (word_of_nat (size_of TYPE('a)) + word_of_nat nat * word_of_nat (size_of TYPE('a)))); \<not> arr; gd (PTR('a) (p + (word_of_nat (size_of TYPE('a)) + word_of_nat nat * word_of_nat (size_of TYPE('a))))); size_of TYPE('a) + nptrs * size_of TYPE('a) < addr_card; p' = PTR('a) (p + (word_of_nat (size_of TYPE('a)) + word_of_nat nat * word_of_nat (size_of TYPE('a)))); nat < nptrs; x = Suc nat\<rbrakk> \<Longrightarrow> {p..+size_of TYPE('a)} \<subseteq> {p..+size_of TYPE('a) + nat * size_of TYPE('a)} proof (prove)
goal:
No subgoals!