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)
|> snd o Local_Theory.note ((bind, []), user_thms)
end
*}



ML {*
fun fvbv_rsp_tac induct fvbv_simps =
  ((((rtac impI THEN' etac induct) ORELSE' rtac induct) THEN_ALL_NEW
  (TRY o rtac @{thm TrueI})) THEN_ALL_NEW asm_full_simp_tac
  (HOL_ss addsimps (@{thm alpha_gen} :: fvbv_simps)))
*}

ML {*
fun constr_rsp_tac inj rsp equivps =
let
  val reflps = map (fn x => @{thm equivp_reflp} OF [x]) equivps
in
  REPEAT o rtac impI THEN'
  simp_tac (HOL_ss addsimps inj) THEN'
  (TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI)) THEN_ALL_NEW
  (asm_simp_tac HOL_ss THEN_ALL_NEW (
   rtac @{thm exI[of _ "0 :: perm"]} THEN'
   asm_full_simp_tac (HOL_ss addsimps (rsp @ reflps @
     @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv}))
  ))
end
*}

(* Testing code
local_setup {* 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 bind funs perms simps induct 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 (map body_type types));
  val args = map Free (indnames ~~ types);
  val perm_at = @{term "permute :: perm \<Rightarrow> atom set \<Rightarrow> atom set"}
  fun eqvtc (fnctn, (arg, perm)) =
    HOLogic.mk_eq ((perm_at $ pi $ (fnctn $ arg)), (fnctn $ (perm $ pi $ arg)))
  val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map eqvtc (funs ~~ (args ~~ perms))))
  fun tac _ = (Datatype_Aux.indtac induct indnames THEN_ALL_NEW
    (asm_full_simp_tac (HOL_ss addsimps
      (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ simps)))) 1
  val thm = Goal.prove ctxt ("p" :: indnames) [] gl tac
  val thms = HOLogic.conj_elims thm
in
  Local_Theory.note ((bind, [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), thms) ctxt
end
*}


ML {*
fun build_alpha_eqvts funs perms simps induct 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 (map body_type types));
  val indnames2 = Name.variant_list ("p" :: indnames) (Datatype_Prop.make_tnames (map body_type types));
  val args = map Free (indnames ~~ types);
  val args2 = map Free (indnames2 ~~ types);
  fun eqvtc ((alpha, perm), (arg, arg2)) =
    HOLogic.mk_imp (alpha $ arg $ arg2,
      (alpha $ (perm $ pi $ arg) $ (perm $ pi $ arg2)))
  val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map eqvtc ((funs ~~ perms) ~~ (args ~~ args2))))
  fun tac _ = (((rtac impI THEN' etac induct) ORELSE' rtac induct) THEN_ALL_NEW
    (asm_full_simp_tac (HOL_ss addsimps 
      (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ simps)))
    THEN_ALL_NEW (TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) THEN_ALL_NEW
      (etac @{thm alpha_gen_compose_eqvt})) THEN_ALL_NEW
    (asm_full_simp_tac (HOL_ss addsimps 
      (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ simps)))
) 1
  val thm = Goal.prove ctxt ("p" :: indnames @ indnames2) [] gl tac
in
  map (fn x => mp OF [x]) (HOLogic.conj_elims thm)
end
*}


end