# HG changeset patch
# User wenzelm
# Date 1470082289 -7200
# Node ID b9bd9e61fd633c07ee4dd6570d75ae4bb4754a14
# Parent  4ea48cbc54c1e8b5442b1c66b23c64f4784b99e7
misc tuning and modernization;

diff -r 4ea48cbc54c1 -r b9bd9e61fd63 src/HOL/Complete_Lattices.thy
--- a/src/HOL/Complete_Lattices.thy	Mon Aug 01 13:51:17 2016 +0200
+++ b/src/HOL/Complete_Lattices.thy	Mon Aug 01 22:11:29 2016 +0200
@@ -1,9 +1,14 @@
-(*  Author:     Tobias Nipkow, Lawrence C Paulson and Markus Wenzel; Florian Haftmann, TU Muenchen *)
+(*  Title:      HOL/Complete_Lattices.thy
+    Author:     Tobias Nipkow
+    Author:     Lawrence C Paulson
+    Author:     Markus Wenzel
+    Author:     Florian Haftmann
+*)
 
 section \<open>Complete lattices\<close>
 
 theory Complete_Lattices
-imports Fun
+  imports Fun
 begin
 
 notation
@@ -14,27 +19,22 @@
 subsection \<open>Syntactic infimum and supremum operations\<close>
 
 class Inf =
-  fixes Inf :: "'a set \<Rightarrow> 'a" ("\<Sqinter>_" [900] 900)
+  fixes Inf :: "'a set \<Rightarrow> 'a"  ("\<Sqinter>_" [900] 900)
 begin
 
 abbreviation INFIMUM :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a"
-where
-  "INFIMUM A f \<equiv> \<Sqinter>(f ` A)"
+  where "INFIMUM A f \<equiv> \<Sqinter>(f ` A)"
 
-lemma INF_image [simp]:
-  "INFIMUM (f ` A) g = INFIMUM A (g \<circ> f)"
+lemma INF_image [simp]: "INFIMUM (f ` A) g = INFIMUM A (g \<circ> f)"
   by (simp add: image_comp)
 
-lemma INF_identity_eq [simp]:
-  "INFIMUM A (\<lambda>x. x) = \<Sqinter>A"
+lemma INF_identity_eq [simp]: "INFIMUM A (\<lambda>x. x) = \<Sqinter>A"
   by simp
 
-lemma INF_id_eq [simp]:
-  "INFIMUM A id = \<Sqinter>A"
+lemma INF_id_eq [simp]: "INFIMUM A id = \<Sqinter>A"
   by simp
 
-lemma INF_cong:
-  "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> INFIMUM A C = INFIMUM B D"
+lemma INF_cong: "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> INFIMUM A C = INFIMUM B D"
   by (simp add: image_def)
 
 lemma strong_INF_cong [cong]:
@@ -44,27 +44,22 @@
 end
 
 class Sup =
-  fixes Sup :: "'a set \<Rightarrow> 'a" ("\<Squnion>_" [900] 900)
+  fixes Sup :: "'a set \<Rightarrow> 'a"  ("\<Squnion>_" [900] 900)
 begin
 
 abbreviation SUPREMUM :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a"
-where
-  "SUPREMUM A f \<equiv> \<Squnion>(f ` A)"
+  where "SUPREMUM A f \<equiv> \<Squnion>(f ` A)"
 
-lemma SUP_image [simp]:
-  "SUPREMUM (f ` A) g = SUPREMUM A (g \<circ> f)"
+lemma SUP_image [simp]: "SUPREMUM (f ` A) g = SUPREMUM A (g \<circ> f)"
   by (simp add: image_comp)
 
-lemma SUP_identity_eq [simp]:
-  "SUPREMUM A (\<lambda>x. x) = \<Squnion>A"
+lemma SUP_identity_eq [simp]: "SUPREMUM A (\<lambda>x. x) = \<Squnion>A"
   by simp
 
-lemma SUP_id_eq [simp]:
-  "SUPREMUM A id = \<Squnion>A"
+lemma SUP_id_eq [simp]: "SUPREMUM A id = \<Squnion>A"
   by (simp add: id_def)
 
-lemma SUP_cong:
-  "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> SUPREMUM A C = SUPREMUM B D"
+lemma SUP_cong: "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> SUPREMUM A C = SUPREMUM B D"
   by (simp add: image_def)
 
 lemma strong_SUP_cong [cong]:
@@ -122,25 +117,25 @@
 
 class complete_lattice = lattice + Inf + Sup + bot + top +
   assumes Inf_lower: "x \<in> A \<Longrightarrow> \<Sqinter>A \<sqsubseteq> x"
-     and Inf_greatest: "(\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x) \<Longrightarrow> z \<sqsubseteq> \<Sqinter>A"
-  assumes Sup_upper: "x \<in> A \<Longrightarrow> x \<sqsubseteq> \<Squnion>A"
-     and Sup_least: "(\<And>x. x \<in> A \<Longrightarrow> x \<sqsubseteq> z) \<Longrightarrow> \<Squnion>A \<sqsubseteq> z"
-  assumes Inf_empty [simp]: "\<Sqinter>{} = \<top>"
-  assumes Sup_empty [simp]: "\<Squnion>{} = \<bottom>"
+    and Inf_greatest: "(\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x) \<Longrightarrow> z \<sqsubseteq> \<Sqinter>A"
+    and Sup_upper: "x \<in> A \<Longrightarrow> x \<sqsubseteq> \<Squnion>A"
+    and Sup_least: "(\<And>x. x \<in> A \<Longrightarrow> x \<sqsubseteq> z) \<Longrightarrow> \<Squnion>A \<sqsubseteq> z"
+    and Inf_empty [simp]: "\<Sqinter>{} = \<top>"
+    and Sup_empty [simp]: "\<Squnion>{} = \<bottom>"
 begin
 
 subclass bounded_lattice
 proof
   fix a
-  show "\<bottom> \<le> a" by (auto intro: Sup_least simp only: Sup_empty [symmetric])
-  show "a \<le> \<top>" by (auto intro: Inf_greatest simp only: Inf_empty [symmetric])
+  show "\<bottom> \<le> a"
+    by (auto intro: Sup_least simp only: Sup_empty [symmetric])
+  show "a \<le> \<top>"
+    by (auto intro: Inf_greatest simp only: Inf_empty [symmetric])
 qed
 
-lemma dual_complete_lattice:
-  "class.complete_lattice Sup Inf sup (op \<ge>) (op >) inf \<top> \<bottom>"
+lemma dual_complete_lattice: "class.complete_lattice Sup Inf sup (op \<ge>) (op >) inf \<top> \<bottom>"
   by (auto intro!: class.complete_lattice.intro dual_lattice)
-    (unfold_locales, (fact Inf_empty Sup_empty
-        Sup_upper Sup_least Inf_lower Inf_greatest)+)
+    (unfold_locales, (fact Inf_empty Sup_empty Sup_upper Sup_least Inf_lower Inf_greatest)+)
 
 end
 
@@ -217,12 +212,10 @@
 lemma SUP_empty [simp]: "(\<Squnion>x\<in>{}. f x) = \<bottom>"
   by (simp cong del: strong_SUP_cong)
 
-lemma Inf_UNIV [simp]:
-  "\<Sqinter>UNIV = \<bottom>"
+lemma Inf_UNIV [simp]: "\<Sqinter>UNIV = \<bottom>"
   by (auto intro!: antisym Inf_lower)
 
-lemma Sup_UNIV [simp]:
-  "\<Squnion>UNIV = \<top>"
+lemma Sup_UNIV [simp]: "\<Squnion>UNIV = \<top>"
   by (auto intro!: antisym Sup_upper)
 
 lemma Inf_Sup: "\<Sqinter>A = \<Squnion>{b. \<forall>a \<in> A. b \<sqsubseteq> a}"
@@ -247,8 +240,7 @@
   with \<open>a \<sqsubseteq> b\<close> show "\<Sqinter>A \<sqsubseteq> b" by auto
 qed
 
-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)"
+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)"
   using Inf_mono [of "g ` B" "f ` A"] by auto
 
 lemma Sup_mono:
@@ -261,17 +253,14 @@
   with \<open>a \<sqsubseteq> b\<close> show "a \<sqsubseteq> \<Squnion>B" by auto
 qed
 
-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)"
+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)"
   using Sup_mono [of "f ` A" "g ` B"] by auto
 
-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)"
+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)"
   \<comment> \<open>The last inclusion is POSITIVE!\<close>
   by (blast intro: INF_mono dest: subsetD)
 
-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)"
+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)"
   by (blast intro: SUP_mono dest: subsetD)
 
 lemma Inf_less_eq:
@@ -296,13 +285,13 @@
 
 lemma INF_eq:
   assumes "\<And>i. i \<in> A \<Longrightarrow> \<exists>j\<in>B. f i \<ge> g j"
-  assumes "\<And>j. j \<in> B \<Longrightarrow> \<exists>i\<in>A. g j \<ge> f i"
+    and "\<And>j. j \<in> B \<Longrightarrow> \<exists>i\<in>A. g j \<ge> f i"
   shows "INFIMUM A f = INFIMUM B g"
   by (intro antisym INF_greatest) (blast intro: INF_lower2 dest: assms)+
 
 lemma SUP_eq:
   assumes "\<And>i. i \<in> A \<Longrightarrow> \<exists>j\<in>B. f i \<le> g j"
-  assumes "\<And>j. j \<in> B \<Longrightarrow> \<exists>i\<in>A. g j \<le> f i"
+    and "\<And>j. j \<in> B \<Longrightarrow> \<exists>i\<in>A. g j \<le> f i"
   shows "SUPREMUM A f = SUPREMUM B g"
   by (intro antisym SUP_least) (blast intro: SUP_upper2 dest: assms)+
 
@@ -315,25 +304,25 @@
 lemma Inf_union_distrib: "\<Sqinter>(A \<union> B) = \<Sqinter>A \<sqinter> \<Sqinter>B"
   by (rule antisym) (auto intro: Inf_greatest Inf_lower le_infI1 le_infI2)
 
-lemma INF_union:
-  "(\<Sqinter>i \<in> A \<union> B. M i) = (\<Sqinter>i \<in> A. M i) \<sqinter> (\<Sqinter>i\<in>B. M i)"
+lemma INF_union: "(\<Sqinter>i \<in> A \<union> B. M i) = (\<Sqinter>i \<in> A. M i) \<sqinter> (\<Sqinter>i\<in>B. M i)"
   by (auto intro!: antisym INF_mono intro: le_infI1 le_infI2 INF_greatest INF_lower)
 
 lemma Sup_union_distrib: "\<Squnion>(A \<union> B) = \<Squnion>A \<squnion> \<Squnion>B"
   by (rule antisym) (auto intro: Sup_least Sup_upper le_supI1 le_supI2)
 
-lemma SUP_union:
-  "(\<Squnion>i \<in> A \<union> B. M i) = (\<Squnion>i \<in> A. M i) \<squnion> (\<Squnion>i\<in>B. M i)"
+lemma SUP_union: "(\<Squnion>i \<in> A \<union> B. M i) = (\<Squnion>i \<in> A. M i) \<squnion> (\<Squnion>i\<in>B. M i)"
   by (auto intro!: antisym SUP_mono intro: le_supI1 le_supI2 SUP_least SUP_upper)
 
 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)"
   by (rule antisym) (rule INF_greatest, auto intro: le_infI1 le_infI2 INF_lower INF_mono)
 
-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")
+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")
 proof (rule antisym)
-  show "?L \<le> ?R" by (auto intro: le_supI1 le_supI2 SUP_upper SUP_mono)
-next
-  show "?R \<le> ?L" by (rule SUP_least) (auto intro: le_supI1 le_supI2 SUP_upper)
+  show "?L \<le> ?R"
+    by (auto intro: le_supI1 le_supI2 SUP_upper SUP_mono)
+  show "?R \<le> ?L"
+    by (rule SUP_least) (auto intro: le_supI1 le_supI2 SUP_upper)
 qed
 
 lemma Inf_top_conv [simp]:
@@ -364,14 +353,14 @@
   using Inf_top_conv [of "B ` A"] by simp_all
 
 lemma Sup_bot_conv [simp]:
-  "\<Squnion>A = \<bottom> \<longleftrightarrow> (\<forall>x\<in>A. x = \<bottom>)" (is ?P)
-  "\<bottom> = \<Squnion>A \<longleftrightarrow> (\<forall>x\<in>A. x = \<bottom>)" (is ?Q)
+  "\<Squnion>A = \<bottom> \<longleftrightarrow> (\<forall>x\<in>A. x = \<bottom>)"
+  "\<bottom> = \<Squnion>A \<longleftrightarrow> (\<forall>x\<in>A. x = \<bottom>)"
   using dual_complete_lattice
   by (rule complete_lattice.Inf_top_conv)+
 
 lemma SUP_bot_conv [simp]:
- "(\<Squnion>x\<in>A. B x) = \<bottom> \<longleftrightarrow> (\<forall>x\<in>A. B x = \<bottom>)"
- "\<bottom> = (\<Squnion>x\<in>A. B x) \<longleftrightarrow> (\<forall>x\<in>A. B x = \<bottom>)"
+  "(\<Squnion>x\<in>A. B x) = \<bottom> \<longleftrightarrow> (\<forall>x\<in>A. B x = \<bottom>)"
+  "\<bottom> = (\<Squnion>x\<in>A. B x) \<longleftrightarrow> (\<forall>x\<in>A. B x = \<bottom>)"
   using Sup_bot_conv [of "B ` A"] by simp_all
 
 lemma INF_const [simp]: "A \<noteq> {} \<Longrightarrow> (\<Sqinter>i\<in>A. f) = f"
@@ -408,25 +397,22 @@
   then show ?thesis by simp
 qed
 
-lemma INF_inf_const1:
-  "I \<noteq> {} \<Longrightarrow> (INF i:I. inf x (f i)) = inf x (INF i:I. f i)"
+lemma INF_inf_const1: "I \<noteq> {} \<Longrightarrow> (INF i:I. inf x (f i)) = inf x (INF i:I. f i)"
   by (intro antisym INF_greatest inf_mono order_refl INF_lower)
      (auto intro: INF_lower2 le_infI2 intro!: INF_mono)
 
-lemma INF_inf_const2:
-  "I \<noteq> {} \<Longrightarrow> (INF i:I. inf (f i) x) = inf (INF i:I. f i) x"
+lemma INF_inf_const2: "I \<noteq> {} \<Longrightarrow> (INF i:I. inf (f i) x) = inf (INF i:I. f i) x"
   using INF_inf_const1[of I x f] by (simp add: inf_commute)
 
-lemma INF_constant:
-  "(\<Sqinter>y\<in>A. c) = (if A = {} then \<top> else c)"
+lemma INF_constant: "(\<Sqinter>y\<in>A. c) = (if A = {} then \<top> else c)"
   by simp
 
-lemma SUP_constant:
-  "(\<Squnion>y\<in>A. c) = (if A = {} then \<bottom> else c)"
+lemma SUP_constant: "(\<Squnion>y\<in>A. c) = (if A = {} then \<bottom> else c)"
   by simp
 
 lemma less_INF_D:
-  assumes "y < (\<Sqinter>i\<in>A. f i)" "i \<in> A" shows "y < f i"
+  assumes "y < (\<Sqinter>i\<in>A. f i)" "i \<in> A"
+  shows "y < f i"
 proof -
   note \<open>y < (\<Sqinter>i\<in>A. f i)\<close>
   also have "(\<Sqinter>i\<in>A. f i) \<le> f i" using \<open>i \<in> A\<close>
@@ -435,20 +421,19 @@
 qed
 
 lemma SUP_lessD:
-  assumes "(\<Squnion>i\<in>A. f i) < y" "i \<in> A" shows "f i < y"
+  assumes "(\<Squnion>i\<in>A. f i) < y" "i \<in> A"
+  shows "f i < y"
 proof -
-  have "f i \<le> (\<Squnion>i\<in>A. f i)" using \<open>i \<in> A\<close>
-    by (rule SUP_upper)
+  have "f i \<le> (\<Squnion>i\<in>A. f i)"
+    using \<open>i \<in> A\<close> by (rule SUP_upper)
   also note \<open>(\<Squnion>i\<in>A. f i) < y\<close>
   finally show "f i < y" .
 qed
 
-lemma INF_UNIV_bool_expand:
-  "(\<Sqinter>b. A b) = A True \<sqinter> A False"
+lemma INF_UNIV_bool_expand: "(\<Sqinter>b. A b) = A True \<sqinter> A False"
   by (simp add: UNIV_bool inf_commute)
 
-lemma SUP_UNIV_bool_expand:
-  "(\<Squnion>b. A b) = A True \<squnion> A False"
+lemma SUP_UNIV_bool_expand: "(\<Squnion>b. A b) = A True \<squnion> A False"
   by (simp add: UNIV_bool sup_commute)
 
 lemma Inf_le_Sup: "A \<noteq> {} \<Longrightarrow> Inf A \<le> Sup A"
@@ -457,21 +442,17 @@
 lemma INF_le_SUP: "A \<noteq> {} \<Longrightarrow> INFIMUM A f \<le> SUPREMUM A f"
   using Inf_le_Sup [of "f ` A"] by simp
 
-lemma INF_eq_const:
-  "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i = x) \<Longrightarrow> INFIMUM I f = x"
+lemma INF_eq_const: "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i = x) \<Longrightarrow> INFIMUM I f = x"
   by (auto intro: INF_eqI)
 
