1structure BoundedRewrites :> BoundedRewrites =
2struct
3
4  open HolKernel boolSyntax Drule boolTheory
5  datatype control = UNBOUNDED | BOUNDED of int ref
6  type controlled_thm = thm * control
7
8  val ERR = mk_HOL_ERR "BoundedRewrites"
9
10  fun MK_BOUNDED th n =
11      if n<0 then raise ERR "MK_BOUNDED" "negative bound"
12      else
13    ADD_ASSUM (mk_comb(bounded_tm, mk_var(Int.toString n, bool))) th
14
15  fun DEST_BOUNDED th =
16      case HOLset.find (aconv bounded_tm o rator) (hypset th) of
17        SOME h => let
18          val arg = rand h
19        in
20          (PROVE_HYP (EQ_MP (SYM (SPEC arg BOUNDED_THM)) TRUTH) th,
21           valOf (Int.fromString (#1 (dest_var arg))))
22        end
23      | NONE => raise ERR "DEST_BOUNDED" "Theorem not bounded"
24
25  val Ntimes = MK_BOUNDED
26  val Once = C Ntimes 1
27
28  fun dest_tagged_rewrite thm = let
29    val (th, n) = DEST_BOUNDED thm
30  in
31    (th, BOUNDED (ref n))
32  end handle HOL_ERR _ => (thm, UNBOUNDED)
33
34
35end
36