src/HOL/Library/Old_SMT/old_z3_proof_tools.ML
author wenzelm
Fri Mar 06 23:52:35 2015 +0100 (2015-03-06)
changeset 59634 4b94cc030ba0
parent 59621 291934bac95e
child 60642 48dd1cefb4ae
permissions -rw-r--r--
clarified context;
blanchet@58058
     1
(*  Title:      HOL/Library/Old_SMT/old_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
blanchet@58058
     7
signature OLD_Z3_PROOF_TOOLS =
boehmes@36898
     8
sig
boehmes@41172
     9
  (*modifying terms*)
boehmes@36898
    10
  val as_meta_eq: cterm -> cterm
boehmes@36898
    11
boehmes@41123
    12
  (*theorem nets*)
boehmes@40164
    13
  val thm_net_of: ('a -> thm) -> 'a list -> 'a Net.net
boehmes@45393
    14
  val net_instances: (int * thm) Net.net -> cterm -> (int * thm) list
boehmes@36898
    15
  val net_instance: thm Net.net -> cterm -> thm option
boehmes@36898
    16
boehmes@41123
    17
  (*proof combinators*)
boehmes@36898
    18
  val under_assumption: (thm -> thm) -> cterm -> thm
boehmes@36898
    19
  val with_conv: conv -> (cterm -> thm) -> cterm -> thm
boehmes@36898
    20
  val discharge: thm -> thm -> thm
boehmes@36898
    21
  val varify: string list -> thm -> thm
boehmes@36898
    22
  val unfold_eqs: Proof.context -> thm list -> conv
boehmes@36898
    23
  val match_instantiate: (cterm -> cterm) -> cterm -> thm -> thm
wenzelm@54883
    24
  val by_tac: Proof.context -> (int -> tactic) -> cterm -> thm
boehmes@36898
    25
  val make_hyp_def: thm -> Proof.context -> thm * Proof.context
boehmes@42992
    26
  val by_abstraction: int -> bool * bool -> Proof.context -> thm list ->
boehmes@36899
    27
    (Proof.context -> cterm -> thm) -> cterm -> thm
boehmes@36898
    28
boehmes@41123
    29
  (*a faster COMP*)
boehmes@36898
    30
  type compose_data
boehmes@36898
    31
  val precompose: (cterm -> cterm list) -> thm -> compose_data
boehmes@36898
    32
  val precompose2: (cterm -> cterm * cterm) -> thm -> compose_data
boehmes@36898
    33
  val compose: compose_data -> thm -> thm
boehmes@36898
    34
boehmes@41123
    35
  (*unfolding of 'distinct'*)
boehmes@36898
    36
  val unfold_distinct_conv: conv
boehmes@36898
    37
boehmes@41123
    38
  (*simpset*)
boehmes@36899
    39
  val add_simproc: Simplifier.simproc -> Context.generic -> Context.generic
boehmes@36898
    40
  val make_simpset: Proof.context -> thm list -> simpset
boehmes@36898
    41
end
boehmes@36898
    42
blanchet@58058
    43
structure Old_Z3_Proof_Tools: OLD_Z3_PROOF_TOOLS =
boehmes@36898
    44
struct
boehmes@36898
    45
boehmes@36898
    46
boehmes@36898
    47
boehmes@41172
    48
(* modifying terms *)
boehmes@36898
    49
boehmes@41328
    50
fun as_meta_eq ct =
blanchet@58058
    51
  uncurry Old_SMT_Utils.mk_cequals (Thm.dest_binop (Old_SMT_Utils.dest_cprop ct))
boehmes@36898
    52
boehmes@36898
    53
boehmes@36898
    54
boehmes@36898
    55
(* theorem nets *)
boehmes@36898
    56
boehmes@40164
    57
fun thm_net_of f xthms =
boehmes@40164
    58
  let fun insert xthm = Net.insert_term (K false) (Thm.prop_of (f xthm), xthm)
boehmes@40164
    59
  in fold insert xthms Net.empty end
boehmes@36898
    60
boehmes@36898
    61
fun maybe_instantiate ct thm =
boehmes@36898
    62
  try Thm.first_order_match (Thm.cprop_of thm, ct)
boehmes@36898
    63
  |> Option.map (fn inst => Thm.instantiate inst thm)
boehmes@36898
    64
boehmes@42322
    65
local
boehmes@42322
    66
  fun instances_from_net match f net ct =
boehmes@42322
    67
    let
boehmes@42322
    68
      val lookup = if match then Net.match_term else Net.unify_term
boehmes@42322
    69
      val xthms = lookup net (Thm.term_of ct)
boehmes@45393
    70
      fun select ct = map_filter (f (maybe_instantiate ct)) xthms 
boehmes@45393
    71
      fun select' ct =
boehmes@42322
    72
        let val thm = Thm.trivial ct
boehmes@45393
    73
        in map_filter (f (try (fn rule => rule COMP thm))) xthms end
boehmes@45393
    74
    in (case select ct of [] => select' ct | xthms' => xthms') end
boehmes@42322
    75
in
boehmes@42322
    76
boehmes@45410
    77
fun net_instances net =
boehmes@45393
    78
  instances_from_net false (fn f => fn (i, thm) => Option.map (pair i) (f thm))
boehmes@45410
    79
    net
boehmes@42322
    80
boehmes@45410
    81
fun net_instance net = try hd o instances_from_net true I net
boehmes@42322
    82
boehmes@42322
    83
end
boehmes@36898
    84
boehmes@36898
    85
boehmes@36898
    86
boehmes@36898
    87
(* proof combinators *)
boehmes@36898
    88
boehmes@36898
    89
fun under_assumption f ct =
blanchet@58058
    90
  let val ct' = Old_SMT_Utils.mk_cprop ct
boehmes@36898
    91
  in Thm.implies_intr ct' (f (Thm.assume ct')) end
boehmes@36898
    92
boehmes@36898
    93
fun with_conv conv prove ct =
boehmes@36898
    94
  let val eq = Thm.symmetric (conv ct)
boehmes@36898
    95
  in Thm.equal_elim eq (prove (Thm.lhs_of eq)) end
boehmes@36898
    96
boehmes@36898
    97
fun discharge p pq = Thm.implies_elim pq p
boehmes@36898
    98
boehmes@36898
    99
fun varify vars = Drule.generalize ([], vars)
boehmes@36898
   100
boehmes@36898
   101
fun unfold_eqs _ [] = Conv.all_conv
boehmes@36898
   102
  | unfold_eqs ctxt eqs =
wenzelm@36936
   103
      Conv.top_sweep_conv (K (Conv.rewrs_conv eqs)) ctxt
boehmes@36898
   104
boehmes@36898
   105
fun match_instantiate f ct thm =
boehmes@36898
   106
  Thm.instantiate (Thm.match (f (Thm.cprop_of thm), ct)) thm
boehmes@36898
   107
wenzelm@54883
   108
fun by_tac ctxt tac ct = Goal.norm_result ctxt (Goal.prove_internal ctxt [] ct (K (tac 1)))
boehmes@36898
   109
boehmes@41123
   110
(*
boehmes@41123
   111
   |- c x == t x ==> P (c x)
boehmes@41123
   112
  ---------------------------
boehmes@41123
   113
      c == t |- P (c x)
boehmes@41123
   114
*) 
boehmes@36898
   115
fun make_hyp_def thm ctxt =
boehmes@36898
   116
  let
boehmes@36898
   117
    val (lhs, rhs) = Thm.dest_binop (Thm.cprem_of thm 1)
boehmes@36898
   118
    val (cf, cvs) = Drule.strip_comb lhs
blanchet@58058
   119
    val eq = Old_SMT_Utils.mk_cequals cf (fold_rev Thm.lambda cvs rhs)
boehmes@36898
   120
    fun apply cv th =
boehmes@36898
   121
      Thm.combination th (Thm.reflexive cv)
boehmes@36898
   122
      |> Conv.fconv_rule (Conv.arg_conv (Thm.beta_conversion false))
boehmes@36898
   123
  in
boehmes@36898
   124
    yield_singleton Assumption.add_assumes eq ctxt
boehmes@36898
   125
    |>> Thm.implies_elim thm o fold apply cvs
boehmes@36898
   126
  end
boehmes@36898
   127
boehmes@36898
   128
boehmes@36898
   129
boehmes@36898
   130
(* abstraction *)
boehmes@36898
   131
boehmes@36898
   132
local
boehmes@36898
   133
boehmes@36898
   134
fun abs_context ctxt = (ctxt, Termtab.empty, 1, false)
boehmes@36898
   135
boehmes@36898
   136
fun context_of (ctxt, _, _, _) = ctxt
boehmes@36898
   137
boehmes@36899
   138
fun replace (_, (cv, ct)) = Thm.forall_elim ct o Thm.forall_intr cv
boehmes@36898
   139
boehmes@36898
   140
fun abs_instantiate (_, tab, _, beta_norm) =
boehmes@36899
   141
  fold replace (Termtab.dest tab) #>
boehmes@36898
   142
  beta_norm ? Conv.fconv_rule (Thm.beta_conversion true)
boehmes@36898
   143
boehmes@36899
   144
fun lambda_abstract cvs t =
boehmes@36898
   145
  let
boehmes@36899
   146
    val frees = map Free (Term.add_frees t [])
boehmes@36899
   147
    val cvs' = filter (fn cv => member (op aconv) frees (Thm.term_of cv)) cvs
boehmes@36899
   148
    val vs = map (Term.dest_Free o Thm.term_of) cvs'
wenzelm@44241
   149
  in (fold_rev absfree vs t, cvs') end
boehmes@36898
   150
boehmes@42992
   151
fun fresh_abstraction (_, cvs) ct (cx as (ctxt, tab, idx, beta_norm)) =
boehmes@36899
   152
  let val (t, cvs') = lambda_abstract cvs (Thm.term_of ct)
boehmes@36898
   153
  in
boehmes@36898
   154
    (case Termtab.lookup tab t of
boehmes@36899
   155
      SOME (cv, _) => (Drule.list_comb (cv, cvs'), cx)
boehmes@36898
   156
    | NONE =>
boehmes@36898
   157
        let
boehmes@36898
   158
          val (n, ctxt') = yield_singleton Variable.variant_fixes "x" ctxt
wenzelm@59621
   159
          val cv = Thm.cterm_of ctxt'
wenzelm@59586
   160
            (Free (n, map Thm.typ_of_cterm cvs' ---> Thm.typ_of_cterm ct))
boehmes@36899
   161
          val cu = Drule.list_comb (cv, cvs')
wenzelm@46497
   162
          val e = (t, (cv, fold_rev Thm.lambda cvs' ct))
boehmes@36898
   163
          val beta_norm' = beta_norm orelse not (null cvs')
boehmes@36899
   164
        in (cu, (ctxt', Termtab.update e tab, idx + 1, beta_norm')) end)
boehmes@36898
   165
  end
boehmes@36898
   166
boehmes@42992
   167
fun abs_comb f g dcvs ct =
boehmes@36898
   168
  let val (cf, cu) = Thm.dest_comb ct
wenzelm@46497
   169
  in f dcvs cf ##>> g dcvs cu #>> uncurry Thm.apply end
boehmes@36898
   170
boehmes@36899
   171
fun abs_arg f = abs_comb (K pair) f
boehmes@36899
   172
boehmes@42992
   173
fun abs_args f dcvs ct =
boehmes@36899
   174
  (case Thm.term_of ct of
boehmes@42992
   175
    _ $ _ => abs_comb (abs_args f) f dcvs ct
boehmes@36899
   176
  | _ => pair ct)
boehmes@36899
   177
boehmes@42992
   178
fun abs_list f g dcvs ct =
boehmes@36898
   179
  (case Thm.term_of ct of
boehmes@36898
   180
    Const (@{const_name Nil}, _) => pair ct
boehmes@36898
   181
  | Const (@{const_name Cons}, _) $ _ $ _ =>
boehmes@42992
   182
      abs_comb (abs_arg f) (abs_list f g) dcvs ct
boehmes@42992
   183
  | _ => g dcvs ct)
boehmes@36898
   184
boehmes@42992
   185
fun abs_abs f (depth, cvs) ct =
boehmes@36898
   186
  let val (cv, cu) = Thm.dest_abs NONE ct
wenzelm@46497
   187
  in f (depth, cv :: cvs) cu #>> Thm.lambda cv end
boehmes@36898
   188
boehmes@41899
   189
val is_atomic =
boehmes@41899
   190
  (fn Free _ => true | Var _ => true | Bound _ => true | _ => false)
boehmes@36898
   191
boehmes@42992
   192
fun abstract depth (ext_logic, with_theories) =
boehmes@36898
   193
  let
boehmes@36898
   194
    fun abstr1 cvs ct = abs_arg abstr cvs ct
boehmes@36898
   195
    and abstr2 cvs ct = abs_comb abstr1 abstr cvs ct
boehmes@36898
   196
    and abstr3 cvs ct = abs_comb abstr2 abstr cvs ct
boehmes@36898
   197
    and abstr_abs cvs ct = abs_arg (abs_abs abstr) cvs ct
boehmes@36898
   198
boehmes@42992
   199
    and abstr (dcvs as (d, cvs)) ct =
boehmes@36898
   200
      (case Thm.term_of ct of
boehmes@42992
   201
        @{const Trueprop} $ _ => abstr1 dcvs ct
wenzelm@56245
   202
      | @{const Pure.imp} $ _ $ _ => abstr2 dcvs ct
boehmes@40579
   203
      | @{const True} => pair ct
boehmes@40579
   204
      | @{const False} => pair ct
boehmes@42992
   205
      | @{const Not} $ _ => abstr1 dcvs ct
boehmes@42992
   206
      | @{const HOL.conj} $ _ $ _ => abstr2 dcvs ct
boehmes@42992
   207
      | @{const HOL.disj} $ _ $ _ => abstr2 dcvs ct
boehmes@42992
   208
      | @{const HOL.implies} $ _ $ _ => abstr2 dcvs ct
boehmes@42992
   209
      | Const (@{const_name HOL.eq}, _) $ _ $ _ => abstr2 dcvs ct
boehmes@40681
   210
      | Const (@{const_name distinct}, _) $ _ =>
boehmes@42992
   211
          if ext_logic then abs_arg (abs_list abstr fresh_abstraction) dcvs ct
boehmes@42992
   212
          else fresh_abstraction dcvs ct
boehmes@36898
   213
      | Const (@{const_name If}, _) $ _ $ _ $ _ =>
boehmes@42992
   214
          if ext_logic then abstr3 dcvs ct else fresh_abstraction dcvs ct
boehmes@36898
   215
      | Const (@{const_name All}, _) $ _ =>
boehmes@42992
   216
          if ext_logic then abstr_abs dcvs ct else fresh_abstraction dcvs ct
boehmes@36898
   217
      | Const (@{const_name Ex}, _) $ _ =>
boehmes@42992
   218
          if ext_logic then abstr_abs dcvs ct else fresh_abstraction dcvs ct
boehmes@36899
   219
      | t => (fn cx =>
boehmes@36899
   220
          if is_atomic t orelse can HOLogic.dest_number t then (ct, cx)
boehmes@36899
   221
          else if with_theories andalso
blanchet@58058
   222
            Old_Z3_Interface.is_builtin_theory_term (context_of cx) t
boehmes@42992
   223
          then abs_args abstr dcvs ct cx
boehmes@42992
   224
          else if d = 0 then fresh_abstraction dcvs ct cx
boehmes@42992
   225
          else
boehmes@42992
   226
            (case Term.strip_comb t of
boehmes@42992
   227
              (Const _, _) => abs_args abstr (d-1, cvs) ct cx
boehmes@42992
   228
            | (Free _, _) => abs_args abstr (d-1, cvs) ct cx
boehmes@42992
   229
            | _ => fresh_abstraction dcvs ct cx)))
boehmes@42992
   230
  in abstr (depth, []) end
boehmes@36898
   231
wenzelm@59634
   232
val cimp = Thm.cterm_of @{context} @{const Pure.imp}
boehmes@40579
   233
boehmes@42992
   234
fun deepen depth f x =
boehmes@42992
   235
  if depth = 0 then f depth x
boehmes@42992
   236
  else (case try (f depth) x of SOME y => y | NONE => deepen (depth - 1) f x)
boehmes@42992
   237
boehmes@42992
   238
fun with_prems depth thms f ct =
boehmes@40579
   239
  fold_rev (Thm.mk_binop cimp o Thm.cprop_of) thms ct
boehmes@42992
   240
  |> deepen depth f
boehmes@36898
   241
  |> fold (fn prem => fn th => Thm.implies_elim th prem) thms
boehmes@36898
   242
boehmes@36898
   243
in
boehmes@36898
   244
boehmes@42992
   245
fun by_abstraction depth mode ctxt thms prove =
boehmes@42992
   246
  with_prems depth thms (fn d => fn ct =>
boehmes@42992
   247
    let val (cu, cx) = abstract d mode ct (abs_context ctxt)
boehmes@42992
   248
    in abs_instantiate cx (prove (context_of cx) cu) end)
boehmes@36898
   249
boehmes@36898
   250
end
boehmes@36898
   251
boehmes@36898
   252
boehmes@36898
   253
boehmes@36898
   254
(* a faster COMP *)
boehmes@36898
   255
boehmes@36898
   256
type compose_data = cterm list * (cterm -> cterm list) * thm
boehmes@36898
   257
boehmes@36898
   258
fun list2 (x, y) = [x, y]
boehmes@36898
   259
boehmes@36898
   260
fun precompose f rule = (f (Thm.cprem_of rule 1), f, rule)
boehmes@36898
   261
fun precompose2 f rule = precompose (list2 o f) rule
boehmes@36898
   262
boehmes@36898
   263
fun compose (cvs, f, rule) thm =
boehmes@36898
   264
  discharge thm (Thm.instantiate ([], cvs ~~ f (Thm.cprop_of thm)) rule)
boehmes@36898
   265
boehmes@36898
   266
boehmes@36898
   267
boehmes@36898
   268
(* unfolding of 'distinct' *)
boehmes@36898
   269
boehmes@36898
   270
local
boehmes@36898
   271
  val set1 = @{lemma "x ~: set [] == ~False" by simp}
boehmes@36898
   272
  val set2 = @{lemma "x ~: set [x] == False" by simp}
boehmes@36898
   273
  val set3 = @{lemma "x ~: set [y] == x ~= y" by simp}
boehmes@36898
   274
  val set4 = @{lemma "x ~: set (x # ys) == False" by simp}
boehmes@36898
   275
  val set5 = @{lemma "x ~: set (y # ys) == x ~= y & x ~: set ys" by simp}
boehmes@36898
   276
boehmes@36898
   277
  fun set_conv ct =
wenzelm@36936
   278
    (Conv.rewrs_conv [set1, set2, set3, set4] else_conv
boehmes@36898
   279
    (Conv.rewr_conv set5 then_conv Conv.arg_conv set_conv)) ct
boehmes@36898
   280
boehmes@40681
   281
  val dist1 = @{lemma "distinct [] == ~False" by (simp add: distinct_def)}
boehmes@40681
   282
  val dist2 = @{lemma "distinct [x] == ~False" by (simp add: distinct_def)}
boehmes@40681
   283
  val dist3 = @{lemma "distinct (x # xs) == x ~: set xs & distinct xs"
boehmes@40274
   284
    by (simp add: distinct_def)}
boehmes@36898
   285
boehmes@36898
   286
  fun binop_conv cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2
boehmes@36898
   287
in
boehmes@36898
   288
fun unfold_distinct_conv ct =
wenzelm@36936
   289
  (Conv.rewrs_conv [dist1, dist2] else_conv
boehmes@36898
   290
  (Conv.rewr_conv dist3 then_conv binop_conv set_conv unfold_distinct_conv)) ct
boehmes@36898
   291
end
boehmes@36898
   292
boehmes@36898
   293
boehmes@36898
   294
boehmes@36898
   295
(* simpset *)
boehmes@36898
   296
boehmes@36898
   297
local
boehmes@36898
   298
  val antisym_le1 = mk_meta_eq @{thm order_class.antisym_conv}
boehmes@36898
   299
  val antisym_le2 = mk_meta_eq @{thm linorder_class.antisym_conv2}
boehmes@36898
   300
  val antisym_less1 = mk_meta_eq @{thm linorder_class.antisym_conv1}
boehmes@36898
   301
  val antisym_less2 = mk_meta_eq @{thm linorder_class.antisym_conv3}
boehmes@36898
   302
boehmes@36898
   303
  fun eq_prop t thm = HOLogic.mk_Trueprop t aconv Thm.prop_of thm
boehmes@36898
   304
  fun dest_binop ((c as Const _) $ t $ u) = (c, t, u)
boehmes@36898
   305
    | dest_binop t = raise TERM ("dest_binop", [t])
boehmes@36898
   306
wenzelm@51717
   307
  fun prove_antisym_le ctxt t =
boehmes@36898
   308
    let
boehmes@36898
   309
      val (le, r, s) = dest_binop t
boehmes@36898
   310
      val less = Const (@{const_name less}, Term.fastype_of le)
wenzelm@51717
   311
      val prems = Simplifier.prems_of ctxt
boehmes@36898
   312
    in
boehmes@36898
   313
      (case find_first (eq_prop (le $ s $ r)) prems of
boehmes@36898
   314
        NONE =>
boehmes@36898
   315
          find_first (eq_prop (HOLogic.mk_not (less $ r $ s))) prems
boehmes@36898
   316
          |> Option.map (fn thm => thm RS antisym_less1)
boehmes@36898
   317
      | SOME thm => SOME (thm RS antisym_le1))
boehmes@36898
   318
    end
boehmes@36898
   319
    handle THM _ => NONE
boehmes@36898
   320
wenzelm@51717
   321
  fun prove_antisym_less ctxt t =
boehmes@36898
   322
    let
boehmes@36898
   323
      val (less, r, s) = dest_binop (HOLogic.dest_not t)
boehmes@36898
   324
      val le = Const (@{const_name less_eq}, Term.fastype_of less)
wenzelm@51717
   325
      val prems = Simplifier.prems_of ctxt
boehmes@36898
   326
    in
boehmes@36898
   327
      (case find_first (eq_prop (le $ r $ s)) prems of
boehmes@36898
   328
        NONE =>
boehmes@36898
   329
          find_first (eq_prop (HOLogic.mk_not (less $ s $ r))) prems
boehmes@36898
   330
          |> Option.map (fn thm => thm RS antisym_less2)
boehmes@36898
   331
      | SOME thm => SOME (thm RS antisym_le2))
boehmes@36898
   332
  end
boehmes@36898
   333
  handle THM _ => NONE
boehmes@36899
   334
wenzelm@51717
   335
  val basic_simpset =
wenzelm@51717
   336
    simpset_of (put_simpset HOL_ss @{context}
wenzelm@51717
   337
      addsimps @{thms field_simps}
wenzelm@51717
   338
      addsimps [@{thm times_divide_eq_right}, @{thm times_divide_eq_left}]
wenzelm@51717
   339
      addsimps @{thms arith_special} addsimps @{thms arith_simps}
wenzelm@51717
   340
      addsimps @{thms rel_simps}
wenzelm@51717
   341
      addsimps @{thms array_rules}
wenzelm@51717
   342
      addsimps @{thms term_true_def} addsimps @{thms term_false_def}
wenzelm@51717
   343
      addsimps @{thms z3div_def} addsimps @{thms z3mod_def}
wenzelm@51717
   344
      addsimprocs [@{simproc binary_int_div}, @{simproc binary_int_mod}]
wenzelm@51717
   345
      addsimprocs [
wenzelm@51717
   346
        Simplifier.simproc_global @{theory} "fast_int_arith" [
wenzelm@51717
   347
          "(m::int) < n", "(m::int) <= n", "(m::int) = n"] Lin_Arith.simproc,
wenzelm@51717
   348
        Simplifier.simproc_global @{theory} "antisym_le" ["(x::'a::order) <= y"]
wenzelm@51717
   349
          prove_antisym_le,
wenzelm@51717
   350
        Simplifier.simproc_global @{theory} "antisym_less" ["~ (x::'a::linorder) < y"]
wenzelm@51717
   351
          prove_antisym_less])
boehmes@36899
   352
boehmes@36899
   353
  structure Simpset = Generic_Data
boehmes@36899
   354
  (
boehmes@36899
   355
    type T = simpset
boehmes@36899
   356
    val empty = basic_simpset
boehmes@36899
   357
    val extend = I
boehmes@36899
   358
    val merge = Simplifier.merge_ss
boehmes@36899
   359
  )
boehmes@36898
   360
in
boehmes@36898
   361
wenzelm@51717
   362
fun add_simproc simproc context =
wenzelm@51717
   363
  Simpset.map (simpset_map (Context.proof_of context)
wenzelm@51717
   364
    (fn ctxt => ctxt addsimprocs [simproc])) context
boehmes@36899
   365
boehmes@36899
   366
fun make_simpset ctxt rules =
wenzelm@51717
   367
  simpset_of (put_simpset (Simpset.get (Context.Proof ctxt)) ctxt addsimps rules)
boehmes@36898
   368
boehmes@36898
   369
end
boehmes@36898
   370
boehmes@36898
   371
end