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