[isabelle] simp fails on rewriting with "âx :: 'a. f x â a â f x = x"



Hi everyone,

today I stumbled upon some behaviour of simp I don't understand.
Consider the following simple theory

    theory Scratch imports Main begin

    consts P :: "bool"
    consts f :: "'a â 'a"

    notepad begin
      fix a  b :: 'a
      assume X: "âx :: 'a. f x â a â f x = x"
      have "f b â a â f b = b"
        apply (simp add: X)
        apply (subst X) apply simp_all
        done
        sorry
    end

Here, "simp add: X" fails, even though all its premises can be solved by
"assumption" -- or, as the second line shows, by "simp". Has anyone got
an idea why this is the case?

Looking at the the simp trace, one seees that the simplifier tries
recursively to rewrite the premis "f x ~= a". This fails ultimately. But
I would have expected it trying to solve the premis by assumption, then.

  -- Lars 'simp is not simple' Noschinski



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