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-13