103

1 
**** Isabelle93 : a faster version of Isabelle92 ****


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 higherorder 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 objectlogics. HOL now contains a treatment of coinduction


39 
and corecursion, 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 MLfiles:


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 casesplitting and simplification tactics have been separated. If you


65 
want to interleave casesplitting 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 casesplitting 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 
