summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Fun.thy

changeset 31949 | 3f933687fae9 |

parent 31775 | 2b04504fcb69 |

child 32139 | e271a64f03ff |

1.1 --- a/src/HOL/Fun.thy Sat Jul 04 23:25:28 2009 +0200 1.2 +++ b/src/HOL/Fun.thy Mon Jul 06 14:19:13 2009 +0200 1.3 @@ -496,6 +496,40 @@ 1.4 1.5 hide (open) const swap 1.6 1.7 + 1.8 +subsection {* Inversion of injective functions *} 1.9 + 1.10 +definition inv :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a)" where 1.11 + "inv f y = (THE x. f x = y)" 1.12 + 1.13 +lemma inv_f_f: 1.14 + assumes "inj f" 1.15 + shows "inv f (f x) = x" 1.16 +proof - 1.17 + from assms have "(THE x'. f x' = f x) = (THE x'. x' = x)" 1.18 + by (simp only: inj_eq) 1.19 + also have "... = x" by (rule the_eq_trivial) 1.20 + finally show ?thesis by (unfold inv_def) 1.21 +qed 1.22 + 1.23 +lemma f_inv_f: 1.24 + assumes "inj f" 1.25 + and "y \<in> range f" 1.26 + shows "f (inv f y) = y" 1.27 +proof (unfold inv_def) 1.28 + from `y \<in> range f` obtain x where "y = f x" .. 1.29 + then have "f x = y" .. 1.30 + then show "f (THE x. f x = y) = y" 1.31 + proof (rule theI) 1.32 + fix x' assume "f x' = y" 1.33 + with `f x = y` have "f x' = f x" by simp 1.34 + with `inj f` show "x' = x" by (rule injD) 1.35 + qed 1.36 +qed 1.37 + 1.38 +hide (open) const inv 1.39 + 1.40 + 1.41 subsection {* Proof tool setup *} 1.42 1.43 text {* simplifies terms of the form