-lemma SUP_eq_const:
-  "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i = x) \<Longrightarrow> SUPREMUM I f = x"
+lemma SUP_eq_const: "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i = x) \<Longrightarrow> SUPREMUM I f = x"
   by (auto intro: SUP_eqI)
 
-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)"
+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)"
   using INF_eq_const [of I f c] INF_lower [of _ I f]
   by (auto intro: antisym cong del: strong_INF_cong)
 
-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)"
+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)"
   using SUP_eq_const [of I f c] SUP_upper [of _ I f]
   by (auto intro: antisym cong del: strong_SUP_cong)
 
@@ -479,61 +460,52 @@
 
 class complete_distrib_lattice = complete_lattice +
   assumes sup_Inf: "a \<squnion> \<Sqinter>B = (\<Sqinter>b\<in>B. a \<squnion> b)"
-  assumes inf_Sup: "a \<sqinter> \<Squnion>B = (\<Squnion>b\<in>B. a \<sqinter> b)"
+    and inf_Sup: "a \<sqinter> \<Squnion>B = (\<Squnion>b\<in>B. a \<sqinter> b)"
 begin
 
-lemma sup_INF:
-  "a \<squnion> (\<Sqinter>b\<in>B. f b) = (\<Sqinter>b\<in>B. a \<squnion> f b)"
+lemma sup_INF: "a \<squnion> (\<Sqinter>b\<in>B. f b) = (\<Sqinter>b\<in>B. a \<squnion> f b)"
   by (simp add: sup_Inf)
 
-lemma inf_SUP:
-  "a \<sqinter> (\<Squnion>b\<in>B. f b) = (\<Squnion>b\<in>B. a \<sqinter> f b)"
+lemma inf_SUP: "a \<sqinter> (\<Squnion>b\<in>B. f b) = (\<Squnion>b\<in>B. a \<sqinter> f b)"
   by (simp add: inf_Sup)
 
 lemma dual_complete_distrib_lattice:
   "class.complete_distrib_lattice Sup Inf sup (op \<ge>) (op >) inf \<top> \<bottom>"
   apply (rule class.complete_distrib_lattice.intro)
-  apply (fact dual_complete_lattice)
+   apply (fact dual_complete_lattice)
   apply (rule class.complete_distrib_lattice_axioms.intro)
-  apply (simp_all add: inf_Sup sup_Inf)
+   apply (simp_all add: inf_Sup sup_Inf)
   done
 
-subclass distrib_lattice proof
+subclass distrib_lattice
+proof
   fix a b c
-  from sup_Inf have "a \<squnion> \<Sqinter>{b, c} = (\<Sqinter>d\<in>{b, c}. a \<squnion> d)" .
+  have "a \<squnion> \<Sqinter>{b, c} = (\<Sqinter>d\<in>{b, c}. a \<squnion> d)" by (rule sup_Inf)
   then show "a \<squnion> b \<sqinter> c = (a \<squnion> b) \<sqinter> (a \<squnion> c)" by simp
 qed
 
-lemma Inf_sup:
-  "\<Sqinter>B \<squnion> a = (\<Sqinter>b\<in>B. b \<squnion> a)"
+lemma Inf_sup: "\<Sqinter>B \<squnion> a = (\<Sqinter>b\<in>B. b \<squnion> a)"
   by (simp add: sup_Inf sup_commute)
 
-lemma Sup_inf:
-  "\<Squnion>B \<sqinter> a = (\<Squnion>b\<in>B. b \<sqinter> a)"
+lemma Sup_inf: "\<Squnion>B \<sqinter> a = (\<Squnion>b\<in>B. b \<sqinter> a)"
   by (simp add: inf_Sup inf_commute)
 
-lemma INF_sup: 
-  "(\<Sqinter>b\<in>B. f b) \<squnion> a = (\<Sqinter>b\<in>B. f b \<squnion> a)"
+lemma INF_sup: "(\<Sqinter>b\<in>B. f b) \<squnion> a = (\<Sqinter>b\<in>B. f b \<squnion> a)"
   by (simp add: sup_INF sup_commute)
 
-lemma SUP_inf:
-  "(\<Squnion>b\<in>B. f b) \<sqinter> a = (\<Squnion>b\<in>B. f b \<sqinter> a)"
+lemma SUP_inf: "(\<Squnion>b\<in>B. f b) \<sqinter> a = (\<Squnion>b\<in>B. f b \<sqinter> a)"
   by (simp add: inf_SUP inf_commute)
 
-lemma Inf_sup_eq_top_iff:
-  "(\<Sqinter>B \<squnion> a = \<top>) \<longleftrightarrow> (\<forall>b\<in>B. b \<squnion> a = \<top>)"
+lemma Inf_sup_eq_top_iff: "(\<Sqinter>B \<squnion> a = \<top>) \<longleftrightarrow> (\<forall>b\<in>B. b \<squnion> a = \<top>)"
   by (simp only: Inf_sup INF_top_conv)
 
-lemma Sup_inf_eq_bot_iff:
-  "(\<Squnion>B \<sqinter> a = \<bottom>) \<longleftrightarrow> (\<forall>b\<in>B. b \<sqinter> a = \<bottom>)"
+lemma Sup_inf_eq_bot_iff: "(\<Squnion>B \<sqinter> a = \<bottom>) \<longleftrightarrow> (\<forall>b\<in>B. b \<sqinter> a = \<bottom>)"
   by (simp only: Sup_inf SUP_bot_conv)
 
-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)"
+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)"
   by (subst INF_commute) (simp add: sup_INF INF_sup)
 
-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)"
+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)"
   by (subst SUP_commute) (simp add: inf_SUP SUP_inf)
 
 context
@@ -541,20 +513,16 @@
   assumes "mono f"
 begin
 
-lemma mono_Inf:
-  shows "f (\<Sqinter>A) \<le> (\<Sqinter>x\<in>A. f x)"
+lemma mono_Inf: "f (\<Sqinter>A) \<le> (\<Sqinter>x\<in>A. f x)"
   using \<open>mono f\<close> by (auto intro: complete_lattice_class.INF_greatest Inf_lower dest: monoD)
 
-lemma mono_Sup:
-  shows "(\<Squnion>x\<in>A. f x) \<le> f (\<Squnion>A)"
+lemma mono_Sup: "(\<Squnion>x\<in>A. f x) \<le> f (\<Squnion>A)"
   using \<open>mono f\<close> by (auto intro: complete_lattice_class.SUP_least Sup_upper dest: monoD)
 
-lemma mono_INF:
-  "f (INF i : I. A i) \<le> (INF x : I. f (A x))"
+lemma mono_INF: "f (INF i : I. A i) \<le> (INF x : I. f (A x))"
   by (intro complete_lattice_class.INF_greatest monoD[OF \<open>mono f\<close>] INF_lower)
 
-lemma mono_SUP:
-  "(SUP x : I. f (A x)) \<le> f (SUP i : I. A i)"
+lemma mono_SUP: "(SUP x : I. f (A x)) \<le> f (SUP i : I. A i)"
   by (intro complete_lattice_class.SUP_least monoD[OF \<open>mono f\<close>] SUP_upper)
 
 end
@@ -566,10 +534,11 @@
 
 lemma dual_complete_boolean_algebra:
   "class.complete_boolean_algebra Sup Inf sup (op \<ge>) (op >) inf \<top> \<bottom> (\<lambda>x y. x \<squnion> - y) uminus"
-  by (rule class.complete_boolean_algebra.intro, rule dual_complete_distrib_lattice, rule dual_boolean_algebra)
+  by (rule class.complete_boolean_algebra.intro,
+      rule dual_complete_distrib_lattice,
+      rule dual_boolean_algebra)
 
-lemma uminus_Inf:
-  "- (\<Sqinter>A) = \<Squnion>(uminus ` A)"
+lemma uminus_Inf: "- (\<Sqinter>A) = \<Squnion>(uminus ` A)"
 proof (rule antisym)
   show "- \<Sqinter>A \<le> \<Squnion>(uminus ` A)"
     by (rule compl_le_swap2, rule Inf_greatest, rule compl_le_swap2, rule Sup_upper) simp
@@ -580,13 +549,13 @@
 lemma uminus_INF: "- (\<Sqinter>x\<in>A. B x) = (\<Squnion>x\<in>A. - B x)"
   by (simp add: uminus_Inf image_image)
 
-lemma uminus_Sup:
-  "- (\<Squnion>A) = \<Sqinter>(uminus ` A)"
+lemma uminus_Sup: "- (\<Squnion>A) = \<Sqinter>(uminus ` A)"
 proof -
-  have "\<Squnion>A = - \<Sqinter>(uminus ` A)" by (simp add: image_image uminus_INF)
+  have "\<Squnion>A = - \<Sqinter>(uminus ` A)"
+    by (simp add: image_image uminus_INF)
   then show ?thesis by simp
 qed
-  
+
 lemma uminus_SUP: "- (\<Squnion>x\<in>A. B x) = (\<Sqinter>x\<in>A. - B x)"
   by (simp add: uminus_Sup image_image)
 
@@ -605,29 +574,27 @@
 lemma complete_linorder_sup_max: "sup = max"
   by (auto intro: antisym simp add: max_def fun_eq_iff)
 
-lemma Inf_less_iff:
-  "\<Sqinter>S \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>S. x \<sqsubset> a)"
+lemma Inf_less_iff: "\<Sqinter>S \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>S. x \<sqsubset> a)"
   by (simp add: not_le [symmetric] le_Inf_iff)
 
-lemma INF_less_iff:
-  "(\<Sqinter>i\<in>A. f i) \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>A. f x \<sqsubset> a)"
+lemma INF_less_iff: "(\<Sqinter>i\<in>A. f i) \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>A. f x \<sqsubset> a)"
   by (simp add: Inf_less_iff [of "f ` A"])
 
-lemma less_Sup_iff:
-  "a \<sqsubset> \<Squnion>S \<longleftrightarrow> (\<exists>x\<in>S. a \<sqsubset> x)"
+lemma less_Sup_iff: "a \<sqsubset> \<Squnion>S \<longleftrightarrow> (\<exists>x\<in>S. a \<sqsubset> x)"
   by (simp add: not_le [symmetric] Sup_le_iff)
 
-lemma less_SUP_iff:
-  "a \<sqsubset> (\<Squnion>i\<in>A. f i) \<longleftrightarrow> (\<exists>x\<in>A. a \<sqsubset> f x)"
+lemma less_SUP_iff: "a \<sqsubset> (\<Squnion>i\<in>A. f i) \<longleftrightarrow> (\<exists>x\<in>A. a \<sqsubset> f x)"
   by (simp add: less_Sup_iff [of _ "f ` A"])
 
-lemma Sup_eq_top_iff [simp]:
-  "\<Squnion>A = \<top> \<longleftrightarrow> (\<forall>x<\<top>. \<exists>i\<in>A. x < i)"
+lemma Sup_eq_top_iff [simp]: "\<Squnion>A = \<top> \<longleftrightarrow> (\<forall>x<\<top>. \<exists>i\<in>A. x < i)"
 proof
   assume *: "\<Squnion>A = \<top>"
-  show "(\<forall>x<\<top>. \<exists>i\<in>A. x < i)" unfolding * [symmetric]
+  show "(\<forall>x<\<top>. \<exists>i\<in>A. x < i)"
+    unfolding * [symmetric]
   proof (intro allI impI)
-    fix x assume "x < \<Squnion>A" then show "\<exists>i\<in>A. x < i"
+    fix x
+    assume "x < \<Squnion>A"
+    then show "\<exists>i\<in>A. x < i"
       by (simp add: less_Sup_iff)
   qed
 next
@@ -635,42 +602,40 @@
   show "\<Squnion>A = \<top>"
   proof (rule ccontr)
     assume "\<Squnion>A \<noteq> \<top>"
-    with top_greatest [of "\<Squnion>A"]
-    have "\<Squnion>A < \<top>" unfolding le_less by auto
-    then have "\<Squnion>A < \<Squnion>A"
-      using * unfolding less_Sup_iff by auto
+    with top_greatest [of "\<Squnion>A"] have "\<Squnion>A < \<top>"
+      unfolding le_less by auto
+    with * have "\<Squnion>A < \<Squnion>A"
+      unfolding less_Sup_iff by auto
     then show False by auto
   qed
 qed
 
-lemma SUP_eq_top_iff [simp]:
-  "(\<Squnion>i\<in>A. f i) = \<top> \<longleftrightarrow> (\<forall>x<\<top>. \<exists>i\<in>A. x < f i)"
+lemma SUP_eq_top_iff [simp]: "(\<Squnion>i\<in>A. f i) = \<top> \<longleftrightarrow> (\<forall>x<\<top>. \<exists>i\<in>A. x < f i)"
   using Sup_eq_top_iff [of "f ` A"] by simp
 
-lemma Inf_eq_bot_iff [simp]:
-  "\<Sqinter>A = \<bottom> \<longleftrightarrow> (\<forall>x>\<bottom>. \<exists>i\<in>A. i < x)"
+lemma Inf_eq_bot_iff [simp]: "\<Sqinter>A = \<bottom> \<longleftrightarrow> (\<forall>x>\<bottom>. \<exists>i\<in>A. i < x)"
   using dual_complete_linorder
   by (rule complete_linorder.Sup_eq_top_iff)
 
-lemma INF_eq_bot_iff [simp]:
-  "(\<Sqinter>i\<in>A. f i) = \<bottom> \<longleftrightarrow> (\<forall>x>\<bottom>. \<exists>i\<in>A. f i < x)"
+lemma INF_eq_bot_iff [simp]: "(\<Sqinter>i\<in>A. f i) = \<bottom> \<longleftrightarrow> (\<forall>x>\<bottom>. \<exists>i\<in>A. f i < x)"
   using Inf_eq_bot_iff [of "f ` A"] by simp
 
 lemma Inf_le_iff: "\<Sqinter>A \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>a\<in>A. y > a)"
 proof safe
-  fix y assume "x \<ge> \<Sqinter>A" "y > x"
+  fix y
+  assume "x \<ge> \<Sqinter>A" "y > x"
   then have "y > \<Sqinter>A" by auto
   then show "\<exists>a\<in>A. y > a"
     unfolding Inf_less_iff .
 qed (auto elim!: allE[of _ "\<Sqinter>A"] simp add: not_le[symmetric] Inf_lower)
 
-lemma INF_le_iff:
-  "INFIMUM A f \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>i\<in>A. y > f i)"
+lemma INF_le_iff: "INFIMUM A f \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>i\<in>A. y > f i)"
   using Inf_le_iff [of "f ` A"] by simp
 
 lemma le_Sup_iff: "x \<le> \<Squnion>A \<longleftrightarrow> (\<forall>y<x. \<exists>a\<in>A. y < a)"
 proof safe
-  fix y assume "x \<le> \<Squnion>A" "y < x"
+  fix y
+  assume "x \<le> \<Squnion>A" "y < x"
   then have "y < \<Squnion>A" by auto
   then show "\<exists>a\<in>A. y < a"
     unfolding less_Sup_iff .
@@ -696,35 +661,29 @@
 instantiation bool :: complete_lattice
 begin
 
-definition
-  [simp, code]: "\<Sqinter>A \<longleftrightarrow> False \<notin> A"
+definition [simp, code]: "\<Sqinter>A \<longleftrightarrow> False \<notin> A"
 
-definition
-  [simp, code]: "\<Squnion>A \<longleftrightarrow> True \<in> A"
+definition [simp, code]: "\<Squnion>A \<longleftrightarrow> True \<in> A"
 
-instance proof
-qed (auto intro: bool_induct)
+instance
+  by standard (auto intro: bool_induct)
 
 end
 
-lemma not_False_in_image_Ball [simp]:
-  "False \<notin> P ` A \<longleftrightarrow> Ball A P"
+lemma not_False_in_image_Ball [simp]: "False \<notin> P ` A \<longleftrightarrow> Ball A P"
   by auto
 
-lemma True_in_image_Bex [simp]:
-  "True \<in> P ` A \<longleftrightarrow> Bex A P"
+lemma True_in_image_Bex [simp]: "True \<in> P ` A \<longleftrightarrow> Bex A P"
   by auto
 
-lemma INF_bool_eq [simp]:
-  "INFIMUM = Ball"
+lemma INF_bool_eq [simp]: "INFIMUM = Ball"
   by (simp add: fun_eq_iff)
 
-lemma SUP_bool_eq [simp]:
-  "SUPREMUM = Bex"
+lemma SUP_bool_eq [simp]: "SUPREMUM = Bex"
   by (simp add: fun_eq_iff)
 
-instance bool :: complete_boolean_algebra proof
-qed (auto intro: bool_induct)
+instance bool :: complete_boolean_algebra
+  by standard (auto intro: bool_induct)
 
 
 subsection \<open>Complete lattice on @{typ "_ \<Rightarrow> _"}\<close>
@@ -732,11 +691,9 @@
 instantiation "fun" :: (type, Inf) Inf
 begin
 
-definition
-  "\<Sqinter>A = (\<lambda>x. \<Sqinter>f\<in>A. f x)"
+definition "\<Sqinter>A = (\<lambda>x. \<Sqinter>f\<in>A. f x)"
 
