*To*: Christian Sternagel <christian.sternagel at uibk.ac.at>*Subject*: Re: [isabelle] inductive_set*From*: Stefan Berghofer <berghofe at in.tum.de>*Date*: Thu, 19 Feb 2009 10:59:20 +0100*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <499D11F7.6090908@uibk.ac.at>*Organization*: Technische Universität München*References*: <499D11F7.6090908@uibk.ac.at>*User-agent*: Thunderbird 2.0.0.19 (X11/20081227)

Christian Sternagel wrote: > and after proving lemmas using e.g., Sp, I can transform them to lemmas > for S using the attribute [to_set] as in, > > lemma refl: "Sp x x" by simp > > lemma "(x,x) : S" using refl[to_set] . Hi, note that inductive_set already proves both the set and the predicate version of the intro, cases, and induct rules for you, so there is no need to prove them manually. For example, if you define inductive_set S :: "('a * 'a)set" where refl: "(x,x) : S" you get the following theorems: S.refl: (x, x) : S Sp.refl: S x x S.induct: [| (x1, x2) : S; !!x. P x x |] ==> P x1 x2 Sp.induct: [| Sp x1 x2; !!x. P x x |] ==> P x1 x2 The [to_set] attribute and the inverse [to_pred] attribute are only needed for transforming more complex theorems that have been derived from the above primitive rules (as it is done e.g. in HOL/Transitive_Closure.thy). > So far so good. However, I was not able to find a method to directly > transform facts like `(a,b) : S` into `Sp a b` and vice versa. What exactly do you mean by "directly"? I could not think of a more "direct" way than the application of an attribute. It is a bit unclear to me why do you need both the set and the predicate version of your definition in the same theory. It might be easier to stick to a particular notation, e.g. the predicate notation, which is usually more lightweight. Greetings, Stefan -- Dr. Stefan Berghofer E-Mail: berghofe at in.tum.de Institut fuer Informatik Phone: +49 89 289 17328 Technische Universitaet Muenchen Fax: +49 89 289 17307 Boltzmannstr. 3 Room: 01.11.059 85748 Garching, GERMANY http://www.in.tum.de/~berghofe

**Follow-Ups**:**Re: [isabelle] inductive_set***From:*Christian Sternagel

**References**:**[isabelle] inductive_set***From:*Christian Sternagel

- Previous by Date: [isabelle] inductive_set
- Next by Date: Re: [isabelle] inductive_set
- Previous by Thread: [isabelle] inductive_set
- Next by Thread: Re: [isabelle] inductive_set
- Cl-isabelle-users February 2009 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