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