theory Isar_Demo
imports Main
begin

section{* An introductory example *}

lemma "\<not> surj(f :: 'a \<Rightarrow> 'a set)"
proof
  assume 0: "surj f"
  from 0 have 1: "\<forall>A. \<exists>a. A = f a" by(simp add: surj_def)
  from 1 have 2: "\<exists>a. {x. x \<notin> f x} = f a" by blast
  from 2 show "False" by blast
qed

text{* A bit shorter: *}

lemma "\<not> surj(f :: 'a \<Rightarrow> 'a set)"
proof
  assume 0: "surj f"
  from 0 have 1: "\<exists>a. {x. x \<notin> f x} = f a" by(auto simp: surj_def)
  from 1 show "False" by blast
qed

subsection{* this, then, hence and thus *}

text{* Avoid labels, use this: *}

lemma "\<not> surj(f :: 'a \<Rightarrow> 'a set)"
proof
  assume "surj f"
  from this have "\<exists>a. {x. x \<notin> f x} = f a" by(auto simp: surj_def)
  from this show "False" by blast
qed

text{* then = from this *}

lemma "\<not> surj(f :: 'a \<Rightarrow> 'a set)"
proof
  assume "surj f"
  then have "\<exists>a. {x. x \<notin> f x} = f a" by(auto simp: surj_def)
  then show "False" by blast
qed

text{* hence = then have, thus = then show *}

lemma "\<not> surj(f :: 'a \<Rightarrow> 'a set)"
proof
  assume "surj f"
  hence "\<exists>a. {x. x \<notin> f x} = f a" by(auto simp: surj_def)
  thus "False" by blast
qed


subsection{* Structured statements: fixes, assumes, shows *}

lemma
  fixes f :: "'a \<Rightarrow> 'a set"
  assumes s: "surj f"
  shows "False"
proof -  --"no automatic proof step!"
  have "\<exists> a. {x. x \<notin> f x} = f a" using s
    by(auto simp: surj_def)
  thus "False" by blast
qed


section{* Proof patterns *}

lemma "P \<longleftrightarrow> Q"
proof
  assume "P"
  show "Q" sorry
next
  assume "Q"
  show "P" sorry
qed

lemma "A = (B::'a set)"
proof
  show "A \<subseteq> B" sorry
next
  show "B \<subseteq> A" sorry
qed

lemma "A \<subseteq> B"
proof
  fix a
  assume "a \<in> A"
  show "a \<in> B" sorry
qed

text{* Contradiction *}

lemma P
proof (rule ccontr)
  assume "\<not>P"
  show "False" sorry
qed

text{* Case distinction *}

lemma "R"
proof cases
  assume "P"
  show "R" sorry
next
  assume "\<not> P"
  show "R" sorry
qed

lemma "R"
proof -
  have "P \<or> Q" sorry
  then show "R"
  proof
    assume "P"
    show "R" sorry
  next
    assume "Q"
    show "R" sorry
  qed
qed


text{* obtain example *}

lemma "\<not> surj(f :: 'a \<Rightarrow> 'a set)"
proof
  assume "surj f"
  hence "\<exists>a. {x. x \<notin> f x} = f a" by(auto simp: surj_def)
  then obtain a where "{x. x \<notin> f x} = f a" by blast
  hence "a \<notin> f a \<longleftrightarrow> a \<in> f a" by blast
  thus "False" by blast
qed


text{* Interactive exercise: *}

lemma assumes "EX x. ALL y. P x y" shows "ALL y. EX x. P x y"
oops


section{* Streamlining proofs *}

subsection{* Pattern matching and ?-variables *}

text{* Show EX *}

lemma "EX xs. length xs = 0" (is "EX xs. ?P xs")
proof
  show "?P([])" by simp
qed

text{* Multiple EX easier with forward proof: *}

lemma "EX x y :: int. x < z & z < y" (is "EX x y. ?P x y")
proof -
  have "?P (z - 1) (z + 1)" by arith
  thus ?thesis by blast
qed


subsection{* Quoting facts: *}

lemma assumes "x < (0::int)" shows "x*x > 0"
proof -
  from `x<0` show ?thesis by(metis mult_neg_neg)
qed


subsection {* Example: Top Down Proof Development *}

text{* The key idea: case distinction on length: *}
lemma assumes "xs = rev xs"
shows "(EX ys. xs = ys @ rev ys) \<or>
       (EX ys a. xs = ys @ a # rev ys)"
proof cases
  assume "EX n. length xs = n+n"
  show ?thesis sorry
next
  assume "\<not> (EX n. length xs = n+n)"
  show ?thesis sorry
qed

text{* The (almost) complete skeleton: *}
lemma assumes "xs = rev xs"
shows "(EX ys. xs = ys @ rev ys) \<or>
       (EX ys a. xs = ys @ a # rev ys)"
proof cases
  assume "EX n. length xs = n+n"
  then obtain n where "length xs = n+n" by blast
  let ?ys = "take n xs"
  have "xs = ?ys @ rev ?ys" sorry
  thus ?thesis by blast
next
  assume "\<not> (EX n. length xs = n+n)"
  then obtain n where "length xs = Suc(n+n)" sorry
  let ?ys = "take n xs"
  have "xs = ?ys @ xs!n # rev ?ys" sorry
  thus ?thesis by blast
qed

text{* The complete proof: *}
lemma assumes "xs = rev xs"
shows "(EX ys. xs = ys @ rev ys) | (EX ys a. xs = ys @ a # rev ys)"
proof cases
  assume "EX n. length xs = n+n"
  then obtain n where "length xs = n+n" by blast
  let ?ys = "take n xs"
  have "xs = ?ys @ rev ?ys"
    by (metis `length xs = n + n` append_take_drop_id assms diff_add_inverse2 rev_take)
  thus ?thesis by blast
next
  assume "\<not> (EX n. length xs = n+n)"
  hence "EX n. length xs = Suc(n+n)" by arith
  then obtain n where "length xs = Suc(n+n)" by blast
  let ?ys = "take n xs"
  have "xs = ?ys @ xs!n # rev ?ys"
    by (metis Suc_le_lessD `length xs = Suc (n + n)` add_Suc_right add_Suc_shift append_take_drop_id assms diff_add_inverse le_add1 nth_drop' rev_take)
  thus ?thesis by blast
qed


subsection {* moreover *}

lemma assumes "A \<and> B" shows "B \<and> A"
proof -
  from `A \<and> B` have "A" by auto
  moreover
  from `A \<and> B` have "B" by auto
  ultimately show "B \<and> A" by auto
qed


subsection{* Raw proof blocks *}

text{* Compare proof of same lemma above: *}
lemma "k dvd (n+k) \<longleftrightarrow> k dvd (n::int)"
proof -
  { fix a assume a: "n+k = k*a"
    have "EX b. n = k*b"
    proof
      show "n = k*(a - 1)" using a by(simp add: algebra_simps)
    qed }
  moreover
  { fix a have "EX b. k*a + k = k*b"
    proof
      show "k*a + k = k*(a+1)" by(simp add: algebra_simps)
    qed }
  ultimately show ?thesis by (auto simp add: dvd_def)
qed


end