equal
deleted
inserted
replaced
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 |