theory Detype_R

lemma word_range_card:
  "base \<le>base + h \<Longrightarrow> card {base..base + (h::word32)} = (unat h) + 1" proof (induct h rule: word_induct2) case zero show ?case by simp next case (suc h) have interval_plus_one_word32:
    "\<And>base ceil. \<lbrakk>base \<le> ceil + 1;ceil \<le> ceil + 1\<rbrakk> \<Longrightarrow>
                 {base..ceil + 1} = {base .. ceil } \<union> {ceil + (1::word32)}" by (auto intro:order_antisym simp:not_le inc_le) show ?case using suc plus_one_helper2[where n = h and x = h,simplified] apply (subst add.commute[where a = 1]) apply (subst add.assoc[symmetric]) apply (subst interval_plus_one_word32) apply (simp add: field_simps) apply (subst add.assoc) apply (rule word_plus_mono_right) apply (simp add: field_simps) apply (simp add: field_simps) apply (subst card_Un_disjoint; simp) apply (clarsimp simp: field_simps) apply (subst suc) apply (erule word_plus_mono_right2) apply (simp add: field_simps) apply simp apply (simp add: unatSuc) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. base \<le> base + h \<Longrightarrow> card {base..base + h} = unat h + 1 proof (state)
goal (2 subgoals):
 1. base \<le> base + 0 \<Longrightarrow> card {base..base + 0} = unat 0 + 1
 2. \<And>n. \<lbrakk>1 + n \<noteq> 0; base \<le> base + n \<Longrightarrow> card {base..base + n} = unat n + 1; base \<le> base + (1 + n)\<rbrakk> \<Longrightarrow> card {base..base + (1 + n)} = unat (1 + n) + 1 proof (state)
this:
base \<le> base + 0

goal (2 subgoals):
 1. base \<le> base + 0 \<Longrightarrow> card {base..base + 0} = unat 0 + 1
 2. \<And>n. \<lbrakk>1 + n \<noteq> 0; base \<le> base + n \<Longrightarrow> card {base..base + n} = unat n + 1; base \<le> base + (1 + n)\<rbrakk> \<Longrightarrow> card {base..base + (1 + n)} = unat (1 + n) + 1 proof (prove)
goal (1 subgoal):
 1. card {base..base + 0} = unat 0 + 1 proof (state)
this:
card {base..base + 0} = unat 0 + 1

goal (1 subgoal):
 1. \<And>n. \<lbrakk>1 + n \<noteq> 0; base \<le> base + n \<Longrightarrow> card {base..base + n} = unat n + 1; base \<le> base + (1 + n)\<rbrakk> \<Longrightarrow> card {base..base + (1 + n)} = unat (1 + n) + 1 proof (state)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>1 + n \<noteq> 0; base \<le> base + n \<Longrightarrow> card {base..base + n} = unat n + 1; base \<le> base + (1 + n)\<rbrakk> \<Longrightarrow> card {base..base + (1 + n)} = unat (1 + n) + 1 proof (state)
this:
1 + h \<noteq> 0
base \<le> base + h \<Longrightarrow> card {base..base + h} = unat h + 1
base \<le> base + (1 + h)

goal (1 subgoal):
 1. \<And>n. \<lbrakk>1 + n \<noteq> 0; base \<le> base + n \<Longrightarrow> card {base..base + n} = unat n + 1; base \<le> base + (1 + n)\<rbrakk> \<Longrightarrow> card {base..base + (1 + n)} = unat (1 + n) + 1 proof (prove)
goal (1 subgoal):
 1. \<And>base ceil. \<lbrakk>base \<le> ceil + 1; ceil \<le> ceil + 1\<rbrakk> \<Longrightarrow> {base..ceil + 1} = {base..ceil} \<union> {ceil + 1} proof (state)
this:
\<lbrakk>?base \<le> ?ceil + 1; ?ceil \<le> ?ceil + 1\<rbrakk> \<Longrightarrow> {?base..?ceil + 1} = {?base..?ceil} \<union> {?ceil + 1}

goal (1 subgoal):
 1. \<And>n. \<lbrakk>1 + n \<noteq> 0; base \<le> base + n \<Longrightarrow> card {base..base + n} = unat n + 1; base \<le> base + (1 + n)\<rbrakk> \<Longrightarrow> card {base..base + (1 + n)} = unat (1 + n) + 1 proof (prove)
