equal
deleted
inserted
replaced
28 Suc_neq_0: "Suc(m) = 0 ==> R" |
28 Suc_neq_0: "Suc(m) = 0 ==> R" |
29 rec_0: "rec(0, a, f) = a" |
29 rec_0: "rec(0, a, f) = a" |
30 rec_Suc: "rec(Suc(m), a, f) = f(m, rec(m, a, f))" |
30 rec_Suc: "rec(Suc(m), a, f) = f(m, rec(m, a, f))" |
31 |
31 |
32 definition |
32 definition |
33 add :: "['a::nat, 'a] => 'a" (infixl "+" 60) |
33 add :: "['a::nat, 'a] => 'a" (infixl "+" 60) where |
34 "m + n = rec(m, n, %x y. Suc(y))" |
34 "m + n = rec(m, n, %x y. Suc(y))" |
35 |
35 |
36 lemma Suc_n_not_n: "Suc(k) ~= (k::'a::nat)" |
36 lemma Suc_n_not_n: "Suc(k) ~= (k::'a::nat)" |
37 apply (rule_tac n = k in induct) |
37 apply (rule_tac n = k in induct) |
38 apply (rule notI) |
38 apply (rule notI) |