293 TRY o REPEAT_ALL_NEW (CHANGED o rtac @{thm conjI}) THEN_ALL_NEW |
293 TRY o REPEAT_ALL_NEW (CHANGED o rtac @{thm conjI}) THEN_ALL_NEW |
294 (etac @{thm alpha_gen_compose_sym} THEN' eresolve_tac eqvt) |
294 (etac @{thm alpha_gen_compose_sym} THEN' eresolve_tac eqvt) |
295 *} |
295 *} |
296 |
296 |
297 ML {* |
297 ML {* |
298 fun transp_tac induct alpha_inj term_inj distinct cases eqvt = |
298 fun imp_elim_tac case_rules = |
299 ((rtac @{thm impI} THEN' etac induct) ORELSE' rtac induct) THEN_ALL_NEW |
299 Subgoal.FOCUS (fn {concl, context, ...} => |
300 (rtac allI THEN' rtac impI THEN' rotate_tac (~1) THEN' |
300 case term_of concl of |
301 eresolve_tac cases) THEN_ALL_NEW |
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 |
302 ( |
324 ( |
303 asm_full_simp_tac (HOL_ss addsimps alpha_inj @ term_inj @ distinct) THEN' |
325 asm_full_simp_tac (HOL_ss addsimps alpha_inj @ term_inj @ distinct) THEN' |
304 TRY o REPEAT_ALL_NEW (CHANGED o rtac @{thm conjI}) THEN_ALL_NEW |
326 TRY o REPEAT_ALL_NEW (CHANGED o rtac @{thm conjI}) THEN_ALL_NEW |
305 (etac @{thm alpha_gen_compose_trans} THEN' RANGE [atac, eresolve_tac eqvt]) |
327 (etac @{thm alpha_gen_compose_trans} THEN' RANGE [atac, eresolve_tac eqvt]) |
306 ) |
328 ) |
326 let |
348 let |
327 val ([x, y, z], ctxt') = Variable.variant_fixes ["x","y","z"] ctxt; |
349 val ([x, y, z], ctxt') = Variable.variant_fixes ["x","y","z"] ctxt; |
328 val (reflg, (symg, transg)) = build_alpha_refl_gl alphas (x, y, z) |
350 val (reflg, (symg, transg)) = build_alpha_refl_gl alphas (x, y, z) |
329 fun reflp_tac' _ = reflp_tac term_induct alpha_inj 1; |
351 fun reflp_tac' _ = reflp_tac term_induct alpha_inj 1; |
330 fun symp_tac' _ = symp_tac alpha_induct alpha_inj eqvt 1; |
352 fun symp_tac' _ = symp_tac alpha_induct alpha_inj eqvt 1; |
331 fun transp_tac' _ = transp_tac alpha_induct alpha_inj term_inj distinct cases eqvt 1; |
353 fun transp_tac' _ = transp_tac ctxt alpha_induct alpha_inj term_inj distinct cases eqvt 1; |
332 val reflt = Goal.prove ctxt' [] [] reflg reflp_tac'; |
354 val reflt = Goal.prove ctxt' [] [] reflg reflp_tac'; |
333 val symt = Goal.prove ctxt' [] [] symg symp_tac'; |
355 val symt = Goal.prove ctxt' [] [] symg symp_tac'; |
334 val transt = Goal.prove ctxt' [] [] transg transp_tac'; |
356 val transt = Goal.prove ctxt' [] [] transg transp_tac'; |
335 val [refltg, symtg, transtg] = Variable.export ctxt' ctxt [reflt, symt, transt] |
357 val [refltg, symtg, transtg] = Variable.export ctxt' ctxt [reflt, symt, transt] |
336 val reflts = HOLogic.conj_elims refltg |
358 val reflts = HOLogic.conj_elims refltg |
347 in |
369 in |
348 map equivp alphas |
370 map equivp alphas |
349 end |
371 end |
350 *} |
372 *} |
351 |
373 |
352 end |
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 |