Theory HOL-Library.Pattern_Aliases
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 \<^prop>‹f x y = rhs›, where ‹x› and ‹y› 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 ∗‹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 \<^const>‹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›: \<^term>‹let (a, b) = x in (b, a)› becomes
\<^term>‹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
fun fake_const T = Const (\<^const_name>‹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, \<^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 "Right-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
fun uncheck_pattern_syntax ctxt t =
case strip_all t of
(vars, \<^Const>‹Trueprop› $ (Const (\<^const_name>‹HOL.eq›, _) $ lhs $ rhs)) =>
let
fun go lhs (rhs as Const (\<^const_name>‹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 (\<^const_name>‹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 \<^context>
|> Pretty.pure_string_of
val expected = "test_2 (?y # (?y' # ?ys =: x') =: x) = x @ x' @ x'"
in \<^assert> (actual = expected) end
›
end
end