forked from seL4/isabelle
/
NEWS
11821 lines (9016 loc) · 464 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
=================================================
New in this Isabelle version
----------------------------
*** HOL ***
* Sledgehammer:
- Minimization is now always enabled by default.
Removed subcommand:
min
New in Isabelle2014 (August 2014)
---------------------------------
*** General ***
* Support for official Standard ML within the Isabelle context.
Command 'SML_file' reads and evaluates the given Standard ML file.
Toplevel bindings are stored within the theory context; the initial
environment is restricted to the Standard ML implementation of
Poly/ML, without the add-ons of Isabelle/ML. Commands 'SML_import'
and 'SML_export' allow to exchange toplevel bindings between the two
separate environments. See also ~~/src/Tools/SML/Examples.thy for
some examples.
* Standard tactics and proof methods such as "clarsimp", "auto" and
"safe" now preserve equality hypotheses "x = expr" where x is a free
variable. Locale assumptions and chained facts containing "x"
continue to be useful. The new method "hypsubst_thin" and the
configuration option "hypsubst_thin" (within the attribute name space)
restore the previous behavior. INCOMPATIBILITY, especially where
induction is done after these methods or when the names of free and
bound variables clash. As first approximation, old proofs may be
repaired by "using [[hypsubst_thin = true]]" in the critical spot.
* More static checking of proof methods, which allows the system to
form a closure over the concrete syntax. Method arguments should be
processed in the original proof context as far as possible, before
operating on the goal state. In any case, the standard discipline for
subgoal-addressing needs to be observed: no subgoals or a subgoal
number that is out of range produces an empty result sequence, not an
exception. Potential INCOMPATIBILITY for non-conformant tactical
proof tools.
* Lexical syntax (inner and outer) supports text cartouches with
arbitrary nesting, and without escapes of quotes etc. The Prover IDE
supports input via ` (backquote).
* The outer syntax categories "text" (for formal comments and document
markup commands) and "altstring" (for literal fact references) allow
cartouches as well, in addition to the traditional mix of quotations.
* Syntax of document antiquotation @{rail} now uses \<newline> instead
of "\\", to avoid the optical illusion of escaped backslash within
string token. General renovation of its syntax using text cartouches.
Minor INCOMPATIBILITY.
* Discontinued legacy_isub_isup, which was a temporary workaround for
Isabelle/ML in Isabelle2013-1. The prover process no longer accepts
old identifier syntax with \<^isub> or \<^isup>. Potential
INCOMPATIBILITY.
* Document antiquotation @{url} produces markup for the given URL,
which results in an active hyperlink within the text.
* Document antiquotation @{file_unchecked} is like @{file}, but does
not check existence within the file-system.
* Updated and extended manuals: codegen, datatypes, implementation,
isar-ref, jedit, system.
*** Prover IDE -- Isabelle/Scala/jEdit ***
* Improved Document panel: simplified interaction where every single
mouse click (re)opens document via desktop environment or as jEdit
buffer.
* Support for Navigator plugin (with toolbar buttons), with connection
to PIDE hyperlinks.
* Auxiliary files ('ML_file' etc.) are managed by the Prover IDE.
Open text buffers take precedence over copies within the file-system.
* Improved support for Isabelle/ML, with jEdit mode "isabelle-ml" for
auxiliary ML files.
* Improved syntactic and semantic completion mechanism, with simple
templates, completion language context, name-space completion,
file-name completion, spell-checker completion.
* Refined GUI popup for completion: more robust key/mouse event
handling and propagation to enclosing text area -- avoid loosing
keystrokes with slow / remote graphics displays.
* Refined insertion of completion items wrt. jEdit text: multiple
selections, rectangular selections, rectangular selection as "tall
caret".
* Integrated spell-checker for document text, comments etc. with
completion popup and context-menu.
* More general "Query" panel supersedes "Find" panel, with GUI access
to commands 'find_theorems' and 'find_consts', as well as print
operations for the context. Minor incompatibility in keyboard
shortcuts etc.: replace action isabelle-find by isabelle-query.
* Search field for all output panels ("Output", "Query", "Info" etc.)
to highlight text via regular expression.
* Option "jedit_print_mode" (see also "Plugin Options / Isabelle /
General") allows to specify additional print modes for the prover
process, without requiring old-fashioned command-line invocation of
"isabelle jedit -m MODE".
* More support for remote files (e.g. http) using standard Java
networking operations instead of jEdit virtual file-systems.
* Improved Console/Scala plugin: more uniform scala.Console output,
more robust treatment of threads and interrupts.
* Improved management of dockable windows: clarified keyboard focus
and window placement wrt. main editor view; optional menu item to
"Detach" a copy where this makes sense.
* New Simplifier Trace panel provides an interactive view of the
simplification process, enabled by the "simp_trace_new" attribute
within the context.
*** Pure ***
* Low-level type-class commands 'classes', 'classrel', 'arities' have
been discontinued to avoid the danger of non-trivial axiomatization
that is not immediately visible. INCOMPATIBILITY, use regular
'instance' command with proof. The required OFCLASS(...) theorem
might be postulated via 'axiomatization' beforehand, or the proof
finished trivially if the underlying class definition is made vacuous
(without any assumptions). See also Isabelle/ML operations
Axclass.class_axiomatization, Axclass.classrel_axiomatization,
Axclass.arity_axiomatization.
* Basic constants of Pure use more conventional names and are always
qualified. Rare INCOMPATIBILITY, but with potentially serious
consequences, notably for tools in Isabelle/ML. The following
renaming needs to be applied:
== ~> Pure.eq
==> ~> Pure.imp
all ~> Pure.all
TYPE ~> Pure.type
dummy_pattern ~> Pure.dummy_pattern
Systematic porting works by using the following theory setup on a
*previous* Isabelle version to introduce the new name accesses for the
old constants:
setup {*
fn thy => thy
|> Sign.root_path
|> Sign.const_alias (Binding.qualify true "Pure" @{binding eq}) "=="
|> Sign.const_alias (Binding.qualify true "Pure" @{binding imp}) "==>"
|> Sign.const_alias (Binding.qualify true "Pure" @{binding all}) "all"
|> Sign.restore_naming thy
*}
Thus ML antiquotations like @{const_name Pure.eq} may be used already.
Later the application is moved to the current Isabelle version, and
the auxiliary aliases are deleted.
* Attributes "where" and "of" allow an optional context of local
variables ('for' declaration): these variables become schematic in the
instantiated theorem.
* Obsolete attribute "standard" has been discontinued (legacy since
Isabelle2012). Potential INCOMPATIBILITY, use explicit 'for' context
where instantiations with schematic variables are intended (for
declaration commands like 'lemmas' or attributes like "of"). The
following temporary definition may help to port old applications:
attribute_setup standard =
"Scan.succeed (Thm.rule_attribute (K Drule.export_without_context))"
* More thorough check of proof context for goal statements and
attributed fact expressions (concerning background theory, declared
hyps). Potential INCOMPATIBILITY, tools need to observe standard
context discipline. See also Assumption.add_assumes and the more
primitive Thm.assume_hyps.
* Inner syntax token language allows regular quoted strings "..."
(only makes sense in practice, if outer syntax is delimited
differently, e.g. via cartouches).
* Command 'print_term_bindings' supersedes 'print_binds' for clarity,
but the latter is retained some time as Proof General legacy.
* Code generator preprocessor: explicit control of simp tracing on a
per-constant basis. See attribute "code_preproc".
*** HOL ***
* Code generator: enforce case of identifiers only for strict target
language requirements. INCOMPATIBILITY.
* Code generator: explicit proof contexts in many ML interfaces.
INCOMPATIBILITY.
* Code generator: minimize exported identifiers by default. Minor
INCOMPATIBILITY.
* Code generation for SML and OCaml: dropped arcane "no_signatures"
option. Minor INCOMPATIBILITY.
* "declare [[code abort: ...]]" replaces "code_abort ...".
INCOMPATIBILITY.
* "declare [[code drop: ...]]" drops all code equations associated
with the given constants.
* Code generations are provided for make, fields, extend and truncate
operations on records.
* Command and antiquotation "value" are now hardcoded against nbe and
ML. Minor INCOMPATIBILITY.
* Renamed command 'enriched_type' to 'functor'. INCOMPATIBILITY.
* The symbol "\<newline>" may be used within char or string literals
to represent (Char Nibble0 NibbleA), i.e. ASCII newline.
* Qualified String.implode and String.explode. INCOMPATIBILITY.
* Simplifier: Enhanced solver of preconditions of rewrite rules can
now deal with conjunctions. For help with converting proofs, the old
behaviour of the simplifier can be restored like this: declare/using
[[simp_legacy_precond]]. This configuration option will disappear
again in the future. INCOMPATIBILITY.
* Simproc "finite_Collect" is no longer enabled by default, due to
spurious crashes and other surprises. Potential INCOMPATIBILITY.
* Moved new (co)datatype package and its dependencies from session
"HOL-BNF" to "HOL". The commands 'bnf', 'wrap_free_constructors',
'datatype_new', 'codatatype', 'primcorec', 'primcorecursive' are now
part of theory "Main".
Theory renamings:
FunDef.thy ~> Fun_Def.thy (and Fun_Def_Base.thy)
Library/Wfrec.thy ~> Wfrec.thy
Library/Zorn.thy ~> Zorn.thy
Cardinals/Order_Relation.thy ~> Order_Relation.thy
Library/Order_Union.thy ~> Cardinals/Order_Union.thy
Cardinals/Cardinal_Arithmetic_Base.thy ~> BNF_Cardinal_Arithmetic.thy
Cardinals/Cardinal_Order_Relation_Base.thy ~> BNF_Cardinal_Order_Relation.thy
Cardinals/Constructions_on_Wellorders_Base.thy ~> BNF_Constructions_on_Wellorders.thy
Cardinals/Wellorder_Embedding_Base.thy ~> BNF_Wellorder_Embedding.thy
Cardinals/Wellorder_Relation_Base.thy ~> BNF_Wellorder_Relation.thy
BNF/Ctr_Sugar.thy ~> Ctr_Sugar.thy
BNF/Basic_BNFs.thy ~> Basic_BNFs.thy
BNF/BNF_Comp.thy ~> BNF_Comp.thy
BNF/BNF_Def.thy ~> BNF_Def.thy
BNF/BNF_FP_Base.thy ~> BNF_FP_Base.thy
BNF/BNF_GFP.thy ~> BNF_GFP.thy
BNF/BNF_LFP.thy ~> BNF_LFP.thy
BNF/BNF_Util.thy ~> BNF_Util.thy
BNF/Coinduction.thy ~> Coinduction.thy
BNF/More_BNFs.thy ~> Library/More_BNFs.thy
BNF/Countable_Type.thy ~> Library/Countable_Set_Type.thy
BNF/Examples/* ~> BNF_Examples/*
New theories:
Wellorder_Extension.thy (split from Zorn.thy)
Library/Cardinal_Notations.thy
Library/BNF_Axomatization.thy
BNF_Examples/Misc_Primcorec.thy
BNF_Examples/Stream_Processor.thy
Discontinued theories:
BNF/BNF.thy
BNF/Equiv_Relations_More.thy
INCOMPATIBILITY.
* New (co)datatype package:
- Command 'primcorec' is fully implemented.
- Command 'datatype_new' generates size functions ("size_xxx" and
"size") as required by 'fun'.
- BNFs are integrated with the Lifting tool and new-style
(co)datatypes with Transfer.
- Renamed commands:
datatype_new_compat ~> datatype_compat
primrec_new ~> primrec
wrap_free_constructors ~> free_constructors
INCOMPATIBILITY.
- The generated constants "xxx_case" and "xxx_rec" have been renamed
"case_xxx" and "rec_xxx" (e.g., "prod_case" ~> "case_prod").
INCOMPATIBILITY.
- The constant "xxx_(un)fold" and related theorems are no longer
generated. Use "xxx_(co)rec" or define "xxx_(un)fold" manually
using "prim(co)rec".
INCOMPATIBILITY.
- No discriminators are generated for nullary constructors by
default, eliminating the need for the odd "=:" syntax.
INCOMPATIBILITY.
- No discriminators or selectors are generated by default by
"datatype_new", unless custom names are specified or the new
"discs_sels" option is passed.
INCOMPATIBILITY.
* Old datatype package:
- The generated theorems "xxx.cases" and "xxx.recs" have been
renamed "xxx.case" and "xxx.rec" (e.g., "sum.cases" ->
"sum.case"). INCOMPATIBILITY.
- The generated constants "xxx_case", "xxx_rec", and "xxx_size" have
been renamed "case_xxx", "rec_xxx", and "size_xxx" (e.g.,
"prod_case" ~> "case_prod"). INCOMPATIBILITY.
* The types "'a list" and "'a option", their set and map functions,
their relators, and their selectors are now produced using the new
BNF-based datatype package.
Renamed constants:
Option.set ~> set_option
Option.map ~> map_option
option_rel ~> rel_option
Renamed theorems:
set_def ~> set_rec[abs_def]
map_def ~> map_rec[abs_def]
Option.map_def ~> map_option_case[abs_def] (with "case_option" instead of "rec_option")
option.recs ~> option.rec
list_all2_def ~> list_all2_iff
set.simps ~> set_simps (or the slightly different "list.set")
map.simps ~> list.map
hd.simps ~> list.sel(1)
tl.simps ~> list.sel(2-3)
the.simps ~> option.sel
INCOMPATIBILITY.
* The following map functions and relators have been renamed:
sum_map ~> map_sum
map_pair ~> map_prod
prod_rel ~> rel_prod
sum_rel ~> rel_sum
fun_rel ~> rel_fun
set_rel ~> rel_set
filter_rel ~> rel_filter
fset_rel ~> rel_fset (in "src/HOL/Library/FSet.thy")
cset_rel ~> rel_cset (in "src/HOL/Library/Countable_Set_Type.thy")
vset ~> rel_vset (in "src/HOL/Library/Quotient_Set.thy")
INCOMPATIBILITY.
* New internal SAT solver "cdclite" that produces models and proof
traces. This solver replaces the internal SAT solvers "enumerate" and
"dpll". Applications that explicitly used one of these two SAT
solvers should use "cdclite" instead. In addition, "cdclite" is now
the default SAT solver for the "sat" and "satx" proof methods and
corresponding tactics; the old default can be restored using "declare
[[sat_solver = zchaff_with_proofs]]". Minor INCOMPATIBILITY.
* SMT module: A new version of the SMT module, temporarily called
"SMT2", uses SMT-LIB 2 and supports recent versions of Z3 (e.g.,
4.3). The new proof method is called "smt2". CVC3 and CVC4 are also
supported as oracles. Yices is no longer supported, because no version
of the solver can handle both SMT-LIB 2 and quantifiers.
* Activation of Z3 now works via "z3_non_commercial" system option
(without requiring restart), instead of former settings variable
"Z3_NON_COMMERCIAL". The option can be edited in Isabelle/jEdit menu
Plugin Options / Isabelle / General.
* Sledgehammer:
- Z3 can now produce Isar proofs.
- MaSh overhaul:
. New SML-based learning algorithms eliminate the dependency on
Python and increase performance and reliability.
. MaSh and MeSh are now used by default together with the
traditional MePo (Meng-Paulson) relevance filter. To disable
MaSh, set the "MaSh" system option in Isabelle/jEdit Plugin
Options / Isabelle / General to "none".
- New option:
smt_proofs
- Renamed options:
isar_compress ~> compress
isar_try0 ~> try0
INCOMPATIBILITY.
* Removed solvers remote_cvc3 and remote_z3. Use cvc3 and z3 instead.
* Nitpick:
- Fixed soundness bug whereby mutually recursive datatypes could
take infinite values.
- Fixed soundness bug with low-level number functions such as
"Abs_Integ" and "Rep_Integ".
- Removed "std" option.
- Renamed "show_datatypes" to "show_types" and "hide_datatypes" to
"hide_types".
* Metis: Removed legacy proof method 'metisFT'. Use 'metis
(full_types)' instead. INCOMPATIBILITY.
* Try0: Added 'algebra' and 'meson' to the set of proof methods.
* Adjustion of INF and SUP operations:
- Elongated constants INFI and SUPR to INFIMUM and SUPREMUM.
- Consolidated theorem names containing INFI and SUPR: have INF and
SUP instead uniformly.
- More aggressive normalization of expressions involving INF and Inf
or SUP and Sup.
- INF_image and SUP_image do not unfold composition.
- Dropped facts INF_comp, SUP_comp.
- Default congruence rules strong_INF_cong and strong_SUP_cong, with
simplifier implication in premises. Generalize and replace former
INT_cong, SUP_cong
INCOMPATIBILITY.
* SUP and INF generalized to conditionally_complete_lattice.
* Swapped orientation of facts image_comp and vimage_comp:
image_compose ~> image_comp [symmetric]
image_comp ~> image_comp [symmetric]
vimage_compose ~> vimage_comp [symmetric]
vimage_comp ~> vimage_comp [symmetric]
INCOMPATIBILITY.
* Theory reorganization: split of Big_Operators.thy into
Groups_Big.thy and Lattices_Big.thy.
* Consolidated some facts about big group operators:
setsum_0' ~> setsum.neutral
setsum_0 ~> setsum.neutral_const
setsum_addf ~> setsum.distrib
setsum_cartesian_product ~> setsum.cartesian_product
setsum_cases ~> setsum.If_cases
setsum_commute ~> setsum.commute
setsum_cong ~> setsum.cong
setsum_delta ~> setsum.delta
setsum_delta' ~> setsum.delta'
setsum_diff1' ~> setsum.remove
setsum_empty ~> setsum.empty
setsum_infinite ~> setsum.infinite
setsum_insert ~> setsum.insert
setsum_inter_restrict'' ~> setsum.inter_filter
setsum_mono_zero_cong_left ~> setsum.mono_neutral_cong_left
setsum_mono_zero_cong_right ~> setsum.mono_neutral_cong_right
setsum_mono_zero_left ~> setsum.mono_neutral_left
setsum_mono_zero_right ~> setsum.mono_neutral_right
setsum_reindex ~> setsum.reindex
setsum_reindex_cong ~> setsum.reindex_cong
setsum_reindex_nonzero ~> setsum.reindex_nontrivial
setsum_restrict_set ~> setsum.inter_restrict
setsum_Plus ~> setsum.Plus
setsum_setsum_restrict ~> setsum.commute_restrict
setsum_Sigma ~> setsum.Sigma
setsum_subset_diff ~> setsum.subset_diff
setsum_Un_disjoint ~> setsum.union_disjoint
setsum_UN_disjoint ~> setsum.UNION_disjoint
setsum_Un_Int ~> setsum.union_inter
setsum_Union_disjoint ~> setsum.Union_disjoint
setsum_UNION_zero ~> setsum.Union_comp
setsum_Un_zero ~> setsum.union_inter_neutral
strong_setprod_cong ~> setprod.strong_cong
strong_setsum_cong ~> setsum.strong_cong
setprod_1' ~> setprod.neutral
setprod_1 ~> setprod.neutral_const
setprod_cartesian_product ~> setprod.cartesian_product
setprod_cong ~> setprod.cong
setprod_delta ~> setprod.delta
setprod_delta' ~> setprod.delta'
setprod_empty ~> setprod.empty
setprod_infinite ~> setprod.infinite
setprod_insert ~> setprod.insert
setprod_mono_one_cong_left ~> setprod.mono_neutral_cong_left
setprod_mono_one_cong_right ~> setprod.mono_neutral_cong_right
setprod_mono_one_left ~> setprod.mono_neutral_left
setprod_mono_one_right ~> setprod.mono_neutral_right
setprod_reindex ~> setprod.reindex
setprod_reindex_cong ~> setprod.reindex_cong
setprod_reindex_nonzero ~> setprod.reindex_nontrivial
setprod_Sigma ~> setprod.Sigma
setprod_subset_diff ~> setprod.subset_diff
setprod_timesf ~> setprod.distrib
setprod_Un2 ~> setprod.union_diff2
setprod_Un_disjoint ~> setprod.union_disjoint
setprod_UN_disjoint ~> setprod.UNION_disjoint
setprod_Un_Int ~> setprod.union_inter
setprod_Union_disjoint ~> setprod.Union_disjoint
setprod_Un_one ~> setprod.union_inter_neutral
Dropped setsum_cong2 (simple variant of setsum.cong).
Dropped setsum_inter_restrict' (simple variant of setsum.inter_restrict)
Dropped setsum_reindex_id, setprod_reindex_id
(simple variants of setsum.reindex [symmetric], setprod.reindex [symmetric]).
INCOMPATIBILITY.
* Abolished slightly odd global lattice interpretation for min/max.
Fact consolidations:
min_max.inf_assoc ~> min.assoc
min_max.inf_commute ~> min.commute
min_max.inf_left_commute ~> min.left_commute
min_max.inf_idem ~> min.idem
min_max.inf_left_idem ~> min.left_idem
min_max.inf_right_idem ~> min.right_idem
min_max.sup_assoc ~> max.assoc
min_max.sup_commute ~> max.commute
min_max.sup_left_commute ~> max.left_commute
min_max.sup_idem ~> max.idem
min_max.sup_left_idem ~> max.left_idem
min_max.sup_inf_distrib1 ~> max_min_distrib2
min_max.sup_inf_distrib2 ~> max_min_distrib1
min_max.inf_sup_distrib1 ~> min_max_distrib2
min_max.inf_sup_distrib2 ~> min_max_distrib1
min_max.distrib ~> min_max_distribs
min_max.inf_absorb1 ~> min.absorb1
min_max.inf_absorb2 ~> min.absorb2
min_max.sup_absorb1 ~> max.absorb1
min_max.sup_absorb2 ~> max.absorb2
min_max.le_iff_inf ~> min.absorb_iff1
min_max.le_iff_sup ~> max.absorb_iff2
min_max.inf_le1 ~> min.cobounded1
min_max.inf_le2 ~> min.cobounded2
le_maxI1, min_max.sup_ge1 ~> max.cobounded1
le_maxI2, min_max.sup_ge2 ~> max.cobounded2
min_max.le_infI1 ~> min.coboundedI1
min_max.le_infI2 ~> min.coboundedI2
min_max.le_supI1 ~> max.coboundedI1
min_max.le_supI2 ~> max.coboundedI2
min_max.less_infI1 ~> min.strict_coboundedI1
min_max.less_infI2 ~> min.strict_coboundedI2
min_max.less_supI1 ~> max.strict_coboundedI1
min_max.less_supI2 ~> max.strict_coboundedI2
min_max.inf_mono ~> min.mono
min_max.sup_mono ~> max.mono
min_max.le_infI, min_max.inf_greatest ~> min.boundedI
min_max.le_supI, min_max.sup_least ~> max.boundedI
min_max.le_inf_iff ~> min.bounded_iff
min_max.le_sup_iff ~> max.bounded_iff
For min_max.inf_sup_aci, prefer (one of) min.commute, min.assoc,
min.left_commute, min.left_idem, max.commute, max.assoc,
max.left_commute, max.left_idem directly.
For min_max.inf_sup_ord, prefer (one of) min.cobounded1,
min.cobounded2, max.cobounded1m max.cobounded2 directly.
For min_ac or max_ac, prefer more general collection ac_simps.
INCOMPATBILITY.
* Theorem disambiguation Inf_le_Sup (on finite sets) ~>
Inf_fin_le_Sup_fin. INCOMPATIBILITY.
* Qualified constant names Wellfounded.acc, Wellfounded.accp.
INCOMPATIBILITY.
* Fact generalization and consolidation:
neq_one_mod_two, mod_2_not_eq_zero_eq_one_int ~> not_mod_2_eq_0_eq_1
INCOMPATIBILITY.
* Purely algebraic definition of even. Fact generalization and
consolidation:
nat_even_iff_2_dvd, int_even_iff_2_dvd ~> even_iff_2_dvd
even_zero_(nat|int) ~> even_zero
INCOMPATIBILITY.
* Abolished neg_numeral.
- Canonical representation for minus one is "- 1".
- Canonical representation for other negative numbers is "- (numeral _)".
- When devising rule sets for number calculation, consider the
following canonical cases: 0, 1, numeral _, - 1, - numeral _.
- HOLogic.dest_number also recognizes numerals in non-canonical forms
like "numeral One", "- numeral One", "- 0" and even "- ... - _".
- Syntax for negative numerals is mere input syntax.
INCOMPATIBILITY.
* Reduced name variants for rules on associativity and commutativity:
add_assoc ~> add.assoc
add_commute ~> add.commute
add_left_commute ~> add.left_commute
mult_assoc ~> mult.assoc
mult_commute ~> mult.commute
mult_left_commute ~> mult.left_commute
nat_add_assoc ~> add.assoc
nat_add_commute ~> add.commute
nat_add_left_commute ~> add.left_commute
nat_mult_assoc ~> mult.assoc
nat_mult_commute ~> mult.commute
eq_assoc ~> iff_assoc
eq_left_commute ~> iff_left_commute
INCOMPATIBILITY.
* Fact collections add_ac and mult_ac are considered old-fashioned.
Prefer ac_simps instead, or specify rules
(add|mult).(assoc|commute|left_commute) individually.
* Elimination of fact duplicates:
equals_zero_I ~> minus_unique
diff_eq_0_iff_eq ~> right_minus_eq
nat_infinite ~> infinite_UNIV_nat
int_infinite ~> infinite_UNIV_int
INCOMPATIBILITY.
* Fact name consolidation:
diff_def, diff_minus, ab_diff_minus ~> diff_conv_add_uminus
minus_le_self_iff ~> neg_less_eq_nonneg
le_minus_self_iff ~> less_eq_neg_nonpos
neg_less_nonneg ~> neg_less_pos
less_minus_self_iff ~> less_neg_neg [simp]
INCOMPATIBILITY.
* More simplification rules on unary and binary minus:
add_diff_cancel, add_diff_cancel_left, add_le_same_cancel1,
add_le_same_cancel2, add_less_same_cancel1, add_less_same_cancel2,
add_minus_cancel, diff_add_cancel, le_add_same_cancel1,
le_add_same_cancel2, less_add_same_cancel1, less_add_same_cancel2,
minus_add_cancel, uminus_add_conv_diff. These correspondingly have
been taken away from fact collections algebra_simps and field_simps.
INCOMPATIBILITY.
To restore proofs, the following patterns are helpful:
a) Arbitrary failing proof not involving "diff_def":
Consider simplification with algebra_simps or field_simps.
b) Lifting rules from addition to subtraction:
Try with "using <rule for addition> of [... "- _" ...]" by simp".
c) Simplification with "diff_def": just drop "diff_def".
Consider simplification with algebra_simps or field_simps;
or the brute way with
"simp add: diff_conv_add_uminus del: add_uminus_conv_diff".
* Introduce bdd_above and bdd_below in theory
Conditionally_Complete_Lattices, use them instead of explicitly
stating boundedness of sets.
* ccpo.admissible quantifies only over non-empty chains to allow more
syntax-directed proof rules; the case of the empty chain shows up as
additional case in fixpoint induction proofs. INCOMPATIBILITY.
* Removed and renamed theorems in Series:
summable_le ~> suminf_le
suminf_le ~> suminf_le_const
series_pos_le ~> setsum_le_suminf
series_pos_less ~> setsum_less_suminf
suminf_ge_zero ~> suminf_nonneg
suminf_gt_zero ~> suminf_pos
suminf_gt_zero_iff ~> suminf_pos_iff
summable_sumr_LIMSEQ_suminf ~> summable_LIMSEQ
suminf_0_le ~> suminf_nonneg [rotate]
pos_summable ~> summableI_nonneg_bounded
ratio_test ~> summable_ratio_test
removed series_zero, replaced by sums_finite
removed auxiliary lemmas:
sumr_offset, sumr_offset2, sumr_offset3, sumr_offset4, sumr_group,
half, le_Suc_ex_iff, lemma_realpow_diff_sumr,
real_setsum_nat_ivl_bounded, summable_le2, ratio_test_lemma2,
sumr_minus_one_realpow_zerom, sumr_one_lb_realpow_zero,
summable_convergent_sumr_iff, sumr_diff_mult_const
INCOMPATIBILITY.
* Replace (F)DERIV syntax by has_derivative:
- "(f has_derivative f') (at x within s)" replaces "FDERIV f x : s : f'"
- "(f has_field_derivative f') (at x within s)" replaces "DERIV f x : s : f'"
- "f differentiable at x within s" replaces "_ differentiable _ in _" syntax
- removed constant isDiff
- "DERIV f x : f'" and "FDERIV f x : f'" syntax is only available as
input syntax.
- "DERIV f x : s : f'" and "FDERIV f x : s : f'" syntax removed.
- Renamed FDERIV_... lemmas to has_derivative_...
- renamed deriv (the syntax constant used for "DERIV _ _ :> _") to DERIV
- removed DERIV_intros, has_derivative_eq_intros
- introduced derivative_intros and deriative_eq_intros which
includes now rules for DERIV, has_derivative and
has_vector_derivative.
- Other renamings:
differentiable_def ~> real_differentiable_def
differentiableE ~> real_differentiableE
fderiv_def ~> has_derivative_at
field_fderiv_def ~> field_has_derivative_at
isDiff_der ~> differentiable_def
deriv_fderiv ~> has_field_derivative_def
deriv_def ~> DERIV_def
INCOMPATIBILITY.
* Include more theorems in continuous_intros. Remove the
continuous_on_intros, isCont_intros collections, these facts are now
in continuous_intros.
* Theorems about complex numbers are now stated only using Re and Im,
the Complex constructor is not used anymore. It is possible to use
primcorec to defined the behaviour of a complex-valued function.
Removed theorems about the Complex constructor from the simpset, they
are available as the lemma collection legacy_Complex_simps. This
especially removes
i_complex_of_real: "ii * complex_of_real r = Complex 0 r".
Instead the reverse direction is supported with
Complex_eq: "Complex a b = a + \<i> * b"
Moved csqrt from Fundamental_Algebra_Theorem to Complex.
Renamings:
Re/Im ~> complex.sel
complex_Re/Im_zero ~> zero_complex.sel
complex_Re/Im_add ~> plus_complex.sel
complex_Re/Im_minus ~> uminus_complex.sel
complex_Re/Im_diff ~> minus_complex.sel
complex_Re/Im_one ~> one_complex.sel
complex_Re/Im_mult ~> times_complex.sel
complex_Re/Im_inverse ~> inverse_complex.sel
complex_Re/Im_scaleR ~> scaleR_complex.sel
complex_Re/Im_i ~> ii.sel
complex_Re/Im_cnj ~> cnj.sel
Re/Im_cis ~> cis.sel
complex_divide_def ~> divide_complex_def
complex_norm_def ~> norm_complex_def
cmod_def ~> norm_complex_de
Removed theorems:
complex_zero_def
complex_add_def
complex_minus_def
complex_diff_def
complex_one_def
complex_mult_def
complex_inverse_def
complex_scaleR_def
INCOMPATIBILITY.
* Theory Lubs moved HOL image to HOL-Library. It is replaced by
Conditionally_Complete_Lattices. INCOMPATIBILITY.
* HOL-Library: new theory src/HOL/Library/Tree.thy.
* HOL-Library: removed theory src/HOL/Library/Kleene_Algebra.thy; it
is subsumed by session Kleene_Algebra in AFP.
* HOL-Cardinals: new theory src/HOL/Cardinals/Ordinal_Arithmetic.thy.
* HOL-Word: bit representations prefer type bool over type bit.
INCOMPATIBILITY.
* HOL-Word:
- Abandoned fact collection "word_arith_alts", which is a duplicate
of "word_arith_wis".
- Dropped first (duplicated) element in fact collections
"sint_word_ariths", "word_arith_alts", "uint_word_ariths",
"uint_word_arith_bintrs".
* HOL-Number_Theory:
- consolidated the proofs of the binomial theorem
- the function fib is again of type nat => nat and not overloaded
- no more references to Old_Number_Theory in the HOL libraries
(except the AFP)
INCOMPATIBILITY.
* HOL-Multivariate_Analysis:
- Type class ordered_real_vector for ordered vector spaces.
- New theory Complex_Basic_Analysis defining complex derivatives,
holomorphic functions, etc., ported from HOL Light's canal.ml.
- Changed order of ordered_euclidean_space to be compatible with
pointwise ordering on products. Therefore instance of
conditionally_complete_lattice and ordered_real_vector.
INCOMPATIBILITY: use box instead of greaterThanLessThan or
explicit set-comprehensions with eucl_less for other (half-)open
intervals.
- removed dependencies on type class ordered_euclidean_space with
introduction of "cbox" on euclidean_space
- renamed theorems:
interval ~> box
mem_interval ~> mem_box
interval_eq_empty ~> box_eq_empty
interval_ne_empty ~> box_ne_empty
interval_sing(1) ~> cbox_sing
interval_sing(2) ~> box_sing
subset_interval_imp ~> subset_box_imp
subset_interval ~> subset_box
open_interval ~> open_box
closed_interval ~> closed_cbox
interior_closed_interval ~> interior_cbox
bounded_closed_interval ~> bounded_cbox
compact_interval ~> compact_cbox
bounded_subset_closed_interval_symmetric ~> bounded_subset_cbox_symmetric
bounded_subset_closed_interval ~> bounded_subset_cbox
mem_interval_componentwiseI ~> mem_box_componentwiseI
convex_box ~> convex_prod
rel_interior_real_interval ~> rel_interior_real_box
convex_interval ~> convex_box
convex_hull_eq_real_interval ~> convex_hull_eq_real_cbox
frechet_derivative_within_closed_interval ~> frechet_derivative_within_cbox
content_closed_interval' ~> content_cbox'
elementary_subset_interval ~> elementary_subset_box
diameter_closed_interval ~> diameter_cbox
frontier_closed_interval ~> frontier_cbox
frontier_open_interval ~> frontier_box
bounded_subset_open_interval_symmetric ~> bounded_subset_box_symmetric
closure_open_interval ~> closure_box
open_closed_interval_convex ~> open_cbox_convex
open_interval_midpoint ~> box_midpoint
content_image_affinity_interval ~> content_image_affinity_cbox
is_interval_interval ~> is_interval_cbox + is_interval_box + is_interval_closed_interval
bounded_interval ~> bounded_closed_interval + bounded_boxes
- respective theorems for intervals over the reals:
content_closed_interval + content_cbox
has_integral + has_integral_real
fine_division_exists + fine_division_exists_real
has_integral_null + has_integral_null_real
tagged_division_union_interval + tagged_division_union_interval_real
has_integral_const + has_integral_const_real
integral_const + integral_const_real
has_integral_bound + has_integral_bound_real
integrable_continuous + integrable_continuous_real
integrable_subinterval + integrable_subinterval_real
has_integral_reflect_lemma + has_integral_reflect_lemma_real
integrable_reflect + integrable_reflect_real
integral_reflect + integral_reflect_real
image_affinity_interval + image_affinity_cbox
image_smult_interval + image_smult_cbox
integrable_const + integrable_const_ivl
integrable_on_subinterval + integrable_on_subcbox
- renamed theorems:
derivative_linear ~> has_derivative_bounded_linear
derivative_is_linear ~> has_derivative_linear
bounded_linear_imp_linear ~> bounded_linear.linear
* HOL-Probability:
- replaced the Lebesgue integral on real numbers by the more general
Bochner integral for functions into a real-normed vector space.
integral_zero ~> integral_zero / integrable_zero
integral_minus ~> integral_minus / integrable_minus
integral_add ~> integral_add / integrable_add
integral_diff ~> integral_diff / integrable_diff
integral_setsum ~> integral_setsum / integrable_setsum
integral_multc ~> integral_mult_left / integrable_mult_left
integral_cmult ~> integral_mult_right / integrable_mult_right
integral_triangle_inequality~> integral_norm_bound
integrable_nonneg ~> integrableI_nonneg
integral_positive ~> integral_nonneg_AE
integrable_abs_iff ~> integrable_abs_cancel
positive_integral_lim_INF ~> positive_integral_liminf
lebesgue_real_affine ~> lborel_real_affine
borel_integral_has_integral ~> has_integral_lebesgue_integral
integral_indicator ~>
integral_real_indicator / integrable_real_indicator
positive_integral_fst ~> positive_integral_fst'
positive_integral_fst_measurable ~> positive_integral_fst
positive_integral_snd_measurable ~> positive_integral_snd
integrable_fst_measurable ~>
integral_fst / integrable_fst / AE_integrable_fst
integrable_snd_measurable ~>
integral_snd / integrable_snd / AE_integrable_snd
integral_monotone_convergence ~>
integral_monotone_convergence / integrable_monotone_convergence
integral_monotone_convergence_at_top ~>
integral_monotone_convergence_at_top /
integrable_monotone_convergence_at_top
has_integral_iff_positive_integral_lebesgue ~>
has_integral_iff_has_bochner_integral_lebesgue_nonneg
lebesgue_integral_has_integral ~>
has_integral_integrable_lebesgue_nonneg
positive_integral_lebesgue_has_integral ~>
integral_has_integral_lebesgue_nonneg /
integrable_has_integral_lebesgue_nonneg
lebesgue_integral_real_affine ~>
positive_integral_real_affine
has_integral_iff_positive_integral_lborel ~>
integral_has_integral_nonneg / integrable_has_integral_nonneg
The following theorems where removed:
lebesgue_integral_nonneg
lebesgue_integral_uminus
lebesgue_integral_cmult
lebesgue_integral_multc
lebesgue_integral_cmult_nonneg
integral_cmul_indicator
integral_real
- Renamed positive_integral to nn_integral:
. Renamed all lemmas "*positive_integral*" to *nn_integral*"
positive_integral_positive ~> nn_integral_nonneg
. Renamed abbreviation integral\<^sup>P to integral\<^sup>N.
- Formalized properties about exponentially, Erlang, and normal
distributed random variables.
* HOL-Decision_Procs: Separate command 'approximate' for approximative
computation in src/HOL/Decision_Procs/Approximation. Minor
INCOMPATIBILITY.
*** Scala ***
* The signature and semantics of Document.Snapshot.cumulate_markup /
select_markup have been clarified. Markup is now traversed in the
order of reports given by the prover: later markup is usually more
specific and may override results accumulated so far. The elements
guard is mandatory and checked precisely. Subtle INCOMPATIBILITY.
* Substantial reworking of internal PIDE protocol communication
channels. INCOMPATIBILITY.
*** ML ***
* Subtle change of semantics of Thm.eq_thm: theory stamps are not
compared (according to Thm.thm_ord), but assumed to be covered by the
current background theory. Thus equivalent data produced in different
branches of the theory graph usually coincides (e.g. relevant for
theory merge). Note that the softer Thm.eq_thm_prop is often more
appropriate than Thm.eq_thm.
* Proper context for basic Simplifier operations: rewrite_rule,
rewrite_goals_rule, rewrite_goals_tac etc. INCOMPATIBILITY, need to
pass runtime Proof.context (and ensure that the simplified entity
actually belongs to it).
* Proper context discipline for read_instantiate and instantiate_tac:
variables that are meant to become schematic need to be given as
fixed, and are generalized by the explicit context of local variables.
This corresponds to Isar attributes "where" and "of" with 'for'
declaration. INCOMPATIBILITY, also due to potential change of indices
of schematic variables.
* Moved ML_Compiler.exn_trace and other operations on exceptions to
structure Runtime. Minor INCOMPATIBILITY.
* Discontinued old Toplevel.debug in favour of system option
"ML_exception_trace", which may be also declared within the context
via "declare [[ML_exception_trace = true]]". Minor INCOMPATIBILITY.
* Renamed configuration option "ML_trace" to "ML_source_trace". Minor
INCOMPATIBILITY.
* Configuration option "ML_print_depth" controls the pretty-printing
depth of the ML compiler within the context. The old print_depth in
ML is still available as default_print_depth, but rarely used. Minor
INCOMPATIBILITY.
* Toplevel function "use" refers to raw ML bootstrap environment,
without Isar context nor antiquotations. Potential INCOMPATIBILITY.
Note that 'ML_file' is the canonical command to load ML files into the
formal context.