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