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



One other thing: when you refer to "the necessary elim-form", I'm not
exactly sure what you mean. (Like, how could I determine what the necessary
elim-form is?) Would you be able to elaborate, or perhaps point me toward
some relevant documentation?

Thanks,
--Josh

P.S. I'm about a hundred pages into *ML for the Working Programmer*, so I
apologize if all of my questions are just a result of my not yet having
read the chapter about constructing a tactical theorem prover [?]

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

GIF image



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