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