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