misc tuning and modernization;
authorwenzelm
Mon Aug 01 22:11:29 2016 +0200 (2016-08-01)
changeset 63575b9bd9e61fd63
parent 63574 4ea48cbc54c1
child 63576 ba972a7dbeba
misc tuning and modernization;
src/HOL/Complete_Lattices.thy
src/HOL/Fun.thy
src/HOL/HOL.thy
src/HOL/Product_Type.thy
src/HOL/Sum_Type.thy
     1.1 --- a/src/HOL/Complete_Lattices.thy	Mon Aug 01 13:51:17 2016 +0200
     1.2 +++ b/src/HOL/Complete_Lattices.thy	Mon Aug 01 22:11:29 2016 +0200
     1.3 @@ -1,9 +1,14 @@
     1.4 -(*  Author:     Tobias Nipkow, Lawrence C Paulson and Markus Wenzel; Florian Haftmann, TU Muenchen *)
     1.5 +(*  Title:      HOL/Complete_Lattices.thy
     1.6 +    Author:     Tobias Nipkow
     1.7 +    Author:     Lawrence C Paulson
     1.8 +    Author:     Markus Wenzel
     1.9 +    Author:     Florian Haftmann
    1.10 +*)
    1.11  
    1.12  section \<open>Complete lattices\<close>
    1.13  
    1.14  theory Complete_Lattices
    1.15 -imports Fun
    1.16 +  imports Fun
    1.17  begin
    1.18  
    1.19  notation
    1.20 @@ -14,27 +19,22 @@
    1.21  subsection \<open>Syntactic infimum and supremum operations\<close>
    1.22  
    1.23  class Inf =
    1.24 -  fixes Inf :: "'a set \<Rightarrow> 'a" ("\<Sqinter>_" [900] 900)
    1.25 +  fixes Inf :: "'a set \<Rightarrow> 'a"  ("\<Sqinter>_" [900] 900)
    1.26  begin
    1.27  
    1.28  abbreviation INFIMUM :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a"
    1.29 -where
    1.30 -  "INFIMUM A f \<equiv> \<Sqinter>(f ` A)"
    1.31 +  where "INFIMUM A f \<equiv> \<Sqinter>(f ` A)"
    1.32  
    1.33 -lemma INF_image [simp]:
    1.34 -  "INFIMUM (f ` A) g = INFIMUM A (g \<circ> f)"
    1.35 +lemma INF_image [simp]: "INFIMUM (f ` A) g = INFIMUM A (g \<circ> f)"
    1.36    by (simp add: image_comp)
    1.37  
    1.38 -lemma INF_identity_eq [simp]:
    1.39 -  "INFIMUM A (\<lambda>x. x) = \<Sqinter>A"
    1.40 +lemma INF_identity_eq [simp]: "INFIMUM A (\<lambda>x. x) = \<Sqinter>A"
    1.41    by simp
    1.42  
    1.43 -lemma INF_id_eq [simp]:
    1.44 -  "INFIMUM A id = \<Sqinter>A"
    1.45 +lemma INF_id_eq [simp]: "INFIMUM A id = \<Sqinter>A"
    1.46    by simp
    1.47  
    1.48 -lemma INF_cong:
    1.49 -  "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> INFIMUM A C = INFIMUM B D"
    1.50 +lemma INF_cong: "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> INFIMUM A C = INFIMUM B D"
    1.51    by (simp add: image_def)
    1.52  
    1.53  lemma strong_INF_cong [cong]:
    1.54 @@ -44,27 +44,22 @@
    1.55  end
    1.56  
    1.57  class Sup =
    1.58 -  fixes Sup :: "'a set \<Rightarrow> 'a" ("\<Squnion>_" [900] 900)
    1.59 +  fixes Sup :: "'a set \<Rightarrow> 'a"  ("\<Squnion>_" [900] 900)
    1.60  begin
    1.61  
    1.62  abbreviation SUPREMUM :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a"
    1.63 -where
    1.64 -  "SUPREMUM A f \<equiv> \<Squnion>(f ` A)"
    1.65 +  where "SUPREMUM A f \<equiv> \<Squnion>(f ` A)"
    1.66  
    1.67 -lemma SUP_image [simp]:
    1.68 -  "SUPREMUM (f ` A) g = SUPREMUM A (g \<circ> f)"
    1.69 +lemma SUP_image [simp]: "SUPREMUM (f ` A) g = SUPREMUM A (g \<circ> f)"
    1.70    by (simp add: image_comp)
    1.71  
    1.72 -lemma SUP_identity_eq [simp]:
    1.73 -  "SUPREMUM A (\<lambda>x. x) = \<Squnion>A"
    1.74 +lemma SUP_identity_eq [simp]: "SUPREMUM A (\<lambda>x. x) = \<Squnion>A"
    1.75    by simp
    1.76  
    1.77 -lemma SUP_id_eq [simp]:
    1.78 -  "SUPREMUM A id = \<Squnion>A"
    1.79 +lemma SUP_id_eq [simp]: "SUPREMUM A id = \<Squnion>A"
    1.80    by (simp add: id_def)
    1.81  
    1.82 -lemma SUP_cong:
    1.83 -  "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> SUPREMUM A C = SUPREMUM B D"
    1.84 +lemma SUP_cong: "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> SUPREMUM A C = SUPREMUM B D"
    1.85    by (simp add: image_def)
    1.86  
    1.87  lemma strong_SUP_cong [cong]:
    1.88 @@ -122,25 +117,25 @@
    1.89  
    1.90  class complete_lattice = lattice + Inf + Sup + bot + top +
    1.91    assumes Inf_lower: "x \<in> A \<Longrightarrow> \<Sqinter>A \<sqsubseteq> x"
    1.92 -     and Inf_greatest: "(\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x) \<Longrightarrow> z \<sqsubseteq> \<Sqinter>A"
    1.93 -  assumes Sup_upper: "x \<in> A \<Longrightarrow> x \<sqsubseteq> \<Squnion>A"
    1.94 -     and Sup_least: "(\<And>x. x \<in> A \<Longrightarrow> x \<sqsubseteq> z) \<Longrightarrow> \<Squnion>A \<sqsubseteq> z"
    1.95 -  assumes Inf_empty [simp]: "\<Sqinter>{} = \<top>"
    1.96 -  assumes Sup_empty [simp]: "\<Squnion>{} = \<bottom>"
    1.97 +    and Inf_greatest: "(\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x) \<Longrightarrow> z \<sqsubseteq> \<Sqinter>A"
    1.98 +    and Sup_upper: "x \<in> A \<Longrightarrow> x \<sqsubseteq> \<Squnion>A"
    1.99 +    and Sup_least: "(\<And>x. x \<in> A \<Longrightarrow> x \<sqsubseteq> z) \<Longrightarrow> \<Squnion>A \<sqsubseteq> z"
   1.100 +    and Inf_empty [simp]: "\<Sqinter>{} = \<top>"
   1.101 +    and Sup_empty [simp]: "\<Squnion>{} = \<bottom>"
   1.102  begin
   1.103  
   1.104  subclass bounded_lattice
   1.105  proof
   1.106    fix a
   1.107 -  show "\<bottom> \<le> a" by (auto intro: Sup_least simp only: Sup_empty [symmetric])
   1.108 -  show "a \<le> \<top>" by (auto intro: Inf_greatest simp only: Inf_empty [symmetric])
   1.109 +  show "\<bottom> \<le> a"
   1.110 +    by (auto intro: Sup_least simp only: Sup_empty [symmetric])
   1.111 +  show "a \<le> \<top>"
   1.112 +    by (auto intro: Inf_greatest simp only: Inf_empty [symmetric])
   1.113  qed
   1.114  
   1.115 -lemma dual_complete_lattice:
   1.116 -  "class.complete_lattice Sup Inf sup (op \<ge>) (op >) inf \<top> \<bottom>"
   1.117 +lemma dual_complete_lattice: "class.complete_lattice Sup Inf sup (op \<ge>) (op >) inf \<top> \<bottom>"
   1.118    by (auto intro!: class.complete_lattice.intro dual_lattice)
   1.119 -    (unfold_locales, (fact Inf_empty Sup_empty
   1.120 -        Sup_upper Sup_least Inf_lower Inf_greatest)+)
   1.121 +    (unfold_locales, (fact Inf_empty Sup_empty Sup_upper Sup_least Inf_lower Inf_greatest)+)
   1.122  
   1.123  end
   1.124  
   1.125 @@ -217,12 +212,10 @@
   1.126  lemma SUP_empty [simp]: "(\<Squnion>x\<in>{}. f x) = \<bottom>"
   1.127    by (simp cong del: strong_SUP_cong)
   1.128  
   1.129 -lemma Inf_UNIV [simp]:
   1.130 -  "\<Sqinter>UNIV = \<bottom>"
   1.131 +lemma Inf_UNIV [simp]: "\<Sqinter>UNIV = \<bottom>"
   1.132    by (auto intro!: antisym Inf_lower)
   1.133  
   1.134 -lemma Sup_UNIV [simp]:
   1.135 -  "\<Squnion>UNIV = \<top>"
   1.136 +lemma Sup_UNIV [simp]: "\<Squnion>UNIV = \<top>"
   1.137    by (auto intro!: antisym Sup_upper)
   1.138  
   1.139  lemma Inf_Sup: "\<Sqinter>A = \<Squnion>{b. \<forall>a \<in> A. b \<sqsubseteq> a}"
   1.140 @@ -247,8 +240,7 @@
   1.141    with \<open>a \<sqsubseteq> b\<close> show "\<Sqinter>A \<sqsubseteq> b" by auto
   1.142  qed
   1.143  
   1.144 -lemma INF_mono:
   1.145 -  "(\<And>m. m \<in> B \<Longrightarrow> \<exists>n\<in>A. f n \<sqsubseteq> g m) \<Longrightarrow> (\<Sqinter>n\<in>A. f n) \<sqsubseteq> (\<Sqinter>n\<in>B. g n)"
   1.146 +lemma INF_mono: "(\<And>m. m \<in> B \<Longrightarrow> \<exists>n\<in>A. f n \<sqsubseteq> g m) \<Longrightarrow> (\<Sqinter>n\<in>A. f n) \<sqsubseteq> (\<Sqinter>n\<in>B. g n)"
   1.147    using Inf_mono [of "g ` B" "f ` A"] by auto
   1.148  
   1.149  lemma Sup_mono:
   1.150 @@ -261,17 +253,14 @@
   1.151    with \<open>a \<sqsubseteq> b\<close> show "a \<sqsubseteq> \<Squnion>B" by auto
   1.152  qed
   1.153  
   1.154 -lemma SUP_mono:
   1.155 -  "(\<And>n. n \<in> A \<Longrightarrow> \<exists>m\<in>B. f n \<sqsubseteq> g m) \<Longrightarrow> (\<Squnion>n\<in>A. f n) \<sqsubseteq> (\<Squnion>n\<in>B. g n)"
   1.156 +lemma SUP_mono: "(\<And>n. n \<in> A \<Longrightarrow> \<exists>m\<in>B. f n \<sqsubseteq> g m) \<Longrightarrow> (\<Squnion>n\<in>A. f n) \<sqsubseteq> (\<Squnion>n\<in>B. g n)"
   1.157    using Sup_mono [of "f ` A" "g ` B"] by auto
   1.158  
   1.159 -lemma INF_superset_mono:
   1.160 -  "B \<subseteq> A \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> f x \<sqsubseteq> g x) \<Longrightarrow> (\<Sqinter>x\<in>A. f x) \<sqsubseteq> (\<Sqinter>x\<in>B. g x)"
   1.161 +lemma INF_superset_mono: "B \<subseteq> A \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> f x \<sqsubseteq> g x) \<Longrightarrow> (\<Sqinter>x\<in>A. f x) \<sqsubseteq> (\<Sqinter>x\<in>B. g x)"
   1.162    \<comment> \<open>The last inclusion is POSITIVE!\<close>
   1.163    by (blast intro: INF_mono dest: subsetD)
   1.164  
   1.165 -lemma SUP_subset_mono:
   1.166 -  "A \<subseteq> B \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<sqsubseteq> g x) \<Longrightarrow> (\<Squnion>x\<in>A. f x) \<sqsubseteq> (\<Squnion>x\<in>B. g x)"
   1.167 +lemma SUP_subset_mono: "A \<subseteq> B \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<sqsubseteq> g x) \<Longrightarrow> (\<Squnion>x\<in>A. f x) \<sqsubseteq> (\<Squnion>x\<in>B. g x)"
   1.168    by (blast intro: SUP_mono dest: subsetD)
   1.169  
   1.170  lemma Inf_less_eq:
   1.171 @@ -296,13 +285,13 @@
   1.172  
   1.173  lemma INF_eq:
   1.174    assumes "\<And>i. i \<in> A \<Longrightarrow> \<exists>j\<in>B. f i \<ge> g j"
   1.175 -  assumes "\<And>j. j \<in> B \<Longrightarrow> \<exists>i\<in>A. g j \<ge> f i"
   1.176 +    and "\<And>j. j \<in> B \<Longrightarrow> \<exists>i\<in>A. g j \<ge> f i"
   1.177    shows "INFIMUM A f = INFIMUM B g"
   1.178    by (intro antisym INF_greatest) (blast intro: INF_lower2 dest: assms)+
   1.179  
   1.180  lemma SUP_eq:
   1.181    assumes "\<And>i. i \<in> A \<Longrightarrow> \<exists>j\<in>B. f i \<le> g j"
   1.182 -  assumes "\<And>j. j \<in> B \<Longrightarrow> \<exists>i\<in>A. g j \<le> f i"
   1.183 +    and "\<And>j. j \<in> B \<Longrightarrow> \<exists>i\<in>A. g j \<le> f i"
   1.184    shows "SUPREMUM A f = SUPREMUM B g"
   1.185    by (intro antisym SUP_least) (blast intro: SUP_upper2 dest: assms)+
   1.186  
   1.187 @@ -315,25 +304,25 @@
   1.188  lemma Inf_union_distrib: "\<Sqinter>(A \<union> B) = \<Sqinter>A \<sqinter> \<Sqinter>B"
   1.189    by (rule antisym) (auto intro: Inf_greatest Inf_lower le_infI1 le_infI2)
   1.190  
   1.191 -lemma INF_union:
   1.192 -  "(\<Sqinter>i \<in> A \<union> B. M i) = (\<Sqinter>i \<in> A. M i) \<sqinter> (\<Sqinter>i\<in>B. M i)"
   1.193 +lemma INF_union: "(\<Sqinter>i \<in> A \<union> B. M i) = (\<Sqinter>i \<in> A. M i) \<sqinter> (\<Sqinter>i\<in>B. M i)"
   1.194    by (auto intro!: antisym INF_mono intro: le_infI1 le_infI2 INF_greatest INF_lower)
   1.195  
   1.196  lemma Sup_union_distrib: "\<Squnion>(A \<union> B) = \<Squnion>A \<squnion> \<Squnion>B"
   1.197    by (rule antisym) (auto intro: Sup_least Sup_upper le_supI1 le_supI2)
   1.198  
   1.199 -lemma SUP_union:
   1.200 -  "(\<Squnion>i \<in> A \<union> B. M i) = (\<Squnion>i \<in> A. M i) \<squnion> (\<Squnion>i\<in>B. M i)"
   1.201 +lemma SUP_union: "(\<Squnion>i \<in> A \<union> B. M i) = (\<Squnion>i \<in> A. M i) \<squnion> (\<Squnion>i\<in>B. M i)"
   1.202    by (auto intro!: antisym SUP_mono intro: le_supI1 le_supI2 SUP_least SUP_upper)
   1.203  
   1.204  lemma INF_inf_distrib: "(\<Sqinter>a\<in>A. f a) \<sqinter> (\<Sqinter>a\<in>A. g a) = (\<Sqinter>a\<in>A. f a \<sqinter> g a)"
   1.205    by (rule antisym) (rule INF_greatest, auto intro: le_infI1 le_infI2 INF_lower INF_mono)
   1.206  
   1.207 -lemma SUP_sup_distrib: "(\<Squnion>a\<in>A. f a) \<squnion> (\<Squnion>a\<in>A. g a) = (\<Squnion>a\<in>A. f a \<squnion> g a)" (is "?L = ?R")
   1.208 +lemma SUP_sup_distrib: "(\<Squnion>a\<in>A. f a) \<squnion> (\<Squnion>a\<in>A. g a) = (\<Squnion>a\<in>A. f a \<squnion> g a)"
   1.209 +  (is "?L = ?R")
   1.210  proof (rule antisym)
   1.211 -  show "?L \<le> ?R" by (auto intro: le_supI1 le_supI2 SUP_upper SUP_mono)
   1.212 -next
   1.213 -  show "?R \<le> ?L" by (rule SUP_least) (auto intro: le_supI1 le_supI2 SUP_upper)
   1.214 +  show "?L \<le> ?R"
   1.215 +    by (auto intro: le_supI1 le_supI2 SUP_upper SUP_mono)
   1.216 +  show "?R \<le> ?L"
   1.217 +    by (rule SUP_least) (auto intro: le_supI1 le_supI2 SUP_upper)
   1.218  qed
   1.219  
   1.220  lemma Inf_top_conv [simp]:
   1.221 @@ -364,14 +353,14 @@
   1.222    using Inf_top_conv [of "B ` A"] by simp_all
   1.223  
   1.224  lemma Sup_bot_conv [simp]:
   1.225 -  "\<Squnion>A = \<bottom> \<longleftrightarrow> (\<forall>x\<in>A. x = \<bottom>)" (is ?P)
   1.226 -  "\<bottom> = \<Squnion>A \<longleftrightarrow> (\<forall>x\<in>A. x = \<bottom>)" (is ?Q)
   1.227 +  "\<Squnion>A = \<bottom> \<longleftrightarrow> (\<forall>x\<in>A. x = \<bottom>)"
   1.228 +  "\<bottom> = \<Squnion>A \<longleftrightarrow> (\<forall>x\<in>A. x = \<bottom>)"
   1.229    using dual_complete_lattice
   1.230    by (rule complete_lattice.Inf_top_conv)+
   1.231  
   1.232  lemma SUP_bot_conv [simp]:
   1.233 - "(\<Squnion>x\<in>A. B x) = \<bottom> \<longleftrightarrow> (\<forall>x\<in>A. B x = \<bottom>)"
   1.234 - "\<bottom> = (\<Squnion>x\<in>A. B x) \<longleftrightarrow> (\<forall>x\<in>A. B x = \<bottom>)"
   1.235 +  "(\<Squnion>x\<in>A. B x) = \<bottom> \<longleftrightarrow> (\<forall>x\<in>A. B x = \<bottom>)"
   1.236 +  "\<bottom> = (\<Squnion>x\<in>A. B x) \<longleftrightarrow> (\<forall>x\<in>A. B x = \<bottom>)"
   1.237    using Sup_bot_conv [of "B ` A"] by simp_all
   1.238  
   1.239  lemma INF_const [simp]: "A \<noteq> {} \<Longrightarrow> (\<Sqinter>i\<in>A. f) = f"
   1.240 @@ -408,25 +397,22 @@
   1.241    then show ?thesis by simp
   1.242  qed
   1.243  
   1.244 -lemma INF_inf_const1:
   1.245 -  "I \<noteq> {} \<Longrightarrow> (INF i:I. inf x (f i)) = inf x (INF i:I. f i)"
   1.246 +lemma INF_inf_const1: "I \<noteq> {} \<Longrightarrow> (INF i:I. inf x (f i)) = inf x (INF i:I. f i)"
   1.247    by (intro antisym INF_greatest inf_mono order_refl INF_lower)
   1.248       (auto intro: INF_lower2 le_infI2 intro!: INF_mono)
   1.249  
   1.250 -lemma INF_inf_const2:
   1.251 -  "I \<noteq> {} \<Longrightarrow> (INF i:I. inf (f i) x) = inf (INF i:I. f i) x"
   1.252 +lemma INF_inf_const2: "I \<noteq> {} \<Longrightarrow> (INF i:I. inf (f i) x) = inf (INF i:I. f i) x"
   1.253    using INF_inf_const1[of I x f] by (simp add: inf_commute)
   1.254  
   1.255 -lemma INF_constant:
   1.256 -  "(\<Sqinter>y\<in>A. c) = (if A = {} then \<top> else c)"
   1.257 +lemma INF_constant: "(\<Sqinter>y\<in>A. c) = (if A = {} then \<top> else c)"
   1.258    by simp
   1.259  
   1.260 -lemma SUP_constant:
   1.261 -  "(\<Squnion>y\<in>A. c) = (if A = {} then \<bottom> else c)"
   1.262 +lemma SUP_constant: "(\<Squnion>y\<in>A. c) = (if A = {} then \<bottom> else c)"
   1.263    by simp
   1.264  
   1.265  lemma less_INF_D:
   1.266 -  assumes "y < (\<Sqinter>i\<in>A. f i)" "i \<in> A" shows "y < f i"
   1.267 +  assumes "y < (\<Sqinter>i\<in>A. f i)" "i \<in> A"
   1.268 +  shows "y < f i"
   1.269  proof -
   1.270    note \<open>y < (\<Sqinter>i\<in>A. f i)\<close>
   1.271    also have "(\<Sqinter>i\<in>A. f i) \<le> f i" using \<open>i \<in> A\<close>
   1.272 @@ -435,20 +421,19 @@
   1.273  qed
   1.274  
   1.275  lemma SUP_lessD:
   1.276 -  assumes "(\<Squnion>i\<in>A. f i) < y" "i \<in> A" shows "f i < y"
   1.277 +  assumes "(\<Squnion>i\<in>A. f i) < y" "i \<in> A"
   1.278 +  shows "f i < y"
   1.279  proof -
   1.280 -  have "f i \<le> (\<Squnion>i\<in>A. f i)" using \<open>i \<in> A\<close>
   1.281 -    by (rule SUP_upper)
   1.282 +  have "f i \<le> (\<Squnion>i\<in>A. f i)"
   1.283 +    using \<open>i \<in> A\<close> by (rule SUP_upper)
   1.284    also note \<open>(\<Squnion>i\<in>A. f i) < y\<close>
   1.285    finally show "f i < y" .
   1.286  qed
   1.287  
   1.288 -lemma INF_UNIV_bool_expand:
   1.289 -  "(\<Sqinter>b. A b) = A True \<sqinter> A False"
   1.290 +lemma INF_UNIV_bool_expand: "(\<Sqinter>b. A b) = A True \<sqinter> A False"
   1.291    by (simp add: UNIV_bool inf_commute)
   1.292  
   1.293 -lemma SUP_UNIV_bool_expand:
   1.294 -  "(\<Squnion>b. A b) = A True \<squnion> A False"
   1.295 +lemma SUP_UNIV_bool_expand: "(\<Squnion>b. A b) = A True \<squnion> A False"
   1.296    by (simp add: UNIV_bool sup_commute)
   1.297  
   1.298  lemma Inf_le_Sup: "A \<noteq> {} \<Longrightarrow> Inf A \<le> Sup A"
   1.299 @@ -457,21 +442,17 @@
   1.300  lemma INF_le_SUP: "A \<noteq> {} \<Longrightarrow> INFIMUM A f \<le> SUPREMUM A f"
   1.301    using Inf_le_Sup [of "f ` A"] by simp
   1.302  
   1.303 -lemma INF_eq_const:
   1.304 -  "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i = x) \<Longrightarrow> INFIMUM I f = x"
   1.305 +lemma INF_eq_const: "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i = x) \<Longrightarrow> INFIMUM I f = x"
   1.306    by (auto intro: INF_eqI)
   1.307  
   1.308 -lemma SUP_eq_const:
   1.309 -  "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i = x) \<Longrightarrow> SUPREMUM I f = x"
   1.310 +lemma SUP_eq_const: "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i = x) \<Longrightarrow> SUPREMUM I f = x"
   1.311    by (auto intro: SUP_eqI)
   1.312  
   1.313 -lemma INF_eq_iff:
   1.314 -  "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i \<le> c) \<Longrightarrow> (INFIMUM I f = c) \<longleftrightarrow> (\<forall>i\<in>I. f i = c)"
   1.315 +lemma INF_eq_iff: "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i \<le> c) \<Longrightarrow> INFIMUM I f = c \<longleftrightarrow> (\<forall>i\<in>I. f i = c)"
   1.316    using INF_eq_const [of I f c] INF_lower [of _ I f]
   1.317    by (auto intro: antisym cong del: strong_INF_cong)
   1.318  
   1.319 -lemma SUP_eq_iff:
   1.320 -  "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> c \<le> f i) \<Longrightarrow> (SUPREMUM I f = c) \<longleftrightarrow> (\<forall>i\<in>I. f i = c)"
   1.321 +lemma SUP_eq_iff: "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> c \<le> f i) \<Longrightarrow> SUPREMUM I f = c \<longleftrightarrow> (\<forall>i\<in>I. f i = c)"
   1.322    using SUP_eq_const [of I f c] SUP_upper [of _ I f]
   1.323    by (auto intro: antisym cong del: strong_SUP_cong)
   1.324  
   1.325 @@ -479,61 +460,52 @@
   1.326  
   1.327  class complete_distrib_lattice = complete_lattice +
   1.328    assumes sup_Inf: "a \<squnion> \<Sqinter>B = (\<Sqinter>b\<in>B. a \<squnion> b)"
   1.329 -  assumes inf_Sup: "a \<sqinter> \<Squnion>B = (\<Squnion>b\<in>B. a \<sqinter> b)"
   1.330 +    and inf_Sup: "a \<sqinter> \<Squnion>B = (\<Squnion>b\<in>B. a \<sqinter> b)"
   1.331  begin
   1.332  
   1.333 -lemma sup_INF:
   1.334 -  "a \<squnion> (\<Sqinter>b\<in>B. f b) = (\<Sqinter>b\<in>B. a \<squnion> f b)"
   1.335 +lemma sup_INF: "a \<squnion> (\<Sqinter>b\<in>B. f b) = (\<Sqinter>b\<in>B. a \<squnion> f b)"
   1.336    by (simp add: sup_Inf)
   1.337  
   1.338 -lemma inf_SUP:
   1.339 -  "a \<sqinter> (\<Squnion>b\<in>B. f b) = (\<Squnion>b\<in>B. a \<sqinter> f b)"
   1.340 +lemma inf_SUP: "a \<sqinter> (\<Squnion>b\<in>B. f b) = (\<Squnion>b\<in>B. a \<sqinter> f b)"
   1.341    by (simp add: inf_Sup)
   1.342  
   1.343  lemma dual_complete_distrib_lattice:
   1.344    "class.complete_distrib_lattice Sup Inf sup (op \<ge>) (op >) inf \<top> \<bottom>"
   1.345    apply (rule class.complete_distrib_lattice.intro)
   1.346 -  apply (fact dual_complete_lattice)
   1.347 +   apply (fact dual_complete_lattice)
   1.348    apply (rule class.complete_distrib_lattice_axioms.intro)
   1.349 -  apply (simp_all add: inf_Sup sup_Inf)
   1.350 +   apply (simp_all add: inf_Sup sup_Inf)
   1.351    done
   1.352  
   1.353 -subclass distrib_lattice proof
   1.354 +subclass distrib_lattice
   1.355 +proof
   1.356    fix a b c
   1.357 -  from sup_Inf have "a \<squnion> \<Sqinter>{b, c} = (\<Sqinter>d\<in>{b, c}. a \<squnion> d)" .
   1.358 +  have "a \<squnion> \<Sqinter>{b, c} = (\<Sqinter>d\<in>{b, c}. a \<squnion> d)" by (rule sup_Inf)
   1.359    then show "a \<squnion> b \<sqinter> c = (a \<squnion> b) \<sqinter> (a \<squnion> c)" by simp
   1.360  qed
   1.361  
   1.362 -lemma Inf_sup:
   1.363 -  "\<Sqinter>B \<squnion> a = (\<Sqinter>b\<in>B. b \<squnion> a)"
   1.364 +lemma Inf_sup: "\<Sqinter>B \<squnion> a = (\<Sqinter>b\<in>B. b \<squnion> a)"
   1.365    by (simp add: sup_Inf sup_commute)
   1.366  
   1.367 -lemma Sup_inf:
   1.368 -  "\<Squnion>B \<sqinter> a = (\<Squnion>b\<in>B. b \<sqinter> a)"
   1.369 +lemma Sup_inf: "\<Squnion>B \<sqinter> a = (\<Squnion>b\<in>B. b \<sqinter> a)"
   1.370    by (simp add: inf_Sup inf_commute)
   1.371  
   1.372 -lemma INF_sup: 
   1.373 -  "(\<Sqinter>b\<in>B. f b) \<squnion> a = (\<Sqinter>b\<in>B. f b \<squnion> a)"
   1.374 +lemma INF_sup: "(\<Sqinter>b\<in>B. f b) \<squnion> a = (\<Sqinter>b\<in>B. f b \<squnion> a)"
   1.375    by (simp add: sup_INF sup_commute)
   1.376  
   1.377 -lemma SUP_inf:
   1.378 -  "(\<Squnion>b\<in>B. f b) \<sqinter> a = (\<Squnion>b\<in>B. f b \<sqinter> a)"
   1.379 +lemma SUP_inf: "(\<Squnion>b\<in>B. f b) \<sqinter> a = (\<Squnion>b\<in>B. f b \<sqinter> a)"
   1.380    by (simp add: inf_SUP inf_commute)
   1.381  
   1.382 -lemma Inf_sup_eq_top_iff:
   1.383 -  "(\<Sqinter>B \<squnion> a = \<top>) \<longleftrightarrow> (\<forall>b\<in>B. b \<squnion> a = \<top>)"
   1.384 +lemma Inf_sup_eq_top_iff: "(\<Sqinter>B \<squnion> a = \<top>) \<longleftrightarrow> (\<forall>b\<in>B. b \<squnion> a = \<top>)"
   1.385    by (simp only: Inf_sup INF_top_conv)
   1.386  
   1.387 -lemma Sup_inf_eq_bot_iff:
   1.388 -  "(\<Squnion>B \<sqinter> a = \<bottom>) \<longleftrightarrow> (\<forall>b\<in>B. b \<sqinter> a = \<bottom>)"
   1.389 +lemma Sup_inf_eq_bot_iff: "(\<Squnion>B \<sqinter> a = \<bottom>) \<longleftrightarrow> (\<forall>b\<in>B. b \<sqinter> a = \<bottom>)"
   1.390    by (simp only: Sup_inf SUP_bot_conv)
   1.391  
   1.392 -lemma INF_sup_distrib2:
   1.393 -  "(\<Sqinter>a\<in>A. f a) \<squnion> (\<Sqinter>b\<in>B. g b) = (\<Sqinter>a\<in>A. \<Sqinter>b\<in>B. f a \<squnion> g b)"
   1.394 +lemma INF_sup_distrib2: "(\<Sqinter>a\<in>A. f a) \<squnion> (\<Sqinter>b\<in>B. g b) = (\<Sqinter>a\<in>A. \<Sqinter>b\<in>B. f a \<squnion> g b)"
   1.395    by (subst INF_commute) (simp add: sup_INF INF_sup)
   1.396  
   1.397 -lemma SUP_inf_distrib2:
   1.398 -  "(\<Squnion>a\<in>A. f a) \<sqinter> (\<Squnion>b\<in>B. g b) = (\<Squnion>a\<in>A. \<Squnion>b\<in>B. f a \<sqinter> g b)"
   1.399 +lemma SUP_inf_distrib2: "(\<Squnion>a\<in>A. f a) \<sqinter> (\<Squnion>b\<in>B. g b) = (\<Squnion>a\<in>A. \<Squnion>b\<in>B. f a \<sqinter> g b)"
   1.400    by (subst SUP_commute) (simp add: inf_SUP SUP_inf)
   1.401  
   1.402  context
   1.403 @@ -541,20 +513,16 @@
   1.404    assumes "mono f"
   1.405  begin
   1.406  
   1.407 -lemma mono_Inf:
   1.408 -  shows "f (\<Sqinter>A) \<le> (\<Sqinter>x\<in>A. f x)"
   1.409 +lemma mono_Inf: "f (\<Sqinter>A) \<le> (\<Sqinter>x\<in>A. f x)"
   1.410    using \<open>mono f\<close> by (auto intro: complete_lattice_class.INF_greatest Inf_lower dest: monoD)
   1.411  
   1.412 -lemma mono_Sup:
   1.413 -  shows "(\<Squnion>x\<in>A. f x) \<le> f (\<Squnion>A)"
   1.414 +lemma mono_Sup: "(\<Squnion>x\<in>A. f x) \<le> f (\<Squnion>A)"
   1.415    using \<open>mono f\<close> by (auto intro: complete_lattice_class.SUP_least Sup_upper dest: monoD)
   1.416  
   1.417 -lemma mono_INF:
   1.418 -  "f (INF i : I. A i) \<le> (INF x : I. f (A x))"
   1.419 +lemma mono_INF: "f (INF i : I. A i) \<le> (INF x : I. f (A x))"
   1.420    by (intro complete_lattice_class.INF_greatest monoD[OF \<open>mono f\<close>] INF_lower)
   1.421  
   1.422 -lemma mono_SUP:
   1.423 -  "(SUP x : I. f (A x)) \<le> f (SUP i : I. A i)"
   1.424 +lemma mono_SUP: "(SUP x : I. f (A x)) \<le> f (SUP i : I. A i)"
   1.425    by (intro complete_lattice_class.SUP_least monoD[OF \<open>mono f\<close>] SUP_upper)
   1.426  
   1.427  end
   1.428 @@ -566,10 +534,11 @@
   1.429  
   1.430  lemma dual_complete_boolean_algebra:
   1.431    "class.complete_boolean_algebra Sup Inf sup (op \<ge>) (op >) inf \<top> \<bottom> (\<lambda>x y. x \<squnion> - y) uminus"
   1.432 -  by (rule class.complete_boolean_algebra.intro, rule dual_complete_distrib_lattice, rule dual_boolean_algebra)
   1.433 +  by (rule class.complete_boolean_algebra.intro,
   1.434 +      rule dual_complete_distrib_lattice,
   1.435 +      rule dual_boolean_algebra)
   1.436  
   1.437 -lemma uminus_Inf:
   1.438 -  "- (\<Sqinter>A) = \<Squnion>(uminus ` A)"
   1.439 +lemma uminus_Inf: "- (\<Sqinter>A) = \<Squnion>(uminus ` A)"
   1.440  proof (rule antisym)
   1.441    show "- \<Sqinter>A \<le> \<Squnion>(uminus ` A)"
   1.442      by (rule compl_le_swap2, rule Inf_greatest, rule compl_le_swap2, rule Sup_upper) simp
   1.443 @@ -580,13 +549,13 @@
   1.444  lemma uminus_INF: "- (\<Sqinter>x\<in>A. B x) = (\<Squnion>x\<in>A. - B x)"
   1.445    by (simp add: uminus_Inf image_image)
   1.446  
   1.447 -lemma uminus_Sup:
   1.448 -  "- (\<Squnion>A) = \<Sqinter>(uminus ` A)"
   1.449 +lemma uminus_Sup: "- (\<Squnion>A) = \<Sqinter>(uminus ` A)"
   1.450  proof -
   1.451 -  have "\<Squnion>A = - \<Sqinter>(uminus ` A)" by (simp add: image_image uminus_INF)
   1.452 +  have "\<Squnion>A = - \<Sqinter>(uminus ` A)"
   1.453 +    by (simp add: image_image uminus_INF)
   1.454    then show ?thesis by simp
   1.455  qed
   1.456 -  
   1.457 +
   1.458  lemma uminus_SUP: "- (\<Squnion>x\<in>A. B x) = (\<Sqinter>x\<in>A. - B x)"
   1.459    by (simp add: uminus_Sup image_image)
   1.460  
   1.461 @@ -605,29 +574,27 @@
   1.462  lemma complete_linorder_sup_max: "sup = max"
   1.463    by (auto intro: antisym simp add: max_def fun_eq_iff)
   1.464  
   1.465 -lemma Inf_less_iff:
   1.466 -  "\<Sqinter>S \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>S. x \<sqsubset> a)"
   1.467 +lemma Inf_less_iff: "\<Sqinter>S \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>S. x \<sqsubset> a)"
   1.468    by (simp add: not_le [symmetric] le_Inf_iff)
   1.469  
   1.470 -lemma INF_less_iff:
   1.471 -  "(\<Sqinter>i\<in>A. f i) \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>A. f x \<sqsubset> a)"
   1.472 +lemma INF_less_iff: "(\<Sqinter>i\<in>A. f i) \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>A. f x \<sqsubset> a)"
   1.473    by (simp add: Inf_less_iff [of "f ` A"])
   1.474  
   1.475 -lemma less_Sup_iff:
   1.476 -  "a \<sqsubset> \<Squnion>S \<longleftrightarrow> (\<exists>x\<in>S. a \<sqsubset> x)"
   1.477 +lemma less_Sup_iff: "a \<sqsubset> \<Squnion>S \<longleftrightarrow> (\<exists>x\<in>S. a \<sqsubset> x)"
   1.478    by (simp add: not_le [symmetric] Sup_le_iff)
   1.479  
   1.480 -lemma less_SUP_iff:
   1.481 -  "a \<sqsubset> (\<Squnion>i\<in>A. f i) \<longleftrightarrow> (\<exists>x\<in>A. a \<sqsubset> f x)"
   1.482 +lemma less_SUP_iff: "a \<sqsubset> (\<Squnion>i\<in>A. f i) \<longleftrightarrow> (\<exists>x\<in>A. a \<sqsubset> f x)"
   1.483    by (simp add: less_Sup_iff [of _ "f ` A"])
   1.484  
   1.485 -lemma Sup_eq_top_iff [simp]:
   1.486 -  "\<Squnion>A = \<top> \<longleftrightarrow> (\<forall>x<\<top>. \<exists>i\<in>A. x < i)"
   1.487 +lemma Sup_eq_top_iff [simp]: "\<Squnion>A = \<top> \<longleftrightarrow> (\<forall>x<\<top>. \<exists>i\<in>A. x < i)"
   1.488  proof
   1.489    assume *: "\<Squnion>A = \<top>"
   1.490 -  show "(\<forall>x<\<top>. \<exists>i\<in>A. x < i)" unfolding * [symmetric]
   1.491 +  show "(\<forall>x<\<top>. \<exists>i\<in>A. x < i)"
   1.492 +    unfolding * [symmetric]
   1.493    proof (intro allI impI)
   1.494 -    fix x assume "x < \<Squnion>A" then show "\<exists>i\<in>A. x < i"
   1.495 +    fix x
   1.496 +    assume "x < \<Squnion>A"
   1.497 +    then show "\<exists>i\<in>A. x < i"
   1.498        by (simp add: less_Sup_iff)
   1.499    qed
   1.500  next
   1.501 @@ -635,42 +602,40 @@
   1.502    show "\<Squnion>A = \<top>"
   1.503    proof (rule ccontr)
   1.504      assume "\<Squnion>A \<noteq> \<top>"
   1.505 -    with top_greatest [of "\<Squnion>A"]
   1.506 -    have "\<Squnion>A < \<top>" unfolding le_less by auto
   1.507 -    then have "\<Squnion>A < \<Squnion>A"
   1.508 -      using * unfolding less_Sup_iff by auto
   1.509 +    with top_greatest [of "\<Squnion>A"] have "\<Squnion>A < \<top>"
   1.510 +      unfolding le_less by auto
   1.511 +    with * have "\<Squnion>A < \<Squnion>A"
   1.512 +      unfolding less_Sup_iff by auto
   1.513      then show False by auto
   1.514    qed
   1.515  qed
   1.516  
   1.517 -lemma SUP_eq_top_iff [simp]:
   1.518 -  "(\<Squnion>i\<in>A. f i) = \<top> \<longleftrightarrow> (\<forall>x<\<top>. \<exists>i\<in>A. x < f i)"
   1.519 +lemma SUP_eq_top_iff [simp]: "(\<Squnion>i\<in>A. f i) = \<top> \<longleftrightarrow> (\<forall>x<\<top>. \<exists>i\<in>A. x < f i)"
   1.520    using Sup_eq_top_iff [of "f ` A"] by simp
   1.521  
   1.522 -lemma Inf_eq_bot_iff [simp]:
   1.523 -  "\<Sqinter>A = \<bottom> \<longleftrightarrow> (\<forall>x>\<bottom>. \<exists>i\<in>A. i < x)"
   1.524 +lemma Inf_eq_bot_iff [simp]: "\<Sqinter>A = \<bottom> \<longleftrightarrow> (\<forall>x>\<bottom>. \<exists>i\<in>A. i < x)"
   1.525    using dual_complete_linorder
   1.526    by (rule complete_linorder.Sup_eq_top_iff)
   1.527  
   1.528 -lemma INF_eq_bot_iff [simp]:
   1.529 -  "(\<Sqinter>i\<in>A. f i) = \<bottom> \<longleftrightarrow> (\<forall>x>\<bottom>. \<exists>i\<in>A. f i < x)"
   1.530 +lemma INF_eq_bot_iff [simp]: "(\<Sqinter>i\<in>A. f i) = \<bottom> \<longleftrightarrow> (\<forall>x>\<bottom>. \<exists>i\<in>A. f i < x)"
   1.531    using Inf_eq_bot_iff [of "f ` A"] by simp
   1.532  
   1.533  lemma Inf_le_iff: "\<Sqinter>A \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>a\<in>A. y > a)"
   1.534  proof safe
   1.535 -  fix y assume "x \<ge> \<Sqinter>A" "y > x"
   1.536 +  fix y
   1.537 +  assume "x \<ge> \<Sqinter>A" "y > x"
   1.538    then have "y > \<Sqinter>A" by auto
   1.539    then show "\<exists>a\<in>A. y > a"
   1.540      unfolding Inf_less_iff .
   1.541  qed (auto elim!: allE[of _ "\<Sqinter>A"] simp add: not_le[symmetric] Inf_lower)
   1.542  
   1.543 -lemma INF_le_iff:
   1.544 -  "INFIMUM A f \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>i\<in>A. y > f i)"
   1.545 +lemma INF_le_iff: "INFIMUM A f \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>i\<in>A. y > f i)"
   1.546    using Inf_le_iff [of "f ` A"] by simp
   1.547  
   1.548  lemma le_Sup_iff: "x \<le> \<Squnion>A \<longleftrightarrow> (\<forall>y<x. \<exists>a\<in>A. y < a)"
   1.549  proof safe
   1.550 -  fix y assume "x \<le> \<Squnion>A" "y < x"
   1.551 +  fix y
   1.552 +  assume "x \<le> \<Squnion>A" "y < x"
   1.553    then have "y < \<Squnion>A" by auto
   1.554    then show "\<exists>a\<in>A. y < a"
   1.555      unfolding less_Sup_iff .
   1.556 @@ -696,35 +661,29 @@
   1.557  instantiation bool :: complete_lattice
   1.558  begin
   1.559  
   1.560 -definition
   1.561 -  [simp, code]: "\<Sqinter>A \<longleftrightarrow> False \<notin> A"
   1.562 +definition [simp, code]: "\<Sqinter>A \<longleftrightarrow> False \<notin> A"
   1.563  
   1.564 -definition
   1.565 -  [simp, code]: "\<Squnion>A \<longleftrightarrow> True \<in> A"
   1.566 +definition [simp, code]: "\<Squnion>A \<longleftrightarrow> True \<in> A"
   1.567  
   1.568 -instance proof
   1.569 -qed (auto intro: bool_induct)
   1.570 +instance
   1.571 +  by standard (auto intro: bool_induct)
   1.572  
   1.573  end
   1.574  
   1.575 -lemma not_False_in_image_Ball [simp]:
   1.576 -  "False \<notin> P ` A \<longleftrightarrow> Ball A P"
   1.577 +lemma not_False_in_image_Ball [simp]: "False \<notin> P ` A \<longleftrightarrow> Ball A P"
   1.578    by auto
   1.579  
   1.580 -lemma True_in_image_Bex [simp]:
   1.581 -  "True \<in> P ` A \<longleftrightarrow> Bex A P"
   1.582 +lemma True_in_image_Bex [simp]: "True \<in> P ` A \<longleftrightarrow> Bex A P"
   1.583    by auto
   1.584  
   1.585 -lemma INF_bool_eq [simp]:
   1.586 -  "INFIMUM = Ball"
   1.587 +lemma INF_bool_eq [simp]: "INFIMUM = Ball"
   1.588    by (simp add: fun_eq_iff)
   1.589  
   1.590 -lemma SUP_bool_eq [simp]:
   1.591 -  "SUPREMUM = Bex"
   1.592 +lemma SUP_bool_eq [simp]: "SUPREMUM = Bex"
   1.593    by (simp add: fun_eq_iff)
   1.594  
   1.595 -instance bool :: complete_boolean_algebra proof
   1.596 -qed (auto intro: bool_induct)
   1.597 +instance bool :: complete_boolean_algebra
   1.598 +  by standard (auto intro: bool_induct)
   1.599  
   1.600  
   1.601  subsection \<open>Complete lattice on @{typ "_ \<Rightarrow> _"}\<close>
   1.602 @@ -732,11 +691,9 @@
   1.603  instantiation "fun" :: (type, Inf) Inf
   1.604  begin
   1.605  
   1.606 -definition
   1.607 -  "\<Sqinter>A = (\<lambda>x. \<Sqinter>f\<in>A. f x)"
   1.608 +definition "\<Sqinter>A = (\<lambda>x. \<Sqinter>f\<in>A. f x)"
   1.609  
   1.610 -lemma Inf_apply [simp, code]:
   1.611 -  "(\<Sqinter>A) x = (\<Sqinter>f\<in>A. f x)"
   1.612 +lemma Inf_apply [simp, code]: "(\<Sqinter>A) x = (\<Sqinter>f\<in>A. f x)"
   1.613    by (simp add: Inf_fun_def)
   1.614  
   1.615  instance ..
   1.616 @@ -746,11 +703,9 @@
   1.617  instantiation "fun" :: (type, Sup) Sup
   1.618  begin
   1.619  
   1.620 -definition
   1.621 -  "\<Squnion>A = (\<lambda>x. \<Squnion>f\<in>A. f x)"
   1.622 +definition "\<Squnion>A = (\<lambda>x. \<Squnion>f\<in>A. f x)"
   1.623  
   1.624 -lemma Sup_apply [simp, code]:
   1.625 -  "(\<Squnion>A) x = (\<Squnion>f\<in>A. f x)"
   1.626 +lemma Sup_apply [simp, code]: "(\<Squnion>A) x = (\<Squnion>f\<in>A. f x)"
   1.627    by (simp add: Sup_fun_def)
   1.628  
   1.629  instance ..
   1.630 @@ -760,57 +715,47 @@
   1.631  instantiation "fun" :: (type, complete_lattice) complete_lattice
   1.632  begin
   1.633  
   1.634 -instance proof
   1.635 -qed (auto simp add: le_fun_def intro: INF_lower INF_greatest SUP_upper SUP_least)
   1.636 +instance
   1.637 +  by standard (auto simp add: le_fun_def intro: INF_lower INF_greatest SUP_upper SUP_least)
   1.638  
   1.639  end
   1.640  
   1.641 -lemma INF_apply [simp]:
   1.642 -  "(\<Sqinter>y\<in>A. f y) x = (\<Sqinter>y\<in>A. f y x)"
   1.643 +lemma INF_apply [simp]: "(\<Sqinter>y\<in>A. f y) x = (\<Sqinter>y\<in>A. f y x)"
   1.644    using Inf_apply [of "f ` A"] by (simp add: comp_def)
   1.645  
   1.646 -lemma SUP_apply [simp]:
   1.647 -  "(\<Squnion>y\<in>A. f y) x = (\<Squnion>y\<in>A. f y x)"
   1.648 +lemma SUP_apply [simp]: "(\<Squnion>y\<in>A. f y) x = (\<Squnion>y\<in>A. f y x)"
   1.649    using Sup_apply [of "f ` A"] by (simp add: comp_def)
   1.650  
   1.651 -instance "fun" :: (type, complete_distrib_lattice) complete_distrib_lattice proof
   1.652 -qed (auto simp add: inf_Sup sup_Inf fun_eq_iff image_image)
   1.653 +instance "fun" :: (type, complete_distrib_lattice) complete_distrib_lattice
   1.654 +  by standard (auto simp add: inf_Sup sup_Inf fun_eq_iff image_image)
   1.655  
   1.656  instance "fun" :: (type, complete_boolean_algebra) complete_boolean_algebra ..
   1.657  
   1.658  
   1.659  subsection \<open>Complete lattice on unary and binary predicates\<close>
   1.660  
   1.661 -lemma Inf1_I: 
   1.662 -  "(\<And>P. P \<in> A \<Longrightarrow> P a) \<Longrightarrow> (\<Sqinter>A) a"
   1.663 +lemma Inf1_I: "(\<And>P. P \<in> A \<Longrightarrow> P a) \<Longrightarrow> (\<Sqinter>A) a"
   1.664    by auto
   1.665  
   1.666 -lemma INF1_I:
   1.667 -  "(\<And>x. x \<in> A \<Longrightarrow> B x b) \<Longrightarrow> (\<Sqinter>x\<in>A. B x) b"
   1.668 +lemma INF1_I: "(\<And>x. x \<in> A \<Longrightarrow> B x b) \<Longrightarrow> (\<Sqinter>x\<in>A. B x) b"
   1.669    by simp
   1.670  
   1.671 -lemma INF2_I:
   1.672 -  "(\<And>x. x \<in> A \<Longrightarrow> B x b c) \<Longrightarrow> (\<Sqinter>x\<in>A. B x) b c"
   1.673 +lemma INF2_I: "(\<And>x. x \<in> A \<Longrightarrow> B x b c) \<Longrightarrow> (\<Sqinter>x\<in>A. B x) b c"
   1.674    by simp
   1.675  
   1.676 -lemma Inf2_I: 
   1.677 -  "(\<And>r. r \<in> A \<Longrightarrow> r a b) \<Longrightarrow> (\<Sqinter>A) a b"
   1.678 +lemma Inf2_I: "(\<And>r. r \<in> A \<Longrightarrow> r a b) \<Longrightarrow> (\<Sqinter>A) a b"
   1.679    by auto
   1.680  
   1.681 -lemma Inf1_D:
   1.682 -  "(\<Sqinter>A) a \<Longrightarrow> P \<in> A \<Longrightarrow> P a"
   1.683 +lemma Inf1_D: "(\<Sqinter>A) a \<Longrightarrow> P \<in> A \<Longrightarrow> P a"
   1.684    by auto
   1.685  
   1.686 -lemma INF1_D:
   1.687 -  "(\<Sqinter>x\<in>A. B x) b \<Longrightarrow> a \<in> A \<Longrightarrow> B a b"
   1.688 +lemma INF1_D: "(\<Sqinter>x\<in>A. B x) b \<Longrightarrow> a \<in> A \<Longrightarrow> B a b"
   1.689    by simp
   1.690  
   1.691 -lemma Inf2_D:
   1.692 -  "(\<Sqinter>A) a b \<Longrightarrow> r \<in> A \<Longrightarrow> r a b"
   1.693 +lemma Inf2_D: "(\<Sqinter>A) a b \<Longrightarrow> r \<in> A \<Longrightarrow> r a b"
   1.694    by auto
   1.695  
   1.696 -lemma INF2_D:
   1.697 -  "(\<Sqinter>x\<in>A. B x) b c \<Longrightarrow> a \<in> A \<Longrightarrow> B a b c"
   1.698 +lemma INF2_D: "(\<Sqinter>x\<in>A. B x) b c \<Longrightarrow> a \<in> A \<Longrightarrow> B a b c"
   1.699    by simp
   1.700  
   1.701  lemma Inf1_E:
   1.702 @@ -833,20 +778,16 @@
   1.703    obtains "B a b c" | "a \<notin> A"
   1.704    using assms by auto
   1.705  
   1.706 -lemma Sup1_I:
   1.707 -  "P \<in> A \<Longrightarrow> P a \<Longrightarrow> (\<Squnion>A) a"
   1.708 +lemma Sup1_I: "P \<in> A \<Longrightarrow> P a \<Longrightarrow> (\<Squnion>A) a"
   1.709    by auto
   1.710  
   1.711 -lemma SUP1_I:
   1.712 -  "a \<in> A \<Longrightarrow> B a b \<Longrightarrow> (\<Squnion>x\<in>A. B x) b"
   1.713 +lemma SUP1_I: "a \<in> A \<Longrightarrow> B a b \<Longrightarrow> (\<Squnion>x\<in>A. B x) b"
   1.714    by auto
   1.715  
   1.716 -lemma Sup2_I:
   1.717 -  "r \<in> A \<Longrightarrow> r a b \<Longrightarrow> (\<Squnion>A) a b"
   1.718 +lemma Sup2_I: "r \<in> A \<Longrightarrow> r a b \<Longrightarrow> (\<Squnion>A) a b"
   1.719    by auto
   1.720  
   1.721 -lemma SUP2_I:
   1.722 -  "a \<in> A \<Longrightarrow> B a b c \<Longrightarrow> (\<Squnion>x\<in>A. B x) b c"
   1.723 +lemma SUP2_I: "a \<in> A \<Longrightarrow> B a b c \<Longrightarrow> (\<Squnion>x\<in>A. B x) b c"
   1.724    by auto
   1.725  
   1.726  lemma Sup1_E:
   1.727 @@ -875,29 +816,25 @@
   1.728  instantiation "set" :: (type) complete_lattice
   1.729  begin
   1.730  
   1.731 -definition
   1.732 -  "\<Sqinter>A = {x. \<Sqinter>((\<lambda>B. x \<in> B) ` A)}"
   1.733 +definition "\<Sqinter>A = {x. \<Sqinter>((\<lambda>B. x \<in> B) ` A)}"
   1.734  
   1.735 -definition
   1.736 -  "\<Squnion>A = {x. \<Squnion>((\<lambda>B. x \<in> B) ` A)}"
   1.737 +definition "\<Squnion>A = {x. \<Squnion>((\<lambda>B. x \<in> B) ` A)}"
   1.738  
   1.739 -instance proof
   1.740 -qed (auto simp add: less_eq_set_def Inf_set_def Sup_set_def le_fun_def)
   1.741 +instance
   1.742 +  by standard (auto simp add: less_eq_set_def Inf_set_def Sup_set_def le_fun_def)
   1.743  
   1.744  end
   1.745  
   1.746  instance "set" :: (type) complete_boolean_algebra
   1.747 -proof
   1.748 -qed (auto simp add: Inf_set_def Sup_set_def image_def)
   1.749 -  
   1.750 +  by standard (auto simp add: Inf_set_def Sup_set_def image_def)
   1.751 +
   1.752  
   1.753  subsubsection \<open>Inter\<close>
   1.754  
   1.755  abbreviation Inter :: "'a set set \<Rightarrow> 'a set"  ("\<Inter>_" [900] 900)
   1.756    where "\<Inter>S \<equiv> \<Sqinter>S"
   1.757 -  
   1.758 -lemma Inter_eq:
   1.759 -  "\<Inter>A = {x. \<forall>B \<in> A. x \<in> B}"
   1.760 +
   1.761 +lemma Inter_eq: "\<Inter>A = {x. \<forall>B \<in> A. x \<in> B}"
   1.762  proof (rule set_eqI)
   1.763    fix x
   1.764    have "(\<forall>Q\<in>{P. \<exists>B\<in>A. P \<longleftrightarrow> x \<in> B}. Q) \<longleftrightarrow> (\<forall>B\<in>A. x \<in> B)"
   1.765 @@ -913,7 +850,7 @@
   1.766    by (simp add: Inter_eq)
   1.767  
   1.768  text \<open>
   1.769 -  \medskip A ``destruct'' rule -- every @{term X} in @{term C}
   1.770 +  \<^medskip> A ``destruct'' rule -- every @{term X} in @{term C}
   1.771    contains @{term A} as an element, but @{prop "A \<in> X"} can hold when
   1.772    @{prop "X \<in> C"} does not!  This rule is analogous to \<open>spec\<close>.
   1.773  \<close>
   1.774 @@ -924,13 +861,12 @@
   1.775  lemma InterE [elim]: "A \<in> \<Inter>C \<Longrightarrow> (X \<notin> C \<Longrightarrow> R) \<Longrightarrow> (A \<in> X \<Longrightarrow> R) \<Longrightarrow> R"
   1.776    \<comment> \<open>``Classical'' elimination rule -- does not require proving
   1.777      @{prop "X \<in> C"}.\<close>
   1.778 -  by (unfold Inter_eq) blast
   1.779 +  unfolding Inter_eq by blast
   1.780  
   1.781  lemma Inter_lower: "B \<in> A \<Longrightarrow> \<Inter>A \<subseteq> B"
   1.782    by (fact Inf_lower)
   1.783  
   1.784 -lemma Inter_subset:
   1.785 -  "(\<And>X. X \<in> A \<Longrightarrow> X \<subseteq> B) \<Longrightarrow> A \<noteq> {} \<Longrightarrow> \<Inter>A \<subseteq> B"
   1.786 +lemma Inter_subset: "(\<And>X. X \<in> A \<Longrightarrow> X \<subseteq> B) \<Longrightarrow> A \<noteq> {} \<Longrightarrow> \<Inter>A \<subseteq> B"
   1.787    by (fact Inf_less_eq)
   1.788  
   1.789  lemma Inter_greatest: "(\<And>X. X \<in> A \<Longrightarrow> C \<subseteq> X) \<Longrightarrow> C \<subseteq> \<Inter>A"
   1.790 @@ -992,8 +928,7 @@
   1.791    [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax INTER} @{syntax_const "_INTER"}]
   1.792  \<close> \<comment> \<open>to avoid eta-contraction of body\<close>
   1.793  
   1.794 -lemma INTER_eq:
   1.795 -  "(\<Inter>x\<in>A. B x) = {y. \<forall>x\<in>A. y \<in> B x}"
   1.796 +lemma INTER_eq: "(\<Inter>x\<in>A. B x) = {y. \<forall>x\<in>A. y \<in> B x}"
   1.797    by (auto intro!: INF_eqI)
   1.798  
   1.799  lemma INT_iff [simp]: "b \<in> (\<Inter>x\<in>A. B x) \<longleftrightarrow> (\<forall>x\<in>A. b \<in> B x)"
   1.800 @@ -1036,23 +971,21 @@
   1.801  lemma INT_Un: "(\<Inter>i \<in> A \<union> B. M i) = (\<Inter>i \<in> A. M i) \<inter> (\<Inter>i\<in>B. M i)"
   1.802    by (fact INF_union)
   1.803  
   1.804 -lemma INT_insert_distrib:
   1.805 -  "u \<in> A \<Longrightarrow> (\<Inter>x\<in>A. insert a (B x)) = insert a (\<Inter>x\<in>A. B x)"
   1.806 +lemma INT_insert_distrib: "u \<in> A \<Longrightarrow> (\<Inter>x\<in>A. insert a (B x)) = insert a (\<Inter>x\<in>A. B x)"
   1.807    by blast
   1.808  
   1.809  lemma INT_constant [simp]: "(\<Inter>y\<in>A. c) = (if A = {} then UNIV else c)"
   1.810    by (fact INF_constant)
   1.811  
   1.812  lemma INTER_UNIV_conv:
   1.813 - "(UNIV = (\<Inter>x\<in>A. B x)) = (\<forall>x\<in>A. B x = UNIV)"
   1.814 - "((\<Inter>x\<in>A. B x) = UNIV) = (\<forall>x\<in>A. B x = UNIV)"
   1.815 +  "(UNIV = (\<Inter>x\<in>A. B x)) = (\<forall>x\<in>A. B x = UNIV)"
   1.816 +  "((\<Inter>x\<in>A. B x) = UNIV) = (\<forall>x\<in>A. B x = UNIV)"
   1.817    by (fact INF_top_conv)+ (* already simp *)
   1.818  
   1.819  lemma INT_bool_eq: "(\<Inter>b. A b) = A True \<inter> A False"
   1.820    by (fact INF_UNIV_bool_expand)
   1.821  
   1.822 -lemma INT_anti_mono:
   1.823 -  "A \<subseteq> B \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<subseteq> g x) \<Longrightarrow> (\<Inter>x\<in>B. f x) \<subseteq> (\<Inter>x\<in>A. g x)"
   1.824 +lemma INT_anti_mono: "A \<subseteq> B \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<subseteq> g x) \<Longrightarrow> (\<Inter>x\<in>B. f x) \<subseteq> (\<Inter>x\<in>A. g x)"
   1.825    \<comment> \<open>The last inclusion is POSITIVE!\<close>
   1.826    by (fact INF_superset_mono)
   1.827  
   1.828 @@ -1068,8 +1001,7 @@
   1.829  abbreviation Union :: "'a set set \<Rightarrow> 'a set"  ("\<Union>_" [900] 900)
   1.830    where "\<Union>S \<equiv> \<Squnion>S"
   1.831  
   1.832 -lemma Union_eq:
   1.833 -  "\<Union>A = {x. \<exists>B \<in> A. x \<in> B}"
   1.834 +lemma Union_eq: "\<Union>A = {x. \<exists>B \<in> A. x \<in> B}"
   1.835  proof (rule set_eqI)
   1.836    fix x
   1.837    have "(\<exists>Q\<in>{P. \<exists>B\<in>A. P \<longleftrightarrow> x \<in> B}. Q) \<longleftrightarrow> (\<exists>B\<in>A. x \<in> B)"
   1.838 @@ -1078,18 +1010,15 @@
   1.839      by (simp add: Sup_set_def image_def)
   1.840  qed
   1.841  
   1.842 -lemma Union_iff [simp]:
   1.843 -  "A \<in> \<Union>C \<longleftrightarrow> (\<exists>X\<in>C. A\<in>X)"
   1.844 +lemma Union_iff [simp]: "A \<in> \<Union>C \<longleftrightarrow> (\<exists>X\<in>C. A\<in>X)"
   1.845    by (unfold Union_eq) blast
   1.846  
   1.847 -lemma UnionI [intro]:
   1.848 -  "X \<in> C \<Longrightarrow> A \<in> X \<Longrightarrow> A \<in> \<Union>C"
   1.849 +lemma UnionI [intro]: "X \<in> C \<Longrightarrow> A \<in> X \<Longrightarrow> A \<in> \<Union>C"
   1.850    \<comment> \<open>The order of the premises presupposes that @{term C} is rigid;
   1.851      @{term A} may be flexible.\<close>
   1.852    by auto
   1.853  
   1.854 -lemma UnionE [elim!]:
   1.855 -  "A \<in> \<Union>C \<Longrightarrow> (\<And>X. A \<in> X \<Longrightarrow> X \<in> C \<Longrightarrow> R) \<Longrightarrow> R"
   1.856 +lemma UnionE [elim!]: "A \<in> \<Union>C \<Longrightarrow> (\<And>X. A \<in> X \<Longrightarrow> X \<in> C \<Longrightarrow> R) \<Longrightarrow> R"
   1.857    by auto
   1.858  
   1.859  lemma Union_upper: "B \<in> A \<Longrightarrow> B \<subseteq> \<Union>A"
   1.860 @@ -1131,6 +1060,7 @@
   1.861  lemma Union_subsetI: "(\<And>x. x \<in> A \<Longrightarrow> \<exists>y. y \<in> B \<and> x \<subseteq> y) \<Longrightarrow> \<Union>A \<subseteq> \<Union>B"
   1.862    by blast
   1.863  
   1.864 +
   1.865  subsubsection \<open>Unions of families\<close>
   1.866  
   1.867  abbreviation UNION :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set"
   1.868 @@ -1169,16 +1099,13 @@
   1.869    [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax UNION} @{syntax_const "_UNION"}]
   1.870  \<close> \<comment> \<open>to avoid eta-contraction of body\<close>
   1.871  
   1.872 -lemma UNION_eq:
   1.873 -  "(\<Union>x\<in>A. B x) = {y. \<exists>x\<in>A. y \<in> B x}"
   1.874 +lemma UNION_eq: "(\<Union>x\<in>A. B x) = {y. \<exists>x\<in>A. y \<in> B x}"
   1.875    by (auto intro!: SUP_eqI)
   1.876  
   1.877 -lemma bind_UNION [code]:
   1.878 -  "Set.bind A f = UNION A f"
   1.879 +lemma bind_UNION [code]: "Set.bind A f = UNION A f"
   1.880    by (simp add: bind_def UNION_eq)
   1.881  
   1.882 -lemma member_bind [simp]:
   1.883 -  "x \<in> Set.bind P f \<longleftrightarrow> x \<in> UNION P f "
   1.884 +lemma member_bind [simp]: "x \<in> Set.bind P f \<longleftrightarrow> x \<in> UNION P f "
   1.885    by (simp add: bind_UNION)
   1.886  
   1.887  lemma Union_SetCompr_eq: "\<Union>{f x| x. P x} = {a. \<exists>x. P x \<and> a \<in> f x}"
   1.888 @@ -1281,6 +1208,7 @@
   1.889  lemma inj_on_image: "inj_on f (\<Union>A) \<Longrightarrow> inj_on (op ` f) A"
   1.890    unfolding inj_on_def by blast
   1.891  
   1.892 +
   1.893  subsubsection \<open>Distributive laws\<close>
   1.894  
   1.895  lemma Int_Union: "A \<inter> \<Union>B = (\<Union>C\<in>B. A \<inter> C)"
   1.896 @@ -1298,10 +1226,10 @@
   1.897  lemma UN_Un_distrib: "(\<Union>i\<in>I. A i \<union> B i) = (\<Union>i\<in>I. A i) \<union> (\<Union>i\<in>I. B i)"
   1.898    by (rule sym) (rule SUP_sup_distrib)
   1.899  
   1.900 -lemma Int_Inter_image: "(\<Inter>x\<in>C. A x \<inter> B x) = \<Inter>(A ` C) \<inter> \<Inter>(B ` C)" \<comment> \<open>FIXME drop\<close>
   1.901 +lemma Int_Inter_image: "(\<Inter>x\<in>C. A x \<inter> B x) = \<Inter>(A ` C) \<inter> \<Inter>(B ` C)"  (* FIXME drop *)
   1.902    by (simp add: INT_Int_distrib)
   1.903  
   1.904 -lemma Un_Union_image: "(\<Union>x\<in>C. A x \<union> B x) = \<Union>(A ` C) \<union> \<Union>(B ` C)" \<comment> \<open>FIXME drop\<close>
   1.905 +lemma Un_Union_image: "(\<Union>x\<in>C. A x \<union> B x) = \<Union>(A ` C) \<union> \<Union>(B ` C)"  (* FIXME drop *)
   1.906    \<comment> \<open>Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5:\<close>
   1.907    \<comment> \<open>Union of a family of unions\<close>
   1.908    by (simp add: UN_Un_distrib)
   1.909 @@ -1323,86 +1251,82 @@
   1.910    by (fact Sup_inf_eq_bot_iff)
   1.911  
   1.912  lemma SUP_UNION: "(SUP x:(UN y:A. g y). f x) = (SUP y:A. SUP x:g y. f x :: _ :: complete_lattice)"
   1.913 -by(rule order_antisym)(blast intro: SUP_least SUP_upper2)+
   1.914 +  by (rule order_antisym) (blast intro: SUP_least SUP_upper2)+
   1.915 +
   1.916  
   1.917  subsection \<open>Injections and bijections\<close>
   1.918  
   1.919 -lemma inj_on_Inter:
   1.920 -  "S \<noteq> {} \<Longrightarrow> (\<And>A. A \<in> S \<Longrightarrow> inj_on f A) \<Longrightarrow> inj_on f (\<Inter>S)"
   1.921 +lemma inj_on_Inter: "S \<noteq> {} \<Longrightarrow> (\<And>A. A \<in> S \<Longrightarrow> inj_on f A) \<Longrightarrow> inj_on f (\<Inter>S)"
   1.922    unfolding inj_on_def by blast
   1.923  
   1.924 -lemma inj_on_INTER:
   1.925 -  "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> inj_on f (A i)) \<Longrightarrow> inj_on f (\<Inter>i \<in> I. A i)"
   1.926 +lemma inj_on_INTER: "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> inj_on f (A i)) \<Longrightarrow> inj_on f (\<Inter>i \<in> I. A i)"
   1.927    unfolding inj_on_def by safe simp
   1.928  
   1.929  lemma inj_on_UNION_chain:
   1.930 -  assumes CH: "\<And> i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> A i \<le> A j \<or> A j \<le> A i" and
   1.931 -         INJ: "\<And> i. i \<in> I \<Longrightarrow> inj_on f (A i)"
   1.932 +  assumes chain: "\<And>i j. i \<in> I \<Longrightarrow> j \<in> I \<Longrightarrow> A i \<le> A j \<or> A j \<le> A i"
   1.933 +    and inj: "\<And>i. i \<in> I \<Longrightarrow> inj_on f (A i)"
   1.934    shows "inj_on f (\<Union>i \<in> I. A i)"
   1.935  proof -
   1.936 -  {
   1.937 -    fix i j x y
   1.938 -    assume *: "i \<in> I" "j \<in> I" and **: "x \<in> A i" "y \<in> A j"
   1.939 -      and ***: "f x = f y"
   1.940 -    have "x = y"
   1.941 -    proof -
   1.942 -      {
   1.943 -        assume "A i \<le> A j"
   1.944 -        with ** have "x \<in> A j" by auto
   1.945 -        with INJ * ** *** have ?thesis
   1.946 -        by(auto simp add: inj_on_def)
   1.947 -      }
   1.948 -      moreover
   1.949 -      {
   1.950 -        assume "A j \<le> A i"
   1.951 -        with ** have "y \<in> A i" by auto
   1.952 -        with INJ * ** *** have ?thesis
   1.953 -        by(auto simp add: inj_on_def)
   1.954 -      }
   1.955 -      ultimately show ?thesis using CH * by blast
   1.956 -    qed
   1.957 -  }
   1.958 -  then show ?thesis by (unfold inj_on_def UNION_eq) auto
   1.959 +  have "x = y"
   1.960 +    if *: "i \<in> I" "j \<in> I"
   1.961 +    and **: "x \<in> A i" "y \<in> A j"
   1.962 +    and ***: "f x = f y"
   1.963 +    for i j x y
   1.964 +    using chain [OF *]
   1.965 +  proof
   1.966 +    assume "A i \<le> A j"
   1.967 +    with ** have "x \<in> A j" by auto
   1.968 +    with inj * ** *** show ?thesis
   1.969 +      by (auto simp add: inj_on_def)
   1.970 +  next
   1.971 +    assume "A j \<le> A i"
   1.972 +    with ** have "y \<in> A i" by auto
   1.973 +    with inj * ** *** show ?thesis
   1.974 +      by (auto simp add: inj_on_def)
   1.975 +  qed
   1.976 +  then show ?thesis
   1.977 +    by (unfold inj_on_def UNION_eq) auto
   1.978  qed
   1.979  
   1.980  lemma bij_betw_UNION_chain:
   1.981 -  assumes CH: "\<And> i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> A i \<le> A j \<or> A j \<le> A i" and
   1.982 -         BIJ: "\<And> i. i \<in> I \<Longrightarrow> bij_betw f (A i) (A' i)"
   1.983 +  assumes chain: "\<And>i j. i \<in> I \<Longrightarrow> j \<in> I \<Longrightarrow> A i \<le> A j \<or> A j \<le> A i"
   1.984 +    and bij: "\<And>i. i \<in> I \<Longrightarrow> bij_betw f (A i) (A' i)"
   1.985    shows "bij_betw f (\<Union>i \<in> I. A i) (\<Union>i \<in> I. A' i)"
   1.986 -proof (unfold bij_betw_def, auto)
   1.987 -  have "\<And> i. i \<in> I \<Longrightarrow> inj_on f (A i)"
   1.988 -  using BIJ bij_betw_def[of f] by auto
   1.989 -  thus "inj_on f (\<Union>i \<in> I. A i)"
   1.990 -  using CH inj_on_UNION_chain[of I A f] by auto
   1.991 +  unfolding bij_betw_def
   1.992 +proof auto  (* slow *)
   1.993 +  have "\<And>i. i \<in> I \<Longrightarrow> inj_on f (A i)"
   1.994 +    using bij bij_betw_def[of f] by auto
   1.995 +  then show "inj_on f (\<Union>i \<in> I. A i)"
   1.996 +    using chain inj_on_UNION_chain[of I A f] by auto
   1.997  next
   1.998    fix i x
   1.999    assume *: "i \<in> I" "x \<in> A i"
  1.1000 -  hence "f x \<in> A' i" using BIJ bij_betw_def[of f] by auto
  1.1001 -  thus "\<exists>j \<in> I. f x \<in> A' j" using * by blast
  1.1002 +  then have "f x \<in> A' i"
  1.1003 +    using bij bij_betw_def[of f] by auto
  1.1004 +  with * show "\<exists>j \<in> I. f x \<in> A' j" by blast
  1.1005  next
  1.1006    fix i x'
  1.1007    assume *: "i \<in> I" "x' \<in> A' i"
  1.1008 -  hence "\<exists>x \<in> A i. x' = f x" using BIJ bij_betw_def[of f] by blast
  1.1009 -  then have "\<exists>j \<in> I. \<exists>x \<in> A j. x' = f x"
  1.1010 -    using * by blast
  1.1011 -  then show "x' \<in> f ` (\<Union>x\<in>I. A x)" by blast
  1.1012 +  then have "\<exists>x \<in> A i. x' = f x"
  1.1013 +    using bij bij_betw_def[of f] by blast
  1.1014 +  with * have "\<exists>j \<in> I. \<exists>x \<in> A j. x' = f x"
  1.1015 +    by blast
  1.1016 +  then show "x' \<in> f ` (\<Union>x\<in>I. A x)"
  1.1017 +    by blast
  1.1018  qed
  1.1019  
  1.1020  (*injectivity's required.  Left-to-right inclusion holds even if A is empty*)
  1.1021 -lemma image_INT:
  1.1022 -   "[| inj_on f C;  ALL x:A. B x <= C;  j:A |]
  1.1023 -    ==> f ` (INTER A B) = (INT x:A. f ` B x)"
  1.1024 -  by (simp add: inj_on_def, auto) blast
  1.1025 +lemma image_INT: "inj_on f C \<Longrightarrow> \<forall>x\<in>A. B x \<subseteq> C \<Longrightarrow> j \<in> A \<Longrightarrow> f ` (INTER A B) = (INT x:A. f ` B x)"
  1.1026 +  by (auto simp add: inj_on_def) blast
  1.1027  
  1.1028 -lemma bij_image_INT: "bij f ==> f ` (INTER A B) = (INT x:A. f ` B x)"
  1.1029 -  apply (simp add: bij_def)
  1.1030 -  apply (simp add: inj_on_def surj_def)
  1.1031 +lemma bij_image_INT: "bij f \<Longrightarrow> f ` (INTER A B) = (INT x:A. f ` B x)"
  1.1032 +  apply (simp only: bij_def)
  1.1033 +  apply (simp only: inj_on_def surj_def)
  1.1034    apply auto
  1.1035    apply blast
  1.1036    done
  1.1037  
  1.1038 -lemma UNION_fun_upd:
  1.1039 -  "UNION J (A(i := B)) = UNION (J - {i}) A \<union> (if i \<in> J then B else {})"
  1.1040 +lemma UNION_fun_upd: "UNION J (A(i := B)) = UNION (J - {i}) A \<union> (if i \<in> J then B else {})"
  1.1041    by (auto simp add: set_eq_iff)
  1.1042  
  1.1043  lemma bij_betw_Pow:
  1.1044 @@ -1436,8 +1360,7 @@
  1.1045  
  1.1046  subsubsection \<open>Miniscoping and maxiscoping\<close>
  1.1047  
  1.1048 -text \<open>\medskip Miniscoping: pushing in quantifiers and big Unions
  1.1049 -           and Intersections.\<close>
  1.1050 +text \<open>\<^medskip> Miniscoping: pushing in quantifiers and big Unions and Intersections.\<close>
  1.1051  
  1.1052  lemma UN_simps [simp]:
  1.1053    "\<And>a B C. (\<Union>x\<in>C. insert a (B x)) = (if C={} then {} else insert a (\<Union>x\<in>C. B x))"
  1.1054 @@ -1473,7 +1396,7 @@
  1.1055    by auto
  1.1056  
  1.1057  
  1.1058 -text \<open>\medskip Maxiscoping: pulling out big Unions and Intersections.\<close>
  1.1059 +text \<open>\<^medskip> Maxiscoping: pulling out big Unions and Intersections.\<close>
  1.1060  
  1.1061  lemma UN_extend_simps:
  1.1062    "\<And>a B C. insert a (\<Union>x\<in>C. B x) = (if C={} then {a} else (\<Union>x\<in>C. insert a (B x)))"
  1.1063 @@ -1513,4 +1436,3 @@
  1.1064    \<comment> \<open>Each of these has ALREADY been added \<open>[simp]\<close> above.\<close>
  1.1065  
  1.1066  end
  1.1067 -
     2.1 --- a/src/HOL/Fun.thy	Mon Aug 01 13:51:17 2016 +0200
     2.2 +++ b/src/HOL/Fun.thy	Mon Aug 01 22:11:29 2016 +0200
     2.3 @@ -7,8 +7,8 @@
     2.4  section \<open>Notions about functions\<close>
     2.5  
     2.6  theory Fun
     2.7 -imports Set
     2.8 -keywords "functor" :: thy_goal
     2.9 +  imports Set
    2.10 +  keywords "functor" :: thy_goal
    2.11  begin
    2.12  
    2.13  lemma apply_inverse: "f x = u \<Longrightarrow> (\<And>x. P x \<Longrightarrow> g (f x) = x) \<Longrightarrow> P x \<Longrightarrow> x = g u"
    2.14 @@ -63,12 +63,10 @@
    2.15  lemma comp_id [simp]: "f \<circ> id = f"
    2.16    by (simp add: fun_eq_iff)
    2.17  
    2.18 -lemma comp_eq_dest:
    2.19 -  "a \<circ> b = c \<circ> d \<Longrightarrow> a (b v) = c (d v)"
    2.20 +lemma comp_eq_dest: "a \<circ> b = c \<circ> d \<Longrightarrow> a (b v) = c (d v)"
    2.21    by (simp add: fun_eq_iff)
    2.22  
    2.23 -lemma comp_eq_elim:
    2.24 -  "a \<circ> b = c \<circ> d \<Longrightarrow> ((\<And>v. a (b v) = c (d v)) \<Longrightarrow> R) \<Longrightarrow> R"
    2.25 +lemma comp_eq_elim: "a \<circ> b = c \<circ> d \<Longrightarrow> ((\<And>v. a (b v) = c (d v)) \<Longrightarrow> R) \<Longrightarrow> R"
    2.26    by (simp add: fun_eq_iff)
    2.27  
    2.28  lemma comp_eq_dest_lhs: "a \<circ> b = c \<Longrightarrow> a (b v) = c v"
    2.29 @@ -104,7 +102,7 @@
    2.30  
    2.31  subsection \<open>The Forward Composition Operator \<open>fcomp\<close>\<close>
    2.32  
    2.33 -definition fcomp :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'c" (infixl "\<circ>>" 60)
    2.34 +definition fcomp :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'c"  (infixl "\<circ>>" 60)
    2.35    where "f \<circ>> g = (\<lambda>x. g (f x))"
    2.36  
    2.37  lemma fcomp_apply [simp]:  "(f \<circ>> g) x = g (f x)"
    2.38 @@ -145,8 +143,10 @@
    2.39  definition bij_betw :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> bool"  \<comment> \<open>bijective\<close>
    2.40    where "bij_betw f A B \<longleftrightarrow> inj_on f A \<and> f ` A = B"
    2.41  
    2.42 -text \<open>A common special case: functions injective, surjective or bijective over
    2.43 -  the entire domain type.\<close>
    2.44 +text \<open>
    2.45 +  A common special case: functions injective, surjective or bijective over
    2.46 +  the entire domain type.
    2.47 +\<close>
    2.48  
    2.49  abbreviation "inj f \<equiv> inj_on f UNIV"
    2.50  
    2.51 @@ -212,7 +212,7 @@
    2.52  
    2.53  lemma inj_on_subset:
    2.54    assumes "inj_on f A"
    2.55 -  assumes "B \<subseteq> A"
    2.56 +    and "B \<subseteq> A"
    2.57    shows "inj_on f B"
    2.58  proof (rule inj_onI)
    2.59    fix a b
    2.60 @@ -296,7 +296,7 @@
    2.61    by (simp add: surj_def)
    2.62  
    2.63  lemma surjE: "surj f \<Longrightarrow> (\<And>x. y = f x \<Longrightarrow> C) \<Longrightarrow> C"
    2.64 -  by (simp add: surj_def, blast)
    2.65 +  by (simp add: surj_def) blast
    2.66  
    2.67  lemma comp_surj: "surj f \<Longrightarrow> surj g \<Longrightarrow> surj (g \<circ> f)"
    2.68    by (simp add: image_comp [symmetric])
    2.69 @@ -354,18 +354,19 @@
    2.70      using img
    2.71    proof (auto simp add: bij_betw_def)
    2.72      assume "inj_on (f' \<circ> f) A"
    2.73 -    then show "inj_on f A" using inj_on_imageI2 by blast
    2.74 +    then show "inj_on f A"
    2.75 +      using inj_on_imageI2 by blast
    2.76    next
    2.77      fix a'
    2.78      assume **: "a' \<in> A'"
    2.79 -    then have "f' a' \<in> A''" using bij unfolding bij_betw_def by auto
    2.80 -    then obtain a where 1: "a \<in> A \<and> f'(f a) = f' a'"
    2.81 -      using * unfolding bij_betw_def by force
    2.82 -    then have "f a \<in> A'" using img by auto
    2.83 -    then have "f a = a'"
    2.84 -      using bij ** 1 unfolding bij_betw_def inj_on_def by auto
    2.85 -    then show "a' \<in> f ` A"
    2.86 -      using 1 by auto
    2.87 +    with bij have "f' a' \<in> A''"
    2.88 +      unfolding bij_betw_def by auto
    2.89 +    with * obtain a where 1: "a \<in> A \<and> f' (f a) = f' a'"
    2.90 +      unfolding bij_betw_def by force
    2.91 +    with img have "f a \<in> A'" by auto
    2.92 +    with bij ** 1 have "f a = a'"
    2.93 +      unfolding bij_betw_def inj_on_def by auto
    2.94 +    with 1 show "a' \<in> f ` A" by auto
    2.95    qed
    2.96  qed
    2.97  
    2.98 @@ -379,9 +380,10 @@
    2.99    let ?g = "\<lambda>b. The (?P b)"
   2.100    have g: "?g b = a" if P: "?P b a" for a b
   2.101    proof -
   2.102 -    from that have ex1: "\<exists>a. ?P b a" using s by blast
   2.103 +    from that s have ex1: "\<exists>a. ?P b a" by blast
   2.104      then have uex1: "\<exists>!a. ?P b a" by (blast dest:inj_onD[OF i])
   2.105 -    then show ?thesis using the1_equality[OF uex1, OF P] P by simp
   2.106 +    then show ?thesis
   2.107 +      using the1_equality[OF uex1, OF P] P by simp
   2.108    qed
   2.109    have "inj_on ?g B"
   2.110    proof (rule inj_onI)
   2.111 @@ -396,15 +398,16 @@
   2.112      fix b
   2.113      assume "b \<in> B"
   2.114      with s obtain a where P: "?P b a" by blast
   2.115 -    then show "?g b \<in> A" using g[OF P] by auto
   2.116 +    with g[OF P] show "?g b \<in> A" by auto
   2.117    next
   2.118      fix a
   2.119      assume "a \<in> A"
   2.120 -    then obtain b where P: "?P b a" using s by blast
   2.121 -    then have "b \<in> B" using s by blast
   2.122 +    with s obtain b where P: "?P b a" by blast
   2.123 +    with s have "b \<in> B" by blast
   2.124      with g[OF P] show "\<exists>b\<in>B. a = ?g b" by blast
   2.125    qed
   2.126 -  ultimately show ?thesis by (auto simp: bij_betw_def)
   2.127 +  ultimately show ?thesis
   2.128 +    by (auto simp: bij_betw_def)
   2.129  qed
   2.130  
   2.131  lemma bij_betw_cong: "(\<And> a. a \<in> A \<Longrightarrow> f a = g a) \<Longrightarrow> bij_betw f A A' = bij_betw g A A'"
   2.132 @@ -500,9 +503,7 @@
   2.133  
   2.134  lemma inj_vimage_singleton: "inj f \<Longrightarrow> f -` {a} \<subseteq> {THE x. f x = a}"
   2.135    \<comment> \<open>The inverse image of a singleton under an injective function is included in a singleton.\<close>
   2.136 -  apply (auto simp add: inj_on_def)
   2.137 -  apply (blast intro: the_equality [symmetric])
   2.138 -  done
   2.139 +  by (simp add: inj_on_def) (blast intro: the_equality [symmetric])
   2.140  
   2.141  lemma inj_on_vimage_singleton: "inj_on f A \<Longrightarrow> f -` {a} \<inter> A \<subseteq> {THE x. x \<in> A \<and> f x = a}"
   2.142    by (auto simp add: inj_on_def intro: the_equality [symmetric])
   2.143 @@ -516,21 +517,21 @@
   2.144  lemma bij_betw_byWitness:
   2.145    assumes left: "\<forall>a \<in> A. f' (f a) = a"
   2.146      and right: "\<forall>a' \<in> A'. f (f' a') = a'"
   2.147 -    and "f ` A \<le> A'"
   2.148 -    and img2: "f' ` A' \<le> A"
   2.149 +    and "f ` A \<subseteq> A'"
   2.150 +    and img2: "f' ` A' \<subseteq> A"
   2.151    shows "bij_betw f A A'"
   2.152    using assms
   2.153    unfolding bij_betw_def inj_on_def
   2.154  proof safe
   2.155    fix a b
   2.156 -  assume *: "a \<in> A" "b \<in> A" and **: "f a = f b"
   2.157 -  have "a = f' (f a) \<and> b = f'(f b)" using * left by simp
   2.158 -  with ** show "a = b" by simp
   2.159 +  assume "a \<in> A" "b \<in> A"
   2.160 +  with left have "a = f' (f a) \<and> b = f' (f b)" by simp
   2.161 +  moreover assume "f a = f b"
   2.162 +  ultimately show "a = b" by simp
   2.163  next
   2.164    fix a' assume *: "a' \<in> A'"
   2.165 -  then have "f' a' \<in> A" using img2 by blast
   2.166 -  moreover
   2.167 -  have "a' = f (f' a')" using * right by simp
   2.168 +  with img2 have "f' a' \<in> A" by blast
   2.169 +  moreover from * right have "a' = f (f' a')" by simp
   2.170    ultimately show "a' \<in> f ` A" by blast
   2.171  qed
   2.172  
   2.173 @@ -565,7 +566,8 @@
   2.174      moreover
   2.175      have False if "f a = f b"
   2.176      proof -
   2.177 -      have "a = b" using * ** that unfolding bij_betw_def inj_on_def by blast
   2.178 +      have "a = b"
   2.179 +        using * ** that unfolding bij_betw_def inj_on_def by blast
   2.180        with \<open>b \<notin> A\<close> ** show ?thesis by blast
   2.181      qed
   2.182      ultimately show "f a \<in> A'" by blast
   2.183 @@ -611,9 +613,9 @@
   2.184  lemma fun_upd_idem_iff: "f(x:=y) = f \<longleftrightarrow> f x = y"
   2.185    unfolding fun_upd_def
   2.186    apply safe
   2.187 -  apply (erule subst)
   2.188 -  apply (rule_tac [2] ext)
   2.189 -  apply auto
   2.190 +   apply (erule subst)
   2.191 +   apply (rule_tac [2] ext)
   2.192 +   apply auto
   2.193    done
   2.194  
   2.195  lemma fun_upd_idem: "f x = y \<Longrightarrow> f(x := y) = f"
   2.196 @@ -667,10 +669,10 @@
   2.197    by (simp add:override_on_def)
   2.198  
   2.199  lemma override_on_insert: "override_on f g (insert x X) = (override_on f g X)(x:=g x)"
   2.200 -unfolding override_on_def by (simp add: fun_eq_iff)
   2.201 +  unfolding override_on_def by (simp add: fun_eq_iff)
   2.202  
   2.203  lemma override_on_insert': "override_on f g (insert x X) = (override_on (f(x:=g x)) g X)"
   2.204 -unfolding override_on_def by (simp add: fun_eq_iff)
   2.205 +  unfolding override_on_def by (simp add: fun_eq_iff)
   2.206  
   2.207  
   2.208  subsection \<open>\<open>swap\<close>\<close>
   2.209 @@ -691,7 +693,7 @@
   2.210    by (simp add: fun_upd_def swap_def fun_eq_iff)
   2.211  
   2.212  lemma swap_nilpotent [simp]: "swap a b (swap a b f) = f"
   2.213 -  by (rule ext, simp add: fun_upd_def swap_def)
   2.214 +  by (rule ext) (simp add: fun_upd_def swap_def)
   2.215  
   2.216  lemma swap_comp_involutory [simp]: "swap a b \<circ> swap a b = id"
   2.217    by (rule ext) simp
   2.218 @@ -757,14 +759,14 @@
   2.219  lemma f_the_inv_into_f: "inj_on f A \<Longrightarrow> y \<in> f ` A  \<Longrightarrow> f (the_inv_into A f y) = y"
   2.220    apply (simp add: the_inv_into_def)
   2.221    apply (rule the1I2)
   2.222 -   apply(blast dest: inj_onD)
   2.223 +   apply (blast dest: inj_onD)
   2.224    apply blast
   2.225    done
   2.226  
   2.227  lemma the_inv_into_into: "inj_on f A \<Longrightarrow> x \<in> f ` A \<Longrightarrow> A \<subseteq> B \<Longrightarrow> the_inv_into A f x \<in> B"
   2.228    apply (simp add: the_inv_into_def)
   2.229    apply (rule the1I2)
   2.230 -   apply(blast dest: inj_onD)
   2.231 +   apply (blast dest: inj_onD)
   2.232    apply blast
   2.233    done
   2.234  
     3.1 --- a/src/HOL/HOL.thy	Mon Aug 01 13:51:17 2016 +0200
     3.2 +++ b/src/HOL/HOL.thy	Mon Aug 01 22:11:29 2016 +0200
     3.3 @@ -218,20 +218,20 @@
     3.4    by (rule trans [OF _ sym])
     3.5  
     3.6  lemma meta_eq_to_obj_eq:
     3.7 -  assumes meq: "A \<equiv> B"
     3.8 +  assumes "A \<equiv> B"
     3.9    shows "A = B"
    3.10 -  by (unfold meq) (rule refl)
    3.11 +  unfolding assms by (rule refl)
    3.12  
    3.13  text \<open>Useful with \<open>erule\<close> for proving equalities from known equalities.\<close>
    3.14       (* a = b
    3.15          |   |
    3.16          c = d   *)
    3.17  lemma box_equals: "\<lbrakk>a = b; a = c; b = d\<rbrakk> \<Longrightarrow> c = d"
    3.18 -apply (rule trans)
    3.19 -apply (rule trans)
    3.20 -apply (rule sym)
    3.21 -apply assumption+
    3.22 -done
    3.23 +  apply (rule trans)
    3.24 +   apply (rule trans)
    3.25 +    apply (rule sym)
    3.26 +    apply assumption+
    3.27 +  done
    3.28  
    3.29  text \<open>For calculational reasoning:\<close>
    3.30  
    3.31 @@ -246,25 +246,25 @@
    3.32  
    3.33  text \<open>Similar to \<open>AP_THM\<close> in Gordon's HOL.\<close>
    3.34  lemma fun_cong: "(f :: 'a \<Rightarrow> 'b) = g \<Longrightarrow> f x = g x"
    3.35 -apply (erule subst)
    3.36 -apply (rule refl)
    3.37 -done
    3.38 +  apply (erule subst)
    3.39 +  apply (rule refl)
    3.40 +  done
    3.41  
    3.42  text \<open>Similar to \<open>AP_TERM\<close> in Gordon's HOL and FOL's \<open>subst_context\<close>.\<close>
    3.43  lemma arg_cong: "x = y \<Longrightarrow> f x = f y"
    3.44 -apply (erule subst)
    3.45 -apply (rule refl)
    3.46 -done
    3.47 +  apply (erule subst)
    3.48 +  apply (rule refl)
    3.49 +  done
    3.50  
    3.51  lemma arg_cong2: "\<lbrakk>a = b; c = d\<rbrakk> \<Longrightarrow> f a c = f b d"
    3.52 -apply (erule ssubst)+
    3.53 -apply (rule refl)
    3.54 -done
    3.55 +  apply (erule ssubst)+
    3.56 +  apply (rule refl)
    3.57 +  done
    3.58  
    3.59  lemma cong: "\<lbrakk>f = g; (x::'a) = y\<rbrakk> \<Longrightarrow> f x = g y"
    3.60 -apply (erule subst)+
    3.61 -apply (rule refl)
    3.62 -done
    3.63 +  apply (erule subst)+
    3.64 +  apply (rule refl)
    3.65 +  done
    3.66  
    3.67  ML \<open>fun cong_tac ctxt = Cong_Tac.cong_tac ctxt @{thm cong}\<close>
    3.68  
    3.69 @@ -295,7 +295,7 @@
    3.70  
    3.71  subsubsection \<open>True\<close>
    3.72  
    3.73 -lemma TrueI: "True"
    3.74 +lemma TrueI: True
    3.75    unfolding True_def by (rule refl)
    3.76  
    3.77  lemma eqTrueI: "P \<Longrightarrow> P = True"
    3.78 @@ -307,14 +307,16 @@
    3.79  
    3.80  subsubsection \<open>Universal quantifier\<close>
    3.81  
    3.82 -lemma allI: assumes "\<And>x::'a. P x" shows "\<forall>x. P x"
    3.83 +lemma allI:
    3.84 +  assumes "\<And>x::'a. P x"
    3.85 +  shows "\<forall>x. P x"
    3.86    unfolding All_def by (iprover intro: ext eqTrueI assms)
    3.87  
    3.88  lemma spec: "\<forall>x::'a. P x \<Longrightarrow> P x"
    3.89 -apply (unfold All_def)
    3.90 -apply (rule eqTrueE)
    3.91 -apply (erule fun_cong)
    3.92 -done
    3.93 +  apply (unfold All_def)
    3.94 +  apply (rule eqTrueE)
    3.95 +  apply (erule fun_cong)
    3.96 +  done
    3.97  
    3.98  lemma allE:
    3.99    assumes major: "\<forall>x. P x"
   3.100 @@ -380,24 +382,24 @@
   3.101  lemma impE:
   3.102    assumes "P \<longrightarrow> Q" P "Q \<Longrightarrow> R"
   3.103    shows R
   3.104 -by (iprover intro: assms mp)
   3.105 +  by (iprover intro: assms mp)
   3.106  
   3.107 -(* Reduces Q to P \<longrightarrow> Q, allowing substitution in P. *)
   3.108 +text \<open>Reduces \<open>Q\<close> to \<open>P \<longrightarrow> Q\<close>, allowing substitution in \<open>P\<close>.\<close>
   3.109  lemma rev_mp: "\<lbrakk>P; P \<longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
   3.110 -by (iprover intro: mp)
   3.111 +  by (iprover intro: mp)
   3.112  
   3.113  lemma contrapos_nn:
   3.114    assumes major: "\<not> Q"
   3.115 -      and minor: "P \<Longrightarrow> Q"
   3.116 +    and minor: "P \<Longrightarrow> Q"
   3.117    shows "\<not> P"
   3.118 -by (iprover intro: notI minor major [THEN notE])
   3.119 +  by (iprover intro: notI minor major [THEN notE])
   3.120  
   3.121 -(*not used at all, but we already have the other 3 combinations *)
   3.122 +text \<open>Not used at all, but we already have the other 3 combinations.\<close>
   3.123  lemma contrapos_pn:
   3.124    assumes major: "Q"
   3.125 -      and minor: "P \<Longrightarrow> \<not> Q"
   3.126 +    and minor: "P \<Longrightarrow> \<not> Q"
   3.127    shows "\<not> P"
   3.128 -by (iprover intro: notI minor major notE)
   3.129 +  by (iprover intro: notI minor major notE)
   3.130  
   3.131  lemma not_sym: "t \<noteq> s \<Longrightarrow> s \<noteq> t"
   3.132    by (erule contrapos_nn) (erule sym)
   3.133 @@ -409,69 +411,56 @@
   3.134  subsubsection \<open>Existential quantifier\<close>
   3.135  
   3.136  lemma exI: "P x \<Longrightarrow> \<exists>x::'a. P x"
   3.137 -apply (unfold Ex_def)
   3.138 -apply (iprover intro: allI allE impI mp)
   3.139 -done
   3.140 +  unfolding Ex_def by (iprover intro: allI allE impI mp)
   3.141  
   3.142  lemma exE:
   3.143    assumes major: "\<exists>x::'a. P x"
   3.144 -      and minor: "\<And>x. P x \<Longrightarrow> Q"
   3.145 +    and minor: "\<And>x. P x \<Longrightarrow> Q"
   3.146    shows "Q"
   3.147 -apply (rule major [unfolded Ex_def, THEN spec, THEN mp])
   3.148 -apply (iprover intro: impI [THEN allI] minor)
   3.149 -done
   3.150 +  by (rule major [unfolded Ex_def, THEN spec, THEN mp]) (iprover intro: impI [THEN allI] minor)
   3.151  
   3.152  
   3.153  subsubsection \<open>Conjunction\<close>
   3.154  
   3.155  lemma conjI: "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> P \<and> Q"
   3.156 -apply (unfold and_def)
   3.157 -apply (iprover intro: impI [THEN allI] mp)
   3.158 -done
   3.159 +  unfolding and_def by (iprover intro: impI [THEN allI] mp)
   3.160  
   3.161  lemma conjunct1: "\<lbrakk>P \<and> Q\<rbrakk> \<Longrightarrow> P"
   3.162 -apply (unfold and_def)
   3.163 -apply (iprover intro: impI dest: spec mp)
   3.164 -done
   3.165 +  unfolding and_def by (iprover intro: impI dest: spec mp)
   3.166  
   3.167  lemma conjunct2: "\<lbrakk>P \<and> Q\<rbrakk> \<Longrightarrow> Q"
   3.168 -apply (unfold and_def)
   3.169 -apply (iprover intro: impI dest: spec mp)
   3.170 -done
   3.171 +  unfolding and_def by (iprover intro: impI dest: spec mp)
   3.172  
   3.173  lemma conjE:
   3.174    assumes major: "P \<and> Q"
   3.175 -      and minor: "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> R"
   3.176 +    and minor: "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> R"
   3.177    shows R
   3.178 -apply (rule minor)
   3.179 -apply (rule major [THEN conjunct1])
   3.180 -apply (rule major [THEN conjunct2])
   3.181 -done
   3.182 +  apply (rule minor)
   3.183 +   apply (rule major [THEN conjunct1])
   3.184 +  apply (rule major [THEN conjunct2])
   3.185 +  done
   3.186  
   3.187  lemma context_conjI:
   3.188 -  assumes P "P \<Longrightarrow> Q" shows "P \<and> Q"
   3.189 -by (iprover intro: conjI assms)
   3.190 +  assumes P "P \<Longrightarrow> Q"
   3.191 +  shows "P \<and> Q"
   3.192 +  by (iprover intro: conjI assms)
   3.193  
   3.194  
   3.195  subsubsection \<open>Disjunction\<close>
   3.196  
   3.197  lemma disjI1: "P \<Longrightarrow> P \<or> Q"
   3.198 -apply (unfold or_def)
   3.199 -apply (iprover intro: allI impI mp)
   3.200 -done
   3.201 +  unfolding or_def by (iprover intro: allI impI mp)
   3.202  
   3.203  lemma disjI2: "Q \<Longrightarrow> P \<or> Q"
   3.204 -apply (unfold or_def)
   3.205 -apply (iprover intro: allI impI mp)
   3.206 -done
   3.207 +  unfolding or_def by (iprover intro: allI impI mp)
   3.208  
   3.209  lemma disjE:
   3.210    assumes major: "P \<or> Q"
   3.211 -      and minorP: "P \<Longrightarrow> R"
   3.212 -      and minorQ: "Q \<Longrightarrow> R"
   3.213 +    and minorP: "P \<Longrightarrow> R"
   3.214 +    and minorQ: "Q \<Longrightarrow> R"
   3.215    shows R
   3.216 -by (iprover intro: minorP minorQ impI
   3.217 -                 major [unfolded or_def, THEN spec, THEN mp, THEN mp])
   3.218 +  by (iprover intro: minorP minorQ impI
   3.219 +      major [unfolded or_def, THEN spec, THEN mp, THEN mp])
   3.220  
   3.221  
   3.222  subsubsection \<open>Classical logic\<close>
   3.223 @@ -479,37 +468,37 @@
   3.224  lemma classical:
   3.225    assumes prem: "\<not> P \<Longrightarrow> P"
   3.226    shows P
   3.227 -apply (rule True_or_False [THEN disjE, THEN eqTrueE])
   3.228 -apply assumption
   3.229 -apply (rule notI [THEN prem, THEN eqTrueI])
   3.230 -apply (erule subst)
   3.231 -apply assumption
   3.232 -done
   3.233 +  apply (rule True_or_False [THEN disjE, THEN eqTrueE])
   3.234 +   apply assumption
   3.235 +  apply (rule notI [THEN prem, THEN eqTrueI])
   3.236 +  apply (erule subst)
   3.237 +  apply assumption
   3.238 +  done
   3.239  
   3.240  lemmas ccontr = FalseE [THEN classical]
   3.241  
   3.242 -(*notE with premises exchanged; it discharges \<not> R so that it can be used to
   3.243 -  make elimination rules*)
   3.244 +text \<open>\<open>notE\<close> with premises exchanged; it discharges \<open>\<not> R\<close> so that it can be used to
   3.245 +  make elimination rules.\<close>
   3.246  lemma rev_notE:
   3.247    assumes premp: P
   3.248 -      and premnot: "\<not> R \<Longrightarrow> \<not> P"
   3.249 +    and premnot: "\<not> R \<Longrightarrow> \<not> P"
   3.250    shows R
   3.251 -apply (rule ccontr)
   3.252 -apply (erule notE [OF premnot premp])
   3.253 -done
   3.254 +  apply (rule ccontr)
   3.255 +  apply (erule notE [OF premnot premp])
   3.256 +  done
   3.257  
   3.258 -(*Double negation law*)
   3.259 +text \<open>Double negation law.\<close>
   3.260  lemma notnotD: "\<not>\<not> P \<Longrightarrow> P"
   3.261 -apply (rule classical)
   3.262 -apply (erule notE)
   3.263 -apply assumption
   3.264 -done
   3.265 +  apply (rule classical)
   3.266 +  apply (erule notE)
   3.267 +  apply assumption
   3.268 +  done
   3.269  
   3.270  lemma contrapos_pp:
   3.271    assumes p1: Q
   3.272 -      and p2: "\<not> P \<Longrightarrow> \<not> Q"
   3.273 +    and p2: "\<not> P \<Longrightarrow> \<not> Q"
   3.274    shows P
   3.275 -by (iprover intro: classical p1 p2 notE)
   3.276 +  by (iprover intro: classical p1 p2 notE)
   3.277  
   3.278  
   3.279  subsubsection \<open>Unique existence\<close>
   3.280 @@ -517,90 +506,87 @@
   3.281  lemma ex1I:
   3.282    assumes "P a" "\<And>x. P x \<Longrightarrow> x = a"
   3.283    shows "\<exists>!x. P x"
   3.284 -by (unfold Ex1_def, iprover intro: assms exI conjI allI impI)
   3.285 +  unfolding Ex1_def by (iprover intro: assms exI conjI allI impI)
   3.286  
   3.287 -text\<open>Sometimes easier to use: the premises have no shared variables.  Safe!\<close>
   3.288 +text \<open>Sometimes easier to use: the premises have no shared variables. Safe!\<close>
   3.289  lemma ex_ex1I:
   3.290    assumes ex_prem: "\<exists>x. P x"
   3.291 -      and eq: "\<And>x y. \<lbrakk>P x; P y\<rbrakk> \<Longrightarrow> x = y"
   3.292 +    and eq: "\<And>x y. \<lbrakk>P x; P y\<rbrakk> \<Longrightarrow> x = y"
   3.293    shows "\<exists>!x. P x"
   3.294 -by (iprover intro: ex_prem [THEN exE] ex1I eq)
   3.295 +  by (iprover intro: ex_prem [THEN exE] ex1I eq)
   3.296  
   3.297  lemma ex1E:
   3.298    assumes major: "\<exists>!x. P x"
   3.299 -      and minor: "\<And>x. \<lbrakk>P x; \<forall>y. P y \<longrightarrow> y = x\<rbrakk> \<Longrightarrow> R"
   3.300 +    and minor: "\<And>x. \<lbrakk>P x; \<forall>y. P y \<longrightarrow> y = x\<rbrakk> \<Longrightarrow> R"
   3.301    shows R
   3.302 -apply (rule major [unfolded Ex1_def, THEN exE])
   3.303 -apply (erule conjE)
   3.304 -apply (iprover intro: minor)
   3.305 -done
   3.306 +  apply (rule major [unfolded Ex1_def, THEN exE])
   3.307 +  apply (erule conjE)
   3.308 +  apply (iprover intro: minor)
   3.309 +  done
   3.310  
   3.311  lemma ex1_implies_ex: "\<exists>!x. P x \<Longrightarrow> \<exists>x. P x"
   3.312 -apply (erule ex1E)
   3.313 -apply (rule exI)
   3.314 -apply assumption
   3.315 -done
   3.316 +  apply (erule ex1E)
   3.317 +  apply (rule exI)
   3.318 +  apply assumption
   3.319 +  done
   3.320  
   3.321  
   3.322  subsubsection \<open>Classical intro rules for disjunction and existential quantifiers\<close>
   3.323  
   3.324  lemma disjCI:
   3.325 -  assumes "\<not> Q \<Longrightarrow> P" shows "P \<or> Q"
   3.326 -apply (rule classical)
   3.327 -apply (iprover intro: assms disjI1 disjI2 notI elim: notE)
   3.328 -done
   3.329 +  assumes "\<not> Q \<Longrightarrow> P"
   3.330 +  shows "P \<or> Q"
   3.331 +  by (rule classical) (iprover intro: assms disjI1 disjI2 notI elim: notE)
   3.332  
   3.333  lemma excluded_middle: "\<not> P \<or> P"
   3.334 -by (iprover intro: disjCI)
   3.335 +  by (iprover intro: disjCI)
   3.336  
   3.337  text \<open>
   3.338    case distinction as a natural deduction rule.
   3.339 -  Note that @{term "\<not> P"} is the second case, not the first
   3.340 +  Note that \<open>\<not> P\<close> is the second case, not the first.
   3.341  \<close>
   3.342  lemma case_split [case_names True False]:
   3.343    assumes prem1: "P \<Longrightarrow> Q"
   3.344 -      and prem2: "\<not> P \<Longrightarrow> Q"
   3.345 +    and prem2: "\<not> P \<Longrightarrow> Q"
   3.346    shows Q
   3.347 -apply (rule excluded_middle [THEN disjE])
   3.348 -apply (erule prem2)
   3.349 -apply (erule prem1)
   3.350 -done
   3.351 +  apply (rule excluded_middle [THEN disjE])
   3.352 +   apply (erule prem2)
   3.353 +  apply (erule prem1)
   3.354 +  done
   3.355  
   3.356 -(*Classical implies (\<longrightarrow>) elimination. *)
   3.357 +text \<open>Classical implies (\<open>\<longrightarrow>\<close>) elimination.\<close>
   3.358  lemma impCE:
   3.359    assumes major: "P \<longrightarrow> Q"
   3.360 -      and minor: "\<not> P \<Longrightarrow> R" "Q \<Longrightarrow> R"
   3.361 +    and minor: "\<not> P \<Longrightarrow> R" "Q \<Longrightarrow> R"
   3.362    shows R
   3.363 -apply (rule excluded_middle [of P, THEN disjE])
   3.364 -apply (iprover intro: minor major [THEN mp])+
   3.365 -done
   3.366 +  apply (rule excluded_middle [of P, THEN disjE])
   3.367 +   apply (iprover intro: minor major [THEN mp])+
   3.368 +  done
   3.369  
   3.370 -(*This version of \<longrightarrow> elimination works on Q before P.  It works best for
   3.371 -  those cases in which P holds "almost everywhere".  Can't install as
   3.372 -  default: would break old proofs.*)
   3.373 +text \<open>
   3.374 +  This version of \<open>\<longrightarrow>\<close> elimination works on \<open>Q\<close> before \<open>P\<close>.  It works best for
   3.375 +  those cases in which \<open>P\<close> holds "almost everywhere".  Can't install as
   3.376 +  default: would break old proofs.
   3.377 +\<close>
   3.378  lemma impCE':
   3.379    assumes major: "P \<longrightarrow> Q"
   3.380 -      and minor: "Q \<Longrightarrow> R" "\<not> P \<Longrightarrow> R"
   3.381 +    and minor: "Q \<Longrightarrow> R" "\<not> P \<Longrightarrow> R"
   3.382    shows R
   3.383 -apply (rule excluded_middle [of P, THEN disjE])
   3.384 -apply (iprover intro: minor major [THEN mp])+
   3.385 -done
   3.386 +  apply (rule excluded_middle [of P, THEN disjE])
   3.387 +   apply (iprover intro: minor major [THEN mp])+
   3.388 +  done
   3.389  
   3.390 -(*Classical <-> elimination. *)
   3.391 +text \<open>Classical \<open>\<longleftrightarrow>\<close> elimination.\<close>
   3.392  lemma iffCE:
   3.393    assumes major: "P = Q"
   3.394 -      and minor: "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> R" "\<lbrakk>\<not> P; \<not> Q\<rbrakk> \<Longrightarrow> R"
   3.395 +    and minor: "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> R" "\<lbrakk>\<not> P; \<not> Q\<rbrakk> \<Longrightarrow> R"
   3.396    shows R
   3.397 -apply (rule major [THEN iffE])
   3.398 -apply (iprover intro: minor elim: impCE notE)
   3.399 -done
   3.400 +  by (rule major [THEN iffE]) (iprover intro: minor elim: impCE notE)
   3.401  
   3.402  lemma exCI:
   3.403    assumes "\<forall>x. \<not> P x \<Longrightarrow> P a"
   3.404    shows "\<exists>x. P x"
   3.405 -apply (rule ccontr)
   3.406 -apply (iprover intro: assms exI allI notI notE [of "\<exists>x. P x"])
   3.407 -done
   3.408 +  by (rule ccontr) (iprover intro: assms exI allI notI notE [of "\<exists>x. P x"])
   3.409  
   3.410  
   3.411  subsubsection \<open>Intuitionistic Reasoning\<close>
   3.412 @@ -650,7 +636,7 @@
   3.413  subsubsection \<open>Atomizing meta-level connectives\<close>
   3.414  
   3.415  axiomatization where
   3.416 -  eq_reflection: "x = y \<Longrightarrow> x \<equiv> y" (*admissible axiom*)
   3.417 +  eq_reflection: "x = y \<Longrightarrow> x \<equiv> y"  \<comment> \<open>admissible axiom\<close>
   3.418  
   3.419  lemma atomize_all [atomize]: "(\<And>x. P x) \<equiv> Trueprop (\<forall>x. P x)"
   3.420  proof
   3.421 @@ -731,9 +717,9 @@
   3.422  subsubsection \<open>Sledgehammer setup\<close>
   3.423  
   3.424  text \<open>
   3.425 -Theorems blacklisted to Sledgehammer. These theorems typically produce clauses
   3.426 -that are prolific (match too many equality or membership literals) and relate to
   3.427 -seldom-used facts. Some duplicate other rules.
   3.428 +  Theorems blacklisted to Sledgehammer. These theorems typically produce clauses
   3.429 +  that are prolific (match too many equality or membership literals) and relate to
   3.430 +  seldom-used facts. Some duplicate other rules.
   3.431  \<close>
   3.432  
   3.433  named_theorems no_atp "theorems that should be filtered out by Sledgehammer"
   3.434 @@ -830,18 +816,18 @@
   3.435  lemmas [intro?] = ext
   3.436    and [elim?] = ex1_implies_ex
   3.437  
   3.438 -(*Better then ex1E for classical reasoner: needs no quantifier duplication!*)
   3.439 +text \<open>Better than \<open>ex1E\<close> for classical reasoner: needs no quantifier duplication!\<close>
   3.440  lemma alt_ex1E [elim!]:
   3.441    assumes major: "\<exists>!x. P x"
   3.442 -      and prem: "\<And>x. \<lbrakk> P x; \<forall>y y'. P y \<and> P y' \<longrightarrow> y = y' \<rbrakk> \<Longrightarrow> R"
   3.443 +    and prem: "\<And>x. \<lbrakk>P x; \<forall>y y'. P y \<and> P y' \<longrightarrow> y = y'\<rbrakk> \<Longrightarrow> R"
   3.444    shows R
   3.445 -apply (rule ex1E [OF major])
   3.446 -apply (rule prem)
   3.447 -apply assumption
   3.448 -apply (rule allI)+
   3.449 -apply (tactic \<open>eresolve_tac @{context} [Classical.dup_elim @{context} @{thm allE}] 1\<close>)
   3.450 -apply iprover
   3.451 -done
   3.452 +  apply (rule ex1E [OF major])
   3.453 +  apply (rule prem)
   3.454 +   apply assumption
   3.455 +  apply (rule allI)+
   3.456 +  apply (tactic \<open>eresolve_tac @{context} [Classical.dup_elim @{context} @{thm allE}] 1\<close>)
   3.457 +  apply iprover
   3.458 +  done
   3.459  
   3.460  ML \<open>
   3.461    structure Blast = Blast
   3.462 @@ -862,27 +848,29 @@
   3.463  
   3.464  lemma the_equality [intro]:
   3.465    assumes "P a"
   3.466 -      and "\<And>x. P x \<Longrightarrow> x = a"
   3.467 +    and "\<And>x. P x \<Longrightarrow> x = a"
   3.468    shows "(THE x. P x) = a"
   3.469    by (blast intro: assms trans [OF arg_cong [where f=The] the_eq_trivial])
   3.470  
   3.471  lemma theI:
   3.472 -  assumes "P a" and "\<And>x. P x \<Longrightarrow> x = a"
   3.473 +  assumes "P a"
   3.474 +    and "\<And>x. P x \<Longrightarrow> x = a"
   3.475    shows "P (THE x. P x)"
   3.476 -by (iprover intro: assms the_equality [THEN ssubst])
   3.477 +  by (iprover intro: assms the_equality [THEN ssubst])
   3.478  
   3.479  lemma theI': "\<exists>!x. P x \<Longrightarrow> P (THE x. P x)"
   3.480    by (blast intro: theI)
   3.481  
   3.482 -(*Easier to apply than theI: only one occurrence of P*)
   3.483 +text \<open>Easier to apply than \<open>theI\<close>: only one occurrence of \<open>P\<close>.\<close>
   3.484  lemma theI2:
   3.485    assumes "P a" "\<And>x. P x \<Longrightarrow> x = a" "\<And>x. P x \<Longrightarrow> Q x"
   3.486    shows "Q (THE x. P x)"
   3.487 -by (iprover intro: assms theI)
   3.488 +  by (iprover intro: assms theI)
   3.489  
   3.490 -lemma the1I2: assumes "\<exists>!x. P x" "\<And>x. P x \<Longrightarrow> Q x" shows "Q (THE x. P x)"
   3.491 -by(iprover intro:assms(2) theI2[where P=P and Q=Q] ex1E[OF assms(1)]
   3.492 -           elim:allE impE)
   3.493 +lemma the1I2:
   3.494 +  assumes "\<exists>!x. P x" "\<And>x. P x \<Longrightarrow> Q x"
   3.495 +  shows "Q (THE x. P x)"
   3.496 +  by (iprover intro: assms(2) theI2[where P=P and Q=Q] ex1E[OF assms(1)] elim: allE impE)
   3.497  
   3.498  lemma the1_equality [elim?]: "\<lbrakk>\<exists>!x. P x; P a\<rbrakk> \<Longrightarrow> (THE x. P x) = a"
   3.499    by blast
   3.500 @@ -929,136 +917,136 @@
   3.501      "\<And>P. (\<forall>x. t = x \<longrightarrow> P x) = P t"
   3.502    by (blast, blast, blast, blast, blast, iprover+)
   3.503  
   3.504 -lemma disj_absorb: "(A \<or> A) = A"
   3.505 +lemma disj_absorb: "A \<or> A \<longleftrightarrow> A"
   3.506    by blast
   3.507  
   3.508 -lemma disj_left_absorb: "(A \<or> (A \<or> B)) = (A \<or> B)"
   3.509 +lemma disj_left_absorb: "A \<or> (A \<or> B) \<longleftrightarrow> A \<or> B"
   3.510    by blast
   3.511  
   3.512 -lemma conj_absorb: "(A \<and> A) = A"
   3.513 +lemma conj_absorb: "A \<and> A \<longleftrightarrow> A"
   3.514    by blast
   3.515  
   3.516 -lemma conj_left_absorb: "(A \<and> (A \<and> B)) = (A \<and> B)"
   3.517 +lemma conj_left_absorb: "A \<and> (A \<and> B) \<longleftrightarrow> A \<and> B"
   3.518    by blast
   3.519  
   3.520  lemma eq_ac:
   3.521    shows eq_commute: "a = b \<longleftrightarrow> b = a"
   3.522      and iff_left_commute: "(P \<longleftrightarrow> (Q \<longleftrightarrow> R)) \<longleftrightarrow> (Q \<longleftrightarrow> (P \<longleftrightarrow> R))"
   3.523 -    and iff_assoc: "((P \<longleftrightarrow> Q) \<longleftrightarrow> R) \<longleftrightarrow> (P \<longleftrightarrow> (Q \<longleftrightarrow> R))" by (iprover, blast+)
   3.524 +    and iff_assoc: "((P \<longleftrightarrow> Q) \<longleftrightarrow> R) \<longleftrightarrow> (P \<longleftrightarrow> (Q \<longleftrightarrow> R))"
   3.525 +  by (iprover, blast+)
   3.526 +
   3.527  lemma neq_commute: "a \<noteq> b \<longleftrightarrow> b \<noteq> a" by iprover
   3.528  
   3.529  lemma conj_comms:
   3.530 -  shows conj_commute: "(P \<and> Q) = (Q \<and> P)"
   3.531 -    and conj_left_commute: "(P \<and> (Q \<and> R)) = (Q \<and> (P \<and> R))" by iprover+
   3.532 -lemma conj_assoc: "((P \<and> Q) \<and> R) = (P \<and> (Q \<and> R))" by iprover
   3.533 +  shows conj_commute: "P \<and> Q \<longleftrightarrow> Q \<and> P"
   3.534 +    and conj_left_commute: "P \<and> (Q \<and> R) \<longleftrightarrow> Q \<and> (P \<and> R)" by iprover+
   3.535 +lemma conj_assoc: "(P \<and> Q) \<and> R \<longleftrightarrow> P \<and> (Q \<and> R)" by iprover
   3.536  
   3.537  lemmas conj_ac = conj_commute conj_left_commute conj_assoc
   3.538  
   3.539  lemma disj_comms:
   3.540 -  shows disj_commute: "(P \<or> Q) = (Q \<or> P)"
   3.541 -    and disj_left_commute: "(P \<or> (Q \<or> R)) = (Q \<or> (P \<or> R))" by iprover+
   3.542 -lemma disj_assoc: "((P \<or> Q) \<or> R) = (P \<or> (Q \<or> R))" by iprover
   3.543 +  shows disj_commute: "P \<or> Q \<longleftrightarrow> Q \<or> P"
   3.544 +    and disj_left_commute: "P \<or> (Q \<or> R) \<longleftrightarrow> Q \<or> (P \<or> R)" by iprover+
   3.545 +lemma disj_assoc: "(P \<or> Q) \<or> R \<longleftrightarrow> P \<or> (Q \<or> R)" by iprover
   3.546  
   3.547  lemmas disj_ac = disj_commute disj_left_commute disj_assoc
   3.548  
   3.549 -lemma conj_disj_distribL: "(P \<and> (Q \<or> R)) = (P \<and> Q \<or> P \<and> R)" by iprover
   3.550 -lemma conj_disj_distribR: "((P \<or> Q) \<and> R) = (P \<and> R \<or> Q \<and> R)" by iprover
   3.551 +lemma conj_disj_distribL: "P \<and> (Q \<or> R) \<longleftrightarrow> P \<and> Q \<or> P \<and> R" by iprover
   3.552 +lemma conj_disj_distribR: "(P \<or> Q) \<and> R \<longleftrightarrow> P \<and> R \<or> Q \<and> R" by iprover
   3.553  
   3.554 -lemma disj_conj_distribL: "(P \<or> (Q \<and> R)) = ((P \<or> Q) \<and> (P \<or> R))" by iprover
   3.555 -lemma disj_conj_distribR: "((P \<and> Q) \<or> R) = ((P \<or> R) \<and> (Q \<or> R))" by iprover
   3.556 +lemma disj_conj_distribL: "P \<or> (Q \<and> R) \<longleftrightarrow> (P \<or> Q) \<and> (P \<or> R)" by iprover
   3.557 +lemma disj_conj_distribR: "(P \<and> Q) \<or> R \<longleftrightarrow> (P \<or> R) \<and> (Q \<or> R)" by iprover
   3.558  
   3.559  lemma imp_conjR: "(P \<longrightarrow> (Q \<and> R)) = ((P \<longrightarrow> Q) \<and> (P \<longrightarrow> R))" by iprover
   3.560  lemma imp_conjL: "((P \<and> Q) \<longrightarrow> R) = (P \<longrightarrow> (Q \<longrightarrow> R))" by iprover
   3.561  lemma imp_disjL: "((P \<or> Q) \<longrightarrow> R) = ((P \<longrightarrow> R) \<and> (Q \<longrightarrow> R))" by iprover
   3.562  
   3.563  text \<open>These two are specialized, but \<open>imp_disj_not1\<close> is useful in \<open>Auth/Yahalom\<close>.\<close>
   3.564 -lemma imp_disj_not1: "(P \<longrightarrow> Q \<or> R) = (\<not> Q \<longrightarrow> P \<longrightarrow> R)" by blast
   3.565 -lemma imp_disj_not2: "(P \<longrightarrow> Q \<or> R) = (\<not> R \<longrightarrow> P \<longrightarrow> Q)" by blast
   3.566 +lemma imp_disj_not1: "(P \<longrightarrow> Q \<or> R) \<longleftrightarrow> (\<not> Q \<longrightarrow> P \<longrightarrow> R)" by blast
   3.567 +lemma imp_disj_not2: "(P \<longrightarrow> Q \<or> R) \<longleftrightarrow> (\<not> R \<longrightarrow> P \<longrightarrow> Q)" by blast
   3.568  
   3.569 -lemma imp_disj1: "((P \<longrightarrow> Q) \<or> R) = (P \<longrightarrow> Q \<or> R)" by blast
   3.570 -lemma imp_disj2: "(Q \<or> (P \<longrightarrow> R)) = (P \<longrightarrow> Q \<or> R)" by blast
   3.571 +lemma imp_disj1: "((P \<longrightarrow> Q) \<or> R) \<longleftrightarrow> (P \<longrightarrow> Q \<or> R)" by blast
   3.572 +lemma imp_disj2: "(Q \<or> (P \<longrightarrow> R)) \<longleftrightarrow> (P \<longrightarrow> Q \<or> R)" by blast
   3.573  
   3.574 -lemma imp_cong: "(P = P') \<Longrightarrow> (P' \<Longrightarrow> (Q = Q')) \<Longrightarrow> ((P \<longrightarrow> Q) = (P' \<longrightarrow> Q'))"
   3.575 +lemma imp_cong: "(P = P') \<Longrightarrow> (P' \<Longrightarrow> (Q = Q')) \<Longrightarrow> ((P \<longrightarrow> Q) \<longleftrightarrow> (P' \<longrightarrow> Q'))"
   3.576    by iprover
   3.577  
   3.578 -lemma de_Morgan_disj: "(\<not> (P \<or> Q)) = (\<not> P \<and> \<not> Q)" by iprover
   3.579 -lemma de_Morgan_conj: "(\<not> (P \<and> Q)) = (\<not> P \<or> \<not> Q)" by blast
   3.580 -lemma not_imp: "(\<not> (P \<longrightarrow> Q)) = (P \<and> \<not> Q)" by blast
   3.581 -lemma not_iff: "(P \<noteq> Q) = (P = (\<not> Q))" by blast
   3.582 -lemma disj_not1: "(\<not> P \<or> Q) = (P \<longrightarrow> Q)" by blast
   3.583 -lemma disj_not2: "(P \<or> \<not> Q) = (Q \<longrightarrow> P)"  \<comment> \<open>changes orientation :-(\<close>
   3.584 -  by blast
   3.585 -lemma imp_conv_disj: "(P \<longrightarrow> Q) = ((\<not> P) \<or> Q)" by blast
   3.586 +lemma de_Morgan_disj: "\<not> (P \<or> Q) \<longleftrightarrow> \<not> P \<and> \<not> Q" by iprover
   3.587 +lemma de_Morgan_conj: "\<not> (P \<and> Q) \<longleftrightarrow> \<not> P \<or> \<not> Q" by blast
   3.588 +lemma not_imp: "\<not> (P \<longrightarrow> Q) \<longleftrightarrow> P \<and> \<not> Q" by blast
   3.589 +lemma not_iff: "P \<noteq> Q \<longleftrightarrow> (P \<longleftrightarrow> \<not> Q)" by blast
   3.590 +lemma disj_not1: "\<not> P \<or> Q \<longleftrightarrow> (P \<longrightarrow> Q)" by blast
   3.591 +lemma disj_not2: "P \<or> \<not> Q \<longleftrightarrow> (Q \<longrightarrow> P)" by blast  \<comment> \<open>changes orientation :-(\<close>
   3.592 +lemma imp_conv_disj: "(P \<longrightarrow> Q) \<longleftrightarrow> (\<not> P) \<or> Q" by blast
   3.593  lemma disj_imp: "P \<or> Q \<longleftrightarrow> \<not> P \<longrightarrow> Q" by blast
   3.594  
   3.595 -lemma iff_conv_conj_imp: "(P = Q) = ((P \<longrightarrow> Q) \<and> (Q \<longrightarrow> P))" by iprover
   3.596 +lemma iff_conv_conj_imp: "(P \<longleftrightarrow> Q) \<longleftrightarrow> (P \<longrightarrow> Q) \<and> (Q \<longrightarrow> P)" by iprover
   3.597  
   3.598  
   3.599 -lemma cases_simp: "((P \<longrightarrow> Q) \<and> (\<not> P \<longrightarrow> Q)) = Q"
   3.600 +lemma cases_simp: "(P \<longrightarrow> Q) \<and> (\<not> P \<longrightarrow> Q) \<longleftrightarrow> Q"
   3.601    \<comment> \<open>Avoids duplication of subgoals after \<open>if_split\<close>, when the true and false\<close>
   3.602    \<comment> \<open>cases boil down to the same thing.\<close>
   3.603    by blast
   3.604  
   3.605 -lemma not_all: "(\<not> (\<forall>x. P x)) = (\<exists>x. \<not> P x)" by blast
   3.606 -lemma imp_all: "((\<forall>x. P x) \<longrightarrow> Q) = (\<exists>x. P x \<longrightarrow> Q)" by blast
   3.607 -lemma not_ex: "(\<not> (\<exists>x. P x)) = (\<forall>x. \<not> P x)" by iprover
   3.608 -lemma imp_ex: "((\<exists>x. P x) \<longrightarrow> Q) = (\<forall>x. P x \<longrightarrow> Q)" by iprover
   3.609 -lemma all_not_ex: "(\<forall>x. P x) = (\<not> (\<exists>x. \<not> P x ))" by blast
   3.610 +lemma not_all: "\<not> (\<forall>x. P x) \<longleftrightarrow> (\<exists>x. \<not> P x)" by blast
   3.611 +lemma imp_all: "((\<forall>x. P x) \<longrightarrow> Q) \<longleftrightarrow> (\<exists>x. P x \<longrightarrow> Q)" by blast
   3.612 +lemma not_ex: "\<not> (\<exists>x. P x) \<longleftrightarrow> (\<forall>x. \<not> P x)" by iprover
   3.613 +lemma imp_ex: "((\<exists>x. P x) \<longrightarrow> Q) \<longleftrightarrow> (\<forall>x. P x \<longrightarrow> Q)" by iprover
   3.614 +lemma all_not_ex: "(\<forall>x. P x) \<longleftrightarrow> \<not> (\<exists>x. \<not> P x)" by blast
   3.615  
   3.616  declare All_def [no_atp]
   3.617  
   3.618 -lemma ex_disj_distrib: "(\<exists>x. P x \<or> Q x) = ((\<exists>x. P x) \<or> (\<exists>x. Q x))" by iprover
   3.619 -lemma all_conj_distrib: "(\<forall>x. P x \<and> Q x) = ((\<forall>x. P x) \<and> (\<forall>x. Q x))" by iprover
   3.620 +lemma ex_disj_distrib: "(\<exists>x. P x \<or> Q x) \<longleftrightarrow> (\<exists>x. P x) \<or> (\<exists>x. Q x)" by iprover
   3.621 +lemma all_conj_distrib: "(\<forall>x. P x \<and> Q x) \<longleftrightarrow> (\<forall>x. P x) \<and> (\<forall>x. Q x)" by iprover
   3.622  
   3.623  text \<open>
   3.624 -  \medskip The \<open>\<and>\<close> congruence rule: not included by default!
   3.625 +  \<^medskip> The \<open>\<and>\<close> congruence rule: not included by default!
   3.626    May slow rewrite proofs down by as much as 50\%\<close>
   3.627  
   3.628 -lemma conj_cong:
   3.629 -    "(P = P') \<Longrightarrow> (P' \<Longrightarrow> (Q = Q')) \<Longrightarrow> ((P \<and> Q) = (P' \<and> Q'))"
   3.630 +lemma conj_cong: "P = P' \<Longrightarrow> (P' \<Longrightarrow> Q = Q') \<Longrightarrow> (P \<and> Q) = (P' \<and> Q')"
   3.631    by iprover
   3.632  
   3.633 -lemma rev_conj_cong:
   3.634 -    "(Q = Q') \<Longrightarrow> (Q' \<Longrightarrow> (P = P')) \<Longrightarrow> ((P \<and> Q) = (P' \<and> Q'))"
   3.635 +lemma rev_conj_cong: "Q = Q' \<Longrightarrow> (Q' \<Longrightarrow> P = P') \<Longrightarrow> (P \<and> Q) = (P' \<and> Q')"
   3.636    by iprover
   3.637  
   3.638  text \<open>The \<open>|\<close> congruence rule: not included by default!\<close>
   3.639  
   3.640 -lemma disj_cong:
   3.641 -    "(P = P') \<Longrightarrow> (\<not> P' \<Longrightarrow> (Q = Q')) \<Longrightarrow> ((P \<or> Q) = (P' \<or> Q'))"
   3.642 +lemma disj_cong: "P = P' \<Longrightarrow> (\<not> P' \<Longrightarrow> Q = Q') \<Longrightarrow> (P \<or> Q) = (P' \<or> Q')"
   3.643    by blast
   3.644  
   3.645  
   3.646 -text \<open>\medskip if-then-else rules\<close>
   3.647 +text \<open>\<^medskip> if-then-else rules\<close>
   3.648  
   3.649  lemma if_True [code]: "(if True then x else y) = x"
   3.650 -  by (unfold If_def) blast
   3.651 +  unfolding If_def by blast
   3.652  
   3.653  lemma if_False [code]: "(if False then x else y) = y"
   3.654 -  by (unfold If_def) blast
   3.655 +  unfolding If_def by blast
   3.656  
   3.657  lemma if_P: "P \<Longrightarrow> (if P then x else y) = x"
   3.658 -  by (unfold If_def) blast
   3.659 +  unfolding If_def by blast
   3.660  
   3.661  lemma if_not_P: "\<not> P \<Longrightarrow> (if P then x else y) = y"
   3.662 -  by (unfold If_def) blast
   3.663 +  unfolding If_def by blast
   3.664  
   3.665  lemma if_split: "P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y))"
   3.666    apply (rule case_split [of Q])
   3.667     apply (simplesubst if_P)
   3.668 -    prefer 3 apply (simplesubst if_not_P, blast+)
   3.669 +    prefer 3
   3.670 +    apply (simplesubst if_not_P)
   3.671 +     apply blast+
   3.672    done
   3.673  
   3.674  lemma if_split_asm: "P (if Q then x else y) = (\<not> ((Q \<and> \<not> P x) \<or> (\<not> Q \<and> \<not> P y)))"
   3.675 -by (simplesubst if_split, blast)
   3.676 +  by (simplesubst if_split) blast
   3.677  
   3.678  lemmas if_splits [no_atp] = if_split if_split_asm
   3.679  
   3.680  lemma if_cancel: "(if c then x else x) = x"
   3.681 -by (simplesubst if_split, blast)
   3.682 +  by (simplesubst if_split) blast
   3.683  
   3.684  lemma if_eq_cancel: "(if x = y then y else x) = x"
   3.685 -by (simplesubst if_split, blast)
   3.686 +  by (simplesubst if_split) blast
   3.687  
   3.688  lemma if_bool_eq_conj: "(if P then Q else R) = ((P \<longrightarrow> Q) \<and> (\<not> P \<longrightarrow> R))"
   3.689    \<comment> \<open>This form is useful for expanding \<open>if\<close>s on the RIGHT of the \<open>\<Longrightarrow>\<close> symbol.\<close>
   3.690 @@ -1068,10 +1056,10 @@
   3.691    \<comment> \<open>And this form is useful for expanding \<open>if\<close>s on the LEFT.\<close>
   3.692    by (simplesubst if_split) blast
   3.693  
   3.694 -lemma Eq_TrueI: "P \<Longrightarrow> P \<equiv> True" by (unfold atomize_eq) iprover
   3.695 -lemma Eq_FalseI: "\<not> P \<Longrightarrow> P \<equiv> False" by (unfold atomize_eq) iprover
   3.696 +lemma Eq_TrueI: "P \<Longrightarrow> P \<equiv> True" unfolding atomize_eq by iprover
   3.697 +lemma Eq_FalseI: "\<not> P \<Longrightarrow> P \<equiv> False" unfolding atomize_eq by iprover
   3.698  
   3.699 -text \<open>\medskip let rules for simproc\<close>
   3.700 +text \<open>\<^medskip> let rules for simproc\<close>
   3.701  
   3.702  lemma Let_folded: "f x \<equiv> g x \<Longrightarrow> Let x f \<equiv> Let x g"
   3.703    by (unfold Let_def)
   3.704 @@ -1085,8 +1073,8 @@
   3.705    its premise.
   3.706  \<close>
   3.707  
   3.708 -definition simp_implies :: "[prop, prop] \<Rightarrow> prop"  (infixr "=simp=>" 1) where
   3.709 -  "simp_implies \<equiv> op \<Longrightarrow>"
   3.710 +definition simp_implies :: "prop \<Rightarrow> prop \<Rightarrow> prop"  (infixr "=simp=>" 1)
   3.711 +  where "simp_implies \<equiv> op \<Longrightarrow>"
   3.712  
   3.713  lemma simp_impliesI:
   3.714    assumes PQ: "(PROP P \<Longrightarrow> PROP Q)"
   3.715 @@ -1098,8 +1086,8 @@
   3.716  
   3.717  lemma simp_impliesE:
   3.718    assumes PQ: "PROP P =simp=> PROP Q"
   3.719 -  and P: "PROP P"
   3.720 -  and QR: "PROP Q \<Longrightarrow> PROP R"
   3.721 +    and P: "PROP P"
   3.722 +    and QR: "PROP Q \<Longrightarrow> PROP R"
   3.723    shows "PROP R"
   3.724    apply (rule QR)
   3.725    apply (rule PQ [unfolded simp_implies_def])
   3.726 @@ -1108,18 +1096,19 @@
   3.727  
   3.728  lemma simp_implies_cong:
   3.729    assumes PP' :"PROP P \<equiv> PROP P'"
   3.730 -  and P'QQ': "PROP P' \<Longrightarrow> (PROP Q \<equiv> PROP Q')"
   3.731 +    and P'QQ': "PROP P' \<Longrightarrow> (PROP Q \<equiv> PROP Q')"
   3.732    shows "(PROP P =simp=> PROP Q) \<equiv> (PROP P' =simp=> PROP Q')"
   3.733 -proof (unfold simp_implies_def, rule equal_intr_rule)
   3.734 +  unfolding simp_implies_def
   3.735 +proof (rule equal_intr_rule)
   3.736    assume PQ: "PROP P \<Longrightarrow> PROP Q"
   3.737 -  and P': "PROP P'"
   3.738 +    and P': "PROP P'"
   3.739    from PP' [symmetric] and P' have "PROP P"
   3.740      by (rule equal_elim_rule1)
   3.741    then have "PROP Q" by (rule PQ)
   3.742    with P'QQ' [OF P'] show "PROP Q'" by (rule equal_elim_rule1)
   3.743  next
   3.744    assume P'Q': "PROP P' \<Longrightarrow> PROP Q'"
   3.745 -  and P: "PROP P"
   3.746 +    and P: "PROP P"
   3.747    from PP' and P have P': "PROP P'" by (rule equal_elim_rule1)
   3.748    then have "PROP Q'" by (rule P'Q')
   3.749    with P'QQ' [OF P', symmetric] show "PROP Q"
   3.750 @@ -1141,12 +1130,10 @@
   3.751    shows "(\<exists>x. P x) = (\<exists>x. Q x)"
   3.752    using assms by blast
   3.753  
   3.754 -lemma all_comm:
   3.755 -  "(\<forall>x y. P x y) = (\<forall>y x. P x y)"
   3.756 +lemma all_comm: "(\<forall>x y. P x y) = (\<forall>y x. P x y)"
   3.757    by blast
   3.758  
   3.759 -lemma ex_comm:
   3.760 -  "(\<exists>x y. P x y) = (\<exists>y x. P x y)"
   3.761 +lemma ex_comm: "(\<exists>x y. P x y) = (\<exists>y x. P x y)"
   3.762    by blast
   3.763  
   3.764  ML_file "Tools/simpdata.ML"
   3.765 @@ -1163,79 +1150,80 @@
   3.766  text \<open>Simproc for proving \<open>(y = x) \<equiv> False\<close> from premise \<open>\<not> (x = y)\<close>:\<close>
   3.767  
   3.768  simproc_setup neq ("x = y") = \<open>fn _ =>
   3.769 -let
   3.770 -  val neq_to_EQ_False = @{thm not_sym} RS @{thm Eq_FalseI};
   3.771 -  fun is_neq eq lhs rhs thm =
   3.772 -    (case Thm.prop_of thm of
   3.773 -      _ $ (Not $ (eq' $ l' $ r')) =>
   3.774 -        Not = HOLogic.Not andalso eq' = eq andalso
   3.775 -        r' aconv lhs andalso l' aconv rhs
   3.776 -    | _ => false);
   3.777 -  fun proc ss ct =
   3.778 -    (case Thm.term_of ct of
   3.779 -      eq $ lhs $ rhs =>
   3.780 -        (case find_first (is_neq eq lhs rhs) (Simplifier.prems_of ss) of
   3.781 -          SOME thm => SOME (thm RS neq_to_EQ_False)
   3.782 -        | NONE => NONE)
   3.783 -     | _ => NONE);
   3.784 -in proc end;
   3.785 +  let
   3.786 +    val neq_to_EQ_False = @{thm not_sym} RS @{thm Eq_FalseI};
   3.787 +    fun is_neq eq lhs rhs thm =
   3.788 +      (case Thm.prop_of thm of
   3.789 +        _ $ (Not $ (eq' $ l' $ r')) =>
   3.790 +          Not = HOLogic.Not andalso eq' = eq andalso
   3.791 +          r' aconv lhs andalso l' aconv rhs
   3.792 +      | _ => false);
   3.793 +    fun proc ss ct =
   3.794 +      (case Thm.term_of ct of
   3.795 +        eq $ lhs $ rhs =>
   3.796 +          (case find_first (is_neq eq lhs rhs) (Simplifier.prems_of ss) of
   3.797 +            SOME thm => SOME (thm RS neq_to_EQ_False)
   3.798 +          | NONE => NONE)
   3.799 +       | _ => NONE);
   3.800 +  in proc end;
   3.801  \<close>
   3.802  
   3.803  simproc_setup let_simp ("Let x f") = \<open>
   3.804 -let
   3.805 -  fun count_loose (Bound i) k = if i >= k then 1 else 0
   3.806 -    | count_loose (s $ t) k = count_loose s k + count_loose t k
   3.807 -    | count_loose (Abs (_, _, t)) k = count_loose  t (k + 1)
   3.808 -    | count_loose _ _ = 0;
   3.809 -  fun is_trivial_let (Const (@{const_name Let}, _) $ x $ t) =
   3.810 -    (case t of
   3.811 -      Abs (_, _, t') => count_loose t' 0 <= 1
   3.812 -    | _ => true);
   3.813 -in
   3.814 -  fn _ => fn ctxt => fn ct =>
   3.815 -    if is_trivial_let (Thm.term_of ct)
   3.816 -    then SOME @{thm Let_def} (*no or one ocurrence of bound variable*)
   3.817 -    else
   3.818 -      let (*Norbert Schirmer's case*)
   3.819 -        val t = Thm.term_of ct;
   3.820 -        val ([t'], ctxt') = Variable.import_terms false [t] ctxt;
   3.821 -      in
   3.822 -        Option.map (hd o Variable.export ctxt' ctxt o single)
   3.823 -          (case t' of Const (@{const_name Let},_) $ x $ f => (* x and f are already in normal form *)
   3.824 -            if is_Free x orelse is_Bound x orelse is_Const x
   3.825 -            then SOME @{thm Let_def}
   3.826 -            else
   3.827 -              let
   3.828 -                val n = case f of (Abs (x, _, _)) => x | _ => "x";
   3.829 -                val cx = Thm.cterm_of ctxt x;
   3.830 -                val xT = Thm.typ_of_cterm cx;
   3.831 -                val cf = Thm.cterm_of ctxt f;
   3.832 -                val fx_g = Simplifier.rewrite ctxt (Thm.apply cf cx);
   3.833 -                val (_ $ _ $ g) = Thm.prop_of fx_g;
   3.834 -                val g' = abstract_over (x, g);
   3.835 -                val abs_g'= Abs (n, xT, g');
   3.836 -              in
   3.837 -                if g aconv g' then
   3.838 -                  let
   3.839 -                    val rl =
   3.840 -                      infer_instantiate ctxt [(("f", 0), cf), (("x", 0), cx)] @{thm Let_unfold};
   3.841 -                  in SOME (rl OF [fx_g]) end
   3.842 -                else if (Envir.beta_eta_contract f) aconv (Envir.beta_eta_contract abs_g')
   3.843 -                then NONE (*avoid identity conversion*)
   3.844 -                else
   3.845 -                  let
   3.846 -                    val g'x = abs_g' $ x;
   3.847 -                    val g_g'x = Thm.symmetric (Thm.beta_conversion false (Thm.cterm_of ctxt g'x));
   3.848 -                    val rl =
   3.849 -                      @{thm Let_folded} |> infer_instantiate ctxt
   3.850 -                        [(("f", 0), Thm.cterm_of ctxt f),
   3.851 -                         (("x", 0), cx),
   3.852 -                         (("g", 0), Thm.cterm_of ctxt abs_g')];
   3.853 -                  in SOME (rl OF [Thm.transitive fx_g g_g'x]) end
   3.854 -              end
   3.855 -          | _ => NONE)
   3.856 -      end
   3.857 -end\<close>
   3.858 +  let
   3.859 +    fun count_loose (Bound i) k = if i >= k then 1 else 0
   3.860 +      | count_loose (s $ t) k = count_loose s k + count_loose t k
   3.861 +      | count_loose (Abs (_, _, t)) k = count_loose  t (k + 1)
   3.862 +      | count_loose _ _ = 0;
   3.863 +    fun is_trivial_let (Const (@{const_name Let}, _) $ x $ t) =
   3.864 +      (case t of
   3.865 +        Abs (_, _, t') => count_loose t' 0 <= 1
   3.866 +      | _ => true);
   3.867 +  in
   3.868 +    fn _ => fn ctxt => fn ct =>
   3.869 +      if is_trivial_let (Thm.term_of ct)
   3.870 +      then SOME @{thm Let_def} (*no or one ocurrence of bound variable*)
   3.871 +      else
   3.872 +        let (*Norbert Schirmer's case*)
   3.873 +          val t = Thm.term_of ct;
   3.874 +          val ([t'], ctxt') = Variable.import_terms false [t] ctxt;
   3.875 +        in
   3.876 +          Option.map (hd o Variable.export ctxt' ctxt o single)
   3.877 +            (case t' of Const (@{const_name Let},_) $ x $ f => (* x and f are already in normal form *)
   3.878 +              if is_Free x orelse is_Bound x orelse is_Const x
   3.879 +              then SOME @{thm Let_def}
   3.880 +              else
   3.881 +                let
   3.882 +                  val n = case f of (Abs (x, _, _)) => x | _ => "x";
   3.883 +                  val cx = Thm.cterm_of ctxt x;
   3.884 +                  val xT = Thm.typ_of_cterm cx;
   3.885 +                  val cf = Thm.cterm_of ctxt f;
   3.886 +                  val fx_g = Simplifier.rewrite ctxt (Thm.apply cf cx);
   3.887 +                  val (_ $ _ $ g) = Thm.prop_of fx_g;
   3.888 +                  val g' = abstract_over (x, g);
   3.889 +                  val abs_g'= Abs (n, xT, g');
   3.890 +                in
   3.891 +                  if g aconv g' then
   3.892 +                    let
   3.893 +                      val rl =
   3.894 +                        infer_instantiate ctxt [(("f", 0), cf), (("x", 0), cx)] @{thm Let_unfold};
   3.895 +                    in SOME (rl OF [fx_g]) end
   3.896 +                  else if (Envir.beta_eta_contract f) aconv (Envir.beta_eta_contract abs_g')
   3.897 +                  then NONE (*avoid identity conversion*)
   3.898 +                  else
   3.899 +                    let
   3.900 +                      val g'x = abs_g' $ x;
   3.901 +                      val g_g'x = Thm.symmetric (Thm.beta_conversion false (Thm.cterm_of ctxt g'x));
   3.902 +                      val rl =
   3.903 +                        @{thm Let_folded} |> infer_instantiate ctxt
   3.904 +                          [(("f", 0), Thm.cterm_of ctxt f),
   3.905 +                           (("x", 0), cx),
   3.906 +                           (("g", 0), Thm.cterm_of ctxt abs_g')];
   3.907 +                    in SOME (rl OF [Thm.transitive fx_g g_g'x]) end
   3.908 +                end
   3.909 +            | _ => NONE)
   3.910 +        end
   3.911 +  end
   3.912 +\<close>
   3.913  
   3.914  lemma True_implies_equals: "(True \<Longrightarrow> PROP P) \<equiv> PROP P"
   3.915  proof
   3.916 @@ -1254,9 +1242,10 @@
   3.917  
   3.918  (* This is not made a simp rule because it does not improve any proofs
   3.919     but slows some AFP entries down by 5% (cpu time). May 2015 *)
   3.920 -lemma implies_False_swap: "NO_MATCH (Trueprop False) P \<Longrightarrow>
   3.921 -  (False \<Longrightarrow> PROP P \<Longrightarrow> PROP Q) \<equiv> (PROP P \<Longrightarrow> False \<Longrightarrow> PROP Q)"
   3.922 -by(rule swap_prems_eq)
   3.923 +lemma implies_False_swap:
   3.924 +  "NO_MATCH (Trueprop False) P \<Longrightarrow>
   3.925 +    (False \<Longrightarrow> PROP P \<Longrightarrow> PROP Q) \<equiv> (PROP P \<Longrightarrow> False \<Longrightarrow> PROP Q)"
   3.926 +  by (rule swap_prems_eq)
   3.927  
   3.928  lemma ex_simps:
   3.929    "\<And>P Q. (\<exists>x. P x \<and> Q)   = ((\<exists>x. P x) \<and> Q)"
   3.930 @@ -1279,19 +1268,19 @@
   3.931    by (iprover | blast)+
   3.932  
   3.933  lemmas [simp] =
   3.934 -  triv_forall_equality (*prunes params*)
   3.935 -  True_implies_equals implies_True_equals (*prune True in asms*)
   3.936 -  False_implies_equals (*prune False in asms*)
   3.937 +  triv_forall_equality  \<comment> \<open>prunes params\<close>
   3.938 +  True_implies_equals implies_True_equals  \<comment> \<open>prune \<open>True\<close> in asms\<close>
   3.939 +  False_implies_equals  \<comment> \<open>prune \<open>False\<close> in asms\<close>
   3.940    if_True
   3.941    if_False
   3.942    if_cancel
   3.943    if_eq_cancel
   3.944 -  imp_disjL
   3.945 -  (*In general it seems wrong to add distributive laws by default: they
   3.946 -    might cause exponential blow-up.  But imp_disjL has been in for a while
   3.947 +  imp_disjL \<comment>
   3.948 +   \<open>In general it seems wrong to add distributive laws by default: they
   3.949 +    might cause exponential blow-up.  But \<open>imp_disjL\<close> has been in for a while
   3.950      and cannot be removed without affecting existing proofs.  Moreover,
   3.951 -    rewriting by "(P \<or> Q \<longrightarrow> R) = ((P \<longrightarrow> R) \<and> (Q \<longrightarrow> R))" might be justified on the
   3.952 -    grounds that it allows simplification of R in the two cases.*)
   3.953 +    rewriting by \<open>(P \<or> Q \<longrightarrow> R) = ((P \<longrightarrow> R) \<and> (Q \<longrightarrow> R))\<close> might be justified on the
   3.954 +    grounds that it allows simplification of \<open>R\<close> in the two cases.\<close>
   3.955    conj_assoc
   3.956    disj_assoc
   3.957    de_Morgan_conj
   3.958 @@ -1314,15 +1303,15 @@
   3.959  
   3.960  ML \<open>val HOL_ss = simpset_of @{context}\<close>
   3.961  
   3.962 -text \<open>Simplifies @{term x} assuming @{prop c} and @{term y} assuming @{prop "\<not> c"}\<close>
   3.963 +text \<open>Simplifies \<open>x\<close> assuming \<open>c\<close> and \<open>y\<close> assuming \<open>\<not> c\<close>.\<close>
   3.964  lemma if_cong:
   3.965    assumes "b = c"
   3.966 -      and "c \<Longrightarrow> x = u"
   3.967 -      and "\<not> c \<Longrightarrow> y = v"
   3.968 +    and "c \<Longrightarrow> x = u"
   3.969 +    and "\<not> c \<Longrightarrow> y = v"
   3.970    shows "(if b then x else y) = (if c then u else v)"
   3.971    using assms by simp
   3.972  
   3.973 -text \<open>Prevents simplification of x and y:
   3.974 +text \<open>Prevents simplification of \<open>x\<close> and \<open>y\<close>:
   3.975    faster and allows the execution of functional programs.\<close>
   3.976  lemma if_weak_cong [cong]:
   3.977    assumes "b = c"
   3.978 @@ -1341,11 +1330,10 @@
   3.979    shows "(t \<equiv> u) \<equiv> (t \<equiv> u')"
   3.980    using assms by simp
   3.981  
   3.982 -lemma if_distrib:
   3.983 -  "f (if c then x else y) = (if c then f x else f y)"
   3.984 +lemma if_distrib: "f (if c then x else y) = (if c then f x else f y)"
   3.985    by simp
   3.986  
   3.987 -text\<open>As a simplification rule, it replaces all function equalities by
   3.988 +text \<open>As a simplification rule, it replaces all function equalities by
   3.989    first-order equalities.\<close>
   3.990  lemma fun_eq_iff: "f = g \<longleftrightarrow> (\<forall>x. f x = g x)"
   3.991    by auto
   3.992 @@ -1578,27 +1566,32 @@
   3.993  
   3.994  lemma choice_eq: "(\<forall>x. \<exists>!y. P x y) = (\<exists>!f. \<forall>x. P x (f x))"
   3.995    apply (rule iffI)
   3.996 -  apply (rule_tac a = "\<lambda>x. THE y. P x y" in ex1I)
   3.997 -  apply (fast dest!: theI')
   3.998 -  apply (fast intro: the1_equality [symmetric])
   3.999 +   apply (rule_tac a = "\<lambda>x. THE y. P x y" in ex1I)
  3.1000 +    apply (fast dest!: theI')
  3.1001 +   apply (fast intro: the1_equality [symmetric])
  3.1002    apply (erule ex1E)
  3.1003    apply (rule allI)
  3.1004    apply (rule ex1I)
  3.1005 -  apply (erule spec)
  3.1006 +   apply (erule spec)
  3.1007    apply (erule_tac x = "\<lambda>z. if z = x then y else f z" in allE)
  3.1008    apply (erule impE)
  3.1009 -  apply (rule allI)
  3.1010 -  apply (case_tac "xa = x")
  3.1011 -  apply (drule_tac [3] x = x in fun_cong, simp_all)
  3.1012 +   apply (rule allI)
  3.1013 +   apply (case_tac "xa = x")
  3.1014 +    apply (drule_tac [3] x = x in fun_cong)
  3.1015 +    apply simp_all
  3.1016    done
  3.1017  
  3.1018  lemmas eq_sym_conv = eq_commute
  3.1019  
  3.1020  lemma nnf_simps:
  3.1021 -  "(\<not>(P \<and> Q)) = (\<not> P \<or> \<not> Q)" "(\<not> (P \<or> Q)) = (\<not> P \<and> \<not>Q)" "(P \<longrightarrow> Q) = (\<not>P \<or> Q)"
  3.1022 -  "(P = Q) = ((P \<and> Q) \<or> (\<not>P \<and> \<not> Q))" "(\<not>(P = Q)) = ((P \<and> \<not> Q) \<or> (\<not>P \<and> Q))"
  3.1023 -  "(\<not> \<not>(P)) = P"
  3.1024 -by blast+
  3.1025 +  "(\<not> (P \<and> Q)) = (\<not> P \<or> \<not> Q)"
  3.1026 +  "(\<not> (P \<or> Q)) = (\<not> P \<and> \<not> Q)"
  3.1027 +  "(P \<longrightarrow> Q) = (\<not> P \<or> Q)"
  3.1028 +  "(P = Q) = ((P \<and> Q) \<or> (\<not> P \<and> \<not> Q))"
  3.1029 +  "(\<not> (P = Q)) = ((P \<and> \<not> Q) \<or> (\<not> P \<and> Q))"
  3.1030 +  "(\<not> \<not> P) = P"
  3.1031 +  by blast+
  3.1032 +
  3.1033  
  3.1034  subsection \<open>Basic ML bindings\<close>
  3.1035  
  3.1036 @@ -1659,12 +1652,15 @@
  3.1037  section \<open>\<open>NO_MATCH\<close> simproc\<close>
  3.1038  
  3.1039  text \<open>
  3.1040 - The simplification procedure can be used to avoid simplification of terms of a certain form
  3.1041 +  The simplification procedure can be used to avoid simplification of terms
  3.1042 +  of a certain form.
  3.1043  \<close>
  3.1044  
  3.1045 -definition NO_MATCH :: "'a \<Rightarrow> 'b \<Rightarrow> bool" where "NO_MATCH pat val \<equiv> True"
  3.1046 +definition NO_MATCH :: "'a \<Rightarrow> 'b \<Rightarrow> bool"
  3.1047 +  where "NO_MATCH pat val \<equiv> True"
  3.1048  
  3.1049 -lemma NO_MATCH_cong[cong]: "NO_MATCH pat val = NO_MATCH pat val" by (rule refl)
  3.1050 +lemma NO_MATCH_cong[cong]: "NO_MATCH pat val = NO_MATCH pat val"
  3.1051 +  by (rule refl)
  3.1052  
  3.1053  declare [[coercion_args NO_MATCH - -]]
  3.1054  
  3.1055 @@ -1678,24 +1674,26 @@
  3.1056  
  3.1057  text \<open>
  3.1058    This setup ensures that a rewrite rule of the form @{term "NO_MATCH pat val \<Longrightarrow> t"}
  3.1059 -  is only applied, if the pattern @{term pat} does not match the value @{term val}.
  3.1060 +  is only applied, if the pattern \<open>pat\<close> does not match the value \<open>val\<close>.
  3.1061  \<close>
  3.1062  
  3.1063  
  3.1064 -text\<open>Tagging a premise of a simp rule with ASSUMPTION forces the simplifier
  3.1065 -not to simplify the argument and to solve it by an assumption.\<close>
  3.1066 +text\<open>
  3.1067 +  Tagging a premise of a simp rule with ASSUMPTION forces the simplifier
  3.1068 +  not to simplify the argument and to solve it by an assumption.
  3.1069 +\<close>
  3.1070  
  3.1071 -definition ASSUMPTION :: "bool \<Rightarrow> bool" where
  3.1072 -"ASSUMPTION A \<equiv> A"
  3.1073 +definition ASSUMPTION :: "bool \<Rightarrow> bool"
  3.1074 +  where "ASSUMPTION A \<equiv> A"
  3.1075  
  3.1076  lemma ASSUMPTION_cong[cong]: "ASSUMPTION A = ASSUMPTION A"
  3.1077 -by (rule refl)
  3.1078 +  by (rule refl)
  3.1079  
  3.1080  lemma ASSUMPTION_I: "A \<Longrightarrow> ASSUMPTION A"
  3.1081 -by(simp add: ASSUMPTION_def)
  3.1082 +  by (simp add: ASSUMPTION_def)
  3.1083  
  3.1084  lemma ASSUMPTION_D: "ASSUMPTION A \<Longrightarrow> A"
  3.1085 -by(simp add: ASSUMPTION_def)
  3.1086 +  by (simp add: ASSUMPTION_def)
  3.1087  
  3.1088  setup \<open>
  3.1089  let
  3.1090 @@ -1712,12 +1710,10 @@
  3.1091  
  3.1092  subsubsection \<open>Generic code generator preprocessor setup\<close>
  3.1093  
  3.1094 -lemma conj_left_cong:
  3.1095 -  "P \<longleftrightarrow> Q \<Longrightarrow> P \<and> R \<longleftrightarrow> Q \<and> R"
  3.1096 +lemma conj_left_cong: "P \<longleftrightarrow> Q \<Longrightarrow> P \<and> R \<longleftrightarrow> Q \<and> R"
  3.1097    by (fact arg_cong)
  3.1098  
  3.1099 -lemma disj_left_cong:
  3.1100 -  "P \<longleftrightarrow> Q \<Longrightarrow> P \<or> R \<longleftrightarrow> Q \<or> R"
  3.1101 +lemma disj_left_cong: "P \<longleftrightarrow> Q \<Longrightarrow> P \<or> R \<longleftrightarrow> Q \<or> R"
  3.1102    by (fact arg_cong)
  3.1103  
  3.1104  setup \<open>
  3.1105 @@ -1772,29 +1768,32 @@
  3.1106    shows "False \<and> P \<longleftrightarrow> False"
  3.1107      and "True \<and> P \<longleftrightarrow> P"
  3.1108      and "P \<and> False \<longleftrightarrow> False"
  3.1109 -    and "P \<and> True \<longleftrightarrow> P" by simp_all
  3.1110 +    and "P \<and> True \<longleftrightarrow> P"
  3.1111 +  by simp_all
  3.1112  
  3.1113  lemma [code]:
  3.1114    shows "False \<or> P \<longleftrightarrow> P"
  3.1115      and "True \<or> P \<longleftrightarrow> True"
  3.1116      and "P \<or> False \<longleftrightarrow> P"
  3.1117 -    and "P \<or> True \<longleftrightarrow> True" by simp_all
  3.1118 +    and "P \<or> True \<longleftrightarrow> True"
  3.1119 +  by simp_all
  3.1120  
  3.1121  lemma [code]:
  3.1122    shows "(False \<longrightarrow> P) \<longleftrightarrow> True"
  3.1123      and "(True \<longrightarrow> P) \<longleftrightarrow> P"
  3.1124      and "(P \<longrightarrow> False) \<longleftrightarrow> \<not> P"
  3.1125 -    and "(P \<longrightarrow> True) \<longleftrightarrow> True" by simp_all
  3.1126 +    and "(P \<longrightarrow> True) \<longleftrightarrow> True"
  3.1127 +  by simp_all
  3.1128  
  3.1129  text \<open>More about @{typ prop}\<close>
  3.1130  
  3.1131  lemma [code nbe]:
  3.1132    shows "(True \<Longrightarrow> PROP Q) \<equiv> PROP Q"
  3.1133      and "(PROP Q \<Longrightarrow> True) \<equiv> Trueprop True"
  3.1134 -    and "(P \<Longrightarrow> R) \<equiv> Trueprop (P \<longrightarrow> R)" by (auto intro!: equal_intr_rule)
  3.1135 +    and "(P \<Longrightarrow> R) \<equiv> Trueprop (P \<longrightarrow> R)"
  3.1136 +  by (auto intro!: equal_intr_rule)
  3.1137  
  3.1138 -lemma Trueprop_code [code]:
  3.1139 -  "Trueprop True \<equiv> Code_Generator.holds"
  3.1140 +lemma Trueprop_code [code]: "Trueprop True \<equiv> Code_Generator.holds"
  3.1141    by (auto intro!: equal_intr_rule holds)
  3.1142  
  3.1143  declare Trueprop_code [symmetric, code_post]
  3.1144 @@ -1806,21 +1805,21 @@
  3.1145  instantiation itself :: (type) equal
  3.1146  begin
  3.1147  
  3.1148 -definition equal_itself :: "'a itself \<Rightarrow> 'a itself \<Rightarrow> bool" where
  3.1149 -  "equal_itself x y \<longleftrightarrow> x = y"
  3.1150 +definition equal_itself :: "'a itself \<Rightarrow> 'a itself \<Rightarrow> bool"
  3.1151 +  where "equal_itself x y \<longleftrightarrow> x = y"
  3.1152  
  3.1153 -instance proof
  3.1154 -qed (fact equal_itself_def)
  3.1155 +instance
  3.1156 +  by standard (fact equal_itself_def)
  3.1157  
  3.1158  end
  3.1159  
  3.1160 -lemma equal_itself_code [code]:
  3.1161 -  "equal TYPE('a) TYPE('a) \<longleftrightarrow> True"
  3.1162 +lemma equal_itself_code [code]: "equal TYPE('a) TYPE('a) \<longleftrightarrow> True"
  3.1163    by (simp add: equal)
  3.1164  
  3.1165  setup \<open>Sign.add_const_constraint (@{const_name equal}, SOME @{typ "'a::type \<Rightarrow> 'a \<Rightarrow> bool"})\<close>
  3.1166  
  3.1167 -lemma equal_alias_cert: "OFCLASS('a, equal_class) \<equiv> ((op = :: 'a \<Rightarrow> 'a \<Rightarrow> bool) \<equiv> equal)" (is "?ofclass \<equiv> ?equal")
  3.1168 +lemma equal_alias_cert: "OFCLASS('a, equal_class) \<equiv> ((op = :: 'a \<Rightarrow> 'a \<Rightarrow> bool) \<equiv> equal)"
  3.1169 +  (is "?ofclass \<equiv> ?equal")
  3.1170  proof
  3.1171    assume "PROP ?ofclass"
  3.1172    show "PROP ?equal"
  3.1173 @@ -1900,15 +1899,13 @@
  3.1174    code_module Pure \<rightharpoonup>
  3.1175      (SML) HOL and (OCaml) HOL and (Haskell) HOL and (Scala) HOL
  3.1176  
  3.1177 -text \<open>using built-in Haskell equality\<close>
  3.1178 -
  3.1179 +text \<open>Using built-in Haskell equality.\<close>
  3.1180  code_printing
  3.1181    type_class equal \<rightharpoonup> (Haskell) "Eq"
  3.1182  | constant HOL.equal \<rightharpoonup> (Haskell) infix 4 "=="
  3.1183  | constant HOL.eq \<rightharpoonup> (Haskell) infix 4 "=="
  3.1184  
  3.1185 -text \<open>undefined\<close>
  3.1186 -
  3.1187 +text \<open>\<open>undefined\<close>\<close>
  3.1188  code_printing
  3.1189    constant undefined \<rightharpoonup>
  3.1190      (SML) "!(raise/ Fail/ \"undefined\")"
  3.1191 @@ -1956,7 +1953,7 @@
  3.1192    and nitpick_choice_spec "choice specification of constants as needed by Nitpick"
  3.1193  
  3.1194  declare if_bool_eq_conj [nitpick_unfold, no_atp]
  3.1195 -        if_bool_eq_disj [no_atp]
  3.1196 +  and if_bool_eq_disj [no_atp]
  3.1197  
  3.1198  
  3.1199  subsection \<open>Preprocessing for the predicate compiler\<close>
     4.1 --- a/src/HOL/Product_Type.thy	Mon Aug 01 13:51:17 2016 +0200
     4.2 +++ b/src/HOL/Product_Type.thy	Mon Aug 01 22:11:29 2016 +0200
     4.3 @@ -6,8 +6,8 @@
     4.4  section \<open>Cartesian products\<close>
     4.5  
     4.6  theory Product_Type
     4.7 -imports Typedef Inductive Fun
     4.8 -keywords "inductive_set" "coinductive_set" :: thy_decl
     4.9 +  imports Typedef Inductive Fun
    4.10 +  keywords "inductive_set" "coinductive_set" :: thy_decl
    4.11  begin
    4.12  
    4.13  subsection \<open>@{typ bool} is a datatype\<close>
    4.14 @@ -38,7 +38,7 @@
    4.15    \<comment> "prefer plain propositional version"
    4.16  
    4.17  lemma [code]: "HOL.equal False P \<longleftrightarrow> \<not> P"
    4.18 -  and [code]: "HOL.equal True P \<longleftrightarrow> P" 
    4.19 +  and [code]: "HOL.equal True P \<longleftrightarrow> P"
    4.20    and [code]: "HOL.equal P False \<longleftrightarrow> \<not> P"
    4.21    and [code]: "HOL.equal P True \<longleftrightarrow> P"
    4.22    and [code nbe]: "HOL.equal P P \<longleftrightarrow> True"
    4.23 @@ -317,7 +317,7 @@
    4.24            (case (head_of t) of
    4.25              Const (@{const_syntax case_prod}, _) => raise Match
    4.26            | _ =>
    4.27 -            let 
    4.28 +            let
    4.29                val (_ :: yT :: _) = binder_types (domain_type T) handle Bind => raise Match;
    4.30                val (y, t') = Syntax_Trans.atomic_abs_tr' ("y", yT, incr_boundvars 1 t $ Bound 0);
    4.31                val (x', t'') = Syntax_Trans.atomic_abs_tr' (x, xT, t');
    4.32 @@ -618,7 +618,7 @@
    4.33  declare case_prodI2' [intro!] \<comment> \<open>postponed to maintain traditional declaration order!\<close>
    4.34  declare case_prodI2 [intro!] \<comment> \<open>postponed to maintain traditional declaration order!\<close>
    4.35  declare case_prodI [intro!] \<comment> \<open>postponed to maintain traditional declaration order!\<close>
    4.36 -  
    4.37 +
    4.38  lemma mem_case_prodE [elim!]:
    4.39    assumes "z \<in> case_prod c p"
    4.40    obtains x y where "p = (x, y)" and "z \<in> c x y"
    4.41 @@ -631,10 +631,10 @@
    4.42      | exists_p_split (Abs (_, _, t)) = exists_p_split t
    4.43      | exists_p_split _ = false;
    4.44  in
    4.45 -fun split_conv_tac ctxt = SUBGOAL (fn (t, i) =>
    4.46 -  if exists_p_split t
    4.47 -  then safe_full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms case_prod_conv}) i
    4.48 -  else no_tac);
    4.49 +  fun split_conv_tac ctxt = SUBGOAL (fn (t, i) =>
    4.50 +    if exists_p_split t
    4.51 +    then safe_full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms case_prod_conv}) i
    4.52 +    else no_tac);
    4.53  end;
    4.54  \<close>
    4.55  
    4.56 @@ -656,7 +656,7 @@
    4.57     a) only helps in special situations
    4.58     b) can lead to nontermination in the presence of split_def
    4.59  *)
    4.60 -lemma split_comp_eq: 
    4.61 +lemma split_comp_eq:
    4.62    fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c"
    4.63      and g :: "'d \<Rightarrow> 'a"
    4.64    shows "(\<lambda>u. f (g (fst u)) (snd u)) = case_prod (\<lambda>x. f (g x))"
    4.65 @@ -836,7 +836,7 @@
    4.66    apply (rule major [THEN imageE])
    4.67    apply (case_tac x)
    4.68    apply (rule cases)
    4.69 -  apply simp_all
    4.70 +   apply simp_all
    4.71    done
    4.72  
    4.73  definition apfst :: "('a \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c \<times> 'b"
    4.74 @@ -845,10 +845,10 @@
    4.75  definition apsnd :: "('b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'a \<times> 'c"
    4.76    where "apsnd f = map_prod id f"
    4.77  
    4.78 -lemma apfst_conv [simp, code]: "apfst f (x, y) = (f x, y)" 
    4.79 +lemma apfst_conv [simp, code]: "apfst f (x, y) = (f x, y)"
    4.80    by (simp add: apfst_def)
    4.81  
    4.82 -lemma apsnd_conv [simp, code]: "apsnd f (x, y) = (x, f y)" 
    4.83 +lemma apsnd_conv [simp, code]: "apsnd f (x, y) = (x, f y)"
    4.84    by (simp add: apsnd_def)
    4.85  
    4.86  lemma fst_apfst [simp]: "fst (apfst f x) = f (fst x)"
    4.87 @@ -1029,11 +1029,11 @@
    4.88  lemma Collect_case_prod_mono: "A \<le> B \<Longrightarrow> Collect (case_prod A) \<subseteq> Collect (case_prod B)"
    4.89    by auto (auto elim!: le_funE)
    4.90  
    4.91 -lemma Collect_split_mono_strong: 
    4.92 +lemma Collect_split_mono_strong:
    4.93    "X = fst ` A \<Longrightarrow> Y = snd ` A \<Longrightarrow> \<forall>a\<in>X. \<forall>b \<in> Y. P a b \<longrightarrow> Q a b
    4.94      \<Longrightarrow> A \<subseteq> Collect (case_prod P) \<Longrightarrow> A \<subseteq> Collect (case_prod Q)"
    4.95    by fastforce
    4.96 -  
    4.97 +
    4.98  lemma UN_Times_distrib: "(\<Union>(a, b)\<in>A \<times> B. E a \<times> F b) = UNION A E \<times> UNION B F"
    4.99    \<comment> \<open>Suggested by Pierre Chartier\<close>
   4.100    by blast
   4.101 @@ -1151,18 +1151,19 @@
   4.102  context
   4.103  begin
   4.104  
   4.105 -qualified definition product :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set" where
   4.106 -  [code_abbrev]: "product A B = A \<times> B"
   4.107 +qualified definition product :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set"
   4.108 +  where [code_abbrev]: "product A B = A \<times> B"
   4.109  
   4.110  lemma member_product: "x \<in> Product_Type.product A B \<longleftrightarrow> x \<in> A \<times> B"
   4.111    by (simp add: product_def)
   4.112  
   4.113  end
   4.114 -  
   4.115 +
   4.116  text \<open>The following @{const map_prod} lemmas are due to Joachim Breitner:\<close>
   4.117  
   4.118  lemma map_prod_inj_on:
   4.119 -  assumes "inj_on f A" and "inj_on g B"
   4.120 +  assumes "inj_on f A"
   4.121 +    and "inj_on g B"
   4.122    shows "inj_on (map_prod f g) (A \<times> B)"
   4.123  proof (rule inj_onI)
   4.124    fix x :: "'a \<times> 'c"
     5.1 --- a/src/HOL/Sum_Type.thy	Mon Aug 01 13:51:17 2016 +0200
     5.2 +++ b/src/HOL/Sum_Type.thy	Mon Aug 01 22:11:29 2016 +0200
     5.3 @@ -3,10 +3,10 @@
     5.4      Copyright   1992  University of Cambridge
     5.5  *)
     5.6  
     5.7 -section\<open>The Disjoint Sum of Two Types\<close>
     5.8 +section \<open>The Disjoint Sum of Two Types\<close>
     5.9  
    5.10  theory Sum_Type
    5.11 -imports Typedef Inductive Fun
    5.12 +  imports Typedef Inductive Fun
    5.13  begin
    5.14  
    5.15  subsection \<open>Construction of the sum type and its basic abstract operations\<close>
    5.16 @@ -85,7 +85,8 @@
    5.17  proof (rule Abs_sum_cases [of s])
    5.18    fix f
    5.19    assume "s = Abs_sum f" and "f \<in> sum"
    5.20 -  with assms show P by (auto simp add: sum_def Inl_def Inr_def)
    5.21 +  with assms show P
    5.22 +    by (auto simp add: sum_def Inl_def Inr_def)
    5.23  qed
    5.24  
    5.25  free_constructors case_sum for
    5.26 @@ -123,9 +124,9 @@
    5.27  setup \<open>Sign.parent_path\<close>
    5.28  
    5.29  primrec map_sum :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> 'a + 'b \<Rightarrow> 'c + 'd"
    5.30 -where
    5.31 -  "map_sum f1 f2 (Inl a) = Inl (f1 a)"
    5.32 -| "map_sum f1 f2 (Inr a) = Inr (f2 a)"
    5.33 +  where
    5.34 +    "map_sum f1 f2 (Inl a) = Inl (f1 a)"
    5.35 +  | "map_sum f1 f2 (Inr a) = Inr (f2 a)"
    5.36  
    5.37  functor map_sum: map_sum
    5.38  proof -