lcp@103

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

lcp@103

2 

lcp@103

3 
Isabelle now runs faster through a combination of improvements: pattern

lcp@103

4 
unification, discrimination nets and removal of assumptions during

lcp@103

5 
simplification. A new simplifier, although less flexible than the old one,

lcp@103

6 
runs many times faster for large subgoals. Classical reasoning

lcp@103

7 
(e.g. fast_tac) runs up to 30% faster when large numbers of rules are

lcp@103

8 
involved. Incompatibilities are few, and mostly concern the simplifier.

lcp@103

9 

lcp@103

10 
THE SPEEDUPS

lcp@103

11 

lcp@103

12 
The new simplifier is described in the Reference Manual, Chapter 8. See

lcp@103

13 
below for advice on converting.

lcp@103

14 

lcp@103

15 
Pattern unification is completely invisible to users. It efficiently

lcp@103

16 
handles a common case of higherorder unification.

lcp@103

17 

lcp@103

18 
Discrimination nets replace the old stringtrees. They provide fast lookup

lcp@103

19 
in a large set of rules for matching or unification. New "net" tactics

lcp@103

20 
replace the "compat_..." tactics based on stringtrees. Tactics

lcp@103

21 
biresolve_from_nets_tac, bimatch_from_nets_tac, resolve_from_net_tac and

lcp@103

22 
match_from_net_tac take a net, rather than a list of rules, and perform

lcp@103

23 
resolution or matching. Tactics net_biresolve_tac, net_bimatch_tac

lcp@103

24 
net_resolve_tac and net_match_tac take a list of rules, build a net

lcp@103

25 
(internally) and perform resolution or matching.

lcp@103

26 

lcp@103

27 
The tactical METAHYPS, which allows a subgoal's hypotheses to be taken as a

lcp@103

28 
list of theorems, has been extended to handle unknowns (although not type

lcp@103

29 
unknowns). The simplification tactics now use METAHYPS to economise on

lcp@103

30 
storage consumption, and to avoid problems involving "parameters" bound in

lcp@103

31 
a subgoal. The modified simplifier now requires the auto_tac to take an

lcp@103

32 
extra argument: a list of theorems, which represents the assumptions of the

lcp@103

33 
current subgoal.

lcp@103

34 

lcp@103

35 
OTHER CHANGES

lcp@103

36 

lcp@103

37 
Apart from minor improvements in Pure Isabelle, the main other changes are

lcp@103

38 
extensions to objectlogics. HOL now contains a treatment of coinduction

lcp@103

39 
and corecursion, while ZF contains a formalization of equivalence classes,

lcp@103

40 
the integers and binary arithmetic. None of this material is documented.

lcp@103

41 

lcp@103

42 

lcp@103

43 
CONVERTING FROM THE OLD TO THE NEW SIMPLIFIER (for FOL/ZF/LCF/HOL)

lcp@103

44 

lcp@103

45 
1. Run a crude shell script to convert your MLfiles:

lcp@103

46 

lcp@103

47 
change_simp *ML

lcp@103

48 

lcp@103

49 
2. Most congruence rules are no longer needed. Hence you should remove all

lcp@103

50 
calls to mk_congs and mk_typed_congs (they no longer exist) and most

lcp@103

51 
occurrences of addcongs. The only exception are congruence rules for special

lcp@103

52 
constants like (in FOL)

lcp@103

53 

lcp@103

54 
[ ?P <> ?P'; ?P' ==> ?Q <> ?Q' ] ==> ?P > ?Q = ?P' > ?Q'

lcp@103

55 
and

lcp@103

56 
[ A=A'; !!x. x:A' ==> P(x) <> P'(x) ] ==>

lcp@103

57 
(ALL x:A. P(x)) <> (ALL x:A'. P'(x))

lcp@103

58 

lcp@103

59 
where some of the arguments are simplified under additional premises. Most

lcp@103

60 
likely you don't have any constructs like that, or they are already included

lcp@103

61 
in the basic simpset.

lcp@103

62 

lcp@103

63 
3. In case you have used the addsplits facilities of the old simplifier:

lcp@103

64 
The casesplitting and simplification tactics have been separated. If you

lcp@103

65 
want to interleave casesplitting with simplification, you have do so

lcp@103

66 
explicitly by the following command:

lcp@103

67 

lcp@103

68 
ss setloop (split_tac split_thms)

lcp@103

69 

lcp@103

70 
where ss is a simpset and split_thms the list of casesplitting theorems.

lcp@103

71 
The shell script in step 1 tries to convert to from addsplits to setloop

lcp@103

72 
automatically.

lcp@103

73 

lcp@103

74 
4. If you have used setauto, you have to change it to setsolver by hand.

lcp@103

75 
The solver is more delicate than the auto tactic used to be. For details see

lcp@103

76 
the full description of the new simplifier. One very slight incompatibility

lcp@103

77 
is the fact that the old auto tactic could sometimes see premises as part of

lcp@103

78 
the proof state, whereas now they are always passed explicit as arguments.

lcp@103

79 

lcp@103

80 
5. It is quite likely that a few proofs require further hand massaging.

lcp@103

81 

lcp@103

82 
Known incompatibilities:

lcp@103

83 
 Applying a rewrite rule cannot instantiate a subgoal. This rules out

lcp@103

84 
solving a premise of a conditional rewrite rule with extra unknowns by

lcp@103

85 
rewriting. Only the solver can instantiate.

lcp@103

86 

lcp@103

87 
Known bugs:

lcp@103

88 
 The names of bound variables can be changed by the simplifier.

lcp@103

89 

lcp@103

90 
