src/HOL/Fun.ML
 author paulson Thu Jan 09 10:23:39 1997 +0100 (1997-01-09) changeset 2499 0bc87b063447 parent 2031 03a843f0f447 child 2890 f27002fc531d permissions -rw-r--r--
Tidying of proofs. New theorems are enterred immediately into the
relevant clasets or simpsets.
 clasohm@1465 ` 1` ```(* Title: HOL/Fun ``` clasohm@923 ` 2` ``` ID: \$Id\$ ``` clasohm@1465 ` 3` ``` Author: Tobias Nipkow, Cambridge University Computer Laboratory ``` clasohm@923 ` 4` ``` Copyright 1993 University of Cambridge ``` clasohm@923 ` 5` clasohm@923 ` 6` ```Lemmas about functions. ``` clasohm@923 ` 7` ```*) ``` clasohm@923 ` 8` clasohm@923 ` 9` ```goal Fun.thy "(f = g) = (!x. f(x)=g(x))"; ``` clasohm@923 ` 10` ```by (rtac iffI 1); ``` clasohm@1264 ` 11` ```by (Asm_simp_tac 1); ``` clasohm@1264 ` 12` ```by (rtac ext 1 THEN Asm_simp_tac 1); ``` clasohm@923 ` 13` ```qed "expand_fun_eq"; ``` clasohm@923 ` 14` clasohm@923 ` 15` ```val prems = goal Fun.thy ``` clasohm@923 ` 16` ``` "[| f(x)=u; !!x. P(x) ==> g(f(x)) = x; P(x) |] ==> x=g(u)"; ``` clasohm@923 ` 17` ```by (rtac (arg_cong RS box_equals) 1); ``` clasohm@923 ` 18` ```by (REPEAT (resolve_tac (prems@[refl]) 1)); ``` clasohm@923 ` 19` ```qed "apply_inverse"; ``` clasohm@923 ` 20` clasohm@923 ` 21` paulson@1883 ` 22` ```(*** Image of a set under a function ***) ``` clasohm@923 ` 23` clasohm@923 ` 24` ```(*Frequently b does not have the syntactic form of f(x).*) ``` clasohm@923 ` 25` ```val prems = goalw Fun.thy [image_def] "[| b=f(x); x:A |] ==> b : f``A"; ``` clasohm@923 ` 26` ```by (REPEAT (resolve_tac (prems @ [CollectI,bexI,prem]) 1)); ``` clasohm@923 ` 27` ```qed "image_eqI"; ``` clasohm@923 ` 28` paulson@1883 ` 29` ```bind_thm ("imageI", refl RS image_eqI); ``` clasohm@923 ` 30` clasohm@923 ` 31` ```(*The eta-expansion gives variable-name preservation.*) ``` clasohm@923 ` 32` ```val major::prems = goalw Fun.thy [image_def] ``` clasohm@923 ` 33` ``` "[| b : (%x.f(x))``A; !!x.[| b=f(x); x:A |] ==> P |] ==> P"; ``` clasohm@923 ` 34` ```by (rtac (major RS CollectD RS bexE) 1); ``` clasohm@923 ` 35` ```by (REPEAT (ares_tac prems 1)); ``` clasohm@923 ` 36` ```qed "imageE"; ``` clasohm@923 ` 37` paulson@2499 ` 38` ```AddIs [imageI]; ``` paulson@2499 ` 39` ```AddSEs [imageE]; ``` paulson@2499 ` 40` clasohm@923 ` 41` ```goalw Fun.thy [o_def] "(f o g)``r = f``(g``r)"; ``` paulson@2499 ` 42` ```by (Fast_tac 1); ``` clasohm@923 ` 43` ```qed "image_compose"; ``` clasohm@923 ` 44` clasohm@923 ` 45` ```goal Fun.thy "f``(A Un B) = f``A Un f``B"; ``` paulson@2499 ` 46` ```by (Fast_tac 1); ``` clasohm@923 ` 47` ```qed "image_Un"; ``` clasohm@923 ` 48` paulson@1883 ` 49` ```(*** Range of a function -- just a translation for image! ***) ``` paulson@1883 ` 50` paulson@1883 ` 51` ```goal Fun.thy "!!b. b=f(x) ==> b : range(f)"; ``` paulson@1883 ` 52` ```by (EVERY1 [etac image_eqI, rtac UNIV_I]); ``` paulson@1883 ` 53` ```bind_thm ("range_eqI", UNIV_I RSN (2,image_eqI)); ``` paulson@1883 ` 54` paulson@1883 ` 55` ```bind_thm ("rangeI", UNIV_I RS imageI); ``` paulson@1883 ` 56` paulson@1883 ` 57` ```val [major,minor] = goal Fun.thy ``` paulson@1883 ` 58` ``` "[| b : range(%x.f(x)); !!x. b=f(x) ==> P |] ==> P"; ``` paulson@1883 ` 59` ```by (rtac (major RS imageE) 1); ``` paulson@1883 ` 60` ```by (etac minor 1); ``` paulson@1883 ` 61` ```qed "rangeE"; ``` clasohm@923 ` 62` ```(*** inj(f): f is a one-to-one function ***) ``` clasohm@923 ` 63` clasohm@923 ` 64` ```val prems = goalw Fun.thy [inj_def] ``` clasohm@923 ` 65` ``` "[| !! x y. f(x) = f(y) ==> x=y |] ==> inj(f)"; ``` berghofe@1754 ` 66` ```by (fast_tac (!claset addIs prems) 1); ``` clasohm@923 ` 67` ```qed "injI"; ``` clasohm@923 ` 68` clasohm@923 ` 69` ```val [major] = goal Fun.thy "(!!x. g(f(x)) = x) ==> inj(f)"; ``` clasohm@923 ` 70` ```by (rtac injI 1); ``` clasohm@923 ` 71` ```by (etac (arg_cong RS box_equals) 1); ``` clasohm@923 ` 72` ```by (rtac major 1); ``` clasohm@923 ` 73` ```by (rtac major 1); ``` clasohm@923 ` 74` ```qed "inj_inverseI"; ``` clasohm@923 ` 75` clasohm@923 ` 76` ```val [major,minor] = goalw Fun.thy [inj_def] ``` clasohm@923 ` 77` ``` "[| inj(f); f(x) = f(y) |] ==> x=y"; ``` clasohm@923 ` 78` ```by (rtac (major RS spec RS spec RS mp) 1); ``` clasohm@923 ` 79` ```by (rtac minor 1); ``` clasohm@923 ` 80` ```qed "injD"; ``` clasohm@923 ` 81` clasohm@923 ` 82` ```(*Useful with the simplifier*) ``` clasohm@923 ` 83` ```val [major] = goal Fun.thy "inj(f) ==> (f(x) = f(y)) = (x=y)"; ``` clasohm@923 ` 84` ```by (rtac iffI 1); ``` clasohm@923 ` 85` ```by (etac (major RS injD) 1); ``` clasohm@923 ` 86` ```by (etac arg_cong 1); ``` clasohm@923 ` 87` ```qed "inj_eq"; ``` clasohm@923 ` 88` clasohm@923 ` 89` ```val [major] = goal Fun.thy "inj(f) ==> (@x.f(x)=f(y)) = y"; ``` clasohm@923 ` 90` ```by (rtac (major RS injD) 1); ``` clasohm@923 ` 91` ```by (rtac selectI 1); ``` clasohm@923 ` 92` ```by (rtac refl 1); ``` clasohm@923 ` 93` ```qed "inj_select"; ``` clasohm@923 ` 94` clasohm@923 ` 95` ```(*A one-to-one function has an inverse (given using select).*) ``` clasohm@923 ` 96` ```val [major] = goalw Fun.thy [Inv_def] "inj(f) ==> Inv f (f x) = x"; ``` clasohm@923 ` 97` ```by (EVERY1 [rtac (major RS inj_select)]); ``` clasohm@923 ` 98` ```qed "Inv_f_f"; ``` clasohm@923 ` 99` clasohm@923 ` 100` ```(* Useful??? *) ``` clasohm@923 ` 101` ```val [oneone,minor] = goal Fun.thy ``` clasohm@923 ` 102` ``` "[| inj(f); !!y. y: range(f) ==> P(Inv f y) |] ==> P(x)"; ``` clasohm@923 ` 103` ```by (res_inst_tac [("t", "x")] (oneone RS (Inv_f_f RS subst)) 1); ``` clasohm@923 ` 104` ```by (rtac (rangeI RS minor) 1); ``` clasohm@923 ` 105` ```qed "inj_transfer"; ``` clasohm@923 ` 106` clasohm@923 ` 107` clasohm@923 ` 108` ```(*** inj_onto f A: f is one-to-one over A ***) ``` clasohm@923 ` 109` clasohm@923 ` 110` ```val prems = goalw Fun.thy [inj_onto_def] ``` clasohm@923 ` 111` ``` "(!! x y. [| f(x) = f(y); x:A; y:A |] ==> x=y) ==> inj_onto f A"; ``` paulson@2499 ` 112` ```by (fast_tac (!claset addIs prems) 1); ``` clasohm@923 ` 113` ```qed "inj_ontoI"; ``` clasohm@923 ` 114` clasohm@923 ` 115` ```val [major] = goal Fun.thy ``` clasohm@923 ` 116` ``` "(!!x. x:A ==> g(f(x)) = x) ==> inj_onto f A"; ``` clasohm@923 ` 117` ```by (rtac inj_ontoI 1); ``` clasohm@923 ` 118` ```by (etac (apply_inverse RS trans) 1); ``` clasohm@923 ` 119` ```by (REPEAT (eresolve_tac [asm_rl,major] 1)); ``` clasohm@923 ` 120` ```qed "inj_onto_inverseI"; ``` clasohm@923 ` 121` clasohm@923 ` 122` ```val major::prems = goalw Fun.thy [inj_onto_def] ``` clasohm@923 ` 123` ``` "[| inj_onto f A; f(x)=f(y); x:A; y:A |] ==> x=y"; ``` clasohm@923 ` 124` ```by (rtac (major RS bspec RS bspec RS mp) 1); ``` clasohm@923 ` 125` ```by (REPEAT (resolve_tac prems 1)); ``` clasohm@923 ` 126` ```qed "inj_ontoD"; ``` clasohm@923 ` 127` clasohm@923 ` 128` ```goal Fun.thy "!!x y.[| inj_onto f A; x:A; y:A |] ==> (f(x)=f(y)) = (x=y)"; ``` berghofe@1754 ` 129` ```by (fast_tac (!claset addSEs [inj_ontoD]) 1); ``` clasohm@923 ` 130` ```qed "inj_onto_iff"; ``` clasohm@923 ` 131` clasohm@923 ` 132` ```val major::prems = goal Fun.thy ``` clasohm@923 ` 133` ``` "[| inj_onto f A; ~x=y; x:A; y:A |] ==> ~ f(x)=f(y)"; ``` clasohm@923 ` 134` ```by (rtac contrapos 1); ``` clasohm@923 ` 135` ```by (etac (major RS inj_ontoD) 2); ``` clasohm@923 ` 136` ```by (REPEAT (resolve_tac prems 1)); ``` clasohm@923 ` 137` ```qed "inj_onto_contraD"; ``` clasohm@923 ` 138` clasohm@923 ` 139` clasohm@923 ` 140` ```(*** Lemmas about inj ***) ``` clasohm@923 ` 141` clasohm@923 ` 142` ```val prems = goalw Fun.thy [o_def] ``` clasohm@923 ` 143` ``` "[| inj(f); inj_onto g (range f) |] ==> inj(g o f)"; ``` clasohm@923 ` 144` ```by (cut_facts_tac prems 1); ``` paulson@2499 ` 145` ```by (fast_tac (!claset addIs [injI] ``` clasohm@923 ` 146` ``` addEs [injD,inj_ontoD]) 1); ``` clasohm@923 ` 147` ```qed "comp_inj"; ``` clasohm@923 ` 148` clasohm@923 ` 149` ```val [prem] = goal Fun.thy "inj(f) ==> inj_onto f A"; ``` berghofe@1754 ` 150` ```by (fast_tac (!claset addIs [prem RS injD, inj_ontoI]) 1); ``` clasohm@923 ` 151` ```qed "inj_imp"; ``` clasohm@923 ` 152` clasohm@923 ` 153` ```val [prem] = goalw Fun.thy [Inv_def] "y : range(f) ==> f(Inv f y) = y"; ``` clasohm@923 ` 154` ```by (EVERY1 [rtac (prem RS rangeE), rtac selectI, etac sym]); ``` clasohm@923 ` 155` ```qed "f_Inv_f"; ``` clasohm@923 ` 156` clasohm@923 ` 157` ```val prems = goal Fun.thy ``` clasohm@923 ` 158` ``` "[| Inv f x=Inv f y; x: range(f); y: range(f) |] ==> x=y"; ``` clasohm@923 ` 159` ```by (rtac (arg_cong RS box_equals) 1); ``` clasohm@923 ` 160` ```by (REPEAT (resolve_tac (prems @ [f_Inv_f]) 1)); ``` clasohm@923 ` 161` ```qed "Inv_injective"; ``` clasohm@923 ` 162` clasohm@923 ` 163` ```val prems = goal Fun.thy ``` clasohm@923 ` 164` ``` "[| inj(f); A<=range(f) |] ==> inj_onto (Inv f) A"; ``` clasohm@923 ` 165` ```by (cut_facts_tac prems 1); ``` berghofe@1754 ` 166` ```by (fast_tac (!claset addIs [inj_ontoI] ``` paulson@2499 ` 167` ``` addEs [Inv_injective,injD]) 1); ``` clasohm@923 ` 168` ```qed "inj_onto_Inv"; ``` clasohm@923 ` 169` clasohm@923 ` 170` paulson@2499 ` 171` ```AddIs [rangeI]; ``` paulson@2499 ` 172` ```AddSEs [rangeE]; ``` berghofe@1754 ` 173` paulson@1837 ` 174` ```val set_cs = !claset delrules [equalityI]; ``` clasohm@923 ` 175` paulson@1883 ` 176`