theory Move_C

lemma ucast_increment:
  assumes "w \<noteq> max_word"
  shows "UCAST('a::len \<rightarrow> 'b::len) w + 1 = UCAST('a \<rightarrow> 'b) (w + 1)" apply (cases "LENGTH('b) \<le> LENGTH('a)") apply (simp add: ucast_down_add is_down) apply (subgoal_tac "uint w + 1 < 2 ^ LENGTH('a)") apply (subgoal_tac "uint w + 1 < 2 ^ LENGTH('b)") apply (subst word_uint_eq_iff) apply (simp add: uint_arith_simps uint_up_ucast is_up) apply (erule less_trans, rule power_strict_increasing, simp, simp) apply (subst less_diff_eq[symmetric]) using assms apply (simp add: not_max_word_iff_less word_less_alt) apply (erule less_le_trans) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. UCAST('a \<rightarrow> 'b) w + 1 = UCAST('a \<rightarrow> 'b) (w + 1) proof (prove)
goal (2 subgoals):
 1. LENGTH('b) \<le> LENGTH('a) \<Longrightarrow> UCAST('a \<rightarrow> 'b) w + 1 = UCAST('a \<rightarrow> 'b) (w + 1)
 2. \<not> LENGTH('b) \<le> LENGTH('a) \<Longrightarrow> UCAST('a \<rightarrow> 'b) w + 1 = UCAST('a \<rightarrow> 'b) (w + 1) proof (prove)
goal (1 subgoal):
 1. \<not> LENGTH('b) \<le> LENGTH('a) \<Longrightarrow> UCAST('a \<rightarrow> 'b) w + 1 = UCAST('a \<rightarrow> 'b) (w + 1) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<not> LENGTH('b) \<le> LENGTH('a); uint w + 1 < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> UCAST('a \<rightarrow> 'b) w + 1 = UCAST('a \<rightarrow> 'b) (w + 1)
 2. \<not> LENGTH('b) \<le> LENGTH('a) \<Longrightarrow> uint w + 1 < 2 ^ LENGTH('a) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<not> LENGTH('b) \<le> LENGTH('a); uint w + 1 < 2 ^ LENGTH('a); uint w + 1 < 2 ^ LENGTH('b)\<rbrakk> \<Longrightarrow> UCAST('a \<rightarrow> 'b) w + 1 = UCAST('a \<rightarrow> 'b) (w + 1)
 2. \<lbrakk>\<not> LENGTH('b) \<le> LENGTH('a); uint w + 1 < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> uint w + 1 < 2 ^ LENGTH('b)
 3. \<not> LENGTH('b) \<le> LENGTH('a) \<Longrightarrow> uint w + 1 < 2 ^ LENGTH('a) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<not> LENGTH('b) \<le> LENGTH('a); uint w + 1 < 2 ^ LENGTH('a); uint w + 1 < 2 ^ LENGTH('b)\<rbrakk> \<Longrightarrow> uint (UCAST('a \<rightarrow> 'b) w + 1) = uint (UCAST('a \<rightarrow> 'b) (w + 1))
 2. \<lbrakk>\<not> LENGTH('b) \<le> LENGTH('a); uint w + 1 < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> uint w + 1 < 2 ^ LENGTH('b)
 3. \<not> LENGTH('b) \<le> LENGTH('a) \<Longrightarrow> uint w + 1 < 2 ^ LENGTH('a) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<not> LENGTH('b) \<le> LENGTH('a); uint w + 1 < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> uint w + 1 < 2 ^ LENGTH('b)
 2. \<not> LENGTH('b) \<le> LENGTH('a) \<Longrightarrow> uint w + 1 < 2 ^ LENGTH('a) proof (prove)
goal (1 subgoal):
 1. \<not> LENGTH('b) \<le> LENGTH('a) \<Longrightarrow> uint w + 1 < 2 ^ LENGTH('a) proof (prove)
goal (1 subgoal):
 1. \<not> LENGTH('b) \<le> LENGTH('a) \<Longrightarrow> uint w < 2 ^ LENGTH('a) - 1 proof (prove)
using this:
w \<noteq> - 1

goal (1 subgoal):
 1. \<not> LENGTH('b) \<le> LENGTH('a) \<Longrightarrow> uint w < 2 ^ LENGTH('a) - 1 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> LENGTH('b) \<le> LENGTH('a); uint w < uint (- 1)\<rbrakk> \<Longrightarrow> uint w < 2 ^ LENGTH('a) - 1 proof (prove)
goal (1 subgoal):
 1. \<not> LENGTH('b) \<le> LENGTH('a) \<Longrightarrow> uint (- 1) \<le> 2 ^ LENGTH('a) - 1 proof (prove)
goal:
No subgoals!