*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Simple question about theory parameter*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Thu, 26 Jul 2012 08:27:56 +0200*In-reply-to*: <50100A16.8070107@inf.ethz.ch>*References*: <500D4DA3.1080604@inf.ethz.ch> <500D9C4F.6090601@in.tum.de> <50100A16.8070107@inf.ethz.ch>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.6; rv:14.0) Gecko/20120713 Thunderbird/14.0

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 >

**Follow-Ups**:**Re: [isabelle] Simple question about theory parameter***From:*Stephan van Staden

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

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

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

- Previous by Date: Re: [isabelle] HOLCF's continuity with partially defined operators
- Next by Date: Re: [isabelle] HOLCF equality type class
- 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