author  wenzelm 
Sat, 20 Jan 2007 14:09:23 +0100  
changeset 22138  b9cbcd8be40f 
parent 22126  420b7b102acc 
child 22151  511f7fb8469e 
permissions  rwrr 
5363  1 
Isabelle NEWS  history userrelevant changes 
2 
============================================== 

2553  3 

20807  4 
New in this Isabelle version 
17754
58a306d9f736
* Command 'find_theorems': support * wildcard in name: criterion.
wenzelm
parents:
17725
diff
changeset

5 
 
58a306d9f736
* Command 'find_theorems': support * wildcard in name: criterion.
wenzelm
parents:
17725
diff
changeset

6 

58a306d9f736
* Command 'find_theorems': support * wildcard in name: criterion.
wenzelm
parents:
17725
diff
changeset

7 
*** General *** 
58a306d9f736
* Command 'find_theorems': support * wildcard in name: criterion.
wenzelm
parents:
17725
diff
changeset

8 

17918
93e26302733e
* Theory syntax: discontinued nonIsar format and old Isar headers;
wenzelm
parents:
17890
diff
changeset

9 
* Theory syntax: the header format ``theory A = B + C:'' has been 
93e26302733e
* Theory syntax: discontinued nonIsar format and old Isar headers;
wenzelm
parents:
17890
diff
changeset

10 
discontinued in favour of ``theory A imports B C begin''. Use isatool 
93e26302733e
* Theory syntax: discontinued nonIsar format and old Isar headers;
wenzelm
parents:
17890
diff
changeset

11 
fixheaders to convert existing theory files. INCOMPATIBILITY. 
93e26302733e
* Theory syntax: discontinued nonIsar format and old Isar headers;
wenzelm
parents:
17890
diff
changeset

12 

93e26302733e
* Theory syntax: discontinued nonIsar format and old Isar headers;
wenzelm
parents:
17890
diff
changeset

13 
* Theory syntax: the old nonIsar theory file format has been 
93e26302733e
* Theory syntax: discontinued nonIsar format and old Isar headers;
wenzelm
parents:
17890
diff
changeset

14 
discontinued altogether. Note that ML proof scripts may still be used 
93e26302733e
* Theory syntax: discontinued nonIsar format and old Isar headers;
wenzelm
parents:
17890
diff
changeset

15 
with Isar theories; migration is usually quite simple with the ML 
93e26302733e
* Theory syntax: discontinued nonIsar format and old Isar headers;
wenzelm
parents:
17890
diff
changeset

16 
function use_legacy_bindings. INCOMPATIBILITY. 
93e26302733e
* Theory syntax: discontinued nonIsar format and old Isar headers;
wenzelm
parents:
17890
diff
changeset

17 

21735  18 
* Theory syntax: some popular names (e.g. "class", "fun", "help", 
19 
"if") are now keywords. INCOMPATIBILITY, use double quotes. 

19814
faa698d46686
* Theory syntax: some popular names (e.g. "class", "if") are now keywords.
wenzelm
parents:
19783
diff
changeset

20 

17981
2602be0d99ae
* Legacy goal package: reduced interface to the bare minimum required to keep existing proof scripts running.
wenzelm
parents:
17918
diff
changeset

21 
* Legacy goal package: reduced interface to the bare minimum required 
2602be0d99ae
* Legacy goal package: reduced interface to the bare minimum required to keep existing proof scripts running.
wenzelm
parents:
17918
diff
changeset

22 
to keep existing proof scripts running. Most other userlevel 
2602be0d99ae
* Legacy goal package: reduced interface to the bare minimum required to keep existing proof scripts running.
wenzelm
parents:
17918
diff
changeset

23 
functions are now part of the OldGoals structure, which is *not* open 
2602be0d99ae
* Legacy goal package: reduced interface to the bare minimum required to keep existing proof scripts running.
wenzelm
parents:
17918
diff
changeset

24 
by default (consider isatool expandshort before open OldGoals). 
2602be0d99ae
* Legacy goal package: reduced interface to the bare minimum required to keep existing proof scripts running.
wenzelm
parents:
17918
diff
changeset

25 
Removed top_sg, prin, printyp, pprint_term/typ altogether, because 
2602be0d99ae
* Legacy goal package: reduced interface to the bare minimum required to keep existing proof scripts running.
wenzelm
parents:
17918
diff
changeset

26 
these tend to cause confusion about the actual goal (!) context being 
2602be0d99ae
* Legacy goal package: reduced interface to the bare minimum required to keep existing proof scripts running.
wenzelm
parents:
17918
diff
changeset

27 
used here, which is not necessarily the same as the_context(). 
17918
93e26302733e
* Theory syntax: discontinued nonIsar format and old Isar headers;
wenzelm
parents:
17890
diff
changeset

28 

17754
58a306d9f736
* Command 'find_theorems': support * wildcard in name: criterion.
wenzelm
parents:
17725
diff
changeset

29 
* Command 'find_theorems': support "*" wildcard in "name:" criterion. 
58a306d9f736
* Command 'find_theorems': support * wildcard in name: criterion.
wenzelm
parents:
17725
diff
changeset

30 

20370  31 
* The ``prems limit'' option (cf. ProofContext.prems_limit) is now 1 
32 
by default, which means that "prems" (and also "fixed variables") are 

33 
suppressed from proof state output. Note that the ProofGeneral 

34 
settings mechanism allows to change and save options persistently, but 

35 
older versions of Isabelle will fail to start up if a negative prems 

36 
limit is imposed. 

37 

21308
73883a528b26
* Local theory targets ``context/locale/class ... begin'' followed by ``end''.
wenzelm
parents:
21265
diff
changeset

38 
* Local theory targets may be specified by nonnested blocks of 
73883a528b26
* Local theory targets ``context/locale/class ... begin'' followed by ``end''.
wenzelm
parents:
21265
diff
changeset

39 
``context/locale/class ... begin'' followed by ``end''. The body may 
73883a528b26
* Local theory targets ``context/locale/class ... begin'' followed by ``end''.
wenzelm
parents:
21265
diff
changeset

40 
contain definitions, theorems etc., including any derived mechanism 
73883a528b26
* Local theory targets ``context/locale/class ... begin'' followed by ``end''.
wenzelm
parents:
21265
diff
changeset

41 
that has been implemented on top of these primitives. This concept 
73883a528b26
* Local theory targets ``context/locale/class ... begin'' followed by ``end''.
wenzelm
parents:
21265
diff
changeset

42 
generalizes the existing ``theorem (in ...)'' towards more versatility 
73883a528b26
* Local theory targets ``context/locale/class ... begin'' followed by ``end''.
wenzelm
parents:
21265
diff
changeset

43 
and scalability. 
73883a528b26
* Local theory targets ``context/locale/class ... begin'' followed by ``end''.
wenzelm
parents:
21265
diff
changeset

44 

21960
0574f192b78a
* Proof General: proper undo of final 'end'; discontinued Isabelle/classic;
wenzelm
parents:
21896
diff
changeset

45 
* Proof General interface: proper undo of final 'end' command; 
0574f192b78a
* Proof General: proper undo of final 'end'; discontinued Isabelle/classic;
wenzelm
parents:
21896
diff
changeset

46 
discontinued Isabelle/classic mode (ML proof scripts). 
0574f192b78a
* Proof General: proper undo of final 'end'; discontinued Isabelle/classic;
wenzelm
parents:
21896
diff
changeset

47 

17754
58a306d9f736
* Command 'find_theorems': support * wildcard in name: criterion.
wenzelm
parents:
17725
diff
changeset

48 

17865  49 
*** Document preparation *** 
50 

21717  51 
* Added antiquotation @{theory name} which prints the given name, 
52 
after checking that it refers to a valid ancestor theory in the 

53 
current context. 

21339  54 

17869  55 
* Added antiquotations @{ML_type text} and @{ML_struct text} which 
56 
check the given source text as ML type/structure, printing verbatim. 

17865  57 

21717  58 
* Added antiquotation @{abbrev "c args"} which prints the abbreviation 
59 
"c args == rhs" given in the current context. (Any number of 

21735  60 
arguments may be given on the LHS.) 
21717  61 

62 

17865  63 

17779  64 
*** Pure *** 
65 

20807  66 
* class_package.ML offers a combination of axclasses and locales to 
67 
achieve Haskelllike type classes in Isabelle. See 

68 
HOL/ex/Classpackage.thy for examples. 

69 

70 
* Yet another code generator framework allows to generate executable 

71 
code for ML and Haskell (including "class"es). A short usage sketch: 

20188
8b22026445af
added notes on class_package.ML and codegen_package.ML
haftmann
parents:
20169
diff
changeset

72 

8b22026445af
added notes on class_package.ML and codegen_package.ML
haftmann
parents:
20169
diff
changeset

