type_ssfrag
simpLib.type_ssfrag : hol_type -> ssfrag
Returns a simpset fragment for simplifying types' constructors.
A call to type_ssfrag ty function returns a simpset fragment that
embodies simplification routines for the type ty.
The fragment includes rewrites that express injectivity and disjointness
of constructors, and which simplify case expressions applied to terms
that have constructors at the outermost level.
Failure
Fails if the string argument does not correspond to a type stored in the
TypeBase.
Example
> val ss = simpLib.type_ssfrag “:'a list”;
val ss =
Simplification set fragment: Datatype list$list
Rewrite rules:
[list$list_size_def]
⊢ (∀f0. list_size f0 [] = 0) ∧
∀f0 a0 a1. list_size f0 (a0::a1) = 1 + (f0 a0 + list_size f0 a1)
[rich_list$CONS_11]
⊢ ∀a0 a1 a0' a1'. a0::a1 = a0'::a1' ⇔ a0 = a0' ∧ a1 = a1'
[rich_list$NOT_CONS_NIL] ⊢ ∀a1 a0. a0::a1 ≠ []
[rich_list$NOT_NIL_CONS] ⊢ ∀a1 a0. [] ≠ a0::a1
[list$list_case_def]
⊢ (∀v f. list_CASE [] v f = v) ∧
∀a0 a1 v f. list_CASE (a0::a1) v f = f a0 a1: ssfrag
> SIMP_CONV (bool_ss ++ ss) [] ``h::t = []``;
val it = ⊢ h::t = [] ⇔ F: thm
Comments
RW_TAC and SRW_TAC automatically include these simpset fragments.
See also
BasicProvers.RW_TAC,
BasicProvers.srw_ss,
bossLib.type_rws,
simpLib.SIMP_CONV, TypeBase