word_lib+crefine: move in word lemmas from CRefine

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

lib/Word_Lib/Word_Lemmas_Internal.thy

@@ -838,4 +838,180 @@ lemma ucast_ucast_mask_id:
    UCAST('b \<rightarrow> 'a) (UCAST('a \<rightarrow> 'b) (x && mask n)) = x && mask n" for x :: "'a::len word"
   by (simp add: ucast_ucast_len[OF eq_mask_less])
 
+lemma msb_le_mono:
+  fixes v w :: "'a::len word"
+  shows "v \<le> w \<Longrightarrow> msb v \<Longrightarrow> msb w"
+  by (simp add: msb_big)
+
+lemma neg_msb_le_mono:
+  fixes v w :: "'a::len word"
+  shows "v \<le> w \<Longrightarrow> \<not> msb w \<Longrightarrow> \<not> msb v"
+  by (simp add: msb_big)
+
+lemmas msb_less_mono = msb_le_mono[OF less_imp_le]
+lemmas neg_msb_less_mono = neg_msb_le_mono[OF less_imp_le]
+
+lemma word_sless_iff_less:
+  "\<lbrakk> \<not> msb v; \<not> msb w \<rbrakk> \<Longrightarrow> v <s w \<longleftrightarrow> v < w"
+  by (simp add: word_sless_alt sint_eq_uint word_less_alt)
+
+lemmas word_sless_imp_less = word_sless_iff_less[THEN iffD1, rotated 2]
+lemmas word_less_imp_sless = word_sless_iff_less[THEN iffD2, rotated 2]
+
+lemma to_bool_if:
+  "(if w \<noteq> 0 then 1 else 0) = (if to_bool w then 1 else 0)"
+  by (auto simp: to_bool_def)
+
+lemma word_sle_iff_le:
+  "\<lbrakk> \<not> msb v; \<not> msb w \<rbrakk> \<Longrightarrow> v <=s w \<longleftrightarrow> v \<le> w"
+  apply (simp add: word_sle_def sint_eq_uint word_le_def)
+  by (metis sint_eq_uint word_sle.rep_eq word_sle_eq)
+
+lemmas word_sle_imp_le = word_sle_iff_le[THEN iffD1, rotated 2]
+lemmas word_le_imp_sle = word_sle_iff_le[THEN iffD2, rotated 2]
+
+lemma word_upcast_shiftr:
+  assumes "LENGTH('a::len) \<le> LENGTH('b::len)"
+  shows "UCAST('a \<rightarrow> 'b) (w >> n) = UCAST('a \<rightarrow> 'b) w >> n"
+  apply (intro word_eqI impI iffI; clarsimp simp: word_size nth_shiftr nth_ucast)
+  apply (drule test_bit_size)
+  using assms by (simp add: word_size)
+
+lemma word_upcast_neg_msb:
+  "LENGTH('a::len) < LENGTH('b::len) \<Longrightarrow> \<not> msb (UCAST('a \<rightarrow> 'b) w)"
+  unfolding ucast_eq msb_word_of_int
+  by clarsimp (metis Suc_pred bit_imp_le_length lens_gt_0(2) not_less_eq)
+
+lemma word_upcast_0_sle:
+  "LENGTH('a::len) < LENGTH('b::len) \<Longrightarrow> 0 <=s UCAST('a \<rightarrow> 'b) w"
+  by (simp add: word_sle_iff_le[OF word_msb_0 word_upcast_neg_msb])
+
+lemma scast_ucast_up_eq_ucast:
+  assumes "LENGTH('a::len) < LENGTH('b::len)"
+  shows "SCAST('b \<rightarrow> 'c) (UCAST('a \<rightarrow> 'b) w) = UCAST('a \<rightarrow> 'c::len) w"
+  using assms
+  apply (subst scast_eq_ucast; simp)
+  apply (simp only: ucast_eq msb_word_of_int)
+   apply (metis bin_nth_uint_imp decr_length_less_iff numeral_nat(7) verit_comp_simplify1(3))
+  by (metis less_or_eq_imp_le ucast_nat_def unat_ucast_up_simp)
+
+lemmas not_max_word_iff_less = word_order.not_eq_extremum
+
+lemma ucast_increment:
+  assumes "w \<noteq> max_word"
+  shows "UCAST('a::len \<rightarrow> 'b::len) w + 1 = UCAST('a \<rightarrow> 'b) (w + 1)"
+  apply (cases "LENGTH('b) \<le> LENGTH('a)")
+   apply (simp add: ucast_down_add is_down)
+  apply (subgoal_tac "uint w + 1 < 2 ^ LENGTH('a)")
+   apply (subgoal_tac "uint w + 1 < 2 ^ LENGTH('b)")
+    apply (subst word_uint_eq_iff)
+    apply (simp add: uint_arith_simps uint_up_ucast is_up)
+   apply (erule less_trans, rule power_strict_increasing, simp, simp)
+  apply (subst less_diff_eq[symmetric])
+  using assms
+  apply (simp add: not_max_word_iff_less word_less_alt)
+  apply (erule less_le_trans)
+  apply simp
+  done
+
+lemma max_word_gt_0:
+  "0 < max_word"
+  by (simp add: le_neq_trans[OF max_word_max])
+
+lemma and_not_max_word:
+  "m \<noteq> max_word \<Longrightarrow> w && m \<noteq> max_word"
+  by (simp add: not_max_word_iff_less word_and_less')
+
+lemma mask_not_max_word:
+  "m < LENGTH('a::len) \<Longrightarrow> mask m \<noteq> (max_word :: 'a word)"
+  by (simp add: mask_eq_exp_minus_1)
+
+lemmas and_mask_not_max_word =
+  and_not_max_word[OF mask_not_max_word]
+
+lemma shiftr_not_max_word:
+  "0 < n \<Longrightarrow> w >> n \<noteq> max_word"
+  by (metis and_mask_eq_iff_shiftr_0 and_mask_not_max_word diff_less len_gt_0 shiftr_le_0 word_shiftr_lt)
+
+lemma word_sandwich1:
+  fixes a b c :: "'a::len word"
+  assumes "a < b"
+  assumes "b <= c"
+  shows "0 < b - a \<and> b - a <= c"
+  using assms diff_add_cancel order_less_irrefl add_0 word_le_imp_diff_le
+        word_le_less_eq word_neq_0_conv
+  by metis
+
+lemma word_sandwich2:
+  fixes a b :: "'a::len word"
+  assumes "0 < a"
+  assumes "a <= b"
+  shows "b - a < b"
+  using assms less_le_trans word_diff_less
+  by blast
+
+lemma unat_and_mask_less_2p:
+  fixes w :: "'a::len word"
+  shows "m < LENGTH('a) \<Longrightarrow> unat (w && mask m) < 2 ^ m"
+  by (simp add: unat_less_helper  and_mask_less')
+
+lemma unat_shiftr_less_2p:
+  fixes w :: "'a::len word"
+  shows "n + m = LENGTH('a) \<Longrightarrow> unat (w >> n) < 2 ^ m"
+  by (cases "n = 0"; simp add: unat_less_helper shiftr_less_t2n3)
+
+lemma nat_div_less_mono:
+  fixes m n :: nat
+  shows "m div d < n div d \<Longrightarrow> m < n"
+  by (meson div_le_mono not_less)
+
+lemma word_shiftr_less_mono:
+  fixes w :: "'a::len word"
+  shows "w >> n < v >> n \<Longrightarrow> w < v"
+  by (auto simp: word_less_nat_alt shiftr_div_2n' elim: nat_div_less_mono)
+
+lemma word_shiftr_less_mask:
+  fixes w :: "'a::len word"
+  shows "(w >> n < v >> n) \<longleftrightarrow> (w && ~~mask n < v && ~~mask n)"
+  by (metis (mono_tags) le_shiftr mask_shift shiftr_eq_neg_mask_eq word_le_less_eq word_le_not_less)
+
+lemma word_shiftr_le_mask:
+  fixes w :: "'a::len word"
+  shows "(w >> n \<le> v >> n) \<longleftrightarrow> (w && ~~mask n \<le> v && ~~mask n)"
+  by (metis (mono_tags) le_shiftr mask_shift shiftr_eq_neg_mask_eq word_le_less_eq word_le_not_less)
+
+lemma word_shiftr_eq_mask:
+  fixes w :: "'a::len word"
+  shows "(w >> n = v >> n) \<longleftrightarrow> (w && ~~mask n = v && ~~mask n)"
+  by (metis (mono_tags) mask_shift shiftr_eq_neg_mask_eq)
+
+lemmas word_shiftr_cmp_mask =
+  word_shiftr_less_mask word_shiftr_le_mask word_shiftr_eq_mask
+
+lemma if_if_if_same_output:
+  "(if c1 then if c2 then t else f else if c3 then t else f) = (if c1 \<and> c2 \<or> \<not>c1 \<and> c3 then t else f)"
+  by (simp split: if_splits)
+
+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]])
+  by (metis (no_types) Orderings.order_eq_iff and_not_eq_minus_and bit.double_compl linorder_linear
+                       neg_mask_mono_le word_and_le2 word_le_minus_cancel word_not_le
+                       word_plus_and_or_coroll2)
+
+lemma uint_minus_1_less_le_eq:
+  "0 < n \<Longrightarrow> (uint (n - 1) < m) = (uint n \<le> m)"
+  by uint_arith
+
+lemma scast_ucast_up_minus_1_ucast:
+  assumes "LENGTH('a::len) < LENGTH('b::len)"
+  assumes "0 < w"
+  shows "SCAST('b \<rightarrow> 'c) (UCAST('a \<rightarrow> 'b) w - 1) = UCAST('a \<rightarrow> 'c::len) (w - 1)"
+  using assms
+  apply (subst scast_eq_ucast; simp)
+   apply (metis gt0_iff_gem1 msb_less_mono ucast_less_ucast_weak unsigned_0 word_upcast_neg_msb)
+  by (metis less_le ucast_nat_def ucast_up_preserves_not0 unat_minus_one unat_ucast_up_simp)
+
 end

