Email Gateway (Aug 18 2022 at 18:58): Email Gateway (Aug 18 2022 at 18:58):From: Peter Lammich <lammich@in.tum.de>
Hi all,
(Referring to Isabelle2011-1)
I recently ran into the following pitfall:
lemma pitfall1:
notes [[show_sorts]]
notes test = refl[where 'a='a]
fixes x::"'a::default"
shows "x=x"
thm test -- "'a has the wrong sort here!"
using test apply -
Now it outputs:
type variables:
'a :: type
'a :: default
and, of course, apply (rule test) fails. When inspecting this failure,
the already confused user gets the following trace from the unifier
(even with show_sorts turned on!)
The following types do not unify:
'a \<Rightarrow> 'a \<Rightarrow> bool
'a \<Rightarrow> 'a \<Rightarrow> bool
I would expect that a type-variable with the same name should also have
the same sort -- at least when I introduce it within the
scope of the very same lemma.
And even more strange, this pitfall can be resolved by just swapping the
notes and the fixes declaration:
lemma pitfall1_resolved:
fixes x::"'a::default"
notes [[show_sorts]]
notes test = refl[where 'a='a]
shows "x=x"
by (rule test)
Regards,
Peter
Email Gateway (Aug 18 2022 at 19:09):From: Makarius <makarius@sketis.net>
Is this just an exercise in driving the system into an unspecified /
uninhabitable state, or does it have some practical significance?
There are many things happening in a compund theorem statement, and the
use of the above words of "wrong", "expect", "strange" are meaningless in
this context. Where is it ever specified that it should behave like that?
The above forms are very uncommon, so uncommon effects are to be expected.
I am not going to explain here the accidental behaviour of certain
boundary cases in complex theorem statements: certain things are
simultaneous here, other things are sequential, other things undefined.
Anyway, I've required some time to guess that "trace from the unifier"
probably means Pattern.trace_unify_fail := true. But that is a global ML
reference, so it already indicates that the related operations are not yet
"localized". That means they don't observe the local context resulting
from your "notes [[show_sorts]]", which is a bit odd anyway.
So when you say "even with show_sorts turned on", it is actually not
turned on for the pattern unification module. When doing the more usual
"declare [[show_sorts]]" before the lemma statement you get the sort
information printed as expected.
Makarius
Email Gateway (Aug 18 2022 at 19:09):From: Peter Lammich <lammich@in.tum.de>
Is this just an exercise in driving the system into an unspecified /
uninhabitable state, or does it have some practical significance?
I have distilled that from a practical example, that went like this:
schematic_lemma
notes [refine_transfer] = <Some lemmas that only makes sense for this
particular refinement proof>
shows "?concrete_program <= abstract_program"
by (tactic that uses lemmas declared with attribute
"refine_transfer" (which is a NamedThms structure)
As I do not know how to refer to the schematic
variable ?concrete_program when I do
proof - note [refine_transfer] = ... show "xxx" ...
(For xxx, neither ?thesis nor "?concrete_program <= abstract_program"
works),
I used the notes-syntax.
An alternative would be to pass the lemmas as parameters to my tactic,
which I have already (partially) implemented (after writing the first
mail ;) ).
Peter
Email Gateway (Aug 18 2022 at 19:09):From: Makarius <makarius@sketis.net>
On Wed, 15 Feb 2012, Peter Lammich wrote:
Is this just an exercise in driving the system into an unspecified /
uninhabitable state, or does it have some practical significance?I have distilled that from a practical example, that went like this:
schematic_lemma
notes [refine_transfer] = <Some lemmas that only makes sense for this
particular refinement proof>
shows "?concrete_program <= abstract_program"
by (tactic that uses lemmas declared with attribute
"refine_transfer" (which is a NamedThms structure)
BTW, the thing given as arguments to the command 'by' is called "proof
method" or just "method" in Isar terminology. There are further
explanations and some examples in section 6.2 of the
Isabelle/Implementation manual. (The same manual also explains the
traditional concept of "tactic" in Isabelle/ML, see section 4.1.)
An alternative would be to pass the lemmas as parameters to my tactic,
which I have already (partially) implemented
This would indeed follow the standard convention: a method that accepts
implicit arguments via the context also allows the same as explicit
arguments on the spot. The my_simp' example from the quoted section 6.2
above does exactly that.
Makarius
Email Gateway (Aug 18 2022 at 19:09):From: Peter Lammich <lammich@in.tum.de>
BTW, the thing given as arguments to the command 'by' is called "proof
method" or just "method" in Isar terminology.
sorry for the confusion here.
An alternative would be to pass the lemmas as parameters to my tactic,
which I have already (partially) implementedThis would indeed follow the standard convention: a method that accepts
implicit arguments via the context also allows the same as explicit
arguments on the spot.
For my application, it has, however, the disadvantage that the setup has
to be repeated each time I apply a method. For example, I want to
support proofs like:
schematic_lemma
notes [refine_transfer] = some lengthy setup
notes [...] = ...
shows "?c <= a"
apply (my_method)
apply (some user-specified proof of subgoal, thereby instantiating
schematics on that the rest of the proof depends)
apply (my_method)
apply (some user-specified instantiation)
apply (my_method)
...
done
When I do the setup locally for the proof method, I have to repeat it
each time I apply the method. What I really want is to do the setup for
the whole proof.
Perhaps, what I'm doing here is an abuse of the original intention of
schematic_lemma ??
Peter
Last updated: Apr 25 2024 at 08:20 UTC