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