theory Move_C

lemma word_le_split_mask:
  "(w \<le> v) \<longleftrightarrow> (w >> n < v >> n \<or> w >> n = v >> n \<and> w && mask n \<le> v && mask n)" apply (simp add: word_shiftr_eq_mask word_shiftr_less_mask) apply (rule subst[where P="\<lambda>c. c \<le> d = e" for d e, OF AND_NOT_mask_plus_AND_mask_eq[where n=n]]) apply (rule subst[where P="\<lambda>c. d \<le> c = e" for d e, OF AND_NOT_mask_plus_AND_mask_eq[where n=n]]) apply (rule iffI) apply safe apply (fold_subgoals (prefix))[2] apply (subst atomize_conj) apply (rule context_conjI) apply (metis AND_NOT_mask_plus_AND_mask_eq neg_mask_mono_le word_le_less_eq) apply (metis add.commute word_and_le1 word_bw_comms(1) word_plus_and_or_coroll2 word_plus_mcs_4) apply (metis Groups.add_ac(2) neg_mask_mono_le word_le_less_eq word_not_le word_plus_and_or_coroll2) apply (metis add.commute word_and_le1 word_bw_comms(1) word_plus_and_or_coroll2 word_plus_mcs_3) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (w \<le> v) = (w >> n < v >> n \<or> w >> n = v >> n \<and> w && mask n \<le> v && mask n) proof (prove)
goal (1 subgoal):
 1. (w \<le> v) = (w && ~~ mask n < v && ~~ mask n \<or> w && ~~ mask n = v && ~~ mask n \<and> w && mask n \<le> v && mask n) proof (prove)
goal (1 subgoal):
 1. ((w && ~~ mask n) + (w && mask n) \<le> v) = (w && ~~ mask n < v && ~~ mask n \<or> w && ~~ mask n = v && ~~ mask n \<and> w && mask n \<le> v && mask n) proof (prove)
goal (1 subgoal):
 1. ((w && ~~ mask n) + (w && mask n) \<le> (v && ~~ mask n) + (v && mask n)) = (w && ~~ mask n < v && ~~ mask n \<or> w && ~~ mask n = v && ~~ mask n \<and> w && mask n \<le> v && mask n) proof (prove)
