Discussion:
[isabelle] simp only:
(too old to reply)
Gergely Buday
2016-07-14 12:05:39 UTC
Permalink
Hi,

The Isabelle/Isar Reference Manual says about simp only:

Implicit solvers remain, which means that trivial rules like reflexivity or

introduction of True are available to solve the simplified subgoals, but

also non-trivial tools like linear arithmetic in HOL. The latter may lead

to some surprise of the meaning of “only” in Isabelle/HOL compared

to English!

I guess print_simpset shows the simpset when using simp add:

Can I somehow print the simpset when using simp only: ?

- Gergely
Andreas Lochbihler
2016-07-14 17:14:02 UTC
Permalink
Hi Gergely,

There's no need to print it. "simp only:" clears all the simpset, so there are no rewrite
rules in there, but all the subgoalers and solvers remain as is. If you specify some
rewrite rules, then these will be the only ones in the simpset. If you want to find out
how the simplifier preprocesses theses rules, you can look at the trace with [[simp_trace]].

Hope this helps,
Andreas
Post by Gergely Buday
Hi,
Implicit solvers remain, which means that trivial rules like reflexivity or
introduction of True are available to solve the simplified subgoals, but
also non-trivial tools like linear arithmetic in HOL. The latter may lead
to some surprise of the meaning of “only” in Isabelle/HOL compared
to English!
Can I somehow print the simpset when using simp only: ?
- Gergely
Gergely Buday
2016-07-15 07:07:59 UTC
Permalink
Post by Andreas Lochbihler
There's no need to print it. "simp only:" clears all the simpset, so there are no
rewrite rules in there, but all the subgoalers and solvers remain as is. If you
specify some rewrite rules, then these will be the only ones in the simpset. If
you want to find out how the simplifier preprocesses theses rules, you can
look at the trace with [[simp_trace]].
Still, I am interested in the standard subgoaler and solver. I have found a section for them at

9.3.6 Configurable Simplifier strategies

in the Isabelle/Isar Reference Manual.

In the source, in HOL/Tools/simpdata.ML there is

val HOL_basic_ss =
empty_simpset @{context}
setSSolver safe_solver
setSolver unsafe_solver
|> Simplifier.set_subgoaler asm_simp_tac
|> Simplifier.set_mksimps (mksimps mksimps_pairs)
|> Simplifier.set_mkeqTrue mk_eq_True
|> Simplifier.set_mkcong mk_meta_cong
|> simpset_of;

is this the basic setup for the simplifier in the HOL object logic?

- Gergely
Andreas Lochbihler
2016-07-15 07:42:40 UTC
Permalink
Hi Gergely,

As the subgoalers and solvers are ML code (rather than theorems), one can only print their
names. You have to look into the source code to see what they are doing. HOL_basic_ss is
indeed the basic setup for the simplifier, but later some more solvers are added, e.g. for
linear arithmetic. HOL_basic_ss is the simpset that you want to start with in most cases
when you implement your own proof tactic that uses a carefully designed set of simp rules
which should not interact with other constants in the goal.

Best,
Andreas
Post by Gergely Buday
Post by Andreas Lochbihler
There's no need to print it. "simp only:" clears all the simpset, so there are no
rewrite rules in there, but all the subgoalers and solvers remain as is. If you
specify some rewrite rules, then these will be the only ones in the simpset. If
you want to find out how the simplifier preprocesses theses rules, you can
look at the trace with [[simp_trace]].
Still, I am interested in the standard subgoaler and solver. I have found a section for them at
9.3.6 Configurable Simplifier strategies
in the Isabelle/Isar Reference Manual.
In the source, in HOL/Tools/simpdata.ML there is
val HOL_basic_ss =
setSSolver safe_solver
setSolver unsafe_solver
|> Simplifier.set_subgoaler asm_simp_tac
|> Simplifier.set_mksimps (mksimps mksimps_pairs)
|> Simplifier.set_mkeqTrue mk_eq_True
|> Simplifier.set_mkcong mk_meta_cong
|> simpset_of;
is this the basic setup for the simplifier in the HOL object logic?
- Gergely
Loading...