# [isabelle] Porting Isabelle definition to HOL4

```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 \<Rightarrow> real) \<Rightarrow> ('a set set * ('a set \<Rightarrow> real)) \<Rightarrow> real set"
```inductive "sfis f M"
intros (*This uses normal forms*)
```
base: "\<lbrakk>f = (\<lambda>t. \<Sum>i\<in>(S::nat set). x i * \<chi>(A i) t);
```  \<forall>i \<in> S. A i \<in> measurable_sets M; nonnegative x; finite S;
```
\<forall>i\<in>S. \<forall>j\<in>S. i \<noteq> j \<longrightarrow> A i \<inter> A j = {}; (\<Union>i\<in>S. A i) = UNIV\<rbrakk>
```  \<Longrightarrow> (\<Sum>i\<in>S. x i * measure M (A i)) \<in> 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 "(\<Sum>i\<in>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 "(\<Sum>i\<in>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``;
<<HOL message: inventing new type variable names: 'a>>
```
```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

```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.