--- a/src/HOL/Groups_List.thy Mon Nov 16 21:36:07 2020 +0000
+++ b/src/HOL/Groups_List.thy Mon Nov 16 21:37:32 2020 +0000
@@ -395,6 +395,12 @@
by (simp add: horner_sum_eq_sum_funpow ac_simps)
qed
+lemma horner_sum_append:
+ \<open>horner_sum f a (xs @ ys) = horner_sum f a xs + a ^ length xs * horner_sum f a ys\<close>
+ using sum.atLeastLessThan_shift_bounds [of _ 0 \<open>length xs\<close> \<open>length ys\<close>]
+ atLeastLessThan_add_Un [of 0 \<open>length xs\<close> \<open>length ys\<close>]
+ by (simp add: horner_sum_eq_sum sum_distrib_left sum.union_disjoint ac_simps nth_append power_add)
+
end
context semiring_bit_shifts
@@ -433,7 +439,7 @@
context unique_euclidean_semiring_with_bit_shifts
begin
-lemma bit_horner_sum_bit_iff:
+lemma bit_horner_sum_bit_iff [bit_simps]:
\<open>bit (horner_sum of_bool 2 bs) n \<longleftrightarrow> n < length bs \<and> bs ! n\<close>
proof (induction bs arbitrary: n)
case Nil
--- a/src/HOL/Library/Bit_Operations.thy Mon Nov 16 21:36:07 2020 +0000
+++ b/src/HOL/Library/Bit_Operations.thy Mon Nov 16 21:37:32 2020 +0000
@@ -16,9 +16,9 @@
and or :: \<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close> (infixr \<open>OR\<close> 59)
and xor :: \<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close> (infixr \<open>XOR\<close> 59)
and mask :: \<open>nat \<Rightarrow> 'a\<close>
- assumes bit_and_iff: \<open>\<And>n. bit (a AND b) n \<longleftrightarrow> bit a n \<and> bit b n\<close>
- and bit_or_iff: \<open>\<And>n. bit (a OR b) n \<longleftrightarrow> bit a n \<or> bit b n\<close>
- and bit_xor_iff: \<open>\<And>n. bit (a XOR b) n \<longleftrightarrow> bit a n \<noteq> bit b n\<close>
+ assumes bit_and_iff [bit_simps]: \<open>\<And>n. bit (a AND b) n \<longleftrightarrow> bit a n \<and> bit b n\<close>
+ and bit_or_iff [bit_simps]: \<open>\<And>n. bit (a OR b) n \<longleftrightarrow> bit a n \<or> bit b n\<close>
+ and bit_xor_iff [bit_simps]: \<open>\<And>n. bit (a XOR b) n \<longleftrightarrow> bit a n \<noteq> bit b n\<close>
and mask_eq_exp_minus_1: \<open>mask n = 2 ^ n - 1\<close>
begin
@@ -119,7 +119,7 @@
\<open>drop_bit n (a XOR b) = drop_bit n a XOR drop_bit n b\<close>
by (rule bit_eqI) (auto simp add: bit_drop_bit_eq bit_xor_iff)
-lemma bit_mask_iff:
+lemma bit_mask_iff [bit_simps]:
\<open>bit (mask m) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> n < m\<close>
by (simp add: mask_eq_exp_minus_1 bit_mask_iff)
@@ -182,7 +182,7 @@
class ring_bit_operations = semiring_bit_operations + ring_parity +
fixes not :: \<open>'a \<Rightarrow> 'a\<close> (\<open>NOT\<close>)
- assumes bit_not_iff: \<open>\<And>n. bit (NOT a) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> \<not> bit a n\<close>
+ assumes bit_not_iff [bit_simps]: \<open>\<And>n. bit (NOT a) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> \<not> bit a n\<close>
assumes minus_eq_not_minus_1: \<open>- a = NOT (a - 1)\<close>
begin
@@ -205,7 +205,7 @@
\<open>- a = NOT a + 1\<close>
using not_eq_complement [of a] by simp
-lemma bit_minus_iff:
+lemma bit_minus_iff [bit_simps]:
\<open>bit (- a) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> \<not> bit (a - 1) n\<close>
by (simp add: minus_eq_not_minus_1 bit_not_iff)
@@ -213,7 +213,7 @@
"even (NOT a) \<longleftrightarrow> odd a"
using bit_not_iff [of a 0] by auto
-lemma bit_not_exp_iff:
+lemma bit_not_exp_iff [bit_simps]:
\<open>bit (NOT (2 ^ m)) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> n \<noteq> m\<close>
by (auto simp add: bit_not_iff bit_exp_iff)
@@ -221,9 +221,9 @@
\<open>bit (- 1) n \<longleftrightarrow> 2 ^ n \<noteq> 0\<close>
by (simp add: bit_minus_iff)
-lemma bit_minus_exp_iff:
+lemma bit_minus_exp_iff [bit_simps]:
\<open>bit (- (2 ^ m)) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> n \<ge> m\<close>
- oops
+ by (auto simp add: bit_simps simp flip: mask_eq_exp_minus_1)
lemma bit_minus_2_iff [simp]:
\<open>bit (- 2) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> n > 0\<close>
@@ -361,7 +361,7 @@
definition flip_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close>
where \<open>flip_bit n a = a XOR push_bit n 1\<close>
-lemma bit_set_bit_iff:
+lemma bit_set_bit_iff [bit_simps]:
\<open>bit (set_bit m a) n \<longleftrightarrow> bit a n \<or> (m = n \<and> 2 ^ n \<noteq> 0)\<close>
by (auto simp add: set_bit_def push_bit_of_1 bit_or_iff bit_exp_iff)
@@ -369,7 +369,7 @@
\<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
-lemma bit_unset_bit_iff:
+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_def push_bit_of_1 bit_and_iff bit_not_iff bit_exp_iff exp_eq_0_imp_not_bit)
@@ -377,7 +377,7 @@
\<open>even (unset_bit m a) \<longleftrightarrow> even a \<or> m = 0\<close>
using bit_unset_bit_iff [of m a 0] by auto
-lemma bit_flip_bit_iff:
+lemma bit_flip_bit_iff [bit_simps]:
\<open>bit (flip_bit m a) n \<longleftrightarrow> (m = n \<longleftrightarrow> \<not> bit a n) \<and> 2 ^ n \<noteq> 0\<close>
by (auto simp add: flip_bit_def push_bit_of_1 bit_xor_iff bit_exp_iff exp_eq_0_imp_not_bit)
@@ -583,7 +583,7 @@
\<open>NOT k div 2 = NOT (k div 2)\<close> for k :: int
by (simp add: not_int_def)
-lemma bit_not_int_iff:
+lemma bit_not_int_iff [bit_simps]:
\<open>bit (NOT k) n \<longleftrightarrow> \<not> bit k n\<close>
for k :: int
by (simp add: bit_not_int_iff' not_int_def)
@@ -973,7 +973,7 @@
\<open>even (of_int k) \<longleftrightarrow> even k\<close>
by (induction k rule: int_bit_induct) simp_all
-lemma bit_of_int_iff:
+lemma bit_of_int_iff [bit_simps]:
\<open>bit (of_int k) n \<longleftrightarrow> (2::'a) ^ n \<noteq> 0 \<and> bit k n\<close>
proof (cases \<open>(2::'a) ^ n = 0\<close>)
case True
@@ -1157,7 +1157,7 @@
definition concat_bit :: \<open>nat \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int\<close>
where \<open>concat_bit n k l = take_bit n k OR push_bit n l\<close>
-lemma bit_concat_bit_iff:
+lemma bit_concat_bit_iff [bit_simps]:
\<open>bit (concat_bit m k l) n \<longleftrightarrow> n < m \<and> bit k n \<or> m \<le> n \<and> bit l (n - m)\<close>
by (simp add: concat_bit_def bit_or_iff bit_and_iff bit_take_bit_iff bit_push_bit_iff ac_simps)
@@ -1259,7 +1259,7 @@
\<open>even (signed_take_bit m a) \<longleftrightarrow> even a\<close>
by (auto simp add: signed_take_bit_def even_or_iff even_mask_iff bit_double_iff)
-lemma bit_signed_take_bit_iff:
+lemma bit_signed_take_bit_iff [bit_simps]:
\<open>bit (signed_take_bit m a) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> bit a (min m n)\<close>
by (simp add: signed_take_bit_def bit_take_bit_iff bit_or_iff bit_not_iff bit_mask_iff min_def not_le)
(use exp_eq_0_imp_not_bit in blast)
@@ -1560,11 +1560,11 @@
instance proof
fix m n q :: nat
show \<open>bit (m AND n) q \<longleftrightarrow> bit m q \<and> bit n q\<close>
- by (auto simp add: bit_nat_iff and_nat_def bit_and_iff less_le bit_eq_iff)
+ by (simp add: and_nat_def bit_simps)
show \<open>bit (m OR n) q \<longleftrightarrow> bit m q \<or> bit n q\<close>
- by (auto simp add: bit_nat_iff or_nat_def bit_or_iff less_le bit_eq_iff)
+ by (simp add: or_nat_def bit_simps)
show \<open>bit (m XOR n) q \<longleftrightarrow> bit m q \<noteq> bit n q\<close>
- by (auto simp add: bit_nat_iff xor_nat_def bit_xor_iff less_le bit_eq_iff)
+ by (simp add: xor_nat_def bit_simps)
qed (simp add: mask_nat_def)
end
--- a/src/HOL/Library/Word.thy Mon Nov 16 21:36:07 2020 +0000
+++ b/src/HOL/Library/Word.thy Mon Nov 16 21:37:32 2020 +0000
@@ -1065,7 +1065,7 @@
context semiring_bits
begin
-lemma bit_unsigned_iff:
+lemma bit_unsigned_iff [bit_simps]:
\<open>bit (unsigned w) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> bit w n\<close>
for w :: \<open>'b::len word\<close>
by (transfer fixing: bit) (simp add: bit_of_nat_iff bit_nat_iff bit_take_bit_iff)
@@ -1175,7 +1175,7 @@
context ring_bit_operations
begin
-lemma bit_signed_iff:
+lemma bit_signed_iff [bit_simps]:
\<open>bit (signed w) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> bit w (min (LENGTH('b) - Suc 0) n)\<close>
for w :: \<open>'b::len word\<close>
by (transfer fixing: bit)
@@ -1779,10 +1779,10 @@
\<open>shiftl1 = (*) 2\<close>
by (rule ext, transfer) simp
-lemma bit_shiftl1_iff:
+lemma bit_shiftl1_iff [bit_simps]:
\<open>bit (shiftl1 w) n \<longleftrightarrow> 0 < n \<and> n < LENGTH('a) \<and> bit w (n - 1)\<close>
for w :: \<open>'a::len word\<close>
- by (simp add: shiftl1_eq_mult_2 bit_double_iff exp_eq_zero_iff not_le) (simp add: ac_simps)
+ by (simp add: shiftl1_eq_mult_2 bit_double_iff not_le) (simp add: ac_simps)
lift_definition shiftr1 :: \<open>'a::len word \<Rightarrow> 'a word\<close>
\<comment> \<open>shift right as unsigned or as signed, ie logical or arithmetic\<close>
@@ -1793,7 +1793,7 @@
\<open>shiftr1 w = w div 2\<close>
by transfer simp
-lemma bit_shiftr1_iff:
+lemma bit_shiftr1_iff [bit_simps]:
\<open>bit (shiftr1 w) n \<longleftrightarrow> bit w (Suc n)\<close>
by transfer (auto simp flip: bit_Suc simp add: bit_take_bit_iff)
@@ -1820,7 +1820,7 @@
\<open>setBit w n = set_bit n w\<close>
by transfer simp
-lemma bit_setBit_iff:
+lemma bit_setBit_iff [bit_simps]:
\<open>bit (setBit w m) n \<longleftrightarrow> (m = n \<and> n < LENGTH('a) \<or> bit w n)\<close>
for w :: \<open>'a::len word\<close>
by transfer (auto simp add: bit_set_bit_iff)
@@ -1833,7 +1833,7 @@
\<open>clearBit w n = unset_bit n w\<close>
by transfer simp
-lemma bit_clearBit_iff:
+lemma bit_clearBit_iff [bit_simps]:
\<open>bit (clearBit w m) n \<longleftrightarrow> m \<noteq> n \<and> bit w n\<close>
for w :: \<open>'a::len word\<close>
by transfer (auto simp add: bit_unset_bit_iff)
@@ -1913,7 +1913,7 @@
using signed_take_bit_decr_length_iff
by (simp add: take_bit_drop_bit) force
-lemma bit_signed_drop_bit_iff:
+lemma bit_signed_drop_bit_iff [bit_simps]:
\<open>bit (signed_drop_bit m w) n \<longleftrightarrow> bit w (if LENGTH('a) - m \<le> n \<and> n < LENGTH('a) then LENGTH('a) - 1 else m + n)\<close>
for w :: \<open>'a::len word\<close>
apply transfer
@@ -2025,7 +2025,7 @@
by simp
qed
-lemma bit_word_rotr_iff:
+lemma bit_word_rotr_iff [bit_simps]:
\<open>bit (word_rotr m w) n \<longleftrightarrow>
n < LENGTH('a) \<and> bit w ((n + m) mod LENGTH('a))\<close>
for w :: \<open>'a::len word\<close>
@@ -2057,13 +2057,13 @@
by simp
qed
-lemma bit_word_rotl_iff:
+lemma bit_word_rotl_iff [bit_simps]:
\<open>bit (word_rotl m w) n \<longleftrightarrow>
n < LENGTH('a) \<and> bit w ((n + (LENGTH('a) - m mod LENGTH('a))) mod LENGTH('a))\<close>
for w :: \<open>'a::len word\<close>
by (simp add: word_rotl_eq_word_rotr bit_word_rotr_iff)
-lemma bit_word_roti_iff:
+lemma bit_word_roti_iff [bit_simps]:
\<open>bit (word_roti k w) n \<longleftrightarrow>
n < LENGTH('a) \<and> bit w (nat ((int n + k) mod int LENGTH('a)))\<close>
for w :: \<open>'a::len word\<close>
@@ -2130,7 +2130,7 @@
for a :: \<open>'a::len word\<close> and b :: \<open>'b::len word\<close>
by transfer (simp add: concat_bit_take_bit_eq)
-lemma bit_word_cat_iff:
+lemma bit_word_cat_iff [bit_simps]:
\<open>bit (word_cat v w :: 'c::len word) n \<longleftrightarrow> n < LENGTH('c) \<and> (if n < LENGTH('b) then bit w n else bit v (n - LENGTH('b)))\<close>
for v :: \<open>'a::len word\<close> and w :: \<open>'b::len word\<close>
by transfer (simp add: bit_concat_bit_iff bit_take_bit_iff)
@@ -3623,7 +3623,7 @@
lemmas word_and_le1 = xtrans(3) [OF word_ao_absorbs (4) [symmetric] le_word_or2]
lemmas word_and_le2 = xtrans(3) [OF word_ao_absorbs (8) [symmetric] le_word_or2]
-lemma bit_horner_sum_bit_word_iff:
+lemma bit_horner_sum_bit_word_iff [bit_simps]:
\<open>bit (horner_sum of_bool (2 :: 'a::len word) bs) n
\<longleftrightarrow> n < min LENGTH('a) (length bs) \<and> bs ! n\<close>
by transfer (simp add: bit_horner_sum_bit_iff)
@@ -3631,7 +3631,7 @@
definition word_reverse :: \<open>'a::len word \<Rightarrow> 'a word\<close>
where \<open>word_reverse w = horner_sum of_bool 2 (rev (map (bit w) [0..<LENGTH('a)]))\<close>
-lemma bit_word_reverse_iff:
+lemma bit_word_reverse_iff [bit_simps]:
\<open>bit (word_reverse w) n \<longleftrightarrow> n < LENGTH('a) \<and> bit w (LENGTH('a) - Suc n)\<close>
for w :: \<open>'a::len word\<close>
by (cases \<open>n < LENGTH('a)\<close>)
@@ -3698,7 +3698,7 @@
apply (simp add: drop_bit_take_bit min_def)
done
-lemma bit_sshiftr1_iff:
+lemma bit_sshiftr1_iff [bit_simps]:
\<open>bit (sshiftr1 w) n \<longleftrightarrow> bit w (if n = LENGTH('a) - 1 then LENGTH('a) - 1 else Suc n)\<close>
for w :: \<open>'a::len word\<close>
apply transfer
@@ -3714,7 +3714,7 @@
using sint_signed_drop_bit_eq [of 1 w]
by (simp add: drop_bit_Suc sshiftr1_eq_signed_drop_bit_Suc_0)
-lemma bit_bshiftr1_iff:
+lemma bit_bshiftr1_iff [bit_simps]:
\<open>bit (bshiftr1 b w) n \<longleftrightarrow> b \<and> n = LENGTH('a) - 1 \<or> bit w (Suc n)\<close>
for w :: \<open>'a::len word\<close>
apply transfer
@@ -3813,7 +3813,7 @@
context
begin
-qualified lemma bit_mask_iff:
+qualified lemma bit_mask_iff [bit_simps]:
\<open>bit (mask m :: 'a::len word) n \<longleftrightarrow> n < min LENGTH('a) m\<close>
by (simp add: bit_mask_iff exp_eq_zero_iff not_le)
@@ -3945,7 +3945,7 @@
then ucast (drop_bit (LENGTH('a) - n) w)
else push_bit (n - LENGTH('a)) (ucast w))\<close>
-lemma bit_slice1_iff:
+lemma bit_slice1_iff [bit_simps]:
\<open>bit (slice1 m w :: 'b::len word) n \<longleftrightarrow> m - LENGTH('a) \<le> n \<and> n < min LENGTH('b) m
\<and> bit w (n + (LENGTH('a) - m) - (m - LENGTH('a)))\<close>
for w :: \<open>'a::len word\<close>
@@ -3955,7 +3955,7 @@
definition slice :: \<open>nat \<Rightarrow> 'a::len word \<Rightarrow> 'b::len word\<close>
where \<open>slice n = slice1 (LENGTH('a) - n)\<close>
-lemma bit_slice_iff:
+lemma bit_slice_iff [bit_simps]:
\<open>bit (slice m w :: 'b::len word) n \<longleftrightarrow> n < min LENGTH('b) (LENGTH('a) - m) \<and> bit w (n + LENGTH('a) - (LENGTH('a) - m))\<close>
for w :: \<open>'a::len word\<close>
by (simp add: slice_def word_size bit_slice1_iff)
@@ -4008,7 +4008,7 @@
definition revcast :: \<open>'a::len word \<Rightarrow> 'b::len word\<close>
where \<open>revcast = slice1 LENGTH('b)\<close>
-lemma bit_revcast_iff:
+lemma bit_revcast_iff [bit_simps]:
\<open>bit (revcast w :: 'b::len word) n \<longleftrightarrow> LENGTH('b) - LENGTH('a) \<le> n \<and> n < LENGTH('b)
\<and> bit w (n + (LENGTH('a) - LENGTH('b)) - (LENGTH('b) - LENGTH('a)))\<close>
for w :: \<open>'a::len word\<close>
--- a/src/HOL/Parity.thy Mon Nov 16 21:36:07 2020 +0000
+++ b/src/HOL/Parity.thy Mon Nov 16 21:37:32 2020 +0000
@@ -906,15 +906,17 @@
\<open>a = b \<longleftrightarrow> (\<forall>n. bit a n \<longleftrightarrow> bit b n)\<close>
by (auto intro: bit_eqI)
-lemma bit_exp_iff:
+named_theorems bit_simps \<open>Simplification rules for \<^const>\<open>bit\<close>\<close>
+
+lemma bit_exp_iff [bit_simps]:
\<open>bit (2 ^ m) n \<longleftrightarrow> 2 ^ m \<noteq> 0 \<and> m = n\<close>
by (auto simp add: bit_iff_odd exp_div_exp_eq)
-lemma bit_1_iff:
+lemma bit_1_iff [bit_simps]:
\<open>bit 1 n \<longleftrightarrow> 1 \<noteq> 0 \<and> n = 0\<close>
using bit_exp_iff [of 0 n] by simp
-lemma bit_2_iff:
+lemma bit_2_iff [bit_simps]:
\<open>bit 2 n \<longleftrightarrow> 2 \<noteq> 0 \<and> n = 1\<close>
using bit_exp_iff [of 1 n] by auto
@@ -931,7 +933,7 @@
ultimately show ?thesis by (simp add: ac_simps)
qed
-lemma bit_double_iff:
+lemma bit_double_iff [bit_simps]:
\<open>bit (2 * a) n \<longleftrightarrow> bit a (n - 1) \<and> n \<noteq> 0 \<and> 2 ^ n \<noteq> 0\<close>
using even_mult_exp_div_exp_iff [of a 1 n]
by (cases n, auto simp add: bit_iff_odd ac_simps)
@@ -1193,7 +1195,7 @@
context semiring_bits
begin
-lemma bit_of_bool_iff:
+lemma bit_of_bool_iff [bit_simps]:
\<open>bit (of_bool b) n \<longleftrightarrow> b \<and> n = 0\<close>
by (simp add: bit_1_iff)
@@ -1201,7 +1203,7 @@
\<open>even (of_nat n) \<longleftrightarrow> even n\<close>
by (induction n rule: nat_bit_induct) simp_all
-lemma bit_of_nat_iff:
+lemma bit_of_nat_iff [bit_simps]:
\<open>bit (of_nat m) n \<longleftrightarrow> (2::'a) ^ n \<noteq> 0 \<and> bit m n\<close>
proof (cases \<open>(2::'a) ^ n = 0\<close>)
case True
@@ -1492,15 +1494,15 @@
\<open>even (push_bit n a) \<longleftrightarrow> n \<noteq> 0 \<or> even a\<close>
by (simp add: push_bit_eq_mult) auto
-lemma bit_push_bit_iff:
+lemma bit_push_bit_iff [bit_simps]:
\<open>bit (push_bit m a) n \<longleftrightarrow> m \<le> n \<and> 2 ^ n \<noteq> 0 \<and> bit a (n - m)\<close>
by (auto simp add: bit_iff_odd push_bit_eq_mult even_mult_exp_div_exp_iff)
-lemma bit_drop_bit_eq:
+lemma bit_drop_bit_eq [bit_simps]:
\<open>bit (drop_bit n a) = bit a \<circ> (+) n\<close>
by (simp add: bit_iff_odd fun_eq_iff ac_simps flip: drop_bit_eq_div)
-lemma bit_take_bit_iff:
+lemma bit_take_bit_iff [bit_simps]:
\<open>bit (take_bit m a) n \<longleftrightarrow> n < m \<and> bit a n\<close>
by (simp add: bit_iff_odd drop_bit_take_bit not_le flip: drop_bit_eq_div)
@@ -1763,7 +1765,7 @@
"drop_bit n (of_nat m) = of_nat (drop_bit n m)"
by (simp add: drop_bit_eq_div Parity.drop_bit_eq_div of_nat_div [of m "2 ^ n"])
-lemma bit_of_nat_iff_bit [simp]:
+lemma bit_of_nat_iff_bit [bit_simps]:
\<open>bit (of_nat m) n \<longleftrightarrow> bit m n\<close>
proof -
have \<open>even (m div 2 ^ n) \<longleftrightarrow> even (of_nat (m div 2 ^ n))\<close>
@@ -1778,7 +1780,7 @@
\<open>of_nat (drop_bit m n) = drop_bit m (of_nat n)\<close>
by (simp add: drop_bit_eq_div semiring_bit_shifts_class.drop_bit_eq_div of_nat_div)
-lemma bit_push_bit_iff_of_nat_iff:
+lemma bit_push_bit_iff_of_nat_iff [bit_simps]:
\<open>bit (push_bit m (of_nat r)) n \<longleftrightarrow> m \<le> n \<and> bit (of_nat r) (n - m)\<close>
by (auto simp add: bit_push_bit_iff)
@@ -1826,12 +1828,12 @@
by (simp add: bit_Suc)
qed
-lemma bit_minus_int_iff:
+lemma bit_minus_int_iff [bit_simps]:
\<open>bit (- k) n \<longleftrightarrow> \<not> bit (k - 1) n\<close>
for k :: int
using bit_not_int_iff' [of \<open>k - 1\<close>] by simp
-lemma bit_nat_iff:
+lemma bit_nat_iff [bit_simps]:
\<open>bit (nat k) n \<longleftrightarrow> k \<ge> 0 \<and> bit k n\<close>
proof (cases \<open>k \<ge> 0\<close>)
case True
@@ -1839,7 +1841,7 @@
ultimately have \<open>k = int m\<close>
by simp
then show ?thesis
- by (auto intro: ccontr)
+ by (simp add: bit_simps)
next
case False
then show ?thesis
--- a/src/HOL/String.thy Mon Nov 16 21:36:07 2020 +0000
+++ b/src/HOL/String.thy Mon Nov 16 21:37:32 2020 +0000
@@ -121,7 +121,7 @@
lemma char_of_nat [simp]:
\<open>char_of (of_nat n) = char_of n\<close>
- by (simp add: char_of_def String.char_of_def drop_bit_of_nat)
+ by (simp add: char_of_def String.char_of_def drop_bit_of_nat bit_simps)
end
--- a/src/Pure/ML/ml_process.scala Mon Nov 16 21:36:07 2020 +0000
+++ b/src/Pure/ML/ml_process.scala Mon Nov 16 21:37:32 2020 +0000
@@ -78,27 +78,36 @@
val eval_options = if (heaps.isEmpty) Nil else List("Options.load_default ()")
// session base
- val eval_session_base =
+ val init_session = Isabelle_System.tmp_file("init_session", ext = "ML")
+ val init_session_name = init_session.getAbsolutePath
+ Isabelle_System.chmod("600", File.path(init_session))
+ File.write(init_session,
session_base match {
- case None => Nil
+ case None => ""
case Some(base) =>
- def print_table(table: List[(String, String)]): String =
+ def print_table: List[(String, String)] => String =
ML_Syntax.print_list(
ML_Syntax.print_pair(
- ML_Syntax.print_string_bytes, ML_Syntax.print_string_bytes))(table)
- def print_list(list: List[String]): String =
- ML_Syntax.print_list(ML_Syntax.print_string_bytes)(list)
- def print_sessions(list: List[(String, Position.T)]): String =
+ ML_Syntax.print_string_bytes, ML_Syntax.print_string_bytes))
+ def print_list: List[String] => String =
+ ML_Syntax.print_list(ML_Syntax.print_string_bytes)
+ def print_sessions: List[(String, Position.T)] => String =
ML_Syntax.print_list(
- ML_Syntax.print_pair(ML_Syntax.print_string_bytes, ML_Syntax.print_properties))(list)
+ ML_Syntax.print_pair(ML_Syntax.print_string_bytes, ML_Syntax.print_properties))
+ def print_bibtex_entries: List[(String, List[String])] => String =
+ ML_Syntax.print_list(
+ ML_Syntax.print_pair(ML_Syntax.print_string_bytes,
+ ML_Syntax.print_list(ML_Syntax.print_string_bytes)))
- List("Resources.init_session" +
+ "Resources.init_session" +
"{session_positions = " + print_sessions(sessions_structure.session_positions) +
", session_directories = " + print_table(sessions_structure.dest_session_directories) +
+ ", session_chapters = " + print_table(sessions_structure.session_chapters) +
+ ", bibtex_entries = " + print_bibtex_entries(sessions_structure.bibtex_entries) +
", docs = " + print_list(base.doc_names) +
", global_theories = " + print_table(base.global_theories.toList) +
- ", loaded_theories = " + print_list(base.loaded_theories.keys) + "}")
- }
+ ", loaded_theories = " + print_list(base.loaded_theories.keys) + "}"
+ })
// process
val eval_process =
@@ -131,7 +140,9 @@
// bash
val bash_args =
ml_runtime_options :::
- (eval_init ::: eval_modes ::: eval_options ::: eval_session_base).flatMap(List("--eval", _)) :::
+ (eval_init ::: eval_modes ::: eval_options).flatMap(List("--eval", _)) :::
+ List("--use", init_session_name,
+ "--eval", "OS.FileSys.remove " + ML_Syntax.print_string_bytes(init_session_name)) :::
use_prelude.flatMap(List("--use", _)) ::: List("--eval", eval_process) ::: args
Bash.process(
@@ -143,6 +154,7 @@
cleanup = () =>
{
isabelle_process_options.delete
+ init_session.delete
Isabelle_System.rm_tree(isabelle_tmp)
cleanup()
})
--- a/src/Pure/PIDE/protocol.ML Mon Nov 16 21:36:07 2020 +0000
+++ b/src/Pure/PIDE/protocol.ML Mon Nov 16 21:37:32 2020 +0000
@@ -25,17 +25,21 @@
val _ =
Isabelle_Process.protocol_command "Prover.init_session"
- (fn [session_positions_yxml, session_directories_yxml, doc_names_yxml, global_theories_yxml,
- loaded_theories_yxml] =>
+ (fn [session_positions_yxml, session_directories_yxml, session_chapters_yxml,
+ bibtex_entries_yxml, doc_names_yxml, global_theories_yxml, loaded_theories_yxml] =>
let
val decode_table = YXML.parse_body #> let open XML.Decode in list (pair string string) end;
val decode_list = YXML.parse_body #> let open XML.Decode in list string end;
val decode_sessions =
YXML.parse_body #> let open XML.Decode in list (pair string properties) end;
+ val decode_bibtex_entries =
+ YXML.parse_body #> let open XML.Decode in list (pair string (list string)) end;
in
Resources.init_session
{session_positions = decode_sessions session_positions_yxml,
session_directories = decode_table session_directories_yxml,
+ session_chapters = decode_table session_chapters_yxml,
+ bibtex_entries = decode_bibtex_entries bibtex_entries_yxml,
docs = decode_list doc_names_yxml,
global_theories = decode_table global_theories_yxml,
loaded_theories = decode_list loaded_theories_yxml}
--- a/src/Pure/PIDE/protocol.scala Mon Nov 16 21:36:07 2020 +0000
+++ b/src/Pure/PIDE/protocol.scala Mon Nov 16 21:37:32 2020 +0000
@@ -285,29 +285,24 @@
/* session base */
- private def encode_table(table: List[(String, String)]): String =
- {
- import XML.Encode._
- Symbol.encode_yxml(list(pair(string, string))(table))
- }
-
- private def encode_list(lst: List[String]): String =
+ def init_session(resources: Resources)
{
import XML.Encode._
- Symbol.encode_yxml(list(string)(lst))
- }
- private def encode_sessions(lst: List[(String, Position.T)]): String =
- {
- import XML.Encode._
- Symbol.encode_yxml(list(pair(string, properties))(lst))
- }
+ def encode_table(arg: List[(String, String)]): String =
+ Symbol.encode_yxml(list(pair(string, string))(arg))
+ def encode_list(arg: List[String]): String =
+ Symbol.encode_yxml(list(string)(arg))
+ def encode_sessions(arg: List[(String, Position.T)]): String =
+ Symbol.encode_yxml(list(pair(string, properties))(arg))
+ def encode_bibtex_entries(arg: List[(String, List[String])]): String =
+ Symbol.encode_yxml(list(pair(string, list(string)))(arg))
- def init_session(resources: Resources)
- {
protocol_command("Prover.init_session",
encode_sessions(resources.sessions_structure.session_positions),
encode_table(resources.sessions_structure.dest_session_directories),
+ encode_table(resources.sessions_structure.session_chapters),
+ encode_bibtex_entries(resources.sessions_structure.bibtex_entries),
encode_list(resources.session_base.doc_names),
encode_table(resources.session_base.global_theories.toList),
encode_list(resources.session_base.loaded_theories.keys))
--- a/src/Pure/PIDE/resources.ML Mon Nov 16 21:36:07 2020 +0000
+++ b/src/Pure/PIDE/resources.ML Mon Nov 16 21:37:32 2020 +0000
@@ -10,6 +10,8 @@
val init_session:
{session_positions: (string * Properties.T) list,
session_directories: (string * string) list,
+ session_chapters: (string * string) list,
+ bibtex_entries: (string * string list) list,
docs: string list,
global_theories: (string * string) list,
loaded_theories: string list} -> unit
@@ -17,12 +19,14 @@
val global_theory: string -> string option
val loaded_theory: string -> bool
val check_session: Proof.context -> string * Position.T -> string
+ val session_chapter: string -> string
val check_doc: Proof.context -> string * Position.T -> string
val master_directory: theory -> Path.T
val imports_of: theory -> (string * Position.T) list
val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory
val thy_path: Path.T -> Path.T
val theory_qualifier: string -> string
+ val theory_bibtex_entries: string -> string list
val find_theory_file: string -> Path.T option
val import_name: string -> Path.T -> string ->
{node_name: Path.T, master_dir: Path.T, theory_name: string}
@@ -54,6 +58,8 @@
val empty_session_base =
{session_positions = []: (string * entry) list,
session_directories = Symtab.empty: Path.T list Symtab.table,
+ session_chapters = Symtab.empty: string Symtab.table,
+ bibtex_entries = Symtab.empty: string list Symtab.table,
docs = []: (string * entry) list,
global_theories = Symtab.empty: string Symtab.table,
loaded_theories = Symtab.empty: unit Symtab.table};
@@ -62,13 +68,16 @@
Synchronized.var "Sessions.base" empty_session_base;
fun init_session
- {session_positions, session_directories, docs, global_theories, loaded_theories} =
+ {session_positions, session_directories, session_chapters,
+ bibtex_entries, docs, global_theories, loaded_theories} =
Synchronized.change global_session_base
(fn _ =>
{session_positions = sort_by #1 (map (apsnd make_entry) session_positions),
session_directories =
fold_rev (fn (dir, name) => Symtab.cons_list (name, Path.explode dir))
session_directories Symtab.empty,
+ session_chapters = Symtab.make session_chapters,
+ bibtex_entries = Symtab.make bibtex_entries,
docs = sort_by #1 (map (apsnd make_entry o rpair []) docs),
global_theories = Symtab.make global_theories,
loaded_theories = Symtab.make_set loaded_theories});
@@ -78,6 +87,8 @@
(fn {global_theories, loaded_theories, ...} =>
{session_positions = [],
session_directories = Symtab.empty,
+ session_chapters = Symtab.empty,
+ bibtex_entries = Symtab.empty,
docs = [],
global_theories = global_theories,
loaded_theories = loaded_theories});
@@ -97,6 +108,9 @@
Markup.entity Markup.sessionN name
|> Markup.properties (Position.entity_properties_of false serial pos));
+fun session_chapter name =
+ the_default "Unsorted" (Symtab.lookup (get_session_base #session_chapters) name);
+
val check_doc = check_name #docs "documentation" (Markup.doc o #1);
@@ -148,6 +162,9 @@
then theory
else Long_Name.qualify qualifier theory;
+fun theory_bibtex_entries theory =
+ Symtab.lookup_list (get_session_base #bibtex_entries) (theory_qualifier theory);
+
fun find_theory_file thy_name =
let
val thy_file = thy_path (Path.basic (Long_Name.base_name thy_name));
--- a/src/Pure/Thy/bibtex.ML Mon Nov 16 21:36:07 2020 +0000
+++ b/src/Pure/Thy/bibtex.ML Mon Nov 16 21:37:32 2020 +0000
@@ -47,7 +47,7 @@
(fn ctxt => fn (opt, citations) =>
let
val thy = Proof_Context.theory_of ctxt;
- val bibtex_entries = Present.get_bibtex_entries thy;
+ val bibtex_entries = Resources.theory_bibtex_entries (Context.theory_long_name thy);
val _ =
if null bibtex_entries andalso Context.theory_name thy <> Context.PureN then ()
else
--- a/src/Pure/Thy/present.ML Mon Nov 16 21:36:07 2020 +0000
+++ b/src/Pure/Thy/present.ML Mon Nov 16 21:37:32 2020 +0000
@@ -6,12 +6,9 @@
signature PRESENT =
sig
- val tex_path: string -> Path.T
- val get_bibtex_entries: theory -> string list
- val theory_qualifier: theory -> string
val init: HTML.symbols -> bool -> Path.T -> string list -> string * string -> bool -> unit
val finish: unit -> unit
- val begin_theory: string list -> int -> (unit -> HTML.text) -> theory -> theory
+ val begin_theory: int -> (unit -> HTML.text) -> theory -> theory
end;
structure Present: PRESENT =
@@ -20,8 +17,6 @@
(** paths **)
-val tex_ext = Path.ext "tex";
-val tex_path = tex_ext o Path.basic;
val html_ext = Path.ext "html";
val html_path = html_ext o Path.basic;
val index_path = Path.basic "index.html";
@@ -33,32 +28,6 @@
-(** theory data **)
-
-type browser_info = {chapter: string, name: string, bibtex_entries: string list};
-val empty_browser_info: browser_info = {chapter = "Unsorted", name = "Unknown", bibtex_entries = []};
-
-structure Browser_Info = Theory_Data
-(
- type T = browser_info
- val empty = empty_browser_info;
- val extend = I;
- val merge = #1;
-);
-
-fun reset_browser_info thy =
- if Browser_Info.get thy = empty_browser_info then NONE
- else SOME (Browser_Info.put empty_browser_info thy);
-
-val _ =
- Theory.setup
- (Theory.at_begin reset_browser_info #>
- Browser_Info.put {chapter = Context.PureN, name = Context.PureN, bibtex_entries = []});
-
-val get_bibtex_entries = #bibtex_entries o Browser_Info.get;
-
-
-
(** global browser info state **)
(* type browser_info *)
@@ -168,7 +137,8 @@
fun theory_link (curr_chapter, curr_session) thy =
let
- val {chapter, name = session, ...} = Browser_Info.get thy;
+ val session = Resources.theory_qualifier (Context.theory_long_name thy);
+ val chapter = Resources.session_chapter session;
val link = html_path (Context.theory_name thy);
in
if curr_session = session then SOME link
@@ -178,7 +148,7 @@
else SOME (Path.parent + Path.parent + Path.basic chapter + Path.basic session + link)
end;
-fun begin_theory bibtex_entries update_time mk_text thy =
+fun begin_theory update_time mk_text thy =
with_session_info thy (fn {symbols, name = session_name, chapter, ...} =>
let
val name = Context.theory_name thy;
@@ -190,14 +160,10 @@
val _ = update_html name (HTML.theory symbols name parent_specs (mk_text ()));
- val bibtex_entries' =
+ val _ =
if is_session_theory thy then
- (add_html_index (update_time, HTML.theory_entry symbols (Url.File (html_path name), name));
- bibtex_entries)
- else [];
- in
- thy
- |> Browser_Info.put {chapter = chapter, name = session_name, bibtex_entries = bibtex_entries'}
- end);
+ add_html_index (update_time, HTML.theory_entry symbols (Url.File (html_path name), name))
+ else ();
+ in thy end);
end;
--- a/src/Pure/Thy/sessions.scala Mon Nov 16 21:36:07 2020 +0000
+++ b/src/Pure/Thy/sessions.scala Mon Nov 16 21:37:32 2020 +0000
@@ -511,7 +511,7 @@
case s => Some(dir + Path.explode(s))
}
- def bibtex_entries: List[Text.Info[String]] =
+ lazy val bibtex_entries: List[Text.Info[String]] =
(for {
(document_dir, file) <- document_files.iterator
if Bibtex.is_bibtex(file.file_name)
@@ -804,6 +804,16 @@
def imports_requirements(ss: List[String]): List[String] = imports_graph.all_preds_rev(ss)
def imports_topological_order: List[String] = imports_graph.topological_order
+ def bibtex_entries: List[(String, List[String])] =
+ build_topological_order.flatMap(name =>
+ apply(name).bibtex_entries match {
+ case Nil => None
+ case entries => Some(name -> entries.map(_.info))
+ })
+
+ def session_chapters: List[(String, String)] =
+ build_topological_order.map(name => name -> apply(name).chapter)
+
override def toString: String =
imports_graph.keys_iterator.mkString("Sessions.Structure(", ", ", ")")
}
--- a/src/Pure/Thy/thy_info.ML Mon Nov 16 21:36:07 2020 +0000
+++ b/src/Pure/Thy/thy_info.ML Mon Nov 16 21:37:32 2020 +0000
@@ -21,7 +21,6 @@
type context =
{options: Options.T,
symbols: HTML.symbols,
- bibtex_entries: string list,
last_timing: Toplevel.transition -> Time.time}
val use_theories: context -> string -> Path.T -> (string * Position.T) list -> unit
val use_thy: string -> unit
@@ -66,11 +65,10 @@
else
let
val thy_name = Context.theory_name thy;
- val document_path = Path.basic "document" + Present.tex_path thy_name;
-
+ val document_tex_name = Path.explode_binding0 ("document/" ^ thy_name ^ ".tex");
val latex = Latex.isabelle_body thy_name body;
val output = [Latex.output_text latex, Latex.output_positions file_pos latex];
- in Export.export thy (Path.binding0 document_path) (XML.blob output) end
+ in Export.export thy document_tex_name (XML.blob output) end
end));
@@ -188,13 +186,11 @@
type context =
{options: Options.T,
symbols: HTML.symbols,
- bibtex_entries: string list,
last_timing: Toplevel.transition -> Time.time};
fun default_context (): context =
{options = Options.default (),
symbols = HTML.no_symbols,
- bibtex_entries = [],
last_timing = K Time.zeroTime};
@@ -304,7 +300,7 @@
fun eval_thy (context: context) update_time master_dir header text_pos text parents =
let
- val {options, symbols, bibtex_entries, last_timing} = context;
+ val {options, symbols, last_timing} = context;
val (name, _) = #name header;
val keywords =
fold (curry Keyword.merge_keywords o Thy_Header.get_keywords) parents
@@ -315,7 +311,7 @@
fun init () =
Resources.begin_theory master_dir header parents
- |> Present.begin_theory bibtex_entries update_time
+ |> Present.begin_theory update_time
(fn () => implode (map (HTML.present_span symbols keywords) spans));
val (results, thy) =
--- a/src/Pure/Tools/build.ML Mon Nov 16 21:36:07 2020 +0000
+++ b/src/Pure/Tools/build.ML Mon Nov 16 21:37:32 2020 +0000
@@ -55,11 +55,10 @@
(* build theories *)
-fun build_theories symbols bibtex_entries last_timing qualifier master_dir (options, thys) =
+fun build_theories symbols last_timing qualifier master_dir (options, thys) =
let
val context =
- {options = options, symbols = symbols, bibtex_entries = bibtex_entries,
- last_timing = last_timing};
+ {options = options, symbols = symbols, last_timing = last_timing};
val condition = space_explode "," (Options.string options "condition");
val conds = filter_out (can getenv_strict) condition;
in
@@ -90,8 +89,8 @@
let
val (symbol_codes, (command_timings, (verbose, (browser_info,
(documents, (parent_name, (chapter, (session_name, (master_dir,
- (theories, (session_positions, (session_directories, (doc_names, (global_theories,
- (loaded_theories, bibtex_entries))))))))))))))) =
+ (theories, (session_positions, (session_directories, (session_chapters,
+ (doc_names, (global_theories, (loaded_theories, bibtex_entries)))))))))))))))) =
YXML.parse_body args_yxml |>
let
open XML.Decode;
@@ -103,8 +102,10 @@
(pair path
(pair (((list (pair Options.decode (list (pair string position))))))
(pair (list (pair string properties))
- (pair (list (pair string string)) (pair (list string)
- (pair (list (pair string string)) (pair (list string) (list string)))))))))))))))
+ (pair (list (pair string string))
+ (pair (list (pair string string)) (pair (list string)
+ (pair (list (pair string string)) (pair (list string)
+ (list (pair string (list string))))))))))))))))))
end;
val symbols = HTML.make_symbols symbol_codes;
@@ -115,6 +116,8 @@
Resources.init_session
{session_positions = session_positions,
session_directories = session_directories,
+ session_chapters = session_chapters,
+ bibtex_entries = bibtex_entries,
docs = doc_names,
global_theories = global_theories,
loaded_theories = loaded_theories};
@@ -133,8 +136,7 @@
val res1 =
theories |>
- (List.app
- (build_theories symbols bibtex_entries last_timing session_name master_dir)
+ (List.app (build_theories symbols last_timing session_name master_dir)
|> session_timing
|> Exn.capture);
val res2 = Exn.capture Session.finish ();
--- a/src/Pure/Tools/build.scala Mon Nov 16 21:36:07 2020 +0000
+++ b/src/Pure/Tools/build.scala Mon Nov 16 21:37:32 2020 +0000
@@ -180,15 +180,18 @@
pair(list(pair(Options.encode, list(pair(string, properties)))),
pair(list(pair(string, properties)),
pair(list(pair(string, string)),
- pair(list(string), pair(list(pair(string, string)),
- pair(list(string), list(string))))))))))))))))(
+ pair(list(pair(string, string)),
+ pair(list(string),
+ pair(list(pair(string, string)),
+ pair(list(string), list(pair(string, list(string)))))))))))))))))))(
(Symbol.codes, (command_timings0, (verbose, (store.browser_info,
(documents, (parent, (info.chapter, (session_name, (Path.current,
(info.theories,
(sessions_structure.session_positions,
(sessions_structure.dest_session_directories,
+ (sessions_structure.session_chapters,
(base.doc_names, (base.global_theories.toList,
- (base.loaded_theories.keys, info.bibtex_entries.map(_.info)))))))))))))))))
+ (base.loaded_theories.keys, sessions_structure.bibtex_entries)))))))))))))))))
})
val env =