equal
deleted
inserted
replaced
4 Copyright 1991 University of Cambridge |
4 Copyright 1991 University of Cambridge |
5 |
5 |
6 Monotonicity of various operations |
6 Monotonicity of various operations |
7 *) |
7 *) |
8 |
8 |
9 Goal "A<=B ==> f``A <= f``B"; |
9 Goal "A<=B ==> f`A <= f`B"; |
10 by (Blast_tac 1); |
10 by (Blast_tac 1); |
11 qed "image_mono"; |
11 qed "image_mono"; |
12 |
12 |
13 Goal "A<=B ==> Pow(A) <= Pow(B)"; |
13 Goal "A<=B ==> Pow(A) <= Pow(B)"; |
14 by (Blast_tac 1); |
14 by (Blast_tac 1); |
105 ex_mono, Collect_mono, in_mono]; |
105 ex_mono, Collect_mono, in_mono]; |
106 |
106 |
107 (* Courtesy of Stephan Merz *) |
107 (* Courtesy of Stephan Merz *) |
108 Goalw [Least_def,mono_def] |
108 Goalw [Least_def,mono_def] |
109 "[| mono (f::'a::order => 'b::order); ? x:S. ! y:S. x <= y |] \ |
109 "[| mono (f::'a::order => 'b::order); ? x:S. ! y:S. x <= y |] \ |
110 \ ==> (LEAST y. y : f``S) = f(LEAST x. x : S)"; |
110 \ ==> (LEAST y. y : f`S) = f(LEAST x. x : S)"; |
111 by (etac bexE 1); |
111 by (etac bexE 1); |
112 by (rtac someI2 1); |
112 by (rtac someI2 1); |
113 by (Force_tac 1); |
113 by (Force_tac 1); |
114 by (rtac some_equality 1); |
114 by (rtac some_equality 1); |
115 by (Force_tac 1); |
115 by (Force_tac 1); |