[isabelle] Experimental tweaks to make HOL intuitionistic-by-default
I've come across a few errors that are blocking my progress. I'm not sure
what to do besides trying to become familiar with *all* of Isabelle's
internals, so I'd appreciate any advice/direction—particularly on the two
specific errors I present below.
These errors have arisen because I've returned to a task that I last
attempted a year or so ago: adapting HOL to make it possible to selectively
"opt-in" to classical logic. I've thought of a few approaches that would
work as initial proof-of-concepts. My intuition is that any of the below
*should* be possible, but one might be more tractable than the others.
Extract HOL.True_or_False into a locale.
- seems like the ideal solution
- Ultimately, I think the locale *should* be named classical *but* I've
currently named it NonIntuitionistic because there's a lemma that's also
named classical and an ML structure named Classical. So if I wanted the
locale usage to stand out in these prototypes, I needed a different name.
- The problem is that the elim rules break:
- on the line "declare NonIntuitionistic.iffCE [elim!]" we see the
exception THM 1 raised (line 332 of "drule.ML"):
RSN: no unifiers
PROP NonIntuitionistic ⟹ ?P = ?Q ⟹ (?P ⟹ ?Q ⟹ ?R) ⟹ (¬ ?P ⟹ ¬ ?Q ⟹
?R) ⟹ ?R
PROP NonIntuitionistic ⟹ (¬ ?P ⟹ ?P) ⟹ ?P
Extract non-classical code into IHOL.thy, which the normal/classical HOL.thy
- Took a lot of time the last time I tried it a year ago, so I don't
have a demonstration patch (yet)
- A major problem is that all future theories will need to be split
- For example, IOrderings.thy for all of the lemmas and theorems that
work in an intuitionistic context, and Orderings.thy as the theory
that contains everything in IOrderings.thy *plus* any lemmas/theories
that actually depend on classical logic.
Replace the global HOL.True_or_False axiomatization with many local
assumptions/dependencies on the individual lemmas and theorems.
- probably the least amount of broad structural change (effectively,
we're just adding one more assumption to any classical lemmas)
- but tedious to make lots of minor changes to make to the proofs of the
- you can see examples of this in my attached patch
- I totally acknowledge that my updated proofs are super-hacky at the
- needed to move the declarations of a bunch of lemmas as elimination
rules *before* the Hypsubst and Classical structures, otherwise I get an
- on the line "declare iffCE [elim!]" we see the message:
exception Option raised (line 81 of "General/basics.ML")
- but if those particular errors go away if I relocate the
- unfortunately, anything elim-related fails with the same error
This archive was generated by a fusion of
Pipermail (Mailman edition) and