Re: [isabelle] Simple question about theory parameter

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

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