[isabelle-dev] Isabelle/HOL axiom ext is redundant[SEC=UNCLASSIFIED]
Dr. Brendan Patrick Mahony
brendan.mahony at dsto.defence.gov.au
Mon Nov 16 02:21:05 CET 2009
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
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.
More information about the isabelle-dev