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