2115
|
1 |
lemma exi: "\<exists>(pi :: perm). P pi \<Longrightarrow> (\<And>(p :: perm). P p \<Longrightarrow> Q (pi \<bullet> p)) \<Longrightarrow> \<exists>pi. Q pi"
|
|
2 |
apply (erule exE)
|
|
3 |
apply (rule_tac x="pi \<bullet> pia" in exI)
|
|
4 |
by auto
|
|
5 |
|
|
6 |
ML {*
|
|
7 |
fun alpha_eqvt_tac induct simps ctxt =
|
|
8 |
rtac induct THEN_ALL_NEW
|
|
9 |
simp_tac (HOL_basic_ss addsimps simps) THEN_ALL_NEW split_conj_tac THEN_ALL_NEW
|
|
10 |
REPEAT o etac @{thm exi[of _ _ "p"]} THEN' split_conj_tac THEN_ALL_NEW
|
|
11 |
asm_full_simp_tac (HOL_ss addsimps (all_eqvts ctxt @ simps)) THEN_ALL_NEW
|
|
12 |
asm_full_simp_tac (HOL_ss addsimps
|
|
13 |
@{thms supp_eqvt[symmetric] inter_eqvt[symmetric] empty_eqvt alphas prod_rel.simps prod_fv.simps}) THEN_ALL_NEW
|
|
14 |
(split_conj_tac THEN_ALL_NEW TRY o resolve_tac
|
|
15 |
@{thms fresh_star_permute_iff[of "- p", THEN iffD1] permute_eq_iff[of "- p", THEN iffD1]})
|
|
16 |
THEN_ALL_NEW
|
|
17 |
asm_full_simp_tac (HOL_ss addsimps (@{thms split_conv permute_minus_cancel permute_plus permute_eqvt[symmetric]} @ all_eqvts ctxt @ simps))
|
|
18 |
*}
|
|
19 |
|
|
20 |
ML {*
|
|
21 |
fun build_alpha_eqvt alpha names =
|
|
22 |
let
|
|
23 |
val pi = Free ("p", @{typ perm});
|
|
24 |
val (tys, _) = strip_type (fastype_of alpha)
|
|
25 |
val indnames = Name.variant_list names (Datatype_Prop.make_tnames (map body_type tys));
|
|
26 |
val args = map Free (indnames ~~ tys);
|
|
27 |
val perm_args = map (fn x => mk_perm pi x) args
|
|
28 |
in
|
|
29 |
(HOLogic.mk_imp (list_comb (alpha, args), list_comb (alpha, perm_args)), indnames @ names)
|
|
30 |
end
|
|
31 |
*}
|
|
32 |
|
|
33 |
ML {*
|
|
34 |
fun build_alpha_eqvts funs tac ctxt =
|
|
35 |
let
|
|
36 |
val (gls, names) = fold_map build_alpha_eqvt funs ["p"]
|
|
37 |
val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj gls)
|
|
38 |
val thm = Goal.prove ctxt names [] gl tac
|
|
39 |
in
|
|
40 |
map (fn x => mp OF [x]) (HOLogic.conj_elims thm)
|
|
41 |
end
|
|
42 |
*}
|
|
43 |
|
2133
|
44 |
(* Given [fv1, fv2, fv3]
|
|
45 |
produces %(x, y, z). fv1 x u fv2 y u fv3 z *)
|
|
46 |
ML {*
|
|
47 |
fun mk_compound_fv fvs =
|
|
48 |
let
|
|
49 |
val nos = (length fvs - 1) downto 0;
|
|
50 |
val fvs_applied = map (fn (fv, no) => fv $ Bound no) (fvs ~~ nos);
|
|
51 |
val fvs_union = mk_union fvs_applied;
|
|
52 |
val (tyh :: tys) = rev (map (domain_type o fastype_of) fvs);
|
|
53 |
fun fold_fun ty t = HOLogic.mk_split (Abs ("", ty, t))
|
|
54 |
in
|
|
55 |
fold fold_fun tys (Abs ("", tyh, fvs_union))
|
|
56 |
end;
|
|
57 |
*}
|
|
58 |
|
|
59 |
(* Given [R1, R2, R3]
|
|
60 |
produces %(x,x'). %(y,y'). %(z,z'). R x x' \<and> R y y' \<and> R z z' *)
|
|
61 |
ML {*
|
|
62 |
fun mk_compound_alpha Rs =
|
|
63 |
let
|
|
64 |
val nos = (length Rs - 1) downto 0;
|
|
65 |
val nos2 = (2 * length Rs - 1) downto length Rs;
|
|
66 |
val Rs_applied = map (fn (R, (no2, no)) => R $ Bound no2 $ Bound no)
|
|
67 |
(Rs ~~ (nos2 ~~ nos));
|
|
68 |
val Rs_conj = foldr1 HOLogic.mk_conj Rs_applied;
|
|
69 |
val (tyh :: tys) = rev (map (domain_type o fastype_of) Rs);
|
|
70 |
fun fold_fun ty t = HOLogic.mk_split (Abs ("", ty, t))
|
|
71 |
val abs_rhs = fold fold_fun tys (Abs ("", tyh, Rs_conj))
|
|
72 |
in
|
|
73 |
fold fold_fun tys (Abs ("", tyh, abs_rhs))
|
|
74 |
end;
|
|
75 |
*}
|