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