Re: [isabelle] Eisbach: HOL vs. Pure



You're correct, there is no deeper reason for residing in HOL other than giving it a default place to live.
The match method's dependence on HOL is also superficial and could be removed by using the proper Object_Logic interface where appropriate.
The use of numerals is a workaround for limitations in the method combinators, in order to pass information inside of a goal state. The proper fix here is to have a more rich type for methods (which has already been discussed), but the existing workaround could be adjusted to use more primitive operations (ultimately it just needs "int -> term" and "term -> int" regardless of the encoding).

These are all things that would disappear if/when Eisbach is integrated into Isar proper, rather than being a separate entity.


> On 29 Jun 2015, at 12:09 am, Lars Hupel <hupel at in.tum.de> wrote:
>
> Dear Makarius and Dan,
>
> what is the reason for Eisbach residing in HOL instead of Pure? As far
> as I can tell, the only dependency on HOL is for the "match" method,
> which treats "Trueprop" specially (makes sense to me), but appears to
> also deal with numerals (I don't understand the corresponding sources).
>
> Anyway, making an exact copy of "Eisbach.thy", removing the line
>
> ML_file "match_method.ML"
>
> ... and changing the import from "Main" to "Pure", it still works. I've
> made a tiny experiment with some "simp" and "rule" invocations and the
> method I defined behaves exactly as expected.
>
> Cheers
> Lars
>


________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.




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