Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Simple question about theory parameter

Email Gateway (Aug 19 2022 at 07:51):

From: Stephan van Staden <Stephan.vanStaden@inf.ethz.ch>
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?

Thanks,
Stephan

Email Gateway (Aug 19 2022 at 07:52):

From: Tobias Nipkow <nipkow@in.tum.de>
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

Email Gateway (Aug 19 2022 at 07:54):

From: Stephan van Staden <Stephan.vanStaden@inf.ethz.ch>
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

Email Gateway (Aug 19 2022 at 07:55):

From: Tobias Nipkow <nipkow@in.tum.de>
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

Email Gateway (Aug 19 2022 at 07:56):

From: Stephan van Staden <Stephan.vanStaden@inf.ethz.ch>
Great, thanks! I used relations just to simplify the example. In
practice I will make additional assumptions about S.

Stephan

Last updated: Apr 19 2024 at 04:17 UTC