theory Rsp

imports Abs

begin

ML {*

fun define_quotient_type args tac ctxt =

let

  val mthd = Method.SIMPLE_METHOD tac

  val mthdt = Method.Basic (fn _ => mthd)

  val bymt = Proof.global_terminal_proof (mthdt, NONE)

in

  bymt (Quotient_Type.quotient_type args ctxt)

end

*}

ML {*

fun const_rsp lthy const =

let

  val nty = fastype_of (Quotient_Term.quotient_lift_const ("", const) lthy)

  val rel = Quotient_Term.equiv_relation_chk lthy (fastype_of const, nty);

in

  HOLogic.mk_Trueprop (rel $ const $ const)

end

*}

(* Replaces bounds by frees and meta implications by implications *)

ML {*

fun prepare_goal trm =

let

  val vars = strip_all_vars trm

  val fs = rev (map Free vars)

  val (fixes, no_alls) = ((map fst vars), subst_bounds (fs, (strip_all_body trm)))

  val prems = map HOLogic.dest_Trueprop (Logic.strip_imp_prems no_alls)

  val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl no_alls)

in

  (fixes, fold (curry HOLogic.mk_imp) prems concl)

end

*}

ML {*

fun get_rsp_goal thy trm =

let

  val goalstate = Goal.init (cterm_of thy trm);

  val tac = REPEAT o rtac @{thm fun_rel_id};

in

  case (SINGLE (tac 1) goalstate) of

    NONE => error "rsp_goal failed"

  | SOME th => prepare_goal (term_of (cprem_of th 1))

end

*}

ML {*

fun repeat_mp thm = repeat_mp (mp OF [thm]) handle THM _ => thm

*}

ML {*

fun prove_const_rsp bind consts tac ctxt =

let

  val rsp_goals = map (const_rsp ctxt) consts

  val thy = ProofContext.theory_of ctxt

  val (fixed, user_goals) = split_list (map (get_rsp_goal thy) rsp_goals)

  val fixed' = distinct (op =) (flat fixed)

  val user_goal = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj user_goals)

  val user_thm = Goal.prove ctxt fixed' [] user_goal tac

  val user_thms = map repeat_mp (HOLogic.conj_elims user_thm)

  fun tac _ = (REPEAT o rtac @{thm fun_rel_id} THEN' resolve_tac user_thms THEN_ALL_NEW atac) 1

  val rsp_thms = map (fn gl => Goal.prove ctxt [] [] gl tac) rsp_goals

in

   ctxt

|> snd o Local_Theory.note 

  ((Binding.empty, [Attrib.internal (fn _ => Quotient_Info.rsp_rules_add)]), rsp_thms)

|> Local_Theory.note ((bind, []), user_thms)

end

*}

ML {*

fun ind_tac induct = (rtac impI THEN' etac induct) ORELSE' rtac induct

*}

ML {*

fun fvbv_rsp_tac induct fvbv_simps ctxt =

  ind_tac induct THEN_ALL_NEW

  (TRY o rtac @{thm TrueI}) THEN_ALL_NEW

  asm_full_simp_tac (HOL_basic_ss addsimps @{thms alpha_gen2}) THEN_ALL_NEW

  asm_full_simp_tac (HOL_ss addsimps (@{thm alpha_gen} :: fvbv_simps)) THEN_ALL_NEW

  REPEAT o eresolve_tac [conjE, exE] THEN_ALL_NEW

  asm_full_simp_tac (HOL_ss addsimps fvbv_simps) THEN_ALL_NEW

  TRY o blast_tac (claset_of ctxt)

*}

ML {*

fun sym_eqvts ctxt = map (fn x => sym OF [x]) (Nominal_ThmDecls.get_eqvts_thms ctxt)

fun all_eqvts ctxt =

  Nominal_ThmDecls.get_eqvts_thms ctxt @ Nominal_ThmDecls.get_eqvts_raw_thms ctxt

val split_conjs = REPEAT o etac conjE THEN' TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI)

*}

ML {*

fun constr_rsp_tac inj rsp =

  REPEAT o rtac impI THEN'

  simp_tac (HOL_ss addsimps inj) THEN' split_conjs THEN_ALL_NEW

  (asm_simp_tac HOL_ss THEN_ALL_NEW (

   REPEAT o rtac @{thm exI[of _ "0 :: perm"]} THEN_ALL_NEW

   simp_tac (HOL_basic_ss addsimps @{thms alpha_gen2}) THEN_ALL_NEW

   asm_full_simp_tac (HOL_ss addsimps (rsp @

     @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv add_0_left}))

  ))

*}

(* Testing code

local_setup {* snd o prove_const_rsp @{binding fv_rtrm2_rsp} [@{term rbv2}]

  (fn _ => fv_rsp_tac @{thm alpha_rtrm2_alpha_rassign.inducts(2)} @{thms fv_rtrm2_fv_rassign.simps} 1) *}*)

