kings-crown/FVELER_Isabelle huggingface dataset:
theory Word_32

lemma cast_chunk_assemble_id_64'[simp]:
  "(((ucast ((scast (x::64 word))::32 word))::64 word) || (((ucast ((scast (x >> 32))::32 word))::64 word) << 32)) = x" by (simp add:cast_chunk_scast_assemble_id)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. UCAST(32 \<rightarrow> 64) (SCAST(64 \<rightarrow> 32) x) || (UCAST(32 \<rightarrow> 64) (SCAST(64 \<rightarrow> 32) (x >> 32)) << 32) = x
theory Word_32

lemma cast_down_u64: "(scast::64 word \<Rightarrow> 32 word) = (ucast::64 word \<Rightarrow> 32 word)" by (subst down_cast_same[symmetric]; simp add:is_down)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. SCAST(64 \<rightarrow> 32) = UCAST(64 \<rightarrow> 32)
theory Word_32

lemma cast_down_s64: "(scast::64 sword \<Rightarrow> 32 word) = (ucast::64 sword \<Rightarrow> 32 word)" by (subst down_cast_same[symmetric]; simp add:is_down)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. SCAST(64 signed \<rightarrow> 32) = UCAST(64 signed \<rightarrow> 32)
theory Word_32

lemma word32_and_max_simp:
  \<open>x AND 0xFFFFFFFF = x\<close> for x :: \<open>32 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 && 4294967295 = x proof (prove)
using this:
x && mask LENGTH(32) = x

goal (1 subgoal):
 1. x && 4294967295 = x
theory Word_Lemmas_Internal

lemma [code]:
  \<open>Enum.enum_all P \<longleftrightarrow> list_all P enum\<close>
  \<open>Enum.enum_ex P \<longleftrightarrow> list_ex P enum\<close> for P :: \<open>'a::len word \<Rightarrow> bool\<close> by (auto simp: list_all_iff list_ex_iff)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. enum_all P = list_all P enum &&& enum_ex P = list_ex P enum
theory Word_Lemmas_Internal

lemma signed_ge_zero_scast_eq_ucast:
 "0 <=s x \<Longrightarrow> scast x = ucast x" by (simp add: scast_eq_ucast word_sle_msb_le)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 0 \<le>s x \<Longrightarrow> SCAST('a \<rightarrow> 'b) x = UCAST('a \<rightarrow> 'b) x
theory Word_Lemmas_Internal

lemma disjCI2:
  "(\<not> P \<Longrightarrow> Q) \<Longrightarrow> P \<or> Q" by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<not> P \<Longrightarrow> Q) \<Longrightarrow> P \<or> Q
theory Word_Lemmas_Internal

lemma nat_diff_diff_le_lhs:
  "a + c - b \<le> d \<Longrightarrow> a - (b - c) \<le> (d :: nat)" by arith

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a + c - b \<le> d \<Longrightarrow> a - (b - c) \<le> d
theory Word_Lemmas_Internal

lemma is_aligned_obvious_no_wrap':
  "\<lbrakk> is_aligned ptr sz; x = 2 ^ sz - 1 \<rbrakk>
   \<Longrightarrow> ptr \<le> ptr + x" by (fastforce simp: field_simps intro: is_aligned_no_overflow)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr sz; x = 2 ^ sz - 1\<rbrakk> \<Longrightarrow> ptr \<le> ptr + x
theory Word_Lemmas_Internal

lemma minus_minus_swap:
  "\<lbrakk> a \<le> c; b \<le> d; b \<le> a; d \<le> c ; (d :: nat) - b = c - a \<rbrakk>
   \<Longrightarrow> a - b = c - d" by arith

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<le> c; b \<le> d; b \<le> a; d \<le> c; d - b = c - a\<rbrakk> \<Longrightarrow> a - b = c - d
theory Word_Lemmas_Internal

lemma minus_minus_swap':
  "\<lbrakk> c \<le> a; d \<le> b; b \<le> a; d \<le> c ; (b :: nat) - d = a - c \<rbrakk>
   \<Longrightarrow> a - b = c - d" by arith

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c \<le> a; d \<le> b; b \<le> a; d \<le> c; b - d = a - c\<rbrakk> \<Longrightarrow> a - b = c - d
theory Word_Lemmas_Internal

