251 end |
251 end |
252 |
252 |
253 fun mk_partial_rules_mutual lthy inner_cont (m as Mutual {parts, fqgars, ...}) proof = |
253 fun mk_partial_rules_mutual lthy inner_cont (m as Mutual {parts, fqgars, ...}) proof = |
254 let |
254 let |
255 val result = inner_cont proof |
255 val result = inner_cont proof |
256 val FunctionResult {G, R, cases, psimps, trsimps, simple_pinducts=[simple_pinduct], |
256 val FunctionResult {G, R, cases, psimps, simple_pinducts=[simple_pinduct], |
257 termination, domintros, ...} = result |
257 termination, domintros, ...} = result |
258 |
258 |
259 val (all_f_defs, fs) = |
259 val (all_f_defs, fs) = |
260 map (fn MutualPart {f_defthm = SOME f_def, f = SOME f, cargTs, ...} => |
260 map (fn MutualPart {f_defthm = SOME f_def, f = SOME f, cargTs, ...} => |
261 (mk_applied_form lthy cargTs (Thm.symmetric f_def), f)) |
261 (mk_applied_form lthy cargTs (Thm.symmetric f_def), f)) |
268 fun mk_mpsimp fqgar sum_psimp = |
268 fun mk_mpsimp fqgar sum_psimp = |
269 in_context lthy fqgar (recover_mutual_psimp all_orig_fdefs parts) sum_psimp |
269 in_context lthy fqgar (recover_mutual_psimp all_orig_fdefs parts) sum_psimp |
270 |
270 |
271 val rew_ss = HOL_basic_ss addsimps all_f_defs |
271 val rew_ss = HOL_basic_ss addsimps all_f_defs |
272 val mpsimps = map2 mk_mpsimp fqgars psimps |
272 val mpsimps = map2 mk_mpsimp fqgars psimps |
273 val mtrsimps = Option.map (map2 mk_mpsimp fqgars) trsimps |
|
274 val minducts = mutual_induct_rules lthy simple_pinduct all_f_defs m |
273 val minducts = mutual_induct_rules lthy simple_pinduct all_f_defs m |
275 val mtermination = full_simplify rew_ss termination |
274 val mtermination = full_simplify rew_ss termination |
276 val mdomintros = Option.map (map (full_simplify rew_ss)) domintros |
275 val mdomintros = Option.map (map (full_simplify rew_ss)) domintros |
277 in |
276 in |
278 FunctionResult { fs=fs, G=G, R=R, |
277 FunctionResult { fs=fs, G=G, R=R, |
279 psimps=mpsimps, simple_pinducts=minducts, |
278 psimps=mpsimps, simple_pinducts=minducts, |
280 cases=cases, termination=mtermination, |
279 cases=cases, termination=mtermination, |
281 domintros=mdomintros, trsimps=mtrsimps} |
280 domintros=mdomintros} |
282 end |
281 end |
283 |
282 |
284 (* nominal *) |
283 (* nominal *) |
285 fun prepare_nominal_function_mutual config defname fixes eqss lthy = |
284 fun prepare_nominal_function_mutual config defname fixes eqss lthy = |
286 let |
285 let |