diff --git a/src/HOL/Fun.thy b/src/HOL/Fun.thy
--- a/src/HOL/Fun.thy
+++ b/src/HOL/Fun.thy
@@ -1,1055 +1,1055 @@
 (*  Title:      HOL/Fun.thy
     Author:     Tobias Nipkow, Cambridge University Computer Laboratory
     Author:     Andrei Popescu, TU Muenchen
     Copyright   1994, 2012
 *)
 
 section \<open>Notions about functions\<close>
 
 theory Fun
   imports Set
   keywords "functor" :: thy_goal_defn
 begin
 
 lemma apply_inverse: "f x = u \<Longrightarrow> (\<And>x. P x \<Longrightarrow> g (f x) = x) \<Longrightarrow> P x \<Longrightarrow> x = g u"
   by auto
 
 text \<open>Uniqueness, so NOT the axiom of choice.\<close>
 lemma uniq_choice: "\<forall>x. \<exists>!y. Q x y \<Longrightarrow> \<exists>f. \<forall>x. Q x (f x)"
   by (force intro: theI')
 
 lemma b_uniq_choice: "\<forall>x\<in>S. \<exists>!y. Q x y \<Longrightarrow> \<exists>f. \<forall>x\<in>S. Q x (f x)"
   by (force intro: theI')
 
 
 subsection \<open>The Identity Function \<open>id\<close>\<close>
 
 definition id :: "'a \<Rightarrow> 'a"
   where "id = (\<lambda>x. x)"
 
 lemma id_apply [simp]: "id x = x"
   by (simp add: id_def)
 
 lemma image_id [simp]: "image id = id"
   by (simp add: id_def fun_eq_iff)
 
 lemma vimage_id [simp]: "vimage id = id"
   by (simp add: id_def fun_eq_iff)
 
 lemma eq_id_iff: "(\<forall>x. f x = x) \<longleftrightarrow> f = id"
   by auto
 
 code_printing
   constant id \<rightharpoonup> (Haskell) "id"
 
 
 subsection \<open>The Composition Operator \<open>f \<circ> g\<close>\<close>
 
 definition comp :: "('b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c"  (infixl "\<circ>" 55)
   where "f \<circ> g = (\<lambda>x. f (g x))"
 
 notation (ASCII)
   comp  (infixl "o" 55)
 
 lemma comp_apply [simp]: "(f \<circ> g) x = f (g x)"
   by (simp add: comp_def)
 
 lemma comp_assoc: "(f \<circ> g) \<circ> h = f \<circ> (g \<circ> h)"
   by (simp add: fun_eq_iff)
 
 lemma id_comp [simp]: "id \<circ> g = g"
   by (simp add: fun_eq_iff)
 
 lemma comp_id [simp]: "f \<circ> id = f"
   by (simp add: fun_eq_iff)
 
 lemma comp_eq_dest: "a \<circ> b = c \<circ> d \<Longrightarrow> a (b v) = c (d v)"
   by (simp add: fun_eq_iff)
 
 lemma comp_eq_elim: "a \<circ> b = c \<circ> d \<Longrightarrow> ((\<And>v. a (b v) = c (d v)) \<Longrightarrow> R) \<Longrightarrow> R"
   by (simp add: fun_eq_iff)
 
 lemma comp_eq_dest_lhs: "a \<circ> b = c \<Longrightarrow> a (b v) = c v"
   by clarsimp
 
 lemma comp_eq_id_dest: "a \<circ> b = id \<circ> c \<Longrightarrow> a (b v) = c v"
   by clarsimp
 
 lemma image_comp: "f ` (g ` r) = (f \<circ> g) ` r"
   by auto
 
 lemma vimage_comp: "f -` (g -` x) = (g \<circ> f) -` x"
   by auto
 
 lemma image_eq_imp_comp: "f ` A = g ` B \<Longrightarrow> (h \<circ> f) ` A = (h \<circ> g) ` B"
   by (auto simp: comp_def elim!: equalityE)
 
 lemma image_bind: "f ` (Set.bind A g) = Set.bind A ((`) f \<circ> g)"
   by (auto simp add: Set.bind_def)
 
 lemma bind_image: "Set.bind (f ` A) g = Set.bind A (g \<circ> f)"
   by (auto simp add: Set.bind_def)
 
 lemma (in group_add) minus_comp_minus [simp]: "uminus \<circ> uminus = id"
   by (simp add: fun_eq_iff)
 
 lemma (in boolean_algebra) minus_comp_minus [simp]: "uminus \<circ> uminus = id"
   by (simp add: fun_eq_iff)
 
 code_printing
   constant comp \<rightharpoonup> (SML) infixl 5 "o" and (Haskell) infixr 9 "."
 
 
 subsection \<open>The Forward Composition Operator \<open>fcomp\<close>\<close>
 
 definition fcomp :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'c"  (infixl "\<circ>>" 60)
   where "f \<circ>> g = (\<lambda>x. g (f x))"
 
 lemma fcomp_apply [simp]:  "(f \<circ>> g) x = g (f x)"
   by (simp add: fcomp_def)
 
 lemma fcomp_assoc: "(f \<circ>> g) \<circ>> h = f \<circ>> (g \<circ>> h)"
   by (simp add: fcomp_def)
 
 lemma id_fcomp [simp]: "id \<circ>> g = g"
   by (simp add: fcomp_def)
 
 lemma fcomp_id [simp]: "f \<circ>> id = f"
   by (simp add: fcomp_def)
 
 lemma fcomp_comp: "fcomp f g = comp g f"
   by (simp add: ext)
 
 code_printing
   constant fcomp \<rightharpoonup> (Eval) infixl 1 "#>"
 
 no_notation fcomp (infixl "\<circ>>" 60)
 
 
 subsection \<open>Mapping functions\<close>
 
 definition map_fun :: "('c \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'c \<Rightarrow> 'd"
   where "map_fun f g h = g \<circ> h \<circ> f"
 
 lemma map_fun_apply [simp]: "map_fun f g h x = g (h (f x))"
   by (simp add: map_fun_def)
 
 
 subsection \<open>Injectivity and Bijectivity\<close>
 
 definition inj_on :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> bool"  \<comment> \<open>injective\<close>
   where "inj_on f A \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>A. f x = f y \<longrightarrow> x = y)"
 
 definition bij_betw :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> bool"  \<comment> \<open>bijective\<close>
   where "bij_betw f A B \<longleftrightarrow> inj_on f A \<and> f ` A = B"
 
 text \<open>
   A common special case: functions injective, surjective or bijective over
   the entire domain type.
 \<close>
 
 abbreviation inj :: "('a \<Rightarrow> 'b) \<Rightarrow> bool"
   where "inj f \<equiv> inj_on f UNIV"
 
 abbreviation surj :: "('a \<Rightarrow> 'b) \<Rightarrow> bool"
   where "surj f \<equiv> range f = UNIV"
 
 translations \<comment> \<open>The negated case:\<close>
   "\<not> CONST surj f" \<leftharpoondown> "CONST range f \<noteq> CONST UNIV"
 
 abbreviation bij :: "('a \<Rightarrow> 'b) \<Rightarrow> bool"
   where "bij f \<equiv> bij_betw f UNIV UNIV"
 
 lemma inj_def: "inj f \<longleftrightarrow> (\<forall>x y. f x = f y \<longrightarrow> x = y)"
   unfolding inj_on_def by blast
 
 lemma injI: "(\<And>x y. f x = f y \<Longrightarrow> x = y) \<Longrightarrow> inj f"
   unfolding inj_def by blast
 
 theorem range_ex1_eq: "inj f \<Longrightarrow> b \<in> range f \<longleftrightarrow> (\<exists>!x. b = f x)"
   unfolding inj_def by blast
 
 lemma injD: "inj f \<Longrightarrow> f x = f y \<Longrightarrow> x = y"
   by (simp add: inj_def)
 
 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"
   by (auto simp: inj_on_def)
 
 lemma inj_on_cong: "(\<And>a. a \<in> A \<Longrightarrow> f a = g a) \<Longrightarrow> inj_on f A \<longleftrightarrow> inj_on g A"
   by (auto simp: inj_on_def)
 
 lemma inj_on_strict_subset: "inj_on f B \<Longrightarrow> A \<subset> B \<Longrightarrow> f ` A \<subset> f ` B"
   unfolding inj_on_def by blast
 
 lemma inj_compose: "inj f \<Longrightarrow> inj g \<Longrightarrow> inj (f \<circ> g)"
   by (simp add: inj_def)
 
 lemma inj_fun: "inj f \<Longrightarrow> inj (\<lambda>x y. f x)"
   by (simp add: inj_def fun_eq_iff)
 
 lemma inj_eq: "inj f \<Longrightarrow> f x = f y \<longleftrightarrow> x = y"
   by (simp add: inj_on_eq_iff)
 
 lemma inj_on_id[simp]: "inj_on id A"
   by (simp add: inj_on_def)
 
 lemma inj_on_id2[simp]: "inj_on (\<lambda>x. x) A"
   by (simp add: inj_on_def)
 
 lemma inj_on_Int: "inj_on f A \<or> inj_on f B \<Longrightarrow> inj_on f (A \<inter> B)"
   unfolding inj_on_def by blast
 
 lemma surj_id: "surj id"
   by simp
 
 lemma bij_id[simp]: "bij id"
   by (simp add: bij_betw_def)
 
 lemma bij_uminus: "bij (uminus :: 'a \<Rightarrow> 'a::ab_group_add)"
   unfolding bij_betw_def inj_on_def
   by (force intro: minus_minus [symmetric])
 
 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"
   by (simp add: inj_on_def)
 
 lemma inj_on_inverseI: "(\<And>x. x \<in> A \<Longrightarrow> g (f x) = x) \<Longrightarrow> inj_on f A"
   by (auto dest: arg_cong [of concl: g] simp add: inj_on_def)
 
 lemma inj_onD: "inj_on f A \<Longrightarrow> f x = f y \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x = y"
   unfolding inj_on_def by blast
 
 lemma inj_on_subset:
   assumes "inj_on f A"
     and "B \<subseteq> A"
   shows "inj_on f B"
 proof (rule inj_onI)
   fix a b
   assume "a \<in> B" and "b \<in> B"
   with assms have "a \<in> A" and "b \<in> A"
     by auto
   moreover assume "f a = f b"
   ultimately show "a = b"
     using assms by (auto dest: inj_onD)
 qed
 
 lemma comp_inj_on: "inj_on f A \<Longrightarrow> inj_on g (f ` A) \<Longrightarrow> inj_on (g \<circ> f) A"
   by (simp add: comp_def inj_on_def)
 
 lemma inj_on_imageI: "inj_on (g \<circ> f) A \<Longrightarrow> inj_on g (f ` A)"
   by (auto simp add: inj_on_def)
 
 lemma inj_on_image_iff:
   "\<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) \<longleftrightarrow> inj_on g A"
   unfolding inj_on_def by blast
 
 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"
   unfolding inj_on_def by blast
 
 lemma inj_singleton [simp]: "inj_on (\<lambda>x. {x}) A"
   by (simp add: inj_on_def)
 
 lemma inj_on_empty[iff]: "inj_on f {}"
   by (simp add: inj_on_def)
 
 lemma subset_inj_on: "inj_on f B \<Longrightarrow> A \<subseteq> B \<Longrightarrow> inj_on f A"
   unfolding inj_on_def by blast
 
 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) = {}"
   unfolding inj_on_def by (blast intro: sym)
 
 lemma inj_on_insert [iff]: "inj_on f (insert a A) \<longleftrightarrow> inj_on f A \<and> f a \<notin> f ` (A - {a})"
   unfolding inj_on_def by (blast intro: sym)
 
 lemma inj_on_diff: "inj_on f A \<Longrightarrow> inj_on f (A - B)"
   unfolding inj_on_def by blast
 
 lemma comp_inj_on_iff: "inj_on f A \<Longrightarrow> inj_on f' (f ` A) \<longleftrightarrow> inj_on (f' \<circ> f) A"
   by (auto simp: comp_inj_on inj_on_def)
 
 lemma inj_on_imageI2: "inj_on (f' \<circ> f) A \<Longrightarrow> inj_on f A"
   by (auto simp: comp_inj_on inj_on_def)
 
 lemma inj_img_insertE:
   assumes "inj_on f A"
   assumes "x \<notin> B"
     and "insert x B = f ` A"
   obtains x' A' where "x' \<notin> A'" and "A = insert x' A'" and "x = f x'" and "B = f ` A'"
 proof -
   from assms have "x \<in> f ` A" by auto
   then obtain x' where *: "x' \<in> A" "x = f x'" by auto
   then have A: "A = insert x' (A - {x'})" by auto
   with assms * have B: "B = f ` (A - {x'})" by (auto dest: inj_on_contraD)
   have "x' \<notin> A - {x'}" by simp
   from this A \<open>x = f x'\<close> B show ?thesis ..
 qed
 
 lemma linorder_inj_onI:
   fixes A :: "'a::order set"
   assumes ne: "\<And>x y. \<lbrakk>x < y; x\<in>A; y\<in>A\<rbrakk> \<Longrightarrow> f x \<noteq> f y" and lin: "\<And>x y. \<lbrakk>x\<in>A; y\<in>A\<rbrakk> \<Longrightarrow> x\<le>y \<or> y\<le>x"
   shows "inj_on f A"
 proof (rule inj_onI)
   fix x y
   assume eq: "f x = f y" and "x\<in>A" "y\<in>A"
   then show "x = y"
     using lin [of x y] ne by (force simp: dual_order.order_iff_strict)
 qed
 
 lemma linorder_injI:
   assumes "\<And>x y::'a::linorder. x < y \<Longrightarrow> f x \<noteq> f y"
   shows "inj f"
     \<comment> \<open>Courtesy of Stephan Merz\<close>
 using assms by (auto intro: linorder_inj_onI linear)
 
 lemma inj_on_image_Pow: "inj_on f A \<Longrightarrow>inj_on (image f) (Pow A)"
   unfolding Pow_def inj_on_def by blast
 
 lemma bij_betw_image_Pow: "bij_betw f A B \<Longrightarrow> bij_betw (image f) (Pow A) (Pow B)"
   by (auto simp add: bij_betw_def inj_on_image_Pow image_Pow_surj)
 
 lemma surj_def: "surj f \<longleftrightarrow> (\<forall>y. \<exists>x. y = f x)"
   by auto
 
 lemma surjI:
   assumes "\<And>x. g (f x) = x"
   shows "surj g"
   using assms [symmetric] by auto
 
 lemma surjD: "surj f \<Longrightarrow> \<exists>x. y = f x"
   by (simp add: surj_def)
 
 lemma surjE: "surj f \<Longrightarrow> (\<And>x. y = f x \<Longrightarrow> C) \<Longrightarrow> C"
   by (simp add: surj_def) blast
 
 lemma comp_surj: "surj f \<Longrightarrow> surj g \<Longrightarrow> surj (g \<circ> f)"
   using image_comp [of g f UNIV] by simp
 
 lemma bij_betw_imageI: "inj_on f A \<Longrightarrow> f ` A = B \<Longrightarrow> bij_betw f A B"
   unfolding bij_betw_def by clarify
 
 lemma bij_betw_imp_surj_on: "bij_betw f A B \<Longrightarrow> f ` A = B"
   unfolding bij_betw_def by clarify
 
 lemma bij_betw_imp_surj: "bij_betw f A UNIV \<Longrightarrow> surj f"
   unfolding bij_betw_def by auto
 
 lemma bij_betw_empty1: "bij_betw f {} A \<Longrightarrow> A = {}"
   unfolding bij_betw_def by blast
 
 lemma bij_betw_empty2: "bij_betw f A {} \<Longrightarrow> A = {}"
   unfolding bij_betw_def by blast
 
 lemma inj_on_imp_bij_betw: "inj_on f A \<Longrightarrow> bij_betw f A (f ` A)"
   unfolding bij_betw_def by simp
 
 lemma bij_betw_apply: "\<lbrakk>bij_betw f A B; a \<in> A\<rbrakk> \<Longrightarrow> f a \<in> B"
   unfolding bij_betw_def by auto
 
 lemma bij_def: "bij f \<longleftrightarrow> inj f \<and> surj f"
   by (rule bij_betw_def)
 
 lemma bijI: "inj f \<Longrightarrow> surj f \<Longrightarrow> bij f"
   by (rule bij_betw_imageI)
 
 lemma bij_is_inj: "bij f \<Longrightarrow> inj f"
   by (simp add: bij_def)
 
 lemma bij_is_surj: "bij f \<Longrightarrow> surj f"
   by (simp add: bij_def)
 
 lemma bij_betw_imp_inj_on: "bij_betw f A B \<Longrightarrow> inj_on f A"
   by (simp add: bij_betw_def)
 
 lemma bij_betw_trans: "bij_betw f A B \<Longrightarrow> bij_betw g B C \<Longrightarrow> bij_betw (g \<circ> f) A C"
   by (auto simp add:bij_betw_def comp_inj_on)
 
 lemma bij_comp: "bij f \<Longrightarrow> bij g \<Longrightarrow> bij (g \<circ> f)"
   by (rule bij_betw_trans)
 
 lemma bij_betw_comp_iff: "bij_betw f A A' \<Longrightarrow> bij_betw f' A' A'' \<longleftrightarrow> bij_betw (f' \<circ> f) A A''"
   by (auto simp add: bij_betw_def inj_on_def)
 
 lemma bij_betw_comp_iff2:
   assumes bij: "bij_betw f' A' A''"
     and img: "f ` A \<le> A'"
   shows "bij_betw f A A' \<longleftrightarrow> bij_betw (f' \<circ> f) A A''"
   using assms
 proof (auto simp add: bij_betw_comp_iff)
   assume *: "bij_betw (f' \<circ> f) A A''"
   then show "bij_betw f A A'"
     using img
   proof (auto simp add: bij_betw_def)
     assume "inj_on (f' \<circ> f) A"
     then show "inj_on f A"
       using inj_on_imageI2 by blast
   next
     fix a'
     assume **: "a' \<in> A'"
     with bij have "f' a' \<in> A''"
       unfolding bij_betw_def by auto
     with * obtain a where 1: "a \<in> A \<and> f' (f a) = f' a'"
       unfolding bij_betw_def by force
     with img have "f a \<in> A'" by auto
     with bij ** 1 have "f a = a'"
       unfolding bij_betw_def inj_on_def by auto
     with 1 show "a' \<in> f ` A" by auto
   qed
 qed
 
 lemma bij_betw_inv:
   assumes "bij_betw f A B"
   shows "\<exists>g. bij_betw g B A"
 proof -
   have i: "inj_on f A" and s: "f ` A = B"
     using assms by (auto simp: bij_betw_def)
   let ?P = "\<lambda>b a. a \<in> A \<and> f a = b"
   let ?g = "\<lambda>b. The (?P b)"
   have g: "?g b = a" if P: "?P b a" for a b
   proof -
     from that s have ex1: "\<exists>a. ?P b a" by blast
     then have uex1: "\<exists>!a. ?P b a" by (blast dest:inj_onD[OF i])
     then show ?thesis
       using the1_equality[OF uex1, OF P] P by simp
   qed
   have "inj_on ?g B"
   proof (rule inj_onI)
     fix x y
     assume "x \<in> B" "y \<in> B" "?g x = ?g y"
     from s \<open>x \<in> B\<close> obtain a1 where a1: "?P x a1" by blast
     from s \<open>y \<in> B\<close> obtain a2 where a2: "?P y a2" by blast
     from g [OF a1] a1 g [OF a2] a2 \<open>?g x = ?g y\<close> show "x = y" by simp
   qed
   moreover have "?g ` B = A"
   proof (auto simp: image_def)
     fix b
     assume "b \<in> B"
     with s obtain a where P: "?P b a" by blast
     with g[OF P] show "?g b \<in> A" by auto
   next
     fix a
     assume "a \<in> A"
     with s obtain b where P: "?P b a" by blast
     with s have "b \<in> B" by blast
     with g[OF P] show "\<exists>b\<in>B. a = ?g b" by blast
   qed
   ultimately show ?thesis
     by (auto simp: bij_betw_def)
 qed
 
 lemma bij_betw_cong: "(\<And>a. a \<in> A \<Longrightarrow> f a = g a) \<Longrightarrow> bij_betw f A A' = bij_betw g A A'"
   unfolding bij_betw_def inj_on_def by safe force+  (* somewhat slow *)
 
 lemma bij_betw_id[intro, simp]: "bij_betw id A A"
   unfolding bij_betw_def id_def by auto
 
 lemma bij_betw_id_iff: "bij_betw id A B \<longleftrightarrow> A = B"
   by (auto simp add: bij_betw_def)
 
 lemma bij_betw_combine:
   "bij_betw f A B \<Longrightarrow> bij_betw f C D \<Longrightarrow> B \<inter> D = {} \<Longrightarrow> bij_betw f (A \<union> C) (B \<union> D)"
   unfolding bij_betw_def inj_on_Un image_Un by auto
 
 lemma bij_betw_subset: "bij_betw f A A' \<Longrightarrow> B \<subseteq> A \<Longrightarrow> f ` B = B' \<Longrightarrow> bij_betw f B B'"
   by (auto simp add: bij_betw_def inj_on_def)
 
 lemma bij_pointE:
   assumes "bij f"
   obtains x where "y = f x" and "\<And>x'. y = f x' \<Longrightarrow> x' = x"
 proof -
   from assms have "inj f" by (rule bij_is_inj)
   moreover from assms have "surj f" by (rule bij_is_surj)
   then have "y \<in> range f" by simp
   ultimately have "\<exists>!x. y = f x" by (simp add: range_ex1_eq)
   with that show thesis by blast
 qed
 
 lemma surj_image_vimage_eq: "surj f \<Longrightarrow> f ` (f -` A) = A"
   by simp
 
 lemma surj_vimage_empty:
   assumes "surj f"
   shows "f -` A = {} \<longleftrightarrow> A = {}"
   using surj_image_vimage_eq [OF \<open>surj f\<close>, of A]
   by (intro iffI) fastforce+
 
 lemma inj_vimage_image_eq: "inj f \<Longrightarrow> f -` (f ` A) = A"
   unfolding inj_def by blast
 
 lemma vimage_subsetD: "surj f \<Longrightarrow> f -` B \<subseteq> A \<Longrightarrow> B \<subseteq> f ` A"
   by (blast intro: sym)
 
 lemma vimage_subsetI: "inj f \<Longrightarrow> B \<subseteq> f ` A \<Longrightarrow> f -` B \<subseteq> A"
   unfolding inj_def by blast
 
 lemma vimage_subset_eq: "bij f \<Longrightarrow> f -` B \<subseteq> A \<longleftrightarrow> B \<subseteq> f ` A"
   unfolding bij_def by (blast del: subsetI intro: vimage_subsetI vimage_subsetD)
 
 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"
   by (fastforce simp: inj_on_def)
 
 lemma inj_on_Un_image_eq_iff: "inj_on f (A \<union> B) \<Longrightarrow> f ` A = f ` B \<longleftrightarrow> A = B"
   by (erule inj_on_image_eq_iff) simp_all
 
 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"
   unfolding inj_on_def by blast
 
 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"
   unfolding inj_on_def by blast
 
 lemma image_Int: "inj f \<Longrightarrow> f ` (A \<inter> B) = f ` A \<inter> f ` B"
   unfolding inj_def by blast
 
 lemma image_set_diff: "inj f \<Longrightarrow> f ` (A - B) = f ` A - f ` B"
   unfolding inj_def by blast
 
 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"
   by (auto simp: inj_on_def)
 
 (*FIXME DELETE*)
 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"
   by (blast dest: inj_onD)
 
 lemma inj_image_mem_iff: "inj f \<Longrightarrow> f a \<in> f ` A \<longleftrightarrow> a \<in> A"
   by (blast dest: injD)
 
 lemma inj_image_subset_iff: "inj f \<Longrightarrow> f ` A \<subseteq> f ` B \<longleftrightarrow> A \<subseteq> B"
   by (blast dest: injD)
 
 lemma inj_image_eq_iff: "inj f \<Longrightarrow> f ` A = f ` B \<longleftrightarrow> A = B"
   by (blast dest: injD)
 
 lemma surj_Compl_image_subset: "surj f \<Longrightarrow> - (f ` A) \<subseteq> f ` (- A)"
   by auto
 
 lemma inj_image_Compl_subset: "inj f \<Longrightarrow> f ` (- A) \<subseteq> - (f ` A)"
   by (auto simp: inj_def)
 
 lemma bij_image_Compl_eq: "bij f \<Longrightarrow> f ` (- A) = - (f ` A)"
   by (simp add: bij_def inj_image_Compl_subset surj_Compl_image_subset equalityI)
 
 lemma inj_vimage_singleton: "inj f \<Longrightarrow> f -` {a} \<subseteq> {THE x. f x = a}"
   \<comment> \<open>The inverse image of a singleton under an injective function is included in a singleton.\<close>
   by (simp add: inj_def) (blast intro: the_equality [symmetric])
 
 lemma inj_on_vimage_singleton: "inj_on f A \<Longrightarrow> f -` {a} \<inter> A \<subseteq> {THE x. x \<in> A \<and> f x = a}"
   by (auto simp add: inj_on_def intro: the_equality [symmetric])
 
 lemma (in ordered_ab_group_add) inj_uminus[simp, intro]: "inj_on uminus A"
   by (auto intro!: inj_onI)
 
 lemma (in linorder) strict_mono_imp_inj_on: "strict_mono f \<Longrightarrow> inj_on f A"
   by (auto intro!: inj_onI dest: strict_mono_eq)
 
 lemma bij_betw_byWitness:
   assumes left: "\<forall>a \<in> A. f' (f a) = a"
     and right: "\<forall>a' \<in> A'. f (f' a') = a'"
     and "f ` A \<subseteq> A'"
     and img2: "f' ` A' \<subseteq> A"
   shows "bij_betw f A A'"
   using assms
   unfolding bij_betw_def inj_on_def
 proof safe
   fix a b
   assume "a \<in> A" "b \<in> A"
   with left have "a = f' (f a) \<and> b = f' (f b)" by simp
   moreover assume "f a = f b"
   ultimately show "a = b" by simp
 next
   fix a' assume *: "a' \<in> A'"
   with img2 have "f' a' \<in> A" by blast
   moreover from * right have "a' = f (f' a')" by simp
   ultimately show "a' \<in> f ` A" by blast
 qed
 
 corollary notIn_Un_bij_betw:
   assumes "b \<notin> A"
     and "f b \<notin> A'"
     and "bij_betw f A A'"
   shows "bij_betw f (A \<union> {b}) (A' \<union> {f b})"
 proof -
   have "bij_betw f {b} {f b}"
     unfolding bij_betw_def inj_on_def by simp
   with assms show ?thesis
     using bij_betw_combine[of f A A' "{b}" "{f b}"] by blast
 qed
 
 lemma notIn_Un_bij_betw3:
   assumes "b \<notin> A"
     and "f b \<notin> A'"
   shows "bij_betw f A A' = bij_betw f (A \<union> {b}) (A' \<union> {f b})"
 proof
   assume "bij_betw f A A'"
   then show "bij_betw f (A \<union> {b}) (A' \<union> {f b})"
     using assms notIn_Un_bij_betw [of b A f A'] by blast
 next
   assume *: "bij_betw f (A \<union> {b}) (A' \<union> {f b})"
   have "f ` A = A'"
   proof auto
     fix a
     assume **: "a \<in> A"
     then have "f a \<in> A' \<union> {f b}"
       using * unfolding bij_betw_def by blast
     moreover
     have False if "f a = f b"
     proof -
       have "a = b"
         using * ** that unfolding bij_betw_def inj_on_def by blast
       with \<open>b \<notin> A\<close> ** show ?thesis by blast
     qed
     ultimately show "f a \<in> A'" by blast
   next
     fix a'
     assume **: "a' \<in> A'"
     then have "a' \<in> f ` (A \<union> {b})"
       using * by (auto simp add: bij_betw_def)
     then obtain a where 1: "a \<in> A \<union> {b} \<and> f a = a'" by blast
     moreover
     have False if "a = b" using 1 ** \<open>f b \<notin> A'\<close> that by blast
     ultimately have "a \<in> A" by blast
     with 1 show "a' \<in> f ` A" by blast
   qed
   then show "bij_betw f A A'"
     using * bij_betw_subset[of f "A \<union> {b}" _ A] by blast
 qed
 
 text \<open>Important examples\<close>
 
 context cancel_semigroup_add
 begin
 
 lemma inj_on_add [simp]:
   "inj_on ((+) a) A"
   by (rule inj_onI) simp
 
 lemma inj_add_left:
   \<open>inj ((+) a)\<close>
   by simp
 
 lemma inj_on_add' [simp]:
   "inj_on (\<lambda>b. b + a) A"
   by (rule inj_onI) simp
 
 lemma bij_betw_add [simp]:
   "bij_betw ((+) a) A B \<longleftrightarrow> (+) a ` A = B"
   by (simp add: bij_betw_def)
 
 end
 
 context ab_group_add
 begin
 
 lemma surj_plus [simp]:
   "surj ((+) a)"
   by (auto intro!: range_eqI [of b "(+) a" "b - a" for b]) (simp add: algebra_simps)
 
 lemma inj_diff_right [simp]:
   \<open>inj (\<lambda>b. b - a)\<close>
 proof -
   have \<open>inj ((+) (- a))\<close>
     by (fact inj_add_left)
   also have \<open>(+) (- a) = (\<lambda>b. b - a)\<close>
     by (simp add: fun_eq_iff)
   finally show ?thesis .
 qed
 
 lemma surj_diff_right [simp]:
   "surj (\<lambda>x. x - a)"
   using surj_plus [of "- a"] by (simp cong: image_cong_simp)
 
 lemma translation_Compl:
   "(+) a ` (- t) = - ((+) a ` t)"
 proof (rule set_eqI)
   fix b
   show "b \<in> (+) a ` (- t) \<longleftrightarrow> b \<in> - (+) a ` t"
     by (auto simp: image_iff algebra_simps intro!: bexI [of _ "b - a"])
 qed
 
 lemma translation_subtract_Compl:
   "(\<lambda>x. x - a) ` (- t) = - ((\<lambda>x. x - a) ` t)"
   using translation_Compl [of "- a" t] by (simp cong: image_cong_simp)
 
 lemma translation_diff:
   "(+) a ` (s - t) = ((+) a ` s) - ((+) a ` t)"
   by auto
 
 lemma translation_subtract_diff:
   "(\<lambda>x. x - a) ` (s - t) = ((\<lambda>x. x - a) ` s) - ((\<lambda>x. x - a) ` t)"
   using translation_diff [of "- a"] by (simp cong: image_cong_simp)
 
 lemma translation_Int:
   "(+) a ` (s \<inter> t) = ((+) a ` s) \<inter> ((+) a ` t)"
   by auto
 
 lemma translation_subtract_Int:
   "(\<lambda>x. x - a) ` (s \<inter> t) = ((\<lambda>x. x - a) ` s) \<inter> ((\<lambda>x. x - a) ` t)"
   using translation_Int [of " -a"] by (simp cong: image_cong_simp)
 
 end
 
 
 subsection \<open>Function Updating\<close>
 
 definition fun_upd :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)"
   where "fun_upd f a b = (\<lambda>x. if x = a then b else f x)"
 
 nonterminal updbinds and updbind
 
 syntax
   "_updbind" :: "'a \<Rightarrow> 'a \<Rightarrow> updbind"             ("(2_ :=/ _)")
   ""         :: "updbind \<Rightarrow> updbinds"             ("_")
   "_updbinds":: "updbind \<Rightarrow> updbinds \<Rightarrow> updbinds" ("_,/ _")
   "_Update"  :: "'a \<Rightarrow> updbinds \<Rightarrow> 'a"            ("_/'((_)')" [1000, 0] 900)
 
 translations
   "_Update f (_updbinds b bs)" \<rightleftharpoons> "_Update (_Update f b) bs"
   "f(x:=y)" \<rightleftharpoons> "CONST fun_upd f x y"
 
 (* Hint: to define the sum of two functions (or maps), use case_sum.
          A nice infix syntax could be defined by
 notation
   case_sum  (infixr "'(+')"80)
 *)
 
 lemma fun_upd_idem_iff: "f(x:=y) = f \<longleftrightarrow> f x = y"
   unfolding fun_upd_def
   apply safe
    apply (erule subst)
    apply (rule_tac [2] ext)
    apply auto
   done
 
 lemma fun_upd_idem: "f x = y \<Longrightarrow> f(x := y) = f"
   by (simp only: fun_upd_idem_iff)
 
 lemma fun_upd_triv [iff]: "f(x := f x) = f"
   by (simp only: fun_upd_idem)
 
 lemma fun_upd_apply [simp]: "(f(x := y)) z = (if z = x then y else f z)"
   by (simp add: fun_upd_def)
 
 (* fun_upd_apply supersedes these two, but they are useful
    if fun_upd_apply is intentionally removed from the simpset *)
 lemma fun_upd_same: "(f(x := y)) x = y"
   by simp
 
 lemma fun_upd_other: "z \<noteq> x \<Longrightarrow> (f(x := y)) z = f z"
   by simp
 
 lemma fun_upd_upd [simp]: "f(x := y, x := z) = f(x := z)"
   by (simp add: fun_eq_iff)
 
 lemma fun_upd_twist: "a \<noteq> c \<Longrightarrow> (m(a := b))(c := d) = (m(c := d))(a := b)"
-  by (rule ext) auto
+  by auto
 
 lemma inj_on_fun_updI: "inj_on f A \<Longrightarrow> y \<notin> f ` A \<Longrightarrow> inj_on (f(x := y)) A"
   by (auto simp: inj_on_def)
 
 lemma fun_upd_image: "f(x := y) ` A = (if x \<in> A then insert y (f ` (A - {x})) else f ` A)"
   by auto
 
 lemma fun_upd_comp: "f \<circ> (g(x := y)) = (f \<circ> g)(x := f y)"
   by auto
 
 lemma fun_upd_eqD: "f(x := y) = g(x := z) \<Longrightarrow> y = z"
   by (simp add: fun_eq_iff split: if_split_asm)
 
 
 subsection \<open>\<open>override_on\<close>\<close>
 
 definition override_on :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'a \<Rightarrow> 'b"
   where "override_on f g A = (\<lambda>a. if a \<in> A then g a else f a)"
 
 lemma override_on_emptyset[simp]: "override_on f g {} = f"
   by (simp add: override_on_def)
 
 lemma override_on_apply_notin[simp]: "a \<notin> A \<Longrightarrow> (override_on f g A) a = f a"
   by (simp add: override_on_def)
 
 lemma override_on_apply_in[simp]: "a \<in> A \<Longrightarrow> (override_on f g A) a = g a"
   by (simp add: override_on_def)
 
 lemma override_on_insert: "override_on f g (insert x X) = (override_on f g X)(x:=g x)"
   by (simp add: override_on_def fun_eq_iff)
 
 lemma override_on_insert': "override_on f g (insert x X) = (override_on (f(x:=g x)) g X)"
   by (simp add: override_on_def fun_eq_iff)
 
 
 subsection \<open>\<open>swap\<close>\<close>
 
 definition swap :: "'a \<Rightarrow> 'a \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)"
   where "swap a b f = f (a := f b, b:= f a)"
 
 lemma swap_apply [simp]:
   "swap a b f a = f b"
   "swap a b f b = f a"
   "c \<noteq> a \<Longrightarrow> c \<noteq> b \<Longrightarrow> swap a b f c = f c"
   by (simp_all add: swap_def)
 
 lemma swap_self [simp]: "swap a a f = f"
   by (simp add: swap_def)
 
 lemma swap_commute: "swap a b f = swap b a f"
   by (simp add: fun_upd_def swap_def fun_eq_iff)
 
 lemma swap_nilpotent [simp]: "swap a b (swap a b f) = f"
   by (rule ext) (simp add: fun_upd_def swap_def)
 
 lemma swap_comp_involutory [simp]: "swap a b \<circ> swap a b = id"
   by (rule ext) simp
 
 lemma swap_triple:
   assumes "a \<noteq> c" and "b \<noteq> c"
   shows "swap a b (swap b c (swap a b f)) = swap a c f"
   using assms by (simp add: fun_eq_iff swap_def)
 
 lemma comp_swap: "f \<circ> swap a b g = swap a b (f \<circ> g)"
   by (rule ext) (simp add: fun_upd_def swap_def)
 
 lemma swap_image_eq [simp]:
   assumes "a \<in> A" "b \<in> A"
   shows "swap a b f ` A = f ` A"
 proof -
   have subset: "\<And>f. swap a b f ` A \<subseteq> f ` A"
     using assms by (auto simp: image_iff swap_def)
   then have "swap a b (swap a b f) ` A \<subseteq> (swap a b f) ` A" .
   with subset[of f] show ?thesis by auto
 qed
 
 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"
   by (auto simp add: inj_on_def swap_def)
 
 lemma inj_on_swap_iff [simp]:
   assumes A: "a \<in> A" "b \<in> A"
   shows "inj_on (swap a b f) A \<longleftrightarrow> inj_on f A"
 proof
   assume "inj_on (swap a b f) A"
   with A have "inj_on (swap a b (swap a b f)) A"
     by (iprover intro: inj_on_imp_inj_on_swap)
   then show "inj_on f A" by simp
 next
   assume "inj_on f A"
   with A show "inj_on (swap a b f) A"
     by (iprover intro: inj_on_imp_inj_on_swap)
 qed
 
 lemma surj_imp_surj_swap: "surj f \<Longrightarrow> surj (swap a b f)"
   by simp
 
 lemma surj_swap_iff [simp]: "surj (swap a b f) \<longleftrightarrow> surj f"
   by simp
 
 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"
   by (auto simp: bij_betw_def)
 
 lemma bij_swap_iff [simp]: "bij (swap a b f) \<longleftrightarrow> bij f"
   by simp
 
 hide_const (open) swap
 
 
 subsection \<open>Inversion of injective functions\<close>
 
 definition the_inv_into :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a)"
   where "the_inv_into A f = (\<lambda>x. THE y. y \<in> A \<and> f y = x)"
 
 lemma the_inv_into_f_f: "inj_on f A \<Longrightarrow> x \<in> A \<Longrightarrow> the_inv_into A f (f x) = x"
   unfolding the_inv_into_def inj_on_def by blast
 
 lemma f_the_inv_into_f: "inj_on f A \<Longrightarrow> y \<in> f ` A  \<Longrightarrow> f (the_inv_into A f y) = y"
   apply (simp add: the_inv_into_def)
   apply (rule the1I2)
    apply (blast dest: inj_onD)
   apply blast
   done
 
 lemma the_inv_into_into: "inj_on f A \<Longrightarrow> x \<in> f ` A \<Longrightarrow> A \<subseteq> B \<Longrightarrow> the_inv_into A f x \<in> B"
   apply (simp add: the_inv_into_def)
   apply (rule the1I2)
    apply (blast dest: inj_onD)
   apply blast
   done
 
 lemma the_inv_into_onto [simp]: "inj_on f A \<Longrightarrow> the_inv_into A f ` (f ` A) = A"
   by (fast intro: the_inv_into_into the_inv_into_f_f [symmetric])
 
 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"
   apply (erule subst)
   apply (erule the_inv_into_f_f)
   apply assumption
   done
 
 lemma the_inv_into_comp:
   "inj_on f (g ` A) \<Longrightarrow> inj_on g A \<Longrightarrow> x \<in> f ` g ` A \<Longrightarrow>
     the_inv_into A (f \<circ> g) x = (the_inv_into A g \<circ> the_inv_into (g ` A) f) x"
   apply (rule the_inv_into_f_eq)
     apply (fast intro: comp_inj_on)
    apply (simp add: f_the_inv_into_f the_inv_into_into)
   apply (simp add: the_inv_into_into)
   done
 
 lemma inj_on_the_inv_into: "inj_on f A \<Longrightarrow> inj_on (the_inv_into A f) (f ` A)"
   by (auto intro: inj_onI simp: the_inv_into_f_f)
 
 lemma bij_betw_the_inv_into: "bij_betw f A B \<Longrightarrow> bij_betw (the_inv_into A f) B A"
   by (auto simp add: bij_betw_def inj_on_the_inv_into the_inv_into_into)
 
 abbreviation the_inv :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a)"
   where "the_inv f \<equiv> the_inv_into UNIV f"
 
 lemma the_inv_f_f: "the_inv f (f x) = x" if "inj f"
   using that UNIV_I by (rule the_inv_into_f_f)
 
 
 subsection \<open>Cantor's Paradox\<close>
 
 theorem Cantors_paradox: "\<nexists>f. f ` A = Pow A"
 proof
   assume "\<exists>f. f ` A = Pow A"
   then obtain f where f: "f ` A = Pow A" ..
   let ?X = "{a \<in> A. a \<notin> f a}"
   have "?X \<in> Pow A" by blast
   then have "?X \<in> f ` A" by (simp only: f)
   then obtain x where "x \<in> A" and "f x = ?X" by blast
   then show False by blast
 qed
 
 subsection \<open>Monotonic functions over a set\<close>
 
 definition "mono_on f A \<equiv> \<forall>r s. r \<in> A \<and> s \<in> A \<and> r \<le> s \<longrightarrow> f r \<le> f s"
 
 lemma mono_onI:
   "(\<And>r s. r \<in> A \<Longrightarrow> s \<in> A \<Longrightarrow> r \<le> s \<Longrightarrow> f r \<le> f s) \<Longrightarrow> mono_on f A"
   unfolding mono_on_def by simp
 
 lemma mono_onD:
   "\<lbrakk>mono_on f A; r \<in> A; s \<in> A; r \<le> s\<rbrakk> \<Longrightarrow> f r \<le> f s"
   unfolding mono_on_def by simp
 
 lemma mono_imp_mono_on: "mono f \<Longrightarrow> mono_on f A"
   unfolding mono_def mono_on_def by auto
 
 lemma mono_on_subset: "mono_on f A \<Longrightarrow> B \<subseteq> A \<Longrightarrow> mono_on f B"
   unfolding mono_on_def by auto
 
 definition "strict_mono_on f A \<equiv> \<forall>r s. r \<in> A \<and> s \<in> A \<and> r < s \<longrightarrow> f r < f s"
 
 lemma strict_mono_onI:
   "(\<And>r s. r \<in> A \<Longrightarrow> s \<in> A \<Longrightarrow> r < s \<Longrightarrow> f r < f s) \<Longrightarrow> strict_mono_on f A"
   unfolding strict_mono_on_def by simp
 
 lemma strict_mono_onD:
   "\<lbrakk>strict_mono_on f A; r \<in> A; s \<in> A; r < s\<rbrakk> \<Longrightarrow> f r < f s"
   unfolding strict_mono_on_def by simp
 
 lemma mono_on_greaterD:
   assumes "mono_on g A" "x \<in> A" "y \<in> A" "g x > (g (y::_::linorder) :: _ :: linorder)"
   shows "x > y"
 proof (rule ccontr)
   assume "\<not>x > y"
   hence "x \<le> y" by (simp add: not_less)
   from assms(1-3) and this have "g x \<le> g y" by (rule mono_onD)
   with assms(4) show False by simp
 qed
 
 lemma strict_mono_inv:
   fixes f :: "('a::linorder) \<Rightarrow> ('b::linorder)"
   assumes "strict_mono f" and "surj f" and inv: "\<And>x. g (f x) = x"
   shows "strict_mono g"
 proof
   fix x y :: 'b assume "x < y"
   from \<open>surj f\<close> obtain x' y' where [simp]: "x = f x'" "y = f y'" by blast
   with \<open>x < y\<close> and \<open>strict_mono f\<close> have "x' < y'" by (simp add: strict_mono_less)
   with inv show "g x < g y" by simp
 qed
 
 lemma strict_mono_on_imp_inj_on:
   assumes "strict_mono_on (f :: (_ :: linorder) \<Rightarrow> (_ :: preorder)) A"
   shows "inj_on f A"
 proof (rule inj_onI)
   fix x y assume "x \<in> A" "y \<in> A" "f x = f y"
   thus "x = y"
     by (cases x y rule: linorder_cases)
        (auto dest: strict_mono_onD[OF assms, of x y] strict_mono_onD[OF assms, of y x])
 qed
 
 lemma strict_mono_on_leD:
   assumes "strict_mono_on (f :: (_ :: linorder) \<Rightarrow> _ :: preorder) A" "x \<in> A" "y \<in> A" "x \<le> y"
   shows "f x \<le> f y"
 proof (insert le_less_linear[of y x], elim disjE)
   assume "x < y"
   with assms have "f x < f y" by (rule_tac strict_mono_onD[OF assms(1)]) simp_all
   thus ?thesis by (rule less_imp_le)
 qed (insert assms, simp)
 
 lemma strict_mono_on_eqD:
   fixes f :: "(_ :: linorder) \<Rightarrow> (_ :: preorder)"
   assumes "strict_mono_on f A" "f x = f y" "x \<in> A" "y \<in> A"
   shows "y = x"
   using assms by (rule_tac linorder_cases[of x y]) (auto dest: strict_mono_onD)
 
 lemma strict_mono_on_imp_mono_on:
   "strict_mono_on (f :: (_ :: linorder) \<Rightarrow> _ :: preorder) A \<Longrightarrow> mono_on f A"
   by (rule mono_onI, rule strict_mono_on_leD)
 
 
 subsection \<open>Setup\<close>
 
 subsubsection \<open>Proof tools\<close>
 
 text \<open>Simplify terms of the form \<open>f(\<dots>,x:=y,\<dots>,x:=z,\<dots>)\<close> to \<open>f(\<dots>,x:=z,\<dots>)\<close>\<close>
 
 simproc_setup fun_upd2 ("f(v := w, x := y)") = \<open>fn _ =>
   let
     fun gen_fun_upd NONE T _ _ = NONE
       | gen_fun_upd (SOME f) T x y = SOME (Const (\<^const_name>\<open>fun_upd\<close>, T) $ f $ x $ y)
     fun dest_fun_T1 (Type (_, T :: Ts)) = T
     fun find_double (t as Const (\<^const_name>\<open>fun_upd\<close>,T) $ f $ x $ y) =
       let
         fun find (Const (\<^const_name>\<open>fun_upd\<close>,T) $ g $ v $ w) =
               if v aconv x then SOME g else gen_fun_upd (find g) T v w
           | find t = NONE
       in (dest_fun_T1 T, gen_fun_upd (find f) T x y) end
 
     val ss = simpset_of \<^context>
 
     fun proc ctxt ct =
       let
         val t = Thm.term_of ct
       in
         (case find_double t of
           (T, NONE) => NONE
         | (T, SOME rhs) =>
             SOME (Goal.prove ctxt [] [] (Logic.mk_equals (t, rhs))
               (fn _ =>
                 resolve_tac ctxt [eq_reflection] 1 THEN
                 resolve_tac ctxt @{thms ext} 1 THEN
                 simp_tac (put_simpset ss ctxt) 1)))
       end
   in proc end
 \<close>
 
 
 subsubsection \<open>Functorial structure of types\<close>
 
 ML_file \<open>Tools/functor.ML\<close>
 
 functor map_fun: map_fun
   by (simp_all add: fun_eq_iff)
 
 functor vimage
   by (simp_all add: fun_eq_iff vimage_comp)
 
 
 text \<open>Legacy theorem names\<close>
 
 lemmas o_def = comp_def
 lemmas o_apply = comp_apply
 lemmas o_assoc = comp_assoc [symmetric]
 lemmas id_o = id_comp
 lemmas o_id = comp_id
 lemmas o_eq_dest = comp_eq_dest
 lemmas o_eq_elim = comp_eq_elim
 lemmas o_eq_dest_lhs = comp_eq_dest_lhs
 lemmas o_eq_id_dest = comp_eq_id_dest
 
 end
diff --git a/src/HOL/Int.thy b/src/HOL/Int.thy
--- a/src/HOL/Int.thy
+++ b/src/HOL/Int.thy
@@ -1,1908 +1,1904 @@
 (*  Title:      HOL/Int.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Author:     Tobias Nipkow, Florian Haftmann, TU Muenchen
 *)
 
 section \<open>The Integers as Equivalence Classes over Pairs of Natural Numbers\<close>
 
 theory Int
   imports Equiv_Relations Power Quotient Fun_Def
 begin
 
 subsection \<open>Definition of integers as a quotient type\<close>
 
 definition intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool"
   where "intrel = (\<lambda>(x, y) (u, v). x + v = u + y)"
 
 lemma intrel_iff [simp]: "intrel (x, y) (u, v) \<longleftrightarrow> x + v = u + y"
   by (simp add: intrel_def)
 
 quotient_type int = "nat \<times> nat" / "intrel"
   morphisms Rep_Integ Abs_Integ
 proof (rule equivpI)
   show "reflp intrel" by (auto simp: reflp_def)
   show "symp intrel" by (auto simp: symp_def)
   show "transp intrel" by (auto simp: transp_def)
 qed
 
 lemma eq_Abs_Integ [case_names Abs_Integ, cases type: int]:
   "(\<And>x y. z = Abs_Integ (x, y) \<Longrightarrow> P) \<Longrightarrow> P"
   by (induct z) auto
 
 
 subsection \<open>Integers form a commutative ring\<close>
 
 instantiation int :: comm_ring_1
 begin
 
 lift_definition zero_int :: "int" is "(0, 0)" .
 
 lift_definition one_int :: "int" is "(1, 0)" .
 
 lift_definition plus_int :: "int \<Rightarrow> int \<Rightarrow> int"
   is "\<lambda>(x, y) (u, v). (x + u, y + v)"
   by clarsimp
 
 lift_definition uminus_int :: "int \<Rightarrow> int"
   is "\<lambda>(x, y). (y, x)"
   by clarsimp
 
 lift_definition minus_int :: "int \<Rightarrow> int \<Rightarrow> int"
   is "\<lambda>(x, y) (u, v). (x + v, y + u)"
   by clarsimp
 
 lift_definition times_int :: "int \<Rightarrow> int \<Rightarrow> int"
   is "\<lambda>(x, y) (u, v). (x*u + y*v, x*v + y*u)"
 proof (clarsimp)
   fix s t u v w x y z :: nat
   assume "s + v = u + t" and "w + z = y + x"
   then have "(s + v) * w + (u + t) * x + u * (w + z) + v * (y + x) =
     (u + t) * w + (s + v) * x + u * (y + x) + v * (w + z)"
     by simp
   then show "(s * w + t * x) + (u * z + v * y) = (u * y + v * z) + (s * x + t * w)"
     by (simp add: algebra_simps)
 qed
 
 instance
   by standard (transfer; clarsimp simp: algebra_simps)+
 
 end
 
 abbreviation int :: "nat \<Rightarrow> int"
   where "int \<equiv> of_nat"
 
 lemma int_def: "int n = Abs_Integ (n, 0)"
   by (induct n) (simp add: zero_int.abs_eq, simp add: one_int.abs_eq plus_int.abs_eq)
 
 lemma int_transfer [transfer_rule]:
   includes lifting_syntax
   shows "rel_fun (=) pcr_int (\<lambda>n. (n, 0)) int"
   by (simp add: rel_fun_def int.pcr_cr_eq cr_int_def int_def)
 
 lemma int_diff_cases: obtains (diff) m n where "z = int m - int n"
   by transfer clarsimp
 
 
 subsection \<open>Integers are totally ordered\<close>
 
 instantiation int :: linorder
 begin
 
 lift_definition less_eq_int :: "int \<Rightarrow> int \<Rightarrow> bool"
   is "\<lambda>(x, y) (u, v). x + v \<le> u + y"
   by auto
 
 lift_definition less_int :: "int \<Rightarrow> int \<Rightarrow> bool"
   is "\<lambda>(x, y) (u, v). x + v < u + y"
   by auto
 
 instance
   by standard (transfer, force)+
 
 end
 
 instantiation int :: distrib_lattice
 begin
 
 definition "(inf :: int \<Rightarrow> int \<Rightarrow> int) = min"
 
 definition "(sup :: int \<Rightarrow> int \<Rightarrow> int) = max"
 
 instance
   by standard (auto simp add: inf_int_def sup_int_def max_min_distrib2)
 
 end
 
 subsection \<open>Ordering properties of arithmetic operations\<close>
 
 instance int :: ordered_cancel_ab_semigroup_add
 proof
   fix i j k :: int
   show "i \<le> j \<Longrightarrow> k + i \<le> k + j"
     by transfer clarsimp
 qed
 
 text \<open>Strict Monotonicity of Multiplication.\<close>
 
 text \<open>Strict, in 1st argument; proof is by induction on \<open>k > 0\<close>.\<close>
 lemma zmult_zless_mono2_lemma: "i < j \<Longrightarrow> 0 < k \<Longrightarrow> int k * i < int k * j"
   for i j :: int
 proof (induct k)
   case 0
   then show ?case by simp
 next
   case (Suc k)
   then show ?case
     by (cases "k = 0") (simp_all add: distrib_right add_strict_mono)
 qed
 
-lemma zero_le_imp_eq_int: "0 \<le> k \<Longrightarrow> \<exists>n. k = int n"
-  for k :: int
-  apply transfer
-  apply clarsimp
-  apply (rule_tac x="a - b" in exI)
-  apply simp
-  done
+lemma zero_le_imp_eq_int:
+  assumes "k \<ge> (0::int)" shows "\<exists>n. k = int n"
+proof -
+  have "b \<le> a \<Longrightarrow> \<exists>n::nat. a = n + b" for a b
+    by (rule_tac x="a - b" in exI) simp
+  with assms show ?thesis
+    by transfer auto
+qed
 
-lemma zero_less_imp_eq_int: "0 < k \<Longrightarrow> \<exists>n>0. k = int n"
-  for k :: int
-  apply transfer
-  apply clarsimp
-  apply (rule_tac x="a - b" in exI)
-  apply simp
-  done
+lemma zero_less_imp_eq_int:
+  assumes "k > (0::int)" shows "\<exists>n>0. k = int n"
+proof -
+  have "b < a \<Longrightarrow> \<exists>n::nat. n>0 \<and> a = n + b" for a b
+    by (rule_tac x="a - b" in exI) simp
+  with assms show ?thesis
+    by transfer auto
+qed
 
 lemma zmult_zless_mono2: "i < j \<Longrightarrow> 0 < k \<Longrightarrow> k * i < k * j"
   for i j k :: int
   by (drule zero_less_imp_eq_int) (auto simp add: zmult_zless_mono2_lemma)
 
 
 text \<open>The integers form an ordered integral domain.\<close>
 
 instantiation int :: linordered_idom
 begin
 
 definition zabs_def: "\<bar>i::int\<bar> = (if i < 0 then - i else i)"
 
 definition zsgn_def: "sgn (i::int) = (if i = 0 then 0 else if 0 < i then 1 else - 1)"
 
 instance
 proof
   fix i j k :: int
   show "i < j \<Longrightarrow> 0 < k \<Longrightarrow> k * i < k * j"
     by (rule zmult_zless_mono2)
   show "\<bar>i\<bar> = (if i < 0 then -i else i)"
     by (simp only: zabs_def)
   show "sgn (i::int) = (if i=0 then 0 else if 0<i then 1 else - 1)"
     by (simp only: zsgn_def)
 qed
 
 end
 
 lemma zless_imp_add1_zle: "w < z \<Longrightarrow> w + 1 \<le> z"
   for w z :: int
   by transfer clarsimp
 
 lemma zless_iff_Suc_zadd: "w < z \<longleftrightarrow> (\<exists>n. z = w + int (Suc n))"
   for w z :: int
-  apply transfer
-  apply auto
-  apply (rename_tac a b c d)
-  apply (rule_tac x="c+b - Suc(a+d)" in exI)
-  apply arith
-  done
+proof -
+  have "\<And>a b c d. a + d < c + b \<Longrightarrow> \<exists>n. c + b = Suc (a + n + d)"
+    by (rule_tac x="c+b - Suc(a+d)" in exI) arith
+  then show ?thesis
+    by transfer auto
+qed
 
 lemma zabs_less_one_iff [simp]: "\<bar>z\<bar> < 1 \<longleftrightarrow> z = 0" (is "?lhs \<longleftrightarrow> ?rhs")
   for z :: int
 proof
   assume ?rhs
   then show ?lhs by simp
 next
   assume ?lhs
   with zless_imp_add1_zle [of "\<bar>z\<bar>" 1] have "\<bar>z\<bar> + 1 \<le> 1" by simp
   then have "\<bar>z\<bar> \<le> 0" by simp
   then show ?rhs by simp
 qed
 
 
 subsection \<open>Embedding of the Integers into any \<open>ring_1\<close>: \<open>of_int\<close>\<close>
 
 context ring_1
 begin
 
 lift_definition of_int :: "int \<Rightarrow> 'a"
   is "\<lambda>(i, j). of_nat i - of_nat j"
   by (clarsimp simp add: diff_eq_eq eq_diff_eq diff_add_eq
       of_nat_add [symmetric] simp del: of_nat_add)
 
 lemma of_int_0 [simp]: "of_int 0 = 0"
   by transfer simp
 
 lemma of_int_1 [simp]: "of_int 1 = 1"
   by transfer simp
 
 lemma of_int_add [simp]: "of_int (w + z) = of_int w + of_int z"
   by transfer (clarsimp simp add: algebra_simps)
 
 lemma of_int_minus [simp]: "of_int (- z) = - (of_int z)"
   by (transfer fixing: uminus) clarsimp
 
 lemma of_int_diff [simp]: "of_int (w - z) = of_int w - of_int z"
   using of_int_add [of w "- z"] by simp
 
 lemma of_int_mult [simp]: "of_int (w*z) = of_int w * of_int z"
   by (transfer fixing: times) (clarsimp simp add: algebra_simps)
 
 lemma mult_of_int_commute: "of_int x * y = y * of_int x"
   by (transfer fixing: times) (auto simp: algebra_simps mult_of_nat_commute)
 
 text \<open>Collapse nested embeddings.\<close>
 lemma of_int_of_nat_eq [simp]: "of_int (int n) = of_nat n"
   by (induct n) auto
 
 lemma of_int_numeral [simp, code_post]: "of_int (numeral k) = numeral k"
   by (simp add: of_nat_numeral [symmetric] of_int_of_nat_eq [symmetric])
 
 lemma of_int_neg_numeral [code_post]: "of_int (- numeral k) = - numeral k"
   by simp
 
 lemma of_int_power [simp]: "of_int (z ^ n) = of_int z ^ n"
   by (induct n) simp_all
 
 lemma of_int_of_bool [simp]:
   "of_int (of_bool P) = of_bool P"
   by auto
 
 end
 
 context ring_char_0
 begin
 
 lemma of_int_eq_iff [simp]: "of_int w = of_int z \<longleftrightarrow> w = z"
   by transfer (clarsimp simp add: algebra_simps of_nat_add [symmetric] simp del: of_nat_add)
 
 text \<open>Special cases where either operand is zero.\<close>
 lemma of_int_eq_0_iff [simp]: "of_int z = 0 \<longleftrightarrow> z = 0"
   using of_int_eq_iff [of z 0] by simp
 
 lemma of_int_0_eq_iff [simp]: "0 = of_int z \<longleftrightarrow> z = 0"
   using of_int_eq_iff [of 0 z] by simp
 
 lemma of_int_eq_1_iff [iff]: "of_int z = 1 \<longleftrightarrow> z = 1"
   using of_int_eq_iff [of z 1] by simp
 
 lemma numeral_power_eq_of_int_cancel_iff [simp]:
   "numeral x ^ n = of_int y \<longleftrightarrow> numeral x ^ n = y"
   using of_int_eq_iff[of "numeral x ^ n" y, unfolded of_int_numeral of_int_power] .
 
 lemma of_int_eq_numeral_power_cancel_iff [simp]:
   "of_int y = numeral x ^ n \<longleftrightarrow> y = numeral x ^ n"
   using numeral_power_eq_of_int_cancel_iff [of x n y] by (metis (mono_tags))
 
 lemma neg_numeral_power_eq_of_int_cancel_iff [simp]:
   "(- numeral x) ^ n = of_int y \<longleftrightarrow> (- numeral x) ^ n = y"
   using of_int_eq_iff[of "(- numeral x) ^ n" y]
   by simp
 
 lemma of_int_eq_neg_numeral_power_cancel_iff [simp]:
   "of_int y = (- numeral x) ^ n \<longleftrightarrow> y = (- numeral x) ^ n"
   using neg_numeral_power_eq_of_int_cancel_iff[of x n y] by (metis (mono_tags))
 
 lemma of_int_eq_of_int_power_cancel_iff[simp]: "(of_int b) ^ w = of_int x \<longleftrightarrow> b ^ w = x"
   by (metis of_int_power of_int_eq_iff)
 
 lemma of_int_power_eq_of_int_cancel_iff[simp]: "of_int x = (of_int b) ^ w \<longleftrightarrow> x = b ^ w"
   by (metis of_int_eq_of_int_power_cancel_iff)
 
 end
 
 context linordered_idom
 begin
 
 text \<open>Every \<open>linordered_idom\<close> has characteristic zero.\<close>
 subclass ring_char_0 ..
 
 lemma of_int_le_iff [simp]: "of_int w \<le> of_int z \<longleftrightarrow> w \<le> z"
   by (transfer fixing: less_eq)
     (clarsimp simp add: algebra_simps of_nat_add [symmetric] simp del: of_nat_add)
 
 lemma of_int_less_iff [simp]: "of_int w < of_int z \<longleftrightarrow> w < z"
   by (simp add: less_le order_less_le)
 
 lemma of_int_0_le_iff [simp]: "0 \<le> of_int z \<longleftrightarrow> 0 \<le> z"
   using of_int_le_iff [of 0 z] by simp
 
 lemma of_int_le_0_iff [simp]: "of_int z \<le> 0 \<longleftrightarrow> z \<le> 0"
   using of_int_le_iff [of z 0] by simp
 
 lemma of_int_0_less_iff [simp]: "0 < of_int z \<longleftrightarrow> 0 < z"
   using of_int_less_iff [of 0 z] by simp
 
 lemma of_int_less_0_iff [simp]: "of_int z < 0 \<longleftrightarrow> z < 0"
   using of_int_less_iff [of z 0] by simp
 
 lemma of_int_1_le_iff [simp]: "1 \<le> of_int z \<longleftrightarrow> 1 \<le> z"
   using of_int_le_iff [of 1 z] by simp
 
 lemma of_int_le_1_iff [simp]: "of_int z \<le> 1 \<longleftrightarrow> z \<le> 1"
   using of_int_le_iff [of z 1] by simp
 
 lemma of_int_1_less_iff [simp]: "1 < of_int z \<longleftrightarrow> 1 < z"
   using of_int_less_iff [of 1 z] by simp
 
 lemma of_int_less_1_iff [simp]: "of_int z < 1 \<longleftrightarrow> z < 1"
   using of_int_less_iff [of z 1] by simp
 
 lemma of_int_pos: "z > 0 \<Longrightarrow> of_int z > 0"
   by simp
 
 lemma of_int_nonneg: "z \<ge> 0 \<Longrightarrow> of_int z \<ge> 0"
   by simp
 
 lemma of_int_abs [simp]: "of_int \<bar>x\<bar> = \<bar>of_int x\<bar>"
   by (auto simp add: abs_if)
 
 lemma of_int_lessD:
   assumes "\<bar>of_int n\<bar> < x"
   shows "n = 0 \<or> x > 1"
 proof (cases "n = 0")
   case True
   then show ?thesis by simp
 next
   case False
   then have "\<bar>n\<bar> \<noteq> 0" by simp
   then have "\<bar>n\<bar> > 0" by simp
   then have "\<bar>n\<bar> \<ge> 1"
     using zless_imp_add1_zle [of 0 "\<bar>n\<bar>"] by simp
   then have "\<bar>of_int n\<bar> \<ge> 1"
     unfolding of_int_1_le_iff [of "\<bar>n\<bar>", symmetric] by simp
   then have "1 < x" using assms by (rule le_less_trans)
   then show ?thesis ..
 qed
 
 lemma of_int_leD:
   assumes "\<bar>of_int n\<bar> \<le> x"
   shows "n = 0 \<or> 1 \<le> x"
 proof (cases "n = 0")
   case True
   then show ?thesis by simp
 next
   case False
   then have "\<bar>n\<bar> \<noteq> 0" by simp
   then have "\<bar>n\<bar> > 0" by simp
   then have "\<bar>n\<bar> \<ge> 1"
     using zless_imp_add1_zle [of 0 "\<bar>n\<bar>"] by simp
   then have "\<bar>of_int n\<bar> \<ge> 1"
     unfolding of_int_1_le_iff [of "\<bar>n\<bar>", symmetric] by simp
   then have "1 \<le> x" using assms by (rule order_trans)
   then show ?thesis ..
 qed
 
 lemma numeral_power_le_of_int_cancel_iff [simp]:
   "numeral x ^ n \<le> of_int a \<longleftrightarrow> numeral x ^ n \<le> a"
   by (metis (mono_tags) local.of_int_eq_numeral_power_cancel_iff of_int_le_iff)
 
 lemma of_int_le_numeral_power_cancel_iff [simp]:
   "of_int a \<le> numeral x ^ n \<longleftrightarrow> a \<le> numeral x ^ n"
   by (metis (mono_tags) local.numeral_power_eq_of_int_cancel_iff of_int_le_iff)
 
 lemma numeral_power_less_of_int_cancel_iff [simp]:
   "numeral x ^ n < of_int a \<longleftrightarrow> numeral x ^ n < a"
   by (metis (mono_tags) local.of_int_eq_numeral_power_cancel_iff of_int_less_iff)
 
 lemma of_int_less_numeral_power_cancel_iff [simp]:
   "of_int a < numeral x ^ n \<longleftrightarrow> a < numeral x ^ n"
   by (metis (mono_tags) local.of_int_eq_numeral_power_cancel_iff of_int_less_iff)
 
 lemma neg_numeral_power_le_of_int_cancel_iff [simp]:
   "(- numeral x) ^ n \<le> of_int a \<longleftrightarrow> (- numeral x) ^ n \<le> a"
   by (metis (mono_tags) of_int_le_iff of_int_neg_numeral of_int_power)
 
 lemma of_int_le_neg_numeral_power_cancel_iff [simp]:
   "of_int a \<le> (- numeral x) ^ n \<longleftrightarrow> a \<le> (- numeral x) ^ n"
   by (metis (mono_tags) of_int_le_iff of_int_neg_numeral of_int_power)
 
 lemma neg_numeral_power_less_of_int_cancel_iff [simp]:
   "(- numeral x) ^ n < of_int a \<longleftrightarrow> (- numeral x) ^ n < a"
   using of_int_less_iff[of "(- numeral x) ^ n" a]
   by simp
 
 lemma of_int_less_neg_numeral_power_cancel_iff [simp]:
   "of_int a < (- numeral x) ^ n \<longleftrightarrow> a < (- numeral x::int) ^ n"
   using of_int_less_iff[of a "(- numeral x) ^ n"]
   by simp
 
 lemma of_int_le_of_int_power_cancel_iff[simp]: "(of_int b) ^ w \<le> of_int x \<longleftrightarrow> b ^ w \<le> x"
   by (metis (mono_tags) of_int_le_iff of_int_power)
 
 lemma of_int_power_le_of_int_cancel_iff[simp]: "of_int x \<le> (of_int b) ^ w\<longleftrightarrow> x \<le> b ^ w"
   by (metis (mono_tags) of_int_le_iff of_int_power)
 
 lemma of_int_less_of_int_power_cancel_iff[simp]: "(of_int b) ^ w < of_int x \<longleftrightarrow> b ^ w < x"
   by (metis (mono_tags) of_int_less_iff of_int_power)
 
 lemma of_int_power_less_of_int_cancel_iff[simp]: "of_int x < (of_int b) ^ w\<longleftrightarrow> x < b ^ w"
   by (metis (mono_tags) of_int_less_iff of_int_power)
 
 lemma of_int_max: "of_int (max x y) = max (of_int x) (of_int y)"
   by (auto simp: max_def)
 
 lemma of_int_min: "of_int (min x y) = min (of_int x) (of_int y)"
   by (auto simp: min_def)
 
 end
 
 context division_ring
 begin
 
 lemmas mult_inverse_of_int_commute =
   mult_commute_imp_mult_inverse_commute[OF mult_of_int_commute]
 
 end
 
 text \<open>Comparisons involving \<^term>\<open>of_int\<close>.\<close>
 
 lemma of_int_eq_numeral_iff [iff]: "of_int z = (numeral n :: 'a::ring_char_0) \<longleftrightarrow> z = numeral n"
   using of_int_eq_iff by fastforce
 
 lemma of_int_le_numeral_iff [simp]:
   "of_int z \<le> (numeral n :: 'a::linordered_idom) \<longleftrightarrow> z \<le> numeral n"
   using of_int_le_iff [of z "numeral n"] by simp
 
 lemma of_int_numeral_le_iff [simp]:
   "(numeral n :: 'a::linordered_idom) \<le> of_int z \<longleftrightarrow> numeral n \<le> z"
   using of_int_le_iff [of "numeral n"] by simp
 
 lemma of_int_less_numeral_iff [simp]:
   "of_int z < (numeral n :: 'a::linordered_idom) \<longleftrightarrow> z < numeral n"
   using of_int_less_iff [of z "numeral n"] by simp
 
 lemma of_int_numeral_less_iff [simp]:
   "(numeral n :: 'a::linordered_idom) < of_int z \<longleftrightarrow> numeral n < z"
   using of_int_less_iff [of "numeral n" z] by simp
 
 lemma of_nat_less_of_int_iff: "(of_nat n::'a::linordered_idom) < of_int x \<longleftrightarrow> int n < x"
   by (metis of_int_of_nat_eq of_int_less_iff)
 
 lemma of_int_eq_id [simp]: "of_int = id"
 proof
   show "of_int z = id z" for z
     by (cases z rule: int_diff_cases) simp
 qed
 
 instance int :: no_top
-  apply standard
-  apply (rule_tac x="x + 1" in exI)
-  apply simp
-  done
+proof
+  show "\<And>x::int. \<exists>y. x < y"
+    by (rule_tac x="x + 1" in exI) simp
+qed
 
 instance int :: no_bot
-  apply standard
-  apply (rule_tac x="x - 1" in exI)
-  apply simp
-  done
+proof
+  show "\<And>x::int. \<exists>y. y < x"
+    by (rule_tac x="x - 1" in exI) simp
+qed
 
 
 subsection \<open>Magnitude of an Integer, as a Natural Number: \<open>nat\<close>\<close>
 
 lift_definition nat :: "int \<Rightarrow> nat" is "\<lambda>(x, y). x - y"
   by auto
 
 lemma nat_int [simp]: "nat (int n) = n"
   by transfer simp
 
 lemma int_nat_eq [simp]: "int (nat z) = (if 0 \<le> z then z else 0)"
   by transfer clarsimp
 
 lemma nat_0_le: "0 \<le> z \<Longrightarrow> int (nat z) = z"
   by simp
 
 lemma nat_le_0 [simp]: "z \<le> 0 \<Longrightarrow> nat z = 0"
   by transfer clarsimp
 
 lemma nat_le_eq_zle: "0 < w \<or> 0 \<le> z \<Longrightarrow> nat w \<le> nat z \<longleftrightarrow> w \<le> z"
   by transfer (clarsimp, arith)
 
 text \<open>An alternative condition is \<^term>\<open>0 \<le> w\<close>.\<close>
 lemma nat_mono_iff: "0 < z \<Longrightarrow> nat w < nat z \<longleftrightarrow> w < z"
   by (simp add: nat_le_eq_zle linorder_not_le [symmetric])
 
 lemma nat_less_eq_zless: "0 \<le> w \<Longrightarrow> nat w < nat z \<longleftrightarrow> w < z"
   by (simp add: nat_le_eq_zle linorder_not_le [symmetric])
 
 lemma zless_nat_conj [simp]: "nat w < nat z \<longleftrightarrow> 0 < z \<and> w < z"
   by transfer (clarsimp, arith)
 
 lemma nonneg_int_cases:
   assumes "0 \<le> k"
   obtains n where "k = int n"
 proof -
   from assms have "k = int (nat k)"
     by simp
   then show thesis
     by (rule that)
 qed
 
 lemma pos_int_cases:
   assumes "0 < k"
   obtains n where "k = int n" and "n > 0"
 proof -
   from assms have "0 \<le> k"
     by simp
   then obtain n where "k = int n"
     by (rule nonneg_int_cases)
   moreover have "n > 0"
     using \<open>k = int n\<close> assms by simp
   ultimately show thesis
     by (rule that)
 qed
 
 lemma nonpos_int_cases:
   assumes "k \<le> 0"
   obtains n where "k = - int n"
 proof -
   from assms have "- k \<ge> 0"
     by simp
   then obtain n where "- k = int n"
     by (rule nonneg_int_cases)
   then have "k = - int n"
     by simp
   then show thesis
     by (rule that)
 qed
 
 lemma neg_int_cases:
   assumes "k < 0"
   obtains n where "k = - int n" and "n > 0"
 proof -
   from assms have "- k > 0"
     by simp
   then obtain n where "- k = int n" and "- k > 0"
     by (blast elim: pos_int_cases)
   then have "k = - int n" and "n > 0"
     by simp_all
   then show thesis
     by (rule that)
 qed
 
 lemma nat_eq_iff: "nat w = m \<longleftrightarrow> (if 0 \<le> w then w = int m else m = 0)"
   by transfer (clarsimp simp add: le_imp_diff_is_add)
 
 lemma nat_eq_iff2: "m = nat w \<longleftrightarrow> (if 0 \<le> w then w = int m else m = 0)"
   using nat_eq_iff [of w m] by auto
 
 lemma nat_0 [simp]: "nat 0 = 0"
   by (simp add: nat_eq_iff)
 
 lemma nat_1 [simp]: "nat 1 = Suc 0"
   by (simp add: nat_eq_iff)
 
 lemma nat_numeral [simp]: "nat (numeral k) = numeral k"
   by (simp add: nat_eq_iff)
 
 lemma nat_neg_numeral [simp]: "nat (- numeral k) = 0"
   by simp
 
 lemma nat_2: "nat 2 = Suc (Suc 0)"
   by simp
 
 lemma nat_less_iff: "0 \<le> w \<Longrightarrow> nat w < m \<longleftrightarrow> w < of_nat m"
   by transfer (clarsimp, arith)
 
 lemma nat_le_iff: "nat x \<le> n \<longleftrightarrow> x \<le> int n"
   by transfer (clarsimp simp add: le_diff_conv)
 
 lemma nat_mono: "x \<le> y \<Longrightarrow> nat x \<le> nat y"
   by transfer auto
 
 lemma nat_0_iff[simp]: "nat i = 0 \<longleftrightarrow> i \<le> 0"
   for i :: int
   by transfer clarsimp
 
 lemma int_eq_iff: "of_nat m = z \<longleftrightarrow> m = nat z \<and> 0 \<le> z"
   by (auto simp add: nat_eq_iff2)
 
 lemma zero_less_nat_eq [simp]: "0 < nat z \<longleftrightarrow> 0 < z"
   using zless_nat_conj [of 0] by auto
 
 lemma nat_add_distrib: "0 \<le> z \<Longrightarrow> 0 \<le> z' \<Longrightarrow> nat (z + z') = nat z + nat z'"
   by transfer clarsimp
 
 lemma nat_diff_distrib': "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> nat (x - y) = nat x - nat y"
   by transfer clarsimp
 
 lemma nat_diff_distrib: "0 \<le> z' \<Longrightarrow> z' \<le> z \<Longrightarrow> nat (z - z') = nat z - nat z'"
   by (rule nat_diff_distrib') auto
 
 lemma nat_zminus_int [simp]: "nat (- int n) = 0"
   by transfer simp
 
 lemma le_nat_iff: "k \<ge> 0 \<Longrightarrow> n \<le> nat k \<longleftrightarrow> int n \<le> k"
   by transfer auto
 
 lemma zless_nat_eq_int_zless: "m < nat z \<longleftrightarrow> int m < z"
   by transfer (clarsimp simp add: less_diff_conv)
 
 lemma (in ring_1) of_nat_nat [simp]: "0 \<le> z \<Longrightarrow> of_nat (nat z) = of_int z"
   by transfer (clarsimp simp add: of_nat_diff)
 
 lemma diff_nat_numeral [simp]: "(numeral v :: nat) - numeral v' = nat (numeral v - numeral v')"
   by (simp only: nat_diff_distrib' zero_le_numeral nat_numeral)
 
 lemma nat_abs_triangle_ineq:
   "nat \<bar>k + l\<bar> \<le> nat \<bar>k\<bar> + nat \<bar>l\<bar>"
   by (simp add: nat_add_distrib [symmetric] nat_le_eq_zle abs_triangle_ineq)
 
 lemma nat_of_bool [simp]:
   "nat (of_bool P) = of_bool P"
   by auto
 
 lemma split_nat [arith_split]: "P (nat i) \<longleftrightarrow> ((\<forall>n. i = int n \<longrightarrow> P n) \<and> (i < 0 \<longrightarrow> P 0))"
   (is "?P = (?L \<and> ?R)")
   for i :: int
 proof (cases "i < 0")
   case True
   then show ?thesis
     by auto
 next
   case False
   have "?P = ?L"
   proof
     assume ?P
     then show ?L using False by auto
   next
     assume ?L
     moreover from False have "int (nat i) = i"
       by (simp add: not_less)
     ultimately show ?P
       by simp
   qed
   with False show ?thesis by simp
 qed
 
 lemma all_nat: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x\<ge>0. P (nat x))"
   by (auto split: split_nat)
 
 lemma ex_nat: "(\<exists>x. P x) \<longleftrightarrow> (\<exists>x. 0 \<le> x \<and> P (nat x))"
 proof
   assume "\<exists>x. P x"
   then obtain x where "P x" ..
   then have "int x \<ge> 0 \<and> P (nat (int x))" by simp
   then show "\<exists>x\<ge>0. P (nat x)" ..
 next
   assume "\<exists>x\<ge>0. P (nat x)"
   then show "\<exists>x. P x" by auto
 qed
 
 
 text \<open>For termination proofs:\<close>
 lemma measure_function_int[measure_function]: "is_measure (nat \<circ> abs)" ..
 
 
 subsection \<open>Lemmas about the Function \<^term>\<open>of_nat\<close> and Orderings\<close>
 
 lemma negative_zless_0: "- (int (Suc n)) < (0 :: int)"
   by (simp add: order_less_le del: of_nat_Suc)
 
 lemma negative_zless [iff]: "- (int (Suc n)) < int m"
   by (rule negative_zless_0 [THEN order_less_le_trans], simp)
 
 lemma negative_zle_0: "- int n \<le> 0"
   by (simp add: minus_le_iff)
 
 lemma negative_zle [iff]: "- int n \<le> int m"
   by (rule order_trans [OF negative_zle_0 of_nat_0_le_iff])
 
 lemma not_zle_0_negative [simp]: "\<not> 0 \<le> - int (Suc n)"
   by (subst le_minus_iff) (simp del: of_nat_Suc)
 
 lemma int_zle_neg: "int n \<le> - int m \<longleftrightarrow> n = 0 \<and> m = 0"
   by transfer simp
 
 lemma not_int_zless_negative [simp]: "\<not> int n < - int m"
   by (simp add: linorder_not_less)
 
 lemma negative_eq_positive [simp]: "- int n = of_nat m \<longleftrightarrow> n = 0 \<and> m = 0"
   by (force simp add: order_eq_iff [of "- of_nat n"] int_zle_neg)
 
 lemma zle_iff_zadd: "w \<le> z \<longleftrightarrow> (\<exists>n. z = w + int n)"
   (is "?lhs \<longleftrightarrow> ?rhs")
 proof
   assume ?rhs
   then show ?lhs by auto
 next
   assume ?lhs
   then have "0 \<le> z - w" by simp
   then obtain n where "z - w = int n"
     using zero_le_imp_eq_int [of "z - w"] by blast
   then have "z = w + int n" by simp
   then show ?rhs ..
 qed
 
 lemma zadd_int_left: "int m + (int n + z) = int (m + n) + z"
   by simp
 
 text \<open>
   This version is proved for all ordered rings, not just integers!
   It is proved here because attribute \<open>arith_split\<close> is not available
   in theory \<open>Rings\<close>.
   But is it really better than just rewriting with \<open>abs_if\<close>?
 \<close>
 lemma abs_split [arith_split, no_atp]: "P \<bar>a\<bar> \<longleftrightarrow> (0 \<le> a \<longrightarrow> P a) \<and> (a < 0 \<longrightarrow> P (- a))"
   for a :: "'a::linordered_idom"
   by (force dest: order_less_le_trans simp add: abs_if linorder_not_less)
 
-lemma negD: "x < 0 \<Longrightarrow> \<exists>n. x = - (int (Suc n))"
-  apply transfer
-  apply clarsimp
-  apply (rule_tac x="b - Suc a" in exI)
-  apply arith
-  done
+lemma negD:
+  assumes "x < 0" shows "\<exists>n. x = - (int (Suc n))"
+proof -
+  have "\<And>a b. a < b \<Longrightarrow> \<exists>n. Suc (a + n) = b"
+    by (rule_tac x="b - Suc a" in exI) arith
+  with assms show ?thesis
+    by transfer auto
+qed
 
 
 subsection \<open>Cases and induction\<close>
 
 text \<open>
   Now we replace the case analysis rule by a more conventional one:
   whether an integer is negative or not.
 \<close>
 
 text \<open>This version is symmetric in the two subgoals.\<close>
 lemma int_cases2 [case_names nonneg nonpos, cases type: int]:
   "(\<And>n. z = int n \<Longrightarrow> P) \<Longrightarrow> (\<And>n. z = - (int n) \<Longrightarrow> P) \<Longrightarrow> P"
   by (cases "z < 0") (auto simp add: linorder_not_less dest!: negD nat_0_le [THEN sym])
 
 text \<open>This is the default, with a negative case.\<close>
 lemma int_cases [case_names nonneg neg, cases type: int]:
-  "(\<And>n. z = int n \<Longrightarrow> P) \<Longrightarrow> (\<And>n. z = - (int (Suc n)) \<Longrightarrow> P) \<Longrightarrow> P"
-  apply (cases "z < 0")
-   apply (blast dest!: negD)
-  apply (simp add: linorder_not_less del: of_nat_Suc)
-  apply auto
-  apply (blast dest: nat_0_le [THEN sym])
-  done
+  assumes pos: "\<And>n. z = int n \<Longrightarrow> P" and neg: "\<And>n. z = - (int (Suc n)) \<Longrightarrow> P"
+  shows P
+proof (cases "z < 0")
+  case True
+  with neg show ?thesis
+    by (blast dest!: negD)
+next
+  case False
+  with pos show ?thesis
+    by (force simp add: linorder_not_less dest: nat_0_le [THEN sym])
+qed
 
 lemma int_cases3 [case_names zero pos neg]:
   fixes k :: int
   assumes "k = 0 \<Longrightarrow> P" and "\<And>n. k = int n \<Longrightarrow> n > 0 \<Longrightarrow> P"
     and "\<And>n. k = - int n \<Longrightarrow> n > 0 \<Longrightarrow> P"
   shows "P"
 proof (cases k "0::int" rule: linorder_cases)
   case equal
   with assms(1) show P by simp
 next
   case greater
   then have *: "nat k > 0" by simp
   moreover from * have "k = int (nat k)" by auto
   ultimately show P using assms(2) by blast
 next
   case less
   then have *: "nat (- k) > 0" by simp
   moreover from * have "k = - int (nat (- k))" by auto
   ultimately show P using assms(3) by blast
 qed
 
 lemma int_of_nat_induct [case_names nonneg neg, induct type: int]:
   "(\<And>n. P (int n)) \<Longrightarrow> (\<And>n. P (- (int (Suc n)))) \<Longrightarrow> P z"
   by (cases z) auto
 
 lemma sgn_mult_dvd_iff [simp]:
   "sgn r * l dvd k \<longleftrightarrow> l dvd k \<and> (r = 0 \<longrightarrow> k = 0)" for k l r :: int
   by (cases r rule: int_cases3) auto
 
 lemma mult_sgn_dvd_iff [simp]:
   "l * sgn r dvd k \<longleftrightarrow> l dvd k \<and> (r = 0 \<longrightarrow> k = 0)" for k l r :: int
   using sgn_mult_dvd_iff [of r l k] by (simp add: ac_simps)
 
 lemma dvd_sgn_mult_iff [simp]:
   "l dvd sgn r * k \<longleftrightarrow> l dvd k \<or> r = 0" for k l r :: int
   by (cases r rule: int_cases3) simp_all
 
 lemma dvd_mult_sgn_iff [simp]:
   "l dvd k * sgn r \<longleftrightarrow> l dvd k \<or> r = 0" for k l r :: int
   using dvd_sgn_mult_iff [of l r k] by (simp add: ac_simps)
 
 lemma int_sgnE:
   fixes k :: int
   obtains n and l where "k = sgn l * int n"
 proof -
   have "k = sgn k * int (nat \<bar>k\<bar>)"
     by (simp add: sgn_mult_abs)
   then show ?thesis ..
 qed
 
 
 subsubsection \<open>Binary comparisons\<close>
 
 text \<open>Preliminaries\<close>
 
 lemma le_imp_0_less:
   fixes z :: int
   assumes le: "0 \<le> z"
   shows "0 < 1 + z"
 proof -
   have "0 \<le> z" by fact
   also have "\<dots> < z + 1" by (rule less_add_one)
   also have "\<dots> = 1 + z" by (simp add: ac_simps)
   finally show "0 < 1 + z" .
 qed
 
 lemma odd_less_0_iff: "1 + z + z < 0 \<longleftrightarrow> z < 0"
   for z :: int
 proof (cases z)
   case (nonneg n)
   then show ?thesis
     by (simp add: linorder_not_less add.assoc add_increasing le_imp_0_less [THEN order_less_imp_le])
 next
   case (neg n)
   then show ?thesis
     by (simp del: of_nat_Suc of_nat_add of_nat_1
         add: algebra_simps of_nat_1 [where 'a=int, symmetric] of_nat_add [symmetric])
 qed
 
 
 subsubsection \<open>Comparisons, for Ordered Rings\<close>
 
 lemma odd_nonzero: "1 + z + z \<noteq> 0"
   for z :: int
 proof (cases z)
   case (nonneg n)
   have le: "0 \<le> z + z"
     by (simp add: nonneg add_increasing)
   then show ?thesis
     using le_imp_0_less [OF le] by (auto simp: ac_simps)
 next
   case (neg n)
   show ?thesis
   proof
     assume eq: "1 + z + z = 0"
     have "0 < 1 + (int n + int n)"
       by (simp add: le_imp_0_less add_increasing)
     also have "\<dots> = - (1 + z + z)"
       by (simp add: neg add.assoc [symmetric])
     also have "\<dots> = 0" by (simp add: eq)
     finally have "0<0" ..
     then show False by blast
   qed
 qed
 
 
 subsection \<open>The Set of Integers\<close>
 
 context ring_1
 begin
 
 definition Ints :: "'a set"  ("\<int>")
   where "\<int> = range of_int"
 
 lemma Ints_of_int [simp]: "of_int z \<in> \<int>"
   by (simp add: Ints_def)
 
 lemma Ints_of_nat [simp]: "of_nat n \<in> \<int>"
   using Ints_of_int [of "of_nat n"] by simp
 
 lemma Ints_0 [simp]: "0 \<in> \<int>"
   using Ints_of_int [of "0"] by simp
 
 lemma Ints_1 [simp]: "1 \<in> \<int>"
   using Ints_of_int [of "1"] by simp
 
 lemma Ints_numeral [simp]: "numeral n \<in> \<int>"
   by (subst of_nat_numeral [symmetric], rule Ints_of_nat)
 
 lemma Ints_add [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a + b \<in> \<int>"
-  apply (auto simp add: Ints_def)
-  apply (rule range_eqI)
-  apply (rule of_int_add [symmetric])
-  done
+  by (force simp add: Ints_def simp flip: of_int_add intro: range_eqI)
 
 lemma Ints_minus [simp]: "a \<in> \<int> \<Longrightarrow> -a \<in> \<int>"
-  apply (auto simp add: Ints_def)
-  apply (rule range_eqI)
-  apply (rule of_int_minus [symmetric])
-  done
+  by (force simp add: Ints_def simp flip: of_int_minus intro: range_eqI)
 
 lemma minus_in_Ints_iff: "-x \<in> \<int> \<longleftrightarrow> x \<in> \<int>"
   using Ints_minus[of x] Ints_minus[of "-x"] by auto
 
 lemma Ints_diff [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a - b \<in> \<int>"
-  apply (auto simp add: Ints_def)
-  apply (rule range_eqI)
-  apply (rule of_int_diff [symmetric])
-  done
+  by (force simp add: Ints_def simp flip: of_int_diff intro: range_eqI)
 
 lemma Ints_mult [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a * b \<in> \<int>"
-  apply (auto simp add: Ints_def)
-  apply (rule range_eqI)
-  apply (rule of_int_mult [symmetric])
-  done
+  by (force simp add: Ints_def simp flip: of_int_mult intro: range_eqI)
 
 lemma Ints_power [simp]: "a \<in> \<int> \<Longrightarrow> a ^ n \<in> \<int>"
   by (induct n) simp_all
 
 lemma Ints_cases [cases set: Ints]:
   assumes "q \<in> \<int>"
   obtains (of_int) z where "q = of_int z"
   unfolding Ints_def
 proof -
   from \<open>q \<in> \<int>\<close> have "q \<in> range of_int" unfolding Ints_def .
   then obtain z where "q = of_int z" ..
   then show thesis ..
 qed
 
 lemma Ints_induct [case_names of_int, induct set: Ints]:
   "q \<in> \<int> \<Longrightarrow> (\<And>z. P (of_int z)) \<Longrightarrow> P q"
   by (rule Ints_cases) auto
 
 lemma Nats_subset_Ints: "\<nat> \<subseteq> \<int>"
   unfolding Nats_def Ints_def
   by (rule subsetI, elim imageE, hypsubst, subst of_int_of_nat_eq[symmetric], rule imageI) simp_all
 
 lemma Nats_altdef1: "\<nat> = {of_int n |n. n \<ge> 0}"
 proof (intro subsetI equalityI)
   fix x :: 'a
   assume "x \<in> {of_int n |n. n \<ge> 0}"
   then obtain n where "x = of_int n" "n \<ge> 0"
     by (auto elim!: Ints_cases)
   then have "x = of_nat (nat n)"
     by (subst of_nat_nat) simp_all
   then show "x \<in> \<nat>"
     by simp
 next
   fix x :: 'a
   assume "x \<in> \<nat>"
   then obtain n where "x = of_nat n"
     by (auto elim!: Nats_cases)
   then have "x = of_int (int n)" by simp
   also have "int n \<ge> 0" by simp
   then have "of_int (int n) \<in> {of_int n |n. n \<ge> 0}" by blast
   finally show "x \<in> {of_int n |n. n \<ge> 0}" .
 qed
 
 end
 
 lemma (in linordered_idom) Ints_abs [simp]:
   shows "a \<in> \<int> \<Longrightarrow> abs a \<in> \<int>"
   by (auto simp: abs_if)
 
 lemma (in linordered_idom) Nats_altdef2: "\<nat> = {n \<in> \<int>. n \<ge> 0}"
 proof (intro subsetI equalityI)
   fix x :: 'a
   assume "x \<in> {n \<in> \<int>. n \<ge> 0}"
   then obtain n where "x = of_int n" "n \<ge> 0"
     by (auto elim!: Ints_cases)
   then have "x = of_nat (nat n)"
     by (subst of_nat_nat) simp_all
   then show "x \<in> \<nat>"
     by simp
 qed (auto elim!: Nats_cases)
 
 lemma (in idom_divide) of_int_divide_in_Ints: 
   "of_int a div of_int b \<in> \<int>" if "b dvd a"
 proof -
   from that obtain c where "a = b * c" ..
   then show ?thesis
     by (cases "of_int b = 0") simp_all
 qed
 
 text \<open>The premise involving \<^term>\<open>Ints\<close> prevents \<^term>\<open>a = 1/2\<close>.\<close>
 
 lemma Ints_double_eq_0_iff:
   fixes a :: "'a::ring_char_0"
   assumes in_Ints: "a \<in> \<int>"
   shows "a + a = 0 \<longleftrightarrow> a = 0"
     (is "?lhs \<longleftrightarrow> ?rhs")
 proof -
   from in_Ints have "a \<in> range of_int"
     unfolding Ints_def [symmetric] .
   then obtain z where a: "a = of_int z" ..
   show ?thesis
   proof
     assume ?rhs
     then show ?lhs by simp
   next
     assume ?lhs
     with a have "of_int (z + z) = (of_int 0 :: 'a)" by simp
     then have "z + z = 0" by (simp only: of_int_eq_iff)
     then have "z = 0" by (simp only: double_zero)
     with a show ?rhs by simp
   qed
 qed
 
 lemma Ints_odd_nonzero:
   fixes a :: "'a::ring_char_0"
   assumes in_Ints: "a \<in> \<int>"
   shows "1 + a + a \<noteq> 0"
 proof -
   from in_Ints have "a \<in> range of_int"
     unfolding Ints_def [symmetric] .
   then obtain z where a: "a = of_int z" ..
   show ?thesis
   proof
     assume "1 + a + a = 0"
     with a have "of_int (1 + z + z) = (of_int 0 :: 'a)" by simp
     then have "1 + z + z = 0" by (simp only: of_int_eq_iff)
     with odd_nonzero show False by blast
   qed
 qed
 
 lemma Nats_numeral [simp]: "numeral w \<in> \<nat>"
   using of_nat_in_Nats [of "numeral w"] by simp
 
 lemma Ints_odd_less_0:
   fixes a :: "'a::linordered_idom"
   assumes in_Ints: "a \<in> \<int>"
   shows "1 + a + a < 0 \<longleftrightarrow> a < 0"
 proof -
   from in_Ints have "a \<in> range of_int"
     unfolding Ints_def [symmetric] .
   then obtain z where a: "a = of_int z" ..
   with a have "1 + a + a < 0 \<longleftrightarrow> of_int (1 + z + z) < (of_int 0 :: 'a)"
     by simp
   also have "\<dots> \<longleftrightarrow> z < 0"
     by (simp only: of_int_less_iff odd_less_0_iff)
   also have "\<dots> \<longleftrightarrow> a < 0"
     by (simp add: a)
   finally show ?thesis .
 qed
 
 
 subsection \<open>\<^term>\<open>sum\<close> and \<^term>\<open>prod\<close>\<close>
 
 context semiring_1
 begin
 
 lemma of_nat_sum [simp]:
   "of_nat (sum f A) = (\<Sum>x\<in>A. of_nat (f x))"
   by (induction A rule: infinite_finite_induct) auto
 
 end
 
 context ring_1
 begin
 
 lemma of_int_sum [simp]:
   "of_int (sum f A) = (\<Sum>x\<in>A. of_int (f x))"
   by (induction A rule: infinite_finite_induct) auto
 
 end
 
 context comm_semiring_1
 begin
 
 lemma of_nat_prod [simp]:
   "of_nat (prod f A) = (\<Prod>x\<in>A. of_nat (f x))"
   by (induction A rule: infinite_finite_induct) auto
 
 end
 
 context comm_ring_1
 begin
 
 lemma of_int_prod [simp]:
   "of_int (prod f A) = (\<Prod>x\<in>A. of_int (f x))"
   by (induction A rule: infinite_finite_induct) auto
 
 end
 
 
 subsection \<open>Setting up simplification procedures\<close>
 
 ML_file \<open>Tools/int_arith.ML\<close>
 
 declaration \<open>K (
   Lin_Arith.add_discrete_type \<^type_name>\<open>Int.int\<close>
   #> Lin_Arith.add_lessD @{thm zless_imp_add1_zle}
   #> Lin_Arith.add_inj_thms @{thms of_nat_le_iff [THEN iffD2] of_nat_eq_iff [THEN iffD2]}
   #> Lin_Arith.add_inj_const (\<^const_name>\<open>of_nat\<close>, \<^typ>\<open>nat \<Rightarrow> int\<close>)
   #> Lin_Arith.add_simps
       @{thms of_int_0 of_int_1 of_int_add of_int_mult of_int_numeral of_int_neg_numeral nat_0 nat_1 diff_nat_numeral nat_numeral
       neg_less_iff_less
       True_implies_equals
       distrib_left [where a = "numeral v" for v]
       distrib_left [where a = "- numeral v" for v]
       div_by_1 div_0
       times_divide_eq_right times_divide_eq_left
       minus_divide_left [THEN sym] minus_divide_right [THEN sym]
       add_divide_distrib diff_divide_distrib
       of_int_minus of_int_diff
       of_int_of_nat_eq}
   #> Lin_Arith.add_simprocs [Int_Arith.zero_one_idom_simproc]
 )\<close>
 
 simproc_setup fast_arith
   ("(m::'a::linordered_idom) < n" |
     "(m::'a::linordered_idom) \<le> n" |
     "(m::'a::linordered_idom) = n") =
   \<open>K Lin_Arith.simproc\<close>
 
 
 subsection\<open>More Inequality Reasoning\<close>
 
 lemma zless_add1_eq: "w < z + 1 \<longleftrightarrow> w < z \<or> w = z"
   for w z :: int
   by arith
 
 lemma add1_zle_eq: "w + 1 \<le> z \<longleftrightarrow> w < z"
   for w z :: int
   by arith
 
 lemma zle_diff1_eq [simp]: "w \<le> z - 1 \<longleftrightarrow> w < z"
   for w z :: int
   by arith
 
 lemma zle_add1_eq_le [simp]: "w < z + 1 \<longleftrightarrow> w \<le> z"
   for w z :: int
   by arith
 
 lemma int_one_le_iff_zero_less: "1 \<le> z \<longleftrightarrow> 0 < z"
   for z :: int
   by arith
 
 lemma Ints_nonzero_abs_ge1:
   fixes x:: "'a :: linordered_idom"
     assumes "x \<in> Ints" "x \<noteq> 0"
     shows "1 \<le> abs x"
 proof (rule Ints_cases [OF \<open>x \<in> Ints\<close>])
   fix z::int
   assume "x = of_int z"
     with \<open>x \<noteq> 0\<close> 
   show "1 \<le> \<bar>x\<bar>"
     apply (auto simp add: abs_if)
     by (metis diff_0 of_int_1 of_int_le_iff of_int_minus zle_diff1_eq)
 qed
   
 lemma Ints_nonzero_abs_less1:
   fixes x:: "'a :: linordered_idom"
   shows "\<lbrakk>x \<in> Ints; abs x < 1\<rbrakk> \<Longrightarrow> x = 0"
     using Ints_nonzero_abs_ge1 [of x] by auto
 
 lemma Ints_eq_abs_less1:
   fixes x:: "'a :: linordered_idom"
   shows "\<lbrakk>x \<in> Ints; y \<in> Ints\<rbrakk> \<Longrightarrow> x = y \<longleftrightarrow> abs (x-y) < 1"
   using eq_iff_diff_eq_0 by (fastforce intro: Ints_nonzero_abs_less1)
  
 
 subsection \<open>The functions \<^term>\<open>nat\<close> and \<^term>\<open>int\<close>\<close>
 
 text \<open>Simplify the term \<^term>\<open>w + - z\<close>.\<close>
 
 lemma one_less_nat_eq [simp]: "Suc 0 < nat z \<longleftrightarrow> 1 < z"
   using zless_nat_conj [of 1 z] by auto
 
 lemma int_eq_iff_numeral [simp]:
   "int m = numeral v \<longleftrightarrow> m = numeral v"
   by (simp add: int_eq_iff)
 
 lemma nat_abs_int_diff:
   "nat \<bar>int a - int b\<bar> = (if a \<le> b then b - a else a - b)"
   by auto
 
 lemma nat_int_add: "nat (int a + int b) = a + b"
   by auto
 
 context ring_1
 begin
 
 lemma of_int_of_nat [nitpick_simp]:
   "of_int k = (if k < 0 then - of_nat (nat (- k)) else of_nat (nat k))"
 proof (cases "k < 0")
   case True
   then have "0 \<le> - k" by simp
   then have "of_nat (nat (- k)) = of_int (- k)" by (rule of_nat_nat)
   with True show ?thesis by simp
 next
   case False
   then show ?thesis by (simp add: not_less)
 qed
 
 end
 
 lemma transfer_rule_of_int:
   includes lifting_syntax
   fixes R :: "'a::ring_1 \<Rightarrow> 'b::ring_1 \<Rightarrow> bool"
   assumes [transfer_rule]: "R 0 0" "R 1 1"
     "(R ===> R ===> R) (+) (+)"
     "(R ===> R) uminus uminus"
   shows "((=) ===> R) of_int of_int"
 proof -
   note assms
   note transfer_rule_of_nat [transfer_rule]
   have [transfer_rule]: "((=) ===> R) of_nat of_nat"
     by transfer_prover
   show ?thesis
     by (unfold of_int_of_nat [abs_def]) transfer_prover
 qed
 
 lemma nat_mult_distrib:
   fixes z z' :: int
   assumes "0 \<le> z"
   shows "nat (z * z') = nat z * nat z'"
 proof (cases "0 \<le> z'")
   case False
   with assms have "z * z' \<le> 0"
     by (simp add: not_le mult_le_0_iff)
   then have "nat (z * z') = 0" by simp
   moreover from False have "nat z' = 0" by simp
   ultimately show ?thesis by simp
 next
   case True
   with assms have ge_0: "z * z' \<ge> 0" by (simp add: zero_le_mult_iff)
   show ?thesis
     by (rule injD [of "of_nat :: nat \<Rightarrow> int", OF inj_of_nat])
       (simp only: of_nat_mult of_nat_nat [OF True]
          of_nat_nat [OF assms] of_nat_nat [OF ge_0], simp)
 qed
 
-lemma nat_mult_distrib_neg: "z \<le> 0 \<Longrightarrow> nat (z * z') = nat (- z) * nat (- z')"
-  for z z' :: int
-  apply (rule trans)
-   apply (rule_tac [2] nat_mult_distrib)
-   apply auto
-  done
+lemma nat_mult_distrib_neg:
+  assumes "z \<le> (0::int)" shows "nat (z * z') = nat (- z) * nat (- z')" (is "?L = ?R")
+proof -
+  have "?L = nat (- z * - z')"
+    using assms by auto
+  also have "... = ?R"
+    by (rule nat_mult_distrib) (use assms in auto)
+  finally show ?thesis .
+qed
 
 lemma nat_abs_mult_distrib: "nat \<bar>w * z\<bar> = nat \<bar>w\<bar> * nat \<bar>z\<bar>"
   by (cases "z = 0 \<or> w = 0")
     (auto simp add: abs_if nat_mult_distrib [symmetric]
       nat_mult_distrib_neg [symmetric] mult_less_0_iff)
 
 lemma int_in_range_abs [simp]: "int n \<in> range abs"
 proof (rule range_eqI)
   show "int n = \<bar>int n\<bar>" by simp
 qed
 
 lemma range_abs_Nats [simp]: "range abs = (\<nat> :: int set)"
 proof -
   have "\<bar>k\<bar> \<in> \<nat>" for k :: int
     by (cases k) simp_all
   moreover have "k \<in> range abs" if "k \<in> \<nat>" for k :: int
     using that by induct simp
   ultimately show ?thesis by blast
 qed
 
 lemma Suc_nat_eq_nat_zadd1: "0 \<le> z \<Longrightarrow> Suc (nat z) = nat (1 + z)"
   for z :: int
   by (rule sym) (simp add: nat_eq_iff)
 
 lemma diff_nat_eq_if:
   "nat z - nat z' =
     (if z' < 0 then nat z
      else
       let d = z - z'
       in if d < 0 then 0 else nat d)"
   by (simp add: Let_def nat_diff_distrib [symmetric])
 
 lemma nat_numeral_diff_1 [simp]: "numeral v - (1::nat) = nat (numeral v - 1)"
   using diff_nat_numeral [of v Num.One] by simp
 
 
 subsection \<open>Induction principles for int\<close>
 
 text \<open>Well-founded segments of the integers.\<close>
 
 definition int_ge_less_than :: "int \<Rightarrow> (int \<times> int) set"
   where "int_ge_less_than d = {(z', z). d \<le> z' \<and> z' < z}"
 
 lemma wf_int_ge_less_than: "wf (int_ge_less_than d)"
 proof -
   have "int_ge_less_than d \<subseteq> measure (\<lambda>z. nat (z - d))"
     by (auto simp add: int_ge_less_than_def)
   then show ?thesis
     by (rule wf_subset [OF wf_measure])
 qed
 
 text \<open>
   This variant looks odd, but is typical of the relations suggested
   by RankFinder.\<close>
 
 definition int_ge_less_than2 :: "int \<Rightarrow> (int \<times> int) set"
   where "int_ge_less_than2 d = {(z',z). d \<le> z \<and> z' < z}"
 
 lemma wf_int_ge_less_than2: "wf (int_ge_less_than2 d)"
 proof -
   have "int_ge_less_than2 d \<subseteq> measure (\<lambda>z. nat (1 + z - d))"
     by (auto simp add: int_ge_less_than2_def)
   then show ?thesis
     by (rule wf_subset [OF wf_measure])
 qed
 
 (* `set:int': dummy construction *)
 theorem int_ge_induct [case_names base step, induct set: int]:
   fixes i :: int
   assumes ge: "k \<le> i"
     and base: "P k"
     and step: "\<And>i. k \<le> i \<Longrightarrow> P i \<Longrightarrow> P (i + 1)"
   shows "P i"
 proof -
   have "\<And>i::int. n = nat (i - k) \<Longrightarrow> k \<le> i \<Longrightarrow> P i" for n
   proof (induct n)
     case 0
     then have "i = k" by arith
     with base show "P i" by simp
   next
     case (Suc n)
     then have "n = nat ((i - 1) - k)" by arith
     moreover have k: "k \<le> i - 1" using Suc.prems by arith
     ultimately have "P (i - 1)" by (rule Suc.hyps)
     from step [OF k this] show ?case by simp
   qed
   with ge show ?thesis by fast
 qed
 
 (* `set:int': dummy construction *)
 theorem int_gr_induct [case_names base step, induct set: int]:
   fixes i k :: int
-  assumes gr: "k < i"
-    and base: "P (k + 1)"
-    and step: "\<And>i. k < i \<Longrightarrow> P i \<Longrightarrow> P (i + 1)"
+  assumes "k < i" "P (k + 1)" "\<And>i. k < i \<Longrightarrow> P i \<Longrightarrow> P (i + 1)"
   shows "P i"
-  apply (rule int_ge_induct[of "k + 1"])
-  using gr apply arith
-   apply (rule base)
-  apply (rule step)
-   apply simp_all
-  done
+proof -
+  have "k+1 \<le> i"
+    using assms by auto
+  then show ?thesis
+    by (induction i rule: int_ge_induct) (auto simp: assms)
+qed
 
 theorem int_le_induct [consumes 1, case_names base step]:
   fixes i k :: int
   assumes le: "i \<le> k"
     and base: "P k"
     and step: "\<And>i. i \<le> k \<Longrightarrow> P i \<Longrightarrow> P (i - 1)"
   shows "P i"
 proof -
   have "\<And>i::int. n = nat(k-i) \<Longrightarrow> i \<le> k \<Longrightarrow> P i" for n
   proof (induct n)
     case 0
     then have "i = k" by arith
     with base show "P i" by simp
   next
     case (Suc n)
     then have "n = nat (k - (i + 1))" by arith
     moreover have k: "i + 1 \<le> k" using Suc.prems by arith
     ultimately have "P (i + 1)" by (rule Suc.hyps)
     from step[OF k this] show ?case by simp
   qed
   with le show ?thesis by fast
 qed
 
 theorem int_less_induct [consumes 1, case_names base step]:
   fixes i k :: int
-  assumes less: "i < k"
-    and base: "P (k - 1)"
-    and step: "\<And>i. i < k \<Longrightarrow> P i \<Longrightarrow> P (i - 1)"
+  assumes "i < k" "P (k - 1)" "\<And>i. i < k \<Longrightarrow> P i \<Longrightarrow> P (i - 1)"
   shows "P i"
-  apply (rule int_le_induct[of _ "k - 1"])
-  using less apply arith
-   apply (rule base)
-  apply (rule step)
-   apply simp_all
-  done
+proof -
+  have "i \<le> k-1"
+    using assms by auto
+  then show ?thesis
+    by (induction i rule: int_le_induct) (auto simp: assms)
+qed
 
 theorem int_induct [case_names base step1 step2]:
   fixes k :: int
   assumes base: "P k"
     and step1: "\<And>i. k \<le> i \<Longrightarrow> P i \<Longrightarrow> P (i + 1)"
     and step2: "\<And>i. k \<ge> i \<Longrightarrow> P i \<Longrightarrow> P (i - 1)"
   shows "P i"
 proof -
   have "i \<le> k \<or> i \<ge> k" by arith
   then show ?thesis
   proof
     assume "i \<ge> k"
     then show ?thesis
       using base by (rule int_ge_induct) (fact step1)
   next
     assume "i \<le> k"
     then show ?thesis
       using base by (rule int_le_induct) (fact step2)
   qed
 qed
 
 
 subsection \<open>Intermediate value theorems\<close>
 
+lemma nat_ivt_aux: 
+  "\<lbrakk>\<forall>i<n. \<bar>f (Suc i) - f i\<bar> \<le> 1; f 0 \<le> k; k \<le> f n\<rbrakk> \<Longrightarrow> \<exists>i \<le> n. f i = k"
+  for m n :: nat and k :: int
+proof (induct n)
+  case (Suc n)
+  show ?case
+  proof (cases "k = f (Suc n)")
+    case False
+    with Suc have "k \<le> f n"
+      by auto
+    with Suc show ?thesis
+      by (auto simp add: abs_if split: if_split_asm intro: le_SucI)
+  qed (use Suc in auto)
+qed auto
+
 lemma nat_intermed_int_val:
-  "\<exists>i. m \<le> i \<and> i \<le> n \<and> f i = k"
-  if "\<forall>i. m \<le> i \<and> i < n \<longrightarrow> \<bar>f (Suc i) - f i\<bar> \<le> 1"
-    "m \<le> n" "f m \<le> k" "k \<le> f n"
-  for m n :: nat and k :: int
+  fixes m n :: nat and k :: int
+  assumes "\<forall>i. m \<le> i \<and> i < n \<longrightarrow> \<bar>f (Suc i) - f i\<bar> \<le> 1" "m \<le> n" "f m \<le> k" "k \<le> f n"
+  shows "\<exists>i. m \<le> i \<and> i \<le> n \<and> f i = k"
 proof -
-  have "(\<forall>i<n. \<bar>f (Suc i) - f i\<bar> \<le> 1) \<Longrightarrow> f 0 \<le> k \<Longrightarrow> k \<le> f n
-    \<Longrightarrow> (\<exists>i \<le> n. f i = k)"
-  for n :: nat and f
-    apply (induct n)
-     apply auto
-    apply (erule_tac x = n in allE)
-    apply (case_tac "k = f (Suc n)")
-     apply (auto simp add: abs_if split: if_split_asm intro: le_SucI)
-    done
-  from this [of "n - m" "f \<circ> plus m"] that show ?thesis
-    apply auto
-    apply (rule_tac x = "m + i" in exI)
-    apply auto
-    done
+  obtain i where "i \<le> n - m" "k = f (m + i)"
+    using nat_ivt_aux [of "n - m" "f \<circ> plus m" k] assms by auto
+  with assms show ?thesis
+    by (rule_tac x = "m + i" in exI) auto
 qed
 
 lemma nat0_intermed_int_val:
   "\<exists>i\<le>n. f i = k"
   if "\<forall>i<n. \<bar>f (i + 1) - f i\<bar> \<le> 1" "f 0 \<le> k" "k \<le> f n"
   for n :: nat and k :: int
   using nat_intermed_int_val [of 0 n f k] that by auto
 
 
 subsection \<open>Products and 1, by T. M. Rasmussen\<close>
 
 lemma abs_zmult_eq_1:
   fixes m n :: int
   assumes mn: "\<bar>m * n\<bar> = 1"
   shows "\<bar>m\<bar> = 1"
 proof -
   from mn have 0: "m \<noteq> 0" "n \<noteq> 0" by auto
   have "\<not> 2 \<le> \<bar>m\<bar>"
   proof
     assume "2 \<le> \<bar>m\<bar>"
     then have "2 * \<bar>n\<bar> \<le> \<bar>m\<bar> * \<bar>n\<bar>" by (simp add: mult_mono 0)
     also have "\<dots> = \<bar>m * n\<bar>" by (simp add: abs_mult)
     also from mn have "\<dots> = 1" by simp
     finally have "2 * \<bar>n\<bar> \<le> 1" .
     with 0 show "False" by arith
   qed
   with 0 show ?thesis by auto
 qed
 
 lemma pos_zmult_eq_1_iff_lemma: "m * n = 1 \<Longrightarrow> m = 1 \<or> m = - 1"
   for m n :: int
   using abs_zmult_eq_1 [of m n] by arith
 
 lemma pos_zmult_eq_1_iff:
   fixes m n :: int
   assumes "0 < m"
   shows "m * n = 1 \<longleftrightarrow> m = 1 \<and> n = 1"
 proof -
   from assms have "m * n = 1 \<Longrightarrow> m = 1"
     by (auto dest: pos_zmult_eq_1_iff_lemma)
   then show ?thesis
     by (auto dest: pos_zmult_eq_1_iff_lemma)
 qed
 
-lemma zmult_eq_1_iff: "m * n = 1 \<longleftrightarrow> (m = 1 \<and> n = 1) \<or> (m = - 1 \<and> n = - 1)"
+lemma zmult_eq_1_iff: "m * n = 1 \<longleftrightarrow> (m = 1 \<and> n = 1) \<or> (m = - 1 \<and> n = - 1)" (is "?L = ?R")
   for m n :: int
-  apply (rule iffI)
-   apply (frule pos_zmult_eq_1_iff_lemma)
-   apply (simp add: mult.commute [of m])
-   apply (frule pos_zmult_eq_1_iff_lemma)
-   apply auto
-  done
+proof
+  assume L: ?L show ?R
+    using pos_zmult_eq_1_iff_lemma [OF L] L by force
+qed auto
 
 lemma infinite_UNIV_int [simp]: "\<not> finite (UNIV::int set)"
 proof
   assume "finite (UNIV::int set)"
   moreover have "inj (\<lambda>i::int. 2 * i)"
     by (rule injI) simp
   ultimately have "surj (\<lambda>i::int. 2 * i)"
     by (rule finite_UNIV_inj_surj)
   then obtain i :: int where "1 = 2 * i" by (rule surjE)
   then show False by (simp add: pos_zmult_eq_1_iff)
 qed
 
 
 subsection \<open>The divides relation\<close>
 
 lemma zdvd_antisym_nonneg: "0 \<le> m \<Longrightarrow> 0 \<le> n \<Longrightarrow> m dvd n \<Longrightarrow> n dvd m \<Longrightarrow> m = n"
   for m n :: int
   by (auto simp add: dvd_def mult.assoc zero_le_mult_iff zmult_eq_1_iff)
 
 lemma zdvd_antisym_abs:
   fixes a b :: int
   assumes "a dvd b" and "b dvd a"
   shows "\<bar>a\<bar> = \<bar>b\<bar>"
 proof (cases "a = 0")
   case True
   with assms show ?thesis by simp
 next
   case False
   from \<open>a dvd b\<close> obtain k where k: "b = a * k"
     unfolding dvd_def by blast
   from \<open>b dvd a\<close> obtain k' where k': "a = b * k'"
     unfolding dvd_def by blast
   from k k' have "a = a * k * k'" by simp
   with mult_cancel_left1[where c="a" and b="k*k'"] have kk': "k * k' = 1"
     using \<open>a \<noteq> 0\<close> by (simp add: mult.assoc)
   then have "k = 1 \<and> k' = 1 \<or> k = -1 \<and> k' = -1"
     by (simp add: zmult_eq_1_iff)
   with k k' show ?thesis by auto
 qed
 
 lemma zdvd_zdiffD: "k dvd m - n \<Longrightarrow> k dvd n \<Longrightarrow> k dvd m"
   for k m n :: int
   using dvd_add_right_iff [of k "- n" m] by simp
 
 lemma zdvd_reduce: "k dvd n + k * m \<longleftrightarrow> k dvd n"
   for k m n :: int
   using dvd_add_times_triv_right_iff [of k n m] by (simp add: ac_simps)
 
 lemma dvd_imp_le_int:
   fixes d i :: int
   assumes "i \<noteq> 0" and "d dvd i"
   shows "\<bar>d\<bar> \<le> \<bar>i\<bar>"
 proof -
   from \<open>d dvd i\<close> obtain k where "i = d * k" ..
   with \<open>i \<noteq> 0\<close> have "k \<noteq> 0" by auto
   then have "1 \<le> \<bar>k\<bar>" and "0 \<le> \<bar>d\<bar>" by auto
   then have "\<bar>d\<bar> * 1 \<le> \<bar>d\<bar> * \<bar>k\<bar>" by (rule mult_left_mono)
   with \<open>i = d * k\<close> show ?thesis by (simp add: abs_mult)
 qed
 
 lemma zdvd_not_zless:
   fixes m n :: int
   assumes "0 < m" and "m < n"
   shows "\<not> n dvd m"
 proof
   from assms have "0 < n" by auto
   assume "n dvd m" then obtain k where k: "m = n * k" ..
   with \<open>0 < m\<close> have "0 < n * k" by auto
   with \<open>0 < n\<close> have "0 < k" by (simp add: zero_less_mult_iff)
   with k \<open>0 < n\<close> \<open>m < n\<close> have "n * k < n * 1" by simp
   with \<open>0 < n\<close> \<open>0 < k\<close> show False unfolding mult_less_cancel_left by auto
 qed
 
 lemma zdvd_mult_cancel:
   fixes k m n :: int
   assumes d: "k * m dvd k * n"
     and "k \<noteq> 0"
   shows "m dvd n"
 proof -
   from d obtain h where h: "k * n = k * m * h"
     unfolding dvd_def by blast
   have "n = m * h"
   proof (rule ccontr)
     assume "\<not> ?thesis"
     with \<open>k \<noteq> 0\<close> have "k * n \<noteq> k * (m * h)" by simp
     with h show False
       by (simp add: mult.assoc)
   qed
   then show ?thesis by simp
 qed
 
 lemma int_dvd_int_iff [simp]:
   "int m dvd int n \<longleftrightarrow> m dvd n"
 proof -
   have "m dvd n" if "int n = int m * k" for k
   proof (cases k)
     case (nonneg q)
     with that have "n = m * q"
       by (simp del: of_nat_mult add: of_nat_mult [symmetric])
     then show ?thesis ..
   next
     case (neg q)
     with that have "int n = int m * (- int (Suc q))"
       by simp
     also have "\<dots> = - (int m * int (Suc q))"
       by (simp only: mult_minus_right)
     also have "\<dots> = - int (m * Suc q)"
       by (simp only: of_nat_mult [symmetric])
     finally have "- int (m * Suc q) = int n" ..
     then show ?thesis
       by (simp only: negative_eq_positive) auto
   qed
   then show ?thesis by (auto simp add: dvd_def)
 qed
 
 lemma dvd_nat_abs_iff [simp]:
   "n dvd nat \<bar>k\<bar> \<longleftrightarrow> int n dvd k"
 proof -
   have "n dvd nat \<bar>k\<bar> \<longleftrightarrow> int n dvd int (nat \<bar>k\<bar>)"
     by (simp only: int_dvd_int_iff)
   then show ?thesis
     by simp
 qed
 
 lemma nat_abs_dvd_iff [simp]:
   "nat \<bar>k\<bar> dvd n \<longleftrightarrow> k dvd int n"
 proof -
   have "nat \<bar>k\<bar> dvd n \<longleftrightarrow> int (nat \<bar>k\<bar>) dvd int n"
     by (simp only: int_dvd_int_iff)
   then show ?thesis
     by simp
 qed
 
 lemma zdvd1_eq [simp]: "x dvd 1 \<longleftrightarrow> \<bar>x\<bar> = 1" (is "?lhs \<longleftrightarrow> ?rhs")
   for x :: int
 proof
   assume ?lhs
   then have "nat \<bar>x\<bar> dvd nat \<bar>1\<bar>"
     by (simp only: nat_abs_dvd_iff) simp
   then have "nat \<bar>x\<bar> = 1"
     by simp
   then show ?rhs
     by (cases "x < 0") simp_all
 next
   assume ?rhs
   then have "x = 1 \<or> x = - 1"
     by auto
   then show ?lhs
     by (auto intro: dvdI)
 qed
 
 lemma zdvd_mult_cancel1:
   fixes m :: int
   assumes mp: "m \<noteq> 0"
   shows "m * n dvd m \<longleftrightarrow> \<bar>n\<bar> = 1"
     (is "?lhs \<longleftrightarrow> ?rhs")
 proof
   assume ?rhs
   then show ?lhs
     by (cases "n > 0") (auto simp add: minus_equation_iff)
 next
   assume ?lhs
   then have "m * n dvd m * 1" by simp
   from zdvd_mult_cancel[OF this mp] show ?rhs
     by (simp only: zdvd1_eq)
 qed
 
 lemma nat_dvd_iff: "nat z dvd m \<longleftrightarrow> (if 0 \<le> z then z dvd int m else m = 0)"
   using nat_abs_dvd_iff [of z m] by (cases "z \<ge> 0") auto
 
 lemma eq_nat_nat_iff: "0 \<le> z \<Longrightarrow> 0 \<le> z' \<Longrightarrow> nat z = nat z' \<longleftrightarrow> z = z'"
   by (auto elim: nonneg_int_cases)
 
 lemma nat_power_eq: "0 \<le> z \<Longrightarrow> nat (z ^ n) = nat z ^ n"
   by (induct n) (simp_all add: nat_mult_distrib)
 
 lemma numeral_power_eq_nat_cancel_iff [simp]:
   "numeral x ^ n = nat y \<longleftrightarrow> numeral x ^ n = y"
   using nat_eq_iff2 by auto
 
 lemma nat_eq_numeral_power_cancel_iff [simp]:
   "nat y = numeral x ^ n \<longleftrightarrow> y = numeral x ^ n"
   using numeral_power_eq_nat_cancel_iff[of x n y]
   by (metis (mono_tags))
 
 lemma numeral_power_le_nat_cancel_iff [simp]:
   "numeral x ^ n \<le> nat a \<longleftrightarrow> numeral x ^ n \<le> a"
   using nat_le_eq_zle[of "numeral x ^ n" a]
   by (auto simp: nat_power_eq)
 
 lemma nat_le_numeral_power_cancel_iff [simp]:
   "nat a \<le> numeral x ^ n \<longleftrightarrow> a \<le> numeral x ^ n"
   by (simp add: nat_le_iff)
 
 lemma numeral_power_less_nat_cancel_iff [simp]:
   "numeral x ^ n < nat a \<longleftrightarrow> numeral x ^ n < a"
   using nat_less_eq_zless[of "numeral x ^ n" a]
   by (auto simp: nat_power_eq)
 
 lemma nat_less_numeral_power_cancel_iff [simp]:
   "nat a < numeral x ^ n \<longleftrightarrow> a < numeral x ^ n"
   using nat_less_eq_zless[of a "numeral x ^ n"]
   by (cases "a < 0") (auto simp: nat_power_eq less_le_trans[where y=0])
 
-lemma zdvd_imp_le: "z dvd n \<Longrightarrow> 0 < n \<Longrightarrow> z \<le> n"
-  for n z :: int
-  apply (cases n)
-  apply auto
-  apply (cases z)
-   apply (auto simp add: dvd_imp_le)
-  done
+lemma zdvd_imp_le: "z \<le> n" if "z dvd n" "0 < n" for n z :: int
+proof (cases n)
+  case (nonneg n)
+  show ?thesis
+    by (cases z) (use nonneg dvd_imp_le that in auto)
+qed (use that in auto)
 
 lemma zdvd_period:
   fixes a d :: int
   assumes "a dvd d"
   shows "a dvd (x + t) \<longleftrightarrow> a dvd ((x + c * d) + t)"
     (is "?lhs \<longleftrightarrow> ?rhs")
 proof -
   from assms have "a dvd (x + t) \<longleftrightarrow> a dvd ((x + t) + c * d)"
     by (simp add: dvd_add_left_iff)
   then show ?thesis
     by (simp add: ac_simps)
 qed
 
 
 subsection \<open>Finiteness of intervals\<close>
 
 lemma finite_interval_int1 [iff]: "finite {i :: int. a \<le> i \<and> i \<le> b}"
 proof (cases "a \<le> b")
   case True
   then show ?thesis
   proof (induct b rule: int_ge_induct)
     case base
     have "{i. a \<le> i \<and> i \<le> a} = {a}" by auto
     then show ?case by simp
   next
     case (step b)
     then have "{i. a \<le> i \<and> i \<le> b + 1} = {i. a \<le> i \<and> i \<le> b} \<union> {b + 1}" by auto
     with step show ?case by simp
   qed
 next
   case False
   then show ?thesis
     by (metis (lifting, no_types) Collect_empty_eq finite.emptyI order_trans)
 qed
 
 lemma finite_interval_int2 [iff]: "finite {i :: int. a \<le> i \<and> i < b}"
   by (rule rev_finite_subset[OF finite_interval_int1[of "a" "b"]]) auto
 
 lemma finite_interval_int3 [iff]: "finite {i :: int. a < i \<and> i \<le> b}"
   by (rule rev_finite_subset[OF finite_interval_int1[of "a" "b"]]) auto
 
 lemma finite_interval_int4 [iff]: "finite {i :: int. a < i \<and> i < b}"
   by (rule rev_finite_subset[OF finite_interval_int1[of "a" "b"]]) auto
 
 
 subsection \<open>Configuration of the code generator\<close>
 
 text \<open>Constructors\<close>
 
 definition Pos :: "num \<Rightarrow> int"
   where [simp, code_abbrev]: "Pos = numeral"
 
 definition Neg :: "num \<Rightarrow> int"
   where [simp, code_abbrev]: "Neg n = - (Pos n)"
 
 code_datatype "0::int" Pos Neg
 
 
 text \<open>Auxiliary operations.\<close>
 
 definition dup :: "int \<Rightarrow> int"
   where [simp]: "dup k = k + k"
 
 lemma dup_code [code]:
   "dup 0 = 0"
   "dup (Pos n) = Pos (Num.Bit0 n)"
   "dup (Neg n) = Neg (Num.Bit0 n)"
   by (simp_all add: numeral_Bit0)
 
 definition sub :: "num \<Rightarrow> num \<Rightarrow> int"
   where [simp]: "sub m n = numeral m - numeral n"
 
 lemma sub_code [code]:
   "sub Num.One Num.One = 0"
   "sub (Num.Bit0 m) Num.One = Pos (Num.BitM m)"
   "sub (Num.Bit1 m) Num.One = Pos (Num.Bit0 m)"
   "sub Num.One (Num.Bit0 n) = Neg (Num.BitM n)"
   "sub Num.One (Num.Bit1 n) = Neg (Num.Bit0 n)"
   "sub (Num.Bit0 m) (Num.Bit0 n) = dup (sub m n)"
   "sub (Num.Bit1 m) (Num.Bit1 n) = dup (sub m n)"
   "sub (Num.Bit1 m) (Num.Bit0 n) = dup (sub m n) + 1"
   "sub (Num.Bit0 m) (Num.Bit1 n) = dup (sub m n) - 1"
   by (simp_all only: sub_def dup_def numeral.simps Pos_def Neg_def numeral_BitM)
 
 text \<open>Implementations.\<close>
 
 lemma one_int_code [code]: "1 = Pos Num.One"
   by simp
 
 lemma plus_int_code [code]:
   "k + 0 = k"
   "0 + l = l"
   "Pos m + Pos n = Pos (m + n)"
   "Pos m + Neg n = sub m n"
   "Neg m + Pos n = sub n m"
   "Neg m + Neg n = Neg (m + n)"
   for k l :: int
   by simp_all
 
 lemma uminus_int_code [code]:
   "uminus 0 = (0::int)"
   "uminus (Pos m) = Neg m"
   "uminus (Neg m) = Pos m"
   by simp_all
 
 lemma minus_int_code [code]:
   "k - 0 = k"
   "0 - l = uminus l"
   "Pos m - Pos n = sub m n"
   "Pos m - Neg n = Pos (m + n)"
   "Neg m - Pos n = Neg (m + n)"
   "Neg m - Neg n = sub n m"
   for k l :: int
   by simp_all
 
 lemma times_int_code [code]:
   "k * 0 = 0"
   "0 * l = 0"
   "Pos m * Pos n = Pos (m * n)"
   "Pos m * Neg n = Neg (m * n)"
   "Neg m * Pos n = Neg (m * n)"
   "Neg m * Neg n = Pos (m * n)"
   for k l :: int
   by simp_all
 
 instantiation int :: equal
 begin
 
 definition "HOL.equal k l \<longleftrightarrow> k = (l::int)"
 
 instance
   by standard (rule equal_int_def)
 
 end
 
 lemma equal_int_code [code]:
   "HOL.equal 0 (0::int) \<longleftrightarrow> True"
   "HOL.equal 0 (Pos l) \<longleftrightarrow> False"
   "HOL.equal 0 (Neg l) \<longleftrightarrow> False"
   "HOL.equal (Pos k) 0 \<longleftrightarrow> False"
   "HOL.equal (Pos k) (Pos l) \<longleftrightarrow> HOL.equal k l"
   "HOL.equal (Pos k) (Neg l) \<longleftrightarrow> False"
   "HOL.equal (Neg k) 0 \<longleftrightarrow> False"
   "HOL.equal (Neg k) (Pos l) \<longleftrightarrow> False"
   "HOL.equal (Neg k) (Neg l) \<longleftrightarrow> HOL.equal k l"
   by (auto simp add: equal)
 
 lemma equal_int_refl [code nbe]: "HOL.equal k k \<longleftrightarrow> True"
   for k :: int
   by (fact equal_refl)
 
 lemma less_eq_int_code [code]:
   "0 \<le> (0::int) \<longleftrightarrow> True"
   "0 \<le> Pos l \<longleftrightarrow> True"
   "0 \<le> Neg l \<longleftrightarrow> False"
   "Pos k \<le> 0 \<longleftrightarrow> False"
   "Pos k \<le> Pos l \<longleftrightarrow> k \<le> l"
   "Pos k \<le> Neg l \<longleftrightarrow> False"
   "Neg k \<le> 0 \<longleftrightarrow> True"
   "Neg k \<le> Pos l \<longleftrightarrow> True"
   "Neg k \<le> Neg l \<longleftrightarrow> l \<le> k"
   by simp_all
 
 lemma less_int_code [code]:
   "0 < (0::int) \<longleftrightarrow> False"
   "0 < Pos l \<longleftrightarrow> True"
   "0 < Neg l \<longleftrightarrow> False"
   "Pos k < 0 \<longleftrightarrow> False"
   "Pos k < Pos l \<longleftrightarrow> k < l"
   "Pos k < Neg l \<longleftrightarrow> False"
   "Neg k < 0 \<longleftrightarrow> True"
   "Neg k < Pos l \<longleftrightarrow> True"
   "Neg k < Neg l \<longleftrightarrow> l < k"
   by simp_all
 
 lemma nat_code [code]:
   "nat (Int.Neg k) = 0"
   "nat 0 = 0"
   "nat (Int.Pos k) = nat_of_num k"
   by (simp_all add: nat_of_num_numeral)
 
 lemma (in ring_1) of_int_code [code]:
   "of_int (Int.Neg k) = - numeral k"
   "of_int 0 = 0"
   "of_int (Int.Pos k) = numeral k"
   by simp_all
 
 
 text \<open>Serializer setup.\<close>
 
 code_identifier
   code_module Int \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
 
 quickcheck_params [default_type = int]
 
 hide_const (open) Pos Neg sub dup
 
 
 text \<open>De-register \<open>int\<close> as a quotient type:\<close>
 
 lifting_update int.lifting
 lifting_forget int.lifting
 
 
 subsection \<open>Duplicates\<close>
 
 lemmas int_sum = of_nat_sum [where 'a=int]
 lemmas int_prod = of_nat_prod [where 'a=int]
 lemmas zle_int = of_nat_le_iff [where 'a=int]
 lemmas int_int_eq = of_nat_eq_iff [where 'a=int]
 lemmas nonneg_eq_int = nonneg_int_cases
 lemmas double_eq_0_iff = double_zero
 
 lemmas int_distrib =
   distrib_right [of z1 z2 w]
   distrib_left [of w z1 z2]
   left_diff_distrib [of z1 z2 w]
   right_diff_distrib [of w z1 z2]
   for z1 z2 w :: int
 
 end
 
diff --git a/src/HOL/Map.thy b/src/HOL/Map.thy
--- a/src/HOL/Map.thy
+++ b/src/HOL/Map.thy
@@ -1,850 +1,862 @@
 (*  Title:      HOL/Map.thy
     Author:     Tobias Nipkow, based on a theory by David von Oheimb
     Copyright   1997-2003 TU Muenchen
 
 The datatype of "maps"; strongly resembles maps in VDM.
 *)
 
 section \<open>Maps\<close>
 
 theory Map
   imports List
   abbrevs "(=" = "\<subseteq>\<^sub>m"
 begin
 
 type_synonym ('a, 'b) "map" = "'a \<Rightarrow> 'b option" (infixr "\<rightharpoonup>" 0)
 
 abbreviation
   empty :: "'a \<rightharpoonup> 'b" where
   "empty \<equiv> \<lambda>x. None"
 
 definition
   map_comp :: "('b \<rightharpoonup> 'c) \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'c)"  (infixl "\<circ>\<^sub>m" 55) where
   "f \<circ>\<^sub>m g = (\<lambda>k. case g k of None \<Rightarrow> None | Some v \<Rightarrow> f v)"
 
 definition
   map_add :: "('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'b)"  (infixl "++" 100) where
   "m1 ++ m2 = (\<lambda>x. case m2 x of None \<Rightarrow> m1 x | Some y \<Rightarrow> Some y)"
 
 definition
   restrict_map :: "('a \<rightharpoonup> 'b) \<Rightarrow> 'a set \<Rightarrow> ('a \<rightharpoonup> 'b)"  (infixl "|`"  110) where
   "m|`A = (\<lambda>x. if x \<in> A then m x else None)"
 
 notation (latex output)
   restrict_map  ("_\<restriction>\<^bsub>_\<^esub>" [111,110] 110)
 
 definition
   dom :: "('a \<rightharpoonup> 'b) \<Rightarrow> 'a set" where
   "dom m = {a. m a \<noteq> None}"
 
 definition
   ran :: "('a \<rightharpoonup> 'b) \<Rightarrow> 'b set" where
   "ran m = {b. \<exists>a. m a = Some b}"
 
 definition
   map_le :: "('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> bool"  (infix "\<subseteq>\<^sub>m" 50) where
   "(m\<^sub>1 \<subseteq>\<^sub>m m\<^sub>2) \<longleftrightarrow> (\<forall>a \<in> dom m\<^sub>1. m\<^sub>1 a = m\<^sub>2 a)"
 
 nonterminal maplets and maplet
 
 syntax
   "_maplet"  :: "['a, 'a] \<Rightarrow> maplet"             ("_ /\<mapsto>/ _")
   "_maplets" :: "['a, 'a] \<Rightarrow> maplet"             ("_ /[\<mapsto>]/ _")
   ""         :: "maplet \<Rightarrow> maplets"             ("_")
   "_Maplets" :: "[maplet, maplets] \<Rightarrow> maplets" ("_,/ _")
   "_MapUpd"  :: "['a \<rightharpoonup> 'b, maplets] \<Rightarrow> 'a \<rightharpoonup> 'b" ("_/'(_')" [900, 0] 900)
   "_Map"     :: "maplets \<Rightarrow> 'a \<rightharpoonup> 'b"            ("(1[_])")
 
 syntax (ASCII)
   "_maplet"  :: "['a, 'a] \<Rightarrow> maplet"             ("_ /|->/ _")
   "_maplets" :: "['a, 'a] \<Rightarrow> maplet"             ("_ /[|->]/ _")
 
 translations
   "_MapUpd m (_Maplets xy ms)"  \<rightleftharpoons> "_MapUpd (_MapUpd m xy) ms"
   "_MapUpd m (_maplet  x y)"    \<rightleftharpoons> "m(x := CONST Some y)"
   "_Map ms"                     \<rightleftharpoons> "_MapUpd (CONST empty) ms"
   "_Map (_Maplets ms1 ms2)"     \<leftharpoondown> "_MapUpd (_Map ms1) ms2"
   "_Maplets ms1 (_Maplets ms2 ms3)" \<leftharpoondown> "_Maplets (_Maplets ms1 ms2) ms3"
 
 primrec map_of :: "('a \<times> 'b) list \<Rightarrow> 'a \<rightharpoonup> 'b"
 where
   "map_of [] = empty"
 | "map_of (p # ps) = (map_of ps)(fst p \<mapsto> snd p)"
 
 definition map_upds :: "('a \<rightharpoonup> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'a \<rightharpoonup> 'b"
   where "map_upds m xs ys = m ++ map_of (rev (zip xs ys))"
 translations
   "_MapUpd m (_maplets x y)" \<rightleftharpoons> "CONST map_upds m x y"
 
 lemma map_of_Cons_code [code]:
   "map_of [] k = None"
   "map_of ((l, v) # ps) k = (if l = k then Some v else map_of ps k)"
   by simp_all
 
 
 subsection \<open>@{term [source] empty}\<close>
 
 lemma empty_upd_none [simp]: "empty(x := None) = empty"
   by (rule ext) simp
 
 
 subsection \<open>@{term [source] map_upd}\<close>
 
 lemma map_upd_triv: "t k = Some x \<Longrightarrow> t(k\<mapsto>x) = t"
   by (rule ext) simp
 
 lemma map_upd_nonempty [simp]: "t(k\<mapsto>x) \<noteq> empty"
 proof
   assume "t(k \<mapsto> x) = empty"
   then have "(t(k \<mapsto> x)) k = None" by simp
   then show False by simp
 qed
 
 lemma map_upd_eqD1:
   assumes "m(a\<mapsto>x) = n(a\<mapsto>y)"
   shows "x = y"
 proof -
   from assms have "(m(a\<mapsto>x)) a = (n(a\<mapsto>y)) a" by simp
   then show ?thesis by simp
 qed
 
 lemma map_upd_Some_unfold:
   "((m(a\<mapsto>b)) x = Some y) = (x = a \<and> b = y \<or> x \<noteq> a \<and> m x = Some y)"
-by auto
+  by auto
 
 lemma image_map_upd [simp]: "x \<notin> A \<Longrightarrow> m(x \<mapsto> y) ` A = m ` A"
-by auto
+  by auto
 
-lemma finite_range_updI: "finite (range f) \<Longrightarrow> finite (range (f(a\<mapsto>b)))"
-unfolding image_def
-apply (simp (no_asm_use) add:full_SetCompr_eq)
-apply (rule finite_subset)
- prefer 2 apply assumption
-apply (auto)
-done
+lemma finite_range_updI:
+  assumes "finite (range f)" shows "finite (range (f(a\<mapsto>b)))"
+proof -
+  have "range (f(a\<mapsto>b)) \<subseteq> insert (Some b) (range f)"
+    by auto
+  then show ?thesis
+    by (rule finite_subset) (use assms in auto)
+qed
 
 
 subsection \<open>@{term [source] map_of}\<close>
 
 lemma map_of_eq_empty_iff [simp]:
   "map_of xys = empty \<longleftrightarrow> xys = []"
 proof
   show "map_of xys = empty \<Longrightarrow> xys = []"
     by (induction xys) simp_all
 qed simp
 
 lemma empty_eq_map_of_iff [simp]:
   "empty = map_of xys \<longleftrightarrow> xys = []"
 by(subst eq_commute) simp
 
 lemma map_of_eq_None_iff:
   "(map_of xys x = None) = (x \<notin> fst ` (set xys))"
 by (induct xys) simp_all
 
 lemma map_of_eq_Some_iff [simp]:
   "distinct(map fst xys) \<Longrightarrow> (map_of xys x = Some y) = ((x,y) \<in> set xys)"
-apply (induct xys)
- apply simp
-apply (auto simp: map_of_eq_None_iff [symmetric])
-done
+proof (induct xys)
+  case (Cons xy xys)
+  then show ?case
+    by (cases xy) (auto simp flip: map_of_eq_None_iff)
+qed auto
 
 lemma Some_eq_map_of_iff [simp]:
   "distinct(map fst xys) \<Longrightarrow> (Some y = map_of xys x) = ((x,y) \<in> set xys)"
 by (auto simp del: map_of_eq_Some_iff simp: map_of_eq_Some_iff [symmetric])
 
-lemma map_of_is_SomeI [simp]: "\<lbrakk> distinct(map fst xys); (x,y) \<in> set xys \<rbrakk>
-    \<Longrightarrow> map_of xys x = Some y"
-apply (induct xys)
- apply simp
-apply force
-done
+lemma map_of_is_SomeI [simp]: 
+  "\<lbrakk>distinct(map fst xys); (x,y) \<in> set xys\<rbrakk> \<Longrightarrow> map_of xys x = Some y"
+  by simp
 
 lemma map_of_zip_is_None [simp]:
   "length xs = length ys \<Longrightarrow> (map_of (zip xs ys) x = None) = (x \<notin> set xs)"
 by (induct rule: list_induct2) simp_all
 
 lemma map_of_zip_is_Some:
   assumes "length xs = length ys"
   shows "x \<in> set xs \<longleftrightarrow> (\<exists>y. map_of (zip xs ys) x = Some y)"
 using assms by (induct rule: list_induct2) simp_all
 
 lemma map_of_zip_upd:
   fixes x :: 'a and xs :: "'a list" and ys zs :: "'b list"
   assumes "length ys = length xs"
     and "length zs = length xs"
     and "x \<notin> set xs"
     and "map_of (zip xs ys)(x \<mapsto> y) = map_of (zip xs zs)(x \<mapsto> z)"
   shows "map_of (zip xs ys) = map_of (zip xs zs)"
 proof
   fix x' :: 'a
   show "map_of (zip xs ys) x' = map_of (zip xs zs) x'"
   proof (cases "x = x'")
     case True
     from assms True map_of_zip_is_None [of xs ys x']
       have "map_of (zip xs ys) x' = None" by simp
     moreover from assms True map_of_zip_is_None [of xs zs x']
       have "map_of (zip xs zs) x' = None" by simp
     ultimately show ?thesis by simp
   next
     case False from assms
       have "(map_of (zip xs ys)(x \<mapsto> y)) x' = (map_of (zip xs zs)(x \<mapsto> z)) x'" by auto
     with False show ?thesis by simp
   qed
 qed
 
 lemma map_of_zip_inject:
   assumes "length ys = length xs"
     and "length zs = length xs"
     and dist: "distinct xs"
     and map_of: "map_of (zip xs ys) = map_of (zip xs zs)"
   shows "ys = zs"
   using assms(1) assms(2)[symmetric]
   using dist map_of
 proof (induct ys xs zs rule: list_induct3)
   case Nil show ?case by simp
 next
   case (Cons y ys x xs z zs)
   from \<open>map_of (zip (x#xs) (y#ys)) = map_of (zip (x#xs) (z#zs))\<close>
     have map_of: "map_of (zip xs ys)(x \<mapsto> y) = map_of (zip xs zs)(x \<mapsto> z)" by simp
   from Cons have "length ys = length xs" and "length zs = length xs"
     and "x \<notin> set xs" by simp_all
   then have "map_of (zip xs ys) = map_of (zip xs zs)" using map_of by (rule map_of_zip_upd)
   with Cons.hyps \<open>distinct (x # xs)\<close> have "ys = zs" by simp
   moreover from map_of have "y = z" by (rule map_upd_eqD1)
   ultimately show ?case by simp
 qed
 
 lemma map_of_zip_nth:
   assumes "length xs = length ys"
   assumes "distinct xs"
   assumes "i < length ys"
   shows "map_of (zip xs ys) (xs ! i) = Some (ys ! i)"
 using assms proof (induct arbitrary: i rule: list_induct2)
   case Nil
   then show ?case by simp
 next
   case (Cons x xs y ys)
   then show ?case
     using less_Suc_eq_0_disj by auto
 qed
 
 lemma map_of_zip_map:
   "map_of (zip xs (map f xs)) = (\<lambda>x. if x \<in> set xs then Some (f x) else None)"
   by (induct xs) (simp_all add: fun_eq_iff)
 
 lemma finite_range_map_of: "finite (range (map_of xys))"
-apply (induct xys)
- apply (simp_all add: image_constant)
-apply (rule finite_subset)
- prefer 2 apply assumption
-apply auto
-done
+proof (induct xys)
+  case (Cons a xys)
+  then show ?case
+    using finite_range_updI by fastforce
+qed auto
 
 lemma map_of_SomeD: "map_of xs k = Some y \<Longrightarrow> (k, y) \<in> set xs"
   by (induct xs) (auto split: if_splits)
 
 lemma map_of_mapk_SomeI:
   "inj f \<Longrightarrow> map_of t k = Some x \<Longrightarrow>
    map_of (map (case_prod (\<lambda>k. Pair (f k))) t) (f k) = Some x"
 by (induct t) (auto simp: inj_eq)
 
 lemma weak_map_of_SomeI: "(k, x) \<in> set l \<Longrightarrow> \<exists>x. map_of l k = Some x"
 by (induct l) auto
 
 lemma map_of_filter_in:
   "map_of xs k = Some z \<Longrightarrow> P k z \<Longrightarrow> map_of (filter (case_prod P) xs) k = Some z"
 by (induct xs) auto
 
 lemma map_of_map:
   "map_of (map (\<lambda>(k, v). (k, f v)) xs) = map_option f \<circ> map_of xs"
   by (induct xs) (auto simp: fun_eq_iff)
 
 lemma dom_map_option:
   "dom (\<lambda>k. map_option (f k) (m k)) = dom m"
   by (simp add: dom_def)
 
 lemma dom_map_option_comp [simp]:
   "dom (map_option g \<circ> m) = dom m"
   using dom_map_option [of "\<lambda>_. g" m] by (simp add: comp_def)
 
 
 subsection \<open>\<^const>\<open>map_option\<close> related\<close>
 
 lemma map_option_o_empty [simp]: "map_option f \<circ> empty = empty"
 by (rule ext) simp
 
 lemma map_option_o_map_upd [simp]:
   "map_option f \<circ> m(a\<mapsto>b) = (map_option f \<circ> m)(a\<mapsto>f b)"
 by (rule ext) simp
 
 
 subsection \<open>@{term [source] map_comp} related\<close>
 
 lemma map_comp_empty [simp]:
   "m \<circ>\<^sub>m empty = empty"
   "empty \<circ>\<^sub>m m = empty"
 by (auto simp: map_comp_def split: option.splits)
 
 lemma map_comp_simps [simp]:
   "m2 k = None \<Longrightarrow> (m1 \<circ>\<^sub>m m2) k = None"
   "m2 k = Some k' \<Longrightarrow> (m1 \<circ>\<^sub>m m2) k = m1 k'"
 by (auto simp: map_comp_def)
 
 lemma map_comp_Some_iff:
   "((m1 \<circ>\<^sub>m m2) k = Some v) = (\<exists>k'. m2 k = Some k' \<and> m1 k' = Some v)"
 by (auto simp: map_comp_def split: option.splits)
 
 lemma map_comp_None_iff:
   "((m1 \<circ>\<^sub>m m2) k = None) = (m2 k = None \<or> (\<exists>k'. m2 k = Some k' \<and> m1 k' = None)) "
 by (auto simp: map_comp_def split: option.splits)
 
 
 subsection \<open>\<open>++\<close>\<close>
 
 lemma map_add_empty[simp]: "m ++ empty = m"
 by(simp add: map_add_def)
 
 lemma empty_map_add[simp]: "empty ++ m = m"
 by (rule ext) (simp add: map_add_def split: option.split)
 
 lemma map_add_assoc[simp]: "m1 ++ (m2 ++ m3) = (m1 ++ m2) ++ m3"
 by (rule ext) (simp add: map_add_def split: option.split)
 
 lemma map_add_Some_iff:
   "((m ++ n) k = Some x) = (n k = Some x \<or> n k = None \<and> m k = Some x)"
 by (simp add: map_add_def split: option.split)
 
 lemma map_add_SomeD [dest!]:
   "(m ++ n) k = Some x \<Longrightarrow> n k = Some x \<or> n k = None \<and> m k = Some x"
 by (rule map_add_Some_iff [THEN iffD1])
 
 lemma map_add_find_right [simp]: "n k = Some xx \<Longrightarrow> (m ++ n) k = Some xx"
 by (subst map_add_Some_iff) fast
 
 lemma map_add_None [iff]: "((m ++ n) k = None) = (n k = None \<and> m k = None)"
 by (simp add: map_add_def split: option.split)
 
 lemma map_add_upd[simp]: "f ++ g(x\<mapsto>y) = (f ++ g)(x\<mapsto>y)"
 by (rule ext) (simp add: map_add_def)
 
 lemma map_add_upds[simp]: "m1 ++ (m2(xs[\<mapsto>]ys)) = (m1++m2)(xs[\<mapsto>]ys)"
 by (simp add: map_upds_def)
 
 lemma map_add_upd_left: "m\<notin>dom e2 \<Longrightarrow> e1(m \<mapsto> u1) ++ e2 = (e1 ++ e2)(m \<mapsto> u1)"
 by (rule ext) (auto simp: map_add_def dom_def split: option.split)
 
 lemma map_of_append[simp]: "map_of (xs @ ys) = map_of ys ++ map_of xs"
-unfolding map_add_def
-apply (induct xs)
- apply simp
-apply (rule ext)
-apply (simp split: option.split)
-done
+  unfolding map_add_def
+proof (induct xs)
+  case (Cons a xs)
+  then show ?case
+    by (force split: option.split)
+qed auto
 
 lemma finite_range_map_of_map_add:
   "finite (range f) \<Longrightarrow> finite (range (f ++ map_of l))"
-apply (induct l)
- apply (auto simp del: fun_upd_apply)
-apply (erule finite_range_updI)
-done
+proof (induct l)
+case (Cons a l)
+  then show ?case
+    by (metis finite_range_updI map_add_upd map_of.simps(2))
+qed auto
 
 lemma inj_on_map_add_dom [iff]:
   "inj_on (m ++ m') (dom m') = inj_on m' (dom m')"
-by (fastforce simp: map_add_def dom_def inj_on_def split: option.splits)
+  by (fastforce simp: map_add_def dom_def inj_on_def split: option.splits)
 
 lemma map_upds_fold_map_upd:
   "m(ks[\<mapsto>]vs) = foldl (\<lambda>m (k, v). m(k \<mapsto> v)) m (zip ks vs)"
 unfolding map_upds_def proof (rule sym, rule zip_obtain_same_length)
   fix ks :: "'a list" and vs :: "'b list"
   assume "length ks = length vs"
   then show "foldl (\<lambda>m (k, v). m(k\<mapsto>v)) m (zip ks vs) = m ++ map_of (rev (zip ks vs))"
     by(induct arbitrary: m rule: list_induct2) simp_all
 qed
 
 lemma map_add_map_of_foldr:
   "m ++ map_of ps = foldr (\<lambda>(k, v) m. m(k \<mapsto> v)) ps m"
   by (induct ps) (auto simp: fun_eq_iff map_add_def)
 
 
 subsection \<open>@{term [source] restrict_map}\<close>
 
 lemma restrict_map_to_empty [simp]: "m|`{} = empty"
-by (simp add: restrict_map_def)
+  by (simp add: restrict_map_def)
 
 lemma restrict_map_insert: "f |` (insert a A) = (f |` A)(a := f a)"
-by (auto simp: restrict_map_def)
+  by (auto simp: restrict_map_def)
 
 lemma restrict_map_empty [simp]: "empty|`D = empty"
-by (simp add: restrict_map_def)
+  by (simp add: restrict_map_def)
 
 lemma restrict_in [simp]: "x \<in> A \<Longrightarrow> (m|`A) x = m x"
-by (simp add: restrict_map_def)
+  by (simp add: restrict_map_def)
 
 lemma restrict_out [simp]: "x \<notin> A \<Longrightarrow> (m|`A) x = None"
-by (simp add: restrict_map_def)
+  by (simp add: restrict_map_def)
 
 lemma ran_restrictD: "y \<in> ran (m|`A) \<Longrightarrow> \<exists>x\<in>A. m x = Some y"
-by (auto simp: restrict_map_def ran_def split: if_split_asm)
+  by (auto simp: restrict_map_def ran_def split: if_split_asm)
 
 lemma dom_restrict [simp]: "dom (m|`A) = dom m \<inter> A"
-by (auto simp: restrict_map_def dom_def split: if_split_asm)
+  by (auto simp: restrict_map_def dom_def split: if_split_asm)
 
 lemma restrict_upd_same [simp]: "m(x\<mapsto>y)|`(-{x}) = m|`(-{x})"
-by (rule ext) (auto simp: restrict_map_def)
+  by (rule ext) (auto simp: restrict_map_def)
 
 lemma restrict_restrict [simp]: "m|`A|`B = m|`(A\<inter>B)"
-by (rule ext) (auto simp: restrict_map_def)
+  by (rule ext) (auto simp: restrict_map_def)
 
 lemma restrict_fun_upd [simp]:
   "m(x := y)|`D = (if x \<in> D then (m|`(D-{x}))(x := y) else m|`D)"
-by (simp add: restrict_map_def fun_eq_iff)
+  by (simp add: restrict_map_def fun_eq_iff)
 
 lemma fun_upd_None_restrict [simp]:
   "(m|`D)(x := None) = (if x \<in> D then m|`(D - {x}) else m|`D)"
-by (simp add: restrict_map_def fun_eq_iff)
+  by (simp add: restrict_map_def fun_eq_iff)
 
 lemma fun_upd_restrict: "(m|`D)(x := y) = (m|`(D-{x}))(x := y)"
-by (simp add: restrict_map_def fun_eq_iff)
+  by (simp add: restrict_map_def fun_eq_iff)
 
 lemma fun_upd_restrict_conv [simp]:
   "x \<in> D \<Longrightarrow> (m|`D)(x := y) = (m|`(D-{x}))(x := y)"
-by (simp add: restrict_map_def fun_eq_iff)
+  by (rule fun_upd_restrict)
 
 lemma map_of_map_restrict:
   "map_of (map (\<lambda>k. (k, f k)) ks) = (Some \<circ> f) |` set ks"
   by (induct ks) (simp_all add: fun_eq_iff restrict_map_insert)
 
 lemma restrict_complement_singleton_eq:
   "f |` (- {x}) = f(x := None)"
-  by (simp add: restrict_map_def fun_eq_iff)
+  by auto
 
 
 subsection \<open>@{term [source] map_upds}\<close>
 
 lemma map_upds_Nil1 [simp]: "m([] [\<mapsto>] bs) = m"
-by (simp add: map_upds_def)
+  by (simp add: map_upds_def)
 
 lemma map_upds_Nil2 [simp]: "m(as [\<mapsto>] []) = m"
-by (simp add:map_upds_def)
+  by (simp add:map_upds_def)
 
 lemma map_upds_Cons [simp]: "m(a#as [\<mapsto>] b#bs) = (m(a\<mapsto>b))(as[\<mapsto>]bs)"
-by (simp add:map_upds_def)
+  by (simp add:map_upds_def)
 
-lemma map_upds_append1 [simp]: "size xs < size ys \<Longrightarrow>
-  m(xs@[x] [\<mapsto>] ys) = m(xs [\<mapsto>] ys)(x \<mapsto> ys!size xs)"
-apply(induct xs arbitrary: ys m)
- apply (clarsimp simp add: neq_Nil_conv)
-apply (case_tac ys)
- apply simp
-apply simp
-done
+lemma map_upds_append1 [simp]:
+  "size xs < size ys \<Longrightarrow> m(xs@[x] [\<mapsto>] ys) = m(xs [\<mapsto>] ys)(x \<mapsto> ys!size xs)"
+proof (induct xs arbitrary: ys m)
+  case Nil
+  then show ?case
+    by (auto simp: neq_Nil_conv)
+next
+  case (Cons a xs)
+  then show ?case
+    by (cases ys) auto
+qed
 
 lemma map_upds_list_update2_drop [simp]:
   "size xs \<le> i \<Longrightarrow> m(xs[\<mapsto>]ys[i:=y]) = m(xs[\<mapsto>]ys)"
-apply (induct xs arbitrary: m ys i)
- apply simp
-apply (case_tac ys)
- apply simp
-apply (simp split: nat.split)
-done
+proof (induct xs arbitrary: m ys i)
+  case Nil
+  then show ?case
+    by auto
+next
+  case (Cons a xs)
+  then show ?case
+    by (cases ys) (use Cons in \<open>auto split: nat.split\<close>)
+qed
 
+text \<open>Something weirdly sensitive about this proof, which needs only four lines in apply style\<close>
 lemma map_upd_upds_conv_if:
   "(f(x\<mapsto>y))(xs [\<mapsto>] ys) =
    (if x \<in> set(take (length ys) xs) then f(xs [\<mapsto>] ys)
                                     else (f(xs [\<mapsto>] ys))(x\<mapsto>y))"
-apply (induct xs arbitrary: x y ys f)
- apply simp
-apply (case_tac ys)
- apply (auto split: if_split simp: fun_upd_twist)
-done
+proof (induct xs arbitrary: x y ys f)
+  case (Cons a xs)
+  show ?case
+  proof (cases ys)
+    case (Cons z zs)
+    then show ?thesis
+      using Cons.hyps
+      apply (auto split: if_split simp: fun_upd_twist)
+      using Cons.hyps apply fastforce+
+      done
+  qed auto
+qed auto
+
 
 lemma map_upds_twist [simp]:
   "a \<notin> set as \<Longrightarrow> m(a\<mapsto>b)(as[\<mapsto>]bs) = m(as[\<mapsto>]bs)(a\<mapsto>b)"
 using set_take_subset by (fastforce simp add: map_upd_upds_conv_if)
 
 lemma map_upds_apply_nontin [simp]:
   "x \<notin> set xs \<Longrightarrow> (f(xs[\<mapsto>]ys)) x = f x"
-apply (induct xs arbitrary: ys)
- apply simp
-apply (case_tac ys)
- apply (auto simp: map_upd_upds_conv_if)
-done
+proof (induct xs arbitrary: ys)
+  case (Cons a xs)
+  then show ?case
+    by (cases ys) (auto simp: map_upd_upds_conv_if)
+qed auto
 
 lemma fun_upds_append_drop [simp]:
   "size xs = size ys \<Longrightarrow> m(xs@zs[\<mapsto>]ys) = m(xs[\<mapsto>]ys)"
-apply (induct xs arbitrary: m ys)
- apply simp
-apply (case_tac ys)
- apply simp_all
-done
+proof (induct xs arbitrary: ys)
+  case (Cons a xs)
+  then show ?case
+    by (cases ys) (auto simp: map_upd_upds_conv_if)
+qed auto
 
 lemma fun_upds_append2_drop [simp]:
   "size xs = size ys \<Longrightarrow> m(xs[\<mapsto>]ys@zs) = m(xs[\<mapsto>]ys)"
-apply (induct xs arbitrary: m ys)
- apply simp
-apply (case_tac ys)
- apply simp_all
-done
-
+proof (induct xs arbitrary: ys)
+  case (Cons a xs)
+  then show ?case
+    by (cases ys) (auto simp: map_upd_upds_conv_if)
+qed auto
 
 lemma restrict_map_upds[simp]:
   "\<lbrakk> length xs = length ys; set xs \<subseteq> D \<rbrakk>
     \<Longrightarrow> m(xs [\<mapsto>] ys)|`D = (m|`(D - set xs))(xs [\<mapsto>] ys)"
-apply (induct xs arbitrary: m ys)
- apply simp
-apply (case_tac ys)
- apply simp
-apply (simp add: Diff_insert [symmetric] insert_absorb)
-apply (simp add: map_upd_upds_conv_if)
-done
+proof (induct xs arbitrary: m ys)
+  case (Cons a xs)
+  then show ?case
+  proof (cases ys)
+    case (Cons z zs)
+    with Cons.hyps Cons.prems show ?thesis
+      apply (simp add: insert_absorb flip: Diff_insert)
+      apply (auto simp add: map_upd_upds_conv_if)
+      done
+  qed auto
+qed auto
 
 
 subsection \<open>@{term [source] dom}\<close>
 
 lemma dom_eq_empty_conv [simp]: "dom f = {} \<longleftrightarrow> f = empty"
   by (auto simp: dom_def)
 
 lemma domI: "m a = Some b \<Longrightarrow> a \<in> dom m"
   by (simp add: dom_def)
 (* declare domI [intro]? *)
 
 lemma domD: "a \<in> dom m \<Longrightarrow> \<exists>b. m a = Some b"
   by (cases "m a") (auto simp add: dom_def)
 
 lemma domIff [iff, simp del, code_unfold]: "a \<in> dom m \<longleftrightarrow> m a \<noteq> None"
   by (simp add: dom_def)
 
 lemma dom_empty [simp]: "dom empty = {}"
   by (simp add: dom_def)
 
 lemma dom_fun_upd [simp]:
   "dom(f(x := y)) = (if y = None then dom f - {x} else insert x (dom f))"
   by (auto simp: dom_def)
 
 lemma dom_if:
   "dom (\<lambda>x. if P x then f x else g x) = dom f \<inter> {x. P x} \<union> dom g \<inter> {x. \<not> P x}"
   by (auto split: if_splits)
 
 lemma dom_map_of_conv_image_fst:
   "dom (map_of xys) = fst ` set xys"
   by (induct xys) (auto simp add: dom_if)
 
 lemma dom_map_of_zip [simp]: "length xs = length ys \<Longrightarrow> dom (map_of (zip xs ys)) = set xs"
   by (induct rule: list_induct2) (auto simp: dom_if)
 
 lemma finite_dom_map_of: "finite (dom (map_of l))"
   by (induct l) (auto simp: dom_def insert_Collect [symmetric])
 
 lemma dom_map_upds [simp]:
   "dom(m(xs[\<mapsto>]ys)) = set(take (length ys) xs) \<union> dom m"
-apply (induct xs arbitrary: m ys)
- apply simp
-apply (case_tac ys)
- apply auto
-done
+proof (induct xs arbitrary: ys)
+  case (Cons a xs)
+  then show ?case
+    by (cases ys) (auto simp: map_upd_upds_conv_if)
+qed auto
+
 
 lemma dom_map_add [simp]: "dom (m ++ n) = dom n \<union> dom m"
   by (auto simp: dom_def)
 
 lemma dom_override_on [simp]:
   "dom (override_on f g A) =
     (dom f  - {a. a \<in> A - dom g}) \<union> {a. a \<in> A \<inter> dom g}"
   by (auto simp: dom_def override_on_def)
 
 lemma map_add_comm: "dom m1 \<inter> dom m2 = {} \<Longrightarrow> m1 ++ m2 = m2 ++ m1"
   by (rule ext) (force simp: map_add_def dom_def split: option.split)
 
 lemma map_add_dom_app_simps:
   "m \<in> dom l2 \<Longrightarrow> (l1 ++ l2) m = l2 m"
   "m \<notin> dom l1 \<Longrightarrow> (l1 ++ l2) m = l2 m"
   "m \<notin> dom l2 \<Longrightarrow> (l1 ++ l2) m = l1 m"
   by (auto simp add: map_add_def split: option.split_asm)
 
 lemma dom_const [simp]:
   "dom (\<lambda>x. Some (f x)) = UNIV"
   by auto
 
 (* Due to John Matthews - could be rephrased with dom *)
 lemma finite_map_freshness:
   "finite (dom (f :: 'a \<rightharpoonup> 'b)) \<Longrightarrow> \<not> finite (UNIV :: 'a set) \<Longrightarrow>
    \<exists>x. f x = None"
   by (bestsimp dest: ex_new_if_finite)
 
 lemma dom_minus:
   "f x = None \<Longrightarrow> dom f - insert x A = dom f - A"
   unfolding dom_def by simp
 
 lemma insert_dom:
   "f x = Some y \<Longrightarrow> insert x (dom f) = dom f"
   unfolding dom_def by auto
 
 lemma map_of_map_keys:
   "set xs = dom m \<Longrightarrow> map_of (map (\<lambda>k. (k, the (m k))) xs) = m"
   by (rule ext) (auto simp add: map_of_map_restrict restrict_map_def)
 
 lemma map_of_eqI:
   assumes set_eq: "set (map fst xs) = set (map fst ys)"
   assumes map_eq: "\<forall>k\<in>set (map fst xs). map_of xs k = map_of ys k"
   shows "map_of xs = map_of ys"
 proof (rule ext)
   fix k show "map_of xs k = map_of ys k"
   proof (cases "map_of xs k")
     case None
     then have "k \<notin> set (map fst xs)" by (simp add: map_of_eq_None_iff)
     with set_eq have "k \<notin> set (map fst ys)" by simp
     then have "map_of ys k = None" by (simp add: map_of_eq_None_iff)
     with None show ?thesis by simp
   next
     case (Some v)
     then have "k \<in> set (map fst xs)" by (auto simp add: dom_map_of_conv_image_fst [symmetric])
     with map_eq show ?thesis by auto
   qed
 qed
 
 lemma map_of_eq_dom:
   assumes "map_of xs = map_of ys"
   shows "fst ` set xs = fst ` set ys"
 proof -
   from assms have "dom (map_of xs) = dom (map_of ys)" by simp
   then show ?thesis by (simp add: dom_map_of_conv_image_fst)
 qed
 
 lemma finite_set_of_finite_maps:
   assumes "finite A" "finite B"
   shows "finite {m. dom m = A \<and> ran m \<subseteq> B}" (is "finite ?S")
 proof -
   let ?S' = "{m. \<forall>x. (x \<in> A \<longrightarrow> m x \<in> Some ` B) \<and> (x \<notin> A \<longrightarrow> m x = None)}"
   have "?S = ?S'"
   proof
     show "?S \<subseteq> ?S'" by (auto simp: dom_def ran_def image_def)
     show "?S' \<subseteq> ?S"
     proof
       fix m assume "m \<in> ?S'"
       hence 1: "dom m = A" by force
       hence 2: "ran m \<subseteq> B" using \<open>m \<in> ?S'\<close> by (auto simp: dom_def ran_def)
       from 1 2 show "m \<in> ?S" by blast
     qed
   qed
   with assms show ?thesis by(simp add: finite_set_of_finite_funs)
 qed
 
 
 subsection \<open>@{term [source] ran}\<close>
 
 lemma ranI: "m a = Some b \<Longrightarrow> b \<in> ran m"
   by (auto simp: ran_def)
 (* declare ranI [intro]? *)
 
 lemma ran_empty [simp]: "ran empty = {}"
   by (auto simp: ran_def)
 
-lemma ran_map_upd [simp]: "m a = None \<Longrightarrow> ran(m(a\<mapsto>b)) = insert b (ran m)"
+lemma ran_map_upd [simp]:  "m a = None \<Longrightarrow> ran(m(a\<mapsto>b)) = insert b (ran m)"
   unfolding ran_def
-apply auto
-apply (subgoal_tac "aa \<noteq> a")
- apply auto
-done
+  by force
 
 lemma ran_map_add:
   assumes "dom m1 \<inter> dom m2 = {}"
   shows "ran (m1 ++ m2) = ran m1 \<union> ran m2"
 proof
   show "ran (m1 ++ m2) \<subseteq> ran m1 \<union> ran m2"
     unfolding ran_def by auto
 next
   show "ran m1 \<union> ran m2 \<subseteq> ran (m1 ++ m2)"
   proof -
     have "(m1 ++ m2) x = Some y" if "m1 x = Some y" for x y
       using assms map_add_comm that by fastforce
     moreover have "(m1 ++ m2) x = Some y" if "m2 x = Some y" for x y
       using assms that by auto
     ultimately show ?thesis
       unfolding ran_def by blast
   qed
 qed
 
 lemma finite_ran:
   assumes "finite (dom p)"
   shows "finite (ran p)"
 proof -
   have "ran p = (\<lambda>x. the (p x)) ` dom p"
     unfolding ran_def by force
   from this \<open>finite (dom p)\<close> show ?thesis by auto
 qed
 
 lemma ran_distinct:
   assumes dist: "distinct (map fst al)"
   shows "ran (map_of al) = snd ` set al"
   using assms
 proof (induct al)
   case Nil
   then show ?case by simp
 next
   case (Cons kv al)
   then have "ran (map_of al) = snd ` set al" by simp
   moreover from Cons.prems have "map_of al (fst kv) = None"
     by (simp add: map_of_eq_None_iff)
   ultimately show ?case by (simp only: map_of.simps ran_map_upd) simp
 qed
 
 lemma ran_map_of_zip:
   assumes "length xs = length ys" "distinct xs"
   shows "ran (map_of (zip xs ys)) = set ys"
 using assms by (simp add: ran_distinct set_map[symmetric])
 
 lemma ran_map_option: "ran (\<lambda>x. map_option f (m x)) = f ` ran m"
   by (auto simp add: ran_def)
 
 
 subsection \<open>\<open>map_le\<close>\<close>
 
 lemma map_le_empty [simp]: "empty \<subseteq>\<^sub>m g"
   by (simp add: map_le_def)
 
 lemma upd_None_map_le [simp]: "f(x := None) \<subseteq>\<^sub>m f"
   by (force simp add: map_le_def)
 
 lemma map_le_upd[simp]: "f \<subseteq>\<^sub>m g ==> f(a := b) \<subseteq>\<^sub>m g(a := b)"
   by (fastforce simp add: map_le_def)
 
 lemma map_le_imp_upd_le [simp]: "m1 \<subseteq>\<^sub>m m2 \<Longrightarrow> m1(x := None) \<subseteq>\<^sub>m m2(x \<mapsto> y)"
   by (force simp add: map_le_def)
 
 lemma map_le_upds [simp]:
   "f \<subseteq>\<^sub>m g \<Longrightarrow> f(as [\<mapsto>] bs) \<subseteq>\<^sub>m g(as [\<mapsto>] bs)"
-apply (induct as arbitrary: f g bs)
- apply simp
-apply (case_tac bs)
- apply auto
-done
+proof (induct as arbitrary: f g bs)
+  case (Cons a as)
+  then show ?case
+    by (cases bs) (use Cons in auto)
+qed auto
 
 lemma map_le_implies_dom_le: "(f \<subseteq>\<^sub>m g) \<Longrightarrow> (dom f \<subseteq> dom g)"
   by (fastforce simp add: map_le_def dom_def)
 
 lemma map_le_refl [simp]: "f \<subseteq>\<^sub>m f"
   by (simp add: map_le_def)
 
 lemma map_le_trans[trans]: "\<lbrakk> m1 \<subseteq>\<^sub>m m2; m2 \<subseteq>\<^sub>m m3\<rbrakk> \<Longrightarrow> m1 \<subseteq>\<^sub>m m3"
   by (auto simp add: map_le_def dom_def)
 
 lemma map_le_antisym: "\<lbrakk> f \<subseteq>\<^sub>m g; g \<subseteq>\<^sub>m f \<rbrakk> \<Longrightarrow> f = g"
-unfolding map_le_def
-apply (rule ext)
-apply (case_tac "x \<in> dom f", simp)
-apply (case_tac "x \<in> dom g", simp, fastforce)
-done
+  unfolding map_le_def
+  by (metis ext domIff)
 
 lemma map_le_map_add [simp]: "f \<subseteq>\<^sub>m g ++ f"
   by (fastforce simp: map_le_def)
 
 lemma map_le_iff_map_add_commute: "f \<subseteq>\<^sub>m f ++ g \<longleftrightarrow> f ++ g = g ++ f"
   by (fastforce simp: map_add_def map_le_def fun_eq_iff split: option.splits)
 
 lemma map_add_le_mapE: "f ++ g \<subseteq>\<^sub>m h \<Longrightarrow> g \<subseteq>\<^sub>m h"
   by (fastforce simp: map_le_def map_add_def dom_def)
 
 lemma map_add_le_mapI: "\<lbrakk> f \<subseteq>\<^sub>m h; g \<subseteq>\<^sub>m h \<rbrakk> \<Longrightarrow> f ++ g \<subseteq>\<^sub>m h"
   by (auto simp: map_le_def map_add_def dom_def split: option.splits)
 
 lemma map_add_subsumed1: "f \<subseteq>\<^sub>m g \<Longrightarrow> f++g = g"
 by (simp add: map_add_le_mapI map_le_antisym)
 
 lemma map_add_subsumed2: "f \<subseteq>\<^sub>m g \<Longrightarrow> g++f = g"
 by (metis map_add_subsumed1 map_le_iff_map_add_commute)
 
 lemma dom_eq_singleton_conv: "dom f = {x} \<longleftrightarrow> (\<exists>v. f = [x \<mapsto> v])"
   (is "?lhs \<longleftrightarrow> ?rhs")
 proof
   assume ?rhs
   then show ?lhs by (auto split: if_split_asm)
 next
   assume ?lhs
   then obtain v where v: "f x = Some v" by auto
   show ?rhs
   proof
     show "f = [x \<mapsto> v]"
     proof (rule map_le_antisym)
       show "[x \<mapsto> v] \<subseteq>\<^sub>m f"
         using v by (auto simp add: map_le_def)
       show "f \<subseteq>\<^sub>m [x \<mapsto> v]"
         using \<open>dom f = {x}\<close> \<open>f x = Some v\<close> by (auto simp add: map_le_def)
     qed
   qed
 qed
 
 lemma map_add_eq_empty_iff[simp]:
   "(f++g = empty) \<longleftrightarrow> f = empty \<and> g = empty"
 by (metis map_add_None)
 
 lemma empty_eq_map_add_iff[simp]:
   "(empty = f++g) \<longleftrightarrow> f = empty \<and> g = empty"
 by(subst map_add_eq_empty_iff[symmetric])(rule eq_commute)
 
 
 subsection \<open>Various\<close>
 
 lemma set_map_of_compr:
   assumes distinct: "distinct (map fst xs)"
   shows "set xs = {(k, v). map_of xs k = Some v}"
   using assms
 proof (induct xs)
   case Nil
   then show ?case by simp
 next
   case (Cons x xs)
   obtain k v where "x = (k, v)" by (cases x) blast
   with Cons.prems have "k \<notin> dom (map_of xs)"
     by (simp add: dom_map_of_conv_image_fst)
   then have *: "insert (k, v) {(k, v). map_of xs k = Some v} =
     {(k', v'). (map_of xs(k \<mapsto> v)) k' = Some v'}"
     by (auto split: if_splits)
   from Cons have "set xs = {(k, v). map_of xs k = Some v}" by simp
   with * \<open>x = (k, v)\<close> show ?case by simp
 qed
 
 lemma eq_key_imp_eq_value:
   "v1 = v2"
   if "distinct (map fst xs)" "(k, v1) \<in> set xs" "(k, v2) \<in> set xs"
 proof -
   from that have "inj_on fst (set xs)"
     by (simp add: distinct_map)
   moreover have "fst (k, v1) = fst (k, v2)"
     by simp
   ultimately have "(k, v1) = (k, v2)"
     by (rule inj_onD) (fact that)+
   then show ?thesis
     by simp
 qed
 
 lemma map_of_inject_set:
   assumes distinct: "distinct (map fst xs)" "distinct (map fst ys)"
   shows "map_of xs = map_of ys \<longleftrightarrow> set xs = set ys" (is "?lhs \<longleftrightarrow> ?rhs")
 proof
   assume ?lhs
   moreover from \<open>distinct (map fst xs)\<close> have "set xs = {(k, v). map_of xs k = Some v}"
     by (rule set_map_of_compr)
   moreover from \<open>distinct (map fst ys)\<close> have "set ys = {(k, v). map_of ys k = Some v}"
     by (rule set_map_of_compr)
   ultimately show ?rhs by simp
 next
   assume ?rhs show ?lhs
   proof
     fix k
     show "map_of xs k = map_of ys k"
     proof (cases "map_of xs k")
       case None
       with \<open>?rhs\<close> have "map_of ys k = None"
         by (simp add: map_of_eq_None_iff)
       with None show ?thesis by simp
     next
       case (Some v)
       with distinct \<open>?rhs\<close> have "map_of ys k = Some v"
         by simp
       with Some show ?thesis by simp
     qed
   qed
 qed
 
 hide_const (open) Map.empty
 
 end