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