src/HOL/Library/simps_case_conv.ML
author Andreas Lochbihler
Tue Jan 01 17:04:53 2019 +0100 (6 months ago)
changeset 69568 de09a7261120
parent 63352 4eaf35781b23
child 69593 3dda49e08b9d
permissions -rw-r--r--
new implementation for case_of_simps based on Code_Lazy's pattern matching elimination algorithm
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
  For a list
noschinl@53426
    36
    f p_11 ... p_1n = t1
noschinl@53426
    37
    f p_21 ... p_2n = t2
noschinl@53426
    38
    ...
noschinl@53426
    39
    f p_mn ... p_mn = tm
noschinl@53426
    40
  of theorems, prove a single theorem
noschinl@53426
    41
    f x1 ... xn = t
noschinl@53429
    42
  where t is a (nested) case expression. f must not be a function
Andreas@69568
    43
  application.
noschinl@53426
    44
*)
noschinl@53426
    45
fun to_case ctxt ths =
noschinl@53426
    46
  let
Andreas@69568
    47
    fun ctr_count (ctr, T) = 
wenzelm@59650
    48
      let
Andreas@69568
    49
        val tyco = body_type T |> dest_Type |> fst
Andreas@69568
    50
        val info = Ctr_Sugar.ctr_sugar_of ctxt tyco
Andreas@69568
    51
        val _ = if is_none info then error ("Pattern match on non-constructor constant " ^ ctr) else ()
Andreas@69568
    52
      in
Andreas@69568
    53
        info |> the |> #ctrs |> length
Andreas@69568
    54
      end
Andreas@69568
    55
    val thms = Case_Converter.to_case ctxt Case_Converter.keep_constructor_context ctr_count ths
Andreas@69568
    56
  in
Andreas@69568
    57
    case thms of SOME thms => hd thms
Andreas@69568
    58
      | _ => error ("Conversion to case expression failed.")
noschinl@53426
    59
  end
noschinl@53426
    60
noschinl@53426
    61
local
noschinl@53426
    62
noschinl@53426
    63
fun was_split t =
noschinl@53426
    64
  let
wenzelm@56252
    65
    val is_free_eq_imp = is_Free o fst o HOLogic.dest_eq o fst o HOLogic.dest_imp
noschinl@53426
    66
    val get_conjs = HOLogic.dest_conj o HOLogic.dest_Trueprop
wenzelm@56252
    67
    fun dest_alls (Const (@{const_name All}, _) $ Abs (_, _, t)) = dest_alls t
noschinl@53426
    68
      | dest_alls t = t
noschinl@53426
    69
  in forall (is_free_eq_imp o dest_alls) (get_conjs t) end
wenzelm@56252
    70
  handle TERM _ => false
noschinl@53426
    71
noschinl@53426
    72
fun apply_split ctxt split thm = Seq.of_list
noschinl@53426
    73
  let val ((_,thm'), ctxt') = Variable.import false [thm] ctxt in
wenzelm@59582
    74
    (Variable.export ctxt' ctxt) (filter (was_split o Thm.prop_of) (thm' RL [split]))
noschinl@53426
    75
  end
noschinl@53426
    76
noschinl@53426
    77
fun forward_tac rules t = Seq.of_list ([t] RL rules)
noschinl@53426
    78
noschinl@53426
    79
val refl_imp = refl RSN (2, mp)
noschinl@53426
    80
noschinl@53426
    81
val get_rules_once_split =
noschinl@53426
    82
  REPEAT (forward_tac [conjunct1, conjunct2])
noschinl@53426
    83
    THEN REPEAT (forward_tac [spec])
noschinl@53426
    84
    THEN (forward_tac [refl_imp])
noschinl@53426
    85
noschinl@53426
    86
fun do_split ctxt split =
noschinl@60355
    87
  case try op RS (split, iffD1) of
noschinl@60355
    88
    NONE => raise TERM ("malformed split rule", [Thm.prop_of split])
noschinl@60355
    89
  | SOME split' =>
