399 by (dtac ball_Constrains_INT 1); |
399 by (dtac ball_Constrains_INT 1); |
400 by (asm_full_simp_tac (simpset() addsimps [Completion]) 1); |
400 by (asm_full_simp_tac (simpset() addsimps [Completion]) 1); |
401 qed "Finite_completion"; |
401 qed "Finite_completion"; |
402 |
402 |
403 |
403 |
404 (** main_def defines the main program as a set; |
|
405 cmd_defs defines the separate commands |
|
406 **) |
|
407 |
|
408 (*proves "ensures/leadsTo" properties when the program is specified*) |
404 (*proves "ensures/leadsTo" properties when the program is specified*) |
409 fun ensures_tac (main_def::cmd_defs) sact = |
405 fun ensures_tac sact = |
410 SELECT_GOAL |
406 SELECT_GOAL |
411 (EVERY [REPEAT (Invariant_Int_tac 1), |
407 (EVERY [REPEAT (Invariant_Int_tac 1), |
412 etac Invariant_LeadsTo_Basis 1 |
408 etac Invariant_LeadsTo_Basis 1 |
413 ORELSE (*subgoal may involve LeadsTo, leadsTo or ensures*) |
409 ORELSE (*subgoal may involve LeadsTo, leadsTo or ensures*) |
414 REPEAT (ares_tac [LeadsTo_Basis, ensuresI] 1), |
410 REPEAT (ares_tac [LeadsTo_Basis, ensuresI] 1), |
415 res_inst_tac [("act", sact)] transient_mem 2, |
411 res_inst_tac [("act", sact)] transient_mem 2, |
416 (*simplify the command's domain*) |
412 (*simplify the command's domain*) |
417 simp_tac (simpset() addsimps (Domain_partial_func::cmd_defs)) 3, |
413 simp_tac (simpset() addsimps [Domain_def]) 3, |
418 (*INSIST that the command belongs to the program*) |
414 constrains_tac 1, |
419 force_tac (claset(), simpset() addsimps [main_def]) 2, |
|
420 constrains_tac (main_def::cmd_defs) 1, |
|
421 rewrite_goals_tac cmd_defs, |
|
422 ALLGOALS Clarify_tac, |
415 ALLGOALS Clarify_tac, |
423 ALLGOALS Asm_full_simp_tac]); |
416 ALLGOALS Asm_full_simp_tac]); |
424 |
417 |
425 |
418 |