src/HOL/Tools/SMT/smt_normalize.ML
author boehmes
Mon Nov 08 12:13:44 2010 +0100 (2010-11-08)
changeset 40424 7550b2cba1cb
parent 40279 96365b4ae7b6
child 40579 98ebd2300823
permissions -rw-r--r--
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes@36898
     1
(*  Title:      HOL/Tools/SMT/smt_normalize.ML
boehmes@36898
     2
    Author:     Sascha Boehme, TU Muenchen
boehmes@36898
     3
boehmes@36898
     4
Normalization steps on theorems required by SMT solvers:
boehmes@36898
     5
  * simplify trivial distincts (those with less than three elements),
boehmes@36898
     6
  * rewrite bool case expressions as if expressions,
boehmes@36898
     7
  * normalize numerals (e.g. replace negative numerals by negated positive
boehmes@36898
     8
    numerals),
boehmes@36898
     9
  * embed natural numbers into integers,
boehmes@36898
    10
  * add extra rules specifying types and constants which occur frequently,
boehmes@36898
    11
  * fully translate into object logic, add universal closure,
boehmes@39483
    12
  * monomorphize (create instances of schematic rules),
boehmes@36898
    13
  * lift lambda terms,
boehmes@36898
    14
  * make applications explicit for functions with varying number of arguments.
boehmes@39483
    15
  * add (hypothetical definitions for) missing datatype selectors,
boehmes@36898
    16
*)
boehmes@36898
    17
boehmes@36898
    18
signature SMT_NORMALIZE =
boehmes@36898
    19
sig
boehmes@40162
    20
  type extra_norm = bool -> (int * thm) list -> Proof.context ->
boehmes@40161
    21
    (int * thm) list * Proof.context
boehmes@40424
    22
  val normalize: extra_norm -> bool -> (int * thm) list -> Proof.context ->
boehmes@40161
    23
    (int * thm) list * Proof.context
boehmes@36899
    24
  val atomize_conv: Proof.context -> conv
boehmes@36898
    25
  val eta_expand_conv: (Proof.context -> conv) -> Proof.context -> conv
boehmes@36898
    26
end
boehmes@36898
    27
boehmes@36898
    28
structure SMT_Normalize: SMT_NORMALIZE =
boehmes@36898
    29
struct
boehmes@36898
    30
boehmes@36898
    31
infix 2 ??
boehmes@36898
    32
fun (test ?? f) x = if test x then f x else x
boehmes@36898
    33
boehmes@36898
    34
fun if_conv c cv1 cv2 ct = (if c (Thm.term_of ct) then cv1 else cv2) ct
boehmes@36898
    35
fun if_true_conv c cv = if_conv c cv Conv.all_conv
boehmes@36898
    36
boehmes@36898
    37
boehmes@36898
    38
boehmes@36898
    39
(* simplification of trivial distincts (distinct should have at least
boehmes@36898
    40
   three elements in the argument list) *)
boehmes@36898
    41
boehmes@36898
    42
local
boehmes@40274
    43
  fun is_trivial_distinct (Const (@{const_name SMT.distinct}, _) $ t) =
boehmes@40274
    44
       (length (HOLogic.dest_list t) <= 2
boehmes@40274
    45
        handle TERM _ => error ("SMT: constant " ^
boehmes@40274
    46
          quote @{const_name SMT.distinct} ^ " must be applied to " ^
boehmes@40274
    47
          "an explicit list."))
boehmes@36898
    48
    | is_trivial_distinct _ = false
boehmes@36898
    49
boehmes@37786
    50
  val thms = map mk_meta_eq @{lemma
boehmes@40274
    51
    "SMT.distinct [] = True"
boehmes@40274
    52
    "SMT.distinct [x] = True"
boehmes@40274
    53
    "SMT.distinct [x, y] = (x ~= y)"
boehmes@40274
    54
    by (simp_all add: distinct_def)}
boehmes@36898
    55
  fun distinct_conv _ =
wenzelm@36936
    56
    if_true_conv is_trivial_distinct (Conv.rewrs_conv thms)
boehmes@36898
    57
in
boehmes@36898
    58
fun trivial_distinct ctxt =
boehmes@40161
    59
  map (apsnd ((Term.exists_subterm is_trivial_distinct o Thm.prop_of) ??
boehmes@40161
    60
    Conv.fconv_rule (Conv.top_conv distinct_conv ctxt)))
boehmes@36898
    61
end
boehmes@36898
    62
boehmes@36898
    63
boehmes@36898
    64
boehmes@36898
    65
(* rewrite bool case expressions as if expressions *)
boehmes@36898
    66
boehmes@36898
    67
local
boehmes@36898
    68
  val is_bool_case = (fn
boehmes@36898
    69
      Const (@{const_name "bool.bool_case"}, _) $ _ $ _ $ _ => true
boehmes@36898
    70
    | _ => false)
boehmes@36898
    71
boehmes@40275
    72
  val thm = mk_meta_eq @{lemma
boehmes@40275
    73
    "(case P of True => x | False => y) = (if P then x else y)" by simp}
