1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7theory Sep_Rotate 8imports Sep_Select 9begin 10 11(* We can build rotators on the basis of selectors *) 12 13ML \<open> 14(* generic rotator *) 15 16fun range lo hi = 17 let 18 fun r lo = if lo > hi then [] else lo::r (lo+1) 19 in r lo end 20 21fun rotator lens tactic ctxt i st = 22 let 23 val len = case Seq.pull ((lens THEN' resolve0_tac [@{thm iffI}]) i st) of 24 NONE => 0 25 | SOME (thm, _) => conj_length ctxt (Thm.cprem_of thm i) 26 val nums = range 1 len 27 val selector = sep_select_tactic lens 28 val tac' = map (fn x => selector [x] ctxt THEN' tactic) nums 29 in 30 (selector [1] ctxt THEN' FIRST' tac') i st 31 end 32 33fun rotator' ctxt lens tactic = rotator lens tactic ctxt 34 35fun sep_apply_tactic ctxt lens_tac thms = lens_tac THEN' eresolve_tac ctxt thms 36\<close> 37 38end 39