(*ML {*

  val rsp_goals = map (const_rsp @{context}) [@{term rbv2}]

  val (fixed, user_goals) = split_list (map (get_rsp_goal @{theory}) rsp_goals)

  val fixed' = distinct (op =) (flat fixed)

  val user_goal = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj user_goals)

*}

prove ug: {* user_goal *}

ML_prf {*

val induct = @{thm alpha_rtrm2_alpha_rassign.inducts(2)}

val fv_simps = @{thms rbv2.simps}

*} 

*)

ML {*

fun build_eqvts_tac induct simps ctxt inds _ = (Datatype_Aux.indtac induct inds THEN_ALL_NEW

    (asm_full_simp_tac (HOL_ss addsimps

      (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ (Nominal_ThmDecls.get_eqvts_raw_thms ctxt) @ simps)))) 1

*}

ML {*

fun perm_arg arg =

let

  val ty = fastype_of arg

in

  Const (@{const_name permute}, @{typ perm} --> ty --> ty)

end

*}

ML {*

fun build_eqvts bind funs tac ctxt =

let

  val pi = Free ("p", @{typ perm});

  val types = map (domain_type o fastype_of) funs;

  val indnames = Name.variant_list ["p"] (Datatype_Prop.make_tnames types);

  val args = map Free (indnames ~~ types);

  val perm_at = @{term "permute :: perm \<Rightarrow> atom set \<Rightarrow> atom set"}

  fun eqvtc (fnctn, arg) =

    HOLogic.mk_eq ((perm_at $ pi $ (fnctn $ arg)), (fnctn $ (perm_arg arg $ pi $ arg)))

  val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map eqvtc (funs ~~ args)))

  val thm = Goal.prove ctxt ("p" :: indnames) [] gl (tac indnames)

  val thms = HOLogic.conj_elims thm

in

  Local_Theory.note ((bind, [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), thms) ctxt

end

*}

lemma exi: "\<exists>(pi :: perm). P pi \<Longrightarrow> (\<And>(p :: perm). P p \<Longrightarrow> Q (pi \<bullet> p)) \<Longrightarrow> \<exists>pi. Q pi"

apply (erule exE)

apply (rule_tac x="pi \<bullet> pia" in exI)

by auto

ML {*

fun mk_minimal_ss ctxt =

  Simplifier.context ctxt empty_ss

    setsubgoaler asm_simp_tac

    setmksimps (mksimps [])

*}

ML {*

fun alpha_eqvt_tac induct simps ctxt =

  ind_tac induct THEN_ALL_NEW

  simp_tac ((mk_minimal_ss ctxt) addsimps simps) THEN_ALL_NEW

  REPEAT o etac @{thm exi[of _ _ "p"]} THEN' split_conjs THEN_ALL_NEW

  asm_full_simp_tac (HOL_ss addsimps (all_eqvts ctxt @ simps)) THEN_ALL_NEW

  asm_full_simp_tac (HOL_ss addsimps 

    @{thms supp_eqvt[symmetric] inter_eqvt[symmetric] empty_eqvt alpha_gen}) THEN_ALL_NEW

  (split_conjs THEN_ALL_NEW TRY o resolve_tac

    @{thms fresh_star_permute_iff[of "- p", THEN iffD1] permute_eq_iff[of "- p", THEN iffD1]})

  THEN_ALL_NEW

  asm_full_simp_tac (HOL_ss addsimps (@{thms split_conv permute_minus_cancel permute_plus permute_eqvt[symmetric]} @ all_eqvts ctxt @ simps))

*}

ML {*

fun build_alpha_eqvt alpha names =

let

  val pi = Free ("p", @{typ perm});

  val (tys, _) = strip_type (fastype_of alpha)

  val indnames = Name.variant_list names (Datatype_Prop.make_tnames (map body_type tys));

  val args = map Free (indnames ~~ tys);

  val perm_args = map (fn x => perm_arg x $ pi $ x) args

in

  (HOLogic.mk_imp (list_comb (alpha, args), list_comb (alpha, perm_args)), indnames @ names)

end

*}

ML {* fold_map build_alpha_eqvt *}

ML {*

fun build_alpha_eqvts funs tac ctxt =

let

  val (gls, names) = fold_map build_alpha_eqvt funs ["p"]

  val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj gls)

  val thm = Goal.prove ctxt names [] gl tac

in

  map (fn x => mp OF [x]) (HOLogic.conj_elims thm)

end

*}

ML {*

fun build_bv_eqvt simps inducts (t, n) ctxt =

  build_eqvts Binding.empty [t] (build_eqvts_tac (nth inducts n) simps ctxt) ctxt

*}

ML {*

fun prove_fv_rsp fv_alphas_lst all_alphas tac ctxt =

let

  val (fvs_alphas, ls) = split_list fv_alphas_lst;

  val (fv_ts, alpha_ts) = split_list fvs_alphas;

  val tys = map (domain_type o fastype_of) alpha_ts;

  val names = Datatype_Prop.make_tnames tys;

  val names2 = Name.variant_list names names;

  val args = map Free (names ~~ tys);

  val args2 = map Free (names2 ~~ tys);

  fun mk_fv_rsp arg arg2 (fv, alpha) = HOLogic.mk_eq ((fv $ arg), (fv $ arg2));

  fun fv_rsp_arg (((fv, alpha), (arg, arg2)), l) =

    HOLogic.mk_imp (

     (alpha $ arg $ arg2),

     (foldr1 HOLogic.mk_conj

       (HOLogic.mk_eq (fv $ arg, fv $ arg2) ::

       (map (mk_fv_rsp arg arg2) l))));

  val nobn_eqs = map fv_rsp_arg (((fv_ts ~~ alpha_ts) ~~ (args ~~ args2)) ~~ ls);

  fun mk_fv_rsp_bn arg arg2 (fv, alpha) =

    HOLogic.mk_imp (

      (alpha $ arg $ arg2),

      HOLogic.mk_eq ((fv $ arg), (fv $ arg2)));

  fun fv_rsp_arg_bn ((arg, arg2), l) =

    map (mk_fv_rsp_bn arg arg2) l;

  val bn_eqs = flat (map fv_rsp_arg_bn ((args ~~ args2) ~~ ls));

  val (_, add_alphas) = chop (length (nobn_eqs @ bn_eqs)) all_alphas;

  val atys = map (domain_type o fastype_of) add_alphas;

  val anames = Name.variant_list (names @ names2) (Datatype_Prop.make_tnames atys);

  val aargs = map Free (anames ~~ atys);

  val aeqs = map2 (fn alpha => fn arg => HOLogic.mk_imp (alpha $ arg $ arg, @{term True}))

    add_alphas aargs;

  val eq = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (nobn_eqs @ bn_eqs @ aeqs));

  val th = Goal.prove ctxt (names @ names2) [] eq tac;

  val ths = HOLogic.conj_elims th;

  val (ths_nobn, ths_bn) = chop (length ls) ths;

  fun project (th, l) =

    Project_Rule.projects ctxt (1 upto (length l + 1)) (hd (Project_Rule.projections ctxt th))

  val ths_nobn_pr = map project (ths_nobn ~~ ls);

in

  (flat ths_nobn_pr @ ths_bn)

end

*}

lemma equivp_rspl:

  "equivp r \<Longrightarrow> r a b \<Longrightarrow> r a c = r b c"

  unfolding equivp_reflp_symp_transp symp_def transp_def 

  by blast

lemma equivp_rspr:

  "equivp r \<Longrightarrow> r a b \<Longrightarrow> r c a = r c b"

  unfolding equivp_reflp_symp_transp symp_def transp_def 

  by blast

ML {*

fun prove_alpha_bn_rsp alphas inducts exhausts inj_dis equivps ctxt (alpha_bn, n) =

let

  val alpha = nth alphas n;

  val ty = domain_type (fastype_of alpha);

  val ([x, y, a], ctxt') = Variable.variant_fixes ["x","y","a"] ctxt;

  val [l, r] = map (fn x => (Free (x, ty))) [x, y]

  val lhs = HOLogic.mk_Trueprop (alpha $ l $ r)

  val g1 =

    Logic.mk_implies (lhs,

      HOLogic.mk_Trueprop (HOLogic.mk_all (a, ty,

        HOLogic.mk_eq (alpha_bn $ l $ Bound 0, alpha_bn $ r $ Bound 0))));

  val g2 =

    Logic.mk_implies (lhs,

      HOLogic.mk_Trueprop (HOLogic.mk_all (a, ty,

        HOLogic.mk_eq (alpha_bn $ Bound 0 $ l, alpha_bn $ Bound 0 $ r))));

  val resl = map (fn x => @{thm equivp_rspl} OF [x]) equivps;

  val resr = map (fn x => @{thm equivp_rspr} OF [x]) equivps;

  fun tac {context, ...} = (

    etac (nth inducts n) THEN_ALL_NEW

    (TRY o rtac @{thm TrueI}) THEN_ALL_NEW rtac allI THEN_ALL_NEW

    split_conjs THEN_ALL_NEW

    InductTacs.case_rule_tac context a (nth exhausts n) THEN_ALL_NEW

    asm_full_simp_tac (HOL_ss addsimps inj_dis) THEN_ALL_NEW

    TRY o REPEAT_ALL_NEW (rtac @{thm arg_cong2[of _ _ _ _ "op \<and>"]}) THEN_ALL_NEW

    TRY o eresolve_tac (resl @ resr) THEN_ALL_NEW

    asm_full_simp_tac (HOL_ss addsimps inj_dis)

  ) 1;

  val t1 = Goal.prove ctxt [] [] g1 tac;

  val t2 = Goal.prove ctxt [] [] g2 tac;

in

  Variable.export ctxt' ctxt [t1, t2]

end

*}

end