13 (*** Big Union -- least upper bound of a set ***) |
13 (*** Big Union -- least upper bound of a set ***) |
14 |
14 |
15 val prems = goal Set.thy |
15 val prems = goal Set.thy |
16 "B:A ==> B <= Union(A)"; |
16 "B:A ==> B <= Union(A)"; |
17 by (REPEAT (ares_tac (prems@[subsetI,UnionI]) 1)); |
17 by (REPEAT (ares_tac (prems@[subsetI,UnionI]) 1)); |
18 val Union_upper = result(); |
18 qed "Union_upper"; |
19 |
19 |
20 val prems = goal Set.thy |
20 val prems = goal Set.thy |
21 "[| !!X. X:A ==> X<=C |] ==> Union(A) <= C"; |
21 "[| !!X. X:A ==> X<=C |] ==> Union(A) <= C"; |
22 by (REPEAT (ares_tac [subsetI] 1 |
22 by (REPEAT (ares_tac [subsetI] 1 |
23 ORELSE eresolve_tac ([UnionE] @ (prems RL [subsetD])) 1)); |
23 ORELSE eresolve_tac ([UnionE] @ (prems RL [subsetD])) 1)); |
24 val Union_least = result(); |
24 qed "Union_least"; |
25 |
25 |
26 |
26 |
27 (*** Big Intersection -- greatest lower bound of a set ***) |
27 (*** Big Intersection -- greatest lower bound of a set ***) |
28 |
28 |
29 val prems = goal Set.thy |
29 val prems = goal Set.thy |
30 "B:A ==> Inter(A) <= B"; |
30 "B:A ==> Inter(A) <= B"; |
31 by (REPEAT (resolve_tac (prems@[subsetI]) 1 |
31 by (REPEAT (resolve_tac (prems@[subsetI]) 1 |
32 ORELSE etac InterD 1)); |
32 ORELSE etac InterD 1)); |
33 val Inter_lower = result(); |
33 qed "Inter_lower"; |
34 |
34 |
35 val prems = goal Set.thy |
35 val prems = goal Set.thy |
36 "[| !!X. X:A ==> C<=X |] ==> C <= Inter(A)"; |
36 "[| !!X. X:A ==> C<=X |] ==> C <= Inter(A)"; |
37 by (REPEAT (ares_tac [subsetI,InterI] 1 |
37 by (REPEAT (ares_tac [subsetI,InterI] 1 |
38 ORELSE eresolve_tac (prems RL [subsetD]) 1)); |
38 ORELSE eresolve_tac (prems RL [subsetD]) 1)); |
39 val Inter_greatest = result(); |
39 qed "Inter_greatest"; |
40 |
40 |
41 (*** Finite Union -- the least upper bound of 2 sets ***) |
41 (*** Finite Union -- the least upper bound of 2 sets ***) |
42 |
42 |
43 goal Set.thy "A <= A Un B"; |
43 goal Set.thy "A <= A Un B"; |
44 by (REPEAT (ares_tac [subsetI,UnI1] 1)); |
44 by (REPEAT (ares_tac [subsetI,UnI1] 1)); |
45 val Un_upper1 = result(); |
45 qed "Un_upper1"; |
46 |
46 |
47 goal Set.thy "B <= A Un B"; |
47 goal Set.thy "B <= A Un B"; |
48 by (REPEAT (ares_tac [subsetI,UnI2] 1)); |
48 by (REPEAT (ares_tac [subsetI,UnI2] 1)); |
49 val Un_upper2 = result(); |
49 qed "Un_upper2"; |
50 |
50 |
51 val prems = goal Set.thy "[| A<=C; B<=C |] ==> A Un B <= C"; |
51 val prems = goal Set.thy "[| A<=C; B<=C |] ==> A Un B <= C"; |
52 by (cut_facts_tac prems 1); |
52 by (cut_facts_tac prems 1); |
53 by (DEPTH_SOLVE (ares_tac [subsetI] 1 |
53 by (DEPTH_SOLVE (ares_tac [subsetI] 1 |
54 ORELSE eresolve_tac [UnE,subsetD] 1)); |
54 ORELSE eresolve_tac [UnE,subsetD] 1)); |
55 val Un_least = result(); |
55 qed "Un_least"; |
56 |
56 |
57 (*** Finite Intersection -- the greatest lower bound of 2 sets *) |
57 (*** Finite Intersection -- the greatest lower bound of 2 sets *) |
58 |
58 |
59 goal Set.thy "A Int B <= A"; |
59 goal Set.thy "A Int B <= A"; |
60 by (REPEAT (ares_tac [subsetI] 1 ORELSE etac IntE 1)); |
60 by (REPEAT (ares_tac [subsetI] 1 ORELSE etac IntE 1)); |
61 val Int_lower1 = result(); |
61 qed "Int_lower1"; |
62 |
62 |
63 goal Set.thy "A Int B <= B"; |
63 goal Set.thy "A Int B <= B"; |
64 by (REPEAT (ares_tac [subsetI] 1 ORELSE etac IntE 1)); |
64 by (REPEAT (ares_tac [subsetI] 1 ORELSE etac IntE 1)); |
65 val Int_lower2 = result(); |
65 qed "Int_lower2"; |
66 |
66 |
67 val prems = goal Set.thy "[| C<=A; C<=B |] ==> C <= A Int B"; |
67 val prems = goal Set.thy "[| C<=A; C<=B |] ==> C <= A Int B"; |
68 by (cut_facts_tac prems 1); |
68 by (cut_facts_tac prems 1); |
69 by (REPEAT (ares_tac [subsetI,IntI] 1 |
69 by (REPEAT (ares_tac [subsetI,IntI] 1 |
70 ORELSE etac subsetD 1)); |
70 ORELSE etac subsetD 1)); |
71 val Int_greatest = result(); |
71 qed "Int_greatest"; |
72 |
72 |
73 (*** Monotonicity ***) |
73 (*** Monotonicity ***) |
74 |
74 |
75 val [prem] = goalw Set.thy [mono_def] |
75 val [prem] = goalw Set.thy [mono_def] |
76 "[| !!A B. A <= B ==> f(A) <= f(B) |] ==> mono(f)"; |
76 "[| !!A B. A <= B ==> f(A) <= f(B) |] ==> mono(f)"; |
77 by (REPEAT (ares_tac [allI, impI, prem] 1)); |
77 by (REPEAT (ares_tac [allI, impI, prem] 1)); |
78 val monoI = result(); |
78 qed "monoI"; |
79 |
79 |
80 val [major,minor] = goalw Set.thy [mono_def] |
80 val [major,minor] = goalw Set.thy [mono_def] |
81 "[| mono(f); A <= B |] ==> f(A) <= f(B)"; |
81 "[| mono(f); A <= B |] ==> f(A) <= f(B)"; |
82 by (rtac (major RS spec RS spec RS mp) 1); |
82 by (rtac (major RS spec RS spec RS mp) 1); |
83 by (rtac minor 1); |
83 by (rtac minor 1); |
84 val monoD = result(); |
84 qed "monoD"; |
85 |
85 |
86 val [prem] = goal Set.thy "mono(f) ==> f(A) Un f(B) <= f(A Un B)"; |
86 val [prem] = goal Set.thy "mono(f) ==> f(A) Un f(B) <= f(A Un B)"; |
87 by (rtac Un_least 1); |
87 by (rtac Un_least 1); |
88 by (rtac (Un_upper1 RS (prem RS monoD)) 1); |
88 by (rtac (Un_upper1 RS (prem RS monoD)) 1); |
89 by (rtac (Un_upper2 RS (prem RS monoD)) 1); |
89 by (rtac (Un_upper2 RS (prem RS monoD)) 1); |
90 val mono_Un = result(); |
90 qed "mono_Un"; |
91 |
91 |
92 val [prem] = goal Set.thy "mono(f) ==> f(A Int B) <= f(A) Int f(B)"; |
92 val [prem] = goal Set.thy "mono(f) ==> f(A Int B) <= f(A) Int f(B)"; |
93 by (rtac Int_greatest 1); |
93 by (rtac Int_greatest 1); |
94 by (rtac (Int_lower1 RS (prem RS monoD)) 1); |
94 by (rtac (Int_lower1 RS (prem RS monoD)) 1); |
95 by (rtac (Int_lower2 RS (prem RS monoD)) 1); |
95 by (rtac (Int_lower2 RS (prem RS monoD)) 1); |
96 val mono_Int = result(); |
96 qed "mono_Int"; |
97 |
97 |
98 (****) |
98 (****) |
99 |
99 |
100 val set_cs = FOL_cs |
100 val set_cs = FOL_cs |
101 addSIs [ballI, subsetI, InterI, INT_I, CollectI, |
101 addSIs [ballI, subsetI, InterI, INT_I, CollectI, |