goal (1 subgoal):
 1. card {base..base + (1 + h)} = unat (1 + h) + 1 proof (prove)
using this:
1 + h \<noteq> 0
base \<le> base + h \<Longrightarrow> card {base..base + h} = unat h + 1
base \<le> base + (1 + h)
h + 1 \<noteq> 0 \<Longrightarrow> h < h + 1

goal (1 subgoal):
 1. card {base..base + (1 + h)} = unat (1 + h) + 1 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>1 + h \<noteq> 0; base \<le> base + h \<Longrightarrow> card {base..base + h} = unat h + 1; base \<le> base + (1 + h); h + 1 \<noteq> 0 \<Longrightarrow> h < h + 1\<rbrakk> \<Longrightarrow> card {base..base + (h + 1)} = unat (1 + h) + 1 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>1 + h \<noteq> 0; base \<le> base + h \<Longrightarrow> card {base..base + h} = unat h + 1; base \<le> base + (1 + h); h + 1 \<noteq> 0 \<Longrightarrow> h < h + 1\<rbrakk> \<Longrightarrow> card {base..base + h + 1} = unat (1 + h) + 1 proof (prove)
goal (3 subgoals):
 1. \<lbrakk>1 + h \<noteq> 0; base \<le> base + h \<Longrightarrow> card {base..base + h} = unat h + 1; base \<le> base + (1 + h); h + 1 \<noteq> 0 \<Longrightarrow> h < h + 1\<rbrakk> \<Longrightarrow> base \<le> base + h + 1
 2. \<lbrakk>1 + h \<noteq> 0; base \<le> base + h \<Longrightarrow> card {base..base + h} = unat h + 1; base \<le> base + (1 + h); h + 1 \<noteq> 0 \<Longrightarrow> h < h + 1\<rbrakk> \<Longrightarrow> base + h \<le> base + h + 1
 3. \<lbrakk>1 + h \<noteq> 0; base \<le> base + h \<Longrightarrow> card {base..base + h} = unat h + 1; base \<le> base + (1 + h); h + 1 \<noteq> 0 \<Longrightarrow> h < h + 1\<rbrakk> \<Longrightarrow> card ({base..base + h} \<union> {base + h + 1}) = unat (1 + h) + 1 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>1 + h \<noteq> 0; base \<le> base + h \<Longrightarrow> card {base..base + h} = unat h + 1; base \<le> base + (1 + h); h + 1 \<noteq> 0 \<Longrightarrow> h < h + 1\<rbrakk> \<Longrightarrow> base + h \<le> base + h + 1
 2. \<lbrakk>1 + h \<noteq> 0; base \<le> base + h \<Longrightarrow> card {base..base + h} = unat h + 1; base \<le> base + (1 + h); h + 1 \<noteq> 0 \<Longrightarrow> h < h + 1\<rbrakk> \<Longrightarrow> card ({base..base + h} \<union> {base + h + 1}) = unat (1 + h) + 1 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>1 + h \<noteq> 0; base \<le> base + h \<Longrightarrow> card {base..base + h} = unat h + 1; base \<le> base + (1 + h); h + 1 \<noteq> 0 \<Longrightarrow> h < h + 1\<rbrakk> \<Longrightarrow> base + h \<le> base + (h + 1)
 2. \<lbrakk>1 + h \<noteq> 0; base \<le> base + h \<Longrightarrow> card {base..base + h} = unat h + 1; base \<le> base + (1 + h); h + 1 \<noteq> 0 \<Longrightarrow> h < h + 1\<rbrakk> \<Longrightarrow> card ({base..base + h} \<union> {base + h + 1}) = unat (1 + h) + 1 proof (prove)
