equal
deleted
inserted
replaced
155 |
155 |
156 (*** nat_rec -- by wf recursion on pred_nat ***) |
156 (*** nat_rec -- by wf recursion on pred_nat ***) |
157 |
157 |
158 (* The unrolling rule for nat_rec *) |
158 (* The unrolling rule for nat_rec *) |
159 goal thy |
159 goal thy |
160 "(%n. nat_rec c d n) = wfrec pred_nat (%f. nat_case ?c (%m. ?d m (f m)))"; |
160 "nat_rec c d = wfrec pred_nat (%f. nat_case c (%m. d m (f m)))"; |
161 by (simp_tac (HOL_ss addsimps [nat_rec_def]) 1); |
161 by (simp_tac (HOL_ss addsimps [nat_rec_def]) 1); |
162 bind_thm("nat_rec_unfold", wf_pred_nat RS |
162 bind_thm("nat_rec_unfold", wf_pred_nat RS |
163 ((result() RS eq_reflection) RS def_wfrec)); |
163 ((result() RS eq_reflection) RS def_wfrec)); |
164 |
164 |
165 (*--------------------------------------------------------------------------- |
165 (*--------------------------------------------------------------------------- |