# HG changeset patch # User Cezary Kaliszyk # Date 1266853498 -3600 # Node ID 0f92257edeee2249998694914650da7fac084751 # Parent 43bd70786f9f21e0b34aa909a9c74656080d3743 A tactic for final equivp diff -r 43bd70786f9f -r 0f92257edeee Quot/Nominal/Fv.thy --- a/Quot/Nominal/Fv.thy Mon Feb 22 16:16:04 2010 +0100 +++ b/Quot/Nominal/Fv.thy Mon Feb 22 16:44:58 2010 +0100 @@ -253,17 +253,17 @@ *} ML {* -fun build_alpha_refl_gl alphas = +fun build_alpha_refl_gl alphas (x, y, z) = let fun build_alpha alpha = let val ty = domain_type (fastype_of alpha); - val var = Free("x", ty); - val var2 = Free("y", ty); - val var3 = Free("z", ty); + val var = Free(x, ty); + val var2 = Free(y, ty); + val var3 = Free(z, ty); val symp = HOLogic.mk_imp (alpha $ var $ var2, alpha $ var2 $ var); val transp = HOLogic.mk_imp (alpha $ var $ var2, - HOLogic.mk_all ("z", ty, + HOLogic.mk_all (z, ty, HOLogic.mk_imp (alpha $ var2 $ var3, alpha $ var $ var3))) in ((alpha $ var $ var), (symp, transp)) @@ -307,17 +307,23 @@ *} ML {* -fun build_equivps alphas induct alpha_inj term_inj distinct cases eqvt ctxt = +fun build_equivps alphas term_induct alpha_induct term_inj alpha_inj distinct cases eqvt ctxt = let - val (reflg, (symg, transg)) = build_alpha_refl_gl alphas - fun reflp_tac' _ = reflp_tac induct term_inj 1; - fun symp_tac' _ = symp_tac induct alpha_inj eqvt 1; - fun transp_tac' _ = transp_tac induct alpha_inj term_inj distinct cases eqvt 1; - val reflt = Goal.prove ctxt ["x"] [] reflg reflp_tac'; - val symt = Goal.prove ctxt ["x","y"] [] symg symp_tac'; - val transt = Goal.prove ctxt ["x","y","z"] [] transg transp_tac'; + val ([x, y, z], ctxt') = Variable.variant_fixes ["x","y","z"] ctxt; + val (reflg, (symg, transg)) = build_alpha_refl_gl alphas (x, y, z) + fun reflp_tac' _ = reflp_tac term_induct alpha_inj 1; + fun symp_tac' _ = symp_tac alpha_induct alpha_inj eqvt 1; + fun transp_tac' _ = transp_tac alpha_induct alpha_inj term_inj distinct cases eqvt 1; + val reflt = Goal.prove ctxt' [] [] reflg reflp_tac'; + val symt = Goal.prove ctxt' [] [] symg symp_tac'; + val transt = Goal.prove ctxt' [] [] transg transp_tac'; + val [refltg, symtg, transtg] = Variable.export ctxt' ctxt [reflt, symt, transt] + fun equivp alpha = + let + val goal = @{term Trueprop} $ (@{term equivp} $ alpha) + val tac = in - (reflt, symt, transt) + (refltg, symtg, transtg) end *} diff -r 43bd70786f9f -r 0f92257edeee Quot/Nominal/Terms.thy --- a/Quot/Nominal/Terms.thy Mon Feb 22 16:16:04 2010 +0100 +++ b/Quot/Nominal/Terms.thy Mon Feb 22 16:44:58 2010 +0100 @@ -116,33 +116,37 @@ apply(simp add: permute_eqvt[symmetric]) done - +ML {* +build_equivps [@{term alpha_rtrm1}, @{term alpha_bp}] @{thm rtrm1_bp.induct} @{thm alpha_rtrm1_alpha_bp.induct} @{thms rtrm1.inject bp.inject} @{thms alpha1_inj} @{thms rtrm1.distinct bp.distinct} @{thms alpha_rtrm1.cases alpha_bp.cases} @{thms alpha1_eqvt} @{context} +*} +ML Variable.export -prove alpha1_reflp_aux: {* fst (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}]) *} +prove alpha1_reflp_aux: {* fst (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}] ("x","y","z")) *} by (tactic {* reflp_tac @{thm rtrm1_bp.induct} @{thms alpha1_inj} 1 *}) -prove alpha1_symp_aux: {* (fst o snd) (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}]) *} +prove alpha1_symp_aux: {* (fst o snd) (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}] ("x","y","z")) *} by (tactic {* symp_tac @{thm alpha_rtrm1_alpha_bp.induct} @{thms alpha1_inj} @{thms alpha1_eqvt} 1 *}) -prove alpha1_transp_aux: {* (snd o snd) (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}]) *} +prove alpha1_transp_aux: {* (snd o snd) (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}] ("x","y","z")) *} by (tactic {* transp_tac @{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 *}) -lemma helper: "(\x y z. R x y \ R y z \ R x z) = (\xa ya. R xa ya \ (\z. R ya z \ R xa z))" -by meson +lemma transp_aux: + "(\xa ya. R xa ya \ (\z. R ya z \ R xa z)) \ transp R" + unfolding transp_def + by blast lemma alpha1_equivp: "equivp alpha_rtrm1" "equivp alpha_bp" -unfolding equivp_reflp_symp_transp reflp_def -apply (simp_all add: alpha1_reflp_aux) -unfolding symp_def -apply (simp_all add: alpha1_symp_aux) -unfolding transp_def -apply (simp_all only: helper) -apply (rule allI)+ -apply (rule conjunct1[OF alpha1_transp_aux]) -apply (rule allI)+ -apply (rule conjunct2[OF alpha1_transp_aux]) +apply (tactic {* + (simp_tac (HOL_ss addsimps @{thms equivp_reflp_symp_transp reflp_def symp_def}) + THEN' rtac @{thm conjI} THEN' rtac @{thm allI} THEN' + resolve_tac (HOLogic.conj_elims @{thm alpha1_reflp_aux}) + THEN' rtac @{thm conjI} THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' + resolve_tac (HOLogic.conj_elims @{thm alpha1_symp_aux}) THEN' rtac @{thm transp_aux} + THEN' resolve_tac (HOLogic.conj_elims @{thm alpha1_transp_aux}) +) +1 *}) done quotient_type trm1 = rtrm1 / alpha_rtrm1 @@ -526,13 +530,13 @@ apply (simp) done -prove alpha5_reflp_aux: {* fst (build_alpha_refl_gl [@{term alpha_rtrm5}, @{term alpha_rlts}]) *} +prove alpha5_reflp_aux: {* fst (build_alpha_refl_gl [@{term alpha_rtrm5}, @{term alpha_rlts}] ("x","y","z")) *} by (tactic {* reflp_tac @{thm rtrm5_rlts.induct} @{thms alpha5_inj} 1 *}) -prove alpha5_symp_aux: {* (fst o snd) (build_alpha_refl_gl [@{term alpha_rtrm5}, @{term alpha_rlts}]) *} +prove alpha5_symp_aux: {* (fst o snd) (build_alpha_refl_gl [@{term alpha_rtrm5}, @{term alpha_rlts}] ("x","y","z")) *} by (tactic {* symp_tac @{thm alpha_rtrm5_alpha_rlts.induct} @{thms alpha5_inj} @{thms alpha5_eqvt} 1 *}) -prove alpha5_transp_aux: {* (snd o snd) (build_alpha_refl_gl [@{term alpha_rtrm5}, @{term alpha_rlts}]) *} +prove alpha5_transp_aux: {* (snd o snd) (build_alpha_refl_gl [@{term alpha_rtrm5}, @{term alpha_rlts}] ("x","y","z")) *} by (tactic {* transp_tac @{thm alpha_rtrm5_alpha_rlts.induct} @{thms alpha5_inj} @{thms rtrm5.inject rlts.inject} @{thms rtrm5.distinct rlts.distinct} @{thms alpha_rtrm5.cases alpha_rlts.cases} @{thms alpha5_eqvt} 1 *}) lemma alpha5_equivps: