| #
a4784f6f |
|
09-Oct-2019 |
haftmann <none@none> |
dedicated fact collections for algebraic simplification rules potentially splitting goals
--HG--
extra : rebase_source : ebbd8d0c13409f8fb536c42910e904c24e43dbe6
|
| #
bb368494 |
|
15-Aug-2019 |
paulson <lp15@cam.ac.uk> |
new material; rotated premises of Lim_transform_eventually
|
| #
ed7a971e |
|
05-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
| #
efe4ca34 |
|
29-Dec-2018 |
nipkow <none@none> |
capitalize proper names in lemma names
|
| #
09859749 |
|
18-Nov-2018 |
haftmann <none@none> |
removed legacy input syntax
|
| #
3241d387 |
|
06-Jun-2018 |
nipkow <none@none> |
Keep filter input syntax
|
| #
e0e22efa |
|
22-May-2018 |
nipkow <none@none> |
First step to remove nonstandard "[x <- xs. P]" syntax: only input
--HG--
extra : amend_source : a2e6a2312b63a5ed1947d3302e43341c073c9f03
|
| #
b15d33eb |
|
13-Apr-2018 |
paulson <lp15@cam.ac.uk> |
Probability builds with new definitions
|
| #
0c2c1490 |
|
11-Feb-2018 |
Lars Hupel <lars.hupel@mytum.de> |
use preferred resolver according to DOI Handbook ยง3.8
|
| #
9cdb4241 |
|
22-Jan-2018 |
Lars Hupel <lars.hupel@mytum.de> |
drop redundant cong rules
--HG--
extra : amend_source : 1974f5021d7fff2ed3f5184e9469a47765225c26
|
| #
1fb195a1 |
|
22-Jan-2018 |
Lars Hupel <lars.hupel@mytum.de> |
tuned
|
| #
a7ccdf43 |
|
10-Jan-2018 |
nipkow <none@none> |
ran isabelle update_op on all sources
|
| #
1387b04b |
|
19-Dec-2017 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
| #
1d1ca5f1 |
|
08-Oct-2017 |
haftmann <none@none> |
avoid name clashes on interpretation of abstract locales
--HG--
extra : rebase_source : f524b077cafad9e920061f751ff3126d7a903434
|
| #
37bd3648 |
|
31-Aug-2017 |
eberlm <eberlm@in.tum.de> |
Connecting PMFs to infinite sums
|
| #
17bc899d |
|
18-Aug-2017 |
wenzelm <none@none> |
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
|
| #
3865ea4c |
|
26-Jun-2017 |
paulson <lp15@cam.ac.uk> |
A few renamings and several tidied-up proofs
|
| #
7f0566a2 |
|
15-Jun-2017 |
paulson <lp15@cam.ac.uk> |
Some new material. SIMPRULE STATUS for sum/prod.delta rules!
|
| #
9b35a540 |
|
04-Apr-2017 |
eberlm <eberlm@in.tum.de> |
moved material from AFP to distribution
|
| #
241de186 |
|
22-Dec-2016 |
haftmann <none@none> |
proper logical constants
|
| #
351cc2e6 |
|
17-Oct-2016 |
nipkow <none@none> |
setsum -> sum
|
| #
fad39d02 |
|
30-Sep-2016 |
hoelzl <none@none> |
HOL-Probability: more about probability, prepare for Markov processes in the AFP
--HG--
extra : rebase_source : f90e6cf5c47f7a2604d0eeacaf0181f3cfe64a14
|
| #
25d17508 |
|
30-Sep-2016 |
hoelzl <none@none> |
Probability: fix proof
|
| #
9a8c3fb3 |
|
19-Sep-2016 |
fleury <Mathias.Fleury@mpi-inf.mpg.de> |
left_distrib ~> distrib_right, right_distrib ~> distrib_left
|
| #
78a9e4a8 |
|
16-Sep-2016 |
hoelzl <none@none> |
move Henstock-Kurzweil integration after Lebesgue_Measure; replace content by abbreviation measure lborel
--HG--
extra : rebase_source : 0321297c249a436ca0371010a76a1a026dd33222
|
| #
131dfaff |
|
15-Sep-2016 |
nipkow <none@none> |
renamed listsum -> sum_list, listprod ~> prod_list
|
| #
9b9c2176 |
|
12-Aug-2016 |
wenzelm <none@none> |
more symbols;
|
| #
14001a0d |
|
22-Jul-2016 |
wenzelm <none@none> |
tuned proofs -- avoid unstructured calculation;
|
| #
48473ab7 |
|
22-Jun-2016 |
wenzelm <none@none> |
bundle lifting_syntax;
|
| #
aa5fce1c |
|
31-May-2016 |
eberlm <none@none> |
Added code generation for PMFs
|
| #
a17d0d04 |
|
17-May-2016 |
Manuel Eberl <eberlm@in.tum.de> |
Resolved name clash
|
| #
94ba250a |
|
17-May-2016 |
eberlm <none@none> |
Moved material from AFP/Randomised_Social_Choice to distribution
|
| #
1daf8189 |
|
13-May-2016 |
wenzelm <none@none> |
eliminated use of empty "assms";
|
| #
a2bc0021 |
|
25-Apr-2016 |
wenzelm <none@none> |
eliminated old 'def';
tuned comments;
|
| #
79d3be54 |
|
14-Apr-2016 |
hoelzl <none@none> |
Probability: move emeasure and nn_integral from ereal to ennreal
--HG--
extra : rebase_source : 5f2ac8a84abb43927a58086db8bbe10e190b2e77
|
| #
35f7dccd |
|
23-Feb-2016 |
nipkow <none@none> |
more canonical names
|
| #
6b18406f |
|
16-Feb-2016 |
traytel <none@none> |
make predicator a first-class bnf citizen
|
| #
5ad25152 |
|
05-Jan-2016 |
hoelzl <none@none> |
add the proof of the central limit theorem
--HG--
extra : rebase_source : 493d99e28392771c51f4102a11b90533880e289f
extra : amend_source : 3fb7b7c607104e57a2c3ba7f733dd570eb42fa3b
|
| #
97ac1d28 |
|
01-Jan-2016 |
wenzelm <none@none> |
more symbols;
|
| #
8e83c9d2 |
|
07-Dec-2015 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
| #
ef370569 |
|
11-Nov-2015 |
Andreas Lochbihler <none@none> |
add various lemmas
|
| #
3f106d8a |
|
10-Nov-2015 |
paulson <lp15@cam.ac.uk> |
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
|
| #
be9ace2b |
|
09-Nov-2015 |
wenzelm <none@none> |
qualifier is mandatory by default;
|
| #
18551fee |
|
13-Oct-2015 |
haftmann <none@none> |
prod_case as canonical name for product type eliminator
|
| #
5012105f |
|
13-Sep-2015 |
wenzelm <none@none> |
tuned proofs -- less legacy;
|
| #
946bd7aa |
|
17-Jun-2015 |
hoelzl <none@none> |
generalized geometric distribution
--HG--
extra : rebase_source : 3d6dc06bc53447664547c0ec71b81fc78ceed195
|
| #
e2fdcde9 |
|
26-Jun-2015 |
wenzelm <none@none> |
premises in 'show' are treated like 'assume';
|
| #
15f23cb8 |
|
17-Jun-2015 |
nipkow <none@none> |
renamed Multiset.set_of to the canonical set_mset
|
| #
f5d675af |
|
14-Apr-2015 |
Andreas Lochbihler <none@none> |
add various lemmas about pmfs
|
| #
3e14dd10 |
|
16-Mar-2015 |
paulson <lp15@cam.ac.uk> |
The factorial function, "fact", now has type "nat => 'a"
|
| #
9e1d6745 |
|
12-Mar-2015 |
hoelzl <none@none> |
rel_pmf on equivalence relation
--HG--
extra : rebase_source : a3bade65cbc32130e74c8bee23179d311f6a904e
|
| #
d5ddd304 |
|
10-Mar-2015 |
hoelzl <none@none> |
generalized bind_cond_pmf_cancel
--HG--
extra : rebase_source : 08d9741e0b845d8a4dca59161347836ac2bae1b0
|
| #
08ee2a04 |
|
10-Mar-2015 |
paulson <lp15@cam.ac.uk> |
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
|
| #
988c1917 |
|
10-Mar-2015 |
hoelzl <none@none> |
add set_pmf lemmas to simpset
|
| #
bc6f15e2 |
|
10-Mar-2015 |
hoelzl <none@none> |
build pmf's on bind
|
| #
55832464 |
|
19-Feb-2015 |
haftmann <none@none> |
establish unique preferred fact names
|
| #
c40d91cc |
|
11-Feb-2015 |
Andreas Lochbihler <none@none> |
rel_pmf preserves orders
|
| #
624fc391 |
|
11-Feb-2015 |
Andreas Lochbihler <none@none> |
generalise lemma
|
| #
44c356fa |
|
11-Feb-2015 |
Andreas Lochbihler <none@none> |
more lemmas
|
| #
9a1a7dfe |
|
10-Feb-2015 |
hoelzl <none@none> |
add bind_cond_pmf_cancel
--HG--
extra : amend_source : 3322aef8e4d59aedc9134764992ee218622d3262
|
| #
b6c27167 |
|
09-Feb-2015 |
Andreas Lochbihler <none@none> |
tuned proof
|
| #
926ac6a8 |
|
09-Feb-2015 |
hoelzl <none@none> |
add cond_map_pmf
|
| #
b942eab7 |
|
09-Feb-2015 |
Andreas Lochbihler <none@none> |
tune proof
|
| #
0b28dc1c |
|
09-Feb-2015 |
hoelzl <none@none> |
introduce discrete conditional probabilities, use it to simplify bnf proof of pmf
|
| #
557571a5 |
|
30-Jan-2015 |
hoelzl <none@none> |
simp rules for return_pmf
--HG--
extra : rebase_source : 6eb5d7d9399aac78051aa3091296a7b7ed6974eb
|
| #
6c7ab2bf |
|
22-Jan-2015 |
hoelzl <none@none> |
import general thms from Density_Compiler
--HG--
extra : rebase_source : 48a3b47f755d8099564008b93076eae81453a674
|
| #
80f26eb2 |
|
09-Jan-2015 |
hoelzl <none@none> |
rel_pmf OO: conversion to nat is not necessary
|
| #
3060f212 |
|
09-Jan-2015 |
Andreas Lochbihler <none@none> |
simplify construction for distribution of rel_pmf over op OO
|
| #
10cdb31d |
|
12-Dec-2014 |
hoelzl <none@none> |
rel_pmf commutes with rel_prod
--HG--
extra : rebase_source : 2e39f9c87956d087ea4a2c473d16ebb812052b50
|
| #
199fb5b2 |
|
05-Dec-2014 |
hoelzl <none@none> |
add Poisson and Binomial distribution
--HG--
extra : rebase_source : 26baade7eecfbe66d3fd85c0be65f2ef0a72fe83
|
| #
2dd36018 |
|
04-Dec-2014 |
hoelzl <none@none> |
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
--HG--
extra : rebase_source : 8c7131ba8a4f577186bc3393e7116b70e552dd7e
|
| #
a7a57d5c |
|
25-Nov-2014 |
hoelzl <none@none> |
tuned proof that pmfs are bnfs
|
| #
85002638 |
|
25-Nov-2014 |
hoelzl <none@none> |
projections of pair_pmf (by D. Traytel)
|
| #
ce7c103d |
|
23-Nov-2014 |
hoelzl <none@none> |
add congruence solver to measurability prover
--HG--
extra : rebase_source : 77341231f7d3ba19edd6c5865552541156a3dd71
|
| #
954b7f0a |
|
20-Nov-2014 |
Andreas Lochbihler <none@none> |
add lemma
|
| #
875d8a7e |
|
20-Nov-2014 |
Andreas Lochbihler <none@none> |
register pmf as BNF
|
| #
92a516b8 |
|
14-Nov-2014 |
hoelzl <none@none> |
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
|
| #
ff53cb2b |
|
13-Nov-2014 |
hoelzl <none@none> |
import general theorems from AFP/Markov_Models
|
| #
61801ce3 |
|
21-Oct-2014 |
hoelzl <none@none> |
add transfer rule for set_pmf
|
| #
e46f9abe |
|
07-Oct-2014 |
hoelzl <none@none> |
add Giry monad
--HG--
extra : rebase_source : 3ceb1c0fa2e24cb05e37856566255a7b56f80af7
|
| #
25bfd10c |
|
06-Oct-2014 |
hoelzl <none@none> |
add type for probability mass functions, i.e. discrete probability distribution
|