doc-src/CHANGES-93.txt
author Walther Neuper <neuper@ist.tugraz.at>
Thu, 12 Aug 2010 15:03:34 +0200
branchisac-from-Isabelle2009-2
changeset 37913 20e3616b2d9c
parent 103 30bd42401ab2
permissions -rw-r--r--
prepare reactivation of isac-update-Isa09-2
     1 **** Isabelle-93 : a faster version of Isabelle-92 ****
     2 
     3 Isabelle now runs faster through a combination of improvements: pattern
     4 unification, discrimination nets and removal of assumptions during
     5 simplification.  A new simplifier, although less flexible than the old one,
     6 runs many times faster for large subgoals.  Classical reasoning
     7 (e.g. fast_tac) runs up to 30% faster when large numbers of rules are
     8 involved.  Incompatibilities are few, and mostly concern the simplifier.
     9 
    10 THE SPEEDUPS
    11 
    12 The new simplifier is described in the Reference Manual, Chapter 8.  See
    13 below for advice on converting.
    14 
    15 Pattern unification is completely invisible to users.  It efficiently
    16 handles a common case of higher-order 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 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.
    41 
    42 
    43 CONVERTING FROM THE OLD TO THE NEW SIMPLIFIER (for FOL/ZF/LCF/HOL)
    44 
    45 1.  Run a crude shell script to convert your ML-files:
    46 
    47 	change_simp *ML
    48 
    49 2.  Most congruence rules are no longer needed.  Hence you should remove all
    50 calls to mk_congs and mk_typed_congs (they no longer exist) and most
    51 occurrences of addcongs.  The only exception are congruence rules for special
    52 constants like (in FOL)
    53 
    54 [| ?P <-> ?P'; ?P' ==> ?Q <-> ?Q' |] ==> ?P --> ?Q = ?P' --> ?Q'
    55 and 
    56 [| A=A';  !!x. x:A' ==> P(x) <-> P'(x) |] ==>
    57 (ALL x:A. P(x)) <-> (ALL x:A'. P'(x))
    58 
    59 where some of the arguments are simplified under additional premises.  Most
    60 likely you don't have any constructs like that, or they are already included
    61 in the basic simpset.
    62 
    63 3.  In case you have used the addsplits facilities of the old simplifier:
    64 The case-splitting and simplification tactics have been separated.  If you
    65 want to interleave case-splitting with simplification, you have do so
    66 explicitly by the following command:
    67 
    68 ss setloop (split_tac split_thms)
    69 
    70 where ss is a simpset and split_thms the list of case-splitting theorems.
    71 The shell script in step 1 tries to convert to from addsplits to setloop
    72 automatically.
    73 
    74 4.  If you have used setauto, you have to change it to setsolver by hand.
    75 The solver is more delicate than the auto tactic used to be.  For details see
    76 the full description of the new simplifier.  One very slight incompatibility
    77 is the fact that the old auto tactic could sometimes see premises as part of
    78 the proof state, whereas now they are always passed explicit as arguments.
    79 
    80 5.  It is quite likely that a few proofs require further hand massaging.
    81 
    82 Known incompatibilities:
    83 - Applying a rewrite rule cannot instantiate a subgoal.  This rules out
    84 solving a premise of a conditional rewrite rule with extra unknowns by
    85 rewriting.  Only the solver can instantiate.
    86 
    87 Known bugs:
    88 - The names of bound variables can be changed by the simplifier.
    89 
    90