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