boehmes@40275
    74
  val unfold_conv = if_true_conv is_bool_case (Conv.rewr_conv thm)
boehmes@36898
    75
in
boehmes@36898
    76
fun rewrite_bool_cases ctxt =
boehmes@40161
    77
  map (apsnd ((Term.exists_subterm is_bool_case o Thm.prop_of) ??
boehmes@40161
    78
    Conv.fconv_rule (Conv.top_conv (K unfold_conv) ctxt)))
boehmes@36898
    79
end
boehmes@36898
    80
boehmes@36898
    81
boehmes@36898
    82
boehmes@36898
    83
(* normalization of numerals: rewriting of negative integer numerals into
boehmes@36898
    84
   positive numerals, Numeral0 into 0, Numeral1 into 1 *)
boehmes@36898
    85
boehmes@36898
    86
local
boehmes@36898
    87
  fun is_number_sort ctxt T =
boehmes@36898
    88
    Sign.of_sort (ProofContext.theory_of ctxt) (T, @{sort number_ring})
boehmes@36898
    89
boehmes@36898
    90
  fun is_strange_number ctxt (t as Const (@{const_name number_of}, _) $ _) =
boehmes@36898
    91
        (case try HOLogic.dest_number t of
boehmes@36898
    92
          SOME (T, i) => is_number_sort ctxt T andalso i < 2
boehmes@36898
    93
        | NONE => false)
boehmes@36898
    94
    | is_strange_number _ _ = false
boehmes@36898
    95
boehmes@36898
    96
  val pos_numeral_ss = HOL_ss
boehmes@36898
    97
    addsimps [@{thm Int.number_of_minus}, @{thm Int.number_of_Min}]
boehmes@36898
    98
    addsimps [@{thm Int.number_of_Pls}, @{thm Int.numeral_1_eq_1}]
boehmes@36898
    99
    addsimps @{thms Int.pred_bin_simps}
boehmes@36898
   100
    addsimps @{thms Int.normalize_bin_simps}
boehmes@36898
   101
    addsimps @{lemma
boehmes@36898
   102
      "Int.Min = - Int.Bit1 Int.Pls"
boehmes@36898
   103
      "Int.Bit0 (- Int.Pls) = - Int.Pls"
boehmes@36898
   104
      "Int.Bit0 (- k) = - Int.Bit0 k"
boehmes@36898
   105
      "Int.Bit1 (- k) = - Int.Bit1 (Int.pred k)"
boehmes@36898
   106
      by simp_all (simp add: pred_def)}
boehmes@36898
   107
boehmes@36898
   108
  fun pos_conv ctxt = if_conv (is_strange_number ctxt)
boehmes@36898
   109
    (Simplifier.rewrite (Simplifier.context ctxt pos_numeral_ss))
boehmes@36898
   110
    Conv.no_conv
boehmes@36898
   111
in
boehmes@36898
   112
fun normalize_numerals ctxt =
boehmes@40161
   113
  map (apsnd ((Term.exists_subterm (is_strange_number ctxt) o Thm.prop_of) ??
boehmes@40161
   114
    Conv.fconv_rule (Conv.top_sweep_conv pos_conv ctxt)))
boehmes@36898
   115
end
boehmes@36898
   116
boehmes@36898
   117
boehmes@36898
   118
boehmes@36898
   119
(* embedding of standard natural number operations into integer operations *)
boehmes@36898
   120
boehmes@36898
   121
local
boehmes@40161
   122
  val nat_embedding = map (pair ~1) @{lemma
boehmes@36898
   123
    "nat (int n) = n"
boehmes@36898
   124
    "i >= 0 --> int (nat i) = i"
boehmes@36898
   125
    "i < 0 --> int (nat i) = 0"
boehmes@36898
   126
    by simp_all}
boehmes@36898
   127
boehmes@36898
   128
  val nat_rewriting = @{lemma
boehmes@36898
   129
    "0 = nat 0"
boehmes@36898
   130
    "1 = nat 1"
boehmes@40279
   131
    "(number_of :: int => nat) = (%i. nat (number_of i))"
boehmes@36898
   132
    "int (nat 0) = 0"
boehmes@36898
   133
    "int (nat 1) = 1"
boehmes@40279
   134
    "op < = (%a b. int a < int b)"
boehmes@40279
   135
    "op <= = (%a b. int a <= int b)"
boehmes@40279
   136
    "Suc = (%a. nat (int a + 1))"
boehmes@40279
   137
    "op + = (%a b. nat (int a + int b))"
boehmes@40279
   138
    "op - = (%a b. nat (int a - int b))"
boehmes@40279
   139
    "op * = (%a b. nat (int a * int b))"
boehmes@40279
   140
    "op div = (%a b. nat (int a div int b))"
boehmes@40279
   141
    "op mod = (%a b. nat (int a mod int b))"
boehmes@40279
   142
    "min = (%a b. nat (min (int a) (int b)))"
boehmes@40279
   143
    "max = (%a b. nat (max (int a) (int b)))"
boehmes@36898
   144
    "int (nat (int a + int b)) = int a + int b"
boehmes@40279
   145
    "int (nat (int a + 1)) = int a + 1"  (* special rule due to Suc above *)
boehmes@36898
   146
    "int (nat (int a * int b)) = int a * int b"
boehmes@36898
   147
    "int (nat (int a div int b)) = int a div int b"
boehmes@36898
   148
    "int (nat (int a mod int b)) = int a mod int b"
boehmes@36898
   149
    "int (nat (min (int a) (int b))) = min (int a) (int b)"
boehmes@36898
   150
    "int (nat (max (int a) (int b))) = max (int a) (int b)"
boehmes@40279
   151
    by (auto intro!: ext simp add: nat_mult_distrib nat_div_distrib
boehmes@40279
   152
      nat_mod_distrib int_mult[symmetric] zdiv_int[symmetric]
boehmes@40279
   153
      zmod_int[symmetric])}
