> 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
# 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)
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev