theory Word_Lemmas

lemma ucast_le_ucast_eq:
  fixes x y :: "'a::len word"
  assumes x: "x < 2 ^ n"
  assumes y: "y < 2 ^ n"
  assumes n: "n = LENGTH('b::len)"
  shows "(UCAST('a \<rightarrow> 'b) x \<le> UCAST('a \<rightarrow> 'b) y) = (x \<le> y)" apply (rule iffI) apply (cases "LENGTH('b) < LENGTH('a)") apply (subst less_mask_eq[OF x, symmetric]) apply (subst less_mask_eq[OF y, symmetric]) apply (unfold n) apply (subst ucast_ucast_mask[symmetric])+ apply (simp add: ucast_le_ucast)+ apply (erule ucast_mono_le[OF _ y[unfolded n]]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (UCAST('a \<rightarrow> 'b) x \<le> UCAST('a \<rightarrow> 'b) y) = (x \<le> y) proof (prove)
goal (2 subgoals):
 1. UCAST('a \<rightarrow> 'b) x \<le> UCAST('a \<rightarrow> 'b) y \<Longrightarrow> x \<le> y
 2. x \<le> y \<Longrightarrow> UCAST('a \<rightarrow> 'b) x \<le> UCAST('a \<rightarrow> 'b) y proof (prove)
goal (3 subgoals):
 1. \<lbrakk>UCAST('a \<rightarrow> 'b) x \<le> UCAST('a \<rightarrow> 'b) y; LENGTH('b) < LENGTH('a)\<rbrakk> \<Longrightarrow> x \<le> y
 2. \<lbrakk>UCAST('a \<rightarrow> 'b) x \<le> UCAST('a \<rightarrow> 'b) y; \<not> LENGTH('b) < LENGTH('a)\<rbrakk> \<Longrightarrow> x \<le> y
 3. x \<le> y \<Longrightarrow> UCAST('a \<rightarrow> 'b) x \<le> UCAST('a \<rightarrow> 'b) y proof (prove)
goal (3 subgoals):
 1. \<lbrakk>UCAST('a \<rightarrow> 'b) x \<le> UCAST('a \<rightarrow> 'b) y; LENGTH('b) < LENGTH('a)\<rbrakk> \<Longrightarrow> x AND mask n \<le> y
 2. \<lbrakk>UCAST('a \<rightarrow> 'b) x \<le> UCAST('a \<rightarrow> 'b) y; \<not> LENGTH('b) < LENGTH('a)\<rbrakk> \<Longrightarrow> x \<le> y
 3. x \<le> y \<Longrightarrow> UCAST('a \<rightarrow> 'b) x \<le> UCAST('a \<rightarrow> 'b) y proof (prove)
goal (3 subgoals):
 1. \<lbrakk>UCAST('a \<rightarrow> 'b) x \<le> UCAST('a \<rightarrow> 'b) y; LENGTH('b) < LENGTH('a)\<rbrakk> \<Longrightarrow> x AND mask n \<le> y AND mask n
 2. \<lbrakk>UCAST('a \<rightarrow> 'b) x \<le> UCAST('a \<rightarrow> 'b) y; \<not> LENGTH('b) < LENGTH('a)\<rbrakk> \<Longrightarrow> x \<le> y
 3. x \<le> y \<Longrightarrow> UCAST('a \<rightarrow> 'b) x \<le> UCAST('a \<rightarrow> 'b) y proof (prove)
goal (3 subgoals):
 1. \<lbrakk>UCAST('a \<rightarrow> 'b) x \<le> UCAST('a \<rightarrow> 'b) y; LENGTH('b) < LENGTH('a)\<rbrakk> \<Longrightarrow> x AND mask LENGTH('b) \<le> y AND mask LENGTH('b)
 2. \<lbrakk>UCAST('a \<rightarrow> 'b) x \<le> UCAST('a \<rightarrow> 'b) y; \<not> LENGTH('b) < LENGTH('a)\<rbrakk> \<Longrightarrow> x \<le> y
 3. x \<le> y \<Longrightarrow> UCAST('a \<rightarrow> 'b) x \<le> UCAST('a \<rightarrow> 'b) y proof (prove)
goal (3 subgoals):
 1. \<lbrakk>UCAST('a \<rightarrow> 'b) x \<le> UCAST('a \<rightarrow> 'b) y; LENGTH('b) < LENGTH('a)\<rbrakk> \<Longrightarrow> UCAST('b \<rightarrow> 'a) (UCAST('a \<rightarrow> 'b) x) \<le> UCAST('b \<rightarrow> 'a) (UCAST('a \<rightarrow> 'b) y)
 2. \<lbrakk>UCAST('a \<rightarrow> 'b) x \<le> UCAST('a \<rightarrow> 'b) y; \<not> LENGTH('b) < LENGTH('a)\<rbrakk> \<Longrightarrow> x \<le> y
 3. x \<le> y \<Longrightarrow> UCAST('a \<rightarrow> 'b) x \<le> UCAST('a \<rightarrow> 'b) y proof (prove)
goal (1 subgoal):
 1. x \<le> y \<Longrightarrow> UCAST('a \<rightarrow> 'b) x \<le> UCAST('a \<rightarrow> 'b) y proof (prove)
goal:
No subgoals!