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 <[email protected]> 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.ML Tue Feb 08 16:10:10 2011 +0100 > +++ b/src/Pure/Syntax/lexicon.ML Tue 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 [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
