--- a/src/HOL/Code_Numeral.thy Mon Mar 09 19:35:07 2020 +0100
+++ b/src/HOL/Code_Numeral.thy Sun Mar 08 17:07:49 2020 +0000
@@ -88,7 +88,7 @@
lemma [transfer_rule]:
"((\<longleftrightarrow>) ===> pcr_integer) of_bool of_bool"
- by (unfold of_bool_def [abs_def]) transfer_prover
+ by (unfold of_bool_def) transfer_prover
lemma [transfer_rule]:
"((=) ===> pcr_integer) int of_nat"
@@ -108,11 +108,11 @@
lemma [transfer_rule]:
"((=) ===> (=) ===> pcr_integer) Num.sub Num.sub"
- by (unfold Num.sub_def [abs_def]) transfer_prover
+ by (unfold Num.sub_def) transfer_prover
lemma [transfer_rule]:
"(pcr_integer ===> (=) ===> pcr_integer) (^) (^)"
- by (unfold power_def [abs_def]) transfer_prover
+ by (unfold power_def) transfer_prover
end
@@ -218,13 +218,19 @@
end
-lemma [transfer_rule]:
- "rel_fun pcr_integer (rel_fun pcr_integer pcr_integer) (min :: _ \<Rightarrow> _ \<Rightarrow> int) (min :: _ \<Rightarrow> _ \<Rightarrow> integer)"
- by (unfold min_def [abs_def]) transfer_prover
+context
+ includes lifting_syntax
+begin
lemma [transfer_rule]:
- "rel_fun pcr_integer (rel_fun pcr_integer pcr_integer) (max :: _ \<Rightarrow> _ \<Rightarrow> int) (max :: _ \<Rightarrow> _ \<Rightarrow> integer)"
- by (unfold max_def [abs_def]) transfer_prover
+ \<open>(pcr_integer ===> pcr_integer ===> pcr_integer) min min\<close>
+ by (unfold min_def) transfer_prover
+
+lemma [transfer_rule]:
+ \<open>(pcr_integer ===> pcr_integer ===> pcr_integer) max max\<close>
+ by (unfold max_def) transfer_prover
+
+end
lemma int_of_integer_min [simp]:
"int_of_integer (min k l) = min (int_of_integer k) (int_of_integer l)"
@@ -304,9 +310,19 @@
end
+context
+ includes lifting_syntax
+begin
+
lemma [transfer_rule]:
- "rel_fun (=) (rel_fun pcr_integer pcr_integer) (take_bit :: _ \<Rightarrow> _ \<Rightarrow> int) (take_bit :: _ \<Rightarrow> _ \<Rightarrow> integer)"
- by (unfold take_bit_eq_mod [abs_def]) transfer_prover
+ \<open>(pcr_integer ===> (=) ===> (\<longleftrightarrow>)) bit bit\<close>
+ by (unfold bit_def) transfer_prover
+
+lemma [transfer_rule]:
+ \<open>((=) ===> pcr_integer ===> pcr_integer) take_bit take_bit\<close>
+ by (unfold take_bit_eq_mod) transfer_prover
+
+end
instance integer :: unique_euclidean_semiring_with_bit_shifts ..
@@ -372,10 +388,16 @@
where
[simp, code_post]: "Pos = numeral"
+context
+ includes lifting_syntax
+begin
+
lemma [transfer_rule]:
- "rel_fun HOL.eq pcr_integer numeral Pos"
+ \<open>((=) ===> pcr_integer) numeral Pos\<close>
by simp transfer_prover
+end
+
lemma Pos_fold [code_unfold]:
"numeral Num.One = Pos Num.One"
"numeral (Num.Bit0 k) = Pos (Num.Bit0 k)"
@@ -386,9 +408,15 @@
where
[simp, code_abbrev]: "Neg n = - Pos n"
+context
+ includes lifting_syntax
+begin
+
lemma [transfer_rule]:
- "rel_fun HOL.eq pcr_integer (\<lambda>n. - numeral n) Neg"
- by (simp add: Neg_def [abs_def]) transfer_prover
+ \<open>((=) ===> pcr_integer) (\<lambda>n. - numeral n) Neg\<close>
+ by (unfold Neg_def) transfer_prover
+
+end
code_datatype "0::integer" Pos Neg
@@ -853,33 +881,39 @@
instance natural :: Rings.dvd ..
+context
+ includes lifting_syntax
+begin
+
lemma [transfer_rule]:
- "rel_fun pcr_natural (rel_fun pcr_natural HOL.iff) Rings.dvd Rings.dvd"
- unfolding dvd_def by transfer_prover
+ \<open>(pcr_natural ===> pcr_natural ===> (\<longleftrightarrow>)) (dvd) (dvd)\<close>
+ by (unfold dvd_def) transfer_prover
lemma [transfer_rule]:
- "rel_fun (=) pcr_natural (of_bool :: bool \<Rightarrow> nat) (of_bool :: bool \<Rightarrow> natural)"
- by (unfold of_bool_def [abs_def]) transfer_prover
+ \<open>((\<longleftrightarrow>) ===> pcr_natural) of_bool of_bool\<close>
+ by (unfold of_bool_def) transfer_prover
lemma [transfer_rule]:
- "rel_fun HOL.eq pcr_natural (\<lambda>n::nat. n) (of_nat :: nat \<Rightarrow> natural)"
+ \<open>((=) ===> pcr_natural) (\<lambda>n. n) of_nat\<close>
proof -
have "rel_fun HOL.eq pcr_natural (of_nat :: nat \<Rightarrow> nat) (of_nat :: nat \<Rightarrow> natural)"
- by (unfold of_nat_def [abs_def]) transfer_prover
+ by (unfold of_nat_def) transfer_prover
then show ?thesis by (simp add: id_def)
qed
lemma [transfer_rule]:
- "rel_fun HOL.eq pcr_natural (numeral :: num \<Rightarrow> nat) (numeral :: num \<Rightarrow> natural)"
+ \<open>((=) ===> pcr_natural) numeral numeral\<close>
proof -
- have "rel_fun HOL.eq pcr_natural (numeral :: num \<Rightarrow> nat) (\<lambda>n. of_nat (numeral n))"
+ have \<open>((=) ===> pcr_natural) numeral (\<lambda>n. of_nat (numeral n))\<close>
by transfer_prover
then show ?thesis by simp
qed
lemma [transfer_rule]:
- "rel_fun pcr_natural (rel_fun (=) pcr_natural) (power :: _ \<Rightarrow> _ \<Rightarrow> nat) (power :: _ \<Rightarrow> _ \<Rightarrow> natural)"
- by (unfold power_def [abs_def]) transfer_prover
+ \<open>(pcr_natural ===> (=) ===> pcr_natural) (^) (^)\<close>
+ by (unfold power_def) transfer_prover
+
+end
lemma nat_of_natural_of_nat [simp]:
"nat_of_natural (of_nat n) = n"
@@ -921,13 +955,19 @@
end
-lemma [transfer_rule]:
- "rel_fun pcr_natural (rel_fun pcr_natural pcr_natural) (min :: _ \<Rightarrow> _ \<Rightarrow> nat) (min :: _ \<Rightarrow> _ \<Rightarrow> natural)"
- by (unfold min_def [abs_def]) transfer_prover
+context
+ includes lifting_syntax
+begin
lemma [transfer_rule]:
- "rel_fun pcr_natural (rel_fun pcr_natural pcr_natural) (max :: _ \<Rightarrow> _ \<Rightarrow> nat) (max :: _ \<Rightarrow> _ \<Rightarrow> natural)"
- by (unfold max_def [abs_def]) transfer_prover
+ \<open>(pcr_natural ===> pcr_natural ===> pcr_natural) min min\<close>
+ by (unfold min_def) transfer_prover
+
+lemma [transfer_rule]:
+ \<open>(pcr_natural ===> pcr_natural ===> pcr_natural) max max\<close>
+ by (unfold max_def) transfer_prover
+
+end
lemma nat_of_natural_min [simp]:
"nat_of_natural (min k l) = min (nat_of_natural k) (nat_of_natural l)"
@@ -1001,9 +1041,19 @@
end
+context
+ includes lifting_syntax
+begin
+
lemma [transfer_rule]:
- "rel_fun (=) (rel_fun pcr_natural pcr_natural) (take_bit :: _ \<Rightarrow> _ \<Rightarrow> nat) (take_bit :: _ \<Rightarrow> _ \<Rightarrow> natural)"
- by (unfold take_bit_eq_mod [abs_def]) transfer_prover
+ \<open>(pcr_natural ===> (=) ===> (\<longleftrightarrow>)) bit bit\<close>
+ by (unfold bit_def) transfer_prover
+
+lemma [transfer_rule]:
+ \<open>((=) ===> pcr_natural ===> pcr_natural) take_bit take_bit\<close>
+ by (unfold take_bit_eq_mod) transfer_prover
+
+end
instance natural :: unique_euclidean_semiring_with_bit_shifts ..
--- a/src/HOL/Euclidean_Division.thy Mon Mar 09 19:35:07 2020 +0100
+++ b/src/HOL/Euclidean_Division.thy Sun Mar 08 17:07:49 2020 +0000
@@ -2002,6 +2002,10 @@
by (simp add: of_nat_mod of_nat_diff)
qed
+lemma of_bool_half_eq_0 [simp]:
+ \<open>of_bool b div 2 = 0\<close>
+ by simp
+
end
class unique_euclidean_ring_with_nat = ring + unique_euclidean_semiring_with_nat
--- a/src/HOL/Parity.thy Mon Mar 09 19:35:07 2020 +0100
+++ b/src/HOL/Parity.thy Sun Mar 08 17:07:49 2020 +0000
@@ -168,6 +168,15 @@
by simp
qed
+lemma mask_eq_seq_sum:
+ \<open>2 ^ n - 1 = ((\<lambda>k. 1 + k * 2) ^^ n) 0\<close>
+proof -
+ have \<open>2 ^ n = ((\<lambda>k. 1 + k * 2) ^^ n) 0 + 1\<close>
+ by (induction n) (simp_all add: ac_simps mult_2)
+ then show ?thesis
+ by simp
+qed
+
end
class ring_parity = ring + semiring_parity
@@ -742,10 +751,14 @@
\<open>bit a 0 \<longleftrightarrow> odd a\<close>
by (simp add: bit_def)
-lemma bit_Suc [simp]:
+lemma bit_Suc:
\<open>bit a (Suc n) \<longleftrightarrow> bit (a div 2) n\<close>
using div_exp_eq [of a 1 n] by (simp add: bit_def)
+lemma bit_rec:
+ \<open>bit a n \<longleftrightarrow> (if n = 0 then odd a else bit (a div 2) (n - 1))\<close>
+ by (cases n) (simp_all add: bit_Suc)
+
lemma bit_0_eq [simp]:
\<open>bit 0 = bot\<close>
by (simp add: fun_eq_iff bit_def)
@@ -768,7 +781,7 @@
lemma stable_imp_bit_iff_odd:
\<open>bit a n \<longleftrightarrow> odd a\<close>
- by (induction n) (simp_all add: stable)
+ by (induction n) (simp_all add: stable bit_Suc)
end
@@ -781,11 +794,11 @@
next
case (rec a b)
from rec.prems [of 1] have [simp]: \<open>b = odd a\<close>
- by (simp add: rec.hyps)
+ by (simp add: rec.hyps bit_Suc)
from rec.hyps have hyp: \<open>(of_bool (odd a) + 2 * a) div 2 = a\<close>
by simp
have \<open>bit a n \<longleftrightarrow> odd a\<close> for n
- using rec.prems [of \<open>Suc n\<close>] by (simp add: hyp)
+ using rec.prems [of \<open>Suc n\<close>] by (simp add: hyp bit_Suc)
then have \<open>a div 2 = a\<close>
by (rule rec.IH)
then have \<open>of_bool (odd a) + 2 * a = 2 * (a div 2) + of_bool (odd a)\<close>
@@ -841,7 +854,7 @@
from rec.prems [of 0] have [simp]: \<open>p = odd b\<close>
by simp
from rec.hyps have \<open>bit a n \<longleftrightarrow> bit (b div 2) n\<close> for n
- using rec.prems [of \<open>Suc n\<close>] by simp
+ using rec.prems [of \<open>Suc n\<close>] by (simp add: bit_Suc)
then have \<open>a = b div 2\<close>
by (rule rec.IH)
then have \<open>2 * a = 2 * (b div 2)\<close>
@@ -912,7 +925,7 @@
moreover from \<open>a div 2 = b div 2\<close> have \<open>bit (a div 2) n = bit (b div 2) n\<close>
by simp
ultimately show ?thesis
- by simp
+ by (simp add: bit_Suc)
qed
qed
qed
@@ -1182,7 +1195,7 @@
"take_bit 0 a = 0"
by (simp add: take_bit_eq_mod)
-lemma take_bit_Suc [simp]:
+lemma take_bit_Suc:
\<open>take_bit (Suc n) a = take_bit n (a div 2) * 2 + of_bool (odd a)\<close>
proof -
have \<open>take_bit (Suc n) (a div 2 * 2 + of_bool (odd a)) = take_bit n (a div 2) * 2 + of_bool (odd a)\<close>
@@ -1193,13 +1206,17 @@
using div_mult_mod_eq [of a 2] by (simp add: mod_2_eq_odd)
qed
+lemma take_bit_rec:
+ \<open>take_bit n a = (if n = 0 then 0 else take_bit (n - 1) (a div 2) * 2 + of_bool (odd a))\<close>
+ by (cases n) (simp_all add: take_bit_Suc)
+
lemma take_bit_of_0 [simp]:
"take_bit n 0 = 0"
by (simp add: take_bit_eq_mod)
lemma take_bit_of_1 [simp]:
"take_bit n 1 = of_bool (n > 0)"
- by (cases n) simp_all
+ by (cases n) (simp_all add: take_bit_Suc)
lemma drop_bit_of_0 [simp]:
"drop_bit n 0 = 0"
@@ -1213,16 +1230,20 @@
"drop_bit 0 = id"
by (simp add: fun_eq_iff drop_bit_eq_div)
-lemma drop_bit_Suc [simp]:
+lemma drop_bit_Suc:
"drop_bit (Suc n) a = drop_bit n (a div 2)"
using div_exp_eq [of a 1] by (simp add: drop_bit_eq_div)
+lemma drop_bit_rec:
+ "drop_bit n a = (if n = 0 then a else drop_bit (n - 1) (a div 2))"
+ by (cases n) (simp_all add: drop_bit_Suc)
+
lemma drop_bit_half:
"drop_bit n (a div 2) = drop_bit n a div 2"
- by (induction n arbitrary: a) simp_all
+ by (induction n arbitrary: a) (simp_all add: drop_bit_Suc)
lemma drop_bit_of_bool [simp]:
- "drop_bit n (of_bool d) = of_bool (n = 0 \<and> d)"
+ "drop_bit n (of_bool b) = of_bool (n = 0 \<and> b)"
by (cases n) simp_all
lemma take_bit_eq_0_imp_dvd:
@@ -1231,7 +1252,7 @@
lemma even_take_bit_eq [simp]:
\<open>even (take_bit n a) \<longleftrightarrow> n = 0 \<or> even a\<close>
- by (cases n) simp_all
+ by (simp add: take_bit_rec [of n a])
lemma take_bit_take_bit [simp]:
"take_bit m (take_bit n a) = take_bit (min m n) a"
@@ -1302,6 +1323,21 @@
\<open>bit (take_bit m a) n \<longleftrightarrow> n < m \<and> bit a n\<close>
by (simp add: bit_def drop_bit_take_bit not_le flip: drop_bit_eq_div)
+lemma stable_imp_drop_bit_eq:
+ \<open>drop_bit n a = a\<close>
+ if \<open>a div 2 = a\<close>
+ by (induction n) (simp_all add: that drop_bit_Suc)
+
+lemma stable_imp_take_bit_eq:
+ \<open>take_bit n a = (if even a then 0 else 2 ^ n - 1)\<close>
+ if \<open>a div 2 = a\<close>
+proof (rule bit_eqI)
+ fix m
+ assume \<open>2 ^ m \<noteq> 0\<close>
+ with that show \<open>bit (take_bit n a) m \<longleftrightarrow> bit (if even a then 0 else 2 ^ n - 1) m\<close>
+ by (simp add: bit_take_bit_iff bit_mask_iff stable_imp_bit_iff_odd)
+qed
+
end
instantiation nat :: semiring_bit_shifts
--- a/src/HOL/Set_Interval.thy Mon Mar 09 19:35:07 2020 +0100
+++ b/src/HOL/Set_Interval.thy Sun Mar 08 17:07:49 2020 +0000
@@ -2072,7 +2072,7 @@
begin
lemma take_bit_sum:
- "take_bit n a = (\<Sum>k = 0..<n. push_bit k (of_bool (odd (drop_bit k a))))"
+ "take_bit n a = (\<Sum>k = 0..<n. push_bit k (of_bool (bit a k)))"
for n :: nat
proof (induction n arbitrary: a)
case 0
@@ -2080,14 +2080,14 @@
by simp
next
case (Suc n)
- have "(\<Sum>k = 0..<Suc n. push_bit k (of_bool (odd (drop_bit k a)))) =
- of_bool (odd a) + (\<Sum>k = Suc 0..<Suc n. push_bit k (of_bool (odd (drop_bit k a))))"
+ have "(\<Sum>k = 0..<Suc n. push_bit k (of_bool (bit a k))) =
+ of_bool (odd a) + (\<Sum>k = Suc 0..<Suc n. push_bit k (of_bool (bit a k)))"
by (simp add: sum.atLeast_Suc_lessThan ac_simps)
- also have "(\<Sum>k = Suc 0..<Suc n. push_bit k (of_bool (odd (drop_bit k a))))
- = (\<Sum>k = 0..<n. push_bit k (of_bool (odd (drop_bit k (a div 2))))) * 2"
- by (simp only: sum.atLeast_Suc_lessThan_Suc_shift) (simp add: sum_distrib_right push_bit_double)
+ also have "(\<Sum>k = Suc 0..<Suc n. push_bit k (of_bool (bit a k)))
+ = (\<Sum>k = 0..<n. push_bit k (of_bool (bit (a div 2) k))) * 2"
+ by (simp only: sum.atLeast_Suc_lessThan_Suc_shift) (simp add: sum_distrib_right push_bit_double drop_bit_Suc bit_Suc)
finally show ?case
- using Suc [of "a div 2"] by (simp add: ac_simps)
+ using Suc [of "a div 2"] by (simp add: ac_simps take_bit_Suc)
qed
end
--- a/src/HOL/String.thy Mon Mar 09 19:35:07 2020 +0100
+++ b/src/HOL/String.thy Sun Mar 08 17:07:49 2020 +0000
@@ -21,6 +21,81 @@
subsubsection \<open>Bytes as datatype\<close>
+context unique_euclidean_semiring_with_bit_shifts
+begin
+
+lemma bit_horner_sum_iff:
+ \<open>bit (foldr (\<lambda>b k. of_bool b + k * 2) bs 0) n \<longleftrightarrow> n < length bs \<and> bs ! n\<close>
+proof (induction bs arbitrary: n)
+ case Nil
+ then show ?case
+ by simp
+next
+ case (Cons b bs)
+ show ?case
+ proof (cases n)
+ case 0
+ then show ?thesis
+ by simp
+ next
+ case (Suc m)
+ with bit_rec [of _ n] Cons.prems Cons.IH [of m]
+ show ?thesis by simp
+ qed
+qed
+
+lemma take_bit_horner_sum_eq:
+ \<open>take_bit n (foldr (\<lambda>b k. of_bool b + k * 2) bs 0) = foldr (\<lambda>b k. of_bool b + k * 2) (take n bs) 0\<close>
+proof (induction bs arbitrary: n)
+ case Nil
+ then show ?case
+ by simp
+next
+ case (Cons b bs)
+ show ?case
+ proof (cases n)
+ case 0
+ then show ?thesis
+ by simp
+ next
+ case (Suc m)
+ with take_bit_rec [of n] Cons.prems Cons.IH [of m]
+ show ?thesis by (simp add: ac_simps)
+ qed
+qed
+
+lemma (in semiring_bit_shifts) take_bit_eq_horner_sum:
+ \<open>take_bit n a = foldr (\<lambda>b k. of_bool b + k * 2) (map (bit a) [0..<n]) 0\<close>
+proof (induction a arbitrary: n rule: bits_induct)
+ case (stable a)
+ have *: \<open>((\<lambda>k. k * 2) ^^ n) 0 = 0\<close>
+ by (induction n) simp_all
+ from stable have \<open>bit a = (\<lambda>_. odd a)\<close>
+ by (simp add: stable_imp_bit_iff_odd fun_eq_iff)
+ then have \<open>map (bit a) [0..<n] = replicate n (odd a)\<close>
+ by (simp add: map_replicate_const)
+ with stable show ?case
+ by (simp add: stable_imp_take_bit_eq mask_eq_seq_sum *)
+next
+ case (rec a b)
+ show ?case
+ proof (cases n)
+ case 0
+ then show ?thesis
+ by simp
+ next
+ case (Suc m)
+ have \<open>map (bit (of_bool b + 2 * a)) [0..<Suc m] = b # map (bit (of_bool b + 2 * a)) [Suc 0..<Suc m]\<close>
+ by (simp only: upt_conv_Cons) simp
+ also have \<open>\<dots> = b # map (bit a) [0..<m]\<close>
+ by (simp only: flip: map_Suc_upt) (simp add: bit_Suc rec.hyps)
+ finally show ?thesis
+ using Suc rec.IH [of m] by (simp add: take_bit_Suc rec.hyps, simp add: ac_simps)
+ qed
+qed
+
+end
+
datatype char =
Char (digit0: bool) (digit1: bool) (digit2: bool) (digit3: bool)
(digit4: bool) (digit5: bool) (digit6: bool) (digit7: bool)
@@ -28,49 +103,37 @@
context comm_semiring_1
begin
-definition of_char :: "char \<Rightarrow> 'a"
- where "of_char c = ((((((of_bool (digit7 c) * 2
- + of_bool (digit6 c)) * 2
- + of_bool (digit5 c)) * 2
- + of_bool (digit4 c)) * 2
- + of_bool (digit3 c)) * 2
- + of_bool (digit2 c)) * 2
- + of_bool (digit1 c)) * 2
- + of_bool (digit0 c)"
+definition of_char :: \<open>char \<Rightarrow> 'a\<close>
+ where \<open>of_char c = foldr (\<lambda>b k. of_bool b + k * 2)
+ [digit0 c, digit1 c, digit2 c, digit3 c, digit4 c, digit5 c, digit6 c, digit7 c] 0\<close>
lemma of_char_Char [simp]:
- "of_char (Char b0 b1 b2 b3 b4 b5 b6 b7) =
- foldr (\<lambda>b k. of_bool b + k * 2) [b0, b1, b2, b3, b4, b5, b6, b7] 0"
- by (simp add: of_char_def ac_simps)
+ \<open>of_char (Char b0 b1 b2 b3 b4 b5 b6 b7) =
+ foldr (\<lambda>b k. of_bool b + k * 2) [b0, b1, b2, b3, b4, b5, b6, b7] 0\<close>
+ by (simp add: of_char_def)
end
context unique_euclidean_semiring_with_bit_shifts
begin
-definition char_of :: "'a \<Rightarrow> char"
- where "char_of n = Char (odd n) (odd (drop_bit 1 n))
- (odd (drop_bit 2 n)) (odd (drop_bit 3 n))
- (odd (drop_bit 4 n)) (odd (drop_bit 5 n))
- (odd (drop_bit 6 n)) (odd (drop_bit 7 n))"
+definition char_of :: \<open>'a \<Rightarrow> char\<close>
+ where \<open>char_of n = Char (odd n) (bit n 1) (bit n 2) (bit n 3) (bit n 4) (bit n 5) (bit n 6) (bit n 7)\<close>
+
+lemma char_of_take_bit_eq:
+ \<open>char_of (take_bit n m) = char_of m\<close> if \<open>n \<ge> 8\<close>
+ using that by (simp add: char_of_def bit_take_bit_iff)
lemma char_of_char [simp]:
- "char_of (of_char c) = c"
-proof (cases c)
- have **: "drop_bit n (q * 2 + of_bool d) = drop_bit (n - 1) q + drop_bit n (of_bool d)"
- if "n > 0" for q :: 'a and n :: nat and d :: bool
- using that by (cases n) simp_all
- case (Char d0 d1 d2 d3 d4 d5 d6 d7)
- then show ?thesis
- by (simp only: of_char_def char_of_def char.simps char.sel drop_bit_of_bool **) simp
-qed
+ \<open>char_of (of_char c) = c\<close>
+ by (simp only: of_char_def char_of_def bit_horner_sum_iff) simp
lemma char_of_comp_of_char [simp]:
"char_of \<circ> of_char = id"
by (simp add: fun_eq_iff)
lemma inj_of_char:
- "inj of_char"
+ \<open>inj of_char\<close>
proof (rule injI)
fix c d
assume "of_char c = of_char d"
@@ -79,45 +142,61 @@
then show "c = d"
by simp
qed
-
+
+lemma of_char_eqI:
+ \<open>c = d\<close> if \<open>of_char c = of_char d\<close>
+ using that inj_of_char by (simp add: inj_eq)
+
lemma of_char_eq_iff [simp]:
- "of_char c = of_char d \<longleftrightarrow> c = d"
- by (simp add: inj_eq inj_of_char)
+ \<open>of_char c = of_char d \<longleftrightarrow> c = d\<close>
+ by (auto intro: of_char_eqI)
lemma of_char_of [simp]:
- "of_char (char_of a) = a mod 256"
+ \<open>of_char (char_of a) = a mod 256\<close>
proof -
- have *: "{0::nat..<8} = {0, 1, 2, 3, 4, 5, 6, 7}"
- by auto
- have "of_char (char_of (take_bit 8 a)) =
- (\<Sum>k\<in>{0, 1, 2, 3, 4, 5, 6, 7}. push_bit k (of_bool (odd (drop_bit k a))))"
- by (simp add: of_char_def char_of_def push_bit_of_1 drop_bit_take_bit)
- also have "\<dots> = take_bit 8 a"
- using * take_bit_sum [of 8 a] by simp
- also have "char_of(take_bit 8 a) = char_of a"
- by (simp add: char_of_def drop_bit_take_bit)
- finally show ?thesis
+ have \<open>[0..<8] = [0, Suc 0, 2, 3, 4, 5, 6, 7 :: nat]\<close>
+ by (simp add: upt_eq_Cons_conv)
+ then have \<open>[odd a, bit a 1, bit a 2, bit a 3, bit a 4, bit a 5, bit a 6, bit a 7] = map (bit a) [0..<8]\<close>
+ by simp
+ then have \<open>of_char (char_of a) = take_bit 8 a\<close>
+ by (simp only: char_of_def of_char_def char.sel take_bit_eq_horner_sum)
+ then show ?thesis
by (simp add: take_bit_eq_mod)
qed
lemma char_of_mod_256 [simp]:
- "char_of (n mod 256) = char_of n"
- by (metis char_of_char of_char_of)
+ \<open>char_of (n mod 256) = char_of n\<close>
+ by (rule of_char_eqI) simp
lemma of_char_mod_256 [simp]:
- "of_char c mod 256 = of_char c"
- by (metis char_of_char of_char_of)
+ \<open>of_char c mod 256 = of_char c\<close>
+proof -
+ have \<open>of_char (char_of (of_char c)) mod 256 = of_char (char_of (of_char c))\<close>
+ by (simp only: of_char_of) simp
+ then show ?thesis
+ by simp
+qed
lemma char_of_quasi_inj [simp]:
- "char_of m = char_of n \<longleftrightarrow> m mod 256 = n mod 256"
- by (metis char_of_mod_256 of_char_of)
+ \<open>char_of m = char_of n \<longleftrightarrow> m mod 256 = n mod 256\<close> (is \<open>?P \<longleftrightarrow> ?Q\<close>)
+proof
+ assume ?Q
+ then show ?P
+ by (auto intro: of_char_eqI)
+next
+ assume ?P
+ then have \<open>of_char (char_of m) = of_char (char_of n)\<close>
+ by simp
+ then show ?Q
+ by simp
+qed
-lemma char_of_nat_eq_iff:
- "char_of n = c \<longleftrightarrow> take_bit 8 n = of_char c"
- by (simp add: take_bit_eq_mod) (use of_char_eq_iff in fastforce)
+lemma char_of_eq_iff:
+ \<open>char_of n = c \<longleftrightarrow> take_bit 8 n = of_char c\<close>
+ by (auto intro: of_char_eqI simp add: take_bit_eq_mod)
lemma char_of_nat [simp]:
- "char_of (of_nat n) = char_of n"
+ \<open>char_of (of_nat n) = char_of n\<close>
by (simp add: char_of_def String.char_of_def drop_bit_of_nat)
end
@@ -168,20 +247,20 @@
begin
lemma [transfer_rule]:
- "(pcr_integer ===> (=)) (char_of :: int \<Rightarrow> char) (char_of :: integer \<Rightarrow> char)"
- by (unfold char_of_def [abs_def]) transfer_prover
+ \<open>(pcr_integer ===> (=)) char_of char_of\<close>
+ by (unfold char_of_def) transfer_prover
lemma [transfer_rule]:
- "((=) ===> pcr_integer) (of_char :: char \<Rightarrow> int) (of_char :: char \<Rightarrow> integer)"
- by (unfold of_char_def [abs_def]) transfer_prover
+ \<open>((=) ===> pcr_integer) of_char of_char\<close>
+ by (unfold of_char_def) transfer_prover
lemma [transfer_rule]:
- "(pcr_natural ===> (=)) (char_of :: nat \<Rightarrow> char) (char_of :: natural \<Rightarrow> char)"
- by (unfold char_of_def [abs_def]) transfer_prover
+ \<open>(pcr_natural ===> (=)) char_of char_of\<close>
+ by (unfold char_of_def) transfer_prover
lemma [transfer_rule]:
- "((=) ===> pcr_natural) (of_char :: char \<Rightarrow> nat) (of_char :: char \<Rightarrow> natural)"
- by (unfold of_char_def [abs_def]) transfer_prover
+ \<open>((=) ===> pcr_natural) of_char of_char\<close>
+ by (unfold of_char_def) transfer_prover
end
@@ -326,7 +405,7 @@
(q6, b6) = bit_cut_integer q5;
(_, b7) = bit_cut_integer q6
in Char b0 b1 b2 b3 b4 b5 b6 b7)"
- by (simp add: bit_cut_integer_def char_of_integer_def char_of_def div_mult2_numeral_eq odd_iff_mod_2_eq_one drop_bit_eq_div)
+ by (simp add: bit_cut_integer_def char_of_integer_def char_of_def div_mult2_numeral_eq bit_iff_odd_drop_bit drop_bit_eq_div)
lemma integer_of_char_code [code]:
"integer_of_char (Char b0 b1 b2 b3 b4 b5 b6 b7) =
@@ -334,7 +413,7 @@
of_bool b5) * 2 + of_bool b4) * 2 +
of_bool b3) * 2 + of_bool b2) * 2 +
of_bool b1) * 2 + of_bool b0"
- by (simp only: integer_of_char_def of_char_def char.sel)
+ by (simp add: integer_of_char_def of_char_def)
subsection \<open>Strings as dedicated type for target language code generation\<close>
@@ -361,8 +440,7 @@
qualified lemma char_of_ascii_of [simp]:
"of_char (ascii_of c) = take_bit 7 (of_char c :: nat)"
- by (cases c)
- (simp add: numeral_3_eq_3 [symmetric] numeral_2_eq_2 [symmetric])
+ by (cases c) (simp only: ascii_of_Char of_char_Char take_bit_horner_sum_eq, simp)
qualified typedef literal = "{cs. \<forall>c\<in>set cs. \<not> digit7 c}"
morphisms explode Abs_literal
@@ -632,9 +710,17 @@
where [simp]: "Literal' = String.Literal"
lemma [code]:
- "Literal' b0 b1 b2 b3 b4 b5 b6 s = String.literal_of_asciis
- [foldr (\<lambda>b k. of_bool b + k * 2) [b0, b1, b2, b3, b4, b5, b6] 0] + s"
- unfolding Literal'_def by transfer (simp add: char_of_def)
+ \<open>Literal' b0 b1 b2 b3 b4 b5 b6 s = String.literal_of_asciis
+ [foldr (\<lambda>b k. of_bool b + k * 2) [b0, b1, b2, b3, b4, b5, b6] 0] + s\<close>
+proof -
+ have \<open>foldr (\<lambda>b k. of_bool b + k * 2) [b0, b1, b2, b3, b4, b5, b6] 0 = of_char (Char b0 b1 b2 b3 b4 b5 b6 False)\<close>
+ by simp
+ moreover have \<open>Literal' b0 b1 b2 b3 b4 b5 b6 s = String.literal_of_asciis
+ [of_char (Char b0 b1 b2 b3 b4 b5 b6 False)] + s\<close>
+ by (unfold Literal'_def) (transfer, simp only: list.simps comp_apply char_of_char, simp)
+ ultimately show ?thesis
+ by simp
+qed
lemma [code_computation_unfold]:
"String.Literal = Literal'"
--- a/src/HOL/ex/Bit_Lists.thy Mon Mar 09 19:35:07 2020 +0100
+++ b/src/HOL/ex/Bit_Lists.thy Sun Mar 08 17:07:49 2020 +0000
@@ -1,4 +1,4 @@
-(* Author: Florian Haftmann, TUM
+ (* Author: Florian Haftmann, TUM
*)
section \<open>Proof(s) of concept for algebraically founded lists of bits\<close>
@@ -44,11 +44,11 @@
next
case (Cons b bs)
then show ?case
- by (cases n) (simp_all add: ac_simps)
+ by (cases n) (simp_all add: ac_simps take_bit_Suc)
qed
lemma unsigned_of_bits_drop [simp]:
- "unsigned_of_bits (drop n bs) = Parity.drop_bit n (unsigned_of_bits bs)"
+ "unsigned_of_bits (drop n bs) = drop_bit n (unsigned_of_bits bs)"
proof (induction bs arbitrary: n)
case Nil
then show ?case
@@ -56,7 +56,7 @@
next
case (Cons b bs)
then show ?case
- by (cases n) simp_all
+ by (cases n) (simp_all add: drop_bit_Suc)
qed
lemma bit_unsigned_of_bits_iff:
@@ -68,7 +68,7 @@
next
case (Cons b bs)
then show ?case
- by (cases n) simp_all
+ by (cases n) (simp_all add: bit_Suc)
qed
primrec n_bits_of :: "nat \<Rightarrow> 'a \<Rightarrow> bool list"
@@ -77,9 +77,9 @@
| "n_bits_of (Suc n) a = odd a # n_bits_of n (a div 2)"
lemma n_bits_of_eq_iff:
- "n_bits_of n a = n_bits_of n b \<longleftrightarrow> Parity.take_bit n a = Parity.take_bit n b"
+ "n_bits_of n a = n_bits_of n b \<longleftrightarrow> take_bit n a = take_bit n b"
apply (induction n arbitrary: a b)
- apply (auto elim!: evenE oddE)
+ apply (auto elim!: evenE oddE simp add: take_bit_Suc)
apply (metis dvd_triv_right even_plus_one_iff)
apply (metis dvd_triv_right even_plus_one_iff)
done
@@ -97,8 +97,8 @@
qed
lemma unsigned_of_bits_n_bits_of [simp]:
- "unsigned_of_bits (n_bits_of n a) = Parity.take_bit n a"
- by (induction n arbitrary: a) (simp_all add: ac_simps)
+ "unsigned_of_bits (n_bits_of n a) = take_bit n a"
+ by (induction n arbitrary: a) (simp_all add: ac_simps take_bit_Suc)
end
@@ -236,7 +236,7 @@
next
case (Cons b bs)
then show ?case
- by (cases n; cases b; cases bs) simp_all
+ by (cases n; cases b; cases bs) (simp_all add: bit_Suc)
qed
lemma of_bits_append [simp]:
@@ -257,7 +257,7 @@
by (auto simp add: of_bits_int_def)
lemma of_bits_drop [simp]:
- "of_bits (drop n bs) = Parity.drop_bit n (of_bits bs :: int)"
+ "of_bits (drop n bs) = drop_bit n (of_bits bs :: int)"
if "n < length bs"
using that proof (induction bs arbitrary: n)
case Nil
@@ -275,7 +275,7 @@
with Cons.prems have "bs \<noteq> []"
by auto
with Suc Cons.IH [of n] Cons.prems show ?thesis
- by (cases b) simp_all
+ by (cases b) (simp_all add: drop_bit_Suc)
qed
qed
--- a/src/HOL/ex/Bit_Operations.thy Mon Mar 09 19:35:07 2020 +0100
+++ b/src/HOL/ex/Bit_Operations.thy Sun Mar 08 17:07:49 2020 +0000
@@ -28,10 +28,6 @@
are specified as definitional class operations.
\<close>
-lemma stable_imp_drop_eq:
- \<open>drop_bit n a = a\<close> if \<open>a div 2 = a\<close>
- by (induction n) (simp_all add: that)
-
sublocale "and": semilattice \<open>(AND)\<close>
by standard (auto simp add: bit_eq_iff bit_and_iff)
@@ -219,7 +215,7 @@
assume *: \<open>2 ^ m \<noteq> 0\<close>
then show \<open>bit (set_bit 0 a) m = bit (1 + 2 * (a div 2)) m\<close>
by (simp add: bit_set_bit_iff bit_double_iff even_bit_succ_iff)
- (cases m, simp_all)
+ (cases m, simp_all add: bit_Suc)
qed
lemma set_bit_Suc [simp]:
@@ -239,7 +235,7 @@
show ?thesis
by (cases a rule: parity_cases)
(simp_all add: bit_set_bit_iff bit_double_iff even_bit_succ_iff *,
- simp_all add: Suc \<open>2 ^ m \<noteq> 0\<close>)
+ simp_all add: Suc \<open>2 ^ m \<noteq> 0\<close> bit_Suc)
qed
qed
@@ -250,7 +246,7 @@
assume *: \<open>2 ^ m \<noteq> 0\<close>
then show \<open>bit (unset_bit 0 a) m = bit (2 * (a div 2)) m\<close>
by (simp add: bit_unset_bit_iff bit_double_iff)
- (cases m, simp_all)
+ (cases m, simp_all add: bit_Suc)
qed
lemma unset_bit_Suc [simp]:
@@ -268,7 +264,7 @@
show ?thesis
by (cases a rule: parity_cases)
(simp_all add: bit_unset_bit_iff bit_double_iff even_bit_succ_iff *,
- simp_all add: Suc)
+ simp_all add: Suc bit_Suc)
qed
qed
@@ -279,7 +275,7 @@
assume *: \<open>2 ^ m \<noteq> 0\<close>
then show \<open>bit (flip_bit 0 a) m = bit (of_bool (even a) + 2 * (a div 2)) m\<close>
by (simp add: bit_flip_bit_iff bit_double_iff even_bit_succ_iff)
- (cases m, simp_all)
+ (cases m, simp_all add: bit_Suc)
qed
lemma flip_bit_Suc [simp]:
@@ -299,7 +295,7 @@
show ?thesis
by (cases a rule: parity_cases)
(simp_all add: bit_flip_bit_iff bit_double_iff even_bit_succ_iff,
- simp_all add: Suc \<open>2 ^ m \<noteq> 0\<close>)
+ simp_all add: Suc \<open>2 ^ m \<noteq> 0\<close> bit_Suc)
qed
qed
@@ -348,7 +344,7 @@
next
case (Suc n)
then show ?case
- by (simp add: rec [of m n])
+ by (simp add: rec [of m n] bit_Suc)
qed
sublocale abel_semigroup F
@@ -461,7 +457,7 @@
next
case (Suc n)
then show ?case
- by (simp add: rec [of k l])
+ by (simp add: rec [of k l] bit_Suc)
qed
sublocale abel_semigroup F
@@ -514,7 +510,7 @@
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_div_2 even_not_iff_int)
+ by (induction n arbitrary: k) (simp_all add: not_int_div_2 even_not_iff_int bit_Suc)
instance proof
fix k l :: int and n :: nat
--- a/src/HOL/ex/Word.thy Mon Mar 09 19:35:07 2020 +0100
+++ b/src/HOL/ex/Word.thy Sun Mar 08 17:07:49 2020 +0000
@@ -29,16 +29,16 @@
then have "(k + 1) mod 2 = 1"
by (simp add: even_iff_mod_2_eq_zero)
with True show ?thesis
- by (simp add: signed_take_bit_eq_take_bit)
+ by (simp add: signed_take_bit_eq_take_bit take_bit_Suc)
next
case False
then show ?thesis
- by (simp add: signed_take_bit_eq_take_bit odd_iff_mod_2_eq_one)
+ by (simp add: signed_take_bit_eq_take_bit odd_iff_mod_2_eq_one take_bit_Suc)
qed
-lemma signed_take_bit_Suc [simp]:
+lemma signed_take_bit_Suc:
"signed_take_bit (Suc n) k = signed_take_bit n (k div 2) * 2 + k mod 2"
- by (simp add: odd_iff_mod_2_eq_one signed_take_bit_eq_take_bit algebra_simps)
+ by (simp add: odd_iff_mod_2_eq_one signed_take_bit_eq_take_bit algebra_simps take_bit_Suc)
lemma signed_take_bit_of_0 [simp]:
"signed_take_bit n 0 = 0"
@@ -46,7 +46,7 @@
lemma signed_take_bit_of_minus_1 [simp]:
"signed_take_bit n (- 1) = - 1"
- by (induct n) simp_all
+ by (induct n) (simp_all add: signed_take_bit_Suc)
lemma signed_take_bit_eq_iff_take_bit_eq:
"signed_take_bit (n - Suc 0) k = signed_take_bit (n - Suc 0) l \<longleftrightarrow> take_bit n k = take_bit n l" (is "?P \<longleftrightarrow> ?Q")
@@ -356,10 +356,10 @@
by transfer simp
show even_iff_mod_2_eq_0: "2 dvd a \<longleftrightarrow> a mod 2 = 0"
for a :: "'a word"
- by transfer (simp_all add: mod_2_eq_odd)
+ by transfer (simp_all add: mod_2_eq_odd take_bit_Suc)
show "\<not> 2 dvd a \<longleftrightarrow> a mod 2 = 1"
for a :: "'a word"
- by transfer (simp_all add: mod_2_eq_odd)
+ by transfer (simp_all add: mod_2_eq_odd take_bit_Suc)
qed
@@ -494,7 +494,7 @@
have \<open>of_bool (odd k) < (1 :: int) \<longleftrightarrow> even k\<close> for k :: int
by auto
with False that show ?thesis
- by (auto; transfer) simp_all
+ by transfer (simp add: eq_iff)
next
case True
obtain n where length: \<open>LENGTH('a) = Suc n\<close>
@@ -533,7 +533,7 @@
by (simp add: take_bit_eq_mod)
with True show \<open>take_bit LENGTH('a) (take_bit LENGTH('a) (1 + k * 2) div take_bit LENGTH('a) 2)
= take_bit LENGTH('a) k\<close>
- by auto
+ by (auto simp add: take_bit_Suc)
qed
ultimately show ?thesis
by simp
@@ -592,7 +592,7 @@
show \<open>(1 + a) div 2 = a div 2\<close>
if \<open>even a\<close>
for a :: \<open>'a word\<close>
- using that by transfer (auto dest: le_Suc_ex)
+ using that by transfer (auto dest: le_Suc_ex simp add: take_bit_Suc)
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)