src/HOL/simpdata.ML
changeset 4718 fc2ba9fb2135
parent 4681 a331c1f5a23e
child 4743 b3bfcbd9fb93
equal deleted inserted replaced
4717:1370ad043564 4718:fc2ba9fb2135
   206 
   206 
   207 prove "de_Morgan_disj" "(~(P | Q)) = (~P & ~Q)";
   207 prove "de_Morgan_disj" "(~(P | Q)) = (~P & ~Q)";
   208 prove "de_Morgan_conj" "(~(P & Q)) = (~P | ~Q)";
   208 prove "de_Morgan_conj" "(~(P & Q)) = (~P | ~Q)";
   209 prove "not_imp" "(~(P --> Q)) = (P & ~Q)";
   209 prove "not_imp" "(~(P --> Q)) = (P & ~Q)";
   210 prove "not_iff" "(P~=Q) = (P = (~Q))";
   210 prove "not_iff" "(P~=Q) = (P = (~Q))";
       
   211 prove "not1_or" "(~P | Q) = (P --> Q)";
       
   212 prove "not2_or" "(P | ~Q) = (Q --> P)"; (* changes orientation :-( *)
   211 
   213 
   212 (*Avoids duplication of subgoals after expand_if, when the true and false 
   214 (*Avoids duplication of subgoals after expand_if, when the true and false 
   213   cases boil down to the same thing.*) 
   215   cases boil down to the same thing.*) 
   214 prove "cases_simp" "((P --> Q) & (~P --> Q)) = Q";
   216 prove "cases_simp" "((P --> Q) & (~P --> Q)) = Q";
   215 
   217 
   352 fun Delsplits splits = (simpset_ref() := simpset() delsplits splits);
   354 fun Delsplits splits = (simpset_ref() := simpset() delsplits splits);
   353 
   355 
   354 qed_goal "if_cancel" HOL.thy "(if c then x else x) = x"
   356 qed_goal "if_cancel" HOL.thy "(if c then x else x) = x"
   355   (K [split_tac [expand_if] 1, blast_tac HOL_cs 1]);
   357   (K [split_tac [expand_if] 1, blast_tac HOL_cs 1]);
   356 
   358 
       
   359 qed_goal "if_eq_cancel" HOL.thy "(if x = y then y else x) = x"
       
   360   (K [split_tac [expand_if] 1, blast_tac HOL_cs 1]);
       
   361 
   357 (** 'if' congruence rules: neither included by default! *)
   362 (** 'if' congruence rules: neither included by default! *)
   358 
   363 
   359 (*Simplifies x assuming c and y assuming ~c*)
   364 (*Simplifies x assuming c and y assuming ~c*)
   360 qed_goal "if_cong" HOL.thy
   365 qed_goal "if_cong" HOL.thy
   361   "[| b=c; c ==> x=u; ~c ==> y=v |] ==>\
   366   "[| b=c; c ==> x=u; ~c ==> y=v |] ==>\
   400 
   405 
   401 val HOL_ss = 
   406 val HOL_ss = 
   402     HOL_basic_ss addsimps 
   407     HOL_basic_ss addsimps 
   403      ([triv_forall_equality, (* prunes params *)
   408      ([triv_forall_equality, (* prunes params *)
   404        True_implies_equals, (* prune asms `True' *)
   409        True_implies_equals, (* prune asms `True' *)
   405        if_True, if_False, if_cancel,
   410        if_True, if_False, if_cancel, if_eq_cancel,
   406        o_apply, imp_disjL, conj_assoc, disj_assoc,
   411        o_apply, imp_disjL, conj_assoc, disj_assoc,
   407        de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2, not_imp,
   412        de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2, not_imp,
   408        not_all, not_ex, cases_simp]
   413        not1_or, not_all, not_ex, cases_simp]
   409      @ ex_simps @ all_simps @ simp_thms)
   414      @ ex_simps @ all_simps @ simp_thms)
   410      addsimprocs [defALL_regroup,defEX_regroup]
   415      addsimprocs [defALL_regroup,defEX_regroup]
   411      addcongs [imp_cong];
   416      addcongs [imp_cong];
   412 
   417 
   413 qed_goal "if_distrib" HOL.thy
   418 qed_goal "if_distrib" HOL.thy