Re: [isabelle] A mystery of resolution.



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.