Re: [isabelle] using global theorems in locale context



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.