1(* ------------------------------------------------------------------------- *)
2(* Some miscellaneous tools for reasoning about boolean sequences.           *)
3(* ------------------------------------------------------------------------- *)
4
5structure sequenceTools :> sequenceTools =
6struct
7
8open HolKernel Parse boolLib;
9open bossLib sequenceTheory HurdUseful;
10
11infixr 0 ++ || ORELSEC ## THENC;
12infix 1 >>;
13nonfix THEN ORELSE;
14
15val op++ = op THEN;
16val op|| = op ORELSE;
17val op>> = op THEN1;
18
19(* ------------------------------------------------------------------------- *)
20(* A sequence `cases' tactic.                                                *)
21(* ------------------------------------------------------------------------- *)
22
23fun POP_ALL_THEN (tac:tactic) ([], g) = tac ([], g)
24  | POP_ALL_THEN tac (a::al, g)
25  = (POP_ASSUM MP_TAC ++ POP_ALL_THEN tac ++ (DISCH_TAC || ALL_TAC))
26    (a::al, g);
27
28fun SEQUENCE_CASES_TAC vtm =
29  MP_TAC (ISPEC vtm SCONS_SURJ)
30  ++ STRIP_TAC
31  ++ POP_ASSUM (fn th => POP_ALL_THEN (PURE_REWRITE_TAC [th]));
32
33val SEQ_CASES_TAC = Q_TAC SEQUENCE_CASES_TAC;
34
35end;
36