CODEWITHSUNDEEP
isabelle
John Wickerson
John Wickerson

Reputation: 1232

Apply simplifier to arbitrary term

I have a term in mind, say "foo 1 2 a b", and I'd like to know if Isabelle can simplify it for me. I'd like to write something like

simplify "foo 1 2 a b"

and have the simplified term printed in the output buffer. Is this possible?

My current 'workaround' is:

lemma "foo 1 2 a b = blah"
apply simp

which works fine but looks a bit hacky.

What doesn't work (in my case) is:

value "foo 1 2 a b"

because a and b are unbound variables, and because my foo involves infinite sets and other fancy stuff, which the code generator chokes on.

Upvotes: 2

Views: 118

Answers (2)

chris
chris

Reputation: 5038

When using the value command, the evaluation of the argument is conducted by registered evaluators (see the Reference Manual of Isabelle2013-2).

It used to be possible to explicitly choose an evaluator in previous versions of Isabelle (e.g., Isabelle2013-2) by giving an extra argument to the value command. E.g.,

value [simp] "foo 1 2 a b"

It seems that in Isabelle2014 this parameter was dropped and according to the Reference Manual of Isabelle2014, the strategy is now fixed to first use ML code generation and in case this fails, normalization by evaluation.

From the NEWS file in the development version (e82c72f3b227) of Isabelle it seems as if this parameter will be enabled again in the upcoming Isabelle release.

UPDATE: As Andreas pointed out, value [simp] does not use the same set of simplification rules as apply simp. So even if available, the solution I described above will most likely not yield the result you want.

Upvotes: 1

Andreas Lochbihler
Andreas Lochbihler

Reputation: 5108

There is no built-in feature AFAIK, but there are several ways to achieve this. You have already discovered one of them, namely state the term as a lemma and then invoke the simplifier. The drawback is that this cannot be used in all contexts, for example, not inside an apply proof script.

Alternatively, you can invoke the simplifier via the attribute [simplified]. This works in all contexts via the thm command and produces the output in the output buffer. First, the term must be injected into a theorem, then you can apply simplify to the theorem and display the result with thm. Here is the preparatory stuff that can go into your theory of miscellaneous stuff.

definition simp :: "'a ⇒ bool" where "simp _ = True"
notation (output) simp ("_")
lemma simp: "simp x" by(simp add: simp_def)

Then, you can write

thm simp[of "foo 1 2 a b", simplified]

and see the simplified term in the output window.

The evaluation mechanism is probably not what you want, because evaluation uses a different set of rewrite rules (namely the code equations) than the simplifier normally uses (the simpset). Therefore, this is likely to evaluate to a different term than by applying the simplifier. To see the difference, apply code_simp instead of simp in your approach with lemma "foo 1 2 a b = blah". The proof method code_simp uses the code equations just like value [simp] used to.

Upvotes: 3

Related Questions