Re: [isabelle] using global theorems in locale context
Than you for your answer.
I understand the reasons. I was hopping that there is a mechanism
such that you can use a global theorem in a local context. I think
that I had this problem before, and I did not find a solution.
I have two subclasses A and B of a complete lattice, and the fusion
theorem would allow me to prove that B is a subclass of A. I have stated
this property in this way:
lemma "class.B (bot::'a::A) ..."
which is satisfactory.
On 4/7/12 5:40 PM, Brian Huffman wrote:
On Sat, Apr 7, 2012 at 3:48 PM, Viorel Preoteasa
<viorel.preoteasa at abo.fi> wrote:
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
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
of a complete lattice, then I would have to build everything about lfp
in the local context.
The reason that lfp_ordinal_induct is not proved in the locale context
is because it refers to the constant "mono".
The constant "mono :: ('a::order => 'b::order) => bool" is not defined
within the "order" locale context because its type mentions not one
order, but two different orders.
If you want to have lfp_ordinal_induct inside the complete_lattice
locale context, the only way I can think of is to define a more
restricted "mono' :: ('a => 'a) => bool" in the locale context, and
then reprove the lfp lemmas in terms of that. (There are only 5 or 6
easy lemmas necessary to prove lfp_ordinal_induct; you could just copy
the proof scripts from Inductive.thy.)
The inability of the class-based locales to handle constants like
"mono" is very unfortunate. Perhaps some of the other developers have
more to add about this; I hope that the situation can be improved in
This archive was generated by a fusion of
Pipermail (Mailman edition) and