Re: [isabelle-dev] NEWS: Rename HOL-Multivariate_Analysis to HOL-Analysis and move measure theory from HOL-Probability to HOL-Analysis
On 08/08/16 17:09, Andreas Lochbihler wrote: > > Additionally, you could declare bundles > with the existing notation > > "(f has_integral x) s" > > for both of them (like is nowadays done for the Lifting package syntax). > Then, you can locally include the notation for the desired integral with > "includes", which is more flexible than a locale interpretation. It is also possible to 'unbundle' syntax bundles globally. With two bundles: foo_syntax, no_foo_syntax, it becomes possible to switch back and forth. E.g. see finfun_syntax vs. no_finfun_syntax. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: Rename HOL-Multivariate_Analysis to HOL-Analysis and move measure theory from HOL-Probability to HOL-Analysis
Hi Johannes, You could define the syntax for has_integral to be literally "(f Bochner.has_integral x) s" and similarly for the other. Additionally, you could declare bundles with the existing notation "(f has_integral x) s" for both of them (like is nowadays done for the Lifting package syntax). Then, you can locally include the notation for the desired integral with "includes", which is more flexible than a locale interpretation. Andreas On 08/08/16 16:57, Johannes Hölzl wrote: Am Montag, den 08.08.2016, 15:03 +0100 schrieb Lawrence Paulson: Thank you for making this change! My idea would be to rename both integrals into something like: has_bc_integral, bc_integrable, bc_integral, has_hk_integral, hk_integrable, hk_integral and consequently rename the integral theorems. I would greatly prefer renaming the relevant theories instead so that we have Bochner.has_integral versus Gauge.has_integral, etc. That is the point of having compound names. I would go so far as to suggest that equivalent theorems with slightly different names should be rationalised. I would prefer this too, but has_integral is not a name. It is special syntax, one writes: (f has_integral x) s Either we remove the syntax (and add it to a locale to be interpreted locally) or rename it. Unfortunately the first option is still problematic. For example, one needs to setup a context to use it, and then one is not allowed to enter a locale context. Another problem is that the theory which gets loaded later is always slightly preferred as it does not need the theory prefix. Only way to avoid this would be to hide the theorem names. Or put it in a context and add the "qualified" command prefix. Unifying the different names (i.e. integral_minus, sub, diff, uminus, cmult, mult_left, ...) is also on my TODO list. - Johannes ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: Rename HOL-Multivariate_Analysis to HOL-Analysis and move measure theory from HOL-Probability to HOL-Analysis
Am Montag, den 08.08.2016, 15:03 +0100 schrieb Lawrence Paulson: > Thank you for making this change! > > > > > My idea would be to rename both integrals into something like: > > has_bc_integral, bc_integrable, bc_integral, > > has_hk_integral, hk_integrable, hk_integral > > and consequently rename the integral theorems. > I would greatly prefer renaming the relevant theories instead so that > we have Bochner.has_integral versus Gauge.has_integral, etc. That is > the point of having compound names. I would go so far as to suggest > that equivalent theorems with slightly different names should be > rationalised. I would prefer this too, but has_integral is not a name. It is special syntax, one writes: (f has_integral x) s Either we remove the syntax (and add it to a locale to be interpreted locally) or rename it. Unfortunately the first option is still problematic. For example, one needs to setup a context to use it, and then one is not allowed to enter a locale context. Another problem is that the theory which gets loaded later is always slightly preferred as it does not need the theory prefix. Only way to avoid this would be to hide the theorem names. Or put it in a context and add the "qualified" command prefix. Unifying the different names (i.e. integral_minus, sub, diff, uminus, cmult, mult_left, ...) is also on my TODO list. - Johannes ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: Rename HOL-Multivariate_Analysis to HOL-Analysis and move measure theory from HOL-Probability to HOL-Analysis
Thank you for making this change! > My idea would be to rename both integrals into something like: > has_bc_integral, bc_integrable, bc_integral, > has_hk_integral, hk_integrable, hk_integral > and consequently rename the integral theorems. I would greatly prefer renaming the relevant theories instead so that we have Bochner.has_integral versus Gauge.has_integral, etc. That is the point of having compound names. I would go so far as to suggest that equivalent theorems with slightly different names should be rationalised. Larry ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] NEWS: Rename HOL-Multivariate_Analysis to HOL-Analysis and move measure theory from HOL-Probability to HOL-Analysis
* Renamed session HOL-Multivariate_Analysis to HOL-Analysis. * Moved measure theory from HOL-Probability to HOL-Analysis. When importing HOL-Analysis some theorems need additional name spaces prefixes due to name clashes. INCOMPATIBILITY. The incompatibility is obviously due to the renaming, but we also have currently two integrals which share now some theorem names. The problem is that one integral does not subsume the other: * The /Bochner/ integral is defined on arbitrary measures, but restricted to be absolutely integrable, i.e. when a function is integrable than also its norm is integrable. * The /Henstock-Kurzweil/ integral is restricted to Euclidean spaces (and the Lebesgue measure on it), but it is not restricted to absolutely integrable functions. My idea would be to rename both integrals into something like: has_bc_integral, bc_integrable, bc_integral, has_hk_integral, hk_integrable, hk_integral and consequently rename the integral theorems. Currently the measure theory is based on the stuff in the former Multivariate_Analysis. My plan is to integrate it further down and then replace some old stuff by more generic definitions/proofs from measure theory. There are currently further restrictions where we are not sure how to solve them: * Dominated convergence is very general on the Bochner integral it works for integrals into Banach spaces, while for the HK integral it is currently only proven for Euclidean spaces. * We require dominated convergence to prove that both integrals are equal. Hence currently equality is only proven for Euclidean spaces. * FTC for the Bochner integral is derived from FTC for the HK integral. Hence FTC for the Bochner integral is only available for Euclidean spaces. - Johannes ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
