src/HOL/Hilbert_Choice.thy

 (*  Title:      HOL/Hilbert_Choice.thy
     Author:     Lawrence C Paulson, Tobias Nipkow
     Copyright   2001  University of Cambridge
 *)
 
-section {* Hilbert's Epsilon-Operator and the Axiom of Choice *}
+section \<open>Hilbert's Epsilon-Operator and the Axiom of Choice\<close>
 
 theory Hilbert_Choice
 imports Nat Wellfounded
 keywords "specification" :: thy_goal
 begin
 
-subsection {* Hilbert's epsilon *}
+subsection \<open>Hilbert's epsilon\<close>
 
 axiomatization Eps :: "('a => bool) => 'a" where
   someI: "P x ==> P (Eps P)"
 
 syntax (epsilon)

 syntax
   "_Eps"        :: "[pttrn, bool] => 'a"    ("(3SOME _./ _)" [0, 10] 10)
 translations
   "SOME x. P" == "CONST Eps (%x. P)"
 
-print_translation {*
+print_translation \<open>
   [(@{const_syntax Eps}, fn _ => fn [Abs abs] =>
       let val (x, t) = Syntax_Trans.atomic_abs_tr' abs
       in Syntax.const @{syntax_const "_Eps"} $ x $ t end)]
-*} -- {* to avoid eta-contraction of body *}
+\<close> -- \<open>to avoid eta-contraction of body\<close>
 
 definition inv_into :: "'a set => ('a => 'b) => ('b => 'a)" where
 "inv_into A f == %x. SOME y. y : A & f y = x"
 
 abbreviation inv :: "('a => 'b) => ('b => 'a)" where
 "inv == inv_into UNIV"
 
 
-subsection {*Hilbert's Epsilon-operator*}
-
-text{*Easier to apply than @{text someI} if the witness comes from an
-existential formula*}
+subsection \<open>Hilbert's Epsilon-operator\<close>
+
+text\<open>Easier to apply than @{text someI} if the witness comes from an
+existential formula\<close>
 lemma someI_ex [elim?]: "\<exists>x. P x ==> P (SOME x. P x)"
 apply (erule exE)
 apply (erule someI)
 done
 
-text{*Easier to apply than @{text someI} because the conclusion has only one
-occurrence of @{term P}.*}
+text\<open>Easier to apply than @{text someI} because the conclusion has only one
+occurrence of @{term P}.\<close>
 lemma someI2: "[| P a;  !!x. P x ==> Q x |] ==> Q (SOME x. P x)"
 by (blast intro: someI)
 
-text{*Easier to apply than @{text someI2} if the witness comes from an
-existential formula*}
+text\<open>Easier to apply than @{text someI2} if the witness comes from an
+existential formula\<close>
 lemma someI2_ex: "[| \<exists>a. P a; !!x. P x ==> Q x |] ==> Q (SOME x. P x)"
 by (blast intro: someI2)
 
 lemma some_equality [intro]:
      "[| P a;  !!x. P x ==> x=a |] ==> (SOME x. P x) = a"

 apply (rule refl)
 apply (erule sym)
 done
 
 
-subsection{*Axiom of Choice, Proved Using the Description Operator*}
+subsection\<open>Axiom of Choice, Proved Using the Description Operator\<close>
 
 lemma choice: "\<forall>x. \<exists>y. Q x y ==> \<exists>f. \<forall>x. Q x (f x)"
 by (fast elim: someI)
 
 lemma bchoice: "\<forall>x\<in>S. \<exists>y. Q x y ==> \<exists>f. \<forall>x\<in>S. Q x (f x)"

   then show "P n (f n)" "Q n (f n) (f (Suc n))"
     by (induct n) auto
 qed
 
 
-subsection {*Function Inverse*}
+subsection \<open>Function Inverse\<close>
 
 lemma inv_def: "inv f = (%y. SOME x. f x = y)"
 by(simp add: inv_into_def)
 
 lemma inv_into_into: "x : f ` A ==> inv_into A f x : A"

 by (simp add:inv_into_f_eq)
 
 lemma inj_imp_inv_eq: "[| inj f; ALL x. f(g x) = x |] ==> inv f = g"
   by (blast intro: inv_into_f_eq)
 
-text{*But is it useful?*}
+text\<open>But is it useful?\<close>
 lemma inj_transfer:
   assumes injf: "inj f" and minor: "!!y. y \<in> range(f) ==> P(inv f y)"
   shows "P x"
 proof -
   have "f x \<in> range f" by auto

     thus "x \<in> range (\<lambda>f\<Colon>'a \<Rightarrow> 'b. inv f b1)" by blast
   qed
   ultimately show "finite (UNIV :: 'a set)" by simp
 qed
 
-text {*
+text \<open>
   Every infinite set contains a countable subset. More precisely we
   show that a set @{text S} is infinite if and only if there exists an
   injective function from the naturals into @{text S}.
 
   The ``only if'' direction is harder because it requires the
   construction of a sequence of pairwise different elements of an
   infinite set @{text S}. The idea is to construct a sequence of
   non-empty and infinite subsets of @{text S} obtained by successively
   removing elements of @{text S}.
-*}
+\<close>
 
 lemma infinite_countable_subset:
   assumes inf: "\<not> finite (S::'a set)"
   shows "\<exists>f. inj (f::nat \<Rightarrow> 'a) \<and> range f \<subseteq> S"
-  -- {* Courtesy of Stephan Merz *}
+  -- \<open>Courtesy of Stephan Merz\<close>
 proof -
   def Sseq \<equiv> "rec_nat S (\<lambda>n T. T - {SOME e. e \<in> T})"
   def pick \<equiv> "\<lambda>n. (SOME e. e \<in> Sseq n)"
   { fix n have "Sseq n \<subseteq> S" "\<not> finite (Sseq n)" by (induct n) (auto simp add: Sseq_def inf) }
   moreover then have *: "\<And>n. pick n \<in> Sseq n"

   then have "inj pick" by (intro linorder_injI) (auto simp add: less_iff_Suc_add)
   ultimately show ?thesis by blast
 qed
 
 lemma infinite_iff_countable_subset: "\<not> finite S \<longleftrightarrow> (\<exists>f. inj (f::nat \<Rightarrow> 'a) \<and> range f \<subseteq> S)"
-  -- {* Courtesy of Stephan Merz *}
+  -- \<open>Courtesy of Stephan Merz\<close>
   using finite_imageD finite_subset infinite_UNIV_char_0 infinite_countable_subset by auto
 
 lemma image_inv_into_cancel:
   assumes SURJ: "f`A=A'" and SUB: "B' \<le> A'"
   shows "f `((inv_into A f)`B') = B'"

 proof -
   let ?f' = "inv_into A f"   let ?f'' = "inv_into A' ?f'"
   have 1: "bij_betw ?f' A' A" using assms
   by (auto simp add: bij_betw_inv_into)
   obtain a' where 2: "a' \<in> A'" and 3: "?f' a' = a"
-    using 1 `a \<in> A` unfolding bij_betw_def by force
+    using 1 \<open>a \<in> A\<close> unfolding bij_betw_def by force
   hence "?f'' a = a'"
-    using `a \<in> A` 1 3 by (auto simp add: f_inv_into_f bij_betw_def)
+    using \<open>a \<in> A\<close> 1 3 by (auto simp add: f_inv_into_f bij_betw_def)
   moreover have "f a = a'" using assms 2 3
     by (auto simp add: bij_betw_def)
   ultimately show "?f'' a = f a" by simp
 qed
 

     and gf: "g \<circ> f = id"
   shows "inv f = g"
   using fg gf inv_equality[of g f] by (auto simp add: fun_eq_iff)
 
 
-subsection {* The Cantor-Bernstein Theorem *}
+subsection \<open>The Cantor-Bernstein Theorem\<close>
 
 lemma Cantor_Bernstein_aux:
   shows "\<exists>A' h. A' \<le> A \<and>
                 (\<forall>a \<in> A'. a \<notin> g`(B - f ` A')) \<and>
                 (\<forall>a \<in> A'. h a = f a) \<and>

   qed
   (*  *)
   ultimately show ?thesis unfolding bij_betw_def by auto
 qed
 
-subsection {*Other Consequences of Hilbert's Epsilon*}
-
-text {*Hilbert's Epsilon and the @{term split} Operator*}
-
-text{*Looping simprule*}
+subsection \<open>Other Consequences of Hilbert's Epsilon\<close>
+
+text \<open>Hilbert's Epsilon and the @{term split} Operator\<close>
+
+text\<open>Looping simprule\<close>
 lemma split_paired_Eps: "(SOME x. P x) = (SOME (a,b). P(a,b))"
   by simp
 
 lemma Eps_split: "Eps (split P) = (SOME xy. P (fst xy) (snd xy))"
   by (simp add: split_def)
 
 lemma Eps_split_eq [simp]: "(@(x',y'). x = x' & y = y') = (x,y)"
   by blast
 
 
-text{*A relation is wellfounded iff it has no infinite descending chain*}
+text\<open>A relation is wellfounded iff it has no infinite descending chain\<close>
 lemma wf_iff_no_infinite_down_chain:
   "wf r = (~(\<exists>f. \<forall>i. (f(Suc i),f i) \<in> r))"
 apply (simp only: wf_eq_minimal)
 apply (rule iffI)
  apply (rule notI)

 apply (rule someI2_ex, blast+)
 done
 
 lemma wf_no_infinite_down_chainE:
   assumes "wf r" obtains k where "(f (Suc k), f k) \<notin> r"
-using `wf r` wf_iff_no_infinite_down_chain[of r] by blast
-
-
-text{*A dynamically-scoped fact for TFL *}
+using \<open>wf r\<close> wf_iff_no_infinite_down_chain[of r] by blast
+
+
+text\<open>A dynamically-scoped fact for TFL\<close>
 lemma tfl_some: "\<forall>P x. P x --> P (Eps P)"
   by (blast intro: someI)
 
 
-subsection {* Least value operator *}
+subsection \<open>Least value operator\<close>
 
 definition
   LeastM :: "['a => 'b::ord, 'a => bool] => 'a" where
   "LeastM m P == SOME x. P x & (\<forall>y. P y --> m x <= m y)"
 

 
 lemma LeastM_nat_le: "P x ==> m (LeastM m P) <= (m x::nat)"
 by (rule LeastM_nat_lemma [THEN conjunct2, THEN spec, THEN mp], assumption, assumption)
 
 
-subsection {* Greatest value operator *}
+subsection \<open>Greatest value operator\<close>
 
 definition
   GreatestM :: "['a => 'b::ord, 'a => bool] => 'a" where
   "GreatestM m P == SOME x. P x & (\<forall>y. P y --> m y <= m x)"
 

     ==> (m x::nat) <= m (GreatestM m P)"
   apply (blast dest: GreatestM_nat_lemma [THEN conjunct2, THEN spec, of P])
   done
 
 
-text {* \medskip Specialization to @{text GREATEST}. *}
+text \<open>\medskip Specialization to @{text GREATEST}.\<close>
 
 lemma GreatestI: "P (k::nat) ==> \<forall>y. P y --> y < b ==> P (GREATEST x. P x)"
   apply (simp add: Greatest_def)
   apply (rule GreatestM_natI, auto)
   done

   apply (simp add: Greatest_def)
   apply (rule GreatestM_nat_le, auto)
   done
 
 
-subsection {* An aside: bounded accessible part *}
-
-text {* Finite monotone eventually stable sequences *}
+subsection \<open>An aside: bounded accessible part\<close>
+
+text \<open>Finite monotone eventually stable sequences\<close>
 
 lemma finite_mono_remains_stable_implies_strict_prefix:
   fixes f :: "nat \<Rightarrow> 'a::order"
   assumes S: "finite (range f)" "mono f" and eq: "\<forall>n. f n = f (Suc n) \<longrightarrow> f (Suc n) = f (Suc (Suc n))"
   shows "\<exists>N. (\<forall>n\<le>N. \<forall>m\<le>N. m < n \<longrightarrow> f m < f n) \<and> (\<forall>n\<ge>N. f N = f n)"

   have "\<exists>n. f n = f (Suc n)"
   proof (rule ccontr)
     assume "\<not> ?thesis"
     then have "\<And>n. f n \<noteq> f (Suc n)" by auto
     then have "\<And>n. f n < f (Suc n)"
-      using  `mono f` by (auto simp: le_less mono_iff_le_Suc)
+      using  \<open>mono f\<close> by (auto simp: le_less mono_iff_le_Suc)
     with lift_Suc_mono_less_iff[of f]
     have *: "\<And>n m. n < m \<Longrightarrow> f n < f m" by auto
     have "inj f"
     proof (intro injI)
       fix x y
       assume "f x = f y"
       then show "x = y" by (cases x y rule: linorder_cases) (auto dest: *)
     qed
-    with `finite (range f)` have "finite (UNIV::nat set)"
+    with \<open>finite (range f)\<close> have "finite (UNIV::nat set)"
       by (rule finite_imageD)
     then show False by simp
   qed
   then obtain n where n: "f n = f (Suc n)" ..
   def N \<equiv> "LEAST n. f n = f (Suc n)"

     proof (induct rule: dec_induct)
       case (step n) then show ?case
         using eq[rule_format, of "n - 1"] N
         by (cases n) (auto simp add: le_Suc_eq)
     qed simp
-    from this[of n] `N \<le> n` show "f N = f n" by auto
+    from this[of n] \<open>N \<le> n\<close> show "f N = f n" by auto
   next
     fix n m :: nat assume "m < n" "n \<le> N"
     then show "f m < f n"
     proof (induct rule: less_Suc_induct[consumes 1])
       case (1 i)
       then have "i < N" by simp
       then have "f i \<noteq> f (Suc i)"
         unfolding N_def by (rule not_less_Least)
-      with `mono f` show ?case by (simp add: mono_iff_le_Suc less_le)
+      with \<open>mono f\<close> show ?case by (simp add: mono_iff_le_Suc less_le)
     qed auto
   qed
 qed
 
 lemma finite_mono_strict_prefix_implies_finite_fixpoint:

     apply (auto simp: not_less)
     done
 qed
 
 
-subsection {* More on injections, bijections, and inverses *}
+subsection \<open>More on injections, bijections, and inverses\<close>
 
 lemma infinite_imp_bij_betw:
 assumes INF: "\<not> finite A"
 shows "\<exists>h. bij_betw h A (A - {a})"
 proof(cases "a \<in> A")

 shows "bij_betw (inv_into A f) B' B"
 using assms unfolding bij_betw_def
 by (auto intro: inj_on_inv_into)
 
 
-subsection {* Specification package -- Hilbertized version *}
+subsection \<open>Specification package -- Hilbertized version\<close>
 
 lemma exE_some: "[| Ex P ; c == Eps P |] ==> P c"
   by (simp only: someI_ex)
 
 ML_file "Tools/choice_specification.ML"