*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*: Thu, 26 Jul 2012 13:16:33 +0200*In-reply-to*: <5010E36C.6090601@in.tum.de>*References*: <500D4DA3.1080604@inf.ethz.ch> <500D9C4F.6090601@in.tum.de> <50100A16.8070107@inf.ethz.ch> <5010E36C.6090601@in.tum.de>*User-agent*: Mozilla/5.0 (X11; Linux i686; rv:14.0) Gecko/20120714 Thunderbird/14.0

Stephan On 07/26/2012 08:27 AM, Tobias Nipkow wrote:

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 endUnless 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). TobiasStephan 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

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

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

- Previous by Date: Re: [isabelle] Sledgehammer and Nitpick from the command line?
- Next by Date: Re: [isabelle] HOLCF's continuity with partially defined operators
- Previous by Thread: Re: [isabelle] Simple question about theory parameter
- Next by Thread: [isabelle] Unicode tokens in jedit
- 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