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



Steve,

Can a formula describing the property a function should hold across
*several* theories? For example, I might have 2 theories T1.thy and T2.thy,
each with its own set of axioms. Can I prove something like there exists a
function F, variables x and y, such that F x y returns r1 in T1 and r2 in T2
and r1 != r2? T1 and T2 are each internally consistent, but together may be
inconsistent.

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.

Alex





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