# HG changeset patch # User paulson # Date 1581937647 0 # Node ID 7b8a6840e85f2443fc72efa53379b322591f8b89 # Parent fb08117a106ba1a7a791983f705caccb9a51aea9# Parent 9edb7fb69bc259a25d9676ed5cbf62b7f5dcf08e merged diff -r 9edb7fb69bc2 -r 7b8a6840e85f .hgtags --- 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 diff -r 9edb7fb69bc2 -r 7b8a6840e85f CONTRIBUTORS --- 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 diff -r 9edb7fb69bc2 -r 7b8a6840e85f NEWS --- 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) diff -r 9edb7fb69bc2 -r 7b8a6840e85f src/HOL/Analysis/Brouwer_Fixpoint.thy --- 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 \ (\x\s. \y\s. x \ y \ (\z\s. z = x \ z = y))" - by (auto simp: card_Suc_eq eval_nat_numeral) - lemma ksimplex_replace_2: assumes s: "ksimplex p n s" and "a \ s" and "n \ 0" and lb: "\jx\s - {a}. x j \ 0" @@ -1231,7 +1228,7 @@ done qed then show ?thesis - using s \a \ s\ by (simp add: card_2_exists Ex1_def) metis + using s \a \ s\ by (simp add: card_2_iff' Ex1_def) metis qed text \Hence another step towards concreteness.\ diff -r 9edb7fb69bc2 -r 7b8a6840e85f src/HOL/Finite_Set.thy --- 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\y" - using assms by (blast dest: card_eq_SucD) - lemma is_singleton_altdef: "is_singleton A \ card A = 1" unfolding is_singleton_def by (auto elim!: card_1_singletonE is_singletonE simp del: One_nat_def) diff -r 9edb7fb69bc2 -r 7b8a6840e85f src/HOL/Library/Ramsey.thy --- 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 = (\x\A. \y\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) diff -r 9edb7fb69bc2 -r 7b8a6840e85f src/HOL/List.thy --- 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 (\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 \ sorted_wrt f (filter P xs)" +by (induction xs) auto + lemma sorted_wrt_rev: "sorted_wrt P (rev xs) = sorted_wrt (\x y. P y x) xs" by (induction xs) (auto simp add: sorted_wrt_append) diff -r 9edb7fb69bc2 -r 7b8a6840e85f src/HOL/Parity.thy --- 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: - \a = b \ (even a \ even b) \ a div 2 = b div 2\ - 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 + \a = b \ (even a \ even b) \ a div 2 = b div 2\ (is \?P = ?Q\) +proof + assume ?P + then show ?Q + by simp +next + assume ?Q + then have \even a \ even b\ and \a div 2 = b div 2\ + by simp_all + show ?P + proof (rule bit_eqI) + fix n + show \bit a n \ bit b n\ + proof (cases n) + case 0 + with \even a \ even b\ show ?thesis + by simp + next + case (Suc n) + moreover from \a div 2 = b div 2\ have \bit (a div 2) n = bit (b div 2) n\ + by simp + ultimately show ?thesis + by simp + qed + qed +qed lemma bit_mask_iff: \bit (2 ^ m - 1) n \ 2 ^ n \ 0 \ n < m\ diff -r 9edb7fb69bc2 -r 7b8a6840e85f src/HOL/Set_Interval.thy --- 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 \ (\x y. S = {x,y} \ x \ y)" +by (auto simp: card_Suc_eq numeral_eq_Suc) + +lemma card_2_iff': "card S = 2 \ (\x\S. \y\S. x \ y \ (\z\S. z = x \ z = y))" +by (auto simp: card_Suc_eq numeral_eq_Suc) + context ord begin diff -r 9edb7fb69bc2 -r 7b8a6840e85f src/HOL/ex/Bit_Lists.thy --- 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 \Bit representations with bit operations\ diff -r 9edb7fb69bc2 -r 7b8a6840e85f src/HOL/ex/Bit_Operations.thy --- 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 \Instances for \<^typ>\integer\ and \<^typ>\natural\\ + +unbundle integer.lifting natural.lifting + +context + includes lifting_syntax +begin + +lemma transfer_rule_bit_integer [transfer_rule]: + \((pcr_integer :: int \ integer \ bool) ===> (=)) bit bit\ + by (unfold bit_def) transfer_prover + +lemma transfer_rule_bit_natural [transfer_rule]: + \((pcr_natural :: nat \ natural \ bool) ===> (=)) bit bit\ + by (unfold bit_def) transfer_prover + end + +instantiation integer :: ring_bit_operations +begin + +lift_definition not_integer :: \integer \ integer\ + is not . + +lift_definition and_integer :: \integer \ integer \ integer\ + is \and\ . + +lift_definition or_integer :: \integer \ integer \ integer\ + is or . + +lift_definition xor_integer :: \integer \ integer \ integer\ + is xor . + +instance proof + fix k l :: \integer\ and n :: nat + show \- k = NOT (k - 1)\ + by transfer (simp add: minus_eq_not_minus_1) + show \bit (NOT k) n \ (2 :: integer) ^ n \ 0 \ \ bit k n\ + by transfer (fact bit_not_iff) + show \bit (k AND l) n \ bit k n \ bit l n\ + by transfer (fact and_int.bit_eq_iff) + show \bit (k OR l) n \ bit k n \ bit l n\ + by transfer (fact or_int.bit_eq_iff) + show \bit (k XOR l) n \ bit k n \ bit l n\ + by transfer (fact xor_int.bit_eq_iff) +qed + +end + +instantiation natural :: semiring_bit_operations +begin + +lift_definition and_natural :: \natural \ natural \ natural\ + is \and\ . + +lift_definition or_natural :: \natural \ natural \ natural\ + is or . + +lift_definition xor_natural :: \natural \ natural \ natural\ + is xor . + +instance proof + fix m n :: \natural\ and q :: nat + show \bit (m AND n) q \ bit m q \ bit n q\ + by transfer (fact and_nat.bit_eq_iff) + show \bit (m OR n) q \ bit m q \ bit n q\ + by transfer (fact or_nat.bit_eq_iff) + show \bit (m XOR n) q \ bit m q \ bit n q\ + 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 diff -r 9edb7fb69bc2 -r 7b8a6840e85f src/HOL/ex/Word.thy --- 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 diff -r 9edb7fb69bc2 -r 7b8a6840e85f src/Pure/Tools/phabricator.scala --- 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] diff -r 9edb7fb69bc2 -r 7b8a6840e85f src/Pure/thm.ML --- 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 =