Add AllCasePreds()

This is meant to be like AllCaseEqs(), but for the situation where
the case statement occurs at the top level.

Yong Kiam threatened he might use every_case_tac if there is no
convenient way to do this.

src/1/TypeBase.sig

@@ -65,6 +65,10 @@ sig
    val CaseEqs            : string list -> thm
    val AllCaseEqs         : unit -> thm
 
+   val CasePred           : string -> thm
+   val CasePreds          : string list -> thm
+   val AllCasePreds       : unit -> thm
+
    (* f (case x of ...) <=> (case x of ..) *)
    val case_rand_of       : hol_type -> thm
    (* f (case x of ...) <=> disjunction of possibilities *)

src/1/TypeBase.sml

@@ -235,6 +235,31 @@ fun case_rand_of ty = let
 val case_pred_disj_of = Prim_rec.prove_case_ho_elim_thm o type_info_of
 val case_pred_imp_of = Prim_rec.prove_case_ho_imp_thm o type_info_of
 
+fun CasePred' tyinfo =
+    let
+      val id = mk_abs(mk_var ("x", bool), mk_var ("x", bool))
+    in
+      {case_def = TypeBasePure.case_def_of tyinfo,
+       nchotomy = TypeBasePure.nchotomy_of tyinfo}
+      |> Prim_rec.prove_case_ho_elim_thm
+      |> Drule.ISPEC id
+      |> Conv.CONV_RULE (Conv.LHS_CONV Thm.BETA_CONV)
+    end
+
+val CasePred = CasePred' o tyi_from_name
+
+val CasePreds = Drule.LIST_CONJ o map CasePred
+fun AllCasePreds() =
+  let
+    fun foldthis(ty, tyi, acc) =
+      case Lib.total CasePred' tyi of
+          NONE => acc
+        | SOME th => if aconv (concl acc) boolSyntax.T then th
+                     else CONJ th acc
+  in
+    TypeBasePure.fold foldthis boolTheory.TRUTH (theTypeBase())
+  end
+
 (* ---------------------------------------------------------------------- *
  * Install case transformation function for parser                        *
  * ---------------------------------------------------------------------- *)