MiLkMaId: count how many inductive proofs are within the scope of PSL

[yutakang]

Use the standard library and the AFP entries as target data.

[yutakang]

Target at induct, induction, and induct_tac for three output files.
A line of an output file format is:
string, bool, int, int, int

The fist string for the location id.
The first bool tells if the induction predicate used by human engineers is within the scope of PSL.
The first int tells the order of the first mathematical induction method that coincides with eigineers' choice. (if outside the scope of PSL)
The second int tells the number of unique induction methods created by PSL.
The third int teslls the number of induction methods PSL attempted to create.