src/HOL/Library/simps_case_conv.ML
author wenzelm
Sat Mar 22 18:15:09 2014 +0100 (2014-03-22)
changeset 56252 b72e0a9d62b9
parent 55997 9dc5ce83202c
child 57628 c80fc5576271
permissions -rw-r--r--
more antiquotations;
noschinl@53426
     1
(*  Title:      HOL/Library/simps_case_conv.ML
noschinl@53426
     2
    Author:     Lars Noschinski, TU Muenchen
wenzelm@53433
     3
    Author:     Gerwin Klein, NICTA
noschinl@53426
     4
wenzelm@53433
     5
Convert function specifications between the representation as a list
wenzelm@53433
     6
of equations (with patterns on the lhs) and a single equation (with a
wenzelm@53433
     7
nested case expression on the rhs).
noschinl@53426
     8
*)
noschinl@53426
     9
noschinl@53426
    10
signature SIMPS_CASE_CONV =
noschinl@53426
    11
sig
noschinl@53426
    12
  val to_case: Proof.context -> thm list -> thm
noschinl@53426
    13
  val gen_to_simps: Proof.context -> thm list -> thm -> thm list
noschinl@53426
    14
  val to_simps: Proof.context -> thm -> thm list
noschinl@53426
    15
end
noschinl@53426
    16
noschinl@53426
    17
structure Simps_Case_Conv: SIMPS_CASE_CONV =
noschinl@53426
    18
struct
noschinl@53426
    19
noschinl@53426
    20
(* Collects all type constructors in a type *)
noschinl@53426
    21
fun collect_Tcons (Type (name,Ts)) = name :: maps collect_Tcons Ts
noschinl@53426
    22
  | collect_Tcons (TFree _) = []
noschinl@53426
    23
  | collect_Tcons (TVar _) = []
noschinl@53426
    24
blanchet@54401
    25
fun get_split_ths ctxt = collect_Tcons
noschinl@53426
    26
    #> distinct (op =)
blanchet@54401
    27
    #> map_filter (Ctr_Sugar.ctr_sugar_of ctxt)
noschinl@53426
    28
    #> map #split
noschinl@53426
    29
noschinl@53426
    30
val strip_eq = prop_of #> HOLogic.dest_Trueprop #> HOLogic.dest_eq
noschinl@53426
    31
noschinl@53426
    32
noschinl@53426
    33
local
noschinl@53426
    34
noschinl@53429
    35
  fun transpose [] = []
noschinl@53429
    36
    | transpose ([] :: xss) = transpose xss
noschinl@53429
    37
    | transpose xss = map hd xss :: transpose (map tl xss);
noschinl@53429
    38
noschinl@53429
    39
  fun same_fun (ts as _ $ _ :: _) =
noschinl@53429
    40
      let
noschinl@53429
    41
        val (fs, argss) = map strip_comb ts |> split_list
noschinl@53429
    42
        val f = hd fs
noschinl@53429
    43
      in if forall (fn x => f = x) fs then SOME (f, argss) else NONE end
noschinl@53429
    44
    | same_fun _ = NONE
noschinl@53429
    45
noschinl@53429
    46
  (* pats must be non-empty *)
noschinl@53429
    47
  fun split_pat pats ctxt =
noschinl@53429
    48
      case same_fun pats of
noschinl@53429
    49
        NONE =>
noschinl@53429
    50
          let
