Re: [Hol-info] Partial Function on lazy list

[Waqar Ahmad via hol-info]

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  wrote:

> The function is already ready for use with any P; the final until_thm
> looks like
>
>
>
> val until_thm =
>
>⊢ (until P [||] = [||]) ∧
>
>  (until P (h:::t) = if P h then [|h|] else h:::until P t): thm
>
>
>
> meaning that one can write things like
>
>
>
>   until (\x. x MOD 3 = 0) ll
>
>
>
> for example.  This seems like a suitably polymorphic function.
>
>
>
> To tweak it to put your example element Q into the list instead of the
> actual elements, change the core definition to also refer to Q. You will
> then need to generalise Q as well as P, and to then skolemize twice.
>
>
>
> Incidentally, Q is a bad name for an element; it looks too much like a
> name for a predicate.  You should use a name like ‘e’ instead.
>
>
>
> Michael
>
>
>
> *From: *Waqar Ahmad <12phdwah...@seecs.edu.pk>
> *Date: *Thursday, 9 August 2018 at 06:08
> *To: *"Norrish, Michael (Data61, Acton)" 
> *Cc: *hol-info 
> *Subject: *Re: [Hol-info] Partial Function on lazy list
>
>
>
> Hi,
>
>
>
> Great!. This really helps alot...:) However, I may be interested in
> defining it for [image: \forall P] so that I don't need to instantiate
> every time with a specific instance of P.  I tried this by myself but every
> time I lost in connecting my definition in llist form to its corresponding
> option theory form...:( Also, what change should be made if I change my
> definition a little
>
>
>
> val recur_llist_fn1_def = Define
>
> `recur_llist_fn1 P Q w =
>
>  if (w = [||]) then [||]
>
>   else if P (THE (LHD w)) then
>
>   THE (LHD w) ::: (recur_llist_fn1 P Q (THE (LTL w)))
>
>else Q:::(recur_llist_fn1 P Q (THE (LTL w)))`;
>
>
>
> Any suggestions or thoughts?
>
>
>
>
>
>
>
>
>
> On Mon, Aug 6, 2018 at 8:52 PM  wrote:
>
> You need to define a helper function that has as its state not only the
> llist that is being consumed but also a Boolean indicating whether or not
> to stop (because a P-satisfying element has been seen).
>
> - -
> val until0_def =
> new_specification ("until0_def", ["until0"],
>   ISPEC ``λbll. if FST bll then NONE
> else if SND bll = [||] then NONE
> else if P (THE (LHD (SND bll))) then
>   SOME ((T, THE (LTL (SND bll))), THE (LHD (SND bll)))
> else SOME ((F, THE (LTL (SND bll))), THE (LHD (SND
> bll)))``
> llist_Axiom_1 |> Q.GEN ‘P’ |> CONV_RULE (HO_REWR_CONV
> SKOLEM_THM));
>
> val until0_T =
> until0_def |> Q.SPEC `P` |> Q.SPEC ‘(T, ll)’ |> SIMP_RULE (srw_ss()) []
>
> val until0_FCONS =
>   until0_def |> Q.SPEC `P` |> Q.SPEC ‘(F, h:::t)’ |> SIMP_RULE (srw_ss())
> []
>  |> SIMP_RULE bool_ss [COND_RAND, Once COND_RATOR]
>  |> SIMP_RULE bool_ss [Once COND_RATOR]
>  |> SIMP_RULE (srw_ss()) [until0_T]
>
> val until0_FNIL =
>   until0_def |> Q.SPEC `P` |> Q.SPEC ‘(F, [||])’ |> SIMP_RULE (srw_ss()) []
>
> val until_def = Define‘until P ll = until0 P (F, ll)’
>
> val until_thm = LIST_CONJ (map (SIMP_RULE bool_ss [GSYM until_def])
>[until0_FNIL, until0_FCONS])
> - -
>
> Michael
>
>
>
> From: Waqar Ahmad via hol-info 
> Reply-To: Waqar Ahmad <12phdwah...@seecs.edu.pk>
> Date: Tuesday, 7 August 2018 at 03:26
> To: hol-info 
> Subject: [Hol-info] Partial Function on lazy list
>
> Hi all,
>
> Is there any easy way to define the following partial function on lazy list
>
> val recur_llist_fn_def = Define
> `recur_llist_fn P w =
>  if P (THE (LHD w)) then [|THE (LHD w)|]
>  else (THE (LHD w)):::(recur_llist_fn P (THE (LTL w)))`;
>
> Otherwise, I can also include the LNIL case as
>
> val recur_llist_fn_def = Define
> `recur_llist_fn P w = if (w = [||]) then [||] else
>  if P (THE (LHD w)) then [|THE (LHD w)|]
>  else (THE (LHD w)):::(recur_llist_fn P (THE (LTL w)))`;
>
> but I'm having issue to write its corresponding axiomatic form for
>
> llist_Axiom_1:
>
> !f. ?g. !x. g x = case f x of NONE => [||] | SOME (a,b) => b:::g a
>
> Particularly for  P (THE (LHD w)) what will be SOME (?)
>
> Any suggestion or thoughts?
>
> --
> 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
>
>
>
>
> --
>
> Waqar Ahmad, Ph.D.
> Post

[Hol-info] PPDP | LOPSTR | WFLP 2018 Common Call for Participation

[David Sabel]

==
 PPDP | LOPSTR | WFLP 2018: Common Call for Participation
==

   20th International Symposium on
   Principles and Practice of Declarative Programming (PPDP 2018)

   28th International Symposium on
Logic-based Program Synthesis and Transformation (LOPSTR 2018)

26th International Workshop on
Functional and Logic Programming (WFLP 2018)

 Frankfurt am Main, Germany, 3-6 September 2018

http://ppdp-lopstr-18.cs.uni-frankfurt.de
==

Program
===
 The full program of PPDP | LOPSTR | WFLP 2018 is online:

   http://ppdp-lopstr-18.cs.uni-frankfurt.de/program/0.htm

 It includes

  * four invited talks:

- Philippa Gardner, Imperial College.
Formal Methods for JavaScript
- Jorge Navas, SRI International.
Constrained Horn Clauses for Verification
- Chung-Chieh Shan, University of Indiana.
Calculating Distributions
- Laure Gonnord, University of Lyon.
Experiences in Designing Scalable Static Analyses

  * invited tutorials:

 LOPSTR includes two invited tutorials:
 - Fabio Fioravanti, University of Chieti-Pescara.
 The VeryMAP System for program transformation and verification
 - Manuel Hermenegildo, IMDEA Software Institute.
 25 Years of Ciao

  * a session in Honour of Martin Hofmann
  PPDP includes a session in honour of Martin Hofmann with an invited talk 
given by
  Nick Benton, Facebook.
  Semantic Equivalence Checking for HHVM Bytecode

Registration

 http://www.ppdp-lopstr-18.cs.uni-frankfurt.de/#registration
 Early registration ends on 15 August, 2018.

Sponsors

 The conferences are financially supported by the
 Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) - 407531063,
 and by the Goethe-University Frankfurt am Main.

