equal
deleted
inserted
replaced
109 by (rule inj_Suc [THEN inj_eq]) |
109 by (rule inj_Suc [THEN inj_eq]) |
110 |
110 |
111 lemma nat_not_singleton: "(\<forall>x. x = (0::nat)) = False" |
111 lemma nat_not_singleton: "(\<forall>x. x = (0::nat)) = False" |
112 by auto |
112 by auto |
113 |
113 |
114 |
114 text {* size of a datatype value *} |
115 text {* size of a datatype value; overloaded *} |
115 |
116 consts size :: "'a => nat" |
116 class size = |
|
117 fixes size :: "'a \<Rightarrow> nat" |
117 |
118 |
118 text {* @{typ nat} is a datatype *} |
119 text {* @{typ nat} is a datatype *} |
119 |
120 |
120 rep_datatype nat |
121 rep_datatype nat |
121 distinct Suc_not_Zero Zero_not_Suc |
122 distinct Suc_not_Zero Zero_not_Suc |
122 inject Suc_Suc_eq |
123 inject Suc_Suc_eq |
123 induction nat_induct [case_names 0 Suc] |
124 induction nat_induct |
|
125 |
|
126 declare nat.induct [case_names 0 Suc, induct type: nat] |
|
127 declare nat.exhaust [case_names 0 Suc, cases type: nat] |
124 |
128 |
125 lemma n_not_Suc_n: "n \<noteq> Suc n" |
129 lemma n_not_Suc_n: "n \<noteq> Suc n" |
126 by (induct n) simp_all |
130 by (induct n) simp_all |
127 |
131 |
128 lemma Suc_n_not_n: "Suc t \<noteq> t" |
132 lemma Suc_n_not_n: "Suc t \<noteq> t" |
470 by auto |
474 by auto |
471 |
475 |
472 |
476 |
473 subsection {* Arithmetic operators *} |
477 subsection {* Arithmetic operators *} |
474 |
478 |
475 axclass power < type |
479 class power = |
476 |
480 fixes power :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infixr "\<^loc>^" 80) |
477 consts |
|
478 power :: "('a::power) => nat => 'a" (infixr "^" 80) |
|
479 |
|
480 |
481 |
481 text {* arithmetic operators @{text "+ -"} and @{text "*"} *} |
482 text {* arithmetic operators @{text "+ -"} and @{text "*"} *} |
482 |
483 |
483 instance nat :: "{plus, minus, times, power}" .. |
484 instance nat :: "{plus, minus, times, power}" .. |
484 |
485 |