src/HOL/Tools/SMT/smt_normalize.ML
changeset 41300 528f5d00b542
parent 41280 a7de9d36f4f2
child 41327 49feace87649
     1.1 --- a/src/HOL/Tools/SMT/smt_normalize.ML	Sun Dec 19 18:38:50 2010 -0800
     1.2 +++ b/src/HOL/Tools/SMT/smt_normalize.ML	Mon Dec 20 08:17:23 2010 +0100
     1.3 @@ -10,8 +10,8 @@
     1.4    type extra_norm = Proof.context -> thm list * thm list -> thm list * thm list
     1.5    val add_extra_norm: SMT_Utils.class * extra_norm -> Context.generic ->
     1.6      Context.generic
     1.7 -  val normalize: Proof.context -> (int * (int option * thm)) list ->
     1.8 -    (int * thm) list
     1.9 +  val normalize: (int * (int option * thm)) list -> Proof.context ->
    1.10 +    (int * thm) list * Proof.context
    1.11    val setup: theory -> theory
    1.12  end
    1.13  
    1.14 @@ -574,17 +574,21 @@
    1.15    rewrite_bool_case_conv ctxt then_conv
    1.16    unfold_abs_min_max_conv ctxt then_conv
    1.17    nat_as_int_conv ctxt then_conv
    1.18 -  normalize_numerals_conv ctxt then_conv
    1.19    Thm.beta_conversion true
    1.20  
    1.21 +fun unfold1 ctxt = map (apsnd (Conv.fconv_rule (unfold_conv ctxt)))
    1.22 +
    1.23  fun burrow_ids f ithms =
    1.24    let
    1.25      val (is, thms) = split_list ithms
    1.26      val (thms', extra_thms) = f thms
    1.27    in (is ~~ thms') @ map (pair ~1) extra_thms end
    1.28  
    1.29 -fun unfold ctxt =
    1.30 -  burrow_ids (map (Conv.fconv_rule (unfold_conv ctxt)) #> add_nat_embedding)
    1.31 +fun unfold2 ithms ctxt =
    1.32 +  ithms
    1.33 +  |> map (apsnd (Conv.fconv_rule (normalize_numerals_conv ctxt)))
    1.34 +  |> burrow_ids add_nat_embedding
    1.35 +  |> rpair ctxt
    1.36  
    1.37  
    1.38  
    1.39 @@ -602,17 +606,20 @@
    1.40  
    1.41  fun add_extra_norm (cs, norm) = Extra_Norms.map (U.dict_update (cs, norm))
    1.42  
    1.43 -fun apply_extra_norms ctxt =
    1.44 +fun apply_extra_norms ithms ctxt =
    1.45    let
    1.46      val cs = SMT_Config.solver_class_of ctxt
    1.47      val es = U.dict_lookup (Extra_Norms.get (Context.Proof ctxt)) cs
    1.48 -  in burrow_ids (fold (fn e => e ctxt) es o rpair []) end
    1.49 +  in (burrow_ids (fold (fn e => e ctxt) es o rpair []) ithms, ctxt) end
    1.50  
    1.51 -fun normalize ctxt iwthms =
    1.52 +fun normalize iwthms ctxt =
    1.53    iwthms
    1.54    |> gen_normalize ctxt
    1.55 -  |> unfold ctxt
    1.56 -  |> apply_extra_norms ctxt
    1.57 +  |> unfold1 ctxt
    1.58 +  |> rpair ctxt
    1.59 +  |-> SMT_Monomorph.monomorph
    1.60 +  |-> unfold2
    1.61 +  |-> apply_extra_norms
    1.62  
    1.63  val setup = Context.theory_map (
    1.64    setup_atomize #>