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 simpl. 5]
⊢ (∀f. list_size f [] = 0) ∧
∀f a0 a1. list_size f (a0::a1) = 1 + (f a0 + list_size f a1)
[list$list simpl. 4]
⊢ ∀a0 a1 a0' a1'. a0::a1 = a0'::a1' ⇔ a0 = a0' ∧ a1 = a1'
[list$list simpl. 3] ⊢ ∀a1 a0. a0::a1 ≠ []
[list$list simpl. 2] ⊢ ∀a1 a0. [] ≠ a0::a1
[list$list simpl. 1]
⊢ (∀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