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