(* Title: HOL/Library/Pattern_Aliases.thy Author: Lars Hupel, Ondrej Kuncar, Tobias Nipkow
*)
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 forfunction definitions (see usage below). All features are packed into a @{command bundle}.
The following caveats should be kept in mind: \<^item> The translation expects a term of the form \<^prop>\<open>f x y = rhs\<close>, where \<open>x\<close> and \<open>y\<close> are patterns
that may contain aliases. The result of the translation is a nested \<^const>\<open>Let\<close>-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> 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. \<^item> To obtain reasonable induction principles in function definitions, the bundle also declares
a custom congruence rule for\<^const>\<open>Let\<close> that only affects @{command fun}. This congruence
rule might lead to an explosion interm size (although that is rare)! In some circumstances
(using\<open>let\<close> to destructure tuples), the internal construction of functions stumbles over this
rule and prints an error. To mitigate this, either \<^item> activate the bundle locally (\<^theory_text>\<open>context includes ... begin\<close>) or \<^item> rewrite the \<open>let\<close>-expression to use \<open>case\<close>: \<^term>\<open>let (a, b) = x in (b, a)\<close> becomes \<^term>\<open>case x of (a, b) \<Rightarrow> (b, a)\<close>. \<^item> The bundle also adds the @{thm Let_def} rule to the simpset. \<close>
subsection \<open>Definition\<close>
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\<open> 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 (\<^const_name>\<open>fake_quant\<close>, (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) inifTerm.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>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ lhs $ rhs)) => let fun go (Const (\<^const_name>\<open>as\<close>, _) $ 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>\<open>Let\<close>, 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>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ lhs $ rhs)) => let (* restricted to going down abstractions; ignores eta-contracted rhs *) fun go lhs (rhs as Const (\<^const_name>\<open>Let\<close>, _) $ 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>\<open>as\<close>, 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
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
