diff --git a/lib/HaskellLemmaBucket.thy b/lib/HaskellLemmaBucket.thy index cbba0983f..62000f21d 100644 --- a/lib/HaskellLemmaBucket.thy +++ b/lib/HaskellLemmaBucket.thy @@ -314,6 +314,7 @@ This is proven for all n < len_of TYPE ('a), which is different to running word_bitwise and expanding into an explicit list of bits. \ +(* FIXME: replace with the version in Word_Lemmas *) lemmas word_eqI_solve_simps = word_and_le1 word_or_zero le_word_or2 shiftL_nat word_FF_is_mask word_1FF_is_mask neg_mask_bang nth_ucast linorder_not_less word_size minus_one_norm word_ops_nth_size diff --git a/lib/Word_Lib/Word_Lemmas.thy b/lib/Word_Lib/Word_Lemmas.thy index 18759dcd5..fd1e1bc86 100644 --- a/lib/Word_Lib/Word_Lemmas.thy +++ b/lib/Word_Lib/Word_Lemmas.thy @@ -508,22 +508,13 @@ lemma upto_enum_word: done lemma word_upto_Cons_eq: - "\x = z; x < y; Suc (unat y) < 2 ^ LENGTH('a)\ - \ [x::'a::len word .e. y] = z # [x + 1 .e. y]" + "x < y \ [x::'a::len word .e. y] = x # [x + 1 .e. y]" apply (subst upto_enum_red) - apply (subst upt_conv_Cons) - apply (simp) - apply (drule unat_mono) - apply arith - apply (simp only: list.map) - apply (subst list.inject) - apply rule - apply (rule to_from_enum) - apply (subst upto_enum_red) - apply (rule map_cong [OF _ refl]) - apply (rule arg_cong2 [where f = "\x y. [x ..< y]"]) - apply unat_arith - apply simp + apply (subst upt_conv_Cons, unat_arith) + apply (simp only: list.map list.inject upto_enum_red to_from_enum simp_thms) + apply (rule map_cong[OF _ refl]) + apply (rule arg_cong2[where f = "\x y. [x ..< y]"], unat_arith) + apply (rule refl) done lemma distinct_enum_upto: @@ -1308,6 +1299,13 @@ lemma word_less_power_trans2: shows "\n < 2 ^ (m - k); k \ m; m < LENGTH('a)\ \ n * 2 ^ k < 2 ^ m" by (subst field_simps, rule word_less_power_trans) +(* shadows the slightly weaker Word.nth_ucast *) +lemma nth_ucast: + "(ucast (w::'a::len0 word)::'b::len0 word) !! n = + (w !! n \ n < min (len_of TYPE('a)) (len_of TYPE('b)))" + by (simp add: ucast_def test_bit_bin word_ubin.eq_norm nth_bintr word_size) + (fast elim!: bin_nth_uint_imp) + lemma ucast_less: "LENGTH('b) < LENGTH('a) \ (ucast (x :: 'b :: len word) :: ('a :: len word)) < 2 ^ LENGTH('b)" @@ -1315,8 +1313,6 @@ lemma ucast_less: apply (simp add: word_size) apply (rule word_eqI) apply (simp add: word_size nth_ucast) - apply safe - apply (simp add: test_bit.Rep[simplified]) done lemma ucast_range_less: @@ -3636,7 +3632,7 @@ lemma sint_ucast_eq_uint: \ sint ((ucast :: ('a::len word \ 'b::len word)) x) = uint x" apply (subst sint_eq_uint) apply (clarsimp simp: msb_nth nth_ucast is_down) - apply (metis Suc_leI Suc_pred bang_conj_lt len_gt_0) + apply (metis Suc_leI Suc_pred len_gt_0) apply (clarsimp simp: uint_up_ucast is_up is_down) done @@ -5217,8 +5213,6 @@ lemma ucast_mask_drop: "LENGTH('a :: len) \ n \ (ucast (x && mask n) :: 'a word) = ucast x" apply (rule word_eqI) apply (simp add: nth_ucast word_size) - apply safe - apply (simp add: test_bit_bl word_size) done lemma alignUp_distance: @@ -5748,4 +5742,302 @@ lemma word_aligned_add_no_wrap_bounded: "\ w + 2^n \ x; w + 2^n \ 0; is_aligned w n \ \ (w::'a::len word) < x" by (blast dest: is_aligned_no_overflow le_less_trans minus_one_helper) +lemma mask_Suc: + "mask (Suc n) = 2^n + mask n" + by (simp add: mask_def) + +lemma is_aligned_no_overflow_mask: + "is_aligned x n \ x \ x + mask n" + by (simp add: mask_def) (erule is_aligned_no_overflow') + +lemma is_aligned_mask_offset_unat: + fixes off :: "('a::len) word" + and x :: "'a word" + assumes al: "is_aligned x sz" + and offv: "off \ mask sz" + shows "unat x + unat off < 2 ^ LENGTH('a)" +proof cases + assume szv: "sz < LENGTH('a)" + from al obtain k where xv: "x = 2 ^ sz * (of_nat k)" + and kl: "k < 2 ^ (LENGTH('a) - sz)" + by (auto elim: is_alignedE) + + from offv szv have offv': "unat off < 2 ^ sz" + apply (simp add: unat_mask word_le_nat_alt) + apply (erule order_le_less_trans) + apply simp + done + + show ?thesis using szv + apply (subst xv) + apply (subst unat_mult_power_lem[OF kl]) + apply (subst mult.commute, rule nat_add_offset_less) + apply (rule less_le_trans[OF offv'], simp) + apply (rule kl) + apply simp + done +next + assume "\ sz < LENGTH('a)" + with al have "x = 0" + apply (simp add: is_aligned_nth not_less) + apply (rule word_eqI, clarsimp simp: word_size) + done + thus ?thesis by simp +qed + +lemma of_bl_max: + "(of_bl xs :: 'a::len word) \ mask (length xs)" + apply (induct xs) + apply simp + apply (simp add: of_bl_Cons mask_Suc) + apply (rule conjI; clarsimp) + apply (erule word_plus_mono_right) + apply (rule is_aligned_no_overflow_mask) + apply (rule is_aligned_triv) + apply (simp add: word_le_nat_alt) + apply (subst unat_add_lem') + apply (rule is_aligned_mask_offset_unat) + apply (rule is_aligned_triv) + apply (simp add: mask_def) + apply simp + done + +lemma mask_over_length: + "LENGTH('a) \ n \ mask n = (-1::'a::len word)" + by (simp add: mask_def) + +lemma is_aligned_over_length: + "\ is_aligned p n; LENGTH('a) \ n \ \ (p::'a::len word) = 0" + by (simp add: is_aligned_mask mask_over_length) + +lemma Suc_2p_unat_mask: + "n < LENGTH('a) \ Suc (2 ^ n * k + unat (mask n :: 'a::len word)) = 2 ^ n * (k+1)" + by (simp add: unat_mask) + +lemma is_aligned_add_step_le: + "\ is_aligned (a::'a::len word) n; is_aligned b n; a < b; b \ a + mask n \ \ False" + apply (simp flip: not_le) + apply (erule notE) + apply (cases "LENGTH('a) \ n") + apply (drule (1) is_aligned_over_length)+ + apply (drule mask_over_length) + apply clarsimp + apply (clarsimp simp: word_le_nat_alt not_less) + apply (subst (asm) unat_plus_simple[THEN iffD1], erule is_aligned_no_overflow_mask) + apply (clarsimp simp: is_aligned_def dvd_def word_le_nat_alt) + apply (drule le_imp_less_Suc) + apply (simp add: Suc_2p_unat_mask) + by (metis Groups.mult_ac(2) Suc_leI linorder_not_less mult_le_mono order_refl times_nat.simps(2)) + +lemma power_2_mult_step_le: + "\n' \ n; 2 ^ n' * k' < 2 ^ n * k\ \ 2 ^ n' * (k' + 1) \ 2 ^ n * (k::nat)" + apply (cases "n'=n", simp) + apply (metis Suc_leI le_refl mult_Suc_right mult_le_mono semiring_normalization_rules(7)) + apply (drule (1) le_neq_trans) + apply clarsimp + apply (subgoal_tac "\m. n = n' + m") + prefer 2 + apply (simp add: le_Suc_ex) + apply (clarsimp simp: power_add) + by (metis Suc_leI mult.assoc mult_Suc_right nat_mult_le_cancel_disj) + +lemma aligned_mask_step: + "\ n' \ n; p' \ p + mask n; is_aligned p n; is_aligned p' n' \ \ + (p'::'a::len word) + mask n' \ p + mask n" + apply (cases "LENGTH('a) \ n") + apply (frule (1) is_aligned_over_length) + apply (drule mask_over_length) + apply clarsimp + apply (simp add: not_le) + apply (simp add: word_le_nat_alt unat_plus_simple) + apply (subst unat_plus_simple[THEN iffD1], erule is_aligned_no_overflow_mask)+ + apply (subst (asm) unat_plus_simple[THEN iffD1], erule is_aligned_no_overflow_mask) + apply (clarsimp simp: is_aligned_def dvd_def) + apply (rename_tac k k') + apply (thin_tac "unat p = x" for p x)+ + apply (subst Suc_le_mono[symmetric]) + apply (simp only: Suc_2p_unat_mask) + apply (drule le_imp_less_Suc, subst (asm) Suc_2p_unat_mask, assumption) + apply (erule (1) power_2_mult_step_le) + done + +lemma mask_mono: + "sz' \ sz \ mask sz' \ (mask sz :: 'a::len word)" + apply (cases "sz < LENGTH('a)") + apply (simp only: mask_def shiftl_1) + apply (rule word_le_minus_mono_left) + apply (erule (1) two_power_increasing) + apply (rule word_1_le_power) + apply simp + apply (simp add: not_less mask_over_length) + done + +lemma aligned_mask_disjoint: + "\ is_aligned (a :: 'a :: len word) n; b \ mask n \ \ a && b = 0" + apply (rule word_eqI) + apply (clarsimp simp: is_aligned_nth word_size mask_def simp del: word_less_sub_le) + apply (frule le2p_bits_unset) + apply (case_tac "na < n") + apply simp + apply simp + done + +lemma word_and_or_mask_aligned: + "\ is_aligned a n; b \ mask n \ \ a + b = a || b" + apply (rule word_plus_and_or_coroll) + apply (erule (1) aligned_mask_disjoint) + done + +lemmas word_and_or_mask_aligned2 = + word_and_or_mask_aligned[where a=b and b=a for a b, + simplified add.commute word_bool_alg.disj.commute] + +named_theorems word_eqI_simps + +lemmas [word_eqI_simps] = + word_ops_nth_size + word_size + word_or_zero + neg_mask_bang + nth_ucast + is_aligned_nth + nth_w2p nth_shiftl + nth_shiftr + less_2p_is_upper_bits_unset + le_mask_high_bits + neg_mask_le_high_bits + bang_eq + +lemma is_aligned_ucastI: + "is_aligned w n \ is_aligned (ucast w) n" + by (clarsimp simp: word_eqI_simps) + +lemma ucast_le_maskI: + "a \ mask n \ UCAST('a::len \ 'b::len) a \ mask n" + apply (clarsimp simp: word_eqI_simps) + done + +lemma ucast_add_mask_aligned: + "\ a \ mask n; is_aligned b n \ \ UCAST ('a::len \ 'b::len) (a + b) = ucast a + ucast b" + apply (simp add: word_and_or_mask_aligned2) + apply (subst word_and_or_mask_aligned2, erule is_aligned_ucastI, erule ucast_le_maskI) + apply (rule word_eqI) + apply (fastforce simp: word_eqI_simps) + done + +lemma ucast_shiftl: + "LENGTH('b) \ LENGTH ('a) \ UCAST ('a::len \ 'b::len) x << n = ucast (x << n)" + by (rule word_eqI) (fastforce simp: word_eqI_simps) + +lemma ucast_leq_mask: + "LENGTH('a) \ n \ ucast (x::'a::len0 word) \ mask n" + by (clarsimp simp: le_mask_high_bits word_size nth_ucast) + +lemma shiftl_inj: + "\ x << n = y << n; x \ mask (LENGTH('a)-n); y \ mask (LENGTH('a)-n) \ \ + x = (y :: 'a :: len word)" + apply (rule word_eqI) + apply (clarsimp simp: word_eqI_simps) + apply (rename_tac n') + apply (case_tac "LENGTH('a) - n \ n'", simp) + apply (simp add: not_le) + apply (erule_tac x="n'+n" in allE) + apply (subgoal_tac "n' + n < LENGTH('a)", simp) + apply arith + done + +lemma distinct_word_add_ucast_shift_inj: + "\ p + (UCAST('a::len \ 'b::len) off << n) = p' + (ucast off' << n); + is_aligned p n'; is_aligned p' n'; n' = n + LENGTH('a); n' < LENGTH('b) \ + \ p' = p \ off' = off" + apply (simp add: word_and_or_mask_aligned le_mask_shiftl_le_mask[where n="LENGTH('a)"] + ucast_leq_mask) + apply (simp add: is_aligned_nth) + apply (rule conjI) + apply (rule word_eqI, clarsimp simp: word_eqI_simps) + apply (metis add_le_cancel_left diff_add_inverse le_Suc_ex nat_less_le) + apply (rule word_eqI, clarsimp simp: word_eqI_simps) + apply (rename_tac i) + apply (erule_tac x="i+n" in allE) + apply simp + done + +lemma aligned_add_mask_lessD: + "\ x + mask n < y; is_aligned x n \ \ x < y" for y::"'a::len word" + by (metis is_aligned_no_overflow' mask_2pm1 order_le_less_trans) + +lemma aligned_add_mask_less_eq: + "\ is_aligned x n; is_aligned y n; n < LENGTH('a) \ \ (x + mask n < y) = (x < y)" + for y::"'a::len word" + apply (rule iffI, erule (1) aligned_add_mask_lessD) + apply (drule (3) gap_between_aligned) + apply (simp add: mask_def) + done + +lemma word_upto_Nil: + "y < x \ [x .e. y ::'a::len word] = []" + by (simp add: upto_enum_red not_le word_less_nat_alt) + +lemma word_enum_decomp_elem: + assumes "[x .e. (y ::'a::len word)] = as @ a # bs" + shows "x \ a \ a \ y" +proof - + have "set as \ set [x .e. y] \ a \ set [x .e. y]" + using assms by (auto dest: arg_cong[where f=set]) + then show ?thesis by auto +qed + +lemma max_word_not_less[simp]: + "\ max_word < x" + by (simp add: not_less) + +lemma word_enum_prefix: + "[x .e. (y ::'a::len word)] = as @ a # bs \ as = (if x < a then [x .e. a - 1] else [])" + apply (induct as arbitrary: x; clarsimp) + apply (case_tac "x < y") + prefer 2 + apply (case_tac "x = y", simp) + apply (simp add: not_less) + apply (drule (1) dual_order.not_eq_order_implies_strict) + apply (simp add: word_upto_Nil) + apply (simp add: word_upto_Cons_eq) + apply (case_tac "x < y") + prefer 2 + apply (case_tac "x = y", simp) + apply (simp add: not_less) + apply (drule (1) dual_order.not_eq_order_implies_strict) + apply (simp add: word_upto_Nil) + apply (clarsimp simp: word_upto_Cons_eq) + apply (frule word_enum_decomp_elem) + apply clarsimp + apply (rule conjI) + prefer 2 + apply (subst word_Suc_le[symmetric]; clarsimp) + apply (drule meta_spec) + apply (drule (1) meta_mp) + apply clarsimp + apply (rule conjI; clarsimp) + apply (subst (2) word_upto_Cons_eq) + apply unat_arith + apply simp + done + +lemma word_enum_decomp_set: + "[x .e. (y ::'a::len word)] = as @ a # bs \ a \ set as" + apply (subst word_enum_prefix, assumption) + apply (cases "x < a"; clarsimp) + apply unat_arith + done + +lemma word_enum_decomp: + assumes "[x .e. (y ::'a::len word)] = as @ a # bs" + shows "x \ a \ a \ y \ a \ set as \ (\z \ set as. x \ z \ z \ y)" +proof - + from assms + have "set as \ set [x .e. y] \ a \ set [x .e. y]" + by (auto dest: arg_cong[where f=set]) + with word_enum_decomp_set[OF assms] + show ?thesis by auto +qed + end diff --git a/lib/Word_Lib/Word_Lemmas_Internal.thy b/lib/Word_Lib/Word_Lemmas_Internal.thy index 476343d7e..007ddf2b7 100644 --- a/lib/Word_Lib/Word_Lemmas_Internal.thy +++ b/lib/Word_Lib/Word_Lemmas_Internal.thy @@ -1619,6 +1619,54 @@ lemma scast_ucast_mask_compare: apply (rename_tac i j; case_tac "i = len_of TYPE('b) - 1"; case_tac "j = len_of TYPE('b) - 1") by auto -end +lemma ucast_less_shiftl_helper': + "\ len_of TYPE('b) + (a::nat) < len_of TYPE('a); 2 ^ (len_of TYPE('b) + a) \ n\ + \ (ucast (x :: 'b::len word) << a) < (n :: 'a::len word)" + apply (erule order_less_le_trans[rotated]) + using ucast_less[where x=x and 'a='a] + apply (simp only: shiftl_t2n field_simps) + apply (rule word_less_power_trans2; simp) + done + +end + +lemma of_bl_mult_and_not_mask_eq: + "\is_aligned (a :: 'a::len word) n; length b + m \ n\ + \ a + of_bl b * (2^m) && ~~ mask n = a" + apply (simp add: shiftl_t2n[simplified mult.commute, symmetric]) + apply (simp add: mask_out_add_aligned[where q="of_bl b << m", symmetric]) + apply (case_tac "n < size a") + prefer 2 + apply (simp add: not_less power_overflow mask_def word_size) + apply (simp add: mask_eq_x_eq_0[symmetric] word_size) + apply (rule less_mask_eq) + apply (rule shiftl_less_t2n, simp_all) + apply (cut_tac 'a='a and xs=b in of_bl_length, simp) + apply (drule nat_move_sub_le) + apply (drule two_power_increasing[where 'a='a], simp) + apply (drule (2) less_le_trans) + done + +lemma bin_to_bl_of_bl_eq: + "\is_aligned (a::'a::len word) n; length b + c \ n; length b + c < LENGTH('a)\ + \ bin_to_bl (length b) (uint ((a + of_bl b * 2^c) >> c)) = b" + apply (subst word_plus_and_or_coroll) + apply (erule is_aligned_get_word_bits) + apply (rule is_aligned_AND_less_0) + apply (simp add: is_aligned_mask) + apply (rule order_less_le_trans) + apply (rule of_bl_length2) + apply simp + apply (simp add: two_power_increasing) + apply simp + apply (rule nth_equalityI) + apply (simp only: len_bin_to_bl) + apply (clarsimp simp only: len_bin_to_bl nth_bin_to_bl word_test_bit_def[symmetric]) + apply (simp add: nth_shiftr nth_shiftl + shiftl_t2n[where n=c, simplified mult.commute, simplified, symmetric]) + apply (simp add: is_aligned_nth[THEN iffD1, rule_format] test_bit_of_bl nth_rev) + apply (case_tac "b ! i", simp_all) + apply arith + done end diff --git a/proof/crefine/X64/Arch_C.thy b/proof/crefine/X64/Arch_C.thy index 180519fca..f8119c473 100644 --- a/proof/crefine/X64/Arch_C.thy +++ b/proof/crefine/X64/Arch_C.thy @@ -4904,17 +4904,19 @@ lemma word_minus_1_shiftr: apply fastforce done +(* FIXME: move to Word *) lemma ucast_shiftr: "UCAST('a::len \ 'b::len) w >> n = UCAST('a \ 'b) ((w && mask LENGTH('b)) >> n)" apply (rule word_eqI[rule_format]; rule iffI; clarsimp simp: nth_ucast nth_shiftr word_size) - apply (drule test_bit_size; simp add: word_size) done +(* FIXME: move to Word *) lemma mask_eq_ucast_shiftr: assumes mask: "w && mask LENGTH('b) = w" shows "UCAST('a::len \ 'b::len) w >> n = UCAST('a \ 'b) (w >> n)" by (rule ucast_shiftr[where 'a='a and 'b='b, of w n, simplified mask]) +(* FIXME: move to Word *) lemma mask_eq_ucast_shiftl: assumes "w && mask (LENGTH('a) - n) = w" shows "UCAST('a::len \ 'b::len) w << n = UCAST('a \ 'b) (w << n)" @@ -4924,11 +4926,13 @@ lemma mask_eq_ucast_shiftl: drule test_bit_size; simp add: word_size) done +(* FIXME: replace by mask_mono *) lemma mask_le_mono: "m \ n \ mask m \ mask n" apply (subst and_mask_eq_iff_le_mask[symmetric]) by (auto intro: word_eqI simp: word_size) +(* FIXME: move to Word *) lemma word_and_mask_eq_le_mono: "w && mask m = w \ m \ n \ w && mask n = w" apply (simp add: and_mask_eq_iff_le_mask) diff --git a/proof/invariant-abstract/ARM/ArchVSpace_AI.thy b/proof/invariant-abstract/ARM/ArchVSpace_AI.thy index a9b2f169a..48c9ecef0 100644 --- a/proof/invariant-abstract/ARM/ArchVSpace_AI.thy +++ b/proof/invariant-abstract/ARM/ArchVSpace_AI.thy @@ -702,9 +702,6 @@ lemma ex_asid_high_bits_plus: prefer 2 apply fastforce apply (clarsimp simp: linorder_not_less) - apply (rule conjI) - prefer 2 - apply arith apply (subgoal_tac "n < 17", simp) apply (clarsimp simp add: linorder_not_le [symmetric]) done @@ -720,9 +717,6 @@ lemma asid_high_bits_shl: apply (rule context_conjI) apply (clarsimp simp add: linorder_not_less [symmetric]) apply simp - apply (rule conjI) - prefer 2 - apply simp apply (subgoal_tac "n < 17", simp) apply (clarsimp simp add: linorder_not_le [symmetric]) done diff --git a/proof/invariant-abstract/ARM_HYP/ArchVSpace_AI.thy b/proof/invariant-abstract/ARM_HYP/ArchVSpace_AI.thy index 72fe2788a..dc495ab22 100644 --- a/proof/invariant-abstract/ARM_HYP/ArchVSpace_AI.thy +++ b/proof/invariant-abstract/ARM_HYP/ArchVSpace_AI.thy @@ -798,9 +798,6 @@ lemma ex_asid_high_bits_plus: prefer 2 apply fastforce apply (clarsimp simp: linorder_not_less) - apply (rule conjI) - prefer 2 - apply arith apply (subgoal_tac "n < 17", simp) apply (clarsimp simp add: linorder_not_le [symmetric]) done @@ -816,9 +813,6 @@ lemma asid_high_bits_shl: apply (rule context_conjI) apply (clarsimp simp add: linorder_not_less [symmetric]) apply simp - apply (rule conjI) - prefer 2 - apply simp apply (subgoal_tac "n < 17", simp) apply (clarsimp simp add: linorder_not_le [symmetric]) done diff --git a/proof/invariant-abstract/RISCV64/ArchAcc_AI.thy b/proof/invariant-abstract/RISCV64/ArchAcc_AI.thy index dde54223b..08e7656cd 100644 --- a/proof/invariant-abstract/RISCV64/ArchAcc_AI.thy +++ b/proof/invariant-abstract/RISCV64/ArchAcc_AI.thy @@ -16,32 +16,6 @@ theory ArchAcc_AI imports "../SubMonad_AI" "Lib.Crunch_Instances_NonDet" begin -(* FIXME: move to Word and replace nth_ucast, possibly breaks things.. *) -lemma nth_ucast': - "(ucast (w::'a::len0 word)::'b::len0 word) !! n = - (w !! n \ n < min (len_of TYPE('a)) (len_of TYPE('b)))" - by (simp add: ucast_def test_bit_bin word_ubin.eq_norm nth_bintr word_size) - (fast elim!: bin_nth_uint_imp) - -(* FIXME: move to Word *) -lemma ucast_leq_mask: - "LENGTH('a) \ n \ ucast (x::'a::len0 word) \ mask n" - by (clarsimp simp: le_mask_high_bits word_size nth_ucast') - -(* FIXME: move to Word *) -lemma shiftl_inj: - "\ x << n = y << n; x \ mask (LENGTH('a)-n); y \ mask (LENGTH('a)-n) \ \ - x = (y :: 'a :: len word)" - apply (rule word_eqI) - apply (clarsimp simp: bang_eq le_mask_high_bits word_eqI_solve_simps) - apply (rename_tac n') - apply (case_tac "LENGTH('a) - n \ n'", simp) - apply (simp add: not_le) - apply (erule_tac x="n'+n" in allE) - apply (subgoal_tac "n' + n < LENGTH('a)", simp) - apply arith - done - context non_vspace_op begin diff --git a/proof/invariant-abstract/RISCV64/ArchArch_AI.thy b/proof/invariant-abstract/RISCV64/ArchArch_AI.thy index 138237d44..4b271bc46 100644 --- a/proof/invariant-abstract/RISCV64/ArchArch_AI.thy +++ b/proof/invariant-abstract/RISCV64/ArchArch_AI.thy @@ -12,19 +12,6 @@ theory ArchArch_AI imports "../Arch_AI" begin -(* FIXME: move to Word *) -lemma aligned_add_mask_lessD: - "\ x + mask n < y; is_aligned x n \ \ x < (y::'a::len word)" - by (metis is_aligned_no_overflow' mask_2pm1 order_le_less_trans) - -(* FIXME: move to Word *) -lemma aligned_add_mask_less_eq: - "\ is_aligned x n; is_aligned y n; n < LENGTH('a) \ \ (x + mask n < y) = (x < (y::'a::len word))" - apply (rule iffI, erule (1) aligned_add_mask_lessD) - apply (drule (3) gap_between_aligned) - apply (simp add: mask_def) - done - context Arch begin global_naming RISCV64 definition diff --git a/proof/invariant-abstract/RISCV64/ArchVSpace_AI.thy b/proof/invariant-abstract/RISCV64/ArchVSpace_AI.thy index e9f896522..54ba50849 100644 --- a/proof/invariant-abstract/RISCV64/ArchVSpace_AI.thy +++ b/proof/invariant-abstract/RISCV64/ArchVSpace_AI.thy @@ -16,89 +16,6 @@ theory ArchVSpace_AI imports "../VSpacePre_AI" begin -(* FIXME: move to Word, replace word_upto_Cons_eq *) -lemma word_upto_Cons: - "x < y \ [x::'a::len word .e. y] = x # [x + 1 .e. y]" - apply (subst upto_enum_red) - apply (subst upt_conv_Cons, unat_arith) - apply (simp only: list.map list.inject upto_enum_red to_from_enum simp_thms) - apply (rule map_cong[OF _ refl]) - apply (rule arg_cong2[where f = "\x y. [x ..< y]"], unat_arith) - apply (rule refl) - done - -(* FIXME: move to Word *) -lemma word_upto_Nil: - "y < x \ [x .e. y ::'a::len word] = []" - by (simp add: upto_enum_red not_le word_less_nat_alt) - -(* FIXME: move to Word *) -lemma word_enum_decomp_elem: - assumes "[x .e. (y ::'a::len word)] = as @ a # bs" - shows "x \ a \ a \ y" -proof - - have "set as \ set [x .e. y] \ a \ set [x .e. y]" - using assms by (auto dest: arg_cong[where f=set]) - then show ?thesis by auto -qed - -(* FIXME: move to Word *) -lemma max_word_not_less[simp]: - "\ max_word < x" - by (simp add: not_less) - -(* FIXME: move to Word *) -lemma word_enum_prefix: - "[x .e. (y ::'a::len word)] = as @ a # bs \ as = (if x < a then [x .e. a - 1] else [])" - apply (induct as arbitrary: x; clarsimp) - apply (case_tac "x < y") - prefer 2 - apply (case_tac "x = y", simp) - apply (simp add: not_less) - apply (drule (1) dual_order.not_eq_order_implies_strict) - apply (simp add: word_upto_Nil) - apply (simp add: word_upto_Cons) - apply (case_tac "x < y") - prefer 2 - apply (case_tac "x = y", simp) - apply (simp add: not_less) - apply (drule (1) dual_order.not_eq_order_implies_strict) - apply (simp add: word_upto_Nil) - apply (clarsimp simp: word_upto_Cons) - apply (frule word_enum_decomp_elem) - apply clarsimp - apply (rule conjI) - prefer 2 - apply (subst word_Suc_le[symmetric]; clarsimp) - apply (drule meta_spec) - apply (drule (1) meta_mp) - apply clarsimp - apply (rule conjI; clarsimp) - apply (subst (2) word_upto_Cons) - apply unat_arith - apply simp - done - -(* FIXME: move to Word *) -lemma word_enum_decomp_set: - "[x .e. (y ::'a::len word)] = as @ a # bs \ a \ set as" - apply (subst word_enum_prefix, assumption) - apply (cases "x < a"; clarsimp) - apply unat_arith - done - -(* FIXME: move to Word *) -lemma word_enum_decomp: - assumes "[x .e. (y ::'a::len word)] = as @ a # bs" - shows "x \ a \ a \ y \ a \ set as \ (\z \ set as. x \ z \ z \ y)" -proof - - from assms - have "set as \ set [x .e. y] \ a \ set [x .e. y]" - by (auto dest: arg_cong[where f=set]) - with word_enum_decomp_set[OF assms] - show ?thesis by auto -qed - (* FIXME: move to lib *) lemma throw_opt_wp[wp]: "\if v = None then E ex else Q (the v)\ throw_opt ex v \Q\,\E\" diff --git a/proof/invariant-abstract/X64/ArchVSpace_AI.thy b/proof/invariant-abstract/X64/ArchVSpace_AI.thy index 59032b9c0..2f3438705 100644 --- a/proof/invariant-abstract/X64/ArchVSpace_AI.thy +++ b/proof/invariant-abstract/X64/ArchVSpace_AI.thy @@ -304,9 +304,6 @@ lemma ex_asid_high_bits_plus: prefer 2 apply fastforce apply (clarsimp simp: linorder_not_less) - apply (rule conjI) - prefer 2 - apply arith apply (subgoal_tac "n < 12", simp) apply (clarsimp simp add: linorder_not_le [symmetric]) done @@ -322,9 +319,6 @@ lemma asid_high_bits_shl: apply (rule context_conjI) apply (clarsimp simp add: linorder_not_less [symmetric]) apply simp - apply (rule conjI) - prefer 2 - apply simp apply (subgoal_tac "n < 12", simp) apply (clarsimp simp add: linorder_not_le [symmetric]) done diff --git a/proof/refine/RISCV64/ADT_H.thy b/proof/refine/RISCV64/ADT_H.thy index a7c925d74..d06c81d85 100644 --- a/proof/refine/RISCV64/ADT_H.thy +++ b/proof/refine/RISCV64/ADT_H.thy @@ -14,24 +14,6 @@ theory ADT_H imports Syscall_R begin -(* FIXME RISCV: move to Word *) -lemma distinct_word_add_ucast_shift_inj: - "\ p + (UCAST('a::len \ 'b::len) off << n) = p' + (ucast off' << n); - is_aligned p n'; is_aligned p' n'; n' = n + LENGTH('a); n' < LENGTH('b) \ - \ p' = p \ off' = off" - apply (simp add: word_and_or_mask_aligned le_mask_shiftl_le_mask[where n="LENGTH('a)"] - ucast_leq_mask) - apply (simp add: is_aligned_nth) - apply (rule conjI) - apply (rule word_eqI, clarsimp simp: bang_eq word_eqI_solve_simps) - apply (metis add_le_cancel_left bang_conj_lt diff_add_inverse le_Suc_ex nat_less_le) - apply (rule word_eqI, clarsimp simp: bang_eq word_eqI_solve_simps) - apply (rename_tac i) - apply (erule_tac x="i+n" in allE) - apply simp - done - - text \ The general refinement calculus (see theory Simulation) requires the definition of a so-called ``abstract datatype'' for each refinement layer. diff --git a/proof/refine/RISCV64/ArchAcc_R.thy b/proof/refine/RISCV64/ArchAcc_R.thy index 6ca90c7ae..6f0e08f06 100644 --- a/proof/refine/RISCV64/ArchAcc_R.thy +++ b/proof/refine/RISCV64/ArchAcc_R.thy @@ -42,135 +42,6 @@ lemma fst_assert_opt: "fst (assert_opt opt s) = (if opt = None then {} else {(the opt,s)})" by (clarsimp simp: assert_opt_def fail_def return_def split: option.split) -(* FIXME RISCV: move to Word *) -lemma mask_Suc: - "mask (Suc n) = 2^n + mask n" - by (simp add: mask_def) - -(* FIXME RISCV: move to Word *) -lemma is_aligned_no_overflow_mask: - "is_aligned x n \ x \ x + mask n" - by (simp add: mask_def) (erule is_aligned_no_overflow') - -(* FIXME RISCV: move to Word *) -lemma is_aligned_mask_offset_unat: - fixes off :: "('a::len) word" - and x :: "'a word" - assumes al: "is_aligned x sz" - and offv: "off \ mask sz" - shows "unat x + unat off < 2 ^ LENGTH('a)" -proof cases - assume szv: "sz < LENGTH('a)" - from al obtain k where xv: "x = 2 ^ sz * (of_nat k)" - and kl: "k < 2 ^ (LENGTH('a) - sz)" - by (auto elim: is_alignedE) - - from offv szv have offv': "unat off < 2 ^ sz" - apply (simp add: unat_mask word_le_nat_alt) - apply (erule order_le_less_trans) - apply simp - done - - show ?thesis using szv - apply (subst xv) - apply (subst unat_mult_power_lem[OF kl]) - apply (subst mult.commute, rule nat_add_offset_less) - apply (rule less_le_trans[OF offv'], simp) - apply (rule kl) - apply simp - done -next - assume "\ sz < LENGTH('a)" - with al have "x = 0" - apply (simp add: is_aligned_nth not_less) - apply (rule word_eqI, clarsimp simp: word_size) - done - thus ?thesis by simp -qed - -(* FIXME RISCV: move to Word *) -lemma of_bl_max: - "(of_bl xs :: 'a::len word) \ mask (length xs)" - apply (induct xs) - apply simp - apply (simp add: of_bl_Cons mask_Suc) - apply (rule conjI; clarsimp) - apply (erule word_plus_mono_right) - apply (rule is_aligned_no_overflow_mask) - apply (rule is_aligned_triv) - apply (simp add: word_le_nat_alt) - apply (subst unat_add_lem') - apply (rule is_aligned_mask_offset_unat) - apply (rule is_aligned_triv) - apply (simp add: mask_def) - apply simp - done - -(* FIXME RISCV: move to Word *) -lemma mask_over_length: - "LENGTH('a) \ n \ mask n = (-1::'a::len word)" - by (simp add: mask_def) - -(* FIXME RISCV: move to Word *) -lemma is_aligned_over_length: - "\ is_aligned p n; LENGTH('a) \ n \ \ (p::'a::len word) = 0" - by (simp add: is_aligned_mask mask_over_length) - -(* FIXME RISCV: move to Word *) -lemma Suc_2p_unat_mask: - "n < LENGTH('a) \ Suc (2 ^ n * k + unat (mask n :: 'a::len word)) = 2 ^ n * (k+1)" - by (simp add: unat_mask) - -(* FIXME RISCV: move to Word *) -lemma is_aligned_add_step_le: - "\ is_aligned (a::'a::len word) n; is_aligned b n; a < b; b \ a + mask n \ \ False" - apply (simp flip: not_le) - apply (erule notE) - apply (cases "LENGTH('a) \ n") - apply (drule (1) is_aligned_over_length)+ - apply (drule mask_over_length) - apply clarsimp - apply (clarsimp simp: word_le_nat_alt not_less) - apply (subst (asm) unat_plus_simple[THEN iffD1], erule is_aligned_no_overflow_mask) - apply (clarsimp simp: is_aligned_def dvd_def word_le_nat_alt) - apply (drule le_imp_less_Suc) - apply (simp add: Suc_2p_unat_mask) - by (metis Groups.mult_ac(2) Suc_leI linorder_not_less mult_le_mono order_refl times_nat.simps(2)) - -(* FIXME RISCV: move to Word *) -lemma power_2_mult_step_le: - "\n' \ n; 2 ^ n' * k' < 2 ^ n * k\ \ 2 ^ n' * (k' + 1) \ 2 ^ n * (k::nat)" - apply (cases "n'=n", simp) - apply (metis Suc_leI le_refl mult_Suc_right mult_le_mono semiring_normalization_rules(7)) - apply (drule (1) le_neq_trans) - apply clarsimp - apply (subgoal_tac "\m. n = n' + m") - prefer 2 - apply (simp add: le_Suc_ex) - apply (clarsimp simp: power_add) - by (metis Suc_leI mult.assoc mult_Suc_right nat_mult_le_cancel_disj) - -(* FIXME RISCV: move to Word *) -lemma aligned_mask_step: - "\ n' \ n; p' \ p + mask n; is_aligned p n; is_aligned p' n' \ \ - (p'::'a::len word) + mask n' \ p + mask n" - apply (cases "LENGTH('a) \ n") - apply (frule (1) is_aligned_over_length) - apply (drule mask_over_length) - apply clarsimp - apply (simp add: not_le) - apply (simp add: word_le_nat_alt unat_plus_simple) - apply (subst unat_plus_simple[THEN iffD1], erule is_aligned_no_overflow_mask)+ - apply (subst (asm) unat_plus_simple[THEN iffD1], erule is_aligned_no_overflow_mask) - apply (clarsimp simp: is_aligned_def dvd_def) - apply (rename_tac k k') - apply (thin_tac "unat p = x" for p x)+ - apply (subst Suc_le_mono[symmetric]) - apply (simp only: Suc_2p_unat_mask) - apply (drule le_imp_less_Suc, subst (asm) Suc_2p_unat_mask, assumption) - apply (erule (1) power_2_mult_step_le) - done - (* FIXME RISCV: move to Invariants_H, maybe further up *) lemma mask_range_subsetD: "\ p' \ mask_range p n; x' \ mask_range p' n'; n' \ n; is_aligned p n; is_aligned p' n' \ \ diff --git a/proof/refine/RISCV64/Arch_R.thy b/proof/refine/RISCV64/Arch_R.thy index 127536be5..e58249b05 100644 --- a/proof/refine/RISCV64/Arch_R.thy +++ b/proof/refine/RISCV64/Arch_R.thy @@ -870,50 +870,6 @@ lemma dom_ucast_eq: apply (word_bitwise) done -(* FIXME RISCV: replace in WordLib (generalised) *) -lemma aligned_mask_disjoint: - "\ is_aligned (a :: 'a :: len word) n; b \ mask n \ \ a && b = 0" - apply (rule word_eqI) - apply (clarsimp simp: is_aligned_nth word_size mask_def simp del: word_less_sub_le) - apply (frule le2p_bits_unset) - apply (case_tac "na < n") - apply simp - apply simp - done - -(* FIXME RISCV: move to WordLib! *) -lemma word_and_or_mask_aligned: - "\ is_aligned a n; b \ mask n \ \ a + b = a || b" - apply (rule word_plus_and_or_coroll) - apply (erule (1) aligned_mask_disjoint) - done - -(* FIXME RISCV: move to WordLib! *) -lemmas word_and_or_mask_aligned2 = - word_and_or_mask_aligned[where a=b and b=a for a b, - simplified add.commute word_bool_alg.disj.commute] - -(* FIXME RISCV: move to WordLib *) -lemma is_aligned_ucastI: - "is_aligned w n \ is_aligned (ucast w) n" - by (clarsimp simp: word_eqI_solve_simps) - -(* FIXME RISCV: move to WordLib *) -lemma ucast_le_maskI: - "a \ mask n \ UCAST('a::len \ 'b::len) a \ mask n" - apply (clarsimp simp: le_mask_high_bits word_eqI_solve_simps) - apply (frule test_bit_size) - apply (simp add: word_size) - done - -(* FIXME RISCV: move to WordLib *) -lemma ucast_add_mask_aligned: - "\ a \ mask n; is_aligned b n \ \ UCAST ('a::len \ 'b::len) (a + b) = ucast a + ucast b" - apply (simp add: word_and_or_mask_aligned2) - apply (subst word_and_or_mask_aligned2, erule is_aligned_ucastI, erule ucast_le_maskI) - apply word_eqI_solve - done - (* FIXME RISCV: replace in ArchArch_AI *) lemma ucast_fst_hd_assocs: assumes "- dom (\x::asid_low_index. pool (ucast x)) \ {x. ucast x + (a::RISCV64_A.asid) \ 0} \ {}" @@ -974,11 +930,6 @@ proof - done qed -(* FIXME RISCV: move to WordLib *) -lemma ucast_shiftl: - "LENGTH('b) \ LENGTH ('a) \ UCAST ('a::len \ 'b::len) x << n = ucast (x << n)" - by word_eqI_solve - lemma dec_arch_inv_corres: notes check_vp_inv[wp del] check_vp_wpR[wp] (* FIXME: check_vp_inv shadowed check_vp_wpR. Instead, diff --git a/proof/refine/RISCV64/Detype_R.thy b/proof/refine/RISCV64/Detype_R.thy index b03261e8a..9f331e64a 100644 --- a/proof/refine/RISCV64/Detype_R.thy +++ b/proof/refine/RISCV64/Detype_R.thy @@ -12,18 +12,6 @@ theory Detype_R imports Retype_R begin -(* FIXME RISCV: move to Word *) -lemma mask_mono: - "sz' \ sz \ mask sz' \ (mask sz :: 'a::len word)" - apply (cases "sz < LENGTH('a)") - apply (simp only: mask_def shiftl_1) - apply (rule word_le_minus_mono_left) - apply (erule (1) two_power_increasing) - apply (rule word_1_le_power) - apply simp - apply (simp add: not_less mask_over_length) - done - context begin interpretation Arch . (*FIXME: arch_split*) text \Establishing that the invariants are maintained @@ -189,16 +177,6 @@ lemma deleteObjects_def3: unless_def alignError_def) done -(* FIXME: move to Word_Lib *) -lemma ucast_less_shiftl_helper': - "\ len_of TYPE('b) + (a::nat) < len_of TYPE('a); 2 ^ (len_of TYPE('b) + a) \ n\ - \ (ucast (x :: 'b::len word) << a) < (n :: 'a::len word)" - apply (erule order_less_le_trans[rotated]) - using ucast_less[where x=x and 'a='a] - apply (simp only: shiftl_t2n field_simps) - apply (rule word_less_power_trans2; simp) - done - lemma obj_relation_cuts_in_obj_range: "\ (y, P) \ obj_relation_cuts ko x; x \ obj_range x ko; kheap s x = Some ko; valid_objs s; pspace_aligned s \ \ y \ obj_range x ko"