author haftmann Sat Jun 24 09:17:35 2017 +0200 (24 months ago) changeset 66190 a41435469559 parent 66189 23917e861eaa child 66191 d91108ba9474
more direct construction of integer_of_num;
code equations for integer_of_char may rely on pattern matching on Char
 src/HOL/Code_Numeral.thy file | annotate | diff | revisions src/HOL/Library/Code_Target_Nat.thy file | annotate | diff | revisions src/HOL/String.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Code_Numeral.thy	Sat Jun 24 09:17:33 2017 +0200
1.2 +++ b/src/HOL/Code_Numeral.thy	Sat Jun 24 09:17:35 2017 +0200
1.3 @@ -149,24 +149,19 @@
1.4    "int_of_integer (Num.sub k l) = Num.sub k l"
1.5    by transfer rule
1.6
1.7 -lift_definition integer_of_num :: "num \<Rightarrow> integer"
1.8 -  is "numeral :: num \<Rightarrow> int"
1.9 -  .
1.10 +definition integer_of_num :: "num \<Rightarrow> integer"
1.11 +  where [simp]: "integer_of_num = numeral"
1.12
1.13  lemma integer_of_num [code]:
1.14 -  "integer_of_num num.One = 1"
1.15 -  "integer_of_num (num.Bit0 n) = (let k = integer_of_num n in k + k)"
1.16 -  "integer_of_num (num.Bit1 n) = (let k = integer_of_num n in k + k + 1)"
1.17 -  by (transfer, simp only: numeral.simps Let_def)+
1.18 -
1.19 -lemma numeral_unfold_integer_of_num:
1.20 -  "numeral = integer_of_num"
1.21 -  by (simp add: integer_of_num_def map_fun_def fun_eq_iff)
1.22 +  "integer_of_num Num.One = 1"
1.23 +  "integer_of_num (Num.Bit0 n) = (let k = integer_of_num n in k + k)"
1.24 +  "integer_of_num (Num.Bit1 n) = (let k = integer_of_num n in k + k + 1)"
1.25 +  by (simp_all only: integer_of_num_def numeral.simps Let_def)
1.26
1.27  lemma integer_of_num_triv:
1.28    "integer_of_num Num.One = 1"
1.29    "integer_of_num (Num.Bit0 Num.One) = 2"
1.30 -  by (transfer, simp)+
1.31 +  by simp_all
1.32
1.33  instantiation integer :: "{linordered_idom, equal}"
1.34  begin
1.35 @@ -301,7 +296,7 @@
1.36  end
1.37
1.38  declare divmod_algorithm_code [where ?'a = integer,
1.39 -  unfolded numeral_unfold_integer_of_num, unfolded integer_of_num_triv,
1.40 +  folded integer_of_num_def, unfolded integer_of_num_triv,
1.41    code]
1.42
1.43  lemma integer_of_nat_0: "integer_of_nat 0 = 0"
```
```     2.1 --- a/src/HOL/Library/Code_Target_Nat.thy	Sat Jun 24 09:17:33 2017 +0200
2.2 +++ b/src/HOL/Library/Code_Target_Nat.thy	Sat Jun 24 09:17:35 2017 +0200
2.3 @@ -59,7 +59,7 @@
2.4
2.5  lemma [code abstract]:
2.6    "integer_of_nat (nat_of_num n) = integer_of_num n"
2.7 -  by transfer (simp add: nat_of_num_numeral)
2.8 +  by (simp add: nat_of_num_numeral integer_of_nat_numeral)
2.9
2.10  lemma [code abstract]:
2.11    "integer_of_nat 0 = 0"
```
```     3.1 --- a/src/HOL/String.thy	Sat Jun 24 09:17:33 2017 +0200
3.2 +++ b/src/HOL/String.thy	Sat Jun 24 09:17:35 2017 +0200
3.3 @@ -160,35 +160,10 @@
3.4    by (simp only: integer_of_char_def integer_of_nat_def comp_apply nat_of_char_Char map_fun_def
3.5      id_apply zmod_int modulo_integer.abs_eq [symmetric]) simp
3.6
3.7 -lemma less_256_integer_of_char_Char:
3.8 -  assumes "numeral k < (256 :: integer)"
3.9 -  shows "integer_of_char (Char k) = numeral k"
3.10 -proof -
3.11 -  have "numeral k mod 256 = (numeral k :: integer)"
3.12 -    by (rule semiring_numeral_div_class.mod_less) (insert assms, simp_all)
3.13 -  then show ?thesis using integer_of_char_Char [of k]
3.14 -    by (simp only:)
3.15 -qed
3.16 -
3.17 -setup \<open>
3.18 -let
3.19 -  val chars = map_range (Thm.cterm_of @{context} o HOLogic.mk_numeral o curry (op +) 1) 255;
3.20 -  val simpset =
3.21 -    put_simpset HOL_ss @{context}
3.22 -      addsimps @{thms numeral_less_iff less_num_simps};
3.23 -  fun mk_code_eqn ct =
3.24 -    Thm.instantiate' [] [SOME ct] @{thm less_256_integer_of_char_Char}
3.25 -    |> full_simplify simpset;
3.26 -  val code_eqns = map mk_code_eqn chars;
3.27 -in
3.28 -  Global_Theory.note_thmss ""
3.29 -    [((@{binding integer_of_char_simps}, []), [(code_eqns, [])])]
3.30 -  #> snd
3.31 -end
3.32 -\<close>
3.33 -
3.34 -declare integer_of_char_simps [code]
3.35 -
3.36 +lemma integer_of_char_Char_code [code]:
3.37 +  "integer_of_char (Char k) = integer_of_num k mod 256"
3.38 +  by simp
3.39 +
3.40  lemma nat_of_char_code [code]:
3.41    "nat_of_char = nat_of_integer \<circ> integer_of_char"
3.42    by (simp add: integer_of_char_def fun_eq_iff)
```