Re: [isabelle] inductive_set



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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.