gistfile1.txt

datatype nat = Z | S nat

fun plus :: "nat ⇒ nat ⇒ nat" where
"plus Z m = m" | 
"plus (S n) m = S (plus n m)"

fun mult :: "nat ⇒ nat ⇒ nat" where
"mult Z m = Z" | 
"mult (S n) m = plus (mult n m) m"

fun factorial :: "nat ⇒ nat" where
"factorial Z = (S Z)" | 
"factorial (S n) = mult (S n) (factorial n)"

definition ten :: nat where "ten = (S (S (S (S (S (S (S (S (S Z)))))))))" 
definition twelve :: nat where "twelve = (S (S (S (S (S (S (S (S (S Z)))))))))"

theorem test_factorial1 : "factorial (S (S (S Z))) = S (S (S (S (S (S Z)))))" by simp

(* simplification only simplifies the left side, not the right side
theorem test_factorial2 : "factorial (S (S (S (S (S Z))))) = mult ten twelve" by simp
*)