48 open BNF_FP_Def_Sugar |
48 open BNF_FP_Def_Sugar |
49 open BNF_FP_N2M_Sugar |
49 open BNF_FP_N2M_Sugar |
50 open BNF_LFP |
50 open BNF_LFP |
51 |
51 |
52 val compat_N = "compat_"; |
52 val compat_N = "compat_"; |
53 val rec_fun_N = "rec_fun_"; |
53 val rec_split_N = "rec_split_"; |
54 |
54 |
55 datatype nesting_preference = Keep_Nesting | Unfold_Nesting; |
55 datatype nesting_preference = Keep_Nesting | Unfold_Nesting; |
56 |
56 |
57 fun mk_fun_rec_rhs ctxt fpTs Cs (recs as rec1 :: _) = |
57 fun mk_split_rec_rhs ctxt fpTs Cs (recs as rec1 :: _) = |
58 let |
58 let |
59 fun repair_rec_arg_args [] [] = [] |
59 fun repair_rec_arg_args [] [] = [] |
60 | repair_rec_arg_args ((g_T as Type (@{type_name fun}, _)) :: g_Ts) (g :: gs) = |
60 | repair_rec_arg_args ((g_T as Type (@{type_name fun}, _)) :: g_Ts) (g :: gs) = |
61 let |
61 let |
62 val (x_Ts, body_T) = strip_type g_T; |
62 val (x_Ts, body_T) = strip_type g_T; |
103 |> Syntax.check_term ctxt; |
103 |> Syntax.check_term ctxt; |
104 in |
104 in |
105 map mk_rec' recs |
105 map mk_rec' recs |
106 end; |
106 end; |
107 |
107 |
108 fun define_fun_recs fpTs Cs recs lthy = |
108 fun define_split_recs fpTs Cs recs lthy = |
109 let |
109 let |
110 val b_names = Name.variant_list [] (map base_name_of_typ fpTs); |
110 val b_names = Name.variant_list [] (map base_name_of_typ fpTs); |
111 |
111 |
112 fun mk_binding b_name = |
112 fun mk_binding b_name = |
113 Binding.qualify true (compat_N ^ b_name) |
113 Binding.qualify true (compat_N ^ b_name) |
114 (Binding.prefix_name rec_fun_N (Binding.name b_name)); |
114 (Binding.prefix_name rec_split_N (Binding.name b_name)); |
115 |
115 |
116 val bs = map mk_binding b_names; |
116 val bs = map mk_binding b_names; |
117 val rhss = mk_fun_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_fun_rec_thmss ctxt rec0_thmss (recs as rec1 :: _) rec_defs = |
122 fun mk_split_rec_thmss ctxt 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 |
168 |> Thm.close_derivation; |
168 |> Thm.close_derivation; |
169 in |
169 in |
170 map (map prove) goalss |
170 map (map prove) goalss |
171 end; |
171 end; |
172 |
172 |
173 fun define_fun_rec_derive_thms induct inducts recs0 rec_thmss fpTs lthy = |
173 fun define_split_rec_derive_induct_rec_thms induct inducts recs0 rec_thmss fpTs lthy = |
174 let |
174 let |
175 val thy = Proof_Context.theory_of lthy; |
175 val thy = Proof_Context.theory_of lthy; |
176 |
176 |
177 (* imperfect: will not yield the expected theorem for functions taking a large number of |
177 (* imperfect: will not yield the expected theorem for functions taking a large number of |
178 arguments *) |
178 arguments *) |
181 val induct' = repair_induct induct; |
181 val induct' = repair_induct induct; |
182 val inducts' = map repair_induct inducts; |
182 val inducts' = map repair_induct inducts; |
183 |
183 |
184 val Cs = map ((fn TVar ((s, _), S) => TFree (s, S)) o body_type o fastype_of) recs0; |
184 val Cs = map ((fn TVar ((s, _), S) => TFree (s, S)) o body_type o fastype_of) recs0; |
185 val recs = map2 (mk_co_rec thy Least_FP Cs) fpTs recs0; |
185 val recs = map2 (mk_co_rec thy Least_FP Cs) fpTs recs0; |
186 val ((recs', rec'_defs), lthy') = define_fun_recs fpTs Cs recs lthy |>> split_list; |
186 val ((recs', rec'_defs), lthy') = define_split_recs fpTs Cs recs lthy |>> split_list; |
187 val rec'_thmss = mk_fun_rec_thmss lthy' rec_thmss recs' rec'_defs; |
187 val rec'_thmss = mk_split_rec_thmss lthy' rec_thmss recs' rec'_defs; |
188 in |
188 in |
189 ((induct', inducts', recs', rec'_thmss), lthy') |
189 ((induct', inducts', recs', rec'_thmss), lthy') |
190 end; |
190 end; |
191 |
191 |
192 fun reindex_desc desc = |
192 fun reindex_desc desc = |
303 | is_nested_rec_type _ = false; |
303 | is_nested_rec_type _ = false; |
304 |
304 |
305 val ((induct', inducts', recs', rec'_thmss), lthy'') = |
305 val ((induct', inducts', recs', rec'_thmss), lthy'') = |
306 if nesting_pref = Unfold_Nesting andalso |
306 if nesting_pref = Unfold_Nesting andalso |
307 exists (exists (exists is_nested_rec_type)) ctr_Tsss then |
307 exists (exists (exists is_nested_rec_type)) ctr_Tsss then |
308 define_fun_rec_derive_thms induct inducts recs rec_thmss fpTs' lthy' |
308 define_split_rec_derive_induct_rec_thms induct inducts recs rec_thmss fpTs' lthy' |
309 else |
309 else |
310 ((induct, inducts, recs, rec_thmss), lthy'); |
310 ((induct, inducts, recs, rec_thmss), lthy'); |
311 |
311 |
312 val rec'_names = map (fst o dest_Const) recs'; |
312 val rec'_names = map (fst o dest_Const) recs'; |
313 val rec'_thms = flat rec'_thmss; |
313 val rec'_thms = flat rec'_thmss; |