(* Certified Functional (Co)programming with Isabelle/HOL *)
(* Jasmin Christian Blanchette, Andreas Lochbihler, Andrei Popescu, Dmitriy Traytel *)
section \Isar examples\
theory Isar
imports Main
begin
text \Cantor's theorem\
lemma "\ surj (f :: 'a \ 'a set)"
proof
assume a: "surj f"
from a have b: "\A. \a. A = f a"
by (simp add: surj_def)
from b have c: "\a. {x. x \ f x} = f a"
by blast
from c show False
by blast
qed
lemma
fixes f :: "'a \ 'a set" assumes s: "surj f"
shows False
proof -
have "\a. {x. x \ f x} = f a"
using s by (auto simp: surj_def)
then show False
by blast
qed
text \Case distinction\
lemma R
proof cases
assume P
show R
sorry
next
assume "\ P"
show R
sorry
qed
lemma
assumes "P \ Q"
shows R
using assms
proof
assume P
show R
sorry
next
assume Q
show R
sorry
qed
text \Contradiction\
lemma "\ P"
proof
assume P
show False
sorry
qed
lemma P
proof (rule ccontr)
assume "\ P"
show False
sorry
qed
text \Equivalence\
lemma "P \ Q"
proof
assume P
show Q
sorry
next
assume Q
show P
sorry
qed
text \Quantifiers\
lemma "\x. P x"
proof
fix x
show "P x"
sorry
qed
lemma "\x. P x"
proof
show "P witness"
sorry
qed
end