[isabelle] mutual and recursive datatype doubts



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




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