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