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