theory Equivp
imports "Fv"
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})
*}

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 =
  rel_indtac 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 =
  rel_indtac 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

ML {*
fun supports_tac perm =
  simp_tac (HOL_ss addsimps @{thms supports_def not_in_union} @ perm) THEN_ALL_NEW (
    REPEAT o rtac allI THEN' REPEAT o rtac impI THEN' split_conj_tac THEN'
    asm_full_simp_tac (HOL_ss addsimps @{thms fresh_def[symmetric]
      swap_fresh_fresh fresh_atom swap_at_base_simps(3) swap_atom_image_fresh
      supp_fset_to_set supp_fmap_atom}))
*}

ML {*
fun mk_supp ty x =
  Const (@{const_name supp}, ty --> @{typ "atom set"}) $ x
*}

ML {*
fun mk_supports_eq thy cnstr =
let
  val (tys, ty) = (strip_type o fastype_of) cnstr
  val names = Datatype_Prop.make_tnames tys
  val frees = map Free (names ~~ tys)
  val rhs = list_comb (cnstr, frees)

  fun mk_supp_arg (x, ty) =
    if is_atom thy ty then mk_supp @{typ atom} (mk_atom ty $ x) else
    if is_atom_set thy ty then mk_supp @{typ "atom set"} (mk_atom_set x) else
    if is_atom_fset thy ty then mk_supp @{typ "atom set"} (mk_atom_fset x)
    else mk_supp ty x
  val lhss = map mk_supp_arg (frees ~~ tys)
  val supports = Const(@{const_name "supports"}, @{typ "atom set"} --> ty --> @{typ bool})
  val eq = HOLogic.mk_Trueprop (supports $ mk_union lhss $ rhs)
in
  (names, eq)
end
*}

ML {*
fun prove_supports ctxt perms cnst =
let
  val (names, eq) = mk_supports_eq (ProofContext.theory_of ctxt) cnst
in
  Goal.prove ctxt names [] eq (fn _ => supports_tac perms 1)
end
*}

ML {*
fun mk_fs tys =
let
  val names = Datatype_Prop.make_tnames tys
  val frees = map Free (names ~~ tys)
  val supps = map2 mk_supp tys frees
  val fin_supps = map (fn x => @{term "finite :: atom set \<Rightarrow> bool"} $ x) supps
in
  (names, HOLogic.mk_Trueprop (mk_conjl fin_supps))
end
*}

