--- a/src/HOL/Bit_Operations.thy Fri Oct 29 00:01:14 2021 +0200
+++ b/src/HOL/Bit_Operations.thy Thu Oct 28 06:39:36 2021 +0000
@@ -3098,7 +3098,7 @@
where \<open>take_bit_num n m =
(if take_bit n (numeral m ::nat) = 0 then None else Some (num_of_nat (take_bit n (numeral m ::nat))))\<close>
-lemma take_bit_num_simps [code]:
+lemma take_bit_num_simps:
\<open>take_bit_num 0 m = None\<close>
\<open>take_bit_num (Suc n) Num.One =
Some Num.One\<close>
@@ -3106,18 +3106,23 @@
(case take_bit_num n m of None \<Rightarrow> None | Some q \<Rightarrow> Some (Num.Bit0 q))\<close>
\<open>take_bit_num (Suc n) (Num.Bit1 m) =
Some (case take_bit_num n 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
- take_bit_Suc_bit0 take_bit_Suc_bit1)
-
-lemma take_bit_num_numeral_simps:
- \<open>take_bit_num (numeral n) Num.One =
+ \<open>take_bit_num (numeral r) Num.One =
Some Num.One\<close>
- \<open>take_bit_num (numeral n) (Num.Bit0 m) =
- (case take_bit_num (pred_numeral n) m of None \<Rightarrow> None | Some q \<Rightarrow> Some (Num.Bit0 q))\<close>
- \<open>take_bit_num (numeral n) (Num.Bit1 m) =
- Some (case take_bit_num (pred_numeral n) m of None \<Rightarrow> Num.One | Some q \<Rightarrow> Num.Bit1 q)\<close>
+ \<open>take_bit_num (numeral r) (Num.Bit0 m) =
+ (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
- take_bit_numeral_bit0 take_bit_numeral_bit1)
+ take_bit_Suc_bit0 take_bit_Suc_bit1 take_bit_numeral_bit0 take_bit_numeral_bit1)
+
+lemma take_bit_num_code [code]:
+ \<comment> \<open>Ocaml-style pattern matching is more robust wrt. different representations of \<^typ>\<open>nat\<close>\<close>
+ \<open>take_bit_num n m = (case (n, m)
+ of (0, _) \<Rightarrow> None
+ | (Suc n, Num.One) \<Rightarrow> Some Num.One
+ | (Suc n, Num.Bit0 m) \<Rightarrow> (case take_bit_num n m of None \<Rightarrow> None | Some q \<Rightarrow> Some (Num.Bit0 q))
+ | (Suc n, Num.Bit1 m) \<Rightarrow> Some (case take_bit_num n m of None \<Rightarrow> Num.One | Some q \<Rightarrow> Num.Bit1 q))\<close>
+ by (cases n; cases m) (simp_all add: take_bit_num_simps)
context semiring_bit_operations
begin
@@ -3176,7 +3181,8 @@
finally show ?thesis .
qed
-declare take_bit_num_simps [simp] take_bit_num_numeral_simps [simp] take_bit_numeral_numeral [simp]
+declare take_bit_num_simps [simp]
+ take_bit_numeral_numeral [simp]
take_bit_numeral_minus_numeral_int [simp]
--- a/src/HOL/Codegenerator_Test/Generate_Target_Nat.thy Fri Oct 29 00:01:14 2021 +0200
+++ b/src/HOL/Codegenerator_Test/Generate_Target_Nat.thy Thu Oct 28 06:39:36 2021 +0000
@@ -16,14 +16,6 @@
by a corresponding \<open>export_code\<close> command.
\<close>
-lemma take_bit_num_code [code]: \<comment> \<open>TODO: move\<close>
- \<open>take_bit_num n m = (case (n, m)
- of (0, _) \<Rightarrow> None
- | (Suc n, Num.One) \<Rightarrow> Some Num.One
- | (Suc n, Num.Bit0 m) \<Rightarrow> (case take_bit_num n m of None \<Rightarrow> None | Some q \<Rightarrow> Some (Num.Bit0 q))
- | (Suc n, Num.Bit1 m) \<Rightarrow> Some (case take_bit_num n m of None \<Rightarrow> Num.One | Some q \<Rightarrow> Num.Bit1 q))\<close>
- by (cases n; cases m) simp_all
-
export_code _ checking SML OCaml? Haskell? Scala
end