Email Gateway (Aug 22 2022 at 13:47): Email Gateway (Aug 22 2022 at 13:47):From: Gergely Buday <buday.gergely@uni-eszterhazy.hu>
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: ?
Email Gateway (Aug 22 2022 at 13:48):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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
Email Gateway (Aug 22 2022 at 13:48):From: Gergely Buday <buday.gergely@uni-eszterhazy.hu>
Andreas Lochbihler wrote:
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?
Email Gateway (Aug 22 2022 at 13:48):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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
Last updated: Apr 26 2024 at 12:28 UTC