Re: [isabelle] simp only:
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.
On 15/07/16 09:00, Gergely Buday wrote:
Andreas Lochbihler wrote:
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 =
|> Simplifier.set_subgoaler asm_simp_tac
|> Simplifier.set_mksimps (mksimps mksimps_pairs)
|> Simplifier.set_mkeqTrue mk_eq_True
|> Simplifier.set_mkcong mk_meta_cong
is this the basic setup for the simplifier in the HOL object logic?
This archive was generated by a fusion of
Pipermail (Mailman edition) and