# HG changeset patch # User paulson # Date 866640691 -7200 # Node ID a14e5451f613f40b57f68ae300e7e184d1a7b2e0 # Parent 96fcfbfa4fb58218712f9b8eea55de070759343d Addition of not_imp (which pushes negation into implication) as a default simprule diff -r 96fcfbfa4fb5 -r a14e5451f613 src/HOL/WF_Rel.ML --- a/src/HOL/WF_Rel.ML Wed Jun 18 15:30:32 1997 +0200 +++ b/src/HOL/WF_Rel.ML Wed Jun 18 15:31:31 1997 +0200 @@ -129,13 +129,8 @@ by(eres_inst_tac [("x","{w. ? i. w=f i}")] allE 1); by(Blast_tac 1); be swap 1; -by(Asm_full_simp_tac 1); -be exE 1; -be swap 1; -br impI 1; -be swap 1; -be exE 1; -by(rename_tac "x" 1); +by (Asm_full_simp_tac 1); +by (Step_tac 1); by(subgoal_tac "!n. nat_rec x (%i y. @z. z:Q & (z,y):r) n : Q" 1); by (res_inst_tac[("x","nat_rec x (%i y. @z. z:Q & (z,y):r)")]exI 1); br allI 1; diff -r 96fcfbfa4fb5 -r a14e5451f613 src/HOL/simpdata.ML --- a/src/HOL/simpdata.ML Wed Jun 18 15:30:32 1997 +0200 +++ b/src/HOL/simpdata.ML Wed Jun 18 15:31:31 1997 +0200 @@ -177,6 +177,7 @@ prove "de_Morgan_disj" "(~(P | Q)) = (~P & ~Q)"; prove "de_Morgan_conj" "(~(P & Q)) = (~P | ~Q)"; +prove "not_imp" "(~(P --> Q)) = (P & ~Q)"; prove "not_iff" "(P~=Q) = (P = (~Q))"; (*Avoids duplication of subgoals after expand_if, when the true and false @@ -301,13 +302,15 @@ setSolver unsafe_solver setmksimps (mksimps mksimps_pairs); -val HOL_ss = HOL_basic_ss addsimps ([triv_forall_equality, (* prunes params *) - if_True, if_False, if_cancel, - o_apply, imp_disjL, conj_assoc, disj_assoc, - de_Morgan_conj, de_Morgan_disj, - not_all, not_ex, cases_simp] - @ ex_simps @ all_simps @ simp_thms) - addcongs [imp_cong]; +val HOL_ss = + HOL_basic_ss addsimps + ([triv_forall_equality, (* prunes params *) + if_True, if_False, if_cancel, + o_apply, imp_disjL, conj_assoc, disj_assoc, + de_Morgan_conj, de_Morgan_disj, not_imp, + not_all, not_ex, cases_simp] + @ ex_simps @ all_simps @ simp_thms) + addcongs [imp_cong]; qed_goal "if_distrib" HOL.thy "f(if c then x else y) = (if c then f x else f y)"