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

src/HOL/UNITY/UNITY_tactics.ML

author | paulson |

Wed Jan 29 11:02:08 2003 +0100 (2003-01-29) | |

changeset 13790 | 8d7e9fce8c50 |

parent 13786 | ab8f39f48a6f |

child 13792 | d1811693899c |

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

converting UNITY to new-style theories

1 (* Title: HOL/UNITY/UNITY_tactics.ML

2 ID: $Id$

3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory

4 Copyright 2003 University of Cambridge

6 Specialized UNITY tactics, and ML bindings of theorems

7 *)

9 (*Extend*)

10 val Restrict_iff = thm "Restrict_iff";

11 val Restrict_UNIV = thm "Restrict_UNIV";

12 val Restrict_empty = thm "Restrict_empty";

13 val Restrict_Int = thm "Restrict_Int";

14 val Restrict_triv = thm "Restrict_triv";

15 val Restrict_subset = thm "Restrict_subset";

16 val Restrict_eq_mono = thm "Restrict_eq_mono";

17 val Restrict_imageI = thm "Restrict_imageI";

18 val Domain_Restrict = thm "Domain_Restrict";

19 val Image_Restrict = thm "Image_Restrict";

20 val insert_Id_image_Acts = thm "insert_Id_image_Acts";

21 val good_mapI = thm "good_mapI";

22 val good_map_is_surj = thm "good_map_is_surj";

23 val fst_inv_equalityI = thm "fst_inv_equalityI";

24 val project_set_iff = thm "project_set_iff";

25 val extend_set_mono = thm "extend_set_mono";

26 val extend_set_empty = thm "extend_set_empty";

27 val project_set_Int_subset = thm "project_set_Int_subset";

28 val Init_extend = thm "Init_extend";

29 val Init_project = thm "Init_project";

30 val Acts_project = thm "Acts_project";

31 val project_set_UNIV = thm "project_set_UNIV";

32 val project_set_Union = thm "project_set_Union";

33 val project_act_mono = thm "project_act_mono";

34 val project_constrains_project_set = thm "project_constrains_project_set";

35 val project_stable_project_set = thm "project_stable_project_set";

38 (*Rename*)

39 val good_map_bij = thm "good_map_bij";

40 val fst_o_inv_eq_inv = thm "fst_o_inv_eq_inv";

41 val mem_rename_set_iff = thm "mem_rename_set_iff";

42 val extend_set_eq_image = thm "extend_set_eq_image";

43 val Init_rename = thm "Init_rename";

44 val extend_set_inv = thm "extend_set_inv";

45 val bij_extend_act_eq_project_act = thm "bij_extend_act_eq_project_act";

46 val bij_extend_act = thm "bij_extend_act";

47 val bij_project_act = thm "bij_project_act";

48 val bij_inv_project_act_eq = thm "bij_inv_project_act_eq";

49 val Acts_project = thm "Acts_project";

50 val extend_inv = thm "extend_inv";

51 val rename_inv_rename = thm "rename_inv_rename";

52 val rename_rename_inv = thm "rename_rename_inv";

53 val rename_inv_eq = thm "rename_inv_eq";

54 val bij_extend = thm "bij_extend";

55 val bij_project = thm "bij_project";

56 val inv_project_eq = thm "inv_project_eq";

57 val Allowed_rename = thm "Allowed_rename";

58 val bij_rename = thm "bij_rename";

59 val surj_rename = thm "surj_rename";

60 val inj_rename_imp_inj = thm "inj_rename_imp_inj";

61 val surj_rename_imp_surj = thm "surj_rename_imp_surj";

62 val bij_rename_imp_bij = thm "bij_rename_imp_bij";

63 val bij_rename_iff = thm "bij_rename_iff";

64 val rename_SKIP = thm "rename_SKIP";

65 val rename_Join = thm "rename_Join";

66 val rename_JN = thm "rename_JN";

67 val rename_constrains = thm "rename_constrains";

68 val rename_stable = thm "rename_stable";

69 val rename_invariant = thm "rename_invariant";

70 val rename_increasing = thm "rename_increasing";

71 val reachable_rename_eq = thm "reachable_rename_eq";

72 val rename_Constrains = thm "rename_Constrains";

73 val rename_Stable = thm "rename_Stable";

74 val rename_Always = thm "rename_Always";

75 val rename_Increasing = thm "rename_Increasing";

76 val rename_transient = thm "rename_transient";

77 val rename_ensures = thm "rename_ensures";

78 val rename_leadsTo = thm "rename_leadsTo";