noschinl@60355
    90
      let val split_rhs = Thm.concl_of (hd (snd (fst (Variable.import false [split'] ctxt))))
noschinl@60355
    91
      in if was_split split_rhs
noschinl@60355
    92
         then DETERM (apply_split ctxt split') THEN get_rules_once_split
noschinl@60355
    93
         else raise TERM ("malformed split rule", [split_rhs])
noschinl@60355
    94
      end
noschinl@53426
    95
noschinl@53426
    96
val atomize_meta_eq = forward_tac [meta_eq_to_obj_eq]
noschinl@53426
    97
noschinl@53426
    98
in
noschinl@53426
    99
noschinl@53426
   100
fun gen_to_simps ctxt splitthms thm =
noschinl@60354
   101
  let val splitthms' = filter (fn t => not (Thm.eq_thm (t, Drule.dummy_thm))) splitthms
noschinl@60354
   102
  in
noschinl@60354
   103
    Seq.list_of ((TRY atomize_meta_eq THEN (REPEAT (FIRST (map (do_split ctxt) splitthms')))) thm)
noschinl@60354
   104
  end
noschinl@53426
   105
noschinl@53426
   106
fun to_simps ctxt thm =
noschinl@53426
   107
  let
noschinl@53426
   108
    val T = thm |> strip_eq |> fst |> strip_comb |> fst |> fastype_of
noschinl@60702
   109
    val splitthms = get_split_ths ctxt [T]
noschinl@53426
   110
  in gen_to_simps ctxt splitthms thm end
noschinl@53426
   111
noschinl@53426
   112
noschinl@53426
   113
end
noschinl@53426
   114
noschinl@53426
   115
fun case_of_simps_cmd (bind, thms_ref) lthy =
noschinl@53426
   116
  let
wenzelm@55997
   117
    val bind' = apsnd (map (Attrib.check_src lthy)) bind
wenzelm@61813
   118
    val thm = Attrib.eval_thms lthy thms_ref |> to_case lthy
noschinl@53426
   119
  in
noschinl@53426
   120
    Local_Theory.note (bind', [thm]) lthy |> snd
noschinl@53426
   121
  end
noschinl@53426
   122
noschinl@53426
   123
fun simps_of_case_cmd ((bind, thm_ref), splits_ref) lthy =
noschinl@53426
   124
  let
wenzelm@55997
   125
    val bind' = apsnd (map (Attrib.check_src lthy)) bind
noschinl@53426
   126
    val thm = singleton (Attrib.eval_thms lthy) thm_ref
noschinl@53426
   127
    val simps = if null splits_ref
noschinl@53426
   128
      then to_simps lthy thm
noschinl@53426
   129
      else gen_to_simps lthy (Attrib.eval_thms lthy splits_ref) thm
noschinl@53426
   130
  in
noschinl@53426
   131
    Local_Theory.note (bind', simps) lthy |> snd
noschinl@53426
   132
  end
noschinl@53426
   133
noschinl@53426
   134
val _ =
wenzelm@59936
   135
  Outer_Syntax.local_theory @{command_keyword case_of_simps}
wenzelm@57628
   136
    "turn a list of equations into a case expression"
wenzelm@62969
   137
    (Parse_Spec.opt_thm_name ":"  -- Parse.thms1 >> case_of_simps_cmd)
noschinl@53426
   138
noschinl@53426
   139
val parse_splits = @{keyword "("} |-- Parse.reserved "splits" |-- @{keyword ":"} |--
wenzelm@62969
   140
  Parse.thms1 --| @{keyword ")"}
noschinl@53426
   141
noschinl@53426
   142
val _ =
wenzelm@59936
   143
  Outer_Syntax.local_theory @{command_keyword simps_of_case}
noschinl@53426
   144
    "perform case split on rule"
wenzelm@62969
   145
    (Parse_Spec.opt_thm_name ":"  -- Parse.thm --
noschinl@53426
   146
      Scan.optional parse_splits [] >> simps_of_case_cmd)
noschinl@53426
   147
noschinl@53426
   148
end
noschinl@53426
   149