src/HOL/simpdata.ML
changeset 1984 5cf82dc3ce67
parent 1968 daa97cc96feb
child 2022 9d47e2962edd
     1.1 --- a/src/HOL/simpdata.ML	Thu Sep 12 10:36:06 1996 +0200
     1.2 +++ b/src/HOL/simpdata.ML	Thu Sep 12 10:36:51 1996 +0200
     1.3 @@ -6,6 +6,8 @@
     1.4  Instantiation of the generic simplifier
     1.5  *)
     1.6  
     1.7 +section "Simplifier";
     1.8 +
     1.9  open Simplifier;
    1.10  
    1.11  (*** Integration of simplifier with classical reasoner ***)
    1.12 @@ -28,6 +30,49 @@
    1.13  fun auto() = by (Auto_tac());
    1.14  
    1.15  
    1.16 +(*** Addition of rules to simpsets and clasets simultaneously ***)
    1.17 +
    1.18 +(*Takes UNCONDITIONAL theorems of the form A<->B to 
    1.19 +	the Safe Intr     rule B==>A and 
    1.20 +	the Safe Destruct rule A==>B.
    1.21 +  Also ~A goes to the Safe Elim rule A ==> ?R
    1.22 +  Failing other cases, A is added as a Safe Intr rule*)
    1.23 +local
    1.24 +  val iff_const = HOLogic.eq_const HOLogic.boolT;
    1.25 +
    1.26 +  fun addIff th = 
    1.27 +      (case HOLogic.dest_Trueprop (#prop(rep_thm th)) of
    1.28 +		(Const("not",_) $ A) =>
    1.29 +		    AddSEs [zero_var_indexes (th RS notE)]
    1.30 +	      | (con $ _ $ _) =>
    1.31 +		    if con=iff_const
    1.32 +		    then (AddSIs [zero_var_indexes (th RS iffD2)];  
    1.33 +			  AddSDs [zero_var_indexes (th RS iffD1)])
    1.34 +		    else  AddSIs [th]
    1.35 +	      | _ => AddSIs [th];
    1.36 +       Addsimps [th])
    1.37 +      handle _ => error ("AddIffs: theorem must be unconditional\n" ^ 
    1.38 +			 string_of_thm th)
    1.39 +
    1.40 +  fun delIff th = 
    1.41 +      (case HOLogic.dest_Trueprop (#prop(rep_thm th)) of
    1.42 +		(Const("not",_) $ A) =>
    1.43 +		    Delrules [zero_var_indexes (th RS notE)]
    1.44 +	      | (con $ _ $ _) =>
    1.45 +		    if con=iff_const
    1.46 +		    then Delrules [zero_var_indexes (th RS iffD2),
    1.47 +				   zero_var_indexes (th RS iffD1)]
    1.48 +		    else Delrules [th]
    1.49 +	      | _ => Delrules [th];
    1.50 +       Delsimps [th])
    1.51 +      handle _ => warning("DelIffs: ignoring conditional theorem\n" ^ 
    1.52 +			  string_of_thm th)
    1.53 +in
    1.54 +val AddIffs = seq addIff
    1.55 +val DelIffs = seq delIff
    1.56 +end;
    1.57 +
    1.58 +
    1.59  local
    1.60  
    1.61    fun prover s = prove_goal HOL.thy s (fn _ => [fast_tac HOL_cs 1]);
    1.62 @@ -268,3 +313,44 @@
    1.63  
    1.64  qed_goalw "o_assoc" HOL.thy [o_def] "f o (g o h) = (f o g o h)"
    1.65    (fn _=>[rtac ext 1, rtac refl 1]);
    1.66 +
    1.67 +
    1.68 +
    1.69 +
    1.70 +(*** Install simpsets and datatypes in theory structure ***)
    1.71 +
    1.72 +simpset := HOL_ss;
    1.73 +
    1.74 +exception SS_DATA of simpset;
    1.75 +
    1.76 +let fun merge [] = SS_DATA empty_ss
    1.77 +      | merge ss = let val ss = map (fn SS_DATA x => x) ss;
    1.78 +                   in SS_DATA (foldl merge_ss (hd ss, tl ss)) end;
    1.79 +
    1.80 +    fun put (SS_DATA ss) = simpset := ss;
    1.81 +
    1.82 +    fun get () = SS_DATA (!simpset);
    1.83 +in add_thydata "HOL"
    1.84 +     ("simpset", ThyMethods {merge = merge, put = put, get = get})
    1.85 +end;
    1.86 +
    1.87 +type dtype_info = {case_const:term, case_rewrites:thm list,
    1.88 +                   constructors:term list, nchotomy:thm, case_cong:thm};
    1.89 +
    1.90 +exception DT_DATA of (string * dtype_info) list;
    1.91 +val datatypes = ref [] : (string * dtype_info) list ref;
    1.92 +
    1.93 +let fun merge [] = DT_DATA []
    1.94 +      | merge ds =
    1.95 +          let val ds = map (fn DT_DATA x => x) ds;
    1.96 +          in DT_DATA (foldl (gen_union eq_fst) (hd ds, tl ds)) end;
    1.97 +
    1.98 +    fun put (DT_DATA ds) = datatypes := ds;
    1.99 +
   1.100 +    fun get () = DT_DATA (!datatypes);
   1.101 +in add_thydata "HOL"
   1.102 +     ("datatypes", ThyMethods {merge = merge, put = put, get = get})
   1.103 +end;
   1.104 +
   1.105 +
   1.106 +add_thy_reader_file "thy_data.ML";