21 |
22 |
22 arities |
23 arities |
23 bool :: "term" |
24 bool :: "term" |
24 fun :: ("term", "term") "term" |
25 fun :: ("term", "term") "term" |
25 |
26 |
|
27 judgment |
|
28 Trueprop :: "bool => prop" ("(_)" 5) |
|
29 |
26 consts |
30 consts |
27 |
|
28 (* Constants *) |
|
29 |
|
30 Trueprop :: "bool => prop" ("(_)" 5) |
|
31 Not :: "bool => bool" ("~ _" [40] 40) |
31 Not :: "bool => bool" ("~ _" [40] 40) |
32 True :: bool |
32 True :: bool |
33 False :: bool |
33 False :: bool |
34 If :: "[bool, 'a, 'a] => 'a" ("(if (_)/ then (_)/ else (_))" 10) |
34 If :: "[bool, 'a, 'a] => 'a" ("(if (_)/ then (_)/ else (_))" 10) |
35 arbitrary :: 'a |
35 arbitrary :: 'a |
36 |
36 |
37 (* Binders *) |
|
38 |
|
39 The :: "('a => bool) => 'a" |
37 The :: "('a => bool) => 'a" |
40 All :: "('a => bool) => bool" (binder "ALL " 10) |
38 All :: "('a => bool) => bool" (binder "ALL " 10) |
41 Ex :: "('a => bool) => bool" (binder "EX " 10) |
39 Ex :: "('a => bool) => bool" (binder "EX " 10) |
42 Ex1 :: "('a => bool) => bool" (binder "EX! " 10) |
40 Ex1 :: "('a => bool) => bool" (binder "EX! " 10) |
43 Let :: "['a, 'a => 'b] => 'b" |
41 Let :: "['a, 'a => 'b] => 'b" |
44 |
42 |
45 (* Infixes *) |
|
46 |
|
47 "=" :: "['a, 'a] => bool" (infixl 50) |
43 "=" :: "['a, 'a] => bool" (infixl 50) |
48 & :: "[bool, bool] => bool" (infixr 35) |
44 & :: "[bool, bool] => bool" (infixr 35) |
49 "|" :: "[bool, bool] => bool" (infixr 30) |
45 "|" :: "[bool, bool] => bool" (infixr 30) |
50 --> :: "[bool, bool] => bool" (infixr 25) |
46 --> :: "[bool, bool] => bool" (infixr 25) |
51 |
47 |
52 local |
48 local |
53 |
49 |
54 |
50 |
55 (* Overloaded Constants *) |
51 subsubsection {* Additional concrete syntax *} |
56 |
|
57 axclass zero < "term" |
|
58 axclass one < "term" |
|
59 axclass plus < "term" |
|
60 axclass minus < "term" |
|
61 axclass times < "term" |
|
62 axclass inverse < "term" |
|
63 |
|
64 global |
|
65 |
|
66 consts |
|
67 "0" :: "'a::zero" ("0") |
|
68 "1" :: "'a::one" ("1") |
|
69 "+" :: "['a::plus, 'a] => 'a" (infixl 65) |
|
70 - :: "['a::minus, 'a] => 'a" (infixl 65) |
|
71 uminus :: "['a::minus] => 'a" ("- _" [81] 80) |
|
72 * :: "['a::times, 'a] => 'a" (infixl 70) |
|
73 |
|
74 typed_print_translation {* |
|
75 let |
|
76 fun tr' c = (c, fn show_sorts => fn T => fn ts => |
|
77 if T = dummyT orelse not (! show_types) andalso can Term.dest_Type T then raise Match |
|
78 else Syntax.const Syntax.constrainC $ Syntax.const c $ Syntax.term_of_typ show_sorts T); |
|
79 in [tr' "0", tr' "1"] end; |
|
80 *} |
|
81 |
|
82 local |
|
83 |
|
84 consts |
|
85 abs :: "'a::minus => 'a" |
|
86 inverse :: "'a::inverse => 'a" |
|
87 divide :: "['a::inverse, 'a] => 'a" (infixl "'/" 70) |
|
88 |
|
89 syntax (xsymbols) |
|
90 abs :: "'a::minus => 'a" ("\<bar>_\<bar>") |
|
91 syntax (HTML output) |
|
92 abs :: "'a::minus => 'a" ("\<bar>_\<bar>") |
|
93 |
|
94 axclass plus_ac0 < plus, zero |
|
95 commute: "x + y = y + x" |
|
96 assoc: "(x + y) + z = x + (y + z)" |
|
97 zero: "0 + x = x" |
|
98 |
|
99 |
|
100 (** Additional concrete syntax **) |
|
101 |
52 |
102 nonterminals |
53 nonterminals |
103 letbinds letbind |
54 letbinds letbind |
104 case_syn cases_syn |
55 case_syn cases_syn |
105 |
56 |
106 syntax |
57 syntax |
107 ~= :: "['a, 'a] => bool" (infixl 50) |
58 ~= :: "['a, 'a] => bool" (infixl 50) |
108 "_The" :: "[pttrn, bool] => 'a" ("(3THE _./ _)" [0, 10] 10) |
59 "_The" :: "[pttrn, bool] => 'a" ("(3THE _./ _)" [0, 10] 10) |
109 |
|
110 (* Let expressions *) |
|
111 |
60 |
112 "_bind" :: "[pttrn, 'a] => letbind" ("(2_ =/ _)" 10) |
61 "_bind" :: "[pttrn, 'a] => letbind" ("(2_ =/ _)" 10) |
113 "" :: "letbind => letbinds" ("_") |
62 "" :: "letbind => letbinds" ("_") |
114 "_binds" :: "[letbind, letbinds] => letbinds" ("_;/ _") |
63 "_binds" :: "[letbind, letbinds] => letbinds" ("_;/ _") |
115 "_Let" :: "[letbinds, 'a] => 'a" ("(let (_)/ in (_))" 10) |
64 "_Let" :: "[letbinds, 'a] => 'a" ("(let (_)/ in (_))" 10) |
116 |
|
117 (* Case expressions *) |
|
118 |
65 |
119 "_case_syntax":: "['a, cases_syn] => 'b" ("(case _ of/ _)" 10) |
66 "_case_syntax":: "['a, cases_syn] => 'b" ("(case _ of/ _)" 10) |
120 "_case1" :: "['a, 'b] => case_syn" ("(2_ =>/ _)" 10) |
67 "_case1" :: "['a, 'b] => case_syn" ("(2_ =>/ _)" 10) |
121 "" :: "case_syn => cases_syn" ("_") |
68 "" :: "case_syn => cases_syn" ("_") |
122 "_case2" :: "[case_syn, cases_syn] => cases_syn" ("_/ | _") |
69 "_case2" :: "[case_syn, cases_syn] => cases_syn" ("_/ | _") |
156 "ALL " :: "[idts, bool] => bool" ("(3! _./ _)" [0, 10] 10) |
103 "ALL " :: "[idts, bool] => bool" ("(3! _./ _)" [0, 10] 10) |
157 "EX " :: "[idts, bool] => bool" ("(3? _./ _)" [0, 10] 10) |
104 "EX " :: "[idts, bool] => bool" ("(3? _./ _)" [0, 10] 10) |
158 "EX! " :: "[idts, bool] => bool" ("(3?! _./ _)" [0, 10] 10) |
105 "EX! " :: "[idts, bool] => bool" ("(3?! _./ _)" [0, 10] 10) |
159 |
106 |
160 |
107 |
161 |
108 subsubsection {* Axioms and basic definitions *} |
162 (** Rules and definitions **) |
|
163 |
109 |
164 axioms |
110 axioms |
165 |
|
166 eq_reflection: "(x=y) ==> (x==y)" |
111 eq_reflection: "(x=y) ==> (x==y)" |
167 |
|
168 (* Basic Rules *) |
|
169 |
112 |
170 refl: "t = (t::'a)" |
113 refl: "t = (t::'a)" |
171 subst: "[| s = t; P(s) |] ==> P(t::'a)" |
114 subst: "[| s = t; P(s) |] ==> P(t::'a)" |
172 |
115 |
173 (*Extensionality is built into the meta-logic, and this rule expresses |
|
174 a related property. It is an eta-expanded version of the traditional |
|
175 rule, and similar to the ABS rule of HOL.*) |
|
176 ext: "(!!x::'a. (f x ::'b) = g x) ==> (%x. f x) = (%x. g x)" |
116 ext: "(!!x::'a. (f x ::'b) = g x) ==> (%x. f x) = (%x. g x)" |
|
117 -- {* Extensionality is built into the meta-logic, and this rule expresses *} |
|
118 -- {* a related property. It is an eta-expanded version of the traditional *} |
|
119 -- {* rule, and similar to the ABS rule of HOL *} |
177 |
120 |
178 the_eq_trivial: "(THE x. x = a) = (a::'a)" |
121 the_eq_trivial: "(THE x. x = a) = (a::'a)" |
179 |
122 |
180 impI: "(P ==> Q) ==> P-->Q" |
123 impI: "(P ==> Q) ==> P-->Q" |
181 mp: "[| P-->Q; P |] ==> Q" |
124 mp: "[| P-->Q; P |] ==> Q" |
182 |
125 |
183 defs |
126 defs |
184 |
|
185 True_def: "True == ((%x::bool. x) = (%x. x))" |
127 True_def: "True == ((%x::bool. x) = (%x. x))" |
186 All_def: "All(P) == (P = (%x. True))" |
128 All_def: "All(P) == (P = (%x. True))" |
187 Ex_def: "Ex(P) == !Q. (!x. P x --> Q) --> Q" |
129 Ex_def: "Ex(P) == !Q. (!x. P x --> Q) --> Q" |
188 False_def: "False == (!P. P)" |
130 False_def: "False == (!P. P)" |
189 not_def: "~ P == P-->False" |
131 not_def: "~ P == P-->False" |
190 and_def: "P & Q == !R. (P-->Q-->R) --> R" |
132 and_def: "P & Q == !R. (P-->Q-->R) --> R" |
191 or_def: "P | Q == !R. (P-->R) --> (Q-->R) --> R" |
133 or_def: "P | Q == !R. (P-->R) --> (Q-->R) --> R" |
192 Ex1_def: "Ex1(P) == ? x. P(x) & (! y. P(y) --> y=x)" |
134 Ex1_def: "Ex1(P) == ? x. P(x) & (! y. P(y) --> y=x)" |
193 |
135 |
194 axioms |
136 axioms |
195 (* Axioms *) |
|
196 |
|
197 iff: "(P-->Q) --> (Q-->P) --> (P=Q)" |
137 iff: "(P-->Q) --> (Q-->P) --> (P=Q)" |
198 True_or_False: "(P=True) | (P=False)" |
138 True_or_False: "(P=True) | (P=False)" |
199 |
139 |
200 defs |
140 defs |
201 (*misc definitions*) |
|
202 Let_def: "Let s f == f(s)" |
141 Let_def: "Let s f == f(s)" |
203 if_def: "If P x y == THE z::'a. (P=True --> z=x) & (P=False --> z=y)" |
142 if_def: "If P x y == THE z::'a. (P=True --> z=x) & (P=False --> z=y)" |
204 |
143 |
205 (*arbitrary is completely unspecified, but is made to appear as a |
|
206 definition syntactically*) |
|
207 arbitrary_def: "False ==> arbitrary == (THE x. False)" |
144 arbitrary_def: "False ==> arbitrary == (THE x. False)" |
208 |
145 -- {* @{term arbitrary} is completely unspecified, but is made to appear as a |
209 |
146 definition syntactically *} |
210 |
147 |
211 (* theory and package setup *) |
148 |
|
149 subsubsection {* Generic algebraic operations *} |
|
150 |
|
151 axclass zero < "term" |
|
152 axclass one < "term" |
|
153 axclass plus < "term" |
|
154 axclass minus < "term" |
|
155 axclass times < "term" |
|
156 axclass inverse < "term" |
|
157 |
|
158 global |
|
159 |
|
160 consts |
|
161 "0" :: "'a::zero" ("0") |
|
162 "1" :: "'a::one" ("1") |
|
163 "+" :: "['a::plus, 'a] => 'a" (infixl 65) |
|
164 - :: "['a::minus, 'a] => 'a" (infixl 65) |
|
165 uminus :: "['a::minus] => 'a" ("- _" [81] 80) |
|
166 * :: "['a::times, 'a] => 'a" (infixl 70) |
|
167 |
|
168 local |
|
169 |
|
170 typed_print_translation {* |
|
171 let |
|
172 fun tr' c = (c, fn show_sorts => fn T => fn ts => |
|
173 if T = dummyT orelse not (! show_types) andalso can Term.dest_Type T then raise Match |
|
174 else Syntax.const Syntax.constrainC $ Syntax.const c $ Syntax.term_of_typ show_sorts T); |
|
175 in [tr' "0", tr' "1"] end; |
|
176 *} -- {* show types that are presumably too general *} |
|
177 |
|
178 |
|
179 consts |
|
180 abs :: "'a::minus => 'a" |
|
181 inverse :: "'a::inverse => 'a" |
|
182 divide :: "['a::inverse, 'a] => 'a" (infixl "'/" 70) |
|
183 |
|
184 syntax (xsymbols) |
|
185 abs :: "'a::minus => 'a" ("\<bar>_\<bar>") |
|
186 syntax (HTML output) |
|
187 abs :: "'a::minus => 'a" ("\<bar>_\<bar>") |
|
188 |
|
189 axclass plus_ac0 < plus, zero |
|
190 commute: "x + y = y + x" |
|
191 assoc: "(x + y) + z = x + (y + z)" |
|
192 zero: "0 + x = x" |
|
193 |
|
194 |
|
195 subsection {* Theory and package setup *} |
|
196 |
|
197 subsubsection {* Basic lemmas *} |
212 |
198 |
213 use "HOL_lemmas.ML" |
199 use "HOL_lemmas.ML" |
214 theorems case_split = case_split_thm [case_names True False] |
200 theorems case_split = case_split_thm [case_names True False] |
215 |
201 |
216 declare trans [trans] (*overridden in theory Calculation*) |
202 declare trans [trans] |
217 |
203 declare impE [CPure.elim] iffD1 [CPure.elim] iffD2 [CPure.elim] |
218 lemma atomize_all: "(!!x. P x) == Trueprop (ALL x. P x)" |
204 |
|
205 |
|
206 subsubsection {* Atomizing meta-level connectives *} |
|
207 |
|
208 lemma atomize_all [atomize]: "(!!x. P x) == Trueprop (ALL x. P x)" |
219 proof (rule equal_intr_rule) |
209 proof (rule equal_intr_rule) |
220 assume "!!x. P x" |
210 assume "!!x. P x" |
221 show "ALL x. P x" by (rule allI) |
211 show "ALL x. P x" by (rule allI) |
222 next |
212 next |
223 assume "ALL x. P x" |
213 assume "ALL x. P x" |
224 thus "!!x. P x" by (rule allE) |
214 thus "!!x. P x" by (rule allE) |
225 qed |
215 qed |
226 |
216 |
227 lemma atomize_imp: "(A ==> B) == Trueprop (A --> B)" |
217 lemma atomize_imp [atomize]: "(A ==> B) == Trueprop (A --> B)" |
228 proof (rule equal_intr_rule) |
218 proof (rule equal_intr_rule) |
229 assume r: "A ==> B" |
219 assume r: "A ==> B" |
230 show "A --> B" by (rule impI) (rule r) |
220 show "A --> B" by (rule impI) (rule r) |
231 next |
221 next |
232 assume "A --> B" and A |
222 assume "A --> B" and A |
233 thus B by (rule mp) |
223 thus B by (rule mp) |
234 qed |
224 qed |
235 |
225 |
236 lemma atomize_eq: "(x == y) == Trueprop (x = y)" |
226 lemma atomize_eq [atomize]: "(x == y) == Trueprop (x = y)" |
237 proof (rule equal_intr_rule) |
227 proof (rule equal_intr_rule) |
238 assume "x == y" |
228 assume "x == y" |
239 show "x = y" by (unfold prems) (rule refl) |
229 show "x = y" by (unfold prems) (rule refl) |
240 next |
230 next |
241 assume "x = y" |
231 assume "x = y" |
242 thus "x == y" by (rule eq_reflection) |
232 thus "x == y" by (rule eq_reflection) |
243 qed |
233 qed |
244 |
234 |
245 lemmas atomize = atomize_all atomize_imp |
235 |
246 lemmas atomize' = atomize atomize_eq |
236 subsubsection {* Classical Reasoner setup *} |
247 |
237 |
248 use "cladata.ML" |
238 use "cladata.ML" |
249 setup hypsubst_setup |
239 setup hypsubst_setup |
250 setup Classical.setup |
240 setup Classical.setup |
251 setup clasetup |
241 setup clasetup |
252 |
242 |
253 declare impE [CPure.elim] iffD1 [CPure.elim] iffD2 [CPure.elim] |
|
254 |
|
255 use "blastdata.ML" |
243 use "blastdata.ML" |
256 setup Blast.setup |
244 setup Blast.setup |
|
245 |
|
246 |
|
247 subsubsection {* Simplifier setup *} |
257 |
248 |
258 use "simpdata.ML" |
249 use "simpdata.ML" |
259 setup Simplifier.setup |
250 setup Simplifier.setup |
260 setup "Simplifier.method_setup Splitter.split_modifiers" setup simpsetup |
251 setup "Simplifier.method_setup Splitter.split_modifiers" setup simpsetup |
261 setup Splitter.setup setup Clasimp.setup |
252 setup Splitter.setup setup Clasimp.setup |
262 |
253 |
|
254 |
|
255 subsection {* Order signatures and orders *} |
|
256 |
|
257 axclass |
|
258 ord < "term" |
|
259 |
|
260 syntax |
|
261 "op <" :: "['a::ord, 'a] => bool" ("op <") |
|
262 "op <=" :: "['a::ord, 'a] => bool" ("op <=") |
|
263 |
|
264 global |
|
265 |
|
266 consts |
|
267 "op <" :: "['a::ord, 'a] => bool" ("(_/ < _)" [50, 51] 50) |
|
268 "op <=" :: "['a::ord, 'a] => bool" ("(_/ <= _)" [50, 51] 50) |
|
269 |
|
270 local |
|
271 |
|
272 syntax (symbols) |
|
273 "op <=" :: "['a::ord, 'a] => bool" ("op \<le>") |
|
274 "op <=" :: "['a::ord, 'a] => bool" ("(_/ \<le> _)" [50, 51] 50) |
|
275 |
|
276 (*Tell blast about overloading of < and <= to reduce the risk of |
|
277 its applying a rule for the wrong type*) |
|
278 ML {* |
|
279 Blast.overloaded ("op <" , domain_type); |
|
280 Blast.overloaded ("op <=", domain_type); |
|
281 *} |
|
282 |
|
283 |
|
284 subsubsection {* Monotonicity *} |
|
285 |
|
286 constdefs |
|
287 mono :: "['a::ord => 'b::ord] => bool" |
|
288 "mono f == ALL A B. A <= B --> f A <= f B" |
|
289 |
|
290 lemma monoI [intro?]: "(!!A B. A <= B ==> f A <= f B) ==> mono f" |
|
291 by (unfold mono_def) blast |
|
292 |
|
293 lemma monoD [dest?]: "mono f ==> A <= B ==> f A <= f B" |
|
294 by (unfold mono_def) blast |
|
295 |
|
296 constdefs |
|
297 min :: "['a::ord, 'a] => 'a" |
|
298 "min a b == (if a <= b then a else b)" |
|
299 max :: "['a::ord, 'a] => 'a" |
|
300 "max a b == (if a <= b then b else a)" |
|
301 |
|
302 lemma min_leastL: "(!!x. least <= x) ==> min least x = least" |
|
303 by (simp add: min_def) |
|
304 |
|
305 lemma min_of_mono: |
|
306 "ALL x y. (f x <= f y) = (x <= y) ==> min (f m) (f n) = f (min m n)" |
|
307 by (simp add: min_def) |
|
308 |
|
309 lemma max_leastL: "(!!x. least <= x) ==> max least x = x" |
|
310 by (simp add: max_def) |
|
311 |
|
312 lemma max_of_mono: |
|
313 "ALL x y. (f x <= f y) = (x <= y) ==> max (f m) (f n) = f (max m n)" |
|
314 by (simp add: max_def) |
|
315 |
|
316 |
|
317 subsubsection "Orders" |
|
318 |
|
319 axclass order < ord |
|
320 order_refl [iff]: "x <= x" |
|
321 order_trans: "x <= y ==> y <= z ==> x <= z" |
|
322 order_antisym: "x <= y ==> y <= x ==> x = y" |
|
323 order_less_le: "(x < y) = (x <= y & x ~= y)" |
|
324 |
|
325 |
|
326 text {* Reflexivity. *} |
|
327 |
|
328 lemma order_eq_refl: "!!x::'a::order. x = y ==> x <= y" |
|
329 -- {* This form is useful with the classical reasoner. *} |
|
330 apply (erule ssubst) |
|
331 apply (rule order_refl) |
|
332 done |
|
333 |
|
334 lemma order_less_irrefl [simp]: "~ x < (x::'a::order)" |
|
335 by (simp add: order_less_le) |
|
336 |
|
337 lemma order_le_less: "((x::'a::order) <= y) = (x < y | x = y)" |
|
338 -- {* NOT suitable for iff, since it can cause PROOF FAILED. *} |
|
339 apply (simp add: order_less_le) |
|
340 apply (blast intro!: order_refl) |
|
341 done |
|
342 |
|
343 lemmas order_le_imp_less_or_eq = order_le_less [THEN iffD1, standard] |
|
344 |
|
345 lemma order_less_imp_le: "!!x::'a::order. x < y ==> x <= y" |
|
346 by (simp add: order_less_le) |
|
347 |
|
348 |
|
349 text {* Asymmetry. *} |
|
350 |
|
351 lemma order_less_not_sym: "(x::'a::order) < y ==> ~ (y < x)" |
|
352 by (simp add: order_less_le order_antisym) |
|
353 |
|
354 lemma order_less_asym: "x < (y::'a::order) ==> (~P ==> y < x) ==> P" |
|
355 apply (drule order_less_not_sym) |
|
356 apply (erule contrapos_np) |
|
357 apply simp |
|
358 done |
|
359 |
|
360 |
|
361 text {* Transitivity. *} |
|
362 |
|
363 lemma order_less_trans: "!!x::'a::order. [| x < y; y < z |] ==> x < z" |
|
364 apply (simp add: order_less_le) |
|
365 apply (blast intro: order_trans order_antisym) |
|
366 done |
|
367 |
|
368 lemma order_le_less_trans: "!!x::'a::order. [| x <= y; y < z |] ==> x < z" |
|
369 apply (simp add: order_less_le) |
|
370 apply (blast intro: order_trans order_antisym) |
|
371 done |
|
372 |
|
373 lemma order_less_le_trans: "!!x::'a::order. [| x < y; y <= z |] ==> x < z" |
|
374 apply (simp add: order_less_le) |
|
375 apply (blast intro: order_trans order_antisym) |
|
376 done |
|
377 |
|
378 |
|
379 text {* Useful for simplification, but too risky to include by default. *} |
|
380 |
|
381 lemma order_less_imp_not_less: "(x::'a::order) < y ==> (~ y < x) = True" |
|
382 by (blast elim: order_less_asym) |
|
383 |
|
384 lemma order_less_imp_triv: "(x::'a::order) < y ==> (y < x --> P) = True" |
|
385 by (blast elim: order_less_asym) |
|
386 |
|
387 lemma order_less_imp_not_eq: "(x::'a::order) < y ==> (x = y) = False" |
|
388 by auto |
|
389 |
|
390 lemma order_less_imp_not_eq2: "(x::'a::order) < y ==> (y = x) = False" |
|
391 by auto |
|
392 |
|
393 |
|
394 text {* Other operators. *} |
|
395 |
|
396 lemma min_leastR: "(!!x::'a::order. least <= x) ==> min x least = least" |
|
397 apply (simp add: min_def) |
|
398 apply (blast intro: order_antisym) |
|
399 done |
|
400 |
|
401 lemma max_leastR: "(!!x::'a::order. least <= x) ==> max x least = x" |
|
402 apply (simp add: max_def) |
|
403 apply (blast intro: order_antisym) |
|
404 done |
|
405 |
|
406 |
|
407 subsubsection {* Least value operator *} |
|
408 |
|
409 constdefs |
|
410 Least :: "('a::ord => bool) => 'a" (binder "LEAST " 10) |
|
411 "Least P == THE x. P x & (ALL y. P y --> x <= y)" |
|
412 -- {* We can no longer use LeastM because the latter requires Hilbert-AC. *} |
|
413 |
|
414 lemma LeastI2: |
|
415 "[| P (x::'a::order); |
|
416 !!y. P y ==> x <= y; |
|
417 !!x. [| P x; ALL y. P y --> x \<le> y |] ==> Q x |] |
|
418 ==> Q (Least P)"; |
|
419 apply (unfold Least_def) |
|
420 apply (rule theI2) |
|
421 apply (blast intro: order_antisym)+ |
|
422 done |
|
423 |
|
424 lemma Least_equality: |
|
425 "[| P (k::'a::order); !!x. P x ==> k <= x |] ==> (LEAST x. P x) = k"; |
|
426 apply (simp add: Least_def) |
|
427 apply (rule the_equality) |
|
428 apply (auto intro!: order_antisym) |
|
429 done |
|
430 |
|
431 |
|
432 subsubsection "Linear / total orders" |
|
433 |
|
434 axclass linorder < order |
|
435 linorder_linear: "x <= y | y <= x" |
|
436 |
|
437 lemma linorder_less_linear: "!!x::'a::linorder. x<y | x=y | y<x" |
|
438 apply (simp add: order_less_le) |
|
439 apply (insert linorder_linear) |
|
440 apply blast |
|
441 done |
|
442 |
|
443 lemma linorder_cases [case_names less equal greater]: |
|
444 "((x::'a::linorder) < y ==> P) ==> (x = y ==> P) ==> (y < x ==> P) ==> P" |
|
445 apply (insert linorder_less_linear) |
|
446 apply blast |
|
447 done |
|
448 |
|
449 lemma linorder_not_less: "!!x::'a::linorder. (~ x < y) = (y <= x)" |
|
450 apply (simp add: order_less_le) |
|
451 apply (insert linorder_linear) |
|
452 apply (blast intro: order_antisym) |
|
453 done |
|
454 |
|
455 lemma linorder_not_le: "!!x::'a::linorder. (~ x <= y) = (y < x)" |
|
456 apply (simp add: order_less_le) |
|
457 apply (insert linorder_linear) |
|
458 apply (blast intro: order_antisym) |
|
459 done |
|
460 |
|
461 lemma linorder_neq_iff: "!!x::'a::linorder. (x ~= y) = (x<y | y<x)" |
|
462 apply (cut_tac x = x and y = y in linorder_less_linear) |
|
463 apply auto |
|
464 done |
|
465 |
|
466 lemma linorder_neqE: "x ~= (y::'a::linorder) ==> (x < y ==> R) ==> (y < x ==> R) ==> R" |
|
467 apply (simp add: linorder_neq_iff) |
|
468 apply blast |
|
469 done |
|
470 |
|
471 |
|
472 subsubsection "Min and max on (linear) orders" |
|
473 |
|
474 lemma min_same [simp]: "min (x::'a::order) x = x" |
|
475 by (simp add: min_def) |
|
476 |
|
477 lemma max_same [simp]: "max (x::'a::order) x = x" |
|
478 by (simp add: max_def) |
|
479 |
|
480 lemma le_max_iff_disj: "!!z::'a::linorder. (z <= max x y) = (z <= x | z <= y)" |
|
481 apply (simp add: max_def) |
|
482 apply (insert linorder_linear) |
|
483 apply (blast intro: order_trans) |
|
484 done |
|
485 |
|
486 lemma le_maxI1: "(x::'a::linorder) <= max x y" |
|
487 by (simp add: le_max_iff_disj) |
|
488 |
|
489 lemma le_maxI2: "(y::'a::linorder) <= max x y" |
|
490 -- {* CANNOT use with @{text "[intro!]"} because blast will give PROOF FAILED. *} |
|
491 by (simp add: le_max_iff_disj) |
|
492 |
|
493 lemma less_max_iff_disj: "!!z::'a::linorder. (z < max x y) = (z < x | z < y)" |
|
494 apply (simp add: max_def order_le_less) |
|
495 apply (insert linorder_less_linear) |
|
496 apply (blast intro: order_less_trans) |
|
497 done |
|
498 |
|
499 lemma max_le_iff_conj [simp]: |
|
500 "!!z::'a::linorder. (max x y <= z) = (x <= z & y <= z)" |
|
501 apply (simp add: max_def) |
|
502 apply (insert linorder_linear) |
|
503 apply (blast intro: order_trans) |
|
504 done |
|
505 |
|
506 lemma max_less_iff_conj [simp]: |
|
507 "!!z::'a::linorder. (max x y < z) = (x < z & y < z)" |
|
508 apply (simp add: order_le_less max_def) |
|
509 apply (insert linorder_less_linear) |
|
510 apply (blast intro: order_less_trans) |
|
511 done |
|
512 |
|
513 lemma le_min_iff_conj [simp]: |
|
514 "!!z::'a::linorder. (z <= min x y) = (z <= x & z <= y)" |
|
515 -- {* @{text "[iff]"} screws up a Q{text blast} in MiniML *} |
|
516 apply (simp add: min_def) |
|
517 apply (insert linorder_linear) |
|
518 apply (blast intro: order_trans) |
|
519 done |
|
520 |
|
521 lemma min_less_iff_conj [simp]: |
|
522 "!!z::'a::linorder. (z < min x y) = (z < x & z < y)" |
|
523 apply (simp add: order_le_less min_def) |
|
524 apply (insert linorder_less_linear) |
|
525 apply (blast intro: order_less_trans) |
|
526 done |
|
527 |
|
528 lemma min_le_iff_disj: "!!z::'a::linorder. (min x y <= z) = (x <= z | y <= z)" |
|
529 apply (simp add: min_def) |
|
530 apply (insert linorder_linear) |
|
531 apply (blast intro: order_trans) |
|
532 done |
|
533 |
|
534 lemma min_less_iff_disj: "!!z::'a::linorder. (min x y < z) = (x < z | y < z)" |
|
535 apply (simp add: min_def order_le_less) |
|
536 apply (insert linorder_less_linear) |
|
537 apply (blast intro: order_less_trans) |
|
538 done |
|
539 |
|
540 lemma split_min: |
|
541 "P (min (i::'a::linorder) j) = ((i <= j --> P(i)) & (~ i <= j --> P(j)))" |
|
542 by (simp add: min_def) |
|
543 |
|
544 lemma split_max: |
|
545 "P (max (i::'a::linorder) j) = ((i <= j --> P(j)) & (~ i <= j --> P(i)))" |
|
546 by (simp add: max_def) |
|
547 |
|
548 |
|
549 subsubsection "Bounded quantifiers" |
|
550 |
|
551 syntax |
|
552 "_lessAll" :: "[idt, 'a, bool] => bool" ("(3ALL _<_./ _)" [0, 0, 10] 10) |
|
553 "_lessEx" :: "[idt, 'a, bool] => bool" ("(3EX _<_./ _)" [0, 0, 10] 10) |
|
554 "_leAll" :: "[idt, 'a, bool] => bool" ("(3ALL _<=_./ _)" [0, 0, 10] 10) |
|
555 "_leEx" :: "[idt, 'a, bool] => bool" ("(3EX _<=_./ _)" [0, 0, 10] 10) |
|
556 |
|
557 syntax (symbols) |
|
558 "_lessAll" :: "[idt, 'a, bool] => bool" ("(3\<forall>_<_./ _)" [0, 0, 10] 10) |
|
559 "_lessEx" :: "[idt, 'a, bool] => bool" ("(3\<exists>_<_./ _)" [0, 0, 10] 10) |
|
560 "_leAll" :: "[idt, 'a, bool] => bool" ("(3\<forall>_\<le>_./ _)" [0, 0, 10] 10) |
|
561 "_leEx" :: "[idt, 'a, bool] => bool" ("(3\<exists>_\<le>_./ _)" [0, 0, 10] 10) |
|
562 |
|
563 syntax (HOL) |
|
564 "_lessAll" :: "[idt, 'a, bool] => bool" ("(3! _<_./ _)" [0, 0, 10] 10) |
|
565 "_lessEx" :: "[idt, 'a, bool] => bool" ("(3? _<_./ _)" [0, 0, 10] 10) |
|
566 "_leAll" :: "[idt, 'a, bool] => bool" ("(3! _<=_./ _)" [0, 0, 10] 10) |
|
567 "_leEx" :: "[idt, 'a, bool] => bool" ("(3? _<=_./ _)" [0, 0, 10] 10) |
|
568 |
|
569 translations |
|
570 "ALL x<y. P" => "ALL x. x < y --> P" |
|
571 "EX x<y. P" => "EX x. x < y & P" |
|
572 "ALL x<=y. P" => "ALL x. x <= y --> P" |
|
573 "EX x<=y. P" => "EX x. x <= y & P" |
|
574 |
263 end |
575 end |