boehmes@36898
   154
boehmes@36898
   155
  fun on_positive num f x = 
boehmes@36898
   156
    (case try HOLogic.dest_number (Thm.term_of num) of
boehmes@36898
   157
      SOME (_, i) => if i >= 0 then SOME (f x) else NONE
boehmes@36898
   158
    | NONE => NONE)
boehmes@36898
   159
boehmes@36898
   160
  val cancel_int_nat_ss = HOL_ss
boehmes@36898
   161
    addsimps [@{thm Nat_Numeral.nat_number_of}]
boehmes@36898
   162
    addsimps [@{thm Nat_Numeral.int_nat_number_of}]
boehmes@36898
   163
    addsimps @{thms neg_simps}
boehmes@36898
   164
boehmes@36898
   165
  fun cancel_int_nat_simproc _ ss ct = 
boehmes@36898
   166
    let
boehmes@36898
   167
      val num = Thm.dest_arg (Thm.dest_arg ct)
boehmes@36898
   168
      val goal = Thm.mk_binop @{cterm "op == :: int => _"} ct num
boehmes@36898
   169
      val simpset = Simplifier.inherit_context ss cancel_int_nat_ss
boehmes@36898
   170
      fun tac _ = Simplifier.simp_tac simpset 1
boehmes@36898
   171
    in on_positive num (Goal.prove_internal [] goal) tac end
boehmes@36898
   172
boehmes@36898
   173
  val nat_ss = HOL_ss
boehmes@36898
   174
    addsimps nat_rewriting
boehmes@40279
   175
    addsimprocs [
boehmes@40279
   176
      Simplifier.make_simproc {
boehmes@40279
   177
        name = "cancel_int_nat_num", lhss = [@{cpat "int (nat _)"}],
boehmes@40279
   178
        proc = cancel_int_nat_simproc, identifier = [] }]
boehmes@36898
   179
boehmes@36898
   180
  fun conv ctxt = Simplifier.rewrite (Simplifier.context ctxt nat_ss)
boehmes@36898
   181
boehmes@36898
   182
  val uses_nat_type = Term.exists_type (Term.exists_subtype (equal @{typ nat}))
boehmes@36898
   183
  val uses_nat_int =
boehmes@36898
   184
    Term.exists_subterm (member (op aconv) [@{term int}, @{term nat}])
boehmes@36898
   185
in
boehmes@36898
   186
fun nat_as_int ctxt =
boehmes@40161
   187
  map (apsnd ((uses_nat_type o Thm.prop_of) ?? Conv.fconv_rule (conv ctxt))) #>
boehmes@40161
   188
  exists (uses_nat_int o Thm.prop_of o snd) ?? append nat_embedding
boehmes@36898
   189
end
boehmes@36898
   190
boehmes@36898
   191
boehmes@36898
   192
boehmes@36898
   193
(* further normalizations: beta/eta, universal closure, atomize *)
boehmes@36898
   194
boehmes@36898
   195
val eta_expand_eq = @{lemma "f == (%x. f x)" by (rule reflexive)}
boehmes@36898
   196
boehmes@36898
   197
fun eta_expand_conv cv ctxt =
boehmes@36898
   198
  Conv.rewr_conv eta_expand_eq then_conv Conv.abs_conv (cv o snd) ctxt
boehmes@36898
   199
boehmes@36898
   200
local
boehmes@36898
   201
  val eta_conv = eta_expand_conv
boehmes@36898
   202
boehmes@40279
   203
  fun args_conv cv ct =
boehmes@40279
   204
    (case Thm.term_of ct of
boehmes@40279
   205
      _ $ _ => Conv.combination_conv (args_conv cv) cv
boehmes@40279
   206
    | _ => Conv.all_conv) ct
boehmes@40279
   207
boehmes@40279
   208
  fun eta_args_conv cv 0 = args_conv o cv
boehmes@40279
   209
    | eta_args_conv cv i = eta_conv (eta_args_conv cv (i-1))
boehmes@40279
   210
wenzelm@36936
   211
  fun keep_conv ctxt = Conv.binder_conv (norm_conv o snd) ctxt
boehmes@36898
   212
  and eta_binder_conv ctxt = Conv.arg_conv (eta_conv norm_conv ctxt)
boehmes@36898
   213
  and keep_let_conv ctxt = Conv.combination_conv
