Canonical sources for HOL4 theorem-proving system. Branch develop is where “mainline development” occurs; when develop passes our regression tests, master is merged forward to catch up.
Add the theorem WF_PULL that allow one to pull something that stays unchanged in the relation when proving WF of a relation
∀P f R g R'.
(∀x. P (f x) ⇒ WF (R (f x))) ∧
(∀x y. R' x y ⇒ P (f x) ∧ f x = f y ∧ R (f x) (g x) (g y)) ⇒
WF R'
An example would be having f=FST and g=SND, and we know that the first component of the tuple remains unchanged and always satisfy P then we can pull it out as an assumption and only have to prove WF of a relation only concerning the SND component under that assumption.
WF_PULL
that allow one to pull something that stays unchanged in the relation when provingWF
of a relationAn example would be having
f=FST
andg=SND
, and we know that the first component of the tuple remains unchanged and always satisfyP
then we can pull it out as an assumption and only have to proveWF
of a relation only concerning theSND
component under that assumption.