equal
deleted
inserted
replaced
250 |
250 |
251 (*Combines a list of invariance THEOREMS into one.*) |
251 (*Combines a list of invariance THEOREMS into one.*) |
252 val Invariant_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS Invariant_Int); |
252 val Invariant_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS Invariant_Int); |
253 |
253 |
254 |
254 |
255 (** main_def defines the main program as a set; |
|
256 cmd_defs defines the separate commands |
|
257 **) |
|
258 |
|
259 (*proves "constrains" properties when the program is specified*) |
255 (*proves "constrains" properties when the program is specified*) |
260 fun constrains_tac (main_def::cmd_defs) = |
256 val constrains_tac = |
261 SELECT_GOAL |
257 SELECT_GOAL |
262 (EVERY [REPEAT (resolve_tac [StableI, stableI, |
258 (EVERY [REPEAT (resolve_tac [StableI, stableI, |
263 constrains_imp_Constrains] 1), |
259 constrains_imp_Constrains] 1), |
264 rtac constrainsI 1, |
260 rtac constrainsI 1, |
265 full_simp_tac (simpset() addsimps [main_def]) 1, |
261 Full_simp_tac 1, |
266 REPEAT_FIRST (etac disjE), |
262 REPEAT_FIRST (etac disjE), |
267 ALLGOALS Clarify_tac, |
263 ALLGOALS Clarify_tac, |
268 ALLGOALS (asm_full_simp_tac (simpset() addsimps cmd_defs))]); |
264 ALLGOALS Asm_full_simp_tac]); |
269 |
265 |
270 |
266 |