boehmes@36898
   214
    (Conv.arg_conv (norm_conv ctxt)) (Conv.abs_conv (norm_conv o snd) ctxt)
boehmes@36898
   215
  and unfold_let_conv ctxt = Conv.combination_conv
boehmes@36898
   216
    (Conv.arg_conv (norm_conv ctxt)) (eta_conv norm_conv ctxt)
boehmes@36898
   217
  and unfold_conv thm ctxt = Conv.rewr_conv thm then_conv keep_conv ctxt
boehmes@36898
   218
  and unfold_ex1_conv ctxt = unfold_conv @{thm Ex1_def} ctxt
boehmes@37786
   219
  and unfold_ball_conv ctxt = unfold_conv (mk_meta_eq @{thm Ball_def}) ctxt
boehmes@37786
   220
  and unfold_bex_conv ctxt = unfold_conv (mk_meta_eq @{thm Bex_def}) ctxt
boehmes@36898
   221
  and norm_conv ctxt ct =
boehmes@36898
   222
    (case Thm.term_of ct of
boehmes@36898
   223
      Const (@{const_name All}, _) $ Abs _ => keep_conv
boehmes@36898
   224
    | Const (@{const_name All}, _) $ _ => eta_binder_conv
boehmes@36898
   225
    | Const (@{const_name All}, _) => eta_conv eta_binder_conv
boehmes@36898
   226
    | Const (@{const_name Ex}, _) $ Abs _ => keep_conv
boehmes@36898
   227
    | Const (@{const_name Ex}, _) $ _ => eta_binder_conv
boehmes@36898
   228
    | Const (@{const_name Ex}, _) => eta_conv eta_binder_conv
boehmes@36898
   229
    | Const (@{const_name Let}, _) $ _ $ Abs _ => keep_let_conv
boehmes@36898
   230
    | Const (@{const_name Let}, _) $ _ $ _ => unfold_let_conv
boehmes@36898
   231
    | Const (@{const_name Let}, _) $ _ => eta_conv unfold_let_conv
boehmes@36898
   232
    | Const (@{const_name Let}, _) => eta_conv (eta_conv unfold_let_conv)
boehmes@36898
   233
    | Const (@{const_name Ex1}, _) $ _ => unfold_ex1_conv
boehmes@36898
   234
    | Const (@{const_name Ex1}, _) => eta_conv unfold_ex1_conv 
boehmes@36898
   235
    | Const (@{const_name Ball}, _) $ _ $ _ => unfold_ball_conv
boehmes@36898
   236
    | Const (@{const_name Ball}, _) $ _ => eta_conv unfold_ball_conv
boehmes@36898
   237
    | Const (@{const_name Ball}, _) => eta_conv (eta_conv unfold_ball_conv)
boehmes@36898
   238
    | Const (@{const_name Bex}, _) $ _ $ _ => unfold_bex_conv
boehmes@36898
   239
    | Const (@{const_name Bex}, _) $ _ => eta_conv unfold_bex_conv
boehmes@36898
   240
    | Const (@{const_name Bex}, _) => eta_conv (eta_conv unfold_bex_conv)
boehmes@36898
   241
    | Abs _ => Conv.abs_conv (norm_conv o snd)
boehmes@40279
   242
    | _ =>
boehmes@40279
   243
        (case Term.strip_comb (Thm.term_of ct) of
boehmes@40279
   244
          (Const (c as (_, T)), ts) =>
boehmes@40279
   245
            if SMT_Builtin.is_builtin ctxt c
boehmes@40279
   246
            then eta_args_conv norm_conv
boehmes@40279
   247
              (length (Term.binder_types T) - length ts)
boehmes@40279
   248
            else args_conv o norm_conv
boehmes@40424
   249
        | _ => args_conv o norm_conv)) ctxt ct
boehmes@36898
   250
boehmes@40279
   251
  fun is_normed ctxt t =
boehmes@36898
   252
    (case t of
boehmes@40279
   253
      Const (@{const_name All}, _) $ Abs (_, _, u) => is_normed ctxt u
boehmes@36898
   254
    | Const (@{const_name All}, _) $ _ => false
boehmes@36898
   255
    | Const (@{const_name All}, _) => false
boehmes@40279
   256
    | Const (@{const_name Ex}, _) $ Abs (_, _, u) => is_normed ctxt u
boehmes@36898
   257
    | Const (@{const_name Ex}, _) $ _ => false
boehmes@36898
   258
    | Const (@{const_name Ex}, _) => false
boehmes@36898
   259
    | Const (@{const_name Let}, _) $ u1 $ Abs (_, _, u2) =>
boehmes@40279
   260
        is_normed ctxt u1 andalso is_normed ctxt u2
boehmes@36898
   261
    | Const (@{const_name Let}, _) $ _ $ _ => false
boehmes@36898
   262
    | Const (@{const_name Let}, _) $ _ => false
boehmes@36898
   263
    | Const (@{const_name Let}, _) => false
boehmes@40279
   264
    | Const (@{const_name Ex1}, _) $ _ => false
boehmes@36898
   265
    | Const (@{const_name Ex1}, _) => false
boehmes@40279
   266
    | Const (@{const_name Ball}, _) $ _ $ _ => false
boehmes@40279
   267
    | Const (@{const_name Ball}, _) $ _ => false
boehmes@36898
   268
    | Const (@{const_name Ball}, _) => false
boehmes@40279
   269
    | Const (@{const_name Bex}, _) $ _ $ _ => false
boehmes@40279
   270
    | Const (@{const_name Bex}, _) $ _ => false
boehmes@36898
   271
    | Const (@{const_name Bex}, _) => false
boehmes@40279
   272
    | Abs (_, _, u) => is_normed ctxt u
boehmes@40279
   273
    | _ =>
boehmes@40279
   274
        (case Term.strip_comb t of
boehmes@40279
   275
          (Const (c as (_, T)), ts) =>
boehmes@40279
   276
            if SMT_Builtin.is_builtin ctxt c
boehmes@40279
   277
            then length (Term.binder_types T) = length ts andalso
boehmes@40279
   278
              forall (is_normed ctxt) ts
boehmes@40279
   279
            else forall (is_normed ctxt) ts
boehmes@40279
   280
        | (_, ts) => forall (is_normed ctxt) ts))
