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.

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.