1 |
|
2 (** basic properties of "Inf" and "Sup" **) |
|
3 |
|
4 (* unique existence *) |
|
5 |
|
6 Goalw [Inf_def] "is_Inf A (Inf A)"; |
|
7 by (rtac (ex_Inf RS spec RS selectI1) 1); |
|
8 qed "Inf_is_Inf"; |
|
9 |
|
10 Goal "is_Inf A inf --> Inf A = inf"; |
|
11 by (rtac impI 1); |
|
12 by (rtac (is_Inf_uniq RS mp) 1); |
|
13 by (rtac conjI 1); |
|
14 by (rtac Inf_is_Inf 1); |
|
15 by (assume_tac 1); |
|
16 qed "Inf_uniq"; |
|
17 |
|
18 Goalw [Ex1_def] "ALL A. EX! inf::'a::clattice. is_Inf A inf"; |
|
19 by Safe_tac; |
|
20 by (Step_tac 1); |
|
21 by (Step_tac 1); |
|
22 by (rtac Inf_is_Inf 1); |
|
23 by (rtac (Inf_uniq RS mp RS sym) 1); |
|
24 by (assume_tac 1); |
|
25 qed "ex1_Inf"; |
|
26 |
|
27 |
|
28 Goalw [Sup_def] "is_Sup A (Sup A)"; |
|
29 by (rtac (ex_Sup RS spec RS selectI1) 1); |
|
30 qed "Sup_is_Sup"; |
|
31 |
|
32 Goal "is_Sup A sup --> Sup A = sup"; |
|
33 by (rtac impI 1); |
|
34 by (rtac (is_Sup_uniq RS mp) 1); |
|
35 by (rtac conjI 1); |
|
36 by (rtac Sup_is_Sup 1); |
|
37 by (assume_tac 1); |
|
38 qed "Sup_uniq"; |
|
39 |
|
40 Goalw [Ex1_def] "ALL A. EX! sup::'a::clattice. is_Sup A sup"; |
|
41 by Safe_tac; |
|
42 by (Step_tac 1); |
|
43 by (Step_tac 1); |
|
44 by (rtac Sup_is_Sup 1); |
|
45 by (rtac (Sup_uniq RS mp RS sym) 1); |
|
46 by (assume_tac 1); |
|
47 qed "ex1_Sup"; |
|
48 |
|
49 |
|
50 (* "Inf" yields g.l.bs, "Sup" yields l.u.bs. --- in pieces *) |
|
51 |
|
52 val prems = goalw thy [Inf_def] "x:A ==> Inf A [= x"; |
|
53 by (cut_facts_tac prems 1); |
|
54 by (rtac someI2 1); |
|
55 by (rtac Inf_is_Inf 1); |
|
56 by (rewtac is_Inf_def); |
|
57 by (Fast_tac 1); |
|
58 qed "Inf_lb"; |
|
59 |
|
60 val [prem] = goalw thy [Inf_def] "(!!x. x:A ==> z [= x) ==> z [= Inf A"; |
|
61 by (rtac someI2 1); |
|
62 by (rtac Inf_is_Inf 1); |
|
63 by (rewtac is_Inf_def); |
|
64 by (Step_tac 1); |
|
65 by (Step_tac 1); |
|
66 by (etac mp 1); |
|
67 by (rtac ballI 1); |
|
68 by (etac prem 1); |
|
69 qed "Inf_ub_lbs"; |
|
70 |
|
71 |
|
72 val prems = goalw thy [Sup_def] "x:A ==> x [= Sup A"; |
|
73 by (cut_facts_tac prems 1); |
|
74 by (rtac someI2 1); |
|
75 by (rtac Sup_is_Sup 1); |
|
76 by (rewtac is_Sup_def); |
|
77 by (Fast_tac 1); |
|
78 qed "Sup_ub"; |
|
79 |
|
80 val [prem] = goalw thy [Sup_def] "(!!x. x:A ==> x [= z) ==> Sup A [= z"; |
|
81 by (rtac someI2 1); |
|
82 by (rtac Sup_is_Sup 1); |
|
83 by (rewtac is_Sup_def); |
|
84 by (Step_tac 1); |
|
85 by (Step_tac 1); |
|
86 by (etac mp 1); |
|
87 by (rtac ballI 1); |
|
88 by (etac prem 1); |
|
89 qed "Sup_lb_ubs"; |
|
90 |
|
91 |
|
92 (** minorized Infs / majorized Sups **) |
|
93 |
|
94 Goal "(x [= Inf A) = (ALL y:A. x [= y)"; |
|
95 by (rtac iffI 1); |
|
96 (*==>*) |
|
97 by (rtac ballI 1); |
|
98 by (rtac (le_trans RS mp) 1); |
|
99 by (etac conjI 1); |
|
100 by (etac Inf_lb 1); |
|
101 (*<==*) |
|
102 by (rtac Inf_ub_lbs 1); |
|
103 by (Fast_tac 1); |
|
104 qed "le_Inf_eq"; |
|
105 |
|
106 Goal "(Sup A [= x) = (ALL y:A. y [= x)"; |
|
107 by (rtac iffI 1); |
|
108 (*==>*) |
|
109 by (rtac ballI 1); |
|
110 by (rtac (le_trans RS mp) 1); |
|
111 by (rtac conjI 1); |
|
112 by (etac Sup_ub 1); |
|
113 by (assume_tac 1); |
|
114 (*<==*) |
|
115 by (rtac Sup_lb_ubs 1); |
|
116 by (Fast_tac 1); |
|
117 qed "ge_Sup_eq"; |
|
118 |
|
119 |
|
120 |
|
121 (** Subsets and limits **) |
|
122 |
|
123 Goal "A <= B --> Inf B [= Inf A"; |
|
124 by (rtac impI 1); |
|
125 by (stac le_Inf_eq 1); |
|
126 by (rewtac Ball_def); |
|
127 by Safe_tac; |
|
128 by (dtac subsetD 1); |
|
129 by (assume_tac 1); |
|
130 by (etac Inf_lb 1); |
|
131 qed "Inf_subset_antimon"; |
|
132 |
|
133 Goal "A <= B --> Sup A [= Sup B"; |
|
134 by (rtac impI 1); |
|
135 by (stac ge_Sup_eq 1); |
|
136 by (rewtac Ball_def); |
|
137 by Safe_tac; |
|
138 by (dtac subsetD 1); |
|
139 by (assume_tac 1); |
|
140 by (etac Sup_ub 1); |
|
141 qed "Sup_subset_mon"; |
|
142 |
|
143 |
|
144 (** singleton / empty limits **) |
|
145 |
|
146 Goal "Inf {x} = x"; |
|
147 by (rtac (Inf_uniq RS mp) 1); |
|
148 by (rewtac is_Inf_def); |
|
149 by Safe_tac; |
|
150 by (rtac le_refl 1); |
|
151 by (Fast_tac 1); |
|
152 qed "sing_Inf_eq"; |
|
153 |
|
154 Goal "Sup {x} = x"; |
|
155 by (rtac (Sup_uniq RS mp) 1); |
|
156 by (rewtac is_Sup_def); |
|
157 by Safe_tac; |
|
158 by (rtac le_refl 1); |
|
159 by (Fast_tac 1); |
|
160 qed "sing_Sup_eq"; |
|
161 |
|
162 |
|
163 Goal "Inf {} = Sup {x. True}"; |
|
164 by (rtac (Inf_uniq RS mp) 1); |
|
165 by (rewtac is_Inf_def); |
|
166 by Safe_tac; |
|
167 by (rtac (sing_Sup_eq RS subst) 1); |
|
168 back(); |
|
169 by (rtac (Sup_subset_mon RS mp) 1); |
|
170 by (Fast_tac 1); |
|
171 qed "empty_Inf_eq"; |
|
172 |
|
173 Goal "Sup {} = Inf {x. True}"; |
|
174 by (rtac (Sup_uniq RS mp) 1); |
|
175 by (rewtac is_Sup_def); |
|
176 by Safe_tac; |
|
177 by (rtac (sing_Inf_eq RS subst) 1); |
|
178 by (rtac (Inf_subset_antimon RS mp) 1); |
|
179 by (Fast_tac 1); |
|
180 qed "empty_Sup_eq"; |
|