equal
deleted
inserted
replaced
66 Zero_nat_def: "0 == Abs_Nat Zero_Rep" |
66 Zero_nat_def: "0 == Abs_Nat Zero_Rep" |
67 One_nat_def [simp]: "1 == Suc 0" |
67 One_nat_def [simp]: "1 == Suc 0" |
68 less_def: "m < n == (m, n) : pred_nat^+" |
68 less_def: "m < n == (m, n) : pred_nat^+" |
69 le_def: "m \<le> (n::nat) == ~ (n < m)" .. |
69 le_def: "m \<le> (n::nat) == ~ (n < m)" .. |
70 |
70 |
71 lemmas [code func del] = less_def le_def |
71 lemmas [code func del] = Zero_nat_def One_nat_def less_def le_def |
72 |
72 |
73 text {* Induction *} |
73 text {* Induction *} |
74 |
74 |
75 theorem nat_induct: "P 0 ==> (!!n. P n ==> P (Suc n)) ==> P n" |
75 theorem nat_induct: "P 0 ==> (!!n. P n ==> P (Suc n)) ==> P n" |
76 apply (unfold Zero_nat_def Suc_def) |
76 apply (unfold Zero_nat_def Suc_def) |
112 text {* size of a datatype value *} |
112 text {* size of a datatype value *} |
113 |
113 |
114 class size = type + |
114 class size = type + |
115 fixes size :: "'a \<Rightarrow> nat" |
115 fixes size :: "'a \<Rightarrow> nat" |
116 |
116 |
117 text {* @{typ nat} is a datatype *} |
117 text {* now we are ready to re-invent primitive types |
|
118 -- dependency on class size is hardwired into datatype package *} |
|
119 |
|
120 rep_datatype bool |
|
121 distinct True_not_False False_not_True |
|
122 induction bool_induct |
|
123 |
|
124 rep_datatype unit |
|
125 induction unit_induct |
|
126 |
|
127 rep_datatype prod |
|
128 inject Pair_eq |
|
129 induction prod_induct |
|
130 |
|
131 rep_datatype sum |
|
132 distinct Inl_not_Inr Inr_not_Inl |
|
133 inject Inl_eq Inr_eq |
|
134 induction sum_induct |
118 |
135 |
119 rep_datatype nat |
136 rep_datatype nat |
120 distinct Suc_not_Zero Zero_not_Suc |
137 distinct Suc_not_Zero Zero_not_Suc |
121 inject Suc_Suc_eq |
138 inject Suc_Suc_eq |
122 induction nat_induct |
139 induction nat_induct |
127 lemmas nat_rec_0 = nat.recs(1) |
144 lemmas nat_rec_0 = nat.recs(1) |
128 and nat_rec_Suc = nat.recs(2) |
145 and nat_rec_Suc = nat.recs(2) |
129 |
146 |
130 lemmas nat_case_0 = nat.cases(1) |
147 lemmas nat_case_0 = nat.cases(1) |
131 and nat_case_Suc = nat.cases(2) |
148 and nat_case_Suc = nat.cases(2) |
132 |
|
133 |
149 |
134 lemma n_not_Suc_n: "n \<noteq> Suc n" |
150 lemma n_not_Suc_n: "n \<noteq> Suc n" |
135 by (induct n) simp_all |
151 by (induct n) simp_all |
136 |
152 |
137 lemma Suc_n_not_n: "Suc t \<noteq> t" |
153 lemma Suc_n_not_n: "Suc t \<noteq> t" |