--- a/ANNOUNCE Sun Jul 01 10:58:14 2018 +0200
+++ b/ANNOUNCE Sun Jul 01 17:38:08 2018 +0200
@@ -4,9 +4,25 @@
Isabelle2018 is now available.
This version introduces many changes over Isabelle2017: see the NEWS
-file for further details. Some notable points:
+file for further details. Here are the main points:
+
+* Improved infix notation within terms.
+
+* Improved syntax for formal comments, within terms and other languages.
+
+* Improved management of ROOT files and session-qualified theories.
+
+* Various improvements of document preparation.
-* FIXME.
+* Many Isabelle/jEdit improvements, including semantic IDE for Bibtex.
+
+* Numerous HOL library improvements, including HOL-Algebra.
+
+* Substantial additions to HOL-Analysis.
+
+* Isabelle server for reactive communication with other programs.
+
+* More uniform 64-bit platform support: smaller Isabelle application.
You may get Isabelle2018 from the following mirror sites:
--- a/Admin/Release/CHECKLIST Sun Jul 01 10:58:14 2018 +0200
+++ b/Admin/Release/CHECKLIST Sun Jul 01 17:38:08 2018 +0200
@@ -5,6 +5,14 @@
- check Admin/components;
+- test "isabelle dump -l Pure ZF";
+
+- test "isabelle -o export_theory -f ZF";
+
+- test "isabelle server" according to "system" manual;
+
+- test Isabelle/VSCode;
+
- test Isabelle/jEdit: print buffer
- test "#!/usr/bin/env isabelle_scala_script";
--- a/CONTRIBUTORS Sun Jul 01 10:58:14 2018 +0200
+++ b/CONTRIBUTORS Sun Jul 01 17:38:08 2018 +0200
@@ -12,6 +12,13 @@
* June 2018: Martin Baillon and Paulo Emílio de Vilhena
A variety of contributions to HOL-Algebra.
+* June 2018: Wenda Li
+ New/strengthened results involving analysis, topology, etc.
+
+* May/June 2018: Makarius Wenzel
+ System infrastructure to export blobs as theory presentation, and to dump
+ PIDE database content in batch mode.
+
* May 2018: Manuel Eberl
Landau symbols and asymptotic equivalence (moved from the AFP).
@@ -34,6 +41,10 @@
* March 2018: Viorel Preoteasa
Generalisation of complete_distrib_lattice
+* February 2018: Wenda Li
+ A unified definition for the order of zeros and poles. Improved reasoning
+ around non-essential singularities.
+
* January 2018: Sebastien Gouezel
Various small additions to HOL-Analysis
--- a/NEWS Sun Jul 01 10:58:14 2018 +0200
+++ b/NEWS Sun Jul 01 17:38:08 2018 +0200
@@ -19,6 +19,11 @@
FOL, ZF, ZFC etc. INCOMPATIBILITY, need to use qualified names for
formerly global "HOL-Probability.Probability" and "HOL-SPARK.SPARK".
+* Global facts need to be closed: no free variables, no hypotheses, no
+pending sort hypotheses. Rare INCOMPATIBILITY: sort hypotheses can be
+allowed via "declare [[pending_shyps]]" in the global theory context,
+but it should be reset to false afterwards.
+
* Marginal comments need to be written exclusively in the new-style form
"\<comment> \<open>text\<close>", old ASCII variants like "-- {* ... *}" are no longer
supported. INCOMPATIBILITY, use the command-line tool "isabelle
@@ -31,13 +36,13 @@
* The "op <infix-op>" syntax for infix operators has been replaced by
"(<infix-op>)". If <infix-op> begins or ends with a "*", there needs to
be a space between the "*" and the corresponding parenthesis.
-INCOMPATIBILITY.
-There is an Isabelle tool "update_op" that converts theory and ML files
-to the new syntax. Because it is based on regular expression matching,
-the result may need a bit of manual postprocessing. Invoking "isabelle
-update_op" converts all files in the current directory (recursively).
-In case you want to exclude conversion of ML files (because the tool
-frequently also converts ML's "op" syntax), use option "-m".
+INCOMPATIBILITY, use the command-line tool "isabelle update_op" to
+convert theory and ML files to the new syntax. Because it is based on
+regular expression matching, the result may need a bit of manual
+postprocessing. Invoking "isabelle update_op" converts all files in the
+current directory (recursively). In case you want to exclude conversion
+of ML files (because the tool frequently also converts ML's "op"
+syntax), use option "-m".
* Theory header 'abbrevs' specifications need to be separated by 'and'.
INCOMPATIBILITY.
@@ -80,11 +85,15 @@
- option -A specifies an alternative ancestor session for options -R
and -S
+ - option -i includes additional sessions into the name-space of
+ theories
+
Examples:
isabelle jedit -R HOL-Number_Theory
isabelle jedit -R HOL-Number_Theory -A HOL
isabelle jedit -d '$AFP' -S Formal_SSA -A HOL
isabelle jedit -d '$AFP' -S Formal_SSA -A HOL-Analysis
+ isabelle jedit -d '$AFP' -S Formal_SSA -A HOL-Analysis -i CryptHOL
* PIDE markup for session ROOT files: allows to complete session names,
follow links to theories and document files etc.
@@ -119,14 +128,14 @@
plain-text document draft. Both are available via the menu "Plugins /
Isabelle".
-* Bibtex database files (.bib) are semantically checked.
-
* When loading text files, the Isabelle symbols encoding UTF-8-Isabelle
is only used if there is no conflict with existing Unicode sequences in
the file. Otherwise, the fallback encoding is plain UTF-8 and Isabelle
symbols remain in literal \<symbol> form. This avoids accidental loss of
Unicode content when saving the file.
+* Bibtex database files (.bib) are semantically checked.
+
* Update to jedit-5.5.0, the latest release.
@@ -198,6 +207,12 @@
Isbelle2016-1). INCOMPATIBILITY, use 'define' instead -- usually with
object-logic equality or equivalence.
+
+*** Pure ***
+
+* The inner syntax category "sort" now includes notation "_" for the
+dummy sort: it is effectively ignored in type-inference.
+
* Rewrites clauses (keyword 'rewrites') were moved into the locale
expression syntax, where they are part of locale instances. In
interpretation commands rewrites clauses now need to occur before 'for'
@@ -209,17 +224,11 @@
locale instances where the qualifier's sole purpose is avoiding
duplicate constant declarations.
-* Proof method 'simp' now supports a new modifier 'flip:' followed by a list
-of theorems. Each of these theorems is removed from the simpset
-(without warning if it is not there) and the symmetric version of the theorem
-(i.e. lhs and rhs exchanged) is added to the simpset.
-For 'auto' and friends the modifier is "simp flip:".
-
-
-*** Pure ***
-
-* The inner syntax category "sort" now includes notation "_" for the
-dummy sort: it is effectively ignored in type-inference.
+* Proof method "simp" now supports a new modifier "flip:" followed by a
+list of theorems. Each of these theorems is removed from the simpset
+(without warning if it is not there) and the symmetric version of the
+theorem (i.e. lhs and rhs exchanged) is added to the simpset. For "auto"
+and friends the modifier is "simp flip:".
*** HOL ***
@@ -382,22 +391,25 @@
* Session HOL-Algebra: renamed (^) to [^] to avoid conflict with new
infix/prefix notation.
-* Session HOL-Algebra: Revamped with much new material.
-The set of isomorphisms between two groups is now denoted iso rather than iso_set.
-INCOMPATIBILITY.
-
-* Session HOL-Analysis: the Arg function now respects the same interval as
-Ln, namely (-pi,pi]; the old Arg function has been renamed Arg2pi.
+* Session HOL-Algebra: revamped with much new material. The set of
+isomorphisms between two groups is now denoted iso rather than iso_set.
+INCOMPATIBILITY.
+
+* Session HOL-Analysis: the Arg function now respects the same interval
+as Ln, namely (-pi,pi]; the old Arg function has been renamed Arg2pi.
+INCOMPATIBILITY.
+
+* Session HOL-Analysis: the functions zorder, zer_poly, porder and
+pol_poly have been redefined. All related lemmas have been reworked.
INCOMPATIBILITY.
* Session HOL-Analysis: infinite products, Moebius functions, the
Riemann mapping theorem, the Vitali covering theorem,
change-of-variables results for integration and measures.
-* Session HOL-Types_To_Sets: more tool support
-(unoverload_type combines internalize_sorts and unoverload) and larger
-experimental application (type based linear algebra transferred to linear
-algebra on subspaces).
+* Session HOL-Types_To_Sets: more tool support (unoverload_type combines
+internalize_sorts and unoverload) and larger experimental application
+(type based linear algebra transferred to linear algebra on subspaces).
*** ML ***
--- a/src/Doc/Implementation/Logic.thy Sun Jul 01 10:58:14 2018 +0200
+++ b/src/Doc/Implementation/Logic.thy Sun Jul 01 17:38:08 2018 +0200
@@ -862,9 +862,13 @@
class empty =
assumes bad: "\<And>(x::'a) y. x \<noteq> y"
+declare [[pending_shyps]]
+
theorem (in empty) false: False
using bad by blast
+declare [[pending_shyps = false]]
+
ML_val \<open>@{assert} (Thm.extra_shyps @{thm false} = [@{sort empty}])\<close>
text \<open>
--- a/src/Doc/JEdit/JEdit.thy Sun Jul 01 10:58:14 2018 +0200
+++ b/src/Doc/JEdit/JEdit.thy Sun Jul 01 17:38:08 2018 +0200
@@ -237,6 +237,7 @@
-b build only
-d DIR include session directory
-f fresh build
+ -i NAME include session in name-space of theories
-j OPTION add jEdit runtime option
(default $JEDIT_OPTIONS)
-l NAME logic image name
@@ -266,6 +267,9 @@
ancestor session for options \<^verbatim>\<open>-R\<close> and \<^verbatim>\<open>-S\<close>: this allows to restructure the
hierarchy of session images on the spot.
+ The \<^verbatim>\<open>-i\<close> option includes additional sessions into the name-space of
+ theories: multiple occurrences are possible.
+
The \<^verbatim>\<open>-m\<close> option specifies additional print modes for the prover process.
Note that the system option @{system_option_ref jedit_print_mode} allows to
do the same persistently (e.g.\ via the \<^emph>\<open>Plugin Options\<close> dialog of
--- a/src/Doc/System/Environment.thy Sun Jul 01 10:58:14 2018 +0200
+++ b/src/Doc/System/Environment.thy Sun Jul 01 17:38:08 2018 +0200
@@ -407,6 +407,7 @@
Options are:
-d DIR include session directory
+ -i NAME include session in name-space of theories
-l NAME logic session name (default ISABELLE_LOGIC)
-m MODE add print mode for output
-n no build of session image on startup
@@ -421,6 +422,9 @@
Option \<^verbatim>\<open>-l\<close> specifies the logic session name. By default, its heap image is
checked and built on demand, but the option \<^verbatim>\<open>-n\<close> skips that.
+ Option \<^verbatim>\<open>-i\<close> includes additional sessions into the name-space of theories:
+ multiple occurrences are possible.
+
Option \<^verbatim>\<open>-r\<close> indicates a bootstrap from the raw Poly/ML system, which is
relevant for Isabelle/Pure development.
--- a/src/FOL/ex/Miniscope.thy Sun Jul 01 10:58:14 2018 +0200
+++ b/src/FOL/ex/Miniscope.thy Sun Jul 01 17:38:08 2018 +0200
@@ -17,14 +17,19 @@
subsubsection \<open>de Morgan laws\<close>
-lemma demorgans:
+lemma demorgans1:
"\<not> (P \<and> Q) \<longleftrightarrow> \<not> P \<or> \<not> Q"
"\<not> (P \<or> Q) \<longleftrightarrow> \<not> P \<and> \<not> Q"
"\<not> \<not> P \<longleftrightarrow> P"
+ by blast+
+
+lemma demorgans2:
"\<And>P. \<not> (\<forall>x. P(x)) \<longleftrightarrow> (\<exists>x. \<not> P(x))"
"\<And>P. \<not> (\<exists>x. P(x)) \<longleftrightarrow> (\<forall>x. \<not> P(x))"
by blast+
+lemmas demorgans = demorgans1 demorgans2
+
(*** Removal of --> and <-> (positive and negative occurrences) ***)
(*Last one is important for computing a compact CNF*)
lemma nnf_simps:
--- a/src/HOL/Algebra/Divisibility.thy Sun Jul 01 10:58:14 2018 +0200
+++ b/src/HOL/Algebra/Divisibility.thy Sun Jul 01 17:38:08 2018 +0200
@@ -763,6 +763,27 @@
apply (metis pp' associated_sym divides_cong_l)
done
+(*by Paulo Emílio de Vilhena*)
+lemma (in comm_monoid_cancel) prime_irreducible:
+ assumes "prime G p"
+ shows "irreducible G p"
+proof (rule irreducibleI)
+ show "p \<notin> Units G"
+ using assms unfolding prime_def by simp
+next
+ fix b assume A: "b \<in> carrier G" "properfactor G b p"
+ then obtain c where c: "c \<in> carrier G" "p = b \<otimes> c"
+ unfolding properfactor_def factor_def by auto
+ hence "p divides c"
+ using A assms unfolding prime_def properfactor_def by auto
+ then obtain b' where b': "b' \<in> carrier G" "c = p \<otimes> b'"
+ unfolding factor_def by auto
+ hence "\<one> = b \<otimes> b'"
+ by (metis A(1) l_cancel m_closed m_lcomm one_closed r_one c)
+ thus "b \<in> Units G"
+ using A(1) Units_one_closed b'(1) unit_factor by presburger
+qed
+
subsection \<open>Factorization and Factorial Monoids\<close>
--- a/src/HOL/Algebra/Group.thy Sun Jul 01 10:58:14 2018 +0200
+++ b/src/HOL/Algebra/Group.thy Sun Jul 01 17:38:08 2018 +0200
@@ -1438,6 +1438,9 @@
shows "m_inv (units_of G) x = m_inv G x"
by (simp add: assms group.inv_equality units_group units_of_carrier units_of_mult units_of_one)
+lemma units_of_units [simp] : "Units (units_of G) = Units G"
+ unfolding units_of_def Units_def by force
+
lemma (in group) surj_const_mult: "a \<in> carrier G \<Longrightarrow> (\<lambda>x. a \<otimes> x) ` carrier G = carrier G"
apply (auto simp add: image_def)
by (metis inv_closed inv_solve_left m_closed)
--- a/src/HOL/Algebra/Module.thy Sun Jul 01 10:58:14 2018 +0200
+++ b/src/HOL/Algebra/Module.thy Sun Jul 01 17:38:08 2018 +0200
@@ -1,6 +1,6 @@
(* Title: HOL/Algebra/Module.thy
Author: Clemens Ballarin, started 15 April 2003
- Copyright: Clemens Ballarin
+ with contributions by Martin Baillon
*)
theory Module
@@ -76,87 +76,95 @@
"!!a x y. [| a \<in> carrier R; x \<in> carrier M; y \<in> carrier M |] ==>
(a \<odot>\<^bsub>M\<^esub> x) \<otimes>\<^bsub>M\<^esub> y = a \<odot>\<^bsub>M\<^esub> (x \<otimes>\<^bsub>M\<^esub> y)"
shows "algebra R M"
-apply intro_locales
-apply (rule cring.axioms ring.axioms abelian_group.axioms comm_monoid.axioms assms)+
-apply (rule module_axioms.intro)
- apply (simp add: smult_closed)
- apply (simp add: smult_l_distr)
- apply (simp add: smult_r_distr)
- apply (simp add: smult_assoc1)
- apply (simp add: smult_one)
-apply (rule cring.axioms ring.axioms abelian_group.axioms comm_monoid.axioms assms)+
-apply (rule algebra_axioms.intro)
- apply (simp add: smult_assoc2)
-done
+ apply intro_locales
+ apply (rule cring.axioms ring.axioms abelian_group.axioms comm_monoid.axioms assms)+
+ apply (rule module_axioms.intro)
+ apply (simp add: smult_closed)
+ apply (simp add: smult_l_distr)
+ apply (simp add: smult_r_distr)
+ apply (simp add: smult_assoc1)
+ apply (simp add: smult_one)
+ apply (rule cring.axioms ring.axioms abelian_group.axioms comm_monoid.axioms assms)+
+ apply (rule algebra_axioms.intro)
+ apply (simp add: smult_assoc2)
+ done
-lemma (in algebra) R_cring:
- "cring R"
- ..
+lemma (in algebra) R_cring: "cring R" ..
-lemma (in algebra) M_cring:
- "cring M"
- ..
+lemma (in algebra) M_cring: "cring M" ..
-lemma (in algebra) module:
- "module R M"
- by (auto intro: moduleI R_cring is_abelian_group
- smult_l_distr smult_r_distr smult_assoc1)
+lemma (in algebra) module: "module R M"
+ by (auto intro: moduleI R_cring is_abelian_group smult_l_distr smult_r_distr smult_assoc1)
-subsection \<open>Basic Properties of Algebras\<close>
+subsection \<open>Basic Properties of Modules\<close>
-lemma (in algebra) smult_l_null [simp]:
- "x \<in> carrier M ==> \<zero> \<odot>\<^bsub>M\<^esub> x = \<zero>\<^bsub>M\<^esub>"
-proof -
- assume M: "x \<in> carrier M"
+lemma (in module) smult_l_null [simp]:
+ "x \<in> carrier M ==> \<zero> \<odot>\<^bsub>M\<^esub> x = \<zero>\<^bsub>M\<^esub>"
+proof-
+ assume M : "x \<in> carrier M"
note facts = M smult_closed [OF R.zero_closed]
- from facts have "\<zero> \<odot>\<^bsub>M\<^esub> x = (\<zero> \<odot>\<^bsub>M\<^esub> x \<oplus>\<^bsub>M\<^esub> \<zero> \<odot>\<^bsub>M\<^esub> x) \<oplus>\<^bsub>M\<^esub> \<ominus>\<^bsub>M\<^esub> (\<zero> \<odot>\<^bsub>M\<^esub> x)" by algebra
- also from M have "... = (\<zero> \<oplus> \<zero>) \<odot>\<^bsub>M\<^esub> x \<oplus>\<^bsub>M\<^esub> \<ominus>\<^bsub>M\<^esub> (\<zero> \<odot>\<^bsub>M\<^esub> x)"
- by (simp add: smult_l_distr del: R.l_zero R.r_zero)
- also from facts have "... = \<zero>\<^bsub>M\<^esub>" apply algebra apply algebra done
- finally show ?thesis .
+ from facts have "\<zero> \<odot>\<^bsub>M\<^esub> x = (\<zero> \<oplus> \<zero>) \<odot>\<^bsub>M\<^esub> x "
+ using smult_l_distr by auto
+ also have "... = \<zero> \<odot>\<^bsub>M\<^esub> x \<oplus>\<^bsub>M\<^esub> \<zero> \<odot>\<^bsub>M\<^esub> x"
+ using smult_l_distr[of \<zero> \<zero> x] facts by auto
+ finally show "\<zero> \<odot>\<^bsub>M\<^esub> x = \<zero>\<^bsub>M\<^esub>" using facts
+ by (metis M.add.r_cancel_one')
qed
-lemma (in algebra) smult_r_null [simp]:
+lemma (in module) smult_r_null [simp]:
"a \<in> carrier R ==> a \<odot>\<^bsub>M\<^esub> \<zero>\<^bsub>M\<^esub> = \<zero>\<^bsub>M\<^esub>"
proof -
assume R: "a \<in> carrier R"
note facts = R smult_closed
from facts have "a \<odot>\<^bsub>M\<^esub> \<zero>\<^bsub>M\<^esub> = (a \<odot>\<^bsub>M\<^esub> \<zero>\<^bsub>M\<^esub> \<oplus>\<^bsub>M\<^esub> a \<odot>\<^bsub>M\<^esub> \<zero>\<^bsub>M\<^esub>) \<oplus>\<^bsub>M\<^esub> \<ominus>\<^bsub>M\<^esub> (a \<odot>\<^bsub>M\<^esub> \<zero>\<^bsub>M\<^esub>)"
- by algebra
+ by (simp add: M.add.inv_solve_right)
also from R have "... = a \<odot>\<^bsub>M\<^esub> (\<zero>\<^bsub>M\<^esub> \<oplus>\<^bsub>M\<^esub> \<zero>\<^bsub>M\<^esub>) \<oplus>\<^bsub>M\<^esub> \<ominus>\<^bsub>M\<^esub> (a \<odot>\<^bsub>M\<^esub> \<zero>\<^bsub>M\<^esub>)"
by (simp add: smult_r_distr del: M.l_zero M.r_zero)
- also from facts have "... = \<zero>\<^bsub>M\<^esub>" by algebra
+ also from facts have "... = \<zero>\<^bsub>M\<^esub>"
+ by (simp add: M.r_neg)
finally show ?thesis .
qed
-lemma (in algebra) smult_l_minus:
- "[| a \<in> carrier R; x \<in> carrier M |] ==> (\<ominus>a) \<odot>\<^bsub>M\<^esub> x = \<ominus>\<^bsub>M\<^esub> (a \<odot>\<^bsub>M\<^esub> x)"
-proof -
+lemma (in module) smult_l_minus:
+"\<lbrakk> a \<in> carrier R; x \<in> carrier M \<rbrakk> \<Longrightarrow> (\<ominus>a) \<odot>\<^bsub>M\<^esub> x = \<ominus>\<^bsub>M\<^esub> (a \<odot>\<^bsub>M\<^esub> x)"
+proof-
assume RM: "a \<in> carrier R" "x \<in> carrier M"
from RM have a_smult: "a \<odot>\<^bsub>M\<^esub> x \<in> carrier M" by simp
from RM have ma_smult: "\<ominus>a \<odot>\<^bsub>M\<^esub> x \<in> carrier M" by simp
note facts = RM a_smult ma_smult
from facts have "(\<ominus>a) \<odot>\<^bsub>M\<^esub> x = (\<ominus>a \<odot>\<^bsub>M\<^esub> x \<oplus>\<^bsub>M\<^esub> a \<odot>\<^bsub>M\<^esub> x) \<oplus>\<^bsub>M\<^esub> \<ominus>\<^bsub>M\<^esub>(a \<odot>\<^bsub>M\<^esub> x)"
- by algebra
+ by (simp add: M.add.inv_solve_right)
also from RM have "... = (\<ominus>a \<oplus> a) \<odot>\<^bsub>M\<^esub> x \<oplus>\<^bsub>M\<^esub> \<ominus>\<^bsub>M\<^esub>(a \<odot>\<^bsub>M\<^esub> x)"
by (simp add: smult_l_distr)
also from facts smult_l_null have "... = \<ominus>\<^bsub>M\<^esub>(a \<odot>\<^bsub>M\<^esub> x)"
- apply algebra apply algebra done
+ by (simp add: R.l_neg)
finally show ?thesis .
qed
-lemma (in algebra) smult_r_minus:
+lemma (in module) smult_r_minus:
"[| a \<in> carrier R; x \<in> carrier M |] ==> a \<odot>\<^bsub>M\<^esub> (\<ominus>\<^bsub>M\<^esub>x) = \<ominus>\<^bsub>M\<^esub> (a \<odot>\<^bsub>M\<^esub> x)"
proof -
assume RM: "a \<in> carrier R" "x \<in> carrier M"
note facts = RM smult_closed
from facts have "a \<odot>\<^bsub>M\<^esub> (\<ominus>\<^bsub>M\<^esub>x) = (a \<odot>\<^bsub>M\<^esub> \<ominus>\<^bsub>M\<^esub>x \<oplus>\<^bsub>M\<^esub> a \<odot>\<^bsub>M\<^esub> x) \<oplus>\<^bsub>M\<^esub> \<ominus>\<^bsub>M\<^esub>(a \<odot>\<^bsub>M\<^esub> x)"
- by algebra
+ by (simp add: M.add.inv_solve_right)
also from RM have "... = a \<odot>\<^bsub>M\<^esub> (\<ominus>\<^bsub>M\<^esub>x \<oplus>\<^bsub>M\<^esub> x) \<oplus>\<^bsub>M\<^esub> \<ominus>\<^bsub>M\<^esub>(a \<odot>\<^bsub>M\<^esub> x)"
by (simp add: smult_r_distr)
- also from facts smult_r_null have "... = \<ominus>\<^bsub>M\<^esub>(a \<odot>\<^bsub>M\<^esub> x)" by algebra
+ also from facts smult_l_null have "... = \<ominus>\<^bsub>M\<^esub>(a \<odot>\<^bsub>M\<^esub> x)"
+ by (metis M.add.inv_closed M.add.inv_solve_right M.l_neg R.zero_closed r_null smult_assoc1)
finally show ?thesis .
qed
+lemma (in module) finsum_smult_ldistr:
+ "\<lbrakk> finite A; a \<in> carrier R; f: A \<rightarrow> carrier M \<rbrakk> \<Longrightarrow>
+ a \<odot>\<^bsub>M\<^esub> (\<Oplus>\<^bsub>M\<^esub> i \<in> A. (f i)) = (\<Oplus>\<^bsub>M\<^esub> i \<in> A. ( a \<odot>\<^bsub>M\<^esub> (f i)))"
+proof (induct set: finite)
+ case empty then show ?case
+ by (metis M.finsum_empty M.zero_closed R.zero_closed r_null smult_assoc1 smult_l_null)
+next
+ case (insert x F) then show ?case
+ by (simp add: Pi_def smult_r_distr)
+qed
+
end
--- a/src/HOL/Algebra/Multiplicative_Group.thy Sun Jul 01 10:58:14 2018 +0200
+++ b/src/HOL/Algebra/Multiplicative_Group.thy Sun Jul 01 17:38:08 2018 +0200
@@ -590,7 +590,11 @@
lemmas mult_of_simps = carrier_mult_of mult_mult_of nat_pow_mult_of one_mult_of
-context field begin
+context field
+begin
+
+lemma mult_of_is_Units: "mult_of R = units_of R"
+ unfolding mult_of_def units_of_def using field_Units by auto
lemma field_mult_group :
shows "group (mult_of R)"
--- a/src/HOL/Algebra/QuotRing.thy Sun Jul 01 10:58:14 2018 +0200
+++ b/src/HOL/Algebra/QuotRing.thy Sun Jul 01 17:38:08 2018 +0200
@@ -1,5 +1,7 @@
(* Title: HOL/Algebra/QuotRing.thy
Author: Stephan Hohe
+ Author: Paulo Emílio de Vilhena
+
*)
theory QuotRing
@@ -306,4 +308,831 @@
qed
qed
+
+lemma (in ring_hom_ring) trivial_hom_iff:
+ "(h ` (carrier R) = { \<zero>\<^bsub>S\<^esub> }) = (a_kernel R S h = carrier R)"
+ using group_hom.trivial_hom_iff[OF a_group_hom] by (simp add: a_kernel_def)
+
+lemma (in ring_hom_ring) trivial_ker_imp_inj:
+ assumes "a_kernel R S h = { \<zero> }"
+ shows "inj_on h (carrier R)"
+ using group_hom.trivial_ker_imp_inj[OF a_group_hom] assms a_kernel_def[of R S h] by simp
+
+lemma (in ring_hom_ring) non_trivial_field_hom_imp_inj:
+ assumes "field R"
+ shows "h ` (carrier R) \<noteq> { \<zero>\<^bsub>S\<^esub> } \<Longrightarrow> inj_on h (carrier R)"
+proof -
+ assume "h ` (carrier R) \<noteq> { \<zero>\<^bsub>S\<^esub> }"
+ hence "a_kernel R S h \<noteq> carrier R"
+ using trivial_hom_iff by linarith
+ hence "a_kernel R S h = { \<zero> }"
+ using field.all_ideals[OF assms] kernel_is_ideal by blast
+ thus "inj_on h (carrier R)"
+ using trivial_ker_imp_inj by blast
+qed
+
+lemma (in ring_hom_ring) img_is_add_subgroup:
+ assumes "subgroup H (add_monoid R)"
+ shows "subgroup (h ` H) (add_monoid S)"
+proof -
+ have "group ((add_monoid R) \<lparr> carrier := H \<rparr>)"
+ using assms R.add.subgroup_imp_group by blast
+ moreover have "H \<subseteq> carrier R" by (simp add: R.add.subgroupE(1) assms)
+ hence "h \<in> hom ((add_monoid R) \<lparr> carrier := H \<rparr>) (add_monoid S)"
+ unfolding hom_def by (auto simp add: subsetD)
+ ultimately have "subgroup (h ` carrier ((add_monoid R) \<lparr> carrier := H \<rparr>)) (add_monoid S)"
+ using group_hom.img_is_subgroup[of "(add_monoid R) \<lparr> carrier := H \<rparr>" "add_monoid S" h]
+ using a_group_hom group_hom_axioms.intro group_hom_def by blast
+ thus "subgroup (h ` H) (add_monoid S)" by simp
+qed
+
+lemma (in ring) ring_ideal_imp_quot_ideal:
+ assumes "ideal I R"
+ shows "ideal J R \<Longrightarrow> ideal ((+>) I ` J) (R Quot I)"
+proof -
+ assume A: "ideal J R" show "ideal (((+>) I) ` J) (R Quot I)"
+ proof (rule idealI)
+ show "ring (R Quot I)"
+ by (simp add: assms(1) ideal.quotient_is_ring)
+ next
+ have "subgroup J (add_monoid R)"
+ by (simp add: additive_subgroup.a_subgroup A ideal.axioms(1))
+ moreover have "((+>) I) \<in> ring_hom R (R Quot I)"
+ by (simp add: assms(1) ideal.rcos_ring_hom)
+ ultimately show "subgroup ((+>) I ` J) (add_monoid (R Quot I))"
+ using assms(1) ideal.rcos_ring_hom_ring ring_hom_ring.img_is_add_subgroup by blast
+ next
+ fix a x assume "a \<in> (+>) I ` J" "x \<in> carrier (R Quot I)"
+ then obtain i j where i: "i \<in> carrier R" "x = I +> i"
+ and j: "j \<in> J" "a = I +> j"
+ unfolding FactRing_def using A_RCOSETS_def'[of R I] by auto
+ hence "a \<otimes>\<^bsub>R Quot I\<^esub> x = [mod I:] (I +> j) \<Otimes> (I +> i)"
+ unfolding FactRing_def by simp
+ hence "a \<otimes>\<^bsub>R Quot I\<^esub> x = I +> (j \<otimes> i)"
+ using ideal.rcoset_mult_add[OF assms(1), of j i] i(1) j(1) A ideal.Icarr by force
+ thus "a \<otimes>\<^bsub>R Quot I\<^esub> x \<in> (+>) I ` J"
+ using A i(1) j(1) by (simp add: ideal.I_r_closed)
+
+ have "x \<otimes>\<^bsub>R Quot I\<^esub> a = [mod I:] (I +> i) \<Otimes> (I +> j)"
+ unfolding FactRing_def i j by simp
+ hence "x \<otimes>\<^bsub>R Quot I\<^esub> a = I +> (i \<otimes> j)"
+ using ideal.rcoset_mult_add[OF assms(1), of i j] i(1) j(1) A ideal.Icarr by force
+ thus "x \<otimes>\<^bsub>R Quot I\<^esub> a \<in> (+>) I ` J"
+ using A i(1) j(1) by (simp add: ideal.I_l_closed)
+ qed
+qed
+
+lemma (in ring_hom_ring) ideal_vimage:
+ assumes "ideal I S"
+ shows "ideal { r \<in> carrier R. h r \<in> I } R" (* or (carrier R) \<inter> (h -` I) *)
+proof
+ show "{ r \<in> carrier R. h r \<in> I } \<subseteq> carrier (add_monoid R)" by auto
+next
+ show "\<one>\<^bsub>add_monoid R\<^esub> \<in> { r \<in> carrier R. h r \<in> I }"
+ by (simp add: additive_subgroup.zero_closed assms ideal.axioms(1))
+next
+ fix a b
+ assume "a \<in> { r \<in> carrier R. h r \<in> I }"
+ and "b \<in> { r \<in> carrier R. h r \<in> I }"
+ hence a: "a \<in> carrier R" "h a \<in> I"
+ and b: "b \<in> carrier R" "h b \<in> I" by auto
+ hence "h (a \<oplus> b) = (h a) \<oplus>\<^bsub>S\<^esub> (h b)" using hom_add by blast
+ moreover have "(h a) \<oplus>\<^bsub>S\<^esub> (h b) \<in> I" using a b assms
+ by (simp add: additive_subgroup.a_closed ideal.axioms(1))
+ ultimately show "a \<otimes>\<^bsub>add_monoid R\<^esub> b \<in> { r \<in> carrier R. h r \<in> I }"
+ using a(1) b (1) by auto
+
+ have "h (\<ominus> a) = \<ominus>\<^bsub>S\<^esub> (h a)" by (simp add: a)
+ moreover have "\<ominus>\<^bsub>S\<^esub> (h a) \<in> I"
+ by (simp add: a(2) additive_subgroup.a_inv_closed assms ideal.axioms(1))
+ ultimately show "inv\<^bsub>add_monoid R\<^esub> a \<in> { r \<in> carrier R. h r \<in> I }"
+ using a by (simp add: a_inv_def)
+next
+ fix a r
+ assume "a \<in> { r \<in> carrier R. h r \<in> I }" and r: "r \<in> carrier R"
+ hence a: "a \<in> carrier R" "h a \<in> I" by auto
+
+ have "h a \<otimes>\<^bsub>S\<^esub> h r \<in> I"
+ using assms a r by (simp add: ideal.I_r_closed)
+ thus "a \<otimes> r \<in> { r \<in> carrier R. h r \<in> I }" by (simp add: a(1) r)
+
+ have "h r \<otimes>\<^bsub>S\<^esub> h a \<in> I"
+ using assms a r by (simp add: ideal.I_l_closed)
+ thus "r \<otimes> a \<in> { r \<in> carrier R. h r \<in> I }" by (simp add: a(1) r)
+qed
+
+lemma (in ring) canonical_proj_vimage_in_carrier:
+ assumes "ideal I R"
+ shows "J \<subseteq> carrier (R Quot I) \<Longrightarrow> \<Union> J \<subseteq> carrier R"
+proof -
+ assume A: "J \<subseteq> carrier (R Quot I)" show "\<Union> J \<subseteq> carrier R"
+ proof
+ fix j assume j: "j \<in> \<Union> J"
+ then obtain j' where j': "j' \<in> J" "j \<in> j'" by blast
+ then obtain r where r: "r \<in> carrier R" "j' = I +> r"
+ using A j' unfolding FactRing_def using A_RCOSETS_def'[of R I] by auto
+ thus "j \<in> carrier R" using j' assms
+ by (meson a_r_coset_subset_G additive_subgroup.a_subset contra_subsetD ideal.axioms(1))
+ qed
+qed
+
+lemma (in ring) canonical_proj_vimage_mem_iff:
+ assumes "ideal I R" "J \<subseteq> carrier (R Quot I)"
+ shows "\<And>a. a \<in> carrier R \<Longrightarrow> (a \<in> (\<Union> J)) = (I +> a \<in> J)"
+proof -
+ fix a assume a: "a \<in> carrier R" show "(a \<in> (\<Union> J)) = (I +> a \<in> J)"
+ proof
+ assume "a \<in> \<Union> J"
+ then obtain j where j: "j \<in> J" "a \<in> j" by blast
+ then obtain r where r: "r \<in> carrier R" "j = I +> r"
+ using assms j unfolding FactRing_def using A_RCOSETS_def'[of R I] by auto
+ hence "I +> r = I +> a"
+ using add.repr_independence[of a I r] j r
+ by (metis a_r_coset_def additive_subgroup.a_subgroup assms(1) ideal.axioms(1))
+ thus "I +> a \<in> J" using r j by simp
+ next
+ assume "I +> a \<in> J"
+ hence "\<zero> \<oplus> a \<in> I +> a"
+ using additive_subgroup.zero_closed[OF ideal.axioms(1)[OF assms(1)]]
+ a_r_coset_def'[of R I a] by blast
+ thus "a \<in> \<Union> J" using a \<open>I +> a \<in> J\<close> by auto
+ qed
+qed
+
+corollary (in ring) quot_ideal_imp_ring_ideal:
+ assumes "ideal I R"
+ shows "ideal J (R Quot I) \<Longrightarrow> ideal (\<Union> J) R"
+proof -
+ assume A: "ideal J (R Quot I)"
+ have "\<Union> J = { r \<in> carrier R. I +> r \<in> J }"
+ using canonical_proj_vimage_in_carrier[OF assms, of J]
+ canonical_proj_vimage_mem_iff[OF assms, of J]
+ additive_subgroup.a_subset[OF ideal.axioms(1)[OF A]] by blast
+ thus "ideal (\<Union> J) R"
+ using ring_hom_ring.ideal_vimage[OF ideal.rcos_ring_hom_ring[OF assms] A] by simp
+qed
+
+lemma (in ring) ideal_incl_iff:
+ assumes "ideal I R" "ideal J R"
+ shows "(I \<subseteq> J) = (J = (\<Union> j \<in> J. I +> j))"
+proof
+ assume A: "J = (\<Union> j \<in> J. I +> j)" hence "I +> \<zero> \<subseteq> J"
+ using additive_subgroup.zero_closed[OF ideal.axioms(1)[OF assms(2)]] by blast
+ thus "I \<subseteq> J" using additive_subgroup.a_subset[OF ideal.axioms(1)[OF assms(1)]] by simp
+next
+ assume A: "I \<subseteq> J" show "J = (\<Union>j\<in>J. I +> j)"
+ proof
+ show "J \<subseteq> (\<Union> j \<in> J. I +> j)"
+ proof
+ fix j assume j: "j \<in> J"
+ have "\<zero> \<in> I" by (simp add: additive_subgroup.zero_closed assms(1) ideal.axioms(1))
+ hence "\<zero> \<oplus> j \<in> I +> j"
+ using a_r_coset_def'[of R I j] by blast
+ thus "j \<in> (\<Union>j\<in>J. I +> j)"
+ using assms(2) j additive_subgroup.a_Hcarr ideal.axioms(1) by fastforce
+ qed
+ next
+ show "(\<Union> j \<in> J. I +> j) \<subseteq> J"
+ proof
+ fix x assume "x \<in> (\<Union> j \<in> J. I +> j)"
+ then obtain j where j: "j \<in> J" "x \<in> I +> j" by blast
+ then obtain i where i: "i \<in> I" "x = i \<oplus> j"
+ using a_r_coset_def'[of R I j] by blast
+ thus "x \<in> J"
+ using assms(2) j A additive_subgroup.a_closed[OF ideal.axioms(1)[OF assms(2)]] by blast
+ qed
+ qed
+qed
+
+theorem (in ring) quot_ideal_correspondence:
+ assumes "ideal I R"
+ shows "bij_betw (\<lambda>J. (+>) I ` J) { J. ideal J R \<and> I \<subseteq> J } { J . ideal J (R Quot I) }"
+proof (rule bij_betw_byWitness[where ?f' = "\<lambda>X. \<Union> X"])
+ show "\<forall>J \<in> { J. ideal J R \<and> I \<subseteq> J }. (\<lambda>X. \<Union> X) ((+>) I ` J) = J"
+ using assms ideal_incl_iff by blast
+next
+ show "(\<lambda>J. (+>) I ` J) ` { J. ideal J R \<and> I \<subseteq> J } \<subseteq> { J. ideal J (R Quot I) }"
+ using assms ring_ideal_imp_quot_ideal by auto
+next
+ show "(\<lambda>X. \<Union> X) ` { J. ideal J (R Quot I) } \<subseteq> { J. ideal J R \<and> I \<subseteq> J }"
+ proof
+ fix J assume "J \<in> ((\<lambda>X. \<Union> X) ` { J. ideal J (R Quot I) })"
+ then obtain J' where J': "ideal J' (R Quot I)" "J = \<Union> J'" by blast
+ hence "ideal J R"
+ using assms quot_ideal_imp_ring_ideal by auto
+ moreover have "I \<in> J'"
+ using additive_subgroup.zero_closed[OF ideal.axioms(1)[OF J'(1)]] unfolding FactRing_def by simp
+ ultimately show "J \<in> { J. ideal J R \<and> I \<subseteq> J }" using J'(2) by auto
+ qed
+next
+ show "\<forall>J' \<in> { J. ideal J (R Quot I) }. ((+>) I ` (\<Union> J')) = J'"
+ proof
+ fix J' assume "J' \<in> { J. ideal J (R Quot I) }"
+ hence subset: "J' \<subseteq> carrier (R Quot I) \<and> ideal J' (R Quot I)"
+ using additive_subgroup.a_subset ideal_def by blast
+ hence "((+>) I ` (\<Union> J')) \<subseteq> J'"
+ using canonical_proj_vimage_in_carrier canonical_proj_vimage_mem_iff
+ by (meson assms contra_subsetD image_subsetI)
+ moreover have "J' \<subseteq> ((+>) I ` (\<Union> J'))"
+ proof
+ fix x assume "x \<in> J'"
+ then obtain r where r: "r \<in> carrier R" "x = I +> r"
+ using subset unfolding FactRing_def A_RCOSETS_def'[of R I] by auto
+ hence "r \<in> (\<Union> J')"
+ using \<open>x \<in> J'\<close> assms canonical_proj_vimage_mem_iff subset by blast
+ thus "x \<in> ((+>) I ` (\<Union> J'))" using r(2) by blast
+ qed
+ ultimately show "((+>) I ` (\<Union> J')) = J'" by blast
+ qed
+qed
+
+lemma (in cring) quot_domain_imp_primeideal:
+ assumes "ideal P R"
+ shows "domain (R Quot P) \<Longrightarrow> primeideal P R"
+proof -
+ assume A: "domain (R Quot P)" show "primeideal P R"
+ proof (rule primeidealI)
+ show "ideal P R" using assms .
+ show "cring R" using is_cring .
+ next
+ show "carrier R \<noteq> P"
+ proof (rule ccontr)
+ assume "\<not> carrier R \<noteq> P" hence "carrier R = P" by simp
+ hence "\<And>I. I \<in> carrier (R Quot P) \<Longrightarrow> I = P"
+ unfolding FactRing_def A_RCOSETS_def' apply simp
+ using a_coset_join2 additive_subgroup.a_subgroup assms ideal.axioms(1) by blast
+ hence "\<one>\<^bsub>(R Quot P)\<^esub> = \<zero>\<^bsub>(R Quot P)\<^esub>"
+ by (metis assms ideal.quotient_is_ring ring.ring_simprules(2) ring.ring_simprules(6))
+ thus False using domain.one_not_zero[OF A] by simp
+ qed
+ next
+ fix a b assume a: "a \<in> carrier R" and b: "b \<in> carrier R" and ab: "a \<otimes> b \<in> P"
+ hence "P +> (a \<otimes> b) = \<zero>\<^bsub>(R Quot P)\<^esub>" unfolding FactRing_def
+ by (simp add: a_coset_join2 additive_subgroup.a_subgroup assms ideal.axioms(1))
+ moreover have "(P +> a) \<otimes>\<^bsub>(R Quot P)\<^esub> (P +> b) = P +> (a \<otimes> b)" unfolding FactRing_def
+ using a b by (simp add: assms ideal.rcoset_mult_add)
+ moreover have "P +> a \<in> carrier (R Quot P) \<and> P +> b \<in> carrier (R Quot P)"
+ by (simp add: a b FactRing_def a_rcosetsI additive_subgroup.a_subset assms ideal.axioms(1))
+ ultimately have "P +> a = \<zero>\<^bsub>(R Quot P)\<^esub> \<or> P +> b = \<zero>\<^bsub>(R Quot P)\<^esub>"
+ using domain.integral[OF A, of "P +> a" "P +> b"] by auto
+ thus "a \<in> P \<or> b \<in> P" unfolding FactRing_def apply simp
+ using a b assms a_coset_join1 additive_subgroup.a_subgroup ideal.axioms(1) by blast
+ qed
+qed
+
+lemma (in cring) quot_domain_iff_primeideal:
+ assumes "ideal P R"
+ shows "domain (R Quot P) = primeideal P R"
+ using quot_domain_imp_primeideal[OF assms] primeideal.quotient_is_domain[of P R] by auto
+
+
+subsection \<open>Isomorphism\<close>
+
+definition
+ ring_iso :: "_ \<Rightarrow> _ \<Rightarrow> ('a \<Rightarrow> 'b) set"
+ where "ring_iso R S = { h. h \<in> ring_hom R S \<and> bij_betw h (carrier R) (carrier S) }"
+
+definition
+ is_ring_iso :: "_ \<Rightarrow> _ \<Rightarrow> bool" (infixr "\<simeq>" 60)
+ where "R \<simeq> S = (ring_iso R S \<noteq> {})"
+
+definition
+ morphic_prop :: "_ \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
+ where "morphic_prop R P =
+ ((P \<one>\<^bsub>R\<^esub>) \<and>
+ (\<forall>r \<in> carrier R. P r) \<and>
+ (\<forall>r1 \<in> carrier R. \<forall>r2 \<in> carrier R. P (r1 \<otimes>\<^bsub>R\<^esub> r2)) \<and>
+ (\<forall>r1 \<in> carrier R. \<forall>r2 \<in> carrier R. P (r1 \<oplus>\<^bsub>R\<^esub> r2)))"
+
+lemma ring_iso_memI:
+ fixes R (structure) and S (structure)
+ assumes "\<And>x. x \<in> carrier R \<Longrightarrow> h x \<in> carrier S"
+ and "\<And>x y. \<lbrakk> x \<in> carrier R; y \<in> carrier R \<rbrakk> \<Longrightarrow> h (x \<otimes> y) = h x \<otimes>\<^bsub>S\<^esub> h y"
+ and "\<And>x y. \<lbrakk> x \<in> carrier R; y \<in> carrier R \<rbrakk> \<Longrightarrow> h (x \<oplus> y) = h x \<oplus>\<^bsub>S\<^esub> h y"
+ and "h \<one> = \<one>\<^bsub>S\<^esub>"
+ and "bij_betw h (carrier R) (carrier S)"
+ shows "h \<in> ring_iso R S"
+ by (auto simp add: ring_hom_memI assms ring_iso_def)
+
+lemma ring_iso_memE:
+ fixes R (structure) and S (structure)
+ assumes "h \<in> ring_iso R S"
+ shows "\<And>x. x \<in> carrier R \<Longrightarrow> h x \<in> carrier S"
+ and "\<And>x y. \<lbrakk> x \<in> carrier R; y \<in> carrier R \<rbrakk> \<Longrightarrow> h (x \<otimes> y) = h x \<otimes>\<^bsub>S\<^esub> h y"
+ and "\<And>x y. \<lbrakk> x \<in> carrier R; y \<in> carrier R \<rbrakk> \<Longrightarrow> h (x \<oplus> y) = h x \<oplus>\<^bsub>S\<^esub> h y"
+ and "h \<one> = \<one>\<^bsub>S\<^esub>"
+ and "bij_betw h (carrier R) (carrier S)"
+ using assms unfolding ring_iso_def ring_hom_def by auto
+
+lemma morphic_propI:
+ fixes R (structure)
+ assumes "P \<one>"
+ and "\<And>r. r \<in> carrier R \<Longrightarrow> P r"
+ and "\<And>r1 r2. \<lbrakk> r1 \<in> carrier R; r2 \<in> carrier R \<rbrakk> \<Longrightarrow> P (r1 \<otimes> r2)"
+ and "\<And>r1 r2. \<lbrakk> r1 \<in> carrier R; r2 \<in> carrier R \<rbrakk> \<Longrightarrow> P (r1 \<oplus> r2)"
+ shows "morphic_prop R P"
+ unfolding morphic_prop_def using assms by auto
+
+lemma morphic_propE:
+ fixes R (structure)
+ assumes "morphic_prop R P"
+ shows "P \<one>"
+ and "\<And>r. r \<in> carrier R \<Longrightarrow> P r"
+ and "\<And>r1 r2. \<lbrakk> r1 \<in> carrier R; r2 \<in> carrier R \<rbrakk> \<Longrightarrow> P (r1 \<otimes> r2)"
+ and "\<And>r1 r2. \<lbrakk> r1 \<in> carrier R; r2 \<in> carrier R \<rbrakk> \<Longrightarrow> P (r1 \<oplus> r2)"
+ using assms unfolding morphic_prop_def by auto
+
+lemma ring_iso_restrict:
+ assumes "f \<in> ring_iso R S"
+ and "\<And>r. r \<in> carrier R \<Longrightarrow> f r = g r"
+ and "ring R"
+ shows "g \<in> ring_iso R S"
+proof (rule ring_iso_memI)
+ show "bij_betw g (carrier R) (carrier S)"
+ using assms(1-2) bij_betw_cong ring_iso_memE(5) by blast
+ show "g \<one>\<^bsub>R\<^esub> = \<one>\<^bsub>S\<^esub>"
+ using assms ring.ring_simprules(6) ring_iso_memE(4) by force
+next
+ fix x y assume x: "x \<in> carrier R" and y: "y \<in> carrier R"
+ show "g x \<in> carrier S"
+ using assms(1-2) ring_iso_memE(1) x by fastforce
+ show "g (x \<otimes>\<^bsub>R\<^esub> y) = g x \<otimes>\<^bsub>S\<^esub> g y"
+ by (metis assms ring.ring_simprules(5) ring_iso_memE(2) x y)
+ show "g (x \<oplus>\<^bsub>R\<^esub> y) = g x \<oplus>\<^bsub>S\<^esub> g y"
+ by (metis assms ring.ring_simprules(1) ring_iso_memE(3) x y)
+qed
+
+lemma ring_iso_morphic_prop:
+ assumes "f \<in> ring_iso R S"
+ and "morphic_prop R P"
+ and "\<And>r. P r \<Longrightarrow> f r = g r"
+ shows "g \<in> ring_iso R S"
+proof -
+ have eq0: "\<And>r. r \<in> carrier R \<Longrightarrow> f r = g r"
+ and eq1: "f \<one>\<^bsub>R\<^esub> = g \<one>\<^bsub>R\<^esub>"
+ and eq2: "\<And>r1 r2. \<lbrakk> r1 \<in> carrier R; r2 \<in> carrier R \<rbrakk> \<Longrightarrow> f (r1 \<otimes>\<^bsub>R\<^esub> r2) = g (r1 \<otimes>\<^bsub>R\<^esub> r2)"
+ and eq3: "\<And>r1 r2. \<lbrakk> r1 \<in> carrier R; r2 \<in> carrier R \<rbrakk> \<Longrightarrow> f (r1 \<oplus>\<^bsub>R\<^esub> r2) = g (r1 \<oplus>\<^bsub>R\<^esub> r2)"
+ using assms(2-3) unfolding morphic_prop_def by auto
+ show ?thesis
+ apply (rule ring_iso_memI)
+ using assms(1) eq0 ring_iso_memE(1) apply fastforce
+ apply (metis assms(1) eq0 eq2 ring_iso_memE(2))
+ apply (metis assms(1) eq0 eq3 ring_iso_memE(3))
+ using assms(1) eq1 ring_iso_memE(4) apply fastforce
+ using assms(1) bij_betw_cong eq0 ring_iso_memE(5) by blast
+qed
+
+lemma (in ring) ring_hom_imp_img_ring:
+ assumes "h \<in> ring_hom R S"
+ shows "ring (S \<lparr> carrier := h ` (carrier R), one := h \<one>, zero := h \<zero> \<rparr>)" (is "ring ?h_img")
+proof -
+ have "h \<in> hom (add_monoid R) (add_monoid S)"
+ using assms unfolding hom_def ring_hom_def by auto
+ hence "comm_group ((add_monoid S) \<lparr> carrier := h ` (carrier R), one := h \<zero> \<rparr>)"
+ using add.hom_imp_img_comm_group[of h "add_monoid S"] by simp
+ hence comm_group: "comm_group (add_monoid ?h_img)"
+ by (auto intro: comm_monoidI simp add: monoid.defs)
+
+ moreover have "h \<in> hom R S"
+ using assms unfolding ring_hom_def hom_def by auto
+ hence "monoid (S \<lparr> carrier := h ` (carrier R), one := h \<one> \<rparr>)"
+ using hom_imp_img_monoid[of h S] by simp
+ hence monoid: "monoid ?h_img"
+ unfolding monoid_def by (simp add: monoid.defs)
+
+ show ?thesis
+ proof (rule ringI, simp_all add: comm_group_abelian_groupI[OF comm_group] monoid)
+ fix x y z assume "x \<in> h ` carrier R" "y \<in> h ` carrier R" "z \<in> h ` carrier R"
+ then obtain r1 r2 r3
+ where r1: "r1 \<in> carrier R" "x = h r1"
+ and r2: "r2 \<in> carrier R" "y = h r2"
+ and r3: "r3 \<in> carrier R" "z = h r3" by blast
+ hence "(x \<oplus>\<^bsub>S\<^esub> y) \<otimes>\<^bsub>S\<^esub> z = h ((r1 \<oplus> r2) \<otimes> r3)"
+ using ring_hom_memE[OF assms] by auto
+ also have " ... = h ((r1 \<otimes> r3) \<oplus> (r2 \<otimes> r3))"
+ using l_distr[OF r1(1) r2(1) r3(1)] by simp
+ also have " ... = (x \<otimes>\<^bsub>S\<^esub> z) \<oplus>\<^bsub>S\<^esub> (y \<otimes>\<^bsub>S\<^esub> z)"
+ using ring_hom_memE[OF assms] r1 r2 r3 by auto
+ finally show "(x \<oplus>\<^bsub>S\<^esub> y) \<otimes>\<^bsub>S\<^esub> z = (x \<otimes>\<^bsub>S\<^esub> z) \<oplus>\<^bsub>S\<^esub> (y \<otimes>\<^bsub>S\<^esub> z)" .
+
+ have "z \<otimes>\<^bsub>S\<^esub> (x \<oplus>\<^bsub>S\<^esub> y) = h (r3 \<otimes> (r1 \<oplus> r2))"
+ using ring_hom_memE[OF assms] r1 r2 r3 by auto
+ also have " ... = h ((r3 \<otimes> r1) \<oplus> (r3 \<otimes> r2))"
+ using r_distr[OF r1(1) r2(1) r3(1)] by simp
+ also have " ... = (z \<otimes>\<^bsub>S\<^esub> x) \<oplus>\<^bsub>S\<^esub> (z \<otimes>\<^bsub>S\<^esub> y)"
+ using ring_hom_memE[OF assms] r1 r2 r3 by auto
+ finally show "z \<otimes>\<^bsub>S\<^esub> (x \<oplus>\<^bsub>S\<^esub> y) = (z \<otimes>\<^bsub>S\<^esub> x) \<oplus>\<^bsub>S\<^esub> (z \<otimes>\<^bsub>S\<^esub> y)" .
+ qed
+qed
+
+lemma (in ring) ring_iso_imp_img_ring:
+ assumes "h \<in> ring_iso R S"
+ shows "ring (S \<lparr> one := h \<one>, zero := h \<zero> \<rparr>)"
+proof -
+ have "ring (S \<lparr> carrier := h ` (carrier R), one := h \<one>, zero := h \<zero> \<rparr>)"
+ using ring_hom_imp_img_ring[of h S] assms unfolding ring_iso_def by auto
+ moreover have "h ` (carrier R) = carrier S"
+ using assms unfolding ring_iso_def bij_betw_def by auto
+ ultimately show ?thesis by simp
+qed
+
+lemma (in cring) ring_iso_imp_img_cring:
+ assumes "h \<in> ring_iso R S"
+ shows "cring (S \<lparr> one := h \<one>, zero := h \<zero> \<rparr>)" (is "cring ?h_img")
+proof -
+ note m_comm
+ interpret h_img?: ring ?h_img
+ using ring_iso_imp_img_ring[OF assms] .
+ show ?thesis
+ proof (unfold_locales)
+ fix x y assume "x \<in> carrier ?h_img" "y \<in> carrier ?h_img"
+ then obtain r1 r2
+ where r1: "r1 \<in> carrier R" "x = h r1"
+ and r2: "r2 \<in> carrier R" "y = h r2"
+ using assms image_iff[where ?f = h and ?A = "carrier R"]
+ unfolding ring_iso_def bij_betw_def by auto
+ have "x \<otimes>\<^bsub>(?h_img)\<^esub> y = h (r1 \<otimes> r2)"
+ using assms r1 r2 unfolding ring_iso_def ring_hom_def by auto
+ also have " ... = h (r2 \<otimes> r1)"
+ using m_comm[OF r1(1) r2(1)] by simp
+ also have " ... = y \<otimes>\<^bsub>(?h_img)\<^esub> x"
+ using assms r1 r2 unfolding ring_iso_def ring_hom_def by auto
+ finally show "x \<otimes>\<^bsub>(?h_img)\<^esub> y = y \<otimes>\<^bsub>(?h_img)\<^esub> x" .
+ qed
+qed
+
+lemma (in domain) ring_iso_imp_img_domain:
+ assumes "h \<in> ring_iso R S"
+ shows "domain (S \<lparr> one := h \<one>, zero := h \<zero> \<rparr>)" (is "domain ?h_img")
+proof -
+ note aux = m_closed integral one_not_zero one_closed zero_closed
+ interpret h_img?: cring ?h_img
+ using ring_iso_imp_img_cring[OF assms] .
+ show ?thesis
+ proof (unfold_locales)
+ show "\<one>\<^bsub>?h_img\<^esub> \<noteq> \<zero>\<^bsub>?h_img\<^esub>"
+ using ring_iso_memE(5)[OF assms] aux(3-4)
+ unfolding bij_betw_def inj_on_def by force
+ next
+ fix a b
+ assume A: "a \<otimes>\<^bsub>?h_img\<^esub> b = \<zero>\<^bsub>?h_img\<^esub>" "a \<in> carrier ?h_img" "b \<in> carrier ?h_img"
+ then obtain r1 r2
+ where r1: "r1 \<in> carrier R" "a = h r1"
+ and r2: "r2 \<in> carrier R" "b = h r2"
+ using assms image_iff[where ?f = h and ?A = "carrier R"]
+ unfolding ring_iso_def bij_betw_def by auto
+ hence "a \<otimes>\<^bsub>?h_img\<^esub> b = h (r1 \<otimes> r2)"
+ using assms r1 r2 unfolding ring_iso_def ring_hom_def by auto
+ hence "h (r1 \<otimes> r2) = h \<zero>"
+ using A(1) by simp
+ hence "r1 \<otimes> r2 = \<zero>"
+ using ring_iso_memE(5)[OF assms] aux(1)[OF r1(1) r2(1)] aux(5)
+ unfolding bij_betw_def inj_on_def by force
+ hence "r1 = \<zero> \<or> r2 = \<zero>"
+ using aux(2)[OF _ r1(1) r2(1)] by simp
+ thus "a = \<zero>\<^bsub>?h_img\<^esub> \<or> b = \<zero>\<^bsub>?h_img\<^esub>"
+ unfolding r1 r2 by auto
+ qed
+qed
+
+lemma (in field) ring_iso_imp_img_field:
+ assumes "h \<in> ring_iso R S"
+ shows "field (S \<lparr> one := h \<one>, zero := h \<zero> \<rparr>)" (is "field ?h_img")
+proof -
+ interpret h_img?: domain ?h_img
+ using ring_iso_imp_img_domain[OF assms] .
+ show ?thesis
+ proof (unfold_locales, auto simp add: Units_def)
+ interpret field R using field_axioms .
+ fix a assume a: "a \<in> carrier S" "a \<otimes>\<^bsub>S\<^esub> h \<zero> = h \<one>"
+ then obtain r where r: "r \<in> carrier R" "a = h r"
+ using assms image_iff[where ?f = h and ?A = "carrier R"]
+ unfolding ring_iso_def bij_betw_def by auto
+ have "a \<otimes>\<^bsub>S\<^esub> h \<zero> = h (r \<otimes> \<zero>)" unfolding r(2)
+ using ring_iso_memE(2)[OF assms r(1)] by simp
+ hence "h \<one> = h \<zero>"
+ using r(1) a(2) by simp
+ thus False
+ using ring_iso_memE(5)[OF assms]
+ unfolding bij_betw_def inj_on_def by force
+ next
+ interpret field R using field_axioms .
+ fix s assume s: "s \<in> carrier S" "s \<noteq> h \<zero>"
+ then obtain r where r: "r \<in> carrier R" "s = h r"
+ using assms image_iff[where ?f = h and ?A = "carrier R"]
+ unfolding ring_iso_def bij_betw_def by auto
+ hence "r \<noteq> \<zero>" using s(2) by auto
+ hence inv_r: "inv r \<in> carrier R" "inv r \<noteq> \<zero>" "r \<otimes> inv r = \<one>" "inv r \<otimes> r = \<one>"
+ using field_Units r(1) by auto
+ have "h (inv r) \<otimes>\<^bsub>S\<^esub> h r = h \<one>" and "h r \<otimes>\<^bsub>S\<^esub> h (inv r) = h \<one>"
+ using ring_iso_memE(2)[OF assms inv_r(1) r(1)] inv_r(3-4)
+ ring_iso_memE(2)[OF assms r(1) inv_r(1)] by auto
+ thus "\<exists>s' \<in> carrier S. s' \<otimes>\<^bsub>S\<^esub> s = h \<one> \<and> s \<otimes>\<^bsub>S\<^esub> s' = h \<one>"
+ using ring_iso_memE(1)[OF assms inv_r(1)] r(2) by auto
+ qed
+qed
+
+lemma ring_iso_same_card: "R \<simeq> S \<Longrightarrow> card (carrier R) = card (carrier S)"
+proof -
+ assume "R \<simeq> S"
+ then obtain h where "bij_betw h (carrier R) (carrier S)"
+ unfolding is_ring_iso_def ring_iso_def by auto
+ thus "card (carrier R) = card (carrier S)"
+ using bij_betw_same_card[of h "carrier R" "carrier S"] by simp
+qed
+
+lemma ring_iso_set_refl: "id \<in> ring_iso R R"
+ by (rule ring_iso_memI) (auto)
+
+corollary ring_iso_refl: "R \<simeq> R"
+ using is_ring_iso_def ring_iso_set_refl by auto
+
+lemma ring_iso_set_trans:
+ "\<lbrakk> f \<in> ring_iso R S; g \<in> ring_iso S Q \<rbrakk> \<Longrightarrow> (g \<circ> f) \<in> ring_iso R Q"
+ unfolding ring_iso_def using bij_betw_trans ring_hom_trans by fastforce
+
+corollary ring_iso_trans: "\<lbrakk> R \<simeq> S; S \<simeq> Q \<rbrakk> \<Longrightarrow> R \<simeq> Q"
+ using ring_iso_set_trans unfolding is_ring_iso_def by blast
+
+lemma ring_iso_set_sym:
+ assumes "ring R"
+ shows "h \<in> ring_iso R S \<Longrightarrow> (inv_into (carrier R) h) \<in> ring_iso S R"
+proof -
+ assume h: "h \<in> ring_iso R S"
+ hence h_hom: "h \<in> ring_hom R S"
+ and h_surj: "h ` (carrier R) = (carrier S)"
+ and h_inj: "\<And> x1 x2. \<lbrakk> x1 \<in> carrier R; x2 \<in> carrier R \<rbrakk> \<Longrightarrow> h x1 = h x2 \<Longrightarrow> x1 = x2"
+ unfolding ring_iso_def bij_betw_def inj_on_def by auto
+
+ have h_inv_bij: "bij_betw (inv_into (carrier R) h) (carrier S) (carrier R)"
+ using bij_betw_inv_into h ring_iso_def by fastforce
+
+ show "inv_into (carrier R) h \<in> ring_iso S R"
+ apply (rule ring_iso_memI)
+ apply (simp add: h_surj inv_into_into)
+ apply (auto simp add: h_inv_bij)
+ apply (smt assms f_inv_into_f h_hom h_inj h_surj inv_into_into
+ ring.ring_simprules(5) ring_hom_closed ring_hom_mult)
+ apply (smt assms f_inv_into_f h_hom h_inj h_surj inv_into_into
+ ring.ring_simprules(1) ring_hom_add ring_hom_closed)
+ by (metis (no_types, hide_lams) assms f_inv_into_f h_hom h_inj
+ imageI inv_into_into ring.ring_simprules(6) ring_hom_one)
+qed
+
+corollary ring_iso_sym:
+ assumes "ring R"
+ shows "R \<simeq> S \<Longrightarrow> S \<simeq> R"
+ using assms ring_iso_set_sym unfolding is_ring_iso_def by auto
+
+lemma (in ring_hom_ring) the_elem_simp [simp]:
+ "\<And>x. x \<in> carrier R \<Longrightarrow> the_elem (h ` ((a_kernel R S h) +> x)) = h x"
+proof -
+ fix x assume x: "x \<in> carrier R"
+ hence "h x \<in> h ` ((a_kernel R S h) +> x)"
+ using homeq_imp_rcos by blast
+ thus "the_elem (h ` ((a_kernel R S h) +> x)) = h x"
+ by (metis (no_types, lifting) x empty_iff homeq_imp_rcos rcos_imp_homeq the_elem_image_unique)
+qed
+
+lemma (in ring_hom_ring) the_elem_inj:
+ "\<And>X Y. \<lbrakk> X \<in> carrier (R Quot (a_kernel R S h)); Y \<in> carrier (R Quot (a_kernel R S h)) \<rbrakk> \<Longrightarrow>
+ the_elem (h ` X) = the_elem (h ` Y) \<Longrightarrow> X = Y"
+proof -
+ fix X Y
+ assume "X \<in> carrier (R Quot (a_kernel R S h))"
+ and "Y \<in> carrier (R Quot (a_kernel R S h))"
+ and Eq: "the_elem (h ` X) = the_elem (h ` Y)"
+ then obtain x y where x: "x \<in> carrier R" "X = (a_kernel R S h) +> x"
+ and y: "y \<in> carrier R" "Y = (a_kernel R S h) +> y"
+ unfolding FactRing_def A_RCOSETS_def' by auto
+ hence "h x = h y" using Eq by simp
+ hence "x \<ominus> y \<in> (a_kernel R S h)"
+ by (simp add: a_minus_def abelian_subgroup.a_rcos_module_imp
+ abelian_subgroup_a_kernel homeq_imp_rcos x(1) y(1))
+ thus "X = Y"
+ by (metis R.a_coset_add_inv1 R.minus_eq abelian_subgroup.a_rcos_const
+ abelian_subgroup_a_kernel additive_subgroup.a_subset additive_subgroup_a_kernel x y)
+qed
+
+lemma (in ring_hom_ring) quot_mem:
+ "\<And>X. X \<in> carrier (R Quot (a_kernel R S h)) \<Longrightarrow> \<exists>x \<in> carrier R. X = (a_kernel R S h) +> x"
+proof -
+ fix X assume "X \<in> carrier (R Quot (a_kernel R S h))"
+ thus "\<exists>x \<in> carrier R. X = (a_kernel R S h) +> x"
+ unfolding FactRing_def RCOSETS_def A_RCOSETS_def by (simp add: a_r_coset_def)
+qed
+
+lemma (in ring_hom_ring) the_elem_wf:
+ "\<And>X. X \<in> carrier (R Quot (a_kernel R S h)) \<Longrightarrow> \<exists>y \<in> carrier S. (h ` X) = { y }"
+proof -
+ fix X assume "X \<in> carrier (R Quot (a_kernel R S h))"
+ then obtain x where x: "x \<in> carrier R" and X: "X = (a_kernel R S h) +> x"
+ using quot_mem by blast
+ hence "\<And>x'. x' \<in> X \<Longrightarrow> h x' = h x"
+ proof -
+ fix x' assume "x' \<in> X" hence "x' \<in> (a_kernel R S h) +> x" using X by simp
+ then obtain k where k: "k \<in> a_kernel R S h" "x' = k \<oplus> x"
+ by (metis R.add.inv_closed R.add.m_assoc R.l_neg R.r_zero
+ abelian_subgroup.a_elemrcos_carrier
+ abelian_subgroup.a_rcos_module_imp abelian_subgroup_a_kernel x)
+ hence "h x' = h k \<oplus>\<^bsub>S\<^esub> h x"
+ by (meson additive_subgroup.a_Hcarr additive_subgroup_a_kernel hom_add x)
+ also have " ... = h x"
+ using k by (auto simp add: x)
+ finally show "h x' = h x" .
+ qed
+ moreover have "h x \<in> h ` X"
+ by (simp add: X homeq_imp_rcos x)
+ ultimately have "(h ` X) = { h x }"
+ by blast
+ thus "\<exists>y \<in> carrier S. (h ` X) = { y }" using x by simp
+qed
+
+corollary (in ring_hom_ring) the_elem_wf':
+ "\<And>X. X \<in> carrier (R Quot (a_kernel R S h)) \<Longrightarrow> \<exists>r \<in> carrier R. (h ` X) = { h r }"
+ using the_elem_wf by (metis quot_mem the_elem_eq the_elem_simp)
+
+lemma (in ring_hom_ring) the_elem_hom:
+ "(\<lambda>X. the_elem (h ` X)) \<in> ring_hom (R Quot (a_kernel R S h)) S"
+proof (rule ring_hom_memI)
+ show "\<And>x. x \<in> carrier (R Quot a_kernel R S h) \<Longrightarrow> the_elem (h ` x) \<in> carrier S"
+ using the_elem_wf by fastforce
+
+ show "the_elem (h ` \<one>\<^bsub>R Quot a_kernel R S h\<^esub>) = \<one>\<^bsub>S\<^esub>"
+ unfolding FactRing_def using the_elem_simp[of "\<one>\<^bsub>R\<^esub>"] by simp
+
+ fix X Y
+ assume "X \<in> carrier (R Quot a_kernel R S h)"
+ and "Y \<in> carrier (R Quot a_kernel R S h)"
+ then obtain x y where x: "x \<in> carrier R" "X = (a_kernel R S h) +> x"
+ and y: "y \<in> carrier R" "Y = (a_kernel R S h) +> y"
+ using quot_mem by blast
+
+ have "X \<otimes>\<^bsub>R Quot a_kernel R S h\<^esub> Y = (a_kernel R S h) +> (x \<otimes> y)"
+ by (simp add: FactRing_def ideal.rcoset_mult_add kernel_is_ideal x y)
+ thus "the_elem (h ` (X \<otimes>\<^bsub>R Quot a_kernel R S h\<^esub> Y)) = the_elem (h ` X) \<otimes>\<^bsub>S\<^esub> the_elem (h ` Y)"
+ by (simp add: x y)
+
+ have "X \<oplus>\<^bsub>R Quot a_kernel R S h\<^esub> Y = (a_kernel R S h) +> (x \<oplus> y)"
+ using ideal.rcos_ring_hom kernel_is_ideal ring_hom_add x y by fastforce
+ thus "the_elem (h ` (X \<oplus>\<^bsub>R Quot a_kernel R S h\<^esub> Y)) = the_elem (h ` X) \<oplus>\<^bsub>S\<^esub> the_elem (h ` Y)"
+ by (simp add: x y)
+qed
+
+lemma (in ring_hom_ring) the_elem_surj:
+ "(\<lambda>X. (the_elem (h ` X))) ` carrier (R Quot (a_kernel R S h)) = (h ` (carrier R))"
+proof
+ show "(\<lambda>X. the_elem (h ` X)) ` carrier (R Quot a_kernel R S h) \<subseteq> h ` carrier R"
+ using the_elem_wf' by fastforce
+next
+ show "h ` carrier R \<subseteq> (\<lambda>X. the_elem (h ` X)) ` carrier (R Quot a_kernel R S h)"
+ proof
+ fix y assume "y \<in> h ` carrier R"
+ then obtain x where x: "x \<in> carrier R" "h x = y"
+ by (metis image_iff)
+ hence "the_elem (h ` ((a_kernel R S h) +> x)) = y" by simp
+ moreover have "(a_kernel R S h) +> x \<in> carrier (R Quot (a_kernel R S h))"
+ unfolding FactRing_def RCOSETS_def A_RCOSETS_def by (auto simp add: x a_r_coset_def)
+ ultimately show "y \<in> (\<lambda>X. (the_elem (h ` X))) ` carrier (R Quot (a_kernel R S h))" by blast
+ qed
+qed
+
+proposition (in ring_hom_ring) FactRing_iso_set_aux:
+ "(\<lambda>X. the_elem (h ` X)) \<in> ring_iso (R Quot (a_kernel R S h)) (S \<lparr> carrier := h ` (carrier R) \<rparr>)"
+proof -
+ have "bij_betw (\<lambda>X. the_elem (h ` X)) (carrier (R Quot a_kernel R S h)) (h ` (carrier R))"
+ unfolding bij_betw_def inj_on_def using the_elem_surj the_elem_inj by simp
+
+ moreover
+ have "(\<lambda>X. the_elem (h ` X)): carrier (R Quot (a_kernel R S h)) \<rightarrow> h ` (carrier R)"
+ using the_elem_wf' by fastforce
+ hence "(\<lambda>X. the_elem (h ` X)) \<in> ring_hom (R Quot (a_kernel R S h)) (S \<lparr> carrier := h ` (carrier R) \<rparr>)"
+ using the_elem_hom the_elem_wf' unfolding ring_hom_def by simp
+
+ ultimately show ?thesis unfolding ring_iso_def using the_elem_hom by simp
+qed
+
+theorem (in ring_hom_ring) FactRing_iso_set:
+ assumes "h ` carrier R = carrier S"
+ shows "(\<lambda>X. the_elem (h ` X)) \<in> ring_iso (R Quot (a_kernel R S h)) S"
+ using FactRing_iso_set_aux assms by auto
+
+corollary (in ring_hom_ring) FactRing_iso:
+ assumes "h ` carrier R = carrier S"
+ shows "R Quot (a_kernel R S h) \<simeq> S"
+ using FactRing_iso_set assms is_ring_iso_def by auto
+
+lemma (in ring_hom_ring) img_is_ring: "ring (S \<lparr> carrier := h ` (carrier R) \<rparr>)"
+proof -
+ let ?the_elem = "\<lambda>X. the_elem (h ` X)"
+ have FactRing_is_ring: "ring (R Quot (a_kernel R S h))"
+ by (simp add: ideal.quotient_is_ring kernel_is_ideal)
+ have "ring ((S \<lparr> carrier := ?the_elem ` (carrier (R Quot (a_kernel R S h))) \<rparr>)
+ \<lparr> one := ?the_elem \<one>\<^bsub>(R Quot (a_kernel R S h))\<^esub>,
+ zero := ?the_elem \<zero>\<^bsub>(R Quot (a_kernel R S h))\<^esub> \<rparr>)"
+ using ring.ring_iso_imp_img_ring[OF FactRing_is_ring, of ?the_elem
+ "S \<lparr> carrier := ?the_elem ` (carrier (R Quot (a_kernel R S h))) \<rparr>"]
+ FactRing_iso_set_aux the_elem_surj by auto
+
+ moreover
+ have "\<zero> \<in> (a_kernel R S h)"
+ using a_kernel_def'[of R S h] by auto
+ hence "\<one> \<in> (a_kernel R S h) +> \<one>"
+ using a_r_coset_def'[of R "a_kernel R S h" \<one>] by force
+ hence "\<one>\<^bsub>S\<^esub> \<in> (h ` ((a_kernel R S h) +> \<one>))"
+ using hom_one by force
+ hence "?the_elem \<one>\<^bsub>(R Quot (a_kernel R S h))\<^esub> = \<one>\<^bsub>S\<^esub>"
+ using the_elem_wf[of "(a_kernel R S h) +> \<one>"] by (simp add: FactRing_def)
+
+ moreover
+ have "\<zero>\<^bsub>S\<^esub> \<in> (h ` (a_kernel R S h))"
+ using a_kernel_def'[of R S h] hom_zero by force
+ hence "\<zero>\<^bsub>S\<^esub> \<in> (h ` \<zero>\<^bsub>(R Quot (a_kernel R S h))\<^esub>)"
+ by (simp add: FactRing_def)
+ hence "?the_elem \<zero>\<^bsub>(R Quot (a_kernel R S h))\<^esub> = \<zero>\<^bsub>S\<^esub>"
+ using the_elem_wf[OF ring.ring_simprules(2)[OF FactRing_is_ring]]
+ by (metis singletonD the_elem_eq)
+
+ ultimately
+ have "ring ((S \<lparr> carrier := h ` (carrier R) \<rparr>) \<lparr> one := \<one>\<^bsub>S\<^esub>, zero := \<zero>\<^bsub>S\<^esub> \<rparr>)"
+ using the_elem_surj by simp
+ thus ?thesis
+ by auto
+qed
+
+lemma (in ring_hom_ring) img_is_cring:
+ assumes "cring S"
+ shows "cring (S \<lparr> carrier := h ` (carrier R) \<rparr>)"
+proof -
+ interpret ring "S \<lparr> carrier := h ` (carrier R) \<rparr>"
+ using img_is_ring .
+ show ?thesis
+ apply unfold_locales
+ using assms unfolding cring_def comm_monoid_def comm_monoid_axioms_def by auto
+qed
+
+lemma (in ring_hom_ring) img_is_domain:
+ assumes "domain S"
+ shows "domain (S \<lparr> carrier := h ` (carrier R) \<rparr>)"
+proof -
+ interpret cring "S \<lparr> carrier := h ` (carrier R) \<rparr>"
+ using img_is_cring assms unfolding domain_def by simp
+ show ?thesis
+ apply unfold_locales
+ using assms unfolding domain_def domain_axioms_def apply auto
+ using hom_closed by blast
+qed
+
+proposition (in ring_hom_ring) primeideal_vimage:
+ assumes "cring R"
+ shows "primeideal P S \<Longrightarrow> primeideal { r \<in> carrier R. h r \<in> P } R"
+proof -
+ assume A: "primeideal P S"
+ hence is_ideal: "ideal P S" unfolding primeideal_def by simp
+ have "ring_hom_ring R (S Quot P) (((+>\<^bsub>S\<^esub>) P) \<circ> h)" (is "ring_hom_ring ?A ?B ?h")
+ using ring_hom_trans[OF homh, of "(+>\<^bsub>S\<^esub>) P" "S Quot P"]
+ ideal.rcos_ring_hom_ring[OF is_ideal] assms
+ unfolding ring_hom_ring_def ring_hom_ring_axioms_def cring_def by simp
+ then interpret hom: ring_hom_ring R "S Quot P" "((+>\<^bsub>S\<^esub>) P) \<circ> h" by simp
+
+ have "inj_on (\<lambda>X. the_elem (?h ` X)) (carrier (R Quot (a_kernel R (S Quot P) ?h)))"
+ using hom.the_elem_inj unfolding inj_on_def by simp
+ moreover
+ have "ideal (a_kernel R (S Quot P) ?h) R"
+ using hom.kernel_is_ideal by auto
+ have hom': "ring_hom_ring (R Quot (a_kernel R (S Quot P) ?h)) (S Quot P) (\<lambda>X. the_elem (?h ` X))"
+ using hom.the_elem_hom hom.kernel_is_ideal
+ by (meson hom.ring_hom_ring_axioms ideal.rcos_ring_hom_ring ring_hom_ring_axioms_def ring_hom_ring_def)
+
+ ultimately
+ have "primeideal (a_kernel R (S Quot P) ?h) R"
+ using ring_hom_ring.inj_on_domain[OF hom'] primeideal.quotient_is_domain[OF A]
+ cring.quot_domain_imp_primeideal[OF assms hom.kernel_is_ideal] by simp
+
+ moreover have "a_kernel R (S Quot P) ?h = { r \<in> carrier R. h r \<in> P }"
+ proof
+ show "a_kernel R (S Quot P) ?h \<subseteq> { r \<in> carrier R. h r \<in> P }"
+ proof
+ fix r assume "r \<in> a_kernel R (S Quot P) ?h"
+ hence r: "r \<in> carrier R" "P +>\<^bsub>S\<^esub> (h r) = P"
+ unfolding a_kernel_def kernel_def FactRing_def by auto
+ hence "h r \<in> P"
+ using S.a_rcosI R.l_zero S.l_zero additive_subgroup.a_subset[OF ideal.axioms(1)[OF is_ideal]]
+ additive_subgroup.zero_closed[OF ideal.axioms(1)[OF is_ideal]] hom_closed by metis
+ thus "r \<in> { r \<in> carrier R. h r \<in> P }" using r by simp
+ qed
+ next
+ show "{ r \<in> carrier R. h r \<in> P } \<subseteq> a_kernel R (S Quot P) ?h"
+ proof
+ fix r assume "r \<in> { r \<in> carrier R. h r \<in> P }"
+ hence r: "r \<in> carrier R" "h r \<in> P" by simp_all
+ hence "?h r = P"
+ by (simp add: S.a_coset_join2 additive_subgroup.a_subgroup ideal.axioms(1) is_ideal)
+ thus "r \<in> a_kernel R (S Quot P) ?h"
+ unfolding a_kernel_def kernel_def FactRing_def using r(1) by auto
+ qed
+ qed
+ ultimately show "primeideal { r \<in> carrier R. h r \<in> P } R" by simp
+qed
+
end
--- a/src/HOL/Algebra/Ring.thy Sun Jul 01 10:58:14 2018 +0200
+++ b/src/HOL/Algebra/Ring.thy Sun Jul 01 17:38:08 2018 +0200
@@ -1,6 +1,7 @@
(* Title: HOL/Algebra/Ring.thy
Author: Clemens Ballarin, started 9 December 1996
- Copyright: Clemens Ballarin
+
+With contributions by Martin Baillon
*)
theory Ring
@@ -333,11 +334,6 @@
and "\<And>x y z. \<lbrakk> x \<in> carrier R; y \<in> carrier R; z \<in> carrier R \<rbrakk> \<Longrightarrow> (x \<oplus> y) \<otimes> z = x \<otimes> z \<oplus> y \<otimes> z"
using assms cring_def apply auto by (simp add: assms cring.axioms(1) ringE(3))
-(*
-lemma (in cring) is_comm_monoid:
- "comm_monoid R"
- by (auto intro!: comm_monoidI m_assoc m_comm)
-*)
lemma (in cring) is_cring:
"cring R" by (rule cring_axioms)
@@ -652,6 +648,15 @@
text \<open>Field would not need to be derived from domain, the properties
for domain follow from the assumptions of field\<close>
+lemma fieldE :
+ fixes R (structure)
+ assumes "field R"
+ shows "cring R"
+ and one_not_zero : "\<one> \<noteq> \<zero>"
+ and integral: "\<And>a b. \<lbrakk> a \<otimes> b = \<zero>; a \<in> carrier R; b \<in> carrier R \<rbrakk> \<Longrightarrow> a = \<zero> \<or> b = \<zero>"
+ and field_Units: "Units R = carrier R - {\<zero>}"
+ using assms unfolding field_def field_axioms_def domain_def domain_axioms_def by simp_all
+
lemma (in cring) cring_fieldI:
assumes field_Units: "Units R = carrier R - {\<zero>}"
shows "field R"
--- a/src/HOL/Algebra/RingHom.thy Sun Jul 01 10:58:14 2018 +0200
+++ b/src/HOL/Algebra/RingHom.thy Sun Jul 01 17:38:08 2018 +0200
@@ -203,4 +203,37 @@
show "x \<in> a_kernel R S h +> a" by (rule homeq_imp_rcos)
qed
+(*contributed by Paulo Emílio de Vilhena*)
+lemma (in ring_hom_ring) inj_on_domain:
+ assumes "inj_on h (carrier R)"
+ shows "domain S \<Longrightarrow> domain R"
+proof -
+ assume A: "domain S" show "domain R"
+ proof
+ have "h \<one> = \<one>\<^bsub>S\<^esub> \<and> h \<zero> = \<zero>\<^bsub>S\<^esub>" by simp
+ hence "h \<one> \<noteq> h \<zero>"
+ using domain.one_not_zero[OF A] by simp
+ thus "\<one> \<noteq> \<zero>"
+ using assms unfolding inj_on_def by fastforce
+ next
+ fix a b
+ assume a: "a \<in> carrier R"
+ and b: "b \<in> carrier R"
+ have "h (a \<otimes> b) = (h a) \<otimes>\<^bsub>S\<^esub> (h b)" by (simp add: a b)
+ also have " ... = (h b) \<otimes>\<^bsub>S\<^esub> (h a)" using a b A cringE(1)[of S]
+ by (simp add: cring.cring_simprules(14) domain_def)
+ also have " ... = h (b \<otimes> a)" by (simp add: a b)
+ finally have "h (a \<otimes> b) = h (b \<otimes> a)" .
+ thus "a \<otimes> b = b \<otimes> a"
+ using assms a b unfolding inj_on_def by simp
+
+ assume ab: "a \<otimes> b = \<zero>"
+ hence "h (a \<otimes> b) = \<zero>\<^bsub>S\<^esub>" by simp
+ hence "(h a) \<otimes>\<^bsub>S\<^esub> (h b) = \<zero>\<^bsub>S\<^esub>" using a b by simp
+ hence "h a = \<zero>\<^bsub>S\<^esub> \<or> h b = \<zero>\<^bsub>S\<^esub>" using a b domain.integral[OF A] by simp
+ thus "a = \<zero> \<or> b = \<zero>"
+ using a b assms unfolding inj_on_def by force
+ qed
+qed
+
end
--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Sun Jul 01 10:58:14 2018 +0200
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Sun Jul 01 17:38:08 2018 +0200
@@ -774,7 +774,27 @@
ultimately show ?thesis unfolding valid_path_def piecewise_C1_differentiable_on_def path_def
using \<open>finite S\<close> by auto
qed
-
+
+lemma valid_path_uminus_comp[simp]:
+ fixes g::"real \<Rightarrow> 'a ::real_normed_field"
+ shows "valid_path (uminus \<circ> g) \<longleftrightarrow> valid_path g"
+proof
+ show "valid_path g \<Longrightarrow> valid_path (uminus \<circ> g)" for g::"real \<Rightarrow> 'a"
+ by (auto intro!: valid_path_compose derivative_intros simp add: deriv_linear[of "-1",simplified])
+ then show "valid_path g" when "valid_path (uminus \<circ> g)"
+ by (metis fun.map_comp group_add_class.minus_comp_minus id_comp that)
+qed
+
+lemma valid_path_offset[simp]:
+ shows "valid_path (\<lambda>t. g t - z) \<longleftrightarrow> valid_path g"
+proof
+ show *: "valid_path (g::real\<Rightarrow>'a) \<Longrightarrow> valid_path (\<lambda>t. g t - z)" for g z
+ unfolding valid_path_def
+ by (fastforce intro:derivative_intros C1_differentiable_imp_piecewise piecewise_C1_differentiable_diff)
+ show "valid_path (\<lambda>t. g t - z) \<Longrightarrow> valid_path g"
+ using *[of "\<lambda>t. g t - z" "-z",simplified] .
+qed
+
subsection\<open>Contour Integrals along a path\<close>
@@ -3554,6 +3574,19 @@
"(\<And>t. \<lbrakk>0 \<le> t; t \<le> 1\<rbrakk> \<Longrightarrow> p t = q t) \<Longrightarrow> winding_number p z = winding_number q z"
by (simp add: winding_number_def winding_number_prop_def pathstart_def pathfinish_def)
+lemma winding_number_constI:
+ assumes "c\<noteq>z" "\<And>t. \<lbrakk>0\<le>t; t\<le>1\<rbrakk> \<Longrightarrow> g t = c"
+ shows "winding_number g z = 0"
+proof -
+ have "winding_number g z = winding_number (linepath c c) z"
+ apply (rule winding_number_cong)
+ using assms unfolding linepath_def by auto
+ moreover have "winding_number (linepath c c) z =0"
+ apply (rule winding_number_trivial)
+ using assms by auto
+ ultimately show ?thesis by auto
+qed
+
lemma winding_number_offset: "winding_number p z = winding_number (\<lambda>w. p w - z) 0"
unfolding winding_number_def
proof (intro ext arg_cong [where f = Eps] arg_cong [where f = All] imp_cong refl, safe)
@@ -4812,8 +4845,7 @@
winding_number (subpath u w g) z"
apply (rule trans [OF winding_number_join [THEN sym]
winding_number_homotopic_paths [OF homotopic_join_subpaths]])
-apply (auto dest: path_image_subpath_subset)
-done
+ using path_image_subpath_subset by auto
subsection\<open>Partial circle path\<close>
@@ -4829,6 +4861,11 @@
"pathfinish(part_circlepath z r s t) = z + r*exp(\<i>*t)"
by (metis part_circlepath_def pathfinish_def pathfinish_linepath)
+lemma reversepath_part_circlepath[simp]:
+ "reversepath (part_circlepath z r s t) = part_circlepath z r t s"
+ unfolding part_circlepath_def reversepath_def linepath_def
+ by (auto simp:algebra_simps)
+
proposition has_vector_derivative_part_circlepath [derivative_intros]:
"((part_circlepath z r s t) has_vector_derivative
(\<i> * r * (of_real t - of_real s) * exp(\<i> * linepath s t x)))
--- a/src/HOL/Analysis/Change_Of_Vars.thy Sun Jul 01 10:58:14 2018 +0200
+++ b/src/HOL/Analysis/Change_Of_Vars.thy Sun Jul 01 17:38:08 2018 +0200
@@ -2937,7 +2937,7 @@
moreover have "integral (g ` S) (h n) \<le> integral S (\<lambda>x. ?D x * f (g x))" for n
using hint by (blast intro: le order_trans)
ultimately show ?thesis
- by (auto intro: Lim_bounded_ereal)
+ by (auto intro: Lim_bounded)
qed
--- a/src/HOL/Analysis/Complex_Transcendental.thy Sun Jul 01 10:58:14 2018 +0200
+++ b/src/HOL/Analysis/Complex_Transcendental.thy Sun Jul 01 17:38:08 2018 +0200
@@ -1177,21 +1177,6 @@
obtains w where "w \<noteq> 0" "z = w ^ n"
by (metis exists_complex_root [of n z] assms power_0_left)
-subsection\<open>The Unwinding Number and the Ln-product Formula\<close>
-
-text\<open>Note that in this special case the unwinding number is -1, 0 or 1.\<close>
-
-definition unwinding :: "complex \<Rightarrow> complex" where
- "unwinding(z) = (z - Ln(exp z)) / (of_real(2*pi) * \<i>)"
-
-lemma unwinding_2pi: "(2*pi) * \<i> * unwinding(z) = z - Ln(exp z)"
- by (simp add: unwinding_def)
-
-lemma Ln_times_unwinding:
- "w \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> Ln(w * z) = Ln(w) + Ln(z) - (2*pi) * \<i> * unwinding(Ln w + Ln z)"
- using unwinding_2pi by (simp add: exp_add)
-
-
subsection\<open>Derivative of Ln away from the branch cut\<close>
lemma
@@ -1465,6 +1450,10 @@
using mpi_less_Im_Ln Im_Ln_le_pi
by (force simp: Ln_times)
+corollary Ln_times_Reals:
+ "\<lbrakk>r \<in> Reals; Re r > 0; z \<noteq> 0\<rbrakk> \<Longrightarrow> Ln(r * z) = ln (Re r) + Ln(z)"
+ using Ln_Reals_eq Ln_times_of_real by fastforce
+
corollary Ln_divide_of_real:
"\<lbrakk>r > 0; z \<noteq> 0\<rbrakk> \<Longrightarrow> Ln(z / of_real r) = Ln(z) - ln r"
using Ln_times_of_real [of "inverse r" z]
@@ -1571,10 +1560,10 @@
subsection\<open>The Argument of a Complex Number\<close>
+text\<open>Finally: it's is defined for the same interval as the complex logarithm: $(-\pi,\pi]$.\<close>
+
definition Arg :: "complex \<Rightarrow> real" where "Arg z \<equiv> (if z = 0 then 0 else Im (Ln z))"
-text\<open>Finally the Argument is defined for the same interval as the complex logarithm: $(-\pi,\pi]$.\<close>
-
lemma Arg_of_real: "Arg (of_real r) = (if r<0 then pi else 0)"
by (simp add: Im_Ln_eq_pi Arg_def)
@@ -1588,6 +1577,9 @@
using assms exp_Ln exp_eq_polar
by (auto simp: Arg_def)
+lemma is_Arg_Arg: "z \<noteq> 0 \<Longrightarrow> is_Arg z (Arg z)"
+ by (simp add: Arg_eq is_Arg_def)
+
lemma Argument_exists:
assumes "z \<noteq> 0" and R: "R = {r-pi<..r+pi}"
obtains s where "is_Arg z s" "s\<in>R"
@@ -1784,6 +1776,47 @@
using continuous_at_Arg continuous_at_imp_continuous_within by blast
+subsection\<open>The Unwinding Number and the Ln-product Formula\<close>
+
+text\<open>Note that in this special case the unwinding number is -1, 0 or 1. But it's always an integer.\<close>
+
+lemma is_Arg_exp_Im: "is_Arg (exp z) (Im z)"
+ using exp_eq_polar is_Arg_def norm_exp_eq_Re by auto
+
+lemma is_Arg_exp_diff_2pi:
+ assumes "is_Arg (exp z) \<theta>"
+ shows "\<exists>k. Im z - of_int k * (2 * pi) = \<theta>"
+proof (intro exI is_Arg_eqI)
+ let ?k = "\<lfloor>(Im z - \<theta>) / (2 * pi)\<rfloor>"
+ show "is_Arg (exp z) (Im z - real_of_int ?k * (2 * pi))"
+ by (metis diff_add_cancel is_Arg_2pi_iff is_Arg_exp_Im)
+ show "\<bar>Im z - real_of_int ?k * (2 * pi) - \<theta>\<bar> < 2 * pi"
+ using floor_divide_upper [of "2*pi" "Im z - \<theta>"] floor_divide_lower [of "2*pi" "Im z - \<theta>"]
+ by (auto simp: algebra_simps abs_if)
+qed (auto simp: is_Arg_exp_Im assms)
+
+lemma Arg_exp_diff_2pi: "\<exists>k. Im z - of_int k * (2 * pi) = Arg (exp z)"
+ using is_Arg_exp_diff_2pi [OF is_Arg_Arg] by auto
+
+lemma unwinding_in_Ints: "(z - Ln(exp z)) / (of_real(2*pi) * \<i>) \<in> \<int>"
+ using Arg_exp_diff_2pi [of z]
+ by (force simp: Ints_def image_def field_simps Arg_def intro!: complex_eqI)
+
+definition unwinding :: "complex \<Rightarrow> int" where
+ "unwinding z \<equiv> THE k. of_int k = (z - Ln(exp z)) / (of_real(2*pi) * \<i>)"
+
+lemma unwinding: "of_int (unwinding z) = (z - Ln(exp z)) / (of_real(2*pi) * \<i>)"
+ using unwinding_in_Ints [of z]
+ unfolding unwinding_def Ints_def by force
+
+lemma unwinding_2pi: "(2*pi) * \<i> * unwinding(z) = z - Ln(exp z)"
+ by (simp add: unwinding)
+
+lemma Ln_times_unwinding:
+ "w \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> Ln(w * z) = Ln(w) + Ln(z) - (2*pi) * \<i> * unwinding(Ln w + Ln z)"
+ using unwinding_2pi by (simp add: exp_add)
+
+
subsection\<open>Relation between Ln and Arg2pi, and hence continuity of Arg2pi\<close>
lemma Arg2pi_Ln:
--- a/src/HOL/Analysis/Interval_Integral.thy Sun Jul 01 10:58:14 2018 +0200
+++ b/src/HOL/Analysis/Interval_Integral.thy Sun Jul 01 17:38:08 2018 +0200
@@ -875,7 +875,7 @@
using A apply (auto simp: einterval_def tendsto_at_iff_sequentially comp_def)
by (drule_tac x = "\<lambda>i. ereal (l i)" in spec, auto)
hence A3: "\<And>i. g (l i) \<ge> A"
- by (intro decseq_le, auto simp: decseq_def)
+ by (intro decseq_ge, auto simp: decseq_def)
have B2: "(\<lambda>i. g (u i)) \<longlonglongrightarrow> B"
using B apply (auto simp: einterval_def tendsto_at_iff_sequentially comp_def)
by (drule_tac x = "\<lambda>i. ereal (u i)" in spec, auto)
@@ -972,7 +972,7 @@
using A apply (auto simp: einterval_def tendsto_at_iff_sequentially comp_def)
by (drule_tac x = "\<lambda>i. ereal (l i)" in spec, auto)
hence A3: "\<And>i. g (l i) \<ge> A"
- by (intro decseq_le, auto simp: decseq_def)
+ by (intro decseq_ge, auto simp: decseq_def)
have B2: "(\<lambda>i. g (u i)) \<longlonglongrightarrow> B"
using B apply (auto simp: einterval_def tendsto_at_iff_sequentially comp_def)
by (drule_tac x = "\<lambda>i. ereal (u i)" in spec, auto)
--- a/src/HOL/Analysis/Measure_Space.thy Sun Jul 01 10:58:14 2018 +0200
+++ b/src/HOL/Analysis/Measure_Space.thy Sun Jul 01 17:38:08 2018 +0200
@@ -389,7 +389,7 @@
show "range (\<lambda>i. A i - (\<Inter>i. A i)) \<subseteq> M" "(\<Inter>i. A i - (\<Inter>i. A i)) = {}"
using A by auto
qed
- from INF_Lim_ereal[OF decseq_f this]
+ from INF_Lim[OF decseq_f this]
have "(INF n. f (A n - (\<Inter>i. A i))) = 0" .
moreover have "(INF n. f (\<Inter>i. A i)) = f (\<Inter>i. A i)"
by auto
@@ -2020,7 +2020,7 @@
finally show ?thesis by simp
qed
ultimately have "emeasure M (\<Union>N. B N) \<le> ennreal (\<Sum>n. measure M (A n))"
- by (simp add: Lim_bounded_ereal)
+ by (simp add: Lim_bounded)
then show "emeasure M (\<Union>n. A n) \<le> (\<Sum>n. measure M (A n))"
unfolding B_def by (metis UN_UN_flatten UN_lessThan_UNIV)
then show "emeasure M (\<Union>n. A n) < \<infinity>"
--- a/src/HOL/Analysis/Path_Connected.thy Sun Jul 01 10:58:14 2018 +0200
+++ b/src/HOL/Analysis/Path_Connected.thy Sun Jul 01 17:38:08 2018 +0200
@@ -929,10 +929,10 @@
done
lemma path_image_subpath_subset:
- "\<lbrakk>path g; u \<in> {0..1}; v \<in> {0..1}\<rbrakk> \<Longrightarrow> path_image(subpath u v g) \<subseteq> path_image g"
+ "\<lbrakk>u \<in> {0..1}; v \<in> {0..1}\<rbrakk> \<Longrightarrow> path_image(subpath u v g) \<subseteq> path_image g"
apply (simp add: closed_segment_real_eq image_affinity_atLeastAtMost path_image_subpath)
apply (auto simp: path_image_def)
- done
+ done
lemma join_subpaths_middle: "subpath (0) ((1 / 2)) p +++ subpath ((1 / 2)) 1 p = p"
by (rule ext) (simp add: joinpaths_def subpath_def divide_simps)
@@ -1751,14 +1751,14 @@
by (simp add: path_connected_def)
qed
-lemma path_component: "path_component s x y \<longleftrightarrow> (\<exists>t. path_connected t \<and> t \<subseteq> s \<and> x \<in> t \<and> y \<in> t)"
+lemma path_component: "path_component S x y \<longleftrightarrow> (\<exists>t. path_connected t \<and> t \<subseteq> S \<and> x \<in> t \<and> y \<in> t)"
apply (intro iffI)
apply (metis path_connected_path_image path_defs(5) pathfinish_in_path_image pathstart_in_path_image)
using path_component_of_subset path_connected_component by blast
lemma path_component_path_component [simp]:
- "path_component_set (path_component_set s x) x = path_component_set s x"
-proof (cases "x \<in> s")
+ "path_component_set (path_component_set S x) x = path_component_set S x"
+proof (cases "x \<in> S")
case True show ?thesis
apply (rule subset_antisym)
apply (simp add: path_component_subset)
@@ -1769,11 +1769,11 @@
qed
lemma path_component_subset_connected_component:
- "(path_component_set s x) \<subseteq> (connected_component_set s x)"
-proof (cases "x \<in> s")
+ "(path_component_set S x) \<subseteq> (connected_component_set S x)"
+proof (cases "x \<in> S")
case True show ?thesis
apply (rule connected_component_maximal)
- apply (auto simp: True path_component_subset path_component_refl path_connected_imp_connected path_connected_path_component)
+ apply (auto simp: True path_component_subset path_component_refl path_connected_imp_connected)
done
next
case False then show ?thesis
@@ -1784,11 +1784,11 @@
lemma path_connected_linear_image:
fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
- assumes "path_connected s" "bounded_linear f"
- shows "path_connected(f ` s)"
+ assumes "path_connected S" "bounded_linear f"
+ shows "path_connected(f ` S)"
by (auto simp: linear_continuous_on assms path_connected_continuous_image)
-lemma is_interval_path_connected: "is_interval s \<Longrightarrow> path_connected s"
+lemma is_interval_path_connected: "is_interval S \<Longrightarrow> path_connected S"
by (simp add: convex_imp_path_connected is_interval_convex)
lemma linear_homeomorphism_image:
--- a/src/HOL/Analysis/Summation_Tests.thy Sun Jul 01 10:58:14 2018 +0200
+++ b/src/HOL/Analysis/Summation_Tests.thy Sun Jul 01 17:38:08 2018 +0200
@@ -752,7 +752,7 @@
assumes lim: "(\<lambda>n. ereal (norm (f n) / norm (f (Suc n)))) \<longlonglongrightarrow> c"
shows "conv_radius f = c"
proof (rule conv_radius_eqI')
- show "c \<ge> 0" by (intro Lim_bounded2_ereal[OF lim]) simp_all
+ show "c \<ge> 0" by (intro Lim_bounded2[OF lim]) simp_all
next
fix r assume r: "0 < r" "ereal r < c"
let ?l = "liminf (\<lambda>n. ereal (norm (f n * of_real r ^ n) / norm (f (Suc n) * of_real r ^ Suc n)))"
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy Sun Jul 01 10:58:14 2018 +0200
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy Sun Jul 01 17:38:08 2018 +0200
@@ -2068,32 +2068,45 @@
lemma islimpt_EMPTY[simp]: "\<not> x islimpt {}"
by (auto simp: islimpt_def)
+lemma finite_ball_include:
+ fixes a :: "'a::metric_space"
+ assumes "finite S"
+ shows "\<exists>e>0. S \<subseteq> ball a e"
+ using assms
+proof induction
+ case (insert x S)
+ then obtain e0 where "e0>0" and e0:"S \<subseteq> ball a e0" by auto
+ define e where "e = max e0 (2 * dist a x)"
+ have "e>0" unfolding e_def using \<open>e0>0\<close> by auto
+ moreover have "insert x S \<subseteq> ball a e"
+ using e0 \<open>e>0\<close> unfolding e_def by auto
+ ultimately show ?case by auto
+qed (auto intro: zero_less_one)
+
lemma finite_set_avoid:
fixes a :: "'a::metric_space"
- assumes fS: "finite S"
+ assumes "finite S"
shows "\<exists>d>0. \<forall>x\<in>S. x \<noteq> a \<longrightarrow> d \<le> dist a x"
-proof (induct rule: finite_induct[OF fS])
- case 1
- then show ?case by (auto intro: zero_less_one)
-next
- case (2 x F)
- from 2 obtain d where d: "d > 0" "\<forall>x\<in>F. x \<noteq> a \<longrightarrow> d \<le> dist a x"
+ using assms
+proof induction
+ case (insert x S)
+ then obtain d where "d > 0" and d: "\<forall>x\<in>S. x \<noteq> a \<longrightarrow> d \<le> dist a x"
by blast
show ?case
proof (cases "x = a")
case True
- with d show ?thesis by auto
+ with \<open>d > 0 \<close>d show ?thesis by auto
next
case False
let ?d = "min d (dist a x)"
- from False d(1) have dp: "?d > 0"
+ from False \<open>d > 0\<close> have dp: "?d > 0"
by auto
- from d have d': "\<forall>x\<in>F. x \<noteq> a \<longrightarrow> ?d \<le> dist a x"
+ from d have d': "\<forall>x\<in>S. x \<noteq> a \<longrightarrow> ?d \<le> dist a x"
by auto
with dp False show ?thesis
- by (auto intro!: exI[where x="?d"])
+ by (metis insert_iff le_less min_less_iff_conj not_less)
qed
-qed
+qed (auto intro: zero_less_one)
lemma islimpt_Un: "x islimpt (S \<union> T) \<longleftrightarrow> x islimpt S \<or> x islimpt T"
by (simp add: islimpt_iff_eventually eventually_conj_iff)
--- a/src/HOL/Computational_Algebra/Polynomial.thy Sun Jul 01 10:58:14 2018 +0200
+++ b/src/HOL/Computational_Algebra/Polynomial.thy Sun Jul 01 17:38:08 2018 +0200
@@ -9,7 +9,7 @@
theory Polynomial
imports
- HOL.Deriv
+ Complex_Main
"HOL-Library.More_List"
"HOL-Library.Infinite_Set"
Factorial_Ring
@@ -1832,10 +1832,13 @@
by simp
qed
-(* Next two lemmas contributed by Wenda Li *)
+(* Next three lemmas contributed by Wenda Li *)
lemma order_1_eq_0 [simp]:"order x 1 = 0"
by (metis order_root poly_1 zero_neq_one)
+lemma order_uminus[simp]: "order x (-p) = order x p"
+ by (metis neg_equal_0_iff_equal order_smult smult_1_left smult_minus_left)
+
lemma order_power_n_n: "order a ([:-a,1:]^n)=n"
proof (induct n) (*might be proved more concisely using nat_less_induct*)
case 0
@@ -2575,17 +2578,28 @@
lemma poly_DERIV [simp]: "DERIV (\<lambda>x. poly p x) x :> poly (pderiv p) x"
by (induct p) (auto intro!: derivative_eq_intros simp add: pderiv_pCons)
+lemma poly_isCont[simp]:
+ fixes x::"'a::real_normed_field"
+ shows "isCont (\<lambda>x. poly p x) x"
+by (rule poly_DERIV [THEN DERIV_isCont])
+
+lemma tendsto_poly [tendsto_intros]: "(f \<longlongrightarrow> a) F \<Longrightarrow> ((\<lambda>x. poly p (f x)) \<longlongrightarrow> poly p a) F"
+ for f :: "_ \<Rightarrow> 'a::real_normed_field"
+ by (rule isCont_tendsto_compose [OF poly_isCont])
+
+lemma continuous_within_poly: "continuous (at z within s) (poly p)"
+ for z :: "'a::{real_normed_field}"
+ by (simp add: continuous_within tendsto_poly)
+
+lemma continuous_poly [continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. poly p (f x))"
+ for f :: "_ \<Rightarrow> 'a::real_normed_field"
+ unfolding continuous_def by (rule tendsto_poly)
+
lemma continuous_on_poly [continuous_intros]:
fixes p :: "'a :: {real_normed_field} poly"
assumes "continuous_on A f"
shows "continuous_on A (\<lambda>x. poly p (f x))"
-proof -
- have "continuous_on A (\<lambda>x. (\<Sum>i\<le>degree p. (f x) ^ i * coeff p i))"
- by (intro continuous_intros assms)
- also have "\<dots> = (\<lambda>x. poly p (f x))"
- by (rule ext) (simp add: poly_altdef mult_ac)
- finally show ?thesis .
-qed
+ by (metis DERIV_continuous_on assms continuous_on_compose2 poly_DERIV subset_UNIV)
text \<open>Consequences of the derivative theorem above.\<close>
@@ -2593,10 +2607,6 @@
for x :: real
by (simp add: real_differentiable_def) (blast intro: poly_DERIV)
-lemma poly_isCont[simp]: "isCont (\<lambda>x. poly p x) x"
- for x :: real
- by (rule poly_DERIV [THEN DERIV_isCont])
-
lemma poly_IVT_pos: "a < b \<Longrightarrow> poly p a < 0 \<Longrightarrow> 0 < poly p b \<Longrightarrow> \<exists>x. a < x \<and> x < b \<and> poly p x = 0"
for a b :: real
using IVT_objl [of "poly p" a 0 b] by (auto simp add: order_le_less)
--- a/src/HOL/Euclidean_Division.thy Sun Jul 01 10:58:14 2018 +0200
+++ b/src/HOL/Euclidean_Division.thy Sun Jul 01 17:38:08 2018 +0200
@@ -1638,7 +1638,7 @@
by (simp only: *, simp only: l q divide_int_unfold)
(auto simp add: sgn_mult sgn_0_0 sgn_1_pos algebra_simps dest: dvd_imp_le)
qed
-qed (use mult_le_mono2 [of 1] in \<open>auto simp add: division_segment_int_def not_le sign_simps abs_mult sgn_mult abs_mod_less sgn_mod nat_mult_distrib\<close>)
+qed (use mult_le_mono2 [of 1] in \<open>auto simp add: division_segment_int_def not_le zero_less_mult_iff mult_less_0_iff abs_mult sgn_mult abs_mod_less sgn_mod nat_mult_distrib\<close>)
end
--- a/src/HOL/Fields.thy Sun Jul 01 10:58:14 2018 +0200
+++ b/src/HOL/Fields.thy Sun Jul 01 17:38:08 2018 +0200
@@ -843,10 +843,6 @@
of positivity/negativity needed for \<open>field_simps\<close>. Have not added \<open>sign_simps\<close> to \<open>field_simps\<close> because the former can lead to case
explosions.\<close>
-lemmas sign_simps = algebra_simps zero_less_mult_iff mult_less_0_iff
-
-lemmas (in -) sign_simps = algebra_simps zero_less_mult_iff mult_less_0_iff
-
(* Only works once linear arithmetic is installed:
text{*An example:*}
lemma fixes a b c d e f :: "'a::linordered_field"
--- a/src/HOL/Library/Extended_Real.thy Sun Jul 01 10:58:14 2018 +0200
+++ b/src/HOL/Library/Extended_Real.thy Sun Jul 01 17:38:08 2018 +0200
@@ -2921,17 +2921,6 @@
lemma Lim_bounded_PInfty2: "f \<longlonglongrightarrow> l \<Longrightarrow> \<forall>n\<ge>N. f n \<le> ereal B \<Longrightarrow> l \<noteq> \<infinity>"
using LIMSEQ_le_const2[of f l "ereal B"] by fastforce
-lemma Lim_bounded_ereal: "f \<longlonglongrightarrow> (l :: 'a::linorder_topology) \<Longrightarrow> \<forall>n\<ge>M. f n \<le> C \<Longrightarrow> l \<le> C"
- by (intro LIMSEQ_le_const2) auto
-
-lemma Lim_bounded2_ereal:
- assumes lim:"f \<longlonglongrightarrow> (l :: 'a::linorder_topology)"
- and ge: "\<forall>n\<ge>N. f n \<ge> C"
- shows "l \<ge> C"
- using ge
- by (intro tendsto_le[OF trivial_limit_sequentially lim tendsto_const])
- (auto simp: eventually_sequentially)
-
lemma real_of_ereal_mult[simp]:
fixes a b :: ereal
shows "real_of_ereal (a * b) = real_of_ereal a * real_of_ereal b"
@@ -3341,7 +3330,7 @@
assumes "\<forall>N. (\<Sum>n<N. f n) \<le> x"
and pos: "\<And>n. 0 \<le> f n"
shows "suminf f \<le> x"
-proof (rule Lim_bounded_ereal)
+proof (rule Lim_bounded)
have "summable f" using pos[THEN summable_ereal_pos] .
then show "(\<lambda>N. \<Sum>n<N. f n) \<longlonglongrightarrow> suminf f"
by (auto dest!: summable_sums simp: sums_def atLeast0LessThan)
@@ -3879,66 +3868,6 @@
shows "X \<longlonglongrightarrow> -\<infinity> \<longleftrightarrow> limsup X = -\<infinity>"
by (metis Limsup_MInfty trivial_limit_sequentially)
-lemma ereal_lim_mono:
- fixes X Y :: "nat \<Rightarrow> 'a::linorder_topology"
- assumes "\<And>n. N \<le> n \<Longrightarrow> X n \<le> Y n"
- and "X \<longlonglongrightarrow> x"
- and "Y \<longlonglongrightarrow> y"
- shows "x \<le> y"
- using assms(1) by (intro LIMSEQ_le[OF assms(2,3)]) auto
-
-lemma incseq_le_ereal:
- fixes X :: "nat \<Rightarrow> 'a::linorder_topology"
- assumes inc: "incseq X"
- and lim: "X \<longlonglongrightarrow> L"
- shows "X N \<le> L"
- using inc
- by (intro ereal_lim_mono[of N, OF _ tendsto_const lim]) (simp add: incseq_def)
-
-lemma decseq_ge_ereal:
- assumes dec: "decseq X"
- and lim: "X \<longlonglongrightarrow> (L::'a::linorder_topology)"
- shows "X N \<ge> L"
- using dec by (intro ereal_lim_mono[of N, OF _ lim tendsto_const]) (simp add: decseq_def)
-
-lemma bounded_abs:
- fixes a :: real
- assumes "a \<le> x"
- and "x \<le> b"
- shows "\<bar>x\<bar> \<le> max \<bar>a\<bar> \<bar>b\<bar>"
- by (metis abs_less_iff assms leI le_max_iff_disj
- less_eq_real_def less_le_not_le less_minus_iff minus_minus)
-
-lemma ereal_Sup_lim:
- fixes a :: "'a::{complete_linorder,linorder_topology}"
- assumes "\<And>n. b n \<in> s"
- and "b \<longlonglongrightarrow> a"
- shows "a \<le> Sup s"
- by (metis Lim_bounded_ereal assms complete_lattice_class.Sup_upper)
-
-lemma ereal_Inf_lim:
- fixes a :: "'a::{complete_linorder,linorder_topology}"
- assumes "\<And>n. b n \<in> s"
- and "b \<longlonglongrightarrow> a"
- shows "Inf s \<le> a"
- by (metis Lim_bounded2_ereal assms complete_lattice_class.Inf_lower)
-
-lemma SUP_Lim_ereal:
- fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
- assumes inc: "incseq X"
- and l: "X \<longlonglongrightarrow> l"
- shows "(SUP n. X n) = l"
- using LIMSEQ_SUP[OF inc] tendsto_unique[OF trivial_limit_sequentially l]
- by simp
-
-lemma INF_Lim_ereal:
- fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
- assumes dec: "decseq X"
- and l: "X \<longlonglongrightarrow> l"
- shows "(INF n. X n) = l"
- using LIMSEQ_INF[OF dec] tendsto_unique[OF trivial_limit_sequentially l]
- by simp
-
lemma SUP_eq_LIMSEQ:
assumes "mono f"
shows "(SUP n. ereal (f n)) = ereal x \<longleftrightarrow> f \<longlonglongrightarrow> x"
@@ -3949,7 +3878,7 @@
assume "f \<longlonglongrightarrow> x"
then have "(\<lambda>i. ereal (f i)) \<longlonglongrightarrow> ereal x"
by auto
- from SUP_Lim_ereal[OF inc this] show "(SUP n. ereal (f n)) = ereal x" .
+ from SUP_Lim[OF inc this] show "(SUP n. ereal (f n)) = ereal x" .
next
assume "(SUP n. ereal (f n)) = ereal x"
with LIMSEQ_SUP[OF inc] show "f \<longlonglongrightarrow> x" by auto
--- a/src/HOL/Library/code_lazy.ML Sun Jul 01 10:58:14 2018 +0200
+++ b/src/HOL/Library/code_lazy.ML Sun Jul 01 17:38:08 2018 +0200
@@ -487,9 +487,9 @@
val add_lazy_ctr_thms = fold (Code.add_eqn_global o rpair true) ctrs_lazy_thms
val add_lazy_case_thms =
fold Code.del_eqn_global case_thms
- #> Code.add_eqn_global (case_lazy_thm, false)
+ #> Code.add_eqn_global (case_lazy_thm, true)
val add_eager_case_thms = Code.del_eqn_global case_lazy_thm
- #> fold (Code.add_eqn_global o rpair false) case_thms
+ #> fold (Code.add_eqn_global o rpair true) case_thms
val delay_dummy_thm = (pat_def_thm RS @{thm symmetric})
|> Drule.infer_instantiate' lthy10
--- a/src/HOL/Limits.thy Sun Jul 01 10:58:14 2018 +0200
+++ b/src/HOL/Limits.thy Sun Jul 01 17:38:08 2018 +0200
@@ -1347,12 +1347,17 @@
unfolding filterlim_at_bot eventually_at_top_dense
by (metis leI less_minus_iff order_less_asym)
-lemma at_top_mirror: "at_top = filtermap uminus (at_bot :: real filter)"
- by (rule filtermap_fun_inverse[symmetric, of uminus])
- (auto intro: filterlim_uminus_at_bot_at_top filterlim_uminus_at_top_at_bot)
-
-lemma at_bot_mirror: "at_bot = filtermap uminus (at_top :: real filter)"
- unfolding at_top_mirror filtermap_filtermap by (simp add: filtermap_ident)
+lemma at_bot_mirror :
+ shows "(at_bot::('a::{ordered_ab_group_add,linorder} filter)) = filtermap uminus at_top"
+ apply (rule filtermap_fun_inverse[of uminus, symmetric])
+ subgoal unfolding filterlim_at_top eventually_at_bot_linorder using le_minus_iff by auto
+ subgoal unfolding filterlim_at_bot eventually_at_top_linorder using minus_le_iff by auto
+ by auto
+
+lemma at_top_mirror :
+ shows "(at_top::('a::{ordered_ab_group_add,linorder} filter)) = filtermap uminus at_bot"
+ apply (subst at_bot_mirror)
+ by (auto simp add: filtermap_filtermap)
lemma filterlim_at_top_mirror: "(LIM x at_top. f x :> F) \<longleftrightarrow> (LIM x at_bot. f (-x::real) :> F)"
unfolding filterlim_def at_top_mirror filtermap_filtermap ..
@@ -2294,7 +2299,7 @@
obtain L where "X \<longlonglongrightarrow> L"
by (auto simp: convergent_def monoseq_def decseq_def)
with \<open>decseq X\<close> show "\<exists>L. X \<longlonglongrightarrow> L \<and> (\<forall>i. L \<le> X i)"
- by (auto intro!: exI[of _ L] decseq_le)
+ by (auto intro!: exI[of _ L] decseq_ge)
qed
--- a/src/HOL/Metis_Examples/Big_O.thy Sun Jul 01 10:58:14 2018 +0200
+++ b/src/HOL/Metis_Examples/Big_O.thy Sun Jul 01 17:38:08 2018 +0200
@@ -457,7 +457,7 @@
hence "\<exists>(v::'a) (u::'a) SKF\<^sub>7::'a \<Rightarrow> 'b. \<bar>inverse c\<bar> * \<bar>g (SKF\<^sub>7 (u * v))\<bar> \<le> u * (v * \<bar>f (SKF\<^sub>7 (u * v))\<bar>)"
by (metis mult_left_mono)
then show "\<exists>ca::'a. \<forall>x::'b. inverse \<bar>c\<bar> * \<bar>g x\<bar> \<le> ca * \<bar>f x\<bar>"
- using A2 F4 by (metis F1 \<open>0 < \<bar>inverse c\<bar>\<close> linordered_field_class.sign_simps(23) mult_le_cancel_left_pos)
+ using A2 F4 by (metis F1 \<open>0 < \<bar>inverse c\<bar>\<close> mult.assoc mult_le_cancel_left_pos)
qed
lemma bigo_const_mult6 [intro]: "(\<lambda>x. c) *o O(f) <= O(f)"
--- a/src/HOL/Num.thy Sun Jul 01 10:58:14 2018 +0200
+++ b/src/HOL/Num.thy Sun Jul 01 17:38:08 2018 +0200
@@ -1282,14 +1282,20 @@
numeral for 1 reduces the number of special cases.
\<close>
-lemma mult_1s:
+lemma mult_1s_semiring_numeral:
"Numeral1 * a = a"
"a * Numeral1 = a"
+ for a :: "'a::semiring_numeral"
+ by simp_all
+
+lemma mult_1s_ring_1:
"- Numeral1 * b = - b"
"b * - Numeral1 = - b"
- for a :: "'a::semiring_numeral" and b :: "'b::ring_1"
+ for b :: "'a::ring_1"
by simp_all
+lemmas mult_1s = mult_1s_semiring_numeral mult_1s_ring_1
+
setup \<open>
Reorient_Proc.add
(fn Const (@{const_name numeral}, _) $ _ => true
@@ -1385,13 +1391,20 @@
"- numeral v + (- numeral w + y) = (- numeral(v + w) + y)"
by (simp_all add: add.assoc [symmetric])
-lemma mult_numeral_left [simp]:
+lemma mult_numeral_left_semiring_numeral:
"numeral v * (numeral w * z) = (numeral(v * w) * z :: 'a::semiring_numeral)"
- "- numeral v * (numeral w * y) = (- numeral(v * w) * y :: 'b::ring_1)"
- "numeral v * (- numeral w * y) = (- numeral(v * w) * y :: 'b::ring_1)"
- "- numeral v * (- numeral w * y) = (numeral(v * w) * y :: 'b::ring_1)"
+ by (simp add: mult.assoc [symmetric])
+
+lemma mult_numeral_left_ring_1:
+ "- numeral v * (numeral w * y) = (- numeral(v * w) * y :: 'a::ring_1)"
+ "numeral v * (- numeral w * y) = (- numeral(v * w) * y :: 'a::ring_1)"
+ "- numeral v * (- numeral w * y) = (numeral(v * w) * y :: 'a::ring_1)"
by (simp_all add: mult.assoc [symmetric])
+lemmas mult_numeral_left [simp] =
+ mult_numeral_left_semiring_numeral
+ mult_numeral_left_ring_1
+
hide_const (open) One Bit0 Bit1 BitM inc pow sqr sub dbl dbl_inc dbl_dec
--- a/src/HOL/Probability/Distribution_Functions.thy Sun Jul 01 10:58:14 2018 +0200
+++ b/src/HOL/Probability/Distribution_Functions.thy Sun Jul 01 17:38:08 2018 +0200
@@ -107,7 +107,7 @@
using \<open>decseq f\<close> unfolding cdf_def
by (intro finite_Lim_measure_decseq) (auto simp: decseq_def)
also have "(\<Inter>i. {.. f i}) = {.. a}"
- using decseq_le[OF f] by (auto intro: order_trans LIMSEQ_le_const[OF f(2)])
+ using decseq_ge[OF f] by (auto intro: order_trans LIMSEQ_le_const[OF f(2)])
finally show "(\<lambda>n. cdf M (f n)) \<longlonglongrightarrow> cdf M a"
by (simp add: cdf_def)
qed simp
--- a/src/HOL/Rat.thy Sun Jul 01 10:58:14 2018 +0200
+++ b/src/HOL/Rat.thy Sun Jul 01 17:38:08 2018 +0200
@@ -529,6 +529,10 @@
end
+lemmas (in linordered_field) sign_simps = algebra_simps zero_less_mult_iff mult_less_0_iff
+lemmas sign_simps = algebra_simps zero_less_mult_iff mult_less_0_iff
+
+
instantiation rat :: distrib_lattice
begin
--- a/src/HOL/Real_Vector_Spaces.thy Sun Jul 01 10:58:14 2018 +0200
+++ b/src/HOL/Real_Vector_Spaces.thy Sun Jul 01 17:38:08 2018 +0200
@@ -1092,7 +1092,7 @@
then show ?thesis
by simp
qed
-
+
subclass uniform_space
proof
fix E x
--- a/src/HOL/Topological_Spaces.thy Sun Jul 01 10:58:14 2018 +0200
+++ b/src/HOL/Topological_Spaces.thy Sun Jul 01 17:38:08 2018 +0200
@@ -1109,7 +1109,7 @@
unfolding Lim_def ..
-subsubsection \<open>Monotone sequences and subsequences\<close>
+subsection \<open>Monotone sequences and subsequences\<close>
text \<open>
Definition of monotonicity.
@@ -1132,7 +1132,7 @@
lemma decseq_def: "decseq X \<longleftrightarrow> (\<forall>m. \<forall>n\<ge>m. X n \<le> X m)"
unfolding antimono_def ..
-text \<open>Definition of subsequence.\<close>
+subsubsection \<open>Definition of subsequence.\<close>
(* For compatibility with the old "subseq" *)
lemma strict_mono_leD: "strict_mono r \<Longrightarrow> m \<le> n \<Longrightarrow> r m \<le> r n"
@@ -1205,7 +1205,7 @@
qed
-text \<open>Subsequence (alternative definition, (e.g. Hoskins)\<close>
+subsubsection \<open>Subsequence (alternative definition, (e.g. Hoskins)\<close>
lemma strict_mono_Suc_iff: "strict_mono f \<longleftrightarrow> (\<forall>n. f n < f (Suc n))"
proof (intro iffI strict_monoI)
@@ -1351,7 +1351,7 @@
by (rule LIMSEQ_offset [where k="Suc 0"]) simp
lemma LIMSEQ_Suc_iff: "(\<lambda>n. f (Suc n)) \<longlonglongrightarrow> l = f \<longlonglongrightarrow> l"
- by (blast intro: LIMSEQ_imp_Suc LIMSEQ_Suc)
+ by (rule filterlim_sequentially_Suc)
lemma LIMSEQ_lessThan_iff_atMost:
shows "(\<lambda>n. f {..<n}) \<longlonglongrightarrow> x \<longleftrightarrow> (\<lambda>n. f {..n}) \<longlonglongrightarrow> x"
@@ -1375,6 +1375,56 @@
for a x :: "'a::linorder_topology"
by (rule LIMSEQ_le[of X x "\<lambda>n. a"]) auto
+lemma Lim_bounded: "f \<longlonglongrightarrow> l \<Longrightarrow> \<forall>n\<ge>M. f n \<le> C \<Longrightarrow> l \<le> C"
+ for l :: "'a::linorder_topology"
+ by (intro LIMSEQ_le_const2) auto
+
+lemma Lim_bounded2:
+ fixes f :: "nat \<Rightarrow> 'a::linorder_topology"
+ assumes lim:"f \<longlonglongrightarrow> l" and ge: "\<forall>n\<ge>N. f n \<ge> C"
+ shows "l \<ge> C"
+ using ge
+ by (intro tendsto_le[OF trivial_limit_sequentially lim tendsto_const])
+ (auto simp: eventually_sequentially)
+
+lemma lim_mono:
+ fixes X Y :: "nat \<Rightarrow> 'a::linorder_topology"
+ assumes "\<And>n. N \<le> n \<Longrightarrow> X n \<le> Y n"
+ and "X \<longlonglongrightarrow> x"
+ and "Y \<longlonglongrightarrow> y"
+ shows "x \<le> y"
+ using assms(1) by (intro LIMSEQ_le[OF assms(2,3)]) auto
+
+lemma Sup_lim:
+ fixes a :: "'a::{complete_linorder,linorder_topology}"
+ assumes "\<And>n. b n \<in> s"
+ and "b \<longlonglongrightarrow> a"
+ shows "a \<le> Sup s"
+ by (metis Lim_bounded assms complete_lattice_class.Sup_upper)
+
+lemma Inf_lim:
+ fixes a :: "'a::{complete_linorder,linorder_topology}"
+ assumes "\<And>n. b n \<in> s"
+ and "b \<longlonglongrightarrow> a"
+ shows "Inf s \<le> a"
+ by (metis Lim_bounded2 assms complete_lattice_class.Inf_lower)
+
+lemma SUP_Lim:
+ fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
+ assumes inc: "incseq X"
+ and l: "X \<longlonglongrightarrow> l"
+ shows "(SUP n. X n) = l"
+ using LIMSEQ_SUP[OF inc] tendsto_unique[OF trivial_limit_sequentially l]
+ by simp
+
+lemma INF_Lim:
+ fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
+ assumes dec: "decseq X"
+ and l: "X \<longlonglongrightarrow> l"
+ shows "(INF n. X n) = l"
+ using LIMSEQ_INF[OF dec] tendsto_unique[OF trivial_limit_sequentially l]
+ by simp
+
lemma convergentD: "convergent X \<Longrightarrow> \<exists>L. X \<longlonglongrightarrow> L"
by (simp add: convergent_def)
@@ -1417,7 +1467,7 @@
for L :: "'a::linorder_topology"
by (metis incseq_def LIMSEQ_le_const)
-lemma decseq_le: "decseq X \<Longrightarrow> X \<longlonglongrightarrow> L \<Longrightarrow> L \<le> X n"
+lemma decseq_ge: "decseq X \<Longrightarrow> X \<longlonglongrightarrow> L \<Longrightarrow> L \<le> X n"
for L :: "'a::linorder_topology"
by (metis decseq_def LIMSEQ_le_const2)
--- a/src/Pure/Admin/isabelle_cronjob.scala Sun Jul 01 10:58:14 2018 +0200
+++ b/src/Pure/Admin/isabelle_cronjob.scala Sun Jul 01 17:38:08 2018 +0200
@@ -299,7 +299,7 @@
" -e ISABELLE_GHC=/usr/local/ghc-8.0.2/bin/ghc" +
" -e ISABELLE_SMLNJ=/usr/local/smlnj-110.81/bin/sml",
args = "-a",
- detect = Build_Log.Settings.ML_PLATFORM + " = " + SQL.string("x86_64-windows"))),
+ detect = Build_Log.Settings.ML_PLATFORM + " = " + SQL.string("x86_64-windows")))
) :::
{
for { (n, hosts) <- List(1 -> List("lxbroy6"), 2 -> List("lxbroy8", "lxbroy5")) }
--- a/src/Pure/Isar/attrib.ML Sun Jul 01 10:58:14 2018 +0200
+++ b/src/Pure/Isar/attrib.ML Sun Jul 01 17:38:08 2018 +0200
@@ -591,6 +591,7 @@
register_config ML_Options.exception_trace_raw #>
register_config ML_Options.exception_debugger_raw #>
register_config ML_Options.debugger_raw #>
+ register_config Global_Theory.pending_shyps_raw #>
register_config Proof_Context.show_abbrevs_raw #>
register_config Goal_Display.goals_limit_raw #>
register_config Goal_Display.show_main_goal_raw #>
--- a/src/Pure/ML/ml_console.scala Sun Jul 01 10:58:14 2018 +0200
+++ b/src/Pure/ML/ml_console.scala Sun Jul 01 17:38:08 2018 +0200
@@ -15,6 +15,7 @@
{
Command_Line.tool {
var dirs: List[Path] = Nil
+ var include_sessions: List[String] = Nil
var logic = Isabelle_System.getenv("ISABELLE_LOGIC")
var modes: List[String] = Nil
var no_build = false
@@ -27,6 +28,7 @@
Options are:
-d DIR include session directory
+ -i NAME include session in name-space of theories
-l NAME logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """)
-m MODE add print mode for output
-n no build of session image on startup
@@ -39,6 +41,7 @@
quote(Isabelle_System.getenv("ISABELLE_LINE_EDITOR")) + """.
""",
"d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
+ "i:" -> (arg => include_sessions = include_sessions ::: List(arg)),
"l:" -> (arg => logic = arg),
"m:" -> (arg => modes = arg :: modes),
"n" -> (arg => no_build = true),
@@ -69,7 +72,8 @@
store = Some(Sessions.store(options, system_mode)),
session_base =
if (raw_ml_system) None
- else Some(Sessions.base_info(options, logic, dirs = dirs).check_base))
+ else Some(Sessions.base_info(
+ options, logic, dirs = dirs, include_sessions = include_sessions).check_base))
val tty_loop = new TTY_Loop(process.stdin, process.stdout, Some(process.interrupt _))
val process_result = Future.thread[Int]("process_result") {
--- a/src/Pure/PIDE/document.ML Sun Jul 01 10:58:14 2018 +0200
+++ b/src/Pure/PIDE/document.ML Sun Jul 01 17:38:08 2018 +0200
@@ -735,8 +735,9 @@
segments = segments};
in
fn _ =>
- (Thy_Info.apply_presentation presentation_context thy;
- commit_consolidated node)
+ Exn.release
+ (Exn.capture (Thy_Info.apply_presentation presentation_context) thy
+ before commit_consolidated node)
end
else fn _ => commit_consolidated node;
--- a/src/Pure/Thy/export_theory.ML Sun Jul 01 10:58:14 2018 +0200
+++ b/src/Pure/Thy/export_theory.ML Sun Jul 01 17:38:08 2018 +0200
@@ -102,6 +102,12 @@
(* axioms and facts *)
+ val standard_prop_of =
+ Thm.transfer thy #>
+ Thm.check_hyps (Context.Theory thy) #>
+ Drule.sort_constraint_intr_shyps #>
+ Thm.full_prop_of;
+
val encode_props =
let open XML.Encode Term_XML.Encode
in triple (list (pair string sort)) (list (pair string typ)) (list term) end;
@@ -114,7 +120,7 @@
in encode_props (typargs, args, props') end;
val export_axiom = export_props o single;
- val export_fact = export_props o Term_Subst.zero_var_indexes_list o map Thm.full_prop_of;
+ val export_fact = export_props o Term_Subst.zero_var_indexes_list o map standard_prop_of;
val _ =
export_entities "axioms" (K (SOME o export_axiom)) Theory.axiom_space
--- a/src/Pure/Thy/sessions.scala Sun Jul 01 10:58:14 2018 +0200
+++ b/src/Pure/Thy/sessions.scala Sun Jul 01 17:38:08 2018 +0200
@@ -461,7 +461,11 @@
{
val sel_sessions1 = session1 :: session :: include_sessions
val select_sessions1 =
- if (session_focus) full_sessions1.imports_descendants(sel_sessions1) else sel_sessions1
+ if (session_focus) {
+ full_sessions1.check_sessions(sel_sessions1)
+ full_sessions1.imports_descendants(sel_sessions1)
+ }
+ else sel_sessions1
full_sessions1.selection(Selection(sessions = select_sessions1))
}
@@ -679,13 +683,16 @@
}
})
+ def check_sessions(names: List[String])
+ {
+ val bad_sessions = SortedSet(names.filterNot(defined(_)): _*).toList
+ if (bad_sessions.nonEmpty)
+ error("Undefined session(s): " + commas_quote(bad_sessions))
+ }
+
def selection(sel: Selection): Structure =
{
- val bad_sessions =
- SortedSet((sel.base_sessions ::: sel.exclude_sessions ::: sel.sessions).
- filterNot(defined(_)): _*).toList
- if (bad_sessions.nonEmpty)
- error("Undefined session(s): " + commas_quote(bad_sessions))
+ check_sessions(sel.base_sessions ::: sel.exclude_sessions ::: sel.sessions)
val excluded = sel.excluded(build_graph).toSet
--- a/src/Pure/Tools/dump.scala Sun Jul 01 10:58:14 2018 +0200
+++ b/src/Pure/Tools/dump.scala Sun Jul 01 17:38:08 2018 +0200
@@ -93,8 +93,8 @@
system_mode: Boolean = false,
selection: Sessions.Selection = Sessions.Selection.empty): Process_Result =
{
- if (Build.build_logic(options, logic, progress = progress, dirs = dirs,
- system_mode = system_mode) != 0) error(logic + " FAILED")
+ if (Build.build_logic(options, logic, build_heap = true, progress = progress,
+ dirs = dirs, system_mode = system_mode) != 0) error(logic + " FAILED")
val dump_options = make_options(options, aspects)
--- a/src/Pure/Tools/server.scala Sun Jul 01 10:58:14 2018 +0200
+++ b/src/Pure/Tools/server.scala Sun Jul 01 17:38:08 2018 +0200
@@ -102,7 +102,7 @@
val session = context.server.the_session(args.session_id)
Server_Commands.Use_Theories.command(
args, session, id = task.id, progress = task.progress)._1
- }),
+ })
},
"purge_theories" ->
{ case (context, Server_Commands.Purge_Theories(args)) =>
--- a/src/Pure/drule.ML Sun Jul 01 10:58:14 2018 +0200
+++ b/src/Pure/drule.ML Sun Jul 01 17:38:08 2018 +0200
@@ -98,6 +98,8 @@
val is_sort_constraint: term -> bool
val sort_constraintI: thm
val sort_constraint_eq: thm
+ val sort_constraint_intr: indexname * sort -> thm -> thm
+ val sort_constraint_intr_shyps: thm -> thm
val with_subgoal: int -> (thm -> thm) -> thm -> thm
val comp_no_flatten: thm * int -> int -> thm -> thm
val rename_bvars: (string * string) list -> thm -> thm
@@ -647,6 +649,26 @@
(Thm.unvarify_global (Context.the_global_context ()) sort_constraintI)))
(implies_intr_list [A, C] (Thm.assume A)));
+val sort_constraint_eq' = Thm.symmetric sort_constraint_eq;
+
+fun sort_constraint_intr tvar thm =
+ Thm.equal_elim
+ (Thm.instantiate
+ ([((("'a", 0), []), Thm.global_ctyp_of (Thm.theory_of_thm thm) (TVar tvar))],
+ [((("A", 0), propT), Thm.cprop_of thm)])
+ sort_constraint_eq') thm;
+
+fun sort_constraint_intr_shyps raw_thm =
+ let val thm = Thm.strip_shyps raw_thm in
+ (case Thm.extra_shyps thm of
+ [] => thm
+ | shyps =>
+ let
+ val names = Name.make_context (map #1 (Thm.fold_terms Term.add_tvar_names thm []));
+ val constraints = map (rpair 0) (Name.invent names Name.aT (length shyps)) ~~ shyps;
+ in Thm.strip_shyps (fold_rev sort_constraint_intr constraints thm) end)
+ end;
+
end;
--- a/src/Pure/global_theory.ML Sun Jul 01 10:58:14 2018 +0200
+++ b/src/Pure/global_theory.ML Sun Jul 01 17:38:08 2018 +0200
@@ -24,6 +24,8 @@
val name_thm: bool -> bool -> string -> thm -> thm
val name_thms: bool -> bool -> string -> thm list -> thm list
val name_thmss: bool -> string -> (thm list * 'a) list -> (thm list * 'a) list
+ val pending_shyps_raw: Config.raw
+ val pending_shyps: bool Config.T
val add_thms_lazy: string -> (binding * thm list lazy) -> theory -> theory
val store_thm: binding * thm -> theory -> thm * theory
val store_thm_open: binding * thm -> theory -> thm * theory
@@ -128,16 +130,35 @@
fun register_proofs thms thy = (thms, Thm.register_proofs (Lazy.value thms) thy);
+val pending_shyps_raw = Config.declare ("pending_shyps", \<^here>) (K (Config.Bool false));
+val pending_shyps = Config.bool pending_shyps_raw;
+
fun add_facts (b, fact) thy =
let
val full_name = Sign.full_name thy b;
val pos = Binding.pos_of b;
- fun err msg =
- error ("Malformed global fact " ^ quote full_name ^ Position.here pos ^ "\n" ^ msg);
- fun check thm =
- ignore (Logic.unvarify_global (Term_Subst.zero_var_indexes (Thm.full_prop_of thm)))
- handle TERM (msg, _) => err msg | TYPE (msg, _, _) => err msg;
- val arg = (b, Lazy.map_finished (tap (List.app check)) fact);
+ fun check fact =
+ fact |> map_index (fn (i, thm) =>
+ let
+ fun err msg =
+ error ("Malformed global fact " ^
+ quote (full_name ^
+ (if length fact = 1 then "" else "(" ^ string_of_int (i + 1) ^ ")")) ^
+ Position.here pos ^ "\n" ^ msg);
+ val prop = Thm.plain_prop_of thm
+ handle THM _ =>
+ thm
+ |> not (Config.get_global thy pending_shyps) ?
+ Thm.check_shyps (Proof_Context.init_global thy)
+ |> Thm.check_hyps (Context.Theory thy)
+ |> Thm.full_prop_of;
+ in
+ ignore (Logic.unvarify_global (Term_Subst.zero_var_indexes prop))
+ handle TYPE (msg, _, _) => err msg
+ | TERM (msg, _) => err msg
+ | ERROR msg => err msg
+ end);
+ val arg = (b, Lazy.map_finished (tap check) fact);
in
thy |> Data.map (Facts.add_static (Context.Theory thy) {strict = true, index = false} arg #> #2)
end;
--- a/src/Tools/VSCode/extension/README.md Sun Jul 01 10:58:14 2018 +0200
+++ b/src/Tools/VSCode/extension/README.md Sun Jul 01 17:38:08 2018 +0200
@@ -1,14 +1,15 @@
# Isabelle Prover IDE support
This extension connects VSCode to the Isabelle Prover IDE infrastructure: it
-requires a repository version of Isabelle.
+requires Isabelle2018.
The implementation is centered around the VSCode Language Server protocol, but
with many add-ons that are specific to VSCode and Isabelle/PIDE.
See also:
- * <https://isabelle.in.tum.de/repos/isabelle/file/tip/src/Tools/VSCode>
+ * <https://isabelle.in.tum.de/website-Isabelle2018>
+ * <https://isabelle.in.tum.de/repos/isabelle/file/Isabelle2018/src/Tools/VSCode>
* <https://github.com/Microsoft/language-server-protocol>
@@ -58,8 +59,8 @@
### Isabelle/VSCode Installation
- * Download a recent Isabelle development snapshot from
- <http://isabelle.in.tum.de/devel/release_snapshot>
+ * Download Isabelle2018 from <https://isabelle.in.tum.de/website-Isabelle2018>
+ or any of its mirror sites.
* Unpack and run the main Isabelle/jEdit application as usual, to ensure that
the logic image is built properly and Isabelle works as expected.
@@ -68,7 +69,7 @@
* Open the VSCode *Extensions* view and install the following:
- + *Isabelle*.
+ + *Isabelle2018* (needs to fit to the underlying Isabelle release).
+ *Prettify Symbols Mode* (important for display of Isabelle symbols).
@@ -89,17 +90,17 @@
+ Linux:
```
- "isabelle.home": "/home/makarius/Isabelle"
+ "isabelle.home": "/home/makarius/Isabelle2018"
```
+ Mac OS X:
```
- "isabelle.home": "/Users/makarius/Isabelle.app/Isabelle"
+ "isabelle.home": "/Users/makarius/Isabelle.app/Isabelle2018"
```
+ Windows:
```
- "isabelle.home": "C:\\Users\\makarius\\Isabelle"
+ "isabelle.home": "C:\\Users\\makarius\\Isabelle2018"
```
* Restart the VSCode application to ensure that all extensions are properly
--- a/src/Tools/VSCode/extension/package.json Sun Jul 01 10:58:14 2018 +0200
+++ b/src/Tools/VSCode/extension/package.json Sun Jul 01 17:38:08 2018 +0200
@@ -1,6 +1,6 @@
{
- "name": "isabelle",
- "displayName": "Isabelle",
+ "name": "Isabelle2018",
+ "displayName": "Isabelle2018",
"description": "Isabelle Prover IDE",
"keywords": [
"theorem prover",
--- a/src/Tools/jEdit/lib/Tools/jedit Sun Jul 01 10:58:14 2018 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit Sun Jul 01 17:38:08 2018 +0200
@@ -106,6 +106,7 @@
echo " -b build only"
echo " -d DIR include session directory"
echo " -f fresh build"
+ echo " -i NAME include session in name-space of theories"
echo " -j OPTION add jEdit runtime option"
echo " (default $JEDIT_OPTIONS)"
echo " -l NAME logic session name"
@@ -142,6 +143,7 @@
JEDIT_LOGIC_ANCESTOR=""
JEDIT_LOGIC_REQUIREMENTS=""
JEDIT_LOGIC_FOCUS=""
+JEDIT_INCLUDE_SESSIONS=""
JEDIT_SESSION_DIRS=""
JEDIT_LOGIC=""
JEDIT_PRINT_MODE=""
@@ -150,7 +152,7 @@
function getoptions()
{
OPTIND=1
- while getopts "A:BFD:J:R:S:bd:fj:l:m:np:s" OPT
+ while getopts "A:BFD:J:R:S:bd:fi:j:l:m:np:s" OPT
do
case "$OPT" in
A)
@@ -181,6 +183,13 @@
JEDIT_SESSION_DIRS="$JEDIT_SESSION_DIRS:$OPTARG"
fi
;;
+ i)
+ if [ -z "$JEDIT_INCLUDE_SESSIONS" ]; then
+ JEDIT_INCLUDE_SESSIONS="$OPTARG"
+ else
+ JEDIT_INCLUDE_SESSIONS="$JEDIT_INCLUDE_SESSIONS:$OPTARG"
+ fi
+ ;;
f)
BUILD_JARS="jars_fresh"
;;
@@ -413,7 +422,7 @@
if [ "$BUILD_ONLY" = false ]
then
export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_LOGIC_ANCESTOR JEDIT_LOGIC_REQUIREMENTS \
- JEDIT_LOGIC_FOCUS JEDIT_PRINT_MODE JEDIT_BUILD_MODE
+ JEDIT_LOGIC_FOCUS JEDIT_INCLUDE_SESSIONS JEDIT_PRINT_MODE JEDIT_BUILD_MODE
export JEDIT_ML_PROCESS_POLICY="$ML_PROCESS_POLICY"
classpath "$JEDIT_HOME/dist/jedit.jar"
exec isabelle java "${JAVA_ARGS[@]}" isabelle.Main "${ARGS[@]}"
--- a/src/Tools/jEdit/src/jedit_sessions.scala Sun Jul 01 10:58:14 2018 +0200
+++ b/src/Tools/jEdit/src/jedit_sessions.scala Sun Jul 01 17:38:08 2018 +0200
@@ -42,6 +42,8 @@
def logic_ancestor: Option[String] = proper_string(Isabelle_System.getenv("JEDIT_LOGIC_ANCESTOR"))
def logic_requirements: Boolean = Isabelle_System.getenv("JEDIT_LOGIC_REQUIREMENTS") == "true"
def logic_focus: Boolean = Isabelle_System.getenv("JEDIT_LOGIC_FOCUS") == "true"
+ def logic_include_sessions: List[String] =
+ space_explode(':', Isabelle_System.getenv("JEDIT_INCLUDE_SESSIONS"))
def logic_info(options: Options): Option[Sessions.Info] =
try {
@@ -108,6 +110,7 @@
def session_base_info(options: Options): Sessions.Base_Info =
Sessions.base_info(options,
dirs = JEdit_Sessions.session_dirs(),
+ include_sessions = logic_include_sessions,
session = logic_name(options),
session_ancestor = logic_ancestor,
session_requirements = logic_requirements,