273 rtac swap3 1, |
273 rtac swap3 1, |
274 eres_inst_tac[("fo",dis_name con1)] monofun_cfun_arg 1] |
274 eres_inst_tac[("fo",dis_name con1)] monofun_cfun_arg 1] |
275 @map(case_UU_tac (con_stricts @ dis_rews)1)(nonlazy args2) |
275 @map(case_UU_tac (con_stricts @ dis_rews)1)(nonlazy args2) |
276 @[asm_simp_tac (HOLCF_ss addsimps dis_rews) 1]); |
276 @[asm_simp_tac (HOLCF_ss addsimps dis_rews) 1]); |
277 fun distinct (con1,args1) (con2,args2) = |
277 fun distinct (con1,args1) (con2,args2) = |
278 let val arg1 = (con1, args1); |
278 let val arg1 = (con1, args1) |
279 val arg2 = (con2, (map (fn (arg,vn) => upd_vname (K vn) arg) |
279 val arg2 = (con2, |
280 (args2~~variantlist(map vname args2,map vname args1)))); |
280 ListPair.map (fn (arg,vn) => upd_vname (K vn) arg) |
|
281 (args2, variantlist(map vname args2,map vname args1))) |
281 in [dist arg1 arg2, dist arg2 arg1] end; |
282 in [dist arg1 arg2, dist arg2 arg1] end; |
282 fun distincts [] = [] |
283 fun distincts [] = [] |
283 | distincts (c::cs) = (map (distinct c) cs) :: distincts cs; |
284 | distincts (c::cs) = (map (distinct c) cs) :: distincts cs; |
284 in distincts cons end; |
285 in distincts cons end; |
285 val dists_le = flat (flat distincts_le); |
286 val dists_le = flat (flat distincts_le); |
289 val (eq1,eq2) = (le1 RS dist_eqI, le2 RS dist_eqI) in |
290 val (eq1,eq2) = (le1 RS dist_eqI, le2 RS dist_eqI) in |
290 if nonlazy args1 = [] then [eq1, eq1 RS not_sym] else |
291 if nonlazy args1 = [] then [eq1, eq1 RS not_sym] else |
291 if nonlazy args2 = [] then [eq2, eq2 RS not_sym] else |
292 if nonlazy args2 = [] then [eq2, eq2 RS not_sym] else |
292 [eq1, eq2] end; |
293 [eq1, eq2] end; |
293 fun distincts [] = [] |
294 fun distincts [] = [] |
294 | distincts ((c,leqs)::cs) = flat(map (distinct c) ((map fst cs)~~leqs)) @ |
295 | distincts ((c,leqs)::cs) = List_.concat |
295 distincts cs; |
296 (ListPair.map (distinct c) ((map #1 cs),leqs)) @ |
|
297 distincts cs; |
296 in distincts (cons~~distincts_le) end; |
298 in distincts (cons~~distincts_le) end; |
297 |
299 |
298 local |
300 local |
299 fun pgterm rel con args = let |
301 fun pgterm rel con args = let |
300 fun append s = upd_vname(fn v => v^s); |
302 fun append s = upd_vname(fn v => v^s); |
301 val (largs,rargs) = (args, map (append "'") args); |
303 val (largs,rargs) = (args, map (append "'") args); |
302 in pg [] (mk_trp (rel(con_app con largs,con_app con rargs)) ===> |
304 in pg [] (mk_trp (rel(con_app con largs,con_app con rargs)) ===> |
303 lift_defined % ((nonlazy largs),lift_defined % ((nonlazy rargs), |
305 lift_defined % ((nonlazy largs),lift_defined % ((nonlazy rargs), |
304 mk_trp (foldr' mk_conj |
306 mk_trp (foldr' mk_conj |
305 (map rel (map %# largs ~~ map %# rargs)))))) end; |
307 (ListPair.map rel |
|
308 (map %# largs, map %# rargs)))))) end; |
306 val cons' = filter (fn (_,args) => args<>[]) cons; |
309 val cons' = filter (fn (_,args) => args<>[]) cons; |
307 in |
310 in |
308 val inverts = map (fn (con,args) => |
311 val inverts = map (fn (con,args) => |
309 pgterm (op <<) con args (flat(map (fn arg => [ |
312 pgterm (op <<) con args (flat(map (fn arg => [ |
310 TRY(rtac conjI 1), |
313 TRY(rtac conjI 1), |