src/HOL/Fun.thy
changeset 60758 d8d85a8172b5
parent 60303 00c06f1315d0
child 60929 bb3610d34e2e
     1.1 --- a/src/HOL/Fun.thy	Sat Jul 18 21:44:18 2015 +0200
     1.2 +++ b/src/HOL/Fun.thy	Sat Jul 18 22:58:50 2015 +0200
     1.3 @@ -4,7 +4,7 @@
     1.4      Copyright   1994, 2012
     1.5  *)
     1.6  
     1.7 -section {* Notions about functions *}
     1.8 +section \<open>Notions about functions\<close>
     1.9  
    1.10  theory Fun
    1.11  imports Set
    1.12 @@ -15,14 +15,14 @@
    1.13    "f x = u \<Longrightarrow> (\<And>x. P x \<Longrightarrow> g (f x) = x) \<Longrightarrow> P x \<Longrightarrow> x = g u"
    1.14    by auto
    1.15  
    1.16 -text{*Uniqueness, so NOT the axiom of choice.*}
    1.17 +text\<open>Uniqueness, so NOT the axiom of choice.\<close>
    1.18  lemma uniq_choice: "\<forall>x. \<exists>!y. Q x y \<Longrightarrow> \<exists>f. \<forall>x. Q x (f x)"
    1.19    by (force intro: theI')
    1.20  
    1.21  lemma b_uniq_choice: "\<forall>x\<in>S. \<exists>!y. Q x y \<Longrightarrow> \<exists>f. \<forall>x\<in>S. Q x (f x)"
    1.22    by (force intro: theI')
    1.23  
    1.24 -subsection {* The Identity Function @{text id} *}
    1.25 +subsection \<open>The Identity Function @{text id}\<close>
    1.26  
    1.27  definition id :: "'a \<Rightarrow> 'a" where
    1.28    "id = (\<lambda>x. x)"
    1.29 @@ -40,7 +40,7 @@
    1.30    constant id \<rightharpoonup> (Haskell) "id"
    1.31  
    1.32  
    1.33 -subsection {* The Composition Operator @{text "f \<circ> g"} *}
    1.34 +subsection \<open>The Composition Operator @{text "f \<circ> g"}\<close>
    1.35  
    1.36  definition comp :: "('b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c" (infixl "o" 55) where
    1.37    "f o g = (\<lambda>x. f (g x))"
    1.38 @@ -98,7 +98,7 @@
    1.39    constant comp \<rightharpoonup> (SML) infixl 5 "o" and (Haskell) infixr 9 "."
    1.40  
    1.41  
    1.42 -subsection {* The Forward Composition Operator @{text fcomp} *}
    1.43 +subsection \<open>The Forward Composition Operator @{text fcomp}\<close>
    1.44  
    1.45  definition fcomp :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'c" (infixl "\<circ>>" 60) where
    1.46    "f \<circ>> g = (\<lambda>x. g (f x))"
    1.47 @@ -121,7 +121,7 @@
    1.48  no_notation fcomp (infixl "\<circ>>" 60)
    1.49  
    1.50  
    1.51 -subsection {* Mapping functions *}
    1.52 +subsection \<open>Mapping functions\<close>
    1.53  
    1.54  definition map_fun :: "('c \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'c \<Rightarrow> 'd" where
    1.55    "map_fun f g h = g \<circ> h \<circ> f"
    1.56 @@ -131,7 +131,7 @@
    1.57    by (simp add: map_fun_def)
    1.58  
    1.59  
    1.60 -subsection {* Injectivity and Bijectivity *}
    1.61 +subsection \<open>Injectivity and Bijectivity\<close>
    1.62  
    1.63  definition inj_on :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> bool" where -- "injective"
    1.64    "inj_on f A \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>A. f x = f y \<longrightarrow> x = y)"
    1.65 @@ -139,8 +139,8 @@
    1.66  definition bij_betw :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> bool" where -- "bijective"
    1.67    "bij_betw f A B \<longleftrightarrow> inj_on f A \<and> f ` A = B"
    1.68  
    1.69 -text{*A common special case: functions injective, surjective or bijective over
    1.70 -the entire domain type.*}
    1.71 +text\<open>A common special case: functions injective, surjective or bijective over
    1.72 +the entire domain type.\<close>
    1.73  
    1.74  abbreviation
    1.75    "inj f \<equiv> inj_on f UNIV"
    1.76 @@ -151,7 +151,7 @@
    1.77  abbreviation
    1.78    "bij f \<equiv> bij_betw f UNIV UNIV"
    1.79  
    1.80 -text{* The negated case: *}
    1.81 +text\<open>The negated case:\<close>
    1.82  translations
    1.83  "\<not> CONST surj f" <= "CONST range f \<noteq> CONST UNIV"
    1.84  
    1.85 @@ -278,14 +278,14 @@
    1.86    with assms * have "B = f ` (A - {x'})"
    1.87      by (auto dest: inj_on_contraD)
    1.88    have "x' \<notin> A - {x'}" by simp
    1.89 -  from `x' \<notin> A - {x'}` `A = insert x' (A - {x'})` `x = f x'` `B = image f (A - {x'})`
    1.90 +  from \<open>x' \<notin> A - {x'}\<close> \<open>A = insert x' (A - {x'})\<close> \<open>x = f x'\<close> \<open>B = image f (A - {x'})\<close>
    1.91    show ?thesis ..
    1.92  qed
    1.93  
    1.94  lemma linorder_injI:
    1.95    assumes hyp: "\<And>x y. x < (y::'a::linorder) \<Longrightarrow> f x \<noteq> f y"
    1.96    shows "inj f"
    1.97 -  -- {* Courtesy of Stephan Merz *}
    1.98 +  -- \<open>Courtesy of Stephan Merz\<close>
    1.99  proof (rule inj_onI)
   1.100    fix x y
   1.101    assume f_eq: "f x = f y"
   1.102 @@ -395,9 +395,9 @@
   1.103    have "inj_on ?g B"
   1.104    proof(rule inj_onI)
   1.105      fix x y assume "x:B" "y:B" "?g x = ?g y"
   1.106 -    from s `x:B` obtain a1 where a1: "?P x a1" by blast
   1.107 -    from s `y:B` obtain a2 where a2: "?P y a2" by blast
   1.108 -    from g[OF a1] a1 g[OF a2] a2 `?g x = ?g y` show "x=y" by simp
   1.109 +    from s \<open>x:B\<close> obtain a1 where a1: "?P x a1" by blast
   1.110 +    from s \<open>y:B\<close> obtain a2 where a2: "?P y a2" by blast
   1.111 +    from g[OF a1] a1 g[OF a2] a2 \<open>?g x = ?g y\<close> show "x=y" by simp
   1.112    qed
   1.113    moreover have "?g ` B = A"
   1.114    proof(auto simp: image_def)
   1.115 @@ -453,7 +453,7 @@
   1.116  
   1.117  lemma surj_vimage_empty:
   1.118    assumes "surj f" shows "f -` A = {} \<longleftrightarrow> A = {}"
   1.119 -  using surj_image_vimage_eq[OF `surj f`, of A]
   1.120 +  using surj_image_vimage_eq[OF \<open>surj f\<close>, of A]
   1.121    by (intro iffI) fastforce+
   1.122  
   1.123  lemma inj_vimage_image_eq: "inj f ==> f -` (f ` A) = A"
   1.124 @@ -515,8 +515,8 @@
   1.125  done
   1.126  
   1.127  lemma inj_vimage_singleton: "inj f \<Longrightarrow> f -` {a} \<subseteq> {THE x. f x = a}"
   1.128 -  -- {* The inverse image of a singleton under an injective function
   1.129 -         is included in a singleton. *}
   1.130 +  -- \<open>The inverse image of a singleton under an injective function
   1.131 +         is included in a singleton.\<close>
   1.132    apply (auto simp add: inj_on_def)
   1.133    apply (blast intro: the_equality [symmetric])
   1.134    done
   1.135 @@ -594,7 +594,7 @@
   1.136  qed
   1.137  
   1.138  
   1.139 -subsection{*Function Updating*}
   1.140 +subsection\<open>Function Updating\<close>
   1.141  
   1.142  definition fun_upd :: "('a => 'b) => 'a => 'b => ('a => 'b)" where
   1.143    "fun_upd f a b == % x. if x=a then b else f x"
   1.144 @@ -658,7 +658,7 @@
   1.145    by auto
   1.146  
   1.147  
   1.148 -subsection {* @{text override_on} *}
   1.149 +subsection \<open>@{text override_on}\<close>
   1.150  
   1.151  definition override_on :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'a \<Rightarrow> 'b" where
   1.152    "override_on f g A = (\<lambda>a. if a \<in> A then g a else f a)"
   1.153 @@ -673,7 +673,7 @@
   1.154  by(simp add:override_on_def)
   1.155  
   1.156  
   1.157 -subsection {* @{text swap} *}
   1.158 +subsection \<open>@{text swap}\<close>
   1.159  
   1.160  definition swap :: "'a \<Rightarrow> 'a \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)"
   1.161  where
   1.162 @@ -750,7 +750,7 @@
   1.163  hide_const (open) swap
   1.164  
   1.165  
   1.166 -subsection {* Inversion of injective functions *}
   1.167 +subsection \<open>Inversion of injective functions\<close>
   1.168  
   1.169  definition the_inv_into :: "'a set => ('a => 'b) => ('b => 'a)" where
   1.170    "the_inv_into A f == %x. THE y. y : A & f y = x"
   1.171 @@ -813,7 +813,7 @@
   1.172    by (rule the_inv_into_f_f)
   1.173  
   1.174  
   1.175 -subsection {* Cantor's Paradox *}
   1.176 +subsection \<open>Cantor's Paradox\<close>
   1.177  
   1.178  lemma Cantors_paradox:
   1.179    "\<not>(\<exists>f. f ` A = Pow A)"
   1.180 @@ -825,14 +825,14 @@
   1.181    thus False by best
   1.182  qed
   1.183  
   1.184 -subsection {* Setup *} 
   1.185 +subsection \<open>Setup\<close> 
   1.186  
   1.187 -subsubsection {* Proof tools *}
   1.188 +subsubsection \<open>Proof tools\<close>
   1.189  
   1.190 -text {* simplifies terms of the form
   1.191 -  f(...,x:=y,...,x:=z,...) to f(...,x:=z,...) *}
   1.192 +text \<open>simplifies terms of the form
   1.193 +  f(...,x:=y,...,x:=z,...) to f(...,x:=z,...)\<close>
   1.194  
   1.195 -simproc_setup fun_upd2 ("f(v := w, x := y)") = {* fn _ =>
   1.196 +simproc_setup fun_upd2 ("f(v := w, x := y)") = \<open>fn _ =>
   1.197  let
   1.198    fun gen_fun_upd NONE T _ _ = NONE
   1.199      | gen_fun_upd (SOME f) T x y = SOME (Const (@{const_name fun_upd}, T) $ f $ x $ y)
   1.200 @@ -860,10 +860,10 @@
   1.201                simp_tac (put_simpset ss ctxt) 1))
   1.202      end
   1.203  in proc end
   1.204 -*}
   1.205 +\<close>
   1.206  
   1.207  
   1.208 -subsubsection {* Functorial structure of types *}
   1.209 +subsubsection \<open>Functorial structure of types\<close>
   1.210  
   1.211  ML_file "Tools/functor.ML"
   1.212  
   1.213 @@ -873,7 +873,7 @@
   1.214  functor vimage
   1.215    by (simp_all add: fun_eq_iff vimage_comp)
   1.216  
   1.217 -text {* Legacy theorem names *}
   1.218 +text \<open>Legacy theorem names\<close>
   1.219  
   1.220  lemmas o_def = comp_def
   1.221  lemmas o_apply = comp_apply