Re: [isabelle] question concerning simplification basics



On Tue, 7 Jul 2009, Andrei Popescu wrote:

consts P::"'a => bool"

definition Q :: "'a => bool"
where "Q = P"

lemma try:
"P x  ==> Q x"
proof-
  assume "P x"
  thus "Q x" by (simp add: Q_def)
qed

This works, because the polymorphic definition Q_def is locally added to the Simplifier context (via "add") and the Simplifier will match it against any goal states, instantiating an arbitrary ?'a by a fixed 'a as expected.

lemma try2:
"P x  ==> Q x"
proof-
  assume "P x"
  thus "Q x" using Q_def by force (* THIS FAILS *)
qed

This fails because Q_def is merely inserted straight into the goal, before regular "force" operation. The unspecified ?'a on the left of the implication that is part of the goal will never be instantiated by the proof tool -- all automated proof tools work like that (simp, auto, fast).

Better be more specific about "unfolding Q_def" before finishing by force etc. Alternatively, you can include it via "simp add: Q_def" into the method context as for simp above.


	Makarius


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