[isabelle-dev] Isabelle/HOL axiom ext is redundant
lp15 at cam.ac.uk
Thu Nov 12 10:29:04 CET 2009
The situation regarding these inference rules is quite different.
Isabelle is primarily based on resolution, which is a big, complicated
piece of code implementing what is supposed to be a sound form of
reasoning in intuitionistic Higher-order logic. However, it claims to
be based on that logic and therefore I included the corresponding
presentation in the form of LCF-style inference rules. They were
almost never used, and very annoyingly, somebody once identified a bug
in one that could break the type system!
It was obvious to me from the start that there were some redundancy
between the built-in resolution code and these rules, but I never saw
this issue as a priority.
On 11 Nov 2009, at 23:22, Brian Huffman wrote:
> (Actually, it is slightly more complicated than that, since there is a
> primitive inference rule Thm.equal_intr that makes (==) at type prop
> the same as bi-implication. I don't really see why equal_intr needs to
> exist at all; maybe just to make simplification easier? Oh, well.)
More information about the isabelle-dev