Re: [isabelle] inductive_set



Stefan Berghofer wrote:
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
The example lemmas are admittedly badly chosen.

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.
Sorry, I overlooked something obvious ( :) ), namely that I can apply attributes within proofs. If I have `(a,b) : S`, I can of course use `(a,b) : S`[to_pred] to get "Sp a b". My fault.

thnx a lot,

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







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