1246
|
1 |
(* Title: FOL/ex/NatClass.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: Markus Wenzel, TU Muenchen
|
|
4 |
*)
|
|
5 |
|
17245
|
6 |
theory NatClass
|
|
7 |
imports FOL
|
|
8 |
begin
|
|
9 |
|
|
10 |
text {*
|
|
11 |
This is an abstract version of theory @{text "Nat"}. Instead of
|
|
12 |
axiomatizing a single type @{text nat} we define the class of all
|
|
13 |
these types (up to isomorphism).
|
|
14 |
|
|
15 |
Note: The @{text rec} operator had to be made \emph{monomorphic},
|
|
16 |
because class axioms may not contain more than one type variable.
|
|
17 |
*}
|
1246
|
18 |
|
|
19 |
consts
|
17245
|
20 |
0 :: 'a ("0")
|
|
21 |
Suc :: "'a => 'a"
|
|
22 |
rec :: "['a, 'a, ['a, 'a] => 'a] => 'a"
|
1246
|
23 |
|
|
24 |
axclass
|
17245
|
25 |
nat < "term"
|
|
26 |
induct: "[| P(0); !!x. P(x) ==> P(Suc(x)) |] ==> P(n)"
|
|
27 |
Suc_inject: "Suc(m) = Suc(n) ==> m = n"
|
|
28 |
Suc_neq_0: "Suc(m) = 0 ==> R"
|
|
29 |
rec_0: "rec(0, a, f) = a"
|
|
30 |
rec_Suc: "rec(Suc(m), a, f) = f(m, rec(m, a, f))"
|
1246
|
31 |
|
19819
|
32 |
definition
|
17245
|
33 |
add :: "['a::nat, 'a] => 'a" (infixl "+" 60)
|
19819
|
34 |
"m + n = rec(m, n, %x y. Suc(y))"
|
|
35 |
|
|
36 |
lemma Suc_n_not_n: "Suc(k) ~= (k::'a::nat)"
|
|
37 |
apply (rule_tac n = k in induct)
|
|
38 |
apply (rule notI)
|
|
39 |
apply (erule Suc_neq_0)
|
|
40 |
apply (rule notI)
|
|
41 |
apply (erule notE)
|
|
42 |
apply (erule Suc_inject)
|
|
43 |
done
|
|
44 |
|
|
45 |
lemma "(k+m)+n = k+(m+n)"
|
|
46 |
apply (rule induct)
|
|
47 |
back
|
|
48 |
back
|
|
49 |
back
|
|
50 |
back
|
|
51 |
back
|
|
52 |
back
|
|
53 |
oops
|
|
54 |
|
|
55 |
lemma add_0 [simp]: "0+n = n"
|
|
56 |
apply (unfold add_def)
|
|
57 |
apply (rule rec_0)
|
|
58 |
done
|
1246
|
59 |
|
19819
|
60 |
lemma add_Suc [simp]: "Suc(m)+n = Suc(m+n)"
|
|
61 |
apply (unfold add_def)
|
|
62 |
apply (rule rec_Suc)
|
|
63 |
done
|
|
64 |
|
|
65 |
lemma add_assoc: "(k+m)+n = k+(m+n)"
|
|
66 |
apply (rule_tac n = k in induct)
|
|
67 |
apply simp
|
|
68 |
apply simp
|
|
69 |
done
|
|
70 |
|
|
71 |
lemma add_0_right: "m+0 = m"
|
|
72 |
apply (rule_tac n = m in induct)
|
|
73 |
apply simp
|
|
74 |
apply simp
|
|
75 |
done
|
|
76 |
|
|
77 |
lemma add_Suc_right: "m+Suc(n) = Suc(m+n)"
|
|
78 |
apply (rule_tac n = m in induct)
|
|
79 |
apply simp_all
|
|
80 |
done
|
|
81 |
|
|
82 |
lemma
|
|
83 |
assumes prem: "!!n. f(Suc(n)) = Suc(f(n))"
|
|
84 |
shows "f(i+j) = i+f(j)"
|
|
85 |
apply (rule_tac n = i in induct)
|
|
86 |
apply simp
|
|
87 |
apply (simp add: prem)
|
|
88 |
done
|
1246
|
89 |
|
|
90 |
end
|