Hi,
Thanks!. The tip is spot on..:) Now, I'm able to define it as
val recur_llist_fn1_thm =
(recur_llist_fn1 P e [||] = [||]) [image: \wedge]
(recur_llist_fn1 P e (h:::t) =
if P h then h:::recur_llist_fn1 P e t
else e:::recur_llist_fn1 P e t)
On Wed, Aug 8, 2018 at 7:20 PM
==
PPDP | LOPSTR | WFLP 2018: Common Call for Participation
==
20th International Symposium on
Principles and Practice of Declarati
Hi,
I appreciate the changes that you are making but I'm still not sure that
why are you re-proving the existing properties that are present in the
latest version [1]. For instance, EXTREAL_SUM_IMAGE_INSERT is already
existed in [1] in different forms:
extreal_hvgTheory.EXTREAL_SUM_IMAGE_PROPERTY
Hi,
I’ve done some rework on EXTREAL_SUM_IMAGE (or SIGMA) of extrealTheory.
My general idea is: SIGMA of extreal can only be defined when there’s no mixing
of +inf and -inf in the summation. So I start with the old definition based on
ITSET:
[EXTREAL_SUM_IMAGE_def] Definition
⊢ ∀f s
Years ago I heard an anecdote that someone had been teaching a class on
verifying software. The example was proving the correctness of a sort function.
For some time, the specification (thing to prove) was that the output of sort
was in order. It was some time before it was realized that the spe
The original version of EXTREAL_SUM_IMAGE_INSERT (or the initial part of
EXTREAL_SUM_IMAGE section) is a mimic of ITSET_INSERT in pred_setTheory without
any knowledge of extreals:
|- !s. FINITE s ==>
!f x. EXTREAL_SUM_IMAGE f (x INSERT s) =
f (CHOICE (x INSERT s)) + EXTRE
