# HG changeset patch
# User haftmann
# Date 1498288655 -7200
# Node ID a41435469559bf904683d909c1c2bd49df51c462
# Parent  23917e861eaa09d026654be5b8ce7a52cef3a18f
more direct construction of integer_of_num;
code equations for integer_of_char may rely on pattern matching on Char

diff -r 23917e861eaa -r a41435469559 src/HOL/Code_Numeral.thy
--- a/src/HOL/Code_Numeral.thy	Sat Jun 24 09:17:33 2017 +0200
+++ b/src/HOL/Code_Numeral.thy	Sat Jun 24 09:17:35 2017 +0200
@@ -149,24 +149,19 @@
   "int_of_integer (Num.sub k l) = Num.sub k l"
   by transfer rule
 
-lift_definition integer_of_num :: "num \<Rightarrow> integer"
-  is "numeral :: num \<Rightarrow> int"
-  .
+definition integer_of_num :: "num \<Rightarrow> integer"
+  where [simp]: "integer_of_num = numeral"
 
 lemma integer_of_num [code]:
-  "integer_of_num num.One = 1"
-  "integer_of_num (num.Bit0 n) = (let k = integer_of_num n in k + k)"
-  "integer_of_num (num.Bit1 n) = (let k = integer_of_num n in k + k + 1)"
-  by (transfer, simp only: numeral.simps Let_def)+
-
-lemma numeral_unfold_integer_of_num:
-  "numeral = integer_of_num"
-  by (simp add: integer_of_num_def map_fun_def fun_eq_iff)
+  "integer_of_num Num.One = 1"
+  "integer_of_num (Num.Bit0 n) = (let k = integer_of_num n in k + k)"
+  "integer_of_num (Num.Bit1 n) = (let k = integer_of_num n in k + k + 1)"
+  by (simp_all only: integer_of_num_def numeral.simps Let_def)
 
 lemma integer_of_num_triv:
   "integer_of_num Num.One = 1"
   "integer_of_num (Num.Bit0 Num.One) = 2"
-  by (transfer, simp)+
+  by simp_all
 
 instantiation integer :: "{linordered_idom, equal}"
 begin
@@ -301,7 +296,7 @@
 end
 
 declare divmod_algorithm_code [where ?'a = integer,
-  unfolded numeral_unfold_integer_of_num, unfolded integer_of_num_triv, 
+  folded integer_of_num_def, unfolded integer_of_num_triv, 
   code]
 
 lemma integer_of_nat_0: "integer_of_nat 0 = 0"
diff -r 23917e861eaa -r a41435469559 src/HOL/Library/Code_Target_Nat.thy
--- a/src/HOL/Library/Code_Target_Nat.thy	Sat Jun 24 09:17:33 2017 +0200
+++ b/src/HOL/Library/Code_Target_Nat.thy	Sat Jun 24 09:17:35 2017 +0200
@@ -59,7 +59,7 @@
 
 lemma [code abstract]:
   "integer_of_nat (nat_of_num n) = integer_of_num n"
-  by transfer (simp add: nat_of_num_numeral)
+  by (simp add: nat_of_num_numeral integer_of_nat_numeral)
 
 lemma [code abstract]:
   "integer_of_nat 0 = 0"
diff -r 23917e861eaa -r a41435469559 src/HOL/String.thy
--- a/src/HOL/String.thy	Sat Jun 24 09:17:33 2017 +0200
+++ b/src/HOL/String.thy	Sat Jun 24 09:17:35 2017 +0200
@@ -160,35 +160,10 @@
   by (simp only: integer_of_char_def integer_of_nat_def comp_apply nat_of_char_Char map_fun_def
     id_apply zmod_int modulo_integer.abs_eq [symmetric]) simp
 
-lemma less_256_integer_of_char_Char:
-  assumes "numeral k < (256 :: integer)"
-  shows "integer_of_char (Char k) = numeral k"
-proof -
-  have "numeral k mod 256 = (numeral k :: integer)"
-    by (rule semiring_numeral_div_class.mod_less) (insert assms, simp_all)
-  then show ?thesis using integer_of_char_Char [of k]
-    by (simp only:)
-qed
-
-setup \<open>
-let
-  val chars = map_range (Thm.cterm_of @{context} o HOLogic.mk_numeral o curry (op +) 1) 255;
-  val simpset =
-    put_simpset HOL_ss @{context}
-      addsimps @{thms numeral_less_iff less_num_simps};
-  fun mk_code_eqn ct =
-    Thm.instantiate' [] [SOME ct] @{thm less_256_integer_of_char_Char}
-    |> full_simplify simpset;
-  val code_eqns = map mk_code_eqn chars;
-in
-  Global_Theory.note_thmss ""
-    [((@{binding integer_of_char_simps}, []), [(code_eqns, [])])]
-  #> snd
-end
-\<close>
-
-declare integer_of_char_simps [code]
-
+lemma integer_of_char_Char_code [code]:
+  "integer_of_char (Char k) = integer_of_num k mod 256"
+  by simp
+  
 lemma nat_of_char_code [code]:
   "nat_of_char = nat_of_integer \<circ> integer_of_char"
   by (simp add: integer_of_char_def fun_eq_iff)