lemma int_and_leR:
  "0 \<le> b \<Longrightarrow> a AND b \<le> (b :: int)" by (rule AND_upper2)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 0 \<le> b \<Longrightarrow> a AND b \<le> b
theory Word_Lemmas_Internal

lemma int_and_leL:
  "0 \<le> a \<Longrightarrow> a AND b \<le> (a :: int)" by (rule AND_upper1)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 0 \<le> a \<Longrightarrow> a AND b \<le> a
theory Word_Lemmas_Internal

lemma if_then_1_else_0:
  "(if P then 1 else 0) = (0 :: 'a :: zero_neq_one) \<longleftrightarrow> \<not>P" by (simp split: if_split)

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

lemma if_then_0_else_1:
  "(if P then 0 else 1) = (0 :: 'a :: zero_neq_one) \<longleftrightarrow> P" by simp

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

lemma createNewCaps_guard:
  fixes x :: "'a :: len word"
  shows "\<lbrakk> unat x = c; b < 2 ^ LENGTH('a) \<rbrakk>
         \<Longrightarrow> (n < of_nat b \<and> n < x) = (n < of_nat (min (min b c) c))" by (metis (no_types) min_less_iff_conj nat_neq_iff unat_less_helper unat_ucast_less_no_overflow
                       unsigned_less word_unat.Rep_inverse)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>unat x = c; b < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> (n < word_of_nat b \<and> n < x) = (n < word_of_nat (min (min b c) c))
theory Word_Lemmas_Internal

lemma bits_2_subtract_ineq:
  "i < (n :: ('a :: len) word)
   \<Longrightarrow> 2 ^ bits + 2 ^ bits * unat (n - (1 + i)) = unat (n - i) * 2 ^ bits" apply (simp add: unat_sub word_minus_one_le_leq) apply (subst unatSuc) apply clarsimp apply unat_arith apply (simp only: mult_Suc_right[symmetric]) apply (rule trans[OF mult.commute], rule arg_cong2[where f="(*)"], simp_all) apply (simp add: word_less_nat_alt) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. i < n \<Longrightarrow> 2 ^ bits + 2 ^ bits * unat (n - (1 + i)) = unat (n - i) * 2 ^ bits proof (prove)
goal (1 subgoal):
 1. i < n \<Longrightarrow> 2 ^ bits + 2 ^ bits * (unat n - unat (1 + i)) = (unat n - unat i) * 2 ^ bits proof (prove)
goal (2 subgoals):
 1. i < n \<Longrightarrow> 1 + i \<noteq> 0
 2. i < n \<Longrightarrow> 2 ^ bits + 2 ^ bits * (unat n - Suc (unat i)) = (unat n - unat i) * 2 ^ bits proof (prove)
goal (2 subgoals):
 1. \<lbrakk>i < n; 1 + i = 0\<rbrakk> \<Longrightarrow> False
 2. i < n \<Longrightarrow> 2 ^ bits + 2 ^ bits * (unat n - Suc (unat i)) = (unat n - unat i) * 2 ^ bits proof (prove)
goal (1 subgoal):
 1. i < n \<Longrightarrow> 2 ^ bits + 2 ^ bits * (unat n - Suc (unat i)) = (unat n - unat i) * 2 ^ bits proof (prove)
goal (1 subgoal):
 1. i < n \<Longrightarrow> 2 ^ bits * Suc (unat n - Suc (unat i)) = (unat n - unat i) * 2 ^ bits proof (prove)
goal (1 subgoal):
 1. i < n \<Longrightarrow> Suc (unat n - Suc (unat i)) = unat n - unat i proof (prove)
goal:
No subgoals!
theory Word_Lemmas_Internal

