--- a/src/HOL/Analysis/Brouwer_Fixpoint.thy Tue Feb 20 22:04:04 2018 +0100
+++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy Tue Feb 20 22:25:23 2018 +0100
@@ -941,8 +941,8 @@
for i j
interpret b: kuhn_simplex p n base ?upd "f' ` {.. n}"
proof
- show "base \<in> {..<n} \<rightarrow> {..<p}" by fact
- { fix i assume "n \<le> i" then show "base i = p" by fact }
+ show "base \<in> {..<n} \<rightarrow> {..<p}" by (rule base)
+ { fix i assume "n \<le> i" then show "base i = p" by (rule base_out) }
show "bij_betw ?upd {..<n} {..<n}" by fact
qed (simp add: f'_def)
have f': "b.enum = f'" unfolding f'_def b.enum_def[abs_def] ..
--- a/src/HOL/Analysis/Caratheodory.thy Tue Feb 20 22:04:04 2018 +0100
+++ b/src/HOL/Analysis/Caratheodory.thy Tue Feb 20 22:25:23 2018 +0100
@@ -854,7 +854,7 @@
{ fix i assume "i \<in> I" then show "\<mu>' (G i) = \<mu> i"
using \<mu>' by (auto intro!: inj sel) }
show "G ` I \<subseteq> Pow \<Omega>"
- by fact
+ by (rule space_closed)
then show "positive (sets M) \<mu>'" "countably_additive (sets M) \<mu>'"
using \<mu>' by (simp_all add: M sets_extend_measure measure_space_def)
qed fact
--- a/src/HOL/Analysis/Derivative.thy Tue Feb 20 22:04:04 2018 +0100
+++ b/src/HOL/Analysis/Derivative.thy Tue Feb 20 22:25:23 2018 +0100
@@ -1088,7 +1088,7 @@
interpret bounded_linear "(f' ?u)"
using u by (auto intro!: has_derivative_bounded_linear assms(2)[rule_format] *)
have "norm (f' ?u (y - x)) \<le> onorm (f' ?u) * norm (y - x)"
- by (rule onorm) fact
+ by (rule onorm) (rule bounded_linear)
also have "onorm (f' ?u) \<le> B"
using u by (auto intro!: assms(3)[rule_format] *)
finally have "norm ((f' ?u) (y - x)) \<le> B * norm (x - y)"
--- a/src/HOL/HOLCF/ConvexPD.thy Tue Feb 20 22:04:04 2018 +0100
+++ b/src/HOL/HOLCF/ConvexPD.thy Tue Feb 20 22:25:23 2018 +0100
@@ -430,8 +430,8 @@
assumes "finite_deflation d" shows "finite_deflation (convex_map\<cdot>d)"
proof (rule finite_deflation_intro)
interpret d: finite_deflation d by fact
- have "deflation d" by fact
- thus "deflation (convex_map\<cdot>d)" by (rule deflation_convex_map)
+ from d.deflation_axioms show "deflation (convex_map\<cdot>d)"
+ by (rule deflation_convex_map)
have "finite (range (\<lambda>x. d\<cdot>x))" by (rule d.finite_range)
hence "finite (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x))"
by (rule finite_vimageI, simp add: inj_on_def Rep_compact_basis_inject)
--- a/src/HOL/HOLCF/LowerPD.thy Tue Feb 20 22:04:04 2018 +0100
+++ b/src/HOL/HOLCF/LowerPD.thy Tue Feb 20 22:25:23 2018 +0100
@@ -423,8 +423,8 @@
assumes "finite_deflation d" shows "finite_deflation (lower_map\<cdot>d)"
proof (rule finite_deflation_intro)
interpret d: finite_deflation d by fact
- have "deflation d" by fact
- thus "deflation (lower_map\<cdot>d)" by (rule deflation_lower_map)
+ from d.deflation_axioms show "deflation (lower_map\<cdot>d)"
+ by (rule deflation_lower_map)
have "finite (range (\<lambda>x. d\<cdot>x))" by (rule d.finite_range)
hence "finite (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x))"
by (rule finite_vimageI, simp add: inj_on_def Rep_compact_basis_inject)
--- a/src/HOL/HOLCF/Map_Functions.thy Tue Feb 20 22:04:04 2018 +0100
+++ b/src/HOL/HOLCF/Map_Functions.thy Tue Feb 20 22:25:23 2018 +0100
@@ -92,8 +92,7 @@
proof (rule finite_deflation_intro)
interpret d1: finite_deflation d1 by fact
interpret d2: finite_deflation d2 by fact
- have "deflation d1" and "deflation d2" by fact+
- then show "deflation (cfun_map\<cdot>d1\<cdot>d2)"
+ from d1.deflation_axioms d2.deflation_axioms show "deflation (cfun_map\<cdot>d1\<cdot>d2)"
by (rule deflation_cfun_map)
have "finite (range (\<lambda>f. cfun_map\<cdot>d1\<cdot>d2\<cdot>f))"
using d1.finite_range d2.finite_range
@@ -158,8 +157,8 @@
proof (rule finite_deflation_intro)
interpret d1: finite_deflation d1 by fact
interpret d2: finite_deflation d2 by fact
- have "deflation d1" and "deflation d2" by fact+
- then show "deflation (prod_map\<cdot>d1\<cdot>d2)" by (rule deflation_prod_map)
+ from d1.deflation_axioms d2.deflation_axioms show "deflation (prod_map\<cdot>d1\<cdot>d2)"
+ by (rule deflation_prod_map)
have "{p. prod_map\<cdot>d1\<cdot>d2\<cdot>p = p} \<subseteq> {x. d1\<cdot>x = x} \<times> {y. d2\<cdot>y = y}"
by auto
then show "finite {p. prod_map\<cdot>d1\<cdot>d2\<cdot>p = p}"
@@ -204,8 +203,7 @@
shows "finite_deflation (u_map\<cdot>d)"
proof (rule finite_deflation_intro)
interpret d: finite_deflation d by fact
- have "deflation d" by fact
- then show "deflation (u_map\<cdot>d)"
+ from d.deflation_axioms show "deflation (u_map\<cdot>d)"
by (rule deflation_u_map)
have "{x. u_map\<cdot>d\<cdot>x = x} \<subseteq> insert \<bottom> ((\<lambda>x. up\<cdot>x) ` {x. d\<cdot>x = x})"
by (rule subsetI, case_tac x, simp_all)
@@ -284,8 +282,7 @@
proof (rule finite_deflation_intro)
interpret d1: finite_deflation d1 by fact
interpret d2: finite_deflation d2 by fact
- have "deflation d1" and "deflation d2" by fact+
- then show "deflation (sprod_map\<cdot>d1\<cdot>d2)"
+ from d1.deflation_axioms d2.deflation_axioms show "deflation (sprod_map\<cdot>d1\<cdot>d2)"
by (rule deflation_sprod_map)
have "{x. sprod_map\<cdot>d1\<cdot>d2\<cdot>x = x} \<subseteq>
insert \<bottom> ((\<lambda>(x, y). (:x, y:)) ` ({x. d1\<cdot>x = x} \<times> {y. d2\<cdot>y = y}))"
@@ -369,8 +366,7 @@
proof (rule finite_deflation_intro)
interpret d1: finite_deflation d1 by fact
interpret d2: finite_deflation d2 by fact
- have "deflation d1" and "deflation d2" by fact+
- then show "deflation (ssum_map\<cdot>d1\<cdot>d2)"
+ from d1.deflation_axioms d2.deflation_axioms show "deflation (ssum_map\<cdot>d1\<cdot>d2)"
by (rule deflation_ssum_map)
have "{x. ssum_map\<cdot>d1\<cdot>d2\<cdot>x = x} \<subseteq>
(\<lambda>x. sinl\<cdot>x) ` {x. d1\<cdot>x = x} \<union>
@@ -442,8 +438,7 @@
proof (intro finite_deflation_intro)
interpret d1: finite_deflation d1 by fact
interpret d2: finite_deflation d2 by fact
- have "deflation d1" and "deflation d2" by fact+
- then show "deflation (sfun_map\<cdot>d1\<cdot>d2)"
+ from d1.deflation_axioms d2.deflation_axioms show "deflation (sfun_map\<cdot>d1\<cdot>d2)"
by (rule deflation_sfun_map)
from assms have "finite_deflation (cfun_map\<cdot>d1\<cdot>d2)"
by (rule finite_deflation_cfun_map)
--- a/src/HOL/HOLCF/UpperPD.thy Tue Feb 20 22:04:04 2018 +0100
+++ b/src/HOL/HOLCF/UpperPD.thy Tue Feb 20 22:25:23 2018 +0100
@@ -416,8 +416,8 @@
assumes "finite_deflation d" shows "finite_deflation (upper_map\<cdot>d)"
proof (rule finite_deflation_intro)
interpret d: finite_deflation d by fact
- have "deflation d" by fact
- thus "deflation (upper_map\<cdot>d)" by (rule deflation_upper_map)
+ from d.deflation_axioms show "deflation (upper_map\<cdot>d)"
+ by (rule deflation_upper_map)
have "finite (range (\<lambda>x. d\<cdot>x))" by (rule d.finite_range)
hence "finite (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x))"
by (rule finite_vimageI, simp add: inj_on_def Rep_compact_basis_inject)
--- a/src/HOL/Library/RBT_Set.thy Tue Feb 20 22:04:04 2018 +0100
+++ b/src/HOL/Library/RBT_Set.thy Tue Feb 20 22:25:23 2018 +0100
@@ -474,7 +474,7 @@
proof -
interpret comp_fun_idem Set.insert
by (fact comp_fun_idem_insert)
- from finite_fold_fold_keys[OF \<open>comp_fun_commute Set.insert\<close>]
+ from finite_fold_fold_keys[OF comp_fun_commute_axioms]
show ?thesis by (auto simp add: union_fold_insert)
qed
@@ -487,7 +487,7 @@
proof -
interpret comp_fun_idem Set.remove
by (fact comp_fun_idem_remove)
- from finite_fold_fold_keys[OF \<open>comp_fun_commute Set.remove\<close>]
+ from finite_fold_fold_keys[OF comp_fun_commute_axioms]
show ?thesis by (auto simp add: minus_fold_remove)
qed
--- a/src/HOL/Probability/Levy.thy Tue Feb 20 22:04:04 2018 +0100
+++ b/src/HOL/Probability/Levy.thy Tue Feb 20 22:25:23 2018 +0100
@@ -219,7 +219,7 @@
{ fix \<epsilon> :: real
assume "\<epsilon> > 0"
have "(?D \<longlongrightarrow> 0) at_bot"
- using \<open>(cdf M1 \<longlongrightarrow> 0) at_bot\<close> \<open>(cdf M2 \<longlongrightarrow> 0) at_bot\<close> by (intro tendsto_eq_intros) auto
+ using M1.cdf_lim_at_bot M2.cdf_lim_at_bot by (intro tendsto_eq_intros) auto
then have "eventually (\<lambda>y. ?D y < \<epsilon> / 2 \<and> y \<le> x) at_bot"
using \<open>\<epsilon> > 0\<close> by (simp only: tendsto_iff dist_real_def diff_0_right eventually_conj eventually_le_at_bot abs_idempotent)
then obtain M where "\<And>y. y \<le> M \<Longrightarrow> ?D y < \<epsilon> / 2" "M \<le> x"