352 eresolve_tac ctxt @{thms Always_LeadsTo_Basis} 1 |
352 eresolve_tac ctxt @{thms Always_LeadsTo_Basis} 1 |
353 ORELSE (*subgoal may involve LeadsTo, leadsTo or ensures*) |
353 ORELSE (*subgoal may involve LeadsTo, leadsTo or ensures*) |
354 REPEAT (ares_tac ctxt [@{thm LeadsTo_Basis}, @{thm leadsTo_Basis}, |
354 REPEAT (ares_tac ctxt [@{thm LeadsTo_Basis}, @{thm leadsTo_Basis}, |
355 @{thm EnsuresI}, @{thm ensuresI}] 1), |
355 @{thm EnsuresI}, @{thm ensuresI}] 1), |
356 (*now there are two subgoals: co & transient*) |
356 (*now there are two subgoals: co & transient*) |
357 simp_tac (ctxt addsimps (Named_Theorems.get ctxt @{named_theorems program})) 2, |
357 simp_tac (ctxt addsimps (Named_Theorems.get ctxt \<^named_theorems>\<open>program\<close>)) 2, |
358 Rule_Insts.res_inst_tac ctxt |
358 Rule_Insts.res_inst_tac ctxt |
359 [((("act", 0), Position.none), sact)] [] @{thm transientI} 2, |
359 [((("act", 0), Position.none), sact)] [] @{thm transientI} 2, |
360 (*simplify the command's domain*) |
360 (*simplify the command's domain*) |
361 simp_tac (ctxt addsimps [@{thm domain_def}]) 3, |
361 simp_tac (ctxt addsimps [@{thm domain_def}]) 3, |
362 (* proving the domain part *) |
362 (* proving the domain part *) |