theory Cas4
  imports Main
begin

lemma inv_slika_lema: "f ` (f -` B) \<subseteq> B"
proof
  fix y
  assume "y \<in> f ` (f -` B)"
  then obtain x where "x \<in> f -` B" "y = f x"
    by auto
  have "f x \<in> B"
    using \<open>x \<in> f -` B\<close>
    by auto
  then show "y \<in> B"
    using `y = f x`
    by auto
qed

lemma 
  assumes "surj f"
  shows "f ` (f -` A) = A"
proof
  show "f ` (f -` A) \<subseteq> A"
    using inv_slika_lema
    by auto
next
  show "A \<subseteq> f ` (f -` A)"
  proof
    fix y
    assume "y \<in> A"
    
    obtain x where "f x = y"
      using `surj f`
      unfolding surj_def
      by metis

    have "x \<in> f -` A"
      using `f x = y` `y \<in> A`
      by auto


    show "y \<in> f ` (f -` A)"
      using \<open>x \<in> f -` A\<close> `f x = y` 
      by auto
  qed
qed

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 (simp add: inj_def)
  then show "x = y"
    using `inj g`
    unfolding inj_def
    by auto
qed


lemma
  shows "A \<and> B \<longrightarrow> B \<and> A"
proof
  assume "A \<and> B"
  then have "A" "B"
    by auto
  show "B \<and> A"
  proof
    show "B"
      by fact
  next
    show "A"
      by fact
  qed
qed


(*

Uvodjenje implikacije:
Ako hoces da dokazes implikaciju, tada
pretpostavi da vazi leva strana i pod tom
pretpostavkom dokazi da vazi desna strana.

Uvodjenje konjunkcije: 
Ako hoces da dokazes konjunkciju, 
dokazi prvo prvi operand, a posle dokazi
drugi operand. 

Osolobadjanje konjunkcije:
Ako znas da je dokazana (ili pretpostavljena) konjunkcija, 
onda smatraj da su dokazani i pojedinacni clanovi. 


*)

thm inv_slika_lema
thm conjI
thm impI
thm conjE

lemma
  shows "A \<and> B \<longrightarrow> B \<and> A"
  apply (rule impI)
  apply (erule conjE)
  apply (rule conjI)
   apply (assumption)
  apply (assumption)
  done

thm disjI1
thm disjI2
thm disjE

lemma
  "A \<or> B \<longrightarrow> B \<or> A"
  apply (rule impI)
  apply (erule disjE)
   apply (rule disjI2)
   apply (assumption)
  apply (rule disjI1)
  apply (assumption)
  done

lemma
  "A \<and> B \<longrightarrow> A \<or> B"
  apply (rule impI)
  apply (rule disjI1)
  apply (erule conjE)
  apply assumption
  done

end