117 val rhss = mk_split_rec_rhs lthy fpTs Cs recs; |
117 val rhss = mk_split_rec_rhs lthy fpTs Cs recs; |
118 in |
118 in |
119 fold_map3 (define_co_rec_as Least_FP Cs) fpTs bs rhss lthy |
119 fold_map3 (define_co_rec_as Least_FP Cs) fpTs bs rhss lthy |
120 end; |
120 end; |
121 |
121 |
122 fun mk_split_rec_thmss ctxt Xs fpTs ctr_Tsss ctrss rec0_thmss (recs as rec1 :: _) rec_defs = |
122 fun mk_split_rec_thmss ctxt Xs ctrXs_Tsss ctrss rec0_thmss (recs as rec1 :: _) rec_defs = |
123 let |
123 let |
124 val f_Ts = binder_fun_types (fastype_of rec1); |
124 val f_Ts = binder_fun_types (fastype_of rec1); |
125 val (fs, _) = mk_Frees "f" f_Ts ctxt; |
125 val (fs, _) = mk_Frees "f" f_Ts ctxt; |
126 val frecs = map (fn recx => Term.list_comb (recx, fs)) recs; |
126 val frecs = map (fn recx => Term.list_comb (recx, fs)) recs; |
127 |
127 |
128 val fpTs_frecs = fpTs ~~ frecs; |
128 val Xs_frecs = Xs ~~ frecs; |
129 val fss = unflat ctrss fs; |
129 val fss = unflat ctrss fs; |
130 |
130 |
131 fun mk_rec_call g n (Type (@{type_name fun}, [dom_T, ran_T])) = |
131 fun mk_rec_call g n (Type (@{type_name fun}, [dom_T, ran_T])) = |
132 Abs (Name.uu, dom_T, mk_rec_call g (n + 1) ran_T) |
132 Abs (Name.uu, dom_T, mk_rec_call g (n + 1) ran_T) |
133 | mk_rec_call g n fpT = |
133 | mk_rec_call g n X = |
134 let |
134 let |
135 val frec = the (AList.lookup (op =) fpTs_frecs fpT); |
135 val frec = the (AList.lookup (op =) Xs_frecs X); |
136 val xg = Term.list_comb (g, map Bound (n - 1 downto 0)); |
136 val xg = Term.list_comb (g, map Bound (n - 1 downto 0)); |
137 in frec $ xg end; |
137 in frec $ xg end; |
138 |
138 |
139 fun mk_rec_arg_arg ctr_T g = |
139 fun mk_rec_arg_arg ctrXs_T g = |
140 g :: (if exists_subtype_in fpTs ctr_T then [mk_rec_call g 0 ctr_T] else []); |
140 g :: (if member (op =) Xs (body_type ctrXs_T) then [mk_rec_call g 0 ctrXs_T] else []); |
141 |
141 |
142 fun mk_goal frec ctr_Ts ctr f = |
142 fun mk_goal frec ctrXs_Ts ctr f = |
143 let |
143 let |
|
144 val ctr_Ts = binder_types (fastype_of ctr); |
144 val (gs, _) = mk_Frees "g" ctr_Ts ctxt; |
145 val (gs, _) = mk_Frees "g" ctr_Ts ctxt; |
145 val gctr = Term.list_comb (ctr, gs); |
146 val gctr = Term.list_comb (ctr, gs); |
146 val fgs = flat_rec_arg_args (map2 mk_rec_arg_arg ctr_Ts gs); |
147 val fgs = flat_rec_arg_args (map2 mk_rec_arg_arg ctrXs_Ts gs); |
147 in |
148 in |
148 fold_rev (fold_rev Logic.all) [fs, gs] |
149 fold_rev (fold_rev Logic.all) [fs, gs] |
149 (mk_Trueprop_eq (frec $ gctr, Term.list_comb (f, fgs))) |
150 (mk_Trueprop_eq (frec $ gctr, Term.list_comb (f, fgs))) |
150 end; |
151 end; |
151 |
152 |
152 val goalss = map4 (map3 o mk_goal) frecs ctr_Tsss ctrss fss; |
153 val goalss = map4 (map3 o mk_goal) frecs ctrXs_Tsss ctrss fss; |
153 |
154 |
154 fun tac ctxt = |
155 fun tac ctxt = |
155 unfold_thms_tac ctxt (@{thms o_apply fst_conv snd_conv} @ rec_defs @ flat rec0_thmss) THEN |
156 unfold_thms_tac ctxt (@{thms o_apply fst_conv snd_conv} @ rec_defs @ flat rec0_thmss) THEN |
156 HEADGOAL (rtac refl); |
157 HEADGOAL (rtac refl); |
157 |
158 |
175 val induct' = repair_induct induct; |
176 val induct' = repair_induct induct; |
176 |
177 |
177 val Cs = map ((fn TVar ((s, _), S) => TFree (s, S)) o body_type o fastype_of) recs0; |
178 val Cs = map ((fn TVar ((s, _), S) => TFree (s, S)) o body_type o fastype_of) recs0; |
178 val recs = map2 (mk_co_rec thy Least_FP Cs) fpTs recs0; |
179 val recs = map2 (mk_co_rec thy Least_FP Cs) fpTs recs0; |
179 val ((recs', rec'_defs), lthy') = define_split_recs fpTs Cs recs lthy |>> split_list; |
180 val ((recs', rec'_defs), lthy') = define_split_recs fpTs Cs recs lthy |>> split_list; |
180 val rec'_thmss = mk_split_rec_thmss lthy' Xs fpTs ctr_Tsss ctrss rec_thmss recs' rec'_defs; |
181 val rec'_thmss = mk_split_rec_thmss lthy' Xs ctrXs_Tsss ctrss rec_thmss recs' rec'_defs; |
181 in |
182 in |
182 ((inducts', induct', recs', rec'_thmss), lthy') |
183 ((inducts', induct', recs', rec'_thmss), lthy') |
183 end; |
184 end; |
184 |
185 |
185 fun reindex_desc desc = |
186 fun reindex_desc desc = |
262 |
263 |
263 val fpTs' = Old_Datatype_Aux.get_rec_types descr; |
264 val fpTs' = Old_Datatype_Aux.get_rec_types descr; |
264 val nn = length fpTs'; |
265 val nn = length fpTs'; |
265 |
266 |
266 val fp_sugars = map (lfp_sugar_of o fst o dest_Type) fpTs'; |
267 val fp_sugars = map (lfp_sugar_of o fst o dest_Type) fpTs'; |
267 val ctr_Tsss = map (map (map dest_dtyp o snd) o #3 o snd) descr; |
268 val ctrXs_Tsss = map (map (map dest_dtyp o snd) o #3 o snd) descr; |
268 val kkssss = |
269 val kkssss = |
269 map (map (map (fn Old_Datatype_Aux.DtRec kk => [kk] | _ => []) o snd) o #3 o snd) descr; |
270 map (map (map (fn Old_Datatype_Aux.DtRec kk => [kk] | _ => []) o snd) o #3 o snd) descr; |
270 |
271 |
271 val callers = map (fn kk => Var ((Name.uu, kk), @{typ "unit => unit"})) (0 upto nn - 1); |
272 val callers = map (fn kk => Var ((Name.uu, kk), @{typ "unit => unit"})) (0 upto nn - 1); |
272 |
273 |
273 fun apply_comps n kk = |
274 fun apply_comps n kk = |
274 mk_partial_compN n (replicate n HOLogic.unitT ---> HOLogic.unitT) (nth callers kk); |
275 mk_partial_compN n (replicate n HOLogic.unitT ---> HOLogic.unitT) (nth callers kk); |
275 |
276 |
276 val callssss = |
277 val callssss = map2 (map2 (map2 (map o apply_comps o num_binder_types))) ctrXs_Tsss kkssss; |
277 map2 (map2 (map2 (fn ctr_T => map (apply_comps (num_binder_types ctr_T))))) ctr_Tsss kkssss; |
|
278 |
278 |
279 val b_names = Name.variant_list [] (map base_name_of_typ fpTs'); |
279 val b_names = Name.variant_list [] (map base_name_of_typ fpTs'); |
280 val compat_b_names = map (prefix compat_N) b_names; |
280 val compat_b_names = map (prefix compat_N) b_names; |
281 val compat_bs = map Binding.name compat_b_names; |
281 val compat_bs = map Binding.name compat_b_names; |
282 |
282 |
285 mutualize_fp_sugars Least_FP cliques compat_bs fpTs' callers callssss fp_sugars lthy |
285 mutualize_fp_sugars Least_FP cliques compat_bs fpTs' callers callssss fp_sugars lthy |
286 else |
286 else |
287 ((fp_sugars, (NONE, NONE)), lthy); |
287 ((fp_sugars, (NONE, NONE)), lthy); |
288 |
288 |
289 fun mk_ctr_of {ctr_sugar = {ctrs, ...}, ...} (Type (_, Ts)) = map (mk_ctr Ts) ctrs; |
289 fun mk_ctr_of {ctr_sugar = {ctrs, ...}, ...} (Type (_, Ts)) = map (mk_ctr Ts) ctrs; |
|
290 val substAT = Term.typ_subst_atomic (var_As ~~ As); |
290 |
291 |
291 val Xs' = map #X fp_sugars'; |
292 val Xs' = map #X fp_sugars'; |
292 val ctr_Tsss' = map (map (binder_types o fastype_of) o #ctrs o #ctr_sugar) fp_sugars'; (*###*) |
293 val ctrXs_Tsss' = map (map (map substAT) o #ctrXs_Tss) fp_sugars'; |
293 val ctrss' = map2 mk_ctr_of fp_sugars' fpTs'; |
294 val ctrss' = map2 mk_ctr_of fp_sugars' fpTs'; |
294 val {common_co_inducts = [induct], ...} :: _ = fp_sugars'; |
295 val {common_co_inducts = [induct], ...} :: _ = fp_sugars'; |
295 val inducts = map (the_single o #co_inducts) fp_sugars'; |
296 val inducts = map (the_single o #co_inducts) fp_sugars'; |
296 val recs = map #co_rec fp_sugars'; |
297 val recs = map #co_rec fp_sugars'; |
297 val rec_thmss = map #co_rec_thms fp_sugars'; |
298 val rec_thmss = map #co_rec_thms fp_sugars'; |
298 |
299 |
299 fun is_nested_rec_type (Type (@{type_name fun}, [_, T])) = member (op =) fpTs' (body_type T) |
300 fun is_nested_rec_type (Type (@{type_name fun}, [_, T])) = member (op =) Xs' (body_type T) |
300 | is_nested_rec_type _ = false; |
301 | is_nested_rec_type _ = false; |
301 |
302 |
302 val ((lfp_sugar_thms'', (inducts', induct', recs', rec'_thmss)), lthy'') = |
303 val ((lfp_sugar_thms'', (inducts', induct', recs', rec'_thmss)), lthy'') = |
303 if nesting_pref = Unfold_Nesting andalso |
304 if nesting_pref = Unfold_Nesting andalso |
304 exists (exists (exists is_nested_rec_type)) ctr_Tsss' then |
305 exists (exists (exists is_nested_rec_type)) ctrXs_Tsss' then |
305 define_split_rec_derive_induct_rec_thms Xs' fpTs' ctr_Tsss' ctrss' inducts induct recs |
306 define_split_rec_derive_induct_rec_thms Xs' fpTs' ctrXs_Tsss' ctrss' inducts induct recs |
306 rec_thmss lthy' |
307 rec_thmss lthy' |
307 |>> `(fn (inducts', induct', _, rec'_thmss) => |
308 |>> `(fn (inducts', induct', _, rec'_thmss) => |
308 SOME ((inducts', induct', mk_induct_attrs ctrss'), (rec'_thmss, []))) |
309 SOME ((inducts', induct', mk_induct_attrs ctrss'), (rec'_thmss, []))) |
309 else |
310 else |
310 ((lfp_sugar_thms', (inducts, induct, recs, rec_thmss)), lthy'); |
311 ((lfp_sugar_thms', (inducts, induct, recs, rec_thmss)), lthy'); |