73 
internal compilation: 
21545  74 
code_gen <list of constants (term syntax)> (SML #) 
20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset

75 
writing SML code to a file: 
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset

76 
code_gen <list of constants (term syntax)> (SML <filename>) 
20188
8b22026445af
added notes on class_package.ML and codegen_package.ML
haftmann
parents:
20169
diff
changeset

77 
writing Haskell code to a bunch of files: 
20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset

78 
code_gen <list of constants (term syntax)> (Haskell <filename>) 
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset

79 

855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset

80 
Reasonable default setup of framework in HOL/Main. 
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset

81 

855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset

82 
See HOL/ex/Code*.thy for examples. 
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset

83 

855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset

84 
Theorem attributs for selecting and transforming function equations theorems: 
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset

85 

855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset

86 
[code fun]: select a theorem as function equation for a specific constant 
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset

87 
[code nofun]: deselect a theorem as function equation for a specific constant 
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset

88 
[code inline]: select an equation theorem for unfolding (inlining) in place 
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset

89 
[code noinline]: deselect an equation theorem for unfolding (inlining) in place 
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset

90 

855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset

91 
Userdefined serializations (target in {SML, Haskell}): 
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset

92 

855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset

93 
code_const <andlist of constants (term syntax)> 
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset

94 
{(target) <andlist of const target syntax>}+ 
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset

95 

855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset

96 
code_type <andlist of type constructors> 
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset

97 
{(target) <andlist of type target syntax>}+ 
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset

98 

855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset

99 
code_instance <andlist of instances> 
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset

100 
{(target)}+ 
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset

101 
where instance ::= <type constructor> :: <class> 
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset

102 

855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset

103 
code_class <and_list of classes> 
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset

104 
{(target) <andlist of class target syntax>}+ 
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset

105 
where class target syntax ::= <class name> {where {<classop> == <target syntax>}+}? 
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset

106 

855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset

107 
For code_instance and code_class, target SML is silently ignored. 
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset

108 

21215
7c9337a0e30a
made locale partial_order compatible with axclass order
haftmann
parents:
21209
diff
changeset

109 
See HOL theories and HOL/ex/Code*.thy for usage examples. Doc/Isar/Advanced/Codegen/ 
7c9337a0e30a
made locale partial_order compatible with axclass order
haftmann
parents:
21209
diff
changeset

110 
provides a tutorial. 
20188
8b22026445af
added notes on class_package.ML and codegen_package.ML
haftmann
parents:
20169
diff
changeset

111 

19254  112 
* Command 'no_translations' removes translation rules from theory 
113 
syntax. 

114 

19625
285771cec083
* Pure: overloaded definitions are now actually checked for acyclic dependencies;
wenzelm
parents:
19587
diff
changeset

115 
* Overloaded definitions are now actually checked for acyclic 
19714  116 
dependencies. The overloading scheme is slightly more general than 
117 
that of Haskell98, although Isabelle does not demand an exact 

118 
correspondence to type class and instance declarations. 

119 
INCOMPATIBILITY, use ``defs (unchecked overloaded)'' to admit more 

120 
exotic versions of overloading  at the discretion of the user! 

19711  121 

122 
Polymorphic constants are represented via type arguments, i.e. the 

123 
instantiation that matches an instance against the most general 

124 
declaration given in the signature. For example, with the declaration 

125 
c :: 'a => 'a => 'a, an instance c :: nat => nat => nat is represented 

126 
as c(nat). Overloading is essentially simultaneous structural 

127 
recursion over such type arguments. Incomplete specification patterns 

19714  128 
impose global constraints on all occurrences, e.g. c('a * 'a) on the 
19715  129 
LHS means that more general c('a * 'b) will be disallowed on any RHS. 
19714  130 
Command 'print_theory' outputs the normalized system of recursive 
131 
equations, see section "definitions". 

19625
285771cec083
* Pure: overloaded definitions are now actually checked for acyclic dependencies;
wenzelm
parents:
19587
diff
changeset

132 

17865  133 
* Isar: improper proof element 'guess' is like 'obtain', but derives 
134 
the obtained context from the course of reasoning! For example: 

135 

136 
assume "EX x y. A x & B y"  "any previous fact" 

137 
then guess x and y by clarify 

138 

139 
This technique is potentially adventurous, depending on the facts and 

140 
proof tools being involved here. 

141 

18020  142 
* Isar: known facts from the proof context may be specified as literal 
143 
propositions, using ASCII backquote syntax. This works wherever 

144 
named facts used to be allowed so far, in proof commands, proof 

145 
methods, attributes etc. Literal facts are retrieved from the context 

146 
according to unification of type and term parameters. For example, 

147 
provided that "A" and "A ==> B" and "!!x. P x ==> Q x" are known 

148 
theorems in the current context, then these are valid literal facts: 

149 
`A` and `A ==> B` and `!!x. P x ==> Q x" as well as `P a ==> Q a` etc. 

150 

151 
There is also a proof method "fact" which does the same composition 

18044  152 
for explicit goal states, e.g. the following proof texts coincide with 
153 
certain special cases of literal facts: 

18020  154 

155 
have "A" by fact == note `A` 

156 
have "A ==> B" by fact == note `A ==> B` 

157 
have "!!x. P x ==> Q x" by fact == note `!!x. P x ==> Q x` 

158 
have "P a ==> Q a" by fact == note `P a ==> Q a` 

159 

20118
0c1ec587a5a8
* Isar: ":" (colon) is no longer a symbolic identifier character;
wenzelm
parents:
20090
diff
changeset

160 
* Isar: ":" (colon) is no longer a symbolic identifier character in 
0c1ec587a5a8
* Isar: ":" (colon) is no longer a symbolic identifier character;
wenzelm
parents:
20090
diff
changeset

161 
outer syntax. Thus symbolic identifiers may be used without 
0c1ec587a5a8
* Isar: ":" (colon) is no longer a symbolic identifier character;
wenzelm
parents:
20090
diff
changeset

162 
additional white space in declarations like this: ``assume *: A''. 
0c1ec587a5a8
* Isar: ":" (colon) is no longer a symbolic identifier character;
wenzelm
parents:
20090
diff
changeset

163 

20013  164 
* Isar: 'print_facts' prints all local facts of the current context, 
165 
both named and unnamed ones. 

166 

18308  167 
* Isar: 'def' now admits simultaneous definitions, e.g.: 
168 

169 
def x == "t" and y == "u" 

170 

18540  171 
* Isar: added command 'unfolding', which is structurally similar to 
172 
'using', but affects both the goal state and facts by unfolding given 

18815
cb778c0ce1b5
Pure/Isar: (un)folded, (un)fold, unfolding support
wenzelm
parents:
18738
diff
changeset

173 
rewrite rules. Thus many occurrences of the 'unfold' method or 
18540  174 
'unfolded' attribute may be replaced by firstclass proof text. 
175 

18815
cb778c0ce1b5
Pure/Isar: (un)folded, (un)fold, unfolding support
wenzelm
parents:
18738
diff
changeset

176 
* Isar: methods 'unfold' / 'fold', attributes 'unfolded' / 'folded', 
cb778c0ce1b5
Pure/Isar: (un)folded, (un)fold, unfolding support
wenzelm
parents:
18738
diff
changeset

177 
and command 'unfolding' now all support objectlevel equalities 
cb778c0ce1b5
Pure/Isar: (un)folded, (un)fold, unfolding support
wenzelm
parents:
18738
diff
changeset

178 
(potentially conditional). The underlying notion of rewrite rule is 
cb778c0ce1b5
Pure/Isar: (un)folded, (un)fold, unfolding support
wenzelm
parents:
18738
diff
changeset

179 
analogous to the 'rule_format' attribute, but *not* that of the 
cb778c0ce1b5
Pure/Isar: (un)folded, (un)fold, unfolding support
wenzelm
parents:
18738
diff
changeset

180 
Simplifier (which is usually more generous). 
cb778c0ce1b5
Pure/Isar: (un)folded, (un)fold, unfolding support
wenzelm
parents:
18738
diff
changeset

181 

19220  182 
* Isar: the goal restriction operator [N] (default N = 1) evaluates a 
183 
method expression within a sandbox consisting of the first N 

19240  184 
subgoals, which need to exist. For example, ``simp_all [3]'' 
185 
simplifies the first three subgoals, while (rule foo, simp_all)[] 

186 
simplifies all new goals that emerge from applying rule foo to the 

187 
originally first one. 

19220  188 

19814
faa698d46686
* Theory syntax: some popular names (e.g. "class", "if") are now keywords.
wenzelm
parents:
19783
diff
changeset

189 
* Isar: schematic goals are no longer restricted to higherorder 
faa698d46686
* Theory syntax: some popular names (e.g. "class", "if") are now keywords.
wenzelm
parents:
19783
diff
changeset

190 
patterns; e.g. ``lemma "?P(?x)" by (rule TrueI)'' now works as 
faa698d46686
* Theory syntax: some popular names (e.g. "class", "if") are now keywords.
wenzelm
parents:
19783
diff
changeset

191 
expected. 
faa698d46686
* Theory syntax: some popular names (e.g. "class", "if") are now keywords.
wenzelm
parents:
19783
diff
changeset

192 

18901  193 
* Isar: the conclusion of a long theorem statement is now either 
194 
'shows' (a simultaneous conjunction, as before), or 'obtains' 

195 
(essentially a disjunction of cases with local parameters and 

196 
assumptions). The latter allows to express general elimination rules 

18910  197 
adequately; in this notation common elimination rules look like this: 
18901  198 

199 
lemma exE:  "EX x. P x ==> (!!x. P x ==> thesis) ==> thesis" 

200 
assumes "EX x. P x" 

201 
obtains x where "P x" 

202 

203 
lemma conjE:  "A & B ==> (A ==> B ==> thesis) ==> thesis" 

204 
assumes "A & B" 

205 
obtains A and B 

206 

207 
lemma disjE:  "A  B ==> (A ==> thesis) ==> (B ==> thesis) ==> thesis" 

208 
assumes "A  B" 

209 
obtains 

210 
A 

211 
 B 

212 

18910  213 
The subsequent classical rules even refer to the formal "thesis" 
18901  214 
explicitly: 
215 

216 
lemma classical:  "(~ thesis ==> thesis) ==> thesis" 

217 
obtains "~ thesis" 

218 

18910  219 
lemma Peirce's_Law:  "((thesis ==> something) ==> thesis) ==> thesis" 
220 
obtains "thesis ==> something" 

18901  221 

222 
The actual proof of an 'obtains' statement is analogous to that of the 

18910  223 
Isar proof element 'obtain', only that there may be several cases. 
224 
Optional case names may be specified in parentheses; these will be 

225 
available both in the present proof and as annotations in the 

226 
resulting rule, for later use with the 'cases' method (cf. attribute 

227 
case_names). 

18901  228 

21447
379f130843f7
* Isar: the assumptions of a long theorem statement are available as assms;
wenzelm
parents:
21406
diff
changeset

229 
* Isar: the assumptions of a long theorem statement are available as 
379f130843f7
* Isar: the assumptions of a long theorem statement are available as assms;
wenzelm
parents:
21406
diff
changeset

230 
"assms" fact in the proof context. This is more appropriate than the 
379f130843f7
* Isar: the assumptions of a long theorem statement are available as assms;
wenzelm
parents:
21406
diff
changeset

231 
(historical) "prems", which refers to all assumptions of the current 
379f130843f7
* Isar: the assumptions of a long theorem statement are available as assms;
wenzelm
parents:
21406
diff
changeset

232 
context, including those from the target locale, proof body etc. 
379f130843f7
* Isar: the assumptions of a long theorem statement are available as assms;
wenzelm
parents:
21406
diff
changeset

233 

19263  234 
* Isar: 'print_statement' prints theorems from the current theory or 
235 
proof context in long statement form, according to the syntax of a 

236 
toplevel lemma. 

237 

18901  238 
* Isar: 'obtain' takes an optional case name for the local context 
239 
introduction rule (default "that"). 

240 

19587  241 
* Isar: removed obsolete 'concl is' patterns. INCOMPATIBILITY, use 
242 
explicit (is "_ ==> ?foo") in the rare cases where this still happens 

243 
to occur. 

244 

19682
c8c301eb965a
* Pure: syntax 'CONST name' produces a fully internalized constant;
wenzelm
parents:
19665
diff
changeset

245 
* Pure: syntax "CONST name" produces a fully internalized constant 
c8c301eb965a
* Pure: syntax 'CONST name' produces a fully internalized constant;
wenzelm
parents:
19665
diff
changeset

246 
according to the current context. This is particularly useful for 
c8c301eb965a
* Pure: syntax 'CONST name' produces a fully internalized constant;
wenzelm
parents:
19665
diff
changeset

247 
syntax translations that should refer to internal constant 
c8c301eb965a
* Pure: syntax 'CONST name' produces a fully internalized constant;
wenzelm
parents:
19665
diff
changeset

248 
representations independently of name spaces. 
c8c301eb965a
* Pure: syntax 'CONST name' produces a fully internalized constant;
wenzelm
parents:
19665
diff
changeset

249 

21537
45b3a85ee548
* Pure: syntax constant for foo (binder) is called foo_binder;
wenzelm
parents:
21471
diff
changeset

250 
* Pure: syntax constant for foo (binder "FOO ") is called "foo_binder" 
45b3a85ee548
* Pure: syntax constant for foo (binder) is called foo_binder;
wenzelm
parents:
21471
diff
changeset

251 
instead of "FOO ". This allows multiple binder declarations to coexist 
45b3a85ee548
* Pure: syntax constant for foo (binder) is called foo_binder;
wenzelm
parents:
21471
diff
changeset

252 
in the same context. INCOMPATIBILITY. 
45b3a85ee548
* Pure: syntax constant for foo (binder) is called foo_binder;
wenzelm
parents:
21471
diff
changeset

253 

21209
dbb8decc36bc
'const_syntax' command: allow fixed variables, renamed to 'notation';
wenzelm
parents:
21200
diff
changeset

254 
* Isar/locales: 'notation' provides a robust interface to the 'syntax' 
dbb8decc36bc
'const_syntax' command: allow fixed variables, renamed to 'notation';
wenzelm
parents:
21200
diff
changeset

255 
primitive that also works in a locale context (both for constants and 
dbb8decc36bc
'const_syntax' command: allow fixed variables, renamed to 'notation';
wenzelm
parents:
21200
diff
changeset

256 
fixed variables). Type declaration and internal syntactic 
dbb8decc36bc
'const_syntax' command: allow fixed variables, renamed to 'notation';
wenzelm
parents:
21200
diff
changeset

257 
representation of given constants retrieved from the context. 
19682
c8c301eb965a
* Pure: syntax 'CONST name' produces a fully internalized constant;
wenzelm
parents:
19665
diff
changeset

258 

19665  259 
* Isar/locales: new derived specification elements 'axiomatization', 
260 
'definition', 'abbreviation', which support typeinference, admit 

19083  261 
objectlevel specifications (equality, equivalence). See also the 
262 
isarref manual. Examples: 

19081
085b5badb8de
* Isar/locales: new derived specification elements 'definition', 'abbreviation', 'axiomatization';
wenzelm
parents:
19034
diff
changeset

263 

19665  264 
axiomatization 
21595  265 
eq (infix "===" 50) where 
266 
eq_refl: "x === x" and eq_subst: "x === y ==> P x ==> P y" 

267 

268 
definition "f x y = x + y + 1" 

269 
definition g where "g x = f x x" 

19081
085b5badb8de
* Isar/locales: new derived specification elements 'definition', 'abbreviation', 'axiomatization';
wenzelm
parents:
19034
diff
changeset

270 

19363  271 
abbreviation 
21595  272 
neq (infix "=!=" 50) where 
19363  273 
"x =!= y == ~ (x === y)" 
19081
085b5badb8de
* Isar/locales: new derived specification elements 'definition', 'abbreviation', 'axiomatization';
wenzelm
parents:
19034
diff
changeset

274 

19083  275 
These specifications may be also used in a locale context. Then the 
276 
constants being introduced depend on certain fixed parameters, and the 

277 
constant name is qualified by the locale base name. An internal 

278 
abbreviation takes care for convenient input and output, making the 

19088  279 
parameters implicit and using the original short name. See also 
19083  280 
HOL/ex/Abstract_NAT.thy for an example of deriving polymorphic 
281 
entities from a monomorphic theory. 

282 

283 
Presently, abbreviations are only available 'in' a target locale, but 

19363  284 
not inherited by general import expressions. Also note that 
285 
'abbreviation' may be used as a typesafe replacement for 'syntax' + 

286 
'translations' in common applications. 

19084  287 

19682
c8c301eb965a
* Pure: syntax 'CONST name' produces a fully internalized constant;
wenzelm
parents:
19665
diff
changeset

288 
Concrete syntax is attached to specified constants in internal form, 
c8c301eb965a
* Pure: syntax 'CONST name' produces a fully internalized constant;
wenzelm
parents:
19665
diff
changeset

289 
independently of name spaces. The parse tree representation is 
21209
dbb8decc36bc
'const_syntax' command: allow fixed variables, renamed to 'notation';
wenzelm
parents:
21200
diff
changeset

290 
slightly different  use 'notation' instead of raw 'syntax', and 
19682
c8c301eb965a
* Pure: syntax 'CONST name' produces a fully internalized constant;
wenzelm
parents:
19665
diff
changeset

291 
'translations' with explicit "CONST" markup to accommodate this. 
19665  292 

21735  293 
* Pure: command 'print_abbrevs' prints all constant abbreviations of 
294 
the current context. Print mode "no_abbrevs" prevents inversion of 

295 
abbreviations on output. 

296 

19783  297 
* Isar/locales: improved parameter handling: 
298 
 use of locales "var" and "struct" no longer necessary; 

299 
 parameter renamings are no longer required to be injective. 

300 
This enables, for example, to define a locale for endomorphisms thus: 

301 
locale endom = homom mult mult h. 

302 

19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19895
diff
changeset

303 
* Isar/locales: changed the way locales with predicates are defined. 
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19895
diff
changeset

304 
Instead of accumulating the specification, the imported expression is 
22126  305 
now an interpretation. INCOMPATIBILITY: different normal form of 
306 
locale expressions. In particular, in interpretations of locales with 

307 
predicates, goals repesenting already interpreted fragments are not 

308 
removed automatically. Use methods `intro_locales' and 

309 
`unfold_locales'; see below. 

310 

311 
* Isar/locales: new methods `intro_locales' and `unfold_locales' 

312 
provide backward reasoning on locales predicates. The methods are 

313 
aware of interpretations and discharge corresponding goals. 

314 
`intro_locales' is less aggressive then `unfold_locales' and does not 

315 
unfold predicates to assumptions. 

19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19895
diff
changeset

316 

fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19895
diff
changeset

317 
* Isar/locales: the order in which locale fragments are accumulated 
22126  318 
has changed. This enables to override declarations from fragments due 
319 
to interpretations  for example, unwanted simp rules. 

19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19895
diff
changeset

320 

18233  321 
* Provers/induct: improved internal context management to support 
322 
local fixes and defines onthefly. Thus explicit metalevel 

323 
connectives !! and ==> are rarely required anymore in inductive goals 

324 
(using objectlogic connectives for this purpose has been long 

325 
obsolete anyway). The subsequent proof patterns illustrate advanced 

326 
techniques of natural induction; general datatypes and inductive sets 

18267  327 
work analogously (see also src/HOL/Lambda for realistic examples). 
328 

329 
(1) This is how to ``strengthen'' an inductive goal wrt. certain 

18239  330 
parameters: 
18233  331 

332 
lemma 

333 
fixes n :: nat and x :: 'a 

334 
assumes a: "A n x" 

335 
shows "P n x" 

336 
using a  {* make induct insert fact a *} 

20503  337 
proof (induct n arbitrary: x)  {* generalize goal to "!!x. A n x ==> P n x" *} 
18248  338 
case 0 
18233  339 
show ?case sorry 
340 
next 

18248  341 
case (Suc n) 
18239  342 
note `!!x. A n x ==> P n x`  {* induction hypothesis, according to induction rule *} 
343 
note `A (Suc n) x`  {* induction premise, stemming from fact a *} 

18233  344 
show ?case sorry 
345 
qed 

346 

18267  347 
(2) This is how to perform induction over ``expressions of a certain 
18233  348 
form'', using a locally defined inductive parameter n == "a x" 
18239  349 
together with strengthening (the latter is usually required to get 
18267  350 
sufficiently flexible induction hypotheses): 
18233  351 

352 
lemma 

353 
fixes a :: "'a => nat" 

354 
assumes a: "A (a x)" 

355 
shows "P (a x)" 

356 
using a 

20503  357 
proof (induct n == "a x" arbitrary: x) 
18233  358 
... 
359 

18267  360 
See also HOL/Isar_examples/Puzzle.thy for an application of the this 
361 
particular technique. 

362 

18901  363 
(3) This is how to perform existential reasoning ('obtains' or 
364 
'obtain') by induction, while avoiding explicit objectlogic 

365 
encodings: 

366 

367 
lemma 

368 
fixes n :: nat 

369 
obtains x :: 'a where "P n x" and "Q n x" 

20503  370 
proof (induct n arbitrary: thesis) 
18267  371 
case 0 
372 
obtain x where "P 0 x" and "Q 0 x" sorry 

18399  373 
then show thesis by (rule 0) 
18267  374 
next 
375 
case (Suc n) 

376 
obtain x where "P n x" and "Q n x" by (rule Suc.hyps) 

377 
obtain x where "P (Suc n) x" and "Q (Suc n) x" sorry 

378 
then show thesis by (rule Suc.prems) 

379 
qed 

380 

20503  381 
Here the 'arbitrary: thesis' specification essentially modifies the 
382 
scope of the formal thesis parameter, in order to the get the whole 

18267  383 
existence statement through the induction as expected. 
18233  384 

18506
96260fb11449
* Provers/induct: support simultaneous goals with mutual rules;
wenzelm
parents:
18495
diff
changeset

385 
* Provers/induct: mutual induction rules are now specified as a list 
96260fb11449
* Provers/induct: support simultaneous goals with mutual rules;
wenzelm
parents:
18495
diff
changeset

386 
of rule sharing the same induction cases. HOL packages usually 
96260fb11449
* Provers/induct: support simultaneous goals with mutual rules;
wenzelm
parents:
18495
diff
changeset

387 
provide foo_bar.inducts for mutually defined items foo and bar 
96260fb11449
* Provers/induct: support simultaneous goals with mutual rules;
wenzelm
parents:
18495
diff
changeset

388 
(e.g. inductive sets or datatypes). INCOMPATIBILITY, users need to 
96260fb11449
* Provers/induct: support simultaneous goals with mutual rules;
wenzelm
parents:
18495
diff
changeset

389 
specify mutual induction rules differently, i.e. like this: 
96260fb11449
* Provers/induct: support simultaneous goals with mutual rules;
wenzelm
parents:
18495
diff
changeset

390 

96260fb11449
* Provers/induct: support simultaneous goals with mutual rules;
wenzelm
parents:
18495
diff
changeset

391 
(induct rule: foo_bar.inducts) 
96260fb11449
* Provers/induct: support simultaneous goals with mutual rules;
wenzelm
parents:
18495
diff
changeset

392 
(induct set: foo bar) 
96260fb11449
* Provers/induct: support simultaneous goals with mutual rules;
wenzelm
parents:
18495
diff
changeset

393 
(induct type: foo bar) 
96260fb11449
* Provers/induct: support simultaneous goals with mutual rules;
wenzelm
parents:
18495
diff
changeset

394 

96260fb11449
* Provers/induct: support simultaneous goals with mutual rules;
wenzelm
parents:
18495
diff
changeset

395 
The ML function ProjectRule.projections turns oldstyle rules into the 
96260fb11449
* Provers/induct: support simultaneous goals with mutual rules;
wenzelm
parents:
18495
diff
changeset

396 
new format. 
96260fb11449
* Provers/induct: support simultaneous goals with mutual rules;
wenzelm
parents:
18495
diff
changeset

397 

96260fb11449
* Provers/induct: support simultaneous goals with mutual rules;
wenzelm
parents:
18495
diff
changeset

398 
* Provers/induct: improved handling of simultaneous goals. Instead of 
96260fb11449
* Provers/induct: support simultaneous goals with mutual rules;
wenzelm
parents:
18495
diff
changeset

399 
introducing objectlevel conjunction, the statement is now split into 
96260fb11449
* Provers/induct: support simultaneous goals with mutual rules;
wenzelm
parents:
18495
diff
changeset

400 
several conclusions, while the corresponding symbolic cases are 
18601
b248754b60bc
* Provers/induct: improved simultaneous goals  nested cases;
wenzelm
parents:
18590
diff
changeset

401 
nested accordingly. INCOMPATIBILITY, proofs need to be structured 
b248754b60bc
* Provers/induct: improved simultaneous goals  nested cases;
wenzelm
parents:
18590
diff
changeset

402 
explicitly. For example: 
18480
8ac97f71369d
* induct: improved treatment of mutual goals and mutual rules;
wenzelm
parents:
18450
diff
changeset

403 

8ac97f71369d
* induct: improved treatment of mutual goals and mutual rules;
wenzelm
parents:
18450
diff
changeset

404 
lemma 
8ac97f71369d
* induct: improved treatment of mutual goals and mutual rules;
wenzelm
parents:
18450
diff
changeset

405 
fixes n :: nat 
8ac97f71369d
* induct: improved treatment of mutual goals and mutual rules;
wenzelm
parents:
18450
diff
changeset

406 
shows "P n" and "Q n" 
8ac97f71369d
* induct: improved treatment of mutual goals and mutual rules;
wenzelm
parents:
18450
diff
changeset

407 
proof (induct n) 
18601
b248754b60bc
* Provers/induct: improved simultaneous goals  nested cases;
wenzelm
parents:
18590
diff
changeset

408 
case 0 case 1 
18480
8ac97f71369d
* induct: improved treatment of mutual goals and mutual rules;
wenzelm
parents:
18450
diff
changeset

409 
show "P 0" sorry 
8ac97f71369d
* induct: improved treatment of mutual goals and mutual rules;
wenzelm
parents:
18450
diff
changeset

410 
next 
18601
b248754b60bc
* Provers/induct: improved simultaneous goals  nested cases;
wenzelm
parents:
18590
diff
changeset

411 
case 0 case 2 
18480
8ac97f71369d
* induct: improved treatment of mutual goals and mutual rules;
wenzelm
parents:
18450
diff
changeset

412 
show "Q 0" sorry 
8ac97f71369d
* induct: improved treatment of mutual goals and mutual rules;
wenzelm
parents:
18450
diff
changeset

413 
next 
18601
b248754b60bc
* Provers/induct: improved simultaneous goals  nested cases;
wenzelm
parents:
18590
diff
changeset

414 
case (Suc n) case 1 
18480
8ac97f71369d
* induct: improved treatment of mutual goals and mutual rules;
wenzelm
parents:
18450
diff
changeset

415 
note `P n` and `Q n` 
8ac97f71369d
* induct: improved treatment of mutual goals and mutual rules;
wenzelm
parents:
18450
diff
changeset

416 
show "P (Suc n)" sorry 
8ac97f71369d
* induct: improved treatment of mutual goals and mutual rules;
wenzelm
parents:
18450
diff
changeset

417 
next 
18601
b248754b60bc
* Provers/induct: improved simultaneous goals  nested cases;
wenzelm
parents:
18590
diff
changeset

418 
case (Suc n) case 2 
18480
8ac97f71369d
* induct: improved treatment of mutual goals and mutual rules;
wenzelm
parents:
18450
diff
changeset

419 
note `P n` and `Q n` 
8ac97f71369d
* induct: improved treatment of mutual goals and mutual rules;
wenzelm
parents:
18450
diff
changeset

420 
show "Q (Suc n)" sorry 
8ac97f71369d
* induct: improved treatment of mutual goals and mutual rules;
wenzelm
parents:
18450
diff
changeset

421 
qed 
8ac97f71369d
* induct: improved treatment of mutual goals and mutual rules;
wenzelm
parents:
18450
diff
changeset

422 

18601
b248754b60bc
* Provers/induct: improved simultaneous goals  nested cases;
wenzelm
parents:
18590
diff
changeset

423 
The split into subcases may be deferred as follows  this is 
b248754b60bc
* Provers/induct: improved simultaneous goals  nested cases;
wenzelm
parents:
18590
diff
changeset

424 
particularly relevant for goal statements with local premises. 
b248754b60bc
* Provers/induct: improved simultaneous goals  nested cases;
wenzelm
parents:
18590
diff
changeset

425 

b248754b60bc
* Provers/induct: improved simultaneous goals  nested cases;
wenzelm
parents:
18590
diff
changeset

426 
lemma 
b248754b60bc
* Provers/induct: improved simultaneous goals  nested cases;
wenzelm
parents:
18590
diff
changeset

427 
fixes n :: nat 
b248754b60bc
* Provers/induct: improved simultaneous goals  nested cases;
wenzelm
parents:
18590
diff
changeset

428 
shows "A n ==> P n" and "B n ==> Q n" 
b248754b60bc
* Provers/induct: improved simultaneous goals  nested cases;
wenzelm
parents:
18590
diff
changeset

429 
proof (induct n) 
b248754b60bc
* Provers/induct: improved simultaneous goals  nested cases;
wenzelm
parents:
18590
diff
changeset

430 
case 0 
b248754b60bc
* Provers/induct: improved simultaneous goals  nested cases;
wenzelm
parents:
18590
diff
changeset

431 
{ 
b248754b60bc
* Provers/induct: improved simultaneous goals  nested cases;
wenzelm
parents:
18590
diff
changeset

432 
case 1 
b248754b60bc
* Provers/induct: improved simultaneous goals  nested cases;
wenzelm
parents:
18590
diff
changeset

433 
note `A 0` 
b248754b60bc
* Provers/induct: improved simultaneous goals  nested cases;
wenzelm
parents:
18590
diff
changeset

434 
show "P 0" sorry 
b248754b60bc
* Provers/induct: improved simultaneous goals  nested cases;
wenzelm
parents:
18590
diff
changeset

435 
next 
b248754b60bc
* Provers/induct: improved simultaneous goals  nested cases;
wenzelm
parents:
18590
diff
changeset

436 
case 2 
b248754b60bc
* Provers/induct: improved simultaneous goals  nested cases;
wenzelm
parents:
18590
diff
changeset

437 
note `B 0` 
b248754b60bc
* Provers/induct: improved simultaneous goals  nested cases;
wenzelm
parents:
18590
diff
changeset

438 
show "Q 0" sorry 
b248754b60bc
* Provers/induct: improved simultaneous goals  nested cases;
wenzelm
parents:
18590
diff
changeset

439 
} 
b248754b60bc
* Provers/induct: improved simultaneous goals  nested cases;
wenzelm
parents:
18590
diff
changeset

440 
next 
b248754b60bc
* Provers/induct: improved simultaneous goals  nested cases;
wenzelm
parents:
18590
diff
changeset

441 
case (Suc n) 
b248754b60bc
* Provers/induct: improved simultaneous goals  nested cases;
wenzelm
parents:
18590
diff
changeset

442 
note `A n ==> P n` and `B n ==> Q n` 
b248754b60bc
* Provers/induct: improved simultaneous goals  nested cases;
wenzelm
parents:
18590
diff
changeset

443 
{ 
b248754b60bc
* Provers/induct: improved simultaneous goals  nested cases;
wenzelm
parents:
18590
diff
changeset

444 
case 1 
b248754b60bc
* Provers/induct: improved simultaneous goals  nested cases;
wenzelm
parents:
18590
diff
changeset

445 
note `A (Suc n)` 
b248754b60bc
* Provers/induct: improved simultaneous goals  nested cases;
wenzelm
parents:
18590
diff
changeset

446 
show "P (Suc n)" sorry 
b248754b60bc
* Provers/induct: improved simultaneous goals  nested cases;
wenzelm
parents:
18590
diff
changeset

447 
next 
b248754b60bc
* Provers/induct: improved simultaneous goals  nested cases;
wenzelm
parents:
18590
diff
changeset

448 
case 2 
b248754b60bc
* Provers/induct: improved simultaneous goals  nested cases;
wenzelm
parents:
18590
diff
changeset

449 
note `B (Suc n)` 
b248754b60bc
* Provers/induct: improved simultaneous goals  nested cases;
wenzelm
parents:
18590
diff
changeset

450 
show "Q (Suc n)" sorry 
b248754b60bc
* Provers/induct: improved simultaneous goals  nested cases;
wenzelm
parents:
18590
diff
changeset

451 
} 
b248754b60bc
* Provers/induct: improved simultaneous goals  nested cases;
wenzelm
parents:
18590
diff
changeset

452 
qed 
b248754b60bc
* Provers/induct: improved simultaneous goals  nested cases;
wenzelm
parents:
18590
diff
changeset

453 

18506
96260fb11449
* Provers/induct: support simultaneous goals with mutual rules;
wenzelm
parents:
18495
diff
changeset

454 
If simultaneous goals are to be used with mutual rules, the statement 
96260fb11449
* Provers/induct: support simultaneous goals with mutual rules;
wenzelm
parents:
18495
diff
changeset

455 
needs to be structured carefully as a twolevel conjunction, using 
96260fb11449
* Provers/induct: support simultaneous goals with mutual rules;
wenzelm
parents:
18495
diff
changeset

456 
lists of propositions separated by 'and': 
96260fb11449
* Provers/induct: support simultaneous goals with mutual rules;
wenzelm
parents:
18495
diff
changeset

457 

18507  458 
lemma 
459 
shows "a : A ==> P1 a" 

460 
"a : A ==> P2 a" 

461 
and "b : B ==> Q1 b" 

462 
"b : B ==> Q2 b" 

463 
"b : B ==> Q3 b" 

464 
proof (induct set: A B) 

18480
8ac97f71369d
* induct: improved treatment of mutual goals and mutual rules;
wenzelm
parents:
18450
diff
changeset

465 

18399  466 
* Provers/induct: support coinduction as well. See 
467 
src/HOL/Library/Coinductive_List.thy for various examples. 

468 

20919
dab803075c62
attribute "symmetric": standardized schematic variables;
wenzelm
parents:
20857
diff
changeset

469 
* Attribute "symmetric" produces result with standardized schematic 
dab803075c62
attribute "symmetric": standardized schematic variables;
wenzelm
parents:
20857
diff
changeset

470 
variables (index 0). Potential INCOMPATIBILITY. 
dab803075c62
attribute "symmetric": standardized schematic variables;
wenzelm
parents:
20857
diff
changeset

471 

22126  472 
* Simplifier: by default the simplifier trace only shows top level 
473 
rewrites now. That is, trace_simp_depth_limit is set to 1 by 

474 
default. Thus there is less danger of being flooded by the trace. The 

475 
trace indicates where parts have been suppressed. 

18674  476 

18536
ab3f32f86847
* Provers/classical: removed obsolete classical version of elim_format;
wenzelm
parents:
18507
diff
changeset

477 
* Provers/classical: removed obsolete classical version of elim_format 
ab3f32f86847
* Provers/classical: removed obsolete classical version of elim_format;
wenzelm
parents:
18507
diff
changeset

478 
attribute; classical elim/dest rules are now treated uniformly when 
ab3f32f86847
* Provers/classical: removed obsolete classical version of elim_format;
wenzelm
parents:
18507
diff
changeset

479 
manipulating the claset. 
ab3f32f86847
* Provers/classical: removed obsolete classical version of elim_format;
wenzelm
parents:
18507
diff
changeset

480 

18694  481 
* Provers/classical: stricter checks to ensure that supplied intro, 
482 
dest and elim rules are wellformed; dest and elim rules must have at 

483 
least one premise. 

484 

485 
* Provers/classical: attributes dest/elim/intro take an optional 

18695  486 
weight argument for the rule (just as the Pure versions). Weights are 
18696  487 
ignored by automated tools, but determine the search order of single 
18694  488 
rule steps. 
18557
60a0f9caa0a2
Provers/classical: stricter checks to ensure that supplied intro, dest and
paulson
parents:
18549
diff
changeset

489 

18536
ab3f32f86847
* Provers/classical: removed obsolete classical version of elim_format;
wenzelm
parents:
18507
diff
changeset

490 
* Syntax: input syntax now supports dummy variable binding "%_. b", 
ab3f32f86847
* Provers/classical: removed obsolete classical version of elim_format;
wenzelm
parents:
18507
diff
changeset

491 
where the body does not mention the bound variable. Note that dummy 
ab3f32f86847
* Provers/classical: removed obsolete classical version of elim_format;
wenzelm
parents:
18507
diff
changeset

492 
patterns implicitly depend on their context of bounds, which makes 
ab3f32f86847
* Provers/classical: removed obsolete classical version of elim_format;
wenzelm
parents:
18507
diff
changeset

493 
"{_. _}" match any set comprehension as expected. Potential 
ab3f32f86847
* Provers/classical: removed obsolete classical version of elim_format;
wenzelm
parents:
18507
diff
changeset

494 
INCOMPATIBILITY  parse translations need to cope with syntactic 
ab3f32f86847
* Provers/classical: removed obsolete classical version of elim_format;
wenzelm
parents:
18507
diff
changeset

495 
constant "_idtdummy" in the binding position. 
ab3f32f86847
* Provers/classical: removed obsolete classical version of elim_format;
wenzelm
parents:
18507
diff
changeset

496 

ab3f32f86847
* Provers/classical: removed obsolete classical version of elim_format;
wenzelm
parents:
18507
diff
changeset

497 
* Syntax: removed obsolete syntactic constant "_K" and its associated 
ab3f32f86847
* Provers/classical: removed obsolete classical version of elim_format;
wenzelm
parents:
18507
diff
changeset

498 
parse translation. INCOMPATIBILITY  use dummy abstraction instead, 
ab3f32f86847
* Provers/classical: removed obsolete classical version of elim_format;
wenzelm
parents:
18507
diff
changeset

499 
for example "A > B" => "Pi A (%_. B)". 
17779  500 

20582
ebd0e03c6a9b
* Pure: 'class_deps' command visualizes the subclass relation;
wenzelm
parents:
20503
diff
changeset

501 
* Pure: 'class_deps' command visualizes the subclass relation, using 
ebd0e03c6a9b
* Pure: 'class_deps' command visualizes the subclass relation;
wenzelm
parents:
20503
diff
changeset

502 
the graph browser tool. 
ebd0e03c6a9b
* Pure: 'class_deps' command visualizes the subclass relation;
wenzelm
parents:
20503
diff
changeset

503 

20620
8b26f58c5646
* Pure: 'print_theory' now suppresses entities with internal name;
wenzelm
parents:
20607
diff
changeset

504 
* Pure: 'print_theory' now suppresses entities with internal name 
8b26f58c5646
* Pure: 'print_theory' now suppresses entities with internal name;
wenzelm
parents:
20607
diff
changeset

505 
(trailing "_") by default; use '!' option for full details. 
8b26f58c5646
* Pure: 'print_theory' now suppresses entities with internal name;
wenzelm
parents:
20607
diff
changeset

506 

17865  507 

17806  508 
*** HOL *** 
509 

22126  510 
* Added syntactic class "size"; overloaded constant "size" now has 
511 
type "'a::size ==> bool" 

512 

513 
* Renamed constants "Divides.op div", "Divides.op mod" and "Divides.op 

514 
dvd" to "Divides.div", "Divides.mod" and 

515 
"Divides.dvd". INCOMPATIBILITY. 

516 

517 
* Added method "lexicographic_order" automatically synthesizes 

518 
termination relations as lexicographic combinations of size measures 

519 
 'function' package. 

520 

521 
* HOL/records: generalised fieldupdate to take a function on the 

522 
field rather than the new value: r(A := x) is translated to A_update 

523 
(K x) r The Kcombinator that is internally used is called K_record. 

21226
a607ae87ee81
fieldupdate in records is generalised to take a function on the field
schirmer
parents:
21215
diff
changeset

524 
INCOMPATIBILITY: Usage of the plain update functions has to be 
a607ae87ee81
fieldupdate in records is generalised to take a function on the field
schirmer
parents:
21215
diff
changeset

525 
adapted. 
a607ae87ee81
fieldupdate in records is generalised to take a function on the field
schirmer
parents:
21215
diff
changeset

526 

22126  527 
* axclass "semiring_0" now contains annihilation axioms x * 0 = 0 and 
528 
0 * x = 0, which are required for a semiring. Richer structures do 

529 
not inherit from semiring_0 anymore, because this property is a 

530 
theorem there, not an axiom. INCOMPATIBILITY: In instances of 

531 
semiring_0, there is more to prove, but this is mostly trivial. 

532 

533 
* axclass "recpower" was generalized to arbitrary monoids, not just 

534 
commutative semirings. INCOMPATIBILITY: If you use recpower and need 

535 
commutativity or a semiring property, add the corresponding classes. 

536 

537 
* Unified locale partial_order with class definition (cf. theory 

538 
Orderings), added parameter ``less''. INCOMPATIBILITY. 

21215
7c9337a0e30a
made locale partial_order compatible with axclass order
haftmann
parents:
21209
diff
changeset

539 

21099  540 
* Constant "List.list_all2" in List.thy now uses authentic syntax. 
22126  541 
INCOMPATIBILITY: translations containing list_all2 may go wrong. On 
542 
Isar level, use abbreviations instead. 

543 

544 
* Renamed constant "List.op mem" to "List.memberl" INCOMPATIBILITY: 

545 
rarely occuring name references (e.g. ``List.op mem.simps'') require 

546 
renaming (e.g. ``List.memberl.simps''). 

547 

548 
* Renamed constants "0" to "HOL.zero" and "1" to "HOL.one". 

549 
INCOMPATIBILITY. 

550 

551 
* Added theory Code_Generator providing class 'eq', allowing for code 

552 
generation with polymorphic equality. 

553 

554 
* Numeral syntax: type 'bin' which was a mere type copy of 'int' has 

555 
been abandoned in favour of plain 'int'. INCOMPATIBILITY  

556 
significant changes for setting up numeral syntax for types: 

20485  557 

558 
 new constants Numeral.pred and Numeral.succ instead 

559 
of former Numeral.bin_pred and Numeral.bin_succ. 

560 
 Use integer operations instead of bin_add, bin_mult and so on. 

561 
 Numeral simplification theorems named Numeral.numeral_simps instead of Bin_simps. 

562 
 ML structure Bin_Simprocs now named Int_Numeral_Base_Simprocs. 

563 

564 
See HOL/Integ/IntArith.thy for an example setup. 

565 

22126  566 
* New top level command 'normal_form' computes the normal form of a 
567 
term that may contain free variables. For example ``normal_form 

568 
"rev[a,b,c]"'' produces ``[b,c,a]'' (without proof). This command is 

569 
suitable for heavyduty computations because the functions are 

570 
compiled to ML first. 

19895  571 

17996  572 
* Alternative iff syntax "A <> B" for equality on bool (with priority 
573 
25 like >); output depends on the "iff" print_mode, the default is 

574 
"A = B" (with priority 50). 

575 

19279  576 
* Renamed constants in HOL.thy and Orderings.thy: 
19233
77ca20b0ed77
renamed HOL +  * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
19226
diff
changeset

577 
op + ~> HOL.plus 
77ca20b0ed77
renamed HOL +  * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
19226
diff
changeset

578 
op  ~> HOL.minus 
77ca20b0ed77
renamed HOL +  * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
19226
diff
changeset

579 
uminus ~> HOL.uminus 
77ca20b0ed77
renamed HOL +  * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
19226
diff
changeset

580 
op * ~> HOL.times 
19277  581 
op < ~> Orderings.less 
582 
op <= ~> Orderings.less_eq 

19233
77ca20b0ed77
renamed HOL +  * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
19226
diff
changeset

583 

77ca20b0ed77
renamed HOL +  * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
19226
diff
changeset

584 
Adaptions may be required in the following cases: 
77ca20b0ed77
renamed HOL +  * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
19226
diff
changeset

585 

19377  586 
a) Userdefined constants using any of the names "plus", "minus", "times", 
587 
"less" or "less_eq". The standard syntax translations for "+", "" and "*" 

