[isabelle-dev] scala-2.12.2

[Florian Haftmann]

> Alternatively, Florian might offer some insight why he set up the code
> equations for that particular constant in that way (see "String.thy",
> where a ML snippet generates 256 code equations). Note that large
> pattern matches on the JVM should be avoided, lest we violate the 64k
> method length limit in class files ("integer_of_char" currently requires
> 58044 bytes).

I took the opportunity to have a look at it and found out it can be done
differently, see attached patch.

The clue about "integer_of_char" is that it had to work regardless
whether HOL chars are represented authentic or by target language
characters (importing "~~/src/HOL/Library/Code_Char").

Nowadays this can be achieved without spelling out the chars explicitly.
 The last stone to turn around before had been the de-constructivation
of the char type (b3f2b8c906a6).

Cheers,
	Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
-------------- next part --------------
# HG changeset patch
# Parent  45d3d43abee7147fd43e63a6b4ba6340a5d4b74f
more direct construction of integer_of_num;
code equations for integer_of_char may rely on pattern matching on Char

diff -r 45d3d43abee7 src/HOL/Code_Numeral.thy
--- a/src/HOL/Code_Numeral.thy	Thu Jun 22 16:59:14 2017 +0200
+++ b/src/HOL/Code_Numeral.thy	Thu Jun 22 17:31:28 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 45d3d43abee7 src/HOL/String.thy
--- a/src/HOL/String.thy	Thu Jun 22 16:59:14 2017 +0200
+++ b/src/HOL/String.thy	Thu Jun 22 17:31:28 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)
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20170622/dcd69c93/attachment.sig>