change_global/local_css move to Provers/clasimp.ML;
authorwenzelm
Fri Mar 31 22:00:36 2000 +0200 (2000-03-31)
changeset 8641978db2870862
parent 8640 2f9b008a27a1
child 8642 140883a538c1
change_global/local_css move to Provers/clasimp.ML;
fixed 'iff' att syntax;
added 'cong' att;
src/HOL/simpdata.ML
     1.1 --- a/src/HOL/simpdata.ML	Fri Mar 31 21:59:37 2000 +0200
     1.2 +++ b/src/HOL/simpdata.ML	Fri Mar 31 22:00:36 2000 +0200
     1.3 @@ -57,38 +57,6 @@
     1.4  end;
     1.5  
     1.6  
     1.7 -(* "iff" attribute *)
     1.8 -
     1.9 -local
    1.10 -  fun change_global_css f (thy, th) =
    1.11 -    let
    1.12 -      val cs_ref = Classical.claset_ref_of thy;
    1.13 -      val ss_ref = Simplifier.simpset_ref_of thy;
    1.14 -      val (cs', ss') = f ((! cs_ref, ! ss_ref), [th]);
    1.15 -    in cs_ref := cs'; ss_ref := ss'; (thy, th) end;
    1.16 -
    1.17 -  fun change_local_css f (ctxt, th) =
    1.18 -    let
    1.19 -      val cs = Classical.get_local_claset ctxt;
    1.20 -      val ss = Simplifier.get_local_simpset ctxt;
    1.21 -      val (cs', ss') = f ((cs, ss), [th]);
    1.22 -      val ctxt' =
    1.23 -        ctxt
    1.24 -        |> Classical.put_local_claset cs'
    1.25 -        |> Simplifier.put_local_simpset ss';
    1.26 -    in (ctxt', th) end;
    1.27 -in
    1.28 -
    1.29 -val iff_add_global = change_global_css (op addIffs);
    1.30 -val iff_add_local = change_local_css (op addIffs);
    1.31 -
    1.32 -val iff_attrib_setup =
    1.33 -  [Attrib.add_attributes [("iff", (Attrib.no_args iff_add_global, Attrib.no_args iff_add_local),
    1.34 -    "add rules to simpset and claset simultaneously")]];
    1.35 -
    1.36 -end;
    1.37 -
    1.38 -
    1.39  val [prem] = goal (the_context ()) "x==y ==> x=y";
    1.40  by (rewtac prem);
    1.41  by (rtac refl 1);
    1.42 @@ -155,6 +123,13 @@
    1.43  fun Addcongs congs = (simpset_ref() := simpset() addcongs congs);
    1.44  fun Delcongs congs = (simpset_ref() := simpset() delcongs congs);
    1.45  
    1.46 +val cong_add_global = Simplifier.change_global_ss (op addcongs);
    1.47 +val cong_add_local = Simplifier.change_local_ss (op addcongs);
    1.48 +
    1.49 +val cong_attrib_setup =
    1.50 +  [Attrib.add_attributes [("cong", (Attrib.no_args cong_add_global, Attrib.no_args cong_add_local),
    1.51 +    "add rules to simpset and claset simultaneously")]];
    1.52 +
    1.53  
    1.54  val imp_cong = impI RSN
    1.55      (2, prove_goal (the_context ()) "(P=P')--> (P'--> (Q=Q'))--> ((P-->Q) = (P'-->Q'))"
    1.56 @@ -524,6 +499,17 @@
    1.57  val HOL_css = (HOL_cs, HOL_ss);
    1.58  
    1.59  
    1.60 +(* "iff" attribute *)
    1.61 +
    1.62 +val iff_add_global = Clasimp.change_global_css (op addIffs);
    1.63 +val iff_add_local = Clasimp.change_local_css (op addIffs);
    1.64 +
    1.65 +val iff_attrib_setup =
    1.66 +  [Attrib.add_attributes [("iff", (Attrib.no_args iff_add_global, Attrib.no_args iff_add_local),
    1.67 +    "add rules to simpset and claset simultaneously")]];
    1.68 +
    1.69 +
    1.70 +
    1.71  (*** A general refutation procedure ***)
    1.72   
    1.73  (* Parameters: