kings-crown/FVELER_Isabelle huggingface dataset:
theory Examples

lemma "\<not> 23 < (27::2 word)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> 23 < 27
theory Examples

lemma "0 < (4::3 word)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 0 < 4
theory Examples

lemma "1 < (4::3 word)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 1 < 4
theory Examples

lemma "0 < (1::3 word)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 0 < 1
theory Examples

lemma "a + 2 * b + c - b = (b + c) + (a :: 32 word)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a + 2 * b + c - b = b + c + a
theory Examples

lemma "uint (234567 :: 10 word) = 71" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. uint 234567 = 71
theory Examples

lemma "uint (-234567 :: 10 word) = 953" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. uint (- 234567) = 953
theory Examples

lemma "sint (234567 :: 10 word) = 71" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sint 234567 = 71
theory Examples

lemma "sint (-234567 :: 10 word) = -71" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sint (- 234567) = - 71
theory Examples

lemma "uint (1 :: 10 word) = 1" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. uint 1 = 1
theory Examples

lemma "unat (-234567 :: 10 word) = 953" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unat (- 234567) = 953
theory Examples

lemma "unat (1 :: 10 word) = 1" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unat 1 = 1
theory Examples

lemma "ucast (0b1010 :: 4 word) = (0b10 :: 2 word)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ucast 10 = 2
theory Examples

lemma "ucast (0b1010 :: 4 word) = (0b1010 :: 10 word)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ucast 10 = 10
theory Examples

lemma "scast (0b1010 :: 4 word) = (0b111010 :: 6 word)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. scast 10 = 58
theory Examples

lemma "ucast (1 :: 4 word) = (1 :: 2 word)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ucast 1 = 1
theory Examples

lemma "i < x \<Longrightarrow> i < i + 1" for i x :: "'a::len word" by unat_arith

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. i < x \<Longrightarrow> i < i + 1
theory Examples

lemma "0b110 AND 0b101 = (0b100 :: 32 word)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 6 AND 5 = 4
theory Examples

lemma "0b110 OR 0b011 = (0b111 :: 8 word)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 6 OR 3 = 7
theory Examples

lemma "0xF0 XOR 0xFF = (0x0F :: 8 word)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 240 XOR 255 = 15
theory Examples

lemma "NOT (0xF0 :: 16 word) = 0xFF0F" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. NOT 240 = 65295
theory Examples

lemma "0 AND 5 = (0 :: 8 word)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 0 AND 5 = 0
theory Examples

lemma "1 AND 1 = (1 :: 8 word)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 1 AND 1 = 1
theory Examples

lemma "1 AND 0 = (0 :: 8 word)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 1 AND 0 = 0
theory Examples

lemma "1 OR 6 = (7 :: 8 word)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 1 OR 6 = 7
theory Examples

lemma "1 OR 1 = (1 :: 8 word)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 1 OR 1 = 1
theory Examples

lemma "1 XOR 7 = (6 :: 8 word)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 1 XOR 7 = 6
theory Examples

lemma "NOT 0 = (255 :: 8 word)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. NOT 0 = 255
theory Examples

lemma "(-1 :: 32 word) = 0xFFFFFFFF" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. - 1 = 4294967295
theory Examples

lemma "bit (0b0010 :: 4 word) 1" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bit 2 1
theory Examples

lemma "\<not> bit (0b0010 :: 4 word) 0" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> bit 2 0
theory Examples

lemma "\<not> bit (0b1000 :: 3 word) 4" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> bit 8 4
theory Examples

lemma "\<not> bit (1 :: 3 word) 2" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> bit 1 2
theory Examples