79 val rename_LeadsTo = thm "rename_LeadsTo";

80 val rename_rename_guarantees_eq = thm "rename_rename_guarantees_eq";

81 val rename_guarantees_eq_rename_inv = thm "rename_guarantees_eq_rename_inv";

82 val rename_preserves = thm "rename_preserves";

83 val ok_rename_iff = thm "ok_rename_iff";

84 val OK_rename_iff = thm "OK_rename_iff";

85 val bij_eq_rename = thm "bij_eq_rename";

86 val rename_image_constrains = thm "rename_image_constrains";

87 val rename_image_stable = thm "rename_image_stable";

88 val rename_image_increasing = thm "rename_image_increasing";

89 val rename_image_invariant = thm "rename_image_invariant";

90 val rename_image_Constrains = thm "rename_image_Constrains";

91 val rename_image_preserves = thm "rename_image_preserves";

92 val rename_image_Stable = thm "rename_image_Stable";

93 val rename_image_Increasing = thm "rename_image_Increasing";

94 val rename_image_Always = thm "rename_image_Always";

95 val rename_image_leadsTo = thm "rename_image_leadsTo";

96 val rename_image_LeadsTo = thm "rename_image_LeadsTo";

100 (*Lift_prog*)

101 val sub_def = thm "sub_def";

102 val lift_map_def = thm "lift_map_def";

103 val drop_map_def = thm "drop_map_def";

104 val insert_map_inverse = thm "insert_map_inverse";

105 val insert_map_delete_map_eq = thm "insert_map_delete_map_eq";

106 val insert_map_inject1 = thm "insert_map_inject1";

107 val insert_map_inject2 = thm "insert_map_inject2";

108 val insert_map_inject = thm "insert_map_inject";

109 val insert_map_inject = thm "insert_map_inject";

110 val lift_map_eq_iff = thm "lift_map_eq_iff";

111 val drop_map_lift_map_eq = thm "drop_map_lift_map_eq";

112 val inj_lift_map = thm "inj_lift_map";

113 val lift_map_drop_map_eq = thm "lift_map_drop_map_eq";

114 val drop_map_inject = thm "drop_map_inject";

115 val surj_lift_map = thm "surj_lift_map";

116 val bij_lift_map = thm "bij_lift_map";

117 val inv_lift_map_eq = thm "inv_lift_map_eq";

118 val inv_drop_map_eq = thm "inv_drop_map_eq";

119 val bij_drop_map = thm "bij_drop_map";

120 val sub_apply = thm "sub_apply";

121 val lift_set_empty = thm "lift_set_empty";

122 val lift_set_iff = thm "lift_set_iff";

123 val lift_set_iff2 = thm "lift_set_iff2";

124 val lift_set_mono = thm "lift_set_mono";

125 val lift_set_Un_distrib = thm "lift_set_Un_distrib";

126 val lift_set_Diff_distrib = thm "lift_set_Diff_distrib";

127 val bij_lift = thm "bij_lift";

128 val lift_SKIP = thm "lift_SKIP";

129 val lift_Join = thm "lift_Join";

130 val lift_JN = thm "lift_JN";

131 val lift_constrains = thm "lift_constrains";

132 val lift_stable = thm "lift_stable";

133 val lift_invariant = thm "lift_invariant";

134 val lift_Constrains = thm "lift_Constrains";

135 val lift_Stable = thm "lift_Stable";

136 val lift_Always = thm "lift_Always";

137 val lift_transient = thm "lift_transient";

138 val lift_ensures = thm "lift_ensures";

139 val lift_leadsTo = thm "lift_leadsTo";

140 val lift_LeadsTo = thm "lift_LeadsTo";

141 val lift_lift_guarantees_eq = thm "lift_lift_guarantees_eq";

142 val lift_guarantees_eq_lift_inv = thm "lift_guarantees_eq_lift_inv";

143 val lift_preserves_snd_I = thm "lift_preserves_snd_I";

144 val delete_map_eqE = thm "delete_map_eqE";

145 val delete_map_eqE = thm "delete_map_eqE";

146 val delete_map_neq_apply = thm "delete_map_neq_apply";

147 val vimage_o_fst_eq = thm "vimage_o_fst_eq";

148 val vimage_sub_eq_lift_set = thm "vimage_sub_eq_lift_set";

149 val mem_lift_act_iff = thm "mem_lift_act_iff";

150 val preserves_snd_lift_stable = thm "preserves_snd_lift_stable";

151 val constrains_imp_lift_constrains = thm "constrains_imp_lift_constrains";

