[isabelle] syntax for lifted / point-free operations


Is anyone interested in a common syntax for point-free operations? By this I mean, for example:

abbreviation (input)
  pred_conj :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" (infixr "\<^bold>\<and>" 35) where
  "a \<^bold>\<and> b \<equiv> \<lambda>s. a s \<and> b s"

i.e., working in the reader monad.

Makarius suggested using \<^bold>. See the attached for the operations Iâve used thus far.

Iâm not so ambitious as to attempt to make list and set comprehensions work, etc.

If there is such interest, and this is a reasonable starting point, can someone add this file to HOL/Library? There are similar operations already defined in Linear_Temporal_Logic_on_Streams, btw.

One limitation is that \<^bold> does not work so well for multi-character tokens, such as:

abbreviation (input)
  pred_If :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" ("(\<^bold>if (_)/ \<^bold>then (_)/ \<^bold>else (_))" [0, 0, 10] 10) where
  â\<^bold>if P \<^bold>then x \<^bold>else y \<equiv> \<lambda>s. if P s then x s else y sâ


Attachment: PointFree.thy
Description: Binary data


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