[isabelle] inductive_set

Hi all,

I have a question concerning `inductive_set'. After defining an inductive set (the following set is just to demonstrate my point, hence its definition is not too important):

 inductive_set S :: "('a * 'a)set" where [intro]: "(x,x) : S"

I get the set

 S :: "('a * 'a)set"

and a predicate version

 Sp :: "'a => 'a => bool"

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] .

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. I'm sure there is some automatic way (currently I always have to use the induction scheme of the predicate to proof membership in the set and the other way round; but such proofs do not run through automatically, I have to explicitly provide the intro-rules) to do so?



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