Re: [isabelle] A mystery of resolution.



Thanks for the explanations, that explains what's going on entirely.

I guess that I have fallen into the habit of assuming too much from the 
unifier.

Cheers,
     Thomas.

On 03/02/18 01:46, Makarius wrote:
> On 02/02/18 13:03, Lawrence Paulson wrote:
>>> On 2 Feb 2018, at 04:42, <Thomas.Sewell at data61.csiro.au> <Thomas.Sewell at data61.csiro.au> wrote:
>>>
>>>    apply (tactic {* match_tac @{context} [(@{thm impI})] 1 *})
>>>
>>> This is quite strange.
>>>
>> I'm afraid that I have to call this behaviour correct, if weird and annoying.
> Here is also the text from the "implementation" manual that has emerged
> from such explanations over the years:
>
>    â @{ML match_tac}, @{ML ematch_tac}, @{ML dmatch_tac}, and @{ML
> bimatch_tac}
>    are similar to @{ML resolve_tac}, @{ML eresolve_tac}, @{ML dresolve_tac},
>    and @{ML biresolve_tac}, respectively, but do not instantiate schematic
>    variables in the goal state.ââStrictly speaking, matching means to
> treat the
>    unknowns in the goal state as constants, but these tactics merely discard
>    unifiers that would update the goal state. In rare situations (where the
>    conclusion and goal state have flexible terms at the same position), the
>    tactic will fail even though an acceptable unifier exists.â These tactics
>    were written for a specific application within the classical reasoner.
>
>    Flexible subgoals are not updated at will, but are left alone.
>
>
> For the purposes of matching in Isar 'is' patterns etc. there is a
> different front-end called Unify.matchers:
> http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2017/src/Pure/more_unify.ML
>
> This has empirically evolved to something that works most of the time
> for the particular applications of structured proofs (Isar) and proof
> methods (Eisbach).
>
>
> 	Makarius


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