proof/crefine/Move_C.thy

@@ -143,180 +143,6 @@ lemma cteSizeBits_le_cte_level_bits[simp]:
   "cteSizeBits \<le> cte_level_bits"
   by (simp add: cte_level_bits_def cteSizeBits_def)
 
-lemma msb_le_mono:
-  fixes v w :: "'a::len word"
-  shows "v \<le> w \<Longrightarrow> msb v \<Longrightarrow> msb w"
-  by (simp add: msb_big)
-
-lemma neg_msb_le_mono:
-  fixes v w :: "'a::len word"
-  shows "v \<le> w \<Longrightarrow> \<not> msb w \<Longrightarrow> \<not> msb v"
-  by (simp add: msb_big)
-
-lemmas msb_less_mono = msb_le_mono[OF less_imp_le]
-lemmas neg_msb_less_mono = neg_msb_le_mono[OF less_imp_le]
-
-lemma word_sless_iff_less:
-  "\<lbrakk> \<not> msb v; \<not> msb w \<rbrakk> \<Longrightarrow> v <s w \<longleftrightarrow> v < w"
-  by (simp add: word_sless_alt sint_eq_uint word_less_alt)
-
-lemmas word_sless_imp_less = word_sless_iff_less[THEN iffD1, rotated 2]
-lemmas word_less_imp_sless = word_sless_iff_less[THEN iffD2, rotated 2]
-
-lemma word_sle_iff_le:
-  "\<lbrakk> \<not> msb v; \<not> msb w \<rbrakk> \<Longrightarrow> v <=s w \<longleftrightarrow> v \<le> w"
-  by (simp add: word_sle_def sint_eq_uint word_le_def)
-
-lemmas word_sle_imp_le = word_sle_iff_le[THEN iffD1, rotated 2]
-lemmas word_le_imp_sle = word_sle_iff_le[THEN iffD2, rotated 2]
-
-lemma to_bool_if:
-  "(if w \<noteq> 0 then 1 else 0) = (if to_bool w then 1 else 0)"
-  by (auto simp: to_bool_def)
-
-(* FIXME: move to Word_Lib *)
-lemma word_upcast_shiftr:
-  assumes "LENGTH('a::len) \<le> LENGTH('b::len)"
-  shows "UCAST('a \<rightarrow> 'b) (w >> n) = UCAST('a \<rightarrow> 'b) w >> n"
-  apply (intro word_eqI impI iffI; clarsimp simp: word_size nth_shiftr nth_ucast)
-  apply (drule test_bit_size)
-  using assms by (simp add: word_size)
-
-lemma word_upcast_neg_msb:
-  "LENGTH('a::len) < LENGTH('b::len) \<Longrightarrow> \<not> msb (UCAST('a \<rightarrow> 'b) w)"
-  unfolding ucast_def msb_word_of_int
-  by clarsimp (metis Suc_pred bit_imp_le_length lens_gt_0(2) not_less_eq)
-
-(* FIXME: move to Word_Lib *)
-lemma word_upcast_0_sle:
-  "LENGTH('a::len) < LENGTH('b::len) \<Longrightarrow> 0 <=s UCAST('a \<rightarrow> 'b) w"
-  by (simp add: word_sle_iff_le[OF word_msb_0 word_upcast_neg_msb])
-
-(* FIXME: move to Word_Lib *)
-lemma scast_ucast_up_eq_ucast:
-  assumes "LENGTH('a::len) < LENGTH('b::len)"
-  shows "SCAST('b \<rightarrow> 'c) (UCAST('a \<rightarrow> 'b) w) = UCAST('a \<rightarrow> 'c::len) w"
-  using assms
-  apply (subst scast_eq_ucast; simp)
-  apply (simp only: ucast_def msb_word_of_int)
-   apply (metis bin_nth_uint_imp decr_length_less_iff numeral_nat(7) verit_comp_simplify1(3))
-  by (metis less_or_eq_imp_le ucast_nat_def unat_ucast_up_simp)
-
-lemma not_max_word_iff_less:
-  "w \<noteq> max_word \<longleftrightarrow> w < max_word"
-  by (simp add: order_less_le)
-
-lemma ucast_increment:
-  assumes "w \<noteq> max_word"
-  shows "UCAST('a::len \<rightarrow> 'b::len) w + 1 = UCAST('a \<rightarrow> 'b) (w + 1)"
-  apply (cases "LENGTH('b) \<le> LENGTH('a)")
-   apply (simp add: ucast_down_add is_down)
-  apply (subgoal_tac "uint w + 1 < 2 ^ LENGTH('a)")
-   apply (subgoal_tac "uint w + 1 < 2 ^ LENGTH('b)")
-    apply (subst word_uint_eq_iff)
-    apply (simp add: uint_arith_simps uint_up_ucast is_up)
-   apply (erule less_trans, rule power_strict_increasing, simp, simp)
-  apply (subst less_diff_eq[symmetric])
-  using assms
-  apply (simp add: not_max_word_iff_less word_less_alt)
-  apply (erule less_le_trans)
-  apply simp
-  done
-
-lemma max_word_gt_0:
-  "0 < max_word"
-  by (simp add: le_neq_trans[OF max_word_max])
-
-lemma and_not_max_word:
-  "m \<noteq> max_word \<Longrightarrow> w && m \<noteq> max_word"
-  by (simp add: not_max_word_iff_less word_and_less')
-
-lemma mask_not_max_word:
-  "m < LENGTH('a::len) \<Longrightarrow> mask m \<noteq> (max_word :: 'a word)"
-  by (simp add: mask_eq_exp_minus_1)
-
-lemmas and_mask_not_max_word =
-  and_not_max_word[OF mask_not_max_word]
-
-lemma shiftr_not_max_word:
-  "0 < n \<Longrightarrow> w >> n \<noteq> max_word"
-  by (metis and_mask_eq_iff_shiftr_0 and_mask_not_max_word diff_less len_gt_0 shiftr_le_0 word_shiftr_lt)
-
-lemma word_sandwich1:
-  fixes a b c :: "'a::len word"
-  assumes "a < b"
-  assumes "b <= c"
-  shows "0 < b - a \<and> b - a <= c"
-  using assms diff_add_cancel order_less_irrefl add_0 word_le_imp_diff_le
-        word_le_less_eq word_neq_0_conv
-  by metis
-
-lemma word_sandwich2:
-  fixes a b :: "'a::len word"
-  assumes "0 < a"
-  assumes "a <= b"
-  shows "b - a < b"
-  using assms less_le_trans word_diff_less
-  by blast
-
-lemma unat_and_mask_less_2p:
-  fixes w :: "'a::len word"
-  shows "m < LENGTH('a) \<Longrightarrow> unat (w && mask m) < 2 ^ m"
-  by (simp add: unat_less_helper  and_mask_less')
-
-lemma unat_shiftr_less_2p:
-  fixes w :: "'a::len word"
-  shows "n + m = LENGTH('a) \<Longrightarrow> unat (w >> n) < 2 ^ m"
-  by (cases "n = 0"; simp add: unat_less_helper shiftr_less_t2n3)
-
-lemma nat_div_less_mono:
-  fixes m n :: nat
-  shows "m div d < n div d \<Longrightarrow> m < n"
-  by (meson div_le_mono not_less)
-
-lemma word_shiftr_less_mono:
-  fixes w :: "'a::len word"
-  shows "w >> n < v >> n \<Longrightarrow> w < v"
-  by (auto simp: word_less_nat_alt shiftr_div_2n' elim: nat_div_less_mono)
-
-lemma word_shiftr_less_mask:
-  fixes w :: "'a::len word"
-  shows "(w >> n < v >> n) \<longleftrightarrow> (w && ~~mask n < v && ~~mask n)"
-  by (metis (mono_tags) le_shiftr mask_shift shiftr_eq_neg_mask_eq word_le_less_eq word_le_not_less)
-
-lemma word_shiftr_le_mask:
-  fixes w :: "'a::len word"
-  shows "(w >> n \<le> v >> n) \<longleftrightarrow> (w && ~~mask n \<le> v && ~~mask n)"
-  by (metis (mono_tags) le_shiftr mask_shift shiftr_eq_neg_mask_eq word_le_less_eq word_le_not_less)
-
-lemma word_shiftr_eq_mask:
-  fixes w :: "'a::len word"
-  shows "(w >> n = v >> n) \<longleftrightarrow> (w && ~~mask n = v && ~~mask n)"
-  by (metis (mono_tags) mask_shift shiftr_eq_neg_mask_eq)
-
-lemmas word_shiftr_cmp_mask =
-  word_shiftr_less_mask word_shiftr_le_mask word_shiftr_eq_mask
-
-lemma if_if_if_same_output:
-  "(if c1 then if c2 then t else f else if c3 then t else f) = (if c1 \<and> c2 \<or> \<not>c1 \<and> c3 then t else f)"
-  by (simp split: if_splits)
-
-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
-
 lemma unat_ucast_prio_mask_simp[simp]:
   "unat (ucast (p::priority) && mask m :: machine_word) = unat (p && mask m)"
   by (simp add: ucast_and_mask)
@@ -325,19 +151,11 @@ lemma unat_ucast_prio_shiftr_simp[simp]:
   "unat (ucast (p::priority) >> n :: machine_word) = unat (p >> n)"
   by simp
 
-lemma from_bool_to_bool_and_1 [simp]:
-  assumes r_size: "1 < size r"
-  shows "from_bool (to_bool (r && 1)) = r && 1"
-proof -
-  from r_size have "r && 1 < 2"
-    by (simp add: and_mask_less_size [where n=1, unfolded mask_def, simplified])
-  thus ?thesis
-    by (fastforce simp add: from_bool_def to_bool_def dest: word_less_cases)
-qed
-
 lemma wb_gt_2:
   "2 < word_bits" by (simp add: word_bits_conv)
 
+declare from_bool_to_bool_and_1[simp]
+
 (* NOTE: unused. *)
 lemma inj_on_option_map:
  "inj_on (map_option f o m) (dom m) \<Longrightarrow> inj_on m (dom m)"