theory Cas3_vezbe imports Main begin (* ponavljanje sa predavanja *) lemma "f = g \ (\ x. f x = g x)" using [[show_types]] by auto term inj term surj term bij thm inj_def thm surj_def thm bij_def lemma "bij f \ inj f \ surj f" (* by auto --- ne prolazi samo po sebi *) (* jedan nacin: using bij_def by auto *) (* drugi nacin: *) unfolding bij_def (* The command “unfolding facts” operates directly on the goal by applying equalities. *) by auto (* The image of a set under a function *) (* https://en.wikipedia.org/wiki/Image_(mathematics) *) find_theorems "image" thm image_def thm image_Un lemma "f ` (A \ B) = f ` A \ f ` B" by auto find_theorems "_ ` _ \ _ ` _" thm image_Int lemma assumes "inj f" shows "f ` (A \ B) = f ` A \ f ` B" (* by auto nece proci *) (* by (auto simp add: image_Int) isto ne prolazi zato sto dokaz ne vidi pretpostavke *) using assms (* neophodno je dodati pretpostavke *) by (auto simp add: image_Int) (* PRIMERI SA FUNKCIJAMA *) (* ponavljanje sa predavanja *) lemma "f ` (A \ B) = f ` A \ f ` B" proof show "f ` (A \ B) \ f ` A \ f ` B" proof fix y (* zato sto odgovara slici *) assume "y \ f ` (A \ B)" thm image_def then have "\ x. x \ A \ B \ f x = y" by auto (* po definiciji f ` *) then obtain x where "x \ A \ B" "f x = y" by auto then have "x \ A \ x \ B" by auto then show "y \ f ` A \ f ` B" proof (* automatski se razbija na dva podcilja *) assume "x \ A" then have "f x \ f ` A" by auto from this `f x = y` have "y \ f ` A" by auto from this show "y \ f ` A \ f ` B" by auto next assume "x \ B" then have "f x \ f ` B" by auto from this `f x = y` have "y \ f ` B" by auto from this show "y \ f ` A \ f ` B" by auto qed qed next show "f ` A \ f ` B \ f ` (A \ B)" proof fix y assume "y \ f ` A \ f ` B" (* prvo razbijamo uniju *) then have "y \ f ` A \ y \ f ` B" by auto then show "y \ f ` (A \ B)" (* pa onda show i proof *) proof assume "y \ f ` A" then obtain x where "x \ A" "f x = y" by auto from this have "x \ A \ B" by auto from this `f x = y` show "y \ f ` (A \ B)" by auto next assume "y \ f ` B" then obtain x where "x \ B" "f x = y" by auto from this have "x \ A \ B" by auto from this `f x = y` show "y \ f ` (A \ B)" by auto qed qed qed (* f2 sa predavanja *) (* prikazacemo dva nacina za dokazivanje, prvo standardno kao sto smo do sada videli, pa zatim sa moreover - ultimately kombinacijom *) lemma assumes "inj f" shows "f ` (A \ B) = f ` A \ f ` B" (is "?l = ?d") proof show "?l \ ?d" proof fix y assume "y \ ?l" from this obtain x where "x \ A \ B" "f x = y" by auto from this have "x \ A" "x \ B" by auto from this `f x = y` have "y \ f ` A" "y \ f ` B" by auto from this show "y \ ?d" by auto qed next show "?d \ ?l" proof fix y assume "y \ ?d" from this have "y \ f ` A" "y \ f ` B" by auto from this obtain xa where "xa \ A" "f xa = y" by auto from \y \ f ` B\ obtain xb where "xb \ B" "f xb = y" by auto from this `f xa = y` have "f xa = f xb" by auto from this `inj f` have "xa = xb" by (auto simp add: inj_def) from this `xa \ A` `xb \ B` have "xa \ A \ B" by auto from this `f xa = y` show "y \ f ` (A \ B)" by auto qed qed (* drugi nacin: moze se iskoristiti kljucna rec moreover za skupljanje cinjenica koje se na kraju iskoriscavaju sa ultimately *) lemma assumes "inj f" shows "f ` (A \ B) = f ` A \ f ` B" (is "?l = ?d") proof show "?l \ ?d" proof fix y assume "y \ f ` (A \ B)" then obtain x where "x \ A \ B" "f x = y" by auto then have "x \ A" "x \ B" by auto then have "f x \ f ` A" "f x \ f ` B" by auto from this `f x = y` show "y \ f ` A \ f ` B" by auto qed next show "?d \ ?l" proof fix y assume "y \ f ` A \ f ` B" then have "y \ f ` A" "y \ f ` B" by auto from \y \ f ` A\ obtain xa where "xa \ A" "f xa = y" by auto moreover (* sluzi da bi bila jasnija struktura dokaza *) from \y \ f ` B\ obtain xb where "xb \ B" "f xb = y" by auto ultimately have "xa = xb" using `inj f` by (auto simp add: inj_def) from this `xb \ B` have "xa \ B" by auto from this `xa \ A` have "xa \ A \ B" by auto from this `f xa = y` show "y \ f ` (A \ B)" by auto qed qed (* inverzna slika skupa *) (* https://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/HOL/HOL/outline.pdf *) thm vimage_def find_theorems "_ -` _" (* ponavljanje f3 *) lemma inv_slika_lemma: (* navescemo ime ovoj lemi zato sto zelimo da je iskoristimo u dokazu naredne leme *) "f ` (f -` B) \ B" proof fix y assume "y \ f ` (f -` B)" then obtain x where "x \ f -` B" "f x = y" by auto then have "f x \ B" by auto from this `f x = y` show "y \ B" by auto qed find_theorems "_` _ -` _ " thm surj_def lemma assumes "surj f" shows "f ` (f -` A) = A" proof show "f ` (f -` A) \ A" using inv_slika_lemma by auto (* ovo je vec dokazano *) next show "A \ f ` (f -` A)" proof fix y assume "y \ A" obtain x where "f x = y" using \surj f\ (* sledgehammer *) by (metis surjD) from this `y \ A` have "x \ f -` A" by auto from this `f x = y` show "y \ f ` (f -` A)" by auto qed qed find_theorems "_ \ _" thm o_apply thm inj_def (* f5 predavanja *) lemma assumes "inj f" "inj g" shows "inj (f \ g)" proof fix x y assume "(f \ g) x = (f \ g) y" then have "f (g x) = f (g y)" by auto then have "g x = g y" using `inj f` by (auto simp add: inj_def) then show "x = y" using `inj g` by (auto simp add: inj_def) qed (* dodatni primeri za funkcije nad skupovima *) lemma assumes "inj f" shows "x \ A \ f x \ f ` A" proof assume "x \ A" from this show "f x \ f ` A" by auto next assume "f x \ f ` A" then obtain x' where "x' \ A" "f x = f x'" by auto from this `inj f` have "x = x'" by (auto simp add: inj_def) from this `x' \ A` show "x \ A" by auto qed lemma "f -` (f ` A) \ A" proof fix x assume "x \ A" from this have "f x \ f ` A" by auto from this show "x \ f -` (f ` A)" by auto qed lemma assumes "inj f" shows "f -` (f ` A) \ A" (* moze i jednako, samo ovo je drugi smer, prvi je prethodna lema *) proof fix x assume "x \ f -` (f ` A)" from this have "f x \ f ` A" by auto then obtain x' where "x' \ A" "f x = f x'" by auto from this assms have "x = x'" by (auto simp add: inj_def) from this `x' \ A` show "x \ A" by auto qed thm surj_def lemma assumes "surj f" "surj g" shows "surj (f \ g)" unfolding surj_def (* alternativa, unfolding pre dokaza The command “unfolding facts” operates directly on the goal by applying equalities.*) proof fix z obtain y where "z = f y" using `surj f` by auto moreover obtain x where "y = g x" using `surj g` by auto ultimately have "z = f (g x)" by auto from this show "\ x. z = (f \ g) x" by auto qed lemma "f -` (- B) = - (f -` B)" (is "?l = ?d") proof show "?l \ ?d" proof fix x assume "x \ f -` (- B)" thm vimage_def from this have "f x \ - B" by auto from this have "f x \ B" by auto from this have "x \ f -` B" by auto from this show "x \ - (f -` B)" by auto qed next show "?d \ ?l" proof fix x assume "x \ - (f -` B)" from this have "x \ f -` B" by auto thm vimage_def from this have "f x \ B" by auto from this have "f x \ - B" by auto from this show "x \ f -` (- B)" by auto qed qed end