From 0486d6165a999e874f9e7af5a4c879c9610a6b25 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Wed, 8 May 2024 11:44:06 -0400 Subject: [PATCH] word_lib+crefine: move in word lemmas from CRefine Signed-off-by: Gerwin Klein --- lib/Word_Lib/Word_Lemmas_Internal.thy | 176 ++++++++++++++++++++++++ proof/crefine/Move_C.thy | 186 +------------------------- 2 files changed, 178 insertions(+), 184 deletions(-) diff --git a/lib/Word_Lib/Word_Lemmas_Internal.thy b/lib/Word_Lib/Word_Lemmas_Internal.thy index 73159d12cf..909316b470 100644 --- a/lib/Word_Lib/Word_Lemmas_Internal.thy +++ b/lib/Word_Lib/Word_Lemmas_Internal.thy @@ -838,4 +838,180 @@ lemma ucast_ucast_mask_id: UCAST('b \ 'a) (UCAST('a \ '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 \ w \ msb v \ msb w" + by (simp add: msb_big) + +lemma neg_msb_le_mono: + fixes v w :: "'a::len word" + shows "v \ w \ \ msb w \ \ 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: + "\ \ msb v; \ msb w \ \ v 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 \ 0 then 1 else 0) = (if to_bool w then 1 else 0)" + by (auto simp: to_bool_def) + +lemma word_sle_iff_le: + "\ \ msb v; \ msb w \ \ v <=s w \ v \ 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) \ LENGTH('b::len)" + shows "UCAST('a \ 'b) (w >> n) = UCAST('a \ '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) \ \ msb (UCAST('a \ '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) \ 0 <=s UCAST('a \ '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 \ 'c) (UCAST('a \ 'b) w) = UCAST('a \ '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 \ max_word" + shows "UCAST('a::len \ 'b::len) w + 1 = UCAST('a \ 'b) (w + 1)" + apply (cases "LENGTH('b) \ 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 \ max_word \ w && m \ max_word" + by (simp add: not_max_word_iff_less word_and_less') + +lemma mask_not_max_word: + "m < LENGTH('a::len) \ mask m \ (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 \ w >> n \ 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 \ 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) \ 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) \ 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 \ m < n" + by (meson div_le_mono not_less) + +lemma word_shiftr_less_mono: + fixes w :: "'a::len word" + shows "w >> n < v >> n \ 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) \ (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 \ v >> n) \ (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_eq_mask: + fixes w :: "'a::len word" + shows "(w >> n = v >> n) \ (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 \ c2 \ \c1 \ c3 then t else f)" + by (simp split: if_splits) + +lemma word_le_split_mask: + "(w \ v) \ (w >> n < v >> n \ w >> n = v >> n \ w && mask n \ v && mask n)" + apply (simp add: word_shiftr_eq_mask word_shiftr_less_mask) + apply (rule subst[where P="\c. c \ d = e" for d e, OF AND_NOT_mask_plus_AND_mask_eq[where n=n]]) + apply (rule subst[where P="\c. d \ 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 \ (uint (n - 1) < m) = (uint n \ m)" + by uint_arith + +lemma scast_ucast_up_minus_1_ucast: + assumes "LENGTH('a::len) < LENGTH('b::len)" + assumes "0 < w" + shows "SCAST('b \ 'c) (UCAST('a \ 'b) w - 1) = UCAST('a \ '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 diff --git a/proof/crefine/Move_C.thy b/proof/crefine/Move_C.thy index e0e8dae8cc..853a2cebe8 100644 --- a/proof/crefine/Move_C.thy +++ b/proof/crefine/Move_C.thy @@ -143,180 +143,6 @@ lemma cteSizeBits_le_cte_level_bits[simp]: "cteSizeBits \ cte_level_bits" by (simp add: cte_level_bits_def cteSizeBits_def) -lemma msb_le_mono: - fixes v w :: "'a::len word" - shows "v \ w \ msb v \ msb w" - by (simp add: msb_big) - -lemma neg_msb_le_mono: - fixes v w :: "'a::len word" - shows "v \ w \ \ msb w \ \ 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: - "\ \ msb v; \ msb w \ \ v 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: - "\ \ msb v; \ msb w \ \ v <=s w \ v \ 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 \ 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) \ LENGTH('b::len)" - shows "UCAST('a \ 'b) (w >> n) = UCAST('a \ '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) \ \ msb (UCAST('a \ '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) \ 0 <=s UCAST('a \ '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 \ 'c) (UCAST('a \ 'b) w) = UCAST('a \ '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 \ max_word \ w < max_word" - by (simp add: order_less_le) - -lemma ucast_increment: - assumes "w \ max_word" - shows "UCAST('a::len \ 'b::len) w + 1 = UCAST('a \ 'b) (w + 1)" - apply (cases "LENGTH('b) \ 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 \ max_word \ w && m \ max_word" - by (simp add: not_max_word_iff_less word_and_less') - -lemma mask_not_max_word: - "m < LENGTH('a::len) \ mask m \ (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 \ w >> n \ 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 \ 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) \ 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) \ 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 \ m < n" - by (meson div_le_mono not_less) - -lemma word_shiftr_less_mono: - fixes w :: "'a::len word" - shows "w >> n < v >> n \ 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) \ (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 \ v >> n) \ (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_eq_mask: - fixes w :: "'a::len word" - shows "(w >> n = v >> n) \ (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 \ c2 \ \c1 \ c3 then t else f)" - by (simp split: if_splits) - -lemma word_le_split_mask: - "(w \ v) \ (w >> n < v >> n \ w >> n = v >> n \ w && mask n \ v && mask n)" - apply (simp add: word_shiftr_eq_mask word_shiftr_less_mask) - apply (rule subst[where P="\c. c \ d = e" for d e, OF AND_NOT_mask_plus_AND_mask_eq[where n=n]]) - apply (rule subst[where P="\c. d \ 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) \ inj_on m (dom m)"