equal
deleted
inserted
replaced
70 qed "bexE"; |
70 qed "bexE"; |
71 |
71 |
72 (*Trival rewrite rule; (! x:A.P)=P holds only if A is nonempty!*) |
72 (*Trival rewrite rule; (! x:A.P)=P holds only if A is nonempty!*) |
73 goal Set.thy "(! x:A. True) = True"; |
73 goal Set.thy "(! x:A. True) = True"; |
74 by (REPEAT (ares_tac [TrueI,ballI,iffI] 1)); |
74 by (REPEAT (ares_tac [TrueI,ballI,iffI] 1)); |
75 qed "ball_rew"; |
75 qed "ball_True"; |
76 Addsimps [ball_rew]; |
76 |
|
77 Addsimps [ball_True]; |
77 |
78 |
78 (** Congruence rules **) |
79 (** Congruence rules **) |
79 |
80 |
80 val prems = goal Set.thy |
81 val prems = goal Set.thy |
81 "[| A=B; !!x. x:B ==> P(x) = Q(x) |] ==> \ |
82 "[| A=B; !!x. x:B ==> P(x) = Q(x) |] ==> \ |
288 [ (rtac (minor RS (major RS equalityD1 RS subsetD RS emptyE)) 1) ]); |
289 [ (rtac (minor RS (major RS equalityD1 RS subsetD RS emptyE)) 1) ]); |
289 |
290 |
290 qed_goal "empty_iff" Set.thy "(c : {}) = False" |
291 qed_goal "empty_iff" Set.thy "(c : {}) = False" |
291 (fn _ => [ (fast_tac (!claset addSEs [emptyE]) 1) ]); |
292 (fn _ => [ (fast_tac (!claset addSEs [emptyE]) 1) ]); |
292 |
293 |
|
294 goal Set.thy "Ball {} P = True"; |
|
295 by (simp_tac (HOL_ss addsimps [mem_Collect_eq, Ball_def, empty_def]) 1); |
|
296 qed "ball_empty"; |
|
297 |
|
298 goal Set.thy "Bex {} P = False"; |
|
299 by (simp_tac (HOL_ss addsimps [mem_Collect_eq, Bex_def, empty_def]) 1); |
|
300 qed "bex_empty"; |
|
301 Addsimps [ball_empty, bex_empty]; |
|
302 |
293 |
303 |
294 section "Augmenting a set -- insert"; |
304 section "Augmenting a set -- insert"; |
295 |
305 |
296 qed_goalw "insertI1" Set.thy [insert_def] "a : insert a B" |
306 qed_goalw "insertI1" Set.thy [insert_def] "a : insert a B" |
297 (fn _ => [rtac (CollectI RS UnI1) 1, rtac refl 1]); |
307 (fn _ => [rtac (CollectI RS UnI1) 1, rtac refl 1]); |