Re: [isabelle] Pairs/tuples
On Thu, 2011-04-07 at 18:41 +0100, Steve W wrote:
> lst :: "'a*nat*nat"
> 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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and