Re: [isabelle] Simple question about theory parameter



Great, thanks! I used relations just to simplify the example. In practice I will make additional assumptions about S.

Stephan


On 07/26/2012 08:27 AM, Tobias Nipkow wrote:
Am 25/07/2012 17:00, schrieb Stephan van Staden:
Thanks. Since Isabelle does not support dependent types, am I then forced to
define the relations on a set in the following (roundabout) way? Stating and
proving closure properties seem rather tedious, and it would be great if there
is a better way to do things.
This is the canocial way in simply typed systems.

definition comp :: "('a × 'b) set ⇒ ('b × 'c) set ⇒ ('a × 'c) set" (infixr ";;"
25) where
"r ;; r' ≡ {t. ∃s s' s''. (s,s') ∈ r ∧ (s',s'') ∈ r' ∧ t = (s,s'')}"
I strongly recommend to reuse existing concepts. It can save you an awful lot of
proofs. In this case ";;" already exists as "O". Don't let the fact that it is
introduced as an inductive set confuse you.

locale relations_on_a_set =
fixes S :: "'a set"
begin
definition Relations_on_S :: "('a × 'a) set set" where
"Relations_on_S ≡ {r. ∀(s, s') ∈ r. s ∈ S ∧ s' ∈ S}"
lemma comp_closed: "r ∈ Relations_on_S ⟹ r' ∈ Relations_on_S ⟹ (r ;; r') ∈
Relations_on_S"
sorry
end
Unless you want to assume some properties of S you can also get rid of the
locale and make S an explicit parameter of Relations_on (which also exists
already, it is called Field).

Tobias

Stephan


On 07/23/2012 08:47 PM, Tobias Nipkow wrote:
Am 23/07/2012 15:12, schrieb Stephan van Staden:
Dear all,

Here is a simplified version of my problem, which should have a simple answer.

I wish to prove a bunch of theorems about an arbitrary set S of numbers that
contains a designated element, say 1. For example, S intersect S and S union S
will both contain 1, etc.

Thereafter, I wish to get theorems for free about particular sets that contain
1. For example, {1,2,3} intersect {1,2,3} contains 1, etc.

What is the recommended way to do this in Isabelle?
It sounds like locales could be the answer.

Tobias

Thanks,
Stephan






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