lemma "bit (0b11000 :: 10 word) n = (n = 4 \<or> n = 3)" by (auto simp add: bit_numeral_rec bit_1_iff split: nat.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bit 24 n = (n = 4 \<or> n = 3)
theory Examples

lemma "set_bit 55 7 True = (183::'a::len word)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. set_bit_class.set_bit 55 7 True = 183
theory Examples

lemma "set_bit 0b0010 7 True = (0b10000010::'a::len word)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. set_bit_class.set_bit 2 7 True = 130
theory Examples

lemma "set_bit 1 3 True = (0b1001::'a::len word)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. set_bit_class.set_bit 1 3 True = 9
theory Examples

lemma "set_bit 1 0 False = (0::'a::len word)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. set_bit_class.set_bit 1 0 False = 0
theory Examples

lemma "set_bit 0 3 False = (0::'a::len word)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. set_bit_class.set_bit 0 3 False = 0
theory Examples

lemma "odd (0b0101::'a::len word)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. odd 5
theory Examples

lemma "even (0b1000::'a::len word)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. even 8
theory Examples

lemma "odd (1::'a::len word)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. odd 1
theory Examples

lemma "even (0::'a::len word)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. even 0
theory Examples

lemma "\<not> msb (0b0101::4 word)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> msb 5
theory Examples

lemma   "msb (0b1000::4 word)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. msb 8
theory Examples

lemma "\<not> msb (1::4 word)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> msb 1
theory Examples

lemma "\<not> msb (0::4 word)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> msb 0
theory Examples

lemma "word_cat (27::4 word) (27::8 word) = (2843::'a::len word)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. word_cat 27 27 = 2843
theory Examples

lemma "word_cat (0b0011::4 word) (0b1111::6word) = (0b0011001111 :: 10 word)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. word_cat 3 15 = 207
theory Examples

lemma "0b1011 << 2 = (0b101100::'a::len word)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 11 << 2 = 44
theory Examples

lemma "0b1011 >> 2 = (0b10::8 word)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 11 >> 2 = 2
theory Examples

lemma "0b1011 >>> 2 = (0b10::8 word)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 11 >>> 2 = 2
theory Examples

lemma "slice 3 (0b101111::6 word) = (0b101::3 word)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. slice 3 47 = 5
theory Examples

lemma "slice 3 (1::6 word) = (0::3 word)" apply simp? oops

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. slice 3 1 = 0 proof (prove)
goal (1 subgoal):
 1. slice 3 1 = 0
theory Examples

lemma "word_rotr 2 0b0110 = (0b1001::4 word)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. word_rotr 2 6 = 9
theory Examples

lemma "word_roti 2 0b1110 = (0b1011::4 word)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. word_roti 2 14 = 11
theory Examples

lemma "word_roti (- 2) 0b0110 = (0b1001::4 word)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. word_roti (- 2) 6 = 9
theory Examples

lemma "word_rotr 2 0 = (0::4 word)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. word_rotr 2 0 = 0
theory Examples

lemma "word_rotr 2 1 = (0b0100::4 word)" apply simp? oops

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. word_rotr 2 1 = 4 proof (prove)
goal (1 subgoal):
 1. word_rotr 2 1 = 4
theory Examples

lemma "word_rotl 2 1 = (0b0100::4 word)" apply simp? oops

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. word_rotl 2 1 = 4 proof (prove)
goal (1 subgoal):
 1. word_rotl 2 1 = 4
theory Examples

lemma "word_roti (- 2) 1 = (0b0100::4 word)" apply simp? oops

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. word_roti (- 2) 1 = 4 proof (prove)
goal (1 subgoal):
 1. word_rotl 2 1 = 4
theory Examples

lemma "(x AND 0xff00) OR (x AND 0x00ff) = (x::16 word)" proof - have "(x AND 0xff00) OR (x AND 0x00ff) = x AND (0xff00 OR 0x00ff)" by (simp only: word_ao_dist2) also have "0xff00 OR 0x00ff = (-1::16 word)" by simp also have "x AND -1 = x" by simp finally show ?thesis . qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x AND 65280 OR x AND 255 = x proof (state)
goal (1 subgoal):
 1. x AND 65280 OR x AND 255 = x proof (prove)
goal (1 subgoal):
 1. x AND 65280 OR x AND 255 = x AND (65280 OR 255) proof (state)
this:
x AND 65280 OR x AND 255 = x AND (65280 OR 255)

goal (1 subgoal):
 1. x AND 65280 OR x AND 255 = x proof (state)
this:
x AND 65280 OR x AND 255 = x AND (65280 OR 255)

goal (1 subgoal):
 1. x AND 65280 OR x AND 255 = x proof (prove)
goal (1 subgoal):
 1. 65280 OR 255 = - 1 proof (state)
this:
65280 OR 255 = - 1

goal (1 subgoal):
 1. x AND 65280 OR x AND 255 = x proof (state)
this:
65280 OR 255 = - 1

goal (1 subgoal):
 1. x AND 65280 OR x AND 255 = x proof (prove)
goal (1 subgoal):
 1. x AND - 1 = x proof (state)
this:
x AND - 1 = x

goal (1 subgoal):
 1. x AND 65280 OR x AND 255 = x proof (chain)
picking this:
x AND 65280 OR x AND 255 = x proof (prove)
using this:
x AND 65280 OR x AND 255 = x

goal (1 subgoal):
 1. x AND 65280 OR x AND 255 = x proof (state)
this:
x AND 65280 OR x AND 255 = x

goal:
No subgoals!
theory Examples

lemma "word_next (2:: 8 word) = 3" by eval

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. word_next 2 = 3
theory Examples

lemma "word_next (255:: 8 word) = 255" by eval

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. word_next 255 = 255
theory Examples

lemma "word_prev (2:: 8 word) = 1" by eval

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. word_prev 2 = 1
theory Examples

lemma "word_prev (0:: 8 word) = 0" by eval

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. word_prev 0 = 0
theory Examples

lemma "1 < (1024::32 word) \<and> 1 \<le> (1024::32 word)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 1 < 1024 \<and> 1 \<le> 1024
theory Examples

lemma "of_bl [True, False, True, True] = (0b1011::'a::len word)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. of_bl [True, False, True, True] = 11
theory Examples

lemma "to_bl (0b110::4 word) = [False, True, True, False]" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. to_bl 6 = [False, True, True, False]
theory Examples

lemma "of_bl (replicate 32 True) = (0xFFFFFFFF::32 word)" by (simp add: numeral_eq_Suc)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. of_bl (replicate 32 True) = 4294967295
theory Examples

lemma "(x AND 0xff00) OR (x AND 0x00ff) = (x::16 word)" by word_bitwise

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x AND 65280 OR x AND 255 = x
theory Examples

lemma "(x AND NOT 3) >> 4 << 2 = ((x >> 2) AND NOT 3)"
  for x :: "10 word" by word_bitwise

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x AND NOT 3 >> 4 << 2 = (x >> 2) AND NOT 3
theory Examples

lemma "((x AND -8) >> 3) AND 7 = (x AND 56) >> 3"
  for x :: "12 word" by word_bitwise

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x AND - 8 >> 3) AND 7 = x AND 56 >> 3
theory Examples

