Re: [isabelle] A constant become a free variable



On Wed, 4 Dec 2013, Yannick Duchêne (Hibou57) wrote:

Le Wed, 04 Dec 2013 16:00:56 +0100, Makarius <makarius at sketis.net> a écrit:

On Wed, 4 Dec 2013, Yannick wrote:

I've just checked, and “HOL.thy” indeed says “(*admissible axiom*)”.
Will try to learn to do without it.

In some sense this belongs to the "implementation" of Isabelle/HOL on top
of the Isabelle/Pure framework.

These days you should hardly ever need == in Isabelle/HOL applications.

Does that mean substitution/simplification is not expressed with “==” but “=” instead ? I always though “==” was the standard for that purpose with logic.

The basic substitution rules of Isabelle/HOL directly refer to =, not ==. This is also relevant to calculational reasoning, e.g. see print_trans_rules. (That gives only very limited support for some basic Pure reasoning with ==).

Some other tools go to the bottom of Pure and use == internally, such as the Simplifier itself (which is somewhat independent of the object-logic). This is also one of several points in the system where both = and == are allowed in user input, but this duplication of interfaces is not universal.

That was important in the past, because the primite 'defs' command was used routinely in user theories, and thus there was considerable mix-up of connectives. For many years already, the 'definition' command allows to use = of Isabelle/HOL, just like other specification elements that are proper to HOL.


	Makarius


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