src/HOL/Tools/SMT/z3_proof_tools.ML
author boehmes
Wed May 12 23:54:02 2010 +0200 (2010-05-12)
changeset 36898 8e55aa1306c5
child 36899 bcd6fce5bf06
permissions -rw-r--r--
integrated SMT into the HOL image
boehmes@36898
     1
(*  Title:      HOL/Tools/SMT/z3_proof_tools.ML
boehmes@36898
     2
    Author:     Sascha Boehme, TU Muenchen
boehmes@36898
     3
boehmes@36898
     4
Helper functions required for Z3 proof reconstruction.
boehmes@36898
     5
*)
boehmes@36898
     6
boehmes@36898
     7
signature Z3_PROOF_TOOLS =
boehmes@36898
     8
sig
boehmes@36898
     9
  (* accessing and modifying terms *)
boehmes@36898
    10
  val term_of: cterm -> term
boehmes@36898
    11
  val prop_of: thm -> term
boehmes@36898
    12
  val mk_prop: cterm -> cterm
boehmes@36898
    13
  val as_meta_eq: cterm -> cterm
boehmes@36898
    14
boehmes@36898
    15
  (* theorem nets *)
boehmes@36898
    16
  val thm_net_of: thm list -> thm Net.net
boehmes@36898
    17
  val net_instance: thm Net.net -> cterm -> thm option
boehmes@36898
    18
boehmes@36898
    19
  (* proof combinators *)
boehmes@36898
    20
  val under_assumption: (thm -> thm) -> cterm -> thm
boehmes@36898
    21
  val with_conv: conv -> (cterm -> thm) -> cterm -> thm
boehmes@36898
    22
  val discharge: thm -> thm -> thm
boehmes@36898
    23
  val varify: string list -> thm -> thm
boehmes@36898
    24
  val unfold_eqs: Proof.context -> thm list -> conv
boehmes@36898
    25
  val match_instantiate: (cterm -> cterm) -> cterm -> thm -> thm
boehmes@36898
    26
  val by_tac: (int -> tactic) -> cterm -> thm
boehmes@36898
    27
  val make_hyp_def: thm -> Proof.context -> thm * Proof.context
boehmes@36898
    28
  val by_abstraction: Proof.context -> thm list -> (Proof.context -> cterm ->
boehmes@36898
    29
    thm) -> cterm -> thm
boehmes@36898
    30
boehmes@36898
    31
  (* a faster COMP *)
boehmes@36898
    32
  type compose_data
boehmes@36898
    33
  val precompose: (cterm -> cterm list) -> thm -> compose_data
boehmes@36898
    34
  val precompose2: (cterm -> cterm * cterm) -> thm -> compose_data
boehmes@36898
    35
  val compose: compose_data -> thm -> thm
boehmes@36898
    36
boehmes@36898
    37
  (* unfolding of 'distinct' *)
boehmes@36898
    38
  val unfold_distinct_conv: conv
boehmes@36898
    39
boehmes@36898
    40
  (* simpset *)
boehmes@36898
    41
  val make_simpset: Proof.context -> thm list -> simpset
boehmes@36898
    42
end
boehmes@36898
    43
boehmes@36898
    44
structure Z3_Proof_Tools: Z3_PROOF_TOOLS =
boehmes@36898
    45
struct
boehmes@36898
    46
boehmes@36898
    47
boehmes@36898
    48
boehmes@36898
    49
(* accessing terms *)
boehmes@36898
    50
boehmes@36898
    51
val dest_prop = (fn @{term Trueprop} $ t => t | t => t)
boehmes@36898
    52
boehmes@36898
    53
fun term_of ct = dest_prop (Thm.term_of ct)
boehmes@36898
    54
fun prop_of thm = dest_prop (Thm.prop_of thm)
boehmes@36898
    55
boehmes@36898
    56
val mk_prop = Thm.capply @{cterm Trueprop}
boehmes@36898
    57
boehmes@36898
    58
