# HG changeset patch
# User wenzelm
# Date 1519161923 -3600
# Node ID 00c43648839802ef0899ecd019427a0e6d7ac719
# Parent  b5058ba95e32133e449fcb86b2bfdf86d5e5fc09
tuned proofs -- prefer explicit names for facts from 'interpret';

diff -r b5058ba95e32 -r 00c436488398 src/HOL/Analysis/Brouwer_Fixpoint.thy
--- 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] ..
diff -r b5058ba95e32 -r 00c436488398 src/HOL/Analysis/Caratheodory.thy
--- 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
diff -r b5058ba95e32 -r 00c436488398 src/HOL/Analysis/Derivative.thy
--- 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)"
diff -r b5058ba95e32 -r 00c436488398 src/HOL/HOLCF/ConvexPD.thy
--- 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)
diff -r b5058ba95e32 -r 00c436488398 src/HOL/HOLCF/LowerPD.thy
--- 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)
diff -r b5058ba95e32 -r 00c436488398 src/HOL/HOLCF/Map_Functions.thy
--- 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)
diff -r b5058ba95e32 -r 00c436488398 src/HOL/HOLCF/UpperPD.thy
--- 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)
diff -r b5058ba95e32 -r 00c436488398 src/HOL/Library/RBT_Set.thy
--- 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
 
diff -r b5058ba95e32 -r 00c436488398 src/HOL/Probability/Levy.thy
--- 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"