boehmes@36898
   281
in
boehmes@40279
   282
fun norm_binder_conv ctxt =
boehmes@40279
   283
  if_conv (is_normed ctxt) Conv.all_conv (norm_conv ctxt)
boehmes@36898
   284
end
boehmes@36898
   285
boehmes@36898
   286
fun norm_def ctxt thm =
boehmes@36898
   287
  (case Thm.prop_of thm of
haftmann@38864
   288
    @{term Trueprop} $ (Const (@{const_name HOL.eq}, _) $ _ $ Abs _) =>
boehmes@36898
   289
      norm_def ctxt (thm RS @{thm fun_cong})
boehmes@36898
   290
  | Const (@{const_name "=="}, _) $ _ $ Abs _ =>
boehmes@36898
   291
      norm_def ctxt (thm RS @{thm meta_eq_to_obj_eq})
boehmes@36898
   292
  | _ => thm)
boehmes@36898
   293
boehmes@36898
   294
fun atomize_conv ctxt ct =
boehmes@36898
   295
  (case Thm.term_of ct of
boehmes@36898
   296
    @{term "op ==>"} $ _ $ _ =>
boehmes@36898
   297
      Conv.binop_conv (atomize_conv ctxt) then_conv
boehmes@36898
   298
      Conv.rewr_conv @{thm atomize_imp}
boehmes@36898
   299
  | Const (@{const_name "=="}, _) $ _ $ _ =>
boehmes@36898
   300
      Conv.binop_conv (atomize_conv ctxt) then_conv
boehmes@36898
   301
      Conv.rewr_conv @{thm atomize_eq}
boehmes@36898
   302
  | Const (@{const_name all}, _) $ Abs _ =>
wenzelm@36936
   303
      Conv.binder_conv (atomize_conv o snd) ctxt then_conv
boehmes@36898
   304
      Conv.rewr_conv @{thm atomize_all}
boehmes@36898
   305
  | _ => Conv.all_conv) ct
boehmes@36898
   306
boehmes@36898
   307
fun normalize_rule ctxt =
boehmes@36898
   308
  Conv.fconv_rule (
boehmes@36898
   309
    (* reduce lambda abstractions, except at known binders: *)
boehmes@36898
   310
    Thm.beta_conversion true then_conv
boehmes@36898
   311
    Thm.eta_conversion then_conv
boehmes@36898
   312
    norm_binder_conv ctxt) #>
boehmes@36898
   313
  norm_def ctxt #>
boehmes@36898
   314
  Drule.forall_intr_vars #>
boehmes@36898
   315
  Conv.fconv_rule (atomize_conv ctxt)
boehmes@36898
   316
boehmes@36898
   317
boehmes@36898
   318
boehmes@36898
   319
(* lift lambda terms into additional rules *)
boehmes@36898
   320
boehmes@36898
   321
local
boehmes@36898
   322
  val meta_eq = @{cpat "op =="}
boehmes@36898
   323
  val meta_eqT = hd (Thm.dest_ctyp (Thm.ctyp_of_term meta_eq))
boehmes@36898
   324
  fun inst_meta cT = Thm.instantiate_cterm ([(meta_eqT, cT)], []) meta_eq
boehmes@36898
   325
  fun mk_meta_eq ct cu = Thm.mk_binop (inst_meta (Thm.ctyp_of_term ct)) ct cu
boehmes@36898
   326
boehmes@36898
   327
  fun cert ctxt = Thm.cterm_of (ProofContext.theory_of ctxt)
boehmes@36898
   328
boehmes@36898
   329
  fun used_vars cvs ct =
boehmes@36898
   330
    let
