ran isabelle update_op on all sources

more symbols via abbrevs;

setprod -> prod

HOL-Probability: more about probability, prepare for Markov processes in the AFP

--HG--
extra : rebase_source : f90e6cf5c47f7a2604d0eeacaf0181f3cfe64a14

move measure theory from HOL-Probability to HOL-Multivariate_Analysis

--HG--
rename : src/HOL/Probability/Binary_Product_Measure.thy => src/HOL/Multivariate_Analysis/Binary_Product_Measure.thy
rename : src/HOL/Probability/Bochner_Integration.thy => src/HOL/Multivariate_Analysis/Bochner_Integration.thy
rename : src/HOL/Probability/Borel_Space.thy => src/HOL/Multivariate_Analysis/Borel_Space.thy
rename : src/HOL/Probability/Caratheodory.thy => src/HOL/Multivariate_Analysis/Caratheodory.thy
rename : src/HOL/Probability/Complete_Measure.thy => src/HOL/Multivariate_Analysis/Complete_Measure.thy
rename : src/HOL/Probability/Embed_Measure.thy => src/HOL/Multivariate_Analysis/Embed_Measure.thy
rename : src/HOL/Probability/Finite_Product_Measure.thy => src/HOL/Multivariate_Analysis/Finite_Product_Measure.thy
rename : src/HOL/Probability/Interval_Integral.thy => src/HOL/Multivariate_Analysis/Interval_Integral.thy
rename : src/HOL/Probability/Lebesgue_Integral_Substitution.thy => src/HOL/Multivariate_Analysis/Lebesgue_Integral_Substitution.thy
rename : src/HOL/Probability/Lebesgue_Measure.thy => src/HOL/Multivariate_Analysis/Lebesgue_Measure.thy
rename : src/HOL/Probability/Measurable.thy => src/HOL/Multivariate_Analysis/Measurable.thy
rename : src/HOL/Probability/Measure_Space.thy => src/HOL/Multivariate_Analysis/Measure_Space.thy
rename : src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy => src/HOL/Multivariate_Analysis/Nonnegative_Lebesgue_Integration.thy
rename : src/HOL/Probability/Radon_Nikodym.thy => src/HOL/Multivariate_Analysis/Radon_Nikodym.thy
rename : src/HOL/Probability/Regularity.thy => src/HOL/Multivariate_Analysis/Regularity.thy
rename : src/HOL/Probability/Set_Integral.thy => src/HOL/Multivariate_Analysis/Set_Integral.thy
rename : src/HOL/Probability/Sigma_Algebra.thy => src/HOL/Multivariate_Analysis/Sigma_Algebra.thy
rename : src/HOL/Probability/measurable.ML => src/HOL/Multivariate_Analysis/measurable.ML
extra : rebase_source : 30ab39c42165c1c5622833cf256065cbfff030f9

tuned proofs -- avoid unstructured calculation;

Probability: move emeasure and nn_integral from ereal to ennreal

--HG--
extra : rebase_source : 5f2ac8a84abb43927a58086db8bbe10e190b2e77

more canonical names

prefer abbreviations for compound operators INFIMUM and SUPREMUM

more symbols;

isabelle update_cartouches -c -t;

Qualifiers in locale expressions default to mandatory regardless of the command.

generalize eqI theorems for product measures

--HG--
extra : rebase_source : 8ba647ae0abab594ceca74071725a61b9f84472e

cleanup projective limit of probability distributions; proved Ionescu-Tulcea; used it to prove infinite prob. distribution

--HG--
extra : rebase_source : cffce7b3e322f3c274d9117a0dfdd311d4ba66a1

tuned proofs -- less legacy;

import general theorems from AFP/Markov_Models

modernized header;

cleanup Wfrec; introduce dependent_wf/wellorder_choice

--HG--
extra : rebase_source : f2bcd9c9ab7554ffc3fe445f9603d177ca3724e7

reduced name variants for assoc and commute on plus and mult

fact consolidation

renamed positive_integral to nn_integral

--HG--
extra : rebase_source : e7a432bee0942b6330cadfd1eb5da8e326238e06

adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'

adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
* * *
more transition of 'xxx_rec' to 'rec_xxx' and same for case
* * *
compile
* * *
'rename_tac's to avoid referring to generated names
* * *
more robust scripts with 'rename_tac'
* * *
'where' -> 'of'
* * *
'where' -> 'of'
* * *
renamed 'xxx_rec' to 'rec_xxx'

renamed 'nat_{case,rec}' to '{case,rec}_nat'

renamed '{prod,sum,bool,unit}_case' to 'case_...'

tuned proofs -- clarified flow of facts wrt. calculation;

standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;

generalized lemmas in Extended_Real_Limits

eliminated slightly odd identifiers;

qualified interpretation of sigma_algebra, to avoid name clashes

--HG--
extra : rebase_source : aaeab4e40463c23ef5a5a07ee360db0335376105

merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure

--HG--
extra : rebase_source : e65af8d29763871aedf04aed10bdeb869effca0b

measurability for nat_case and comb_seq

renamed to more appropriate lim_P for projective limit

regularity of measures, therefore:
characterization of closure with infimum distance;
characterize of compact sets as totally bounded;
added Diagonal_Subsequence to Library;
introduced (enumerable) topological basis;
rational boxes as basis of ordered euclidean space;
moved some lemmas upwards

--HG--
extra : rebase_source : f535a1f0a613567ad927269eca5c0ba4e00f737b

moved lemmas into projective_family; added header for theory Projective_Family

removed redundant/unnecessary assumptions from projective_family

--HG--
extra : rebase_source : 31291167471e134480d8b83cfc14a4f96008f522

assume probability spaces; allow empty index set

--HG--
extra : rebase_source : b3d95630019975c608692231481caa8c9db431aa

added projective_family; generalized generator in product_prob_space to projective_family

--HG--
extra : rebase_source : 841ddd7f5a7409751925f93c41f6429a7160c7a4

moved lemmas further up

--HG--
extra : rebase_source : 4c6685cd2523ee2d6bc5c3519495244644f2e8cc

use measurability prover

infinite product measure is invariant under adding prefixes

infprod generator works also with empty index set

remove incseq assumption from measure_eqI_generator_eq

merge should operate on pairs

tuned product measurability

add Caratheodories theorem for semi-rings of sets

reworked Probability theory

--HG--
extra : rebase_source : 04bef352ab6c7feafcf64ecca49fecffac43bb41

prefer abs_def over def_raw;

tuned proofs -- eliminated pointless chaining of facts after 'interpret';

avoid undeclared variables in let bindings;
tuned proofs;

remove unnecessary sublocale instantiations in HOL-Probability (for clarity and speedup); remove Infinite_Product_Measure.product_prob_space which was a duplicate of Probability_Measure.product_prob_space

renamed Complete_Lattices lemmas, removed legacy names

Rename extreal => ereal

--HG--
rename : src/HOL/Library/Extended_Reals.thy => src/HOL/Library/Extended_Real.thy

rename lemma Infinite_Product_Measure.sigma_sets_subseteq, it hides Sigma_Algebra.sigma_sets_subseteq

move lemmas to Extended_Reals and Extended_Real_Limits

the measurable sets with null measure form a ring

add some lemmas for infinite product measure

prove measurable_into_infprod_algebra and measure_infprod

products of probability measures are probability measures

rename Probability_Space to Probability_Measure

--HG--
rename : src/HOL/Probability/Probability_Space.thy => src/HOL/Probability/Probability_Measure.thy

add infinite product measure