There are a great many examples of theorems involving various coercion functions and the relations =, <, <=. In a number of cases, the “real” versions were declared as [iff]-rules, while the “of_nat/of_int” versions were declared as [simp]-rules only. When identifying the two, I decided it would make sense to go for iff, for maximum automation, but I now think this was a mistake. I’m trying the alternative right now.
Larry > On 12 Nov 2015, at 13:30, Tobias Nipkow <nip...@in.tum.de> wrote: > > I am not surprised at all that the simplifier behaves differently because the > simpset is modified all the time and is full of theorems wih coercions. But > blast is another matter. Concrete questions: > > - Are there any coercion-related permanent intro/dest/elim theorems (either > before or now)? > > - Could they kick in during a proof concerned only with basic set theory and > first order logic? > > I want to make sure that it is not something else that caused blast to break. > > Tobias > _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
