144 |
144 |
145 (*Treatment of all parts*) |
145 (*Treatment of all parts*) |
146 val (_, case_lists) = List.foldr add_case_list (1,[]) con_ty_lists; |
146 val (_, case_lists) = List.foldr add_case_list (1,[]) con_ty_lists; |
147 |
147 |
148 (*extract the types of all the variables*) |
148 (*extract the types of all the variables*) |
149 val case_typ = List.concat (map (map (#2 o #1)) con_ty_lists) ---> @{typ "i => i"}; |
149 val case_typ = maps (map (#2 o #1)) con_ty_lists ---> @{typ "i => i"}; |
150 |
150 |
151 val case_base_name = big_rec_base_name ^ "_case"; |
151 val case_base_name = big_rec_base_name ^ "_case"; |
152 val case_name = full_name case_base_name; |
152 val case_name = full_name case_base_name; |
153 |
153 |
154 (*The list of all the function variables*) |
154 (*The list of all the function variables*) |
155 val case_args = List.concat (map (map #1) case_lists); |
155 val case_args = maps (map #1) case_lists; |
156 |
156 |
157 val case_const = Const (case_name, case_typ); |
157 val case_const = Const (case_name, case_typ); |
158 val case_tm = list_comb (case_const, case_args); |
158 val case_tm = list_comb (case_const, case_args); |
159 |
159 |
160 val case_def = PrimitiveDefs.mk_defpair |
160 val case_def = PrimitiveDefs.mk_defpair |
216 |
216 |
217 (*Treatment of all parts*) |
217 (*Treatment of all parts*) |
218 val (_, recursor_lists) = List.foldr add_case_list (1,[]) rec_ty_lists; |
218 val (_, recursor_lists) = List.foldr add_case_list (1,[]) rec_ty_lists; |
219 |
219 |
220 (*extract the types of all the variables*) |
220 (*extract the types of all the variables*) |
221 val recursor_typ = List.concat (map (map (#2 o #1)) rec_ty_lists) ---> @{typ "i => i"}; |
221 val recursor_typ = maps (map (#2 o #1)) rec_ty_lists ---> @{typ "i => i"}; |
222 |
222 |
223 val recursor_base_name = big_rec_base_name ^ "_rec"; |
223 val recursor_base_name = big_rec_base_name ^ "_rec"; |
224 val recursor_name = full_name recursor_base_name; |
224 val recursor_name = full_name recursor_base_name; |
225 |
225 |
226 (*The list of all the function variables*) |
226 (*The list of all the function variables*) |
227 val recursor_args = List.concat (map (map #1) recursor_lists); |
227 val recursor_args = maps (map #1) recursor_lists; |
228 |
228 |
229 val recursor_tm = |
229 val recursor_tm = |
230 list_comb (Const (recursor_name, recursor_typ), recursor_args); |
230 list_comb (Const (recursor_name, recursor_typ), recursor_args); |
231 |
231 |
232 val recursor_cases = map call_recursor |
232 val recursor_cases = map call_recursor (flat case_lists ~~ flat recursor_lists); |
233 (List.concat case_lists ~~ List.concat recursor_lists) |
|
234 |
233 |
235 val recursor_def = |
234 val recursor_def = |
236 PrimitiveDefs.mk_defpair |
235 PrimitiveDefs.mk_defpair |
237 (recursor_tm, |
236 (recursor_tm, |
238 @{const Univ.Vrecursor} $ |
237 @{const Univ.Vrecursor} $ |
250 else thy; |
249 else thy; |
251 |
250 |
252 val (con_defs, thy0) = thy_path |
251 val (con_defs, thy0) = thy_path |
253 |> Sign.add_consts_i |
252 |> Sign.add_consts_i |
254 (map (fn (c, T, mx) => (Binding.name c, T, mx)) |
253 (map (fn (c, T, mx) => (Binding.name c, T, mx)) |
255 ((case_base_name, case_typ, NoSyn) :: map #1 (List.concat con_ty_lists))) |
254 ((case_base_name, case_typ, NoSyn) :: map #1 (flat con_ty_lists))) |
256 |> PureThy.add_defs false |
255 |> PureThy.add_defs false |
257 (map (Thm.no_attributes o apfst Binding.name) |
256 (map (Thm.no_attributes o apfst Binding.name) |
258 (case_def :: |
257 (case_def :: |
259 List.concat (ListPair.map mk_con_defs |
258 flat (ListPair.map mk_con_defs (1 upto npart, con_ty_lists)))) |
260 (1 upto npart, con_ty_lists)))) |
|
261 ||> add_recursor |
259 ||> add_recursor |
262 ||> Sign.parent_path |
260 ||> Sign.parent_path |
263 |
261 |
264 val intr_names = map (Binding.name o #2) (List.concat con_ty_lists); |
262 val intr_names = map (Binding.name o #2) (flat con_ty_lists); |
265 val (thy1, ind_result) = |
263 val (thy1, ind_result) = |
266 thy0 |> Ind_Package.add_inductive_i |
264 thy0 |> Ind_Package.add_inductive_i |
267 false (rec_tms, dom_sum) (map Thm.no_attributes (intr_names ~~ intr_tms)) |
265 false (rec_tms, dom_sum) (map Thm.no_attributes (intr_names ~~ intr_tms)) |
268 (monos, con_defs, type_intrs @ Datatype_Arg.intrs, type_elims @ Datatype_Arg.elims); |
266 (monos, con_defs, type_intrs @ Datatype_Arg.intrs, type_elims @ Datatype_Arg.elims); |
269 |
267 |
294 rtac case_trans 1, |
292 rtac case_trans 1, |
295 REPEAT (resolve_tac [refl, split_trans, Su.case_inl RS trans, Su.case_inr RS trans] 1)]); |
293 REPEAT (resolve_tac [refl, split_trans, Su.case_inl RS trans, Su.case_inr RS trans] 1)]); |
296 |
294 |
297 val free_iffs = map standard (con_defs RL [@{thm def_swap_iff}]); |
295 val free_iffs = map standard (con_defs RL [@{thm def_swap_iff}]); |
298 |
296 |
299 val case_eqns = |
297 val case_eqns = map prove_case_eqn (flat con_ty_lists ~~ case_args ~~ tl con_defs); |
300 map prove_case_eqn |
|
301 (List.concat con_ty_lists ~~ case_args ~~ tl con_defs); |
|
302 |
298 |
303 (*** Prove the recursor theorems ***) |
299 (*** Prove the recursor theorems ***) |
304 |
300 |
305 val recursor_eqns = case try (Drule.get_def thy1) recursor_base_name of |
301 val recursor_eqns = case try (Drule.get_def thy1) recursor_base_name of |
306 NONE => (writeln " [ No recursion operator ]"; |
302 NONE => (writeln " [ No recursion operator ]"; |
334 (fn _ => EVERY |
330 (fn _ => EVERY |
335 [rtac recursor_trans 1, |
331 [rtac recursor_trans 1, |
336 simp_tac (rank_ss addsimps case_eqns) 1, |
332 simp_tac (rank_ss addsimps case_eqns) 1, |
337 IF_UNSOLVED (simp_tac (rank_ss addsimps tl con_defs) 1)]); |
333 IF_UNSOLVED (simp_tac (rank_ss addsimps tl con_defs) 1)]); |
338 in |
334 in |
339 map prove_recursor_eqn (List.concat con_ty_lists ~~ recursor_cases) |
335 map prove_recursor_eqn (flat con_ty_lists ~~ recursor_cases) |
340 end |
336 end |
341 |
337 |
342 val constructors = |
338 val constructors = |
343 map (head_of o #1 o Logic.dest_equals o #prop o rep_thm) (tl con_defs); |
339 map (head_of o #1 o Logic.dest_equals o #prop o rep_thm) (tl con_defs); |
344 |
340 |