[isabelle-dev] Isabelle/HOL axiom ext is redundant[SEC=UNCLASSIFIED]

[Dr. Brendan Patrick Mahony]

Thanks for this interesting and enlightening discussion.

I have always had an intuitive appreciation of the meta-logic in  
Isabelle. I find it clarifies the both the modeling and proof  
activities profoundly.

I would be interested also in a discussion of an important place where  
the meta-logic is not distinguished from the object logic in Isabelle/ 
HOL, i.e. in the function model. HOL functions are completely  
identified with meta-functions (I like to call them operators) and  
there is no explicit function application operator. This makes for  
lots of inconvenience in making proofs about HOL functions, especially  
in the vagaries higher-order unification.

Any insights in why HOL-application is not as worthy of distinction  
from meta-application as = is from ==? Especially as meta-application  
itself is so subtly identified with term construction?

On 13/11/2009, at 5:36 AM, Brian Huffman wrote:

> Right, having two kinds of implication (--> and ==>) is convenient
> because (==>) is used to encode subgoals with premises in apply-style
> Isabelle proofs.


IMPORTANT: This email remains the property of the Australian Defence Organisation and is subject to the jurisdiction of section 70 of the CRIMES ACT 1914.  If you have received this email in error, you are requested to contact the sender and delete the email.