Simplify pretty-printing of naturals

问题:

Let's say I wrote a function for reversing a list. I want to test it out using the value command, just to assure myself that I probably got it right. But the output looks horrible:

value "reverse [1,8,3]"
> "[1 + 1 + 1, 1 + 1 + (1 + 1) + (1 + 1 + (1 + 1)), 1]" :: "'a list"

If I tell Isabelle to treat those numeric characters as naturals, the output is even worse:

value "reverse [1::nat,8,3]"
> "[Suc (Suc (Suc 0)), Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))), Suc 0]" :: "nat list"

Sometimes I resort to using strings, but that's looks a bit funny with all those apostrophes everywhere:

value "reverse [''1'',''8'',''3'']"
> "[''3'', ''8'', ''1'']" :: "char list list"

Can I instruct Isabelle's pretty-printer to print Suc (Suc (Suc 0)) as 3, and so on? Perhaps by giving some magical incantation to the syntax or translations commands?

---

Here's my complete example, in case you'd like to paste it into Isabelle:

theory Scratch imports Main begin

fun reverse where 
  "reverse [] = []"
| "reverse (x#xs) = reverse xs @ [x]"

value "reverse [1,8,3]"
value "reverse [1::nat,8,3]"
value "reverse [''1'',''8'',''3'']"

end

回答1:

Short answer: My first thought is to use type int, since (unlike nat) its code generator setup uses a binary numeral representation by default.

Importing "~~/src/HOL/Library/Code_Target_Nat", as naT suggests, is also a good idea if you don't want to use the Suc representation for type nat.

Explanation: Numerals in Isabelle are encoded using constructors defined in Num.thy; e.g. 5 is an abbreviation for numeral (Bit1 (Bit0 One)). Here One, Bit0 and Bit1 are constructors of type num. numeral is overloaded, and works for any type with a 1 and an associative +. Here are the code equations for numeral:

lemma numeral_code [code]:
  "numeral One = 1"
  "numeral (Bit0 n) = (let m = numeral n in m + m)"
  "numeral (Bit1 n) = (let m = numeral n in m + m + 1)"

If we generate code for 5::'a::numeral, then 1 and + on type 'a are treated as uninterpreted constants, so they remain in the output: (1 + 1) + (1 + 1) + 1.

Generating code for 5::nat works the same, except we do have code for 1 and + on type nat, in terms of Suc. Thus (1 + 1) + (1 + 1) + 1 reduces further to Suc (Suc (Suc (Suc (Suc 0)))).

Type int works differently. The code generator setup in Int.thy uses three constructor functions for type int: Pos and Neg of type num => int, as well as 0. A code_abbrev declaration causes each occurrence of numeral at type num => int to be replaced by Pos during code generation. After the code is run, Pos is then turned back into numeral before Isabelle displays the result. Thus 5::int evaluates to just 5.

Special code setup theories: src/HOL/Library contains a few different theories for customizing code generation for numerals.

• "~~/src/HOL/Library/Code_Target_Nat" tells the code generator to use the target language's (e.g. SML or Haskell's) built-in numerals for type nat. For example, 5::nat is usually translated to SML as numeral (Bit1 (Bit0 One)); however, with this library loaded it gets translated as 5 in SML. Results of value are translated back into the Isabelle numeral representation afterward.

• "~~/src/HOL/Library/Code_Target_Int" is the same, but for type int instead of nat.

• "~~/src/HOL/Library/Code_Target_Numeral" simply loads both of the previous two libraries. It only affects types nat and int, not any other types in class numeral.

• "~~/src/HOL/Library/Code_Binary_Nat" configures nat in the same style as the default code setup for int: with constructors 0 and nat_of_num::num => nat and a code_abbrev declaration. With this library, value "5::nat" also returns 5.

回答2:

Note: I hope my answer here doesn't prevent Brian Huffman or Florian Haftmann from giving an answer. If it does, that would be a bad thing. Hopefully, I'm just doing some gofer work to set either of them up.

Short answer 1: The pertinent mailing list email is Re: [isabelle] value no longer pretty-prints numbers of type nat.

Short answer 2: A solution for nat is to import "~~/src/HOL/Library/Code_Target_Nat". Because I'm not clear on the details of how numeral and num are completely tied into HOL at the low level, the solution I'm giving you is not necessarily a good and final solution.

A big part of my answer here is partly to say, before Brian Huffman or Florian Haftmann get here, who are the authors of Num.thy, "I'm interested in this too, because it's related to numeral, which is a powerful part of HOL. The more info I have about the intricacies of using numeral, the better".

Basically, they made a design choice change for Isabelle2013-1, which is to have the default for nat and numeral be represented in a successor form. That's what the mailing list email is about.

If you use declare[[show_sorts=true]], you will see that your value "reverse [1,8,3]" is using type class numeral. I mention that because I've been putting a lot of effort into trying to learn about numeral, and even with concrete types, such as nat and int, the use of constants such as 44 and 5 involve numeral, at least for the input. And even with a concrete type like nat, numeral can be involved in simp rules that are being used.

Before saying more, one way to get nice nat output for value "reverse [1::nat,8,3]" is, again, to use the following import:

"~~/src/HOL/Library/Code_Target_Nat"

The reason I'm interested in your question is because that's just a plug-n-play solution I saw by Andreas Lochbihler in that email.

I can't get value "reverse [1,8,3]" to not use sums of 1 by importing this:

"~~/src/HOL/Library/Code_Target_Numeral"

So, I want to know about how to get numeral to be in that nice form we love to see.

Anyway, numeral is at the core of using number constants. Consider this:

lemma "(3::nat) = z"
using[[simp_trace, simp_trace_depth_limit=100, linarith_trace, rule_trace]]
using[[blast_trace, blast_stats]]
apply simp
oops

Part of the simp trace is this:

[1]SIMPLIFIER INVOKED ON THE FOLLOWING TERM:
3 = z 
[1]Procedure "Num.reorient_numeral" produced rewrite rule:
?a1 = ?b1 ≡ ?b1 = ?a1 
[1]Applying instance of rewrite rule
?a1 = ?b1 ≡ ?b1 = ?a1 
[1]Rewriting:
3 = z ≡ z = 3 

If you look at simp traces involving number constants, you'll see that Num rules show up a lot, which come from that most excellent of Num.thy.