author | Cezary Kaliszyk <kaliszyk@in.tum.de> |
Mon, 10 May 2010 15:45:04 +0200 | |
changeset 2093 | 751d1349329b |
parent 2070 | ff69913e2608 |
child 2108 | c5b7be27f105 |
permissions | -rw-r--r-- |
1830
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
1 |
theory Equivp |
2019
0a04acc91ca1
Remove dependency on NewFv
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2008
diff
changeset
|
2 |
imports "NewFv" "Tacs" "Rsp" |
1830
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
3 |
begin |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
4 |
|
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
5 |
ML {* |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
6 |
fun build_alpha_sym_trans_gl alphas (x, y, z) = |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
7 |
let |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
8 |
fun build_alpha alpha = |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
9 |
let |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
10 |
val ty = domain_type (fastype_of alpha); |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
11 |
val var = Free(x, ty); |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
12 |
val var2 = Free(y, ty); |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
13 |
val var3 = Free(z, ty); |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
14 |
val symp = HOLogic.mk_imp (alpha $ var $ var2, alpha $ var2 $ var); |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
15 |
val transp = HOLogic.mk_imp (alpha $ var $ var2, |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
16 |
HOLogic.mk_all (z, ty, |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
17 |
HOLogic.mk_imp (alpha $ var2 $ var3, alpha $ var $ var3))) |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
18 |
in |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
19 |
(symp, transp) |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
20 |
end; |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
21 |
val eqs = map build_alpha alphas |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
22 |
val (sym_eqs, trans_eqs) = split_list eqs |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
23 |
fun conj l = @{term Trueprop} $ foldr1 HOLogic.mk_conj l |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
24 |
in |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
25 |
(conj sym_eqs, conj trans_eqs) |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
26 |
end |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
27 |
*} |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
28 |
|
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
29 |
ML {* |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
30 |
fun build_alpha_refl_gl fv_alphas_lst alphas = |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
31 |
let |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
32 |
val (fvs_alphas, _) = split_list fv_alphas_lst; |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
33 |
val (_, alpha_ts) = split_list fvs_alphas; |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
34 |
val tys = map (domain_type o fastype_of) alpha_ts; |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
35 |
val names = Datatype_Prop.make_tnames tys; |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
36 |
val args = map Free (names ~~ tys); |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
37 |
fun find_alphas ty x = |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
38 |
domain_type (fastype_of x) = ty; |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
39 |
fun refl_eq_arg (ty, arg) = |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
40 |
let |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
41 |
val rel_alphas = filter (find_alphas ty) alphas; |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
42 |
in |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
43 |
map (fn x => x $ arg $ arg) rel_alphas |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
44 |
end; |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
45 |
(* Flattening loses the induction structure *) |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
46 |
val eqs = map (foldr1 HOLogic.mk_conj) (map refl_eq_arg (tys ~~ args)) |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
47 |
in |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
48 |
(names, HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj eqs)) |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
49 |
end |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
50 |
*} |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
51 |
|
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
52 |
ML {* |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
53 |
fun reflp_tac induct eq_iff = |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
54 |
rtac induct THEN_ALL_NEW |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
55 |
simp_tac (HOL_basic_ss addsimps eq_iff) THEN_ALL_NEW |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
56 |
split_conj_tac THEN_ALL_NEW REPEAT o rtac @{thm exI[of _ "0 :: perm"]} |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
57 |
THEN_ALL_NEW split_conj_tac THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
58 |
@{thms alphas fresh_star_def fresh_zero_perm permute_zero ball_triv |
2070
ff69913e2608
prod_rel.simps and Fixed for new isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2019
diff
changeset
|
59 |
add_0_left supp_zero_perm Int_empty_left split_conv prod_rel.simps}) |
1830
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
60 |
*} |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
61 |
|
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
62 |
ML {* |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
63 |
fun build_alpha_refl fv_alphas_lst alphas induct eq_iff ctxt = |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
64 |
let |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
65 |
val (names, gl) = build_alpha_refl_gl fv_alphas_lst alphas; |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
66 |
val refl_conj = Goal.prove ctxt names [] gl (fn _ => reflp_tac induct eq_iff 1); |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
67 |
in |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
68 |
HOLogic.conj_elims refl_conj |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
69 |
end |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
70 |
*} |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
71 |
|
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
72 |
lemma exi_neg: "\<exists>(pi :: perm). P pi \<Longrightarrow> (\<And>(p :: perm). P p \<Longrightarrow> Q (- p)) \<Longrightarrow> \<exists>pi. Q pi" |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
73 |
apply (erule exE) |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
74 |
apply (rule_tac x="-pi" in exI) |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
75 |
by auto |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
76 |
|
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
77 |
ML {* |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
78 |
fun symp_tac induct inj eqvt ctxt = |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
79 |
rel_indtac induct THEN_ALL_NEW |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
80 |
simp_tac (HOL_basic_ss addsimps inj) THEN_ALL_NEW split_conj_tac |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
81 |
THEN_ALL_NEW |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
82 |
REPEAT o etac @{thm exi_neg} |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
83 |
THEN_ALL_NEW |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
84 |
split_conj_tac THEN_ALL_NEW |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
85 |
asm_full_simp_tac (HOL_ss addsimps @{thms supp_minus_perm minus_add[symmetric]}) THEN_ALL_NEW |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
86 |
TRY o (resolve_tac @{thms alphas_compose_sym2} ORELSE' resolve_tac @{thms alphas_compose_sym}) THEN_ALL_NEW |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
87 |
(asm_full_simp_tac (HOL_ss addsimps (eqvt @ all_eqvts ctxt))) |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
88 |
*} |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
89 |
|
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
90 |
|
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
91 |
lemma exi_sum: "\<exists>(pi :: perm). P pi \<Longrightarrow> \<exists>(pi :: perm). Q pi \<Longrightarrow> (\<And>(p :: perm) (pi :: perm). P p \<Longrightarrow> Q pi \<Longrightarrow> R (pi + p)) \<Longrightarrow> \<exists>pi. R pi" |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
92 |
apply (erule exE)+ |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
93 |
apply (rule_tac x="pia + pi" in exI) |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
94 |
by auto |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
95 |
|
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
96 |
|
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
97 |
ML {* |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
98 |
fun eetac rule = |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
99 |
Subgoal.FOCUS_PARAMS (fn focus => |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
100 |
let |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
101 |
val concl = #concl focus |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
102 |
val prems = Logic.strip_imp_prems (term_of concl) |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
103 |
val exs = filter (fn x => is_ex (HOLogic.dest_Trueprop x)) prems |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
104 |
val cexs = map (SOME o (cterm_of (ProofContext.theory_of (#context focus)))) exs |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
105 |
val thins = map (fn cex => Drule.instantiate' [] [cex] Drule.thin_rl) cexs |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
106 |
in |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
107 |
(etac rule THEN' RANGE[atac, eresolve_tac thins]) 1 |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
108 |
end |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
109 |
) |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
110 |
*} |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
111 |
|
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
112 |
ML {* |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
113 |
fun transp_tac ctxt induct alpha_inj term_inj distinct cases eqvt = |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
114 |
rel_indtac induct THEN_ALL_NEW |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
115 |
(TRY o rtac allI THEN' imp_elim_tac cases ctxt) THEN_ALL_NEW |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
116 |
asm_full_simp_tac (HOL_basic_ss addsimps alpha_inj) THEN_ALL_NEW |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
117 |
split_conj_tac THEN_ALL_NEW REPEAT o (eetac @{thm exi_sum} ctxt) THEN_ALL_NEW split_conj_tac |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
118 |
THEN_ALL_NEW (asm_full_simp_tac (HOL_ss addsimps (term_inj @ distinct))) |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
119 |
THEN_ALL_NEW split_conj_tac THEN_ALL_NEW |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
120 |
TRY o (eresolve_tac @{thms alphas_compose_trans2} ORELSE' eresolve_tac @{thms alphas_compose_trans}) THEN_ALL_NEW |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
121 |
(asm_full_simp_tac (HOL_ss addsimps (all_eqvts ctxt @ eqvt @ term_inj @ distinct))) |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
122 |
*} |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
123 |
|
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
124 |
lemma transpI: |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
125 |
"(\<And>xa ya. R xa ya \<longrightarrow> (\<forall>z. R ya z \<longrightarrow> R xa z)) \<Longrightarrow> transp R" |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
126 |
unfolding transp_def |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
127 |
by blast |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
128 |
|
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
129 |
ML {* |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
130 |
fun equivp_tac reflps symps transps = |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
131 |
(*let val _ = tracing (PolyML.makestring (reflps, symps, transps)) in *) |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
132 |
simp_tac (HOL_ss addsimps @{thms equivp_reflp_symp_transp reflp_def symp_def}) |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
133 |
THEN' rtac conjI THEN' rtac allI THEN' |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
134 |
resolve_tac reflps THEN' |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
135 |
rtac conjI THEN' rtac allI THEN' rtac allI THEN' |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
136 |
resolve_tac symps THEN' |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
137 |
rtac @{thm transpI} THEN' resolve_tac transps |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
138 |
*} |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
139 |
|
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
140 |
ML {* |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
141 |
fun build_equivps alphas reflps alpha_induct term_inj alpha_inj distinct cases eqvt ctxt = |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
142 |
let |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
143 |
val ([x, y, z], ctxt') = Variable.variant_fixes ["x","y","z"] ctxt; |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
144 |
val (symg, transg) = build_alpha_sym_trans_gl alphas (x, y, z) |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
145 |
fun symp_tac' _ = symp_tac alpha_induct alpha_inj eqvt ctxt 1; |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
146 |
fun transp_tac' _ = transp_tac ctxt alpha_induct alpha_inj term_inj distinct cases eqvt 1; |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
147 |
val symp_loc = Goal.prove ctxt' [] [] symg symp_tac'; |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
148 |
val transp_loc = Goal.prove ctxt' [] [] transg transp_tac'; |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
149 |
val [symp, transp] = Variable.export ctxt' ctxt [symp_loc, transp_loc] |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
150 |
val symps = HOLogic.conj_elims symp |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
151 |
val transps = HOLogic.conj_elims transp |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
152 |
fun equivp alpha = |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
153 |
let |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
154 |
val equivp = Const (@{const_name equivp}, fastype_of alpha --> @{typ bool}) |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
155 |
val goal = @{term Trueprop} $ (equivp $ alpha) |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
156 |
fun tac _ = equivp_tac reflps symps transps 1 |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
157 |
in |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
158 |
Goal.prove ctxt [] [] goal tac |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
159 |
end |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
160 |
in |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
161 |
map equivp alphas |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
162 |
end |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
163 |
*} |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
164 |
|
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
165 |
lemma not_in_union: "c \<notin> a \<union> b \<equiv> (c \<notin> a \<and> c \<notin> b)" |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
166 |
by auto |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
167 |
|
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
168 |
ML {* |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
169 |
fun supports_tac perm = |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
170 |
simp_tac (HOL_ss addsimps @{thms supports_def not_in_union} @ perm) THEN_ALL_NEW ( |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
171 |
REPEAT o rtac allI THEN' REPEAT o rtac impI THEN' split_conj_tac THEN' |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
172 |
asm_full_simp_tac (HOL_ss addsimps @{thms fresh_def[symmetric] |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
173 |
swap_fresh_fresh fresh_atom swap_at_base_simps(3) swap_atom_image_fresh |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
174 |
supp_fset_to_set supp_fmap_atom})) |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
175 |
*} |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
176 |
|
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
177 |
ML {* |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
178 |
fun mk_supp ty x = |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
179 |
Const (@{const_name supp}, ty --> @{typ "atom set"}) $ x |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
180 |
*} |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
181 |
|
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
182 |
ML {* |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
183 |
fun mk_supports_eq thy cnstr = |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
184 |
let |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
185 |
val (tys, ty) = (strip_type o fastype_of) cnstr |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
186 |
val names = Datatype_Prop.make_tnames tys |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
187 |
val frees = map Free (names ~~ tys) |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
188 |
val rhs = list_comb (cnstr, frees) |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
189 |
|
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
190 |
fun mk_supp_arg (x, ty) = |
2008
1bddffddc03f
attempted to remove dependency on (old) Fv and (old) Parser; lifting still uses Fv.thy; the examples do not work at the moment (with equivp proofs failing)
Christian Urban <urbanc@in.tum.de>
parents:
1898
diff
changeset
|
191 |
if is_atom thy ty then mk_supp @{typ atom} (mk_atom_ty ty x) else |
1830
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
192 |
if is_atom_set thy ty then mk_supp @{typ "atom set"} (mk_atom_set x) else |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
193 |
if is_atom_fset thy ty then mk_supp @{typ "atom set"} (mk_atom_fset x) |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
194 |
else mk_supp ty x |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
195 |
val lhss = map mk_supp_arg (frees ~~ tys) |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
196 |
val supports = Const(@{const_name "supports"}, @{typ "atom set"} --> ty --> @{typ bool}) |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
197 |
val eq = HOLogic.mk_Trueprop (supports $ mk_union lhss $ rhs) |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
198 |
in |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
199 |
(names, eq) |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
200 |
end |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
201 |
*} |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
202 |
|
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
203 |
ML {* |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
204 |
fun prove_supports ctxt perms cnst = |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
205 |
let |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
206 |
val (names, eq) = mk_supports_eq (ProofContext.theory_of ctxt) cnst |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
207 |
in |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
208 |
Goal.prove ctxt names [] eq (fn _ => supports_tac perms 1) |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
209 |
end |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
210 |
*} |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
211 |
|
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
212 |
ML {* |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
213 |
fun mk_fs tys = |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
214 |
let |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
215 |
val names = Datatype_Prop.make_tnames tys |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
216 |
val frees = map Free (names ~~ tys) |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
217 |
val supps = map2 mk_supp tys frees |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
218 |
val fin_supps = map (fn x => @{term "finite :: atom set \<Rightarrow> bool"} $ x) supps |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
219 |
in |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
220 |
(names, HOLogic.mk_Trueprop (mk_conjl fin_supps)) |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
221 |
end |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
222 |
*} |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
223 |
|
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
224 |
ML {* |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
225 |
fun fs_tac induct supports = rel_indtac induct THEN_ALL_NEW ( |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
226 |
rtac @{thm supports_finite} THEN' resolve_tac supports) THEN_ALL_NEW |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
227 |
asm_full_simp_tac (HOL_ss addsimps @{thms supp_atom supp_atom_image supp_fset_to_set |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
228 |
supp_fmap_atom finite_insert finite.emptyI finite_Un finite_supp}) |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
229 |
*} |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
230 |
|
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
231 |
ML {* |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
232 |
fun prove_fs ctxt induct supports tys = |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
233 |
let |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
234 |
val (names, eq) = mk_fs tys |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
235 |
in |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
236 |
Goal.prove ctxt names [] eq (fn _ => fs_tac induct supports 1) |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
237 |
end |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
238 |
*} |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
239 |
|
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
240 |
ML {* |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
241 |
fun mk_supp x = Const (@{const_name supp}, fastype_of x --> @{typ "atom set"}) $ x; |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
242 |
|
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
243 |
fun mk_supp_neq arg (fv, alpha) = |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
244 |
let |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
245 |
val collect = Const ("Collect", @{typ "(atom \<Rightarrow> bool) \<Rightarrow> atom \<Rightarrow> bool"}); |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
246 |
val ty = fastype_of arg; |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
247 |
val perm = Const ("Nominal2_Base.pt_class.permute", @{typ perm} --> ty --> ty); |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
248 |
val finite = @{term "finite :: atom set \<Rightarrow> bool"} |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
249 |
val rhs = collect $ Abs ("a", @{typ atom}, |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
250 |
HOLogic.mk_not (finite $ |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
251 |
(collect $ Abs ("b", @{typ atom}, |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
252 |
HOLogic.mk_not (alpha $ (perm $ (@{term swap} $ Bound 1 $ Bound 0) $ arg) $ arg))))) |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
253 |
in |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
254 |
HOLogic.mk_eq (fv $ arg, rhs) |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
255 |
end; |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
256 |
|
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
257 |
fun supp_eq fv_alphas_lst = |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
258 |
let |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
259 |
val (fvs_alphas, ls) = split_list fv_alphas_lst; |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
260 |
val (fv_ts, _) = split_list fvs_alphas; |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
261 |
val tys = map (domain_type o fastype_of) fv_ts; |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
262 |
val names = Datatype_Prop.make_tnames tys; |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
263 |
val args = map Free (names ~~ tys); |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
264 |
fun supp_eq_arg ((fv, arg), l) = |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
265 |
mk_conjl |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
266 |
((HOLogic.mk_eq (fv $ arg, mk_supp arg)) :: |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
267 |
(map (mk_supp_neq arg) l)) |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
268 |
val eqs = mk_conjl (map supp_eq_arg ((fv_ts ~~ args) ~~ ls)) |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
269 |
in |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
270 |
(names, HOLogic.mk_Trueprop eqs) |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
271 |
end |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
272 |
*} |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
273 |
|
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
274 |
ML {* |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
275 |
fun combine_fv_alpha_bns (fv_ts_nobn, fv_ts_bn) (alpha_ts_nobn, alpha_ts_bn) bn_nos = |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
276 |
if length fv_ts_bn < length alpha_ts_bn then |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
277 |
(fv_ts_nobn ~~ alpha_ts_nobn) ~~ (replicate (length fv_ts_nobn) []) |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
278 |
else let |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
279 |
val fv_alpha_nos = 0 upto (length fv_ts_nobn - 1); |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
280 |
fun filter_fn i (x, j) = if j = i then SOME x else NONE; |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
281 |
val fv_alpha_bn_nos = (fv_ts_bn ~~ alpha_ts_bn) ~~ bn_nos; |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
282 |
val fv_alpha_bn_all = map (fn i => map_filter (filter_fn i) fv_alpha_bn_nos) fv_alpha_nos; |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
283 |
in |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
284 |
(fv_ts_nobn ~~ alpha_ts_nobn) ~~ fv_alpha_bn_all |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
285 |
end |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
286 |
*} |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
287 |
|
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
288 |
(* TODO: this is a hack, it assumes that only one type of Abs's is present |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
289 |
in the type and chooses this supp_abs. Additionally single atoms are |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
290 |
treated properly. *) |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
291 |
ML {* |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
292 |
fun choose_alpha_abs eqiff = |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
293 |
let |
2070
ff69913e2608
prod_rel.simps and Fixed for new isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2019
diff
changeset
|
294 |
fun exists_subterms f ts = member (op =) (map (exists_subterm f) ts) true; |
1830
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
295 |
val terms = map prop_of eqiff; |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
296 |
fun check cname = exists_subterms (fn x => fst(dest_Const x) = cname handle _ => false) terms |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
297 |
val no = |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
298 |
if check @{const_name alpha_lst} then 2 else |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
299 |
if check @{const_name alpha_res} then 1 else |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
300 |
if check @{const_name alpha_gen} then 0 else |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
301 |
error "Failure choosing supp_abs" |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
302 |
in |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
303 |
nth @{thms supp_abs[symmetric]} no |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
304 |
end |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
305 |
*} |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
306 |
lemma supp_abs_atom: "supp (Abs {atom a} (x :: 'a :: fs)) = supp x - {atom a}" |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
307 |
by (rule supp_abs(1)) |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
308 |
|
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
309 |
lemma supp_abs_sum: |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
310 |
"supp (Abs x (a :: 'a :: fs)) \<union> supp (Abs x (b :: 'b :: fs)) = supp (Abs x (a, b))" |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
311 |
"supp (Abs_res x (a :: 'a :: fs)) \<union> supp (Abs_res x (b :: 'b :: fs)) = supp (Abs_res x (a, b))" |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
312 |
"supp (Abs_lst y (a :: 'a :: fs)) \<union> supp (Abs_lst y (b :: 'b :: fs)) = supp (Abs_lst y (a, b))" |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
313 |
apply (simp_all add: supp_abs supp_Pair) |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
314 |
apply blast+ |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
315 |
done |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
316 |
|
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
317 |
|
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
318 |
ML {* |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
319 |
fun supp_eq_tac ind fv perm eqiff ctxt = |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
320 |
rel_indtac ind THEN_ALL_NEW |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
321 |
asm_full_simp_tac (HOL_basic_ss addsimps fv) THEN_ALL_NEW |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
322 |
asm_full_simp_tac (HOL_basic_ss addsimps @{thms supp_abs_atom[symmetric]}) THEN_ALL_NEW |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
323 |
asm_full_simp_tac (HOL_basic_ss addsimps [choose_alpha_abs eqiff]) THEN_ALL_NEW |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
324 |
simp_tac (HOL_basic_ss addsimps @{thms supp_abs_sum}) THEN_ALL_NEW |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
325 |
simp_tac (HOL_basic_ss addsimps @{thms supp_def}) THEN_ALL_NEW |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
326 |
simp_tac (HOL_basic_ss addsimps (@{thms permute_abs} @ perm)) THEN_ALL_NEW |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
327 |
simp_tac (HOL_basic_ss addsimps (@{thms Abs_eq_iff} @ eqiff)) THEN_ALL_NEW |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
328 |
simp_tac (HOL_basic_ss addsimps @{thms alphas3 alphas2}) THEN_ALL_NEW |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
329 |
simp_tac (HOL_basic_ss addsimps @{thms alphas}) THEN_ALL_NEW |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
330 |
asm_full_simp_tac (HOL_basic_ss addsimps (@{thm supp_Pair} :: sym_eqvts ctxt)) THEN_ALL_NEW |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
331 |
asm_full_simp_tac (HOL_basic_ss addsimps (@{thm Pair_eq} :: all_eqvts ctxt)) THEN_ALL_NEW |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
332 |
simp_tac (HOL_basic_ss addsimps @{thms supp_at_base[symmetric,simplified supp_def]}) THEN_ALL_NEW |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
333 |
simp_tac (HOL_basic_ss addsimps @{thms Collect_disj_eq[symmetric]}) THEN_ALL_NEW |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
334 |
simp_tac (HOL_basic_ss addsimps @{thms infinite_Un[symmetric]}) THEN_ALL_NEW |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
335 |
simp_tac (HOL_basic_ss addsimps @{thms Collect_disj_eq[symmetric]}) THEN_ALL_NEW |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
336 |
simp_tac (HOL_basic_ss addsimps @{thms de_Morgan_conj[symmetric]}) THEN_ALL_NEW |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
337 |
simp_tac (HOL_basic_ss addsimps @{thms ex_simps(1,2)[symmetric]}) THEN_ALL_NEW |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
338 |
simp_tac (HOL_ss addsimps @{thms Collect_const finite.emptyI}) |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
339 |
*} |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
340 |
|
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
341 |
|
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
342 |
|
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
343 |
ML {* |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
344 |
fun build_eqvt_gl pi frees fnctn ctxt = |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
345 |
let |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
346 |
val typ = domain_type (fastype_of fnctn); |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
347 |
val arg = the (AList.lookup (op=) frees typ); |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
348 |
in |
1898
f8c8e2afcc18
deleting function perm_arg in favour of the library function mk_perm
Christian Urban <urbanc@in.tum.de>
parents:
1830
diff
changeset
|
349 |
([HOLogic.mk_eq (mk_perm pi (fnctn $ arg), fnctn $ (mk_perm pi arg))], ctxt) |
1830
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
350 |
end |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
351 |
*} |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
352 |
|
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
353 |
ML {* |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
354 |
fun prove_eqvt tys ind simps funs ctxt = |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
355 |
let |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
356 |
val ([pi], ctxt') = Variable.variant_fixes ["p"] ctxt; |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
357 |
val pi = Free (pi, @{typ perm}); |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
358 |
val tac = asm_full_simp_tac (HOL_ss addsimps (@{thms atom_eqvt permute_list.simps} @ simps @ all_eqvts ctxt')) |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
359 |
val ths_loc = prove_by_induct tys (build_eqvt_gl pi) ind tac funs ctxt' |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
360 |
val ths = Variable.export ctxt' ctxt ths_loc |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
361 |
val add_eqvt = Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add) |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
362 |
in |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
363 |
(ths, snd (Local_Theory.note ((Binding.empty, [add_eqvt]), ths) ctxt)) |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
364 |
end |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
365 |
*} |
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
366 |
|
8db45a106569
Initial cleaning/reorganization in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
367 |
end |