*To*: <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] Simple question about theory parameter*From*: Stephan van Staden <Stephan.vanStaden at inf.ethz.ch>*Date*: Wed, 25 Jul 2012 17:00:38 +0200*In-reply-to*: <500D9C4F.6090601@in.tum.de>*References*: <500D4DA3.1080604@inf.ethz.ch> <500D9C4F.6090601@in.tum.de>*User-agent*: Mozilla/5.0 (X11; Linux i686; rv:14.0) Gecko/20120714 Thunderbird/14.0

"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}"

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. TobiasThanks, Stephan

**Follow-Ups**:**Re: [isabelle] Simple question about theory parameter***From:*Tobias Nipkow

**References**:**[isabelle] Simple question about theory parameter***From:*Stephan van Staden

**Re: [isabelle] Simple question about theory parameter***From:*Tobias Nipkow

- Previous by Date: Re: [isabelle] HOLCF's continuity with partially defined operators
- Next by Date: [isabelle] skip_proofs in Isabelle2012
- Previous by Thread: Re: [isabelle] Simple question about theory parameter
- Next by Thread: Re: [isabelle] Simple question about theory parameter
- Cl-isabelle-users July 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list