588 
may go wrong. 

19233
77ca20b0ed77
renamed HOL +  * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
19226
diff
changeset

589 
INCOMPATIBILITY: use more specific names. 
77ca20b0ed77
renamed HOL +  * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
19226
diff
changeset

590 

19277  591 
b) Variables named "plus", "minus", "times", "less", "less_eq" 
19233
77ca20b0ed77
renamed HOL +  * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
19226
diff
changeset

592 
INCOMPATIBILITY: use more specific names. 
77ca20b0ed77
renamed HOL +  * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
19226
diff
changeset

593 

19377  594 
c) Permutative equations (e.g. "a + b = b + a") 
595 
Since the change of names also changes the order of terms, permutative 

596 
rewrite rules may get applied in a different order. Experience shows that 

597 
this is rarely the case (only two adaptions in the whole Isabelle 

598 
distribution). 

599 
INCOMPATIBILITY: rewrite proofs 

19233
77ca20b0ed77
renamed HOL +  * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
19226
diff
changeset

600 

77ca20b0ed77
renamed HOL +  * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
19226
diff
changeset

601 
d) ML code directly refering to constant names 
77ca20b0ed77
renamed HOL +  * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
19226
diff
changeset

602 
This in general only affects handwritten proof tactics, simprocs and so on. 
77ca20b0ed77
renamed HOL +  * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
19226
diff
changeset

