Re: [isabelle] simp only:



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

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 =
   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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.