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
Hi,
> let me make a little more comments to the formalized extended reals.
>
> I’m actually reviewing the improved version of extrealTheory as part of
> [1] (the link "Required Theories”). I don’t know if there’re further
> updates, but comparing with the existing definitions shipped in HOL4, I
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
Hi,
let me make a little more comments to the formalized extended reals.
I’m actually reviewing the improved version of extrealTheory as part of [1]
(the link "Required Theories”). I don’t know if there’re further updates, but
comparing with the existing definitions shipped in HOL4, I think
Hi,
is the improved version you’re using available somewhere?
—Chun
> Il giorno 05 ago 2018, alle ore 18:09, Waqar Ahmad <12phdwah...@seecs.edu.pk>
> ha scritto:
>
> Hi Chun,
>
> I'm not sure about your potential conflict question but we are now using an
> improved definition of
Hi Thomas,
thanks for detailed explanations!
—Chun
> Il giorno 05 ago 2018, alle ore 19:58, Thomas Tuerk
> ha scritto:
>
> Hi Chun, Waqar,
>
> "Define" does indeed give priority to earlier clauses. Under the hood pattern
> compilation takes place. So what is actually is going on for
>> val
Hi Chun, Waqar,
"Define" does indeed give priority to earlier clauses. Under the hood
pattern compilation takes place. So what is actually is going on for
> val extreal_add_def = Define`
> (extreal_add (Normal x) (Normal y) = (Normal (x + y))) /\
> (extreal_add PosInf a = PosInf) /\
>
Hi Chun,
I'm not sure about your potential conflict question but we are now using an
improved definition of "extreal_add_def"
val extreal_add_def = Define`
(extreal_add (Normal x) (Normal y) = (Normal (x + y))) /\
(extreal_add (Normal _) a = a) /\
(extreal_add b (Normal _) = b) /\
Hi,the version of “extreal” (extended real numbers) in latest HOL4 has a wrong definition for sum:val _ = Hol_datatype`extreal = NegInf | PosInf | Normal of real`;val extreal_add_def = Define` (extreal_add (Normal x) (Normal y) = (Normal (x + y))) /\ (extreal_add PosInf a = PosInf) /\
