# [isabelle] match_tac, schematic and bound variables

*To*: isabelle-users <isabelle-users at cl.cam.ac.uk>
*Subject*: [isabelle] match_tac, schematic and bound variables
*From*: Lars Noschinski <noschinl at in.tum.de>
*Date*: Mon, 12 Aug 2013 14:00:46 +0200
*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:10.0.12) Gecko/20130116 Icedove/10.0.12

Hi,
I stumbled upon some odd behaviour of match_tac. When match_tac
- must match a schematic variable in the rule against a schematic
variable in the goal and the schematic variable,
- the schematic in the goal has bound variables as parameters,
- one of these bound variables x occurs at least twice in the
parameters, and
- there is another bound variable between the occurences of x,

`then match_tac fails (i.e. empty proof sequence / failed to apply proof
``method).
`

`Has anyone got an explanation for this behaviour? I would have expected
``that the implementation of matching for this quasi-first-order case is
``complete.
`

`This behaviour occurs both in Isabelle 2012 and in a current development
``snapshot (0cd62cb233e0).
`
definition "TT ≡ λx. True"
lemma TT_I: "TT x" unfolding TT_def by simp
schematic_lemma "⋀x y. TT (?P x y x )"
apply (tactic {* match_tac @{thms TT_I} 1 *})
(* fails *)
oops
schematic_lemma "⋀x y. TT (?P x y )"
apply (tactic {* match_tac @{thms TT_I} 1 *})
done
schematic_lemma "⋀x y. TT (?P x x y )"
apply (tactic {* match_tac @{thms TT_I} 1 *})
done
schematic_lemma "⋀x y. TT (P x y x )"
apply (tactic {* match_tac @{thms TT_I} 1 *})
done
schematic_lemma "⋀x. TT (?P x y x )"
apply (tactic {* match_tac @{thms TT_I} 1 *})
done
-- Lars

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