It looks to me as if the assumption
!x y. P x /\ P y ==> x <= y
Is false for all sets with cardinality greater than 1. (If <= is over the
reals, and P encodes a set with more than one element, then one or other will
be strictly less than the other. Then, it’s easy to specialise the above with
x and y to be those two elements and have the assumption reduce to F.)
Michael
From: Waqar Ahmad via hol-info <hol-info@lists.sourceforge.net>
Reply-To: Waqar Ahmad <12phdwah...@seecs.edu.pk>
Date: Saturday, 1 September 2018 at 09:31
To: hol-info <hol-info@lists.sourceforge.net>
Subject: [Hol-info] Partial Order for Set Supremum
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
