summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/AxClasses/Lattice/CLattice.ML

author | paulson |

Wed Nov 05 13:23:46 1997 +0100 (1997-11-05) | |

changeset 4153 | e534c4c32d54 |

parent 4091 | 771b1f6422a8 |

child 5069 | 3ea049f7979d |

permissions | -rw-r--r-- |

Ran expandshort, especially to introduce Safe_tac

2 open CLattice;

5 (** basic properties of "Inf" and "Sup" **)

7 (* unique existence *)

9 goalw thy [Inf_def] "is_Inf A (Inf A)";

10 by (rtac (ex_Inf RS spec RS selectI1) 1);

11 qed "Inf_is_Inf";

13 goal thy "is_Inf A inf --> Inf A = inf";

14 by (rtac impI 1);

15 by (rtac (is_Inf_uniq RS mp) 1);

16 by (rtac conjI 1);

17 by (rtac Inf_is_Inf 1);

18 by (assume_tac 1);

19 qed "Inf_uniq";

21 goalw thy [Ex1_def] "ALL A. EX! inf::'a::clattice. is_Inf A inf";

22 by Safe_tac;

23 by (Step_tac 1);

24 by (Step_tac 1);

25 by (rtac Inf_is_Inf 1);

26 by (rtac (Inf_uniq RS mp RS sym) 1);

27 by (assume_tac 1);

28 qed "ex1_Inf";

31 goalw thy [Sup_def] "is_Sup A (Sup A)";

32 by (rtac (ex_Sup RS spec RS selectI1) 1);

33 qed "Sup_is_Sup";

35 goal thy "is_Sup A sup --> Sup A = sup";

36 by (rtac impI 1);

37 by (rtac (is_Sup_uniq RS mp) 1);

38 by (rtac conjI 1);

39 by (rtac Sup_is_Sup 1);

40 by (assume_tac 1);

41 qed "Sup_uniq";

43 goalw thy [Ex1_def] "ALL A. EX! sup::'a::clattice. is_Sup A sup";

44 by Safe_tac;

45 by (Step_tac 1);

46 by (Step_tac 1);

47 by (rtac Sup_is_Sup 1);

48 by (rtac (Sup_uniq RS mp RS sym) 1);

49 by (assume_tac 1);

50 qed "ex1_Sup";

53 (* "Inf" yields g.l.bs, "Sup" yields l.u.bs. --- in pieces *)

55 val prems = goalw thy [Inf_def] "x:A ==> Inf A [= x";

56 by (cut_facts_tac prems 1);

57 by (rtac selectI2 1);

58 by (rtac Inf_is_Inf 1);

59 by (rewtac is_Inf_def);

60 by (Fast_tac 1);

61 qed "Inf_lb";

63 val [prem] = goalw thy [Inf_def] "(!!x. x:A ==> z [= x) ==> z [= Inf A";

64 by (rtac selectI2 1);

65 by (rtac Inf_is_Inf 1);

66 by (rewtac is_Inf_def);

67 by (Step_tac 1);

68 by (Step_tac 1);

69 by (etac mp 1);

70 by (rtac ballI 1);

71 by (etac prem 1);

72 qed "Inf_ub_lbs";

75 val prems = goalw thy [Sup_def] "x:A ==> x [= Sup A";

76 by (cut_facts_tac prems 1);

77 by (rtac selectI2 1);

78 by (rtac Sup_is_Sup 1);

79 by (rewtac is_Sup_def);

80 by (Fast_tac 1);

81 qed "Sup_ub";

83 val [prem] = goalw thy [Sup_def] "(!!x. x:A ==> x [= z) ==> Sup A [= z";

84 by (rtac selectI2 1);

85 by (rtac Sup_is_Sup 1);

86 by (rewtac is_Sup_def);

87 by (Step_tac 1);

88 by (Step_tac 1);

89 by (etac mp 1);

90 by (rtac ballI 1);

91 by (etac prem 1);

92 qed "Sup_lb_ubs";

95 (** minorized Infs / majorized Sups **)

97 goal thy "(x [= Inf A) = (ALL y:A. x [= y)";

98 by (rtac iffI 1);

99 (*==>*)

100 by (rtac ballI 1);

101 by (rtac (le_trans RS mp) 1);

102 by (etac conjI 1);

103 by (etac Inf_lb 1);

104 (*<==*)

105 by (rtac Inf_ub_lbs 1);

106 by (Fast_tac 1);

107 qed "le_Inf_eq";

109 goal thy "(Sup A [= x) = (ALL y:A. y [= x)";

110 by (rtac iffI 1);

111 (*==>*)

112 by (rtac ballI 1);

113 by (rtac (le_trans RS mp) 1);

114 by (rtac conjI 1);

115 by (etac Sup_ub 1);

116 by (assume_tac 1);

117 (*<==*)

118 by (rtac Sup_lb_ubs 1);

119 by (Fast_tac 1);

120 qed "ge_Sup_eq";

124 (** Subsets and limits **)

126 goal thy "A <= B --> Inf B [= Inf A";

127 by (rtac impI 1);

128 by (stac le_Inf_eq 1);

129 by (rewtac Ball_def);

130 by Safe_tac;

131 by (dtac subsetD 1);

132 by (assume_tac 1);

133 by (etac Inf_lb 1);

134 qed "Inf_subset_antimon";

136 goal thy "A <= B --> Sup A [= Sup B";

137 by (rtac impI 1);

138 by (stac ge_Sup_eq 1);

139 by (rewtac Ball_def);

140 by Safe_tac;

141 by (dtac subsetD 1);

142 by (assume_tac 1);

143 by (etac Sup_ub 1);

144 qed "Sup_subset_mon";

147 (** singleton / empty limits **)

149 goal thy "Inf {x} = x";

150 by (rtac (Inf_uniq RS mp) 1);

151 by (rewtac is_Inf_def);

152 by Safe_tac;

153 by (rtac le_refl 1);

154 by (Fast_tac 1);

155 qed "sing_Inf_eq";

157 goal thy "Sup {x} = x";

158 by (rtac (Sup_uniq RS mp) 1);

159 by (rewtac is_Sup_def);

160 by Safe_tac;

161 by (rtac le_refl 1);

162 by (Fast_tac 1);

163 qed "sing_Sup_eq";

166 goal thy "Inf {} = Sup {x. True}";

167 by (rtac (Inf_uniq RS mp) 1);

168 by (rewtac is_Inf_def);

169 by Safe_tac;

170 by (rtac (sing_Sup_eq RS subst) 1);

171 back();

172 by (rtac (Sup_subset_mon RS mp) 1);

173 by (Fast_tac 1);

174 qed "empty_Inf_eq";

176 goal thy "Sup {} = Inf {x. True}";

177 by (rtac (Sup_uniq RS mp) 1);

178 by (rewtac is_Sup_def);

179 by Safe_tac;

180 by (rtac (sing_Inf_eq RS subst) 1);

181 by (rtac (Inf_subset_antimon RS mp) 1);

182 by (Fast_tac 1);

183 qed "empty_Sup_eq";