lemma unat_sub_le_strg:
  "unat v \<le> v2 \<and> x \<le> v \<and> y \<le> v \<and> y < (x :: ('a :: len) word)
    \<longrightarrow> unat (x + (- 1 - y)) \<le> v2" apply clarsimp apply (erule order_trans[rotated]) apply (fold word_le_nat_alt) apply (rule order_trans[rotated], assumption) apply (rule order_trans[rotated], rule word_sub_le[where y="y + 1"]) apply (erule Word.inc_le) apply (simp add: field_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unat v \<le> v2 \<and> x \<le> v \<and> y \<le> v \<and> y < x \<longrightarrow> unat (x + (- 1 - y)) \<le> v2 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>unat v \<le> v2; x \<le> v; y \<le> v; y < x\<rbrakk> \<Longrightarrow> unat (x + (- 1 - y)) \<le> v2 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<le> v; y \<le> v; y < x\<rbrakk> \<Longrightarrow> unat (x + (- 1 - y)) \<le> unat v proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<le> v; y \<le> v; y < x\<rbrakk> \<Longrightarrow> x + (- 1 - y) \<le> v proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<le> v; y \<le> v; y < x\<rbrakk> \<Longrightarrow> x + (- 1 - y) \<le> x proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<le> v; y \<le> v; y < x\<rbrakk> \<Longrightarrow> y + 1 \<le> x
 2. \<lbrakk>x \<le> v; y \<le> v; y < x\<rbrakk> \<Longrightarrow> x + (- 1 - y) \<le> x - (y + 1) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<le> v; y \<le> v; y < x\<rbrakk> \<Longrightarrow> x + (- 1 - y) \<le> x - (y + 1) proof (prove)
goal:
No subgoals!
theory Word_Lemmas_Internal

lemma multi_lessD:
  "\<lbrakk> (a :: nat) * b < c; 0 < a; 0 < b \<rbrakk>
   \<Longrightarrow> a < c \<and> b < c" by (cases a, simp_all,cases b,simp_all)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a * b < c; 0 < a; 0 < b\<rbrakk> \<Longrightarrow> a < c \<and> b < c
theory Word_Lemmas_Internal

