[isabelle-dev] Occur-Check Lemma and Unifikations-Algorithmus

[Makarius]

On Fri, 22 Jul 2011, Lars Noschinski wrote:

> In this case it also works for the simplifier. Actually, I had to go to the 
> old HOL manual, to find out, why one would usually use the splitter for this. 
> In our case, the if is in the assumption, so one would need
>
>    (simp split: split_if_asm)
>
> here instead. But I'm quite fuzzy on the semantics of the split 
> parameter -- why would split_if be applied to the conclusion and 
> split_if_asm to the hypotheses? Is there somewhere a high-level 
> description of the splitter?

These ancient explanations of simplifier components are still awaiting to 
be updated and moved to isar-ref.  I have recently done most of that for 
the classical reasoner, in conjunction with some "localization" and 
simplification of the implementation (except for wrappers and addss stuff, 
which is seen in Isar source as "fastsimp").

I will continue that eventually.


> BTW: Is the isar-ref documentation about the split method correct? It 
> does not seem (and need) to accept the "(asm)" option?

That is indeed a bit outdated -- more than 10 years.  See now 
http://isabelle.in.tum.de/repos/isabelle/rev/f7bbfdf4b4a7


 	Makarius