-lemma Inf_apply [simp, code]:
-  "(\<Sqinter>A) x = (\<Sqinter>f\<in>A. f x)"
+lemma Inf_apply [simp, code]: "(\<Sqinter>A) x = (\<Sqinter>f\<in>A. f x)"
   by (simp add: Inf_fun_def)
 
 instance ..
@@ -746,11 +703,9 @@
 instantiation "fun" :: (type, Sup) Sup
 begin
 
-definition
-  "\<Squnion>A = (\<lambda>x. \<Squnion>f\<in>A. f x)"
+definition "\<Squnion>A = (\<lambda>x. \<Squnion>f\<in>A. f x)"
 
-lemma Sup_apply [simp, code]:
-  "(\<Squnion>A) x = (\<Squnion>f\<in>A. f x)"
+lemma Sup_apply [simp, code]: "(\<Squnion>A) x = (\<Squnion>f\<in>A. f x)"
   by (simp add: Sup_fun_def)
 
 instance ..
@@ -760,57 +715,47 @@
 instantiation "fun" :: (type, complete_lattice) complete_lattice
 begin
 
-instance proof
-qed (auto simp add: le_fun_def intro: INF_lower INF_greatest SUP_upper SUP_least)
+instance
+  by standard (auto simp add: le_fun_def intro: INF_lower INF_greatest SUP_upper SUP_least)
 
 end
 
-lemma INF_apply [simp]:
-  "(\<Sqinter>y\<in>A. f y) x = (\<Sqinter>y\<in>A. f y x)"
+lemma INF_apply [simp]: "(\<Sqinter>y\<in>A. f y) x = (\<Sqinter>y\<in>A. f y x)"
   using Inf_apply [of "f ` A"] by (simp add: comp_def)
 
-lemma SUP_apply [simp]:
-  "(\<Squnion>y\<in>A. f y) x = (\<Squnion>y\<in>A. f y x)"
+lemma SUP_apply [simp]: "(\<Squnion>y\<in>A. f y) x = (\<Squnion>y\<in>A. f y x)"
   using Sup_apply [of "f ` A"] by (simp add: comp_def)
 
-instance "fun" :: (type, complete_distrib_lattice) complete_distrib_lattice proof
-qed (auto simp add: inf_Sup sup_Inf fun_eq_iff image_image)
+instance "fun" :: (type, complete_distrib_lattice) complete_distrib_lattice
+  by standard (auto simp add: inf_Sup sup_Inf fun_eq_iff image_image)
 
 instance "fun" :: (type, complete_boolean_algebra) complete_boolean_algebra ..
 
 
 subsection \<open>Complete lattice on unary and binary predicates\<close>
 
-lemma Inf1_I: 
-  "(\<And>P. P \<in> A \<Longrightarrow> P a) \<Longrightarrow> (\<Sqinter>A) a"
+lemma Inf1_I: "(\<And>P. P \<in> A \<Longrightarrow> P a) \<Longrightarrow> (\<Sqinter>A) a"
   by auto
 
-lemma INF1_I:
-  "(\<And>x. x \<in> A \<Longrightarrow> B x b) \<Longrightarrow> (\<Sqinter>x\<in>A. B x) b"
+lemma INF1_I: "(\<And>x. x \<in> A \<Longrightarrow> B x b) \<Longrightarrow> (\<Sqinter>x\<in>A. B x) b"
   by simp
 
-lemma INF2_I:
-  "(\<And>x. x \<in> A \<Longrightarrow> B x b c) \<Longrightarrow> (\<Sqinter>x\<in>A. B x) b c"
+lemma INF2_I: "(\<And>x. x \<in> A \<Longrightarrow> B x b c) \<Longrightarrow> (\<Sqinter>x\<in>A. B x) b c"
   by simp
 
-lemma Inf2_I: 
-  "(\<And>r. r \<in> A \<Longrightarrow> r a b) \<Longrightarrow> (\<Sqinter>A) a b"
+lemma Inf2_I: "(\<And>r. r \<in> A \<Longrightarrow> r a b) \<Longrightarrow> (\<Sqinter>A) a b"
   by auto
 
-lemma Inf1_D:
-  "(\<Sqinter>A) a \<Longrightarrow> P \<in> A \<Longrightarrow> P a"
+lemma Inf1_D: "(\<Sqinter>A) a \<Longrightarrow> P \<in> A \<Longrightarrow> P a"
   by auto
 
-lemma INF1_D:
-  "(\<Sqinter>x\<in>A. B x) b \<Longrightarrow> a \<in> A \<Longrightarrow> B a b"
+lemma INF1_D: "(\<Sqinter>x\<in>A. B x) b \<Longrightarrow> a \<in> A \<Longrightarrow> B a b"
   by simp
 
-lemma Inf2_D:
-  "(\<Sqinter>A) a b \<Longrightarrow> r \<in> A \<Longrightarrow> r a b"
+lemma Inf2_D: "(\<Sqinter>A) a b \<Longrightarrow> r \<in> A \<Longrightarrow> r a b"
   by auto
 
-lemma INF2_D:
-  "(\<Sqinter>x\<in>A. B x) b c \<Longrightarrow> a \<in> A \<Longrightarrow> B a b c"
+lemma INF2_D: "(\<Sqinter>x\<in>A. B x) b c \<Longrightarrow> a \<in> A \<Longrightarrow> B a b c"
   by simp
 
 lemma Inf1_E:
@@ -833,20 +778,16 @@
   obtains "B a b c" | "a \<notin> A"
   using assms by auto
 
-lemma Sup1_I:
-  "P \<in> A \<Longrightarrow> P a \<Longrightarrow> (\<Squnion>A) a"
+lemma Sup1_I: "P \<in> A \<Longrightarrow> P a \<Longrightarrow> (\<Squnion>A) a"
   by auto
 
-lemma SUP1_I:
-  "a \<in> A \<Longrightarrow> B a b \<Longrightarrow> (\<Squnion>x\<in>A. B x) b"
+lemma SUP1_I: "a \<in> A \<Longrightarrow> B a b \<Longrightarrow> (\<Squnion>x\<in>A. B x) b"
   by auto
 
-lemma Sup2_I:
-  "r \<in> A \<Longrightarrow> r a b \<Longrightarrow> (\<Squnion>A) a b"
+lemma Sup2_I: "r \<in> A \<Longrightarrow> r a b \<Longrightarrow> (\<Squnion>A) a b"
   by auto
 
-lemma SUP2_I:
-  "a \<in> A \<Longrightarrow> B a b c \<Longrightarrow> (\<Squnion>x\<in>A. B x) b c"
+lemma SUP2_I: "a \<in> A \<Longrightarrow> B a b c \<Longrightarrow> (\<Squnion>x\<in>A. B x) b c"
   by auto
 
 lemma Sup1_E:
@@ -875,29 +816,25 @@
 instantiation "set" :: (type) complete_lattice
 begin
 
-definition
-  "\<Sqinter>A = {x. \<Sqinter>((\<lambda>B. x \<in> B) ` A)}"
+definition "\<Sqinter>A = {x. \<Sqinter>((\<lambda>B. x \<in> B) ` A)}"
 
-definition
-  "\<Squnion>A = {x. \<Squnion>((\<lambda>B. x \<in> B) ` A)}"
+definition "\<Squnion>A = {x. \<Squnion>((\<lambda>B. x \<in> B) ` A)}"
 
-instance proof
-qed (auto simp add: less_eq_set_def Inf_set_def Sup_set_def le_fun_def)
+instance
+  by standard (auto simp add: less_eq_set_def Inf_set_def Sup_set_def le_fun_def)
 
 end
 
 instance "set" :: (type) complete_boolean_algebra
-proof
-qed (auto simp add: Inf_set_def Sup_set_def image_def)
-  
+  by standard (auto simp add: Inf_set_def Sup_set_def image_def)
+
 
 subsubsection \<open>Inter\<close>
 
 abbreviation Inter :: "'a set set \<Rightarrow> 'a set"  ("\<Inter>_" [900] 900)
   where "\<Inter>S \<equiv> \<Sqinter>S"
-  
-lemma Inter_eq:
-  "\<Inter>A = {x. \<forall>B \<in> A. x \<in> B}"
+
+lemma Inter_eq: "\<Inter>A = {x. \<forall>B \<in> A. x \<in> B}"
 proof (rule set_eqI)
   fix x
   have "(\<forall>Q\<in>{P. \<exists>B\<in>A. P \<longleftrightarrow> x \<in> B}. Q) \<longleftrightarrow> (\<forall>B\<in>A. x \<in> B)"
@@ -913,7 +850,7 @@
   by (simp add: Inter_eq)
 
 text \<open>
-  \medskip A ``destruct'' rule -- every @{term X} in @{term C}
+  \<^medskip> A ``destruct'' rule -- every @{term X} in @{term C}
   contains @{term A} as an element, but @{prop "A \<in> X"} can hold when
   @{prop "X \<in> C"} does not!  This rule is analogous to \<open>spec\<close>.
 \<close>
@@ -924,13 +861,12 @@
 lemma InterE [elim]: "A \<in> \<Inter>C \<Longrightarrow> (X \<notin> C \<Longrightarrow> R) \<Longrightarrow> (A \<in> X \<Longrightarrow> R) \<Longrightarrow> R"
   \<comment> \<open>``Classical'' elimination rule -- does not require proving
     @{prop "X \<in> C"}.\<close>
-  by (unfold Inter_eq) blast
+  unfolding Inter_eq by blast
 
 lemma Inter_lower: "B \<in> A \<Longrightarrow> \<Inter>A \<subseteq> B"
   by (fact Inf_lower)
 
-lemma Inter_subset:
-  "(\<And>X. X \<in> A \<Longrightarrow> X \<subseteq> B) \<Longrightarrow> A \<noteq> {} \<Longrightarrow> \<Inter>A \<subseteq> B"
+lemma Inter_subset: "(\<And>X. X \<in> A \<Longrightarrow> X \<subseteq> B) \<Longrightarrow> A \<noteq> {} \<Longrightarrow> \<Inter>A \<subseteq> B"
   by (fact Inf_less_eq)
 
 lemma Inter_greatest: "(\<And>X. X \<in> A \<Longrightarrow> C \<subseteq> X) \<Longrightarrow> C \<subseteq> \<Inter>A"
@@ -992,8 +928,7 @@
   [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax INTER} @{syntax_const "_INTER"}]
 \<close> \<comment> \<open>to avoid eta-contraction of body\<close>
 
-lemma INTER_eq:
-  "(\<Inter>x\<in>A. B x) = {y. \<forall>x\<in>A. y \<in> B x}"
+lemma INTER_eq: "(\<Inter>x\<in>A. B x) = {y. \<forall>x\<in>A. y \<in> B x}"
   by (auto intro!: INF_eqI)
 
 lemma INT_iff [simp]: "b \<in> (\<Inter>x\<in>A. B x) \<longleftrightarrow> (\<forall>x\<in>A. b \<in> B x)"
@@ -1036,23 +971,21 @@
 lemma INT_Un: "(\<Inter>i \<in> A \<union> B. M i) = (\<Inter>i \<in> A. M i) \<inter> (\<Inter>i\<in>B. M i)"
   by (fact INF_union)
 
-lemma INT_insert_distrib:
-  "u \<in> A \<Longrightarrow> (\<Inter>x\<in>A. insert a (B x)) = insert a (\<Inter>x\<in>A. B x)"
+lemma INT_insert_distrib: "u \<in> A \<Longrightarrow> (\<Inter>x\<in>A. insert a (B x)) = insert a (\<Inter>x\<in>A. B x)"
   by blast
 
 lemma INT_constant [simp]: "(\<Inter>y\<in>A. c) = (if A = {} then UNIV else c)"
   by (fact INF_constant)
 
 lemma INTER_UNIV_conv:
- "(UNIV = (\<Inter>x\<in>A. B x)) = (\<forall>x\<in>A. B x = UNIV)"
- "((\<Inter>x\<in>A. B x) = UNIV) = (\<forall>x\<in>A. B x = UNIV)"
+  "(UNIV = (\<Inter>x\<in>A. B x)) = (\<forall>x\<in>A. B x = UNIV)"
+  "((\<Inter>x\<in>A. B x) = UNIV) = (\<forall>x\<in>A. B x = UNIV)"
   by (fact INF_top_conv)+ (* already simp *)
 
 lemma INT_bool_eq: "(\<Inter>b. A b) = A True \<inter> A False"
   by (fact INF_UNIV_bool_expand)
 
-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)"
+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)"
   \<comment> \<open>The last inclusion is POSITIVE!\<close>
   by (fact INF_superset_mono)
 
@@ -1068,8 +1001,7 @@
 abbreviation Union :: "'a set set \<Rightarrow> 'a set"  ("\<Union>_" [900] 900)
   where "\<Union>S \<equiv> \<Squnion>S"
 
-lemma Union_eq:
-  "\<Union>A = {x. \<exists>B \<in> A. x \<in> B}"
+lemma Union_eq: "\<Union>A = {x. \<exists>B \<in> A. x \<in> B}"
 proof (rule set_eqI)
   fix x
   have "(\<exists>Q\<in>{P. \<exists>B\<in>A. P \<longleftrightarrow> x \<in> B}. Q) \<longleftrightarrow> (\<exists>B\<in>A. x \<in> B)"
@@ -1078,18 +1010,15 @@
     by (simp add: Sup_set_def image_def)
 qed
 
-lemma Union_iff [simp]:
-  "A \<in> \<Union>C \<longleftrightarrow> (\<exists>X\<in>C. A\<in>X)"
+lemma Union_iff [simp]: "A \<in> \<Union>C \<longleftrightarrow> (\<exists>X\<in>C. A\<in>X)"
   by (unfold Union_eq) blast
 
-lemma UnionI [intro]:
-  "X \<in> C \<Longrightarrow> A \<in> X \<Longrightarrow> A \<in> \<Union>C"
+lemma UnionI [intro]: "X \<in> C \<Longrightarrow> A \<in> X \<Longrightarrow> A \<in> \<Union>C"
   \<comment> \<open>The order of the premises presupposes that @{term C} is rigid;
     @{term A} may be flexible.\<close>
   by auto
 
-lemma UnionE [elim!]:
-  "A \<in> \<Union>C \<Longrightarrow> (\<And>X. A \<in> X \<Longrightarrow> X \<in> C \<Longrightarrow> R) \<Longrightarrow> R"
+lemma UnionE [elim!]: "A \<in> \<Union>C \<Longrightarrow> (\<And>X. A \<in> X \<Longrightarrow> X \<in> C \<Longrightarrow> R) \<Longrightarrow> R"
   by auto
 
 lemma Union_upper: "B \<in> A \<Longrightarrow> B \<subseteq> \<Union>A"
@@ -1131,6 +1060,7 @@
 lemma Union_subsetI: "(\<And>x. x \<in> A \<Longrightarrow> \<exists>y. y \<in> B \<and> x \<subseteq> y) \<Longrightarrow> \<Union>A \<subseteq> \<Union>B"
   by blast
 
+
 subsubsection \<open>Unions of families\<close>
 
 abbreviation UNION :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set"
@@ -1169,16 +1099,13 @@
   [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax UNION} @{syntax_const "_UNION"}]
 \<close> \<comment> \<open>to avoid eta-contraction of body\<close>
 
-lemma UNION_eq:
-  "(\<Union>x\<in>A. B x) = {y. \<exists>x\<in>A. y \<in> B x}"
+lemma UNION_eq: "(\<Union>x\<in>A. B x) = {y. \<exists>x\<in>A. y \<in> B x}"
   by (auto intro!: SUP_eqI)
 
-lemma bind_UNION [code]:
-  "Set.bind A f = UNION A f"
+lemma bind_UNION [code]: "Set.bind A f = UNION A f"
   by (simp add: bind_def UNION_eq)
 
-lemma member_bind [simp]:
-  "x \<in> Set.bind P f \<longleftrightarrow> x \<in> UNION P f "
+lemma member_bind [simp]: "x \<in> Set.bind P f \<longleftrightarrow> x \<in> UNION P f "
   by (simp add: bind_UNION)
 
 lemma Union_SetCompr_eq: "\<Union>{f x| x. P x} = {a. \<exists>x. P x \<and> a \<in> f x}"
@@ -1281,6 +1208,7 @@
 lemma inj_on_image: "inj_on f (\<Union>A) \<Longrightarrow> inj_on (op ` f) A"
   unfolding inj_on_def by blast
 
+
 subsubsection \<open>Distributive laws\<close>
 
 lemma Int_Union: "A \<inter> \<Union>B = (\<Union>C\<in>B. A \<inter> C)"
@@ -1298,10 +1226,10 @@
 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)"
   by (rule sym) (rule SUP_sup_distrib)
 
-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>
+lemma Int_Inter_image: "(\<Inter>x\<in>C. A x \<inter> B x) = \<Inter>(A ` C) \<inter> \<Inter>(B ` C)"  (* FIXME drop *)
   by (simp add: INT_Int_distrib)
 
-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>
+lemma Un_Union_image: "(\<Union>x\<in>C. A x \<union> B x) = \<Union>(A ` C) \<union> \<Union>(B ` C)"  (* FIXME drop *)
   \<comment> \<open>Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5:\<close>
   \<comment> \<open>Union of a family of unions\<close>
   by (simp add: UN_Un_distrib)
@@ -1323,86 +1251,82 @@
   by (fact Sup_inf_eq_bot_iff)
 
 lemma SUP_UNION: "(SUP x:(UN y:A. g y). f x) = (SUP y:A. SUP x:g y. f x :: _ :: complete_lattice)"
