src/HOL/simpdata.ML
changeset 5552 dcd3e7711cac
parent 5447 df03d330aeab
child 5975 cd19eaa90f45
     1.1 --- a/src/HOL/simpdata.ML	Thu Sep 24 17:07:24 1998 +0200
     1.2 +++ b/src/HOL/simpdata.ML	Thu Sep 24 17:16:06 1998 +0200
     1.3 @@ -72,16 +72,23 @@
     1.4  
     1.5  in
     1.6  
     1.7 -  fun meta_eq r = r RS eq_reflection;
     1.8 +(*Make meta-equalities.  The operator below is Trueprop*)
     1.9 +
    1.10 +  fun mk_meta_eq r = r RS eq_reflection;
    1.11  
    1.12 -  fun mk_meta_eq th = case concl_of th of
    1.13 +  fun mk_eq th = case concl_of th of
    1.14            Const("==",_)$_$_       => th
    1.15 -      |   _$(Const("op =",_)$_$_) => meta_eq th
    1.16 +      |   _$(Const("op =",_)$_$_) => mk_meta_eq th
    1.17        |   _$(Const("Not",_)$_)    => th RS not_P_imp_P_eq_False
    1.18        |   _                       => th RS P_imp_P_eq_True;
    1.19    (* last 2 lines requires all formulae to be of the from Trueprop(.) *)
    1.20  
    1.21 -  fun mk_meta_eq_True r = Some(r RS meta_eq_to_obj_eq RS P_imp_P_eq_True);
    1.22 +  fun mk_eq_True r = Some(r RS meta_eq_to_obj_eq RS P_imp_P_eq_True);
    1.23 +
    1.24 +  fun mk_meta_cong rl =
    1.25 +    standard(mk_meta_eq(replicate (nprems_of rl) meta_eq_to_obj_eq MRS rl))
    1.26 +    handle THM _ =>
    1.27 +    error("Premises and conclusion of congruence rules must be =-equalities");
    1.28  
    1.29  
    1.30  val simp_thms = map prover
    1.31 @@ -106,21 +113,17 @@
    1.32     "(? x. x=t & P(x)) = P(t)",		(*essential for termination!!*)
    1.33     "(! x. t=x --> P(x)) = P(t)" ];      (*covers a stray case*)
    1.34  
    1.35 -(*Add congruence rules for = (instead of ==) *)
    1.36 -infix 4 addcongs delcongs;
    1.37 +(* Add congruence rules for = (instead of ==) *)
    1.38  
    1.39 -fun mk_meta_cong rl =
    1.40 -  standard(meta_eq(replicate (nprems_of rl) meta_eq_to_obj_eq MRS rl))
    1.41 -  handle THM _ =>
    1.42 -  error("Premises and conclusion of congruence rules must be =-equalities");
    1.43 -
    1.44 +(* ###FIXME: Move to simplifier, 
    1.45 +   taking mk_meta_cong as input, eliminating addeqcongs and deleqcongs *)
    1.46 +infix 4 addcongs delcongs;
    1.47  fun ss addcongs congs = ss addeqcongs (map mk_meta_cong congs);
    1.48 -
    1.49  fun ss delcongs congs = ss deleqcongs (map mk_meta_cong congs);
    1.50 -
    1.51  fun Addcongs congs = (simpset_ref() := simpset() addcongs congs);
    1.52  fun Delcongs congs = (simpset_ref() := simpset() delcongs congs);
    1.53  
    1.54 +
    1.55  val imp_cong = impI RSN
    1.56      (2, prove_goal HOL.thy "(P=P')--> (P'--> (Q=Q'))--> ((P-->Q) = (P'-->Q'))"
    1.57          (fn _=> [Blast_tac 1]) RS mp RS mp);
    1.58 @@ -328,7 +331,7 @@
    1.59  structure SplitterData =
    1.60    struct
    1.61    structure Simplifier = Simplifier
    1.62 -  val mk_meta_eq     = mk_meta_eq
    1.63 +  val mk_eq          = mk_eq
    1.64    val meta_eq_to_iff = meta_eq_to_obj_eq
    1.65    val iffD           = iffD2
    1.66    val disjE          = disjE
    1.67 @@ -382,10 +385,10 @@
    1.68     ("All", [spec]), ("True", []), ("False", []),
    1.69     ("If", [if_bool_eq_conj RS iffD1])];
    1.70  
    1.71 -(* FIXME: move to Provers/simplifier.ML
    1.72 +(* ###FIXME: move to Provers/simplifier.ML
    1.73  val mk_atomize:      (string * thm list) list -> thm -> thm list
    1.74  *)
    1.75 -(* FIXME: move to Provers/simplifier.ML*)
    1.76 +(* ###FIXME: move to Provers/simplifier.ML *)
    1.77  fun mk_atomize pairs =
    1.78    let fun atoms th =
    1.79          (case concl_of th of
    1.80 @@ -399,7 +402,7 @@
    1.81           | _ => [th])
    1.82    in atoms end;
    1.83  
    1.84 -fun mksimps pairs = (map mk_meta_eq o mk_atomize pairs o gen_all);
    1.85 +fun mksimps pairs = (map mk_eq o mk_atomize pairs o gen_all);
    1.86  
    1.87  fun unsafe_solver prems = FIRST'[resolve_tac (reflexive_thm::TrueI::refl::prems),
    1.88  				 atac, etac FalseE];
    1.89 @@ -411,7 +414,7 @@
    1.90  			    setSSolver   safe_solver
    1.91  			    setSolver  unsafe_solver
    1.92  			    setmksimps (mksimps mksimps_pairs)
    1.93 -			    setmkeqTrue mk_meta_eq_True;
    1.94 +			    setmkeqTrue mk_eq_True;
    1.95  
    1.96  val HOL_ss = 
    1.97      HOL_basic_ss addsimps 
    1.98 @@ -454,10 +457,9 @@
    1.99  (*** integration of simplifier with classical reasoner ***)
   1.100  
   1.101  structure Clasimp = ClasimpFun
   1.102 - (structure Simplifier = Simplifier and Classical = Classical and Blast = Blast
   1.103 -  val op addcongs = op addcongs and op delcongs = op delcongs
   1.104 -  and op addSaltern = op addSaltern and op addbefore = op addbefore);
   1.105 -
   1.106 + (structure Simplifier = Simplifier 
   1.107 +        and Classical  = Classical 
   1.108 +        and Blast      = Blast);
   1.109  open Clasimp;
   1.110  
   1.111  val HOL_css = (HOL_cs, HOL_ss);