[isabelle] Trying to use "datatype" to restrict types of formulas used, getting error



Hi,

I'm trying to set up this formula,

!q. !P. ?u. (!x. x \<in> u <-> (x \<in> q & P x)),

so that P is only a FOL formula with a free variable x. I'm getting an error when I get to the part that uses quantification.

Currently P is of type (sT => bool), but I want to restrict it according to the following recursive definition:

Let x and y be variables, and let f and g be formulas, then
x \<in> y is a formula,
x = y is a formula,
~(f) is a formula,
(f & g) is a formula,
(f | g) is a formula,
(f --> g) is a formula,
(f <-> g) is formula,
(!x. f) is a formula,
(?x. f) is a formula, and
nothing else is a formula.

Really, all I want to do is restrict the syntax that can be used, but P has to have a type, P has to be based on recursion, and I have to use pattern matching, so I guess I have to use "datatype".

Here is what I have, where the last line causes an error, with the error shown below.

-------------------
typedecl sT

consts inS :: "sT => sT => bool" (infixl "inS" 55)

datatype sFOLdt =
In sT sT
|Eq sT sT
|Not bool
|And bool bool
|Or bool bool
|Imp bool bool
|Iff bool bool
|Forall sT bool

function sFOLf :: "sFOLdt => bool" where
"sFOLf (In u1 u2) = (u1 inS u2)" |
"sFOLf (Eq u1 u2) = (u1 = u2)" |
"sFOLf (Not f) = (~(f))" |
"sFOLf (And f1 f2) = (f1 & f2)" |
"sFOLf (Or f1 f2) = (f1 | f2)" |
"sFOLf (Imp f1 f2) = (f1 --> f2)" |
"sFOLf (Iff f1 f2) = (f1 <-> f2)" |
"sFOLf (Forall u f) = (!u. f)"

OUTPUT WINDOW ERROR:
Additional type variable(s) in specification of "sFOLf_graph": 'a
Specification depends on extra type variables: "'a"
The error(s) above occurred in "sTs.sFOLf_sumC_def"
The error(s) above occurred in definition "sFOLf_sumC_def":
"(sFOLf_sumC ≡ (%(x::sFOLdt). (THE_default undefined (%(y::bool). (sFOLf_graph TYPE('a) x y)))))"
-------------------

I've attached a 33KB screen capture which shows the same thing. I switched the screen capture from JPG to PNG and it went from 244KB to 33KB, using http://lightscreen.sourceforge.net/

Thanks,
GB








Attachment: function error.1.png
Description: PNG image



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