# HG changeset patch
# User nipkow
# Date 1494758792 -7200
# Node ID 416aa3b00cbea0f179bc6ffec03b60f4c5865e75
# Parent  bdd17b18e10356f7078ff1b1946d06995597bf85
added lemma

diff -r bdd17b18e103 -r 416aa3b00cbe src/HOL/Hilbert_Choice.thy
--- a/src/HOL/Hilbert_Choice.thy	Fri May 12 20:03:50 2017 +0200
+++ b/src/HOL/Hilbert_Choice.thy	Sun May 14 12:46:32 2017 +0200
@@ -30,11 +30,14 @@
       in Syntax.const @{syntax_const "_Eps"} $ x $ t end)]
 \<close> \<comment> \<open>to avoid eta-contraction of body\<close>
 
-definition inv_into :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a)"
-  where "inv_into A f \<equiv> \<lambda>x. SOME y. y \<in> A \<and> f y = x"
+definition inv_into :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a)" where
+"inv_into A f = (\<lambda>x. SOME y. y \<in> A \<and> f y = x)"
 
-abbreviation inv :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a)"
-  where "inv \<equiv> inv_into UNIV"
+lemma inv_into_def2: "inv_into A f x = (SOME y. y \<in> A \<and> f y = x)"
+by(simp add: inv_into_def)
+
+abbreviation inv :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a)" where
+"inv \<equiv> inv_into UNIV"
 
 
 subsection \<open>Hilbert's Epsilon-operator\<close>