--- a/.hgtags Mon Feb 17 11:07:09 2020 +0000
+++ b/.hgtags Mon Feb 17 11:07:27 2020 +0000
@@ -36,3 +36,4 @@
64b47495676d5d6bdec02032a7a90fe6e1ff6c50 Isabelle2017
91162dd89571fb9ddfa36844fdb1a16aea13adcf Isabelle2018
83774d669b5181fb28d19d7a0219fbf6c6d38aab Isabelle2019
+21c0b3a9d2f8f27800f7ea9c8f0fe92139e9e2c3 Isabelle2020-RC0
--- a/CONTRIBUTORS Mon Feb 17 11:07:09 2020 +0000
+++ b/CONTRIBUTORS Mon Feb 17 11:07:27 2020 +0000
@@ -6,23 +6,34 @@
Contributions to this Isabelle2020
----------------------------------
-* 2019: Makarius Wenzel
- More scalable Isabelle dump and underlying headless PIDE session.
+* February 2020: E. Gunther, M. Pagano and P. Sánchez Terraf
+ Simplified, generalised version of ZF/Constructible.
+
+* January 2020: LC Paulson
+ The full finite Ramsey's theorem and elements of finite and infinite
+ Ramsey theory.
-* December 2019:
- Basil Fürer, Andreas Lochbihler, Joshua Schneider, Dmitriy Traytel
+* December 2019: Basil Fürer, Andreas Lochbihler, Joshua Schneider, Dmitriy
+ Traytel
Extension of lift_bnf to support quotient types.
+* October..December 2019: Makarius Wenzel
+ Isabelle/Phabrictor server setup, including Linux platform support in
+ Isabelle/Scala. Client-side tool "isabelle hg_setup".
+
* October 2019: Maximilian Schäffeler
Port of the HOL Light decision procedure for metric spaces.
-* January 2020: LC Paulson
- The full finite Ramsey's theorem and elements of finite and infinite
- Ramsey theory.
+* October 2019: Makarius Wenzel
+ More scalable Isabelle dump and underlying headless PIDE session.
-* February 2020: E. Gunther, M. Pagano and P. Sánchez Terraf
- Simplified, generalised version of ZF/Constructible.
+* August 2019: Makarius Wenzel
+ Better support for proof terms in Isabelle/Pure, notably via method
+ combinator SUBPROOFS (ML) and "subproofs" (Isar).
+* July 2019: Alexander Krauss, Makarius Wenzel
+ Minimal support for a soft-type system within the Isabelle logical
+ framework.
Contributions to Isabelle2019
--- a/NEWS Mon Feb 17 11:07:09 2020 +0000
+++ b/NEWS Mon Feb 17 11:07:27 2020 +0000
@@ -33,6 +33,12 @@
facts. The former graph visualization has been discontinued, because it
was hardly usable.
+* Refined treatment of proof terms, including type-class proofs for
+minor object-logics (FOL, FOLP, Sequents).
+
+* The inference kernel is now confined to one main module: structure
+Thm, without the former circular dependency on structure Axclass.
+
*** Isar ***
@@ -97,8 +103,11 @@
* Session HOL-Analysis: proof method "metric" implements a decision
procedure for simple linear statements in metric spaces.
-* Session HOL-Word: Bitwise NOT-operator has proper prefix syntax. Minor
-INCOMPATIBILITY.
+* Session HOL-Word: bitwise NOT-operator has proper prefix syntax. Minor
+INCOMPATIBILITY.
+
+* Session HOL-Proofs: build faster thanks to better treatment of proof
+terms in Isabelle/Pure.
*** ML ***
@@ -109,6 +118,16 @@
* Antiquotation @{oracle_name} inlines a formally checked oracle name.
+* Minimal support for a soft-type system within the Isabelle logical
+framework (module Soft_Type_System).
+
+* Former Proof_Context.auto_fixes has been replaced by slightly more
+general Proof_Context.augment: it is subject to an optional soft-type
+system of the underlying object-logic. Minor INCOMPATIBILITY.
+
+* More scalable Export.export using XML.tree to avoid premature string
+allocations, with convenient shortcut XML.blob. Minor INCOMPATIBILITY.
+
*** System ***
@@ -140,6 +159,12 @@
splitting sessions and supporting a base logic image. Minor
INCOMPATIBILITY in options and parameters.
+* Isabelle/Scala support for the Linux platform (Ubuntu): packages,
+users, system services.
+
+* Isabelle/Scala support for proof terms (with full type/term
+information) in module isabelle.Term.
+
* Theory export via Isabelle/Scala has been reworked. The former "fact"
name space is now split into individual "thm" items: names are
potentially indexed, such as "foo" for singleton facts, or "bar(1)",
@@ -151,6 +176,13 @@
* Old settings variables ISABELLE_PLATFORM and ISABELLE_WINDOWS_PLATFORM
have been discontinued -- deprecated since Isabelle2018.
+* More complete x86_64 platform support on macOS, notably Catalina where
+old x86 has been discontinued.
+
+* Update to GHC stack 2.1.3 with stackage lts-13.19/ghc-8.6.4.
+
+* Update to OCaml Opam 2.0.6 (using ocaml 4.05.0 as before).
+
New in Isabelle2019 (June 2019)
--- a/src/HOL/Analysis/Brouwer_Fixpoint.thy Mon Feb 17 11:07:09 2020 +0000
+++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy Mon Feb 17 11:07:27 2020 +0000
@@ -851,9 +851,6 @@
by simp
qed
-lemma card_2_exists: "card s = 2 \<longleftrightarrow> (\<exists>x\<in>s. \<exists>y\<in>s. x \<noteq> y \<and> (\<forall>z\<in>s. z = x \<or> z = y))"
- by (auto simp: card_Suc_eq eval_nat_numeral)
-
lemma ksimplex_replace_2:
assumes s: "ksimplex p n s" and "a \<in> s" and "n \<noteq> 0"
and lb: "\<forall>j<n. \<exists>x\<in>s - {a}. x j \<noteq> 0"
@@ -1231,7 +1228,7 @@
done
qed
then show ?thesis
- using s \<open>a \<in> s\<close> by (simp add: card_2_exists Ex1_def) metis
+ using s \<open>a \<in> s\<close> by (simp add: card_2_iff' Ex1_def) metis
qed
text \<open>Hence another step towards concreteness.\<close>
--- a/src/HOL/Finite_Set.thy Mon Feb 17 11:07:09 2020 +0000
+++ b/src/HOL/Finite_Set.thy Mon Feb 17 11:07:27 2020 +0000
@@ -1785,11 +1785,6 @@
obtains x where "A = {x}"
using assms by (auto simp: card_Suc_eq)
-lemma card_2_doubletonE:
- assumes "card A = Suc (Suc 0)"
- obtains x y where "A = {x,y}" "x\<noteq>y"
- using assms by (blast dest: card_eq_SucD)
-
lemma is_singleton_altdef: "is_singleton A \<longleftrightarrow> card A = 1"
unfolding is_singleton_def
by (auto elim!: card_1_singletonE is_singletonE simp del: One_nat_def)
--- a/src/HOL/Library/Ramsey.thy Mon Feb 17 11:07:09 2020 +0000
+++ b/src/HOL/Library/Ramsey.thy Mon Feb 17 11:07:27 2020 +0000
@@ -19,8 +19,7 @@
by (auto simp: nsets_def)
lemma nsets_2_eq: "nsets A 2 = (\<Union>x\<in>A. \<Union>y\<in>A - {x}. {{x, y}})"
- unfolding numeral_2_eq_2
- by (auto simp: nsets_def elim!: card_2_doubletonE)
+by (auto simp: nsets_def card_2_iff)
lemma nsets_doubleton_2_eq [simp]: "[{x, y}]\<^bsup>2\<^esup> = (if x=y then {} else {{x, y}})"
by (auto simp: nsets_2_eq)
--- a/src/HOL/List.thy Mon Feb 17 11:07:09 2020 +0000
+++ b/src/HOL/List.thy Mon Feb 17 11:07:27 2020 +0000
@@ -5172,6 +5172,20 @@
"sorted_wrt R (map f xs) = sorted_wrt (\<lambda>x y. R (f x) (f y)) xs"
by (induction xs) simp_all
+lemma
+ assumes "sorted_wrt f xs"
+ shows sorted_wrt_take: "sorted_wrt f (take n xs)"
+ and sorted_wrt_drop: "sorted_wrt f (drop n xs)"
+proof -
+ from assms have "sorted_wrt f (take n xs @ drop n xs)" by simp
+ thus "sorted_wrt f (take n xs)" and "sorted_wrt f (drop n xs)"
+ unfolding sorted_wrt_append by simp_all
+qed
+
+lemma sorted_wrt_filter:
+ "sorted_wrt f xs \<Longrightarrow> sorted_wrt f (filter P xs)"
+by (induction xs) auto
+
lemma sorted_wrt_rev:
"sorted_wrt P (rev xs) = sorted_wrt (\<lambda>x y. P y x) xs"
by (induction xs) (auto simp add: sorted_wrt_append)
--- a/src/HOL/Parity.thy Mon Feb 17 11:07:09 2020 +0000
+++ b/src/HOL/Parity.thy Mon Feb 17 11:07:27 2020 +0000
@@ -890,17 +890,32 @@
by (cases n, auto simp add: bit_def ac_simps)
lemma bit_eq_rec:
- \<open>a = b \<longleftrightarrow> (even a \<longleftrightarrow> even b) \<and> a div 2 = b div 2\<close>
- apply (auto simp add: bit_eq_iff)
- using bit_0 apply blast
- using bit_0 apply blast
- using bit_Suc apply blast
- using bit_Suc apply blast
- apply (metis bit_eq_iff even_iff_mod_2_eq_zero mod_div_mult_eq)
- apply (metis bit_eq_iff even_iff_mod_2_eq_zero mod_div_mult_eq)
- apply (metis bit_eq_iff mod2_eq_if mod_div_mult_eq)
- apply (metis bit_eq_iff mod2_eq_if mod_div_mult_eq)
- done
+ \<open>a = b \<longleftrightarrow> (even a \<longleftrightarrow> even b) \<and> a div 2 = b div 2\<close> (is \<open>?P = ?Q\<close>)
+proof
+ assume ?P
+ then show ?Q
+ by simp
+next
+ assume ?Q
+ then have \<open>even a \<longleftrightarrow> even b\<close> and \<open>a div 2 = b div 2\<close>
+ by simp_all
+ show ?P
+ proof (rule bit_eqI)
+ fix n
+ show \<open>bit a n \<longleftrightarrow> bit b n\<close>
+ proof (cases n)
+ case 0
+ with \<open>even a \<longleftrightarrow> even b\<close> show ?thesis
+ by simp
+ next
+ case (Suc n)
+ moreover from \<open>a div 2 = b div 2\<close> have \<open>bit (a div 2) n = bit (b div 2) n\<close>
+ by simp
+ ultimately show ?thesis
+ by simp
+ qed
+ qed
+qed
lemma bit_mask_iff:
\<open>bit (2 ^ m - 1) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> n < m\<close>
--- a/src/HOL/Set_Interval.thy Mon Feb 17 11:07:09 2020 +0000
+++ b/src/HOL/Set_Interval.thy Mon Feb 17 11:07:27 2020 +0000
@@ -15,6 +15,13 @@
imports Divides
begin
+(* Belongs in Finite_Set but 2 is not available there *)
+lemma card_2_iff: "card S = 2 \<longleftrightarrow> (\<exists>x y. S = {x,y} \<and> x \<noteq> y)"
+by (auto simp: card_Suc_eq numeral_eq_Suc)
+
+lemma card_2_iff': "card S = 2 \<longleftrightarrow> (\<exists>x\<in>S. \<exists>y\<in>S. x \<noteq> y \<and> (\<forall>z\<in>S. z = x \<or> z = y))"
+by (auto simp: card_Suc_eq numeral_eq_Suc)
+
context ord
begin
--- a/src/HOL/ex/Bit_Lists.thy Mon Feb 17 11:07:09 2020 +0000
+++ b/src/HOL/ex/Bit_Lists.thy Mon Feb 17 11:07:27 2020 +0000
@@ -285,6 +285,8 @@
"unsigned_of_bits bs = (of_bits (bs @ [False]) :: int)"
by (simp add: of_bits_int_def)
+unbundle word.lifting
+
instantiation word :: (len) bit_representation
begin
@@ -303,6 +305,9 @@
end
+lifting_update word.lifting
+lifting_forget word.lifting
+
subsection \<open>Bit representations with bit operations\<close>
--- a/src/HOL/ex/Bit_Operations.thy Mon Feb 17 11:07:09 2020 +0000
+++ b/src/HOL/ex/Bit_Operations.thy Mon Feb 17 11:07:27 2020 +0000
@@ -530,4 +530,84 @@
end
+
+subsubsection \<open>Instances for \<^typ>\<open>integer\<close> and \<^typ>\<open>natural\<close>\<close>
+
+unbundle integer.lifting natural.lifting
+
+context
+ includes lifting_syntax
+begin
+
+lemma transfer_rule_bit_integer [transfer_rule]:
+ \<open>((pcr_integer :: int \<Rightarrow> integer \<Rightarrow> bool) ===> (=)) bit bit\<close>
+ by (unfold bit_def) transfer_prover
+
+lemma transfer_rule_bit_natural [transfer_rule]:
+ \<open>((pcr_natural :: nat \<Rightarrow> natural \<Rightarrow> bool) ===> (=)) bit bit\<close>
+ by (unfold bit_def) transfer_prover
+
end
+
+instantiation integer :: ring_bit_operations
+begin
+
+lift_definition not_integer :: \<open>integer \<Rightarrow> integer\<close>
+ is not .
+
+lift_definition and_integer :: \<open>integer \<Rightarrow> integer \<Rightarrow> integer\<close>
+ is \<open>and\<close> .
+
+lift_definition or_integer :: \<open>integer \<Rightarrow> integer \<Rightarrow> integer\<close>
+ is or .
+
+lift_definition xor_integer :: \<open>integer \<Rightarrow> integer \<Rightarrow> integer\<close>
+ is xor .
+
+instance proof
+ fix k l :: \<open>integer\<close> and n :: nat
+ show \<open>- k = NOT (k - 1)\<close>
+ by transfer (simp add: minus_eq_not_minus_1)
+ show \<open>bit (NOT k) n \<longleftrightarrow> (2 :: integer) ^ n \<noteq> 0 \<and> \<not> bit k n\<close>
+ by transfer (fact bit_not_iff)
+ show \<open>bit (k AND l) n \<longleftrightarrow> bit k n \<and> bit l n\<close>
+ by transfer (fact and_int.bit_eq_iff)
+ show \<open>bit (k OR l) n \<longleftrightarrow> bit k n \<or> bit l n\<close>
+ by transfer (fact or_int.bit_eq_iff)
+ show \<open>bit (k XOR l) n \<longleftrightarrow> bit k n \<noteq> bit l n\<close>
+ by transfer (fact xor_int.bit_eq_iff)
+qed
+
+end
+
+instantiation natural :: semiring_bit_operations
+begin
+
+lift_definition and_natural :: \<open>natural \<Rightarrow> natural \<Rightarrow> natural\<close>
+ is \<open>and\<close> .
+
+lift_definition or_natural :: \<open>natural \<Rightarrow> natural \<Rightarrow> natural\<close>
+ is or .
+
+lift_definition xor_natural :: \<open>natural \<Rightarrow> natural \<Rightarrow> natural\<close>
+ is xor .
+
+instance proof
+ fix m n :: \<open>natural\<close> and q :: nat
+ show \<open>bit (m AND n) q \<longleftrightarrow> bit m q \<and> bit n q\<close>
+ by transfer (fact and_nat.bit_eq_iff)
+ show \<open>bit (m OR n) q \<longleftrightarrow> bit m q \<or> bit n q\<close>
+ by transfer (fact or_nat.bit_eq_iff)
+ show \<open>bit (m XOR n) q \<longleftrightarrow> bit m q \<noteq> bit n q\<close>
+ by transfer (fact xor_nat.bit_eq_iff)
+qed
+
+end
+
+lifting_update integer.lifting
+lifting_forget integer.lifting
+
+lifting_update natural.lifting
+lifting_forget natural.lifting
+
+end
--- a/src/HOL/ex/Word.thy Mon Feb 17 11:07:09 2020 +0000
+++ b/src/HOL/ex/Word.thy Mon Feb 17 11:07:27 2020 +0000
@@ -715,4 +715,7 @@
end
+lifting_update word.lifting
+lifting_forget word.lifting
+
end
--- a/src/Pure/Tools/phabricator.scala Mon Feb 17 11:07:09 2020 +0000
+++ b/src/Pure/Tools/phabricator.scala Mon Feb 17 11:07:27 2020 +0000
@@ -63,7 +63,7 @@
val alternative_system_port = 222
val default_server_port = 2222
- val standard_mercurial_source = "https://www.mercurial-scm.org/release/mercurial-2.8.2.tar.gz"
+ val standard_mercurial_source = "https://www.mercurial-scm.org/release/mercurial-3.9.2.tar.gz"
@@ -461,6 +461,8 @@
DocumentRoot """ + config.home.implode + """/webroot
ErrorLog ${APACHE_LOG_DIR}/error.log
+ CustomLog ${APACHE_LOG_DIR}/access.log combined
+
RewriteEngine on
RewriteRule ^(.*)$ /index.php?__path__=$1 [B,L,QSA]
</VirtualHost>
--- a/src/Pure/thm.ML Mon Feb 17 11:07:09 2020 +0000
+++ b/src/Pure/thm.ML Mon Feb 17 11:07:27 2020 +0000
@@ -1694,8 +1694,10 @@
end |> solve_constraints;
(*Remove extra sorts that are witnessed by type signature information*)
-fun strip_shyps (thm as Thm (_, {shyps = [], ...})) = thm
- | strip_shyps (thm as Thm (der, {cert, tags, maxidx, constraints, shyps, hyps, tpairs, prop})) =
+fun strip_shyps thm =
+ (case thm of
+ Thm (_, {shyps = [], ...}) => thm
+ | Thm (der, {cert, tags, maxidx, constraints, shyps, hyps, tpairs, prop}) =>
let
val thy = theory_of_thm thm;
val algebra = Sign.classes_of thy;
@@ -1705,13 +1707,16 @@
val witnessed = Sign.witness_sorts thy present extra;
val extra' = fold (Sorts.remove_sort o #2) witnessed extra
|> Sorts.minimal_sorts algebra;
+ val constraints' = fold (insert_constraints thy) witnessed constraints;
val shyps' = fold (Sorts.insert_sort o #2) present extra';
in
Thm (deriv_rule_unconditional
(Proofterm.strip_shyps_proof algebra present witnessed extra') der,
- {cert = cert, tags = tags, maxidx = maxidx, constraints = constraints,
+ {cert = cert, tags = tags, maxidx = maxidx, constraints = constraints',
shyps = shyps', hyps = hyps, tpairs = tpairs, prop = prop})
- end;
+ end)
+ |> solve_constraints;
+
(*Internalize sort constraints of type variables*)
val unconstrainT =