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



Dear Gottfried,

--"HOL equal is defined."
axiomatization where
   Ax_x: "!q.!p. ( !x. (inS x q) <-> (inS x p) ) <-> (p = q)"
>
Okay. I don't really compute equality, I define it as shown above by
axiom Ax_x. I stuck that axiom into the experimental fFOLdt theory and
it didn't get rid of the error.
The error remains because
1. you did not declare the axiom Ax_x as a code equation, and
2. it is not executable as the !x-quantifier ranges over sT for which you have not provided an implementation.

The code generator will not work unless you provide a concrete representation for the elements of sT.

Even after only having made the statement "typedecl sT", HOL will prove
that "=" for type "sT" is reflexive, symmetric, and transitive.
No, it is not HOL that proves these three properties, = on any type is by axiom in HOL.thy reflexive, transitive and symmetric. As you use axiomatization, it is your job to make sure that your specification is consistent with HOL's axioms.

Regards,
Andreas





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