Re: [isabelle] Failing simproc



On 20.07.2012 17:51, Florian Haftmann wrote:
$ zgrep 'IGNORED result of simproc' * | cut -d\" -f2 | sort | uniq -c
      86 equal

Ok, these numbers are flawed. Despite the wording of the warning message

  "IGNORED result of simproc " ^ quote name ^ " -- does not match"

the warning message is printed not only for non-matching equalities but also for anything which can not successfully be used for rewriting. This explains the big number for record_eq_simp (which generates conditional rules).

I'm wondering a little bit about this.  The simproc »equal« is part of
the code generatorm, preprocessor, as follows:

setup {*
   Code_Preproc.map_pre (fn simpset =>
     simpset addsimprocs [Simplifier.simproc_global_i @{theory} "equal"
[ at {term HOL.eq}]
       (fn thy =>  fn _ =>
         fn Const (_, Type ("fun", [Type _, _])) =>  SOME @{thm eq_equal}
| _ =>  NONE)])
*}

Are there situations where this rewrite step is expected to fail (maybe due to sort constraints)? Then this warning would be expected, too.

  -- Lars





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