diff -r 99706604c573 -r 9038c9549073 Nominal/Equivp.thy --- a/Nominal/Equivp.thy Wed Jun 23 06:45:03 2010 +0100 +++ b/Nominal/Equivp.thy Wed Jun 23 06:54:48 2010 +0100 @@ -2,166 +2,6 @@ imports "Abs" "Perm" "Tacs" "Rsp" begin -ML {* -fun build_alpha_sym_trans_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 - (symp, transp) - end; - val eqs = map build_alpha alphas - val (sym_eqs, trans_eqs) = split_list eqs - fun conj l = @{term Trueprop} $ foldr1 HOLogic.mk_conj l -in - (conj sym_eqs, conj trans_eqs) -end -*} - -ML {* -fun build_alpha_refl_gl fv_alphas_lst alphas = -let - val (fvs_alphas, _) = split_list fv_alphas_lst; - val (_, alpha_ts) = split_list fvs_alphas; - val tys = map (domain_type o fastype_of) alpha_ts; - val names = Datatype_Prop.make_tnames tys; - val args = map Free (names ~~ tys); - fun find_alphas ty x = - domain_type (fastype_of x) = ty; - fun refl_eq_arg (ty, arg) = - let - val rel_alphas = filter (find_alphas ty) alphas; - in - map (fn x => x $ arg $ arg) rel_alphas - end; - (* Flattening loses the induction structure *) - val eqs = map (foldr1 HOLogic.mk_conj) (map refl_eq_arg (tys ~~ args)) -in - (names, HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj eqs)) -end -*} - -ML {* -fun reflp_tac induct eq_iff = - rtac induct THEN_ALL_NEW - simp_tac (HOL_basic_ss addsimps eq_iff) THEN_ALL_NEW - split_conj_tac THEN_ALL_NEW REPEAT o rtac @{thm exI[of _ "0 :: perm"]} - THEN_ALL_NEW split_conj_tac THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps - @{thms alphas fresh_star_def fresh_zero_perm permute_zero ball_triv - add_0_left supp_zero_perm Int_empty_left split_conv prod_rel.simps}) -*} - -ML {* -fun build_alpha_refl fv_alphas_lst alphas induct eq_iff ctxt = -let - val (names, gl) = build_alpha_refl_gl fv_alphas_lst alphas; - val refl_conj = Goal.prove ctxt names [] gl (fn _ => reflp_tac induct eq_iff 1); -in - HOLogic.conj_elims refl_conj -end -*} - -lemma exi_neg: "\(pi :: perm). P pi \ (\(p :: perm). P p \ Q (- p)) \ \pi. Q pi" -apply (erule exE) -apply (rule_tac x="-pi" in exI) -by auto - -ML {* -fun symp_tac induct inj eqvt ctxt = - rtac induct THEN_ALL_NEW - simp_tac (HOL_basic_ss addsimps inj) THEN_ALL_NEW split_conj_tac - THEN_ALL_NEW - REPEAT o etac @{thm exi_neg} - THEN_ALL_NEW - split_conj_tac THEN_ALL_NEW - asm_full_simp_tac (HOL_ss addsimps @{thms supp_minus_perm minus_add[symmetric]}) THEN_ALL_NEW - TRY o (resolve_tac @{thms alphas_compose_sym2} ORELSE' resolve_tac @{thms alphas_compose_sym}) THEN_ALL_NEW - (asm_full_simp_tac (HOL_ss addsimps (eqvt @ all_eqvts ctxt))) -*} - - -lemma exi_sum: "\(pi :: perm). P pi \ \(pi :: perm). Q pi \ (\(p :: perm) (pi :: perm). P p \ Q pi \ R (pi + p)) \ \pi. R pi" -apply (erule exE)+ -apply (rule_tac x="pia + pi" in exI) -by auto - - -ML {* -fun eetac rule = - Subgoal.FOCUS_PARAMS (fn focus => - let - val concl = #concl focus - val prems = Logic.strip_imp_prems (term_of concl) - val exs = filter (fn x => is_ex (HOLogic.dest_Trueprop x)) prems - val cexs = map (SOME o (cterm_of (ProofContext.theory_of (#context focus)))) exs - val thins = map (fn cex => Drule.instantiate' [] [cex] Drule.thin_rl) cexs - in - (etac rule THEN' RANGE[atac, eresolve_tac thins]) 1 - end - ) -*} - -ML {* -fun transp_tac ctxt induct alpha_inj term_inj distinct cases eqvt = - rtac induct THEN_ALL_NEW - (TRY o rtac allI THEN' imp_elim_tac cases ctxt) THEN_ALL_NEW - asm_full_simp_tac (HOL_basic_ss addsimps alpha_inj) THEN_ALL_NEW - split_conj_tac THEN_ALL_NEW REPEAT o (eetac @{thm exi_sum} ctxt) THEN_ALL_NEW split_conj_tac - THEN_ALL_NEW (asm_full_simp_tac (HOL_ss addsimps (term_inj @ distinct))) - THEN_ALL_NEW split_conj_tac THEN_ALL_NEW - TRY o (eresolve_tac @{thms alphas_compose_trans2} ORELSE' eresolve_tac @{thms alphas_compose_trans}) THEN_ALL_NEW - (asm_full_simp_tac (HOL_ss addsimps (all_eqvts ctxt @ eqvt @ term_inj @ distinct))) -*} - -lemma transpI: - "(\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 = - (*let val _ = tracing (PolyML.makestring (reflps, symps, transps)) in *) - 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 transpI} THEN' resolve_tac transps -*} - -ML {* -fun build_equivps alphas reflps alpha_induct term_inj alpha_inj distinct cases eqvt ctxt = -let - val ([x, y, z], ctxt') = Variable.variant_fixes ["x","y","z"] ctxt; - val (symg, transg) = build_alpha_sym_trans_gl alphas (x, y, z) - fun symp_tac' _ = symp_tac alpha_induct alpha_inj eqvt ctxt 1; - fun transp_tac' _ = transp_tac ctxt alpha_induct alpha_inj term_inj distinct cases eqvt 1; - val symp_loc = Goal.prove ctxt' [] [] symg symp_tac'; - val transp_loc = Goal.prove ctxt' [] [] transg transp_tac'; - val [symp, transp] = Variable.export ctxt' ctxt [symp_loc, transp_loc] - val symps = HOLogic.conj_elims symp - val transps = HOLogic.conj_elims transp - 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 reflps symps transps 1 - in - Goal.prove ctxt [] [] goal tac - end -in - map equivp alphas -end -*} - lemma not_in_union: "c \ a \ b \ (c \ a \ c \ b)" by auto