exclude_ssfrags

simpLib.exclude_ssfrags : string list -> simpset -> simpset

Removes named simpset fragments and records the exclusion in the simpset.

A call to exclude_ssfrags fragnames simpset returns a simpset that is the same as simpset except that 1. every fragment with a name in fragnames has been removed from the simpset’s history (as with remove_ssfrags); and 2. the names in fragnames are recorded in the simpset’s excluded set, so that any subsequent attempt to add a fragment with one of those names via the ++ operator is a silent no-op.

Use force_add (or, in user-facing thm-list arguments to simplification tactics, the SF marker) to opt back in: it adds a fragment and removes its name from the excluded set in one step.

This is the function used to implement the Proof[exclude_frags = ...] attribute on theorem proofs.

Failure

Never fails (unlike remove_ssfrags, no Conv.UNCHANGED is raised when none of the names match a fragment in the simpset).

Example

> val base = simpLib.exclude_ssfrags ["ARITH"] (srw_ss());
val base =
   Included fragments (with 1 anonymous fragment [remove using name ""]):
      ABBREV, ARITH_RWTS, ASCIInumbers, BOOL, COMBIN, CONG, ConseqConv,
      Datatype bool$itself, Datatype cv$cv, Datatype example$atree,
      Datatype example$example, Datatype fcp$bit0, Datatype fcp$bit1,
      Datatype fcp$cart, Datatype foo$exp, Datatype foo$foo,
      Datatype foo$point, Datatype integer$int, Datatype list$list,
      Datatype min$bool, Datatype min$fun, Datatype num$num,
      Datatype one$one, Datatype option$option, Datatype pair$prod,
      Datatype patricia$ptree, Datatype string$char, Datatype sum$sum,
      Datatype ternaryComparisons$ordering, GSPEC_SIMP, LABEL_CONG, MOD,
      NORMEQ, NOT, Omega, PURE, REAL_REDUCE, RMULCANON, RMULRELNORM,
      SET_SPEC, UNWIND, While, arithmetic, bag, basicSize, bit, bitstring,
      blast, bool, combin, cooper, cv, cv_prim, cv_rep, cv_type, divides,
      fcp, frac, gcd, hide, hol, hrat, hreal, ind_type, indexedLists,
      intExtension, intReduce, int_arith, integer, integer_word, iterate,
      list, list EQ, logroot, marker, normalForms, normalizer, num, numeral,
      numeral_bit, numpair, numposrep, one, option, pair, patricia,
      patternMatches, patternMatchesSimp, permutes, pred_set, prim_rec,
      primeFactor, quantHeuristics, quotient, rat, real, real_arith, realax,
      reduce, relation, rich_list, sat, sizes, sorting, string, sum, sum_num,
      ternaryComparisons, word arith, word ground, word logic, word shift,
      word subtract, words
   Rewrites (with 689 anonymous rewrites) 
   Other net names/keys:
      .rewrite:ADD_0'.1, .rewrite:ADD_INV_0_EQ'.1, .rewrite:ADD_INV_0_EQ'.2,
      .rewrite:ADD_MONO_LESS_EQ.1, .rewrite:ADD_SUB'.1,
      .rewrite:COND_BOOL_CLAUSES.1, .rewrite:COND_BOOL_CLAUSES.2,
      .rewrite:COND_BOOL_CLAUSES.3, .rewrite:COND_BOOL_CLAUSES.4,
      .rewrite:EQ_MONO_ADD_EQ.1, .rewrite:EXCLUDED_MIDDLE'.1,
[...Output elided...]

> List.exists (fn n => n = "ARITH")
             (simpLib.ssfrag_names_of (base ++ numSimps.ARITH_ss));
val it = false: bool


> List.exists (fn n => n = "ARITH")
             (simpLib.ssfrag_names_of
                (simpLib.force_add base numSimps.ARITH_ss));
val it = true: bool

See also

simpLib.remove_ssfrags, simpLib.force_add, bossLib.SF