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/
Description: PNG image