move top-level hypotheses to the conclusion
Major Section: PROOF-CHECKER-COMMANDS
Examples: demote -- demote all top-level hypotheses (demote 3 5) -- demote hypotheses 3 and 5For example, if the top-level hypotheses are
yand the conclusion is
z, then after execution of
demote, the conclusion will be
(implies (and x y) z)and there will be no (top-level) hypotheses.
General Form: (demote &rest hyps-indices)Eliminate the indicated (top-level) hypotheses, but replace the conclusion
(implies hyps conc)where
hypsis the conjunction of the hypotheses that were eliminated. If no arguments are supplied, then all hypotheses are demoted, i.e.
demoteis the same as
(demote 1 2 ... n)where
nis the number of top-level hypotheses.
Remark: You must be at the top of the conclusion in order to use
this command. Otherwise, first invoke
demote fails if
there are no top-level hypotheses or if indices are supplied that
are out of range.