diff --git a/src/HOL/Analysis/Abstract_Topology_2.thy b/src/HOL/Analysis/Abstract_Topology_2.thy
--- a/src/HOL/Analysis/Abstract_Topology_2.thy
+++ b/src/HOL/Analysis/Abstract_Topology_2.thy
@@ -1,1616 +1,1616 @@
 (*  Author:     L C Paulson, University of Cambridge
     Author:     Amine Chaieb, University of Cambridge
     Author:     Robert Himmelmann, TU Muenchen
     Author:     Brian Huffman, Portland State University
 *)
 
 section \<open>Abstract Topology 2\<close>
 
 theory Abstract_Topology_2
   imports
     Elementary_Topology
     Abstract_Topology
     "HOL-Library.Indicator_Function"
 begin
 
 text \<open>Combination of Elementary and Abstract Topology\<close>
 
 (* FIXME: move elsewhere *)
 
 lemma approachable_lt_le: "(\<exists>(d::real) > 0. \<forall>x. f x < d \<longrightarrow> P x) \<longleftrightarrow> (\<exists>d>0. \<forall>x. f x \<le> d \<longrightarrow> P x)"
   apply auto
   apply (rule_tac x="d/2" in exI)
   apply auto
   done
 
 lemma approachable_lt_le2:  \<comment> \<open>like the above, but pushes aside an extra formula\<close>
     "(\<exists>(d::real) > 0. \<forall>x. Q x \<longrightarrow> f x < d \<longrightarrow> P x) \<longleftrightarrow> (\<exists>d>0. \<forall>x. f x \<le> d \<longrightarrow> Q x \<longrightarrow> P x)"
   apply auto
   apply (rule_tac x="d/2" in exI, auto)
   done
 
 lemma triangle_lemma:
   fixes x y z :: real
   assumes x: "0 \<le> x"
     and y: "0 \<le> y"
     and z: "0 \<le> z"
     and xy: "x\<^sup>2 \<le> y\<^sup>2 + z\<^sup>2"
   shows "x \<le> y + z"
 proof -
   have "y\<^sup>2 + z\<^sup>2 \<le> y\<^sup>2 + 2 * y * z + z\<^sup>2"
     using z y by simp
   with xy have th: "x\<^sup>2 \<le> (y + z)\<^sup>2"
     by (simp add: power2_eq_square field_simps)
   from y z have yz: "y + z \<ge> 0"
     by arith
   from power2_le_imp_le[OF th yz] show ?thesis .
 qed
 
 lemma isCont_indicator:
   fixes x :: "'a::t2_space"
   shows "isCont (indicator A :: 'a \<Rightarrow> real) x = (x \<notin> frontier A)"
 proof auto
   fix x
   assume cts_at: "isCont (indicator A :: 'a \<Rightarrow> real) x" and fr: "x \<in> frontier A"
   with continuous_at_open have 1: "\<forall>V::real set. open V \<and> indicator A x \<in> V \<longrightarrow>
     (\<exists>U::'a set. open U \<and> x \<in> U \<and> (\<forall>y\<in>U. indicator A y \<in> V))" by auto
   show False
   proof (cases "x \<in> A")
     assume x: "x \<in> A"
     hence "indicator A x \<in> ({0<..<2} :: real set)" by simp
     hence "\<exists>U. open U \<and> x \<in> U \<and> (\<forall>y\<in>U. indicator A y \<in> ({0<..<2} :: real set))"
       using 1 open_greaterThanLessThan by blast
     then guess U .. note U = this
     hence "\<forall>y\<in>U. indicator A y > (0::real)"
       unfolding greaterThanLessThan_def by auto
     hence "U \<subseteq> A" using indicator_eq_0_iff by force
     hence "x \<in> interior A" using U interiorI by auto
     thus ?thesis using fr unfolding frontier_def by simp
   next
     assume x: "x \<notin> A"
     hence "indicator A x \<in> ({-1<..<1} :: real set)" by simp
     hence "\<exists>U. open U \<and> x \<in> U \<and> (\<forall>y\<in>U. indicator A y \<in> ({-1<..<1} :: real set))"
       using 1 open_greaterThanLessThan by blast
     then guess U .. note U = this
     hence "\<forall>y\<in>U. indicator A y < (1::real)"
       unfolding greaterThanLessThan_def by auto
     hence "U \<subseteq> -A" by auto
     hence "x \<in> interior (-A)" using U interiorI by auto
     thus ?thesis using fr interior_complement unfolding frontier_def by auto
   qed
 next
   assume nfr: "x \<notin> frontier A"
   hence "x \<in> interior A \<or> x \<in> interior (-A)"
     by (auto simp: frontier_def closure_interior)
   thus "isCont ((indicator A)::'a \<Rightarrow> real) x"
   proof
     assume int: "x \<in> interior A"
     then obtain U where U: "open U" "x \<in> U" "U \<subseteq> A" unfolding interior_def by auto
     hence "\<forall>y\<in>U. indicator A y = (1::real)" unfolding indicator_def by auto
     hence "continuous_on U (indicator A)" by (simp add: indicator_eq_1_iff)
     thus ?thesis using U continuous_on_eq_continuous_at by auto
   next
     assume ext: "x \<in> interior (-A)"
     then obtain U where U: "open U" "x \<in> U" "U \<subseteq> -A" unfolding interior_def by auto
     then have "continuous_on U (indicator A)"
       using continuous_on_topological by (auto simp: subset_iff)
     thus ?thesis using U continuous_on_eq_continuous_at by auto
   qed
 qed
 
 lemma closedin_limpt:
   "closedin (top_of_set T) S \<longleftrightarrow> S \<subseteq> T \<and> (\<forall>x. x islimpt S \<and> x \<in> T \<longrightarrow> x \<in> S)"
   apply (simp add: closedin_closed, safe)
    apply (simp add: closed_limpt islimpt_subset)
   apply (rule_tac x="closure S" in exI, simp)
   apply (force simp: closure_def)
   done
 
 lemma closedin_closed_eq: "closed S \<Longrightarrow> closedin (top_of_set S) T \<longleftrightarrow> closed T \<and> T \<subseteq> S"
   by (meson closedin_limpt closed_subset closedin_closed_trans)
 
 lemma connected_closed_set:
    "closed S
     \<Longrightarrow> connected S \<longleftrightarrow> (\<nexists>A B. closed A \<and> closed B \<and> A \<noteq> {} \<and> B \<noteq> {} \<and> A \<union> B = S \<and> A \<inter> B = {})"
   unfolding connected_closedin_eq closedin_closed_eq connected_closedin_eq by blast
 
 text \<open>If a connnected set is written as the union of two nonempty closed sets, then these sets
 have to intersect.\<close>
 
 lemma connected_as_closed_union:
   assumes "connected C" "C = A \<union> B" "closed A" "closed B" "A \<noteq> {}" "B \<noteq> {}"
   shows "A \<inter> B \<noteq> {}"
 by (metis assms closed_Un connected_closed_set)
 
 lemma closedin_subset_trans:
   "closedin (top_of_set U) S \<Longrightarrow> S \<subseteq> T \<Longrightarrow> T \<subseteq> U \<Longrightarrow>
     closedin (top_of_set T) S"
   by (meson closedin_limpt subset_iff)
 
 lemma openin_subset_trans:
   "openin (top_of_set U) S \<Longrightarrow> S \<subseteq> T \<Longrightarrow> T \<subseteq> U \<Longrightarrow>
     openin (top_of_set T) S"
   by (auto simp: openin_open)
 
 lemma closedin_compact:
    "\<lbrakk>compact S; closedin (top_of_set S) T\<rbrakk> \<Longrightarrow> compact T"
 by (metis closedin_closed compact_Int_closed)
 
 lemma closedin_compact_eq:
   fixes S :: "'a::t2_space set"
   shows
    "compact S
          \<Longrightarrow> (closedin (top_of_set S) T \<longleftrightarrow>
               compact T \<and> T \<subseteq> S)"
 by (metis closedin_imp_subset closedin_compact closed_subset compact_imp_closed)
 
 
 subsection \<open>Closure\<close>
 
 lemma euclidean_closure_of [simp]: "euclidean closure_of S = closure S"
   by (auto simp: closure_of_def closure_def islimpt_def)
 
 lemma closure_openin_Int_closure:
   assumes ope: "openin (top_of_set U) S" and "T \<subseteq> U"
   shows "closure(S \<inter> closure T) = closure(S \<inter> T)"
 proof
   obtain V where "open V" and S: "S = U \<inter> V"
     using ope using openin_open by metis
   show "closure (S \<inter> closure T) \<subseteq> closure (S \<inter> T)"
     proof (clarsimp simp: S)
       fix x
       assume  "x \<in> closure (U \<inter> V \<inter> closure T)"
       then have "V \<inter> closure T \<subseteq> A \<Longrightarrow> x \<in> closure A" for A
           by (metis closure_mono subsetD inf.coboundedI2 inf_assoc)
       then have "x \<in> closure (T \<inter> V)"
          by (metis \<open>open V\<close> closure_closure inf_commute open_Int_closure_subset)
       then show "x \<in> closure (U \<inter> V \<inter> T)"
         by (metis \<open>T \<subseteq> U\<close> inf.absorb_iff2 inf_assoc inf_commute)
     qed
 next
   show "closure (S \<inter> T) \<subseteq> closure (S \<inter> closure T)"
     by (meson Int_mono closure_mono closure_subset order_refl)
 qed
 
 corollary infinite_openin:
   fixes S :: "'a :: t1_space set"
   shows "\<lbrakk>openin (top_of_set U) S; x \<in> S; x islimpt U\<rbrakk> \<Longrightarrow> infinite S"
   by (clarsimp simp add: openin_open islimpt_eq_acc_point inf_commute)
 
 lemma closure_Int_ballI:
   assumes "\<And>U. \<lbrakk>openin (top_of_set S) U; U \<noteq> {}\<rbrakk> \<Longrightarrow> T \<inter> U \<noteq> {}"
   shows "S \<subseteq> closure T"
 proof (clarsimp simp: closure_iff_nhds_not_empty)
   fix x and A and V
   assume "x \<in> S" "V \<subseteq> A" "open V" "x \<in> V" "T \<inter> A = {}"
   then have "openin (top_of_set S) (A \<inter> V \<inter> S)"
     by (auto simp: openin_open intro!: exI[where x="V"])
   moreover have "A \<inter> V \<inter> S \<noteq> {}" using \<open>x \<in> V\<close> \<open>V \<subseteq> A\<close> \<open>x \<in> S\<close>
     by auto
   ultimately have "T \<inter> (A \<inter> V \<inter> S) \<noteq> {}"
     by (rule assms)
   with \<open>T \<inter> A = {}\<close> show False by auto
 qed
 
 
 subsection \<open>Frontier\<close>
 
 lemma euclidean_interior_of [simp]: "euclidean interior_of S = interior S"
   by (auto simp: interior_of_def interior_def)
 
 lemma euclidean_frontier_of [simp]: "euclidean frontier_of S = frontier S"
   by (auto simp: frontier_of_def frontier_def)
 
 lemma connected_Int_frontier:
      "\<lbrakk>connected s; s \<inter> t \<noteq> {}; s - t \<noteq> {}\<rbrakk> \<Longrightarrow> (s \<inter> frontier t \<noteq> {})"
   apply (simp add: frontier_interiors connected_openin, safe)
   apply (drule_tac x="s \<inter> interior t" in spec, safe)
    apply (drule_tac [2] x="s \<inter> interior (-t)" in spec)
    apply (auto simp: disjoint_eq_subset_Compl dest: interior_subset [THEN subsetD])
   done
 
 subsection \<open>Compactness\<close>
 
 lemma openin_delete:
   fixes a :: "'a :: t1_space"
   shows "openin (top_of_set u) s
          \<Longrightarrow> openin (top_of_set u) (s - {a})"
 by (metis Int_Diff open_delete openin_open)
 
 lemma compact_eq_openin_cover:
   "compact S \<longleftrightarrow>
     (\<forall>C. (\<forall>c\<in>C. openin (top_of_set S) c) \<and> S \<subseteq> \<Union>C \<longrightarrow>
       (\<exists>D\<subseteq>C. finite D \<and> S \<subseteq> \<Union>D))"
 proof safe
   fix C
   assume "compact S" and "\<forall>c\<in>C. openin (top_of_set S) c" and "S \<subseteq> \<Union>C"
   then have "\<forall>c\<in>{T. open T \<and> S \<inter> T \<in> C}. open c" and "S \<subseteq> \<Union>{T. open T \<and> S \<inter> T \<in> C}"
     unfolding openin_open by force+
   with \<open>compact S\<close> obtain D where "D \<subseteq> {T. open T \<and> S \<inter> T \<in> C}" and "finite D" and "S \<subseteq> \<Union>D"
     by (meson compactE)
   then have "image (\<lambda>T. S \<inter> T) D \<subseteq> C \<and> finite (image (\<lambda>T. S \<inter> T) D) \<and> S \<subseteq> \<Union>(image (\<lambda>T. S \<inter> T) D)"
     by auto
   then show "\<exists>D\<subseteq>C. finite D \<and> S \<subseteq> \<Union>D" ..
 next
   assume 1: "\<forall>C. (\<forall>c\<in>C. openin (top_of_set S) c) \<and> S \<subseteq> \<Union>C \<longrightarrow>
         (\<exists>D\<subseteq>C. finite D \<and> S \<subseteq> \<Union>D)"
   show "compact S"
   proof (rule compactI)
     fix C
     let ?C = "image (\<lambda>T. S \<inter> T) C"
     assume "\<forall>t\<in>C. open t" and "S \<subseteq> \<Union>C"
     then have "(\<forall>c\<in>?C. openin (top_of_set S) c) \<and> S \<subseteq> \<Union>?C"
       unfolding openin_open by auto
     with 1 obtain D where "D \<subseteq> ?C" and "finite D" and "S \<subseteq> \<Union>D"
       by metis
     let ?D = "inv_into C (\<lambda>T. S \<inter> T) ` D"
     have "?D \<subseteq> C \<and> finite ?D \<and> S \<subseteq> \<Union>?D"
     proof (intro conjI)
       from \<open>D \<subseteq> ?C\<close> show "?D \<subseteq> C"
         by (fast intro: inv_into_into)
       from \<open>finite D\<close> show "finite ?D"
         by (rule finite_imageI)
       from \<open>S \<subseteq> \<Union>D\<close> show "S \<subseteq> \<Union>?D"
         apply (rule subset_trans, clarsimp)
         apply (frule subsetD [OF \<open>D \<subseteq> ?C\<close>, THEN f_inv_into_f])
         apply (erule rev_bexI, fast)
         done
     qed
     then show "\<exists>D\<subseteq>C. finite D \<and> S \<subseteq> \<Union>D" ..
   qed
 qed
 
 
 subsection \<open>Continuity\<close>
 
 lemma interior_image_subset:
   assumes "inj f" "\<And>x. continuous (at x) f"
   shows "interior (f ` S) \<subseteq> f ` (interior S)"
 proof
   fix x assume "x \<in> interior (f ` S)"
   then obtain T where as: "open T" "x \<in> T" "T \<subseteq> f ` S" ..
   then have "x \<in> f ` S" by auto
   then obtain y where y: "y \<in> S" "x = f y" by auto
   have "open (f -` T)"
     using assms \<open>open T\<close> by (simp add: continuous_at_imp_continuous_on open_vimage)
   moreover have "y \<in> vimage f T"
     using \<open>x = f y\<close> \<open>x \<in> T\<close> by simp
   moreover have "vimage f T \<subseteq> S"
     using \<open>T \<subseteq> image f S\<close> \<open>inj f\<close> unfolding inj_on_def subset_eq by auto
   ultimately have "y \<in> interior S" ..
   with \<open>x = f y\<close> show "x \<in> f ` interior S" ..
 qed
 
 subsection\<^marker>\<open>tag unimportant\<close> \<open>Equality of continuous functions on closure and related results\<close>
 
 lemma continuous_closedin_preimage_constant:
   fixes f :: "_ \<Rightarrow> 'b::t1_space"
   shows "continuous_on S f \<Longrightarrow> closedin (top_of_set S) {x \<in> S. f x = a}"
   using continuous_closedin_preimage[of S f "{a}"] by (simp add: vimage_def Collect_conj_eq)
 
 lemma continuous_closed_preimage_constant:
   fixes f :: "_ \<Rightarrow> 'b::t1_space"
   shows "continuous_on S f \<Longrightarrow> closed S \<Longrightarrow> closed {x \<in> S. f x = a}"
   using continuous_closed_preimage[of S f "{a}"] by (simp add: vimage_def Collect_conj_eq)
 
 lemma continuous_constant_on_closure:
   fixes f :: "_ \<Rightarrow> 'b::t1_space"
   assumes "continuous_on (closure S) f"
       and "\<And>x. x \<in> S \<Longrightarrow> f x = a"
       and "x \<in> closure S"
   shows "f x = a"
     using continuous_closed_preimage_constant[of "closure S" f a]
       assms closure_minimal[of S "{x \<in> closure S. f x = a}"] closure_subset
     unfolding subset_eq
     by auto
 
 lemma image_closure_subset:
   assumes contf: "continuous_on (closure S) f"
     and "closed T"
     and "(f ` S) \<subseteq> T"
   shows "f ` (closure S) \<subseteq> T"
 proof -
   have "S \<subseteq> {x \<in> closure S. f x \<in> T}"
     using assms(3) closure_subset by auto
   moreover have "closed (closure S \<inter> f -` T)"
     using continuous_closed_preimage[OF contf] \<open>closed T\<close> by auto
   ultimately have "closure S = (closure S \<inter> f -` T)"
     using closure_minimal[of S "(closure S \<inter> f -` T)"] by auto
   then show ?thesis by auto
 qed
 
 subsection\<^marker>\<open>tag unimportant\<close> \<open>A function constant on a set\<close>
 
 definition constant_on  (infixl "(constant'_on)" 50)
   where "f constant_on A \<equiv> \<exists>y. \<forall>x\<in>A. f x = y"
 
 lemma constant_on_subset: "\<lbrakk>f constant_on A; B \<subseteq> A\<rbrakk> \<Longrightarrow> f constant_on B"
   unfolding constant_on_def by blast
 
 lemma injective_not_constant:
   fixes S :: "'a::{perfect_space} set"
   shows "\<lbrakk>open S; inj_on f S; f constant_on S\<rbrakk> \<Longrightarrow> S = {}"
 unfolding constant_on_def
 by (metis equals0I inj_on_contraD islimpt_UNIV islimpt_def)
 
 lemma constant_on_closureI:
   fixes f :: "_ \<Rightarrow> 'b::t1_space"
   assumes cof: "f constant_on S" and contf: "continuous_on (closure S) f"
     shows "f constant_on (closure S)"
 using continuous_constant_on_closure [OF contf] cof unfolding constant_on_def
 by metis
 
 
 subsection\<^marker>\<open>tag unimportant\<close> \<open>Continuity relative to a union.\<close>
 
 lemma continuous_on_Un_local:
     "\<lbrakk>closedin (top_of_set (s \<union> t)) s; closedin (top_of_set (s \<union> t)) t;
       continuous_on s f; continuous_on t f\<rbrakk>
      \<Longrightarrow> continuous_on (s \<union> t) f"
   unfolding continuous_on closedin_limpt
   by (metis Lim_trivial_limit Lim_within_union Un_iff trivial_limit_within)
 
 lemma continuous_on_cases_local:
      "\<lbrakk>closedin (top_of_set (s \<union> t)) s; closedin (top_of_set (s \<union> t)) t;
        continuous_on s f; continuous_on t g;
        \<And>x. \<lbrakk>x \<in> s \<and> \<not>P x \<or> x \<in> t \<and> P x\<rbrakk> \<Longrightarrow> f x = g x\<rbrakk>
       \<Longrightarrow> continuous_on (s \<union> t) (\<lambda>x. if P x then f x else g x)"
   by (rule continuous_on_Un_local) (auto intro: continuous_on_eq)
 
 lemma continuous_on_cases_le:
   fixes h :: "'a :: topological_space \<Rightarrow> real"
   assumes "continuous_on {t \<in> s. h t \<le> a} f"
       and "continuous_on {t \<in> s. a \<le> h t} g"
       and h: "continuous_on s h"
       and "\<And>t. \<lbrakk>t \<in> s; h t = a\<rbrakk> \<Longrightarrow> f t = g t"
     shows "continuous_on s (\<lambda>t. if h t \<le> a then f(t) else g(t))"
 proof -
   have s: "s = (s \<inter> h -` atMost a) \<union> (s \<inter> h -` atLeast a)"
     by force
   have 1: "closedin (top_of_set s) (s \<inter> h -` atMost a)"
     by (rule continuous_closedin_preimage [OF h closed_atMost])
   have 2: "closedin (top_of_set s) (s \<inter> h -` atLeast a)"
     by (rule continuous_closedin_preimage [OF h closed_atLeast])
   have eq: "s \<inter> h -` {..a} = {t \<in> s. h t \<le> a}" "s \<inter> h -` {a..} = {t \<in> s. a \<le> h t}"
     by auto
   show ?thesis
     apply (rule continuous_on_subset [of s, OF _ order_refl])
     apply (subst s)
     apply (rule continuous_on_cases_local)
     using 1 2 s assms apply (auto simp: eq)
     done
 qed
 
 lemma continuous_on_cases_1:
   fixes s :: "real set"
   assumes "continuous_on {t \<in> s. t \<le> a} f"
       and "continuous_on {t \<in> s. a \<le> t} g"
       and "a \<in> s \<Longrightarrow> f a = g a"
     shows "continuous_on s (\<lambda>t. if t \<le> a then f(t) else g(t))"
 using assms
 by (auto intro: continuous_on_cases_le [where h = id, simplified])
 
 
 subsection\<^marker>\<open>tag unimportant\<close>\<open>Inverse function property for open/closed maps\<close>
 
 lemma continuous_on_inverse_open_map:
   assumes contf: "continuous_on S f"
     and imf: "f ` S = T"
     and injf: "\<And>x. x \<in> S \<Longrightarrow> g (f x) = x"
     and oo: "\<And>U. openin (top_of_set S) U \<Longrightarrow> openin (top_of_set T) (f ` U)"
   shows "continuous_on T g"
 proof -
   from imf injf have gTS: "g ` T = S"
     by force
   from imf injf have fU: "U \<subseteq> S \<Longrightarrow> (f ` U) = T \<inter> g -` U" for U
     by force
   show ?thesis
     by (simp add: continuous_on_open [of T g] gTS) (metis openin_imp_subset fU oo)
 qed
 
 lemma continuous_on_inverse_closed_map:
   assumes contf: "continuous_on S f"
     and imf: "f ` S = T"
     and injf: "\<And>x. x \<in> S \<Longrightarrow> g(f x) = x"
     and oo: "\<And>U. closedin (top_of_set S) U \<Longrightarrow> closedin (top_of_set T) (f ` U)"
   shows "continuous_on T g"
 proof -
   from imf injf have gTS: "g ` T = S"
     by force
   from imf injf have fU: "U \<subseteq> S \<Longrightarrow> (f ` U) = T \<inter> g -` U" for U
     by force
   show ?thesis
     by (simp add: continuous_on_closed [of T g] gTS) (metis closedin_imp_subset fU oo)
 qed
 
 lemma homeomorphism_injective_open_map:
   assumes contf: "continuous_on S f"
     and imf: "f ` S = T"
     and injf: "inj_on f S"
     and oo: "\<And>U. openin (top_of_set S) U \<Longrightarrow> openin (top_of_set T) (f ` U)"
   obtains g where "homeomorphism S T f g"
 proof
   have "continuous_on T (inv_into S f)"
     by (metis contf continuous_on_inverse_open_map imf injf inv_into_f_f oo)
   with imf injf contf show "homeomorphism S T f (inv_into S f)"
     by (auto simp: homeomorphism_def)
 qed
 
 lemma homeomorphism_injective_closed_map:
   assumes contf: "continuous_on S f"
     and imf: "f ` S = T"
     and injf: "inj_on f S"
     and oo: "\<And>U. closedin (top_of_set S) U \<Longrightarrow> closedin (top_of_set T) (f ` U)"
   obtains g where "homeomorphism S T f g"
 proof
   have "continuous_on T (inv_into S f)"
     by (metis contf continuous_on_inverse_closed_map imf injf inv_into_f_f oo)
   with imf injf contf show "homeomorphism S T f (inv_into S f)"
     by (auto simp: homeomorphism_def)
 qed
 
 lemma homeomorphism_imp_open_map:
   assumes hom: "homeomorphism S T f g"
     and oo: "openin (top_of_set S) U"
   shows "openin (top_of_set T) (f ` U)"
 proof -
   from hom oo have [simp]: "f ` U = T \<inter> g -` U"
     using openin_subset by (fastforce simp: homeomorphism_def rev_image_eqI)
   from hom have "continuous_on T g"
     unfolding homeomorphism_def by blast
   moreover have "g ` T = S"
     by (metis hom homeomorphism_def)
   ultimately show ?thesis
     by (simp add: continuous_on_open oo)
 qed
 
 lemma homeomorphism_imp_closed_map:
   assumes hom: "homeomorphism S T f g"
     and oo: "closedin (top_of_set S) U"
   shows "closedin (top_of_set T) (f ` U)"
 proof -
   from hom oo have [simp]: "f ` U = T \<inter> g -` U"
     using closedin_subset by (fastforce simp: homeomorphism_def rev_image_eqI)
   from hom have "continuous_on T g"
     unfolding homeomorphism_def by blast
   moreover have "g ` T = S"
     by (metis hom homeomorphism_def)
   ultimately show ?thesis
     by (simp add: continuous_on_closed oo)
 qed
 
 subsection\<^marker>\<open>tag unimportant\<close> \<open>Seperability\<close>
 
 lemma subset_second_countable:
   obtains \<B> :: "'a:: second_countable_topology set set"
     where "countable \<B>"
           "{} \<notin> \<B>"
           "\<And>C. C \<in> \<B> \<Longrightarrow> openin(top_of_set S) C"
           "\<And>T. openin(top_of_set S) T \<Longrightarrow> \<exists>\<U>. \<U> \<subseteq> \<B> \<and> T = \<Union>\<U>"
 proof -
   obtain \<B> :: "'a set set"
     where "countable \<B>"
       and opeB: "\<And>C. C \<in> \<B> \<Longrightarrow> openin(top_of_set S) C"
       and \<B>:    "\<And>T. openin(top_of_set S) T \<Longrightarrow> \<exists>\<U>. \<U> \<subseteq> \<B> \<and> T = \<Union>\<U>"
   proof -
     obtain \<C> :: "'a set set"
       where "countable \<C>" and ope: "\<And>C. C \<in> \<C> \<Longrightarrow> open C"
         and \<C>: "\<And>S. open S \<Longrightarrow> \<exists>U. U \<subseteq> \<C> \<and> S = \<Union>U"
       by (metis univ_second_countable that)
     show ?thesis
     proof
       show "countable ((\<lambda>C. S \<inter> C) ` \<C>)"
         by (simp add: \<open>countable \<C>\<close>)
       show "\<And>C. C \<in> (\<inter>) S ` \<C> \<Longrightarrow> openin (top_of_set S) C"
         using ope by auto
       show "\<And>T. openin (top_of_set S) T \<Longrightarrow> \<exists>\<U>\<subseteq>(\<inter>) S ` \<C>. T = \<Union>\<U>"
         by (metis \<C> image_mono inf_Sup openin_open)
     qed
   qed
   show ?thesis
   proof
     show "countable (\<B> - {{}})"
       using \<open>countable \<B>\<close> by blast
     show "\<And>C. \<lbrakk>C \<in> \<B> - {{}}\<rbrakk> \<Longrightarrow> openin (top_of_set S) C"
       by (simp add: \<open>\<And>C. C \<in> \<B> \<Longrightarrow> openin (top_of_set S) C\<close>)
     show "\<exists>\<U>\<subseteq>\<B> - {{}}. T = \<Union>\<U>" if "openin (top_of_set S) T" for T
       using \<B> [OF that]
       apply clarify
       apply (rule_tac x="\<U> - {{}}" in exI, auto)
         done
   qed auto
 qed
 
 lemma Lindelof_openin:
   fixes \<F> :: "'a::second_countable_topology set set"
   assumes "\<And>S. S \<in> \<F> \<Longrightarrow> openin (top_of_set U) S"
   obtains \<F>' where "\<F>' \<subseteq> \<F>" "countable \<F>'" "\<Union>\<F>' = \<Union>\<F>"
 proof -
   have "\<And>S. S \<in> \<F> \<Longrightarrow> \<exists>T. open T \<and> S = U \<inter> T"
     using assms by (simp add: openin_open)
   then obtain tf where tf: "\<And>S. S \<in> \<F> \<Longrightarrow> open (tf S) \<and> (S = U \<inter> tf S)"
     by metis
   have [simp]: "\<And>\<F>'. \<F>' \<subseteq> \<F> \<Longrightarrow> \<Union>\<F>' = U \<inter> \<Union>(tf ` \<F>')"
     using tf by fastforce
   obtain \<G> where "countable \<G> \<and> \<G> \<subseteq> tf ` \<F>" "\<Union>\<G> = \<Union>(tf ` \<F>)"
     using tf by (force intro: Lindelof [of "tf ` \<F>"])
   then obtain \<F>' where \<F>': "\<F>' \<subseteq> \<F>" "countable \<F>'" "\<Union>\<F>' = \<Union>\<F>"
     by (clarsimp simp add: countable_subset_image)
   then show ?thesis ..
 qed
 
 
 subsection\<^marker>\<open>tag unimportant\<close>\<open>Closed Maps\<close>
 
 lemma continuous_imp_closed_map:
   fixes f :: "'a::t2_space \<Rightarrow> 'b::t2_space"
   assumes "closedin (top_of_set S) U"
           "continuous_on S f" "f ` S = T" "compact S"
     shows "closedin (top_of_set T) (f ` U)"
   by (metis assms closedin_compact_eq compact_continuous_image continuous_on_subset subset_image_iff)
 
 lemma closed_map_restrict:
   assumes cloU: "closedin (top_of_set (S \<inter> f -` T')) U"
     and cc: "\<And>U. closedin (top_of_set S) U \<Longrightarrow> closedin (top_of_set T) (f ` U)"
     and "T' \<subseteq> T"
   shows "closedin (top_of_set T') (f ` U)"
 proof -
   obtain V where "closed V" "U = S \<inter> f -` T' \<inter> V"
     using cloU by (auto simp: closedin_closed)
   with cc [of "S \<inter> V"] \<open>T' \<subseteq> T\<close> show ?thesis
     by (fastforce simp add: closedin_closed)
 qed
 
 subsection\<^marker>\<open>tag unimportant\<close>\<open>Open Maps\<close>
 
 lemma open_map_restrict:
   assumes opeU: "openin (top_of_set (S \<inter> f -` T')) U"
     and oo: "\<And>U. openin (top_of_set S) U \<Longrightarrow> openin (top_of_set T) (f ` U)"
     and "T' \<subseteq> T"
   shows "openin (top_of_set T') (f ` U)"
 proof -
   obtain V where "open V" "U = S \<inter> f -` T' \<inter> V"
     using opeU by (auto simp: openin_open)
   with oo [of "S \<inter> V"] \<open>T' \<subseteq> T\<close> show ?thesis
     by (fastforce simp add: openin_open)
 qed
 
 
 subsection\<^marker>\<open>tag unimportant\<close>\<open>Quotient maps\<close>
 
 lemma quotient_map_imp_continuous_open:
   assumes T: "f ` S \<subseteq> T"
       and ope: "\<And>U. U \<subseteq> T
               \<Longrightarrow> (openin (top_of_set S) (S \<inter> f -` U) \<longleftrightarrow>
                    openin (top_of_set T) U)"
     shows "continuous_on S f"
 proof -
   have [simp]: "S \<inter> f -` f ` S = S" by auto
   show ?thesis
     using ope [OF T]
     apply (simp add: continuous_on_open)
     by (meson ope openin_imp_subset openin_trans)
 qed
 
 lemma quotient_map_imp_continuous_closed:
   assumes T: "f ` S \<subseteq> T"
       and ope: "\<And>U. U \<subseteq> T
                   \<Longrightarrow> (closedin (top_of_set S) (S \<inter> f -` U) \<longleftrightarrow>
                        closedin (top_of_set T) U)"
     shows "continuous_on S f"
 proof -
   have [simp]: "S \<inter> f -` f ` S = S" by auto
   show ?thesis
     using ope [OF T]
     apply (simp add: continuous_on_closed)
     by (metis (no_types, lifting) ope closedin_imp_subset closedin_trans)
 qed
 
 lemma open_map_imp_quotient_map:
   assumes contf: "continuous_on S f"
       and T: "T \<subseteq> f ` S"
       and ope: "\<And>T. openin (top_of_set S) T
                    \<Longrightarrow> openin (top_of_set (f ` S)) (f ` T)"
     shows "openin (top_of_set S) (S \<inter> f -` T) =
            openin (top_of_set (f ` S)) T"
 proof -
   have "T = f ` (S \<inter> f -` T)"
     using T by blast
   then show ?thesis
     using "ope" contf continuous_on_open by metis
 qed
 
 lemma closed_map_imp_quotient_map:
   assumes contf: "continuous_on S f"
       and T: "T \<subseteq> f ` S"
       and ope: "\<And>T. closedin (top_of_set S) T
               \<Longrightarrow> closedin (top_of_set (f ` S)) (f ` T)"
     shows "openin (top_of_set S) (S \<inter> f -` T) \<longleftrightarrow>
            openin (top_of_set (f ` S)) T"
           (is "?lhs = ?rhs")
 proof
   assume ?lhs
   then have *: "closedin (top_of_set S) (S - (S \<inter> f -` T))"
     using closedin_diff by fastforce
   have [simp]: "(f ` S - f ` (S - (S \<inter> f -` T))) = T"
     using T by blast
   show ?rhs
     using ope [OF *, unfolded closedin_def] by auto
 next
   assume ?rhs
   with contf show ?lhs
     by (auto simp: continuous_on_open)
 qed
 
 lemma continuous_right_inverse_imp_quotient_map:
   assumes contf: "continuous_on S f" and imf: "f ` S \<subseteq> T"
       and contg: "continuous_on T g" and img: "g ` T \<subseteq> S"
       and fg [simp]: "\<And>y. y \<in> T \<Longrightarrow> f(g y) = y"
       and U: "U \<subseteq> T"
     shows "openin (top_of_set S) (S \<inter> f -` U) \<longleftrightarrow>
            openin (top_of_set T) U"
           (is "?lhs = ?rhs")
 proof -
   have f: "\<And>Z. openin (top_of_set (f ` S)) Z \<Longrightarrow>
                 openin (top_of_set S) (S \<inter> f -` Z)"
   and  g: "\<And>Z. openin (top_of_set (g ` T)) Z \<Longrightarrow>
                 openin (top_of_set T) (T \<inter> g -` Z)"
     using contf contg by (auto simp: continuous_on_open)
   show ?thesis
   proof
     have "T \<inter> g -` (g ` T \<inter> (S \<inter> f -` U)) = {x \<in> T. f (g x) \<in> U}"
       using imf img by blast
     also have "... = U"
       using U by auto
     finally have eq: "T \<inter> g -` (g ` T \<inter> (S \<inter> f -` U)) = U" .
     assume ?lhs
     then have *: "openin (top_of_set (g ` T)) (g ` T \<inter> (S \<inter> f -` U))"
       by (meson img openin_Int openin_subtopology_Int_subset openin_subtopology_self)
     show ?rhs
       using g [OF *] eq by auto
   next
     assume rhs: ?rhs
     show ?lhs
       by (metis f fg image_eqI image_subset_iff imf img openin_subopen openin_subtopology_self openin_trans rhs)
   qed
 qed
 
 lemma continuous_left_inverse_imp_quotient_map:
   assumes "continuous_on S f"
       and "continuous_on (f ` S) g"
       and  "\<And>x. x \<in> S \<Longrightarrow> g(f x) = x"
       and "U \<subseteq> f ` S"
     shows "openin (top_of_set S) (S \<inter> f -` U) \<longleftrightarrow>
            openin (top_of_set (f ` S)) U"
 apply (rule continuous_right_inverse_imp_quotient_map)
 using assms apply force+
 done
 
 lemma continuous_imp_quotient_map:
   fixes f :: "'a::t2_space \<Rightarrow> 'b::t2_space"
   assumes "continuous_on S f" "f ` S = T" "compact S" "U \<subseteq> T"
     shows "openin (top_of_set S) (S \<inter> f -` U) \<longleftrightarrow>
            openin (top_of_set T) U"
   by (metis (no_types, lifting) assms closed_map_imp_quotient_map continuous_imp_closed_map)
 
 subsection\<^marker>\<open>tag unimportant\<close>\<open>Pasting lemmas for functions, for of casewise definitions\<close>
 
 subsubsection\<open>on open sets\<close>
 
 lemma pasting_lemma:
   assumes ope: "\<And>i. i \<in> I \<Longrightarrow> openin X (T i)"
       and cont: "\<And>i. i \<in> I \<Longrightarrow> continuous_map(subtopology X (T i)) Y (f i)"
       and f: "\<And>i j x. \<lbrakk>i \<in> I; j \<in> I; x \<in> topspace X \<inter> T i \<inter> T j\<rbrakk> \<Longrightarrow> f i x = f j x"
       and g: "\<And>x. x \<in> topspace X \<Longrightarrow> \<exists>j. j \<in> I \<and> x \<in> T j \<and> g x = f j x"
     shows "continuous_map X Y g"
   unfolding continuous_map_openin_preimage_eq
 proof (intro conjI allI impI)
   show "g ` topspace X \<subseteq> topspace Y"
     using g cont continuous_map_image_subset_topspace by fastforce
 next
   fix U
   assume Y: "openin Y U"
   have T: "T i \<subseteq> topspace X" if "i \<in> I" for i
     using ope by (simp add: openin_subset that)
   have *: "topspace X \<inter> g -` U = (\<Union>i \<in> I. T i \<inter> f i -` U)"
     using f g T by fastforce
   have "\<And>i. i \<in> I \<Longrightarrow> openin X (T i \<inter> f i -` U)"
     using cont unfolding continuous_map_openin_preimage_eq
     by (metis Y T inf.commute inf_absorb1 ope topspace_subtopology openin_trans_full)
   then show "openin X (topspace X \<inter> g -` U)"
     by (auto simp: *)
 qed
 
 lemma pasting_lemma_exists:
   assumes X: "topspace X \<subseteq> (\<Union>i \<in> I. T i)"
       and ope: "\<And>i. i \<in> I \<Longrightarrow> openin X (T i)"
       and cont: "\<And>i. i \<in> I \<Longrightarrow> continuous_map (subtopology X (T i)) Y (f i)"
       and f: "\<And>i j x. \<lbrakk>i \<in> I; j \<in> I; x \<in> topspace X \<inter> T i \<inter> T j\<rbrakk> \<Longrightarrow> f i x = f j x"
     obtains g where "continuous_map X Y g" "\<And>x i. \<lbrakk>i \<in> I; x \<in> topspace X \<inter> T i\<rbrakk> \<Longrightarrow> g x = f i x"
 proof
   let ?h = "\<lambda>x. f (SOME i. i \<in> I \<and> x \<in> T i) x"
   show "continuous_map X Y ?h"
     apply (rule pasting_lemma [OF ope cont])
      apply (blast intro: f)+
     by (metis (no_types, lifting) UN_E X subsetD someI_ex)
   show "f (SOME i. i \<in> I \<and> x \<in> T i) x = f i x" if "i \<in> I" "x \<in> topspace X \<inter> T i" for i x
     by (metis (no_types, lifting) IntD2 IntI f someI_ex that)
 qed
 
 lemma pasting_lemma_locally_finite:
   assumes fin: "\<And>x. x \<in> topspace X \<Longrightarrow> \<exists>V. openin X V \<and> x \<in> V \<and> finite {i \<in> I. T i \<inter> V \<noteq> {}}"
     and clo: "\<And>i. i \<in> I \<Longrightarrow> closedin X (T i)"
     and cont:  "\<And>i. i \<in> I \<Longrightarrow> continuous_map(subtopology X (T i)) Y (f i)"
     and f: "\<And>i j x. \<lbrakk>i \<in> I; j \<in> I; x \<in> topspace X \<inter> T i \<inter> T j\<rbrakk> \<Longrightarrow> f i x = f j x"
     and g: "\<And>x. x \<in> topspace X \<Longrightarrow> \<exists>j. j \<in> I \<and> x \<in> T j \<and> g x = f j x"
   shows "continuous_map X Y g"
   unfolding continuous_map_closedin_preimage_eq
 proof (intro conjI allI impI)
   show "g ` topspace X \<subseteq> topspace Y"
     using g cont continuous_map_image_subset_topspace by fastforce
 next
   fix U
   assume Y: "closedin Y U"
   have T: "T i \<subseteq> topspace X" if "i \<in> I" for i
     using clo by (simp add: closedin_subset that)
   have *: "topspace X \<inter> g -` U = (\<Union>i \<in> I. T i \<inter> f i -` U)"
     using f g T by fastforce
   have cTf: "\<And>i. i \<in> I \<Longrightarrow> closedin X (T i \<inter> f i -` U)"
     using cont unfolding continuous_map_closedin_preimage_eq topspace_subtopology
     by (simp add: Int_absorb1 T Y clo closedin_closed_subtopology)
   have sub: "{Z \<in> (\<lambda>i. T i \<inter> f i -` U) ` I. Z \<inter> V \<noteq> {}}
            \<subseteq> (\<lambda>i. T i \<inter> f i -` U) ` {i \<in> I. T i \<inter> V \<noteq> {}}" for V
     by auto
   have 1: "(\<Union>i\<in>I. T i \<inter> f i -` U) \<subseteq> topspace X"
     using T by blast
   then have lf: "locally_finite_in X ((\<lambda>i. T i \<inter> f i -` U) ` I)"
     unfolding locally_finite_in_def
     using finite_subset [OF sub] fin by force
   show "closedin X (topspace X \<inter> g -` U)"
     apply (subst *)
     apply (rule closedin_locally_finite_Union)
      apply (auto intro: cTf lf)
     done
 qed
 
 subsubsection\<open>Likewise on closed sets, with a finiteness assumption\<close>
 
 lemma pasting_lemma_closed:
   assumes fin: "finite I"
     and clo: "\<And>i. i \<in> I \<Longrightarrow> closedin X (T i)"
     and cont:  "\<And>i. i \<in> I \<Longrightarrow> continuous_map(subtopology X (T i)) Y (f i)"
     and f: "\<And>i j x. \<lbrakk>i \<in> I; j \<in> I; x \<in> topspace X \<inter> T i \<inter> T j\<rbrakk> \<Longrightarrow> f i x = f j x"
     and g: "\<And>x. x \<in> topspace X \<Longrightarrow> \<exists>j. j \<in> I \<and> x \<in> T j \<and> g x = f j x"
   shows "continuous_map X Y g"
   using pasting_lemma_locally_finite [OF _ clo cont f g] fin by auto
 
 lemma pasting_lemma_exists_locally_finite:
   assumes fin: "\<And>x. x \<in> topspace X \<Longrightarrow> \<exists>V. openin X V \<and> x \<in> V \<and> finite {i \<in> I. T i \<inter> V \<noteq> {}}"
     and X: "topspace X \<subseteq> \<Union>(T ` I)"
     and clo: "\<And>i. i \<in> I \<Longrightarrow> closedin X (T i)"
     and cont:  "\<And>i. i \<in> I \<Longrightarrow> continuous_map(subtopology X (T i)) Y (f i)"
     and f: "\<And>i j x. \<lbrakk>i \<in> I; j \<in> I; x \<in> topspace X \<inter> T i \<inter> T j\<rbrakk> \<Longrightarrow> f i x = f j x"
     and g: "\<And>x. x \<in> topspace X \<Longrightarrow> \<exists>j. j \<in> I \<and> x \<in> T j \<and> g x = f j x"
   obtains g where "continuous_map X Y g" "\<And>x i. \<lbrakk>i \<in> I; x \<in> topspace X \<inter> T i\<rbrakk> \<Longrightarrow> g x = f i x"
 proof
   show "continuous_map X Y (\<lambda>x. f(@i. i \<in> I \<and> x \<in> T i) x)"
     apply (rule pasting_lemma_locally_finite [OF fin])
         apply (blast intro: assms)+
     by (metis (no_types, lifting) UN_E X set_rev_mp someI_ex)
 next
   fix x i
   assume "i \<in> I" and "x \<in> topspace X \<inter> T i"
   show "f (SOME i. i \<in> I \<and> x \<in> T i) x = f i x"
     apply (rule someI2_ex)
     using \<open>i \<in> I\<close> \<open>x \<in> topspace X \<inter> T i\<close> apply blast
     by (meson Int_iff \<open>i \<in> I\<close> \<open>x \<in> topspace X \<inter> T i\<close> f)
 qed
 
 lemma pasting_lemma_exists_closed:
   assumes fin: "finite I"
     and X: "topspace X \<subseteq> \<Union>(T ` I)"
     and clo: "\<And>i. i \<in> I \<Longrightarrow> closedin X (T i)"
     and cont:  "\<And>i. i \<in> I \<Longrightarrow> continuous_map(subtopology X (T i)) Y (f i)"
     and f: "\<And>i j x. \<lbrakk>i \<in> I; j \<in> I; x \<in> topspace X \<inter> T i \<inter> T j\<rbrakk> \<Longrightarrow> f i x = f j x"
   obtains g where "continuous_map X Y g" "\<And>x i. \<lbrakk>i \<in> I; x \<in> topspace X \<inter> T i\<rbrakk> \<Longrightarrow> g x = f i x"
 proof
   show "continuous_map X Y (\<lambda>x. f (SOME i. i \<in> I \<and> x \<in> T i) x)"
     apply (rule pasting_lemma_closed [OF \<open>finite I\<close> clo cont])
      apply (blast intro: f)+
     by (metis (mono_tags, lifting) UN_iff X someI_ex subset_iff)
 next
   fix x i
   assume "i \<in> I" "x \<in> topspace X \<inter> T i"
   then show "f (SOME i. i \<in> I \<and> x \<in> T i) x = f i x"
     by (metis (no_types, lifting) IntD2 IntI f someI_ex)
 qed
 
 lemma continuous_map_cases:
   assumes f: "continuous_map (subtopology X (X closure_of {x. P x})) Y f"
       and g: "continuous_map (subtopology X (X closure_of {x. \<not> P x})) Y g"
       and fg: "\<And>x. x \<in> X frontier_of {x. P x} \<Longrightarrow> f x = g x"
   shows "continuous_map X Y (\<lambda>x. if P x then f x else g x)"
 proof (rule pasting_lemma_closed)
   let ?f = "\<lambda>b. if b then f else g"
   let ?g = "\<lambda>x. if P x then f x else g x"
   let ?T = "\<lambda>b. if b then X closure_of {x. P x} else X closure_of {x. ~P x}"
   show "finite {True,False}" by auto
   have eq: "topspace X - Collect P = topspace X \<inter> {x. \<not> P x}"
     by blast
   show "?f i x = ?f j x"
     if "i \<in> {True,False}" "j \<in> {True,False}" and x: "x \<in> topspace X \<inter> ?T i \<inter> ?T j" for i j x
   proof -
     have "f x = g x"
       if "i" "\<not> j"
       apply (rule fg)
       unfolding frontier_of_closures eq
       using x that closure_of_restrict by fastforce
     moreover
     have "g x = f x"
       if "x \<in> X closure_of {x. \<not> P x}" "x \<in> X closure_of Collect P" "\<not> i" "j" for x
         apply (rule fg [symmetric])
         unfolding frontier_of_closures eq
         using x that closure_of_restrict by fastforce
     ultimately show ?thesis
       using that by (auto simp flip: closure_of_restrict)
   qed
   show "\<exists>j. j \<in> {True,False} \<and> x \<in> ?T j \<and> (if P x then f x else g x) = ?f j x"
     if "x \<in> topspace X" for x
     apply simp
     apply safe
     apply (metis Int_iff closure_of inf_sup_absorb mem_Collect_eq that)
     by (metis DiffI eq closure_of_subset_Int contra_subsetD mem_Collect_eq that)
 qed (auto simp: f g)
 
 lemma continuous_map_cases_alt:
   assumes f: "continuous_map (subtopology X (X closure_of {x \<in> topspace X. P x})) Y f"
       and g: "continuous_map (subtopology X (X closure_of {x \<in> topspace X. ~P x})) Y g"
       and fg: "\<And>x. x \<in> X frontier_of {x \<in> topspace X. P x} \<Longrightarrow> f x = g x"
     shows "continuous_map X Y (\<lambda>x. if P x then f x else g x)"
   apply (rule continuous_map_cases)
   using assms
     apply (simp_all add: Collect_conj_eq closure_of_restrict [symmetric] frontier_of_restrict [symmetric])
   done
 
 lemma continuous_map_cases_function:
   assumes contp: "continuous_map X Z p"
     and contf: "continuous_map (subtopology X {x \<in> topspace X. p x \<in> Z closure_of U}) Y f"
     and contg: "continuous_map (subtopology X {x \<in> topspace X. p x \<in> Z closure_of (topspace Z - U)}) Y g"
     and fg: "\<And>x. \<lbrakk>x \<in> topspace X; p x \<in> Z frontier_of U\<rbrakk> \<Longrightarrow> f x = g x"
   shows "continuous_map X Y (\<lambda>x. if p x \<in> U then f x else g x)"
 proof (rule continuous_map_cases_alt)
   show "continuous_map (subtopology X (X closure_of {x \<in> topspace X. p x \<in> U})) Y f"
   proof (rule continuous_map_from_subtopology_mono)
     let ?T = "{x \<in> topspace X. p x \<in> Z closure_of U}"
     show "continuous_map (subtopology X ?T) Y f"
       by (simp add: contf)
     show "X closure_of {x \<in> topspace X. p x \<in> U} \<subseteq> ?T"
       by (rule continuous_map_closure_preimage_subset [OF contp])
   qed
   show "continuous_map (subtopology X (X closure_of {x \<in> topspace X. p x \<notin> U})) Y g"
   proof (rule continuous_map_from_subtopology_mono)
     let ?T = "{x \<in> topspace X. p x \<in> Z closure_of (topspace Z - U)}"
     show "continuous_map (subtopology X ?T) Y g"
       by (simp add: contg)
     have "X closure_of {x \<in> topspace X. p x \<notin> U} \<subseteq> X closure_of {x \<in> topspace X. p x \<in> topspace Z - U}"
       apply (rule closure_of_mono)
       using continuous_map_closedin contp by fastforce
     then show "X closure_of {x \<in> topspace X. p x \<notin> U} \<subseteq> ?T"
       by (rule order_trans [OF _ continuous_map_closure_preimage_subset [OF contp]])
   qed
 next
   show "f x = g x" if "x \<in> X frontier_of {x \<in> topspace X. p x \<in> U}" for x
     using that continuous_map_frontier_frontier_preimage_subset [OF contp, of U] fg by blast
 qed
 
 subsection \<open>Retractions\<close>
 
 definition\<^marker>\<open>tag important\<close> retraction :: "('a::topological_space) set \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> bool"
 where "retraction S T r \<longleftrightarrow>
   T \<subseteq> S \<and> continuous_on S r \<and> r ` S \<subseteq> T \<and> (\<forall>x\<in>T. r x = x)"
 
 definition\<^marker>\<open>tag important\<close> retract_of (infixl "retract'_of" 50) where
 "T retract_of S  \<longleftrightarrow>  (\<exists>r. retraction S T r)"
 
 lemma retraction_idempotent: "retraction S T r \<Longrightarrow> x \<in> S \<Longrightarrow>  r (r x) = r x"
   unfolding retraction_def by auto
 
 text \<open>Preservation of fixpoints under (more general notion of) retraction\<close>
 
 lemma invertible_fixpoint_property:
   fixes S :: "'a::topological_space set"
     and T :: "'b::topological_space set"
   assumes contt: "continuous_on T i"
     and "i ` T \<subseteq> S"
     and contr: "continuous_on S r"
     and "r ` S \<subseteq> T"
     and ri: "\<And>y. y \<in> T \<Longrightarrow> r (i y) = y"
     and FP: "\<And>f. \<lbrakk>continuous_on S f; f ` S \<subseteq> S\<rbrakk> \<Longrightarrow> \<exists>x\<in>S. f x = x"
     and contg: "continuous_on T g"
     and "g ` T \<subseteq> T"
   obtains y where "y \<in> T" and "g y = y"
 proof -
   have "\<exists>x\<in>S. (i \<circ> g \<circ> r) x = x"
   proof (rule FP)
     show "continuous_on S (i \<circ> g \<circ> r)"
       by (meson contt contr assms(4) contg assms(8) continuous_on_compose continuous_on_subset)
     show "(i \<circ> g \<circ> r) ` S \<subseteq> S"
       using assms(2,4,8) by force
   qed
   then obtain x where x: "x \<in> S" "(i \<circ> g \<circ> r) x = x" ..
   then have *: "g (r x) \<in> T"
     using assms(4,8) by auto
   have "r ((i \<circ> g \<circ> r) x) = r x"
     using x by auto
   then show ?thesis
     using "*" ri that by auto
 qed
 
 lemma homeomorphic_fixpoint_property:
   fixes S :: "'a::topological_space set"
     and T :: "'b::topological_space set"
   assumes "S homeomorphic T"
   shows "(\<forall>f. continuous_on S f \<and> f ` S \<subseteq> S \<longrightarrow> (\<exists>x\<in>S. f x = x)) \<longleftrightarrow>
          (\<forall>g. continuous_on T g \<and> g ` T \<subseteq> T \<longrightarrow> (\<exists>y\<in>T. g y = y))"
          (is "?lhs = ?rhs")
 proof -
   obtain r i where r:
       "\<forall>x\<in>S. i (r x) = x" "r ` S = T" "continuous_on S r"
       "\<forall>y\<in>T. r (i y) = y" "i ` T = S" "continuous_on T i"
     using assms unfolding homeomorphic_def homeomorphism_def  by blast
   show ?thesis
   proof
     assume ?lhs
     with r show ?rhs
       by (metis invertible_fixpoint_property[of T i S r] order_refl)
   next
     assume ?rhs
     with r show ?lhs
       by (metis invertible_fixpoint_property[of S r T i] order_refl)
   qed
 qed
 
 lemma retract_fixpoint_property:
   fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
     and S :: "'a set"
   assumes "T retract_of S"
     and FP: "\<And>f. \<lbrakk>continuous_on S f; f ` S \<subseteq> S\<rbrakk> \<Longrightarrow> \<exists>x\<in>S. f x = x"
     and contg: "continuous_on T g"
     and "g ` T \<subseteq> T"
   obtains y where "y \<in> T" and "g y = y"
 proof -
   obtain h where "retraction S T h"
     using assms(1) unfolding retract_of_def ..
   then show ?thesis
     unfolding retraction_def
     using invertible_fixpoint_property[OF continuous_on_id _ _ _ _ FP]
     by (metis assms(4) contg image_ident that)
 qed
 
 lemma retraction:
   "retraction S T r \<longleftrightarrow>
     T \<subseteq> S \<and> continuous_on S r \<and> r ` S = T \<and> (\<forall>x \<in> T. r x = x)"
   by (force simp: retraction_def)
 
 lemma retractionE: \<comment> \<open>yields properties normalized wrt. simp -- less likely to loop\<close>
   assumes "retraction S T r"
   obtains "T = r ` S" "r ` S \<subseteq> S" "continuous_on S r" "\<And>x. x \<in> S \<Longrightarrow> r (r x) = r x"
 proof (rule that)
   from retraction [of S T r] assms
   have "T \<subseteq> S" "continuous_on S r" "r ` S = T" and "\<forall>x \<in> T. r x = x"
     by simp_all
   then show "T = r ` S" "r ` S \<subseteq> S" "continuous_on S r"
     by simp_all
   from \<open>\<forall>x \<in> T. r x = x\<close> have "r x = x" if "x \<in> T" for x
     using that by simp
   with \<open>r ` S = T\<close> show "r (r x) = r x" if "x \<in> S" for x
     using that by auto
 qed
 
 lemma retract_ofE: \<comment> \<open>yields properties normalized wrt. simp -- less likely to loop\<close>
   assumes "T retract_of S"
   obtains r where "T = r ` S" "r ` S \<subseteq> S" "continuous_on S r" "\<And>x. x \<in> S \<Longrightarrow> r (r x) = r x"
 proof -
   from assms obtain r where "retraction S T r"
     by (auto simp add: retract_of_def)
   with that show thesis
     by (auto elim: retractionE)
 qed
 
 lemma retract_of_imp_extensible:
   assumes "S retract_of T" and "continuous_on S f" and "f ` S \<subseteq> U"
   obtains g where "continuous_on T g" "g ` T \<subseteq> U" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
 proof -
   from \<open>S retract_of T\<close> obtain r where "retraction T S r"
     by (auto simp add: retract_of_def)
   show thesis
     by (rule that [of "f \<circ> r"])
       (use \<open>continuous_on S f\<close> \<open>f ` S \<subseteq> U\<close> \<open>retraction T S r\<close> in \<open>auto simp: continuous_on_compose2 retraction\<close>)
 qed
 
 lemma idempotent_imp_retraction:
   assumes "continuous_on S f" and "f ` S \<subseteq> S" and "\<And>x. x \<in> S \<Longrightarrow> f(f x) = f x"
     shows "retraction S (f ` S) f"
 by (simp add: assms retraction)
 
 lemma retraction_subset:
   assumes "retraction S T r" and "T \<subseteq> s'" and "s' \<subseteq> S"
   shows "retraction s' T r"
   unfolding retraction_def
   by (metis assms continuous_on_subset image_mono retraction)
 
 lemma retract_of_subset:
   assumes "T retract_of S" and "T \<subseteq> s'" and "s' \<subseteq> S"
     shows "T retract_of s'"
 by (meson assms retract_of_def retraction_subset)
 
 lemma retraction_refl [simp]: "retraction S S (\<lambda>x. x)"
 by (simp add: retraction)
 
 lemma retract_of_refl [iff]: "S retract_of S"
   unfolding retract_of_def retraction_def
   using continuous_on_id by blast
 
 lemma retract_of_imp_subset:
    "S retract_of T \<Longrightarrow> S \<subseteq> T"
 by (simp add: retract_of_def retraction_def)
 
 lemma retract_of_empty [simp]:
      "({} retract_of S) \<longleftrightarrow> S = {}"  "(S retract_of {}) \<longleftrightarrow> S = {}"
 by (auto simp: retract_of_def retraction_def)
 
 lemma retract_of_singleton [iff]: "({x} retract_of S) \<longleftrightarrow> x \<in> S"
   unfolding retract_of_def retraction_def by force
 
 lemma retraction_comp:
    "\<lbrakk>retraction S T f; retraction T U g\<rbrakk>
         \<Longrightarrow> retraction S U (g \<circ> f)"
 apply (auto simp: retraction_def intro: continuous_on_compose2)
 by blast
 
 lemma retract_of_trans [trans]:
   assumes "S retract_of T" and "T retract_of U"
     shows "S retract_of U"
 using assms by (auto simp: retract_of_def intro: retraction_comp)
 
 lemma closedin_retract:
   fixes S :: "'a :: t2_space set"
   assumes "S retract_of T"
     shows "closedin (top_of_set T) S"
 proof -
   obtain r where r: "S \<subseteq> T" "continuous_on T r" "r ` T \<subseteq> S" "\<And>x. x \<in> S \<Longrightarrow> r x = x"
     using assms by (auto simp: retract_of_def retraction_def)
   have "S = {x\<in>T. x = r x}"
     using r by auto
   also have "\<dots> = T \<inter> ((\<lambda>x. (x, r x)) -` ({y. \<exists>x. y = (x, x)}))"
     unfolding vimage_def mem_Times_iff fst_conv snd_conv
     using r
     by auto
   also have "closedin (top_of_set T) \<dots>"
     by (rule continuous_closedin_preimage) (auto intro!: closed_diagonal continuous_on_Pair r)
   finally show ?thesis .
 qed
 
 lemma closedin_self [simp]: "closedin (top_of_set S) S"
   by simp
 
 lemma retract_of_closed:
     fixes S :: "'a :: t2_space set"
     shows "\<lbrakk>closed T; S retract_of T\<rbrakk> \<Longrightarrow> closed S"
   by (metis closedin_retract closedin_closed_eq)
 
 lemma retract_of_compact:
      "\<lbrakk>compact T; S retract_of T\<rbrakk> \<Longrightarrow> compact S"
   by (metis compact_continuous_image retract_of_def retraction)
 
 lemma retract_of_connected:
     "\<lbrakk>connected T; S retract_of T\<rbrakk> \<Longrightarrow> connected S"
   by (metis Topological_Spaces.connected_continuous_image retract_of_def retraction)
 
 lemma retraction_openin_vimage_iff:
   "openin (top_of_set S) (S \<inter> r -` U) \<longleftrightarrow> openin (top_of_set T) U"
   if retraction: "retraction S T r" and "U \<subseteq> T"
   using retraction apply (rule retractionE)
   apply (rule continuous_right_inverse_imp_quotient_map [where g=r])
   using \<open>U \<subseteq> T\<close> apply (auto elim: continuous_on_subset)
   done
 
 lemma retract_of_Times:
    "\<lbrakk>S retract_of s'; T retract_of t'\<rbrakk> \<Longrightarrow> (S \<times> T) retract_of (s' \<times> t')"
 apply (simp add: retract_of_def retraction_def Sigma_mono, clarify)
 apply (rename_tac f g)
 apply (rule_tac x="\<lambda>z. ((f \<circ> fst) z, (g \<circ> snd) z)" in exI)
 apply (rule conjI continuous_intros | erule continuous_on_subset | force)+
 done
 
 subsection\<open>Retractions on a topological space\<close>
 
 definition retract_of_space :: "'a set \<Rightarrow> 'a topology \<Rightarrow> bool" (infix "retract'_of'_space" 50)
   where "S retract_of_space X
          \<equiv> S \<subseteq> topspace X \<and> (\<exists>r. continuous_map X (subtopology X S) r \<and> (\<forall>x \<in> S. r x = x))"
 
 lemma retract_of_space_retraction_maps:
    "S retract_of_space X \<longleftrightarrow> S \<subseteq> topspace X \<and> (\<exists>r. retraction_maps X (subtopology X S) r id)"
   by (auto simp: retract_of_space_def retraction_maps_def)
 
 lemma retract_of_space_section_map:
    "S retract_of_space X \<longleftrightarrow> S \<subseteq> topspace X \<and> section_map (subtopology X S) X id"
   unfolding retract_of_space_def retraction_maps_def section_map_def
   by (auto simp: continuous_map_from_subtopology)
 
 lemma retract_of_space_imp_subset:
    "S retract_of_space X \<Longrightarrow> S \<subseteq> topspace X"
   by (simp add: retract_of_space_def)
 
 lemma retract_of_space_topspace:
    "topspace X retract_of_space X"
   using retract_of_space_def by force
 
 lemma retract_of_space_empty [simp]:
    "{} retract_of_space X \<longleftrightarrow> topspace X = {}"
   by (auto simp: continuous_map_def retract_of_space_def)
 
 lemma retract_of_space_singleton [simp]:
   "{a} retract_of_space X \<longleftrightarrow> a \<in> topspace X"
 proof -
   have "continuous_map X (subtopology X {a}) (\<lambda>x. a) \<and> (\<lambda>x. a) a = a" if "a \<in> topspace X"
     using that by simp
   then show ?thesis
     by (force simp: retract_of_space_def)
 qed
 
 lemma retract_of_space_clopen:
   assumes "openin X S" "closedin X S" "S = {} \<Longrightarrow> topspace X = {}"
   shows "S retract_of_space X"
 proof (cases "S = {}")
   case False
   then obtain a where "a \<in> S"
     by blast
   show ?thesis
     unfolding retract_of_space_def
   proof (intro exI conjI)
     show "S \<subseteq> topspace X"
       by (simp add: assms closedin_subset)
     have "continuous_map X X (\<lambda>x. if x \<in> S then x else a)"
     proof (rule continuous_map_cases)
       show "continuous_map (subtopology X (X closure_of {x. x \<in> S})) X (\<lambda>x. x)"
         by (simp add: continuous_map_from_subtopology)
       show "continuous_map (subtopology X (X closure_of {x. x \<notin> S})) X (\<lambda>x. a)"
         using \<open>S \<subseteq> topspace X\<close> \<open>a \<in> S\<close> by force
       show "x = a" if "x \<in> X frontier_of {x. x \<in> S}" for x
         using assms that clopenin_eq_frontier_of by fastforce
     qed
     then show "continuous_map X (subtopology X S) (\<lambda>x. if x \<in> S then x else a)"
       using \<open>S \<subseteq> topspace X\<close> \<open>a \<in> S\<close>  by (auto simp: continuous_map_in_subtopology)
   qed auto
 qed (use assms in auto)
 
 lemma retract_of_space_disjoint_union:
   assumes "openin X S" "openin X T" and ST: "disjnt S T" "S \<union> T = topspace X" and "S = {} \<Longrightarrow> topspace X = {}"
   shows "S retract_of_space X"
 proof (rule retract_of_space_clopen)
   have "S \<inter> T = {}"
     by (meson ST disjnt_def)
   then have "S = topspace X - T"
     using ST by auto
   then show "closedin X S"
     using \<open>openin X T\<close> by blast
 qed (auto simp: assms)
 
 lemma retraction_maps_section_image1:
   assumes "retraction_maps X Y r s"
   shows "s ` (topspace Y) retract_of_space X"
   unfolding retract_of_space_section_map
 proof
   show "s ` topspace Y \<subseteq> topspace X"
     using assms continuous_map_image_subset_topspace retraction_maps_def by blast
   show "section_map (subtopology X (s ` topspace Y)) X id"
     unfolding section_map_def
     using assms retraction_maps_to_retract_maps by blast
 qed
 
 lemma retraction_maps_section_image2:
    "retraction_maps X Y r s
         \<Longrightarrow> subtopology X (s ` (topspace Y)) homeomorphic_space Y"
   using embedding_map_imp_homeomorphic_space homeomorphic_space_sym section_imp_embedding_map
         section_map_def by blast
 
 subsection\<open>Paths and path-connectedness\<close>
 
 definition pathin :: "'a topology \<Rightarrow> (real \<Rightarrow> 'a) \<Rightarrow> bool" where
    "pathin X g \<equiv> continuous_map (subtopology euclideanreal {0..1}) X g"
 
 lemma pathin_compose:
      "\<lbrakk>pathin X g; continuous_map X Y f\<rbrakk> \<Longrightarrow> pathin Y (f \<circ> g)"
    by (simp add: continuous_map_compose pathin_def)
 
 lemma pathin_subtopology:
      "pathin (subtopology X S) g \<longleftrightarrow> pathin X g \<and> (\<forall>x \<in> {0..1}. g x \<in> S)"
   by (auto simp: pathin_def continuous_map_in_subtopology)
 
 lemma pathin_const:
    "pathin X (\<lambda>x. a) \<longleftrightarrow> a \<in> topspace X"
   by (simp add: pathin_def)
    
 lemma path_start_in_topspace: "pathin X g \<Longrightarrow> g 0 \<in> topspace X"
   by (force simp: pathin_def continuous_map)
 
 lemma path_finish_in_topspace: "pathin X g \<Longrightarrow> g 1 \<in> topspace X"
   by (force simp: pathin_def continuous_map)
 
 lemma path_image_subset_topspace: "pathin X g \<Longrightarrow> g ` ({0..1}) \<subseteq> topspace X"
   by (force simp: pathin_def continuous_map)
 
 definition path_connected_space :: "'a topology \<Rightarrow> bool"
   where "path_connected_space X \<equiv> \<forall>x \<in> topspace X. \<forall> y \<in> topspace X. \<exists>g. pathin X g \<and> g 0 = x \<and> g 1 = y"
 
 definition path_connectedin :: "'a topology \<Rightarrow> 'a set \<Rightarrow> bool"
   where "path_connectedin X S \<equiv> S \<subseteq> topspace X \<and> path_connected_space(subtopology X S)"
 
 lemma path_connectedin_absolute [simp]:
      "path_connectedin (subtopology X S) S \<longleftrightarrow> path_connectedin X S"
   by (simp add: path_connectedin_def subtopology_subtopology)
 
 lemma path_connectedin_subset_topspace:
      "path_connectedin X S \<Longrightarrow> S \<subseteq> topspace X"
   by (simp add: path_connectedin_def)
 
 lemma path_connectedin_subtopology:
      "path_connectedin (subtopology X S) T \<longleftrightarrow> path_connectedin X T \<and> T \<subseteq> S"
   by (auto simp: path_connectedin_def subtopology_subtopology inf.absorb2)
 
 lemma path_connectedin:
      "path_connectedin X S \<longleftrightarrow>
         S \<subseteq> topspace X \<and>
         (\<forall>x \<in> S. \<forall>y \<in> S. \<exists>g. pathin X g \<and> g ` {0..1} \<subseteq> S \<and> g 0 = x \<and> g 1 = y)"
   unfolding path_connectedin_def path_connected_space_def pathin_def continuous_map_in_subtopology
   by (intro conj_cong refl ball_cong) (simp_all add: inf.absorb_iff2)
 
 lemma path_connectedin_topspace:
      "path_connectedin X (topspace X) \<longleftrightarrow> path_connected_space X"
   by (simp add: path_connectedin_def)
 
 lemma path_connected_imp_connected_space:
   assumes "path_connected_space X"
   shows "connected_space X"
 proof -
   have *: "\<exists>S. connectedin X S \<and> g 0 \<in> S \<and> g 1 \<in> S" if "pathin X g" for g
   proof (intro exI conjI)
     have "continuous_map (subtopology euclideanreal {0..1}) X g"
       using connectedin_absolute that by (simp add: pathin_def)
     then show "connectedin X (g ` {0..1})"
       by (rule connectedin_continuous_map_image) auto
   qed auto
   show ?thesis
     using assms
     by (auto intro: * simp add: path_connected_space_def connected_space_subconnected Ball_def)
 qed
 
 lemma path_connectedin_imp_connectedin:
      "path_connectedin X S \<Longrightarrow> connectedin X S"
   by (simp add: connectedin_def path_connected_imp_connected_space path_connectedin_def)
 
 lemma path_connected_space_topspace_empty:
      "topspace X = {} \<Longrightarrow> path_connected_space X"
   by (simp add: path_connected_space_def)
 
 lemma path_connectedin_empty [simp]: "path_connectedin X {}"
   by (simp add: path_connectedin)
 
 lemma path_connectedin_singleton [simp]: "path_connectedin X {a} \<longleftrightarrow> a \<in> topspace X"
 proof
   show "path_connectedin X {a} \<Longrightarrow> a \<in> topspace X"
     by (simp add: path_connectedin)
   show "a \<in> topspace X \<Longrightarrow> path_connectedin X {a}"
     unfolding path_connectedin
     using pathin_const by fastforce
 qed
 
 lemma path_connectedin_continuous_map_image:
   assumes f: "continuous_map X Y f" and S: "path_connectedin X S"
   shows "path_connectedin Y (f ` S)"
 proof -
   have fX: "f ` (topspace X) \<subseteq> topspace Y"
     by (metis f continuous_map_image_subset_topspace)
   show ?thesis
     unfolding path_connectedin
   proof (intro conjI ballI; clarify?)
     fix x
     assume "x \<in> S"
     show "f x \<in> topspace Y"
       by (meson S fX \<open>x \<in> S\<close> image_subset_iff path_connectedin_subset_topspace set_mp)
   next
     fix x y
     assume "x \<in> S" and "y \<in> S"
     then obtain g where g: "pathin X g" "g ` {0..1} \<subseteq> S" "g 0 = x" "g 1 = y"
       using S  by (force simp: path_connectedin)
     show "\<exists>g. pathin Y g \<and> g ` {0..1} \<subseteq> f ` S \<and> g 0 = f x \<and> g 1 = f y"
     proof (intro exI conjI)
       show "pathin Y (f \<circ> g)"
         using \<open>pathin X g\<close> f pathin_compose by auto
     qed (use g in auto)
   qed
 qed
 
 lemma path_connectedin_discrete_topology:
   "path_connectedin (discrete_topology U) S \<longleftrightarrow> S \<subseteq> U \<and> (\<exists>a. S \<subseteq> {a})"
   apply safe
   using path_connectedin_subset_topspace apply fastforce
    apply (meson connectedin_discrete_topology path_connectedin_imp_connectedin)
   using subset_singletonD by fastforce
 
 lemma path_connected_space_discrete_topology:
    "path_connected_space (discrete_topology U) \<longleftrightarrow> (\<exists>a. U \<subseteq> {a})"
   by (metis path_connectedin_discrete_topology path_connectedin_topspace path_connected_space_topspace_empty
             subset_singletonD topspace_discrete_topology)
 
 
 lemma homeomorphic_path_connected_space_imp:
      "\<lbrakk>path_connected_space X; X homeomorphic_space Y\<rbrakk> \<Longrightarrow> path_connected_space Y"
   unfolding homeomorphic_space_def homeomorphic_maps_def
   by (metis (no_types, hide_lams) continuous_map_closedin continuous_map_image_subset_topspace imageI order_class.order.antisym path_connectedin_continuous_map_image path_connectedin_topspace subsetI)
 
 lemma homeomorphic_path_connected_space:
    "X homeomorphic_space Y \<Longrightarrow> path_connected_space X \<longleftrightarrow> path_connected_space Y"
   by (meson homeomorphic_path_connected_space_imp homeomorphic_space_sym)
 
 lemma homeomorphic_map_path_connectedness:
   assumes "homeomorphic_map X Y f" "U \<subseteq> topspace X"
   shows "path_connectedin Y (f ` U) \<longleftrightarrow> path_connectedin X U"
   unfolding path_connectedin_def
 proof (intro conj_cong homeomorphic_path_connected_space)
   show "(f ` U \<subseteq> topspace Y) = (U \<subseteq> topspace X)"
     using assms homeomorphic_imp_surjective_map by blast
 next
   assume "U \<subseteq> topspace X"
   show "subtopology Y (f ` U) homeomorphic_space subtopology X U"
     using assms unfolding homeomorphic_eq_everything_map
     by (metis (no_types, hide_lams) assms homeomorphic_map_subtopologies homeomorphic_space homeomorphic_space_sym image_mono inf.absorb_iff2)
 qed
 
 lemma homeomorphic_map_path_connectedness_eq:
    "homeomorphic_map X Y f \<Longrightarrow> path_connectedin X U \<longleftrightarrow> U \<subseteq> topspace X \<and> path_connectedin Y (f ` U)"
   by (meson homeomorphic_map_path_connectedness path_connectedin_def)
 
 subsection\<open>Connected components\<close>
 
 definition connected_component_of :: "'a topology \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
   where "connected_component_of X x y \<equiv>
         \<exists>T. connectedin X T \<and> x \<in> T \<and> y \<in> T"
 
 abbreviation connected_component_of_set
   where "connected_component_of_set X x \<equiv> Collect (connected_component_of X x)"
 
 definition connected_components_of :: "'a topology \<Rightarrow> ('a set) set"
   where "connected_components_of X \<equiv> connected_component_of_set X ` topspace X"
 
 lemma connected_component_in_topspace:
    "connected_component_of X x y \<Longrightarrow> x \<in> topspace X \<and> y \<in> topspace X"
   by (meson connected_component_of_def connectedin_subset_topspace in_mono)
 
 lemma connected_component_of_refl:
    "connected_component_of X x x \<longleftrightarrow> x \<in> topspace X"
   by (meson connected_component_in_topspace connected_component_of_def connectedin_sing insertI1)
 
 lemma connected_component_of_sym:
    "connected_component_of X x y \<longleftrightarrow> connected_component_of X y x"
   by (meson connected_component_of_def)
 
 lemma connected_component_of_trans:
    "\<lbrakk>connected_component_of X x y; connected_component_of X y z\<rbrakk>
         \<Longrightarrow> connected_component_of X x z"
   unfolding connected_component_of_def
-  using connectedin_Un by fastforce
+  using connectedin_Un by blast
 
 lemma connected_component_of_mono:
    "\<lbrakk>connected_component_of (subtopology X S) x y; S \<subseteq> T\<rbrakk>
         \<Longrightarrow> connected_component_of (subtopology X T) x y"
   by (metis connected_component_of_def connectedin_subtopology inf.absorb_iff2 subtopology_subtopology)
 
 lemma connected_component_of_set:
    "connected_component_of_set X x = {y. \<exists>T. connectedin X T \<and> x \<in> T \<and> y \<in> T}"
   by (meson connected_component_of_def)
 
 lemma connected_component_of_subset_topspace:
    "connected_component_of_set X x \<subseteq> topspace X"
   using connected_component_in_topspace by force
 
 lemma connected_component_of_eq_empty:
    "connected_component_of_set X x = {} \<longleftrightarrow> (x \<notin> topspace X)"
   using connected_component_in_topspace connected_component_of_refl by fastforce
 
 lemma connected_space_iff_connected_component:
    "connected_space X \<longleftrightarrow> (\<forall>x \<in> topspace X. \<forall>y \<in> topspace X. connected_component_of X x y)"
   by (simp add: connected_component_of_def connected_space_subconnected)
 
 lemma connected_space_imp_connected_component_of:
    "\<lbrakk>connected_space X; a \<in> topspace X; b \<in> topspace X\<rbrakk>
     \<Longrightarrow> connected_component_of X a b"
   by (simp add: connected_space_iff_connected_component)
 
 lemma connected_space_connected_component_set:
    "connected_space X \<longleftrightarrow> (\<forall>x \<in> topspace X. connected_component_of_set X x = topspace X)"
   using connected_component_of_subset_topspace connected_space_iff_connected_component by fastforce
 
 lemma connected_component_of_maximal:
    "\<lbrakk>connectedin X S; x \<in> S\<rbrakk> \<Longrightarrow> S \<subseteq> connected_component_of_set X x"
   by (meson Ball_Collect connected_component_of_def)
 
 lemma connected_component_of_equiv:
    "connected_component_of X x y \<longleftrightarrow>
     x \<in> topspace X \<and> y \<in> topspace X \<and> connected_component_of X x = connected_component_of X y"
   apply (simp add: connected_component_in_topspace fun_eq_iff)
   by (meson connected_component_of_refl connected_component_of_sym connected_component_of_trans)
 
 lemma connected_component_of_disjoint:
    "disjnt (connected_component_of_set X x) (connected_component_of_set X y)
     \<longleftrightarrow> ~(connected_component_of X x y)"
   using connected_component_of_equiv unfolding disjnt_iff by force
 
 lemma connected_component_of_eq:
    "connected_component_of X x = connected_component_of X y \<longleftrightarrow>
         (x \<notin> topspace X) \<and> (y \<notin> topspace X) \<or>
         x \<in> topspace X \<and> y \<in> topspace X \<and>
         connected_component_of X x y"
   by (metis Collect_empty_eq_bot connected_component_of_eq_empty connected_component_of_equiv)
 
 lemma connectedin_connected_component_of:
    "connectedin X (connected_component_of_set X x)"
 proof -
   have "connected_component_of_set X x = \<Union> {T. connectedin X T \<and> x \<in> T}"
     by (auto simp: connected_component_of_def)
   then show ?thesis
     apply (rule ssubst)
     by (blast intro: connectedin_Union)
 qed
 
 
 lemma Union_connected_components_of:
    "\<Union>(connected_components_of X) = topspace X"
   unfolding connected_components_of_def
   apply (rule equalityI)
   apply (simp add: SUP_least connected_component_of_subset_topspace)
   using connected_component_of_refl by fastforce
 
 lemma connected_components_of_maximal:
    "\<lbrakk>C \<in> connected_components_of X; connectedin X S; ~disjnt C S\<rbrakk> \<Longrightarrow> S \<subseteq> C"
   unfolding connected_components_of_def disjnt_def
   apply clarify
   by (metis Int_emptyI connected_component_of_def connected_component_of_trans mem_Collect_eq)
 
 lemma pairwise_disjoint_connected_components_of:
    "pairwise disjnt (connected_components_of X)"
   unfolding connected_components_of_def pairwise_def
   apply clarify
   by (metis connected_component_of_disjoint connected_component_of_equiv)
 
 lemma complement_connected_components_of_Union:
    "C \<in> connected_components_of X
       \<Longrightarrow> topspace X - C = \<Union> (connected_components_of X - {C})"
   apply (rule equalityI)
   using Union_connected_components_of apply fastforce
   by (metis Diff_cancel Diff_subset Union_connected_components_of cSup_singleton diff_Union_pairwise_disjoint equalityE insert_subsetI pairwise_disjoint_connected_components_of)
 
 lemma nonempty_connected_components_of:
    "C \<in> connected_components_of X \<Longrightarrow> C \<noteq> {}"
   unfolding connected_components_of_def
   by (metis (no_types, lifting) connected_component_of_eq_empty imageE)
 
 lemma connected_components_of_subset:
    "C \<in> connected_components_of X \<Longrightarrow> C \<subseteq> topspace X"
   using Union_connected_components_of by fastforce
 
 lemma connectedin_connected_components_of:
   assumes "C \<in> connected_components_of X"
   shows "connectedin X C"
 proof -
   have "C \<in> connected_component_of_set X ` topspace X"
     using assms connected_components_of_def by blast
 then show ?thesis
   using connectedin_connected_component_of by fastforce
 qed
 
 lemma connected_component_in_connected_components_of:
    "connected_component_of_set X a \<in> connected_components_of X \<longleftrightarrow> a \<in> topspace X"
   apply (rule iffI)
   using connected_component_of_eq_empty nonempty_connected_components_of apply fastforce
   by (simp add: connected_components_of_def)
 
 lemma connected_space_iff_components_eq:
    "connected_space X \<longleftrightarrow> (\<forall>C \<in> connected_components_of X. \<forall>C' \<in> connected_components_of X. C = C')"
   apply (rule iffI)
   apply (force simp: connected_components_of_def connected_space_connected_component_set image_iff)
   by (metis connected_component_in_connected_components_of connected_component_of_refl connected_space_iff_connected_component mem_Collect_eq)
 
 lemma connected_components_of_eq_empty:
    "connected_components_of X = {} \<longleftrightarrow> topspace X = {}"
   by (simp add: connected_components_of_def)
 
 lemma connected_components_of_empty_space:
    "topspace X = {} \<Longrightarrow> connected_components_of X = {}"
   by (simp add: connected_components_of_eq_empty)
 
 lemma connected_components_of_subset_sing:
    "connected_components_of X \<subseteq> {S} \<longleftrightarrow> connected_space X \<and> (topspace X = {} \<or> topspace X = S)"
 proof (cases "topspace X = {}")
   case True
   then show ?thesis
     by (simp add: connected_components_of_empty_space connected_space_topspace_empty)
 next
   case False
   then show ?thesis
     by (metis (no_types, hide_lams) Union_connected_components_of ccpo_Sup_singleton
         connected_components_of_eq_empty connected_space_iff_components_eq insertI1 singletonD
         subsetI subset_singleton_iff)
 qed
 
 lemma connected_space_iff_components_subset_singleton:
    "connected_space X \<longleftrightarrow> (\<exists>a. connected_components_of X \<subseteq> {a})"
   by (simp add: connected_components_of_subset_sing)
 
 lemma connected_components_of_eq_singleton:
    "connected_components_of X = {S}
 \<longleftrightarrow> connected_space X \<and> topspace X \<noteq> {} \<and> S = topspace X"
   by (metis ccpo_Sup_singleton connected_components_of_subset_sing insert_not_empty subset_singleton_iff)
 
 lemma connected_components_of_connected_space:
    "connected_space X \<Longrightarrow> connected_components_of X = (if topspace X = {} then {} else {topspace X})"
   by (simp add: connected_components_of_eq_empty connected_components_of_eq_singleton)
 
 lemma exists_connected_component_of_superset:
   assumes "connectedin X S" and ne: "topspace X \<noteq> {}"
   shows "\<exists>C. C \<in> connected_components_of X \<and> S \<subseteq> C"
 proof (cases "S = {}")
   case True
   then show ?thesis
     using ne connected_components_of_def by blast
 next
   case False
   then show ?thesis
     by (meson all_not_in_conv assms(1) connected_component_in_connected_components_of connected_component_of_maximal connectedin_subset_topspace in_mono)
 qed
 
 lemma closedin_connected_components_of:
   assumes "C \<in> connected_components_of X"
   shows   "closedin X C"
 proof -
   obtain x where "x \<in> topspace X" and x: "C = connected_component_of_set X x"
     using assms by (auto simp: connected_components_of_def)
   have "connected_component_of_set X x \<subseteq> topspace X"
     by (simp add: connected_component_of_subset_topspace)
   moreover have "X closure_of connected_component_of_set X x \<subseteq> connected_component_of_set X x"
   proof (rule connected_component_of_maximal)
     show "connectedin X (X closure_of connected_component_of_set X x)"
       by (simp add: connectedin_closure_of connectedin_connected_component_of)
     show "x \<in> X closure_of connected_component_of_set X x"
       by (simp add: \<open>x \<in> topspace X\<close> closure_of connected_component_of_refl)
   qed
   ultimately
   show ?thesis
     using closure_of_subset_eq x by auto
 qed
 
 lemma closedin_connected_component_of:
    "closedin X (connected_component_of_set X x)"
   by (metis closedin_connected_components_of closedin_empty connected_component_in_connected_components_of connected_component_of_eq_empty)
 
 lemma connected_component_of_eq_overlap:
    "connected_component_of_set X x = connected_component_of_set X y \<longleftrightarrow>
       (x \<notin> topspace X) \<and> (y \<notin> topspace X) \<or>
       ~(connected_component_of_set X x \<inter> connected_component_of_set X y = {})"
   using connected_component_of_equiv by fastforce
 
 lemma connected_component_of_nonoverlap:
    "connected_component_of_set X x \<inter> connected_component_of_set X y = {} \<longleftrightarrow>
      (x \<notin> topspace X) \<or> (y \<notin> topspace X) \<or>
      ~(connected_component_of_set X x = connected_component_of_set X y)"
   by (metis connected_component_of_eq_empty connected_component_of_eq_overlap inf.idem)
 
 lemma connected_component_of_overlap:
    "~(connected_component_of_set X x \<inter> connected_component_of_set X y = {}) \<longleftrightarrow>
     x \<in> topspace X \<and> y \<in> topspace X \<and>
     connected_component_of_set X x = connected_component_of_set X y"
   by (meson connected_component_of_nonoverlap)
 
 
 end
\ No newline at end of file
diff --git a/src/HOL/HOL.thy b/src/HOL/HOL.thy
--- a/src/HOL/HOL.thy
+++ b/src/HOL/HOL.thy
@@ -1,2122 +1,2141 @@
 (*  Title:      HOL/HOL.thy
     Author:     Tobias Nipkow, Markus Wenzel, and Larry Paulson
 *)
 
 section \<open>The basis of Higher-Order Logic\<close>
 
 theory HOL
 imports Pure Tools.Code_Generator
 keywords
   "try" "solve_direct" "quickcheck" "print_coercions" "print_claset"
     "print_induct_rules" :: diag and
   "quickcheck_params" :: thy_decl
 abbrevs "?<" = "\<exists>\<^sub>\<le>\<^sub>1"
 begin
 
 ML_file \<open>~~/src/Tools/misc_legacy.ML\<close>
 ML_file \<open>~~/src/Tools/try.ML\<close>
 ML_file \<open>~~/src/Tools/quickcheck.ML\<close>
 ML_file \<open>~~/src/Tools/solve_direct.ML\<close>
 ML_file \<open>~~/src/Tools/IsaPlanner/zipper.ML\<close>
 ML_file \<open>~~/src/Tools/IsaPlanner/isand.ML\<close>
 ML_file \<open>~~/src/Tools/IsaPlanner/rw_inst.ML\<close>
 ML_file \<open>~~/src/Provers/hypsubst.ML\<close>
 ML_file \<open>~~/src/Provers/splitter.ML\<close>
 ML_file \<open>~~/src/Provers/classical.ML\<close>
 ML_file \<open>~~/src/Provers/blast.ML\<close>
 ML_file \<open>~~/src/Provers/clasimp.ML\<close>
 ML_file \<open>~~/src/Tools/eqsubst.ML\<close>
 ML_file \<open>~~/src/Provers/quantifier1.ML\<close>
 ML_file \<open>~~/src/Tools/atomize_elim.ML\<close>
 ML_file \<open>~~/src/Tools/cong_tac.ML\<close>
 ML_file \<open>~~/src/Tools/intuitionistic.ML\<close> setup \<open>Intuitionistic.method_setup \<^binding>\<open>iprover\<close>\<close>
 ML_file \<open>~~/src/Tools/project_rule.ML\<close>
 ML_file \<open>~~/src/Tools/subtyping.ML\<close>
 ML_file \<open>~~/src/Tools/case_product.ML\<close>
 
 
 ML \<open>Plugin_Name.declare_setup \<^binding>\<open>extraction\<close>\<close>
 
 ML \<open>
   Plugin_Name.declare_setup \<^binding>\<open>quickcheck_random\<close>;
   Plugin_Name.declare_setup \<^binding>\<open>quickcheck_exhaustive\<close>;
   Plugin_Name.declare_setup \<^binding>\<open>quickcheck_bounded_forall\<close>;
   Plugin_Name.declare_setup \<^binding>\<open>quickcheck_full_exhaustive\<close>;
   Plugin_Name.declare_setup \<^binding>\<open>quickcheck_narrowing\<close>;
 \<close>
 ML \<open>
   Plugin_Name.define_setup \<^binding>\<open>quickcheck\<close>
    [\<^plugin>\<open>quickcheck_exhaustive\<close>,
     \<^plugin>\<open>quickcheck_random\<close>,
     \<^plugin>\<open>quickcheck_bounded_forall\<close>,
     \<^plugin>\<open>quickcheck_full_exhaustive\<close>,
     \<^plugin>\<open>quickcheck_narrowing\<close>]
 \<close>
 
 
 subsection \<open>Primitive logic\<close>
 
 text \<open>
 The definition of the logic is based on Mike Gordon's technical report @{cite "Gordon-TR68"} that
 describes the first implementation of HOL. However, there are a number of differences.
 In particular, we start with the definite description operator and introduce Hilbert's \<open>\<epsilon>\<close> operator
 only much later. Moreover, axiom \<open>(P \<longrightarrow> Q) \<longrightarrow> (Q \<longrightarrow> P) \<longrightarrow> (P = Q)\<close> is derived from the other
 axioms. The fact that this axiom is derivable was first noticed by Bruno Barras (for Mike Gordon's
 line of HOL systems) and later independently by Alexander Maletzky (for Isabelle/HOL).
 \<close>
 
 subsubsection \<open>Core syntax\<close>
 
 setup \<open>Axclass.class_axiomatization (\<^binding>\<open>type\<close>, [])\<close>
 default_sort type
 setup \<open>Object_Logic.add_base_sort \<^sort>\<open>type\<close>\<close>
 
 setup \<open>Proofterm.set_preproc (Proof_Rewrite_Rules.standard_preproc [])\<close>
 
 axiomatization where fun_arity: "OFCLASS('a \<Rightarrow> 'b, type_class)"
 instance "fun" :: (type, type) type by (rule fun_arity)
 
 axiomatization where itself_arity: "OFCLASS('a itself, type_class)"
 instance itself :: (type) type by (rule itself_arity)
 
 typedecl bool
 
 judgment Trueprop :: "bool \<Rightarrow> prop"  ("(_)" 5)
 
 axiomatization implies :: "[bool, bool] \<Rightarrow> bool"  (infixr "\<longrightarrow>" 25)
   and eq :: "['a, 'a] \<Rightarrow> bool"
   and The :: "('a \<Rightarrow> bool) \<Rightarrow> 'a"
 
 notation (input)
   eq  (infixl "=" 50)
 notation (output)
   eq  (infix "=" 50)
 
 text \<open>The input syntax for \<open>eq\<close> is more permissive than the output syntax
 because of the large amount of material that relies on infixl.\<close>
 
 subsubsection \<open>Defined connectives and quantifiers\<close>
 
 definition True :: bool
   where "True \<equiv> ((\<lambda>x::bool. x) = (\<lambda>x. x))"
 
 definition All :: "('a \<Rightarrow> bool) \<Rightarrow> bool"  (binder "\<forall>" 10)
   where "All P \<equiv> (P = (\<lambda>x. True))"
 
 definition Ex :: "('a \<Rightarrow> bool) \<Rightarrow> bool"  (binder "\<exists>" 10)
   where "Ex P \<equiv> \<forall>Q. (\<forall>x. P x \<longrightarrow> Q) \<longrightarrow> Q"
 
 definition False :: bool
   where "False \<equiv> (\<forall>P. P)"
 
 definition Not :: "bool \<Rightarrow> bool"  ("\<not> _" [40] 40)
   where not_def: "\<not> P \<equiv> P \<longrightarrow> False"
 
 definition conj :: "[bool, bool] \<Rightarrow> bool"  (infixr "\<and>" 35)
   where and_def: "P \<and> Q \<equiv> \<forall>R. (P \<longrightarrow> Q \<longrightarrow> R) \<longrightarrow> R"
 
 definition disj :: "[bool, bool] \<Rightarrow> bool"  (infixr "\<or>" 30)
   where or_def: "P \<or> Q \<equiv> \<forall>R. (P \<longrightarrow> R) \<longrightarrow> (Q \<longrightarrow> R) \<longrightarrow> R"
 
 definition Uniq :: "('a \<Rightarrow> bool) \<Rightarrow> bool"
   where "Uniq P \<equiv> (\<forall>x y. P x \<longrightarrow> P y \<longrightarrow> y = x)"
 
 definition Ex1 :: "('a \<Rightarrow> bool) \<Rightarrow> bool"
   where "Ex1 P \<equiv> \<exists>x. P x \<and> (\<forall>y. P y \<longrightarrow> y = x)"
 
 
 subsubsection \<open>Additional concrete syntax\<close>
 
 syntax (ASCII) "_Uniq" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool"  ("(4?< _./ _)" [0, 10] 10)
 syntax "_Uniq" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool"  ("(2\<exists>\<^sub>\<le>\<^sub>1 _./ _)" [0, 10] 10)
 translations "\<exists>\<^sub>\<le>\<^sub>1x. P" \<rightleftharpoons> "CONST Uniq (\<lambda>x. P)"
 
 print_translation \<open>
  [Syntax_Trans.preserve_binder_abs_tr' \<^const_syntax>\<open>Uniq\<close> \<^syntax_const>\<open>_Uniq\<close>]
 \<close> \<comment> \<open>to avoid eta-contraction of body\<close>
 
 
 syntax (ASCII)
   "_Ex1" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool"  ("(3EX! _./ _)" [0, 10] 10)
 syntax (input)
   "_Ex1" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool"  ("(3?! _./ _)" [0, 10] 10)
 syntax "_Ex1" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool"  ("(3\<exists>!_./ _)" [0, 10] 10)
 translations "\<exists>!x. P" \<rightleftharpoons> "CONST Ex1 (\<lambda>x. P)"
 
 print_translation \<open>
  [Syntax_Trans.preserve_binder_abs_tr' \<^const_syntax>\<open>Ex1\<close> \<^syntax_const>\<open>_Ex1\<close>]
 \<close> \<comment> \<open>to avoid eta-contraction of body\<close>
 
 
 syntax
   "_Not_Ex" :: "idts \<Rightarrow> bool \<Rightarrow> bool"  ("(3\<nexists>_./ _)" [0, 10] 10)
   "_Not_Ex1" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool"  ("(3\<nexists>!_./ _)" [0, 10] 10)
 translations
   "\<nexists>x. P" \<rightleftharpoons> "\<not> (\<exists>x. P)"
   "\<nexists>!x. P" \<rightleftharpoons> "\<not> (\<exists>!x. P)"
 
 
 abbreviation not_equal :: "['a, 'a] \<Rightarrow> bool"  (infix "\<noteq>" 50)
   where "x \<noteq> y \<equiv> \<not> (x = y)"
 
 notation (ASCII)
   Not  ("~ _" [40] 40) and
   conj  (infixr "&" 35) and
   disj  (infixr "|" 30) and
   implies  (infixr "-->" 25) and
   not_equal  (infix "~=" 50)
 
 abbreviation (iff)
   iff :: "[bool, bool] \<Rightarrow> bool"  (infixr "\<longleftrightarrow>" 25)
   where "A \<longleftrightarrow> B \<equiv> A = B"
 
 syntax "_The" :: "[pttrn, bool] \<Rightarrow> 'a"  ("(3THE _./ _)" [0, 10] 10)
 translations "THE x. P" \<rightleftharpoons> "CONST The (\<lambda>x. P)"
 print_translation \<open>
   [(\<^const_syntax>\<open>The\<close>, fn _ => fn [Abs abs] =>
       let val (x, t) = Syntax_Trans.atomic_abs_tr' abs
       in Syntax.const \<^syntax_const>\<open>_The\<close> $ x $ t end)]
 \<close>  \<comment> \<open>To avoid eta-contraction of body\<close>
 
 nonterminal letbinds and letbind
 syntax
   "_bind"       :: "[pttrn, 'a] \<Rightarrow> letbind"              ("(2_ =/ _)" 10)
   ""            :: "letbind \<Rightarrow> letbinds"                 ("_")
   "_binds"      :: "[letbind, letbinds] \<Rightarrow> letbinds"     ("_;/ _")
   "_Let"        :: "[letbinds, 'a] \<Rightarrow> 'a"                ("(let (_)/ in (_))" [0, 10] 10)
 
 nonterminal case_syn and cases_syn
 syntax
   "_case_syntax" :: "['a, cases_syn] \<Rightarrow> 'b"  ("(case _ of/ _)" 10)
   "_case1" :: "['a, 'b] \<Rightarrow> case_syn"  ("(2_ \<Rightarrow>/ _)" 10)
   "" :: "case_syn \<Rightarrow> cases_syn"  ("_")
   "_case2" :: "[case_syn, cases_syn] \<Rightarrow> cases_syn"  ("_/ | _")
 syntax (ASCII)
   "_case1" :: "['a, 'b] \<Rightarrow> case_syn"  ("(2_ =>/ _)" 10)
 
 notation (ASCII)
   All  (binder "ALL " 10) and
   Ex  (binder "EX " 10)
 
 notation (input)
   All  (binder "! " 10) and
   Ex  (binder "? " 10)
 
 
 subsubsection \<open>Axioms and basic definitions\<close>
 
 axiomatization where
   refl: "t = (t::'a)" and
   subst: "s = t \<Longrightarrow> P s \<Longrightarrow> P t" and
   ext: "(\<And>x::'a. (f x ::'b) = g x) \<Longrightarrow> (\<lambda>x. f x) = (\<lambda>x. g x)"
     \<comment> \<open>Extensionality is built into the meta-logic, and this rule expresses
          a related property.  It is an eta-expanded version of the traditional
          rule, and similar to the ABS rule of HOL\<close> and
 
   the_eq_trivial: "(THE x. x = a) = (a::'a)"
 
 axiomatization where
   impI: "(P \<Longrightarrow> Q) \<Longrightarrow> P \<longrightarrow> Q" and
   mp: "\<lbrakk>P \<longrightarrow> Q; P\<rbrakk> \<Longrightarrow> Q" and
 
   True_or_False: "(P = True) \<or> (P = False)"
 
 definition If :: "bool \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a" ("(if (_)/ then (_)/ else (_))" [0, 0, 10] 10)
   where "If P x y \<equiv> (THE z::'a. (P = True \<longrightarrow> z = x) \<and> (P = False \<longrightarrow> z = y))"
 
 definition Let :: "'a \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b"
   where "Let s f \<equiv> f s"
 
 translations
   "_Let (_binds b bs) e"  \<rightleftharpoons> "_Let b (_Let bs e)"
   "let x = a in e"        \<rightleftharpoons> "CONST Let a (\<lambda>x. e)"
 
 axiomatization undefined :: 'a
 
 class default = fixes default :: 'a
 
 
 subsection \<open>Fundamental rules\<close>
 
 subsubsection \<open>Equality\<close>
 
 lemma sym: "s = t \<Longrightarrow> t = s"
   by (erule subst) (rule refl)
 
 lemma ssubst: "t = s \<Longrightarrow> P s \<Longrightarrow> P t"
   by (drule sym) (erule subst)
 
 lemma trans: "\<lbrakk>r = s; s = t\<rbrakk> \<Longrightarrow> r = t"
   by (erule subst)
 
 lemma trans_sym [Pure.elim?]: "r = s \<Longrightarrow> t = s \<Longrightarrow> r = t"
   by (rule trans [OF _ sym])
 
 lemma meta_eq_to_obj_eq:
   assumes "A \<equiv> B"
   shows "A = B"
   unfolding assms by (rule refl)
 
 text \<open>Useful with \<open>erule\<close> for proving equalities from known equalities.\<close>
      (* a = b
         |   |
         c = d   *)
 lemma box_equals: "\<lbrakk>a = b; a = c; b = d\<rbrakk> \<Longrightarrow> c = d"
   by (iprover intro: sym trans)
 
 text \<open>For calculational reasoning:\<close>
 
 lemma forw_subst: "a = b \<Longrightarrow> P b \<Longrightarrow> P a"
   by (rule ssubst)
 
 lemma back_subst: "P a \<Longrightarrow> a = b \<Longrightarrow> P b"
   by (rule subst)
 
 
 subsubsection \<open>Congruence rules for application\<close>
 
 text \<open>Similar to \<open>AP_THM\<close> in Gordon's HOL.\<close>
 lemma fun_cong: "(f :: 'a \<Rightarrow> 'b) = g \<Longrightarrow> f x = g x"
   by (iprover intro: refl elim: subst)
 
 text \<open>Similar to \<open>AP_TERM\<close> in Gordon's HOL and FOL's \<open>subst_context\<close>.\<close>
 lemma arg_cong: "x = y \<Longrightarrow> f x = f y"
   by (iprover intro: refl elim: subst)
 
 lemma arg_cong2: "\<lbrakk>a = b; c = d\<rbrakk> \<Longrightarrow> f a c = f b d"
   by (iprover intro: refl elim: subst)
 
 lemma cong: "\<lbrakk>f = g; (x::'a) = y\<rbrakk> \<Longrightarrow> f x = g y"
   by (iprover intro: refl elim: subst)
 
 ML \<open>fun cong_tac ctxt = Cong_Tac.cong_tac ctxt @{thm cong}\<close>
 
 
 subsubsection \<open>Equality of booleans -- iff\<close>
 
 lemma iffD2: "\<lbrakk>P = Q; Q\<rbrakk> \<Longrightarrow> P"
   by (erule ssubst)
 
 lemma rev_iffD2: "\<lbrakk>Q; P = Q\<rbrakk> \<Longrightarrow> P"
   by (erule iffD2)
 
 lemma iffD1: "Q = P \<Longrightarrow> Q \<Longrightarrow> P"
   by (drule sym) (rule iffD2)
 
 lemma rev_iffD1: "Q \<Longrightarrow> Q = P \<Longrightarrow> P"
   by (drule sym) (rule rev_iffD2)
 
 lemma iffE:
   assumes major: "P = Q"
     and minor: "\<lbrakk>P \<longrightarrow> Q; Q \<longrightarrow> P\<rbrakk> \<Longrightarrow> R"
   shows R
   by (iprover intro: minor impI major [THEN iffD2] major [THEN iffD1])
 
 
 subsubsection \<open>True (1)\<close>
 
 lemma TrueI: True
   unfolding True_def by (rule refl)
 
 lemma eqTrueE: "P = True \<Longrightarrow> P"
   by (erule iffD2) (rule TrueI)
 
 
 subsubsection \<open>Universal quantifier (1)\<close>
 
 lemma spec: "\<forall>x::'a. P x \<Longrightarrow> P x"
   unfolding All_def by (iprover intro: eqTrueE fun_cong)
 
 lemma allE:
   assumes major: "\<forall>x. P x" and minor: "P x \<Longrightarrow> R"
   shows R
   by (iprover intro: minor major [THEN spec])
 
 lemma all_dupE:
   assumes major: "\<forall>x. P x" and minor: "\<lbrakk>P x; \<forall>x. P x\<rbrakk> \<Longrightarrow> R"
   shows R
   by (iprover intro: minor major major [THEN spec])
 
 
 subsubsection \<open>False\<close>
 
 text \<open>
   Depends upon \<open>spec\<close>; it is impossible to do propositional
   logic before quantifiers!
 \<close>
 
 lemma FalseE: "False \<Longrightarrow> P"
   unfolding False_def by (erule spec)
 
 lemma False_neq_True: "False = True \<Longrightarrow> P"
   by (erule eqTrueE [THEN FalseE])
 
 
 subsubsection \<open>Negation\<close>
 
 lemma notI:
   assumes "P \<Longrightarrow> False"
   shows "\<not> P"
   unfolding not_def by (iprover intro: impI assms)
 
 lemma False_not_True: "False \<noteq> True"
   by (iprover intro: notI elim: False_neq_True)
 
 lemma True_not_False: "True \<noteq> False"
   by (iprover intro: notI dest: sym elim: False_neq_True)
 
 lemma notE: "\<lbrakk>\<not> P; P\<rbrakk> \<Longrightarrow> R"
   unfolding not_def
   by (iprover intro: mp [THEN FalseE])
 
 
 subsubsection \<open>Implication\<close>
 
 lemma impE:
   assumes "P \<longrightarrow> Q" P "Q \<Longrightarrow> R"
   shows R
   by (iprover intro: assms mp)
 
 text \<open>Reduces \<open>Q\<close> to \<open>P \<longrightarrow> Q\<close>, allowing substitution in \<open>P\<close>.\<close>
 lemma rev_mp: "\<lbrakk>P; P \<longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
   by (rule mp)
 
 lemma contrapos_nn:
   assumes major: "\<not> Q"
     and minor: "P \<Longrightarrow> Q"
   shows "\<not> P"
   by (iprover intro: notI minor major [THEN notE])
 
 text \<open>Not used at all, but we already have the other 3 combinations.\<close>
 lemma contrapos_pn:
   assumes major: "Q"
     and minor: "P \<Longrightarrow> \<not> Q"
   shows "\<not> P"
   by (iprover intro: notI minor major notE)
 
 lemma not_sym: "t \<noteq> s \<Longrightarrow> s \<noteq> t"
   by (erule contrapos_nn) (erule sym)
 
 lemma eq_neq_eq_imp_neq: "\<lbrakk>x = a; a \<noteq> b; b = y\<rbrakk> \<Longrightarrow> x \<noteq> y"
   by (erule subst, erule ssubst, assumption)
 
 
 subsubsection \<open>Disjunction (1)\<close>
 
 lemma disjE:
   assumes major: "P \<or> Q"
     and minorP: "P \<Longrightarrow> R"
     and minorQ: "Q \<Longrightarrow> R"
   shows R
   by (iprover intro: minorP minorQ impI
       major [unfolded or_def, THEN spec, THEN mp, THEN mp])
 
 
 subsubsection \<open>Derivation of \<open>iffI\<close>\<close>
 
 text \<open>In an intuitionistic version of HOL \<open>iffI\<close> needs to be an axiom.\<close>
 
 lemma iffI:
   assumes "P \<Longrightarrow> Q" and "Q \<Longrightarrow> P"
   shows "P = Q"
 proof (rule disjE[OF True_or_False[of P]])
   assume 1: "P = True"
   note Q = assms(1)[OF eqTrueE[OF this]]
   from 1 show ?thesis
   proof (rule ssubst)
     from True_or_False[of Q] show "True = Q"
     proof (rule disjE)
       assume "Q = True"
       thus ?thesis by(rule sym)
     next
       assume "Q = False"
       with Q have False by (rule rev_iffD1)
       thus ?thesis by (rule FalseE)
     qed
   qed
 next
   assume 2: "P = False"
   thus ?thesis
   proof (rule ssubst)
     from True_or_False[of Q] show "False = Q"
     proof (rule disjE)
       assume "Q = True"
       from 2 assms(2)[OF eqTrueE[OF this]] have False by (rule iffD1)
       thus ?thesis by (rule FalseE)
     next
       assume "Q = False"
       thus ?thesis by(rule sym)
     qed
   qed
 qed
 
 
 subsubsection \<open>True (2)\<close>
 
 lemma eqTrueI: "P \<Longrightarrow> P = True"
   by (iprover intro: iffI TrueI)
 
 
 subsubsection \<open>Universal quantifier (2)\<close>
 
 lemma allI:
   assumes "\<And>x::'a. P x"
   shows "\<forall>x. P x"
   unfolding All_def by (iprover intro: ext eqTrueI assms)
 
 
 subsubsection \<open>Existential quantifier\<close>
 
 lemma exI: "P x \<Longrightarrow> \<exists>x::'a. P x"
   unfolding Ex_def by (iprover intro: allI allE impI mp)
 
 lemma exE:
   assumes major: "\<exists>x::'a. P x"
     and minor: "\<And>x. P x \<Longrightarrow> Q"
   shows "Q"
   by (rule major [unfolded Ex_def, THEN spec, THEN mp]) (iprover intro: impI [THEN allI] minor)
 
 
 subsubsection \<open>Conjunction\<close>
 
 lemma conjI: "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> P \<and> Q"
   unfolding and_def by (iprover intro: impI [THEN allI] mp)
 
 lemma conjunct1: "\<lbrakk>P \<and> Q\<rbrakk> \<Longrightarrow> P"
   unfolding and_def by (iprover intro: impI dest: spec mp)
 
 lemma conjunct2: "\<lbrakk>P \<and> Q\<rbrakk> \<Longrightarrow> Q"
   unfolding and_def by (iprover intro: impI dest: spec mp)
 
 lemma conjE:
   assumes major: "P \<and> Q"
     and minor: "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> R"
   shows R
 proof (rule minor)
   show P by (rule major [THEN conjunct1])
   show Q by (rule major [THEN conjunct2])
 qed
 
 lemma context_conjI:
   assumes P "P \<Longrightarrow> Q"
   shows "P \<and> Q"
   by (iprover intro: conjI assms)
 
 
 subsubsection \<open>Disjunction (2)\<close>
 
 lemma disjI1: "P \<Longrightarrow> P \<or> Q"
   unfolding or_def by (iprover intro: allI impI mp)
 
 lemma disjI2: "Q \<Longrightarrow> P \<or> Q"
   unfolding or_def by (iprover intro: allI impI mp)
 
 
 subsubsection \<open>Classical logic\<close>
 
 lemma classical:
   assumes "\<not> P \<Longrightarrow> P"
   shows P
 proof (rule True_or_False [THEN disjE])
   show P if "P = True"
     using that by (iprover intro: eqTrueE)
   show P if "P = False"
   proof (intro notI assms)
     assume P
     with that show False
       by (iprover elim: subst)
   qed
 qed
 
 lemmas ccontr = FalseE [THEN classical]
 
 text \<open>\<open>notE\<close> with premises exchanged; it discharges \<open>\<not> R\<close> so that it can be used to
   make elimination rules.\<close>
 lemma rev_notE:
   assumes premp: P
     and premnot: "\<not> R \<Longrightarrow> \<not> P"
   shows R
   by (iprover intro: ccontr notE [OF premnot premp])
 
 
 text \<open>Double negation law.\<close>
 lemma notnotD: "\<not>\<not> P \<Longrightarrow> P"
   by (iprover intro: ccontr notE )
 
 lemma contrapos_pp:
   assumes p1: Q
     and p2: "\<not> P \<Longrightarrow> \<not> Q"
   shows P
   by (iprover intro: classical p1 p2 notE)
 
 
 subsubsection \<open>Unique existence\<close>
 
 lemma Uniq_I [intro?]:
   assumes "\<And>x y. \<lbrakk>P x; P y\<rbrakk> \<Longrightarrow> y = x"
   shows "Uniq P"
   unfolding Uniq_def by (iprover intro: assms allI impI)
 
 lemma Uniq_D [dest?]: "\<lbrakk>Uniq P; P a; P b\<rbrakk> \<Longrightarrow> a=b"
   unfolding Uniq_def by (iprover dest: spec mp)
 
 lemma ex1I:
   assumes "P a" "\<And>x. P x \<Longrightarrow> x = a"
   shows "\<exists>!x. P x"
   unfolding Ex1_def by (iprover intro: assms exI conjI allI impI)
 
 text \<open>Sometimes easier to use: the premises have no shared variables. Safe!\<close>
 lemma ex_ex1I:
   assumes ex_prem: "\<exists>x. P x"
     and eq: "\<And>x y. \<lbrakk>P x; P y\<rbrakk> \<Longrightarrow> x = y"
   shows "\<exists>!x. P x"
   by (iprover intro: ex_prem [THEN exE] ex1I eq)
 
 lemma ex1E:
   assumes major: "\<exists>!x. P x" and minor: "\<And>x. \<lbrakk>P x; \<forall>y. P y \<longrightarrow> y = x\<rbrakk> \<Longrightarrow> R"
   shows R
 proof (rule major [unfolded Ex1_def, THEN exE])
   show "\<And>x. P x \<and> (\<forall>y. P y \<longrightarrow> y = x) \<Longrightarrow> R"
     by (iprover intro: minor elim: conjE)
 qed
 
 lemma ex1_implies_ex: "\<exists>!x. P x \<Longrightarrow> \<exists>x. P x"
   by (iprover intro: exI elim: ex1E)
 
 subsubsection \<open>Classical intro rules for disjunction and existential quantifiers\<close>
 
 lemma disjCI:
   assumes "\<not> Q \<Longrightarrow> P"
   shows "P \<or> Q"
   by (rule classical) (iprover intro: assms disjI1 disjI2 notI elim: notE)
 
 lemma excluded_middle: "\<not> P \<or> P"
   by (iprover intro: disjCI)
 
 text \<open>
   case distinction as a natural deduction rule.
   Note that \<open>\<not> P\<close> is the second case, not the first.
 \<close>
 lemma case_split [case_names True False]:
   assumes "P \<Longrightarrow> Q" "\<not> P \<Longrightarrow> Q"
   shows Q
   using excluded_middle [of P]
     by (iprover intro: assms elim: disjE)
 
 text \<open>Classical implies (\<open>\<longrightarrow>\<close>) elimination.\<close>
 lemma impCE:
   assumes major: "P \<longrightarrow> Q"
     and minor: "\<not> P \<Longrightarrow> R" "Q \<Longrightarrow> R"
   shows R
   using excluded_middle [of P]
   by (iprover intro: minor major [THEN mp] elim: disjE)+
 
 text \<open>
   This version of \<open>\<longrightarrow>\<close> elimination works on \<open>Q\<close> before \<open>P\<close>.  It works best for
   those cases in which \<open>P\<close> holds "almost everywhere".  Can't install as
   default: would break old proofs.
 \<close>
 lemma impCE':
   assumes major: "P \<longrightarrow> Q"
     and minor: "Q \<Longrightarrow> R" "\<not> P \<Longrightarrow> R"
   shows R
   using assms by (elim impCE)
 
 
 text \<open>Classical \<open>\<longleftrightarrow>\<close> elimination.\<close>
 lemma iffCE:
   assumes major: "P = Q"
     and minor: "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> R" "\<lbrakk>\<not> P; \<not> Q\<rbrakk> \<Longrightarrow> R"
   shows R
   by (rule major [THEN iffE]) (iprover intro: minor elim: impCE notE)
 
 lemma exCI:
   assumes "\<forall>x. \<not> P x \<Longrightarrow> P a"
   shows "\<exists>x. P x"
   by (rule ccontr) (iprover intro: assms exI allI notI notE [of "\<exists>x. P x"])
 
 
 subsubsection \<open>Intuitionistic Reasoning\<close>
 
 lemma impE':
   assumes 1: "P \<longrightarrow> Q"
     and 2: "Q \<Longrightarrow> R"
     and 3: "P \<longrightarrow> Q \<Longrightarrow> P"
   shows R
 proof -
   from 3 and 1 have P .
   with 1 have Q by (rule impE)
   with 2 show R .
 qed
 
 lemma allE':
   assumes 1: "\<forall>x. P x"
     and 2: "P x \<Longrightarrow> \<forall>x. P x \<Longrightarrow> Q"
   shows Q
 proof -
   from 1 have "P x" by (rule spec)
   from this and 1 show Q by (rule 2)
 qed
 
 lemma notE':
   assumes 1: "\<not> P"
     and 2: "\<not> P \<Longrightarrow> P"
   shows R
 proof -
   from 2 and 1 have P .
   with 1 show R by (rule notE)
 qed
 
 lemma TrueE: "True \<Longrightarrow> P \<Longrightarrow> P" .
 lemma notFalseE: "\<not> False \<Longrightarrow> P \<Longrightarrow> P" .
 
 lemmas [Pure.elim!] = disjE iffE FalseE conjE exE TrueE notFalseE
   and [Pure.intro!] = iffI conjI impI TrueI notI allI refl
   and [Pure.elim 2] = allE notE' impE'
   and [Pure.intro] = exI disjI2 disjI1
 
 lemmas [trans] = trans
   and [sym] = sym not_sym
   and [Pure.elim?] = iffD1 iffD2 impE
 
 
 subsubsection \<open>Atomizing meta-level connectives\<close>
 
 axiomatization where
   eq_reflection: "x = y \<Longrightarrow> x \<equiv> y"  \<comment> \<open>admissible axiom\<close>
 
 lemma atomize_all [atomize]: "(\<And>x. P x) \<equiv> Trueprop (\<forall>x. P x)"
 proof
   assume "\<And>x. P x"
   then show "\<forall>x. P x" ..
 next
   assume "\<forall>x. P x"
   then show "\<And>x. P x" by (rule allE)
 qed
 
 lemma atomize_imp [atomize]: "(A \<Longrightarrow> B) \<equiv> Trueprop (A \<longrightarrow> B)"
 proof
   assume r: "A \<Longrightarrow> B"
   show "A \<longrightarrow> B" by (rule impI) (rule r)
 next
   assume "A \<longrightarrow> B" and A
   then show B by (rule mp)
 qed
 
 lemma atomize_not: "(A \<Longrightarrow> False) \<equiv> Trueprop (\<not> A)"
 proof
   assume r: "A \<Longrightarrow> False"
   show "\<not> A" by (rule notI) (rule r)
 next
   assume "\<not> A" and A
   then show False by (rule notE)
 qed
 
 lemma atomize_eq [atomize, code]: "(x \<equiv> y) \<equiv> Trueprop (x = y)"
 proof
   assume "x \<equiv> y"
   show "x = y" by (unfold \<open>x \<equiv> y\<close>) (rule refl)
 next
   assume "x = y"
   then show "x \<equiv> y" by (rule eq_reflection)
 qed
 
 lemma atomize_conj [atomize]: "(A &&& B) \<equiv> Trueprop (A \<and> B)"
 proof
   assume conj: "A &&& B"
   show "A \<and> B"
   proof (rule conjI)
     from conj show A by (rule conjunctionD1)
     from conj show B by (rule conjunctionD2)
   qed
 next
   assume conj: "A \<and> B"
   show "A &&& B"
   proof -
     from conj show A ..
     from conj show B ..
   qed
 qed
 
 lemmas [symmetric, rulify] = atomize_all atomize_imp
   and [symmetric, defn] = atomize_all atomize_imp atomize_eq
 
 
 subsubsection \<open>Atomizing elimination rules\<close>
 
 lemma atomize_exL[atomize_elim]: "(\<And>x. P x \<Longrightarrow> Q) \<equiv> ((\<exists>x. P x) \<Longrightarrow> Q)"
   by rule iprover+
 
 lemma atomize_conjL[atomize_elim]: "(A \<Longrightarrow> B \<Longrightarrow> C) \<equiv> (A \<and> B \<Longrightarrow> C)"
   by rule iprover+
 
 lemma atomize_disjL[atomize_elim]: "((A \<Longrightarrow> C) \<Longrightarrow> (B \<Longrightarrow> C) \<Longrightarrow> C) \<equiv> ((A \<or> B \<Longrightarrow> C) \<Longrightarrow> C)"
   by rule iprover+
 
 lemma atomize_elimL[atomize_elim]: "(\<And>B. (A \<Longrightarrow> B) \<Longrightarrow> B) \<equiv> Trueprop A" ..
 
 
 subsection \<open>Package setup\<close>
 
 ML_file \<open>Tools/hologic.ML\<close>
 ML_file \<open>Tools/rewrite_hol_proof.ML\<close>
 
 setup \<open>Proofterm.set_preproc (Proof_Rewrite_Rules.standard_preproc Rewrite_HOL_Proof.rews)\<close>
 
 
 subsubsection \<open>Sledgehammer setup\<close>
 
 text \<open>
   Theorems blacklisted to Sledgehammer. These theorems typically produce clauses
   that are prolific (match too many equality or membership literals) and relate to
   seldom-used facts. Some duplicate other rules.
 \<close>
 
 named_theorems no_atp "theorems that should be filtered out by Sledgehammer"
 
 
 subsubsection \<open>Classical Reasoner setup\<close>
 
 lemma imp_elim: "P \<longrightarrow> Q \<Longrightarrow> (\<not> R \<Longrightarrow> P) \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R"
   by (rule classical) iprover
 
 lemma swap: "\<not> P \<Longrightarrow> (\<not> R \<Longrightarrow> P) \<Longrightarrow> R"
   by (rule classical) iprover
 
 lemma thin_refl: "\<lbrakk>x = x; PROP W\<rbrakk> \<Longrightarrow> PROP W" .
 
 ML \<open>
 structure Hypsubst = Hypsubst
 (
   val dest_eq = HOLogic.dest_eq
   val dest_Trueprop = HOLogic.dest_Trueprop
   val dest_imp = HOLogic.dest_imp
   val eq_reflection = @{thm eq_reflection}
   val rev_eq_reflection = @{thm meta_eq_to_obj_eq}
   val imp_intr = @{thm impI}
   val rev_mp = @{thm rev_mp}
   val subst = @{thm subst}
   val sym = @{thm sym}
   val thin_refl = @{thm thin_refl};
 );
 open Hypsubst;
 
 structure Classical = Classical
 (
   val imp_elim = @{thm imp_elim}
   val not_elim = @{thm notE}
   val swap = @{thm swap}
   val classical = @{thm classical}
   val sizef = Drule.size_of_thm
   val hyp_subst_tacs = [Hypsubst.hyp_subst_tac]
 );
 
 structure Basic_Classical: BASIC_CLASSICAL = Classical;
 open Basic_Classical;
 \<close>
 
 setup \<open>
   (*prevent substitution on bool*)
   let
     fun non_bool_eq (\<^const_name>\<open>HOL.eq\<close>, Type (_, [T, _])) = T <> \<^typ>\<open>bool\<close>
       | non_bool_eq _ = false;
     fun hyp_subst_tac' ctxt =
       SUBGOAL (fn (goal, i) =>
         if Term.exists_Const non_bool_eq goal
         then Hypsubst.hyp_subst_tac ctxt i
         else no_tac);
   in
     Context_Rules.addSWrapper (fn ctxt => fn tac => hyp_subst_tac' ctxt ORELSE' tac)
   end
 \<close>
 
 declare iffI [intro!]
   and notI [intro!]
   and impI [intro!]
   and disjCI [intro!]
   and conjI [intro!]
   and TrueI [intro!]
   and refl [intro!]
 
 declare iffCE [elim!]
   and FalseE [elim!]
   and impCE [elim!]
   and disjE [elim!]
   and conjE [elim!]
 
 declare ex_ex1I [intro!]
   and allI [intro!]
   and exI [intro]
 
 declare exE [elim!]
   allE [elim]
 
 ML \<open>val HOL_cs = claset_of \<^context>\<close>
 
 lemma contrapos_np: "\<not> Q \<Longrightarrow> (\<not> P \<Longrightarrow> Q) \<Longrightarrow> P"
   by (erule swap)
 
 declare ex_ex1I [rule del, intro! 2]
   and ex1I [intro]
 
 declare ext [intro]
 
 lemmas [intro?] = ext
   and [elim?] = ex1_implies_ex
 
 text \<open>Better than \<open>ex1E\<close> for classical reasoner: needs no quantifier duplication!\<close>
 lemma alt_ex1E [elim!]:
   assumes major: "\<exists>!x. P x"
     and minor: "\<And>x. \<lbrakk>P x; \<forall>y y'. P y \<and> P y' \<longrightarrow> y = y'\<rbrakk> \<Longrightarrow> R"
   shows R
 proof (rule ex1E [OF major minor])
   show "\<forall>y y'. P y \<and> P y' \<longrightarrow> y = y'" if "P x" and \<section>: "\<forall>y. P y \<longrightarrow> y = x" for x
     using \<open>P x\<close> \<section> \<section> by fast
 qed assumption
 
 text \<open>And again using Uniq\<close>
 lemma alt_ex1E':
   assumes  "\<exists>!x. P x" "\<And>x. \<lbrakk>P x; \<exists>\<^sub>\<le>\<^sub>1x. P x\<rbrakk> \<Longrightarrow> R"
   shows R
   using assms unfolding Uniq_def by fast
 
 lemma ex1_iff_ex_Uniq: "(\<exists>!x. P x) \<longleftrightarrow> (\<exists>x. P x) \<and> (\<exists>\<^sub>\<le>\<^sub>1x. P x)"
   unfolding Uniq_def by fast
 
 
 ML \<open>
   structure Blast = Blast
   (
     structure Classical = Classical
     val Trueprop_const = dest_Const \<^const>\<open>Trueprop\<close>
     val equality_name = \<^const_name>\<open>HOL.eq\<close>
     val not_name = \<^const_name>\<open>Not\<close>
     val notE = @{thm notE}
     val ccontr = @{thm ccontr}
     val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
   );
   val blast_tac = Blast.blast_tac;
 \<close>
 
 
 subsubsection \<open>THE: definite description operator\<close>
 
 lemma the_equality [intro]:
   assumes "P a"
     and "\<And>x. P x \<Longrightarrow> x = a"
   shows "(THE x. P x) = a"
   by (blast intro: assms trans [OF arg_cong [where f=The] the_eq_trivial])
 
 lemma theI:
   assumes "P a"
     and "\<And>x. P x \<Longrightarrow> x = a"
   shows "P (THE x. P x)"
   by (iprover intro: assms the_equality [THEN ssubst])
 
 lemma theI': "\<exists>!x. P x \<Longrightarrow> P (THE x. P x)"
   by (blast intro: theI)
 
 text \<open>Easier to apply than \<open>theI\<close>: only one occurrence of \<open>P\<close>.\<close>
 lemma theI2:
   assumes "P a" "\<And>x. P x \<Longrightarrow> x = a" "\<And>x. P x \<Longrightarrow> Q x"
   shows "Q (THE x. P x)"
   by (iprover intro: assms theI)
 
 lemma the1I2:
   assumes "\<exists>!x. P x" "\<And>x. P x \<Longrightarrow> Q x"
   shows "Q (THE x. P x)"
   by (iprover intro: assms(2) theI2[where P=P and Q=Q] ex1E[OF assms(1)] elim: allE impE)
 
 lemma the1_equality [elim?]: "\<lbrakk>\<exists>!x. P x; P a\<rbrakk> \<Longrightarrow> (THE x. P x) = a"
   by blast
 
 lemma the1_equality': "\<lbrakk>\<exists>\<^sub>\<le>\<^sub>1x. P x; P a\<rbrakk> \<Longrightarrow> (THE x. P x) = a"
   unfolding Uniq_def by blast
 
 lemma the_sym_eq_trivial: "(THE y. x = y) = x"
   by blast
 
 
 subsubsection \<open>Simplifier\<close>
 
 lemma eta_contract_eq: "(\<lambda>s. f s) = f" ..
 
 lemma simp_thms:
   shows not_not: "(\<not> \<not> P) = P"
   and Not_eq_iff: "((\<not> P) = (\<not> Q)) = (P = Q)"
   and
     "(P \<noteq> Q) = (P = (\<not> Q))"
     "(P \<or> \<not>P) = True"    "(\<not> P \<or> P) = True"
     "(x = x) = True"
   and not_True_eq_False [code]: "(\<not> True) = False"
   and not_False_eq_True [code]: "(\<not> False) = True"
   and
     "(\<not> P) \<noteq> P"  "P \<noteq> (\<not> P)"
     "(True = P) = P"
   and eq_True: "(P = True) = P"
   and "(False = P) = (\<not> P)"
   and eq_False: "(P = False) = (\<not> P)"
   and
     "(True \<longrightarrow> P) = P"  "(False \<longrightarrow> P) = True"
     "(P \<longrightarrow> True) = True"  "(P \<longrightarrow> P) = True"
     "(P \<longrightarrow> False) = (\<not> P)"  "(P \<longrightarrow> \<not> P) = (\<not> P)"
     "(P \<and> True) = P"  "(True \<and> P) = P"
     "(P \<and> False) = False"  "(False \<and> P) = False"
     "(P \<and> P) = P"  "(P \<and> (P \<and> Q)) = (P \<and> Q)"
     "(P \<and> \<not> P) = False"    "(\<not> P \<and> P) = False"
     "(P \<or> True) = True"  "(True \<or> P) = True"
     "(P \<or> False) = P"  "(False \<or> P) = P"
     "(P \<or> P) = P"  "(P \<or> (P \<or> Q)) = (P \<or> Q)" and
     "(\<forall>x. P) = P"  "(\<exists>x. P) = P"  "\<exists>x. x = t"  "\<exists>x. t = x"
   and
     "\<And>P. (\<exists>x. x = t \<and> P x) = P t"
     "\<And>P. (\<exists>x. t = x \<and> P x) = P t"
     "\<And>P. (\<forall>x. x = t \<longrightarrow> P x) = P t"
     "\<And>P. (\<forall>x. t = x \<longrightarrow> P x) = P t"
     "(\<forall>x. x \<noteq> t) = False"  "(\<forall>x. t \<noteq> x) = False"
   by (blast, blast, blast, blast, blast, iprover+)
 
 lemma disj_absorb: "A \<or> A \<longleftrightarrow> A"
   by blast
 
 lemma disj_left_absorb: "A \<or> (A \<or> B) \<longleftrightarrow> A \<or> B"
   by blast
 
 lemma conj_absorb: "A \<and> A \<longleftrightarrow> A"
   by blast
 
 lemma conj_left_absorb: "A \<and> (A \<and> B) \<longleftrightarrow> A \<and> B"
   by blast
 
 lemma eq_ac:
   shows eq_commute: "a = b \<longleftrightarrow> b = a"
     and iff_left_commute: "(P \<longleftrightarrow> (Q \<longleftrightarrow> R)) \<longleftrightarrow> (Q \<longleftrightarrow> (P \<longleftrightarrow> R))"
     and iff_assoc: "((P \<longleftrightarrow> Q) \<longleftrightarrow> R) \<longleftrightarrow> (P \<longleftrightarrow> (Q \<longleftrightarrow> R))"
   by (iprover, blast+)
 
 lemma neq_commute: "a \<noteq> b \<longleftrightarrow> b \<noteq> a" by iprover
 
 lemma conj_comms:
   shows conj_commute: "P \<and> Q \<longleftrightarrow> Q \<and> P"
     and conj_left_commute: "P \<and> (Q \<and> R) \<longleftrightarrow> Q \<and> (P \<and> R)" by iprover+
 lemma conj_assoc: "(P \<and> Q) \<and> R \<longleftrightarrow> P \<and> (Q \<and> R)" by iprover
 
 lemmas conj_ac = conj_commute conj_left_commute conj_assoc
 
 lemma disj_comms:
   shows disj_commute: "P \<or> Q \<longleftrightarrow> Q \<or> P"
     and disj_left_commute: "P \<or> (Q \<or> R) \<longleftrightarrow> Q \<or> (P \<or> R)" by iprover+
 lemma disj_assoc: "(P \<or> Q) \<or> R \<longleftrightarrow> P \<or> (Q \<or> R)" by iprover
 
 lemmas disj_ac = disj_commute disj_left_commute disj_assoc
 
 lemma conj_disj_distribL: "P \<and> (Q \<or> R) \<longleftrightarrow> P \<and> Q \<or> P \<and> R" by iprover
 lemma conj_disj_distribR: "(P \<or> Q) \<and> R \<longleftrightarrow> P \<and> R \<or> Q \<and> R" by iprover
 
 lemma disj_conj_distribL: "P \<or> (Q \<and> R) \<longleftrightarrow> (P \<or> Q) \<and> (P \<or> R)" by iprover
 lemma disj_conj_distribR: "(P \<and> Q) \<or> R \<longleftrightarrow> (P \<or> R) \<and> (Q \<or> R)" by iprover
 
 lemma imp_conjR: "(P \<longrightarrow> (Q \<and> R)) = ((P \<longrightarrow> Q) \<and> (P \<longrightarrow> R))" by iprover
 lemma imp_conjL: "((P \<and> Q) \<longrightarrow> R) = (P \<longrightarrow> (Q \<longrightarrow> R))" by iprover
 lemma imp_disjL: "((P \<or> Q) \<longrightarrow> R) = ((P \<longrightarrow> R) \<and> (Q \<longrightarrow> R))" by iprover
 
 text \<open>These two are specialized, but \<open>imp_disj_not1\<close> is useful in \<open>Auth/Yahalom\<close>.\<close>
 lemma imp_disj_not1: "(P \<longrightarrow> Q \<or> R) \<longleftrightarrow> (\<not> Q \<longrightarrow> P \<longrightarrow> R)" by blast
 lemma imp_disj_not2: "(P \<longrightarrow> Q \<or> R) \<longleftrightarrow> (\<not> R \<longrightarrow> P \<longrightarrow> Q)" by blast
 
 lemma imp_disj1: "((P \<longrightarrow> Q) \<or> R) \<longleftrightarrow> (P \<longrightarrow> Q \<or> R)" by blast
 lemma imp_disj2: "(Q \<or> (P \<longrightarrow> R)) \<longleftrightarrow> (P \<longrightarrow> Q \<or> R)" by blast
 
 lemma imp_cong: "(P = P') \<Longrightarrow> (P' \<Longrightarrow> (Q = Q')) \<Longrightarrow> ((P \<longrightarrow> Q) \<longleftrightarrow> (P' \<longrightarrow> Q'))"
   by iprover
 
 lemma de_Morgan_disj: "\<not> (P \<or> Q) \<longleftrightarrow> \<not> P \<and> \<not> Q" by iprover
 lemma de_Morgan_conj: "\<not> (P \<and> Q) \<longleftrightarrow> \<not> P \<or> \<not> Q" by blast
 lemma not_imp: "\<not> (P \<longrightarrow> Q) \<longleftrightarrow> P \<and> \<not> Q" by blast
 lemma not_iff: "P \<noteq> Q \<longleftrightarrow> (P \<longleftrightarrow> \<not> Q)" by blast
 lemma disj_not1: "\<not> P \<or> Q \<longleftrightarrow> (P \<longrightarrow> Q)" by blast
 lemma disj_not2: "P \<or> \<not> Q \<longleftrightarrow> (Q \<longrightarrow> P)" by blast  \<comment> \<open>changes orientation :-(\<close>
 lemma imp_conv_disj: "(P \<longrightarrow> Q) \<longleftrightarrow> (\<not> P) \<or> Q" by blast
 lemma disj_imp: "P \<or> Q \<longleftrightarrow> \<not> P \<longrightarrow> Q" by blast
 
 lemma iff_conv_conj_imp: "(P \<longleftrightarrow> Q) \<longleftrightarrow> (P \<longrightarrow> Q) \<and> (Q \<longrightarrow> P)" by iprover
 
 
 lemma cases_simp: "(P \<longrightarrow> Q) \<and> (\<not> P \<longrightarrow> Q) \<longleftrightarrow> Q"
   \<comment> \<open>Avoids duplication of subgoals after \<open>if_split\<close>, when the true and false\<close>
   \<comment> \<open>cases boil down to the same thing.\<close>
   by blast
 
 lemma not_all: "\<not> (\<forall>x. P x) \<longleftrightarrow> (\<exists>x. \<not> P x)" by blast
 lemma imp_all: "((\<forall>x. P x) \<longrightarrow> Q) \<longleftrightarrow> (\<exists>x. P x \<longrightarrow> Q)" by blast
 lemma not_ex: "\<not> (\<exists>x. P x) \<longleftrightarrow> (\<forall>x. \<not> P x)" by iprover
 lemma imp_ex: "((\<exists>x. P x) \<longrightarrow> Q) \<longleftrightarrow> (\<forall>x. P x \<longrightarrow> Q)" by iprover
 lemma all_not_ex: "(\<forall>x. P x) \<longleftrightarrow> \<not> (\<exists>x. \<not> P x)" by blast
 
 declare All_def [no_atp]
 
 lemma ex_disj_distrib: "(\<exists>x. P x \<or> Q x) \<longleftrightarrow> (\<exists>x. P x) \<or> (\<exists>x. Q x)" by iprover
 lemma all_conj_distrib: "(\<forall>x. P x \<and> Q x) \<longleftrightarrow> (\<forall>x. P x) \<and> (\<forall>x. Q x)" by iprover
 
 text \<open>
   \<^medskip> The \<open>\<and>\<close> congruence rule: not included by default!
   May slow rewrite proofs down by as much as 50\%\<close>
 
 lemma conj_cong: "P = P' \<Longrightarrow> (P' \<Longrightarrow> Q = Q') \<Longrightarrow> (P \<and> Q) = (P' \<and> Q')"
   by iprover
 
 lemma rev_conj_cong: "Q = Q' \<Longrightarrow> (Q' \<Longrightarrow> P = P') \<Longrightarrow> (P \<and> Q) = (P' \<and> Q')"
   by iprover
 
 text \<open>The \<open>|\<close> congruence rule: not included by default!\<close>
 
 lemma disj_cong: "P = P' \<Longrightarrow> (\<not> P' \<Longrightarrow> Q = Q') \<Longrightarrow> (P \<or> Q) = (P' \<or> Q')"
   by blast
 
 
 text \<open>\<^medskip> if-then-else rules\<close>
 
 lemma if_True [code]: "(if True then x else y) = x"
   unfolding If_def by blast
 
 lemma if_False [code]: "(if False then x else y) = y"
   unfolding If_def by blast
 
 lemma if_P: "P \<Longrightarrow> (if P then x else y) = x"
   unfolding If_def by blast
 
 lemma if_not_P: "\<not> P \<Longrightarrow> (if P then x else y) = y"
   unfolding If_def by blast
 
 lemma if_split: "P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y))"
 proof (rule case_split [of Q])
   show ?thesis if Q
     using that by (simplesubst if_P) blast+
   show ?thesis if "\<not> Q"
     using that by (simplesubst if_not_P) blast+
 qed
 
 lemma if_split_asm: "P (if Q then x else y) = (\<not> ((Q \<and> \<not> P x) \<or> (\<not> Q \<and> \<not> P y)))"
   by (simplesubst if_split) blast
 
 lemmas if_splits [no_atp] = if_split if_split_asm
 
 lemma if_cancel: "(if c then x else x) = x"
   by (simplesubst if_split) blast
 
 lemma if_eq_cancel: "(if x = y then y else x) = x"
   by (simplesubst if_split) blast
 
 lemma if_bool_eq_conj: "(if P then Q else R) = ((P \<longrightarrow> Q) \<and> (\<not> P \<longrightarrow> R))"
   \<comment> \<open>This form is useful for expanding \<open>if\<close>s on the RIGHT of the \<open>\<Longrightarrow>\<close> symbol.\<close>
   by (rule if_split)
 
 lemma if_bool_eq_disj: "(if P then Q else R) = ((P \<and> Q) \<or> (\<not> P \<and> R))"
   \<comment> \<open>And this form is useful for expanding \<open>if\<close>s on the LEFT.\<close>
   by (simplesubst if_split) blast
 
 lemma Eq_TrueI: "P \<Longrightarrow> P \<equiv> True" unfolding atomize_eq by iprover
 lemma Eq_FalseI: "\<not> P \<Longrightarrow> P \<equiv> False" unfolding atomize_eq by iprover
 
 text \<open>\<^medskip> let rules for simproc\<close>
 
 lemma Let_folded: "f x \<equiv> g x \<Longrightarrow> Let x f \<equiv> Let x g"
   by (unfold Let_def)
 
 lemma Let_unfold: "f x \<equiv> g \<Longrightarrow> Let x f \<equiv> g"
   by (unfold Let_def)
 
 text \<open>
   The following copy of the implication operator is useful for
   fine-tuning congruence rules.  It instructs the simplifier to simplify
   its premise.
 \<close>
 
 definition simp_implies :: "prop \<Rightarrow> prop \<Rightarrow> prop"  (infixr "=simp=>" 1)
   where "simp_implies \<equiv> (\<Longrightarrow>)"
 
 lemma simp_impliesI:
   assumes PQ: "(PROP P \<Longrightarrow> PROP Q)"
   shows "PROP P =simp=> PROP Q"
   unfolding simp_implies_def
   by (iprover intro: PQ)
 
 lemma simp_impliesE:
   assumes PQ: "PROP P =simp=> PROP Q"
     and P: "PROP P"
     and QR: "PROP Q \<Longrightarrow> PROP R"
   shows "PROP R"
   by (iprover intro: QR P PQ [unfolded simp_implies_def])
 
 lemma simp_implies_cong:
   assumes PP' :"PROP P \<equiv> PROP P'"
     and P'QQ': "PROP P' \<Longrightarrow> (PROP Q \<equiv> PROP Q')"
   shows "(PROP P =simp=> PROP Q) \<equiv> (PROP P' =simp=> PROP Q')"
   unfolding simp_implies_def
 proof (rule equal_intr_rule)
   assume PQ: "PROP P \<Longrightarrow> PROP Q"
     and P': "PROP P'"
   from PP' [symmetric] and P' have "PROP P"
     by (rule equal_elim_rule1)
   then have "PROP Q" by (rule PQ)
   with P'QQ' [OF P'] show "PROP Q'" by (rule equal_elim_rule1)
 next
   assume P'Q': "PROP P' \<Longrightarrow> PROP Q'"
     and P: "PROP P"
   from PP' and P have P': "PROP P'" by (rule equal_elim_rule1)
   then have "PROP Q'" by (rule P'Q')
   with P'QQ' [OF P', symmetric] show "PROP Q"
     by (rule equal_elim_rule1)
 qed
 
 lemma uncurry:
   assumes "P \<longrightarrow> Q \<longrightarrow> R"
   shows "P \<and> Q \<longrightarrow> R"
   using assms by blast
 
 lemma iff_allI:
   assumes "\<And>x. P x = Q x"
   shows "(\<forall>x. P x) = (\<forall>x. Q x)"
   using assms by blast
 
 lemma iff_exI:
   assumes "\<And>x. P x = Q x"
   shows "(\<exists>x. P x) = (\<exists>x. Q x)"
   using assms by blast
 
 lemma all_comm: "(\<forall>x y. P x y) = (\<forall>y x. P x y)"
   by blast
 
 lemma ex_comm: "(\<exists>x y. P x y) = (\<exists>y x. P x y)"
   by blast
 
 ML_file \<open>Tools/simpdata.ML\<close>
 ML \<open>open Simpdata\<close>
 
 setup \<open>
   map_theory_simpset (put_simpset HOL_basic_ss) #>
   Simplifier.method_setup Splitter.split_modifiers
 \<close>
 
 simproc_setup defined_Ex ("\<exists>x. P x") = \<open>K Quantifier1.rearrange_ex\<close>
 simproc_setup defined_All ("\<forall>x. P x") = \<open>K Quantifier1.rearrange_all\<close>
 
 text \<open>Simproc for proving \<open>(y = x) \<equiv> False\<close> from premise \<open>\<not> (x = y)\<close>:\<close>
 
 simproc_setup neq ("x = y") = \<open>fn _ =>
   let
     val neq_to_EQ_False = @{thm not_sym} RS @{thm Eq_FalseI};
     fun is_neq eq lhs rhs thm =
       (case Thm.prop_of thm of
         _ $ (Not $ (eq' $ l' $ r')) =>
           Not = HOLogic.Not andalso eq' = eq andalso
           r' aconv lhs andalso l' aconv rhs
       | _ => false);
     fun proc ss ct =
       (case Thm.term_of ct of
         eq $ lhs $ rhs =>
           (case find_first (is_neq eq lhs rhs) (Simplifier.prems_of ss) of
             SOME thm => SOME (thm RS neq_to_EQ_False)
           | NONE => NONE)
        | _ => NONE);
   in proc end
 \<close>
 
 simproc_setup let_simp ("Let x f") = \<open>
   let
     fun count_loose (Bound i) k = if i >= k then 1 else 0
       | count_loose (s $ t) k = count_loose s k + count_loose t k
       | count_loose (Abs (_, _, t)) k = count_loose  t (k + 1)
       | count_loose _ _ = 0;
     fun is_trivial_let (Const (\<^const_name>\<open>Let\<close>, _) $ x $ t) =
       (case t of
         Abs (_, _, t') => count_loose t' 0 <= 1
       | _ => true);
   in
     fn _ => fn ctxt => fn ct =>
       if is_trivial_let (Thm.term_of ct)
       then SOME @{thm Let_def} (*no or one ocurrence of bound variable*)
       else
         let (*Norbert Schirmer's case*)
           val t = Thm.term_of ct;
           val (t', ctxt') = yield_singleton (Variable.import_terms false) t ctxt;
         in
           Option.map (hd o Variable.export ctxt' ctxt o single)
             (case t' of Const (\<^const_name>\<open>Let\<close>,_) $ x $ f => (* x and f are already in normal form *)
               if is_Free x orelse is_Bound x orelse is_Const x
               then SOME @{thm Let_def}
               else
                 let
                   val n = case f of (Abs (x, _, _)) => x | _ => "x";
                   val cx = Thm.cterm_of ctxt x;
                   val xT = Thm.typ_of_cterm cx;
                   val cf = Thm.cterm_of ctxt f;
                   val fx_g = Simplifier.rewrite ctxt (Thm.apply cf cx);
                   val (_ $ _ $ g) = Thm.prop_of fx_g;
                   val g' = abstract_over (x, g);
                   val abs_g'= Abs (n, xT, g');
                 in
                   if g aconv g' then
                     let
                       val rl =
                         infer_instantiate ctxt [(("f", 0), cf), (("x", 0), cx)] @{thm Let_unfold};
                     in SOME (rl OF [fx_g]) end
                   else if (Envir.beta_eta_contract f) aconv (Envir.beta_eta_contract abs_g')
                   then NONE (*avoid identity conversion*)
                   else
                     let
                       val g'x = abs_g' $ x;
                       val g_g'x = Thm.symmetric (Thm.beta_conversion false (Thm.cterm_of ctxt g'x));
                       val rl =
                         @{thm Let_folded} |> infer_instantiate ctxt
                           [(("f", 0), Thm.cterm_of ctxt f),
                            (("x", 0), cx),
                            (("g", 0), Thm.cterm_of ctxt abs_g')];
                     in SOME (rl OF [Thm.transitive fx_g g_g'x]) end
                 end
             | _ => NONE)
         end
   end
 \<close>
 
 lemma True_implies_equals: "(True \<Longrightarrow> PROP P) \<equiv> PROP P"
 proof
   assume "True \<Longrightarrow> PROP P"
   from this [OF TrueI] show "PROP P" .
 next
   assume "PROP P"
   then show "PROP P" .
 qed
 
 lemma implies_True_equals: "(PROP P \<Longrightarrow> True) \<equiv> Trueprop True"
   by standard (intro TrueI)
 
 lemma False_implies_equals: "(False \<Longrightarrow> P) \<equiv> Trueprop True"
   by standard simp_all
 
-(* This is not made a simp rule because it does not improve any proofs
-   but slows some AFP entries down by 5% (cpu time). May 2015 *)
+(* It seems that making this a simp rule is slower than using the simproc below *)
 lemma implies_False_swap:
-  "NO_MATCH (Trueprop False) P \<Longrightarrow>
-    (False \<Longrightarrow> PROP P \<Longrightarrow> PROP Q) \<equiv> (PROP P \<Longrightarrow> False \<Longrightarrow> PROP Q)"
+  "(False \<Longrightarrow> PROP P \<Longrightarrow> PROP Q) \<equiv> (PROP P \<Longrightarrow> False \<Longrightarrow> PROP Q)"
   by (rule swap_prems_eq)
 
+ML \<open>
+fun eliminate_false_implies ct =
+  let
+    val (prems, concl) = Logic.strip_horn (Thm.term_of ct)
+    fun go n =
+      if n > 1 then
+        Conv.rewr_conv @{thm Pure.swap_prems_eq}
+        then_conv Conv.arg_conv (go (n - 1))
+        then_conv Conv.rewr_conv @{thm HOL.implies_True_equals}
+      else
+        Conv.rewr_conv @{thm HOL.False_implies_equals}
+  in
+    case concl of
+      Const (@{const_name HOL.Trueprop}, _) $ _ => SOME (go (length prems) ct)
+    | _ => NONE
+  end
+\<close>
+
+simproc_setup eliminate_false_implies ("False \<Longrightarrow> PROP P") = \<open>K (K eliminate_false_implies)\<close>
+
+
 lemma ex_simps:
   "\<And>P Q. (\<exists>x. P x \<and> Q)   = ((\<exists>x. P x) \<and> Q)"
   "\<And>P Q. (\<exists>x. P \<and> Q x)   = (P \<and> (\<exists>x. Q x))"
   "\<And>P Q. (\<exists>x. P x \<or> Q)   = ((\<exists>x. P x) \<or> Q)"
   "\<And>P Q. (\<exists>x. P \<or> Q x)   = (P \<or> (\<exists>x. Q x))"
   "\<And>P Q. (\<exists>x. P x \<longrightarrow> Q) = ((\<forall>x. P x) \<longrightarrow> Q)"
   "\<And>P Q. (\<exists>x. P \<longrightarrow> Q x) = (P \<longrightarrow> (\<exists>x. Q x))"
   \<comment> \<open>Miniscoping: pushing in existential quantifiers.\<close>
   by (iprover | blast)+
 
 lemma all_simps:
   "\<And>P Q. (\<forall>x. P x \<and> Q)   = ((\<forall>x. P x) \<and> Q)"
   "\<And>P Q. (\<forall>x. P \<and> Q x)   = (P \<and> (\<forall>x. Q x))"
   "\<And>P Q. (\<forall>x. P x \<or> Q)   = ((\<forall>x. P x) \<or> Q)"
   "\<And>P Q. (\<forall>x. P \<or> Q x)   = (P \<or> (\<forall>x. Q x))"
   "\<And>P Q. (\<forall>x. P x \<longrightarrow> Q) = ((\<exists>x. P x) \<longrightarrow> Q)"
   "\<And>P Q. (\<forall>x. P \<longrightarrow> Q x) = (P \<longrightarrow> (\<forall>x. Q x))"
   \<comment> \<open>Miniscoping: pushing in universal quantifiers.\<close>
   by (iprover | blast)+
 
 lemmas [simp] =
   triv_forall_equality  \<comment> \<open>prunes params\<close>
   True_implies_equals implies_True_equals  \<comment> \<open>prune \<open>True\<close> in asms\<close>
   False_implies_equals  \<comment> \<open>prune \<open>False\<close> in asms\<close>
   if_True
   if_False
   if_cancel
   if_eq_cancel
   imp_disjL \<comment> \<open>In general it seems wrong to add distributive laws by default: they
     might cause exponential blow-up.  But \<open>imp_disjL\<close> has been in for a while
     and cannot be removed without affecting existing proofs.  Moreover,
     rewriting by \<open>(P \<or> Q \<longrightarrow> R) = ((P \<longrightarrow> R) \<and> (Q \<longrightarrow> R))\<close> might be justified on the
     grounds that it allows simplification of \<open>R\<close> in the two cases.\<close>
   conj_assoc
   disj_assoc
   de_Morgan_conj
   de_Morgan_disj
   imp_disj1
   imp_disj2
   not_imp
   disj_not1
   not_all
   not_ex
   cases_simp
   the_eq_trivial
   the_sym_eq_trivial
   ex_simps
   all_simps
   simp_thms
 
 lemmas [cong] = imp_cong simp_implies_cong
 lemmas [split] = if_split
 
 ML \<open>val HOL_ss = simpset_of \<^context>\<close>
 
 text \<open>Simplifies \<open>x\<close> assuming \<open>c\<close> and \<open>y\<close> assuming \<open>\<not> c\<close>.\<close>
 lemma if_cong:
   assumes "b = c"
     and "c \<Longrightarrow> x = u"
     and "\<not> c \<Longrightarrow> y = v"
   shows "(if b then x else y) = (if c then u else v)"
   using assms by simp
 
 text \<open>Prevents simplification of \<open>x\<close> and \<open>y\<close>:
   faster and allows the execution of functional programs.\<close>
 lemma if_weak_cong [cong]:
   assumes "b = c"
   shows "(if b then x else y) = (if c then x else y)"
   using assms by (rule arg_cong)
 
 text \<open>Prevents simplification of t: much faster\<close>
 lemma let_weak_cong:
   assumes "a = b"
   shows "(let x = a in t x) = (let x = b in t x)"
   using assms by (rule arg_cong)
 
 text \<open>To tidy up the result of a simproc.  Only the RHS will be simplified.\<close>
 lemma eq_cong2:
   assumes "u = u'"
   shows "(t \<equiv> u) \<equiv> (t \<equiv> u')"
   using assms by simp
 
 lemma if_distrib: "f (if c then x else y) = (if c then f x else f y)"
   by simp
 
 lemma if_distribR: "(if b then f else g) x = (if b then f x else g x)"
   by simp
 
 lemma all_if_distrib: "(\<forall>x. if x = a then P x else Q x) \<longleftrightarrow> P a \<and> (\<forall>x. x\<noteq>a \<longrightarrow> Q x)"
   by auto
 
 lemma ex_if_distrib: "(\<exists>x. if x = a then P x else Q x) \<longleftrightarrow> P a \<or> (\<exists>x. x\<noteq>a \<and> Q x)"
   by auto
 
 lemma if_if_eq_conj: "(if P then if Q then x else y else y) = (if P \<and> Q then x else y)"
   by simp
 
 text \<open>As a simplification rule, it replaces all function equalities by
   first-order equalities.\<close>
 lemma fun_eq_iff: "f = g \<longleftrightarrow> (\<forall>x. f x = g x)"
   by auto
 
 
 subsubsection \<open>Generic cases and induction\<close>
 
 text \<open>Rule projections:\<close>
 ML \<open>
 structure Project_Rule = Project_Rule
 (
   val conjunct1 = @{thm conjunct1}
   val conjunct2 = @{thm conjunct2}
   val mp = @{thm mp}
 );
 \<close>
 
 context
 begin
 
 qualified definition "induct_forall P \<equiv> \<forall>x. P x"
 qualified definition "induct_implies A B \<equiv> A \<longrightarrow> B"
 qualified definition "induct_equal x y \<equiv> x = y"
 qualified definition "induct_conj A B \<equiv> A \<and> B"
 qualified definition "induct_true \<equiv> True"
 qualified definition "induct_false \<equiv> False"
 
 lemma induct_forall_eq: "(\<And>x. P x) \<equiv> Trueprop (induct_forall (\<lambda>x. P x))"
   by (unfold atomize_all induct_forall_def)
 
 lemma induct_implies_eq: "(A \<Longrightarrow> B) \<equiv> Trueprop (induct_implies A B)"
   by (unfold atomize_imp induct_implies_def)
 
 lemma induct_equal_eq: "(x \<equiv> y) \<equiv> Trueprop (induct_equal x y)"
   by (unfold atomize_eq induct_equal_def)
 
 lemma induct_conj_eq: "(A &&& B) \<equiv> Trueprop (induct_conj A B)"
   by (unfold atomize_conj induct_conj_def)
 
 lemmas induct_atomize' = induct_forall_eq induct_implies_eq induct_conj_eq
 lemmas induct_atomize = induct_atomize' induct_equal_eq
 lemmas induct_rulify' [symmetric] = induct_atomize'
 lemmas induct_rulify [symmetric] = induct_atomize
 lemmas induct_rulify_fallback =
   induct_forall_def induct_implies_def induct_equal_def induct_conj_def
   induct_true_def induct_false_def
 
 lemma induct_forall_conj: "induct_forall (\<lambda>x. induct_conj (A x) (B x)) =
     induct_conj (induct_forall A) (induct_forall B)"
   by (unfold induct_forall_def induct_conj_def) iprover
 
 lemma induct_implies_conj: "induct_implies C (induct_conj A B) =
     induct_conj (induct_implies C A) (induct_implies C B)"
   by (unfold induct_implies_def induct_conj_def) iprover
 
 lemma induct_conj_curry: "(induct_conj A B \<Longrightarrow> PROP C) \<equiv> (A \<Longrightarrow> B \<Longrightarrow> PROP C)"
 proof
   assume r: "induct_conj A B \<Longrightarrow> PROP C"
   assume ab: A B
   show "PROP C" by (rule r) (simp add: induct_conj_def ab)
 next
   assume r: "A \<Longrightarrow> B \<Longrightarrow> PROP C"
   assume ab: "induct_conj A B"
   show "PROP C" by (rule r) (simp_all add: ab [unfolded induct_conj_def])
 qed
 
 lemmas induct_conj = induct_forall_conj induct_implies_conj induct_conj_curry
 
 lemma induct_trueI: "induct_true"
   by (simp add: induct_true_def)
 
 text \<open>Method setup.\<close>
 
 ML_file \<open>~~/src/Tools/induct.ML\<close>
 ML \<open>
 structure Induct = Induct
 (
   val cases_default = @{thm case_split}
   val atomize = @{thms induct_atomize}
   val rulify = @{thms induct_rulify'}
   val rulify_fallback = @{thms induct_rulify_fallback}
   val equal_def = @{thm induct_equal_def}
   fun dest_def (Const (\<^const_name>\<open>induct_equal\<close>, _) $ t $ u) = SOME (t, u)
     | dest_def _ = NONE
   fun trivial_tac ctxt = match_tac ctxt @{thms induct_trueI}
 )
 \<close>
 
 ML_file \<open>~~/src/Tools/induction.ML\<close>
 
 declaration \<open>
   fn _ => Induct.map_simpset (fn ss => ss
     addsimprocs
       [Simplifier.make_simproc \<^context> "swap_induct_false"
         {lhss = [\<^term>\<open>induct_false \<Longrightarrow> PROP P \<Longrightarrow> PROP Q\<close>],
          proc = fn _ => fn _ => fn ct =>
           (case Thm.term_of ct of
             _ $ (P as _ $ \<^const>\<open>induct_false\<close>) $ (_ $ Q $ _) =>
               if P <> Q then SOME Drule.swap_prems_eq else NONE
           | _ => NONE)},
        Simplifier.make_simproc \<^context> "induct_equal_conj_curry"
         {lhss = [\<^term>\<open>induct_conj P Q \<Longrightarrow> PROP R\<close>],
          proc = fn _ => fn _ => fn ct =>
           (case Thm.term_of ct of
             _ $ (_ $ P) $ _ =>
               let
                 fun is_conj (\<^const>\<open>induct_conj\<close> $ P $ Q) =
                       is_conj P andalso is_conj Q
                   | is_conj (Const (\<^const_name>\<open>induct_equal\<close>, _) $ _ $ _) = true
                   | is_conj \<^const>\<open>induct_true\<close> = true
                   | is_conj \<^const>\<open>induct_false\<close> = true
                   | is_conj _ = false
               in if is_conj P then SOME @{thm induct_conj_curry} else NONE end
             | _ => NONE)}]
     |> Simplifier.set_mksimps (fn ctxt =>
         Simpdata.mksimps Simpdata.mksimps_pairs ctxt #>
         map (rewrite_rule ctxt (map Thm.symmetric @{thms induct_rulify_fallback}))))
 \<close>
 
 text \<open>Pre-simplification of induction and cases rules\<close>
 
 lemma [induct_simp]: "(\<And>x. induct_equal x t \<Longrightarrow> PROP P x) \<equiv> PROP P t"
   unfolding induct_equal_def
 proof
   assume r: "\<And>x. x = t \<Longrightarrow> PROP P x"
   show "PROP P t" by (rule r [OF refl])
 next
   fix x
   assume "PROP P t" "x = t"
   then show "PROP P x" by simp
 qed
 
 lemma [induct_simp]: "(\<And>x. induct_equal t x \<Longrightarrow> PROP P x) \<equiv> PROP P t"
   unfolding induct_equal_def
 proof
   assume r: "\<And>x. t = x \<Longrightarrow> PROP P x"
   show "PROP P t" by (rule r [OF refl])
 next
   fix x
   assume "PROP P t" "t = x"
   then show "PROP P x" by simp
 qed
 
 lemma [induct_simp]: "(induct_false \<Longrightarrow> P) \<equiv> Trueprop induct_true"
   unfolding induct_false_def induct_true_def
   by (iprover intro: equal_intr_rule)
 
 lemma [induct_simp]: "(induct_true \<Longrightarrow> PROP P) \<equiv> PROP P"
   unfolding induct_true_def
 proof
   assume "True \<Longrightarrow> PROP P"
   then show "PROP P" using TrueI .
 next
   assume "PROP P"
   then show "PROP P" .
 qed
 
 lemma [induct_simp]: "(PROP P \<Longrightarrow> induct_true) \<equiv> Trueprop induct_true"
   unfolding induct_true_def
   by (iprover intro: equal_intr_rule)
 
 lemma [induct_simp]: "(\<And>x::'a::{}. induct_true) \<equiv> Trueprop induct_true"
   unfolding induct_true_def
   by (iprover intro: equal_intr_rule)
 
 lemma [induct_simp]: "induct_implies induct_true P \<equiv> P"
   by (simp add: induct_implies_def induct_true_def)
 
 lemma [induct_simp]: "x = x \<longleftrightarrow> True"
   by (rule simp_thms)
 
 end
 
 ML_file \<open>~~/src/Tools/induct_tacs.ML\<close>
 
 
 subsubsection \<open>Coherent logic\<close>
 
 ML_file \<open>~~/src/Tools/coherent.ML\<close>
 ML \<open>
 structure Coherent = Coherent
 (
   val atomize_elimL = @{thm atomize_elimL};
   val atomize_exL = @{thm atomize_exL};
   val atomize_conjL = @{thm atomize_conjL};
   val atomize_disjL = @{thm atomize_disjL};
   val operator_names = [\<^const_name>\<open>HOL.disj\<close>, \<^const_name>\<open>HOL.conj\<close>, \<^const_name>\<open>Ex\<close>];
 );
 \<close>
 
 
 subsubsection \<open>Reorienting equalities\<close>
 
 ML \<open>
 signature REORIENT_PROC =
 sig
   val add : (term -> bool) -> theory -> theory
   val proc : morphism -> Proof.context -> cterm -> thm option
 end;
 
 structure Reorient_Proc : REORIENT_PROC =
 struct
   structure Data = Theory_Data
   (
     type T = ((term -> bool) * stamp) list;
     val empty = [];
     val extend = I;
     fun merge data : T = Library.merge (eq_snd (op =)) data;
   );
   fun add m = Data.map (cons (m, stamp ()));
   fun matches thy t = exists (fn (m, _) => m t) (Data.get thy);
 
   val meta_reorient = @{thm eq_commute [THEN eq_reflection]};
   fun proc phi ctxt ct =
     let
       val thy = Proof_Context.theory_of ctxt;
     in
       case Thm.term_of ct of
         (_ $ t $ u) => if matches thy u then NONE else SOME meta_reorient
       | _ => NONE
     end;
 end;
 \<close>
 
 
 subsection \<open>Other simple lemmas and lemma duplicates\<close>
 
 lemma all_cong1: "(\<And>x. P x = P' x) \<Longrightarrow> (\<forall>x. P x) = (\<forall>x. P' x)"
   by auto
 
 lemma ex_cong1: "(\<And>x. P x = P' x) \<Longrightarrow> (\<exists>x. P x) = (\<exists>x. P' x)"
   by auto
 
 lemma all_cong: "(\<And>x. Q x \<Longrightarrow> P x = P' x) \<Longrightarrow> (\<forall>x. Q x \<longrightarrow> P x) = (\<forall>x. Q x \<longrightarrow> P' x)"
   by auto
 
 lemma ex_cong: "(\<And>x. Q x \<Longrightarrow> P x = P' x) \<Longrightarrow> (\<exists>x. Q x \<and> P x) = (\<exists>x. Q x \<and> P' x)"
   by auto
 
 lemma ex1_eq [iff]: "\<exists>!x. x = t" "\<exists>!x. t = x"
   by blast+
 
 lemma choice_eq: "(\<forall>x. \<exists>!y. P x y) = (\<exists>!f. \<forall>x. P x (f x))" (is "?lhs = ?rhs")
 proof (intro iffI allI)
   assume L: ?lhs
   then have \<section>: "\<forall>x. P x (THE y. P x y)"
     by (best intro: theI')
   show ?rhs
     by (rule ex1I) (use L \<section> in \<open>fast+\<close>)
 next
   fix x
   assume R: ?rhs
   then obtain f where f: "\<forall>x. P x (f x)" and f1: "\<And>y. (\<forall>x. P x (y x)) \<Longrightarrow> y = f"
     by (blast elim: ex1E)
   show "\<exists>!y. P x y"
   proof (rule ex1I)
     show "P x (f x)"
       using f by blast
     show "y = f x" if "P x y" for y
     proof -
       have "P z (if z = x then y else f z)" for z
         using f that by (auto split: if_split)
       with f1 [of "\<lambda>z. if z = x then y else f z"] f
       show ?thesis
         by (auto simp add: split: if_split_asm dest: fun_cong)
     qed
   qed
 qed
 
 lemmas eq_sym_conv = eq_commute
 
 lemma nnf_simps:
   "(\<not> (P \<and> Q)) = (\<not> P \<or> \<not> Q)"
   "(\<not> (P \<or> Q)) = (\<not> P \<and> \<not> Q)"
   "(P \<longrightarrow> Q) = (\<not> P \<or> Q)"
   "(P = Q) = ((P \<and> Q) \<or> (\<not> P \<and> \<not> Q))"
   "(\<not> (P = Q)) = ((P \<and> \<not> Q) \<or> (\<not> P \<and> Q))"
   "(\<not> \<not> P) = P"
   by blast+
 
 
 subsection \<open>Basic ML bindings\<close>
 
 ML \<open>
 val FalseE = @{thm FalseE}
 val Let_def = @{thm Let_def}
 val TrueI = @{thm TrueI}
 val allE = @{thm allE}
 val allI = @{thm allI}
 val all_dupE = @{thm all_dupE}
 val arg_cong = @{thm arg_cong}
 val box_equals = @{thm box_equals}
 val ccontr = @{thm ccontr}
 val classical = @{thm classical}
 val conjE = @{thm conjE}
 val conjI = @{thm conjI}
 val conjunct1 = @{thm conjunct1}
 val conjunct2 = @{thm conjunct2}
 val disjCI = @{thm disjCI}
 val disjE = @{thm disjE}
 val disjI1 = @{thm disjI1}
 val disjI2 = @{thm disjI2}
 val eq_reflection = @{thm eq_reflection}
 val ex1E = @{thm ex1E}
 val ex1I = @{thm ex1I}
 val ex1_implies_ex = @{thm ex1_implies_ex}
 val exE = @{thm exE}
 val exI = @{thm exI}
 val excluded_middle = @{thm excluded_middle}
 val ext = @{thm ext}
 val fun_cong = @{thm fun_cong}
 val iffD1 = @{thm iffD1}
 val iffD2 = @{thm iffD2}
 val iffI = @{thm iffI}
 val impE = @{thm impE}
 val impI = @{thm impI}
 val meta_eq_to_obj_eq = @{thm meta_eq_to_obj_eq}
 val mp = @{thm mp}
 val notE = @{thm notE}
 val notI = @{thm notI}
 val not_all = @{thm not_all}
 val not_ex = @{thm not_ex}
 val not_iff = @{thm not_iff}
 val not_not = @{thm not_not}
 val not_sym = @{thm not_sym}
 val refl = @{thm refl}
 val rev_mp = @{thm rev_mp}
 val spec = @{thm spec}
 val ssubst = @{thm ssubst}
 val subst = @{thm subst}
 val sym = @{thm sym}
 val trans = @{thm trans}
 \<close>
 
 locale cnf
 begin
 
 lemma clause2raw_notE: "\<lbrakk>P; \<not>P\<rbrakk> \<Longrightarrow> False" by auto
 lemma clause2raw_not_disj: "\<lbrakk>\<not> P; \<not> Q\<rbrakk> \<Longrightarrow> \<not> (P \<or> Q)" by auto
 lemma clause2raw_not_not: "P \<Longrightarrow> \<not>\<not> P" by auto
 
 lemma iff_refl: "(P::bool) = P" by auto
 lemma iff_trans: "[| (P::bool) = Q; Q = R |] ==> P = R" by auto
 lemma conj_cong: "[| P = P'; Q = Q' |] ==> (P \<and> Q) = (P' \<and> Q')" by auto
 lemma disj_cong: "[| P = P'; Q = Q' |] ==> (P \<or> Q) = (P' \<or> Q')" by auto
 
 lemma make_nnf_imp: "[| (\<not>P) = P'; Q = Q' |] ==> (P \<longrightarrow> Q) = (P' \<or> Q')" by auto
 lemma make_nnf_iff: "[| P = P'; (\<not>P) = NP; Q = Q'; (\<not>Q) = NQ |] ==> (P = Q) = ((P' \<or> NQ) \<and> (NP \<or> Q'))" by auto
 lemma make_nnf_not_false: "(\<not>False) = True" by auto
 lemma make_nnf_not_true: "(\<not>True) = False" by auto
 lemma make_nnf_not_conj: "[| (\<not>P) = P'; (\<not>Q) = Q' |] ==> (\<not>(P \<and> Q)) = (P' \<or> Q')" by auto
 lemma make_nnf_not_disj: "[| (\<not>P) = P'; (\<not>Q) = Q' |] ==> (\<not>(P \<or> Q)) = (P' \<and> Q')" by auto
 lemma make_nnf_not_imp: "[| P = P'; (\<not>Q) = Q' |] ==> (\<not>(P \<longrightarrow> Q)) = (P' \<and> Q')" by auto
 lemma make_nnf_not_iff: "[| P = P'; (\<not>P) = NP; Q = Q'; (\<not>Q) = NQ |] ==> (\<not>(P = Q)) = ((P' \<or> Q') \<and> (NP \<or> NQ))" by auto
 lemma make_nnf_not_not: "P = P' ==> (\<not>\<not>P) = P'" by auto
 
 lemma simp_TF_conj_True_l: "[| P = True; Q = Q' |] ==> (P \<and> Q) = Q'" by auto
 lemma simp_TF_conj_True_r: "[| P = P'; Q = True |] ==> (P \<and> Q) = P'" by auto
 lemma simp_TF_conj_False_l: "P = False ==> (P \<and> Q) = False" by auto
 lemma simp_TF_conj_False_r: "Q = False ==> (P \<and> Q) = False" by auto
 lemma simp_TF_disj_True_l: "P = True ==> (P \<or> Q) = True" by auto
 lemma simp_TF_disj_True_r: "Q = True ==> (P \<or> Q) = True" by auto
 lemma simp_TF_disj_False_l: "[| P = False; Q = Q' |] ==> (P \<or> Q) = Q'" by auto
 lemma simp_TF_disj_False_r: "[| P = P'; Q = False |] ==> (P \<or> Q) = P'" by auto
 
 lemma make_cnf_disj_conj_l: "[| (P \<or> R) = PR; (Q \<or> R) = QR |] ==> ((P \<and> Q) \<or> R) = (PR \<and> QR)" by auto
 lemma make_cnf_disj_conj_r: "[| (P \<or> Q) = PQ; (P \<or> R) = PR |] ==> (P \<or> (Q \<and> R)) = (PQ \<and> PR)" by auto
 
 lemma make_cnfx_disj_ex_l: "((\<exists>(x::bool). P x) \<or> Q) = (\<exists>x. P x \<or> Q)" by auto
 lemma make_cnfx_disj_ex_r: "(P \<or> (\<exists>(x::bool). Q x)) = (\<exists>x. P \<or> Q x)" by auto
 lemma make_cnfx_newlit: "(P \<or> Q) = (\<exists>x. (P \<or> x) \<and> (Q \<or> \<not>x))" by auto
 lemma make_cnfx_ex_cong: "(\<forall>(x::bool). P x = Q x) \<Longrightarrow> (\<exists>x. P x) = (\<exists>x. Q x)" by auto
 
 lemma weakening_thm: "[| P; Q |] ==> Q" by auto
 
 lemma cnftac_eq_imp: "[| P = Q; P |] ==> Q" by auto
 
 end
 
 ML_file \<open>Tools/cnf.ML\<close>
 
 
 section \<open>\<open>NO_MATCH\<close> simproc\<close>
 
 text \<open>
   The simplification procedure can be used to avoid simplification of terms
   of a certain form.
 \<close>
 
 definition NO_MATCH :: "'a \<Rightarrow> 'b \<Rightarrow> bool"
   where "NO_MATCH pat val \<equiv> True"
 
 lemma NO_MATCH_cong[cong]: "NO_MATCH pat val = NO_MATCH pat val"
   by (rule refl)
 
 declare [[coercion_args NO_MATCH - -]]
 
 simproc_setup NO_MATCH ("NO_MATCH pat val") = \<open>fn _ => fn ctxt => fn ct =>
   let
     val thy = Proof_Context.theory_of ctxt
     val dest_binop = Term.dest_comb #> apfst (Term.dest_comb #> snd)
     val m = Pattern.matches thy (dest_binop (Thm.term_of ct))
   in if m then NONE else SOME @{thm NO_MATCH_def} end
 \<close>
 
 text \<open>
   This setup ensures that a rewrite rule of the form \<^term>\<open>NO_MATCH pat val \<Longrightarrow> t\<close>
   is only applied, if the pattern \<open>pat\<close> does not match the value \<open>val\<close>.
 \<close>
 
 
 text\<open>
   Tagging a premise of a simp rule with ASSUMPTION forces the simplifier
   not to simplify the argument and to solve it by an assumption.
 \<close>
 
 definition ASSUMPTION :: "bool \<Rightarrow> bool"
   where "ASSUMPTION A \<equiv> A"
 
 lemma ASSUMPTION_cong[cong]: "ASSUMPTION A = ASSUMPTION A"
   by (rule refl)
 
 lemma ASSUMPTION_I: "A \<Longrightarrow> ASSUMPTION A"
   by (simp add: ASSUMPTION_def)
 
 lemma ASSUMPTION_D: "ASSUMPTION A \<Longrightarrow> A"
   by (simp add: ASSUMPTION_def)
 
 setup \<open>
 let
   val asm_sol = mk_solver "ASSUMPTION" (fn ctxt =>
     resolve_tac ctxt [@{thm ASSUMPTION_I}] THEN'
     resolve_tac ctxt (Simplifier.prems_of ctxt))
 in
   map_theory_simpset (fn ctxt => Simplifier.addSolver (ctxt,asm_sol))
 end
 \<close>
 
 
 subsection \<open>Code generator setup\<close>
 
 subsubsection \<open>Generic code generator preprocessor setup\<close>
 
 lemma conj_left_cong: "P \<longleftrightarrow> Q \<Longrightarrow> P \<and> R \<longleftrightarrow> Q \<and> R"
   by (fact arg_cong)
 
 lemma disj_left_cong: "P \<longleftrightarrow> Q \<Longrightarrow> P \<or> R \<longleftrightarrow> Q \<or> R"
   by (fact arg_cong)
 
 setup \<open>
   Code_Preproc.map_pre (put_simpset HOL_basic_ss) #>
   Code_Preproc.map_post (put_simpset HOL_basic_ss) #>
   Code_Simp.map_ss (put_simpset HOL_basic_ss #>
   Simplifier.add_cong @{thm conj_left_cong} #>
   Simplifier.add_cong @{thm disj_left_cong})
 \<close>
 
 
 subsubsection \<open>Equality\<close>
 
 class equal =
   fixes equal :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
   assumes equal_eq: "equal x y \<longleftrightarrow> x = y"
 begin
 
 lemma equal: "equal = (=)"
   by (rule ext equal_eq)+
 
 lemma equal_refl: "equal x x \<longleftrightarrow> True"
   unfolding equal by rule+
 
 lemma eq_equal: "(=) \<equiv> equal"
   by (rule eq_reflection) (rule ext, rule ext, rule sym, rule equal_eq)
 
 end
 
 declare eq_equal [symmetric, code_post]
 declare eq_equal [code]
 
 setup \<open>
   Code_Preproc.map_pre (fn ctxt =>
     ctxt addsimprocs
       [Simplifier.make_simproc \<^context> "equal"
         {lhss = [\<^term>\<open>HOL.eq\<close>],
          proc = fn _ => fn _ => fn ct =>
           (case Thm.term_of ct of
             Const (_, Type (\<^type_name>\<open>fun\<close>, [Type _, _])) => SOME @{thm eq_equal}
           | _ => NONE)}])
 \<close>
 
 
 subsubsection \<open>Generic code generator foundation\<close>
 
 text \<open>Datatype \<^typ>\<open>bool\<close>\<close>
 
 code_datatype True False
 
 lemma [code]:
   shows "False \<and> P \<longleftrightarrow> False"
     and "True \<and> P \<longleftrightarrow> P"
     and "P \<and> False \<longleftrightarrow> False"
     and "P \<and> True \<longleftrightarrow> P"
   by simp_all
 
 lemma [code]:
   shows "False \<or> P \<longleftrightarrow> P"
     and "True \<or> P \<longleftrightarrow> True"
     and "P \<or> False \<longleftrightarrow> P"
     and "P \<or> True \<longleftrightarrow> True"
   by simp_all
 
 lemma [code]:
   shows "(False \<longrightarrow> P) \<longleftrightarrow> True"
     and "(True \<longrightarrow> P) \<longleftrightarrow> P"
     and "(P \<longrightarrow> False) \<longleftrightarrow> \<not> P"
     and "(P \<longrightarrow> True) \<longleftrightarrow> True"
   by simp_all
 
 text \<open>More about \<^typ>\<open>prop\<close>\<close>
 
 lemma [code nbe]:
   shows "(True \<Longrightarrow> PROP Q) \<equiv> PROP Q"
     and "(PROP Q \<Longrightarrow> True) \<equiv> Trueprop True"
     and "(P \<Longrightarrow> R) \<equiv> Trueprop (P \<longrightarrow> R)"
   by (auto intro!: equal_intr_rule)
 
 lemma Trueprop_code [code]: "Trueprop True \<equiv> Code_Generator.holds"
   by (auto intro!: equal_intr_rule holds)
 
 declare Trueprop_code [symmetric, code_post]
 
 text \<open>Equality\<close>
 
 declare simp_thms(6) [code nbe]
 
 instantiation itself :: (type) equal
 begin
 
 definition equal_itself :: "'a itself \<Rightarrow> 'a itself \<Rightarrow> bool"
   where "equal_itself x y \<longleftrightarrow> x = y"
 
 instance
   by standard (fact equal_itself_def)
 
 end
 
 lemma equal_itself_code [code]: "equal TYPE('a) TYPE('a) \<longleftrightarrow> True"
   by (simp add: equal)
 
 setup \<open>Sign.add_const_constraint (\<^const_name>\<open>equal\<close>, SOME \<^typ>\<open>'a::type \<Rightarrow> 'a \<Rightarrow> bool\<close>)\<close>
 
 lemma equal_alias_cert: "OFCLASS('a, equal_class) \<equiv> (((=) :: 'a \<Rightarrow> 'a \<Rightarrow> bool) \<equiv> equal)"
   (is "?ofclass \<equiv> ?equal")
 proof
   assume "PROP ?ofclass"
   show "PROP ?equal"
     by (tactic \<open>ALLGOALS (resolve_tac \<^context> [Thm.unconstrainT @{thm eq_equal}])\<close>)
       (fact \<open>PROP ?ofclass\<close>)
 next
   assume "PROP ?equal"
   show "PROP ?ofclass" proof
   qed (simp add: \<open>PROP ?equal\<close>)
 qed
 
 setup \<open>Sign.add_const_constraint (\<^const_name>\<open>equal\<close>, SOME \<^typ>\<open>'a::equal \<Rightarrow> 'a \<Rightarrow> bool\<close>)\<close>
 
 setup \<open>Nbe.add_const_alias @{thm equal_alias_cert}\<close>
 
 text \<open>Cases\<close>
 
 lemma Let_case_cert:
   assumes "CASE \<equiv> (\<lambda>x. Let x f)"
   shows "CASE x \<equiv> f x"
   using assms by simp_all
 
 setup \<open>
   Code.declare_case_global @{thm Let_case_cert} #>
   Code.declare_undefined_global \<^const_name>\<open>undefined\<close>
 \<close>
 
 declare [[code abort: undefined]]
 
 
 subsubsection \<open>Generic code generator target languages\<close>
 
 text \<open>type \<^typ>\<open>bool\<close>\<close>
 
 code_printing
   type_constructor bool \<rightharpoonup>
     (SML) "bool" and (OCaml) "bool" and (Haskell) "Bool" and (Scala) "Boolean"
 | constant True \<rightharpoonup>
     (SML) "true" and (OCaml) "true" and (Haskell) "True" and (Scala) "true"
 | constant False \<rightharpoonup>
     (SML) "false" and (OCaml) "false" and (Haskell) "False" and (Scala) "false"
 
 code_reserved SML
   bool true false
 
 code_reserved OCaml
   bool
 
 code_reserved Scala
   Boolean
 
 code_printing
   constant Not \<rightharpoonup>
     (SML) "not" and (OCaml) "not" and (Haskell) "not" and (Scala) "'! _"
 | constant HOL.conj \<rightharpoonup>
     (SML) infixl 1 "andalso" and (OCaml) infixl 3 "&&" and (Haskell) infixr 3 "&&" and (Scala) infixl 3 "&&"
 | constant HOL.disj \<rightharpoonup>
     (SML) infixl 0 "orelse" and (OCaml) infixl 2 "||" and (Haskell) infixl 2 "||" and (Scala) infixl 1 "||"
 | constant HOL.implies \<rightharpoonup>
     (SML) "!(if (_)/ then (_)/ else true)"
     and (OCaml) "!(if (_)/ then (_)/ else true)"
     and (Haskell) "!(if (_)/ then (_)/ else True)"
     and (Scala) "!(if ((_))/ (_)/ else true)"
 | constant If \<rightharpoonup>
     (SML) "!(if (_)/ then (_)/ else (_))"
     and (OCaml) "!(if (_)/ then (_)/ else (_))"
     and (Haskell) "!(if (_)/ then (_)/ else (_))"
     and (Scala) "!(if ((_))/ (_)/ else (_))"
 
 code_reserved SML
   not
 
 code_reserved OCaml
   not
 
 code_identifier
   code_module Pure \<rightharpoonup>
     (SML) HOL and (OCaml) HOL and (Haskell) HOL and (Scala) HOL
 
 text \<open>Using built-in Haskell equality.\<close>
 code_printing
   type_class equal \<rightharpoonup> (Haskell) "Eq"
 | constant HOL.equal \<rightharpoonup> (Haskell) infix 4 "=="
 | constant HOL.eq \<rightharpoonup> (Haskell) infix 4 "=="
 
 text \<open>\<open>undefined\<close>\<close>
 code_printing
   constant undefined \<rightharpoonup>
     (SML) "!(raise/ Fail/ \"undefined\")"
     and (OCaml) "failwith/ \"undefined\""
     and (Haskell) "error/ \"undefined\""
     and (Scala) "!sys.error(\"undefined\")"
 
 
 subsubsection \<open>Evaluation and normalization by evaluation\<close>
 
 method_setup eval = \<open>
   let
     fun eval_tac ctxt =
       let val conv = Code_Runtime.dynamic_holds_conv ctxt
       in
         CONVERSION (Conv.params_conv ~1 (K (Conv.concl_conv ~1 conv)) ctxt) THEN'
         resolve_tac ctxt [TrueI]
       end
   in
     Scan.succeed (SIMPLE_METHOD' o eval_tac)
   end
 \<close> "solve goal by evaluation"
 
 method_setup normalization = \<open>
   Scan.succeed (fn ctxt =>
     SIMPLE_METHOD'
       (CHANGED_PROP o
         (CONVERSION (Nbe.dynamic_conv ctxt)
           THEN_ALL_NEW (TRY o resolve_tac ctxt [TrueI]))))
 \<close> "solve goal by normalization"
 
 
 subsection \<open>Counterexample Search Units\<close>
 
 subsubsection \<open>Quickcheck\<close>
 
 quickcheck_params [size = 5, iterations = 50]
 
 
 subsubsection \<open>Nitpick setup\<close>
 
 named_theorems nitpick_unfold "alternative definitions of constants as needed by Nitpick"
   and nitpick_simp "equational specification of constants as needed by Nitpick"
   and nitpick_psimp "partial equational specification of constants as needed by Nitpick"
   and nitpick_choice_spec "choice specification of constants as needed by Nitpick"
 
 declare if_bool_eq_conj [nitpick_unfold, no_atp]
   and if_bool_eq_disj [no_atp]
 
 
 subsection \<open>Preprocessing for the predicate compiler\<close>
 
 named_theorems code_pred_def "alternative definitions of constants for the Predicate Compiler"
   and code_pred_inline "inlining definitions for the Predicate Compiler"
   and code_pred_simp "simplification rules for the optimisations in the Predicate Compiler"
 
 
 subsection \<open>Legacy tactics and ML bindings\<close>
 
 ML \<open>
   (* combination of (spec RS spec RS ...(j times) ... spec RS mp) *)
   local
     fun wrong_prem (Const (\<^const_name>\<open>All\<close>, _) $ Abs (_, _, t)) = wrong_prem t
       | wrong_prem (Bound _) = true
       | wrong_prem _ = false;
     val filter_right = filter (not o wrong_prem o HOLogic.dest_Trueprop o hd o Thm.prems_of);
     fun smp i = funpow i (fn m => filter_right ([spec] RL m)) [mp];
   in
     fun smp_tac ctxt j = EVERY' [dresolve_tac ctxt (smp j), assume_tac ctxt];
   end;
 
   local
     val nnf_ss =
       simpset_of (put_simpset HOL_basic_ss \<^context> addsimps @{thms simp_thms nnf_simps});
   in
     fun nnf_conv ctxt = Simplifier.rewrite (put_simpset nnf_ss ctxt);
   end
 \<close>
 
 hide_const (open) eq equal
 
 end