[isabelledev] scala2.12.2
Florian Haftmann
florian.haftmann at informatik.tumuenchen.de
Thu Jun 22 17:43:07 CEST 2017
> 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 deconstructivation
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 nontext attachment was scrubbed...
Name: signature.asc
Type: application/pgpsignature
Size: 819 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelledev/attachments/20170622/dcd69c93/attachment.sig>
More information about the isabelledev
mailing list