302 (ListPair.map (distinct c) ((map #1 cs),leqs)) @ |
302 (ListPair.map (distinct c) ((map #1 cs),leqs)) @ |
303 distincts cs; |
303 distincts cs; |
304 in map standard (distincts (cons~~distincts_le)) end; |
304 in map standard (distincts (cons~~distincts_le)) end; |
305 |
305 |
306 local |
306 local |
307 fun pgterm rel con args = let |
307 fun pgterm rel con args = |
308 fun append s = upd_vname(fn v => v^s); |
308 let |
309 val (largs,rargs) = (args, map (append "'") args); |
309 fun append s = upd_vname(fn v => v^s); |
310 in pg [] (mk_trp (rel(con_app con largs,con_app con rargs)) ===> |
310 val (largs,rargs) = (args, map (append "'") args); |
311 lift_defined %: ((nonlazy largs),lift_defined %: ((nonlazy rargs), |
311 val concl = mk_trp (foldr' mk_conj (ListPair.map rel (map %# largs, map %# rargs))); |
312 mk_trp (foldr' mk_conj |
312 val prem = mk_trp (rel(con_app con largs,con_app con rargs)); |
313 (ListPair.map rel |
313 val prop = prem ===> lift_defined %: (nonlazy largs, concl); |
314 (map %# largs, map %# rargs)))))) end; |
314 in pg con_appls prop end; |
315 val cons' = List.filter (fn (_,args) => args<>[]) cons; |
315 val cons' = List.filter (fn (_,args) => args<>[]) cons; |
316 in |
316 in |
317 val inverts = map (fn (con,args) => |
317 val inverts = |
318 pgterm (op <<) con args (List.concat(map (fn arg => [ |
318 let |
319 TRY(rtac conjI 1), |
319 val abs_less = ax_abs_iso RS (allI RS injection_less) RS iffD1; |
320 dres_inst_tac [("f",sel_of arg)] monofun_cfun_arg 1, |
320 val simps = [up_less, spair_less]; |
321 asm_full_simp_tac (HOLCF_ss addsimps sel_apps) 1] |
321 val tacs = [ |
322 ) args))) cons'; |
322 dtac abs_less 1, |
323 val injects = map (fn ((con,args),inv_thm) => |
323 REPEAT (dresolve_tac [sinl_less RS iffD1, sinr_less RS iffD1] 1), |
324 pgterm (op ===) con args [ |
324 asm_full_simp_tac (HOLCF_ss addsimps simps) 1]; |
325 etac (antisym_less_inverse RS conjE) 1, |
325 in map (fn (con,args) => pgterm (op <<) con args tacs) cons' end; |
326 dtac inv_thm 1, REPEAT(atac 1), |
326 val injects = |
327 dtac inv_thm 1, REPEAT(atac 1), |
327 let |
328 TRY(safe_tac HOL_cs), |
328 val abs_eq = ax_abs_iso RS (allI RS injection_eq) RS iffD1; |
329 REPEAT(rtac antisym_less 1 ORELSE atac 1)] ) |
329 val simps = [up_eq, spair_eq]; |
330 (cons'~~inverts); |
330 val tacs = [ |
|
331 dtac abs_eq 1, |
|
332 REPEAT (dresolve_tac [sinl_inject, sinr_inject] 1), |
|
333 asm_full_simp_tac (HOLCF_ss addsimps simps) 1]; |
|
334 in map (fn (con,args) => pgterm (op ===) con args tacs) cons' end; |
331 end; |
335 end; |
332 |
336 |
333 (* ----- theorems concerning one induction step ----------------------------- *) |
337 (* ----- theorems concerning one induction step ----------------------------- *) |
334 |
338 |
335 val copy_strict = pg[ax_copy_def](mk_trp(strict(dc_copy`%"f"))) [ |
339 val copy_strict = pg[ax_copy_def](mk_trp(strict(dc_copy`%"f"))) [ |