kings-crown/FVELER_Isabelle huggingface dataset:
theory Word_Lemmas

lemma upto_enum_step_subset:
  "set [x, y .e. z] \<subseteq> {x .. z}" apply (clarsimp simp: upto_enum_step_def linorder_not_less) apply (drule div_to_mult_word_lt) apply (rule conjI) apply (erule word_random[rotated]) apply simp apply (rule order_trans) apply (erule word_plus_mono_right) apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. set [x , y .e. z] \<subseteq> {x..z} proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>x \<le> z; xa \<le> (z - x) div (y - x)\<rbrakk> \<Longrightarrow> x \<le> x + xa * (y - x) \<and> x + xa * (y - x) \<le> z proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>x \<le> z; xa * (y - x) \<le> z - x\<rbrakk> \<Longrightarrow> x \<le> x + xa * (y - x) \<and> x + xa * (y - x) \<le> z proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>x \<le> z; xa * (y - x) \<le> z - x\<rbrakk> \<Longrightarrow> x \<le> x + xa * (y - x)
 2. \<And>xa. \<lbrakk>x \<le> z; xa * (y - x) \<le> z - x\<rbrakk> \<Longrightarrow> x + xa * (y - x) \<le> z proof (prove)
goal (2 subgoals):
 1. \<And>xa. x \<le> z \<Longrightarrow> x \<le> x + (z - x)
 2. \<And>xa. \<lbrakk>x \<le> z; xa * (y - x) \<le> z - x\<rbrakk> \<Longrightarrow> x + xa * (y - x) \<le> z proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>x \<le> z; xa * (y - x) \<le> z - x\<rbrakk> \<Longrightarrow> x + xa * (y - x) \<le> z proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>x \<le> z; xa * (y - x) \<le> z - x\<rbrakk> \<Longrightarrow> x + xa * (y - x) \<le> ?y20 xa
 2. \<And>xa. \<lbrakk>x \<le> z; xa * (y - x) \<le> z - x\<rbrakk> \<Longrightarrow> ?y20 xa \<le> z proof (prove)
goal (2 subgoals):
 1. \<And>xa. x \<le> z \<Longrightarrow> x \<le> x + (z - x)
 2. \<And>xa. \<lbrakk>x \<le> z; xa * (y - x) \<le> z - x\<rbrakk> \<Longrightarrow> x + (z - x) \<le> z proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>x \<le> z; xa * (y - x) \<le> z - x\<rbrakk> \<Longrightarrow> x + (z - x) \<le> z proof (prove)
goal:
No subgoals!
theory Word_Lemmas

