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

src/HOL/Inductive.thy

changeset 31949 | 3f933687fae9 |

parent 31784 | bd3486c57ba3 |

child 32587 | caa5ada96a00 |

1.1 --- a/src/HOL/Inductive.thy Sat Jul 04 23:25:28 2009 +0200 1.2 +++ b/src/HOL/Inductive.thy Mon Jul 06 14:19:13 2009 +0200 1.3 @@ -258,38 +258,6 @@ 1.4 1.5 subsection {* Inductive predicates and sets *} 1.6 1.7 -text {* 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 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 text {* Package setup. *} 1.40 1.41 theorems basic_monos =