Email Gateway (Aug 18 2022 at 13:01): Email Gateway (Aug 18 2022 at 13:01):From: Christian Sternagel <christian.sternagel@uibk.ac.at>
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?
cheers
christian
Email Gateway (Aug 18 2022 at 13:01):From: Stefan Berghofer <berghofe@in.tum.de>
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) : SintoSp a band 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
Email Gateway (Aug 18 2022 at 13:01):From: Christian Sternagel <christian.sternagel@uibk.ac.at>
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 x2The [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) : SintoSp a band 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
Email Gateway (Aug 18 2022 at 16:04):From: Christian Sternagel <christian.sternagel@uibk.ac.at>
Hi there,
apparently inductive_set does modify ALL occurrences of inductive
predicates stemming from other inductive_set commands inside intro rules
as if the attribute [to_set] was used. Is this wanted / necessary / on
purpose? Can I prevent it? :)
A minimal (and therefore nonsensical) example:
inductive_set foo :: "('a * 'a) set"
where "(a, b) : foo"
inductive_set bar :: "('a * 'a) set"
where "foop a b ==> (a, b) : bar"
Here I obtain bar.intros
"(?a, ?b) : foo ==> (?a, ?b) : bar
but I would rather like to have
"foop ?a ?b ==> (?a, ?b) : bar"
(that is, what I have written in the definition).
best regards
chris
Email Gateway (Aug 18 2022 at 16:04):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Christian,
according to the sources inductive_set seems indeed to behave like that.
You may call this a bug or a feature.
The rules used for to_set / to_pred conversions are added using
attribute pred_set_conv. Unfortunately, this only allows addition, not
removal, preventing an ad-hoc solution for your problem. Maybe we have
to think about that.
Hope this helps,
Florian
signature.asc
Email Gateway (Aug 18 2022 at 16:06):From: berghofe@in.tum.de
Quoting Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>:
Hi Christian and Florian,
note that the purpose of inductive_set is mainly to make existing
theories using
the old set notation work with the new inductive definition package. The only
promise we are making is that everything that used to work with the old
inductive command will also work with inductive_set. If you are using the
new "...p" predicates introduced by inductive_set to achieve some special
effects, you are on your own, i.e. it may or may not work as you expect.
Greetings,
Stefan
Email Gateway (Aug 18 2022 at 16:06):From: Christian Sternagel <christian.sternagel@uibk.ac.at>
Thnx for your replies,
Does that mean that the general recommendation is to use "inductive"
instead of "inductive_set"? From the documentation (isar-ref) it was not
obvious to me that "inductive_set" is something bad :)
cheers
chris
Email Gateway (Aug 18 2022 at 16:06):From: Tobias Nipkow <nipkow@in.tum.de>
Inductive_set is not bad and will not disappear.
Tobias
Christian Sternagel schrieb:
Email Gateway (Aug 18 2022 at 16:06):From: Christian Sternagel <christian.sternagel@uibk.ac.at>
Hi all,
good to know. Nevertheless, I tried to get rid of the "...p" predicates
provided of my inductive sets. After most of the changes went through
without problems, I now know again, why I originally used "...p"
predicates. It was just in order for "..." in calculational reasoning to
work.
In my concrete example I use the proper subterm relation on first-order
terms. It is now defined as inductive set "supt" such that "(s, t) :
supt" means that s is a superterm of t. Additionally there is an
abbreviation "s |> t" standing for "(s, t) : supt".
In calculational reasoning I want to do steps like
have "s |> t" sorry
also have "... |> u" sorry
but this doesn't work since the dots do not refer to "t" of the first
statement. Can I somehow influence what "..." refers to for special
constants? Or is there any other easy way to make this work (previously
"s |> t" was an abbreviation for "suptp s t" and hence "..." referred to
"t").
cheers
chris
Email Gateway (Aug 18 2022 at 16:06):From: Tobias Nipkow <nipkow@in.tum.de>
Quite independent of inductive_set, I have on occasion wished I could
use "..." to denote particular subterms other than in the default setup.
But this would require a change to Isar and one would need a new concept
for describing "..." positions in terms.
For the time being I recommend to use (is "_ |> ?t") to create your own
"..." in each step. The overhead is bearable, and you can even reuse ?t
in each step and do not have to use ?t1, ?t2 etc.
Tobias
Christian Sternagel schrieb:
Last updated: May 06 2024 at 16:21 UTC