Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] pat_completeness exception

view this post on Zulip Email Gateway (Nov 03 2020 at 12:50):

From: Tobias Nipkow <>
Dear pat_completeness experts,

pat_completeness does not seem to like ~=, eg

lemma exception: "(⋀x y. x ≠ y ⟹ P True) ⟹ P t"

exception TERM raised (line 271 of "~~/src/HOL/Tools/hologic.ML")

This came up in trying to prove (via induction_schema) an induction schema with
two subcases, one with x = y and the other with x ~= y.

Probably pat_completness was not designed to handle this.


Last updated: Dec 08 2021 at 08:24 UTC