theory Demo1
imports Main
begin
section{*Logic*}
subsection{*Propositional logic*}
subsubsection{*Introduction rules*}
lemma "A \ A"
proof (rule impI)
assume a: "A"
show "A" by(rule a)
qed
text{* \isakeyword{proof} *}
lemma "A \ A"
proof
assume a: A
show A by(rule a)
qed
text{* \isakeyword{.} *}
lemma "A \ A"
proof
assume "A"
show "A" .
qed
text{* \isakeyword{by} *}
lemma "A \ A \ A"
proof
assume "A"
show "A \ A" by(rule conjI)
qed
text{* \isakeyword{..} *}
lemma "A \ A \ A"
proof
assume "A"
show "A \ A" ..
qed
subsubsection{*Elimination rules*}
lemma "A \ B \ B \ A"
proof
assume AB: "A \ B"
show "B \ A"
proof (rule conjE[OF AB])
assume "A" "B"
show ?thesis ..
qed
qed
lemma "A \ B \ B \ A"
proof
assume AB: "A \ B"
from AB show "B \ A"
proof
assume "A" "B"
show ?thesis ..
qed
qed
text{* @{text this}, \isakeyword{then}, \isakeyword{thus} *}
lemma "A \ B \ B \ A"
proof
assume "A \ B"
from this show "B \ A"
proof
assume "A" "B"
show ?thesis ..
qed
qed
lemma "A \ B \ B \ A"
proof
assume ab: "A \ B"
from ab have a: "A" ..
from ab have b: "B" ..
from b a show "B \ A" ..
qed
subsection{*More constructs*}
text{* \isakeyword{hence}, \isakeyword{with} *}
lemma "\ (A \ B) \ \ A \ \ B"
proof
assume n: "\ (A \ B)"
show "\ A \ \ B"
proof (rule ccontr)
assume nn: "\ (\ A \ \ B)"
have "\ A"
proof
assume "A"
have "\ B"
proof
assume "B"
have "A \ B" ..
from n this show False ..
qed
hence "\ A \ \ B" ..
with nn show False ..
qed
hence "\ A \ \ B" ..
with nn show False ..
qed
qed
text{* Interactive exercise: *}
lemma "A & (B | C) \ (A & B) | (A & C)"
oops
subsection{*Avoiding duplication*}
lemma "A \ B \ B \ A"
proof
assume "A \ B" thus "B" ..
next
assume "A \ B" thus "A" ..
qed
lemma "large_A \ large_B \ large_B \ large_A"
(is "?AB \ ?B \ ?A")
proof
assume "?AB" thus "?B" ..
next
assume "?AB" thus "?A" ..
qed
lemma assumes AB: "large_A \ large_B"
shows "large_B \ large_A" (is "?B \ ?A")
proof
from AB show "?B" ..
next
from AB show "?A" ..
qed
lemma assumes AB: "large_A \ large_B"
shows "large_B \ large_A" (is "?B \ ?A")
using AB
proof
assume "?A" "?B" show ?thesis ..
qed
lemma assumes AB: "A \ B" shows "B \ A"
proof - -- "- = do nothing"
from AB show ?thesis
proof
assume A show ?thesis ..
next
assume B show ?thesis ..
qed
qed
subsection{*Predicate calculus*}
text{* \isakeyword{fix} *}
lemma assumes P: "\x. P x" shows "\x. P(f x)"
proof
fix a
from P show "P(f a)" ..
qed
text{* Proof text can only refer to global constants, free variables
in the lemma, and local names introduced via \isakeyword{fix} or
\isakeyword{obtain}. *}
lemma assumes Pf: "\x. P(f x)" shows "\y. P y"
proof -
from Pf show ?thesis
proof
fix x
assume "P(f x)"
show ?thesis ..
qed
qed
lemma assumes Pf: "\x. P(f x)" shows "\y. P y"
proof -
from Pf obtain x where "P(f x)" ..
thus "\y. P y" ..
qed
lemma assumes ex: "\x. \y. P x y" shows "\y. \x. P x y"
proof
fix y
from ex obtain x where "\y. P x y" ..
hence "P x y" ..
thus "\x. P x y" ..
qed
subsection{*Making bigger steps*}
theorem "\S. S \ range (f :: 'a \ 'a set)"
proof
let ?S = "{x. x \ f x}"
show "?S \ range f"
proof
assume "?S \ range f"
then obtain y where fy: "?S = f y" ..
show False
proof cases
assume "y \ ?S"
with fy show False by blast
next
assume "y \ ?S"
with fy show False by blast
qed
qed
qed
theorem "\S. S \ range (f :: 'a \ 'a set)"
proof
let ?S = "{x. x \ f x}"
show "?S \ range f"
proof
assume "?S \ range f"
then obtain y where fy: "?S = f y" ..
show False
proof cases
assume "y \ ?S"
hence "y \ f y" by simp
hence "y \ ?S" by(simp add:fy)
thus False by contradiction
next
assume "y \ ?S"
hence "y \ f y" by simp
hence "y \ ?S" by(simp add:fy)
thus False by contradiction
qed
qed
qed
text{* Interactive exercise: *}
lemma "EX x. P x \ (ALL x. P x)"
oops
subsection{*Further refinements*}
subsubsection{*\isakeyword{obtain}*}
lemma assumes A: "\x y. P x y \ 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 \ (A \ B) \ B"
proof
assume "A"
thus "(A \B) \ B"
apply - -- "make all incoming facts assumptions"
apply(rule impI)
apply(erule mp)
apply assumption
done
qed
end