src/FOL/simpdata.ML
changeset 9300 ee5c9672d208
parent 8643 331f0c75e3dc
child 9713 2c5b42311eb0
equal deleted inserted replaced
9299:c5cda71de65d 9300:ee5c9672d208
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1994  University of Cambridge
     4     Copyright   1994  University of Cambridge
     5 
     5 
     6 Simplification data for FOL
     6 Simplification data for FOL
     7 *)
     7 *)
       
     8 
       
     9 (*** Addition of rules to simpsets and clasets simultaneously ***)	(* FIXME move to Provers/clasimp.ML? *)
       
    10 
       
    11 infix 4 addIffs delIffs;
       
    12 
       
    13 (*Takes UNCONDITIONAL theorems of the form A<->B to 
       
    14         the Safe Intr     rule B==>A and 
       
    15         the Safe Destruct rule A==>B.
       
    16   Also ~A goes to the Safe Elim rule A ==> ?R
       
    17   Failing other cases, A is added as a Safe Intr rule*)
       
    18 local
       
    19   fun addIff ((cla, simp), th) = 
       
    20       (case FOLogic.dest_Trueprop (#prop (rep_thm th)) of
       
    21                 (Const("Not", _) $ A) =>
       
    22                     cla addSEs [zero_var_indexes (th RS notE)]
       
    23               | (Const("op <->", _) $ _ $ _) =>
       
    24                     cla addSIs [zero_var_indexes (th RS iffD2)]  
       
    25                         addSDs [zero_var_indexes (th RS iffD1)]
       
    26               | _ => cla addSIs [th],
       
    27        simp addsimps [th])
       
    28       handle TERM _ => error ("AddIffs: theorem must be unconditional\n" ^ 
       
    29                          string_of_thm th);
       
    30 
       
    31   fun delIff ((cla, simp), th) = 
       
    32       (case FOLogic.dest_Trueprop (#prop (rep_thm th)) of
       
    33 	   (Const ("Not", _) $ A) =>
       
    34 	       cla delrules [zero_var_indexes (th RS notE)]
       
    35 	 | (Const("op <->", _) $ _ $ _) =>
       
    36 	       cla delrules [zero_var_indexes (th RS iffD2),
       
    37 			     cla_make_elim (zero_var_indexes (th RS iffD1))]
       
    38 	 | _ => cla delrules [th],
       
    39        simp delsimps [th])
       
    40       handle TERM _ => (warning("DelIffs: ignoring conditional theorem\n" ^ 
       
    41 				string_of_thm th); (cla, simp));
       
    42 
       
    43   fun store_clasimp (cla, simp) = (claset_ref () := cla; simpset_ref () := simp)
       
    44 in
       
    45 val op addIffs = foldl addIff;
       
    46 val op delIffs = foldl delIff;
       
    47 fun AddIffs thms = store_clasimp ((claset (), simpset ()) addIffs thms);
       
    48 fun DelIffs thms = store_clasimp ((claset (), simpset ()) delIffs thms);
       
    49 end;
       
    50 
       
    51 
     8 
    52 
     9 (* Elimination of True from asumptions: *)
    53 (* Elimination of True from asumptions: *)
    10 
    54 
    11 val True_implies_equals = prove_goal IFOL.thy
    55 val True_implies_equals = prove_goal IFOL.thy
    12  "(True ==> PROP P) == PROP P"
    56  "(True ==> PROP P) == PROP P"