equal
deleted
inserted
replaced
350 |
350 |
351 ML {* |
351 ML {* |
352 (*proves "ensures/leadsTo" properties when the program is specified*) |
352 (*proves "ensures/leadsTo" properties when the program is specified*) |
353 fun ensures_tac ctxt sact = |
353 fun ensures_tac ctxt sact = |
354 SELECT_GOAL |
354 SELECT_GOAL |
355 (EVERY [REPEAT (Always_Int_tac 1), |
355 (EVERY [REPEAT (Always_Int_tac ctxt 1), |
356 etac @{thm Always_LeadsTo_Basis} 1 |
356 etac @{thm Always_LeadsTo_Basis} 1 |
357 ORELSE (*subgoal may involve LeadsTo, leadsTo or ensures*) |
357 ORELSE (*subgoal may involve LeadsTo, leadsTo or ensures*) |
358 REPEAT (ares_tac [@{thm LeadsTo_Basis}, @{thm leadsTo_Basis}, |
358 REPEAT (ares_tac [@{thm LeadsTo_Basis}, @{thm leadsTo_Basis}, |
359 @{thm EnsuresI}, @{thm ensuresI}] 1), |
359 @{thm EnsuresI}, @{thm ensuresI}] 1), |
360 (*now there are two subgoals: co & transient*) |
360 (*now there are two subgoals: co & transient*) |