603 
INCOMPATIBILITY: grep your sourcecode and replace names. 
77ca20b0ed77
renamed HOL +  * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
19226
diff
changeset

604 

21265  605 
* Relations less (<) and less_eq (<=) are also available on type bool. 
606 
Modified syntax to disallow nesting without explicit parentheses, 

607 
e.g. "(x < y) < z" or "x < (y < z)", but NOT "x < y < z". 

608 

18674  609 
* "LEAST x:A. P" expands to "LEAST x. x:A & P" (input only). 
610 

20716
a6686a8e1b68
Changed precedence of "op O" (relation composition) from 60 to 75.
krauss
parents:
20712
diff
changeset

611 
* Relation composition operator "op O" now has precedence 75 and binds 
a6686a8e1b68
Changed precedence of "op O" (relation composition) from 60 to 75.
krauss
parents:
20712
diff
changeset

612 
stronger than union and intersection. INCOMPATIBILITY. 
a6686a8e1b68
Changed precedence of "op O" (relation composition) from 60 to 75.
krauss
parents:
20712
diff
changeset

613 

22126  614 
* The old set interval syntax "{m..n(}" (and relatives) has been 
615 
removed. Use "{m..<n}" (and relatives) instead. 

19377  616 

17865  617 
* In the context of the assumption "~(s = t)" the Simplifier rewrites 
618 
"t = s" to False (by simproc "neq_simproc"). For backward 

619 
compatibility this can be disabled by ML "reset use_neq_simproc". 

17779  620 

22126  621 
* "m dvd n" where m and n are numbers is evaluated to True/False by 
622 
simp. 

623 

624 
* Theorem Cons_eq_map_conv no longer declared as ``simp''. 

19211  625 

19279  626 
* Theorem setsum_mult renamed to setsum_right_distrib. 
627 

19211  628 
* Prefer ex1I over ex_ex1I in singlestep reasoning, e.g. by the 
22126  629 
``rule'' method. 
630 

631 
* Reimplemented methods ``sat'' and ``satx'', with several 

632 
improvements: goals no longer need to be stated as "<prems> ==> 

633 
False", equivalences (i.e. "=" on type bool) are handled, variable 

634 
names of the form "lit_<n>" are no longer reserved, significant 

635 
speedup. 

636 

637 
* Methods ``sat'' and ``satx'' can now replay MiniSat proof traces. 

638 
zChaff is still supported as well. 

639 

640 
* 'inductive' and 'datatype': provide projections of mutual rules, 

641 
bundled as foo_bar.inducts; 

642 

643 
* Library: moved theories Parity, GCD, Binomial, Infinite_Set to 

644 
Library. 

21256  645 

646 
* Library: moved theory Accessible_Part to main HOL. 

19572
a4b3176f19dd
* Library: theory Accessible_Part has been move to main HOL.
wenzelm
parents:
19508
diff
changeset

647 

18446  648 
* Library: added theory Coinductive_List of potentially infinite lists 
649 
as greatest fixedpoint. 

18399  650 

19254  651 
* Library: added theory AssocList which implements (finite) maps as 
19252  652 
association lists. 
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17806
diff
changeset

653 

22126  654 
* Added proof method ``evaluation'' for efficiently solving a goal 
655 
(i.e. a boolean expression) by compiling it to ML. The goal is 

656 
"proved" (via an oracle) if it evaluates to True. 

20807  657 

658 
* Linear arithmetic now splits certain operators (e.g. min, max, abs) 

659 
also when invoked by the simplifier. This results in the simplifier 

21056  660 
being more powerful on arithmetic goals. INCOMPATIBILITY. Set 
20807  661 
fast_arith_split_limit to 0 to obtain the old behavior. 
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20188
diff
changeset

662 

22126  663 
* Support for hex (0x20) and binary (0b1001) numerals. 
19254  664 

20807  665 
* New method: reify eqs (t), where eqs are equations for an 
666 
interpretation I :: 'a list => 'b => 'c and t::'c is an optional 

667 
parameter, computes a term s::'b and a list xs::'a list and proves the 

668 
theorem I xs s = t. This is also known as reification or quoting. The 

669 
resulting theorem is applied to the subgoal to substitute t with I xs 

670 
s. If t is omitted, the subgoal itself is reified. 

671 

672 
* New method: reflection corr_thm eqs (t). The parameters eqs and (t) 

673 
are as explained above. corr_thm is a theorem for I vs (f t) = I vs t, 

674 
where f is supposed to be a computable function (in the sense of code 

675 
generattion). The method uses reify to compute s and xs as above then 

676 
applies corr_thm and uses normalization by evaluation to "prove" f s = 

677 
r and finally gets the theorem t = r, which is again applied to the 

678 
subgoal. An Example is available in HOL/ex/ReflectionEx.thy. 

679 

680 
* Reflection: Automatic refification now handels binding, an example 

681 
is available in HOL/ex/ReflectionEx.thy 

682 

683 

20169  684 
*** HOLAlgebra *** 
685 

21170  686 
* Formalisation of ideals and the quotient construction over rings. 
687 

688 
* Order and lattice theory no longer based on records. 

689 
INCOMPATIBILITY. 

690 

22126  691 
* Renamed lemmas least_carrier > least_closed and greatest_carrier > 
692 
greatest_closed. INCOMPATIBILITY. 

21896
9a7949815a84
Experimenting with interpretations of "definition".
ballarin
parents:
21879
diff
changeset

693 

