Re: [isabelle] Pairs/tuples


On Thu, 2011-04-07 at 18:41 +0100, Steve W wrote:
> axiomatization
> lst :: "'a*nat*nat"
> axioms
> ax : "lst = (1,2,3)"
> lemma "snd (snd lst) = 3"
> apply (simp add: ax)
> doesn't find a proof. How come changing the type of an element could make
> such a difference?

In the axiom ax, 'a provides a constant 1, i.e., 'a is of sort "one".
Hence the inferred (most general) type of lst in ax is 'a::one * nat *
nat.  Switch on Isabelle > Settings > Display > Show Sorts and have
Isabelle print the axiom ("thm ax") to see this.

In the lemma, however, the inferred type of lst is its declared type
'a * nat * nat, which is more general than 'a::one * nat * nat.
Therefore, the axiom ax does not apply.

By the way, you should really use definition instead of axiomatization/
axioms in your formalizations.

Kind regards,

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