1\DOC
2
3\TYPE {simpLib.type_ssfrag : string -> ssfrag}
4
5\SYNOPSIS Returns a simpset fragment for simplifying types' constructors.
6
7\KEYWORDS simplification, data types
8
9\DESCRIBE
10
11A call to {type_ssfrag(s)} function returns a simpset fragment that
12embodies simplification routines for the type named by the string {s}.
13The fragment includes rewrites that express injectivity and
14disjointness of constructors, and which simplify {case} expressions
15applied to terms that have constructors at the outermost level.
16
17\FAILURE
18Fails if the string argument does not correspond to a type stored in
19the {TypeBase}.
20
21\EXAMPLE
22{
23- val ss = simpLib.type_ssfrag "list";
24> val ss =
25    simpLib.SSFRAG{ac = [], congs = [], convs = [], dprocs = [],
26                   filter = NONE,
27                   rewrs =
28                     [|- (!v f. case v f [] = v) /\
29                         !v f a0 a1. case v f (a0::a1) = f a0 a1,
30                      |- !a1 a0. ~([] = a0::a1),
31                      |- !a1 a0. ~(a0::a1 = []),
32                      |- !a0 a1 a0' a1'. (a0::a1 = a0'::a1') =
33                                         (a0 = a0') /\ (a1 = a1')]}
34     : ssfrag
35
36- SIMP_CONV (bool_ss ++ ss) [] ``h::t = []``;
37<<HOL message: inventing new type variable names: 'a>>
38> val it = |- (h::t = []) = F : thm
39}
40
41\COMMENTS
42{RW_TAC} and {SRW_TAC} automatically include these simpset fragments.
43
44
45\SEEALSO
46BasicProvers.RW_TAC, BasicProvers.srw_ss, bossLib.type_rws, simpLib.SIMP_CONV, TypeBase.
47
48\ENDDOC
49