Add STRIP_ALL_THEN and CHOOSE_ALL_THEN

[ordinarymath]

Add STRIP_ALL_THEN and CHOOSE_ALL_THEN

Only STRIP_ALL_THEN is exposed in the signature.

STRIP_ALL_THEN should behave like REPEAT_TCL STRIP_THM_THEN
and
CHOOSE_ALL_THEN should behave like REPEAT_TCL CHOOSE_THEN

This change is intended to speedup record construction time
where STRIP_ALL_THEN is being called via STRUCT_CASES_TAC

[mn200]

Please write a documentation file for STRIP_ALL_THEN in help/Docfiles. Use the template or other examples for formatting.

[mn200]

The dest_exist_opt function is Lib.total dest_exists.

[ordinarymath]

I've figured out why this is way slower than using MP with a induction thm + GENL.

HOL/src/1/Thm_cont.sml

Lines 104 to 133 in a902f2d

	(* -------------------------------------------------------------------------*)
	(* REVISED 22 Oct 1992 by TFM. Bugfix. *)
	(* *)
	(* The problem was, for example: *)
	(* *)
	(* th = |- ?n. ((?n. n = SUC 0) \/ F) /\ (n = 0) *)
	(* set_goal ([], "F");; *)
	(* expandf (STRIP_ASSUME_TAC th);; *)
	(* OK.. *)
	(* "F" *)
	(* [ "n = SUC 0" ] (n.b. should be n') *)
	(* [ "n = 0" ] *)
	(* *)
	(* let DISJ_CASES_THEN2 ttac1 ttac2 disth :tactic = *)
	(* let a1,a2 = dest_disj (concl disth) ? failwith `DISJ_CASES_THEN2` in *)
	(* \(asl,w). *)
	(* let gl1,prf1 = ttac1 (ASSUME a1) (asl,w) *)
	(* and gl2,prf2 = ttac2 (ASSUME a2) (asl,w) *)
	(* in *)
	(* gl1 @ gl2, *)
	(* \thl. let thl1,thl2 = chop_list (length gl1) thl in *)
	(* DISJ_CASES disth (prf1 thl1) (prf2 thl2);; *)
	(* -------------------------------------------------------------------------*)
	(*---------------------------------------------------------------------------
	foo needs to return a theorem with M as conclusion, and M as one
	of the assumptions, and all of the assumptions of th as well:
	foo th M = mk_thm(M::Thm.hyp th, M)
	---------------------------------------------------------------------------*)

This bug fix means that the thm passed through the continuation gets bigger and bigger with more hyps and resulting call of CHOOSE has to check for var_occurs for all of the hyps.