src/HOL/Inductive.thy
 changeset 31949 3f933687fae9 parent 31784 bd3486c57ba3 child 32587 caa5ada96a00
1.1 --- a/src/HOL/Inductive.thy	Sat Jul 04 23:25:28 2009 +0200
1.2 +++ b/src/HOL/Inductive.thy	Mon Jul 06 14:19:13 2009 +0200
1.3 @@ -258,38 +258,6 @@
1.5  subsection {* Inductive predicates and sets *}
1.7 -text {* Inversion of injective functions. *}
1.8 -
1.9 -constdefs
1.10 -  myinv :: "('a => 'b) => ('b => 'a)"
1.11 -  "myinv (f :: 'a => 'b) == \<lambda>y. THE x. f x = y"
1.12 -
1.13 -lemma myinv_f_f: "inj f ==> myinv f (f x) = x"
1.14 -proof -
1.15 -  assume "inj f"
1.16 -  hence "(THE x'. f x' = f x) = (THE x'. x' = x)"
1.17 -    by (simp only: inj_eq)
1.18 -  also have "... = x" by (rule the_eq_trivial)
1.19 -  finally show ?thesis by (unfold myinv_def)
1.20 -qed
1.21 -
1.22 -lemma f_myinv_f: "inj f ==> y \<in> range f ==> f (myinv f y) = y"
1.23 -proof (unfold myinv_def)
1.24 -  assume inj: "inj f"
1.25 -  assume "y \<in> range f"
1.26 -  then obtain x where "y = f x" ..
1.27 -  hence x: "f x = y" ..
1.28 -  thus "f (THE x. f x = y) = y"
1.29 -  proof (rule theI)
1.30 -    fix x' assume "f x' = y"
1.31 -    with x have "f x' = f x" by simp
1.32 -    with inj show "x' = x" by (rule injD)
1.33 -  qed
1.34 -qed
1.35 -
1.36 -hide const myinv
1.37 -
1.38 -
1.39  text {* Package setup. *}
1.41  theorems basic_monos =