theory Word_Lemmas

lemma le_max_word_ucast_id:
  \<open>UCAST('b \<rightarrow> 'a) (UCAST('a \<rightarrow> 'b) x) = x\<close>
    if \<open>x \<le> UCAST('b::len \<rightarrow> 'a) (- 1)\<close>
    for x :: \<open>'a::len word\<close> proof - from that have a1: \<open>x \<le> word_of_int (uint (word_of_int (2 ^ LENGTH('b) - 1) :: 'b word))\<close> by (simp add: of_int_mask_eq) have f2: "((\<exists>i ia. (0::int) \<le> i \<and> \<not> 0 \<le> i + - 1 * ia \<and> i mod ia \<noteq> i) \<or>
            \<not> (0::int) \<le> - 1 + 2 ^ LENGTH('b) \<or> (0::int) \<le> - 1 + 2 ^ LENGTH('b) + - 1 * 2 ^ LENGTH('b) \<or>
            (- (1::int) + 2 ^ LENGTH('b)) mod 2 ^ LENGTH('b) =
              - 1 + 2 ^ LENGTH('b)) = ((\<exists>i ia. (0::int) \<le> i \<and> \<not> 0 \<le> i + - 1 * ia \<and> i mod ia \<noteq> i) \<or>
            \<not> (1::int) \<le> 2 ^ LENGTH('b) \<or>
            2 ^ LENGTH('b) + - (1::int) * ((- 1 + 2 ^ LENGTH('b)) mod 2 ^ LENGTH('b)) = 1)" by force have f3: "\<forall>i ia. \<not> (0::int) \<le> i \<or> 0 \<le> i + - 1 * ia \<or> i mod ia = i" using mod_pos_pos_trivial by force have "(1::int) \<le> 2 ^ LENGTH('b)" by simp then have "2 ^ LENGTH('b) + - (1::int) * ((- 1 + 2 ^ LENGTH('b)) mod 2 ^ len_of TYPE ('b)) = 1" using f3 f2 by blast then have f4: "- (1::int) + 2 ^ LENGTH('b) = (- 1 + 2 ^ LENGTH('b)) mod 2 ^ LENGTH('b)" by linarith have f5: "x \<le> word_of_int (uint (word_of_int (- 1 + 2 ^ LENGTH('b))::'b word))" using a1 by force have f6: "2 ^ LENGTH('b) + - (1::int) = - 1 + 2 ^ LENGTH('b)" by force have f7: "- (1::int) * 1 = - 1" by auto have "\<forall>x0 x1. (x1::int) - x0 = x1 + - 1 * x0" by force then have "x \<le> 2 ^ LENGTH('b) - 1" using f7 f6 f5 f4 by (metis uint_word_of_int wi_homs(2) word_arith_wis(8) word_of_int_2p) then have \<open>uint x \<le> uint (2 ^ LENGTH('b) - (1 :: 'a word))\<close> by (simp add: word_le_def) then have \<open>uint x \<le> 2 ^ LENGTH('b) - 1\<close> by (simp add: uint_word_ariths)
      (metis \<open>1 \<le> 2 ^ LENGTH('b)\<close> \<open>uint x \<le> uint (2 ^ LENGTH('b) - 1)\<close> linorder_not_less lt2p_lem uint_1 uint_minus_simple_alt uint_power_lower word_le_def zle_diff1_eq) then show ?thesis apply (simp add: unsigned_ucast_eq take_bit_word_eq_self_iff) apply (meson \<open>x \<le> 2 ^ LENGTH('b) - 1\<close> not_le word_less_sub_le) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. UCAST('b \<rightarrow> 'a) (UCAST('a \<rightarrow> 'b) x) = x proof (state)
goal (1 subgoal):
 1. UCAST('b \<rightarrow> 'a) (UCAST('a \<rightarrow> 'b) x) = x proof (chain)
picking this:
x \<le> UCAST('b \<rightarrow> 'a) (- 1) proof (prove)
using this:
x \<le> UCAST('b \<rightarrow> 'a) (- 1)

goal (1 subgoal):
 1. x \<le> word_of_int (uint (word_of_int (2 ^ LENGTH('b) - 1))) proof (state)
this:
x \<le> word_of_int (uint (word_of_int (2 ^ LENGTH('b) - 1)))

goal (1 subgoal):
 1. UCAST('b \<rightarrow> 'a) (UCAST('a \<rightarrow> 'b) x) = x proof (prove)
goal (1 subgoal):
 1. ((\<exists>i ia. 0 \<le> i \<and> \<not> 0 \<le> i + - 1 * ia \<and> i mod ia \<noteq> i) \<or> \<not> 0 \<le> - 1 + 2 ^ LENGTH('b) \<or> 0 \<le> - 1 + 2 ^ LENGTH('b) + - 1 * 2 ^ LENGTH('b) \<or> (- 1 + 2 ^ LENGTH('b)) mod 2 ^ LENGTH('b) = - 1 + 2 ^ LENGTH('b)) = ((\<exists>i ia. 0 \<le> i \<and> \<not> 0 \<le> i + - 1 * ia \<and> i mod ia \<noteq> i) \<or> \<not> 1 \<le> 2 ^ LENGTH('b) \<or> 2 ^ LENGTH('b) + - 1 * ((- 1 + 2 ^ LENGTH('b)) mod 2 ^ LENGTH('b)) = 1) proof (state)
this:
((\<exists>i ia. 0 \<le> i \<and> \<not> 0 \<le> i + - 1 * ia \<and> i mod ia \<noteq> i) \<or> \<not> 0 \<le> - 1 + 2 ^ LENGTH('b) \<or> 0 \<le> - 1 + 2 ^ LENGTH('b) + - 1 * 2 ^ LENGTH('b) \<or> (- 1 + 2 ^ LENGTH('b)) mod 2 ^ LENGTH('b) = - 1 + 2 ^ LENGTH('b)) = ((\<exists>i ia. 0 \<le> i \<and> \<not> 0 \<le> i + - 1 * ia \<and> i mod ia \<noteq> i) \<or> \<not> 1 \<le> 2 ^ LENGTH('b) \<or> 2 ^ LENGTH('b) + - 1 * ((- 1 + 2 ^ LENGTH('b)) mod 2 ^ LENGTH('b)) = 1)

goal (1 subgoal):
 1. UCAST('b \<rightarrow> 'a) (UCAST('a \<rightarrow> 'b) x) = x proof (prove)
goal (1 subgoal):
 1. \<forall>i ia. \<not> 0 \<le> i \<or> 0 \<le> i + - 1 * ia \<or> i mod ia = i proof (prove)
using this:
\<lbrakk>0 \<le> ?k; ?k < ?l\<rbrakk> \<Longrightarrow> ?k mod ?l = ?k

goal (1 subgoal):
 1. \<forall>i ia. \<not> 0 \<le> i \<or> 0 \<le> i + - 1 * ia \<or> i mod ia = i proof (state)
this:
\<forall>i ia. \<not> 0 \<le> i \<or> 0 \<le> i + - 1 * ia \<or> i mod ia = i

goal (1 subgoal):
 1. UCAST('b \<rightarrow> 'a) (UCAST('a \<rightarrow> 'b) x) = x proof (prove)
goal (1 subgoal):
 1. 1 \<le> 2 ^ LENGTH('b) proof (state)
this:
1 \<le> 2 ^ LENGTH('b)

goal (1 subgoal):
 1. UCAST('b \<rightarrow> 'a) (UCAST('a \<rightarrow> 'b) x) = x proof (chain)
picking this:
1 \<le> 2 ^ LENGTH('b) proof (prove)
using this:
1 \<le> 2 ^ LENGTH('b)

goal (1 subgoal):
 1. 2 ^ LENGTH('b) + - 1 * ((- 1 + 2 ^ LENGTH('b)) mod 2 ^ LENGTH('b)) = 1 proof (prove)
using this:
1 \<le> 2 ^ LENGTH('b)
\<forall>i ia. \<not> 0 \<le> i \<or> 0 \<le> i + - 1 * ia \<or> i mod ia = i
((\<exists>i ia. 0 \<le> i \<and> \<not> 0 \<le> i + - 1 * ia \<and> i mod ia \<noteq> i) \<or> \<not> 0 \<le> - 1 + 2 ^ LENGTH('b) \<or> 0 \<le> - 1 + 2 ^ LENGTH('b) + - 1 * 2 ^ LENGTH('b) \<or> (- 1 + 2 ^ LENGTH('b)) mod 2 ^ LENGTH('b) = - 1 + 2 ^ LENGTH('b)) = ((\<exists>i ia. 0 \<le> i \<and> \<not> 0 \<le> i + - 1 * ia \<and> i mod ia \<noteq> i) \<or> \<not> 1 \<le> 2 ^ LENGTH('b) \<or> 2 ^ LENGTH('b) + - 1 * ((- 1 + 2 ^ LENGTH('b)) mod 2 ^ LENGTH('b)) = 1)

goal (1 subgoal):
 1. 2 ^ LENGTH('b) + - 1 * ((- 1 + 2 ^ LENGTH('b)) mod 2 ^ LENGTH('b)) = 1 proof (state)
this:
2 ^ LENGTH('b) + - 1 * ((- 1 + 2 ^ LENGTH('b)) mod 2 ^ LENGTH('b)) = 1

goal (1 subgoal):
 1. UCAST('b \<rightarrow> 'a) (UCAST('a \<rightarrow> 'b) x) = x proof (chain)
picking this:
2 ^ LENGTH('b) + - 1 * ((- 1 + 2 ^ LENGTH('b)) mod 2 ^ LENGTH('b)) = 1 proof (prove)
using this:
2 ^ LENGTH('b) + - 1 * ((- 1 + 2 ^ LENGTH('b)) mod 2 ^ LENGTH('b)) = 1

goal (1 subgoal):
 1. - 1 + 2 ^ LENGTH('b) = (- 1 + 2 ^ LENGTH('b)) mod 2 ^ LENGTH('b) proof (state)
this:
- 1 + 2 ^ LENGTH('b) = (- 1 + 2 ^ LENGTH('b)) mod 2 ^ LENGTH('b)

goal (1 subgoal):
 1. UCAST('b \<rightarrow> 'a) (UCAST('a \<rightarrow> 'b) x) = x proof (prove)
goal (1 subgoal):
 1. x \<le> word_of_int (uint (word_of_int (- 1 + 2 ^ LENGTH('b)))) proof (prove)
using this:
x \<le> word_of_int (uint (word_of_int (2 ^ LENGTH('b) - 1)))

goal (1 subgoal):
 1. x \<le> word_of_int (uint (word_of_int (- 1 + 2 ^ LENGTH('b)))) proof (state)
this:
x \<le> word_of_int (uint (word_of_int (- 1 + 2 ^ LENGTH('b))))

goal (1 subgoal):
 1. UCAST('b \<rightarrow> 'a) (UCAST('a \<rightarrow> 'b) x) = x proof (prove)
goal (1 subgoal):
 1. 2 ^ LENGTH('b) + - 1 = - 1 + 2 ^ LENGTH('b) proof (state)
this:
2 ^ LENGTH('b) + - 1 = - 1 + 2 ^ LENGTH('b)

goal (1 subgoal):
 1. UCAST('b \<rightarrow> 'a) (UCAST('a \<rightarrow> 'b) x) = x proof (prove)
goal (1 subgoal):
 1. - 1 * 1 = - 1 proof (state)
this:
- 1 * 1 = - 1

goal (1 subgoal):
 1. UCAST('b \<rightarrow> 'a) (UCAST('a \<rightarrow> 'b) x) = x proof (prove)
goal (1 subgoal):
 1. \<forall>x0 x1. x1 - x0 = x1 + - 1 * x0 proof (state)
this:
\<forall>x0 x1. x1 - x0 = x1 + - 1 * x0

goal (1 subgoal):
 1. UCAST('b \<rightarrow> 'a) (UCAST('a \<rightarrow> 'b) x) = x proof (chain)
picking this:
\<forall>x0 x1. x1 - x0 = x1 + - 1 * x0 proof (prove)
using this:
\<forall>x0 x1. x1 - x0 = x1 + - 1 * x0

goal (1 subgoal):
 1. x \<le> 2 ^ LENGTH('b) - 1 proof (prove)
using this:
\<forall>x0 x1. x1 - x0 = x1 + - 1 * x0
- 1 * 1 = - 1
2 ^ LENGTH('b) + - 1 = - 1 + 2 ^ LENGTH('b)
x \<le> word_of_int (uint (word_of_int (- 1 + 2 ^ LENGTH('b))))
- 1 + 2 ^ LENGTH('b) = (- 1 + 2 ^ LENGTH('b)) mod 2 ^ LENGTH('b)

goal (1 subgoal):
 1. x \<le> 2 ^ LENGTH('b) - 1 proof (state)
this:
x \<le> 2 ^ LENGTH('b) - 1

goal (1 subgoal):
 1. UCAST('b \<rightarrow> 'a) (UCAST('a \<rightarrow> 'b) x) = x proof (chain)
picking this:
x \<le> 2 ^ LENGTH('b) - 1 proof (prove)
using this:
x \<le> 2 ^ LENGTH('b) - 1

goal (1 subgoal):
 1. uint x \<le> uint (2 ^ LENGTH('b) - 1) proof (state)
this:
uint x \<le> uint (2 ^ LENGTH('b) - 1)

goal (1 subgoal):
 1. UCAST('b \<rightarrow> 'a) (UCAST('a \<rightarrow> 'b) x) = x proof (chain)
picking this:
uint x \<le> uint (2 ^ LENGTH('b) - 1) proof (prove)
using this:
uint x \<le> uint (2 ^ LENGTH('b) - 1)

goal (1 subgoal):
 1. uint x \<le> 2 ^ LENGTH('b) - 1 proof (state)
this:
uint x \<le> 2 ^ LENGTH('b) - 1

goal (1 subgoal):
 1. UCAST('b \<rightarrow> 'a) (UCAST('a \<rightarrow> 'b) x) = x proof (chain)
picking this:
uint x \<le> 2 ^ LENGTH('b) - 1 proof (prove)
using this:
uint x \<le> 2 ^ LENGTH('b) - 1

goal (1 subgoal):
 1. UCAST('b \<rightarrow> 'a) (UCAST('a \<rightarrow> 'b) x) = x proof (prove)
goal (1 subgoal):
 1. uint x < 2 ^ LENGTH('b) \<Longrightarrow> LENGTH('a) \<le> LENGTH('b) \<or> x < 2 ^ LENGTH('b) proof (prove)
goal:
No subgoals! proof (state)
this:
UCAST('b \<rightarrow> 'a) (UCAST('a \<rightarrow> 'b) x) = x

goal:
No subgoals!