[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.

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



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.