author | wenzelm |

Fri Jul 20 22:00:06 2001 +0200 (2001-07-20) | |

changeset 11436 | 3f74b80d979f |

parent 11435 | bd1a7f53c11b |

child 11437 | 2338bce575ae |

private "myinv" (uses "The" instead of "Eps");

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"