21170  694 
* Method algebra is now set up via an attribute. For examples see 
21896
9a7949815a84
Experimenting with interpretations of "definition".
ballarin
parents:
21879
diff
changeset

695 
Ring.thy. INCOMPATIBILITY: the method is now weaker on combinations 
21170  696 
of algebraic structures. 
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
20217
diff
changeset

697 

22126  698 
* Renamed theory CRing to Ring. 
20169  699 

20807  700 

19653  701 
*** HOLComplex *** 
702 

703 
* Theory Real: new method ferrack implements quantifier elimination 

704 
for linear arithmetic over the reals. The quantifier elimination 

705 
feature is used only for decision, for compatibility with arith. This 

706 
means a goal is either solved or left unchanged, no simplification. 

707 

21791  708 
* Real: New axiomatic classes formalize real normed vector spaces and 
709 
algebras, using new overloaded constants scaleR :: real => 'a => 'a 

710 
and norm :: 'a => real. 

711 

22126  712 
* Real: New constant of_real :: real => 'a::real_algebra_1 injects 
713 
from reals into other types. The overloaded constant Reals :: 'a set 

714 
is now defined as range of_real; potential INCOMPATIBILITY. 

715 

716 
* Hyperreal: Several constants that previously worked only for the 

717 
reals have been generalized, so they now work over arbitrary vector 

718 
spaces. Type annotations may need to be added in some cases; potential 

719 
INCOMPATIBILITY. 

21791  720 

