Re: [isabelle] Experimental tweaks to make HOL intuitionistic-by-default



First, thank you for comments!


The problem with elim declarations is that your rules (once exported from
> the locale) no longer have the necessary elim-form. You could declare them
> as such WITHIN the locale. They won’t work as you wish outside.

>From your explanation, I would have expected the following code to work:

context NonIntuitionistic begin
declare iffCE [elim!]
end

But I still see the same error on the declare line

exception THM 1 raised (line 332 of "drule.ML"):
RSN: no unifiers
?P = ?Q ⟹ (?P ⟹ ?Q ⟹ ?R) ⟹ (¬ ?P ⟹ ¬ ?Q ⟹ ?R) ⟹ ?R
PROP NonIntuitionistic ⟹ (¬ ?P ⟹ ?P) ⟹ ?P




I don’t think you can build all of HOL while separating out the classical
> part. It is just too huge, and there are too many things to change.


   1. I don't intend to change *all* of the theories that are a part
   Main.thy—in fact, for the time being I'm only interested in changing
   HOL.thy, Orderings.thy, Groups.thy, and Rings.thy.
   2. Even if only changing those few files is a huge effort, would it be
   okay to continue to ask questions on the mailing list when I run into
   problems? The way I see it, every stumbling block I come across might be an
   opportunity to learn more about Isabelle's implementation.

Again, thank you very much!

On Fri, Nov 21, 2014 at 7:27 PM, Lawrence Paulson <lp15 at cam.ac.uk> wrote:

> The problem with elim declarations is that your rules (once exported from
> the locale) no longer have the necessary elim-form. You could declare them
> as such WITHIN the locale. They won’t work as you wish outside.
>
> So overall, I don’t think you can build all of HOL while separating out
> the classical part. It is just too huge, and there are too many things to
> change.
>
> Larry Paulson
>
>
> > On 21 Nov 2014, at 22:09, Josh Tilles <merelyapseudonym at gmail.com>
> wrote:
> >
> >   - 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
> >
>
>



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