[isabelle] match_tac, schematic and bound variables



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.