Re: [isabelle] Pairs/tuples



On Thu, Apr 7, 2011 at 7:14 PM, Tjark Weber <webertj at in.tum.de> wrote:

> Steve,
>
> 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.
>

I see. But why is 'a of sort "one"? Is there a way to declare "lst =
(1,2,3)" without fixing the sort?

Thanks
Steve




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