*To*: isabelle-users at cl.cam.ac.uk*Subject*: [isabelle] mutual and recursive datatype doubts*From*: "Lucas Cavalcante" <thesupervisar at gmail.com>*Date*: Thu, 11 Oct 2007 22:34:40 -0300

I thank you in advance for any clarification concerning my following doubts! * * * 1. Suppose I want to define a new datatype in terms of other fresh datatypes, and then define a function over this new datatype, as for instance in: datatype mytype = typ0 | typ1 and typ0 = Zero and typ1 = One consts And :: "[mytype, mytype] => mytype" primrec "And Zero One = Zero" "And Zero Zero = Zero" "And One Zero = Zero" "And One One = One" Why does Isabelle complain that the constructors Zero and One do not have type "mytype", as I explicitly declared typ0 and typ1 as particular cases of mytype? I also tried to define, more simply: consts AND :: "[mytype, mytype] => mytype" primrec "AND Zero x = Zero" "AND x y = y" bu that went even worse for Isabelle... I found the error messages somewhat unexpected, as a completely similar definition works fine in ML. Of course, this is just a simple example of the problem I'm having. What I am really interested in is in defining functions involving mutually recursive datatypes, but first I have to understand what happens in simpler cases such as the above one! * * * 2. Can I not use the same constructor name for different datatypes? In the following example the second step of primrec is not correct because Two is not from 'a n1 datatype anymore, but 'a n2. datatype 'a n1 = One 'a | Two 'a | LotOf 'a datatype 'a n2 = Two 'a | OddPrime 'a consts ct :: "'a n1 => 'a n1" primrec "ct (One x) = One x" "ct (Two x::'a n1) = (One x::'a n1)" * * * 3. When using the same syntax sugar for different constructors of different datatypes, Isabelle finds it ambiguous to correctly parse the terms. Can I not use the same connective symbol for these constructions? Details follow in the example below: datatype 'a t1 = At1 'a | Not1 "'a t1" ("not_" [50]) | Imp1 "'a t1" "'a t1" ("_imp_" [45]) datatype 'a t2 = "'a t3" | Not "'a t3" ("not_" [50]) and 'a t3 = At 'a | Imp "'a t2" "'a t2" ("_imp_" [45]) consts valid_t1 :: "'a t1 => prop" ("(_)" 5) valid_t2 :: "'a t2 => prop" ("(_)" 5) valid_t3 :: "'a t3 => prop" ("(_)" 5) axioms impIa: "(P ==> Q) ==> P imp Q" * * * Lucas

**Follow-Ups**:**Re: [isabelle] mutual and recursive datatype doubts***From:*Tobias Nipkow

**Re: [isabelle] mutual and recursive datatype doubts***From:*Brian Huffman

**Re: [isabelle] mutual and recursive datatype doubts***From:*Brian Huffman

- Previous by Date: [isabelle] IJCAR Call for Papers, and Workshop and Tutorial Proposals
- Next by Date: Re: [isabelle] mutual and recursive datatype doubts
- Previous by Thread: [isabelle] IJCAR Call for Papers, and Workshop and Tutorial Proposals
- Next by Thread: Re: [isabelle] mutual and recursive datatype doubts
- Cl-isabelle-users October 2007 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