src/HOL/Hilbert_Choice.thy
changeset 65815 416aa3b00cbe
parent 64591 240a39af9ec4
child 65952 dec96cb3fbe0
     1.1 --- a/src/HOL/Hilbert_Choice.thy	Fri May 12 20:03:50 2017 +0200
     1.2 +++ b/src/HOL/Hilbert_Choice.thy	Sun May 14 12:46:32 2017 +0200
     1.3 @@ -30,11 +30,14 @@
     1.4        in Syntax.const @{syntax_const "_Eps"} $ x $ t end)]
     1.5  \<close> \<comment> \<open>to avoid eta-contraction of body\<close>
     1.6  
     1.7 -definition inv_into :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a)"
     1.8 -  where "inv_into A f \<equiv> \<lambda>x. SOME y. y \<in> A \<and> f y = x"
     1.9 +definition inv_into :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a)" where
    1.10 +"inv_into A f = (\<lambda>x. SOME y. y \<in> A \<and> f y = x)"
    1.11  
    1.12 -abbreviation inv :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a)"
    1.13 -  where "inv \<equiv> inv_into UNIV"
    1.14 +lemma inv_into_def2: "inv_into A f x = (SOME y. y \<in> A \<and> f y = x)"
    1.15 +by(simp add: inv_into_def)
    1.16 +
    1.17 +abbreviation inv :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a)" where
    1.18 +"inv \<equiv> inv_into UNIV"
    1.19  
    1.20  
    1.21  subsection \<open>Hilbert's Epsilon-operator\<close>