src/HOL/simpdata.ML
changeset 1758 60613b065e9b
parent 1722 bb326972ede6
child 1821 bc506bcb9fe4
equal deleted 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)"