HOL: Reference

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, BoolconvContext, COMBIN, CONG,
      Canon_Port_Context, 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,
      EnumTypeContext, GSPEC_SIMP, InductiveDefinitionContext, LABEL_CONG,
      MOD, NORMEQ, NOT, NumConvContext, Omega, PURE, REAL_REDUCE, RMULCANON,
      RMULRELNORM, RealFieldContext, SET_SPEC, SubAndCondContext, UNWIND,
      While, arithmetic, bag, basicSize, bit, bitstring, blast, bnfFixBNF,
      bnfInitial, bnfMutual, bnfPrelims, bool, boolSimpsContext,
      canonContext, cardinalityCore, combin, cooper, cv, cv_prim, cv_rep,
      cv_type, divides, fcp, folMappingContext, folToolsContext, frac, gcd,
      hide, hol, hrat, hreal, hurdUtilsContext, ind_type, indexedLists,
      intExtension, intReduce, int_arith, integer, integer_word, iterate,
      list, list EQ, logroot, marker, mesonLibContext, normalForms,
      normalFormsContext, normalizer, num, numeral, numeral_bit, numpair,
      numposrep, one, option, ordinalBasic, pair, pairToolsContext, patricia,
      patternMatches, patternMatchesSimp, permutes, pred_set, prim_rec,
      primeFactor, quantHeuristics, quotient, rat, real, real_arith, realax,
      reduce, relation, rich_list, sat, schneiderUtilsContext, set_relation,
      sizes, sorting, string, sum, sum_num, ternaryComparisons, wellorder,
      word arith, word ground, word logic, word shift, word subtract, words
   Rewrites (with 689 anonymous rewrites) 
   Other net names/keys:
[...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