Re: [isabelle-dev] Fwd: [isabelle] Problem with frule_tac substitution
The simplicity of the new code compared with the old suggests that this
treatment is easier to understand, so we should give it a try.
It is interesting that local scopes within structured proofs generate theorems
with nonzero indices, but of course that is a separate matter.
Larry
On 8 Feb 2011, at 17:19, Brian Huffman wrote:
On Tue, Feb 8, 2011 at 9:01 AM, Lawrence Paulson l...@cam.ac.uk wrote:
Historically, the point is that index numbers were regarded as very
important in variable names, while identifiers ending with digits were not
seen as important. And there are other ways of making multiple identifiers.
Nowadays, there aren't that many situations where a user would need to refer
to a nonzero index number.
Larry
I tried changing the parsing/printing of indexnames, to see how
serious of an incompatibility it would be. The diffs of
Syntax/lexicon.ML (parsing) and term.ML (printing) are pasted at the
bottom of this email.
I found that nothing in HOL-Main is affected by this change. A few
proof scripts below Complex_Main are affected, though, where the proof
script actually does need to refer to a nonzero index number. There
are two kinds of situations where this happens:
* Explicitly instantiating a rule made with THEN or OF, such as
apply (rule_tac ?a.1 = log a x in add_left_cancel [THEN iffD1])
* Instantiating a rule proved within an open-brace-close-brace block
in a structured proof. I was surprised by this one. For example:
lemma True
proof -
{ fix n :: nat
have n = n by simp
}
this:
?n2 = ?n2
I expected this to have the form ?n = ?n, with index 0. But for
some reason, the actual rule uses index 2. Some proof scripts in
SEQ.thy use something like note foo = this, followed later with an
instantiation using the where attribute that refers to the nonzero
index.
- Brian
diff -r ab3f6d76fb23 src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.MLTue Feb 08 16:10:10 2011 +0100
+++ b/src/Pure/Syntax/lexicon.MLTue Feb 08 09:03:50 2011 -0800
@@ -297,21 +297,9 @@
let
fun nat n [] = n
| nat n (c :: cs) = nat (n * 10 + (ord c - ord 0)) cs;
-
-fun idxname cs ds = (implode (rev cs), nat 0 ds);
-fun chop_idx [] ds = idxname [] ds
- | chop_idx (cs as (_ :: \\^isub :: _)) ds = idxname cs ds
- | chop_idx (cs as (_ :: \\^isup :: _)) ds = idxname cs ds
- | chop_idx (c :: cs) ds =
- if Symbol.is_digit c then chop_idx cs (c :: ds)
- else idxname (c :: cs) ds;
-
-val scan = (scan_id map Symbol_Pos.symbol) --
- Scan.optional ($$$ . |-- scan_nat (nat 0 o map
Symbol_Pos.symbol)) ~1;
in
-scan
- (fn (cs, ~1) = chop_idx (rev cs) []
-| (cs, i) = (implode cs, i))
+(scan_id (implode o map Symbol_Pos.symbol)) --
+ Scan.optional ($$$ . |-- scan_nat (nat 0 o map
Symbol_Pos.symbol)) 0
end;
in
diff -r ab3f6d76fb23 src/Pure/term.ML
--- a/src/Pure/term.ML Tue Feb 08 16:10:10 2011 +0100
+++ b/src/Pure/term.ML Tue Feb 08 09:03:50 2011 -0800
@@ -990,15 +990,8 @@
fun string_of_vname (x, i) =
let
val idx = string_of_int i;
-val dot =
- (case rev (Symbol.explode x) of
-_ :: \\^isub :: _ = false
- | _ :: \\^isup :: _ = false
- | c :: _ = Symbol.is_digit c
- | _ = true);
in
-if dot then ? ^ x ^ . ^ idx
-else if i 0 then ? ^ x ^ idx
+if i 0 then ? ^ x ^ . ^ idx
else ? ^ x
end;
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Fwd: [isabelle] Problem with frule_tac substitution
This indeed is probably one of the chief reasons for the existing arrangements. Larry On 9 Feb 2011, at 08:36, Alexander Krauss wrote: An incompatibility that will not be reported by tests is that intermediate goal states, where nonzero indexnames are quite frequent, will look significantly different and contain many dots. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Fwd: [isabelle] Problem with frule_tac substitution
On Wed, 9 Feb 2011, Gerwin Klein wrote: I don't mind either way, but I'd like to point out that the _tac instantiations are everything but out of fashion. I'm fully aware that they are bad style, rely on dynamic names, etc, but there is no way around them if you write apply style. Having observed the conceptual problems already many years ago, I am also fully aware that the res_inst_tac variants still occur in practically important proof script. At some point one should seriously revisit the question why this is so, and what needs to be done to make a significant step forward (away from adhoc instantiations). Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Fwd: [isabelle] Problem with frule_tac substitution
On Wed, 9 Feb 2011, Tobias Nipkow wrote: It is interesting that local scopes within structured proofs generate theorems with nonzero indices, but of course that is a separate matter. Yes, that is a new aspect that was introduced around 1998/1999. I would be more interested in the why than the when. Generating unpredictable names does not contribute to stability of proofs. The stage of 1998/1999 refers the way how Isar generally treats local fixes, with import and export of results. Apart from introducing a whole new conceptual level of proper local context, it has also solved older known problems (e.g. of the freeze_thaw family of functions, although there are still there as legacy). After 1999 there were further aspects coming in -- I can't give a comprehensive overview right now, apart from what is written in the implementation manual. (How many people have actually read it?) Working with nested scopes naturally involves situation where literal names cannot be maintained from start to end. Otherwise lambda calculus with capture-free substitution etc. would be trivial. If you take the res_inst_tac family for example, there is an internal treatment of names like x, xa, xb that some people know by the jargon name of as-they-are-printed, with some funny effects. There are many more fine points that have shown up and been adressed concerning the delicate question of contexts, variable scoping, renaming etc. over years. The discussion right now seems to say: This has all been nonsense, and should be thrown away. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Fwd: [isabelle] Problem with frule_tac substitution
If your analogy with lambda calculus is correct, than there are
situations when one must rename something exported from a proof block.
That I do not understand. Take this example:
lemma True
proof-
{ fix n::nat have n=n by auto }
produces ?n2 = ?n2. I do not see why it could not produce ?n = ?n.
To continue your analogy with lambda-calculus: I can understand why
renaming is necessary in lambda-calculus without reading an
implementation manual. Of course, certain implementations of
lambda-calculus may rename more than is necessary, for implementation
reasons - is that what you mean?
Tobias
Makarius schrieb:
On Wed, 9 Feb 2011, Tobias Nipkow wrote:
It is interesting that local scopes within structured proofs
generate theorems with nonzero indices, but of course that is a
separate matter.
Yes, that is a new aspect that was introduced around 1998/1999.
I would be more interested in the why than the when. Generating
unpredictable names does not contribute to stability of proofs.
The stage of 1998/1999 refers the way how Isar generally treats local
fixes, with import and export of results. Apart from introducing a
whole new conceptual level of proper local context, it has also solved
older known problems (e.g. of the freeze_thaw family of functions,
although there are still there as legacy). After 1999 there were
further aspects coming in -- I can't give a comprehensive overview right
now, apart from what is written in the implementation manual. (How many
people have actually read it?)
Working with nested scopes naturally involves situation where literal
names cannot be maintained from start to end. Otherwise lambda calculus
with capture-free substitution etc. would be trivial. If you take the
res_inst_tac family for example, there is an internal treatment of names
like x, xa, xb that some people know by the jargon name of
as-they-are-printed, with some funny effects.
There are many more fine points that have shown up and been adressed
concerning the delicate question of contexts, variable scoping, renaming
etc. over years. The discussion right now seems to say: This has all
been nonsense, and should be thrown away.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Fwd: [isabelle] Problem with frule_tac substitution
On 02/09/2011 03:39 PM, Tobias Nipkow wrote:
If your analogy with lambda calculus is correct, than there are
situations when one must rename something exported from a proof block.
That I do not understand. Take this example:
lemma True
proof-
{ fix n::nat have n=n by auto }
produces ?n2 = ?n2. I do not see why it could not produce ?n = ?n.
AFAIK this question is mostly equivalent to the question
Why does Variable.export use maxidx instead of reusing names and
relying on an invariant like 'names are always fixed'?
and the answer I was given (by Makarius in May 2010 in private Email
conversation)
to that question is something like
tools aren't this well behaved, such an invariant does not hold in
general.
IIRC I even had the pleasure to witness this behaviour in actual code.
Regards,
Andy
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Fwd: [isabelle] Problem with frule_tac substitution
On Wed, 9 Feb 2011, Alexander Krauss wrote: I don't think that anybody wants to say (or imply) anything like that. As I understood it, this particular point (Why do nonzero indexnames show up in this situation, and shouldn't they rather be normalized to zero as they are in other situations (e.g. toplevel statements), too?) may simply be yet another fine point that one might want to address in the future. In particular, this fine point is completely orthogonal to the issue of concrete syntax for indexnames that was raised initially. I have worked on all this for many years, and there are connections in very fine points. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Fwd: [isabelle] Problem with frule_tac substitution
On Wed, 9 Feb 2011, Tobias Nipkow wrote: I can see the technical reason for having to rename sometimes (almost never, as you write), but disagree with renaming by default. In 2005/2006 I have myself reconsidered this question again thoroughly, and concluded that it is the less surprising way. I even consulted with Christian as the Nominal expert at that point and he agreed :-) A related profane example from the Java. The JVM has UTF-16 encoding for unicode and almost always there is a one-to-one correspondence between characters and code-points. In rare cases they have to use 2 characters to represent symbols from some newer variant unicode standard. Since this happens rarely, practically no Java program treats it correctly, violating the official standards. If they would have used UTF-8 instead (which did not exist when Java emerged) programmers would be used to multi-byte sequences regularly and we could now have \A as 풜 without crashing the editor. But I am glad that at least top-level theorems are not subject to this - I assume scope intrusion can happen there as well? The toplevel works a bit differently (there is also a formal flag to distinguish statement mode from proof body mode). An interesting challenge for toplevel results are the morphisms that are applied to move between hypothetical contexts and application contexts. There is also an interaction with the of and where attributes here. One of the long-pending reforms is move instantiation out of this dangerous zone, for example. (I am pondering this for quite some years already. Someday all the Mikado sticks will have been removed in proper order.) Anyway, conversation about Isabelle history (past and future) is interesting, but there is a whole lot of work in the pipeline (work that has been thought through for a long time already). Makarius___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Fwd: [isabelle] Problem with frule_tac substitution
The Java analogy is a bit odd. There you have the choice between following the standard and not following it. But when instantiating a thm obtained from a proof block, you are at the mercy of the renaming chosen by the system. And if the system choses a different index tomorrow, practically all those instantiations break. But if the indices are normalized, then only those almost never cases break. Tobias Makarius schrieb: On Wed, 9 Feb 2011, Tobias Nipkow wrote: I can see the technical reason for having to rename sometimes (almost never, as you write), but disagree with renaming by default. In 2005/2006 I have myself reconsidered this question again thoroughly, and concluded that it is the less surprising way. I even consulted with Christian as the Nominal expert at that point and he agreed :-) A related profane example from the Java. The JVM has UTF-16 encoding for unicode and almost always there is a one-to-one correspondence between characters and code-points. In rare cases they have to use 2 characters to represent symbols from some newer variant unicode standard. Since this happens rarely, practically no Java program treats it correctly, violating the official standards. If they would have used UTF-8 instead (which did not exist when Java emerged) programmers would be used to multi-byte sequences regularly and we could now have \A as 풜 without crashing the editor. But I am glad that at least top-level theorems are not subject to this - I assume scope intrusion can happen there as well? The toplevel works a bit differently (there is also a formal flag to distinguish statement mode from proof body mode). An interesting challenge for toplevel results are the morphisms that are applied to move between hypothetical contexts and application contexts. There is also an interaction with the of and where attributes here. One of the long-pending reforms is move instantiation out of this dangerous zone, for example. (I am pondering this for quite some years already. Someday all the Mikado sticks will have been removed in proper order.) Anyway, conversation about Isabelle history (past and future) is interesting, but there is a whole lot of work in the pipeline (work that has been thought through for a long time already). Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Fwd: [isabelle] Problem with frule_tac substitution
The *_tac-style instantiation might be out of fashion, but the same parsing rules for indexnames are also used with the where attribute, which is still quite useful. - Brian On Tue, Feb 8, 2011 at 7:59 AM, Lawrence Paulson l...@cam.ac.uk wrote: Obviously this proposal would involve a significant incompatibility. It may not even be very relevant any more, as this sort of instantiation is rather out of fashion. But it is worth a discussion. Larry Begin forwarded message: I would propose to simplify the parsing rules to work like this: Any variable name with index 0 can be referred to without a question mark or dot, and a dot is always required for indices other than 0. x, ?x and ?x.0 parse as (x, 0) x0, ?x0 and ?x0.0 parse as (x0, 0) x2, ?x2 and ?x2.0 parse as (x2, 0) ?x.2 parses as (x, 2) ___ 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] Fwd: [isabelle] Problem with frule_tac substitution
On Tue, Feb 8, 2011 at 9:01 AM, Lawrence Paulson l...@cam.ac.uk wrote:
Historically, the point is that index numbers were regarded as very important
in variable names, while identifiers ending with digits were not seen as
important. And there are other ways of making multiple identifiers. Nowadays,
there aren't that many situations where a user would need to refer to a
nonzero index number.
Larry
I tried changing the parsing/printing of indexnames, to see how
serious of an incompatibility it would be. The diffs of
Syntax/lexicon.ML (parsing) and term.ML (printing) are pasted at the
bottom of this email.
I found that nothing in HOL-Main is affected by this change. A few
proof scripts below Complex_Main are affected, though, where the proof
script actually does need to refer to a nonzero index number. There
are two kinds of situations where this happens:
* Explicitly instantiating a rule made with THEN or OF, such as
apply (rule_tac ?a.1 = log a x in add_left_cancel [THEN iffD1])
* Instantiating a rule proved within an open-brace-close-brace block
in a structured proof. I was surprised by this one. For example:
lemma True
proof -
{ fix n :: nat
have n = n by simp
}
this:
?n2 = ?n2
I expected this to have the form ?n = ?n, with index 0. But for
some reason, the actual rule uses index 2. Some proof scripts in
SEQ.thy use something like note foo = this, followed later with an
instantiation using the where attribute that refers to the nonzero
index.
- Brian
diff -r ab3f6d76fb23 src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.MLTue Feb 08 16:10:10 2011 +0100
+++ b/src/Pure/Syntax/lexicon.MLTue Feb 08 09:03:50 2011 -0800
@@ -297,21 +297,9 @@
let
fun nat n [] = n
| nat n (c :: cs) = nat (n * 10 + (ord c - ord 0)) cs;
-
-fun idxname cs ds = (implode (rev cs), nat 0 ds);
-fun chop_idx [] ds = idxname [] ds
- | chop_idx (cs as (_ :: \\^isub :: _)) ds = idxname cs ds
- | chop_idx (cs as (_ :: \\^isup :: _)) ds = idxname cs ds
- | chop_idx (c :: cs) ds =
- if Symbol.is_digit c then chop_idx cs (c :: ds)
- else idxname (c :: cs) ds;
-
-val scan = (scan_id map Symbol_Pos.symbol) --
- Scan.optional ($$$ . |-- scan_nat (nat 0 o map
Symbol_Pos.symbol)) ~1;
in
-scan
- (fn (cs, ~1) = chop_idx (rev cs) []
-| (cs, i) = (implode cs, i))
+(scan_id (implode o map Symbol_Pos.symbol)) --
+ Scan.optional ($$$ . |-- scan_nat (nat 0 o map Symbol_Pos.symbol)) 0
end;
in
diff -r ab3f6d76fb23 src/Pure/term.ML
--- a/src/Pure/term.ML Tue Feb 08 16:10:10 2011 +0100
+++ b/src/Pure/term.ML Tue Feb 08 09:03:50 2011 -0800
@@ -990,15 +990,8 @@
fun string_of_vname (x, i) =
let
val idx = string_of_int i;
-val dot =
- (case rev (Symbol.explode x) of
-_ :: \\^isub :: _ = false
- | _ :: \\^isup :: _ = false
- | c :: _ = Symbol.is_digit c
- | _ = true);
in
-if dot then ? ^ x ^ . ^ idx
-else if i 0 then ? ^ x ^ idx
+if i 0 then ? ^ x ^ . ^ idx
else ? ^ x
end;
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Fwd: [isabelle] Problem with frule_tac substitution
On Tue, 8 Feb 2011, Brian Huffman wrote: The *_tac-style instantiation might be out of fashion, but the same parsing rules for indexnames are also used with the where attribute, which is still quite useful. In fact, the where attribute has its own embrace-and-extend version of Larry's standard of 25+ years, and I can't say on the spot what are the fine points of it. When inspecting these things some years ago, I added various comments like FIXME and cleanup this mess!!! here and there. Instead of peep-whole tuning of such old custums, I would rather like to see some conceptual advances. E.g. the user writes down rule statements in a certain format, and later is exposed to internal machine-representation of index names. How can this be addressed at a more conceptual level? How can printing of indexnames be avoided altogether? (Without low-level tweaking like show_question_marks.) Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Fwd: [isabelle] Problem with frule_tac substitution
I don't mind either way, but I'd like to point out that the _tac instantiations are everything but out of fashion. I'm fully aware that they are bad style, rely on dynamic names, etc, but there is no way around them if you write apply style. Cheers, Gerwin On 09/02/2011, at 3:58 AM, Brian Huffman wrote: The *_tac-style instantiation might be out of fashion, but the same parsing rules for indexnames are also used with the where attribute, which is still quite useful. - Brian On Tue, Feb 8, 2011 at 7:59 AM, Lawrence Paulson l...@cam.ac.uk wrote: Obviously this proposal would involve a significant incompatibility. It may not even be very relevant any more, as this sort of instantiation is rather out of fashion. But it is worth a discussion. Larry Begin forwarded message: I would propose to simplify the parsing rules to work like this: Any variable name with index 0 can be referred to without a question mark or dot, and a dot is always required for indices other than 0. x, ?x and ?x.0 parse as (x, 0) x0, ?x0 and ?x0.0 parse as (x0, 0) x2, ?x2 and ?x2.0 parse as (x2, 0) ?x.2 parses as (x, 2) ___ 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