lemma "x \<le> 42 \<Longrightarrow> x \<le> 89"
  for x :: "8 word" apply word_bitwise apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<le> 42 \<Longrightarrow> x \<le> 89 proof (prove)
goal (1 subgoal):
 1. \<not> bit x 7 \<and> \<not> bit x 6 \<and> (bit x 5 \<longrightarrow> \<not> bit x 4 \<and> (bit x 3 \<longrightarrow> \<not> bit x 2 \<and> (bit x 1 \<longrightarrow> \<not> bit x 0))) \<Longrightarrow> \<not> bit x 7 \<and> (bit x 6 \<longrightarrow> \<not> bit x 5 \<and> (bit x 3 \<longrightarrow> bit x 4 \<longrightarrow> \<not> bit x 2 \<and> \<not> bit x 1)) proof (prove)
goal:
No subgoals!
theory Examples

lemma "(x AND 1023) = 0 \<Longrightarrow> x \<le> -1024"
  for x :: \<open>32 word\<close> apply word_bitwise apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x AND 1023 = 0 \<Longrightarrow> x \<le> - 1024 proof (prove)
goal (1 subgoal):
 1. \<not> bit x 0 \<and> \<not> bit x 1 \<and> \<not> bit x 2 \<and> \<not> bit x 3 \<and> \<not> bit x 4 \<and> \<not> bit x 5 \<and> \<not> bit x 6 \<and> \<not> bit x 7 \<and> \<not> bit x 8 \<and> \<not> bit x 9 \<Longrightarrow> bit x 10 \<longrightarrow> bit x 11 \<longrightarrow> bit x 12 \<longrightarrow> bit x 13 \<longrightarrow> bit x 14 \<longrightarrow> bit x 15 \<longrightarrow> bit x 16 \<longrightarrow> bit x 17 \<longrightarrow> bit x 18 \<longrightarrow> bit x 19 \<longrightarrow> bit x 20 \<longrightarrow> bit x 21 \<longrightarrow> bit x 22 \<longrightarrow> bit x 23 \<longrightarrow> bit x 24 \<longrightarrow> bit x 25 \<longrightarrow> bit x 26 \<longrightarrow> bit x 27 \<longrightarrow> bit x 28 \<longrightarrow> bit x 29 \<longrightarrow> bit x 30 \<longrightarrow> bit x 31 \<longrightarrow> \<not> bit x 9 \<and> \<not> bit x 8 \<and> \<not> bit x 7 \<and> \<not> bit x 6 \<and> \<not> bit x 5 \<and> \<not> bit x 4 \<and> \<not> bit x 3 \<and> \<not> bit x 2 \<and> \<not> bit x 1 \<and> \<not> bit x 0 proof (prove)
