src/HOL/simpdata.ML
 changeset 1758 60613b065e9b parent 1722 bb326972ede6 child 1821 bc506bcb9fe4
equal inserted replaced
1757:f7a573c46611 1758:60613b065e9b
`   190 prove "not_ex"  "(~ (? x.P(x))) = (! x.~P(x))";`
`   190 prove "not_ex"  "(~ (? x.P(x))) = (! x.~P(x))";`
`   191 `
`   191 `
`   192 prove "ex_disj_distrib" "(? x. P(x) | Q(x)) = ((? x. P(x)) | (? x. Q(x)))";`
`   192 prove "ex_disj_distrib" "(? x. P(x) | Q(x)) = ((? x. P(x)) | (? x. Q(x)))";`
`   193 prove "all_conj_distrib" "(!x. P(x) & Q(x)) = ((! x. P(x)) & (! x. Q(x)))";`
`   193 prove "all_conj_distrib" "(!x. P(x) & Q(x)) = ((! x. P(x)) & (! x. Q(x)))";`
`   194 `
`   194 `
`       `
`   195 prove "ex_imp" "((? x. P x) --> Q) = (!x. P x --> Q)";`
`       `
`   196 `
`   195 qed_goal "if_cancel" HOL.thy "(if c then x else x) = x"`
`   197 qed_goal "if_cancel" HOL.thy "(if c then x else x) = x"`
`   196   (fn _ => [simp_tac (HOL_ss setloop (split_tac [expand_if])) 1]);`
`   198   (fn _ => [simp_tac (HOL_ss setloop (split_tac [expand_if])) 1]);`
`   197 `
`   199 `
`   198 qed_goal "if_distrib" HOL.thy`
`   200 qed_goal "if_distrib" HOL.thy`
`   199   "f(if c then x else y) = (if c then f x else f y)" `
`   201   "f(if c then x else y) = (if c then f x else f y)" `