author | wenzelm |
Fri, 07 Mar 1997 11:48:46 +0100 | |
changeset 2754 | 59bd96046ad6 |
parent 1849 | bec272e3e888 |
child 2922 | 580647a879cf |
permissions | -rw-r--r-- |
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 |
||
9 |
goal Set.thy "!!A B. A<=B ==> f``A <= f``B"; |
|
1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1515
diff
changeset
|
10 |
by (Fast_tac 1); |
923 | 11 |
qed "image_mono"; |
12 |
||
13 |
goal Set.thy "!!A B. A<=B ==> Pow(A) <= Pow(B)"; |
|
1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1515
diff
changeset
|
14 |
by (Fast_tac 1); |
923 | 15 |
qed "Pow_mono"; |
16 |
||
17 |
goal Set.thy "!!A B. A<=B ==> Union(A) <= Union(B)"; |
|
1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1515
diff
changeset
|
18 |
by (Fast_tac 1); |
923 | 19 |
qed "Union_mono"; |
20 |
||
21 |
goal Set.thy "!!A B. B<=A ==> Inter(A) <= Inter(B)"; |
|
1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1515
diff
changeset
|
22 |
by (Fast_tac 1); |
923 | 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))"; |
|
1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1515
diff
changeset
|
28 |
by (fast_tac (!claset addIs (prems RL [subsetD])) 1); |
923 | 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))"; |
|
1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1515
diff
changeset
|
33 |
by (fast_tac (!claset addIs [prem RS subsetD]) 1); |
923 | 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))"; |
|
1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1515
diff
changeset
|
39 |
by (fast_tac (!claset addIs (prems RL [subsetD])) 1); |
923 | 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))"; |
|
1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1515
diff
changeset
|
45 |
by (fast_tac (!claset addIs [prem RS subsetD]) 1); |
923 | 46 |
qed "INT1_mono"; |
47 |
||
1849 | 48 |
goal Set.thy "!!C D. C<=D ==> insert a C <= insert a D"; |
49 |
by (Fast_tac 1); |
|
50 |
qed "insert_mono"; |
|
51 |
||
923 | 52 |
goal Set.thy "!!A B. [| A<=C; B<=D |] ==> A Un B <= C Un D"; |
1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1515
diff
changeset
|
53 |
by (Fast_tac 1); |
923 | 54 |
qed "Un_mono"; |
55 |
||
56 |
goal Set.thy "!!A B. [| A<=C; B<=D |] ==> A Int B <= C Int D"; |
|
1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1515
diff
changeset
|
57 |
by (Fast_tac 1); |
923 | 58 |
qed "Int_mono"; |
59 |
||
60 |
goal Set.thy "!!A::'a set. [| A<=C; D<=B |] ==> A-B <= C-D"; |
|
1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1515
diff
changeset
|
61 |
by (Fast_tac 1); |
923 | 62 |
qed "Diff_mono"; |
63 |
||
64 |
goal Set.thy "!!A B. A<=B ==> Compl(B) <= Compl(A)"; |
|
1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1515
diff
changeset
|
65 |
by (Fast_tac 1); |
923 | 66 |
qed "Compl_anti_mono"; |
67 |
||
68 |
(** Monotonicity of implications. For inductive definitions **) |
|
69 |
||
70 |
goal Set.thy "!!A B x. A<=B ==> x:A --> x:B"; |
|
71 |
by (rtac impI 1); |
|
72 |
by (etac subsetD 1); |
|
73 |
by (assume_tac 1); |
|
74 |
qed "in_mono"; |
|
75 |
||
76 |
goal HOL.thy "!!P1 P2 Q1 Q2. [| P1-->Q1; P2-->Q2 |] ==> (P1&P2) --> (Q1&Q2)"; |
|
1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1515
diff
changeset
|
77 |
by (Fast_tac 1); |
923 | 78 |
qed "conj_mono"; |
79 |
||
80 |
goal HOL.thy "!!P1 P2 Q1 Q2. [| P1-->Q1; P2-->Q2 |] ==> (P1|P2) --> (Q1|Q2)"; |
|
1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1515
diff
changeset
|
81 |
by (Fast_tac 1); |
923 | 82 |
qed "disj_mono"; |
83 |
||
84 |
goal HOL.thy "!!P1 P2 Q1 Q2.[| Q1-->P1; P2-->Q2 |] ==> (P1-->P2)-->(Q1-->Q2)"; |
|
1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1515
diff
changeset
|
85 |
by (Fast_tac 1); |
923 | 86 |
qed "imp_mono"; |
87 |
||
88 |
goal HOL.thy "P-->P"; |
|
89 |
by (rtac impI 1); |
|
90 |
by (assume_tac 1); |
|
91 |
qed "imp_refl"; |
|
92 |
||
93 |
val [PQimp] = goal HOL.thy |
|
94 |
"[| !!x. P(x) --> Q(x) |] ==> (EX x.P(x)) --> (EX x.Q(x))"; |
|
1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1515
diff
changeset
|
95 |
by (fast_tac (!claset addIs [PQimp RS mp]) 1); |
923 | 96 |
qed "ex_mono"; |
97 |
||
98 |
val [PQimp] = goal HOL.thy |
|
99 |
"[| !!x. P(x) --> Q(x) |] ==> (ALL x.P(x)) --> (ALL x.Q(x))"; |
|
1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1515
diff
changeset
|
100 |
by (fast_tac (!claset addIs [PQimp RS mp]) 1); |
923 | 101 |
qed "all_mono"; |
102 |
||
103 |
val [PQimp] = goal Set.thy |
|
104 |
"[| !!x. P(x) --> Q(x) |] ==> Collect(P) <= Collect(Q)"; |
|
1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1515
diff
changeset
|
105 |
by (fast_tac (!claset addIs [PQimp RS mp]) 1); |
923 | 106 |
qed "Collect_mono"; |
107 |
||
108 |
(*Used in indrule.ML*) |
|
109 |
val [subs,PQimp] = goal Set.thy |
|
110 |
"[| A<=B; !!x. x:A ==> P(x) --> Q(x) \ |
|
111 |
\ |] ==> A Int Collect(P) <= B Int Collect(Q)"; |
|
1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1515
diff
changeset
|
112 |
by (fast_tac (!claset addIs [subs RS subsetD, PQimp RS mp]) 1); |
923 | 113 |
qed "Int_Collect_mono"; |
114 |
||
115 |
(*Used in intr_elim.ML and in individual datatype definitions*) |
|
116 |
val basic_monos = [subset_refl, imp_refl, disj_mono, conj_mono, |
|
1515 | 117 |
ex_mono, Collect_mono, in_mono]; |
923 | 118 |