src/HOL/Library/simps_case_conv.ML
author noschinl
Fri Sep 06 10:56:40 2013 +0200 (2013-09-06)
changeset 53426 92db671e0ac6
child 53429 9d9945941eab
permissions -rw-r--r--
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl@53426
     1
(*  Title:      HOL/Library/simps_case_conv.ML
noschinl@53426
     2
    Author:     Lars Noschinski, TU Muenchen
noschinl@53426
     3
                Gerwin Klein, NICTA
noschinl@53426
     4
noschinl@53426
     5
  Converts function specifications between the representation as
noschinl@53426
     6
  a list of equations (with patterns on the lhs) and a single
noschinl@53426
     7
  equation (with a 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@53426
    25
fun get_split_ths thy = collect_Tcons
noschinl@53426
    26
    #> distinct (op =)
noschinl@53426
    27
    #> map_filter (Datatype_Data.get_info thy)
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@53426
    35
(*Creates free variables for a list of types*)
noschinl@53426
    36
fun mk_Frees Ts ctxt =
noschinl@53426
    37
  let
noschinl@53426
    38
    val (names,ctxt') = Variable.variant_fixes (replicate (length Ts) "x") ctxt
noschinl@53426
    39
    val ts = map Free (names ~~ Ts)
noschinl@53426
    40
  in (ts, ctxt') end
noschinl@53426
    41
noschinl@53426
    42
fun tac ctxt {splits, intros, defs} =
noschinl@53426
    43
  let val ctxt' = Classical.addSIs (ctxt, intros) in
noschinl@53426
    44
    REPEAT_DETERM1 (FIRSTGOAL (split_tac splits))
noschinl@53426
    45
    THEN Local_Defs.unfold_tac ctxt defs
noschinl@53426
    46
    THEN safe_tac ctxt'
noschinl@53426
    47
  end
noschinl@53426
    48
noschinl@53426
    49
fun import [] ctxt = ([], ctxt)
noschinl@53426
    50
  | import (thm :: thms) ctxt =
noschinl@53426
    51
    let
noschinl@53426
    52
      val fun_ct = strip_eq #> fst #> strip_comb #> fst #> Logic.mk_term
noschinl@53426
    53
        #> Thm.cterm_of (Proof_Context.theory_of ctxt)
noschinl@53426
    54
      val ct = fun_ct thm
noschinl@53426
    55
      val cts = map fun_ct thms
noschinl@53426
    56
      val pairs = map (fn s => (s,ct)) cts
noschinl@53426
    57
      val thms' = map (fn (th,p) => Thm.instantiate (Thm.match p) th) (thms ~~ pairs)
noschinl@53426
    58
    in Variable.import true (thm :: thms') ctxt |> apfst snd end
noschinl@53426
    59
noschinl@53426
    60
in
noschinl@53426
    61
noschinl@53426
    62
(*
noschinl@53426
    63
  For a list
noschinl@53426
    64
    f p_11 ... p_1n = t1
noschinl@53426
    65
    f p_21 ... p_2n = t2
noschinl@53426
    66
    ...
noschinl@53426
    67
    f p_mn ... p_mn = tm
noschinl@53426
    68
  of theorems, prove a single theorem
noschinl@53426
    69
    f x1 ... xn = t
noschinl@53426
    70
  where t is a (nested) case expression. The terms p_11, ..., p_mn must
noschinl@53426
    71
  be exhaustive, non-overlapping datatype patterns. f must not be a function
noschinl@53426
    72
  application.
noschinl@53426
    73
*)
noschinl@53426
    74
fun to_case ctxt ths =
noschinl@53426
    75
  let
noschinl@53426
    76
    val (iths, ctxt') = import ths ctxt
noschinl@53426
    77
    val (fun_t, arg_ts) = hd iths |> strip_eq |> fst |> strip_comb
noschinl@53426
    78
    val eqs = map (strip_eq #> apfst (snd o strip_comb)) iths
noschinl@53426
    79
    val (arg_Frees, ctxt'') = mk_Frees (map fastype_of arg_ts) ctxt'
noschinl@53426
    80
noschinl@53426
    81
    fun hide_rhs ((pat, rhs), name) lthy = let
noschinl@53426
    82
        val frees = fold Term.add_frees pat []
noschinl@53426
    83
        val abs_rhs = fold absfree frees rhs
noschinl@53426
    84
        val ((f,def), lthy') = Local_Defs.add_def
noschinl@53426
    85
          ((Binding.name name, Mixfix.NoSyn), abs_rhs) lthy
noschinl@53426
    86
      in ((list_comb (f, map Free (rev frees)), def), lthy') end
noschinl@53426
    87
noschinl@53426
    88
    val ((def_ts, def_thms), ctxt3) = let
noschinl@53426
    89
        val nctxt = Variable.names_of ctxt''
noschinl@53426
    90
        val names = Name.invent nctxt "rhs" (length eqs)
noschinl@53426
    91
      in fold_map hide_rhs (eqs ~~ names) ctxt'' |> apfst split_list end
noschinl@53426
    92
noschinl@53426
    93
    val (cases, split_thms) =
noschinl@53426
    94
      let
noschinl@53426
    95
        val pattern = map (fst #> HOLogic.mk_tuple) eqs
noschinl@53426
    96
        val case_arg = HOLogic.mk_tuple arg_Frees
noschinl@53426
    97
        val cases = Case_Translation.make_case ctxt Case_Translation.Warning Name.context
noschinl@53426
    98
          case_arg (pattern ~~ def_ts)
noschinl@53426
    99
        val split_thms = get_split_ths (Proof_Context.theory_of ctxt3) (fastype_of case_arg)
noschinl@53426
   100
      in (cases, split_thms) end
noschinl@53426
   101
noschinl@53426
   102
    val t = (list_comb (fun_t, arg_Frees), cases)
noschinl@53426
   103
      |> HOLogic.mk_eq
noschinl@53426
   104
      |> HOLogic.mk_Trueprop
noschinl@53426
   105
    val th = Goal.prove ctxt3 [] [] t (fn {context=ctxt, ...} =>
noschinl@53426
   106
          tac ctxt {splits=split_thms, intros=ths, defs=def_thms})
noschinl@53426
   107
  in th
noschinl@53426
   108
    |> singleton (Proof_Context.export ctxt3 ctxt)
noschinl@53426
   109
    |> Goal.norm_result
noschinl@53426
   110
  end
noschinl@53426
   111
noschinl@53426
   112
end
noschinl@53426
   113
noschinl@53426
   114
local
noschinl@53426
   115
noschinl@53426
   116
fun was_split t =
noschinl@53426
   117
  let
noschinl@53426
   118
    val is_free_eq_imp = is_Free o fst o HOLogic.dest_eq
noschinl@53426
   119
              o fst o HOLogic.dest_imp
noschinl@53426
   120
    val get_conjs = HOLogic.dest_conj o HOLogic.dest_Trueprop
noschinl@53426
   121
    fun dest_alls (Const ("HOL.All", _) $ Abs (_, _, t)) = dest_alls t
noschinl@53426
   122
      | dest_alls t = t
noschinl@53426
   123
  in forall (is_free_eq_imp o dest_alls) (get_conjs t) end
noschinl@53426
   124
        handle TERM _ => false
noschinl@53426
   125
noschinl@53426
   126
fun apply_split ctxt split thm = Seq.of_list
noschinl@53426
   127
  let val ((_,thm'), ctxt') = Variable.import false [thm] ctxt in
noschinl@53426
   128
    (Variable.export ctxt' ctxt) (filter (was_split o prop_of) (thm' RL [split]))
noschinl@53426
   129
  end
noschinl@53426
   130
noschinl@53426
   131
fun forward_tac rules t = Seq.of_list ([t] RL rules)
noschinl@53426
   132
noschinl@53426
   133
val refl_imp = refl RSN (2, mp)
noschinl@53426
   134
noschinl@53426
   135
val get_rules_once_split =
noschinl@53426
   136
  REPEAT (forward_tac [conjunct1, conjunct2])
noschinl@53426
   137
    THEN REPEAT (forward_tac [spec])
noschinl@53426
   138
    THEN (forward_tac [refl_imp])
noschinl@53426
   139
noschinl@53426
   140
fun do_split ctxt split =
noschinl@53426
   141
  let
noschinl@53426
   142
    val split' = split RS iffD1;
noschinl@53426
   143
    val split_rhs = concl_of (hd (snd (fst (Variable.import false [split'] ctxt))))
noschinl@53426
   144
  in if was_split split_rhs
noschinl@53426
   145
     then DETERM (apply_split ctxt split') THEN get_rules_once_split
noschinl@53426
   146
     else raise TERM ("malformed split rule", [split_rhs])
noschinl@53426
   147
  end
noschinl@53426
   148
noschinl@53426
   149
val atomize_meta_eq = forward_tac [meta_eq_to_obj_eq]
noschinl@53426
   150
noschinl@53426
   151
in
noschinl@53426
   152
noschinl@53426
   153
fun gen_to_simps ctxt splitthms thm =
noschinl@53426
   154
  Seq.list_of ((TRY atomize_meta_eq
noschinl@53426
   155
                 THEN (REPEAT (FIRST (map (do_split ctxt) splitthms)))) thm)
noschinl@53426
   156
noschinl@53426
   157
fun to_simps ctxt thm =
noschinl@53426
   158
  let
noschinl@53426
   159
    val T = thm |> strip_eq |> fst |> strip_comb |> fst |> fastype_of
noschinl@53426
   160
    val splitthms = get_split_ths (Proof_Context.theory_of ctxt) T
noschinl@53426
   161
  in gen_to_simps ctxt splitthms thm end
noschinl@53426
   162
noschinl@53426
   163
noschinl@53426
   164
end
noschinl@53426
   165
noschinl@53426
   166
fun case_of_simps_cmd (bind, thms_ref) lthy =
noschinl@53426
   167
  let
noschinl@53426
   168
    val thy = Proof_Context.theory_of lthy
noschinl@53426
   169
    val bind' = apsnd (map (Attrib.intern_src thy)) bind
noschinl@53426
   170
    val thm = (Attrib.eval_thms lthy) thms_ref |> to_case lthy
noschinl@53426
   171
  in
noschinl@53426
   172
    Local_Theory.note (bind', [thm]) lthy |> snd
noschinl@53426
   173
  end
noschinl@53426
   174
noschinl@53426
   175
fun simps_of_case_cmd ((bind, thm_ref), splits_ref) lthy =
noschinl@53426
   176
  let
noschinl@53426
   177
    val thy = Proof_Context.theory_of lthy
noschinl@53426
   178
    val bind' = apsnd (map (Attrib.intern_src thy)) bind
noschinl@53426
   179
    val thm = singleton (Attrib.eval_thms lthy) thm_ref
noschinl@53426
   180
    val simps = if null splits_ref
noschinl@53426
   181
      then to_simps lthy thm
noschinl@53426
   182
      else gen_to_simps lthy (Attrib.eval_thms lthy splits_ref) thm
noschinl@53426
   183
  in
noschinl@53426
   184
    Local_Theory.note (bind', simps) lthy |> snd
noschinl@53426
   185
  end
noschinl@53426
   186
noschinl@53426
   187
val _ =
noschinl@53426
   188
  Outer_Syntax.local_theory @{command_spec "case_of_simps"}
noschinl@53426
   189
    "turns a list of equations into a case expression"
noschinl@53426
   190
    (Parse_Spec.opt_thm_name ":"  -- Parse_Spec.xthms1 >> case_of_simps_cmd)
noschinl@53426
   191
noschinl@53426
   192
val parse_splits = @{keyword "("} |-- Parse.reserved "splits" |-- @{keyword ":"} |--
noschinl@53426
   193
  Parse_Spec.xthms1 --| @{keyword ")"}
noschinl@53426
   194
noschinl@53426
   195
val _ =
noschinl@53426
   196
  Outer_Syntax.local_theory @{command_spec "simps_of_case"}
noschinl@53426
   197
    "perform case split on rule"
noschinl@53426
   198
    (Parse_Spec.opt_thm_name ":"  -- Parse_Spec.xthm --
noschinl@53426
   199
      Scan.optional parse_splits [] >> simps_of_case_cmd)
noschinl@53426
   200
noschinl@53426
   201
end
noschinl@53426
   202