theory week02B_demo_Isar imports Main begin

\<comment> \<open> ------------------------------------------------------------------ \<close>

\<comment> \<open> {* Motivation *} \<close>

lemma "(A \<longrightarrow> B) = (B \<or> \<not>A)"
by blast

value "True \<longrightarrow> False"
value "False \<or> \<not> True"

lemma "(A \<longrightarrow> B) = (B \<or> \<not>A)"
  apply (rule iffI)
   apply (cases A)
    apply (rule disjI1)
    apply (erule impE)
     apply assumption
    apply assumption
   apply (rule disjI2)
   apply assumption
  apply (rule impI)
  apply (erule disjE)
   apply assumption
  apply (erule notE)
  apply assumption
  done


lemma "(A \<longrightarrow> B) = (B \<or> \<not>A)"
 proof (rule iffI)
   assume AimpB: "A\<longrightarrow>B"
   show "B \<or> \<not> A"
   proof (cases A)
     assume A: "A"
     from AimpB A have B:"B" by (rule impE)
     from B show "B \<or> \<not>A" by (rule disjI1)
   next
     assume notA: "\<not> A"
     from notA show "B \<or> \<not>A" by (rule disjI2)
   qed
 next
   assume BA: "B \<or> \<not> A"
   show "A\<longrightarrow>B"
   proof (rule impI)
     assume A: "A"
     from BA A show B
     proof (elim disjE)
       assume B: "B"
       from B show B by assumption
       next
       assume notA: "\<not> A"
       from A notA show B by (elim notE)
     qed
   qed
  qed


(* with this/thus/hence/etc *)
lemma "(A \<longrightarrow> B) = (B \<or> \<not>A)"
proof
  assume AimpB: "A \<longrightarrow> B"
  show " B \<or> \<not> A"
  proof (cases A)
    assume A
    with AimpB have B by (rule impE)
    thus ?thesis by (rule disjI1)
    next
    assume "\<not>A"
    thus ?thesis by (rule disjI2)
  qed
  next
  assume BA: "B \<or> \<not>A"
  show " A \<longrightarrow> B"
  proof
    assume A: A
    from BA show B
    proof
      assume B
      thus B by assumption
      next
      assume notA: "\<not>A"
      from notA A show ?thesis by (rule notE)
    qed
  qed
  qed

\<comment> \<open> ------------------------------------------------------------------ \<close>

\<comment> \<open> {* Isar *} \<close>

lemma "\<lbrakk> A; B \<rbrakk> \<Longrightarrow> A \<and> B"
proof (rule conjI)
  assume A: "A"
  from A show "A" by assumption
next
  assume "B"
  from `B` show "B" by assumption
qed


lemma
  assumes A: "A"
  assumes B: "B"
  shows "A \<and> B"
proof (rule conjI)
  from A show "A" by assumption
  from B show "B" by assumption
qed


lemma "(x::nat) + 1 = 1 + x"
proof -
  have A: "x + 1 = Suc x" by simp
  have B: "1 + x = Suc x" by simp
  show "x + 1 = 1 + x" by (simp only: A B)
qed

\<comment> \<open> ------------------------------------------------------------------ \<close>

section "More Isar"

\<comment> \<open> {* . = by assumption,  .. = by rule *} \<close>

lemma "\<lbrakk> A; B \<rbrakk> \<Longrightarrow> B \<and> A"
proof
  assume A: "A" and B: "B"
  from A show "A" .
  from B show "B" .
qed

lemma "\<lbrakk> A; B \<rbrakk> \<Longrightarrow> B \<and> A"
proof -
  assume A: "A" and B: "B"
  from B A
  show "B \<and> A" ..
qed


\<comment> \<open> {* backward/forward *} \<close>

lemma "A \<and> B \<longrightarrow> B \<and> A"
proof
  assume AB: "A \<and> B"
  from AB show "B \<and> A"
  proof
    assume "B" "A"
    from this
    show "B \<and> A" ..
  qed
qed


\<comment> \<open> {* fix *} \<close>

lemma assumes P: "\<forall>x. P x" shows "\<forall>x. P (f x)"
proof
  fix a
  (* from P show "P (f a)" by (rule spec) *)
  from P show "P (f a)" ..
qed

\<comment> \<open> {* Proof text can only refer to global constants, free variables
in the lemma, and local names introduced via fix or obtain. *} \<close>

lemma assumes Pf: "\<exists>x. P (f x)" shows "\<exists>y. P y"
proof -
  from Pf show ?thesis
  proof
    fix x
    assume "P (f x)"
    from this
    show ?thesis ..
  qed
qed

\<comment> \<open> {* obtain *} \<close>

lemma assumes Pf: "\<exists>x. P (f x)" shows "\<exists>y. P y"
proof -
  from Pf obtain x where "P(f x)" ..
  thus "\<exists>y. P y" ..
qed


lemma assumes ex: "\<exists>x. \<forall>y. P x y" shows "\<forall>y. \<exists>x. P x y"
proof
  fix y
  from ex obtain x where "\<forall>y. P x y" ..
  from this have  "P x y" ..
  (*hence "P x y" ..*)
  from this show   "\<exists>x. P x y" ..
  (*thus "\<exists>x. P x y" .. *)
qed
thm exE
lemma
  assumes A: "\<forall>x y. P x y \<and> Q x y"
  shows "\<exists>x y. P x y \<and> Q x y"
proof -
  from A obtain x y where P: "P x y" and Q: "Q x y" by blast
  thus ?thesis by blast
qed


lemma
  assumes A: "\<forall>x y. P x y \<and> Q x y"
  shows "\<exists>x y. P x y \<and> Q x y"
  apply(rule exI)
  apply(rule exI)
  apply(insert A)
  apply(drule spec)
  apply(drule spec)
  apply assumption
  done

\<comment> \<open> {* moreover *} \<close>

lemma "A \<and> B \<longrightarrow> B \<and> A"
proof
  assume AB: "A \<and> B"
  from AB have "B" by (rule conjunct2)
  moreover from AB have "A" by (rule conjunct1)
  ultimately show "B \<and> A" by (rule conjI)
qed

thm mono_def
thm monoI

lemma
  assumes mono_f: "mono (f::int\<Rightarrow>int)"
      and mono_g: "mono (g::int\<Rightarrow>int)"
  shows "mono (\<lambda>i. f i + g i)"
proof (rule monoI)
  fix i and j :: "int"
  assume A: "i \<le> j"
  from A mono_f
  have "f i \<le> f j" by (simp add: mono_def)
  moreover
  from A mono_g have "g i \<le> g j" by (simp add: mono_def)
  ultimately
  show "f i + g i \<le> f j + g j" by simp
qed

\<comment> \<open> --------------------------------------- \<close>

lemma "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B"
  apply(rule conjI)
  proof -
  assume A thus A .
  assume B thus B .
  qed

end