# HG changeset patch # User paulson # Date 1724539445 -3600 # Node ID 8f96e1329845348c1d82e8180e2194fd680bf587 # Parent 32f0e953cc96fe65a607fe395a8ebc6319dde74e Some tidying diff -r 32f0e953cc96 -r 8f96e1329845 src/HOL/Bit_Operations.thy --- a/src/HOL/Bit_Operations.thy Sat Aug 24 14:14:57 2024 +0100 +++ b/src/HOL/Bit_Operations.thy Sat Aug 24 23:44:05 2024 +0100 @@ -148,7 +148,7 @@ lemma bit_imp_possible_bit: \possible_bit TYPE('a) n\ if \bit a n\ - by (rule ccontr) (use that in \auto simp add: bit_iff_odd possible_bit_def\) + by (rule ccontr) (use that in \auto simp: bit_iff_odd possible_bit_def\) lemma impossible_bit: \\ bit a n\ if \\ possible_bit TYPE('a) n\ @@ -161,7 +161,7 @@ lemma possible_bit_min [simp]: \possible_bit TYPE('a) (min i j) \ possible_bit TYPE('a) i \ possible_bit TYPE('a) j\ - by (auto simp add: min_def elim: possible_bit_less_imp) + by (auto simp: min_def elim: possible_bit_less_imp) lemma bit_eqI: \a = b\ if \\n. possible_bit TYPE('a) n \ bit a n \ bit b n\ @@ -213,7 +213,7 @@ also have \\ = b\ by (fact mod_mult_div_eq) finally show ?case - by (auto simp add: mod2_eq_if) + by (auto simp: mod2_eq_if) qed qed @@ -262,7 +262,7 @@ \bit (2 * a) (Suc n) \ possible_bit TYPE('a) (Suc n) \ bit a n\ using even_double_div_exp_iff [of n a] by (cases \possible_bit TYPE('a) (Suc n)\) - (auto simp add: bit_iff_odd possible_bit_def) + (auto simp: bit_iff_odd possible_bit_def) lemma bit_double_iff [bit_simps]: \bit (2 * a) n \ possible_bit TYPE('a) n \ n \ 0 \ bit a (n - 1)\ @@ -382,7 +382,7 @@ with rec [of n True] show ?case by simp qed -qed (auto simp add: div_mult2_eq bit_nat_def) +qed (auto simp: div_mult2_eq bit_nat_def) end @@ -422,12 +422,12 @@ case (even m) then show ?case by (cases n) - (auto simp add: bit_double_iff Bit_Operations.bit_double_iff possible_bit_def bit_0 dest: mult_not_zero) + (auto simp: bit_double_iff Bit_Operations.bit_double_iff possible_bit_def bit_0 dest: mult_not_zero) next case (odd m) then show ?case by (cases n) - (auto simp add: bit_double_iff even_bit_succ_iff possible_bit_def + (auto simp: bit_double_iff even_bit_succ_iff possible_bit_def Bit_Operations.bit_Suc Bit_Operations.bit_0 dest: mult_not_zero) qed with True show ?thesis @@ -521,7 +521,7 @@ with rec [of k True] show ?case by (simp add: ac_simps) qed -qed (auto simp add: zdiv_zmult2_eq bit_int_def) +qed (auto simp: zdiv_zmult2_eq bit_int_def) end @@ -637,25 +637,25 @@ qed sublocale "and": semilattice \(AND)\ - by standard (auto simp add: bit_eq_iff bit_and_iff) + by standard (auto simp: bit_eq_iff bit_and_iff) sublocale or: semilattice_neutr \(OR)\ 0 - by standard (auto simp add: bit_eq_iff bit_or_iff) + by standard (auto simp: bit_eq_iff bit_or_iff) sublocale xor: comm_monoid \(XOR)\ 0 - by standard (auto simp add: bit_eq_iff bit_xor_iff) + by standard (auto simp: bit_eq_iff bit_xor_iff) lemma even_and_iff: \even (a AND b) \ even a \ even b\ - using bit_and_iff [of a b 0] by (auto simp add: bit_0) + using bit_and_iff [of a b 0] by (auto simp: bit_0) lemma even_or_iff: \even (a OR b) \ even a \ even b\ - using bit_or_iff [of a b 0] by (auto simp add: bit_0) + using bit_or_iff [of a b 0] by (auto simp: bit_0) lemma even_xor_iff: \even (a XOR b) \ (even a \ even b)\ - using bit_xor_iff [of a b 0] by (auto simp add: bit_0) + using bit_xor_iff [of a b 0] by (auto simp: bit_0) lemma zero_and_eq [simp]: \0 AND a = 0\ @@ -667,7 +667,7 @@ lemma one_and_eq: \1 AND a = a mod 2\ - by (simp add: bit_eq_iff bit_and_iff) (auto simp add: bit_1_iff bit_0) + by (simp add: bit_eq_iff bit_and_iff) (auto simp: bit_1_iff bit_0) lemma and_one_eq: \a AND 1 = a mod 2\ @@ -676,7 +676,7 @@ lemma one_or_eq: \1 OR a = a + of_bool (even a)\ by (simp add: bit_eq_iff bit_or_iff add.commute [of _ 1] even_bit_succ_iff) - (auto simp add: bit_1_iff bit_0) + (auto simp: bit_1_iff bit_0) lemma or_one_eq: \a OR 1 = a + of_bool (even a)\ @@ -685,7 +685,7 @@ lemma one_xor_eq: \1 XOR a = a + of_bool (even a) - of_bool (odd a)\ by (simp add: bit_eq_iff bit_xor_iff add.commute [of _ 1] even_bit_succ_iff) - (auto simp add: bit_1_iff odd_bit_iff_bit_pred bit_0 elim: oddE) + (auto simp: bit_1_iff odd_bit_iff_bit_pred bit_0 elim: oddE) lemma xor_one_eq: \a XOR 1 = a + of_bool (even a) - of_bool (odd a)\ @@ -762,7 +762,7 @@ lemma even_mask_iff: \even (mask n) \ n = 0\ - using bit_mask_iff [of n 0] by (auto simp add: bit_0) + using bit_mask_iff [of n 0] by (auto simp: bit_0) lemma mask_Suc_0 [simp]: \mask (Suc 0) = 1\ @@ -770,7 +770,7 @@ lemma mask_Suc_exp: \mask (Suc n) = 2 ^ n OR mask n\ - by (auto simp add: bit_eq_iff bit_simps) + by (auto simp: bit_eq_iff bit_simps) lemma mask_numeral: \mask (numeral n) = 1 + 2 * mask (pred_numeral n)\ @@ -793,20 +793,19 @@ proof (induction n arbitrary: m) case 0 then show ?case - by (auto simp add: bit_0 push_bit_eq_mult) + by (auto simp: bit_0 push_bit_eq_mult) next case (Suc n) show ?case proof (cases m) case 0 then show ?thesis - by (auto simp add: bit_imp_possible_bit) + by (auto simp: bit_imp_possible_bit) next - case (Suc m) - with Suc.prems Suc.IH [of m] show ?thesis + case (Suc m') + with Suc.prems Suc.IH [of m'] show ?thesis apply (simp add: push_bit_double) - apply (simp add: bit_simps mult.commute [of _ 2]) - apply (auto simp add: possible_bit_less_imp) + apply (auto simp: possible_bit_less_imp bit_simps mult.commute [of _ 2]) done qed qed @@ -849,7 +848,7 @@ lemma disjunctive_xor_eq_or: \a XOR b = a OR b\ if \a AND b = 0\ - using that by (auto simp add: bit_eq_iff bit_simps) + using that by (auto simp: bit_eq_iff bit_simps) lemma disjunctive_add_eq_or: \a + b = a OR b\ if \a AND b = 0\ @@ -864,11 +863,11 @@ proof (induction n arbitrary: a b) case 0 from "0"(2)[of 0] show ?case - by (auto simp add: even_or_iff bit_0) + by (auto simp: even_or_iff bit_0) next case (Suc n) from Suc.prems(2) [of 0] have even: \even a \ even b\ - by (auto simp add: bit_0) + by (auto simp: bit_0) have bit: \\ bit (a div 2) n \ \ bit (b div 2) n\ for n using Suc.prems(2) [of \Suc n\] by (simp add: bit_Suc) from Suc.prems have \possible_bit TYPE('a) n\ @@ -879,7 +878,7 @@ have \a + b = (a div 2 * 2 + a mod 2) + (b div 2 * 2 + b mod 2)\ using div_mult_mod_eq [of a 2] div_mult_mod_eq [of b 2] by simp also have \\ = of_bool (odd a \ odd b) + 2 * (a div 2 + b div 2)\ - using even by (auto simp add: algebra_simps mod2_eq_if) + using even by (auto simp: algebra_simps mod2_eq_if) finally have \bit ((a + b) div 2) n \ bit (a div 2 + b div 2) n\ using \possible_bit TYPE('a) (Suc n)\ by simp (simp_all flip: bit_Suc add: bit_double_iff possible_bit_def) also have \\ \ bit (a div 2 OR b div 2) n\ @@ -929,9 +928,9 @@ also have \\ \ m \ n \ bit a n \ n < m \ bit a n\ by auto also have \m \ n \ bit a n \ bit (push_bit m (drop_bit m a)) n\ - by (auto simp add: bit_simps bit_imp_possible_bit) + by (auto simp: bit_simps bit_imp_possible_bit) finally show ?thesis - by (auto simp add: bit_simps) + by (auto simp: bit_simps) qed lemma take_bit_Suc: @@ -1004,19 +1003,19 @@ lemma push_bit_take_bit: \push_bit m (take_bit n a) = take_bit (m + n) (push_bit m a)\ - by (rule bit_eqI) (auto simp add: bit_simps) + by (rule bit_eqI) (auto simp: bit_simps) lemma take_bit_push_bit: \take_bit m (push_bit n a) = push_bit n (take_bit (m - n) a)\ - by (rule bit_eqI) (auto simp add: bit_simps) + by (rule bit_eqI) (auto simp: bit_simps) lemma take_bit_drop_bit: \take_bit m (drop_bit n a) = drop_bit n (take_bit (m + n) a)\ - by (rule bit_eqI) (auto simp add: bit_simps) + by (rule bit_eqI) (auto simp: bit_simps) lemma drop_bit_take_bit: \drop_bit m (take_bit n a) = take_bit (n - m) (drop_bit m a)\ - by (rule bit_eqI) (auto simp add: bit_simps) + by (rule bit_eqI) (auto simp: bit_simps) lemma even_push_bit_iff [simp]: \even (push_bit n a) \ n \ 0 \ even a\ @@ -1091,49 +1090,49 @@ then have \ \ bit a (n + (m - n))\ by (simp add: bit_simps) then show \bit (take_bit n a) m \ bit a m\ - by (cases \m < n\) (auto simp add: bit_simps) + by (cases \m < n\) (auto simp: bit_simps) qed qed lemma drop_bit_exp_eq: \drop_bit m (2 ^ n) = of_bool (m \ n \ possible_bit TYPE('a) n) * 2 ^ (n - m)\ - by (auto simp add: bit_eq_iff bit_simps) + by (auto simp: bit_eq_iff bit_simps) lemma take_bit_and [simp]: \take_bit n (a AND b) = take_bit n a AND take_bit n b\ - by (auto simp add: bit_eq_iff bit_simps) + by (auto simp: bit_eq_iff bit_simps) lemma take_bit_or [simp]: \take_bit n (a OR b) = take_bit n a OR take_bit n b\ - by (auto simp add: bit_eq_iff bit_simps) + by (auto simp: bit_eq_iff bit_simps) lemma take_bit_xor [simp]: \take_bit n (a XOR b) = take_bit n a XOR take_bit n b\ - by (auto simp add: bit_eq_iff bit_simps) + by (auto simp: bit_eq_iff bit_simps) lemma push_bit_and [simp]: \push_bit n (a AND b) = push_bit n a AND push_bit n b\ - by (auto simp add: bit_eq_iff bit_simps) + by (auto simp: bit_eq_iff bit_simps) lemma push_bit_or [simp]: \push_bit n (a OR b) = push_bit n a OR push_bit n b\ - by (auto simp add: bit_eq_iff bit_simps) + by (auto simp: bit_eq_iff bit_simps) lemma push_bit_xor [simp]: \push_bit n (a XOR b) = push_bit n a XOR push_bit n b\ - by (auto simp add: bit_eq_iff bit_simps) + by (auto simp: bit_eq_iff bit_simps) lemma drop_bit_and [simp]: \drop_bit n (a AND b) = drop_bit n a AND drop_bit n b\ - by (auto simp add: bit_eq_iff bit_simps) + by (auto simp: bit_eq_iff bit_simps) lemma drop_bit_or [simp]: \drop_bit n (a OR b) = drop_bit n a OR drop_bit n b\ - by (auto simp add: bit_eq_iff bit_simps) + by (auto simp: bit_eq_iff bit_simps) lemma drop_bit_xor [simp]: \drop_bit n (a XOR b) = drop_bit n a XOR drop_bit n b\ - by (auto simp add: bit_eq_iff bit_simps) + by (auto simp: bit_eq_iff bit_simps) lemma take_bit_of_mask [simp]: \take_bit m (mask n) = mask (min m n)\ @@ -1141,11 +1140,11 @@ lemma take_bit_eq_mask: \take_bit n a = a AND mask n\ - by (auto simp add: bit_eq_iff bit_simps) + by (auto simp: bit_eq_iff bit_simps) lemma or_eq_0_iff: \a OR b = 0 \ a = 0 \ b = 0\ - by (auto simp add: bit_eq_iff bit_or_iff) + by (auto simp: bit_eq_iff bit_or_iff) lemma bit_iff_and_drop_bit_eq_1: \bit a n \ drop_bit n a AND 1 = 1\ @@ -1157,23 +1156,23 @@ lemma bit_set_bit_iff [bit_simps]: \bit (set_bit m a) n \ bit a n \ (m = n \ possible_bit TYPE('a) n)\ - by (auto simp add: set_bit_eq_or bit_or_iff bit_exp_iff) + by (auto simp: set_bit_eq_or bit_or_iff bit_exp_iff) lemma even_set_bit_iff: \even (set_bit m a) \ even a \ m \ 0\ - using bit_set_bit_iff [of m a 0] by (auto simp add: bit_0) + using bit_set_bit_iff [of m a 0] by (auto simp: bit_0) lemma bit_unset_bit_iff [bit_simps]: \bit (unset_bit m a) n \ bit a n \ m \ n\ - by (auto simp add: unset_bit_eq_or_xor bit_simps dest: bit_imp_possible_bit) + by (auto simp: unset_bit_eq_or_xor bit_simps dest: bit_imp_possible_bit) lemma even_unset_bit_iff: \even (unset_bit m a) \ even a \ m = 0\ - using bit_unset_bit_iff [of m a 0] by (auto simp add: bit_0) + using bit_unset_bit_iff [of m a 0] by (auto simp: bit_0) lemma bit_flip_bit_iff [bit_simps]: \bit (flip_bit m a) n \ (m = n \ \ bit a n) \ possible_bit TYPE('a) n\ - by (auto simp add: bit_eq_iff bit_simps flip_bit_eq_xor bit_imp_possible_bit) + by (auto simp: bit_eq_iff bit_simps flip_bit_eq_xor bit_imp_possible_bit) lemma even_flip_bit_iff: \even (flip_bit m a) \ \ (even a \ m = 0)\ @@ -1182,7 +1181,7 @@ lemma and_exp_eq_0_iff_not_bit: \a AND 2 ^ n = 0 \ \ bit a n\ (is \?P \ ?Q\) using bit_imp_possible_bit[of a n] - by (auto simp add: bit_eq_iff bit_simps) + by (auto simp: bit_eq_iff bit_simps) lemma bit_sum_mult_2_cases: assumes a: \\j. \ bit a (Suc j)\ @@ -1191,52 +1190,52 @@ from a have \n = 0\ if \bit a n\ for n using that by (cases n) simp_all then have \a = 0 \ a = 1\ - by (auto simp add: bit_eq_iff bit_1_iff) + by (auto simp: bit_eq_iff bit_1_iff) then show ?thesis - by (cases n) (auto simp add: bit_0 bit_double_iff even_bit_succ_iff) + by (cases n) (auto simp: bit_0 bit_double_iff even_bit_succ_iff) qed lemma set_bit_0 [simp]: \set_bit 0 a = 1 + 2 * (a div 2)\ - by (auto simp add: bit_eq_iff bit_simps even_bit_succ_iff simp flip: bit_Suc) + by (auto simp: bit_eq_iff bit_simps even_bit_succ_iff simp flip: bit_Suc) lemma set_bit_Suc: \set_bit (Suc n) a = a mod 2 + 2 * set_bit n (a div 2)\ - by (auto simp add: bit_eq_iff bit_sum_mult_2_cases bit_simps bit_0 simp flip: bit_Suc + by (auto simp: bit_eq_iff bit_sum_mult_2_cases bit_simps bit_0 simp flip: bit_Suc elim: possible_bit_less_imp) lemma unset_bit_0 [simp]: \unset_bit 0 a = 2 * (a div 2)\ - by (auto simp add: bit_eq_iff bit_simps simp flip: bit_Suc) + by (auto simp: bit_eq_iff bit_simps simp flip: bit_Suc) lemma unset_bit_Suc: \unset_bit (Suc n) a = a mod 2 + 2 * unset_bit n (a div 2)\ - by (auto simp add: bit_eq_iff bit_sum_mult_2_cases bit_simps bit_0 simp flip: bit_Suc) + by (auto simp: bit_eq_iff bit_sum_mult_2_cases bit_simps bit_0 simp flip: bit_Suc) lemma flip_bit_0 [simp]: \flip_bit 0 a = of_bool (even a) + 2 * (a div 2)\ - by (auto simp add: bit_eq_iff bit_simps even_bit_succ_iff bit_0 simp flip: bit_Suc) + by (auto simp: bit_eq_iff bit_simps even_bit_succ_iff bit_0 simp flip: bit_Suc) lemma flip_bit_Suc: \flip_bit (Suc n) a = a mod 2 + 2 * flip_bit n (a div 2)\ - by (auto simp add: bit_eq_iff bit_sum_mult_2_cases bit_simps bit_0 simp flip: bit_Suc + by (auto simp: bit_eq_iff bit_sum_mult_2_cases bit_simps bit_0 simp flip: bit_Suc elim: possible_bit_less_imp) lemma flip_bit_eq_if: \flip_bit n a = (if bit a n then unset_bit else set_bit) n a\ - by (rule bit_eqI) (auto simp add: bit_set_bit_iff bit_unset_bit_iff bit_flip_bit_iff) + by (rule bit_eqI) (auto simp: bit_set_bit_iff bit_unset_bit_iff bit_flip_bit_iff) lemma take_bit_set_bit_eq: \take_bit n (set_bit m a) = (if n \ m then take_bit n a else set_bit m (take_bit n a))\ - by (rule bit_eqI) (auto simp add: bit_take_bit_iff bit_set_bit_iff) + by (rule bit_eqI) (auto simp: bit_take_bit_iff bit_set_bit_iff) lemma take_bit_unset_bit_eq: \take_bit n (unset_bit m a) = (if n \ m then take_bit n a else unset_bit m (take_bit n a))\ - by (rule bit_eqI) (auto simp add: bit_take_bit_iff bit_unset_bit_iff) + by (rule bit_eqI) (auto simp: bit_take_bit_iff bit_unset_bit_iff) lemma take_bit_flip_bit_eq: \take_bit n (flip_bit m a) = (if n \ m then take_bit n a else flip_bit m (take_bit n a))\ - by (rule bit_eqI) (auto simp add: bit_take_bit_iff bit_flip_bit_iff) + by (rule bit_eqI) (auto simp: bit_take_bit_iff bit_flip_bit_iff) lemma bit_1_0 [simp]: \bit 1 0\ @@ -1272,17 +1271,17 @@ with bit_rec [of _ n] Cons.prems Cons.IH [of m] show ?thesis by (simp add: bit_simps) - (auto simp add: possible_bit_less_imp bit_simps simp flip: bit_Suc) + (auto simp: possible_bit_less_imp bit_simps simp flip: bit_Suc) qed qed lemma horner_sum_bit_eq_take_bit: \horner_sum of_bool 2 (map (bit a) [0.. - by (rule bit_eqI) (auto simp add: bit_simps) + by (rule bit_eqI) (auto simp: bit_simps) lemma take_bit_horner_sum_bit_eq: \take_bit n (horner_sum of_bool 2 bs) = horner_sum of_bool 2 (take n bs)\ - by (auto simp add: bit_eq_iff bit_take_bit_iff bit_horner_sum_bit_iff) + by (auto simp: bit_eq_iff bit_take_bit_iff bit_horner_sum_bit_iff) lemma take_bit_sum: \take_bit n a = (\k = 0.. @@ -1292,9 +1291,9 @@ \set_bit n a = a + of_bool (\ bit a n) * 2 ^ n\ proof - have \a AND of_bool (\ bit a n) * 2 ^ n = 0\ - by (auto simp add: bit_eq_iff bit_simps) + by (auto simp: bit_eq_iff bit_simps) then show ?thesis - by (auto simp add: bit_eq_iff bit_simps disjunctive_add_eq_or) + by (auto simp: bit_eq_iff bit_simps disjunctive_add_eq_or) qed end @@ -1360,7 +1359,7 @@ lemma bit_not_exp_iff [bit_simps]: \bit (NOT (2 ^ m)) n \ possible_bit TYPE('a) n \ n \ m\ - by (auto simp add: bit_not_iff bit_exp_iff) + by (auto simp: bit_not_iff bit_exp_iff) lemma bit_minus_iff [bit_simps]: \bit (- a) n \ possible_bit TYPE('a) n \ \ bit (a - 1) n\ @@ -1372,7 +1371,7 @@ lemma bit_minus_exp_iff [bit_simps]: \bit (- (2 ^ m)) n \ possible_bit TYPE('a) n \ n \ m\ - by (auto simp add: bit_simps simp flip: mask_eq_exp_minus_1) + by (auto simp: bit_simps simp flip: mask_eq_exp_minus_1) lemma bit_minus_2_iff [simp]: \bit (- 2) n \ possible_bit TYPE('a) n \ n > 0\ @@ -1394,13 +1393,13 @@ by standard (rule bit_eqI, simp add: bit_and_iff) sublocale bit: abstract_boolean_algebra \(AND)\ \(OR)\ NOT 0 \- 1\ - by standard (auto simp add: bit_and_iff bit_or_iff bit_not_iff intro: bit_eqI) + by standard (auto simp: bit_and_iff bit_or_iff bit_not_iff intro: bit_eqI) sublocale bit: abstract_boolean_algebra_sym_diff \(AND)\ \(OR)\ NOT 0 \- 1\ \(XOR)\ - apply standard - apply (rule bit_eqI) - apply (auto simp add: bit_simps) - done +proof + show \\x y. x XOR y = x AND NOT y OR NOT x AND y\ + by (intro bit_eqI) (auto simp: bit_simps) +qed lemma and_eq_not_not_or: \a AND b = NOT (NOT a OR NOT b)\ @@ -1424,7 +1423,7 @@ lemma disjunctive_and_not_eq_xor: \a AND NOT b = a XOR b\ if \NOT a AND b = 0\ - using that by (auto simp add: bit_eq_iff bit_simps) + using that by (auto simp: bit_eq_iff bit_simps) lemma disjunctive_diff_eq_and_not: \a - b = a AND NOT b\ if \NOT a AND b = 0\ @@ -1447,11 +1446,11 @@ lemma take_bit_not_take_bit: \take_bit n (NOT (take_bit n a)) = take_bit n (NOT a)\ - by (auto simp add: bit_eq_iff bit_take_bit_iff bit_not_iff) + by (auto simp: bit_eq_iff bit_take_bit_iff bit_not_iff) lemma take_bit_not_iff: \take_bit n (NOT a) = take_bit n (NOT b) \ take_bit n a = take_bit n b\ - by (auto simp add: bit_eq_iff bit_simps) + by (auto simp: bit_eq_iff bit_simps) lemma take_bit_not_eq_mask_diff: \take_bit n (NOT a) = mask n - take_bit n a\ @@ -1459,7 +1458,7 @@ have \NOT (mask n) AND take_bit n a = 0\ by (simp add: bit_eq_iff bit_simps) moreover have \take_bit n (NOT a) = mask n AND NOT (take_bit n a)\ - by (auto simp add: bit_eq_iff bit_simps) + by (auto simp: bit_eq_iff bit_simps) ultimately show ?thesis by (simp add: disjunctive_diff_eq_and_not) qed @@ -1486,14 +1485,11 @@ lemma unset_bit_eq_and_not: \unset_bit n a = a AND NOT (push_bit n 1)\ - by (rule bit_eqI) (auto simp add: bit_simps) + by (rule bit_eqI) (auto simp: bit_simps) lemma push_bit_Suc_minus_numeral [simp]: \push_bit (Suc n) (- numeral k) = push_bit n (- numeral (Num.Bit0 k))\ - apply (simp only: numeral_Bit0) - apply simp - apply (simp only: numeral_mult mult_2_right numeral_add) - done + using local.push_bit_Suc_numeral push_bit_minus by presburger lemma push_bit_minus_numeral [simp]: \push_bit (numeral l) (- numeral k) = push_bit (pred_numeral l) (- numeral (Num.Bit0 k))\ @@ -1509,11 +1505,11 @@ lemma push_bit_mask_eq: \push_bit m (mask n) = mask (n + m) AND NOT (mask m)\ - by (rule bit_eqI) (auto simp add: bit_simps not_less possible_bit_less_imp) + by (rule bit_eqI) (auto simp: bit_simps not_less possible_bit_less_imp) lemma slice_eq_mask: \push_bit n (take_bit m (drop_bit n a)) = a AND mask (m + n) AND NOT (mask n)\ - by (rule bit_eqI) (auto simp add: bit_simps) + by (rule bit_eqI) (auto simp: bit_simps) lemma push_bit_numeral_minus_1 [simp]: \push_bit (numeral n) (- 1) = - (2 ^ numeral n)\ @@ -1523,9 +1519,9 @@ \unset_bit n a = a - of_bool (bit a n) * 2 ^ n\ proof - have \NOT a AND of_bool (bit a n) * 2 ^ n = 0\ - by (auto simp add: bit_eq_iff bit_simps) + by (auto simp: bit_eq_iff bit_simps) moreover have \unset_bit n a = a AND NOT (of_bool (bit a n) * 2 ^ n)\ - by (auto simp add: bit_eq_iff bit_simps) + by (auto simp: bit_eq_iff bit_simps) ultimately show ?thesis by (simp add: disjunctive_diff_eq_and_not) qed @@ -1616,7 +1612,7 @@ lemma drop_bit_mask_eq: \drop_bit m (mask n) = mask (n - m)\ - by (rule bit_eqI) (auto simp add: bit_simps possible_bit_def) + by (rule bit_eqI) (auto simp: bit_simps possible_bit_def) lemma bit_push_bit_iff': \bit (push_bit m a) n \ m \ n \ bit a (n - m)\ @@ -1645,7 +1641,7 @@ proof (rule ccontr) assume \\ 0 < take_bit m a\ then have \take_bit m a = 0\ - by (auto simp add: not_less intro: order_antisym) + by (auto simp: not_less intro: order_antisym) then have \bit (take_bit m a) n = bit 0 n\ by simp with that show False @@ -1659,7 +1655,7 @@ lemma drop_bit_push_bit: \drop_bit m (push_bit n a) = drop_bit (m - n) (push_bit (n - m) a)\ by (cases \m \ n\) - (auto simp add: mult.left_commute [of _ \2 ^ n\] mult.commute [of _ \2 ^ n\] mult.assoc + (auto simp: mult.left_commute [of _ \2 ^ n\] mult.commute [of _ \2 ^ n\] mult.assoc mult.commute [of a] drop_bit_eq_div push_bit_eq_mult not_le power_add Orderings.not_le dest!: le_Suc_ex less_imp_Suc_add) end @@ -1684,7 +1680,7 @@ have less_eq: \\k div 2\ \ \k\\ for k :: int by (cases k) (simp_all add: divide_int_def nat_add_distrib) then have less: \\k div 2\ < \k\\ if \k \ {0, - 1}\ for k :: int - using that by (auto simp add: less_le [of k]) + using that by (auto simp: less_le [of k]) show \wf (measure (\(k, l). nat (\k\ + \l\)))\ by simp show \((k div 2, l div 2), k, l) \ measure (\(k, l). nat (\k\ + \l\))\ @@ -1721,11 +1717,11 @@ proof (cases \k \ {0, - 1} \ l \ {0, - 1}\) case True then show ?thesis - by (auto simp add: F.simps [of 0] F.simps [of \- 1\]) + by (auto simp: F.simps [of 0] F.simps [of \- 1\]) next case False then show ?thesis - by (auto simp add: ac_simps F.simps [of k l]) + by (auto simp: ac_simps F.simps [of k l]) qed lemma bit_iff: @@ -1800,7 +1796,7 @@ fix k l :: int and m n :: nat show \unset_bit n k = (k OR push_bit n 1) XOR push_bit n 1\ by (rule bit_eqI) - (auto simp add: unset_bit_int_def + (auto simp: unset_bit_int_def and_int.bit_iff or_int.bit_iff xor_int.bit_iff bit_not_int_iff push_bit_int_def bit_simps) qed (fact and_int.rec or_int.rec xor_int.rec mask_int_def set_bit_int_def flip_bit_int_def push_bit_int_def drop_bit_int_def take_bit_int_def not_int_def)+ @@ -1837,13 +1833,13 @@ case (even k) then show ?case using bit_double_iff [of \of_int k\ n] Bit_Operations.bit_double_iff [of k n] - by (cases n) (auto simp add: ac_simps possible_bit_def dest: mult_not_zero) + by (cases n) (auto simp: ac_simps possible_bit_def dest: mult_not_zero) next case (odd k) then show ?case using bit_double_iff [of \of_int k\ n] by (cases n) - (auto simp add: ac_simps bit_double_iff even_bit_succ_iff Bit_Operations.bit_0 Bit_Operations.bit_Suc + (auto simp: ac_simps bit_double_iff even_bit_succ_iff Bit_Operations.bit_0 Bit_Operations.bit_Suc possible_bit_def dest: mult_not_zero) qed with True show ?thesis @@ -1953,7 +1949,7 @@ by simp with and_int.rec [of \1 + k * 2\ l] show ?case - by (auto simp add: zero_le_mult_iff not_le) + by (auto simp: zero_le_mult_iff not_le) qed lemma and_negative_int_iff [simp]: @@ -2018,7 +2014,7 @@ lemma xor_negative_int_iff [simp]: \k XOR l < 0 \ (k < 0) \ (l < 0)\ for k l :: int - by (subst Not_eq_iff [symmetric]) (auto simp add: not_less) + by (subst Not_eq_iff [symmetric]) (auto simp: not_less) lemma OR_upper: \<^marker>\contributor \Stefan Berghofer\\ \x OR y < 2 ^ n\ if \0 \ x\ \x < 2 ^ n\ \y < 2 ^ n\ for x y :: int @@ -2034,12 +2030,12 @@ case (even x) from even.IH [of \n - 1\ \y div 2\] even.prems even.hyps show ?case - by (cases n) (auto simp add: or_int.rec [of \_ * 2\] elim: oddE) + by (cases n) (auto simp: or_int.rec [of \_ * 2\] elim: oddE) next case (odd x) from odd.IH [of \n - 1\ \y div 2\] odd.prems odd.hyps show ?case - by (cases n) (auto simp add: or_int.rec [of \1 + _ * 2\], linarith) + by (cases n) (auto simp: or_int.rec [of \1 + _ * 2\], linarith) qed lemma XOR_upper: \<^marker>\contributor \Stefan Berghofer\\ @@ -2056,12 +2052,12 @@ case (even x) from even.IH [of \n - 1\ \y div 2\] even.prems even.hyps show ?case - by (cases n) (auto simp add: xor_int.rec [of \_ * 2\] elim: oddE) + by (cases n) (auto simp: xor_int.rec [of \_ * 2\] elim: oddE) next case (odd x) from odd.IH [of \n - 1\ \y div 2\] odd.prems odd.hyps show ?case - by (cases n) (auto simp add: xor_int.rec [of \1 + _ * 2\]) + by (cases n) (auto simp: xor_int.rec [of \1 + _ * 2\]) qed lemma AND_lower [simp]: \<^marker>\contributor \Stefan Berghofer\\ @@ -2120,12 +2116,12 @@ case (even x) from even.IH [of \y div 2\] show ?case - by (auto simp add: and_int.rec [of _ y] or_int.rec [of _ y] elim: oddE) + by (auto simp: and_int.rec [of _ y] or_int.rec [of _ y] elim: oddE) next case (odd x) from odd.IH [of \y div 2\] show ?case - by (auto simp add: and_int.rec [of _ y] or_int.rec [of _ y] elim: oddE) + by (auto simp: and_int.rec [of _ y] or_int.rec [of _ y] elim: oddE) qed lemma push_bit_minus_one: @@ -2182,7 +2178,7 @@ lemma drop_bit_nonnegative_int_iff [simp]: \drop_bit n k \ 0 \ k \ 0\ for k :: int - by (induction n) (auto simp add: drop_bit_Suc drop_bit_half) + by (induction n) (auto simp: drop_bit_Suc drop_bit_half) lemma drop_bit_negative_int_iff [simp]: \drop_bit n k < 0 \ k < 0\ for k :: int @@ -2223,17 +2219,17 @@ lemma and_int_unfold: \k AND l = (if k = 0 \ l = 0 then 0 else if k = - 1 then l else if l = - 1 then k else (k mod 2) * (l mod 2) + 2 * ((k div 2) AND (l div 2)))\ for k l :: int - by (auto simp add: and_int.rec [of k l] zmult_eq_1_iff elim: oddE) + by (auto simp: and_int.rec [of k l] zmult_eq_1_iff elim: oddE) lemma or_int_unfold: \k OR l = (if k = - 1 \ l = - 1 then - 1 else if k = 0 then l else if l = 0 then k else max (k mod 2) (l mod 2) + 2 * ((k div 2) OR (l div 2)))\ for k l :: int - by (auto simp add: or_int.rec [of k l] elim: oddE) + by (auto simp: or_int.rec [of k l] elim: oddE) lemma xor_int_unfold: \k XOR l = (if k = - 1 then NOT l else if l = - 1 then NOT k else if k = 0 then l else if l = 0 then k else \k mod 2 - l mod 2\ + 2 * ((k div 2) XOR (l div 2)))\ for k l :: int - by (auto simp add: xor_int.rec [of k l] not_int_def elim!: oddE) + by (auto simp: xor_int.rec [of k l] not_int_def elim!: oddE) lemma bit_minus_int_iff: \bit (- k) n \ bit (NOT (k - 1)) n\ for k :: int @@ -2325,7 +2321,7 @@ lemma take_bit_int_less_self_iff: \take_bit n k < k \ 2 ^ n \ k\ for k :: int - by (auto simp add: less_le take_bit_int_less_eq_self_iff take_bit_int_eq_self_iff + by (auto simp: less_le take_bit_int_less_eq_self_iff take_bit_int_eq_self_iff intro: order_trans [of 0 \2 ^ n\ k]) lemma take_bit_int_greater_self_iff: @@ -2334,7 +2330,7 @@ lemma take_bit_int_greater_eq_self_iff: \k \ take_bit n k \ k < 2 ^ n\ for k :: int - by (auto simp add: le_less take_bit_int_greater_self_iff take_bit_int_eq_self_iff + by (auto simp: le_less take_bit_int_greater_self_iff take_bit_int_eq_self_iff dest: sym not_sym intro: less_trans [of k 0 \2 ^ n\]) lemma take_bit_tightened_less_eq_int: @@ -2370,7 +2366,7 @@ fix m assume \nat k \ m\ then show \bit k m \ bit k (nat k)\ - by (auto simp add: * bit_iff_odd power_add zdiv_zmult2_eq dest!: le_Suc_ex) + by (auto simp: * bit_iff_odd power_add zdiv_zmult2_eq dest!: le_Suc_ex) qed next case False @@ -2388,7 +2384,7 @@ fix m assume \nat (- k) \ m\ then show \bit k m \ bit k (nat (- k))\ - by (auto simp add: * bit_iff_odd power_add zdiv_zmult2_eq minus_1_div_exp_eq_int dest!: le_Suc_ex) + by (auto simp: * bit_iff_odd power_add zdiv_zmult2_eq minus_1_div_exp_eq_int dest!: le_Suc_ex) qed qed show thesis @@ -2408,18 +2404,12 @@ moreover have \finite N\ \r \ N\ using ** N_def \r < q\ by auto moreover define n where \n = Suc (Max N)\ - ultimately have \\m. n \ m \ bit k m \ bit k n\ - apply auto - apply (metis (full_types, lifting) "*" Max_ge_iff Suc_n_not_le_n \finite N\ all_not_in_conv mem_Collect_eq not_le) - apply (metis "*" Max_ge Suc_n_not_le_n \finite N\ linorder_not_less mem_Collect_eq) - apply (metis "*" Max_ge Suc_n_not_le_n \finite N\ linorder_not_less mem_Collect_eq) - apply (metis (full_types, lifting) "*" Max_ge_iff Suc_n_not_le_n \finite N\ all_not_in_conv mem_Collect_eq not_le) - done + ultimately have \: \\m. n \ m \ bit k m \ bit k n\ + by (smt (verit) "*" Max_ge Suc_n_not_le_n linorder_not_less mem_Collect_eq not_less_eq_eq) have \bit k (Max N) \ bit k n\ by (metis (mono_tags, lifting) "*" Max_in N_def \\m. n \ m \ bit k m = bit k n\ \finite N\ \r \ N\ empty_iff le_cases mem_Collect_eq) - show thesis apply (rule that [of n]) - using \\m. n \ m \ bit k m = bit k n\ apply blast - using \bit k (Max N) \ bit k n\ n_def by auto + with \ n_def that [of n] show thesis + by fastforce qed qed @@ -2591,17 +2581,17 @@ lemma and_nat_unfold [code]: \m AND n = (if m = 0 \ n = 0 then 0 else (m mod 2) * (n mod 2) + 2 * ((m div 2) AND (n div 2)))\ for m n :: nat - by (auto simp add: and_rec [of m n] elim: oddE) + by (auto simp: and_rec [of m n] elim: oddE) lemma or_nat_unfold [code]: \m OR n = (if m = 0 then n else if n = 0 then m else max (m mod 2) (n mod 2) + 2 * ((m div 2) OR (n div 2)))\ for m n :: nat - by (auto simp add: or_rec [of m n] elim: oddE) + by (auto simp: or_rec [of m n] elim: oddE) lemma xor_nat_unfold [code]: \m XOR n = (if m = 0 then n else if n = 0 then m else (m mod 2 + n mod 2) mod 2 + 2 * ((m div 2) XOR (n div 2)))\ for m n :: nat - by (auto simp add: xor_rec [of m n] elim!: oddE) + by (auto simp: xor_rec [of m n] elim!: oddE) lemma [code]: \unset_bit 0 m = 2 * (m div 2)\ @@ -2680,10 +2670,11 @@ lemma drop_bit_nat_eq: \drop_bit n (nat k) = nat (drop_bit n k)\ - apply (cases \k \ 0\) - apply (simp_all add: drop_bit_eq_div nat_div_distrib nat_power_eq not_le) - apply (simp add: divide_int_def) - done +proof (cases \k \ 0\) + case True + then show ?thesis + by (metis drop_bit_of_nat int_nat_eq nat_int) +qed (simp add: nat_eq_iff2) lemma take_bit_nat_eq: \take_bit n (nat k) = nat (take_bit n k)\ if \k \ 0\ @@ -2932,7 +2923,7 @@ \numeral (Num.Bit1 m) AND NOT (1 :: int) = numeral (Num.Bit0 m)\ \numeral (Num.Bit1 m) AND NOT (numeral (Num.Bit0 n)) = 1 + (2 :: int) * (numeral m AND NOT (numeral n))\ \numeral (Num.Bit1 m) AND NOT (numeral (Num.Bit1 n)) = (2 :: int) * (numeral m AND NOT (numeral n))\ - by (simp_all add: bit_eq_iff) (auto simp add: bit_0 bit_simps bit_Suc bit_numeral_rec BitM_inc_eq sub_inc_One_eq split: nat.split) + by (simp_all add: bit_eq_iff) (auto simp: bit_0 bit_simps bit_Suc bit_numeral_rec BitM_inc_eq sub_inc_One_eq split: nat.split) fun and_not_num :: \num \ num \ num option\ \<^marker>\contributor \Andreas Lochbihler\\ where @@ -2989,7 +2980,7 @@ \numeral (Num.Bit1 m) OR NOT (numeral (Num.Bit0 n)) = 1 + (2 :: int) * (numeral m OR NOT (numeral n))\ \numeral (Num.Bit1 m) OR NOT (numeral (Num.Bit1 n)) = 1 + (2 :: int) * (numeral m OR NOT (numeral n))\ by (simp_all add: bit_eq_iff) - (auto simp add: bit_0 bit_simps bit_Suc bit_numeral_rec sub_inc_One_eq split: nat.split) + (auto simp: bit_0 bit_simps bit_Suc bit_numeral_rec sub_inc_One_eq split: nat.split) fun or_not_num_neg :: \num \ num \ num\ \<^marker>\contributor \Andreas Lochbihler\\ where @@ -3055,7 +3046,7 @@ (case take_bit_num (pred_numeral r) m of None \ None | Some q \ Some (Num.Bit0 q))\ \take_bit_num (numeral r) (Num.Bit1 m) = Some (case take_bit_num (pred_numeral r) m of None \ Num.One | Some q \ Num.Bit1 q)\ - by (auto simp add: take_bit_num_def ac_simps mult_2 num_of_nat_double + by (auto simp: take_bit_num_def ac_simps mult_2 num_of_nat_double take_bit_Suc_bit0 take_bit_Suc_bit1 take_bit_numeral_bit0 take_bit_numeral_bit1) lemma take_bit_num_code [code]: @@ -3085,7 +3076,7 @@ \take_bit m (numeral n) = numeral q\ if \take_bit_num m n = Some q\ proof - from that have \take_bit m (numeral n :: nat) = numeral q\ - by (auto simp add: take_bit_num_def Num.numeral_num_of_nat_unfold split: if_splits) + by (auto simp: take_bit_num_def Num.numeral_num_of_nat_unfold split: if_splits) then have \of_nat (take_bit m (numeral n)) = of_nat (numeral q)\ by simp then show ?thesis @@ -3193,7 +3184,7 @@ \Int.Neg num.One AND Int.Pos m = Int.Pos m\ \Int.Neg (num.Bit0 n) AND Int.Pos m = Num.sub (or_not_num_neg (Num.BitM n) m) num.One\ \Int.Neg (num.Bit1 n) AND Int.Pos m = Num.sub (or_not_num_neg (num.Bit0 n) m) num.One\ - apply (auto simp add: and_num_eq_None_iff [where ?'a = int] and_num_eq_Some_iff [where ?'a = int] + apply (auto simp: and_num_eq_None_iff [where ?'a = int] and_num_eq_Some_iff [where ?'a = int] split: option.split) apply (simp_all only: sub_one_eq_not_neg numeral_or_not_num_eq minus_minus and_not_numerals bit.de_Morgan_disj bit.double_compl and_not_num_eq_None_iff and_not_num_eq_Some_iff ac_simps) @@ -3236,7 +3227,7 @@ \Int.Neg num.One OR Int.Pos m = Int.Neg num.One\ \Int.Neg (num.Bit0 n) OR Int.Pos m = (case and_not_num (Num.BitM n) m of None \ -1 | Some n' \ Int.Neg (Num.inc n'))\ \Int.Neg (num.Bit1 n) OR Int.Pos m = (case and_not_num (num.Bit0 n) m of None \ -1 | Some n' \ Int.Neg (Num.inc n'))\ - apply (auto simp add: numeral_or_num_eq split: option.splits) + apply (auto simp: numeral_or_num_eq split: option.splits) apply (simp_all only: and_not_num_eq_None_iff and_not_num_eq_Some_iff and_not_numerals numeral_or_not_num_eq or_eq_not_not_and bit.double_compl ac_simps flip: numeral_eq_iff [where ?'a = int]) apply simp_all @@ -3372,11 +3363,11 @@ lemma concat_bit_assoc: \concat_bit n k (concat_bit m l r) = concat_bit (m + n) (concat_bit n k l) r\ - by (rule bit_eqI) (auto simp add: bit_concat_bit_iff ac_simps) + by (rule bit_eqI) (auto simp: bit_concat_bit_iff ac_simps) lemma concat_bit_assoc_sym: \concat_bit m (concat_bit n k l) r = concat_bit (min m n) k (concat_bit (m - n) l r)\ - by (rule bit_eqI) (auto simp add: bit_concat_bit_iff ac_simps min_def) + by (rule bit_eqI) (auto simp: bit_concat_bit_iff ac_simps min_def) lemma concat_bit_eq_iff: \concat_bit n k l = concat_bit n r s @@ -3394,14 +3385,14 @@ fix m from * [of m] show \bit (take_bit n k) m \ bit (take_bit n r) m\ - by (auto simp add: bit_take_bit_iff bit_concat_bit_iff) + by (auto simp: bit_take_bit_iff bit_concat_bit_iff) qed moreover have \push_bit n l = push_bit n s\ proof (rule bit_eqI) fix m from * [of m] show \bit (push_bit n l) m \ bit (push_bit n s) m\ - by (auto simp add: bit_push_bit_iff bit_concat_bit_iff) + by (auto simp: bit_push_bit_iff bit_concat_bit_iff) qed then have \l = s\ by (simp add: push_bit_eq_mult) @@ -3412,7 +3403,7 @@ lemma take_bit_concat_bit_eq: \take_bit m (concat_bit n k l) = concat_bit (min m n) k (take_bit (m - n) l)\ by (rule bit_eqI) - (auto simp add: bit_take_bit_iff bit_concat_bit_iff min_def) + (auto simp: bit_take_bit_iff bit_concat_bit_iff min_def) lemma concat_bit_take_bit_eq: \concat_bit n (take_bit n b) = concat_bit n b\ @@ -3437,7 +3428,7 @@ lemma even_signed_take_bit_iff: \even (signed_take_bit m a) \ even a\ - by (auto simp add: bit_0 signed_take_bit_def even_or_iff even_mask_iff bit_double_iff) + by (auto simp: bit_0 signed_take_bit_def even_or_iff even_mask_iff bit_double_iff) lemma bit_signed_take_bit_iff [bit_simps]: \bit (signed_take_bit m a) n \ possible_bit TYPE('a) n \ bit a (min m n)\ @@ -3479,21 +3470,21 @@ by (simp add: fun_eq_iff bit_signed_take_bit_iff bit_take_bit_iff not_le less_Suc_eq_le min_def) (use bit_imp_possible_bit in fastforce) then show ?thesis - by (auto simp add: fun_eq_iff intro: bit_eqI) + by (auto simp: fun_eq_iff intro: bit_eqI) qed lemma signed_take_bit_signed_take_bit [simp]: \signed_take_bit m (signed_take_bit n a) = signed_take_bit (min m n) a\ - by (auto simp add: bit_eq_iff bit_simps ac_simps) + by (auto simp: bit_eq_iff bit_simps ac_simps) lemma signed_take_bit_take_bit: \signed_take_bit m (take_bit n a) = (if n \ m then take_bit n else signed_take_bit m) a\ - by (rule bit_eqI) (auto simp add: bit_signed_take_bit_iff min_def bit_take_bit_iff) + by (rule bit_eqI) (auto simp: bit_signed_take_bit_iff min_def bit_take_bit_iff) lemma take_bit_signed_take_bit: \take_bit m (signed_take_bit n a) = take_bit m a\ if \m \ Suc n\ using that by (rule le_SucE; intro bit_eqI) - (auto simp add: bit_take_bit_iff bit_signed_take_bit_iff min_def less_Suc_eq) + (auto simp: bit_take_bit_iff bit_signed_take_bit_iff min_def less_Suc_eq) lemma signed_take_bit_eq_take_bit_add: \signed_take_bit n k = take_bit (Suc n) k + NOT (mask (Suc n)) * of_bool (bit k n)\ @@ -3504,7 +3495,7 @@ next case True have \signed_take_bit n k = take_bit (Suc n) k OR NOT (mask (Suc n))\ - by (rule bit_eqI) (auto simp add: bit_signed_take_bit_iff min_def bit_take_bit_iff bit_or_iff bit_not_iff bit_mask_iff less_Suc_eq True) + by (rule bit_eqI) (auto simp: bit_signed_take_bit_iff min_def bit_take_bit_iff bit_or_iff bit_not_iff bit_mask_iff less_Suc_eq True) also have \\ = take_bit (Suc n) k + NOT (mask (Suc n))\ by (simp add: disjunctive_add_eq_or bit_eq_iff bit_simps) finally show ?thesis @@ -3623,7 +3614,7 @@ lemma signed_take_bit_int_eq_self_iff: \signed_take_bit n k = k \ - (2 ^ n) \ k \ k < 2 ^ n\ for k :: int - by (auto simp add: signed_take_bit_eq_take_bit_shift take_bit_int_eq_self_iff algebra_simps) + by (auto simp: signed_take_bit_eq_take_bit_shift take_bit_int_eq_self_iff algebra_simps) lemma signed_take_bit_int_eq_self: \signed_take_bit n k = k\ if \- (2 ^ n) \ k\ \k < 2 ^ n\ @@ -3782,9 +3773,8 @@ lemma exp_div_exp_eq: \2 ^ m div 2 ^ n = of_bool (2 ^ m \ 0 \ m \ n) * 2 ^ (m - n)\ - apply (rule bit_eqI) - using bit_exp_iff div_exp_eq apply (auto simp add: bit_iff_odd possible_bit_def) - done + using bit_exp_iff div_exp_eq + by (intro bit_eqI) (auto simp: bit_iff_odd possible_bit_def) lemma bits_1_div_2: \1 div 2 = 0\ @@ -3855,11 +3845,11 @@ with that show ?thesis proof (induction n arbitrary: a b) case 0 from "0.prems"(1) [of 0] show ?case - by (auto simp add: bit_0) + by (auto simp: bit_0) next case (Suc n) from Suc.prems(1) [of 0] have even: \even a \ even b\ - by (auto simp add: bit_0) + by (auto simp: bit_0) have bit: \\ bit (a div 2) n \ \ bit (b div 2) n\ for n using Suc.prems(1) [of \Suc n\] by (simp add: bit_Suc) from Suc.prems(2) have \possible_bit TYPE('a) (Suc n)\ \possible_bit TYPE('a) n\ @@ -3867,7 +3857,7 @@ have \a + b = (a div 2 * 2 + a mod 2) + (b div 2 * 2 + b mod 2)\ using div_mult_mod_eq [of a 2] div_mult_mod_eq [of b 2] by simp also have \\ = of_bool (odd a \ odd b) + 2 * (a div 2 + b div 2)\ - using even by (auto simp add: algebra_simps mod2_eq_if) + using even by (auto simp: algebra_simps mod2_eq_if) finally have \bit ((a + b) div 2) n \ bit (a div 2 + b div 2) n\ using \possible_bit TYPE('a) (Suc n)\ by simp (simp_all flip: bit_Suc add: bit_double_iff possible_bit_def) also have \\ \ bit (a div 2) n \ bit (b div 2) n\ @@ -3884,7 +3874,7 @@ lemma even_mask_div_iff: \even ((2 ^ m - 1) div 2 ^ n) \ 2 ^ n = 0 \ m \ n\ - using bit_mask_iff [of m n] by (auto simp add: mask_eq_exp_minus_1 bit_iff_odd possible_bit_def) + using bit_mask_iff [of m n] by (auto simp: mask_eq_exp_minus_1 bit_iff_odd possible_bit_def) lemma mod_exp_eq: \a mod 2 ^ m mod 2 ^ n = a mod 2 ^ min m n\ @@ -3920,7 +3910,7 @@ lemma even_mod_exp_div_exp_iff: \even (a mod 2 ^ m div 2 ^ n) \ m \ n \ even (a div 2 ^ n)\ - by (auto simp add: even_drop_bit_iff_not_bit bit_simps simp flip: drop_bit_eq_div take_bit_eq_mod) + by (auto simp: even_drop_bit_iff_not_bit bit_simps simp flip: drop_bit_eq_div take_bit_eq_mod) end @@ -3931,7 +3921,7 @@ \a - b = a AND NOT b\ if \\n. bit b n \ bit a n\ proof - have \NOT a + b = NOT a OR b\ - by (rule disjunctive_add) (auto simp add: bit_not_iff dest: that) + by (rule disjunctive_add) (auto simp: bit_not_iff dest: that) then have \NOT (NOT a + b) = NOT (NOT a OR b)\ by simp then show ?thesis diff -r 32f0e953cc96 -r 8f96e1329845 src/HOL/List.thy --- a/src/HOL/List.thy Sat Aug 24 14:14:57 2024 +0100 +++ b/src/HOL/List.thy Sat Aug 24 23:44:05 2024 +0100 @@ -3359,12 +3359,7 @@ lemma nth_take_lemma: "k \ length xs \ k \ length ys \ (\i. i < k \ xs!i = ys!i) \ take k xs = take k ys" -proof (induct k arbitrary: xs ys) - case (Suc k) - then show ?case - apply (simp add: less_Suc_eq_0_disj) - by (simp add: Suc.prems(3) take_Suc_conv_app_nth) -qed simp + by (induct k arbitrary: xs ys) (simp_all add: take_Suc_conv_app_nth) lemma nth_equalityI: "\length xs = length ys; \i. i < length xs \ xs!i = ys!i\ \ xs = ys" @@ -3712,7 +3707,7 @@ lemma nth_eq_iff_index_eq: "\ distinct xs; i < length xs; j < length xs \ \ (xs!i = xs!j) = (i = j)" -by(auto simp: distinct_conv_nth) + by(auto simp: distinct_conv_nth) lemma distinct_Ex1: "distinct xs \ x \ set xs \ (\!i. i < length xs \ xs ! i = x)" @@ -3733,9 +3728,7 @@ lemma distinct_swap[simp]: "\ i < size xs; j < size xs\ \ distinct(xs[i := xs!j, j := xs!i]) = distinct xs" - apply (simp add: distinct_conv_nth nth_list_update) - apply (safe; metis) - done + by (smt (verit, del_insts) distinct_conv_nth length_list_update nth_list_update) lemma set_swap[simp]: "\ i < size xs; j < size xs \ \ set(xs[i := xs!j, j := xs!i]) = set xs" @@ -4320,7 +4313,7 @@ next case (Cons x xs) thus ?case apply(auto simp: nth_Cons' split: if_splits) - using diff_Suc_1[unfolded One_nat_def] less_Suc_eq_0_disj by fastforce + using diff_Suc_1 less_Suc_eq_0_disj by fastforce qed lemmas find_Some_iff2 = find_Some_iff[THEN eq_iff_swap] @@ -4514,9 +4507,16 @@ distinct (removeAll [] xs) \ (\ys. ys \ set xs \ distinct ys) \ (\ys zs. ys \ set xs \ zs \ set xs \ ys \ zs \ set ys \ set zs = {})" -apply (induct xs) - apply(simp_all, safe, auto) -by (metis Int_iff UN_I empty_iff equals0I set_empty) +proof (induct xs) + case Nil + then show ?case by auto +next + case (Cons a xs) + have "\set a \ \ (set ` set xs) = {}; a \ set xs\ \ a=[]" + by (metis Int_iff UN_I empty_iff equals0I set_empty) + then show ?case + by (auto simp: Cons) +qed subsubsection \\<^const>\replicate\\ @@ -4535,24 +4535,24 @@ qed lemma Ex_list_of_length: "\xs. length xs = n" -by (rule exI[of _ "replicate n undefined"]) simp + by (rule exI[of _ "replicate n undefined"]) simp lemma map_replicate [simp]: "map f (replicate n x) = replicate n (f x)" -by (induct n) auto + by (induct n) auto lemma map_replicate_const: "map (\ x. k) lst = replicate (length lst) k" -by (induct lst) auto + by (induct lst) auto lemma replicate_app_Cons_same: -"(replicate n x) @ (x # xs) = x # replicate n x @ xs" -by (induct n) auto + "(replicate n x) @ (x # xs) = x # replicate n x @ xs" + by (induct n) auto lemma rev_replicate [simp]: "rev (replicate n x) = replicate n x" -by (induct n) (auto simp: replicate_app_Cons_same) + by (metis length_rev map_replicate map_replicate_const rev_map) lemma replicate_add: "replicate (n + m) x = replicate n x @ replicate m x" -by (induct n) auto + by (induct n) auto text\Courtesy of Matthias Daum:\ lemma append_replicate_commute: @@ -4899,10 +4899,7 @@ lemma nth_rotate: \rotate m xs ! n = xs ! ((m + n) mod length xs)\ if \n < length xs\ - using that apply (auto simp add: rotate_drop_take nth_append not_less less_diff_conv ac_simps dest!: le_Suc_ex) - apply (metis add.commute mod_add_right_eq mod_less) - apply (metis (no_types, lifting) Nat.diff_diff_right add.commute add_diff_cancel_right' diff_le_self dual_order.strict_trans2 length_greater_0_conv less_nat_zero_code list.size(3) mod_add_right_eq mod_add_self2 mod_le_divisor mod_less) - done + by (smt (verit) add.commute hd_rotate_conv_nth length_rotate not_less0 list.size(3) mod_less rotate_rotate that) lemma nth_rotate1: \rotate1 xs ! n = xs ! (Suc n mod length xs)\ if \n < length xs\ @@ -4944,10 +4941,8 @@ by (auto simp add: nths_def) lemma nths_all: "\i < length xs. i \ I \ nths xs I = xs" -apply (simp add: nths_def) -apply (subst filter_True) - apply (auto simp: in_set_zip subset_iff) -done + unfolding nths_def + by (metis add_0 diff_zero filter_True in_set_zip length_upt nth_upt zip_eq_conv) lemma length_nths: "length (nths xs I) = card{i. i < length xs \ i \ I}" @@ -5343,8 +5338,7 @@ show ?thesis unfolding transpose.simps \i = Suc j\ nth_Cons_Suc "3.hyps"[OF j_less] - apply (auto simp: transpose_aux_filter_tail filter_map comp_def length_transpose * ** *** XS_def[symmetric]) - by (simp add: nth_tl) + by (auto simp: nth_tl transpose_aux_filter_tail filter_map comp_def length_transpose * ** *** XS_def[symmetric]) qed qed simp_all @@ -6644,14 +6638,9 @@ have "(xs,ys) \ ?L (Suc n)" if r: "(xs,ys) \ ?R (Suc n)" for xs ys proof - from r obtain xys where r': "?len (Suc n) xs" "?len (Suc n) ys" "?P xs ys xys" by auto - then show ?thesis - proof (cases xys) - case Nil - thus ?thesis using r' by (auto simp: image_Collect lex_prod_def) - next - case Cons - thus ?thesis using r' Suc by (fastforce simp: image_Collect lex_prod_def) - qed + then show ?thesis + using r' Suc + by (cases xys; fastforce simp: image_Collect lex_prod_def) qed moreover have "(xs,ys) \ ?L (Suc n) \ (xs,ys) \ ?R (Suc n)" for xs ys using Suc by (auto simp add: image_Collect lex_prod_def)(blast, meson Cons_eq_appendI) @@ -6867,25 +6856,25 @@ lemma lexord_same_pref_iff: "(xs @ ys, xs @ zs) \ lexord r \ (\x \ set xs. (x,x) \ r) \ (ys, zs) \ lexord r" -by(induction xs) auto + by(induction xs) auto lemma lexord_same_pref_if_irrefl[simp]: "irrefl r \ (xs @ ys, xs @ zs) \ lexord r \ (ys, zs) \ lexord r" -by (simp add: irrefl_def lexord_same_pref_iff) + by (simp add: irrefl_def lexord_same_pref_iff) lemma lexord_append_rightI: "\ b z. y = b # z \ (x, x @ y) \ lexord r" -by (metis append_Nil2 lexord_Nil_left lexord_same_pref_iff) + by (metis append_Nil2 lexord_Nil_left lexord_same_pref_iff) lemma lexord_append_left_rightI: "(a,b) \ r \ (u @ a # x, u @ b # y) \ lexord r" -by (simp add: lexord_same_pref_iff) + by (simp add: lexord_same_pref_iff) lemma lexord_append_leftI: "(u,v) \ lexord r \ (x @ u, x @ v) \ lexord r" -by (simp add: lexord_same_pref_iff) + by (simp add: lexord_same_pref_iff) lemma lexord_append_leftD: "\(x @ u, x @ v) \ lexord r; (\a. (a,a) \ r) \ \ (u,v) \ lexord r" -by (simp add: lexord_same_pref_iff) + by (simp add: lexord_same_pref_iff) lemma lexord_take_index_conv: "((x,y) \ lexord r) = @@ -6897,9 +6886,13 @@ moreover have "(\u a b. (a, b) \ r \ (\v. x = u @ a # v) \ (\w. y = u @ b # w)) = (\i take i x = take i y \ (x ! i, y ! i) \ r)" - apply safe - using less_iff_Suc_add apply auto[1] - by (metis id_take_nth_drop) + (is "?L=?R") + proof + show "?L\?R" + by (metis append_eq_conv_conj drop_all leI list.simps(3) nth_append_length) + show "?R\?L" + by (metis id_take_nth_drop) + qed ultimately show ?thesis by (auto simp: lexord_def Let_def) qed @@ -7118,19 +7111,19 @@ by(subst lexordp_eq.simps, fastforce)+ lemma lexordp_append_rightI: "ys \ Nil \ lexordp xs (xs @ ys)" -by(induct xs)(auto simp add: neq_Nil_conv) + by(induct xs)(auto simp add: neq_Nil_conv) lemma lexordp_append_left_rightI: "x < y \ lexordp (us @ x # xs) (us @ y # ys)" -by(induct us) auto + by(induct us) auto lemma lexordp_eq_refl: "lexordp_eq xs xs" -by(induct xs) simp_all + by(induct xs) simp_all lemma lexordp_append_leftI: "lexordp us vs \ lexordp (xs @ us) (xs @ vs)" -by(induct xs) auto + by(induct xs) auto lemma lexordp_append_leftD: "\ lexordp (xs @ us) (xs @ vs); \a. \ a < a \ \ lexordp us vs" -by(induct xs) auto + by(induct xs) auto lemma lexordp_irreflexive: assumes irrefl: "\x. \ x < x" @@ -7251,21 +7244,21 @@ definition "measures fs = inv_image (lex less_than) (%a. map (%f. f a) fs)" lemma wf_measures[simp]: "wf (measures fs)" -unfolding measures_def -by blast + unfolding measures_def + by blast lemma in_measures[simp]: "(x, y) \ measures [] = False" "(x, y) \ measures (f # fs) = (f x < f y \ (f x = f y \ (x, y) \ measures fs))" -unfolding measures_def -by auto + unfolding measures_def + by auto lemma measures_less: "f x < f y \ (x, y) \ measures (f#fs)" -by simp + by simp lemma measures_lesseq: "f x \ f y \ (x, y) \ measures fs \ (x, y) \ measures (f#fs)" -by auto + by auto subsubsection \Lifting Relations to Lists: one element\ @@ -7286,27 +7279,27 @@ unfolding listrel1_def by auto lemma not_Nil_listrel1 [iff]: "([], xs) \ listrel1 r" -unfolding listrel1_def by blast + unfolding listrel1_def by blast lemma not_listrel1_Nil [iff]: "(xs, []) \ listrel1 r" -unfolding listrel1_def by blast + unfolding listrel1_def by blast lemma Cons_listrel1_Cons [iff]: "(x # xs, y # ys) \ listrel1 r \ (x,y) \ r \ xs = ys \ x = y \ (xs, ys) \ listrel1 r" -by (simp add: listrel1_def Cons_eq_append_conv) (blast) + by (simp add: listrel1_def Cons_eq_append_conv) (blast) lemma listrel1I1: "(x,y) \ r \ (x # xs, y # xs) \ listrel1 r" -by fast + by fast lemma listrel1I2: "(xs, ys) \ listrel1 r \ (x # xs, x # ys) \ listrel1 r" -by fast + by fast lemma append_listrel1I: "(xs, ys) \ listrel1 r \ us = vs \ xs = ys \ (us, vs) \ listrel1 r \ (xs @ us, ys @ vs) \ listrel1 r" -unfolding listrel1_def -by auto (blast intro: append_eq_appendI)+ + unfolding listrel1_def + by auto (blast intro: append_eq_appendI)+ lemma Cons_listrel1E1[elim!]: assumes "(x # xs, ys) \ listrel1 r" @@ -7333,19 +7326,19 @@ qed lemma listrel1_eq_len: "(xs,ys) \ listrel1 r \ length xs = length ys" -unfolding listrel1_def by auto + unfolding listrel1_def by auto lemma listrel1_mono: "r \ s \ listrel1 r \ listrel1 s" -unfolding listrel1_def by blast + unfolding listrel1_def by blast lemma listrel1_converse: "listrel1 (r\) = (listrel1 r)\" -unfolding listrel1_def by blast + unfolding listrel1_def by blast lemma in_listrel1_converse: "(x,y) \ listrel1 (r\) \ (x,y) \ (listrel1 r)\" -unfolding listrel1_def by blast + unfolding listrel1_def by blast lemma listrel1_iff_update: "(xs,ys) \ (listrel1 r) @@ -7618,19 +7611,19 @@ stack overflow in some target languages.\ fun map_tailrec_rev :: "('a \ 'b) \ 'a list \ 'b list \ 'b list" where -"map_tailrec_rev f [] bs = bs" | -"map_tailrec_rev f (a#as) bs = map_tailrec_rev f as (f a # bs)" + "map_tailrec_rev f [] bs = bs" | + "map_tailrec_rev f (a#as) bs = map_tailrec_rev f as (f a # bs)" lemma map_tailrec_rev: "map_tailrec_rev f as bs = rev(map f as) @ bs" -by(induction as arbitrary: bs) simp_all + by(induction as arbitrary: bs) simp_all definition map_tailrec :: "('a \ 'b) \ 'a list \ 'b list" where -"map_tailrec f as = rev (map_tailrec_rev f as [])" + "map_tailrec f as = rev (map_tailrec_rev f as [])" text\Code equation:\ lemma map_eq_map_tailrec: "map = map_tailrec" -by(simp add: fun_eq_iff map_tailrec_def map_tailrec_rev) + by(simp add: fun_eq_iff map_tailrec_def map_tailrec_rev) subsubsection \Counterparts for set-related operations\ @@ -8375,7 +8368,7 @@ lemma list_all_transfer [transfer_rule]: "((A ===> (=)) ===> list_all2 A ===> (=)) list_all list_all" - unfolding list_all_iff [abs_def] by transfer_prover + using list.pred_transfer by blast lemma list_ex_transfer [transfer_rule]: "((A ===> (=)) ===> list_all2 A ===> (=)) list_ex list_ex"