--- a/src/FOL/simpdata.ML Thu Mar 17 13:07:48 1994 +0100
+++ b/src/FOL/simpdata.ML Thu Mar 17 13:54:50 1994 +0100
@@ -1,7 +1,7 @@
(* Title: FOL/simpdata
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1991 University of Cambridge
+ Copyright 1994 University of Cambridge
Simplification data for FOL
*)
@@ -9,14 +9,16 @@
(*** Rewrite rules ***)
fun int_prove_fun s =
- (writeln s; prove_goal IFOL.thy s
- (fn prems => [ (cut_facts_tac prems 1), (Int.fast_tac 1) ]));
+ (writeln s;
+ prove_goal IFOL.thy s
+ (fn prems => [ (cut_facts_tac prems 1),
+ (Int.fast_tac 1) ]));
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
@@ -26,7 +28,8 @@
"(P | Q) | R <-> P | (Q | R)"];
val not_rews = map int_prove_fun
- ["~ False <-> True", "~ True <-> False"];
+ ["~(P|Q) <-> ~P & ~Q",
+ "~ False <-> True", "~ True <-> False"];
val imp_rews = map int_prove_fun
["(P --> False) <-> ~P", "(P --> True) <-> True",
@@ -43,79 +46,78 @@
(*These are NOT supplied by default!*)
val distrib_rews = map int_prove_fun
- ["~(P|Q) <-> ~P & ~Q",
- "P & (Q | R) <-> P&Q | P&R", "(Q | R) & P <-> Q&P | R&P",
+ ["P & (Q | R) <-> P&Q | P&R",
+ "(Q | R) & P <-> Q&P | R&P",
"(P | Q --> R) <-> (P --> R) & (Q --> R)"];
-val P_Imp_P_iff_T = int_prove_fun "P ==> (P <-> True)";
-
-fun make_iff_T th = th RS P_Imp_P_iff_T;
-
-val refl_iff_T = make_iff_T refl;
-
-val notFalseI = int_prove_fun "~False";
-
-(* Conversion into rewrite rules *)
-
-val not_P_imp_P_iff_F = int_prove_fun "~P ==> (P <-> False)";
-
-fun mk_meta_eq th = case concl_of th of
- _ $ (Const("op <->",_)$_$_) => th RS iff_reflection
- | _ $ (Const("op =",_)$_$_) => th RS eq_reflection
- | _ $ (Const("Not",_)$_) => (th RS not_P_imp_P_iff_F) RS iff_reflection
- | _ => (make_iff_T th) RS iff_reflection;
-
-fun atomize th = case concl_of th of (*The operator below is Trueprop*)
- _ $ (Const("op -->",_) $ _ $ _) => atomize(th RS mp)
- | _ $ (Const("op &",_) $ _ $ _) => atomize(th RS conjunct1) @
- atomize(th RS conjunct2)
- | _ $ (Const("All",_) $ _) => atomize(th RS spec)
- | _ $ (Const("True",_)) => []
- | _ $ (Const("False",_)) => []
- | _ => [th];
+(** Conversion into rewrite rules **)
fun gen_all th = forall_elim_vars (#maxidx(rep_thm th)+1) th;
-fun mk_rew_rules th = map mk_meta_eq (atomize(gen_all th));
+(*Make atomic rewrite rules*)
+fun atomize th = case concl_of th of
+ _ $ (Const("op &",_) $ _ $ _) => atomize(th RS conjunct1) @
+ atomize(th RS conjunct2)
+ | _ $ (Const("op -->",_) $ _ $ _) => atomize(th RS mp)
+ | _ $ (Const("All",_) $ _) => atomize(th RS spec)
+ | _ $ (Const("True",_)) => []
+ | _ $ (Const("False",_)) => []
+ | _ => [th];
+
+val P_iff_F = int_prove_fun "~P ==> (P <-> False)";
+val iff_reflection_F = P_iff_F RS iff_reflection;
+
+val P_iff_T = int_prove_fun "P ==> (P <-> True)";
+val iff_reflection_T = P_iff_T RS iff_reflection;
+
+(*Make meta-equalities. The operator below is Trueprop*)
+fun mk_meta_eq th = case concl_of th of
+ _ $ (Const("op =",_)$_$_) => th RS eq_reflection
+ | _ $ (Const("op <->",_)$_$_) => th RS iff_reflection
+ | _ $ (Const("Not",_)$_) => th RS iff_reflection_F
+ | _ => th RS iff_reflection_T;
structure Induction = InductionFun(struct val spec=IFOL.spec end);
-val IFOL_rews =
- [refl_iff_T] @ conj_rews @ disj_rews @ not_rews @
- imp_rews @ iff_rews @ quant_rews;
-
open Simplifier Induction;
infix addcongs;
fun ss addcongs congs =
- ss addeqcongs (congs RL [eq_reflection,iff_reflection]);
+ ss addeqcongs (congs RL [eq_reflection,iff_reflection]);
+
+val IFOL_rews =
+ [refl RS P_iff_T] @ conj_rews @ disj_rews @ not_rews @
+ imp_rews @ iff_rews @ quant_rews;
-val IFOL_ss = empty_ss
- setmksimps mk_rew_rules
- setsolver
- (fn prems => resolve_tac (TrueI::refl::iff_refl::notFalseI::prems)
- ORELSE' atac)
- setsubgoaler asm_simp_tac
- addsimps IFOL_rews
- addcongs [imp_cong];
+val notFalseI = int_prove_fun "~False";
+val triv_rls = [TrueI,refl,iff_refl,notFalseI];
+
+val IFOL_ss =
+ empty_ss
+ setmksimps (map mk_meta_eq o atomize o gen_all)
+ setsolver (fn prems => resolve_tac (triv_rls@prems) ORELSE' assume_tac)
+ setsubgoaler asm_simp_tac
+ addsimps IFOL_rews
+ addcongs [imp_cong];
(*Classical version...*)
fun prove_fun s =
- (writeln s; prove_goal FOL.thy s
- (fn prems => [ (cut_facts_tac prems 1), (Cla.fast_tac FOL_cs 1) ]));
-
+ (writeln s;
+ prove_goal FOL.thy s
+ (fn prems => [ (cut_facts_tac prems 1),
+ (Cla.fast_tac FOL_cs 1) ]));
val cla_rews = map prove_fun
- ["P | ~P", "~P | P",
+ ["~(P&Q) <-> ~P | ~Q",
+ "P | ~P", "~P | P",
"~ ~ P <-> P", "(~P --> P) <-> P"];
val FOL_ss = IFOL_ss addsimps cla_rews;
(*** case splitting ***)
-val split_tac =
- let val eq_reflection2 = prove_goal FOL.thy "x==y ==> x=y"
- (fn [prem] => [rewtac prem, rtac refl 1])
- val iff_reflection2 = prove_goal FOL.thy "x==y ==> x<->y"
- (fn [prem] => [rewtac prem, rtac iff_refl 1])
- val [iffD] = [eq_reflection2,iff_reflection2] RL [iffD2]
- in fn splits => mk_case_split_tac iffD (map mk_meta_eq splits) end;
+val meta_iffD =
+ prove_goal FOL.thy "[| P==Q; Q |] ==> P"
+ (fn [prem1,prem2] => [rewtac prem1, rtac prem2 1])
+
+fun split_tac splits =
+ mk_case_split_tac meta_iffD (map mk_meta_eq splits);