src/HOL/simpdata.ML
changeset 6514 381fb2b084a4
parent 6394 3d9fd50fcc43
child 6915 4ab8e31a8421
     1.1 --- a/src/HOL/simpdata.ML	Tue Apr 27 10:43:52 1999 +0200
     1.2 +++ b/src/HOL/simpdata.ML	Tue Apr 27 10:44:17 1999 +0200
     1.3 @@ -8,7 +8,7 @@
     1.4  
     1.5  section "Simplifier";
     1.6  
     1.7 -(*** Addition of rules to simpsets and clasets simultaneously ***)
     1.8 +(*** Addition of rules to simpsets and clasets simultaneously ***)	(* FIXME move to Provers/clasimp.ML? *)
     1.9  
    1.10  infix 4 addIffs delIffs;
    1.11  
    1.12 @@ -57,6 +57,38 @@
    1.13  end;
    1.14  
    1.15  
    1.16 +(* "iff" attribute *)
    1.17 +
    1.18 +local
    1.19 +  fun change_global_css f (thy, th) =
    1.20 +    let
    1.21 +      val cs_ref = Classical.claset_ref_of thy;
    1.22 +      val ss_ref = Simplifier.simpset_ref_of thy;
    1.23 +      val (cs', ss') = f ((! cs_ref, ! ss_ref), [th]);
    1.24 +    in cs_ref := cs'; ss_ref := ss'; (thy, th) end;
    1.25 +
    1.26 +  fun change_local_css f (ctxt, th) =
    1.27 +    let
    1.28 +      val cs = Classical.get_local_claset ctxt;
    1.29 +      val ss = Simplifier.get_local_simpset ctxt;
    1.30 +      val (cs', ss') = f ((cs, ss), [th]);
    1.31 +      val ctxt' =
    1.32 +        ctxt
    1.33 +        |> Classical.put_local_claset cs'
    1.34 +        |> Simplifier.put_local_simpset ss';
    1.35 +    in (ctxt', th) end;
    1.36 +in
    1.37 +
    1.38 +val iff_add_global = change_global_css (op addIffs);
    1.39 +val iff_add_local = change_local_css (op addIffs);
    1.40 +
    1.41 +val simpdata_setup =
    1.42 +  [Attrib.add_attributes [("iff", (Attrib.no_args iff_add_global, Attrib.no_args iff_add_local),
    1.43 +    "add rules to simpset and claset simultaneously")]];
    1.44 +
    1.45 +end;
    1.46 +
    1.47 +
    1.48  qed_goal "meta_eq_to_obj_eq" HOL.thy "x==y ==> x=y"
    1.49    (fn [prem] => [rewtac prem, rtac refl 1]);
    1.50