Re: [isabelle] Pairs/tuples



On Sun, 2011-04-10 at 19:21 +0100, Steve W wrote:
> I see. But why is 'a of sort "one"?

Because you used the constant 1 in ax.  In Isabelle/HOL, the (most
general) type of 1 is 'a::one (rather than, e.g., nat or int).

> Is there a way to declare "lst = (1,2,3)" without fixing the sort?

Well, if 1 was of type 'a (rather than 'a::one), the type of lst in your
axiom would be 'a * nat * nat (rather than 'a::one * nat * nat).  For
instance, consider

  consts myconst :: 'a
  axiomatization lst :: "'a * nat * nat"
  axioms ax : "lst = (myconst,2,3)"

  lemma "snd (snd lst) = 3"
  by (simp add: ax)

However, none of this is very idiomatic.  It might be helpful to know
more about what you're actually trying to achieve.

Kind regards,
Tjark







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