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