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