Structure DatatypeSimps

signature DatatypeSimps =
sig
  include Abbrev
  type tyinfo = TypeBasePure.tyinfo
  type ssfrag = simpLib.ssfrag

(*---------------------------------------------------------------------------*)
(* Generating various types of theorems from type-info.                      *)
(*                                                                           *)
(* As a running example, the datatype generated by                           *)
(* val _ = Datatype.Hol_datatype `test_ty = C1 | C2 of bool`                 *)
(* is used                                                                   *)
(*---------------------------------------------------------------------------*)

(* mk_case_cong_thm_tyinfo generate a congruence theorem for
   usage with the simplifier. Running example output:

   |- !M M' f0 f1 f0' f1'.
      (M = M') ==>
      ((M' = C1) ==> (f0 = f0')) ==>
      (!x0. (M' = C2 x0) ==> (f1 x0 = f1' x0)) ==>
      ((case M  of C1 => f0  | C2 x0 => f1  x0) =
        case M' of C1 => f0' | C2 x0 => f1' x0)
*)
val mk_case_cong_thm_tyinfo : tyinfo -> thm

(* mk_type_rewrites_tyinfo generates a list of theorems useful for
   rewriting. Running example output:

   |- !M c. (case M of C1 => c | C2 x0 => c) = c,
   |- !v f. test_ty_CASE C1 v f = v,
   |- !a v f. test_ty_CASE (C2 a) v f = f a,
   |- !a. C1 <> C2 a,
   |- !a. C2 a <> C1,
   |- !a a'. (C2 a = C2 a') <=> (a <=> a')
*)
val mk_type_rewrites_tyinfo : tyinfo -> thm list

(* mk_case_cong_thm_tyinfo generates an elimination theorem
   that fires if all inputs give the same result. 
 
   |- !M c. (case M of C1 => c | C2 x0 => c) = c  
*)
val mk_case_elim_thm_tyinfo : tyinfo -> thm

(* The functions mk_type_exists_thm_tyinfo,
   mk_type_forall_thm_tyinfo and mk_type_quant_thms_tyinfo
   generate theorems that are able perform case-splits for
   existential and universal quantification.

   |- !P. (!tt. P tt) <=> P C1 /\ !b. P (C2 b)
   |- !P. (?tt. P tt) <=> P C1 \/ ?b. P (C2 b)
*)
val mk_type_exists_thm_tyinfo : tyinfo -> thm
val mk_type_forall_thm_tyinfo : tyinfo -> thm
val mk_type_quant_thms_tyinfo : tyinfo -> thm * thm

(* mk_case_rand_thm_tyinfo, mk_case_rand_thm_tyinfo and
   mk_case_abs_thm_tyinfo provide theorems that are used for
   lifting case constants. Use carefully, since their application
   easily loops. 

   |- !M f f0 f1.
        f (case M of C1 => f0 | C2 x0 => f1 x0) =
        case M of C1 => f f0 | C2 x0 => f (f1 x0)

   |- !M x f0 f1.
        (case M of C1 => f0 | C2 x0 => f1 x0) x =
        case M of C1 => f0 x | C2 x0 => f1 x0 x

   |- !M x f0 f1.
        (\x. case M of C1 => f0 x | C2 x0 => f1 x0 x) =
        case M of C1 => (\x. f0 x) | C2 x0 => (\x. f1 x0 x)
*)

val mk_case_rand_thm_tyinfo  : tyinfo -> thm
val mk_case_rator_thm_tyinfo : tyinfo -> thm
val mk_case_abs_thm_tyinfo   : tyinfo -> thm
  
(*---------------------------------------------------------------------------*)
(* Simpsets                                                                  *)
(*---------------------------------------------------------------------------*)

(* Lifting case distinctions as high as possible *)
val lift_cases_ss : hol_type list -> ssfrag
val lift_cases_stateful_ss : unit -> ssfrag
val lift_cases_typeinfos_ss : tyinfo list -> ssfrag

(* Reverse Lifting case distinctions as high as possible *)
val unlift_cases_ss : hol_type list -> ssfrag
val unlift_cases_stateful_ss : unit -> ssfrag
val unlift_cases_typeinfos_ss : tyinfo list -> ssfrag

(* simple rewrites for types *)
val type_rewrites_ss : hol_type list -> ssfrag
val type_rewrites_stateful_ss : unit -> ssfrag
val type_rewrites_typeinfos_ss : tyinfo list -> ssfrag

(* type rewrites + congruence theorems *)
val case_cong_ss : hol_type list -> ssfrag
val case_cong_stateful_ss : unit -> ssfrag
val case_cong_typeinfos_ss : tyinfo list -> ssfrag

(* quantifier case splits *)
val expand_type_quants_typeinfos_ss : tyinfo list -> ssfrag
val expand_type_quants_ss : hol_type list -> ssfrag
val expand_type_quants_stateful_ss : unit -> ssfrag


(*---------------------------------------------------------------------------*)
(* Rules                                                                     *)
(*---------------------------------------------------------------------------*)

(* cases_to_top_RULE eliminates case-splits on the right hand side of an equational
   theorem by moving the case split to top-level, i.e. having multiple equations on
   for an input variable that got originally split on the right hand side *)
val cases_to_top_RULE : rule

end

HOL 4, Kananaskis-10