src/HOL/Library/Pattern_Aliases.thy
author haftmann
Fri Mar 22 19:18:08 2019 +0000 (3 months ago)
changeset 69946 494934c30f38
parent 69597 ff784d5a5bfb
permissions -rw-r--r--
improved code equations taken over from AFP
     1 (*  Title:      HOL/Library/Pattern_Aliases.thy
     2     Author:     Lars Hupel, Ondrej Kuncar, Tobias Nipkow
     3 *)
     4 
     5 section \<open>Input syntax for pattern aliases (or ``as-patterns'' in Haskell)\<close>
     6 
     7 theory Pattern_Aliases
     8 imports Main
     9 begin
    10 
    11 text \<open>
    12   Most functional languages (Haskell, ML, Scala) support aliases in patterns. This allows to refer
    13   to a subpattern with a variable name. This theory implements this using a check phase. It works
    14   well for function definitions (see usage below). All features are packed into a @{command bundle}.
    15 
    16   The following caveats should be kept in mind:
    17   \<^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
    18     that may contain aliases. The result of the translation is a nested \<^const>\<open>Let\<close>-expression on
    19     the right hand side. The code generator \<^emph>\<open>does not\<close> print Isabelle pattern aliases to target
    20     language pattern aliases.
    21   \<^item> The translation does not process nested equalities; only the top-level equality is translated.
    22   \<^item> Terms that do not adhere to the above shape may either stay untranslated or produce an error
    23     message. The @{command fun} command will complain if pattern aliases are left untranslated.
    24     In particular, there are no checks whether the patterns are wellformed or linear.
    25   \<^item> The corresponding uncheck phase attempts to reverse the translation (no guarantee). The
    26     additionally introduced variables are bound using a ``fake quantifier'' that does not
    27     appear in the output.
    28   \<^item> To obtain reasonable induction principles in function definitions, the bundle also declares
    29     a custom congruence rule for \<^const>\<open>Let\<close> that only affects @{command fun}. This congruence
    30     rule might lead to an explosion in term size (although that is rare)! In some circumstances
    31     (using \<open>let\<close> to destructure tuples), the internal construction of functions stumbles over this
    32     rule and prints an error. To mitigate this, either
    33     \<^item> activate the bundle locally (\<^theory_text>\<open>context includes ... begin\<close>) or
    34     \<^item> rewrite the \<open>let\<close>-expression to use \<open>case\<close>: \<^term>\<open>let (a, b) = x in (b, a)\<close> becomes
    35       \<^term>\<open>case x of (a, b) \<Rightarrow> (b, a)\<close>.
    36   \<^item> The bundle also adds the @{thm Let_def} rule to the simpset.
    37 \<close>
    38 
    39 
    40 subsection \<open>Definition\<close>
    41 
    42 consts
    43   as :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
    44   fake_quant :: "('a \<Rightarrow> prop) \<Rightarrow> prop"
    45 
    46 lemma let_cong_unfolding: "M = N \<Longrightarrow> f N = g N \<Longrightarrow> Let M f = Let N g"
    47 by simp
    48 
    49 translations "P" <= "CONST fake_quant (\<lambda>x. P)"
    50 
    51 ML\<open>
    52 local
    53 
    54 fun let_typ a b = a --> (a --> b) --> b
    55 fun as_typ a = a --> a --> a
    56 
    57 fun strip_all t =
    58   case try Logic.dest_all t of
    59     NONE => ([], t)
    60   | SOME (var, t) => apfst (cons var) (strip_all t)
    61 
    62 fun all_Frees t =
    63   fold_aterms (fn Free (x, t) => insert (op =) (x, t) | _ => I) t []
    64 
    65 fun subst_once (old, new) t =
    66   let
    67     fun go t =
    68       if t = old then
    69         (new, true)
    70       else
    71         case t of
    72           u $ v =>
    73             let
    74               val (u', substituted) = go u
    75             in
    76               if substituted then
    77                 (u' $ v, true)
    78               else
    79                 case go v of (v', substituted) => (u $ v', substituted)
    80             end
    81         | Abs (name, typ, t) =>
    82             (case go t of (t', substituted) => (Abs (name, typ, t'), substituted))
    83         | _ => (t, false)
    84   in fst (go t) end
    85 
    86 (* adapted from logic.ML *)
    87 fun fake_const T = Const (\<^const_name>\<open>fake_quant\<close>, (T --> propT) --> propT);
    88 
    89 fun dependent_fake_name v t =
    90   let
    91     val x = Term.term_name v
    92     val T = Term.fastype_of v
    93     val t' = Term.abstract_over (v, t)
    94   in if Term.is_dependent t' then fake_const T $ Abs (x, T, t') else t end
    95 
    96 in
    97 
    98 fun check_pattern_syntax t =
    99   case strip_all t of
   100     (vars, \<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ lhs $ rhs)) =>
   101       let
   102         fun go (Const (\<^const_name>\<open>as\<close>, _) $ pat $ var, rhs) =
   103               let
   104                 val (pat', rhs') = go (pat, rhs)
   105                 val _ = if is_Free var then () else error "Right-hand side of =: must be a free variable"
   106                 val rhs'' =
   107                   Const (\<^const_name>\<open>Let\<close>, let_typ (fastype_of var) (fastype_of rhs)) $
   108                     pat' $ lambda var rhs'
   109               in
   110                 (pat', rhs'')
   111               end
   112           | go (t $ u, rhs) =
   113               let
   114                 val (t', rhs') = go (t, rhs)
   115                 val (u', rhs'') = go (u, rhs')
   116               in (t' $ u', rhs'') end
   117           | go (t, rhs) = (t, rhs)
   118 
   119         val (lhs', rhs') = go (lhs, rhs)
   120 
   121         val res = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs', rhs'))
   122 
   123         val frees = filter (member (op =) vars) (all_Frees res)
   124       in fold (fn v => Logic.dependent_all_name ("", v)) (map Free frees) res end
   125   | _ => t
   126 
   127 fun uncheck_pattern_syntax ctxt t =
   128   case strip_all t of
   129     (vars, \<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ lhs $ rhs)) =>
   130       let
   131         (* restricted to going down abstractions; ignores eta-contracted rhs *)
   132         fun go lhs (rhs as Const (\<^const_name>\<open>Let\<close>, _) $ pat $ Abs (name, typ, t)) ctxt frees =
   133               if exists_subterm (fn t' => t' = pat) lhs then
   134                 let
   135                   val ([name'], ctxt') = Variable.variant_fixes [name] ctxt
   136                   val free = Free (name', typ)
   137                   val subst = (pat, Const (\<^const_name>\<open>as\<close>, as_typ typ) $ pat $ free)
   138                   val lhs' = subst_once subst lhs
   139                   val rhs' = subst_bound (free, t)
   140                 in
   141                   go lhs' rhs' ctxt' (Free (name', typ) :: frees)
   142                 end
   143               else
   144                 (lhs, rhs, ctxt, frees)
   145           | go lhs rhs ctxt frees = (lhs, rhs, ctxt, frees)
   146 
   147         val (lhs', rhs', _, frees) = go lhs rhs ctxt []
   148 
   149         val res =
   150           HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs', rhs'))
   151           |> fold (fn v => Logic.dependent_all_name ("", v)) (map Free vars)
   152           |> fold dependent_fake_name frees
   153       in
   154         if null frees then t else res
   155       end
   156   | _ => t
   157 
   158 end
   159 \<close>
   160 
   161 bundle pattern_aliases begin
   162 
   163   notation as (infixr "=:" 1)
   164 
   165   declaration \<open>K (Syntax_Phases.term_check 98 "pattern_syntax" (K (map check_pattern_syntax)))\<close>
   166   declaration \<open>K (Syntax_Phases.term_uncheck 98 "pattern_syntax" (map o uncheck_pattern_syntax))\<close>
   167 
   168   declare let_cong_unfolding [fundef_cong]
   169   declare Let_def [simp]
   170 
   171 end
   172 
   173 hide_const as
   174 hide_const fake_quant
   175 
   176 
   177 subsection \<open>Usage\<close>
   178 
   179 context includes pattern_aliases begin
   180 
   181 text \<open>Not very useful for plain definitions, but works anyway.\<close>
   182 
   183 private definition "test_1 x (y =: z) = y + z"
   184 
   185 lemma "test_1 x y = y + y"
   186 by (rule test_1_def[unfolded Let_def])
   187 
   188 text \<open>Very useful for function definitions.\<close>
   189 
   190 private fun test_2 where
   191 "test_2 (y # (y' # ys =: x') =: x) = x @ x' @ x'" |
   192 "test_2 _ = []"
   193 
   194 lemma "test_2 (y # y' # ys) = (y # y' # ys) @ (y' # ys) @ (y' # ys)"
   195 by (rule test_2.simps[unfolded Let_def])
   196 
   197 ML\<open>
   198 let
   199   val actual =
   200     @{thm test_2.simps(1)}
   201     |> Thm.prop_of
   202     |> Syntax.string_of_term \<^context>
   203     |> YXML.content_of
   204   val expected = "test_2 (?y # (?y' # ?ys =: x') =: x) = x @ x' @ x'"
   205 in \<^assert> (actual = expected) end
   206 \<close>
   207 
   208 end
   209 
   210 end