theory Vendredi = Main:

consts snoc :: "'a list => 'a => 'a list"
primrec
"snoc [] elt = [elt]"
"snoc (Cons a l) elt = (Cons a (snoc l elt))"

lemma [simp] : "l @ [a, x] = snoc (l @ [a]) x"
apply (induct l)
apply auto
done

theorem rev_cons: "rev (x # xs) = snoc (rev xs) x"
apply (induct xs)
apply auto
done

consts pow :: "nat => nat => nat"
primrec
"pow x 0 = 1"
"pow x (Suc n) = x * (pow x n)"

lemma [simp] : "pow x (m + n) = pow x m * pow x n"
apply (induct n)
apply auto
done

theorem pow_mult: "pow x (m * n) = pow (pow x m) n"
apply (induct n)
apply auto
done

consts sum :: "nat list => nat"
primrec
"sum [] = 0"
"sum (Cons a l) = a + (sum l)"

lemma [simp] : "sum (l @ [a]) = a + sum l"
apply (induct l)
apply auto
done

theorem sum_rev : "sum (rev xs) = sum xs"
apply (induct xs)
apply auto
done

consts Sum :: "(nat => nat) => nat => nat"
primrec
"Sum f 0 = 0"
"Sum f (Suc n) = (f n) + (Sum f n)"

theorem "Sum (%i. f i + g i) k = Sum f k + Sum g k"
apply (induct k)
apply auto
done

theorem "Sum f (k + l) = Sum f k + Sum (%i. f(i + k)) l"
apply (induct l)
apply auto
apply (simp add: add_ac)
done

theorem "Sum f k = sum (map f [0..k(])"
apply (induct k)
apply auto
done

datatype peg = A | B | C
types move = "peg * peg"

consts moves :: "nat => peg => peg => peg => move list"
primrec
"moves 0 a b c = []"
"moves (Suc n) a b c = (moves n a c b) @ [(A,C)] @ (moves n b a c)"

lemma [simp] : "2 ^ n + 2 ^ n - Suc 0 = 2 * 2 ^ n - Suc 0"
apply (induct n)
apply auto
done

theorem "! a b c. length (moves n a b c) = 2^n - 1"
apply (induct n)
apply auto
done