Re: [isabelle] Eisbach: HOL vs. Pure



I agree that it would be right for Eisbach to be installed generically, and available to all object-logics. Everything is Isabelle/HOL these days, but you never know when Isabelle/ZF might get a small revival. The original idea of Isabelle is that everything is available everywhere as much as possible.

Larry Paulson


> On 29 Jun 2015, at 04:45, Daniel Matichuk <daniel.matichuk at nicta.com.au> wrote:
> 
> 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.