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