src/HOL/Tools/SMT/smt_normalize.ML
author boehmes
Tue Mar 27 17:11:02 2012 +0200 (2012-03-27)
changeset 47155 ade3fc826af3
parent 47108 2a1953f0d20d
child 47207 9368aa814518
permissions -rw-r--r--
dropped support for List.distinct in binding to SMT solvers: only few applications benefited from this support, and in some cases the smt method fails due to its support for List.distinct
     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: (int * (int option * thm)) list -> Proof.context ->
    14     (int * thm) list * Proof.context
    15   val setup: theory -> theory
    16 end
    17 
    18 structure SMT_Normalize: SMT_NORMALIZE =
    19 struct
    20 
    21 
    22 (* general theorem normalizations *)
    23 
    24 (** instantiate elimination rules **)
    25  
    26 local
    27   val (cpfalse, cfalse) =
    28     `SMT_Utils.mk_cprop (Thm.cterm_of @{theory} @{const False})
    29 
    30   fun inst f ct thm =
    31     let val cv = f (Drule.strip_imp_concl (Thm.cprop_of thm))
    32     in Thm.instantiate ([], [(cv, ct)]) thm end
    33 in
    34 
    35 fun instantiate_elim thm =
    36   (case Thm.concl_of thm of
    37     @{const Trueprop} $ Var (_, @{typ bool}) => inst Thm.dest_arg cfalse thm
    38   | Var _ => inst I cpfalse thm
    39   | _ => thm)
    40 
    41 end
    42 
    43 
    44 (** normalize definitions **)
    45 
    46 fun norm_def thm =
    47   (case Thm.prop_of thm of
    48     @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ _ $ Abs _) =>
    49       norm_def (thm RS @{thm fun_cong})
    50   | Const (@{const_name "=="}, _) $ _ $ Abs _ =>
    51       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 "==>"} $ _ $ _ =>
    60       Conv.binop_conv (atomize_conv ctxt) then_conv
    61       Conv.rewr_conv @{thm atomize_imp}
    62   | Const (@{const_name "=="}, _) $ _ $ _ =>
    63       Conv.binop_conv (atomize_conv ctxt) then_conv
    64       Conv.rewr_conv @{thm atomize_eq}
    65   | Const (@{const_name all}, _) $ Abs _ =>
    66       Conv.binder_conv (atomize_conv o snd) ctxt then_conv
    67       Conv.rewr_conv @{thm atomize_all}
    68   | _ => Conv.all_conv) ct
    69 
    70 val setup_atomize =
    71   fold SMT_Builtin.add_builtin_fun_ext'' [@{const_name "==>"},
    72     @{const_name "=="}, @{const_name all}, @{const_name Trueprop}]
    73 
    74 
    75 (** unfold special quantifiers **)
    76 
    77 local
    78   val ex1_def = mk_meta_eq @{lemma
    79     "Ex1 = (%P. EX x. P x & (ALL y. P y --> y = x))"
    80     by (rule ext) (simp only: Ex1_def)}
    81 
    82   val ball_def = mk_meta_eq @{lemma "Ball = (%A P. ALL x. x : A --> P x)"
    83     by (rule ext)+ (rule Ball_def)}
    84 
    85   val bex_def = mk_meta_eq @{lemma "Bex = (%A P. EX x. x : A & P x)"
    86     by (rule ext)+ (rule Bex_def)}
    87 
    88   val special_quants = [(@{const_name Ex1}, ex1_def),
    89     (@{const_name Ball}, ball_def), (@{const_name Bex}, bex_def)]
    90   
    91   fun special_quant (Const (n, _)) = AList.lookup (op =) special_quants n
    92     | special_quant _ = NONE
    93 
    94   fun special_quant_conv _ ct =
    95     (case special_quant (Thm.term_of ct) of
    96       SOME thm => Conv.rewr_conv thm
    97     | NONE => Conv.all_conv) ct
    98 in
    99 
   100 fun unfold_special_quants_conv ctxt =
   101   SMT_Utils.if_exists_conv (is_some o special_quant)
   102     (Conv.top_conv special_quant_conv ctxt)
   103 
   104 val setup_unfolded_quants =
   105   fold (SMT_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 (SMT_Utils.term_of ct) then
   144       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 (SMT_Builtin.is_builtin_fun_ext ctxt c ts) andalso
   173         forall (is_constr_pat (Proof_Context.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 =
   198     SMT_Utils.mk_const_pat @{theory} @{const_name SMT.pat} SMT_Utils.destT1
   199   fun mk_pat ct = Thm.apply (SMT_Utils.instT' ct pat) ct
   200 
   201   fun mk_clist T = pairself (Thm.cterm_of @{theory})
   202     (HOLogic.cons_const T, HOLogic.nil_const T)
   203   fun mk_list (ccons, cnil) f cts = fold_rev (Thm.mk_binop ccons o f) cts cnil
   204   val mk_pat_list = mk_list (mk_clist @{typ SMT.pattern})
   205   val mk_mpat_list = mk_list (mk_clist @{typ "SMT.pattern list"})  
   206   fun mk_trigger ctss = mk_mpat_list (mk_pat_list mk_pat) ctss
   207 
   208   val trigger_eq =
   209     mk_meta_eq @{lemma "p = SMT.trigger t p" by (simp add: trigger_def)}
   210 
   211   fun insert_trigger_conv [] ct = Conv.all_conv ct
   212     | insert_trigger_conv ctss ct =
   213         let val (ctr, cp) = Thm.dest_binop (Thm.rhs_of trigger_eq) ||> rpair ct
   214         in Thm.instantiate ([], [cp, (ctr, mk_trigger ctss)]) trigger_eq end
   215 
   216   fun infer_trigger_eq_conv outer_ctxt (ctxt, cvs) ct =
   217     let
   218       val (lhs, rhs) = dest_cond_eq ct
   219 
   220       val vs = map Thm.term_of cvs
   221       val thy = Proof_Context.theory_of ctxt
   222 
   223       fun get_mpats ct =
   224         if is_simp_lhs ctxt (Thm.term_of ct) then minimal_pats vs ct
   225         else []
   226       val gen = Variable.export_terms ctxt outer_ctxt
   227       val filter_mpats = filter (proper_mpat thy gen (Thm.term_of rhs))
   228 
   229     in insert_trigger_conv (filter_mpats (get_mpats lhs)) ct end
   230 
   231   fun has_trigger (@{const SMT.trigger} $ _ $ _) = true
   232     | has_trigger _ = false
   233 
   234   fun try_trigger_conv cv ct =
   235     if SMT_Utils.under_quant has_trigger (SMT_Utils.term_of ct) then
   236       Conv.all_conv ct
   237     else Conv.try_conv cv ct
   238 
   239   fun infer_trigger_conv ctxt =
   240     if Config.get ctxt SMT_Config.infer_triggers then
   241       try_trigger_conv
   242         (SMT_Utils.under_quant_conv (infer_trigger_eq_conv ctxt) ctxt)
   243     else Conv.all_conv
   244 in
   245 
   246 fun trigger_conv ctxt =
   247   SMT_Utils.prop_conv
   248     (check_trigger_conv ctxt then_conv infer_trigger_conv ctxt)
   249 
   250 val setup_trigger =
   251   fold SMT_Builtin.add_builtin_fun_ext''
   252     [@{const_name SMT.pat}, @{const_name SMT.nopat}, @{const_name SMT.trigger}]
   253 
   254 end
   255 
   256 
   257 (** adding quantifier weights **)
   258 
   259 local
   260   (*** check weight syntax ***)
   261 
   262   val has_no_weight =
   263     not o Term.exists_subterm (fn @{const SMT.weight} => true | _ => false)
   264 
   265   fun is_weight (@{const SMT.weight} $ w $ t) =
   266         (case try HOLogic.dest_number w of
   267           SOME (_, i) => i >= 0 andalso has_no_weight t
   268         | _ => false)
   269     | is_weight t = has_no_weight t
   270 
   271   fun proper_trigger (@{const SMT.trigger} $ _ $ t) = is_weight t
   272     | proper_trigger t = is_weight t 
   273 
   274   fun check_weight_error ctxt t =
   275     error ("SMT weight must be a non-negative number and must only occur " ^
   276       "under the top-most quantifier and an optional trigger: " ^
   277       Syntax.string_of_term ctxt t)
   278 
   279   fun check_weight_conv ctxt ct =
   280     if SMT_Utils.under_quant proper_trigger (SMT_Utils.term_of ct) then
   281       Conv.all_conv ct
   282     else check_weight_error ctxt (Thm.term_of ct)
   283 
   284 
   285   (*** insertion of weights ***)
   286 
   287   fun under_trigger_conv cv ct =
   288     (case Thm.term_of ct of
   289       @{const SMT.trigger} $ _ $ _ => Conv.arg_conv cv
   290     | _ => cv) ct
   291 
   292   val weight_eq =
   293     mk_meta_eq @{lemma "p = SMT.weight i p" by (simp add: weight_def)}
   294   fun mk_weight_eq w =
   295     let val cv = Thm.dest_arg1 (Thm.rhs_of weight_eq)
   296     in
   297       Thm.instantiate ([], [(cv, Numeral.mk_cnumber @{ctyp int} w)]) weight_eq
   298     end
   299 
   300   fun add_weight_conv NONE _ = Conv.all_conv
   301     | add_weight_conv (SOME weight) ctxt =
   302         let val cv = Conv.rewr_conv (mk_weight_eq weight)
   303         in SMT_Utils.under_quant_conv (K (under_trigger_conv cv)) ctxt end
   304 in
   305 
   306 fun weight_conv weight ctxt = 
   307   SMT_Utils.prop_conv
   308     (check_weight_conv ctxt then_conv add_weight_conv weight ctxt)
   309 
   310 val setup_weight = SMT_Builtin.add_builtin_fun_ext'' @{const_name SMT.weight}
   311 
   312 end
   313 
   314 
   315 (** combined general normalizations **)
   316 
   317 fun gen_normalize1_conv ctxt weight =
   318   atomize_conv ctxt then_conv
   319   unfold_special_quants_conv ctxt then_conv
   320   Thm.beta_conversion true then_conv
   321   trigger_conv ctxt then_conv
   322   weight_conv weight ctxt
   323 
   324 fun gen_normalize1 ctxt weight thm =
   325   thm
   326   |> instantiate_elim
   327   |> norm_def
   328   |> Conv.fconv_rule (Thm.beta_conversion true then_conv Thm.eta_conversion)
   329   |> Drule.forall_intr_vars
   330   |> Conv.fconv_rule (gen_normalize1_conv ctxt weight)
   331 
   332 fun drop_fact_warning ctxt =
   333   let val pre = prefix "Warning: dropping assumption: "
   334   in SMT_Config.verbose_msg ctxt (pre o Display.string_of_thm ctxt) end
   335 
   336 fun gen_norm1_safe ctxt (i, (weight, thm)) =
   337   if Config.get ctxt SMT_Config.drop_bad_facts then
   338     (case try (gen_normalize1 ctxt weight) thm of
   339       SOME thm' => SOME (i, thm')
   340     | NONE => (drop_fact_warning ctxt thm; NONE))
   341   else SOME (i, gen_normalize1 ctxt weight thm)
   342 
   343 fun gen_normalize ctxt iwthms = map_filter (gen_norm1_safe ctxt) iwthms
   344 
   345 
   346 
   347 (* unfolding of definitions and theory-specific rewritings *)
   348 
   349 (** rewrite bool case expressions as if expressions **)
   350 
   351 local
   352   fun is_bool_case (Const (@{const_name "bool.bool_case"}, _)) = true
   353     | is_bool_case _ = false
   354 
   355   val thm = mk_meta_eq @{lemma
   356     "bool_case = (%x y P. if P then x else y)" by (rule ext)+ simp}
   357 
   358   fun unfold_conv _ = SMT_Utils.if_true_conv is_bool_case (Conv.rewr_conv thm)
   359 in
   360 
   361 fun rewrite_bool_case_conv ctxt =
   362   SMT_Utils.if_exists_conv is_bool_case (Conv.top_conv unfold_conv ctxt)
   363 
   364 val setup_bool_case =
   365   SMT_Builtin.add_builtin_fun_ext'' @{const_name "bool.bool_case"}
   366 
   367 end
   368 
   369 
   370 (** unfold abs, min and max **)
   371 
   372 local
   373   val abs_def = mk_meta_eq @{lemma
   374     "abs = (%a::'a::abs_if. if a < 0 then - a else a)"
   375     by (rule ext) (rule abs_if)}
   376 
   377   val min_def = mk_meta_eq @{lemma "min = (%a b. if a <= b then a else b)"
   378     by (rule ext)+ (rule min_def)}
   379 
   380   val max_def = mk_meta_eq  @{lemma "max = (%a b. if a <= b then b else a)"
   381     by (rule ext)+ (rule max_def)}
   382 
   383   val defs = [(@{const_name min}, min_def), (@{const_name max}, max_def),
   384     (@{const_name abs}, abs_def)]
   385 
   386   fun is_builtinT ctxt T =
   387     SMT_Builtin.is_builtin_typ_ext ctxt (Term.domain_type T)
   388 
   389   fun abs_min_max ctxt (Const (n, T)) =
   390         (case AList.lookup (op =) defs n of
   391           NONE => NONE
   392         | SOME thm => if is_builtinT ctxt T then SOME thm else NONE)
   393     | abs_min_max _ _ = NONE
   394 
   395   fun unfold_amm_conv ctxt ct =
   396     (case abs_min_max ctxt (Thm.term_of ct) of
   397       SOME thm => Conv.rewr_conv thm
   398     | NONE => Conv.all_conv) ct
   399 in
   400 
   401 fun unfold_abs_min_max_conv ctxt =
   402   SMT_Utils.if_exists_conv (is_some o abs_min_max ctxt)
   403     (Conv.top_conv unfold_amm_conv ctxt)
   404   
   405 val setup_abs_min_max = fold (SMT_Builtin.add_builtin_fun_ext'' o fst) defs
   406 
   407 end
   408 
   409 
   410 (** embedding of standard natural number operations into integer operations **)
   411 
   412 local
   413   val nat_embedding = @{lemma
   414     "ALL n. nat (int n) = n"
   415     "ALL i. i >= 0 --> int (nat i) = i"
   416     "ALL i. i < 0 --> int (nat i) = 0"
   417     by simp_all}
   418 
   419   val simple_nat_ops = [
   420     @{const less (nat)}, @{const less_eq (nat)},
   421     @{const Suc}, @{const plus (nat)}, @{const minus (nat)}]
   422 
   423   val mult_nat_ops =
   424     [@{const times (nat)}, @{const div (nat)}, @{const mod (nat)}]
   425 
   426   val nat_ops = simple_nat_ops @ mult_nat_ops
   427 
   428   val nat_consts = nat_ops @ [@{const numeral (nat)},
   429     @{const zero_class.zero (nat)}, @{const one_class.one (nat)}]
   430 
   431   val nat_int_coercions = [@{const of_nat (int)}, @{const nat}]
   432 
   433   val builtin_nat_ops = nat_int_coercions @ simple_nat_ops
   434 
   435   val is_nat_const = member (op aconv) nat_consts
   436 
   437   fun is_nat_const' @{const of_nat (int)} = true
   438     | is_nat_const' t = is_nat_const t
   439 
   440   val expands = map mk_meta_eq @{lemma
   441     "0 = nat 0"
   442     "1 = nat 1"
   443     "(numeral :: num => nat) = (%i. nat (numeral i))"
   444     "op < = (%a b. int a < int b)"
   445     "op <= = (%a b. int a <= int b)"
   446     "Suc = (%a. nat (int a + 1))"
   447     "op + = (%a b. nat (int a + int b))"
   448     "op - = (%a b. nat (int a - int b))"
   449     "op * = (%a b. nat (int a * int b))"
   450     "op div = (%a b. nat (int a div int b))"
   451     "op mod = (%a b. nat (int a mod int b))"
   452     by (fastforce simp add: nat_mult_distrib nat_div_distrib nat_mod_distrib)+}
   453 
   454   val ints = map mk_meta_eq @{lemma
   455     "int 0 = 0"
   456     "int 1 = 1"
   457     "int (Suc n) = int n + 1"
   458     "int (n + m) = int n + int m"
   459     "int (n - m) = int (nat (int n - int m))"
   460     "int (n * m) = int n * int m"
   461     "int (n div m) = int n div int m"
   462     "int (n mod m) = int n mod int m"
   463     "int (if P then n else m) = (if P then int n else int m)"
   464     by (auto simp add: int_mult zdiv_int zmod_int)}
   465 
   466   fun mk_number_eq ctxt i lhs =
   467     let
   468       val eq = SMT_Utils.mk_cequals lhs (Numeral.mk_cnumber @{ctyp int} i)
   469       val ss = HOL_ss
   470         addsimps [@{thm Nat_Numeral.int_numeral}]
   471       fun tac _ = Simplifier.simp_tac (Simplifier.context ctxt ss) 1       
   472     in Goal.norm_result (Goal.prove_internal [] eq tac) end
   473 
   474   fun expand_head_conv cv ct =
   475     (case Thm.term_of ct of
   476       _ $ _ =>
   477         Conv.fun_conv (expand_head_conv cv) then_conv
   478         Thm.beta_conversion false
   479     | _ => cv) ct
   480 
   481   fun int_conv ctxt ct =
   482     (case Thm.term_of ct of
   483       @{const of_nat (int)} $ (n as (@{const numeral (nat)} $ _)) =>
   484         Conv.rewr_conv (mk_number_eq ctxt (snd (HOLogic.dest_number n)) ct)
   485     | @{const of_nat (int)} $ _ =>
   486         (Conv.rewrs_conv ints then_conv Conv.sub_conv ints_conv ctxt) else_conv
   487         Conv.sub_conv (Conv.top_sweep_conv nat_conv) ctxt        
   488     | _ => Conv.no_conv) ct
   489 
   490   and ints_conv ctxt = Conv.top_sweep_conv int_conv ctxt
   491 
   492   and expand_conv ctxt =
   493     SMT_Utils.if_conv (is_nat_const o Term.head_of)
   494       (expand_head_conv (Conv.rewrs_conv expands) then_conv ints_conv ctxt)
   495       (int_conv ctxt)
   496 
   497   and nat_conv ctxt = SMT_Utils.if_exists_conv is_nat_const'
   498     (Conv.top_sweep_conv expand_conv ctxt)
   499 
   500   val uses_nat_int = Term.exists_subterm (member (op aconv) nat_int_coercions)
   501 in
   502 
   503 val nat_as_int_conv = nat_conv
   504 
   505 fun add_nat_embedding thms =
   506   if exists (uses_nat_int o Thm.prop_of) thms then (thms, nat_embedding)
   507   else (thms, [])
   508 
   509 val setup_nat_as_int =
   510   SMT_Builtin.add_builtin_typ_ext (@{typ nat}, K true) #>
   511   fold (SMT_Builtin.add_builtin_fun_ext' o Term.dest_Const) builtin_nat_ops
   512 
   513 end
   514 
   515 
   516 (** normalize numerals **)
   517 
   518 local
   519   (*
   520     rewrite negative numerals into positive numerals,
   521     rewrite Numeral0 into 0
   522     rewrite Numeral1 into 1
   523   *)
   524 
   525   fun is_strange_number ctxt (t as Const (@{const_name neg_numeral}, _) $ _) =
   526         (case try HOLogic.dest_number t of
   527           SOME (_, i) => SMT_Builtin.is_builtin_num ctxt t andalso i < 2
   528         | NONE => false)
   529     | is_strange_number _ _ = false
   530 
   531   val pos_num_ss = HOL_ss
   532     addsimps [@{thm Num.numeral_One}]
   533     addsimps [@{thm Num.neg_numeral_def}]
   534 
   535   fun norm_num_conv ctxt =
   536     SMT_Utils.if_conv (is_strange_number ctxt)
   537       (Simplifier.rewrite (Simplifier.context ctxt pos_num_ss)) Conv.no_conv
   538 in
   539 
   540 fun normalize_numerals_conv ctxt =
   541   SMT_Utils.if_exists_conv (is_strange_number ctxt)
   542     (Conv.top_sweep_conv norm_num_conv ctxt)
   543 
   544 end
   545 
   546 
   547 (** combined unfoldings and rewritings **)
   548 
   549 fun unfold_conv ctxt =
   550   rewrite_bool_case_conv ctxt then_conv
   551   unfold_abs_min_max_conv ctxt then_conv
   552   nat_as_int_conv ctxt then_conv
   553   Thm.beta_conversion true
   554 
   555 fun unfold1 ctxt = map (apsnd (Conv.fconv_rule (unfold_conv ctxt)))
   556 
   557 fun burrow_ids f ithms =
   558   let
   559     val (is, thms) = split_list ithms
   560     val (thms', extra_thms) = f thms
   561   in (is ~~ thms') @ map (pair ~1) extra_thms end
   562 
   563 fun unfold2 ithms ctxt =
   564   ithms
   565   |> map (apsnd (Conv.fconv_rule (normalize_numerals_conv ctxt)))
   566   |> burrow_ids add_nat_embedding
   567   |> rpair ctxt
   568 
   569 
   570 
   571 (* overall normalization *)
   572 
   573 type extra_norm = Proof.context -> thm list * thm list -> thm list * thm list
   574 
   575 structure Extra_Norms = Generic_Data
   576 (
   577   type T = extra_norm SMT_Utils.dict
   578   val empty = []
   579   val extend = I
   580   fun merge data = SMT_Utils.dict_merge fst data
   581 )
   582 
   583 fun add_extra_norm (cs, norm) =
   584   Extra_Norms.map (SMT_Utils.dict_update (cs, norm))
   585 
   586 fun apply_extra_norms ithms ctxt =
   587   let
   588     val cs = SMT_Config.solver_class_of ctxt
   589     val es = SMT_Utils.dict_lookup (Extra_Norms.get (Context.Proof ctxt)) cs
   590   in (burrow_ids (fold (fn e => e ctxt) es o rpair []) ithms, ctxt) end
   591 
   592 local
   593   val ignored = member (op =) [@{const_name All}, @{const_name Ex},
   594     @{const_name Let}, @{const_name If}, @{const_name HOL.eq}]
   595 
   596   val schematic_consts_of =
   597     let
   598       fun collect (@{const SMT.trigger} $ p $ t) =
   599             collect_trigger p #> collect t
   600         | collect (t $ u) = collect t #> collect u
   601         | collect (Abs (_, _, t)) = collect t
   602         | collect (t as Const (n, _)) = 
   603             if not (ignored n) then Monomorph.add_schematic_consts_of t else I
   604         | collect _ = I
   605       and collect_trigger t =
   606         let val dest = these o try HOLogic.dest_list 
   607         in fold (fold collect_pat o dest) (dest t) end
   608       and collect_pat (Const (@{const_name SMT.pat}, _) $ t) = collect t
   609         | collect_pat (Const (@{const_name SMT.nopat}, _) $ t) = collect t
   610         | collect_pat _ = I
   611     in (fn t => collect t Symtab.empty) end
   612 in
   613 
   614 fun monomorph xthms ctxt =
   615   let val (xs, thms) = split_list xthms
   616   in
   617     (map (pair 1) thms, ctxt)
   618     |-> Monomorph.monomorph schematic_consts_of
   619     |>> maps (uncurry (map o pair)) o map2 pair xs o map (map snd)
   620   end
   621 
   622 end
   623 
   624 fun normalize iwthms ctxt =
   625   iwthms
   626   |> gen_normalize ctxt
   627   |> unfold1 ctxt
   628   |> rpair ctxt
   629   |-> monomorph
   630   |-> unfold2
   631   |-> apply_extra_norms
   632 
   633 val setup = Context.theory_map (
   634   setup_atomize #>
   635   setup_unfolded_quants #>
   636   setup_trigger #>
   637   setup_weight #>
   638   setup_bool_case #>
   639   setup_abs_min_max #>
   640   setup_nat_as_int)
   641 
   642 end