[isabelle-dev] [isabelle] match_tac, schematic and bound variables

[Lawrence Paulson]

I think that the only way to achieve the documented behaviour is to replace all schematic variables in the goal by Frees before attempting resolution. I'm not sure what effect this would have on performance.
Larry

On 13 Aug 2013, at 10:35, Lars Noschinski <noschinl at in.tum.de> wrote:

> On 12.08.2013 18:13, Makarius wrote:
>> 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.
> 
> Peter and I did some investigation and this seems to be the source of this behaviour: If two schematic variables (with only bound variables as arguments) are to be unified, Unifiers.unify will always provide a single unifier with the schematic variables reordered.
> 
> It might be interesting to note that also Unify.matchers is not able to match such term.
> 
> 
> 
> theory Scratch imports Main begin (* Isabelle 2013 *)
> 
> ML {*
>  val pat = @{cpat "⋀x y. ?P x y"}
>  val term = @{cpat "⋀x y. ?Q x y x"}
>  val pair = [(term_of pat, term_of term)]
> 
>  fun maxidx_of_cterm ct = case rep_cterm ct of
>    {maxidx, ...} => maxidx
>  val maxidx = Int.max (maxidx_of_cterm pat, maxidx_of_cterm term)
> *}
> 
> ML {*
>  fun pretty_subst ctxt ((name,_), (typ, term)) =
>    [Pretty.str name, Syntax.pretty_typ ctxt typ, Syntax.pretty_term ctxt term]
>    |> Pretty.list "" ""
>  val pretty_env =
>    Envir.term_env #> Vartab.dest #> map (pretty_subst @{context}) #> Pretty.big_list "Unifier"
>  val pretty_env_list = map pretty_env #> Pretty.big_list "Unifiers"
> *}
> 
> ML {*
>  Unify.unifiers (@{theory}, Envir.empty maxidx, pair)
>  |> Seq.list_of
>  |> map fst
>  |> pretty_env_list
>  |> Pretty.string_of
>  |> tracing
> *}
> 
> ML {*
>  Unify.matchers @{theory} pair |> Seq.list_of |> pretty_env_list |> Pretty.string_of |> tracing
> *}
> 
>