author  berghofe 
Tue, 30 May 2000 18:02:49 +0200  
changeset 9001  93af64f54bf2 
parent 7713  f4fe9d620107 
child 9969  4753185f1dd2 
permissions  rwrr 
1465  1 
(* Title: HOL/mono.ML 
923  2 
ID: $Id$ 
1465  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
923  4 
Copyright 1991 University of Cambridge 
5 

6 
Monotonicity of various operations 

7 
*) 

8 

5316  9 
Goal "A<=B ==> f``A <= f``B"; 
2922  10 
by (Blast_tac 1); 
923  11 
qed "image_mono"; 
12 

5316  13 
Goal "A<=B ==> Pow(A) <= Pow(B)"; 
2922  14 
by (Blast_tac 1); 
923  15 
qed "Pow_mono"; 
16 

5316  17 
Goal "A<=B ==> Union(A) <= Union(B)"; 
2922  18 
by (Blast_tac 1); 
923  19 
qed "Union_mono"; 
20 

5316  21 
Goal "B<=A ==> Inter(A) <= Inter(B)"; 
2922  22 
by (Blast_tac 1); 
923  23 
qed "Inter_anti_mono"; 
24 

5316  25 
val prems = Goal 
923  26 
"[ A<=B; !!x. x:A ==> f(x)<=g(x) ] ==> \ 
27 
\ (UN x:A. f(x)) <= (UN x:B. g(x))"; 

4089  28 
by (blast_tac (claset() addIs (prems RL [subsetD])) 1); 
923  29 
qed "UN_mono"; 
30 

4159
4aff9b7e5597
UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents:
4089
diff
changeset

31 
(*The last inclusion is POSITIVE! *) 
5316  32 
val prems = Goal 
923  33 
"[ B<=A; !!x. x:A ==> f(x)<=g(x) ] ==> \ 
34 
\ (INT x:A. f(x)) <= (INT x:A. g(x))"; 

4089  35 
by (blast_tac (claset() addIs (prems RL [subsetD])) 1); 
923  36 
qed "INT_anti_mono"; 
37 

5316  38 
Goal "C<=D ==> insert a C <= insert a D"; 
2922  39 
by (Blast_tac 1); 
1849  40 
qed "insert_mono"; 
41 

5316  42 
Goal "[ A<=C; B<=D ] ==> A Un B <= C Un D"; 
2922  43 
by (Blast_tac 1); 
923  44 
qed "Un_mono"; 
45 

5316  46 
Goal "[ A<=C; B<=D ] ==> A Int B <= C Int D"; 
2922  47 
by (Blast_tac 1); 
923  48 
qed "Int_mono"; 
49 

5316  50 
Goal "!!A::'a set. [ A<=C; D<=B ] ==> AB <= CD"; 
2922  51 
by (Blast_tac 1); 
923  52 
qed "Diff_mono"; 
53 

5490  54 
Goal "!!A::'a set. A <= B ==> B <= A"; 
2922  55 
by (Blast_tac 1); 
923  56 
qed "Compl_anti_mono"; 
57 

58 
(** Monotonicity of implications. For inductive definitions **) 

59 

5316  60 
Goal "A<=B ==> x:A > x:B"; 
923  61 
by (rtac impI 1); 
62 
by (etac subsetD 1); 

63 
by (assume_tac 1); 

64 
qed "in_mono"; 

65 

5316  66 
Goal "[ P1>Q1; P2>Q2 ] ==> (P1&P2) > (Q1&Q2)"; 
2922  67 
by (Blast_tac 1); 
923  68 
qed "conj_mono"; 
69 

5316  70 
Goal "[ P1>Q1; P2>Q2 ] ==> (P1P2) > (Q1Q2)"; 
2922  71 
by (Blast_tac 1); 
923  72 
qed "disj_mono"; 
73 

5316  74 
Goal "[ Q1>P1; P2>Q2 ] ==> (P1>P2)>(Q1>Q2)"; 
2922  75 
by (Blast_tac 1); 
923  76 
qed "imp_mono"; 
77 

5316  78 
Goal "P>P"; 
923  79 
by (rtac impI 1); 
80 
by (assume_tac 1); 

81 
qed "imp_refl"; 

82 

5316  83 
val [PQimp] = Goal 
3842  84 
"[ !!x. P(x) > Q(x) ] ==> (EX x. P(x)) > (EX x. Q(x))"; 
4089  85 
by (blast_tac (claset() addIs [PQimp RS mp]) 1); 
923  86 
qed "ex_mono"; 
87 

5316  88 
val [PQimp] = Goal 
3842  89 
"[ !!x. P(x) > Q(x) ] ==> (ALL x. P(x)) > (ALL x. Q(x))"; 
4089  90 
by (blast_tac (claset() addIs [PQimp RS mp]) 1); 
923  91 
qed "all_mono"; 
92 

5316  93 
val [PQimp] = Goal 
923  94 
"[ !!x. P(x) > Q(x) ] ==> Collect(P) <= Collect(Q)"; 
4089  95 
by (blast_tac (claset() addIs [PQimp RS mp]) 1); 
923  96 
qed "Collect_mono"; 
97 

5316  98 
val [subs,PQimp] = Goal 
923  99 
"[ A<=B; !!x. x:A ==> P(x) > Q(x) \ 
100 
\ ] ==> A Int Collect(P) <= B Int Collect(Q)"; 

4089  101 
by (blast_tac (claset() addIs [subs RS subsetD, PQimp RS mp]) 1); 
923  102 
qed "Int_Collect_mono"; 
103 

104 
val basic_monos = [subset_refl, imp_refl, disj_mono, conj_mono, 

1515  105 
ex_mono, Collect_mono, in_mono]; 
923  106 

7109  107 
(* Courtesy of Stephan Merz *) 
7064  108 
Goalw [Least_def,mono_def] 
109 
"[ mono (f::'a::order => 'b::order); ? x:S. ! y:S. x <= y ] \ 

110 
\ ==> (LEAST y. y : f``S) = f(LEAST x. x : S)"; 

111 
by (etac bexE 1); 

112 
by (rtac selectI2 1); 

113 
by (Force_tac 1); 

114 
by (rtac select_equality 1); 

115 
by (Force_tac 1); 

116 
by (force_tac (claset() addSIs [order_antisym], simpset()) 1); 

117 
qed "Least_mono"; 

7713  118 

119 
Goal "[ a = b; c = d; b > d ] ==> a > c"; 

120 
by (Fast_tac 1); 

121 
qed "eq_to_mono"; 

122 

123 
Goal "[ a = b; c = d; ~ b > ~ d ] ==> ~ a > ~ c"; 

124 
by (Fast_tac 1); 

125 
qed "eq_to_mono2"; 