Email Gateway (Aug 18 2022 at 12:01): Email Gateway (Aug 18 2022 at 12:01):From: Peter Lammich <peter.lammich@uni-muenster.de>
Assume I have some lemma in a locale
locale test = fixes A::"'a list set"
assumes [...]
begin
[...]
lemma test[simp]: "a@b\<in>A <--> a\<in>A & b\<in>A"
in order to apply this lemma also to lists of the form "a#as", outside a
locale, I would usually do
lemmas test'[simp] = test[of "[x]", simplified, standard]
the problem is, that standard does not only convert the fixed variable x
to a wildcard variable ?x, but it also prefixes the lemma with an
assumption "test A", because we are inside the locale. Instead of the
desired
"?x#?b\<in>A <--> [?x]\<in>A & b\<in>A",
I get
"test A ==> ?x#?b\<in>A <--> [?x]\<in>A & b\<in>A"
and this lemma won't work as a simplification rule inside the locale
context.
Is there a way to the fixed variables replaced by wildcards, but not
getting this locale-assumption in front of the lemma (of course, without
retyping and proving the special version of the lemma ;) ) ?
Regards,
Peter
Email Gateway (Aug 18 2022 at 12:01):From: Makarius <makarius@sketis.net>
On Wed, 11 Jun 2008, Peter Lammich wrote:
Assume I have some lemma in a locale
locale test = fixes A::"'a list set"
assumes [...]
begin
[...]lemma test[simp]: "a@b\<in>A <--> a\<in>A & b\<in>A"
in order to apply this lemma also to lists of the form "a#as", outside a
locale, I would usually do
lemmas test'[simp] = test[of "[x]", simplified, standard]
Such forward inferences via "simplified" and "standard" as part of fact
declarations do not work well within general local theory targets. You
have already encountered the inherent global nature of "standard". The
"simplified" rule has other potential problems, when transforming locale
results by interpretation, or even just when re-entering the locale
context in a different theory, because the simplification process is
repeated within different dynamic contexts each time!
Is there a way to the fixed variables replaced by wildcards, but not
getting this locale-assumption in front of the lemma (of course, without
retyping and proving the special version of the lemma ;) ) ?
I am not aware of any sane way, apart from the canonical one:
lemma test': "x # b : A <-> [x] : A & b : A"
by (rule test [of "[x]", simplified])
Makarius
Email Gateway (Aug 18 2022 at 12:01):From: Jeremy Dawson <jeremy@rsise.anu.edu.au>
Peter Lammich wrote:
Peter,
I've never tried doing this inside a locale, but, to turn free variables
into ?-variables,
without doing the other stuff that standard does, I have used
(gen_all o forall_intr_frees), thus
val mp' = "[| P --> Q; P |] ==> Q" : Thm.thm
(gen_all o forall_intr_frees) mp';
val it = "[| ?P --> ?Q; ?P |] ==> ?Q" : Thm.thm
Jeremy
Email Gateway (Aug 18 2022 at 12:01):From: Brian Huffman <brianh@cs.pdx.edu>
Quoting Jeremy Dawson <jeremy@rsise.anu.edu.au>:
Peter Lammich wrote:
Is there a way to the fixed variables replaced by wildcards, but
not getting this locale-assumption in front of the lemma (of
course, without retyping and proving the special version of the
lemma ;) ) ?Regards,
PeterPeter,
I've never tried doing this inside a locale, but, to turn free
variables into ?-variables,
without doing the other stuff that standard does, I have used(gen_all o forall_intr_frees), thus
val mp' = "[| P --> Q; P |] ==> Q" : Thm.thm
(gen_all o forall_intr_frees) mp';
val it = "[| ?P --> ?Q; ?P |] ==> ?Q" : Thm.thmJeremy
If you want to use this from Isar, it is actually pretty easy to
define your own theorem attributes, given a function of type thm -> thm:
setup {*
Attrib.add_attributes
[("wildcard",
Attrib.no_args (Thm.rule_attribute (K (gen_all o forall_intr_frees))),
"replace fixed variables by wildcards")];
*}
You can use it like this:
thm mp [of R S]
"[| R --> S; R |] ==> S"
thm mp [of R S, wildcard]
"[| ?R --> ?S; ?R |] ==> ?S"
thm mp [of "x = y", wildcard]
"[| ?x2 = ?y2 --> ?Q; ?x2 = ?y2 |] ==> ?Q"
The "standard" attribute is defined very similarly to this; the code
is in Pure/Isar/attrib.ML:
val standard = no_args (Thm.rule_attribute (K Drule.standard));
It refers to the function Drule.standard from Pure/drule.ML:
val standard' =
implies_intr_hyps
#> forall_intr_frees
#> `Thm.maxidx_of
#-> (fn maxidx =>
Thm.forall_elim_vars (maxidx + 1)
#> Thm.strip_shyps
#> zero_var_indexes
#> Thm.varifyT);
val standard =
flexflex_unique
#> standard'
#> Thm.close_derivation;
As you can see, the "standard" attribute does quite a few things. One
other feature of "standard" you might want to add to "wildcard" would
be to zero the variable indexes, to avoid the problem with the third
example above.
Email Gateway (Aug 18 2022 at 12:01):From: Makarius <makarius@sketis.net>
Note that anything modeled after the old "standard" only works in a global
context. In fact, fixed variables cannot be generalized without leaving
the context, which is not allowed an attribute anyway. So strictly
speaking, the "standard" attribute is a legacy feature, despite its rather
misleading name.
Going back to the original motivation, the demand for generalizing
variables was coming from fact declarations like this:
lemmas a = b [of x]
Here x is an undeclared free variable, and there is no official way to
ever get rid of it. What you actually want is to say that x should be
fixed in the context of the statement, such that it becomes arbitrary in
the result. I.e. something analogous to
lemma a: fixes x shows B x ...
or
lemma a: shows B x ...
where the fixing is implicit.
Neither form is available for compact fact expressions, without an
explicit statement. There are some plans for a more uniform way to put
arbitrary statements (definitions and theorems) into a auxiliary context,
with local fixes and assumes just like the special form for long theorem
statements. At the moment we are still very busy to struggle with
old-style global operations showing up in unexpected corners ...
Makarius
Last updated: May 03 2024 at 12:27 UTC