Re: [isabelle] match_tac, schematic and bound variables



Am 12/08/2013 18:13, schrieb Makarius:
> On Mon, 12 Aug 2013, Lars Noschinski wrote:
> 
>> I stumbled upon some odd behaviour of match_tac.
> 
> Larry is the one to explain what really happens.
> 
> When I came across match_tac for the first time as a very young student in 1993,
> I was already wondering about it -- but it was always document in the manner of
> what is now in "implementation" manual (section 4.2.1):
> 
>   \item @{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.
> 
>   Flexible subgoals are not updated at will, but are left alone.
>   Strictly speaking, matching means to treat the unknowns in the goal
>   state as constants; these tactics merely discard unifiers that would
>   update the goal state.
> 
> This sounds like it is better not to lean out of the window too far.

It is the documentation that is leaning too far out of the window. The
difference between

schematic_lemma "⋀x y. TT (?P x y x )"
  apply (tactic {* match_tac @{thms TT_I} 1 *})
  (* fails *)
  oops

and

schematic_lemma "⋀x y. TT (P x y x )"
  apply (tactic {* match_tac @{thms TT_I} 1 *})
  done

shows that in some situations it is not doing what it claims: "matching means to
treat the unknowns in the goal state as constants".

Tobias




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