src/Provers/splitter.ML
author wenzelm
Fri May 05 22:32:25 2000 +0200 (2000-05-05 ago)
changeset 8815 187547eae4c5
parent 8634 3f34637cb9c0
child 9267 dbf30a2d1b56
permissions -rw-r--r--
use Args.colon / Args.parens;
nipkow@4
     1
(*  Title:      Provers/splitter
nipkow@4
     2
    ID:         $Id$
nipkow@4
     3
    Author:     Tobias Nipkow
nipkow@1030
     4
    Copyright   1995  TU Munich
nipkow@4
     5
nipkow@4
     6
Generic case-splitter, suitable for most logics.
clasohm@0
     7
*)
clasohm@0
     8
oheimb@5304
     9
infix 4 addsplits delsplits;
oheimb@5304
    10
oheimb@5304
    11
signature SPLITTER_DATA =
oheimb@5304
    12
sig
oheimb@5304
    13
  structure Simplifier: SIMPLIFIER
oheimb@5553
    14
  val mk_eq         : thm -> thm
oheimb@5304
    15
  val meta_eq_to_iff: thm (* "x == y ==> x = y"                    *)
oheimb@5304
    16
  val iffD          : thm (* "[| P = Q; Q |] ==> P"                *)
oheimb@5304
    17
  val disjE         : thm (* "[| P | Q; P ==> R; Q ==> R |] ==> R" *)
oheimb@5304
    18
  val conjE         : thm (* "[| P & Q; [| P; Q |] ==> R |] ==> R" *)
oheimb@5304
    19
  val exE           : thm (* "[|  x. P x; !!x. P x ==> Q |] ==> Q" *)
oheimb@5304
    20
  val contrapos     : thm (* "[| ~ Q; P ==> Q |] ==> ~ P"          *)
oheimb@5304
    21
  val contrapos2    : thm (* "[| Q; ~ P ==> ~ Q |] ==> P"          *)
oheimb@5304
    22
  val notnotD       : thm (* "~ ~ P ==> P"                         *)
oheimb@5304
    23
end
oheimb@5304
    24
oheimb@5304
    25
signature SPLITTER =
oheimb@5304
    26
sig
oheimb@5304
    27
  type simpset
oheimb@5304
    28
  val split_tac       : thm list -> int -> tactic
oheimb@5304
    29
  val split_inside_tac: thm list -> int -> tactic
oheimb@5304
    30
  val split_asm_tac   : thm list -> int -> tactic
oheimb@5304
    31
  val addsplits       : simpset * thm list -> simpset
oheimb@5304
    32
  val delsplits       : simpset * thm list -> simpset
oheimb@5304
    33
  val Addsplits       : thm list -> unit
oheimb@5304
    34
  val Delsplits       : thm list -> unit
wenzelm@8468
    35
  val split_add_global: theory attribute
wenzelm@8468
    36
  val split_del_global: theory attribute
wenzelm@8468
    37
  val split_add_local: Proof.context attribute
wenzelm@8468
    38
  val split_del_local: Proof.context attribute
wenzelm@8468
    39
  val split_modifiers : (Args.T list -> (Method.modifier * Args.T list)) list
wenzelm@8468
    40
  val setup: (theory -> theory) list
oheimb@5304
    41
end;
oheimb@5304
    42
oheimb@5304
    43
functor SplitterFun(Data: SPLITTER_DATA): SPLITTER =
oheimb@5304
    44
struct 
oheimb@5304
    45
wenzelm@8468
    46
structure Simplifier = Data.Simplifier;
wenzelm@8468
    47
type simpset = Simplifier.simpset;
oheimb@5304
    48
oheimb@5304
    49
val Const ("==>", _) $ (Const ("Trueprop", _) $
oheimb@5304
    50
         (Const (const_not, _) $ _    )) $ _ = #prop (rep_thm(Data.notnotD));
oheimb@5304
    51
oheimb@5304
    52
val Const ("==>", _) $ (Const ("Trueprop", _) $
oheimb@5304
    53
         (Const (const_or , _) $ _ $ _)) $ _ = #prop (rep_thm(Data.disjE));
