--- a/NEWS Thu Oct 20 23:42:12 2016 +0200
+++ b/NEWS Thu Oct 20 23:42:41 2016 +0200
@@ -281,6 +281,9 @@
mod_1 ~> mod_by_Suc_0
INCOMPATIBILITY.
+* Renamed constants "setsum" ~> "sum" and "setprod" ~> "prod".
+ Corresponding renaming of theorems.
+
* New type class "idom_abs_sgn" specifies algebraic properties
of sign and absolute value functions. Type class "sgn_if" has
disappeared. Slight INCOMPATIBILITY.
--- a/src/HOL/Analysis/Borel_Space.thy Thu Oct 20 23:42:12 2016 +0200
+++ b/src/HOL/Analysis/Borel_Space.thy Thu Oct 20 23:42:41 2016 +0200
@@ -345,6 +345,14 @@
"A \<in> sets borel \<Longrightarrow> insert x A \<in> sets (borel :: 'a::t1_space measure)"
unfolding insert_def by (rule sets.Un) auto
+lemma sets_borel_eq_count_space: "sets (borel :: 'a::{countable, t2_space} measure) = count_space UNIV"
+proof -
+ have "(\<Union>a\<in>A. {a}) \<in> sets borel" for A :: "'a set"
+ by (intro sets.countable_UN') auto
+ then show ?thesis
+ by auto
+qed
+
lemma borel_comp[measurable]: "A \<in> sets borel \<Longrightarrow> - A \<in> sets borel"
unfolding Compl_eq_Diff_UNIV by simp
--- a/src/HOL/Analysis/Extended_Real_Limits.thy Thu Oct 20 23:42:12 2016 +0200
+++ b/src/HOL/Analysis/Extended_Real_Limits.thy Thu Oct 20 23:42:41 2016 +0200
@@ -56,6 +56,15 @@
by simp
qed
+instance enat :: second_countable_topology
+proof
+ show "\<exists>B::enat set set. countable B \<and> open = generate_topology B"
+ proof (intro exI conjI)
+ show "countable (range lessThan \<union> range greaterThan::enat set set)"
+ by auto
+ qed (simp add: open_enat_def)
+qed
+
instance ereal :: second_countable_topology
proof (standard, intro exI conjI)
let ?B = "(\<Union>r\<in>\<rat>. {{..< r}, {r <..}} :: ereal set set)"
--- a/src/HOL/Analysis/Measurable.thy Thu Oct 20 23:42:12 2016 +0200
+++ b/src/HOL/Analysis/Measurable.thy Thu Oct 20 23:42:41 2016 +0200
@@ -646,6 +646,14 @@
shows "liminf A \<in> sets M"
by (subst liminf_SUP_INF, auto)
+lemma measurable_case_enat[measurable (raw)]:
+ assumes f: "f \<in> M \<rightarrow>\<^sub>M count_space UNIV" and g: "\<And>i. g i \<in> M \<rightarrow>\<^sub>M N" and h: "h \<in> M \<rightarrow>\<^sub>M N"
+ shows "(\<lambda>x. case f x of enat i \<Rightarrow> g i x | \<infinity> \<Rightarrow> h x) \<in> M \<rightarrow>\<^sub>M N"
+ apply (rule measurable_compose_countable[OF _ f])
+ subgoal for i
+ by (cases i) (auto intro: g h)
+ done
+
hide_const (open) pred
end
--- a/src/HOL/Analysis/Measure_Space.thy Thu Oct 20 23:42:12 2016 +0200
+++ b/src/HOL/Analysis/Measure_Space.thy Thu Oct 20 23:42:41 2016 +0200
@@ -1469,6 +1469,9 @@
lemma distr_id[simp]: "distr N N (\<lambda>x. x) = N"
by (rule measure_eqI) (auto simp: emeasure_distr)
+lemma distr_id2: "sets M = sets N \<Longrightarrow> distr N M (\<lambda>x. x) = N"
+ by (rule measure_eqI) (auto simp: emeasure_distr)
+
lemma measure_distr:
"f \<in> measurable M N \<Longrightarrow> S \<in> sets N \<Longrightarrow> measure (distr M N f) S = measure M (f -` S \<inter> space M)"
by (simp add: emeasure_distr measure_def)
@@ -3516,6 +3519,11 @@
finally show ?thesis .
qed
+lemma measurable_SUP2:
+ "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f \<in> measurable N (M i)) \<Longrightarrow>
+ (\<And>i j. i \<in> I \<Longrightarrow> j \<in> I \<Longrightarrow> space (M i) = space (M j)) \<Longrightarrow> f \<in> measurable N (SUP i:I. M i)"
+ by (auto intro!: measurable_Sup2)
+
lemma sets_Sup_sigma:
assumes [simp]: "M \<noteq> {}" and M: "\<And>m. m \<in> M \<Longrightarrow> m \<subseteq> Pow \<Omega>"
shows "sets (SUP m:M. sigma \<Omega> m) = sets (sigma \<Omega> (\<Union>M))"
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy Thu Oct 20 23:42:12 2016 +0200
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy Thu Oct 20 23:42:41 2016 +0200
@@ -458,6 +458,11 @@
(fastforce simp: topological_space_class.topological_basis_def)+
qed
+instance nat :: second_countable_topology
+proof
+ show "\<exists>B::nat set set. countable B \<and> open = generate_topology B"
+ by (intro exI[of _ "range lessThan \<union> range greaterThan"]) (auto simp: open_nat_def)
+qed
lemma countable_separating_set_linorder1:
shows "\<exists>B::('a::{linorder_topology, second_countable_topology} set). countable B \<and> (\<forall>x y. x < y \<longrightarrow> (\<exists>b \<in> B. x < b \<and> b \<le> y))"
--- a/src/HOL/Data_Structures/document/root.tex Thu Oct 20 23:42:12 2016 +0200
+++ b/src/HOL/Data_Structures/document/root.tex Thu Oct 20 23:42:41 2016 +0200
@@ -1,6 +1,8 @@
\documentclass[11pt,a4paper]{article}
\usepackage{isabelle,isabellesym}
\usepackage{latexsym}
+\usepackage{amssymb}
+\usepackage{amsmath}
% this should be the last package used
\usepackage{pdfsetup}
--- a/src/HOL/Library/Extended_Nonnegative_Real.thy Thu Oct 20 23:42:12 2016 +0200
+++ b/src/HOL/Library/Extended_Nonnegative_Real.thy Thu Oct 20 23:42:41 2016 +0200
@@ -1131,6 +1131,9 @@
lemma enn2real_positive_iff: "0 < enn2real x \<longleftrightarrow> (0 < x \<and> x < top)"
by (cases x rule: ennreal_cases) auto
+lemma enn2real_eq_1_iff[simp]: "enn2real x = 1 \<longleftrightarrow> x = 1"
+ by (cases x) auto
+
subsection \<open>Coercion from @{typ enat} to @{typ ennreal}\<close>
--- a/src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy Thu Oct 20 23:42:12 2016 +0200
+++ b/src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy Thu Oct 20 23:42:41 2016 +0200
@@ -662,7 +662,7 @@
lemma sfilter_not_P[simp]: "\<not> P (shd s) \<Longrightarrow> sfilter P s = sfilter P (stl s)"
using sfilter_Stream[of P "shd s" "stl s"] by simp
-lemma sfilter_eq:
+lemma sfilter_eq:
assumes "ev (holds P) s"
shows "sfilter P s = x ## s' \<longleftrightarrow>
P x \<and> (not (holds P) suntil (HLD {x} aand nxt (\<lambda>s. sfilter P s = s'))) s"
@@ -685,7 +685,7 @@
proof
assume "alw Q (sfilter P s)" with * show "alw (\<lambda>x. Q (sfilter P x)) s"
proof (coinduction arbitrary: s rule: alw_coinduct)
- case (stl s)
+ case (stl s)
then have "ev (holds P) s"
by blast
from this stl show ?case
@@ -694,7 +694,7 @@
next
assume "alw (\<lambda>x. Q (sfilter P x)) s" with * show "alw Q (sfilter P s)"
proof (coinduction arbitrary: s rule: alw_coinduct)
- case (stl s)
+ case (stl s)
then have "ev (holds P) s"
by blast
from this stl show ?case
@@ -767,4 +767,22 @@
lemma hld_smap': "HLD x (smap f s) = HLD (f -` x) s"
by (simp add: HLD_def)
+lemma pigeonhole_stream:
+ assumes "alw (HLD s) \<omega>"
+ assumes "finite s"
+ shows "\<exists>x\<in>s. alw (ev (HLD {x})) \<omega>"
+proof -
+ have "\<forall>i\<in>UNIV. \<exists>x\<in>s. \<omega> !! i = x"
+ using `alw (HLD s) \<omega>` by (simp add: alw_iff_sdrop HLD_iff)
+ from pigeonhole_infinite_rel[OF infinite_UNIV_nat `finite s` this]
+ show ?thesis
+ by (simp add: HLD_iff infinite_iff_alw_ev[symmetric])
+qed
+
+lemma ev_eq_suntil: "ev P \<omega> \<longleftrightarrow> (not P suntil P) \<omega>"
+proof
+ assume "ev P \<omega>" then show "((\<lambda>xs. \<not> P xs) suntil P) \<omega>"
+ by (induction rule: ev_induct_strong) (auto intro: suntil.intros)
+qed (auto simp: ev_suntil)
+
end
--- a/src/HOL/Library/Stream.thy Thu Oct 20 23:42:12 2016 +0200
+++ b/src/HOL/Library/Stream.thy Thu Oct 20 23:42:41 2016 +0200
@@ -242,7 +242,7 @@
lemma sdrop_snth: "sdrop n s !! m = s !! (n + m)"
by (induct n arbitrary: m s) auto
-partial_function (tailrec) sdrop_while :: "('a \<Rightarrow> bool) \<Rightarrow> 'a stream \<Rightarrow> 'a stream" where
+partial_function (tailrec) sdrop_while :: "('a \<Rightarrow> bool) \<Rightarrow> 'a stream \<Rightarrow> 'a stream" where
"sdrop_while P s = (if P (shd s) then sdrop_while P (stl s) else s)"
lemma sdrop_while_SCons[code]:
@@ -342,7 +342,7 @@
by (induct n arbitrary: u) (auto simp: rotate1_rotate_swap rotate1_hd_tl rotate_conv_mod[symmetric])
lemma sset_cycle[simp]:
- assumes "xs \<noteq> []"
+ assumes "xs \<noteq> []"
shows "sset (cycle xs) = set xs"
proof (intro set_eqI iffI)
fix x
@@ -408,6 +408,14 @@
lemma sconst_streams: "x \<in> A \<Longrightarrow> sconst x \<in> streams A"
by (simp add: streams_iff_sset)
+lemma streams_empty_iff: "streams S = {} \<longleftrightarrow> S = {}"
+proof safe
+ fix x assume "x \<in> S" "streams S = {}"
+ then have "sconst x \<in> streams S"
+ by (intro sconst_streams)
+ then show "x \<in> {}"
+ unfolding \<open>streams S = {}\<close> by simp
+qed (auto simp: streams_empty)
subsection \<open>stream of natural numbers\<close>
@@ -442,11 +450,11 @@
lemma flat_unfold: "shd ws \<noteq> [] \<Longrightarrow> flat ws = shd ws @- flat (stl ws)"
by (cases ws) auto
-lemma flat_snth: "\<forall>xs \<in> sset s. xs \<noteq> [] \<Longrightarrow> flat s !! n = (if n < length (shd s) then
+lemma flat_snth: "\<forall>xs \<in> sset s. xs \<noteq> [] \<Longrightarrow> flat s !! n = (if n < length (shd s) then
shd s ! n else flat (stl s) !! (n - length (shd s)))"
by (metis flat_unfold not_less shd_sset shift_snth_ge shift_snth_less)
-lemma sset_flat[simp]: "\<forall>xs \<in> sset s. xs \<noteq> [] \<Longrightarrow>
+lemma sset_flat[simp]: "\<forall>xs \<in> sset s. xs \<noteq> [] \<Longrightarrow>
sset (flat s) = (\<Union>xs \<in> sset s. set xs)" (is "?P \<Longrightarrow> ?L = ?R")
proof safe
fix x assume ?P "x : ?L"
--- a/src/HOL/Number_Theory/Number_Theory.thy Thu Oct 20 23:42:12 2016 +0200
+++ b/src/HOL/Number_Theory/Number_Theory.thy Thu Oct 20 23:42:41 2016 +0200
@@ -2,7 +2,7 @@
section \<open>Comprehensive number theory\<close>
theory Number_Theory
-imports Fib Residues Eratosthenes QuadraticReciprocity Pocklington
+imports Fib Residues Eratosthenes Quadratic_Reciprocity Pocklington
begin
end
--- a/src/HOL/Number_Theory/QuadraticReciprocity.thy Thu Oct 20 23:42:12 2016 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,387 +0,0 @@
-(* Author: Jaime Mendizabal Roche *)
-
-theory QuadraticReciprocity
-imports Gauss
-begin
-
-text {* The proof is based on Gauss's fifth proof, which can be found at http://www.lehigh.edu/~shw2/q-recip/gauss5.pdf *}
-
-locale QR =
- fixes p :: "nat"
- fixes q :: "nat"
-
- assumes p_prime: "prime p"
- assumes p_ge_2: "2 < p"
- assumes q_prime: "prime q"
- assumes q_ge_2: "2 < q"
- assumes pq_neq: "p \<noteq> q"
-begin
-
-lemma odd_p: "odd p" using p_ge_2 p_prime prime_odd_nat by blast
-
-lemma p_ge_0: "0 < int p"
- using p_prime not_prime_0[where 'a = nat] by fastforce+
-
-lemma p_eq2: "int p = (2 * ((int p - 1) div 2)) + 1" using odd_p by simp
-
-lemma odd_q: "odd q" using q_ge_2 q_prime prime_odd_nat by blast
-
-lemma q_ge_0: "0 < int q" using q_prime not_prime_0[where 'a = nat] by fastforce+
-
-lemma q_eq2: "int q = (2 * ((int q - 1) div 2)) + 1" using odd_q by simp
-
-lemma pq_eq2: "int p * int q = (2 * ((int p * int q - 1) div 2)) + 1" using odd_p odd_q by simp
-
-lemma pq_coprime: "coprime p q"
- using pq_neq p_prime primes_coprime_nat q_prime by blast
-
-lemma pq_coprime_int: "coprime (int p) (int q)"
- using pq_coprime transfer_int_nat_gcd(1) by presburger
-
-lemma qp_ineq: "(int p * k \<le> (int p * int q - 1) div 2) = (k \<le> (int q - 1) div 2)"
-proof -
- have "(2 * int p * k \<le> int p * int q - 1) = (2 * k \<le> int q - 1)" using p_ge_0 by auto
- thus ?thesis by auto
-qed
-
-lemma QRqp: "QR q p" using QR_def QR_axioms by simp
-
-lemma pq_commute: "int p * int q = int q * int p" by simp
-
-lemma pq_ge_0: "int p * int q > 0" using p_ge_0 q_ge_0 mult_pos_pos by blast
-
-definition "r = ((p - 1) div 2)*((q - 1) div 2)"
-definition "m = card (GAUSS.E p q)"
-definition "n = card (GAUSS.E q p)"
-
-abbreviation "Res (k::int) \<equiv> {0 .. k - 1}"
-abbreviation "Res_ge_0 (k::int) \<equiv> {0 <.. k - 1}"
-abbreviation "Res_0 (k::int) \<equiv> {0::int}"
-abbreviation "Res_l (k::int) \<equiv> {0 <.. (k - 1) div 2}"
-abbreviation "Res_h (k::int) \<equiv> {(k - 1) div 2 <.. k - 1}"
-
-abbreviation "Sets_pq r0 r1 r2 \<equiv>
- {(x::int). x \<in> r0 (int p * int q) \<and> x mod p \<in> r1 (int p) \<and> x mod q \<in> r2 (int q)}"
-
-definition "A = Sets_pq Res_l Res_l Res_h"
-definition "B = Sets_pq Res_l Res_h Res_l"
-definition "C = Sets_pq Res_h Res_h Res_l"
-definition "D = Sets_pq Res_l Res_h Res_h"
-definition "E = Sets_pq Res_l Res_0 Res_h"
-definition "F = Sets_pq Res_l Res_h Res_0"
-
-definition "a = card A"
-definition "b = card B"
-definition "c = card C"
-definition "d = card D"
-definition "e = card E"
-definition "f = card F"
-
-lemma Gpq: "GAUSS p q" unfolding GAUSS_def
- using p_prime pq_neq p_ge_2 q_prime
- by (auto simp: cong_altdef_int zdvd_int [symmetric] dest: primes_dvd_imp_eq)
-
-lemma Gqp: "GAUSS q p" using QRqp QR.Gpq by simp
-
-lemma QR_lemma_01: "(\<lambda>x. x mod q) ` E = GAUSS.E q p"
-proof
- {
- fix x
- assume a1: "x \<in> E"
- then obtain k where k: "x = int p * k" unfolding E_def by blast
- have "x \<in> Res_l (int p * int q)" using a1 E_def by blast
- hence "k \<in> GAUSS.A q" using Gqp GAUSS.A_def k qp_ineq by (simp add: zero_less_mult_iff)
- hence "x mod q \<in> GAUSS.E q p"
- using GAUSS.C_def[of q p] Gqp k GAUSS.B_def[of q p] a1 GAUSS.E_def[of q p]
- unfolding E_def by force
- hence "x \<in> E \<longrightarrow> x mod int q \<in> GAUSS.E q p" by auto
- }
- thus "(\<lambda>x. x mod int q) ` E \<subseteq> GAUSS.E q p" by auto
-next
- show "GAUSS.E q p \<subseteq> (\<lambda>x. x mod q) ` E"
- proof
- fix x
- assume a1: "x \<in> GAUSS.E q p"
- then obtain ka where ka: "ka \<in> GAUSS.A q" "x = (ka * p) mod q"
- using Gqp GAUSS.B_def GAUSS.C_def GAUSS.E_def by auto
- hence "ka * p \<in> Res_l (int p * int q)"
- using GAUSS.A_def Gqp p_ge_0 qp_ineq by (simp add: Groups.mult_ac(2))
- thus "x \<in> (\<lambda>x. x mod q) ` E" unfolding E_def using ka a1 Gqp GAUSS.E_def q_ge_0 by force
- qed
-qed
-
-lemma QR_lemma_02: "e= n"
-proof -
- {
- fix x y
- assume a: "x \<in> E" "y \<in> E" "x mod q = y mod q"
- obtain p_inv where p_inv: "[int p * p_inv = 1] (mod int q)"
- using pq_coprime_int cong_solve_coprime_int by blast
- obtain kx ky where k: "x = int p * kx" "y = int p * ky" using a E_def dvd_def[of p x] by blast
- hence "0 < x" "int p * kx \<le> (int p * int q - 1) div 2"
- "0 < y" "int p * ky \<le> (int p * int q - 1) div 2"
- using E_def a greaterThanAtMost_iff mem_Collect_eq by blast+
- hence "0 \<le> kx" "kx < q" "0 \<le> ky" "ky < q" using qp_ineq k by (simp add: zero_less_mult_iff)+
- moreover have "(p_inv * (p * kx)) mod q = (p_inv * (p * ky)) mod q"
- using a(3) mod_mult_cong k by blast
- hence "(p * p_inv * kx) mod q = (p * p_inv * ky) mod q" by (simp add:algebra_simps)
- hence "kx mod q = ky mod q"
- using p_inv mod_mult_cong[of "p * p_inv" "q" "1"] cong_int_def by auto
- hence "[kx = ky] (mod q)" using cong_int_def by blast
- ultimately have "x = y" using cong_less_imp_eq_int k by blast
- }
- hence "inj_on (\<lambda>x. x mod q) E" unfolding inj_on_def by auto
- thus ?thesis using QR_lemma_01 card_image e_def n_def by fastforce
-qed
-
-lemma QR_lemma_03: "f = m"
-proof -
- have "F = QR.E q p" unfolding F_def pq_commute using QRqp QR.E_def[of q p] by fastforce
- hence "f = QR.e q p" unfolding f_def using QRqp QR.e_def[of q p] by presburger
- thus ?thesis using QRqp QR.QR_lemma_02 m_def QRqp QR.n_def by presburger
-qed
-
-definition f_1 :: "int \<Rightarrow> int \<times> int" where
- "f_1 x = ((x mod p), (x mod q))"
-
-definition P_1 :: "int \<times> int \<Rightarrow> int \<Rightarrow> bool" where
- "P_1 res x \<longleftrightarrow> x mod p = fst res & x mod q = snd res & x \<in> Res (int p * int q)"
-
-definition g_1 :: "int \<times> int \<Rightarrow> int" where
- "g_1 res = (THE x. P_1 res x)"
-
-lemma P_1_lemma: assumes "0 \<le> fst res" "fst res < p" "0 \<le> snd res" "snd res < q"
- shows "\<exists>! x. P_1 res x"
-proof -
- obtain y k1 k2 where yk: "y = nat (fst res) + k1 * p" "y = nat (snd res) + k2 * q"
- using chinese_remainder[of p q] pq_coprime p_ge_0 q_ge_0 by fastforce
- have h1: "[y = fst res] (mod p)" "[y = snd res] (mod q)"
- using yk(1) assms(1) cong_iff_lin_int[of "fst res"] cong_sym_int apply simp
- using yk(2) assms(3) cong_iff_lin_int[of "snd res"] cong_sym_int by simp
- have "(y mod (int p * int q)) mod int p = fst res" "(y mod (int p * int q)) mod int q = snd res"
- using h1(1) mod_mod_cancel[of "int p"] assms(1) assms(2) cong_int_def apply simp
- using h1(2) mod_mod_cancel[of "int q"] assms(3) assms(4) cong_int_def by simp
- then obtain x where "P_1 res x" unfolding P_1_def
- using Divides.pos_mod_bound Divides.pos_mod_sign pq_ge_0 by fastforce
- moreover {
- fix a b
- assume a: "P_1 res a" "P_1 res b"
- hence "int p * int q dvd a - b"
- using divides_mult[of "int p" "a - b" "int q"] pq_coprime_int zmod_eq_dvd_iff[of a _ b]
- unfolding P_1_def by force
- hence "a = b" using dvd_imp_le_int[of "a - b"] a unfolding P_1_def by fastforce
- }
- ultimately show ?thesis by auto
-qed
-
-lemma g_1_lemma: assumes "0 \<le> fst res" "fst res < p" "0 \<le> snd res" "snd res < q"
- shows "P_1 res (g_1 res)" using assms P_1_lemma theI'[of "P_1 res"] g_1_def by presburger
-
-definition "BuC = Sets_pq Res_ge_0 Res_h Res_l"
-
-lemma QR_lemma_04: "card BuC = card ((Res_h p) \<times> (Res_l q))"
- using card_bij_eq[of f_1 "BuC" "(Res_h p) \<times> (Res_l q)" g_1]
-proof
- {
- fix x y
- assume a: "x \<in> BuC" "y \<in> BuC" "f_1 x = f_1 y"
- hence "int p * int q dvd x - y"
- using f_1_def pq_coprime_int divides_mult[of "int p" "x - y" "int q"]
- zmod_eq_dvd_iff[of x _ y] by auto
- hence "x = y"
- using dvd_imp_le_int[of "x - y" "int p * int q"] a unfolding BuC_def by force
- }
- thus "inj_on f_1 BuC" unfolding inj_on_def by auto
-next
- {
- fix x y
- assume a: "x \<in> (Res_h p) \<times> (Res_l q)" "y \<in> (Res_h p) \<times> (Res_l q)" "g_1 x = g_1 y"
- hence "0 \<le> fst x" "fst x < p" "0 \<le> snd x" "snd x < q"
- "0 \<le> fst y" "fst y < p" "0 \<le> snd y" "snd y < q"
- using mem_Sigma_iff prod.collapse by fastforce+
- hence "x = y" using g_1_lemma[of x] g_1_lemma[of y] a P_1_def by fastforce
- }
- thus "inj_on g_1 ((Res_h p) \<times> (Res_l q))" unfolding inj_on_def by auto
-next
- show "g_1 ` ((Res_h p) \<times> (Res_l q)) \<subseteq> BuC"
- proof
- fix y
- assume "y \<in> g_1 ` ((Res_h p) \<times> (Res_l q))"
- then obtain x where x: "y = g_1 x" "x \<in> ((Res_h p) \<times> (Res_l q))" by blast
- hence "P_1 x y" using g_1_lemma by fastforce
- thus "y \<in> BuC" unfolding P_1_def BuC_def mem_Collect_eq using x SigmaE prod.sel by fastforce
- qed
-qed (auto simp: BuC_def finite_subset f_1_def)
-
-lemma QR_lemma_05: "card ((Res_h p) \<times> (Res_l q)) = r"
-proof -
- have "card (Res_l q) = (q - 1) div 2" "card (Res_h p) = (p - 1) div 2" using p_eq2 by force+
- thus ?thesis unfolding r_def using card_cartesian_product[of "Res_h p" "Res_l q"] by presburger
-qed
-
-lemma QR_lemma_06: "b + c = r"
-proof -
- have "B \<inter> C = {}" "finite B" "finite C" "B \<union> C = BuC" unfolding B_def C_def BuC_def by fastforce+
- thus ?thesis
- unfolding b_def c_def using card_empty card_Un_Int QR_lemma_04 QR_lemma_05 by fastforce
-qed
-
-definition f_2:: "int \<Rightarrow> int" where
- "f_2 x = (int p * int q) - x"
-
-lemma f_2_lemma_1: "\<And>x. f_2 (f_2 x) = x" unfolding f_2_def by simp
-
-lemma f_2_lemma_2: "[f_2 x = int p - x] (mod p)" unfolding f_2_def using cong_altdef_int by simp
-
-lemma f_2_lemma_3: "f_2 x \<in> S \<Longrightarrow> x \<in> f_2 ` S"
- using f_2_lemma_1[of x] image_eqI[of x f_2 "f_2 x" S] by presburger
-
-lemma QR_lemma_07: "f_2 ` Res_l (int p * int q) = Res_h (int p * int q)"
- "f_2 ` Res_h (int p * int q) = Res_l (int p * int q)"
-proof -
- have h1: "f_2 ` Res_l (int p * int q) \<subseteq> Res_h (int p * int q)" using f_2_def by force
- have h2: "f_2 ` Res_h (int p * int q) \<subseteq> Res_l (int p * int q)" using f_2_def pq_eq2 by fastforce
- have h3: "Res_h (int p * int q) \<subseteq> f_2 ` Res_l (int p * int q)" using h2 f_2_lemma_3 by blast
- have h4: "Res_l (int p * int q) \<subseteq> f_2 ` Res_h (int p * int q)" using h1 f_2_lemma_3 by blast
- show "f_2 ` Res_l (int p * int q) = Res_h (int p * int q)" using h1 h3 by blast
- show "f_2 ` Res_h (int p * int q) = Res_l (int p * int q)" using h2 h4 by blast
-qed
-
-lemma QR_lemma_08: "(f_2 x mod p \<in> Res_l p) = (x mod p \<in> Res_h p)"
- "(f_2 x mod p \<in> Res_h p) = (x mod p \<in> Res_l p)"
- using f_2_lemma_2[of x] cong_int_def[of "f_2 x" "p - x" p] minus_mod_self2[of x p]
- zmod_zminus1_eq_if[of x p] p_eq2 by auto
-
-lemma QR_lemma_09: "(f_2 x mod q \<in> Res_l q) = (x mod q \<in> Res_h q)"
- "(f_2 x mod q \<in> Res_h q) = (x mod q \<in> Res_l q)"
- using QRqp QR.QR_lemma_08 f_2_def QR.f_2_def pq_commute by auto+
-
-lemma QR_lemma_10: "a = c" unfolding a_def c_def apply (rule card_bij_eq[of f_2 A C f_2])
- unfolding A_def C_def
- using QR_lemma_07 QR_lemma_08 QR_lemma_09 apply ((simp add: inj_on_def f_2_def),blast)+
- by fastforce+
-
-definition "BuD = Sets_pq Res_l Res_h Res_ge_0"
-definition "BuDuF = Sets_pq Res_l Res_h Res"
-
-definition f_3 :: "int \<Rightarrow> int \<times> int" where
- "f_3 x = (x mod p, x div p + 1)"
-
-definition g_3 :: "int \<times> int \<Rightarrow> int" where
- "g_3 x = fst x + (snd x - 1) * p"
-
-lemma QR_lemma_11: "card BuDuF = card ((Res_h p) \<times> (Res_l q))"
- using card_bij_eq[of f_3 BuDuF "(Res_h p) \<times> (Res_l q)" g_3]
-proof
- show "f_3 ` BuDuF \<subseteq> (Res_h p) \<times> (Res_l q)"
- proof
- fix y
- assume "y \<in> f_3 ` BuDuF"
- then obtain x where x: "y = f_3 x" "x \<in> BuDuF" by blast
- hence "x \<le> int p * (int q - 1) div 2 + (int p - 1) div 2"
- unfolding BuDuF_def using p_eq2 int_distrib(4) by auto
- moreover have "(int p - 1) div 2 \<le> - 1 + x mod p" using x BuDuF_def by auto
- moreover have "int p * (int q - 1) div 2 = int p * ((int q - 1) div 2)"
- using zdiv_zmult1_eq odd_q by auto
- hence "p * (int q - 1) div 2 = p * ((int q + 1) div 2 - 1)" by fastforce
- ultimately have "x \<le> p * ((int q + 1) div 2 - 1) - 1 + x mod p" by linarith
- hence "x div p < (int q + 1) div 2 - 1"
- using mult.commute[of "int p" "x div p"] p_ge_0 div_mult_mod_eq[of x p]
- mult_less_cancel_left_pos[of p "x div p" "(int q + 1) div 2 - 1"] by linarith
- moreover have "0 < x div p + 1"
- using pos_imp_zdiv_neg_iff[of p x] p_ge_0 x mem_Collect_eq BuDuF_def by auto
- ultimately show "y \<in> (Res_h p) \<times> (Res_l q)" using x BuDuF_def f_3_def by auto
- qed
-next
- have h1: "\<And>x. x \<in> ((Res_h p) \<times> (Res_l q)) \<Longrightarrow> f_3 (g_3 x) = x"
- proof -
- fix x
- assume a: "x \<in> ((Res_h p) \<times> (Res_l q))"
- moreover have h: "(fst x + (snd x - 1) * int p) mod int p = fst x" using a by force
- ultimately have "(fst x + (snd x - 1) * int p) div int p + 1 = snd x"
- by (auto simp: semiring_numeral_div_class.div_less)
- with h show "f_3 (g_3 x) = x" unfolding f_3_def g_3_def by simp
- qed
- show "inj_on g_3 ((Res_h p) \<times> (Res_l q))" apply (rule inj_onI[of "(Res_h p) \<times> (Res_l q)" g_3])
- proof -
- fix x y
- assume "x \<in> ((Res_h p) \<times> (Res_l q))" "y \<in> ((Res_h p) \<times> (Res_l q))" "g_3 x = g_3 y"
- thus "x = y" using h1[of x] h1[of y] by presburger
- qed
-next
- show "g_3 ` ((Res_h p) \<times> (Res_l q)) \<subseteq> BuDuF"
- proof
- fix y
- assume "y \<in> g_3 ` ((Res_h p) \<times> (Res_l q))"
- then obtain x where x: "y = g_3 x" "x \<in> (Res_h p) \<times> (Res_l q)" by blast
- hence "snd x \<le> (int q - 1) div 2" by force
- moreover have "int p * ((int q - 1) div 2) = (int p * int q - int p) div 2"
- using int_distrib(4) zdiv_zmult1_eq[of "int p" "int q - 1" 2] odd_q by fastforce
- ultimately have "(snd x) * int p \<le> (int q * int p - int p) div 2"
- using mult_right_mono[of "snd x" "(int q - 1) div 2" p] mult.commute[of "(int q - 1) div 2" p]
- pq_commute by presburger
- hence "(snd x - 1) * int p \<le> (int q * int p - 1) div 2 - int p"
- using p_ge_0 int_distrib(3) by auto
- moreover have "fst x \<le> int p - 1" using x by force
- ultimately have "fst x + (snd x - 1) * int p \<le> (int p * int q - 1) div 2"
- using pq_commute by linarith
- moreover have "0 < fst x" "0 \<le> (snd x - 1) * p" using x(2) by fastforce+
- ultimately show "y \<in> BuDuF" unfolding BuDuF_def using q_ge_0 x g_3_def x(1) by auto
- qed
-next
- show "finite BuDuF" unfolding BuDuF_def by fastforce
-qed (simp add: inj_on_inverseI[of BuDuF g_3] f_3_def g_3_def QR_lemma_05)+
-
-lemma QR_lemma_12: "b + d + m = r"
-proof -
- have "B \<inter> D = {}" "finite B" "finite D" "B \<union> D = BuD" unfolding B_def D_def BuD_def by fastforce+
- hence "b + d = card BuD" unfolding b_def d_def using card_Un_Int by fastforce
- moreover have "BuD \<inter> F = {}" "finite BuD" "finite F" unfolding BuD_def F_def by fastforce+
- moreover have "BuD \<union> F = BuDuF" unfolding BuD_def F_def BuDuF_def
- using q_ge_0 ivl_disj_un_singleton(5)[of 0 "int q - 1"] by auto
- ultimately show ?thesis using QR_lemma_03 QR_lemma_05 QR_lemma_11 card_Un_disjoint[of BuD F]
- unfolding b_def d_def f_def by presburger
-qed
-
-lemma QR_lemma_13: "a + d + n = r"
-proof -
- have "A = QR.B q p" unfolding A_def pq_commute using QRqp QR.B_def[of q p] by blast
- hence "a = QR.b q p" using a_def QRqp QR.b_def[of q p] by presburger
- moreover have "D = QR.D q p" unfolding D_def pq_commute using QRqp QR.D_def[of q p] by blast
- hence "d = QR.d q p" using d_def QRqp QR.d_def[of q p] by presburger
- moreover have "n = QR.m q p" using n_def QRqp QR.m_def[of q p] by presburger
- moreover have "r = QR.r q p" unfolding r_def using QRqp QR.r_def[of q p] by auto
- ultimately show ?thesis using QRqp QR.QR_lemma_12 by presburger
-qed
-
-lemma QR_lemma_14: "(-1::int) ^ (m + n) = (-1) ^ r"
-proof -
- have "m + n + 2 * d = r" using QR_lemma_06 QR_lemma_10 QR_lemma_12 QR_lemma_13 by auto
- thus ?thesis using power_add[of "-1::int" "m + n" "2 * d"] by fastforce
-qed
-
-lemma Quadratic_Reciprocity:
- "(Legendre p q) * (Legendre q p) = (-1::int) ^ ((p - 1) div 2 * ((q - 1) div 2))"
- using Gpq Gqp GAUSS.gauss_lemma power_add[of "-1::int" m n] QR_lemma_14
- unfolding r_def m_def n_def by auto
-
-end
-
-theorem Quadratic_Reciprocity: assumes "prime p" "2 < p" "prime q" "2 < q" "p \<noteq> q"
- shows "(Legendre p q) * (Legendre q p) = (-1::int) ^ ((p - 1) div 2 * ((q - 1) div 2))"
- using QR.Quadratic_Reciprocity QR_def assms by blast
-
-theorem Quadratic_Reciprocity_int: assumes "prime (nat p)" "2 < p" "prime (nat q)" "2 < q" "p \<noteq> q"
- shows "(Legendre p q) * (Legendre q p) = (-1::int) ^ (nat ((p - 1) div 2 * ((q - 1) div 2)))"
-proof -
- have "0 \<le> (p - 1) div 2" using assms by simp
- moreover have "(nat p - 1) div 2 = nat ((p - 1) div 2)" "(nat q - 1) div 2 = nat ((q - 1) div 2)"
- by fastforce+
- ultimately have "(nat p - 1) div 2 * ((nat q - 1) div 2) = nat ((p - 1) div 2 * ((q - 1) div 2))"
- using nat_mult_distrib by presburger
- moreover have "2 < nat p" "2 < nat q" "nat p \<noteq> nat q" "int (nat p) = p" "int (nat q) = q"
- using assms by linarith+
- ultimately show ?thesis using Quadratic_Reciprocity[of "nat p" "nat q"] assms by presburger
-qed
-
-end
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Number_Theory/Quadratic_Reciprocity.thy Thu Oct 20 23:42:41 2016 +0200
@@ -0,0 +1,387 @@
+(* Author: Jaime Mendizabal Roche *)
+
+theory Quadratic_Reciprocity
+imports Gauss
+begin
+
+text {* The proof is based on Gauss's fifth proof, which can be found at http://www.lehigh.edu/~shw2/q-recip/gauss5.pdf *}
+
+locale QR =
+ fixes p :: "nat"
+ fixes q :: "nat"
+
+ assumes p_prime: "prime p"
+ assumes p_ge_2: "2 < p"
+ assumes q_prime: "prime q"
+ assumes q_ge_2: "2 < q"
+ assumes pq_neq: "p \<noteq> q"
+begin
+
+lemma odd_p: "odd p" using p_ge_2 p_prime prime_odd_nat by blast
+
+lemma p_ge_0: "0 < int p"
+ using p_prime not_prime_0[where 'a = nat] by fastforce+
+
+lemma p_eq2: "int p = (2 * ((int p - 1) div 2)) + 1" using odd_p by simp
+
+lemma odd_q: "odd q" using q_ge_2 q_prime prime_odd_nat by blast
+
+lemma q_ge_0: "0 < int q" using q_prime not_prime_0[where 'a = nat] by fastforce+
+
+lemma q_eq2: "int q = (2 * ((int q - 1) div 2)) + 1" using odd_q by simp
+
+lemma pq_eq2: "int p * int q = (2 * ((int p * int q - 1) div 2)) + 1" using odd_p odd_q by simp
+
+lemma pq_coprime: "coprime p q"
+ using pq_neq p_prime primes_coprime_nat q_prime by blast
+
+lemma pq_coprime_int: "coprime (int p) (int q)"
+ using pq_coprime transfer_int_nat_gcd(1) by presburger
+
+lemma qp_ineq: "(int p * k \<le> (int p * int q - 1) div 2) = (k \<le> (int q - 1) div 2)"
+proof -
+ have "(2 * int p * k \<le> int p * int q - 1) = (2 * k \<le> int q - 1)" using p_ge_0 by auto
+ thus ?thesis by auto
+qed
+
+lemma QRqp: "QR q p" using QR_def QR_axioms by simp
+
+lemma pq_commute: "int p * int q = int q * int p" by simp
+
+lemma pq_ge_0: "int p * int q > 0" using p_ge_0 q_ge_0 mult_pos_pos by blast
+
+definition "r = ((p - 1) div 2)*((q - 1) div 2)"
+definition "m = card (GAUSS.E p q)"
+definition "n = card (GAUSS.E q p)"
+
+abbreviation "Res (k::int) \<equiv> {0 .. k - 1}"
+abbreviation "Res_ge_0 (k::int) \<equiv> {0 <.. k - 1}"
+abbreviation "Res_0 (k::int) \<equiv> {0::int}"
+abbreviation "Res_l (k::int) \<equiv> {0 <.. (k - 1) div 2}"
+abbreviation "Res_h (k::int) \<equiv> {(k - 1) div 2 <.. k - 1}"
+
+abbreviation "Sets_pq r0 r1 r2 \<equiv>
+ {(x::int). x \<in> r0 (int p * int q) \<and> x mod p \<in> r1 (int p) \<and> x mod q \<in> r2 (int q)}"
+
+definition "A = Sets_pq Res_l Res_l Res_h"
+definition "B = Sets_pq Res_l Res_h Res_l"
+definition "C = Sets_pq Res_h Res_h Res_l"
+definition "D = Sets_pq Res_l Res_h Res_h"
+definition "E = Sets_pq Res_l Res_0 Res_h"
+definition "F = Sets_pq Res_l Res_h Res_0"
+
+definition "a = card A"
+definition "b = card B"
+definition "c = card C"
+definition "d = card D"
+definition "e = card E"
+definition "f = card F"
+
+lemma Gpq: "GAUSS p q" unfolding GAUSS_def
+ using p_prime pq_neq p_ge_2 q_prime
+ by (auto simp: cong_altdef_int zdvd_int [symmetric] dest: primes_dvd_imp_eq)
+
+lemma Gqp: "GAUSS q p" using QRqp QR.Gpq by simp
+
+lemma QR_lemma_01: "(\<lambda>x. x mod q) ` E = GAUSS.E q p"
+proof
+ {
+ fix x
+ assume a1: "x \<in> E"
+ then obtain k where k: "x = int p * k" unfolding E_def by blast
+ have "x \<in> Res_l (int p * int q)" using a1 E_def by blast
+ hence "k \<in> GAUSS.A q" using Gqp GAUSS.A_def k qp_ineq by (simp add: zero_less_mult_iff)
+ hence "x mod q \<in> GAUSS.E q p"
+ using GAUSS.C_def[of q p] Gqp k GAUSS.B_def[of q p] a1 GAUSS.E_def[of q p]
+ unfolding E_def by force
+ hence "x \<in> E \<longrightarrow> x mod int q \<in> GAUSS.E q p" by auto
+ }
+ thus "(\<lambda>x. x mod int q) ` E \<subseteq> GAUSS.E q p" by auto
+next
+ show "GAUSS.E q p \<subseteq> (\<lambda>x. x mod q) ` E"
+ proof
+ fix x
+ assume a1: "x \<in> GAUSS.E q p"
+ then obtain ka where ka: "ka \<in> GAUSS.A q" "x = (ka * p) mod q"
+ using Gqp GAUSS.B_def GAUSS.C_def GAUSS.E_def by auto
+ hence "ka * p \<in> Res_l (int p * int q)"
+ using GAUSS.A_def Gqp p_ge_0 qp_ineq by (simp add: Groups.mult_ac(2))
+ thus "x \<in> (\<lambda>x. x mod q) ` E" unfolding E_def using ka a1 Gqp GAUSS.E_def q_ge_0 by force
+ qed
+qed
+
+lemma QR_lemma_02: "e= n"
+proof -
+ {
+ fix x y
+ assume a: "x \<in> E" "y \<in> E" "x mod q = y mod q"
+ obtain p_inv where p_inv: "[int p * p_inv = 1] (mod int q)"
+ using pq_coprime_int cong_solve_coprime_int by blast
+ obtain kx ky where k: "x = int p * kx" "y = int p * ky" using a E_def dvd_def[of p x] by blast
+ hence "0 < x" "int p * kx \<le> (int p * int q - 1) div 2"
+ "0 < y" "int p * ky \<le> (int p * int q - 1) div 2"
+ using E_def a greaterThanAtMost_iff mem_Collect_eq by blast+
+ hence "0 \<le> kx" "kx < q" "0 \<le> ky" "ky < q" using qp_ineq k by (simp add: zero_less_mult_iff)+
+ moreover have "(p_inv * (p * kx)) mod q = (p_inv * (p * ky)) mod q"
+ using a(3) mod_mult_cong k by blast
+ hence "(p * p_inv * kx) mod q = (p * p_inv * ky) mod q" by (simp add:algebra_simps)
+ hence "kx mod q = ky mod q"
+ using p_inv mod_mult_cong[of "p * p_inv" "q" "1"] cong_int_def by auto
+ hence "[kx = ky] (mod q)" using cong_int_def by blast
+ ultimately have "x = y" using cong_less_imp_eq_int k by blast
+ }
+ hence "inj_on (\<lambda>x. x mod q) E" unfolding inj_on_def by auto
+ thus ?thesis using QR_lemma_01 card_image e_def n_def by fastforce
+qed
+
+lemma QR_lemma_03: "f = m"
+proof -
+ have "F = QR.E q p" unfolding F_def pq_commute using QRqp QR.E_def[of q p] by fastforce
+ hence "f = QR.e q p" unfolding f_def using QRqp QR.e_def[of q p] by presburger
+ thus ?thesis using QRqp QR.QR_lemma_02 m_def QRqp QR.n_def by presburger
+qed
+
+definition f_1 :: "int \<Rightarrow> int \<times> int" where
+ "f_1 x = ((x mod p), (x mod q))"
+
+definition P_1 :: "int \<times> int \<Rightarrow> int \<Rightarrow> bool" where
+ "P_1 res x \<longleftrightarrow> x mod p = fst res & x mod q = snd res & x \<in> Res (int p * int q)"
+
+definition g_1 :: "int \<times> int \<Rightarrow> int" where
+ "g_1 res = (THE x. P_1 res x)"
+
+lemma P_1_lemma: assumes "0 \<le> fst res" "fst res < p" "0 \<le> snd res" "snd res < q"
+ shows "\<exists>! x. P_1 res x"
+proof -
+ obtain y k1 k2 where yk: "y = nat (fst res) + k1 * p" "y = nat (snd res) + k2 * q"
+ using chinese_remainder[of p q] pq_coprime p_ge_0 q_ge_0 by fastforce
+ have h1: "[y = fst res] (mod p)" "[y = snd res] (mod q)"
+ using yk(1) assms(1) cong_iff_lin_int[of "fst res"] cong_sym_int apply simp
+ using yk(2) assms(3) cong_iff_lin_int[of "snd res"] cong_sym_int by simp
+ have "(y mod (int p * int q)) mod int p = fst res" "(y mod (int p * int q)) mod int q = snd res"
+ using h1(1) mod_mod_cancel[of "int p"] assms(1) assms(2) cong_int_def apply simp
+ using h1(2) mod_mod_cancel[of "int q"] assms(3) assms(4) cong_int_def by simp
+ then obtain x where "P_1 res x" unfolding P_1_def
+ using Divides.pos_mod_bound Divides.pos_mod_sign pq_ge_0 by fastforce
+ moreover {
+ fix a b
+ assume a: "P_1 res a" "P_1 res b"
+ hence "int p * int q dvd a - b"
+ using divides_mult[of "int p" "a - b" "int q"] pq_coprime_int zmod_eq_dvd_iff[of a _ b]
+ unfolding P_1_def by force
+ hence "a = b" using dvd_imp_le_int[of "a - b"] a unfolding P_1_def by fastforce
+ }
+ ultimately show ?thesis by auto
+qed
+
+lemma g_1_lemma: assumes "0 \<le> fst res" "fst res < p" "0 \<le> snd res" "snd res < q"
+ shows "P_1 res (g_1 res)" using assms P_1_lemma theI'[of "P_1 res"] g_1_def by presburger
+
+definition "BuC = Sets_pq Res_ge_0 Res_h Res_l"
+
+lemma QR_lemma_04: "card BuC = card ((Res_h p) \<times> (Res_l q))"
+ using card_bij_eq[of f_1 "BuC" "(Res_h p) \<times> (Res_l q)" g_1]
+proof
+ {
+ fix x y
+ assume a: "x \<in> BuC" "y \<in> BuC" "f_1 x = f_1 y"
+ hence "int p * int q dvd x - y"
+ using f_1_def pq_coprime_int divides_mult[of "int p" "x - y" "int q"]
+ zmod_eq_dvd_iff[of x _ y] by auto
+ hence "x = y"
+ using dvd_imp_le_int[of "x - y" "int p * int q"] a unfolding BuC_def by force
+ }
+ thus "inj_on f_1 BuC" unfolding inj_on_def by auto
+next
+ {
+ fix x y
+ assume a: "x \<in> (Res_h p) \<times> (Res_l q)" "y \<in> (Res_h p) \<times> (Res_l q)" "g_1 x = g_1 y"
+ hence "0 \<le> fst x" "fst x < p" "0 \<le> snd x" "snd x < q"
+ "0 \<le> fst y" "fst y < p" "0 \<le> snd y" "snd y < q"
+ using mem_Sigma_iff prod.collapse by fastforce+
+ hence "x = y" using g_1_lemma[of x] g_1_lemma[of y] a P_1_def by fastforce
+ }
+ thus "inj_on g_1 ((Res_h p) \<times> (Res_l q))" unfolding inj_on_def by auto
+next
+ show "g_1 ` ((Res_h p) \<times> (Res_l q)) \<subseteq> BuC"
+ proof
+ fix y
+ assume "y \<in> g_1 ` ((Res_h p) \<times> (Res_l q))"
+ then obtain x where x: "y = g_1 x" "x \<in> ((Res_h p) \<times> (Res_l q))" by blast
+ hence "P_1 x y" using g_1_lemma by fastforce
+ thus "y \<in> BuC" unfolding P_1_def BuC_def mem_Collect_eq using x SigmaE prod.sel by fastforce
+ qed
+qed (auto simp: BuC_def finite_subset f_1_def)
+
+lemma QR_lemma_05: "card ((Res_h p) \<times> (Res_l q)) = r"
+proof -
+ have "card (Res_l q) = (q - 1) div 2" "card (Res_h p) = (p - 1) div 2" using p_eq2 by force+
+ thus ?thesis unfolding r_def using card_cartesian_product[of "Res_h p" "Res_l q"] by presburger
+qed
+
+lemma QR_lemma_06: "b + c = r"
+proof -
+ have "B \<inter> C = {}" "finite B" "finite C" "B \<union> C = BuC" unfolding B_def C_def BuC_def by fastforce+
+ thus ?thesis
+ unfolding b_def c_def using card_empty card_Un_Int QR_lemma_04 QR_lemma_05 by fastforce
+qed
+
+definition f_2:: "int \<Rightarrow> int" where
+ "f_2 x = (int p * int q) - x"
+
+lemma f_2_lemma_1: "\<And>x. f_2 (f_2 x) = x" unfolding f_2_def by simp
+
+lemma f_2_lemma_2: "[f_2 x = int p - x] (mod p)" unfolding f_2_def using cong_altdef_int by simp
+
+lemma f_2_lemma_3: "f_2 x \<in> S \<Longrightarrow> x \<in> f_2 ` S"
+ using f_2_lemma_1[of x] image_eqI[of x f_2 "f_2 x" S] by presburger
+
+lemma QR_lemma_07: "f_2 ` Res_l (int p * int q) = Res_h (int p * int q)"
+ "f_2 ` Res_h (int p * int q) = Res_l (int p * int q)"
+proof -
+ have h1: "f_2 ` Res_l (int p * int q) \<subseteq> Res_h (int p * int q)" using f_2_def by force
+ have h2: "f_2 ` Res_h (int p * int q) \<subseteq> Res_l (int p * int q)" using f_2_def pq_eq2 by fastforce
+ have h3: "Res_h (int p * int q) \<subseteq> f_2 ` Res_l (int p * int q)" using h2 f_2_lemma_3 by blast
+ have h4: "Res_l (int p * int q) \<subseteq> f_2 ` Res_h (int p * int q)" using h1 f_2_lemma_3 by blast
+ show "f_2 ` Res_l (int p * int q) = Res_h (int p * int q)" using h1 h3 by blast
+ show "f_2 ` Res_h (int p * int q) = Res_l (int p * int q)" using h2 h4 by blast
+qed
+
+lemma QR_lemma_08: "(f_2 x mod p \<in> Res_l p) = (x mod p \<in> Res_h p)"
+ "(f_2 x mod p \<in> Res_h p) = (x mod p \<in> Res_l p)"
+ using f_2_lemma_2[of x] cong_int_def[of "f_2 x" "p - x" p] minus_mod_self2[of x p]
+ zmod_zminus1_eq_if[of x p] p_eq2 by auto
+
+lemma QR_lemma_09: "(f_2 x mod q \<in> Res_l q) = (x mod q \<in> Res_h q)"
+ "(f_2 x mod q \<in> Res_h q) = (x mod q \<in> Res_l q)"
+ using QRqp QR.QR_lemma_08 f_2_def QR.f_2_def pq_commute by auto+
+
+lemma QR_lemma_10: "a = c" unfolding a_def c_def apply (rule card_bij_eq[of f_2 A C f_2])
+ unfolding A_def C_def
+ using QR_lemma_07 QR_lemma_08 QR_lemma_09 apply ((simp add: inj_on_def f_2_def),blast)+
+ by fastforce+
+
+definition "BuD = Sets_pq Res_l Res_h Res_ge_0"
+definition "BuDuF = Sets_pq Res_l Res_h Res"
+
+definition f_3 :: "int \<Rightarrow> int \<times> int" where
+ "f_3 x = (x mod p, x div p + 1)"
+
+definition g_3 :: "int \<times> int \<Rightarrow> int" where
+ "g_3 x = fst x + (snd x - 1) * p"
+
+lemma QR_lemma_11: "card BuDuF = card ((Res_h p) \<times> (Res_l q))"
+ using card_bij_eq[of f_3 BuDuF "(Res_h p) \<times> (Res_l q)" g_3]
+proof
+ show "f_3 ` BuDuF \<subseteq> (Res_h p) \<times> (Res_l q)"
+ proof
+ fix y
+ assume "y \<in> f_3 ` BuDuF"
+ then obtain x where x: "y = f_3 x" "x \<in> BuDuF" by blast
+ hence "x \<le> int p * (int q - 1) div 2 + (int p - 1) div 2"
+ unfolding BuDuF_def using p_eq2 int_distrib(4) by auto
+ moreover have "(int p - 1) div 2 \<le> - 1 + x mod p" using x BuDuF_def by auto
+ moreover have "int p * (int q - 1) div 2 = int p * ((int q - 1) div 2)"
+ using zdiv_zmult1_eq odd_q by auto
+ hence "p * (int q - 1) div 2 = p * ((int q + 1) div 2 - 1)" by fastforce
+ ultimately have "x \<le> p * ((int q + 1) div 2 - 1) - 1 + x mod p" by linarith
+ hence "x div p < (int q + 1) div 2 - 1"
+ using mult.commute[of "int p" "x div p"] p_ge_0 div_mult_mod_eq[of x p]
+ mult_less_cancel_left_pos[of p "x div p" "(int q + 1) div 2 - 1"] by linarith
+ moreover have "0 < x div p + 1"
+ using pos_imp_zdiv_neg_iff[of p x] p_ge_0 x mem_Collect_eq BuDuF_def by auto
+ ultimately show "y \<in> (Res_h p) \<times> (Res_l q)" using x BuDuF_def f_3_def by auto
+ qed
+next
+ have h1: "\<And>x. x \<in> ((Res_h p) \<times> (Res_l q)) \<Longrightarrow> f_3 (g_3 x) = x"
+ proof -
+ fix x
+ assume a: "x \<in> ((Res_h p) \<times> (Res_l q))"
+ moreover have h: "(fst x + (snd x - 1) * int p) mod int p = fst x" using a by force
+ ultimately have "(fst x + (snd x - 1) * int p) div int p + 1 = snd x"
+ by (auto simp: semiring_numeral_div_class.div_less)
+ with h show "f_3 (g_3 x) = x" unfolding f_3_def g_3_def by simp
+ qed
+ show "inj_on g_3 ((Res_h p) \<times> (Res_l q))" apply (rule inj_onI[of "(Res_h p) \<times> (Res_l q)" g_3])
+ proof -
+ fix x y
+ assume "x \<in> ((Res_h p) \<times> (Res_l q))" "y \<in> ((Res_h p) \<times> (Res_l q))" "g_3 x = g_3 y"
+ thus "x = y" using h1[of x] h1[of y] by presburger
+ qed
+next
+ show "g_3 ` ((Res_h p) \<times> (Res_l q)) \<subseteq> BuDuF"
+ proof
+ fix y
+ assume "y \<in> g_3 ` ((Res_h p) \<times> (Res_l q))"
+ then obtain x where x: "y = g_3 x" "x \<in> (Res_h p) \<times> (Res_l q)" by blast
+ hence "snd x \<le> (int q - 1) div 2" by force
+ moreover have "int p * ((int q - 1) div 2) = (int p * int q - int p) div 2"
+ using int_distrib(4) zdiv_zmult1_eq[of "int p" "int q - 1" 2] odd_q by fastforce
+ ultimately have "(snd x) * int p \<le> (int q * int p - int p) div 2"
+ using mult_right_mono[of "snd x" "(int q - 1) div 2" p] mult.commute[of "(int q - 1) div 2" p]
+ pq_commute by presburger
+ hence "(snd x - 1) * int p \<le> (int q * int p - 1) div 2 - int p"
+ using p_ge_0 int_distrib(3) by auto
+ moreover have "fst x \<le> int p - 1" using x by force
+ ultimately have "fst x + (snd x - 1) * int p \<le> (int p * int q - 1) div 2"
+ using pq_commute by linarith
+ moreover have "0 < fst x" "0 \<le> (snd x - 1) * p" using x(2) by fastforce+
+ ultimately show "y \<in> BuDuF" unfolding BuDuF_def using q_ge_0 x g_3_def x(1) by auto
+ qed
+next
+ show "finite BuDuF" unfolding BuDuF_def by fastforce
+qed (simp add: inj_on_inverseI[of BuDuF g_3] f_3_def g_3_def QR_lemma_05)+
+
+lemma QR_lemma_12: "b + d + m = r"
+proof -
+ have "B \<inter> D = {}" "finite B" "finite D" "B \<union> D = BuD" unfolding B_def D_def BuD_def by fastforce+
+ hence "b + d = card BuD" unfolding b_def d_def using card_Un_Int by fastforce
+ moreover have "BuD \<inter> F = {}" "finite BuD" "finite F" unfolding BuD_def F_def by fastforce+
+ moreover have "BuD \<union> F = BuDuF" unfolding BuD_def F_def BuDuF_def
+ using q_ge_0 ivl_disj_un_singleton(5)[of 0 "int q - 1"] by auto
+ ultimately show ?thesis using QR_lemma_03 QR_lemma_05 QR_lemma_11 card_Un_disjoint[of BuD F]
+ unfolding b_def d_def f_def by presburger
+qed
+
+lemma QR_lemma_13: "a + d + n = r"
+proof -
+ have "A = QR.B q p" unfolding A_def pq_commute using QRqp QR.B_def[of q p] by blast
+ hence "a = QR.b q p" using a_def QRqp QR.b_def[of q p] by presburger
+ moreover have "D = QR.D q p" unfolding D_def pq_commute using QRqp QR.D_def[of q p] by blast
+ hence "d = QR.d q p" using d_def QRqp QR.d_def[of q p] by presburger
+ moreover have "n = QR.m q p" using n_def QRqp QR.m_def[of q p] by presburger
+ moreover have "r = QR.r q p" unfolding r_def using QRqp QR.r_def[of q p] by auto
+ ultimately show ?thesis using QRqp QR.QR_lemma_12 by presburger
+qed
+
+lemma QR_lemma_14: "(-1::int) ^ (m + n) = (-1) ^ r"
+proof -
+ have "m + n + 2 * d = r" using QR_lemma_06 QR_lemma_10 QR_lemma_12 QR_lemma_13 by auto
+ thus ?thesis using power_add[of "-1::int" "m + n" "2 * d"] by fastforce
+qed
+
+lemma Quadratic_Reciprocity:
+ "(Legendre p q) * (Legendre q p) = (-1::int) ^ ((p - 1) div 2 * ((q - 1) div 2))"
+ using Gpq Gqp GAUSS.gauss_lemma power_add[of "-1::int" m n] QR_lemma_14
+ unfolding r_def m_def n_def by auto
+
+end
+
+theorem Quadratic_Reciprocity: assumes "prime p" "2 < p" "prime q" "2 < q" "p \<noteq> q"
+ shows "(Legendre p q) * (Legendre q p) = (-1::int) ^ ((p - 1) div 2 * ((q - 1) div 2))"
+ using QR.Quadratic_Reciprocity QR_def assms by blast
+
+theorem Quadratic_Reciprocity_int: assumes "prime (nat p)" "2 < p" "prime (nat q)" "2 < q" "p \<noteq> q"
+ shows "(Legendre p q) * (Legendre q p) = (-1::int) ^ (nat ((p - 1) div 2 * ((q - 1) div 2)))"
+proof -
+ have "0 \<le> (p - 1) div 2" using assms by simp
+ moreover have "(nat p - 1) div 2 = nat ((p - 1) div 2)" "(nat q - 1) div 2 = nat ((q - 1) div 2)"
+ by fastforce+
+ ultimately have "(nat p - 1) div 2 * ((nat q - 1) div 2) = nat ((p - 1) div 2 * ((q - 1) div 2))"
+ using nat_mult_distrib by presburger
+ moreover have "2 < nat p" "2 < nat q" "nat p \<noteq> nat q" "int (nat p) = p" "int (nat q) = q"
+ using assms by linarith+
+ ultimately show ?thesis using Quadratic_Reciprocity[of "nat p" "nat q"] assms by presburger
+qed
+
+end
--- a/src/HOL/Probability/Distribution_Functions.thy Thu Oct 20 23:42:12 2016 +0200
+++ b/src/HOL/Probability/Distribution_Functions.thy Thu Oct 20 23:42:41 2016 +0200
@@ -36,11 +36,11 @@
by (simp add: cdf_def)
locale finite_borel_measure = finite_measure M for M :: "real measure" +
- assumes M_super_borel: "sets borel \<subseteq> sets M"
+ assumes M_is_borel: "sets M = sets borel"
begin
lemma sets_M[intro]: "a \<in> sets borel \<Longrightarrow> a \<in> sets M"
- using M_super_borel by auto
+ using M_is_borel by auto
lemma cdf_diff_eq:
assumes "x < y"
@@ -57,7 +57,7 @@
unfolding cdf_def by (auto intro!: finite_measure_mono)
lemma borel_UNIV: "space M = UNIV"
- by (metis in_mono sets.sets_into_space space_in_borel top_le M_super_borel)
+ by (metis in_mono sets.sets_into_space space_in_borel top_le M_is_borel)
lemma cdf_nonneg: "cdf M x \<ge> 0"
unfolding cdf_def by (rule measure_nonneg)
@@ -142,11 +142,17 @@
end
locale real_distribution = prob_space M for M :: "real measure" +
- assumes events_eq_borel [simp, measurable_cong]: "sets M = sets borel" and space_eq_univ [simp]: "space M = UNIV"
+ assumes events_eq_borel [simp, measurable_cong]: "sets M = sets borel"
begin
+lemma finite_borel_measure_M: "finite_borel_measure M"
+ by standard auto
+
sublocale finite_borel_measure M
- by standard auto
+ by (rule finite_borel_measure_M)
+
+lemma space_eq_univ [simp]: "space M = UNIV"
+ using events_eq_borel[THEN sets_eq_imp_space_eq] by simp
lemma cdf_bounded_prob: "\<And>x. cdf M x \<le> 1"
by (subst prob_space [symmetric], rule cdf_bounded)
@@ -167,20 +173,23 @@
"random_variable borel X \<Longrightarrow> real_distribution (distr M borel X)"
unfolding real_distribution_def real_distribution_axioms_def by (auto intro!: prob_space_distr)
-subsection \<open>uniqueness\<close>
+subsection \<open>Uniqueness\<close>
-lemma (in real_distribution) emeasure_Ioc:
+lemma (in finite_borel_measure) emeasure_Ioc:
assumes "a \<le> b" shows "emeasure M {a <.. b} = cdf M b - cdf M a"
proof -
have "{a <.. b} = {..b} - {..a}"
by auto
- with \<open>a \<le> b\<close> show ?thesis
+ moreover have "{..x} \<in> sets M" for x
+ using atMost_borel[of x] M_is_borel by auto
+ moreover note \<open>a \<le> b\<close>
+ ultimately show ?thesis
by (simp add: emeasure_eq_measure finite_measure_Diff cdf_def)
qed
-lemma cdf_unique:
+lemma cdf_unique':
fixes M1 M2
- assumes "real_distribution M1" and "real_distribution M2"
+ assumes "finite_borel_measure M1" and "finite_borel_measure M2"
assumes "cdf M1 = cdf M2"
shows "M1 = M2"
proof (rule measure_eqI_generator_eq[where \<Omega>=UNIV])
@@ -188,14 +197,56 @@
then obtain a b where Xeq: "X = {a<..b}" by auto
then show "emeasure M1 X = emeasure M2 X"
by (cases "a \<le> b")
- (simp_all add: assms(1,2)[THEN real_distribution.emeasure_Ioc] assms(3))
+ (simp_all add: assms(1,2)[THEN finite_borel_measure.emeasure_Ioc] assms(3))
next
show "(\<Union>i. {- real (i::nat)<..real i}) = UNIV"
by (rule UN_Ioc_eq_UNIV)
-qed (auto simp: real_distribution.emeasure_Ioc[OF assms(1)]
- assms(1,2)[THEN real_distribution.events_eq_borel] borel_sigma_sets_Ioc
+qed (auto simp: finite_borel_measure.emeasure_Ioc[OF assms(1)]
+ assms(1,2)[THEN finite_borel_measure.M_is_borel] borel_sigma_sets_Ioc
Int_stable_def)
+lemma cdf_unique:
+ "real_distribution M1 \<Longrightarrow> real_distribution M2 \<Longrightarrow> cdf M1 = cdf M2 \<Longrightarrow> M1 = M2"
+ using cdf_unique'[of M1 M2] by (simp add: real_distribution.finite_borel_measure_M)
+
+lemma
+ fixes F :: "real \<Rightarrow> real"
+ assumes nondecF : "\<And> x y. x \<le> y \<Longrightarrow> F x \<le> F y"
+ and right_cont_F : "\<And>a. continuous (at_right a) F"
+ and lim_F_at_bot : "(F \<longlongrightarrow> 0) at_bot"
+ and lim_F_at_top : "(F \<longlongrightarrow> m) at_top"
+ and m: "0 \<le> m"
+ shows interval_measure_UNIV: "emeasure (interval_measure F) UNIV = m"
+ and finite_borel_measure_interval_measure: "finite_borel_measure (interval_measure F)"
+proof -
+ let ?F = "interval_measure F"
+ { have "ennreal (m - 0) = (SUP i::nat. ennreal (F (real i) - F (- real i)))"
+ by (intro LIMSEQ_unique[OF _ LIMSEQ_SUP] tendsto_ennrealI tendsto_intros
+ lim_F_at_bot[THEN filterlim_compose] lim_F_at_top[THEN filterlim_compose]
+ lim_F_at_bot[THEN filterlim_compose] filterlim_real_sequentially
+ filterlim_uminus_at_top[THEN iffD1])
+ (auto simp: incseq_def nondecF intro!: diff_mono)
+ also have "\<dots> = (SUP i::nat. emeasure ?F {- real i<..real i})"
+ by (subst emeasure_interval_measure_Ioc) (simp_all add: nondecF right_cont_F)
+ also have "\<dots> = emeasure ?F (\<Union>i::nat. {- real i<..real i})"
+ by (rule SUP_emeasure_incseq) (auto simp: incseq_def)
+ also have "(\<Union>i. {- real (i::nat)<..real i}) = space ?F"
+ by (simp add: UN_Ioc_eq_UNIV)
+ finally have "emeasure ?F (space ?F) = m"
+ by simp }
+ note * = this
+ then show "emeasure (interval_measure F) UNIV = m"
+ by simp
+
+ interpret finite_measure ?F
+ proof
+ show "emeasure ?F (space ?F) \<noteq> \<infinity>"
+ using * by simp
+ qed
+ show "finite_borel_measure (interval_measure F)"
+ proof qed simp_all
+qed
+
lemma real_distribution_interval_measure:
fixes F :: "real \<Rightarrow> real"
assumes nondecF : "\<And> x y. x \<le> y \<Longrightarrow> F x \<le> F y" and
@@ -206,53 +257,47 @@
proof -
let ?F = "interval_measure F"
interpret prob_space ?F
- proof
- have "ennreal (1 - 0) = (SUP i::nat. ennreal (F (real i) - F (- real i)))"
- by (intro LIMSEQ_unique[OF _ LIMSEQ_SUP] tendsto_ennrealI tendsto_intros
- lim_F_at_bot[THEN filterlim_compose] lim_F_at_top[THEN filterlim_compose]
- lim_F_at_bot[THEN filterlim_compose] filterlim_real_sequentially
- filterlim_uminus_at_top[THEN iffD1])
- (auto simp: incseq_def nondecF intro!: diff_mono)
- also have "\<dots> = (SUP i::nat. emeasure ?F {- real i<..real i})"
- by (subst emeasure_interval_measure_Ioc) (simp_all add: nondecF right_cont_F)
- also have "\<dots> = emeasure ?F (\<Union>i::nat. {- real i<..real i})"
- by (rule SUP_emeasure_incseq) (auto simp: incseq_def)
- also have "(\<Union>i. {- real (i::nat)<..real i}) = space ?F"
- by (simp add: UN_Ioc_eq_UNIV)
- finally show "emeasure ?F (space ?F) = 1"
- by (simp add: one_ereal_def)
- qed
+ proof qed (use interval_measure_UNIV[OF assms] in simp)
show ?thesis
proof qed simp_all
qed
-lemma cdf_interval_measure:
+lemma
fixes F :: "real \<Rightarrow> real"
assumes nondecF : "\<And> x y. x \<le> y \<Longrightarrow> F x \<le> F y" and
right_cont_F : "\<And>a. continuous (at_right a) F" and
- lim_F_at_bot : "(F \<longlongrightarrow> 0) at_bot" and
- lim_F_at_top : "(F \<longlongrightarrow> 1) at_top"
- shows "cdf (interval_measure F) = F"
+ lim_F_at_bot : "(F \<longlongrightarrow> 0) at_bot"
+ shows emeasure_interval_measure_Iic: "emeasure (interval_measure F) {.. x} = F x"
+ and measure_interval_measure_Iic: "measure (interval_measure F) {.. x} = F x"
unfolding cdf_def
-proof (intro ext)
- interpret real_distribution "interval_measure F"
- by (rule real_distribution_interval_measure) fact+
- fix x
- have "F x - 0 = measure (interval_measure F) (\<Union>i::nat. {-real i <.. x})"
- proof (intro LIMSEQ_unique[OF _ finite_Lim_measure_incseq])
+proof -
+ have F_nonneg[simp]: "0 \<le> F y" for y
+ using lim_F_at_bot by (rule tendsto_upperbound) (auto simp: eventually_at_bot_linorder nondecF intro!: exI[of _ y])
+
+ have "emeasure (interval_measure F) (\<Union>i::nat. {-real i <.. x}) = F x - ennreal 0"
+ proof (intro LIMSEQ_unique[OF Lim_emeasure_incseq])
have "(\<lambda>i. F x - F (- real i)) \<longlonglongrightarrow> F x - 0"
by (intro tendsto_intros lim_F_at_bot[THEN filterlim_compose] filterlim_real_sequentially
filterlim_uminus_at_top[THEN iffD1])
- then show "(\<lambda>i. measure (interval_measure F) {- real i<..x}) \<longlonglongrightarrow> F x - 0"
- apply (rule filterlim_cong[OF refl refl, THEN iffD1, rotated])
+ from tendsto_ennrealI[OF this]
+ show "(\<lambda>i. emeasure (interval_measure F) {- real i<..x}) \<longlonglongrightarrow> F x - ennreal 0"
+ apply (rule filterlim_cong[THEN iffD1, rotated 3])
+ apply simp
+ apply simp
apply (rule eventually_sequentiallyI[where c="nat (ceiling (- x))"])
- apply (simp add: measure_interval_measure_Ioc right_cont_F nondecF)
+ apply (simp add: emeasure_interval_measure_Ioc right_cont_F nondecF)
done
qed (auto simp: incseq_def)
also have "(\<Union>i::nat. {-real i <.. x}) = {..x}"
by auto (metis minus_minus neg_less_iff_less reals_Archimedean2)
- finally show "measure (interval_measure F) {..x} = F x"
+ finally show "emeasure (interval_measure F) {..x} = F x"
by simp
+ then show "measure (interval_measure F) {..x} = F x"
+ by (simp add: measure_def)
qed
+lemma cdf_interval_measure:
+ "(\<And> x y. x \<le> y \<Longrightarrow> F x \<le> F y) \<Longrightarrow> (\<And>a. continuous (at_right a) F) \<Longrightarrow> (F \<longlongrightarrow> 0) at_bot \<Longrightarrow> cdf (interval_measure F) = F"
+ by (simp add: cdf_def fun_eq_iff measure_interval_measure_Iic)
+
end
--- a/src/HOL/Probability/Essential_Supremum.thy Thu Oct 20 23:42:12 2016 +0200
+++ b/src/HOL/Probability/Essential_Supremum.thy Thu Oct 20 23:42:41 2016 +0200
@@ -13,18 +13,18 @@
of measure $0$. It is convenient to define it to be infinity for non-measurable functions, as
it allows for neater statements in general. This is a prerequisiste to define the space $L^\infty$.*}
-definition esssup::"'a measure \<Rightarrow> ('a \<Rightarrow> ereal) \<Rightarrow> ereal"
- where "esssup M f = (if f \<in> borel_measurable M then Inf {z. emeasure M {x \<in> space M. f x > z} = 0} else \<infinity>)"
+definition esssup::"'a measure \<Rightarrow> ('a \<Rightarrow> 'b::{second_countable_topology, dense_linorder, linorder_topology, complete_linorder}) \<Rightarrow> 'b"
+ where "esssup M f = (if f \<in> borel_measurable M then Inf {z. emeasure M {x \<in> space M. f x > z} = 0} else top)"
lemma esssup_zero_measure:
"emeasure M {x \<in> space M. f x > esssup M f} = 0"
-proof (cases "esssup M f = \<infinity>")
+proof (cases "esssup M f = top")
case True
then show ?thesis by auto
next
case False
then have [measurable]: "f \<in> borel_measurable M" unfolding esssup_def by meson
- have "esssup M f < \<infinity>" using False by auto
+ have "esssup M f < top" using False by (auto simp: less_top)
have *: "{x \<in> space M. f x > z} \<in> null_sets M" if "z > esssup M f" for z
proof -
have "\<exists>w. w < z \<and> emeasure M {x \<in> space M. f x > w} = 0"
@@ -35,8 +35,8 @@
have b: "{x \<in> space M. f x > z} \<subseteq> {x \<in> space M. f x > w}" using `w < z` by auto
show ?thesis using null_sets_subset[OF a _ b] by simp
qed
- obtain u::"nat \<Rightarrow> ereal" where u: "\<And>n. u n > esssup M f" "u \<longlonglongrightarrow> esssup M f"
- using approx_from_above_dense_linorder[OF `esssup M f < \<infinity>`] by auto
+ obtain u::"nat \<Rightarrow> 'b" where u: "\<And>n. u n > esssup M f" "u \<longlonglongrightarrow> esssup M f"
+ using approx_from_above_dense_linorder[OF `esssup M f < top`] by auto
have "{x \<in> space M. f x > esssup M f} = (\<Union>n. {x \<in> space M. f x > u n})"
using u apply auto
apply (metis (mono_tags, lifting) order_tendsto_iff eventually_mono LIMSEQ_unique)
@@ -54,7 +54,7 @@
apply (rule AE_I[OF _ esssup_zero_measure[of _ f]]) using True by auto
next
case False
- then have "esssup M f = \<infinity>" unfolding esssup_def by auto
+ then have "esssup M f = top" unfolding esssup_def by auto
then show ?thesis by auto
qed
@@ -65,7 +65,7 @@
lemma esssup_non_measurable:
assumes "f \<notin> borel_measurable M"
- shows "esssup M f = \<infinity>"
+ shows "esssup M f = top"
using assms unfolding esssup_def by auto
lemma esssup_I [intro]:
@@ -122,7 +122,7 @@
lemma esssup_cmult:
assumes "c > (0::real)"
- shows "esssup M (\<lambda>x. c * f x) = c * esssup M f"
+ shows "esssup M (\<lambda>x. c * f x::ereal) = c * esssup M f"
proof (cases "f \<in> borel_measurable M")
case True
then have a [measurable]: "f \<in> borel_measurable M" by simp
@@ -154,8 +154,8 @@
finally show ?thesis by simp
next
case False
- have "esssup M f = \<infinity>" using False unfolding esssup_def by auto
- then have *: "c * esssup M f = \<infinity>" using assms by (simp add: ennreal_mult_eq_top_iff)
+ have "esssup M f = top" using False unfolding esssup_def by auto
+ then have *: "c * esssup M f = \<infinity>" using assms by (simp add: ennreal_mult_eq_top_iff top_ereal_def)
have "(\<lambda>x. c * f x) \<notin> borel_measurable M"
proof (rule ccontr)
assume "\<not> (\<lambda>x. c * f x) \<notin> borel_measurable M"
@@ -165,12 +165,12 @@
by (metis "*" PInfty_neq_ereal(1) divide_inverse divide_self_if ereal_zero_mult mult.assoc mult.commute mult.left_neutral one_ereal_def times_ereal.simps(1) zero_ereal_def)
ultimately show False using False by auto
qed
- then have "esssup M (\<lambda>x. c * f x) = \<infinity>" unfolding esssup_def by simp
+ then have "esssup M (\<lambda>x. c * f x) = \<infinity>" unfolding esssup_def by (simp add: top_ereal_def)
then show ?thesis using * by auto
qed
lemma esssup_add:
- "esssup M (\<lambda>x. f x + g x) \<le> esssup M f + esssup M g"
+ "esssup M (\<lambda>x. f x + g x::ereal) \<le> esssup M f + esssup M g"
proof (cases "f \<in> borel_measurable M \<and> g \<in> borel_measurable M")
case True
then have [measurable]: "(\<lambda>x. f x + g x) \<in> borel_measurable M" by auto
@@ -181,14 +181,14 @@
then show ?thesis using esssup_I by auto
next
case False
- then have "esssup M f + esssup M g = \<infinity>" unfolding esssup_def by auto
+ then have "esssup M f + esssup M g = \<infinity>" unfolding esssup_def top_ereal_def by auto
then show ?thesis by auto
qed
lemma esssup_zero_space:
assumes "emeasure M (space M) = 0"
"f \<in> borel_measurable M"
- shows "esssup M f = - \<infinity>"
+ shows "esssup M f = (- \<infinity>::ereal)"
proof -
have "emeasure M {x \<in> space M. f x > - \<infinity>} = 0"
using assms(1) emeasure_mono emeasure_eq_0 by fastforce
--- a/src/HOL/Probability/Giry_Monad.thy Thu Oct 20 23:42:12 2016 +0200
+++ b/src/HOL/Probability/Giry_Monad.thy Thu Oct 20 23:42:41 2016 +0200
@@ -1778,4 +1778,10 @@
shows "space (M \<bind> f) = space B"
using M by (intro space_bind[OF sets_kernel[OF f]]) auto
+lemma bind_distr_return:
+ "f \<in> M \<rightarrow>\<^sub>M N \<Longrightarrow> g \<in> N \<rightarrow>\<^sub>M L \<Longrightarrow> space M \<noteq> {} \<Longrightarrow>
+ distr M N f \<bind> (\<lambda>x. return L (g x)) = distr M L (\<lambda>x. g (f x))"
+ by (subst bind_distr[OF _ measurable_compose[OF _ return_measurable]])
+ (auto intro!: bind_return_distr')
+
end
--- a/src/HOL/Probability/Probability.thy Thu Oct 20 23:42:12 2016 +0200
+++ b/src/HOL/Probability/Probability.thy Thu Oct 20 23:42:41 2016 +0200
@@ -13,6 +13,7 @@
Stream_Space
Conditional_Expectation
Essential_Supremum
+ Stopping_Time
begin
end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Probability/Stopping_Time.thy Thu Oct 20 23:42:41 2016 +0200
@@ -0,0 +1,262 @@
+(* Author: Johannes Hölzl <hoelzl@in.tum.de> *)
+
+section {* Stopping times *}
+
+theory Stopping_Time
+ imports "../Analysis/Analysis"
+begin
+
+subsection \<open>Stopping Time\<close>
+
+text \<open>This is also called strong stopping time. Then stopping time is T with alternative is
+ \<open>T x < t\<close> measurable.\<close>
+
+definition stopping_time :: "('t::linorder \<Rightarrow> 'a measure) \<Rightarrow> ('a \<Rightarrow> 't) \<Rightarrow> bool"
+where
+ "stopping_time F T = (\<forall>t. Measurable.pred (F t) (\<lambda>x. T x \<le> t))"
+
+lemma stopping_time_cong: "(\<And>t x. x \<in> space (F t) \<Longrightarrow> T x = S x) \<Longrightarrow> stopping_time F T = stopping_time F S"
+ unfolding stopping_time_def by (intro arg_cong[where f=All] ext measurable_cong) simp
+
+lemma stopping_timeD: "stopping_time F T \<Longrightarrow> Measurable.pred (F t) (\<lambda>x. T x \<le> t)"
+ by (auto simp: stopping_time_def)
+
+lemma stopping_timeD2: "stopping_time F T \<Longrightarrow> Measurable.pred (F t) (\<lambda>x. t < T x)"
+ unfolding not_le[symmetric] by (auto intro: stopping_timeD Measurable.pred_intros_logic)
+
+lemma stopping_timeI[intro?]: "(\<And>t. Measurable.pred (F t) (\<lambda>x. T x \<le> t)) \<Longrightarrow> stopping_time F T"
+ by (auto simp: stopping_time_def)
+
+lemma measurable_stopping_time:
+ fixes T :: "'a \<Rightarrow> 't::{linorder_topology, second_countable_topology}"
+ assumes T: "stopping_time F T"
+ and M: "\<And>t. sets (F t) \<subseteq> sets M" "\<And>t. space (F t) = space M"
+ shows "T \<in> M \<rightarrow>\<^sub>M borel"
+proof (rule borel_measurableI_le)
+ show "{x \<in> space M. T x \<le> t} \<in> sets M" for t
+ using stopping_timeD[OF T] M by (auto simp: Measurable.pred_def)
+qed
+
+lemma stopping_time_const: "stopping_time F (\<lambda>x. c)"
+ by (auto simp: stopping_time_def)
+
+lemma stopping_time_min:
+ "stopping_time F T \<Longrightarrow> stopping_time F S \<Longrightarrow> stopping_time F (\<lambda>x. min (T x) (S x))"
+ by (auto simp: stopping_time_def min_le_iff_disj intro!: pred_intros_logic)
+
+lemma stopping_time_max:
+ "stopping_time F T \<Longrightarrow> stopping_time F S \<Longrightarrow> stopping_time F (\<lambda>x. max (T x) (S x))"
+ by (auto simp: stopping_time_def intro!: pred_intros_logic)
+
+section \<open>Filtration\<close>
+
+locale filtration =
+ fixes \<Omega> :: "'a set" and F :: "'t::{linorder_topology, second_countable_topology} \<Rightarrow> 'a measure"
+ assumes space_F: "\<And>i. space (F i) = \<Omega>"
+ assumes sets_F_mono: "\<And>i j. i \<le> j \<Longrightarrow> sets (F i) \<le> sets (F j)"
+begin
+
+subsection \<open>$\sigma$-algebra of a Stopping Time\<close>
+
+definition pre_sigma :: "('a \<Rightarrow> 't) \<Rightarrow> 'a measure"
+where
+ "pre_sigma T = sigma \<Omega> {A. \<forall>t. {\<omega>\<in>A. T \<omega> \<le> t} \<in> sets (F t)}"
+
+lemma space_pre_sigma: "space (pre_sigma T) = \<Omega>"
+ unfolding pre_sigma_def using sets.space_closed[of "F _"]
+ by (intro space_measure_of) (auto simp: space_F)
+
+lemma measure_pre_sigma[simp]: "emeasure (pre_sigma T) = (\<lambda>_. 0)"
+ by (simp add: pre_sigma_def emeasure_sigma)
+
+lemma sigma_algebra_pre_sigma:
+ assumes T: "stopping_time F T"
+ shows "sigma_algebra \<Omega> {A. \<forall>t. {\<omega>\<in>A. T \<omega> \<le> t} \<in> sets (F t)}"
+ unfolding sigma_algebra_iff2
+proof (intro sigma_algebra_iff2[THEN iffD2] conjI ballI allI impI CollectI)
+ show "{A. \<forall>t. {\<omega> \<in> A. T \<omega> \<le> t} \<in> sets (F t)} \<subseteq> Pow \<Omega>"
+ using sets.space_closed[of "F _"] by (auto simp: space_F)
+next
+ fix A t assume "A \<in> {A. \<forall>t. {\<omega> \<in> A. T \<omega> \<le> t} \<in> sets (F t)}"
+ then have "{\<omega> \<in> space (F t). T \<omega> \<le> t} - {\<omega> \<in> A. T \<omega> \<le> t} \<in> sets (F t)"
+ using T stopping_timeD[measurable] by auto
+ also have "{\<omega> \<in> space (F t). T \<omega> \<le> t} - {\<omega> \<in> A. T \<omega> \<le> t} = {\<omega> \<in> \<Omega> - A. T \<omega> \<le> t}"
+ by (auto simp: space_F)
+ finally show "{\<omega> \<in> \<Omega> - A. T \<omega> \<le> t} \<in> sets (F t)" .
+next
+ fix AA :: "nat \<Rightarrow> 'a set" and t assume "range AA \<subseteq> {A. \<forall>t. {\<omega> \<in> A. T \<omega> \<le> t} \<in> sets (F t)}"
+ then have "(\<Union>i. {\<omega> \<in> AA i. T \<omega> \<le> t}) \<in> sets (F t)" for t
+ by auto
+ also have "(\<Union>i. {\<omega> \<in> AA i. T \<omega> \<le> t}) = {\<omega> \<in> UNION UNIV AA. T \<omega> \<le> t}"
+ by auto
+ finally show "{\<omega> \<in> UNION UNIV AA. T \<omega> \<le> t} \<in> sets (F t)" .
+qed auto
+
+lemma sets_pre_sigma: "stopping_time F T \<Longrightarrow> sets (pre_sigma T) = {A. \<forall>t. {\<omega>\<in>A. T \<omega> \<le> t} \<in> sets (F t)}"
+ unfolding pre_sigma_def by (rule sigma_algebra.sets_measure_of_eq[OF sigma_algebra_pre_sigma])
+
+lemma sets_pre_sigmaI: "stopping_time F T \<Longrightarrow> (\<And>t. {\<omega>\<in>A. T \<omega> \<le> t} \<in> sets (F t)) \<Longrightarrow> A \<in> sets (pre_sigma T)"
+ unfolding sets_pre_sigma by auto
+
+lemma pred_pre_sigmaI:
+ assumes T: "stopping_time F T"
+ shows "(\<And>t. Measurable.pred (F t) (\<lambda>\<omega>. P \<omega> \<and> T \<omega> \<le> t)) \<Longrightarrow> Measurable.pred (pre_sigma T) P"
+ unfolding pred_def space_F space_pre_sigma by (intro sets_pre_sigmaI[OF T]) simp
+
+lemma sets_pre_sigmaD: "stopping_time F T \<Longrightarrow> A \<in> sets (pre_sigma T) \<Longrightarrow> {\<omega>\<in>A. T \<omega> \<le> t} \<in> sets (F t)"
+ unfolding sets_pre_sigma by auto
+
+lemma stopping_time_le_const: "stopping_time F T \<Longrightarrow> s \<le> t \<Longrightarrow> Measurable.pred (F t) (\<lambda>\<omega>. T \<omega> \<le> s)"
+ using stopping_timeD[of F T] sets_F_mono[of _ t] by (auto simp: pred_def space_F)
+
+lemma measurable_stopping_time_pre_sigma:
+ assumes T: "stopping_time F T" shows "T \<in> pre_sigma T \<rightarrow>\<^sub>M borel"
+proof (intro borel_measurableI_le sets_pre_sigmaI[OF T])
+ fix t t'
+ have "{\<omega>\<in>space (F (min t' t)). T \<omega> \<le> min t' t} \<in> sets (F (min t' t))"
+ using T unfolding pred_def[symmetric] by (rule stopping_timeD)
+ also have "\<dots> \<subseteq> sets (F t)"
+ by (rule sets_F_mono) simp
+ finally show "{\<omega> \<in> {x \<in> space (pre_sigma T). T x \<le> t'}. T \<omega> \<le> t} \<in> sets (F t)"
+ by (simp add: space_pre_sigma space_F)
+qed
+
+lemma mono_pre_sigma:
+ assumes T: "stopping_time F T" and S: "stopping_time F S"
+ and le: "\<And>\<omega>. \<omega> \<in> \<Omega> \<Longrightarrow> T \<omega> \<le> S \<omega>"
+ shows "sets (pre_sigma T) \<subseteq> sets (pre_sigma S)"
+ unfolding sets_pre_sigma[OF S] sets_pre_sigma[OF T]
+proof safe
+ interpret sigma_algebra \<Omega> "{A. \<forall>t. {\<omega>\<in>A. T \<omega> \<le> t} \<in> sets (F t)}"
+ using T by (rule sigma_algebra_pre_sigma)
+ fix A t assume A: "\<forall>t. {\<omega>\<in>A. T \<omega> \<le> t} \<in> sets (F t)"
+ then have "A \<subseteq> \<Omega>"
+ using sets_into_space by auto
+ from A have "{\<omega>\<in>A. T \<omega> \<le> t} \<inter> {\<omega>\<in>space (F t). S \<omega> \<le> t} \<in> sets (F t)"
+ using stopping_timeD[OF S] by (auto simp: pred_def)
+ also have "{\<omega>\<in>A. T \<omega> \<le> t} \<inter> {\<omega>\<in>space (F t). S \<omega> \<le> t} = {\<omega>\<in>A. S \<omega> \<le> t}"
+ using \<open>A \<subseteq> \<Omega>\<close> sets_into_space[of A] le by (auto simp: space_F intro: order_trans)
+ finally show "{\<omega>\<in>A. S \<omega> \<le> t} \<in> sets (F t)"
+ by auto
+qed
+
+lemma stopping_time_less_const:
+ assumes T: "stopping_time F T" shows "Measurable.pred (F t) (\<lambda>\<omega>. T \<omega> < t)"
+proof -
+ guess D :: "'t set" by (rule countable_dense_setE)
+ note D = this
+ show ?thesis
+ proof cases
+ assume *: "\<forall>t'<t. \<exists>t''. t' < t'' \<and> t'' < t"
+ { fix t' assume "t' < t"
+ with * have "{t' <..< t} \<noteq> {}"
+ by fastforce
+ with D(2)[OF _ this]
+ have "\<exists>d\<in>D. t'< d \<and> d < t"
+ by auto }
+ note ** = this
+
+ show ?thesis
+ proof (rule measurable_cong[THEN iffD2])
+ show "T \<omega> < t \<longleftrightarrow> (\<exists>r\<in>{r\<in>D. r < t}. T \<omega> \<le> r)" for \<omega>
+ by (auto dest: ** intro: less_imp_le)
+ show "Measurable.pred (F t) (\<lambda>w. \<exists>r\<in>{r \<in> D. r < t}. T w \<le> r)"
+ by (intro measurable_pred_countable stopping_time_le_const[OF T] countable_Collect D) auto
+ qed
+ next
+ assume "\<not> (\<forall>t'<t. \<exists>t''. t' < t'' \<and> t'' < t)"
+ then obtain t' where t': "t' < t" "\<And>t''. t'' < t \<Longrightarrow> t'' \<le> t'"
+ by (auto simp: not_less[symmetric])
+ show ?thesis
+ proof (rule measurable_cong[THEN iffD2])
+ show "T \<omega> < t \<longleftrightarrow> T \<omega> \<le> t'" for \<omega>
+ using t' by auto
+ show "Measurable.pred (F t) (\<lambda>w. T w \<le> t')"
+ using \<open>t'<t\<close> by (intro stopping_time_le_const[OF T]) auto
+ qed
+ qed
+qed
+
+lemma stopping_time_eq_const: "stopping_time F T \<Longrightarrow> Measurable.pred (F t) (\<lambda>\<omega>. T \<omega> = t)"
+ unfolding eq_iff using stopping_time_less_const[of T t]
+ by (intro pred_intros_logic stopping_time_le_const) (auto simp: not_less[symmetric] )
+
+lemma stopping_time_less:
+ assumes T: "stopping_time F T" and S: "stopping_time F S"
+ shows "Measurable.pred (pre_sigma T) (\<lambda>\<omega>. T \<omega> < S \<omega>)"
+proof (rule pred_pre_sigmaI[OF T])
+ fix t
+ obtain D :: "'t set"
+ where [simp]: "countable D" and semidense_D: "\<And>x y. x < y \<Longrightarrow> (\<exists>b\<in>D. x \<le> b \<and> b < y)"
+ using countable_separating_set_linorder2 by auto
+ show "Measurable.pred (F t) (\<lambda>\<omega>. T \<omega> < S \<omega> \<and> T \<omega> \<le> t)"
+ proof (rule measurable_cong[THEN iffD2])
+ let ?f = "\<lambda>\<omega>. if T \<omega> = t then \<not> S \<omega> \<le> t else \<exists>s\<in>{s\<in>D. s \<le> t}. T \<omega> \<le> s \<and> \<not> (S \<omega> \<le> s)"
+ { fix \<omega> assume "T \<omega> \<le> t" "T \<omega> \<noteq> t" "T \<omega> < S \<omega>"
+ then have "T \<omega> < min t (S \<omega>)"
+ by auto
+ then obtain r where "r \<in> D" "T \<omega> \<le> r" "r < min t (S \<omega>)"
+ by (metis semidense_D)
+ then have "\<exists>s\<in>{s\<in>D. s \<le> t}. T \<omega> \<le> s \<and> s < S \<omega>"
+ by auto }
+ then show "(T \<omega> < S \<omega> \<and> T \<omega> \<le> t) = ?f \<omega>" for \<omega>
+ by (auto simp: not_le)
+ show "Measurable.pred (F t) ?f"
+ by (intro pred_intros_logic measurable_If measurable_pred_countable countable_Collect
+ stopping_time_le_const predE stopping_time_eq_const T S)
+ auto
+ qed
+qed
+
+end
+
+lemma stopping_time_SUP_enat:
+ fixes T :: "nat \<Rightarrow> ('a \<Rightarrow> enat)"
+ shows "(\<And>i. stopping_time F (T i)) \<Longrightarrow> stopping_time F (SUP i. T i)"
+ unfolding stopping_time_def SUP_apply SUP_le_iff by (auto intro!: pred_intros_countable)
+
+lemma less_eSuc_iff: "a < eSuc b \<longleftrightarrow> (a \<le> b \<and> a \<noteq> \<infinity>)"
+ by (cases a) auto
+
+lemma stopping_time_Inf_enat:
+ fixes F :: "enat \<Rightarrow> 'a measure"
+ assumes F: "filtration \<Omega> F"
+ assumes P: "\<And>i. Measurable.pred (F i) (P i)"
+ shows "stopping_time F (\<lambda>\<omega>. Inf {i. P i \<omega>})"
+proof (rule stopping_timeI, cases)
+ fix t :: enat assume "t = \<infinity>" then show "Measurable.pred (F t) (\<lambda>\<omega>. Inf {i. P i \<omega>} \<le> t)"
+ by auto
+next
+ fix t :: enat assume "t \<noteq> \<infinity>"
+ moreover
+ { fix i \<omega> assume "Inf {i. P i \<omega>} \<le> t"
+ with \<open>t \<noteq> \<infinity>\<close> have "(\<exists>i\<le>t. P i \<omega>)"
+ unfolding Inf_le_iff by (cases t) (auto elim!: allE[of _ "eSuc t"] simp: less_eSuc_iff) }
+ ultimately have *: "\<And>\<omega>. Inf {i. P i \<omega>} \<le> t \<longleftrightarrow> (\<exists>i\<in>{..t}. P i \<omega>)"
+ by (auto intro!: Inf_lower2)
+ show "Measurable.pred (F t) (\<lambda>\<omega>. Inf {i. P i \<omega>} \<le> t)"
+ unfolding * using filtration.sets_F_mono[OF F, of _ t] P
+ by (intro pred_intros_countable_bounded) (auto simp: pred_def filtration.space_F[OF F])
+qed
+
+lemma stopping_time_Inf_nat:
+ fixes F :: "nat \<Rightarrow> 'a measure"
+ assumes F: "filtration \<Omega> F"
+ assumes P: "\<And>i. Measurable.pred (F i) (P i)" and wf: "\<And>i \<omega>. \<omega> \<in> \<Omega> \<Longrightarrow> \<exists>n. P n \<omega>"
+ shows "stopping_time F (\<lambda>\<omega>. Inf {i. P i \<omega>})"
+ unfolding stopping_time_def
+proof (intro allI, subst measurable_cong)
+ fix t \<omega> assume "\<omega> \<in> space (F t)"
+ then have "\<omega> \<in> \<Omega>"
+ using filtration.space_F[OF F] by auto
+ from wf[OF this] have "((LEAST n. P n \<omega>) \<le> t) = (\<exists>i\<le>t. P i \<omega>)"
+ by (rule LeastI2_wellorder_ex) auto
+ then show "(Inf {i. P i \<omega>} \<le> t) = (\<exists>i\<in>{..t}. P i \<omega>)"
+ by (simp add: Inf_nat_def Bex_def)
+next
+ fix t from P show "Measurable.pred (F t) (\<lambda>w. \<exists>i\<in>{..t}. P i w)"
+ using filtration.sets_F_mono[OF F, of _ t]
+ by (intro pred_intros_countable_bounded) (auto simp: pred_def filtration.space_F[OF F])
+qed
+
+end
--- a/src/HOL/Probability/Stream_Space.thy Thu Oct 20 23:42:12 2016 +0200
+++ b/src/HOL/Probability/Stream_Space.thy Thu Oct 20 23:42:41 2016 +0200
@@ -446,6 +446,17 @@
by (cases "xs = []") (auto simp: * space_stream_space del: in_listsD)
qed (auto simp: * ae sets_M del: in_listsD intro!: streams_sets)
+lemma sets_sstart[measurable]: "sstart \<Omega> xs \<in> sets (stream_space (count_space UNIV))"
+proof (induction xs)
+ case (Cons x xs)
+ note this[measurable]
+ have "sstart \<Omega> (x # xs) = {\<omega>\<in>space (stream_space (count_space UNIV)). \<omega> \<in> sstart \<Omega> (x # xs)}"
+ by (auto simp: space_stream_space)
+ also have "\<dots> \<in> sets (stream_space (count_space UNIV))"
+ unfolding in_sstart by measurable
+ finally show ?case .
+qed (auto intro!: streams_sets)
+
primrec scylinder :: "'a set \<Rightarrow> 'a set list \<Rightarrow> 'a stream set"
where
"scylinder S [] = streams S"
--- a/src/HOL/ROOT Thu Oct 20 23:42:12 2016 +0200
+++ b/src/HOL/ROOT Thu Oct 20 23:42:41 2016 +0200
@@ -181,7 +181,7 @@
theories [document = false]
"Less_False"
"~~/src/HOL/Library/Multiset"
- "~~/src/HOL/Library/Float"
+ "~~/src/HOL/Number_Theory/Fib"
theories
Balance
Tree_Map