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

[Lawrence Paulson]

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 <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;