src/HOL/Inductive.thy
 changeset 11436 3f74b80d979f parent 11325 a5e0289dd56c child 11439 9aaab1a160a5
equal inserted replaced
11435:bd1a7f53c11b 11436:3f74b80d979f
`    54 lemmas inductive_conj = forall_conj implies_conj conj_curry`
`    54 lemmas inductive_conj = forall_conj implies_conj conj_curry`
`    55 `
`    55 `
`    56 hide const forall implies equal conj`
`    56 hide const forall implies equal conj`
`    57 `
`    57 `
`    58 `
`    58 `
`       `
`    59 (* inversion of injective functions *)`
`       `
`    60 `
`       `
`    61 constdefs`
`       `
`    62   myinv :: "('a => 'b) => ('b => 'a)"`
`       `
`    63   "myinv (f :: 'a => 'b) == \<lambda>y. THE x. f x = y"`
`       `
`    64 `
`       `
`    65 lemma myinv_f_f: "inj f ==> myinv f (f x) = x"`
`       `
`    66 proof -`
`       `
`    67   assume "inj f"`
`       `
`    68   hence "(THE x'. f x' = f x) = (THE x'. x' = x)"`
`       `
`    69     by (simp only: inj_eq)`
`       `
`    70   also have "... = x" by (rule the_eq_trivial)`
`       `
`    71   finally (trans) show ?thesis by (unfold myinv_def)`
`       `
`    72 qed`
`       `
`    73 `
`       `
`    74 lemma f_myinv_f: "inj f ==> y \<in> range f ==> f (myinv f y) = y"`
`       `
`    75 proof (unfold myinv_def)`
`       `
`    76   assume inj: "inj f"`
`       `
`    77   assume "y \<in> range f"`
`       `
`    78   then obtain x where "y = f x" ..`
`       `
`    79   hence x: "f x = y" ..`
`       `
`    80   thus "f (THE x. f x = y) = y"`
`       `
`    81   proof (rule theI)`
`       `
`    82     fix x' assume "f x' = y"`
`       `
`    83     with x have "f x' = f x" by simp`
`       `
`    84     with inj show "x' = x" by (rule injD)`
`       `
`    85   qed`
`       `
`    86 qed`
`       `
`    87 `
`       `
`    88 hide const myinv`
`       `
`    89 `
`       `
`    90 `
`    59 (* setup packages *)`
`    91 (* setup packages *)`
`    60 `
`    92 `
`    61 use "Tools/induct_method.ML"`
`    93 use "Tools/induct_method.ML"`
`    62 setup InductMethod.setup`
`    94 setup InductMethod.setup`
`    63 `
`    95 `