theory More_Word

lemma unat_ucast_no_overflow_le:
  assumes no_overflow: "unat b < (2 :: nat) ^ LENGTH('a)"
  and upward_cast: "LENGTH('a) < LENGTH('b)"
  shows "(ucast (f::'a::len word) < (b :: 'b :: len word)) = (unat f < unat b)" proof - have LR: "ucast f < b \<Longrightarrow> unat f < unat b" apply (rule unat_less_helper) apply (simp add:ucast_nat_def) apply (rule_tac 'b1 = 'b in  ucast_less_ucast[OF order.strict_implies_order, THEN iffD1]) apply (rule upward_cast) apply (simp add: ucast_ucast_mask less_mask_eq word_less_nat_alt
                     unat_power_lower[OF upward_cast] no_overflow) done have RL: "unat f < unat b \<Longrightarrow> ucast f < b" proof- assume ineq: "unat f < unat b" have "ucast (f::'a::len word) < ((ucast (ucast b ::'a::len word)) :: 'b :: len word)" apply (simp add: ucast_less_ucast[OF order.strict_implies_order] upward_cast) apply (simp only: flip: ucast_nat_def) apply (rule unat_ucast_less_no_overflow[OF no_overflow ineq]) done then show ?thesis apply (rule order_less_le_trans) apply (simp add:ucast_ucast_mask word_and_le2) done qed then show ?thesis by (simp add:RL LR iffI) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (ucast f < b) = (unat f < unat b) proof (state)
goal (1 subgoal):
 1. (ucast f < b) = (unat f < unat b) proof (prove)
goal (1 subgoal):
 1. ucast f < b \<Longrightarrow> unat f < unat b proof (prove)
goal (1 subgoal):
 1. ucast f < b \<Longrightarrow> f < word_of_nat (unat b) proof (prove)
goal (1 subgoal):
 1. ucast f < b \<Longrightarrow> f < ucast b proof (prove)
goal (2 subgoals):
 1. ucast f < b \<Longrightarrow> LENGTH('a) < LENGTH('b)
 2. ucast f < b \<Longrightarrow> ucast f < ucast (ucast b) proof (prove)
goal (1 subgoal):
 1. ucast f < b \<Longrightarrow> ucast f < ucast (ucast b) proof (prove)
goal:
No subgoals! proof (state)
this:
ucast f < b \<Longrightarrow> unat f < unat b

goal (1 subgoal):
 1. (ucast f < b) = (unat f < unat b) proof (prove)
goal (1 subgoal):
 1. unat f < unat b \<Longrightarrow> ucast f < b proof (state)
goal (1 subgoal):
 1. unat f < unat b \<Longrightarrow> ucast f < b proof (state)
this:
unat f < unat b

goal (1 subgoal):
 1. unat f < unat b \<Longrightarrow> ucast f < b proof (prove)
goal (1 subgoal):
 1. ucast f < ucast (ucast b) proof (prove)
goal (1 subgoal):
 1. f < ucast b proof (prove)
goal (1 subgoal):
 1. f < word_of_nat (unat b) proof (prove)
goal:
No subgoals! proof (state)
this:
ucast f < ucast (ucast b)

goal (1 subgoal):
 1. unat f < unat b \<Longrightarrow> ucast f < b proof (chain)
picking this:
ucast f < ucast (ucast b) proof (prove)
using this:
ucast f < ucast (ucast b)

goal (1 subgoal):
 1. ucast f < b proof (prove)
goal (1 subgoal):
 1. ucast (ucast b) \<le> b proof (prove)
goal:
No subgoals! proof (state)
this:
ucast f < b

goal:
No subgoals! proof (state)
this:
unat f < unat b \<Longrightarrow> ucast f < b

goal (1 subgoal):
 1. (ucast f < b) = (unat f < unat b) proof (chain)
picking this:
unat f < unat b \<Longrightarrow> ucast f < b proof (prove)
using this:
unat f < unat b \<Longrightarrow> ucast f < b

goal (1 subgoal):
 1. (ucast f < b) = (unat f < unat b) proof (state)
this:
(ucast f < b) = (unat f < unat b)

goal:
No subgoals!