Attempt at a mechanism for expanding definitions in Metamath

df-at-exp.mm

$[ set.mm $]


$( TO EXPAND THE FOLLOWING TWO AXIOMS ~ cat and ~ df-at WHICH TOGETHER MAKE UP ` HAtoms ` ...

  @( Extend class notation with set of atoms on a Hilbert lattice. @)
  cat @a class HAtoms @.

  @{
    @d x y @.
    @( Define the set of atoms in a Hilbert lattice.  An atom is a nonzero
       element of a lattice such that anything less than it is zero, i.e. it is
       the smallest nonzero element of the lattice.  Definition of atom in
       [Kalmbach] p. 15.  See ~ ela and ~ elat2 for membership relations.
       (Contributed by NM, 14-Aug-2002.)  (New usage is discouraged.) @)
    df-at @a |- HAtoms = { x e. CH | 0H <oH x } @.
  @}

$)
$( ... WE PROVE TWO JUSTIFICATION THEOREMS
       (basically expansions of ` HAtoms ` with a fresh variable ` y ` ) ... $)

    $( Note that this proof was completely found by MM-PA. $)
    EXP.cat $p class { y e. CH | 0H <oH y } $=
        c0h vy cv ccv wbr vy cch crab $.

    ${ $d x y $.
    $( Note that this proof was completely found by MM-PA
       after ~ cbvrabv was given as the first step. $)
    EXP.df-at $p |- { y e. CH | 0H <oH y } = { x e. CH | 0H <oH x } $=
        c0h vy cv ccv wbr c0h vx cv ccv wbr vy vx cch vy cv vx cv c0h ccv breq2
        cbvrabv $.
    $}


$( ... THEN WE TAKE ANY THEOREM
       (like ~ atssch which proves ` |- HAtoms C_ CH ` ) ...

    @( Atoms are a subset of the Hilbert lattice.  (Contributed by NM,
       14-Aug-2002.)  (New usage is discouraged.) @)
    atssch @p |- HAtoms C_ CH @=
        cat
        c0h vx cv ccv wbr vx cch crab cch vx
        df-at
        c0h vx cv ccv wbr vx cch ssrab2 eqsstri @.

$)
$( ... AND WE DO A SYSTEMATIC SEARCH-AND-REPLACE OF THE AXIOMS BY THEIR JUSTIFICATIONS ... $)

    ${ $d x y $.
    $(
        This proof was constructed from the proof of ~ atssch ,
        by replacing ~ cat and ~ df-at by the above justification theorems.
    $)
    EXP.atssch $p |- { y e. CH | 0H <oH y } C_ CH $=
        vy EXP.cat $( was: cat $)
        c0h vx cv ccv wbr vx cch crab cch vx
        vy EXP.df-at $( was: df-at $)
        c0h vx cv ccv wbr vx cch ssrab2 eqsstri $.
    $}


$( ... AND WE HAVE AUTOMATICALLY CREATED AN EXPANDED VERSION OF THE THEOREM
       (so ~ atssch expands to ` |- { y e. CH | 0H <oH y } C_ CH ` ). $)

$( (AND IF THE THEOREM HADN'T CONTAINED ` HAtoms ` THEN IT WOULD BE UNCHANGED,
   SO ~ cat AND ~ df-at ARE A CONSERVATIVE EXTENSION.) $)