*To*: isabelle-users <isabelle-users at cl.cam.ac.uk>*Subject*: [isabelle] Experimental tweaks to make HOL intuitionistic-by-default*From*: Josh Tilles <merelyapseudonym at gmail.com>*Date*: Fri, 21 Nov 2014 17:09:05 -0500

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. Thank you, --Josh Tilles 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 message: 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 subsequently imports. - 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 similarly - 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 lemmas - you can see examples of this in my attached patch - I totally acknowledge that my updated proofs are super-hacky at the moment. - needed to move the declarations of a bunch of lemmas as elimination rules *before* the Hypsubst and Classical structures, otherwise I get an error: - 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 declarations - unfortunately, anything elim-related fails with the same error

**Follow-Ups**:**Re: [isabelle] Experimental tweaks to make HOL intuitionistic-by-default***From:*Josh Tilles

**Re: [isabelle] Experimental tweaks to make HOL intuitionistic-by-default***From:*Lawrence Paulson

- Previous by Date: Re: [isabelle] sledgehammer, smt and metis
- Next by Date: Re: [isabelle] Experimental tweaks to make HOL intuitionistic-by-default
- Previous by Thread: Re: [isabelle] Problems with nitpick
- Next by Thread: Re: [isabelle] Experimental tweaks to make HOL intuitionistic-by-default
- Cl-isabelle-users November 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list