t01.thy

theory T01
imports Main
begin
fun add::"nat⇒nat⇒nat" where
"add 0 m = m" |
"add (Suc m) n = Suc (add m n)"

fun double :: "nat ⇒ nat" where
"double 0 = add 0 0" |
"double (Suc m) = Suc(Suc (double m))"

theorem add_assoc [simp] : "add (add x y) z = add x (add y z)"
apply(induction x)
apply(auto)
done
lemma add_zero [simp] : "add x 0 = add 0 x"
apply(induction x)
apply(auto)
done
lemma add2 [simp] : "add x (Suc y) = Suc (add x y)"
apply(induction x)
apply(auto)
done
theorem add_com [simp]: "add x y = add y x"
apply(induction x)
apply(auto)
done

theorem add_d [simp] : "double x = add x x"
apply(induction x)
apply(auto)
done
end