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
==
PPDP | LOPSTR | WFLP 2018: Common Call for Participation
==
20th International Symposium on
Principles and Practice of
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:
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)) +
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
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
