equal
deleted
inserted
replaced
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)" |