Hi,
Lately, I proved the equivalence of two supremum functions as:
|- !P.
(!x y. P x /\ P y ==> x <= y) /\ P <> {} ==>
(BIGSUP $<= P P = SOME (sup P)): thm
where BIGSUP is defined in [1] and "sup" can be found in HOL realTheory.
I'm not sure why the premise (!x y. P x /\ P y ==> x <= y) is required
mainly due to the fact that the binary relation $<= implicitly maintains
the partial order in a set. This can be easily proved for any set:
rest_WeakOrder_le;
val it = |- !P. rest_WeakOrder P $<=: thm
Is there any way to discharge the first premise or can be inferred from the
lemma "rest_WeakOrder_le"?
[1] (
https://github.com/HOL-Theorem-Prover/HOL/blob/master/examples/separationLogic/src/latticeScript.sml
)
latticeTheory.BIGSUP_def;
val it = |- !f D M. BIGSUP f D M = OPTION_SELECT (\s. IS_SUPREMUM f D M s):
thm
--
Waqar Ahmad, Ph.D.
Post Doc at Hardware Verification Group (HVG)
Department of Electrical and Computer Engineering
Concordia University, QC, Canada
Web: http://save.seecs.nust.edu.pk/waqar-ahmad/
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
