src/FOL/simpdata.ML
changeset 9300 ee5c9672d208
parent 8643 331f0c75e3dc
child 9713 2c5b42311eb0
     1.1 --- a/src/FOL/simpdata.ML	Thu Jul 13 11:44:02 2000 +0200
     1.2 +++ b/src/FOL/simpdata.ML	Thu Jul 13 12:56:42 2000 +0200
     1.3 @@ -6,6 +6,50 @@
     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  val True_implies_equals = prove_goal IFOL.thy