added simps_of_case and case_of_simps to convert between simps and case rules
authornoschinl
Fri Sep 06 10:56:40 2013 +0200 (2013-09-06)
changeset 5342692db671e0ac6
parent 53395 a1a78a271682
child 53427 415354b68f0c
added simps_of_case and case_of_simps to convert between simps and case rules
src/HOL/Library/Simps_Case_Conv.thy
src/HOL/Library/simps_case_conv.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Library/Simps_Case_Conv.thy	Fri Sep 06 10:56:40 2013 +0200
     1.3 @@ -0,0 +1,12 @@
     1.4 +(*  Title:    HOL/Library/Simps_Case_Conv.thy
     1.5 +    Author:   Lars Noschinski
     1.6 +*)
     1.7 +
     1.8 +theory Simps_Case_Conv
     1.9 +  imports Main
    1.10 +  keywords "simps_of_case" "case_of_simps" :: thy_decl
    1.11 +begin
    1.12 +
    1.13 +ML_file "simps_case_conv.ML"
    1.14 +
    1.15 +end
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Library/simps_case_conv.ML	Fri Sep 06 10:56:40 2013 +0200
     2.3 @@ -0,0 +1,202 @@
     2.4 +(*  Title:      HOL/Library/simps_case_conv.ML
     2.5 +    Author:     Lars Noschinski, TU Muenchen
     2.6 +                Gerwin Klein, NICTA
     2.7 +
     2.8 +  Converts function specifications between the representation as
     2.9 +  a list of equations (with patterns on the lhs) and a single
    2.10 +  equation (with a nested case expression on the rhs).
    2.11 +*)
    2.12 +
    2.13 +signature SIMPS_CASE_CONV =
    2.14 +sig
    2.15 +  val to_case: Proof.context -> thm list -> thm
    2.16 +  val gen_to_simps: Proof.context -> thm list -> thm -> thm list
    2.17 +  val to_simps: Proof.context -> thm -> thm list
    2.18 +end
    2.19 +
    2.20 +structure Simps_Case_Conv: SIMPS_CASE_CONV =
    2.21 +struct
    2.22 +
    2.23 +(* Collects all type constructors in a type *)
    2.24 +fun collect_Tcons (Type (name,Ts)) = name :: maps collect_Tcons Ts
    2.25 +  | collect_Tcons (TFree _) = []
    2.26 +  | collect_Tcons (TVar _) = []
    2.27 +
    2.28 +fun get_split_ths thy = collect_Tcons
    2.29 +    #> distinct (op =)
    2.30 +    #> map_filter (Datatype_Data.get_info thy)
    2.31 +    #> map #split
    2.32 +
    2.33 +val strip_eq = prop_of #> HOLogic.dest_Trueprop #> HOLogic.dest_eq
    2.34 +
    2.35 +
    2.36 +local
    2.37 +
    2.38 +(*Creates free variables for a list of types*)
    2.39 +fun mk_Frees Ts ctxt =
    2.40 +  let
    2.41 +    val (names,ctxt') = Variable.variant_fixes (replicate (length Ts) "x") ctxt
    2.42 +    val ts = map Free (names ~~ Ts)
    2.43 +  in (ts, ctxt') end
    2.44 +
    2.45 +fun tac ctxt {splits, intros, defs} =
    2.46 +  let val ctxt' = Classical.addSIs (ctxt, intros) in
    2.47 +    REPEAT_DETERM1 (FIRSTGOAL (split_tac splits))
    2.48 +    THEN Local_Defs.unfold_tac ctxt defs
    2.49 +    THEN safe_tac ctxt'
    2.50 +  end
    2.51 +
    2.52 +fun import [] ctxt = ([], ctxt)
    2.53 +  | import (thm :: thms) ctxt =
    2.54 +    let
    2.55 +      val fun_ct = strip_eq #> fst #> strip_comb #> fst #> Logic.mk_term
    2.56 +        #> Thm.cterm_of (Proof_Context.theory_of ctxt)
    2.57 +      val ct = fun_ct thm
    2.58 +      val cts = map fun_ct thms
    2.59 +      val pairs = map (fn s => (s,ct)) cts
    2.60 +      val thms' = map (fn (th,p) => Thm.instantiate (Thm.match p) th) (thms ~~ pairs)
    2.61 +    in Variable.import true (thm :: thms') ctxt |> apfst snd end
    2.62 +
    2.63 +in
    2.64 +
    2.65 +(*
    2.66 +  For a list
    2.67 +    f p_11 ... p_1n = t1
    2.68 +    f p_21 ... p_2n = t2
    2.69 +    ...
    2.70 +    f p_mn ... p_mn = tm
    2.71 +  of theorems, prove a single theorem
    2.72 +    f x1 ... xn = t
    2.73 +  where t is a (nested) case expression. The terms p_11, ..., p_mn must
    2.74 +  be exhaustive, non-overlapping datatype patterns. f must not be a function
    2.75 +  application.
    2.76 +*)
    2.77 +fun to_case ctxt ths =
    2.78 +  let
    2.79 +    val (iths, ctxt') = import ths ctxt
    2.80 +    val (fun_t, arg_ts) = hd iths |> strip_eq |> fst |> strip_comb
    2.81 +    val eqs = map (strip_eq #> apfst (snd o strip_comb)) iths
    2.82 +    val (arg_Frees, ctxt'') = mk_Frees (map fastype_of arg_ts) ctxt'
    2.83 +
    2.84 +    fun hide_rhs ((pat, rhs), name) lthy = let
    2.85 +        val frees = fold Term.add_frees pat []
    2.86 +        val abs_rhs = fold absfree frees rhs
    2.87 +        val ((f,def), lthy') = Local_Defs.add_def
    2.88 +          ((Binding.name name, Mixfix.NoSyn), abs_rhs) lthy
    2.89 +      in ((list_comb (f, map Free (rev frees)), def), lthy') end
    2.90 +
    2.91 +    val ((def_ts, def_thms), ctxt3) = let
    2.92 +        val nctxt = Variable.names_of ctxt''
    2.93 +        val names = Name.invent nctxt "rhs" (length eqs)
    2.94 +      in fold_map hide_rhs (eqs ~~ names) ctxt'' |> apfst split_list end
    2.95 +
    2.96 +    val (cases, split_thms) =
    2.97 +      let
    2.98 +        val pattern = map (fst #> HOLogic.mk_tuple) eqs
    2.99 +        val case_arg = HOLogic.mk_tuple arg_Frees
   2.100 +        val cases = Case_Translation.make_case ctxt Case_Translation.Warning Name.context
   2.101 +          case_arg (pattern ~~ def_ts)
   2.102 +        val split_thms = get_split_ths (Proof_Context.theory_of ctxt3) (fastype_of case_arg)
   2.103 +      in (cases, split_thms) end
   2.104 +
   2.105 +    val t = (list_comb (fun_t, arg_Frees), cases)
   2.106 +      |> HOLogic.mk_eq
   2.107 +      |> HOLogic.mk_Trueprop
   2.108 +    val th = Goal.prove ctxt3 [] [] t (fn {context=ctxt, ...} =>
   2.109 +          tac ctxt {splits=split_thms, intros=ths, defs=def_thms})
   2.110 +  in th
   2.111 +    |> singleton (Proof_Context.export ctxt3 ctxt)
   2.112 +    |> Goal.norm_result
   2.113 +  end
   2.114 +
   2.115 +end
   2.116 +
   2.117 +local
   2.118 +
   2.119 +fun was_split t =
   2.120 +  let
   2.121 +    val is_free_eq_imp = is_Free o fst o HOLogic.dest_eq
   2.122 +              o fst o HOLogic.dest_imp
   2.123 +    val get_conjs = HOLogic.dest_conj o HOLogic.dest_Trueprop
   2.124 +    fun dest_alls (Const ("HOL.All", _) $ Abs (_, _, t)) = dest_alls t
   2.125 +      | dest_alls t = t
   2.126 +  in forall (is_free_eq_imp o dest_alls) (get_conjs t) end
   2.127 +        handle TERM _ => false
   2.128 +
   2.129 +fun apply_split ctxt split thm = Seq.of_list
   2.130 +  let val ((_,thm'), ctxt') = Variable.import false [thm] ctxt in
   2.131 +    (Variable.export ctxt' ctxt) (filter (was_split o prop_of) (thm' RL [split]))
   2.132 +  end
   2.133 +
   2.134 +fun forward_tac rules t = Seq.of_list ([t] RL rules)
   2.135 +
   2.136 +val refl_imp = refl RSN (2, mp)
   2.137 +
   2.138 +val get_rules_once_split =
   2.139 +  REPEAT (forward_tac [conjunct1, conjunct2])
   2.140 +    THEN REPEAT (forward_tac [spec])
   2.141 +    THEN (forward_tac [refl_imp])
   2.142 +
   2.143 +fun do_split ctxt split =
   2.144 +  let
   2.145 +    val split' = split RS iffD1;
   2.146 +    val split_rhs = concl_of (hd (snd (fst (Variable.import false [split'] ctxt))))
   2.147 +  in if was_split split_rhs
   2.148 +     then DETERM (apply_split ctxt split') THEN get_rules_once_split
   2.149 +     else raise TERM ("malformed split rule", [split_rhs])
   2.150 +  end
   2.151 +
   2.152 +val atomize_meta_eq = forward_tac [meta_eq_to_obj_eq]
   2.153 +
   2.154 +in
   2.155 +
   2.156 +fun gen_to_simps ctxt splitthms thm =
   2.157 +  Seq.list_of ((TRY atomize_meta_eq
   2.158 +                 THEN (REPEAT (FIRST (map (do_split ctxt) splitthms)))) thm)
   2.159 +
   2.160 +fun to_simps ctxt thm =
   2.161 +  let
   2.162 +    val T = thm |> strip_eq |> fst |> strip_comb |> fst |> fastype_of
   2.163 +    val splitthms = get_split_ths (Proof_Context.theory_of ctxt) T
   2.164 +  in gen_to_simps ctxt splitthms thm end
   2.165 +
   2.166 +
   2.167 +end
   2.168 +
   2.169 +fun case_of_simps_cmd (bind, thms_ref) lthy =
   2.170 +  let
   2.171 +    val thy = Proof_Context.theory_of lthy
   2.172 +    val bind' = apsnd (map (Attrib.intern_src thy)) bind
   2.173 +    val thm = (Attrib.eval_thms lthy) thms_ref |> to_case lthy
   2.174 +  in
   2.175 +    Local_Theory.note (bind', [thm]) lthy |> snd
   2.176 +  end
   2.177 +
   2.178 +fun simps_of_case_cmd ((bind, thm_ref), splits_ref) lthy =
   2.179 +  let
   2.180 +    val thy = Proof_Context.theory_of lthy
   2.181 +    val bind' = apsnd (map (Attrib.intern_src thy)) bind
   2.182 +    val thm = singleton (Attrib.eval_thms lthy) thm_ref
   2.183 +    val simps = if null splits_ref
   2.184 +      then to_simps lthy thm
   2.185 +      else gen_to_simps lthy (Attrib.eval_thms lthy splits_ref) thm
   2.186 +  in
   2.187 +    Local_Theory.note (bind', simps) lthy |> snd
   2.188 +  end
   2.189 +
   2.190 +val _ =
   2.191 +  Outer_Syntax.local_theory @{command_spec "case_of_simps"}
   2.192 +    "turns a list of equations into a case expression"
   2.193 +    (Parse_Spec.opt_thm_name ":"  -- Parse_Spec.xthms1 >> case_of_simps_cmd)
   2.194 +
   2.195 +val parse_splits = @{keyword "("} |-- Parse.reserved "splits" |-- @{keyword ":"} |--
   2.196 +  Parse_Spec.xthms1 --| @{keyword ")"}
   2.197 +
   2.198 +val _ =
   2.199 +  Outer_Syntax.local_theory @{command_spec "simps_of_case"}
   2.200 +    "perform case split on rule"
   2.201 +    (Parse_Spec.opt_thm_name ":"  -- Parse_Spec.xthm --
   2.202 +      Scan.optional parse_splits [] >> simps_of_case_cmd)
   2.203 +
   2.204 +end
   2.205 +