src/HOL/simpdata.ML
 changeset 4718 fc2ba9fb2135 parent 4681 a331c1f5a23e child 4743 b3bfcbd9fb93
equal inserted replaced
`   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`