[isabelle-dev] HOL iff notation

[Makarius]

On Mon, 2 Sep 2013, Makarius wrote:

> I find myself using the "iff" notation most of the time to make theories 
> look "nice".
>
> Are there clubs of "iff" vs. "non-iff"?  If almost everybody is a member of 
> the "iff" club we could just remove that print mode.

I've forgotten to point out the relationship to this isabelle-users 
thread about "Isabelle operator precedence":
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2012-November/msg00020.html

Part of it was some confusion about "infixl" vs. "infix" of HOL eq and 
not_equal, which was coming from a bit too many variants being there, and 
some of them not quite right (it is probably right at 
Isabelle/b46e6cd75dc6).


Back then I wrote:

   I think the "=" notation is going back to a time even before the
   'infixl' / 'infixr' macros for the general mixfix form, and there were also some
   special tweaks for output and breaks unlike regular infixes. 'infix' is
   much younger than all that.

   In the last 10 years, there have been some slight reforms towards more
   regularity of notation for eq/not_equal in HOL. It might be worth trying
   again to make it all just plain infix 50, although just from the
   ancienticity of it it could cause some surprises in some dark corners.

Trying the latter, i.e. using just plain infix 50 for = and its negated 
version, reveals problems rather early.  For example in Set.thy:

   lemma subset_eq [no_atp]: "A ≤ B = (∀x∈A. x ∈ B)" by blast

So any of the infixes with priority 50 will cause problems that do not 
exist with the iff notation, since that has weaker priority.  The latter 
also allows to remove many parentheses.

The above example also has ≤ instead of ⊆ for sets, which is somehow 
related.  (Continuing that train of thought will inevitably expose cans of 
worms, so this speculative thread is definitely not relevant for the 
coming release.)


 	Makarius