src/HOL/Tools/SMT/smt_normalize.ML
changeset 40278 0fc78bb54f18
parent 40275 eed48b11abdb
child 40279 96365b4ae7b6
     1.1 --- a/src/HOL/Tools/SMT/smt_normalize.ML	Fri Oct 29 18:17:08 2010 +0200
     1.2 +++ b/src/HOL/Tools/SMT/smt_normalize.ML	Fri Oct 29 18:17:09 2010 +0200
     1.3 @@ -19,7 +19,8 @@
     1.4  sig
     1.5    type extra_norm = bool -> (int * thm) list -> Proof.context ->
     1.6      (int * thm) list * Proof.context
     1.7 -  val normalize: extra_norm -> bool -> (int * thm) list -> Proof.context ->
     1.8 +  val normalize: (Proof.context -> (thm -> string) -> thm -> unit) -> bool ->
     1.9 +    extra_norm -> bool -> (int * thm) list -> Proof.context ->
    1.10      (int * thm) list * Proof.context
    1.11    val atomize_conv: Proof.context -> conv
    1.12    val eta_expand_conv: (Proof.context -> conv) -> Proof.context -> conv
    1.13 @@ -486,18 +487,28 @@
    1.14  
    1.15  fun with_context f irules ctxt = (f ctxt irules, ctxt)
    1.16  
    1.17 -fun normalize extra_norm with_datatypes irules ctxt =
    1.18 -  irules
    1.19 -  |> trivial_distinct ctxt
    1.20 -  |> rewrite_bool_cases ctxt
    1.21 -  |> normalize_numerals ctxt
    1.22 -  |> nat_as_int ctxt
    1.23 -  |> rpair ctxt
    1.24 -  |-> extra_norm with_datatypes
    1.25 -  |-> with_context (fn cx => map (apsnd (normalize_rule cx)))
    1.26 -  |-> SMT_Monomorph.monomorph
    1.27 -  |-> lift_lambdas
    1.28 -  |-> with_context explicit_application
    1.29 -  |-> (if with_datatypes then datatype_selectors else pair)
    1.30 +fun normalize trace keep_assms extra_norm with_datatypes irules ctxt =
    1.31 +  let
    1.32 +    fun norm f ctxt' (i, thm) =
    1.33 +      if keep_assms then SOME (i, f ctxt' thm)
    1.34 +      else
    1.35 +        (case try (f ctxt') thm of
    1.36 +          SOME thm' => SOME (i, thm')
    1.37 +        | NONE => (trace ctxt' (prefix ("SMT warning: " ^
    1.38 +            "dropping assumption: ") o Display.string_of_thm ctxt') thm; NONE))
    1.39 +  in
    1.40 +    irules
    1.41 +    |> trivial_distinct ctxt
    1.42 +    |> rewrite_bool_cases ctxt
    1.43 +    |> normalize_numerals ctxt
    1.44 +    |> nat_as_int ctxt
    1.45 +    |> rpair ctxt
    1.46 +    |-> extra_norm with_datatypes
    1.47 +    |-> with_context (map_filter o norm normalize_rule)
    1.48 +    |-> SMT_Monomorph.monomorph
    1.49 +    |-> lift_lambdas
    1.50 +    |-> with_context explicit_application
    1.51 +    |-> (if with_datatypes then datatype_selectors else pair)
    1.52 +  end
    1.53  
    1.54  end