1(* ------------------------------------------------------------------------- *) 2(* Hierarchy of Tools Library *) 3(* *) 4(* Author: Joseph Chan *) 5(* Date: December, 2014 *) 6(* ------------------------------------------------------------------------- *) 7 80 helperNum -- extends HOL library on numbers. 9* divides 10* gcd 11 121 helperSet -- extends HOL library on sets. 13* pred_set 14* 0 helperNum 15 161 helperList -- extends HOL library on lists. 17* pred_set 18* list 19* rich_list 20* listRange 21* 0 helperNum 22 232 helperFunction -- useful theorems on functions. 24* 0 helperNum 25* 1 helperList 26* 1 helperSet 27 282 sublist -- order-preserving sublist and properties. 29* 0 listRange 30* 1 helperList 31 323 logPower -- properties of perfect power, power free, and upper logarithm. 33* logroot 34* 0 helperNum 35* 0 helperSet 36* 2 helperFunction 37 383 binomial -- properties of binomial coefficients in Pascal's Triangle. 39* 0 helperNum 40* 1 helperSet 41* 1 helperList 42* 2 helperFunction 43 443 Euler -- number-theoretic sets, and Euler's phi function. 45* 0 helperNum 46* 1 helperSet 47* 2 helperFunction 48 494 Gauss -- coprimes, properties of phi function, and Gauss' Little Theorem. 50* 0 helperNum 51* 1 helperSet 52* 1 helperList 53* 2 helperFunction 54* 3 Euler 55 564 primes -- properties of two-factors, and a primality test. 57* 0 helperNum 58* 2 helperFunction 59* 3 logPower 60 614 triangle -- properties of Leibniz's Denominator Triangle, relating to consecutive LCM. 62* listRange 63* relation 64* 0 helperNum 65* 1 helperSet 66* 1 helperList 67* 2 helperFunction 68* 3 binomial 69* 3 Euler 70 715 primePower -- properties of prime powers and divisors, an investigation on consecutive LCM. 72* listRange 73* option 74* 0 helperNum 75* 1 helperSet 76* 1 helperList 77* 2 helperFunction 78* 3 logPower 79* 3 Euler 80* 4 triangle 81 825 Mobius -- work on Mobius Inversion. 83* 0 helperNum 84* 1 helperSet 85* 1 helperList 86* 3 Euler 87* 4 Gauss 88