|
1 (* Title: HOL/mono |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1991 University of Cambridge |
|
5 |
|
6 Monotonicity of various operations |
|
7 *) |
|
8 |
|
9 goal Set.thy "!!A B. A<=B ==> f``A <= f``B"; |
|
10 by (fast_tac set_cs 1); |
|
11 qed "image_mono"; |
|
12 |
|
13 goal Set.thy "!!A B. A<=B ==> Pow(A) <= Pow(B)"; |
|
14 by (fast_tac set_cs 1); |
|
15 qed "Pow_mono"; |
|
16 |
|
17 goal Set.thy "!!A B. A<=B ==> Union(A) <= Union(B)"; |
|
18 by (fast_tac set_cs 1); |
|
19 qed "Union_mono"; |
|
20 |
|
21 goal Set.thy "!!A B. B<=A ==> Inter(A) <= Inter(B)"; |
|
22 by (fast_tac set_cs 1); |
|
23 qed "Inter_anti_mono"; |
|
24 |
|
25 val prems = goal Set.thy |
|
26 "[| A<=B; !!x. x:A ==> f(x)<=g(x) |] ==> \ |
|
27 \ (UN x:A. f(x)) <= (UN x:B. g(x))"; |
|
28 by (fast_tac (set_cs addIs (prems RL [subsetD])) 1); |
|
29 qed "UN_mono"; |
|
30 |
|
31 val [prem] = goal Set.thy |
|
32 "[| !!x. f(x)<=g(x) |] ==> (UN x. f(x)) <= (UN x. g(x))"; |
|
33 by (fast_tac (set_cs addIs [prem RS subsetD]) 1); |
|
34 qed "UN1_mono"; |
|
35 |
|
36 val prems = goal Set.thy |
|
37 "[| B<=A; !!x. x:A ==> f(x)<=g(x) |] ==> \ |
|
38 \ (INT x:A. f(x)) <= (INT x:A. g(x))"; |
|
39 by (fast_tac (set_cs addIs (prems RL [subsetD])) 1); |
|
40 qed "INT_anti_mono"; |
|
41 |
|
42 (*The inclusion is POSITIVE! *) |
|
43 val [prem] = goal Set.thy |
|
44 "[| !!x. f(x)<=g(x) |] ==> (INT x. f(x)) <= (INT x. g(x))"; |
|
45 by (fast_tac (set_cs addIs [prem RS subsetD]) 1); |
|
46 qed "INT1_mono"; |
|
47 |
|
48 goal Set.thy "!!A B. [| A<=C; B<=D |] ==> A Un B <= C Un D"; |
|
49 by (fast_tac set_cs 1); |
|
50 qed "Un_mono"; |
|
51 |
|
52 goal Set.thy "!!A B. [| A<=C; B<=D |] ==> A Int B <= C Int D"; |
|
53 by (fast_tac set_cs 1); |
|
54 qed "Int_mono"; |
|
55 |
|
56 goal Set.thy "!!A::'a set. [| A<=C; D<=B |] ==> A-B <= C-D"; |
|
57 by (fast_tac set_cs 1); |
|
58 qed "Diff_mono"; |
|
59 |
|
60 goal Set.thy "!!A B. A<=B ==> Compl(B) <= Compl(A)"; |
|
61 by (fast_tac set_cs 1); |
|
62 qed "Compl_anti_mono"; |
|
63 |
|
64 val prems = goal Prod.thy |
|
65 "[| A<=C; !!x. x:A ==> B<=D |] ==> Sigma A (%x.B) <= Sigma C (%x.D)"; |
|
66 by (cut_facts_tac prems 1); |
|
67 by (fast_tac (set_cs addIs (prems RL [subsetD]) |
|
68 addSIs [SigmaI] |
|
69 addSEs [SigmaE]) 1); |
|
70 qed "Sigma_mono"; |
|
71 |
|
72 |
|
73 (** Monotonicity of implications. For inductive definitions **) |
|
74 |
|
75 goal Set.thy "!!A B x. A<=B ==> x:A --> x:B"; |
|
76 by (rtac impI 1); |
|
77 by (etac subsetD 1); |
|
78 by (assume_tac 1); |
|
79 qed "in_mono"; |
|
80 |
|
81 goal HOL.thy "!!P1 P2 Q1 Q2. [| P1-->Q1; P2-->Q2 |] ==> (P1&P2) --> (Q1&Q2)"; |
|
82 by (fast_tac HOL_cs 1); |
|
83 qed "conj_mono"; |
|
84 |
|
85 goal HOL.thy "!!P1 P2 Q1 Q2. [| P1-->Q1; P2-->Q2 |] ==> (P1|P2) --> (Q1|Q2)"; |
|
86 by (fast_tac HOL_cs 1); |
|
87 qed "disj_mono"; |
|
88 |
|
89 goal HOL.thy "!!P1 P2 Q1 Q2.[| Q1-->P1; P2-->Q2 |] ==> (P1-->P2)-->(Q1-->Q2)"; |
|
90 by (fast_tac HOL_cs 1); |
|
91 qed "imp_mono"; |
|
92 |
|
93 goal HOL.thy "P-->P"; |
|
94 by (rtac impI 1); |
|
95 by (assume_tac 1); |
|
96 qed "imp_refl"; |
|
97 |
|
98 val [PQimp] = goal HOL.thy |
|
99 "[| !!x. P(x) --> Q(x) |] ==> (EX x.P(x)) --> (EX x.Q(x))"; |
|
100 by (fast_tac (HOL_cs addIs [PQimp RS mp]) 1); |
|
101 qed "ex_mono"; |
|
102 |
|
103 val [PQimp] = goal HOL.thy |
|
104 "[| !!x. P(x) --> Q(x) |] ==> (ALL x.P(x)) --> (ALL x.Q(x))"; |
|
105 by (fast_tac (HOL_cs addIs [PQimp RS mp]) 1); |
|
106 qed "all_mono"; |
|
107 |
|
108 val [PQimp] = goal Set.thy |
|
109 "[| !!x. P(x) --> Q(x) |] ==> Collect(P) <= Collect(Q)"; |
|
110 by (fast_tac (set_cs addIs [PQimp RS mp]) 1); |
|
111 qed "Collect_mono"; |
|
112 |
|
113 (*Used in indrule.ML*) |
|
114 val [subs,PQimp] = goal Set.thy |
|
115 "[| A<=B; !!x. x:A ==> P(x) --> Q(x) \ |
|
116 \ |] ==> A Int Collect(P) <= B Int Collect(Q)"; |
|
117 by (fast_tac (set_cs addIs [subs RS subsetD, PQimp RS mp]) 1); |
|
118 qed "Int_Collect_mono"; |
|
119 |
|
120 (*Used in intr_elim.ML and in individual datatype definitions*) |
|
121 val basic_monos = [subset_refl, imp_refl, disj_mono, conj_mono, |
|
122 ex_mono, Collect_mono, Part_mono, in_mono]; |
|
123 |