-by(rule order_antisym)(blast intro: SUP_least SUP_upper2)+
+  by (rule order_antisym) (blast intro: SUP_least SUP_upper2)+
+
 
 subsection \<open>Injections and bijections\<close>
 
-lemma inj_on_Inter:
-  "S \<noteq> {} \<Longrightarrow> (\<And>A. A \<in> S \<Longrightarrow> inj_on f A) \<Longrightarrow> inj_on f (\<Inter>S)"
+lemma inj_on_Inter: "S \<noteq> {} \<Longrightarrow> (\<And>A. A \<in> S \<Longrightarrow> inj_on f A) \<Longrightarrow> inj_on f (\<Inter>S)"
   unfolding inj_on_def by blast
 
-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)"
+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)"
   unfolding inj_on_def by safe simp
 
 lemma inj_on_UNION_chain:
-  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
-         INJ: "\<And> i. i \<in> I \<Longrightarrow> inj_on f (A i)"
+  assumes chain: "\<And>i j. i \<in> I \<Longrightarrow> j \<in> I \<Longrightarrow> A i \<le> A j \<or> A j \<le> A i"
+    and inj: "\<And>i. i \<in> I \<Longrightarrow> inj_on f (A i)"
   shows "inj_on f (\<Union>i \<in> I. A i)"
 proof -
-  {
-    fix i j x y
-    assume *: "i \<in> I" "j \<in> I" and **: "x \<in> A i" "y \<in> A j"
-      and ***: "f x = f y"
-    have "x = y"
-    proof -
-      {
-        assume "A i \<le> A j"
-        with ** have "x \<in> A j" by auto
-        with INJ * ** *** have ?thesis
-        by(auto simp add: inj_on_def)
-      }
-      moreover
-      {
-        assume "A j \<le> A i"
-        with ** have "y \<in> A i" by auto
-        with INJ * ** *** have ?thesis
-        by(auto simp add: inj_on_def)
-      }
-      ultimately show ?thesis using CH * by blast
-    qed
-  }
-  then show ?thesis by (unfold inj_on_def UNION_eq) auto
+  have "x = y"
+    if *: "i \<in> I" "j \<in> I"
+    and **: "x \<in> A i" "y \<in> A j"
+    and ***: "f x = f y"
+    for i j x y
+    using chain [OF *]
+  proof
+    assume "A i \<le> A j"
+    with ** have "x \<in> A j" by auto
+    with inj * ** *** show ?thesis
+      by (auto simp add: inj_on_def)
+  next
+    assume "A j \<le> A i"
+    with ** have "y \<in> A i" by auto
+    with inj * ** *** show ?thesis
+      by (auto simp add: inj_on_def)
+  qed
+  then show ?thesis
+    by (unfold inj_on_def UNION_eq) auto
 qed
 
 lemma bij_betw_UNION_chain:
-  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
-         BIJ: "\<And> i. i \<in> I \<Longrightarrow> bij_betw f (A i) (A' i)"
+  assumes chain: "\<And>i j. i \<in> I \<Longrightarrow> j \<in> I \<Longrightarrow> A i \<le> A j \<or> A j \<le> A i"
+    and bij: "\<And>i. i \<in> I \<Longrightarrow> bij_betw f (A i) (A' i)"
   shows "bij_betw f (\<Union>i \<in> I. A i) (\<Union>i \<in> I. A' i)"
-proof (unfold bij_betw_def, auto)
-  have "\<And> i. i \<in> I \<Longrightarrow> inj_on f (A i)"
-  using BIJ bij_betw_def[of f] by auto
-  thus "inj_on f (\<Union>i \<in> I. A i)"
-  using CH inj_on_UNION_chain[of I A f] by auto
+  unfolding bij_betw_def
+proof auto  (* slow *)
+  have "\<And>i. i \<in> I \<Longrightarrow> inj_on f (A i)"
+    using bij bij_betw_def[of f] by auto
+  then show "inj_on f (\<Union>i \<in> I. A i)"
+    using chain inj_on_UNION_chain[of I A f] by auto
 next
   fix i x
   assume *: "i \<in> I" "x \<in> A i"
-  hence "f x \<in> A' i" using BIJ bij_betw_def[of f] by auto
-  thus "\<exists>j \<in> I. f x \<in> A' j" using * by blast
+  then have "f x \<in> A' i"
+    using bij bij_betw_def[of f] by auto
+  with * show "\<exists>j \<in> I. f x \<in> A' j" by blast
 next
   fix i x'
   assume *: "i \<in> I" "x' \<in> A' i"
-  hence "\<exists>x \<in> A i. x' = f x" using BIJ bij_betw_def[of f] by blast
-  then have "\<exists>j \<in> I. \<exists>x \<in> A j. x' = f x"
-    using * by blast
-  then show "x' \<in> f ` (\<Union>x\<in>I. A x)" by blast
+  then have "\<exists>x \<in> A i. x' = f x"
+    using bij bij_betw_def[of f] by blast
+  with * have "\<exists>j \<in> I. \<exists>x \<in> A j. x' = f x"
+    by blast
+  then show "x' \<in> f ` (\<Union>x\<in>I. A x)"
+    by blast
 qed
 
 (*injectivity's required.  Left-to-right inclusion holds even if A is empty*)
-lemma image_INT:
-   "[| inj_on f C;  ALL x:A. B x <= C;  j:A |]
-    ==> f ` (INTER A B) = (INT x:A. f ` B x)"
-  by (simp add: inj_on_def, auto) blast
+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)"
+  by (auto simp add: inj_on_def) blast
 
-lemma bij_image_INT: "bij f ==> f ` (INTER A B) = (INT x:A. f ` B x)"
-  apply (simp add: bij_def)
-  apply (simp add: inj_on_def surj_def)
+lemma bij_image_INT: "bij f \<Longrightarrow> f ` (INTER A B) = (INT x:A. f ` B x)"
+  apply (simp only: bij_def)
+  apply (simp only: inj_on_def surj_def)
   apply auto
   apply blast
   done
 
-lemma UNION_fun_upd:
-  "UNION J (A(i := B)) = UNION (J - {i}) A \<union> (if i \<in> J then B else {})"
+lemma UNION_fun_upd: "UNION J (A(i := B)) = UNION (J - {i}) A \<union> (if i \<in> J then B else {})"
   by (auto simp add: set_eq_iff)
 
 lemma bij_betw_Pow:
@@ -1436,8 +1360,7 @@
 
 subsubsection \<open>Miniscoping and maxiscoping\<close>
 
-text \<open>\medskip Miniscoping: pushing in quantifiers and big Unions
-           and Intersections.\<close>
+text \<open>\<^medskip> Miniscoping: pushing in quantifiers and big Unions and Intersections.\<close>
 
 lemma UN_simps [simp]:
   "\<And>a B C. (\<Union>x\<in>C. insert a (B x)) = (if C={} then {} else insert a (\<Union>x\<in>C. B x))"
@@ -1473,7 +1396,7 @@
   by auto
 
 
-text \<open>\medskip Maxiscoping: pulling out big Unions and Intersections.\<close>
+text \<open>\<^medskip> Maxiscoping: pulling out big Unions and Intersections.\<close>
 
 lemma UN_extend_simps:
   "\<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)))"
@@ -1513,4 +1436,3 @@
   \<comment> \<open>Each of these has ALREADY been added \<open>[simp]\<close> above.\<close>
 
 end
-
diff -r 4ea48cbc54c1 -r b9bd9e61fd63 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Mon Aug 01 13:51:17 2016 +0200
+++ b/src/HOL/Fun.thy	Mon Aug 01 22:11:29 2016 +0200
@@ -7,8 +7,8 @@
 section \<open>Notions about functions\<close>
 
 theory Fun
-imports Set
-keywords "functor" :: thy_goal
+  imports Set
+  keywords "functor" :: thy_goal
 begin
 
 lemma apply_inverse: "f x = u \<Longrightarrow> (\<And>x. P x \<Longrightarrow> g (f x) = x) \<Longrightarrow> P x \<Longrightarrow> x = g u"
@@ -63,12 +63,10 @@
 lemma comp_id [simp]: "f \<circ> id = f"
   by (simp add: fun_eq_iff)
 
-lemma comp_eq_dest:
-  "a \<circ> b = c \<circ> d \<Longrightarrow> a (b v) = c (d v)"
+lemma comp_eq_dest: "a \<circ> b = c \<circ> d \<Longrightarrow> a (b v) = c (d v)"
   by (simp add: fun_eq_iff)
 
-lemma comp_eq_elim:
-  "a \<circ> b = c \<circ> d \<Longrightarrow> ((\<And>v. a (b v) = c (d v)) \<Longrightarrow> R) \<Longrightarrow> R"
+lemma comp_eq_elim: "a \<circ> b = c \<circ> d \<Longrightarrow> ((\<And>v. a (b v) = c (d v)) \<Longrightarrow> R) \<Longrightarrow> R"
   by (simp add: fun_eq_iff)
 
 lemma comp_eq_dest_lhs: "a \<circ> b = c \<Longrightarrow> a (b v) = c v"
@@ -104,7 +102,7 @@
 
 subsection \<open>The Forward Composition Operator \<open>fcomp\<close>\<close>
 
-definition fcomp :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'c" (infixl "\<circ>>" 60)
+definition fcomp :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'c"  (infixl "\<circ>>" 60)
   where "f \<circ>> g = (\<lambda>x. g (f x))"
 
 lemma fcomp_apply [simp]:  "(f \<circ>> g) x = g (f x)"
@@ -145,8 +143,10 @@
 definition bij_betw :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> bool"  \<comment> \<open>bijective\<close>
   where "bij_betw f A B \<longleftrightarrow> inj_on f A \<and> f ` A = B"
 
-text \<open>A common special case: functions injective, surjective or bijective over
-  the entire domain type.\<close>
+text \<open>
+  A common special case: functions injective, surjective or bijective over
+  the entire domain type.
+\<close>
 
 abbreviation "inj f \<equiv> inj_on f UNIV"
 
@@ -212,7 +212,7 @@
 
 lemma inj_on_subset:
   assumes "inj_on f A"
-  assumes "B \<subseteq> A"
+    and "B \<subseteq> A"
   shows "inj_on f B"
 proof (rule inj_onI)
   fix a b
@@ -296,7 +296,7 @@
   by (simp add: surj_def)
 
 lemma surjE: "surj f \<Longrightarrow> (\<And>x. y = f x \<Longrightarrow> C) \<Longrightarrow> C"
-  by (simp add: surj_def, blast)
+  by (simp add: surj_def) blast
 
 lemma comp_surj: "surj f \<Longrightarrow> surj g \<Longrightarrow> surj (g \<circ> f)"
   by (simp add: image_comp [symmetric])
@@ -354,18 +354,19 @@
     using img
   proof (auto simp add: bij_betw_def)
     assume "inj_on (f' \<circ> f) A"
-    then show "inj_on f A" using inj_on_imageI2 by blast
+    then show "inj_on f A"
+      using inj_on_imageI2 by blast
   next
     fix a'
     assume **: "a' \<in> A'"
-    then have "f' a' \<in> A''" using bij unfolding bij_betw_def by auto
-    then obtain a where 1: "a \<in> A \<and> f'(f a) = f' a'"
-      using * unfolding bij_betw_def by force
-    then have "f a \<in> A'" using img by auto
-    then have "f a = a'"
-      using bij ** 1 unfolding bij_betw_def inj_on_def by auto
-    then show "a' \<in> f ` A"
-      using 1 by auto
+    with bij have "f' a' \<in> A''"
+      unfolding bij_betw_def by auto
+    with * obtain a where 1: "a \<in> A \<and> f' (f a) = f' a'"
+      unfolding bij_betw_def by force
+    with img have "f a \<in> A'" by auto
+    with bij ** 1 have "f a = a'"
+      unfolding bij_betw_def inj_on_def by auto
+    with 1 show "a' \<in> f ` A" by auto
   qed
 qed
 
@@ -379,9 +380,10 @@
   let ?g = "\<lambda>b. The (?P b)"
   have g: "?g b = a" if P: "?P b a" for a b
   proof -
-    from that have ex1: "\<exists>a. ?P b a" using s by blast
+    from that s have ex1: "\<exists>a. ?P b a" by blast
     then have uex1: "\<exists>!a. ?P b a" by (blast dest:inj_onD[OF i])
-    then show ?thesis using the1_equality[OF uex1, OF P] P by simp
+    then show ?thesis
+      using the1_equality[OF uex1, OF P] P by simp
   qed
   have "inj_on ?g B"
   proof (rule inj_onI)
@@ -396,15 +398,16 @@
     fix b
     assume "b \<in> B"
     with s obtain a where P: "?P b a" by blast
-    then show "?g b \<in> A" using g[OF P] by auto
+    with g[OF P] show "?g b \<in> A" by auto
   next
     fix a
     assume "a \<in> A"
-    then obtain b where P: "?P b a" using s by blast
-    then have "b \<in> B" using s by blast
+    with s obtain b where P: "?P b a" by blast
+    with s have "b \<in> B" by blast
     with g[OF P] show "\<exists>b\<in>B. a = ?g b" by blast
   qed
-  ultimately show ?thesis by (auto simp: bij_betw_def)
+  ultimately show ?thesis
+    by (auto simp: bij_betw_def)
 qed
 
 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'"
@@ -500,9 +503,7 @@
 
 lemma inj_vimage_singleton: "inj f \<Longrightarrow> f -` {a} \<subseteq> {THE x. f x = a}"
   \<comment> \<open>The inverse image of a singleton under an injective function is included in a singleton.\<close>
-  apply (auto simp add: inj_on_def)
-  apply (blast intro: the_equality [symmetric])
-  done
+  by (simp add: inj_on_def) (blast intro: the_equality [symmetric])
 
 lemma inj_on_vimage_singleton: "inj_on f A \<Longrightarrow> f -` {a} \<inter> A \<subseteq> {THE x. x \<in> A \<and> f x = a}"
   by (auto simp add: inj_on_def intro: the_equality [symmetric])
@@ -516,21 +517,21 @@
 lemma bij_betw_byWitness:
   assumes left: "\<forall>a \<in> A. f' (f a) = a"
     and right: "\<forall>a' \<in> A'. f (f' a') = a'"
-    and "f ` A \<le> A'"
-    and img2: "f' ` A' \<le> A"
+    and "f ` A \<subseteq> A'"
+    and img2: "f' ` A' \<subseteq> A"
   shows "bij_betw f A A'"
   using assms
   unfolding bij_betw_def inj_on_def
 proof safe
   fix a b
-  assume *: "a \<in> A" "b \<in> A" and **: "f a = f b"
-  have "a = f' (f a) \<and> b = f'(f b)" using * left by simp
-  with ** show "a = b" by simp
+  assume "a \<in> A" "b \<in> A"
+  with left have "a = f' (f a) \<and> b = f' (f b)" by simp
+  moreover assume "f a = f b"
+  ultimately show "a = b" by simp
 next
   fix a' assume *: "a' \<in> A'"
-  then have "f' a' \<in> A" using img2 by blast
-  moreover
-  have "a' = f (f' a')" using * right by simp
+  with img2 have "f' a' \<in> A" by blast
+  moreover from * right have "a' = f (f' a')" by simp
   ultimately show "a' \<in> f ` A" by blast
 qed
 
@@ -565,7 +566,8 @@
     moreover
     have False if "f a = f b"
     proof -
-      have "a = b" using * ** that unfolding bij_betw_def inj_on_def by blast
+      have "a = b"
+        using * ** that unfolding bij_betw_def inj_on_def by blast
       with \<open>b \<notin> A\<close> ** show ?thesis by blast
     qed
     ultimately show "f a \<in> A'" by blast
@@ -611,9 +613,9 @@
 lemma fun_upd_idem_iff: "f(x:=y) = f \<longleftrightarrow> f x = y"
   unfolding fun_upd_def
   apply safe
-  apply (erule subst)
-  apply (rule_tac [2] ext)
-  apply auto
+   apply (erule subst)
+   apply (rule_tac [2] ext)
+   apply auto
   done
 
 lemma fun_upd_idem: "f x = y \<Longrightarrow> f(x := y) = f"
@@ -667,10 +669,10 @@
   by (simp add:override_on_def)
 
 lemma override_on_insert: "override_on f g (insert x X) = (override_on f g X)(x:=g x)"
-unfolding override_on_def by (simp add: fun_eq_iff)
+  unfolding override_on_def by (simp add: fun_eq_iff)
 
 lemma override_on_insert': "override_on f g (insert x X) = (override_on (f(x:=g x)) g X)"
-unfolding override_on_def by (simp add: fun_eq_iff)
+  unfolding override_on_def by (simp add: fun_eq_iff)
 
 
 subsection \<open>\<open>swap\<close>\<close>
@@ -691,7 +693,7 @@
   by (simp add: fun_upd_def swap_def fun_eq_iff)
 
 lemma swap_nilpotent [simp]: "swap a b (swap a b f) = f"
-  by (rule ext, simp add: fun_upd_def swap_def)
+  by (rule ext) (simp add: fun_upd_def swap_def)
 
 lemma swap_comp_involutory [simp]: "swap a b \<circ> swap a b = id"
   by (rule ext) simp
@@ -757,14 +759,14 @@
 lemma f_the_inv_into_f: "inj_on f A \<Longrightarrow> y \<in> f ` A  \<Longrightarrow> f (the_inv_into A f y) = y"
   apply (simp add: the_inv_into_def)
   apply (rule the1I2)
