Re: [isabelle-dev] [isabelle] match_tac, schematic and bound variables
This is a tricky point, but on balance, I think it's better to have complete documentation even if it draws people's attention to things they should overlook. Larry On 19 Aug 2013, at 22:41, Makarius makar...@sketis.net wrote: Of course you are welcome to update your documentation snippet on match_tac. I am also ready to remove it from the documentation altogether. Brushing up the old ref material since 2008 for the implementation manual has introduced some bias towards vintage operations. E.g. some readers have pointed out the relative insignificance of the res_inst_tac family just after I had reconstructed that section -- and they were right about it. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [isabelle] match_tac, schematic and bound variables
Am 17/08/2013 15:20, schrieb Makarius: On Thu, 15 Aug 2013, Lawrence Paulson wrote: I think that the only way to achieve the documented behaviour is to replace all schematic variables in the goal by Frees before attempting resolution. Which can be done safely outside the kernel. If you would do that for the quais-match mode of unify.ML in general it would probably break down everything else. Doing the above in user space instead, in the actual application at hand (which was not explained on this thread so far) it might turn out trivial. So every application that needs matching should implement it separately? I have seen more elegant designs ;-) Tobias Combinators like Subgoal.FOCUS have replaced a lot of old-style tinkering with goals; within the focused parts things are fixed and don't get instantiated by accident. (Tools built on such high-level elements need to be ready to work with renamings of the original schematic variables. This is the normal situation in structured proof elements.) Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [isabelle] match_tac, schematic and bound variables
Your point of view makes sense on general principles, but not in this particular case. I had actually forgotten that these tactics existed. But they form a core part of the classical reasoner, and there are good reasons why they work the way they do. The proof state could be very large, so their quick and dirty method of leaving it unchanged (by deleting updates to it, rather than replacing its variables by constants) is necessary to achieve acceptable performance. I included these tactics in the documentation in a spirit of openness, and it made sense 20 years ago, when there weren't many developers and anything might be expected to not quite work as advertised in what was obviously a research prototype. But now people have the right to expect things to work as documented. In this case, I would change the documentation, and perhaps make it clear that these are very specialist tools. Larry On 19 Aug 2013, at 07:11, Tobias Nipkow nip...@in.tum.de wrote: Am 17/08/2013 15:20, schrieb Makarius: On Thu, 15 Aug 2013, Lawrence Paulson wrote: I think that the only way to achieve the documented behaviour is to replace all schematic variables in the goal by Frees before attempting resolution. Which can be done safely outside the kernel. If you would do that for the quais-match mode of unify.ML in general it would probably break down everything else. Doing the above in user space instead, in the actual application at hand (which was not explained on this thread so far) it might turn out trivial. So every application that needs matching should implement it separately? I have seen more elegant designs ;-) Tobias Combinators like Subgoal.FOCUS have replaced a lot of old-style tinkering with goals; within the focused parts things are fixed and don't get instantiated by accident. (Tools built on such high-level elements need to be ready to work with renamings of the original schematic variables. This is the normal situation in structured proof elements.) Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [isabelle] match_tac, schematic and bound variables
Am 19/08/2013 12:45, schrieb Lawrence Paulson: Your point of view makes sense on general principles, but not in this particular case. I had actually forgotten that these tactics existed. But they form a core part of the classical reasoner, and there are good reasons why they work the way they do. The proof state could be very large, so their quick and dirty method of leaving it unchanged (by deleting updates to it, rather than replacing its variables by constants) is necessary to achieve acceptable performance. I agree and it is not a top priority. But it is an interesting challenge to do it outside the kernel, and I do wonder if the performance would take a real hit. I included these tactics in the documentation in a spirit of openness, and it made sense 20 years ago, when there weren't many developers and anything might be expected to not quite work as advertised in what was obviously a research prototype. But now people have the right to expect things to work as documented. In this case, I would change the documentation, and perhaps make it clear that these are very specialist tools. That's what I meant. It should merely state explicitly that these tactics merely discard unifiers that would update the goal state. can lead to incompleteness. Tobias Larry On 19 Aug 2013, at 07:11, Tobias Nipkow nip...@in.tum.de wrote: Am 17/08/2013 15:20, schrieb Makarius: On Thu, 15 Aug 2013, Lawrence Paulson wrote: I think that the only way to achieve the documented behaviour is to replace all schematic variables in the goal by Frees before attempting resolution. Which can be done safely outside the kernel. If you would do that for the quais-match mode of unify.ML in general it would probably break down everything else. Doing the above in user space instead, in the actual application at hand (which was not explained on this thread so far) it might turn out trivial. So every application that needs matching should implement it separately? I have seen more elegant designs ;-) Tobias Combinators like Subgoal.FOCUS have replaced a lot of old-style tinkering with goals; within the focused parts things are fixed and don't get instantiated by accident. (Tools built on such high-level elements need to be ready to work with renamings of the original schematic variables. This is the normal situation in structured proof elements.) Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [isabelle] match_tac, schematic and bound variables
I was about to change the documentation to say just that, only to discover that
almost exactly the same change was made in November 2008.
wenzelm 50072 Wed Nov 07 16:02:43 2012 +0100
src/Doc/IsarImplementation/Tactic.thy:321: \item @{ML match_tac}, @{ML
ematch_tac}, @{ML dmatch_tac}, and @{ML
wenzelm 50072 Wed Nov 07 16:02:43 2012 +0100
src/Doc/IsarImplementation/Tactic.thy:322: bimatch_tac} are similar to @{ML
resolve_tac}, @{ML eresolve_tac},
wenzelm 50072 Wed Nov 07 16:02:43 2012 +0100
src/Doc/IsarImplementation/Tactic.thy:323: @{ML dresolve_tac}, and @{ML
biresolve_tac}, respectively, but do
wenzelm 50072 Wed Nov 07 16:02:43 2012 +0100
src/Doc/IsarImplementation/Tactic.thy:324: not instantiate schematic
variables in the goal state.
wenzelm 28783 Thu Nov 13 22:05:49 2008 +0100
doc-src/IsarImplementation/Thy/tactic.thy:321:
wenzelm 28783 Thu Nov 13 22:05:49 2008 +0100
doc-src/IsarImplementation/Thy/tactic.thy:322: Flexible subgoals are not
updated at will, but are left alone.
wenzelm 28783 Thu Nov 13 22:05:49 2008 +0100
doc-src/IsarImplementation/Thy/tactic.thy:323: Strictly speaking, matching
means to treat the unknowns in the goal
wenzelm 28783 Thu Nov 13 22:05:49 2008 +0100
doc-src/IsarImplementation/Thy/tactic.thy:324: state as constants; these
tactics merely discard unifiers that would
wenzelm 28783 Thu Nov 13 22:05:49 2008 +0100
doc-src/IsarImplementation/Thy/tactic.thy:325: update the goal state.
Larry
On 19 Aug 2013, at 12:30, Tobias Nipkow nip...@in.tum.de wrote:
Am 19/08/2013 12:45, schrieb Lawrence Paulson:
Your point of view makes sense on general principles, but not in this
particular case.
I had actually forgotten that these tactics existed. But they form a core
part of the classical reasoner, and there are good reasons why they work the
way they do. The proof state could be very large, so their quick and dirty
method of leaving it unchanged (by deleting updates to it, rather than
replacing its variables by constants) is necessary to achieve acceptable
performance.
I agree and it is not a top priority. But it is an interesting challenge to do
it outside the kernel, and I do wonder if the performance would take a real
hit.
I included these tactics in the documentation in a spirit of openness, and
it made sense 20 years ago, when there weren't many developers and anything
might be expected to not quite work as advertised in what was obviously a
research prototype. But now people have the right to expect things to work
as documented. In this case, I would change the documentation, and perhaps
make it clear that these are very specialist tools.
That's what I meant. It should merely state explicitly that these tactics
merely discard unifiers that would update the goal state. can lead to
incompleteness.
Tobias
Larry
On 19 Aug 2013, at 07:11, Tobias Nipkow nip...@in.tum.de wrote:
Am 17/08/2013 15:20, schrieb Makarius:
On Thu, 15 Aug 2013, Lawrence Paulson wrote:
I think that the only way to achieve the documented behaviour is to
replace
all schematic variables in the goal by Frees before attempting resolution.
Which can be done safely outside the kernel.
If you would do that for the quais-match mode of unify.ML in general it
would
probably break down everything else.
Doing the above in user space instead, in the actual application at hand
(which
was not explained on this thread so far) it might turn out trivial.
So every application that needs matching should implement it separately? I
have
seen more elegant designs ;-)
Tobias
Combinators like Subgoal.FOCUS have replaced a lot of old-style tinkering
with
goals; within the focused parts things are fixed and don't get
instantiated by
accident. (Tools built on such high-level elements need to be ready to
work
with renamings of the original schematic variables. This is the normal
situation
in structured proof elements.)
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [isabelle] match_tac, schematic and bound variables
On Sun, 18 Aug 2013, Lars Noschinski wrote: Combinators like Subgoal.FOCUS have replaced a lot of old-style tinkering with goals; within the focused parts things are fixed and don't get instantiated by accident. I seem to remember a discussion on the mailing list that Subgoal.FOCUS does not export schematic type variables. So this would give us another not-quite correct match implementation. I still have this on my list to look after it in further detail, but as far as I can tell it was about situations that are conceptially not allowed anyway: schematic type variables within fixed-term variables. The inference kernel happens to allow that in primitive rules, but almost everything will break down. Type-inference is part of the syntactic phase, and needs to be finished before doing the actual logical inferencing. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [isabelle] match_tac, schematic and bound variables
On Mon, 19 Aug 2013, Tobias Nipkow wrote: Am 17/08/2013 15:20, schrieb Makarius: On Thu, 15 Aug 2013, Lawrence Paulson wrote: I think that the only way to achieve the documented behaviour is to replace all schematic variables in the goal by Frees before attempting resolution. Which can be done safely outside the kernel. If you would do that for the quais-match mode of unify.ML in general it would probably break down everything else. Doing the above in user space instead, in the actual application at hand (which was not explained on this thread so far) it might turn out trivial. So every application that needs matching should implement it separately? So far the actual application and its concrete approach was not really explained on this thread. It is bread-and-butter in the use of the operations around pattern.ML and unify.ML to look closely what they can do and what not. I have my own catalogue of things that just don't work, e.g see this recent incident here https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2013-July/msg00084.html concerning ?P x where x has function type. I don't think that it is realistic to fix these highly complex modules without causing much greater harm. To get it really right, someone would have to sit down and spend substantial time and effort on it, and preferably do some formal proofs about the whole complex. Actually integrating an improved implementation would then be a second step, with the usual surprises to be expected, when things at the very bottom are changed and other tools expect the old behaviour, even it was a bad one. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [isabelle] match_tac, schematic and bound variables
On Mon, 19 Aug 2013, Lawrence Paulson wrote:
I was about to change the documentation to say just that, only to
discover that almost exactly the same change was made in November 2008.
wenzelm 50072 Wed Nov 07 16:02:43 2012 +0100
src/Doc/IsarImplementation/Tactic.thy:321: \item @{ML match_tac}, @{ML
ematch_tac}, @{ML dmatch_tac}, and @{ML
wenzelm 50072 Wed Nov 07 16:02:43 2012 +0100
src/Doc/IsarImplementation/Tactic.thy:322: bimatch_tac} are similar to @{ML
resolve_tac}, @{ML eresolve_tac},
wenzelm 50072 Wed Nov 07 16:02:43 2012 +0100
src/Doc/IsarImplementation/Tactic.thy:323: @{ML dresolve_tac}, and @{ML
biresolve_tac}, respectively, but do
wenzelm 50072 Wed Nov 07 16:02:43 2012 +0100
src/Doc/IsarImplementation/Tactic.thy:324: not instantiate schematic
variables in the goal state.
wenzelm 28783 Thu Nov 13 22:05:49 2008 +0100
doc-src/IsarImplementation/Thy/tactic.thy:321:
wenzelm 28783 Thu Nov 13 22:05:49 2008 +0100
doc-src/IsarImplementation/Thy/tactic.thy:322: Flexible subgoals are not
updated at will, but are left alone.
wenzelm 28783 Thu Nov 13 22:05:49 2008 +0100
doc-src/IsarImplementation/Thy/tactic.thy:323: Strictly speaking, matching
means to treat the unknowns in the goal
wenzelm 28783 Thu Nov 13 22:05:49 2008 +0100
doc-src/IsarImplementation/Thy/tactic.thy:324: state as constants; these
tactics merely discard unifiers that would
wenzelm 28783 Thu Nov 13 22:05:49 2008 +0100
doc-src/IsarImplementation/Thy/tactic.thy:325: update the goal state.
I cannot read the above copy paste from what you see on your screen. When
pointing to the history you need to tell the changeset id (abbreviated
hashkey) not the phyical index or date.
Refurbishing all these old manuals over several years, I have moved around
things between different files and directories, so that match_tac is now
in the implementation manual here:
http://isabelle.in.tum.de/repos/isabelle/file/15fe0ca088b3/src/Doc/IsarImplementation/Tactic.thy#l336
It originally comes from your initial version of the ref manual
http://isabelle.in.tum.de/repos/isabelle/annotate/d8205bb279a7/doc-src/Ref/tactic.tex#l74
This text from Nov 1993 gives a sense of the anciety of this stuff.
Clearly the system around it has improved way beyond the research
prototype nature of the original Isabelle with unify.ML at its core.
(I am still convinced that it was a very good approach, and don't want to
see it destroyed at the very core.)
Of course you are welcome to update your documentation snippet on
match_tac. I am also ready to remove it from the documentation
altogether. Brushing up the old ref material since 2008 for the
implementation manual has introduced some bias towards vintage
operations. E.g. some readers have pointed out the relative insignificance
of the res_inst_tac family just after I had reconstructed that section --
and they were right about it.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [isabelle] match_tac, schematic and bound variables
On Thu, 15 Aug 2013, Lawrence Paulson wrote: I think that the only way to achieve the documented behaviour is to replace all schematic variables in the goal by Frees before attempting resolution. If you would do that for the quais-match mode of unify.ML in general it would probably break down everything else. Doing the above in user space instead, in the actual application at hand (which was not explained on this thread so far) it might turn out trivial. Combinators like Subgoal.FOCUS have replaced a lot of old-style tinkering with goals; within the focused parts things are fixed and don't get instantiated by accident. (Tools built on such high-level elements need to be ready to work with renamings of the original schematic variables. This is the normal situation in structured proof elements.) Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [isabelle] match_tac, schematic and bound variables
On Thu, 15 Aug 2013, Lawrence Paulson wrote: On 13 Aug 2013, at 10:35, Lars Noschinski nosch...@in.tum.de wrote: It might be interesting to note that also Unify.matchers is not able to match such term. This old thread on Unify.matchers might be also interesting: https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2011-August/msg00080.html Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [isabelle] match_tac, schematic and bound variables
Probably you are right. Larry On 17 Aug 2013, at 14:20, Makarius makar...@sketis.net wrote: On Thu, 15 Aug 2013, Lawrence Paulson wrote: I think that the only way to achieve the documented behaviour is to replace all schematic variables in the goal by Frees before attempting resolution. If you would do that for the quais-match mode of unify.ML in general it would probably break down everything else. Doing the above in user space instead, in the actual application at hand (which was not explained on this thread so far) it might turn out trivial. Combinators like Subgoal.FOCUS have replaced a lot of old-style tinkering with goals; within the focused parts things are fixed and don't get instantiated by accident. (Tools built on such high-level elements need to be ready to work with renamings of the original schematic variables. This is the normal situation in structured proof elements.) Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [isabelle] match_tac, schematic and bound variables
I think that the only way to achieve the documented behaviour is to replace all
schematic variables in the goal by Frees before attempting resolution. I'm not
sure what effect this would have on performance.
Larry
On 13 Aug 2013, at 10:35, Lars Noschinski nosch...@in.tum.de wrote:
On 12.08.2013 18:13, Makarius wrote:
Flexible subgoals are not updated at will, but are left alone.
Strictly speaking, matching means to treat the unknowns in the goal
state as constants; these tactics merely discard unifiers that would
update the goal state.
Peter and I did some investigation and this seems to be the source of this
behaviour: If two schematic variables (with only bound variables as
arguments) are to be unified, Unifiers.unify will always provide a single
unifier with the schematic variables reordered.
It might be interesting to note that also Unify.matchers is not able to match
such term.
theory Scratch imports Main begin (* Isabelle 2013 *)
ML {*
val pat = @{cpat ⋀x y. ?P x y}
val term = @{cpat ⋀x y. ?Q x y x}
val pair = [(term_of pat, term_of term)]
fun maxidx_of_cterm ct = case rep_cterm ct of
{maxidx, ...} = maxidx
val maxidx = Int.max (maxidx_of_cterm pat, maxidx_of_cterm term)
*}
ML {*
fun pretty_subst ctxt ((name,_), (typ, term)) =
[Pretty.str name, Syntax.pretty_typ ctxt typ, Syntax.pretty_term ctxt term]
| Pretty.list
val pretty_env =
Envir.term_env # Vartab.dest # map (pretty_subst @{context}) #
Pretty.big_list Unifier
val pretty_env_list = map pretty_env # Pretty.big_list Unifiers
*}
ML {*
Unify.unifiers (@{theory}, Envir.empty maxidx, pair)
| Seq.list_of
| map fst
| pretty_env_list
| Pretty.string_of
| tracing
*}
ML {*
Unify.matchers @{theory} pair | Seq.list_of | pretty_env_list |
Pretty.string_of | tracing
*}
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
