*To*: Steve W <s.wong.731 at gmail.com>*Subject*: Re: [isabelle] Pairs/tuples*From*: Tjark Weber <webertj at in.tum.de>*Date*: Sun, 10 Apr 2011 20:10:19 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <BANLkTi=cAOa9DQW2Tiow1-yz=J1cTTs_TQ@mail.gmail.com>*References*: <0022158df35b795080049fc94265@google.com> <4D957D2E.2010304@in.tum.de> <BANLkTimbqkLHUGOKHVCU4+5-CsW2rDb38g@mail.gmail.com> <1302200046.2358.111.camel@weber> <BANLkTi=cAOa9DQW2Tiow1-yz=J1cTTs_TQ@mail.gmail.com>

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

**References**:**Re: [isabelle] Pairs/tuples***From:*Lars Noschinski

**Re: [isabelle] Pairs/tuples***From:*Steve W

**Re: [isabelle] Pairs/tuples***From:*Tjark Weber

**Re: [isabelle] Pairs/tuples***From:*Steve W

- Previous by Date: Re: [isabelle] Pairs/tuples
- Next by Date: [isabelle] Workshop on Automated Theory Engineering (2nd CfP)
- Previous by Thread: Re: [isabelle] Pairs/tuples
- Next by Thread: [isabelle] rule Unifies With Chained Facts?
- Cl-isabelle-users April 2011 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list