1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/doc-src/CHANGES-93.txt	Tue Nov 09 16:47:38 1993 +0100
     1.3 @@ -0,0 +1,90 @@
     1.4 +**** Isabelle-93 : a faster version of Isabelle-92 ****
     1.5 +
     1.6 +Isabelle now runs faster through a combination of improvements: pattern
     1.7 +unification, discrimination nets and removal of assumptions during
     1.8 +simplification.  A new simplifier, although less flexible than the old one,
     1.9 +runs many times faster for large subgoals.  Classical reasoning
    1.10 +(e.g. fast_tac) runs up to 30% faster when large numbers of rules are
    1.11 +involved.  Incompatibilities are few, and mostly concern the simplifier.
    1.12 +
    1.13 +THE SPEEDUPS
    1.14 +
    1.15 +The new simplifier is described in the Reference Manual, Chapter 8.  See
    1.16 +below for advice on converting.
    1.17 +
    1.18 +Pattern unification is completely invisible to users.  It efficiently
    1.19 +handles a common case of higher-order unification.
    1.20 +
    1.21 +Discrimination nets replace the old stringtrees.  They provide fast lookup
    1.22 +in a large set of rules for matching or unification.  New "net" tactics
    1.23 +replace the "compat_..." tactics based on stringtrees.  Tactics
    1.24 +biresolve_from_nets_tac, bimatch_from_nets_tac, resolve_from_net_tac and
    1.25 +match_from_net_tac take a net, rather than a list of rules, and perform
    1.26 +resolution or matching.  Tactics net_biresolve_tac, net_bimatch_tac
    1.27 +net_resolve_tac and net_match_tac take a list of rules, build a net
    1.28 +(internally) and perform resolution or matching.
    1.29 +
    1.30 +The tactical METAHYPS, which allows a subgoal's hypotheses to be taken as a
    1.31 +list of theorems, has been extended to handle unknowns (although not type
    1.32 +unknowns).  The simplification tactics now use METAHYPS to economise on
    1.33 +storage consumption, and to avoid problems involving "parameters" bound in
    1.34 +a subgoal.  The modified simplifier now requires the auto_tac to take an
    1.35 +extra argument: a list of theorems, which represents the assumptions of the
    1.36 +current subgoal.
    1.37 +
    1.38 +OTHER CHANGES
    1.39 +
    1.40 +Apart from minor improvements in Pure Isabelle, the main other changes are
    1.41 +extensions to object-logics.  HOL now contains a treatment of co-induction
    1.42 +and co-recursion, while ZF contains a formalization of equivalence classes,
    1.43 +the integers and binary arithmetic.  None of this material is documented.
    1.44 +
    1.45 +
    1.46 +CONVERTING FROM THE OLD TO THE NEW SIMPLIFIER (for FOL/ZF/LCF/HOL)
    1.47 +
    1.48 +1.  Run a crude shell script to convert your ML-files:
    1.49 +
    1.50 +	change_simp *ML
    1.51 +
    1.52 +2.  Most congruence rules are no longer needed.  Hence you should remove all
    1.53 +calls to mk_congs and mk_typed_congs (they no longer exist) and most
    1.54 +occurrences of addcongs.  The only exception are congruence rules for special
    1.55 +constants like (in FOL)
    1.56 +
    1.57 +[| ?P <-> ?P'; ?P' ==> ?Q <-> ?Q' |] ==> ?P --> ?Q = ?P' --> ?Q'
    1.58 +and 
    1.59 +[| A=A';  !!x. x:A' ==> P(x) <-> P'(x) |] ==>
    1.60 +(ALL x:A. P(x)) <-> (ALL x:A'. P'(x))
    1.61 +
    1.62 +where some of the arguments are simplified under additional premises.  Most
    1.63 +likely you don't have any constructs like that, or they are already included
    1.64 +in the basic simpset.
    1.65 +
    1.66 +3.  In case you have used the addsplits facilities of the old simplifier:
    1.67 +The case-splitting and simplification tactics have been separated.  If you
    1.68 +want to interleave case-splitting with simplification, you have do so
    1.69 +explicitly by the following command:
    1.70 +
    1.71 +ss setloop (split_tac split_thms)
    1.72 +
    1.73 +where ss is a simpset and split_thms the list of case-splitting theorems.
    1.74 +The shell script in step 1 tries to convert to from addsplits to setloop
    1.75 +automatically.
    1.76 +
    1.77 +4.  If you have used setauto, you have to change it to setsolver by hand.
    1.78 +The solver is more delicate than the auto tactic used to be.  For details see
    1.79 +the full description of the new simplifier.  One very slight incompatibility
    1.80 +is the fact that the old auto tactic could sometimes see premises as part of
    1.81 +the proof state, whereas now they are always passed explicit as arguments.
    1.82 +
    1.83 +5.  It is quite likely that a few proofs require further hand massaging.
    1.84 +
    1.85 +Known incompatibilities:
    1.86 +- Applying a rewrite rule cannot instantiate a subgoal.  This rules out
    1.87 +solving a premise of a conditional rewrite rule with extra unknowns by
    1.88 +rewriting.  Only the solver can instantiate.
    1.89 +
    1.90 +Known bugs:
    1.91 +- The names of bound variables can be changed by the simplifier.
    1.92 +
    1.93 +