-   apply(blast dest: inj_onD)
+   apply (blast dest: inj_onD)
   apply blast
   done
 
 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"
   apply (simp add: the_inv_into_def)
   apply (rule the1I2)
-   apply(blast dest: inj_onD)
+   apply (blast dest: inj_onD)
   apply blast
   done
 
diff -r 4ea48cbc54c1 -r b9bd9e61fd63 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Mon Aug 01 13:51:17 2016 +0200
+++ b/src/HOL/HOL.thy	Mon Aug 01 22:11:29 2016 +0200
@@ -218,20 +218,20 @@
   by (rule trans [OF _ sym])
 
 lemma meta_eq_to_obj_eq:
-  assumes meq: "A \<equiv> B"
+  assumes "A \<equiv> B"
   shows "A = B"
-  by (unfold meq) (rule refl)
+  unfolding assms by (rule refl)
 
 text \<open>Useful with \<open>erule\<close> for proving equalities from known equalities.\<close>
      (* a = b
         |   |
         c = d   *)
 lemma box_equals: "\<lbrakk>a = b; a = c; b = d\<rbrakk> \<Longrightarrow> c = d"
-apply (rule trans)
-apply (rule trans)
-apply (rule sym)
-apply assumption+
-done
+  apply (rule trans)
+   apply (rule trans)
+    apply (rule sym)
+    apply assumption+
+  done
 
 text \<open>For calculational reasoning:\<close>
 
@@ -246,25 +246,25 @@
 
 text \<open>Similar to \<open>AP_THM\<close> in Gordon's HOL.\<close>
 lemma fun_cong: "(f :: 'a \<Rightarrow> 'b) = g \<Longrightarrow> f x = g x"
-apply (erule subst)
-apply (rule refl)
-done
+  apply (erule subst)
+  apply (rule refl)
+  done
 
 text \<open>Similar to \<open>AP_TERM\<close> in Gordon's HOL and FOL's \<open>subst_context\<close>.\<close>
 lemma arg_cong: "x = y \<Longrightarrow> f x = f y"
-apply (erule subst)
-apply (rule refl)
-done
+  apply (erule subst)
+  apply (rule refl)
+  done
 
 lemma arg_cong2: "\<lbrakk>a = b; c = d\<rbrakk> \<Longrightarrow> f a c = f b d"
-apply (erule ssubst)+
-apply (rule refl)
-done
+  apply (erule ssubst)+
+  apply (rule refl)
+  done
 
 lemma cong: "\<lbrakk>f = g; (x::'a) = y\<rbrakk> \<Longrightarrow> f x = g y"
-apply (erule subst)+
-apply (rule refl)
-done
+  apply (erule subst)+
+  apply (rule refl)
+  done
 
 ML \<open>fun cong_tac ctxt = Cong_Tac.cong_tac ctxt @{thm cong}\<close>
 
@@ -295,7 +295,7 @@
 
 subsubsection \<open>True\<close>
 
-lemma TrueI: "True"
+lemma TrueI: True
   unfolding True_def by (rule refl)
 
 lemma eqTrueI: "P \<Longrightarrow> P = True"
@@ -307,14 +307,16 @@
 
 subsubsection \<open>Universal quantifier\<close>
 
-lemma allI: assumes "\<And>x::'a. P x" shows "\<forall>x. P x"
+lemma allI:
+  assumes "\<And>x::'a. P x"
+  shows "\<forall>x. P x"
   unfolding All_def by (iprover intro: ext eqTrueI assms)
 
 lemma spec: "\<forall>x::'a. P x \<Longrightarrow> P x"
-apply (unfold All_def)
-apply (rule eqTrueE)
-apply (erule fun_cong)
-done
+  apply (unfold All_def)
+  apply (rule eqTrueE)
+  apply (erule fun_cong)
+  done
 
 lemma allE:
   assumes major: "\<forall>x. P x"
@@ -380,24 +382,24 @@
 lemma impE:
   assumes "P \<longrightarrow> Q" P "Q \<Longrightarrow> R"
   shows R
-by (iprover intro: assms mp)
+  by (iprover intro: assms mp)
 
-(* Reduces Q to P \<longrightarrow> Q, allowing substitution in P. *)
+text \<open>Reduces \<open>Q\<close> to \<open>P \<longrightarrow> Q\<close>, allowing substitution in \<open>P\<close>.\<close>
 lemma rev_mp: "\<lbrakk>P; P \<longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
-by (iprover intro: mp)
+  by (iprover intro: mp)
 
 lemma contrapos_nn:
   assumes major: "\<not> Q"
-      and minor: "P \<Longrightarrow> Q"
+    and minor: "P \<Longrightarrow> Q"
   shows "\<not> P"
-by (iprover intro: notI minor major [THEN notE])
+  by (iprover intro: notI minor major [THEN notE])
 
-(*not used at all, but we already have the other 3 combinations *)
+text \<open>Not used at all, but we already have the other 3 combinations.\<close>
 lemma contrapos_pn:
   assumes major: "Q"
-      and minor: "P \<Longrightarrow> \<not> Q"
+    and minor: "P \<Longrightarrow> \<not> Q"
   shows "\<not> P"
-by (iprover intro: notI minor major notE)
+  by (iprover intro: notI minor major notE)
 
 lemma not_sym: "t \<noteq> s \<Longrightarrow> s \<noteq> t"
   by (erule contrapos_nn) (erule sym)
@@ -409,69 +411,56 @@
 subsubsection \<open>Existential quantifier\<close>
 
 lemma exI: "P x \<Longrightarrow> \<exists>x::'a. P x"
-apply (unfold Ex_def)
-apply (iprover intro: allI allE impI mp)
-done
+  unfolding Ex_def by (iprover intro: allI allE impI mp)
 
 lemma exE:
   assumes major: "\<exists>x::'a. P x"
-      and minor: "\<And>x. P x \<Longrightarrow> Q"
+    and minor: "\<And>x. P x \<Longrightarrow> Q"
   shows "Q"
-apply (rule major [unfolded Ex_def, THEN spec, THEN mp])
-apply (iprover intro: impI [THEN allI] minor)
-done
+  by (rule major [unfolded Ex_def, THEN spec, THEN mp]) (iprover intro: impI [THEN allI] minor)
 
 
 subsubsection \<open>Conjunction\<close>
 
 lemma conjI: "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> P \<and> Q"
-apply (unfold and_def)
-apply (iprover intro: impI [THEN allI] mp)
-done
+  unfolding and_def by (iprover intro: impI [THEN allI] mp)
 
 lemma conjunct1: "\<lbrakk>P \<and> Q\<rbrakk> \<Longrightarrow> P"
-apply (unfold and_def)
-apply (iprover intro: impI dest: spec mp)
-done
+  unfolding and_def by (iprover intro: impI dest: spec mp)
 
 lemma conjunct2: "\<lbrakk>P \<and> Q\<rbrakk> \<Longrightarrow> Q"
-apply (unfold and_def)
-apply (iprover intro: impI dest: spec mp)
-done
+  unfolding and_def by (iprover intro: impI dest: spec mp)
 
 lemma conjE:
   assumes major: "P \<and> Q"
-      and minor: "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> R"
+    and minor: "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> R"
   shows R
-apply (rule minor)
-apply (rule major [THEN conjunct1])
-apply (rule major [THEN conjunct2])
-done
+  apply (rule minor)
+   apply (rule major [THEN conjunct1])
+  apply (rule major [THEN conjunct2])
+  done
 
 lemma context_conjI:
-  assumes P "P \<Longrightarrow> Q" shows "P \<and> Q"
-by (iprover intro: conjI assms)
+  assumes P "P \<Longrightarrow> Q"
+  shows "P \<and> Q"
+  by (iprover intro: conjI assms)
 
 
 subsubsection \<open>Disjunction\<close>
 
 lemma disjI1: "P \<Longrightarrow> P \<or> Q"
-apply (unfold or_def)
-apply (iprover intro: allI impI mp)
-done
+  unfolding or_def by (iprover intro: allI impI mp)
 
 lemma disjI2: "Q \<Longrightarrow> P \<or> Q"
-apply (unfold or_def)
-apply (iprover intro: allI impI mp)
-done
+  unfolding or_def by (iprover intro: allI impI mp)
 
 lemma disjE:
   assumes major: "P \<or> Q"
-      and minorP: "P \<Longrightarrow> R"
-      and minorQ: "Q \<Longrightarrow> R"
+    and minorP: "P \<Longrightarrow> R"
+    and minorQ: "Q \<Longrightarrow> R"
   shows R
-by (iprover intro: minorP minorQ impI
-                 major [unfolded or_def, THEN spec, THEN mp, THEN mp])
+  by (iprover intro: minorP minorQ impI
+      major [unfolded or_def, THEN spec, THEN mp, THEN mp])
 
 
 subsubsection \<open>Classical logic\<close>
@@ -479,37 +468,37 @@
 lemma classical:
   assumes prem: "\<not> P \<Longrightarrow> P"
   shows P
-apply (rule True_or_False [THEN disjE, THEN eqTrueE])
-apply assumption
-apply (rule notI [THEN prem, THEN eqTrueI])
-apply (erule subst)
-apply assumption
-done
+  apply (rule True_or_False [THEN disjE, THEN eqTrueE])
+   apply assumption
+  apply (rule notI [THEN prem, THEN eqTrueI])
+  apply (erule subst)
+  apply assumption
+  done
 
 lemmas ccontr = FalseE [THEN classical]
 
-(*notE with premises exchanged; it discharges \<not> R so that it can be used to
-  make elimination rules*)
+text \<open>\<open>notE\<close> with premises exchanged; it discharges \<open>\<not> R\<close> so that it can be used to
+  make elimination rules.\<close>
 lemma rev_notE:
   assumes premp: P
-      and premnot: "\<not> R \<Longrightarrow> \<not> P"
+    and premnot: "\<not> R \<Longrightarrow> \<not> P"
   shows R
-apply (rule ccontr)
-apply (erule notE [OF premnot premp])
-done
+  apply (rule ccontr)
+  apply (erule notE [OF premnot premp])
+  done
 
-(*Double negation law*)
+text \<open>Double negation law.\<close>
 lemma notnotD: "\<not>\<not> P \<Longrightarrow> P"
-apply (rule classical)
-apply (erule notE)
-apply assumption
-done
+  apply (rule classical)
+  apply (erule notE)
+  apply assumption
+  done
 
 lemma contrapos_pp:
   assumes p1: Q
-      and p2: "\<not> P \<Longrightarrow> \<not> Q"
+    and p2: "\<not> P \<Longrightarrow> \<not> Q"
   shows P
-by (iprover intro: classical p1 p2 notE)
+  by (iprover intro: classical p1 p2 notE)
 
 
 subsubsection \<open>Unique existence\<close>
@@ -517,90 +506,87 @@
 lemma ex1I:
   assumes "P a" "\<And>x. P x \<Longrightarrow> x = a"
   shows "\<exists>!x. P x"
-by (unfold Ex1_def, iprover intro: assms exI conjI allI impI)
+  unfolding Ex1_def by (iprover intro: assms exI conjI allI impI)
 
-text\<open>Sometimes easier to use: the premises have no shared variables.  Safe!\<close>
+text \<open>Sometimes easier to use: the premises have no shared variables. Safe!\<close>
 lemma ex_ex1I:
   assumes ex_prem: "\<exists>x. P x"
-      and eq: "\<And>x y. \<lbrakk>P x; P y\<rbrakk> \<Longrightarrow> x = y"
+    and eq: "\<And>x y. \<lbrakk>P x; P y\<rbrakk> \<Longrightarrow> x = y"
   shows "\<exists>!x. P x"
-by (iprover intro: ex_prem [THEN exE] ex1I eq)
+  by (iprover intro: ex_prem [THEN exE] ex1I eq)
 
 lemma ex1E:
   assumes major: "\<exists>!x. P x"
-      and minor: "\<And>x. \<lbrakk>P x; \<forall>y. P y \<longrightarrow> y = x\<rbrakk> \<Longrightarrow> R"
+    and minor: "\<And>x. \<lbrakk>P x; \<forall>y. P y \<longrightarrow> y = x\<rbrakk> \<Longrightarrow> R"
   shows R
-apply (rule major [unfolded Ex1_def, THEN exE])
-apply (erule conjE)
-apply (iprover intro: minor)
-done
+  apply (rule major [unfolded Ex1_def, THEN exE])
+  apply (erule conjE)
+  apply (iprover intro: minor)
+  done
 
 lemma ex1_implies_ex: "\<exists>!x. P x \<Longrightarrow> \<exists>x. P x"
-apply (erule ex1E)
-apply (rule exI)
-apply assumption
-done
+  apply (erule ex1E)
+  apply (rule exI)
+  apply assumption
+  done
 
 
 subsubsection \<open>Classical intro rules for disjunction and existential quantifiers\<close>
 
 lemma disjCI:
-  assumes "\<not> Q \<Longrightarrow> P" shows "P \<or> Q"
-apply (rule classical)
-apply (iprover intro: assms disjI1 disjI2 notI elim: notE)
-done
+  assumes "\<not> Q \<Longrightarrow> P"
+  shows "P \<or> Q"
+  by (rule classical) (iprover intro: assms disjI1 disjI2 notI elim: notE)
 
 lemma excluded_middle: "\<not> P \<or> P"
-by (iprover intro: disjCI)
+  by (iprover intro: disjCI)
 
 text \<open>
   case distinction as a natural deduction rule.
-  Note that @{term "\<not> P"} is the second case, not the first
+  Note that \<open>\<not> P\<close> is the second case, not the first.
 \<close>
 lemma case_split [case_names True False]:
   assumes prem1: "P \<Longrightarrow> Q"
-      and prem2: "\<not> P \<Longrightarrow> Q"
+    and prem2: "\<not> P \<Longrightarrow> Q"
   shows Q
-apply (rule excluded_middle [THEN disjE])
-apply (erule prem2)
-apply (erule prem1)
-done
+  apply (rule excluded_middle [THEN disjE])
+   apply (erule prem2)
+  apply (erule prem1)
+  done
 
-(*Classical implies (\<longrightarrow>) elimination. *)
+text \<open>Classical implies (\<open>\<longrightarrow>\<close>) elimination.\<close>
 lemma impCE:
   assumes major: "P \<longrightarrow> Q"
-      and minor: "\<not> P \<Longrightarrow> R" "Q \<Longrightarrow> R"
+    and minor: "\<not> P \<Longrightarrow> R" "Q \<Longrightarrow> R"
   shows R
-apply (rule excluded_middle [of P, THEN disjE])
-apply (iprover intro: minor major [THEN mp])+
-done
+  apply (rule excluded_middle [of P, THEN disjE])
+   apply (iprover intro: minor major [THEN mp])+
+  done
 
-(*This version of \<longrightarrow> elimination works on Q before P.  It works best for
-  those cases in which P holds "almost everywhere".  Can't install as
-  default: would break old proofs.*)
+text \<open>
+  This version of \<open>\<longrightarrow>\<close> elimination works on \<open>Q\<close> before \<open>P\<close>.  It works best for
+  those cases in which \<open>P\<close> holds "almost everywhere".  Can't install as
+  default: would break old proofs.
+\<close>
 lemma impCE':
   assumes major: "P \<longrightarrow> Q"
-      and minor: "Q \<Longrightarrow> R" "\<not> P \<Longrightarrow> R"
+    and minor: "Q \<Longrightarrow> R" "\<not> P \<Longrightarrow> R"
   shows R
-apply (rule excluded_middle [of P, THEN disjE])
-apply (iprover intro: minor major [THEN mp])+
-done
+  apply (rule excluded_middle [of P, THEN disjE])
+   apply (iprover intro: minor major [THEN mp])+
+  done
 
-(*Classical <-> elimination. *)
+text \<open>Classical \<open>\<longleftrightarrow>\<close> elimination.\<close>
 lemma iffCE:
   assumes major: "P = Q"
-      and minor: "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> R" "\<lbrakk>\<not> P; \<not> Q\<rbrakk> \<Longrightarrow> R"
+    and minor: "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> R" "\<lbrakk>\<not> P; \<not> Q\<rbrakk> \<Longrightarrow> R"
   shows R
-apply (rule major [THEN iffE])
-apply (iprover intro: minor elim: impCE notE)
-done
+  by (rule major [THEN iffE]) (iprover intro: minor elim: impCE notE)
 
 lemma exCI:
   assumes "\<forall>x. \<not> P x \<Longrightarrow> P a"
   shows "\<exists>x. P x"
-apply (rule ccontr)
-apply (iprover intro: assms exI allI notI notE [of "\<exists>x. P x"])
-done
+  by (rule ccontr) (iprover intro: assms exI allI notI notE [of "\<exists>x. P x"])
 
 
 subsubsection \<open>Intuitionistic Reasoning\<close>
@@ -650,7 +636,7 @@
 subsubsection \<open>Atomizing meta-level connectives\<close>
 
 axiomatization where
-  eq_reflection: "x = y \<Longrightarrow> x \<equiv> y" (*admissible axiom*)
+  eq_reflection: "x = y \<Longrightarrow> x \<equiv> y"  \<comment> \<open>admissible axiom\<close>
 
 lemma atomize_all [atomize]: "(\<And>x. P x) \<equiv> Trueprop (\<forall>x. P x)"
 proof
