--- 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:
\<open>possible_bit TYPE('a) n\<close> if \<open>bit a n\<close>
- by (rule ccontr) (use that in \<open>auto simp add: bit_iff_odd possible_bit_def\<close>)
+ by (rule ccontr) (use that in \<open>auto simp: bit_iff_odd possible_bit_def\<close>)
lemma impossible_bit:
\<open>\<not> bit a n\<close> if \<open>\<not> possible_bit TYPE('a) n\<close>
@@ -161,7 +161,7 @@
lemma possible_bit_min [simp]:
\<open>possible_bit TYPE('a) (min i j) \<longleftrightarrow> possible_bit TYPE('a) i \<or> possible_bit TYPE('a) j\<close>
- by (auto simp add: min_def elim: possible_bit_less_imp)
+ by (auto simp: min_def elim: possible_bit_less_imp)
lemma bit_eqI:
\<open>a = b\<close> if \<open>\<And>n. possible_bit TYPE('a) n \<Longrightarrow> bit a n \<longleftrightarrow> bit b n\<close>
@@ -213,7 +213,7 @@
also have \<open>\<dots> = b\<close>
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 @@
\<open>bit (2 * a) (Suc n) \<longleftrightarrow> possible_bit TYPE('a) (Suc n) \<and> bit a n\<close>
using even_double_div_exp_iff [of n a]
by (cases \<open>possible_bit TYPE('a) (Suc n)\<close>)
- (auto simp add: bit_iff_odd possible_bit_def)
+ (auto simp: bit_iff_odd possible_bit_def)
lemma bit_double_iff [bit_simps]:
\<open>bit (2 * a) n \<longleftrightarrow> possible_bit TYPE('a) n \<and> n \<noteq> 0 \<and> bit a (n - 1)\<close>
@@ -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 \<open>(AND)\<close>
- 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 \<open>(OR)\<close> 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 \<open>(XOR)\<close> 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:
\<open>even (a AND b) \<longleftrightarrow> even a \<or> even b\<close>
- 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:
\<open>even (a OR b) \<longleftrightarrow> even a \<and> even b\<close>
- 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:
\<open>even (a XOR b) \<longleftrightarrow> (even a \<longleftrightarrow> even b)\<close>
- 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]:
\<open>0 AND a = 0\<close>
@@ -667,7 +667,7 @@
lemma one_and_eq:
\<open>1 AND a = a mod 2\<close>
- 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:
\<open>a AND 1 = a mod 2\<close>
@@ -676,7 +676,7 @@
lemma one_or_eq:
\<open>1 OR a = a + of_bool (even a)\<close>
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:
\<open>a OR 1 = a + of_bool (even a)\<close>
@@ -685,7 +685,7 @@
lemma one_xor_eq:
\<open>1 XOR a = a + of_bool (even a) - of_bool (odd a)\<close>
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:
\<open>a XOR 1 = a + of_bool (even a) - of_bool (odd a)\<close>
@@ -762,7 +762,7 @@
lemma even_mask_iff:
\<open>even (mask n) \<longleftrightarrow> n = 0\<close>
- 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]:
\<open>mask (Suc 0) = 1\<close>
@@ -770,7 +770,7 @@
lemma mask_Suc_exp:
\<open>mask (Suc n) = 2 ^ n OR mask n\<close>
- by (auto simp add: bit_eq_iff bit_simps)
+ by (auto simp: bit_eq_iff bit_simps)
lemma mask_numeral:
\<open>mask (numeral n) = 1 + 2 * mask (pred_numeral n)\<close>
@@ -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:
\<open>a XOR b = a OR b\<close> if \<open>a AND b = 0\<close>
- 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:
\<open>a + b = a OR b\<close> if \<open>a AND b = 0\<close>
@@ -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: \<open>even a \<or> even b\<close>
- by (auto simp add: bit_0)
+ by (auto simp: bit_0)
have bit: \<open>\<not> bit (a div 2) n \<or> \<not> bit (b div 2) n\<close> for n
using Suc.prems(2) [of \<open>Suc n\<close>] by (simp add: bit_Suc)
from Suc.prems have \<open>possible_bit TYPE('a) n\<close>
@@ -879,7 +878,7 @@
have \<open>a + b = (a div 2 * 2 + a mod 2) + (b div 2 * 2 + b mod 2)\<close>
using div_mult_mod_eq [of a 2] div_mult_mod_eq [of b 2] by simp
also have \<open>\<dots> = of_bool (odd a \<or> odd b) + 2 * (a div 2 + b div 2)\<close>
- using even by (auto simp add: algebra_simps mod2_eq_if)
+ using even by (auto simp: algebra_simps mod2_eq_if)
finally have \<open>bit ((a + b) div 2) n \<longleftrightarrow> bit (a div 2 + b div 2) n\<close>
using \<open>possible_bit TYPE('a) (Suc n)\<close> by simp (simp_all flip: bit_Suc add: bit_double_iff possible_bit_def)
also have \<open>\<dots> \<longleftrightarrow> bit (a div 2 OR b div 2) n\<close>
@@ -929,9 +928,9 @@
also have \<open>\<dots> \<longleftrightarrow> m \<le> n \<and> bit a n \<or> n < m \<and> bit a n\<close>
by auto
also have \<open>m \<le> n \<and> bit a n \<longleftrightarrow> bit (push_bit m (drop_bit m a)) n\<close>
- 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:
\<open>push_bit m (take_bit n a) = take_bit (m + n) (push_bit m a)\<close>
- by (rule bit_eqI) (auto simp add: bit_simps)
+ by (rule bit_eqI) (auto simp: bit_simps)
lemma take_bit_push_bit:
\<open>take_bit m (push_bit n a) = push_bit n (take_bit (m - n) a)\<close>
- by (rule bit_eqI) (auto simp add: bit_simps)
+ by (rule bit_eqI) (auto simp: bit_simps)
lemma take_bit_drop_bit:
\<open>take_bit m (drop_bit n a) = drop_bit n (take_bit (m + n) a)\<close>
- by (rule bit_eqI) (auto simp add: bit_simps)
+ by (rule bit_eqI) (auto simp: bit_simps)
lemma drop_bit_take_bit:
\<open>drop_bit m (take_bit n a) = take_bit (n - m) (drop_bit m a)\<close>
- by (rule bit_eqI) (auto simp add: bit_simps)
+ by (rule bit_eqI) (auto simp: bit_simps)
lemma even_push_bit_iff [simp]:
\<open>even (push_bit n a) \<longleftrightarrow> n \<noteq> 0 \<or> even a\<close>
@@ -1091,49 +1090,49 @@
then have \<open> \<not> bit a (n + (m - n))\<close>
by (simp add: bit_simps)
then show \<open>bit (take_bit n a) m \<longleftrightarrow> bit a m\<close>
- by (cases \<open>m < n\<close>) (auto simp add: bit_simps)
+ by (cases \<open>m < n\<close>) (auto simp: bit_simps)
qed
qed
lemma drop_bit_exp_eq:
\<open>drop_bit m (2 ^ n) = of_bool (m \<le> n \<and> possible_bit TYPE('a) n) * 2 ^ (n - m)\<close>
- by (auto simp add: bit_eq_iff bit_simps)
+ by (auto simp: bit_eq_iff bit_simps)
lemma take_bit_and [simp]:
\<open>take_bit n (a AND b) = take_bit n a AND take_bit n b\<close>
- by (auto simp add: bit_eq_iff bit_simps)
+ by (auto simp: bit_eq_iff bit_simps)
lemma take_bit_or [simp]:
\<open>take_bit n (a OR b) = take_bit n a OR take_bit n b\<close>
- by (auto simp add: bit_eq_iff bit_simps)
+ by (auto simp: bit_eq_iff bit_simps)
lemma take_bit_xor [simp]:
\<open>take_bit n (a XOR b) = take_bit n a XOR take_bit n b\<close>
- by (auto simp add: bit_eq_iff bit_simps)
+ by (auto simp: bit_eq_iff bit_simps)
lemma push_bit_and [simp]:
\<open>push_bit n (a AND b) = push_bit n a AND push_bit n b\<close>
- by (auto simp add: bit_eq_iff bit_simps)
+ by (auto simp: bit_eq_iff bit_simps)
lemma push_bit_or [simp]:
\<open>push_bit n (a OR b) = push_bit n a OR push_bit n b\<close>
- by (auto simp add: bit_eq_iff bit_simps)
+ by (auto simp: bit_eq_iff bit_simps)
lemma push_bit_xor [simp]:
\<open>push_bit n (a XOR b) = push_bit n a XOR push_bit n b\<close>
- by (auto simp add: bit_eq_iff bit_simps)
+ by (auto simp: bit_eq_iff bit_simps)
lemma drop_bit_and [simp]:
\<open>drop_bit n (a AND b) = drop_bit n a AND drop_bit n b\<close>
- by (auto simp add: bit_eq_iff bit_simps)
+ by (auto simp: bit_eq_iff bit_simps)
lemma drop_bit_or [simp]:
\<open>drop_bit n (a OR b) = drop_bit n a OR drop_bit n b\<close>
- by (auto simp add: bit_eq_iff bit_simps)
+ by (auto simp: bit_eq_iff bit_simps)
lemma drop_bit_xor [simp]:
\<open>drop_bit n (a XOR b) = drop_bit n a XOR drop_bit n b\<close>
- by (auto simp add: bit_eq_iff bit_simps)
+ by (auto simp: bit_eq_iff bit_simps)
lemma take_bit_of_mask [simp]:
\<open>take_bit m (mask n) = mask (min m n)\<close>
@@ -1141,11 +1140,11 @@
lemma take_bit_eq_mask:
\<open>take_bit n a = a AND mask n\<close>
- by (auto simp add: bit_eq_iff bit_simps)
+ by (auto simp: bit_eq_iff bit_simps)
lemma or_eq_0_iff:
\<open>a OR b = 0 \<longleftrightarrow> a = 0 \<and> b = 0\<close>
- 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:
\<open>bit a n \<longleftrightarrow> drop_bit n a AND 1 = 1\<close>
@@ -1157,23 +1156,23 @@
lemma bit_set_bit_iff [bit_simps]:
\<open>bit (set_bit m a) n \<longleftrightarrow> bit a n \<or> (m = n \<and> possible_bit TYPE('a) n)\<close>
- 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:
\<open>even (set_bit m a) \<longleftrightarrow> even a \<and> m \<noteq> 0\<close>
- 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]:
\<open>bit (unset_bit m a) n \<longleftrightarrow> bit a n \<and> m \<noteq> n\<close>
- 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:
\<open>even (unset_bit m a) \<longleftrightarrow> even a \<or> m = 0\<close>
- 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]:
\<open>bit (flip_bit m a) n \<longleftrightarrow> (m = n \<longleftrightarrow> \<not> bit a n) \<and> possible_bit TYPE('a) n\<close>
- 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:
\<open>even (flip_bit m a) \<longleftrightarrow> \<not> (even a \<longleftrightarrow> m = 0)\<close>
@@ -1182,7 +1181,7 @@
lemma and_exp_eq_0_iff_not_bit:
\<open>a AND 2 ^ n = 0 \<longleftrightarrow> \<not> bit a n\<close> (is \<open>?P \<longleftrightarrow> ?Q\<close>)
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: \<open>\<forall>j. \<not> bit a (Suc j)\<close>
@@ -1191,52 +1190,52 @@
from a have \<open>n = 0\<close> if \<open>bit a n\<close> for n using that
by (cases n) simp_all
then have \<open>a = 0 \<or> a = 1\<close>
- 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]:
\<open>set_bit 0 a = 1 + 2 * (a div 2)\<close>
- 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:
\<open>set_bit (Suc n) a = a mod 2 + 2 * set_bit n (a div 2)\<close>
- 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]:
\<open>unset_bit 0 a = 2 * (a div 2)\<close>
- 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:
\<open>unset_bit (Suc n) a = a mod 2 + 2 * unset_bit n (a div 2)\<close>
- 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]:
\<open>flip_bit 0 a = of_bool (even a) + 2 * (a div 2)\<close>
- 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:
\<open>flip_bit (Suc n) a = a mod 2 + 2 * flip_bit n (a div 2)\<close>
- 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:
\<open>flip_bit n a = (if bit a n then unset_bit else set_bit) n a\<close>
- 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:
\<open>take_bit n (set_bit m a) = (if n \<le> m then take_bit n a else set_bit m (take_bit n a))\<close>
- 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:
\<open>take_bit n (unset_bit m a) = (if n \<le> m then take_bit n a else unset_bit m (take_bit n a))\<close>
- 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:
\<open>take_bit n (flip_bit m a) = (if n \<le> m then take_bit n a else flip_bit m (take_bit n a))\<close>
- 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]:
\<open>bit 1 0\<close>
@@ -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:
\<open>horner_sum of_bool 2 (map (bit a) [0..<n]) = take_bit n a\<close>
- by (rule bit_eqI) (auto simp add: bit_simps)
+ by (rule bit_eqI) (auto simp: bit_simps)
lemma take_bit_horner_sum_bit_eq:
\<open>take_bit n (horner_sum of_bool 2 bs) = horner_sum of_bool 2 (take n bs)\<close>
- 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:
\<open>take_bit n a = (\<Sum>k = 0..<n. push_bit k (of_bool (bit a k)))\<close>
@@ -1292,9 +1291,9 @@
\<open>set_bit n a = a + of_bool (\<not> bit a n) * 2 ^ n\<close>
proof -
have \<open>a AND of_bool (\<not> bit a n) * 2 ^ n = 0\<close>
- 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]:
\<open>bit (NOT (2 ^ m)) n \<longleftrightarrow> possible_bit TYPE('a) n \<and> n \<noteq> m\<close>
- 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]:
\<open>bit (- a) n \<longleftrightarrow> possible_bit TYPE('a) n \<and> \<not> bit (a - 1) n\<close>
@@ -1372,7 +1371,7 @@
lemma bit_minus_exp_iff [bit_simps]:
\<open>bit (- (2 ^ m)) n \<longleftrightarrow> possible_bit TYPE('a) n \<and> n \<ge> m\<close>
- 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]:
\<open>bit (- 2) n \<longleftrightarrow> possible_bit TYPE('a) n \<and> n > 0\<close>
@@ -1394,13 +1393,13 @@
by standard (rule bit_eqI, simp add: bit_and_iff)
sublocale bit: abstract_boolean_algebra \<open>(AND)\<close> \<open>(OR)\<close> NOT 0 \<open>- 1\<close>
- 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 \<open>(AND)\<close> \<open>(OR)\<close> NOT 0 \<open>- 1\<close> \<open>(XOR)\<close>
- apply standard
- apply (rule bit_eqI)
- apply (auto simp add: bit_simps)
- done
+proof
+ show \<open>\<And>x y. x XOR y = x AND NOT y OR NOT x AND y\<close>
+ by (intro bit_eqI) (auto simp: bit_simps)
+qed
lemma and_eq_not_not_or:
\<open>a AND b = NOT (NOT a OR NOT b)\<close>
@@ -1424,7 +1423,7 @@
lemma disjunctive_and_not_eq_xor:
\<open>a AND NOT b = a XOR b\<close> if \<open>NOT a AND b = 0\<close>
- 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:
\<open>a - b = a AND NOT b\<close> if \<open>NOT a AND b = 0\<close>
@@ -1447,11 +1446,11 @@
lemma take_bit_not_take_bit:
\<open>take_bit n (NOT (take_bit n a)) = take_bit n (NOT a)\<close>
- 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:
\<open>take_bit n (NOT a) = take_bit n (NOT b) \<longleftrightarrow> take_bit n a = take_bit n b\<close>
- by (auto simp add: bit_eq_iff bit_simps)
+ by (auto simp: bit_eq_iff bit_simps)
lemma take_bit_not_eq_mask_diff:
\<open>take_bit n (NOT a) = mask n - take_bit n a\<close>
@@ -1459,7 +1458,7 @@
have \<open>NOT (mask n) AND take_bit n a = 0\<close>
by (simp add: bit_eq_iff bit_simps)
moreover have \<open>take_bit n (NOT a) = mask n AND NOT (take_bit n a)\<close>
- 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:
\<open>unset_bit n a = a AND NOT (push_bit n 1)\<close>
- by (rule bit_eqI) (auto simp add: bit_simps)
+ by (rule bit_eqI) (auto simp: bit_simps)
lemma push_bit_Suc_minus_numeral [simp]:
\<open>push_bit (Suc n) (- numeral k) = push_bit n (- numeral (Num.Bit0 k))\<close>
- 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]:
\<open>push_bit (numeral l) (- numeral k) = push_bit (pred_numeral l) (- numeral (Num.Bit0 k))\<close>
@@ -1509,11 +1505,11 @@
lemma push_bit_mask_eq:
\<open>push_bit m (mask n) = mask (n + m) AND NOT (mask m)\<close>
- 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:
\<open>push_bit n (take_bit m (drop_bit n a)) = a AND mask (m + n) AND NOT (mask n)\<close>
- by (rule bit_eqI) (auto simp add: bit_simps)
+ by (rule bit_eqI) (auto simp: bit_simps)
lemma push_bit_numeral_minus_1 [simp]:
\<open>push_bit (numeral n) (- 1) = - (2 ^ numeral n)\<close>
@@ -1523,9 +1519,9 @@
\<open>unset_bit n a = a - of_bool (bit a n) * 2 ^ n\<close>
proof -
have \<open>NOT a AND of_bool (bit a n) * 2 ^ n = 0\<close>
- by (auto simp add: bit_eq_iff bit_simps)
+ by (auto simp: bit_eq_iff bit_simps)
moreover have \<open>unset_bit n a = a AND NOT (of_bool (bit a n) * 2 ^ n)\<close>
- 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:
\<open>drop_bit m (mask n) = mask (n - m)\<close>
- 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':
\<open>bit (push_bit m a) n \<longleftrightarrow> m \<le> n \<and> bit a (n - m)\<close>
@@ -1645,7 +1641,7 @@
proof (rule ccontr)
assume \<open>\<not> 0 < take_bit m a\<close>
then have \<open>take_bit m a = 0\<close>
- by (auto simp add: not_less intro: order_antisym)
+ by (auto simp: not_less intro: order_antisym)
then have \<open>bit (take_bit m a) n = bit 0 n\<close>
by simp
with that show False
@@ -1659,7 +1655,7 @@
lemma drop_bit_push_bit:
\<open>drop_bit m (push_bit n a) = drop_bit (m - n) (push_bit (n - m) a)\<close>
by (cases \<open>m \<le> n\<close>)
- (auto simp add: mult.left_commute [of _ \<open>2 ^ n\<close>] mult.commute [of _ \<open>2 ^ n\<close>] mult.assoc
+ (auto simp: mult.left_commute [of _ \<open>2 ^ n\<close>] mult.commute [of _ \<open>2 ^ n\<close>] 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: \<open>\<bar>k div 2\<bar> \<le> \<bar>k\<bar>\<close> for k :: int
by (cases k) (simp_all add: divide_int_def nat_add_distrib)
then have less: \<open>\<bar>k div 2\<bar> < \<bar>k\<bar>\<close> if \<open>k \<notin> {0, - 1}\<close> for k :: int
- using that by (auto simp add: less_le [of k])
+ using that by (auto simp: less_le [of k])
show \<open>wf (measure (\<lambda>(k, l). nat (\<bar>k\<bar> + \<bar>l\<bar>)))\<close>
by simp
show \<open>((k div 2, l div 2), k, l) \<in> measure (\<lambda>(k, l). nat (\<bar>k\<bar> + \<bar>l\<bar>))\<close>
@@ -1721,11 +1717,11 @@
proof (cases \<open>k \<in> {0, - 1} \<and> l \<in> {0, - 1}\<close>)
case True
then show ?thesis
- by (auto simp add: F.simps [of 0] F.simps [of \<open>- 1\<close>])
+ by (auto simp: F.simps [of 0] F.simps [of \<open>- 1\<close>])
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 \<open>unset_bit n k = (k OR push_bit n 1) XOR push_bit n 1\<close>
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 \<open>of_int k\<close> 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 \<open>of_int k\<close> 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 \<open>1 + k * 2\<close> 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]:
\<open>k XOR l < 0 \<longleftrightarrow> (k < 0) \<noteq> (l < 0)\<close> 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>\<open>contributor \<open>Stefan Berghofer\<close>\<close>
\<open>x OR y < 2 ^ n\<close> if \<open>0 \<le> x\<close> \<open>x < 2 ^ n\<close> \<open>y < 2 ^ n\<close> for x y :: int
@@ -2034,12 +2030,12 @@
case (even x)
from even.IH [of \<open>n - 1\<close> \<open>y div 2\<close>] even.prems even.hyps
show ?case
- by (cases n) (auto simp add: or_int.rec [of \<open>_ * 2\<close>] elim: oddE)
+ by (cases n) (auto simp: or_int.rec [of \<open>_ * 2\<close>] elim: oddE)
next
case (odd x)
from odd.IH [of \<open>n - 1\<close> \<open>y div 2\<close>] odd.prems odd.hyps
show ?case
- by (cases n) (auto simp add: or_int.rec [of \<open>1 + _ * 2\<close>], linarith)
+ by (cases n) (auto simp: or_int.rec [of \<open>1 + _ * 2\<close>], linarith)
qed
lemma XOR_upper: \<^marker>\<open>contributor \<open>Stefan Berghofer\<close>\<close>
@@ -2056,12 +2052,12 @@
case (even x)
from even.IH [of \<open>n - 1\<close> \<open>y div 2\<close>] even.prems even.hyps
show ?case
- by (cases n) (auto simp add: xor_int.rec [of \<open>_ * 2\<close>] elim: oddE)
+ by (cases n) (auto simp: xor_int.rec [of \<open>_ * 2\<close>] elim: oddE)
next
case (odd x)
from odd.IH [of \<open>n - 1\<close> \<open>y div 2\<close>] odd.prems odd.hyps
show ?case
- by (cases n) (auto simp add: xor_int.rec [of \<open>1 + _ * 2\<close>])
+ by (cases n) (auto simp: xor_int.rec [of \<open>1 + _ * 2\<close>])
qed
lemma AND_lower [simp]: \<^marker>\<open>contributor \<open>Stefan Berghofer\<close>\<close>
@@ -2120,12 +2116,12 @@
case (even x)
from even.IH [of \<open>y div 2\<close>]
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 \<open>y div 2\<close>]
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]:
\<open>drop_bit n k \<ge> 0 \<longleftrightarrow> k \<ge> 0\<close> 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]:
\<open>drop_bit n k < 0 \<longleftrightarrow> k < 0\<close> for k :: int
@@ -2223,17 +2219,17 @@
lemma and_int_unfold:
\<open>k AND l = (if k = 0 \<or> 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)))\<close> 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:
\<open>k OR l = (if k = - 1 \<or> 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)))\<close> 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:
\<open>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 \<bar>k mod 2 - l mod 2\<bar> + 2 * ((k div 2) XOR (l div 2)))\<close> 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:
\<open>bit (- k) n \<longleftrightarrow> bit (NOT (k - 1)) n\<close> for k :: int
@@ -2325,7 +2321,7 @@
lemma take_bit_int_less_self_iff:
\<open>take_bit n k < k \<longleftrightarrow> 2 ^ n \<le> k\<close> 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 \<open>2 ^ n\<close> k])
lemma take_bit_int_greater_self_iff:
@@ -2334,7 +2330,7 @@
lemma take_bit_int_greater_eq_self_iff:
\<open>k \<le> take_bit n k \<longleftrightarrow> k < 2 ^ n\<close> 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 \<open>2 ^ n\<close>])
lemma take_bit_tightened_less_eq_int:
@@ -2370,7 +2366,7 @@
fix m
assume \<open>nat k \<le> m\<close>
then show \<open>bit k m \<longleftrightarrow> bit k (nat k)\<close>
- 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 \<open>nat (- k) \<le> m\<close>
then show \<open>bit k m \<longleftrightarrow> bit k (nat (- k))\<close>
- 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 \<open>finite N\<close> \<open>r \<in> N\<close>
using ** N_def \<open>r < q\<close> by auto
moreover define n where \<open>n = Suc (Max N)\<close>
- ultimately have \<open>\<And>m. n \<le> m \<Longrightarrow> bit k m \<longleftrightarrow> bit k n\<close>
- apply auto
- apply (metis (full_types, lifting) "*" Max_ge_iff Suc_n_not_le_n \<open>finite N\<close> all_not_in_conv mem_Collect_eq not_le)
- apply (metis "*" Max_ge Suc_n_not_le_n \<open>finite N\<close> linorder_not_less mem_Collect_eq)
- apply (metis "*" Max_ge Suc_n_not_le_n \<open>finite N\<close> linorder_not_less mem_Collect_eq)
- apply (metis (full_types, lifting) "*" Max_ge_iff Suc_n_not_le_n \<open>finite N\<close> all_not_in_conv mem_Collect_eq not_le)
- done
+ ultimately have \<dagger>: \<open>\<And>m. n \<le> m \<Longrightarrow> bit k m \<longleftrightarrow> bit k n\<close>
+ by (smt (verit) "*" Max_ge Suc_n_not_le_n linorder_not_less mem_Collect_eq not_less_eq_eq)
have \<open>bit k (Max N) \<noteq> bit k n\<close>
by (metis (mono_tags, lifting) "*" Max_in N_def \<open>\<And>m. n \<le> m \<Longrightarrow> bit k m = bit k n\<close> \<open>finite N\<close> \<open>r \<in> N\<close> empty_iff le_cases mem_Collect_eq)
- show thesis apply (rule that [of n])
- using \<open>\<And>m. n \<le> m \<Longrightarrow> bit k m = bit k n\<close> apply blast
- using \<open>bit k (Max N) \<noteq> bit k n\<close> n_def by auto
+ with \<dagger> n_def that [of n] show thesis
+ by fastforce
qed
qed
@@ -2591,17 +2581,17 @@
lemma and_nat_unfold [code]:
\<open>m AND n = (if m = 0 \<or> n = 0 then 0 else (m mod 2) * (n mod 2) + 2 * ((m div 2) AND (n div 2)))\<close>
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]:
\<open>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)))\<close> 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]:
\<open>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)))\<close> 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]:
\<open>unset_bit 0 m = 2 * (m div 2)\<close>
@@ -2680,10 +2670,11 @@
lemma drop_bit_nat_eq:
\<open>drop_bit n (nat k) = nat (drop_bit n k)\<close>
- apply (cases \<open>k \<ge> 0\<close>)
- 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 \<open>k \<ge> 0\<close>)
+ 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:
\<open>take_bit n (nat k) = nat (take_bit n k)\<close> if \<open>k \<ge> 0\<close>
@@ -2932,7 +2923,7 @@
\<open>numeral (Num.Bit1 m) AND NOT (1 :: int) = numeral (Num.Bit0 m)\<close>
\<open>numeral (Num.Bit1 m) AND NOT (numeral (Num.Bit0 n)) = 1 + (2 :: int) * (numeral m AND NOT (numeral n))\<close>
\<open>numeral (Num.Bit1 m) AND NOT (numeral (Num.Bit1 n)) = (2 :: int) * (numeral m AND NOT (numeral n))\<close>
- 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 :: \<open>num \<Rightarrow> num \<Rightarrow> num option\<close> \<^marker>\<open>contributor \<open>Andreas Lochbihler\<close>\<close>
where
@@ -2989,7 +2980,7 @@
\<open>numeral (Num.Bit1 m) OR NOT (numeral (Num.Bit0 n)) = 1 + (2 :: int) * (numeral m OR NOT (numeral n))\<close>
\<open>numeral (Num.Bit1 m) OR NOT (numeral (Num.Bit1 n)) = 1 + (2 :: int) * (numeral m OR NOT (numeral n))\<close>
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 :: \<open>num \<Rightarrow> num \<Rightarrow> num\<close> \<^marker>\<open>contributor \<open>Andreas Lochbihler\<close>\<close>
where
@@ -3055,7 +3046,7 @@
(case take_bit_num (pred_numeral r) m of None \<Rightarrow> None | Some q \<Rightarrow> Some (Num.Bit0 q))\<close>
\<open>take_bit_num (numeral r) (Num.Bit1 m) =
Some (case take_bit_num (pred_numeral r) m of None \<Rightarrow> Num.One | Some q \<Rightarrow> Num.Bit1 q)\<close>
- 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 @@
\<open>take_bit m (numeral n) = numeral q\<close> if \<open>take_bit_num m n = Some q\<close>
proof -
from that have \<open>take_bit m (numeral n :: nat) = numeral q\<close>
- 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 \<open>of_nat (take_bit m (numeral n)) = of_nat (numeral q)\<close>
by simp
then show ?thesis
@@ -3193,7 +3184,7 @@
\<open>Int.Neg num.One AND Int.Pos m = Int.Pos m\<close>
\<open>Int.Neg (num.Bit0 n) AND Int.Pos m = Num.sub (or_not_num_neg (Num.BitM n) m) num.One\<close>
\<open>Int.Neg (num.Bit1 n) AND Int.Pos m = Num.sub (or_not_num_neg (num.Bit0 n) m) num.One\<close>
- 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 @@
\<open>Int.Neg num.One OR Int.Pos m = Int.Neg num.One\<close>
\<open>Int.Neg (num.Bit0 n) OR Int.Pos m = (case and_not_num (Num.BitM n) m of None \<Rightarrow> -1 | Some n' \<Rightarrow> Int.Neg (Num.inc n'))\<close>
\<open>Int.Neg (num.Bit1 n) OR Int.Pos m = (case and_not_num (num.Bit0 n) m of None \<Rightarrow> -1 | Some n' \<Rightarrow> Int.Neg (Num.inc n'))\<close>
- 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:
\<open>concat_bit n k (concat_bit m l r) = concat_bit (m + n) (concat_bit n k l) r\<close>
- 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:
\<open>concat_bit m (concat_bit n k l) r = concat_bit (min m n) k (concat_bit (m - n) l r)\<close>
- 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:
\<open>concat_bit n k l = concat_bit n r s
@@ -3394,14 +3385,14 @@
fix m
from * [of m]
show \<open>bit (take_bit n k) m \<longleftrightarrow> bit (take_bit n r) m\<close>
- 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 \<open>push_bit n l = push_bit n s\<close>
proof (rule bit_eqI)
fix m
from * [of m]
show \<open>bit (push_bit n l) m \<longleftrightarrow> bit (push_bit n s) m\<close>
- 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 \<open>l = s\<close>
by (simp add: push_bit_eq_mult)
@@ -3412,7 +3403,7 @@
lemma take_bit_concat_bit_eq:
\<open>take_bit m (concat_bit n k l) = concat_bit (min m n) k (take_bit (m - n) l)\<close>
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:
\<open>concat_bit n (take_bit n b) = concat_bit n b\<close>
@@ -3437,7 +3428,7 @@
lemma even_signed_take_bit_iff:
\<open>even (signed_take_bit m a) \<longleftrightarrow> even a\<close>
- 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]:
\<open>bit (signed_take_bit m a) n \<longleftrightarrow> possible_bit TYPE('a) n \<and> bit a (min m n)\<close>
@@ -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]:
\<open>signed_take_bit m (signed_take_bit n a) = signed_take_bit (min m n) a\<close>
- 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:
\<open>signed_take_bit m (take_bit n a) = (if n \<le> m then take_bit n else signed_take_bit m) a\<close>
- 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:
\<open>take_bit m (signed_take_bit n a) = take_bit m a\<close> if \<open>m \<le> Suc n\<close>
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:
\<open>signed_take_bit n k = take_bit (Suc n) k + NOT (mask (Suc n)) * of_bool (bit k n)\<close>
@@ -3504,7 +3495,7 @@
next
case True
have \<open>signed_take_bit n k = take_bit (Suc n) k OR NOT (mask (Suc n))\<close>
- 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 \<open>\<dots> = take_bit (Suc n) k + NOT (mask (Suc n))\<close>
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:
\<open>signed_take_bit n k = k \<longleftrightarrow> - (2 ^ n) \<le> k \<and> k < 2 ^ n\<close>
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:
\<open>signed_take_bit n k = k\<close> if \<open>- (2 ^ n) \<le> k\<close> \<open>k < 2 ^ n\<close>
@@ -3782,9 +3773,8 @@
lemma exp_div_exp_eq:
\<open>2 ^ m div 2 ^ n = of_bool (2 ^ m \<noteq> 0 \<and> m \<ge> n) * 2 ^ (m - n)\<close>
- 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:
\<open>1 div 2 = 0\<close>
@@ -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: \<open>even a \<or> even b\<close>
- by (auto simp add: bit_0)
+ by (auto simp: bit_0)
have bit: \<open>\<not> bit (a div 2) n \<or> \<not> bit (b div 2) n\<close> for n
using Suc.prems(1) [of \<open>Suc n\<close>] by (simp add: bit_Suc)
from Suc.prems(2) have \<open>possible_bit TYPE('a) (Suc n)\<close> \<open>possible_bit TYPE('a) n\<close>
@@ -3867,7 +3857,7 @@
have \<open>a + b = (a div 2 * 2 + a mod 2) + (b div 2 * 2 + b mod 2)\<close>
using div_mult_mod_eq [of a 2] div_mult_mod_eq [of b 2] by simp
also have \<open>\<dots> = of_bool (odd a \<or> odd b) + 2 * (a div 2 + b div 2)\<close>
- using even by (auto simp add: algebra_simps mod2_eq_if)
+ using even by (auto simp: algebra_simps mod2_eq_if)
finally have \<open>bit ((a + b) div 2) n \<longleftrightarrow> bit (a div 2 + b div 2) n\<close>
using \<open>possible_bit TYPE('a) (Suc n)\<close> by simp (simp_all flip: bit_Suc add: bit_double_iff possible_bit_def)
also have \<open>\<dots> \<longleftrightarrow> bit (a div 2) n \<or> bit (b div 2) n\<close>
@@ -3884,7 +3874,7 @@
lemma even_mask_div_iff:
\<open>even ((2 ^ m - 1) div 2 ^ n) \<longleftrightarrow> 2 ^ n = 0 \<or> m \<le> n\<close>
- 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:
\<open>a mod 2 ^ m mod 2 ^ n = a mod 2 ^ min m n\<close>
@@ -3920,7 +3910,7 @@
lemma even_mod_exp_div_exp_iff:
\<open>even (a mod 2 ^ m div 2 ^ n) \<longleftrightarrow> m \<le> n \<or> even (a div 2 ^ n)\<close>
- 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 @@
\<open>a - b = a AND NOT b\<close> if \<open>\<And>n. bit b n \<Longrightarrow> bit a n\<close>
proof -
have \<open>NOT a + b = NOT a OR b\<close>
- 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 \<open>NOT (NOT a + b) = NOT (NOT a OR b)\<close>
by simp
then show ?thesis
--- 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 \<le> length xs \<Longrightarrow> k \<le> length ys \<Longrightarrow>
(\<And>i. i < k \<longrightarrow> xs!i = ys!i) \<Longrightarrow> 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:
"\<lbrakk>length xs = length ys; \<And>i. i < length xs \<Longrightarrow> xs!i = ys!i\<rbrakk> \<Longrightarrow> xs = ys"
@@ -3712,7 +3707,7 @@
lemma nth_eq_iff_index_eq:
"\<lbrakk> distinct xs; i < length xs; j < length xs \<rbrakk> \<Longrightarrow> (xs!i = xs!j) = (i = j)"
-by(auto simp: distinct_conv_nth)
+ by(auto simp: distinct_conv_nth)
lemma distinct_Ex1:
"distinct xs \<Longrightarrow> x \<in> set xs \<Longrightarrow> (\<exists>!i. i < length xs \<and> xs ! i = x)"
@@ -3733,9 +3728,7 @@
lemma distinct_swap[simp]: "\<lbrakk> i < size xs; j < size xs\<rbrakk> \<Longrightarrow>
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]:
"\<lbrakk> i < size xs; j < size xs \<rbrakk> \<Longrightarrow> 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) \<and>
(\<forall>ys. ys \<in> set xs \<longrightarrow> distinct ys) \<and>
(\<forall>ys zs. ys \<in> set xs \<and> zs \<in> set xs \<and> ys \<noteq> zs \<longrightarrow> set ys \<inter> 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 "\<lbrakk>set a \<inter> \<Union> (set ` set xs) = {}; a \<in> set xs\<rbrakk> \<Longrightarrow> a=[]"
+ by (metis Int_iff UN_I empty_iff equals0I set_empty)
+ then show ?case
+ by (auto simp: Cons)
+qed
subsubsection \<open>\<^const>\<open>replicate\<close>\<close>
@@ -4535,24 +4535,24 @@
qed
lemma Ex_list_of_length: "\<exists>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 (\<lambda> 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\<open>Courtesy of Matthias Daum:\<close>
lemma append_replicate_commute:
@@ -4899,10 +4899,7 @@
lemma nth_rotate:
\<open>rotate m xs ! n = xs ! ((m + n) mod length xs)\<close> if \<open>n < length xs\<close>
- 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:
\<open>rotate1 xs ! n = xs ! (Suc n mod length xs)\<close> if \<open>n < length xs\<close>
@@ -4944,10 +4941,8 @@
by (auto simp add: nths_def)
lemma nths_all: "\<forall>i < length xs. i \<in> I \<Longrightarrow> 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 \<and> i \<in> I}"
@@ -5343,8 +5338,7 @@
show ?thesis
unfolding transpose.simps \<open>i = Suc j\<close> 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) \<in> ?L (Suc n)" if r: "(xs,ys) \<in> ?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) \<in> ?L (Suc n) \<Longrightarrow> (xs,ys) \<in> ?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) \<in> lexord r \<longleftrightarrow> (\<exists>x \<in> set xs. (x,x) \<in> r) \<or> (ys, zs) \<in> lexord r"
-by(induction xs) auto
+ by(induction xs) auto
lemma lexord_same_pref_if_irrefl[simp]:
"irrefl r \<Longrightarrow> (xs @ ys, xs @ zs) \<in> lexord r \<longleftrightarrow> (ys, zs) \<in> lexord r"
-by (simp add: irrefl_def lexord_same_pref_iff)
+ by (simp add: irrefl_def lexord_same_pref_iff)
lemma lexord_append_rightI: "\<exists> b z. y = b # z \<Longrightarrow> (x, x @ y) \<in> 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) \<in> r \<Longrightarrow> (u @ a # x, u @ b # y) \<in> lexord r"
-by (simp add: lexord_same_pref_iff)
+ by (simp add: lexord_same_pref_iff)
lemma lexord_append_leftI: "(u,v) \<in> lexord r \<Longrightarrow> (x @ u, x @ v) \<in> lexord r"
-by (simp add: lexord_same_pref_iff)
+ by (simp add: lexord_same_pref_iff)
lemma lexord_append_leftD:
"\<lbrakk>(x @ u, x @ v) \<in> lexord r; (\<forall>a. (a,a) \<notin> r) \<rbrakk> \<Longrightarrow> (u,v) \<in> lexord r"
-by (simp add: lexord_same_pref_iff)
+ by (simp add: lexord_same_pref_iff)
lemma lexord_take_index_conv:
"((x,y) \<in> lexord r) =
@@ -6897,9 +6886,13 @@
moreover
have "(\<exists>u a b. (a, b) \<in> r \<and> (\<exists>v. x = u @ a # v) \<and> (\<exists>w. y = u @ b # w)) =
(\<exists>i<length x. i < length y \<and> take i x = take i y \<and> (x ! i, y ! i) \<in> r)"
- apply safe
- using less_iff_Suc_add apply auto[1]
- by (metis id_take_nth_drop)
+ (is "?L=?R")
+ proof
+ show "?L\<Longrightarrow>?R"
+ by (metis append_eq_conv_conj drop_all leI list.simps(3) nth_append_length)
+ show "?R\<Longrightarrow>?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 \<noteq> Nil \<Longrightarrow> 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 \<Longrightarrow> 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 \<Longrightarrow> lexordp (xs @ us) (xs @ vs)"
-by(induct xs) auto
+ by(induct xs) auto
lemma lexordp_append_leftD: "\<lbrakk> lexordp (xs @ us) (xs @ vs); \<forall>a. \<not> a < a \<rbrakk> \<Longrightarrow> lexordp us vs"
-by(induct xs) auto
+ by(induct xs) auto
lemma lexordp_irreflexive:
assumes irrefl: "\<forall>x. \<not> 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) \<in> measures [] = False"
"(x, y) \<in> measures (f # fs)
= (f x < f y \<or> (f x = f y \<and> (x, y) \<in> measures fs))"
-unfolding measures_def
-by auto
+ unfolding measures_def
+ by auto
lemma measures_less: "f x < f y \<Longrightarrow> (x, y) \<in> measures (f#fs)"
-by simp
+ by simp
lemma measures_lesseq: "f x \<le> f y \<Longrightarrow> (x, y) \<in> measures fs \<Longrightarrow> (x, y) \<in> measures (f#fs)"
-by auto
+ by auto
subsubsection \<open>Lifting Relations to Lists: one element\<close>
@@ -7286,27 +7279,27 @@
unfolding listrel1_def by auto
lemma not_Nil_listrel1 [iff]: "([], xs) \<notin> listrel1 r"
-unfolding listrel1_def by blast
+ unfolding listrel1_def by blast
lemma not_listrel1_Nil [iff]: "(xs, []) \<notin> listrel1 r"
-unfolding listrel1_def by blast
+ unfolding listrel1_def by blast
lemma Cons_listrel1_Cons [iff]:
"(x # xs, y # ys) \<in> listrel1 r \<longleftrightarrow>
(x,y) \<in> r \<and> xs = ys \<or> x = y \<and> (xs, ys) \<in> 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) \<in> r \<Longrightarrow> (x # xs, y # xs) \<in> listrel1 r"
-by fast
+ by fast
lemma listrel1I2: "(xs, ys) \<in> listrel1 r \<Longrightarrow> (x # xs, x # ys) \<in> listrel1 r"
-by fast
+ by fast
lemma append_listrel1I:
"(xs, ys) \<in> listrel1 r \<and> us = vs \<or> xs = ys \<and> (us, vs) \<in> listrel1 r
\<Longrightarrow> (xs @ us, ys @ vs) \<in> 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) \<in> listrel1 r"
@@ -7333,19 +7326,19 @@
qed
lemma listrel1_eq_len: "(xs,ys) \<in> listrel1 r \<Longrightarrow> length xs = length ys"
-unfolding listrel1_def by auto
+ unfolding listrel1_def by auto
lemma listrel1_mono:
"r \<subseteq> s \<Longrightarrow> listrel1 r \<subseteq> listrel1 s"
-unfolding listrel1_def by blast
+ unfolding listrel1_def by blast
lemma listrel1_converse: "listrel1 (r\<inverse>) = (listrel1 r)\<inverse>"
-unfolding listrel1_def by blast
+ unfolding listrel1_def by blast
lemma in_listrel1_converse:
"(x,y) \<in> listrel1 (r\<inverse>) \<longleftrightarrow> (x,y) \<in> (listrel1 r)\<inverse>"
-unfolding listrel1_def by blast
+ unfolding listrel1_def by blast
lemma listrel1_iff_update:
"(xs,ys) \<in> (listrel1 r)
@@ -7618,19 +7611,19 @@
stack overflow in some target languages.\<close>
fun map_tailrec_rev :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> '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 \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list" where
-"map_tailrec f as = rev (map_tailrec_rev f as [])"
+ "map_tailrec f as = rev (map_tailrec_rev f as [])"
text\<open>Code equation:\<close>
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 \<open>Counterparts for set-related operations\<close>
@@ -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"