goal (2 subgoals):
 1. (w && ~~ mask n) + (w && mask n) \<le> (v && ~~ mask n) + (v && mask n) \<Longrightarrow> w && ~~ mask n < v && ~~ mask n \<or> w && ~~ mask n = v && ~~ mask n \<and> w && mask n \<le> v && mask n
 2. w && ~~ mask n < v && ~~ mask n \<or> w && ~~ mask n = v && ~~ mask n \<and> w && mask n \<le> v && mask n \<Longrightarrow> (w && ~~ mask n) + (w && mask n) \<le> (v && ~~ mask n) + (v && mask n) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>(w && ~~ mask n) + (w && mask n) \<le> (v && ~~ mask n) + (v && mask n); \<not> w && ~~ mask n < v && ~~ mask n\<rbrakk> \<Longrightarrow> w && ~~ mask n = v && ~~ mask n
 2. \<lbrakk>(w && ~~ mask n) + (w && mask n) \<le> (v && ~~ mask n) + (v && mask n); \<not> w && ~~ mask n < v && ~~ mask n\<rbrakk> \<Longrightarrow> w && mask n \<le> v && mask n
 3. w && ~~ mask n < v && ~~ mask n \<Longrightarrow> (w && ~~ mask n) + (w && mask n) \<le> (v && ~~ mask n) + (v && mask n)
 4. \<lbrakk>w && ~~ mask n = v && ~~ mask n; w && mask n \<le> v && mask n\<rbrakk> \<Longrightarrow> (w && ~~ mask n) + (w && mask n) \<le> (v && ~~ mask n) + (v && mask n) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>(w && ~~ mask n) + (w && mask n) \<le> (v && ~~ mask n) + (v && mask n); \<not> w && ~~ mask n < v && ~~ mask n\<rbrakk> \<Longrightarrow> w && ~~ mask n = v && ~~ mask n &&& w && mask n \<le> v && mask n
 2. w && ~~ mask n < v && ~~ mask n \<Longrightarrow> (w && ~~ mask n) + (w && mask n) \<le> (v && ~~ mask n) + (v && mask n)
 3. \<lbrakk>w && ~~ mask n = v && ~~ mask n; w && mask n \<le> v && mask n\<rbrakk> \<Longrightarrow> (w && ~~ mask n) + (w && mask n) \<le> (v && ~~ mask n) + (v && mask n) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>(w && ~~ mask n) + (w && mask n) \<le> (v && ~~ mask n) + (v && mask n); \<not> w && ~~ mask n < v && ~~ mask n\<rbrakk> \<Longrightarrow> w && ~~ mask n = v && ~~ mask n \<and> w && mask n \<le> v && mask n
 2. w && ~~ mask n < v && ~~ mask n \<Longrightarrow> (w && ~~ mask n) + (w && mask n) \<le> (v && ~~ mask n) + (v && mask n)
 3. \<lbrakk>w && ~~ mask n = v && ~~ mask n; w && mask n \<le> v && mask n\<rbrakk> \<Longrightarrow> (w && ~~ mask n) + (w && mask n) \<le> (v && ~~ mask n) + (v && mask n) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>(w && ~~ mask n) + (w && mask n) \<le> (v && ~~ mask n) + (v && mask n); \<not> w && ~~ mask n < v && ~~ mask n\<rbrakk> \<Longrightarrow> w && ~~ mask n = v && ~~ mask n
 2. \<lbrakk>(w && ~~ mask n) + (w && mask n) \<le> (v && ~~ mask n) + (v && mask n); \<not> w && ~~ mask n < v && ~~ mask n; w && ~~ mask n = v && ~~ mask n\<rbrakk> \<Longrightarrow> w && mask n \<le> v && mask n
 3. w && ~~ mask n < v && ~~ mask n \<Longrightarrow> (w && ~~ mask n) + (w && mask n) \<le> (v && ~~ mask n) + (v && mask n)
 4. \<lbrakk>w && ~~ mask n = v && ~~ mask n; w && mask n \<le> v && mask n\<rbrakk> \<Longrightarrow> (w && ~~ mask n) + (w && mask n) \<le> (v && ~~ mask n) + (v && mask n) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>(w && ~~ mask n) + (w && mask n) \<le> (v && ~~ mask n) + (v && mask n); \<not> w && ~~ mask n < v && ~~ mask n; w && ~~ mask n = v && ~~ mask n\<rbrakk> \<Longrightarrow> w && mask n \<le> v && mask n
 2. w && ~~ mask n < v && ~~ mask n \<Longrightarrow> (w && ~~ mask n) + (w && mask n) \<le> (v && ~~ mask n) + (v && mask n)
 3. \<lbrakk>w && ~~ mask n = v && ~~ mask n; w && mask n \<le> v && mask n\<rbrakk> \<Longrightarrow> (w && ~~ mask n) + (w && mask n) \<le> (v && ~~ mask n) + (v && mask n) proof (prove)
goal (2 subgoals):
 1. w && ~~ mask n < v && ~~ mask n \<Longrightarrow> (w && ~~ mask n) + (w && mask n) \<le> (v && ~~ mask n) + (v && mask n)
 2. \<lbrakk>w && ~~ mask n = v && ~~ mask n; w && mask n \<le> v && mask n\<rbrakk> \<Longrightarrow> (w && ~~ mask n) + (w && mask n) \<le> (v && ~~ mask n) + (v && mask n) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>w && ~~ mask n = v && ~~ mask n; w && mask n \<le> v && mask n\<rbrakk> \<Longrightarrow> (w && ~~ mask n) + (w && mask n) \<le> (v && ~~ mask n) + (v && mask n) proof (prove)
goal:
No subgoals!