-
Notifications
You must be signed in to change notification settings - Fork 40
/
Copy pathNEWS
18404 lines (14081 loc) · 726 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 ***
* The Simplifier now supports special "congprocs", using keyword
'congproc' or 'weak_congproc' in the 'simproc_setup' command (or ML
antiquotation of the same name). See also
~~/src/HOL/Imperative_HOL/ex/Congproc_Ex.thy for further explanations
and examples.
* The attribute "cong_format" produces the internal format of Simplifier
"cong" rules, notably for congproc implementations.
*** Inner syntax --- the term language ***
* Markup for free variables now works uniformly for parsing and
printing, concerning declaration scopes and highlighting of undeclared
variables.
* Syntax translations now work in a local theory context, notably within
"bundle begin ... end".
* Syntax translations now support formal dependencies via commands
'syntax_types' or 'syntax_consts'. This is essentially an abstract
specification of the effect of 'translations' (or translation functions
in ML). Most Isabelle theories have been adapted accordingly, such that
hyperlinks work properly e.g. for "['a, 'b] \<Rightarrow> 'c" or "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> C" in
Pure, and "\<forall>x\<in>A. B x" or "\<exists>x\<in>A. B x" in HOL.
* Pattern matching of AST constant "c" works for ("_constrain" "c" T) if
the type T encodes a position (from parsing) or if constraints are
considered optional (for printing): the type is dropped in both cases.
Likewise, the printing of ASTs wrt. mixfix syntax has been adapted to
accept "c" or ("_constrain" "c" T).
* Parsing now supports type constraints for logical constants that carry
mixfix syntax (as before for constants without notation). Rare
INCOMPATIBILITY for ML translation functions: need to cope with ASTs
like ("_constrain" "c" T) or pre-terms Const ("_type_constraint_", _) $
Const ("c", _). Translation rules (command 'translations') usually work
without changes, because pattern matching has become more liberal wrt.
type constraints.
* Printing now supports type constraints for logical constants, with or
without mixfix syntax. This is guarded by the configuration options
"show_consts_markup" (default true) and "show_markup" (default true for
PIDE interaction). AST translation rules (command 'translations')
already work with extra type constraints, but the result omits the type
of a matched constant. ML translation functions (command
'print_ast_translation') based on Ast.unfold_ast etc. work in the same
manner, but more complex translations may require manual changes: rare
INCOMPATIBILITY.
* Printing term abbreviations now uses more efficient matching and
rewrite strategy: alternate top-down, bottom-up, top-down etc. until a
normal form is reached. This usually works better than the former
top-down strategy, it also conforms to AST rewriting (command
'translations'). Rare INCOMPATIBILITY, slightly different results could
be printed.
* Blocks in mixfix annotations now support properties "open_block"
(bool) and "notation" (string as cartouche). When "open_block" is
enabled, the block has no impact on formatting, but it may carry markup
information via "notation". The latter uses formal kinds (e.g. "mixfix",
"infix", "binder") together with informal words to describe the
notation. This markup affects both parsing and printing --- it can be
explored via mouse hovering in the Prover IDE, or programmatically by
Isabelle/Scala tools. Markup for "infix" and "binder" declarations are
automatic, but general mixfix forms require manual annotations in the
theory library. Plenty of existing examples may be found in the Isabelle
sources by searching for "notation=" (without quotes and no extra
space). Occasional INCOMPATIBILITY for 'no_syntax' or 'no_notation'
declarations in user applications: the mixfix template needs to be
adapted accordingly, but it is often better to use "unbundle no
foobar_syntax", as explained for HOL libraries below.
* The option "show_brackets" has been discontinued: its inaccurate
placement of extra parentheses has been superseded by markup of mixfix
blocks (which allows to explore subterm structure in the Prover IDE via
C-mouse hovering).
* Command "unbundle b" and its variants like "context includes b" allow
an optional name prefix with the reserved word "no": "unbundle no b"
etc. This reverses both the order and polarity of bundled declarations
like 'notation' vs. 'no_notation', and thus avoids redundant bundle
definitions like "foobar_syntax" vs. "no_foobar_syntax", because "no
foobar_syntax" may be used instead. Consequently, the syntax for
multiple bundle names has been changed slightly, demanding an explicit
'and' keyword. Minor INCOMPATIBILITY.
* Command "open_bundle b" is like "bundle b" followed by "unbundle b",
so its declarations are applied immediately, but also named for later
re-use: "unbundle no b" etc.
* Various HOL declaration bundles support adhoc modification of
notation, notably like this:
unbundle no abs_syntax
unbundle no binomial_syntax
unbundle no converse_syntax
unbundle no floor_ceiling_syntax
unbundle no funcset_syntax
unbundle no let_syntax
unbundle no list_comprehension_syntax
unbundle no list_enumeration_syntax
unbundle no list_maplet_syntax
unbundle no list_syntax
unbundle no list_update_syntax
unbundle no maplet_syntax
unbundle no prod_list_syntax
unbundle no reflcl_syntax
unbundle no relcomp_syntax
unbundle no rtrancl_syntax
unbundle no set_enumeration_syntax
unbundle no sum_list_syntax
unbundle no trancl_syntax
unbundle no tuple_syntax
unbundle no uminus_syntax
unbundle no update_syntax
This is more robust than individual 'no_syntax' / 'no_notation'
commands, which need to copy mixfix declarations from elsewhere and thus
break after changes in the library.
* Theory "HOL-Library.Datatype_Records" provides bundle
"datatype_record_syntax" to exchange its alternative notation versus
regular "record_syntax". This also allows to swap record syntax later
on, notably like this:
unbundle no datatype_record_syntax
* Printing of constants and bound variables is more careful to avoid
free variables, and fixed variables with mixfix syntax (including
'structure'). Rare INCOMPATIBILITY, e.g. in "subgoal_tac", "rule_tac".
*** Isabelle/jEdit Prover IDE ***
* Action isabelle.select_structure (with keyboard shortcut C+7) extends
the editor selection by adding the enclosing formal structure, based on
formal markup by the prover. Repeated invocation of this action extends
the selection incrementally.
* The Output dockable (and its variants used elsewhere) has been
improved as follows:
- Its vertical scroll position is maintained more carefully, when
messages are printed incrementally.
- Performance of printing messages repeatedly has improved slightly,
with less load on the GUI thread.
- Highlighting works via mouse hovering alone, without requiring
C-modifier.
- Search results are shown as tree view.
* An active highlight area in the input buffer or output panel may be
turned into a text selection by using the ALT modifier.
* The "Documentation" panel supports plain text files again, notably
"jedit-changes". This was broken in Isabelle2022, Isabelle2023,
Isabelle2024.
* Text rendering performance on macOS may be improved by using old
OpenGL instead of new Metal. This is controlled by the java command-line
option "-Dsun.java2d.metal=false", which is now the default.
* Update to jEdit 5.7.0, the latest release.
*** Isabelle/VSCode Prover IDE ***
* General improvements: Persistent decorations for PIDE markup, correct
font and formatting in panels, and proper completions. Moreover, the
PIDE extension of the LSP now features additional protocol messages
(e.g. to obtain the set of Isabelle symbols) and more fine-grained
control for recoding of Unicode symbols.
* Active "sendback" markup can now be used via LSP code actions, e.g. to
insert proof methods from Sledgehammer output.
* Relevant Isabelle options can now be overriden from the
Isabelle/VSCode extension settings.
*** Document preparation ***
* LaTeX output from printed entities (types, terms, thms) now contains
additional markup as follows:
tclass -- type class "a"
tconst -- type constructor "a"
tfree -- free type variable "'a"
tvar -- schematic type variable "?'a"
const -- constant "a"
free -- free variable "a"
bound -- bound variable "a"
skolem -- skolem variable "a"
var -- schematic variable "?a"
These markup names are turned into LaTeX macros using the prefix "\isa",
e.g. "\isaconst{...}" for "const". By default, these macros have no
effect, but may be defined in root.tex like this:
\renewcommand{\isatconst}[1]{{\color{darkgray}#1}}
\renewcommand{\isaconst}[1]{\textsl{\color{darkgray}#1}}
* LaTeX presentation of outer syntax keywords now distinguishes
keyword1, keyword2, keyword3 more carefully. This allows to imitate
Isabelle/jEdit rendering like this:
\renewcommand{\isacommand}[1]{\isakeywordONE{#1}}
\renewcommand{\isakeywordONE}[1]{\isakeyword{\color[RGB]{0,102,153}#1}}
\renewcommand{\isakeywordTWO}[1]{\isakeyword{\color[RGB]{0,153,102}#1}}
\renewcommand{\isakeywordTHREE}[1]{\isakeyword{\color[RGB]{0,153,255}#1}}
*** HOL ***
* Code generator: command 'code_reserved' now uses parentheses for
target languages, similar to 'code_printing'.
* Theory HOL-Library.Code_Target_Bit_Shifts implemented bit shifts on numeric
types by target-language operations; this is also used by
HOL-Library.Code_Target_Numeral.
* Sledgehammer:
- Update of bundled provers:
. E 3.1 -- with patch on Windows/Cygwin for proper interrupts
- Added instantiations of facts using the "of" attribute
(e.g. "assms(1)[of x]"), which can be activated using the
Sledgehammer option "instantiate" (default: smart, i.e. only if
preplaying failed). This uses Metis internally to infer the
variable instantiations (see below).
- Added extensionality (fact "ext") to some "metis (lifting)" calls.
- Use pretty-printing to format suggested one-line proofs.
* Metis:
- Added inference of variable instantiations, which can be activated
using the configuration option "metis_instantiate" (default: false).
This outputs a suggestion with instantiations of the facts using the
"of" attribute (e.g. "assms(1)[of x]").
* Theory HOL-Library.Discrete has been renamed
HOL-Library.Discrete_Functions
Discrete.log -> floor_log
Discrete.sqrt -> floor_sqrt
Renamed lemmas accordingly (...log/sqrt... -> ...floor_log/sqrt...)
* Theory "HOL.Wellfounded":
- Removed lemma wellorder.wfP_less. Use wellorder.wfp_on_less instead.
Minor INCOMPATIBILITY.
- Renamed lemmas. Minor INCOMPATIBILITY.
accp_wfPD ~> accp_wfpD
accp_wfPI ~> accp_wfpI
wfPUNIVI ~> wfpUNIVI
wfP_SUP ~> wfp_SUP
wfP_accp_iff ~> wfp_iff_accp
wfP_acyclicP ~> wfp_acyclicP
wfP_def ~> wfp_def
wfP_empty ~> wfp_empty
wfP_eq_minimal ~> wfp_eq_minimal
wfP_if_convertible_to_nat ~> wfp_if_convertible_to_nat
wfP_if_convertible_to_wfP ~> wfp_if_convertible_to_wfp
wfP_imp_asymp ~> wfp_imp_asymp
wfP_imp_irreflp ~> wfp_imp_irreflp
wfP_induct ~> wfp_induct
wfP_induct_rule ~> wfp_induct_rule
wfP_subset ~> wfp_subset
wfP_trancl ~> wfp_tranclp
wfP_wf_eq ~> wfp_wf_eq
wf_acc_iff ~> wf_iff_acc
- Added lemmas.
wf_on_antimono_stronger
wfp_on_antimono_stronger
* Theory "HOL-Library.Multiset":
- Renamed lemmas. Minor INCOMPATIBILITY.
wfP_less_multiset ~> wfp_less_multiset
wfP_multp ~> wfp_multp
wfP_subset_mset ~> wfp_subset_mset
- Added lemmas.
image_mset_diff_if_inj
minus_add_mset_if_not_in_lhs[simp]
* Transitional theory "HOL.Divides" moved to "HOL-Library.Divides" and
supposed to be removed in a future release. Minor INCOMPATIBILITY.
Import "HOL-Library.Divides" and keep an eye on qualified names with prefix
"Divides" to ease transition.
* The real-valued versions of ln, log, powr have been totalised by "ln 0
= x" and "ln (- x) = ln x". Many related theorems are now unconditional,
with ln_mult_pos and ln_divide_pos introduced for legacy purposes.
*** ML ***
* Term.variant_bounds replaces former Term.variant_frees for logical
manipulation of terms, without inner-syntax operations (e.g. reading a
term in the context of goal parameters). In contrast, former
Term.variant_frees made some attempts to work with constants as well,
but without taking the formal name space or abbreviations into account.
The existing operations Logic.goal_params, Logic.concl_of_goal,
Logic.prems_of_goal are now based on Term.variant_bounds, and thus
change their semantics silently! Rare INCOMPATIBILITY, better use
Variable.variant_names or Variable.focus_params, instead of
Logic.goal_params etc.
* Antiquotation \<^bundle>\<open>name\<close> inlines a formally checked bundle name.
* The new operation Pattern.rewrite_term_yoyo alternates top-down,
bottom-up, top-down etc. until a normal form is reached. This often
works better than former rewrite_term_top --- that is still available,
but has been renamed to rewrite_term_topdown to emphasize that something
notable has changed here.
* Constructors for type Pretty.T (such as Pretty.str, Pretty.mark_str,
Pretty.markup_block) are now value-oriented. Use of the global
print_mode is restricted to ultimate Pretty.string_of (and some
variants), while the underlying Pretty.output operation supports an
explicit Pretty.output_ops argument for alternative applications.
* Pretty.pure_output_ops and Pretty.pure_string_of support
pretty-printed output without PIDE markup. This is occasionally useful
for special tools, in contrast to regular user output. Manipulation of
the print_mode via (Print_Mode.setmp []) is no longer required.
* The print_mode "latex" only affects inner syntax variants, while its
impact on Output/Markup/Pretty operations has been removed. Thus the
print_mode operations Output.output and Output.escape have become
obsolete: superseded by Latex.output_ and Latex.escape specifically for
LaTeX. Rare INCOMPATIBILITY for ambitious document antiquotations that
generate Latex source on their own account, instead of using regular
Pretty.T interfaces (that are based on Latex.output_ops internally).
Note that basic Markup.markup cannot be used for Latex output: proper
Pretty.T operations are required (e.g. Pretty.mark_str).
*** System ***
* Find_Facts is a full-text search engine as web application based on
Apache Solr (see also https://solr.apache.org). Minimal example:
isabelle find_facts_index HOL
isabelle find_facts_server
open http://localhost:8080/app#search?q=Hilbert
Persistent data is stored in $ISABELLE_HOME_USER/find_facts/.
* The Build_Manager module has replaced previous glue-code for Jenkins
integration. The module contains a server that coordinates continuous
integration jobs and user-submitted build tasks and displays them via
web front-end. Users can submit tasks in the same manner as with the
local build tool, for example:
isabelle build_task -o build_manager_ssh_user=huch -c -A: -a -X slow
This requires SSH access to the server and membership in a common Unix
group (same requirements as push access to the Isabelle repository).
* The Isabelle/Scala type Bytes has become more scalable, with support
for incremental construction via Bytes.Builder. There is no longer an
artificial size limit, in contrast to Java byte arrays (max. 2 GiB).
Bytes operations on files, streams, encode/decode, compress/uncompress,
etc. have become more efficient, and bypass Java strings (max. 1 GiB).
In particular, YXML parsing and printing now works on very large byte
vectors as well: only the individual content nodes are limited by the
built-in string size.
* Update to current Phorge (formerly Phabricator) on Ubuntu 22.04 and
24.04; see also https://we.phorge.it/w/changelog/2024.35/. The Isabelle
"system" manual now refers to the project as "Phorge", but "phabricator"
remains for formal names (files, DNS etc.).
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