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 <nosch...@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
> *}
>
>
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