lemma ucast_distrib:
  fixes M :: "'a::len word \<Rightarrow> 'a::len word \<Rightarrow> 'a::len word"
  fixes M' :: "'b::len word \<Rightarrow> 'b::len word \<Rightarrow> 'b::len word"
  fixes L :: "int \<Rightarrow> int \<Rightarrow> int"
  assumes lift_M: "\<And>x y. uint (M x y) = L (uint x) (uint y)  mod 2 ^ LENGTH('a)"
  assumes lift_M': "\<And>x y. uint (M' x y) = L (uint x) (uint y)  mod 2 ^ LENGTH('b)"
  assumes distrib: "\<And>x y. (L (x mod (2 ^ LENGTH('b))) (y mod (2 ^ LENGTH('b)))) mod (2 ^ LENGTH('b))
                               = (L x y) mod (2 ^ LENGTH('b))"
  assumes is_down: "is_down (ucast :: 'a word \<Rightarrow> 'b word)"
  shows "ucast (M a b) = M' (ucast a) (ucast b)" apply (simp only: ucast_eq) apply (subst lift_M) apply (subst of_int_uint [symmetric], subst lift_M') apply (metis local.distrib local.is_down take_bit_eq_mod ucast_down_wi uint_word_of_int_eq word_of_int_uint) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. UCAST('a \<rightarrow> 'b) (M a b) = M' (UCAST('a \<rightarrow> 'b) a) (UCAST('a \<rightarrow> 'b) b) proof (prove)
goal (1 subgoal):
 1. word_of_int (uint (M a b)) = M' (word_of_int (uint a)) (word_of_int (uint b)) proof (prove)
goal (1 subgoal):
 1. word_of_int (L (uint a) (uint b) mod 2 ^ LENGTH('a)) = M' (word_of_int (uint a)) (word_of_int (uint b)) proof (prove)
goal (1 subgoal):
 1. word_of_int (L (uint a) (uint b) mod 2 ^ LENGTH('a)) = word_of_int (L (uint (word_of_int (uint a))) (uint (word_of_int (uint b))) mod 2 ^ LENGTH('b)) proof (prove)
goal:
No subgoals!
theory Word_Lemmas

lemma ucast_down_add:
    "is_down (ucast:: 'a word \<Rightarrow> 'b word) \<Longrightarrow>  ucast ((a :: 'a::len word) + b) = (ucast a + ucast b :: 'b::len word)" by (rule ucast_distrib [where L="(+)"], (clarsimp simp: uint_word_ariths)+, presburger, simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_down UCAST('a \<rightarrow> 'b) \<Longrightarrow> UCAST('a \<rightarrow> 'b) (a + b) = UCAST('a \<rightarrow> 'b) a + UCAST('a \<rightarrow> 'b) b
theory Word_Lemmas

lemma ucast_down_minus:
    "is_down (ucast:: 'a word \<Rightarrow> 'b word) \<Longrightarrow>  ucast ((a :: 'a::len word) - b) = (ucast a - ucast b :: 'b::len word)" apply (rule ucast_distrib [where L="(-)"], (clarsimp simp: uint_word_ariths)+) apply (metis mod_diff_left_eq mod_diff_right_eq) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_down UCAST('a \<rightarrow> 'b) \<Longrightarrow> UCAST('a \<rightarrow> 'b) (a - b) = UCAST('a \<rightarrow> 'b) a - UCAST('a \<rightarrow> 'b) b proof (prove)
goal (2 subgoals):
 1. \<And>x y. is_down UCAST('a \<rightarrow> 'b) \<Longrightarrow> (x mod 2 ^ LENGTH('b) - y mod 2 ^ LENGTH('b)) mod 2 ^ LENGTH('b) = (x - y) mod 2 ^ LENGTH('b)
 2. is_down UCAST('a \<rightarrow> 'b) \<Longrightarrow> is_down UCAST('a \<rightarrow> 'b) proof (prove)
goal (1 subgoal):
 1. is_down UCAST('a \<rightarrow> 'b) \<Longrightarrow> is_down UCAST('a \<rightarrow> 'b) proof (prove)
goal:
No subgoals!
theory Word_Lemmas

lemma ucast_down_mult:
    "is_down (ucast:: 'a word \<Rightarrow> 'b word) \<Longrightarrow>  ucast ((a :: 'a::len word) * b) = (ucast a * ucast b :: 'b::len word)" apply (rule ucast_distrib [where L="(*)"], (clarsimp simp: uint_word_ariths)+) apply (metis mod_mult_eq) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_down UCAST('a \<rightarrow> 'b) \<Longrightarrow> UCAST('a \<rightarrow> 'b) (a * b) = UCAST('a \<rightarrow> 'b) a * UCAST('a \<rightarrow> 'b) b proof (prove)
goal (2 subgoals):
 1. \<And>x y. is_down UCAST('a \<rightarrow> 'b) \<Longrightarrow> x mod 2 ^ LENGTH('b) * (y mod 2 ^ LENGTH('b)) mod 2 ^ LENGTH('b) = x * y mod 2 ^ LENGTH('b)
 2. is_down UCAST('a \<rightarrow> 'b) \<Longrightarrow> is_down UCAST('a \<rightarrow> 'b) proof (prove)
goal (1 subgoal):
 1. is_down UCAST('a \<rightarrow> 'b) \<Longrightarrow> is_down UCAST('a \<rightarrow> 'b) proof (prove)
goal:
No subgoals!
theory Word_Lemmas

lemma scast_distrib:
  fixes M :: "'a::len word \<Rightarrow> 'a::len word \<Rightarrow> 'a::len word"
  fixes M' :: "'b::len word \<Rightarrow> 'b::len word \<Rightarrow> 'b::len word"
  fixes L :: "int \<Rightarrow> int \<Rightarrow> int"
  assumes lift_M: "\<And>x y. uint (M x y) = L (uint x) (uint y)  mod 2 ^ LENGTH('a)"
  assumes lift_M': "\<And>x y. uint (M' x y) = L (uint x) (uint y)  mod 2 ^ LENGTH('b)"
  assumes distrib: "\<And>x y. (L (x mod (2 ^ LENGTH('b))) (y mod (2 ^ LENGTH('b)))) mod (2 ^ LENGTH('b))
                               = (L x y) mod (2 ^ LENGTH('b))"
  assumes is_down: "is_down (scast :: 'a word \<Rightarrow> 'b word)"
  shows "scast (M a b) = M' (scast a) (scast b)" apply (subst (1 2 3) down_cast_same [symmetric]) apply (insert is_down) apply (clarsimp simp: is_down_def target_size source_size is_down) apply (rule ucast_distrib [where L=L, OF lift_M lift_M' distrib]) apply (insert is_down) apply (clarsimp simp: is_down_def target_size source_size is_down) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. SCAST('a \<rightarrow> 'b) (M a b) = M' (SCAST('a \<rightarrow> 'b) a) (SCAST('a \<rightarrow> 'b) b) proof (prove)
goal (2 subgoals):
 1. is_down UCAST('a \<rightarrow> 'b)
 2. UCAST('a \<rightarrow> 'b) (M a b) = M' (UCAST('a \<rightarrow> 'b) a) (UCAST('a \<rightarrow> 'b) b) proof (prove)
goal (2 subgoals):
 1. is_down SCAST('a \<rightarrow> 'b) \<Longrightarrow> is_down UCAST('a \<rightarrow> 'b)
 2. is_down SCAST('a \<rightarrow> 'b) \<Longrightarrow> UCAST('a \<rightarrow> 'b) (M a b) = M' (UCAST('a \<rightarrow> 'b) a) (UCAST('a \<rightarrow> 'b) b) proof (prove)
goal (1 subgoal):
 1. is_down SCAST('a \<rightarrow> 'b) \<Longrightarrow> UCAST('a \<rightarrow> 'b) (M a b) = M' (UCAST('a \<rightarrow> 'b) a) (UCAST('a \<rightarrow> 'b) b) proof (prove)
goal (1 subgoal):
 1. is_down SCAST('a \<rightarrow> 'b) \<Longrightarrow> is_down UCAST('a \<rightarrow> 'b) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_down SCAST('a \<rightarrow> 'b); is_down SCAST('a \<rightarrow> 'b)\<rbrakk> \<Longrightarrow> is_down UCAST('a \<rightarrow> 'b) proof (prove)
goal:
No subgoals!
theory Word_Lemmas

lemma scast_down_add:
    "is_down (scast:: 'a word \<Rightarrow> 'b word) \<Longrightarrow>  scast ((a :: 'a::len word) + b) = (scast a + scast b :: 'b::len word)" by (rule scast_distrib [where L="(+)"], (clarsimp simp: uint_word_ariths)+, presburger, simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_down SCAST('a \<rightarrow> 'b) \<Longrightarrow> SCAST('a \<rightarrow> 'b) (a + b) = SCAST('a \<rightarrow> 'b) a + SCAST('a \<rightarrow> 'b) b
theory Word_Lemmas

lemma scast_down_minus:
    "is_down (scast:: 'a word \<Rightarrow> 'b word) \<Longrightarrow>  scast ((a :: 'a::len word) - b) = (scast a - scast b :: 'b::len word)" apply (rule scast_distrib [where L="(-)"], (clarsimp simp: uint_word_ariths)+) apply (metis mod_diff_left_eq mod_diff_right_eq) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_down SCAST('a \<rightarrow> 'b) \<Longrightarrow> SCAST('a \<rightarrow> 'b) (a - b) = SCAST('a \<rightarrow> 'b) a - SCAST('a \<rightarrow> 'b) b proof (prove)
goal (2 subgoals):
 1. \<And>x y. is_down SCAST('a \<rightarrow> 'b) \<Longrightarrow> (x mod 2 ^ LENGTH('b) - y mod 2 ^ LENGTH('b)) mod 2 ^ LENGTH('b) = (x - y) mod 2 ^ LENGTH('b)
 2. is_down SCAST('a \<rightarrow> 'b) \<Longrightarrow> is_down SCAST('a \<rightarrow> 'b) proof (prove)
goal (1 subgoal):
 1. is_down SCAST('a \<rightarrow> 'b) \<Longrightarrow> is_down SCAST('a \<rightarrow> 'b) proof (prove)
goal:
No subgoals!
theory Word_Lemmas

lemma scast_down_mult:
    "is_down (scast:: 'a word \<Rightarrow> 'b word) \<Longrightarrow>  scast ((a :: 'a::len word) * b) = (scast a * scast b :: 'b::len word)" apply (rule scast_distrib [where L="(*)"], (clarsimp simp: uint_word_ariths)+) apply (metis mod_mult_eq) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_down SCAST('a \<rightarrow> 'b) \<Longrightarrow> SCAST('a \<rightarrow> 'b) (a * b) = SCAST('a \<rightarrow> 'b) a * SCAST('a \<rightarrow> 'b) b proof (prove)
goal (2 subgoals):
 1. \<And>x y. is_down SCAST('a \<rightarrow> 'b) \<Longrightarrow> x mod 2 ^ LENGTH('b) * (y mod 2 ^ LENGTH('b)) mod 2 ^ LENGTH('b) = x * y mod 2 ^ LENGTH('b)
 2. is_down SCAST('a \<rightarrow> 'b) \<Longrightarrow> is_down SCAST('a \<rightarrow> 'b) proof (prove)
goal (1 subgoal):
 1. is_down SCAST('a \<rightarrow> 'b) \<Longrightarrow> is_down SCAST('a \<rightarrow> 'b) proof (prove)
goal:
No subgoals!
theory Word_Lemmas

lemma scast_ucast_1:
  "\<lbrakk> is_down (ucast :: 'a word \<Rightarrow> 'b word); is_down (ucast :: 'b word \<Rightarrow> 'c word) \<rbrakk> \<Longrightarrow>
         (scast (ucast (a :: 'a::len word) :: 'b::len word) :: 'c::len word) = ucast a" by (metis down_cast_same ucast_eq ucast_down_wi)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_down UCAST('a \<rightarrow> 'b); is_down UCAST('b \<rightarrow> 'c)\<rbrakk> \<Longrightarrow> SCAST('b \<rightarrow> 'c) (UCAST('a \<rightarrow> 'b) a) = UCAST('a \<rightarrow> 'c) a
theory Word_Lemmas

lemma scast_ucast_3:
  "\<lbrakk> is_down (ucast :: 'a word \<Rightarrow> 'c word); is_down (ucast :: 'b word \<Rightarrow> 'c word) \<rbrakk> \<Longrightarrow>
         (scast (ucast (a :: 'a::len word) :: 'b::len word) :: 'c::len word) = ucast a" by (metis down_cast_same ucast_eq ucast_down_wi)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_down UCAST('a \<rightarrow> 'c); is_down UCAST('b \<rightarrow> 'c)\<rbrakk> \<Longrightarrow> SCAST('b \<rightarrow> 'c) (UCAST('a \<rightarrow> 'b) a) = UCAST('a \<rightarrow> 'c) a
theory Word_Lemmas

lemma scast_ucast_4:
  "\<lbrakk> is_up (ucast :: 'a word \<Rightarrow> 'b word); is_down (ucast :: 'b word \<Rightarrow> 'c word) \<rbrakk> \<Longrightarrow>
         (scast (ucast (a :: 'a::len word) :: 'b::len word) :: 'c::len word) = ucast a" by (metis down_cast_same ucast_eq ucast_down_wi)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_up UCAST('a \<rightarrow> 'b); is_down UCAST('b \<rightarrow> 'c)\<rbrakk> \<Longrightarrow> SCAST('b \<rightarrow> 'c) (UCAST('a \<rightarrow> 'b) a) = UCAST('a \<rightarrow> 'c) a
theory Word_Lemmas

lemma ucast_scast_1:
  "\<lbrakk> is_down (scast :: 'a word \<Rightarrow> 'b word); is_down (ucast :: 'b word \<Rightarrow> 'c word) \<rbrakk> \<Longrightarrow>
            (ucast (scast (a :: 'a::len word) :: 'b::len word) :: 'c::len word) = scast a" by (metis scast_eq ucast_down_wi)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_down SCAST('a \<rightarrow> 'b); is_down UCAST('b \<rightarrow> 'c)\<rbrakk> \<Longrightarrow> UCAST('b \<rightarrow> 'c) (SCAST('a \<rightarrow> 'b) a) = SCAST('a \<rightarrow> 'c) a
theory Word_Lemmas

lemma ucast_scast_3:
  "\<lbrakk> is_down (scast :: 'a word \<Rightarrow> 'c word); is_down (ucast :: 'b word \<Rightarrow> 'c word) \<rbrakk> \<Longrightarrow>
     (ucast (scast (a :: 'a::len word) :: 'b::len word) :: 'c::len word) = scast a" by (metis scast_eq ucast_down_wi)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_down SCAST('a \<rightarrow> 'c); is_down UCAST('b \<rightarrow> 'c)\<rbrakk> \<Longrightarrow> UCAST('b \<rightarrow> 'c) (SCAST('a \<rightarrow> 'b) a) = SCAST('a \<rightarrow> 'c) a
theory Word_Lemmas

lemma ucast_scast_4:
  "\<lbrakk> is_up (scast :: 'a word \<Rightarrow> 'b word); is_down (ucast :: 'b word \<Rightarrow> 'c word) \<rbrakk> \<Longrightarrow>
     (ucast (scast (a :: 'a::len word) :: 'b::len word) :: 'c::len word) = scast a" by (metis down_cast_same scast_eq sint_up_scast)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_up SCAST('a \<rightarrow> 'b); is_down UCAST('b \<rightarrow> 'c)\<rbrakk> \<Longrightarrow> UCAST('b \<rightarrow> 'c) (SCAST('a \<rightarrow> 'b) a) = SCAST('a \<rightarrow> 'c) a
theory Word_Lemmas

lemma ucast_ucast_a:
  "\<lbrakk> is_down (ucast :: 'b word \<Rightarrow> 'c word) \<rbrakk> \<Longrightarrow>
        (ucast (ucast (a :: 'a::len word) :: 'b::len word) :: 'c::len word) = ucast a" by (metis down_cast_same ucast_eq ucast_down_wi)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_down UCAST('b \<rightarrow> 'c) \<Longrightarrow> UCAST('b \<rightarrow> 'c) (UCAST('a \<rightarrow> 'b) a) = UCAST('a \<rightarrow> 'c) a
theory Word_Lemmas

lemma ucast_ucast_b:
  "\<lbrakk> is_up (ucast :: 'a word \<Rightarrow> 'b word) \<rbrakk> \<Longrightarrow>
     (ucast (ucast (a :: 'a::len word) :: 'b::len word) :: 'c::len word) = ucast a" by (metis ucast_up_ucast)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_up UCAST('a \<rightarrow> 'b) \<Longrightarrow> UCAST('b \<rightarrow> 'c) (UCAST('a \<rightarrow> 'b) a) = UCAST('a \<rightarrow> 'c) a
theory Word_Lemmas

lemma scast_scast_a:
  "\<lbrakk> is_down (scast :: 'b word \<Rightarrow> 'c word) \<rbrakk> \<Longrightarrow>
            (scast (scast (a :: 'a::len word) :: 'b::len word) :: 'c::len word) = scast a" apply (simp only: scast_eq) apply (metis down_cast_same is_up_down scast_eq ucast_down_wi) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_down SCAST('b \<rightarrow> 'c) \<Longrightarrow> SCAST('b \<rightarrow> 'c) (SCAST('a \<rightarrow> 'b) a) = SCAST('a \<rightarrow> 'c) a proof (prove)
goal (1 subgoal):
 1. is_down SCAST('b \<rightarrow> 'c) \<Longrightarrow> word_of_int (sint (word_of_int (sint a))) = word_of_int (sint a) proof (prove)
goal:
No subgoals!
theory Word_Lemmas

lemma scast_down_wi [OF refl]:
  "uc = scast \<Longrightarrow> is_down uc \<Longrightarrow> uc (word_of_int x) = word_of_int x" by (metis down_cast_same is_up_down ucast_down_wi)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>uc = SCAST('a \<rightarrow> 'b); is_down uc\<rbrakk> \<Longrightarrow> uc (word_of_int x) = word_of_int x
theory Word_Lemmas

lemma signed_arith_sint:
  "((- (2 ^ (size a - 1)) \<le> (sint a + sint b)) \<and> (sint a + sint b \<le> (2 ^ (size a - 1) - 1)))
    \<Longrightarrow> sint (a + b) = (sint a + sint b)"
  "((- (2 ^ (size a - 1)) \<le> (sint a - sint b)) \<and> (sint a - sint b \<le> (2 ^ (size a - 1) - 1)))
    \<Longrightarrow> sint (a - b) = (sint a - sint b)"
  "((- (2 ^ (size a - 1)) \<le> (- sint a)) \<and> (- sint a) \<le> (2 ^ (size a - 1) - 1))
    \<Longrightarrow> sint (- a) = (- sint a)"
  "((- (2 ^ (size a - 1)) \<le> (sint a * sint b)) \<and> (sint a * sint b \<le> (2 ^ (size a - 1) - 1)))
    \<Longrightarrow> sint (a * b) = (sint a * sint b)"
  "((- (2 ^ (size a - 1)) \<le> (sint a sdiv sint b)) \<and> (sint a sdiv sint b \<le> (2 ^ (size a - 1) - 1)))
    \<Longrightarrow> sint (a sdiv b) = (sint a sdiv sint b)"
  "((- (2 ^ (size a - 1)) \<le> (sint a smod sint b)) \<and> (sint a smod sint b \<le> (2 ^ (size a - 1) - 1)))
    \<Longrightarrow> sint (a smod b) = (sint a smod sint b)" by (subst (asm) signed_arith_ineq_checks_to_eq; simp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((- (2 ^ (size a - 1)) \<le> sint a + sint b \<and> sint a + sint b \<le> 2 ^ (size a - 1) - 1 \<Longrightarrow> sint (a + b) = sint a + sint b) &&& (- (2 ^ (size a - 1)) \<le> sint a - sint b \<and> sint a - sint b \<le> 2 ^ (size a - 1) - 1 \<Longrightarrow> sint (a - b) = sint a - sint b) &&& (- (2 ^ (size a - 1)) \<le> - sint a \<and> - sint a \<le> 2 ^ (size a - 1) - 1 \<Longrightarrow> sint (- a) = - sint a)) &&& (- (2 ^ (size a - 1)) \<le> sint a * sint b \<and> sint a * sint b \<le> 2 ^ (size a - 1) - 1 \<Longrightarrow> sint (a * b) = sint a * sint b) &&& (- (2 ^ (size a - 1)) \<le> sint a sdiv sint b \<and> sint a sdiv sint b \<le> 2 ^ (size a - 1) - 1 \<Longrightarrow> sint (a sdiv b) = sint a sdiv sint b) &&& (- (2 ^ (size a - 1)) \<le> sint a smod sint b \<and> sint a smod sint b \<le> 2 ^ (size a - 1) - 1 \<Longrightarrow> sint (a smod b) = sint a smod sint b)
theory Word_Lemmas

lemma nasty_split_lt:
  \<open>x * 2 ^ n + (2 ^ n - 1) \<le> 2 ^ m - 1\<close>
    if \<open>x < 2 ^ (m - n)\<close> \<open>n \<le> m\<close> \<open>m < LENGTH('a::len)\<close>
    for x :: \<open>'a::len word\<close> proof - define q where \<open>q = m - n\<close> with \<open>n \<le> m\<close> have \<open>m = q + n\<close> by simp with \<open>x < 2 ^ (m - n)\<close> have *: \<open>i < q\<close> if \<open>bit x i\<close> for i using that by simp (metis bit_take_bit_iff take_bit_word_eq_self_iff) from \<open>m = q + n\<close> have \<open>push_bit n x OR mask n \<le> mask m\<close> by (auto simp add: le_mask_high_bits word_size bit_simps dest!: *) then have \<open>push_bit n x + mask n \<le> mask m\<close> by (simp add: disjunctive_add bit_simps) then show ?thesis by (simp add: mask_eq_exp_minus_1 push_bit_eq_mult) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x * 2 ^ n + (2 ^ n - 1) \<le> 2 ^ m - 1 proof (state)
goal (1 subgoal):
 1. x * 2 ^ n + (2 ^ n - 1) \<le> 2 ^ m - 1 proof (state)
this:
q = m - n

goal (1 subgoal):
 1. x * 2 ^ n + (2 ^ n - 1) \<le> 2 ^ m - 1 proof (chain)
picking this:
n \<le> m
q = m - n proof (prove)
using this:
n \<le> m
q = m - n

goal (1 subgoal):
 1. m = q + n proof (state)
this:
m = q + n

goal (1 subgoal):
 1. x * 2 ^ n + (2 ^ n - 1) \<le> 2 ^ m - 1 proof (chain)
picking this:
x < 2 ^ (m - n)
m = q + n proof (prove)
using this:
x < 2 ^ (m - n)
m = q + n

goal (1 subgoal):
 1. i < q proof (prove)
using this:
x < 2 ^ (m - n)
m = q + n
bit x i

goal (1 subgoal):
 1. i < q proof (state)
this:
bit x ?i \<Longrightarrow> ?i < q

goal (1 subgoal):
 1. x * 2 ^ n + (2 ^ n - 1) \<le> 2 ^ m - 1 proof (chain)
picking this:
m = q + n proof (prove)
using this:
m = q + n

goal (1 subgoal):
 1. push_bit n x OR mask n \<le> mask m proof (state)
this:
push_bit n x OR mask n \<le> mask m

goal (1 subgoal):
 1. x * 2 ^ n + (2 ^ n - 1) \<le> 2 ^ m - 1 proof (chain)
picking this:
push_bit n x OR mask n \<le> mask m proof (prove)
using this:
push_bit n x OR mask n \<le> mask m

goal (1 subgoal):
 1. push_bit n x + mask n \<le> mask m proof (state)
this:
push_bit n x + mask n \<le> mask m

goal (1 subgoal):
 1. x * 2 ^ n + (2 ^ n - 1) \<le> 2 ^ m - 1 proof (chain)
picking this:
push_bit n x + mask n \<le> mask m proof (prove)
using this:
push_bit n x + mask n \<le> mask m

goal (1 subgoal):
 1. x * 2 ^ n + (2 ^ n - 1) \<le> 2 ^ m - 1 proof (state)
this:
x * 2 ^ n + (2 ^ n - 1) \<le> 2 ^ m - 1

goal:
No subgoals!
theory Word_Lemmas

lemma shiftr_eq_neg_mask_eq:
  "a >> b = c >> b \<Longrightarrow> a AND NOT (mask b) = c AND NOT (mask b)" for a :: "'a::len word" by word_eqI (metis less_eqE)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a >> b = c >> b \<Longrightarrow> a AND NOT (mask b) = c AND NOT (mask b)
theory Word_8

lemma len8: "len_of (x :: 8 itself) = 8" by simp

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

lemma word8_and_max_simp:
  \<open>x AND 0xFF = x\<close> for x :: \<open>8 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 AND 255 = x proof (prove)
using this:
x AND mask LENGTH(8) = x

goal (1 subgoal):
 1. x AND 255 = x
theory Word_8

lemma set_enum_word8_def:
  "(set enum :: 8 word set) = {0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19,
                            20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36,
                            37, 38, 39, 40, 41, 42, 43, 44, 45, 46, 47, 48, 49, 50, 51, 52, 53,
                            54, 55, 56, 57, 58, 59, 60, 61, 62, 63, 64, 65, 66, 67, 68, 69, 70,
                            71, 72, 73, 74, 75, 76, 77, 78, 79, 80, 81, 82, 83, 84, 85, 86, 87,
                            88, 89, 90, 91, 92, 93, 94, 95, 96, 97, 98, 99, 100, 101, 102, 103,
                            104, 105, 106, 107, 108, 109, 110, 111, 112, 113, 114, 115, 116, 117,
                            118, 119, 120, 121, 122, 123, 124, 125, 126, 127, 128, 129, 130, 131,
                            132, 133, 134, 135, 136, 137, 138, 139, 140, 141, 142, 143, 144, 145,
                            146, 147, 148, 149, 150, 151, 152, 153, 154, 155, 156, 157, 158, 159,
                            160, 161, 162, 163, 164, 165, 166, 167, 168, 169, 170, 171, 172, 173,
                            174, 175, 176, 177, 178, 179, 180, 181, 182, 183, 184, 185, 186, 187,
                            188, 189, 190, 191, 192, 193, 194, 195, 196, 197, 198, 199, 200, 201,
                            202, 203, 204, 205, 206, 207, 208, 209, 210, 211, 212, 213, 214, 215,
                            216, 217, 218, 219, 220, 221, 222, 223, 224, 225, 226, 227, 228, 229,
                            230, 231, 232, 233, 234, 235, 236, 237, 238, 239, 240, 241, 242, 243,
                            244, 245, 246, 247, 248, 249, 250, 251, 252, 253, 254, 255}" by (simp add: enum_word8_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. set enum = {0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36, 37, 38, 39, 40, 41, 42, 43, 44, 45, 46, 47, 48, 49, 50, 51, 52, 53, 54, 55, 56, 57, 58, 59, 60, 61, 62, 63, 64, 65, 66, 67, 68, 69, 70, 71, 72, 73, 74, 75, 76, 77, 78, 79, 80, 81, 82, 83, 84, 85, 86, 87, 88, 89, 90, 91, 92, 93, 94, 95, 96, 97, 98, 99, 100, 101, 102, 103, 104, 105, 106, 107, 108, 109, 110, 111, 112, 113, 114, 115, 116, 117, 118, 119, 120, 121, 122, 123, 124, 125, 126, 127, 128, 129, 130, 131, 132, 133, 134, 135, 136, 137, 138, 139, 140, 141, 142, 143, 144, 145, 146, 147, 148, 149, 150, 151, 152, 153, 154, 155, 156, 157, 158, 159, 160, 161, 162, 163, 164, 165, 166, 167, 168, 169, 170, 171, 172, 173, 174, 175, 176, 177, 178, 179, 180, 181, 182, 183, 184, 185, 186, 187, 188, 189, 190, 191, 192, 193, 194, 195, 196, 197, 198, 199, 200, 201, 202, 203, 204, 205, 206, 207, 208, 209, 210, 211, 212, 213, 214, 215, 216, 217, 218, 219, 220, 221, 222, 223, 224, 225, 226, 227, 228, 229, 230, 231, 232, 233, 234, 235, 236, 237, 238, 239, 240, 241, 242, 243, 244, 245, 246, 247, 248, 249, 250, 251, 252, 253, 254, 255}