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;
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.