forked from object-logics/isabelle_para
-
Notifications
You must be signed in to change notification settings - Fork 0
/
NEWS
14868 lines (11392 loc) · 584 KB
/
NEWS
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
Isabelle NEWS -- history of user-relevant changes
=================================================
(Note: Isabelle/jEdit shows a tree-view of the NEWS file in Sidekick.)
New in this Isabelle version
----------------------------
*** General ***
* Marginal comments need to be written exclusively in the new-style form
"\<comment> \<open>text\<close>", old ASCII variants like "-- {* ... *}" are no longer
supported. INCOMPATIBILITY, use the command-line tool "isabelle
update_comments" to update existing theory files.
* The "op <infix-op>" syntax for infix operators has been replaced by
"(<infix-op>)". If <infix-op> begins or ends with a "*", there needs to
be a space between the "*" and the corresponding parenthesis.
INCOMPATIBILITY.
There is an Isabelle tool "update_op" that converts theory and ML files
to the new syntax. Because it is based on regular expression matching,
the result may need a bit of manual postprocessing. Invoking "isabelle
update_op" converts all files in the current directory (recursively).
In case you want to exclude conversion of ML files (because the tool
frequently also converts ML's "op" syntax), use option "-m".
* The old 'def' command has been discontinued (legacy since
Isbelle2016-1). INCOMPATIBILITY, use 'define' instead -- usually with
object-logic equality or equivalence.
* Session-qualified theory names are mandatory: it is no longer possible
to refer to unqualified theories from the parent session.
INCOMPATIBILITY for old developments that have not been updated to
Isabelle2017 yet (using the "isabelle imports" tool).
* Theory header 'abbrevs' specifications need to be separated by 'and'.
INCOMPATIBILITY.
* Only the most fundamental theory names are global, usually the entry
points to major logic sessions: Pure, Main, Complex_Main, HOLCF, IFOL,
FOL, ZF, ZFC etc. INCOMPATIBILITY, need to use qualified names for
formerly global "HOL-Probability.Probability" and "HOL-SPARK.SPARK".
* Command 'external_file' declares the formal dependency on the given
file name, such that the Isabelle build process knows about it, but
without specific Prover IDE management.
* Session ROOT entries no longer allow specification of 'files'. Rare
INCOMPATIBILITY, use command 'external_file' within a proper theory
context.
* Session root directories may be specified multiple times: each
accessible ROOT file is processed only once. This facilitates
specification of $ISABELLE_HOME_USER/ROOTS or command-line options like
-d or -D for "isabelle build" and "isabelle jedit". Example:
isabelle build -D '~~/src/ZF'
* The command 'display_drafts' has been discontinued. INCOMPATIBILITY,
use action "isabelle.draft" (or "print") in Isabelle/jEdit instead.
* Isabelle symbol "\<hyphen>" is rendered as explicit Unicode hyphen U+2010, to
avoid unclear meaning of the old "soft hyphen" U+00AD. Rare
INCOMPATIBILITY, e.g. copy-paste of historic Isabelle HTML output.
*** Isabelle/jEdit Prover IDE ***
* System options "spell_checker_include" and "spell_checker_exclude"
supersede former "spell_checker_elements" to determine regions of text
that are subject to spell-checking. Minor INCOMPATIBILITY.
* PIDE markup for session ROOT files: allows to complete session names,
follow links to theories and document files etc.
* Completion supports theory header imports, using theory base name.
E.g. "Prob" may be completed to "HOL-Probability.Probability".
* The command-line tool "isabelle jedit" provides more flexible options
for session selection:
- options -P opens the parent session image of -l
- options -A and -B modify the meaning of -l to produce a base
image on the spot, based on the specified ancestor (or parent)
- option -F focuses on the specified logic session
- option -R has changed: it only opens the session ROOT entry
- option -S sets up the development environment to edit the
specified session: it abbreviates -B -F -R -l
Examples:
isabelle jedit -d '$AFP' -S Formal_SSA -A HOL
isabelle jedit -d '$AFP' -S Formal_SSA -A HOL-Analysis
* Named control symbols (without special Unicode rendering) are shown as
bold-italic keyword. This is particularly useful for the short form of
antiquotations with control symbol: \<^name>\<open>argument\<close>. The action
"isabelle.antiquoted_cartouche" turns an antiquotation with 0 or 1
arguments into this format.
* Completion provides templates for named symbols with arguments,
e.g. "\<comment> \<open>ARGUMENT\<close>" or "\<^emph>\<open>ARGUMENT\<close>".
* Bibtex database files (.bib) are semantically checked.
* Action "isabelle.preview" is able to present more file formats,
notably bibtex database files and ML files.
* Action "isabelle.draft" is similar to "isabelle.preview", but shows a
plain-text document draft.
* When loading text files, the Isabelle symbols encoding UTF-8-Isabelle
is only used if there is no conflict with existing Unicode sequences in
the file. Otherwise, the fallback encoding is plain UTF-8 and Isabelle
symbols remain in literal \<symbol> form. This avoids accidental loss of
Unicode content when saving the file.
*** Isabelle/VSCode Prover IDE ***
* HTML preview of theories and other file-formats similar to
Isabelle/jEdit.
*** Document preparation ***
* Formal comments work uniformly in outer syntax, inner syntax (term
language), Isabelle/ML and some other embedded languages of Isabelle.
See also "Document comments" in the isar-ref manual. The following forms
are supported:
- marginal text comment: \<comment> \<open>\<dots>\<close>
- canceled source: \<^cancel>\<open>\<dots>\<close>
- raw LaTeX: \<^latex>\<open>\<dots>\<close>
* Embedded languages such as inner syntax and ML may contain formal
comments of the form "\<comment> \<open>text\<close>". As in marginal comments of outer
syntax, antiquotations are interpreted wrt. the presentation context of
the enclosing command.
* Outside of the inner theory body, the default presentation context is
theory Pure. Thus elementary antiquotations may be used in markup
commands (e.g. 'chapter', 'section', 'text') and formal comments.
* System option "document_tags" specifies a default for otherwise
untagged commands. This is occasionally useful to control the global
visibility of commands via session options (e.g. in ROOT).
* Document markup commands ('section', 'text' etc.) are implicitly
tagged as "document" and visible by default. This avoids the application
of option "document_tags" to these commands.
* Isabelle names are mangled into LaTeX macro names to allow the full
identifier syntax with underscore, prime, digits. This is relevant for
antiquotations in control symbol notation, e.g. \<^const_name> becomes
\isactrlconstUNDERSCOREname.
* Document antiquotation @{cite} now checks the given Bibtex entries
against the Bibtex database files -- only in batch-mode session builds.
* Document antiquotation @{session name} checks and prints the given
session name verbatim.
* Document preparation with skip_proofs option now preserves the content
more accurately: only terminal proof steps ('by' etc.) are skipped.
* Command-line tool "isabelle document" has been re-implemented in
Isabelle/Scala, with simplified arguments and explicit errors from the
latex and bibtex process. Minor INCOMPATIBILITY.
*** HOL ***
* A new command parametric_constant for proving parametricity of
non-recursive definitions. For constants that are not fully parametric
the command will infer conditions on relations (e.g., bi_unique,
bi_total, or type class conditions such as "respects 0") sufficient for
parametricity. See ~~/src/HOL/ex/Conditional_Parametricity_Examples for
some examples.
* SMT module:
- The 'smt_oracle' option is now necessary when using the 'smt' method
with a solver other than Z3. INCOMPATIBILITY.
- The encoding to first-order logic is now more complete in the
presence of higher-order quantifiers. An 'smt_explicit_application'
option has been added to control this. INCOMPATIBILITY.
* Datatypes:
- The legacy command 'old_datatype', provided by
'~~/src/HOL/Library/Old_Datatype.thy', has been removed. INCOMPATIBILITY.
* Theory HOL-Computational_Algebra.Polynomial_Factorial does not provide
instances of rat, real, complex as factorial rings etc. Import
HOL-Computational_Algebra.Field_as_Ring explicitly in case of need.
INCOMPATIBILITY.
* Fact mod_mult_self4 (on nat) renamed to mod_mult_self3', to avoid
clash with fact mod_mult_self4 (on more generic semirings).
INCOMPATIBILITY.
* Facts sum.commute(_restrict) and prod.commute(_restrict) renamed to
sum.swap(_restrict) and prod.swap(_restrict), to avoid name clashes on
interpretation of abstract locales. INCOMPATIBILITY.
* Predicate pairwise_coprime abolished, use "pairwise coprime" instead.
INCOMPATIBILITY.
* HOL-Algebra: renamed (^) to [^]
* Session HOL-Analysis: Moebius functions and the Riemann mapping
theorem.
* Class linordered_semiring_1 covers zero_less_one also, ruling out
pathologic instances. Minor INCOMPATIBILITY.
* Removed nat-int transfer machinery. Rare INCOMPATIBILITY.
* Predicate coprime is now a real definition, not a mere
abbreviation. INCOMPATIBILITY.
* Code generation: Code generation takes an explicit option
"case_insensitive" to accomodate case-insensitive file systems.
*** System ***
* The command-line tool "isabelle update_comments" normalizes formal
comments in outer syntax as follows: \<comment> \<open>text\<close> (whith a single space to
approximate the appearance in document output). This is more specific
than former "isabelle update_cartouches -c": the latter tool option has
been discontinued.
* Session ROOT entry: empty 'document_files' means there is no document
for this session. There is no need to specify options [document = false]
anymore.
* The command-line tool "isabelle mkroot" now always produces a document
outline: its options have been adapted accordingly. INCOMPATIBILITY.
* The command-line tool "isabelle mkroot -I" initializes a Mercurial
repository for the generated session files.
* Linux and Windows/Cygwin is for x86_64 only. Old 32bit platform
support has been discontinued.
* Mac OS X 10.10 Yosemite is now the baseline version; Mavericks is no
longer supported.
* Java runtime is for x86_64 only. Corresponding Isabelle settings have
been renamed to ISABELLE_TOOL_JAVA_OPTIONS and JEDIT_JAVA_OPTIONS,
instead of former 32/64 variants. INCOMPATIBILITY.
* Command-line tool "isabelle build" supports new options:
- option -B NAME: include session NAME and all descendants
- option -S: only observe changes of sources, not heap images
- option -f: forces a fresh build
* Command-line tool "isabelle build" takes "condition" options with the
corresponding environment values into account, when determining the
up-to-date status of a session.
* Command-line tool "isabelle imports -I" also reports actual session
imports. This helps to minimize the session dependency graph.
* Update to current Poly/ML 5.7.1 with slightly improved performance and
PIDE markup for identifier bindings.
* ISABELLE_LATEX and ISABELLE_PDFLATEX now include platform-specific
options for improved error reporting. Potential INCOMPATIBILITY with
unusual LaTeX installations, may have to adapt these settings.
New in Isabelle2017 (October 2017)
----------------------------------
*** General ***
* Experimental support for Visual Studio Code (VSCode) as alternative
Isabelle/PIDE front-end, see also
https://marketplace.visualstudio.com/items?itemName=makarius.Isabelle2017
VSCode is a new type of application that continues the concepts of
"programmer's editor" and "integrated development environment" towards
fully semantic editing and debugging -- in a relatively light-weight
manner. Thus it fits nicely on top of the Isabelle/PIDE infrastructure.
Technically, VSCode is based on the Electron application framework
(Node.js + Chromium browser + V8), which is implemented in JavaScript
and TypeScript, while Isabelle/VSCode mainly consists of Isabelle/Scala
modules around a Language Server implementation.
* Theory names are qualified by the session name that they belong to.
This affects imports, but not the theory name space prefix (which is
just the theory base name as before).
In order to import theories from other sessions, the ROOT file format
provides a new 'sessions' keyword. In contrast, a theory that is
imported in the old-fashioned manner via an explicit file-system path
belongs to the current session, and might cause theory name conflicts
later on. Theories that are imported from other sessions are excluded
from the current session document. The command-line tool "isabelle
imports" helps to update theory imports.
* The main theory entry points for some non-HOL sessions have changed,
to avoid confusion with the global name "Main" of the session HOL. This
leads to the follow renamings:
CTT/Main.thy ~> CTT/CTT.thy
ZF/Main.thy ~> ZF/ZF.thy
ZF/Main_ZF.thy ~> ZF/ZF.thy
ZF/Main_ZFC.thy ~> ZF/ZFC.thy
ZF/ZF.thy ~> ZF/ZF_Base.thy
INCOMPATIBILITY.
* Commands 'alias' and 'type_alias' introduce aliases for constants and
type constructors, respectively. This allows adhoc changes to name-space
accesses within global or local theory contexts, e.g. within a 'bundle'.
* Document antiquotations @{prf} and @{full_prf} output proof terms
(again) in the same way as commands 'prf' and 'full_prf'.
* Computations generated by the code generator can be embedded directly
into ML, alongside with @{code} antiquotations, using the following
antiquotations:
@{computation ... terms: ... datatypes: ...} :
((term -> term) -> 'ml option -> 'a) -> Proof.context -> term -> 'a
@{computation_conv ... terms: ... datatypes: ...} :
(Proof.context -> 'ml -> conv) -> Proof.context -> conv
@{computation_check terms: ... datatypes: ...} : Proof.context -> conv
See src/HOL/ex/Computations.thy,
src/HOL/Decision_Procs/Commutative_Ring.thy and
src/HOL/Decision_Procs/Reflective_Field.thy for examples and the
tutorial on code generation.
*** Prover IDE -- Isabelle/Scala/jEdit ***
* Session-qualified theory imports allow the Prover IDE to process
arbitrary theory hierarchies independently of the underlying logic
session image (e.g. option "isabelle jedit -l"), but the directory
structure needs to be known in advance (e.g. option "isabelle jedit -d"
or a line in the file $ISABELLE_HOME_USER/ROOTS).
* The PIDE document model maintains file content independently of the
status of jEdit editor buffers. Reloading jEdit buffers no longer causes
changes of formal document content. Theory dependencies are always
resolved internally, without the need for corresponding editor buffers.
The system option "jedit_auto_load" has been discontinued: it is
effectively always enabled.
* The Theories dockable provides a "Purge" button, in order to restrict
the document model to theories that are required for open editor
buffers.
* The Theories dockable indicates the overall status of checking of each
entry. When all forked tasks of a theory are finished, the border is
painted with thick lines; remaining errors in this situation are
represented by a different border color.
* Automatic indentation is more careful to avoid redundant spaces in
intermediate situations. Keywords are indented after input (via typed
characters or completion); see also option "jedit_indent_input".
* Action "isabelle.preview" opens an HTML preview of the current theory
document in the default web browser.
* Command-line invocation "isabelle jedit -R -l LOGIC" opens the ROOT
entry of the specified logic session in the editor, while its parent is
used for formal checking.
* The main Isabelle/jEdit plugin may be restarted manually (using the
jEdit Plugin Manager), as long as the "Isabelle Base" plugin remains
enabled at all times.
* Update to current jedit-5.4.0.
*** Pure ***
* Deleting the last code equations for a particular function using
[code del] results in function with no equations (runtime abort) rather
than an unimplemented function (generation time abort). Use explicit
[[code drop:]] to enforce the latter. Minor INCOMPATIBILITY.
* Proper concept of code declarations in code.ML:
- Regular code declarations act only on the global theory level, being
ignored with warnings if syntactically malformed.
- Explicitly global code declarations yield errors if syntactically
malformed.
- Default code declarations are silently ignored if syntactically
malformed.
Minor INCOMPATIBILITY.
* Clarified and standardized internal data bookkeeping of code
declarations: history of serials allows to track potentially
non-monotonous declarations appropriately. Minor INCOMPATIBILITY.
*** HOL ***
* The Nunchaku model finder is now part of "Main".
* SMT module:
- A new option, 'smt_nat_as_int', has been added to translate 'nat' to
'int' and benefit from the SMT solver's theory reasoning. It is
disabled by default.
- The legacy module "src/HOL/Library/Old_SMT.thy" has been removed.
- Several small issues have been rectified in the 'smt' command.
* (Co)datatype package: The 'size_gen_o_map' lemma is no longer
generated for datatypes with type class annotations. As a result, the
tactic that derives it no longer fails on nested datatypes. Slight
INCOMPATIBILITY.
* Command and antiquotation "value" with modified default strategy:
terms without free variables are always evaluated using plain evaluation
only, with no fallback on normalization by evaluation. Minor
INCOMPATIBILITY.
* Theories "GCD" and "Binomial" are already included in "Main" (instead
of "Complex_Main").
* Constant "surj" is a full input/output abbreviation (again).
Minor INCOMPATIBILITY.
* Dropped aliasses RangeP, DomainP for Rangep, Domainp respectively.
INCOMPATIBILITY.
* Renamed ii to imaginary_unit in order to free up ii as a variable
name. The syntax \<i> remains available. INCOMPATIBILITY.
* Dropped abbreviations transP, antisymP, single_valuedP; use constants
transp, antisymp, single_valuedp instead. INCOMPATIBILITY.
* Constant "subseq" in Topological_Spaces has been removed -- it is
subsumed by "strict_mono". Some basic lemmas specific to "subseq" have
been renamed accordingly, e.g. "subseq_o" -> "strict_mono_o" etc.
* Theory List: "sublist" renamed to "nths" in analogy with "nth", and
"sublisteq" renamed to "subseq". Minor INCOMPATIBILITY.
* Theory List: new generic function "sorted_wrt".
* Named theorems mod_simps covers various congruence rules concerning
mod, replacing former zmod_simps. INCOMPATIBILITY.
* Swapped orientation of congruence rules mod_add_left_eq,
mod_add_right_eq, mod_add_eq, mod_mult_left_eq, mod_mult_right_eq,
mod_mult_eq, mod_minus_eq, mod_diff_left_eq, mod_diff_right_eq,
mod_diff_eq. INCOMPATIBILITY.
* Generalized some facts:
measure_induct_rule
measure_induct
zminus_zmod ~> mod_minus_eq
zdiff_zmod_left ~> mod_diff_left_eq
zdiff_zmod_right ~> mod_diff_right_eq
zmod_eq_dvd_iff ~> mod_eq_dvd_iff
INCOMPATIBILITY.
* Algebraic type class hierarchy of euclidean (semi)rings in HOL:
euclidean_(semi)ring, euclidean_(semi)ring_cancel,
unique_euclidean_(semi)ring; instantiation requires provision of a
euclidean size.
* Theory "HOL-Number_Theory.Euclidean_Algorithm" has been reworked:
- Euclidean induction is available as rule eucl_induct.
- Constants Euclidean_Algorithm.gcd, Euclidean_Algorithm.lcm,
Euclidean_Algorithm.Gcd and Euclidean_Algorithm.Lcm allow
easy instantiation of euclidean (semi)rings as GCD (semi)rings.
- Coefficients obtained by extended euclidean algorithm are
available as "bezout_coefficients".
INCOMPATIBILITY.
* Theory "Number_Theory.Totient" introduces basic notions about Euler's
totient function previously hidden as solitary example in theory
Residues. Definition changed so that "totient 1 = 1" in agreement with
the literature. Minor INCOMPATIBILITY.
* New styles in theory "HOL-Library.LaTeXsugar":
- "dummy_pats" for printing equations with "_" on the lhs;
- "eta_expand" for printing eta-expanded terms.
* Theory "HOL-Library.Permutations": theorem bij_swap_ompose_bij has
been renamed to bij_swap_compose_bij. INCOMPATIBILITY.
* New theory "HOL-Library.Going_To_Filter" providing the "f going_to F"
filter for describing points x such that f(x) is in the filter F.
* Theory "HOL-Library.Formal_Power_Series": constants X/E/L/F have been
renamed to fps_X/fps_exp/fps_ln/fps_hypergeo to avoid polluting the name
space. INCOMPATIBILITY.
* Theory "HOL-Library.FinFun" has been moved to AFP (again).
INCOMPATIBILITY.
* Theory "HOL-Library.FuncSet": some old and rarely used ASCII
replacement syntax has been removed. INCOMPATIBILITY, standard syntax
with symbols should be used instead. The subsequent commands help to
reproduce the old forms, e.g. to simplify porting old theories:
syntax (ASCII)
"_PiE" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set" ("(3PIE _:_./ _)" 10)
"_Pi" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set" ("(3PI _:_./ _)" 10)
"_lam" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)" ("(3%_:_./ _)" [0,0,3] 3)
* Theory "HOL-Library.Multiset": the simprocs on subsets operators of
multisets have been renamed:
msetless_cancel_numerals ~> msetsubset_cancel
msetle_cancel_numerals ~> msetsubset_eq_cancel
INCOMPATIBILITY.
* Theory "HOL-Library.Pattern_Aliases" provides input and output syntax
for pattern aliases as known from Haskell, Scala and ML.
* Theory "HOL-Library.Uprod" formalizes the type of unordered pairs.
* Session HOL-Analysis: more material involving arcs, paths, covering
spaces, innessential maps, retracts, infinite products, simplicial
complexes. Baire Category theorem. Major results include the Jordan
Curve Theorem and the Great Picard Theorem.
* Session HOL-Algebra has been extended by additional lattice theory:
the Knaster-Tarski fixed point theorem and Galois Connections.
* Sessions HOL-Computational_Algebra and HOL-Number_Theory: new notions
of squarefreeness, n-th powers, and prime powers.
* Session "HOL-Computional_Algebra" covers many previously scattered
theories, notably Euclidean_Algorithm, Factorial_Ring,
Formal_Power_Series, Fraction_Field, Fundamental_Theorem_Algebra,
Normalized_Fraction, Polynomial_FPS, Polynomial, Primes. Minor
INCOMPATIBILITY.
*** System ***
* Isabelle/Scala: the SQL module supports access to relational
databases, either as plain file (SQLite) or full-scale server
(PostgreSQL via local port or remote ssh connection).
* Results of "isabelle build" are recorded as SQLite database (i.e.
"Application File Format" in the sense of
https://www.sqlite.org/appfileformat.html). This allows systematic
access via operations from module Sessions.Store in Isabelle/Scala.
* System option "parallel_proofs" is 1 by default (instead of more
aggressive 2). This requires less heap space and avoids burning parallel
CPU cycles, while full subproof parallelization is enabled for repeated
builds (according to parallel_subproofs_threshold).
* System option "record_proofs" allows to change the global
Proofterm.proofs variable for a session. Regular values are are 0, 1, 2;
a negative value means the current state in the ML heap image remains
unchanged.
* Isabelle settings variable ISABELLE_SCALA_BUILD_OPTIONS has been
renamed to ISABELLE_SCALAC_OPTIONS. Rare INCOMPATIBILITY.
* Isabelle settings variables ISABELLE_WINDOWS_PLATFORM,
ISABELLE_WINDOWS_PLATFORM32, ISABELLE_WINDOWS_PLATFORM64 indicate the
native Windows platform (independently of the Cygwin installation). This
is analogous to ISABELLE_PLATFORM, ISABELLE_PLATFORM32,
ISABELLE_PLATFORM64.
* Command-line tool "isabelle build_docker" builds a Docker image from
the Isabelle application bundle for Linux. See also
https://hub.docker.com/r/makarius/isabelle
* Command-line tool "isabelle vscode_server" provides a Language Server
Protocol implementation, e.g. for the Visual Studio Code editor. It
serves as example for alternative PIDE front-ends.
* Command-line tool "isabelle imports" helps to maintain theory imports
wrt. session structure. Examples for the main Isabelle distribution:
isabelle imports -I -a
isabelle imports -U -a
isabelle imports -U -i -a
isabelle imports -M -a -d '~~/src/Benchmarks'
New in Isabelle2016-1 (December 2016)
-------------------------------------
*** General ***
* Splitter in proof methods "simp", "auto" and friends:
- The syntax "split add" has been discontinued, use plain "split",
INCOMPATIBILITY.
- For situations with many conditional or case expressions, there is
an alternative splitting strategy that can be much faster. It is
selected by writing "split!" instead of "split". It applies safe
introduction and elimination rules after each split rule. As a
result the subgoal may be split into several subgoals.
* Command 'bundle' provides a local theory target to define a bundle
from the body of specification commands (such as 'declare',
'declaration', 'notation', 'lemmas', 'lemma'). For example:
bundle foo
begin
declare a [simp]
declare b [intro]
end
* Command 'unbundle' is like 'include', but works within a local theory
context. Unlike "context includes ... begin", the effect of 'unbundle'
on the target context persists, until different declarations are given.
* Simplified outer syntax: uniform category "name" includes long
identifiers. Former "xname" / "nameref" / "name reference" has been
discontinued.
* Embedded content (e.g. the inner syntax of types, terms, props) may be
delimited uniformly via cartouches. This works better than old-fashioned
quotes when sub-languages are nested.
* Mixfix annotations support general block properties, with syntax
"(\<open>x=a y=b z \<dots>\<close>". Notable property names are "indent", "consistent",
"unbreakable", "markup". The existing notation "(DIGITS" is equivalent
to "(\<open>indent=DIGITS\<close>". The former notation "(00" for unbreakable blocks
is superseded by "(\<open>unbreabable\<close>" --- rare INCOMPATIBILITY.
* Proof method "blast" is more robust wrt. corner cases of Pure
statements without object-logic judgment.
* Commands 'prf' and 'full_prf' are somewhat more informative (again):
proof terms are reconstructed and cleaned from administrative thm nodes.
* Code generator: config option "code_timing" triggers measurements of
different phases of code generation. See src/HOL/ex/Code_Timing.thy for
examples.
* Code generator: implicits in Scala (stemming from type class
instances) are generated into companion object of corresponding type
class, to resolve some situations where ambiguities may occur.
* Solve direct: option "solve_direct_strict_warnings" gives explicit
warnings for lemma statements with trivial proofs.
*** Prover IDE -- Isabelle/Scala/jEdit ***
* More aggressive flushing of machine-generated input, according to
system option editor_generated_input_delay (in addition to existing
editor_input_delay for regular user edits). This may affect overall PIDE
reactivity and CPU usage.
* Syntactic indentation according to Isabelle outer syntax. Action
"indent-lines" (shortcut C+i) indents the current line according to
command keywords and some command substructure. Action
"isabelle.newline" (shortcut ENTER) indents the old and the new line
according to command keywords only; see also option
"jedit_indent_newline".
* Semantic indentation for unstructured proof scripts ('apply' etc.) via
number of subgoals. This requires information of ongoing document
processing and may thus lag behind, when the user is editing too
quickly; see also option "jedit_script_indent" and
"jedit_script_indent_limit".
* Refined folding mode "isabelle" based on Isar syntax: 'next' and 'qed'
are treated as delimiters for fold structure; 'begin' and 'end'
structure of theory specifications is treated as well.
* Command 'proof' provides information about proof outline with cases,
e.g. for proof methods "cases", "induct", "goal_cases".
* Completion templates for commands involving "begin ... end" blocks,
e.g. 'context', 'notepad'.
* Sidekick parser "isabelle-context" shows nesting of context blocks
according to 'begin' and 'end' structure.
* Highlighting of entity def/ref positions wrt. cursor.
* Action "isabelle.select-entity" (shortcut CS+ENTER) selects all
occurrences of the formal entity at the caret position. This facilitates
systematic renaming.
* PIDE document markup works across multiple Isar commands, e.g. the
results established at the end of a proof are properly identified in the
theorem statement.
* Cartouche abbreviations work both for " and ` to accomodate typical
situations where old ASCII notation may be updated.
* Dockable window "Symbols" also provides access to 'abbrevs' from the
outer syntax of the current theory buffer. This provides clickable
syntax templates, including entries with empty abbrevs name (which are
inaccessible via keyboard completion).
* IDE support for the Isabelle/Pure bootstrap process, with the
following independent stages:
src/Pure/ROOT0.ML
src/Pure/ROOT.ML
src/Pure/Pure.thy
src/Pure/ML_Bootstrap.thy
The ML ROOT files act like quasi-theories in the context of theory
ML_Bootstrap: this allows continuous checking of all loaded ML files.
The theory files are presented with a modified header to import Pure
from the running Isabelle instance. Results from changed versions of
each stage are *not* propagated to the next stage, and isolated from the
actual Isabelle/Pure that runs the IDE itself. The sequential
dependencies of the above files are only observed for batch build.
* Isabelle/ML and Standard ML files are presented in Sidekick with the
tree structure of section headings: this special comment format is
described in "implementation" chapter 0, e.g. (*** section ***).
* Additional abbreviations for syntactic completion may be specified
within the theory header as 'abbrevs'. The theory syntax for 'keywords'
has been simplified accordingly: optional abbrevs need to go into the
new 'abbrevs' section.
* Global abbreviations via $ISABELLE_HOME/etc/abbrevs and
$ISABELLE_HOME_USER/etc/abbrevs are no longer supported. Minor
INCOMPATIBILITY, use 'abbrevs' within theory header instead.
* Action "isabelle.keymap-merge" asks the user to resolve pending
Isabelle keymap changes that are in conflict with the current jEdit
keymap; non-conflicting changes are always applied implicitly. This
action is automatically invoked on Isabelle/jEdit startup and thus
increases chances that users see new keyboard shortcuts when re-using
old keymaps.
* ML and document antiquotations for file-systems paths are more uniform
and diverse:
@{path NAME} -- no file-system check
@{file NAME} -- check for plain file
@{dir NAME} -- check for directory
Minor INCOMPATIBILITY, former uses of @{file} and @{file_unchecked} may
have to be changed.
*** Document preparation ***
* New symbol \<circle>, e.g. for temporal operator.
* New document and ML antiquotation @{locale} for locales, similar to
existing antiquotation @{class}.
* Mixfix annotations support delimiters like \<^control>\<open>cartouche\<close> --
this allows special forms of document output.
* Raw LaTeX output now works via \<^latex>\<open>...\<close> instead of raw control
symbol \<^raw:...>. INCOMPATIBILITY, notably for LaTeXsugar.thy and its
derivatives.
* \<^raw:...> symbols are no longer supported.
* Old 'header' command is no longer supported (legacy since
Isabelle2015).
*** Isar ***
* Many specification elements support structured statements with 'if' /
'for' eigen-context, e.g. 'axiomatization', 'abbreviation',
'definition', 'inductive', 'function'.
* Toplevel theorem statements support eigen-context notation with 'if' /
'for' (in postfix), which corresponds to 'assumes' / 'fixes' in the
traditional long statement form (in prefix). Local premises are called
"that" or "assms", respectively. Empty premises are *not* bound in the
context: INCOMPATIBILITY.
* Command 'define' introduces a local (non-polymorphic) definition, with
optional abstraction over local parameters. The syntax resembles
'definition' and 'obtain'. It fits better into the Isar language than
old 'def', which is now a legacy feature.
* Command 'obtain' supports structured statements with 'if' / 'for'
context.
* Command '\<proof>' is an alias for 'sorry', with different
typesetting. E.g. to produce proof holes in examples and documentation.
* The defining position of a literal fact \<open>prop\<close> is maintained more
carefully, and made accessible as hyperlink in the Prover IDE.
* Commands 'finally' and 'ultimately' used to expose the result as
literal fact: this accidental behaviour has been discontinued. Rare
INCOMPATIBILITY, use more explicit means to refer to facts in Isar.
* Command 'axiomatization' has become more restrictive to correspond
better to internal axioms as singleton facts with mandatory name. Minor
INCOMPATIBILITY.
* Proof methods may refer to the main facts via the dynamic fact
"method_facts". This is particularly useful for Eisbach method
definitions.
* Proof method "use" allows to modify the main facts of a given method
expression, e.g.
(use facts in simp)
(use facts in \<open>simp add: ...\<close>)
* The old proof method "default" has been removed (legacy since
Isabelle2016). INCOMPATIBILITY, use "standard" instead.
*** Pure ***
* Pure provides basic versions of proof methods "simp" and "simp_all"
that only know about meta-equality (==). Potential INCOMPATIBILITY in
theory imports that merge Pure with e.g. Main of Isabelle/HOL: the order
is relevant to avoid confusion of Pure.simp vs. HOL.simp.
* The command 'unfolding' and proof method "unfold" include a second
stage where given equations are passed through the attribute "abs_def"
before rewriting. This ensures that definitions are fully expanded,
regardless of the actual parameters that are provided. Rare
INCOMPATIBILITY in some corner cases: use proof method (simp only:)
instead, or declare [[unfold_abs_def = false]] in the proof context.
* Type-inference improves sorts of newly introduced type variables for
the object-logic, using its base sort (i.e. HOL.type for Isabelle/HOL).
Thus terms like "f x" or "\<And>x. P x" without any further syntactic context
produce x::'a::type in HOL instead of x::'a::{} in Pure. Rare
INCOMPATIBILITY, need to provide explicit type constraints for Pure
types where this is really intended.
*** HOL ***
* New proof method "argo" using the built-in Argo solver based on SMT
technology. The method can be used to prove goals of quantifier-free
propositional logic, goals based on a combination of quantifier-free
propositional logic with equality, and goals based on a combination of
quantifier-free propositional logic with linear real arithmetic
including min/max/abs. See HOL/ex/Argo_Examples.thy for examples.
* The new "nunchaku" command integrates the Nunchaku model finder. The
tool is experimental. See ~~/src/HOL/Nunchaku/Nunchaku.thy for details.
* Metis: The problem encoding has changed very slightly. This might
break existing proofs. INCOMPATIBILITY.
* Sledgehammer:
- The MaSh relevance filter is now faster than before.
- Produce syntactically correct Vampire 4.0 problem files.
* (Co)datatype package:
- New commands for defining corecursive functions and reasoning about
them in "~~/src/HOL/Library/BNF_Corec.thy": 'corec', 'corecursive',
'friend_of_corec', and 'corecursion_upto'; and 'corec_unique' proof
method. See 'isabelle doc corec'.
- The predicator :: ('a \<Rightarrow> bool) \<Rightarrow> 'a F \<Rightarrow> bool is now a first-class
citizen in bounded natural functors.
- 'primrec' now allows nested calls through the predicator in addition
to the map function.
- 'bnf' automatically discharges reflexive proof obligations.
- 'bnf' outputs a slightly modified proof obligation expressing rel in
terms of map and set
(not giving a specification for rel makes this one reflexive).
- 'bnf' outputs a new proof obligation expressing pred in terms of set
(not giving a specification for pred makes this one reflexive).
INCOMPATIBILITY: manual 'bnf' declarations may need adjustment.
- Renamed lemmas:
rel_prod_apply ~> rel_prod_inject
pred_prod_apply ~> pred_prod_inject
INCOMPATIBILITY.
- The "size" plugin has been made compatible again with locales.
- The theorems about "rel" and "set" may have a slightly different (but
equivalent) form.
INCOMPATIBILITY.
* The 'coinductive' command produces a proper coinduction rule for
mutual coinductive predicates. This new rule replaces the old rule,
which exposed details of the internal fixpoint construction and was
hard to use. INCOMPATIBILITY.
* New abbreviations for negated existence (but not bounded existence):
\<nexists>x. P x \<equiv> \<not> (\<exists>x. P x)
\<nexists>!x. P x \<equiv> \<not> (\<exists>!x. P x)
* The print mode "HOL" for ASCII syntax of binders "!", "?", "?!", "@"
has been removed for output. It is retained for input only, until it is
eliminated altogether.
* The unique existence quantifier no longer provides 'binder' syntax,
but uses syntax translations (as for bounded unique existence). Thus
iterated quantification \<exists>!x y. P x y with its slightly confusing
sequential meaning \<exists>!x. \<exists>!y. P x y is no longer possible. Instead,
pattern abstraction admits simultaneous unique existence \<exists>!(x, y). P x y
(analogous to existing notation \<exists>!(x, y)\<in>A. P x y). Potential
INCOMPATIBILITY in rare situations.
* Conventional syntax "%(). t" for unit abstractions. Slight syntactic
INCOMPATIBILITY.
* Renamed constants and corresponding theorems:
setsum ~> sum
setprod ~> prod
listsum ~> sum_list
listprod ~> prod_list
INCOMPATIBILITY.
* Sligthly more standardized theorem names:
sgn_times ~> sgn_mult
sgn_mult' ~> Real_Vector_Spaces.sgn_mult
divide_zero_left ~> div_0
zero_mod_left ~> mod_0
divide_zero ~> div_by_0
divide_1 ~> div_by_1
nonzero_mult_divide_cancel_left ~> nonzero_mult_div_cancel_left
div_mult_self1_is_id ~> nonzero_mult_div_cancel_left
nonzero_mult_divide_cancel_right ~> nonzero_mult_div_cancel_right
div_mult_self2_is_id ~> nonzero_mult_div_cancel_right
is_unit_divide_mult_cancel_left ~> is_unit_div_mult_cancel_left
is_unit_divide_mult_cancel_right ~> is_unit_div_mult_cancel_right
mod_div_equality ~> div_mult_mod_eq
mod_div_equality2 ~> mult_div_mod_eq
mod_div_equality3 ~> mod_div_mult_eq
mod_div_equality4 ~> mod_mult_div_eq
minus_div_eq_mod ~> minus_div_mult_eq_mod
minus_div_eq_mod2 ~> minus_mult_div_eq_mod
minus_mod_eq_div ~> minus_mod_eq_div_mult
minus_mod_eq_div2 ~> minus_mod_eq_mult_div
div_mod_equality' ~> minus_mod_eq_div_mult [symmetric]
mod_div_equality' ~> minus_div_mult_eq_mod [symmetric]
zmod_zdiv_equality ~> mult_div_mod_eq [symmetric]
zmod_zdiv_equality' ~> minus_div_mult_eq_mod [symmetric]
Divides.mult_div_cancel ~> minus_mod_eq_mult_div [symmetric]
mult_div_cancel ~> minus_mod_eq_mult_div [symmetric]
zmult_div_cancel ~> minus_mod_eq_mult_div [symmetric]
div_1 ~> div_by_Suc_0
mod_1 ~> mod_by_Suc_0
INCOMPATIBILITY.
* New type class "idom_abs_sgn" specifies algebraic properties
of sign and absolute value functions. Type class "sgn_if" has
disappeared. Slight INCOMPATIBILITY.
* Dedicated syntax LENGTH('a) for length of types.
* Characters (type char) are modelled as finite algebraic type
corresponding to {0..255}.
- Logical representation:
* 0 is instantiated to the ASCII zero character.
* All other characters are represented as "Char n"
with n being a raw numeral expression less than 256.
* Expressions of the form "Char n" with n greater than 255
are non-canonical.
- Printing and parsing:
* Printable characters are printed and parsed as "CHR ''\<dots>''"
(as before).
* The ASCII zero character is printed and parsed as "0".
* All other canonical characters are printed as "CHR 0xXX"
with XX being the hexadecimal character code. "CHR n"
is parsable for every numeral expression n.
* Non-canonical characters have no special syntax and are
printed as their logical representation.
- Explicit conversions from and to the natural numbers are
provided as char_of_nat, nat_of_char (as before).
- The auxiliary nibble type has been discontinued.
INCOMPATIBILITY.
* Type class "div" with operation "mod" renamed to type class "modulo"
with operation "modulo", analogously to type class "divide". This
eliminates the need to qualify any of those names in the presence of
infix "mod" syntax. INCOMPATIBILITY.
* Statements and proofs of Knaster-Tarski fixpoint combinators lfp/gfp
have been clarified. The fixpoint properties are lfp_fixpoint, its
symmetric lfp_unfold (as before), and the duals for gfp. Auxiliary items
for the proof (lfp_lemma2 etc.) are no longer exported, but can be
easily recovered by composition with eq_refl. Minor INCOMPATIBILITY.
* Constant "surj" is a mere input abbreviation, to avoid hiding an
equation in term output. Minor INCOMPATIBILITY.
* Command 'code_reflect' accepts empty constructor lists for datatypes,
which renders those abstract effectively.
* Command 'export_code' checks given constants for abstraction
violations: a small guarantee that given constants specify a safe
interface for the generated code.
* Code generation for Scala: ambiguous implicts in class diagrams are
spelt out explicitly.
* Static evaluators (Code_Evaluation.static_* in Isabelle/ML) rely on