Re: [isabelle] Proving formulae from separate sets of axioms



This is not possible. In some cases it is possible to localize axioms by just making them assumptions of some lemmas. The locale mechanism (see locale tutorial) gives some tool support for doing this.

If I localise axioms, then would I be able to check whether r1 != r2?
Checking r1 != r2 seems to need to look at *both* sets of axioms.

I meant that you could prove something like

  "(Ax1 ==> f x = r1) ==> (Ax2 ==> f x = r2) ==> r1 = r2"

Also, can I check whether F is instantiated to the same thing on each
side?

Not sure what you mean here with instantiated. If you have different descriptions of a function f, say "Ax1 f" and "Ax2 f", then the question can probably be expressed using the formula

  "Ax1 f ==> Ax2 f' ==> f = f'"

Maybe you want to prove a statement like this.

Alex





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