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