Email Gateway (Aug 18 2022 at 19:30): Email Gateway (Aug 18 2022 at 19:30):From: Viorel Preoteasa <viorel.preoteasa@abo.fi>
Hello,
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
begin
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
Email Gateway (Aug 18 2022 at 19:31):From: Brian Huffman <huffman@in.tum.de>
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
the future!
Email Gateway (Aug 18 2022 at 19:31):From: Viorel Preoteasa <viorel.preoteasa@abo.fi>
Hello Brian,
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.
Viorel
Last updated: Apr 25 2024 at 20:15 UTC