Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Porting Isabelle definition to HOL4

Email Gateway (Aug 18 2022 at 12:45):

From: n_ab@encs.concordia.ca
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

Last updated: May 03 2024 at 08:18 UTC