summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

doc-src/CHANGES-93.txt

changeset 103 | 30bd42401ab2 |

--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/CHANGES-93.txt Tue Nov 09 16:47:38 1993 +0100 @@ -0,0 +1,90 @@ +**** Isabelle-93 : a faster version of Isabelle-92 **** + +Isabelle now runs faster through a combination of improvements: pattern +unification, discrimination nets and removal of assumptions during +simplification. A new simplifier, although less flexible than the old one, +runs many times faster for large subgoals. Classical reasoning +(e.g. fast_tac) runs up to 30% faster when large numbers of rules are +involved. Incompatibilities are few, and mostly concern the simplifier. + +THE SPEEDUPS + +The new simplifier is described in the Reference Manual, Chapter 8. See +below for advice on converting. + +Pattern unification is completely invisible to users. It efficiently +handles a common case of higher-order unification. + +Discrimination nets replace the old stringtrees. They provide fast lookup +in a large set of rules for matching or unification. New "net" tactics +replace the "compat_..." tactics based on stringtrees. Tactics +biresolve_from_nets_tac, bimatch_from_nets_tac, resolve_from_net_tac and +match_from_net_tac take a net, rather than a list of rules, and perform +resolution or matching. Tactics net_biresolve_tac, net_bimatch_tac +net_resolve_tac and net_match_tac take a list of rules, build a net +(internally) and perform resolution or matching. + +The tactical METAHYPS, which allows a subgoal's hypotheses to be taken as a +list of theorems, has been extended to handle unknowns (although not type +unknowns). The simplification tactics now use METAHYPS to economise on +storage consumption, and to avoid problems involving "parameters" bound in +a subgoal. The modified simplifier now requires the auto_tac to take an +extra argument: a list of theorems, which represents the assumptions of the +current subgoal. + +OTHER CHANGES + +Apart from minor improvements in Pure Isabelle, the main other changes are +extensions to object-logics. HOL now contains a treatment of co-induction +and co-recursion, while ZF contains a formalization of equivalence classes, +the integers and binary arithmetic. None of this material is documented. + + +CONVERTING FROM THE OLD TO THE NEW SIMPLIFIER (for FOL/ZF/LCF/HOL) + +1. Run a crude shell script to convert your ML-files: + + change_simp *ML + +2. Most congruence rules are no longer needed. Hence you should remove all +calls to mk_congs and mk_typed_congs (they no longer exist) and most +occurrences of addcongs. The only exception are congruence rules for special +constants like (in FOL) + +[| ?P <-> ?P'; ?P' ==> ?Q <-> ?Q' |] ==> ?P --> ?Q = ?P' --> ?Q' +and +[| A=A'; !!x. x:A' ==> P(x) <-> P'(x) |] ==> +(ALL x:A. P(x)) <-> (ALL x:A'. P'(x)) + +where some of the arguments are simplified under additional premises. Most +likely you don't have any constructs like that, or they are already included +in the basic simpset. + +3. In case you have used the addsplits facilities of the old simplifier: +The case-splitting and simplification tactics have been separated. If you +want to interleave case-splitting with simplification, you have do so +explicitly by the following command: + +ss setloop (split_tac split_thms) + +where ss is a simpset and split_thms the list of case-splitting theorems. +The shell script in step 1 tries to convert to from addsplits to setloop +automatically. + +4. If you have used setauto, you have to change it to setsolver by hand. +The solver is more delicate than the auto tactic used to be. For details see +the full description of the new simplifier. One very slight incompatibility +is the fact that the old auto tactic could sometimes see premises as part of +the proof state, whereas now they are always passed explicit as arguments. + +5. It is quite likely that a few proofs require further hand massaging. + +Known incompatibilities: +- Applying a rewrite rule cannot instantiate a subgoal. This rules out +solving a premise of a conditional rewrite rule with extra unknowns by +rewriting. Only the solver can instantiate. + +Known bugs: +- The names of bound variables can be changed by the simplifier. + +