src/HOL/Fun.thy
changeset 61799 4cf66f21b764
parent 61699 a81dc5c4d6a9
child 61955 e96292f32c3c
     1.1 --- a/src/HOL/Fun.thy	Mon Dec 07 10:23:50 2015 +0100
     1.2 +++ b/src/HOL/Fun.thy	Mon Dec 07 10:38:04 2015 +0100
     1.3 @@ -22,7 +22,7 @@
     1.4  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.5    by (force intro: theI')
     1.6  
     1.7 -subsection \<open>The Identity Function @{text id}\<close>
     1.8 +subsection \<open>The Identity Function \<open>id\<close>\<close>
     1.9  
    1.10  definition id :: "'a \<Rightarrow> 'a" where
    1.11    "id = (\<lambda>x. x)"
    1.12 @@ -40,7 +40,7 @@
    1.13    constant id \<rightharpoonup> (Haskell) "id"
    1.14  
    1.15  
    1.16 -subsection \<open>The Composition Operator @{text "f \<circ> g"}\<close>
    1.17 +subsection \<open>The Composition Operator \<open>f \<circ> g\<close>\<close>
    1.18  
    1.19  definition comp :: "('b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c" (infixl "o" 55) where
    1.20    "f o g = (\<lambda>x. f (g x))"
    1.21 @@ -103,7 +103,7 @@
    1.22    constant comp \<rightharpoonup> (SML) infixl 5 "o" and (Haskell) infixr 9 "."
    1.23  
    1.24  
    1.25 -subsection \<open>The Forward Composition Operator @{text fcomp}\<close>
    1.26 +subsection \<open>The Forward Composition Operator \<open>fcomp\<close>\<close>
    1.27  
    1.28  definition fcomp :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'c" (infixl "\<circ>>" 60) where
    1.29    "f \<circ>> g = (\<lambda>x. g (f x))"
    1.30 @@ -141,10 +141,10 @@
    1.31  
    1.32  subsection \<open>Injectivity and Bijectivity\<close>
    1.33  
    1.34 -definition inj_on :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> bool" where -- "injective"
    1.35 +definition inj_on :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> bool" where \<comment> "injective"
    1.36    "inj_on f A \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>A. f x = f y \<longrightarrow> x = y)"
    1.37  
    1.38 -definition bij_betw :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> bool" where -- "bijective"
    1.39 +definition bij_betw :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> bool" where \<comment> "bijective"
    1.40    "bij_betw f A B \<longleftrightarrow> inj_on f A \<and> f ` A = B"
    1.41  
    1.42  text\<open>A common special case: functions injective, surjective or bijective over
    1.43 @@ -153,7 +153,7 @@
    1.44  abbreviation
    1.45    "inj f \<equiv> inj_on f UNIV"
    1.46  
    1.47 -abbreviation surj :: "('a \<Rightarrow> 'b) \<Rightarrow> bool" where -- "surjective"
    1.48 +abbreviation surj :: "('a \<Rightarrow> 'b) \<Rightarrow> bool" where \<comment> "surjective"
    1.49    "surj f \<equiv> (range f = UNIV)"
    1.50  
    1.51  abbreviation
    1.52 @@ -290,7 +290,7 @@
    1.53  lemma linorder_injI:
    1.54    assumes hyp: "\<And>x y. x < (y::'a::linorder) \<Longrightarrow> f x \<noteq> f y"
    1.55    shows "inj f"
    1.56 -  -- \<open>Courtesy of Stephan Merz\<close>
    1.57 +  \<comment> \<open>Courtesy of Stephan Merz\<close>
    1.58  proof (rule inj_onI)
    1.59    fix x y
    1.60    assume f_eq: "f x = f y"
    1.61 @@ -524,7 +524,7 @@
    1.62  done
    1.63  
    1.64  lemma inj_vimage_singleton: "inj f \<Longrightarrow> f -` {a} \<subseteq> {THE x. f x = a}"
    1.65 -  -- \<open>The inverse image of a singleton under an injective function
    1.66 +  \<comment> \<open>The inverse image of a singleton under an injective function
    1.67           is included in a singleton.\<close>
    1.68    apply (auto simp add: inj_on_def)
    1.69    apply (blast intro: the_equality [symmetric])
    1.70 @@ -669,7 +669,7 @@
    1.71  lemma fun_upd_eqD: "f(x := y) = g(x := z) \<Longrightarrow> y = z"
    1.72  by(simp add: fun_eq_iff split: split_if_asm)
    1.73  
    1.74 -subsection \<open>@{text override_on}\<close>
    1.75 +subsection \<open>\<open>override_on\<close>\<close>
    1.76  
    1.77  definition override_on :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'a \<Rightarrow> 'b" where
    1.78    "override_on f g A = (\<lambda>a. if a \<in> A then g a else f a)"
    1.79 @@ -684,7 +684,7 @@
    1.80  by(simp add:override_on_def)
    1.81  
    1.82  
    1.83 -subsection \<open>@{text swap}\<close>
    1.84 +subsection \<open>\<open>swap\<close>\<close>
    1.85  
    1.86  definition swap :: "'a \<Rightarrow> 'a \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)"
    1.87  where