noschinl@53429
    51
            val (name, ctxt') = yield_singleton Variable.variant_fixes "x" ctxt
noschinl@53429
    52
            val var = Free (name, fastype_of (hd pats))
noschinl@53429
    53
          in (((var, [var]), map single pats), ctxt') end
noschinl@53429
    54
      | SOME (f, argss) =>
noschinl@53429
    55
          let
noschinl@53429
    56
            val (((def_pats, def_frees), case_patss), ctxt') =
noschinl@53429
    57
              split_pats argss ctxt
noschinl@53429
    58
            val def_pat = list_comb (f, def_pats)
noschinl@53429
    59
          in (((def_pat, flat def_frees), case_patss), ctxt') end
noschinl@53429
    60
  and
noschinl@53429
    61
      split_pats patss ctxt =
noschinl@53429
    62
        let
noschinl@53429
    63
          val (splitted, ctxt') = fold_map split_pat (transpose patss) ctxt
noschinl@53429
    64
          val r = splitted |> split_list |> apfst split_list |> apsnd (transpose #> map flat)
noschinl@53429
    65
        in (r, ctxt') end
noschinl@53429
    66
noschinl@53429
    67
(*
noschinl@53429
    68
  Takes a list lhss of left hand sides (which are lists of patterns)
noschinl@53429
    69
  and a list rhss of right hand sides. Returns
noschinl@53429
    70
    - a single equation with a (nested) case-expression on the rhs
noschinl@53429
    71
    - a list of all split-thms needed to split the rhs
noschinl@53429
    72
  Patterns which have the same outer context in all lhss remain
noschinl@53429
    73
  on the lhs of the computed equation.
noschinl@53429
    74
*)
noschinl@53429
    75
fun build_case_t fun_t lhss rhss ctxt =
noschinl@53426
    76
  let
noschinl@53429
    77
    val (((def_pats, def_frees), case_patss), ctxt') =
noschinl@53429
    78
      split_pats lhss ctxt
noschinl@53429
    79
    val pattern = map HOLogic.mk_tuple case_patss
noschinl@53429
    80
    val case_arg = HOLogic.mk_tuple (flat def_frees)
noschinl@53429
    81
    val cases = Case_Translation.make_case ctxt' Case_Translation.Warning Name.context
noschinl@53429
    82
      case_arg (pattern ~~ rhss)
blanchet@54401
    83
    val split_thms = get_split_ths ctxt' (fastype_of case_arg)
noschinl@53429
    84
    val t = (list_comb (fun_t, def_pats), cases)
noschinl@53429
    85
      |> HOLogic.mk_eq
noschinl@53429
    86
      |> HOLogic.mk_Trueprop
noschinl@53429
    87
  in ((t, split_thms), ctxt') end
noschinl@53426
    88
noschinl@53426
    89
fun tac ctxt {splits, intros, defs} =
noschinl@53426
    90
  let val ctxt' = Classical.addSIs (ctxt, intros) in
noschinl@53426
    91
    REPEAT_DETERM1 (FIRSTGOAL (split_tac splits))
noschinl@53426
    92
    THEN Local_Defs.unfold_tac ctxt defs
noschinl@53426
    93
    THEN safe_tac ctxt'
noschinl@53426
    94
  end
noschinl@53426
    95
noschinl@53426
    96
fun import [] ctxt = ([], ctxt)
noschinl@53426
    97
  | import (thm :: thms) ctxt =
noschinl@53426
    98
    let
noschinl@53426
    99
      val fun_ct = strip_eq #> fst #> strip_comb #> fst #> Logic.mk_term
noschinl@53426
   100
        #> Thm.cterm_of (Proof_Context.theory_of ctxt)
noschinl@53426
   101
      val ct = fun_ct thm
noschinl@53426
   102
      val cts = map fun_ct thms
noschinl@53426
   103
      val pairs = map (fn s => (s,ct)) cts
noschinl@53426
   104
      val thms' = map (fn (th,p) => Thm.instantiate (Thm.match p) th) (thms ~~ pairs)
noschinl@53426
   105
    in Variable.import true (thm :: thms') ctxt |> apfst snd end
noschinl@53426
   106
noschinl@53426
   107
in
noschinl@53426
   108
noschinl@53426
   109
(*
noschinl@53426
   110
  For a list
noschinl@53426
   111
    f p_11 ... p_1n = t1
noschinl@53426
   112
    f p_21 ... p_2n = t2
noschinl@53426
   113
    ...
noschinl@53426
   114
    f p_mn ... p_mn = tm
noschinl@53426
   115
  of theorems, prove a single theorem
noschinl@53426
   116
    f x1 ... xn = t
noschinl@53429
   117
  where t is a (nested) case expression. f must not be a function
noschinl@53429
   118
  application. Moreover, the terms p_11, ..., p_mn must be non-overlapping
noschinl@53429
   119
  datatype patterns. The patterns must be exhausting up to common constructor
noschinl@53429
   120
  contexts.
noschinl@53426
   121
*)
noschinl@53426
   122
fun to_case ctxt ths =
noschinl@53426
   123
  let
noschinl@53426
   124
    val (iths, ctxt') = import ths ctxt
noschinl@53429
   125
    val fun_t = hd iths |> strip_eq |> fst |> head_of
noschinl@53426
   126
    val eqs = map (strip_eq #> apfst (snd o strip_comb)) iths
noschinl@53426
   127
noschinl@53426
   128
    fun hide_rhs ((pat, rhs), name) lthy = let
noschinl@53426
   129
        val frees = fold Term.add_frees pat []
noschinl@53426
   130
        val abs_rhs = fold absfree frees rhs
noschinl@53426
   131
        val ((f,def), lthy') = Local_Defs.add_def
noschinl@53426
   132
          ((Binding.name name, Mixfix.NoSyn), abs_rhs) lthy
noschinl@53426
   133
      in ((list_comb (f, map Free (rev frees)), def), lthy') end
noschinl@53426
   134
noschinl@53429
   135
    val ((def_ts, def_thms), ctxt2) = let
noschinl@53429
   136
        val nctxt = Variable.names_of ctxt'
noschinl@53426
   137
        val names = Name.invent nctxt "rhs" (length eqs)
noschinl@53429
   138
      in fold_map hide_rhs (eqs ~~ names) ctxt' |> apfst split_list end
noschinl@53426
   139
noschinl@53429
   140
    val ((t, split_thms), ctxt3) = build_case_t fun_t (map fst eqs) def_ts ctxt2
noschinl@53426
   141
noschinl@53426
   142
    val th = Goal.prove ctxt3 [] [] t (fn {context=ctxt, ...} =>
noschinl@53426
   143
          tac ctxt {splits=split_thms, intros=ths, defs=def_thms})
noschinl@53426
   144
  in th
noschinl@53426
   145
    |> singleton (Proof_Context.export ctxt3 ctxt)
wenzelm@54883
   146
    |> Goal.norm_result ctxt
noschinl@53426
   147
  end
noschinl@53426
   148
noschinl@53426
   149
end
noschinl@53426
   150
noschinl@53426
   151
local
noschinl@53426
   152
noschinl@53426
   153
fun was_split t =
noschinl@53426
   154
  let
wenzelm@56252
   155
    val is_free_eq_imp = is_Free o fst o HOLogic.dest_eq o fst o HOLogic.dest_imp
noschinl@53426
   156
    val get_conjs = HOLogic.dest_conj o HOLogic.dest_Trueprop
wenzelm@56252
   157
    fun dest_alls (Const (@{const_name All}, _) $ Abs (_, _, t)) = dest_alls t
noschinl@53426
   158
      | dest_alls t = t
noschinl@53426
   159
  in forall (is_free_eq_imp o dest_alls) (get_conjs t) end
wenzelm@56252
   160
  handle TERM _ => false
noschinl@53426
   161
noschinl@53426
   162
fun apply_split ctxt split thm = Seq.of_list
noschinl@53426
   163
  let val ((_,thm'), ctxt') = Variable.import false [thm] ctxt in
noschinl@53426
   164
    (Variable.export ctxt' ctxt) (filter (was_split o prop_of) (thm' RL [split]))
noschinl@53426
   165
  end
noschinl@53426
   166
noschinl@53426
   167
fun forward_tac rules t = Seq.of_list ([t] RL rules)
noschinl@53426
   168
noschinl@53426
   169
val refl_imp = refl RSN (2, mp)
noschinl@53426
   170
noschinl@53426
   171
val get_rules_once_split =
noschinl@53426
   172
  REPEAT (forward_tac [conjunct1, conjunct2])
noschinl@53426
   173
    THEN REPEAT (forward_tac [spec])
noschinl@53426
   174
    THEN (forward_tac [refl_imp])
noschinl@53426
   175
noschinl@53426
   176
fun do_split ctxt split =
noschinl@53426
   177
  let
noschinl@53426
   178
    val split' = split RS iffD1;
noschinl@53426
   179
    val split_rhs = concl_of (hd (snd (fst (Variable.import false [split'] ctxt))))
noschinl@53426
   180
  in if was_split split_rhs
noschinl@53426
   181
     then DETERM (apply_split ctxt split') THEN get_rules_once_split
noschinl@53426
   182
     else raise TERM ("malformed split rule", [split_rhs])
noschinl@53426
   183
  end
noschinl@53426
   184
noschinl@53426
   185
val atomize_meta_eq = forward_tac [meta_eq_to_obj_eq]
noschinl@53426
   186
noschinl@53426
   187
in
noschinl@53426
   188
noschinl@53426
   189
fun gen_to_simps ctxt splitthms thm =
noschinl@53426
   190
  Seq.list_of ((TRY atomize_meta_eq
noschinl@53426
   191
                 THEN (REPEAT (FIRST (map (do_split ctxt) splitthms)))) thm)
noschinl@53426
   192
noschinl@53426
   193
fun to_simps ctxt thm =
noschinl@53426
   194
  let
noschinl@53426
   195
    val T = thm |> strip_eq |> fst |> strip_comb |> fst |> fastype_of
blanchet@54401
   196
    val splitthms = get_split_ths ctxt T
noschinl@53426
   197
  in gen_to_simps ctxt splitthms thm end
noschinl@53426
   198
noschinl@53426
   199
noschinl@53426
   200
end
noschinl@53426
   201
noschinl@53426
   202
fun case_of_simps_cmd (bind, thms_ref) lthy =
noschinl@53426
   203
  let
wenzelm@55997
   204
    val bind' = apsnd (map (Attrib.check_src lthy)) bind
noschinl@53426
   205
    val thm = (Attrib.eval_thms lthy) thms_ref |> to_case lthy
noschinl@53426
   206
  in
noschinl@53426
   207
    Local_Theory.note (bind', [thm]) lthy |> snd
noschinl@53426
   208
  end
noschinl@53426
   209
noschinl@53426
   210
fun simps_of_case_cmd ((bind, thm_ref), splits_ref) lthy =
noschinl@53426
   211
  let
wenzelm@55997
   212
    val bind' = apsnd (map (Attrib.check_src lthy)) bind
noschinl@53426
   213
    val thm = singleton (Attrib.eval_thms lthy) thm_ref
noschinl@53426
   214
    val simps = if null splits_ref
noschinl@53426
   215
      then to_simps lthy thm
noschinl@53426
   216
      else gen_to_simps lthy (Attrib.eval_thms lthy splits_ref) thm
noschinl@53426
   217
  in
noschinl@53426
   218
    Local_Theory.note (bind', simps) lthy |> snd
noschinl@53426
   219
  end
noschinl@53426
   220
noschinl@53426
   221
val _ =
noschinl@53426
   222
  Outer_Syntax.local_theory @{command_spec "case_of_simps"}
noschinl@53426
   223
    "turns a list of equations into a case expression"
noschinl@53426
   224
    (Parse_Spec.opt_thm_name ":"  -- Parse_Spec.xthms1 >> case_of_simps_cmd)
noschinl@53426
   225
noschinl@53426
   226
val parse_splits = @{keyword "("} |-- Parse.reserved "splits" |-- @{keyword ":"} |--
noschinl@53426
   227
  Parse_Spec.xthms1 --| @{keyword ")"}
noschinl@53426
   228
noschinl@53426
   229
val _ =
noschinl@53426
   230
  Outer_Syntax.local_theory @{command_spec "simps_of_case"}
noschinl@53426
   231
    "perform case split on rule"
noschinl@53426
   232
    (Parse_Spec.opt_thm_name ":"  -- Parse_Spec.xthm --
noschinl@53426
   233
      Scan.optional parse_splits [] >> simps_of_case_cmd)
noschinl@53426
   234
noschinl@53426
   235
end
noschinl@53426
   236