goal (3 subgoals):
 1. \<lbrakk>1 + h \<noteq> 0; base \<le> base + h \<Longrightarrow> card {base..base + h} = unat h + 1; base \<le> base + (1 + h); h + 1 \<noteq> 0 \<Longrightarrow> h < h + 1\<rbrakk> \<Longrightarrow> h \<le> h + 1
 2. \<lbrakk>1 + h \<noteq> 0; base \<le> base + h \<Longrightarrow> card {base..base + h} = unat h + 1; base \<le> base + (1 + h); h + 1 \<noteq> 0 \<Longrightarrow> h < h + 1\<rbrakk> \<Longrightarrow> base \<le> base + (h + 1)
 3. \<lbrakk>1 + h \<noteq> 0; base \<le> base + h \<Longrightarrow> card {base..base + h} = unat h + 1; base \<le> base + (1 + h); h + 1 \<noteq> 0 \<Longrightarrow> h < h + 1\<rbrakk> \<Longrightarrow> card ({base..base + h} \<union> {base + h + 1}) = unat (1 + h) + 1 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>1 + h \<noteq> 0; base \<le> base + h \<Longrightarrow> card {base..base + h} = unat h + 1; base \<le> base + (1 + h); h + 1 \<noteq> 0 \<Longrightarrow> h < h + 1\<rbrakk> \<Longrightarrow> base \<le> base + (h + 1)
 2. \<lbrakk>1 + h \<noteq> 0; base \<le> base + h \<Longrightarrow> card {base..base + h} = unat h + 1; base \<le> base + (1 + h); h + 1 \<noteq> 0 \<Longrightarrow> h < h + 1\<rbrakk> \<Longrightarrow> card ({base..base + h} \<union> {base + h + 1}) = unat (1 + h) + 1 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>1 + h \<noteq> 0; base \<le> base + h \<Longrightarrow> card {base..base + h} = unat h + 1; base \<le> base + (1 + h); h + 1 \<noteq> 0 \<Longrightarrow> h < h + 1\<rbrakk> \<Longrightarrow> card ({base..base + h} \<union> {base + h + 1}) = unat (1 + h) + 1 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>1 + h \<noteq> 0; base \<le> base + h \<Longrightarrow> card {base..base + h} = Suc (unat h); base \<le> base + (1 + h); h + 1 \<noteq> 0 \<Longrightarrow> h < h + 1\<rbrakk> \<Longrightarrow> base \<le> base + h + 1 \<longrightarrow> base + h \<noteq> - 1
 2. \<lbrakk>1 + h \<noteq> 0; base \<le> base + h \<Longrightarrow> card {base..base + h} = Suc (unat h); base \<le> base + (1 + h); h + 1 \<noteq> 0 \<Longrightarrow> h < h + 1\<rbrakk> \<Longrightarrow> card {base..base + h} = unat (1 + h) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>1 + h \<noteq> 0; base \<le> base + h \<Longrightarrow> card {base..base + h} = Suc (unat h); base \<le> base + (1 + h); h + 1 \<noteq> 0 \<Longrightarrow> h < h + 1\<rbrakk> \<Longrightarrow> card {base..base + h} = unat (1 + h) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>1 + h \<noteq> 0; base \<le> base + h \<Longrightarrow> card {base..base + h} = Suc (unat h); base \<le> base + (1 + h); h + 1 \<noteq> 0 \<Longrightarrow> h < h + 1\<rbrakk> \<Longrightarrow> base \<le> base + h
 2. \<lbrakk>1 + h \<noteq> 0; base \<le> base + h \<Longrightarrow> card {base..base + h} = Suc (unat h); base \<le> base + (1 + h); h + 1 \<noteq> 0 \<Longrightarrow> h < h + 1\<rbrakk> \<Longrightarrow> unat h + 1 = unat (1 + h) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>1 + h \<noteq> 0; base \<le> base + h \<Longrightarrow> card {base..base + h} = Suc (unat h); h + 1 \<noteq> 0 \<Longrightarrow> h < h + 1\<rbrakk> \<Longrightarrow> h \<le> 1 + h
 2. \<lbrakk>1 + h \<noteq> 0; base \<le> base + h \<Longrightarrow> card {base..base + h} = Suc (unat h); base \<le> base + (1 + h); h + 1 \<noteq> 0 \<Longrightarrow> h < h + 1\<rbrakk> \<Longrightarrow> unat h + 1 = unat (1 + h) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>1 + h \<noteq> 0; base \<le> base + h \<Longrightarrow> card {base..base + h} = Suc (unat h); base \<le> base + (1 + h); h + 1 \<noteq> 0 \<Longrightarrow> h < h + 1\<rbrakk> \<Longrightarrow> unat h + 1 = unat (1 + h) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>1 + h \<noteq> 0; base \<le> base + h \<Longrightarrow> card {base..base + h} = Suc (unat h); base \<le> base + (1 + h); h + 1 \<noteq> 0 \<Longrightarrow> h < h + 1\<rbrakk> \<Longrightarrow> Suc (unat h) = unat (1 + h) proof (prove)
goal:
No subgoals! proof (state)
this:
card {base..base + (1 + h)} = unat (1 + h) + 1

goal:
No subgoals!