[isabelle-dev] Fwd: [isabelle] Problem with frule_tac substitution
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
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] doc test failed
On Tue, 8 Feb 2011, Makarius wrote: ### No timeout support on this ML platform This is a known (documented) feature of polyml-5.2, which is used in this test. To avoid further confusion in the future, I will discontinue this old Poly/ML version altogether and dispose the dummy versions of multithreading and timeouts. See also 05514b09bb4b and ae1a46cdb9cb. There is some change that isatest will swallow this. Another important question is why isatest did not report the failure of the important at-poly session This is still open. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] interrupts and timeouts
In the past few months/weeks/days certain issues of interrupts and timeouts (which are based on interrupts internally) have emerged in private mail conversations with several people. Recently David Matthews has kindly clarified some extreme corner cases, so I've made another round to robustify this on our side, e.g. see the vicinity of 82339c3fd74a. There are still some pending questions concerning interactive auto checking tools, though. I've first thought that this could be related, but the reasons might be much more profane. (The above-mentioned corner cases of Poly/ML interrupts are so extreme, that they might not have shown up in practice so far.) 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 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
Re: [isabelle-dev] [Fwd: doc test failed]
On 09/02/2011, at 1:50 AM, Makarius wrote: On Tue, 8 Feb 2011, Gerwin Klein wrote: The test should build all images, but it is possible that the doc test is started before the rest of the test gets there. Explicitly building ZF when processing doc-src should make that work. I'm about to push that change. We will see if that helps.. That's now eb5900951702, but it merely treats the symptoms by changing my traditional document setup in an adhoc fashion (and giving a misleading explanation in the log entry). Not really. Isar-Ref was the non-traditional one. All other documentation parts did exactly what Isar-Ref does now, which is what we do in all other Makefiles that refer to a logic image (and which is why the other ones worked). You're right that it does only treat the symptom, though. ### No timeout support on this ML platform This is a known (documented) feature of polyml-5.2, which is used in this test. To avoid further confusion in the future, I will discontinue this old Poly/ML version altogether and dispose the dummy versions of multithreading and timeouts. (Tests with real time parameters remain inherently erratic, of course.) Yes, that's a good idea. Another important question is why isatest did not report the failure of the important at-poly session, which is one of the core tests in some sense. That is indeed strange. I'll see if I can track it down. Cheers, Gerwin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [isabelle] Problem with frule_tac substitution
On Tue, 2011-02-08 at 06:53 -0800, Brian Huffman wrote: Honestly, I think the above parsing rules are quite confusing, and should be changed. I instantiate variables in theorems quite often, and many theorems use variable names that end in digits, but I almost never need to refer to variables with indices other than 0. For what it's worth, I agree with Brian here. I remember that this was one of the minor hurdles when I first encountered Isabelle -- the kind of technicality that can take a new user anywhere from 5 minutes to \infty to figure out. Changing the current behavior in my humble opinion would be an improvement. Kind regards, Tjark ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [isabelle] Problem with frule_tac substitution
Having to instantiate an indexed ?-variable can require a bit of experimentation if you don't remember the exact syntax. I am all for an improvement here, and as Gerwin pointed out, one of our flagship projects is using apply's heavily, where it probably comes up more frequently than otherwise. Tobias Tjark Weber schrieb: On Tue, 2011-02-08 at 06:53 -0800, Brian Huffman wrote: Honestly, I think the above parsing rules are quite confusing, and should be changed. I instantiate variables in theorems quite often, and many theorems use variable names that end in digits, but I almost never need to refer to variables with indices other than 0. For what it's worth, I agree with Brian here. I remember that this was one of the minor hurdles when I first encountered Isabelle -- the kind of technicality that can take a new user anywhere from 5 minutes to \infty to figure out. Changing the current behavior in my humble opinion would be an improvement. Kind regards, Tjark ___ 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
