358 ORELSE (*subgoal may involve LeadsTo, leadsTo or ensures*) |
358 ORELSE (*subgoal may involve LeadsTo, leadsTo or ensures*) |
359 REPEAT (ares_tac [@{thm LeadsTo_Basis}, @{thm leadsTo_Basis}, |
359 REPEAT (ares_tac [@{thm LeadsTo_Basis}, @{thm leadsTo_Basis}, |
360 @{thm EnsuresI}, @{thm ensuresI}] 1), |
360 @{thm EnsuresI}, @{thm ensuresI}] 1), |
361 (*now there are two subgoals: co & transient*) |
361 (*now there are two subgoals: co & transient*) |
362 simp_tac (ss addsimps (ProgramDefs.get ctxt)) 2, |
362 simp_tac (ss addsimps (ProgramDefs.get ctxt)) 2, |
363 res_inst_tac [("act", sact)] @{thm transientI} 2, |
363 RuleInsts.res_inst_tac ctxt [(("act", 0), sact)] @{thm transientI} 2, |
364 (*simplify the command's domain*) |
364 (*simplify the command's domain*) |
365 simp_tac (ss addsimps [@{thm domain_def}]) 3, |
365 simp_tac (ss addsimps [@{thm domain_def}]) 3, |
366 (* proving the domain part *) |
366 (* proving the domain part *) |
367 clarify_tac cs 3, dtac @{thm swap} 3, force_tac css 4, |
367 clarify_tac cs 3, dtac @{thm swap} 3, force_tac css 4, |
368 rtac @{thm ReplaceI} 3, force_tac css 3, force_tac css 4, |
368 rtac @{thm ReplaceI} 3, force_tac css 3, force_tac css 4, |