[isabelledev] Fwd: [isabelle] Problem with frule_tac substitution
Brian Huffman
brianh at cs.pdx.edu
Tue Feb 8 18:19:52 CET 2011
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 HOLMain 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 openbraceclosebrace 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;
More information about the isabelledev
mailing list