--- a/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy Mon Jan 14 14:19:00 2019 +0000
+++ b/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy Mon Jan 14 16:47:29 2019 +0100
@@ -900,10 +900,6 @@
"(\<And>x. x \<in> space M =simp=> u x = v x) \<Longrightarrow> integral\<^sup>N M u = integral\<^sup>N M v"
by (auto intro: nn_integral_cong simp: simp_implies_def)
-lemma nn_integral_cong_strong:
- "M = N \<Longrightarrow> (\<And>x. x \<in> space M \<Longrightarrow> u x = v x) \<Longrightarrow> integral\<^sup>N M u = integral\<^sup>N N v"
- by (auto intro: nn_integral_cong)
-
lemma incseq_nn_integral:
assumes "incseq f" shows "incseq (\<lambda>i. integral\<^sup>N M (f i))"
proof -
--- a/src/HOL/Analysis/Tagged_Division.thy Mon Jan 14 14:19:00 2019 +0000
+++ b/src/HOL/Analysis/Tagged_Division.thy Mon Jan 14 16:47:29 2019 +0100
@@ -4,7 +4,7 @@
*)
section \<open>Tagged Divisions for Henstock-Kurzweil Integration\<close>
-(*FIXME move together with Henstock_Kurzweil_Integration.thy *)
+
theory Tagged_Division
imports Topology_Euclidean_Space
begin
--- a/src/HOL/Data_Structures/Array_Braun.thy Mon Jan 14 14:19:00 2019 +0000
+++ b/src/HOL/Data_Structures/Array_Braun.thy Mon Jan 14 16:47:29 2019 +0100
@@ -501,7 +501,7 @@
function list_fast_rec :: "'a tree list \<Rightarrow> 'a list" where
"list_fast_rec ts = (if ts = [] then [] else
let us = filter (\<lambda>t. t \<noteq> Leaf) ts
- in map root_val us @ list_fast_rec (map left us @ map right us))"
+ in map value us @ list_fast_rec (map left us @ map right us))"
by (pat_completeness, auto)
lemma list_fast_rec_term: "\<lbrakk> ts \<noteq> []; us = filter (\<lambda>t. t \<noteq> \<langle>\<rangle>) ts \<rbrakk> \<Longrightarrow>
@@ -576,13 +576,13 @@
case False
with less.prems(2) have *:
"\<forall>i < 2 ^ k. ts ! i \<noteq> Leaf
- \<and> root_val (ts ! i) = xs ! i
+ \<and> value (ts ! i) = xs ! i
\<and> braun_list (left (ts ! i)) (take_nths (i + 2 ^ k) (Suc k) xs)
\<and> (\<forall>ys. ys = take_nths (i + 2 * 2 ^ k) (Suc k) xs
\<longrightarrow> braun_list (right (ts ! i)) ys)"
by (auto simp: take_nths_empty hd_take_nths braun_list_not_Nil take_nths_take_nths
algebra_simps)
- have 1: "map root_val ts = take (2 ^ k) xs"
+ have 1: "map value ts = take (2 ^ k) xs"
using less.prems(1) False by (simp add: list_eq_iff_nth_eq *)
have 2: "list_fast_rec (map left ts @ map right ts) = drop (2 ^ k) xs"
using less.prems(1) False
--- a/src/HOL/Groups_Big.thy Mon Jan 14 14:19:00 2019 +0000
+++ b/src/HOL/Groups_Big.thy Mon Jan 14 16:47:29 2019 +0100
@@ -147,7 +147,7 @@
using g_h unfolding \<open>A = B\<close>
by (induct B rule: infinite_finite_induct) auto
-lemma cong_strong [cong]:
+lemma cong_simp [cong]:
"\<lbrakk> A = B; \<And>x. x \<in> B =simp=> g x = h x \<rbrakk> \<Longrightarrow> F (\<lambda>x. g x) A = F (\<lambda>x. h x) B"
by (rule cong) (simp_all add: simp_implies_def)
--- a/src/HOL/Hoare_Parallel/OG_Examples.thy Mon Jan 14 14:19:00 2019 +0000
+++ b/src/HOL/Hoare_Parallel/OG_Examples.thy Mon Jan 14 16:47:29 2019 +0100
@@ -534,9 +534,9 @@
COEND
\<lbrace>\<acute>x=n\<rbrace>"
apply oghoare
-apply (simp_all cong del: sum.cong_strong)
+apply (simp_all cong del: sum.cong_simp)
apply (tactic \<open>ALLGOALS (clarify_tac \<^context>)\<close>)
-apply (simp_all cong del: sum.cong_strong)
+apply (simp_all cong del: sum.cong_simp)
apply(erule (1) Example2_lemma2)
apply(erule (1) Example2_lemma2)
apply(erule (1) Example2_lemma2)
--- a/src/HOL/Library/FSet.thy Mon Jan 14 14:19:00 2019 +0000
+++ b/src/HOL/Library/FSet.thy Mon Jan 14 16:47:29 2019 +0100
@@ -755,7 +755,7 @@
lemmas cong[fundef_cong] = set.cong[Transfer.transferred]
-lemma cong_strong[cong]:
+lemma cong_simp[cong]:
"\<lbrakk> A = B; \<And>x. x |\<in>| B =simp=> g x = h x \<rbrakk> \<Longrightarrow> F g A = F h B"
unfolding simp_implies_def by (auto cong: cong)
--- a/src/HOL/Library/Tree.thy Mon Jan 14 14:19:00 2019 +0000
+++ b/src/HOL/Library/Tree.thy Mon Jan 14 16:47:29 2019 +0100
@@ -9,7 +9,7 @@
datatype 'a tree =
Leaf ("\<langle>\<rangle>") |
- Node "'a tree" (root_val: 'a) "'a tree" ("(1\<langle>_,/ _,/ _\<rangle>)")
+ Node "'a tree" ("value": 'a) "'a tree" ("(1\<langle>_,/ _,/ _\<rangle>)")
datatype_compat tree
primrec left :: "'a tree \<Rightarrow> 'a tree" where
--- a/src/HOL/Number_Theory/Gauss.thy Mon Jan 14 14:19:00 2019 +0000
+++ b/src/HOL/Number_Theory/Gauss.thy Mon Jan 14 16:47:29 2019 +0100
@@ -339,7 +339,7 @@
theorem pre_gauss_lemma: "[a ^ nat((int p - 1) div 2) = (-1) ^ (card E)] (mod p)"
proof -
have "[prod id A = prod id F * prod id D](mod p)"
- by (auto simp: prod_D_F_eq_prod_A mult.commute cong del: prod.cong_strong)
+ by (auto simp: prod_D_F_eq_prod_A mult.commute cong del: prod.cong_simp)
then have "[prod id A = ((-1)^(card E) * prod id E) * prod id D] (mod p)"
by (rule cong_trans) (metis cong_scalar_right prod_F_zcong)
then have "[prod id A = ((-1)^(card E) * prod id C)] (mod p)"
@@ -364,7 +364,7 @@
(-1)^(card E) * a^(card A) * (-1)^(card E)](mod p)"
by (rule cong_trans) (simp add: a ac_simps)
then have "[prod id A * (-1)^(card E) = prod id A * a^(card A)](mod p)"
- by (rule cong_trans) (simp add: aux cong del: prod.cong_strong)
+ by (rule cong_trans) (simp add: aux cong del: prod.cong_simp)
with A_prod_relprime have "[(- 1) ^ card E = a ^ card A](mod p)"
by (metis cong_mult_lcancel)
then show ?thesis
--- a/src/HOL/Probability/Information.thy Mon Jan 14 14:19:00 2019 +0000
+++ b/src/HOL/Probability/Information.thy Mon Jan 14 16:47:29 2019 +0100
@@ -1913,7 +1913,7 @@
also have "\<dots> = entropy b (count_space (Y ` space M) \<Otimes>\<^sub>M count_space (X ` space M)) (\<lambda>x. (Y x, X x))"
by (subst entropy_distr[OF simple_distributed_joint[OF YX]])
(auto simp: pair_measure_count_space sigma_finite_measure_count_space_finite lebesgue_integral_count_space_finite
- cong del: sum.cong_strong intro!: sum.mono_neutral_left measure_nonneg)
+ cong del: sum.cong_simp intro!: sum.mono_neutral_left measure_nonneg)
finally have "\<H>(\<lambda>x. (X x, Y x)) = entropy b (count_space (Y ` space M) \<Otimes>\<^sub>M count_space (X ` space M)) (\<lambda>x. (Y x, X x))" .
then show ?thesis
unfolding conditional_entropy_eq_entropy_simple[OF Y X] by simp
--- a/src/HOL/Probability/Tree_Space.thy Mon Jan 14 14:19:00 2019 +0000
+++ b/src/HOL/Probability/Tree_Space.thy Mon Jan 14 16:47:29 2019 +0100
@@ -231,18 +231,18 @@
unfolding * using A by (intro sets.Un Node_in_tree_sigma pair_measureI) auto
qed
-lemma measurable_root_val': "root_val \<in> restrict_space (tree_sigma M) (-{Leaf}) \<rightarrow>\<^sub>M M"
+lemma measurable_value': "value \<in> restrict_space (tree_sigma M) (-{Leaf}) \<rightarrow>\<^sub>M M"
proof (rule measurableI)
- show "t \<in> space (restrict_space (tree_sigma M) (- {Leaf})) \<Longrightarrow> root_val t \<in> space M" for t
+ show "t \<in> space (restrict_space (tree_sigma M) (- {Leaf})) \<Longrightarrow> value t \<in> space M" for t
by (cases t) (auto simp: space_restrict_space space_tree_sigma)
fix A assume A: "A \<in> sets M"
from sets.sets_into_space[OF this]
- have "root_val -` A \<inter> space (restrict_space (tree_sigma M) (- {Leaf})) =
+ have "value -` A \<inter> space (restrict_space (tree_sigma M) (- {Leaf})) =
{Node l a r | l a r. (a, l, r) \<in> A \<times> space (tree_sigma M) \<times> space (tree_sigma M)}"
by (auto simp: space_tree_sigma space_restrict_space elim: trees.cases)
also have "\<dots> \<in> sets (tree_sigma M)"
using A by (intro sets.Un Node_in_tree_sigma pair_measureI) auto
- finally show "root_val -` A \<inter> space (restrict_space (tree_sigma M) (- {Leaf})) \<in>
+ finally show "value -` A \<inter> space (restrict_space (tree_sigma M) (- {Leaf})) \<in>
sets (restrict_space (tree_sigma M) (- {Leaf}))"
by (auto simp: sets_restrict_space_iff space_restrict_space)
qed
@@ -254,14 +254,14 @@
(insert \<open>B \<subseteq> A\<close>, auto)
-lemma measurable_root_val[measurable (raw)]:
+lemma measurable_value[measurable (raw)]:
assumes "f \<in> X \<rightarrow>\<^sub>M tree_sigma M"
and "\<And>x. x \<in> space X \<Longrightarrow> f x \<noteq> Leaf"
- shows "(\<lambda>\<omega>. root_val (f \<omega>)) \<in> X \<rightarrow>\<^sub>M M"
+ shows "(\<lambda>\<omega>. value (f \<omega>)) \<in> X \<rightarrow>\<^sub>M M"
proof -
from assms have "f \<in> X \<rightarrow>\<^sub>M restrict_space (tree_sigma M) (- {Leaf})"
by (intro measurable_restrict_space2) auto
- from this and measurable_root_val' show ?thesis by (rule measurable_compose)
+ from this and measurable_value' show ?thesis by (rule measurable_compose)
qed
@@ -344,7 +344,7 @@
qed
next
case (Node ls u rs)
- let ?F = "\<lambda>\<omega>. ?N (\<omega>, left (t \<omega>), root_val (t \<omega>), right (t \<omega>),
+ let ?F = "\<lambda>\<omega>. ?N (\<omega>, left (t \<omega>), value (t \<omega>), right (t \<omega>),
rec_tree (l \<omega>) (n \<omega>) (left (t \<omega>)), rec_tree (l \<omega>) (n \<omega>) (right (t \<omega>)))"
show ?case
proof (rule measurable_cong[THEN iffD2])
@@ -366,7 +366,7 @@
by (rule measurable_restrict_space1)
(rule measurable_compose[OF Node(3) measurable_right])
subgoal
- apply (rule measurable_compose[OF _ measurable_root_val'])
+ apply (rule measurable_compose[OF _ measurable_value'])
apply (rule measurable_restrict_space3[OF Node(3)])
by auto
subgoal
--- a/src/HOL/Transcendental.thy Mon Jan 14 14:19:00 2019 +0000
+++ b/src/HOL/Transcendental.thy Mon Jan 14 16:47:29 2019 +0100
@@ -6088,7 +6088,7 @@
also have "\<dots> = (\<Sum>(i,j) \<in> (SIGMA i : atMost n. lessThan i). a i * (x - y) * (y^(i - Suc j) * x^j))"
by (simp add: sum.Sigma)
also have "\<dots> = (\<Sum>(j,i) \<in> (SIGMA j : lessThan n. {Suc j..n}). a i * (x - y) * (y^(i - Suc j) * x^j))"
- by (auto simp: sum.reindex_bij_betw [OF h, symmetric] intro: sum.cong_strong)
+ by (auto simp: sum.reindex_bij_betw [OF h, symmetric] intro: sum.cong_simp)
also have "\<dots> = (\<Sum>j<n. \<Sum>i=Suc j..n. a i * (x - y) * (y^(i - Suc j) * x^j))"
by (simp add: sum.Sigma)
also have "\<dots> = (x - y) * (\<Sum>j<n. (\<Sum>i=Suc j..n. a i * y^(i - j - 1)) * x^j)"
@@ -6110,7 +6110,7 @@
apply (rule_tac x="x + Suc j" in image_eqI, auto)
done
then show ?thesis
- by (auto simp: sum.reindex_bij_betw [OF h, symmetric] intro: sum.cong_strong)
+ by (auto simp: sum.reindex_bij_betw [OF h, symmetric] intro: sum.cong_simp)
qed
then show ?thesis
by (simp add: polyfun_diff [OF assms] sum_distrib_right)