src/FOL/simpdata.ML
changeset 9851 e22db9397e17
parent 9713 2c5b42311eb0
child 9889 8802b140334c
     1.1 --- a/src/FOL/simpdata.ML	Tue Sep 05 18:45:51 2000 +0200
     1.2 +++ b/src/FOL/simpdata.ML	Tue Sep 05 18:46:36 2000 +0200
     1.3 @@ -6,49 +6,6 @@
     1.4  Simplification data for FOL
     1.5  *)
     1.6  
     1.7 -(*** Addition of rules to simpsets and clasets simultaneously ***)      (* FIXME move to Provers/clasimp.ML? *)
     1.8 -
     1.9 -infix 4 addIffs delIffs;
    1.10 -
    1.11 -(*Takes UNCONDITIONAL theorems of the form A<->B to 
    1.12 -        the Safe Intr     rule B==>A and 
    1.13 -        the Safe Destruct rule A==>B.
    1.14 -  Also ~A goes to the Safe Elim rule A ==> ?R
    1.15 -  Failing other cases, A is added as a Safe Intr rule*)
    1.16 -local
    1.17 -  fun addIff ((cla, simp), th) = 
    1.18 -      (case FOLogic.dest_Trueprop (#prop (rep_thm th)) of
    1.19 -                (Const("Not", _) $ A) =>
    1.20 -                    cla addSEs [zero_var_indexes (th RS notE)]
    1.21 -              | (Const("op <->", _) $ _ $ _) =>
    1.22 -                    cla addSIs [zero_var_indexes (th RS iffD2)]  
    1.23 -                        addSDs [zero_var_indexes (th RS iffD1)]
    1.24 -              | _ => cla addSIs [th],
    1.25 -       simp addsimps [th])
    1.26 -      handle TERM _ => error ("AddIffs: theorem must be unconditional\n" ^ 
    1.27 -                         string_of_thm th);
    1.28 -
    1.29 -  fun delIff ((cla, simp), th) = 
    1.30 -      (case FOLogic.dest_Trueprop (#prop (rep_thm th)) of
    1.31 -           (Const ("Not", _) $ A) =>
    1.32 -               cla delrules [zero_var_indexes (th RS notE)]
    1.33 -         | (Const("op <->", _) $ _ $ _) =>
    1.34 -               cla delrules [zero_var_indexes (th RS iffD2),
    1.35 -                             cla_make_elim (zero_var_indexes (th RS iffD1))]
    1.36 -         | _ => cla delrules [th],
    1.37 -       simp delsimps [th])
    1.38 -      handle TERM _ => (warning("DelIffs: ignoring conditional theorem\n" ^ 
    1.39 -                                string_of_thm th); (cla, simp));
    1.40 -
    1.41 -  fun store_clasimp (cla, simp) = (claset_ref () := cla; simpset_ref () := simp)
    1.42 -in
    1.43 -val op addIffs = foldl addIff;
    1.44 -val op delIffs = foldl delIff;
    1.45 -fun AddIffs thms = store_clasimp ((claset (), simpset ()) addIffs thms);
    1.46 -fun DelIffs thms = store_clasimp ((claset (), simpset ()) delIffs thms);
    1.47 -end;
    1.48 -
    1.49 -
    1.50  
    1.51  (* Elimination of True from asumptions: *)
    1.52  
    1.53 @@ -391,7 +348,11 @@
    1.54  
    1.55  structure Clasimp = ClasimpFun
    1.56   (structure Simplifier = Simplifier and Splitter = Splitter
    1.57 -   and Classical  = Cla and Blast = Blast);
    1.58 +  and Classical  = Cla and Blast = Blast
    1.59 +  val dest_Trueprop = FOLogic.dest_Trueprop
    1.60 +  val iff_const = FOLogic.iff val not_const = FOLogic.not
    1.61 +  val notE = notE val iffD1 = iffD1 val iffD2 = iffD2
    1.62 +  val cla_make_elim = cla_make_elim);
    1.63  open Clasimp;
    1.64  
    1.65  val FOL_css = (FOL_cs, FOL_ss);