3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory
4 Copyright 1991 University of Cambridge
6 Set theory for higher-order logic. A set is simply a predicate.
9 section "Relating predicates and sets";
11 Addsimps [Collect_mem_eq];
12 AddIffs [mem_Collect_eq];
14 Goal "P(a) ==> a : {x. P(x)}";
18 Goal "a : {x. P(x)} ==> P(a)";
19 by (Asm_full_simp_tac 1);
22 bind_thm ("CollectE", make_elim CollectD);
24 val [prem] = Goal "[| !!x. (x:A) = (x:B) |] ==> A = B";
25 by (rtac (prem RS ext RS arg_cong RS box_equals) 1);
26 by (rtac Collect_mem_eq 1);
27 by (rtac Collect_mem_eq 1);
30 val [prem] = Goal "[| !!x. P(x)=Q(x) |] ==> {x. P(x)} = {x. Q(x)}";
31 by (rtac (prem RS ext RS arg_cong) 1);
34 val CollectE = make_elim CollectD;
40 section "Bounded quantifiers";
42 val prems = Goalw [Ball_def]
43 "[| !!x. x:A ==> P(x) |] ==> ! x:A. P(x)";
44 by (REPEAT (ares_tac (prems @ [allI,impI]) 1));
47 Goalw [Ball_def] "[| ! x:A. P(x); x:A |] ==> P(x)";
51 val major::prems = Goalw [Ball_def]
52 "[| ! x:A. P(x); P(x) ==> Q; x~:A ==> Q |] ==> Q";
53 by (rtac (major RS spec RS impCE) 1);
54 by (REPEAT (eresolve_tac prems 1));
57 (*Takes assumptions ! x:A.P(x) and a:A; creates assumption P(a)*)
58 fun ball_tac i = etac ballE i THEN contr_tac (i+1);
63 (* gives better instantiation for bound: *)
64 claset_ref() := claset() addWrapper ("bspec", fn tac2 =>
65 (dtac bspec THEN' atac) APPEND' tac2);
67 (*Normally the best argument order: P(x) constrains the choice of x:A*)
68 Goalw [Bex_def] "[| P(x); x:A |] ==> ? x:A. P(x)";
72 (*The best argument order when there is only one x:A*)
73 Goalw [Bex_def] "[| x:A; P(x) |] ==> ? x:A. P(x)";
78 "[| ! x:A. ~P(x) ==> P(a); a:A |] ==> ? x:A. P(x)";
79 by (rtac classical 1);
80 by (REPEAT (ares_tac (prems@[bexI,ballI,notI,notE]) 1)) ;
83 val major::prems = Goalw [Bex_def]
84 "[| ? x:A. P(x); !!x. [| x:A; P(x) |] ==> Q |] ==> Q";
85 by (rtac (major RS exE) 1);
86 by (REPEAT (eresolve_tac (prems @ [asm_rl,conjE]) 1));
92 (*Trival rewrite rule*)
93 Goal "(! x:A. P) = ((? x. x:A) --> P)";
94 by (simp_tac (simpset() addsimps [Ball_def]) 1);
97 (*Dual form for existentials*)
98 Goal "(? x:A. P) = ((? x. x:A) & P)";
99 by (simp_tac (simpset() addsimps [Bex_def]) 1);
102 Addsimps [ball_triv, bex_triv];
104 (** Congruence rules **)
106 val prems = Goalw [Ball_def]
107 "[| A=B; !!x. x:B ==> P(x) = Q(x) |] ==> \
108 \ (! x:A. P(x)) = (! x:B. Q(x))";
109 by (asm_simp_tac (simpset() addsimps prems) 1);
112 val prems = Goalw [Bex_def]
113 "[| A=B; !!x. x:B ==> P(x) = Q(x) |] ==> \
114 \ (? x:A. P(x)) = (? x:B. Q(x))";
115 by (asm_simp_tac (simpset() addcongs [conj_cong] addsimps prems) 1);
118 Addcongs [ball_cong,bex_cong];
122 val prems = Goalw [subset_def] "(!!x. x:A ==> x:B) ==> A <= B";
123 by (REPEAT (ares_tac (prems @ [ballI]) 1));
126 (*Map the type ('a set => anything) to just 'a.
127 For overloading constants whose first argument has type "'a set" *)
128 fun overload_1st_set s = Blast.overloaded (s, HOLogic.dest_setT o domain_type);
130 (*While (:) is not, its type must be kept
131 for overloading of = to work.*)
132 Blast.overloaded ("op :", domain_type);
134 overload_1st_set "Ball"; (*need UNION, INTER also?*)
135 overload_1st_set "Bex";
137 (*Image: retain the type of the set being expressed*)
138 Blast.overloaded ("image", domain_type);
140 (*Rule in Modus Ponens style*)
141 Goalw [subset_def] "[| A <= B; c:A |] ==> c:B";
146 (*The same, with reversed premises for use with etac -- cf rev_mp*)
147 Goal "[| c:A; A <= B |] ==> c:B";
148 by (REPEAT (ares_tac [subsetD] 1)) ;
150 AddXIs [rev_subsetD];
152 (*Converts A<=B to x:A ==> x:B*)
153 fun impOfSubs th = th RSN (2, rev_subsetD);
155 Goal "[| A <= B; c ~: B |] ==> c ~: A";
156 by (REPEAT (eresolve_tac [asm_rl, contrapos, subsetD] 1)) ;
157 qed "contra_subsetD";
159 Goal "[| c ~: B; A <= B |] ==> c ~: A";
160 by (REPEAT (eresolve_tac [asm_rl, contrapos, subsetD] 1)) ;
161 qed "rev_contra_subsetD";
163 (*Classical elimination rule*)
164 val major::prems = Goalw [subset_def]
165 "[| A <= B; c~:A ==> P; c:B ==> P |] ==> P";
166 by (rtac (major RS ballE) 1);
167 by (REPEAT (eresolve_tac prems 1));
170 (*Takes assumptions A<=B; c:A and creates the assumption c:B *)
171 fun set_mp_tac i = etac subsetCE i THEN mp_tac i;
174 AddEs [subsetD, subsetCE];
176 Goal "A <= (A::'a set)";
178 qed "subset_refl"; (*Blast_tac would try order_refl and fail*)
180 Goal "[| A<=B; B<=C |] ==> A<=(C::'a set)";
187 (*Anti-symmetry of the subset relation*)
188 Goal "[| A <= B; B <= A |] ==> A = (B::'a set)";
190 by (blast_tac (claset() addIs [subsetD]) 1);
191 qed "subset_antisym";
192 val equalityI = subset_antisym;
196 (* Equality rules from ZF set theory -- are they appropriate here? *)
197 Goal "A = B ==> A<=(B::'a set)";
199 by (rtac subset_refl 1);
202 Goal "A = B ==> B<=(A::'a set)";
204 by (rtac subset_refl 1);
208 "[| A = B; [| A<=B; B<=(A::'a set) |] ==> P |] ==> P";
209 by (resolve_tac prems 1);
210 by (REPEAT (resolve_tac (prems RL [equalityD1,equalityD2]) 1));
213 val major::prems = Goal
214 "[| A = B; [| c:A; c:B |] ==> P; [| c~:A; c~:B |] ==> P |] ==> P";
215 by (rtac (major RS equalityE) 1);
216 by (REPEAT (contr_tac 1 ORELSE eresolve_tac ([asm_rl,subsetCE]@prems) 1));
219 (*Lemma for creating induction formulae -- for "pattern matching" on p
220 To make the induction hypotheses usable, apply "spec" or "bspec" to
221 put universal quantifiers over the free variables in p. *)
223 "[| p:A; !!z. z:A ==> p=z --> R |] ==> R";
225 by (REPEAT (resolve_tac (refl::prems) 1));
226 qed "setup_induction";
229 section "The universal set -- UNIV";
231 Goalw [UNIV_def] "x : UNIV";
232 by (rtac CollectI 1);
237 AddIs [UNIV_I]; (*unsafe makes it less likely to cause problems*)
244 (** Eta-contracting these two rules (to remove P) causes them to be ignored
245 because of their interaction with congruence rules. **)
247 Goalw [Ball_def] "Ball UNIV P = All P";
251 Goalw [Bex_def] "Bex UNIV P = Ex P";
254 Addsimps [ball_UNIV, bex_UNIV];
257 section "The empty set -- {}";
259 Goalw [empty_def] "(c : {}) = False";
263 Addsimps [empty_iff];
266 by (Full_simp_tac 1);
275 (*One effect is to delete the ASSUMPTION {} <= A*)
276 AddIffs [empty_subsetI];
278 val [prem]= Goal "[| !!y. y:A ==> False |] ==> A={}";
279 by (blast_tac (claset() addIs [prem RS FalseE]) 1) ;
282 (*Use for reasoning about disjointness: A Int B = {} *)
283 Goal "A={} ==> a ~: A";
287 AddDs [equals0D, sym RS equals0D];
289 Goalw [Ball_def] "Ball {} P = True";
293 Goalw [Bex_def] "Bex {} P = False";
296 Addsimps [ball_empty, bex_empty];
299 by (blast_tac (claset() addEs [equalityE]) 1);
300 qed "UNIV_not_empty";
301 AddIffs [UNIV_not_empty];
305 section "The Powerset operator -- Pow";
307 Goalw [Pow_def] "(A : Pow(B)) = (A <= B)";
313 Goalw [Pow_def] "A <= B ==> A : Pow(B)";
314 by (etac CollectI 1);
317 Goalw [Pow_def] "A : Pow(B) ==> A<=B";
318 by (etac CollectD 1);
322 val Pow_bottom = empty_subsetI RS PowI; (* {}: Pow(B) *)
323 val Pow_top = subset_refl RS PowI; (* A : Pow(A) *)
326 section "Set complement";
328 Goalw [Compl_def] "(c : -A) = (c~:A)";
332 Addsimps [Compl_iff];
334 val prems = Goalw [Compl_def] "[| c:A ==> False |] ==> c : -A";
335 by (REPEAT (ares_tac (prems @ [CollectI,notI]) 1));
338 (*This form, with negated conclusion, works well with the Classical prover.
339 Negated assumptions behave like formulae on the right side of the notional
341 Goalw [Compl_def] "c : -A ==> c~:A";
342 by (etac CollectD 1);
345 val ComplE = make_elim ComplD;
351 section "Binary union -- Un";
353 Goalw [Un_def] "(c : A Un B) = (c:A | c:B)";
358 Goal "c:A ==> c : A Un B";
362 Goal "c:B ==> c : A Un B";
366 (*Classical introduction rule: no commitment to A vs B*)
368 val prems = Goal "(c~:B ==> c:A) ==> c : A Un B";
370 by (REPEAT (ares_tac (prems@[disjCI]) 1)) ;
373 val major::prems = Goalw [Un_def]
374 "[| c : A Un B; c:A ==> P; c:B ==> P |] ==> P";
375 by (rtac (major RS CollectD RS disjE) 1);
376 by (REPEAT (eresolve_tac prems 1));
383 section "Binary intersection -- Int";
385 Goalw [Int_def] "(c : A Int B) = (c:A & c:B)";
390 Goal "[| c:A; c:B |] ==> c : A Int B";
394 Goal "c : A Int B ==> c:A";
395 by (Asm_full_simp_tac 1);
398 Goal "c : A Int B ==> c:B";
399 by (Asm_full_simp_tac 1);
402 val [major,minor] = Goal
403 "[| c : A Int B; [| c:A; c:B |] ==> P |] ==> P";
405 by (rtac (major RS IntD1) 1);
406 by (rtac (major RS IntD2) 1);
412 section "Set difference";
414 Goalw [set_diff_def] "(c : A-B) = (c:A & c~:B)";
419 Goal "[| c : A; c ~: B |] ==> c : A - B";
420 by (Asm_simp_tac 1) ;
423 Goal "c : A - B ==> c : A";
424 by (Asm_full_simp_tac 1) ;
427 Goal "[| c : A - B; c : B |] ==> P";
428 by (Asm_full_simp_tac 1) ;
431 val prems = Goal "[| c : A - B; [| c:A; c~:B |] ==> P |] ==> P";
432 by (resolve_tac prems 1);
433 by (REPEAT (ares_tac (prems RL [DiffD1, DiffD2 RS notI]) 1)) ;
440 section "Augmenting a set -- insert";
442 Goalw [insert_def] "a : insert b A = (a=b | a:A)";
445 Addsimps [insert_iff];
447 Goal "a : insert a B";
451 Goal "!!a. a : B ==> a : insert b B";
455 val major::prems = Goalw [insert_def]
456 "[| a : insert b A; a=b ==> P; a:A ==> P |] ==> P";
457 by (rtac (major RS UnE) 1);
458 by (REPEAT (eresolve_tac (prems @ [CollectE]) 1));
461 (*Classical introduction rule*)
462 val prems = Goal "(a~:B ==> a=b) ==> a: insert b B";
464 by (REPEAT (ares_tac (prems@[disjCI]) 1)) ;
470 Goal "A <= insert x B ==> A <= B & x ~: A | (? B'. A = insert x B' & B' <= B)";
471 by (case_tac "x:A" 1);
474 by (res_inst_tac [("x","A-{x}")] exI 1);
476 qed "subset_insertD";
478 section "Singletons, using insert";
481 by (rtac insertI1 1) ;
484 Goal "b : {a} ==> b=a";
488 bind_thm ("singletonE", make_elim singletonD);
490 Goal "(b : {a}) = (b=a)";
494 Goal "{a}={b} ==> a=b";
495 by (blast_tac (claset() addEs [equalityE]) 1);
496 qed "singleton_inject";
498 (*Redundant? But unlike insertCI, it proves the subgoal immediately!*)
500 AddSDs [singleton_inject];
503 Goal "{b} = insert a A = (a = b & A <= {b})";
504 by (safe_tac (claset() addSEs [equalityE]));
505 by (ALLGOALS Blast_tac);
506 qed "singleton_insert_inj_eq";
508 Goal "(insert a A = {b} ) = (a = b & A <= {b})";
509 by (rtac (singleton_insert_inj_eq RS (eq_sym_conv RS trans)) 1);
510 qed "singleton_insert_inj_eq'";
512 Goal "A <= {x} ==> A={} | A = {x}";
514 qed "subset_singletonD";
516 Goal "{x. x=a} = {a}";
518 qed "singleton_conv";
519 Addsimps [singleton_conv];
521 Goal "{x. a=x} = {a}";
523 qed "singleton_conv2";
524 Addsimps [singleton_conv2];
527 section "Unions of families -- UNION x:A. B(x) is Union(B``A)";
529 Goalw [UNION_def] "(b: (UN x:A. B(x))) = (EX x:A. b: B(x))";
535 (*The order of the premises presupposes that A is rigid; b may be flexible*)
536 Goal "[| a:A; b: B(a) |] ==> b: (UN x:A. B(x))";
540 val major::prems = Goalw [UNION_def]
541 "[| b : (UN x:A. B(x)); !!x.[| x:A; b: B(x) |] ==> R |] ==> R";
542 by (rtac (major RS CollectD RS bexE) 1);
543 by (REPEAT (ares_tac prems 1));
549 val prems = Goalw [UNION_def]
550 "[| A=B; !!x. x:B ==> C(x) = D(x) |] ==> \
551 \ (UN x:A. C(x)) = (UN x:B. D(x))";
552 by (asm_simp_tac (simpset() addsimps prems) 1);
556 section "Intersections of families -- INTER x:A. B(x) is Inter(B``A)";
558 Goalw [INTER_def] "(b: (INT x:A. B(x))) = (ALL x:A. b: B(x))";
564 val prems = Goalw [INTER_def]
565 "(!!x. x:A ==> b: B(x)) ==> b : (INT x:A. B(x))";
566 by (REPEAT (ares_tac ([CollectI,ballI] @ prems) 1));
569 Goal "[| b : (INT x:A. B(x)); a:A |] ==> b: B(a)";
573 (*"Classical" elimination -- by the Excluded Middle on a:A *)
574 val major::prems = Goalw [INTER_def]
575 "[| b : (INT x:A. B(x)); b: B(a) ==> R; a~:A ==> R |] ==> R";
576 by (rtac (major RS CollectD RS ballE) 1);
577 by (REPEAT (eresolve_tac prems 1));
581 AddEs [INT_D, INT_E];
583 val prems = Goalw [INTER_def]
584 "[| A=B; !!x. x:B ==> C(x) = D(x) |] ==> \
585 \ (INT x:A. C(x)) = (INT x:B. D(x))";
586 by (asm_simp_tac (simpset() addsimps prems) 1);
592 Goalw [Union_def] "(A : Union(C)) = (EX X:C. A:X)";
596 Addsimps [Union_iff];
598 (*The order of the premises presupposes that C is rigid; A may be flexible*)
599 Goal "[| X:C; A:X |] ==> A : Union(C)";
603 val major::prems = Goalw [Union_def]
604 "[| A : Union(C); !!X.[| A:X; X:C |] ==> R |] ==> R";
605 by (rtac (major RS UN_E) 1);
606 by (REPEAT (ares_tac prems 1));
615 Goalw [Inter_def] "(A : Inter(C)) = (ALL X:C. A:X)";
619 Addsimps [Inter_iff];
621 val prems = Goalw [Inter_def]
622 "[| !!X. X:C ==> A:X |] ==> A : Inter(C)";
623 by (REPEAT (ares_tac ([INT_I] @ prems) 1));
626 (*A "destruct" rule -- every X in C contains A as an element, but
627 A:X can hold when X:C does not! This rule is analogous to "spec". *)
628 Goal "[| A : Inter(C); X:C |] ==> A:X";
632 (*"Classical" elimination rule -- does not require proving X:C *)
633 val major::prems = Goalw [Inter_def]
634 "[| A : Inter(C); X~:C ==> R; A:X ==> R |] ==> R";
635 by (rtac (major RS INT_E) 1);
636 by (REPEAT (eresolve_tac prems 1));
640 AddEs [InterD, InterE];
643 (*** Image of a set under a function ***)
645 (*Frequently b does not have the syntactic form of f(x).*)
646 Goalw [image_def] "[| b=f(x); x:A |] ==> b : f``A";
649 Addsimps [image_eqI];
651 bind_thm ("imageI", refl RS image_eqI);
653 (*This version's more effective when we already have the required x*)
654 Goalw [image_def] "[| x:A; b=f(x) |] ==> b : f``A";
658 (*The eta-expansion gives variable-name preservation.*)
659 val major::prems = Goalw [image_def]
660 "[| b : (%x. f(x))``A; !!x.[| b=f(x); x:A |] ==> P |] ==> P";
661 by (rtac (major RS CollectD RS bexE) 1);
662 by (REPEAT (ares_tac prems 1));
668 Goal "f``(A Un B) = f``A Un f``B";
672 Goal "(z : f``A) = (EX x:A. z = f x)";
676 (*This rewrite rule would confuse users if made default.*)
677 Goal "(f``A <= B) = (ALL x:A. f(x): B)";
679 qed "image_subset_iff";
681 (*Replaces the three steps subsetI, imageE, hyp_subst_tac, but breaks too
682 many existing proofs.*)
683 val prems = Goal "(!!x. x:A ==> f(x) : B) ==> f``A <= B";
684 by (blast_tac (claset() addIs prems) 1);
688 (*** Range of a function -- just a translation for image! ***)
690 Goal "b=f(x) ==> b : range(f)";
691 by (EVERY1 [etac image_eqI, rtac UNIV_I]);
692 bind_thm ("range_eqI", UNIV_I RSN (2,image_eqI));
694 bind_thm ("rangeI", UNIV_I RS imageI);
696 val [major,minor] = Goal
697 "[| b : range(%x. f(x)); !!x. b=f(x) ==> P |] ==> P";
698 by (rtac (major RS imageE) 1);
703 (*** Set reasoning tools ***)
706 (** Rewrite rules for boolean case-splitting: faster than
710 bind_thm ("split_if_eq1", read_instantiate [("P", "%x. x = ?b")] split_if);
711 bind_thm ("split_if_eq2", read_instantiate [("P", "%x. ?a = x")] split_if);
713 (*Split ifs on either side of the membership relation.
714 Not for Addsimps -- can cause goals to blow up!*)
715 bind_thm ("split_if_mem1",
716 read_instantiate_sg (Theory.sign_of Set.thy) [("P", "%x. x : ?b")] split_if);
717 bind_thm ("split_if_mem2",
718 read_instantiate_sg (Theory.sign_of Set.thy) [("P", "%x. ?a : x")] split_if);
720 val split_ifs = [if_bool_eq_conj, split_if_eq1, split_if_eq2,
721 split_if_mem1, split_if_mem2];
724 (*Each of these has ALREADY been added to simpset() above.*)
725 val mem_simps = [insert_iff, empty_iff, Un_iff, Int_iff, Compl_iff, Diff_iff,
726 mem_Collect_eq, UN_iff, Union_iff, INT_iff, Inter_iff];
728 val mksimps_pairs = ("Ball",[bspec]) :: mksimps_pairs;
730 simpset_ref() := simpset() setmksimps (mksimps mksimps_pairs);
732 Addsimps[subset_UNIV, subset_refl];
735 (*** The 'proper subset' relation (<) ***)
737 Goalw [psubset_def] "!!A::'a set. [| A <= B; A ~= B |] ==> A<B";
742 Goalw [psubset_def] "A < insert x B ==> (x ~: A) & A<=B | x:A & A-{x}<B";
744 qed "psubset_insertD";
746 bind_thm ("psubset_eq", psubset_def RS meta_eq_to_obj_eq);
748 bind_thm ("psubset_imp_subset", psubset_eq RS iffD1 RS conjunct1);
750 Goal"[| (A::'a set) < B; B <= C |] ==> A < C";
751 by (auto_tac (claset(), simpset() addsimps [psubset_eq]));
752 qed "psubset_subset_trans";
754 Goal"[| (A::'a set) <= B; B < C|] ==> A < C";
755 by (auto_tac (claset(), simpset() addsimps [psubset_eq]));
756 qed "subset_psubset_trans";
758 Goalw [psubset_def] "A < B ==> EX b. b : (B - A)";
760 qed "psubset_imp_ex_mem";
767 fun gen_rulify_prems x =
768 Attrib.no_args (Drule.rule_attribute (fn _ => (standard o
769 rule_by_tactic (REPEAT (ALLGOALS (resolve_tac [allI, ballI, impI])))))) x;
773 val rulify_prems_attrib_setup =
774 [Attrib.add_attributes
775 [("rulify_prems", (gen_rulify_prems, gen_rulify_prems), "put theorem into standard rule form")]];