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