@@ -731,9 +717,9 @@
 subsubsection \<open>Sledgehammer setup\<close>
 
 text \<open>
-Theorems blacklisted to Sledgehammer. These theorems typically produce clauses
-that are prolific (match too many equality or membership literals) and relate to
-seldom-used facts. Some duplicate other rules.
+  Theorems blacklisted to Sledgehammer. These theorems typically produce clauses
+  that are prolific (match too many equality or membership literals) and relate to
+  seldom-used facts. Some duplicate other rules.
 \<close>
 
 named_theorems no_atp "theorems that should be filtered out by Sledgehammer"
@@ -830,18 +816,18 @@
 lemmas [intro?] = ext
   and [elim?] = ex1_implies_ex
 
-(*Better then ex1E for classical reasoner: needs no quantifier duplication!*)
+text \<open>Better than \<open>ex1E\<close> for classical reasoner: needs no quantifier duplication!\<close>
 lemma alt_ex1E [elim!]:
   assumes major: "\<exists>!x. P x"
-      and prem: "\<And>x. \<lbrakk> P x; \<forall>y y'. P y \<and> P y' \<longrightarrow> y = y' \<rbrakk> \<Longrightarrow> R"
+    and prem: "\<And>x. \<lbrakk>P x; \<forall>y y'. P y \<and> P y' \<longrightarrow> y = y'\<rbrakk> \<Longrightarrow> R"
   shows R
-apply (rule ex1E [OF major])
-apply (rule prem)
-apply assumption
-apply (rule allI)+
-apply (tactic \<open>eresolve_tac @{context} [Classical.dup_elim @{context} @{thm allE}] 1\<close>)
-apply iprover
-done
+  apply (rule ex1E [OF major])
+  apply (rule prem)
+   apply assumption
+  apply (rule allI)+
+  apply (tactic \<open>eresolve_tac @{context} [Classical.dup_elim @{context} @{thm allE}] 1\<close>)
+  apply iprover
+  done
 
 ML \<open>
   structure Blast = Blast
@@ -862,27 +848,29 @@
 
 lemma the_equality [intro]:
   assumes "P a"
-      and "\<And>x. P x \<Longrightarrow> x = a"
+    and "\<And>x. P x \<Longrightarrow> x = a"
   shows "(THE x. P x) = a"
   by (blast intro: assms trans [OF arg_cong [where f=The] the_eq_trivial])
 
 lemma theI:
-  assumes "P a" and "\<And>x. P x \<Longrightarrow> x = a"
+  assumes "P a"
+    and "\<And>x. P x \<Longrightarrow> x = a"
   shows "P (THE x. P x)"
-by (iprover intro: assms the_equality [THEN ssubst])
+  by (iprover intro: assms the_equality [THEN ssubst])
 
 lemma theI': "\<exists>!x. P x \<Longrightarrow> P (THE x. P x)"
   by (blast intro: theI)
 
-(*Easier to apply than theI: only one occurrence of P*)
+text \<open>Easier to apply than \<open>theI\<close>: only one occurrence of \<open>P\<close>.\<close>
 lemma theI2:
   assumes "P a" "\<And>x. P x \<Longrightarrow> x = a" "\<And>x. P x \<Longrightarrow> Q x"
   shows "Q (THE x. P x)"
-by (iprover intro: assms theI)
+  by (iprover intro: assms theI)
 
-lemma the1I2: assumes "\<exists>!x. P x" "\<And>x. P x \<Longrightarrow> Q x" shows "Q (THE x. P x)"
-by(iprover intro:assms(2) theI2[where P=P and Q=Q] ex1E[OF assms(1)]
-           elim:allE impE)
+lemma the1I2:
+  assumes "\<exists>!x. P x" "\<And>x. P x \<Longrightarrow> Q x"
+  shows "Q (THE x. P x)"
+  by (iprover intro: assms(2) theI2[where P=P and Q=Q] ex1E[OF assms(1)] elim: allE impE)
 
 lemma the1_equality [elim?]: "\<lbrakk>\<exists>!x. P x; P a\<rbrakk> \<Longrightarrow> (THE x. P x) = a"
   by blast
@@ -929,136 +917,136 @@
     "\<And>P. (\<forall>x. t = x \<longrightarrow> P x) = P t"
   by (blast, blast, blast, blast, blast, iprover+)
 
-lemma disj_absorb: "(A \<or> A) = A"
+lemma disj_absorb: "A \<or> A \<longleftrightarrow> A"
   by blast
 
-lemma disj_left_absorb: "(A \<or> (A \<or> B)) = (A \<or> B)"
+lemma disj_left_absorb: "A \<or> (A \<or> B) \<longleftrightarrow> A \<or> B"
   by blast
 
-lemma conj_absorb: "(A \<and> A) = A"
+lemma conj_absorb: "A \<and> A \<longleftrightarrow> A"
   by blast
 
-lemma conj_left_absorb: "(A \<and> (A \<and> B)) = (A \<and> B)"
+lemma conj_left_absorb: "A \<and> (A \<and> B) \<longleftrightarrow> A \<and> B"
   by blast
 
 lemma eq_ac:
   shows eq_commute: "a = b \<longleftrightarrow> b = a"
     and iff_left_commute: "(P \<longleftrightarrow> (Q \<longleftrightarrow> R)) \<longleftrightarrow> (Q \<longleftrightarrow> (P \<longleftrightarrow> R))"
-    and iff_assoc: "((P \<longleftrightarrow> Q) \<longleftrightarrow> R) \<longleftrightarrow> (P \<longleftrightarrow> (Q \<longleftrightarrow> R))" by (iprover, blast+)
+    and iff_assoc: "((P \<longleftrightarrow> Q) \<longleftrightarrow> R) \<longleftrightarrow> (P \<longleftrightarrow> (Q \<longleftrightarrow> R))"
+  by (iprover, blast+)
+
 lemma neq_commute: "a \<noteq> b \<longleftrightarrow> b \<noteq> a" by iprover
 
 lemma conj_comms:
-  shows conj_commute: "(P \<and> Q) = (Q \<and> P)"
-    and conj_left_commute: "(P \<and> (Q \<and> R)) = (Q \<and> (P \<and> R))" by iprover+
-lemma conj_assoc: "((P \<and> Q) \<and> R) = (P \<and> (Q \<and> R))" by iprover
+  shows conj_commute: "P \<and> Q \<longleftrightarrow> Q \<and> P"
+    and conj_left_commute: "P \<and> (Q \<and> R) \<longleftrightarrow> Q \<and> (P \<and> R)" by iprover+
+lemma conj_assoc: "(P \<and> Q) \<and> R \<longleftrightarrow> P \<and> (Q \<and> R)" by iprover
 
 lemmas conj_ac = conj_commute conj_left_commute conj_assoc
 
 lemma disj_comms:
-  shows disj_commute: "(P \<or> Q) = (Q \<or> P)"
-    and disj_left_commute: "(P \<or> (Q \<or> R)) = (Q \<or> (P \<or> R))" by iprover+
-lemma disj_assoc: "((P \<or> Q) \<or> R) = (P \<or> (Q \<or> R))" by iprover
+  shows disj_commute: "P \<or> Q \<longleftrightarrow> Q \<or> P"
+    and disj_left_commute: "P \<or> (Q \<or> R) \<longleftrightarrow> Q \<or> (P \<or> R)" by iprover+
+lemma disj_assoc: "(P \<or> Q) \<or> R \<longleftrightarrow> P \<or> (Q \<or> R)" by iprover
 
 lemmas disj_ac = disj_commute disj_left_commute disj_assoc
 
-lemma conj_disj_distribL: "(P \<and> (Q \<or> R)) = (P \<and> Q \<or> P \<and> R)" by iprover
-lemma conj_disj_distribR: "((P \<or> Q) \<and> R) = (P \<and> R \<or> Q \<and> R)" by iprover
+lemma conj_disj_distribL: "P \<and> (Q \<or> R) \<longleftrightarrow> P \<and> Q \<or> P \<and> R" by iprover
+lemma conj_disj_distribR: "(P \<or> Q) \<and> R \<longleftrightarrow> P \<and> R \<or> Q \<and> R" by iprover
 
-lemma disj_conj_distribL: "(P \<or> (Q \<and> R)) = ((P \<or> Q) \<and> (P \<or> R))" by iprover
-lemma disj_conj_distribR: "((P \<and> Q) \<or> R) = ((P \<or> R) \<and> (Q \<or> R))" by iprover
+lemma disj_conj_distribL: "P \<or> (Q \<and> R) \<longleftrightarrow> (P \<or> Q) \<and> (P \<or> R)" by iprover
+lemma disj_conj_distribR: "(P \<and> Q) \<or> R \<longleftrightarrow> (P \<or> R) \<and> (Q \<or> R)" by iprover
 
 lemma imp_conjR: "(P \<longrightarrow> (Q \<and> R)) = ((P \<longrightarrow> Q) \<and> (P \<longrightarrow> R))" by iprover
 lemma imp_conjL: "((P \<and> Q) \<longrightarrow> R) = (P \<longrightarrow> (Q \<longrightarrow> R))" by iprover
 lemma imp_disjL: "((P \<or> Q) \<longrightarrow> R) = ((P \<longrightarrow> R) \<and> (Q \<longrightarrow> R))" by iprover
 
 text \<open>These two are specialized, but \<open>imp_disj_not1\<close> is useful in \<open>Auth/Yahalom\<close>.\<close>
-lemma imp_disj_not1: "(P \<longrightarrow> Q \<or> R) = (\<not> Q \<longrightarrow> P \<longrightarrow> R)" by blast
-lemma imp_disj_not2: "(P \<longrightarrow> Q \<or> R) = (\<not> R \<longrightarrow> P \<longrightarrow> Q)" by blast
+lemma imp_disj_not1: "(P \<longrightarrow> Q \<or> R) \<longleftrightarrow> (\<not> Q \<longrightarrow> P \<longrightarrow> R)" by blast
+lemma imp_disj_not2: "(P \<longrightarrow> Q \<or> R) \<longleftrightarrow> (\<not> R \<longrightarrow> P \<longrightarrow> Q)" by blast
 
-lemma imp_disj1: "((P \<longrightarrow> Q) \<or> R) = (P \<longrightarrow> Q \<or> R)" by blast
-lemma imp_disj2: "(Q \<or> (P \<longrightarrow> R)) = (P \<longrightarrow> Q \<or> R)" by blast
+lemma imp_disj1: "((P \<longrightarrow> Q) \<or> R) \<longleftrightarrow> (P \<longrightarrow> Q \<or> R)" by blast
+lemma imp_disj2: "(Q \<or> (P \<longrightarrow> R)) \<longleftrightarrow> (P \<longrightarrow> Q \<or> R)" by blast
 
-lemma imp_cong: "(P = P') \<Longrightarrow> (P' \<Longrightarrow> (Q = Q')) \<Longrightarrow> ((P \<longrightarrow> Q) = (P' \<longrightarrow> Q'))"
+lemma imp_cong: "(P = P') \<Longrightarrow> (P' \<Longrightarrow> (Q = Q')) \<Longrightarrow> ((P \<longrightarrow> Q) \<longleftrightarrow> (P' \<longrightarrow> Q'))"
   by iprover
 
