doc-src/CHANGES-93.txt
author blanchet
Thu, 19 Jan 2012 21:37:12 +0100
changeset 46300 6ded25a6098a
parent 103 30bd42401ab2
permissions -rw-r--r--
updated Sledge docs some more
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
     1
**** Isabelle-93 : a faster version of Isabelle-92 ****
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
     2
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
     3
Isabelle now runs faster through a combination of improvements: pattern
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
     4
unification, discrimination nets and removal of assumptions during
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
     5
simplification.  A new simplifier, although less flexible than the old one,
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
     6
runs many times faster for large subgoals.  Classical reasoning
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
     7
(e.g. fast_tac) runs up to 30% faster when large numbers of rules are
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
     8
involved.  Incompatibilities are few, and mostly concern the simplifier.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
     9
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    10
THE SPEEDUPS
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    11
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    12
The new simplifier is described in the Reference Manual, Chapter 8.  See
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    13
below for advice on converting.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    14
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    15
Pattern unification is completely invisible to users.  It efficiently
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    16
handles a common case of higher-order unification.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    17
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    18
Discrimination nets replace the old stringtrees.  They provide fast lookup
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    19
in a large set of rules for matching or unification.  New "net" tactics
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    20
replace the "compat_..." tactics based on stringtrees.  Tactics
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    21
biresolve_from_nets_tac, bimatch_from_nets_tac, resolve_from_net_tac and
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    22
match_from_net_tac take a net, rather than a list of rules, and perform
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    23
resolution or matching.  Tactics net_biresolve_tac, net_bimatch_tac
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    24
net_resolve_tac and net_match_tac take a list of rules, build a net
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    25
(internally) and perform resolution or matching.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    26
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    27
The tactical METAHYPS, which allows a subgoal's hypotheses to be taken as a
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    28
list of theorems, has been extended to handle unknowns (although not type
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    29
unknowns).  The simplification tactics now use METAHYPS to economise on
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    30
storage consumption, and to avoid problems involving "parameters" bound in
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    31
a subgoal.  The modified simplifier now requires the auto_tac to take an
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    32
extra argument: a list of theorems, which represents the assumptions of the
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    33
current subgoal.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    34
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    35
OTHER CHANGES
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    36
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    37
Apart from minor improvements in Pure Isabelle, the main other changes are
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    38
extensions to object-logics.  HOL now contains a treatment of co-induction
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    39
and co-recursion, while ZF contains a formalization of equivalence classes,
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    40
the integers and binary arithmetic.  None of this material is documented.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    41
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    42
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    43
CONVERTING FROM THE OLD TO THE NEW SIMPLIFIER (for FOL/ZF/LCF/HOL)
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    44
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    45
1.  Run a crude shell script to convert your ML-files:
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    46
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    47
	change_simp *ML
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    48
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    49
2.  Most congruence rules are no longer needed.  Hence you should remove all
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    50
calls to mk_congs and mk_typed_congs (they no longer exist) and most
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    51
occurrences of addcongs.  The only exception are congruence rules for special
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    52
constants like (in FOL)
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    53
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    54
[| ?P <-> ?P'; ?P' ==> ?Q <-> ?Q' |] ==> ?P --> ?Q = ?P' --> ?Q'
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    55
and 
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    56
[| A=A';  !!x. x:A' ==> P(x) <-> P'(x) |] ==>
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    57
(ALL x:A. P(x)) <-> (ALL x:A'. P'(x))
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    58
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    59
where some of the arguments are simplified under additional premises.  Most
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    60
likely you don't have any constructs like that, or they are already included
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    61
in the basic simpset.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    62
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    63
3.  In case you have used the addsplits facilities of the old simplifier:
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    64
The case-splitting and simplification tactics have been separated.  If you
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    65
want to interleave case-splitting with simplification, you have do so
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    66
explicitly by the following command:
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    67
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    68
ss setloop (split_tac split_thms)
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    69
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    70
where ss is a simpset and split_thms the list of case-splitting theorems.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    71
The shell script in step 1 tries to convert to from addsplits to setloop
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    72
automatically.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    73
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    74
4.  If you have used setauto, you have to change it to setsolver by hand.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    75
The solver is more delicate than the auto tactic used to be.  For details see
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    76
the full description of the new simplifier.  One very slight incompatibility
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    77
is the fact that the old auto tactic could sometimes see premises as part of
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    78
the proof state, whereas now they are always passed explicit as arguments.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    79
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    80
5.  It is quite likely that a few proofs require further hand massaging.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    81
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    82
Known incompatibilities:
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    83
- Applying a rewrite rule cannot instantiate a subgoal.  This rules out
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    84
solving a premise of a conditional rewrite rule with extra unknowns by
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    85
rewriting.  Only the solver can instantiate.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    86
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    87
Known bugs:
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    88
- The names of bound variables can be changed by the simplifier.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    89
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    90