[Hol-info] Porting Isabelle definition to HOL4 From: - 2008-12-12 05:38 ```Hi, I am trying to port the following Isabelle definition to HOL4 Kananaskis 4 and need help. I am posting this message to both HOL and Isabelle mailing lists and would appreciate any help from both communities. ========================================== consts sfis:: "('a \ real) \ ('a set set * ('a set \ real)) \ real set" inductive "sfis f M" intros (*This uses normal forms*) base: "\f = (\t. \i\(S::nat set). x i * \(A i) t); \i \ S. A i \ measurable_sets M; nonnegative x; finite S; \i\S. \j\S. i \ j \ A i \ A j = {}; (\i\S. A i) = UNIV\ \ (\i\S. x i * measure M (A i)) \ sfis f M" ========================================== I have a few questions: 1) I am able to find equivalents for the measurable_sets and measure in HOL4 kananaskis-3 as follows: - measurable_sets_def; > val it = |- !a mu. measurable_sets (a,mu) = a : thm - measure_def; > val it = |- !a mu. measure (a,mu) = mu : thm - I have not been able to find these functions in Kananaskis 4. In Kananaskis 3 after loading and opening "measureTheory" I can find these definitions, however I couldn't find "measureTheory" in kananskis 4 which makes me believe that the measure theory has been renamed somehow, Am I right? 2) I am not sure how to define "(\i\S. x i * measure M (A i))" part in HOL4. Looking at this part of the definition, I understand that it is a sum of products of two functions, namely "x i" and "measure M (A i)", both return a real number. "measure M" i think returns "mu" whose type is "'a->real", and "(A i)" returns an element of set A of type "'a" and thats how I think "measure M (A i)" would returns a real. In my description I plan to use SIGMA_REAL defined as follows for "(\i\S." part - val SIGMA_REAL_defn = Hol_defn "SIGMA_REAL_defn" `SIGMA_REAL f s = ITSET (\e acc. f e + acc) s 0`; which is similar to SIGMA in pred_setTheory defined for natural numbers. Its type is: - type_of ``SIGMA_REAL``; <> > val it = ``:('a -> real) -> ('a -> bool) -> real`` : hol_type - I was wondering if I am on the right track here? 3) In the Isabelle definition the type of function sfis is sepcified as follows: sfis: ('a->real) -> (('a->bool)->bool # ('a->bool)->real) -> (real->bool) It takes two arguments a function of type ('a->real) and a pair of type (('a->bool)->bool # ('a->bool)->real), and returns a real set (real->bool). x I am not very familiar with Isabelle and having difficulty understanding how the above definition of sfis returns a real set, and how is it inductive. Naeem ```