[isabelle] using global theorems in locale context


I have the following theorem

lemma small_fusion: "h : Disjunctive ==> mono f ==> mono g ==> h o f = g o h ==> h (lfp f) = lfp g"

which is proved as a global theorem.

However I would like to use it in a context of a complete lattice

context complete_lattice
   lemma ...
      apply (cut_tac ... in small_fusion)

The main reason I have small_fusion as a global theorem is because I use
lfp_ordinal_induct to prove it. If I want to prove small_fusion in the context
of a complete lattice, then I would have to build everything about lfp
in the local context.

Best regards,

Viorel Preoteasa

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