tuned proofs;
authorwenzelm
Fri May 27 23:58:24 2016 +0200 (2016-05-27)
changeset 63172d4f459eb7ed0
parent 63171 a0088f1c049d
child 63173 3413b1cf30cd
child 63176 878bd5922f3b
tuned proofs;
src/HOL/Complete_Lattices.thy
src/HOL/Orderings.thy
src/HOL/Zorn.thy
     1.1 --- a/src/HOL/Complete_Lattices.thy	Fri May 27 23:35:13 2016 +0200
     1.2 +++ b/src/HOL/Complete_Lattices.thy	Fri May 27 23:58:24 2016 +0200
     1.3 @@ -484,11 +484,11 @@
     1.4  
     1.5  lemma sup_INF:
     1.6    "a \<squnion> (\<Sqinter>b\<in>B. f b) = (\<Sqinter>b\<in>B. a \<squnion> f b)"
     1.7 -  unfolding sup_Inf by simp
     1.8 +  by (simp add: sup_Inf)
     1.9  
    1.10  lemma inf_SUP:
    1.11    "a \<sqinter> (\<Squnion>b\<in>B. f b) = (\<Squnion>b\<in>B. a \<sqinter> f b)"
    1.12 -  unfolding inf_Sup by simp
    1.13 +  by (simp add: inf_Sup)
    1.14  
    1.15  lemma dual_complete_distrib_lattice:
    1.16    "class.complete_distrib_lattice Sup Inf sup (op \<ge>) (op >) inf \<top> \<bottom>"
    1.17 @@ -607,19 +607,19 @@
    1.18  
    1.19  lemma Inf_less_iff:
    1.20    "\<Sqinter>S \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>S. x \<sqsubset> a)"
    1.21 -  unfolding not_le [symmetric] le_Inf_iff by auto
    1.22 +  by (simp add: not_le [symmetric] le_Inf_iff)
    1.23  
    1.24  lemma INF_less_iff:
    1.25    "(\<Sqinter>i\<in>A. f i) \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>A. f x \<sqsubset> a)"
    1.26 -  using Inf_less_iff [of "f ` A"] by simp
    1.27 +  by (simp add: Inf_less_iff [of "f ` A"])
    1.28  
    1.29  lemma less_Sup_iff:
    1.30    "a \<sqsubset> \<Squnion>S \<longleftrightarrow> (\<exists>x\<in>S. a \<sqsubset> x)"
    1.31 -  unfolding not_le [symmetric] Sup_le_iff by auto
    1.32 +  by (simp add: not_le [symmetric] Sup_le_iff)
    1.33  
    1.34  lemma less_SUP_iff:
    1.35    "a \<sqsubset> (\<Squnion>i\<in>A. f i) \<longleftrightarrow> (\<exists>x\<in>A. a \<sqsubset> f x)"
    1.36 -  using less_Sup_iff [of _ "f ` A"] by simp
    1.37 +  by (simp add: less_Sup_iff [of _ "f ` A"])
    1.38  
    1.39  lemma Sup_eq_top_iff [simp]:
    1.40    "\<Squnion>A = \<top> \<longleftrightarrow> (\<forall>x<\<top>. \<exists>i\<in>A. x < i)"
    1.41 @@ -628,7 +628,7 @@
    1.42    show "(\<forall>x<\<top>. \<exists>i\<in>A. x < i)" unfolding * [symmetric]
    1.43    proof (intro allI impI)
    1.44      fix x assume "x < \<Squnion>A" then show "\<exists>i\<in>A. x < i"
    1.45 -      unfolding less_Sup_iff by auto
    1.46 +      by (simp add: less_Sup_iff)
    1.47    qed
    1.48  next
    1.49    assume *: "\<forall>x<\<top>. \<exists>i\<in>A. x < i"
     2.1 --- a/src/HOL/Orderings.thy	Fri May 27 23:35:13 2016 +0200
     2.2 +++ b/src/HOL/Orderings.thy	Fri May 27 23:58:24 2016 +0200
     2.3 @@ -134,7 +134,7 @@
     2.4  by (simp add: less_le_not_le)
     2.5  
     2.6  lemma less_imp_le: "x < y \<Longrightarrow> x \<le> y"
     2.7 -unfolding less_le_not_le by blast
     2.8 +by (simp add: less_le_not_le)
     2.9  
    2.10  
    2.11  text \<open>Asymmetry.\<close>
    2.12 @@ -202,7 +202,7 @@
    2.13  by (fact order.order_iff_strict)
    2.14  
    2.15  lemma le_imp_less_or_eq: "x \<le> y \<Longrightarrow> x < y \<or> x = y"
    2.16 -unfolding less_le by blast
    2.17 +by (simp add: less_le)
    2.18  
    2.19  
    2.20  text \<open>Useful for simplification, but too risky to include by default.\<close>
     3.1 --- a/src/HOL/Zorn.thy	Fri May 27 23:35:13 2016 +0200
     3.2 +++ b/src/HOL/Zorn.thy	Fri May 27 23:58:24 2016 +0200
     3.3 @@ -416,7 +416,7 @@
     3.4  
     3.5  lemma chains_extend:
     3.6    "[| c \<in> chains S; z \<in> S; \<forall>x \<in> c. x \<subseteq> (z:: 'a set) |] ==> {z} Un c \<in> chains S"
     3.7 -  by (unfold chains_def chain_subset_def) blast
     3.8 +  unfolding chains_def chain_subset_def by blast
     3.9  
    3.10  lemma mono_Chains: "r \<subseteq> s \<Longrightarrow> Chains r \<subseteq> Chains s"
    3.11    unfolding Chains_def by blast
    3.12 @@ -453,10 +453,10 @@
    3.13  text\<open>Various other lemmas\<close>
    3.14  
    3.15  lemma chainsD: "[| c \<in> chains S; x \<in> c; y \<in> c |] ==> x \<subseteq> y | y \<subseteq> x"
    3.16 -by (unfold chains_def chain_subset_def) blast
    3.17 +  unfolding chains_def chain_subset_def by blast
    3.18  
    3.19  lemma chainsD2: "!!(c :: 'a set set). c \<in> chains S ==> c \<subseteq> S"
    3.20 -by (unfold chains_def) blast
    3.21 +  unfolding chains_def by blast
    3.22  
    3.23  lemma Zorns_po_lemma:
    3.24    assumes po: "Partial_order r"
    3.25 @@ -682,11 +682,11 @@
    3.26      moreover have "Total ?m" using \<open>Total m\<close> and Fm by (auto simp: total_on_def)
    3.27      moreover have "wf (?m - Id)"
    3.28      proof -
    3.29 -      have "wf ?s" using \<open>x \<notin> Field m\<close> unfolding wf_eq_minimal Field_def
    3.30 -        by (auto simp: Bex_def)
    3.31 +      have "wf ?s" using \<open>x \<notin> Field m\<close> 
    3.32 +        by (auto simp: wf_eq_minimal Field_def Bex_def)
    3.33        thus ?thesis using \<open>wf (m - Id)\<close> and \<open>x \<notin> Field m\<close>
    3.34          wf_subset [OF \<open>wf ?s\<close> Diff_subset]
    3.35 -        unfolding Un_Diff Field_def by (auto intro: wf_Un)
    3.36 +        by (auto simp: Un_Diff Field_def intro: wf_Un)
    3.37      qed
    3.38      ultimately have "Well_order ?m" by (simp add: order_on_defs)
    3.39  \<comment>\<open>We show that the extension is above m\<close>