val (eqT, eq) = `(hd o Thm.dest_ctyp o Thm.ctyp_of_term) @{cpat "op =="}
boehmes@36898
    59
fun mk_meta_eq_cterm ct cu =
boehmes@36898
    60
  let val inst = ([(eqT, Thm.ctyp_of_term ct)], [])
boehmes@36898
    61
  in Thm.mk_binop (Thm.instantiate_cterm inst eq) ct cu end
boehmes@36898
    62
boehmes@36898
    63
fun as_meta_eq ct = uncurry mk_meta_eq_cterm (Thm.dest_binop (Thm.dest_arg ct))
boehmes@36898
    64
boehmes@36898
    65
boehmes@36898
    66
boehmes@36898
    67
(* theorem nets *)
boehmes@36898
    68
boehmes@36898
    69
fun thm_net_of thms =
boehmes@36898
    70
  let fun insert thm = Net.insert_term (K false) (Thm.prop_of thm, thm)
boehmes@36898
    71
  in fold insert thms Net.empty end
boehmes@36898
    72
boehmes@36898
    73
fun maybe_instantiate ct thm =
boehmes@36898
    74
  try Thm.first_order_match (Thm.cprop_of thm, ct)
boehmes@36898
    75
  |> Option.map (fn inst => Thm.instantiate inst thm)
boehmes@36898
    76
boehmes@36898
    77
fun first_of thms ct = get_first (maybe_instantiate ct) thms
boehmes@36898
    78
fun net_instance net ct = first_of (Net.match_term net (Thm.term_of ct)) ct
boehmes@36898
    79
boehmes@36898
    80
boehmes@36898
    81
boehmes@36898
    82
(* proof combinators *)
boehmes@36898
    83
boehmes@36898
    84
fun under_assumption f ct =
boehmes@36898
    85
  let val ct' = mk_prop ct
boehmes@36898
    86
  in Thm.implies_intr ct' (f (Thm.assume ct')) end
boehmes@36898
    87
boehmes@36898
    88
fun with_conv conv prove ct =
boehmes@36898
    89
  let val eq = Thm.symmetric (conv ct)
boehmes@36898
    90
  in Thm.equal_elim eq (prove (Thm.lhs_of eq)) end
boehmes@36898
    91
boehmes@36898
    92
fun discharge p pq = Thm.implies_elim pq p
boehmes@36898
    93
boehmes@36898
    94
fun varify vars = Drule.generalize ([], vars)
boehmes@36898
    95
boehmes@36898
    96
fun unfold_eqs _ [] = Conv.all_conv
boehmes@36898
    97
  | unfold_eqs ctxt eqs =
boehmes@36898
    98
      More_Conv.top_sweep_conv (K (More_Conv.rewrs_conv eqs)) ctxt
boehmes@36898
    99
boehmes@36898
   100
fun match_instantiate f ct thm =
boehmes@36898
   101
  Thm.instantiate (Thm.match (f (Thm.cprop_of thm), ct)) thm
boehmes@36898
   102
boehmes@36898
   103
fun by_tac tac ct = Goal.norm_result (Goal.prove_internal [] ct (K (tac 1)))
boehmes@36898
   104
boehmes@36898
   105
(* |- c x == t x ==> P (c x)  ~~>  c == t |- P (c x) *) 
boehmes@36898
   106
fun make_hyp_def thm ctxt =
boehmes@36898
   107
  let
boehmes@36898
   108
    val (lhs, rhs) = Thm.dest_binop (Thm.cprem_of thm 1)
boehmes@36898
   109
    val (cf, cvs) = Drule.strip_comb lhs
boehmes@36898
   110
    val eq = mk_meta_eq_cterm cf (fold_rev Thm.cabs cvs rhs)
boehmes@36898
   111
    fun apply cv th =
boehmes@36898
   112
      Thm.combination th (Thm.reflexive cv)
boehmes@36898
   113
      |> Conv.fconv_rule (Conv.arg_conv (Thm.beta_conversion false))
boehmes@36898
   114
  in
boehmes@36898
   115
    yield_singleton Assumption.add_assumes eq ctxt
boehmes@36898
   116
    |>> Thm.implies_elim thm o fold apply cvs
boehmes@36898
   117
  end
boehmes@36898
   118
boehmes@36898
   119
boehmes@36898
   120
boehmes@36898
   121
(* abstraction *)
boehmes@36898
   122
boehmes@36898
   123
local
boehmes@36898
   124
boehmes@36898
   125
fun typ_of ct = #T (Thm.rep_cterm ct)
boehmes@36898
   126
fun certify ctxt = Thm.cterm_of (ProofContext.theory_of ctxt)
boehmes@36898
   127
boehmes@36898
   128
fun abs_context ctxt = (ctxt, Termtab.empty, 1, false)
boehmes@36898
   129
boehmes@36898
   130
fun context_of (ctxt, _, _, _) = ctxt
boehmes@36898
   131
boehmes@36898
   132
fun replace (cv, ct) = Thm.forall_elim ct o Thm.forall_intr cv
boehmes@36898
   133
boehmes@36898
   134
fun abs_instantiate (_, tab, _, beta_norm) =
boehmes@36898
   135
  fold replace (map snd (Termtab.dest tab)) #>
boehmes@36898
   136
  beta_norm ? Conv.fconv_rule (Thm.beta_conversion true)
boehmes@36898
   137
boehmes@36898
   138
fun generalize cvs =
boehmes@36898
   139
  let
boehmes@36898
   140
    val no_name = ""
boehmes@36898
   141
boehmes@36898
   142
    fun dest (Free (n, _)) = n
boehmes@36898
   143
      | dest _ = no_name
boehmes@36898
   144
boehmes@36898
   145
    fun gen vs (t as Free (n, _)) =
boehmes@36898
   146
          let val i = find_index (equal n) vs
boehmes@36898
   147
          in
boehmes@36898
   148
            if i >= 0 then insert (op aconvc) (nth cvs i) #> pair (Bound i)
boehmes@36898
   149
            else pair t
boehmes@36898
   150
          end
boehmes@36898
   151
      | gen vs (t $ u) = gen vs t ##>> gen vs u #>> (op $)
boehmes@36898
   152
      | gen vs (Abs (n, T, t)) =
boehmes@36898
   153
          gen (no_name :: vs) t #>> (fn u => Abs (n, T, u))
boehmes@36898
   154
      | gen _ t = pair t
boehmes@36898
   155
boehmes@36898
   156
  in (fn ct => gen (map (dest o Thm.term_of) cvs) (Thm.term_of ct) []) end
boehmes@36898
   157
boehmes@36898
   158
fun fresh_abstraction cvs ct (cx as (ctxt, tab, idx, beta_norm)) =
boehmes@36898
   159
  let val (t, cvs') = generalize cvs ct
boehmes@36898
   160
  in
boehmes@36898
   161
    (case Termtab.lookup tab t of
boehmes@36898
   162
      SOME (cv, _) => (cv, cx)
boehmes@36898
   163
    | NONE =>
boehmes@36898
   164
        let
boehmes@36898
   165
          val (n, ctxt') = yield_singleton Variable.variant_fixes "x" ctxt
boehmes@36898
   166
          val cv = certify ctxt (Free (n, map typ_of cvs' ---> typ_of ct))
boehmes@36898
   167
          val cv' = Drule.list_comb (cv, cvs')
boehmes@36898
   168
          val e = (t, (cv, fold_rev Thm.cabs cvs' ct))
boehmes@36898
   169
          val beta_norm' = beta_norm orelse not (null cvs')
boehmes@36898
   170
        in (cv', (ctxt', Termtab.update e tab, idx + 1, beta_norm')) end)
boehmes@36898
   171
  end
boehmes@36898
   172
boehmes@36898
   173
fun abs_arg f cvs ct =
boehmes@36898
   174
  let val (cf, cu) = Thm.dest_comb ct
boehmes@36898
   175
  in f cvs cu #>> Thm.capply cf end
boehmes@36898
   176
boehmes@36898
   177
fun abs_comb f g cvs ct =
boehmes@36898
   178
  let val (cf, cu) = Thm.dest_comb ct
boehmes@36898
   179
  in f cvs cf ##>> g cvs cu #>> uncurry Thm.capply end
boehmes@36898
   180
boehmes@36898
   181
fun abs_list f g cvs ct =
boehmes@36898
   182
  (case Thm.term_of ct of
boehmes@36898
   183
    Const (@{const_name Nil}, _) => pair ct
boehmes@36898
   184
  | Const (@{const_name Cons}, _) $ _ $ _ =>
boehmes@36898
   185
      abs_comb (abs_arg f) (abs_list f g) cvs ct
boehmes@36898
   186
  | _ => g cvs ct)
boehmes@36898
   187
boehmes@36898
   188
fun abs_abs f cvs ct =
boehmes@36898
   189
  let val (cv, cu) = Thm.dest_abs NONE ct
boehmes@36898
   190
  in f (cv :: cvs) cu #>> Thm.cabs cv end
boehmes@36898
   191
boehmes@36898
   192
val is_atomic = (fn _ $ _ => false | Abs _ => false | _ => true)
boehmes@36898
   193
val is_arithT = (fn @{typ int} => true | @{typ real} => true | _ => false)
boehmes@36898
   194
fun is_number t =
boehmes@36898
   195
  (case try HOLogic.dest_number t of
boehmes@36898
   196
    SOME (T, _) => is_arithT T
boehmes@36898
   197
  | NONE => false)
boehmes@36898
   198
boehmes@36898
   199
fun abstract (ext_logic, with_theories) =
boehmes@36898
   200
  let
boehmes@36898
   201
    fun abstr1 cvs ct = abs_arg abstr cvs ct
boehmes@36898
   202
    and abstr2 cvs ct = abs_comb abstr1 abstr cvs ct
boehmes@36898
   203
    and abstr3 cvs ct = abs_comb abstr2 abstr cvs ct
boehmes@36898
   204
    and abstr_abs cvs ct = abs_arg (abs_abs abstr) cvs ct
boehmes@36898
   205
boehmes@36898
   206
    and abstr cvs ct =
boehmes@36898
   207
      (case Thm.term_of ct of
boehmes@36898
   208
        @{term Trueprop} $ _ => abstr1 cvs ct
boehmes@36898
   209
      | @{term "op ==>"} $ _ $ _ => abstr2 cvs ct
boehmes@36898
   210
      | @{term True} => pair ct
boehmes@36898
   211
      | @{term False} => pair ct
boehmes@36898
   212
      | @{term Not} $ _ => abstr1 cvs ct
boehmes@36898
   213
      | @{term "op &"} $ _ $ _ => abstr2 cvs ct
boehmes@36898
   214
      | @{term "op |"} $ _ $ _ => abstr2 cvs ct
boehmes@36898
   215
      | @{term "op -->"} $ _ $ _ => abstr2 cvs ct
boehmes@36898
   216
      | Const (@{const_name "op ="}, _) $ _ $ _ => abstr2 cvs ct
boehmes@36898
   217
      | Const (@{const_name distinct}, _) $ _ =>
boehmes@36898
   218
          if ext_logic then abs_arg (abs_list abstr fresh_abstraction) cvs ct
boehmes@36898
   219
          else fresh_abstraction cvs ct
boehmes@36898
   220
      | Const (@{const_name If}, _) $ _ $ _ $ _ =>
boehmes@36898
   221
          if ext_logic then abstr3 cvs ct else fresh_abstraction cvs ct
boehmes@36898
   222
      | Const (@{const_name All}, _) $ _ =>
boehmes@36898
   223
          if ext_logic then abstr_abs cvs ct else fresh_abstraction cvs ct
boehmes@36898
   224
      | Const (@{const_name Ex}, _) $ _ =>
boehmes@36898
   225
          if ext_logic then abstr_abs cvs ct else fresh_abstraction cvs ct
boehmes@36898
   226
      | @{term "uminus :: int => _"} $ _ => abstr1 cvs ct
boehmes@36898
   227
      | @{term "uminus :: real => _"} $ _ => abstr1 cvs ct
boehmes@36898
   228
      | @{term "op + :: int => _"} $ _ $ _ => abstr2 cvs ct
boehmes@36898
   229
      | @{term "op + :: real => _"} $ _ $ _ => abstr2 cvs ct
boehmes@36898
   230
      | @{term "op - :: int => _"} $ _ $ _ => abstr2 cvs ct
boehmes@36898
   231
      | @{term "op - :: real => _"} $ _ $ _ => abstr2 cvs ct
boehmes@36898
   232
      | @{term "op * :: int => _"} $ _ $ _ => abstr2 cvs ct
boehmes@36898
   233
      | @{term "op * :: real => _"} $ _ $ _ => abstr2 cvs ct
boehmes@36898
   234
      | @{term "op div :: int => _"} $ _ $ _ => abstr2 cvs ct
boehmes@36898
   235
      | @{term "op mod :: int => _"} $ _ $ _ => abstr2 cvs ct
boehmes@36898
   236
      | @{term "op / :: real => _"} $ _ $ _ => abstr2 cvs ct
boehmes@36898
   237
      | @{term "op < :: int => _"} $ _ $ _ => abstr2 cvs ct
boehmes@36898
   238
      | @{term "op < :: real => _"} $ _ $ _ => abstr2 cvs ct
boehmes@36898
   239
      | @{term "op <= :: int => _"} $ _ $ _ => abstr2 cvs ct
boehmes@36898
   240
      | @{term "op <= :: real => _"} $ _ $ _ => abstr2 cvs ct
boehmes@36898
   241
      | Const (@{const_name apply}, _) $ _ $ _ => abstr2 cvs ct
boehmes@36898
   242
      | Const (@{const_name fun_upd}, _) $ _ $ _ $ _ => abstr3 cvs ct
boehmes@36898
   243
      | t =>
boehmes@36898
   244
          if is_atomic t orelse is_number t then pair ct
boehmes@36898
   245
          else fresh_abstraction cvs ct)
boehmes@36898
   246
  in abstr [] end
boehmes@36898
   247
boehmes@36898
   248
fun with_prems thms f ct =
boehmes@36898
   249
  fold_rev (Thm.mk_binop @{cterm "op ==>"} o Thm.cprop_of) thms ct
boehmes@36898
   250
  |> f
boehmes@36898
   251
  |> fold (fn prem => fn th => Thm.implies_elim th prem) thms
boehmes@36898
   252
boehmes@36898
   253
in
boehmes@36898
   254
boehmes@36898
   255
fun by_abstraction ctxt thms prove = with_prems thms (fn ct =>
boehmes@36898
   256
  let val (cu, cx) = abstract (true, true) ct (abs_context ctxt)
boehmes@36898
   257
  in abs_instantiate cx (prove (context_of cx) cu) end)
boehmes@36898
   258
boehmes@36898
   259
end
boehmes@36898
   260
boehmes@36898
   261
boehmes@36898
   262
boehmes@36898
   263
(* a faster COMP *)
boehmes@36898
   264
boehmes@36898
   265
type compose_data = cterm list * (cterm -> cterm list) * thm
boehmes@36898
   266
boehmes@36898
   267
fun list2 (x, y) = [x, y]
boehmes@36898
   268
boehmes@36898
   269
fun precompose f rule = (f (Thm.cprem_of rule 1), f, rule)
boehmes@36898
   270
fun precompose2 f rule = precompose (list2 o f) rule
boehmes@36898
   271
boehmes@36898
   272
fun compose (cvs, f, rule) thm =
boehmes@36898
   273
  discharge thm (Thm.instantiate ([], cvs ~~ f (Thm.cprop_of thm)) rule)
boehmes@36898
   274
boehmes@36898
   275
boehmes@36898
   276
boehmes@36898
   277
(* unfolding of 'distinct' *)
boehmes@36898
   278
boehmes@36898
   279
local
boehmes@36898
   280
  val set1 = @{lemma "x ~: set [] == ~False" by simp}
boehmes@36898
   281
  val set2 = @{lemma "x ~: set [x] == False" by simp}
boehmes@36898
   282
  val set3 = @{lemma "x ~: set [y] == x ~= y" by simp}
boehmes@36898
   283
  val set4 = @{lemma "x ~: set (x # ys) == False" by simp}
boehmes@36898
   284
  val set5 = @{lemma "x ~: set (y # ys) == x ~= y & x ~: set ys" by simp}
boehmes@36898
   285
boehmes@36898
   286
  fun set_conv ct =
boehmes@36898
   287
    (More_Conv.rewrs_conv [set1, set2, set3, set4] else_conv
boehmes@36898
   288
    (Conv.rewr_conv set5 then_conv Conv.arg_conv set_conv)) ct
boehmes@36898
   289
boehmes@36898
   290
  val dist1 = @{lemma "distinct [] == ~False" by simp}
boehmes@36898
   291
  val dist2 = @{lemma "distinct [x] == ~False" by simp}
boehmes@36898
   292
  val dist3 = @{lemma "distinct (x # xs) == x ~: set xs & distinct xs"
boehmes@36898
   293
    by simp}
boehmes@36898
   294
boehmes@36898
   295
  fun binop_conv cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2
boehmes@36898
   296
in
boehmes@36898
   297
fun unfold_distinct_conv ct =
boehmes@36898
   298
  (More_Conv.rewrs_conv [dist1, dist2] else_conv
boehmes@36898
   299
  (Conv.rewr_conv dist3 then_conv binop_conv set_conv unfold_distinct_conv)) ct
boehmes@36898
   300
end
boehmes@36898
   301
boehmes@36898
   302
boehmes@36898
   303
boehmes@36898
   304
(* simpset *)
boehmes@36898
   305
boehmes@36898
   306
local
boehmes@36898
   307
  val antisym_le1 = mk_meta_eq @{thm order_class.antisym_conv}
boehmes@36898
   308
  val antisym_le2 = mk_meta_eq @{thm linorder_class.antisym_conv2}
boehmes@36898
   309
  val antisym_less1 = mk_meta_eq @{thm linorder_class.antisym_conv1}
boehmes@36898
   310
  val antisym_less2 = mk_meta_eq @{thm linorder_class.antisym_conv3}
boehmes@36898
   311
boehmes@36898
   312
  fun eq_prop t thm = HOLogic.mk_Trueprop t aconv Thm.prop_of thm
boehmes@36898
   313
  fun dest_binop ((c as Const _) $ t $ u) = (c, t, u)
boehmes@36898
   314
    | dest_binop t = raise TERM ("dest_binop", [t])
boehmes@36898
   315
boehmes@36898
   316
  fun prove_antisym_le ss t =
boehmes@36898
   317
    let
boehmes@36898
   318
      val (le, r, s) = dest_binop t
boehmes@36898
   319
      val less = Const (@{const_name less}, Term.fastype_of le)
boehmes@36898
   320
      val prems = Simplifier.prems_of_ss ss
boehmes@36898
   321
    in
boehmes@36898
   322
      (case find_first (eq_prop (le $ s $ r)) prems of
boehmes@36898
   323
        NONE =>
boehmes@36898
   324
          find_first (eq_prop (HOLogic.mk_not (less $ r $ s))) prems
boehmes@36898
   325
          |> Option.map (fn thm => thm RS antisym_less1)
boehmes@36898
   326
      | SOME thm => SOME (thm RS antisym_le1))
boehmes@36898
   327
    end
boehmes@36898
   328
    handle THM _ => NONE
boehmes@36898
   329
boehmes@36898
   330
  fun prove_antisym_less ss t =
boehmes@36898
   331
    let
boehmes@36898
   332
      val (less, r, s) = dest_binop (HOLogic.dest_not t)
boehmes@36898
   333
      val le = Const (@{const_name less_eq}, Term.fastype_of less)
boehmes@36898
   334
      val prems = prems_of_ss ss
boehmes@36898
   335
    in
boehmes@36898
   336
      (case find_first (eq_prop (le $ r $ s)) prems of
boehmes@36898
   337
        NONE =>
boehmes@36898
   338
          find_first (eq_prop (HOLogic.mk_not (less $ s $ r))) prems
boehmes@36898
   339
          |> Option.map (fn thm => thm RS antisym_less2)
boehmes@36898
   340
      | SOME thm => SOME (thm RS antisym_le2))
boehmes@36898
   341
  end
boehmes@36898
   342
  handle THM _ => NONE
boehmes@36898
   343
in
boehmes@36898
   344
boehmes@36898
   345
fun make_simpset ctxt rules = Simplifier.context ctxt (HOL_ss
boehmes@36898
   346
  addsimps @{thms field_simps}
boehmes@36898
   347
  addsimps [@{thm times_divide_eq_right}, @{thm times_divide_eq_left}]
boehmes@36898
   348
  addsimps @{thms arith_special} addsimps @{thms less_bin_simps}
boehmes@36898
   349
  addsimps @{thms le_bin_simps} addsimps @{thms eq_bin_simps}
boehmes@36898
   350
  addsimps @{thms add_bin_simps} addsimps @{thms succ_bin_simps}
boehmes@36898
   351
  addsimps @{thms minus_bin_simps} addsimps @{thms pred_bin_simps}
boehmes@36898
   352
  addsimps @{thms mult_bin_simps} addsimps @{thms iszero_simps}
boehmes@36898
   353
  addsimps @{thms array_rules}
boehmes@36898
   354
  addsimprocs [
boehmes@36898
   355
    Simplifier.simproc @{theory} "fast_int_arith" [
boehmes@36898
   356
      "(m::int) < n", "(m::int) <= n", "(m::int) = n"] (K Lin_Arith.simproc),
boehmes@36898
   357
    Simplifier.simproc @{theory} "fast_real_arith" [
boehmes@36898
   358
      "(m::real) < n", "(m::real) <= n", "(m::real) = n"]
boehmes@36898
   359
      (K Lin_Arith.simproc),
boehmes@36898
   360
    Simplifier.simproc @{theory} "antisym_le" ["(x::'a::order) <= y"]
boehmes@36898
   361
      (K prove_antisym_le),
boehmes@36898
   362
    Simplifier.simproc @{theory} "antisym_less" ["~ (x::'a::linorder) < y"]
boehmes@36898
   363
      (K prove_antisym_less)]
boehmes@36898
   364
  addsimps rules)
boehmes@36898
   365
boehmes@36898
   366
end
boehmes@36898
   367
boehmes@36898
   368
end