Hi Brian, w.r.t. this part of your post
> The other use is for using labeled predicates. This makes proof outlines
much more compact and understandable.
> At user command, a tactic will replace predicate labels with the text of
the predicate, having substituted actual parameters for formals.
> Here is a bit trickier because I want to substitute a predicate for a
predicate label rather than set or class variables.
we use local class definition a lot, but you can also use local wff
definition.
For example, you can take a look at the last hypothesis of
~ ioodvbdlimc1lem2
|- ( ch <-> ( ( ( ( ( ph /\ x e. RR+ )
/\ j e. ( ZZ>= ` N ) )
/\ ( abs ` ( ( S ` j ) - ( limsup ` S ) ) ) < ( x / 2 ) )
/\ z e. ( A (,) B ) ) /\ ( abs ` ( z - A ) ) < ( 1 / j ) ) )
Disclaimer: today I would write a much sorter, more readable proof of that
lemma (at the cost of more sublemmas) but I tried this "technique" as an
experiment of local definition of a wff (as you write, it "could" make
proof outlines more compact and understandable, not sure I succeeded in
this specific example).
The invoking theorem, most of the time, will simply use a biid or a bitri
and a bunch of cbv* (if disjoint vars have to be handled), in a very
similar way of local class definitions (eqid and may be cbv*)
Doing a quick search, other contributors used local definitions for wffs,
see for instance ~ bnj1189
Glauco
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/5b2fbb63-965a-4b8a-be12-ba46e8e0a238n%40googlegroups.com.