berghofe@1721
    54
nipkow@4668
    55
fun split_format_err() = error("Wrong format for split rule");
nipkow@4668
    56
oheimb@5553
    57
fun split_thm_info thm = case concl_of (Data.mk_eq thm) of
oheimb@5304
    58
     Const("==", _)$(Var _$t)$c =>
oheimb@5304
    59
        (case strip_comb t of
oheimb@5304
    60
           (Const(a,_),_) => (a,case c of (Const(s,_)$_)=>s=const_not|_=> false)
oheimb@5304
    61
         | _              => split_format_err())
oheimb@5304
    62
   | _ => split_format_err();
oheimb@5304
    63
oheimb@5304
    64
fun mk_case_split_tac order =
clasohm@0
    65
let
clasohm@0
    66
berghofe@1686
    67
berghofe@1686
    68
(************************************************************
berghofe@1686
    69
   Create lift-theorem "trlift" :
berghofe@1686
    70
berghofe@7672
    71
   [| !!x. Q x == R x; P(%x. R x) == C |] ==> P (%x. Q x) == C
berghofe@1686
    72
berghofe@1686
    73
*************************************************************)
oheimb@5304
    74
oheimb@5304
    75
val meta_iffD = Data.meta_eq_to_iff RS Data.iffD;
nipkow@943
    76