-lemma de_Morgan_disj: "(\<not> (P \<or> Q)) = (\<not> P \<and> \<not> Q)" by iprover
-lemma de_Morgan_conj: "(\<not> (P \<and> Q)) = (\<not> P \<or> \<not> Q)" by blast
-lemma not_imp: "(\<not> (P \<longrightarrow> Q)) = (P \<and> \<not> Q)" by blast
-lemma not_iff: "(P \<noteq> Q) = (P = (\<not> Q))" by blast
-lemma disj_not1: "(\<not> P \<or> Q) = (P \<longrightarrow> Q)" by blast
-lemma disj_not2: "(P \<or> \<not> Q) = (Q \<longrightarrow> P)"  \<comment> \<open>changes orientation :-(\<close>
-  by blast
-lemma imp_conv_disj: "(P \<longrightarrow> Q) = ((\<not> P) \<or> Q)" by blast
+lemma de_Morgan_disj: "\<not> (P \<or> Q) \<longleftrightarrow> \<not> P \<and> \<not> Q" by iprover
+lemma de_Morgan_conj: "\<not> (P \<and> Q) \<longleftrightarrow> \<not> P \<or> \<not> Q" by blast
+lemma not_imp: "\<not> (P \<longrightarrow> Q) \<longleftrightarrow> P \<and> \<not> Q" by blast
+lemma not_iff: "P \<noteq> Q \<longleftrightarrow> (P \<longleftrightarrow> \<not> Q)" by blast
+lemma disj_not1: "\<not> P \<or> Q \<longleftrightarrow> (P \<longrightarrow> Q)" by blast
+lemma disj_not2: "P \<or> \<not> Q \<longleftrightarrow> (Q \<longrightarrow> P)" by blast  \<comment> \<open>changes orientation :-(\<close>
+lemma imp_conv_disj: "(P \<longrightarrow> Q) \<longleftrightarrow> (\<not> P) \<or> Q" by blast
 lemma disj_imp: "P \<or> Q \<longleftrightarrow> \<not> P \<longrightarrow> Q" by blast
 
-lemma iff_conv_conj_imp: "(P = Q) = ((P \<longrightarrow> Q) \<and> (Q \<longrightarrow> P))" by iprover
+lemma iff_conv_conj_imp: "(P \<longleftrightarrow> Q) \<longleftrightarrow> (P \<longrightarrow> Q) \<and> (Q \<longrightarrow> P)" by iprover
 
 
-lemma cases_simp: "((P \<longrightarrow> Q) \<and> (\<not> P \<longrightarrow> Q)) = Q"
+lemma cases_simp: "(P \<longrightarrow> Q) \<and> (\<not> P \<longrightarrow> Q) \<longleftrightarrow> Q"
   \<comment> \<open>Avoids duplication of subgoals after \<open>if_split\<close>, when the true and false\<close>
   \<comment> \<open>cases boil down to the same thing.\<close>
   by blast
 
-lemma not_all: "(\<not> (\<forall>x. P x)) = (\<exists>x. \<not> P x)" by blast
-lemma imp_all: "((\<forall>x. P x) \<longrightarrow> Q) = (\<exists>x. P x \<longrightarrow> Q)" by blast
-lemma not_ex: "(\<not> (\<exists>x. P x)) = (\<forall>x. \<not> P x)" by iprover
-lemma imp_ex: "((\<exists>x. P x) \<longrightarrow> Q) = (\<forall>x. P x \<longrightarrow> Q)" by iprover
-lemma all_not_ex: "(\<forall>x. P x) = (\<not> (\<exists>x. \<not> P x ))" by blast
+lemma not_all: "\<not> (\<forall>x. P x) \<longleftrightarrow> (\<exists>x. \<not> P x)" by blast
+lemma imp_all: "((\<forall>x. P x) \<longrightarrow> Q) \<longleftrightarrow> (\<exists>x. P x \<longrightarrow> Q)" by blast
+lemma not_ex: "\<not> (\<exists>x. P x) \<longleftrightarrow> (\<forall>x. \<not> P x)" by iprover
+lemma imp_ex: "((\<exists>x. P x) \<longrightarrow> Q) \<longleftrightarrow> (\<forall>x. P x \<longrightarrow> Q)" by iprover
+lemma all_not_ex: "(\<forall>x. P x) \<longleftrightarrow> \<not> (\<exists>x. \<not> P x)" by blast
 
 declare All_def [no_atp]
 
-lemma ex_disj_distrib: "(\<exists>x. P x \<or> Q x) = ((\<exists>x. P x) \<or> (\<exists>x. Q x))" by iprover
-lemma all_conj_distrib: "(\<forall>x. P x \<and> Q x) = ((\<forall>x. P x) \<and> (\<forall>x. Q x))" by iprover
+lemma ex_disj_distrib: "(\<exists>x. P x \<or> Q x) \<longleftrightarrow> (\<exists>x. P x) \<or> (\<exists>x. Q x)" by iprover
+lemma all_conj_distrib: "(\<forall>x. P x \<and> Q x) \<longleftrightarrow> (\<forall>x. P x) \<and> (\<forall>x. Q x)" by iprover
 
 text \<open>
-  \medskip The \<open>\<and>\<close> congruence rule: not included by default!
+  \<^medskip> The \<open>\<and>\<close> congruence rule: not included by default!
   May slow rewrite proofs down by as much as 50\%\<close>
 
-lemma conj_cong:
-    "(P = P') \<Longrightarrow> (P' \<Longrightarrow> (Q = Q')) \<Longrightarrow> ((P \<and> Q) = (P' \<and> Q'))"
+lemma conj_cong: "P = P' \<Longrightarrow> (P' \<Longrightarrow> Q = Q') \<Longrightarrow> (P \<and> Q) = (P' \<and> Q')"
   by iprover
 
-lemma rev_conj_cong:
-    "(Q = Q') \<Longrightarrow> (Q' \<Longrightarrow> (P = P')) \<Longrightarrow> ((P \<and> Q) = (P' \<and> Q'))"
+lemma rev_conj_cong: "Q = Q' \<Longrightarrow> (Q' \<Longrightarrow> P = P') \<Longrightarrow> (P \<and> Q) = (P' \<and> Q')"
   by iprover
 
 text \<open>The \<open>|\<close> congruence rule: not included by default!\<close>
 
-lemma disj_cong:
-    "(P = P') \<Longrightarrow> (\<not> P' \<Longrightarrow> (Q = Q')) \<Longrightarrow> ((P \<or> Q) = (P' \<or> Q'))"
+lemma disj_cong: "P = P' \<Longrightarrow> (\<not> P' \<Longrightarrow> Q = Q') \<Longrightarrow> (P \<or> Q) = (P' \<or> Q')"
   by blast
 
 
-text \<open>\medskip if-then-else rules\<close>
+text \<open>\<^medskip> if-then-else rules\<close>
 
 lemma if_True [code]: "(if True then x else y) = x"
-  by (unfold If_def) blast
+  unfolding If_def by blast
 
 lemma if_False [code]: "(if False then x else y) = y"
-  by (unfold If_def) blast
+  unfolding If_def by blast
 
 lemma if_P: "P \<Longrightarrow> (if P then x else y) = x"
-  by (unfold If_def) blast
+  unfolding If_def by blast
 
 lemma if_not_P: "\<not> P \<Longrightarrow> (if P then x else y) = y"
-  by (unfold If_def) blast
+  unfolding If_def by blast
 
 lemma if_split: "P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y))"
   apply (rule case_split [of Q])
    apply (simplesubst if_P)
-    prefer 3 apply (simplesubst if_not_P, blast+)
+    prefer 3
+    apply (simplesubst if_not_P)
+     apply blast+
   done
 
 lemma if_split_asm: "P (if Q then x else y) = (\<not> ((Q \<and> \<not> P x) \<or> (\<not> Q \<and> \<not> P y)))"
-by (simplesubst if_split, blast)
+  by (simplesubst if_split) blast
 
 lemmas if_splits [no_atp] = if_split if_split_asm
 
 lemma if_cancel: "(if c then x else x) = x"
-by (simplesubst if_split, blast)
+  by (simplesubst if_split) blast
 
 lemma if_eq_cancel: "(if x = y then y else x) = x"
-by (simplesubst if_split, blast)
+  by (simplesubst if_split) blast
 
 lemma if_bool_eq_conj: "(if P then Q else R) = ((P \<longrightarrow> Q) \<and> (\<not> P \<longrightarrow> R))"
   \<comment> \<open>This form is useful for expanding \<open>if\<close>s on the RIGHT of the \<open>\<Longrightarrow>\<close> symbol.\<close>
@@ -1068,10 +1056,10 @@
   \<comment> \<open>And this form is useful for expanding \<open>if\<close>s on the LEFT.\<close>
   by (simplesubst if_split) blast
 
-lemma Eq_TrueI: "P \<Longrightarrow> P \<equiv> True" by (unfold atomize_eq) iprover
-lemma Eq_FalseI: "\<not> P \<Longrightarrow> P \<equiv> False" by (unfold atomize_eq) iprover
+lemma Eq_TrueI: "P \<Longrightarrow> P \<equiv> True" unfolding atomize_eq by iprover
+lemma Eq_FalseI: "\<not> P \<Longrightarrow> P \<equiv> False" unfolding atomize_eq by iprover
 
-text \<open>\medskip let rules for simproc\<close>
+text \<open>\<^medskip> let rules for simproc\<close>
 
 lemma Let_folded: "f x \<equiv> g x \<Longrightarrow> Let x f \<equiv> Let x g"
   by (unfold Let_def)
@@ -1085,8 +1073,8 @@
   its premise.
 \<close>
 
-definition simp_implies :: "[prop, prop] \<Rightarrow> prop"  (infixr "=simp=>" 1) where
-  "simp_implies \<equiv> op \<Longrightarrow>"
+definition simp_implies :: "prop \<Rightarrow> prop \<Rightarrow> prop"  (infixr "=simp=>" 1)
+  where "simp_implies \<equiv> op \<Longrightarrow>"
 
 lemma simp_impliesI:
   assumes PQ: "(PROP P \<Longrightarrow> PROP Q)"
@@ -1098,8 +1086,8 @@
 
 lemma simp_impliesE:
   assumes PQ: "PROP P =simp=> PROP Q"
-  and P: "PROP P"
-  and QR: "PROP Q \<Longrightarrow> PROP R"
+    and P: "PROP P"
+    and QR: "PROP Q \<Longrightarrow> PROP R"
   shows "PROP R"
   apply (rule QR)
   apply (rule PQ [unfolded simp_implies_def])
@@ -1108,18 +1096,19 @@
 
 lemma simp_implies_cong:
   assumes PP' :"PROP P \<equiv> PROP P'"
-  and P'QQ': "PROP P' \<Longrightarrow> (PROP Q \<equiv> PROP Q')"
+    and P'QQ': "PROP P' \<Longrightarrow> (PROP Q \<equiv> PROP Q')"
   shows "(PROP P =simp=> PROP Q) \<equiv> (PROP P' =simp=> PROP Q')"
-proof (unfold simp_implies_def, rule equal_intr_rule)
+  unfolding simp_implies_def
+proof (rule equal_intr_rule)
   assume PQ: "PROP P \<Longrightarrow> PROP Q"
-  and P': "PROP P'"
+    and P': "PROP P'"
   from PP' [symmetric] and P' have "PROP P"
     by (rule equal_elim_rule1)
   then have "PROP Q" by (rule PQ)
   with P'QQ' [OF P'] show "PROP Q'" by (rule equal_elim_rule1)
 next
   assume P'Q': "PROP P' \<Longrightarrow> PROP Q'"
-  and P: "PROP P"
+    and P: "PROP P"
   from PP' and P have P': "PROP P'" by (rule equal_elim_rule1)
   then have "PROP Q'" by (rule P'Q')
   with P'QQ' [OF P', symmetric] show "PROP Q"
@@ -1141,12 +1130,10 @@
   shows "(\<exists>x. P x) = (\<exists>x. Q x)"
   using assms by blast
 
-lemma all_comm:
-  "(\<forall>x y. P x y) = (\<forall>y x. P x y)"
+lemma all_comm: "(\<forall>x y. P x y) = (\<forall>y x. P x y)"
   by blast
 
-lemma ex_comm:
-  "(\<exists>x y. P x y) = (\<exists>y x. P x y)"
+lemma ex_comm: "(\<exists>x y. P x y) = (\<exists>y x. P x y)"
   by blast
 
 ML_file "Tools/simpdata.ML"
@@ -1163,79 +1150,80 @@
 text \<open>Simproc for proving \<open>(y = x) \<equiv> False\<close> from premise \<open>\<not> (x = y)\<close>:\<close>
 
 simproc_setup neq ("x = y") = \<open>fn _ =>
-let
-  val neq_to_EQ_False = @{thm not_sym} RS @{thm Eq_FalseI};
-  fun is_neq eq lhs rhs thm =
-    (case Thm.prop_of thm of
-      _ $ (Not $ (eq' $ l' $ r')) =>
-        Not = HOLogic.Not andalso eq' = eq andalso
-        r' aconv lhs andalso l' aconv rhs
-    | _ => false);
-  fun proc ss ct =
-    (case Thm.term_of ct of
-      eq $ lhs $ rhs =>
-        (case find_first (is_neq eq lhs rhs) (Simplifier.prems_of ss) of
-          SOME thm => SOME (thm RS neq_to_EQ_False)
-        | NONE => NONE)
-     | _ => NONE);
-in proc end;
+  let
+    val neq_to_EQ_False = @{thm not_sym} RS @{thm Eq_FalseI};
+    fun is_neq eq lhs rhs thm =
+      (case Thm.prop_of thm of
+        _ $ (Not $ (eq' $ l' $ r')) =>
+          Not = HOLogic.Not andalso eq' = eq andalso
+          r' aconv lhs andalso l' aconv rhs
+      | _ => false);
+    fun proc ss ct =
+      (case Thm.term_of ct of
+        eq $ lhs $ rhs =>
+          (case find_first (is_neq eq lhs rhs) (Simplifier.prems_of ss) of
+            SOME thm => SOME (thm RS neq_to_EQ_False)
+          | NONE => NONE)
+       | _ => NONE);
+  in proc end;
 \<close>
 
 simproc_setup let_simp ("Let x f") = \<open>
-let
-  fun count_loose (Bound i) k = if i >= k then 1 else 0
-    | count_loose (s $ t) k = count_loose s k + count_loose t k
-    | count_loose (Abs (_, _, t)) k = count_loose  t (k + 1)
-    | count_loose _ _ = 0;
-  fun is_trivial_let (Const (@{const_name Let}, _) $ x $ t) =
-    (case t of
-      Abs (_, _, t') => count_loose t' 0 <= 1
-    | _ => true);
-in
-  fn _ => fn ctxt => fn ct =>
-    if is_trivial_let (Thm.term_of ct)
-    then SOME @{thm Let_def} (*no or one ocurrence of bound variable*)
-    else
-      let (*Norbert Schirmer's case*)
-        val t = Thm.term_of ct;
-        val ([t'], ctxt') = Variable.import_terms false [t] ctxt;
-      in
-        Option.map (hd o Variable.export ctxt' ctxt o single)
-          (case t' of Const (@{const_name Let},_) $ x $ f => (* x and f are already in normal form *)
-            if is_Free x orelse is_Bound x orelse is_Const x
-            then SOME @{thm Let_def}
-            else
-              let
-                val n = case f of (Abs (x, _, _)) => x | _ => "x";
-                val cx = Thm.cterm_of ctxt x;
-                val xT = Thm.typ_of_cterm cx;
-                val cf = Thm.cterm_of ctxt f;
-                val fx_g = Simplifier.rewrite ctxt (Thm.apply cf cx);
-                val (_ $ _ $ g) = Thm.prop_of fx_g;
-                val g' = abstract_over (x, g);
-                val abs_g'= Abs (n, xT, g');
-              in
-                if g aconv g' then
-                  let
-                    val rl =
-                      infer_instantiate ctxt [(("f", 0), cf), (("x", 0), cx)] @{thm Let_unfold};
-                  in SOME (rl OF [fx_g]) end
-                else if (Envir.beta_eta_contract f) aconv (Envir.beta_eta_contract abs_g')
-                then NONE (*avoid identity conversion*)
-                else
-                  let
-                    val g'x = abs_g' $ x;
-                    val g_g'x = Thm.symmetric (Thm.beta_conversion false (Thm.cterm_of ctxt g'x));
-                    val rl =
-                      @{thm Let_folded} |> infer_instantiate ctxt
-                        [(("f", 0), Thm.cterm_of ctxt f),
-                         (("x", 0), cx),
-                         (("g", 0), Thm.cterm_of ctxt abs_g')];
-                  in SOME (rl OF [Thm.transitive fx_g g_g'x]) end
-              end
-          | _ => NONE)
-      end
-end\<close>
+  let
+    fun count_loose (Bound i) k = if i >= k then 1 else 0
+      | count_loose (s $ t) k = count_loose s k + count_loose t k
+      | count_loose (Abs (_, _, t)) k = count_loose  t (k + 1)
+      | count_loose _ _ = 0;
+    fun is_trivial_let (Const (@{const_name Let}, _) $ x $ t) =
+      (case t of
+        Abs (_, _, t') => count_loose t' 0 <= 1
+      | _ => true);
+  in
+    fn _ => fn ctxt => fn ct =>
+      if is_trivial_let (Thm.term_of ct)
+      then SOME @{thm Let_def} (*no or one ocurrence of bound variable*)
+      else
+        let (*Norbert Schirmer's case*)
+          val t = Thm.term_of ct;
+          val ([t'], ctxt') = Variable.import_terms false [t] ctxt;
+        in
+          Option.map (hd o Variable.export ctxt' ctxt o single)
+            (case t' of Const (@{const_name Let},_) $ x $ f => (* x and f are already in normal form *)
+              if is_Free x orelse is_Bound x orelse is_Const x
+              then SOME @{thm Let_def}
+              else
+                let
+                  val n = case f of (Abs (x, _, _)) => x | _ => "x";
+                  val cx = Thm.cterm_of ctxt x;
+                  val xT = Thm.typ_of_cterm cx;
+                  val cf = Thm.cterm_of ctxt f;
+                  val fx_g = Simplifier.rewrite ctxt (Thm.apply cf cx);
+                  val (_ $ _ $ g) = Thm.prop_of fx_g;
+                  val g' = abstract_over (x, g);
+                  val abs_g'= Abs (n, xT, g');
+                in
+                  if g aconv g' then
+                    let
+                      val rl =
+                        infer_instantiate ctxt [(("f", 0), cf), (("x", 0), cx)] @{thm Let_unfold};
+                    in SOME (rl OF [fx_g]) end
+                  else if (Envir.beta_eta_contract f) aconv (Envir.beta_eta_contract abs_g')
+                  then NONE (*avoid identity conversion*)
+                  else
+                    let
+                      val g'x = abs_g' $ x;
+                      val g_g'x = Thm.symmetric (Thm.beta_conversion false (Thm.cterm_of ctxt g'x));
+                      val rl =
+                        @{thm Let_folded} |> infer_instantiate ctxt
+                          [(("f", 0), Thm.cterm_of ctxt f),
+                           (("x", 0), cx),
+                           (("g", 0), Thm.cterm_of ctxt abs_g')];
+                    in SOME (rl OF [Thm.transitive fx_g g_g'x]) end
+                end
+            | _ => NONE)
+        end
+  end
+\<close>
 
 lemma True_implies_equals: "(True \<Longrightarrow> PROP P) \<equiv> PROP P"
 proof
@@ -1254,9 +1242,10 @@
 
 (* This is not made a simp rule because it does not improve any proofs
    but slows some AFP entries down by 5% (cpu time). May 2015 *)
-lemma implies_False_swap: "NO_MATCH (Trueprop False) P \<Longrightarrow>
-  (False \<Longrightarrow> PROP P \<Longrightarrow> PROP Q) \<equiv> (PROP P \<Longrightarrow> False \<Longrightarrow> PROP Q)"
-by(rule swap_prems_eq)
+lemma implies_False_swap:
+  "NO_MATCH (Trueprop False) P \<Longrightarrow>
+    (False \<Longrightarrow> PROP P \<Longrightarrow> PROP Q) \<equiv> (PROP P \<Longrightarrow> False \<Longrightarrow> PROP Q)"
+  by (rule swap_prems_eq)
 
 lemma ex_simps:
   "\<And>P Q. (\<exists>x. P x \<and> Q)   = ((\<exists>x. P x) \<and> Q)"
@@ -1279,19 +1268,19 @@
   by (iprover | blast)+
 
 lemmas [simp] =
-  triv_forall_equality (*prunes params*)
-  True_implies_equals implies_True_equals (*prune True in asms*)
-  False_implies_equals (*prune False in asms*)
+  triv_forall_equality  \<comment> \<open>prunes params\<close>
+  True_implies_equals implies_True_equals  \<comment> \<open>prune \<open>True\<close> in asms\<close>
+  False_implies_equals  \<comment> \<open>prune \<open>False\<close> in asms\<close>
   if_True
   if_False
   if_cancel
   if_eq_cancel
-  imp_disjL
-  (*In general it seems wrong to add distributive laws by default: they
-    might cause exponential blow-up.  But imp_disjL has been in for a while
+  imp_disjL \<comment>
+   \<open>In general it seems wrong to add distributive laws by default: they
+    might cause exponential blow-up.  But \<open>imp_disjL\<close> has been in for a while
     and cannot be removed without affecting existing proofs.  Moreover,
-    rewriting by "(P \<or> Q \<longrightarrow> R) = ((P \<longrightarrow> R) \<and> (Q \<longrightarrow> R))" might be justified on the
-    grounds that it allows simplification of R in the two cases.*)
+    rewriting by \<open>(P \<or> Q \<longrightarrow> R) = ((P \<longrightarrow> R) \<and> (Q \<longrightarrow> R))\<close> might be justified on the
+    grounds that it allows simplification of \<open>R\<close> in the two cases.\<close>
   conj_assoc
   disj_assoc
   de_Morgan_conj
@@ -1314,15 +1303,15 @@
 
 ML \<open>val HOL_ss = simpset_of @{context}\<close>
 
-text \<open>Simplifies @{term x} assuming @{prop c} and @{term y} assuming @{prop "\<not> c"}\<close>
+text \<open>Simplifies \<open>x\<close> assuming \<open>c\<close> and \<open>y\<close> assuming \<open>\<not> c\<close>.\<close>
 lemma if_cong:
   assumes "b = c"
-      and "c \<Longrightarrow> x = u"
-      and "\<not> c \<Longrightarrow> y = v"
+    and "c \<Longrightarrow> x = u"
+    and "\<not> c \<Longrightarrow> y = v"
   shows "(if b then x else y) = (if c then u else v)"
   using assms by simp
 
-text \<open>Prevents simplification of x and y:
+text \<open>Prevents simplification of \<open>x\<close> and \<open>y\<close>:
   faster and allows the execution of functional programs.\<close>
 lemma if_weak_cong [cong]:
   assumes "b = c"
@@ -1341,11 +1330,10 @@
   shows "(t \<equiv> u) \<equiv> (t \<equiv> u')"
   using assms by simp
 
-lemma if_distrib:
-  "f (if c then x else y) = (if c then f x else f y)"
+lemma if_distrib: "f (if c then x else y) = (if c then f x else f y)"
   by simp
 
-text\<open>As a simplification rule, it replaces all function equalities by
+text \<open>As a simplification rule, it replaces all function equalities by
   first-order equalities.\<close>
 lemma fun_eq_iff: "f = g \<longleftrightarrow> (\<forall>x. f x = g x)"
   by auto
@@ -1578,27 +1566,32 @@
 
 lemma choice_eq: "(\<forall>x. \<exists>!y. P x y) = (\<exists>!f. \<forall>x. P x (f x))"
   apply (rule iffI)
-  apply (rule_tac a = "\<lambda>x. THE y. P x y" in ex1I)
-  apply (fast dest!: theI')
-  apply (fast intro: the1_equality [symmetric])
+   apply (rule_tac a = "\<lambda>x. THE y. P x y" in ex1I)
+    apply (fast dest!: theI')
+   apply (fast intro: the1_equality [symmetric])
   apply (erule ex1E)
   apply (rule allI)
   apply (rule ex1I)
-  apply (erule spec)
+   apply (erule spec)
   apply (erule_tac x = "\<lambda>z. if z = x then y else f z" in allE)
   apply (erule impE)
-  apply (rule allI)
-  apply (case_tac "xa = x")
-  apply (drule_tac [3] x = x in fun_cong, simp_all)
+   apply (rule allI)
+   apply (case_tac "xa = x")
+    apply (drule_tac [3] x = x in fun_cong)
+    apply simp_all
   done
 
 lemmas eq_sym_conv = eq_commute
 
 lemma nnf_simps:
-  "(\<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)"
-  "(P = Q) = ((P \<and> Q) \<or> (\<not>P \<and> \<not> Q))" "(\<not>(P = Q)) = ((P \<and> \<not> Q) \<or> (\<not>P \<and> Q))"
-  "(\<not> \<not>(P)) = P"
-by blast+
+  "(\<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)"
+  "(P = Q) = ((P \<and> Q) \<or> (\<not> P \<and> \<not> Q))"
+  "(\<not> (P = Q)) = ((P \<and> \<not> Q) \<or> (\<not> P \<and> Q))"
+  "(\<not> \<not> P) = P"
+  by blast+
+
 
 subsection \<open>Basic ML bindings\<close>
 
@@ -1659,12 +1652,15 @@
 section \<open>\<open>NO_MATCH\<close> simproc\<close>
 
 text \<open>
- The simplification procedure can be used to avoid simplification of terms of a certain form
+  The simplification procedure can be used to avoid simplification of terms
+  of a certain form.
 \<close>
 
-definition NO_MATCH :: "'a \<Rightarrow> 'b \<Rightarrow> bool" where "NO_MATCH pat val \<equiv> True"
+definition NO_MATCH :: "'a \<Rightarrow> 'b \<Rightarrow> bool"
+  where "NO_MATCH pat val \<equiv> True"
 
-lemma NO_MATCH_cong[cong]: "NO_MATCH pat val = NO_MATCH pat val" by (rule refl)
+lemma NO_MATCH_cong[cong]: "NO_MATCH pat val = NO_MATCH pat val"
+  by (rule refl)
 
 declare [[coercion_args NO_MATCH - -]]
 
@@ -1678,24 +1674,26 @@
 
 text \<open>
   This setup ensures that a rewrite rule of the form @{term "NO_MATCH pat val \<Longrightarrow> t"}
-  is only applied, if the pattern @{term pat} does not match the value @{term val}.
+  is only applied, if the pattern \<open>pat\<close> does not match the value \<open>val\<close>.
 \<close>
 
 
-text\<open>Tagging a premise of a simp rule with ASSUMPTION forces the simplifier
-not to simplify the argument and to solve it by an assumption.\<close>
+text\<open>
+  Tagging a premise of a simp rule with ASSUMPTION forces the simplifier
+  not to simplify the argument and to solve it by an assumption.
+\<close>
 
-definition ASSUMPTION :: "bool \<Rightarrow> bool" where
-"ASSUMPTION A \<equiv> A"
+definition ASSUMPTION :: "bool \<Rightarrow> bool"
+  where "ASSUMPTION A \<equiv> A"
 
 lemma ASSUMPTION_cong[cong]: "ASSUMPTION A = ASSUMPTION A"
-by (rule refl)
+  by (rule refl)
 
 lemma ASSUMPTION_I: "A \<Longrightarrow> ASSUMPTION A"
-by(simp add: ASSUMPTION_def)
+  by (simp add: ASSUMPTION_def)
 
 lemma ASSUMPTION_D: "ASSUMPTION A \<Longrightarrow> A"
-by(simp add: ASSUMPTION_def)
+  by (simp add: ASSUMPTION_def)
 
 setup \<open>
 let
@@ -1712,12 +1710,10 @@
 
 subsubsection \<open>Generic code generator preprocessor setup\<close>
 
-lemma conj_left_cong:
-  "P \<longleftrightarrow> Q \<Longrightarrow> P \<and> R \<longleftrightarrow> Q \<and> R"
+lemma conj_left_cong: "P \<longleftrightarrow> Q \<Longrightarrow> P \<and> R \<longleftrightarrow> Q \<and> R"
   by (fact arg_cong)
 
-lemma disj_left_cong:
-  "P \<longleftrightarrow> Q \<Longrightarrow> P \<or> R \<longleftrightarrow> Q \<or> R"
+lemma disj_left_cong: "P \<longleftrightarrow> Q \<Longrightarrow> P \<or> R \<longleftrightarrow> Q \<or> R"
   by (fact arg_cong)
 
 setup \<open>
@@ -1772,29 +1768,32 @@
   shows "False \<and> P \<longleftrightarrow> False"
     and "True \<and> P \<longleftrightarrow> P"
     and "P \<and> False \<longleftrightarrow> False"
-    and "P \<and> True \<longleftrightarrow> P" by simp_all
+    and "P \<and> True \<longleftrightarrow> P"
+  by simp_all
 
 lemma [code]:
   shows "False \<or> P \<longleftrightarrow> P"
     and "True \<or> P \<longleftrightarrow> True"
     and "P \<or> False \<longleftrightarrow> P"
-    and "P \<or> True \<longleftrightarrow> True" by simp_all
+    and "P \<or> True \<longleftrightarrow> True"
+  by simp_all
 
 lemma [code]:
   shows "(False \<longrightarrow> P) \<longleftrightarrow> True"
     and "(True \<longrightarrow> P) \<longleftrightarrow> P"
     and "(P \<longrightarrow> False) \<longleftrightarrow> \<not> P"
-    and "(P \<longrightarrow> True) \<longleftrightarrow> True" by simp_all
+    and "(P \<longrightarrow> True) \<longleftrightarrow> True"
+  by simp_all
 
 text \<open>More about @{typ prop}\<close>
 
 lemma [code nbe]:
   shows "(True \<Longrightarrow> PROP Q) \<equiv> PROP Q"
     and "(PROP Q \<Longrightarrow> True) \<equiv> Trueprop True"
-    and "(P \<Longrightarrow> R) \<equiv> Trueprop (P \<longrightarrow> R)" by (auto intro!: equal_intr_rule)
+    and "(P \<Longrightarrow> R) \<equiv> Trueprop (P \<longrightarrow> R)"
+  by (auto intro!: equal_intr_rule)
 
-lemma Trueprop_code [code]:
-  "Trueprop True \<equiv> Code_Generator.holds"
+lemma Trueprop_code [code]: "Trueprop True \<equiv> Code_Generator.holds"
   by (auto intro!: equal_intr_rule holds)
 
 declare Trueprop_code [symmetric, code_post]
@@ -1806,21 +1805,21 @@
 instantiation itself :: (type) equal
 begin
 
-definition equal_itself :: "'a itself \<Rightarrow> 'a itself \<Rightarrow> bool" where
-  "equal_itself x y \<longleftrightarrow> x = y"
+definition equal_itself :: "'a itself \<Rightarrow> 'a itself \<Rightarrow> bool"
+  where "equal_itself x y \<longleftrightarrow> x = y"
 
-instance proof
-qed (fact equal_itself_def)
+instance
+  by standard (fact equal_itself_def)
 
 end
 
-lemma equal_itself_code [code]:
-  "equal TYPE('a) TYPE('a) \<longleftrightarrow> True"
+lemma equal_itself_code [code]: "equal TYPE('a) TYPE('a) \<longleftrightarrow> True"
   by (simp add: equal)
 
 setup \<open>Sign.add_const_constraint (@{const_name equal}, SOME @{typ "'a::type \<Rightarrow> 'a \<Rightarrow> bool"})\<close>
 
-lemma equal_alias_cert: "OFCLASS('a, equal_class) \<equiv> ((op = :: 'a \<Rightarrow> 'a \<Rightarrow> bool) \<equiv> equal)" (is "?ofclass \<equiv> ?equal")
+lemma equal_alias_cert: "OFCLASS('a, equal_class) \<equiv> ((op = :: 'a \<Rightarrow> 'a \<Rightarrow> bool) \<equiv> equal)"
+  (is "?ofclass \<equiv> ?equal")
 proof
   assume "PROP ?ofclass"
   show "PROP ?equal"
@@ -1900,15 +1899,13 @@
   code_module Pure \<rightharpoonup>
     (SML) HOL and (OCaml) HOL and (Haskell) HOL and (Scala) HOL
 
-text \<open>using built-in Haskell equality\<close>
-
+text \<open>Using built-in Haskell equality.\<close>
 code_printing
   type_class equal \<rightharpoonup> (Haskell) "Eq"
 | constant HOL.equal \<rightharpoonup> (Haskell) infix 4 "=="
 | constant HOL.eq \<rightharpoonup> (Haskell) infix 4 "=="
 
-text \<open>undefined\<close>
-
+text \<open>\<open>undefined\<close>\<close>
 code_printing
   constant undefined \<rightharpoonup>
     (SML) "!(raise/ Fail/ \"undefined\")"
@@ -1956,7 +1953,7 @@
   and nitpick_choice_spec "choice specification of constants as needed by Nitpick"
 
 declare if_bool_eq_conj [nitpick_unfold, no_atp]
-        if_bool_eq_disj [no_atp]
+  and if_bool_eq_disj [no_atp]
 
 
 subsection \<open>Preprocessing for the predicate compiler\<close>
diff -r 4ea48cbc54c1 -r b9bd9e61fd63 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Mon Aug 01 13:51:17 2016 +0200
+++ b/src/HOL/Product_Type.thy	Mon Aug 01 22:11:29 2016 +0200
@@ -6,8 +6,8 @@
 section \<open>Cartesian products\<close>
 
 theory Product_Type
-imports Typedef Inductive Fun
-keywords "inductive_set" "coinductive_set" :: thy_decl
+  imports Typedef Inductive Fun
+  keywords "inductive_set" "coinductive_set" :: thy_decl
 begin
 
 subsection \<open>@{typ bool} is a datatype\<close>
@@ -38,7 +38,7 @@
   \<comment> "prefer plain propositional version"
 
 lemma [code]: "HOL.equal False P \<longleftrightarrow> \<not> P"
-  and [code]: "HOL.equal True P \<longleftrightarrow> P" 
+  and [code]: "HOL.equal True P \<longleftrightarrow> P"
   and [code]: "HOL.equal P False \<longleftrightarrow> \<not> P"
   and [code]: "HOL.equal P True \<longleftrightarrow> P"
   and [code nbe]: "HOL.equal P P \<longleftrightarrow> True"
@@ -317,7 +317,7 @@
           (case (head_of t) of
             Const (@{const_syntax case_prod}, _) => raise Match
           | _ =>
-            let 
+            let
               val (_ :: yT :: _) = binder_types (domain_type T) handle Bind => raise Match;
               val (y, t') = Syntax_Trans.atomic_abs_tr' ("y", yT, incr_boundvars 1 t $ Bound 0);
               val (x', t'') = Syntax_Trans.atomic_abs_tr' (x, xT, t');
@@ -618,7 +618,7 @@
 declare case_prodI2' [intro!] \<comment> \<open>postponed to maintain traditional declaration order!\<close>
 declare case_prodI2 [intro!] \<comment> \<open>postponed to maintain traditional declaration order!\<close>
 declare case_prodI [intro!] \<comment> \<open>postponed to maintain traditional declaration order!\<close>
-  
+
 lemma mem_case_prodE [elim!]:
   assumes "z \<in> case_prod c p"
   obtains x y where "p = (x, y)" and "z \<in> c x y"
@@ -631,10 +631,10 @@
     | exists_p_split (Abs (_, _, t)) = exists_p_split t
     | exists_p_split _ = false;
 in
-fun split_conv_tac ctxt = SUBGOAL (fn (t, i) =>
-  if exists_p_split t
-  then safe_full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms case_prod_conv}) i
-  else no_tac);
+  fun split_conv_tac ctxt = SUBGOAL (fn (t, i) =>
+    if exists_p_split t
+    then safe_full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms case_prod_conv}) i
+    else no_tac);
 end;
 \<close>
 
@@ -656,7 +656,7 @@
    a) only helps in special situations
    b) can lead to nontermination in the presence of split_def
 *)
-lemma split_comp_eq: 
+lemma split_comp_eq:
   fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c"
     and g :: "'d \<Rightarrow> 'a"
   shows "(\<lambda>u. f (g (fst u)) (snd u)) = case_prod (\<lambda>x. f (g x))"
@@ -836,7 +836,7 @@
   apply (rule major [THEN imageE])
   apply (case_tac x)
   apply (rule cases)
-  apply simp_all
+   apply simp_all
   done
 
 definition apfst :: "('a \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c \<times> 'b"
@@ -845,10 +845,10 @@
 definition apsnd :: "('b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'a \<times> 'c"
   where "apsnd f = map_prod id f"
 
-lemma apfst_conv [simp, code]: "apfst f (x, y) = (f x, y)" 
+lemma apfst_conv [simp, code]: "apfst f (x, y) = (f x, y)"
   by (simp add: apfst_def)
 
-lemma apsnd_conv [simp, code]: "apsnd f (x, y) = (x, f y)" 
+lemma apsnd_conv [simp, code]: "apsnd f (x, y) = (x, f y)"
   by (simp add: apsnd_def)
 
 lemma fst_apfst [simp]: "fst (apfst f x) = f (fst x)"
@@ -1029,11 +1029,11 @@
 lemma Collect_case_prod_mono: "A \<le> B \<Longrightarrow> Collect (case_prod A) \<subseteq> Collect (case_prod B)"
   by auto (auto elim!: le_funE)
 
-lemma Collect_split_mono_strong: 
+lemma Collect_split_mono_strong:
   "X = fst ` A \<Longrightarrow> Y = snd ` A \<Longrightarrow> \<forall>a\<in>X. \<forall>b \<in> Y. P a b \<longrightarrow> Q a b
     \<Longrightarrow> A \<subseteq> Collect (case_prod P) \<Longrightarrow> A \<subseteq> Collect (case_prod Q)"
   by fastforce
-  
+
 lemma UN_Times_distrib: "(\<Union>(a, b)\<in>A \<times> B. E a \<times> F b) = UNION A E \<times> UNION B F"
   \<comment> \<open>Suggested by Pierre Chartier\<close>
   by blast
@@ -1151,18 +1151,19 @@
 context
 begin
 
-qualified definition product :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set" where
-  [code_abbrev]: "product A B = A \<times> B"
+qualified definition product :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set"
+  where [code_abbrev]: "product A B = A \<times> B"
 
 lemma member_product: "x \<in> Product_Type.product A B \<longleftrightarrow> x \<in> A \<times> B"
   by (simp add: product_def)
 
 end
-  
+
 text \<open>The following @{const map_prod} lemmas are due to Joachim Breitner:\<close>
 
 lemma map_prod_inj_on:
-  assumes "inj_on f A" and "inj_on g B"
+  assumes "inj_on f A"
+    and "inj_on g B"
   shows "inj_on (map_prod f g) (A \<times> B)"
 proof (rule inj_onI)
   fix x :: "'a \<times> 'c"
diff -r 4ea48cbc54c1 -r b9bd9e61fd63 src/HOL/Sum_Type.thy
--- a/src/HOL/Sum_Type.thy	Mon Aug 01 13:51:17 2016 +0200
+++ b/src/HOL/Sum_Type.thy	Mon Aug 01 22:11:29 2016 +0200
@@ -3,10 +3,10 @@
     Copyright   1992  University of Cambridge
 *)
 
-section\<open>The Disjoint Sum of Two Types\<close>
+section \<open>The Disjoint Sum of Two Types\<close>
 
 theory Sum_Type
-imports Typedef Inductive Fun
+  imports Typedef Inductive Fun
 begin
 
 subsection \<open>Construction of the sum type and its basic abstract operations\<close>
@@ -85,7 +85,8 @@
 proof (rule Abs_sum_cases [of s])
   fix f
   assume "s = Abs_sum f" and "f \<in> sum"
-  with assms show P by (auto simp add: sum_def Inl_def Inr_def)
+  with assms show P
+    by (auto simp add: sum_def Inl_def Inr_def)
 qed
 
 free_constructors case_sum for
@@ -123,9 +124,9 @@
 setup \<open>Sign.parent_path\<close>
 
 primrec map_sum :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> 'a + 'b \<Rightarrow> 'c + 'd"
-where
-  "map_sum f1 f2 (Inl a) = Inl (f1 a)"
-| "map_sum f1 f2 (Inr a) = Inr (f2 a)"
+  where
+    "map_sum f1 f2 (Inl a) = Inl (f1 a)"
+  | "map_sum f1 f2 (Inr a) = Inr (f2 a)"
 
 functor map_sum: map_sum
 proof -