theory Cas3_vezbe
imports Main

begin

(* ponavljanje sa predavanja *)
lemma "f = g \<longleftrightarrow> (\<forall> 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 \<longleftrightarrow> inj f \<and> 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 \<union> B) = f ` A \<union> f ` B"
  by auto

find_theorems "_ ` _ \<inter> _ ` _"

thm image_Int

lemma 
  assumes "inj f"
  shows "f ` (A \<inter> B) = f ` A \<inter> 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 \<union> B) = f ` A \<union> f ` B"
proof 
  show "f ` (A \<union> B) \<subseteq> f ` A \<union> f ` B"
  proof
    fix y (* zato sto odgovara slici *)
    assume "y \<in> f ` (A \<union> B)" 
    thm image_def
    then have "\<exists> x. x \<in> A \<union> B \<and> f x = y" by auto (* po definiciji f ` *)
    then obtain x where "x \<in> A \<union> B" "f x = y" by auto
    then have "x \<in> A \<or> x \<in> B" by auto
    then show "y \<in> f ` A \<union> f ` B"
    proof (* automatski se razbija na dva podcilja *)
      assume "x \<in> A" 
      then have "f x \<in> f ` A" by auto
      from this `f x = y` have "y \<in> f ` A" by auto
      from this show "y \<in> f ` A \<union> f ` B" by auto
    next 
      assume "x \<in> B" 
      then have "f x \<in> f ` B" by auto
      from this `f x = y` have "y \<in> f ` B" by auto
      from this show "y \<in> f ` A \<union> f ` B" by auto
    qed
  qed
next 
  show "f ` A \<union> f ` B \<subseteq> f ` (A \<union> B)"
  proof
    fix y 
    assume "y \<in> f ` A \<union> f ` B" (* prvo razbijamo uniju *)
    then have "y \<in> f ` A \<or> y \<in> f ` B" by auto
    then show "y \<in> f ` (A \<union> B)" (* pa onda show i proof *)
    proof 
      assume "y \<in> f ` A"
      then obtain x where "x \<in> A" "f x = y" by auto
      from this have "x \<in> A \<union> B" by auto
      from this `f x = y` 
      show "y \<in> f ` (A \<union> B)" by auto
    next 
      assume "y \<in> f ` B" 
      then obtain x where "x \<in> B" "f x = y" by auto
      from this have "x \<in> A \<union> B" by auto
      from this `f x = y` 
      show "y \<in> f ` (A \<union> 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 \<inter> B) = f ` A \<inter> f ` B" (is "?l = ?d")
proof
  show "?l \<subseteq> ?d"
  proof
    fix y
    assume "y \<in> ?l"
    from this obtain x where "x \<in> A \<inter> B" "f x = y" by auto
    from this have "x \<in> A" "x \<in> B" by auto
    from this `f x = y` have "y \<in> f ` A" "y \<in> f ` B" by auto
    from this show "y \<in> ?d" by auto
  qed
next
  show "?d \<subseteq> ?l"
  proof
    fix y
    assume "y \<in> ?d"
    from this have "y \<in> f ` A" "y \<in> f ` B" by auto
    from this obtain xa where "xa \<in> A" "f xa = y" by auto
    from \<open>y \<in> f ` B\<close> obtain xb where "xb \<in> 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 \<in> A` `xb \<in> B` have "xa \<in> A \<inter> B" by auto
    from this `f xa = y` show "y \<in> f ` (A \<inter> 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 \<inter> B) = f ` A \<inter> f ` B" (is "?l = ?d")
proof 
  show "?l \<subseteq> ?d" 
  proof
    fix y
    assume "y \<in> f ` (A \<inter> B)" 
    then obtain x where "x \<in> A \<inter> B" "f x = y" by auto
    then have "x \<in> A" "x \<in> B" by auto
    then have "f x \<in> f ` A" "f x \<in> f ` B" by auto
    from this `f x = y` 
    show "y \<in> f ` A \<inter> f ` B" by auto
  qed
next 
  show "?d \<subseteq> ?l" 
  proof 
    fix y 
    assume "y \<in> f ` A \<inter> f ` B"
    then have "y \<in> f ` A" "y \<in> f ` B" by auto

    from \<open>y \<in> f ` A\<close>
    obtain xa where "xa \<in> A" "f xa = y" by auto

    moreover (* sluzi da bi bila jasnija struktura dokaza *)

    from \<open>y \<in> f ` B\<close>
    obtain xb where "xb \<in> B" "f xb = y" by auto

    ultimately

    have "xa = xb" using `inj f` by (auto simp add: inj_def)
    from this `xb \<in> B` have "xa \<in> B" by auto
    from this `xa \<in> A` have "xa \<in> A \<inter> B" by auto
    from this `f xa = y` 
    show "y \<in> f ` (A \<inter> 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) \<subseteq> B"
proof
  fix y
  assume "y \<in> f ` (f -` B)"
  then obtain x where "x \<in> f -` B" "f x = y" by auto
  then have "f x \<in> B" by auto
  from this `f x = y` 
  show "y \<in> B" by auto
qed

find_theorems "_` _ -` _ "

thm surj_def

lemma assumes "surj f"
  shows "f ` (f -` A) = A"
proof 
  show "f ` (f -` A) \<subseteq> A" using inv_slika_lemma by auto (* ovo je vec dokazano *)
next 
  show "A \<subseteq> f ` (f -` A)" 
  proof 
    fix y
    assume "y \<in> A"
    obtain x where "f x = y" using \<open>surj f\<close> 
      (* sledgehammer *)
      by (metis surjD)

    from this `y \<in> A` 
    have "x \<in> f -` A" by auto

    from this `f x = y`
    show "y \<in> f ` (f -` A)" by auto
  qed
qed

find_theorems "_ \<circ> _"
thm o_apply
thm inj_def

(* f5 predavanja *)
lemma assumes "inj f" "inj g"
  shows "inj (f \<circ> g)"
proof
  fix x y
  assume "(f \<circ> g) x = (f \<circ> 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 \<in> A \<longleftrightarrow> f x \<in> f ` A"
proof 
  assume "x \<in> A" 
  from this
  show "f x \<in> f ` A"  by auto
next 
  assume "f x \<in> f ` A" 
  then obtain x' where "x' \<in> A" "f x = f x'" by auto
  from this `inj f` have "x = x'" by (auto simp add: inj_def)
  from this `x' \<in> A` 
  show "x \<in> A" by auto
qed


lemma "f -` (f ` A) \<supseteq> A"
proof 
  fix x 
  assume "x \<in> A"
  from this have "f x \<in> f ` A" by auto
  from this show "x \<in> f -` (f ` A)" by auto
qed

lemma
  assumes "inj f"
  shows "f -` (f ` A) \<subseteq> A" (* moze i jednako, samo ovo je drugi smer, prvi je prethodna lema *)
proof 
  fix x
  assume "x \<in> f -` (f ` A)" 
  from this have "f x \<in> f ` A" by auto
  then obtain x' where "x' \<in> A" "f x = f x'" by auto
  from this assms have "x = x'" by (auto simp add: inj_def)
  from this `x' \<in> A` show "x \<in> A" by auto
qed

thm surj_def

lemma
  assumes "surj f" "surj g"
  shows "surj (f \<circ> 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 "\<exists> x. z = (f \<circ> g) x" by auto
qed

lemma "f -` (- B) = - (f -` B)" (is "?l = ?d")
proof
  show "?l \<subseteq> ?d"
  proof
    fix x
    assume "x \<in> f -` (- B)"
    thm vimage_def
    from this have "f x \<in> - B" by auto
    from this have "f x \<notin> B" by auto
    from this have "x \<notin> f -` B" by auto
    from this show "x \<in> - (f -` B)" by auto
  qed
next
  show "?d \<subseteq> ?l" 
  proof
    fix x
    assume "x \<in> - (f -` B)"
    from this have "x \<notin> f -` B" by auto
    thm vimage_def
    from this have "f x \<notin> B" by auto
    from this have "f x \<in> - B" by auto
    from this show "x \<in> f -` (- B)" by auto
  qed
qed


end