theory Logic = Main:

section{*Logic \label{sec:Logic}*}

subsection{*Propositional logic*}

subsubsection{*Introduction rules*}


lemma "A \<longrightarrow> A"
proof (rule impI)
  assume a: "A"
  show "A" by(rule a)
qed

(* proof *)

lemma "A \<longrightarrow> A"
proof
  assume a: A
  show A by(rule a)
qed

(* . *)

lemma "A \<longrightarrow> A"
proof
  assume "A"
  show "A" .
qed

(* by *)

lemma "A \<longrightarrow> A \<and> A"
proof
  assume "A"
  show "A \<and> A" by(rule conjI)
qed

(* .. *)

lemma "A \<longrightarrow> A \<and> A"
proof
  assume "A"
  show "A \<and> A" ..
qed


subsubsection{*Elimination rules*}


lemma "A \<and> B \<longrightarrow> B \<and> A"
proof
  assume AB: "A \<and> B"
  show "B \<and> A"
  proof (rule conjE[OF AB])  
    assume "A" "B"
    show ?thesis ..
  qed
qed


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

(* this, then, thus *)

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


lemma "A \<and> B \<longrightarrow> B \<and> A"
proof
  assume ab: "A \<and> B"
  from ab have a: "A" ..
  from ab have b: "B" ..
  from b a show "B \<and> A" ..
qed



subsection{*More constructs*}


lemma "A \<and> B \<longrightarrow> B \<and> A"
proof
  assume ab: "A \<and> B"
  from ab have "B" ..
  moreover
  from ab have "A" ..
  ultimately show "B \<and> A" ..
qed

(* hence, with *)

lemma "\<not> (A \<and> B) \<longrightarrow> \<not> A \<or> \<not> B"
proof
  assume n: "\<not> (A \<and> B)"
  show "\<not> A \<or> \<not> B"
  proof (rule ccontr)
    assume nn: "\<not> (\<not> A \<or> \<not> B)"
    have "\<not> A"
    proof
      assume "A"
      have "\<not> B"
      proof
        assume "B"
        have "A \<and> B" ..
        with n show False ..
      qed
      hence "\<not> A \<or> \<not> B" ..
      with nn show False ..
    qed
    hence "\<not> A \<or> \<not> B" ..
    with nn show False ..
  qed
qed


lemma "A & (B | C) \<longrightarrow> (A & B) | (A & C)"
sorry
    
subsection{*Avoiding duplication*}


lemma "A \<and> B \<Longrightarrow> B \<and> A"
proof
  assume "A \<and> B" thus "B" ..
next
  assume "A \<and> B" thus "A" ..
qed


lemma "large_A \<and> large_B \<Longrightarrow> large_B \<and> large_A"
      (is "?AB \<Longrightarrow> ?B \<and> ?A")
proof
  assume "?AB" thus "?B" ..
next
  assume "?AB" thus "?A" ..
qed


lemma assumes AB: "large_A \<and> large_B"
  shows "large_B \<and> large_A" (is "?B \<and> ?A")
proof
  from AB show "?B" ..
next
  from AB show "?A" ..
qed


lemma assumes AB: "large_A \<and> large_B"
  shows "large_B \<and> large_A" (is "?B \<and> ?A")
using AB
proof
  assume "?A" "?B" show ?thesis ..
qed


lemma assumes AB: "A \<or> B" shows "B \<or> A"
proof -
  from AB show ?thesis
  proof
    assume A show ?thesis ..
  next
    assume B show ?thesis ..
  qed
qed


subsection{*Predicate calculus*}

(* fix *)

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

(* Text can only refer to global constants, free variables
   in the lemma, and local names introduced via "fix"/"obtain" *)

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)"
    show ?thesis ..  
  qed
qed


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" ..
  hence "P x y" ..
  thus "\<exists>x. P x y" ..
qed

lemma "EX x. P x \<longrightarrow> (ALL x. P x)"
sorry

subsection{*Making bigger steps*}


theorem "\<exists>S. S \<notin> range (f :: 'a \<Rightarrow> 'a set)"
proof
  let ?S = "{x. x \<notin> f x}"
  show "?S \<notin> range f"
  proof
    assume "?S \<in> range f"
    then obtain y where fy: "?S = f y" ..
    show False
    proof cases
      assume "y \<in> ?S"
      with fy show False by blast
    next
      assume "y \<notin> ?S"
      with fy show False by blast
    qed
  qed
qed


theorem "\<exists>S. S \<notin> range (f :: 'a \<Rightarrow> 'a set)"
proof
  let ?S = "{x. x \<notin> f x}"
  show "?S \<notin> range f"
  proof
    assume "?S \<in> range f"
    then obtain y where fy: "?S = f y" ..
    show False
    proof cases
      assume "y \<in> ?S"
      hence "y \<notin> f y"   by simp
      hence "y \<notin> ?S"    by(simp add:fy)
      thus False         by contradiction
    next
      assume "y \<notin> ?S"
      hence "y \<in> f y"   by simp
      hence "y \<in> ?S"    by(simp add:fy)
      thus False         by contradiction
    qed
  qed
qed


theorem "\<exists>S. S \<notin> range (f :: 'a \<Rightarrow> 'a set)"
by best
(* Of course this only works in the context of HOL's carefully
constructed introduction and elimination rules for set theory.*)

subsection{*Raw proof blocks*}


ML"set quick_and_dirty"
lemma "\<forall>x y. A x y \<and> B x y \<longrightarrow> C x y"
proof
  fix x show "\<forall>y. A x y \<and> B x y \<longrightarrow> C x y"
  proof
    fix y show "A x y \<and> B x y \<longrightarrow> C x y"
    proof
      assume "A x y \<and> B x y"
      show "C x y" sorry
    qed
  qed
qed


lemma "\<forall>x y. A x y \<and> B x y \<longrightarrow> C x y"
proof -
  have "\<And>x y. \<lbrakk> A x y; B x y \<rbrakk> \<Longrightarrow> C x y"
  proof -
    fix x y assume "A x y" "B x y"
    show "C x y" sorry
  qed
  thus ?thesis by blast
qed



lemma "\<forall>x y. A x y \<and> B x y \<longrightarrow> C x y"
proof -
  { fix x y assume "A x y" "B x y"
    have "C x y" sorry }
  thus ?thesis by blast
qed



subsection{*Further refinements*}



subsubsection{*\isakeyword{obtain}*}



lemma assumes A: "\<exists>x y. P x y \<and> Q x y" shows "R"
proof -
  from A obtain x y where P: "P x y" and Q: "Q x y"  by blast
oops


subsubsection{*Combining proof styles*}



lemma "A \<longrightarrow> (A \<longrightarrow> B) \<longrightarrow> B"
proof
  assume a: "A"
  show "(A \<longrightarrow>B) \<longrightarrow> B"
    apply(rule impI)
    apply(erule impE)
    apply(rule a)
    apply assumption
    done
qed



end