721 
Infinitesimal :: ('a::real_normed_vector) star set" 

722 
HFinite :: ('a::real_normed_vector) star set" 

723 
HInfinite :: ('a::real_normed_vector) star set" 

724 
approx :: ('a::real_normed_vector) star => 'a star => bool 

725 
monad :: ('a::real_normed_vector) star => 'a star set 

726 
galaxy :: ('a::real_normed_vector) star => 'a star set 

727 
(NS)LIMSEQ :: [nat, 'a::real_normed_vector, 'a] => bool 

728 
(NS)convergent :: (nat => 'a::real_normed_vector) => bool 

729 
(NS)Bseq :: (nat => 'a::real_normed_vector) => bool 

730 
(NS)Cauchy :: (nat => 'a::real_normed_vector) => bool 

731 
(NS)LIM :: ['a::real_normed_vector => 'b::real_normed_vector, 'a, 'b] => bool 

732 
is(NS)Cont :: ['a::real_normed_vector => 'b::real_normed_vector, 'a] => bool 

733 
deriv :: ['a::real_normed_field => 'a, 'a, 'a] => bool 

734 

735 
* Complex: Some complexspecific constants are now abbreviations for 

22126  736 
overloaded ones: complex_of_real = of_real, cmod = norm, hcmod = 
737 
hnorm. Other constants have been entirely removed in favor of the 

738 
polymorphic versions (INCOMPATIBILITY): 

21791  739 

740 
approx < capprox 

741 
HFinite < CFinite 

742 
HInfinite < CInfinite 

743 
Infinitesimal < CInfinitesimal 

744 
monad < cmonad 

745 
galaxy < cgalaxy 

746 
(NS)LIM < (NS)CLIM, (NS)CRLIM 

747 
is(NS)Cont < is(NS)Contc, is(NS)contCR 

748 
(ns)deriv < (ns)cderiv 

749 

19653  750 

17878  751 
*** ML *** 
752 

22138  753 
* ML within Isar: antiquotations allow to embed staticallychecked 
754 
formal entities in the source, referring to the context available at 

755 
compiletime. For example: 

756 

757 
ML {* @{typ "'a => 'b"} *} 

758 
ML {* @{term "%x. x"} *} 

759 
ML {* @{prop "x == y"} *} 

760 
ML {* @{ctyp "'a => 'b"} *} 

761 
ML {* @{cterm "%x. x"} *} 

762 
ML {* @{cprop "x == y"} *} 

763 
ML {* @{thm asm_rl} *} 

764 
ML {* @{thms asm_rl} *} 

765 
ML {* @{context} *} 

766 
ML {* @{theory} *} 

767 
ML {* @{theory Pure} *} 

768 
ML {* @{simpset} *} 

769 
ML {* @{claset} *} 

770 
ML {* @{clasimpset} *} 

771 

20348  772 
* Pure/library: 
773 

18450
e57731ba01dd
discontinued unflat in favour of burrow and burrow_split
haftmann
parents:
18446
diff
changeset

774 
val burrow: ('a list > 'b list) > 'a list list > 'b list list 
18549
5308a6ea3b96
rearranged burrow_split to fold_burrow to allow composition with fold_map
haftmann
parents:
18540
diff
changeset

775 
val fold_burrow: ('a list > 'c > 'b list * 'd) > 'a list list > 'c > 'b list list * 'd 
18450
e57731ba01dd
discontinued unflat in favour of burrow and burrow_split
haftmann
parents:
18446
diff
changeset

776 

18540  777 
The semantics of "burrow" is: "take a function with *simulatanously* 
778 
transforms a list of value, and apply it *simulatanously* to a list of 

22126  779 
list of values of the appropriate type". Compare this with "map" which 
18540  780 
would *not* apply its argument function simulatanously but in 
22126  781 
sequence; "fold_burrow" has an additional context. 
18450
e57731ba01dd
discontinued unflat in favour of burrow and burrow_split
haftmann
parents:
18446
diff
changeset

782 

18446  783 
* Pure/library: functions map2 and fold2 with curried syntax for 
784 
simultanous mapping and folding: 

785 

18422
875451c9d253
rearranged tuples (theory * 'a) to ('a * theory) in Pure
haftmann
parents:
18399
diff
changeset

786 
val map2: ('a > 'b > 'c) > 'a list > 'b list > 'c list 
875451c9d253
rearranged tuples (theory * 'a) to ('a * theory) in Pure
haftmann
parents:
18399
diff
changeset

787 
val fold2: ('a > 'b > 'c > 'c) > 'a list > 'b list > 'c > 'c 
875451c9d253
rearranged tuples (theory * 'a) to ('a * theory) in Pure
haftmann
parents:
18399
diff
changeset

788 

18446  789 
* Pure/library: indexed lists  some functions in the Isabelle library 
790 
treating lists over 'a as finite mappings from [0...n] to 'a have been 

791 
given more convenient names and signatures reminiscent of similar 

792 
functions for alists, tables, etc: 

18051  793 

794 
val nth: 'a list > int > 'a 

795 
val nth_map: int > ('a > 'a) > 'a list > 'a list 

796 
val fold_index: (int * 'a > 'b > 'b) > 'a list > 'b > 'b 

797 

18446  798 
Note that fold_index starts counting at index 0, not 1 like foldln 
799 
used to. 

800 

22126  801 
* Pure/library: added general ``divide_and_conquer'' combinator on 
802 
lists. 

19032  803 

804 
* Pure/General/table.ML: the join operations now works via exceptions 

19081
085b5badb8de
* Isar/locales: new derived specification elements 'definition', 'abbreviation', 'axiomatization';
wenzelm
parents:
19034
diff
changeset

805 
DUP/SAME instead of type option. This is simpler in simple cases, and 
085b5badb8de
* Isar/locales: new derived specification elements 'definition', 'abbreviation', 'axiomatization';
wenzelm
parents:
19034
diff
changeset

806 
admits slightly more efficient complex applications. 
18446  807 

18642  808 
* Pure: datatype Context.generic joins theory/Proof.context and 
18644  809 
provides some facilities for code that works in either kind of 
18642  810 
context, notably GenericDataFun for uniform theory and proof data. 
811 

18862
bd83590be0f7
* Pure: 'advanced' translation functions use Context.generic instead of just theory;
wenzelm
parents:
18815
diff
changeset

812 
* Pure: 'advanced' translation functions (parse_translation etc.) now 
bd83590be0f7
* Pure: 'advanced' translation functions use Context.generic instead of just theory;
wenzelm
parents:
18815
diff
changeset

813 
use Context.generic instead of just theory. 
bd83590be0f7
* Pure: 'advanced' translation functions use Context.generic instead of just theory;
wenzelm
parents:
18815
diff
changeset

814 

18737  815 
* Pure: simplified internal attribute type, which is now always 
816 
Context.generic * thm > Context.generic * thm. Global (theory) 

817 
vs. local (Proof.context) attributes have been discontinued, while 

18738  818 
minimizing code duplication. Thm.rule_attribute and 
819 
Thm.declaration_attribute build canonical attributes; see also 

19006
2427684c201c
* ML/Pure: generic Args/Attrib syntax everywhere;
wenzelm
parents:
18979
diff
changeset

820 
structure Context for further operations on Context.generic, notably 
2427684c201c
* ML/Pure: generic Args/Attrib syntax everywhere;
wenzelm
parents:
18979
diff
changeset

821 
GenericDataFun. INCOMPATIBILITY, need to adapt attribute type 
2427684c201c
* ML/Pure: generic Args/Attrib syntax everywhere;
wenzelm
parents:
18979
diff
changeset

822 
declarations and definitions. 
2427684c201c
* ML/Pure: generic Args/Attrib syntax everywhere;
wenzelm
parents:
18979
diff
changeset

823 

19508  824 
* Pure/kernel: consts certification ignores sort constraints given in 
825 
signature declarations. (This information is not relevant to the 

22126  826 
logic, but only for type inference.) IMPORTANT INTERNAL CHANGE, 
827 
potential INCOMPATIBILITY. 

19508  828 

829 
* Pure: axiomatic type classes are now purely definitional, with 

830 
explicit proofs of class axioms and super class relations performed 

831 
internally. See Pure/axclass.ML for the main internal interfaces  

832 
notably AxClass.define_class supercedes AxClass.add_axclass, and 

833 
AxClass.axiomatize_class/classrel/arity supercede 

834 
Sign.add_classes/classrel/arities. 

835 

19006
2427684c201c
* ML/Pure: generic Args/Attrib syntax everywhere;
wenzelm
parents:
18979
diff
changeset

836 
* Pure/Isar: Args/Attrib parsers operate on Context.generic  
2427684c201c
* ML/Pure: generic Args/Attrib syntax everywhere;
wenzelm
parents:
18979
diff
changeset

837 
global/local versions on theory vs. Proof.context have been 
2427684c201c
* ML/Pure: generic Args/Attrib syntax everywhere;
wenzelm
parents:
18979
diff
changeset

838 
discontinued; Attrib.syntax and Method.syntax have been adapted 
2427684c201c
* ML/Pure: generic Args/Attrib syntax everywhere;
wenzelm
parents:
18979
diff
changeset

839 
accordingly. INCOMPATIBILITY, need to adapt parser expressions for 
2427684c201c
* ML/Pure: generic Args/Attrib syntax everywhere;
wenzelm
parents:
18979
diff
changeset

840 
attributes, methods, etc. 
18642  841 

18446  842 
* Pure: several functions of signature "... > theory > theory * ..." 
843 
have been reoriented to "... > theory > ... * theory" in order to 

844 
allow natural usage in combination with the >, >>, > and 

845 
fold_map combinators. 

18051  846 

21647
fccafa917a68
* Pure: official theorem names and additional comments are now strictly separate.
wenzelm
parents:
21595
diff
changeset

847 
* Pure: official theorem names (closed derivations) and additional 
fccafa917a68
* Pure: official theorem names and additional comments are now strictly separate.
wenzelm
parents:
21595
diff
changeset

848 
comments (tags) are now strictly separate. Name hints  which are 
fccafa917a68
* Pure: official theorem names and additional comments are now strictly separate.
wenzelm
parents:
21595
diff
changeset

849 
maintained as tags  may be attached any time without affecting the 
fccafa917a68
* Pure: official theorem names and additional comments are now strictly separate.
wenzelm
parents:
21595
diff
changeset

850 
derivation. 
fccafa917a68
* Pure: official theorem names and additional comments are now strictly separate.
wenzelm
parents:
21595
diff
changeset

851 

18020  852 
* Pure: primitive rule lift_rule now takes goal cterm instead of an 
18145  853 
actual goal state (thm). Use Thm.lift_rule (Thm.cprem_of st i) to 
18020  854 
achieve the old behaviour. 
855 

856 
* Pure: the "Goal" constant is now called "prop", supporting a 

857 
slightly more general idea of ``protecting'' metalevel rule 

858 
statements. 

859 

20040
02c59ec2f2e1
* Pure: structure Variable provides operations for proper treatment of fixed/schematic variables;
wenzelm
parents:
20013
diff
changeset

860 
* Pure: Logic.(un)varify only works in a global context, which is now 
02c59ec2f2e1
* Pure: structure Variable provides operations for proper treatment of fixed/schematic variables;
wenzelm
parents:
20013
diff
changeset

861 
enforced instead of silently assumed. INCOMPATIBILITY, may use 
02c59ec2f2e1
* Pure: structure Variable provides operations for proper treatment of fixed/schematic variables;
wenzelm
parents:
20013
diff
changeset

862 
Logic.legacy_(un)varify as temporary workaround. 
02c59ec2f2e1
* Pure: structure Variable provides operations for proper treatment of fixed/schematic variables;
wenzelm
parents:
20013
diff
changeset

863 

20090  864 
* Pure: structure Name provides scalable operations for generating 
865 
internal variable names, notably Name.variants etc. This replaces 

866 
some popular functions from term.ML: 

867 

868 
Term.variant > Name.variant 

869 
Term.variantlist > Name.variant_list (*canonical argument order*) 

870 
Term.invent_names > Name.invent_list 

871 

872 
Note that lowlevel renaming rarely occurs in new code  operations 

873 
from structure Variable are used instead (see below). 

874 

20040
02c59ec2f2e1
* Pure: structure Variable provides operations for proper treatment of fixed/schematic variables;
wenzelm
parents:
20013
diff
changeset

875 
* Pure: structure Variable provides fundamental operations for proper 
02c59ec2f2e1
* Pure: structure Variable provides operations for proper treatment of fixed/schematic variables;
wenzelm
parents:
20013
diff
changeset

876 
treatment of fixed/schematic variables in a context. For example, 
02c59ec2f2e1
* Pure: structure Variable provides operations for proper treatment of fixed/schematic variables;
wenzelm
parents:
20013
diff
changeset

877 
Variable.import introduces fixes for schematics of given facts and 
02c59ec2f2e1
* Pure: structure Variable provides operations for proper treatment of fixed/schematic variables;
wenzelm
parents:
20013
diff
changeset

878 
Variable.export reverses the effect (up to renaming)  this replaces 
02c59ec2f2e1
* Pure: structure Variable provides operations for proper treatment of fixed/schematic variables;
wenzelm
parents:
20013
diff
changeset

879 
various freeze_thaw operations. 
02c59ec2f2e1
* Pure: structure Variable provides operations for proper treatment of fixed/schematic variables;
wenzelm
parents:
20013
diff
changeset

880 

18567  881 
* Pure: structure Goal provides simple interfaces for 
17981
2602be0d99ae
* Legacy goal package: reduced interface to the bare minimum required to keep existing proof scripts running.
wenzelm
parents:
17918
diff
changeset

882 
init/conclude/finish and tactical prove operations (replacing former 
20040
02c59ec2f2e1
* Pure: structure Variable provides operations for proper treatment of fixed/schematic variables;
wenzelm
parents:
20013
diff
changeset

883 
Tactic.prove). Goal.prove is the canonical way to prove results 
02c59ec2f2e1
* Pure: structure Variable provides operations for proper treatment of fixed/schematic variables;
wenzelm
parents:
20013
diff
changeset

884 
within a given context; Goal.prove_global is a degraded version for 
02c59ec2f2e1
* Pure: structure Variable provides operations for proper treatment of fixed/schematic variables;
wenzelm
parents:
20013
diff
changeset

885 
theory level goals, including a global Drule.standard. Note that 
02c59ec2f2e1
* Pure: structure Variable provides operations for proper treatment of fixed/schematic variables;
wenzelm
parents:
20013
diff
changeset

886 
OldGoals.prove_goalw_cterm has long been obsolete, since it is 
02c59ec2f2e1
* Pure: structure Variable provides operations for proper treatment of fixed/schematic variables;
wenzelm
parents:
20013
diff
changeset

887 
illbehaved in a local proof context (e.g. with local fixes/assumes or 
02c59ec2f2e1
* Pure: structure Variable provides operations for proper treatment of fixed/schematic variables;
wenzelm
parents:
20013
diff
changeset

888 
in a locale context). 
17981
2602be0d99ae
* Legacy goal package: reduced interface to the bare minimum required to keep existing proof scripts running.
wenzelm
parents:
17918
diff
changeset

889 

18815
cb778c0ce1b5
Pure/Isar: (un)folded, (un)fold, unfolding support
wenzelm
parents:
18738
diff
changeset

890 
* Isar: simplified treatment of userlevel errors, using exception 
18687  891 
ERROR of string uniformly. Function error now merely raises ERROR, 
18686
cbbc71acf994
* ML/Isar: simplified treatment of userlevel errors;
wenzelm
parents:
18674
diff
changeset

892 
without any side effect on output channels. The Isar toplevel takes 
cbbc71acf994
* ML/Isar: simplified treatment of userlevel errors;
wenzelm
parents:
18674
diff
changeset

893 
care of proper display of ERROR exceptions. ML code may use plain 
cbbc71acf994
* ML/Isar: simplified treatment of userlevel errors;
wenzelm
parents:
18674
diff
changeset

894 
handle/can/try; cat_error may be used to concatenate errors like this: 
cbbc71acf994
* ML/Isar: simplified treatment of userlevel errors;
wenzelm
parents:
18674
diff
changeset

895 

cbbc71acf994
* ML/Isar: simplified treatment of userlevel errors;
wenzelm
parents:
18674
diff
changeset

896 
... handle ERROR msg => cat_error msg "..." 
cbbc71acf994
* ML/Isar: simplified treatment of userlevel errors;
wenzelm
parents:
18674
diff
changeset

897 

cbbc71acf994
* ML/Isar: simplified treatment of userlevel errors;
wenzelm
parents:
18674
diff
changeset

898 
Toplevel ML code (run directly or through the Isar toplevel) may be 
18687  899 
embedded into the Isar toplevel with exception display/debug like 
900 
this: 

18686
cbbc71acf994
* ML/Isar: simplified treatment of userlevel errors;
wenzelm
parents:
18674
diff
changeset

901 

cbbc71acf994
* ML/Isar: simplified treatment of userlevel errors;
wenzelm
parents:
18674
diff
changeset

902 
Isar.toplevel (fn () => ...) 
cbbc71acf994
* ML/Isar: simplified treatment of userlevel errors;
wenzelm
parents:
18674
diff
changeset

903 

cbbc71acf994
* ML/Isar: simplified treatment of userlevel errors;
wenzelm
parents:
18674
diff
changeset

904 
INCOMPATIBILITY, removed special transform_error facilities, removed 
cbbc71acf994
* ML/Isar: simplified treatment of userlevel errors;
wenzelm
parents:
18674
diff
changeset

905 
obsolete variants of userlevel exceptions (ERROR_MESSAGE, 
cbbc71acf994
* ML/Isar: simplified treatment of userlevel errors;
wenzelm
parents:
18674
diff
changeset

906 
Context.PROOF, ProofContext.CONTEXT, Proof.STATE, ProofHistory.FAIL) 
cbbc71acf994
* ML/Isar: simplified treatment of userlevel errors;
wenzelm
parents:
18674
diff
changeset

907 
 use plain ERROR instead. 
cbbc71acf994
* ML/Isar: simplified treatment of userlevel errors;
wenzelm
parents:
18674
diff
changeset

908 

18815
cb778c0ce1b5
Pure/Isar: (un)folded, (un)fold, unfolding support
wenzelm
parents:
18738
diff
changeset

909 
* Isar: theory setup now has type (theory > theory), instead of a 
18722
0888eca0f1be
* ML/Isar: theory setup has type (theory > theory);
wenzelm
parents:
18696
diff
changeset

910 
list. INCOMPATIBILITY, may use #> to compose setup functions. 
0888eca0f1be
* ML/Isar: theory setup has type (theory > theory);
wenzelm
parents:
18696
diff
changeset

911 

18815
cb778c0ce1b5
Pure/Isar: (un)folded, (un)fold, unfolding support
wenzelm
parents:
18738
diff
changeset

912 
* Isar: installed ML toplevel pretty printer for type Proof.context, 
cb778c0ce1b5
Pure/Isar: (un)folded, (un)fold, unfolding support
wenzelm
parents:
18738
diff
changeset

913 
subject to ProofContext.debug/verbose flags. 
cb778c0ce1b5
Pure/Isar: (un)folded, (un)fold, unfolding support
wenzelm
parents:
18738
diff
changeset

914 

cb778c0ce1b5
Pure/Isar: (un)folded, (un)fold, unfolding support
wenzelm
parents:
18738
diff
changeset

915 
* Isar: Toplevel.theory_to_proof admits transactions that modify the 
cb778c0ce1b5
Pure/Isar: (un)folded, (un)fold, unfolding support
wenzelm
parents:
18738
diff
changeset

916 
theory before entering a proof state. Transactions now always see a 
cb778c0ce1b5
Pure/Isar: (un)folded, (un)fold, unfolding support
wenzelm
parents:
18738
diff
changeset

917 
quasifunctional intermediate checkpoint, both in interactive and 
18590
f6a553aa3d81
Pure/Isar: Toplevel.theory_to_proof admits transactions that modify the theory;
wenzelm
parents:
18568
diff
changeset

918 
batch mode. 
18567  919 

17878  920 
* Simplifier: the simpset of a running simplification process now 
921 
contains a proof context (cf. Simplifier.the_context), which is the 

922 
very context that the initial simpset has been retrieved from (by 

17890  923 
simpset_of/local_simpset_of). Consequently, all plugin components 
17878  924 
(solver, looper etc.) may depend on arbitrary proof data. 
925 

926 
* Simplifier.inherit_context inherits the proof context (plus the 

927 
local bounds) of the current simplification process; any simproc 

928 
etc. that calls the Simplifier recursively should do this! Removed 

929 
former Simplifier.inherit_bounds, which is already included here  

17890  930 
INCOMPATIBILITY. Tools based on lowlevel rewriting may even have to 
931 
specify an explicit context using Simplifier.context/theory_context. 

17878  932 

933 
* Simplifier/Classical Reasoner: more abstract interfaces 

934 
change_simpset/claset for modifying the simpset/claset reference of a 

935 
theory; raw versions simpset/claset_ref etc. have been discontinued  

936 
INCOMPATIBILITY. 

937 

18540  938 
* Provers: more generic wrt. syntax of objectlogics, avoid hardwired 
939 
"Trueprop" etc. 

940 

17878  941 

20988
0887d0dd3210
* isabelleprocess: option S (secure mode) disables some critical operations;
wenzelm
parents:
20951
diff
changeset

942 
*** System *** 
0887d0dd3210
* isabelleprocess: option S (secure mode) disables some critical operations;
wenzelm
parents:
20951
diff
changeset

943 

21471
03a5ef1936c5
* settings: ML_IDENTIFIER includes the Isabelle version identifier;
wenzelm
parents:
21462
diff
changeset

944 
* settings: ML_IDENTIFIER  which is appended to user specific heap 
03a5ef1936c5
* settings: ML_IDENTIFIER includes the Isabelle version identifier;
wenzelm
parents:
21462
diff
changeset

945 
locations  now includes the Isabelle version identifier as well. 
03a5ef1936c5
* settings: ML_IDENTIFIER includes the Isabelle version identifier;
wenzelm
parents:
21462
diff
changeset

946 
This simplifies use of multiple Isabelle installations. 
03a5ef1936c5
* settings: ML_IDENTIFIER includes the Isabelle version identifier;
wenzelm
parents:
21462
diff
changeset

947 

20988
0887d0dd3210
* isabelleprocess: option S (secure mode) disables some critical operations;
wenzelm
parents:
20951
diff
changeset

948 
* isabelleprocess: option S (secure mode) disables some critical 
0887d0dd3210
* isabelleprocess: option S (secure mode) disables some critical operations;
wenzelm
parents:
20951
diff
changeset

949 
operations, notably runtime compilation and evaluation of ML source 
0887d0dd3210
* isabelleprocess: option S (secure mode) disables some critical operations;
wenzelm
parents:
20951
diff
changeset

950 
code. 
0887d0dd3210
* isabelleprocess: option S (secure mode) disables some critical operations;
wenzelm
parents:
20951
diff
changeset

951 

17754
58a306d9f736
* Command 'find_theorems': support * wildcard in name: criterion.
wenzelm
parents:
17725
diff
changeset

952 

17720  953 
New in Isabelle2005 (October 2005) 
954 
 

14655
8a95abf87dd3
Pure: considerably improved version of 'constdefs' command;
wenzelm
parents:
14624
diff
changeset

955 

8a95abf87dd3
Pure: considerably improved version of 'constdefs' command;
wenzelm
parents:
14624
diff
changeset

956 
*** General *** 
8a95abf87dd3
Pure: considerably improved version of 'constdefs' command;
wenzelm
parents:
14624
diff
changeset

957 

15130  958 
* Theory headers: the new header syntax for Isar theories is 
959 

960 
theory <name> 

16234  961 
imports <theory1> ... <theoryN> 
962 
uses <file1> ... <fileM> 

15130  963 
begin 
964 

16234  965 
where the 'uses' part is optional. The previous syntax 
966 

967 
theory <name> = <theory1> + ... + <theoryN>: 

968 

16717  969 
will disappear in the next release. Use isatool fixheaders to convert 
970 
existing theory files. Note that there is no change in ancient 

17371  971 
nonIsar theories now, but these will disappear soon. 
15130  972 

15475
fdf9434b04ea
 Proofs are now hidden by default when generating documents
berghofe
parents:
15454
diff
changeset

973 
* Theory loader: parent theories can now also be referred to via 
16234  974 
relative and absolute paths. 
975 

17408
551c9a4dd693
command 'thms_containing' has been discontinued in favour of 'find_theorems';
wenzelm
parents:
17402
diff
changeset

976 
* Command 'find_theorems' searches for a list of criteria instead of a 
551c9a4dd693
command 'thms_containing' has been discontinued in favour of 'find_theorems';
wenzelm
parents:
17402
diff
changeset

977 
list of constants. Known criteria are: intro, elim, dest, name:string, 
551c9a4dd693
command 'thms_containing' has been discontinued in favour of 'find_theorems';
wenzelm
parents:
17402
diff
changeset

978 
simp:term, and any term. Criteria can be preceded by '' to select 
551c9a4dd693
command 'thms_containing' has been discontinued in favour of 'find_theorems';
wenzelm
parents:
17402
diff
changeset

979 
theorems that do not match. Intro, elim, dest select theorems that 
551c9a4dd693
command 'thms_containing' has been discontinued in favour of 'find_theorems';
wenzelm
parents:
17402
diff
changeset

980 
match the current goal, name:s selects theorems whose fully qualified 
551c9a4dd693
command 'thms_containing' has been discontinued in favour of 'find_theorems';
wenzelm
parents:
17402
diff
changeset

981 
name contain s, and simp:term selects all simplification rules whose 
551c9a4dd693
command 'thms_containing' has been discontinued in favour of 'find_theorems';
wenzelm
parents:
17402
diff
changeset

982 
lhs match term. Any other term is interpreted as pattern and selects 
551c9a4dd693
command 'thms_containing' has been discontinued in favour of 'find_theorems';
wenzelm
parents:
17402
diff
changeset

983 
all theorems matching the pattern. Available in ProofGeneral under 
551c9a4dd693
command 'thms_containing' has been discontinued in favour of 'find_theorems';
wenzelm
parents:
17402
diff
changeset

984 
'ProofGeneral > Find Theorems' or Cc Cf. Example: 
16234  985 

17275
44d8fbc2e52d
axclass: name space prefix is now "c_class" instead of just "c";
wenzelm
parents:
17269
diff
changeset

986 
Cc Cf (100) "(_::nat) + _ + _" intro name: "HOL." 
16234  987 

988 
prints the last 100 theorems matching the pattern "(_::nat) + _ + _", 

989 
matching the current goal as introduction rule and not having "HOL." 

990 
in their name (i.e. not being defined in theory HOL). 

16013
3010430d894d
removed find_rewrites (superceded by improved thms_containing);
wenzelm
parents:
16000
diff
changeset

991 

17408
551c9a4dd693
command 'thms_containing' has been discontinued in favour of 'find_theorems';
wenzelm
parents:
17402
diff
changeset

992 
* Command 'thms_containing' has been discontinued in favour of 
551c9a4dd693
command 'thms_containing' has been discontinued in favour of 'find_theorems';
wenzelm
parents:
17402
diff
changeset

993 
'find_theorems'; INCOMPATIBILITY. 
551c9a4dd693
command 'thms_containing' has been discontinued in favour of 'find_theorems';
wenzelm
parents:
17402
diff
changeset

994 

17385  995 
* Communication with Proof General is now 8bit clean, which means that 
996 
Unicode text in UTF8 encoding may be used within theory texts (both 

17408
551c9a4dd693
command 'thms_containing' has been discontinued in favour of 'find_theorems';
wenzelm
parents:
17402
diff
changeset

997 
formal and informal parts). Cf. option U of the Isabelle Proof 
17538  998 
General interface. Here are some simple examples (cf. src/HOL/ex): 
999 

1000 
http://isabelle.in.tum.de/library/HOL/ex/Hebrew.html 

1001 
http://isabelle.in.tum.de/library/HOL/ex/Chinese.html 

17385  1002 

17425  1003 
* Improved efficiency of the Simplifier and, to a lesser degree, the 
1004 
Classical Reasoner. Typical big applications run around 2 times 

1005 
faster. 

1006 

15703  1007 

1008 
*** Document preparation *** 

1009 

16234  1010 
* Commands 'display_drafts' and 'print_drafts' perform simple output 
1011 
of raw sources. Only those symbols that do not require additional 

1012 
LaTeX packages (depending on comments in isabellesym.sty) are 

1013 
displayed properly, everything else is left verbatim. isatool display 

1014 
and isatool print are used as front ends (these are subject to the 

1015 
DVI/PDF_VIEWER and PRINT_COMMAND settings, respectively). 

1016 

17047
e2e2d75bb37b
* Command tags control specific markup of certain regions of text (replaces usedir H);
wenzelm
parents:
17016
diff
changeset

1017 
* Command tags control specific markup of certain regions of text, 
e2e2d75bb37b
* Command tags control specific markup of certain regions of text (replaces usedir H);
wenzelm
parents:
17016
diff
changeset

1018 
notably folding and hiding. Predefined tags include "theory" (for 
e2e2d75bb37b
* Command tags control specific markup of certain regions of text (replaces usedir H);
wenzelm
parents:
17016
diff
changeset

1019 
theory begin and end), "proof" for proof commands, and "ML" for 
e2e2d75bb37b
* Command tags control specific markup of certain regions of text (replaces usedir H);
wenzelm
parents:
17016
diff
changeset

1020 
commands involving ML code; the additional tags "visible" and 
e2e2d75bb37b
* Command tags control specific markup of certain regions of text (replaces usedir H);
wenzelm
parents:
17016
diff
changeset

1021 
"invisible" are unused by default. Users may give explicit tag 
e2e2d75bb37b
* Command tags control specific markup of certain regions of text (replaces usedir H);
wenzelm
parents:
17016
diff
changeset

1022 
specifications in the text, e.g. ''by %invisible (auto)''. The 
e2e2d75bb37b
* Command tags control specific markup of certain regions of text (replaces usedir H);
wenzelm
parents:
17016
diff
changeset

1023 
interpretation of tags is determined by the LaTeX job during document 
e2e2d75bb37b
* Command tags control specific markup of certain regions of text (replaces usedir H);
wenzelm
parents:
17016
diff
changeset

1024 
preparation: see option V of isatool usedir, or options n and t of 
e2e2d75bb37b
* Command tags control specific markup of certain regions of text (replaces usedir H);
wenzelm
parents:
17016
diff
changeset

1025 
isatool document, or even the LaTeX macros \isakeeptag, \isafoldtag, 
e2e2d75bb37b
* Command tags control specific markup of certain regions of text (replaces usedir H);
wenzelm
parents:
17016
diff
changeset

1026 
\isadroptag. 
e2e2d75bb37b
* Command tags control specific markup of certain regions of text (replaces usedir H);
wenzelm
parents:
17016
diff
changeset

1027 

e2e2d75bb37b
* Command tags control specific markup of certain regions of text (replaces usedir H);
wenzelm
parents:
17016
diff
changeset

1028 
Several document versions may be produced at the same time via isatool 
e2e2d75bb37b
* Command tags control specific markup of certain regions of text (replaces usedir H);
wenzelm
parents:
17016
diff
changeset

1029 
usedir (the generated index.html will link all of them). Typical 
e2e2d75bb37b
* Command tags control specific markup of certain regions of text (replaces usedir H);
wenzelm
parents:
17016
diff
changeset

1030 
specifications include ''V document=theory,proof,ML'' to present 
e2e2d75bb37b
* Command tags control specific markup of certain regions of text (replaces usedir H);
wenzelm
parents:
17016
diff
changeset

1031 
theory/proof/ML parts faithfully, ''V outline=/proof,/ML'' to fold 
e2e2d75bb37b
* Command tags control specific markup of certain regions of text (replaces usedir H);
wenzelm
parents:
17016
diff
changeset

1032 
proof and ML commands, and ''V mutilated=theory,proof,ML'' to omit 
e2e2d75bb37b
* Command tags control specific markup of certain regions of text (replaces usedir H);
wenzelm
parents:
17016
diff
changeset

1033 
these parts without any formal replacement text. The Isabelle site 
e2e2d75bb37b
* Command tags control specific markup of certain regions of text (replaces usedir H);
wenzelm
parents:
17016
diff
changeset

1034 
default settings produce ''document'' and ''outline'' versions as 
e2e2d75bb37b
* Command tags control specific markup of certain regions of text (replaces usedir H);
wenzelm
parents:
17016
diff
changeset

1035 
specified above. 
16234  1036 

17402  1037 
* Several new antiquotations: 
15979  1038 

1039 
@{term_type term} prints a term with its type annotated; 

1040 

1041 
@{typeof term} prints the type of a term; 

1042 

16234  1043 
@{const const} is the same as @{term const}, but checks that the 
1044 
argument is a known logical constant; 

15979  1045 

1046 
@{term_style style term} and @{thm_style style thm} print a term or 

16234  1047 
theorem applying a "style" to it 
1048 

17117
e2bed9e82454
* The ML antiquotation prints typechecked ML expressions verbatim.
wenzelm
parents:
17097
diff
changeset

1049 
@{ML text} 
e2bed9e82454
* The ML antiquotation prints typechecked ML expressions verbatim.
wenzelm
parents:
17097
diff
changeset

1050 

16234  1051 
Predefined styles are 'lhs' and 'rhs' printing the lhs/rhs of 
1052 
definitions, equations, inequations etc., 'concl' printing only the 

17393  1053 
conclusion of a metalogical statement theorem, and 'prem1' .. 'prem19' 
16234  1054 
to print the specified premise. TermStyle.add_style provides an ML 
1055 
interface for introducing further styles. See also the "LaTeX Sugar" 

17117
e2bed9e82454
* The ML antiquotation prints typechecked ML expressions verbatim.
wenzelm
parents:
17097
diff
changeset

1056 
document practical applications. The ML antiquotation prints 
e2bed9e82454
* The ML antiquotation prints typechecked ML expressions verbatim.
wenzelm
parents:
17097
diff
changeset

1057 
typechecked ML expressions verbatim. 
16234  1058 

17259
dda237f1d299
Markup commands 'chapter' .. 'text' support optional locale specification;
wenzelm
parents:
17228
diff
changeset

1059 
* Markup commands 'chapter', 'section', 'subsection', 'subsubsection', 
dda237f1d299
Markup commands 'chapter' .. 'text' support optional locale specification;
wenzelm
parents:
17228
diff
changeset

1060 
and 'text' support optional locale specification '(in loc)', which 
17269  1061 
specifies the default context for interpreting antiquotations. For 
1062 
example: 'text (in lattice) {* @{thm inf_assoc}*}'. 

17259
dda237f1d299
Markup commands 'chapter' .. 'text' support optional locale specification;
wenzelm
parents:
17228
diff
changeset

1063 

dda237f1d299
Markup commands 'chapter' .. 'text' support optional locale specification;
wenzelm
parents:
17228
diff
changeset

1064 
* Option 'locale=NAME' of antiquotations specifies an alternative 
dda237f1d299
Markup commands 'chapter' .. 'text' support optional locale specification;
wenzelm
parents:
17228
diff
changeset

1065 
context interpreting the subsequent argument. For example: @{thm 
17269  1066 
[locale=lattice] inf_assoc}. 
17259
dda237f1d299
Markup commands 'chapter' .. 'text' support optional locale specification;
wenzelm
parents:
17228
diff
changeset

1067 

17097
78f1b66f70a4
* Proper output of proof terms within a proof context;
wenzelm
parents:
17095
diff
changeset

1068 
* Proper output of proof terms (@{prf ...} and @{full_prf ...}) within 
78f1b66f70a4
* Proper output of proof terms within a proof context;
wenzelm
parents:
17095
diff
changeset

1069 
a proof context. 
78f1b66f70a4
* Proper output of proof terms within a proof context;
wenzelm
parents:
17095
diff
changeset

1070 

78f1b66f70a4
* Proper output of proof terms within a proof context;
wenzelm
parents:
17095
diff
changeset

1071 
* Proper output of antiquotations for theory commands involving a 
78f1b66f70a4
* Proper output of proof terms within a proof context;
wenzelm
parents:
17095
diff
changeset

1072 
proof context (such as 'locale' or 'theorem (in loc) ...'). 
78f1b66f70a4
* Proper output of proof terms within a proof context;
wenzelm
parents:
17095
diff
changeset

1073 

17193
83708f724822
* Delimiters of outer tokens now produce separate LaTeX macros;
wenzelm
parents:
17189
diff
changeset

1074 
* Delimiters of outer tokens (string etc.) now produce separate LaTeX 
83708f724822
* Delimiters of outer tokens now produce separate LaTeX macros;
wenzelm
parents:
17189
diff
changeset

1075 
macros (\isachardoublequoteopen, isachardoublequoteclose etc.). 
83708f724822
* Delimiters of outer tokens now produce separate LaTeX macros;
wenzelm
parents:
17189
diff
changeset

1076 

83708f724822
* Delimiters of outer tokens now produce separate LaTeX macros;
wenzelm
parents:
17189
diff
changeset

1077 
* isatool usedir: new option C (default true) controls whether option 
83708f724822
* Delimiters of outer tokens now produce separate LaTeX macros;
wenzelm
parents:
17189
diff
changeset

1078 
D should include a copy of the original document directory; C false 
83708f724822
* Delimiters of outer tokens now produce separate LaTeX macros;
wenzelm
parents:
17189
diff
changeset

1079 
prevents unwanted effects such as copying of administrative CVS data. 
83708f724822
* Delimiters of outer tokens now produce separate LaTeX macros;
wenzelm
parents:
17189
diff
changeset

1080 

16234  1081 

1082 
*** Pure *** 

1083 

1084 
* Considerably improved version of 'constdefs' command. Now performs 

1085 
automatic typeinference of declared constants; additional support for 

1086 
local structure declarations (cf. locales and HOL records), see also 

1087 
isarref manual. Potential INCOMPATIBILITY: need to observe strictly 

1088 
sequential dependencies of definitions within a single 'constdefs' 

1089 
section; moreover, the declared name needs to be an identifier. If 

1090 
all fails, consider to fall back on 'consts' and 'defs' separately. 

1091 

1092 
* Improved indexed syntax and implicit structures. First of all, 

1093 
indexed syntax provides a notational device for subscripted 

1094 
application, using the new syntax \<^bsub>term\<^esub> for arbitrary 

1095 
expressions. Secondly, in a local context with structure 

1096 
declarations, number indexes \<^sub>n or the empty index (default 

1097 
number 1) refer to a certain fixed variable implicitly; option 

1098 
show_structs controls printing of implicit structures. Typical 

1099 
applications of these concepts involve record types and locales. 

1100 

1101 
* New command 'no_syntax' removes grammar declarations (and 

1102 
translations) resulting from the given syntax specification, which is 

1103 
interpreted in the same manner as for the 'syntax' command. 

1104 

1105 
* 'Advanced' translation functions (parse_translation etc.) may depend 

1106 
on the signature of the theory context being presently used for 

1107 
parsing/printing, see also isarref manual. 

1108 

16856  1109 
* Improved 'oracle' command provides a typesafe interface to turn an 
1110 
ML expression of type theory > T > term into a primitive rule of 

1111 
type theory > T > thm (i.e. the functionality of Thm.invoke_oracle 

1112 
is already included here); see also FOL/ex/IffExample.thy; 

1113 
INCOMPATIBILITY. 

1114 

17275
44d8fbc2e52d
axclass: name space prefix is now "c_class" instead of just "c";
wenzelm
parents:
17269
diff
changeset

1115 
* axclass: name space prefix for class "c" is now "c_class" (was "c" 
44d8fbc2e52d
axclass: name space prefix is now "c_class" instead of just "c";
wenzelm
parents:
17269
diff
changeset

1116 
before); "cI" is no longer bound, use "c.intro" instead. 
44d8fbc2e52d
axclass: name space prefix is now "c_class" instead of just "c";
wenzelm
parents:
17269
diff
changeset

1117 
INCOMPATIBILITY. This change avoids clashes of fact bindings for 
44d8fbc2e52d
axclass: name space prefix is now "c_class" instead of just "c";
wenzelm
parents:
17269
diff
changeset

1118 
axclasses vs. locales. 
44d8fbc2e52d
axclass: name space prefix is now "c_class" instead of just "c";
wenzelm
parents:
17269
diff
changeset

1119 

16234  1120 
* Improved internal renaming of symbolic identifiers  attach primes 
1121 
instead of base 26 numbers. 

1122 

1123 
* New flag show_question_marks controls printing of leading question 

1124 
marks in schematic variable names. 

1125 

1126 
* In schematic variable names, *any* symbol following \<^isub> or 

1127 
\<^isup> is now treated as part of the base name. For example, the 

1128 
following works without printing of awkward ".0" indexes: 

1129 

1130 
lemma "x\<^isub>1 = x\<^isub>2 ==> x\<^isub>2 = x\<^isub>1" 

1131 
by simp 

1132 

1133 
* Inner syntax includes (*(*nested*) comments*). 

1134 

17548  1135 
* Pretty printer now supports unbreakable blocks, specified in mixfix 
16234  1136 
annotations as "(00...)". 
1137 

1138 
* Clear separation of logical types and nonterminals, where the latter 

1139 
may only occur in 'syntax' specifications or type abbreviations. 

1140 
Before that distinction was only partially implemented via type class 

1141 
"logic" vs. "{}". Potential INCOMPATIBILITY in rare cases of improper 

1142 
use of 'types'/'consts' instead of 'nonterminals'/'syntax'. Some very 

1143 
exotic syntax specifications may require further adaption 

17691  1144 
(e.g. Cube/Cube.thy). 
16234  1145 

1146 
* Removed obsolete type class "logic", use the top sort {} instead. 

1147 
Note that nonlogical types should be declared as 'nonterminals' 

1148 
rather than 'types'. INCOMPATIBILITY for new objectlogic 

1149 
specifications. 

1150 

17095  1151 
* Attributes 'induct' and 'cases': type or set names may now be 
1152 
locally fixed variables as well. 

1153 

16234  1154 
* Simplifier: can now control the depth to which conditional rewriting 
1155 
is traced via the PG menu Isabelle > Settings > Trace Simp Depth 

1156 
Limit. 

1157 

1158 
* Simplifier: simplification procedures may now take the current 

1159 
simpset into account (cf. Simplifier.simproc(_i) / mk_simproc 

1160 
interface), which is very useful for calling the Simplifier 

1161 
recursively. Minor INCOMPATIBILITY: the 'prems' argument of simprocs 

1162 
is gone  use prems_of_ss on the simpset instead. Moreover, the 

1163 
lowlevel mk_simproc no longer applies Logic.varify internally, to 

1164 
allow for use in a context of fixed variables. 

1165 

1166 
* thin_tac now works even if the assumption being deleted contains !! 

1167 
or ==>. More generally, erule now works even if the major premise of 

1168 
the elimination rule contains !! or ==>. 

1169 

17597  1170 
* Method 'rules' has been renamed to 'iprover'. INCOMPATIBILITY. 
17590  1171 

16234  1172 
* Reorganized bootstrapping of the Pure theories; CPure is now derived 
1173 
from Pure, which contains all common declarations already. Both 

1174 
theories are defined via plain Isabelle/Isar .thy files. 

1175 
INCOMPATIBILITY: elements of CPure (such as the CPure.intro / 

1176 
CPure.elim / CPure.dest attributes) now appear in the Pure name space; 

1177 
use isatool fixcpure to adapt your theory and ML sources. 

1178 

1179 
* New syntax 'name(ij, i, i, ...)' for referring to specific 

1180 
selections of theorems in named facts via index ranges. 

1181 

17097
78f1b66f70a4
* Proper output of proof terms within a proof context;
wenzelm
parents:
17095
diff
changeset

1182 
* 'print_theorems': in theory mode, really print the difference 
78f1b66f70a4
* Proper output of proof terms within a proof context;
wenzelm
parents:
17095
diff
changeset

1183 
wrt. the last state (works for interactive theory development only), 
78f1b66f70a4
* Proper output of proof terms within a proof context;
wenzelm
parents:
17095
diff
changeset

1184 
in proof mode print all local facts (cf. 'print_facts'); 
78f1b66f70a4
* Proper output of proof terms within a proof context;
wenzelm
parents:
17095
diff
changeset

1185 

17397  1186 
* 'hide': option '(open)' hides only base names. 
1187 

17275
44d8fbc2e52d
axclass: name space prefix is now "c_class" instead of just "c";
wenzelm
parents:
17269
diff
changeset

1188 
* More efficient treatment of intermediate checkpoints in interactive 
44d8fbc2e52d
axclass: name space prefix is now "c_class" instead of just "c";
wenzelm
parents:
17269
diff
changeset

1189 
theory development. 
44d8fbc2e52d
axclass: name space prefix is now "c_class" instead of just "c";
wenzelm
parents:
17269
diff
changeset

1190 

17663
28be54ff74f8
Added entries for code_module, code_library, and value.
berghofe
parents:
17641
diff
changeset

1191 
* Code generator is now invoked via code_module (incremental code 
17664  1192 
generation) and code_library (modular code generation, ML structures 
1193 
for each theory). INCOMPATIBILITY: new keywords 'file' and 'contains' 

1194 
must be quoted when used as identifiers. 

1195 

1196 
* New 'value' command for reading, evaluating and printing terms using 

1197 
the code generator. INCOMPATIBILITY: command keyword 'value' must be 

1198 
quoted when used as identifier. 

17663
28be54ff74f8
Added entries for code_module, code_library, and value.
berghofe
parents:
17641
diff
changeset

1199 

16234  1200 

1201 
*** Locales *** 

17095  1202 

17385  1203 
* New commands for the interpretation of locale expressions in 
1204 
theories (1), locales (2) and proof contexts (3). These generate 

1205 
proof obligations from the expression specification. After the 

1206 
obligations have been discharged, theorems of the expression are added 

1207 
to the theory, target locale or proof context. The synopsis of the 

1208 
commands is a follows: 

1209 

17095  1210 
(1) interpretation expr inst 
1211 
(2) interpretation target < expr 

1212 
(3) interpret expr inst 

17385  1213 

17095  1214 
Interpretation in theories and proof contexts require a parameter 
1215 
instantiation of terms from the current context. This is applied to 

17385  1216 
specifications and theorems of the interpreted expression. 
1217 
Interpretation in locales only permits parameter renaming through the 

1218 
locale expression. Interpretation is smart in that interpretations 

1219 
that are active already do not occur in proof obligations, neither are 

1220 
instantiated theorems stored in duplicate. Use 'print_interps' to 

1221 
inspect active interpretations of a particular locale. For details, 

17436  1222 
see the Isar Reference manual. Examples can be found in 
1223 
HOL/Finite_Set.thy and HOL/Algebra/UnivPoly.thy. 

16234  1224 

1225 
INCOMPATIBILITY: former 'instantiate' has been withdrawn, use 

1226 
'interpret' instead. 

1227 

17385  1228 
* New context element 'constrains' for adding type constraints to 
1229 
parameters. 

1230 

1231 
* Context expressions: renaming of parameters with syntax 

1232 
redeclaration. 

17095  1233 

1234 
* Locale declaration: 'includes' disallowed. 

1235 

16234  1236 
* Proper static binding of attribute syntax  i.e. types / terms / 
1237 
facts mentioned as arguments are always those of the locale definition 

1238 
context, independently of the context of later invocations. Moreover, 

1239 
locale operations (renaming and type / term instantiation) are applied 

1240 
to attribute arguments as expected. 

1241 

1242 
INCOMPATIBILITY of the ML interface: always pass Attrib.src instead of 

1243 
actual attributes; rare situations may require Attrib.attribute to 

1244 
embed those attributes into Attrib.src that lack concrete syntax. 

1245 
Attribute implementations need to cooperate properly with the static 

1246 
binding mechanism. Basic parsers Args.XXX_typ/term/prop and 

1247 
Attrib.XXX_thm etc. already do the right thing without further 

1248 
intervention. Only unusual applications  such as "where" or "of" 

1249 
(cf. src/Pure/Isar/attrib.ML), which process arguments depending both 

1250 
on the context and the facts involved  may have to assign parsed 

1251 
values to argument tokens explicitly. 

1252 

1253 
* Changed parameter management in theorem generation for long goal 

1254 
statements with 'includes'. INCOMPATIBILITY: produces a different 

1255 
theorem statement in rare situations. 

1256 

17228  1257 
* Locale inspection command 'print_locale' omits notes elements. Use 
1258 
'print_locale!' to have them included in the output. 

1259 

16234  1260 

1261 
*** Provers *** 

1262 

1263 
* Provers/hypsubst.ML: improved version of the subst method, for 

1264 
singlestep rewriting: it now works in bound variable contexts. New is 

1265 
'subst (asm)', for rewriting an assumption. INCOMPATIBILITY: may 

1266 
rewrite a different subterm than the original subst method, which is 

1267 
still available as 'simplesubst'. 

1268 

1269 
* Provers/quasi.ML: new transitivity reasoners for transitivity only 

1270 
and quasi orders. 

1271 

1272 
* Provers/trancl.ML: new transitivity reasoner for transitive and 

1273 
reflexivetransitive closure of relations. 

1274 

1275 
* Provers/blast.ML: new reference depth_limit to make blast's depth 

1276 
limit (previously hardcoded with a value of 20) userdefinable. 

1277 

1278 
* Provers/simplifier.ML has been moved to Pure, where Simplifier.setup 

1279 
is peformed already. Objectlogics merely need to finish their 

1280 
initial simpset configuration as before. INCOMPATIBILITY. 

15703  1281 

15475
fdf9434b04ea
 Proofs are now hidden by default when generating documents
berghofe
parents:
15454
diff
changeset

1282 

14700
2f885b7e5ba7
reimplementation of HOL records; only one type is created for
schirmer
parents:
14699
diff
changeset

1283 
*** HOL *** 
2f885b7e5ba7
reimplementation of HOL records; only one type is created for
schirmer
parents:
14699
diff
changeset

1284 

16234  1285 
* Symbolic syntax of Hilbert Choice Operator is now as follows: 
14878  1286 

1287 
syntax (epsilon) 

1288 
"_Eps" :: "[pttrn, bool] => 'a" ("(3\<some>_./ _)" [0, 10] 10) 

1289 

16234  1290 
The symbol \<some> is displayed as the alternative epsilon of LaTeX 
1291 
and xsymbol; use option 'm epsilon' to get it actually printed. 

1292 
Moreover, the mathematically important symbolic identifier \<epsilon> 

1293 
becomes available as variable, constant etc. INCOMPATIBILITY, 

1294 

1295 
* "x > y" abbreviates "y < x" and "x >= y" abbreviates "y <= x". 

1296 
Similarly for all quantifiers: "ALL x > y" etc. The xsymbol for >= 

17371  1297 
is \<ge>. New transitivity rules have been added to HOL/Orderings.thy to 
17016
73c74cb1d744
mentioned change to exp_ge_add_one_self, new transitivity rules
avigad
parents:
16997
diff
changeset

1298 
support corresponding Isar calculations. 
16234  1299 

1300 
* "{x:A. P}" abbreviates "{x. x:A & P}", and similarly for "\<in>" 

1301 
instead of ":". 

1302 

1303 
* theory SetInterval: changed the syntax for open intervals: 

1304 

1305 
Old New 

1306 
{..n(} {..<n} 

1307 
{)n..} {n<..} 

1308 
{m..n(} {m..<n} 

1309 
{)m..n} {m<..n} 

1310 
{)m..n(} {m<..<n} 

1311 

1312 
The old syntax is still supported but will disappear in the next 

1313 
release. For conversion use the following Emacs search and replace 

1314 
patterns (these are not perfect but work quite well): 

15046  1315 

1316 
{)\([^\.]*\)\.\. > {\1<\.\.} 

1317 
\.\.\([^(}]*\)(} > \.\.<\1} 

1318 

17533  1319 
* Theory Commutative_Ring (in Library): method comm_ring for proving 
1320 
equalities in commutative rings; method 'algebra' provides a generic 

1321 
interface. 

17389
b4743198b939
Method comm_ring for proving equalities in commutative rings.
wenzelm
parents:
17385
diff
changeset

1322 

b4743198b939
Method comm_ring for proving equalities in commutative rings.
wenzelm
parents:
17385
diff
changeset

1323 
* Theory Finite_Set: changed the syntax for 'setsum', summation over 
16234  1324 
finite sets: "setsum (%x. e) A", which used to be "\<Sum>x:A. e", is 
17371  1325 
now either "SUM x:A. e" or "\<Sum>x \<in> A. e". The bound variable can 
17189  1326 
be a tuple pattern. 
16234  1327 

1328 
Some new syntax forms are available: 

1329 

1330 
"\<Sum>x  P. e" for "setsum (%x. e) {x. P}" 

1331 
"\<Sum>x = a..b. e" for "setsum (%x. e) {a..b}" 

1332 
"\<Sum>x = a..<b. e" for "setsum (%x. e) {a..<b}" 

1333 
"\<Sum>x < k. e" for "setsum (%x. e) {..<k}" 

1334 

1335 
The latter form "\<Sum>x < k. e" used to be based on a separate 

1336 
function "Summation", which has been discontinued. 

1337 

1338 
* theory Finite_Set: in structured induction proofs, the insert case 

1339 
is now 'case (insert x F)' instead of the old counterintuitive 'case 

1340 
(insert F x)'. 

1341 

1342 
* The 'refute' command has been extended to support a much larger 

1343 
fragment of HOL, including axiomatic type classes, constdefs and 

1344 
typedefs, inductive datatypes and recursion. 

1345 

17700  1346 
* New tactics 'sat' and 'satx' to prove propositional tautologies. 
1347 
Requires zChaff with proof generation to be installed. See 

1348 
HOL/ex/SAT_Examples.thy for examples. 

17619  1349 

16234  1350 
* Datatype induction via method 'induct' now preserves the name of the 
1351 
induction variable. For example, when proving P(xs::'a list) by 

1352 
induction on xs, the induction step is now P(xs) ==> P(a#xs) rather 

1353 
than P(list) ==> P(a#list) as previously. Potential INCOMPATIBILITY 

1354 
in unstructured proof scripts. 

1355 

1356 
* Reworked implementation of records. Improved scalability for 

1357 
records with many fields, avoiding performance problems for type 

1358 
inference. Records are no longer composed of nested field types, but 

1359 
of nested extension types. Therefore the record type only grows linear 

1360 
in the number of extensions and not in the number of fields. The 

1361 
toplevel (users) view on records is preserved. Potential 

1362 
INCOMPATIBILITY only in strange cases, where the theory depends on the 

1363 
old record representation. The type generated for a record is called 

1364 
<record_name>_ext_type. 

1365 

1366 
Flag record_quick_and_dirty_sensitive can be enabled to skip the 

1367 
proofs triggered by a record definition or a simproc (if 

1368 
quick_and_dirty is enabled). Definitions of large records can take 

1369 
quite long. 

1370 

1371 
New simproc record_upd_simproc for simplification of multiple record 

1372 
updates enabled by default. Moreover, trivial updates are also 

1373 
removed: r(x := x r) = r. INCOMPATIBILITY: old proofs break 

1374 
occasionally, since simplification is more powerful by default. 

1375 

17275
44d8fbc2e52d
axclass: name space prefix is now "c_class" instead of just "c";
wenzelm
parents:
17269
diff
changeset

1376 
* typedef: proper support for polymorphic sets, which contain extra 
44d8fbc2e52d
axclass: name space prefix is now "c_class" instead of just "c";
wenzelm
parents:
17269
diff
changeset

1377 
typevariables in the term. 
44d8fbc2e52d
axclass: name space prefix is now "c_class" instead of just "c";
wenzelm
parents:
17269
diff
changeset

1378 

16234  1379 
* Simplifier: automatically reasons about transitivity chains 
1380 
involving "trancl" (r^+) and "rtrancl" (r^*) by setting up tactics 

1381 
provided by Provers/trancl.ML as additional solvers. INCOMPATIBILITY: 

1382 
old proofs break occasionally as simplification may now solve more 

1383 
goals than previously. 

1384 

1385 
* Simplifier: converts x <= y into x = y if assumption y <= x is 

1386 
present. Works for all partial orders (class "order"), in particular 

1387 
numbers and sets. For linear orders (e.g. numbers) it treats ~ x < y 

1388 
just like y <= x. 

1389 

1390 
* Simplifier: new simproc for "let x = a in f x". If a is a free or 

1391 
bound variable or a constant then the let is unfolded. Otherwise 

1392 
first a is simplified to b, and then f b is simplified to g. If 

1393 
possible we abstract b from g arriving at "let x = b in h x", 

1394 
otherwise we unfold the let and arrive at g. The simproc can be 

1395 
enabled/disabled by the reference use_let_simproc. Potential 

1396 
INCOMPATIBILITY since simplification is more powerful by default. 

15776  1397 

16563  1398 
* Classical reasoning: the meson method now accepts theorems as arguments. 
1399 

17595  1400 
* Prover support: prerelease of the IsabelleATP linkup, which runs background 
1401 
jobs to provide advice on the provability of subgoals. 

1402 

16891  1403 
* Theory OrderedGroup and Ring_and_Field: various additions and 
1404 
improvements to faciliate calculations involving equalities and 

1405 
inequalities. 

1406 

1407 
The following theorems have been eliminated or modified 

1408 
(INCOMPATIBILITY): 

16888  1409 

1410 
abs_eq now named abs_of_nonneg 

17371  1411 
abs_of_ge_0 now named abs_of_nonneg 
1412 
abs_minus_eq now named abs_of_nonpos 

16888  1413 
imp_abs_id now named abs_of_nonneg 
1414 
imp_abs_neg_id now named abs_of_nonpos 

1415 
mult_pos now named mult_pos_pos 

1416 
mult_pos_le now named mult_nonneg_nonneg 
