isarmathlib-devel
[Top][All Lists]
Advanced

[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



reply via email to

[Prev in Thread] Current Thread [Next in Thread]