author  paulson 
Thu, 11 Jul 1996 15:14:41 +0200  
changeset 1849  bec272e3e888 
parent 1760  6f41a494f3b1 
child 2922  580647a879cf 
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 

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 ] ==> AB <= CD"; 

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 ] ==> (P1P2) > (Q1Q2)"; 

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 