Re: [isabelle] Trying to use "datatype" to restrict types of formulas used, getting error
--"HOL equal is defined."
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.
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.
Even after only having made the statement "typedecl sT", HOL will prove
that "=" for type "sT" is reflexive, symmetric, and transitive.
This archive was generated by a fusion of
Pipermail (Mailman edition) and