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