--- a/src/FOL/simpdata.ML Tue Sep 05 18:45:51 2000 +0200
+++ b/src/FOL/simpdata.ML Tue Sep 05 18:46:36 2000 +0200
@@ -6,49 +6,6 @@
Simplification data for FOL
*)
-(*** Addition of rules to simpsets and clasets simultaneously ***) (* FIXME move to Provers/clasimp.ML? *)
-
-infix 4 addIffs delIffs;
-
-(*Takes UNCONDITIONAL theorems of the form A<->B to
- the Safe Intr rule B==>A and
- the Safe Destruct rule A==>B.
- Also ~A goes to the Safe Elim rule A ==> ?R
- Failing other cases, A is added as a Safe Intr rule*)
-local
- fun addIff ((cla, simp), th) =
- (case FOLogic.dest_Trueprop (#prop (rep_thm th)) of
- (Const("Not", _) $ A) =>
- cla addSEs [zero_var_indexes (th RS notE)]
- | (Const("op <->", _) $ _ $ _) =>
- cla addSIs [zero_var_indexes (th RS iffD2)]
- addSDs [zero_var_indexes (th RS iffD1)]
- | _ => cla addSIs [th],
- simp addsimps [th])
- handle TERM _ => error ("AddIffs: theorem must be unconditional\n" ^
- string_of_thm th);
-
- fun delIff ((cla, simp), th) =
- (case FOLogic.dest_Trueprop (#prop (rep_thm th)) of
- (Const ("Not", _) $ A) =>
- cla delrules [zero_var_indexes (th RS notE)]
- | (Const("op <->", _) $ _ $ _) =>
- cla delrules [zero_var_indexes (th RS iffD2),
- cla_make_elim (zero_var_indexes (th RS iffD1))]
- | _ => cla delrules [th],
- simp delsimps [th])
- handle TERM _ => (warning("DelIffs: ignoring conditional theorem\n" ^
- string_of_thm th); (cla, simp));
-
- fun store_clasimp (cla, simp) = (claset_ref () := cla; simpset_ref () := simp)
-in
-val op addIffs = foldl addIff;
-val op delIffs = foldl delIff;
-fun AddIffs thms = store_clasimp ((claset (), simpset ()) addIffs thms);
-fun DelIffs thms = store_clasimp ((claset (), simpset ()) delIffs thms);
-end;
-
-
(* Elimination of True from asumptions: *)
@@ -391,7 +348,11 @@
structure Clasimp = ClasimpFun
(structure Simplifier = Simplifier and Splitter = Splitter
- and Classical = Cla and Blast = Blast);
+ and Classical = Cla and Blast = Blast
+ val dest_Trueprop = FOLogic.dest_Trueprop
+ val iff_const = FOLogic.iff val not_const = FOLogic.not
+ val notE = notE val iffD1 = iffD1 val iffD2 = iffD2
+ val cla_make_elim = cla_make_elim);
open Clasimp;
val FOL_css = (FOL_cs, FOL_ss);
--- a/src/HOL/simpdata.ML Tue Sep 05 18:45:51 2000 +0200
+++ b/src/HOL/simpdata.ML Tue Sep 05 18:46:36 2000 +0200
@@ -8,56 +8,6 @@
section "Simplifier";
-(*** Addition of rules to simpsets and clasets simultaneously ***) (* FIXME move to Provers/clasimp.ML? *)
-
-infix 4 addIffs delIffs;
-
-(*Takes UNCONDITIONAL theorems of the form A<->B to
- the Safe Intr rule B==>A and
- the Safe Destruct rule A==>B.
- Also ~A goes to the Safe Elim rule A ==> ?R
- Failing other cases, A is added as a Safe Intr rule*)
-local
- val iff_const = HOLogic.eq_const HOLogic.boolT;
-
- fun addIff ((cla, simp), th) =
- (case HOLogic.dest_Trueprop (#prop (rep_thm th)) of
- (Const("Not", _) $ A) =>
- cla addSEs [zero_var_indexes (th RS notE)]
- | (con $ _ $ _) =>
- if con = iff_const
- then cla addSIs [zero_var_indexes (th RS iffD2)]
- addSDs [zero_var_indexes (th RS iffD1)]
- else cla addSIs [th]
- | _ => cla addSIs [th],
- simp addsimps [th])
- handle TERM _ => error ("AddIffs: theorem must be unconditional\n" ^
- string_of_thm th);
-
- fun delIff ((cla, simp), th) =
- (case HOLogic.dest_Trueprop (#prop (rep_thm th)) of
- (Const ("Not", _) $ A) =>
- cla delrules [zero_var_indexes (th RS notE)]
- | (con $ _ $ _) =>
- if con = iff_const
- then cla delrules
- [zero_var_indexes (th RS iffD2),
- cla_make_elim (zero_var_indexes (th RS iffD1))]
- else cla delrules [th]
- | _ => cla delrules [th],
- simp delsimps [th])
- handle TERM _ => (warning("DelIffs: ignoring conditional theorem\n" ^
- string_of_thm th); (cla, simp));
-
- fun store_clasimp (cla, simp) = (claset_ref () := cla; simpset_ref () := simp)
-in
-val op addIffs = foldl addIff;
-val op delIffs = foldl delIff;
-fun AddIffs thms = store_clasimp ((claset (), simpset ()) addIffs thms);
-fun DelIffs thms = store_clasimp ((claset (), simpset ()) delIffs thms);
-end;
-
-
val [prem] = goal (the_context ()) "x==y ==> x=y";
by (rewtac prem);
by (rtac refl 1);
@@ -306,8 +256,8 @@
(*** make simplification procedures for quantifier elimination ***)
-structure Quantifier1 = Quantifier1Fun(
-struct
+structure Quantifier1 = Quantifier1Fun
+(struct
(*abstract syntax*)
fun dest_eq((c as Const("op =",_)) $ s $ t) = Some(c,s,t)
| dest_eq _ = None;
@@ -507,7 +457,7 @@
in
-val attrib_setup =
+val rulify_attrib_setup =
[Attrib.add_attributes
[("rulify", (gen_rulify, gen_rulify), "put theorem into standard rule form")]];
@@ -517,26 +467,17 @@
structure Clasimp = ClasimpFun
(structure Simplifier = Simplifier and Splitter = Splitter
- and Classical = Classical and Blast = Blast);
+ and Classical = Classical and Blast = Blast
+ val dest_Trueprop = HOLogic.dest_Trueprop
+ val iff_const = HOLogic.eq_const HOLogic.boolT
+ val not_const = HOLogic.not_const
+ val notE = notE val iffD1 = iffD1 val iffD2 = iffD2
+ val cla_make_elim = cla_make_elim);
open Clasimp;
val HOL_css = (HOL_cs, HOL_ss);
-(* "iff" attribute *)
-
-val iff_add_global = Clasimp.change_global_css (op addIffs);
-val iff_del_global = Clasimp.change_global_css (op delIffs);
-val iff_add_local = Clasimp.change_local_css (op addIffs);
-val iff_del_local = Clasimp.change_local_css (op delIffs);
-
-val iff_attrib_setup =
- [Attrib.add_attributes
- [("iff", (Attrib.add_del_args iff_add_global iff_del_global,
- Attrib.add_del_args iff_add_local iff_del_local),
- "declare simplifier / classical rules")]];
-
-
(*** A general refutation procedure ***)