val lift =
oheimb@5304
    77
  let val ct = read_cterm (#sign(rep_thm Data.iffD))
nipkow@943
    78
           ("[| !!x::'b::logic. Q(x) == R(x) |] ==> \
wenzelm@3835
    79
            \P(%x. Q(x)) == P(%x. R(x))::'a::logic",propT)
nipkow@943
    80
  in prove_goalw_cterm [] ct
nipkow@943
    81
     (fn [prem] => [rewtac prem, rtac reflexive_thm 1])
nipkow@943
    82
  end;
nipkow@4
    83
clasohm@0
    84
val trlift = lift RS transitive_thm;
berghofe@7672
    85
val _ $ (P $ _) $ _ = concl_of trlift;
clasohm@0
    86
clasohm@0
    87
berghofe@1686
    88
(************************************************************************ 
berghofe@1686
    89
   Set up term for instantiation of P in the lift-theorem
berghofe@1686
    90
   
berghofe@1686
    91
   Ts    : types of parameters (i.e. variables bound by meta-quantifiers)
berghofe@1686
    92
   t     : lefthand side of meta-equality in subgoal
berghofe@1686
    93
           the lift theorem is applied to (see select)
berghofe@1686
    94
   pos   : "path" leading to abstraction, coded as a list
berghofe@1686
    95
   T     : type of body of P(...)
berghofe@1686
    96
   maxi  : maximum index of Vars
berghofe@1686
    97
*************************************************************************)
berghofe@1686
    98
nipkow@1030
    99
fun mk_cntxt Ts t pos T maxi =
nipkow@1030
   100
  let fun var (t,i) = Var(("X",i),type_of1(Ts,t));
nipkow@1030
   101
      fun down [] t i = Bound 0
nipkow@1030
   102
        | down (p::ps) t i =
nipkow@1030
   103
            let val (h,ts) = strip_comb t
paulson@2266
   104
                val v1 = ListPair.map var (take(p,ts), i upto (i+p-1))
nipkow@1030
   105
                val u::us = drop(p,ts)
paulson@2266
   106
                val v2 = ListPair.map var (us, (i+p) upto (i+length(ts)-2))
nipkow@1030
   107
      in list_comb(h,v1@[down ps u (i+length ts)]@v2) end;
nipkow@1030
   108
  in Abs("", T, down (rev pos) t maxi) end;
nipkow@1030
   109
berghofe@1686
   110
berghofe@1686
   111
(************************************************************************ 
berghofe@1686
   112
   Set up term for instantiation of P in the split-theorem
berghofe@1686
   113
   P(...) == rhs
berghofe@1686
   114
berghofe@1686
   115
   t     : lefthand side of meta-equality in subgoal
berghofe@1686
   116
           the split theorem is applied to (see select)
berghofe@1686
   117
   T     : type of body of P(...)
berghofe@4232
   118
   tt    : the term  Const(key,..) $ ...
berghofe@1686
   119
*************************************************************************)
berghofe@1686
   120
berghofe@4232
   121
fun mk_cntxt_splitthm t tt T =
berghofe@4232
   122
  let fun repl lev t =
berghofe@7672
   123
    if incr_boundvars lev tt aconv t then Bound lev
berghofe@4232
   124
    else case t of
berghofe@4232
   125
        (Abs (v, T2, t)) => Abs (v, T2, repl (lev+1) t)
berghofe@4232
   126
      | (Bound i) => Bound (if i>=lev then i+1 else i)
berghofe@4232
   127
      | (t1 $ t2) => (repl lev t1) $ (repl lev t2)
berghofe@4232
   128
      | t => t
berghofe@4232
   129
  in Abs("", T, repl 0 t) end;
berghofe@1686
   130
berghofe@1686
   131
berghofe@1686
   132
(* add all loose bound variables in t to list is *)
nipkow@1030
   133
fun add_lbnos(is,t) = add_loose_bnos(t,0,is);
nipkow@1030
   134
berghofe@7672
   135
(* check if the innermost abstraction that needs to be removed
nipkow@1064
   136
   has a body of type T; otherwise the expansion thm will fail later on
nipkow@1064
   137
*)
nipkow@1064
   138
fun type_test(T,lbnos,apsns) =
paulson@2143
   139
  let val (_,U,_) = nth_elem(foldl Int.min (hd lbnos, tl lbnos), apsns)
nipkow@1064
   140
  in T=U end;
clasohm@0
   141
berghofe@1686
   142
(*************************************************************************
berghofe@1686
   143
   Create a "split_pack".
berghofe@1686
   144
berghofe@1686
   145
   thm   : the relevant split-theorem, i.e. P(...) == rhs , where P(...)
berghofe@1686
   146
           is of the form
berghofe@1686
   147
           P( Const(key,...) $ t_1 $ ... $ t_n )      (e.g. key = "if")
berghofe@1686
   148
   T     : type of P(...)
berghofe@7672
   149
   T'    : type of term to be scanned
berghofe@1686
   150
   n     : number of arguments expected by Const(key,...)
berghofe@1686
   151
   ts    : list of arguments actually found
berghofe@1686
   152
   apsns : list of tuples of the form (T,U,pos), one tuple for each
berghofe@1686
   153
           abstraction that is encountered on the way to the position where 
berghofe@1686
   154
           Const(key, ...) $ ...  occurs, where
berghofe@1686
   155
           T   : type of the variable bound by the abstraction
berghofe@1686
   156
           U   : type of the abstraction's body
berghofe@1686
   157
           pos : "path" leading to the body of the abstraction
berghofe@1686
   158
   pos   : "path" leading to the position where Const(key, ...) $ ...  occurs.
berghofe@1686
   159
   TB    : type of  Const(key,...) $ t_1 $ ... $ t_n
berghofe@1721
   160
   t     : the term Const(key,...) $ t_1 $ ... $ t_n
berghofe@1686
   161
berghofe@1686
   162
   A split pack is a tuple of the form
berghofe@7672
   163
   (thm, apsns, pos, TB, tt)
berghofe@1686
   164
   Note : apsns is reversed, so that the outermost quantifier's position
berghofe@1686
   165
          comes first ! If the terms in ts don't contain variables bound
berghofe@1686
   166
          by other than meta-quantifiers, apsns is empty, because no further
berghofe@1686
   167
          lifting is required before applying the split-theorem.
berghofe@1686
   168
******************************************************************************) 
berghofe@1686
   169
berghofe@7672
   170
fun mk_split_pack(thm, T, T', n, ts, apsns, pos, TB, t) =
nipkow@1064
   171
  if n > length ts then []
nipkow@1064
   172
  else let val lev = length apsns
nipkow@1030
   173
           val lbnos = foldl add_lbnos ([],take(n,ts))
nipkow@1030
   174
           val flbnos = filter (fn i => i < lev) lbnos
berghofe@4232
   175
           val tt = incr_boundvars (~lev) t
berghofe@7672
   176
       in if null flbnos then
berghofe@7672
   177
            if T = T' then [(thm,[],pos,TB,tt)] else []
berghofe@7672
   178
          else if type_test(T,flbnos,apsns) then [(thm, rev apsns,pos,TB,tt)]
paulson@2143
   179
               else []
nipkow@1064
   180
       end;
clasohm@0
   181
berghofe@1686
   182
berghofe@1686
   183
(****************************************************************************
berghofe@1686
   184
   Recursively scans term for occurences of Const(key,...) $ ...
berghofe@1686
   185
   Returns a list of "split-packs" (one for each occurence of Const(key,...) )
berghofe@1686
   186
berghofe@1686
   187
   cmap : association list of split-theorems that should be tried.
berghofe@1686
   188
          The elements have the format (key,(thm,T,n)) , where
berghofe@1686
   189
          key : the theorem's key constant ( Const(key,...) $ ... )
berghofe@1686
   190
          thm : the theorem itself
berghofe@1686
   191
          T   : type of P( Const(key,...) $ ... )
berghofe@1686
   192
          n   : number of arguments expected by Const(key,...)
berghofe@1686
   193
   Ts   : types of parameters
berghofe@1686
   194
   t    : the term to be scanned
berghofe@1686
   195
******************************************************************************)
berghofe@1686
   196
nipkow@6130
   197
fun split_posns cmap sg Ts t =
nipkow@6130
   198
  let
berghofe@7672
   199
    val T' = fastype_of1 (Ts, t);
berghofe@7672
   200
    fun posns Ts pos apsns (Abs (_, T, t)) =
berghofe@7672
   201
          let val U = fastype_of1 (T::Ts,t)
berghofe@7672
   202
          in posns (T::Ts) (0::pos) ((T, U, pos)::apsns) t end
nipkow@6130
   203
      | posns Ts pos apsns t =
nipkow@6130
   204
          let
berghofe@7672
   205
            val (h, ts) = strip_comb t
berghofe@7672
   206
            fun iter((i, a), t) = (i+1, (posns Ts (i::pos) apsns t) @ a);
nipkow@6130
   207
            val a = case h of
berghofe@7672
   208
              Const(c, cT) =>
berghofe@7672
   209
                (case assoc(cmap, c) of
nipkow@6130
   210
                   Some(gcT, thm, T, n) =>
nipkow@6130
   211
                     if Type.typ_instance(Sign.tsig_of sg, cT, gcT)
nipkow@6130
   212
                     then
nipkow@6130
   213
                       let val t2 = list_comb (h, take (n, ts))
berghofe@7672
   214
                       in mk_split_pack (thm, T, T', n, ts, apsns, pos, type_of1 (Ts, t2), t2)
nipkow@6130
   215
                       end
nipkow@6130
   216
                     else []
nipkow@6130
   217
                 | None => [])
nipkow@6130
   218
            | _ => []
berghofe@7672
   219
          in snd(foldl iter ((0, a), ts)) end
nipkow@1030
   220
  in posns Ts [] [] t end;
clasohm@0
   221
berghofe@1686
   222
clasohm@0
   223
fun nth_subgoal i thm = nth_elem(i-1,prems_of thm);
clasohm@0
   224
berghofe@1721
   225
fun shorter((_,ps,pos,_,_),(_,qs,qos,_,_)) =
wenzelm@4519
   226
  prod_ord (int_ord o pairself length) (order o pairself length)
wenzelm@4519
   227
    ((ps, pos), (qs, qos));
wenzelm@4519
   228
berghofe@1686
   229
berghofe@1686
   230
berghofe@1686
   231
(************************************************************
berghofe@1686
   232
   call split_posns with appropriate parameters
berghofe@1686
   233
*************************************************************)
clasohm@0
   234
nipkow@1030
   235
fun select cmap state i =
nipkow@6130
   236
  let val sg = #sign(rep_thm state)
nipkow@6130
   237
      val goali = nth_subgoal i state
nipkow@1030
   238
      val Ts = rev(map #2 (Logic.strip_params goali))
nipkow@1030
   239
      val _ $ t $ _ = Logic.strip_assums_concl goali;
nipkow@6130
   240
  in (Ts,t, sort shorter (split_posns cmap sg Ts t)) end;
nipkow@1030
   241
berghofe@1686
   242
berghofe@1686
   243
(*************************************************************
berghofe@1686
   244
   instantiate lift theorem
berghofe@1686
   245
berghofe@1686
   246
   if t is of the form
berghofe@1686
   247
   ... ( Const(...,...) $ Abs( .... ) ) ...
berghofe@1686
   248
   then
berghofe@1686
   249
   P = %a.  ... ( Const(...,...) $ a ) ...
berghofe@1686
   250
   where a has type T --> U
berghofe@1686
   251
berghofe@1686
   252
   Ts      : types of parameters
berghofe@1686
   253
   t       : lefthand side of meta-equality in subgoal
berghofe@1686
   254
             the split theorem is applied to (see cmap)
berghofe@1686
   255
   T,U,pos : see mk_split_pack
berghofe@1686
   256
   state   : current proof state
berghofe@1686
   257
   lift    : the lift theorem
berghofe@1686
   258
   i       : no. of subgoal
berghofe@1686
   259
**************************************************************)
berghofe@1686
   260
berghofe@7672
   261
fun inst_lift Ts t (T, U, pos) state i =
berghofe@7672
   262
  let
berghofe@7672
   263
    val cert = cterm_of (sign_of_thm state);
berghofe@7672
   264
    val cntxt = mk_cntxt Ts t pos (T --> U) (#maxidx(rep_thm trlift));    
berghofe@7672
   265
  in cterm_instantiate [(cert P, cert cntxt)] trlift
berghofe@7672
   266
  end;
clasohm@0
   267
clasohm@0
   268
berghofe@1686
   269
(*************************************************************
berghofe@1686
   270
   instantiate split theorem
berghofe@1686
   271
berghofe@1686
   272
   Ts    : types of parameters
berghofe@1686
   273
   t     : lefthand side of meta-equality in subgoal
berghofe@1686
   274
           the split theorem is applied to (see cmap)
berghofe@4232
   275
   tt    : the term  Const(key,..) $ ...
berghofe@1686
   276
   thm   : the split theorem
berghofe@1686
   277
   TB    : type of body of P(...)
berghofe@1686
   278
   state : current proof state
berghofe@4232
   279
   i     : number of subgoal
berghofe@1686
   280
**************************************************************)
berghofe@1686
   281
berghofe@4232
   282
fun inst_split Ts t tt thm TB state i =
berghofe@7672
   283
  let 
berghofe@7672
   284
    val thm' = Thm.lift_rule (state, i) thm;
berghofe@7672
   285
    val (P, _) = strip_comb (fst (Logic.dest_equals
berghofe@7672
   286
      (Logic.strip_assums_concl (#prop (rep_thm thm')))));
berghofe@7672
   287
    val cert = cterm_of (sign_of_thm state);
berghofe@7672
   288
    val cntxt = mk_cntxt_splitthm t tt TB;
berghofe@7672
   289
    val abss = foldl (fn (t, T) => Abs ("", T, t));
berghofe@7672
   290
  in cterm_instantiate [(cert P, cert (abss (cntxt, Ts)))] thm'
berghofe@4232
   291
  end;
berghofe@1686
   292
berghofe@7672
   293
berghofe@1686
   294
(*****************************************************************************
berghofe@1686
   295
   The split-tactic
berghofe@1686
   296
   
berghofe@1686
   297
   splits : list of split-theorems to be tried
berghofe@1686
   298
   i      : number of subgoal the tactic should be applied to
berghofe@1686
   299
*****************************************************************************)
berghofe@1686
   300
clasohm@0
   301
fun split_tac [] i = no_tac
clasohm@0
   302
  | split_tac splits i =
oheimb@5553
   303
  let val splits = map Data.mk_eq splits;
oheimb@5304
   304
      fun const(thm) =
nipkow@3918
   305
            (case concl_of thm of _$(t as _$lhs)$_ =>
nipkow@6130
   306
               (case strip_comb lhs of (Const(a,aT),args) =>
nipkow@6130
   307
                  (a,(aT,thm,fastype_of t,length args))
nipkow@4668
   308
                | _ => split_format_err())
nipkow@4668
   309
             | _ => split_format_err())
clasohm@0
   310
      val cmap = map const splits;
berghofe@7672
   311
      fun lift_tac Ts t p st = rtac (inst_lift Ts t p st i) i st
berghofe@7672
   312
      fun lift_split_tac state =
berghofe@7672
   313
            let val (Ts, t, splits) = select cmap state i
nipkow@1030
   314
            in case splits of
berghofe@7672
   315
                 [] => no_tac state
berghofe@7672
   316
               | (thm, apsns, pos, TB, tt)::_ =>
nipkow@1030
   317
                   (case apsns of
berghofe@7672
   318
                      [] => compose_tac (false, inst_split Ts t tt thm TB state i, 0) i state
berghofe@7672
   319
                    | p::_ => EVERY [lift_tac Ts t p,
berghofe@7672
   320
                                     rtac reflexive_thm (i+1),
berghofe@7672
   321
                                     lift_split_tac] state)
nipkow@1030
   322
            end
paulson@3537
   323
  in COND (has_fewer_prems i) no_tac 
oheimb@5304
   324
          (rtac meta_iffD i THEN lift_split_tac)
clasohm@0
   325
  end;
clasohm@0
   326
clasohm@0
   327
in split_tac end;
berghofe@1721
   328
oheimb@5304
   329
oheimb@5304
   330
val split_tac        = mk_case_split_tac              int_ord;
oheimb@4189
   331
oheimb@5304
   332
val split_inside_tac = mk_case_split_tac (rev_order o int_ord);
oheimb@5304
   333
oheimb@4189
   334
oheimb@4189
   335
(*****************************************************************************
oheimb@4189
   336
   The split-tactic for premises
oheimb@4189
   337
   
oheimb@4189
   338
   splits : list of split-theorems to be tried
oheimb@5304
   339
****************************************************************************)
oheimb@4202
   340
fun split_asm_tac []     = K no_tac
oheimb@4202
   341
  | split_asm_tac splits = 
oheimb@5304
   342
oheimb@4930
   343
  let val cname_list = map (fst o split_thm_info) splits;
oheimb@4189
   344
      fun is_case (a,_) = a mem cname_list;
oheimb@4189
   345
      fun tac (t,i) = 
oheimb@4189
   346
	  let val n = find_index (exists_Const is_case) 
oheimb@4189
   347
				 (Logic.strip_assums_hyp t);
oheimb@4189
   348
	      fun first_prem_is_disj (Const ("==>", _) $ (Const ("Trueprop", _)
oheimb@5304
   349
				 $ (Const (s, _) $ _ $ _ )) $ _ ) = (s=const_or)
oheimb@4202
   350
	      |   first_prem_is_disj (Const("all",_)$Abs(_,_,t)) = 
oheimb@4202
   351
					first_prem_is_disj t
oheimb@4189
   352
	      |   first_prem_is_disj _ = false;
oheimb@5437
   353
      (* does not work properly if the split variable is bound by a quantfier *)
oheimb@4202
   354
	      fun flat_prems_tac i = SUBGOAL (fn (t,i) => 
oheimb@5304
   355
			   (if first_prem_is_disj t
oheimb@5304
   356
			    then EVERY[etac Data.disjE i,rotate_tac ~1 i,
oheimb@5304
   357
				       rotate_tac ~1  (i+1),
oheimb@5304
   358
				       flat_prems_tac (i+1)]
oheimb@5304
   359
			    else all_tac) 
oheimb@5304
   360
			   THEN REPEAT (eresolve_tac [Data.conjE,Data.exE] i)
oheimb@5304
   361
			   THEN REPEAT (dresolve_tac [Data.notnotD]   i)) i;
oheimb@4189
   362
	  in if n<0 then no_tac else DETERM (EVERY'
oheimb@5304
   363
		[rotate_tac n, etac Data.contrapos2,
oheimb@4189
   364
		 split_tac splits, 
oheimb@5304
   365
		 rotate_tac ~1, etac Data.contrapos, rotate_tac ~1, 
oheimb@4202
   366
		 flat_prems_tac] i)
oheimb@4189
   367
	  end;
oheimb@4189
   368
  in SUBGOAL tac
oheimb@4189
   369
  end;
oheimb@4189
   370
wenzelm@8468
   371
wenzelm@8468
   372
wenzelm@8468
   373
(** declare split rules **)
wenzelm@8468
   374
wenzelm@8468
   375
(* addsplits / delsplits *)
wenzelm@8468
   376
oheimb@5304
   377
fun split_name name asm = "split " ^ name ^ (if asm then " asm" else "");
oheimb@4189
   378
oheimb@5304
   379
fun ss addsplits splits =
oheimb@5304
   380
  let fun addsplit (ss,split) =
oheimb@5304
   381
        let val (name,asm) = split_thm_info split
wenzelm@8468
   382
        in Simplifier.addloop(ss,(split_name name asm,
oheimb@5304
   383
		       (if asm then split_asm_tac else split_tac) [split])) end
oheimb@5304
   384
  in foldl addsplit (ss,splits) end;
berghofe@1721
   385
oheimb@5304
   386
fun ss delsplits splits =
oheimb@5304
   387
  let fun delsplit(ss,split) =
oheimb@5304
   388
        let val (name,asm) = split_thm_info split
wenzelm@8468
   389
        in Simplifier.delloop(ss,split_name name asm)
oheimb@5304
   390
  end in foldl delsplit (ss,splits) end;
berghofe@1721
   391
wenzelm@8468
   392
fun Addsplits splits = (Simplifier.simpset_ref() := 
wenzelm@8468
   393
			Simplifier.simpset() addsplits splits);
wenzelm@8468
   394
fun Delsplits splits = (Simplifier.simpset_ref() := 
wenzelm@8468
   395
			Simplifier.simpset() delsplits splits);
wenzelm@8468
   396
wenzelm@8468
   397
wenzelm@8468
   398
(* attributes *)
wenzelm@8468
   399
wenzelm@8468
   400
val splitN = "split";
wenzelm@8468
   401
wenzelm@8468
   402
val split_add_global = Simplifier.change_global_ss (op addsplits);
wenzelm@8468
   403
val split_del_global = Simplifier.change_global_ss (op delsplits);
wenzelm@8468
   404
val split_add_local = Simplifier.change_local_ss (op addsplits);
wenzelm@8468
   405
val split_del_local = Simplifier.change_local_ss (op delsplits);
wenzelm@8468
   406
wenzelm@8634
   407
val split_attr =
wenzelm@8634
   408
 (Attrib.add_del_args split_add_global split_del_global,
wenzelm@8634
   409
  Attrib.add_del_args split_add_local split_del_local);
wenzelm@8634
   410
wenzelm@8634
   411
val setup_attrs =
wenzelm@8634
   412
  Attrib.add_attributes [(splitN, split_attr, "declare splitter rule")];
wenzelm@8634
   413
wenzelm@8468
   414
wenzelm@8468
   415
(* method modifiers *)
wenzelm@8468
   416
wenzelm@8468
   417
val split_modifiers =
wenzelm@8815
   418
 [Args.$$$ splitN -- Args.colon >> K ((I, split_add_local): Method.modifier),
wenzelm@8815
   419
  Args.$$$ splitN -- Args.$$$ "add" -- Args.colon >> K (I, split_add_local),
wenzelm@8815
   420
  Args.$$$ splitN -- Args.$$$ "del" -- Args.colon >> K (I, split_del_local)];
wenzelm@8468
   421
wenzelm@8468
   422
wenzelm@8468
   423
wenzelm@8468
   424
(** theory setup **)
wenzelm@8468
   425
wenzelm@8468
   426
val setup = [setup_attrs];
oheimb@4189
   427
berghofe@1721
   428
end;