#
949e8cdf |
|
12-Mar-2020 |
Michael Norrish <michael.norrish@data61.csiro.au> |
Fixes after removal of hurdUtils.Reverse
|
#
c4db120b |
|
19-Sep-2019 |
Chun Tian <binghe.lisp@gmail.com> |
The new HOL-Probability based on [0,+Inf]-measure theory (#735) * The new HOL-Probability based on [0,+Inf]-measure theory * Noted the new HOL-Probability in next-release notes; Added a dedicated README.md in `src/probability`.
|
#
c02e74f7 |
|
27-May-2019 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fix examples/miller for tight equality
|
#
8d83067c |
|
21-Oct-2018 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Remove TABs from examples
|
#
e6280aab |
|
20-Jul-2017 |
Chun Tian (binghe) <binghe.lisp@gmail.com> |
Migrated all prob scripts to latest probabilityTheory with two cheats left
|
#
23463a9b |
|
02-Aug-2016 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fix Miller example in light of pat_assum rename
|
#
8daabfb9 |
|
19-Jul-2012 |
Michael Norrish <michael.norrish@nicta.com.au> |
Put src/probability in build-sequence; change Miller example to cope. Changes are necessary because the HurdUseful that the Miller example depends on no longer has REVERSE in its API.
|
#
474acc2b |
|
09-Jul-2012 |
Michael Norrish <michael.norrish@nicta.com.au> |
Reorganise files under examples/miller. In particular, combine formalizeUseful, subTypeUseful and ho_proverUseful into one HurdUseful that is in its own directory. Also, put Know and Suff tactics into that library so that they don't need to be repeatedly redefined at the head of the various Script files.
|
#
42a7bdc6 |
|
09-Dec-2008 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Further progress towards getting this example to build. One problem at least caused by differences between standard and experimental kernel. I think I've robustified things so that it will work in both. Still not quite there: I'm going to consult with a standard kernel build to see if my current problem is present there too...
|
#
a9e682a9 |
|
12-Mar-2008 |
Peter Homeier <palantir@trustworthytools.com> |
Fixed example/miller (which was broken) so that it builds during ../bin/build -symlink -selftest 2
|
#
e133123f |
|
19-Jan-2007 |
Joe Hurd <joe@gilith.com> |
Ported the Miller-Rabin example to the latest snapshot version of HOL4 (although it's only been tested with the experimental kernel). I'm sure you don't wish to know, but I'm going to tell you anyway what were the main offenders in making this port so painful: * The addition of o_THM to std_ss, because o is used everywhere in my formalization of probability theory to construct sets and functions with specific properties. * When set comprehensions are expanded the bound variables get sensible names instead of variations on x. Thanks to whoever did this, but it certainly required a lot of changes to existing proofs. * My own terrible proof style at the time :-)
|
#
6821d5a8 |
|
08-Jan-2002 |
Joe Hurd <joe@gilith.com> |
This example is a verification of the Miller-Rabin probabilistic primality test incorporating version 2 of probability theory and some cute example probabilistic programs. The reason I haven't incorporated it into src/ is that it takes about 2 hours to build, and carries a lot of `baggage' from my experiments with proof tools. The most convenient way to build it is change to the examples/miller/ directory, and use the `m' bash script (it also understands `m clean' to clean the directories). If this doesn't work, or you can't do this, then there's a longer version: cd ho_prover Holmake --qof cd ../subtypes Holmake -I ../ho_prover --qof cd ../RSA Holmake --qof cd ../formalize Holmake -I ../ho_prover -I ../subtypes -I ../RSA --qof cd ../prob Holmake -I ../ho_prover -I ../subtypes -I ../RSA -I ../formalize --qof cd ../groups Holmake -I ../ho_prover -I ../subtypes -I ../RSA -I ../formalize --qof cd ../miller Holmake -I ../ho_prover -I ../subtypes -I ../RSA -I ../formalize -I ../prob -I ../groups --qof cd .. It does build RIGHT NOW, but is quite sensitive to changes in the HOL proof tools. I'll try and support it (especially if anyone uses it), but sadly it might become more trouble than it's worth.
|