-
Notifications
You must be signed in to change notification settings - Fork 5
/
Copy pathNEWS
18022 lines (13781 loc) · 710 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 Isabelle2024 (May 2024)
------------------------------
*** General ***
* Dropped support for very old operating systems. The platform
base-lines are now as follows:
- Ubuntu Linux 18.04 LTS
- macOS 11 Big Sur
- Windows 10 or Windows Server 2012 R2
* The arm64-linux platform is now officially supported, although a few
(non-essential) tools are missing:
- Z3
- CVC4
- MLton
- Nunchaku + smbc (experimental)
* The configuration option "unify_trace" (default: false) guards tracing
of higher-order unification, which is ubiquitous in assumption steps and
rule applications via resolution. This is disabled by default to avoid
breakdown due to massive amounts of spurious messages.
*** Document preparation ***
* The bundled LaTeX LNCS style has been updated to version 2.23
(02-Nov-2023). See also src/Doc/Demo_LLNCS/.
*** HOL ***
* Generated Scala code now works both with scalac -new-syntax or
-old-syntax, but option -no-indent should always be used for robustness.
Note that ISABELLE_SCALAC_OPTIONS provides options for Isabelle/Scala,
which are also used for "export_code ... checking Scala".
* Commands 'inductive_cases', 'inductive_simps', 'case_of_simps',
'simps_of_case' now print results like 'theorem'.
* Sledgehammer
- Update/rebuild of bundled provers:
. E prover 3.0, with native ARM64 executables
. Vampire 4.8 HO - Sledgehammer schedules (2023-10-19)
. veriT 2021.06.1-rmx - rebuild for arm64-linux
. Z3 4.4.1 for arm64-linux has been removed: unreliable, unstable.
- New implementation of moura tactic. INCOMPATIBILITY.
- Added support for "order" proof method to proof reconstruction.
* Mirabelle:
- Removed proof reconstruction from "sledgehammer" action; the related
option "proof_method" was removed. Proof reconstruction is supported
directly by Sledgehammer and should be used instead. For more
information, see Sledgehammer's documentation relating to
"preplay_timeout". INCOMPATIBILITY.
- Added the action "order" testing the proof method of the same name.
* Explicit type class for discrete_linear_ordered_semidom for integral
semidomains with a discrete linear order.
* Type class linordered_euclidean_semiring replaces the (rather
technical) type class unique_euclidean_semiring_with_nat; type class
unique_euclidean_ring_with_nat, which barely admits instances other than
isomorphic to int, is discontinued; type class
unique_euclidean_semiring_with_bit_operations is renamed to
linordered_euclidean_semiring_bit_operations. Minor INCOMPATIBILITY.
* Streamlined specification of type class (semi)ring_parity. Minor
INCOMPATIBILITY.
* Lemma even_succ_div_2 renamed to even_half_succ_eq. Minor
INCOMPATIBILITY.
* Theory "HOL.Relation":
- Added lemmas.
antisymp_on_image
asymp_on_image
irreflp_on_image
reflp_on_image
symp_on_image
totalp_on_image
transp_on_image
* Theory "HOL.Transitive_Closure":
- Renamed lemma antisymp_on_reflcp to antisymp_on_reflclp.
Minor INCOMPATIBILITY.
- Added lemmas.
antisym_on_reflcl_if_asym_on
antisymp_on_reflclp_if_asymp_on
order_reflclp_if_transp_and_asymp
reflclp_greater_eq[simp]
reflclp_less_eq[simp]
relpow_left_unique
relpow_right_unique
relpow_trans[trans]
relpowp_left_unique
relpowp_right_unique
relpowp_trans[trans]
rtranclp_greater_eq[simp]
rtranclp_ident_if_reflp_and_transp
rtranclp_less_eq[simp]
tranclp_greater[simp]
tranclp_greater_eq[simp]
tranclp_ident_if_and_transp
tranclp_less[simp]
tranclp_less_eq[simp]
* Theory "HOL.Wellfounded":
- Added predicates wf_on and wfp_on and redefined wfP to be
abbreviations. Lemmas wf_def and wfP_def are explicitly provided for
backward compatibility but their usage is discouraged. Minor
INCOMPATIBILITY.
- Added wfp as alias for wfP for greater consistency with other
predicates such as asymp, transp, or totalp.
- Added lemmas.
wellorder.wfp_on_less[simp]
wf_iff_ex_minimal
wf_onE_pf
wf_onI_pf
wf_on_antimono
wf_on_antimono_strong
wf_on_if_convertible_to_wf_on
wf_on_iff_ex_minimal
wf_on_iff_wf
wf_on_induct
wf_on_subset
wfp_iff_ex_minimal
wfp_on_antimono
wfp_on_antimono_strong
wfp_on_if_convertible_to_wfp_on
wfp_on_iff_ex_minimal
wfp_on_image
wfp_on_induct
wfp_on_inv_imagep
wfp_on_subset
wfp_on_wf_on_eq
* Theory "HOL-Library.FSet":
- Added syntax for fBall and fBex.
* Theory "HOL-Library.Multiset":
- Added lemmas.
trans_on_mult
transp_on_multp
* Theory "HOL-ex.Sketch_and_Explore": improvements to generate more
natural and readable proof sketches from proof states.
* Session "HOL-Analysis": the syntax of Lebesgue integrals (LINT, LBINT,
\<integral>, etc.) now requires parentheses in most cases. INCOMPATIBILITY.
* Session "HOL-Analysis": corrected the definition of convex function
(convex_on) to require the underlying set to be convex. INCOMPATIBILITY.
* Session "HOL-Complex_Analysis": new, more general definition of
meromorphicity. INCOMPATIBILITY.
* Session "HOL-Data_Structures": automatic translation from HOL
functions into corresponding step-counting running-time functions. See
theory "HOL-Data_Structures.Define_Time_Function".
*** ML ***
* ML antiquotation "try" provides variants of exception handling that
avoids accidental capture of physical interrupts (which could affect ML
semantics in unpredictable ways):
\<^try>\<open>EXPR catch HANDLER\<close>
\<^try>\<open>EXPR finally HANDLER\<close>
\<^try>\<open>EXPR\<close>
See also the implementations Isabelle_Thread.try_catch / try_finally /
try. The HANDLER always runs as uninterruptible, but the EXPR uses the
the current thread attributes (normally interruptible). Various examples
occur in the Isabelle sources (.ML and .thy files).
* Isabelle/ML explicitly rejects 'handle' with catch-all patterns.
INCOMPATIBILITY, better use \<^try>\<open>...\<close> with 'catch' or 'finally', or
as last resort declare [[ML_catch_all]] within the theory context.
* ML antiquotation "simproc_setup" inlines an invocation of
Simplifier.simproc_setup, using the same concrete syntax as the
corresponding Isar command. This allows to introduce a new simproc
conveniently within an ML module, and refer directly to its ML value.
For example, the simproc "Record.eq" is defined in
~~/src/HOL/Tools/record.ML as follows:
val eq_simproc = \<^simproc_setup>\<open>eq ("r = s") = \<open>K eq_proc\<close>\<close>;
* Simplification procedures may be distinguished via characteristic
theorems that are specified as 'identifier' in ML antiquotation
"simproc_setup" (but not in the corresponding Isar command). This allows
to work with several versions of the simproc, e.g. due to locale
interpretations.
* Proper interrupts (e.g. timeouts) are now distinguished from Poly/ML
runtime system breakdown, using Exn.Interrupt_Breakdown as quasi-error.
Exn.is_interrupt covers all kinds of interrupts as before, but
Exn.is_interrupt_proper and Exn.is_interrupt_breakdown are more
specific. Subtle INCOMPATIBILITY in the semantics of ML evaluation.
*** System ***
* More robust and scalable support for distributed build clusters, based
on SSH and PostgreSQL. This includes advanced scheduling as follows:
isabelle build -o build_engine=build_schedule -H host1 -H host2
* The command-line tool "isabelle build" now uses default 0 (instead of
1) for option -j. This means that "isabelle build -H" will initialize
the build queue and oversee remote workers, but not run any Isabelle
sessions on its own account. INCOMPATIBILITY, use "isabelle build -j1
-H" for the old behaviour, to have the local host participate as worker.
* The Isabelle/Scala module isabelle.Registry provides hierarchic system
configuration, based on a collection of TOML files (see also
https://toml.io/en/v1.0.0). The settings variable ISABELLE_REGISTRY
tells which files are included into isabelle.Registry.global by default.
The bash function "isabelle_registry" may be used in component
etc/settings or $ISABELLE_HOME_USER/etc/settings to append further
files: a trailing question mark means that the entry is optional. The
default settings use "$ISABELLE_HOME/etc/registry.toml?" and
"$ISABELLE_HOME_USER/etc/registry.toml?" (in that order).
* Isabelle build cluster specifications, as seen in "isabelle build"
option "-H", now use the underlying system registry to determine actual
host names, parameters, and system options. A name without prefix refers
to the registry table "host": each entry consists of an optional
"hostname" and further options. A name with the prefix "cluster." refers
to the table "cluster": each entry provides "hosts", an array of names
for entries of the table "host" as above, and additional options that
apply to all hosts simultaneously.
For example, consider "isabelle build -H a -H b -H cluster.xy" in the
context of a system registry $ISABELLE_HOME_USER/etc/registry.toml like
this:
host.a = { hostname = "host-a.acme.org", jobs = 2 }
host.b = { hostname = "host-b.acme.org", jobs = 2 }
host.x = { hostname = "server1.example.com" }
host.y = { hostname = "server2.example.com" }
cluster.xy = { hosts = ["x", "y"], jobs = 4 }
If "hostname" is omitted, its default is the table entry name itself. If
that contains a dot, it needs to be quoted according to TOML syntax:
host."host-a.acme.org" = { jobs = 2 }
host."host-b.acme.org" = { jobs = 2 }
* Isabelle/Scala and derived Scala tools now use the syntax of Scala
3.3, instead of 3.1. This is the "-old-syntax" variant (Java-like) as
before, not "-new-syntax" (Python-like). Minor INCOMPATIBILITY.
* Isabelle/Scala supports mailing via SMTP, based on new system
component javamail (previously javax.mail) from jakarta 2.1.2
using eclipse angus 2.0.2/2.0.1.
* Isabelle/Scala now has some support for web-apps, using HTML 5 forms.
* Directory src/Tools/Demo provides an Isabelle system component with
command-line tool that is implemented in Isabelle/Scala. It serves as
demonstration for user-defined tools.
* Old $ISABELLE_HOME/bin/isabelle_scala_script has been removed.
Command-line tools in Isabelle/Scala should be provided by a proper
system component with etc/build.props, e.g. see src/Tools/Demo/.
* The Isabelle component for the MLton compiler now covers macOS and
Linux (Intel), while Windows and Linux (ARM) are unsupported. The
default for ISABELLE_MLTON_OPTIONS should work most of the time, but may
have to be overridden (e.g. in $ISABELLE_HOME_USER/etc/settings).
* The command-line tools "isabelle go_setup" and "isabelle go" /
"isabelle gofmt" support the Go development environment. This works
uniformly on all Isabelle OS platforms, separately or simultaneously.
For example:
isabelle go_setup
isabelle go env
isabelle go
isabelle go_setup -p all
* Update to GHC stack-2.15.5, stackage-lts-22.15, ghc-9.6.4 with support
for all platforms, including ARM Linux and Apple Silicon.
* Update to .NET / Fsharp 8.0.x: the current long-term support version.
* Update to official Poly/ML 5.9.1.
* Update to OpenJDK 21: the current long-term support version of Java.
New in Isabelle2023 (September 2023)
------------------------------------
*** General ***
* Toplevel results --- like declared consts and proven theorems --- are
printed as regular "writeln" message instead of "state", which is no
specifically for proof states. This affects Isabelle/jEdit panels for
Output vs. State in particular.
* Session build dependencies (sources and heaps) are now recorded in
more details, with one SHA1 digest per file and a symbolic version of
the file name -- similar to the Unix command-line tool "sha1sum". For
portability of results, well-known directory names are folded into path
variables according to cumulative "isabelle_directory" declarations in
etc/settings (user projects may add to that). See also "isabelle getenv
ISABELLE_DIRECTORIES" for the effective result, which is used by the
Isabelle/Scala function isabelle.File.symbolic_path() for its
first-match policy in reverse order.
* ML heap usage and stored heap size has been significantly reduced,
especially for applications with a lot 'locale' or 'class' context
switches, e.g. "definition (in loc)". The shrink factor is usually in
the range 1.1 .. 2.0, but a factor 2 .. 25 has been seen as well. This
often allows big applications to return to the "small" 64_32 memory
model with its hard limit of 16 GiB, and thus reduce the heap size by
another factor 1.8.
* The special "of_class" introduction rule for 'class' definitions has
been renamed from "class.NAME.of_class.intro" to "NAME.intro_of_class"
(where NAME is the name specification of the class). E.g. see the HOL
library:
class.preorder.of_class.intro ~> preorder.intro_of_class
class.order.of_class.intro ~> order.intro_of_class
* The Eisbach 'method' command now takes an optional description for
display with 'print_methods', similar to the 'method_setup' command.
* Experimental support for distributed build clusters, based on SSH and
PostgreSQL. Example for 3 nodes (local, host1, host2):
isabelle build -a -j2 -o threads=8 \
-H host1:jobs=2,threads=8
-H host2:jobs=4:threads=4,numa,shared
Like the "isabelle sync" tool, this requires a proper Isabelle
repository clone (e.g. via "isabelle/Admin/init -r Isabelle2023").
The build database server needs to be specified for each remote node in
$USER_HOME/.isabelle/build_cluster (according to option
"build_cluster_identifier").
See also "isabelle build_process -?" and "isabelle build_worker -?".
*** Document preparation ***
* Support for interactive document preparation in PIDE, notably via the
Isabelle/jEdit Document panel.
* Various well-known LaTeX styles are included as Isabelle components,
with demo documents in the regular Isabelle "doc" space:
- Easychair as session "Demo_Easychair" / doc "demo_easychair"
- EPTCS as session "Demo_EPTCS" / doc "demo_eptcs"
- FoilTeX as session "Demo_FoilTeX" / doc "demo_foiltex"
- Dagstuhl LIPIcs style as session "Demo_LIPIcs" / doc "demo_lipics"
- Springer LaTeX LNCS style as session "Demo_LLNCS" / doc "demo_llncs"
* Support for more "cite" antiquotations, notably for \nocite and
natbib's \citet / \citep. The antiquotation syntax now supports
control-symbol-cartouche form, with an embedded argument:
\<^cite>\<open>arg\<close>. The embedded argument syntax supports both the optional
and mandatory argument of the underlying \cite-like macro.
Examples:
\<^cite>\<open>\<open>\S1.2\<close> in "isabelle-system"\<close>
\<^cite>\<open>"isabelle-system" and "isabelle-jedit"\<close>
\<^nocite>\<open>"isabelle-isar-ref"\<close>
The old antiquotation option "cite_macro" has been superseded by
explicit syntax: \<^cite>\<open>\<dots> using macro_name\<close>.
The command-line tool "isabelle update -u cite" helps to update former
uses of LaTeX \cite commands and old-style @{cite "name"} document
antiquotations.
*** HOL ***
* Sledgehammer:
- Added an inconsistency check mode to find likely unprovable
conjectures. It is disabled by default and can be controlled using
the 'falsify' option.
- Added an abduction mode to find likely missing hypotheses to
conjectures. It works only with the E prover. It is disabled by
default and can be controlled using the 'abduce' option.
* Metis:
- Made clausifier more robust in the face of nested lambdas.
Minor INCOMPATIBILITY.
* Command "try0":
- Add proof method "order".
* 'primcorec': Made the internal tactic more robust in the face of
nested corecursion.
* Theory "HOL.Map":
- Map.empty has been demoted to an input abbreviation.
- Map update syntax "_(_ \<mapsto> _)" now has the same priorities
as function update syntax "_(_ := _)". This means:
1. "f t(a \<mapsto> b)" must now be written "(f t)(a \<mapsto> b)"
2. "t(a \<mapsto> b)(c \<mapsto> d)" must now be written
"t(a \<mapsto> b, c \<mapsto> d)" or
"(t(a \<mapsto> b))(c \<mapsto> d)".
Moreover, ":=" and "\<mapsto>" can be mixed freely now.
Except in "[...]" maps where ":=" would create a clash with
list update syntax "xs[i := x]".
* Theory "HOL.Fun":
- Renamed lemma inj_on_strict_subset to image_strict_mono.
Minor INCOMPATIBILITY.
* Theory "HOL.Euclidean_Division" renamed to "HOL.Euclidean_Rings";
"euclidean division" typically denotes a particular division on
integers. Minor INCOMPATIBILITY.
* Theory "HOL.Finite_Set"
- Imported Relation instead of Product_Type, Sum_Type, and Fields.
Minor INCOMPATIBILITY.
- Added lemmas.
Finite_Set.bex_greatest_element
Finite_Set.bex_least_element
Finite_Set.bex_max_element
Finite_Set.bex_max_element_with_property
Finite_Set.bex_min_element
Finite_Set.bex_min_element_with_property
is_max_element_in_set_iff
is_min_element_in_set_iff
* Theory "HOL.Relation":
- Imported Product_Type, Sum_Type, and Fields instead of Finite_Set.
Minor INCOMPATIBILITY.
- Added predicates irrefl_on and irreflp_on and redefined irrefl and
irreflp to be abbreviations. Lemmas irrefl_def and irreflp_def are
explicitly provided for backward compatibility but their usage is
discouraged. Minor INCOMPATIBILITY.
- Added predicates sym_on and symp_on and redefined sym and symp to be
abbreviations. Lemmas sym_def and symp_def are explicitly provided
for backward compatibility but their usage is discouraged. Minor
INCOMPATIBILITY.
- Added predicates asym_on and asymp_on and redefined asym and asymp
to be abbreviations. INCOMPATIBILITY.
- Added predicates antisym_on and antisymp_on and redefined antisym
and antisymp to be abbreviations. Lemmas antisym_def and
antisymp_def are explicitly provided for backward compatibility but
their usage is discouraged. Minor INCOMPATIBILITY.
- Added predicates trans_on and transp_on and redefined trans and
transp to be abbreviations. Lemmas trans_def and transp_def are
explicitly provided for backward compatibility but their usage is
discouraged. Minor INCOMPATIBILITY.
- Renamed wrongly named lemma totalp_on_refl_on_eq to
totalp_on_total_on_eq. Minor INCOMPATIBILITY.
- Strengthened (and renamed) lemmas. Minor INCOMPATIBILITY.
antisym_converse[simp] ~> antisym_on_converse[simp]
order.antisymp_ge[simp] ~> order.antisymp_on_ge[simp]
order.antisymp_le[simp] ~> order.antisymp_on_le[simp]
preorder.asymp_greater[simp] ~> preorder.asymp_on_greater[simp]
preorder.asymp_less[simp] ~> preorder.asymp_on_less[simp]
preorder.irreflp_greater[simp] ~> preorder.irreflp_on_greater[simp]
preorder.irreflp_less[simp] ~> preorder.irreflp_on_less[simp]
preorder.transp_ge[simp] ~> preorder.transp_on_ge[simp]
preorder.transp_gr[simp] ~> preorder.transp_on_greater[simp]
preorder.transp_le[simp] ~> preorder.transp_on_le[simp]
preorder.transp_less[simp] ~> preorder.transp_on_less[simp]
reflp_equality[simp] ~> reflp_on_equality[simp]
sym_converse[simp] ~> sym_on_converse[simp]
total_on_singleton
trans_converse[simp] ~> trans_on_converse[simp]
- Added lemmas.
antisym_onD
antisym_onI
antisym_on_if_asymp_on
antisym_on_subset
antisymp_onD
antisymp_onI
antisymp_on_antisym_on_eq[pred_set_conv]
antisymp_on_conversep[simp]
antisymp_on_if_asymp_on
antisymp_on_subset
asym_on_iff_irrefl_on_if_trans_on
asym_onD
asym_onI
asym_on_converse[simp]
asymp_on_iff_irreflp_on_if_transp_on
asymp_onD
asymp_onI
asymp_on_asym_on_eq[pred_set_conv]
asymp_on_conversep[simp]
irreflD
irrefl_onD
irrefl_onI
irrefl_on_converse[simp]
irrefl_on_if_asym_on[simp]
irrefl_on_subset
irreflpD
irreflp_onD
irreflp_onI
irreflp_on_converse[simp]
irreflp_on_if_asymp_on[simp]
irreflp_on_irrefl_on_eq[pred_set_conv]
irreflp_on_subset
linorder.totalp_on_ge[simp]
linorder.totalp_on_greater[simp]
linorder.totalp_on_le[simp]
linorder.totalp_on_less[simp]
order.antisymp_ge[simp]
order.antisymp_le[simp]
preorder.antisymp_on_greater[simp]
preorder.antisymp_on_less[simp]
preorder.reflp_on_ge[simp]
preorder.reflp_on_le[simp]
reflD
reflI
reflp_on_conversp[simp]
sym_onD
sym_onI
sym_on_subset
symp_onD
symp_onI
symp_on_conversep[simp]
symp_on_subset
symp_on_sym_on_eq[pred_set_conv]
totalI
totalp_on_converse[simp]
totalp_on_singleton[simp]
trans_onD
trans_onI
trans_on_subset
transp_onD
transp_onI
transp_on_conversep
transp_on_subset
transp_on_trans_on_eq[pred_set_conv]
* Theory "HOL.Transitive_Closure":
- Strengthened (and renamed) lemmas. Minor INCOMPATIBILITY.
antisym_reflcl[simp] ~> antisym_on_reflcl[simp]
reflp_rtranclp[simp] ~> reflp_on_rtranclp[simp]
symp_symclp[simp] ~> symp_on_symclp[simp]
trans_reflclI[simp] ~> trans_on_reflcl[simp]
- Added lemmas.
antisymp_on_reflcp[simp]
reflclp_ident_if_reflp[simp]
reflp_on_reflclp[simp]
transp_on_reflclp[simp]
* Theory "HOL.Wellfounded":
- Added lemmas.
asym_lex_prod[simp]
asym_on_lex_prod[simp]
irrefl_lex_prod[simp]
irrefl_on_lex_prod[simp]
refl_lex_prod[simp]
sym_lex_prod[simp]
sym_on_lex_prod[simp]
trans_on_lex_prod[simp]
wfP_if_convertible_to_nat
wfP_if_convertible_to_wfP
wf_if_convertible_to_wf
* Theory "HOL-Library.FSet":
- Redefined fmember as an abbreviation based on Set.member.
Minor INCOMPATIBILITY.
- Redefined notin_fset as an abbreviation based on Set.not_member and
renamed to not_fmember. Minor INCOMPATIBILITY.
- Redefined fBall and fBex as abbreviations based on Set.Ball and Set.Bex.
Minor INCOMPATIBILITY.
- Removed lemmas. Minor INCOMPATIBILITIES.
fmember_iff_member_fset
notin_fset
- Added lemmas.
ffUnion_fsubset_iff
fimage_strict_mono
wfP_pfsubset
* Theory "HOL-Library.BigO" is obsolete and has been moved to
"HOL-ex.BigO" (it corresponds to "HOL-Metis_Examples.Big_O").
* Theory "HOL-Library.Multiset":
- Strengthened lemmas. Minor INCOMPATIBILITIES.
mult_cancel
mult_cancel_add_mset
mult_cancel_max
mult_cancel_max0
multeqp_code_iff_reflcl_mult
multp_cancel
multp_cancel_add_mset
multp_cancel_max
multp_code_iff_mult
- Used transp_on and reorder assumptions of lemmas bex_least_element
and bex_greatest_element. Minor INCOMPATIBILITIES.
- Added lemmas.
count_minus_inter_lt_count_minus_inter_iff
minus_inter_eq_minus_inter_iff
mult_mono_strong
multeqp_code_iff_reflclp_multp
multp_code_iff_multp
multp_image_mset_image_msetI
multp_mono_strong
multp_repeat_mset_repeat_msetI
total_mult
total_on_mult
totalp_multp
totalp_on_multp
wfP_subset_mset[simp]
* Theory "HOL-Library.Multiset_Order":
- Added lemmas.
asymp_multpHO
asymp_not_liftable_to_multpHO
asymp_on_multpHO
irreflp_on_multpHO[simp]
multpDM_mono_strong
multpDM_plus_plusI[simp]
multpHO_double_double[simp]
multpHO_iff_set_mset_lessHO_set_mset
multpHO_implies_one_step_strong
multpHO_minus_inter_minus_inter_iff
multpHO_mono_strong
multpHO_plus_plus[simp]
multpHO_repeat_mset_repeat_mset[simp]
strict_subset_implies_multpDM
strict_subset_implies_multpHO
totalp_multpDM
totalp_multpHO
totalp_on_multpDM
totalp_on_multpHO
transp_multpHO
transp_on_multpHO
* Session "HOL-Algebra": new theories "HOL-Algebra.SimpleGroups" and
"HOL-Algebra.SndIsomorphismGrp" (second isomorphism theorem for groups),
by Jakob von Raumer.
* Session "HOL-Analysis":
- Some results reformulated to use f \<in> A\<rightarrow>B rather than f`A \<subseteq> B,
INCOMPATIBILITY, use image_subset_iff_funcset to fix.
- Some results reformulated to use X = trivial_topology rather than
topspace X = {}, INCOMPATIBILITY, use null_topspace_iff_trivial to fix.
- Imported the HOL Light abstract metric space library and numerous
results in abstract topology (1200+ lemmas).
- New material on infinite sums and integration, due to Manuel Eberl
and Wenda Li.
* Session "Mirabelle": Added session name to output directory structure.
Minor INCOMPATIBILITY.
*** ML ***
* ML antiquotation \<^if_none>\<open>expr\<close> inlines a function (fn SOME x => x
| NONE => expr); this is a non-strict version of the regular function
"the_default". Both are particularly useful with the |> combinator.
* Improved implementations and signatures of functor Table() and
corresponding functor Set().
- Specific Set().T supersedes Table().set = unit table, with concrete
instances Intset, Symset, Termset etc.
- Data representation is more compact than before, approx. 85% .. 110%
of a plain list (e.g. see structure AList or Ord_List, respectively).
- The new "size" operation works with constant time complexity and
minimal space overhead: small structures have no size descriptor.
* Operations ML_Heap.sizeof1 and ML_Heap.sizeof determine the object
size on the heap in bytes. The latter works simultaneously on multiple
objects, taking implicit sharing of values into account. Examples for
the default 64_32 platform (4 bytes per machine word):
val s = "aaaabbbbcccc";
val a = ML_Heap.sizeof1 s;
(*20: 2 words descriptor + 3 words content*)
val b = ML_Heap.sizeof [s, s];
(*20: shared values without list structure*)
val c = ML_Heap.sizeof1 [s, s];
(*44 = 20 + 24: shared values + 2 * 3 words per list cons*)
* Operations for Zstd compression (via Isabelle/Scala):
Zstd.compress: Bytes.T -> Bytes.T
Zstd.uncompress: Bytes.T -> Bytes.T
*** System ***
* The command-line tool "isabelle build" now supports option -A to
include AFP as directory, without selecting any sessions yet.
* The command-line tool "isabelle profiling" produces per-session
statistics from ML heap images. Command-line options are similar to
"isabelle build". Output is in CSV format, which can be opened by common
spreadsheet applications (e.g. LibreOffice Calc).
* The command-line tool "isabelle update" is now directly based on
"isabelle build" instead of "isabelle dump". Thus it has become more
scalable, and supports most options from "isabelle build". Partial
builds are supported as well, e.g. "isabelle update -n -a".
* The command-line tool "isabelle log" has been renamed to "isabelle
build_log", to emphasize its relation to "isabelle build".
* The command-line tool "isabelle build_docker" has been renamed to
"isabelle docker_build", to emphasize its non-relation to "isabelle
build".
* System options "context_theory_tracing" and "context_proof_tracing"
store information about persistent context values (ML types theory,
local_theory, Proof.context). This may reveal "memory leaks" in
Isabelle/ML infrastructure or user tools, typically due to the lack of
Thm.trim_context when thm values are stored as theory data.
Below is a minimal example for Isabelle/ZF. The idea is to build a clean
heap image with the above options enabled, and inspect the resulting ML
heap later:
isabelle build -o context_theory_tracing -o context_proof_tracing -b -c ZF
isabelle process -l ZF -e "Session.print_context_tracing (K true)"
An alternative to "isabelle process -l ZF" is "isabelle jedit -l ZF"
with the subsequent Isar commands:
print_context_tracing
print_context_tracing ZF.Nat ZF.Int \<comment> \<open>restriction to theories\<close>
* The "rsync" tool has been bundled as Isabelle component, with uniform
version and compilation options on all platforms. This allows to use
more recent options for extra robustness, notably "--secluded-args"
(formerly "--protected-args"). Option -P of "isabelle hg_sync" and
"isabelle sync" has been eliminated accordingly.
* Remote SSH host of "isabelle hg_sync" and "isabelle sync" now works
via options -s, -p, -u. The TARGET argument is a plain file-system path
in Isabelle notation, no longer an rsync target (host:directory). Minor
INCOMPATIBILITY of command-line syntax.
* System option "build_through" determines if session builds should
observe dependency of options that contribute to the formal content.
This is specified via option tags given in etc/options (e.g. see
"isabelle options -l -t content,document"). A change of such options
causes a fresh build. For example:
isabelle build FOL
isabelle build -o show_types FOL # unchanged, no depency on options
isabelle build -o build_thorough -o show_types FOL # changed
isabelle build -o build_thorough FOL # changed
* System option "build_pide_reports" has been discontinued: it coincides
with "pide_reports".
* System option "ML_process_policy" has been renamed to
"process_policy", as it may affect other processes as well (notably in
"isabelle build").
* The command-line tools "isabelle dotnet_setup" and "isabelle dotnet"
support the Dotnet platform (.NET), which includes Fsharp (F#). This
works uniformly on all Isabelle OS platforms, even as cross-platform
installation: "isabelle dotnet_setup -p linux_arm,linux,macos,windows".
Example:
isabelle dotnet_setup
isabelle dotnet fsi
> 1 + 1;;
> #quit;;
* The headless PIDE server (e.g. command-line tool "isabelle server")
now observes the option "show_states" as given in the server command
"session_start". If enabled, the server command "use_theories" will
expose proof state output via its "messages" field.
* Isabelle server command "session_build" no longer supports the
"verbose" flag. Instead, all messages are shown unconditionally, while
the property {"verbose": bool} indicates whether the result is meant to
depend on verbose mode.
* Isabelle/Scala provides generic support for XZ and Zstd compression,
via Compress.Options and Compress.Cache. Bytes.uncompress automatically
detects the compression scheme.
* File.set_executable in Isabelle/Scala has changed its mandatory "flag"
to optional "reset", which opposite polarity. INCOMPATIBILITY.
* Update to GHC stack 2.9.3 with support for arm64-linux.
* Isabelle/Scala supports TOML (Tom's Obvious, Minimal Language), which
aims to be a minimal configuration file format. See also
https://toml.io/en/v1.0.0
* Update of Poly/ML with more robust support for ARM64 platform, notably
Apple Silicon M1/M2.
New in Isabelle2022 (October 2022)
----------------------------------
*** General ***
* The instantiation of schematic goals is now displayed explicitly as a
list of variable assignments. This works for proof state output, and at
the end of a toplevel proof. In rare situations, a proof command or
proof method may violate the intended goal discipline, by not producing
an instance of the original goal, but there is only a warning, no hard
error.
* Session ROOT files support 'chapter_definition' entries (optional).
This allows to associate additional information as follows:
- "chapter_definition NAME (GROUPS)" to make all sessions that belong
to this chapter members of the given groups
- "chapter_definition NAME description TEXT" to provide a description
for presentation purposes
* Old-style {* verbatim *} tokens have been discontinued (legacy feature
since Isabelle2019). INCOMPATIBILITY, use \<open>cartouche\<close> syntax instead.
*** Isabelle/jEdit Prover IDE ***
* Command 'print_state' outputs a plain message, i.e. "writeln" instead
of "state". Thus it is displayed in the Output panel, even if the option
"editor_output_state" is disabled.
*** Isabelle/VSCode Prover IDE ***
* VSCodium, an open-source distribution of VSCode without MS telemetry,
has been bundled with Isabelle as add-on component. The command-line
tool "isabelle vscode" automatically configures it as Isabelle/VSCode
and starts the application. This includes special support for the
UTF-8-Isabelle encoding and the corresponding Isabelle fonts.
* Command-line tools "isabelle electron" and "isabelle node" provide
access to the underlying technologies of VSCodium, for use in other
applications. This essentially provides a freely programmable Chromium
browser engine that works uniformly on all platforms.
Example:
URL="https://isabelle.in.tum.de" isabelle electron \
--app="$(isabelle getenv -b ISABELLE_HOME)"/src/Tools/Electron/test
*** HTML/PDF presentation ***
* Management of dependencies has become more robust and accurate,
following the session build hierarchy, and the up-to-date notion of
"isabelle build". Changed sessions and updated builds will cause new
HTML presentation, when that is enabled eventually. Unchanged sessions
retain their HTML output that is already present. Thus HTML presentation
for basic sessions like "HOL" and "HOL-Analysis" is produced at most
once, as required by user sessions.
* HTML presentation no longer supports README.html, which was meant as
add-on to the index.html of a session. Rare INCOMPATIBILITY, consider
using a separate theory "README" with Isabelle document markup/markdown.
* ML files (and other auxiliary files) are presented with detailed
hyperlinks, just like regular theory sources.
* Support for external hyperlinks (URLs).
* Support for internal hyperlinks to files that belong formally to the
presented session.
*** HOL ***
* HOL record types: new simproc that sorts update expressions, guarded
by configuration option "record_sort_updates" (default: false). Some
examples are in theory "HOL-Examples.Records".
* More explanations on the new, verified order prover for partial and
linear orders, which first appeared in Isabelle2021-1.
The order prover rearranges the goal to prove False, then retrieves
order literals (i.e. x = y, x <= y, x < y, and their negated versions)
from the premises and finally tries to derive a contradiction. Its main
use case is as a solver to the Simplifier, where it e.g. solves premises
of conditional rewrite rules.
The new prover (src/Provers/order_tac.ML) replaces the old prover
(src/Provers/order.ML) and improves upon the old one in several ways:
- The completeness of the prover is verified in Isabelle (see the ATVA
2021 paper "A Verified Decision Procedure for Orders in
Isabelle/HOL").
- The new prover is complete for partial orders.
- The interface to register new orders was reworked to reduce
boilerplate.
The prover has two configuration attributes that control its behaviour:
- order_trace (default: false) to enable tracing for the solver.
- order_split_limit (default: 8) to limit the number of order literals
of the form ~ x < y that are passed to the solver since those lead
to case splitting and thus exponential runtime. This only applies to
partial orders.
The prover is agnostic to the object-logic, but the default setup is for
HOL: see theory HOL.Orderings with ML structure HOL_Order_Tac. The
structure allows us to register new orders with the functions
HOL_Order_Tac.declare_order and HOL_Order_Tac.declare_linorder. Using
these functions, we register the orders of the type classes order and
linorder with the solver. If possible, one should instantiate these type
classes instead of adding new orders to the solver. One can also
interpret the type class locale as in src/HOL/Library/Sublist.thy, which
contains e.g. the prefix order on lists.
The proof method "order" invokes the prover in a standalone fashion.
The diagnostic command 'print_orders' shows all orders known to the
prover in the current context.
* Meson: added support for polymorphic "using" facts. Minor
INCOMPATIBILITY.
* Moved auxiliary computation constant "divmod_nat" to theory
"HOL.Euclidean_Division". Minor INCOMPATIBILITY.
* Renamed attribute "arith_split" to "linarith_split". Minor
INCOMPATIBILITY.
* Theory "HOL.Rings": rule split_of_bool_asm is not split any longer,
analogously to split_if_asm. INCOMPATIBILITY.
* Theory "HOL.Bit_Operations": rule bit_0 is not default [simp] any
longer. INCOMPATIBILITY.
* Streamlined primitive definitions of division and modulus on integers.
INCOMPATIBILITY.
* Theory "HOL.Fun":
- Added predicate monotone_on and redefined monotone to be an
abbreviation. Lemma monotone_def is explicitly provided for backward
compatibility but its usage is discouraged. Minor INCOMPATIBILITY.
- Changed argument order of mono_on and strict_mono_on to uniformize
with monotone_on and the general "characterizing set at the beginning
of predicates" preference. Also change them to be abbreviations
of monotone_of. Lemmas mono_on_def and strict_mono_on_def are
explicitly provided for backward compatibility but their usage is
discouraged. INCOMPATIBILITY.
- Move mono, strict_mono, antimono, and relevant lemmas to Fun theory.
Also change them to be abbreviations of mono_on, strict_mono_on,
and monotone, respectively. Lemmas mono_def, strict_mono_def, and
antimono_def are explicitly provided for backward compatibility but
their usage is discouraged. Minor INCOMPATIBILITY.
- Added lemmas.
monotone_onD
monotone_onI
monotone_on_empty[simp]
monotone_on_o
monotone_on_subset
* Theory "HOL.Relation":
- Added predicate reflp_on and redefined reflp to be an abbreviation.
Lemma reflp_def is explicitly provided for backward compatibility
but its usage is discouraged. Minor INCOMPATIBILITY.
- Added predicate totalp_on and abbreviation totalp.
- Replaced HOL.implies by Pure.imp in lemma reflp_mono for consistency
with other lemmas. Minor INCOMPATIBILITY.
- Added lemmas.
preorder.asymp_greater
preorder.asymp_less
reflp_onD
reflp_onI
reflp_on_Inf
reflp_on_Sup
reflp_on_empty[simp]
reflp_on_inf
reflp_on_mono
reflp_on_subset
reflp_on_sup
total_on_subset