goal:
No subgoals!
theory Examples

lemma shiftr_overflow: "32 \<le> a \<Longrightarrow> b >> a = 0"
  for b :: \<open>32 word\<close> apply word_bitwise apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 32 \<le> a \<Longrightarrow> b >> a = 0 proof (prove)
goal (1 subgoal):
 1. 32 \<le> a \<Longrightarrow> takefill False (Suc (Suc (Suc (Suc 28)))) (drop a [bit b 0, bit b 1, bit b 2, bit b 3, bit b 4, bit b 5, bit b 6, bit b 7, bit b 8, bit b 9, bit b 10, bit b 11, bit b 12, bit b 13, bit b 14, bit b 15, bit b 16, bit b 17, bit b 18, bit b 19, bit b 20, bit b 21, bit b 22, bit b 23, bit b 24, bit b 25, bit b 26, bit b 27, bit b 28, bit b 29, bit b 30, bit b 31]) = [False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False] proof (prove)
goal:
No subgoals!
theory Examples

lemma "((x :: 32 word) >> 3) AND 7 = (x AND 56) >> 3" by word_bitwise

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x >> 3) AND 7 = x AND 56 >> 3
theory Word_64

lemma len64: "len_of (x :: 64 itself) = 64" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. len_of x = 64
theory Word_64

lemma ucast_8_64_inj:
  "inj (ucast ::  8 word \<Rightarrow> 64 word)" by (rule down_ucast_inj) (clarsimp simp: is_down_def target_size source_size)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. inj UCAST(8 \<rightarrow> 64)
theory Word_64

