270 (fv_c $ list_comb (c, args), mk_union (map fv_arg (dts ~~ args ~~ arg_nos)))) |
270 (fv_c $ list_comb (c, args), mk_union (map fv_arg (dts ~~ args ~~ arg_nos)))) |
271 val alpha_rhs = |
271 val alpha_rhs = |
272 HOLogic.mk_Trueprop (alpha $ (list_comb (c, args)) $ (list_comb (c, args2))); |
272 HOLogic.mk_Trueprop (alpha $ (list_comb (c, args)) $ (list_comb (c, args2))); |
273 fun alpha_arg ((dt, arg_no), (arg, arg2)) = |
273 fun alpha_arg ((dt, arg_no), (arg, arg2)) = |
274 let |
274 let |
275 val relevant = filter (fn ((_, i, j), _) => i = arg_no orelse j = arg_no) bind_pis; |
275 val rel_in_simp_binds = filter (fn ((NONE, i, _), _) => i = arg_no | _ => false) bind_pis; |
|
276 val rel_in_comp_binds = filter (fn ((SOME _, i, _), _) => i = arg_no | _ => false) bind_pis; |
|
277 val rel_has_binds = filter (fn ((SOME _, _, j), _) => j = arg_no | _ => false) bind_pis; |
276 in |
278 in |
277 if relevant = [] then ( |
279 case (rel_in_simp_binds, rel_in_comp_binds, rel_has_binds) of |
278 if is_rec_type dt then (nth alpha_frees (body_index dt) $ arg $ arg2) |
280 ([], [], []) => |
279 else (HOLogic.mk_eq (arg, arg2))) |
281 if is_rec_type dt then (nth alpha_frees (body_index dt) $ arg $ arg2) |
280 else |
282 else (HOLogic.mk_eq (arg, arg2)) |
281 if is_rec_type dt then let |
283 (* TODO: if more then check and accept *) |
282 (* THE HARD CASE *) |
284 | (_, [], []) => @{term True} |
|
285 | ([], [(((SOME (bn, _)), _, _), pi)], []) => |
|
286 nth alpha_bnfrees (find_index (fn (b, _, _) => b = bn) bns) $ pi $ arg $ arg2 |
|
287 | ([], [], relevant) => |
|
288 let |
283 val (rbinds, rpis) = split_list relevant |
289 val (rbinds, rpis) = split_list relevant |
284 val lhs_binds = fv_binds args rbinds |
290 val lhs_binds = fv_binds args rbinds |
285 val lhs = mk_pair (lhs_binds, arg); |
291 val lhs = mk_pair (lhs_binds, arg); |
286 val rhs_binds = fv_binds args2 rbinds; |
292 val rhs_binds = fv_binds args2 rbinds; |
287 val rhs = mk_pair (rhs_binds, arg2); |
293 val rhs = mk_pair (rhs_binds, arg2); |
291 val alpha_gen_pre = Const (@{const_name alpha_gen}, dummyT) $ lhs $ alpha $ fv $ pi $ rhs; |
297 val alpha_gen_pre = Const (@{const_name alpha_gen}, dummyT) $ lhs $ alpha $ fv $ pi $ rhs; |
292 val alpha_gen = Syntax.check_term lthy alpha_gen_pre |
298 val alpha_gen = Syntax.check_term lthy alpha_gen_pre |
293 (* val pi_supps = map ((curry op $) @{term "supp :: perm \<Rightarrow> atom set"}) rpis; |
299 (* val pi_supps = map ((curry op $) @{term "supp :: perm \<Rightarrow> atom set"}) rpis; |
294 val pi_supps_eq = HOLogic.mk_eq (mk_inter pi_supps, @{term "{} :: atom set"}) *) |
300 val pi_supps_eq = HOLogic.mk_eq (mk_inter pi_supps, @{term "{} :: atom set"}) *) |
295 in |
301 in |
296 (*if length pi_supps > 1 then HOLogic.mk_conj (alpha_gen, pi_supps_eq) else*) |
302 (* if length pi_supps > 1 then HOLogic.mk_conj (alpha_gen, pi_supps_eq) else*) |
297 alpha_gen |
303 alpha_gen |
298 (* TODO Add some test that is makes sense *) |
304 end |
299 end else @{term "True"} |
|
300 end |
305 end |
301 val alphas = map alpha_arg (dts ~~ arg_nos ~~ (args ~~ args2)) |
306 val alphas = map alpha_arg (dts ~~ arg_nos ~~ (args ~~ args2)) |
302 val alpha_lhss = mk_conjl alphas |
307 val alpha_lhss = mk_conjl alphas |
303 val alpha_lhss_ex = |
308 val alpha_lhss_ex = |
304 fold (fn pi_str => fn t => HOLogic.mk_exists (pi_str, @{typ perm}, t)) pi_strs alpha_lhss |
309 fold (fn pi_str => fn t => HOLogic.mk_exists (pi_str, @{typ perm}, t)) pi_strs alpha_lhss |