clasohm@0

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

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

clasohm@0

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

clasohm@0

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