Quelle  Pattern_Aliases.thy

(*  Title:      HOL/Library/Pattern_Aliases.thy
  Author: Lars Hupel, Ondrej Kuncar, Tobias Nipkow
*)

section ‹Input syntax for pattern aliases (or ``as-patterns'' in Haskell)›

theory Pattern_Aliases
imports Main
begin

text ‹
  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). All features are packed into a @{command bundle}.
 
  The following caveats should be kept in mind:
  🪙 The translation expects a term of the form 🍋‹f x y = rhs›, where ‹x› and ‹y› are patterns
  that may contain aliases. The result of the translation is a nested 🍋‹Let›-expression on
  the right hand side. The code generator 🪙‹does not› print Isabelle pattern aliases to target
  language pattern aliases.
  🪙 The translation does not process nested equalities; only the top-level equality is translated.
  🪙 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.
  🪙 The corresponding uncheck phase attempts to reverse the translation (no guarantee). The
  additionally introduced variables are bound using a ``fake quantifier'' that does not
  appear in the output.
  🪙 To obtain reasonable induction principles in function definitions, the bundle also declares
  a custom congruence rule for 🍋‹Let› that only affects @{command fun}. This congruence
  rule might lead to an explosion in term size (although that is rare)! In some circumstances
  (using ‹let› to destructure tuples), the internal construction of functions stumbles over this
  rule and prints an error. To mitigate this, either
  🪙 activate the bundle locally (🪙‹context includes ... begin›) or
  🪙 rewrite the ‹let›-expression to use ‹case›: 🍋‹let (a, b) = x in (b, a)› becomes
  🍋‹case x of (a, b) ==> (b, a)›.
  🪙 The bundle also adds the @{thm Let_def} rule to the simpset.
 ›


subsection ‹Definition›

consts
  as :: "'a ==> 'a ==> 'a"
  fake_quant :: "('a ==> prop) ==> prop"

lemma let_cong_unfolding: "M = N ==> f N = g N ==> Let M f = Let N g"
by simp

translations "P" <= "CONST fake_quant (λx. P)"

ML‹
 local
 
 fun let_typ a b = a --> (a --> b) --> b
 fun as_typ a = a --> a --> a
 
 fun strip_all t =
  case try Logic.dest_all_global 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 []
 
 fun subst_once (old, new) t =
  let
  fun go t =
  if t = old then
  (new, true)
  else
  case t of
  u $ v =>
  let
  val (u', substituted) = go u
  in
  if substituted then
  (u' $ v, true)
  else
  case go v of (v', substituted) => (u $ v', substituted)
  end
  | Abs (name, typ, t) =>
  (case go t of (t', substituted) => (Abs (name, typ, t'), substituted))
  | _ => (t, false)
  in fst (go t) end
 
(* adapted from logic.ML *)
fun fake_const T = Const (🍋‹fake_quant›, (T --> propT) --> propT);

fun dependent_fake_name v t =
  let
    val x = Term.term_name v
    val T = Term.fastype_of v
    val t' = Term.abstract_over (v, t)
  in if Term.is_dependent t' then fake_const T $ Abs (x, T, t') else t end

in

fun check_pattern_syntax t =
  case strip_all t of
    (vars, 🍋‹Trueprop› $ (Const (🍋‹HOL.eq›, _) $ lhs $ rhs)) =>
      let
        fun go (Const (🍋‹as›, _) $ pat $ var, rhs) =
              let
                val (pat', rhs') = go (pat, rhs)
                val _ = if is_Free var then () else error "Right-hand side of =: must be a free variable"
                val rhs'' =
                  Const (🍋‹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

fun uncheck_pattern_syntax ctxt t =
  case strip_all t of
    (vars, 🍋‹Trueprop› $ (Const (🍋‹HOL.eq›, _) $ lhs $ rhs)) =>
      let
        (* restricted to going down abstractions; ignores eta-contracted rhs *)
        fun go lhs (rhs as Const (🍋‹Let›, _) $ pat $ Abs (name, typ, t)) ctxt frees =
              if exists_subterm (fn t' => t' = pat) lhs then
                let
                  val ([name'], ctxt') = Variable.variant_fixes [name] ctxt
                  val free = Free (name', typ)
                  val subst = (pat, Const (🍋‹as›, as_typ typ) $ pat $ free)
                  val lhs' = subst_once subst lhs
                  val rhs' = subst_bound (free, t)
                in
                  go lhs' rhs' ctxt' (Free (name', typ) :: frees)
                end
              else
                (lhs, rhs, ctxt, frees)
          | go lhs rhs ctxt frees = (lhs, rhs, ctxt, frees)

        val (lhs', rhs', _, frees) = go lhs rhs ctxt []

        val res =
          HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs', rhs'))
          |> fold (fn v => Logic.dependent_all_name ("", v)) (map Free vars)
          |> fold dependent_fake_name frees
      in
        if null frees then t else res
      end
  | _ => t

end
›

bundle pattern_aliases begin

  notation as (infixr ‹=:› 1)

  declaration ‹K (Syntax_Phases.term_check 98 "pattern_syntax" (K (map check_pattern_syntax)))›
  declaration ‹K (Syntax_Phases.term_uncheck 98 "pattern_syntax" (map o uncheck_pattern_syntax))›

  declare let_cong_unfolding [fundef_cong]
  declare Let_def [simp]

end

hide_const as
hide_const fake_quant


subsection ‹Usage›

context includes pattern_aliases begin

text ‹Not very useful for plain definitions, but works anyway.›

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 ‹Very useful for function definitions.›

private fun test_2 where
"test_2 (y # (y' # ys =: x') =: x) = x @ x' @ x'" |
"test_2 _ = []"

lemma "test_2 (y # y' # ys) = (y # y' # ys) @ (y' # ys) @ (y' # ys)"
by (rule test_2.simps[unfolded Let_def])

ML‹
 let
  val actual =
  @{thm test_2.simps(1)}
  |> Thm.prop_of
  |> Syntax.pretty_term 🍋
  |> Pretty.pure_string_of
  val expected = "test_2 (?y # (?y' # ?ys =: x') =: x) = x @ x' @ x'"
 in 🍋 (actual = expected) end
 ›

end

end