Re: [isabelle] Failing simproc

On 20.07.2012 15:06, Brian Huffman wrote:
This exception is thrown by the simproc natless_cancel_sums (in
Nat_Arith.nat_cancel_sums), as the following succeeds:

   ML_prf {* Delsimprocs [nth Nat_Arith.nat_cancel_sums 1] *}
   have "(\<And>ys zs. length ys<  Suc (length zs + length ys))" by simp
   hence True
     by simp

The other simprocs in Nat_Arith also seem to be affected.

For the record: This problem was caused by an interaction between
simprocs and schematic type variables. More specifically, some
internal proofs done by Nat_Arith simprocs would fail on terms that
contain schematics. The problem is now fixed in revision 868dc809c8a2.

Authors of simprocs should take note: The simplifier may run simprocs
on terms containing schematics (type and/or term variables) and it is
the responsibility of the simproc to handle this situation properly.

There are also other simprocs, which produce equations, which are ignored by the simplifier. I haven't checked closely yet, but these are most likely due to instantiations of schematic variables:

$ zgrep 'IGNORED result of simproc' * | cut -d\" -f2 | sort | uniq -c
     45 Cfun.beta_cfun_proc
     86 equal
      2 Numeral_Simprocs.inteq_cancel_numerals
    941 perm_simproc_fun
  24814 record_eq_simp

(src/HOL make all)

A simproc must never instantiate any schematic variable. Some
guidelines for simproc writers: Internal proofs should use the
simplifier only in "safe" mode, i.e. only using the "safe" solvers,
which avoid instantiating schematics. Also, avoid instantiating rules
with terms from the input and then using those rules with rtac,
because schematic variables in a rule are not preserved when the rule
is applied. (The Nat_Arith simprocs failed to follow either of these

So you decided against the generic approach of importing the schematic variables? Was it because of efficiency?

  -- Lars

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.