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{* Quoting facts: *}
lemma "A \ A"
proof
assume "A"
show "A" by(rule `A`)
qed
subsubsection{*Forward reasoning*}
lemma "A \ A \ A"
proof
assume "A"
show "A \ A" by(rule conjI[OF `A` `A`])
qed
text{* \isakeyword{from} *}
lemma "A \ A \ A"
proof
assume "A"
from `A` `A` show "A \ A" by(rule conjI)
qed
text{* Default rules and ".." *}
lemma "A \ A \ A"
proof
assume "A"
from `A` `A` show "A \ A" by(rule)
qed
subsubsection{*Elimination rules*}
lemma "A \ B \ B \ A"
proof
assume "A \ B"
show "B \ A"
proof (rule conjE[OF `A\B`])
assume "A" "B"
from `B` `A` show ?thesis ..
qed
qed
lemma "A \ B \ B \ A"
proof
assume AB: "A \ B"
from AB show "B \ A"
proof
assume "A" "B"
from `B` `A` show ?thesis ..
qed
qed
text{* @{text this}, \isakeyword{then} *}
lemma "A \ B \ B \ A"
proof
assume "A \ B"
from this show "B \ A"
proof
assume "A" "B"
from `B` `A` show ?thesis ..
qed
qed
lemma "A \ B \ B \ A"
proof
assume "A \ B"
then show "B \ A"
proof
assume "B" "A"
then show ?thesis ..
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 A: "large_A" and B: "large_B"
shows "large_B \ large_A" (is "?B \ ?A")
proof
show "?A" by(rule A)
next
show "?B" by(rule B)
qed
lemma assumes AB: "A \ B" shows "B \ A"
proof - -- "- = do nothing"
from AB show ?thesis
proof
assume A then show ?thesis by(rule disjI2)
next
assume B then 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