Re: [isabelle] Trying to use "datatype" to restrict types of formulas used, getting error
If you want to prove that your notion of equality of sT is really
reflexive, transitive and symmetric, then you might do the following:
As you use axiomatization, it is your job to make sure that your
specification is consistent with HOL's axioms.
And that is a major concern of mine, and my fFOLdt and fFOLf idea was an
attempt to deal with unknowns that might cause my logic to be inconsistent.
definition eq :: "sT => sT => bool" where
"eq p q = (!x. inS x q <--> inS x p)"
lemma "eq x x" <proof>
lemma "eq x y = eq y x" <proof>
lemma "eq x y ==> eq y z ==> eq x z" <proof>
By using your own predicate eq instead of =, you avoid that the
automated proof methods use any of HOL's predefined properties.
This archive was generated by a fusion of
Pipermail (Mailman edition) and