#
8d83067c |
|
21-Oct-2018 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Remove TABs from examples
|
#
6b4d41ff |
|
31-Jul-2017 |
Chun Tian (binghe) <binghe.lisp@gmail.com> |
Move FINITE_BIJ_COUNT_EQ to pred_setTheory to simplify FINITE_BIJ_COUNT, with miller and diningcryptos examples adjusted
|
#
9241da95 |
|
23-Jul-2017 |
Chun Tian (binghe) <binghe.lisp@gmail.com> |
[diningcryptos] Fixed loading extra_pred_setScript.sml
|
#
44dee8ca |
|
23-Jul-2017 |
Chun Tian (binghe) <binghe.lisp@gmail.com> |
Clean up of extra_pred_setScript.sml
|
#
ade7610b |
|
20-Jul-2017 |
Chun Tian (binghe) <binghe.lisp@gmail.com> |
Removed version 2 of measure & probabilityTheory
|
#
4199267b |
|
10-Jul-2017 |
Chun Tian (binghe) <binghe.lisp@gmail.com> |
Fixed remain issues in examples/miller
|
#
ae2ba344 |
|
09-Jul-2017 |
Chun Tian (binghe) <binghe.lisp@gmail.com> |
Fixed examples/miller/formalize by removing (some) duplicated definitions in latest pred_setTheory
|
#
23463a9b |
|
02-Aug-2016 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fix Miller example in light of pat_assum rename
|
#
9524847d |
|
10-Mar-2016 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Remove some duplicates of the theorem TRUTH. These are: • INFINITE_DEF and IN_LIST_TO_SET (replaced with overloadings) • IN_APP_applied and IN_ABS_applied (inadvertently generated) Also, made changes to try to avoid new definitions in listTheory accidentally having a "_DEF" suffix instead of "_def". Old naming inconsistencies still remain in listTheory (e.g. EXISTS_DEF, FIND_def and FLAT). These changes will break a few proofs but patches should be trivial (i.e. removing references to these TRUTH theorems and/ or renaming "_DEF" to "_def").
|
#
5c617c33 |
|
10-Dec-2012 |
Michael Norrish <michael.norrish@nicta.com.au> |
Correct Miller-Rabin primality test example given change to case constants. This is progress with github issue #97.
|
#
7b2db5fb |
|
30-Jul-2012 |
Tarek <tarek@Tarek-Ubuntu.(none)> |
Added extra theories to examples/miller.
|
#
effedf1e |
|
24-Jul-2012 |
Michael Norrish <michael.norrish@nicta.com.au> |
Cleanups to get miller example to build again under Moscow ML. First deleted a redundant copy of extra_pred_set, and then used PRE_INCLUDES so that some source files local to the example got used rather than those in sigobj (ultimiately from src/probability).
|
#
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.
|
#
8cb0a8de |
|
08-Mar-2011 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Fix broken proof.
|
#
345581ca |
|
17-Mar-2010 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Remove count and BIGINTER from examples/miller/formalize/extra_pred_set. These constants are now in the core src/pred_set theory.
|
#
4761143b |
|
10-Aug-2009 |
Tjark Weber <Tjark.Weber@cl.cam.ac.uk> |
Removed trailing whitespace from all .sml and .sig files. This affects over 900 files and was done using emacs's delete-trailing-whitespace function in batch mode. Building the system with Poly/ML and Moscow ML seems to work, so I'm hoping these changes don't break anything. Please complain if they do!
|
#
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.
|