249 in |
250 in |
250 Variable.export ctxt' ctxt thms |
251 Variable.export ctxt' ctxt thms |
251 end |
252 end |
252 *} |
253 *} |
253 |
254 |
254 end |
255 ML {* |
|
256 fun build_alpha_refl_gl alphas (x, y, z) = |
|
257 let |
|
258 fun build_alpha alpha = |
|
259 let |
|
260 val ty = domain_type (fastype_of alpha); |
|
261 val var = Free(x, ty); |
|
262 val var2 = Free(y, ty); |
|
263 val var3 = Free(z, ty); |
|
264 val symp = HOLogic.mk_imp (alpha $ var $ var2, alpha $ var2 $ var); |
|
265 val transp = HOLogic.mk_imp (alpha $ var $ var2, |
|
266 HOLogic.mk_all (z, ty, |
|
267 HOLogic.mk_imp (alpha $ var2 $ var3, alpha $ var $ var3))) |
|
268 in |
|
269 ((alpha $ var $ var), (symp, transp)) |
|
270 end; |
|
271 val (refl_eqs, eqs) = split_list (map build_alpha alphas) |
|
272 val (sym_eqs, trans_eqs) = split_list eqs |
|
273 fun conj l = @{term Trueprop} $ foldr1 HOLogic.mk_conj l |
|
274 in |
|
275 (conj refl_eqs, (conj sym_eqs, conj trans_eqs)) |
|
276 end |
|
277 *} |
|
278 |
|
279 ML {* |
|
280 fun reflp_tac induct inj = |
|
281 rtac induct THEN_ALL_NEW |
|
282 asm_full_simp_tac (HOL_ss addsimps inj) THEN_ALL_NEW |
|
283 TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) THEN_ALL_NEW |
|
284 (rtac @{thm exI[of _ "0 :: perm"]} THEN' |
|
285 asm_full_simp_tac (HOL_ss addsimps |
|
286 @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv})) |
|
287 *} |
|
288 |
|
289 ML {* |
|
290 fun symp_tac induct inj eqvt = |
|
291 ((rtac @{thm impI} THEN' etac induct) ORELSE' rtac induct) THEN_ALL_NEW |
|
292 asm_full_simp_tac (HOL_ss addsimps inj) THEN_ALL_NEW |
|
293 TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) THEN_ALL_NEW |
|
294 (etac @{thm alpha_gen_compose_sym} THEN' eresolve_tac eqvt) |
|
295 *} |
|
296 |
|
297 ML {* |
|
298 fun imp_elim_tac case_rules = |
|
299 Subgoal.FOCUS (fn {concl, context, ...} => |
|
300 case term_of concl of |
|
301 _ $ (_ $ asm $ _) => |
|
302 let |
|
303 fun filter_fn case_rule = ( |
|
304 case Logic.strip_assums_hyp (prop_of case_rule) of |
|
305 ((_ $ asmc) :: _) => |
|
306 let |
|
307 val thy = ProofContext.theory_of context |
|
308 in |
|
309 Pattern.matches thy (asmc, asm) |
|
310 end |
|
311 | _ => false) |
|
312 val matching_rules = filter filter_fn case_rules |
|
313 in |
|
314 (rtac impI THEN' rotate_tac (~1) THEN' eresolve_tac matching_rules) 1 |
|
315 end |
|
316 | _ => no_tac |
|
317 ) |
|
318 *} |
|
319 |
|
320 ML {* |
|
321 fun transp_tac ctxt induct alpha_inj term_inj distinct cases eqvt = |
|
322 ((rtac impI THEN' etac induct) ORELSE' rtac induct) THEN_ALL_NEW |
|
323 (TRY o rtac allI THEN' imp_elim_tac cases ctxt) THEN_ALL_NEW |
|
324 ( |
|
325 asm_full_simp_tac (HOL_ss addsimps alpha_inj @ term_inj @ distinct) THEN' |
|
326 TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) THEN_ALL_NEW |
|
327 (etac @{thm alpha_gen_compose_trans} THEN' RANGE [atac, eresolve_tac eqvt]) |
|
328 ) |
|
329 *} |
|
330 |
|
331 lemma transp_aux: |
|
332 "(\<And>xa ya. R xa ya \<longrightarrow> (\<forall>z. R ya z \<longrightarrow> R xa z)) \<Longrightarrow> transp R" |
|
333 unfolding transp_def |
|
334 by blast |
|
335 |
|
336 ML {* |
|
337 fun equivp_tac reflps symps transps = |
|
338 simp_tac (HOL_ss addsimps @{thms equivp_reflp_symp_transp reflp_def symp_def}) |
|
339 THEN' rtac conjI THEN' rtac allI THEN' |
|
340 resolve_tac reflps THEN' |
|
341 rtac conjI THEN' rtac allI THEN' rtac allI THEN' |
|
342 resolve_tac symps THEN' |
|
343 rtac @{thm transp_aux} THEN' resolve_tac transps |
|
344 *} |
|
345 |
|
346 ML {* |
|
347 fun build_equivps alphas term_induct alpha_induct term_inj alpha_inj distinct cases eqvt ctxt = |
|
348 let |
|
349 val ([x, y, z], ctxt') = Variable.variant_fixes ["x","y","z"] ctxt; |
|
350 val (reflg, (symg, transg)) = build_alpha_refl_gl alphas (x, y, z) |
|
351 fun reflp_tac' _ = reflp_tac term_induct alpha_inj 1; |
|
352 fun symp_tac' _ = symp_tac alpha_induct alpha_inj eqvt 1; |
|
353 fun transp_tac' _ = transp_tac ctxt alpha_induct alpha_inj term_inj distinct cases eqvt 1; |
|
354 val reflt = Goal.prove ctxt' [] [] reflg reflp_tac'; |
|
355 val symt = Goal.prove ctxt' [] [] symg symp_tac'; |
|
356 val transt = Goal.prove ctxt' [] [] transg transp_tac'; |
|
357 val [refltg, symtg, transtg] = Variable.export ctxt' ctxt [reflt, symt, transt] |
|
358 val reflts = HOLogic.conj_elims refltg |
|
359 val symts = HOLogic.conj_elims symtg |
|
360 val transts = HOLogic.conj_elims transtg |
|
361 fun equivp alpha = |
|
362 let |
|
363 val equivp = Const (@{const_name equivp}, fastype_of alpha --> @{typ bool}) |
|
364 val goal = @{term Trueprop} $ (equivp $ alpha) |
|
365 fun tac _ = equivp_tac reflts symts transts 1 |
|
366 in |
|
367 Goal.prove ctxt [] [] goal tac |
|
368 end |
|
369 in |
|
370 map equivp alphas |
|
371 end |
|
372 *} |
|
373 |
|
374 (* |
|
375 Tests: |
|
376 prove alpha1_reflp_aux: {* fst (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}] ("x","y","z")) *} |
|
377 by (tactic {* reflp_tac @{thm rtrm1_bp.induct} @{thms alpha1_inj} 1 *}) |
|
378 |
|
379 prove alpha1_symp_aux: {* (fst o snd) (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}] ("x","y","z")) *} |
|
380 by (tactic {* symp_tac @{thm alpha_rtrm1_alpha_bp.induct} @{thms alpha1_inj} @{thms alpha1_eqvt} 1 *}) |
|
381 |
|
382 prove alpha1_transp_aux: {* (snd o snd) (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}] ("x","y","z")) *} |
|
383 by (tactic {* transp_tac @{context} @{thm alpha_rtrm1_alpha_bp.induct} @{thms alpha1_inj} @{thms rtrm1.inject bp.inject} @{thms rtrm1.distinct bp.distinct} @{thms alpha_rtrm1.cases alpha_bp.cases} @{thms alpha1_eqvt} 1 *}) |
|
384 |
|
385 lemma alpha1_equivp: |
|
386 "equivp alpha_rtrm1" |
|
387 "equivp alpha_bp" |
|
388 apply (tactic {* |
|
389 (simp_tac (HOL_ss addsimps @{thms equivp_reflp_symp_transp reflp_def symp_def}) |
|
390 THEN' rtac @{thm conjI} THEN' rtac @{thm allI} THEN' |
|
391 resolve_tac (HOLogic.conj_elims @{thm alpha1_reflp_aux}) |
|
392 THEN' rtac @{thm conjI} THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' |
|
393 resolve_tac (HOLogic.conj_elims @{thm alpha1_symp_aux}) THEN' rtac @{thm transp_aux} |
|
394 THEN' resolve_tac (HOLogic.conj_elims @{thm alpha1_transp_aux}) |
|
395 ) |
|
396 1 *}) |
|
397 done*) |
|
398 |
|
399 end |