src/HOL/Library/simps_case_conv.ML
author wenzelm
Wed Jun 17 11:03:05 2015 +0200 (2015-06-17)
changeset 60500 903bb1495239
parent 60355 ccafd7d193e7
child 60702 5e03e1bd1be0
permissions -rw-r--r--
isabelle update_cartouches;
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
wenzelm@59582
    30
val strip_eq = Thm.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
wenzelm@58956
    91
    REPEAT_DETERM1 (FIRSTGOAL (split_tac ctxt 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
wenzelm@59621
   100
        #> Thm.cterm_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
wenzelm@59650
   128
    fun hide_rhs ((pat, rhs), name) lthy =
wenzelm@59650
   129
      let
noschinl@53426
   130
        val frees = fold Term.add_frees pat []
noschinl@53426
   131
        val abs_rhs = fold absfree frees rhs
noschinl@53426
   132
        val ((f,def), lthy') = Local_Defs.add_def
noschinl@53426
   133
          ((Binding.name name, Mixfix.NoSyn), abs_rhs) lthy
noschinl@53426
   134
      in ((list_comb (f, map Free (rev frees)), def), lthy') end
noschinl@53426
   135
wenzelm@59650
   136
    val ((def_ts, def_thms), ctxt2) =
wenzelm@59650
   137
      let val names = Name.invent (Variable.names_of ctxt') "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
wenzelm@59582
   164
    (Variable.export ctxt' ctxt) (filter (was_split o Thm.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@60355
   177
  case try op RS (split, iffD1) of
noschinl@60355
   178
    NONE => raise TERM ("malformed split rule", [Thm.prop_of split])
noschinl@60355
   179
  | SOME split' =>
noschinl@60355
   180
      let val split_rhs = Thm.concl_of (hd (snd (fst (Variable.import false [split'] ctxt))))
noschinl@60355
   181
      in if was_split split_rhs
noschinl@60355
   182
         then DETERM (apply_split ctxt split') THEN get_rules_once_split
noschinl@60355
   183
         else raise TERM ("malformed split rule", [split_rhs])
noschinl@60355
   184
      end
noschinl@53426
   185
noschinl@53426
   186
val atomize_meta_eq = forward_tac [meta_eq_to_obj_eq]
noschinl@53426
   187
noschinl@53426
   188
in
noschinl@53426
   189
noschinl@53426
   190
fun gen_to_simps ctxt splitthms thm =
noschinl@60354
   191
  let val splitthms' = filter (fn t => not (Thm.eq_thm (t, Drule.dummy_thm))) splitthms
noschinl@60354
   192
  in
noschinl@60354
   193
    Seq.list_of ((TRY atomize_meta_eq THEN (REPEAT (FIRST (map (do_split ctxt) splitthms')))) thm)
noschinl@60354
   194
  end
noschinl@53426
   195
noschinl@53426
   196
fun to_simps ctxt thm =
noschinl@53426
   197
  let
noschinl@53426
   198
    val T = thm |> strip_eq |> fst |> strip_comb |> fst |> fastype_of
blanchet@54401
   199
    val splitthms = get_split_ths ctxt T
noschinl@53426
   200
  in gen_to_simps ctxt splitthms thm end
noschinl@53426
   201
noschinl@53426
   202
noschinl@53426
   203
end
noschinl@53426
   204
noschinl@53426
   205
fun case_of_simps_cmd (bind, thms_ref) lthy =
noschinl@53426
   206
  let
wenzelm@55997
   207
    val bind' = apsnd (map (Attrib.check_src lthy)) bind
noschinl@53426
   208
    val thm = (Attrib.eval_thms lthy) thms_ref |> to_case lthy
noschinl@53426
   209
  in
noschinl@53426
   210
    Local_Theory.note (bind', [thm]) lthy |> snd
noschinl@53426
   211
  end
noschinl@53426
   212
noschinl@53426
   213
fun simps_of_case_cmd ((bind, thm_ref), splits_ref) lthy =
noschinl@53426
   214
  let
wenzelm@55997
   215
    val bind' = apsnd (map (Attrib.check_src lthy)) bind
noschinl@53426
   216
    val thm = singleton (Attrib.eval_thms lthy) thm_ref
noschinl@53426
   217
    val simps = if null splits_ref
noschinl@53426
   218
      then to_simps lthy thm
noschinl@53426
   219
      else gen_to_simps lthy (Attrib.eval_thms lthy splits_ref) thm
noschinl@53426
   220
  in
noschinl@53426
   221
    Local_Theory.note (bind', simps) lthy |> snd
noschinl@53426
   222
  end
noschinl@53426
   223
noschinl@53426
   224
val _ =
wenzelm@59936
   225
  Outer_Syntax.local_theory @{command_keyword case_of_simps}
wenzelm@57628
   226
    "turn a list of equations into a case expression"
wenzelm@58028
   227
    (Parse_Spec.opt_thm_name ":"  -- Parse.xthms1 >> case_of_simps_cmd)
noschinl@53426
   228
noschinl@53426
   229
val parse_splits = @{keyword "("} |-- Parse.reserved "splits" |-- @{keyword ":"} |--
wenzelm@58028
   230
  Parse.xthms1 --| @{keyword ")"}
noschinl@53426
   231
noschinl@53426
   232
val _ =
wenzelm@59936
   233
  Outer_Syntax.local_theory @{command_keyword simps_of_case}
noschinl@53426
   234
    "perform case split on rule"
wenzelm@58028
   235
    (Parse_Spec.opt_thm_name ":"  -- Parse.xthm --
noschinl@53426
   236
      Scan.optional parse_splits [] >> simps_of_case_cmd)
noschinl@53426
   237
noschinl@53426
   238
end
noschinl@53426
   239