src/FOL/simpdata.ML
changeset 5555 4b9386224084
parent 5496 42d13691be86
child 6114 45958e54d72e
     1.1 --- a/src/FOL/simpdata.ML	Thu Sep 24 17:17:56 1998 +0200
     1.2 +++ b/src/FOL/simpdata.ML	Thu Sep 24 17:18:33 1998 +0200
     1.3 @@ -76,21 +76,31 @@
     1.4  val iff_reflection_T = P_iff_T RS iff_reflection;
     1.5  
     1.6  (*Make meta-equalities.  The operator below is Trueprop*)
     1.7 +
     1.8  fun mk_meta_eq th = case concl_of th of
     1.9 +    _ $ (Const("op =",_)$_$_)   => th RS eq_reflection
    1.10 +  | _ $ (Const("op <->",_)$_$_) => th RS iff_reflection
    1.11 +  | _                           => 
    1.12 +  error("conclusion must be a =-equality or <->");;
    1.13 +
    1.14 +fun mk_eq th = case concl_of th of
    1.15      Const("==",_)$_$_           => th
    1.16 -  | _ $ (Const("op =",_)$_$_)   => th RS eq_reflection
    1.17 -  | _ $ (Const("op <->",_)$_$_) => th RS iff_reflection
    1.18 +  | _ $ (Const("op =",_)$_$_)   => mk_meta_eq th
    1.19 +  | _ $ (Const("op <->",_)$_$_) => mk_meta_eq th
    1.20    | _ $ (Const("Not",_)$_)      => th RS iff_reflection_F
    1.21    | _                           => th RS iff_reflection_T;
    1.22  
    1.23 +fun mk_meta_cong rl = standard (mk_meta_eq rl); 
    1.24 +(*FIXME: how about the premises?*)
    1.25 +
    1.26  val mksimps_pairs =
    1.27    [("op -->", [mp]), ("op &", [conjunct1,conjunct2]),
    1.28     ("All", [spec]), ("True", []), ("False", [])];
    1.29  
    1.30 -(* FIXME: move to Provers/simplifier.ML
    1.31 +(* ###FIXME: move to Provers/simplifier.ML
    1.32  val mk_atomize:      (string * thm list) list -> thm -> thm list
    1.33  *)
    1.34 -(* FIXME: move to Provers/simplifier.ML*)
    1.35 +(* ###FIXME: move to Provers/simplifier.ML *)
    1.36  fun mk_atomize pairs =
    1.37    let fun atoms th =
    1.38          (case concl_of th of
    1.39 @@ -104,7 +114,7 @@
    1.40           | _ => [th])
    1.41    in atoms end;
    1.42  
    1.43 -fun mksimps pairs = (map mk_meta_eq o mk_atomize pairs o gen_all);
    1.44 +fun mksimps pairs = (map mk_eq o mk_atomize pairs o gen_all);
    1.45  
    1.46  (*** Classical laws ***)
    1.47  
    1.48 @@ -252,7 +262,7 @@
    1.49  structure SplitterData =
    1.50    struct
    1.51    structure Simplifier = Simplifier
    1.52 -  val mk_meta_eq     = mk_meta_eq
    1.53 +  val mk_eq          = mk_eq
    1.54    val meta_eq_to_iff = meta_eq_to_iff
    1.55    val iffD           = iffD2
    1.56    val disjE          = disjE
    1.57 @@ -280,13 +290,14 @@
    1.58  
    1.59  open Induction;
    1.60  
    1.61 -(*Add congruence rules for = or <-> (instead of ==) *)
    1.62 +
    1.63 +(* Add congruence rules for = or <-> (instead of ==) *)
    1.64 +
    1.65 +(* ###FIXME: Move to simplifier, 
    1.66 +   taking mk_meta_cong as input, eliminating addeqcongs and deleqcongs *)
    1.67  infix 4 addcongs delcongs;
    1.68 -fun ss addcongs congs =
    1.69 -        ss addeqcongs (map standard (congs RL [eq_reflection,iff_reflection]));
    1.70 -fun ss delcongs congs =
    1.71 -        ss deleqcongs (map standard (congs RL [eq_reflection,iff_reflection]));
    1.72 -
    1.73 +fun ss addcongs congs = ss addeqcongs (map mk_meta_cong congs);
    1.74 +fun ss delcongs congs = ss deleqcongs (map mk_meta_cong congs);
    1.75  fun Addcongs congs = (simpset_ref() := simpset() addcongs congs);
    1.76  fun Delcongs congs = (simpset_ref() := simpset() delcongs congs);
    1.77  
    1.78 @@ -342,10 +353,9 @@
    1.79  (*** integration of simplifier with classical reasoner ***)
    1.80  
    1.81  structure Clasimp = ClasimpFun
    1.82 - (structure Simplifier = Simplifier and Classical = Cla and Blast = Blast
    1.83 -  val op addcongs = op addcongs and op delcongs = op delcongs
    1.84 -  and op addSaltern = op addSaltern and op addbefore = op addbefore);
    1.85 -
    1.86 + (structure Simplifier = Simplifier 
    1.87 +        and Classical  = Cla
    1.88 +        and Blast      = Blast);
    1.89  open Clasimp;
    1.90  
    1.91  val FOL_css = (FOL_cs, FOL_ss);