--- a/src/Doc/Sledgehammer/document/root.tex Wed Sep 30 17:09:12 2015 +0100
+++ b/src/Doc/Sledgehammer/document/root.tex Wed Sep 30 17:17:53 2015 +0100
@@ -278,7 +278,7 @@
provers might be missing or present with a \textit{remote\_} prefix.
For each successful prover, Sledgehammer gives a one-line \textit{metis} or
-\textit{smt2} method call. Rough timings are shown in parentheses, indicating how
+\textit{smt} method call. Rough timings are shown in parentheses, indicating how
fast the call is. You can click the proof to insert it into the theory text.
In addition, you can ask Sledgehammer for an Isar text proof by enabling the
@@ -289,7 +289,7 @@
\postw
When Isar proof construction is successful, it can yield proofs that are more
-readable and also faster than the \textit{metis} or \textit{smt2} one-line
+readable and also faster than the \textit{metis} or \textit{smt} one-line
proofs. This feature is experimental and is only available for ATPs.
\section{Hints}
@@ -341,7 +341,7 @@
\item[\labelitemi] \textbf{\textit{isar\_proofs}} (\S\ref{output-format}) specifies
that Isar proofs should be generated, in addition to one-line \textit{metis} or
-\textit{smt2} proofs. The length of the Isar proofs can be controlled by setting
+\textit{smt} proofs. The length of the Isar proofs can be controlled by setting
\textit{compress} (\S\ref{output-format}).
\item[\labelitemi] \textbf{\textit{timeout}} (\S\ref{timeouts}) controls the
@@ -1277,9 +1277,9 @@
The collection of methods is roughly the same as for the \textbf{try0} command.
\opsmart{smt\_proofs}{no\_smt\_proofs}
-Specifies whether the \textit{smt2} proof method should be tried in addition to
+Specifies whether the \textit{smt} proof method should be tried in addition to
Isabelle's other proof methods. If the option is set to \textit{smart} (the
-default), the \textit{smt2} method is used for one-line proofs but not in Isar
+default), the \textit{smt} method is used for one-line proofs but not in Isar
proofs.
\end{enum}
--- a/src/HOL/Code_Numeral.thy Wed Sep 30 17:09:12 2015 +0100
+++ b/src/HOL/Code_Numeral.thy Wed Sep 30 17:17:53 2015 +0100
@@ -147,6 +147,25 @@
"int_of_integer (Num.sub k l) = Num.sub k l"
by transfer rule
+lift_definition integer_of_num :: "num \<Rightarrow> integer"
+ is "numeral :: num \<Rightarrow> int"
+ .
+
+lemma integer_of_num [code]:
+ "integer_of_num num.One = 1"
+ "integer_of_num (num.Bit0 n) = (let k = integer_of_num n in k + k)"
+ "integer_of_num (num.Bit1 n) = (let k = integer_of_num n in k + k + 1)"
+ by (transfer, simp only: numeral.simps Let_def)+
+
+lemma numeral_unfold_integer_of_num:
+ "numeral = integer_of_num"
+ by (simp add: integer_of_num_def map_fun_def fun_eq_iff)
+
+lemma integer_of_num_triv:
+ "integer_of_num Num.One = 1"
+ "integer_of_num (Num.Bit0 Num.One) = 2"
+ by (transfer, simp)+
+
instantiation integer :: "{ring_div, equal, linordered_idom}"
begin
@@ -215,18 +234,43 @@
"of_nat (nat_of_integer k) = max 0 k"
by transfer auto
-instance integer :: semiring_numeral_div
- by intro_classes (transfer,
- fact le_add_diff_inverse2
- semiring_numeral_div_class.div_less
- semiring_numeral_div_class.mod_less
- semiring_numeral_div_class.div_positive
- semiring_numeral_div_class.mod_less_eq_dividend
- semiring_numeral_div_class.pos_mod_bound
- semiring_numeral_div_class.pos_mod_sign
- semiring_numeral_div_class.mod_mult2_eq
- semiring_numeral_div_class.div_mult2_eq
- semiring_numeral_div_class.discrete)+
+instantiation integer :: semiring_numeral_div
+begin
+
+definition divmod_integer :: "num \<Rightarrow> num \<Rightarrow> integer \<times> integer"
+where
+ divmod_integer'_def: "divmod_integer m n = (numeral m div numeral n, numeral m mod numeral n)"
+
+definition divmod_step_integer :: "num \<Rightarrow> integer \<times> integer \<Rightarrow> integer \<times> integer"
+where
+ "divmod_step_integer l qr = (let (q, r) = qr
+ in if r \<ge> numeral l then (2 * q + 1, r - numeral l)
+ else (2 * q, r))"
+
+instance proof
+ show "divmod m n = (numeral m div numeral n :: integer, numeral m mod numeral n)"
+ for m n by (fact divmod_integer'_def)
+ show "divmod_step l qr = (let (q, r) = qr
+ in if r \<ge> numeral l then (2 * q + 1, r - numeral l)
+ else (2 * q, r))" for l and qr :: "integer \<times> integer"
+ by (fact divmod_step_integer_def)
+qed (transfer,
+ fact le_add_diff_inverse2
+ semiring_numeral_div_class.div_less
+ semiring_numeral_div_class.mod_less
+ semiring_numeral_div_class.div_positive
+ semiring_numeral_div_class.mod_less_eq_dividend
+ semiring_numeral_div_class.pos_mod_bound
+ semiring_numeral_div_class.pos_mod_sign
+ semiring_numeral_div_class.mod_mult2_eq
+ semiring_numeral_div_class.div_mult2_eq
+ semiring_numeral_div_class.discrete)+
+
+end
+
+declare divmod_algorithm_code [where ?'a = integer,
+ unfolded numeral_unfold_integer_of_num, unfolded integer_of_num_triv,
+ code]
lemma integer_of_nat_0: "integer_of_nat 0 = 0"
by transfer simp
@@ -244,12 +288,18 @@
definition Pos :: "num \<Rightarrow> integer"
where
- [simp, code_abbrev]: "Pos = numeral"
+ [simp, code_post]: "Pos = numeral"
lemma [transfer_rule]:
"rel_fun HOL.eq pcr_integer numeral Pos"
by simp transfer_prover
+lemma Pos_fold [code_unfold]:
+ "numeral Num.One = Pos Num.One"
+ "numeral (Num.Bit0 k) = Pos (Num.Bit0 k)"
+ "numeral (Num.Bit1 k) = Pos (Num.Bit1 k)"
+ by simp_all
+
definition Neg :: "num \<Rightarrow> integer"
where
[simp, code_abbrev]: "Neg n = - Pos n"
@@ -434,16 +484,6 @@
"Neg k < Neg l \<longleftrightarrow> l < k"
by simp_all
-lift_definition integer_of_num :: "num \<Rightarrow> integer"
- is "numeral :: num \<Rightarrow> int"
- .
-
-lemma integer_of_num [code]:
- "integer_of_num num.One = 1"
- "integer_of_num (num.Bit0 n) = (let k = integer_of_num n in k + k)"
- "integer_of_num (num.Bit1 n) = (let k = integer_of_num n in k + k + 1)"
- by (transfer, simp only: numeral.simps Let_def)+
-
lift_definition num_of_integer :: "integer \<Rightarrow> num"
is "num_of_nat \<circ> nat"
.
--- a/src/HOL/Divides.thy Wed Sep 30 17:09:12 2015 +0100
+++ b/src/HOL/Divides.thy Wed Sep 30 17:17:53 2015 +0100
@@ -567,6 +567,16 @@
and mod_mult2_eq: "0 \<le> c \<Longrightarrow> a mod (b * c) = b * (a div b mod c) + a mod b"
and div_mult2_eq: "0 \<le> c \<Longrightarrow> a div (b * c) = a div b div c"
assumes discrete: "a < b \<longleftrightarrow> a + 1 \<le> b"
+ fixes divmod :: "num \<Rightarrow> num \<Rightarrow> 'a \<times> 'a"
+ and divmod_step :: "num \<Rightarrow> 'a \<times> 'a \<Rightarrow> 'a \<times> 'a"
+ assumes divmod_def: "divmod m n = (numeral m div numeral n, numeral m mod numeral n)"
+ and divmod_step_def: "divmod_step l qr = (let (q, r) = qr
+ in if r \<ge> numeral l then (2 * q + 1, r - numeral l)
+ else (2 * q, r))"
+ -- \<open>These are conceptually definitions but force generated code
+ to be monomorphic wrt. particular instances of this class which
+ yields a significant speedup.\<close>
+
begin
lemma mult_div_cancel:
@@ -650,10 +660,6 @@
by (simp_all add: div mod)
qed
-definition divmod :: "num \<Rightarrow> num \<Rightarrow> 'a \<times> 'a"
-where
- "divmod m n = (numeral m div numeral n, numeral m mod numeral n)"
-
lemma fst_divmod:
"fst (divmod m n) = numeral m div numeral n"
by (simp add: divmod_def)
@@ -662,12 +668,6 @@
"snd (divmod m n) = numeral m mod numeral n"
by (simp add: divmod_def)
-definition divmod_step :: "num \<Rightarrow> 'a \<times> 'a \<Rightarrow> 'a \<times> 'a"
-where
- "divmod_step l qr = (let (q, r) = qr
- in if r \<ge> numeral l then (2 * q + 1, r - numeral l)
- else (2 * q, r))"
-
text \<open>
This is a formulation of one step (referring to one digit position)
in school-method division: compare the dividend at the current
@@ -675,7 +675,7 @@
and evaluate accordingly.
\<close>
-lemma divmod_step_eq [code, simp]:
+lemma divmod_step_eq [simp]:
"divmod_step l (q, r) = (if numeral l \<le> r
then (2 * q + 1, r - numeral l) else (2 * q, r))"
by (simp add: divmod_step_def)
@@ -735,7 +735,7 @@
text \<open>The division rewrite proper -- first, trivial results involving @{text 1}\<close>
-lemma divmod_trivial [simp, code]:
+lemma divmod_trivial [simp]:
"divmod Num.One Num.One = (numeral Num.One, 0)"
"divmod (Num.Bit0 m) Num.One = (numeral (Num.Bit0 m), 0)"
"divmod (Num.Bit1 m) Num.One = (numeral (Num.Bit1 m), 0)"
@@ -745,7 +745,7 @@
text \<open>Division by an even number is a right-shift\<close>
-lemma divmod_cancel [simp, code]:
+lemma divmod_cancel [simp]:
"divmod (Num.Bit0 m) (Num.Bit0 n) = (case divmod m n of (q, r) \<Rightarrow> (q, 2 * r))" (is ?P)
"divmod (Num.Bit1 m) (Num.Bit0 n) = (case divmod m n of (q, r) \<Rightarrow> (q, 2 * r + 1))" (is ?Q)
proof -
@@ -761,7 +761,7 @@
text \<open>The really hard work\<close>
-lemma divmod_steps [simp, code]:
+lemma divmod_steps [simp]:
"divmod (num.Bit0 m) (num.Bit1 n) =
(if m \<le> n then (0, numeral (num.Bit0 m))
else divmod_step (num.Bit1 n)
@@ -774,6 +774,8 @@
(num.Bit0 (num.Bit1 n))))"
by (simp_all add: divmod_divmod_step)
+lemmas divmod_algorithm_code = divmod_step_eq divmod_trivial divmod_cancel divmod_steps
+
text \<open>Special case: divisibility\<close>
definition divides_aux :: "'a \<times> 'a \<Rightarrow> bool"
@@ -1177,9 +1179,26 @@
lemma mod_mult2_eq: "a mod (b * c) = b * (a div b mod c) + a mod (b::nat)"
by (auto simp add: mult.commute divmod_nat_rel [THEN divmod_nat_rel_mult2_eq, THEN mod_nat_unique])
-instance nat :: semiring_numeral_div
- by intro_classes (auto intro: div_positive simp add: mult_div_cancel mod_mult2_eq div_mult2_eq)
-
+instantiation nat :: semiring_numeral_div
+begin
+
+definition divmod_nat :: "num \<Rightarrow> num \<Rightarrow> nat \<times> nat"
+where
+ divmod'_nat_def: "divmod_nat m n = (numeral m div numeral n, numeral m mod numeral n)"
+
+definition divmod_step_nat :: "num \<Rightarrow> nat \<times> nat \<Rightarrow> nat \<times> nat"
+where
+ "divmod_step_nat l qr = (let (q, r) = qr
+ in if r \<ge> numeral l then (2 * q + 1, r - numeral l)
+ else (2 * q, r))"
+
+instance
+ by standard (auto intro: div_positive simp add: divmod'_nat_def divmod_step_nat_def mod_mult2_eq div_mult2_eq)
+
+end
+
+declare divmod_algorithm_code [where ?'a = nat, code]
+
subsubsection \<open>Further Facts about Quotient and Remainder\<close>
@@ -2304,12 +2323,26 @@
subsubsection \<open>Computation of Division and Remainder\<close>
-instance int :: semiring_numeral_div
- by intro_classes (auto intro: zmod_le_nonneg_dividend
- simp add:
- zmult_div_cancel
- pos_imp_zdiv_pos_iff div_pos_pos_trivial mod_pos_pos_trivial
- zmod_zmult2_eq zdiv_zmult2_eq)
+instantiation int :: semiring_numeral_div
+begin
+
+definition divmod_int :: "num \<Rightarrow> num \<Rightarrow> int \<times> int"
+where
+ "divmod_int m n = (numeral m div numeral n, numeral m mod numeral n)"
+
+definition divmod_step_int :: "num \<Rightarrow> int \<times> int \<Rightarrow> int \<times> int"
+where
+ "divmod_step_int l qr = (let (q, r) = qr
+ in if r \<ge> numeral l then (2 * q + 1, r - numeral l)
+ else (2 * q, r))"
+
+instance
+ by standard (auto intro: zmod_le_nonneg_dividend simp add: divmod_int_def divmod_step_int_def
+ pos_imp_zdiv_pos_iff div_pos_pos_trivial mod_pos_pos_trivial zmod_zmult2_eq zdiv_zmult2_eq)
+
+end
+
+declare divmod_algorithm_code [where ?'a = int, code]
context
begin
--- a/src/HOL/Library/Code_Target_Int.thy Wed Sep 30 17:09:12 2015 +0100
+++ b/src/HOL/Library/Code_Target_Int.thy Wed Sep 30 17:17:53 2015 +0100
@@ -79,6 +79,11 @@
by simp
lemma [code]:
+ "divmod m n = map_prod int_of_integer int_of_integer (divmod m n)"
+ unfolding prod_eq_iff divmod_def map_prod_def case_prod_beta fst_conv snd_conv
+ by transfer simp
+
+lemma [code]:
"HOL.equal k l = HOL.equal (of_int k :: integer) (of_int l)"
by transfer (simp add: equal)
--- a/src/HOL/Library/Code_Target_Nat.thy Wed Sep 30 17:09:12 2015 +0100
+++ b/src/HOL/Library/Code_Target_Nat.thy Wed Sep 30 17:17:53 2015 +0100
@@ -85,6 +85,12 @@
by (fact divmod_nat_div_mod)
lemma [code]:
+ "divmod m n = map_prod nat_of_integer nat_of_integer (divmod m n)"
+ by (simp only: prod_eq_iff divmod_def map_prod_def case_prod_beta fst_conv snd_conv)
+ (transfer, simp_all only: nat_div_distrib nat_mod_distrib
+ zero_le_numeral nat_numeral)
+
+lemma [code]:
"HOL.equal m n = HOL.equal (of_nat m :: integer) (of_nat n)"
by transfer (simp add: equal)
--- a/src/HOL/MacLaurin.thy Wed Sep 30 17:09:12 2015 +0100
+++ b/src/HOL/MacLaurin.thy Wed Sep 30 17:17:53 2015 +0100
@@ -430,16 +430,16 @@
apply (cut_tac f = sin and n = n and x = x
and diff = "%n x. sin (x + 1/2*real n * pi)" in Maclaurin_all_lt_objl)
apply safe
-apply (simp (no_asm))
-apply (simp (no_asm) add: sin_expansion_lemma)
-apply (force intro!: derivative_eq_intros)
-apply (subst (asm) setsum.neutral, auto)[1]
-apply (rule ccontr, simp)
-apply (drule_tac x = x in spec, simp)
+ apply (simp)
+ apply (simp add: sin_expansion_lemma del: real_of_nat_Suc)
+ apply (force intro!: derivative_eq_intros)
+ apply (subst (asm) setsum.neutral, auto)[1]
+ apply (rule ccontr, simp)
+ apply (drule_tac x = x in spec, simp)
apply (erule ssubst)
apply (rule_tac x = t in exI, simp)
apply (rule setsum.cong[OF refl])
-apply (auto simp add: sin_coeff_def sin_zero_iff elim: oddE)
+apply (auto simp add: sin_coeff_def sin_zero_iff elim: oddE simp del: real_of_nat_Suc)
done
lemma Maclaurin_sin_expansion:
@@ -458,13 +458,13 @@
+ ((sin(t + 1/2 * real(n) *pi) / (fact n)) * x ^ n)"
apply (cut_tac f = sin and n = n and h = x and diff = "%n x. sin (x + 1/2*real (n) *pi)" in Maclaurin_objl)
apply safe
-apply simp
-apply (simp (no_asm) add: sin_expansion_lemma)
-apply (force intro!: derivative_eq_intros)
-apply (erule ssubst)
-apply (rule_tac x = t in exI, simp)
-apply (rule setsum.cong[OF refl])
-apply (auto simp add: sin_coeff_def sin_zero_iff elim: oddE)
+ apply simp
+ apply (simp (no_asm) add: sin_expansion_lemma del: real_of_nat_Suc)
+ apply (force intro!: derivative_eq_intros)
+ apply (erule ssubst)
+ apply (rule_tac x = t in exI, simp)
+ apply (rule setsum.cong[OF refl])
+ apply (auto simp add: sin_coeff_def sin_zero_iff elim: oddE simp del: real_of_nat_Suc)
done
lemma Maclaurin_sin_expansion4:
@@ -475,13 +475,13 @@
+ ((sin(t + 1/2 * real (n) *pi) / (fact n)) * x ^ n)"
apply (cut_tac f = sin and n = n and h = x and diff = "%n x. sin (x + 1/2*real (n) *pi)" in Maclaurin2_objl)
apply safe
-apply simp
-apply (simp (no_asm) add: sin_expansion_lemma)
-apply (force intro!: derivative_eq_intros)
-apply (erule ssubst)
-apply (rule_tac x = t in exI, simp)
-apply (rule setsum.cong[OF refl])
-apply (auto simp add: sin_coeff_def sin_zero_iff elim: oddE)
+ apply simp
+ apply (simp (no_asm) add: sin_expansion_lemma del: real_of_nat_Suc)
+ apply (force intro!: derivative_eq_intros)
+ apply (erule ssubst)
+ apply (rule_tac x = t in exI, simp)
+ apply (rule setsum.cong[OF refl])
+ apply (auto simp add: sin_coeff_def sin_zero_iff elim: oddE simp del: real_of_nat_Suc)
done
@@ -502,10 +502,10 @@
+ ((cos(t + 1/2 * real (n) *pi) / (fact n)) * x ^ n)"
apply (cut_tac f = cos and n = n and x = x and diff = "%n x. cos (x + 1/2*real (n) *pi)" in Maclaurin_all_lt_objl)
apply safe
-apply (simp (no_asm))
-apply (simp (no_asm) add: cos_expansion_lemma)
-apply (case_tac "n", simp)
-apply (simp del: setsum_lessThan_Suc)
+ apply (simp (no_asm))
+ apply (simp (no_asm) add: cos_expansion_lemma del: real_of_nat_Suc)
+ apply (case_tac "n", simp)
+ apply (simp del: setsum_lessThan_Suc)
apply (rule ccontr, simp)
apply (drule_tac x = x in spec, simp)
apply (erule ssubst)
@@ -522,10 +522,10 @@
+ ((cos(t + 1/2 * real (n) *pi) / (fact n)) * x ^ n)"
apply (cut_tac f = cos and n = n and h = x and diff = "%n x. cos (x + 1/2*real (n) *pi)" in Maclaurin_objl)
apply safe
-apply simp
-apply (simp (no_asm) add: cos_expansion_lemma)
-apply (erule ssubst)
-apply (rule_tac x = t in exI, simp)
+ apply simp
+ apply (simp (no_asm) add: cos_expansion_lemma del: real_of_nat_Suc)
+ apply (erule ssubst)
+ apply (rule_tac x = t in exI, simp)
apply (rule setsum.cong[OF refl])
apply (auto simp add: cos_coeff_def cos_zero_iff elim: evenE)
done
@@ -538,8 +538,8 @@
+ ((cos(t + 1/2 * real (n) *pi) / (fact n)) * x ^ n)"
apply (cut_tac f = cos and n = n and h = x and diff = "%n x. cos (x + 1/2*real (n) *pi)" in Maclaurin_minus_objl)
apply safe
-apply simp
-apply (simp (no_asm) add: cos_expansion_lemma)
+ apply simp
+ apply (simp (no_asm) add: cos_expansion_lemma del: real_of_nat_Suc)
apply (erule ssubst)
apply (rule_tac x = t in exI, simp)
apply (rule setsum.cong[OF refl])
--- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Wed Sep 30 17:09:12 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Wed Sep 30 17:17:53 2015 +0100
@@ -1742,7 +1742,7 @@
have "(\<Sum>i\<in>Basis. \<bar>real (r (b' i)) - real (q (b' i))\<bar>) \<le> (\<Sum>(i::'a)\<in>Basis. 1)"
apply (rule setsum_mono)
using rs(1)[OF b'_im]
- apply (auto simp add:* field_simps)
+ apply (auto simp add:* field_simps simp del: real_of_nat_Suc)
done
also have "\<dots> < e * real p"
using p \<open>e > 0\<close> \<open>p > 0\<close>
@@ -1754,7 +1754,7 @@
have "(\<Sum>i\<in>Basis. \<bar>real (s (b' i)) - real (q (b' i))\<bar>) \<le> (\<Sum>(i::'a)\<in>Basis. 1)"
apply (rule setsum_mono)
using rs(2)[OF b'_im]
- apply (auto simp add:* field_simps)
+ apply (auto simp add:* field_simps simp del: real_of_nat_Suc)
done
also have "\<dots> < e * real p"
using p \<open>e > 0\<close> \<open>p > 0\<close>
--- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy Wed Sep 30 17:09:12 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy Wed Sep 30 17:17:53 2015 +0100
@@ -3030,7 +3030,7 @@
path_integral (linepath (h (n/N)) (g (n/N))) f = 0"
using path_integral_unique [OF pi0] Suc.prems
by (simp add: g h fpa valid_path_subpath path_integrable_subpath
- fpa1 fpa2 fpa3 algebra_simps)
+ fpa1 fpa2 fpa3 algebra_simps del: real_of_nat_Suc)
have *: "\<And>hn he hn' gn gd gn' hgn ghn gh0 ghn'.
\<lbrakk>hn - gn = ghn - gh0;
gd + ghn' + he + hgn = (0::complex);
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Wed Sep 30 17:09:12 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Wed Sep 30 17:17:53 2015 +0100
@@ -560,7 +560,7 @@
lemma real_arch_inv: "0 < e \<longleftrightarrow> (\<exists>n::nat. n \<noteq> 0 \<and> 0 < inverse (real n) \<and> inverse (real n) < e)"
using reals_Archimedean[of e] less_trans[of 0 "1 / real n" e for n::nat]
- by (auto simp add: field_simps cong: conj_cong)
+ by (auto simp add: field_simps cong: conj_cong simp del: real_of_nat_Suc)
text\<open>Bernoulli's inequality\<close>
lemma Bernoulli_inequality:
@@ -654,9 +654,7 @@
(\<And>n. P (inverse (real (Suc n)))) \<Longrightarrow> 0 < e \<Longrightarrow> P e"
apply (rule forall_pos_mono)
apply auto
- apply (atomize)
- apply (erule_tac x="n - 1" in allE)
- apply auto
+ apply (metis Suc_pred real_of_nat_Suc)
done
lemma real_archimedian_rdiv_eq_0:
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Wed Sep 30 17:09:12 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Wed Sep 30 17:17:53 2015 +0100
@@ -6597,8 +6597,7 @@
then have "\<exists>N::nat. inverse (real (N + 1)) < e"
using real_arch_inv[of e]
apply (auto simp add: Suc_pred')
- apply (rule_tac x="n - 1" in exI)
- apply auto
+ apply (metis Suc_pred' real_of_nat_Suc)
done
then obtain N :: nat where "inverse (real (N + 1)) < e"
by auto
--- a/src/HOL/Multivariate_Analysis/Weierstrass.thy Wed Sep 30 17:09:12 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Weierstrass.thy Wed Sep 30 17:17:53 2015 +0100
@@ -664,9 +664,9 @@
apply simp
done
also have "... \<le> j*e + e*(n - j + 1)*e/n "
- using \<open>1 \<le> n\<close> e by (simp add: field_simps)
+ using \<open>1 \<le> n\<close> e by (simp add: field_simps del: real_of_nat_Suc)
also have "... \<le> j*e + e*e"
- using \<open>1 \<le> n\<close> e j1 by (simp add: field_simps)
+ using \<open>1 \<le> n\<close> e j1 by (simp add: field_simps del: real_of_nat_Suc)
also have "... < (j + 1/3)*e"
using e by (auto simp: field_simps)
finally have gj1: "g t < (j + 1 / 3) * e" .
--- a/src/HOL/NSA/HSEQ.thy Wed Sep 30 17:09:12 2015 +0100
+++ b/src/HOL/NSA/HSEQ.thy Wed Sep 30 17:17:53 2015 +0100
@@ -225,11 +225,11 @@
by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_zero)
lemma NSLIMSEQ_inverse_real_of_nat: "(%n. inverse(real(Suc n))) ----NS> 0"
-by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_real_of_nat)
+by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_real_of_nat del: real_of_nat_Suc)
lemma NSLIMSEQ_inverse_real_of_nat_add:
"(%n. r + inverse(real(Suc n))) ----NS> r"
-by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_real_of_nat_add)
+by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_real_of_nat_add del: real_of_nat_Suc)
lemma NSLIMSEQ_inverse_real_of_nat_add_minus:
"(%n. r + -inverse(real(Suc n))) ----NS> r"
--- a/src/HOL/NSA/HyperDef.thy Wed Sep 30 17:09:12 2015 +0100
+++ b/src/HOL/NSA/HyperDef.thy Wed Sep 30 17:17:53 2015 +0100
@@ -266,7 +266,7 @@
lemma not_ex_hypreal_of_real_eq_epsilon: "~ (\<exists>x. hypreal_of_real x = epsilon)"
by (auto simp add: epsilon_def star_of_def star_n_eq_iff
- lemma_finite_epsilon_set [THEN FreeUltrafilterNat.finite])
+ lemma_finite_epsilon_set [THEN FreeUltrafilterNat.finite] simp del: real_of_nat_Suc)
lemma hypreal_of_real_not_eq_epsilon: "hypreal_of_real x \<noteq> epsilon"
by (insert not_ex_hypreal_of_real_eq_epsilon, auto)
--- a/src/HOL/NSA/NSA.thy Wed Sep 30 17:09:12 2015 +0100
+++ b/src/HOL/NSA/NSA.thy Wed Sep 30 17:17:53 2015 +0100
@@ -2025,7 +2025,7 @@
lemma lemma_Infinitesimal:
"(\<forall>r. 0 < r --> x < r) = (\<forall>n. x < inverse(real (Suc n)))"
-apply (auto simp add: real_of_nat_Suc_gt_zero)
+apply (auto simp add: real_of_nat_Suc_gt_zero simp del: real_of_nat_Suc)
apply (blast dest!: reals_Archimedean intro: order_less_trans)
done
@@ -2033,12 +2033,12 @@
"(\<forall>r \<in> Reals. 0 < r --> x < r) =
(\<forall>n. x < inverse(hypreal_of_nat (Suc n)))"
apply safe
-apply (drule_tac x = "inverse (hypreal_of_real (real (Suc n))) " in bspec)
-apply (simp (no_asm_use))
-apply (rule real_of_nat_Suc_gt_zero [THEN positive_imp_inverse_positive, THEN star_of_less [THEN iffD2], THEN [2] impE])
-prefer 2 apply assumption
-apply (simp add: real_of_nat_def)
-apply (auto dest!: reals_Archimedean simp add: SReal_iff)
+ apply (drule_tac x = "inverse (hypreal_of_real (real (Suc n))) " in bspec)
+ apply (simp (no_asm_use))
+ apply (rule real_of_nat_Suc_gt_zero [THEN positive_imp_inverse_positive, THEN star_of_less [THEN iffD2], THEN [2] impE])
+ prefer 2 apply assumption
+ apply (simp add: real_of_nat_def)
+apply (auto dest!: reals_Archimedean simp add: SReal_iff simp del: real_of_nat_Suc)
apply (drule star_of_less [THEN iffD2])
apply (simp add: real_of_nat_def)
apply (blast intro: order_less_trans)
@@ -2148,7 +2148,7 @@
lemma finite_inverse_real_of_posnat_gt_real:
"0 < u ==> finite {n. u < inverse(real(Suc n))}"
-apply (simp (no_asm_simp) add: real_of_nat_less_inverse_iff)
+apply (simp (no_asm_simp) add: real_of_nat_less_inverse_iff del: real_of_nat_Suc)
apply (simp (no_asm_simp) add: real_of_nat_Suc less_diff_eq [symmetric])
apply (rule finite_real_of_nat_less_real)
done
@@ -2161,7 +2161,8 @@
lemma finite_inverse_real_of_posnat_ge_real:
"0 < u ==> finite {n. u \<le> inverse(real(Suc n))}"
-by (auto simp add: lemma_real_le_Un_eq2 lemma_finite_epsilon_set finite_inverse_real_of_posnat_gt_real)
+by (auto simp add: lemma_real_le_Un_eq2 lemma_finite_epsilon_set finite_inverse_real_of_posnat_gt_real
+ simp del: real_of_nat_Suc)
lemma inverse_real_of_posnat_ge_real_FreeUltrafilterNat:
"0 < u ==> \<not> eventually (\<lambda>n. u \<le> inverse(real(Suc n))) FreeUltrafilterNat"
@@ -2188,10 +2189,8 @@
lemma SEQ_Infinitesimal:
"( *f* (%n::nat. inverse(real(Suc n)))) whn : Infinitesimal"
-apply (simp add: hypnat_omega_def starfun_star_n star_n_inverse)
-apply (simp add: Infinitesimal_FreeUltrafilterNat_iff)
-apply (simp add: real_of_nat_Suc_gt_zero FreeUltrafilterNat_inverse_real_of_posnat)
-done
+by (simp add: hypnat_omega_def starfun_star_n star_n_inverse Infinitesimal_FreeUltrafilterNat_iff
+ real_of_nat_Suc_gt_zero FreeUltrafilterNat_inverse_real_of_posnat del: real_of_nat_Suc)
text{* Example where we get a hyperreal from a real sequence
for which a particular property holds. The theorem is
--- a/src/HOL/NSA/StarDef.thy Wed Sep 30 17:09:12 2015 +0100
+++ b/src/HOL/NSA/StarDef.thy Wed Sep 30 17:17:53 2015 +0100
@@ -1009,18 +1009,42 @@
apply(transfer, rule zero_not_eq_two)
done
-instance star :: (semiring_numeral_div) semiring_numeral_div
-apply intro_classes
-apply(transfer, fact semiring_numeral_div_class.div_less)
-apply(transfer, fact semiring_numeral_div_class.mod_less)
-apply(transfer, fact semiring_numeral_div_class.div_positive)
-apply(transfer, fact semiring_numeral_div_class.mod_less_eq_dividend)
-apply(transfer, fact semiring_numeral_div_class.pos_mod_bound)
-apply(transfer, fact semiring_numeral_div_class.pos_mod_sign)
-apply(transfer, fact semiring_numeral_div_class.mod_mult2_eq)
-apply(transfer, fact semiring_numeral_div_class.div_mult2_eq)
-apply(transfer, fact discrete)
-done
+instantiation star :: (semiring_numeral_div) semiring_numeral_div
+begin
+
+definition divmod_star :: "num \<Rightarrow> num \<Rightarrow> 'a star \<times> 'a star"
+where
+ divmod_star_def: "divmod_star m n = (numeral m div numeral n, numeral m mod numeral n)"
+
+definition divmod_step_star :: "num \<Rightarrow> 'a star \<times> 'a star \<Rightarrow> 'a star \<times> 'a star"
+where
+ "divmod_step_star l qr = (let (q, r) = qr
+ in if r \<ge> numeral l then (2 * q + 1, r - numeral l)
+ else (2 * q, r))"
+
+instance proof
+ show "divmod m n = (numeral m div numeral n :: 'a star, numeral m mod numeral n)"
+ for m n by (fact divmod_star_def)
+ show "divmod_step l qr = (let (q, r) = qr
+ in if r \<ge> numeral l then (2 * q + 1, r - numeral l)
+ else (2 * q, r))" for l and qr :: "'a star \<times> 'a star"
+ by (fact divmod_step_star_def)
+qed (transfer,
+ fact
+ semiring_numeral_div_class.div_less
+ semiring_numeral_div_class.mod_less
+ semiring_numeral_div_class.div_positive
+ semiring_numeral_div_class.mod_less_eq_dividend
+ semiring_numeral_div_class.pos_mod_bound
+ semiring_numeral_div_class.pos_mod_sign
+ semiring_numeral_div_class.mod_mult2_eq
+ semiring_numeral_div_class.div_mult2_eq
+ semiring_numeral_div_class.discrete)+
+
+end
+
+declare divmod_algorithm_code [where ?'a = "'a::semiring_numeral_div star", code]
+
subsection {* Finite class *}
--- a/src/HOL/Probability/Borel_Space.thy Wed Sep 30 17:09:12 2015 +0100
+++ b/src/HOL/Probability/Borel_Space.thy Wed Sep 30 17:17:53 2015 +0100
@@ -618,7 +618,7 @@
interpret sigma_algebra UNIV ?SIGMA
by (intro sigma_algebra_sigma_sets) simp_all
have *: "?set = (\<Union>n. UNIV - {x::'a. x \<bullet> i < a + 1 / real (Suc n)})"
- proof (safe, simp_all add: not_less)
+ proof (safe, simp_all add: not_less del: real_of_nat_Suc)
fix x :: 'a assume "a < x \<bullet> i"
with reals_Archimedean[of "x \<bullet> i - a"]
obtain n where "a + 1 / real (Suc n) < x \<bullet> i"
@@ -655,7 +655,7 @@
fix a :: real and i :: 'a assume "(a, i) \<in> UNIV \<times> Basis"
then have i: "i \<in> Basis" by auto
have *: "{x::'a. x\<bullet>i < a} = (\<Union>n. {x. x\<bullet>i \<le> a - 1/real (Suc n)})"
- proof (safe, simp_all)
+ proof (safe, simp_all del: real_of_nat_Suc)
fix x::'a assume *: "x\<bullet>i < a"
with reals_Archimedean[of "a - x\<bullet>i"]
obtain n where "x \<bullet> i < a - 1 / (real (Suc n))"
--- a/src/HOL/Probability/Caratheodory.thy Wed Sep 30 17:09:12 2015 +0100
+++ b/src/HOL/Probability/Caratheodory.thy Wed Sep 30 17:17:53 2015 +0100
@@ -41,49 +41,43 @@
ultimately
show ?thesis unfolding g_def using pos
by (auto intro!: SUP_eq simp: setsum.cartesian_product reindex SUP_upper2
- setsum_nonneg suminf_ereal_eq_SUP SUP_pair
+ suminf_ereal_eq_SUP SUP_pair
SUP_ereal_setsum[symmetric] incseq_setsumI setsum_nonneg)
qed
subsection {* Characterizations of Measures *}
-definition subadditive where "subadditive M f \<longleftrightarrow>
- (\<forall>x\<in>M. \<forall>y\<in>M. x \<inter> y = {} \<longrightarrow> f (x \<union> y) \<le> f x + f y)"
-
-definition countably_subadditive where "countably_subadditive M f \<longleftrightarrow>
- (\<forall>A. range A \<subseteq> M \<longrightarrow> disjoint_family A \<longrightarrow> (\<Union>i. A i) \<in> M \<longrightarrow>
- (f (\<Union>i. A i) \<le> (\<Sum>i. f (A i))))"
+definition subadditive where
+ "subadditive M f \<longleftrightarrow> (\<forall>x\<in>M. \<forall>y\<in>M. x \<inter> y = {} \<longrightarrow> f (x \<union> y) \<le> f x + f y)"
-definition outer_measure_space where "outer_measure_space M f \<longleftrightarrow>
- positive M f \<and> increasing M f \<and> countably_subadditive M f"
+definition countably_subadditive where
+ "countably_subadditive M f \<longleftrightarrow>
+ (\<forall>A. range A \<subseteq> M \<longrightarrow> disjoint_family A \<longrightarrow> (\<Union>i. A i) \<in> M \<longrightarrow> (f (\<Union>i. A i) \<le> (\<Sum>i. f (A i))))"
-definition measure_set where "measure_set M f X = {r.
- \<exists>A. range A \<subseteq> M \<and> disjoint_family A \<and> X \<subseteq> (\<Union>i. A i) \<and> (\<Sum>i. f (A i)) = r}"
+definition outer_measure_space where
+ "outer_measure_space M f \<longleftrightarrow> positive M f \<and> increasing M f \<and> countably_subadditive M f"
-lemma subadditiveD:
- "subadditive M f \<Longrightarrow> x \<inter> y = {} \<Longrightarrow> x \<in> M \<Longrightarrow> y \<in> M \<Longrightarrow> f (x \<union> y) \<le> f x + f y"
+lemma subadditiveD: "subadditive M f \<Longrightarrow> x \<inter> y = {} \<Longrightarrow> x \<in> M \<Longrightarrow> y \<in> M \<Longrightarrow> f (x \<union> y) \<le> f x + f y"
by (auto simp add: subadditive_def)
subsubsection {* Lambda Systems *}
-definition lambda_system where "lambda_system \<Omega> M f = {l \<in> M.
- \<forall>x \<in> M. f (l \<inter> x) + f ((\<Omega> - l) \<inter> x) = f x}"
+definition lambda_system where
+ "lambda_system \<Omega> M f = {l \<in> M. \<forall>x \<in> M. f (l \<inter> x) + f ((\<Omega> - l) \<inter> x) = f x}"
lemma (in algebra) lambda_system_eq:
- shows "lambda_system \<Omega> M f = {l \<in> M. \<forall>x \<in> M. f (x \<inter> l) + f (x - l) = f x}"
+ "lambda_system \<Omega> M f = {l \<in> M. \<forall>x \<in> M. f (x \<inter> l) + f (x - l) = f x}"
proof -
- have [simp]: "!!l x. l \<in> M \<Longrightarrow> x \<in> M \<Longrightarrow> (\<Omega> - l) \<inter> x = x - l"
+ have [simp]: "\<And>l x. l \<in> M \<Longrightarrow> x \<in> M \<Longrightarrow> (\<Omega> - l) \<inter> x = x - l"
by (metis Int_Diff Int_absorb1 Int_commute sets_into_space)
show ?thesis
by (auto simp add: lambda_system_def) (metis Int_commute)+
qed
-lemma (in algebra) lambda_system_empty:
- "positive M f \<Longrightarrow> {} \<in> lambda_system \<Omega> M f"
+lemma (in algebra) lambda_system_empty: "positive M f \<Longrightarrow> {} \<in> lambda_system \<Omega> M f"
by (auto simp add: positive_def lambda_system_eq)
-lemma lambda_system_sets:
- "x \<in> lambda_system \<Omega> M f \<Longrightarrow> x \<in> M"
+lemma lambda_system_sets: "x \<in> lambda_system \<Omega> M f \<Longrightarrow> x \<in> M"
by (simp add: lambda_system_def)
lemma (in algebra) lambda_system_Compl:
@@ -201,12 +195,10 @@
by (auto simp add: Un o_def suminf_binaryset_eq positive_def)
qed
-lemma lambda_system_increasing:
- "increasing M f \<Longrightarrow> increasing (lambda_system \<Omega> M f) f"
+lemma lambda_system_increasing: "increasing M f \<Longrightarrow> increasing (lambda_system \<Omega> M f) f"
by (simp add: increasing_def lambda_system_def)
-lemma lambda_system_positive:
- "positive M f \<Longrightarrow> positive (lambda_system \<Omega> M f) f"
+lemma lambda_system_positive: "positive M f \<Longrightarrow> positive (lambda_system \<Omega> M f) f"
by (simp add: positive_def lambda_system_def)
lemma (in algebra) lambda_system_strong_sum:
@@ -258,66 +250,56 @@
have *: "\<And>i. 0 \<le> f (A i)" using pos A'' unfolding positive_def by auto
have dis: "\<And>N. disjoint_family_on A {..<N}" by (intro disjoint_family_on_mono[OF _ disj]) auto
show "(\<Sum>i. f (A i)) \<le> f (\<Union>i. A i)"
- using ls.additive_sum [OF lambda_system_positive[OF pos] lambda_system_additive _ A' dis]
- using A''
+ using ls.additive_sum [OF lambda_system_positive[OF pos] lambda_system_additive _ A' dis] A''
by (intro suminf_bound[OF _ *]) (auto intro!: increasingD[OF inc] countable_UN)
qed
- {
- fix a
- assume a [iff]: "a \<in> M"
- have "f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i)) = f a"
- proof -
- show ?thesis
- proof (rule antisym)
- have "range (\<lambda>i. a \<inter> A i) \<subseteq> M" using A''
- by blast
- moreover
- have "disjoint_family (\<lambda>i. a \<inter> A i)" using disj
- by (auto simp add: disjoint_family_on_def)
- moreover
- have "a \<inter> (\<Union>i. A i) \<in> M"
- by (metis Int U_in a)
- ultimately
- have "f (a \<inter> (\<Union>i. A i)) \<le> (\<Sum>i. f (a \<inter> A i))"
- using csa[unfolded countably_subadditive_def, rule_format, of "(\<lambda>i. a \<inter> A i)"]
- by (simp add: o_def)
- hence "f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i)) \<le>
- (\<Sum>i. f (a \<inter> A i)) + f (a - (\<Union>i. A i))"
- by (rule add_right_mono)
- moreover
- have "(\<Sum>i. f (a \<inter> A i)) + f (a - (\<Union>i. A i)) \<le> f a"
- proof (intro suminf_bound_add allI)
- fix n
- have UNION_in: "(\<Union>i\<in>{0..<n}. A i) \<in> M"
- by (metis A'' UNION_in_sets)
- have le_fa: "f (UNION {0..<n} A \<inter> a) \<le> f a" using A''
- by (blast intro: increasingD [OF inc] A'' UNION_in_sets)
- have ls: "(\<Union>i\<in>{0..<n}. A i) \<in> lambda_system \<Omega> M f"
- using ls.UNION_in_sets by (simp add: A)
- hence eq_fa: "f a = f (a \<inter> (\<Union>i\<in>{0..<n}. A i)) + f (a - (\<Union>i\<in>{0..<n}. A i))"
- by (simp add: lambda_system_eq UNION_in)
- have "f (a - (\<Union>i. A i)) \<le> f (a - (\<Union>i\<in>{0..<n}. A i))"
- by (blast intro: increasingD [OF inc] UNION_in U_in)
- thus "(\<Sum>i<n. f (a \<inter> A i)) + f (a - (\<Union>i. A i)) \<le> f a"
- by (simp add: lambda_system_strong_sum pos A disj eq_fa add_left_mono atLeast0LessThan[symmetric])
- next
- have "\<And>i. a \<inter> A i \<in> M" using A'' by auto
- then show "\<And>i. 0 \<le> f (a \<inter> A i)" using pos[unfolded positive_def] by auto
- have "\<And>i. a - (\<Union>i. A i) \<in> M" using A'' by auto
- then have "\<And>i. 0 \<le> f (a - (\<Union>i. A i))" using pos[unfolded positive_def] by auto
- then show "f (a - (\<Union>i. A i)) \<noteq> -\<infinity>" by auto
- qed
- ultimately show "f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i)) \<le> f a"
- by (rule order_trans)
- next
- have "f a \<le> f (a \<inter> (\<Union>i. A i) \<union> (a - (\<Union>i. A i)))"
- by (blast intro: increasingD [OF inc] U_in)
- also have "... \<le> f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i))"
- by (blast intro: subadditiveD [OF sa] U_in)
- finally show "f a \<le> f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i))" .
- qed
- qed
- }
+ have "f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i)) = f a"
+ if a [iff]: "a \<in> M" for a
+ proof (rule antisym)
+ have "range (\<lambda>i. a \<inter> A i) \<subseteq> M" using A''
+ by blast
+ moreover
+ have "disjoint_family (\<lambda>i. a \<inter> A i)" using disj
+ by (auto simp add: disjoint_family_on_def)
+ moreover
+ have "a \<inter> (\<Union>i. A i) \<in> M"
+ by (metis Int U_in a)
+ ultimately
+ have "f (a \<inter> (\<Union>i. A i)) \<le> (\<Sum>i. f (a \<inter> A i))"
+ using csa[unfolded countably_subadditive_def, rule_format, of "(\<lambda>i. a \<inter> A i)"]
+ by (simp add: o_def)
+ hence "f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i)) \<le> (\<Sum>i. f (a \<inter> A i)) + f (a - (\<Union>i. A i))"
+ by (rule add_right_mono)
+ also have "\<dots> \<le> f a"
+ proof (intro suminf_bound_add allI)
+ fix n
+ have UNION_in: "(\<Union>i\<in>{0..<n}. A i) \<in> M"
+ by (metis A'' UNION_in_sets)
+ have le_fa: "f (UNION {0..<n} A \<inter> a) \<le> f a" using A''
+ by (blast intro: increasingD [OF inc] A'' UNION_in_sets)
+ have ls: "(\<Union>i\<in>{0..<n}. A i) \<in> lambda_system \<Omega> M f"
+ using ls.UNION_in_sets by (simp add: A)
+ hence eq_fa: "f a = f (a \<inter> (\<Union>i\<in>{0..<n}. A i)) + f (a - (\<Union>i\<in>{0..<n}. A i))"
+ by (simp add: lambda_system_eq UNION_in)
+ have "f (a - (\<Union>i. A i)) \<le> f (a - (\<Union>i\<in>{0..<n}. A i))"
+ by (blast intro: increasingD [OF inc] UNION_in U_in)
+ thus "(\<Sum>i<n. f (a \<inter> A i)) + f (a - (\<Union>i. A i)) \<le> f a"
+ by (simp add: lambda_system_strong_sum pos A disj eq_fa add_left_mono atLeast0LessThan[symmetric])
+ next
+ have "\<And>i. a \<inter> A i \<in> M" using A'' by auto
+ then show "\<And>i. 0 \<le> f (a \<inter> A i)" using pos[unfolded positive_def] by auto
+ have "\<And>i. a - (\<Union>i. A i) \<in> M" using A'' by auto
+ then have "\<And>i. 0 \<le> f (a - (\<Union>i. A i))" using pos[unfolded positive_def] by auto
+ then show "f (a - (\<Union>i. A i)) \<noteq> -\<infinity>" by auto
+ qed
+ finally show "f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i)) \<le> f a" .
+ next
+ have "f a \<le> f (a \<inter> (\<Union>i. A i) \<union> (a - (\<Union>i. A i)))"
+ by (blast intro: increasingD [OF inc] U_in)
+ also have "... \<le> f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i))"
+ by (blast intro: subadditiveD [OF sa] U_in)
+ finally show "f a \<le> f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i))" .
+ qed
thus ?thesis
by (simp add: lambda_system_eq sums_iff U_eq U_in)
qed
@@ -345,300 +327,186 @@
using pos by (simp add: measure_space_def)
qed
-lemma inf_measure_nonempty:
- assumes f: "positive M f" and b: "b \<in> M" and a: "a \<subseteq> b" "{} \<in> M"
- shows "f b \<in> measure_set M f a"
-proof -
- let ?A = "\<lambda>i::nat. (if i = 0 then b else {})"
- have "(\<Sum>i. f (?A i)) = (\<Sum>i<1::nat. f (?A i))"
- by (rule suminf_finite) (simp_all add: f[unfolded positive_def])
- also have "... = f b"
- by simp
- finally show ?thesis using assms
- by (auto intro!: exI [of _ ?A]
- simp: measure_set_def disjoint_family_on_def split_if_mem2 comp_def)
-qed
+definition outer_measure :: "'a set set \<Rightarrow> ('a set \<Rightarrow> ereal) \<Rightarrow> 'a set \<Rightarrow> ereal" where
+ "outer_measure M f X =
+ (INF A:{A. range A \<subseteq> M \<and> disjoint_family A \<and> X \<subseteq> (\<Union>i. A i)}. \<Sum>i. f (A i))"
-lemma (in ring_of_sets) inf_measure_agrees:
- assumes posf: "positive M f" and ca: "countably_additive M f"
- and s: "s \<in> M"
- shows "Inf (measure_set M f s) = f s"
-proof (intro Inf_eqI)
- fix z
- assume z: "z \<in> measure_set M f s"
- from this obtain A where
- A: "range A \<subseteq> M" and disj: "disjoint_family A"
- and "s \<subseteq> (\<Union>x. A x)" and si: "(\<Sum>i. f (A i)) = z"
- by (auto simp add: measure_set_def comp_def)
- hence seq: "s = (\<Union>i. A i \<inter> s)" by blast
+lemma (in ring_of_sets) outer_measure_agrees:
+ assumes posf: "positive M f" and ca: "countably_additive M f" and s: "s \<in> M"
+ shows "outer_measure M f s = f s"
+ unfolding outer_measure_def
+proof (safe intro!: antisym INF_greatest)
+ fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> M" and dA: "disjoint_family A" and sA: "s \<subseteq> (\<Union>x. A x)"
have inc: "increasing M f"
by (metis additive_increasing ca countably_additive_additive posf)
- have sums: "(\<Sum>i. f (A i \<inter> s)) = f (\<Union>i. A i \<inter> s)"
- proof (rule ca[unfolded countably_additive_def, rule_format])
- show "range (\<lambda>n. A n \<inter> s) \<subseteq> M" using A s
- by blast
- show "disjoint_family (\<lambda>n. A n \<inter> s)" using disj
- by (auto simp add: disjoint_family_on_def)
- show "(\<Union>i. A i \<inter> s) \<in> M" using A s
- by (metis UN_extend_simps(4) s seq)
- qed
- hence "f s = (\<Sum>i. f (A i \<inter> s))"
- using seq [symmetric] by (simp add: sums_iff)
+ have "f s = f (\<Union>i. A i \<inter> s)"
+ using sA by (auto simp: Int_absorb1)
+ also have "\<dots> = (\<Sum>i. f (A i \<inter> s))"
+ using sA dA A s
+ by (intro ca[unfolded countably_additive_def, rule_format, symmetric])
+ (auto simp: Int_absorb1 disjoint_family_on_def)
also have "... \<le> (\<Sum>i. f (A i))"
- proof (rule suminf_le_pos)
- fix n show "f (A n \<inter> s) \<le> f (A n)" using A s
- by (force intro: increasingD [OF inc])
- fix N have "A N \<inter> s \<in> M" using A s by auto
- then show "0 \<le> f (A N \<inter> s)" using posf unfolding positive_def by auto
- qed
- also have "... = z" by (rule si)
- finally show "f s \<le> z" .
-qed (blast intro: inf_measure_nonempty [of _ f, OF posf s subset_refl])
-
-lemma measure_set_pos:
- assumes posf: "positive M f" "r \<in> measure_set M f X"
- shows "0 \<le> r"
-proof -
- obtain A where "range A \<subseteq> M" and r: "r = (\<Sum>i. f (A i))"
- using `r \<in> measure_set M f X` unfolding measure_set_def by auto
- then show "0 \<le> r" using posf unfolding r positive_def
- by (intro suminf_0_le) auto
-qed
-
-lemma inf_measure_pos:
- assumes posf: "positive M f"
- shows "0 \<le> Inf (measure_set M f X)"
-proof (rule complete_lattice_class.Inf_greatest)
- fix r assume "r \<in> measure_set M f X" with posf show "0 \<le> r"
- by (rule measure_set_pos)
+ using A s by (intro suminf_le_pos increasingD[OF inc] positiveD2[OF posf]) auto
+ finally show "f s \<le> (\<Sum>i. f (A i))" .
+next
+ have "(\<Sum>i. f (if i = 0 then s else {})) \<le> f s"
+ using positiveD1[OF posf] by (subst suminf_finite[of "{0}"]) auto
+ with s show "(INF A:{A. range A \<subseteq> M \<and> disjoint_family A \<and> s \<subseteq> UNION UNIV A}. \<Sum>i. f (A i)) \<le> f s"
+ by (intro INF_lower2[of "\<lambda>i. if i = 0 then s else {}"])
+ (auto simp: disjoint_family_on_def)
qed
-lemma inf_measure_empty:
+lemma outer_measure_nonneg: "positive M f \<Longrightarrow> 0 \<le> outer_measure M f X"
+ by (auto intro!: INF_greatest suminf_0_le intro: positiveD2 simp: outer_measure_def)
+
+lemma outer_measure_empty:
assumes posf: "positive M f" and "{} \<in> M"
- shows "Inf (measure_set M f {}) = 0"
+ shows "outer_measure M f {} = 0"
proof (rule antisym)
- show "Inf (measure_set M f {}) \<le> 0"
- by (metis complete_lattice_class.Inf_lower `{} \<in> M`
- inf_measure_nonempty[OF posf] subset_refl posf[unfolded positive_def])
-qed (rule inf_measure_pos[OF posf])
+ show "outer_measure M f {} \<le> 0"
+ using assms by (auto intro!: INF_lower2[of "\<lambda>_. {}"] simp: outer_measure_def disjoint_family_on_def positive_def)
+qed (intro outer_measure_nonneg posf)
+
+lemma (in ring_of_sets) positive_outer_measure:
+ assumes "positive M f" shows "positive (Pow \<Omega>) (outer_measure M f)"
+ unfolding positive_def by (auto simp: assms outer_measure_empty outer_measure_nonneg)
+
+lemma (in ring_of_sets) increasing_outer_measure: "increasing (Pow \<Omega>) (outer_measure M f)"
+ by (force simp: increasing_def outer_measure_def intro!: INF_greatest intro: INF_lower)
-lemma (in ring_of_sets) inf_measure_positive:
- assumes p: "positive M f" and "{} \<in> M"
- shows "positive M (\<lambda>x. Inf (measure_set M f x))"
-proof (unfold positive_def, intro conjI ballI)
- show "Inf (measure_set M f {}) = 0" using inf_measure_empty[OF assms] by auto
- fix A assume "A \<in> M"
-qed (rule inf_measure_pos[OF p])
+lemma (in ring_of_sets) outer_measure_le:
+ assumes pos: "positive M f" and inc: "increasing M f" and A: "range A \<subseteq> M" and X: "X \<subseteq> (\<Union>i. A i)"
+ shows "outer_measure M f X \<le> (\<Sum>i. f (A i))"
+ unfolding outer_measure_def
+proof (safe intro!: INF_lower2[of "disjointed A"] del: subsetI)
+ show dA: "range (disjointed A) \<subseteq> M"
+ by (auto intro!: A range_disjointed_sets)
+ have "\<forall>n. f (disjointed A n) \<le> f (A n)"
+ by (metis increasingD [OF inc] UNIV_I dA image_subset_iff disjointed_subset A)
+ moreover have "\<forall>i. 0 \<le> f (disjointed A i)"
+ using pos dA unfolding positive_def by auto
+ ultimately show "(\<Sum>i. f (disjointed A i)) \<le> (\<Sum>i. f (A i))"
+ by (blast intro!: suminf_le_pos)
+qed (auto simp: X UN_disjointed_eq disjoint_family_disjointed)
-lemma (in ring_of_sets) inf_measure_increasing:
- assumes posf: "positive M f"
- shows "increasing (Pow \<Omega>) (\<lambda>x. Inf (measure_set M f x))"
-apply (clarsimp simp add: increasing_def)
-apply (rule complete_lattice_class.Inf_greatest)
-apply (rule complete_lattice_class.Inf_lower)
-apply (clarsimp simp add: measure_set_def, rule_tac x=A in exI, blast)
-done
-
-lemma (in ring_of_sets) inf_measure_le:
- assumes posf: "positive M f" and inc: "increasing M f"
- and x: "x \<in> {r . \<exists>A. range A \<subseteq> M \<and> s \<subseteq> (\<Union>i. A i) \<and> (\<Sum>i. f (A i)) = r}"
- shows "Inf (measure_set M f s) \<le> x"
+lemma (in ring_of_sets) outer_measure_close:
+ assumes posf: "positive M f" and "0 < e" and "outer_measure M f X \<noteq> \<infinity>"
+ shows "\<exists>A. range A \<subseteq> M \<and> disjoint_family A \<and> X \<subseteq> (\<Union>i. A i) \<and> (\<Sum>i. f (A i)) \<le> outer_measure M f X + e"
proof -
- obtain A where A: "range A \<subseteq> M" and ss: "s \<subseteq> (\<Union>i. A i)"
- and xeq: "(\<Sum>i. f (A i)) = x"
- using x by auto
- have dA: "range (disjointed A) \<subseteq> M"
- by (metis A range_disjointed_sets)
- have "\<forall>n. f (disjointed A n) \<le> f (A n)"
- by (metis increasingD [OF inc] UNIV_I dA image_subset_iff disjointed_subset A comp_def)
- moreover have "\<forall>i. 0 \<le> f (disjointed A i)"
- using posf dA unfolding positive_def by auto
- ultimately have sda: "(\<Sum>i. f (disjointed A i)) \<le> (\<Sum>i. f (A i))"
- by (blast intro!: suminf_le_pos)
- hence ley: "(\<Sum>i. f (disjointed A i)) \<le> x"
- by (metis xeq)
- hence y: "(\<Sum>i. f (disjointed A i)) \<in> measure_set M f s"
- apply (auto simp add: measure_set_def)
- apply (rule_tac x="disjointed A" in exI)
- apply (simp add: disjoint_family_disjointed UN_disjointed_eq ss dA comp_def)
- done
+ from `outer_measure M f X \<noteq> \<infinity>` have fin: "\<bar>outer_measure M f X\<bar> \<noteq> \<infinity>"
+ using outer_measure_nonneg[OF posf, of X] by auto
show ?thesis
- by (blast intro: y order_trans [OF _ ley] posf complete_lattice_class.Inf_lower)
-qed
-
-lemma (in ring_of_sets) inf_measure_close:
- fixes e :: ereal
- assumes posf: "positive M f" and e: "0 < e" and ss: "s \<subseteq> (\<Omega>)" and "Inf (measure_set M f s) \<noteq> \<infinity>"
- shows "\<exists>A. range A \<subseteq> M \<and> disjoint_family A \<and> s \<subseteq> (\<Union>i. A i) \<and>
- (\<Sum>i. f (A i)) \<le> Inf (measure_set M f s) + e"
-proof -
- from `Inf (measure_set M f s) \<noteq> \<infinity>` have fin: "\<bar>Inf (measure_set M f s)\<bar> \<noteq> \<infinity>"
- using inf_measure_pos[OF posf, of s] by auto
- obtain l where "l \<in> measure_set M f s" "l \<le> Inf (measure_set M f s) + e"
- using Inf_ereal_close[OF fin e] by auto
- thus ?thesis
- by (auto intro!: exI[of _ l] simp: measure_set_def comp_def)
+ using Inf_ereal_close[OF fin[unfolded outer_measure_def INF_def], OF \<open>0 < e\<close>]
+ unfolding INF_def[symmetric] outer_measure_def[symmetric] by (auto intro: less_imp_le)
qed
-lemma (in ring_of_sets) inf_measure_countably_subadditive:
+lemma (in ring_of_sets) countably_subadditive_outer_measure:
assumes posf: "positive M f" and inc: "increasing M f"
- shows "countably_subadditive (Pow \<Omega>) (\<lambda>x. Inf (measure_set M f x))"
+ shows "countably_subadditive (Pow \<Omega>) (outer_measure M f)"
proof (simp add: countably_subadditive_def, safe)
- fix A :: "nat \<Rightarrow> 'a set"
- let ?outer = "\<lambda>B. Inf (measure_set M f B)"
- assume A: "range A \<subseteq> Pow (\<Omega>)"
- and disj: "disjoint_family A"
- and sb: "(\<Union>i. A i) \<subseteq> \<Omega>"
+ fix A :: "nat \<Rightarrow> _" assume A: "range A \<subseteq> Pow (\<Omega>)" and sb: "(\<Union>i. A i) \<subseteq> \<Omega>"
+ let ?O = "outer_measure M f"
- { fix e :: ereal assume e: "0 < e" and "\<forall>i. ?outer (A i) \<noteq> \<infinity>"
- hence "\<exists>BB. \<forall>n. range (BB n) \<subseteq> M \<and> disjoint_family (BB n) \<and>
- A n \<subseteq> (\<Union>i. BB n i) \<and> (\<Sum>i. f (BB n i)) \<le> ?outer (A n) + e * (1/2)^(Suc n)"
- apply (safe intro!: choice inf_measure_close [of f, OF posf])
- using e sb by (auto simp: ereal_zero_less_0_iff one_ereal_def)
- then obtain BB
- where BB: "\<And>n. (range (BB n) \<subseteq> M)"
- and disjBB: "\<And>n. disjoint_family (BB n)"
- and sbBB: "\<And>n. A n \<subseteq> (\<Union>i. BB n i)"
- and BBle: "\<And>n. (\<Sum>i. f (BB n i)) \<le> ?outer (A n) + e * (1/2)^(Suc n)"
+ { fix e :: ereal assume e: "0 < e" and "\<forall>i. ?O (A i) \<noteq> \<infinity>"
+ hence "\<exists>B. \<forall>n. range (B n) \<subseteq> M \<and> disjoint_family (B n) \<and> A n \<subseteq> (\<Union>i. B n i) \<and>
+ (\<Sum>i. f (B n i)) \<le> ?O (A n) + e * (1/2)^(Suc n)"
+ using e sb by (auto intro!: choice outer_measure_close [of f, OF posf] simp: ereal_zero_less_0_iff one_ereal_def)
+ then obtain B
+ where B: "\<And>n. range (B n) \<subseteq> M"
+ and sbB: "\<And>n. A n \<subseteq> (\<Union>i. B n i)"
+ and Ble: "\<And>n. (\<Sum>i. f (B n i)) \<le> ?O (A n) + e * (1/2)^(Suc n)"
by auto blast
- have sll: "(\<Sum>n. \<Sum>i. (f (BB n i))) \<le> (\<Sum>n. ?outer (A n)) + e"
- proof -
- have sum_eq_1: "(\<Sum>n. e*(1/2) ^ Suc n) = e"
- using suminf_half_series_ereal e
- by (simp add: ereal_zero_le_0_iff zero_le_divide_ereal suminf_cmult_ereal)
- have "\<And>n i. 0 \<le> f (BB n i)" using posf[unfolded positive_def] BB by auto
- then have "\<And>n. 0 \<le> (\<Sum>i. f (BB n i))" by (rule suminf_0_le)
- then have "(\<Sum>n. \<Sum>i. (f (BB n i))) \<le> (\<Sum>n. ?outer (A n) + e*(1/2) ^ Suc n)"
- by (rule suminf_le_pos[OF BBle])
- also have "... = (\<Sum>n. ?outer (A n)) + e"
- using sum_eq_1 inf_measure_pos[OF posf] e
- by (subst suminf_add_ereal) (auto simp add: ereal_zero_le_0_iff)
- finally show ?thesis .
- qed
- def C \<equiv> "(split BB) o prod_decode"
- from BB have "\<And>i j. BB i j \<in> M"
+
+ def C \<equiv> "split B o prod_decode"
+ from B have B_in_M: "\<And>i j. B i j \<in> M"
by (rule range_subsetD)
- then have C: "\<And>n. C n \<in> M"
- by (simp add: C_def split_def)
- have sbC: "(\<Union>i. A i) \<subseteq> (\<Union>i. C i)"
- proof (auto simp add: C_def)
- fix x i
- assume x: "x \<in> A i"
- with sbBB [of i] obtain j where "x \<in> BB i j"
- by blast
- thus "\<exists>i. x \<in> split BB (prod_decode i)"
- by (metis prod_encode_inverse prod.case)
- qed
- have "(f \<circ> C) = (f \<circ> (\<lambda>(x, y). BB x y)) \<circ> prod_decode"
- by (rule ext) (auto simp add: C_def)
- moreover have "suminf ... = (\<Sum>n. \<Sum>i. f (BB n i))" using BBle
- using BB posf[unfolded positive_def]
- by (force intro!: suminf_ereal_2dimen simp: o_def)
- ultimately have Csums: "(\<Sum>i. f (C i)) = (\<Sum>n. \<Sum>i. f (BB n i))" by (simp add: o_def)
- have "?outer (\<Union>i. A i) \<le> (\<Sum>n. \<Sum>i. f (BB n i))"
- apply (rule inf_measure_le [OF posf(1) inc], auto)
- apply (rule_tac x="C" in exI)
- apply (auto simp add: C sbC Csums)
- done
- also have "... \<le> (\<Sum>n. ?outer (A n)) + e" using sll
- by blast
- finally have "?outer (\<Union>i. A i) \<le> (\<Sum>n. ?outer (A n)) + e" . }
- note for_finite_Inf = this
+ then have C: "range C \<subseteq> M"
+ by (auto simp add: C_def split_def)
+ have A_C: "(\<Union>i. A i) \<subseteq> (\<Union>i. C i)"
+ using sbB by (auto simp add: C_def subset_eq) (metis prod.case prod_encode_inverse)
- show "?outer (\<Union>i. A i) \<le> (\<Sum>n. ?outer (A n))"
+ have "?O (\<Union>i. A i) \<le> ?O (\<Union>i. C i)"
+ using A_C A C by (intro increasing_outer_measure[THEN increasingD]) (auto dest!: sets_into_space)
+ also have "\<dots> \<le> (\<Sum>i. f (C i))"
+ using C by (intro outer_measure_le[OF posf inc]) auto
+ also have "\<dots> = (\<Sum>n. \<Sum>i. f (B n i))"
+ using B_in_M unfolding C_def comp_def by (intro suminf_ereal_2dimen positiveD2[OF posf]) auto
+ also have "\<dots> \<le> (\<Sum>n. ?O (A n) + e*(1/2) ^ Suc n)"
+ using B_in_M by (intro suminf_le_pos[OF Ble] suminf_0_le posf[THEN positiveD2]) auto
+ also have "... = (\<Sum>n. ?O (A n)) + (\<Sum>n. e*(1/2) ^ Suc n)"
+ using e by (subst suminf_add_ereal) (auto simp add: ereal_zero_le_0_iff outer_measure_nonneg posf)
+ also have "(\<Sum>n. e*(1/2) ^ Suc n) = e"
+ using suminf_half_series_ereal e by (simp add: ereal_zero_le_0_iff suminf_cmult_ereal)
+ finally have "?O (\<Union>i. A i) \<le> (\<Sum>n. ?O (A n)) + e" . }
+ note * = this
+
+ show "?O (\<Union>i. A i) \<le> (\<Sum>n. ?O (A n))"
proof cases
- assume "\<forall>i. ?outer (A i) \<noteq> \<infinity>"
- with for_finite_Inf show ?thesis
+ assume "\<forall>i. ?O (A i) \<noteq> \<infinity>" with * show ?thesis
by (intro ereal_le_epsilon) auto
- next
- assume "\<not> (\<forall>i. ?outer (A i) \<noteq> \<infinity>)"
- then have "\<exists>i. ?outer (A i) = \<infinity>"
- by auto
- then have "(\<Sum>n. ?outer (A n)) = \<infinity>"
- using suminf_PInfty[OF inf_measure_pos, OF posf]
- by metis
- then show ?thesis by simp
- qed
+ qed (metis suminf_PInfty[OF outer_measure_nonneg, OF posf] ereal_less_eq(1))
qed
-lemma (in ring_of_sets) inf_measure_outer:
- "\<lbrakk> positive M f ; increasing M f \<rbrakk> \<Longrightarrow>
- outer_measure_space (Pow \<Omega>) (\<lambda>x. Inf (measure_set M f x))"
- using inf_measure_pos[of M f]
- by (simp add: outer_measure_space_def inf_measure_empty
- inf_measure_increasing inf_measure_countably_subadditive positive_def)
+lemma (in ring_of_sets) outer_measure_space_outer_measure:
+ "positive M f \<Longrightarrow> increasing M f \<Longrightarrow> outer_measure_space (Pow \<Omega>) (outer_measure M f)"
+ by (simp add: outer_measure_space_def
+ positive_outer_measure increasing_outer_measure countably_subadditive_outer_measure)
lemma (in ring_of_sets) algebra_subset_lambda_system:
assumes posf: "positive M f" and inc: "increasing M f"
and add: "additive M f"
- shows "M \<subseteq> lambda_system \<Omega> (Pow \<Omega>) (\<lambda>x. Inf (measure_set M f x))"
+ shows "M \<subseteq> lambda_system \<Omega> (Pow \<Omega>) (outer_measure M f)"
proof (auto dest: sets_into_space
simp add: algebra.lambda_system_eq [OF algebra_Pow])
- fix x s
- assume x: "x \<in> M"
- and s: "s \<subseteq> \<Omega>"
- have [simp]: "!!x. x \<in> M \<Longrightarrow> s \<inter> (\<Omega> - x) = s-x" using s
+ fix x s assume x: "x \<in> M" and s: "s \<subseteq> \<Omega>"
+ have [simp]: "\<And>x. x \<in> M \<Longrightarrow> s \<inter> (\<Omega> - x) = s - x" using s
by blast
- have "Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))
- \<le> Inf (measure_set M f s)"
- proof cases
- assume "Inf (measure_set M f s) = \<infinity>" then show ?thesis by simp
- next
- assume fin: "Inf (measure_set M f s) \<noteq> \<infinity>"
- then have "measure_set M f s \<noteq> {}"
- by (auto simp: top_ereal_def)
- show ?thesis
- proof (rule complete_lattice_class.Inf_greatest)
- fix r assume "r \<in> measure_set M f s"
- then obtain A where A: "disjoint_family A" "range A \<subseteq> M" "s \<subseteq> (\<Union>i. A i)"
- and r: "r = (\<Sum>i. f (A i))" unfolding measure_set_def by auto
- have "Inf (measure_set M f (s \<inter> x)) \<le> (\<Sum>i. f (A i \<inter> x))"
- unfolding measure_set_def
- proof (safe intro!: complete_lattice_class.Inf_lower exI[of _ "\<lambda>i. A i \<inter> x"])
- from A(1) show "disjoint_family (\<lambda>i. A i \<inter> x)"
- by (rule disjoint_family_on_bisimulation) auto
- qed (insert x A, auto)
- moreover
- have "Inf (measure_set M f (s - x)) \<le> (\<Sum>i. f (A i - x))"
- unfolding measure_set_def
- proof (safe intro!: complete_lattice_class.Inf_lower exI[of _ "\<lambda>i. A i - x"])
- from A(1) show "disjoint_family (\<lambda>i. A i - x)"
- by (rule disjoint_family_on_bisimulation) auto
- qed (insert x A, auto)
- ultimately have "Inf (measure_set M f (s \<inter> x)) + Inf (measure_set M f (s - x)) \<le>
- (\<Sum>i. f (A i \<inter> x)) + (\<Sum>i. f (A i - x))" by (rule add_mono)
- also have "\<dots> = (\<Sum>i. f (A i \<inter> x) + f (A i - x))"
- using A(2) x posf by (subst suminf_add_ereal) (auto simp: positive_def)
- also have "\<dots> = (\<Sum>i. f (A i))"
- using A x
- by (subst add[THEN additiveD, symmetric])
- (auto intro!: arg_cong[where f=suminf] arg_cong[where f=f])
- finally show "Inf (measure_set M f (s \<inter> x)) + Inf (measure_set M f (s - x)) \<le> r"
- using r by simp
- qed
+ have "outer_measure M f (s \<inter> x) + outer_measure M f (s - x) \<le> outer_measure M f s"
+ unfolding outer_measure_def[of M f s]
+ proof (safe intro!: INF_greatest)
+ fix A :: "nat \<Rightarrow> 'a set" assume A: "disjoint_family A" "range A \<subseteq> M" "s \<subseteq> (\<Union>i. A i)"
+ have "outer_measure M f (s \<inter> x) \<le> (\<Sum>i. f (A i \<inter> x))"
+ unfolding outer_measure_def
+ proof (safe intro!: INF_lower2[of "\<lambda>i. A i \<inter> x"])
+ from A(1) show "disjoint_family (\<lambda>i. A i \<inter> x)"
+ by (rule disjoint_family_on_bisimulation) auto
+ qed (insert x A, auto)
+ moreover
+ have "outer_measure M f (s - x) \<le> (\<Sum>i. f (A i - x))"
+ unfolding outer_measure_def
+ proof (safe intro!: INF_lower2[of "\<lambda>i. A i - x"])
+ from A(1) show "disjoint_family (\<lambda>i. A i - x)"
+ by (rule disjoint_family_on_bisimulation) auto
+ qed (insert x A, auto)
+ ultimately have "outer_measure M f (s \<inter> x) + outer_measure M f (s - x) \<le>
+ (\<Sum>i. f (A i \<inter> x)) + (\<Sum>i. f (A i - x))" by (rule add_mono)
+ also have "\<dots> = (\<Sum>i. f (A i \<inter> x) + f (A i - x))"
+ using A(2) x posf by (subst suminf_add_ereal) (auto simp: positive_def)
+ also have "\<dots> = (\<Sum>i. f (A i))"
+ using A x
+ by (subst add[THEN additiveD, symmetric])
+ (auto intro!: arg_cong[where f=suminf] arg_cong[where f=f])
+ finally show "outer_measure M f (s \<inter> x) + outer_measure M f (s - x) \<le> (\<Sum>i. f (A i))" .
qed
moreover
- have "Inf (measure_set M f s)
- \<le> Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))"
+ have "outer_measure M f s \<le> outer_measure M f (s \<inter> x) + outer_measure M f (s - x)"
proof -
- have "Inf (measure_set M f s) = Inf (measure_set M f ((s\<inter>x) \<union> (s-x)))"
+ have "outer_measure M f s = outer_measure M f ((s \<inter> x) \<union> (s - x))"
by (metis Un_Diff_Int Un_commute)
- also have "... \<le> Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))"
+ also have "... \<le> outer_measure M f (s \<inter> x) + outer_measure M f (s - x)"
apply (rule subadditiveD)
apply (rule ring_of_sets.countably_subadditive_subadditive [OF ring_of_sets_Pow])
- apply (simp add: positive_def inf_measure_empty[OF posf] inf_measure_pos[OF posf])
- apply (rule inf_measure_countably_subadditive)
+ apply (simp add: positive_def outer_measure_empty[OF posf] outer_measure_nonneg[OF posf])
+ apply (rule countably_subadditive_outer_measure)
using s by (auto intro!: posf inc)
finally show ?thesis .
qed
ultimately
- show "Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))
- = Inf (measure_set M f s)"
+ show "outer_measure M f (s \<inter> x) + outer_measure M f (s - x) = outer_measure M f s"
by (rule order_antisym)
qed
-lemma measure_down:
- "measure_space \<Omega> N \<mu> \<Longrightarrow> sigma_algebra \<Omega> M \<Longrightarrow> M \<subseteq> N \<Longrightarrow> measure_space \<Omega> M \<mu>"
+lemma measure_down: "measure_space \<Omega> N \<mu> \<Longrightarrow> sigma_algebra \<Omega> M \<Longrightarrow> M \<subseteq> N \<Longrightarrow> measure_space \<Omega> M \<mu>"
by (auto simp add: measure_space_def positive_def countably_additive_def subset_eq)
subsection {* Caratheodory's theorem *}
@@ -649,11 +517,11 @@
proof -
have inc: "increasing M f"
by (metis additive_increasing ca countably_additive_additive posf)
- let ?infm = "(\<lambda>x. Inf (measure_set M f x))"
- def ls \<equiv> "lambda_system \<Omega> (Pow \<Omega>) ?infm"
- have mls: "measure_space \<Omega> ls ?infm"
+ let ?O = "outer_measure M f"
+ def ls \<equiv> "lambda_system \<Omega> (Pow \<Omega>) ?O"
+ have mls: "measure_space \<Omega> ls ?O"
using sigma_algebra.caratheodory_lemma
- [OF sigma_algebra_Pow inf_measure_outer [OF posf inc]]
+ [OF sigma_algebra_Pow outer_measure_space_outer_measure [OF posf inc]]
by (simp add: ls_def)
hence sls: "sigma_algebra \<Omega> ls"
by (simp add: measure_space_def)
@@ -663,11 +531,11 @@
hence sgs_sb: "sigma_sets (\<Omega>) (M) \<subseteq> ls"
using sigma_algebra.sigma_sets_subset [OF sls, of "M"]
by simp
- have "measure_space \<Omega> (sigma_sets \<Omega> M) ?infm"
+ have "measure_space \<Omega> (sigma_sets \<Omega> M) ?O"
by (rule measure_down [OF mls], rule sigma_algebra_sigma_sets)
(simp_all add: sgs_sb space_closed)
- thus ?thesis using inf_measure_agrees [OF posf ca]
- by (intro exI[of _ ?infm]) auto
+ thus ?thesis using outer_measure_agrees [OF posf ca]
+ by (intro exI[of _ ?O]) auto
qed
lemma (in ring_of_sets) caratheodory_empty_continuous:
@@ -1069,5 +937,4 @@
then show ?thesis by simp
qed
-
end
--- a/src/HOL/Probability/Lebesgue_Measure.thy Wed Sep 30 17:09:12 2015 +0100
+++ b/src/HOL/Probability/Lebesgue_Measure.thy Wed Sep 30 17:17:53 2015 +0100
@@ -1298,7 +1298,7 @@
proof (subst integral_FTC_Icc_real)
fix x show "DERIV (\<lambda>x. x^Suc k / Suc k) x :> x^k"
by (intro derivative_eq_intros) auto
-qed (auto simp: field_simps)
+qed (auto simp: field_simps simp del: real_of_nat_Suc)
subsection {* Integration by parts *}
--- a/src/HOL/Probability/Regularity.thy Wed Sep 30 17:09:12 2015 +0100
+++ b/src/HOL/Probability/Regularity.thy Wed Sep 30 17:17:53 2015 +0100
@@ -192,7 +192,7 @@
also have "\<dots> \<le> (\<Sum>n. ereal (e*2 powr - real (Suc n)))"
using B_compl_le by (intro suminf_le_pos) (simp_all add: measure_nonneg emeasure_eq_measure)
also have "\<dots> \<le> (\<Sum>n. ereal (e * (1 / 2) ^ Suc n))"
- by (simp add: Transcendental.powr_minus powr_realpow field_simps)
+ by (simp add: Transcendental.powr_minus powr_realpow field_simps del: real_of_nat_Suc)
also have "\<dots> = (\<Sum>n. ereal e * ((1 / 2) ^ Suc n))"
unfolding times_ereal.simps[symmetric] ereal_power[symmetric] one_ereal_def numeral_eq_ereal
by simp
@@ -254,7 +254,7 @@
from in_closed_iff_infdist_zero[OF `closed A` `A \<noteq> {}`]
have "A = {x. infdist x A = 0}" by auto
also have "\<dots> = (\<Inter>i. ?G (1/real (Suc i)))"
- proof (auto, rule ccontr)
+ proof (auto simp del: real_of_nat_Suc, rule ccontr)
fix x
assume "infdist x A \<noteq> 0"
hence pos: "infdist x A > 0" using infdist_nonneg[of x A] by simp
@@ -262,7 +262,7 @@
moreover
assume "\<forall>i. infdist x A < 1 / real (Suc i)"
hence "infdist x A < 1 / real (Suc n)" by auto
- ultimately show False by simp
+ ultimately show False by simp
qed
also have "M \<dots> = (INF n. emeasure M (?G (1 / real (Suc n))))"
proof (rule INF_emeasure_decseq[symmetric], safe)
@@ -439,7 +439,7 @@
by (intro suminf_le_pos, subst emeasure_Diff)
(auto simp: emeasure_Diff emeasure_eq_measure sb measure_nonneg intro: less_imp_le)
also have "\<dots> \<le> (\<Sum>n. ereal (e * (1 / 2) ^ Suc n))"
- by (simp add: powr_minus inverse_eq_divide powr_realpow field_simps power_divide)
+ by (simp add: powr_minus inverse_eq_divide powr_realpow field_simps power_divide del: real_of_nat_Suc)
also have "\<dots> = (\<Sum>n. ereal e * ((1 / 2) ^ Suc n))"
unfolding times_ereal.simps[symmetric] ereal_power[symmetric] one_ereal_def numeral_eq_ereal
by simp
--- a/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy Wed Sep 30 17:09:12 2015 +0100
+++ b/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy Wed Sep 30 17:17:53 2015 +0100
@@ -471,7 +471,7 @@
using entropy_le_card[of "t\<circ>OB", OF simple_distributedI[OF simple_function_finite refl]] by simp
also have "\<dots> \<le> log b (real (n + 1)^card observations)"
using card_T_bound not_empty
- by (auto intro!: log_le simp: card_gt_0_iff power_real_of_nat simp del: real_of_nat_power)
+ by (auto intro!: log_le simp: card_gt_0_iff power_real_of_nat simp del: real_of_nat_power real_of_nat_Suc)
also have "\<dots> = real (card observations) * log b (real n + 1)"
by (simp add: log_nat_power real_of_nat_Suc)
finally show ?thesis .
--- a/src/HOL/Real.thy Wed Sep 30 17:09:12 2015 +0100
+++ b/src/HOL/Real.thy Wed Sep 30 17:17:53 2015 +0100
@@ -22,7 +22,7 @@
subsection \<open>Preliminary lemmas\<close>
-lemma inj_add_left [simp]:
+lemma inj_add_left [simp]:
fixes x :: "'a::cancel_semigroup_add" shows "inj (op+ x)"
by (meson add_left_imp_eq injI)
@@ -945,7 +945,7 @@
then obtain s where s: "\<forall>y\<in>X. y \<le> s" "\<And>z. \<forall>y\<in>X. y \<le> z \<Longrightarrow> s \<le> z"
using complete_real[of X] by blast
then have "Sup X = s"
- unfolding Sup_real_def by (best intro: Least_equality)
+ unfolding Sup_real_def by (best intro: Least_equality)
also from s z have "... \<le> z"
by blast
finally show "Sup X \<le> z" . }
@@ -971,7 +971,7 @@
lifting_update real.lifting
lifting_forget real.lifting
-
+
subsection\<open>More Lemmas\<close>
text \<open>BH: These lemmas should not be necessary; they should be
@@ -1010,7 +1010,7 @@
instantiation nat :: real_of
begin
-definition real_nat :: "nat \<Rightarrow> real" where real_of_nat_def [code_unfold]: "real \<equiv> of_nat"
+definition real_nat :: "nat \<Rightarrow> real" where real_of_nat_def [code_unfold]: "real \<equiv> of_nat"
instance ..
end
@@ -1018,7 +1018,7 @@
instantiation int :: real_of
begin
-definition real_int :: "int \<Rightarrow> real" where real_of_int_def [code_unfold]: "real \<equiv> of_int"
+definition real_int :: "int \<Rightarrow> real" where real_of_int_def [code_unfold]: "real \<equiv> of_int"
instance ..
end
@@ -1042,23 +1042,23 @@
lemma real_eq_of_int: "real = of_int"
unfolding real_of_int_def ..
-lemma real_of_int_zero [simp]: "real (0::int) = 0"
-by (simp add: real_of_int_def)
+lemma real_of_int_zero [simp]: "real (0::int) = 0"
+by (simp add: real_of_int_def)
lemma real_of_one [simp]: "real (1::int) = (1::real)"
-by (simp add: real_of_int_def)
+by (simp add: real_of_int_def)
lemma real_of_int_add [simp]: "real(x + y) = real (x::int) + real y"
-by (simp add: real_of_int_def)
+by (simp add: real_of_int_def)
lemma real_of_int_minus [simp]: "real(-x) = -real (x::int)"
-by (simp add: real_of_int_def)
+by (simp add: real_of_int_def)
lemma real_of_int_diff [simp]: "real(x - y) = real (x::int) - real y"
-by (simp add: real_of_int_def)
+by (simp add: real_of_int_def)
lemma real_of_int_mult [simp]: "real(x * y) = real (x::int) * real y"
-by (simp add: real_of_int_def)
+by (simp add: real_of_int_def)
lemma real_of_int_power [simp]: "real (x ^ n) = real (x::int) ^ n"
by (simp add: real_of_int_def of_int_power)
@@ -1070,31 +1070,31 @@
apply (rule of_int_setsum)
done
-lemma real_of_int_setprod [simp]: "real ((PROD x:A. f x)::int) =
+lemma real_of_int_setprod [simp]: "real ((PROD x:A. f x)::int) =
(PROD x:A. real(f x))"
apply (subst real_eq_of_int)+
apply (rule of_int_setprod)
done
lemma real_of_int_zero_cancel [simp, algebra, presburger]: "(real x = 0) = (x = (0::int))"
-by (simp add: real_of_int_def)
+by (simp add: real_of_int_def)
lemma real_of_int_inject [iff, algebra, presburger]: "(real (x::int) = real y) = (x = y)"
-by (simp add: real_of_int_def)
+by (simp add: real_of_int_def)
lemma real_of_int_less_iff [iff, presburger]: "(real (x::int) < real y) = (x < y)"
-by (simp add: real_of_int_def)
+by (simp add: real_of_int_def)
lemma real_of_int_le_iff [simp, presburger]: "(real (x::int) \<le> real y) = (x \<le> y)"
-by (simp add: real_of_int_def)
+by (simp add: real_of_int_def)
lemma real_of_int_gt_zero_cancel_iff [simp, presburger]: "(0 < real (n::int)) = (0 < n)"
-by (simp add: real_of_int_def)
+by (simp add: real_of_int_def)
lemma real_of_int_ge_zero_cancel_iff [simp, presburger]: "(0 <= real (n::int)) = (0 <= n)"
-by (simp add: real_of_int_def)
+by (simp add: real_of_int_def)
-lemma real_of_int_lt_zero_cancel_iff [simp, presburger]: "(real (n::int) < 0) = (n < 0)"
+lemma real_of_int_lt_zero_cancel_iff [simp, presburger]: "(real (n::int) < 0) = (n < 0)"
by (simp add: real_of_int_def)
lemma real_of_int_le_zero_cancel_iff [simp, presburger]: "(real (n::int) <= 0) = (n <= 0)"
@@ -1127,7 +1127,7 @@
apply simp
done
-lemma real_of_int_div_aux: "(real (x::int)) / (real d) =
+lemma real_of_int_div_aux: "(real (x::int)) / (real d) =
real (x div d) + (real (x mod d)) / (real d)"
proof -
have "x = (x div d) * d + x mod d"
@@ -1167,7 +1167,7 @@
apply (auto simp add: divide_le_eq intro: order_less_imp_le)
done
-lemma real_of_int_div4: "real (n div x) <= real (n::int) / real x"
+lemma real_of_int_div4: "real (n div x) <= real (n::int) / real x"
by (insert real_of_int_div2 [of n x], simp)
lemma Ints_real_of_int [simp]: "real (x::int) \<in> \<int>"
@@ -1188,11 +1188,10 @@
lemma real_of_nat_add [simp]: "real (m + n) = real (m::nat) + real n"
by (simp add: real_of_nat_def)
-(*Not for addsimps: often the LHS is used to represent a positive natural*)
-lemma real_of_nat_Suc: "real (Suc n) = real n + (1::real)"
+lemma real_of_nat_Suc [simp]: "real (Suc n) = real n + (1::real)"
by (simp add: real_of_nat_def)
-lemma real_of_nat_less_iff [iff]:
+lemma real_of_nat_less_iff [iff]:
"(real (n::nat) < real m) = (n < m)"
by (simp add: real_of_nat_def)
@@ -1213,13 +1212,13 @@
lemmas power_real_of_nat = real_of_nat_power [symmetric]
-lemma real_of_nat_setsum [simp]: "real ((SUM x:A. f x)::nat) =
+lemma real_of_nat_setsum [simp]: "real ((SUM x:A. f x)::nat) =
(SUM x:A. real(f x))"
apply (subst real_eq_of_nat)+
apply (rule of_nat_setsum)
done
-lemma real_of_nat_setprod [simp]: "real ((PROD x:A. f x)::nat) =
+lemma real_of_nat_setprod [simp]: "real ((PROD x:A. f x)::nat) =
(PROD x:A. real(f x))"
apply (subst real_eq_of_nat)+
apply (rule of_nat_setprod)
@@ -1250,18 +1249,12 @@
by (simp add: add: real_of_nat_def)
lemma nat_less_real_le: "((n::nat) < m) = (real n + 1 <= real m)"
- apply (subgoal_tac "real n + 1 = real (Suc n)")
- apply simp
- apply (auto simp add: real_of_nat_Suc)
-done
+by (metis discrete real_of_nat_1 real_of_nat_add real_of_nat_le_iff)
lemma nat_le_real_less: "((n::nat) <= m) = (real n < real m + 1)"
- apply (subgoal_tac "real m + 1 = real (Suc m)")
- apply (simp add: less_Suc_eq_le)
- apply (simp add: real_of_nat_Suc)
-done
+ by (meson nat_less_real_le not_le)
-lemma real_of_nat_div_aux: "(real (x::nat)) / (real d) =
+lemma real_of_nat_div_aux: "(real (x::nat)) / (real d) =
real (x div d) + (real (x mod d)) / (real d)"
proof -
have "x = (x div d) * d + x mod d"
@@ -1295,7 +1288,7 @@
apply simp
done
-lemma real_of_nat_div4: "real (n div x) <= real (n::nat) / real x"
+lemma real_of_nat_div4: "real (n div x) <= real (n::nat) / real x"
by (insert real_of_nat_div2 [of n x], simp)
lemma real_of_int_of_nat_eq [simp]: "real (of_nat n :: int) = real n"
@@ -1399,7 +1392,7 @@
by (rule dvd_mult_div_cancel)
from \<open>n \<noteq> 0\<close> and gcd_l
have "?gcd * ?l \<noteq> 0" by simp
- then have "?l \<noteq> 0" by (blast dest!: mult_not_zero)
+ then have "?l \<noteq> 0" by (blast dest!: mult_not_zero)
moreover
have "\<bar>x\<bar> = real ?k / real ?l"
proof -
@@ -1432,8 +1425,8 @@
assumes "x < y" shows "\<exists>r\<in>\<rat>. x < r \<and> r < y"
proof -
from \<open>x<y\<close> have "0 < y-x" by simp
- with reals_Archimedean obtain q::nat
- where q: "inverse (real q) < y-x" and "0 < q" by auto
+ with reals_Archimedean obtain q::nat
+ where q: "inverse (real q) < y-x" and "0 < q" by blast
def p \<equiv> "ceiling (y * real q) - 1"
def r \<equiv> "of_int p / real q"
from q have "x < y - inverse (real q)" by simp
@@ -1493,7 +1486,7 @@
subsection\<open>Simprules combining x+y and 0: ARE THEY NEEDED?\<close>
-lemma real_add_minus_iff [simp]: "(x + - a = (0::real)) = (x=a)"
+lemma real_add_minus_iff [simp]: "(x + - a = (0::real)) = (x=a)"
by arith
text \<open>FIXME: redundant with @{text add_eq_0_iff} below\<close>
@@ -1649,7 +1642,7 @@
lemma abs_add_one_not_less_self: "~ abs(x) + (1::real) < x"
by simp
-
+
lemma abs_sum_triangle_ineq: "abs ((x::real) + y + (-l + -m)) \<le> abs(x + -l) + abs(y + -m)"
by simp
@@ -2017,7 +2010,7 @@
lemma real_inverse_code [code]: "inverse (Ratreal x) = Ratreal (inverse x)"
by (simp add: of_rat_inverse)
-
+
lemma real_divide_code [code]: "Ratreal x / Ratreal y = Ratreal (x / y)"
by (simp add: of_rat_divide)
--- a/src/HOL/Transcendental.thy Wed Sep 30 17:09:12 2015 +0100
+++ b/src/HOL/Transcendental.thy Wed Sep 30 17:17:53 2015 +0100
@@ -870,7 +870,7 @@
from DERIV_D[OF DERIV_f[where n=n], THEN LIM_D, OF \<open>0 < ?r\<close>, unfolded real_norm_def]
obtain s where s_bound: "0 < s \<and> (\<forall>x. x \<noteq> 0 \<and> \<bar>x\<bar> < s \<longrightarrow> \<bar>?diff n x - f' x0 n\<bar> < ?r)"
by auto
- have "0 < ?s n" by (rule someI2[where a=s]) (auto simp add: s_bound)
+ have "0 < ?s n" by (rule someI2[where a=s]) (auto simp add: s_bound simp del: real_of_nat_Suc)
thus "0 < x" unfolding \<open>x = ?s n\<close> .
qed
qed auto
@@ -930,7 +930,7 @@
by (rule setsum_constant)
also have "\<dots> = real ?N * ?r"
unfolding real_eq_of_nat by auto
- also have "\<dots> = r/3" by auto
+ also have "\<dots> = r/3" by (auto simp del: real_of_nat_Suc)
finally have "\<bar>\<Sum>n<?N. ?diff n x - f' x0 n \<bar> < r / 3" (is "?diff_part < r / 3") .
from suminf_diff[OF allf_summable[OF x_in_I] allf_summable[OF x0_in_I]]
@@ -1042,7 +1042,7 @@
by (rule mult_left_mono) auto
show "norm (f n * x^n) \<le> norm (f n * real (Suc n) * x^n)"
unfolding real_norm_def abs_mult
- by (rule mult_right_mono) (auto simp add: le[unfolded mult_1_right])
+ using le mult_right_mono by fastforce
qed (rule powser_insidea[OF converges[OF \<open>R' \<in> {-R <..< R}\<close>] \<open>norm x < norm R'\<close>])
from this[THEN summable_mult2[where c=x], unfolded mult.assoc, unfolded mult.commute]
show "summable (?f x)" by auto
@@ -5110,7 +5110,7 @@
}
have "?a 1 ----> 0"
unfolding tendsto_rabs_zero_iff power_one divide_inverse One_nat_def
- by (auto intro!: tendsto_mult LIMSEQ_linear LIMSEQ_inverse_real_of_nat)
+ by (auto intro!: tendsto_mult LIMSEQ_linear LIMSEQ_inverse_real_of_nat simp del: real_of_nat_Suc)
have "?diff 1 ----> 0"
proof (rule LIMSEQ_I)
fix r :: real
--- a/src/Pure/GUI/system_dialog.scala Wed Sep 30 17:09:12 2015 +0100
+++ b/src/Pure/GUI/system_dialog.scala Wed Sep 30 17:17:53 2015 +0100
@@ -7,16 +7,15 @@
package isabelle
-import java.awt.{GraphicsEnvironment, Point}
-import javax.swing.WindowConstants
-import java.io.{File => JFile, BufferedReader, InputStreamReader}
+import java.awt.event.{WindowEvent, WindowAdapter}
+import javax.swing.{WindowConstants, JFrame, JDialog}
import scala.swing.{ScrollPane, Button, CheckBox, FlowPanel,
BorderPanel, Frame, TextArea, Component, Label}
import scala.swing.event.ButtonClicked
-class System_Dialog extends Build.Progress
+class System_Dialog(owner: JFrame = null) extends Progress
{
/* component state -- owned by GUI thread */
@@ -35,10 +34,8 @@
_window = Some(window)
window.pack()
- val point = GraphicsEnvironment.getLocalGraphicsEnvironment().getCenterPoint()
- window.location =
- new Point(point.x - window.size.width / 2, point.y - window.size.height / 2)
- window.visible = true
+ window.setLocationRelativeTo(owner)
+ window.setVisible(true)
window
}
@@ -54,7 +51,7 @@
_window match {
case None =>
case Some(window) =>
- window.visible = false
+ window.setVisible(false)
window.dispose
_window = None
}
@@ -69,10 +66,9 @@
/* window */
- private class Window extends Frame
+ private class Window extends JDialog(owner, _title)
{
- title = _title
- peer.setIconImages(GUI.isabelle_images())
+ setIconImages(GUI.isabelle_images())
/* text */
@@ -82,7 +78,7 @@
columns = 65
rows = 24
}
- if (GUI.is_windows_laf) text.font = (new Label).font
+ text.font = (new Label).font
val scroll_text = new ScrollPane(text)
@@ -94,7 +90,7 @@
layout_panel.layout(scroll_text) = BorderPanel.Position.Center
layout_panel.layout(action_panel) = BorderPanel.Position.South
- contents = layout_panel
+ setContentPane(layout_panel.peer)
def set_actions(cs: Component*)
{
@@ -107,12 +103,14 @@
/* close */
- peer.setDefaultCloseOperation(WindowConstants.DO_NOTHING_ON_CLOSE)
+ setDefaultCloseOperation(WindowConstants.DO_NOTHING_ON_CLOSE)
- override def closeOperation {
- if (_return_code.isDefined) conclude()
- else stopping()
- }
+ addWindowListener(new WindowAdapter {
+ override def windowClosing(e: WindowEvent) {
+ if (_return_code.isDefined) conclude()
+ else stopping()
+ }
+ })
def stopping()
{
@@ -162,7 +160,7 @@
def title(txt: String): Unit =
GUI_Thread.later {
_title = txt
- _window.foreach(window => window.title = txt)
+ _window.foreach(window => window.setTitle(txt))
}
def return_code(rc: Int): Unit =
@@ -187,26 +185,4 @@
@volatile private var is_stopped = false
override def stopped: Boolean = is_stopped
-
-
- /* system operations */
-
- def execute(cwd: JFile, env: Map[String, String], args: String*): Int =
- {
- val proc = Isabelle_System.raw_execute(cwd, env, true, args: _*)
- proc.getOutputStream.close
-
- val stdout = new BufferedReader(new InputStreamReader(proc.getInputStream, UTF8.charset))
- try {
- var line = stdout.readLine
- while (line != null) {
- echo(line)
- line = stdout.readLine
- }
- }
- finally { stdout.close }
-
- proc.waitFor
- }
}
-
--- a/src/Pure/PIDE/batch_session.scala Wed Sep 30 17:09:12 2015 +0100
+++ b/src/Pure/PIDE/batch_session.scala Wed Sep 30 17:17:53 2015 +0100
@@ -24,7 +24,7 @@
val parent_session =
session_info.parent getOrElse error("No parent session for " + quote(session))
- if (Build.build(options, new Build.Console_Progress(verbose),
+ if (Build.build(options, new Console_Progress(verbose),
verbose = verbose, build_heap = true,
dirs = dirs, sessions = List(parent_session)) != 0)
new RuntimeException
@@ -36,7 +36,7 @@
new Resources(content.loaded_theories, content.known_theories, content.syntax)
}
- val progress = new Build.Console_Progress(verbose)
+ val progress = new Console_Progress(verbose)
val prover_session = new Session(resources)
val batch_session = new Batch_Session(prover_session)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/cygwin.scala Wed Sep 30 17:17:53 2015 +0100
@@ -0,0 +1,87 @@
+/* Title: Pure/Tools/cygwin.scala
+ Author: Makarius
+
+Cygwin as POSIX emulation on Windows.
+*/
+
+package isabelle
+
+
+import java.io.{File => JFile}
+import java.nio.file.Files
+
+import scala.annotation.tailrec
+
+
+object Cygwin
+{
+ /** Cygwin init (e.g. after extraction via 7zip) **/
+
+ def init()
+ {
+ val isabelle_home0 = System.getenv("ISABELLE_HOME")
+ if (isabelle_home0 == null || isabelle_home0 == "") {
+
+ /* isabelle_home */
+
+ val isabelle_home = System.getProperty("isabelle.home", "")
+
+ if (isabelle_home == "")
+ error("Unknown Isabelle home directory")
+
+ if (!(new JFile(isabelle_home)).isDirectory)
+ error("Bad Isabelle home directory: " + quote(isabelle_home))
+
+ def execute(args: String*)
+ {
+ val cwd = new JFile(isabelle_home)
+ val env = Map("CYGWIN" -> "nodosfilewarning")
+ val proc = Isabelle_System.raw_execute(cwd, env, true, args: _*)
+ val (output, rc) = Isabelle_System.process_output(proc)
+ if (rc != 0) error(output)
+ }
+
+
+ /* cygwin_root */
+
+ val cygwin_root = isabelle_home + "\\contrib\\cygwin"
+ if ((new JFile(cygwin_root)).isDirectory)
+ System.setProperty("cygwin.root", cygwin_root)
+
+
+ /* init */
+
+ val uninitialized_file = new JFile(cygwin_root, "isabelle\\uninitialized")
+ val uninitialized = uninitialized_file.isFile && uninitialized_file.delete
+
+ if (uninitialized) {
+ val symlinks =
+ {
+ val path = (new JFile(cygwin_root + "\\isabelle\\symlinks")).toPath
+ Files.readAllLines(path, UTF8.charset).toArray.toList.asInstanceOf[List[String]]
+ }
+ @tailrec def recover_symlinks(list: List[String]): Unit =
+ {
+ list match {
+ case Nil | List("") =>
+ case link :: content :: rest =>
+ val path = (new JFile(isabelle_home, link)).toPath
+
+ val writer = Files.newBufferedWriter(path, UTF8.charset)
+ try { writer.write("!<symlink>" + content + "\u0000") }
+ finally { writer.close }
+
+ Files.setAttribute(path, "dos:system", true)
+
+ recover_symlinks(rest)
+ case _ => error("Unbalanced symlinks list")
+ }
+ }
+ recover_symlinks(symlinks)
+
+ execute(cygwin_root + "\\bin\\dash.exe", "/isabelle/rebaseall")
+ execute(cygwin_root + "\\bin\\bash.exe", "/isabelle/postinstall")
+ }
+ }
+ }
+}
--- a/src/Pure/System/isabelle_system.scala Wed Sep 30 17:09:12 2015 +0100
+++ b/src/Pure/System/isabelle_system.scala Wed Sep 30 17:17:53 2015 +0100
@@ -8,10 +8,12 @@
package isabelle
-import java.io.{File => JFile, IOException}
+import java.io.{File => JFile, IOException, BufferedReader, InputStreamReader}
import java.nio.file.{Path => JPath, Files, SimpleFileVisitor, FileVisitResult}
import java.nio.file.attribute.BasicFileAttributes
+import scala.collection.mutable
+
object Isabelle_System
{
@@ -194,9 +196,10 @@
proc.start
}
- private def process_output(proc: Process): (String, Int) =
+ def process_output(proc: Process): (String, Int) =
{
proc.getOutputStream.close
+
val output = File.read_stream(proc.getInputStream)
val rc =
try { proc.waitFor }
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/progress.scala Wed Sep 30 17:17:53 2015 +0100
@@ -0,0 +1,33 @@
+/* Title: Pure/System/progress.scala
+ Author: Makarius
+
+Progress context for system processes.
+*/
+
+package isabelle
+
+
+class Progress
+{
+ def echo(msg: String) {}
+ def theory(session: String, theory: String) {}
+ def stopped: Boolean = false
+ override def toString: String = if (stopped) "Progress(stopped)" else "Progress"
+}
+
+object Ignore_Progress extends Progress
+
+class Console_Progress(verbose: Boolean = false) extends Progress
+{
+ override def echo(msg: String) { Console.println(msg) }
+ override def theory(session: String, theory: String): Unit =
+ if (verbose) echo(session + ": theory " + theory)
+
+ @volatile private var is_stopped = false
+ def interrupt_handler[A](e: => A): A = POSIX_Interrupt.handler { is_stopped = true } { e }
+ override def stopped: Boolean =
+ {
+ if (Thread.interrupted) is_stopped = true
+ is_stopped
+ }
+}
--- a/src/Pure/Tools/build.scala Wed Sep 30 17:09:12 2015 +0100
+++ b/src/Pure/Tools/build.scala Wed Sep 30 17:17:53 2015 +0100
@@ -19,35 +19,6 @@
object Build
{
- /** progress context **/
-
- class Progress
- {
- def echo(msg: String) {}
- def theory(session: String, theory: String) {}
- def stopped: Boolean = false
- override def toString: String = if (stopped) "Progress(stopped)" else "Progress"
- }
-
- object Ignore_Progress extends Progress
-
- class Console_Progress(verbose: Boolean = false) extends Progress
- {
- override def echo(msg: String) { Console.println(msg) }
- override def theory(session: String, theory: String): Unit =
- if (verbose) echo(session + ": theory " + theory)
-
- @volatile private var is_stopped = false
- def interrupt_handler[A](e: => A): A = POSIX_Interrupt.handler { is_stopped = true } { e }
- override def stopped: Boolean =
- {
- if (Thread.interrupted) is_stopped = true
- is_stopped
- }
- }
-
-
-
/** session information **/
// external version
--- a/src/Pure/Tools/build_console.scala Wed Sep 30 17:09:12 2015 +0100
+++ b/src/Pure/Tools/build_console.scala Wed Sep 30 17:17:53 2015 +0100
@@ -13,7 +13,7 @@
def build_console(
options: Options,
- progress: Build.Progress = Build.Ignore_Progress,
+ progress: Progress = Ignore_Progress,
dirs: List[Path] = Nil,
no_build: Boolean = false,
system_mode: Boolean = false,
@@ -45,7 +45,7 @@
val options = (Options.init() /: system_options)(_ + _)
File.write(Path.explode(options_file), YXML.string_of_body(options.encode))
- val progress = new Build.Console_Progress()
+ val progress = new Console_Progress()
progress.interrupt_handler {
build_console(options, progress,
dirs.map(Path.explode(_)), no_build, system_mode, session)
--- a/src/Pure/Tools/build_doc.scala Wed Sep 30 17:09:12 2015 +0100
+++ b/src/Pure/Tools/build_doc.scala Wed Sep 30 17:17:53 2015 +0100
@@ -16,7 +16,7 @@
def build_doc(
options: Options,
- progress: Build.Progress = Build.Ignore_Progress,
+ progress: Progress = Ignore_Progress,
all_docs: Boolean = false,
max_jobs: Int = 1,
system_mode: Boolean = false,
@@ -79,7 +79,7 @@
Properties.Value.Boolean(system_mode) ::
Command_Line.Chunks(docs) =>
val options = Options.init()
- val progress = new Build.Console_Progress()
+ val progress = new Console_Progress()
progress.interrupt_handler {
build_doc(options, progress, all_docs, max_jobs, system_mode, docs)
}
--- a/src/Pure/Tools/check_keywords.scala Wed Sep 30 17:09:12 2015 +0100
+++ b/src/Pure/Tools/check_keywords.scala Wed Sep 30 17:17:53 2015 +0100
@@ -32,7 +32,7 @@
}
def check_keywords(
- progress: Build.Progress,
+ progress: Progress,
keywords: Keyword.Keywords,
check: Set[String],
paths: List[Path])
--- a/src/Pure/Tools/main.scala Wed Sep 30 17:09:12 2015 +0100
+++ b/src/Pure/Tools/main.scala Wed Sep 30 17:17:53 2015 +0100
@@ -8,218 +8,82 @@
import java.lang.{Class, ClassLoader}
-import java.io.{File => JFile, BufferedReader, InputStreamReader}
-import java.nio.file.Files
-
-import scala.annotation.tailrec
object Main
{
- /** main entry point **/
+ /* main entry point */
def main(args: Array[String])
{
- val system_dialog = new System_Dialog
-
- def exit_error(exn: Throwable): Nothing =
- {
- GUI.dialog(null, "Isabelle", GUI.scrollable_text(Exn.message(exn)))
- system_dialog.return_code(Exn.return_code(exn, 2))
- system_dialog.join_exit
- }
-
- def build()
+ val start =
{
try {
- GUI.init_laf()
+ /* system init */
+
+ if (Platform.is_windows) Cygwin.init()
+
Isabelle_System.init()
- val mode = Isabelle_System.getenv("JEDIT_BUILD_MODE")
- if (mode == "none")
- system_dialog.return_code(0)
- else {
- val options = Options.init()
- val system_mode = mode == "" || mode == "system"
- val dirs = Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS"))
- val session = Isabelle_System.default_logic(
- Isabelle_System.getenv("JEDIT_LOGIC"),
- options.string("jedit_logic"))
+
+ /* settings directory */
- if (Build.build(options = options, build_heap = true, no_build = true,
- dirs = dirs, system_mode = system_mode, sessions = List(session)) == 0)
- system_dialog.return_code(0)
- else {
- system_dialog.title("Isabelle build (" +
- Isabelle_System.getenv("ML_IDENTIFIER") + " / " +
- "jdk-" + Platform.jvm_version + "_" + Platform.jvm_platform + ")")
- system_dialog.echo("Build started for Isabelle/" + session + " ...")
+ val settings_dir = Path.explode("$JEDIT_SETTINGS")
+ Isabelle_System.mkdirs(settings_dir + Path.explode("DockableWindowManager"))
- val (out, rc) =
- try {
- ("",
- Build.build(options = options, progress = system_dialog, build_heap = true,
- dirs = dirs, system_mode = system_mode, sessions = List(session)))
- }
- catch {
- case exn: Throwable =>
- (Output.error_text(Exn.message(exn)) + "\n", Exn.return_code(exn, 2))
- }
-
- system_dialog.echo(out + (if (rc == 0) "OK\n" else "Return code: " + rc + "\n"))
- system_dialog.return_code(rc)
- }
- }
- }
- catch { case exn: Throwable => exit_error(exn) }
- }
-
- def start()
- {
- val do_start =
- {
- try {
- /* settings directory */
-
- val settings_dir = Path.explode("$JEDIT_SETTINGS")
- Isabelle_System.mkdirs(settings_dir + Path.explode("DockableWindowManager"))
-
- if (!(settings_dir + Path.explode("perspective.xml")).is_file) {
- File.write(settings_dir + Path.explode("DockableWindowManager/perspective-view0.xml"),
- """<DOCKING LEFT="" TOP="" RIGHT="isabelle-documentation" BOTTOM="" LEFT_POS="0" TOP_POS="0" RIGHT_POS="250" BOTTOM_POS="250" />""")
- File.write(settings_dir + Path.explode("perspective.xml"),
- """<?xml version="1.0" encoding="UTF-8" ?>
+ if (!(settings_dir + Path.explode("perspective.xml")).is_file) {
+ File.write(settings_dir + Path.explode("DockableWindowManager/perspective-view0.xml"),
+ """<DOCKING LEFT="" TOP="" RIGHT="isabelle-documentation" BOTTOM="" LEFT_POS="0" TOP_POS="0" RIGHT_POS="250" BOTTOM_POS="250" />""")
+ File.write(settings_dir + Path.explode("perspective.xml"),
+ """<?xml version="1.0" encoding="UTF-8" ?>
<!DOCTYPE PERSPECTIVE SYSTEM "perspective.dtd">
<PERSPECTIVE>
<VIEW PLAIN="FALSE">
<GEOMETRY X="0" Y="35" WIDTH="1072" HEIGHT="787" EXT_STATE="0" />
</VIEW>
</PERSPECTIVE>""")
- }
+ }
- /* args */
+ /* args */
- val jedit_options =
- Isabelle_System.getenv_strict("JEDIT_OPTIONS").split(" +")
+ val jedit_options =
+ Isabelle_System.getenv_strict("JEDIT_OPTIONS").split(" +")
- val jedit_settings =
- Array("-settings=" + File.platform_path(Path.explode("$JEDIT_SETTINGS")))
+ val jedit_settings =
+ Array("-settings=" + File.platform_path(Path.explode("$JEDIT_SETTINGS")))
- val more_args =
- if (args.isEmpty)
- Array(File.platform_path(Path.explode("$USER_HOME/Scratch.thy")))
- else args
+ val more_args =
+ if (args.isEmpty)
+ Array(File.platform_path(Path.explode("$USER_HOME/Scratch.thy")))
+ else args
- /* startup */
-
- update_environment()
-
- System.setProperty("jedit.home", File.platform_path(Path.explode("$JEDIT_HOME/dist")))
- System.setProperty("scala.home", File.platform_path(Path.explode("$SCALA_HOME")))
-
- val jedit =
- Class.forName("org.gjt.sp.jedit.jEdit", true, ClassLoader.getSystemClassLoader)
- val jedit_main = jedit.getMethod("main", classOf[Array[String]])
+ /* main startup */
- () => jedit_main.invoke(null, jedit_options ++ jedit_settings ++ more_args)
- }
- catch { case exn: Throwable => exit_error(exn) }
- }
- do_start()
- }
+ update_environment()
- if (Platform.is_windows) {
- try {
- GUI.init_laf()
+ System.setProperty("jedit.home", File.platform_path(Path.explode("$JEDIT_HOME/dist")))
+ System.setProperty("scala.home", File.platform_path(Path.explode("$SCALA_HOME")))
- val isabelle_home0 = System.getenv("ISABELLE_HOME")
- val isabelle_home = System.getProperty("isabelle.home")
-
- if (isabelle_home0 == null || isabelle_home0 == "") {
- if (isabelle_home == null || isabelle_home == "")
- error("Unknown Isabelle home directory")
- if (!(new JFile(isabelle_home)).isDirectory)
- error("Bad Isabelle home directory: " + quote(isabelle_home))
+ val jedit =
+ Class.forName("org.gjt.sp.jedit.jEdit", true, ClassLoader.getSystemClassLoader)
+ val jedit_main = jedit.getMethod("main", classOf[Array[String]])
- val cygwin_root = isabelle_home + "\\contrib\\cygwin"
- if ((new JFile(cygwin_root)).isDirectory)
- System.setProperty("cygwin.root", cygwin_root)
-
- val uninitialized_file = new JFile(cygwin_root, "isabelle\\uninitialized")
- val uninitialized = uninitialized_file.isFile && uninitialized_file.delete
-
- if (uninitialized) cygwin_init(system_dialog, isabelle_home, cygwin_root)
- }
+ () => jedit_main.invoke(null, jedit_options ++ jedit_settings ++ more_args)
}
- catch { case exn: Throwable => exit_error(exn) }
-
- if (system_dialog.stopped) {
- system_dialog.return_code(Exn.Interrupt.return_code)
- system_dialog.join_exit
+ catch {
+ case exn: Throwable =>
+ GUI.init_laf()
+ GUI.dialog(null, "Isabelle", GUI.scrollable_text(Exn.message(exn)))
+ sys.exit(2)
}
}
-
- build()
- val rc = system_dialog.join
- if (rc == 0) start() else sys.exit(rc)
+ start()
}
-
- /** Cygwin init (e.g. after extraction via 7zip) **/
-
- private def cygwin_init(system_dialog: System_Dialog, isabelle_home: String, cygwin_root: String)
- {
- system_dialog.title("Isabelle system initialization")
- system_dialog.echo("Initializing Cygwin ...")
-
- def execute(args: String*): Int =
- {
- val cwd = new JFile(isabelle_home)
- val env = Map("CYGWIN" -> "nodosfilewarning")
- system_dialog.execute(cwd, env, args: _*)
- }
-
- system_dialog.echo("symlinks ...")
- val symlinks =
- {
- val path = (new JFile(cygwin_root + "\\isabelle\\symlinks")).toPath
- Files.readAllLines(path, UTF8.charset).toArray.toList.asInstanceOf[List[String]]
- }
- @tailrec def recover_symlinks(list: List[String]): Unit =
- {
- list match {
- case Nil | List("") =>
- case link :: content :: rest =>
- val path = (new JFile(isabelle_home, link)).toPath
-
- val writer = Files.newBufferedWriter(path, UTF8.charset)
- try { writer.write("!<symlink>" + content + "\u0000") }
- finally { writer.close }
-
- Files.setAttribute(path, "dos:system", true)
-
- recover_symlinks(rest)
- case _ => error("Unbalanced symlinks list")
- }
- }
- recover_symlinks(symlinks)
-
- system_dialog.echo("rebaseall ...")
- execute(cygwin_root + "\\bin\\dash.exe", "/isabelle/rebaseall")
-
- system_dialog.echo("postinstall ...")
- execute(cygwin_root + "\\bin\\bash.exe", "/isabelle/postinstall")
-
- system_dialog.echo("init ...")
- Isabelle_System.init()
- }
-
-
-
- /** adhoc update of JVM environment variables **/
+ /* adhoc update of JVM environment variables */
def update_environment()
{
@@ -255,4 +119,3 @@
}
}
}
-
--- a/src/Pure/build-jars Wed Sep 30 17:09:12 2015 +0100
+++ b/src/Pure/build-jars Wed Sep 30 17:17:53 2015 +0100
@@ -74,6 +74,7 @@
PIDE/xml.scala
PIDE/yxml.scala
ROOT.scala
+ System/cygwin.scala
System/command_line.scala
System/invoke_scala.scala
System/isabelle_charset.scala
@@ -82,6 +83,7 @@
System/options.scala
System/platform.scala
System/posix_interrupt.scala
+ System/progress.scala
System/system_channel.scala
System/utf8.scala
Thy/html.scala
--- a/src/Tools/jEdit/src/plugin.scala Wed Sep 30 17:09:12 2015 +0100
+++ b/src/Tools/jEdit/src/plugin.scala Wed Sep 30 17:17:53 2015 +0100
@@ -262,6 +262,59 @@
}
+ /* session build */
+
+ def session_build(): Int =
+ {
+ val system_dialog = new System_Dialog(jEdit.getActiveView())
+
+ try {
+ val mode = Isabelle_System.getenv("JEDIT_BUILD_MODE")
+ if (mode == "none")
+ system_dialog.return_code(0)
+ else {
+ val system_mode = mode == "" || mode == "system"
+ val dirs = Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS"))
+ val session = Isabelle_System.default_logic(
+ Isabelle_System.getenv("JEDIT_LOGIC"),
+ PIDE.options.string("jedit_logic"))
+
+ if (Build.build(options = PIDE.options.value, build_heap = true, no_build = true,
+ dirs = dirs, system_mode = system_mode, sessions = List(session)) == 0)
+ system_dialog.return_code(0)
+ else {
+ system_dialog.title("Isabelle build (" +
+ Isabelle_System.getenv("ML_IDENTIFIER") + " / " +
+ "jdk-" + Platform.jvm_version + "_" + Platform.jvm_platform + ")")
+ system_dialog.echo("Build started for Isabelle/" + session + " ...")
+
+ val (out, rc) =
+ try {
+ ("",
+ Build.build(options = PIDE.options.value, progress = system_dialog,
+ build_heap = true, dirs = dirs, system_mode = system_mode,
+ sessions = List(session)))
+ }
+ catch {
+ case exn: Throwable =>
+ (Output.error_text(Exn.message(exn)) + "\n", Exn.return_code(exn, 2))
+ }
+
+ system_dialog.echo(out + (if (rc == 0) "OK\n" else "Return code: " + rc + "\n"))
+ system_dialog.return_code(rc)
+ }
+ }
+ }
+ catch {
+ case exn: Throwable =>
+ GUI.dialog(null, "Isabelle", GUI.scrollable_text(Exn.message(exn)))
+ system_dialog.return_code(Exn.return_code(exn, 2))
+ }
+
+ system_dialog.join()
+ }
+
+
/* session phase */
private val session_phase =
@@ -320,14 +373,17 @@
if (PIDE.startup_failure.isEmpty) {
message match {
case msg: EditorStarted =>
- PIDE.session.start("Isabelle", Isabelle_Logic.session_args())
-
if (Distribution.is_identified && !Distribution.is_official) {
GUI.warning_dialog(jEdit.getActiveView, "Isabelle version for testing",
"This is " + Distribution.version + ".",
"It is for testing only, not for production use.")
}
+ Simple_Thread.fork("session_build") {
+ val rc = session_build()
+ if (rc == 0) PIDE.session.start("Isabelle", Isabelle_Logic.session_args())
+ }
+
case msg: BufferUpdate
if msg.getWhat == BufferUpdate.LOADED ||
msg.getWhat == BufferUpdate.PROPERTIES_CHANGED ||
@@ -384,7 +440,6 @@
Debug.DISABLE_SEARCH_DIALOG_POOL = true
PIDE.plugin = this
- Isabelle_System.init()
GUI.install_fonts()
PIDE.options.update(Options.init())