theory Word_Lemmas

lemma scast_ucast_high_bits:
  \<open>scast (ucast w :: 'b::len word) = w
     \<longleftrightarrow> (\<forall> i \<in> {LENGTH('b) ..< size w}. bit w i = bit w (LENGTH('b) - 1))\<close> proof (cases \<open>LENGTH('a) \<le> LENGTH('b)\<close>) case True moreover define m where \<open>m = LENGTH('b) - LENGTH('a)\<close> ultimately have \<open>LENGTH('b) = m + LENGTH('a)\<close> by simp then show ?thesis by (simp add: signed_ucast_eq word_size) word_eqI next case False define q where \<open>q = LENGTH('b) - 1\<close> then have \<open>LENGTH('b) = Suc q\<close> by simp moreover define m where \<open>m = Suc LENGTH('a) - LENGTH('b)\<close> with False \<open>LENGTH('b) = Suc q\<close> have \<open>LENGTH('a) = m + q\<close> by (simp add: not_le) ultimately show ?thesis apply (simp add: signed_ucast_eq word_size) apply (transfer fixing: m q) apply (simp add: signed_take_bit_take_bit) apply (rule impI) apply (subst bit_eq_iff) apply (simp add: bit_take_bit_iff bit_signed_take_bit_iff min_def) by (auto simp add: Suc_le_eq) (meson dual_order.strict_iff_not)+ qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (SCAST('b \<rightarrow> 'a) (UCAST('a \<rightarrow> 'b) w) = w) = (\<forall>i\<in>{LENGTH('b)..<size w}. bit w i = bit w (LENGTH('b) - 1)) proof (state)
goal (2 subgoals):
 1. LENGTH('a) \<le> LENGTH('b) \<Longrightarrow> (SCAST('b \<rightarrow> 'a) (UCAST('a \<rightarrow> 'b) w) = w) = (\<forall>i\<in>{LENGTH('b)..<size w}. bit w i = bit w (LENGTH('b) - 1))
 2. \<not> LENGTH('a) \<le> LENGTH('b) \<Longrightarrow> (SCAST('b \<rightarrow> 'a) (UCAST('a \<rightarrow> 'b) w) = w) = (\<forall>i\<in>{LENGTH('b)..<size w}. bit w i = bit w (LENGTH('b) - 1)) proof (state)
this:
LENGTH('a) \<le> LENGTH('b)

goal (2 subgoals):
 1. LENGTH('a) \<le> LENGTH('b) \<Longrightarrow> (SCAST('b \<rightarrow> 'a) (UCAST('a \<rightarrow> 'b) w) = w) = (\<forall>i\<in>{LENGTH('b)..<size w}. bit w i = bit w (LENGTH('b) - 1))
 2. \<not> LENGTH('a) \<le> LENGTH('b) \<Longrightarrow> (SCAST('b \<rightarrow> 'a) (UCAST('a \<rightarrow> 'b) w) = w) = (\<forall>i\<in>{LENGTH('b)..<size w}. bit w i = bit w (LENGTH('b) - 1)) proof (state)
this:
LENGTH('a) \<le> LENGTH('b)

goal (2 subgoals):
 1. LENGTH('a) \<le> LENGTH('b) \<Longrightarrow> (SCAST('b \<rightarrow> 'a) (UCAST('a \<rightarrow> 'b) w) = w) = (\<forall>i\<in>{LENGTH('b)..<size w}. bit w i = bit w (LENGTH('b) - 1))
 2. \<not> LENGTH('a) \<le> LENGTH('b) \<Longrightarrow> (SCAST('b \<rightarrow> 'a) (UCAST('a \<rightarrow> 'b) w) = w) = (\<forall>i\<in>{LENGTH('b)..<size w}. bit w i = bit w (LENGTH('b) - 1)) proof (state)
this:
m = LENGTH('b) - LENGTH('a)

goal (2 subgoals):
 1. LENGTH('a) \<le> LENGTH('b) \<Longrightarrow> (SCAST('b \<rightarrow> 'a) (UCAST('a \<rightarrow> 'b) w) = w) = (\<forall>i\<in>{LENGTH('b)..<size w}. bit w i = bit w (LENGTH('b) - 1))
 2. \<not> LENGTH('a) \<le> LENGTH('b) \<Longrightarrow> (SCAST('b \<rightarrow> 'a) (UCAST('a \<rightarrow> 'b) w) = w) = (\<forall>i\<in>{LENGTH('b)..<size w}. bit w i = bit w (LENGTH('b) - 1)) proof (chain)
picking this:
LENGTH('a) \<le> LENGTH('b)
m = LENGTH('b) - LENGTH('a) proof (prove)
using this:
LENGTH('a) \<le> LENGTH('b)
m = LENGTH('b) - LENGTH('a)

goal (1 subgoal):
 1. LENGTH('b) = m + LENGTH('a) proof (state)
this:
LENGTH('b) = m + LENGTH('a)

goal (2 subgoals):
 1. LENGTH('a) \<le> LENGTH('b) \<Longrightarrow> (SCAST('b \<rightarrow> 'a) (UCAST('a \<rightarrow> 'b) w) = w) = (\<forall>i\<in>{LENGTH('b)..<size w}. bit w i = bit w (LENGTH('b) - 1))
 2. \<not> LENGTH('a) \<le> LENGTH('b) \<Longrightarrow> (SCAST('b \<rightarrow> 'a) (UCAST('a \<rightarrow> 'b) w) = w) = (\<forall>i\<in>{LENGTH('b)..<size w}. bit w i = bit w (LENGTH('b) - 1)) proof (chain)
picking this:
LENGTH('b) = m + LENGTH('a) proof (prove)
using this:
LENGTH('b) = m + LENGTH('a)

goal (1 subgoal):
 1. (SCAST('b \<rightarrow> 'a) (UCAST('a \<rightarrow> 'b) w) = w) = (\<forall>i\<in>{LENGTH('b)..<size w}. bit w i = bit w (LENGTH('b) - 1)) proof (state)
this:
(SCAST('b \<rightarrow> 'a) (UCAST('a \<rightarrow> 'b) w) = w) = (\<forall>i\<in>{LENGTH('b)..<size w}. bit w i = bit w (LENGTH('b) - 1))

goal (1 subgoal):
 1. \<not> LENGTH('a) \<le> LENGTH('b) \<Longrightarrow> (SCAST('b \<rightarrow> 'a) (UCAST('a \<rightarrow> 'b) w) = w) = (\<forall>i\<in>{LENGTH('b)..<size w}. bit w i = bit w (LENGTH('b) - 1)) proof (state)
goal (1 subgoal):
 1. \<not> LENGTH('a) \<le> LENGTH('b) \<Longrightarrow> (SCAST('b \<rightarrow> 'a) (UCAST('a \<rightarrow> 'b) w) = w) = (\<forall>i\<in>{LENGTH('b)..<size w}. bit w i = bit w (LENGTH('b) - 1)) proof (state)
this:
\<not> LENGTH('a) \<le> LENGTH('b)

goal (1 subgoal):
 1. \<not> LENGTH('a) \<le> LENGTH('b) \<Longrightarrow> (SCAST('b \<rightarrow> 'a) (UCAST('a \<rightarrow> 'b) w) = w) = (\<forall>i\<in>{LENGTH('b)..<size w}. bit w i = bit w (LENGTH('b) - 1)) proof (state)
this:
q = LENGTH('b) - 1

goal (1 subgoal):
 1. \<not> LENGTH('a) \<le> LENGTH('b) \<Longrightarrow> (SCAST('b \<rightarrow> 'a) (UCAST('a \<rightarrow> 'b) w) = w) = (\<forall>i\<in>{LENGTH('b)..<size w}. bit w i = bit w (LENGTH('b) - 1)) proof (chain)
picking this:
q = LENGTH('b) - 1 proof (prove)
using this:
q = LENGTH('b) - 1

goal (1 subgoal):
 1. LENGTH('b) = Suc q proof (state)
this:
LENGTH('b) = Suc q

goal (1 subgoal):
 1. \<not> LENGTH('a) \<le> LENGTH('b) \<Longrightarrow> (SCAST('b \<rightarrow> 'a) (UCAST('a \<rightarrow> 'b) w) = w) = (\<forall>i\<in>{LENGTH('b)..<size w}. bit w i = bit w (LENGTH('b) - 1)) proof (state)
this:
LENGTH('b) = Suc q

goal (1 subgoal):
 1. \<not> LENGTH('a) \<le> LENGTH('b) \<Longrightarrow> (SCAST('b \<rightarrow> 'a) (UCAST('a \<rightarrow> 'b) w) = w) = (\<forall>i\<in>{LENGTH('b)..<size w}. bit w i = bit w (LENGTH('b) - 1)) proof (state)
this:
m = Suc LENGTH('a) - LENGTH('b)

goal (1 subgoal):
 1. \<not> LENGTH('a) \<le> LENGTH('b) \<Longrightarrow> (SCAST('b \<rightarrow> 'a) (UCAST('a \<rightarrow> 'b) w) = w) = (\<forall>i\<in>{LENGTH('b)..<size w}. bit w i = bit w (LENGTH('b) - 1)) proof (chain)
picking this:
\<not> LENGTH('a) \<le> LENGTH('b)
LENGTH('b) = Suc q
m = Suc LENGTH('a) - LENGTH('b) proof (prove)
using this:
\<not> LENGTH('a) \<le> LENGTH('b)
LENGTH('b) = Suc q
m = Suc LENGTH('a) - LENGTH('b)

goal (1 subgoal):
 1. LENGTH('a) = m + q proof (state)
this:
LENGTH('a) = m + q

goal (1 subgoal):
 1. \<not> LENGTH('a) \<le> LENGTH('b) \<Longrightarrow> (SCAST('b \<rightarrow> 'a) (UCAST('a \<rightarrow> 'b) w) = w) = (\<forall>i\<in>{LENGTH('b)..<size w}. bit w i = bit w (LENGTH('b) - 1)) proof (chain)
picking this:
LENGTH('b) = Suc q
LENGTH('a) = m + q proof (prove)
using this:
LENGTH('b) = Suc q
LENGTH('a) = m + q

goal (1 subgoal):
 1. (SCAST('b \<rightarrow> 'a) (UCAST('a \<rightarrow> 'b) w) = w) = (\<forall>i\<in>{LENGTH('b)..<size w}. bit w i = bit w (LENGTH('b) - 1)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>LENGTH('b) = Suc q; LENGTH('a) = m + q\<rbrakk> \<Longrightarrow> (signed_take_bit q w = w) = (\<forall>i\<in>{Suc q..<m + q}. bit w i = bit w q) proof (prove)
goal (1 subgoal):
 1. \<And>w. \<lbrakk>LENGTH('b) = Suc q; LENGTH('a) = m + q\<rbrakk> \<Longrightarrow> (take_bit LENGTH('a) (signed_take_bit q (take_bit LENGTH('a) w)) = take_bit LENGTH('a) w) = (\<forall>i\<in>{Suc q..<m + q}. (i < LENGTH('a) \<and> bit w i) = (q < LENGTH('a) \<and> bit w q)) proof (prove)
goal (1 subgoal):
 1. \<And>w. \<lbrakk>LENGTH('b) = Suc q; LENGTH('a) = m + q\<rbrakk> \<Longrightarrow> 0 < m \<longrightarrow> (take_bit (m + q) (signed_take_bit q w) = take_bit (m + q) w) = (\<forall>i\<in>{Suc q..<m + q}. bit w i = bit w q) proof (prove)
goal (1 subgoal):
 1. \<And>w. \<lbrakk>LENGTH('b) = Suc q; LENGTH('a) = m + q; 0 < m\<rbrakk> \<Longrightarrow> (take_bit (m + q) (signed_take_bit q w) = take_bit (m + q) w) = (\<forall>i\<in>{Suc q..<m + q}. bit w i = bit w q) proof (prove)
goal (1 subgoal):
 1. \<And>w. \<lbrakk>LENGTH('b) = Suc q; LENGTH('a) = m + q; 0 < m\<rbrakk> \<Longrightarrow> (\<forall>n. possible_bit TYPE(int) n \<longrightarrow> bit (take_bit (m + q) (signed_take_bit q w)) n = bit (take_bit (m + q) w) n) = (\<forall>i\<in>{Suc q..<m + q}. bit w i = bit w q) proof (prove)
goal (1 subgoal):
 1. \<And>w. \<lbrakk>LENGTH('b) = Suc q; LENGTH('a) = m + q; 0 < m\<rbrakk> \<Longrightarrow> (\<forall>n\<ge>q. (n < m + q \<and> bit w q) = (n < m + q \<and> bit w n)) = (\<forall>i\<in>{Suc q..<m + q}. bit w i = bit w q) proof (state)
this:
(SCAST('b \<rightarrow> 'a) (UCAST('a \<rightarrow> 'b) w) = w) = (\<forall>i\<in>{LENGTH('b)..<size w}. bit w i = bit w (LENGTH('b) - 1))

goal:
No subgoals!