Conference Organisers
=

PPDP
 Program Committee
 See http://www.ppdp-lopstr-18.cs.uni-frankfurt.de/ppdp18.html#pc
 Program Chair
 Peter Thiemann, Universität Freiburg, Germany

LOPSTR
 Program Committee
 See http://ppdp-lopstr-18.cs.uni-frankfurt.de/lopstr18.html#pc
 Program Chairs
 Fred Mesnard, University of Reunion Island, France
 Peter Stuckey, University of Melbourne, Australia

WFLP
 Program Committee
 See http://ppdp-lopstr-18.cs.uni-frankfurt.de/wflp18.html#pc
 Program Chair
Josep Silva, Universitat Politècnica de València, Spain

Organizing Committee (Goethe-University Frankfurt am Main, Germany)
Ehud Cseresnyes
Nils Dallmeyer
Bircan Dölek
Ronja Düffel
Lars Huth
Leonard Priester
David Sabel (General Chair)






--
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

Re: [Hol-info] New extrealTheory (was: Re: conflicts auto-resolved by Define?)

[Waqar Ahmad via hol-info]

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 (THEOREM)
--
|- !f s.
   FINITE s ==>
   !e.
   (!x. x IN e INSERT s ==> f x <> NegInf) \/
   (!x. x IN e INSERT s ==> f x <> PosInf) ==>
   (SIGMA f (e INSERT s) = f e + SIGMA f (s DELETE e))


