--- a/src/HOL/Analysis/Complex_Transcendental.thy Sun Dec 01 11:51:17 2019 +0100
+++ b/src/HOL/Analysis/Complex_Transcendental.thy Mon Dec 02 10:31:51 2019 +0100
@@ -4053,4 +4053,6 @@
apply (auto simp: Re_complex_div_eq_0 exp_of_nat_mult [symmetric] mult_ac exp_Euler)
done
+
+
end
--- a/src/HOL/Analysis/Homeomorphism.thy Sun Dec 01 11:51:17 2019 +0100
+++ b/src/HOL/Analysis/Homeomorphism.thy Mon Dec 02 10:31:51 2019 +0100
@@ -2184,7 +2184,6 @@
qed
qed
-
corollary covering_space_lift_stronger:
fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
and f :: "'c::real_normed_vector \<Rightarrow> 'b"
@@ -2252,4 +2251,36 @@
by (metis that covering_space_lift_strong [OF cov _ \<open>z \<in> U\<close> U contf fim])
qed
+subsection\<^marker>\<open>tag unimportant\<close> \<open>Homeomorphisms of arc images\<close>
+
+lemma homeomorphism_arc:
+ fixes g :: "real \<Rightarrow> 'a::t2_space"
+ assumes "arc g"
+ obtains h where "homeomorphism {0..1} (path_image g) g h"
+using assms by (force simp: arc_def homeomorphism_compact path_def path_image_def)
+
+lemma homeomorphic_arc_image_interval:
+ fixes g :: "real \<Rightarrow> 'a::t2_space" and a::real
+ assumes "arc g" "a < b"
+ shows "(path_image g) homeomorphic {a..b}"
+proof -
+ have "(path_image g) homeomorphic {0..1::real}"
+ by (meson assms(1) homeomorphic_def homeomorphic_sym homeomorphism_arc)
+ also have "\<dots> homeomorphic {a..b}"
+ using assms by (force intro: homeomorphic_closed_intervals_real)
+ finally show ?thesis .
+qed
+
+lemma homeomorphic_arc_images:
+ fixes g :: "real \<Rightarrow> 'a::t2_space" and h :: "real \<Rightarrow> 'b::t2_space"
+ assumes "arc g" "arc h"
+ shows "(path_image g) homeomorphic (path_image h)"
+proof -
+ have "(path_image g) homeomorphic {0..1::real}"
+ by (meson assms homeomorphic_def homeomorphic_sym homeomorphism_arc)
+ also have "\<dots> homeomorphic (path_image h)"
+ by (meson assms homeomorphic_def homeomorphism_arc)
+ finally show ?thesis .
+qed
+
end
--- a/src/HOL/Analysis/Path_Connected.thy Sun Dec 01 11:51:17 2019 +0100
+++ b/src/HOL/Analysis/Path_Connected.thy Mon Dec 02 10:31:51 2019 +0100
@@ -4055,7 +4055,6 @@
shows "\<exists>g. homeomorphism S T f g"
using assms injective_into_1d_eq_homeomorphism by blast
-
subsection\<^marker>\<open>tag unimportant\<close> \<open>Rectangular paths\<close>
definition\<^marker>\<open>tag unimportant\<close> rectpath where
--- a/src/HOL/Analysis/Retracts.thy Sun Dec 01 11:51:17 2019 +0100
+++ b/src/HOL/Analysis/Retracts.thy Mon Dec 02 10:31:51 2019 +0100
@@ -2591,4 +2591,51 @@
shows "connected(-S)"
using assms path_connected_complement_homeomorphic_interval path_connected_imp_connected by blast
+
+lemma path_connected_arc_complement:
+ fixes \<gamma> :: "real \<Rightarrow> 'a::euclidean_space"
+ assumes "arc \<gamma>" "2 \<le> DIM('a)"
+ shows "path_connected(- path_image \<gamma>)"
+proof -
+ have "path_image \<gamma> homeomorphic {0..1::real}"
+ by (simp add: assms homeomorphic_arc_image_interval)
+ then
+ show ?thesis
+ apply (rule path_connected_complement_homeomorphic_convex_compact)
+ apply (auto simp: assms)
+ done
+qed
+
+lemma connected_arc_complement:
+ fixes \<gamma> :: "real \<Rightarrow> 'a::euclidean_space"
+ assumes "arc \<gamma>" "2 \<le> DIM('a)"
+ shows "connected(- path_image \<gamma>)"
+ by (simp add: assms path_connected_arc_complement path_connected_imp_connected)
+
+lemma inside_arc_empty:
+ fixes \<gamma> :: "real \<Rightarrow> 'a::euclidean_space"
+ assumes "arc \<gamma>"
+ shows "inside(path_image \<gamma>) = {}"
+proof (cases "DIM('a) = 1")
+ case True
+ then show ?thesis
+ using assms connected_arc_image connected_convex_1_gen inside_convex by blast
+next
+ case False
+ show ?thesis
+ proof (rule inside_bounded_complement_connected_empty)
+ show "connected (- path_image \<gamma>)"
+ apply (rule connected_arc_complement [OF assms])
+ using False
+ by (metis DIM_ge_Suc0 One_nat_def Suc_1 not_less_eq_eq order_class.order.antisym)
+ show "bounded (path_image \<gamma>)"
+ by (simp add: assms bounded_arc_image)
+ qed
+qed
+
+lemma inside_simple_curve_imp_closed:
+ fixes \<gamma> :: "real \<Rightarrow> 'a::euclidean_space"
+ shows "\<lbrakk>simple_path \<gamma>; x \<in> inside(path_image \<gamma>)\<rbrakk> \<Longrightarrow> pathfinish \<gamma> = pathstart \<gamma>"
+ using arc_simple_path inside_arc_empty by blast
+
end
--- a/src/HOL/Code_Numeral.thy Sun Dec 01 11:51:17 2019 +0100
+++ b/src/HOL/Code_Numeral.thy Mon Dec 02 10:31:51 2019 +0100
@@ -299,7 +299,7 @@
instance by (standard; transfer)
(fact bit_eq_rec bit_induct push_bit_eq_mult drop_bit_eq_div
bits_div_0 bits_div_by_1 bit_mod_div_trivial even_succ_div_2
- div_exp_eq mod_exp_eq mult_exp_mod_exp_eq div_exp_mod_exp_eq)+
+ exp_div_exp_eq div_exp_eq mod_exp_eq mult_exp_mod_exp_eq div_exp_mod_exp_eq)+
end
@@ -995,7 +995,7 @@
instance by (standard; transfer)
(fact bit_eq_rec bit_induct push_bit_eq_mult drop_bit_eq_div
bits_div_0 bits_div_by_1 bit_mod_div_trivial even_succ_div_2
- div_exp_eq mod_exp_eq mult_exp_mod_exp_eq div_exp_mod_exp_eq)+
+ exp_div_exp_eq div_exp_eq mod_exp_eq mult_exp_mod_exp_eq div_exp_mod_exp_eq)+
end
--- a/src/HOL/Parity.thy Sun Dec 01 11:51:17 2019 +0100
+++ b/src/HOL/Parity.thy Mon Dec 02 10:31:51 2019 +0100
@@ -577,6 +577,7 @@
and bits_div_by_1 [simp]: \<open>a div 1 = a\<close>
and bit_mod_div_trivial [simp]: \<open>a mod b div b = 0\<close>
and even_succ_div_2 [simp]: \<open>even a \<Longrightarrow> (1 + a) div 2 = a div 2\<close>
+ and exp_div_exp_eq: \<open>2 ^ m div 2 ^ n = of_bool (2 ^ m \<noteq> 0 \<and> m \<ge> n) * 2 ^ (m - n)\<close>
and div_exp_eq: \<open>a div 2 ^ m div 2 ^ n = a div 2 ^ (m + n)\<close>
and mod_exp_eq: \<open>a mod 2 ^ m mod 2 ^ n = a mod 2 ^ min m n\<close>
and mult_exp_mod_exp_eq: \<open>m \<le> n \<Longrightarrow> (a * 2 ^ m) mod (2 ^ n) = (a mod 2 ^ (n - m)) * 2 ^ m\<close>
@@ -750,6 +751,10 @@
apply (metis bit_eq_iff local.mod2_eq_if local.mod_div_mult_eq)
done
+lemma bit_exp_iff:
+ \<open>bit (2 ^ m) n \<longleftrightarrow> 2 ^ m \<noteq> 0 \<and> m = n\<close>
+ by (auto simp add: bit_def exp_div_exp_eq)
+
end
lemma nat_bit_induct [case_names zero even odd]:
@@ -810,7 +815,7 @@
apply (auto simp add: mod_mod_cancel div_mult2_eq power_add mod_mult2_eq le_iff_add split: split_min_lin)
apply (simp add: mult.commute)
done
-qed (auto simp add: div_mult2_eq mod_mult2_eq power_add)
+qed (auto simp add: div_mult2_eq mod_mult2_eq power_add power_diff)
lemma int_bit_induct [case_names zero minus even odd]:
"P k" if zero_int: "P 0"
@@ -891,6 +896,24 @@
with rec [of k True] show ?case
by (simp add: ac_simps)
qed
+ show \<open>(2::int) ^ m div 2 ^ n = of_bool ((2::int) ^ m \<noteq> 0 \<and> n \<le> m) * 2 ^ (m - n)\<close>
+ for m n :: nat
+ proof (cases \<open>m < n\<close>)
+ case True
+ then have \<open>n = m + (n - m)\<close>
+ by simp
+ then have \<open>(2::int) ^ m div 2 ^ n = (2::int) ^ m div 2 ^ (m + (n - m))\<close>
+ by simp
+ also have \<open>\<dots> = (2::int) ^ m div (2 ^ m * 2 ^ (n - m))\<close>
+ by (simp add: power_add)
+ also have \<open>\<dots> = (2::int) ^ m div 2 ^ m div 2 ^ (n - m)\<close>
+ by (simp add: zdiv_zmult2_eq)
+ finally show ?thesis using \<open>m < n\<close> by simp
+ next
+ case False
+ then show ?thesis
+ by (simp add: power_diff)
+ qed
show \<open>k mod 2 ^ m mod 2 ^ n = k mod 2 ^ min m n\<close>
for m n :: nat and k :: int
using mod_exp_eq [of \<open>nat k\<close> m n]
@@ -905,7 +928,7 @@
apply (auto simp add: power_add zmod_zmult2_eq le_iff_add split: split_min_lin)
apply (simp add: ac_simps)
done
-qed (auto simp add: zdiv_zmult2_eq zmod_zmult2_eq power_add)
+qed (auto simp add: zdiv_zmult2_eq zmod_zmult2_eq power_add power_diff not_le)
class semiring_bit_shifts = semiring_bits +
fixes push_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close>
--- a/src/HOL/Transfer.thy Sun Dec 01 11:51:17 2019 +0100
+++ b/src/HOL/Transfer.thy Mon Dec 02 10:31:51 2019 +0100
@@ -642,13 +642,25 @@
end
-subsection \<open>\<^const>\<open>of_nat\<close>\<close>
+subsection \<open>\<^const>\<open>of_bool\<close> and \<^const>\<open>of_nat\<close>\<close>
+
+context
+ includes lifting_syntax
+begin
+
+lemma transfer_rule_of_bool:
+ \<open>((\<longleftrightarrow>) ===> (\<cong>)) of_bool of_bool\<close>
+ if [transfer_rule]: \<open>0 \<cong> 0\<close> \<open>1 \<cong> 1\<close>
+ for R :: \<open>'a::zero_neq_one \<Rightarrow> 'b::zero_neq_one \<Rightarrow> bool\<close> (infix \<open>\<cong>\<close> 50)
+ by (unfold of_bool_def [abs_def]) transfer_prover
lemma transfer_rule_of_nat:
- fixes R :: "'a::semiring_1 \<Rightarrow> 'b::semiring_1 \<Rightarrow> bool"
- assumes [transfer_rule]: "R 0 0" "R 1 1"
- "rel_fun R (rel_fun R R) plus plus"
- shows "rel_fun HOL.eq R of_nat of_nat"
+ "((=) ===> (\<cong>)) of_nat of_nat"
+ if [transfer_rule]: \<open>0 \<cong> 0\<close> \<open>1 \<cong> 1\<close>
+ \<open>((\<cong>) ===> (\<cong>) ===> (\<cong>)) (+) (+)\<close>
+ for R :: \<open>'a::semiring_1 \<Rightarrow> 'b::semiring_1 \<Rightarrow> bool\<close> (infix \<open>\<cong>\<close> 50)
by (unfold of_nat_def [abs_def]) transfer_prover
end
+
+end
--- a/src/HOL/ex/Bit_Operations.thy Sun Dec 01 11:51:17 2019 +0100
+++ b/src/HOL/ex/Bit_Operations.thy Mon Dec 02 10:31:51 2019 +0100
@@ -9,12 +9,39 @@
Main
begin
+lemma minus_1_div_exp_eq_int [simp]:
+ \<open>- 1 div (2 :: int) ^ n = - 1\<close>
+ for n :: nat
+ by (induction n) (use div_exp_eq [symmetric, of \<open>- 1 :: int\<close> 1] in \<open>simp_all add: ac_simps\<close>)
+
+context semiring_bits
+begin
+
+lemma bits_div_by_0 [simp]:
+ \<open>a div 0 = 0\<close>
+ by (metis local.add_cancel_right_right local.bit_mod_div_trivial local.mod_mult_div_eq local.mult_not_zero)
+
+lemma bit_0_eq [simp]:
+ \<open>bit 0 = bot\<close>
+ by (simp add: fun_eq_iff bit_def)
+
+end
+
+context semiring_bit_shifts
+begin
+
+end
+
+
subsection \<open>Bit operations in suitable algebraic structures\<close>
class semiring_bit_operations = semiring_bit_shifts +
- fixes "and" :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "AND" 64)
- and or :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "OR" 59)
- and xor :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "XOR" 59)
+ fixes "and" :: \<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close> (infixr "AND" 64)
+ and or :: \<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close> (infixr "OR" 59)
+ and xor :: \<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close> (infixr "XOR" 59)
+ 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>
begin
text \<open>
@@ -40,7 +67,7 @@
text \<open>
Having
- <^const>\<open>set_bit\<close>, \<^const>\<open>unset_bit\<close> and \<^const>\<open>flip_bit\<close> as separate
+ \<^const>\<open>set_bit\<close>, \<^const>\<open>unset_bit\<close> and \<^const>\<open>flip_bit\<close> as separate
operations allows to implement them using bit masks later.
\<close>
@@ -85,19 +112,38 @@
class ring_bit_operations = semiring_bit_operations + ring_parity +
fixes not :: \<open>'a \<Rightarrow> 'a\<close> (\<open>NOT\<close>)
- assumes boolean_algebra: \<open>boolean_algebra (AND) (OR) NOT 0 (- 1)\<close>
- and boolean_algebra_xor_eq: \<open>boolean_algebra.xor (AND) (OR) NOT = (XOR)\<close>
+ assumes bits_even_minus_1_div_exp_iff [simp]: \<open>even (- 1 div 2 ^ n) \<longleftrightarrow> 2 ^ n = 0\<close>
+ assumes bit_not_iff: \<open>\<And>n. bit (NOT a) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> \<not> bit a n\<close>
begin
+lemma bits_minus_1_mod_2_eq [simp]:
+ \<open>(- 1) mod 2 = 1\<close>
+ by (simp add: mod_2_eq_odd)
+
+lemma bit_minus_1_iff [simp]:
+ \<open>bit (- 1) n \<longleftrightarrow> 2 ^ n \<noteq> 0\<close>
+ by (simp add: bit_def)
+
sublocale bit: boolean_algebra \<open>(AND)\<close> \<open>(OR)\<close> NOT 0 \<open>- 1\<close>
rewrites \<open>bit.xor = (XOR)\<close>
proof -
interpret bit: boolean_algebra \<open>(AND)\<close> \<open>(OR)\<close> NOT 0 \<open>- 1\<close>
- by (fact boolean_algebra)
+ apply standard
+ apply (auto simp add: bit_eq_iff bit_and_iff bit_or_iff bit_not_iff)
+ apply (metis local.bit_def local.bit_exp_iff local.bits_div_by_0)
+ apply (metis local.bit_def local.bit_exp_iff local.bits_div_by_0)
+ done
show \<open>boolean_algebra (AND) (OR) NOT 0 (- 1)\<close>
by standard
- show \<open>boolean_algebra.xor (AND) (OR) NOT = (XOR)\<close>
- by (fact boolean_algebra_xor_eq)
+ show \<open>boolean_algebra.xor (AND) (OR) NOT = (XOR)\<close>
+ apply (auto simp add: fun_eq_iff bit.xor_def bit_eq_iff bit_and_iff bit_or_iff bit_not_iff bit_xor_iff)
+ apply (metis local.bit_def local.bit_exp_iff local.bits_div_by_0)
+ apply (metis local.bit_def local.bit_exp_iff local.bits_div_by_0)
+ apply (metis local.bit_def local.bit_exp_iff local.bits_div_by_0)
+ apply (metis local.bit_def local.bit_exp_iff local.bits_div_by_0)
+ apply (metis local.bit_def local.bit_exp_iff local.bits_div_by_0)
+ apply (metis local.bit_def local.bit_exp_iff local.bits_div_by_0)
+ done
qed
text \<open>
@@ -265,7 +311,39 @@
"n XOR 0 = n" for n :: nat
by simp
-instance ..
+instance proof
+ fix m n q :: nat
+ show \<open>bit (m AND n) q \<longleftrightarrow> bit m q \<and> bit n q\<close>
+ proof (rule sym, induction q arbitrary: m n)
+ case 0
+ then show ?case
+ by (simp add: and_nat.even_iff)
+ next
+ case (Suc q)
+ with and_nat.rec [of m n] show ?case
+ by simp
+ qed
+ show \<open>bit (m OR n) q \<longleftrightarrow> bit m q \<or> bit n q\<close>
+ proof (rule sym, induction q arbitrary: m n)
+ case 0
+ then show ?case
+ by (simp add: or_nat.even_iff)
+ next
+ case (Suc q)
+ with or_nat.rec [of m n] show ?case
+ by simp
+ qed
+ show \<open>bit (m XOR n) q \<longleftrightarrow> bit m q \<noteq> bit n q\<close>
+ proof (rule sym, induction q arbitrary: m n)
+ case 0
+ then show ?case
+ by (simp add: xor_nat.even_iff)
+ next
+ case (Suc q)
+ with xor_nat.rec [of m n] show ?case
+ by simp
+ qed
+qed
end
@@ -625,89 +703,49 @@
lemma even_not_iff [simp]:
"even (NOT k) \<longleftrightarrow> odd k"
- for k :: int
+ for k :: int
by (simp add: not_int_def)
+lemma bit_not_iff_int:
+ \<open>bit (NOT k) n \<longleftrightarrow> \<not> bit k n\<close>
+ for k :: int
+ by (induction n arbitrary: k)
+ (simp_all add: not_int_def flip: complement_div_2)
+
+
instance proof
- interpret bit_int: boolean_algebra "(AND)" "(OR)" NOT 0 "- 1 :: int"
- proof
- show "k AND (l OR r) = k AND l OR k AND r"
- for k l r :: int
- proof (induction k arbitrary: l r rule: int_bit_induct)
- case zero
- show ?case
- by simp
- next
- case minus
- show ?case
- by simp
- next
- case (even k)
- then show ?case by (simp add: and_int.rec [of "k * 2"]
- or_int.rec [of "(k AND l div 2) * 2"] or_int.rec [of l])
- next
- case (odd k)
- then show ?case by (simp add: and_int.rec [of "1 + k * 2"]
- or_int.rec [of "(k AND l div 2) * 2"] or_int.rec [of "1 + (k AND l div 2) * 2"] or_int.rec [of l])
- qed
- show "k OR l AND r = (k OR l) AND (k OR r)"
- for k l r :: int
- proof (induction k arbitrary: l r rule: int_bit_induct)
- case zero
- then show ?case
- by simp
- next
- case minus
- then show ?case
- by simp
- next
- case (even k)
- then show ?case by (simp add: or_int.rec [of "k * 2"]
- and_int.rec [of "(k OR l div 2) * 2"] and_int.rec [of "1 + (k OR l div 2) * 2"] and_int.rec [of l])
- next
- case (odd k)
- then show ?case by (simp add: or_int.rec [of "1 + k * 2"]
- and_int.rec [of "1 + (k OR l div 2) * 2"] and_int.rec [of l])
- qed
- show "k AND NOT k = 0" for k :: int
- by (induction k rule: int_bit_induct)
- (simp_all add: not_int_def complement_half minus_diff_commute [of 1])
- show "k OR NOT k = - 1" for k :: int
- by (induction k rule: int_bit_induct)
- (simp_all add: not_int_def complement_half minus_diff_commute [of 1])
- qed (simp_all add: and_int.assoc or_int.assoc,
- simp_all add: and_int.commute or_int.commute)
- show "boolean_algebra (AND) (OR) NOT 0 (- 1 :: int)"
- by (fact bit_int.boolean_algebra_axioms)
- show "bit_int.xor = ((XOR) :: int \<Rightarrow> _)"
- proof (rule ext)+
- fix k l :: int
- have "k XOR l = k AND NOT l OR NOT k AND l"
- proof (induction k arbitrary: l rule: int_bit_induct)
- case zero
- show ?case
- by simp
- next
- case minus
- show ?case
- by (simp add: not_int_def)
- next
- case (even k)
- then show ?case
- by (simp add: xor_int.rec [of "k * 2"] and_int.rec [of "k * 2"]
- or_int.rec [of _ "1 + 2 * NOT k AND l"] not_div_2)
- (simp add: and_int.rec [of _ l])
- next
- case (odd k)
- then show ?case
- by (simp add: xor_int.rec [of "1 + k * 2"] and_int.rec [of "1 + k * 2"]
- or_int.rec [of _ "2 * NOT k AND l"] not_div_2)
- (simp add: and_int.rec [of _ l])
- qed
- then show "bit_int.xor k l = k XOR l"
- by (simp add: bit_int.xor_def)
+ fix k l :: int and n :: nat
+ show \<open>bit (k AND l) n \<longleftrightarrow> bit k n \<and> bit l n\<close>
+ proof (rule sym, induction n arbitrary: k l)
+ case 0
+ then show ?case
+ by (simp add: and_int.even_iff)
+ next
+ case (Suc n)
+ with and_int.rec [of k l] show ?case
+ by simp
qed
-qed
+ show \<open>bit (k OR l) n \<longleftrightarrow> bit k n \<or> bit l n\<close>
+ proof (rule sym, induction n arbitrary: k l)
+ case 0
+ then show ?case
+ by (simp add: or_int.even_iff)
+ next
+ case (Suc n)
+ with or_int.rec [of k l] show ?case
+ by simp
+ qed
+ show \<open>bit (k XOR l) n \<longleftrightarrow> bit k n \<noteq> bit l n\<close>
+ proof (rule sym, induction n arbitrary: k l)
+ case 0
+ then show ?case
+ by (simp add: xor_int.even_iff)
+ next
+ case (Suc n)
+ with xor_int.rec [of k l] show ?case
+ by simp
+ qed
+qed (simp_all add: bit_not_iff_int)
end
@@ -743,36 +781,21 @@
lemma take_bit_not_iff:
"Parity.take_bit n (NOT k) = Parity.take_bit n (NOT l) \<longleftrightarrow> Parity.take_bit n k = Parity.take_bit n l"
for k l :: int
- by (simp add: not_int_def take_bit_complement_iff)
+ by (auto simp add: bit_eq_iff bit_take_bit_iff bit_not_iff_int)
lemma take_bit_and [simp]:
"Parity.take_bit n (k AND l) = Parity.take_bit n k AND Parity.take_bit n l"
for k l :: int
- apply (induction n arbitrary: k l)
- apply simp
- apply (subst and_int.rec)
- apply (subst (2) and_int.rec)
- apply simp
- done
+ by (auto simp add: bit_eq_iff bit_take_bit_iff bit_and_iff)
lemma take_bit_or [simp]:
"Parity.take_bit n (k OR l) = Parity.take_bit n k OR Parity.take_bit n l"
for k l :: int
- apply (induction n arbitrary: k l)
- apply simp
- apply (subst or_int.rec)
- apply (subst (2) or_int.rec)
- apply simp
- done
+ by (auto simp add: bit_eq_iff bit_take_bit_iff bit_or_iff)
lemma take_bit_xor [simp]:
"Parity.take_bit n (k XOR l) = Parity.take_bit n k XOR Parity.take_bit n l"
for k l :: int
- apply (induction n arbitrary: k l)
- apply simp
- apply (subst xor_int.rec)
- apply (subst (2) xor_int.rec)
- apply simp
- done
+ by (auto simp add: bit_eq_iff bit_take_bit_iff bit_xor_iff)
end
--- a/src/HOL/ex/Word.thy Sun Dec 01 11:51:17 2019 +0100
+++ b/src/HOL/ex/Word.thy Mon Dec 02 10:31:51 2019 +0100
@@ -10,6 +10,19 @@
"HOL-ex.Bit_Operations"
begin
+context
+ includes lifting_syntax
+begin
+
+lemma transfer_rule_of_bool:
+ \<open>((\<longleftrightarrow>) ===> (\<cong>)) of_bool of_bool\<close>
+ if [transfer_rule]: \<open>0 \<cong> 0\<close> \<open>1 \<cong> 1\<close>
+ for R :: \<open>'a::zero_neq_one \<Rightarrow> 'b::zero_neq_one \<Rightarrow> bool\<close> (infix \<open>\<cong>\<close> 50)
+ by (unfold of_bool_def [abs_def]) transfer_prover
+
+end
+
+
subsection \<open>Preliminaries\<close>
lemma length_not_greater_eq_2_iff [simp]:
@@ -161,12 +174,18 @@
context
includes lifting_syntax
- notes transfer_rule_numeral [transfer_rule]
+ notes
+ transfer_rule_of_bool [transfer_rule]
+ transfer_rule_numeral [transfer_rule]
transfer_rule_of_nat [transfer_rule]
transfer_rule_of_int [transfer_rule]
begin
lemma [transfer_rule]:
+ "((=) ===> (pcr_word :: int \<Rightarrow> 'a::len word \<Rightarrow> bool)) of_bool of_bool"
+ by transfer_prover
+
+lemma [transfer_rule]:
"((=) ===> (pcr_word :: int \<Rightarrow> 'a::len word \<Rightarrow> bool)) numeral numeral"
by transfer_prover
@@ -324,6 +343,10 @@
\<open>a div 0 = 0\<close> for a :: \<open>'a::len0 word\<close>
by transfer simp
+(*lemma
+ \<open>a div a = of_bool (a \<noteq> 0)\<close> for a :: \<open>'a::len word\<close>
+ by transfer simp*)
+
context
includes lifting_syntax
begin
@@ -389,6 +412,11 @@
by (transfer; cases rule: length_cases [where ?'a = 'a]) (simp_all add: mod_2_eq_odd)
qed
+(*lemma
+ \<open>2 ^ n = (0 :: 'a word) \<longleftrightarrow> LENGTH('a::len) \<le> n\<close>
+ apply transfer*)
+
+
subsubsection \<open>Orderings\<close>
@@ -612,6 +640,9 @@
if \<open>even a\<close>
for a :: \<open>'a word\<close>
using that by transfer (auto dest: le_Suc_ex)
+ show \<open>(2 :: 'a word) ^ m div 2 ^ n = of_bool ((2 :: 'a word) ^ m \<noteq> 0 \<and> n \<le> m) * 2 ^ (m - n)\<close>
+ for m n :: nat
+ by transfer (simp, simp add: exp_div_exp_eq)
show "a div 2 ^ m div 2 ^ n = a div 2 ^ (m + n)"
for a :: "'a word" and m n :: nat
apply transfer
@@ -637,6 +668,23 @@
done
qed
+context
+ includes lifting_syntax
+begin
+
+lemma transfer_rule_bit_word [transfer_rule]:
+ \<open>((pcr_word :: int \<Rightarrow> 'a::len word \<Rightarrow> bool) ===> (=)) (\<lambda>k n. n < LENGTH('a) \<and> bit k n) bit\<close>
+proof -
+ let ?t = \<open>\<lambda>a n. odd (take_bit LENGTH('a) a div take_bit LENGTH('a) ((2::int) ^ n))\<close>
+ have \<open>((pcr_word :: int \<Rightarrow> 'a word \<Rightarrow> bool) ===> (=)) ?t bit\<close>
+ by (unfold bit_def) transfer_prover
+ also have \<open>?t = (\<lambda>k n. n < LENGTH('a) \<and> bit k n)\<close>
+ by (simp add: fun_eq_iff bit_take_bit_iff flip: bit_def)
+ finally show ?thesis .
+qed
+
+end
+
instantiation word :: (len) semiring_bit_shifts
begin
@@ -702,25 +750,18 @@
by simp
instance proof
- interpret bit_word: boolean_algebra "(AND)" "(OR)" NOT 0 "- 1 :: 'a word"
- proof
- show "a AND (b OR c) = a AND b OR a AND c"
- for a b c :: "'a word"
- by transfer (simp add: bit.conj_disj_distrib)
- show "a OR b AND c = (a OR b) AND (a OR c)"
- for a b c :: "'a word"
- by transfer (simp add: bit.disj_conj_distrib)
- qed (transfer; simp add: ac_simps)+
- show "boolean_algebra (AND) (OR) NOT 0 (- 1 :: 'a word)"
- by (fact bit_word.boolean_algebra_axioms)
- show "bit_word.xor = ((XOR) :: 'a word \<Rightarrow> _)"
- proof (rule ext)+
- fix a b :: "'a word"
- have "a XOR b = a AND NOT b OR NOT a AND b"
- by transfer (simp add: bit.xor_def)
- then show "bit_word.xor a b = a XOR b"
- by (simp add: bit_word.xor_def)
- qed
+ fix a b :: \<open>'a word\<close> and n :: nat
+ show \<open>even (- 1 div (2 :: 'a word) ^ n) \<longleftrightarrow> (2 :: 'a word) ^ n = 0\<close>
+ by transfer
+ (simp flip: drop_bit_eq_div add: drop_bit_take_bit, simp add: drop_bit_eq_div)
+ show \<open>bit (NOT a) n \<longleftrightarrow> (2 :: 'a word) ^ n \<noteq> 0 \<and> \<not> bit a n\<close>
+ by transfer (simp add: bit_not_iff)
+ show \<open>bit (a AND b) n \<longleftrightarrow> bit a n \<and> bit b n\<close>
+ by transfer (auto simp add: bit_and_iff)
+ show \<open>bit (a OR b) n \<longleftrightarrow> bit a n \<or> bit b n\<close>
+ by transfer (auto simp add: bit_or_iff)
+ show \<open>bit (a XOR b) n \<longleftrightarrow> bit a n \<noteq> bit b n\<close>
+ by transfer (auto simp add: bit_xor_iff)
qed
end