Re: [isabelle] match_tac, schematic and bound variables



Sorry but I have totally forgotten about these. They are relics from a remote past. 
Larry

On 12 Aug 2013, at 17:13, Makarius <makarius at sketis.net> wrote:

> 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.
> 
> 
> 	Makarius
> 





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