137 let val ty1 = fastype_of fst |
137 let val ty1 = fastype_of fst |
138 val ty2 = fastype_of snd |
138 val ty2 = fastype_of snd |
139 val c = HOLogic.pair_const ty1 ty2 |
139 val c = HOLogic.pair_const ty1 ty2 |
140 in c $ fst $ snd |
140 in c $ fst $ snd |
141 end; |
141 end; |
142 |
142 *} |
143 *} |
143 |
|
144 (* Given [fv1, fv2, fv3] creates %(x, y, z). fv1 x u fv2 y u fv3 z *) |
|
145 ML {* |
|
146 fun mk_compound_fv fvs = |
|
147 let |
|
148 val nos = (length fvs - 1) downto 0; |
|
149 val fvs_applied = map (fn (fv, no) => fv $ Bound no) (fvs ~~ nos); |
|
150 val fvs_union = mk_union fvs_applied; |
|
151 val (tyh :: tys) = rev (map (domain_type o fastype_of) fvs); |
|
152 fun fold_fun ty t = HOLogic.mk_split (Abs ("", ty, t)) |
|
153 in |
|
154 fold fold_fun tys (Abs ("", tyh, fvs_union)) |
|
155 end; |
|
156 *} |
|
157 |
|
158 ML {* @{term "\<lambda>(x, y, z). \<lambda>(x', y', z'). R x x' \<and> R2 y y' \<and> R3 z z'"} *} |
|
159 |
|
160 (* Given [R1, R2, R3] creates %(x,x'). %(y,y'). %(z,z'). R x x' \<and> R y y' \<and> R z z' *) |
|
161 ML {* |
|
162 fun mk_compound_alpha Rs = |
|
163 let |
|
164 val nos = (length Rs - 1) downto 0; |
|
165 val nos2 = (2 * length Rs - 1) downto length Rs; |
|
166 val Rs_applied = map (fn (R, (no2, no)) => R $ Bound no2 $ Bound no) (Rs ~~ (nos2 ~~ nos)); |
|
167 val Rs_conj = mk_conjl Rs_applied; |
|
168 val (tyh :: tys) = rev (map (domain_type o fastype_of) Rs); |
|
169 fun fold_fun ty t = HOLogic.mk_split (Abs ("", ty, t)) |
|
170 val abs_rhs = fold fold_fun tys (Abs ("", tyh, Rs_conj)) |
|
171 in |
|
172 fold fold_fun tys (Abs ("", tyh, abs_rhs)) |
|
173 end; |
|
174 *} |
|
175 |
|
176 ML {* cterm_of @{theory} (mk_compound_alpha [@{term "R :: 'a \<Rightarrow> 'a \<Rightarrow> bool"}, @{term "R2 :: 'b \<Rightarrow> 'b \<Rightarrow> bool"}, @{term "R3 :: 'b \<Rightarrow> 'b \<Rightarrow> bool"}]) *} |
144 |
177 |
145 ML {* fun add_perm (p1, p2) = Const(@{const_name plus}, @{typ "perm \<Rightarrow> perm \<Rightarrow> perm"}) $ p1 $ p2 *} |
178 ML {* fun add_perm (p1, p2) = Const(@{const_name plus}, @{typ "perm \<Rightarrow> perm \<Rightarrow> perm"}) $ p1 $ p2 *} |
146 |
179 |
147 ML {* |
180 ML {* |
148 fun non_rec_binds l = |
181 fun non_rec_binds l = |
326 HOLogic.mk_Trueprop (alpha $ (list_comb (c, args)) $ (list_comb (c, args2))); |
359 HOLogic.mk_Trueprop (alpha $ (list_comb (c, args)) $ (list_comb (c, args2))); |
327 fun alpha_arg ((dt, arg_no), (arg, arg2)) = |
360 fun alpha_arg ((dt, arg_no), (arg, arg2)) = |
328 let |
361 let |
329 val rel_in_simp_binds = filter (fn ((NONE, i, _), _) => i = arg_no | _ => false) bind_pis; |
362 val rel_in_simp_binds = filter (fn ((NONE, i, _), _) => i = arg_no | _ => false) bind_pis; |
330 val rel_in_comp_binds = filter (fn ((SOME _, i, _), _) => i = arg_no | _ => false) bind_pis; |
363 val rel_in_comp_binds = filter (fn ((SOME _, i, _), _) => i = arg_no | _ => false) bind_pis; |
331 val rel_has_binds = filter (fn ((_, _, j), _) => j = arg_no | _ => false) bind_pis; |
364 val rel_has_binds = filter (fn ((NONE, _, j), _) => j = arg_no |
|
365 | ((SOME (_, false), _, j), _) => j = arg_no |
|
366 | _ => false) bind_pis; |
332 in |
367 in |
333 case (rel_in_simp_binds, rel_in_comp_binds, rel_has_binds) of |
368 case (rel_in_simp_binds, rel_in_comp_binds, rel_has_binds) of |
334 ([], [], []) => |
369 ([], [], []) => |
335 if is_rec_type dt then (nth alpha_frees (body_index dt) $ arg $ arg2) |
370 if is_rec_type dt then (nth alpha_frees (body_index dt) $ arg $ arg2) |
336 else (HOLogic.mk_eq (arg, arg2)) |
371 else (HOLogic.mk_eq (arg, arg2)) |
338 | ([], ((((SOME (bn, is_rec)), _, _), pi) :: _), []) => |
373 | ([], ((((SOME (bn, is_rec)), _, _), pi) :: _), []) => |
339 if not (bns_same rel_in_comp_binds) then error "incompatible bindings for an argument" else |
374 if not (bns_same rel_in_comp_binds) then error "incompatible bindings for an argument" else |
340 if is_rec then |
375 if is_rec then |
341 let |
376 let |
342 val (rbinds, rpis) = split_list rel_in_comp_binds |
377 val (rbinds, rpis) = split_list rel_in_comp_binds |
|
378 val bound_in_nos = map (fn (_, _, i) => i) rbinds |
|
379 val bound_in_ty_nos = map (fn i => body_index (nth dts i)) bound_in_nos; |
|
380 val bound_args = arg :: map (nth args) bound_in_nos; |
|
381 val bound_args2 = arg2 :: map (nth args2) bound_in_nos; |
|
382 fun bound_in args (_, _, i) = nth args i; |
343 val lhs_binds = fv_binds args rbinds |
383 val lhs_binds = fv_binds args rbinds |
344 val lhs = mk_pair (lhs_binds, arg); |
384 val lhs_arg = foldr1 HOLogic.mk_prod bound_args |
|
385 val lhs = mk_pair (lhs_binds, lhs_arg); |
345 val rhs_binds = fv_binds args2 rbinds; |
386 val rhs_binds = fv_binds args2 rbinds; |
346 val rhs = mk_pair (rhs_binds, arg2); |
387 val rhs_arg = foldr1 HOLogic.mk_prod bound_args2; |
347 val alpha = nth alpha_frees (body_index dt); |
388 val rhs = mk_pair (rhs_binds, rhs_arg); |
348 val fv = nth fv_frees (body_index dt); |
389 val _ = tracing (PolyML.makestring bound_in_ty_nos); |
|
390 val fvs = map (nth fv_frees) ((body_index dt) :: bound_in_ty_nos); |
|
391 val _ = tracing (PolyML.makestring fvs); |
|
392 val fv = mk_compound_fv fvs; |
|
393 val alphas = map (nth alpha_frees) ((body_index dt) :: bound_in_ty_nos); |
|
394 val _ = tracing (PolyML.makestring alphas); |
|
395 val alpha = mk_compound_alpha alphas; |
349 val pi = foldr1 add_perm (distinct (op =) rpis); |
396 val pi = foldr1 add_perm (distinct (op =) rpis); |
350 val alpha_gen_pre = Const (@{const_name alpha_gen}, dummyT) $ lhs $ alpha $ fv $ pi $ rhs; |
397 val alpha_gen_pre = Const (@{const_name alpha_gen}, dummyT) $ lhs $ alpha $ fv $ pi $ rhs; |
|
398 val _ = tracing (PolyML.makestring alpha_gen_pre); |
351 val alpha_gen = Syntax.check_term lthy alpha_gen_pre |
399 val alpha_gen = Syntax.check_term lthy alpha_gen_pre |
352 in |
400 in |
353 alpha_gen |
401 alpha_gen |
354 end |
402 end |
355 else |
403 else |