ML {*
fun fs_tac induct supports = rel_indtac induct THEN_ALL_NEW (
  rtac @{thm supports_finite} THEN' resolve_tac supports) THEN_ALL_NEW
  asm_full_simp_tac (HOL_ss addsimps @{thms supp_atom supp_atom_image supp_fset_to_set
    supp_fmap_atom finite_insert finite.emptyI finite_Un finite_supp})
*}

ML {*
fun prove_fs ctxt induct supports tys =
let
  val (names, eq) = mk_fs tys
in
  Goal.prove ctxt names [] eq (fn _ => fs_tac induct supports 1)
end
*}

ML {*
fun mk_supp x = Const (@{const_name supp}, fastype_of x --> @{typ "atom set"}) $ x;

fun mk_supp_neq arg (fv, alpha) =
let
  val collect = Const ("Collect", @{typ "(atom \<Rightarrow> bool) \<Rightarrow> atom \<Rightarrow> bool"});
  val ty = fastype_of arg;
  val perm = Const ("Nominal2_Base.pt_class.permute", @{typ perm} --> ty --> ty);
  val finite = @{term "finite :: atom set \<Rightarrow> bool"}
  val rhs = collect $ Abs ("a", @{typ atom},
    HOLogic.mk_not (finite $
      (collect $ Abs ("b", @{typ atom},
        HOLogic.mk_not (alpha $ (perm $ (@{term swap} $ Bound 1 $ Bound 0) $ arg) $ arg)))))
in
  HOLogic.mk_eq (fv $ arg, rhs)
end;

fun supp_eq fv_alphas_lst =
let
  val (fvs_alphas, ls) = split_list fv_alphas_lst;
  val (fv_ts, _) = split_list fvs_alphas;
  val tys = map (domain_type o fastype_of) fv_ts;
  val names = Datatype_Prop.make_tnames tys;
  val args = map Free (names ~~ tys);
  fun supp_eq_arg ((fv, arg), l) =
    mk_conjl
      ((HOLogic.mk_eq (fv $ arg, mk_supp arg)) ::
       (map (mk_supp_neq arg) l))
  val eqs = mk_conjl (map supp_eq_arg ((fv_ts ~~ args) ~~ ls))
in
  (names, HOLogic.mk_Trueprop eqs)
end
*}

ML {*
fun combine_fv_alpha_bns (fv_ts_nobn, fv_ts_bn) (alpha_ts_nobn, alpha_ts_bn) bn_nos =
if length fv_ts_bn < length alpha_ts_bn then
  (fv_ts_nobn ~~ alpha_ts_nobn) ~~ (replicate (length fv_ts_nobn) [])
else let
  val fv_alpha_nos = 0 upto (length fv_ts_nobn - 1);
  fun filter_fn i (x, j) = if j = i then SOME x else NONE;
  val fv_alpha_bn_nos = (fv_ts_bn ~~ alpha_ts_bn) ~~ bn_nos;
  val fv_alpha_bn_all = map (fn i => map_filter (filter_fn i) fv_alpha_bn_nos) fv_alpha_nos;
in
  (fv_ts_nobn ~~ alpha_ts_nobn) ~~ fv_alpha_bn_all
end
*}

(* TODO: this is a hack, it assumes that only one type of Abs's is present
   in the type and chooses this supp_abs. Additionally single atoms are
   treated properly. *)
ML {*
fun choose_alpha_abs eqiff =
let
  fun exists_subterms f ts = true mem (map (exists_subterm f) ts);
  val terms = map prop_of eqiff;
  fun check cname = exists_subterms (fn x => fst(dest_Const x) = cname handle _ => false) terms
  val no =
    if check @{const_name alpha_lst} then 2 else
    if check @{const_name alpha_res} then 1 else
    if check @{const_name alpha_gen} then 0 else
    error "Failure choosing supp_abs"
in
  nth @{thms supp_abs[symmetric]} no
end
*}
lemma supp_abs_atom: "supp (Abs {atom a} (x :: 'a :: fs)) = supp x - {atom a}"
by (rule supp_abs(1))

lemma supp_abs_sum:
  "supp (Abs x (a :: 'a :: fs)) \<union> supp (Abs x (b :: 'b :: fs)) = supp (Abs x (a, b))"
  "supp (Abs_res x (a :: 'a :: fs)) \<union> supp (Abs_res x (b :: 'b :: fs)) = supp (Abs_res x (a, b))"
  "supp (Abs_lst y (a :: 'a :: fs)) \<union> supp (Abs_lst y (b :: 'b :: fs)) = supp (Abs_lst y (a, b))"
  apply (simp_all add: supp_abs supp_Pair)
  apply blast+
  done


ML {*
fun supp_eq_tac ind fv perm eqiff ctxt =
  rel_indtac ind THEN_ALL_NEW
  asm_full_simp_tac (HOL_basic_ss addsimps fv) THEN_ALL_NEW
  asm_full_simp_tac (HOL_basic_ss addsimps @{thms supp_abs_atom[symmetric]}) THEN_ALL_NEW
  asm_full_simp_tac (HOL_basic_ss addsimps [choose_alpha_abs eqiff]) THEN_ALL_NEW
  simp_tac (HOL_basic_ss addsimps @{thms supp_abs_sum}) THEN_ALL_NEW
  simp_tac (HOL_basic_ss addsimps @{thms supp_def}) THEN_ALL_NEW
  simp_tac (HOL_basic_ss addsimps (@{thms permute_abs} @ perm)) THEN_ALL_NEW
  simp_tac (HOL_basic_ss addsimps (@{thms Abs_eq_iff} @ eqiff)) THEN_ALL_NEW
  simp_tac (HOL_basic_ss addsimps @{thms alphas3 alphas2}) THEN_ALL_NEW
  simp_tac (HOL_basic_ss addsimps @{thms alphas}) THEN_ALL_NEW
  asm_full_simp_tac (HOL_basic_ss addsimps (@{thm supp_Pair} :: sym_eqvts ctxt)) THEN_ALL_NEW
  asm_full_simp_tac (HOL_basic_ss addsimps (@{thm Pair_eq} :: all_eqvts ctxt)) THEN_ALL_NEW
  simp_tac (HOL_basic_ss addsimps @{thms supp_at_base[symmetric,simplified supp_def]}) THEN_ALL_NEW
  simp_tac (HOL_basic_ss addsimps @{thms Collect_disj_eq[symmetric]}) THEN_ALL_NEW
  simp_tac (HOL_basic_ss addsimps @{thms infinite_Un[symmetric]}) THEN_ALL_NEW
  simp_tac (HOL_basic_ss addsimps @{thms Collect_disj_eq[symmetric]}) THEN_ALL_NEW
  simp_tac (HOL_basic_ss addsimps @{thms de_Morgan_conj[symmetric]}) THEN_ALL_NEW
  simp_tac (HOL_basic_ss addsimps @{thms ex_simps(1,2)[symmetric]}) THEN_ALL_NEW
  simp_tac (HOL_ss addsimps @{thms Collect_const finite.emptyI})
*}



ML {*
fun build_eqvt_gl pi frees fnctn ctxt =
let
  val typ = domain_type (fastype_of fnctn);
  val arg = the (AList.lookup (op=) frees typ);
in
  ([HOLogic.mk_eq (mk_perm pi (fnctn $ arg), fnctn $ (mk_perm pi arg))], ctxt)
end
*}

ML {*
fun prove_eqvt tys ind simps funs ctxt =
let
  val ([pi], ctxt') = Variable.variant_fixes ["p"] ctxt;
  val pi = Free (pi, @{typ perm});
  val tac = asm_full_simp_tac (HOL_ss addsimps (@{thms atom_eqvt permute_list.simps} @ simps @ all_eqvts ctxt'))
  val ths_loc = prove_by_induct tys (build_eqvt_gl pi) ind tac funs ctxt'
  val ths = Variable.export ctxt' ctxt ths_loc
  val add_eqvt = Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)
in
  (ths, snd (Local_Theory.note ((Binding.empty, [add_eqvt]), ths) ctxt))
end
*}

end