--- a/NEWS Mon Sep 24 14:33:08 2018 +0100
+++ b/NEWS Mon Sep 24 14:33:17 2018 +0100
@@ -7,11 +7,10 @@
New in this Isabelle version
----------------------------
-*** System ***
-
-* Isabelle server command "use_theories" supports "nodes_status_delay"
-for continuous output of node status information. The time interval is
-specified in seconds; a negative value means it is disabled (default).
+*** General ***
+
+* Old-style inner comments (* ... *) within the term language are no
+longer supported (legacy feature in Isabelle2018).
*** Isar ***
@@ -19,6 +18,10 @@
* More robust treatment of structural errors: begin/end blocks take
precedence over goal/proof.
+* Implicit cases goal1, goal2, goal3, etc. have been discontinued
+(legacy feature since Isabelle2016).
+
+
*** HOL ***
@@ -35,6 +38,9 @@
and prod_mset.swap, similarly to sum.swap and prod.swap.
INCOMPATIBILITY.
+* Theory "HOL-Library.Multiset": the <Union># operator now has the same
+precedence as any other prefix function symbol.
+
*** ML ***
@@ -64,7 +70,11 @@
*** System ***
-* Isabelle Server message "use_theories" terminates more robustly in the
+* Isabelle server command "use_theories" supports "nodes_status_delay"
+for continuous output of node status information. The time interval is
+specified in seconds; a negative value means it is disabled (default).
+
+* Isabelle Server command "use_theories" terminates more robustly in the
presence of structurally broken sources: full consolidation of theories
is no longer required.
--- a/src/Doc/Isar_Ref/Outer_Syntax.thy Mon Sep 24 14:33:08 2018 +0100
+++ b/src/Doc/Isar_Ref/Outer_Syntax.thy Mon Sep 24 14:33:17 2018 +0100
@@ -150,11 +150,10 @@
blocks of ``@{verbatim "\<open>"}~\<open>\<dots>\<close>~@{verbatim "\<close>"}''. Note that the rendering
of cartouche delimiters is usually like this: ``\<open>\<open> \<dots> \<close>\<close>''.
- Source comments take the form \<^verbatim>\<open>(*\<close>~\<open>\<dots>\<close>~\<^verbatim>\<open>*)\<close> and may be nested, although
- the user-interface might prevent this. Note that this form indicates source
- comments only, which are stripped after lexical analysis of the input. The
- Isar syntax also provides proper \<^emph>\<open>document comments\<close> that are considered as
- part of the text (see \secref{sec:comments}).
+ Source comments take the form \<^verbatim>\<open>(*\<close>~\<open>\<dots>\<close>~\<^verbatim>\<open>*)\<close> and may be nested: the text is
+ removed after lexical analysis of the input and thus not suitable for
+ documentation. The Isar syntax also provides proper \<^emph>\<open>document comments\<close>
+ that are considered as part of the text (see \secref{sec:comments}).
Common mathematical symbols such as \<open>\<forall>\<close> are represented in Isabelle as \<^verbatim>\<open>\<forall>\<close>.
There are infinitely many Isabelle symbols like this, although proper
--- a/src/HOL/Analysis/Function_Topology.thy Mon Sep 24 14:33:08 2018 +0100
+++ b/src/HOL/Analysis/Function_Topology.thy Mon Sep 24 14:33:17 2018 +0100
@@ -1,9 +1,9 @@
-(* Author: Sébastien Gouëzel sebastien.gouezel@univ-rennes1.fr
+(* Author: Sébastien Gouëzel sebastien.gouezel@univ-rennes1.fr with additions from LCP
License: BSD
*)
theory Function_Topology
-imports Topology_Euclidean_Space Bounded_Linear_Function Finite_Product_Measure
+imports Topology_Euclidean_Space Bounded_Linear_Function Finite_Product_Measure
begin
@@ -94,13 +94,12 @@
using assms(3) apply (induct rule: generate_topology_on.induct)
using assms(1) assms(2) unfolding istopology_def by auto
-definition%unimportant topology_generated_by::"('a set set) \<Rightarrow> ('a topology)"
- where "topology_generated_by S = topology (generate_topology_on S)"
+abbreviation%unimportant topology_generated_by::"('a set set) \<Rightarrow> ('a topology)"
+ where "topology_generated_by S \<equiv> topology (generate_topology_on S)"
lemma%unimportant openin_topology_generated_by_iff:
"openin (topology_generated_by S) s \<longleftrightarrow> generate_topology_on S s"
-using topology_inverse'[OF istopology_generate_topology_on[of S]]
-unfolding topology_generated_by_def by simp
+ using topology_inverse'[OF istopology_generate_topology_on[of S]] by simp
lemma%unimportant openin_topology_generated_by:
"openin (topology_generated_by S) s \<Longrightarrow> generate_topology_on S s"
@@ -127,6 +126,138 @@
"s \<in> S \<Longrightarrow> openin (topology_generated_by S) s"
by%unimportant (simp only: openin_topology_generated_by_iff, auto simp: generate_topology_on.Basis)
+lemma generate_topology_on_Inter:
+ "\<lbrakk>finite \<F>; \<And>K. K \<in> \<F> \<Longrightarrow> generate_topology_on \<S> K; \<F> \<noteq> {}\<rbrakk> \<Longrightarrow> generate_topology_on \<S> (\<Inter>\<F>)"
+ by (induction \<F> rule: finite_induct; force intro: generate_topology_on.intros)
+
+subsection\<open>Topology bases and sub-bases\<close>
+
+lemma istopology_base_alt:
+ "istopology (arbitrary union_of P) \<longleftrightarrow>
+ (\<forall>S T. (arbitrary union_of P) S \<and> (arbitrary union_of P) T
+ \<longrightarrow> (arbitrary union_of P) (S \<inter> T))"
+ by (simp add: istopology_def) (blast intro: arbitrary_union_of_Union)
+
+lemma istopology_base_eq:
+ "istopology (arbitrary union_of P) \<longleftrightarrow>
+ (\<forall>S T. P S \<and> P T \<longrightarrow> (arbitrary union_of P) (S \<inter> T))"
+ by (simp add: istopology_base_alt arbitrary_union_of_Int_eq)
+
+lemma istopology_base:
+ "(\<And>S T. \<lbrakk>P S; P T\<rbrakk> \<Longrightarrow> P(S \<inter> T)) \<Longrightarrow> istopology (arbitrary union_of P)"
+ by (simp add: arbitrary_def istopology_base_eq union_of_inc)
+
+lemma openin_topology_base_unique:
+ "openin X = arbitrary union_of P \<longleftrightarrow>
+ (\<forall>V. P V \<longrightarrow> openin X V) \<and> (\<forall>U x. openin X U \<and> x \<in> U \<longrightarrow> (\<exists>V. P V \<and> x \<in> V \<and> V \<subseteq> U))"
+ (is "?lhs = ?rhs")
+proof
+ assume ?lhs
+ then show ?rhs
+ by (auto simp: union_of_def arbitrary_def)
+next
+ assume R: ?rhs
+ then have *: "\<exists>\<U>\<subseteq>Collect P. \<Union>\<U> = S" if "openin X S" for S
+ using that by (rule_tac x="{V. P V \<and> V \<subseteq> S}" in exI) fastforce
+ from R show ?lhs
+ by (fastforce simp add: union_of_def arbitrary_def intro: *)
+qed
+
+lemma topology_base_unique:
+ "\<lbrakk>\<And>S. P S \<Longrightarrow> openin X S;
+ \<And>U x. \<lbrakk>openin X U; x \<in> U\<rbrakk> \<Longrightarrow> \<exists>B. P B \<and> x \<in> B \<and> B \<subseteq> U\<rbrakk>
+ \<Longrightarrow> topology(arbitrary union_of P) = X"
+ by (metis openin_topology_base_unique openin_inverse [of X])
+
+lemma topology_bases_eq_aux:
+ "\<lbrakk>(arbitrary union_of P) S;
+ \<And>U x. \<lbrakk>P U; x \<in> U\<rbrakk> \<Longrightarrow> \<exists>V. Q V \<and> x \<in> V \<and> V \<subseteq> U\<rbrakk>
+ \<Longrightarrow> (arbitrary union_of Q) S"
+ by (metis arbitrary_union_of_alt arbitrary_union_of_idempot)
+
+lemma topology_bases_eq:
+ "\<lbrakk>\<And>U x. \<lbrakk>P U; x \<in> U\<rbrakk> \<Longrightarrow> \<exists>V. Q V \<and> x \<in> V \<and> V \<subseteq> U;
+ \<And>V x. \<lbrakk>Q V; x \<in> V\<rbrakk> \<Longrightarrow> \<exists>U. P U \<and> x \<in> U \<and> U \<subseteq> V\<rbrakk>
+ \<Longrightarrow> topology (arbitrary union_of P) =
+ topology (arbitrary union_of Q)"
+ by (fastforce intro: arg_cong [where f=topology] elim: topology_bases_eq_aux)
+
+lemma istopology_subbase:
+ "istopology (arbitrary union_of (finite intersection_of P relative_to S))"
+ by (simp add: finite_intersection_of_Int istopology_base relative_to_Int)
+
+lemma openin_subbase:
+ "openin (topology (arbitrary union_of (finite intersection_of B relative_to U))) S
+ \<longleftrightarrow> (arbitrary union_of (finite intersection_of B relative_to U)) S"
+ by (simp add: istopology_subbase topology_inverse')
+
+lemma topspace_subbase [simp]:
+ "topspace(topology (arbitrary union_of (finite intersection_of B relative_to U))) = U" (is "?lhs = _")
+proof
+ show "?lhs \<subseteq> U"
+ by (metis arbitrary_union_of_relative_to openin_subbase openin_topspace relative_to_imp_subset)
+ show "U \<subseteq> ?lhs"
+ by (metis arbitrary_union_of_inc finite_intersection_of_empty inf.orderE istopology_subbase
+ openin_subset relative_to_inc subset_UNIV topology_inverse')
+qed
+
+lemma minimal_topology_subbase:
+ "\<lbrakk>\<And>S. P S \<Longrightarrow> openin X S; openin X U;
+ openin(topology(arbitrary union_of (finite intersection_of P relative_to U))) S\<rbrakk>
+ \<Longrightarrow> openin X S"
+ apply (simp add: istopology_subbase topology_inverse)
+ apply (simp add: union_of_def intersection_of_def relative_to_def)
+ apply (blast intro: openin_Int_Inter)
+ done
+
+lemma istopology_subbase_UNIV:
+ "istopology (arbitrary union_of (finite intersection_of P))"
+ by (simp add: istopology_base finite_intersection_of_Int)
+
+
+lemma generate_topology_on_eq:
+ "generate_topology_on S = arbitrary union_of finite' intersection_of (\<lambda>x. x \<in> S)" (is "?lhs = ?rhs")
+proof (intro ext iffI)
+ fix A
+ assume "?lhs A"
+ then show "?rhs A"
+ proof induction
+ case (Int a b)
+ then show ?case
+ by (metis (mono_tags, lifting) istopology_base_alt finite'_intersection_of_Int istopology_base)
+ next
+ case (UN K)
+ then show ?case
+ by (simp add: arbitrary_union_of_Union)
+ next
+ case (Basis s)
+ then show ?case
+ by (simp add: Sup_upper arbitrary_union_of_inc finite'_intersection_of_inc relative_to_subset)
+ qed auto
+next
+ fix A
+ assume "?rhs A"
+ then obtain \<U> where \<U>: "\<And>T. T \<in> \<U> \<Longrightarrow> \<exists>\<F>. finite' \<F> \<and> \<F> \<subseteq> S \<and> \<Inter>\<F> = T" and eq: "A = \<Union>\<U>"
+ unfolding union_of_def intersection_of_def by auto
+ show "?lhs A"
+ unfolding eq
+ proof (rule generate_topology_on.UN)
+ fix T
+ assume "T \<in> \<U>"
+ with \<U> obtain \<F> where "finite' \<F>" "\<F> \<subseteq> S" "\<Inter>\<F> = T"
+ by blast
+ have "generate_topology_on S (\<Inter>\<F>)"
+ proof (rule generate_topology_on_Inter)
+ show "finite \<F>" "\<F> \<noteq> {}"
+ by (auto simp: \<open>finite' \<F>\<close>)
+ show "\<And>K. K \<in> \<F> \<Longrightarrow> generate_topology_on S K"
+ by (metis \<open>\<F> \<subseteq> S\<close> generate_topology_on.simps subset_iff)
+ qed
+ then show "generate_topology_on S T"
+ using \<open>\<Inter>\<F> = T\<close> by blast
+ qed
+qed
+
subsubsection%important \<open>Continuity\<close>
text \<open>We will need to deal with continuous maps in terms of topologies and not in terms
@@ -315,11 +446,113 @@
text \<open>The total set of the product topology is the product of the total sets
along each coordinate.\<close>
-lemma%important product_topology_topspace:
+proposition product_topology:
+ "product_topology X I =
+ topology
+ (arbitrary union_of
+ ((finite intersection_of
+ (\<lambda>F. \<exists>i U. F = {f. f i \<in> U} \<and> i \<in> I \<and> openin (X i) U))
+ relative_to (\<Pi>\<^sub>E i\<in>I. topspace (X i))))"
+ (is "_ = topology (_ union_of ((_ intersection_of ?\<Psi>) relative_to ?TOP))")
+proof -
+ let ?\<Omega> = "(\<lambda>F. \<exists>Y. F = Pi\<^sub>E I Y \<and> (\<forall>i. openin (X i) (Y i)) \<and> finite {i. Y i \<noteq> topspace (X i)})"
+ have *: "(finite' intersection_of ?\<Omega>) A = (finite intersection_of ?\<Psi> relative_to ?TOP) A" for A
+ proof -
+ have 1: "\<exists>U. (\<exists>\<U>. finite \<U> \<and> \<U> \<subseteq> Collect ?\<Psi> \<and> \<Inter>\<U> = U) \<and> ?TOP \<inter> U = \<Inter>\<U>"
+ if \<U>: "\<U> \<subseteq> Collect ?\<Omega>" and "finite' \<U>" "A = \<Inter>\<U>" "\<U> \<noteq> {}" for \<U>
+ proof -
+ have "\<forall>U \<in> \<U>. \<exists>Y. U = Pi\<^sub>E I Y \<and> (\<forall>i. openin (X i) (Y i)) \<and> finite {i. Y i \<noteq> topspace (X i)}"
+ using \<U> by auto
+ then obtain Y where Y: "\<And>U. U \<in> \<U> \<Longrightarrow> U = Pi\<^sub>E I (Y U) \<and> (\<forall>i. openin (X i) (Y U i)) \<and> finite {i. (Y U) i \<noteq> topspace (X i)}"
+ by metis
+ obtain U where "U \<in> \<U>"
+ using \<open>\<U> \<noteq> {}\<close> by blast
+ let ?F = "\<lambda>U. (\<lambda>i. {f. f i \<in> Y U i}) ` {i \<in> I. Y U i \<noteq> topspace (X i)}"
+ show ?thesis
+ proof (intro conjI exI)
+ show "finite (\<Union>U\<in>\<U>. ?F U)"
+ using Y \<open>finite' \<U>\<close> by auto
+ show "?TOP \<inter> \<Inter>(\<Union>U\<in>\<U>. ?F U) = \<Inter>\<U>"
+ proof
+ have *: "f \<in> U"
+ if "U \<in> \<U>" and "\<forall>V\<in>\<U>. \<forall>i. i \<in> I \<and> Y V i \<noteq> topspace (X i) \<longrightarrow> f i \<in> Y V i"
+ and "\<forall>i\<in>I. f i \<in> topspace (X i)" and "f \<in> extensional I" for f U
+ proof -
+ have "Pi\<^sub>E I (Y U) = U"
+ using Y \<open>U \<in> \<U>\<close> by blast
+ then show "f \<in> U"
+ using that unfolding PiE_def Pi_def by blast
+ qed
+ show "?TOP \<inter> \<Inter>(\<Union>U\<in>\<U>. ?F U) \<subseteq> \<Inter>\<U>"
+ by (auto simp: PiE_iff *)
+ show "\<Inter>\<U> \<subseteq> ?TOP \<inter> \<Inter>(\<Union>U\<in>\<U>. ?F U)"
+ using Y openin_subset \<open>finite' \<U>\<close> by fastforce
+ qed
+ qed (use Y openin_subset in \<open>blast+\<close>)
+ qed
+ have 2: "\<exists>\<U>'. finite' \<U>' \<and> \<U>' \<subseteq> Collect ?\<Omega> \<and> \<Inter>\<U>' = ?TOP \<inter> \<Inter>\<U>"
+ if \<U>: "\<U> \<subseteq> Collect ?\<Psi>" and "finite \<U>" for \<U>
+ proof (cases "\<U>={}")
+ case True
+ then show ?thesis
+ apply (rule_tac x="{?TOP}" in exI, simp)
+ apply (rule_tac x="\<lambda>i. topspace (X i)" in exI)
+ apply force
+ done
+ next
+ case False
+ then obtain U where "U \<in> \<U>"
+ by blast
+ have "\<forall>U \<in> \<U>. \<exists>i Y. U = {f. f i \<in> Y} \<and> i \<in> I \<and> openin (X i) Y"
+ using \<U> by auto
+ then obtain J Y where
+ Y: "\<And>U. U \<in> \<U> \<Longrightarrow> U = {f. f (J U) \<in> Y U} \<and> J U \<in> I \<and> openin (X (J U)) (Y U)"
+ by metis
+ let ?G = "\<lambda>U. \<Pi>\<^sub>E i\<in>I. if i = J U then Y U else topspace (X i)"
+ show ?thesis
+ proof (intro conjI exI)
+ show "finite (?G ` \<U>)" "?G ` \<U> \<noteq> {}"
+ using \<open>finite \<U>\<close> \<open>U \<in> \<U>\<close> by blast+
+ have *: "\<And>U. U \<in> \<U> \<Longrightarrow> openin (X (J U)) (Y U)"
+ using Y by force
+ show "?G ` \<U> \<subseteq> {Pi\<^sub>E I Y |Y. (\<forall>i. openin (X i) (Y i)) \<and> finite {i. Y i \<noteq> topspace (X i)}}"
+ apply clarsimp
+ apply (rule_tac x=" (\<lambda>i. if i = J U then Y U else topspace (X i))" in exI)
+ apply (auto simp: *)
+ done
+ next
+ show "(\<Inter>U\<in>\<U>. ?G U) = ?TOP \<inter> \<Inter>\<U>"
+ proof
+ have "(\<Pi>\<^sub>E i\<in>I. if i = J U then Y U else topspace (X i)) \<subseteq> (\<Pi>\<^sub>E i\<in>I. topspace (X i))"
+ apply (clarsimp simp: PiE_iff Ball_def all_conj_distrib split: if_split_asm)
+ using Y \<open>U \<in> \<U>\<close> openin_subset by blast+
+ then have "(\<Inter>U\<in>\<U>. ?G U) \<subseteq> ?TOP"
+ using \<open>U \<in> \<U>\<close>
+ by fastforce
+ moreover have "(\<Inter>U\<in>\<U>. ?G U) \<subseteq> \<Inter>\<U>"
+ using PiE_mem Y by fastforce
+ ultimately show "(\<Inter>U\<in>\<U>. ?G U) \<subseteq> ?TOP \<inter> \<Inter>\<U>"
+ by auto
+ qed (use Y in fastforce)
+ qed
+ qed
+ show ?thesis
+ unfolding relative_to_def intersection_of_def
+ by (safe; blast dest!: 1 2)
+ qed
+ show ?thesis
+ unfolding product_topology_def generate_topology_on_eq
+ apply (rule arg_cong [where f = topology])
+ apply (rule arg_cong [where f = "(union_of)arbitrary"])
+ apply (force simp: *)
+ done
+qed
+
+lemma%important topspace_product_topology:
"topspace (product_topology T I) = (\<Pi>\<^sub>E i\<in>I. topspace(T i))"
proof%unimportant
show "topspace (product_topology T I) \<subseteq> (\<Pi>\<^sub>E i\<in>I. topspace (T i))"
- unfolding product_topology_def apply (simp only: topology_generated_by_topspace)
+ unfolding product_topology_def topology_generated_by_topspace
unfolding topspace_def by auto
have "(\<Pi>\<^sub>E i\<in>I. topspace (T i)) \<in> {(\<Pi>\<^sub>E i\<in>I. X i) |X. (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)}}"
using openin_topspace not_finite_existsD by auto
@@ -330,11 +563,11 @@
lemma%unimportant product_topology_basis:
assumes "\<And>i. openin (T i) (X i)" "finite {i. X i \<noteq> topspace (T i)}"
shows "openin (product_topology T I) (\<Pi>\<^sub>E i\<in>I. X i)"
-unfolding product_topology_def apply (rule topology_generated_by_Basis) using assms by auto
+ unfolding product_topology_def
+ by (rule topology_generated_by_Basis) (use assms in auto)
lemma%important product_topology_open_contains_basis:
- assumes "openin (product_topology T I) U"
- "x \<in> U"
+ assumes "openin (product_topology T I) U" "x \<in> U"
shows "\<exists>X. x \<in> (\<Pi>\<^sub>E i\<in>I. X i) \<and> (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)} \<and> (\<Pi>\<^sub>E i\<in>I. X i) \<subseteq> U"
proof%unimportant -
have "generate_topology_on {(\<Pi>\<^sub>E i\<in>I. X i) |X. (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)}} U"
@@ -375,6 +608,114 @@
qed
+lemma openin_product_topology:
+ "openin (product_topology X I) =
+ arbitrary union_of
+ ((finite intersection_of (\<lambda>F. (\<exists>i U. F = {f. f i \<in> U} \<and> i \<in> I \<and> openin (X i) U)))
+ relative_to topspace (product_topology X I))"
+ apply (subst product_topology)
+ apply (simp add: topspace_product_topology topology_inverse' [OF istopology_subbase])
+ done
+
+lemma subtopology_PiE:
+ "subtopology (product_topology X I) (\<Pi>\<^sub>E i\<in>I. (S i)) = product_topology (\<lambda>i. subtopology (X i) (S i)) I"
+proof -
+ let ?P = "\<lambda>F. \<exists>i U. F = {f. f i \<in> U} \<and> i \<in> I \<and> openin (X i) U"
+ let ?X = "\<Pi>\<^sub>E i\<in>I. topspace (X i)"
+ have "finite intersection_of ?P relative_to ?X \<inter> Pi\<^sub>E I S =
+ finite intersection_of (?P relative_to ?X \<inter> Pi\<^sub>E I S) relative_to ?X \<inter> Pi\<^sub>E I S"
+ by (rule finite_intersection_of_relative_to)
+ also have "\<dots> = finite intersection_of
+ ((\<lambda>F. \<exists>i U. F = {f. f i \<in> U} \<and> i \<in> I \<and> (openin (X i) relative_to S i) U)
+ relative_to ?X \<inter> Pi\<^sub>E I S)
+ relative_to ?X \<inter> Pi\<^sub>E I S"
+ apply (rule arg_cong2 [where f = "(relative_to)"])
+ apply (rule arg_cong [where f = "(intersection_of)finite"])
+ apply (rule ext)
+ apply (auto simp: relative_to_def intersection_of_def)
+ done
+ finally
+ have "finite intersection_of ?P relative_to ?X \<inter> Pi\<^sub>E I S =
+ finite intersection_of
+ (\<lambda>F. \<exists>i U. F = {f. f i \<in> U} \<and> i \<in> I \<and> (openin (X i) relative_to S i) U)
+ relative_to ?X \<inter> Pi\<^sub>E I S"
+ by (metis finite_intersection_of_relative_to)
+ then show ?thesis
+ unfolding topology_eq
+ apply clarify
+ apply (simp add: openin_product_topology flip: openin_relative_to)
+ apply (simp add: arbitrary_union_of_relative_to topspace_product_topology topspace_subtopology flip: PiE_Int)
+ done
+qed
+
+
+lemma product_topology_base_alt:
+ "finite intersection_of (\<lambda>F. (\<exists>i U. F = {f. f i \<in> U} \<and> i \<in> I \<and> openin (X i) U))
+ relative_to topspace(product_topology X I) =
+ (\<lambda>F. (\<exists>U. F = Pi\<^sub>E I U \<and> finite {i \<in> I. U i \<noteq> topspace(X i)} \<and> (\<forall>i \<in> I. openin (X i) (U i))))"
+ (is "?lhs = ?rhs")
+proof -
+ have "(\<forall>F. ?lhs F \<longrightarrow> ?rhs F)"
+ unfolding all_relative_to all_intersection_of topspace_product_topology
+ proof clarify
+ fix \<F>
+ assume "finite \<F>" and "\<F> \<subseteq> {{f. f i \<in> U} |i U. i \<in> I \<and> openin (X i) U}"
+ then show "\<exists>U. (\<Pi>\<^sub>E i\<in>I. topspace (X i)) \<inter> \<Inter>\<F> = Pi\<^sub>E I U \<and>
+ finite {i \<in> I. U i \<noteq> topspace (X i)} \<and> (\<forall>i\<in>I. openin (X i) (U i))"
+ proof (induction)
+ case (insert F \<F>)
+ then obtain U where eq: "(\<Pi>\<^sub>E i\<in>I. topspace (X i)) \<inter> \<Inter>\<F> = Pi\<^sub>E I U"
+ and fin: "finite {i \<in> I. U i \<noteq> topspace (X i)}"
+ and ope: "\<And>i. i \<in> I \<Longrightarrow> openin (X i) (U i)"
+ by auto
+ obtain i V where "F = {f. f i \<in> V}" "i \<in> I" "openin (X i) V"
+ using insert by auto
+ let ?U = "\<lambda>j. U j \<inter> (if j = i then V else topspace(X j))"
+ show ?case
+ proof (intro exI conjI)
+ show "(\<Pi>\<^sub>E i\<in>I. topspace (X i)) \<inter> \<Inter>insert F \<F> = Pi\<^sub>E I ?U"
+ using eq PiE_mem \<open>i \<in> I\<close> by (auto simp: \<open>F = {f. f i \<in> V}\<close>) fastforce
+ next
+ show "finite {i \<in> I. ?U i \<noteq> topspace (X i)}"
+ by (rule rev_finite_subset [OF finite.insertI [OF fin]]) auto
+ next
+ show "\<forall>i\<in>I. openin (X i) (?U i)"
+ by (simp add: \<open>openin (X i) V\<close> ope openin_Int)
+ qed
+ qed (auto intro: dest: not_finite_existsD)
+ qed
+ moreover have "(\<forall>F. ?rhs F \<longrightarrow> ?lhs F)"
+ proof clarify
+ fix U :: "'a \<Rightarrow> 'b set"
+ assume fin: "finite {i \<in> I. U i \<noteq> topspace (X i)}" and ope: "\<forall>i\<in>I. openin (X i) (U i)"
+ let ?U = "\<Inter>i\<in>{i \<in> I. U i \<noteq> topspace (X i)}. {x. x i \<in> U i}"
+ show "?lhs (Pi\<^sub>E I U)"
+ unfolding relative_to_def topspace_product_topology
+ proof (intro exI conjI)
+ show "(finite intersection_of (\<lambda>F. \<exists>i U. F = {f. f i \<in> U} \<and> i \<in> I \<and> openin (X i) U)) ?U"
+ using fin ope by (intro finite_intersection_of_Inter finite_intersection_of_inc) auto
+ show "(\<Pi>\<^sub>E i\<in>I. topspace (X i)) \<inter> ?U = Pi\<^sub>E I U"
+ using ope openin_subset by fastforce
+ qed
+ qed
+ ultimately show ?thesis
+ by meson
+qed
+
+
+lemma topspace_product_topology_alt:
+ "topspace (product_topology Y I) = {f \<in> extensional I. \<forall>k \<in> I. f k \<in> topspace(Y k)}"
+ by (force simp: product_topology PiE_def)
+
+lemma openin_product_topology_alt:
+ "openin (product_topology X I) S \<longleftrightarrow>
+ (\<forall>x \<in> S. \<exists>U. finite {i \<in> I. U i \<noteq> topspace(X i)} \<and>
+ (\<forall>i \<in> I. openin (X i) (U i)) \<and> x \<in> Pi\<^sub>E I U \<and> Pi\<^sub>E I U \<subseteq> S)"
+ apply (simp add: openin_product_topology arbitrary_union_of_alt product_topology_base_alt, auto)
+ apply (drule bspec; blast)
+ done
+
+
text \<open>The basic property of the product topology is the continuity of projections:\<close>
lemma%unimportant continuous_on_topo_product_coordinates [simp]:
@@ -396,7 +737,7 @@
using ** by auto
}
then show ?thesis unfolding continuous_on_topo_def
- by (auto simp add: assms product_topology_topspace PiE_iff)
+ by (auto simp add: assms topspace_product_topology PiE_iff)
qed
lemma%important continuous_on_topo_coordinatewise_then_product [intro]:
@@ -427,7 +768,7 @@
show "f `topspace T1 \<subseteq> \<Union>{Pi\<^sub>E I X |X. (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)}}"
apply (subst topology_generated_by_topspace[symmetric])
apply (subst product_topology_def[symmetric])
- apply (simp only: product_topology_topspace)
+ apply (simp only: topspace_product_topology)
apply (auto simp add: PiE_iff)
using assms unfolding continuous_on_topo_def by auto
qed
@@ -449,7 +790,7 @@
have "f x \<in> topspace (product_topology T I)"
using assms \<open>x \<in> topspace T1\<close> unfolding continuous_on_topo_def by auto
then have "f x \<in> (\<Pi>\<^sub>E i\<in>I. topspace (T i))"
- using product_topology_topspace by metis
+ using topspace_product_topology by metis
then show "f x i = undefined"
using \<open>i \<notin> I\<close> by (auto simp add: PiE_iff extensional_def)
qed
@@ -479,7 +820,7 @@
instance proof%unimportant
have "topspace (product_topology (\<lambda>(i::'a). euclidean::('b topology)) UNIV) = UNIV"
- unfolding product_topology_topspace topspace_euclidean by auto
+ unfolding topspace_product_topology topspace_euclidean by auto
then show "open (UNIV::('a \<Rightarrow> 'b) set)"
unfolding open_fun_def by (metis openin_topspace)
qed (auto simp add: open_fun_def)
@@ -1233,6 +1574,8 @@
by standard
+
+
subsection%important \<open>Measurability\<close> (*FIX ME mv *)
text \<open>There are two natural sigma-algebras on a product space: the borel sigma algebra,
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy Mon Sep 24 14:33:08 2018 +0100
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy Mon Sep 24 14:33:17 2018 +0100
@@ -11,6 +11,7 @@
"HOL-Library.Indicator_Function"
"HOL-Library.Countable_Set"
"HOL-Library.FuncSet"
+ "HOL-Library.Set_Idioms"
Linear_Algebra
Norm_Arith
begin
@@ -817,6 +818,9 @@
unfolding subtopology_def topology_inverse'[OF istopology_subtopology]
by auto
+lemma openin_relative_to: "(openin X relative_to S) = openin (subtopology X S)"
+ by (force simp: relative_to_def openin_subtopology)
+
lemma topspace_subtopology: "topspace (subtopology U V) = topspace U \<inter> V"
by (auto simp: topspace_def openin_subtopology)
--- a/src/HOL/Data_Structures/Sorting.thy Mon Sep 24 14:33:08 2018 +0100
+++ b/src/HOL/Data_Structures/Sorting.thy Mon Sep 24 14:33:17 2018 +0100
@@ -270,7 +270,7 @@
subsubsection "Functional Correctness"
lemma mset_merge_adj:
- "\<Union># image_mset mset (mset (merge_adj xss)) = \<Union># image_mset mset (mset xss)"
+ "\<Union># (image_mset mset (mset (merge_adj xss))) = \<Union># (image_mset mset (mset xss))"
by(induction xss rule: merge_adj.induct) (auto simp: mset_merge)
lemma mset_merge_all:
--- a/src/HOL/Data_Structures/Tree234_Map.thy Mon Sep 24 14:33:08 2018 +0100
+++ b/src/HOL/Data_Structures/Tree234_Map.thy Mon Sep 24 14:33:17 2018 +0100
@@ -66,7 +66,7 @@
GT \<Rightarrow> (case cmp x (fst ab3) of
LT \<Rightarrow> (case upd x y t3 of
T\<^sub>i t3' \<Rightarrow> T\<^sub>i (Node4 t1 ab1 t2 ab2 t3' ab3 t4)
- | Up\<^sub>i t31 q t32 => Up\<^sub>i (Node2 t1 ab1 t2) ab2(*q*) (Node3 t31 q t32 ab3 t4)) |
+ | Up\<^sub>i t31 q t32 => Up\<^sub>i (Node2 t1 ab1 t2) ab2\<^cancel>\<open>q\<close> (Node3 t31 q t32 ab3 t4)) |
EQ \<Rightarrow> T\<^sub>i (Node4 t1 ab1 t2 ab2 t3 (x,y) t4) |
GT \<Rightarrow> (case upd x y t4 of
T\<^sub>i t4' => T\<^sub>i (Node4 t1 ab1 t2 ab2 t3 ab3 t4')
--- a/src/HOL/GCD.thy Mon Sep 24 14:33:08 2018 +0100
+++ b/src/HOL/GCD.thy Mon Sep 24 14:33:17 2018 +0100
@@ -1092,14 +1092,14 @@
sublocale Gcd_fin: bounded_quasi_semilattice_set gcd 0 1 normalize
defines
- Gcd_fin ("Gcd\<^sub>f\<^sub>i\<^sub>n _" [900] 900) = "Gcd_fin.F :: 'a set \<Rightarrow> 'a" ..
+ Gcd_fin ("Gcd\<^sub>f\<^sub>i\<^sub>n") = "Gcd_fin.F :: 'a set \<Rightarrow> 'a" ..
abbreviation gcd_list :: "'a list \<Rightarrow> 'a"
where "gcd_list xs \<equiv> Gcd\<^sub>f\<^sub>i\<^sub>n (set xs)"
sublocale Lcm_fin: bounded_quasi_semilattice_set lcm 1 0 normalize
defines
- Lcm_fin ("Lcm\<^sub>f\<^sub>i\<^sub>n _" [900] 900) = Lcm_fin.F ..
+ Lcm_fin ("Lcm\<^sub>f\<^sub>i\<^sub>n") = Lcm_fin.F ..
abbreviation lcm_list :: "'a list \<Rightarrow> 'a"
where "lcm_list xs \<equiv> Lcm\<^sub>f\<^sub>i\<^sub>n (set xs)"
--- a/src/HOL/Library/Complete_Partial_Order2.thy Mon Sep 24 14:33:08 2018 +0100
+++ b/src/HOL/Library/Complete_Partial_Order2.thy Mon Sep 24 14:33:17 2018 +0100
@@ -161,7 +161,7 @@
end
lemma Sup_image_mono_le:
- fixes le_b (infix "\<sqsubseteq>" 60) and Sup_b ("\<Or> _" [900] 900)
+ fixes le_b (infix "\<sqsubseteq>" 60) and Sup_b ("\<Or>")
assumes ccpo: "class.ccpo Sup_b (\<sqsubseteq>) lt_b"
assumes chain: "Complete_Partial_Order.chain (\<sqsubseteq>) Y"
and mono: "\<And>x y. \<lbrakk> x \<sqsubseteq> y; x \<in> Y \<rbrakk> \<Longrightarrow> f x \<le> f y"
@@ -556,7 +556,7 @@
context
fixes ord :: "'b \<Rightarrow> 'b \<Rightarrow> bool" (infix "\<sqsubseteq>" 60)
- and lub :: "'b set \<Rightarrow> 'b" ("\<Or> _" [900] 900)
+ and lub :: "'b set \<Rightarrow> 'b" ("\<Or>")
begin
lemma cont_fun_lub_Sup:
@@ -677,7 +677,7 @@
by(rule monotoneI)(auto intro: bot intro: mono order_trans)
lemma (in ccpo) mcont_if_bot:
- fixes bot and lub ("\<Or> _" [900] 900) and ord (infix "\<sqsubseteq>" 60)
+ fixes bot and lub ("\<Or>") and ord (infix "\<sqsubseteq>" 60)
assumes ccpo: "class.ccpo lub (\<sqsubseteq>) lt"
and mono: "\<And>x y. \<lbrakk> x \<le> y; \<not> x \<le> bound \<rbrakk> \<Longrightarrow> f x \<sqsubseteq> f y"
and cont: "\<And>Y. \<lbrakk> Complete_Partial_Order.chain (\<le>) Y; Y \<noteq> {}; \<And>x. x \<in> Y \<Longrightarrow> \<not> x \<le> bound \<rbrakk> \<Longrightarrow> f (\<Squnion>Y) = \<Or>(f ` Y)"
@@ -877,7 +877,7 @@
end
lemma admissible_leI:
- fixes ord (infix "\<sqsubseteq>" 60) and lub ("\<Or> _" [900] 900)
+ fixes ord (infix "\<sqsubseteq>" 60) and lub ("\<Or>")
assumes "class.ccpo lub (\<sqsubseteq>) (mk_less (\<sqsubseteq>))"
and "mcont luba orda lub (\<sqsubseteq>) (\<lambda>x. f x)"
and "mcont luba orda lub (\<sqsubseteq>) (\<lambda>x. g x)"
--- a/src/HOL/Library/Multiset.thy Mon Sep 24 14:33:08 2018 +0100
+++ b/src/HOL/Library/Multiset.thy Mon Sep 24 14:33:17 2018 +0100
@@ -2385,7 +2385,7 @@
shows \<open>(\<Sum>x\<in>#A. y) = of_nat (size A) * y\<close>
by (induction A) (auto simp: algebra_simps)
-abbreviation Union_mset :: "'a multiset multiset \<Rightarrow> 'a multiset" ("\<Union># _" [900] 900)
+abbreviation Union_mset :: "'a multiset multiset \<Rightarrow> 'a multiset" ("\<Union>#")
where "\<Union># MM \<equiv> sum_mset MM" \<comment> \<open>FIXME ambiguous notation --
could likewise refer to \<open>\<Squnion>#\<close>\<close>
--- a/src/HOL/Mirabelle/ex/Ex.thy Mon Sep 24 14:33:08 2018 +0100
+++ b/src/HOL/Mirabelle/ex/Ex.thy Mon Sep 24 14:33:17 2018 +0100
@@ -3,7 +3,7 @@
ML \<open>
val rc = Isabelle_System.bash
- "cd \"$ISABELLE_HOME/src/HOL/Analysis\"; isabelle mirabelle arith Inner_Product.thy";
+ "cd \"$ISABELLE_HOME/src/HOL/Analysis\"; if isabelle build -n \"$MIRABELLE_LOGIC\"; then isabelle mirabelle arith Inner_Product.thy; fi";
if rc <> 0 then error ("Mirabelle example failed: " ^ string_of_int rc)
else ();
\<close> \<comment> \<open>some arbitrary small test case\<close>
--- a/src/Pure/Isar/locale.ML Mon Sep 24 14:33:08 2018 +0100
+++ b/src/Pure/Isar/locale.ML Mon Sep 24 14:33:17 2018 +0100
@@ -56,13 +56,6 @@
val specification_of: theory -> string -> term option * term list
val hyp_spec_of: theory -> string -> Element.context_i list
- type content =
- {type_params: (string * sort) list,
- params: ((string * typ) * mixfix) list,
- asm: term option,
- defs: term list}
- val dest_locales: theory -> (string * content) list
-
(* Storing results *)
val add_facts: string -> string -> Attrib.fact list -> Proof.context -> Proof.context
val add_declaration: string -> bool -> declaration -> Proof.context -> Proof.context
@@ -93,6 +86,7 @@
val add_dependency: string -> registration -> theory -> theory
(* Diagnostic *)
+ val get_locales: theory -> string list
val print_locales: bool -> theory -> unit
val print_locale: theory -> bool -> xstring * Position.T -> unit
val print_registrations: Proof.context -> xstring * Position.T -> unit
@@ -215,19 +209,6 @@
Locales.map o Name_Space.map_table_entry name o map_locale o apsnd;
-(* content *)
-
-type content =
- {type_params: (string * sort) list,
- params: ((string * typ) * mixfix) list,
- asm: term option,
- defs: term list};
-
-fun dest_locales thy =
- (Locales.get thy, []) |-> Name_Space.fold_table
- (fn (name, Loc {parameters = (type_params, params), spec = (asm, defs), ...}) =>
- cons (name, {type_params = type_params, params = params, asm = asm, defs = defs}));
-
(** Primitive operations **)
@@ -715,6 +696,8 @@
(*** diagnostic commands and interfaces ***)
+fun get_locales thy = map #1 (Name_Space.dest_table (Locales.get thy));
+
fun print_locales verbose thy =
Pretty.block
(Pretty.breaks
--- a/src/Pure/Isar/proof.ML Mon Sep 24 14:33:08 2018 +0100
+++ b/src/Pure/Isar/proof.ML Mon Sep 24 14:33:17 2018 +0100
@@ -415,24 +415,11 @@
local
-fun goalN i = "goal" ^ string_of_int i;
-fun goals st = map goalN (1 upto Thm.nprems_of st);
-
-fun no_goal_cases st = map (rpair NONE) (goals st);
-
-fun goal_cases ctxt st =
- Rule_Cases.make_common ctxt (Thm.prop_of st) (map (rpair [] o rpair []) (goals st));
-
fun apply_method text ctxt state =
find_goal state |> (fn (goal_ctxt, {statement, using, goal, before_qed, after_qed}) =>
Method.evaluate text ctxt using (goal_ctxt, goal)
|> Seq.map_result (fn (goal_ctxt', goal') =>
- let
- val goal_ctxt'' = goal_ctxt'
- |> Proof_Context.update_cases_legacy (no_goal_cases goal @ goal_cases ctxt goal');
- val state' = state
- |> map_goal (K (goal_ctxt'', statement, using, goal', before_qed, after_qed));
- in state' end));
+ state |> map_goal (K (goal_ctxt', statement, using, goal', before_qed, after_qed))));
in
--- a/src/Pure/Isar/proof_context.ML Mon Sep 24 14:33:08 2018 +0100
+++ b/src/Pure/Isar/proof_context.ML Mon Sep 24 14:33:17 2018 +0100
@@ -151,9 +151,8 @@
val add_assms_cmd: Assumption.export ->
(Thm.binding * (string * string list) list) list ->
Proof.context -> (string * thm list) list * Proof.context
- val dest_cases: Proof.context option -> Proof.context -> (string * (Rule_Cases.T * {legacy: bool})) list
+ val dest_cases: Proof.context option -> Proof.context -> (string * Rule_Cases.T) list
val update_cases: (string * Rule_Cases.T option) list -> Proof.context -> Proof.context
- val update_cases_legacy: (string * Rule_Cases.T option) list -> Proof.context -> Proof.context
val apply_case: Rule_Cases.T -> Proof.context -> (string * term list) list * Proof.context
val check_case: Proof.context -> bool ->
string * Position.T -> binding option list -> Rule_Cases.T
@@ -228,7 +227,7 @@
(** Isar proof context information **)
-type cases = (Rule_Cases.T * {legacy: bool}) Name_Space.table;
+type cases = Rule_Cases.T Name_Space.table;
val empty_cases: cases = Name_Space.empty_table Markup.caseN;
datatype data =
@@ -238,7 +237,7 @@
tsig: Type.tsig * Type.tsig, (*local/global type signature -- local name space / defsort only*)
consts: Consts.T * Consts.T, (*local/global consts -- local name space / abbrevs only*)
facts: Facts.T, (*local facts, based on initial global facts*)
- cases: cases}; (*named case contexts: case, legacy, running index*)
+ cases: cases}; (*named case contexts*)
fun make_data (mode, syntax, tsig, consts, facts, cases) =
Data {mode = mode, syntax = syntax, tsig = tsig, consts = consts, facts = facts, cases = cases};
@@ -1319,17 +1318,10 @@
fun drop_schematic (b as (xi, SOME t)) = if Term.exists_subterm is_Var t then (xi, NONE) else b
| drop_schematic b = b;
-fun update_case _ _ ("", _) cases = cases
- | update_case _ _ (name, NONE) cases = Name_Space.del_table name cases
- | update_case context legacy (name, SOME c) cases =
- let
- val binding = Binding.name name |> legacy ? Binding.concealed;
- val (_, cases') = Name_Space.define context false (binding, (c, {legacy = legacy})) cases;
- in cases' end;
-
-fun update_cases' legacy args ctxt =
- let val context = Context.Proof ctxt |> Name_Space.map_naming (K Name_Space.global_naming);
- in map_cases (fold (update_case context legacy) args) ctxt end;
+fun update_case _ ("", _) cases = cases
+ | update_case _ (name, NONE) cases = Name_Space.del_table name cases
+ | update_case context (name, SOME c) cases =
+ #2 (Name_Space.define context false (Binding.name name, c) cases);
fun fix (b, T) ctxt =
let val ([x], ctxt') = add_fixes [(b, SOME T, NoSyn)] ctxt
@@ -1337,8 +1329,9 @@
in
-val update_cases = update_cases' false;
-val update_cases_legacy = update_cases' true;
+fun update_cases args ctxt =
+ let val context = Context.Proof ctxt |> Name_Space.map_naming (K Name_Space.global_naming);
+ in map_cases (fold (update_case context) args) ctxt end;
fun case_result c ctxt =
let
@@ -1356,13 +1349,8 @@
fun check_case ctxt internal (name, pos) param_specs =
let
- val (_, (Rule_Cases.Case {fixes, assumes, binds, cases}, {legacy})) =
+ val (_, Rule_Cases.Case {fixes, assumes, binds, cases}) =
Name_Space.check (Context.Proof ctxt) (cases_of ctxt) (name, pos);
- val _ =
- if legacy then
- legacy_feature ("Bad case " ^ quote name ^ Position.here pos ^
- " -- use proof method \"goal_cases\" instead")
- else ();
val _ = List.app (fn NONE => () | SOME b => ignore (check_var internal b)) param_specs;
fun replace (opt_x :: xs) ((y, T) :: ys) = (the_default y opt_x, T) :: replace xs ys
@@ -1537,10 +1525,9 @@
fun pretty_cases ctxt =
let
- fun mk_case (_, (_, {legacy = true})) = NONE
- | mk_case (name, (c as Rule_Cases.Case {fixes, ...}, {legacy = false})) =
- SOME (name, (fixes, case_result c ctxt));
- val cases = dest_cases NONE ctxt |> map_filter mk_case;
+ val cases =
+ dest_cases NONE ctxt |> map (fn (name, c as Rule_Cases.Case {fixes, ...}) =>
+ (name, (fixes, case_result c ctxt)));
in
if null cases then []
else [Pretty.big_list "cases:" (map pretty_case cases)]
@@ -1563,20 +1550,18 @@
fun is_case x t =
x = Rule_Cases.case_conclN andalso not (Term.exists_subterm Term.is_Var t);
- fun print_proof (name, (Rule_Cases.Case {fixes, binds, ...}, {legacy})) =
- if legacy then NONE
- else
- let
- val concl =
- if exists (fn ((x, _), SOME t) => is_case x t | _ => false) binds
- then Rule_Cases.case_conclN else Auto_Bind.thesisN;
- in
- SOME (cat_lines
- [" case " ^ print_case name (map (Binding.name_of o #1) fixes),
- " then show ?" ^ concl ^ " sorry"])
- end;
+ fun print_proof (name, Rule_Cases.Case {fixes, binds, ...}) =
+ let
+ val concl =
+ if exists (fn ((x, _), SOME t) => is_case x t | _ => false) binds
+ then Rule_Cases.case_conclN else Auto_Bind.thesisN;
+ in
+ cat_lines
+ [" case " ^ print_case name (map (Binding.name_of o #1) fixes),
+ " then show ?" ^ concl ^ " sorry"]
+ end;
in
- (case map_filter print_proof (dest_cases (SOME ctxt0) ctxt) of
+ (case map print_proof (dest_cases (SOME ctxt0) ctxt) of
[] => ""
| proofs =>
"Proof outline with cases:\n" ^
--- a/src/Pure/PIDE/headless.scala Mon Sep 24 14:33:08 2018 +0100
+++ b/src/Pure/PIDE/headless.scala Mon Sep 24 14:33:17 2018 +0100
@@ -71,6 +71,12 @@
val nodes: List[(Document.Node.Name, Document_Status.Node_Status)],
val nodes_committed: List[(Document.Node.Name, Document_Status.Node_Status)])
{
+ def nodes_pending: List[(Document.Node.Name, Document_Status.Node_Status)] =
+ {
+ val committed = nodes_committed.iterator.map(_._1).toSet
+ nodes.filter(p => !committed(p._1))
+ }
+
def snapshot(name: Document.Node.Name): Document.Snapshot =
stable_snapshot(state, version, name)
@@ -136,31 +142,29 @@
commit: Option[(Document.Snapshot, Document_Status.Node_Status) => Unit])
: Use_Theories_State =
{
- val st1 =
+ val already_committed1 =
if (commit.isDefined) {
- val already_committed1 =
- (already_committed /: dep_theories)({ case (committed, name) =>
- def parents_committed: Boolean =
- version.nodes(name).header.imports.forall({ case (parent, _) =>
- Sessions.is_pure(parent.theory) || committed.isDefinedAt(parent)
- })
- if (!committed.isDefinedAt(name) && parents_committed &&
- state.node_consolidated(version, name))
- {
- val snapshot = stable_snapshot(state, version, name)
- val status = Document_Status.Node_Status.make(state, version, name)
- commit.get.apply(snapshot, status)
- committed + (name -> status)
- }
- else committed
- })
- copy(already_committed = already_committed1)
+ (already_committed /: dep_theories)({ case (committed, name) =>
+ def parents_committed: Boolean =
+ version.nodes(name).header.imports.forall({ case (parent, _) =>
+ Sessions.is_pure(parent.theory) || committed.isDefinedAt(parent)
+ })
+ if (!committed.isDefinedAt(name) && parents_committed &&
+ state.node_consolidated(version, name))
+ {
+ val snapshot = stable_snapshot(state, version, name)
+ val status = Document_Status.Node_Status.make(state, version, name)
+ commit.get.apply(snapshot, status)
+ committed + (name -> status)
+ }
+ else committed
+ })
}
- else this
+ else already_committed
if (beyond_limit || watchdog(watchdog_timeout) ||
dep_theories.forall(name =>
- already_committed.isDefinedAt(name) ||
+ already_committed1.isDefinedAt(name) ||
state.node_consolidated(version, name) ||
nodes_status.quasi_consolidated(name)))
{
@@ -170,14 +174,14 @@
val nodes_committed =
for {
name <- dep_theories
- status <- already_committed.get(name)
+ status <- already_committed1.get(name)
} yield (name -> status)
try { result.fulfill(new Use_Theories_Result(state, version, nodes, nodes_committed)) }
catch { case _: IllegalStateException => }
}
- st1
+ copy(already_committed = already_committed1)
}
}
--- a/src/Pure/Syntax/lexicon.ML Mon Sep 24 14:33:08 2018 +0100
+++ b/src/Pure/Syntax/lexicon.ML Mon Sep 24 14:33:17 2018 +0100
@@ -22,7 +22,7 @@
val is_tid: string -> bool
datatype token_kind =
Literal | Ident | Long_Ident | Var | Type_Ident | Type_Var | Num | Float | Str |
- String | Cartouche | Space | Comment of Comment.kind option | Dummy | EOF
+ String | Cartouche | Space | Comment of Comment.kind | Dummy | EOF
eqtype token
val kind_of_token: token -> token_kind
val str_of_token: token -> string
@@ -120,13 +120,13 @@
datatype token_kind =
Literal | Ident | Long_Ident | Var | Type_Ident | Type_Var | Num | Float | Str |
- String | Cartouche | Space | Comment of Comment.kind option | Dummy | EOF;
+ String | Cartouche | Space | Comment of Comment.kind | Dummy | EOF;
val token_kinds =
Vector.fromList
[Literal, Ident, Long_Ident, Var, Type_Ident, Type_Var, Num, Float, Str,
- String, Cartouche, Space, Comment NONE, Comment (SOME Comment.Comment),
- Comment (SOME Comment.Cancel), Comment (SOME Comment.Latex), Dummy, EOF];
+ String, Cartouche, Space, Comment Comment.Comment, Comment Comment.Cancel,
+ Comment Comment.Latex, Dummy, EOF];
fun token_kind i = Vector.sub (token_kinds, i);
fun token_kind_index k = #1 (the (Vector.findi (fn (_, k') => k = k') token_kinds));
@@ -301,8 +301,7 @@
val scan =
Symbol_Pos.scan_cartouche err_prefix >> token Cartouche ||
- Symbol_Pos.scan_comment err_prefix >> token (Comment NONE) ||
- Comment.scan >> (fn (kind, ss) => token (Comment (SOME kind)) ss) ||
+ Comment.scan >> (fn (kind, ss) => token (Comment kind) ss) ||
Scan.max token_leq scan_lit scan_val ||
scan_string >> token String ||
scan_str >> token Str ||
--- a/src/Pure/Syntax/syntax_phases.ML Mon Sep 24 14:33:08 2018 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML Mon Sep 24 14:33:17 2018 +0100
@@ -341,12 +341,6 @@
val toks = Syntax.tokenize syn raw syms;
val _ = Context_Position.reports ctxt (map Lexicon.report_of_token toks);
- val _ = toks |> List.app (fn tok =>
- (case Lexicon.kind_of_token tok of
- Lexicon.Comment NONE =>
- legacy_feature ("Old-style inner comment: use \"\<comment> \<open>...\<close>\" or \"\<^cancel>\<open>...\<close>\" instead" ^
- Position.here (Lexicon.pos_of_token tok))
- | _ => ()));
val pts = Syntax.parse syn root (filter Lexicon.is_proper toks)
handle ERROR msg =>
--- a/src/Pure/Thy/export_theory.ML Mon Sep 24 14:33:08 2018 +0100
+++ b/src/Pure/Thy/export_theory.ML Mon Sep 24 14:33:17 2018 +0100
@@ -70,23 +70,29 @@
(fold_types o fold_atyps) (fn TFree (a, S) => is_free used a ? insert (op =) (a, S) | _ => I);
-(* locale support *)
+(* locale content *)
-fun locale_axioms thy loc =
+fun locale_content thy loc =
let
- val (intro1, intro2) = Locale.intros_of thy loc;
- fun intros_tac ctxt = Method.try_intros_tac ctxt (the_list intro1 @ the_list intro2);
- val res =
- Proof_Context.init_global thy
- |> Interpretation.interpretation ([(loc, (("", false), (Expression.Named [], [])))], [])
- |> Proof.refine (Method.Basic (METHOD o intros_tac))
- |> Seq.filter_results
- |> try Seq.hd;
- in
- (case res of
- SOME st => Thm.prems_of (#goal (Proof.goal st))
- | NONE => raise Fail ("Cannot unfold locale " ^ quote loc))
- end;
+ val args = map #1 (Locale.params_of thy loc);
+ val axioms =
+ let
+ val (intro1, intro2) = Locale.intros_of thy loc;
+ fun intros_tac ctxt = Method.try_intros_tac ctxt (the_list intro1 @ the_list intro2);
+ val inst = Expression.Named (args |> map (fn (x, T) => (x, Free (x, T))));
+ val res =
+ Proof_Context.init_global thy
+ |> Interpretation.interpretation ([(loc, (("", false), (inst, [])))], [])
+ |> Proof.refine (Method.Basic (METHOD o intros_tac))
+ |> Seq.filter_results
+ |> try Seq.hd;
+ in
+ (case res of
+ SOME st => Thm.prems_of (#goal (Proof.goal st))
+ | NONE => raise Fail ("Cannot unfold locale " ^ quote loc))
+ end;
+ val typargs = rev (fold Term.add_tfrees (map Free args @ axioms) []);
+ in {typargs = typargs, args = args, axioms = axioms} end;
(* general setup *)
@@ -272,17 +278,19 @@
let open XML.Encode Term_XML.Encode
in triple (list (pair string sort)) (list (pair string typ)) (list (encode_axiom used)) end;
- fun export_locale loc ({type_params, params, ...}: Locale.content) =
+ fun export_locale loc =
let
- val axioms = locale_axioms thy loc;
- val args = map #1 params;
- val typargs = rev (fold Term.add_tfrees (map Free args @ axioms) (rev type_params));
+ val {typargs, args, axioms} = locale_content thy loc;
val used = fold Name.declare (map #1 typargs @ map #1 args) Name.context;
- in encode_locale used (typargs, args, axioms) end;
+ in encode_locale used (typargs, args, axioms) end
+ handle ERROR msg =>
+ cat_error msg ("The error(s) above occurred in locale " ^
+ quote (Locale.markup_name thy_ctxt loc));
val _ =
- export_entities "locales" (SOME oo export_locale) Locale.locale_space
- (Locale.dest_locales thy);
+ export_entities "locales" (fn loc => fn () => SOME (export_locale loc))
+ Locale.locale_space
+ (map (rpair ()) (Locale.get_locales thy));
(* parents *)
--- a/src/Pure/Thy/present.scala Mon Sep 24 14:33:08 2018 +0100
+++ b/src/Pure/Thy/present.scala Mon Sep 24 14:33:17 2018 +0100
@@ -319,6 +319,6 @@
build_document(document_dir = document_dir, document_name = document_name,
document_format = document_format, tags = tags)
}
- catch { case ERROR(msg) => Output.writeln(msg); sys.exit(1) }
+ catch { case ERROR(msg) => Output.writeln(msg); sys.exit(2) }
})
}
--- a/src/Pure/Thy/sessions.scala Mon Sep 24 14:33:08 2018 +0100
+++ b/src/Pure/Thy/sessions.scala Mon Sep 24 14:33:17 2018 +0100
@@ -196,21 +196,31 @@
def imported_sources(name: String): List[SHA1.Digest] =
session_bases(name).imported_sources.map(_._2)
- def used_theories_condition(warning: String => Unit = _ => ()): List[Document.Node.Name] =
+ def used_theories_condition(default_options: Options, warning: String => Unit = _ => ())
+ : List[(Options, Document.Node.Name)] =
+ {
+ val default_skip_proofs = default_options.bool("skip_proofs")
for {
session_name <- sessions_structure.build_topological_order
(options, name) <- session_bases(session_name).used_theories
if {
+ def warn(msg: String): Unit = warning("Skipping theory " + name + " (" + msg + ")")
+
val conditions =
space_explode(',', options.string("condition")).
filter(cond => Isabelle_System.getenv(cond) == "")
- if (conditions.isEmpty) true
- else {
- warning("Skipping theory " + name + " (condition " + conditions.mkString(" ") + ")")
+ if (conditions.nonEmpty) {
+ warn("condition " + conditions.mkString(" "))
false
}
+ else if (default_skip_proofs && !options.bool("skip_proofs")) {
+ warn("option skip_proofs")
+ false
+ }
+ else true
}
- } yield name
+ } yield (options, name)
+ }
def sources(name: String): List[SHA1.Digest] =
session_bases(name).sources.map(_._2)
--- a/src/Pure/Tools/dump.scala Mon Sep 24 14:33:08 2018 +0100
+++ b/src/Pure/Tools/dump.scala Mon Sep 24 14:33:17 2018 +0100
@@ -95,7 +95,7 @@
commit_cleanup_delay: Time = Headless.default_commit_cleanup_delay,
watchdog_timeout: Time = Headless.default_watchdog_timeout,
system_mode: Boolean = false,
- selection: Sessions.Selection = Sessions.Selection.empty): Process_Result =
+ selection: Sessions.Selection = Sessions.Selection.empty): Boolean =
{
if (Build.build_logic(options, logic, build_heap = true, progress = progress,
dirs = dirs ::: select_dirs, system_mode = system_mode) != 0) error(logic + " FAILED")
@@ -112,7 +112,9 @@
val include_sessions =
deps.sessions_structure.imports_topological_order
- val use_theories = deps.used_theories_condition(progress.echo_warning).map(_.theory)
+ val use_theories =
+ for { (_, name) <- deps.used_theories_condition(dump_options, progress.echo_warning) }
+ yield name.theory
/* dump aspects asynchronously */
@@ -165,12 +167,16 @@
commit_cleanup_delay = commit_cleanup_delay,
watchdog_timeout = watchdog_timeout)
- val session_result = session.stop()
+ session.stop()
val consumer_ok = Consumer.shutdown()
- if (use_theories_result.ok && consumer_ok) session_result
- else session_result.error_rc
+ use_theories_result.nodes_pending match {
+ case Nil =>
+ case pending => error("Pending theories " + commas_quote(pending.map(p => p._1.toString)))
+ }
+
+ use_theories_result.ok && consumer_ok
}
@@ -243,7 +249,7 @@
val progress = new Console_Progress(verbose = verbose)
- val result =
+ val ok =
progress.interrupt_handler {
dump(options, logic,
aspects = aspects,
@@ -264,8 +270,6 @@
sessions = sessions))
}
- progress.echo(result.timing.message_resources)
-
- sys.exit(result.rc)
+ if (!ok) sys.exit(2)
})
}
--- a/src/Pure/Tools/server.scala Mon Sep 24 14:33:08 2018 +0100
+++ b/src/Pure/Tools/server.scala Mon Sep 24 14:33:17 2018 +0100
@@ -485,7 +485,7 @@
}
else if (operation_exit) {
val ok = Server.exit(name)
- sys.exit(if (ok) 0 else 1)
+ sys.exit(if (ok) 0 else 2)
}
else {
val log = Logger.make(log_file)
--- a/src/Tools/VSCode/src/server.scala Mon Sep 24 14:33:08 2018 +0100
+++ b/src/Tools/VSCode/src/server.scala Mon Sep 24 14:33:17 2018 +0100
@@ -361,7 +361,7 @@
def exit() {
log("\n")
- sys.exit(if (session_.value.isDefined) 1 else 0)
+ sys.exit(if (session_.value.isDefined) 2 else 0)
}