253 end |
253 end |
254 |
254 |
255 fun mk_partial_rules_mutual lthy inner_cont (m as Mutual {parts, fqgars, ...}) proof = |
255 fun mk_partial_rules_mutual lthy inner_cont (m as Mutual {parts, fqgars, ...}) proof = |
256 let |
256 let |
257 val result = inner_cont proof |
257 val result = inner_cont proof |
258 val FunctionResult {G, R, cases, psimps, simple_pinducts=[simple_pinduct], |
258 val NominalFunctionResult {G, R, cases, psimps, simple_pinducts=[simple_pinduct], |
259 termination, domintros, ...} = result |
259 termination, domintros, eqvts,...} = result |
|
260 |
|
261 (* |
|
262 val _ = tracing ("premutual induct:\n" ^ @{make_string} simple_pinduct) |
|
263 val _ = tracing ("premutual termination:\n" ^ @{make_string} termination) |
|
264 val _ = tracing ("premutual psimps:\n" ^ cat_lines (map @{make_string} psimps)) |
|
265 val _ = tracing ("premutual eqvts:\n" ^ cat_lines (map @{make_string} eqvts)) |
|
266 *) |
260 |
267 |
261 val (all_f_defs, fs) = |
268 val (all_f_defs, fs) = |
262 map (fn MutualPart {f_defthm = SOME f_def, f = SOME f, cargTs, ...} => |
269 map (fn MutualPart {f_defthm = SOME f_def, f = SOME f, cargTs, ...} => |
263 (mk_applied_form lthy cargTs (Thm.symmetric f_def), f)) |
270 (mk_applied_form lthy cargTs (Thm.symmetric f_def), f)) |
264 parts |
271 parts |
273 val rew_ss = HOL_basic_ss addsimps all_f_defs |
280 val rew_ss = HOL_basic_ss addsimps all_f_defs |
274 val mpsimps = map2 mk_mpsimp fqgars psimps |
281 val mpsimps = map2 mk_mpsimp fqgars psimps |
275 val minducts = mutual_induct_rules lthy simple_pinduct all_f_defs m |
282 val minducts = mutual_induct_rules lthy simple_pinduct all_f_defs m |
276 val mtermination = full_simplify rew_ss termination |
283 val mtermination = full_simplify rew_ss termination |
277 val mdomintros = Option.map (map (full_simplify rew_ss)) domintros |
284 val mdomintros = Option.map (map (full_simplify rew_ss)) domintros |
278 in |
285 |
279 FunctionResult { fs=fs, G=G, R=R, |
286 (* |
|
287 val _ = tracing ("postmutual psimps:\n" ^ cat_lines (map @{make_string} mpsimps)) |
|
288 val _ = tracing ("postmutual induct:\n" ^ cat_lines (map @{make_string} minducts)) |
|
289 val _ = tracing ("postmutual termination:\n" ^ @{make_string} mtermination) |
|
290 *) |
|
291 in |
|
292 NominalFunctionResult { fs=fs, G=G, R=R, |
280 psimps=mpsimps, simple_pinducts=minducts, |
293 psimps=mpsimps, simple_pinducts=minducts, |
281 cases=cases, termination=mtermination, |
294 cases=cases, termination=mtermination, |
282 domintros=mdomintros} |
295 domintros=mdomintros, eqvts=eqvts } |
283 end |
296 end |
284 |
297 |
285 (* nominal *) |
298 (* nominal *) |
286 fun prepare_nominal_function_mutual config defname fixes eqss lthy = |
299 fun prepare_nominal_function_mutual config defname fixes eqss lthy = |
287 let |
300 let |