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