src/HOL/Library/simps_case_conv.ML
author haftmann
Fri Mar 22 19:18:08 2019 +0000 (3 months ago)
changeset 69946 494934c30f38
parent 69593 3dda49e08b9d
permissions -rw-r--r--
improved code equations taken over from AFP
     1 (*  Title:      HOL/Library/simps_case_conv.ML
     2     Author:     Lars Noschinski, TU Muenchen
     3     Author:     Gerwin Klein, NICTA
     4 
     5 Convert function specifications between the representation as a list
     6 of equations (with patterns on the lhs) and a single equation (with a
     7 nested case expression on the rhs).
     8 *)
     9 
    10 signature SIMPS_CASE_CONV =
    11 sig
    12   val to_case: Proof.context -> thm list -> thm
    13   val gen_to_simps: Proof.context -> thm list -> thm -> thm list
    14   val to_simps: Proof.context -> thm -> thm list
    15 end
    16 
    17 structure Simps_Case_Conv: SIMPS_CASE_CONV =
    18 struct
    19 
    20 (* Collects all type constructors in a type *)
    21 fun collect_Tcons (Type (name,Ts)) = name :: maps collect_Tcons Ts
    22   | collect_Tcons (TFree _) = []
    23   | collect_Tcons (TVar _) = []
    24 
    25 fun get_type_infos ctxt =
    26     maps collect_Tcons
    27     #> distinct (op =)
    28     #> map_filter (Ctr_Sugar.ctr_sugar_of ctxt)
    29 
    30 fun get_split_ths ctxt = get_type_infos ctxt #> map #split
    31 
    32 val strip_eq = Thm.prop_of #> HOLogic.dest_Trueprop #> HOLogic.dest_eq
    33 
    34 (*
    35   For a list
    36     f p_11 ... p_1n = t1
    37     f p_21 ... p_2n = t2
    38     ...
    39     f p_mn ... p_mn = tm
    40   of theorems, prove a single theorem
    41     f x1 ... xn = t
    42   where t is a (nested) case expression. f must not be a function
    43   application.
    44 *)
    45 fun to_case ctxt ths =
    46   let
    47     fun ctr_count (ctr, T) = 
    48       let
    49         val tyco = body_type T |> dest_Type |> fst
    50         val info = Ctr_Sugar.ctr_sugar_of ctxt tyco
    51         val _ = if is_none info then error ("Pattern match on non-constructor constant " ^ ctr) else ()
    52       in
    53         info |> the |> #ctrs |> length
    54       end
    55     val thms = Case_Converter.to_case ctxt Case_Converter.keep_constructor_context ctr_count ths
    56   in
    57     case thms of SOME thms => hd thms
    58       | _ => error ("Conversion to case expression failed.")
    59   end
    60 
    61 local
    62 
    63 fun was_split t =
    64   let
    65     val is_free_eq_imp = is_Free o fst o HOLogic.dest_eq o fst o HOLogic.dest_imp
    66     val get_conjs = HOLogic.dest_conj o HOLogic.dest_Trueprop
    67     fun dest_alls (Const (\<^const_name>\<open>All\<close>, _) $ Abs (_, _, t)) = dest_alls t
    68       | dest_alls t = t
    69   in forall (is_free_eq_imp o dest_alls) (get_conjs t) end
    70   handle TERM _ => false
    71 
    72 fun apply_split ctxt split thm = Seq.of_list
    73   let val ((_,thm'), ctxt') = Variable.import false [thm] ctxt in
    74     (Variable.export ctxt' ctxt) (filter (was_split o Thm.prop_of) (thm' RL [split]))
    75   end
    76 
    77 fun forward_tac rules t = Seq.of_list ([t] RL rules)
    78 
    79 val refl_imp = refl RSN (2, mp)
    80 
    81 val get_rules_once_split =
    82   REPEAT (forward_tac [conjunct1, conjunct2])
    83     THEN REPEAT (forward_tac [spec])
    84     THEN (forward_tac [refl_imp])
    85 
    86 fun do_split ctxt split =
    87   case try op RS (split, iffD1) of
    88     NONE => raise TERM ("malformed split rule", [Thm.prop_of split])
    89   | SOME split' =>
    90       let val split_rhs = Thm.concl_of (hd (snd (fst (Variable.import false [split'] ctxt))))
    91       in if was_split split_rhs
    92          then DETERM (apply_split ctxt split') THEN get_rules_once_split
    93          else raise TERM ("malformed split rule", [split_rhs])
    94       end
    95 
    96 val atomize_meta_eq = forward_tac [meta_eq_to_obj_eq]
    97 
    98 in
    99 
   100 fun gen_to_simps ctxt splitthms thm =
   101   let val splitthms' = filter (fn t => not (Thm.eq_thm (t, Drule.dummy_thm))) splitthms
   102   in
   103     Seq.list_of ((TRY atomize_meta_eq THEN (REPEAT (FIRST (map (do_split ctxt) splitthms')))) thm)
   104   end
   105 
   106 fun to_simps ctxt thm =
   107   let
   108     val T = thm |> strip_eq |> fst |> strip_comb |> fst |> fastype_of
   109     val splitthms = get_split_ths ctxt [T]
   110   in gen_to_simps ctxt splitthms thm end
   111 
   112 
   113 end
   114 
   115 fun case_of_simps_cmd (bind, thms_ref) lthy =
   116   let
   117     val bind' = apsnd (map (Attrib.check_src lthy)) bind
   118     val thm = Attrib.eval_thms lthy thms_ref |> to_case lthy
   119   in
   120     Local_Theory.note (bind', [thm]) lthy |> snd
   121   end
   122 
   123 fun simps_of_case_cmd ((bind, thm_ref), splits_ref) lthy =
   124   let
   125     val bind' = apsnd (map (Attrib.check_src lthy)) bind
   126     val thm = singleton (Attrib.eval_thms lthy) thm_ref
   127     val simps = if null splits_ref
   128       then to_simps lthy thm
   129       else gen_to_simps lthy (Attrib.eval_thms lthy splits_ref) thm
   130   in
   131     Local_Theory.note (bind', simps) lthy |> snd
   132   end
   133 
   134 val _ =
   135   Outer_Syntax.local_theory \<^command_keyword>\<open>case_of_simps\<close>
   136     "turn a list of equations into a case expression"
   137     (Parse_Spec.opt_thm_name ":"  -- Parse.thms1 >> case_of_simps_cmd)
   138 
   139 val parse_splits = \<^keyword>\<open>(\<close> |-- Parse.reserved "splits" |-- \<^keyword>\<open>:\<close> |--
   140   Parse.thms1 --| \<^keyword>\<open>)\<close>
   141 
   142 val _ =
   143   Outer_Syntax.local_theory \<^command_keyword>\<open>simps_of_case\<close>
   144     "perform case split on rule"
   145     (Parse_Spec.opt_thm_name ":"  -- Parse.thm --
   146       Scan.optional parse_splits [] >> simps_of_case_cmd)
   147 
   148 end
   149