summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

CHANGES-92f.txt

author | wenzelm |

Fri Mar 08 16:24:06 2002 +0100 (2002-03-08) | |

changeset 13049 | ce180e5b7fa0 |

parent 0 | a5a9c433f639 |

permissions | -rw-r--r-- |

tuned;

1 **** Isabelle-92f : a faster version of Isabelle-92 ****

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.

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.

13 THE SPEEDUPS

15 Pattern unification is completely invisible to users. It efficiently

16 handles a common case of higher-order unification.

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.

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.

35 OTHER CHANGES

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.