The simp set supp_norm

Declares the simp set supp_norm, in a file of its own because an attribute cannot be used in the file declaring it. CslibFrontier.Tactic.SuppCases tags its lemmas and defines the tactic supp_cases that uses it.

Main definitions

• supp_norm: rewrites a membership in the support of a program or distribution into existentials over the supports of its parts and equations for its returned values.

def Parser.Attr.supp_norm : Lean.ParserDescr

The simp set supp_norm rewrites a membership in the support of a PMF, or in the possible results of an OracleComp program, built with bind, map, pure and if, into existentials over the supports of its parts and equations for its returned values. Uniform draws contribute no membership condition, and returned pairs are compared componentwise.

def Parser.Attr.supp_norm_proc : Lean.ParserDescr

Simplification procedure