--- a/CONTRIBUTORS Sun Nov 15 22:04:16 2020 +0100
+++ b/CONTRIBUTORS Sun Nov 15 22:26:13 2020 +0100
@@ -6,6 +6,9 @@
Contributions to this Isabelle version
--------------------------------------
+* November 2020: Florian Haftmann
+ Bundle mixins for locale and class expressions.
+
* October 2020: Jasmin Blanchette, Martin Desharnais, Mathias Fleury
Use veriT in proof preplay in Sledgehammer.
@@ -15,6 +18,10 @@
* October 2020: Jasmin Blanchette, Martin Desharnais
Integration of E 2.5 for Sledgehammer.
+* September 2020: Florian Haftmann
+ Substantial reworking and modularization of Word library, with
+ generic type conversions.
+
* August 2020: Makarius Wenzel
Improved monitoring of runtime statistics: ML GC progress and Java.
@@ -24,6 +31,10 @@
* June 2020: Makarius Wenzel
Batch-builds via "isabelle build" allow to invoke Scala from ML.
+* June 2020: Florian Haftmann
+ Simproc defined_all for more aggressive substitution with variables
+ from assumptions.
+
* May 2020: Makarius Wenzel
Antiquotations for Isabelle systems programming, notably @{scala_function}
and @{scala} to invoke Scala from ML.
@@ -31,14 +42,6 @@
* May 2020: Florian Haftmann
Generic algebraically founded bit operations NOT, AND, OR, XOR.
-* Sept. 2020: Florian Haftmann
- Substantial reworking and modularization of Word library, with
- generic type conversions.
-
-* June 2020: Florian Haftmann
- Simproc defined_all for more aggressive substitution with variables
- from assumptions.
-
Contributions to Isabelle2020
-----------------------------
--- a/NEWS Sun Nov 15 22:04:16 2020 +0100
+++ b/NEWS Sun Nov 15 22:26:13 2020 +0100
@@ -179,6 +179,9 @@
* Syntax for state monad combinators fcomp and scomp is organized in
bundle state_combinator_syntax. Minor INCOMPATIBILITY.
+* Syntax for reflected term syntax is organized in bundle term_syntax,
+discontinuing previous locale term_syntax. Minor INCOMPATIBILITY.
+
*** FOL ***
--- a/src/HOL/Analysis/Abstract_Topology.thy Sun Nov 15 22:04:16 2020 +0100
+++ b/src/HOL/Analysis/Abstract_Topology.thy Sun Nov 15 22:26:13 2020 +0100
@@ -56,7 +56,7 @@
"\<And>K. (\<forall>S \<in> K. openin U S) \<Longrightarrow> openin U (\<Union>K)"
using openin[of U] unfolding istopology_def by auto
-lemma openin_subset[intro]: "openin U S \<Longrightarrow> S \<subseteq> topspace U"
+lemma openin_subset: "openin U S \<Longrightarrow> S \<subseteq> topspace U"
unfolding topspace_def by blast
lemma openin_empty[simp]: "openin U {}"
@@ -147,24 +147,17 @@
lemma closedin_INT[intro]:
assumes "A \<noteq> {}" "\<And>x. x \<in> A \<Longrightarrow> closedin U (B x)"
shows "closedin U (\<Inter>x\<in>A. B x)"
- apply (rule closedin_Inter)
- using assms
- apply auto
- done
+ using assms by blast
lemma closedin_Int[intro]: "closedin U S \<Longrightarrow> closedin U T \<Longrightarrow> closedin U (S \<inter> T)"
using closedin_Inter[of "{S,T}" U] by auto
lemma openin_closedin_eq: "openin U S \<longleftrightarrow> S \<subseteq> topspace U \<and> closedin U (topspace U - S)"
- apply (auto simp: closedin_def Diff_Diff_Int inf_absorb2)
- apply (metis openin_subset subset_eq)
- done
+ by (metis Diff_subset closedin_def double_diff equalityD1 openin_subset)
lemma topology_finer_closedin:
"topspace X = topspace Y \<Longrightarrow> (\<forall>S. openin Y S \<longrightarrow> openin X S) \<longleftrightarrow> (\<forall>S. closedin Y S \<longrightarrow> closedin X S)"
- apply safe
- apply (simp add: closedin_def)
- by (simp add: openin_closedin_eq)
+ by (metis closedin_def openin_closedin_eq)
lemma openin_closedin: "S \<subseteq> topspace U \<Longrightarrow> (openin U S \<longleftrightarrow> closedin U (topspace U - S))"
by (simp add: openin_closedin_eq)
@@ -425,10 +418,7 @@
where "top_of_set \<equiv> subtopology (topology open)"
lemma open_openin: "open S \<longleftrightarrow> openin euclidean S"
- apply (rule cong[where x=S and y=S])
- apply (rule topology_inverse[symmetric])
- apply (auto simp: istopology_def)
- done
+ by (simp add: istopology_open topology_inverse')
declare open_openin [symmetric, simp]
@@ -510,8 +500,7 @@
unfolding T_def
apply clarsimp
apply (rule_tac x="d - dist x a" in exI)
- apply (clarsimp simp add: less_diff_eq)
- by (metis dist_commute dist_triangle_lt)
+ by (metis add_0_left dist_commute dist_triangle_lt less_diff_eq)
assume ?rhs then have 2: "S = U \<inter> T"
unfolding T_def
by auto (metis dist_self)
@@ -532,8 +521,8 @@
openin (top_of_set S) E2 \<and>
E1 \<union> E2 = S \<and> E1 \<inter> E2 = {} \<and>
E1 \<noteq> {} \<and> E2 \<noteq> {})"
- apply (simp add: connected_openin, safe, blast)
- by (metis Int_lower1 Un_subset_iff openin_open subset_antisym)
+ unfolding connected_openin
+ by (metis (no_types, lifting) Un_subset_iff openin_imp_subset subset_antisym)
lemma connected_closedin:
"connected S \<longleftrightarrow>
@@ -572,8 +561,8 @@
closedin (top_of_set S) E2 \<and>
E1 \<union> E2 = S \<and> E1 \<inter> E2 = {} \<and>
E1 \<noteq> {} \<and> E2 \<noteq> {})"
- apply (simp add: connected_closedin, safe, blast)
- by (metis Int_lower1 Un_subset_iff closedin_closed subset_antisym)
+ unfolding connected_closedin
+ by (metis Un_subset_iff closedin_imp_subset subset_antisym)
text \<open>These "transitivity" results are handy too\<close>
@@ -639,8 +628,7 @@
"X derived_set_of (S \<union> T) = X derived_set_of S \<union> X derived_set_of T" (is "?lhs = ?rhs")
proof
show "?lhs \<subseteq> ?rhs"
- apply (clarsimp simp: in_derived_set_of)
- by (metis IntE IntI openin_Int)
+ by (clarsimp simp: in_derived_set_of) (metis IntE IntI openin_Int)
show "?rhs \<subseteq> ?lhs"
by (simp add: derived_set_of_mono)
qed
@@ -654,9 +642,13 @@
qed auto
lemma derived_set_of_topspace:
- "X derived_set_of (topspace X) = {x \<in> topspace X. \<not> openin X {x}}"
- apply (auto simp: in_derived_set_of)
- by (metis Set.set_insert all_not_in_conv insertCI openin_subset subsetCE)
+ "X derived_set_of (topspace X) = {x \<in> topspace X. \<not> openin X {x}}" (is "?lhs = ?rhs")
+proof
+ show "?lhs \<subseteq> ?rhs"
+ by (auto simp: in_derived_set_of)
+ show "?rhs \<subseteq> ?lhs"
+ by (clarsimp simp: in_derived_set_of) (metis openin_closedin_eq openin_subopen singletonD subset_eq)
+qed
lemma discrete_topology_unique_derived_set:
"discrete_topology U = X \<longleftrightarrow> topspace X = U \<and> X derived_set_of U = {}"
@@ -676,7 +668,8 @@
"S \<inter> X derived_set_of S = {} \<Longrightarrow> subtopology X S = discrete_topology(topspace X \<inter> S)"
by (metis Int_lower1 derived_set_of_restrict inf_assoc inf_bot_right subtopology_eq_discrete_topology_eq subtopology_subtopology subtopology_topspace)
-lemma subtopology_discrete_topology [simp]: "subtopology (discrete_topology U) S = discrete_topology(U \<inter> S)"
+lemma subtopology_discrete_topology [simp]:
+ "subtopology (discrete_topology U) S = discrete_topology(U \<inter> S)"
proof -
have "(\<lambda>T. \<exists>Sa. T = Sa \<inter> S \<and> Sa \<subseteq> U) = (\<lambda>Sa. Sa \<subseteq> U \<and> Sa \<subseteq> S)"
by force
@@ -688,10 +681,14 @@
by (auto simp: derived_set_of_def)
lemma openin_Int_derived_set_of_eq:
- "openin X S \<Longrightarrow> S \<inter> X derived_set_of T = S \<inter> X derived_set_of (S \<inter> T)"
- apply auto
- apply (meson IntI openin_Int_derived_set_of_subset subsetCE)
- by (meson derived_set_of_mono inf_sup_ord(2) subset_eq)
+ assumes "openin X S"
+ shows "S \<inter> X derived_set_of T = S \<inter> X derived_set_of (S \<inter> T)" (is "?lhs = ?rhs")
+proof
+ show "?lhs \<subseteq> ?rhs"
+ by (simp add: assms openin_Int_derived_set_of_subset)
+ show "?rhs \<subseteq> ?lhs"
+ by (metis derived_set_of_mono inf_commute inf_le1 inf_mono order_refl)
+qed
subsection\<open> Closure with respect to a topological space\<close>
@@ -701,9 +698,7 @@
lemma closure_of_restrict: "X closure_of S = X closure_of (topspace X \<inter> S)"
unfolding closure_of_def
- apply safe
- apply (meson IntI openin_subset subset_iff)
- by auto
+ using openin_subset by blast
lemma in_closure_of:
"x \<in> X closure_of S \<longleftrightarrow>
@@ -769,18 +764,13 @@
by (auto simp: closure_of_def)
lemma closure_of_subset_eq: "S \<subseteq> topspace X \<and> X closure_of S \<subseteq> S \<longleftrightarrow> closedin X S"
-proof (cases "S \<subseteq> topspace X")
- case True
- then have "\<forall>x. x \<in> topspace X \<and> (\<forall>T. x \<in> T \<and> openin X T \<longrightarrow> (\<exists>y\<in>S. y \<in> T)) \<longrightarrow> x \<in> S
- \<Longrightarrow> openin X (topspace X - S)"
- apply (subst openin_subopen, safe)
- by (metis DiffI subset_eq openin_subset [of X])
+proof -
+ have "openin X (topspace X - S)"
+ if "\<And>x. \<lbrakk>x \<in> topspace X; \<forall>T. x \<in> T \<and> openin X T \<longrightarrow> S \<inter> T \<noteq> {}\<rbrakk> \<Longrightarrow> x \<in> S"
+ apply (subst openin_subopen)
+ by (metis Diff_iff Diff_mono Diff_triv inf.commute openin_subset order_refl that)
then show ?thesis
- by (auto simp: closedin_def closure_of_def)
-next
- case False
- then show ?thesis
- by (simp add: closedin_def)
+ by (auto simp: closedin_def closure_of_def disjoint_iff_not_equal)
qed
lemma closure_of_eq: "X closure_of S = S \<longleftrightarrow> closedin X S"
@@ -890,15 +880,23 @@
qed
lemma openin_Int_closure_of_eq:
- "openin X S \<Longrightarrow> S \<inter> X closure_of T = S \<inter> X closure_of (S \<inter> T)"
- apply (rule equalityI)
- apply (simp add: openin_Int_closure_of_subset)
- by (meson closure_of_mono inf.cobounded2 inf_mono subset_refl)
+ assumes "openin X S" shows "S \<inter> X closure_of T = S \<inter> X closure_of (S \<inter> T)" (is "?lhs = ?rhs")
+proof
+ show "?lhs \<subseteq> ?rhs"
+ by (simp add: assms openin_Int_closure_of_subset)
+ show "?rhs \<subseteq> ?lhs"
+ by (metis closure_of_mono inf_commute inf_le1 inf_mono order_refl)
+qed
lemma openin_Int_closure_of_eq_empty:
- "openin X S \<Longrightarrow> S \<inter> X closure_of T = {} \<longleftrightarrow> S \<inter> T = {}"
- apply (subst openin_Int_closure_of_eq, auto)
- by (meson IntI closure_of_subset_Int disjoint_iff_not_equal openin_subset subset_eq)
+ assumes "openin X S" shows "S \<inter> X closure_of T = {} \<longleftrightarrow> S \<inter> T = {}" (is "?lhs = ?rhs")
+proof
+ show "?lhs \<Longrightarrow> ?rhs"
+ unfolding disjoint_iff
+ by (meson assms in_closure_of in_mono openin_subset)
+ show "?rhs \<Longrightarrow> ?lhs"
+ by (simp add: assms openin_Int_closure_of_eq)
+qed
lemma closure_of_openin_Int_superset:
"openin X S \<and> S \<subseteq> X closure_of T
@@ -998,11 +996,13 @@
lemma interior_of_subset_subtopology: "(subtopology X S) interior_of T \<subseteq> S"
by (meson openin_imp_subset openin_interior_of)
-lemma interior_of_Int: "X interior_of (S \<inter> T) = X interior_of S \<inter> X interior_of T"
- apply (rule equalityI)
- apply (simp add: interior_of_mono)
- apply (auto simp: interior_of_maximal_eq openin_Int interior_of_subset le_infI1 le_infI2)
- done
+lemma interior_of_Int: "X interior_of (S \<inter> T) = X interior_of S \<inter> X interior_of T" (is "?lhs = ?rhs")
+proof
+ show "?lhs \<subseteq> ?rhs"
+ by (simp add: interior_of_mono)
+ show "?rhs \<subseteq> ?lhs"
+ by (meson inf_mono interior_of_maximal interior_of_subset openin_Int openin_interior_of)
+qed
lemma interior_of_Inter_subset: "X interior_of (\<Inter>\<F>) \<subseteq> (\<Inter>S \<in> \<F>. X interior_of S)"
by (simp add: INT_greatest Inf_lower interior_of_mono)
@@ -1252,9 +1252,15 @@
by (simp add: frontier_of_Int)
lemma frontier_of_Int_closedin:
- "\<lbrakk>closedin X S; closedin X T\<rbrakk> \<Longrightarrow> X frontier_of(S \<inter> T) = X frontier_of S \<inter> T \<union> S \<inter> X frontier_of T"
- apply (simp add: frontier_of_Int closedin_Int closure_of_closedin)
- using frontier_of_subset_closedin by blast
+ assumes "closedin X S" "closedin X T"
+ shows "X frontier_of(S \<inter> T) = X frontier_of S \<inter> T \<union> S \<inter> X frontier_of T" (is "?lhs = ?rhs")
+proof
+ show "?lhs \<subseteq> ?rhs"
+ using assms by (force simp add: frontier_of_Int closedin_Int closure_of_closedin)
+ show "?rhs \<subseteq> ?lhs"
+ using assms frontier_of_subset_closedin
+ by (auto simp add: frontier_of_Int closedin_Int closure_of_closedin)
+qed
lemma frontier_of_Un_subset: "X frontier_of(S \<union> T) \<subseteq> X frontier_of S \<union> X frontier_of T"
by (metis Diff_Un frontier_of_Int_subset frontier_of_complement)
@@ -1296,10 +1302,10 @@
assumes "locally_finite_in X \<A>" "\<B> \<subseteq> \<A>"
shows "locally_finite_in X \<B>"
proof -
- have "finite {U \<in> \<A>. U \<inter> V \<noteq> {}} \<Longrightarrow> finite {U \<in> \<B>. U \<inter> V \<noteq> {}}" for V
- apply (erule rev_finite_subset) using \<open>\<B> \<subseteq> \<A>\<close> by blast
+ have "finite (\<A> \<inter> {U. U \<inter> V \<noteq> {}}) \<Longrightarrow> finite (\<B> \<inter> {U. U \<inter> V \<noteq> {}})" for V
+ by (meson \<open>\<B> \<subseteq> \<A>\<close> finite_subset inf_le1 inf_le2 le_inf_iff subset_trans)
then show ?thesis
- using assms unfolding locally_finite_in_def by (fastforce simp add:)
+ using assms unfolding locally_finite_in_def Int_def by fastforce
qed
lemma locally_finite_in_refinement:
@@ -1411,11 +1417,16 @@
by clarify (meson Union_upper closure_of_mono subsetD)
lemma closure_of_locally_finite_Union:
- "locally_finite_in X \<A> \<Longrightarrow> X closure_of (\<Union>\<A>) = \<Union>((\<lambda>S. X closure_of S) ` \<A>)"
- apply (rule closure_of_unique)
- apply (simp add: SUP_upper2 Sup_le_iff closure_of_subset locally_finite_in_def)
- apply (simp add: closedin_Union_locally_finite_closure)
- by (simp add: Sup_le_iff closure_of_minimal)
+ assumes "locally_finite_in X \<A>"
+ shows "X closure_of (\<Union>\<A>) = \<Union>((\<lambda>S. X closure_of S) ` \<A>)"
+proof (rule closure_of_unique)
+ show "\<Union> \<A> \<subseteq> \<Union> ((closure_of) X ` \<A>)"
+ using assms by (simp add: SUP_upper2 Sup_le_iff closure_of_subset locally_finite_in_def)
+ show "closedin X (\<Union> ((closure_of) X ` \<A>))"
+ using assms by (simp add: closedin_Union_locally_finite_closure)
+ show "\<And>T'. \<lbrakk>\<Union> \<A> \<subseteq> T'; closedin X T'\<rbrakk> \<Longrightarrow> \<Union> ((closure_of) X ` \<A>) \<subseteq> T'"
+ by (simp add: Sup_le_iff closure_of_minimal)
+qed
subsection\<^marker>\<open>tag important\<close> \<open>Continuous maps\<close>
@@ -1595,11 +1606,16 @@
qed
lemma topology_finer_continuous_id:
- "topspace X = topspace Y \<Longrightarrow> ((\<forall>S. openin X S \<longrightarrow> openin Y S) \<longleftrightarrow> continuous_map Y X id)"
- unfolding continuous_map_def
- apply auto
- using openin_subopen openin_subset apply fastforce
- using openin_subopen topspace_def by fastforce
+ assumes "topspace X = topspace Y"
+ shows "(\<forall>S. openin X S \<longrightarrow> openin Y S) \<longleftrightarrow> continuous_map Y X id" (is "?lhs = ?rhs")
+proof
+ show "?lhs \<Longrightarrow> ?rhs"
+ unfolding continuous_map_def
+ using assms openin_subopen openin_subset by fastforce
+ show "?rhs \<Longrightarrow> ?lhs"
+ unfolding continuous_map_def
+ using assms openin_subopen topspace_def by fastforce
+qed
lemma continuous_map_const [simp]:
"continuous_map X Y (\<lambda>x. C) \<longleftrightarrow> topspace X = {} \<or> C \<in> topspace Y"
@@ -1895,22 +1911,34 @@
unfolding closed_map_def closedin_subtopology_alt by blast
lemma open_map_restriction:
- "\<lbrakk>open_map X X' f; {x. x \<in> topspace X \<and> f x \<in> V} = U\<rbrakk>
- \<Longrightarrow> open_map (subtopology X U) (subtopology X' V) f"
- unfolding open_map_def openin_subtopology_alt
- apply clarify
- apply (rename_tac T)
- apply (rule_tac x="f ` T" in image_eqI)
- using openin_closedin_eq by fastforce+
+ assumes f: "open_map X X' f" and U: "{x \<in> topspace X. f x \<in> V} = U"
+ shows "open_map (subtopology X U) (subtopology X' V) f"
+ unfolding open_map_def
+proof clarsimp
+ fix W
+ assume "openin (subtopology X U) W"
+ then obtain T where "openin X T" "W = T \<inter> U"
+ by (meson openin_subtopology)
+ with f U have "f ` W = (f ` T) \<inter> V"
+ unfolding open_map_def openin_closedin_eq by auto
+ then show "openin (subtopology X' V) (f ` W)"
+ by (metis \<open>openin X T\<close> f open_map_def openin_subtopology_Int)
+qed
lemma closed_map_restriction:
- "\<lbrakk>closed_map X X' f; {x. x \<in> topspace X \<and> f x \<in> V} = U\<rbrakk>
- \<Longrightarrow> closed_map (subtopology X U) (subtopology X' V) f"
- unfolding closed_map_def closedin_subtopology_alt
- apply clarify
- apply (rename_tac T)
- apply (rule_tac x="f ` T" in image_eqI)
- using closedin_def by fastforce+
+ assumes f: "closed_map X X' f" and U: "{x \<in> topspace X. f x \<in> V} = U"
+ shows "closed_map (subtopology X U) (subtopology X' V) f"
+ unfolding closed_map_def
+proof clarsimp
+ fix W
+ assume "closedin (subtopology X U) W"
+ then obtain T where "closedin X T" "W = T \<inter> U"
+ by (meson closedin_subtopology)
+ with f U have "f ` W = (f ` T) \<inter> V"
+ unfolding closed_map_def closedin_def by auto
+ then show "closedin (subtopology X' V) (f ` W)"
+ by (metis \<open>closedin X T\<close> closed_map_def closedin_subtopology f)
+qed
subsection\<open>Quotient maps\<close>
@@ -2112,9 +2140,7 @@
lemma quotient_map_compose_eq:
"quotient_map X X' f \<Longrightarrow> quotient_map X X'' (g \<circ> f) \<longleftrightarrow> quotient_map X' X'' g"
- apply safe
- apply (meson continuous_compose_quotient_map_eq quotient_imp_continuous_map quotient_map_from_composition)
- by (simp add: quotient_map_compose)
+ by (meson continuous_compose_quotient_map_eq quotient_imp_continuous_map quotient_map_compose quotient_map_from_composition)
lemma quotient_map_restriction:
assumes quo: "quotient_map X Y f" and U: "{x \<in> topspace X. f x \<in> V} = U" and disj: "openin Y V \<or> closedin Y V"
@@ -2263,10 +2289,8 @@
by (metis closedin_def closure_of_eq inf_commute)
lemma separatedin_subtopology:
- "separatedin (subtopology X U) S T \<longleftrightarrow> S \<subseteq> U \<and> T \<subseteq> U \<and> separatedin X S T"
- apply (simp add: separatedin_def closure_of_subtopology)
- apply (safe; metis Int_absorb1 inf.assoc inf.orderE insert_disjoint(2) mk_disjoint_insert)
- done
+ "separatedin (subtopology X U) S T \<longleftrightarrow> S \<subseteq> U \<and> T \<subseteq> U \<and> separatedin X S T" (is "?lhs = ?rhs")
+ by (auto simp: separatedin_def closure_of_subtopology Int_ac disjoint_iff elim!: inf.orderE)
lemma separatedin_discrete_topology:
"separatedin (discrete_topology U) S T \<longleftrightarrow> S \<subseteq> U \<and> T \<subseteq> U \<and> disjnt S T"
@@ -2292,24 +2316,24 @@
lemma separatedin_openin_diff:
"\<lbrakk>openin X S; openin X T\<rbrakk> \<Longrightarrow> separatedin X (S - T) (T - S)"
unfolding separatedin_def
- apply (intro conjI)
- apply (meson Diff_subset openin_subset subset_trans)+
- using openin_Int_closure_of_eq_empty by fastforce+
+ by (metis Diff_Int_distrib2 Diff_disjoint Diff_empty Diff_mono empty_Diff empty_subsetI openin_Int_closure_of_eq_empty openin_subset)
lemma separatedin_closedin_diff:
- "\<lbrakk>closedin X S; closedin X T\<rbrakk> \<Longrightarrow> separatedin X (S - T) (T - S)"
- apply (simp add: separatedin_def Diff_Int_distrib2 closure_of_minimal inf_absorb2)
- apply (meson Diff_subset closedin_subset subset_trans)
- done
+ assumes "closedin X S" "closedin X T"
+ shows "separatedin X (S - T) (T - S)"
+proof -
+ have "S - T \<subseteq> topspace X" "T - S \<subseteq> topspace X"
+ using assms closedin_subset by auto
+ with assms show ?thesis
+ by (simp add: separatedin_def Diff_Int_distrib2 closure_of_minimal inf_absorb2)
+qed
lemma separation_closedin_Un_gen:
"separatedin X S T \<longleftrightarrow>
S \<subseteq> topspace X \<and> T \<subseteq> topspace X \<and> disjnt S T \<and>
closedin (subtopology X (S \<union> T)) S \<and>
closedin (subtopology X (S \<union> T)) T"
- apply (simp add: separatedin_def closedin_Int_closure_of disjnt_iff)
- using closure_of_subset apply blast
- done
+ by (auto simp add: separatedin_def closedin_Int_closure_of disjnt_iff dest: closure_of_subset)
lemma separation_openin_Un_gen:
"separatedin X S T \<longleftrightarrow>
@@ -2342,7 +2366,7 @@
"\<lbrakk>homeomorphic_maps X Y f g;
\<And>x. x \<in> topspace X \<Longrightarrow> f x = f' x; \<And>y. y \<in> topspace Y \<Longrightarrow> g y = g' y\<rbrakk>
\<Longrightarrow> homeomorphic_maps X Y f' g'"
- apply (simp add: homeomorphic_maps_def)
+ unfolding homeomorphic_maps_def
by (metis continuous_map_eq continuous_map_eq_image_closure_subset_gen image_subset_iff)
lemma homeomorphic_maps_sym:
@@ -2350,8 +2374,7 @@
by (auto simp: homeomorphic_maps_def)
lemma homeomorphic_maps_id:
- "homeomorphic_maps X Y id id \<longleftrightarrow> Y = X"
- (is "?lhs = ?rhs")
+ "homeomorphic_maps X Y id id \<longleftrightarrow> Y = X" (is "?lhs = ?rhs")
proof
assume L: ?lhs
then have "topspace X = topspace Y"
@@ -2621,28 +2644,24 @@
(\<forall>T. T \<subseteq> topspace Y \<longrightarrow> f x \<in> T \<longrightarrow> openin Y T \<longrightarrow> (\<exists>y. y \<noteq> f x \<and> y \<in> f ` S \<and> y \<in> T))"
if "x \<in> topspace X" for x
proof -
- have 1: "(x \<in> T \<and> openin X T) = (T \<subseteq> topspace X \<and> f x \<in> f ` T \<and> openin Y (f ` T))" for T
+ have \<section>: "(x \<in> T \<and> openin X T) = (T \<subseteq> topspace X \<and> f x \<in> f ` T \<and> openin Y (f ` T))" for T
by (meson hom homeomorphic_map_openness_eq inj inj_on_image_mem_iff that)
- have 2: "(\<exists>y. y \<noteq> x \<and> y \<in> S \<and> y \<in> T) = (\<exists>y. y \<noteq> f x \<and> y \<in> f ` S \<and> y \<in> f ` T)" (is "?lhs = ?rhs")
+ moreover have "(\<exists>y. y \<noteq> x \<and> y \<in> S \<and> y \<in> T) = (\<exists>y. y \<noteq> f x \<and> y \<in> f ` S \<and> y \<in> f ` T)" (is "?lhs = ?rhs")
if "T \<subseteq> topspace X \<and> f x \<in> f ` T \<and> openin Y (f ` T)" for T
proof
show "?lhs \<Longrightarrow> ?rhs"
- by (meson "1" imageI inj inj_on_eq_iff inj_on_subset that)
+ by (meson \<section> imageI inj inj_on_eq_iff inj_on_subset that)
show "?rhs \<Longrightarrow> ?lhs"
using S inj inj_onD that by fastforce
qed
- show ?thesis
- apply (simp flip: fim add: all_subset_image)
- apply (simp flip: imp_conjL)
- by (intro all_cong1 imp_cong 1 2)
+ ultimately show ?thesis
+ by (auto simp flip: fim simp: all_subset_image)
qed
have *: "\<lbrakk>T = f ` S; \<And>x. x \<in> S \<Longrightarrow> P x \<longleftrightarrow> Q(f x)\<rbrakk> \<Longrightarrow> {y. y \<in> T \<and> Q y} = f ` {x \<in> S. P x}" for T S P Q
by auto
show ?thesis
unfolding derived_set_of_def
- apply (rule *)
- using fim apply blast
- using iff openin_subset by force
+ by (rule *) (use fim iff openin_subset in force)+
qed
@@ -2724,14 +2743,21 @@
by (meson homeomorphic_map_maps homeomorphic_maps_subtopologies)
lemma homeomorphic_map_subtopologies_alt:
- "\<lbrakk>homeomorphic_map X Y f;
- \<And>x. \<lbrakk>x \<in> topspace X; f x \<in> topspace Y\<rbrakk> \<Longrightarrow> f x \<in> T \<longleftrightarrow> x \<in> S\<rbrakk>
- \<Longrightarrow> homeomorphic_map (subtopology X S) (subtopology Y T) f"
- unfolding homeomorphic_map_maps
- apply (erule ex_forward)
- apply (rule homeomorphic_maps_subtopologies)
- apply (auto simp: homeomorphic_maps_def continuous_map_def)
- by (metis IntI image_iff)
+ assumes hom: "homeomorphic_map X Y f"
+ and S: "\<And>x. \<lbrakk>x \<in> topspace X; f x \<in> topspace Y\<rbrakk> \<Longrightarrow> f x \<in> T \<longleftrightarrow> x \<in> S"
+ shows "homeomorphic_map (subtopology X S) (subtopology Y T) f"
+proof -
+ have "homeomorphic_maps (subtopology X S) (subtopology Y T) f g"
+ if "homeomorphic_maps X Y f g" for g
+ proof (rule homeomorphic_maps_subtopologies [OF that])
+ show "f ` (topspace X \<inter> S) = topspace Y \<inter> T"
+ using that S
+ apply (auto simp: homeomorphic_maps_def continuous_map_def)
+ by (metis IntI image_iff)
+ qed
+ then show ?thesis
+ using hom by (meson homeomorphic_map_maps)
+qed
subsection\<open>Relation of homeomorphism between topological spaces\<close>
@@ -2859,10 +2885,7 @@
"connected_space X \<longleftrightarrow>
(\<nexists>E1 E2. closedin X E1 \<and> closedin X E2 \<and>
E1 \<union> E2 = topspace X \<and> E1 \<inter> E2 = {} \<and> E1 \<noteq> {} \<and> E2 \<noteq> {})"
- apply (simp add: connected_space_closedin)
- apply (intro all_cong)
- using closedin_subset apply blast
- done
+ by (metis closedin_Un closedin_def connected_space_closedin subset_antisym)
lemma connected_space_clopen_in:
"connected_space X \<longleftrightarrow>
@@ -2881,16 +2904,14 @@
S \<subseteq> topspace X \<and>
(\<nexists>E1 E2.
openin X E1 \<and> openin X E2 \<and>
- S \<subseteq> E1 \<union> E2 \<and> E1 \<inter> E2 \<inter> S = {} \<and> E1 \<inter> S \<noteq> {} \<and> E2 \<inter> S \<noteq> {})"
+ S \<subseteq> E1 \<union> E2 \<and> E1 \<inter> E2 \<inter> S = {} \<and> E1 \<inter> S \<noteq> {} \<and> E2 \<inter> S \<noteq> {})" (is "?lhs = ?rhs")
proof -
have *: "(\<exists>E1:: 'a set. \<exists>E2:: 'a set. (\<exists>T1:: 'a set. P1 T1 \<and> E1 = f1 T1) \<and> (\<exists>T2:: 'a set. P2 T2 \<and> E2 = f2 T2) \<and>
R E1 E2) \<longleftrightarrow> (\<exists>T1 T2. P1 T1 \<and> P2 T2 \<and> R(f1 T1) (f2 T2))" for P1 f1 P2 f2 R
by auto
- show ?thesis
- unfolding connectedin_def connected_space_def openin_subtopology topspace_subtopology Not_eq_iff *
- apply (intro conj_cong arg_cong [where f=Not] ex_cong1 refl)
- apply (blast elim: dest!: openin_subset)+
- done
+ show ?thesis
+ unfolding connectedin_def connected_space_def openin_subtopology topspace_subtopology *
+ by (intro conj_cong arg_cong [where f=Not] ex_cong1; blast dest!: openin_subset)
qed
lemma connectedin_iff_connected [simp]: "connectedin euclidean S \<longleftrightarrow> connected S"
@@ -2908,10 +2929,8 @@
R E1 E2) \<longleftrightarrow> (\<exists>T1 T2. P1 T1 \<and> P2 T2 \<and> R(f1 T1) (f2 T2))" for P1 f1 P2 f2 R
by auto
show ?thesis
- unfolding connectedin_def connected_space_closedin closedin_subtopology topspace_subtopology Not_eq_iff *
- apply (intro conj_cong arg_cong [where f=Not] ex_cong1 refl)
- apply (blast elim: dest!: openin_subset)+
- done
+ unfolding connectedin_def connected_space_closedin closedin_subtopology topspace_subtopology *
+ by (intro conj_cong arg_cong [where f=Not] ex_cong1; blast dest!: openin_subset)
qed
lemma connectedin_empty [simp]: "connectedin X {}"
@@ -2926,9 +2945,7 @@
lemma connectedin_absolute [simp]:
"connectedin (subtopology X S) S \<longleftrightarrow> connectedin X S"
- apply (simp only: connectedin_def topspace_subtopology subtopology_subtopology)
- apply (intro conj_cong imp_cong arg_cong [where f=Not] all_cong1 ex_cong1 refl)
- by auto
+ by (simp add: connectedin_subtopology)
lemma connectedin_Union:
assumes \<U>: "\<And>S. S \<in> \<U> \<Longrightarrow> connectedin X S" and ne: "\<Inter>\<U> \<noteq> {}"
@@ -3008,14 +3025,14 @@
assumes "connectedin X S" "S \<subseteq> T" "T \<subseteq> X closure_of S"
shows "connectedin X T"
proof -
- have S: "S \<subseteq> topspace X"and T: "T \<subseteq> topspace X"
+ have S: "S \<subseteq> topspace X" and T: "T \<subseteq> topspace X"
using assms by (meson closure_of_subset_topspace dual_order.trans)+
- show ?thesis
- using assms
- apply (simp add: connectedin closure_of_subset_topspace S T)
- apply (elim all_forward imp_forward2 asm_rl)
- apply (blast dest: openin_Int_closure_of_eq_empty [of X _ S])+
- done
+ have \<section>: "\<And>E1 E2. \<lbrakk>openin X E1; openin X E2; E1 \<inter> S = {} \<or> E2 \<inter> S = {}\<rbrakk> \<Longrightarrow> E1 \<inter> T = {} \<or> E2 \<inter> T = {}"
+ using assms unfolding disjoint_iff by (meson in_closure_of subsetD)
+ then show ?thesis
+ using assms
+ unfolding connectedin closure_of_subset_topspace S T
+ by (metis Int_empty_right T dual_order.trans inf.orderE inf_left_commute)
qed
lemma connectedin_closure_of:
@@ -3035,15 +3052,13 @@
"connectedin X S \<longleftrightarrow>
S \<subseteq> topspace X \<and>
(\<nexists>C1 C2. C1 \<union> C2 = S \<and> C1 \<noteq> {} \<and> C2 \<noteq> {} \<and> separatedin X C1 C2)"
- apply (simp add: separatedin_def connectedin_separation)
- apply (intro conj_cong all_cong1 refl, blast)
- done
+ unfolding separatedin_def by (metis connectedin_separation sup.boundedE)
lemma connectedin_eq_not_separated_subset:
"connectedin X S \<longleftrightarrow>
S \<subseteq> topspace X \<and> (\<nexists>C1 C2. S \<subseteq> C1 \<union> C2 \<and> S \<inter> C1 \<noteq> {} \<and> S \<inter> C2 \<noteq> {} \<and> separatedin X C1 C2)"
proof -
- have *: "\<forall>C1 C2. S \<subseteq> C1 \<union> C2 \<longrightarrow> S \<inter> C1 = {} \<or> S \<inter> C2 = {} \<or> \<not> separatedin X C1 C2"
+ have "\<forall>C1 C2. S \<subseteq> C1 \<union> C2 \<longrightarrow> S \<inter> C1 = {} \<or> S \<inter> C2 = {} \<or> \<not> separatedin X C1 C2"
if "\<And>C1 C2. C1 \<union> C2 = S \<longrightarrow> C1 = {} \<or> C2 = {} \<or> \<not> separatedin X C1 C2"
proof (intro allI)
fix C1 C2
@@ -3051,11 +3066,8 @@
using that [of "S \<inter> C1" "S \<inter> C2"]
by (auto simp: separatedin_mono)
qed
- show ?thesis
- apply (simp add: connectedin_eq_not_separated)
- apply (intro conj_cong refl iffI *)
- apply (blast elim!: all_forward)+
- done
+ then show ?thesis
+ by (metis Un_Int_eq(1) Un_Int_eq(2) connectedin_eq_not_separated order_refl)
qed
lemma connected_space_eq_not_separated:
@@ -3066,20 +3078,25 @@
lemma connected_space_eq_not_separated_subset:
"connected_space X \<longleftrightarrow>
(\<nexists>C1 C2. topspace X \<subseteq> C1 \<union> C2 \<and> C1 \<noteq> {} \<and> C2 \<noteq> {} \<and> separatedin X C1 C2)"
- apply (simp add: connected_space_eq_not_separated)
- apply (intro all_cong1)
- by (metis Un_absorb dual_order.antisym separatedin_def subset_refl sup_mono)
+ by (metis connected_space_eq_not_separated le_sup_iff separatedin_def subset_antisym)
lemma connectedin_subset_separated_union:
"\<lbrakk>connectedin X C; separatedin X S T; C \<subseteq> S \<union> T\<rbrakk> \<Longrightarrow> C \<subseteq> S \<or> C \<subseteq> T"
unfolding connectedin_eq_not_separated_subset by blast
lemma connectedin_nonseparated_union:
- "\<lbrakk>connectedin X S; connectedin X T; \<not>separatedin X S T\<rbrakk> \<Longrightarrow> connectedin X (S \<union> T)"
- apply (simp add: connectedin_eq_not_separated_subset, auto)
- apply (metis (no_types, hide_lams) Diff_subset_conv Diff_triv disjoint_iff_not_equal separatedin_mono sup_commute)
- apply (metis (no_types, hide_lams) Diff_subset_conv Diff_triv disjoint_iff_not_equal separatedin_mono separatedin_sym sup_commute)
- by (meson disjoint_iff_not_equal)
+ assumes "connectedin X S" "connectedin X T" "\<not>separatedin X S T"
+ shows "connectedin X (S \<union> T)"
+proof -
+ have "\<And>C1 C2. \<lbrakk>T \<subseteq> C1 \<union> C2; S \<subseteq> C1 \<union> C2\<rbrakk> \<Longrightarrow>
+ S \<inter> C1 = {} \<and> T \<inter> C1 = {} \<or> S \<inter> C2 = {} \<and> T \<inter> C2 = {} \<or> \<not> separatedin X C1 C2"
+ using assms
+ unfolding connectedin_eq_not_separated_subset
+ by (metis (no_types, lifting) assms connectedin_subset_separated_union inf.orderE separatedin_empty(1) separatedin_mono separatedin_sym)
+ then show ?thesis
+ unfolding connectedin_eq_not_separated_subset
+ by (simp add: assms(1) assms(2) connectedin_subset_topspace Int_Un_distrib2)
+qed
lemma connected_space_closures:
"connected_space X \<longleftrightarrow>
@@ -3104,6 +3121,7 @@
have "S \<subseteq> topspace X" and *:
"\<And>E1 E2. openin X E1 \<longrightarrow> openin X E2 \<longrightarrow> E1 \<inter> E2 \<inter> S = {} \<longrightarrow> S \<subseteq> E1 \<union> E2 \<longrightarrow> E1 \<inter> S = {} \<or> E2 \<inter> S = {}"
using \<open>connectedin X S\<close> by (auto simp: connectedin)
+ moreover
have "S - (topspace X \<inter> T) \<noteq> {}"
using assms(3) by blast
moreover
@@ -3114,17 +3132,18 @@
proof -
have null: "S \<inter> (X closure_of T - X interior_of T) = {}"
using that unfolding frontier_of_def by blast
- have 1: "X interior_of T \<inter> (topspace X - X closure_of T) \<inter> S = {}"
+ have "X interior_of T \<inter> (topspace X - X closure_of T) \<inter> S = {}"
by (metis Diff_disjoint inf_bot_left interior_of_Int interior_of_complement interior_of_empty)
- have 2: "S \<subseteq> X interior_of T \<union> (topspace X - X closure_of T)"
+ moreover have "S \<subseteq> X interior_of T \<union> (topspace X - X closure_of T)"
using that \<open>S \<subseteq> topspace X\<close> null by auto
- have 3: "S \<inter> X interior_of T \<noteq> {}"
+ moreover have "S \<inter> X interior_of T \<noteq> {}"
using closure_of_subset that(1) that(3) null by fastforce
- show ?thesis
- using null \<open>S \<subseteq> topspace X\<close> that * [of "X interior_of T" "topspace X - X closure_of T"]
- apply (clarsimp simp add: openin_diff 1 2)
- apply (simp add: Int_commute Diff_Int_distrib 3)
- by (metis Int_absorb2 contra_subsetD interior_of_subset)
+ ultimately have "S \<inter> X interior_of (topspace X - T) = {}"
+ by (metis "*" inf_commute interior_of_complement openin_interior_of)
+ then have "topspace (subtopology X S) \<inter> X interior_of T = S"
+ using \<open>S \<subseteq> topspace X\<close> interior_of_complement null by fastforce
+ then show ?thesis
+ using that by (metis Diff_eq_empty_iff inf_le2 interior_of_subset subset_trans)
qed
ultimately show ?thesis
by (metis Int_lower1 frontier_of_restrict inf_assoc)
@@ -3152,7 +3171,7 @@
have 2: "openin X ?U" "openin X ?V"
using \<open>openin Y U\<close> \<open>openin Y V\<close> continuous_map f by fastforce+
show "False"
- using * [of ?U ?V] UV \<open>S \<subseteq> topspace X\<close>
+ using * [of ?U ?V] UV \<open>S \<subseteq> topspace X\<close>
by (auto simp: 1 2)
qed
qed
@@ -3160,9 +3179,7 @@
lemma homeomorphic_connected_space:
"X homeomorphic_space Y \<Longrightarrow> connected_space X \<longleftrightarrow> connected_space Y"
unfolding homeomorphic_space_def homeomorphic_maps_def
- apply safe
- apply (metis connectedin_continuous_map_image connected_space_subconnected continuous_map_image_subset_topspace image_eqI image_subset_iff)
- by (metis (no_types, hide_lams) connectedin_continuous_map_image connectedin_topspace continuous_map_def continuous_map_image_subset_topspace imageI set_eq_subset subsetI)
+ by (metis connected_space_subconnected connectedin_continuous_map_image connectedin_topspace continuous_map_image_subset_topspace image_eqI image_subset_iff)
lemma homeomorphic_map_connectedness:
assumes f: "homeomorphic_map X Y f" and U: "U \<subseteq> topspace X"
@@ -3197,9 +3214,10 @@
proof (cases "S = {}")
case False
moreover have "connectedin (discrete_topology U) S \<longleftrightarrow> (\<exists>a. S = {a})"
- apply safe
- using False connectedin_inter_frontier_of insert_Diff apply fastforce
- using True by auto
+ proof
+ show "connectedin (discrete_topology U) S \<Longrightarrow> \<exists>a. S = {a}"
+ using False connectedin_inter_frontier_of insert_Diff by fastforce
+ qed (use True in auto)
ultimately show ?thesis
by auto
qed simp
@@ -3262,9 +3280,7 @@
by (simp add: compactin_subspace)
lemma compactin_subtopology: "compactin (subtopology X S) T \<longleftrightarrow> compactin X T \<and> T \<subseteq> S"
-apply (simp add: compactin_subspace)
- by (metis inf.orderE inf_commute subtopology_subtopology)
-
+ by (metis compactin_subspace inf.absorb_iff2 le_inf_iff subtopology_subtopology topspace_subtopology)
lemma compactin_subset_topspace: "compactin X S \<Longrightarrow> S \<subseteq> topspace X"
by (simp add: compactin_subspace)
@@ -3419,8 +3435,8 @@
proof (cases "topspace X = {}")
case True
then show ?thesis
- apply (clarsimp simp add: compact_space_def closedin_topspace_empty)
- by (metis finite.emptyI finite_insert infinite_super insertI1 subsetI)
+unfolding compact_space_def
+ by (metis Sup_bot_conv(1) closedin_topspace_empty compactin_empty finite.emptyI finite_UnionD order_refl)
next
case False
show ?thesis
@@ -3482,9 +3498,7 @@
((\<forall>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<longrightarrow> S \<inter> \<Inter>\<F> \<noteq> {}) \<longrightarrow> S \<inter> \<Inter>\<U> \<noteq> {})" for \<U>
by simp (use \<open>S \<noteq> {}\<close> in blast)
show ?thesis
- apply (simp only: imp_conjL [symmetric] all_finite_subset_image eq)
- apply (simp add: subset_eq)
- done
+ unfolding imp_conjL [symmetric] all_finite_subset_image eq by blast
qed
finally show ?thesis
using True by simp
@@ -3559,9 +3573,7 @@
lemma discrete_compactin_eq_finite:
"S \<inter> X derived_set_of S = {} \<Longrightarrow> compactin X S \<longleftrightarrow> S \<subseteq> topspace X \<and> finite S"
- apply (rule iffI)
- using compactin_imp_Bolzano_Weierstrass compactin_subset_topspace apply blast
- by (simp add: finite_imp_compactin_eq)
+ by (meson compactin_imp_Bolzano_Weierstrass finite_imp_compactin_eq order_refl)
lemma discrete_compact_space_eq_finite:
"X derived_set_of (topspace X) = {} \<Longrightarrow> (compact_space X \<longleftrightarrow> finite(topspace X))"
@@ -3664,27 +3676,23 @@
by (force simp: embedding_map_def homeomorphic_eq_everything_map)
lemma embedding_map_in_subtopology:
- "embedding_map X (subtopology Y S) f \<longleftrightarrow> embedding_map X Y f \<and> f ` (topspace X) \<subseteq> S"
- apply (auto simp: embedding_map_def subtopology_subtopology Int_absorb1)
- apply (metis (no_types) homeomorphic_imp_surjective_map subtopology_subtopology subtopology_topspace topspace_subtopology)
- apply (simp add: continuous_map_def homeomorphic_eq_everything_map)
- done
+ "embedding_map X (subtopology Y S) f \<longleftrightarrow> embedding_map X Y f \<and> f ` (topspace X) \<subseteq> S" (is "?lhs = ?rhs")
+proof
+ show "?lhs \<Longrightarrow> ?rhs"
+ unfolding embedding_map_def
+ by (metis continuous_map_in_subtopology homeomorphic_imp_continuous_map inf_absorb2 subtopology_subtopology)
+qed (simp add: embedding_map_def inf.absorb_iff2 subtopology_subtopology)
lemma injective_open_imp_embedding_map:
"\<lbrakk>continuous_map X Y f; open_map X Y f; inj_on f (topspace X)\<rbrakk> \<Longrightarrow> embedding_map X Y f"
unfolding embedding_map_def
- apply (rule bijective_open_imp_homeomorphic_map)
- using continuous_map_in_subtopology apply blast
- apply (auto simp: continuous_map_in_subtopology open_map_into_subtopology continuous_map)
- done
+ by (simp add: continuous_map_in_subtopology continuous_open_quotient_map eq_iff homeomorphic_map_def open_map_imp_subset open_map_into_subtopology)
lemma injective_closed_imp_embedding_map:
"\<lbrakk>continuous_map X Y f; closed_map X Y f; inj_on f (topspace X)\<rbrakk> \<Longrightarrow> embedding_map X Y f"
unfolding embedding_map_def
- apply (rule bijective_closed_imp_homeomorphic_map)
- apply (simp_all add: continuous_map_into_subtopology closed_map_into_subtopology)
- apply (simp add: continuous_map inf.absorb_iff2)
- done
+ by (simp add: closed_map_imp_subset closed_map_into_subtopology continuous_closed_quotient_map
+ continuous_map_in_subtopology dual_order.eq_iff homeomorphic_map_def)
lemma embedding_map_imp_homeomorphic_space:
"embedding_map X Y f \<Longrightarrow> X homeomorphic_space (subtopology Y (f ` (topspace X)))"
@@ -3727,9 +3735,23 @@
by (simp add: homeomorphic_maps_def retraction_maps_def)
lemma section_and_retraction_eq_homeomorphic_map:
- "section_map X Y f \<and> retraction_map X Y f \<longleftrightarrow> homeomorphic_map X Y f"
- apply (auto simp: section_map_def retraction_map_def homeomorphic_map_maps retraction_maps_def homeomorphic_maps_def)
- by (metis (full_types) continuous_map_image_subset_topspace image_subset_iff)
+ "section_map X Y f \<and> retraction_map X Y f \<longleftrightarrow> homeomorphic_map X Y f" (is "?lhs = ?rhs")
+proof
+ assume ?lhs
+ then obtain g g' where f: "continuous_map X Y f"
+ and g: "continuous_map Y X g" "\<forall>x\<in>topspace X. g (f x) = x"
+ and g': "continuous_map Y X g'" "\<forall>x\<in>topspace Y. f (g' x) = x"
+ by (auto simp: retraction_map_def retraction_maps_def section_map_def)
+ then have "homeomorphic_maps X Y f g"
+ by (force simp add: homeomorphic_maps_def continuous_map_def)
+ then show ?rhs
+ using homeomorphic_map_maps by blast
+next
+ assume ?rhs
+ then show ?lhs
+ unfolding retraction_map_def section_map_def
+ by (meson homeomorphic_imp_retraction_maps homeomorphic_map_maps homeomorphic_maps_sym)
+qed
lemma section_imp_embedding_map:
"section_map X Y f \<Longrightarrow> embedding_map X Y f"
@@ -3810,10 +3832,7 @@
lemma continuous_map_subtopology_eu [simp]:
"continuous_map (top_of_set S) (subtopology euclidean T) h \<longleftrightarrow> continuous_on S h \<and> h ` S \<subseteq> T"
- apply safe
- apply (metis continuous_map_closedin_preimage_eq continuous_map_in_subtopology continuous_on_closed order_refl topspace_euclidean_subtopology)
- apply (simp add: continuous_map_closedin_preimage_eq image_subset_iff)
- by (metis (no_types, hide_lams) continuous_map_closedin_preimage_eq continuous_map_in_subtopology continuous_on_closed order_refl topspace_euclidean_subtopology)
+ by (simp add: continuous_map_in_subtopology)
lemma continuous_map_euclidean_top_of_set:
assumes eq: "f -` S = UNIV" and cont: "continuous_on UNIV f"
@@ -3850,20 +3869,13 @@
qed
lemma continuous_openin_preimage_eq:
- "continuous_on S f \<longleftrightarrow>
- (\<forall>T. open T \<longrightarrow> openin (top_of_set S) (S \<inter> f -` T))"
-apply safe
-apply (simp add: continuous_openin_preimage_gen)
-apply (fastforce simp add: continuous_on_open openin_open)
-done
+ "continuous_on S f \<longleftrightarrow> (\<forall>T. open T \<longrightarrow> openin (top_of_set S) (S \<inter> f -` T))"
+ by (metis Int_commute continuous_on_open_invariant open_openin openin_subtopology)
lemma continuous_closedin_preimage_eq:
"continuous_on S f \<longleftrightarrow>
(\<forall>T. closed T \<longrightarrow> closedin (top_of_set S) (S \<inter> f -` T))"
-apply safe
-apply (simp add: continuous_closedin_preimage)
-apply (fastforce simp add: continuous_on_closed closedin_closed)
-done
+ by (metis Int_commute closedin_closed continuous_on_closed_invariant)
lemma continuous_open_preimage:
assumes contf: "continuous_on S f" and "open S" "open T"
@@ -3943,17 +3955,17 @@
proof
assume ?lhs
have "openin (top_of_set S) S'"
- apply (subst openin_subopen, clarify)
- apply (rule Times_in_interior_subtopology [OF _ \<open>?lhs\<close>])
- using \<open>y \<in> T'\<close>
- apply auto
- done
+ proof (subst openin_subopen, clarify)
+ show "\<exists>U. openin (top_of_set S) U \<and> x \<in> U \<and> U \<subseteq> S'" if "x \<in> S'" for x
+ using that \<open>y \<in> T'\<close> Times_in_interior_subtopology [OF _ \<open>?lhs\<close>, of x y]
+ by simp (metis mem_Sigma_iff subsetD subsetI)
+ qed
moreover have "openin (top_of_set T) T'"
- apply (subst openin_subopen, clarify)
- apply (rule Times_in_interior_subtopology [OF _ \<open>?lhs\<close>])
- using \<open>x \<in> S'\<close>
- apply auto
- done
+ proof (subst openin_subopen, clarify)
+ show "\<exists>U. openin (top_of_set T) U \<and> y \<in> U \<and> U \<subseteq> T'" if "y \<in> T'" for y
+ using that \<open>x \<in> S'\<close> Times_in_interior_subtopology [OF _ \<open>?lhs\<close>, of x y]
+ by simp (metis mem_Sigma_iff subsetD subsetI)
+ qed
ultimately show ?rhs
by simp
next
@@ -4077,12 +4089,11 @@
smallest topology containing all the elements of \<open>S\<close>:\<close>
lemma generate_topology_on_coarsest:
- assumes "istopology T"
- "\<And>s. s \<in> S \<Longrightarrow> T s"
- "generate_topology_on S s0"
+ assumes T: "istopology T" "\<And>s. s \<in> S \<Longrightarrow> T s"
+ and gen: "generate_topology_on S s0"
shows "T s0"
-using assms(3) apply (induct rule: generate_topology_on.induct)
-using assms(1) assms(2) unfolding istopology_def by auto
+ using gen
+by (induct rule: generate_topology_on.induct) (use T in \<open>auto simp: istopology_def\<close>)
abbreviation\<^marker>\<open>tag unimportant\<close> topology_generated_by::"('a set set) \<Rightarrow> ('a topology)"
where "topology_generated_by S \<equiv> topology (generate_topology_on S)"
@@ -4198,13 +4209,15 @@
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
+ assumes X: "\<And>S. P S \<Longrightarrow> openin X S" and "openin X U"
+ and S: "openin(topology(arbitrary union_of (finite intersection_of P relative_to U))) S"
+shows "openin X S"
+proof -
+ have "(arbitrary union_of (finite intersection_of P relative_to U)) S"
+ using S openin_subbase by blast
+ with X \<open>openin X U\<close> show ?thesis
+ by (force simp add: union_of_def intersection_of_def relative_to_def intro: openin_Int_Inter)
+qed
lemma istopology_subbase_UNIV:
"istopology (arbitrary union_of (finite intersection_of P))"
--- a/src/HOL/Bali/DefiniteAssignment.thy Sun Nov 15 22:04:16 2020 +0100
+++ b/src/HOL/Bali/DefiniteAssignment.thy Sun Nov 15 22:26:13 2020 +0100
@@ -566,7 +566,7 @@
in this rule. For example, if \<^term>\<open>e\<close> is constantly \<^term>\<open>True\<close> then
\<^term>\<open>assigns_if False e = UNIV\<close> and therefor \<^term>\<open>nrm C2=UNIV\<close>.
So finally \<^term>\<open>nrm A = nrm C1\<close>. For the break maps this trick
- workd too, because the trival break map will map all labels to
+ workd too, because the trivial break map will map all labels to
\<^term>\<open>UNIV\<close>. In the example, if no break occurs in \<^term>\<open>c2\<close> the break
maps will trivially map to \<^term>\<open>UNIV\<close> and if a break occurs it will map
to \<^term>\<open>UNIV\<close> too, because \<^term>\<open>assigns_if False e = UNIV\<close>. So
--- a/src/HOL/Code_Evaluation.thy Sun Nov 15 22:04:16 2020 +0100
+++ b/src/HOL/Code_Evaluation.thy Sun Nov 15 22:26:13 2020 +0100
@@ -52,7 +52,7 @@
abbreviation valtermify :: "'a \<Rightarrow> 'a \<times> (unit \<Rightarrow> term)" where
"valtermify x \<equiv> (x, \<lambda>u. termify x)"
-locale term_syntax
+bundle term_syntax
begin
notation App (infixl "<\<cdot>>" 70)
@@ -60,11 +60,6 @@
end
-interpretation term_syntax .
-
-no_notation App (infixl "<\<cdot>>" 70)
- and valapp (infixl "{\<cdot>}" 70)
-
subsection \<open>Tools setup and evaluation\<close>
--- a/src/HOL/Computational_Algebra/Polynomial.thy Sun Nov 15 22:04:16 2020 +0100
+++ b/src/HOL/Computational_Algebra/Polynomial.thy Sun Nov 15 22:26:13 2020 +0100
@@ -3131,7 +3131,7 @@
for p :: "'a::field poly"
by (cases "p = 0") (auto simp: is_unit_triv is_unit_iff_degree)
-lemma is_unit_monom_trival: "is_unit p \<Longrightarrow> monom (coeff p (degree p)) 0 = p"
+lemma is_unit_monom_trivial: "is_unit p \<Longrightarrow> monom (coeff p (degree p)) 0 = p"
for p :: "'a::field poly"
by (cases p) (simp_all add: monom_0 is_unit_pCons_iff)
--- a/src/HOL/Divides.thy Sun Nov 15 22:04:16 2020 +0100
+++ b/src/HOL/Divides.thy Sun Nov 15 22:26:13 2020 +0100
@@ -440,7 +440,7 @@
by auto
qed
-lemma zmod_trival_iff:
+lemma zmod_trivial_iff:
fixes i k :: int
shows "i mod k = i \<longleftrightarrow> k = 0 \<or> 0 \<le> i \<and> i < k \<or> i \<le> 0 \<and> k < i"
proof -
@@ -488,7 +488,7 @@
using pos_mod_bound [of l k] apply linarith
done
with \<open>l > 0\<close> have \<open>(k mod l - 1) mod l = k mod l - 1\<close>
- by (simp add: zmod_trival_iff)
+ by (simp add: zmod_trivial_iff)
ultimately show ?thesis
apply (simp only: zmod_zminus1_eq_if)
apply (simp add: mod_eq_0_iff_dvd algebra_simps mod_simps)
@@ -1240,7 +1240,7 @@
have \<open>(k + 1) mod 2 ^ n = (k mod 2 ^ n + 1) mod 2 ^ n\<close>
by (simp add: mod_simps)
also have \<open>\<dots> = k mod 2 ^ n + 1\<close>
- using * by (simp add: zmod_trival_iff)
+ using * by (simp add: zmod_trivial_iff)
finally have \<open>(k + 1) mod 2 ^ n = k mod 2 ^ n + 1\<close> .
then show ?thesis
by (simp add: take_bit_eq_mod)
@@ -1259,7 +1259,7 @@
have \<open>(k - 1) mod 2 ^ n = (k mod 2 ^ n - 1) mod 2 ^ n\<close>
by (simp add: mod_simps)
also have \<open>\<dots> = k mod 2 ^ n - 1\<close>
- by (simp add: zmod_trival_iff)
+ by (simp add: zmod_trivial_iff)
(use \<open>k mod 2 ^ n < 2 ^ n\<close> * in linarith)
finally have \<open>(k - 1) mod 2 ^ n = k mod 2 ^ n - 1\<close> .
then show ?thesis
--- a/src/HOL/Library/Bit_Operations.thy Sun Nov 15 22:04:16 2020 +0100
+++ b/src/HOL/Library/Bit_Operations.thy Sun Nov 15 22:26:13 2020 +0100
@@ -16,9 +16,9 @@
and or :: \<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close> (infixr \<open>OR\<close> 59)
and xor :: \<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close> (infixr \<open>XOR\<close> 59)
and mask :: \<open>nat \<Rightarrow> 'a\<close>
- assumes bit_and_iff: \<open>\<And>n. bit (a AND b) n \<longleftrightarrow> bit a n \<and> bit b n\<close>
- and bit_or_iff: \<open>\<And>n. bit (a OR b) n \<longleftrightarrow> bit a n \<or> bit b n\<close>
- and bit_xor_iff: \<open>\<And>n. bit (a XOR b) n \<longleftrightarrow> bit a n \<noteq> bit b n\<close>
+ assumes bit_and_iff [bit_simps]: \<open>\<And>n. bit (a AND b) n \<longleftrightarrow> bit a n \<and> bit b n\<close>
+ and bit_or_iff [bit_simps]: \<open>\<And>n. bit (a OR b) n \<longleftrightarrow> bit a n \<or> bit b n\<close>
+ and bit_xor_iff [bit_simps]: \<open>\<And>n. bit (a XOR b) n \<longleftrightarrow> bit a n \<noteq> bit b n\<close>
and mask_eq_exp_minus_1: \<open>mask n = 2 ^ n - 1\<close>
begin
@@ -119,7 +119,7 @@
\<open>drop_bit n (a XOR b) = drop_bit n a XOR drop_bit n b\<close>
by (rule bit_eqI) (auto simp add: bit_drop_bit_eq bit_xor_iff)
-lemma bit_mask_iff:
+lemma bit_mask_iff [bit_simps]:
\<open>bit (mask m) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> n < m\<close>
by (simp add: mask_eq_exp_minus_1 bit_mask_iff)
@@ -182,7 +182,7 @@
class ring_bit_operations = semiring_bit_operations + ring_parity +
fixes not :: \<open>'a \<Rightarrow> 'a\<close> (\<open>NOT\<close>)
- assumes bit_not_iff: \<open>\<And>n. bit (NOT a) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> \<not> bit a n\<close>
+ assumes bit_not_iff [bit_simps]: \<open>\<And>n. bit (NOT a) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> \<not> bit a n\<close>
assumes minus_eq_not_minus_1: \<open>- a = NOT (a - 1)\<close>
begin
@@ -205,7 +205,7 @@
\<open>- a = NOT a + 1\<close>
using not_eq_complement [of a] by simp
-lemma bit_minus_iff:
+lemma bit_minus_iff [bit_simps]:
\<open>bit (- a) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> \<not> bit (a - 1) n\<close>
by (simp add: minus_eq_not_minus_1 bit_not_iff)
@@ -213,7 +213,7 @@
"even (NOT a) \<longleftrightarrow> odd a"
using bit_not_iff [of a 0] by auto
-lemma bit_not_exp_iff:
+lemma bit_not_exp_iff [bit_simps]:
\<open>bit (NOT (2 ^ m)) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> n \<noteq> m\<close>
by (auto simp add: bit_not_iff bit_exp_iff)
@@ -221,9 +221,9 @@
\<open>bit (- 1) n \<longleftrightarrow> 2 ^ n \<noteq> 0\<close>
by (simp add: bit_minus_iff)
-lemma bit_minus_exp_iff:
+lemma bit_minus_exp_iff [bit_simps]:
\<open>bit (- (2 ^ m)) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> n \<ge> m\<close>
- oops
+ by (auto simp add: bit_simps simp flip: mask_eq_exp_minus_1)
lemma bit_minus_2_iff [simp]:
\<open>bit (- 2) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> n > 0\<close>
@@ -361,7 +361,7 @@
definition flip_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close>
where \<open>flip_bit n a = a XOR push_bit n 1\<close>
-lemma bit_set_bit_iff:
+lemma bit_set_bit_iff [bit_simps]:
\<open>bit (set_bit m a) n \<longleftrightarrow> bit a n \<or> (m = n \<and> 2 ^ n \<noteq> 0)\<close>
by (auto simp add: set_bit_def push_bit_of_1 bit_or_iff bit_exp_iff)
@@ -369,7 +369,7 @@
\<open>even (set_bit m a) \<longleftrightarrow> even a \<and> m \<noteq> 0\<close>
using bit_set_bit_iff [of m a 0] by auto
-lemma bit_unset_bit_iff:
+lemma bit_unset_bit_iff [bit_simps]:
\<open>bit (unset_bit m a) n \<longleftrightarrow> bit a n \<and> m \<noteq> n\<close>
by (auto simp add: unset_bit_def push_bit_of_1 bit_and_iff bit_not_iff bit_exp_iff exp_eq_0_imp_not_bit)
@@ -377,7 +377,7 @@
\<open>even (unset_bit m a) \<longleftrightarrow> even a \<or> m = 0\<close>
using bit_unset_bit_iff [of m a 0] by auto
-lemma bit_flip_bit_iff:
+lemma bit_flip_bit_iff [bit_simps]:
\<open>bit (flip_bit m a) n \<longleftrightarrow> (m = n \<longleftrightarrow> \<not> bit a n) \<and> 2 ^ n \<noteq> 0\<close>
by (auto simp add: flip_bit_def push_bit_of_1 bit_xor_iff bit_exp_iff exp_eq_0_imp_not_bit)
@@ -583,7 +583,7 @@
\<open>NOT k div 2 = NOT (k div 2)\<close> for k :: int
by (simp add: not_int_def)
-lemma bit_not_int_iff:
+lemma bit_not_int_iff [bit_simps]:
\<open>bit (NOT k) n \<longleftrightarrow> \<not> bit k n\<close>
for k :: int
by (simp add: bit_not_int_iff' not_int_def)
@@ -973,7 +973,7 @@
\<open>even (of_int k) \<longleftrightarrow> even k\<close>
by (induction k rule: int_bit_induct) simp_all
-lemma bit_of_int_iff:
+lemma bit_of_int_iff [bit_simps]:
\<open>bit (of_int k) n \<longleftrightarrow> (2::'a) ^ n \<noteq> 0 \<and> bit k n\<close>
proof (cases \<open>(2::'a) ^ n = 0\<close>)
case True
@@ -1157,7 +1157,7 @@
definition concat_bit :: \<open>nat \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int\<close>
where \<open>concat_bit n k l = take_bit n k OR push_bit n l\<close>
-lemma bit_concat_bit_iff:
+lemma bit_concat_bit_iff [bit_simps]:
\<open>bit (concat_bit m k l) n \<longleftrightarrow> n < m \<and> bit k n \<or> m \<le> n \<and> bit l (n - m)\<close>
by (simp add: concat_bit_def bit_or_iff bit_and_iff bit_take_bit_iff bit_push_bit_iff ac_simps)
@@ -1259,7 +1259,7 @@
\<open>even (signed_take_bit m a) \<longleftrightarrow> even a\<close>
by (auto simp add: signed_take_bit_def even_or_iff even_mask_iff bit_double_iff)
-lemma bit_signed_take_bit_iff:
+lemma bit_signed_take_bit_iff [bit_simps]:
\<open>bit (signed_take_bit m a) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> bit a (min m n)\<close>
by (simp add: signed_take_bit_def bit_take_bit_iff bit_or_iff bit_not_iff bit_mask_iff min_def not_le)
(use exp_eq_0_imp_not_bit in blast)
@@ -1560,11 +1560,11 @@
instance proof
fix m n q :: nat
show \<open>bit (m AND n) q \<longleftrightarrow> bit m q \<and> bit n q\<close>
- by (auto simp add: bit_nat_iff and_nat_def bit_and_iff less_le bit_eq_iff)
+ by (simp add: and_nat_def bit_simps)
show \<open>bit (m OR n) q \<longleftrightarrow> bit m q \<or> bit n q\<close>
- by (auto simp add: bit_nat_iff or_nat_def bit_or_iff less_le bit_eq_iff)
+ by (simp add: or_nat_def bit_simps)
show \<open>bit (m XOR n) q \<longleftrightarrow> bit m q \<noteq> bit n q\<close>
- by (auto simp add: bit_nat_iff xor_nat_def bit_xor_iff less_le bit_eq_iff)
+ by (simp add: xor_nat_def bit_simps)
qed (simp add: mask_nat_def)
end
--- a/src/HOL/Library/DAList.thy Sun Nov 15 22:04:16 2020 +0100
+++ b/src/HOL/Library/DAList.thy Sun Nov 15 22:26:13 2020 +0100
@@ -128,21 +128,21 @@
subsection \<open>Quickcheck generators\<close>
-definition (in term_syntax)
+context
+ includes state_combinator_syntax term_syntax
+begin
+
+definition
valterm_empty :: "('key :: typerep, 'value :: typerep) alist \<times> (unit \<Rightarrow> Code_Evaluation.term)"
where "valterm_empty = Code_Evaluation.valtermify empty"
-definition (in term_syntax)
+definition
valterm_update :: "'key :: typerep \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow>
'value :: typerep \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow>
('key, 'value) alist \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow>
('key, 'value) alist \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
[code_unfold]: "valterm_update k v a = Code_Evaluation.valtermify update {\<cdot>} k {\<cdot>} v {\<cdot>}a"
-context
- includes state_combinator_syntax
-begin
-
fun random_aux_alist
where
"random_aux_alist i j =
--- a/src/HOL/Library/FSet.thy Sun Nov 15 22:04:16 2020 +0100
+++ b/src/HOL/Library/FSet.thy Sun Nov 15 22:26:13 2020 +0100
@@ -1314,12 +1314,18 @@
notation Quickcheck_Exhaustive.orelse (infixr "orelse" 55)
-definition (in term_syntax) [code_unfold]:
+context
+ includes term_syntax
+begin
+
+definition [code_unfold]:
"valterm_femptyset = Code_Evaluation.valtermify ({||} :: ('a :: typerep) fset)"
-definition (in term_syntax) [code_unfold]:
+definition [code_unfold]:
"valtermify_finsert x s = Code_Evaluation.valtermify finsert {\<cdot>} (x :: ('a :: typerep * _)) {\<cdot>} s"
+end
+
instantiation fset :: (exhaustive) exhaustive
begin
--- a/src/HOL/Library/Float.thy Sun Nov 15 22:04:16 2020 +0100
+++ b/src/HOL/Library/Float.thy Sun Nov 15 22:26:13 2020 +0100
@@ -318,9 +318,15 @@
end
-definition (in term_syntax) [code_unfold]:
+context
+ includes term_syntax
+begin
+
+definition [code_unfold]:
"valtermify_float x y = Code_Evaluation.valtermify Float {\<cdot>} x {\<cdot>} y"
+end
+
instantiation float :: full_exhaustive
begin
--- a/src/HOL/Library/IArray.thy Sun Nov 15 22:04:16 2020 +0100
+++ b/src/HOL/Library/IArray.thy Sun Nov 15 22:26:13 2020 +0100
@@ -89,7 +89,8 @@
"IArray.all p = Not \<circ> IArray.exists (Not \<circ> p)"
by (simp add: fun_eq_iff)
-context term_syntax
+context
+ includes term_syntax
begin
lemma [code]:
--- a/src/HOL/Library/Interval.thy Sun Nov 15 22:04:16 2020 +0100
+++ b/src/HOL/Library/Interval.thy Sun Nov 15 22:26:13 2020 +0100
@@ -816,9 +816,15 @@
end
-definition (in term_syntax) [code_unfold]:
+context
+ includes term_syntax
+begin
+
+definition [code_unfold]:
"valtermify_interval x y = Code_Evaluation.valtermify (Ivl::'a::{preorder,typerep}\<Rightarrow>_) {\<cdot>} x {\<cdot>} y"
+end
+
instantiation interval :: ("{full_exhaustive,preorder,typerep}") full_exhaustive
begin
--- a/src/HOL/Library/Multiset.thy Sun Nov 15 22:04:16 2020 +0100
+++ b/src/HOL/Library/Multiset.thy Sun Nov 15 22:26:13 2020 +0100
@@ -3534,11 +3534,17 @@
text \<open>Quickcheck generators\<close>
-definition (in term_syntax)
+context
+ includes term_syntax
+begin
+
+definition
msetify :: "'a::typerep list \<times> (unit \<Rightarrow> Code_Evaluation.term)
\<Rightarrow> 'a multiset \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
[code_unfold]: "msetify xs = Code_Evaluation.valtermify mset {\<cdot>} xs"
+end
+
instantiation multiset :: (random) random
begin
--- a/src/HOL/Library/Word.thy Sun Nov 15 22:04:16 2020 +0100
+++ b/src/HOL/Library/Word.thy Sun Nov 15 22:26:13 2020 +0100
@@ -1065,7 +1065,7 @@
context semiring_bits
begin
-lemma bit_unsigned_iff:
+lemma bit_unsigned_iff [bit_simps]:
\<open>bit (unsigned w) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> bit w n\<close>
for w :: \<open>'b::len word\<close>
by (transfer fixing: bit) (simp add: bit_of_nat_iff bit_nat_iff bit_take_bit_iff)
@@ -1175,7 +1175,7 @@
context ring_bit_operations
begin
-lemma bit_signed_iff:
+lemma bit_signed_iff [bit_simps]:
\<open>bit (signed w) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> bit w (min (LENGTH('b) - Suc 0) n)\<close>
for w :: \<open>'b::len word\<close>
by (transfer fixing: bit)
@@ -1779,10 +1779,10 @@
\<open>shiftl1 = (*) 2\<close>
by (rule ext, transfer) simp
-lemma bit_shiftl1_iff:
+lemma bit_shiftl1_iff [bit_simps]:
\<open>bit (shiftl1 w) n \<longleftrightarrow> 0 < n \<and> n < LENGTH('a) \<and> bit w (n - 1)\<close>
for w :: \<open>'a::len word\<close>
- by (simp add: shiftl1_eq_mult_2 bit_double_iff exp_eq_zero_iff not_le) (simp add: ac_simps)
+ by (simp add: shiftl1_eq_mult_2 bit_double_iff not_le) (simp add: ac_simps)
lift_definition shiftr1 :: \<open>'a::len word \<Rightarrow> 'a word\<close>
\<comment> \<open>shift right as unsigned or as signed, ie logical or arithmetic\<close>
@@ -1793,7 +1793,7 @@
\<open>shiftr1 w = w div 2\<close>
by transfer simp
-lemma bit_shiftr1_iff:
+lemma bit_shiftr1_iff [bit_simps]:
\<open>bit (shiftr1 w) n \<longleftrightarrow> bit w (Suc n)\<close>
by transfer (auto simp flip: bit_Suc simp add: bit_take_bit_iff)
@@ -1820,7 +1820,7 @@
\<open>setBit w n = set_bit n w\<close>
by transfer simp
-lemma bit_setBit_iff:
+lemma bit_setBit_iff [bit_simps]:
\<open>bit (setBit w m) n \<longleftrightarrow> (m = n \<and> n < LENGTH('a) \<or> bit w n)\<close>
for w :: \<open>'a::len word\<close>
by transfer (auto simp add: bit_set_bit_iff)
@@ -1833,7 +1833,7 @@
\<open>clearBit w n = unset_bit n w\<close>
by transfer simp
-lemma bit_clearBit_iff:
+lemma bit_clearBit_iff [bit_simps]:
\<open>bit (clearBit w m) n \<longleftrightarrow> m \<noteq> n \<and> bit w n\<close>
for w :: \<open>'a::len word\<close>
by transfer (auto simp add: bit_unset_bit_iff)
@@ -1913,7 +1913,7 @@
using signed_take_bit_decr_length_iff
by (simp add: take_bit_drop_bit) force
-lemma bit_signed_drop_bit_iff:
+lemma bit_signed_drop_bit_iff [bit_simps]:
\<open>bit (signed_drop_bit m w) n \<longleftrightarrow> bit w (if LENGTH('a) - m \<le> n \<and> n < LENGTH('a) then LENGTH('a) - 1 else m + n)\<close>
for w :: \<open>'a::len word\<close>
apply transfer
@@ -2025,7 +2025,7 @@
by simp
qed
-lemma bit_word_rotr_iff:
+lemma bit_word_rotr_iff [bit_simps]:
\<open>bit (word_rotr m w) n \<longleftrightarrow>
n < LENGTH('a) \<and> bit w ((n + m) mod LENGTH('a))\<close>
for w :: \<open>'a::len word\<close>
@@ -2057,13 +2057,13 @@
by simp
qed
-lemma bit_word_rotl_iff:
+lemma bit_word_rotl_iff [bit_simps]:
\<open>bit (word_rotl m w) n \<longleftrightarrow>
n < LENGTH('a) \<and> bit w ((n + (LENGTH('a) - m mod LENGTH('a))) mod LENGTH('a))\<close>
for w :: \<open>'a::len word\<close>
by (simp add: word_rotl_eq_word_rotr bit_word_rotr_iff)
-lemma bit_word_roti_iff:
+lemma bit_word_roti_iff [bit_simps]:
\<open>bit (word_roti k w) n \<longleftrightarrow>
n < LENGTH('a) \<and> bit w (nat ((int n + k) mod int LENGTH('a)))\<close>
for w :: \<open>'a::len word\<close>
@@ -2130,7 +2130,7 @@
for a :: \<open>'a::len word\<close> and b :: \<open>'b::len word\<close>
by transfer (simp add: concat_bit_take_bit_eq)
-lemma bit_word_cat_iff:
+lemma bit_word_cat_iff [bit_simps]:
\<open>bit (word_cat v w :: 'c::len word) n \<longleftrightarrow> n < LENGTH('c) \<and> (if n < LENGTH('b) then bit w n else bit v (n - LENGTH('b)))\<close>
for v :: \<open>'a::len word\<close> and w :: \<open>'b::len word\<close>
by transfer (simp add: bit_concat_bit_iff bit_take_bit_iff)
@@ -3623,7 +3623,7 @@
lemmas word_and_le1 = xtrans(3) [OF word_ao_absorbs (4) [symmetric] le_word_or2]
lemmas word_and_le2 = xtrans(3) [OF word_ao_absorbs (8) [symmetric] le_word_or2]
-lemma bit_horner_sum_bit_word_iff:
+lemma bit_horner_sum_bit_word_iff [bit_simps]:
\<open>bit (horner_sum of_bool (2 :: 'a::len word) bs) n
\<longleftrightarrow> n < min LENGTH('a) (length bs) \<and> bs ! n\<close>
by transfer (simp add: bit_horner_sum_bit_iff)
@@ -3631,7 +3631,7 @@
definition word_reverse :: \<open>'a::len word \<Rightarrow> 'a word\<close>
where \<open>word_reverse w = horner_sum of_bool 2 (rev (map (bit w) [0..<LENGTH('a)]))\<close>
-lemma bit_word_reverse_iff:
+lemma bit_word_reverse_iff [bit_simps]:
\<open>bit (word_reverse w) n \<longleftrightarrow> n < LENGTH('a) \<and> bit w (LENGTH('a) - Suc n)\<close>
for w :: \<open>'a::len word\<close>
by (cases \<open>n < LENGTH('a)\<close>)
@@ -3698,7 +3698,7 @@
apply (simp add: drop_bit_take_bit min_def)
done
-lemma bit_sshiftr1_iff:
+lemma bit_sshiftr1_iff [bit_simps]:
\<open>bit (sshiftr1 w) n \<longleftrightarrow> bit w (if n = LENGTH('a) - 1 then LENGTH('a) - 1 else Suc n)\<close>
for w :: \<open>'a::len word\<close>
apply transfer
@@ -3714,7 +3714,7 @@
using sint_signed_drop_bit_eq [of 1 w]
by (simp add: drop_bit_Suc sshiftr1_eq_signed_drop_bit_Suc_0)
-lemma bit_bshiftr1_iff:
+lemma bit_bshiftr1_iff [bit_simps]:
\<open>bit (bshiftr1 b w) n \<longleftrightarrow> b \<and> n = LENGTH('a) - 1 \<or> bit w (Suc n)\<close>
for w :: \<open>'a::len word\<close>
apply transfer
@@ -3813,7 +3813,7 @@
context
begin
-qualified lemma bit_mask_iff:
+qualified lemma bit_mask_iff [bit_simps]:
\<open>bit (mask m :: 'a::len word) n \<longleftrightarrow> n < min LENGTH('a) m\<close>
by (simp add: bit_mask_iff exp_eq_zero_iff not_le)
@@ -3945,7 +3945,7 @@
then ucast (drop_bit (LENGTH('a) - n) w)
else push_bit (n - LENGTH('a)) (ucast w))\<close>
-lemma bit_slice1_iff:
+lemma bit_slice1_iff [bit_simps]:
\<open>bit (slice1 m w :: 'b::len word) n \<longleftrightarrow> m - LENGTH('a) \<le> n \<and> n < min LENGTH('b) m
\<and> bit w (n + (LENGTH('a) - m) - (m - LENGTH('a)))\<close>
for w :: \<open>'a::len word\<close>
@@ -3955,7 +3955,7 @@
definition slice :: \<open>nat \<Rightarrow> 'a::len word \<Rightarrow> 'b::len word\<close>
where \<open>slice n = slice1 (LENGTH('a) - n)\<close>
-lemma bit_slice_iff:
+lemma bit_slice_iff [bit_simps]:
\<open>bit (slice m w :: 'b::len word) n \<longleftrightarrow> n < min LENGTH('b) (LENGTH('a) - m) \<and> bit w (n + LENGTH('a) - (LENGTH('a) - m))\<close>
for w :: \<open>'a::len word\<close>
by (simp add: slice_def word_size bit_slice1_iff)
@@ -4008,7 +4008,7 @@
definition revcast :: \<open>'a::len word \<Rightarrow> 'b::len word\<close>
where \<open>revcast = slice1 LENGTH('b)\<close>
-lemma bit_revcast_iff:
+lemma bit_revcast_iff [bit_simps]:
\<open>bit (revcast w :: 'b::len word) n \<longleftrightarrow> LENGTH('b) - LENGTH('a) \<le> n \<and> n < LENGTH('b)
\<and> bit w (n + (LENGTH('a) - LENGTH('b)) - (LENGTH('b) - LENGTH('a)))\<close>
for w :: \<open>'a::len word\<close>
--- a/src/HOL/Parity.thy Sun Nov 15 22:04:16 2020 +0100
+++ b/src/HOL/Parity.thy Sun Nov 15 22:26:13 2020 +0100
@@ -906,15 +906,17 @@
\<open>a = b \<longleftrightarrow> (\<forall>n. bit a n \<longleftrightarrow> bit b n)\<close>
by (auto intro: bit_eqI)
-lemma bit_exp_iff:
+named_theorems bit_simps \<open>Simplification rules for \<^const>\<open>bit\<close>\<close>
+
+lemma bit_exp_iff [bit_simps]:
\<open>bit (2 ^ m) n \<longleftrightarrow> 2 ^ m \<noteq> 0 \<and> m = n\<close>
by (auto simp add: bit_iff_odd exp_div_exp_eq)
-lemma bit_1_iff:
+lemma bit_1_iff [bit_simps]:
\<open>bit 1 n \<longleftrightarrow> 1 \<noteq> 0 \<and> n = 0\<close>
using bit_exp_iff [of 0 n] by simp
-lemma bit_2_iff:
+lemma bit_2_iff [bit_simps]:
\<open>bit 2 n \<longleftrightarrow> 2 \<noteq> 0 \<and> n = 1\<close>
using bit_exp_iff [of 1 n] by auto
@@ -931,7 +933,7 @@
ultimately show ?thesis by (simp add: ac_simps)
qed
-lemma bit_double_iff:
+lemma bit_double_iff [bit_simps]:
\<open>bit (2 * a) n \<longleftrightarrow> bit a (n - 1) \<and> n \<noteq> 0 \<and> 2 ^ n \<noteq> 0\<close>
using even_mult_exp_div_exp_iff [of a 1 n]
by (cases n, auto simp add: bit_iff_odd ac_simps)
@@ -1193,7 +1195,7 @@
context semiring_bits
begin
-lemma bit_of_bool_iff:
+lemma bit_of_bool_iff [bit_simps]:
\<open>bit (of_bool b) n \<longleftrightarrow> b \<and> n = 0\<close>
by (simp add: bit_1_iff)
@@ -1201,7 +1203,7 @@
\<open>even (of_nat n) \<longleftrightarrow> even n\<close>
by (induction n rule: nat_bit_induct) simp_all
-lemma bit_of_nat_iff:
+lemma bit_of_nat_iff [bit_simps]:
\<open>bit (of_nat m) n \<longleftrightarrow> (2::'a) ^ n \<noteq> 0 \<and> bit m n\<close>
proof (cases \<open>(2::'a) ^ n = 0\<close>)
case True
@@ -1492,15 +1494,15 @@
\<open>even (push_bit n a) \<longleftrightarrow> n \<noteq> 0 \<or> even a\<close>
by (simp add: push_bit_eq_mult) auto
-lemma bit_push_bit_iff:
+lemma bit_push_bit_iff [bit_simps]:
\<open>bit (push_bit m a) n \<longleftrightarrow> m \<le> n \<and> 2 ^ n \<noteq> 0 \<and> bit a (n - m)\<close>
by (auto simp add: bit_iff_odd push_bit_eq_mult even_mult_exp_div_exp_iff)
-lemma bit_drop_bit_eq:
+lemma bit_drop_bit_eq [bit_simps]:
\<open>bit (drop_bit n a) = bit a \<circ> (+) n\<close>
by (simp add: bit_iff_odd fun_eq_iff ac_simps flip: drop_bit_eq_div)
-lemma bit_take_bit_iff:
+lemma bit_take_bit_iff [bit_simps]:
\<open>bit (take_bit m a) n \<longleftrightarrow> n < m \<and> bit a n\<close>
by (simp add: bit_iff_odd drop_bit_take_bit not_le flip: drop_bit_eq_div)
@@ -1763,7 +1765,7 @@
"drop_bit n (of_nat m) = of_nat (drop_bit n m)"
by (simp add: drop_bit_eq_div Parity.drop_bit_eq_div of_nat_div [of m "2 ^ n"])
-lemma bit_of_nat_iff_bit [simp]:
+lemma bit_of_nat_iff_bit [bit_simps]:
\<open>bit (of_nat m) n \<longleftrightarrow> bit m n\<close>
proof -
have \<open>even (m div 2 ^ n) \<longleftrightarrow> even (of_nat (m div 2 ^ n))\<close>
@@ -1778,7 +1780,7 @@
\<open>of_nat (drop_bit m n) = drop_bit m (of_nat n)\<close>
by (simp add: drop_bit_eq_div semiring_bit_shifts_class.drop_bit_eq_div of_nat_div)
-lemma bit_push_bit_iff_of_nat_iff:
+lemma bit_push_bit_iff_of_nat_iff [bit_simps]:
\<open>bit (push_bit m (of_nat r)) n \<longleftrightarrow> m \<le> n \<and> bit (of_nat r) (n - m)\<close>
by (auto simp add: bit_push_bit_iff)
@@ -1826,12 +1828,12 @@
by (simp add: bit_Suc)
qed
-lemma bit_minus_int_iff:
+lemma bit_minus_int_iff [bit_simps]:
\<open>bit (- k) n \<longleftrightarrow> \<not> bit (k - 1) n\<close>
for k :: int
using bit_not_int_iff' [of \<open>k - 1\<close>] by simp
-lemma bit_nat_iff:
+lemma bit_nat_iff [bit_simps]:
\<open>bit (nat k) n \<longleftrightarrow> k \<ge> 0 \<and> bit k n\<close>
proof (cases \<open>k \<ge> 0\<close>)
case True
@@ -1839,7 +1841,7 @@
ultimately have \<open>k = int m\<close>
by simp
then show ?thesis
- by (auto intro: ccontr)
+ by (simp add: bit_simps)
next
case False
then show ?thesis
--- a/src/HOL/Probability/PMF_Impl.thy Sun Nov 15 22:04:16 2020 +0100
+++ b/src/HOL/Probability/PMF_Impl.thy Sun Nov 15 22:26:13 2020 +0100
@@ -530,22 +530,22 @@
definition single :: "'a \<Rightarrow> 'a multiset" where
"single s = {#s#}"
-definition (in term_syntax)
- pmfify :: "('a::typerep multiset \<times> (unit \<Rightarrow> Code_Evaluation.term)) \<Rightarrow>
- 'a \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow>
- 'a pmf \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
+instantiation pmf :: (random) random
+begin
+
+context
+ includes state_combinator_syntax term_syntax
+begin
+
+definition
+ pmfify :: "('b::typerep multiset \<times> (unit \<Rightarrow> Code_Evaluation.term)) \<Rightarrow>
+ 'b \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow>
+ 'b pmf \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
[code_unfold]: "pmfify A x =
Code_Evaluation.valtermify pmf_of_multiset {\<cdot>}
(Code_Evaluation.valtermify (+) {\<cdot>} A {\<cdot>}
(Code_Evaluation.valtermify single {\<cdot>} x))"
-instantiation pmf :: (random) random
-begin
-
-context
- includes state_combinator_syntax
-begin
-
definition
"Quickcheck_Random.random i =
Quickcheck_Random.random i \<circ>\<rightarrow> (\<lambda>A.
--- a/src/HOL/Quickcheck_Exhaustive.thy Sun Nov 15 22:04:16 2020 +0100
+++ b/src/HOL/Quickcheck_Exhaustive.thy Sun Nov 15 22:26:13 2020 +0100
@@ -180,10 +180,16 @@
end
-definition (in term_syntax)
+context
+ includes term_syntax
+begin
+
+definition
[code_unfold]: "valtermify_pair x y =
Code_Evaluation.valtermify (Pair :: 'a::typerep \<Rightarrow> 'b::typerep \<Rightarrow> 'a \<times> 'b) {\<cdot>} x {\<cdot>} y"
+end
+
instantiation prod :: (full_exhaustive, full_exhaustive) full_exhaustive
begin
@@ -253,11 +259,17 @@
(\<lambda>_::'a. v,
\<lambda>u::unit. Code_Evaluation.Abs (STR ''x'') (Typerep.typerep TYPE('a::typerep)) (t ())))"
-definition (in term_syntax)
+context
+ includes term_syntax
+begin
+
+definition
[code_unfold]: "valtermify_fun_upd g a b =
Code_Evaluation.valtermify
(fun_upd :: ('a::typerep \<Rightarrow> 'b::typerep) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b) {\<cdot>} g {\<cdot>} a {\<cdot>} b"
+end
+
instantiation "fun" :: ("{equal,full_exhaustive}", full_exhaustive) full_exhaustive
begin
@@ -296,11 +308,17 @@
else check_all (\<lambda>(x, xt).
check_all_n_lists (\<lambda>(xs, xst). f ((x # xs), (\<lambda>_. (xt () # xst ())))) (n - 1)))"
-definition (in term_syntax)
+context
+ includes term_syntax
+begin
+
+definition
[code_unfold]: "termify_fun_upd g a b =
(Code_Evaluation.termify
(fun_upd :: ('a::typerep \<Rightarrow> 'b::typerep) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b) <\<cdot>> g <\<cdot>> a <\<cdot>> b)"
+end
+
definition mk_map_term ::
"(unit \<Rightarrow> typerep) \<Rightarrow> (unit \<Rightarrow> typerep) \<Rightarrow>
(unit \<Rightarrow> term list) \<Rightarrow> (unit \<Rightarrow> term list) \<Rightarrow> unit \<Rightarrow> term"
@@ -357,7 +375,11 @@
end
-fun (in term_syntax) check_all_subsets ::
+context
+ includes term_syntax
+begin
+
+fun check_all_subsets ::
"(('a::typerep) set \<times> (unit \<Rightarrow> term) \<Rightarrow> (bool \<times> term list) option) \<Rightarrow>
('a \<times> (unit \<Rightarrow> term)) list \<Rightarrow> (bool \<times> term list) option"
where
@@ -365,18 +387,19 @@
| "check_all_subsets f (x # xs) =
check_all_subsets (\<lambda>s. case f s of Some ts \<Rightarrow> Some ts | None \<Rightarrow> f (valtermify_insert x s)) xs"
-
-definition (in term_syntax)
+definition
[code_unfold]: "term_emptyset = Code_Evaluation.termify ({} :: ('a::typerep) set)"
-definition (in term_syntax)
+definition
[code_unfold]: "termify_insert x s =
Code_Evaluation.termify (insert :: ('a::typerep) \<Rightarrow> 'a set \<Rightarrow> 'a set) <\<cdot>> x <\<cdot>> s"
-definition (in term_syntax) setify :: "('a::typerep) itself \<Rightarrow> term list \<Rightarrow> term"
+definition setify :: "('a::typerep) itself \<Rightarrow> term list \<Rightarrow> term"
where
"setify T ts = foldr (termify_insert T) ts (term_emptyset T)"
+end
+
instantiation set :: (check_all) check_all
begin
@@ -423,10 +446,16 @@
end
-definition (in term_syntax) [code_unfold]:
+context
+ includes term_syntax
+begin
+
+definition [code_unfold]:
"termify_pair x y =
Code_Evaluation.termify (Pair :: 'a::typerep \<Rightarrow> 'b :: typerep \<Rightarrow> 'a * 'b) <\<cdot>> x <\<cdot>> y"
+end
+
instantiation prod :: (check_all, check_all) check_all
begin
@@ -442,14 +471,20 @@
end
-definition (in term_syntax)
+context
+ includes term_syntax
+begin
+
+definition
[code_unfold]: "valtermify_Inl x =
Code_Evaluation.valtermify (Inl :: 'a::typerep \<Rightarrow> 'a + 'b :: typerep) {\<cdot>} x"
-definition (in term_syntax)
+definition
[code_unfold]: "valtermify_Inr x =
Code_Evaluation.valtermify (Inr :: 'b::typerep \<Rightarrow> 'a::typerep + 'b) {\<cdot>} x"
+end
+
instantiation sum :: (check_all, check_all) check_all
begin
--- a/src/HOL/Quickcheck_Random.thy Sun Nov 15 22:04:16 2020 +0100
+++ b/src/HOL/Quickcheck_Random.thy Sun Nov 15 22:26:13 2020 +0100
@@ -201,13 +201,18 @@
lemma beyond_zero: "beyond k 0 = 0"
by (simp add: beyond_def)
+context
+ includes term_syntax
+begin
-definition (in term_syntax) [code_unfold]:
+definition [code_unfold]:
"valterm_emptyset = Code_Evaluation.valtermify ({} :: ('a :: typerep) set)"
-definition (in term_syntax) [code_unfold]:
+definition [code_unfold]:
"valtermify_insert x s = Code_Evaluation.valtermify insert {\<cdot>} (x :: ('a :: typerep * _)) {\<cdot>} s"
+end
+
instantiation set :: (random) random
begin
--- a/src/HOL/Rat.thy Sun Nov 15 22:04:16 2020 +0100
+++ b/src/HOL/Rat.thy Sun Nov 15 22:26:13 2020 +0100
@@ -998,12 +998,18 @@
text \<open>Quickcheck\<close>
-definition (in term_syntax)
+context
+ includes term_syntax
+begin
+
+definition
valterm_fract :: "int \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow>
int \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow>
rat \<times> (unit \<Rightarrow> Code_Evaluation.term)"
where [code_unfold]: "valterm_fract k l = Code_Evaluation.valtermify Fract {\<cdot>} k {\<cdot>} l"
+end
+
instantiation rat :: random
begin
--- a/src/HOL/Real.thy Sun Nov 15 22:04:16 2020 +0100
+++ b/src/HOL/Real.thy Sun Nov 15 22:26:13 2020 +0100
@@ -1634,10 +1634,16 @@
text \<open>Quickcheck\<close>
-definition (in term_syntax)
+context
+ includes term_syntax
+begin
+
+definition
valterm_ratreal :: "rat \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow> real \<times> (unit \<Rightarrow> Code_Evaluation.term)"
where [code_unfold]: "valterm_ratreal k = Code_Evaluation.valtermify Ratreal {\<cdot>} k"
+end
+
instantiation real :: random
begin
--- a/src/HOL/Set.thy Sun Nov 15 22:04:16 2020 +0100
+++ b/src/HOL/Set.thy Sun Nov 15 22:26:13 2020 +0100
@@ -383,7 +383,7 @@
unfolding Bex_def by blast
lemma ball_triv [simp]: "(\<forall>x\<in>A. P) \<longleftrightarrow> ((\<exists>x. x \<in> A) \<longrightarrow> P)"
- \<comment> \<open>Trival rewrite rule.\<close>
+ \<comment> \<open>trivial rewrite rule.\<close>
by (simp add: Ball_def)
lemma bex_triv [simp]: "(\<exists>x\<in>A. P) \<longleftrightarrow> ((\<exists>x. x \<in> A) \<and> P)"
--- a/src/HOL/String.thy Sun Nov 15 22:04:16 2020 +0100
+++ b/src/HOL/String.thy Sun Nov 15 22:26:13 2020 +0100
@@ -121,7 +121,7 @@
lemma char_of_nat [simp]:
\<open>char_of (of_nat n) = char_of n\<close>
- by (simp add: char_of_def String.char_of_def drop_bit_of_nat)
+ by (simp add: char_of_def String.char_of_def drop_bit_of_nat bit_simps)
end
--- a/src/Pure/Isar/bundle.ML Sun Nov 15 22:04:16 2020 +0100
+++ b/src/Pure/Isar/bundle.ML Sun Nov 15 22:26:13 2020 +0100
@@ -6,8 +6,9 @@
signature BUNDLE =
sig
+ type name = string
val check: Proof.context -> xstring * Position.T -> string
- val get: Proof.context -> string -> Attrib.thms
+ val get: Proof.context -> name -> Attrib.thms
val read: Proof.context -> xstring * Position.T -> Attrib.thms
val print_bundles: bool -> Proof.context -> unit
val bundle: binding * Attrib.thms ->
@@ -15,13 +16,13 @@
val bundle_cmd: binding * (Facts.ref * Token.src list) list ->
(binding * string option * mixfix) list -> local_theory -> local_theory
val init: binding -> theory -> local_theory
- val unbundle: string list -> local_theory -> local_theory
+ val unbundle: name list -> local_theory -> local_theory
val unbundle_cmd: (xstring * Position.T) list -> local_theory -> local_theory
- val includes: string list -> Proof.context -> Proof.context
+ val includes: name list -> Proof.context -> Proof.context
val includes_cmd: (xstring * Position.T) list -> Proof.context -> Proof.context
- val include_: string list -> Proof.state -> Proof.state
+ val include_: name list -> Proof.state -> Proof.state
val include_cmd: (xstring * Position.T) list -> Proof.state -> Proof.state
- val including: string list -> Proof.state -> Proof.state
+ val including: name list -> Proof.state -> Proof.state
val including_cmd: (xstring * Position.T) list -> Proof.state -> Proof.state
end;
@@ -42,6 +43,8 @@
(* bundles *)
+type name = string
+
val get_all_generic = #1 o Data.get;
val get_all = get_all_generic o Context.Proof;
--- a/src/Pure/Isar/class_declaration.ML Sun Nov 15 22:04:16 2020 +0100
+++ b/src/Pure/Isar/class_declaration.ML Sun Nov 15 22:26:13 2020 +0100
@@ -6,7 +6,7 @@
signature CLASS_DECLARATION =
sig
- val class: binding -> string list -> class list ->
+ val class: binding -> Bundle.name list -> class list ->
Element.context_i list -> theory -> string * local_theory
val class_cmd: binding -> (xstring * Position.T) list -> xstring list ->
Element.context list -> theory -> string * local_theory
--- a/src/Pure/Isar/expression.ML Sun Nov 15 22:04:16 2020 +0100
+++ b/src/Pure/Isar/expression.ML Sun Nov 15 22:26:13 2020 +0100
@@ -32,7 +32,7 @@
val read_declaration: expression -> (Proof.context -> Proof.context) -> Element.context list ->
Proof.context -> (((string * typ) * mixfix) list * (string * morphism) list
* Element.context_i list * Proof.context) * ((string * typ) list * Proof.context)
- val add_locale: binding -> binding -> string list ->
+ val add_locale: binding -> binding -> Bundle.name list ->
expression_i -> Element.context_i list -> theory -> string * local_theory
val add_locale_cmd: binding -> binding -> (xstring * Position.T) list ->
expression -> Element.context list -> theory -> string * local_theory
--- a/src/Pure/Isar/named_target.ML Sun Nov 15 22:04:16 2020 +0100
+++ b/src/Pure/Isar/named_target.ML Sun Nov 15 22:26:13 2020 +0100
@@ -11,7 +11,7 @@
val locale_of: local_theory -> string option
val bottom_locale_of: local_theory -> string option
val class_of: local_theory -> string option
- val init: string list -> string -> theory -> local_theory
+ val init: Bundle.name list -> string -> theory -> local_theory
val theory_init: theory -> local_theory
val theory_map: (local_theory -> local_theory) -> theory -> theory
val theory_map_result: (morphism -> 'a -> 'b) -> (local_theory -> 'a * local_theory) ->