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



Gottfried,

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.
If you want to prove that your notion of equality of sT is really reflexive, transitive and symmetric, then you might do the following:

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.

Andreas





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