152 val insert_map_upd_same = thm "insert_map_upd_same";

153 val insert_map_upd = thm "insert_map_upd";

154 val insert_map_eq_diff = thm "insert_map_eq_diff";

155 val lift_map_eq_diff = thm "lift_map_eq_diff";

156 val lift_transient_eq_disj = thm "lift_transient_eq_disj";

157 val lift_map_image_Times = thm "lift_map_image_Times";

158 val lift_preserves_eq = thm "lift_preserves_eq";

159 val lift_preserves_sub = thm "lift_preserves_sub";

160 val o_equiv_assoc = thm "o_equiv_assoc";

161 val o_equiv_apply = thm "o_equiv_apply";

162 val fst_o_lift_map = thm "fst_o_lift_map";

163 val snd_o_lift_map = thm "snd_o_lift_map";

164 val extend_act_extend_act = thm "extend_act_extend_act";

165 val project_act_project_act = thm "project_act_project_act";

166 val project_act_extend_act = thm "project_act_extend_act";

167 val act_in_UNION_preserves_fst = thm "act_in_UNION_preserves_fst";

168 val UNION_OK_lift_I = thm "UNION_OK_lift_I";

169 val OK_lift_I = thm "OK_lift_I";

170 val Allowed_lift = thm "Allowed_lift";

171 val lift_image_preserves = thm "lift_image_preserves";

174 (*PPROD*)

175 val Init_PLam = thm "Init_PLam";

176 val PLam_empty = thm "PLam_empty";

177 val PLam_SKIP = thm "PLam_SKIP";

178 val PLam_insert = thm "PLam_insert";

179 val PLam_component_iff = thm "PLam_component_iff";

180 val component_PLam = thm "component_PLam";

181 val PLam_constrains = thm "PLam_constrains";

182 val PLam_stable = thm "PLam_stable";

183 val PLam_transient = thm "PLam_transient";

184 val PLam_ensures = thm "PLam_ensures";

185 val PLam_leadsTo_Basis = thm "PLam_leadsTo_Basis";

186 val invariant_imp_PLam_invariant = thm "invariant_imp_PLam_invariant";

187 val PLam_preserves_fst = thm "PLam_preserves_fst";

188 val PLam_preserves_snd = thm "PLam_preserves_snd";

189 val guarantees_PLam_I = thm "guarantees_PLam_I";

190 val Allowed_PLam = thm "Allowed_PLam";

191 val PLam_preserves = thm "PLam_preserves";

194 (*proves "co" properties when the program is specified*)

195 fun gen_constrains_tac(cs,ss) i =

196 SELECT_GOAL

197 (EVERY [REPEAT (Always_Int_tac 1),

198 REPEAT (etac Always_ConstrainsI 1

199 ORELSE

200 resolve_tac [StableI, stableI,

201 constrains_imp_Constrains] 1),

202 rtac constrainsI 1,

203 full_simp_tac ss 1,

204 REPEAT (FIRSTGOAL (etac disjE)),

205 ALLGOALS (clarify_tac cs),

206 ALLGOALS (asm_lr_simp_tac ss)]) i;

208 (*proves "ensures/leadsTo" properties when the program is specified*)

209 fun gen_ensures_tac(cs,ss) sact =

210 SELECT_GOAL

211 (EVERY [REPEAT (Always_Int_tac 1),

212 etac Always_LeadsTo_Basis 1

213 ORELSE (*subgoal may involve LeadsTo, leadsTo or ensures*)

214 REPEAT (ares_tac [LeadsTo_Basis, leadsTo_Basis,

215 EnsuresI, ensuresI] 1),

216 (*now there are two subgoals: co & transient*)

217 simp_tac ss 2,

218 res_inst_tac [("act", sact)] transientI 2,

219 (*simplify the command's domain*)

220 simp_tac (ss addsimps [Domain_def]) 3,

221 gen_constrains_tac (cs,ss) 1,

222 ALLGOALS (clarify_tac cs),

223 ALLGOALS (asm_lr_simp_tac ss)]);

226 (*Composition equivalences, from Lift_prog*)

228 fun make_o_equivs th =

229 [th,

230 th RS o_equiv_assoc |> simplify (HOL_ss addsimps [o_assoc]),

231 th RS o_equiv_apply |> simplify (HOL_ss addsimps [o_def, sub_def])];

233 Addsimps (make_o_equivs fst_o_funPair @ make_o_equivs snd_o_funPair);

235 Addsimps (make_o_equivs fst_o_lift_map @ make_o_equivs snd_o_lift_map);