|
1 **** Isabelle-92f : a faster version of Isabelle-92 **** |
|
2 |
|
3 Isabelle now runs faster through a combination of improvements: pattern |
|
4 unification, discrimination nets and removal of assumptions during |
|
5 simplification. Classical reasoning (e.g. fast_tac) runs up to 30% faster |
|
6 when large numbers of rules are involved. Rewriting (e.g. SIMP_TAC) runs |
|
7 up to 3 times faster for large subgoals. |
|
8 |
|
9 The new version will not benefit everybody; unless you require greater |
|
10 speed, it may be best to stay with the existing version. The new changes |
|
11 have not been documented properly, and there are a few incompatibilities. |
|
12 |
|
13 THE SPEEDUPS |
|
14 |
|
15 Pattern unification is completely invisible to users. It efficiently |
|
16 handles a common case of higher-order unification. |
|
17 |
|
18 Discrimination nets replace the old stringtrees. They provide fast lookup |
|
19 in a large set of rules for matching or unification. New "net" tactics |
|
20 replace the "compat_..." tactics based on stringtrees. Tactics |
|
21 biresolve_from_nets_tac, bimatch_from_nets_tac, resolve_from_net_tac and |
|
22 match_from_net_tac take a net, rather than a list of rules, and perform |
|
23 resolution or matching. Tactics net_biresolve_tac, net_bimatch_tac |
|
24 net_resolve_tac and net_match_tac take a list of rules, build a net |
|
25 (internally) and perform resolution or matching. |
|
26 |
|
27 The tactical METAHYPS, which allows a subgoal's hypotheses to be taken as a |
|
28 list of theorems, has been extended to handle unknowns (although not type |
|
29 unknowns). The simplification tactics now use METAHYPS to economise on |
|
30 storage consumption, and to avoid problems involving "parameters" bound in |
|
31 a subgoal. The modified simplifier now requires the auto_tac to take an |
|
32 extra argument: a list of theorems, which represents the assumptions of the |
|
33 current subgoal. |
|
34 |
|
35 OTHER CHANGES |
|
36 |
|
37 Apart from minor improvements in Pure Isabelle, the main other changes are |
|
38 extensions to object-logics. HOL now contains a treatment of co-induction |
|
39 and co-recursion, while ZF contains a formalization of equivalence classes, |
|
40 the integers and binary arithmetic. None of this material is documented. |