# Re: [isabelle] Simple question about theory parameter

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.
```

```
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'')}"

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

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.

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.