misc tuning and modernization;
authorwenzelm
Fri Aug 05 18:14:28 2016 +0200 (2016-08-05)
changeset 636127195acc2fe93
parent 63611 fb63942e470e
child 63613 1555dc12cfb6
misc tuning and modernization;
src/HOL/Complete_Partial_Order.thy
src/HOL/Finite_Set.thy
src/HOL/Hilbert_Choice.thy
src/HOL/Relation.thy
src/HOL/Transitive_Closure.thy
src/HOL/Wellfounded.thy
     1.1 --- a/src/HOL/Complete_Partial_Order.thy	Fri Aug 05 16:36:03 2016 +0200
     1.2 +++ b/src/HOL/Complete_Partial_Order.thy	Fri Aug 05 18:14:28 2016 +0200
     1.3 @@ -1,12 +1,12 @@
     1.4 -(* Title:    HOL/Complete_Partial_Order.thy
     1.5 -   Author:   Brian Huffman, Portland State University
     1.6 -   Author:   Alexander Krauss, TU Muenchen
     1.7 +(*  Title:      HOL/Complete_Partial_Order.thy
     1.8 +    Author:     Brian Huffman, Portland State University
     1.9 +    Author:     Alexander Krauss, TU Muenchen
    1.10  *)
    1.11  
    1.12  section \<open>Chain-complete partial orders and their fixpoints\<close>
    1.13  
    1.14  theory Complete_Partial_Order
    1.15 -imports Product_Type
    1.16 +  imports Product_Type
    1.17  begin
    1.18  
    1.19  subsection \<open>Monotone functions\<close>
    1.20 @@ -14,131 +14,139 @@
    1.21  text \<open>Dictionary-passing version of @{const Orderings.mono}.\<close>
    1.22  
    1.23  definition monotone :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
    1.24 -where "monotone orda ordb f \<longleftrightarrow> (\<forall>x y. orda x y \<longrightarrow> ordb (f x) (f y))"
    1.25 +  where "monotone orda ordb f \<longleftrightarrow> (\<forall>x y. orda x y \<longrightarrow> ordb (f x) (f y))"
    1.26  
    1.27 -lemma monotoneI[intro?]: "(\<And>x y. orda x y \<Longrightarrow> ordb (f x) (f y))
    1.28 - \<Longrightarrow> monotone orda ordb f"
    1.29 -unfolding monotone_def by iprover
    1.30 +lemma monotoneI[intro?]: "(\<And>x y. orda x y \<Longrightarrow> ordb (f x) (f y)) \<Longrightarrow> monotone orda ordb f"
    1.31 +  unfolding monotone_def by iprover
    1.32  
    1.33  lemma monotoneD[dest?]: "monotone orda ordb f \<Longrightarrow> orda x y \<Longrightarrow> ordb (f x) (f y)"
    1.34 -unfolding monotone_def by iprover
    1.35 +  unfolding monotone_def by iprover
    1.36  
    1.37  
    1.38  subsection \<open>Chains\<close>
    1.39  
    1.40 -text \<open>A chain is a totally-ordered set. Chains are parameterized over
    1.41 +text \<open>
    1.42 +  A chain is a totally-ordered set. Chains are parameterized over
    1.43    the order for maximal flexibility, since type classes are not enough.
    1.44  \<close>
    1.45  
    1.46 -definition
    1.47 -  chain :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool"
    1.48 -where
    1.49 -  "chain ord S \<longleftrightarrow> (\<forall>x\<in>S. \<forall>y\<in>S. ord x y \<or> ord y x)"
    1.50 +definition chain :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool"
    1.51 +  where "chain ord S \<longleftrightarrow> (\<forall>x\<in>S. \<forall>y\<in>S. ord x y \<or> ord y x)"
    1.52  
    1.53  lemma chainI:
    1.54    assumes "\<And>x y. x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> ord x y \<or> ord y x"
    1.55    shows "chain ord S"
    1.56 -using assms unfolding chain_def by fast
    1.57 +  using assms unfolding chain_def by fast
    1.58  
    1.59  lemma chainD:
    1.60    assumes "chain ord S" and "x \<in> S" and "y \<in> S"
    1.61    shows "ord x y \<or> ord y x"
    1.62 -using assms unfolding chain_def by fast
    1.63 +  using assms unfolding chain_def by fast
    1.64  
    1.65  lemma chainE:
    1.66    assumes "chain ord S" and "x \<in> S" and "y \<in> S"
    1.67    obtains "ord x y" | "ord y x"
    1.68 -using assms unfolding chain_def by fast
    1.69 +  using assms unfolding chain_def by fast
    1.70  
    1.71  lemma chain_empty: "chain ord {}"
    1.72 -by(simp add: chain_def)
    1.73 +  by (simp add: chain_def)
    1.74  
    1.75  lemma chain_equality: "chain op = A \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>A. x = y)"
    1.76 -by(auto simp add: chain_def)
    1.77 +  by (auto simp add: chain_def)
    1.78 +
    1.79 +lemma chain_subset: "chain ord A \<Longrightarrow> B \<subseteq> A \<Longrightarrow> chain ord B"
    1.80 +  by (rule chainI) (blast dest: chainD)
    1.81  
    1.82 -lemma chain_subset:
    1.83 -  "\<lbrakk> chain ord A; B \<subseteq> A \<rbrakk>
    1.84 -  \<Longrightarrow> chain ord B"
    1.85 -by(rule chainI)(blast dest: chainD)
    1.86 +lemma chain_imageI:
    1.87 +  assumes chain: "chain le_a Y"
    1.88 +    and mono: "\<And>x y. x \<in> Y \<Longrightarrow> y \<in> Y \<Longrightarrow> le_a x y \<Longrightarrow> le_b (f x) (f y)"
    1.89 +  shows "chain le_b (f ` Y)"
    1.90 +  by (blast intro: chainI dest: chainD[OF chain] mono)
    1.91  
    1.92 -lemma chain_imageI: 
    1.93 -  assumes chain: "chain le_a Y"
    1.94 -  and mono: "\<And>x y. \<lbrakk> x \<in> Y; y \<in> Y; le_a x y \<rbrakk> \<Longrightarrow> le_b (f x) (f y)"
    1.95 -  shows "chain le_b (f ` Y)"
    1.96 -by(blast intro: chainI dest: chainD[OF chain] mono)
    1.97  
    1.98  subsection \<open>Chain-complete partial orders\<close>
    1.99  
   1.100  text \<open>
   1.101 -  A ccpo has a least upper bound for any chain.  In particular, the
   1.102 -  empty set is a chain, so every ccpo must have a bottom element.
   1.103 +  A \<open>ccpo\<close> has a least upper bound for any chain.  In particular, the
   1.104 +  empty set is a chain, so every \<open>ccpo\<close> must have a bottom element.
   1.105  \<close>
   1.106  
   1.107  class ccpo = order + Sup +
   1.108 -  assumes ccpo_Sup_upper: "\<lbrakk>chain (op \<le>) A; x \<in> A\<rbrakk> \<Longrightarrow> x \<le> Sup A"
   1.109 -  assumes ccpo_Sup_least: "\<lbrakk>chain (op \<le>) A; \<And>x. x \<in> A \<Longrightarrow> x \<le> z\<rbrakk> \<Longrightarrow> Sup A \<le> z"
   1.110 +  assumes ccpo_Sup_upper: "chain (op \<le>) A \<Longrightarrow> x \<in> A \<Longrightarrow> x \<le> Sup A"
   1.111 +  assumes ccpo_Sup_least: "chain (op \<le>) A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> x \<le> z) \<Longrightarrow> Sup A \<le> z"
   1.112  begin
   1.113  
   1.114  lemma chain_singleton: "Complete_Partial_Order.chain op \<le> {x}"
   1.115 -by(rule chainI) simp
   1.116 +  by (rule chainI) simp
   1.117  
   1.118  lemma ccpo_Sup_singleton [simp]: "\<Squnion>{x} = x"
   1.119 -by(rule antisym)(auto intro: ccpo_Sup_least ccpo_Sup_upper simp add: chain_singleton)
   1.120 +  by (rule antisym)(auto intro: ccpo_Sup_least ccpo_Sup_upper simp add: chain_singleton)
   1.121 +
   1.122  
   1.123  subsection \<open>Transfinite iteration of a function\<close>
   1.124  
   1.125 -context notes [[inductive_internals]] begin
   1.126 +context notes [[inductive_internals]]
   1.127 +begin
   1.128  
   1.129  inductive_set iterates :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a set"
   1.130 -for f :: "'a \<Rightarrow> 'a"
   1.131 -where
   1.132 -  step: "x \<in> iterates f \<Longrightarrow> f x \<in> iterates f"
   1.133 -| Sup: "chain (op \<le>) M \<Longrightarrow> \<forall>x\<in>M. x \<in> iterates f \<Longrightarrow> Sup M \<in> iterates f"
   1.134 +  for f :: "'a \<Rightarrow> 'a"
   1.135 +  where
   1.136 +    step: "x \<in> iterates f \<Longrightarrow> f x \<in> iterates f"
   1.137 +  | Sup: "chain (op \<le>) M \<Longrightarrow> \<forall>x\<in>M. x \<in> iterates f \<Longrightarrow> Sup M \<in> iterates f"
   1.138  
   1.139  end
   1.140  
   1.141 -lemma iterates_le_f:
   1.142 -  "x \<in> iterates f \<Longrightarrow> monotone (op \<le>) (op \<le>) f \<Longrightarrow> x \<le> f x"
   1.143 -by (induct x rule: iterates.induct)
   1.144 -  (force dest: monotoneD intro!: ccpo_Sup_upper ccpo_Sup_least)+
   1.145 +lemma iterates_le_f: "x \<in> iterates f \<Longrightarrow> monotone (op \<le>) (op \<le>) f \<Longrightarrow> x \<le> f x"
   1.146 +  by (induct x rule: iterates.induct)
   1.147 +    (force dest: monotoneD intro!: ccpo_Sup_upper ccpo_Sup_least)+
   1.148  
   1.149  lemma chain_iterates:
   1.150    assumes f: "monotone (op \<le>) (op \<le>) f"
   1.151    shows "chain (op \<le>) (iterates f)" (is "chain _ ?C")
   1.152  proof (rule chainI)
   1.153 -  fix x y assume "x \<in> ?C" "y \<in> ?C"
   1.154 +  fix x y
   1.155 +  assume "x \<in> ?C" "y \<in> ?C"
   1.156    then show "x \<le> y \<or> y \<le> x"
   1.157    proof (induct x arbitrary: y rule: iterates.induct)
   1.158 -    fix x y assume y: "y \<in> ?C"
   1.159 -    and IH: "\<And>z. z \<in> ?C \<Longrightarrow> x \<le> z \<or> z \<le> x"
   1.160 +    fix x y
   1.161 +    assume y: "y \<in> ?C"
   1.162 +      and IH: "\<And>z. z \<in> ?C \<Longrightarrow> x \<le> z \<or> z \<le> x"
   1.163      from y show "f x \<le> y \<or> y \<le> f x"
   1.164      proof (induct y rule: iterates.induct)
   1.165 -      case (step y) with IH f show ?case by (auto dest: monotoneD)
   1.166 +      case (step y)
   1.167 +      with IH f show ?case by (auto dest: monotoneD)
   1.168      next
   1.169        case (Sup M)
   1.170        then have chM: "chain (op \<le>) M"
   1.171          and IH': "\<And>z. z \<in> M \<Longrightarrow> f x \<le> z \<or> z \<le> f x" by auto
   1.172        show "f x \<le> Sup M \<or> Sup M \<le> f x"
   1.173        proof (cases "\<exists>z\<in>M. f x \<le> z")
   1.174 -        case True then have "f x \<le> Sup M"
   1.175 +        case True
   1.176 +        then have "f x \<le> Sup M"
   1.177            apply rule
   1.178            apply (erule order_trans)
   1.179 -          by (rule ccpo_Sup_upper[OF chM])
   1.180 -        thus ?thesis ..
   1.181 +          apply (rule ccpo_Sup_upper[OF chM])
   1.182 +          apply assumption
   1.183 +          done
   1.184 +        then show ?thesis ..
   1.185        next
   1.186 -        case False with IH'
   1.187 -        show ?thesis by (auto intro: ccpo_Sup_least[OF chM])
   1.188 +        case False
   1.189 +        with IH' show ?thesis
   1.190 +          by (auto intro: ccpo_Sup_least[OF chM])
   1.191        qed
   1.192      qed
   1.193    next
   1.194      case (Sup M y)
   1.195      show ?case
   1.196      proof (cases "\<exists>x\<in>M. y \<le> x")
   1.197 -      case True then have "y \<le> Sup M"
   1.198 +      case True
   1.199 +      then have "y \<le> Sup M"
   1.200          apply rule
   1.201          apply (erule order_trans)
   1.202 -        by (rule ccpo_Sup_upper[OF Sup(1)])
   1.203 -      thus ?thesis ..
   1.204 +        apply (rule ccpo_Sup_upper[OF Sup(1)])
   1.205 +        apply assumption
   1.206 +        done
   1.207 +      then show ?thesis ..
   1.208      next
   1.209        case False with Sup
   1.210        show ?thesis by (auto intro: ccpo_Sup_least)
   1.211 @@ -147,19 +155,19 @@
   1.212  qed
   1.213  
   1.214  lemma bot_in_iterates: "Sup {} \<in> iterates f"
   1.215 -by(auto intro: iterates.Sup simp add: chain_empty)
   1.216 +  by (auto intro: iterates.Sup simp add: chain_empty)
   1.217 +
   1.218  
   1.219  subsection \<open>Fixpoint combinator\<close>
   1.220  
   1.221 -definition
   1.222 -  fixp :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a"
   1.223 -where
   1.224 -  "fixp f = Sup (iterates f)"
   1.225 +definition fixp :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a"
   1.226 +  where "fixp f = Sup (iterates f)"
   1.227  
   1.228  lemma iterates_fixp:
   1.229 -  assumes f: "monotone (op \<le>) (op \<le>) f" shows "fixp f \<in> iterates f"
   1.230 -unfolding fixp_def
   1.231 -by (simp add: iterates.Sup chain_iterates f)
   1.232 +  assumes f: "monotone (op \<le>) (op \<le>) f"
   1.233 +  shows "fixp f \<in> iterates f"
   1.234 +  unfolding fixp_def
   1.235 +  by (simp add: iterates.Sup chain_iterates f)
   1.236  
   1.237  lemma fixp_unfold:
   1.238    assumes f: "monotone (op \<le>) (op \<le>) f"
   1.239 @@ -169,35 +177,45 @@
   1.240      by (intro iterates_le_f iterates_fixp f)
   1.241    have "f (fixp f) \<le> Sup (iterates f)"
   1.242      by (intro ccpo_Sup_upper chain_iterates f iterates.step iterates_fixp)
   1.243 -  thus "f (fixp f) \<le> fixp f"
   1.244 -    unfolding fixp_def .
   1.245 +  then show "f (fixp f) \<le> fixp f"
   1.246 +    by (simp only: fixp_def)
   1.247  qed
   1.248  
   1.249  lemma fixp_lowerbound:
   1.250 -  assumes f: "monotone (op \<le>) (op \<le>) f" and z: "f z \<le> z" shows "fixp f \<le> z"
   1.251 -unfolding fixp_def
   1.252 +  assumes f: "monotone (op \<le>) (op \<le>) f"
   1.253 +    and z: "f z \<le> z"
   1.254 +  shows "fixp f \<le> z"
   1.255 +  unfolding fixp_def
   1.256  proof (rule ccpo_Sup_least[OF chain_iterates[OF f]])
   1.257 -  fix x assume "x \<in> iterates f"
   1.258 -  thus "x \<le> z"
   1.259 +  fix x
   1.260 +  assume "x \<in> iterates f"
   1.261 +  then show "x \<le> z"
   1.262    proof (induct x rule: iterates.induct)
   1.263 -    fix x assume "x \<le> z" with f have "f x \<le> f z" by (rule monotoneD)
   1.264 -    also note z finally show "f x \<le> z" .
   1.265 -  qed (auto intro: ccpo_Sup_least)
   1.266 +    case (step x)
   1.267 +    from f \<open>x \<le> z\<close> have "f x \<le> f z" by (rule monotoneD)
   1.268 +    also note z
   1.269 +    finally show "f x \<le> z" .
   1.270 +  next
   1.271 +    case (Sup M)
   1.272 +    then show ?case
   1.273 +      by (auto intro: ccpo_Sup_least)
   1.274 +  qed
   1.275  qed
   1.276  
   1.277  end
   1.278  
   1.279 +
   1.280  subsection \<open>Fixpoint induction\<close>
   1.281  
   1.282  setup \<open>Sign.map_naming (Name_Space.mandatory_path "ccpo")\<close>
   1.283  
   1.284  definition admissible :: "('a set \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
   1.285 -where "admissible lub ord P = (\<forall>A. chain ord A \<longrightarrow> (A \<noteq> {}) \<longrightarrow> (\<forall>x\<in>A. P x) \<longrightarrow> P (lub A))"
   1.286 +  where "admissible lub ord P \<longleftrightarrow> (\<forall>A. chain ord A \<longrightarrow> A \<noteq> {} \<longrightarrow> (\<forall>x\<in>A. P x) \<longrightarrow> P (lub A))"
   1.287  
   1.288  lemma admissibleI:
   1.289    assumes "\<And>A. chain ord A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> \<forall>x\<in>A. P x \<Longrightarrow> P (lub A)"
   1.290    shows "ccpo.admissible lub ord P"
   1.291 -using assms unfolding ccpo.admissible_def by fast
   1.292 +  using assms unfolding ccpo.admissible_def by fast
   1.293  
   1.294  lemma admissibleD:
   1.295    assumes "ccpo.admissible lub ord P"
   1.296 @@ -205,7 +223,7 @@
   1.297    assumes "A \<noteq> {}"
   1.298    assumes "\<And>x. x \<in> A \<Longrightarrow> P x"
   1.299    shows "P (lub A)"
   1.300 -using assms by (auto simp: ccpo.admissible_def)
   1.301 +  using assms by (auto simp: ccpo.admissible_def)
   1.302  
   1.303  setup \<open>Sign.map_naming Name_Space.parent_path\<close>
   1.304  
   1.305 @@ -215,44 +233,54 @@
   1.306    assumes bot: "P (Sup {})"
   1.307    assumes step: "\<And>x. P x \<Longrightarrow> P (f x)"
   1.308    shows "P (fixp f)"
   1.309 -unfolding fixp_def using adm chain_iterates[OF mono]
   1.310 +  unfolding fixp_def
   1.311 +  using adm chain_iterates[OF mono]
   1.312  proof (rule ccpo.admissibleD)
   1.313 -  show "iterates f \<noteq> {}" using bot_in_iterates by auto
   1.314 -  fix x assume "x \<in> iterates f"
   1.315 -  thus "P x"
   1.316 -    by (induct rule: iterates.induct)
   1.317 -      (case_tac "M = {}", auto intro: step bot ccpo.admissibleD adm)
   1.318 +  show "iterates f \<noteq> {}"
   1.319 +    using bot_in_iterates by auto
   1.320 +next
   1.321 +  fix x
   1.322 +  assume "x \<in> iterates f"
   1.323 +  then show "P x"
   1.324 +  proof (induct rule: iterates.induct)
   1.325 +    case prems: (step x)
   1.326 +    from this(2) show ?case by (rule step)
   1.327 +  next
   1.328 +    case (Sup M)
   1.329 +    then show ?case by (cases "M = {}") (auto intro: step bot ccpo.admissibleD adm)
   1.330 +  qed
   1.331  qed
   1.332  
   1.333  lemma admissible_True: "ccpo.admissible lub ord (\<lambda>x. True)"
   1.334 -unfolding ccpo.admissible_def by simp
   1.335 +  unfolding ccpo.admissible_def by simp
   1.336  
   1.337  (*lemma admissible_False: "\<not> ccpo.admissible lub ord (\<lambda>x. False)"
   1.338  unfolding ccpo.admissible_def chain_def by simp
   1.339  *)
   1.340  lemma admissible_const: "ccpo.admissible lub ord (\<lambda>x. t)"
   1.341 -by(auto intro: ccpo.admissibleI)
   1.342 +  by (auto intro: ccpo.admissibleI)
   1.343  
   1.344  lemma admissible_conj:
   1.345    assumes "ccpo.admissible lub ord (\<lambda>x. P x)"
   1.346    assumes "ccpo.admissible lub ord (\<lambda>x. Q x)"
   1.347    shows "ccpo.admissible lub ord (\<lambda>x. P x \<and> Q x)"
   1.348 -using assms unfolding ccpo.admissible_def by simp
   1.349 +  using assms unfolding ccpo.admissible_def by simp
   1.350  
   1.351  lemma admissible_all:
   1.352    assumes "\<And>y. ccpo.admissible lub ord (\<lambda>x. P x y)"
   1.353    shows "ccpo.admissible lub ord (\<lambda>x. \<forall>y. P x y)"
   1.354 -using assms unfolding ccpo.admissible_def by fast
   1.355 +  using assms unfolding ccpo.admissible_def by fast
   1.356  
   1.357  lemma admissible_ball:
   1.358    assumes "\<And>y. y \<in> A \<Longrightarrow> ccpo.admissible lub ord (\<lambda>x. P x y)"
   1.359    shows "ccpo.admissible lub ord (\<lambda>x. \<forall>y\<in>A. P x y)"
   1.360 -using assms unfolding ccpo.admissible_def by fast
   1.361 +  using assms unfolding ccpo.admissible_def by fast
   1.362  
   1.363  lemma chain_compr: "chain ord A \<Longrightarrow> chain ord {x \<in> A. P x}"
   1.364 -unfolding chain_def by fast
   1.365 +  unfolding chain_def by fast
   1.366  
   1.367 -context ccpo begin
   1.368 +context ccpo
   1.369 +begin
   1.370  
   1.371  lemma admissible_disj_lemma:
   1.372    assumes A: "chain (op \<le>)A"
   1.373 @@ -280,17 +308,24 @@
   1.374    assumes Q: "ccpo.admissible Sup (op \<le>) (\<lambda>x. Q x)"
   1.375    shows "ccpo.admissible Sup (op \<le>) (\<lambda>x. P x \<or> Q x)"
   1.376  proof (rule ccpo.admissibleI)
   1.377 -  fix A :: "'a set" assume A: "chain (op \<le>) A"
   1.378 -  assume "A \<noteq> {}"
   1.379 -    and "\<forall>x\<in>A. P x \<or> Q x"
   1.380 -  hence "(\<exists>x\<in>A. P x) \<and> (\<forall>x\<in>A. \<exists>y\<in>A. x \<le> y \<and> P y) \<or> (\<exists>x\<in>A. Q x) \<and> (\<forall>x\<in>A. \<exists>y\<in>A. x \<le> y \<and> Q y)"
   1.381 -    using chainD[OF A] by blast
   1.382 -  hence "(\<exists>x. x \<in> A \<and> P x) \<and> Sup A = Sup {x \<in> A. P x} \<or> (\<exists>x. x \<in> A \<and> Q x) \<and> Sup A = Sup {x \<in> A. Q x}"
   1.383 +  fix A :: "'a set"
   1.384 +  assume A: "chain (op \<le>) A"
   1.385 +  assume "A \<noteq> {}" and "\<forall>x\<in>A. P x \<or> Q x"
   1.386 +  then have "(\<exists>x\<in>A. P x) \<and> (\<forall>x\<in>A. \<exists>y\<in>A. x \<le> y \<and> P y) \<or> (\<exists>x\<in>A. Q x) \<and> (\<forall>x\<in>A. \<exists>y\<in>A. x \<le> y \<and> Q y)"
   1.387 +    using chainD[OF A] by blast  (* slow *)
   1.388 +  then have "(\<exists>x. x \<in> A \<and> P x) \<and> Sup A = Sup {x \<in> A. P x} \<or> (\<exists>x. x \<in> A \<and> Q x) \<and> Sup A = Sup {x \<in> A. Q x}"
   1.389      using admissible_disj_lemma [OF A] by blast
   1.390 -  thus "P (Sup A) \<or> Q (Sup A)"
   1.391 -    apply (rule disjE, simp_all)
   1.392 -    apply (rule disjI1, rule ccpo.admissibleD [OF P chain_compr [OF A]], simp, simp)
   1.393 -    apply (rule disjI2, rule ccpo.admissibleD [OF Q chain_compr [OF A]], simp, simp)
   1.394 +  then show "P (Sup A) \<or> Q (Sup A)"
   1.395 +    apply (rule disjE)
   1.396 +     apply simp_all
   1.397 +     apply (rule disjI1)
   1.398 +     apply (rule ccpo.admissibleD [OF P chain_compr [OF A]])
   1.399 +      apply simp
   1.400 +     apply simp
   1.401 +    apply (rule disjI2)
   1.402 +    apply (rule ccpo.admissibleD [OF Q chain_compr [OF A]])
   1.403 +     apply simp
   1.404 +    apply simp
   1.405      done
   1.406  qed
   1.407  
   1.408 @@ -300,7 +335,8 @@
   1.409    by standard (fast intro: Sup_upper Sup_least)+
   1.410  
   1.411  lemma lfp_eq_fixp:
   1.412 -  assumes f: "mono f" shows "lfp f = fixp f"
   1.413 +  assumes f: "mono f"
   1.414 +  shows "lfp f = fixp f"
   1.415  proof (rule antisym)
   1.416    from f have f': "monotone (op \<le>) (op \<le>) f"
   1.417      unfolding mono_def monotone_def .
     2.1 --- a/src/HOL/Finite_Set.thy	Fri Aug 05 16:36:03 2016 +0200
     2.2 +++ b/src/HOL/Finite_Set.thy	Fri Aug 05 18:14:28 2016 +0200
     2.3 @@ -1,24 +1,26 @@
     2.4  (*  Title:      HOL/Finite_Set.thy
     2.5 -    Author:     Tobias Nipkow, Lawrence C Paulson and Markus Wenzel
     2.6 -                with contributions by Jeremy Avigad and Andrei Popescu
     2.7 +    Author:     Tobias Nipkow
     2.8 +    Author:     Lawrence C Paulson
     2.9 +    Author:     Markus Wenzel
    2.10 +    Author:     Jeremy Avigad
    2.11 +    Author:     Andrei Popescu
    2.12  *)
    2.13  
    2.14  section \<open>Finite sets\<close>
    2.15  
    2.16  theory Finite_Set
    2.17 -imports Product_Type Sum_Type Fields
    2.18 +  imports Product_Type Sum_Type Fields
    2.19  begin
    2.20  
    2.21  subsection \<open>Predicate for finite sets\<close>
    2.22  
    2.23 -context
    2.24 -  notes [[inductive_internals]]
    2.25 +context notes [[inductive_internals]]
    2.26  begin
    2.27  
    2.28  inductive finite :: "'a set \<Rightarrow> bool"
    2.29 -where
    2.30 -  emptyI [simp, intro!]: "finite {}"
    2.31 -| insertI [simp, intro!]: "finite A \<Longrightarrow> finite (insert a A)"
    2.32 +  where
    2.33 +    emptyI [simp, intro!]: "finite {}"
    2.34 +  | insertI [simp, intro!]: "finite A \<Longrightarrow> finite (insert a A)"
    2.35  
    2.36  end
    2.37  
    2.38 @@ -145,7 +147,7 @@
    2.39    shows "\<exists>f n::nat. f ` A = {i. i < n} \<and> inj_on f A"
    2.40  proof -
    2.41    from finite_imp_nat_seg_image_inj_on [OF \<open>finite A\<close>]
    2.42 -  obtain f and n::nat where bij: "bij_betw f {i. i<n} A"
    2.43 +  obtain f and n :: nat where bij: "bij_betw f {i. i<n} A"
    2.44      by (auto simp: bij_betw_def)
    2.45    let ?f = "the_inv_into {i. i<n} f"
    2.46    have "inj_on ?f A \<and> ?f ` A = {i. i<n}"
    2.47 @@ -317,7 +319,7 @@
    2.48  next
    2.49    case insert
    2.50    then show ?case
    2.51 -    by (clarsimp simp del: image_insert simp add: image_insert [symmetric]) blast
    2.52 +    by (clarsimp simp del: image_insert simp add: image_insert [symmetric]) blast  (* slow *)
    2.53  qed
    2.54  
    2.55  lemma finite_vimage_IntI: "finite F \<Longrightarrow> inj_on h A \<Longrightarrow> finite (h -` F \<inter> A)"
    2.56 @@ -328,7 +330,8 @@
    2.57    done
    2.58  
    2.59  lemma finite_finite_vimage_IntI:
    2.60 -  assumes "finite F" and "\<And>y. y \<in> F \<Longrightarrow> finite ((h -` {y}) \<inter> A)"
    2.61 +  assumes "finite F"
    2.62 +    and "\<And>y. y \<in> F \<Longrightarrow> finite ((h -` {y}) \<inter> A)"
    2.63    shows "finite (h -` F \<inter> A)"
    2.64  proof -
    2.65    have *: "h -` F \<inter> A = (\<Union> y\<in>F. (h -` {y}) \<inter> A)"
    2.66 @@ -464,7 +467,7 @@
    2.67  proof
    2.68    assume "finite (Pow A)"
    2.69    then have "finite ((\<lambda>x. {x}) ` A)"
    2.70 -    by (blast intro: finite_subset)
    2.71 +    by (blast intro: finite_subset)  (* somewhat slow *)
    2.72    then show "finite A"
    2.73      by (rule finite_imageD [unfolded inj_on_def]) simp
    2.74  next
    2.75 @@ -492,7 +495,7 @@
    2.76    from finite_subset[OF this] assms have 1: "finite (?F ` ?S)"
    2.77      by simp
    2.78    have 2: "inj_on ?F ?S"
    2.79 -    by (fastforce simp add: inj_on_def set_eq_iff fun_eq_iff)
    2.80 +    by (fastforce simp add: inj_on_def set_eq_iff fun_eq_iff)  (* somewhat slow *)
    2.81    show ?thesis
    2.82      by (rule finite_imageD [OF 1 2])
    2.83  qed
    2.84 @@ -524,7 +527,7 @@
    2.85  
    2.86  lemma finite_subset_induct [consumes 2, case_names empty insert]:
    2.87    assumes "finite F" and "F \<subseteq> A"
    2.88 -  assumes empty: "P {}"
    2.89 +    and empty: "P {}"
    2.90      and insert: "\<And>a F. finite F \<Longrightarrow> a \<in> A \<Longrightarrow> a \<notin> F \<Longrightarrow> P F \<Longrightarrow> P (insert a F)"
    2.91    shows "P F"
    2.92    using \<open>finite F\<close> \<open>F \<subseteq> A\<close>
    2.93 @@ -545,7 +548,7 @@
    2.94  
    2.95  lemma finite_empty_induct:
    2.96    assumes "finite A"
    2.97 -  assumes "P A"
    2.98 +    and "P A"
    2.99      and remove: "\<And>a A. finite A \<Longrightarrow> a \<in> A \<Longrightarrow> P A \<Longrightarrow> P (A - {a})"
   2.100    shows "P {}"
   2.101  proof -
   2.102 @@ -604,8 +607,8 @@
   2.103  
   2.104  lemma finite_subset_induct' [consumes 2, case_names empty insert]:
   2.105    assumes "finite F" and "F \<subseteq> A"
   2.106 -  and empty: "P {}"
   2.107 -  and insert: "\<And>a F. \<lbrakk>finite F; a \<in> A; F \<subseteq> A; a \<notin> F; P F \<rbrakk> \<Longrightarrow> P (insert a F)"
   2.108 +    and empty: "P {}"
   2.109 +    and insert: "\<And>a F. \<lbrakk>finite F; a \<in> A; F \<subseteq> A; a \<notin> F; P F \<rbrakk> \<Longrightarrow> P (insert a F)"
   2.110    shows "P F"
   2.111  proof -
   2.112    from \<open>finite F\<close>
   2.113 @@ -632,7 +635,8 @@
   2.114  
   2.115  subsection \<open>Class \<open>finite\<close>\<close>
   2.116  
   2.117 -class finite = assumes finite_UNIV: "finite (UNIV :: 'a set)"
   2.118 +class finite =
   2.119 +  assumes finite_UNIV: "finite (UNIV :: 'a set)"
   2.120  begin
   2.121  
   2.122  lemma finite [simp]: "finite (A :: 'a set)"
   2.123 @@ -700,9 +704,9 @@
   2.124  
   2.125  inductive fold_graph :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> bool"
   2.126    for f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" and z :: 'b
   2.127 -where
   2.128 -  emptyI [intro]: "fold_graph f z {} z"
   2.129 -| insertI [intro]: "x \<notin> A \<Longrightarrow> fold_graph f z A y \<Longrightarrow> fold_graph f z (insert x A) (f x y)"
   2.130 +  where
   2.131 +    emptyI [intro]: "fold_graph f z {} z"
   2.132 +  | insertI [intro]: "x \<notin> A \<Longrightarrow> fold_graph f z A y \<Longrightarrow> fold_graph f z (insert x A) (f x y)"
   2.133  
   2.134  inductive_cases empty_fold_graphE [elim!]: "fold_graph f z {} x"
   2.135  
   2.136 @@ -1069,7 +1073,7 @@
   2.137    interpret comp_fun_idem Set.remove
   2.138      by (fact comp_fun_idem_remove)
   2.139    from \<open>finite A\<close> have "fold Set.remove B A = B - A"
   2.140 -    by (induct A arbitrary: B) auto
   2.141 +    by (induct A arbitrary: B) auto  (* slow *)
   2.142    then show ?thesis ..
   2.143  qed
   2.144  
   2.145 @@ -1124,7 +1128,7 @@
   2.146  qed
   2.147  
   2.148  lemma comp_fun_commute_Pow_fold: "comp_fun_commute (\<lambda>x A. A \<union> Set.insert x ` A)"
   2.149 -  by (clarsimp simp: fun_eq_iff comp_fun_commute_def) blast
   2.150 +  by (clarsimp simp: fun_eq_iff comp_fun_commute_def) blast  (* somewhat slow *)
   2.151  
   2.152  lemma Pow_fold:
   2.153    assumes "finite A"
   2.154 @@ -1222,13 +1226,12 @@
   2.155  subsubsection \<open>The natural case\<close>
   2.156  
   2.157  locale folding =
   2.158 -  fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b"
   2.159 -  fixes z :: "'b"
   2.160 +  fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" and z :: "'b"
   2.161    assumes comp_fun_commute: "f y \<circ> f x = f x \<circ> f y"
   2.162  begin
   2.163  
   2.164  interpretation fold?: comp_fun_commute f
   2.165 -  by standard (insert comp_fun_commute, simp add: fun_eq_iff)
   2.166 +  by standard (use comp_fun_commute in \<open>simp add: fun_eq_iff\<close>)
   2.167  
   2.168  definition F :: "'a set \<Rightarrow> 'b"
   2.169    where eq_fold: "F A = fold f z A"
   2.170 @@ -1332,14 +1335,14 @@
   2.171  
   2.172  lemma card_Suc_Diff1: "finite A \<Longrightarrow> x \<in> A \<Longrightarrow> Suc (card (A - {x})) = card A"
   2.173    apply (rule insert_Diff [THEN subst, where t = A])
   2.174 -  apply assumption
   2.175 +   apply assumption
   2.176    apply (simp del: insert_Diff_single)
   2.177    done
   2.178  
   2.179  lemma card_insert_le_m1: "n > 0 \<Longrightarrow> card y \<le> n - 1 \<Longrightarrow> card (insert x y) \<le> n"
   2.180    apply (cases "finite y")
   2.181 -  apply (cases "x \<in> y")
   2.182 -  apply (auto simp: insert_absorb)
   2.183 +   apply (cases "x \<in> y")
   2.184 +    apply (auto simp: insert_absorb)
   2.185    done
   2.186  
   2.187  lemma card_Diff_singleton: "finite A \<Longrightarrow> x \<in> A \<Longrightarrow> card (A - {x}) = card A - 1"
   2.188 @@ -1397,7 +1400,7 @@
   2.189  
   2.190  lemma card_seteq: "finite B \<Longrightarrow> (\<And>A. A \<subseteq> B \<Longrightarrow> card B \<le> card A \<Longrightarrow> A = B)"
   2.191    apply (induct rule: finite_induct)
   2.192 -  apply simp
   2.193 +   apply simp
   2.194    apply clarify
   2.195    apply (subgoal_tac "finite A \<and> A - {x} \<subseteq> F")
   2.196     prefer 2 apply (blast intro: finite_subset, atomize)
   2.197 @@ -1430,7 +1433,7 @@
   2.198  lemma card_Un_le: "card (A \<union> B) \<le> card A + card B"
   2.199    apply (cases "finite A")
   2.200     apply (cases "finite B")
   2.201 -    using le_iff_add card_Un_Int apply blast
   2.202 +    apply (use le_iff_add card_Un_Int in blast)
   2.203     apply simp
   2.204    apply simp
   2.205    done
   2.206 @@ -1539,7 +1542,7 @@
   2.207  
   2.208  lemma insert_partition:
   2.209    "x \<notin> F \<Longrightarrow> \<forall>c1 \<in> insert x F. \<forall>c2 \<in> insert x F. c1 \<noteq> c2 \<longrightarrow> c1 \<inter> c2 = {} \<Longrightarrow> x \<inter> \<Union>F = {}"
   2.210 -  by auto
   2.211 +  by auto  (* somewhat slow *)
   2.212  
   2.213  lemma finite_psubset_induct [consumes 1, case_names psubset]:
   2.214    assumes finite: "finite A"
   2.215 @@ -1597,13 +1600,13 @@
   2.216      and remove: "\<And>A. finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> A \<subseteq> B \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> P (A - {x})) \<Longrightarrow> P A"
   2.217    shows "P B"
   2.218  proof (cases "finite B")
   2.219 -  assume "\<not>finite B"
   2.220 +  case False
   2.221    then show ?thesis by (rule infinite)
   2.222  next
   2.223 +  case True
   2.224    define A where "A = B"
   2.225 -  assume "finite B"
   2.226 -  then have "finite A" "A \<subseteq> B"
   2.227 -    by (simp_all add: A_def)
   2.228 +  with True have "finite A" "A \<subseteq> B"
   2.229 +    by simp_all
   2.230    then show "P A"
   2.231    proof (induct "card A" arbitrary: A)
   2.232      case 0
   2.233 @@ -1623,9 +1626,9 @@
   2.234  
   2.235  lemma finite_remove_induct [consumes 1, case_names empty remove]:
   2.236    fixes P :: "'a set \<Rightarrow> bool"
   2.237 -  assumes finite: "finite B"
   2.238 -    and empty: "P {}"
   2.239 -    and rm: "\<And>A. finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> A \<subseteq> B \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> P (A - {x})) \<Longrightarrow> P A"
   2.240 +  assumes "finite B"
   2.241 +    and "P {}"
   2.242 +    and "\<And>A. finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> A \<subseteq> B \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> P (A - {x})) \<Longrightarrow> P A"
   2.243    defines "B' \<equiv> B"
   2.244    shows "P B'"
   2.245    by (induct B' rule: remove_induct) (simp_all add: assms)
   2.246 @@ -1636,10 +1639,14 @@
   2.247    "finite C \<Longrightarrow> finite (\<Union>C) \<Longrightarrow> (\<forall>c\<in>C. card c = k) \<Longrightarrow>
   2.248      (\<forall>c1 \<in> C. \<forall>c2 \<in> C. c1 \<noteq> c2 \<longrightarrow> c1 \<inter> c2 = {}) \<Longrightarrow>
   2.249      k * card C = card (\<Union>C)"
   2.250 -  apply (induct rule: finite_induct)
   2.251 -  apply simp
   2.252 -  apply (simp add: card_Un_disjoint insert_partition finite_subset [of _ "\<Union>(insert x F)"])
   2.253 -  done
   2.254 +proof (induct rule: finite_induct)
   2.255 +  case empty
   2.256 +  then show ?case by simp
   2.257 +next
   2.258 +  case (insert x F)
   2.259 +  then show ?case
   2.260 +    by (simp add: card_Un_disjoint insert_partition finite_subset [of _ "\<Union>(insert _ _)"])
   2.261 +qed
   2.262  
   2.263  lemma card_eq_UNIV_imp_eq_UNIV:
   2.264    assumes fin: "finite (UNIV :: 'a set)"
   2.265 @@ -1679,7 +1686,7 @@
   2.266      show "b \<notin> A - {b}"
   2.267        by blast
   2.268      show "card (A - {b}) = k" and "k = 0 \<longrightarrow> A - {b} = {}"
   2.269 -      using assms b fin by(fastforce dest:mk_disjoint_insert)+
   2.270 +      using assms b fin by (fastforce dest: mk_disjoint_insert)+
   2.271    qed
   2.272  qed
   2.273  
   2.274 @@ -1688,7 +1695,7 @@
   2.275      (\<exists>b B. A = insert b B \<and> b \<notin> B \<and> card B = k \<and> (k = 0 \<longrightarrow> B = {}))"
   2.276    apply (auto elim!: card_eq_SucD)
   2.277    apply (subst card.insert)
   2.278 -  apply (auto simp add: intro:ccontr)
   2.279 +    apply (auto simp add: intro:ccontr)
   2.280    done
   2.281  
   2.282  lemma card_1_singletonE:
   2.283 @@ -1761,7 +1768,7 @@
   2.284  qed
   2.285  
   2.286  lemma bij_betw_same_card: "bij_betw f A B \<Longrightarrow> card A = card B"
   2.287 -  by(auto simp: card_image bij_betw_def)
   2.288 +  by (auto simp: card_image bij_betw_def)
   2.289  
   2.290  lemma endo_inj_surj: "finite A \<Longrightarrow> f ` A \<subseteq> A \<Longrightarrow> inj_on f A \<Longrightarrow> f ` A = A"
   2.291    by (simp add: card_seteq card_image)
   2.292 @@ -1852,12 +1859,12 @@
   2.293    from finite_Pow_iff[THEN iffD2, OF \<open>finite B\<close>] have "finite (?F ` A)"
   2.294      by (blast intro: rev_finite_subset)
   2.295    from pigeonhole_infinite [where f = ?F, OF assms(1) this]
   2.296 -  obtain a0 where "a0 \<in> A" and 1: "\<not> finite {a\<in>A. ?F a = ?F a0}" ..
   2.297 +  obtain a0 where "a0 \<in> A" and infinite: "\<not> finite {a\<in>A. ?F a = ?F a0}" ..
   2.298    obtain b0 where "b0 \<in> B" and "R a0 b0"
   2.299      using \<open>a0 \<in> A\<close> assms(3) by blast
   2.300 -  have "finite {a\<in>A. ?F a = ?F a0}" if "finite{a:A. R a b0}"
   2.301 +  have "finite {a\<in>A. ?F a = ?F a0}" if "finite {a\<in>A. R a b0}"
   2.302      using \<open>b0 \<in> B\<close> \<open>R a0 b0\<close> that by (blast intro: rev_finite_subset)
   2.303 -  with 1 \<open>b0 : B\<close> show ?thesis
   2.304 +  with infinite \<open>b0 \<in> B\<close> show ?thesis
   2.305      by blast
   2.306  qed
   2.307  
   2.308 @@ -1896,7 +1903,7 @@
   2.309      then show ?case
   2.310        apply simp
   2.311        apply (subst card_Un_disjoint)
   2.312 -      apply (auto simp add: disjoint_eq_subset_Compl)
   2.313 +         apply (auto simp add: disjoint_eq_subset_Compl)
   2.314        done
   2.315    qed
   2.316  qed
   2.317 @@ -1914,10 +1921,12 @@
   2.318      by (simp add: eq_card_imp_inj_on)
   2.319  qed
   2.320  
   2.321 -lemma finite_UNIV_surj_inj: "finite(UNIV:: 'a set) \<Longrightarrow> surj f \<Longrightarrow> inj f" for f :: "'a \<Rightarrow> 'a"
   2.322 +lemma finite_UNIV_surj_inj: "finite(UNIV:: 'a set) \<Longrightarrow> surj f \<Longrightarrow> inj f"
   2.323 +  for f :: "'a \<Rightarrow> 'a"
   2.324    by (blast intro: finite_surj_inj subset_UNIV)
   2.325  
   2.326 -lemma finite_UNIV_inj_surj: "finite(UNIV:: 'a set) \<Longrightarrow> inj f \<Longrightarrow> surj f" for f :: "'a \<Rightarrow> 'a"
   2.327 +lemma finite_UNIV_inj_surj: "finite(UNIV:: 'a set) \<Longrightarrow> inj f \<Longrightarrow> surj f"
   2.328 +  for f :: "'a \<Rightarrow> 'a"
   2.329    by (fastforce simp:surj_def dest!: endo_inj_surj)
   2.330  
   2.331  corollary infinite_UNIV_nat [iff]: "\<not> finite (UNIV :: nat set)"
   2.332 @@ -2013,7 +2022,7 @@
   2.333        using psubset.hyps by blast
   2.334      show False
   2.335        apply (rule psubset.IH [where B = "A - {x}"])
   2.336 -      using \<open>x \<in> A\<close> apply blast
   2.337 +       apply (use \<open>x \<in> A\<close> in blast)
   2.338        apply (simp add: \<open>X (A - {x})\<close>)
   2.339        done
   2.340    qed
     3.1 --- a/src/HOL/Hilbert_Choice.thy	Fri Aug 05 16:36:03 2016 +0200
     3.2 +++ b/src/HOL/Hilbert_Choice.thy	Fri Aug 05 18:14:28 2016 +0200
     3.3 @@ -6,23 +6,23 @@
     3.4  section \<open>Hilbert's Epsilon-Operator and the Axiom of Choice\<close>
     3.5  
     3.6  theory Hilbert_Choice
     3.7 -imports Wellfounded
     3.8 -keywords "specification" :: thy_goal
     3.9 +  imports Wellfounded
    3.10 +  keywords "specification" :: thy_goal
    3.11  begin
    3.12  
    3.13  subsection \<open>Hilbert's epsilon\<close>
    3.14  
    3.15 -axiomatization Eps :: "('a => bool) => 'a" where
    3.16 -  someI: "P x ==> P (Eps P)"
    3.17 +axiomatization Eps :: "('a \<Rightarrow> bool) \<Rightarrow> 'a"
    3.18 +  where someI: "P x \<Longrightarrow> P (Eps P)"
    3.19  
    3.20  syntax (epsilon)
    3.21 -  "_Eps"        :: "[pttrn, bool] => 'a"    ("(3\<some>_./ _)" [0, 10] 10)
    3.22 +  "_Eps" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a"  ("(3\<some>_./ _)" [0, 10] 10)
    3.23  syntax (input)
    3.24 -  "_Eps"        :: "[pttrn, bool] => 'a"    ("(3@ _./ _)" [0, 10] 10)
    3.25 +  "_Eps" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a"  ("(3@ _./ _)" [0, 10] 10)
    3.26  syntax
    3.27 -  "_Eps"        :: "[pttrn, bool] => 'a"    ("(3SOME _./ _)" [0, 10] 10)
    3.28 +  "_Eps" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a"  ("(3SOME _./ _)" [0, 10] 10)
    3.29  translations
    3.30 -  "SOME x. P" == "CONST Eps (%x. P)"
    3.31 +  "SOME x. P" \<rightleftharpoons> "CONST Eps (\<lambda>x. P)"
    3.32  
    3.33  print_translation \<open>
    3.34    [(@{const_syntax Eps}, fn _ => fn [Abs abs] =>
    3.35 @@ -30,90 +30,92 @@
    3.36        in Syntax.const @{syntax_const "_Eps"} $ x $ t end)]
    3.37  \<close> \<comment> \<open>to avoid eta-contraction of body\<close>
    3.38  
    3.39 -definition inv_into :: "'a set => ('a => 'b) => ('b => 'a)" where
    3.40 -"inv_into A f == %x. SOME y. y : A & f y = x"
    3.41 +definition inv_into :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a)"
    3.42 +  where "inv_into A f \<equiv> \<lambda>x. SOME y. y \<in> A \<and> f y = x"
    3.43  
    3.44 -abbreviation inv :: "('a => 'b) => ('b => 'a)" where
    3.45 -"inv == inv_into UNIV"
    3.46 +abbreviation inv :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a)"
    3.47 +  where "inv \<equiv> inv_into UNIV"
    3.48  
    3.49  
    3.50  subsection \<open>Hilbert's Epsilon-operator\<close>
    3.51  
    3.52 -text\<open>Easier to apply than \<open>someI\<close> if the witness comes from an
    3.53 -existential formula\<close>
    3.54 -lemma someI_ex [elim?]: "\<exists>x. P x ==> P (SOME x. P x)"
    3.55 -apply (erule exE)
    3.56 -apply (erule someI)
    3.57 -done
    3.58 +text \<open>
    3.59 +  Easier to apply than \<open>someI\<close> if the witness comes from an
    3.60 +  existential formula.
    3.61 +\<close>
    3.62 +lemma someI_ex [elim?]: "\<exists>x. P x \<Longrightarrow> P (SOME x. P x)"
    3.63 +  apply (erule exE)
    3.64 +  apply (erule someI)
    3.65 +  done
    3.66  
    3.67 -text\<open>Easier to apply than \<open>someI\<close> because the conclusion has only one
    3.68 -occurrence of @{term P}.\<close>
    3.69 -lemma someI2: "[| P a;  !!x. P x ==> Q x |] ==> Q (SOME x. P x)"
    3.70 +text \<open>
    3.71 +  Easier to apply than \<open>someI\<close> because the conclusion has only one
    3.72 +  occurrence of @{term P}.
    3.73 +\<close>
    3.74 +lemma someI2: "P a \<Longrightarrow> (\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> Q (SOME x. P x)"
    3.75    by (blast intro: someI)
    3.76  
    3.77 -text\<open>Easier to apply than \<open>someI2\<close> if the witness comes from an
    3.78 -existential formula\<close>
    3.79 -
    3.80 -lemma someI2_ex: "[| \<exists>a. P a; !!x. P x ==> Q x |] ==> Q (SOME x. P x)"
    3.81 -  by (blast intro: someI2)
    3.82 -
    3.83 -lemma someI2_bex: "[| \<exists>a\<in>A. P a; !!x. x \<in> A \<and> P x ==> Q x |] ==> Q (SOME x. x \<in> A \<and> P x)"
    3.84 +text \<open>
    3.85 +  Easier to apply than \<open>someI2\<close> if the witness comes from an
    3.86 +  existential formula.
    3.87 +\<close>
    3.88 +lemma someI2_ex: "\<exists>a. P a \<Longrightarrow> (\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> Q (SOME x. P x)"
    3.89    by (blast intro: someI2)
    3.90  
    3.91 -lemma some_equality [intro]:
    3.92 -     "[| P a;  !!x. P x ==> x=a |] ==> (SOME x. P x) = a"
    3.93 -by (blast intro: someI2)
    3.94 +lemma someI2_bex: "\<exists>a\<in>A. P a \<Longrightarrow> (\<And>x. x \<in> A \<and> P x \<Longrightarrow> Q x) \<Longrightarrow> Q (SOME x. x \<in> A \<and> P x)"
    3.95 +  by (blast intro: someI2)
    3.96 +
    3.97 +lemma some_equality [intro]: "P a \<Longrightarrow> (\<And>x. P x \<Longrightarrow> x = a) \<Longrightarrow> (SOME x. P x) = a"
    3.98 +  by (blast intro: someI2)
    3.99  
   3.100 -lemma some1_equality: "[| EX!x. P x; P a |] ==> (SOME x. P x) = a"
   3.101 -by blast
   3.102 +lemma some1_equality: "EX!x. P x \<Longrightarrow> P a \<Longrightarrow> (SOME x. P x) = a"
   3.103 +  by blast
   3.104  
   3.105 -lemma some_eq_ex: "P (SOME x. P x) =  (\<exists>x. P x)"
   3.106 -by (blast intro: someI)
   3.107 +lemma some_eq_ex: "P (SOME x. P x) \<longleftrightarrow> (\<exists>x. P x)"
   3.108 +  by (blast intro: someI)
   3.109  
   3.110  lemma some_in_eq: "(SOME x. x \<in> A) \<in> A \<longleftrightarrow> A \<noteq> {}"
   3.111    unfolding ex_in_conv[symmetric] by (rule some_eq_ex)
   3.112  
   3.113 -lemma some_eq_trivial [simp]: "(SOME y. y=x) = x"
   3.114 -apply (rule some_equality)
   3.115 -apply (rule refl, assumption)
   3.116 -done
   3.117 +lemma some_eq_trivial [simp]: "(SOME y. y = x) = x"
   3.118 +  by (rule some_equality) (rule refl)
   3.119  
   3.120 -lemma some_sym_eq_trivial [simp]: "(SOME y. x=y) = x"
   3.121 -apply (rule some_equality)
   3.122 -apply (rule refl)
   3.123 -apply (erule sym)
   3.124 -done
   3.125 +lemma some_sym_eq_trivial [simp]: "(SOME y. x = y) = x"
   3.126 +  apply (rule some_equality)
   3.127 +   apply (rule refl)
   3.128 +  apply (erule sym)
   3.129 +  done
   3.130  
   3.131  
   3.132 -subsection\<open>Axiom of Choice, Proved Using the Description Operator\<close>
   3.133 +subsection \<open>Axiom of Choice, Proved Using the Description Operator\<close>
   3.134  
   3.135 -lemma choice: "\<forall>x. \<exists>y. Q x y ==> \<exists>f. \<forall>x. Q x (f x)"
   3.136 -by (fast elim: someI)
   3.137 +lemma choice: "\<forall>x. \<exists>y. Q x y \<Longrightarrow> \<exists>f. \<forall>x. Q x (f x)"
   3.138 +  by (fast elim: someI)
   3.139  
   3.140 -lemma bchoice: "\<forall>x\<in>S. \<exists>y. Q x y ==> \<exists>f. \<forall>x\<in>S. Q x (f x)"
   3.141 -by (fast elim: someI)
   3.142 +lemma bchoice: "\<forall>x\<in>S. \<exists>y. Q x y \<Longrightarrow> \<exists>f. \<forall>x\<in>S. Q x (f x)"
   3.143 +  by (fast elim: someI)
   3.144  
   3.145  lemma choice_iff: "(\<forall>x. \<exists>y. Q x y) \<longleftrightarrow> (\<exists>f. \<forall>x. Q x (f x))"
   3.146 -by (fast elim: someI)
   3.147 +  by (fast elim: someI)
   3.148  
   3.149  lemma choice_iff': "(\<forall>x. P x \<longrightarrow> (\<exists>y. Q x y)) \<longleftrightarrow> (\<exists>f. \<forall>x. P x \<longrightarrow> Q x (f x))"
   3.150 -by (fast elim: someI)
   3.151 +  by (fast elim: someI)
   3.152  
   3.153  lemma bchoice_iff: "(\<forall>x\<in>S. \<exists>y. Q x y) \<longleftrightarrow> (\<exists>f. \<forall>x\<in>S. Q x (f x))"
   3.154 -by (fast elim: someI)
   3.155 +  by (fast elim: someI)
   3.156  
   3.157  lemma bchoice_iff': "(\<forall>x\<in>S. P x \<longrightarrow> (\<exists>y. Q x y)) \<longleftrightarrow> (\<exists>f. \<forall>x\<in>S. P x \<longrightarrow> Q x (f x))"
   3.158 -by (fast elim: someI)
   3.159 +  by (fast elim: someI)
   3.160  
   3.161  lemma dependent_nat_choice:
   3.162 -  assumes  1: "\<exists>x. P 0 x" and
   3.163 -           2: "\<And>x n. P n x \<Longrightarrow> \<exists>y. P (Suc n) y \<and> Q n x y"
   3.164 +  assumes 1: "\<exists>x. P 0 x"
   3.165 +    and 2: "\<And>x n. P n x \<Longrightarrow> \<exists>y. P (Suc n) y \<and> Q n x y"
   3.166    shows "\<exists>f. \<forall>n. P n (f n) \<and> Q n (f n) (f (Suc n))"
   3.167  proof (intro exI allI conjI)
   3.168    fix n
   3.169    define f where "f = rec_nat (SOME x. P 0 x) (\<lambda>n x. SOME y. P (Suc n) y \<and> Q n x y)"
   3.170 -  have "P 0 (f 0)" "\<And>n. P n (f n) \<Longrightarrow> P (Suc n) (f (Suc n)) \<and> Q n (f n) (f (Suc n))"
   3.171 -    using someI_ex[OF 1] someI_ex[OF 2] by (simp_all add: f_def)
   3.172 +  then have "P 0 (f 0)" "\<And>n. P n (f n) \<Longrightarrow> P (Suc n) (f (Suc n)) \<and> Q n (f n) (f (Suc n))"
   3.173 +    using someI_ex[OF 1] someI_ex[OF 2] by simp_all
   3.174    then show "P n (f n)" "Q n (f n) (f (Suc n))"
   3.175      by (induct n) auto
   3.176  qed
   3.177 @@ -121,181 +123,172 @@
   3.178  
   3.179  subsection \<open>Function Inverse\<close>
   3.180  
   3.181 -lemma inv_def: "inv f = (%y. SOME x. f x = y)"
   3.182 -by(simp add: inv_into_def)
   3.183 +lemma inv_def: "inv f = (\<lambda>y. SOME x. f x = y)"
   3.184 +  by (simp add: inv_into_def)
   3.185  
   3.186 -lemma inv_into_into: "x : f ` A ==> inv_into A f x : A"
   3.187 -apply (simp add: inv_into_def)
   3.188 -apply (fast intro: someI2)
   3.189 -done
   3.190 +lemma inv_into_into: "x \<in> f ` A \<Longrightarrow> inv_into A f x \<in> A"
   3.191 +  by (simp add: inv_into_def) (fast intro: someI2)
   3.192  
   3.193 -lemma inv_identity [simp]:
   3.194 -  "inv (\<lambda>a. a) = (\<lambda>a. a)"
   3.195 +lemma inv_identity [simp]: "inv (\<lambda>a. a) = (\<lambda>a. a)"
   3.196    by (simp add: inv_def)
   3.197  
   3.198 -lemma inv_id [simp]:
   3.199 -  "inv id = id"
   3.200 +lemma inv_id [simp]: "inv id = id"
   3.201    by (simp add: id_def)
   3.202  
   3.203 -lemma inv_into_f_f [simp]:
   3.204 -  "[| inj_on f A;  x : A |] ==> inv_into A f (f x) = x"
   3.205 -apply (simp add: inv_into_def inj_on_def)
   3.206 -apply (blast intro: someI2)
   3.207 -done
   3.208 +lemma inv_into_f_f [simp]: "inj_on f A \<Longrightarrow> x \<in> A \<Longrightarrow> inv_into A f (f x) = x"
   3.209 +  by (simp add: inv_into_def inj_on_def) (blast intro: someI2)
   3.210  
   3.211 -lemma inv_f_f: "inj f ==> inv f (f x) = x"
   3.212 -by simp
   3.213 +lemma inv_f_f: "inj f \<Longrightarrow> inv f (f x) = x"
   3.214 +  by simp
   3.215  
   3.216 -lemma f_inv_into_f: "y : f`A  ==> f (inv_into A f y) = y"
   3.217 -apply (simp add: inv_into_def)
   3.218 -apply (fast intro: someI2)
   3.219 -done
   3.220 +lemma f_inv_into_f: "y : f`A \<Longrightarrow> f (inv_into A f y) = y"
   3.221 +  by (simp add: inv_into_def) (fast intro: someI2)
   3.222  
   3.223 -lemma inv_into_f_eq: "[| inj_on f A; x : A; f x = y |] ==> inv_into A f y = x"
   3.224 -apply (erule subst)
   3.225 -apply (fast intro: inv_into_f_f)
   3.226 -done
   3.227 +lemma inv_into_f_eq: "inj_on f A \<Longrightarrow> x \<in> A \<Longrightarrow> f x = y \<Longrightarrow> inv_into A f y = x"
   3.228 +  by (erule subst) (fast intro: inv_into_f_f)
   3.229  
   3.230 -lemma inv_f_eq: "[| inj f; f x = y |] ==> inv f y = x"
   3.231 -by (simp add:inv_into_f_eq)
   3.232 +lemma inv_f_eq: "inj f \<Longrightarrow> f x = y \<Longrightarrow> inv f y = x"
   3.233 +  by (simp add:inv_into_f_eq)
   3.234  
   3.235 -lemma inj_imp_inv_eq: "[| inj f; ALL x. f(g x) = x |] ==> inv f = g"
   3.236 +lemma inj_imp_inv_eq: "inj f \<Longrightarrow> \<forall>x. f (g x) = x \<Longrightarrow> inv f = g"
   3.237    by (blast intro: inv_into_f_eq)
   3.238  
   3.239 -text\<open>But is it useful?\<close>
   3.240 +text \<open>But is it useful?\<close>
   3.241  lemma inj_transfer:
   3.242 -  assumes injf: "inj f" and minor: "!!y. y \<in> range(f) ==> P(inv f y)"
   3.243 +  assumes inj: "inj f"
   3.244 +    and minor: "\<And>y. y \<in> range f \<Longrightarrow> P (inv f y)"
   3.245    shows "P x"
   3.246  proof -
   3.247    have "f x \<in> range f" by auto
   3.248 -  hence "P(inv f (f x))" by (rule minor)
   3.249 -  thus "P x" by (simp add: inv_into_f_f [OF injf])
   3.250 +  then have "P(inv f (f x))" by (rule minor)
   3.251 +  then show "P x" by (simp add: inv_into_f_f [OF inj])
   3.252  qed
   3.253  
   3.254 -lemma inj_iff: "(inj f) = (inv f o f = id)"
   3.255 -apply (simp add: o_def fun_eq_iff)
   3.256 -apply (blast intro: inj_on_inverseI inv_into_f_f)
   3.257 -done
   3.258 +lemma inj_iff: "inj f \<longleftrightarrow> inv f \<circ> f = id"
   3.259 +  by (simp add: o_def fun_eq_iff) (blast intro: inj_on_inverseI inv_into_f_f)
   3.260  
   3.261 -lemma inv_o_cancel[simp]: "inj f ==> inv f o f = id"
   3.262 -by (simp add: inj_iff)
   3.263 +lemma inv_o_cancel[simp]: "inj f \<Longrightarrow> inv f \<circ> f = id"
   3.264 +  by (simp add: inj_iff)
   3.265 +
   3.266 +lemma o_inv_o_cancel[simp]: "inj f \<Longrightarrow> g \<circ> inv f \<circ> f = g"
   3.267 +  by (simp add: comp_assoc)
   3.268  
   3.269 -lemma o_inv_o_cancel[simp]: "inj f ==> g o inv f o f = g"
   3.270 -by (simp add: comp_assoc)
   3.271 +lemma inv_into_image_cancel[simp]: "inj_on f A \<Longrightarrow> S \<subseteq> A \<Longrightarrow> inv_into A f ` f ` S = S"
   3.272 +  by (fastforce simp: image_def)
   3.273  
   3.274 -lemma inv_into_image_cancel[simp]:
   3.275 -  "inj_on f A ==> S <= A ==> inv_into A f ` f ` S = S"
   3.276 -by(fastforce simp: image_def)
   3.277 +lemma inj_imp_surj_inv: "inj f \<Longrightarrow> surj (inv f)"
   3.278 +  by (blast intro!: surjI inv_into_f_f)
   3.279  
   3.280 -lemma inj_imp_surj_inv: "inj f ==> surj (inv f)"
   3.281 -by (blast intro!: surjI inv_into_f_f)
   3.282 -
   3.283 -lemma surj_f_inv_f: "surj f ==> f(inv f y) = y"
   3.284 -by (simp add: f_inv_into_f)
   3.285 +lemma surj_f_inv_f: "surj f \<Longrightarrow> f (inv f y) = y"
   3.286 +  by (simp add: f_inv_into_f)
   3.287  
   3.288  lemma inv_into_injective:
   3.289    assumes eq: "inv_into A f x = inv_into A f y"
   3.290 -      and x: "x: f`A"
   3.291 -      and y: "y: f`A"
   3.292 -  shows "x=y"
   3.293 +    and x: "x \<in> f`A"
   3.294 +    and y: "y \<in> f`A"
   3.295 +  shows "x = y"
   3.296  proof -
   3.297 -  have "f (inv_into A f x) = f (inv_into A f y)" using eq by simp
   3.298 -  thus ?thesis by (simp add: f_inv_into_f x y)
   3.299 +  from eq have "f (inv_into A f x) = f (inv_into A f y)"
   3.300 +    by simp
   3.301 +  with x y show ?thesis
   3.302 +    by (simp add: f_inv_into_f)
   3.303  qed
   3.304  
   3.305 -lemma inj_on_inv_into: "B <= f`A ==> inj_on (inv_into A f) B"
   3.306 -by (blast intro: inj_onI dest: inv_into_injective injD)
   3.307 +lemma inj_on_inv_into: "B \<subseteq> f`A \<Longrightarrow> inj_on (inv_into A f) B"
   3.308 +  by (blast intro: inj_onI dest: inv_into_injective injD)
   3.309  
   3.310 -lemma bij_betw_inv_into: "bij_betw f A B ==> bij_betw (inv_into A f) B A"
   3.311 -by (auto simp add: bij_betw_def inj_on_inv_into)
   3.312 +lemma bij_betw_inv_into: "bij_betw f A B \<Longrightarrow> bij_betw (inv_into A f) B A"
   3.313 +  by (auto simp add: bij_betw_def inj_on_inv_into)
   3.314  
   3.315 -lemma surj_imp_inj_inv: "surj f ==> inj (inv f)"
   3.316 -by (simp add: inj_on_inv_into)
   3.317 +lemma surj_imp_inj_inv: "surj f \<Longrightarrow> inj (inv f)"
   3.318 +  by (simp add: inj_on_inv_into)
   3.319  
   3.320 -lemma surj_iff: "(surj f) = (f o inv f = id)"
   3.321 -by (auto intro!: surjI simp: surj_f_inv_f fun_eq_iff[where 'b='a])
   3.322 +lemma surj_iff: "surj f \<longleftrightarrow> f \<circ> inv f = id"
   3.323 +  by (auto intro!: surjI simp: surj_f_inv_f fun_eq_iff[where 'b='a])
   3.324  
   3.325  lemma surj_iff_all: "surj f \<longleftrightarrow> (\<forall>x. f (inv f x) = x)"
   3.326 -  unfolding surj_iff by (simp add: o_def fun_eq_iff)
   3.327 +  by (simp add: o_def surj_iff fun_eq_iff)
   3.328  
   3.329 -lemma surj_imp_inv_eq: "[| surj f; \<forall>x. g(f x) = x |] ==> inv f = g"
   3.330 -apply (rule ext)
   3.331 -apply (drule_tac x = "inv f x" in spec)
   3.332 -apply (simp add: surj_f_inv_f)
   3.333 -done
   3.334 +lemma surj_imp_inv_eq: "surj f \<Longrightarrow> \<forall>x. g (f x) = x \<Longrightarrow> inv f = g"
   3.335 +  apply (rule ext)
   3.336 +  apply (drule_tac x = "inv f x" in spec)
   3.337 +  apply (simp add: surj_f_inv_f)
   3.338 +  done
   3.339  
   3.340 -lemma bij_imp_bij_inv: "bij f ==> bij (inv f)"
   3.341 -by (simp add: bij_def inj_imp_surj_inv surj_imp_inj_inv)
   3.342 +lemma bij_imp_bij_inv: "bij f \<Longrightarrow> bij (inv f)"
   3.343 +  by (simp add: bij_def inj_imp_surj_inv surj_imp_inj_inv)
   3.344  
   3.345 -lemma inv_equality: "[| !!x. g (f x) = x;  !!y. f (g y) = y |] ==> inv f = g"
   3.346 -apply (rule ext)
   3.347 -apply (auto simp add: inv_into_def)
   3.348 -done
   3.349 +lemma inv_equality: "(\<And>x. g (f x) = x) \<Longrightarrow> (\<And>y. f (g y) = y) \<Longrightarrow> inv f = g"
   3.350 +  by (rule ext) (auto simp add: inv_into_def)
   3.351 +
   3.352 +lemma inv_inv_eq: "bij f \<Longrightarrow> inv (inv f) = f"
   3.353 +  by (rule inv_equality) (auto simp add: bij_def surj_f_inv_f)
   3.354  
   3.355 -lemma inv_inv_eq: "bij f ==> inv (inv f) = f"
   3.356 -apply (rule inv_equality)
   3.357 -apply (auto simp add: bij_def surj_f_inv_f)
   3.358 -done
   3.359 -
   3.360 -(** bij(inv f) implies little about f.  Consider f::bool=>bool such that
   3.361 -    f(True)=f(False)=True.  Then it's consistent with axiom someI that
   3.362 -    inv f could be any function at all, including the identity function.
   3.363 -    If inv f=id then inv f is a bijection, but inj f, surj(f) and
   3.364 -    inv(inv f)=f all fail.
   3.365 -**)
   3.366 +text \<open>
   3.367 +  \<open>bij (inv f)\<close> implies little about \<open>f\<close>. Consider \<open>f :: bool \<Rightarrow> bool\<close> such
   3.368 +  that \<open>f True = f False = True\<close>. Then it ia consistent with axiom \<open>someI\<close>
   3.369 +  that \<open>inv f\<close> could be any function at all, including the identity function.
   3.370 +  If \<open>inv f = id\<close> then \<open>inv f\<close> is a bijection, but \<open>inj f\<close>, \<open>surj f\<close> and \<open>inv
   3.371 +  (inv f) = f\<close> all fail.
   3.372 +\<close>
   3.373  
   3.374  lemma inv_into_comp:
   3.375 -  "[| inj_on f (g ` A); inj_on g A; x : f ` g ` A |] ==>
   3.376 -  inv_into A (f o g) x = (inv_into A g o inv_into (g ` A) f) x"
   3.377 -apply (rule inv_into_f_eq)
   3.378 -  apply (fast intro: comp_inj_on)
   3.379 - apply (simp add: inv_into_into)
   3.380 -apply (simp add: f_inv_into_f inv_into_into)
   3.381 -done
   3.382 +  "inj_on f (g ` A) \<Longrightarrow> inj_on g A \<Longrightarrow> x \<in> f ` g ` A \<Longrightarrow>
   3.383 +    inv_into A (f \<circ> g) x = (inv_into A g \<circ> inv_into (g ` A) f) x"
   3.384 +  apply (rule inv_into_f_eq)
   3.385 +    apply (fast intro: comp_inj_on)
   3.386 +   apply (simp add: inv_into_into)
   3.387 +  apply (simp add: f_inv_into_f inv_into_into)
   3.388 +  done
   3.389  
   3.390 -lemma o_inv_distrib: "[| bij f; bij g |] ==> inv (f o g) = inv g o inv f"
   3.391 -apply (rule inv_equality)
   3.392 -apply (auto simp add: bij_def surj_f_inv_f)
   3.393 -done
   3.394 +lemma o_inv_distrib: "bij f \<Longrightarrow> bij g \<Longrightarrow> inv (f \<circ> g) = inv g \<circ> inv f"
   3.395 +  by (rule inv_equality) (auto simp add: bij_def surj_f_inv_f)
   3.396  
   3.397 -lemma image_surj_f_inv_f: "surj f ==> f ` (inv f ` A) = A"
   3.398 +lemma image_surj_f_inv_f: "surj f \<Longrightarrow> f ` (inv f ` A) = A"
   3.399    by (simp add: surj_f_inv_f image_comp comp_def)
   3.400  
   3.401 -lemma image_inv_f_f: "inj f ==> inv f ` (f ` A) = A"
   3.402 +lemma image_inv_f_f: "inj f \<Longrightarrow> inv f ` (f ` A) = A"
   3.403    by simp
   3.404  
   3.405 -lemma inv_image_comp: "inj f ==> inv f ` (f ` X) = X"
   3.406 +lemma inv_image_comp: "inj f \<Longrightarrow> inv f ` (f ` X) = X"
   3.407    by (fact image_inv_f_f)
   3.408  
   3.409 -lemma bij_image_Collect_eq: "bij f ==> f ` Collect P = {y. P (inv f y)}"
   3.410 -apply auto
   3.411 -apply (force simp add: bij_is_inj)
   3.412 -apply (blast intro: bij_is_surj [THEN surj_f_inv_f, symmetric])
   3.413 -done
   3.414 +lemma bij_image_Collect_eq: "bij f \<Longrightarrow> f ` Collect P = {y. P (inv f y)}"
   3.415 +  apply auto
   3.416 +   apply (force simp add: bij_is_inj)
   3.417 +  apply (blast intro: bij_is_surj [THEN surj_f_inv_f, symmetric])
   3.418 +  done
   3.419  
   3.420 -lemma bij_vimage_eq_inv_image: "bij f ==> f -` A = inv f ` A"
   3.421 -apply (auto simp add: bij_is_surj [THEN surj_f_inv_f])
   3.422 -apply (blast intro: bij_is_inj [THEN inv_into_f_f, symmetric])
   3.423 -done
   3.424 +lemma bij_vimage_eq_inv_image: "bij f \<Longrightarrow> f -` A = inv f ` A"
   3.425 +  apply (auto simp add: bij_is_surj [THEN surj_f_inv_f])
   3.426 +  apply (blast intro: bij_is_inj [THEN inv_into_f_f, symmetric])
   3.427 +  done
   3.428  
   3.429  lemma finite_fun_UNIVD1:
   3.430    assumes fin: "finite (UNIV :: ('a \<Rightarrow> 'b) set)"
   3.431 -  and card: "card (UNIV :: 'b set) \<noteq> Suc 0"
   3.432 +    and card: "card (UNIV :: 'b set) \<noteq> Suc 0"
   3.433    shows "finite (UNIV :: 'a set)"
   3.434  proof -
   3.435 -  from fin have finb: "finite (UNIV :: 'b set)" by (rule finite_fun_UNIVD2)
   3.436 +  from fin have finb: "finite (UNIV :: 'b set)"
   3.437 +    by (rule finite_fun_UNIVD2)
   3.438    with card have "card (UNIV :: 'b set) \<ge> Suc (Suc 0)"
   3.439      by (cases "card (UNIV :: 'b set)") (auto simp add: card_eq_0_iff)
   3.440 -  then obtain n where "card (UNIV :: 'b set) = Suc (Suc n)" "n = card (UNIV :: 'b set) - Suc (Suc 0)" by auto
   3.441 -  then obtain b1 b2 where b1b2: "(b1 :: 'b) \<noteq> (b2 :: 'b)" by (auto simp add: card_Suc_eq)
   3.442 -  from fin have "finite (range (\<lambda>f :: 'a \<Rightarrow> 'b. inv f b1))" by (rule finite_imageI)
   3.443 +  then obtain n where "card (UNIV :: 'b set) = Suc (Suc n)" "n = card (UNIV :: 'b set) - Suc (Suc 0)"
   3.444 +    by auto
   3.445 +  then obtain b1 b2 where b1b2: "(b1 :: 'b) \<noteq> (b2 :: 'b)"
   3.446 +    by (auto simp add: card_Suc_eq)
   3.447 +  from fin have "finite (range (\<lambda>f :: 'a \<Rightarrow> 'b. inv f b1))"
   3.448 +    by (rule finite_imageI)
   3.449    moreover have "UNIV = range (\<lambda>f :: 'a \<Rightarrow> 'b. inv f b1)"
   3.450    proof (rule UNIV_eq_I)
   3.451      fix x :: 'a
   3.452 -    from b1b2 have "x = inv (\<lambda>y. if y = x then b1 else b2) b1" by (simp add: inv_into_def)
   3.453 -    thus "x \<in> range (\<lambda>f::'a \<Rightarrow> 'b. inv f b1)" by blast
   3.454 +    from b1b2 have "x = inv (\<lambda>y. if y = x then b1 else b2) b1"
   3.455 +      by (simp add: inv_into_def)
   3.456 +    then show "x \<in> range (\<lambda>f::'a \<Rightarrow> 'b. inv f b1)"
   3.457 +      by blast
   3.458    qed
   3.459 -  ultimately show "finite (UNIV :: 'a set)" by simp
   3.460 +  ultimately show "finite (UNIV :: 'a set)"
   3.461 +    by simp
   3.462  qed
   3.463  
   3.464  text \<open>
   3.465 @@ -318,18 +311,18 @@
   3.466    define Sseq where "Sseq = rec_nat S (\<lambda>n T. T - {SOME e. e \<in> T})"
   3.467    define pick where "pick n = (SOME e. e \<in> Sseq n)" for n
   3.468    have *: "Sseq n \<subseteq> S" "\<not> finite (Sseq n)" for n
   3.469 -    by (induct n) (auto simp add: Sseq_def inf)
   3.470 +    by (induct n) (auto simp: Sseq_def inf)
   3.471    then have **: "\<And>n. pick n \<in> Sseq n"
   3.472      unfolding pick_def by (subst (asm) finite.simps) (auto simp add: ex_in_conv intro: someI_ex)
   3.473    with * have "range pick \<subseteq> S" by auto
   3.474 -  moreover
   3.475 -  {
   3.476 -    fix n m
   3.477 +  moreover have "pick n \<noteq> pick (n + Suc m)" for m n
   3.478 +  proof -
   3.479      have "pick n \<notin> Sseq (n + Suc m)"
   3.480        by (induct m) (auto simp add: Sseq_def pick_def)
   3.481 -    with ** have "pick n \<noteq> pick (n + Suc m)" by auto
   3.482 -  }
   3.483 -  then have "inj pick" by (intro linorder_injI) (auto simp add: less_iff_Suc_add)
   3.484 +    with ** show ?thesis by auto
   3.485 +  qed
   3.486 +  then have "inj pick"
   3.487 +    by (intro linorder_injI) (auto simp add: less_iff_Suc_add)
   3.488    ultimately show ?thesis by blast
   3.489  qed
   3.490  
   3.491 @@ -338,31 +331,35 @@
   3.492    using finite_imageD finite_subset infinite_UNIV_char_0 infinite_countable_subset by auto
   3.493  
   3.494  lemma image_inv_into_cancel:
   3.495 -  assumes SURJ: "f`A=A'" and SUB: "B' \<le> A'"
   3.496 +  assumes surj: "f`A = A'"
   3.497 +    and sub: "B' \<subseteq> A'"
   3.498    shows "f `((inv_into A f)`B') = B'"
   3.499    using assms
   3.500 -proof (auto simp add: f_inv_into_f)
   3.501 -  let ?f' = "(inv_into A f)"
   3.502 -  fix a' assume *: "a' \<in> B'"
   3.503 -  then have "a' \<in> A'" using SUB by auto
   3.504 -  then have "a' = f (?f' a')"
   3.505 -    using SURJ by (auto simp add: f_inv_into_f)
   3.506 -  then show "a' \<in> f ` (?f' ` B')" using * by blast
   3.507 +proof (auto simp: f_inv_into_f)
   3.508 +  let ?f' = "inv_into A f"
   3.509 +  fix a'
   3.510 +  assume *: "a' \<in> B'"
   3.511 +  with sub have "a' \<in> A'" by auto
   3.512 +  with surj have "a' = f (?f' a')"
   3.513 +    by (auto simp: f_inv_into_f)
   3.514 +  with * show "a' \<in> f ` (?f' ` B')" by blast
   3.515  qed
   3.516  
   3.517  lemma inv_into_inv_into_eq:
   3.518 -  assumes "bij_betw f A A'" "a \<in> A"
   3.519 +  assumes "bij_betw f A A'"
   3.520 +    and a: "a \<in> A"
   3.521    shows "inv_into A' (inv_into A f) a = f a"
   3.522  proof -
   3.523 -  let ?f' = "inv_into A f"   let ?f'' = "inv_into A' ?f'"
   3.524 -  have 1: "bij_betw ?f' A' A" using assms
   3.525 -  by (auto simp add: bij_betw_inv_into)
   3.526 -  obtain a' where 2: "a' \<in> A'" and 3: "?f' a' = a"
   3.527 -    using 1 \<open>a \<in> A\<close> unfolding bij_betw_def by force
   3.528 -  hence "?f'' a = a'"
   3.529 -    using \<open>a \<in> A\<close> 1 3 by (auto simp add: f_inv_into_f bij_betw_def)
   3.530 -  moreover have "f a = a'" using assms 2 3
   3.531 -    by (auto simp add: bij_betw_def)
   3.532 +  let ?f' = "inv_into A f"
   3.533 +  let ?f'' = "inv_into A' ?f'"
   3.534 +  from assms have *: "bij_betw ?f' A' A"
   3.535 +    by (auto simp: bij_betw_inv_into)
   3.536 +  with a obtain a' where a': "a' \<in> A'" "?f' a' = a"
   3.537 +    unfolding bij_betw_def by force
   3.538 +  with a * have "?f'' a = a'"
   3.539 +    by (auto simp: f_inv_into_f bij_betw_def)
   3.540 +  moreover from assms a' have "f a = a'"
   3.541 +    by (auto simp: bij_betw_def)
   3.542    ultimately show "?f'' a = f a" by simp
   3.543  qed
   3.544  
   3.545 @@ -370,72 +367,82 @@
   3.546    assumes "A \<noteq> {}"
   3.547    shows "(\<exists>f. inj_on f A \<and> f ` A \<le> A') \<longleftrightarrow> (\<exists>g. g ` A' = A)"
   3.548  proof safe
   3.549 -  fix f assume INJ: "inj_on f A" and INCL: "f ` A \<le> A'"
   3.550 -  let ?phi = "\<lambda>a' a. a \<in> A \<and> f a = a'"  let ?csi = "\<lambda>a. a \<in> A"
   3.551 +  fix f
   3.552 +  assume inj: "inj_on f A" and incl: "f ` A \<subseteq> A'"
   3.553 +  let ?phi = "\<lambda>a' a. a \<in> A \<and> f a = a'"
   3.554 +  let ?csi = "\<lambda>a. a \<in> A"
   3.555    let ?g = "\<lambda>a'. if a' \<in> f ` A then (SOME a. ?phi a' a) else (SOME a. ?csi a)"
   3.556    have "?g ` A' = A"
   3.557    proof
   3.558 -    show "?g ` A' \<le> A"
   3.559 +    show "?g ` A' \<subseteq> A"
   3.560      proof clarify
   3.561 -      fix a' assume *: "a' \<in> A'"
   3.562 +      fix a'
   3.563 +      assume *: "a' \<in> A'"
   3.564        show "?g a' \<in> A"
   3.565 -      proof cases
   3.566 -        assume Case1: "a' \<in> f ` A"
   3.567 +      proof (cases "a' \<in> f ` A")
   3.568 +        case True
   3.569          then obtain a where "?phi a' a" by blast
   3.570 -        hence "?phi a' (SOME a. ?phi a' a)" using someI[of "?phi a'" a] by blast
   3.571 -        with Case1 show ?thesis by auto
   3.572 +        then have "?phi a' (SOME a. ?phi a' a)"
   3.573 +          using someI[of "?phi a'" a] by blast
   3.574 +        with True show ?thesis by auto
   3.575        next
   3.576 -        assume Case2: "a' \<notin> f ` A"
   3.577 -        hence "?csi (SOME a. ?csi a)" using assms someI_ex[of ?csi] by blast
   3.578 -        with Case2 show ?thesis by auto
   3.579 +        case False
   3.580 +        with assms have "?csi (SOME a. ?csi a)"
   3.581 +          using someI_ex[of ?csi] by blast
   3.582 +        with False show ?thesis by auto
   3.583        qed
   3.584      qed
   3.585    next
   3.586 -    show "A \<le> ?g ` A'"
   3.587 -    proof-
   3.588 -      {fix a assume *: "a \<in> A"
   3.589 -       let ?b = "SOME aa. ?phi (f a) aa"
   3.590 -       have "?phi (f a) a" using * by auto
   3.591 -       hence 1: "?phi (f a) ?b" using someI[of "?phi(f a)" a] by blast
   3.592 -       hence "?g(f a) = ?b" using * by auto
   3.593 -       moreover have "a = ?b" using 1 INJ * by (auto simp add: inj_on_def)
   3.594 -       ultimately have "?g(f a) = a" by simp
   3.595 -       with INCL * have "?g(f a) = a \<and> f a \<in> A'" by auto
   3.596 -      }
   3.597 -      thus ?thesis by force
   3.598 +    show "A \<subseteq> ?g ` A'"
   3.599 +    proof -
   3.600 +      have "?g (f a) = a \<and> f a \<in> A'" if a: "a \<in> A" for a
   3.601 +      proof -
   3.602 +        let ?b = "SOME aa. ?phi (f a) aa"
   3.603 +        from a have "?phi (f a) a" by auto
   3.604 +        then have *: "?phi (f a) ?b"
   3.605 +          using someI[of "?phi(f a)" a] by blast
   3.606 +        then have "?g (f a) = ?b" using a by auto
   3.607 +        moreover from inj * a have "a = ?b"
   3.608 +          by (auto simp add: inj_on_def)
   3.609 +        ultimately have "?g(f a) = a" by simp
   3.610 +        with incl a show ?thesis by auto
   3.611 +      qed
   3.612 +      then show ?thesis by force
   3.613      qed
   3.614    qed
   3.615 -  thus "\<exists>g. g ` A' = A" by blast
   3.616 +  then show "\<exists>g. g ` A' = A" by blast
   3.617  next
   3.618 -  fix g  let ?f = "inv_into A' g"
   3.619 +  fix g
   3.620 +  let ?f = "inv_into A' g"
   3.621    have "inj_on ?f (g ` A')"
   3.622 -    by (auto simp add: inj_on_inv_into)
   3.623 -  moreover
   3.624 -  {fix a' assume *: "a' \<in> A'"
   3.625 -   let ?phi = "\<lambda> b'. b' \<in> A' \<and> g b' = g a'"
   3.626 -   have "?phi a'" using * by auto
   3.627 -   hence "?phi(SOME b'. ?phi b')" using someI[of ?phi] by blast
   3.628 -   hence "?f(g a') \<in> A'" unfolding inv_into_def by auto
   3.629 -  }
   3.630 -  ultimately show "\<exists>f. inj_on f (g ` A') \<and> f ` g ` A' \<subseteq> A'" by auto
   3.631 +    by (auto simp: inj_on_inv_into)
   3.632 +  moreover have "?f (g a') \<in> A'" if a': "a' \<in> A'" for a'
   3.633 +  proof -
   3.634 +    let ?phi = "\<lambda> b'. b' \<in> A' \<and> g b' = g a'"
   3.635 +    from a' have "?phi a'" by auto
   3.636 +    then have "?phi (SOME b'. ?phi b')"
   3.637 +      using someI[of ?phi] by blast
   3.638 +    then show ?thesis by (auto simp: inv_into_def)
   3.639 +  qed
   3.640 +  ultimately show "\<exists>f. inj_on f (g ` A') \<and> f ` g ` A' \<subseteq> A'"
   3.641 +    by auto
   3.642  qed
   3.643  
   3.644  lemma Ex_inj_on_UNION_Sigma:
   3.645    "\<exists>f. (inj_on f (\<Union>i \<in> I. A i) \<and> f ` (\<Union>i \<in> I. A i) \<le> (SIGMA i : I. A i))"
   3.646  proof
   3.647 -  let ?phi = "\<lambda> a i. i \<in> I \<and> a \<in> A i"
   3.648 -  let ?sm = "\<lambda> a. SOME i. ?phi a i"
   3.649 +  let ?phi = "\<lambda>a i. i \<in> I \<and> a \<in> A i"
   3.650 +  let ?sm = "\<lambda>a. SOME i. ?phi a i"
   3.651    let ?f = "\<lambda>a. (?sm a, a)"
   3.652 -  have "inj_on ?f (\<Union>i \<in> I. A i)" unfolding inj_on_def by auto
   3.653 +  have "inj_on ?f (\<Union>i \<in> I. A i)"
   3.654 +    by (auto simp: inj_on_def)
   3.655    moreover
   3.656 -  { { fix i a assume "i \<in> I" and "a \<in> A i"
   3.657 -      hence "?sm a \<in> I \<and> a \<in> A(?sm a)" using someI[of "?phi a" i] by auto
   3.658 -    }
   3.659 -    hence "?f ` (\<Union>i \<in> I. A i) \<le> (SIGMA i : I. A i)" by auto
   3.660 -  }
   3.661 -  ultimately
   3.662 -  show "inj_on ?f (\<Union>i \<in> I. A i) \<and> ?f ` (\<Union>i \<in> I. A i) \<le> (SIGMA i : I. A i)"
   3.663 -  by auto
   3.664 +  have "?sm a \<in> I \<and> a \<in> A(?sm a)" if "i \<in> I" and "a \<in> A i" for i a
   3.665 +    using that someI[of "?phi a" i] by auto
   3.666 +  then have "?f ` (\<Union>i \<in> I. A i) \<le> (SIGMA i : I. A i)"
   3.667 +    by auto
   3.668 +  ultimately show "inj_on ?f (\<Union>i \<in> I. A i) \<and> ?f ` (\<Union>i \<in> I. A i) \<le> (SIGMA i : I. A i)"
   3.669 +    by auto
   3.670  qed
   3.671  
   3.672  lemma inv_unique_comp:
   3.673 @@ -448,190 +455,199 @@
   3.674  subsection \<open>The Cantor-Bernstein Theorem\<close>
   3.675  
   3.676  lemma Cantor_Bernstein_aux:
   3.677 -  shows "\<exists>A' h. A' \<le> A \<and>
   3.678 -                (\<forall>a \<in> A'. a \<notin> g`(B - f ` A')) \<and>
   3.679 -                (\<forall>a \<in> A'. h a = f a) \<and>
   3.680 -                (\<forall>a \<in> A - A'. h a \<in> B - (f ` A') \<and> a = g(h a))"
   3.681 -proof-
   3.682 -  obtain H where H_def: "H = (\<lambda> A'. A - (g`(B - (f ` A'))))" by blast
   3.683 -  have 0: "mono H" unfolding mono_def H_def by blast
   3.684 -  then obtain A' where 1: "H A' = A'" using lfp_unfold by blast
   3.685 -  hence 2: "A' = A - (g`(B - (f ` A')))" unfolding H_def by simp
   3.686 -  hence 3: "A' \<le> A" by blast
   3.687 -  have 4: "\<forall>a \<in> A'.  a \<notin> g`(B - f ` A')"
   3.688 -  using 2 by blast
   3.689 -  have 5: "\<forall>a \<in> A - A'. \<exists>b \<in> B - (f ` A'). a = g b"
   3.690 -  using 2 by blast
   3.691 -  (*  *)
   3.692 -  obtain h where h_def:
   3.693 -  "h = (\<lambda> a. if a \<in> A' then f a else (SOME b. b \<in> B - (f ` A') \<and> a = g b))" by blast
   3.694 -  hence "\<forall>a \<in> A'. h a = f a" by auto
   3.695 -  moreover
   3.696 -  have "\<forall>a \<in> A - A'. h a \<in> B - (f ` A') \<and> a = g(h a)"
   3.697 +  "\<exists>A' h. A' \<subseteq> A \<and>
   3.698 +    (\<forall>a \<in> A'. a \<notin> g ` (B - f ` A')) \<and>
   3.699 +    (\<forall>a \<in> A'. h a = f a) \<and>
   3.700 +    (\<forall>a \<in> A - A'. h a \<in> B - (f ` A') \<and> a = g (h a))"
   3.701 +proof -
   3.702 +  define H where "H A' = A - (g ` (B - (f ` A')))" for A'
   3.703 +  have "mono H" unfolding mono_def H_def by blast
   3.704 +  from lfp_unfold [OF this] obtain A' where "H A' = A'" by blast
   3.705 +  then have "A' = A - (g ` (B - (f ` A')))" by (simp add: H_def)
   3.706 +  then have 1: "A' \<subseteq> A"
   3.707 +    and 2: "\<forall>a \<in> A'.  a \<notin> g ` (B - f ` A')"
   3.708 +    and 3: "\<forall>a \<in> A - A'. \<exists>b \<in> B - (f ` A'). a = g b"
   3.709 +    by blast+
   3.710 +  define h where "h a = (if a \<in> A' then f a else (SOME b. b \<in> B - (f ` A') \<and> a = g b))" for a
   3.711 +  then have 4: "\<forall>a \<in> A'. h a = f a" by simp
   3.712 +  have "\<forall>a \<in> A - A'. h a \<in> B - (f ` A') \<and> a = g (h a)"
   3.713    proof
   3.714 -    fix a assume *: "a \<in> A - A'"
   3.715 -    let ?phi = "\<lambda> b. b \<in> B - (f ` A') \<and> a = g b"
   3.716 -    have "h a = (SOME b. ?phi b)" using h_def * by auto
   3.717 -    moreover have "\<exists>b. ?phi b" using 5 *  by auto
   3.718 -    ultimately show  "?phi (h a)" using someI_ex[of ?phi] by auto
   3.719 +    fix a
   3.720 +    let ?phi = "\<lambda>b. b \<in> B - (f ` A') \<and> a = g b"
   3.721 +    assume *: "a \<in> A - A'"
   3.722 +    from * have "h a = (SOME b. ?phi b)" by (auto simp: h_def)
   3.723 +    moreover from 3 * have "\<exists>b. ?phi b" by auto
   3.724 +    ultimately show "?phi (h a)"
   3.725 +      using someI_ex[of ?phi] by auto
   3.726    qed
   3.727 -  ultimately show ?thesis using 3 4 by blast
   3.728 +  with 1 2 4 show ?thesis by blast
   3.729  qed
   3.730  
   3.731  theorem Cantor_Bernstein:
   3.732 -  assumes INJ1: "inj_on f A" and SUB1: "f ` A \<le> B" and
   3.733 -          INJ2: "inj_on g B" and SUB2: "g ` B \<le> A"
   3.734 +  assumes inj1: "inj_on f A" and sub1: "f ` A \<subseteq> B"
   3.735 +    and inj2: "inj_on g B" and sub2: "g ` B \<subseteq> A"
   3.736    shows "\<exists>h. bij_betw h A B"
   3.737  proof-
   3.738 -  obtain A' and h where 0: "A' \<le> A" and
   3.739 -  1: "\<forall>a \<in> A'. a \<notin> g`(B - f ` A')" and
   3.740 -  2: "\<forall>a \<in> A'. h a = f a" and
   3.741 -  3: "\<forall>a \<in> A - A'. h a \<in> B - (f ` A') \<and> a = g(h a)"
   3.742 -  using Cantor_Bernstein_aux[of A g B f] by blast
   3.743 +  obtain A' and h where "A' \<subseteq> A"
   3.744 +    and 1: "\<forall>a \<in> A'. a \<notin> g ` (B - f ` A')"
   3.745 +    and 2: "\<forall>a \<in> A'. h a = f a"
   3.746 +    and 3: "\<forall>a \<in> A - A'. h a \<in> B - (f ` A') \<and> a = g (h a)"
   3.747 +    using Cantor_Bernstein_aux [of A g B f] by blast
   3.748    have "inj_on h A"
   3.749    proof (intro inj_onI)
   3.750      fix a1 a2
   3.751      assume 4: "a1 \<in> A" and 5: "a2 \<in> A" and 6: "h a1 = h a2"
   3.752      show "a1 = a2"
   3.753 -    proof(cases "a1 \<in> A'")
   3.754 -      assume Case1: "a1 \<in> A'"
   3.755 +    proof (cases "a1 \<in> A'")
   3.756 +      case True
   3.757        show ?thesis
   3.758 -      proof(cases "a2 \<in> A'")
   3.759 -        assume Case11: "a2 \<in> A'"
   3.760 -        hence "f a1 = f a2" using Case1 2 6 by auto
   3.761 -        thus ?thesis using INJ1 Case1 Case11 0
   3.762 -        unfolding inj_on_def by blast
   3.763 +      proof (cases "a2 \<in> A'")
   3.764 +        case True': True
   3.765 +        with True 2 6 have "f a1 = f a2" by auto
   3.766 +        with inj1 \<open>A' \<subseteq> A\<close> True True' show ?thesis
   3.767 +          unfolding inj_on_def by blast
   3.768        next
   3.769 -        assume Case12: "a2 \<notin> A'"
   3.770 -        hence False using 3 5 2 6 Case1 by force
   3.771 -        thus ?thesis by simp
   3.772 +        case False
   3.773 +        with 2 3 5 6 True have False by force
   3.774 +        then show ?thesis ..
   3.775        qed
   3.776      next
   3.777 -    assume Case2: "a1 \<notin> A'"
   3.778 +      case False
   3.779        show ?thesis
   3.780 -      proof(cases "a2 \<in> A'")
   3.781 -        assume Case21: "a2 \<in> A'"
   3.782 -        hence False using 3 4 2 6 Case2 by auto
   3.783 -        thus ?thesis by simp
   3.784 +      proof (cases "a2 \<in> A'")
   3.785 +        case True
   3.786 +        with 2 3 4 6 False have False by auto
   3.787 +        then show ?thesis ..
   3.788        next
   3.789 -        assume Case22: "a2 \<notin> A'"
   3.790 -        hence "a1 = g(h a1) \<and> a2 = g(h a2)" using Case2 4 5 3 by auto
   3.791 -        thus ?thesis using 6 by simp
   3.792 +        case False': False
   3.793 +        with False 3 4 5 have "a1 = g (h a1)" "a2 = g (h a2)" by auto
   3.794 +        with 6 show ?thesis by simp
   3.795        qed
   3.796      qed
   3.797    qed
   3.798 -  (*  *)
   3.799 -  moreover
   3.800 -  have "h ` A = B"
   3.801 +  moreover have "h ` A = B"
   3.802    proof safe
   3.803 -    fix a assume "a \<in> A"
   3.804 -    thus "h a \<in> B" using SUB1 2 3 by (cases "a \<in> A'") auto
   3.805 +    fix a
   3.806 +    assume "a \<in> A"
   3.807 +    with sub1 2 3 show "h a \<in> B" by (cases "a \<in> A'") auto
   3.808    next
   3.809 -    fix b assume *: "b \<in> B"
   3.810 +    fix b
   3.811 +    assume *: "b \<in> B"
   3.812      show "b \<in> h ` A"
   3.813 -    proof(cases "b \<in> f ` A'")
   3.814 -      assume Case1: "b \<in> f ` A'"
   3.815 -      then obtain a where "a \<in> A' \<and> b = f a" by blast
   3.816 -      thus ?thesis using 2 0 by force
   3.817 +    proof (cases "b \<in> f ` A'")
   3.818 +      case True
   3.819 +      then obtain a where "a \<in> A'" "b = f a" by blast
   3.820 +      with \<open>A' \<subseteq> A\<close> 2 show ?thesis by force
   3.821      next
   3.822 -      assume Case2: "b \<notin> f ` A'"
   3.823 -      hence "g b \<notin> A'" using 1 * by auto
   3.824 -      hence 4: "g b \<in> A - A'" using * SUB2 by auto
   3.825 -      hence "h(g b) \<in> B \<and> g(h(g b)) = g b"
   3.826 -      using 3 by auto
   3.827 -      hence "h(g b) = b" using * INJ2 unfolding inj_on_def by auto
   3.828 -      thus ?thesis using 4 by force
   3.829 +      case False
   3.830 +      with 1 * have "g b \<notin> A'" by auto
   3.831 +      with sub2 * have 4: "g b \<in> A - A'" by auto
   3.832 +      with 3 have "h (g b) \<in> B" "g (h (g b)) = g b" by auto
   3.833 +      with inj2 * have "h (g b) = b" by (auto simp: inj_on_def)
   3.834 +      with 4 show ?thesis by force
   3.835      qed
   3.836    qed
   3.837 -  (*  *)
   3.838 -  ultimately show ?thesis unfolding bij_betw_def by auto
   3.839 +  ultimately show ?thesis
   3.840 +    by (auto simp: bij_betw_def)
   3.841  qed
   3.842  
   3.843 +
   3.844  subsection \<open>Other Consequences of Hilbert's Epsilon\<close>
   3.845  
   3.846  text \<open>Hilbert's Epsilon and the @{term split} Operator\<close>
   3.847  
   3.848 -text\<open>Looping simprule\<close>
   3.849 -lemma split_paired_Eps: "(SOME x. P x) = (SOME (a,b). P(a,b))"
   3.850 +text \<open>Looping simprule!\<close>
   3.851 +lemma split_paired_Eps: "(SOME x. P x) = (SOME (a, b). P (a, b))"
   3.852    by simp
   3.853  
   3.854  lemma Eps_case_prod: "Eps (case_prod P) = (SOME xy. P (fst xy) (snd xy))"
   3.855    by (simp add: split_def)
   3.856  
   3.857 -lemma Eps_case_prod_eq [simp]: "(@(x',y'). x = x' & y = y') = (x,y)"
   3.858 +lemma Eps_case_prod_eq [simp]: "(SOME (x', y'). x = x' \<and> y = y') = (x, y)"
   3.859    by blast
   3.860  
   3.861  
   3.862 -text\<open>A relation is wellfounded iff it has no infinite descending chain\<close>
   3.863 -lemma wf_iff_no_infinite_down_chain:
   3.864 -  "wf r = (~(\<exists>f. \<forall>i. (f(Suc i),f i) \<in> r))"
   3.865 -apply (simp only: wf_eq_minimal)
   3.866 -apply (rule iffI)
   3.867 - apply (rule notI)
   3.868 - apply (erule exE)
   3.869 - apply (erule_tac x = "{w. \<exists>i. w=f i}" in allE, blast)
   3.870 -apply (erule contrapos_np, simp, clarify)
   3.871 -apply (subgoal_tac "\<forall>n. rec_nat x (%i y. @z. z:Q & (z,y) :r) n \<in> Q")
   3.872 - apply (rule_tac x = "rec_nat x (%i y. @z. z:Q & (z,y) :r)" in exI)
   3.873 - apply (rule allI, simp)
   3.874 - apply (rule someI2_ex, blast, blast)
   3.875 -apply (rule allI)
   3.876 -apply (induct_tac "n", simp_all)
   3.877 -apply (rule someI2_ex, blast+)
   3.878 -done
   3.879 +text \<open>A relation is wellfounded iff it has no infinite descending chain.\<close>
   3.880 +lemma wf_iff_no_infinite_down_chain: "wf r \<longleftrightarrow> (\<not> (\<exists>f. \<forall>i. (f (Suc i), f i) \<in> r))"
   3.881 +  apply (simp only: wf_eq_minimal)
   3.882 +  apply (rule iffI)
   3.883 +   apply (rule notI)
   3.884 +   apply (erule exE)
   3.885 +   apply (erule_tac x = "{w. \<exists>i. w = f i}" in allE)
   3.886 +   apply blast
   3.887 +  apply (erule contrapos_np)
   3.888 +  apply simp
   3.889 +  apply clarify
   3.890 +  apply (subgoal_tac "\<forall>n. rec_nat x (\<lambda>i y. SOME z. z \<in> Q \<and> (z, y) \<in> r) n \<in> Q")
   3.891 +   apply (rule_tac x = "rec_nat x (\<lambda>i y. SOME z. z \<in> Q \<and> (z, y) \<in> r)" in exI)
   3.892 +   apply (rule allI)
   3.893 +   apply simp
   3.894 +   apply (rule someI2_ex)
   3.895 +    apply blast
   3.896 +   apply blast
   3.897 +  apply (rule allI)
   3.898 +  apply (induct_tac n)
   3.899 +   apply simp_all
   3.900 +  apply (rule someI2_ex)
   3.901 +   apply blast
   3.902 +  apply blast
   3.903 +  done
   3.904  
   3.905  lemma wf_no_infinite_down_chainE:
   3.906 -  assumes "wf r" obtains k where "(f (Suc k), f k) \<notin> r"
   3.907 -using \<open>wf r\<close> wf_iff_no_infinite_down_chain[of r] by blast
   3.908 +  assumes "wf r"
   3.909 +  obtains k where "(f (Suc k), f k) \<notin> r"
   3.910 +  using assms wf_iff_no_infinite_down_chain[of r] by blast
   3.911  
   3.912  
   3.913 -text\<open>A dynamically-scoped fact for TFL\<close>
   3.914 -lemma tfl_some: "\<forall>P x. P x --> P (Eps P)"
   3.915 +text \<open>A dynamically-scoped fact for TFL\<close>
   3.916 +lemma tfl_some: "\<forall>P x. P x \<longrightarrow> P (Eps P)"
   3.917    by (blast intro: someI)
   3.918  
   3.919  
   3.920  subsection \<open>Least value operator\<close>
   3.921  
   3.922 -definition
   3.923 -  LeastM :: "['a => 'b::ord, 'a => bool] => 'a" where
   3.924 -  "LeastM m P == SOME x. P x & (\<forall>y. P y --> m x <= m y)"
   3.925 +definition LeastM :: "('a \<Rightarrow> 'b::ord) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a"
   3.926 +  where "LeastM m P \<equiv> (SOME x. P x \<and> (\<forall>y. P y \<longrightarrow> m x \<le> m y))"
   3.927  
   3.928  syntax
   3.929 -  "_LeastM" :: "[pttrn, 'a => 'b::ord, bool] => 'a"    ("LEAST _ WRT _. _" [0, 4, 10] 10)
   3.930 +  "_LeastM" :: "pttrn \<Rightarrow> ('a \<Rightarrow> 'b::ord) \<Rightarrow> bool \<Rightarrow> 'a"  ("LEAST _ WRT _. _" [0, 4, 10] 10)
   3.931  translations
   3.932 -  "LEAST x WRT m. P" == "CONST LeastM m (%x. P)"
   3.933 +  "LEAST x WRT m. P" \<rightleftharpoons> "CONST LeastM m (\<lambda>x. P)"
   3.934  
   3.935  lemma LeastMI2:
   3.936 -  "P x ==> (!!y. P y ==> m x <= m y)
   3.937 -    ==> (!!x. P x ==> \<forall>y. P y --> m x \<le> m y ==> Q x)
   3.938 -    ==> Q (LeastM m P)"
   3.939 +  "P x \<Longrightarrow>
   3.940 +    (\<And>y. P y \<Longrightarrow> m x \<le> m y) \<Longrightarrow>
   3.941 +    (\<And>x. P x \<Longrightarrow> \<forall>y. P y \<longrightarrow> m x \<le> m y \<Longrightarrow> Q x) \<Longrightarrow>
   3.942 +    Q (LeastM m P)"
   3.943    apply (simp add: LeastM_def)
   3.944 -  apply (rule someI2_ex, blast, blast)
   3.945 +  apply (rule someI2_ex)
   3.946 +   apply blast
   3.947 +  apply blast
   3.948    done
   3.949  
   3.950  lemma LeastM_equality:
   3.951 -  "P k ==> (!!x. P x ==> m k <= m x)
   3.952 -    ==> m (LEAST x WRT m. P x) = (m k::'a::order)"
   3.953 -  apply (rule LeastMI2, assumption, blast)
   3.954 +  "P k \<Longrightarrow> (\<And>x. P x \<Longrightarrow> m k \<le> m x) \<Longrightarrow> m (LEAST x WRT m. P x) = (m k :: 'a::order)"
   3.955 +  apply (rule LeastMI2)
   3.956 +    apply assumption
   3.957 +   apply blast
   3.958    apply (blast intro!: order_antisym)
   3.959    done
   3.960  
   3.961  lemma wf_linord_ex_has_least:
   3.962 -  "wf r ==> \<forall>x y. ((x,y):r^+) = ((y,x)~:r^*) ==> P k
   3.963 -    ==> \<exists>x. P x & (!y. P y --> (m x,m y):r^*)"
   3.964 +  "wf r \<Longrightarrow> \<forall>x y. (x, y) \<in> r\<^sup>+ \<longleftrightarrow> (y, x) \<notin> r\<^sup>* \<Longrightarrow> P k \<Longrightarrow> \<exists>x. P x \<and> (\<forall>y. P y \<longrightarrow> (m x, m y) \<in> r\<^sup>*)"
   3.965    apply (drule wf_trancl [THEN wf_eq_minimal [THEN iffD1]])
   3.966 -  apply (drule_tac x = "m`Collect P" in spec, force)
   3.967 +  apply (drule_tac x = "m ` Collect P" in spec)
   3.968 +  apply force
   3.969    done
   3.970  
   3.971 -lemma ex_has_least_nat:
   3.972 -    "P k ==> \<exists>x. P x & (\<forall>y. P y --> m x <= (m y::nat))"
   3.973 +lemma ex_has_least_nat: "P k \<Longrightarrow> \<exists>x. P x \<and> (\<forall>y. P y \<longrightarrow> m x \<le> (m y :: nat))"
   3.974    apply (simp only: pred_nat_trancl_eq_le [symmetric])
   3.975    apply (rule wf_pred_nat [THEN wf_linord_ex_has_least])
   3.976 -   apply (simp add: less_eq linorder_not_le pred_nat_trancl_eq_le, assumption)
   3.977 +   apply (simp add: less_eq linorder_not_le pred_nat_trancl_eq_le)
   3.978 +  apply assumption
   3.979    done
   3.980  
   3.981 -lemma LeastM_nat_lemma:
   3.982 -    "P k ==> P (LeastM m P) & (\<forall>y. P y --> m (LeastM m P) <= (m y::nat))"
   3.983 +lemma LeastM_nat_lemma: "P k \<Longrightarrow> P (LeastM m P) \<and> (\<forall>y. P y \<longrightarrow> m (LeastM m P) \<le> (m y :: nat))"
   3.984    apply (simp add: LeastM_def)
   3.985    apply (rule someI_ex)
   3.986    apply (erule ex_has_least_nat)
   3.987 @@ -639,91 +655,87 @@
   3.988  
   3.989  lemmas LeastM_natI = LeastM_nat_lemma [THEN conjunct1]
   3.990  
   3.991 -lemma LeastM_nat_le: "P x ==> m (LeastM m P) <= (m x::nat)"
   3.992 -by (rule LeastM_nat_lemma [THEN conjunct2, THEN spec, THEN mp], assumption, assumption)
   3.993 +lemma LeastM_nat_le: "P x \<Longrightarrow> m (LeastM m P) \<le> (m x :: nat)"
   3.994 +  by (rule LeastM_nat_lemma [THEN conjunct2, THEN spec, THEN mp])
   3.995  
   3.996  
   3.997  subsection \<open>Greatest value operator\<close>
   3.998  
   3.999 -definition
  3.1000 -  GreatestM :: "['a => 'b::ord, 'a => bool] => 'a" where
  3.1001 -  "GreatestM m P == SOME x. P x & (\<forall>y. P y --> m y <= m x)"
  3.1002 +definition GreatestM :: "('a \<Rightarrow> 'b::ord) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a"
  3.1003 +  where "GreatestM m P \<equiv> SOME x. P x \<and> (\<forall>y. P y \<longrightarrow> m y \<le> m x)"
  3.1004  
  3.1005 -definition
  3.1006 -  Greatest :: "('a::ord => bool) => 'a" (binder "GREATEST " 10) where
  3.1007 -  "Greatest == GreatestM (%x. x)"
  3.1008 +definition Greatest :: "('a::ord \<Rightarrow> bool) \<Rightarrow> 'a"  (binder "GREATEST " 10)
  3.1009 +  where "Greatest \<equiv> GreatestM (\<lambda>x. x)"
  3.1010  
  3.1011  syntax
  3.1012 -  "_GreatestM" :: "[pttrn, 'a => 'b::ord, bool] => 'a"
  3.1013 -      ("GREATEST _ WRT _. _" [0, 4, 10] 10)
  3.1014 +  "_GreatestM" :: "pttrn \<Rightarrow> ('a \<Rightarrow> 'b::ord) \<Rightarrow> bool \<Rightarrow> 'a"  ("GREATEST _ WRT _. _" [0, 4, 10] 10)
  3.1015  translations
  3.1016 -  "GREATEST x WRT m. P" == "CONST GreatestM m (%x. P)"
  3.1017 +  "GREATEST x WRT m. P" \<rightleftharpoons> "CONST GreatestM m (\<lambda>x. P)"
  3.1018  
  3.1019  lemma GreatestMI2:
  3.1020 -  "P x ==> (!!y. P y ==> m y <= m x)
  3.1021 -    ==> (!!x. P x ==> \<forall>y. P y --> m y \<le> m x ==> Q x)
  3.1022 -    ==> Q (GreatestM m P)"
  3.1023 +  "P x \<Longrightarrow>
  3.1024 +    (\<And>y. P y \<Longrightarrow> m y \<le> m x) \<Longrightarrow>
  3.1025 +    (\<And>x. P x \<Longrightarrow> \<forall>y. P y \<longrightarrow> m y \<le> m x \<Longrightarrow> Q x) \<Longrightarrow>
  3.1026 +    Q (GreatestM m P)"
  3.1027    apply (simp add: GreatestM_def)
  3.1028 -  apply (rule someI2_ex, blast, blast)
  3.1029 +  apply (rule someI2_ex)
  3.1030 +   apply blast
  3.1031 +  apply blast
  3.1032    done
  3.1033  
  3.1034  lemma GreatestM_equality:
  3.1035 - "P k ==> (!!x. P x ==> m x <= m k)
  3.1036 -    ==> m (GREATEST x WRT m. P x) = (m k::'a::order)"
  3.1037 -  apply (rule_tac m = m in GreatestMI2, assumption, blast)
  3.1038 +  "P k \<Longrightarrow>
  3.1039 +    (\<And>x. P x \<Longrightarrow> m x \<le> m k) \<Longrightarrow>
  3.1040 +    m (GREATEST x WRT m. P x) = (m k :: 'a::order)"
  3.1041 +  apply (rule GreatestMI2 [where m = m])
  3.1042 +    apply assumption
  3.1043 +   apply blast
  3.1044    apply (blast intro!: order_antisym)
  3.1045    done
  3.1046  
  3.1047 -lemma Greatest_equality:
  3.1048 -  "P (k::'a::order) ==> (!!x. P x ==> x <= k) ==> (GREATEST x. P x) = k"
  3.1049 +lemma Greatest_equality: "P k \<Longrightarrow> (\<And>x. P x \<Longrightarrow> x \<le> k) \<Longrightarrow> (GREATEST x. P x) = k"
  3.1050 +  for k :: "'a::order"
  3.1051    apply (simp add: Greatest_def)
  3.1052 -  apply (erule GreatestM_equality, blast)
  3.1053 +  apply (erule GreatestM_equality)
  3.1054 +  apply blast
  3.1055    done
  3.1056  
  3.1057  lemma ex_has_greatest_nat_lemma:
  3.1058 -  "P k ==> \<forall>x. P x --> (\<exists>y. P y & ~ ((m y::nat) <= m x))
  3.1059 -    ==> \<exists>y. P y & ~ (m y < m k + n)"
  3.1060 -  apply (induct n, force)
  3.1061 -  apply (force simp add: le_Suc_eq)
  3.1062 -  done
  3.1063 +  "P k \<Longrightarrow> \<forall>x. P x \<longrightarrow> (\<exists>y. P y \<and> \<not> m y \<le> (m x :: nat)) \<Longrightarrow> \<exists>y. P y \<and> \<not> m y < m k + n"
  3.1064 +  by (induct n) (force simp: le_Suc_eq)+
  3.1065  
  3.1066  lemma ex_has_greatest_nat:
  3.1067 -  "P k ==> \<forall>y. P y --> m y < b
  3.1068 -    ==> \<exists>x. P x & (\<forall>y. P y --> (m y::nat) <= m x)"
  3.1069 +  "P k \<Longrightarrow> \<forall>y. P y \<longrightarrow> m y < b \<Longrightarrow> \<exists>x. P x \<and> (\<forall>y. P y \<longrightarrow> m y \<le> (m x :: nat))"
  3.1070    apply (rule ccontr)
  3.1071    apply (cut_tac P = P and n = "b - m k" in ex_has_greatest_nat_lemma)
  3.1072 -    apply (subgoal_tac [3] "m k <= b", auto)
  3.1073 +    apply (subgoal_tac [3] "m k \<le> b")
  3.1074 +     apply auto
  3.1075    done
  3.1076  
  3.1077  lemma GreatestM_nat_lemma:
  3.1078 -  "P k ==> \<forall>y. P y --> m y < b
  3.1079 -    ==> P (GreatestM m P) & (\<forall>y. P y --> (m y::nat) <= m (GreatestM m P))"
  3.1080 +  "P k \<Longrightarrow> \<forall>y. P y \<longrightarrow> m y < b \<Longrightarrow>
  3.1081 +    P (GreatestM m P) \<and> (\<forall>y. P y \<longrightarrow> (m y :: nat) \<le> m (GreatestM m P))"
  3.1082    apply (simp add: GreatestM_def)
  3.1083    apply (rule someI_ex)
  3.1084 -  apply (erule ex_has_greatest_nat, assumption)
  3.1085 +  apply (erule ex_has_greatest_nat)
  3.1086 +  apply assumption
  3.1087    done
  3.1088  
  3.1089  lemmas GreatestM_natI = GreatestM_nat_lemma [THEN conjunct1]
  3.1090  
  3.1091 -lemma GreatestM_nat_le:
  3.1092 -  "P x ==> \<forall>y. P y --> m y < b
  3.1093 -    ==> (m x::nat) <= m (GreatestM m P)"
  3.1094 -  apply (blast dest: GreatestM_nat_lemma [THEN conjunct2, THEN spec, of P])
  3.1095 -  done
  3.1096 +lemma GreatestM_nat_le: "P x \<Longrightarrow> \<forall>y. P y \<longrightarrow> m y < b \<Longrightarrow> (m x :: nat) \<le> m (GreatestM m P)"
  3.1097 +  by (blast dest: GreatestM_nat_lemma [THEN conjunct2, THEN spec, of P])
  3.1098  
  3.1099  
  3.1100 -text \<open>\medskip Specialization to \<open>GREATEST\<close>.\<close>
  3.1101 +text \<open>\<^medskip> Specialization to \<open>GREATEST\<close>.\<close>
  3.1102  
  3.1103 -lemma GreatestI: "P (k::nat) ==> \<forall>y. P y --> y < b ==> P (GREATEST x. P x)"
  3.1104 -  apply (simp add: Greatest_def)
  3.1105 -  apply (rule GreatestM_natI, auto)
  3.1106 -  done
  3.1107 +lemma GreatestI: "P k \<Longrightarrow> \<forall>y. P y \<longrightarrow> y < b \<Longrightarrow> P (GREATEST x. P x)"
  3.1108 +  for k :: nat
  3.1109 +  unfolding Greatest_def by (rule GreatestM_natI) auto
  3.1110  
  3.1111 -lemma Greatest_le:
  3.1112 -    "P x ==> \<forall>y. P y --> y < b ==> (x::nat) <= (GREATEST x. P x)"
  3.1113 -  apply (simp add: Greatest_def)
  3.1114 -  apply (rule GreatestM_nat_le, auto)
  3.1115 -  done
  3.1116 +lemma Greatest_le: "P x \<Longrightarrow> \<forall>y. P y \<longrightarrow> y < b \<Longrightarrow> x \<le> (GREATEST x. P x)"
  3.1117 +  for x :: nat
  3.1118 +  unfolding Greatest_def by (rule GreatestM_nat_le) auto
  3.1119  
  3.1120  
  3.1121  subsection \<open>An aside: bounded accessible part\<close>
  3.1122 @@ -732,7 +744,8 @@
  3.1123  
  3.1124  lemma finite_mono_remains_stable_implies_strict_prefix:
  3.1125    fixes f :: "nat \<Rightarrow> 'a::order"
  3.1126 -  assumes S: "finite (range f)" "mono f" and eq: "\<forall>n. f n = f (Suc n) \<longrightarrow> f (Suc n) = f (Suc (Suc n))"
  3.1127 +  assumes S: "finite (range f)" "mono f"
  3.1128 +    and eq: "\<forall>n. f n = f (Suc n) \<longrightarrow> f (Suc n) = f (Suc (Suc n))"
  3.1129    shows "\<exists>N. (\<forall>n\<le>N. \<forall>m\<le>N. m < n \<longrightarrow> f m < f n) \<and> (\<forall>n\<ge>N. f N = f n)"
  3.1130    using assms
  3.1131  proof -
  3.1132 @@ -740,15 +753,16 @@
  3.1133    proof (rule ccontr)
  3.1134      assume "\<not> ?thesis"
  3.1135      then have "\<And>n. f n \<noteq> f (Suc n)" by auto
  3.1136 -    then have "\<And>n. f n < f (Suc n)"
  3.1137 -      using  \<open>mono f\<close> by (auto simp: le_less mono_iff_le_Suc)
  3.1138 -    with lift_Suc_mono_less_iff[of f]
  3.1139 -    have *: "\<And>n m. n < m \<Longrightarrow> f n < f m" by auto
  3.1140 +    with \<open>mono f\<close> have "\<And>n. f n < f (Suc n)"
  3.1141 +      by (auto simp: le_less mono_iff_le_Suc)
  3.1142 +    with lift_Suc_mono_less_iff[of f] have *: "\<And>n m. n < m \<Longrightarrow> f n < f m"
  3.1143 +      by auto
  3.1144      have "inj f"
  3.1145      proof (intro injI)
  3.1146        fix x y
  3.1147        assume "f x = f y"
  3.1148 -      then show "x = y" by (cases x y rule: linorder_cases) (auto dest: *)
  3.1149 +      then show "x = y"
  3.1150 +        by (cases x y rule: linorder_cases) (auto dest: *)
  3.1151      qed
  3.1152      with \<open>finite (range f)\<close> have "finite (UNIV::nat set)"
  3.1153        by (rule finite_imageD)
  3.1154 @@ -760,16 +774,22 @@
  3.1155      unfolding N_def using n by (rule LeastI)
  3.1156    show ?thesis
  3.1157    proof (intro exI[of _ N] conjI allI impI)
  3.1158 -    fix n assume "N \<le> n"
  3.1159 +    fix n
  3.1160 +    assume "N \<le> n"
  3.1161      then have "\<And>m. N \<le> m \<Longrightarrow> m \<le> n \<Longrightarrow> f m = f N"
  3.1162      proof (induct rule: dec_induct)
  3.1163 -      case (step n) then show ?case
  3.1164 -        using eq[rule_format, of "n - 1"] N
  3.1165 +      case base
  3.1166 +      then show ?case by simp
  3.1167 +    next
  3.1168 +      case (step n)
  3.1169 +      then show ?case
  3.1170 +        using eq [rule_format, of "n - 1"] N
  3.1171          by (cases n) (auto simp add: le_Suc_eq)
  3.1172 -    qed simp
  3.1173 +    qed
  3.1174      from this[of n] \<open>N \<le> n\<close> show "f N = f n" by auto
  3.1175    next
  3.1176 -    fix n m :: nat assume "m < n" "n \<le> N"
  3.1177 +    fix n m :: nat
  3.1178 +    assume "m < n" "n \<le> N"
  3.1179      then show "f m < f n"
  3.1180      proof (induct rule: less_Suc_induct)
  3.1181        case (1 i)
  3.1182 @@ -777,37 +797,41 @@
  3.1183        then have "f i \<noteq> f (Suc i)"
  3.1184          unfolding N_def by (rule not_less_Least)
  3.1185        with \<open>mono f\<close> show ?case by (simp add: mono_iff_le_Suc less_le)
  3.1186 -    qed auto
  3.1187 +    next
  3.1188 +      case 2
  3.1189 +      then show ?case by simp
  3.1190 +    qed
  3.1191    qed
  3.1192  qed
  3.1193  
  3.1194  lemma finite_mono_strict_prefix_implies_finite_fixpoint:
  3.1195    fixes f :: "nat \<Rightarrow> 'a set"
  3.1196    assumes S: "\<And>i. f i \<subseteq> S" "finite S"
  3.1197 -    and inj: "\<exists>N. (\<forall>n\<le>N. \<forall>m\<le>N. m < n \<longrightarrow> f m \<subset> f n) \<and> (\<forall>n\<ge>N. f N = f n)"
  3.1198 +    and ex: "\<exists>N. (\<forall>n\<le>N. \<forall>m\<le>N. m < n \<longrightarrow> f m \<subset> f n) \<and> (\<forall>n\<ge>N. f N = f n)"
  3.1199    shows "f (card S) = (\<Union>n. f n)"
  3.1200  proof -
  3.1201 -  from inj obtain N where inj: "(\<forall>n\<le>N. \<forall>m\<le>N. m < n \<longrightarrow> f m \<subset> f n)" and eq: "(\<forall>n\<ge>N. f N = f n)" by auto
  3.1202 -
  3.1203 -  { fix i have "i \<le> N \<Longrightarrow> i \<le> card (f i)"
  3.1204 -    proof (induct i)
  3.1205 -      case 0 then show ?case by simp
  3.1206 -    next
  3.1207 -      case (Suc i)
  3.1208 -      with inj[rule_format, of "Suc i" i]
  3.1209 -      have "(f i) \<subset> (f (Suc i))" by auto
  3.1210 -      moreover have "finite (f (Suc i))" using S by (rule finite_subset)
  3.1211 -      ultimately have "card (f i) < card (f (Suc i))" by (intro psubset_card_mono)
  3.1212 -      with Suc show ?case using inj by auto
  3.1213 -    qed
  3.1214 -  }
  3.1215 +  from ex obtain N where inj: "\<And>n m. n \<le> N \<Longrightarrow> m \<le> N \<Longrightarrow> m < n \<Longrightarrow> f m \<subset> f n"
  3.1216 +    and eq: "\<forall>n\<ge>N. f N = f n"
  3.1217 +    by atomize auto
  3.1218 +  have "i \<le> N \<Longrightarrow> i \<le> card (f i)" for i
  3.1219 +  proof (induct i)
  3.1220 +    case 0
  3.1221 +    then show ?case by simp
  3.1222 +  next
  3.1223 +    case (Suc i)
  3.1224 +    with inj [of "Suc i" i] have "(f i) \<subset> (f (Suc i))" by auto
  3.1225 +    moreover have "finite (f (Suc i))" using S by (rule finite_subset)
  3.1226 +    ultimately have "card (f i) < card (f (Suc i))" by (intro psubset_card_mono)
  3.1227 +    with Suc inj show ?case by auto
  3.1228 +  qed
  3.1229    then have "N \<le> card (f N)" by simp
  3.1230    also have "\<dots> \<le> card S" using S by (intro card_mono)
  3.1231    finally have "f (card S) = f N" using eq by auto
  3.1232 -  then show ?thesis using eq inj[rule_format, of N]
  3.1233 +  then show ?thesis
  3.1234 +    using eq inj [of N]
  3.1235      apply auto
  3.1236      apply (case_tac "n < N")
  3.1237 -    apply (auto simp: not_less)
  3.1238 +     apply (auto simp: not_less)
  3.1239      done
  3.1240  qed
  3.1241  
  3.1242 @@ -819,183 +843,174 @@
  3.1243    assumes bij: "bij f"
  3.1244  begin
  3.1245  
  3.1246 -lemma bij_inv:
  3.1247 -  "bij (inv f)"
  3.1248 +lemma bij_inv: "bij (inv f)"
  3.1249    using bij by (rule bij_imp_bij_inv)
  3.1250  
  3.1251 -lemma surj [simp]:
  3.1252 -  "surj f"
  3.1253 +lemma surj [simp]: "surj f"
  3.1254    using bij by (rule bij_is_surj)
  3.1255  
  3.1256 -lemma inj:
  3.1257 -  "inj f"
  3.1258 +lemma inj: "inj f"
  3.1259    using bij by (rule bij_is_inj)
  3.1260  
  3.1261 -lemma surj_inv [simp]:
  3.1262 -  "surj (inv f)"
  3.1263 +lemma surj_inv [simp]: "surj (inv f)"
  3.1264    using inj by (rule inj_imp_surj_inv)
  3.1265  
  3.1266 -lemma inj_inv:
  3.1267 -  "inj (inv f)"
  3.1268 +lemma inj_inv: "inj (inv f)"
  3.1269    using surj by (rule surj_imp_inj_inv)
  3.1270  
  3.1271 -lemma eqI:
  3.1272 -  "f a = f b \<Longrightarrow> a = b"
  3.1273 +lemma eqI: "f a = f b \<Longrightarrow> a = b"
  3.1274    using inj by (rule injD)
  3.1275  
  3.1276 -lemma eq_iff [simp]:
  3.1277 -  "f a = f b \<longleftrightarrow> a = b"
  3.1278 +lemma eq_iff [simp]: "f a = f b \<longleftrightarrow> a = b"
  3.1279    by (auto intro: eqI)
  3.1280  
  3.1281 -lemma eq_invI:
  3.1282 -  "inv f a = inv f b \<Longrightarrow> a = b"
  3.1283 +lemma eq_invI: "inv f a = inv f b \<Longrightarrow> a = b"
  3.1284    using inj_inv by (rule injD)
  3.1285  
  3.1286 -lemma eq_inv_iff [simp]:
  3.1287 -  "inv f a = inv f b \<longleftrightarrow> a = b"
  3.1288 +lemma eq_inv_iff [simp]: "inv f a = inv f b \<longleftrightarrow> a = b"
  3.1289    by (auto intro: eq_invI)
  3.1290  
  3.1291 -lemma inv_left [simp]:
  3.1292 -  "inv f (f a) = a"
  3.1293 +lemma inv_left [simp]: "inv f (f a) = a"
  3.1294    using inj by (simp add: inv_f_eq)
  3.1295  
  3.1296 -lemma inv_comp_left [simp]:
  3.1297 -  "inv f \<circ> f = id"
  3.1298 +lemma inv_comp_left [simp]: "inv f \<circ> f = id"
  3.1299    by (simp add: fun_eq_iff)
  3.1300  
  3.1301 -lemma inv_right [simp]:
  3.1302 -  "f (inv f a) = a"
  3.1303 +lemma inv_right [simp]: "f (inv f a) = a"
  3.1304    using surj by (simp add: surj_f_inv_f)
  3.1305  
  3.1306 -lemma inv_comp_right [simp]:
  3.1307 -  "f \<circ> inv f = id"
  3.1308 +lemma inv_comp_right [simp]: "f \<circ> inv f = id"
  3.1309    by (simp add: fun_eq_iff)
  3.1310  
  3.1311 -lemma inv_left_eq_iff [simp]:
  3.1312 -  "inv f a = b \<longleftrightarrow> f b = a"
  3.1313 +lemma inv_left_eq_iff [simp]: "inv f a = b \<longleftrightarrow> f b = a"
  3.1314    by auto
  3.1315  
  3.1316 -lemma inv_right_eq_iff [simp]:
  3.1317 -  "b = inv f a \<longleftrightarrow> f b = a"
  3.1318 +lemma inv_right_eq_iff [simp]: "b = inv f a \<longleftrightarrow> f b = a"
  3.1319    by auto
  3.1320  
  3.1321  end
  3.1322  
  3.1323  lemma infinite_imp_bij_betw:
  3.1324 -assumes INF: "\<not> finite A"
  3.1325 -shows "\<exists>h. bij_betw h A (A - {a})"
  3.1326 -proof(cases "a \<in> A")
  3.1327 -  assume Case1: "a \<notin> A"  hence "A - {a} = A" by blast
  3.1328 -  thus ?thesis using bij_betw_id[of A] by auto
  3.1329 +  assumes infinite: "\<not> finite A"
  3.1330 +  shows "\<exists>h. bij_betw h A (A - {a})"
  3.1331 +proof (cases "a \<in> A")
  3.1332 +  case False
  3.1333 +  then have "A - {a} = A" by blast
  3.1334 +  then show ?thesis
  3.1335 +    using bij_betw_id[of A] by auto
  3.1336  next
  3.1337 -  assume Case2: "a \<in> A"
  3.1338 -  have "\<not> finite (A - {a})" using INF by auto
  3.1339 -  with infinite_iff_countable_subset[of "A - {a}"] obtain f::"nat \<Rightarrow> 'a"
  3.1340 -  where 1: "inj f" and 2: "f ` UNIV \<le> A - {a}" by blast
  3.1341 -  obtain g where g_def: "g = (\<lambda> n. if n = 0 then a else f (Suc n))" by blast
  3.1342 -  obtain A' where A'_def: "A' = g ` UNIV" by blast
  3.1343 -  have temp: "\<forall>y. f y \<noteq> a" using 2 by blast
  3.1344 -  have 3: "inj_on g UNIV \<and> g ` UNIV \<le> A \<and> a \<in> g ` UNIV"
  3.1345 -  proof(auto simp add: Case2 g_def, unfold inj_on_def, intro ballI impI,
  3.1346 -        case_tac "x = 0", auto simp add: 2)
  3.1347 -    fix y  assume "a = (if y = 0 then a else f (Suc y))"
  3.1348 -    thus "y = 0" using temp by (case_tac "y = 0", auto)
  3.1349 +  case True
  3.1350 +  with infinite have "\<not> finite (A - {a})" by auto
  3.1351 +  with infinite_iff_countable_subset[of "A - {a}"]
  3.1352 +  obtain f :: "nat \<Rightarrow> 'a" where 1: "inj f" and 2: "f ` UNIV \<subseteq> A - {a}" by blast
  3.1353 +  define g where "g n = (if n = 0 then a else f (Suc n))" for n
  3.1354 +  define A' where "A' = g ` UNIV"
  3.1355 +  have *: "\<forall>y. f y \<noteq> a" using 2 by blast
  3.1356 +  have 3: "inj_on g UNIV \<and> g ` UNIV \<subseteq> A \<and> a \<in> g ` UNIV"
  3.1357 +    apply (auto simp add: True g_def [abs_def])
  3.1358 +     apply (unfold inj_on_def)
  3.1359 +     apply (intro ballI impI)
  3.1360 +     apply (case_tac "x = 0")
  3.1361 +      apply (auto simp add: 2)
  3.1362 +  proof -
  3.1363 +    fix y
  3.1364 +    assume "a = (if y = 0 then a else f (Suc y))"
  3.1365 +    then show "y = 0" by (cases "y = 0") (use * in auto)
  3.1366    next
  3.1367      fix x y
  3.1368      assume "f (Suc x) = (if y = 0 then a else f (Suc y))"
  3.1369 -    thus "x = y" using 1 temp unfolding inj_on_def by (case_tac "y = 0", auto)
  3.1370 +    with 1 * show "x = y" by (cases "y = 0") (auto simp: inj_on_def)
  3.1371    next
  3.1372 -    fix n show "f (Suc n) \<in> A" using 2 by blast
  3.1373 +    fix n
  3.1374 +    from 2 show "f (Suc n) \<in> A" by blast
  3.1375    qed
  3.1376 -  hence 4: "bij_betw g UNIV A' \<and> a \<in> A' \<and> A' \<le> A"
  3.1377 -  using inj_on_imp_bij_betw[of g] unfolding A'_def by auto
  3.1378 -  hence 5: "bij_betw (inv g) A' UNIV"
  3.1379 -  by (auto simp add: bij_betw_inv_into)
  3.1380 -  (*  *)
  3.1381 -  obtain n where "g n = a" using 3 by auto
  3.1382 -  hence 6: "bij_betw g (UNIV - {n}) (A' - {a})"
  3.1383 -  using 3 4 unfolding A'_def
  3.1384 -  by clarify (rule bij_betw_subset, auto simp: image_set_diff)
  3.1385 -  (*  *)
  3.1386 -  obtain v where v_def: "v = (\<lambda> m. if m < n then m else Suc m)" by blast
  3.1387 +  then have 4: "bij_betw g UNIV A' \<and> a \<in> A' \<and> A' \<subseteq> A"
  3.1388 +    using inj_on_imp_bij_betw[of g] by (auto simp: A'_def)
  3.1389 +  then have 5: "bij_betw (inv g) A' UNIV"
  3.1390 +    by (auto simp add: bij_betw_inv_into)
  3.1391 +  from 3 obtain n where n: "g n = a" by auto
  3.1392 +  have 6: "bij_betw g (UNIV - {n}) (A' - {a})"
  3.1393 +    by (rule bij_betw_subset) (use 3 4 n in \<open>auto simp: image_set_diff A'_def\<close>)
  3.1394 +  define v where "v m = (if m < n then m else Suc m)" for m
  3.1395    have 7: "bij_betw v UNIV (UNIV - {n})"
  3.1396 -  proof(unfold bij_betw_def inj_on_def, intro conjI, clarify)
  3.1397 -    fix m1 m2 assume "v m1 = v m2"
  3.1398 -    thus "m1 = m2"
  3.1399 -    by(case_tac "m1 < n", case_tac "m2 < n",
  3.1400 -       auto simp add: inj_on_def v_def, case_tac "m2 < n", auto)
  3.1401 +  proof (unfold bij_betw_def inj_on_def, intro conjI, clarify)
  3.1402 +    fix m1 m2
  3.1403 +    assume "v m1 = v m2"
  3.1404 +    then show "m1 = m2"
  3.1405 +      apply (cases "m1 < n")
  3.1406 +       apply (cases "m2 < n")
  3.1407 +        apply (auto simp: inj_on_def v_def [abs_def])
  3.1408 +      apply (cases "m2 < n")
  3.1409 +       apply auto
  3.1410 +      done
  3.1411    next
  3.1412      show "v ` UNIV = UNIV - {n}"
  3.1413 -    proof(auto simp add: v_def)
  3.1414 -      fix m assume *: "m \<noteq> n" and **: "m \<notin> Suc ` {m'. \<not> m' < n}"
  3.1415 -      {assume "n \<le> m" with * have 71: "Suc n \<le> m" by auto
  3.1416 -       then obtain m' where 72: "m = Suc m'" using Suc_le_D by auto
  3.1417 -       with 71 have "n \<le> m'" by auto
  3.1418 -       with 72 ** have False by auto
  3.1419 -      }
  3.1420 -      thus "m < n" by force
  3.1421 +    proof (auto simp: v_def [abs_def])
  3.1422 +      fix m
  3.1423 +      assume "m \<noteq> n"
  3.1424 +      assume *: "m \<notin> Suc ` {m'. \<not> m' < n}"
  3.1425 +      have False if "n \<le> m"
  3.1426 +      proof -
  3.1427 +        from \<open>m \<noteq> n\<close> that have **: "Suc n \<le> m" by auto
  3.1428 +        from Suc_le_D [OF this] obtain m' where m': "m = Suc m'" ..
  3.1429 +        with ** have "n \<le> m'" by auto
  3.1430 +        with m' * show ?thesis by auto
  3.1431 +      qed
  3.1432 +      then show "m < n" by force
  3.1433      qed
  3.1434    qed
  3.1435 -  (*  *)
  3.1436 -  obtain h' where h'_def: "h' = g o v o (inv g)" by blast
  3.1437 -  hence 8: "bij_betw h' A' (A' - {a})" using 5 7 6
  3.1438 -  by (auto simp add: bij_betw_trans)
  3.1439 -  (*  *)
  3.1440 -  obtain h where h_def: "h = (\<lambda> b. if b \<in> A' then h' b else b)" by blast
  3.1441 -  have "\<forall>b \<in> A'. h b = h' b" unfolding h_def by auto
  3.1442 -  hence "bij_betw h  A' (A' - {a})" using 8 bij_betw_cong[of A' h] by auto
  3.1443 +  define h' where "h' = g \<circ> v \<circ> (inv g)"
  3.1444 +  with 5 6 7 have 8: "bij_betw h' A' (A' - {a})"
  3.1445 +    by (auto simp add: bij_betw_trans)
  3.1446 +  define h where "h b = (if b \<in> A' then h' b else b)" for b
  3.1447 +  then have "\<forall>b \<in> A'. h b = h' b" by simp
  3.1448 +  with 8 have "bij_betw h  A' (A' - {a})"
  3.1449 +    using bij_betw_cong[of A' h] by auto
  3.1450    moreover
  3.1451 -  {have "\<forall>b \<in> A - A'. h b = b" unfolding h_def by auto
  3.1452 -   hence "bij_betw h  (A - A') (A - A')"
  3.1453 -   using bij_betw_cong[of "A - A'" h id] bij_betw_id[of "A - A'"] by auto
  3.1454 -  }
  3.1455 +  have "\<forall>b \<in> A - A'. h b = b" by (auto simp: h_def)
  3.1456 +  then have "bij_betw h  (A - A') (A - A')"
  3.1457 +    using bij_betw_cong[of "A - A'" h id] bij_betw_id[of "A - A'"] by auto
  3.1458    moreover
  3.1459 -  have "(A' Int (A - A') = {} \<and> A' \<union> (A - A') = A) \<and>
  3.1460 -        ((A' - {a}) Int (A - A') = {} \<and> (A' - {a}) \<union> (A - A') = A - {a})"
  3.1461 -  using 4 by blast
  3.1462 +  from 4 have "(A' \<inter> (A - A') = {} \<and> A' \<union> (A - A') = A) \<and>
  3.1463 +    ((A' - {a}) \<inter> (A - A') = {} \<and> (A' - {a}) \<union> (A - A') = A - {a})"
  3.1464 +    by blast
  3.1465    ultimately have "bij_betw h A (A - {a})"
  3.1466 -  using bij_betw_combine[of h A' "A' - {a}" "A - A'" "A - A'"] by simp
  3.1467 -  thus ?thesis by blast
  3.1468 +    using bij_betw_combine[of h A' "A' - {a}" "A - A'" "A - A'"] by simp
  3.1469 +  then show ?thesis by blast
  3.1470  qed
  3.1471  
  3.1472  lemma infinite_imp_bij_betw2:
  3.1473 -assumes INF: "\<not> finite A"
  3.1474 -shows "\<exists>h. bij_betw h A (A \<union> {a})"
  3.1475 -proof(cases "a \<in> A")
  3.1476 -  assume Case1: "a \<in> A"  hence "A \<union> {a} = A" by blast
  3.1477 -  thus ?thesis using bij_betw_id[of A] by auto
  3.1478 +  assumes "\<not> finite A"
  3.1479 +  shows "\<exists>h. bij_betw h A (A \<union> {a})"
  3.1480 +proof (cases "a \<in> A")
  3.1481 +  case True
  3.1482 +  then have "A \<union> {a} = A" by blast
  3.1483 +  then show ?thesis using bij_betw_id[of A] by auto
  3.1484  next
  3.1485 +  case False
  3.1486    let ?A' = "A \<union> {a}"
  3.1487 -  assume Case2: "a \<notin> A" hence "A = ?A' - {a}" by blast
  3.1488 -  moreover have "\<not> finite ?A'" using INF by auto
  3.1489 +  from False have "A = ?A' - {a}" by blast
  3.1490 +  moreover from assms have "\<not> finite ?A'" by auto
  3.1491    ultimately obtain f where "bij_betw f ?A' A"
  3.1492 -  using infinite_imp_bij_betw[of ?A' a] by auto
  3.1493 -  hence "bij_betw(inv_into ?A' f) A ?A'" using bij_betw_inv_into by blast
  3.1494 -  thus ?thesis by auto
  3.1495 +    using infinite_imp_bij_betw[of ?A' a] by auto
  3.1496 +  then have "bij_betw (inv_into ?A' f) A ?A'" by (rule bij_betw_inv_into)
  3.1497 +  then show ?thesis by auto
  3.1498  qed
  3.1499  
  3.1500 -lemma bij_betw_inv_into_left:
  3.1501 -assumes BIJ: "bij_betw f A A'" and IN: "a \<in> A"
  3.1502 -shows "(inv_into A f) (f a) = a"
  3.1503 -using assms unfolding bij_betw_def
  3.1504 -by clarify (rule inv_into_f_f)
  3.1505 +lemma bij_betw_inv_into_left: "bij_betw f A A' \<Longrightarrow> a \<in> A \<Longrightarrow> inv_into A f (f a) = a"
  3.1506 +  unfolding bij_betw_def by clarify (rule inv_into_f_f)
  3.1507  
  3.1508 -lemma bij_betw_inv_into_right:
  3.1509 -assumes "bij_betw f A A'" "a' \<in> A'"
  3.1510 -shows "f(inv_into A f a') = a'"
  3.1511 -using assms unfolding bij_betw_def using f_inv_into_f by force
  3.1512 +lemma bij_betw_inv_into_right: "bij_betw f A A' \<Longrightarrow> a' \<in> A' \<Longrightarrow> f (inv_into A f a') = a'"
  3.1513 +  unfolding bij_betw_def using f_inv_into_f by force
  3.1514  
  3.1515  lemma bij_betw_inv_into_subset:
  3.1516 -assumes BIJ: "bij_betw f A A'" and
  3.1517 -        SUB: "B \<le> A" and IM: "f ` B = B'"
  3.1518 -shows "bij_betw (inv_into A f) B' B"
  3.1519 -using assms unfolding bij_betw_def
  3.1520 -by (auto intro: inj_on_inv_into)
  3.1521 +  "bij_betw f A A' \<Longrightarrow> B \<subseteq> A \<Longrightarrow> f ` B = B' \<Longrightarrow> bij_betw (inv_into A f) B' B"
  3.1522 +  by (auto simp: bij_betw_def intro: inj_on_inv_into)
  3.1523  
  3.1524  
  3.1525  subsection \<open>Specification package -- Hilbertized version\<close>
  3.1526  
  3.1527 -lemma exE_some: "[| Ex P ; c == Eps P |] ==> P c"
  3.1528 +lemma exE_some: "Ex P \<Longrightarrow> c \<equiv> Eps P \<Longrightarrow> P c"
  3.1529    by (simp only: someI_ex)
  3.1530  
  3.1531  ML_file "Tools/choice_specification.ML"
     4.1 --- a/src/HOL/Relation.thy	Fri Aug 05 16:36:03 2016 +0200
     4.2 +++ b/src/HOL/Relation.thy	Fri Aug 05 18:14:28 2016 +0200
     4.3 @@ -1,11 +1,12 @@
     4.4  (*  Title:      HOL/Relation.thy
     4.5 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory; Stefan Berghofer, TU Muenchen
     4.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4.7 +    Author:     Stefan Berghofer, TU Muenchen
     4.8  *)
     4.9  
    4.10  section \<open>Relations -- as sets of pairs, and binary predicates\<close>
    4.11  
    4.12  theory Relation
    4.13 -imports Finite_Set
    4.14 +  imports Finite_Set
    4.15  begin
    4.16  
    4.17  text \<open>A preliminary: classical rules for reasoning on predicates\<close>
    4.18 @@ -400,16 +401,17 @@
    4.19    by (auto intro: transpI)
    4.20  
    4.21  lemma trans_empty [simp]: "trans {}"
    4.22 -by (blast intro: transI)
    4.23 +  by (blast intro: transI)
    4.24  
    4.25  lemma transp_empty [simp]: "transp (\<lambda>x y. False)"
    4.26 -using trans_empty[to_pred] by(simp add: bot_fun_def)
    4.27 +  using trans_empty[to_pred] by (simp add: bot_fun_def)
    4.28  
    4.29  lemma trans_singleton [simp]: "trans {(a, a)}"
    4.30 -by (blast intro: transI)
    4.31 +  by (blast intro: transI)
    4.32  
    4.33  lemma transp_singleton [simp]: "transp (\<lambda>x y. x = a \<and> y = a)"
    4.34 -by(simp add: transp_def)
    4.35 +  by (simp add: transp_def)
    4.36 +
    4.37  
    4.38  subsubsection \<open>Totality\<close>
    4.39  
    4.40 @@ -418,7 +420,7 @@
    4.41  
    4.42  lemma total_onI [intro?]:
    4.43    "(\<And>x y. \<lbrakk>x \<in> A; y \<in> A; x \<noteq> y\<rbrakk> \<Longrightarrow> (x, y) \<in> r \<or> (y, x) \<in> r) \<Longrightarrow> total_on A r"
    4.44 -unfolding total_on_def by blast
    4.45 +  unfolding total_on_def by blast
    4.46  
    4.47  abbreviation "total \<equiv> total_on UNIV"
    4.48  
    4.49 @@ -426,7 +428,8 @@
    4.50    by (simp add: total_on_def)
    4.51  
    4.52  lemma total_on_singleton [simp]: "total_on {x} {(x, x)}"
    4.53 -unfolding total_on_def by blast
    4.54 +  unfolding total_on_def by blast
    4.55 +
    4.56  
    4.57  subsubsection \<open>Single valued relations\<close>
    4.58  
    4.59 @@ -496,7 +499,7 @@
    4.60  
    4.61  subsubsection \<open>Diagonal: identity over a set\<close>
    4.62  
    4.63 -definition Id_on  :: "'a set \<Rightarrow> 'a rel"
    4.64 +definition Id_on :: "'a set \<Rightarrow> 'a rel"
    4.65    where "Id_on A = (\<Union>x\<in>A. {(x, x)})"
    4.66  
    4.67  lemma Id_on_empty [simp]: "Id_on {} = {}"
    4.68 @@ -633,7 +636,7 @@
    4.69  lemma relcompp_apply: "(R OO S) a c \<longleftrightarrow> (\<exists>b. R a b \<and> S b c)"
    4.70    unfolding relcomp_unfold [to_pred] ..
    4.71  
    4.72 -lemma eq_OO: "op= OO R = R"
    4.73 +lemma eq_OO: "op = OO R = R"
    4.74    by blast
    4.75  
    4.76  lemma OO_eq: "R OO op = = R"
    4.77 @@ -728,10 +731,10 @@
    4.78  lemma conversep_inject[simp]: "r\<inverse>\<inverse> = s \<inverse>\<inverse> \<longleftrightarrow> r = s"
    4.79    by (fact converse_inject[to_pred])
    4.80  
    4.81 -lemma converse_subset_swap: "r \<subseteq> s \<inverse> = (r \<inverse> \<subseteq> s)"
    4.82 +lemma converse_subset_swap: "r \<subseteq> s \<inverse> \<longleftrightarrow> r \<inverse> \<subseteq> s"
    4.83    by auto
    4.84  
    4.85 -lemma conversep_le_swap: "r \<le> s \<inverse>\<inverse> = (r \<inverse>\<inverse> \<le> s)"
    4.86 +lemma conversep_le_swap: "r \<le> s \<inverse>\<inverse> \<longleftrightarrow> r \<inverse>\<inverse> \<le> s"
    4.87    by (fact converse_subset_swap[to_pred])
    4.88  
    4.89  lemma converse_Id [simp]: "Id\<inverse> = Id"
    4.90 @@ -800,7 +803,7 @@
    4.91    where "Field r = Domain r \<union> Range r"
    4.92  
    4.93  lemma FieldI1: "(i, j) \<in> R \<Longrightarrow> i \<in> Field R"
    4.94 -unfolding Field_def by blast
    4.95 +  unfolding Field_def by blast
    4.96  
    4.97  lemma FieldI2: "(i, j) \<in> R \<Longrightarrow> j \<in> Field R"
    4.98    unfolding Field_def by auto
    4.99 @@ -932,7 +935,7 @@
   4.100    by blast
   4.101  
   4.102  lemma Field_square [simp]: "Field (x \<times> x) = x"
   4.103 -unfolding Field_def by blast
   4.104 +  unfolding Field_def by blast
   4.105  
   4.106  
   4.107  subsubsection \<open>Image of a set under a relation\<close>
   4.108 @@ -972,7 +975,7 @@
   4.109    by blast
   4.110  
   4.111  lemma Image_Int_eq: "single_valued (converse R) \<Longrightarrow> R `` (A \<inter> B) = R `` A \<inter> R `` B"
   4.112 -  by (simp add: single_valued_def, blast)
   4.113 +  by (auto simp: single_valued_def)
   4.114  
   4.115  lemma Image_Un: "R `` (A \<union> B) = R `` A \<union> R `` B"
   4.116    by blast
   4.117 @@ -1079,7 +1082,7 @@
   4.118    interpret comp_fun_idem Set.insert
   4.119      by (fact comp_fun_idem_insert)
   4.120    show ?thesis
   4.121 -    by standard (auto simp add: fun_eq_iff comp_fun_commute split: prod.split)
   4.122 +    by standard (auto simp: fun_eq_iff comp_fun_commute split: prod.split)
   4.123  qed
   4.124  
   4.125  lemma Image_fold:
     5.1 --- a/src/HOL/Transitive_Closure.thy	Fri Aug 05 16:36:03 2016 +0200
     5.2 +++ b/src/HOL/Transitive_Closure.thy	Fri Aug 05 18:14:28 2016 +0200
     5.3 @@ -6,7 +6,7 @@
     5.4  section \<open>Reflexive and Transitive closure of a relation\<close>
     5.5  
     5.6  theory Transitive_Closure
     5.7 -imports Relation
     5.8 +  imports Relation
     5.9  begin
    5.10  
    5.11  ML_file "~~/src/Provers/trancl.ML"
    5.12 @@ -16,25 +16,24 @@
    5.13    \<open>trancl\<close> is transitive closure,
    5.14    \<open>reflcl\<close> is reflexive closure.
    5.15  
    5.16 -  These postfix operators have \emph{maximum priority}, forcing their
    5.17 +  These postfix operators have \<^emph>\<open>maximum priority\<close>, forcing their
    5.18    operands to be atomic.
    5.19  \<close>
    5.20  
    5.21 -context
    5.22 -  notes [[inductive_internals]]
    5.23 +context notes [[inductive_internals]]
    5.24  begin
    5.25  
    5.26  inductive_set rtrancl :: "('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set"  ("(_\<^sup>*)" [1000] 999)
    5.27    for r :: "('a \<times> 'a) set"
    5.28 -where
    5.29 -  rtrancl_refl [intro!, Pure.intro!, simp]: "(a, a) \<in> r\<^sup>*"
    5.30 -| rtrancl_into_rtrancl [Pure.intro]: "(a, b) \<in> r\<^sup>* \<Longrightarrow> (b, c) \<in> r \<Longrightarrow> (a, c) \<in> r\<^sup>*"
    5.31 +  where
    5.32 +    rtrancl_refl [intro!, Pure.intro!, simp]: "(a, a) \<in> r\<^sup>*"
    5.33 +  | rtrancl_into_rtrancl [Pure.intro]: "(a, b) \<in> r\<^sup>* \<Longrightarrow> (b, c) \<in> r \<Longrightarrow> (a, c) \<in> r\<^sup>*"
    5.34  
    5.35  inductive_set trancl :: "('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set"  ("(_\<^sup>+)" [1000] 999)
    5.36    for r :: "('a \<times> 'a) set"
    5.37 -where
    5.38 -  r_into_trancl [intro, Pure.intro]: "(a, b) \<in> r \<Longrightarrow> (a, b) \<in> r\<^sup>+"
    5.39 -| trancl_into_trancl [Pure.intro]: "(a, b) \<in> r\<^sup>+ \<Longrightarrow> (b, c) \<in> r \<Longrightarrow> (a, c) \<in> r\<^sup>+"
    5.40 +  where
    5.41 +    r_into_trancl [intro, Pure.intro]: "(a, b) \<in> r \<Longrightarrow> (a, b) \<in> r\<^sup>+"
    5.42 +  | trancl_into_trancl [Pure.intro]: "(a, b) \<in> r\<^sup>+ \<Longrightarrow> (b, c) \<in> r \<Longrightarrow> (a, c) \<in> r\<^sup>+"
    5.43  
    5.44  notation
    5.45    rtranclp  ("(_\<^sup>*\<^sup>*)" [1000] 1000) and
    5.46 @@ -215,7 +214,9 @@
    5.47  
    5.48  lemma rtrancl_r_diff_Id: "(r - Id)\<^sup>* = r\<^sup>*"
    5.49    apply (rule sym)
    5.50 -  apply (rule rtrancl_subset, blast, clarify)
    5.51 +  apply (rule rtrancl_subset)
    5.52 +   apply blast
    5.53 +  apply clarify
    5.54    apply (rename_tac a b)
    5.55    apply (case_tac "a = b")
    5.56     apply blast
    5.57 @@ -258,10 +259,10 @@
    5.58  lemmas converse_rtrancl_induct = converse_rtranclp_induct [to_set]
    5.59  
    5.60  lemmas converse_rtranclp_induct2 =
    5.61 -  converse_rtranclp_induct [of _ "(ax,ay)" "(bx,by)", split_rule, consumes 1, case_names refl step]
    5.62 +  converse_rtranclp_induct [of _ "(ax, ay)" "(bx, by)", split_rule, consumes 1, case_names refl step]
    5.63  
    5.64  lemmas converse_rtrancl_induct2 =
    5.65 -  converse_rtrancl_induct [of "(ax,ay)" "(bx,by)", split_format (complete),
    5.66 +  converse_rtrancl_induct [of "(ax, ay)" "(bx, by)", split_format (complete),
    5.67      consumes 1, case_names refl step]
    5.68  
    5.69  lemma converse_rtranclpE [consumes 1, case_names base step]:
    5.70 @@ -283,24 +284,30 @@
    5.71  
    5.72  lemma r_comp_rtrancl_eq: "r O r\<^sup>* = r\<^sup>* O r"
    5.73    by (blast elim: rtranclE converse_rtranclE
    5.74 -    intro: rtrancl_into_rtrancl converse_rtrancl_into_rtrancl)
    5.75 +      intro: rtrancl_into_rtrancl converse_rtrancl_into_rtrancl)
    5.76  
    5.77  lemma rtrancl_unfold: "r\<^sup>* = Id \<union> r\<^sup>* O r"
    5.78    by (auto intro: rtrancl_into_rtrancl elim: rtranclE)
    5.79  
    5.80  lemma rtrancl_Un_separatorE:
    5.81    "(a, b) \<in> (P \<union> Q)\<^sup>* \<Longrightarrow> \<forall>x y. (a, x) \<in> P\<^sup>* \<longrightarrow> (x, y) \<in> Q \<longrightarrow> x = y \<Longrightarrow> (a, b) \<in> P\<^sup>*"
    5.82 -  apply (induct rule:rtrancl.induct)
    5.83 -   apply blast
    5.84 -  apply (blast intro:rtrancl_trans)
    5.85 -  done
    5.86 +proof (induct rule: rtrancl.induct)
    5.87 +  case rtrancl_refl
    5.88 +  then show ?case by blast
    5.89 +next
    5.90 +  case rtrancl_into_rtrancl
    5.91 +  then show ?case by (blast intro: rtrancl_trans)
    5.92 +qed
    5.93  
    5.94  lemma rtrancl_Un_separator_converseE:
    5.95    "(a, b) \<in> (P \<union> Q)\<^sup>* \<Longrightarrow> \<forall>x y. (x, b) \<in> P\<^sup>* \<longrightarrow> (y, x) \<in> Q \<longrightarrow> y = x \<Longrightarrow> (a, b) \<in> P\<^sup>*"
    5.96 -  apply (induct rule:converse_rtrancl_induct)
    5.97 -   apply blast
    5.98 -  apply (blast intro:rtrancl_trans)
    5.99 -  done
   5.100 +proof (induct rule: converse_rtrancl_induct)
   5.101 +  case base
   5.102 +  then show ?case by blast
   5.103 +next
   5.104 +  case step
   5.105 +  then show ?case by (blast intro: rtrancl_trans)
   5.106 +qed
   5.107  
   5.108  lemma Image_closed_trancl:
   5.109    assumes "r `` X \<subseteq> X"
   5.110 @@ -368,10 +375,10 @@
   5.111  lemmas trancl_induct [induct set: trancl] = tranclp_induct [to_set]
   5.112  
   5.113  lemmas tranclp_induct2 =
   5.114 -  tranclp_induct [of _ "(ax,ay)" "(bx,by)", split_rule, consumes 1, case_names base step]
   5.115 +  tranclp_induct [of _ "(ax, ay)" "(bx, by)", split_rule, consumes 1, case_names base step]
   5.116  
   5.117  lemmas trancl_induct2 =
   5.118 -  trancl_induct [of "(ax,ay)" "(bx,by)", split_format (complete),
   5.119 +  trancl_induct [of "(ax, ay)" "(bx, by)", split_format (complete),
   5.120      consumes 1, case_names base step]
   5.121  
   5.122  lemma tranclp_trans_induct:
   5.123 @@ -394,7 +401,7 @@
   5.124    apply (rule subsetI)
   5.125    apply auto
   5.126    apply (erule trancl_induct)
   5.127 -  apply auto
   5.128 +   apply auto
   5.129    done
   5.130  
   5.131  lemma trancl_unfold: "r\<^sup>+ = r \<union> r\<^sup>+ O r"
   5.132 @@ -449,7 +456,7 @@
   5.133  lemma tranclp_converseI: "(r\<^sup>+\<^sup>+)\<inverse>\<inverse> x y \<Longrightarrow> (r\<inverse>\<inverse>)\<^sup>+\<^sup>+ x y"
   5.134    apply (drule conversepD)
   5.135    apply (erule tranclp_induct)
   5.136 -  apply (iprover intro: conversepI tranclp_trans)+
   5.137 +   apply (iprover intro: conversepI tranclp_trans)+
   5.138    done
   5.139  
   5.140  lemmas trancl_converseI = tranclp_converseI [to_set]
   5.141 @@ -457,7 +464,7 @@
   5.142  lemma tranclp_converseD: "(r\<inverse>\<inverse>)\<^sup>+\<^sup>+ x y \<Longrightarrow> (r\<^sup>+\<^sup>+)\<inverse>\<inverse> x y"
   5.143    apply (rule conversepI)
   5.144    apply (erule tranclp_induct)
   5.145 -  apply (iprover dest: conversepD intro: tranclp_trans)+
   5.146 +   apply (iprover dest: conversepD intro: tranclp_trans)+
   5.147    done
   5.148  
   5.149  lemmas trancl_converseD = tranclp_converseD [to_set]
   5.150 @@ -493,7 +500,7 @@
   5.151  lemma converse_tranclpE:
   5.152    assumes major: "tranclp r x z"
   5.153      and base: "r x z \<Longrightarrow> P"
   5.154 -    and step: "\<And> y. r x y \<Longrightarrow> tranclp r y z \<Longrightarrow> P"
   5.155 +    and step: "\<And>y. r x y \<Longrightarrow> tranclp r y z \<Longrightarrow> P"
   5.156    shows P
   5.157  proof -
   5.158    from tranclpD [OF major] obtain y where "r x y" and "rtranclp r y z"
   5.159 @@ -582,7 +589,7 @@
   5.160     apply (blast intro: rtrancl_into_trancl1 trancl_into_rtrancl trancl_trans)
   5.161    apply (rule subsetI)
   5.162    apply (blast intro: trancl_mono rtrancl_mono
   5.163 -    [THEN [2] rev_subsetD] rtrancl_trancl_trancl rtrancl_into_trancl2)
   5.164 +      [THEN [2] rev_subsetD] rtrancl_trancl_trancl rtrancl_into_trancl2)
   5.165    done
   5.166  
   5.167  lemma trancl_insert2:
   5.168 @@ -655,26 +662,23 @@
   5.169  lemma single_valued_confluent:
   5.170    "single_valued r \<Longrightarrow> (x, y) \<in> r\<^sup>* \<Longrightarrow> (x, z) \<in> r\<^sup>* \<Longrightarrow> (y, z) \<in> r\<^sup>* \<or> (z, y) \<in> r\<^sup>*"
   5.171    apply (erule rtrancl_induct)
   5.172 -  apply simp
   5.173 +   apply simp
   5.174    apply (erule disjE)
   5.175     apply (blast elim:converse_rtranclE dest:single_valuedD)
   5.176 -  apply(blast intro:rtrancl_trans)
   5.177 +  apply (blast intro:rtrancl_trans)
   5.178    done
   5.179  
   5.180  lemma r_r_into_trancl: "(a, b) \<in> R \<Longrightarrow> (b, c) \<in> R \<Longrightarrow> (a, c) \<in> R\<^sup>+"
   5.181    by (fast intro: trancl_trans)
   5.182  
   5.183  lemma trancl_into_trancl: "(a, b) \<in> r\<^sup>+ \<Longrightarrow> (b, c) \<in> r \<Longrightarrow> (a, c) \<in> r\<^sup>+"
   5.184 -  apply (induct rule: trancl_induct)
   5.185 -   apply (fast intro: r_r_into_trancl)
   5.186 -  apply (fast intro: r_r_into_trancl trancl_trans)
   5.187 -  done
   5.188 +  by (induct rule: trancl_induct) (fast intro: r_r_into_trancl trancl_trans)+
   5.189  
   5.190  lemma tranclp_rtranclp_tranclp: "r\<^sup>+\<^sup>+ a b \<Longrightarrow> r\<^sup>*\<^sup>* b c \<Longrightarrow> r\<^sup>+\<^sup>+ a c"
   5.191    apply (drule tranclpD)
   5.192    apply (elim exE conjE)
   5.193    apply (drule rtranclp_trans, assumption)
   5.194 -  apply (drule rtranclp_into_tranclp2, assumption, assumption)
   5.195 +  apply (drule (2) rtranclp_into_tranclp2)
   5.196    done
   5.197  
   5.198  lemmas trancl_rtrancl_trancl = tranclp_rtranclp_tranclp [to_set]
   5.199 @@ -704,14 +708,14 @@
   5.200  begin
   5.201  
   5.202  primrec relpow :: "nat \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set"
   5.203 -where
   5.204 -  "relpow 0 R = Id"
   5.205 -| "relpow (Suc n) R = (R ^^ n) O R"
   5.206 +  where
   5.207 +    "relpow 0 R = Id"
   5.208 +  | "relpow (Suc n) R = (R ^^ n) O R"
   5.209  
   5.210  primrec relpowp :: "nat \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool)"
   5.211 -where
   5.212 -  "relpowp 0 R = HOL.eq"
   5.213 -| "relpowp (Suc n) R = (R ^^ n) OO R"
   5.214 +  where
   5.215 +    "relpowp 0 R = HOL.eq"
   5.216 +  | "relpowp (Suc n) R = (R ^^ n) OO R"
   5.217  
   5.218  end
   5.219  
   5.220 @@ -740,10 +744,12 @@
   5.221  hide_const (open) relpow
   5.222  hide_const (open) relpowp
   5.223  
   5.224 -lemma relpow_1 [simp]: "R ^^ 1 = R" for R :: "('a \<times> 'a) set"
   5.225 +lemma relpow_1 [simp]: "R ^^ 1 = R"
   5.226 +  for R :: "('a \<times> 'a) set"
   5.227    by simp
   5.228  
   5.229 -lemma relpowp_1 [simp]: "P ^^ 1 = P" for P :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
   5.230 +lemma relpowp_1 [simp]: "P ^^ 1 = P"
   5.231 +  for P :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
   5.232    by (fact relpow_1 [to_pred])
   5.233  
   5.234  lemma relpow_0_I: "(x, x) \<in> R ^^ 0"
   5.235 @@ -777,22 +783,20 @@
   5.236    by (fact relpow_Suc_E [to_pred])
   5.237  
   5.238  lemma relpow_E:
   5.239 -  "(x, z) \<in>  R ^^ n \<Longrightarrow>  (n = 0 \<Longrightarrow> x = z \<Longrightarrow> P)
   5.240 -   \<Longrightarrow> (\<And>y m. n = Suc m \<Longrightarrow> (x, y) \<in>  R ^^ m \<Longrightarrow> (y, z) \<in> R \<Longrightarrow> P)
   5.241 -   \<Longrightarrow> P"
   5.242 +  "(x, z) \<in>  R ^^ n \<Longrightarrow>
   5.243 +    (n = 0 \<Longrightarrow> x = z \<Longrightarrow> P) \<Longrightarrow>
   5.244 +    (\<And>y m. n = Suc m \<Longrightarrow> (x, y) \<in>  R ^^ m \<Longrightarrow> (y, z) \<in> R \<Longrightarrow> P) \<Longrightarrow> P"
   5.245    by (cases n) auto
   5.246  
   5.247  lemma relpowp_E:
   5.248 -  "(P ^^ n) x z \<Longrightarrow> (n = 0 \<Longrightarrow> x = z \<Longrightarrow> Q)
   5.249 -  \<Longrightarrow> (\<And>y m. n = Suc m \<Longrightarrow> (P ^^ m) x y \<Longrightarrow> P y z \<Longrightarrow> Q)
   5.250 -  \<Longrightarrow> Q"
   5.251 +  "(P ^^ n) x z \<Longrightarrow>
   5.252 +    (n = 0 \<Longrightarrow> x = z \<Longrightarrow> Q) \<Longrightarrow>
   5.253 +    (\<And>y m. n = Suc m \<Longrightarrow> (P ^^ m) x y \<Longrightarrow> P y z \<Longrightarrow> Q) \<Longrightarrow> Q"
   5.254    by (fact relpow_E [to_pred])
   5.255  
   5.256  lemma relpow_Suc_D2: "(x, z) \<in> R ^^ Suc n \<Longrightarrow> (\<exists>y. (x, y) \<in> R \<and> (y, z) \<in> R ^^ n)"
   5.257 -  apply (induct n arbitrary: x z)
   5.258 -   apply (blast intro: relpow_0_I elim: relpow_0_E relpow_Suc_E)
   5.259 -  apply (blast intro: relpow_Suc_I elim: relpow_0_E relpow_Suc_E)
   5.260 -  done
   5.261 +  by (induct n arbitrary: x z)
   5.262 +    (blast intro: relpow_0_I relpow_Suc_I elim: relpow_0_E relpow_Suc_E)+
   5.263  
   5.264  lemma relpowp_Suc_D2: "(P ^^ Suc n) x z \<Longrightarrow> \<exists>y. P x y \<and> (P ^^ n) y z"
   5.265    by (fact relpow_Suc_D2 [to_pred])
   5.266 @@ -810,18 +814,21 @@
   5.267    by (fact relpow_Suc_D2' [to_pred])
   5.268  
   5.269  lemma relpow_E2:
   5.270 -  "(x, z) \<in> R ^^ n \<Longrightarrow>  (n = 0 \<Longrightarrow> x = z \<Longrightarrow> P)
   5.271 -     \<Longrightarrow> (\<And>y m. n = Suc m \<Longrightarrow> (x, y) \<in> R \<Longrightarrow> (y, z) \<in> R ^^ m \<Longrightarrow> P)
   5.272 -   \<Longrightarrow> P"
   5.273 -  apply (cases n, simp)
   5.274 +  "(x, z) \<in> R ^^ n \<Longrightarrow>
   5.275 +    (n = 0 \<Longrightarrow> x = z \<Longrightarrow> P) \<Longrightarrow>
   5.276 +    (\<And>y m. n = Suc m \<Longrightarrow> (x, y) \<in> R \<Longrightarrow> (y, z) \<in> R ^^ m \<Longrightarrow> P) \<Longrightarrow> P"
   5.277 +  apply (cases n)
   5.278 +   apply simp
   5.279    apply (rename_tac nat)
   5.280 -  apply (cut_tac n=nat and R=R in relpow_Suc_D2', simp, blast)
   5.281 +  apply (cut_tac n=nat and R=R in relpow_Suc_D2')
   5.282 +  apply simp
   5.283 +  apply blast
   5.284    done
   5.285  
   5.286  lemma relpowp_E2:
   5.287 -  "(P ^^ n) x z \<Longrightarrow> (n = 0 \<Longrightarrow> x = z \<Longrightarrow> Q)
   5.288 -    \<Longrightarrow> (\<And>y m. n = Suc m \<Longrightarrow> P x y \<Longrightarrow> (P ^^ m) y z \<Longrightarrow> Q)
   5.289 -  \<Longrightarrow> Q"
   5.290 +  "(P ^^ n) x z \<Longrightarrow>
   5.291 +    (n = 0 \<Longrightarrow> x = z \<Longrightarrow> Q) \<Longrightarrow>
   5.292 +    (\<And>y m. n = Suc m \<Longrightarrow> P x y \<Longrightarrow> (P ^^ m) y z \<Longrightarrow> Q) \<Longrightarrow> Q"
   5.293    by (fact relpow_E2 [to_pred])
   5.294  
   5.295  lemma relpow_add: "R ^^ (m + n) = R^^m O R^^n"
   5.296 @@ -848,7 +855,8 @@
   5.297  proof (cases p)
   5.298    case (Pair x y)
   5.299    with assms have "(x, y) \<in> R\<^sup>*" by simp
   5.300 -  then have "(x, y) \<in> (\<Union>n. R ^^ n)" proof induct
   5.301 +  then have "(x, y) \<in> (\<Union>n. R ^^ n)"
   5.302 +  proof induct
   5.303      case base
   5.304      show ?case by (blast intro: relpow_0_I)
   5.305    next
   5.306 @@ -869,7 +877,8 @@
   5.307  proof (cases p)
   5.308    case (Pair x y)
   5.309    with assms have "(x, y) \<in> R ^^ n" by simp
   5.310 -  then have "(x, y) \<in> R\<^sup>*" proof (induct n arbitrary: x y)
   5.311 +  then have "(x, y) \<in> R\<^sup>*"
   5.312 +  proof (induct n arbitrary: x y)
   5.313      case 0
   5.314      then show ?case by simp
   5.315    next
   5.316 @@ -905,10 +914,12 @@
   5.317     apply (clarsimp simp: relcomp_unfold)
   5.318     apply fastforce
   5.319    apply clarsimp
   5.320 -  apply (case_tac n, simp)
   5.321 +  apply (case_tac n)
   5.322 +   apply simp
   5.323    apply clarsimp
   5.324    apply (drule relpow_imp_rtrancl)
   5.325 -  apply (drule rtrancl_into_trancl1) apply auto
   5.326 +  apply (drule rtrancl_into_trancl1)
   5.327 +   apply auto
   5.328    done
   5.329  
   5.330  lemma tranclp_power: "(P\<^sup>+\<^sup>+) x y \<longleftrightarrow> (\<exists>n > 0. (P ^^ n) x y)"
   5.331 @@ -954,7 +965,8 @@
   5.332  lemma relpow_finite_bounded1:
   5.333    fixes R :: "('a \<times> 'a) set"
   5.334    assumes "finite R" and "k > 0"
   5.335 -  shows "R^^k \<subseteq> (\<Union>n\<in>{n. 0 < n \<and> n \<le> card R}. R^^n)" (is "_ \<subseteq> ?r")
   5.336 +  shows "R^^k \<subseteq> (\<Union>n\<in>{n. 0 < n \<and> n \<le> card R}. R^^n)"
   5.337 +    (is "_ \<subseteq> ?r")
   5.338  proof -
   5.339    have "(a, b) \<in> R^^(Suc k) \<Longrightarrow> \<exists>n. 0 < n \<and> n \<le> card R \<and> (a, b) \<in> R^^n" for a b k
   5.340    proof (induct k arbitrary: b)
   5.341 @@ -1050,8 +1062,7 @@
   5.342    shows "R^^k \<subseteq> (UN n:{n. n \<le> card R}. R^^n)"
   5.343    apply (cases k)
   5.344     apply force
   5.345 -  using relpow_finite_bounded1[OF assms, of k]
   5.346 -  apply auto
   5.347 +  apply (use relpow_finite_bounded1[OF assms, of k] in auto)
   5.348    done
   5.349  
   5.350  lemma rtrancl_finite_eq_relpow: "finite R \<Longrightarrow> R\<^sup>* = (\<Union>n\<in>{n. n \<le> card R}. R^^n)"
   5.351 @@ -1076,20 +1087,26 @@
   5.352    fixes R :: "('a \<times> 'a) set"
   5.353    assumes "finite R"
   5.354    shows "n > 0 \<Longrightarrow> finite (R^^n)"
   5.355 -  apply (induct n)
   5.356 -   apply simp
   5.357 -  apply (case_tac n)
   5.358 -   apply (simp_all add: assms)
   5.359 -  done
   5.360 +proof (induct n)
   5.361 +  case 0
   5.362 +  then show ?case by simp
   5.363 +next
   5.364 +  case (Suc n)
   5.365 +  then show ?case by (cases n) (use assms in simp_all)
   5.366 +qed
   5.367  
   5.368  lemma single_valued_relpow:
   5.369    fixes R :: "('a \<times> 'a) set"
   5.370    shows "single_valued R \<Longrightarrow> single_valued (R ^^ n)"
   5.371 -  apply (induct n arbitrary: R)
   5.372 -  apply simp_all
   5.373 -  apply (rule single_valuedI)
   5.374 -  apply (fast dest: single_valuedD elim: relpow_Suc_E)
   5.375 -  done
   5.376 +proof (induct n arbitrary: R)
   5.377 +  case 0
   5.378 +  then show ?case by simp
   5.379 +next
   5.380 +  case (Suc n)
   5.381 +  show ?case
   5.382 +    by (rule single_valuedI)
   5.383 +      (use Suc in \<open>fast dest: single_valuedD elim: relpow_Suc_E\<close>)
   5.384 +qed
   5.385  
   5.386  
   5.387  subsection \<open>Bounded transitive closure\<close>
   5.388 @@ -1101,7 +1118,6 @@
   5.389  proof
   5.390    show "R \<subseteq> ntrancl 0 R"
   5.391      unfolding ntrancl_def by fastforce
   5.392 -next
   5.393    have "0 < i \<and> i \<le> Suc 0 \<longleftrightarrow> i = 1" for i
   5.394      by auto
   5.395    then show "ntrancl 0 R \<le> R"
   5.396 @@ -1110,31 +1126,30 @@
   5.397  
   5.398  lemma ntrancl_Suc [simp]: "ntrancl (Suc n) R = ntrancl n R O (Id \<union> R)"
   5.399  proof
   5.400 -  {
   5.401 -    fix a b
   5.402 -    assume "(a, b) \<in> ntrancl (Suc n) R"
   5.403 -    from this obtain i where "0 < i" "i \<le> Suc (Suc n)" "(a, b) \<in> R ^^ i"
   5.404 +  have "(a, b) \<in> ntrancl n R O (Id \<union> R)" if "(a, b) \<in> ntrancl (Suc n) R" for a b
   5.405 +  proof -
   5.406 +    from that obtain i where "0 < i" "i \<le> Suc (Suc n)" "(a, b) \<in> R ^^ i"
   5.407        unfolding ntrancl_def by auto
   5.408 -    have "(a, b) \<in> ntrancl n R O (Id \<union> R)"
   5.409 +    show ?thesis
   5.410      proof (cases "i = 1")
   5.411        case True
   5.412        from this \<open>(a, b) \<in> R ^^ i\<close> show ?thesis
   5.413 -        unfolding ntrancl_def by auto
   5.414 +        by (auto simp: ntrancl_def)
   5.415      next
   5.416        case False
   5.417 -      from this \<open>0 < i\<close> obtain j where j: "i = Suc j" "0 < j"
   5.418 +      with \<open>0 < i\<close> obtain j where j: "i = Suc j" "0 < j"
   5.419          by (cases i) auto
   5.420 -      from this \<open>(a, b) \<in> R ^^ i\<close> obtain c where c1: "(a, c) \<in> R ^^ j" and c2:"(c, b) \<in> R"
   5.421 +      with \<open>(a, b) \<in> R ^^ i\<close> obtain c where c1: "(a, c) \<in> R ^^ j" and c2: "(c, b) \<in> R"
   5.422          by auto
   5.423        from c1 j \<open>i \<le> Suc (Suc n)\<close> have "(a, c) \<in> ntrancl n R"
   5.424 -        unfolding ntrancl_def by fastforce
   5.425 -      from this c2 show ?thesis by fastforce
   5.426 +        by (fastforce simp: ntrancl_def)
   5.427 +      with c2 show ?thesis by fastforce
   5.428      qed
   5.429 -  }
   5.430 +  qed
   5.431    then show "ntrancl (Suc n) R \<subseteq> ntrancl n R O (Id \<union> R)"
   5.432      by auto
   5.433    show "ntrancl n R O (Id \<union> R) \<subseteq> ntrancl (Suc n) R"
   5.434 -    unfolding ntrancl_def by fastforce
   5.435 +    by (fastforce simp: ntrancl_def)
   5.436  qed
   5.437  
   5.438  lemma [code]: "ntrancl (Suc n) r = (let r' = ntrancl n r in r' \<union> r' O r)"
   5.439 @@ -1169,9 +1184,7 @@
   5.440  qed
   5.441  
   5.442  lemma acyclic_insert [iff]: "acyclic (insert (y, x) r) \<longleftrightarrow> acyclic r \<and> (x, y) \<notin> r\<^sup>*"
   5.443 -  apply (simp add: acyclic_def trancl_insert)
   5.444 -  apply (blast intro: rtrancl_trans)
   5.445 -  done
   5.446 +  by (simp add: acyclic_def trancl_insert) (blast intro: rtrancl_trans)
   5.447  
   5.448  lemma acyclic_converse [iff]: "acyclic (r\<inverse>) \<longleftrightarrow> acyclic r"
   5.449    by (simp add: acyclic_def trancl_converse)
   5.450 @@ -1179,9 +1192,8 @@
   5.451  lemmas acyclicP_converse [iff] = acyclic_converse [to_pred]
   5.452  
   5.453  lemma acyclic_impl_antisym_rtrancl: "acyclic r \<Longrightarrow> antisym (r\<^sup>*)"
   5.454 -  apply (simp add: acyclic_def antisym_def)
   5.455 -  apply (blast elim: rtranclE intro: rtrancl_into_trancl1 rtrancl_trancl_trancl)
   5.456 -  done
   5.457 +  by (simp add: acyclic_def antisym_def)
   5.458 +    (blast elim: rtranclE intro: rtrancl_into_trancl1 rtrancl_trancl_trancl)
   5.459  
   5.460  (* Other direction:
   5.461  acyclic = no loops
   5.462 @@ -1197,7 +1209,6 @@
   5.463  subsection \<open>Setup of transitivity reasoner\<close>
   5.464  
   5.465  ML \<open>
   5.466 -
   5.467  structure Trancl_Tac = Trancl_Tac
   5.468  (
   5.469    val r_into_trancl = @{thm trancl.r_into_trancl};
     6.1 --- a/src/HOL/Wellfounded.thy	Fri Aug 05 16:36:03 2016 +0200
     6.2 +++ b/src/HOL/Wellfounded.thy	Fri Aug 05 18:14:28 2016 +0200
     6.3 @@ -187,9 +187,7 @@
     6.4  text \<open>Well-foundedness of subsets\<close>
     6.5  
     6.6  lemma wf_subset: "wf r \<Longrightarrow> p \<subseteq> r \<Longrightarrow> wf p"
     6.7 -  apply (simp add: wf_eq_minimal)
     6.8 -  apply fast
     6.9 -  done
    6.10 +  by (simp add: wf_eq_minimal) fast
    6.11  
    6.12  lemmas wfP_subset = wf_subset [to_pred]
    6.13  
    6.14 @@ -198,11 +196,12 @@
    6.15  lemma wf_empty [iff]: "wf {}"
    6.16    by (simp add: wf_def)
    6.17  
    6.18 -lemma wfP_empty [iff]:
    6.19 -  "wfP (\<lambda>x y. False)"
    6.20 +lemma wfP_empty [iff]: "wfP (\<lambda>x y. False)"
    6.21  proof -
    6.22 -  have "wfP bot" by (fact wf_empty [to_pred bot_empty_eq2])
    6.23 -  then show ?thesis by (simp add: bot_fun_def)
    6.24 +  have "wfP bot"
    6.25 +    by (fact wf_empty [to_pred bot_empty_eq2])
    6.26 +  then show ?thesis
    6.27 +    by (simp add: bot_fun_def)
    6.28  qed
    6.29  
    6.30  lemma wf_Int1: "wf r \<Longrightarrow> wf (r \<inter> r')"
    6.31 @@ -217,9 +216,10 @@
    6.32    shows "wf R"
    6.33  proof (rule wfI_pf)
    6.34    fix A assume "A \<subseteq> R `` A"
    6.35 -  then have "A \<subseteq> (R ^^ n) `` A" by (induct n) force+
    6.36 -  with \<open>wf (R ^^ n)\<close>
    6.37 -  show "A = {}" by (rule wfE_pf)
    6.38 +  then have "A \<subseteq> (R ^^ n) `` A"
    6.39 +    by (induct n) force+
    6.40 +  with \<open>wf (R ^^ n)\<close> show "A = {}"
    6.41 +    by (rule wfE_pf)
    6.42  qed
    6.43  
    6.44  text \<open>Well-foundedness of \<open>insert\<close>.\<close>
    6.45 @@ -257,7 +257,7 @@
    6.46    apply (case_tac "\<exists>p. f p \<in> Q")
    6.47     apply (erule_tac x = "{p. f p \<in> Q}" in allE)
    6.48     apply (fast dest: inj_onD)
    6.49 -apply blast
    6.50 +  apply blast
    6.51    done
    6.52  
    6.53  
    6.54 @@ -379,7 +379,7 @@
    6.55    qed
    6.56  qed
    6.57  
    6.58 -lemma wf_comp_self: "wf R = wf (R O R)"  \<comment> \<open>special case\<close>
    6.59 +lemma wf_comp_self: "wf R \<longleftrightarrow> wf (R O R)"  \<comment> \<open>special case\<close>
    6.60    by (rule wf_union_merge [where S = "{}", simplified])
    6.61  
    6.62  
    6.63 @@ -390,12 +390,13 @@
    6.64  lemma qc_wf_relto_iff:
    6.65    assumes "R O S \<subseteq> (R \<union> S)\<^sup>* O R" \<comment> \<open>R quasi-commutes over S\<close>
    6.66    shows "wf (S\<^sup>* O R O S\<^sup>*) \<longleftrightarrow> wf R"
    6.67 -  (is "wf ?S \<longleftrightarrow> _")
    6.68 +    (is "wf ?S \<longleftrightarrow> _")
    6.69  proof
    6.70    show "wf R" if "wf ?S"
    6.71    proof -
    6.72      have "R \<subseteq> ?S" by auto
    6.73 -    with that show "wf R" using wf_subset by auto
    6.74 +    with wf_subset [of ?S] that show "wf R"
    6.75 +      by auto
    6.76    qed
    6.77  next
    6.78    show "wf ?S" if "wf R"
    6.79 @@ -607,10 +608,7 @@
    6.80  qed
    6.81  
    6.82  lemma accp_downwards_aux: "r\<^sup>*\<^sup>* b a \<Longrightarrow> accp r a \<longrightarrow> accp r b"
    6.83 -  apply (erule rtranclp_induct)
    6.84 -   apply blast
    6.85 -  apply (blast dest: accp_downward)
    6.86 -  done
    6.87 +  by (erule rtranclp_induct) (blast dest: accp_downward)+
    6.88  
    6.89  theorem accp_downwards: "accp r a \<Longrightarrow> r\<^sup>*\<^sup>* b a \<Longrightarrow> accp r b"
    6.90    by (blast dest: accp_downwards_aux)
    6.91 @@ -691,7 +689,7 @@
    6.92  text \<open>Inverse Image\<close>
    6.93  
    6.94  lemma wf_inv_image [simp,intro!]: "wf r \<Longrightarrow> wf (inv_image r f)"
    6.95 - for f :: "'a \<Rightarrow> 'b"
    6.96 +  for f :: "'a \<Rightarrow> 'b"
    6.97    apply (simp add: inv_image_def wf_eq_minimal)
    6.98    apply clarify
    6.99    apply (subgoal_tac "\<exists>w::'b. w \<in> {w. \<exists>x::'a. x \<in> Q \<and> f x = w}")
   6.100 @@ -776,7 +774,7 @@
   6.101    done
   6.102  
   6.103  lemma trans_finite_psubset: "trans finite_psubset"
   6.104 -  by (auto simp add: finite_psubset_def less_le trans_def)
   6.105 +  by (auto simp: finite_psubset_def less_le trans_def)
   6.106  
   6.107  lemma in_finite_psubset[simp]: "(A, B) \<in> finite_psubset \<longleftrightarrow> A \<subset> B \<and> finite B"
   6.108    unfolding finite_psubset_def by auto