lemma word_up_bound:
  "(ptr :: 'a :: len word) \<le> 2 ^ LENGTH('a) - 1 " by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ptr \<le> 2 ^ LENGTH('a) - 1
theory Word_Lemmas_Internal

lemma base_length_minus_one_inequality:
  assumes foo: "wbase \<le> 2 ^ sz - 1"
    "1 \<le> (wlength :: ('a :: len) word)"
    "wlength \<le> 2 ^ sz - wbase"
    "sz < LENGTH ('a)"
  shows "wbase \<le> wbase + wlength - 1" proof - note sz_less = power_strict_increasing[OF foo(4), where a=2] from foo have plus: "unat wbase + unat wlength < 2 ^ LENGTH('a)" apply - apply (rule order_le_less_trans[rotated], rule sz_less, simp) apply (simp add: unat_arith_simps split: if_split_asm) done from foo show ?thesis by (simp add: unat_arith_simps plus) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. wbase \<le> wbase + wlength - 1 proof (state)
goal (1 subgoal):
 1. wbase \<le> wbase + wlength - 1 proof (state)
this:
(1::?'b1) < (2::?'b1) \<Longrightarrow> (2::?'b1) ^ sz < (2::?'b1) ^ LENGTH('a)

goal (1 subgoal):
 1. wbase \<le> wbase + wlength - 1 proof (chain)
picking this:
wbase \<le> 2 ^ sz - 1
1 \<le> wlength
wlength \<le> 2 ^ sz - wbase
sz < LENGTH('a) proof (prove)
using this:
wbase \<le> 2 ^ sz - 1
1 \<le> wlength
wlength \<le> 2 ^ sz - wbase
sz < LENGTH('a)

goal (1 subgoal):
 1. unat wbase + unat wlength < 2 ^ LENGTH('a) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>wbase \<le> 2 ^ sz - 1; 1 \<le> wlength; wlength \<le> 2 ^ sz - wbase; sz < LENGTH('a)\<rbrakk> \<Longrightarrow> unat wbase + unat wlength < 2 ^ LENGTH('a) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>wbase \<le> 2 ^ sz - 1; 1 \<le> wlength; wlength \<le> 2 ^ sz - wbase; sz < LENGTH('a)\<rbrakk> \<Longrightarrow> unat wbase + unat wlength \<le> 2 ^ sz proof (prove)
goal:
No subgoals! proof (state)
this:
unat wbase + unat wlength < 2 ^ LENGTH('a)

goal (1 subgoal):
 1. wbase \<le> wbase + wlength - 1 proof (chain)
picking this:
wbase \<le> 2 ^ sz - 1
1 \<le> wlength
wlength \<le> 2 ^ sz - wbase
sz < LENGTH('a) proof (prove)
using this:
wbase \<le> 2 ^ sz - 1
1 \<le> wlength
wlength \<le> 2 ^ sz - wbase
sz < LENGTH('a)

goal (1 subgoal):
 1. wbase \<le> wbase + wlength - 1 proof (state)
this:
wbase \<le> wbase + wlength - 1

goal:
No subgoals!
theory Word_Lemmas_Internal

lemma inj_ucast:
  "\<lbrakk> uc = ucast; is_up uc \<rbrakk>
   \<Longrightarrow> inj uc" using down_ucast_inj is_up_down by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>uc = UCAST('a \<rightarrow> 'b); is_up uc\<rbrakk> \<Longrightarrow> inj uc proof (prove)
using this:
is_down UCAST(?'b \<rightarrow> ?'a) \<Longrightarrow> inj_on UCAST(?'a \<rightarrow> ?'b) ?A
is_up ?c = is_down ?d

goal (1 subgoal):
 1. \<lbrakk>uc = UCAST('a \<rightarrow> 'b); is_up uc\<rbrakk> \<Longrightarrow> inj uc
theory Word_Lemmas_Internal

lemma ucast_eq_0[OF refl]:
  "\<lbrakk> c = ucast; is_up c \<rbrakk>
   \<Longrightarrow> (c x = 0) = (x = 0)" by (metis uint_0_iff uint_up_ucast)

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

lemma uint_is_up_compose:
  fixes uc :: "'a :: len word \<Rightarrow> 'b :: len word"
    and uc' :: "'b word \<Rightarrow> 'c :: len sword"
  assumes "uc = ucast"
    and "uc' = ucast"
    and " uuc = uc' \<circ> uc"
  shows "\<lbrakk> is_up uc; is_up uc' \<rbrakk>
         \<Longrightarrow> uint (uuc b) = uint b" apply (simp add: assms) apply (frule is_up_compose) apply (simp_all ) apply (simp only: Word.uint_up_ucast) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_up uc; is_up uc'\<rbrakk> \<Longrightarrow> uint (uuc b) = uint b proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_up UCAST('a \<rightarrow> 'b); is_up UCAST('b \<rightarrow> 'c signed)\<rbrakk> \<Longrightarrow> uint (UCAST('b \<rightarrow> 'c signed) (UCAST('a \<rightarrow> 'b) b)) = uint b proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_up UCAST('a \<rightarrow> 'b); is_up UCAST('b \<rightarrow> 'c signed)\<rbrakk> \<Longrightarrow> is_up ?uc'1
 2. \<lbrakk>is_up UCAST('a \<rightarrow> 'b); is_up UCAST('b \<rightarrow> 'c signed); is_up (?uc'1 \<circ> UCAST('a \<rightarrow> 'b))\<rbrakk> \<Longrightarrow> uint (UCAST('b \<rightarrow> 'c signed) (UCAST('a \<rightarrow> 'b) b)) = uint b proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_up UCAST('a \<rightarrow> 'b); is_up UCAST('b \<rightarrow> 'c signed); is_up (UCAST('b \<rightarrow> 'c signed) \<circ> UCAST('a \<rightarrow> 'b))\<rbrakk> \<Longrightarrow> uint (UCAST('b \<rightarrow> 'c signed) (UCAST('a \<rightarrow> 'b) b)) = uint b proof (prove)
goal:
No subgoals!
theory Word_Lemmas_Internal

lemma uint_is_up_compose_pred:
  fixes uc :: "'a :: len word \<Rightarrow> 'b :: len word"
    and uc' :: "'b word \<Rightarrow> 'c :: len sword"
  assumes "uc = ucast" and "uc' = ucast" and " uuc = uc' \<circ> uc"
  shows "\<lbrakk> is_up uc; is_up uc' \<rbrakk>
         \<Longrightarrow> P (uint (uuc b)) \<longleftrightarrow> P( uint b)" apply (simp add: assms) apply (frule is_up_compose) apply (simp_all ) apply (simp only: Word.uint_up_ucast) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_up uc; is_up uc'\<rbrakk> \<Longrightarrow> P (uint (uuc b)) = P (uint b) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_up UCAST('a \<rightarrow> 'b); is_up UCAST('b \<rightarrow> 'c signed)\<rbrakk> \<Longrightarrow> P (uint (UCAST('b \<rightarrow> 'c signed) (UCAST('a \<rightarrow> 'b) b))) = P (uint b) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_up UCAST('a \<rightarrow> 'b); is_up UCAST('b \<rightarrow> 'c signed)\<rbrakk> \<Longrightarrow> is_up ?uc'1
 2. \<lbrakk>is_up UCAST('a \<rightarrow> 'b); is_up UCAST('b \<rightarrow> 'c signed); is_up (?uc'1 \<circ> UCAST('a \<rightarrow> 'b))\<rbrakk> \<Longrightarrow> P (uint (UCAST('b \<rightarrow> 'c signed) (UCAST('a \<rightarrow> 'b) b))) = P (uint b) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_up UCAST('a \<rightarrow> 'b); is_up UCAST('b \<rightarrow> 'c signed); is_up (UCAST('b \<rightarrow> 'c signed) \<circ> UCAST('a \<rightarrow> 'b))\<rbrakk> \<Longrightarrow> P (uint (UCAST('b \<rightarrow> 'c signed) (UCAST('a \<rightarrow> 'b) b))) = P (uint b) proof (prove)
goal:
No subgoals!
theory Word_Lemmas_Internal

lemma is_down_up_sword:
  fixes uc :: "'a :: len word \<Rightarrow> 'b :: len sword"
  shows "\<lbrakk> uc = ucast; LENGTH('a) < LENGTH('b) \<rbrakk>
         \<Longrightarrow> is_up uc = (\<not> is_down uc)" by (simp add: target_size source_size  is_up_def is_down_def )

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>uc = UCAST('a \<rightarrow> 'b signed); LENGTH('a) < LENGTH('b)\<rbrakk> \<Longrightarrow> is_up uc = (\<not> is_down uc)
theory Word_Lemmas_Internal

lemma is_not_down_compose:
  fixes uc :: "'a :: len word \<Rightarrow> 'b :: len word"
    and uc' :: "'b word \<Rightarrow> 'c :: len sword"
  shows "\<lbrakk> uc = ucast; uc' = ucast; LENGTH('a) < LENGTH('c) \<rbrakk>
         \<Longrightarrow> \<not> is_down (uc' \<circ> uc)" unfolding is_down_def by (simp add: Word.target_size Word.source_size)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>uc = UCAST('a \<rightarrow> 'b); uc' = UCAST('b \<rightarrow> 'c signed); LENGTH('a) < LENGTH('c)\<rbrakk> \<Longrightarrow> \<not> is_down (uc' \<circ> uc) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>uc = UCAST('a \<rightarrow> 'b); uc' = UCAST('b \<rightarrow> 'c signed); LENGTH('a) < LENGTH('c)\<rbrakk> \<Longrightarrow> \<not> map_fun (map_fun Word.Word Word.rep) id (\<lambda>_. LENGTH('c signed) \<le> LENGTH('a)) (uc' \<circ> uc)
theory Word_Lemmas_Internal

lemma sint_ucast_uint:
  fixes uc :: "'a :: len word \<Rightarrow> 'b :: len word"
    and uc' :: "'b word \<Rightarrow> 'c :: len sword"
  assumes "uc = ucast" and " uc' = ucast" and "uuc=uc' \<circ> uc "
    and "LENGTH('a) < LENGTH('c signed)"
  shows "\<lbrakk> is_up uc; is_up uc'\<rbrakk>
         \<Longrightarrow> sint (uuc b) = uint b" apply (simp add: assms) apply (frule is_up_compose') apply simp_all apply (simp add: ucast_ucast_b) apply (rule sint_ucast_eq_uint) apply (insert assms) apply (simp add: is_down_def target_size source_size) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_up uc; is_up uc'\<rbrakk> \<Longrightarrow> sint (uuc b) = uint b proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_up UCAST('a \<rightarrow> 'b); is_up UCAST('b \<rightarrow> 'c signed)\<rbrakk> \<Longrightarrow> sint (UCAST('b \<rightarrow> 'c signed) (UCAST('a \<rightarrow> 'b) b)) = uint b proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_up UCAST('a \<rightarrow> 'b); is_up UCAST('b \<rightarrow> 'c signed)\<rbrakk> \<Longrightarrow> is_up ?uc'1
 2. \<lbrakk>is_up UCAST('a \<rightarrow> 'b); is_up UCAST('b \<rightarrow> 'c signed); is_up (?uc'1 \<circ> UCAST('a \<rightarrow> 'b))\<rbrakk> \<Longrightarrow> sint (UCAST('b \<rightarrow> 'c signed) (UCAST('a \<rightarrow> 'b) b)) = uint b proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_up UCAST('a \<rightarrow> 'b); is_up UCAST('b \<rightarrow> 'c signed); is_up (UCAST('b \<rightarrow> 'c signed) \<circ> UCAST('a \<rightarrow> 'b))\<rbrakk> \<Longrightarrow> sint (UCAST('b \<rightarrow> 'c signed) (UCAST('a \<rightarrow> 'b) b)) = uint b proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_up UCAST('a \<rightarrow> 'b); is_up UCAST('b \<rightarrow> 'c signed); is_up (UCAST('b \<rightarrow> 'c signed) \<circ> UCAST('a \<rightarrow> 'b))\<rbrakk> \<Longrightarrow> sint (UCAST('a \<rightarrow> 'c signed) b) = uint b proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_up UCAST('a \<rightarrow> 'b); is_up UCAST('b \<rightarrow> 'c signed); is_up (UCAST('b \<rightarrow> 'c signed) \<circ> UCAST('a \<rightarrow> 'b))\<rbrakk> \<Longrightarrow> \<not> is_down UCAST('a \<rightarrow> 'c signed) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_up UCAST('a \<rightarrow> 'b); is_up UCAST('b \<rightarrow> 'c signed); is_up (UCAST('b \<rightarrow> 'c signed) \<circ> UCAST('a \<rightarrow> 'b)); uc = UCAST('a \<rightarrow> 'b); uc' = UCAST('b \<rightarrow> 'c signed); uuc = uc' \<circ> uc; LENGTH('a) < LENGTH('c signed)\<rbrakk> \<Longrightarrow> \<not> is_down UCAST('a \<rightarrow> 'c signed) proof (prove)
goal:
No subgoals!
theory Word_Lemmas_Internal

lemma sint_ucast_uint_pred:
  fixes uc :: "'a :: len word \<Rightarrow> 'b :: len word"
    and uc' :: "'b word \<Rightarrow> 'c :: len sword"
    and uuc :: "'a word \<Rightarrow> 'c sword"
  assumes "uc = ucast" and " uc' = ucast" and "uuc=uc' \<circ> uc "
    and "LENGTH('a) < LENGTH('c )"
  shows "\<lbrakk> is_up uc; is_up uc' \<rbrakk>
         \<Longrightarrow> P (uint b) \<longleftrightarrow> P (sint (uuc b))" apply (simp add: assms ) apply (insert sint_ucast_uint[where uc=uc and uc'=uc' and uuc=uuc and b = b]) apply (simp add: assms) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_up uc; is_up uc'\<rbrakk> \<Longrightarrow> P (uint b) = P (sint (uuc b)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_up UCAST('a \<rightarrow> 'b); is_up UCAST('b \<rightarrow> 'c signed)\<rbrakk> \<Longrightarrow> P (uint b) = P (sint (UCAST('b \<rightarrow> 'c signed) (UCAST('a \<rightarrow> 'b) b))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_up UCAST('a \<rightarrow> 'b); is_up UCAST('b \<rightarrow> 'c signed); \<lbrakk>uc = UCAST('a \<rightarrow> 'b); uc' = UCAST('b \<rightarrow> 'c signed); uuc = uc' \<circ> uc; LENGTH('a) < LENGTH('c signed); is_up uc; is_up uc'\<rbrakk> \<Longrightarrow> sint (uuc b) = uint b\<rbrakk> \<Longrightarrow> P (uint b) = P (sint (UCAST('b \<rightarrow> 'c signed) (UCAST('a \<rightarrow> 'b) b))) proof (prove)
goal:
No subgoals!
theory Word_Lemmas_Internal

lemma sint_uucast_uint_uucast_pred:
  fixes uc :: "'a :: len word \<Rightarrow> 'b :: len word"
    and uc' :: "'b word \<Rightarrow> 'c :: len sword"
  assumes "uc = ucast" and " uc' = ucast" and "uuc=uc' \<circ> uc "
    and "LENGTH('a) < LENGTH('c )"
  shows "\<lbrakk> is_up uc; is_up uc' \<rbrakk>
         \<Longrightarrow> P (uint(uuc b)) \<longleftrightarrow> P (sint (uuc b))" apply (simp add: assms ) apply (insert sint_ucast_uint[where uc=uc and uc'=uc' and uuc=uuc and b = b]) apply (insert uint_is_up_compose_pred[where uc=uc and uc'=uc' and uuc=uuc and b=b]) apply (simp add: assms uint_is_up_compose_pred) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_up uc; is_up uc'\<rbrakk> \<Longrightarrow> P (uint (uuc b)) = P (sint (uuc b)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_up UCAST('a \<rightarrow> 'b); is_up UCAST('b \<rightarrow> 'c signed)\<rbrakk> \<Longrightarrow> P (uint (UCAST('b \<rightarrow> 'c signed) (UCAST('a \<rightarrow> 'b) b))) = P (sint (UCAST('b \<rightarrow> 'c signed) (UCAST('a \<rightarrow> 'b) b))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_up UCAST('a \<rightarrow> 'b); is_up UCAST('b \<rightarrow> 'c signed); \<lbrakk>uc = UCAST('a \<rightarrow> 'b); uc' = UCAST('b \<rightarrow> 'c signed); uuc = uc' \<circ> uc; LENGTH('a) < LENGTH('c signed); is_up uc; is_up uc'\<rbrakk> \<Longrightarrow> sint (uuc b) = uint b\<rbrakk> \<Longrightarrow> P (uint (UCAST('b \<rightarrow> 'c signed) (UCAST('a \<rightarrow> 'b) b))) = P (sint (UCAST('b \<rightarrow> 'c signed) (UCAST('a \<rightarrow> 'b) b))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_up UCAST('a \<rightarrow> 'b); is_up UCAST('b \<rightarrow> 'c signed); \<lbrakk>uc = UCAST('a \<rightarrow> 'b); uc' = UCAST('b \<rightarrow> 'c signed); uuc = uc' \<circ> uc; LENGTH('a) < LENGTH('c signed); is_up uc; is_up uc'\<rbrakk> \<Longrightarrow> sint (uuc b) = uint b; \<And>P. \<lbrakk>uc = UCAST('a \<rightarrow> 'b); uc' = UCAST('b \<rightarrow> 'c signed); uuc = uc' \<circ> uc; is_up uc; is_up uc'\<rbrakk> \<Longrightarrow> P (uint (uuc b)) = P (uint b)\<rbrakk> \<Longrightarrow> P (uint (UCAST('b \<rightarrow> 'c signed) (UCAST('a \<rightarrow> 'b) b))) = P (sint (UCAST('b \<rightarrow> 'c signed) (UCAST('a \<rightarrow> 'b) b))) proof (prove)
goal:
No subgoals!
theory Word_Lemmas_Internal

lemma unat_minus':
  fixes x :: "'a :: len word"
  shows "x \<noteq> 0 \<Longrightarrow> unat (-x) = 2 ^ LENGTH('a) - unat x" by (simp add: unat_minus wsst_TYs(3))

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> unat (- x) = 2 ^ LENGTH('a) - unat x
theory Word_Lemmas_Internal

lemma word_nth_neq:
  "n < LENGTH('a) \<Longrightarrow> (~~ x :: 'a :: len word) !! n = (\<not> x !! n)" by (simp add: word_size word_ops_nth_size)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n < LENGTH('a) \<Longrightarrow> (~~ x) !! n = (\<not> x !! n)