[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[Isarmathlib-devel] Sublocale loops
From: |
Victor Porton |
Subject: |
[Isarmathlib-devel] Sublocale loops |
Date: |
Sun, 02 Jan 2011 20:30:11 +0300 |
I decided to attempt to implement order locales for IsarMathLib (and afterward
I hope to implement lattices and complete lattices).
For testing I made the following toy theory:
<<<
theory MyOrder
imports Main_ZF
begin
locale poset =
fixes base::i
fixes order::i
assumes "order<=base\<times>base" and "refl(base,order)" and "antisym(order)"
and "trans(order)"
locale strict_poset =
fixes base::i
fixes strict_order::i
assumes "strict_order<=base\<times>base" and "irrefl(base,strict_order)" and
"antisym(strict_order)" and "trans(strict_order)"
sublocale strict_poset < poset "base" "order Un id(base)"
proof
show "order Un id(base) \<subseteq> base \<times> base" sorry
show "refl(base, order Un id(base))" sorry
show "antisym(order Un id(base))" sorry
show "trans(order Un id(base))" sorry
qed
sublocale poset < strict_poset "base" "order-id(base)"
proof
show "order - id(base) \<subseteq> base \<times> base" sorry
show "irrefl(base, order - id(base))" sorry
show "antisym(order - id(base))" sorry
show "trans(order - id(base))" sorry
qed
end
>>>
I wonder why it works without a proof that switching from a "poset" to a
"strict_poset" and back to "poset" produces the same order as was in the
beginning.
I also would formulate that this forth-back switching leaves the locale
unchanged, but don't see how to formulate this in terms of locales.
Maybe core of Isabelle needs a change that would allow to formulate such kinds
of theorems in terms of locales?
If it does not need a change please explain me how to manage this with Isabelle
2009-2.
--
Victor Porton - http://portonvictor.org
[Prev in Thread] |
Current Thread |
[Next in Thread] |
- [Isarmathlib-devel] Sublocale loops,
Victor Porton <=