private "myinv" (uses "The" instead of "Eps");
authorwenzelm
Fri Jul 20 22:00:06 2001 +0200 (2001-07-20)
changeset 114363f74b80d979f
parent 11435 bd1a7f53c11b
child 11437 2338bce575ae
private "myinv" (uses "The" instead of "Eps");
src/HOL/Inductive.thy
     1.1 --- a/src/HOL/Inductive.thy	Fri Jul 20 21:59:11 2001 +0200
     1.2 +++ b/src/HOL/Inductive.thy	Fri Jul 20 22:00:06 2001 +0200
     1.3 @@ -56,6 +56,38 @@
     1.4  hide const forall implies equal conj
     1.5  
     1.6  
     1.7 +(* 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 (trans) 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  (* setup packages *)
    1.40  
    1.41  use "Tools/induct_method.ML"