boehmes@36898
   331
      val lookup = AList.lookup (op aconv) (map (` Thm.term_of) cvs)
boehmes@36898
   332
      val add = (fn SOME ct => insert (op aconvc) ct | _ => I)
boehmes@36898
   333
    in Term.fold_aterms (add o lookup) (Thm.term_of ct) [] end
boehmes@36898
   334
boehmes@36898
   335
  fun apply cv thm = 
boehmes@36898
   336
    let val thm' = Thm.combination thm (Thm.reflexive cv)
boehmes@36898
   337
    in Thm.transitive thm' (Thm.beta_conversion false (Thm.rhs_of thm')) end
boehmes@36898
   338
  fun apply_def cvs eq = Thm.symmetric (fold apply cvs eq)
boehmes@36898
   339
boehmes@36898
   340
  fun replace_lambda cvs ct (cx as (ctxt, defs)) =
boehmes@36898
   341
    let
boehmes@36898
   342
      val cvs' = used_vars cvs ct
boehmes@36898
   343
      val ct' = fold_rev Thm.cabs cvs' ct
boehmes@36898
   344
    in
boehmes@36898
   345
      (case Termtab.lookup defs (Thm.term_of ct') of
boehmes@36898
   346
        SOME eq => (apply_def cvs' eq, cx)
boehmes@36898
   347
      | NONE =>
boehmes@36898
   348
          let
boehmes@36898
   349
            val {T, ...} = Thm.rep_cterm ct' and n = Name.uu
boehmes@36898
   350
            val (n', ctxt') = yield_singleton Variable.variant_fixes n ctxt
boehmes@36898
   351
            val cu = mk_meta_eq (cert ctxt (Free (n', T))) ct'
boehmes@36898
   352
            val (eq, ctxt'') = yield_singleton Assumption.add_assumes cu ctxt'
boehmes@36898
   353
            val defs' = Termtab.update (Thm.term_of ct', eq) defs
boehmes@36898
   354
          in (apply_def cvs' eq, (ctxt'', defs')) end)
boehmes@36898
   355
    end
boehmes@36898
   356
boehmes@36898
   357
  fun none ct cx = (Thm.reflexive ct, cx)
boehmes@36898
   358
  fun in_comb f g ct cx =
boehmes@36898
   359
    let val (cu1, cu2) = Thm.dest_comb ct
boehmes@36898
   360
    in cx |> f cu1 ||>> g cu2 |>> uncurry Thm.combination end
boehmes@36898
   361
  fun in_arg f = in_comb none f
boehmes@36898
   362
  fun in_abs f cvs ct (ctxt, defs) =
boehmes@36898
   363
    let
boehmes@36898
   364
      val (n, ctxt') = yield_singleton Variable.variant_fixes Name.uu ctxt
boehmes@36898
   365
      val (cv, cu) = Thm.dest_abs (SOME n) ct
boehmes@36898
   366
    in  (ctxt', defs) |> f (cv :: cvs) cu |>> Thm.abstract_rule n cv end
boehmes@36898
   367
boehmes@36898
   368
  fun traverse cvs ct =
boehmes@36898
   369
    (case Thm.term_of ct of
boehmes@36898
   370
      Const (@{const_name All}, _) $ Abs _ => in_arg (in_abs traverse cvs)
boehmes@36898
   371
    | Const (@{const_name Ex}, _) $ Abs _ => in_arg (in_abs traverse cvs)
boehmes@36898
   372
    | Const (@{const_name Let}, _) $ _ $ Abs _ =>
boehmes@36898
   373
        in_comb (in_arg (traverse cvs)) (in_abs traverse cvs)
boehmes@36898
   374
    | Abs _ => at_lambda cvs
boehmes@36898
   375
    | _ $ _ => in_comb (traverse cvs) (traverse cvs)
boehmes@36898
   376
    | _ => none) ct
boehmes@36898
   377
boehmes@36898
   378
  and at_lambda cvs ct =
boehmes@36898
   379
    in_abs traverse cvs ct #-> (fn thm =>
boehmes@36898
   380
    replace_lambda cvs (Thm.rhs_of thm) #>> Thm.transitive thm)
boehmes@36898
   381
boehmes@36898
   382
  fun has_free_lambdas t =
boehmes@36898
   383
    (case t of
boehmes@36898
   384
      Const (@{const_name All}, _) $ Abs (_, _, u) => has_free_lambdas u
boehmes@36898
   385
    | Const (@{const_name Ex}, _) $ Abs (_, _, u) => has_free_lambdas u
boehmes@36898
   386
    | Const (@{const_name Let}, _) $ u1 $ Abs (_, _, u2) =>
boehmes@36898
   387
        has_free_lambdas u1 orelse has_free_lambdas u2
boehmes@36898
   388
    | Abs _ => true
boehmes@36898
   389
    | u1 $ u2 => has_free_lambdas u1 orelse has_free_lambdas u2
boehmes@36898
   390
    | _ => false)
boehmes@36898
   391
boehmes@36898
   392
  fun lift_lm f thm cx =
boehmes@36898
   393
    if not (has_free_lambdas (Thm.prop_of thm)) then (thm, cx)
boehmes@36898
   394
    else cx |> f (Thm.cprop_of thm) |>> (fn thm' => Thm.equal_elim thm' thm)
boehmes@36898
   395
in
boehmes@40161
   396
fun lift_lambdas irules ctxt =
boehmes@36898
   397
  let
boehmes@36898
   398
    val cx = (ctxt, Termtab.empty)
boehmes@40161
   399
    val (idxs, thms) = split_list irules
boehmes@36898
   400
    val (thms', (ctxt', defs)) = fold_map (lift_lm (traverse [])) thms cx
boehmes@36898
   401
    val eqs = Termtab.fold (cons o normalize_rule ctxt' o snd) defs []
boehmes@40161
   402
  in (map (pair ~1) eqs @ (idxs ~~ thms'), ctxt') end
boehmes@36898
   403
end
boehmes@36898
   404
boehmes@36898
   405
boehmes@36898
   406
boehmes@36898
   407
(* make application explicit for functions with varying number of arguments *)
boehmes@36898
   408
boehmes@36898
   409
local
boehmes@36898
   410
  val const = prefix "c" and free = prefix "f"
boehmes@36898
   411
  fun min i (e as (_, j)) = if i <> j then (true, Int.min (i, j)) else e
boehmes@36898
   412
  fun add t i = Symtab.map_default (t, (false, i)) (min i)
boehmes@36898
   413
  fun traverse t =
boehmes@36898
   414
    (case Term.strip_comb t of
boehmes@36898
   415
      (Const (n, _), ts) => add (const n) (length ts) #> fold traverse ts 
boehmes@36898
   416
    | (Free (n, _), ts) => add (free n) (length ts) #> fold traverse ts
boehmes@36898
   417
    | (Abs (_, _, u), ts) => fold traverse (u :: ts)
boehmes@36898
   418
    | (_, ts) => fold traverse ts)
boehmes@40161
   419
  fun prune tab = Symtab.fold (fn (n, (true, i)) =>
boehmes@40161
   420
    Symtab.update (n, i) | _ => I) tab Symtab.empty
boehmes@36898
   421
boehmes@36898
   422
  fun binop_conv cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2
boehmes@36898
   423
  fun nary_conv conv1 conv2 ct =
boehmes@36898
   424
    (Conv.combination_conv (nary_conv conv1 conv2) conv2 else_conv conv1) ct
boehmes@36898
   425
  fun abs_conv conv tb = Conv.abs_conv (fn (cv, cx) =>
boehmes@36898
   426
    let val n = fst (Term.dest_Free (Thm.term_of cv))
boehmes@36898
   427
    in conv (Symtab.update (free n, 0) tb) cx end)
boehmes@37153
   428
  val fun_app_rule = @{lemma "f x == fun_app f x" by (simp add: fun_app_def)}
boehmes@36898
   429
in
boehmes@40161
   430
fun explicit_application ctxt irules =
boehmes@36898
   431
  let
boehmes@36898
   432
    fun sub_conv tb ctxt ct =
boehmes@36898
   433
      (case Term.strip_comb (Thm.term_of ct) of
boehmes@36898
   434
        (Const (n, _), ts) => app_conv tb (const n) (length ts) ctxt
boehmes@36898
   435
      | (Free (n, _), ts) => app_conv tb (free n) (length ts) ctxt
boehmes@36898
   436
      | (Abs _, _) => nary_conv (abs_conv sub_conv tb ctxt) (sub_conv tb ctxt)
boehmes@36898
   437
      | (_, _) => nary_conv Conv.all_conv (sub_conv tb ctxt)) ct
boehmes@36898
   438
    and app_conv tb n i ctxt =
boehmes@36898
   439
      (case Symtab.lookup tb n of
boehmes@36898
   440
        NONE => nary_conv Conv.all_conv (sub_conv tb ctxt)
boehmes@37153
   441
      | SOME j => fun_app_conv tb ctxt (i - j))
boehmes@37153
   442
    and fun_app_conv tb ctxt i ct = (
boehmes@36898
   443
      if i = 0 then nary_conv Conv.all_conv (sub_conv tb ctxt)
boehmes@36898
   444
      else
boehmes@37153
   445
        Conv.rewr_conv fun_app_rule then_conv
boehmes@37153
   446
        binop_conv (fun_app_conv tb ctxt (i-1)) (sub_conv tb ctxt)) ct
boehmes@36898
   447
boehmes@36898
   448
    fun needs_exp_app tab = Term.exists_subterm (fn
boehmes@36898
   449
        Bound _ $ _ => true
boehmes@36898
   450
      | Const (n, _) => Symtab.defined tab (const n)
boehmes@36898
   451
      | Free (n, _) => Symtab.defined tab (free n)
boehmes@36898
   452
      | _ => false)
boehmes@36898
   453
boehmes@36898
   454
    fun rewrite tab ctxt thm =
boehmes@36898
   455
      if not (needs_exp_app tab (Thm.prop_of thm)) then thm
boehmes@36898
   456
      else Conv.fconv_rule (sub_conv tab ctxt) thm
boehmes@36898
   457
boehmes@40161
   458
    val tab = prune (fold (traverse o Thm.prop_of o snd) irules Symtab.empty)
boehmes@40161
   459
  in map (apsnd (rewrite tab ctxt)) irules end
boehmes@36898
   460
end
boehmes@36898
   461
boehmes@36898
   462
boehmes@36898
   463
boehmes@39483
   464
(* add missing datatype selectors via hypothetical definitions *)
boehmes@39483
   465
boehmes@39483
   466
local
boehmes@39483
   467
  val add = (fn Type (n, _) => Symtab.update (n, ()) | _ => I)
boehmes@39483
   468
boehmes@39483
   469
  fun collect t =
boehmes@39483
   470
    (case Term.strip_comb t of
boehmes@39483
   471
      (Abs (_, T, t), _) => add T #> collect t
boehmes@39483
   472
    | (Const (_, T), ts) => collects T ts
boehmes@39483
   473
    | (Free (_, T), ts) => collects T ts
boehmes@39483
   474
    | _ => I)
boehmes@39483
   475
  and collects T ts =
boehmes@39483
   476
    let val ((Ts, Us), U) = Term.strip_type T |> apfst (chop (length ts))
boehmes@39483
   477
    in fold add Ts #> add (Us ---> U) #> fold collect ts end
boehmes@39483
   478
boehmes@39483
   479
  fun add_constructors thy n =
boehmes@39483
   480
    (case Datatype.get_info thy n of
boehmes@39483
   481
      NONE => I
boehmes@39483
   482
    | SOME {descr, ...} => fold (fn (_, (_, _, cs)) => fold (fn (n, ds) =>
boehmes@39483
   483
        fold (insert (op =) o pair n) (1 upto length ds)) cs) descr)
boehmes@39483
   484
boehmes@39483
   485
  fun add_selector (c as (n, i)) ctxt =
boehmes@39483
   486
    (case Datatype_Selectors.lookup_selector ctxt c of
boehmes@39483
   487
      SOME _ => ctxt
boehmes@39483
   488
    | NONE =>
boehmes@39483
   489
        let
boehmes@39483
   490
          val T = Sign.the_const_type (ProofContext.theory_of ctxt) n
boehmes@39483
   491
          val U = Term.body_type T --> nth (Term.binder_types T) (i-1)
boehmes@39483
   492
        in
boehmes@39483
   493
          ctxt
boehmes@39483
   494
          |> yield_singleton Variable.variant_fixes Name.uu
boehmes@39483
   495
          |>> pair ((n, T), i) o rpair U
boehmes@39483
   496
          |-> Context.proof_map o Datatype_Selectors.add_selector
boehmes@39483
   497
        end)
boehmes@39483
   498
in
boehmes@39483
   499
boehmes@40161
   500
fun datatype_selectors irules ctxt =
boehmes@39483
   501
  let
boehmes@40161
   502
    val ns = Symtab.keys (fold (collect o Thm.prop_of o snd) irules Symtab.empty)
boehmes@39483
   503
    val cs = fold (add_constructors (ProofContext.theory_of ctxt)) ns []
boehmes@40161
   504
  in (irules, fold add_selector cs ctxt) end
boehmes@39483
   505
    (* FIXME: also generate hypothetical definitions for the selectors *)
boehmes@39483
   506
boehmes@39483
   507
end
boehmes@39483
   508
boehmes@39483
   509
boehmes@39483
   510
boehmes@36898
   511
(* combined normalization *)
boehmes@36898
   512
boehmes@40162
   513
type extra_norm = bool -> (int * thm) list -> Proof.context ->
boehmes@40161
   514
  (int * thm) list * Proof.context
boehmes@36898
   515
boehmes@40161
   516
fun with_context f irules ctxt = (f ctxt irules, ctxt)
boehmes@36898
   517
boehmes@40424
   518
fun normalize extra_norm with_datatypes irules ctxt =
boehmes@40278
   519
  let
boehmes@40278
   520
    fun norm f ctxt' (i, thm) =
boehmes@40424
   521
      if Config.get ctxt' SMT_Config.drop_bad_facts then
boehmes@40278
   522
        (case try (f ctxt') thm of
boehmes@40278
   523
          SOME thm' => SOME (i, thm')
boehmes@40424
   524
        | NONE => (SMT_Config.verbose_msg ctxt' (prefix ("Warning: " ^
boehmes@40278
   525
            "dropping assumption: ") o Display.string_of_thm ctxt') thm; NONE))
boehmes@40424
   526
      else SOME (i, f ctxt' thm)
boehmes@40278
   527
  in
boehmes@40278
   528
    irules
boehmes@40278
   529
    |> trivial_distinct ctxt
boehmes@40278
   530
    |> rewrite_bool_cases ctxt
boehmes@40278
   531
    |> normalize_numerals ctxt
boehmes@40278
   532
    |> nat_as_int ctxt
boehmes@40278
   533
    |> rpair ctxt
boehmes@40278
   534
    |-> extra_norm with_datatypes
boehmes@40278
   535
    |-> with_context (map_filter o norm normalize_rule)
boehmes@40278
   536
    |-> SMT_Monomorph.monomorph
boehmes@40278
   537
    |-> lift_lambdas
boehmes@40278
   538
    |-> with_context explicit_application
boehmes@40278
   539
    |-> (if with_datatypes then datatype_selectors else pair)
boehmes@40278
   540
  end
boehmes@36898
   541
boehmes@36898
   542
end