diff -r 160343d86a6f -r 20f76fde8ef1 Quot/Nominal/Fv.thy --- a/Quot/Nominal/Fv.thy Tue Feb 23 13:32:35 2010 +0100 +++ b/Quot/Nominal/Fv.thy Tue Feb 23 13:33:01 2010 +0100 @@ -90,6 +90,7 @@ *} +(* TODO: Notice datatypes without bindings and replace alpha with equality *) ML {* (* Currently needs just one full_tname to access Datatype *) fun define_fv_alpha full_tname bindsall lthy = @@ -219,11 +220,11 @@ ML {* fun alpha_inj_tac dist_inj intrs elims = SOLVED' (asm_full_simp_tac (HOL_ss addsimps intrs)) ORELSE' - rtac @{thm iffI} THEN' RANGE [ + (rtac @{thm iffI} THEN' RANGE [ (eresolve_tac elims THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps dist_inj) ), - (asm_full_simp_tac (HOL_ss addsimps intrs))] + asm_full_simp_tac (HOL_ss addsimps intrs)]) *} ML {* @@ -251,4 +252,148 @@ end *} +ML {* +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 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_imp (alpha $ var2 $ var3, alpha $ var $ var3))) + in + ((alpha $ var $ var), (symp, transp)) + end; + val (refl_eqs, eqs) = split_list (map build_alpha alphas) + val (sym_eqs, trans_eqs) = split_list eqs + fun conj l = @{term Trueprop} $ foldr1 HOLogic.mk_conj l +in + (conj refl_eqs, (conj sym_eqs, conj trans_eqs)) end +*} + +ML {* +fun reflp_tac induct inj = + rtac induct THEN_ALL_NEW + asm_full_simp_tac (HOL_ss addsimps inj) THEN_ALL_NEW + TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) THEN_ALL_NEW + (rtac @{thm exI[of _ "0 :: perm"]} THEN' + asm_full_simp_tac (HOL_ss addsimps + @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv})) +*} + +ML {* +fun symp_tac induct inj eqvt = + ((rtac @{thm impI} THEN' etac induct) ORELSE' rtac induct) THEN_ALL_NEW + asm_full_simp_tac (HOL_ss addsimps inj) THEN_ALL_NEW + TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) THEN_ALL_NEW + (etac @{thm alpha_gen_compose_sym} THEN' eresolve_tac eqvt) +*} + +ML {* +fun imp_elim_tac case_rules = + Subgoal.FOCUS (fn {concl, context, ...} => + case term_of concl of + _ $ (_ $ asm $ _) => + let + fun filter_fn case_rule = ( + case Logic.strip_assums_hyp (prop_of case_rule) of + ((_ $ asmc) :: _) => + let + val thy = ProofContext.theory_of context + in + Pattern.matches thy (asmc, asm) + end + | _ => false) + val matching_rules = filter filter_fn case_rules + in + (rtac impI THEN' rotate_tac (~1) THEN' eresolve_tac matching_rules) 1 + end + | _ => no_tac + ) +*} + +ML {* +fun transp_tac ctxt induct alpha_inj term_inj distinct cases eqvt = + ((rtac impI THEN' etac induct) ORELSE' rtac induct) THEN_ALL_NEW + (TRY o rtac allI THEN' imp_elim_tac cases ctxt) THEN_ALL_NEW + ( + asm_full_simp_tac (HOL_ss addsimps alpha_inj @ term_inj @ distinct) THEN' + TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) THEN_ALL_NEW + (etac @{thm alpha_gen_compose_trans} THEN' RANGE [atac, eresolve_tac eqvt]) + ) +*} + +lemma transp_aux: + "(\xa ya. R xa ya \ (\z. R ya z \ R xa z)) \ transp R" + unfolding transp_def + by blast + +ML {* +fun equivp_tac reflps symps transps = + simp_tac (HOL_ss addsimps @{thms equivp_reflp_symp_transp reflp_def symp_def}) + THEN' rtac conjI THEN' rtac allI THEN' + resolve_tac reflps THEN' + rtac conjI THEN' rtac allI THEN' rtac allI THEN' + resolve_tac symps THEN' + rtac @{thm transp_aux} THEN' resolve_tac transps +*} + +ML {* +fun build_equivps alphas term_induct alpha_induct term_inj alpha_inj distinct cases eqvt ctxt = +let + 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 ctxt 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] + val reflts = HOLogic.conj_elims refltg + val symts = HOLogic.conj_elims symtg + val transts = HOLogic.conj_elims transtg + fun equivp alpha = + let + val equivp = Const (@{const_name equivp}, fastype_of alpha --> @{typ bool}) + val goal = @{term Trueprop} $ (equivp $ alpha) + fun tac _ = equivp_tac reflts symts transts 1 + in + Goal.prove ctxt [] [] goal tac + end +in + map equivp alphas +end +*} + +(* +Tests: +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}] ("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}] ("x","y","z")) *} +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 *}) + +lemma alpha1_equivp: + "equivp alpha_rtrm1" + "equivp alpha_bp" +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*) + +end