Re: [isabelle] using global theorems in locale context




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


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:
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.
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!

- Brian








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