# HG changeset patch # User lcp # Date 763908890 -3600 # Node ID 731b27c90d2f3358d09b63ad02a2de09a1a7b20b # Parent f1f96b9e6285374cfdc63705119f68967256502c FOL/simpdata: tidied FOL/simpdata/not_rews: moved the law "~(P|Q) <-> ~P & ~Q" from distrib_rews FOL/simpdata/cla_rews: added the law "~(P&Q) <-> ~P | ~Q" diff -r f1f96b9e6285 -r 731b27c90d2f src/FOL/simpdata.ML --- 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);