equal
deleted
inserted
replaced
56 |
56 |
57 local |
57 local |
58 |
58 |
59 defs |
59 defs |
60 Zero_nat_def: "0 == Abs_Nat Zero_Rep" |
60 Zero_nat_def: "0 == Abs_Nat Zero_Rep" |
61 Suc_def: "Suc == (%n. Abs_Nat (Suc_Rep (Rep_Nat n)))" |
61 Suc_def: "Suc == (%n. Abs_Nat (Suc_Rep (Rep_Nat n)))" |
62 One_nat_def [simp]: "1 == Suc 0" |
62 One_nat_def: "1 == Suc 0" |
63 |
63 |
64 -- {* nat operations *} |
64 -- {* nat operations *} |
65 pred_nat_def: "pred_nat == {(m, n). n = Suc m}" |
65 pred_nat_def: "pred_nat == {(m, n). n = Suc m}" |
66 |
66 |
67 less_def: "m < n == (m, n) : trancl pred_nat" |
67 less_def: "m < n == (m, n) : trancl pred_nat" |
68 |
68 |
69 le_def: "m \<le> (n::nat) == ~ (n < m)" |
69 le_def: "m \<le> (n::nat) == ~ (n < m)" |
|
70 |
|
71 declare One_nat_def [simp] |
70 |
72 |
71 |
73 |
72 text {* Induction *} |
74 text {* Induction *} |
73 |
75 |
74 theorem nat_induct: "P 0 ==> (!!n. P n ==> P (Suc n)) ==> P n" |
76 theorem nat_induct: "P 0 ==> (!!n. P n ==> P (Suc n)) ==> P n" |