--- a/Admin/components/bundled-windows Mon Sep 20 14:24:11 2021 +0200
+++ b/Admin/components/bundled-windows Thu Oct 07 10:20:10 2021 +0200
@@ -1,3 +1,3 @@
#additional components to be bundled for release
-cygwin-20201130
+cygwin-20211004
windows_app-20181006
--- a/Admin/components/components.sha1 Mon Sep 20 14:24:11 2021 +0200
+++ b/Admin/components/components.sha1 Thu Oct 07 10:20:10 2021 +0200
@@ -68,6 +68,7 @@
0107343cd2562618629f73b2581168f0045c3234 cygwin-20201002.tar.gz
a3d481401b633c0ee6abf1da07d75da94076574c cygwin-20201130.tar.gz
5b1820b87b25d8f2d237515d9854e3ce54ee331b cygwin-20211002.tar.gz
+5dff30be394d88dd83ea584fa6f8063bdcdc21fd cygwin-20211004.tar.gz
0fe549949a025d65d52d6deca30554de8fca3b6e e-1.5.tar.gz
2e293256a134eb8e5b1a283361b15eb812fbfbf1 e-1.6-1.tar.gz
e1919e72416cbd7ac8de5455caba8901acc7b44d e-1.6-2.tar.gz
@@ -81,6 +82,7 @@
6b962a6b4539b7ca4199977973c61a8c98a492e8 e-2.0.tar.gz
66449a7b68b7d85a7189e10735a81069356123b6 e-2.5-1.tar.gz
813b66ca151d7a39b5cacb39ab52acabc2a54845 e-2.5.tar.gz
+6e63f9f354b8c06035952845b987080699a12d55 e-2.6-1.tar.gz
a3bebab5df4294dac2dd7fd2065a94df00e0b3ff e-2.6.tar.gz
6d34b18ca0aa1e10bab6413045d079188c0e2dfb exec_process-1.0.1.tar.gz
8b9bffd10e396d965e815418295f2ee2849bea75 exec_process-1.0.2.tar.gz
@@ -124,6 +126,7 @@
b166b4bd583b6442a5d75eab06f7adbb66919d6d isabelle_fonts-20210319.tar.gz
9467ad54a9ac10a6e7e8db5458d8d2a5516eba96 isabelle_fonts-20210321.tar.gz
1f7a0b9829ecac6552b21e995ad0f0ac168634f3 isabelle_fonts-20210322.tar.gz
+667000ce6dd6ea3c2d11601a41c206060468807d isabelle_fonts-20211004.tar.gz
916adccd2f40c55116b68b92ce1eccb24d4dd9a2 isabelle_setup-20210630.tar.gz
c611e363287fcc9bdd93c33bef85fa4e66cd3f37 isabelle_setup-20210701.tar.gz
a0e7527448ef0f7ce164a38a50dc26e98de3cad6 isabelle_setup-20210709.tar.gz
@@ -273,6 +276,7 @@
002f74c9e65e650de2638bf54d7b012b8de76c28 opam-2.0.3.tar.gz
ddb3b438430d9565adbf5e3d913bd52af8337511 opam-2.0.6.tar.gz
fc66802c169f44511d3be30435eb89a11e635742 opam-2.0.7.tar.gz
+108e947d17e9aa6170872614492d8f647802f483 opam-2.1.0.tar.gz
1c8cb6a8f4cbeaedce2d6d1ba8fc7e2ab3663aeb polyml-5.4.1.tar.gz
a3f9c159a0ee9a63b7a5d0c835ed9c2c908f8b56 polyml-5.5.0-1.tar.gz
7d604a99355efbfc1459d80db3279ffa7ade3e39 polyml-5.5.0-2.tar.gz
@@ -409,10 +413,13 @@
e8648878f908e93d64a393231ab21fdac976a9c2 sumatra_pdf-3.3.3.tar.gz
869ea6d8ea35c8ba68d7fcb028f16b2b7064c5fd vampire-1.0.tar.gz
399f687b56575b93e730f68c91c989cb48aa34d8 vampire-4.2.2.tar.gz
+0402978ca952f08eea73e483b694928ac402a304 vampire-4.5.1-1.tar.gz
26d9d171e169c6420a08aa99eda03ef5abb9c545 vampire-4.5.1.tar.gz
+4571c042efd6fc3097e105a528826959acd888a3 vampire-4.6.tar.gz
98c5c79fef7256db9f64c8feea2edef0a789ce46 verit-2016post.tar.gz
52ba18a6c96b53c5ae9b179d5a805a0c08f1da6d verit-2020.10-rmx-1.tar.gz
b6706e74e20e14038e9b38f0acdb5639a134246a verit-2020.10-rmx.tar.gz
+d33e1e36139e86b9e9a48d8b46a6f90d7863a51c verit-2021.06-rmx-1.tar.gz
c11d1120fcefaec79f099fe2be05b03cd2aed8b9 verit-2021.06-rmx.tar.gz
81d21dfd0ea5c58f375301f5166be9dbf8921a7a windows_app-20130716.tar.gz
fe15e1079cf5ad86f3cbab4553722a0d20002d11 windows_app-20130905.tar.gz
@@ -445,4 +452,5 @@
aa20745f0b03e606b1a4149598e0c7572b63c657 z3-4.8.3.tar.gz
9dfeb39c87393af7b6a34118507637aa53aca05e zipperposition-2.0-1.tar.gz
b884c60653002a7811e3b652ae0515e825d98667 zipperposition-2.0.tar.gz
+b129ec4f8a4474953ec107536298ee08a01fbebc zipperposition-2.1-1.tar.gz
5f53a77efb5cbe9d0c95d74a1588cc923bd711a7 zipperposition-2.1.tar.gz
--- a/Admin/components/main Mon Sep 20 14:24:11 2021 +0200
+++ b/Admin/components/main Thu Oct 07 10:20:10 2021 +0200
@@ -4,10 +4,10 @@
bib2xhtml-20190409
csdp-6.1.1
cvc4-1.8
-e-2.6
+e-2.6-1
flatlaf-1.6
idea-icons-20210508
-isabelle_fonts-20210322
+isabelle_fonts-20211004
isabelle_setup-20210922
jdk-17+35
jedit-20210802
@@ -24,8 +24,8 @@
sqlite-jdbc-3.36.0.3
ssh-java-20190323
stack-2.7.3
-vampire-4.5.1
-verit-2021.06-rmx
+vampire-4.6
+verit-2021.06-rmx-1
xz-java-1.9
z3-4.4.0pre-3
-zipperposition-2.1
+zipperposition-2.1-1
--- a/Admin/isabelle_fonts/IsabelleSymbols.sfd Mon Sep 20 14:24:11 2021 +0200
+++ b/Admin/isabelle_fonts/IsabelleSymbols.sfd Thu Oct 07 10:20:10 2021 +0200
@@ -20,7 +20,7 @@
OS2_WeightWidthSlopeOnly: 0
OS2_UseTypoMetrics: 1
CreationTime: 1050361371
-ModificationTime: 1616429436
+ModificationTime: 1633346733
PfmFamily: 17
TTFWeight: 400
TTFWidth: 5
@@ -2242,11 +2242,11 @@
DisplaySize: -96
AntiAlias: 1
FitToEm: 1
-WinInfo: 10980 12 6
+WinInfo: 8196 12 6
BeginPrivate: 0
EndPrivate
TeXData: 1 0 0 631296 315648 210432 572416 -1048576 210432 783286 444596 497025 792723 393216 433062 380633 303038 157286 324010 404750 52429 2506097 1059062 262144
-BeginChars: 1114189 1462
+BeginChars: 1114189 1463
StartChar: u10000
Encoding: 65536 65536 0
@@ -63624,5 +63624,44 @@
1271 1288 1271 1288 1271 1280 c 0,0,1
EndSplineSet
EndChar
+
+StartChar: uni2016
+Encoding: 8214 8214 1462
+Width: 1408
+VWidth: 3930
+Flags: W
+VStem: 324.48 188.739<-502.563 1702.56> 912.78 188.739<-500.697 1716.06>
+LayerCount: 2
+Fore
+SplineSet
+324.48046875 1636.74023438 m 2,0,1
+ 324.48046875 1676.40625 324.48046875 1676.40625 352.905273438 1703.41015625 c 0,2,3
+ 380.89453125 1730 380.89453125 1730 419.959960938 1730 c 0,4,5
+ 438.3125 1730 438.3125 1730 454.934570312 1722.7734375 c 128,-1,6
+ 471.557617188 1715.546875 471.557617188 1715.546875 485.162109375 1701.94238281 c 128,-1,7
+ 498.767578125 1688.3359375 498.767578125 1688.3359375 505.994140625 1671.71582031 c 128,-1,8
+ 513.219726562 1655.09667969 513.219726562 1655.09667969 513.219726562 1636.74023438 c 2,9,-1
+ 513.219726562 -436.740234375 l 2,10,11
+ 513.219726562 -473.883789062 513.219726562 -473.883789062 485.162109375 -501.94140625 c 128,-1,12
+ 457.104492188 -530 457.104492188 -530 419.959960938 -530 c 0,13,14
+ 380.89453125 -530 380.89453125 -530 352.904296875 -503.41015625 c 0,15,16
+ 324.48046875 -476.40625 324.48046875 -476.40625 324.48046875 -436.740234375 c 2,17,-1
+ 324.48046875 1636.74023438 l 2,0,1
+1101.51953125 -436.740234375 m 2,18,19
+ 1101.51953125 -473.584960938 1101.51953125 -473.584960938 1074.9296875 -501.57421875 c 0,20,21
+ 1047.92578125 -530 1047.92578125 -530 1008.25976562 -530 c 0,22,23
+ 969.194335938 -530 969.194335938 -530 941.206054688 -503.41015625 c 0,24,25
+ 912.780273438 -476.40625 912.780273438 -476.40625 912.780273438 -436.740234375 c 2,26,-1
+ 912.780273438 1636.74023438 l 2,27,28
+ 912.780273438 1656.08203125 912.780273438 1656.08203125 920.038085938 1673.13964844 c 128,-1,29
+ 927.295898438 1690.19628906 927.295898438 1690.19628906 941.205078125 1703.41015625 c 0,30,31
+ 969.194335938 1730 969.194335938 1730 1008.25976562 1730 c 0,32,33
+ 1027.6015625 1730 1027.6015625 1730 1044.65917969 1722.7421875 c 128,-1,34
+ 1061.71582031 1715.484375 1061.71582031 1715.484375 1074.9296875 1701.57421875 c 0,35,36
+ 1087.87402344 1687.94921875 1087.87402344 1687.94921875 1094.69628906 1671.43066406 c 128,-1,37
+ 1101.51953125 1654.91113281 1101.51953125 1654.91113281 1101.51953125 1636.74023438 c 2,38,-1
+ 1101.51953125 -436.740234375 l 2,18,19
+EndSplineSet
+EndChar
EndChars
EndSplineFont
--- a/Admin/isabelle_fonts/IsabelleSymbolsBold.sfd Mon Sep 20 14:24:11 2021 +0200
+++ b/Admin/isabelle_fonts/IsabelleSymbolsBold.sfd Thu Oct 07 10:20:10 2021 +0200
@@ -21,7 +21,7 @@
OS2_WeightWidthSlopeOnly: 0
OS2_UseTypoMetrics: 1
CreationTime: 1050374980
-ModificationTime: 1616429477
+ModificationTime: 1633346753
PfmFamily: 17
TTFWeight: 700
TTFWidth: 5
@@ -1679,10 +1679,10 @@
DisplaySize: -96
AntiAlias: 1
FitToEm: 1
-WinInfo: 10978 11 8
+WinInfo: 8195 11 8
BeginPrivate: 0
EndPrivate
-BeginChars: 1114115 1450
+BeginChars: 1114115 1451
StartChar: .notdef
Encoding: 1114112 -1 0
@@ -71737,5 +71737,63 @@
1131.20656165 1403 1131.20656165 1403 1167.81653987 1380.08960467 c 1,0,1
EndSplineSet
EndChar
+
+StartChar: uni2016
+Encoding: 8214 8214 1450
+Width: 1408
+VWidth: 3930
+Flags: W
+LayerCount: 2
+Fore
+SplineSet
+273.48046875 1636.74023438 m 2
+ 274.305963608 1698.42980182 274.305963608 1698.42980182 317.779016975 1740.38509515 c 0
+ 331.5651659 1753.48196068 331.5651659 1753.48196068 348.024849563 1762.58337143 c 0
+ 364.484533226 1771.68478217 364.484533226 1771.68478217 382.684388387 1776.34239109 c 0
+ 400.884243548 1781 400.884243548 1781 419.959960938 1781 c 0
+ 434.214451746 1781 434.214451746 1781 448.226135404 1778.10483503 c 0
+ 462.237819061 1775.20967007 462.237819061 1775.20967007 475.267592525 1769.544884 c 0
+ 500.772123393 1758.45726043 500.772123393 1758.45726043 521.225849377 1738.00353445 c 0
+ 527.877534153 1731.35137223 527.877534153 1731.35137223 533.617741307 1724.04056682 c 0
+ 539.357948462 1716.7297614 539.357948462 1716.7297614 544.207481245 1708.65391055 c 0
+ 549.057014029 1700.5780597 549.057014029 1700.5780597 552.764844573 1692.05055051 c 0
+ 564.219726562 1665.70385748 564.219726562 1665.70385748 564.219726562 1636.74023438 c 2
+ 564.219726562 -436.740234375 l 2
+ 564.219726562 -495.008680733 564.219726562 -495.008680733 521.225182787 -538.003224508 c 0
+ 507.658300589 -551.57057891 507.658300589 -551.57057891 491.595678193 -561.145395835 c 0
+ 475.533055797 -570.720212761 475.533055797 -570.720212761 457.267144636 -575.860106381 c 0
+ 439.001233476 -581 439.001233476 -581 419.959960938 -581 c 0
+ 391.253451691 -581 391.253451691 -581 364.896337999 -570.553783949 c 0
+ 338.539224308 -560.107567898 338.539224308 -560.107567898 317.777206298 -540.384302725 c 0
+ 296.387100388 -520.062746736 296.387100388 -520.062746736 284.933784569 -493.217738834 c 0
+ 273.48046875 -466.372730933 273.48046875 -466.372730933 273.48046875 -436.740234375 c 2
+ 273.48046875 1636.74023438 l 2
+1152.51953125 -436.740234375 m 2
+ 1151.74952957 -494.144209416 1151.74952957 -494.144209416 1111.90503919 -536.700040691 c 0
+ 1091.58360184 -558.091491525 1091.58360184 -558.091491525 1064.73824301 -569.545745762 c 0
+ 1037.89288418 -581 1037.89288418 -581 1008.25976562 -581 c 0
+ 979.553949558 -581 979.553949558 -581 953.196369328 -570.553430392 c 0
+ 926.838789099 -560.106860784 926.838789099 -560.106860784 906.080232746 -540.385507945 c 0
+ 861.780273438 -498.301459752 861.780273438 -498.301459752 861.780273438 -436.740234375 c 2
+ 861.780273438 1636.74023438 l 2
+ 861.780273438 1651.32239562 861.780273438 1651.32239562 864.624564811 1665.58641717 c 0
+ 867.468856184 1679.85043872 867.468856184 1679.85043872 873.10986998 1693.10818737 c 0
+ 878.772167602 1706.41519628 878.772167602 1706.41519628 887.133373164 1718.37257459 c 0
+ 895.494578727 1730.3299529 895.494578727 1730.3299529 906.078821663 1740.38509515 c 0
+ 948.831274571 1781 948.831274571 1781 1008.25976562 1781 c 0
+ 1038.00042276 1781 1038.00042276 1781 1064.62771862 1769.67040346 c 0
+ 1073.50484059 1765.89307777 1073.50484059 1765.89307777 1081.84644385 1760.86774412 c 0
+ 1090.18804712 1755.84241046 1090.18804712 1755.84241046 1097.70707391 1749.78666415 c 0
+ 1105.2261007 1743.73091784 1105.2261007 1743.73091784 1111.90386462 1736.70127707 c 0
+ 1116.65951952 1731.69555114 1116.65951952 1731.69555114 1120.93180299 1726.3118946 c 0
+ 1125.20408645 1720.92823807 1125.20408645 1720.92823807 1128.97353615 1715.18962916 c 0
+ 1132.74298584 1709.45102026 1132.74298584 1709.45102026 1135.97975475 1703.34407818 c 0
+ 1139.21652366 1697.2371361 1139.21652366 1697.2371361 1141.83366456 1690.90032844 c 0
+ 1145.36294721 1682.35569623 1145.36294721 1682.35569623 1147.74798058 1673.36655214 c 0
+ 1150.13301394 1664.37740804 1150.13301394 1664.37740804 1151.3262726 1655.19274645 c 0
+ 1152.51953125 1646.00808487 1152.51953125 1646.00808487 1152.51953125 1636.74023438 c 2
+ 1152.51953125 -436.740234375 l 2
+EndSplineSet
+EndChar
EndChars
EndSplineFont
--- a/CONTRIBUTORS Mon Sep 20 14:24:11 2021 +0200
+++ b/CONTRIBUTORS Thu Oct 07 10:20:10 2021 +0200
@@ -6,6 +6,9 @@
Contributions to Isabelle2021-1
-------------------------------
+* July .. September 2021: Makarius Wenzel
+ Significantly improved Isabelle/Haskell library.
+
* July 2021: Florian Haftmann
Further consolidation of bit operations and word types.
--- a/NEWS Mon Sep 20 14:24:11 2021 +0200
+++ b/NEWS Thu Oct 07 10:20:10 2021 +0200
@@ -4,8 +4,8 @@
(Note: Isabelle/jEdit shows a tree-view of the NEWS file in Sidekick.)
-New in Isabelle2021 (December 2021)
------------------------------------
+New in Isabelle2021-1 (December 2021)
+-------------------------------------
*** General ***
@@ -30,6 +30,13 @@
See also the group "Z Notation" in the Symbols dockable of
Isabelle/jEdit.
+* The Isabelle/Haskell library ($ISABELLE_HOME/src/Tools/Haskell) has
+been significantly improved. In particular, module Isabelle.Bytes
+provides type Bytes for light-weight byte strings (with optional UTF8
+interpretation), similar to type string in Isabelle/ML. Isabelle symbols
+now work uniformly in Isabelle/Haskell vs. Isabelle/ML vs.
+Isabelle/Scala/PIDE.
+
*** Isar ***
@@ -59,8 +66,8 @@
*** Document preparation ***
-* More predefined symbols: \<interleave> \<sslash> (package "stmaryrd"), \<checkmark> \<crossmark> (LaTeX package
-"pifont").
+* More predefined symbols: \<Parallel> \<interleave> \<sslash> (package "stmaryrd"), \<checkmark> \<crossmark> (LaTeX
+package "pifont").
* High-quality blackboard-bold symbols from font "txmia" (LaTeX package
"pxfonts"): \<bbbA>\<bool>\<complex>\<bbbD>\<bbbE>\<bbbF>\<bbbG>\<bbbH>\<bbbI>\<bbbJ>\<bbbK>\<bbbL>\<bbbM>\<nat>\<bbbO>\<bbbP>\<rat>\<real>\<bbbS>\<bbbT>\<bbbU>\<bbbV>\<bbbW>\<bbbX>\<bbbY>\<int>.
@@ -183,13 +190,20 @@
INCOMPATIBILITY.
* Sledgehammer:
- - Removed legacy "lam_lifting" (synonym for "lifting") from option
- "lam_trans". Minor INCOMPATIBILITY.
- - Renamed "hide_lams" to "opaque_lifting" in option "lam_trans". Minor
- INCOMPATIBILITY.
- - Added "opaque_combs" to option "lam_trans": lambda expressions are
- rewritten using combinators, but the combinators are kept opaque,
- i.e. without definitions.
+ - Update of bundled provers:
+ E 2.6
+ Vampire 4.6 (with Open Source license)
+ veriT 2021.06-rmx
+ Zipperposition 2.1
+ - Adjusted default provers:
+ cvc4 vampire verit e spass z3 zipperposition
+ - Removed legacy "lam_lifting" (synonym for "lifting") from option
+ "lam_trans". Minor INCOMPATIBILITY.
+ - Renamed "hide_lams" to "opaque_lifting" in option "lam_trans". Minor
+ INCOMPATIBILITY.
+ - Added "opaque_combs" to option "lam_trans": lambda expressions are
+ rewritten using combinators, but the combinators are kept opaque,
+ i.e. without definitions.
* Metis: Renamed option "hide_lams" to "opaque_lifting". Minor
INCOMPATIBILITY.
@@ -329,8 +343,11 @@
The main Isabelle/ML interface is Isabelle_System.bash_process with
result type Process_Result.T (resembling class Process_Result in Scala);
derived operations Isabelle_System.bash and Isabelle_System.bash_output
-provide similar functionality as before. Rare INCOMPATIBILITY due to
-subtle semantic differences:
+provide similar functionality as before. The underlying TCP/IP server
+within Isabelle/Scala is available to other programming languages as
+well, notably Isabelle/Haskell.
+
+Rare INCOMPATIBILITY due to subtle semantic differences:
- Processes invoked from Isabelle/ML actually run in the context of
the Java VM of Isabelle/Scala. The settings environment and current
@@ -352,20 +369,19 @@
like Isabelle_System.with_tmp_file to create a file name and
File.read to retrieve its content.
- - Just like any other Scala function invoked from ML,
- Isabelle_System.bash_process requires a proper PIDE session context.
- This could be a regular batch session (e.g. "isabelle build"), a
- PIDE editor session (e.g. "isabelle jedit"), or headless PIDE (e.g.
- "isabelle dump" or "isabelle server"). Note that old "isabelle
- console" or raw "isabelle process" don't have that.
+ - The Isabelle/Scala "bash_process" server requires a PIDE session
+ context. This could be a regular batch session (e.g. "isabelle
+ build"), a PIDE editor session (e.g. "isabelle jedit"), or headless
+ PIDE (e.g. "isabelle dump" or "isabelle server"). Note that old
+ "isabelle console" or raw "isabelle process" don't have that.
New Process_Result.timing works as in Isabelle/Scala, based on direct
measurements of the bash_process wrapper in C: elapsed time is always
available, CPU time is only available on Linux and macOS, GC time is
unavailable.
-* Likewise, the following Isabelle/ML system operations are run in the
-context of Isabelle/Scala:
+* The following Isabelle/ML system operations are run in the context of
+Isabelle/Scala, within a PIDE session context:
- Isabelle_System.make_directory
- Isabelle_System.copy_dir
@@ -388,6 +404,8 @@
*** System ***
+* Update to OpenJDK 17: the current long-term support version of Java.
+
* Each Isabelle component may specify a Scala/Java jar module
declaratively via etc/build.props (file names are relative to the
component directory). E.g. see $ISABELLE_HOME/etc/build.props with
--- a/etc/symbols Mon Sep 20 14:24:11 2021 +0200
+++ b/etc/symbols Thu Oct 07 10:20:10 2021 +0200
@@ -301,6 +301,7 @@
\<preceq> code: 0x00227c group: relation
\<succeq> code: 0x00227d group: relation
\<parallel> code: 0x002225 group: relation abbrev: ||
+\<Parallel> code: 0x002016 group: relation abbrev: ||
\<interleave> code: 0x002af4 group: relation abbrev: ||
\<sslash> code: 0x002afd group: relation abbrev: ||
\<bar> code: 0x0000a6 group: punctuation abbrev: ||
--- a/lib/texinputs/isabellesym.sty Mon Sep 20 14:24:11 2021 +0200
+++ b/lib/texinputs/isabellesym.sty Thu Oct 07 10:20:10 2021 +0200
@@ -303,6 +303,7 @@
\newcommand{\isasympreceq}{\isamath{\preceq}}
\newcommand{\isasymsucceq}{\isamath{\succeq}}
\newcommand{\isasymparallel}{\isamath{\parallel}}
+\newcommand{\isasymParallel}{\isamath{\bigparallel}} %requires stmaryrd
\newcommand{\isasyminterleace}{\isamath{\interleave}} %requires stmaryrd
\newcommand{\isasymsslash}{\isamath{\sslash}} %requires stmaryrd
\newcommand{\isasymbar}{\isamath{\mid}}
--- a/src/CCL/CCL.thy Mon Sep 20 14:24:11 2021 +0200
+++ b/src/CCL/CCL.thy Thu Oct 07 10:20:10 2021 +0200
@@ -232,15 +232,15 @@
ML \<open>
local
- fun pairs_of f x [] = []
+ fun pairs_of _ _ [] = []
| pairs_of f x (y::ys) = (f x y) :: (f y x) :: (pairs_of f x ys)
- fun mk_combs ff [] = []
+ fun mk_combs _ [] = []
| mk_combs ff (x::xs) = (pairs_of ff x xs) @ mk_combs ff xs
(* Doesn't handle binder types correctly *)
fun saturate thy sy name =
- let fun arg_str 0 a s = s
+ let fun arg_str 0 _ s = s
| arg_str 1 a s = "(" ^ a ^ "a" ^ s ^ ")"
| arg_str n a s = arg_str (n-1) a ("," ^ a ^ (chr((ord "a")+n-1)) ^ s)
val T = Sign.the_const_type thy (Sign.intern_const thy sy);
--- a/src/CCL/Term.thy Mon Sep 20 14:24:11 2021 +0200
+++ b/src/CCL/Term.thy Thu Oct 07 10:20:10 2021 +0200
@@ -45,15 +45,11 @@
definition ncase :: "[i,i,i\<Rightarrow>i]\<Rightarrow>i"
where "ncase(n,b,c) == when(n, \<lambda>x. b, \<lambda>y. c(y))"
-
-no_syntax
- "_Let" :: "[letbinds, 'a] => 'a" ("(let (_)/ in (_))" 10)
+definition "let1" :: "[i,i\<Rightarrow>i]\<Rightarrow>i"
+ where let_def: "let1(t, f) == case(t,f(true),f(false), \<lambda>x y. f(<x,y>), \<lambda>u. f(lam x. u(x)))"
-definition "let" :: "[i,i\<Rightarrow>i]\<Rightarrow>i"
- where "let(t, f) == case(t,f(true),f(false), \<lambda>x y. f(<x,y>), \<lambda>u. f(lam x. u(x)))"
-
-syntax
- "_Let" :: "[letbinds, 'a] => 'a" ("(let (_)/ in (_))" 10)
+syntax "_let1" :: "[idt,i,i]\<Rightarrow>i" ("(3let _ be _/ in _)" [0,0,60] 60)
+translations "let x be a in e" == "CONST let1(a, \<lambda>x. e)"
definition letrec :: "[[i,i\<Rightarrow>i]\<Rightarrow>i,(i\<Rightarrow>i)\<Rightarrow>i]\<Rightarrow>i"
where "letrec(h, b) == b(\<lambda>x. fix(\<lambda>f. lam x. h(x,\<lambda>y. f`y))`x)"
@@ -68,67 +64,65 @@
\<lambda>g'. f(\<lambda>x y z. g'(<x,<y,z>>)))"
syntax
- "_let" :: "[id,i,i]\<Rightarrow>i" ("(3let _ be _/ in _)" [0,0,60] 60)
- "_letrec" :: "[id,id,i,i]\<Rightarrow>i" ("(3letrec _ _ be _/ in _)" [0,0,0,60] 60)
- "_letrec2" :: "[id,id,id,i,i]\<Rightarrow>i" ("(3letrec _ _ _ be _/ in _)" [0,0,0,0,60] 60)
- "_letrec3" :: "[id,id,id,id,i,i]\<Rightarrow>i" ("(3letrec _ _ _ _ be _/ in _)" [0,0,0,0,0,60] 60)
-
-ML \<open>
-(** Quantifier translations: variable binding **)
-
-(* FIXME does not handle "_idtdummy" *)
-(* FIXME should use Syntax_Trans.mark_bound, Syntax_Trans.variant_abs' *)
-
-fun let_tr [Free x, a, b] = Const(\<^const_syntax>\<open>let\<close>,dummyT) $ a $ absfree x b;
-fun let_tr' [a,Abs(id,T,b)] =
- let val (id',b') = Syntax_Trans.variant_abs(id,T,b)
- in Const(\<^syntax_const>\<open>_let\<close>,dummyT) $ Free(id',T) $ a $ b' end;
-
-fun letrec_tr [Free f, Free x, a, b] =
- Const(\<^const_syntax>\<open>letrec\<close>, dummyT) $ absfree x (absfree f a) $ absfree f b;
-fun letrec2_tr [Free f, Free x, Free y, a, b] =
- Const(\<^const_syntax>\<open>letrec2\<close>, dummyT) $ absfree x (absfree y (absfree f a)) $ absfree f b;
-fun letrec3_tr [Free f, Free x, Free y, Free z, a, b] =
- Const(\<^const_syntax>\<open>letrec3\<close>, dummyT) $
- absfree x (absfree y (absfree z (absfree f a))) $ absfree f b;
+ "_letrec" :: "[idt,idt,i,i]\<Rightarrow>i" ("(3letrec _ _ be _/ in _)" [0,0,0,60] 60)
+ "_letrec2" :: "[idt,idt,idt,i,i]\<Rightarrow>i" ("(3letrec _ _ _ be _/ in _)" [0,0,0,0,60] 60)
+ "_letrec3" :: "[idt,idt,idt,idt,i,i]\<Rightarrow>i" ("(3letrec _ _ _ _ be _/ in _)" [0,0,0,0,0,60] 60)
+parse_translation \<open>
+ let
+ fun abs_tr t u = Syntax_Trans.abs_tr [t, u];
+ fun letrec_tr [f, x, a, b] =
+ Syntax.const \<^const_syntax>\<open>letrec\<close> $ abs_tr x (abs_tr f a) $ abs_tr f b;
+ fun letrec2_tr [f, x, y, a, b] =
+ Syntax.const \<^const_syntax>\<open>letrec2\<close> $ abs_tr x (abs_tr y (abs_tr f a)) $ abs_tr f b;
+ fun letrec3_tr [f, x, y, z, a, b] =
+ Syntax.const \<^const_syntax>\<open>letrec3\<close> $ abs_tr x (abs_tr y (abs_tr z (abs_tr f a))) $ abs_tr f b;
+ in
+ [(\<^syntax_const>\<open>_letrec\<close>, K letrec_tr),
+ (\<^syntax_const>\<open>_letrec2\<close>, K letrec2_tr),
+ (\<^syntax_const>\<open>_letrec3\<close>, K letrec3_tr)]
+ end
+\<close>
+print_translation \<open>
+ let
+ val bound = Syntax_Trans.mark_bound_abs;
-fun letrec_tr' [Abs(x,T,Abs(f,S,a)),Abs(ff,SS,b)] =
- let val (f',b') = Syntax_Trans.variant_abs(ff,SS,b)
- val (_,a'') = Syntax_Trans.variant_abs(f,S,a)
- val (x',a') = Syntax_Trans.variant_abs(x,T,a'')
- in Const(\<^syntax_const>\<open>_letrec\<close>,dummyT) $ Free(f',SS) $ Free(x',T) $ a' $ b' end;
-fun letrec2_tr' [Abs(x,T,Abs(y,U,Abs(f,S,a))),Abs(ff,SS,b)] =
- let val (f',b') = Syntax_Trans.variant_abs(ff,SS,b)
- val ( _,a1) = Syntax_Trans.variant_abs(f,S,a)
- val (y',a2) = Syntax_Trans.variant_abs(y,U,a1)
- val (x',a') = Syntax_Trans.variant_abs(x,T,a2)
- in Const(\<^syntax_const>\<open>_letrec2\<close>,dummyT) $ Free(f',SS) $ Free(x',T) $ Free(y',U) $ a' $ b'
+ fun letrec_tr' [Abs(x,T,Abs(f,S,a)),Abs(ff,SS,b)] =
+ let
+ val (f',b') = Syntax_Trans.print_abs(ff,SS,b)
+ val (_,a'') = Syntax_Trans.print_abs(f,S,a)
+ val (x',a') = Syntax_Trans.print_abs(x,T,a'')
+ in
+ Syntax.const \<^syntax_const>\<open>_letrec\<close> $ bound(f',SS) $ bound(x',T) $ a' $ b'
+ end;
+
+ fun letrec2_tr' [Abs(x,T,Abs(y,U,Abs(f,S,a))),Abs(ff,SS,b)] =
+ let
+ val (f',b') = Syntax_Trans.print_abs(ff,SS,b)
+ val ( _,a1) = Syntax_Trans.print_abs(f,S,a)
+ val (y',a2) = Syntax_Trans.print_abs(y,U,a1)
+ val (x',a') = Syntax_Trans.print_abs(x,T,a2)
+ in
+ Syntax.const \<^syntax_const>\<open>_letrec2\<close> $ bound(f',SS) $ bound(x',T) $ bound(y',U) $ a' $ b'
end;
-fun letrec3_tr' [Abs(x,T,Abs(y,U,Abs(z,V,Abs(f,S,a)))),Abs(ff,SS,b)] =
- let val (f',b') = Syntax_Trans.variant_abs(ff,SS,b)
- val ( _,a1) = Syntax_Trans.variant_abs(f,S,a)
- val (z',a2) = Syntax_Trans.variant_abs(z,V,a1)
- val (y',a3) = Syntax_Trans.variant_abs(y,U,a2)
- val (x',a') = Syntax_Trans.variant_abs(x,T,a3)
- in Const(\<^syntax_const>\<open>_letrec3\<close>,dummyT) $ Free(f',SS) $ Free(x',T) $ Free(y',U) $ Free(z',V) $ a' $ b'
+
+ fun letrec3_tr' [Abs(x,T,Abs(y,U,Abs(z,V,Abs(f,S,a)))),Abs(ff,SS,b)] =
+ let
+ val (f',b') = Syntax_Trans.print_abs(ff,SS,b)
+ val ( _,a1) = Syntax_Trans.print_abs(f,S,a)
+ val (z',a2) = Syntax_Trans.print_abs(z,V,a1)
+ val (y',a3) = Syntax_Trans.print_abs(y,U,a2)
+ val (x',a') = Syntax_Trans.print_abs(x,T,a3)
+ in
+ Syntax.const \<^syntax_const>\<open>_letrec3\<close> $
+ bound(f',SS) $ bound(x',T) $ bound(y',U) $ bound(z',V) $ a' $ b'
end;
+ in
+ [(\<^const_syntax>\<open>letrec\<close>, K letrec_tr'),
+ (\<^const_syntax>\<open>letrec2\<close>, K letrec2_tr'),
+ (\<^const_syntax>\<open>letrec3\<close>, K letrec3_tr')]
+ end
\<close>
-parse_translation \<open>
- [(\<^syntax_const>\<open>_let\<close>, K let_tr),
- (\<^syntax_const>\<open>_letrec\<close>, K letrec_tr),
- (\<^syntax_const>\<open>_letrec2\<close>, K letrec2_tr),
- (\<^syntax_const>\<open>_letrec3\<close>, K letrec3_tr)]
-\<close>
-
-print_translation \<open>
- [(\<^const_syntax>\<open>let\<close>, K let_tr'),
- (\<^const_syntax>\<open>letrec\<close>, K letrec_tr'),
- (\<^const_syntax>\<open>letrec2\<close>, K letrec2_tr'),
- (\<^const_syntax>\<open>letrec3\<close>, K letrec3_tr')]
-\<close>
-
-
definition nrec :: "[i,i,[i,i]\<Rightarrow>i]\<Rightarrow>i"
where "nrec(n,b,c) == letrec g x be ncase(x, b, \<lambda>y. c(y,g(y))) in g(n)"
@@ -165,38 +159,31 @@
apply (unfold let_def)
apply (erule rev_mp)
apply (rule_tac t = "t" in term_case)
- apply (simp_all add: caseBtrue caseBfalse caseBpair caseBlam)
+ apply simp_all
done
lemma letBabot: "let x be bot in f(x) = bot"
- apply (unfold let_def)
- apply (rule caseBbot)
- done
+ unfolding let_def by (rule caseBbot)
lemma letBbbot: "let x be t in bot = bot"
apply (unfold let_def)
apply (rule_tac t = t in term_case)
apply (rule caseBbot)
- apply (simp_all add: caseBtrue caseBfalse caseBpair caseBlam)
+ apply simp_all
done
lemma applyB: "(lam x. b(x)) ` a = b(a)"
- apply (unfold apply_def)
- apply (simp add: caseBtrue caseBfalse caseBpair caseBlam)
- done
+ by (simp add: apply_def)
lemma applyBbot: "bot ` a = bot"
- apply (unfold apply_def)
- apply (rule caseBbot)
- done
+ unfolding apply_def by (rule caseBbot)
lemma fixB: "fix(f) = f(fix(f))"
apply (unfold fix_def)
apply (rule applyB [THEN ssubst], rule refl)
done
-lemma letrecB:
- "letrec g x be h(x,g) in g(a) = h(a,\<lambda>y. letrec g x be h(x,g) in g(y))"
+lemma letrecB: "letrec g x be h(x,g) in g(a) = h(a,\<lambda>y. letrec g x be h(x,g) in g(y))"
apply (unfold letrec_def)
apply (rule fixB [THEN ssubst], rule applyB [THEN ssubst], rule refl)
done
@@ -205,8 +192,10 @@
method_setup beta_rl = \<open>
Scan.succeed (fn ctxt =>
- SIMPLE_METHOD' (CHANGED o
- simp_tac (ctxt addsimps @{thms rawBs} setloop (fn _ => stac ctxt @{thm letrecB}))))
+ let val ctxt' = Context_Position.set_visible false ctxt in
+ SIMPLE_METHOD' (CHANGED o
+ simp_tac (ctxt' addsimps @{thms rawBs} setloop (fn _ => stac ctxt @{thm letrecB})))
+ end)
\<close>
lemma ifBtrue: "if true then t else u = t"
--- a/src/CCL/Trancl.thy Mon Sep 20 14:24:11 2021 +0200
+++ b/src/CCL/Trancl.thy Thu Oct 07 10:20:10 2021 +0200
@@ -66,7 +66,6 @@
lemmas [intro] = compI idI
and [elim] = compE idE
- and [elim!] = pair_inject
lemma comp_mono: "\<lbrakk>r'<=r; s'<=s\<rbrakk> \<Longrightarrow> (r' O s') <= (r O s)"
by blast
@@ -202,8 +201,6 @@
done
lemma trancl_into_trancl2: "\<lbrakk><a,b> : r; <b,c> : r^+\<rbrakk> \<Longrightarrow> <a,c> : r^+"
- apply (rule r_into_trancl [THEN trans_trancl [THEN transD]])
- apply assumption+
- done
+ by (rule r_into_trancl [THEN trans_trancl [THEN transD]])
end
--- a/src/Doc/Isar_Ref/Symbols.thy Mon Sep 20 14:24:11 2021 +0200
+++ b/src/Doc/Isar_Ref/Symbols.thy Thu Oct 07 10:20:10 2021 +0200
@@ -37,4 +37,6 @@
\end{center}
\<close>
+external_file %invisible \<open>~~/lib/texinputs/isabellesym.sty\<close>
+
end
--- a/src/Doc/Isar_Ref/document/root.tex Mon Sep 20 14:24:11 2021 +0200
+++ b/src/Doc/Isar_Ref/document/root.tex Thu Oct 07 10:20:10 2021 +0200
@@ -7,7 +7,7 @@
\usepackage{eurosym}
\usepackage{pifont}
\usepackage[english]{babel}
-\usepackage[only,bigsqcap,fatsemi,interleave,sslash]{stmaryrd}
+\usepackage[only,bigsqcap,fatsemi,bigparallel,interleave,sslash]{stmaryrd}
\usepackage{graphicx}
\let\intorig=\int %iman.sty redefines \int
\usepackage{iman,extra,isar,proof}
--- a/src/HOL/Analysis/Ball_Volume.thy Mon Sep 20 14:24:11 2021 +0200
+++ b/src/HOL/Analysis/Ball_Volume.thy Thu Oct 07 10:20:10 2021 +0200
@@ -1,4 +1,4 @@
-(*
+(*
File: HOL/Analysis/Ball_Volume.thy
Author: Manuel Eberl, TU München
*)
@@ -25,11 +25,11 @@
text \<open>
We first need the value of the following integral, which is at the core of
- computing the measure of an \<open>n + 1\<close>-dimensional ball in terms of the measure of an
+ computing the measure of an \<open>n + 1\<close>-dimensional ball in terms of the measure of an
\<open>n\<close>-dimensional one.
\<close>
lemma emeasure_cball_aux_integral:
- "(\<integral>\<^sup>+x. indicator {-1..1} x * sqrt (1 - x\<^sup>2) ^ n \<partial>lborel) =
+ "(\<integral>\<^sup>+x. indicator {-1..1} x * sqrt (1 - x\<^sup>2) ^ n \<partial>lborel) =
ennreal (Beta (1 / 2) (real n / 2 + 1))"
proof -
have "((\<lambda>t. t powr (-1 / 2) * (1 - t) powr (real n / 2)) has_integral
@@ -37,7 +37,7 @@
using has_integral_Beta_real[of "1/2" "n / 2 + 1"] by simp
from nn_integral_has_integral_lebesgue[OF _ this] have
"ennreal (Beta (1 / 2) (real n / 2 + 1)) =
- nn_integral lborel (\<lambda>t. ennreal (t powr (-1 / 2) * (1 - t) powr (real n / 2) *
+ nn_integral lborel (\<lambda>t. ennreal (t powr (-1 / 2) * (1 - t) powr (real n / 2) *
indicator {0^2..1^2} t))"
by (simp add: mult_ac ennreal_mult' ennreal_indicator)
also have "\<dots> = (\<integral>\<^sup>+ x. ennreal (x\<^sup>2 powr - (1 / 2) * (1 - x\<^sup>2) powr (real n / 2) * (2 * x) *
@@ -45,7 +45,7 @@
by (subst nn_integral_substitution[where g = "\<lambda>x. x ^ 2" and g' = "\<lambda>x. 2 * x"])
(auto intro!: derivative_eq_intros continuous_intros simp: set_borel_measurable_def)
also have "\<dots> = (\<integral>\<^sup>+ x. 2 * ennreal ((1 - x\<^sup>2) powr (real n / 2) * indicator {0..1} x) \<partial>lborel)"
- by (intro nn_integral_cong_AE AE_I[of _ _ "{0}"])
+ by (intro nn_integral_cong_AE AE_I[of _ _ "{0}"])
(auto simp: indicator_def powr_minus powr_half_sqrt field_split_simps ennreal_mult')
also have "\<dots> = (\<integral>\<^sup>+ x. ennreal ((1 - x\<^sup>2) powr (real n / 2) * indicator {0..1} x) \<partial>lborel) +
(\<integral>\<^sup>+ x. ennreal ((1 - x\<^sup>2) powr (real n / 2) * indicator {0..1} x) \<partial>lborel)"
@@ -54,7 +54,7 @@
by (subst nn_integral_real_affine[of _ "-1" 0])
(auto simp: indicator_def intro!: nn_integral_cong)
hence "?I + ?I = \<dots> + ?I" by simp
- also have "\<dots> = (\<integral>\<^sup>+ x. ennreal ((1 - x\<^sup>2) powr (real n / 2) *
+ also have "\<dots> = (\<integral>\<^sup>+ x. ennreal ((1 - x\<^sup>2) powr (real n / 2) *
(indicator {-1..0} x + indicator{0..1} x)) \<partial>lborel)"
by (subst nn_integral_add [symmetric]) (auto simp: algebra_simps)
also have "\<dots> = (\<integral>\<^sup>+ x. ennreal ((1 - x\<^sup>2) powr (real n / 2) * indicator {-1..1} x) \<partial>lborel)"
@@ -69,13 +69,10 @@
lemma real_sqrt_le_iff': "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> sqrt x \<le> y \<longleftrightarrow> x \<le> y ^ 2"
using real_le_lsqrt sqrt_le_D by blast
-lemma power2_le_iff_abs_le: "y \<ge> 0 \<Longrightarrow> (x::real) ^ 2 \<le> y ^ 2 \<longleftrightarrow> abs x \<le> y"
- by (subst real_sqrt_le_iff' [symmetric]) auto
-
text \<open>
- Isabelle's type system makes it very difficult to do an induction over the dimension
- of a Euclidean space type, because the type would change in the inductive step. To avoid
- this problem, we instead formulate the problem in a more concrete way by unfolding the
+ Isabelle's type system makes it very difficult to do an induction over the dimension
+ of a Euclidean space type, because the type would change in the inductive step. To avoid
+ this problem, we instead formulate the problem in a more concrete way by unfolding the
definition of the Euclidean norm.
\<close>
lemma emeasure_cball_aux:
@@ -92,17 +89,17 @@
case (insert i A r)
interpret product_sigma_finite "\<lambda>_. lborel"
by standard
- have "emeasure (Pi\<^sub>M (insert i A) (\<lambda>_. lborel))
+ have "emeasure (Pi\<^sub>M (insert i A) (\<lambda>_. lborel))
({f. sqrt (\<Sum>i\<in>insert i A. (f i)\<^sup>2) \<le> r} \<inter> space (Pi\<^sub>M (insert i A) (\<lambda>_. lborel))) =
nn_integral (Pi\<^sub>M (insert i A) (\<lambda>_. lborel))
(indicator ({f. sqrt (\<Sum>i\<in>insert i A. (f i)\<^sup>2) \<le> r} \<inter>
space (Pi\<^sub>M (insert i A) (\<lambda>_. lborel))))"
by (subst nn_integral_indicator) auto
- also have "\<dots> = (\<integral>\<^sup>+ y. \<integral>\<^sup>+ x. indicator ({f. sqrt ((f i)\<^sup>2 + (\<Sum>i\<in>A. (f i)\<^sup>2)) \<le> r} \<inter>
- space (Pi\<^sub>M (insert i A) (\<lambda>_. lborel))) (x(i := y))
+ also have "\<dots> = (\<integral>\<^sup>+ y. \<integral>\<^sup>+ x. indicator ({f. sqrt ((f i)\<^sup>2 + (\<Sum>i\<in>A. (f i)\<^sup>2)) \<le> r} \<inter>
+ space (Pi\<^sub>M (insert i A) (\<lambda>_. lborel))) (x(i := y))
\<partial>Pi\<^sub>M A (\<lambda>_. lborel) \<partial>lborel)"
using insert.prems insert.hyps by (subst product_nn_integral_insert_rev) auto
- also have "\<dots> = (\<integral>\<^sup>+ (y::real). \<integral>\<^sup>+ x. indicator {-r..r} y * indicator ({f. sqrt ((\<Sum>i\<in>A. (f i)\<^sup>2)) \<le>
+ also have "\<dots> = (\<integral>\<^sup>+ (y::real). \<integral>\<^sup>+ x. indicator {-r..r} y * indicator ({f. sqrt ((\<Sum>i\<in>A. (f i)\<^sup>2)) \<le>
sqrt (r ^ 2 - y ^ 2)} \<inter> space (Pi\<^sub>M A (\<lambda>_. lborel))) x \<partial>Pi\<^sub>M A (\<lambda>_. lborel) \<partial>lborel)"
proof (intro nn_integral_cong, goal_cases)
case (1 y f)
@@ -118,13 +115,13 @@
thus ?case using 1 \<open>r > 0\<close>
by (auto simp: sum_nonneg real_sqrt_le_iff' indicator_def PiE_def space_PiM dest!: *)
qed
- also have "\<dots> = (\<integral>\<^sup>+ (y::real). indicator {-r..r} y * (\<integral>\<^sup>+ x. indicator ({f. sqrt ((\<Sum>i\<in>A. (f i)\<^sup>2))
+ also have "\<dots> = (\<integral>\<^sup>+ (y::real). indicator {-r..r} y * (\<integral>\<^sup>+ x. indicator ({f. sqrt ((\<Sum>i\<in>A. (f i)\<^sup>2))
\<le> sqrt (r ^ 2 - y ^ 2)} \<inter> space (Pi\<^sub>M A (\<lambda>_. lborel))) x
\<partial>Pi\<^sub>M A (\<lambda>_. lborel)) \<partial>lborel)" by (subst nn_integral_cmult) auto
- also have "\<dots> = (\<integral>\<^sup>+ (y::real). indicator {-r..r} y * emeasure (PiM A (\<lambda>_. lborel))
+ also have "\<dots> = (\<integral>\<^sup>+ (y::real). indicator {-r..r} y * emeasure (PiM A (\<lambda>_. lborel))
({f. sqrt ((\<Sum>i\<in>A. (f i)\<^sup>2)) \<le> sqrt (r ^ 2 - y ^ 2)} \<inter> space (Pi\<^sub>M A (\<lambda>_. lborel))) \<partial>lborel)"
using \<open>finite A\<close> by (intro nn_integral_cong, subst nn_integral_indicator) auto
- also have "\<dots> = (\<integral>\<^sup>+ (y::real). indicator {-r..r} y * ennreal (unit_ball_vol (real (card A)) *
+ also have "\<dots> = (\<integral>\<^sup>+ (y::real). indicator {-r..r} y * ennreal (unit_ball_vol (real (card A)) *
(sqrt (r ^ 2 - y ^ 2)) ^ card A) \<partial>lborel)"
proof (intro nn_integral_cong_AE, goal_cases)
case 1
@@ -141,28 +138,28 @@
qed (insert elim, auto)
qed
qed
- also have "\<dots> = ennreal (unit_ball_vol (real (card A))) *
+ also have "\<dots> = ennreal (unit_ball_vol (real (card A))) *
(\<integral>\<^sup>+ (y::real). indicator {-r..r} y * (sqrt (r ^ 2 - y ^ 2)) ^ card A \<partial>lborel)"
by (subst nn_integral_cmult [symmetric])
(auto simp: mult_ac ennreal_mult' [symmetric] indicator_def intro!: nn_integral_cong)
also have "(\<integral>\<^sup>+ (y::real). indicator {-r..r} y * (sqrt (r ^ 2 - y ^ 2)) ^ card A \<partial>lborel) =
- (\<integral>\<^sup>+ (y::real). r ^ card A * indicator {-1..1} y * (sqrt (1 - y ^ 2)) ^ card A
+ (\<integral>\<^sup>+ (y::real). r ^ card A * indicator {-1..1} y * (sqrt (1 - y ^ 2)) ^ card A
\<partial>(distr lborel borel ((*) (1/r))))" using \<open>r > 0\<close>
by (subst nn_integral_distr)
(auto simp: indicator_def field_simps real_sqrt_divide intro!: nn_integral_cong)
- also have "\<dots> = (\<integral>\<^sup>+ x. ennreal (r ^ Suc (card A)) *
+ also have "\<dots> = (\<integral>\<^sup>+ x. ennreal (r ^ Suc (card A)) *
(indicator {- 1..1} x * sqrt (1 - x\<^sup>2) ^ card A) \<partial>lborel)" using \<open>r > 0\<close>
by (subst lborel_distr_mult) (auto simp: nn_integral_density ennreal_mult' [symmetric] mult_ac)
- also have "\<dots> = ennreal (r ^ Suc (card A)) * (\<integral>\<^sup>+ x. indicator {- 1..1} x *
+ also have "\<dots> = ennreal (r ^ Suc (card A)) * (\<integral>\<^sup>+ x. indicator {- 1..1} x *
sqrt (1 - x\<^sup>2) ^ card A \<partial>lborel)"
by (subst nn_integral_cmult) auto
also note emeasure_cball_aux_integral
also have "ennreal (unit_ball_vol (real (card A))) * (ennreal (r ^ Suc (card A)) *
- ennreal (Beta (1/2) (card A / 2 + 1))) =
+ ennreal (Beta (1/2) (card A / 2 + 1))) =
ennreal (unit_ball_vol (card A) * Beta (1/2) (card A / 2 + 1) * r ^ Suc (card A))"
using \<open>r > 0\<close> by (simp add: ennreal_mult' [symmetric] mult_ac)
also have "unit_ball_vol (card A) * Beta (1/2) (card A / 2 + 1) = unit_ball_vol (Suc (card A))"
- by (auto simp: unit_ball_vol_def Beta_def Gamma_eq_zero_iff field_simps
+ by (auto simp: unit_ball_vol_def Beta_def Gamma_eq_zero_iff field_simps
Gamma_one_half_real powr_half_sqrt [symmetric] powr_add [symmetric])
also have "Suc (card A) = card (insert i A)" using insert.hyps by simp
finally show ?case .
@@ -182,11 +179,11 @@
proof (cases "r = 0")
case False
with r have r: "r > 0" by simp
- have "(lborel :: 'a measure) =
+ have "(lborel :: 'a measure) =
distr (Pi\<^sub>M Basis (\<lambda>_. lborel)) borel (\<lambda>f. \<Sum>b\<in>Basis. f b *\<^sub>R b)"
by (rule lborel_eq)
- also have "emeasure \<dots> (cball 0 r) =
- emeasure (Pi\<^sub>M Basis (\<lambda>_. lborel))
+ also have "emeasure \<dots> (cball 0 r) =
+ emeasure (Pi\<^sub>M Basis (\<lambda>_. lborel))
({y. dist 0 (\<Sum>b\<in>Basis. y b *\<^sub>R b :: 'a) \<le> r} \<inter> space (Pi\<^sub>M Basis (\<lambda>_. lborel)))"
by (subst emeasure_distr) (auto simp: cball_def)
also have "{f. dist 0 (\<Sum>b\<in>Basis. f b *\<^sub>R b :: 'a) \<le> r} = {f. sqrt (\<Sum>i\<in>Basis. (f i)\<^sup>2) \<le> r}"
@@ -227,7 +224,7 @@
text \<open>
- Lastly, we now prove some nicer explicit formulas for the volume of the unit balls in
+ Lastly, we now prove some nicer explicit formulas for the volume of the unit balls in
the cases of even and odd integer dimensions.
\<close>
lemma unit_ball_vol_even:
@@ -240,7 +237,7 @@
"unit_ball_vol (real (2 * n + 1)) =
(2 ^ (2 * Suc n) * fact (Suc n)) / fact (2 * Suc n) * pi ^ n"
proof -
- have "unit_ball_vol (real (2 * n + 1)) =
+ have "unit_ball_vol (real (2 * n + 1)) =
pi powr (real n + 1 / 2) / Gamma (1 / 2 + real (Suc n))"
by (simp add: unit_ball_vol_def field_simps)
also have "pochhammer (1 / 2) (Suc n) = Gamma (1 / 2 + real (Suc n)) / Gamma (1 / 2)"
@@ -250,7 +247,7 @@
also have "pi powr (real n + 1 / 2) / \<dots> = pi ^ n / pochhammer (1 / 2) (Suc n)"
by (simp add: powr_add powr_half_sqrt powr_realpow)
finally show "unit_ball_vol (real (2 * n + 1)) = \<dots>" .
- also have "pochhammer (1 / 2 :: real) (Suc n) =
+ also have "pochhammer (1 / 2 :: real) (Suc n) =
fact (2 * Suc n) / (2 ^ (2 * Suc n) * fact (Suc n))"
using fact_double[of "Suc n", where ?'a = real] by (simp add: divide_simps mult_ac)
also have "pi ^n / \<dots> = (2 ^ (2 * Suc n) * fact (Suc n)) / fact (2 * Suc n) * pi ^ n"
@@ -263,7 +260,7 @@
"unit_ball_vol (numeral (Num.Bit1 n)) = 2 ^ (2 * Suc (numeral n)) * fact (Suc (numeral n)) /
fact (2 * Suc (numeral n)) * pi ^ numeral n" (is ?th2)
proof -
- have "numeral (Num.Bit0 n) = (2 * numeral n :: nat)"
+ have "numeral (Num.Bit0 n) = (2 * numeral n :: nat)"
by (simp only: numeral_Bit0 mult_2 ring_distribs)
also have "unit_ball_vol \<dots> = pi ^ numeral n / fact (numeral n)"
by (rule unit_ball_vol_even)
--- a/src/HOL/Finite_Set.thy Mon Sep 20 14:24:11 2021 +0200
+++ b/src/HOL/Finite_Set.thy Thu Oct 07 10:20:10 2021 +0200
@@ -373,6 +373,17 @@
lemma finite_vimage_iff: "bij h \<Longrightarrow> finite (h -` F) \<longleftrightarrow> finite F"
unfolding bij_def by (auto elim: finite_vimageD finite_vimageI)
+lemma finite_inverse_image_gen:
+ assumes "finite A" "inj_on f D"
+ shows "finite {j\<in>D. f j \<in> A}"
+ using finite_vimage_IntI [OF assms]
+ by (simp add: Collect_conj_eq inf_commute vimage_def)
+
+lemma finite_inverse_image:
+ assumes "finite A" "inj f"
+ shows "finite {j. f j \<in> A}"
+ using finite_inverse_image_gen [OF assms] by simp
+
lemma finite_Collect_bex [simp]:
assumes "finite A"
shows "finite {x. \<exists>y\<in>A. Q x y} \<longleftrightarrow> (\<forall>y\<in>A. finite {x. Q x y})"
--- a/src/HOL/Groups_Big.thy Mon Sep 20 14:24:11 2021 +0200
+++ b/src/HOL/Groups_Big.thy Thu Oct 07 10:20:10 2021 +0200
@@ -1560,6 +1560,20 @@
then show ?case by (force intro: mult_strict_mono' prod_nonneg)
qed
+lemma prod_le_power:
+ assumes A: "\<And>i. i \<in> A \<Longrightarrow> 0 \<le> f i \<and> f i \<le> n" "card A \<le> k" and "n \<ge> 1"
+ shows "prod f A \<le> n ^ k"
+ using A
+proof (induction A arbitrary: k rule: infinite_finite_induct)
+ case (insert i A)
+ then obtain k' where k': "card A \<le> k'" "k = Suc k'"
+ using Suc_le_D by force
+ have "f i * prod f A \<le> n * n ^ k'"
+ using insert \<open>n \<ge> 1\<close> k' by (intro prod_nonneg mult_mono; force)
+ then show ?case
+ by (auto simp: \<open>k = Suc k'\<close> insert.hyps)
+qed (use \<open>n \<ge> 1\<close> in auto)
+
end
lemma prod_mono2:
--- a/src/HOL/Library/Countable_Set.thy Mon Sep 20 14:24:11 2021 +0200
+++ b/src/HOL/Library/Countable_Set.thy Thu Oct 07 10:20:10 2021 +0200
@@ -110,6 +110,25 @@
using to_nat_on_infinite[of S, unfolded bij_betw_def]
by (auto cong: bij_betw_cong intro: bij_betw_inv_into to_nat_on_infinite)
+text \<open>
+ The sum/product over the enumeration of a finite set equals simply the sum/product over the set
+\<close>
+context comm_monoid_set
+begin
+
+lemma card_from_nat_into:
+ "F (\<lambda>i. h (from_nat_into A i)) {..<card A} = F h A"
+proof (cases "finite A")
+ case True
+ have "F (\<lambda>i. h (from_nat_into A i)) {..<card A} = F h (from_nat_into A ` {..<card A})"
+ by (metis True bij_betw_def bij_betw_from_nat_into_finite reindex_cong)
+ also have "... = F h A"
+ by (metis True bij_betw_def bij_betw_from_nat_into_finite)
+ finally show ?thesis .
+qed auto
+
+end
+
lemma countable_as_injective_image:
assumes "countable A" "infinite A"
obtains f :: "nat \<Rightarrow> 'a" where "A = range f" "inj f"
--- a/src/HOL/Library/Disjoint_Sets.thy Mon Sep 20 14:24:11 2021 +0200
+++ b/src/HOL/Library/Disjoint_Sets.thy Thu Oct 07 10:20:10 2021 +0200
@@ -167,6 +167,20 @@
by (intro disjointD[OF d]) auto
qed
+lemma disjoint_family_on_iff_disjoint_image:
+ assumes "\<And>i. i \<in> I \<Longrightarrow> A i \<noteq> {}"
+ shows "disjoint_family_on A I \<longleftrightarrow> disjoint (A ` I) \<and> inj_on A I"
+proof
+ assume "disjoint_family_on A I"
+ then show "disjoint (A ` I) \<and> inj_on A I"
+ by (metis (mono_tags, lifting) assms disjoint_family_onD disjoint_family_on_disjoint_image inf.idem inj_onI)
+qed (use disjoint_image_disjoint_family_on in metis)
+
+lemma card_UN_disjoint':
+ assumes "disjoint_family_on A I" "\<And>i. i \<in> I \<Longrightarrow> finite (A i)" "finite I"
+ shows "card (\<Union>i\<in>I. A i) = (\<Sum>i\<in>I. card (A i))"
+ using assms by (simp add: card_UN_disjoint disjoint_family_on_def)
+
lemma disjoint_UN:
assumes F: "\<And>i. i \<in> I \<Longrightarrow> disjoint (F i)" and *: "disjoint_family_on (\<lambda>i. \<Union>(F i)) I"
shows "disjoint (\<Union>i\<in>I. F i)"
@@ -217,6 +231,25 @@
using disjoint_UN[of "{C, B}" "\<lambda>x. x"] by (auto simp add: disjoint_family_on_def)
text \<open>
+ Sum/product of the union of a finite disjoint family
+\<close>
+context comm_monoid_set
+begin
+
+lemma UNION_disjoint_family:
+ assumes "finite I" and "\<forall>i\<in>I. finite (A i)"
+ and "disjoint_family_on A I"
+ shows "F g (\<Union>(A ` I)) = F (\<lambda>x. F g (A x)) I"
+ using assms unfolding disjoint_family_on_def by (rule UNION_disjoint)
+
+lemma Union_disjoint_sets:
+ assumes "\<forall>A\<in>C. finite A" and "disjoint C"
+ shows "F g (\<Union>C) = (F \<circ> F) g C"
+ using assms unfolding disjoint_def by (rule Union_disjoint)
+
+end
+
+text \<open>
The union of an infinite disjoint family of non-empty sets is infinite.
\<close>
lemma infinite_disjoint_family_imp_infinite_UNION:
@@ -353,6 +386,11 @@
lemma finite_elements: "finite A \<Longrightarrow> partition_on A P \<Longrightarrow> finite P"
using partition_onD1[of A P] by (simp add: finite_UnionD)
+lemma product_partition:
+ assumes "partition_on A P" and "\<And>p. p \<in> P \<Longrightarrow> finite p"
+ shows "card A = (\<Sum>p\<in>P. card p)"
+ using assms unfolding partition_on_def by (meson card_Union_disjoint)
+
subsection \<open>Equivalence of partitions and equivalence classes\<close>
lemma partition_on_quotient:
--- a/src/HOL/Power.thy Mon Sep 20 14:24:11 2021 +0200
+++ b/src/HOL/Power.thy Thu Oct 07 10:20:10 2021 +0200
@@ -810,6 +810,10 @@
by (auto intro!: power2_le_imp_le [OF _ abs_ge_zero])
qed
+lemma power2_le_iff_abs_le:
+ "y \<ge> 0 \<Longrightarrow> x\<^sup>2 \<le> y\<^sup>2 \<longleftrightarrow> \<bar>x\<bar> \<le> y"
+ by (metis abs_le_square_iff abs_of_nonneg)
+
lemma abs_square_le_1:"x\<^sup>2 \<le> 1 \<longleftrightarrow> \<bar>x\<bar> \<le> 1"
using abs_le_square_iff [of x 1] by simp
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Mon Sep 20 14:24:11 2021 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Thu Oct 07 10:20:10 2021 +0200
@@ -177,7 +177,7 @@
(* The first ATP of the list is used by Auto Sledgehammer. *)
fun default_provers_param_value mode ctxt =
- [cvc4N, vampireN, veritN, eN, spassN, z3N, zipperpositionN]
+ [cvc4N, vampireN, veritN, eN, spassN, z3N, zipperpositionN] \<comment> \<open>see also \<^system_option>\<open>sledgehammer_provers\<close>\<close>
|> map_filter (remotify_prover_if_not_installed ctxt)
(* In "try" mode, leave at least one thread to another slow tool (e.g. Nitpick) *)
|> take (Multithreading.max_threads () - (if mode = Try then 1 else 0))
--- a/src/Pure/Admin/build_fonts.scala Mon Sep 20 14:24:11 2021 +0200
+++ b/src/Pure/Admin/build_fonts.scala Thu Oct 07 10:20:10 2021 +0200
@@ -57,6 +57,7 @@
0x2013, // dash
0x2014, // dash
0x2015, // dash
+ 0x2016, // big parallel
0x2020, // dagger
0x2021, // double dagger
0x2022, // bullet
--- a/src/Pure/Admin/build_vampire.scala Mon Sep 20 14:24:11 2021 +0200
+++ b/src/Pure/Admin/build_vampire.scala Thu Oct 07 10:20:10 2021 +0200
@@ -1,7 +1,7 @@
/* Title: Pure/Admin/build_vampire.scala
Author: Makarius
-Build Isabelle Vampire component from repository.
+Build Isabelle Vampire component from official download.
*/
package isabelle
@@ -9,80 +9,92 @@
object Build_Vampire
{
- val default_repository = "https://github.com/vprover/vampire.git"
- val default_version1 = "4.5.1"
- val default_version2 = "df87588848db"
+ val default_download_url = "https://github.com/vprover/vampire/archive/refs/tags/v4.6.tar.gz"
val default_jobs = 1
- def make_component_name(version: String): String = "vampire-" + version
+ def make_component_name(version: String): String =
+ "vampire-" + Library.try_unprefix("v", version).getOrElse(version)
/* build Vampire */
def build_vampire(
- repository: String = default_repository,
- version1: String = default_version1,
- version2: String = default_version2,
+ download_url: String = default_download_url,
jobs: Int = default_jobs,
component_name: String = "",
verbose: Boolean = false,
progress: Progress = new Progress,
target_dir: Path = Path.current): Unit =
{
- Isabelle_System.require_command("git")
Isabelle_System.require_command("cmake")
Isabelle_System.with_tmp_dir("build")(tmp_dir =>
{
- /* component and platform */
+ /* component */
+
+ val Archive_Name = """^.*?([^/]+)$""".r
+ val Version = """^v?([0-9.]+)\.tar.gz$""".r
- val component = proper_string(component_name) getOrElse make_component_name(version1)
+ val archive_name =
+ download_url match {
+ case Archive_Name(name) => name
+ case _ => error("Failed to determine source archive name from " + quote(download_url))
+ }
+
+ val version =
+ archive_name match {
+ case Version(version) => version
+ case _ => error("Failed to determine component version from " + quote(archive_name))
+ }
+
+ val component = proper_string(component_name) getOrElse make_component_name(version)
val component_dir = Isabelle_System.new_directory(target_dir + Path.basic(component))
progress.echo("Component " + component_dir)
+
+ /* platform */
+
val platform_name =
proper_string(Isabelle_System.getenv("ISABELLE_PLATFORM64")) getOrElse
error("No 64bit platform")
+
val platform_dir = Isabelle_System.make_directory(component_dir + Path.basic(platform_name))
- /* clone repository */
+ /* download source */
+
+ val archive_path = tmp_dir + Path.basic(archive_name)
+ Isabelle_System.download_file(download_url, archive_path, progress = progress)
- progress.echo("Cloning repository " + repository)
- progress.bash("git clone " + Bash.string(repository) + " vampire",
- cwd = tmp_dir.file, echo = verbose).check
+ Isabelle_System.bash("tar xzf " + File.bash_path(archive_path), cwd = tmp_dir.file).check
+ val source_name = File.get_dir(tmp_dir)
- val source_dir = tmp_dir + Path.explode("vampire")
-
- Isabelle_System.copy_file(source_dir + Path.explode("LICENCE"), component_dir)
+ Isabelle_System.bash(
+ "tar xzf " + archive_path + " && mv " + Bash.string(source_name) + " src",
+ cwd = component_dir.file).check
- /* build versions */
+ /* build */
- for { (rev, exe) <- List(version1 -> "vampire", version2 -> "vampire_polymorphic") } {
- progress.echo("Building " + exe + " (rev " + rev + ")")
- progress.bash("git checkout --quiet --detach " + Bash.string(rev),
- cwd = source_dir.file, echo = verbose).check
+ progress.echo("Building Vampire for " + platform_name + " ...")
- val build_dir = source_dir + Path.explode("build")
- Isabelle_System.rm_tree(build_dir)
- Isabelle_System.make_directory(build_dir)
+ val build_dir = tmp_dir + Path.basic(source_name)
+ Isabelle_System.copy_file(build_dir + Path.explode("LICENCE"), component_dir)
- val cmake_opts = if (Platform.is_linux) "-DBUILD_SHARED_LIBS=0 " else ""
- val cmake_out =
- progress.bash("cmake " + cmake_opts + """-G "Unix Makefiles" ..""",
- cwd = build_dir.file, echo = verbose).check.out
+ val cmake_opts = if (Platform.is_linux) "-DBUILD_SHARED_LIBS=0 " else ""
+ val cmake_out =
+ progress.bash("cmake " + cmake_opts + """-G "Unix Makefiles" .""",
+ cwd = build_dir.file, echo = verbose).check.out
- val Pattern = """-- Setting binary name to '?([^\s']*)'?""".r
- val binary =
- split_lines(cmake_out).collectFirst({ case Pattern(name) => name })
- .getOrElse(error("Failed to determine binary name from cmake output:\n" + cmake_out))
+ val Pattern = """-- Setting binary name to '?([^\s']*)'?""".r
+ val binary =
+ split_lines(cmake_out).collectFirst({ case Pattern(name) => name })
+ .getOrElse(error("Failed to determine binary name from cmake output:\n" + cmake_out))
- progress.bash("make -j" + jobs, cwd = build_dir.file, echo = verbose).check
+ progress.bash("make -j" + jobs, cwd = build_dir.file, echo = verbose).check
- Isabelle_System.copy_file(build_dir + Path.basic("bin") + Path.basic(binary).platform_exe,
- platform_dir + Path.basic(exe).platform_exe)
- }
+ Isabelle_System.copy_file(build_dir + Path.basic("bin") + Path.basic(binary).platform_exe,
+ platform_dir + Path.basic("vampire").platform_exe)
/* settings */
@@ -94,26 +106,16 @@
VAMPIRE_HOME="$COMPONENT/$ISABELLE_PLATFORM64"
ISABELLE_VAMPIRE="$VAMPIRE_HOME/vampire"
-ISABELLE_VAMPIRE_POLYMORPHIC="$VAMPIRE_HOME/vampire_polymorphic"
""")
/* README */
File.write(component_dir + Path.basic("README"),
- "This Isabelle component provides two versions of Vampire from\n" + repository + """
-
- * vampire: standard version (regular stable release)
- * vampire_polymorphic: special version for polymorphic FOL and HOL
- (intermediate repository version)
+ "This Isabelle component provides Vampire " + version + """using the
+original sources from """.stripMargin + download_url + """
-The executables have been built like this:
-
- git checkout COMMIT
- cmake .
- make
-
-The precise commit id is revealed by executing "vampire --version".
+The executables have been built via "cmake . && make"
Makarius
@@ -129,9 +131,7 @@
args =>
{
var target_dir = Path.current
- var repository = default_repository
- var version1 = default_version1
- var version2 = default_version2
+ var download_url = default_download_url
var jobs = default_jobs
var component_name = ""
var verbose = false
@@ -141,19 +141,16 @@
Options are:
-D DIR target directory (default ".")
- -U URL repository (default: """" + default_repository + """")
- -V REV1 standard version (default: """" + default_version1 + """")
- -W REV2 polymorphic version (default: """" + default_version2 + """")
+ -U URL download URL
+ (default: """" + default_download_url + """")
-j NUMBER parallel jobs for make (default: """ + default_jobs + """)
- -n NAME component name (default: """" + make_component_name("REV1") + """")
+ -n NAME component name (default: """" + make_component_name("VERSION") + """")
-v verbose
Build prover component from official download.
""",
"D:" -> (arg => target_dir = Path.explode(arg)),
- "U:" -> (arg => repository = arg),
- "V:" -> (arg => version1 = arg),
- "W:" -> (arg => version2 = arg),
+ "U:" -> (arg => download_url = arg),
"j:" -> (arg => jobs = Value.Nat.parse(arg)),
"n:" -> (arg => component_name = arg),
"v" -> (_ => verbose = true))
@@ -163,8 +160,7 @@
val progress = new Console_Progress()
- build_vampire(repository = repository, version1 = version1, version2 = version2,
- component_name = component_name, jobs = jobs, verbose = verbose, progress = progress,
- target_dir = target_dir)
+ build_vampire(download_url = download_url, component_name = component_name,
+ jobs = jobs, verbose = verbose, progress = progress, target_dir = target_dir)
})
}
--- a/src/Pure/Admin/build_zipperposition.scala Mon Sep 20 14:24:11 2021 +0200
+++ b/src/Pure/Admin/build_zipperposition.scala Thu Oct 07 10:20:10 2021 +0200
@@ -22,7 +22,7 @@
{
Isabelle_System.with_tmp_dir("build")(build_dir =>
{
- if (!Platform.is_windows) Isabelle_System.require_command("patchelf")
+ if (Platform.is_linux) Isabelle_System.require_command("patchelf")
/* component */
--- a/src/Pure/Admin/isabelle_cronjob.scala Mon Sep 20 14:24:11 2021 +0200
+++ b/src/Pure/Admin/isabelle_cronjob.scala Thu Oct 07 10:20:10 2021 +0200
@@ -315,7 +315,7 @@
List(
List(Remote_Build("Linux A", "augsburg1",
options = "-m32 -B -M1x2,2,4" +
- " -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAMLFIND=ocamlfind -e ISABELLE_OCAML_SETUP=true" +
+ " -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAMLFIND=ocamlfind" +
" -e ISABELLE_GHC_SETUP=true" +
" -e ISABELLE_MLTON=mlton" +
" -e ISABELLE_SMLNJ=sml" +
--- a/src/Pure/Isar/toplevel.ML Mon Sep 20 14:24:11 2021 +0200
+++ b/src/Pure/Isar/toplevel.ML Thu Oct 07 10:20:10 2021 +0200
@@ -10,6 +10,7 @@
type state
val init_toplevel: unit -> state
val theory_toplevel: theory -> state
+ val get_prev_theory: theory -> serial
val is_toplevel: state -> bool
val is_theory: state -> bool
val is_proof: state -> bool
@@ -146,6 +147,14 @@
fun init_toplevel () = State (node_presentation Toplevel, NONE);
fun theory_toplevel thy = State (node_presentation (Theory (Context.Theory thy)), NONE);
+val prev_theory = Config.declare_int ("prev_theory", Position.none) (K 0);
+fun get_prev_theory thy = Config.get_global thy prev_theory;
+fun set_prev_theory (State (_, SOME prev_thy)) (Theory gthy) =
+ let
+ val put = Config.put_global prev_theory (Context.theory_identifier prev_thy);
+ val gthy' = gthy |> Context.mapping put (Local_Theory.raw_theory put);
+ in Theory gthy' end
+ | set_prev_theory _ node = node;
fun level state =
(case node_of state of
@@ -302,7 +311,7 @@
Runtime.controlled_execution (try generic_theory_of state)
(fn () => (f int state; State (node_presentation node, previous_theory_of state))) ()
| (Transaction _, Toplevel) => raise UNDEF
- | (Transaction (f, g), node) => apply (fn x => f int x) g node
+ | (Transaction (f, g), node) => apply (fn x => f int x) g (set_prev_theory state node)
| _ => raise UNDEF);
fun apply_union _ [] state = raise FAILURE (state, UNDEF)
--- a/src/Pure/Syntax/syntax_trans.ML Mon Sep 20 14:24:11 2021 +0200
+++ b/src/Pure/Syntax/syntax_trans.ML Thu Oct 07 10:20:10 2021 +0200
@@ -38,8 +38,7 @@
val mk_binder_tr': string * string -> string * (Proof.context -> term list -> term)
val preserve_binder_abs_tr': string -> string -> string * (Proof.context -> term list -> term)
val preserve_binder_abs2_tr': string -> string -> string * (Proof.context -> term list -> term)
- val variant_abs: string * typ * term -> string * term
- val variant_abs': string * typ * term -> string * term
+ val print_abs: string * typ * term -> string * term
val dependent_tr': string * string -> term list -> term
val antiquote_tr': string -> term -> term
val quote_tr': string -> term -> term
@@ -129,8 +128,7 @@
fun abs_tr [Free x, t] = absfree_proper x t
| abs_tr [Const ("_idtdummy", T), t] = absdummy T t
- | abs_tr [Const ("_constrain", _) $ x $ tT, t] =
- Syntax.const "_constrainAbs" $ abs_tr [x, t] $ tT
+ | abs_tr [Const ("_constrain", _) $ x $ tT, t] = Syntax.const "_constrainAbs" $ abs_tr [x, t] $ tT
| abs_tr ts = raise TERM ("abs_tr", ts);
@@ -140,9 +138,7 @@
let
fun err ts = raise TERM ("binder_tr: " ^ syn, ts)
fun binder_tr [Const ("_idts", _) $ idt $ idts, t] = binder_tr [idt, binder_tr [idts, t]]
- | binder_tr [x, t] =
- let val abs = abs_tr [x, t] handle TERM _ => err [x, t]
- in Syntax.const name $ abs end
+ | binder_tr [x, t] = Syntax.const name $ (abs_tr [x, t] handle TERM _ => err [x, t])
| binder_tr ts = err ts;
in (syn, fn _ => binder_tr) end;
@@ -392,16 +388,13 @@
(* dependent / nondependent quantifiers *)
-fun var_abs mark (x, T, b) =
+fun print_abs (x, T, b) =
let val (x', _) = Name.variant x (Term.declare_term_names b Name.context)
- in (x', subst_bound (mark (x', T), b)) end;
-
-val variant_abs = var_abs Free;
-val variant_abs' = var_abs mark_bound_abs;
+ in (x', subst_bound (mark_bound_abs (x', T), b)) end;
fun dependent_tr' (q, r) (A :: Abs (x, T, B) :: ts) =
if Term.is_dependent B then
- let val (x', B') = variant_abs' (x, dummyT, B);
+ let val (x', B') = print_abs (x, dummyT, B);
in Term.list_comb (Syntax.const q $ mark_bound_abs (x', T) $ A $ B', ts) end
else Term.list_comb (Syntax.const r $ A $ incr_boundvars ~1 B, ts)
| dependent_tr' _ _ = raise Match;
--- a/src/Pure/Tools/build_docker.scala Mon Sep 20 14:24:11 2021 +0200
+++ b/src/Pure/Tools/build_docker.scala Thu Oct 07 10:20:10 2021 +0200
@@ -15,7 +15,7 @@
private val Isabelle_Name = """^.*?(Isabelle[^/\\:]+)_linux\.tar\.gz$""".r
val packages: List[String] =
- List("curl", "less", "libfontconfig1", "libgomp1", "perl", "pwgen", "rlwrap", "unzip")
+ List("curl", "less", "libfontconfig1", "libgomp1", "pwgen", "rlwrap", "unzip")
val package_collections: Map[String, List[String]] =
Map("X11" -> List("libx11-6", "libxext6", "libxrender1", "libxtst6", "libxi6"),
--- a/src/Pure/Tools/mkroot.scala Mon Sep 20 14:24:11 2021 +0200
+++ b/src/Pure/Tools/mkroot.scala Thu Oct 07 10:20:10 2021 +0200
@@ -85,8 +85,8 @@
%\""" + """usepackage{eurosym}
%for \<euro>
-%\""" + """usepackage[only,bigsqcap,fatsemi,interleave,sslash]{stmaryrd}
- %for \<Sqinter>, \<Zsemi>
+%\""" + """usepackage[only,bigsqcap,bigparallel,fatsemi,interleave,sslash]{stmaryrd}
+ %for \<Sqinter>, \<Parallel>, \<Zsemi>, \<Parallel>, \<sslash>
%\""" + """usepackage{eufrak}
%for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)
--- a/src/Pure/context.ML Mon Sep 20 14:24:11 2021 +0200
+++ b/src/Pure/context.ML Thu Oct 07 10:20:10 2021 +0200
@@ -39,6 +39,7 @@
val theory_long_name: theory -> string
val theory_name: theory -> string
val theory_name': {long: bool} -> theory -> string
+ val theory_identifier: theory -> serial
val PureN: string
val pretty_thy: theory -> Pretty.T
val pretty_abbrev_thy: theory -> Pretty.T
@@ -155,7 +156,6 @@
val theory_identity = #1 o rep_theory;
val theory_id = #theory_id o theory_identity;
-
val identity_of_id = #1 o rep_theory_id;
val identity_of = identity_of_id o theory_id;
val history_of_id = #2 o rep_theory_id;
@@ -173,6 +173,7 @@
val theory_long_name = #name o history_of;
val theory_name = Long_Name.base_name o theory_long_name;
fun theory_name' {long} = if long then theory_long_name else theory_name;
+val theory_identifier = #id o identity_of_id o theory_id;
val parents_of = #parents o ancestry_of;
val ancestors_of = #ancestors o ancestry_of;
--- a/src/Pure/term.ML Mon Sep 20 14:24:11 2021 +0200
+++ b/src/Pure/term.ML Thu Oct 07 10:20:10 2021 +0200
@@ -165,6 +165,7 @@
val could_beta_contract: term -> bool
val could_eta_contract: term -> bool
val could_beta_eta_contract: term -> bool
+ val used_free: string -> term -> bool
val dest_abs: string * typ * term -> string * term
val dummy_pattern: typ -> term
val dummy: term
--- a/src/Tools/Code/code_thingol.ML Mon Sep 20 14:24:11 2021 +0200
+++ b/src/Tools/Code/code_thingol.ML Thu Oct 07 10:20:10 2021 +0200
@@ -622,9 +622,8 @@
pair (IVar (SOME v))
| translate_term ctxt algbr eqngr permissive some_thm (Abs (v, ty, t), some_abs) =
let
- val (v', t') = Syntax_Trans.variant_abs (Name.desymbolize (SOME false) v, ty, t);
- val v'' = if member (op =) (Term.add_free_names t' []) v'
- then SOME v' else NONE
+ val (v', t') = Term.dest_abs (Name.desymbolize (SOME false) v, ty, t);
+ val v'' = if Term.used_free v' t' then SOME v' else NONE
in
translate_typ ctxt algbr eqngr permissive ty
##>> translate_term ctxt algbr eqngr permissive some_thm (t', some_abs)