theory Introduction
imports Main
begin
section{*Propositional Logic in HOL*}
thm conjI
thm disjI1 disjI2
thm notI
thm impI
section{*First Order Logic (Quantifiers)*}
thm allI
thm exI
lemma "(a \ b \ c) \ (a \ b \ c)" by blast
lemma "\x. x"
apply(rule)
quickcheck
oops
section{*Introduction to Isabelle and functional Programming*}
(*finds all fives in a list of natural numbers*)
fun find_fives :: "nat list \ nat list" where
"find_fives [] = []"
| "find_fives (x#xs) = (if x = 5 then 5 # find_fives xs else find_fives xs)"
value "find_fives [1,3,5,8,5,2,5]"
lemma "find_fives [1,3,5,8,5,2,5] = [5,5,5]" by simp
(*the library function filter*)
term filter
lemma "find_fives l = filter (\x. x = 5) l"
by(induction l, simp_all)
end