src/HOL/Tools/SMT/smt_normalize.ML
author paulson
Thu Dec 16 12:19:00 2010 +0000 (2010-12-16)
changeset 41194 9796e5e01b61
parent 41174 10eb369f8c01
parent 41193 dc33b8ea4526
child 41224 8a104c2a186f
permissions -rw-r--r--
merged
     1 (*  Title:      HOL/Tools/SMT/smt_normalize.ML
     2     Author:     Sascha Boehme, TU Muenchen
     3 
     4 Normalization steps on theorems required by SMT solvers.
     5 *)
     6 
     7 signature SMT_NORMALIZE =
     8 sig
     9   val atomize_conv: Proof.context -> conv
    10   type extra_norm = Proof.context -> thm list * thm list -> thm list * thm list
    11   val add_extra_norm: SMT_Utils.class * extra_norm -> Context.generic ->
    12     Context.generic
    13   val normalize: Proof.context -> (int * (int option * thm)) list ->
    14     (int * thm) list
    15   val setup: theory -> theory
    16 end
    17 
    18 structure SMT_Normalize: SMT_NORMALIZE =
    19 struct
    20 
    21 structure U = SMT_Utils
    22 structure B = SMT_Builtin
    23 
    24 
    25 (* general theorem normalizations *)
    26 
    27 (** instantiate elimination rules **)
    28  
    29 local
    30   val (cpfalse, cfalse) = `U.mk_cprop (Thm.cterm_of @{theory} @{const False})
    31 
    32   fun inst f ct thm =
    33     let val cv = f (Drule.strip_imp_concl (Thm.cprop_of thm))
    34     in Thm.instantiate ([], [(cv, ct)]) thm end
    35 in
    36 
    37 fun instantiate_elim thm =
    38   (case Thm.concl_of thm of
    39     @{const Trueprop} $ Var (_, @{typ bool}) => inst Thm.dest_arg cfalse thm
    40   | Var _ => inst I cpfalse thm
    41   | _ => thm)
    42 
    43 end
    44 
    45 
    46 (** normalize definitions **)
    47 
    48 fun norm_def thm =
    49   (case Thm.prop_of thm of
    50     @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ _ $ Abs _) =>
    51       norm_def (thm RS @{thm fun_cong})
    52   | Const (@{const_name "=="}, _) $ _ $ Abs _ =>
    53       norm_def (thm RS @{thm meta_eq_to_obj_eq})
    54   | _ => thm)
    55 
    56 
    57 (** atomization **)
    58 
    59 fun atomize_conv ctxt ct =
    60   (case Thm.term_of ct of
    61     @{const "==>"} $ _ $ _ =>
    62       Conv.binop_conv (atomize_conv ctxt) then_conv
    63       Conv.rewr_conv @{thm atomize_imp}
    64   | Const (@{const_name "=="}, _) $ _ $ _ =>
    65       Conv.binop_conv (atomize_conv ctxt) then_conv
    66       Conv.rewr_conv @{thm atomize_eq}
    67   | Const (@{const_name all}, _) $ Abs _ =>
    68       Conv.binder_conv (atomize_conv o snd) ctxt then_conv
    69       Conv.rewr_conv @{thm atomize_all}
    70   | _ => Conv.all_conv) ct
    71 
    72 val setup_atomize =
    73   fold B.add_builtin_fun_ext'' [@{const_name "==>"}, @{const_name "=="},
    74     @{const_name all}, @{const_name Trueprop}]
    75 
    76 
    77 (** unfold special quantifiers **)
    78 
    79 local
    80   val ex1_def = mk_meta_eq @{lemma
    81     "Ex1 = (%P. EX x. P x & (ALL y. P y --> y = x))"
    82     by (rule ext) (simp only: Ex1_def)}
    83 
    84   val ball_def = mk_meta_eq @{lemma "Ball = (%A P. ALL x. x : A --> P x)"
    85     by (rule ext)+ (rule Ball_def)}
    86 
    87   val bex_def = mk_meta_eq @{lemma "Bex = (%A P. EX x. x : A & P x)"
    88     by (rule ext)+ (rule Bex_def)}
    89 
    90   val special_quants = [(@{const_name Ex1}, ex1_def),
    91     (@{const_name Ball}, ball_def), (@{const_name Bex}, bex_def)]
    92   
    93   fun special_quant (Const (n, _)) = AList.lookup (op =) special_quants n
    94     | special_quant _ = NONE
    95 
    96   fun special_quant_conv _ ct =
    97     (case special_quant (Thm.term_of ct) of
    98       SOME thm => Conv.rewr_conv thm
    99     | NONE => Conv.all_conv) ct
   100 in
   101 
   102 fun unfold_special_quants_conv ctxt =
   103   U.if_exists_conv (is_some o special_quant)
   104     (Conv.top_conv special_quant_conv ctxt)
   105 
   106 val setup_unfolded_quants = fold (B.add_builtin_fun_ext'' o fst) special_quants
   107 
   108 end
   109 
   110 
   111 (** trigger inference **)
   112 
   113 local
   114   (*** check trigger syntax ***)
   115 
   116   fun dest_trigger (Const (@{const_name pat}, _) $ _) = SOME true
   117     | dest_trigger (Const (@{const_name nopat}, _) $ _) = SOME false
   118     | dest_trigger _ = NONE
   119 
   120   fun eq_list [] = false
   121     | eq_list (b :: bs) = forall (equal b) bs
   122 
   123   fun proper_trigger t =
   124     t
   125     |> these o try HOLogic.dest_list
   126     |> map (map_filter dest_trigger o these o try HOLogic.dest_list)
   127     |> (fn [] => false | bss => forall eq_list bss)
   128 
   129   fun proper_quant inside f t =
   130     (case t of
   131       Const (@{const_name All}, _) $ Abs (_, _, u) => proper_quant true f u
   132     | Const (@{const_name Ex}, _) $ Abs (_, _, u) => proper_quant true f u
   133     | @{const trigger} $ p $ u =>
   134         (if inside then f p else false) andalso proper_quant false f u
   135     | Abs (_, _, u) => proper_quant false f u
   136     | u1 $ u2 => proper_quant false f u1 andalso proper_quant false f u2
   137     | _ => true)
   138 
   139   fun check_trigger_error ctxt t =
   140     error ("SMT triggers must only occur under quantifier and multipatterns " ^
   141       "must have the same kind: " ^ Syntax.string_of_term ctxt t)
   142 
   143   fun check_trigger_conv ctxt ct =
   144     if proper_quant false proper_trigger (U.term_of ct) then Conv.all_conv ct
   145     else check_trigger_error ctxt (Thm.term_of ct)
   146 
   147 
   148   (*** infer simple triggers ***)
   149 
   150   fun dest_cond_eq ct =
   151     (case Thm.term_of ct of
   152       Const (@{const_name HOL.eq}, _) $ _ $ _ => Thm.dest_binop ct
   153     | @{const HOL.implies} $ _ $ _ => dest_cond_eq (Thm.dest_arg ct)
   154     | _ => raise CTERM ("no equation", [ct]))
   155 
   156   fun get_constrs thy (Type (n, _)) = these (Datatype.get_constrs thy n)
   157     | get_constrs _ _ = []
   158 
   159   fun is_constr thy (n, T) =
   160     let fun match (m, U) = m = n andalso Sign.typ_instance thy (T, U)
   161     in can (the o find_first match o get_constrs thy o Term.body_type) T end
   162 
   163   fun is_constr_pat thy t =
   164     (case Term.strip_comb t of
   165       (Free _, []) => true
   166     | (Const c, ts) => is_constr thy c andalso forall (is_constr_pat thy) ts
   167     | _ => false)
   168 
   169   fun is_simp_lhs ctxt t =
   170     (case Term.strip_comb t of
   171       (Const c, ts as _ :: _) =>
   172         not (B.is_builtin_fun_ext ctxt c ts) andalso
   173         forall (is_constr_pat (ProofContext.theory_of ctxt)) ts
   174     | _ => false)
   175 
   176   fun has_all_vars vs t =
   177     subset (op aconv) (vs, map Free (Term.add_frees t []))
   178 
   179   fun minimal_pats vs ct =
   180     if has_all_vars vs (Thm.term_of ct) then
   181       (case Thm.term_of ct of
   182         _ $ _ =>
   183           (case pairself (minimal_pats vs) (Thm.dest_comb ct) of
   184             ([], []) => [[ct]]
   185           | (ctss, ctss') => union (eq_set (op aconvc)) ctss ctss')
   186       | _ => [])
   187     else []
   188 
   189   fun proper_mpat _ _ _ [] = false
   190     | proper_mpat thy gen u cts =
   191         let
   192           val tps = (op ~~) (`gen (map Thm.term_of cts))
   193           fun some_match u = tps |> exists (fn (t', t) =>
   194             Pattern.matches thy (t', u) andalso not (t aconv u))
   195         in not (Term.exists_subterm some_match u) end
   196 
   197   val pat = U.mk_const_pat @{theory} @{const_name SMT.pat} U.destT1
   198   fun mk_pat ct = Thm.capply (U.instT' ct pat) ct
   199 
   200   fun mk_clist T = pairself (Thm.cterm_of @{theory})
   201     (HOLogic.cons_const T, HOLogic.nil_const T)
   202   fun mk_list (ccons, cnil) f cts = fold_rev (Thm.mk_binop ccons o f) cts cnil
   203   val mk_pat_list = mk_list (mk_clist @{typ SMT.pattern})
   204   val mk_mpat_list = mk_list (mk_clist @{typ "SMT.pattern list"})  
   205   fun mk_trigger ctss = mk_mpat_list (mk_pat_list mk_pat) ctss
   206 
   207   val trigger_eq =
   208     mk_meta_eq @{lemma "p = SMT.trigger t p" by (simp add: trigger_def)}
   209 
   210   fun insert_trigger_conv [] ct = Conv.all_conv ct
   211     | insert_trigger_conv ctss ct =
   212         let val (ctr, cp) = Thm.dest_binop (Thm.rhs_of trigger_eq) ||> rpair ct
   213         in Thm.instantiate ([], [cp, (ctr, mk_trigger ctss)]) trigger_eq end
   214 
   215   fun infer_trigger_eq_conv outer_ctxt (ctxt, cvs) ct =
   216     let
   217       val (lhs, rhs) = dest_cond_eq ct
   218 
   219       val vs = map Thm.term_of cvs
   220       val thy = ProofContext.theory_of ctxt
   221 
   222       fun get_mpats ct =
   223         if is_simp_lhs ctxt (Thm.term_of ct) then minimal_pats vs ct
   224         else []
   225       val gen = Variable.export_terms ctxt outer_ctxt
   226       val filter_mpats = filter (proper_mpat thy gen (Thm.term_of rhs))
   227 
   228     in insert_trigger_conv (filter_mpats (get_mpats lhs)) ct end
   229 
   230   fun has_trigger (@{const SMT.trigger} $ _ $ _) = true
   231     | has_trigger _ = false
   232 
   233   fun try_trigger_conv cv ct =
   234     if U.under_quant has_trigger (U.term_of ct) then Conv.all_conv ct
   235     else Conv.try_conv cv ct
   236 
   237   fun infer_trigger_conv ctxt =
   238     if Config.get ctxt SMT_Config.infer_triggers then
   239       try_trigger_conv (U.under_quant_conv (infer_trigger_eq_conv ctxt) ctxt)
   240     else Conv.all_conv
   241 in
   242 
   243 fun trigger_conv ctxt =
   244   U.prop_conv (check_trigger_conv ctxt then_conv infer_trigger_conv ctxt)
   245 
   246 val setup_trigger = fold B.add_builtin_fun_ext''
   247   [@{const_name SMT.pat}, @{const_name SMT.nopat}, @{const_name SMT.trigger}]
   248 
   249 end
   250 
   251 
   252 (** adding quantifier weights **)
   253 
   254 local
   255   (*** check weight syntax ***)
   256 
   257   val has_no_weight =
   258     not o Term.exists_subterm (fn @{const SMT.weight} => true | _ => false)
   259 
   260   fun is_weight (@{const SMT.weight} $ w $ t) =
   261         (case try HOLogic.dest_number w of
   262           SOME (_, i) => i >= 0 andalso has_no_weight t
   263         | _ => false)
   264     | is_weight t = has_no_weight t
   265 
   266   fun proper_trigger (@{const SMT.trigger} $ _ $ t) = is_weight t
   267     | proper_trigger t = is_weight t 
   268 
   269   fun check_weight_error ctxt t =
   270     error ("SMT weight must be a non-negative number and must only occur " ^
   271       "under the top-most quantifier and an optional trigger: " ^
   272       Syntax.string_of_term ctxt t)
   273 
   274   fun check_weight_conv ctxt ct =
   275     if U.under_quant proper_trigger (U.term_of ct) then Conv.all_conv ct
   276     else check_weight_error ctxt (Thm.term_of ct)
   277 
   278 
   279   (*** insertion of weights ***)
   280 
   281   fun under_trigger_conv cv ct =
   282     (case Thm.term_of ct of
   283       @{const SMT.trigger} $ _ $ _ => Conv.arg_conv cv
   284     | _ => cv) ct
   285 
   286   val weight_eq =
   287     mk_meta_eq @{lemma "p = SMT.weight i p" by (simp add: weight_def)}
   288   fun mk_weight_eq w =
   289     let val cv = Thm.dest_arg1 (Thm.rhs_of weight_eq)
   290     in
   291       Thm.instantiate ([], [(cv, Numeral.mk_cnumber @{ctyp int} w)]) weight_eq
   292     end
   293 
   294   fun add_weight_conv NONE _ = Conv.all_conv
   295     | add_weight_conv (SOME weight) ctxt =
   296         let val cv = Conv.rewr_conv (mk_weight_eq weight)
   297         in U.under_quant_conv (K (under_trigger_conv cv)) ctxt end
   298 in
   299 
   300 fun weight_conv weight ctxt = 
   301   U.prop_conv (check_weight_conv ctxt then_conv add_weight_conv weight ctxt)
   302 
   303 val setup_weight = B.add_builtin_fun_ext'' @{const_name SMT.weight}
   304 
   305 end
   306 
   307 
   308 (** combined general normalizations **)
   309 
   310 fun gen_normalize1_conv ctxt weight =
   311   atomize_conv ctxt then_conv
   312   unfold_special_quants_conv ctxt then_conv
   313   trigger_conv ctxt then_conv
   314   weight_conv weight ctxt
   315 
   316 fun gen_normalize1 ctxt weight thm =
   317   thm
   318   |> instantiate_elim
   319   |> norm_def
   320   |> Conv.fconv_rule (Thm.beta_conversion true then_conv Thm.eta_conversion)
   321   |> Drule.forall_intr_vars
   322   |> Conv.fconv_rule (gen_normalize1_conv ctxt weight)
   323 
   324 fun drop_fact_warning ctxt =
   325   let val pre = prefix "Warning: dropping assumption: "
   326   in SMT_Config.verbose_msg ctxt (pre o Display.string_of_thm ctxt) end
   327 
   328 fun gen_norm1_safe ctxt (i, (weight, thm)) =
   329   if Config.get ctxt SMT_Config.drop_bad_facts then
   330     (case try (gen_normalize1 ctxt weight) thm of
   331       SOME thm' => SOME (i, thm')
   332     | NONE => (drop_fact_warning ctxt thm; NONE))
   333   else SOME (i, gen_normalize1 ctxt weight thm)
   334 
   335 fun gen_normalize ctxt iwthms = map_filter (gen_norm1_safe ctxt) iwthms
   336 
   337 
   338 
   339 (* unfolding of definitions and theory-specific rewritings *)
   340 
   341 (** unfold trivial distincts **)
   342 
   343 local
   344   fun is_trivial_distinct (Const (@{const_name distinct}, _) $ t) =
   345         (case try HOLogic.dest_list t of
   346           SOME [] => true
   347         | SOME [_] => true
   348         | _ => false)
   349     | is_trivial_distinct _ = false
   350 
   351   val thms = map mk_meta_eq @{lemma
   352     "distinct [] = True"
   353     "distinct [x] = True"
   354     "distinct [x, y] = (x ~= y)"
   355     by simp_all}
   356   fun distinct_conv _ =
   357     U.if_true_conv is_trivial_distinct (Conv.rewrs_conv thms)
   358 in
   359 
   360 fun trivial_distinct_conv ctxt = U.if_exists_conv is_trivial_distinct
   361   (Conv.top_conv distinct_conv ctxt)
   362 
   363 end
   364 
   365 
   366 (** rewrite bool case expressions as if expressions **)
   367 
   368 local
   369   fun is_bool_case (Const (@{const_name "bool.bool_case"}, _)) = true
   370     | is_bool_case _ = false
   371 
   372   val thm = mk_meta_eq @{lemma
   373     "bool_case = (%x y P. if P then x else y)" by (rule ext)+ simp}
   374 
   375   fun unfold_conv _ = U.if_true_conv is_bool_case (Conv.rewr_conv thm)
   376 in
   377 
   378 fun rewrite_bool_case_conv ctxt = U.if_exists_conv is_bool_case
   379   (Conv.top_conv unfold_conv ctxt)
   380 
   381 val setup_bool_case = B.add_builtin_fun_ext'' @{const_name "bool.bool_case"}
   382 
   383 end
   384 
   385 
   386 (** unfold abs, min and max **)
   387 
   388 local
   389   val abs_def = mk_meta_eq @{lemma
   390     "abs = (%a::'a::abs_if. if a < 0 then - a else a)"
   391     by (rule ext) (rule abs_if)}
   392 
   393   val min_def = mk_meta_eq @{lemma "min = (%a b. if a <= b then a else b)"
   394     by (rule ext)+ (rule min_def)}
   395 
   396   val max_def = mk_meta_eq  @{lemma "max = (%a b. if a <= b then b else a)"
   397     by (rule ext)+ (rule max_def)}
   398 
   399   val defs = [(@{const_name min}, min_def), (@{const_name max}, max_def),
   400     (@{const_name abs}, abs_def)]
   401 
   402   fun is_builtinT ctxt T = B.is_builtin_typ_ext ctxt (Term.domain_type T)
   403 
   404   fun abs_min_max ctxt (Const (n, T)) =
   405         (case AList.lookup (op =) defs n of
   406           NONE => NONE
   407         | SOME thm => if is_builtinT ctxt T then SOME thm else NONE)
   408     | abs_min_max _ _ = NONE
   409 
   410   fun unfold_amm_conv ctxt ct =
   411     (case abs_min_max ctxt (Thm.term_of ct) of
   412       SOME thm => Conv.rewr_conv thm
   413     | NONE => Conv.all_conv) ct
   414 in
   415 
   416 fun unfold_abs_min_max_conv ctxt =
   417   U.if_exists_conv (is_some o abs_min_max ctxt)
   418     (Conv.top_conv unfold_amm_conv ctxt)
   419   
   420 val setup_abs_min_max = fold (B.add_builtin_fun_ext'' o fst) defs
   421 
   422 end
   423 
   424 
   425 (** embedding of standard natural number operations into integer operations **)
   426 
   427 local
   428   val nat_embedding = @{lemma
   429     "ALL n. nat (int n) = n"
   430     "ALL i. i >= 0 --> int (nat i) = i"
   431     "ALL i. i < 0 --> int (nat i) = 0"
   432     by simp_all}
   433 
   434   val nat_ops = [
   435     @{const less (nat)}, @{const less_eq (nat)},
   436     @{const Suc}, @{const plus (nat)}, @{const minus (nat)},
   437     @{const times (nat)}, @{const div (nat)}, @{const mod (nat)}]
   438 
   439   val nat_consts = nat_ops @ [@{const number_of (nat)},
   440     @{const zero_class.zero (nat)}, @{const one_class.one (nat)}]
   441 
   442   val nat_int_coercions = [@{const of_nat (int)}, @{const nat}]
   443 
   444   val nat_ops' = nat_int_coercions @ nat_ops
   445 
   446   val is_nat_const = member (op aconv) nat_consts
   447 
   448   val expands = map mk_meta_eq @{lemma
   449     "0 = nat 0"
   450     "1 = nat 1"
   451     "(number_of :: int => nat) = (%i. nat (number_of i))"
   452     "op < = (%a b. int a < int b)"
   453     "op <= = (%a b. int a <= int b)"
   454     "Suc = (%a. nat (int a + 1))"
   455     "op + = (%a b. nat (int a + int b))"
   456     "op - = (%a b. nat (int a - int b))"
   457     "op * = (%a b. nat (int a * int b))"
   458     "op div = (%a b. nat (int a div int b))"
   459     "op mod = (%a b. nat (int a mod int b))"
   460     by (auto intro!: ext simp add: nat_mult_distrib nat_div_distrib
   461       nat_mod_distrib)}
   462 
   463   val ints = map mk_meta_eq @{lemma
   464     "int 0 = 0"
   465     "int 1 = 1"
   466     "int (Suc n) = int n + 1"
   467     "int (n + m) = int n + int m"
   468     "int (n - m) = int (nat (int n - int m))"
   469     "int (n * m) = int n * int m"
   470     "int (n div m) = int n div int m"
   471     "int (n mod m) = int n mod int m"
   472     "int (if P then n else m) = (if P then int n else int m)"
   473     by (auto simp add: int_mult zdiv_int zmod_int)}
   474 
   475   fun mk_number_eq ctxt i lhs =
   476     let
   477       val eq = U.mk_cequals lhs (Numeral.mk_cnumber @{ctyp int} i)
   478       val ss = HOL_ss
   479         addsimps [@{thm Nat_Numeral.int_nat_number_of}]
   480         addsimps @{thms neg_simps}
   481       fun tac _ = Simplifier.simp_tac (Simplifier.context ctxt ss) 1       
   482     in Goal.norm_result (Goal.prove_internal [] eq tac) end
   483 
   484   fun expand_head_conv cv ct =
   485     (case Thm.term_of ct of
   486       _ $ _ =>
   487         Conv.fun_conv (expand_head_conv cv) then_conv
   488         Thm.beta_conversion false
   489     | _ => cv) ct
   490 
   491   fun int_conv ctxt ct =
   492     (case Thm.term_of ct of
   493       @{const of_nat (int)} $ (n as (@{const number_of (nat)} $ _)) =>
   494         Conv.rewr_conv (mk_number_eq ctxt (snd (HOLogic.dest_number n)) ct)
   495     | @{const of_nat (int)} $ _ =>
   496         (Conv.rewrs_conv ints then_conv Conv.sub_conv ints_conv ctxt) else_conv
   497         Conv.top_sweep_conv nat_conv ctxt        
   498     | _ => Conv.no_conv) ct
   499 
   500   and ints_conv ctxt = Conv.top_sweep_conv int_conv ctxt
   501 
   502   and expand_conv ctxt =
   503     U.if_conv (not o is_nat_const o Term.head_of) Conv.no_conv
   504       (expand_head_conv (Conv.rewrs_conv expands) then_conv ints_conv ctxt)
   505 
   506   and nat_conv ctxt = U.if_exists_conv is_nat_const
   507     (Conv.top_sweep_conv expand_conv ctxt)
   508 
   509   val uses_nat_int = Term.exists_subterm (member (op aconv) nat_int_coercions)
   510 in
   511 
   512 val nat_as_int_conv = nat_conv
   513 
   514 fun add_nat_embedding thms =
   515   if exists (uses_nat_int o Thm.prop_of) thms then (thms, nat_embedding)
   516   else (thms, [])
   517 
   518 val setup_nat_as_int =
   519   B.add_builtin_typ_ext (@{typ nat}, K true) #>
   520   fold (B.add_builtin_fun_ext' o Term.dest_Const) nat_ops'
   521 
   522 end
   523 
   524 
   525 (** normalize numerals **)
   526 
   527 local
   528   (*
   529     rewrite negative numerals into positive numerals,
   530     rewrite Numeral0 into 0
   531     rewrite Numeral1 into 1
   532   *)
   533 
   534   fun is_strange_number ctxt (t as Const (@{const_name number_of}, _) $ _) =
   535         (case try HOLogic.dest_number t of
   536           SOME (_, i) => B.is_builtin_num ctxt t andalso i < 2
   537         | NONE => false)
   538     | is_strange_number _ _ = false
   539 
   540   val pos_num_ss = HOL_ss
   541     addsimps [@{thm Int.number_of_minus}, @{thm Int.number_of_Min}]
   542     addsimps [@{thm Int.number_of_Pls}, @{thm Int.numeral_1_eq_1}]
   543     addsimps @{thms Int.pred_bin_simps}
   544     addsimps @{thms Int.normalize_bin_simps}
   545     addsimps @{lemma
   546       "Int.Min = - Int.Bit1 Int.Pls"
   547       "Int.Bit0 (- Int.Pls) = - Int.Pls"
   548       "Int.Bit0 (- k) = - Int.Bit0 k"
   549       "Int.Bit1 (- k) = - Int.Bit1 (Int.pred k)"
   550       by simp_all (simp add: pred_def)}
   551 
   552   fun norm_num_conv ctxt = U.if_conv (is_strange_number ctxt)
   553     (Simplifier.rewrite (Simplifier.context ctxt pos_num_ss)) Conv.no_conv
   554 in
   555 
   556 fun normalize_numerals_conv ctxt = U.if_exists_conv (is_strange_number ctxt)
   557   (Conv.top_sweep_conv norm_num_conv ctxt)
   558 
   559 end
   560 
   561 
   562 (** combined unfoldings and rewritings **)
   563 
   564 fun unfold_conv ctxt =
   565   trivial_distinct_conv ctxt then_conv
   566   rewrite_bool_case_conv ctxt then_conv
   567   unfold_abs_min_max_conv ctxt then_conv
   568   nat_as_int_conv ctxt then_conv
   569   normalize_numerals_conv ctxt then_conv
   570   Thm.beta_conversion true
   571 
   572 fun burrow_ids f ithms =
   573   let
   574     val (is, thms) = split_list ithms
   575     val (thms', extra_thms) = f thms
   576   in (is ~~ thms') @ map (pair ~1) extra_thms end
   577 
   578 fun unfold ctxt =
   579   burrow_ids (map (Conv.fconv_rule (unfold_conv ctxt)) #> add_nat_embedding)
   580 
   581 
   582 
   583 (* overall normalization *)
   584 
   585 type extra_norm = Proof.context -> thm list * thm list -> thm list * thm list
   586 
   587 structure Extra_Norms = Generic_Data
   588 (
   589   type T = extra_norm U.dict
   590   val empty = []
   591   val extend = I
   592   fun merge xx = U.dict_merge fst xx
   593 )
   594 
   595 fun add_extra_norm (cs, norm) = Extra_Norms.map (U.dict_update (cs, norm))
   596 
   597 fun apply_extra_norms ctxt =
   598   let
   599     val cs = SMT_Config.solver_class_of ctxt
   600     val es = U.dict_lookup (Extra_Norms.get (Context.Proof ctxt)) cs
   601   in burrow_ids (fold (fn e => e ctxt) es o rpair []) end
   602 
   603 fun normalize ctxt iwthms =
   604   iwthms
   605   |> gen_normalize ctxt
   606   |> unfold ctxt
   607   |> apply_extra_norms ctxt
   608 
   609 val setup = Context.theory_map (
   610   setup_atomize #>
   611   setup_unfolded_quants #>
   612   setup_trigger #>
   613   setup_weight #>
   614   setup_bool_case #>
   615   setup_abs_min_max #>
   616   setup_nat_as_int)
   617 
   618 end