theory Retype_C

lemma intvl_sum:
  "{p..+ i + j}
    = {p ..+ i} \<union> {(p :: ('a :: len) word) + of_nat i ..+ j}" apply (simp add: intvl_def, safe) apply clarsimp apply (case_tac "k < i") apply auto[1] apply (drule_tac x="k - i" in spec) apply simp apply fastforce apply (rule_tac x="k + i" in exI) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. {p..+i + j} = {p..+i} \<union> {p + word_of_nat i..+j} proof (prove)
goal (3 subgoals):
 1. \<And>x k. \<lbrakk>\<nexists>ka. p + word_of_nat k = p + word_of_nat i + word_of_nat ka \<and> ka < j; k < i + j\<rbrakk> \<Longrightarrow> \<exists>ka. p + word_of_nat k = p + word_of_nat ka \<and> ka < i
 2. \<And>x k. k < i \<Longrightarrow> \<exists>ka. p + word_of_nat k = p + word_of_nat ka \<and> ka < i + j
 3. \<And>x k. k < j \<Longrightarrow> \<exists>ka. p + word_of_nat i + word_of_nat k = p + word_of_nat ka \<and> ka < i + j proof (prove)
goal (3 subgoals):
 1. \<And>k. \<lbrakk>\<forall>ka. word_of_nat k = word_of_nat i + word_of_nat ka \<longrightarrow> \<not> ka < j; k < i + j\<rbrakk> \<Longrightarrow> \<exists>ka. word_of_nat k = word_of_nat ka \<and> ka < i
 2. \<And>x k. k < i \<Longrightarrow> \<exists>ka. p + word_of_nat k = p + word_of_nat ka \<and> ka < i + j
 3. \<And>x k. k < j \<Longrightarrow> \<exists>ka. p + word_of_nat i + word_of_nat k = p + word_of_nat ka \<and> ka < i + j proof (prove)
goal (4 subgoals):
 1. \<And>k. \<lbrakk>\<forall>ka. word_of_nat k = word_of_nat i + word_of_nat ka \<longrightarrow> \<not> ka < j; k < i + j; k < i\<rbrakk> \<Longrightarrow> \<exists>ka. word_of_nat k = word_of_nat ka \<and> ka < i
 2. \<And>k. \<lbrakk>\<forall>ka. word_of_nat k = word_of_nat i + word_of_nat ka \<longrightarrow> \<not> ka < j; k < i + j; \<not> k < i\<rbrakk> \<Longrightarrow> \<exists>ka. word_of_nat k = word_of_nat ka \<and> ka < i
 3. \<And>x k. k < i \<Longrightarrow> \<exists>ka. p + word_of_nat k = p + word_of_nat ka \<and> ka < i + j
 4. \<And>x k. k < j \<Longrightarrow> \<exists>ka. p + word_of_nat i + word_of_nat k = p + word_of_nat ka \<and> ka < i + j proof (prove)
goal (3 subgoals):
 1. \<And>k. \<lbrakk>\<forall>ka. word_of_nat k = word_of_nat i + word_of_nat ka \<longrightarrow> \<not> ka < j; k < i + j; \<not> k < i\<rbrakk> \<Longrightarrow> \<exists>ka. word_of_nat k = word_of_nat ka \<and> ka < i
 2. \<And>x k. k < i \<Longrightarrow> \<exists>ka. p + word_of_nat k = p + word_of_nat ka \<and> ka < i + j
 3. \<And>x k. k < j \<Longrightarrow> \<exists>ka. p + word_of_nat i + word_of_nat k = p + word_of_nat ka \<and> ka < i + j proof (prove)
goal (3 subgoals):
 1. \<And>k. \<lbrakk>k < i + j; \<not> k < i; word_of_nat k = word_of_nat i + word_of_nat (k - i) \<longrightarrow> \<not> k - i < j\<rbrakk> \<Longrightarrow> \<exists>ka. word_of_nat k = word_of_nat ka \<and> ka < i
 2. \<And>x k. k < i \<Longrightarrow> \<exists>ka. p + word_of_nat k = p + word_of_nat ka \<and> ka < i + j
 3. \<And>x k. k < j \<Longrightarrow> \<exists>ka. p + word_of_nat i + word_of_nat k = p + word_of_nat ka \<and> ka < i + j proof (prove)
goal (2 subgoals):
 1. \<And>x k. k < i \<Longrightarrow> \<exists>ka. p + word_of_nat k = p + word_of_nat ka \<and> ka < i + j
 2. \<And>x k. k < j \<Longrightarrow> \<exists>ka. p + word_of_nat i + word_of_nat k = p + word_of_nat ka \<and> ka < i + j proof (prove)
goal (1 subgoal):
 1. \<And>x k. k < j \<Longrightarrow> \<exists>ka. p + word_of_nat i + word_of_nat k = p + word_of_nat ka \<and> ka < i + j proof (prove)
goal (1 subgoal):
 1. \<And>x k. k < j \<Longrightarrow> p + word_of_nat i + word_of_nat k = p + word_of_nat (k + i) \<and> k + i < i + j proof (prove)
goal:
No subgoals!