--- a/src/FOLP/simpdata.ML Mon Jan 29 13:56:41 1996 +0100
+++ b/src/FOLP/simpdata.ML Mon Jan 29 13:58:15 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: FOL/simpdata
+(* Title: FOL/simpdata
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
Simplification data for FOL
@@ -15,33 +15,33 @@
fun int_prove_fun s = int_prove_fun_raw ("?p : "^s);
val conj_rews = map int_prove_fun
- ["P & True <-> P", "True & P <-> P",
+ ["P & True <-> P", "True & P <-> P",
"P & False <-> False", "False & P <-> False",
"P & P <-> P",
- "P & ~P <-> False", "~P & P <-> False",
+ "P & ~P <-> False", "~P & P <-> False",
"(P & Q) & R <-> P & (Q & R)"];
val disj_rews = map int_prove_fun
- ["P | True <-> True", "True | P <-> True",
- "P | False <-> P", "False | P <-> P",
+ ["P | True <-> True", "True | P <-> True",
+ "P | False <-> P", "False | P <-> P",
"P | P <-> P",
"(P | Q) | R <-> P | (Q | R)"];
val not_rews = map int_prove_fun
- ["~ False <-> True", "~ True <-> False"];
+ ["~ False <-> True", "~ True <-> False"];
val imp_rews = map int_prove_fun
- ["(P --> False) <-> ~P", "(P --> True) <-> True",
- "(False --> P) <-> True", "(True --> P) <-> P",
- "(P --> P) <-> True", "(P --> ~P) <-> ~P"];
+ ["(P --> False) <-> ~P", "(P --> True) <-> True",
+ "(False --> P) <-> True", "(True --> P) <-> P",
+ "(P --> P) <-> True", "(P --> ~P) <-> ~P"];
val iff_rews = map int_prove_fun
- ["(True <-> P) <-> P", "(P <-> True) <-> P",
+ ["(True <-> P) <-> P", "(P <-> True) <-> P",
"(P <-> P) <-> True",
- "(False <-> P) <-> ~P", "(P <-> False) <-> ~P"];
+ "(False <-> P) <-> ~P", "(P <-> False) <-> ~P"];
val quant_rews = map int_prove_fun
- ["(ALL x.P) <-> P", "(EX x.P) <-> P"];
+ ["(ALL x.P) <-> P", "(EX x.P) <-> P"];
(*These are NOT supplied by default!*)
val distrib_rews = map int_prove_fun
@@ -60,7 +60,7 @@
val refl_iff_T = make_iff_T refl;
val norm_thms = [(norm_eq RS sym, norm_eq),
- (NORM_iff RS iff_sym, NORM_iff)];
+ (NORM_iff RS iff_sym, NORM_iff)];
(* Conversion into rewrite rules *)
@@ -76,7 +76,7 @@
fun atomize th = case concl_of th of (*The operator below is "Proof $ P $ p"*)
_ $ (Const("op -->",_) $ _ $ _) $ _ => atomize(th RS mp)
| _ $ (Const("op &",_) $ _ $ _) $ _ => atomize(th RS conjunct1) @
- atomize(th RS conjunct2)
+ atomize(th RS conjunct2)
| _ $ (Const("All",_) $ _) $ _ => atomize(th RS spec)
| _ $ (Const("True",_)) $ _ => []
| _ $ (Const("False",_)) $ _ => []
@@ -90,15 +90,15 @@
structure FOLP_SimpData : SIMP_DATA =
struct
- val refl_thms = [refl, iff_refl]
- val trans_thms = [trans, iff_trans]
- val red1 = iffD1
- val red2 = iffD2
- val mk_rew_rules = mk_rew_rules
- val case_splits = [] (*NO IF'S!*)
- val norm_thms = norm_thms
- val subst_thms = [subst];
- val dest_red = dest_red
+ val refl_thms = [refl, iff_refl]
+ val trans_thms = [trans, iff_trans]
+ val red1 = iffD1
+ val red2 = iffD2
+ val mk_rew_rules = mk_rew_rules
+ val case_splits = [] (*NO IF'S!*)
+ val norm_thms = norm_thms
+ val subst_thms = [subst];
+ val dest_red = dest_red
end;
structure FOLP_Simp = SimpFun(FOLP_SimpData);
@@ -124,8 +124,8 @@
(fn prems => [ (cut_facts_tac prems 1), (Cla.fast_tac FOLP_cs 1) ]));
val cla_rews = map prove_fun
- ["?p:P | ~P", "?p:~P | P",
- "?p:~ ~ P <-> P", "?p:(~P --> P) <-> P"];
+ ["?p:P | ~P", "?p:~P | P",
+ "?p:~ ~ P <-> P", "?p:(~P --> P) <-> P"];
val FOLP_rews = IFOLP_rews@cla_rews;