extreal_hvgTheory.EXTREAL_SUM_IMAGE_PROPERTY_NEG (THEOREM)
--
|- !f s.
   FINITE s ==>
   !e.
   (!x. x IN e INSERT s ==> f x <> NegInf) ==>
   (SIGMA f (e INSERT s) = f e + SIGMA f (s DELETE e))


extreal_hvgTheory.EXTREAL_SUM_IMAGE_PROPERTY_POS (THEOREM)
--
|- !f s.
   FINITE s ==>
   !e.
   (!x. x IN e INSERT s ==> f x <> PosInf) ==>
   (SIGMA f (e INSERT s) = f e + SIGMA f (s DELETE e))

You can simply merge the latest extrealTheory (extreal_hvgTheory) with the
HOL sources and that will be it?


[1] http://hvg.ece.concordia.ca/code/hol/DFT/index.php


On Thu, Aug 9, 2018 at 5:26 PM Chun Tian (binghe) 
wrote:

> 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. SIGMA f s = ITSET (λe acc. f e + acc) s 0
>
> And I proved a general theorem EXTREAL_SUM_IMAGE_THM which captures all
> its properties (thus all remaining results should be derived from just this
> single theorem without using the original definition):
>
>[EXTREAL_SUM_IMAGE_THM]  Theorem
>
>   ⊢ ∀f.
> (SIGMA f ∅ = 0) ∧
> ∀e s.
> ((∀x. x ∈ e INSERT s ⇒ f x ≠ PosInf) ∨
>  ∀x. x ∈ e INSERT s ⇒ f x ≠ NegInf) ∧ FINITE s ⇒
> (SIGMA f (e INSERT s) = f e + SIGMA f (s DELETE e))
>
> a weaker (but practical) corollary is the following one (see the
> differences of function f):
>
>[EXTREAL_SUM_IMAGE_INSERT]  Theorem
>
>   ⊢ ∀f s.
> (∀x. f x ≠ PosInf) ∨ (∀x. f x ≠ NegInf) ⇒
> ∀e s.
> FINITE s ⇒
> (SIGMA f (e INSERT s) = f e + SIGMA f (s DELETE e))
>
> once I got EXTREAL_SUM_IMAGE_THM  almost all other SIGMA theorems either
> has trivial proofs or their existing proofs still work. But the proof of
> above theorem is not easy, I have to prove 6 lemmas first (3 for +inf, 3
> for -inf), I show the ones for +inf here:
>
> [lemma1]
> ⊢ ∀f s.
>  FINITE s ⇒
>  ∀x b.
>  (∀z. z ∈ x INSERT s ⇒ f z ≠ PosInf) ∧ b ≠ PosInf ⇒
>  (ITSET (λe acc. f e + acc) (x INSERT s) b =
>   ITSET (λe acc. f e + acc) (s DELETE x)
> ((λe acc. f e + acc) x b))
>
> [lemma2]
> ⊢ ∀f s.
>  (∀x. x ∈ s ⇒ f x ≠ PosInf) ∧ FINITE s ⇒
>  ∀b. b ≠ PosInf ⇒ ITSET (λe acc. f e + acc) s b ≠ PosInf
>
> [lemma3]
> ⊢ ∀b f x s.
>  (∀y. y ∈ x INSERT s ⇒ f y ≠ PosInf) ∧ b ≠ PosInf ∧ FINITE s ⇒
>  (ITSET (λe acc. f e + acc) (x INSERT s) b =
>   (λe acc. f e + acc) x (ITSET (λe acc. f e + acc) (s DELETE x) b))
>
> These proofs were learnt from similar proofs in pred_setTheory and digged
> into the nature of extreal. Noticed that they are all lemmas about ITSET
> (pred_setTheory), λ-function (λe acc. f e + acc), and a extreal `b`, and
> once I set `b = 0` the whole ITSET just become SIGMA for extreals.  Thus
> these proofs were done even before EXTREAL_SUM_IMAGE is defined.
>
> Then I re-used most proofs from the new version of extrealTheory, with
> almost all new theorems originally in HOL4’s version preserved (sometimes
> re-proved).
>
> The new “extrealScript.sml” can be found here [1]. Now I have a satisfied
> extended real theory and have switched to merge the new measureTheory (with
> measure type ``:‘a set -> extreal`` instead of old ``:’a set -> real``)
> into HOL4.
>
> [1]
> https://github.com/binghe/HOL/blob/HOL-Probability/src/probability/extrealScript.sml
>
> Feel free to comment, I’ll be appreciated if you could let the original
> authors know these changes.
>
> Regards,
>
> Chun
>
> Il giorno 07 ago 2018, alle ore 18:35, Waqar Ahmad <
> 12phdwah...@seecs.edu.pk> ha scritto:
>
> Hi,
>
> You're welcome to suggest improvements.. maybe step forward to put the
> extrealTheory on right footings.. I'll be more than happy, if I could be of
> any help to you at any point.
>
> On Tue, Aug 7, 2018 at 11:56 AM Chun Tian (binghe) 
> wrote:
>
>> Hi,
>>
>> I just want to see a textbook-correct theory of extended reals. Actually
>> I’m not quite sure how the improved measureTheory (of

[Hol-info] New extrealTheory (was: Re: conflicts auto-resolved by Define?)

[Chun Tian (binghe)]

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. SIGMA f s = ITSET (λe acc. f e + acc) s 0

And I proved a general theorem EXTREAL_SUM_IMAGE_THM which captures all its 
properties (thus all remaining results should be derived from just this single 
theorem without using the original definition):

   [EXTREAL_SUM_IMAGE_THM]  Theorem

  ⊢ ∀f.
(SIGMA f ∅ = 0) ∧
∀e s.
((∀x. x ∈ e INSERT s ⇒ f x ≠ PosInf) ∨
 ∀x. x ∈ e INSERT s ⇒ f x ≠ NegInf) ∧ FINITE s ⇒
(SIGMA f (e INSERT s) = f e + SIGMA f (s DELETE e))

a weaker (but practical) corollary is the following one (see the differences of 
function f):

   [EXTREAL_SUM_IMAGE_INSERT]  Theorem

  ⊢ ∀f s.
(∀x. f x ≠ PosInf) ∨ (∀x. f x ≠ NegInf) ⇒
∀e s.
FINITE s ⇒
(SIGMA f (e INSERT s) = f e + SIGMA f (s DELETE e))

once I got EXTREAL_SUM_IMAGE_THM  almost all other SIGMA theorems either has 
trivial proofs or their existing proofs still work. But the proof of above 
theorem is not easy, I have to prove 6 lemmas first (3 for +inf, 3 for -inf), I 
show the ones for +inf here:

[lemma1]
⊢ ∀f s.
 FINITE s ⇒
 ∀x b.
 (∀z. z ∈ x INSERT s ⇒ f z ≠ PosInf) ∧ b ≠ PosInf ⇒
 (ITSET (λe acc. f e + acc) (x INSERT s) b =
  ITSET (λe acc. f e + acc) (s DELETE x)
((λe acc. f e + acc) x b))

[lemma2]
⊢ ∀f s.
 (∀x. x ∈ s ⇒ f x ≠ PosInf) ∧ FINITE s ⇒
 ∀b. b ≠ PosInf ⇒ ITSET (λe acc. f e + acc) s b ≠ PosInf

[lemma3]
⊢ ∀b f x s.
 (∀y. y ∈ x INSERT s ⇒ f y ≠ PosInf) ∧ b ≠ PosInf ∧ FINITE s ⇒
 (ITSET (λe acc. f e + acc) (x INSERT s) b =
  (λe acc. f e + acc) x (ITSET (λe acc. f e + acc) (s DELETE x) b))

These proofs were learnt from similar proofs in pred_setTheory and digged into 
the nature of extreal. Noticed that they are all lemmas about ITSET 
(pred_setTheory), λ-function (λe acc. f e + acc), and a extreal `b`, and once I 
set `b = 0` the whole ITSET just become SIGMA for extreals.  Thus these proofs 
were done even before EXTREAL_SUM_IMAGE is defined.

Then I re-used most proofs from the new version of extrealTheory, with almost 
all new theorems originally in HOL4’s version preserved (sometimes re-proved).

The new “extrealScript.sml” can be found here [1]. Now I have a satisfied 
extended real theory and have switched to merge the new measureTheory (with 
measure type ``:‘a set -> extreal`` instead of old ``:’a set -> real``) into 
HOL4.

[1] 
https://github.com/binghe/HOL/blob/HOL-Probability/src/probability/extrealScript.sml

Feel free to comment, I’ll be appreciated if you could let the original authors 
know these changes.

Regards,

Chun

> Il giorno 07 ago 2018, alle ore 18:35, Waqar Ahmad <12phdwah...@seecs.edu.pk> 
> ha scritto:
> 
> Hi,
> 
> You're welcome to suggest improvements.. maybe step forward to put the 
> extrealTheory on right footings.. I'll be more than happy, if I could be of 
> any help to you at any point.
> 
> On Tue, Aug 7, 2018 at 11:56 AM Chun Tian (binghe)  > wrote:
> Hi,
> 
> I just want to see a textbook-correct theory of extended reals. Actually I’m 
> not quite sure how the improved measureTheory (of extreal) is connected with 
> the improved extrealTheory (with different definitions on +, -, inv). What I 
> observed so far is, the new measureTheory does use some new theorems from the 
> new extrealTheory, but those theorems should be also proved in the old 
> version of extrealTheory.
> 
> Of course the consequent formalization must be consistent, as long as we 
> don’t use axioms and cheats in the proof scripts.  The biggest enemy in 
> formalizations is the “wrong” definition, a correctly proved theorem based on 
> wrongly defined things would be useless. (but here it’s not that “wrong” 
> actually, because in probability measure there’s no mixing of PosInf and 
> NegInf at all; on the other side I’m not sure how the changes in 
> “extreal_inv” affects the new measureTheory.)
> 
>> Skipping the PosInf + a = PosInf requires to prove the termination of 
>> "EXTREAL_SUM_IMAGE" function as it has been done.
> 
> 
> I don’t think so. The termination of both old and new definition comes from 
> the finiteness of sets involved. A proper subset of finite set always has 
> smaller (by one) cardinality (CARD_PSUBSET), as shown in the following proof 
> scripts:
> 
> (WF_REL_TAC `measure (CARD o SND)` THEN
>METIS_TAC [CARD_PSUBSET, REST_PSUBSET])
> 
> Actually under the new definition of ``extreal_add``, we can’t prove the 
> following theorem (EXTREAL_SUM_IMAGE_THM in old version):
> 
>   ``!f. (EXTREAL_SUM_IMAGE f {} = 0) /\
>

[Hol-info] anecdote that the spec for sorting is output is sorted AND a permutation?

[Black, Paul E. (Fed)]

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 spec had to be 
that the output was in order AND that the output was a permutation of the input.

I used this anecdote as an example that merely using "formal method" (proofs) 
doesn't automatically remove all errors. (Specs have to be validated.) The 
person I was talking to asked for a reference. I have looked and looked, but 
cannot find this published anywhere.

If you have details about this, especially if it is in a book or article, 
please let me know.

I hope nobody minds me posting this on the hol-info mailing list.

-paul-
Paul E. Black
paul.bl...@nist.gov
http://hissa.nist.gov/~black/


--
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

Re: [Hol-info] New extrealTheory (was: Re: conflicts auto-resolved by Define?)

[Chun Tian (binghe)]

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)) +  EXTREAL_SUM_IMAGE f (REST (x INSERT 
s))

