--- a/src/HOL/Complete_Lattices.thy Fri May 27 23:35:13 2016 +0200
+++ b/src/HOL/Complete_Lattices.thy Fri May 27 23:58:24 2016 +0200
@@ -484,11 +484,11 @@
lemma sup_INF:
"a \<squnion> (\<Sqinter>b\<in>B. f b) = (\<Sqinter>b\<in>B. a \<squnion> f b)"
- unfolding sup_Inf by simp
+ by (simp add: sup_Inf)
lemma inf_SUP:
"a \<sqinter> (\<Squnion>b\<in>B. f b) = (\<Squnion>b\<in>B. a \<sqinter> f b)"
- unfolding inf_Sup by simp
+ by (simp add: inf_Sup)
lemma dual_complete_distrib_lattice:
"class.complete_distrib_lattice Sup Inf sup (op \<ge>) (op >) inf \<top> \<bottom>"
@@ -607,19 +607,19 @@
lemma Inf_less_iff:
"\<Sqinter>S \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>S. x \<sqsubset> a)"
- unfolding not_le [symmetric] le_Inf_iff by auto
+ by (simp add: not_le [symmetric] le_Inf_iff)
lemma INF_less_iff:
"(\<Sqinter>i\<in>A. f i) \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>A. f x \<sqsubset> a)"
- using Inf_less_iff [of "f ` A"] by simp
+ by (simp add: Inf_less_iff [of "f ` A"])
lemma less_Sup_iff:
"a \<sqsubset> \<Squnion>S \<longleftrightarrow> (\<exists>x\<in>S. a \<sqsubset> x)"
- unfolding not_le [symmetric] Sup_le_iff by auto
+ by (simp add: not_le [symmetric] Sup_le_iff)
lemma less_SUP_iff:
"a \<sqsubset> (\<Squnion>i\<in>A. f i) \<longleftrightarrow> (\<exists>x\<in>A. a \<sqsubset> f x)"
- using less_Sup_iff [of _ "f ` A"] by simp
+ by (simp add: less_Sup_iff [of _ "f ` A"])
lemma Sup_eq_top_iff [simp]:
"\<Squnion>A = \<top> \<longleftrightarrow> (\<forall>x<\<top>. \<exists>i\<in>A. x < i)"
@@ -628,7 +628,7 @@
show "(\<forall>x<\<top>. \<exists>i\<in>A. x < i)" unfolding * [symmetric]
proof (intro allI impI)
fix x assume "x < \<Squnion>A" then show "\<exists>i\<in>A. x < i"
- unfolding less_Sup_iff by auto
+ by (simp add: less_Sup_iff)
qed
next
assume *: "\<forall>x<\<top>. \<exists>i\<in>A. x < i"
--- a/src/HOL/Orderings.thy Fri May 27 23:35:13 2016 +0200
+++ b/src/HOL/Orderings.thy Fri May 27 23:58:24 2016 +0200
@@ -134,7 +134,7 @@
by (simp add: less_le_not_le)
lemma less_imp_le: "x < y \<Longrightarrow> x \<le> y"
-unfolding less_le_not_le by blast
+by (simp add: less_le_not_le)
text \<open>Asymmetry.\<close>
@@ -202,7 +202,7 @@
by (fact order.order_iff_strict)
lemma le_imp_less_or_eq: "x \<le> y \<Longrightarrow> x < y \<or> x = y"
-unfolding less_le by blast
+by (simp add: less_le)
text \<open>Useful for simplification, but too risky to include by default.\<close>
--- a/src/HOL/Zorn.thy Fri May 27 23:35:13 2016 +0200
+++ b/src/HOL/Zorn.thy Fri May 27 23:58:24 2016 +0200
@@ -416,7 +416,7 @@
lemma chains_extend:
"[| c \<in> chains S; z \<in> S; \<forall>x \<in> c. x \<subseteq> (z:: 'a set) |] ==> {z} Un c \<in> chains S"
- by (unfold chains_def chain_subset_def) blast
+ unfolding chains_def chain_subset_def by blast
lemma mono_Chains: "r \<subseteq> s \<Longrightarrow> Chains r \<subseteq> Chains s"
unfolding Chains_def by blast
@@ -453,10 +453,10 @@
text\<open>Various other lemmas\<close>
lemma chainsD: "[| c \<in> chains S; x \<in> c; y \<in> c |] ==> x \<subseteq> y | y \<subseteq> x"
-by (unfold chains_def chain_subset_def) blast
+ unfolding chains_def chain_subset_def by blast
lemma chainsD2: "!!(c :: 'a set set). c \<in> chains S ==> c \<subseteq> S"
-by (unfold chains_def) blast
+ unfolding chains_def by blast
lemma Zorns_po_lemma:
assumes po: "Partial_order r"
@@ -682,11 +682,11 @@
moreover have "Total ?m" using \<open>Total m\<close> and Fm by (auto simp: total_on_def)
moreover have "wf (?m - Id)"
proof -
- have "wf ?s" using \<open>x \<notin> Field m\<close> unfolding wf_eq_minimal Field_def
- by (auto simp: Bex_def)
+ have "wf ?s" using \<open>x \<notin> Field m\<close>
+ by (auto simp: wf_eq_minimal Field_def Bex_def)
thus ?thesis using \<open>wf (m - Id)\<close> and \<open>x \<notin> Field m\<close>
wf_subset [OF \<open>wf ?s\<close> Diff_subset]
- unfolding Un_Diff Field_def by (auto intro: wf_Un)
+ by (auto simp: Un_Diff Field_def intro: wf_Un)
qed
ultimately have "Well_order ?m" by (simp add: order_on_defs)
\<comment>\<open>We show that the extension is above m\<close>