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