misc tuning and modernization;
authorwenzelm
Mon Jun 20 17:03:50 2016 +0200 (2016-06-20)
changeset 63322bc1f17d45e91
parent 63316 dff40165618c
child 63323 814541a57d89
misc tuning and modernization;
src/HOL/Fun.thy
src/HOL/Lattices.thy
     1.1 --- a/src/HOL/Fun.thy	Sun Jun 19 22:51:42 2016 +0200
     1.2 +++ b/src/HOL/Fun.thy	Mon Jun 20 17:03:50 2016 +0200
     1.3 @@ -11,11 +11,10 @@
     1.4  keywords "functor" :: thy_goal
     1.5  begin
     1.6  
     1.7 -lemma apply_inverse:
     1.8 -  "f x = u \<Longrightarrow> (\<And>x. P x \<Longrightarrow> g (f x) = x) \<Longrightarrow> P x \<Longrightarrow> x = g u"
     1.9 +lemma apply_inverse: "f x = u \<Longrightarrow> (\<And>x. P x \<Longrightarrow> g (f x) = x) \<Longrightarrow> P x \<Longrightarrow> x = g u"
    1.10    by auto
    1.11  
    1.12 -text\<open>Uniqueness, so NOT the axiom of choice.\<close>
    1.13 +text \<open>Uniqueness, so NOT the axiom of choice.\<close>
    1.14  lemma uniq_choice: "\<forall>x. \<exists>!y. Q x y \<Longrightarrow> \<exists>f. \<forall>x. Q x (f x)"
    1.15    by (force intro: theI')
    1.16  
    1.17 @@ -24,8 +23,8 @@
    1.18  
    1.19  subsection \<open>The Identity Function \<open>id\<close>\<close>
    1.20  
    1.21 -definition id :: "'a \<Rightarrow> 'a" where
    1.22 -  "id = (\<lambda>x. x)"
    1.23 +definition id :: "'a \<Rightarrow> 'a"
    1.24 +  where "id = (\<lambda>x. x)"
    1.25  
    1.26  lemma id_apply [simp]: "id x = x"
    1.27    by (simp add: id_def)
    1.28 @@ -51,55 +50,51 @@
    1.29  notation (ASCII)
    1.30    comp  (infixl "o" 55)
    1.31  
    1.32 -lemma comp_apply [simp]: "(f o g) x = f (g x)"
    1.33 +lemma comp_apply [simp]: "(f \<circ> g) x = f (g x)"
    1.34    by (simp add: comp_def)
    1.35  
    1.36 -lemma comp_assoc: "(f o g) o h = f o (g o h)"
    1.37 +lemma comp_assoc: "(f \<circ> g) \<circ> h = f \<circ> (g \<circ> h)"
    1.38    by (simp add: fun_eq_iff)
    1.39  
    1.40 -lemma id_comp [simp]: "id o g = g"
    1.41 +lemma id_comp [simp]: "id \<circ> g = g"
    1.42    by (simp add: fun_eq_iff)
    1.43  
    1.44 -lemma comp_id [simp]: "f o id = f"
    1.45 +lemma comp_id [simp]: "f \<circ> id = f"
    1.46    by (simp add: fun_eq_iff)
    1.47  
    1.48  lemma comp_eq_dest:
    1.49 -  "a o b = c o d \<Longrightarrow> a (b v) = c (d v)"
    1.50 +  "a \<circ> b = c \<circ> d \<Longrightarrow> a (b v) = c (d v)"
    1.51    by (simp add: fun_eq_iff)
    1.52  
    1.53  lemma comp_eq_elim:
    1.54 -  "a o b = c o d \<Longrightarrow> ((\<And>v. a (b v) = c (d v)) \<Longrightarrow> R) \<Longrightarrow> R"
    1.55 +  "a \<circ> b = c \<circ> d \<Longrightarrow> ((\<And>v. a (b v) = c (d v)) \<Longrightarrow> R) \<Longrightarrow> R"
    1.56    by (simp add: fun_eq_iff)
    1.57  
    1.58 -lemma comp_eq_dest_lhs: "a o b = c \<Longrightarrow> a (b v) = c v"
    1.59 -  by clarsimp
    1.60 -
    1.61 -lemma comp_eq_id_dest: "a o b = id o c \<Longrightarrow> a (b v) = c v"
    1.62 +lemma comp_eq_dest_lhs: "a \<circ> b = c \<Longrightarrow> a (b v) = c v"
    1.63    by clarsimp
    1.64  
    1.65 -lemma image_comp:
    1.66 -  "f ` (g ` r) = (f o g) ` r"
    1.67 +lemma comp_eq_id_dest: "a \<circ> b = id \<circ> c \<Longrightarrow> a (b v) = c v"
    1.68 +  by clarsimp
    1.69 +
    1.70 +lemma image_comp: "f ` (g ` r) = (f \<circ> g) ` r"
    1.71    by auto
    1.72  
    1.73 -lemma vimage_comp:
    1.74 -  "f -` (g -` x) = (g \<circ> f) -` x"
    1.75 +lemma vimage_comp: "f -` (g -` x) = (g \<circ> f) -` x"
    1.76    by auto
    1.77  
    1.78 -lemma image_eq_imp_comp: "f ` A = g ` B \<Longrightarrow> (h o f) ` A = (h o g) ` B"
    1.79 +lemma image_eq_imp_comp: "f ` A = g ` B \<Longrightarrow> (h \<circ> f) ` A = (h \<circ> g) ` B"
    1.80    by (auto simp: comp_def elim!: equalityE)
    1.81  
    1.82  lemma image_bind: "f ` (Set.bind A g) = Set.bind A (op ` f \<circ> g)"
    1.83 -by(auto simp add: Set.bind_def)
    1.84 +  by (auto simp add: Set.bind_def)
    1.85  
    1.86  lemma bind_image: "Set.bind (f ` A) g = Set.bind A (g \<circ> f)"
    1.87 -by(auto simp add: Set.bind_def)
    1.88 +  by (auto simp add: Set.bind_def)
    1.89  
    1.90 -lemma (in group_add) minus_comp_minus [simp]:
    1.91 -  "uminus \<circ> uminus = id"
    1.92 +lemma (in group_add) minus_comp_minus [simp]: "uminus \<circ> uminus = id"
    1.93    by (simp add: fun_eq_iff)
    1.94  
    1.95 -lemma (in boolean_algebra) minus_comp_minus [simp]:
    1.96 -  "uminus \<circ> uminus = id"
    1.97 +lemma (in boolean_algebra) minus_comp_minus [simp]: "uminus \<circ> uminus = id"
    1.98    by (simp add: fun_eq_iff)
    1.99  
   1.100  code_printing
   1.101 @@ -108,8 +103,8 @@
   1.102  
   1.103  subsection \<open>The Forward Composition Operator \<open>fcomp\<close>\<close>
   1.104  
   1.105 -definition fcomp :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'c" (infixl "\<circ>>" 60) where
   1.106 -  "f \<circ>> g = (\<lambda>x. g (f x))"
   1.107 +definition fcomp :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'c" (infixl "\<circ>>" 60)
   1.108 +  where "f \<circ>> g = (\<lambda>x. g (f x))"
   1.109  
   1.110  lemma fcomp_apply [simp]:  "(f \<circ>> g) x = g (f x)"
   1.111    by (simp add: fcomp_def)
   1.112 @@ -123,7 +118,7 @@
   1.113  lemma fcomp_id [simp]: "f \<circ>> id = f"
   1.114    by (simp add: fcomp_def)
   1.115  
   1.116 -lemma fcomp_comp: "fcomp f g = comp g f" 
   1.117 +lemma fcomp_comp: "fcomp f g = comp g f"
   1.118    by (simp add: ext)
   1.119  
   1.120  code_printing
   1.121 @@ -134,168 +129,143 @@
   1.122  
   1.123  subsection \<open>Mapping functions\<close>
   1.124  
   1.125 -definition map_fun :: "('c \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'c \<Rightarrow> 'd" where
   1.126 -  "map_fun f g h = g \<circ> h \<circ> f"
   1.127 +definition map_fun :: "('c \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'c \<Rightarrow> 'd"
   1.128 +  where "map_fun f g h = g \<circ> h \<circ> f"
   1.129  
   1.130 -lemma map_fun_apply [simp]:
   1.131 -  "map_fun f g h x = g (h (f x))"
   1.132 +lemma map_fun_apply [simp]: "map_fun f g h x = g (h (f x))"
   1.133    by (simp add: map_fun_def)
   1.134  
   1.135  
   1.136  subsection \<open>Injectivity and Bijectivity\<close>
   1.137  
   1.138 -definition inj_on :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> bool" where \<comment> "injective"
   1.139 -  "inj_on f A \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>A. f x = f y \<longrightarrow> x = y)"
   1.140 +definition inj_on :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> bool"  \<comment> \<open>injective\<close>
   1.141 +  where "inj_on f A \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>A. f x = f y \<longrightarrow> x = y)"
   1.142  
   1.143 -definition bij_betw :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> bool" where \<comment> "bijective"
   1.144 -  "bij_betw f A B \<longleftrightarrow> inj_on f A \<and> f ` A = B"
   1.145 +definition bij_betw :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> bool"  \<comment> \<open>bijective\<close>
   1.146 +  where "bij_betw f A B \<longleftrightarrow> inj_on f A \<and> f ` A = B"
   1.147  
   1.148 -text\<open>A common special case: functions injective, surjective or bijective over
   1.149 -the entire domain type.\<close>
   1.150 +text \<open>A common special case: functions injective, surjective or bijective over
   1.151 +  the entire domain type.\<close>
   1.152  
   1.153 -abbreviation
   1.154 -  "inj f \<equiv> inj_on f UNIV"
   1.155 +abbreviation "inj f \<equiv> inj_on f UNIV"
   1.156  
   1.157 -abbreviation surj :: "('a \<Rightarrow> 'b) \<Rightarrow> bool" where \<comment> "surjective"
   1.158 -  "surj f \<equiv> (range f = UNIV)"
   1.159 +abbreviation surj :: "('a \<Rightarrow> 'b) \<Rightarrow> bool"  \<comment> "surjective"
   1.160 +  where "surj f \<equiv> range f = UNIV"
   1.161  
   1.162 -abbreviation
   1.163 -  "bij f \<equiv> bij_betw f UNIV UNIV"
   1.164 +abbreviation "bij f \<equiv> bij_betw f UNIV UNIV"
   1.165  
   1.166 -text\<open>The negated case:\<close>
   1.167 +text \<open>The negated case:\<close>
   1.168  translations
   1.169 -"\<not> CONST surj f" <= "CONST range f \<noteq> CONST UNIV"
   1.170 -
   1.171 -lemma injI:
   1.172 -  assumes "\<And>x y. f x = f y \<Longrightarrow> x = y"
   1.173 -  shows "inj f"
   1.174 -  using assms unfolding inj_on_def by auto
   1.175 -
   1.176 -theorem range_ex1_eq: "inj f \<Longrightarrow> b : range f = (EX! x. b = f x)"
   1.177 -  by (unfold inj_on_def, blast)
   1.178 +  "\<not> CONST surj f" \<leftharpoondown> "CONST range f \<noteq> CONST UNIV"
   1.179  
   1.180 -lemma injD: "[| inj(f); f(x) = f(y) |] ==> x=y"
   1.181 -by (simp add: inj_on_def)
   1.182 -
   1.183 -lemma inj_on_eq_iff: "\<lbrakk>inj_on f A; x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow> (f x = f y) = (x = y)"
   1.184 -by (force simp add: inj_on_def)
   1.185 +lemma injI: "(\<And>x y. f x = f y \<Longrightarrow> x = y) \<Longrightarrow> inj f"
   1.186 +  unfolding inj_on_def by auto
   1.187  
   1.188 -lemma inj_on_cong:
   1.189 -  "(\<And> a. a : A \<Longrightarrow> f a = g a) \<Longrightarrow> inj_on f A = inj_on g A"
   1.190 -unfolding inj_on_def by auto
   1.191 -
   1.192 -lemma inj_on_strict_subset:
   1.193 -  "inj_on f B \<Longrightarrow> A \<subset> B \<Longrightarrow> f ` A \<subset> f ` B"
   1.194 +theorem range_ex1_eq: "inj f \<Longrightarrow> b \<in> range f \<longleftrightarrow> (\<exists>!x. b = f x)"
   1.195    unfolding inj_on_def by blast
   1.196  
   1.197 -lemma inj_comp:
   1.198 -  "inj f \<Longrightarrow> inj g \<Longrightarrow> inj (f \<circ> g)"
   1.199 +lemma injD: "inj f \<Longrightarrow> f x = f y \<Longrightarrow> x = y"
   1.200 +  by (simp add: inj_on_def)
   1.201 +
   1.202 +lemma inj_on_eq_iff: "inj_on f A \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> f x = f y \<longleftrightarrow> x = y"
   1.203 +  by (force simp add: inj_on_def)
   1.204 +
   1.205 +lemma inj_on_cong: "(\<And>a. a \<in> A \<Longrightarrow> f a = g a) \<Longrightarrow> inj_on f A = inj_on g A"
   1.206 +  unfolding inj_on_def by auto
   1.207 +
   1.208 +lemma inj_on_strict_subset: "inj_on f B \<Longrightarrow> A \<subset> B \<Longrightarrow> f ` A \<subset> f ` B"
   1.209 +  unfolding inj_on_def by blast
   1.210 +
   1.211 +lemma inj_comp: "inj f \<Longrightarrow> inj g \<Longrightarrow> inj (f \<circ> g)"
   1.212    by (simp add: inj_on_def)
   1.213  
   1.214  lemma inj_fun: "inj f \<Longrightarrow> inj (\<lambda>x y. f x)"
   1.215    by (simp add: inj_on_def fun_eq_iff)
   1.216  
   1.217 -lemma inj_eq: "inj f ==> (f(x) = f(y)) = (x=y)"
   1.218 -by (simp add: inj_on_eq_iff)
   1.219 +lemma inj_eq: "inj f \<Longrightarrow> f x = f y \<longleftrightarrow> x = y"
   1.220 +  by (simp add: inj_on_eq_iff)
   1.221  
   1.222  lemma inj_on_id[simp]: "inj_on id A"
   1.223    by (simp add: inj_on_def)
   1.224  
   1.225 -lemma inj_on_id2[simp]: "inj_on (%x. x) A"
   1.226 -by (simp add: inj_on_def)
   1.227 +lemma inj_on_id2[simp]: "inj_on (\<lambda>x. x) A"
   1.228 +  by (simp add: inj_on_def)
   1.229  
   1.230  lemma inj_on_Int: "inj_on f A \<or> inj_on f B \<Longrightarrow> inj_on f (A \<inter> B)"
   1.231 -unfolding inj_on_def by blast
   1.232 +  unfolding inj_on_def by blast
   1.233  
   1.234  lemma surj_id: "surj id"
   1.235 -by simp
   1.236 +  by simp
   1.237  
   1.238  lemma bij_id[simp]: "bij id"
   1.239 -by (simp add: bij_betw_def)
   1.240 +  by (simp add: bij_betw_def)
   1.241  
   1.242 -lemma bij_uminus:
   1.243 -  fixes x :: "'a :: ab_group_add"
   1.244 -  shows "bij (uminus :: 'a\<Rightarrow>'a)"
   1.245 -unfolding bij_betw_def inj_on_def
   1.246 -by (force intro: minus_minus [symmetric])
   1.247 +lemma bij_uminus: "bij (uminus :: 'a \<Rightarrow> 'a::ab_group_add)"
   1.248 +  unfolding bij_betw_def inj_on_def
   1.249 +  by (force intro: minus_minus [symmetric])
   1.250  
   1.251 -lemma inj_onI [intro?]:
   1.252 -    "(!! x y. [|  x:A;  y:A;  f(x) = f(y) |] ==> x=y) ==> inj_on f A"
   1.253 -by (simp add: inj_on_def)
   1.254 +lemma inj_onI [intro?]: "(\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> f x = f y \<Longrightarrow> x = y) \<Longrightarrow> inj_on f A"
   1.255 +  by (simp add: inj_on_def)
   1.256  
   1.257 -lemma inj_on_inverseI: "(!!x. x:A ==> g(f(x)) = x) ==> inj_on f A"
   1.258 -by (auto dest:  arg_cong [of concl: g] simp add: inj_on_def)
   1.259 -
   1.260 -lemma inj_onD: "[| inj_on f A;  f(x)=f(y);  x:A;  y:A |] ==> x=y"
   1.261 -by (unfold inj_on_def, blast)
   1.262 +lemma inj_on_inverseI: "(\<And>x. x \<in> A \<Longrightarrow> g (f x) = x) \<Longrightarrow> inj_on f A"
   1.263 +  by (auto dest:  arg_cong [of concl: g] simp add: inj_on_def)
   1.264  
   1.265 -lemma comp_inj_on:
   1.266 -     "[| inj_on f A;  inj_on g (f`A) |] ==> inj_on (g o f) A"
   1.267 -by (simp add: comp_def inj_on_def)
   1.268 +lemma inj_onD: "inj_on f A \<Longrightarrow> f x = f y \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x = y"
   1.269 +  unfolding inj_on_def by blast
   1.270  
   1.271 -lemma inj_on_imageI: "inj_on (g o f) A \<Longrightarrow> inj_on g (f ` A)"
   1.272 +lemma comp_inj_on: "inj_on f A \<Longrightarrow> inj_on g (f ` A) \<Longrightarrow> inj_on (g \<circ> f) A"
   1.273 +  by (simp add: comp_def inj_on_def)
   1.274 +
   1.275 +lemma inj_on_imageI: "inj_on (g \<circ> f) A \<Longrightarrow> inj_on g (f ` A)"
   1.276    by (auto simp add: inj_on_def)
   1.277  
   1.278 -lemma inj_on_image_iff: "\<lbrakk> ALL x:A. ALL y:A. (g(f x) = g(f y)) = (g x = g y);
   1.279 -  inj_on f A \<rbrakk> \<Longrightarrow> inj_on g (f ` A) = inj_on g A"
   1.280 -unfolding inj_on_def by blast
   1.281 +lemma inj_on_image_iff:
   1.282 +  "\<forall>x\<in>A. \<forall>y\<in>A. g (f x) = g (f y) \<longleftrightarrow> g x = g y \<Longrightarrow> inj_on f A \<Longrightarrow> inj_on g (f ` A) = inj_on g A"
   1.283 +  unfolding inj_on_def by blast
   1.284  
   1.285 -lemma inj_on_contraD: "[| inj_on f A;  ~x=y;  x:A;  y:A |] ==> ~ f(x)=f(y)"
   1.286 -unfolding inj_on_def by blast
   1.287 +lemma inj_on_contraD: "inj_on f A \<Longrightarrow> x \<noteq> y \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> f x \<noteq> f y"
   1.288 +  unfolding inj_on_def by blast
   1.289  
   1.290  lemma inj_singleton [simp]: "inj_on (\<lambda>x. {x}) A"
   1.291    by (simp add: inj_on_def)
   1.292  
   1.293  lemma inj_on_empty[iff]: "inj_on f {}"
   1.294 -by(simp add: inj_on_def)
   1.295 -
   1.296 -lemma subset_inj_on: "[| inj_on f B; A <= B |] ==> inj_on f A"
   1.297 -unfolding inj_on_def by blast
   1.298 +  by (simp add: inj_on_def)
   1.299  
   1.300 -lemma inj_on_Un:
   1.301 - "inj_on f (A Un B) =
   1.302 -  (inj_on f A & inj_on f B & f`(A-B) Int f`(B-A) = {})"
   1.303 -apply(unfold inj_on_def)
   1.304 -apply (blast intro:sym)
   1.305 -done
   1.306 +lemma subset_inj_on: "inj_on f B \<Longrightarrow> A \<subseteq> B \<Longrightarrow> inj_on f A"
   1.307 +  unfolding inj_on_def by blast
   1.308 +
   1.309 +lemma inj_on_Un: "inj_on f (A \<union> B) \<longleftrightarrow> inj_on f A \<and> inj_on f B \<and> f ` (A - B) \<inter> f ` (B - A) = {}"
   1.310 +  unfolding inj_on_def by (blast intro: sym)
   1.311  
   1.312 -lemma inj_on_insert[iff]:
   1.313 -  "inj_on f (insert a A) = (inj_on f A & f a ~: f`(A-{a}))"
   1.314 -apply(unfold inj_on_def)
   1.315 -apply (blast intro:sym)
   1.316 -done
   1.317 +lemma inj_on_insert [iff]: "inj_on f (insert a A) \<longleftrightarrow> inj_on f A \<and> f a \<notin> f ` (A - {a})"
   1.318 +  unfolding inj_on_def by (blast intro: sym)
   1.319 +
   1.320 +lemma inj_on_diff: "inj_on f A \<Longrightarrow> inj_on f (A - B)"
   1.321 +  unfolding inj_on_def by blast
   1.322  
   1.323 -lemma inj_on_diff: "inj_on f A ==> inj_on f (A-B)"
   1.324 -apply(unfold inj_on_def)
   1.325 -apply (blast)
   1.326 -done
   1.327 +lemma comp_inj_on_iff: "inj_on f A \<Longrightarrow> inj_on f' (f ` A) \<longleftrightarrow> inj_on (f' \<circ> f) A"
   1.328 +  by (auto simp add: comp_inj_on inj_on_def)
   1.329  
   1.330 -lemma comp_inj_on_iff:
   1.331 -  "inj_on f A \<Longrightarrow> inj_on f' (f ` A) \<longleftrightarrow> inj_on (f' o f) A"
   1.332 -by(auto simp add: comp_inj_on inj_on_def)
   1.333 -
   1.334 -lemma inj_on_imageI2:
   1.335 -  "inj_on (f' o f) A \<Longrightarrow> inj_on f A"
   1.336 -by(auto simp add: comp_inj_on inj_on_def)
   1.337 +lemma inj_on_imageI2: "inj_on (f' \<circ> f) A \<Longrightarrow> inj_on f A"
   1.338 +  by (auto simp add: comp_inj_on inj_on_def)
   1.339  
   1.340  lemma inj_img_insertE:
   1.341    assumes "inj_on f A"
   1.342 -  assumes "x \<notin> B" and "insert x B = f ` A"
   1.343 -  obtains x' A' where "x' \<notin> A'" and "A = insert x' A'"
   1.344 -    and "x = f x'" and "B = f ` A'"
   1.345 +  assumes "x \<notin> B"
   1.346 +    and "insert x B = f ` A"
   1.347 +  obtains x' A' where "x' \<notin> A'" and "A = insert x' A'" and "x = f x'" and "B = f ` A'"
   1.348  proof -
   1.349    from assms have "x \<in> f ` A" by auto
   1.350    then obtain x' where *: "x' \<in> A" "x = f x'" by auto
   1.351 -  then have "A = insert x' (A - {x'})" by auto
   1.352 -  with assms * have "B = f ` (A - {x'})"
   1.353 -    by (auto dest: inj_on_contraD)
   1.354 +  then have A: "A = insert x' (A - {x'})" by auto
   1.355 +  with assms * have B: "B = f ` (A - {x'})" by (auto dest: inj_on_contraD)
   1.356    have "x' \<notin> A - {x'}" by simp
   1.357 -  from \<open>x' \<notin> A - {x'}\<close> \<open>A = insert x' (A - {x'})\<close> \<open>x = f x'\<close> \<open>B = image f (A - {x'})\<close>
   1.358 -  show ?thesis ..
   1.359 +  from this A \<open>x = f x'\<close> B show ?thesis ..
   1.360  qed
   1.361  
   1.362  lemma linorder_injI:
   1.363 -  assumes hyp: "\<And>x y. x < (y::'a::linorder) \<Longrightarrow> f x \<noteq> f y"
   1.364 +  assumes hyp: "\<And>x y::'a::linorder. x < y \<Longrightarrow> f x \<noteq> f y"
   1.365    shows "inj f"
   1.366    \<comment> \<open>Courtesy of Stephan Merz\<close>
   1.367  proof (rule inj_onI)
   1.368 @@ -307,7 +277,9 @@
   1.369  lemma surj_def: "surj f \<longleftrightarrow> (\<forall>y. \<exists>x. y = f x)"
   1.370    by auto
   1.371  
   1.372 -lemma surjI: assumes *: "\<And> x. g (f x) = x" shows "surj g"
   1.373 +lemma surjI:
   1.374 +  assumes *: "\<And> x. g (f x) = x"
   1.375 +  shows "surj g"
   1.376    using *[symmetric] by auto
   1.377  
   1.378  lemma surjD: "surj f \<Longrightarrow> \<exists>x. y = f x"
   1.379 @@ -316,15 +288,17 @@
   1.380  lemma surjE: "surj f \<Longrightarrow> (\<And>x. y = f x \<Longrightarrow> C) \<Longrightarrow> C"
   1.381    by (simp add: surj_def, blast)
   1.382  
   1.383 -lemma comp_surj: "[| surj f;  surj g |] ==> surj (g o f)"
   1.384 -apply (simp add: comp_def surj_def, clarify)
   1.385 -apply (drule_tac x = y in spec, clarify)
   1.386 -apply (drule_tac x = x in spec, blast)
   1.387 -done
   1.388 +lemma comp_surj: "surj f \<Longrightarrow> surj g \<Longrightarrow> surj (g \<circ> f)"
   1.389 +  apply (simp add: comp_def surj_def)
   1.390 +  apply clarify
   1.391 +  apply (drule_tac x = y in spec)
   1.392 +  apply clarify
   1.393 +  apply (drule_tac x = x in spec)
   1.394 +  apply blast
   1.395 +  done
   1.396  
   1.397 -lemma bij_betw_imageI:
   1.398 -  "\<lbrakk> inj_on f A; f ` A = B \<rbrakk> \<Longrightarrow> bij_betw f A B"
   1.399 -unfolding bij_betw_def by clarify
   1.400 +lemma bij_betw_imageI: "inj_on f A \<Longrightarrow> f ` A = B \<Longrightarrow> bij_betw f A B"
   1.401 +  unfolding bij_betw_def by clarify
   1.402  
   1.403  lemma bij_betw_imp_surj_on: "bij_betw f A B \<Longrightarrow> f ` A = B"
   1.404    unfolding bij_betw_def by clarify
   1.405 @@ -332,122 +306,119 @@
   1.406  lemma bij_betw_imp_surj: "bij_betw f A UNIV \<Longrightarrow> surj f"
   1.407    unfolding bij_betw_def by auto
   1.408  
   1.409 -lemma bij_betw_empty1:
   1.410 -  assumes "bij_betw f {} A"
   1.411 -  shows "A = {}"
   1.412 -using assms unfolding bij_betw_def by blast
   1.413 +lemma bij_betw_empty1: "bij_betw f {} A \<Longrightarrow> A = {}"
   1.414 +  unfolding bij_betw_def by blast
   1.415  
   1.416 -lemma bij_betw_empty2:
   1.417 -  assumes "bij_betw f A {}"
   1.418 -  shows "A = {}"
   1.419 -using assms unfolding bij_betw_def by blast
   1.420 +lemma bij_betw_empty2: "bij_betw f A {} \<Longrightarrow> A = {}"
   1.421 +  unfolding bij_betw_def by blast
   1.422  
   1.423 -lemma inj_on_imp_bij_betw:
   1.424 -  "inj_on f A \<Longrightarrow> bij_betw f A (f ` A)"
   1.425 -unfolding bij_betw_def by simp
   1.426 +lemma inj_on_imp_bij_betw: "inj_on f A \<Longrightarrow> bij_betw f A (f ` A)"
   1.427 +  unfolding bij_betw_def by simp
   1.428  
   1.429  lemma bij_def: "bij f \<longleftrightarrow> inj f \<and> surj f"
   1.430    unfolding bij_betw_def ..
   1.431  
   1.432 -lemma bijI: "[| inj f; surj f |] ==> bij f"
   1.433 -by (simp add: bij_def)
   1.434 +lemma bijI: "inj f \<Longrightarrow> surj f \<Longrightarrow> bij f"
   1.435 +  by (simp add: bij_def)
   1.436  
   1.437 -lemma bij_is_inj: "bij f ==> inj f"
   1.438 -by (simp add: bij_def)
   1.439 +lemma bij_is_inj: "bij f \<Longrightarrow> inj f"
   1.440 +  by (simp add: bij_def)
   1.441  
   1.442 -lemma bij_is_surj: "bij f ==> surj f"
   1.443 -by (simp add: bij_def)
   1.444 +lemma bij_is_surj: "bij f \<Longrightarrow> surj f"
   1.445 +  by (simp add: bij_def)
   1.446  
   1.447  lemma bij_betw_imp_inj_on: "bij_betw f A B \<Longrightarrow> inj_on f A"
   1.448 -by (simp add: bij_betw_def)
   1.449 +  by (simp add: bij_betw_def)
   1.450  
   1.451 -lemma bij_betw_trans:
   1.452 -  "bij_betw f A B \<Longrightarrow> bij_betw g B C \<Longrightarrow> bij_betw (g o f) A C"
   1.453 -by(auto simp add:bij_betw_def comp_inj_on)
   1.454 +lemma bij_betw_trans: "bij_betw f A B \<Longrightarrow> bij_betw g B C \<Longrightarrow> bij_betw (g \<circ> f) A C"
   1.455 +  by (auto simp add:bij_betw_def comp_inj_on)
   1.456  
   1.457 -lemma bij_comp: "bij f \<Longrightarrow> bij g \<Longrightarrow> bij (g o f)"
   1.458 +lemma bij_comp: "bij f \<Longrightarrow> bij g \<Longrightarrow> bij (g \<circ> f)"
   1.459    by (rule bij_betw_trans)
   1.460  
   1.461 -lemma bij_betw_comp_iff:
   1.462 -  "bij_betw f A A' \<Longrightarrow> bij_betw f' A' A'' \<longleftrightarrow> bij_betw (f' o f) A A''"
   1.463 -by(auto simp add: bij_betw_def inj_on_def)
   1.464 +lemma bij_betw_comp_iff: "bij_betw f A A' \<Longrightarrow> bij_betw f' A' A'' \<longleftrightarrow> bij_betw (f' \<circ> f) A A''"
   1.465 +  by (auto simp add: bij_betw_def inj_on_def)
   1.466  
   1.467  lemma bij_betw_comp_iff2:
   1.468 -  assumes BIJ: "bij_betw f' A' A''" and IM: "f ` A \<le> A'"
   1.469 -  shows "bij_betw f A A' \<longleftrightarrow> bij_betw (f' o f) A A''"
   1.470 -using assms
   1.471 -proof(auto simp add: bij_betw_comp_iff)
   1.472 +  assumes bij: "bij_betw f' A' A''"
   1.473 +    and img: "f ` A \<le> A'"
   1.474 +  shows "bij_betw f A A' \<longleftrightarrow> bij_betw (f' \<circ> f) A A''"
   1.475 +  using assms
   1.476 +proof (auto simp add: bij_betw_comp_iff)
   1.477    assume *: "bij_betw (f' \<circ> f) A A''"
   1.478 -  thus "bij_betw f A A'"
   1.479 -  using IM
   1.480 -  proof(auto simp add: bij_betw_def)
   1.481 +  then show "bij_betw f A A'"
   1.482 +    using img
   1.483 +  proof (auto simp add: bij_betw_def)
   1.484      assume "inj_on (f' \<circ> f) A"
   1.485 -    thus "inj_on f A" using inj_on_imageI2 by blast
   1.486 +    then show "inj_on f A" using inj_on_imageI2 by blast
   1.487    next
   1.488 -    fix a' assume **: "a' \<in> A'"
   1.489 -    hence "f' a' \<in> A''" using BIJ unfolding bij_betw_def by auto
   1.490 -    then obtain a where 1: "a \<in> A \<and> f'(f a) = f' a'" using *
   1.491 -    unfolding bij_betw_def by force
   1.492 -    hence "f a \<in> A'" using IM by auto
   1.493 -    hence "f a = a'" using BIJ ** 1 unfolding bij_betw_def inj_on_def by auto
   1.494 -    thus "a' \<in> f ` A" using 1 by auto
   1.495 +    fix a'
   1.496 +    assume **: "a' \<in> A'"
   1.497 +    then have "f' a' \<in> A''" using bij unfolding bij_betw_def by auto
   1.498 +    then obtain a where 1: "a \<in> A \<and> f'(f a) = f' a'"
   1.499 +      using * unfolding bij_betw_def by force
   1.500 +    then have "f a \<in> A'" using img by auto
   1.501 +    then have "f a = a'"
   1.502 +      using bij ** 1 unfolding bij_betw_def inj_on_def by auto
   1.503 +    then show "a' \<in> f ` A"
   1.504 +      using 1 by auto
   1.505    qed
   1.506  qed
   1.507  
   1.508 -lemma bij_betw_inv: assumes "bij_betw f A B" shows "EX g. bij_betw g B A"
   1.509 +lemma bij_betw_inv:
   1.510 +  assumes "bij_betw f A B"
   1.511 +  shows "\<exists>g. bij_betw g B A"
   1.512  proof -
   1.513    have i: "inj_on f A" and s: "f ` A = B"
   1.514 -    using assms by(auto simp:bij_betw_def)
   1.515 -  let ?P = "%b a. a:A \<and> f a = b" let ?g = "%b. The (?P b)"
   1.516 -  { fix a b assume P: "?P b a"
   1.517 -    hence ex1: "\<exists>a. ?P b a" using s by blast
   1.518 -    hence uex1: "\<exists>!a. ?P b a" by(blast dest:inj_onD[OF i])
   1.519 -    hence " ?g b = a" using the1_equality[OF uex1, OF P] P by simp
   1.520 -  } note g = this
   1.521 +    using assms by (auto simp: bij_betw_def)
   1.522 +  let ?P = "\<lambda>b a. a \<in> A \<and> f a = b"
   1.523 +  let ?g = "\<lambda>b. The (?P b)"
   1.524 +  have g: "?g b = a" if P: "?P b a" for a b
   1.525 +  proof -
   1.526 +    from that have ex1: "\<exists>a. ?P b a" using s by blast
   1.527 +    then have uex1: "\<exists>!a. ?P b a" by (blast dest:inj_onD[OF i])
   1.528 +    then show ?thesis using the1_equality[OF uex1, OF P] P by simp
   1.529 +  qed
   1.530    have "inj_on ?g B"
   1.531 -  proof(rule inj_onI)
   1.532 -    fix x y assume "x:B" "y:B" "?g x = ?g y"
   1.533 -    from s \<open>x:B\<close> obtain a1 where a1: "?P x a1" by blast
   1.534 -    from s \<open>y:B\<close> obtain a2 where a2: "?P y a2" by blast
   1.535 -    from g[OF a1] a1 g[OF a2] a2 \<open>?g x = ?g y\<close> show "x=y" by simp
   1.536 +  proof (rule inj_onI)
   1.537 +    fix x y
   1.538 +    assume "x \<in> B" "y \<in> B" "?g x = ?g y"
   1.539 +    from s \<open>x \<in> B\<close> obtain a1 where a1: "?P x a1" by blast
   1.540 +    from s \<open>y \<in> B\<close> obtain a2 where a2: "?P y a2" by blast
   1.541 +    from g [OF a1] a1 g [OF a2] a2 \<open>?g x = ?g y\<close> show "x = y" by simp
   1.542    qed
   1.543    moreover have "?g ` B = A"
   1.544 -  proof(auto simp: image_def)
   1.545 -    fix b assume "b:B"
   1.546 +  proof (auto simp: image_def)
   1.547 +    fix b
   1.548 +    assume "b \<in> B"
   1.549      with s obtain a where P: "?P b a" by blast
   1.550 -    thus "?g b \<in> A" using g[OF P] by auto
   1.551 +    then show "?g b \<in> A" using g[OF P] by auto
   1.552    next
   1.553 -    fix a assume "a:A"
   1.554 +    fix a
   1.555 +    assume "a \<in> A"
   1.556      then obtain b where P: "?P b a" using s by blast
   1.557 -    then have "b:B" using s by blast
   1.558 +    then have "b \<in> B" using s by blast
   1.559      with g[OF P] show "\<exists>b\<in>B. a = ?g b" by blast
   1.560    qed
   1.561 -  ultimately show ?thesis by(auto simp:bij_betw_def)
   1.562 +  ultimately show ?thesis by (auto simp: bij_betw_def)
   1.563  qed
   1.564  
   1.565 -lemma bij_betw_cong:
   1.566 -  "(\<And> a. a \<in> A \<Longrightarrow> f a = g a) \<Longrightarrow> bij_betw f A A' = bij_betw g A A'"
   1.567 -unfolding bij_betw_def inj_on_def by force
   1.568 +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'"
   1.569 +  unfolding bij_betw_def inj_on_def by force
   1.570  
   1.571 -lemma bij_betw_id[intro, simp]:
   1.572 -  "bij_betw id A A"
   1.573 -unfolding bij_betw_def id_def by auto
   1.574 +lemma bij_betw_id[intro, simp]: "bij_betw id A A"
   1.575 +  unfolding bij_betw_def id_def by auto
   1.576  
   1.577 -lemma bij_betw_id_iff:
   1.578 -  "bij_betw id A B \<longleftrightarrow> A = B"
   1.579 -by(auto simp add: bij_betw_def)
   1.580 +lemma bij_betw_id_iff: "bij_betw id A B \<longleftrightarrow> A = B"
   1.581 +  by (auto simp add: bij_betw_def)
   1.582  
   1.583  lemma bij_betw_combine:
   1.584    assumes "bij_betw f A B" "bij_betw f C D" "B \<inter> D = {}"
   1.585    shows "bij_betw f (A \<union> C) (B \<union> D)"
   1.586    using assms unfolding bij_betw_def inj_on_Un image_Un by auto
   1.587  
   1.588 -lemma bij_betw_subset:
   1.589 -  assumes BIJ: "bij_betw f A A'" and
   1.590 -          SUB: "B \<le> A" and IM: "f ` B = B'"
   1.591 -  shows "bij_betw f B B'"
   1.592 -using assms
   1.593 -by(unfold bij_betw_def inj_on_def, auto simp add: inj_on_def)
   1.594 +lemma bij_betw_subset: "bij_betw f A A' \<Longrightarrow> B \<le> A \<Longrightarrow> f ` B = B' \<Longrightarrow> bij_betw f B B'"
   1.595 +  by (auto simp add: bij_betw_def inj_on_def)
   1.596  
   1.597  lemma bij_pointE:
   1.598    assumes "bij f"
   1.599 @@ -460,85 +431,77 @@
   1.600    with that show thesis by blast
   1.601  qed
   1.602  
   1.603 -lemma surj_image_vimage_eq: "surj f ==> f ` (f -` A) = A"
   1.604 -by simp
   1.605 +lemma surj_image_vimage_eq: "surj f \<Longrightarrow> f ` (f -` A) = A"
   1.606 +  by simp
   1.607  
   1.608  lemma surj_vimage_empty:
   1.609 -  assumes "surj f" shows "f -` A = {} \<longleftrightarrow> A = {}"
   1.610 -  using surj_image_vimage_eq[OF \<open>surj f\<close>, of A]
   1.611 +  assumes "surj f"
   1.612 +  shows "f -` A = {} \<longleftrightarrow> A = {}"
   1.613 +  using surj_image_vimage_eq [OF \<open>surj f\<close>, of A]
   1.614    by (intro iffI) fastforce+
   1.615  
   1.616 -lemma inj_vimage_image_eq: "inj f ==> f -` (f ` A) = A"
   1.617 -by (simp add: inj_on_def, blast)
   1.618 +lemma inj_vimage_image_eq: "inj f \<Longrightarrow> f -` (f ` A) = A"
   1.619 +  unfolding inj_on_def by blast
   1.620  
   1.621 -lemma vimage_subsetD: "surj f ==> f -` B <= A ==> B <= f ` A"
   1.622 -by (blast intro: sym)
   1.623 +lemma vimage_subsetD: "surj f \<Longrightarrow> f -` B \<subseteq> A \<Longrightarrow> B \<subseteq> f ` A"
   1.624 +  by (blast intro: sym)
   1.625  
   1.626 -lemma vimage_subsetI: "inj f ==> B <= f ` A ==> f -` B <= A"
   1.627 -by (unfold inj_on_def, blast)
   1.628 +lemma vimage_subsetI: "inj f \<Longrightarrow> B \<subseteq> f ` A \<Longrightarrow> f -` B \<subseteq> A"
   1.629 +  unfolding inj_on_def by blast
   1.630  
   1.631 -lemma vimage_subset_eq: "bij f ==> (f -` B <= A) = (B <= f ` A)"
   1.632 -apply (unfold bij_def)
   1.633 -apply (blast del: subsetI intro: vimage_subsetI vimage_subsetD)
   1.634 -done
   1.635 +lemma vimage_subset_eq: "bij f \<Longrightarrow> f -` B \<subseteq> A \<longleftrightarrow> B \<subseteq> f ` A"
   1.636 +  unfolding bij_def by (blast del: subsetI intro: vimage_subsetI vimage_subsetD)
   1.637  
   1.638 -lemma inj_on_image_eq_iff: "\<lbrakk> inj_on f C; A \<subseteq> C; B \<subseteq> C \<rbrakk> \<Longrightarrow> f ` A = f ` B \<longleftrightarrow> A = B"
   1.639 -by(fastforce simp add: inj_on_def)
   1.640 +lemma inj_on_image_eq_iff: "inj_on f C \<Longrightarrow> A \<subseteq> C \<Longrightarrow> B \<subseteq> C \<Longrightarrow> f ` A = f ` B \<longleftrightarrow> A = B"
   1.641 +  by (fastforce simp add: inj_on_def)
   1.642  
   1.643  lemma inj_on_Un_image_eq_iff: "inj_on f (A \<union> B) \<Longrightarrow> f ` A = f ` B \<longleftrightarrow> A = B"
   1.644 -by(erule inj_on_image_eq_iff) simp_all
   1.645 +  by (erule inj_on_image_eq_iff) simp_all
   1.646  
   1.647 -lemma inj_on_image_Int:
   1.648 -   "[| inj_on f C;  A<=C;  B<=C |] ==> f`(A Int B) = f`A Int f`B"
   1.649 -  by (simp add: inj_on_def, blast)
   1.650 +lemma inj_on_image_Int: "inj_on f C \<Longrightarrow> A \<subseteq> C \<Longrightarrow> B \<subseteq> C \<Longrightarrow> f ` (A \<inter> B) = f ` A \<inter> f ` B"
   1.651 +  unfolding inj_on_def by blast
   1.652 +
   1.653 +lemma inj_on_image_set_diff: "inj_on f C \<Longrightarrow> A - B \<subseteq> C \<Longrightarrow> B \<subseteq> C \<Longrightarrow> f ` (A - B) = f ` A - f ` B"
   1.654 +  unfolding inj_on_def by blast
   1.655  
   1.656 -lemma inj_on_image_set_diff:
   1.657 -   "[| inj_on f C;  A-B \<subseteq> C;  B \<subseteq> C |] ==> f`(A-B) = f`A - f`B"
   1.658 -  by (simp add: inj_on_def, blast)
   1.659 +lemma image_Int: "inj f \<Longrightarrow> f ` (A \<inter> B) = f ` A \<inter> f ` B"
   1.660 +  unfolding inj_on_def by blast
   1.661  
   1.662 -lemma image_Int: "inj f ==> f`(A Int B) = f`A Int f`B"
   1.663 -  by (simp add: inj_on_def, blast)
   1.664 +lemma image_set_diff: "inj f \<Longrightarrow> f ` (A - B) = f ` A - f ` B"
   1.665 +  unfolding inj_on_def by blast
   1.666  
   1.667 -lemma image_set_diff: "inj f ==> f`(A-B) = f`A - f`B"
   1.668 -by (simp add: inj_on_def, blast)
   1.669 -
   1.670 -lemma inj_on_image_mem_iff: "\<lbrakk>inj_on f B; a \<in> B; A \<subseteq> B\<rbrakk> \<Longrightarrow> f a \<in> f`A \<longleftrightarrow> a \<in> A"
   1.671 +lemma inj_on_image_mem_iff: "inj_on f B \<Longrightarrow> a \<in> B \<Longrightarrow> A \<subseteq> B \<Longrightarrow> f a \<in> f ` A \<longleftrightarrow> a \<in> A"
   1.672    by (auto simp: inj_on_def)
   1.673  
   1.674  (*FIXME DELETE*)
   1.675 -lemma inj_on_image_mem_iff_alt: "inj_on f B \<Longrightarrow> A \<subseteq> B \<Longrightarrow> f a \<in> f`A \<Longrightarrow> a \<in> B \<Longrightarrow> a \<in> A"
   1.676 +lemma inj_on_image_mem_iff_alt: "inj_on f B \<Longrightarrow> A \<subseteq> B \<Longrightarrow> f a \<in> f ` A \<Longrightarrow> a \<in> B \<Longrightarrow> a \<in> A"
   1.677    by (blast dest: inj_onD)
   1.678  
   1.679 -lemma inj_image_mem_iff: "inj f \<Longrightarrow> f a \<in> f`A \<longleftrightarrow> a \<in> A"
   1.680 +lemma inj_image_mem_iff: "inj f \<Longrightarrow> f a \<in> f ` A \<longleftrightarrow> a \<in> A"
   1.681    by (blast dest: injD)
   1.682  
   1.683 -lemma inj_image_subset_iff: "inj f ==> (f`A <= f`B) = (A<=B)"
   1.684 +lemma inj_image_subset_iff: "inj f \<Longrightarrow> f ` A \<subseteq> f ` B \<longleftrightarrow> A \<subseteq> B"
   1.685    by (blast dest: injD)
   1.686  
   1.687 -lemma inj_image_eq_iff: "inj f ==> (f`A = f`B) = (A = B)"
   1.688 +lemma inj_image_eq_iff: "inj f \<Longrightarrow> f ` A = f ` B \<longleftrightarrow> A = B"
   1.689    by (blast dest: injD)
   1.690  
   1.691 -lemma surj_Compl_image_subset: "surj f ==> -(f`A) <= f`(-A)"
   1.692 -by auto
   1.693 -
   1.694 -lemma inj_image_Compl_subset: "inj f ==> f`(-A) <= -(f`A)"
   1.695 -by (auto simp add: inj_on_def)
   1.696 +lemma surj_Compl_image_subset: "surj f \<Longrightarrow> - (f ` A) \<subseteq> f ` (- A)"
   1.697 +  by auto
   1.698  
   1.699 -lemma bij_image_Compl_eq: "bij f ==> f`(-A) = -(f`A)"
   1.700 -apply (simp add: bij_def)
   1.701 -apply (rule equalityI)
   1.702 -apply (simp_all (no_asm_simp) add: inj_image_Compl_subset surj_Compl_image_subset)
   1.703 -done
   1.704 +lemma inj_image_Compl_subset: "inj f \<Longrightarrow> f ` (- A) \<subseteq> - (f ` A)"
   1.705 +  by (auto simp add: inj_on_def)
   1.706 +
   1.707 +lemma bij_image_Compl_eq: "bij f \<Longrightarrow> f ` (- A) = - (f ` A)"
   1.708 +  by (simp add: bij_def inj_image_Compl_subset surj_Compl_image_subset equalityI)
   1.709  
   1.710  lemma inj_vimage_singleton: "inj f \<Longrightarrow> f -` {a} \<subseteq> {THE x. f x = a}"
   1.711 -  \<comment> \<open>The inverse image of a singleton under an injective function
   1.712 -         is included in a singleton.\<close>
   1.713 +  \<comment> \<open>The inverse image of a singleton under an injective function is included in a singleton.\<close>
   1.714    apply (auto simp add: inj_on_def)
   1.715    apply (blast intro: the_equality [symmetric])
   1.716    done
   1.717  
   1.718 -lemma inj_on_vimage_singleton:
   1.719 -  "inj_on f A \<Longrightarrow> f -` {a} \<inter> A \<subseteq> {THE x. x \<in> A \<and> f x = a}"
   1.720 +lemma inj_on_vimage_singleton: "inj_on f A \<Longrightarrow> f -` {a} \<inter> A \<subseteq> {THE x. x \<in> A \<and> f x = a}"
   1.721    by (auto simp add: inj_on_def intro: the_equality [symmetric])
   1.722  
   1.723  lemma (in ordered_ab_group_add) inj_uminus[simp, intro]: "inj_on uminus A"
   1.724 @@ -548,84 +511,92 @@
   1.725    by (auto intro!: inj_onI dest: strict_mono_eq)
   1.726  
   1.727  lemma bij_betw_byWitness:
   1.728 -assumes LEFT: "\<forall>a \<in> A. f'(f a) = a" and
   1.729 -        RIGHT: "\<forall>a' \<in> A'. f(f' a') = a'" and
   1.730 -        IM1: "f ` A \<le> A'" and IM2: "f' ` A' \<le> A"
   1.731 -shows "bij_betw f A A'"
   1.732 -using assms
   1.733 -proof(unfold bij_betw_def inj_on_def, safe)
   1.734 -  fix a b assume *: "a \<in> A" "b \<in> A" and **: "f a = f b"
   1.735 -  have "a = f'(f a) \<and> b = f'(f b)" using * LEFT by simp
   1.736 +  assumes left: "\<forall>a \<in> A. f' (f a) = a"
   1.737 +    and right: "\<forall>a' \<in> A'. f (f' a') = a'"
   1.738 +    and "f ` A \<le> A'"
   1.739 +    and img2: "f' ` A' \<le> A"
   1.740 +  shows "bij_betw f A A'"
   1.741 +  using assms
   1.742 +proof (unfold bij_betw_def inj_on_def, safe)
   1.743 +  fix a b
   1.744 +  assume *: "a \<in> A" "b \<in> A" and **: "f a = f b"
   1.745 +  have "a = f' (f a) \<and> b = f'(f b)" using * left by simp
   1.746    with ** show "a = b" by simp
   1.747  next
   1.748    fix a' assume *: "a' \<in> A'"
   1.749 -  hence "f' a' \<in> A" using IM2 by blast
   1.750 +  hence "f' a' \<in> A" using img2 by blast
   1.751    moreover
   1.752 -  have "a' = f(f' a')" using * RIGHT by simp
   1.753 +  have "a' = f (f' a')" using * right by simp
   1.754    ultimately show "a' \<in> f ` A" by blast
   1.755  qed
   1.756  
   1.757  corollary notIn_Un_bij_betw:
   1.758 -assumes NIN: "b \<notin> A" and NIN': "f b \<notin> A'" and
   1.759 -       BIJ: "bij_betw f A A'"
   1.760 -shows "bij_betw f (A \<union> {b}) (A' \<union> {f b})"
   1.761 -proof-
   1.762 +  assumes "b \<notin> A"
   1.763 +    and "f b \<notin> A'"
   1.764 +    and "bij_betw f A A'"
   1.765 +  shows "bij_betw f (A \<union> {b}) (A' \<union> {f b})"
   1.766 +proof -
   1.767    have "bij_betw f {b} {f b}"
   1.768 -  unfolding bij_betw_def inj_on_def by simp
   1.769 +    unfolding bij_betw_def inj_on_def by simp
   1.770    with assms show ?thesis
   1.771 -  using bij_betw_combine[of f A A' "{b}" "{f b}"] by blast
   1.772 +    using bij_betw_combine[of f A A' "{b}" "{f b}"] by blast
   1.773  qed
   1.774  
   1.775  lemma notIn_Un_bij_betw3:
   1.776 -assumes NIN: "b \<notin> A" and NIN': "f b \<notin> A'"
   1.777 -shows "bij_betw f A A' = bij_betw f (A \<union> {b}) (A' \<union> {f b})"
   1.778 +  assumes "b \<notin> A"
   1.779 +    and "f b \<notin> A'"
   1.780 +  shows "bij_betw f A A' = bij_betw f (A \<union> {b}) (A' \<union> {f b})"
   1.781  proof
   1.782    assume "bij_betw f A A'"
   1.783 -  thus "bij_betw f (A \<union> {b}) (A' \<union> {f b})"
   1.784 -  using assms notIn_Un_bij_betw[of b A f A'] by blast
   1.785 +  then show "bij_betw f (A \<union> {b}) (A' \<union> {f b})"
   1.786 +    using assms notIn_Un_bij_betw [of b A f A'] by blast
   1.787  next
   1.788    assume *: "bij_betw f (A \<union> {b}) (A' \<union> {f b})"
   1.789    have "f ` A = A'"
   1.790 -  proof(auto)
   1.791 -    fix a assume **: "a \<in> A"
   1.792 -    hence "f a \<in> A' \<union> {f b}" using * unfolding bij_betw_def by blast
   1.793 +  proof auto
   1.794 +    fix a
   1.795 +    assume **: "a \<in> A"
   1.796 +    then have "f a \<in> A' \<union> {f b}"
   1.797 +      using * unfolding bij_betw_def by blast
   1.798      moreover
   1.799 -    {assume "f a = f b"
   1.800 -     hence "a = b" using * ** unfolding bij_betw_def inj_on_def by blast
   1.801 -     with NIN ** have False by blast
   1.802 -    }
   1.803 +    have False if "f a = f b"
   1.804 +    proof -
   1.805 +      have "a = b" using * ** that unfolding bij_betw_def inj_on_def by blast
   1.806 +      with \<open>b \<notin> A\<close> ** show ?thesis by blast
   1.807 +    qed
   1.808      ultimately show "f a \<in> A'" by blast
   1.809    next
   1.810 -    fix a' assume **: "a' \<in> A'"
   1.811 -    hence "a' \<in> f`(A \<union> {b})"
   1.812 -    using * by (auto simp add: bij_betw_def)
   1.813 +    fix a'
   1.814 +    assume **: "a' \<in> A'"
   1.815 +    then have "a' \<in> f ` (A \<union> {b})"
   1.816 +      using * by (auto simp add: bij_betw_def)
   1.817      then obtain a where 1: "a \<in> A \<union> {b} \<and> f a = a'" by blast
   1.818      moreover
   1.819 -    {assume "a = b" with 1 ** NIN' have False by blast
   1.820 -    }
   1.821 +    have False if "a = b" using 1 ** \<open>f b \<notin> A'\<close> that by blast
   1.822      ultimately have "a \<in> A" by blast
   1.823      with 1 show "a' \<in> f ` A" by blast
   1.824    qed
   1.825 -  thus "bij_betw f A A'" using * bij_betw_subset[of f "A \<union> {b}" _ A] by blast
   1.826 +  then show "bij_betw f A A'"
   1.827 +    using * bij_betw_subset[of f "A \<union> {b}" _ A] by blast
   1.828  qed
   1.829  
   1.830  
   1.831 -subsection\<open>Function Updating\<close>
   1.832 +subsection \<open>Function Updating\<close>
   1.833  
   1.834 -definition fun_upd :: "('a => 'b) => 'a => 'b => ('a => 'b)" where
   1.835 -  "fun_upd f a b == % x. if x=a then b else f x"
   1.836 +definition fun_upd :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)"
   1.837 +  where "fun_upd f a b \<equiv> \<lambda>x. if x = a then b else f x"
   1.838  
   1.839  nonterminal updbinds and updbind
   1.840  
   1.841  syntax
   1.842 -  "_updbind" :: "['a, 'a] => updbind"             ("(2_ :=/ _)")
   1.843 -  ""         :: "updbind => updbinds"             ("_")
   1.844 -  "_updbinds":: "[updbind, updbinds] => updbinds" ("_,/ _")
   1.845 -  "_Update"  :: "['a, updbinds] => 'a"            ("_/'((_)')" [1000, 0] 900)
   1.846 +  "_updbind" :: "'a \<Rightarrow> 'a \<Rightarrow> updbind"             ("(2_ :=/ _)")
   1.847 +  ""         :: "updbind \<Rightarrow> updbinds"             ("_")
   1.848 +  "_updbinds":: "updbind \<Rightarrow> updbinds \<Rightarrow> updbinds" ("_,/ _")
   1.849 +  "_Update"  :: "'a \<Rightarrow> updbinds \<Rightarrow> 'a"            ("_/'((_)')" [1000, 0] 900)
   1.850  
   1.851  translations
   1.852 -  "_Update f (_updbinds b bs)" == "_Update (_Update f b) bs"
   1.853 -  "f(x:=y)" == "CONST fun_upd f x y"
   1.854 +  "_Update f (_updbinds b bs)" \<rightleftharpoons> "_Update (_Update f b) bs"
   1.855 +  "f(x:=y)" \<rightleftharpoons> "CONST fun_upd f x y"
   1.856  
   1.857  (* Hint: to define the sum of two functions (or maps), use case_sum.
   1.858           A nice infix syntax could be defined by
   1.859 @@ -633,69 +604,69 @@
   1.860    case_sum  (infixr "'(+')"80)
   1.861  *)
   1.862  
   1.863 -lemma fun_upd_idem_iff: "(f(x:=y) = f) = (f x = y)"
   1.864 -apply (simp add: fun_upd_def, safe)
   1.865 -apply (erule subst)
   1.866 -apply (rule_tac [2] ext, auto)
   1.867 -done
   1.868 +lemma fun_upd_idem_iff: "f(x:=y) = f \<longleftrightarrow> f x = y"
   1.869 +  unfolding fun_upd_def
   1.870 +  apply safe
   1.871 +  apply (erule subst)
   1.872 +  apply (rule_tac [2] ext)
   1.873 +  apply auto
   1.874 +  done
   1.875  
   1.876 -lemma fun_upd_idem: "f x = y ==> f(x:=y) = f"
   1.877 +lemma fun_upd_idem: "f x = y \<Longrightarrow> f(x := y) = f"
   1.878    by (simp only: fun_upd_idem_iff)
   1.879  
   1.880  lemma fun_upd_triv [iff]: "f(x := f x) = f"
   1.881    by (simp only: fun_upd_idem)
   1.882  
   1.883 -lemma fun_upd_apply [simp]: "(f(x:=y))z = (if z=x then y else f z)"
   1.884 -by (simp add: fun_upd_def)
   1.885 +lemma fun_upd_apply [simp]: "(f(x := y)) z = (if z = x then y else f z)"
   1.886 +  by (simp add: fun_upd_def)
   1.887  
   1.888 -(* fun_upd_apply supersedes these two,   but they are useful
   1.889 +(* fun_upd_apply supersedes these two, but they are useful
   1.890     if fun_upd_apply is intentionally removed from the simpset *)
   1.891 -lemma fun_upd_same: "(f(x:=y)) x = y"
   1.892 -by simp
   1.893 +lemma fun_upd_same: "(f(x := y)) x = y"
   1.894 +  by simp
   1.895  
   1.896 -lemma fun_upd_other: "z~=x ==> (f(x:=y)) z = f z"
   1.897 -by simp
   1.898 -
   1.899 -lemma fun_upd_upd [simp]: "f(x:=y,x:=z) = f(x:=z)"
   1.900 -by (simp add: fun_eq_iff)
   1.901 +lemma fun_upd_other: "z \<noteq> x \<Longrightarrow> (f(x := y)) z = f z"
   1.902 +  by simp
   1.903  
   1.904 -lemma fun_upd_twist: "a ~= c ==> (m(a:=b))(c:=d) = (m(c:=d))(a:=b)"
   1.905 -by (rule ext, auto)
   1.906 +lemma fun_upd_upd [simp]: "f(x := y, x := z) = f(x := z)"
   1.907 +  by (simp add: fun_eq_iff)
   1.908  
   1.909 -lemma inj_on_fun_updI:
   1.910 -  "inj_on f A \<Longrightarrow> y \<notin> f ` A \<Longrightarrow> inj_on (f(x := y)) A"
   1.911 +lemma fun_upd_twist: "a \<noteq> c \<Longrightarrow> (m(a := b))(c := d) = (m(c := d))(a := b)"
   1.912 +  by (rule ext) auto
   1.913 +
   1.914 +lemma inj_on_fun_updI: "inj_on f A \<Longrightarrow> y \<notin> f ` A \<Longrightarrow> inj_on (f(x := y)) A"
   1.915    by (fastforce simp: inj_on_def)
   1.916  
   1.917 -lemma fun_upd_image:
   1.918 -     "f(x:=y) ` A = (if x \<in> A then insert y (f ` (A-{x})) else f ` A)"
   1.919 -by auto
   1.920 +lemma fun_upd_image: "f(x := y) ` A = (if x \<in> A then insert y (f ` (A - {x})) else f ` A)"
   1.921 +  by auto
   1.922  
   1.923  lemma fun_upd_comp: "f \<circ> (g(x := y)) = (f \<circ> g)(x := f y)"
   1.924    by auto
   1.925  
   1.926  lemma fun_upd_eqD: "f(x := y) = g(x := z) \<Longrightarrow> y = z"
   1.927 -by(simp add: fun_eq_iff split: if_split_asm)
   1.928 +  by (simp add: fun_eq_iff split: if_split_asm)
   1.929 +
   1.930  
   1.931  subsection \<open>\<open>override_on\<close>\<close>
   1.932  
   1.933 -definition override_on :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'a \<Rightarrow> 'b" where
   1.934 -  "override_on f g A = (\<lambda>a. if a \<in> A then g a else f a)"
   1.935 +definition override_on :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'a \<Rightarrow> 'b"
   1.936 +  where "override_on f g A = (\<lambda>a. if a \<in> A then g a else f a)"
   1.937  
   1.938  lemma override_on_emptyset[simp]: "override_on f g {} = f"
   1.939 -by(simp add:override_on_def)
   1.940 +  by (simp add:override_on_def)
   1.941  
   1.942 -lemma override_on_apply_notin[simp]: "a ~: A ==> (override_on f g A) a = f a"
   1.943 -by(simp add:override_on_def)
   1.944 +lemma override_on_apply_notin[simp]: "a \<notin> A \<Longrightarrow> (override_on f g A) a = f a"
   1.945 +  by (simp add:override_on_def)
   1.946  
   1.947 -lemma override_on_apply_in[simp]: "a : A ==> (override_on f g A) a = g a"
   1.948 -by(simp add:override_on_def)
   1.949 +lemma override_on_apply_in[simp]: "a \<in> A \<Longrightarrow> (override_on f g A) a = g a"
   1.950 +  by (simp add:override_on_def)
   1.951  
   1.952  
   1.953  subsection \<open>\<open>swap\<close>\<close>
   1.954  
   1.955  definition swap :: "'a \<Rightarrow> 'a \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)"
   1.956 -where
   1.957 -  "swap a b f = f (a := f b, b:= f a)"
   1.958 +  where "swap a b f = f (a := f b, b:= f a)"
   1.959  
   1.960  lemma swap_apply [simp]:
   1.961    "swap a b f a = f b"
   1.962 @@ -703,20 +674,16 @@
   1.963    "c \<noteq> a \<Longrightarrow> c \<noteq> b \<Longrightarrow> swap a b f c = f c"
   1.964    by (simp_all add: swap_def)
   1.965  
   1.966 -lemma swap_self [simp]:
   1.967 -  "swap a a f = f"
   1.968 +lemma swap_self [simp]: "swap a a f = f"
   1.969    by (simp add: swap_def)
   1.970  
   1.971 -lemma swap_commute:
   1.972 -  "swap a b f = swap b a f"
   1.973 +lemma swap_commute: "swap a b f = swap b a f"
   1.974    by (simp add: fun_upd_def swap_def fun_eq_iff)
   1.975  
   1.976 -lemma swap_nilpotent [simp]:
   1.977 -  "swap a b (swap a b f) = f"
   1.978 +lemma swap_nilpotent [simp]: "swap a b (swap a b f) = f"
   1.979    by (rule ext, simp add: fun_upd_def swap_def)
   1.980  
   1.981 -lemma swap_comp_involutory [simp]:
   1.982 -  "swap a b \<circ> swap a b = id"
   1.983 +lemma swap_comp_involutory [simp]: "swap a b \<circ> swap a b = id"
   1.984    by (rule ext) simp
   1.985  
   1.986  lemma swap_triple:
   1.987 @@ -725,10 +692,11 @@
   1.988    using assms by (simp add: fun_eq_iff swap_def)
   1.989  
   1.990  lemma comp_swap: "f \<circ> swap a b g = swap a b (f \<circ> g)"
   1.991 -  by (rule ext, simp add: fun_upd_def swap_def)
   1.992 +  by (rule ext) (simp add: fun_upd_def swap_def)
   1.993  
   1.994  lemma swap_image_eq [simp]:
   1.995 -  assumes "a \<in> A" "b \<in> A" shows "swap a b f ` A = f ` A"
   1.996 +  assumes "a \<in> A" "b \<in> A"
   1.997 +  shows "swap a b f ` A = f ` A"
   1.998  proof -
   1.999    have subset: "\<And>f. swap a b f ` A \<subseteq> f ` A"
  1.1000      using assms by (auto simp: image_iff swap_def)
  1.1001 @@ -736,20 +704,21 @@
  1.1002    with subset[of f] show ?thesis by auto
  1.1003  qed
  1.1004  
  1.1005 -lemma inj_on_imp_inj_on_swap:
  1.1006 -  "\<lbrakk>inj_on f A; a \<in> A; b \<in> A\<rbrakk> \<Longrightarrow> inj_on (swap a b f) A"
  1.1007 -  by (simp add: inj_on_def swap_def, blast)
  1.1008 +lemma inj_on_imp_inj_on_swap: "inj_on f A \<Longrightarrow> a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> inj_on (swap a b f) A"
  1.1009 +  by (auto simp add: inj_on_def swap_def)
  1.1010  
  1.1011  lemma inj_on_swap_iff [simp]:
  1.1012 -  assumes A: "a \<in> A" "b \<in> A" shows "inj_on (swap a b f) A \<longleftrightarrow> inj_on f A"
  1.1013 +  assumes A: "a \<in> A" "b \<in> A"
  1.1014 +  shows "inj_on (swap a b f) A \<longleftrightarrow> inj_on f A"
  1.1015  proof
  1.1016    assume "inj_on (swap a b f) A"
  1.1017    with A have "inj_on (swap a b (swap a b f)) A"
  1.1018      by (iprover intro: inj_on_imp_inj_on_swap)
  1.1019 -  thus "inj_on f A" by simp
  1.1020 +  then show "inj_on f A" by simp
  1.1021  next
  1.1022    assume "inj_on f A"
  1.1023 -  with A show "inj_on (swap a b f) A" by (iprover intro: inj_on_imp_inj_on_swap)
  1.1024 +  with A show "inj_on (swap a b f) A"
  1.1025 +    by (iprover intro: inj_on_imp_inj_on_swap)
  1.1026  qed
  1.1027  
  1.1028  lemma surj_imp_surj_swap: "surj f \<Longrightarrow> surj (swap a b f)"
  1.1029 @@ -758,8 +727,7 @@
  1.1030  lemma surj_swap_iff [simp]: "surj (swap a b f) \<longleftrightarrow> surj f"
  1.1031    by simp
  1.1032  
  1.1033 -lemma bij_betw_swap_iff [simp]:
  1.1034 -  "\<lbrakk> x \<in> A; y \<in> A \<rbrakk> \<Longrightarrow> bij_betw (swap x y f) A B \<longleftrightarrow> bij_betw f A B"
  1.1035 +lemma bij_betw_swap_iff [simp]: "x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> bij_betw (swap x y f) A B \<longleftrightarrow> bij_betw f A B"
  1.1036    by (auto simp: bij_betw_def)
  1.1037  
  1.1038  lemma bij_swap_iff [simp]: "bij (swap a b f) \<longleftrightarrow> bij f"
  1.1039 @@ -770,114 +738,107 @@
  1.1040  
  1.1041  subsection \<open>Inversion of injective functions\<close>
  1.1042  
  1.1043 -definition the_inv_into :: "'a set => ('a => 'b) => ('b => 'a)" where
  1.1044 -  "the_inv_into A f == %x. THE y. y : A & f y = x"
  1.1045 +definition the_inv_into :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a)"
  1.1046 +  where "the_inv_into A f \<equiv> \<lambda>x. THE y. y \<in> A \<and> f y = x"
  1.1047 +
  1.1048 +lemma the_inv_into_f_f: "inj_on f A \<Longrightarrow> x \<in> A \<Longrightarrow> the_inv_into A f (f x) = x"
  1.1049 +  unfolding the_inv_into_def inj_on_def by blast
  1.1050  
  1.1051 -lemma the_inv_into_f_f:
  1.1052 -  "[| inj_on f A;  x : A |] ==> the_inv_into A f (f x) = x"
  1.1053 -apply (simp add: the_inv_into_def inj_on_def)
  1.1054 -apply blast
  1.1055 -done
  1.1056 -
  1.1057 -lemma f_the_inv_into_f:
  1.1058 -  "inj_on f A ==> y : f`A  ==> f (the_inv_into A f y) = y"
  1.1059 -apply (simp add: the_inv_into_def)
  1.1060 -apply (rule the1I2)
  1.1061 - apply(blast dest: inj_onD)
  1.1062 -apply blast
  1.1063 -done
  1.1064 +lemma f_the_inv_into_f: "inj_on f A \<Longrightarrow> y \<in> f ` A  \<Longrightarrow> f (the_inv_into A f y) = y"
  1.1065 +  apply (simp add: the_inv_into_def)
  1.1066 +  apply (rule the1I2)
  1.1067 +   apply(blast dest: inj_onD)
  1.1068 +  apply blast
  1.1069 +  done
  1.1070  
  1.1071 -lemma the_inv_into_into:
  1.1072 -  "[| inj_on f A; x : f ` A; A <= B |] ==> the_inv_into A f x : B"
  1.1073 -apply (simp add: the_inv_into_def)
  1.1074 -apply (rule the1I2)
  1.1075 - apply(blast dest: inj_onD)
  1.1076 -apply blast
  1.1077 -done
  1.1078 +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"
  1.1079 +  apply (simp add: the_inv_into_def)
  1.1080 +  apply (rule the1I2)
  1.1081 +   apply(blast dest: inj_onD)
  1.1082 +  apply blast
  1.1083 +  done
  1.1084  
  1.1085 -lemma the_inv_into_onto[simp]:
  1.1086 -  "inj_on f A ==> the_inv_into A f ` (f ` A) = A"
  1.1087 -by (fast intro:the_inv_into_into the_inv_into_f_f[symmetric])
  1.1088 +lemma the_inv_into_onto [simp]: "inj_on f A \<Longrightarrow> the_inv_into A f ` (f ` A) = A"
  1.1089 +  by (fast intro: the_inv_into_into the_inv_into_f_f [symmetric])
  1.1090  
  1.1091 -lemma the_inv_into_f_eq:
  1.1092 -  "[| inj_on f A; f x = y; x : A |] ==> the_inv_into A f y = x"
  1.1093 +lemma the_inv_into_f_eq: "inj_on f A \<Longrightarrow> f x = y \<Longrightarrow> x \<in> A \<Longrightarrow> the_inv_into A f y = x"
  1.1094    apply (erule subst)
  1.1095 -  apply (erule the_inv_into_f_f, assumption)
  1.1096 +  apply (erule the_inv_into_f_f)
  1.1097 +  apply assumption
  1.1098    done
  1.1099  
  1.1100  lemma the_inv_into_comp:
  1.1101 -  "[| inj_on f (g ` A); inj_on g A; x : f ` g ` A |] ==>
  1.1102 -  the_inv_into A (f o g) x = (the_inv_into A g o the_inv_into (g ` A) f) x"
  1.1103 -apply (rule the_inv_into_f_eq)
  1.1104 -  apply (fast intro: comp_inj_on)
  1.1105 - apply (simp add: f_the_inv_into_f the_inv_into_into)
  1.1106 -apply (simp add: the_inv_into_into)
  1.1107 -done
  1.1108 +  "inj_on f (g ` A) \<Longrightarrow> inj_on g A \<Longrightarrow> x \<in> f ` g ` A \<Longrightarrow>
  1.1109 +    the_inv_into A (f \<circ> g) x = (the_inv_into A g \<circ> the_inv_into (g ` A) f) x"
  1.1110 +  apply (rule the_inv_into_f_eq)
  1.1111 +    apply (fast intro: comp_inj_on)
  1.1112 +   apply (simp add: f_the_inv_into_f the_inv_into_into)
  1.1113 +  apply (simp add: the_inv_into_into)
  1.1114 +  done
  1.1115  
  1.1116 -lemma inj_on_the_inv_into:
  1.1117 -  "inj_on f A \<Longrightarrow> inj_on (the_inv_into A f) (f ` A)"
  1.1118 -by (auto intro: inj_onI simp: the_inv_into_f_f)
  1.1119 +lemma inj_on_the_inv_into: "inj_on f A \<Longrightarrow> inj_on (the_inv_into A f) (f ` A)"
  1.1120 +  by (auto intro: inj_onI simp: the_inv_into_f_f)
  1.1121  
  1.1122 -lemma bij_betw_the_inv_into:
  1.1123 -  "bij_betw f A B \<Longrightarrow> bij_betw (the_inv_into A f) B A"
  1.1124 -by (auto simp add: bij_betw_def inj_on_the_inv_into the_inv_into_into)
  1.1125 +lemma bij_betw_the_inv_into: "bij_betw f A B \<Longrightarrow> bij_betw (the_inv_into A f) B A"
  1.1126 +  by (auto simp add: bij_betw_def inj_on_the_inv_into the_inv_into_into)
  1.1127  
  1.1128 -abbreviation the_inv :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a)" where
  1.1129 -  "the_inv f \<equiv> the_inv_into UNIV f"
  1.1130 +abbreviation the_inv :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a)"
  1.1131 +  where "the_inv f \<equiv> the_inv_into UNIV f"
  1.1132  
  1.1133  lemma the_inv_f_f:
  1.1134    assumes "inj f"
  1.1135 -  shows "the_inv f (f x) = x" using assms UNIV_I
  1.1136 -  by (rule the_inv_into_f_f)
  1.1137 +  shows "the_inv f (f x) = x"
  1.1138 +  using assms UNIV_I by (rule the_inv_into_f_f)
  1.1139  
  1.1140  
  1.1141  subsection \<open>Cantor's Paradox\<close>
  1.1142  
  1.1143 -lemma Cantors_paradox:
  1.1144 -  "\<not>(\<exists>f. f ` A = Pow A)"
  1.1145 +lemma Cantors_paradox: "\<not> (\<exists>f. f ` A = Pow A)"
  1.1146  proof clarify
  1.1147 -  fix f assume "f ` A = Pow A" hence *: "Pow A \<le> f ` A" by blast
  1.1148 +  fix f
  1.1149 +  assume "f ` A = Pow A"
  1.1150 +  then have *: "Pow A \<subseteq> f ` A" by blast
  1.1151    let ?X = "{a \<in> A. a \<notin> f a}"
  1.1152    have "?X \<in> Pow A" unfolding Pow_def by auto
  1.1153    with * obtain x where "x \<in> A \<and> f x = ?X" by blast
  1.1154 -  thus False by best
  1.1155 +  then show False by best
  1.1156  qed
  1.1157  
  1.1158 +
  1.1159  subsection \<open>Setup\<close>
  1.1160  
  1.1161  subsubsection \<open>Proof tools\<close>
  1.1162  
  1.1163 -text \<open>simplifies terms of the form
  1.1164 -  f(...,x:=y,...,x:=z,...) to f(...,x:=z,...)\<close>
  1.1165 +text \<open>Simplify terms of the form f(...,x:=y,...,x:=z,...) to f(...,x:=z,...)\<close>
  1.1166  
  1.1167  simproc_setup fun_upd2 ("f(v := w, x := y)") = \<open>fn _ =>
  1.1168 -let
  1.1169 -  fun gen_fun_upd NONE T _ _ = NONE
  1.1170 -    | gen_fun_upd (SOME f) T x y = SOME (Const (@{const_name fun_upd}, T) $ f $ x $ y)
  1.1171 -  fun dest_fun_T1 (Type (_, T :: Ts)) = T
  1.1172 -  fun find_double (t as Const (@{const_name fun_upd},T) $ f $ x $ y) =
  1.1173 -    let
  1.1174 -      fun find (Const (@{const_name fun_upd},T) $ g $ v $ w) =
  1.1175 -            if v aconv x then SOME g else gen_fun_upd (find g) T v w
  1.1176 -        | find t = NONE
  1.1177 -    in (dest_fun_T1 T, gen_fun_upd (find f) T x y) end
  1.1178 +  let
  1.1179 +    fun gen_fun_upd NONE T _ _ = NONE
  1.1180 +      | gen_fun_upd (SOME f) T x y = SOME (Const (@{const_name fun_upd}, T) $ f $ x $ y)
  1.1181 +    fun dest_fun_T1 (Type (_, T :: Ts)) = T
  1.1182 +    fun find_double (t as Const (@{const_name fun_upd},T) $ f $ x $ y) =
  1.1183 +      let
  1.1184 +        fun find (Const (@{const_name fun_upd},T) $ g $ v $ w) =
  1.1185 +              if v aconv x then SOME g else gen_fun_upd (find g) T v w
  1.1186 +          | find t = NONE
  1.1187 +      in (dest_fun_T1 T, gen_fun_upd (find f) T x y) end
  1.1188  
  1.1189 -  val ss = simpset_of @{context}
  1.1190 +    val ss = simpset_of @{context}
  1.1191  
  1.1192 -  fun proc ctxt ct =
  1.1193 -    let
  1.1194 -      val t = Thm.term_of ct
  1.1195 -    in
  1.1196 -      case find_double t of
  1.1197 -        (T, NONE) => NONE
  1.1198 -      | (T, SOME rhs) =>
  1.1199 -          SOME (Goal.prove ctxt [] [] (Logic.mk_equals (t, rhs))
  1.1200 -            (fn _ =>
  1.1201 -              resolve_tac ctxt [eq_reflection] 1 THEN
  1.1202 -              resolve_tac ctxt @{thms ext} 1 THEN
  1.1203 -              simp_tac (put_simpset ss ctxt) 1))
  1.1204 -    end
  1.1205 -in proc end
  1.1206 +    fun proc ctxt ct =
  1.1207 +      let
  1.1208 +        val t = Thm.term_of ct
  1.1209 +      in
  1.1210 +        case find_double t of
  1.1211 +          (T, NONE) => NONE
  1.1212 +        | (T, SOME rhs) =>
  1.1213 +            SOME (Goal.prove ctxt [] [] (Logic.mk_equals (t, rhs))
  1.1214 +              (fn _ =>
  1.1215 +                resolve_tac ctxt [eq_reflection] 1 THEN
  1.1216 +                resolve_tac ctxt @{thms ext} 1 THEN
  1.1217 +                simp_tac (put_simpset ss ctxt) 1))
  1.1218 +      end
  1.1219 +  in proc end
  1.1220  \<close>
  1.1221  
  1.1222  
  1.1223 @@ -891,6 +852,7 @@
  1.1224  functor vimage
  1.1225    by (simp_all add: fun_eq_iff vimage_comp)
  1.1226  
  1.1227 +
  1.1228  text \<open>Legacy theorem names\<close>
  1.1229  
  1.1230  lemmas o_def = comp_def
  1.1231 @@ -904,4 +866,3 @@
  1.1232  lemmas o_eq_id_dest = comp_eq_id_dest
  1.1233  
  1.1234  end
  1.1235 -
     2.1 --- a/src/HOL/Lattices.thy	Sun Jun 19 22:51:42 2016 +0200
     2.2 +++ b/src/HOL/Lattices.thy	Mon Jun 20 17:03:50 2016 +0200
     2.3 @@ -21,24 +21,23 @@
     2.4  begin
     2.5  
     2.6  lemma left_idem [simp]: "a \<^bold>* (a \<^bold>* b) = a \<^bold>* b"
     2.7 -by (simp add: assoc [symmetric])
     2.8 +  by (simp add: assoc [symmetric])
     2.9  
    2.10  lemma right_idem [simp]: "(a \<^bold>* b) \<^bold>* b = a \<^bold>* b"
    2.11 -by (simp add: assoc)
    2.12 +  by (simp add: assoc)
    2.13  
    2.14  end
    2.15  
    2.16  locale semilattice_neutr = semilattice + comm_monoid
    2.17  
    2.18  locale semilattice_order = semilattice +
    2.19 -  fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<^bold>\<le>" 50)
    2.20 -    and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<^bold><" 50)
    2.21 +  fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"  (infix "\<^bold>\<le>" 50)
    2.22 +    and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool"  (infix "\<^bold><" 50)
    2.23    assumes order_iff: "a \<^bold>\<le> b \<longleftrightarrow> a = a \<^bold>* b"
    2.24      and strict_order_iff: "a \<^bold>< b \<longleftrightarrow> a = a \<^bold>* b \<and> a \<noteq> b"
    2.25  begin
    2.26  
    2.27 -lemma orderI:
    2.28 -  "a = a \<^bold>* b \<Longrightarrow> a \<^bold>\<le> b"
    2.29 +lemma orderI: "a = a \<^bold>* b \<Longrightarrow> a \<^bold>\<le> b"
    2.30    by (simp add: order_iff)
    2.31  
    2.32  lemma orderE:
    2.33 @@ -49,7 +48,7 @@
    2.34  sublocale ordering less_eq less
    2.35  proof
    2.36    fix a b
    2.37 -  show "a \<^bold>< b \<longleftrightarrow> a \<^bold>\<le> b \<and> a \<noteq> b"
    2.38 +  show "a \<^bold>< b \<longleftrightarrow> a \<^bold>\<le> b \<and> a \<noteq> b" for a b
    2.39      by (simp add: order_iff strict_order_iff)
    2.40  next
    2.41    fix a
    2.42 @@ -74,12 +73,10 @@
    2.43    then show "a \<^bold>\<le> c" by (rule orderI)
    2.44  qed
    2.45  
    2.46 -lemma cobounded1 [simp]:
    2.47 -  "a \<^bold>* b \<^bold>\<le> a"
    2.48 -  by (simp add: order_iff commute)  
    2.49 +lemma cobounded1 [simp]: "a \<^bold>* b \<^bold>\<le> a"
    2.50 +  by (simp add: order_iff commute)
    2.51  
    2.52 -lemma cobounded2 [simp]:
    2.53 -  "a \<^bold>* b \<^bold>\<le> b"
    2.54 +lemma cobounded2 [simp]: "a \<^bold>* b \<^bold>\<le> b"
    2.55    by (simp add: order_iff)
    2.56  
    2.57  lemma boundedI:
    2.58 @@ -95,8 +92,7 @@
    2.59    obtains "a \<^bold>\<le> b" and "a \<^bold>\<le> c"
    2.60    using assms by (blast intro: trans cobounded1 cobounded2)
    2.61  
    2.62 -lemma bounded_iff [simp]:
    2.63 -  "a \<^bold>\<le> b \<^bold>* c \<longleftrightarrow> a \<^bold>\<le> b \<and> a \<^bold>\<le> c"
    2.64 +lemma bounded_iff [simp]: "a \<^bold>\<le> b \<^bold>* c \<longleftrightarrow> a \<^bold>\<le> b \<and> a \<^bold>\<le> c"
    2.65    by (blast intro: boundedI elim: boundedE)
    2.66  
    2.67  lemma strict_boundedE:
    2.68 @@ -104,21 +100,17 @@
    2.69    obtains "a \<^bold>< b" and "a \<^bold>< c"
    2.70    using assms by (auto simp add: commute strict_iff_order elim: orderE intro!: that)+
    2.71  
    2.72 -lemma coboundedI1:
    2.73 -  "a \<^bold>\<le> c \<Longrightarrow> a \<^bold>* b \<^bold>\<le> c"
    2.74 +lemma coboundedI1: "a \<^bold>\<le> c \<Longrightarrow> a \<^bold>* b \<^bold>\<le> c"
    2.75    by (rule trans) auto
    2.76  
    2.77 -lemma coboundedI2:
    2.78 -  "b \<^bold>\<le> c \<Longrightarrow> a \<^bold>* b \<^bold>\<le> c"
    2.79 +lemma coboundedI2: "b \<^bold>\<le> c \<Longrightarrow> a \<^bold>* b \<^bold>\<le> c"
    2.80    by (rule trans) auto
    2.81  
    2.82 -lemma strict_coboundedI1:
    2.83 -  "a \<^bold>< c \<Longrightarrow> a \<^bold>* b \<^bold>< c"
    2.84 +lemma strict_coboundedI1: "a \<^bold>< c \<Longrightarrow> a \<^bold>* b \<^bold>< c"
    2.85    using irrefl
    2.86      by (auto intro: not_eq_order_implies_strict coboundedI1 strict_implies_order elim: strict_boundedE)
    2.87  
    2.88 -lemma strict_coboundedI2:
    2.89 -  "b \<^bold>< c \<Longrightarrow> a \<^bold>* b \<^bold>< c"
    2.90 +lemma strict_coboundedI2: "b \<^bold>< c \<Longrightarrow> a \<^bold>* b \<^bold>< c"
    2.91    using strict_coboundedI1 [of b c a] by (simp add: commute)
    2.92  
    2.93  lemma mono: "a \<^bold>\<le> c \<Longrightarrow> b \<^bold>\<le> d \<Longrightarrow> a \<^bold>* b \<^bold>\<le> c \<^bold>* d"
    2.94 @@ -152,7 +144,7 @@
    2.95  class inf =
    2.96    fixes inf :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 70)
    2.97  
    2.98 -class sup = 
    2.99 +class sup =
   2.100    fixes sup :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<squnion>" 65)
   2.101  
   2.102  
   2.103 @@ -175,10 +167,9 @@
   2.104  
   2.105  text \<open>Dual lattice\<close>
   2.106  
   2.107 -lemma dual_semilattice:
   2.108 -  "class.semilattice_inf sup greater_eq greater"
   2.109 -by (rule class.semilattice_inf.intro, rule dual_order)
   2.110 -  (unfold_locales, simp_all add: sup_least)
   2.111 +lemma dual_semilattice: "class.semilattice_inf sup greater_eq greater"
   2.112 +  by (rule class.semilattice_inf.intro, rule dual_order)
   2.113 +    (unfold_locales, simp_all add: sup_least)
   2.114  
   2.115  end
   2.116  
   2.117 @@ -190,12 +181,10 @@
   2.118  context semilattice_inf
   2.119  begin
   2.120  
   2.121 -lemma le_infI1:
   2.122 -  "a \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x"
   2.123 +lemma le_infI1: "a \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x"
   2.124    by (rule order_trans) auto
   2.125  
   2.126 -lemma le_infI2:
   2.127 -  "b \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x"
   2.128 +lemma le_infI2: "b \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x"
   2.129    by (rule order_trans) auto
   2.130  
   2.131  lemma le_infI: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<sqinter> b"
   2.132 @@ -204,20 +193,16 @@
   2.133  lemma le_infE: "x \<sqsubseteq> a \<sqinter> b \<Longrightarrow> (x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> P) \<Longrightarrow> P"
   2.134    by (blast intro: order_trans inf_le1 inf_le2)
   2.135  
   2.136 -lemma le_inf_iff:
   2.137 -  "x \<sqsubseteq> y \<sqinter> z \<longleftrightarrow> x \<sqsubseteq> y \<and> x \<sqsubseteq> z"
   2.138 +lemma le_inf_iff: "x \<sqsubseteq> y \<sqinter> z \<longleftrightarrow> x \<sqsubseteq> y \<and> x \<sqsubseteq> z"
   2.139    by (blast intro: le_infI elim: le_infE)
   2.140  
   2.141 -lemma le_iff_inf:
   2.142 -  "x \<sqsubseteq> y \<longleftrightarrow> x \<sqinter> y = x"
   2.143 +lemma le_iff_inf: "x \<sqsubseteq> y \<longleftrightarrow> x \<sqinter> y = x"
   2.144    by (auto intro: le_infI1 antisym dest: eq_iff [THEN iffD1] simp add: le_inf_iff)
   2.145  
   2.146  lemma inf_mono: "a \<sqsubseteq> c \<Longrightarrow> b \<sqsubseteq> d \<Longrightarrow> a \<sqinter> b \<sqsubseteq> c \<sqinter> d"
   2.147    by (fast intro: inf_greatest le_infI1 le_infI2)
   2.148  
   2.149 -lemma mono_inf:
   2.150 -  fixes f :: "'a \<Rightarrow> 'b::semilattice_inf"
   2.151 -  shows "mono f \<Longrightarrow> f (A \<sqinter> B) \<sqsubseteq> f A \<sqinter> f B"
   2.152 +lemma mono_inf: "mono f \<Longrightarrow> f (A \<sqinter> B) \<sqsubseteq> f A \<sqinter> f B" for f :: "'a \<Rightarrow> 'b::semilattice_inf"
   2.153    by (auto simp add: mono_def intro: Lattices.inf_greatest)
   2.154  
   2.155  end
   2.156 @@ -225,36 +210,28 @@
   2.157  context semilattice_sup
   2.158  begin
   2.159  
   2.160 -lemma le_supI1:
   2.161 -  "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
   2.162 +lemma le_supI1: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
   2.163 +  by (rule order_trans) auto
   2.164 +
   2.165 +lemma le_supI2: "x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
   2.166    by (rule order_trans) auto
   2.167  
   2.168 -lemma le_supI2:
   2.169 -  "x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
   2.170 -  by (rule order_trans) auto 
   2.171 -
   2.172 -lemma le_supI:
   2.173 -  "a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> a \<squnion> b \<sqsubseteq> x"
   2.174 +lemma le_supI: "a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> a \<squnion> b \<sqsubseteq> x"
   2.175    by (fact sup_least) (* FIXME: duplicate lemma *)
   2.176  
   2.177 -lemma le_supE:
   2.178 -  "a \<squnion> b \<sqsubseteq> x \<Longrightarrow> (a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> P) \<Longrightarrow> P"
   2.179 +lemma le_supE: "a \<squnion> b \<sqsubseteq> x \<Longrightarrow> (a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> P) \<Longrightarrow> P"
   2.180    by (blast intro: order_trans sup_ge1 sup_ge2)
   2.181  
   2.182 -lemma le_sup_iff:
   2.183 -  "x \<squnion> y \<sqsubseteq> z \<longleftrightarrow> x \<sqsubseteq> z \<and> y \<sqsubseteq> z"
   2.184 +lemma le_sup_iff: "x \<squnion> y \<sqsubseteq> z \<longleftrightarrow> x \<sqsubseteq> z \<and> y \<sqsubseteq> z"
   2.185    by (blast intro: le_supI elim: le_supE)
   2.186  
   2.187 -lemma le_iff_sup:
   2.188 -  "x \<sqsubseteq> y \<longleftrightarrow> x \<squnion> y = y"
   2.189 +lemma le_iff_sup: "x \<sqsubseteq> y \<longleftrightarrow> x \<squnion> y = y"
   2.190    by (auto intro: le_supI2 antisym dest: eq_iff [THEN iffD1] simp add: le_sup_iff)
   2.191  
   2.192  lemma sup_mono: "a \<sqsubseteq> c \<Longrightarrow> b \<sqsubseteq> d \<Longrightarrow> a \<squnion> b \<sqsubseteq> c \<squnion> d"
   2.193    by (fast intro: sup_least le_supI1 le_supI2)
   2.194  
   2.195 -lemma mono_sup:
   2.196 -  fixes f :: "'a \<Rightarrow> 'b::semilattice_sup"
   2.197 -  shows "mono f \<Longrightarrow> f A \<squnion> f B \<sqsubseteq> f (A \<squnion> B)"
   2.198 +lemma mono_sup: "mono f \<Longrightarrow> f A \<squnion> f B \<sqsubseteq> f (A \<squnion> B)" for f :: "'a \<Rightarrow> 'b::semilattice_sup"
   2.199    by (auto simp add: mono_def intro: Lattices.sup_least)
   2.200  
   2.201  end
   2.202 @@ -302,7 +279,7 @@
   2.203  
   2.204  lemma inf_absorb2: "y \<sqsubseteq> x \<Longrightarrow> x \<sqinter> y = y"
   2.205    by (rule antisym) auto
   2.206 - 
   2.207 +
   2.208  lemmas inf_aci = inf_commute inf_assoc inf_left_commute inf_left_idem
   2.209  
   2.210  end
   2.211 @@ -352,8 +329,7 @@
   2.212  context lattice
   2.213  begin
   2.214  
   2.215 -lemma dual_lattice:
   2.216 -  "class.lattice sup (op \<ge>) (op >) inf"
   2.217 +lemma dual_lattice: "class.lattice sup (op \<ge>) (op >) inf"
   2.218    by (rule class.lattice.intro, rule dual_semilattice, rule class.semilattice_sup.intro, rule dual_order)
   2.219      (unfold_locales, auto)
   2.220  
   2.221 @@ -375,47 +351,48 @@
   2.222  lemma distrib_inf_le: "(x \<sqinter> y) \<squnion> (x \<sqinter> z) \<sqsubseteq> x \<sqinter> (y \<squnion> z)"
   2.223    by (auto intro: le_infI1 le_infI2 le_supI1 le_supI2)
   2.224  
   2.225 -text\<open>If you have one of them, you have them all.\<close>
   2.226 +text \<open>If you have one of them, you have them all.\<close>
   2.227  
   2.228  lemma distrib_imp1:
   2.229 -assumes D: "!!x y z. x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
   2.230 -shows "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
   2.231 +  assumes distrib: "\<And>x y z. x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
   2.232 +  shows "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
   2.233  proof-
   2.234 -  have "x \<squnion> (y \<sqinter> z) = (x \<squnion> (x \<sqinter> z)) \<squnion> (y \<sqinter> z)" by simp
   2.235 +  have "x \<squnion> (y \<sqinter> z) = (x \<squnion> (x \<sqinter> z)) \<squnion> (y \<sqinter> z)"
   2.236 +    by simp
   2.237    also have "\<dots> = x \<squnion> (z \<sqinter> (x \<squnion> y))"
   2.238 -    by (simp add: D inf_commute sup_assoc del: sup_inf_absorb)
   2.239 +    by (simp add: distrib inf_commute sup_assoc del: sup_inf_absorb)
   2.240    also have "\<dots> = ((x \<squnion> y) \<sqinter> x) \<squnion> ((x \<squnion> y) \<sqinter> z)"
   2.241 -    by(simp add: inf_commute)
   2.242 -  also have "\<dots> = (x \<squnion> y) \<sqinter> (x \<squnion> z)" by(simp add:D)
   2.243 +    by (simp add: inf_commute)
   2.244 +  also have "\<dots> = (x \<squnion> y) \<sqinter> (x \<squnion> z)" by(simp add:distrib)
   2.245    finally show ?thesis .
   2.246  qed
   2.247  
   2.248  lemma distrib_imp2:
   2.249 -assumes D: "!!x y z. x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
   2.250 -shows "x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
   2.251 +  assumes distrib: "\<And>x y z. x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
   2.252 +  shows "x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
   2.253  proof-
   2.254 -  have "x \<sqinter> (y \<squnion> z) = (x \<sqinter> (x \<squnion> z)) \<sqinter> (y \<squnion> z)" by simp
   2.255 +  have "x \<sqinter> (y \<squnion> z) = (x \<sqinter> (x \<squnion> z)) \<sqinter> (y \<squnion> z)"
   2.256 +    by simp
   2.257    also have "\<dots> = x \<sqinter> (z \<squnion> (x \<sqinter> y))"
   2.258 -    by (simp add: D sup_commute inf_assoc del: inf_sup_absorb)
   2.259 +    by (simp add: distrib sup_commute inf_assoc del: inf_sup_absorb)
   2.260    also have "\<dots> = ((x \<sqinter> y) \<squnion> x) \<sqinter> ((x \<sqinter> y) \<squnion> z)"
   2.261 -    by(simp add: sup_commute)
   2.262 -  also have "\<dots> = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" by(simp add:D)
   2.263 +    by (simp add: sup_commute)
   2.264 +  also have "\<dots> = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" by (simp add:distrib)
   2.265    finally show ?thesis .
   2.266  qed
   2.267  
   2.268  end
   2.269  
   2.270 +
   2.271  subsubsection \<open>Strict order\<close>
   2.272  
   2.273  context semilattice_inf
   2.274  begin
   2.275  
   2.276 -lemma less_infI1:
   2.277 -  "a \<sqsubset> x \<Longrightarrow> a \<sqinter> b \<sqsubset> x"
   2.278 +lemma less_infI1: "a \<sqsubset> x \<Longrightarrow> a \<sqinter> b \<sqsubset> x"
   2.279    by (auto simp add: less_le inf_absorb1 intro: le_infI1)
   2.280  
   2.281 -lemma less_infI2:
   2.282 -  "b \<sqsubset> x \<Longrightarrow> a \<sqinter> b \<sqsubset> x"
   2.283 +lemma less_infI2: "b \<sqsubset> x \<Longrightarrow> a \<sqinter> b \<sqsubset> x"
   2.284    by (auto simp add: less_le inf_absorb2 intro: le_infI2)
   2.285  
   2.286  end
   2.287 @@ -423,13 +400,11 @@
   2.288  context semilattice_sup
   2.289  begin
   2.290  
   2.291 -lemma less_supI1:
   2.292 -  "x \<sqsubset> a \<Longrightarrow> x \<sqsubset> a \<squnion> b"
   2.293 +lemma less_supI1: "x \<sqsubset> a \<Longrightarrow> x \<sqsubset> a \<squnion> b"
   2.294    using dual_semilattice
   2.295    by (rule semilattice_inf.less_infI1)
   2.296  
   2.297 -lemma less_supI2:
   2.298 -  "x \<sqsubset> b \<Longrightarrow> x \<sqsubset> a \<squnion> b"
   2.299 +lemma less_supI2: "x \<sqsubset> b \<Longrightarrow> x \<sqsubset> a \<squnion> b"
   2.300    using dual_semilattice
   2.301    by (rule semilattice_inf.less_infI2)
   2.302  
   2.303 @@ -444,31 +419,24 @@
   2.304  context distrib_lattice
   2.305  begin
   2.306  
   2.307 -lemma sup_inf_distrib2:
   2.308 -  "(y \<sqinter> z) \<squnion> x = (y \<squnion> x) \<sqinter> (z \<squnion> x)"
   2.309 +lemma sup_inf_distrib2: "(y \<sqinter> z) \<squnion> x = (y \<squnion> x) \<sqinter> (z \<squnion> x)"
   2.310    by (simp add: sup_commute sup_inf_distrib1)
   2.311  
   2.312 -lemma inf_sup_distrib1:
   2.313 -  "x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
   2.314 +lemma inf_sup_distrib1: "x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
   2.315    by (rule distrib_imp2 [OF sup_inf_distrib1])
   2.316  
   2.317 -lemma inf_sup_distrib2:
   2.318 -  "(y \<squnion> z) \<sqinter> x = (y \<sqinter> x) \<squnion> (z \<sqinter> x)"
   2.319 +lemma inf_sup_distrib2: "(y \<squnion> z) \<sqinter> x = (y \<sqinter> x) \<squnion> (z \<sqinter> x)"
   2.320    by (simp add: inf_commute inf_sup_distrib1)
   2.321  
   2.322 -lemma dual_distrib_lattice:
   2.323 -  "class.distrib_lattice sup (op \<ge>) (op >) inf"
   2.324 +lemma dual_distrib_lattice: "class.distrib_lattice sup (op \<ge>) (op >) inf"
   2.325    by (rule class.distrib_lattice.intro, rule dual_lattice)
   2.326      (unfold_locales, fact inf_sup_distrib1)
   2.327  
   2.328 -lemmas sup_inf_distrib =
   2.329 -  sup_inf_distrib1 sup_inf_distrib2
   2.330 +lemmas sup_inf_distrib = sup_inf_distrib1 sup_inf_distrib2
   2.331  
   2.332 -lemmas inf_sup_distrib =
   2.333 -  inf_sup_distrib1 inf_sup_distrib2
   2.334 +lemmas inf_sup_distrib = inf_sup_distrib1 inf_sup_distrib2
   2.335  
   2.336 -lemmas distrib =
   2.337 -  sup_inf_distrib1 sup_inf_distrib2 inf_sup_distrib1 inf_sup_distrib2
   2.338 +lemmas distrib = sup_inf_distrib1 sup_inf_distrib2 inf_sup_distrib1 inf_sup_distrib2
   2.339  
   2.340  end
   2.341  
   2.342 @@ -481,8 +449,7 @@
   2.343  sublocale inf_top: semilattice_neutr inf top
   2.344    + inf_top: semilattice_neutr_order inf top less_eq less
   2.345  proof
   2.346 -  fix x
   2.347 -  show "x \<sqinter> \<top> = x"
   2.348 +  show "x \<sqinter> \<top> = x" for x
   2.349      by (rule inf_absorb1) simp
   2.350  qed
   2.351  
   2.352 @@ -494,8 +461,7 @@
   2.353  sublocale sup_bot: semilattice_neutr sup bot
   2.354    + sup_bot: semilattice_neutr_order sup bot greater_eq greater
   2.355  proof
   2.356 -  fix x
   2.357 -  show "x \<squnion> \<bottom> = x"
   2.358 +  show "x \<squnion> \<bottom> = x" for x
   2.359      by (rule sup_absorb1) simp
   2.360  qed
   2.361  
   2.362 @@ -506,28 +472,22 @@
   2.363  
   2.364  subclass bounded_semilattice_sup_bot ..
   2.365  
   2.366 -lemma inf_bot_left [simp]:
   2.367 -  "\<bottom> \<sqinter> x = \<bottom>"
   2.368 +lemma inf_bot_left [simp]: "\<bottom> \<sqinter> x = \<bottom>"
   2.369    by (rule inf_absorb1) simp
   2.370  
   2.371 -lemma inf_bot_right [simp]:
   2.372 -  "x \<sqinter> \<bottom> = \<bottom>"
   2.373 +lemma inf_bot_right [simp]: "x \<sqinter> \<bottom> = \<bottom>"
   2.374    by (rule inf_absorb2) simp
   2.375  
   2.376 -lemma sup_bot_left:
   2.377 -  "\<bottom> \<squnion> x = x"
   2.378 +lemma sup_bot_left: "\<bottom> \<squnion> x = x"
   2.379    by (fact sup_bot.left_neutral)
   2.380  
   2.381 -lemma sup_bot_right:
   2.382 -  "x \<squnion> \<bottom> = x"
   2.383 +lemma sup_bot_right: "x \<squnion> \<bottom> = x"
   2.384    by (fact sup_bot.right_neutral)
   2.385  
   2.386 -lemma sup_eq_bot_iff [simp]:
   2.387 -  "x \<squnion> y = \<bottom> \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>"
   2.388 +lemma sup_eq_bot_iff [simp]: "x \<squnion> y = \<bottom> \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>"
   2.389    by (simp add: eq_iff)
   2.390  
   2.391 -lemma bot_eq_sup_iff [simp]:
   2.392 -  "\<bottom> = x \<squnion> y \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>"
   2.393 +lemma bot_eq_sup_iff [simp]: "\<bottom> = x \<squnion> y \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>"
   2.394    by (simp add: eq_iff)
   2.395  
   2.396  end
   2.397 @@ -537,24 +497,19 @@
   2.398  
   2.399  subclass bounded_semilattice_inf_top ..
   2.400  
   2.401 -lemma sup_top_left [simp]:
   2.402 -  "\<top> \<squnion> x = \<top>"
   2.403 +lemma sup_top_left [simp]: "\<top> \<squnion> x = \<top>"
   2.404    by (rule sup_absorb1) simp
   2.405  
   2.406 -lemma sup_top_right [simp]:
   2.407 -  "x \<squnion> \<top> = \<top>"
   2.408 +lemma sup_top_right [simp]: "x \<squnion> \<top> = \<top>"
   2.409    by (rule sup_absorb2) simp
   2.410  
   2.411 -lemma inf_top_left:
   2.412 -  "\<top> \<sqinter> x = x"
   2.413 +lemma inf_top_left: "\<top> \<sqinter> x = x"
   2.414    by (fact inf_top.left_neutral)
   2.415  
   2.416 -lemma inf_top_right:
   2.417 -  "x \<sqinter> \<top> = x"
   2.418 +lemma inf_top_right: "x \<sqinter> \<top> = x"
   2.419    by (fact inf_top.right_neutral)
   2.420  
   2.421 -lemma inf_eq_top_iff [simp]:
   2.422 -  "x \<sqinter> y = \<top> \<longleftrightarrow> x = \<top> \<and> y = \<top>"
   2.423 +lemma inf_eq_top_iff [simp]: "x \<sqinter> y = \<top> \<longleftrightarrow> x = \<top> \<and> y = \<top>"
   2.424    by (simp add: eq_iff)
   2.425  
   2.426  end
   2.427 @@ -565,8 +520,7 @@
   2.428  subclass bounded_lattice_bot ..
   2.429  subclass bounded_lattice_top ..
   2.430  
   2.431 -lemma dual_bounded_lattice:
   2.432 -  "class.bounded_lattice sup greater_eq greater inf \<top> \<bottom>"
   2.433 +lemma dual_bounded_lattice: "class.bounded_lattice sup greater_eq greater inf \<top> \<bottom>"
   2.434    by unfold_locales (auto simp add: less_le_not_le)
   2.435  
   2.436  end
   2.437 @@ -582,12 +536,10 @@
   2.438    by (rule class.boolean_algebra.intro, rule dual_bounded_lattice, rule dual_distrib_lattice)
   2.439      (unfold_locales, auto simp add: inf_compl_bot sup_compl_top diff_eq)
   2.440  
   2.441 -lemma compl_inf_bot [simp]:
   2.442 -  "- x \<sqinter> x = \<bottom>"
   2.443 +lemma compl_inf_bot [simp]: "- x \<sqinter> x = \<bottom>"
   2.444    by (simp add: inf_commute inf_compl_bot)
   2.445  
   2.446 -lemma compl_sup_top [simp]:
   2.447 -  "- x \<squnion> x = \<top>"
   2.448 +lemma compl_sup_top [simp]: "- x \<squnion> x = \<top>"
   2.449    by (simp add: sup_commute sup_compl_top)
   2.450  
   2.451  lemma compl_unique:
   2.452 @@ -606,12 +558,10 @@
   2.453    then show "- x = y" by simp
   2.454  qed
   2.455  
   2.456 -lemma double_compl [simp]:
   2.457 -  "- (- x) = x"
   2.458 +lemma double_compl [simp]: "- (- x) = x"
   2.459    using compl_inf_bot compl_sup_top by (rule compl_unique)
   2.460  
   2.461 -lemma compl_eq_compl_iff [simp]:
   2.462 -  "- x = - y \<longleftrightarrow> x = y"
   2.463 +lemma compl_eq_compl_iff [simp]: "- x = - y \<longleftrightarrow> x = y"
   2.464  proof
   2.465    assume "- x = - y"
   2.466    then have "- (- x) = - (- y)" by (rule arg_cong)
   2.467 @@ -621,22 +571,19 @@
   2.468    then show "- x = - y" by simp
   2.469  qed
   2.470  
   2.471 -lemma compl_bot_eq [simp]:
   2.472 -  "- \<bottom> = \<top>"
   2.473 +lemma compl_bot_eq [simp]: "- \<bottom> = \<top>"
   2.474  proof -
   2.475    from sup_compl_top have "\<bottom> \<squnion> - \<bottom> = \<top>" .
   2.476    then show ?thesis by simp
   2.477  qed
   2.478  
   2.479 -lemma compl_top_eq [simp]:
   2.480 -  "- \<top> = \<bottom>"
   2.481 +lemma compl_top_eq [simp]: "- \<top> = \<bottom>"
   2.482  proof -
   2.483    from inf_compl_bot have "\<top> \<sqinter> - \<top> = \<bottom>" .
   2.484    then show ?thesis by simp
   2.485  qed
   2.486  
   2.487 -lemma compl_inf [simp]:
   2.488 -  "- (x \<sqinter> y) = - x \<squnion> - y"
   2.489 +lemma compl_inf [simp]: "- (x \<sqinter> y) = - x \<squnion> - y"
   2.490  proof (rule compl_unique)
   2.491    have "(x \<sqinter> y) \<sqinter> (- x \<squnion> - y) = (y \<sqinter> (x \<sqinter> - x)) \<squnion> (x \<sqinter> (y \<sqinter> - y))"
   2.492      by (simp only: inf_sup_distrib inf_aci)
   2.493 @@ -649,86 +596,87 @@
   2.494      by (simp add: sup_compl_top)
   2.495  qed
   2.496  
   2.497 -lemma compl_sup [simp]:
   2.498 -  "- (x \<squnion> y) = - x \<sqinter> - y"
   2.499 +lemma compl_sup [simp]: "- (x \<squnion> y) = - x \<sqinter> - y"
   2.500    using dual_boolean_algebra
   2.501    by (rule boolean_algebra.compl_inf)
   2.502  
   2.503  lemma compl_mono:
   2.504 -  "x \<sqsubseteq> y \<Longrightarrow> - y \<sqsubseteq> - x"
   2.505 +  assumes "x \<sqsubseteq> y"
   2.506 +  shows "- y \<sqsubseteq> - x"
   2.507  proof -
   2.508 -  assume "x \<sqsubseteq> y"
   2.509 -  then have "x \<squnion> y = y" by (simp only: le_iff_sup)
   2.510 +  from assms have "x \<squnion> y = y" by (simp only: le_iff_sup)
   2.511    then have "- (x \<squnion> y) = - y" by simp
   2.512    then have "- x \<sqinter> - y = - y" by simp
   2.513    then have "- y \<sqinter> - x = - y" by (simp only: inf_commute)
   2.514 -  then show "- y \<sqsubseteq> - x" by (simp only: le_iff_inf)
   2.515 +  then show ?thesis by (simp only: le_iff_inf)
   2.516  qed
   2.517  
   2.518 -lemma compl_le_compl_iff [simp]:
   2.519 -  "- x \<sqsubseteq> - y \<longleftrightarrow> y \<sqsubseteq> x"
   2.520 +lemma compl_le_compl_iff [simp]: "- x \<sqsubseteq> - y \<longleftrightarrow> y \<sqsubseteq> x"
   2.521    by (auto dest: compl_mono)
   2.522  
   2.523  lemma compl_le_swap1:
   2.524 -  assumes "y \<sqsubseteq> - x" shows "x \<sqsubseteq> -y"
   2.525 +  assumes "y \<sqsubseteq> - x"
   2.526 +  shows "x \<sqsubseteq> -y"
   2.527  proof -
   2.528    from assms have "- (- x) \<sqsubseteq> - y" by (simp only: compl_le_compl_iff)
   2.529    then show ?thesis by simp
   2.530  qed
   2.531  
   2.532  lemma compl_le_swap2:
   2.533 -  assumes "- y \<sqsubseteq> x" shows "- x \<sqsubseteq> y"
   2.534 +  assumes "- y \<sqsubseteq> x"
   2.535 +  shows "- x \<sqsubseteq> y"
   2.536  proof -
   2.537    from assms have "- x \<sqsubseteq> - (- y)" by (simp only: compl_le_compl_iff)
   2.538    then show ?thesis by simp
   2.539  qed
   2.540  
   2.541 -lemma compl_less_compl_iff: (* TODO: declare [simp] ? *)
   2.542 -  "- x \<sqsubset> - y \<longleftrightarrow> y \<sqsubset> x"
   2.543 +lemma compl_less_compl_iff: "- x \<sqsubset> - y \<longleftrightarrow> y \<sqsubset> x"  (* TODO: declare [simp] ? *)
   2.544    by (auto simp add: less_le)
   2.545  
   2.546  lemma compl_less_swap1:
   2.547 -  assumes "y \<sqsubset> - x" shows "x \<sqsubset> - y"
   2.548 +  assumes "y \<sqsubset> - x"
   2.549 +  shows "x \<sqsubset> - y"
   2.550  proof -
   2.551    from assms have "- (- x) \<sqsubset> - y" by (simp only: compl_less_compl_iff)
   2.552    then show ?thesis by simp
   2.553  qed
   2.554  
   2.555  lemma compl_less_swap2:
   2.556 -  assumes "- y \<sqsubset> x" shows "- x \<sqsubset> y"
   2.557 +  assumes "- y \<sqsubset> x"
   2.558 +  shows "- x \<sqsubset> y"
   2.559  proof -
   2.560    from assms have "- x \<sqsubset> - (- y)" by (simp only: compl_less_compl_iff)
   2.561    then show ?thesis by simp
   2.562  qed
   2.563  
   2.564  lemma sup_cancel_left1: "sup (sup x a) (sup (- x) b) = top"
   2.565 -by(simp add: inf_sup_aci sup_compl_top)
   2.566 +  by (simp add: inf_sup_aci sup_compl_top)
   2.567  
   2.568  lemma sup_cancel_left2: "sup (sup (- x) a) (sup x b) = top"
   2.569 -by(simp add: inf_sup_aci sup_compl_top)
   2.570 +  by (simp add: inf_sup_aci sup_compl_top)
   2.571  
   2.572  lemma inf_cancel_left1: "inf (inf x a) (inf (- x) b) = bot"
   2.573 -by(simp add: inf_sup_aci inf_compl_bot)
   2.574 +  by (simp add: inf_sup_aci inf_compl_bot)
   2.575  
   2.576  lemma inf_cancel_left2: "inf (inf (- x) a) (inf x b) = bot"
   2.577 -by(simp add: inf_sup_aci inf_compl_bot)
   2.578 +  by (simp add: inf_sup_aci inf_compl_bot)
   2.579  
   2.580 -declare inf_compl_bot [simp] sup_compl_top [simp]
   2.581 +declare inf_compl_bot [simp] and sup_compl_top [simp]
   2.582  
   2.583  lemma sup_compl_top_left1 [simp]: "sup (- x) (sup x y) = top"
   2.584 -by(simp add: sup_assoc[symmetric])
   2.585 +  by (simp add: sup_assoc[symmetric])
   2.586  
   2.587  lemma sup_compl_top_left2 [simp]: "sup x (sup (- x) y) = top"
   2.588 -using sup_compl_top_left1[of "- x" y] by simp
   2.589 +  using sup_compl_top_left1[of "- x" y] by simp
   2.590  
   2.591  lemma inf_compl_bot_left1 [simp]: "inf (- x) (inf x y) = bot"
   2.592 -by(simp add: inf_assoc[symmetric])
   2.593 +  by (simp add: inf_assoc[symmetric])
   2.594  
   2.595  lemma inf_compl_bot_left2 [simp]: "inf x (inf (- x) y) = bot"
   2.596 -using inf_compl_bot_left1[of "- x" y] by simp
   2.597 +  using inf_compl_bot_left1[of "- x" y] by simp
   2.598  
   2.599  lemma inf_compl_bot_right [simp]: "inf x (inf y (- x)) = bot"
   2.600 -by(subst inf_left_commute) simp
   2.601 +  by (subst inf_left_commute) simp
   2.602  
   2.603  end
   2.604  
   2.605 @@ -740,6 +688,7 @@
   2.606  simproc_setup boolean_algebra_cancel_inf ("inf a b::'a::boolean_algebra") =
   2.607    \<open>fn phi => fn ss => try Boolean_Algebra_Cancel.cancel_inf_conv\<close>
   2.608  
   2.609 +
   2.610  subsection \<open>\<open>min/max\<close> as special case of lattice\<close>
   2.611  
   2.612  context linorder
   2.613 @@ -749,64 +698,48 @@
   2.614    + max: semilattice_order max greater_eq greater
   2.615    by standard (auto simp add: min_def max_def)
   2.616  
   2.617 -lemma min_le_iff_disj:
   2.618 -  "min x y \<le> z \<longleftrightarrow> x \<le> z \<or> y \<le> z"
   2.619 +lemma min_le_iff_disj: "min x y \<le> z \<longleftrightarrow> x \<le> z \<or> y \<le> z"
   2.620    unfolding min_def using linear by (auto intro: order_trans)
   2.621  
   2.622 -lemma le_max_iff_disj:
   2.623 -  "z \<le> max x y \<longleftrightarrow> z \<le> x \<or> z \<le> y"
   2.624 +lemma le_max_iff_disj: "z \<le> max x y \<longleftrightarrow> z \<le> x \<or> z \<le> y"
   2.625    unfolding max_def using linear by (auto intro: order_trans)
   2.626  
   2.627 -lemma min_less_iff_disj:
   2.628 -  "min x y < z \<longleftrightarrow> x < z \<or> y < z"
   2.629 +lemma min_less_iff_disj: "min x y < z \<longleftrightarrow> x < z \<or> y < z"
   2.630    unfolding min_def le_less using less_linear by (auto intro: less_trans)
   2.631  
   2.632 -lemma less_max_iff_disj:
   2.633 -  "z < max x y \<longleftrightarrow> z < x \<or> z < y"
   2.634 +lemma less_max_iff_disj: "z < max x y \<longleftrightarrow> z < x \<or> z < y"
   2.635    unfolding max_def le_less using less_linear by (auto intro: less_trans)
   2.636  
   2.637 -lemma min_less_iff_conj [simp]:
   2.638 -  "z < min x y \<longleftrightarrow> z < x \<and> z < y"
   2.639 +lemma min_less_iff_conj [simp]: "z < min x y \<longleftrightarrow> z < x \<and> z < y"
   2.640    unfolding min_def le_less using less_linear by (auto intro: less_trans)
   2.641  
   2.642 -lemma max_less_iff_conj [simp]:
   2.643 -  "max x y < z \<longleftrightarrow> x < z \<and> y < z"
   2.644 +lemma max_less_iff_conj [simp]: "max x y < z \<longleftrightarrow> x < z \<and> y < z"
   2.645    unfolding max_def le_less using less_linear by (auto intro: less_trans)
   2.646  
   2.647 -lemma min_max_distrib1:
   2.648 -  "min (max b c) a = max (min b a) (min c a)"
   2.649 +lemma min_max_distrib1: "min (max b c) a = max (min b a) (min c a)"
   2.650    by (auto simp add: min_def max_def not_le dest: le_less_trans less_trans intro: antisym)
   2.651  
   2.652 -lemma min_max_distrib2:
   2.653 -  "min a (max b c) = max (min a b) (min a c)"
   2.654 +lemma min_max_distrib2: "min a (max b c) = max (min a b) (min a c)"
   2.655    by (auto simp add: min_def max_def not_le dest: le_less_trans less_trans intro: antisym)
   2.656  
   2.657 -lemma max_min_distrib1:
   2.658 -  "max (min b c) a = min (max b a) (max c a)"
   2.659 +lemma max_min_distrib1: "max (min b c) a = min (max b a) (max c a)"
   2.660    by (auto simp add: min_def max_def not_le dest: le_less_trans less_trans intro: antisym)
   2.661  
   2.662 -lemma max_min_distrib2:
   2.663 -  "max a (min b c) = min (max a b) (max a c)"
   2.664 +lemma max_min_distrib2: "max a (min b c) = min (max a b) (max a c)"
   2.665    by (auto simp add: min_def max_def not_le dest: le_less_trans less_trans intro: antisym)
   2.666  
   2.667  lemmas min_max_distribs = min_max_distrib1 min_max_distrib2 max_min_distrib1 max_min_distrib2
   2.668  
   2.669 -lemma split_min [no_atp]:
   2.670 -  "P (min i j) \<longleftrightarrow> (i \<le> j \<longrightarrow> P i) \<and> (\<not> i \<le> j \<longrightarrow> P j)"
   2.671 +lemma split_min [no_atp]: "P (min i j) \<longleftrightarrow> (i \<le> j \<longrightarrow> P i) \<and> (\<not> i \<le> j \<longrightarrow> P j)"
   2.672    by (simp add: min_def)
   2.673  
   2.674 -lemma split_max [no_atp]:
   2.675 -  "P (max i j) \<longleftrightarrow> (i \<le> j \<longrightarrow> P j) \<and> (\<not> i \<le> j \<longrightarrow> P i)"
   2.676 +lemma split_max [no_atp]: "P (max i j) \<longleftrightarrow> (i \<le> j \<longrightarrow> P j) \<and> (\<not> i \<le> j \<longrightarrow> P i)"
   2.677    by (simp add: max_def)
   2.678  
   2.679 -lemma min_of_mono:
   2.680 -  fixes f :: "'a \<Rightarrow> 'b::linorder"
   2.681 -  shows "mono f \<Longrightarrow> min (f m) (f n) = f (min m n)"
   2.682 +lemma min_of_mono: "mono f \<Longrightarrow> min (f m) (f n) = f (min m n)" for f :: "'a \<Rightarrow> 'b::linorder"
   2.683    by (auto simp: mono_def Orderings.min_def min_def intro: Orderings.antisym)
   2.684  
   2.685 -lemma max_of_mono:
   2.686 -  fixes f :: "'a \<Rightarrow> 'b::linorder"
   2.687 -  shows "mono f \<Longrightarrow> max (f m) (f n) = f (max m n)"
   2.688 +lemma max_of_mono: "mono f \<Longrightarrow> max (f m) (f n) = f (max m n)" for f :: "'a \<Rightarrow> 'b::linorder"
   2.689    by (auto simp: mono_def Orderings.max_def max_def intro: Orderings.antisym)
   2.690  
   2.691  end
   2.692 @@ -821,27 +754,33 @@
   2.693  subsection \<open>Uniqueness of inf and sup\<close>
   2.694  
   2.695  lemma (in semilattice_inf) inf_unique:
   2.696 -  fixes f (infixl "\<triangle>" 70)
   2.697 -  assumes le1: "\<And>x y. x \<triangle> y \<sqsubseteq> x" and le2: "\<And>x y. x \<triangle> y \<sqsubseteq> y"
   2.698 -  and greatest: "\<And>x y z. x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<triangle> z"
   2.699 +  fixes f  (infixl "\<triangle>" 70)
   2.700 +  assumes le1: "\<And>x y. x \<triangle> y \<sqsubseteq> x"
   2.701 +    and le2: "\<And>x y. x \<triangle> y \<sqsubseteq> y"
   2.702 +    and greatest: "\<And>x y z. x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<triangle> z"
   2.703    shows "x \<sqinter> y = x \<triangle> y"
   2.704  proof (rule antisym)
   2.705 -  show "x \<triangle> y \<sqsubseteq> x \<sqinter> y" by (rule le_infI) (rule le1, rule le2)
   2.706 -next
   2.707 -  have leI: "\<And>x y z. x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<triangle> z" by (blast intro: greatest)
   2.708 -  show "x \<sqinter> y \<sqsubseteq> x \<triangle> y" by (rule leI) simp_all
   2.709 +  show "x \<triangle> y \<sqsubseteq> x \<sqinter> y"
   2.710 +    by (rule le_infI) (rule le1, rule le2)
   2.711 +  have leI: "\<And>x y z. x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<triangle> z"
   2.712 +    by (blast intro: greatest)
   2.713 +  show "x \<sqinter> y \<sqsubseteq> x \<triangle> y"
   2.714 +    by (rule leI) simp_all
   2.715  qed
   2.716  
   2.717  lemma (in semilattice_sup) sup_unique:
   2.718 -  fixes f (infixl "\<nabla>" 70)
   2.719 -  assumes ge1 [simp]: "\<And>x y. x \<sqsubseteq> x \<nabla> y" and ge2: "\<And>x y. y \<sqsubseteq> x \<nabla> y"
   2.720 -  and least: "\<And>x y z. y \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> x \<Longrightarrow> y \<nabla> z \<sqsubseteq> x"
   2.721 +  fixes f  (infixl "\<nabla>" 70)
   2.722 +  assumes ge1 [simp]: "\<And>x y. x \<sqsubseteq> x \<nabla> y"
   2.723 +    and ge2: "\<And>x y. y \<sqsubseteq> x \<nabla> y"
   2.724 +    and least: "\<And>x y z. y \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> x \<Longrightarrow> y \<nabla> z \<sqsubseteq> x"
   2.725    shows "x \<squnion> y = x \<nabla> y"
   2.726  proof (rule antisym)
   2.727 -  show "x \<squnion> y \<sqsubseteq> x \<nabla> y" by (rule le_supI) (rule ge1, rule ge2)
   2.728 -next
   2.729 -  have leI: "\<And>x y z. x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<nabla> y \<sqsubseteq> z" by (blast intro: least)
   2.730 -  show "x \<nabla> y \<sqsubseteq> x \<squnion> y" by (rule leI) simp_all
   2.731 +  show "x \<squnion> y \<sqsubseteq> x \<nabla> y"
   2.732 +    by (rule le_supI) (rule ge1, rule ge2)
   2.733 +  have leI: "\<And>x y z. x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<nabla> y \<sqsubseteq> z"
   2.734 +    by (blast intro: least)
   2.735 +  show "x \<nabla> y \<sqsubseteq> x \<squnion> y"
   2.736 +    by (rule leI) simp_all
   2.737  qed
   2.738  
   2.739  
   2.740 @@ -850,33 +789,25 @@
   2.741  instantiation bool :: boolean_algebra
   2.742  begin
   2.743  
   2.744 -definition
   2.745 -  bool_Compl_def [simp]: "uminus = Not"
   2.746 +definition bool_Compl_def [simp]: "uminus = Not"
   2.747  
   2.748 -definition
   2.749 -  bool_diff_def [simp]: "A - B \<longleftrightarrow> A \<and> \<not> B"
   2.750 +definition bool_diff_def [simp]: "A - B \<longleftrightarrow> A \<and> \<not> B"
   2.751  
   2.752 -definition
   2.753 -  [simp]: "P \<sqinter> Q \<longleftrightarrow> P \<and> Q"
   2.754 +definition [simp]: "P \<sqinter> Q \<longleftrightarrow> P \<and> Q"
   2.755  
   2.756 -definition
   2.757 -  [simp]: "P \<squnion> Q \<longleftrightarrow> P \<or> Q"
   2.758 +definition [simp]: "P \<squnion> Q \<longleftrightarrow> P \<or> Q"
   2.759  
   2.760 -instance proof
   2.761 -qed auto
   2.762 +instance by standard auto
   2.763  
   2.764  end
   2.765  
   2.766 -lemma sup_boolI1:
   2.767 -  "P \<Longrightarrow> P \<squnion> Q"
   2.768 +lemma sup_boolI1: "P \<Longrightarrow> P \<squnion> Q"
   2.769    by simp
   2.770  
   2.771 -lemma sup_boolI2:
   2.772 -  "Q \<Longrightarrow> P \<squnion> Q"
   2.773 +lemma sup_boolI2: "Q \<Longrightarrow> P \<squnion> Q"
   2.774    by simp
   2.775  
   2.776 -lemma sup_boolE:
   2.777 -  "P \<squnion> Q \<Longrightarrow> (P \<Longrightarrow> R) \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R"
   2.778 +lemma sup_boolE: "P \<squnion> Q \<Longrightarrow> (P \<Longrightarrow> R) \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R"
   2.779    by auto
   2.780  
   2.781  
   2.782 @@ -885,48 +816,40 @@
   2.783  instantiation "fun" :: (type, semilattice_sup) semilattice_sup
   2.784  begin
   2.785  
   2.786 -definition
   2.787 -  "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)"
   2.788 +definition "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)"
   2.789  
   2.790 -lemma sup_apply [simp, code]:
   2.791 -  "(f \<squnion> g) x = f x \<squnion> g x"
   2.792 +lemma sup_apply [simp, code]: "(f \<squnion> g) x = f x \<squnion> g x"
   2.793    by (simp add: sup_fun_def)
   2.794  
   2.795 -instance proof
   2.796 -qed (simp_all add: le_fun_def)
   2.797 +instance by standard (simp_all add: le_fun_def)
   2.798  
   2.799  end
   2.800  
   2.801  instantiation "fun" :: (type, semilattice_inf) semilattice_inf
   2.802  begin
   2.803  
   2.804 -definition
   2.805 -  "f \<sqinter> g = (\<lambda>x. f x \<sqinter> g x)"
   2.806 +definition "f \<sqinter> g = (\<lambda>x. f x \<sqinter> g x)"
   2.807  
   2.808 -lemma inf_apply [simp, code]:
   2.809 -  "(f \<sqinter> g) x = f x \<sqinter> g x"
   2.810 +lemma inf_apply [simp, code]: "(f \<sqinter> g) x = f x \<sqinter> g x"
   2.811    by (simp add: inf_fun_def)
   2.812  
   2.813 -instance proof
   2.814 -qed (simp_all add: le_fun_def)
   2.815 +instance by standard (simp_all add: le_fun_def)
   2.816  
   2.817  end
   2.818  
   2.819  instance "fun" :: (type, lattice) lattice ..
   2.820  
   2.821 -instance "fun" :: (type, distrib_lattice) distrib_lattice proof
   2.822 -qed (rule ext, simp add: sup_inf_distrib1)
   2.823 +instance "fun" :: (type, distrib_lattice) distrib_lattice
   2.824 +  by standard (rule ext, simp add: sup_inf_distrib1)
   2.825  
   2.826  instance "fun" :: (type, bounded_lattice) bounded_lattice ..
   2.827  
   2.828  instantiation "fun" :: (type, uminus) uminus
   2.829  begin
   2.830  
   2.831 -definition
   2.832 -  fun_Compl_def: "- A = (\<lambda>x. - A x)"
   2.833 +definition fun_Compl_def: "- A = (\<lambda>x. - A x)"
   2.834  
   2.835 -lemma uminus_apply [simp, code]:
   2.836 -  "(- A) x = - (A x)"
   2.837 +lemma uminus_apply [simp, code]: "(- A) x = - (A x)"
   2.838    by (simp add: fun_Compl_def)
   2.839  
   2.840  instance ..
   2.841 @@ -936,19 +859,17 @@
   2.842  instantiation "fun" :: (type, minus) minus
   2.843  begin
   2.844  
   2.845 -definition
   2.846 -  fun_diff_def: "A - B = (\<lambda>x. A x - B x)"
   2.847 +definition fun_diff_def: "A - B = (\<lambda>x. A x - B x)"
   2.848  
   2.849 -lemma minus_apply [simp, code]:
   2.850 -  "(A - B) x = A x - B x"
   2.851 +lemma minus_apply [simp, code]: "(A - B) x = A x - B x"
   2.852    by (simp add: fun_diff_def)
   2.853  
   2.854  instance ..
   2.855  
   2.856  end
   2.857  
   2.858 -instance "fun" :: (type, boolean_algebra) boolean_algebra proof
   2.859 -qed (rule ext, simp_all add: inf_compl_bot sup_compl_top diff_eq)+
   2.860 +instance "fun" :: (type, boolean_algebra) boolean_algebra
   2.861 +  by standard (rule ext, simp_all add: inf_compl_bot sup_compl_top diff_eq)+
   2.862  
   2.863  
   2.864  subsection \<open>Lattice on unary and binary predicates\<close>
   2.865 @@ -995,10 +916,7 @@
   2.866  lemma sup2E: "(A \<squnion> B) x y \<Longrightarrow> (A x y \<Longrightarrow> P) \<Longrightarrow> (B x y \<Longrightarrow> P) \<Longrightarrow> P"
   2.867    by (simp add: sup_fun_def) iprover
   2.868  
   2.869 -text \<open>
   2.870 -  \medskip Classical introduction rule: no commitment to \<open>A\<close> vs
   2.871 -  \<open>B\<close>.
   2.872 -\<close>
   2.873 +text \<open> \<^medskip> Classical introduction rule: no commitment to \<open>A\<close> vs \<open>B\<close>.\<close>
   2.874  
   2.875  lemma sup1CI: "(\<not> B x \<Longrightarrow> A x) \<Longrightarrow> (A \<squnion> B) x"
   2.876    by (auto simp add: sup_fun_def)
   2.877 @@ -1012,4 +930,3 @@
   2.878    less (infix "\<sqsubset>" 50)
   2.879  
   2.880  end
   2.881 -