lemma less_4_cases:
  "(x::word64) < 4 \<Longrightarrow> x=0 \<or> x=1 \<or> x=2 \<or> x=3" apply clarsimp apply (drule word_less_cases, erule disjE, simp, simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x < 4 \<Longrightarrow> x = 0 \<or> x = 1 \<or> x = 2 \<or> x = 3 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x < 4; x \<noteq> 0; x \<noteq> 1; x \<noteq> 3\<rbrakk> \<Longrightarrow> x = 2 proof (prove)
goal:
No subgoals!
theory Word_64

lemma ucast_le_ucast_8_64:
  "(ucast x \<le> (ucast y :: word64)) = (x \<le> (y :: 8 word))" by (simp add: ucast_le_ucast)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (UCAST(8 \<rightarrow> 64) x \<le> UCAST(8 \<rightarrow> 64) y) = (x \<le> y)
theory Word_64

lemma eq_2_64_0:
  "(2 ^ 64 :: word64) = 0" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 2 ^ 64 = 0
theory Word_64

lemma of_nat64_n_less_equal_power_2:
 "n < 64 \<Longrightarrow> ((of_nat n)::64 word) < 2 ^ n" by (rule of_nat_n_less_equal_power_2, clarsimp simp: word_size)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n < 64 \<Longrightarrow> word_of_nat n < 2 ^ n
theory Word_64

lemma unat_ucast_10_64 :
  fixes x :: "10 word"
  shows "unat (ucast x :: word64) = unat x" by transfer simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unat (UCAST(10 \<rightarrow> 64) x) = unat x
theory Word_64

lemma word64_bounds:
  "- (2 ^ (size (x :: word64) - 1)) = (-9223372036854775808 :: int)"
  "((2 ^ (size (x :: word64) - 1)) - 1) = (9223372036854775807 :: int)"
  "- (2 ^ (size (y :: 64 signed word) - 1)) = (-9223372036854775808 :: int)"
  "((2 ^ (size (y :: 64 signed word) - 1)) - 1) = (9223372036854775807 :: int)" by (simp_all add: word_size)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (- (2 ^ (size x - 1)) = - 9223372036854775808 &&& 2 ^ (size x - 1) - 1 = 9223372036854775807) &&& - (2 ^ (size y - 1)) = - 9223372036854775808 &&& 2 ^ (size y - 1) - 1 = 9223372036854775807
theory Word_64

lemma ucast_of_nats [simp]:
  "(ucast (of_nat x :: word64) :: sword64) = (of_nat x)"
  "(ucast (of_nat x :: word64) :: 16 sword) = (of_nat x)"
  "(ucast (of_nat x :: word64) :: 8 sword) = (of_nat x)" by (simp_all add: of_nat_take_bit take_bit_word_eq_self unsigned_of_nat)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. UCAST(64 \<rightarrow> 64 signed) (word_of_nat x) = word_of_nat x &&& UCAST(64 \<rightarrow> 16 signed) (word_of_nat x) = word_of_nat x &&& UCAST(64 \<rightarrow> 8 signed) (word_of_nat x) = word_of_nat x
theory Word_64

lemma word64_31_less:
  "31 < len_of TYPE (64 signed)" "31 > (0 :: nat)"
  "31 < len_of TYPE (64)" "31 > (0 :: nat)" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (31 < LENGTH(64 signed) &&& 0 < 31) &&& 31 < LENGTH(64) &&& 0 < 31
theory Word_64

lemma unat_of_int_64:
  "\<lbrakk>i \<ge> 0; i \<le> 2 ^ 63\<rbrakk> \<Longrightarrow> (unat ((of_int i)::sword64)) = nat i" by (simp add: unsigned_of_int nat_take_bit_eq take_bit_nat_eq_self)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 \<le> i; i \<le> 2 ^ 63\<rbrakk> \<Longrightarrow> unat (word_of_int i) = nat i
theory Word_64

lemma word64_and_max_simp:
  \<open>x AND 0xFFFFFFFFFFFFFFFF = x\<close> for x :: \<open>64 word\<close> using word_and_full_mask_simp [of x] by (simp add: numeral_eq_Suc mask_Suc_exp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x && 18446744073709551615 = x proof (prove)
using this:
x && mask LENGTH(64) = x

goal (1 subgoal):
 1. x && 18446744073709551615 = x
theory Machine_Word_64_Basics

lemma word_bits_conv [code]:
  \<open>word_bits = 64\<close> by (simp add: word_bits_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. word_bits = 64
theory Machine_Word_64_Basics

lemma n_less_word_bits:
  "(n < word_bits) = (n < 64)" by (simp add: word_bits_def word_size_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (n < word_bits) = (n < 64)
theory Machine_Word_64_Basics

lemma of_nat64_0:
  "\<lbrakk>of_nat n = (0::word64); n < 2 ^ word_bits\<rbrakk> \<Longrightarrow> n = 0" by (erule of_nat_0, simp add: word_bits_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>word_of_nat n = 0; n < 2 ^ word_bits\<rbrakk> \<Longrightarrow> n = 0
theory Machine_Word_64

lemma word_bits_len_of:
  \<open>LENGTH(machine_word_len) = word_bits\<close> by (simp add: word_bits_conv)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. LENGTH(64) = word_bits
theory Machine_Word_64

lemma word_bits_size:
  "size (w :: machine_word) = word_bits" by (simp add: word_bits_def word_size)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. size w = word_bits
theory Machine_Word_64

lemma word_bits_word_size_conv:
  \<open>word_bits = word_size * 8\<close> by (simp add: word_bits_def word_size_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. word_bits = word_size * 8
theory Machine_Word_64

lemma lt_word_bits_lt_pow:
  "sz < word_bits \<Longrightarrow> sz < 2 ^ word_bits" by (simp add: word_bits_conv)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sz < word_bits \<Longrightarrow> sz < 2 ^ word_bits
theory Machine_Word_64

lemma if_then_1_else_0:
  "((if P then 1 else 0) = (0 :: machine_word)) = (\<not> P)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((if P then 1 else 0) = 0) = (\<not> P)
theory Machine_Word_64

lemma if_then_0_else_1:
  "((if P then 0 else 1) = (0 :: machine_word)) = (P)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((if P then 0 else 1) = 0) = P
theory Machine_Word_64

lemma bool_mask [simp]:
  \<open>0 < x AND 1 \<longleftrightarrow> x AND 1 = 1\<close> for x :: machine_word by (rule bool_mask') auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (0 < x && 1) = (x && 1 = 1)
theory Machine_Word_64

lemma in_16_range:
  "0 \<in> S \<Longrightarrow> r \<in> (\<lambda>x. r + x * (16 :: machine_word)) ` S"
  "n - 1 \<in> S \<Longrightarrow> (r + (16 * n - 16)) \<in> (\<lambda>x :: machine_word. r + x * 16) ` S" by (clarsimp simp: image_def elim!: bexI[rotated])+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (0 \<in> S \<Longrightarrow> r \<in> (\<lambda>x. r + x * 16) ` S) &&& (n - 1 \<in> S \<Longrightarrow> r + (16 * n - 16) \<in> (\<lambda>x. r + x * 16) ` S)
theory Machine_Word_64

lemma le_step_down_word_3:
  fixes x :: machine_word
  shows "\<lbrakk>x \<le> y; x \<noteq> y\<rbrakk> \<Longrightarrow> x \<le> y - 1" by (fact le_step_down_word_2)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<le> y; x \<noteq> y\<rbrakk> \<Longrightarrow> x \<le> y - 1
theory Machine_Word_64

lemma shiftr_1:
  "(x::machine_word) >> 1 = 0 \<Longrightarrow> x < 2" apply transfer apply (simp add: take_bit_drop_bit) apply (simp add: drop_bit_Suc) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x >> 1 = 0 \<Longrightarrow> x < 2 proof (prove)
goal (1 subgoal):
 1. \<And>x. take_bit LENGTH(64) (drop_bit 1 (take_bit LENGTH(64) x)) = take_bit LENGTH(64) 0 \<Longrightarrow> take_bit LENGTH(64) x < take_bit LENGTH(64) 2 proof (prove)
goal (1 subgoal):
 1. \<And>x. drop_bit (Suc 0) (take_bit 64 x) = 0 \<Longrightarrow> take_bit 64 x < 2 proof (prove)
goal:
No subgoals!
theory Machine_Word_64

lemma Suc_unat_mask_div:
  "Suc (unat (mask sz div word_size :: machine_word)) = 2 ^ (min sz word_bits - word_size_bits)" by (simp add: word_size_word_size_bits unat_drop_bit_eq unat_mask_eq drop_bit_mask_eq Suc_mask_eq_exp
    flip: drop_bit_eq_div word_bits_conv)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Suc (unat (mask sz div word_size)) = 2 ^ (min sz word_bits - word_size_bits)