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.4  
     1.5  subsection {* Inductive predicates and sets *}
     1.6  
     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.40  
    1.41  theorems basic_monos =