Hi Qasim, in this proof the induct method implicitly applies the rule "borel_measurable_induct", which does induction on the construction of Borel-measurable functions by indicator function, addition, constant multiplication, countable supremum and congruence.
This induction rule is derived from: borel_measurable_implies_simple_function_sequence which is Theorem 16 in Tareks 2010 paper. I don't know its HOL4 name. The traditional way in measure theory is to show that the integral equality for density holds for simple functions and then reduces the problem for Borel-measurable function to a sequence of simple functions. The induction rule allows us to do this in one proof. The induction rule is also described in Section 2.4.3 of my thesis: http://home.in.tum.de/~hoelzl/documents/hoelzl2012thesis.pdf - Johannes Am Freitag, den 22.05.2015, 22:13 -0400 schrieb Muhammad Qasim: > Hello Everyone, > > A theorem named nn_integral_density' in > Nonnegative_Lebesgue_Integration theory of isabelle. They used induct > to prove it. When applied induct 5 cases where returned. Does someone > know of an alternative in HOL4 ? > > I am trying to prove the same theorem in HOL4 i.e., > > `!f g M. > f IN measurable (m_space M,measurable_sets M) Borel /\ > (?x. x IN m_space M /\ 0 <= f x) /\ > g IN measurable (m_space M,measurable_sets M) Borel /\ > (!x. 0 <= g x) ==> > (pos_fn_integral > (m_space M,measurable_sets M, > (\A. > if A IN measurable_sets M then > pos_fn_integral M (\x. f x * indicator_fn A x) > else 0)) g = > pos_fn_integral M (\x. f x * g x))` > > Below is a link to the theory. > > http://isabelle.in.tum.de/dist/library/HOL/HOL-Probability/Nonnegative_Lebesgue_Integration.html > > Best Regards > > Qasim > > > ------------------------------------------------------------------------------ > One dashboard for servers and applications across Physical-Virtual-Cloud > Widest out-of-the-box monitoring support with 50+ applications > Performance metrics, stats and reports that give you Actionable Insights > Deep dive visibility with transaction tracing using APM Insight. > http://ad.doubleclick.net/ddm/clk/290420510;117567292;y > _______________________________________________ > hol-info mailing list > hol-info@lists.sourceforge.net > https://lists.sourceforge.net/lists/listinfo/hol-info ------------------------------------------------------------------------------ One dashboard for servers and applications across Physical-Virtual-Cloud Widest out-of-the-box monitoring support with 50+ applications Performance metrics, stats and reports that give you Actionable Insights Deep dive visibility with transaction tracing using APM Insight. http://ad.doubleclick.net/ddm/clk/290420510;117567292;y _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
