--- 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: "\<exists>(pi :: perm). P pi \<Longrightarrow> (\<And>(p :: perm). P p \<Longrightarrow> Q (- p)) \<Longrightarrow> \<exists>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: "\<exists>(pi :: perm). P pi \<Longrightarrow> \<exists>(pi :: perm). Q pi \<Longrightarrow> (\<And>(p :: perm) (pi :: perm). P p \<Longrightarrow> Q pi \<Longrightarrow> R (pi + p)) \<Longrightarrow> \<exists>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:
- "(\<And>xa ya. R xa ya \<longrightarrow> (\<forall>z. R ya z \<longrightarrow> R xa z)) \<Longrightarrow> 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 \<notin> a \<union> b \<equiv> (c \<notin> a \<and> c \<notin> b)"
by auto