0

1 
**** Isabelle92f : a faster version of Isabelle92 ****


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 higherorder 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 objectlogics. HOL now contains a treatment of coinduction


39 
and corecursion, while ZF contains a formalization of equivalence classes,


40 
the integers and binary arithmetic. None of this material is documented.
