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