syntax for pattern aliases

--- a/NEWS	Thu Aug 17 22:29:30 2017 +0200
+++ b/NEWS	Fri Aug 18 14:57:23 2017 +0200
@@ -121,6 +121,9 @@
 
 *** HOL ***
 
+* Theory Library/Pattern_Aliases provides input syntax for pattern
+aliases as known from Haskell, Scala and ML.
+
 * Constant "subseq" in Topological_Spaces removed and subsumed by
 "strict_mono". Some basic lemmas specific to "subseq" have been renamed
 accordingly, e.g. "subseq_o" -> "strict_mono_o" etc.

--- a/src/HOL/Library/Library.thy	Thu Aug 17 22:29:30 2017 +0200
+++ b/src/HOL/Library/Library.thy	Fri Aug 18 14:57:23 2017 +0200
@@ -52,6 +52,7 @@
   Option_ord
   Order_Continuity
   Parallel
+  Pattern_Aliases
   Periodic_Fun
   Perm
   Permutation
@@ -82,4 +83,4 @@
   While_Combinator
 begin
 end
-(*>*)
\ No newline at end of file
+(*>*)

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Pattern_Aliases.thy	Fri Aug 18 14:57:23 2017 +0200
@@ -0,0 +1,114 @@
+(*  Title:      HOL/Library/Pattern_Aliases.thy
+    Author:     Lars Hupel, Ondrej Kuncar
+*)
+
+section \<open>Input syntax for pattern aliases (or ``as-patterns'' in Haskell)\<close>
+
+theory Pattern_Aliases
+imports Main
+begin
+
+text \<open>
+  Most functional languages (Haskell, ML, Scala) support aliases in patterns. This allows to refer
+  to a subpattern with a variable name. This theory implements this using a check phase. It works
+  well for function definitions (see usage below).
+
+  The following caveats should be kept in mind:
+  \<^item> The translation expects a term of the form @{prop "f x y = rhs"}, where \<open>x\<close> and \<open>y\<close> are patterns
+    that may contain aliases. The result of the translation is a nested @{const Let}-expression on
+    the right hand side. The code generator \<^emph>\<open>does not\<close> print Isabelle pattern aliases to target
+    language pattern aliases.
+  \<^item> The translation does not process nested equalities; only the top-level equality is translated.
+  \<^item> Terms that do not adhere to the above shape may either stay untranslated or produce an error
+    message. The @{command fun} command will complain if pattern aliases are left untranslated.
+    In particular, there are no checks whether the patterns are wellformed or linear.
+  \<^item> There is no corresonding uncheck phase, because it is unclear in which situations the
+    translation should be reversed.
+\<close>
+
+
+subsection \<open>Definition\<close>
+
+consts as :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
+
+ML\<open>
+local
+
+fun let_typ a b = a --> (a --> b) --> b
+
+fun strip_all t =
+  case try Logic.dest_all t of
+    NONE => ([], t)
+  | SOME (var, t) => apfst (cons var) (strip_all t)
+
+fun all_Frees t =
+  fold_aterms (fn Free (x, t) => insert op = (x, t) | _ => I) t []
+
+in
+
+fun check_pattern_syntax t =
+  case strip_all t of
+    (vars, @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ lhs $ rhs)) =>
+      let
+        fun go (Const (@{const_name as}, _) $ pat $ var, rhs) =
+              let
+                val (pat', rhs') = go (pat, rhs)
+                val _ = if is_Free var then () else error "Left-hand side of =: must be a free variable"
+                val rhs'' =
+                  Const (@{const_name Let}, let_typ (fastype_of var) (fastype_of rhs)) $
+                    pat' $ lambda var rhs'
+              in
+                (pat', rhs'')
+              end
+          | go (t $ u, rhs) =
+              let
+                val (t', rhs') = go (t, rhs)
+                val (u', rhs'') = go (u, rhs')
+              in (t' $ u', rhs'') end
+          | go (t, rhs) = (t, rhs)
+
+        val (lhs', rhs') = go (lhs, rhs)
+
+        val res = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs', rhs'))
+
+        val frees = filter (member op = vars) (all_Frees res)
+      in fold (fn v => Logic.dependent_all_name ("", v)) (map Free frees) res end
+  | _ => t
+
+end
+\<close>
+
+bundle pattern_aliases begin
+
+  notation as (infixr "=:" 1)
+
+  declaration \<open>K (Syntax_Phases.term_check 98 "pattern_syntax" (K (map check_pattern_syntax)))\<close>
+
+end
+
+hide_const (open) as
+
+
+subsection \<open>Usage\<close>
+
+context includes pattern_aliases begin
+
+text \<open>Not very useful for plain definitions, but works anyway.\<close>
+
+private definition "test_1 x (y =: z) = y + z"
+
+lemma "test_1 x y = y + y"
+by (rule test_1_def[unfolded Let_def])
+
+text \<open>Very useful for function definitions.\<close>
+
+private fun test_2 where
+"test_2 (y # (y' # ys =: x') =: x) = x @ x'" |
+"test_2 _ = []"
+
+lemma "test_2 (y # y' # ys) = (y # y' # ys) @ y' # ys"
+by (rule test_2.simps[unfolded Let_def])
+
+end
+
+end
\ No newline at end of file