[isabelle-dev] Fwd: [isabelle] Problem with frule_tac substitution

[Brian Huffman]

On Tue, Feb 8, 2011 at 9:01 AM, Lawrence Paulson <lp15 at 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.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;