it’s just the original definition, if you replace all appearances of ``(x 
INSERT s)`` with t and see ``FINITE t`` easily holds.

I don’t need to repeat the same basic proof schemas for handling CHOICE and 
REST, once I finished the core proof.

This is mainly an improvement at proof engineering level. All set iteration 
operators should be defined by ITSET, I think it was abandoned because the 
original authors could resolve the issues that I saw and resolved. However, all 
existing definitions (of SUM_IMAGE) are equivalent, for people who doesn’t 
care, my changes are meaningless (except the selective merging of new “add”, 
“sub” but keeping old “inv”).

—Chun

> Il giorno 10 ago 2018, alle ore 00:20, Waqar Ahmad <12phdwah...@seecs.edu.pk> 
> ha scritto:
> 
> 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 (THEOREM)
> --
> |- !f s.
>FINITE s ==>
>!e.
>(!x. x IN e INSERT s ==> f x <> NegInf) \/
>(!x. x IN e INSERT s ==> f x <> PosInf) ==>
>(SIGMA f (e INSERT s) = f e + SIGMA f (s DELETE e))
> 
> 
> extreal_hvgTheory.EXTREAL_SUM_IMAGE_PROPERTY_NEG (THEOREM)
> --
> |- !f s.
>FINITE s ==>
>!e.
>(!x. x IN e INSERT s ==> f x <> NegInf) ==>
>(SIGMA f (e INSERT s) = f e + SIGMA f (s DELETE e))
> 
> 
> extreal_hvgTheory.EXTREAL_SUM_IMAGE_PROPERTY_POS (THEOREM)
> --
> |- !f s.
>FINITE s ==>
>!e.
>(!x. x IN e INSERT s ==> f x <> PosInf) ==>
>(SIGMA f (e INSERT s) = f e + SIGMA f (s DELETE e))
> 
> You can simply merge the latest extrealTheory (extreal_hvgTheory) with the 
> HOL sources and that will be it?
> 
> 
> [1] http://hvg.ece.concordia.ca/code/hol/DFT/index.php 
> 
> 
> 
> On Thu, Aug 9, 2018 at 5:26 PM Chun Tian (binghe)  > wrote:
> 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. SIGMA f s = ITSET (λe acc. f e + acc) s 0
> 
> And I proved a general theorem EXTREAL_SUM_IMAGE_THM which captures all its 
> properties (thus all remaining results should be derived from just this 
> single theorem without using the original definition):
> 
>[EXTREAL_SUM_IMAGE_THM]  Theorem
> 
>   ⊢ ∀f.
> (SIGMA f ∅ = 0) ∧
> ∀e s.
> ((∀x. x ∈ e INSERT s ⇒ f x ≠ PosInf) ∨
>  ∀x. x ∈ e INSERT s ⇒ f x ≠ NegInf) ∧ FINITE s ⇒
> (SIGMA f (e INSERT s) = f e + SIGMA f (s DELETE e))
> 
> a weaker (but practical) corollary is the following one (see the differences 
> of function f):
> 
>[EXTREAL_SUM_IMAGE_INSERT]  Theorem
> 
>   ⊢ ∀f s.
> (∀x. f x ≠ PosInf) ∨ (∀x. f x ≠ NegInf) ⇒
> ∀e s.
> FINITE s ⇒
> (SIGMA f (e INSERT s) = f e + SIGMA f (s DELETE e))
> 
> once I got EXTREAL_SUM_IMAGE_THM  almost all other SIGMA theorems either has 
> trivial proofs or their existing proofs still work. But the proof of above 
> theorem is not easy, I have to prove 6 lemmas first (3 for +inf, 3 for -inf), 
> I show the ones for +inf here:
> 
> [lemma1]
> ⊢ ∀f s.
>  FINITE s ⇒
>  ∀x b.
>  (∀z. z ∈ x INSERT s ⇒ f z ≠ PosInf) ∧ b ≠ PosInf ⇒
>  (ITSET (λe acc. f e + acc) (x INSERT s) b =
>   ITSET (λe acc. f e + acc) (s DELETE x)
> ((λe acc. f e + acc) x b))
> 
> [lemma2]
> ⊢ ∀f s.
>  (∀x. x ∈ s ⇒ f x ≠ PosInf) ∧ FINITE s ⇒
>  ∀b. b ≠ PosInf ⇒ ITSET (λe acc. f e + acc) s b ≠ PosInf
> 
> [lemma3]
> ⊢ ∀b f x s.
>  (∀y. y ∈ x INSERT s ⇒ f y ≠ PosInf) ∧ b ≠ PosInf ∧ FINITE s ⇒
>  (ITSET (λe acc. f e + acc) (x INSERT s) b =
>   (λe acc. f e + acc) x (ITSET (λe acc. f e + acc) (s DELETE x) b))
> 
> These proofs were learnt from similar proofs in pred_setTheory and digged 
> into the nature of extreal. Noticed that they are all lemmas about ITSET 
> (pred_setTheory), λ-function (λe acc. f