iff declarations moved to clasimp.ML;
authorwenzelm
Tue Sep 05 18:46:36 2000 +0200 (2000-09-05 ago)
changeset 9851e22db9397e17
parent 9850 bee6eb4b6a42
child 9852 6ca7fcac3e23
iff declarations moved to clasimp.ML;
src/FOL/simpdata.ML
src/HOL/simpdata.ML
     1.1 --- a/src/FOL/simpdata.ML	Tue Sep 05 18:45:51 2000 +0200
     1.2 +++ b/src/FOL/simpdata.ML	Tue Sep 05 18:46:36 2000 +0200
     1.3 @@ -6,49 +6,6 @@
     1.4  Simplification data for FOL
     1.5  *)
     1.6  
     1.7 -(*** Addition of rules to simpsets and clasets simultaneously ***)      (* FIXME move to Provers/clasimp.ML? *)
     1.8 -
     1.9 -infix 4 addIffs delIffs;
    1.10 -
    1.11 -(*Takes UNCONDITIONAL theorems of the form A<->B to 
    1.12 -        the Safe Intr     rule B==>A and 
    1.13 -        the Safe Destruct rule A==>B.
    1.14 -  Also ~A goes to the Safe Elim rule A ==> ?R
    1.15 -  Failing other cases, A is added as a Safe Intr rule*)
    1.16 -local
    1.17 -  fun addIff ((cla, simp), th) = 
    1.18 -      (case FOLogic.dest_Trueprop (#prop (rep_thm th)) of
    1.19 -                (Const("Not", _) $ A) =>
    1.20 -                    cla addSEs [zero_var_indexes (th RS notE)]
    1.21 -              | (Const("op <->", _) $ _ $ _) =>
    1.22 -                    cla addSIs [zero_var_indexes (th RS iffD2)]  
    1.23 -                        addSDs [zero_var_indexes (th RS iffD1)]
    1.24 -              | _ => cla addSIs [th],
    1.25 -       simp addsimps [th])
    1.26 -      handle TERM _ => error ("AddIffs: theorem must be unconditional\n" ^ 
    1.27 -                         string_of_thm th);
    1.28 -
    1.29 -  fun delIff ((cla, simp), th) = 
    1.30 -      (case FOLogic.dest_Trueprop (#prop (rep_thm th)) of
    1.31 -           (Const ("Not", _) $ A) =>
    1.32 -               cla delrules [zero_var_indexes (th RS notE)]
    1.33 -         | (Const("op <->", _) $ _ $ _) =>
    1.34 -               cla delrules [zero_var_indexes (th RS iffD2),
    1.35 -                             cla_make_elim (zero_var_indexes (th RS iffD1))]
    1.36 -         | _ => cla delrules [th],
    1.37 -       simp delsimps [th])
    1.38 -      handle TERM _ => (warning("DelIffs: ignoring conditional theorem\n" ^ 
    1.39 -                                string_of_thm th); (cla, simp));
    1.40 -
    1.41 -  fun store_clasimp (cla, simp) = (claset_ref () := cla; simpset_ref () := simp)
    1.42 -in
    1.43 -val op addIffs = foldl addIff;
    1.44 -val op delIffs = foldl delIff;
    1.45 -fun AddIffs thms = store_clasimp ((claset (), simpset ()) addIffs thms);
    1.46 -fun DelIffs thms = store_clasimp ((claset (), simpset ()) delIffs thms);
    1.47 -end;
    1.48 -
    1.49 -
    1.50  
    1.51  (* Elimination of True from asumptions: *)
    1.52  
    1.53 @@ -391,7 +348,11 @@
    1.54  
    1.55  structure Clasimp = ClasimpFun
    1.56   (structure Simplifier = Simplifier and Splitter = Splitter
    1.57 -   and Classical  = Cla and Blast = Blast);
    1.58 +  and Classical  = Cla and Blast = Blast
    1.59 +  val dest_Trueprop = FOLogic.dest_Trueprop
    1.60 +  val iff_const = FOLogic.iff val not_const = FOLogic.not
    1.61 +  val notE = notE val iffD1 = iffD1 val iffD2 = iffD2
    1.62 +  val cla_make_elim = cla_make_elim);
    1.63  open Clasimp;
    1.64  
    1.65  val FOL_css = (FOL_cs, FOL_ss);
     2.1 --- a/src/HOL/simpdata.ML	Tue Sep 05 18:45:51 2000 +0200
     2.2 +++ b/src/HOL/simpdata.ML	Tue Sep 05 18:46:36 2000 +0200
     2.3 @@ -8,56 +8,6 @@
     2.4  
     2.5  section "Simplifier";
     2.6  
     2.7 -(*** Addition of rules to simpsets and clasets simultaneously ***)      (* FIXME move to Provers/clasimp.ML? *)
     2.8 -
     2.9 -infix 4 addIffs delIffs;
    2.10 -
    2.11 -(*Takes UNCONDITIONAL theorems of the form A<->B to
    2.12 -        the Safe Intr     rule B==>A and
    2.13 -        the Safe Destruct rule A==>B.
    2.14 -  Also ~A goes to the Safe Elim rule A ==> ?R
    2.15 -  Failing other cases, A is added as a Safe Intr rule*)
    2.16 -local
    2.17 -  val iff_const = HOLogic.eq_const HOLogic.boolT;
    2.18 -
    2.19 -  fun addIff ((cla, simp), th) =
    2.20 -      (case HOLogic.dest_Trueprop (#prop (rep_thm th)) of
    2.21 -                (Const("Not", _) $ A) =>
    2.22 -                    cla addSEs [zero_var_indexes (th RS notE)]
    2.23 -              | (con $ _ $ _) =>
    2.24 -                    if con = iff_const
    2.25 -                    then cla addSIs [zero_var_indexes (th RS iffD2)]
    2.26 -                              addSDs [zero_var_indexes (th RS iffD1)]
    2.27 -                    else  cla addSIs [th]
    2.28 -              | _ => cla addSIs [th],
    2.29 -       simp addsimps [th])
    2.30 -      handle TERM _ => error ("AddIffs: theorem must be unconditional\n" ^
    2.31 -                         string_of_thm th);
    2.32 -
    2.33 -  fun delIff ((cla, simp), th) =
    2.34 -      (case HOLogic.dest_Trueprop (#prop (rep_thm th)) of
    2.35 -           (Const ("Not", _) $ A) =>
    2.36 -               cla delrules [zero_var_indexes (th RS notE)]
    2.37 -         | (con $ _ $ _) =>
    2.38 -               if con = iff_const
    2.39 -               then cla delrules
    2.40 -                        [zero_var_indexes (th RS iffD2),
    2.41 -                         cla_make_elim (zero_var_indexes (th RS iffD1))]
    2.42 -               else cla delrules [th]
    2.43 -         | _ => cla delrules [th],
    2.44 -       simp delsimps [th])
    2.45 -      handle TERM _ => (warning("DelIffs: ignoring conditional theorem\n" ^
    2.46 -                                string_of_thm th); (cla, simp));
    2.47 -
    2.48 -  fun store_clasimp (cla, simp) = (claset_ref () := cla; simpset_ref () := simp)
    2.49 -in
    2.50 -val op addIffs = foldl addIff;
    2.51 -val op delIffs = foldl delIff;
    2.52 -fun AddIffs thms = store_clasimp ((claset (), simpset ()) addIffs thms);
    2.53 -fun DelIffs thms = store_clasimp ((claset (), simpset ()) delIffs thms);
    2.54 -end;
    2.55 -
    2.56 -
    2.57  val [prem] = goal (the_context ()) "x==y ==> x=y";
    2.58  by (rewtac prem);
    2.59  by (rtac refl 1);
    2.60 @@ -306,8 +256,8 @@
    2.61  
    2.62  (*** make simplification procedures for quantifier elimination ***)
    2.63  
    2.64 -structure Quantifier1 = Quantifier1Fun(
    2.65 -struct
    2.66 +structure Quantifier1 = Quantifier1Fun
    2.67 +(struct
    2.68    (*abstract syntax*)
    2.69    fun dest_eq((c as Const("op =",_)) $ s $ t) = Some(c,s,t)
    2.70      | dest_eq _ = None;
    2.71 @@ -507,7 +457,7 @@
    2.72  
    2.73  in
    2.74  
    2.75 -val attrib_setup =
    2.76 +val rulify_attrib_setup =
    2.77   [Attrib.add_attributes
    2.78    [("rulify", (gen_rulify, gen_rulify), "put theorem into standard rule form")]];
    2.79  
    2.80 @@ -517,26 +467,17 @@
    2.81  
    2.82  structure Clasimp = ClasimpFun
    2.83   (structure Simplifier = Simplifier and Splitter = Splitter
    2.84 -   and Classical  = Classical and Blast = Blast);
    2.85 +  and Classical  = Classical and Blast = Blast
    2.86 +  val dest_Trueprop = HOLogic.dest_Trueprop
    2.87 +  val iff_const = HOLogic.eq_const HOLogic.boolT
    2.88 +  val not_const = HOLogic.not_const
    2.89 +  val notE = notE val iffD1 = iffD1 val iffD2 = iffD2
    2.90 +  val cla_make_elim = cla_make_elim);
    2.91  open Clasimp;
    2.92  
    2.93  val HOL_css = (HOL_cs, HOL_ss);
    2.94  
    2.95  
    2.96 -(* "iff" attribute *)
    2.97 -
    2.98 -val iff_add_global = Clasimp.change_global_css (op addIffs);
    2.99 -val iff_del_global = Clasimp.change_global_css (op delIffs);
   2.100 -val iff_add_local = Clasimp.change_local_css (op addIffs);
   2.101 -val iff_del_local = Clasimp.change_local_css (op delIffs);
   2.102 -
   2.103 -val iff_attrib_setup =
   2.104 - [Attrib.add_attributes
   2.105 -  [("iff", (Attrib.add_del_args iff_add_global iff_del_global,
   2.106 -    Attrib.add_del_args iff_add_local iff_del_local),
   2.107 -    "declare simplifier / classical rules")]];
   2.108 -
   2.109 -
   2.110  
   2.111  (*** A general refutation procedure ***)
   2.112