Re: [isabelle] match_tac, schematic and bound variables



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
*}





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