(*  Title:      nominal_dt_rawperm.ML
    Author:     Cezary Kaliszyk
    Author:     Christian Urban

  Definitions of the raw permutations and
  proof that the raw datatypes are in the
  pt-class.
*)

signature NOMINAL_DT_RAWPERM =
sig
  val define_raw_perms: string list -> typ list -> term list -> thm -> local_theory -> 
    (term list * thm list * thm list) * local_theory
end


structure Nominal_Dt_RawPerm: NOMINAL_DT_RAWPERM =
struct


(** proves the two pt-type class properties **)

fun prove_permute_zero induct perm_defs perm_fns lthy =
let
  val perm_types = map (body_type o fastype_of) perm_fns
  val perm_indnames = Datatype_Prop.make_tnames perm_types
  
  fun single_goal ((perm_fn, T), x) =
    HOLogic.mk_eq (perm_fn $ @{term "0::perm"} $ Free (x, T), Free (x, T))

  val goals =
    HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
      (map single_goal (perm_fns ~~ perm_types ~~ perm_indnames)))

  val simps = HOL_basic_ss addsimps (@{thm permute_zero} :: perm_defs)

  val tac = (Datatype_Aux.indtac induct perm_indnames 
             THEN_ALL_NEW asm_simp_tac simps) 1
in
  Goal.prove lthy perm_indnames [] goals (K tac)
  |> Datatype_Aux.split_conj_thm
end


fun prove_permute_plus induct perm_defs perm_fns lthy =
let
  val p = Free ("p", @{typ perm})
  val q = Free ("q", @{typ perm})
  val perm_types = map (body_type o fastype_of) perm_fns
  val perm_indnames = Datatype_Prop.make_tnames perm_types
  
  fun single_goal ((perm_fn, T), x) = HOLogic.mk_eq 
      (perm_fn $ (mk_plus p q) $ Free (x, T), perm_fn $ p $ (perm_fn $ q $ Free (x, T)))

  val goals =
    HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
      (map single_goal (perm_fns ~~ perm_types ~~ perm_indnames)))

  val simps = HOL_basic_ss addsimps (@{thm permute_plus} :: perm_defs)

  val tac = (Datatype_Aux.indtac induct perm_indnames
             THEN_ALL_NEW asm_simp_tac simps) 1
in
  Goal.prove lthy ("p" :: "q" :: perm_indnames) [] goals (K tac)
  |> Datatype_Aux.split_conj_thm 
end


fun mk_perm_eq ty_perm_assoc cnstr = 
let
  fun lookup_perm p (ty, arg) = 
    case (AList.lookup (op=) ty_perm_assoc ty) of
      SOME perm => perm $ p $ arg
    | NONE => Const (@{const_name permute}, perm_ty ty) $ p $ arg

  val p = Free ("p", @{typ perm})
  val (arg_tys, ty) =
    fastype_of cnstr
    |> strip_type

  val arg_names = Name.variant_list ["p"] (Datatype_Prop.make_tnames arg_tys)
  val args = map Free (arg_names ~~ arg_tys)

  val lhs = lookup_perm p (ty, list_comb (cnstr, args))
  val rhs = list_comb (cnstr, map (lookup_perm p) (arg_tys ~~ args))
  
  val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))  
in
  (Attrib.empty_binding, eq)
end


fun define_raw_perms full_ty_names tys constrs induct_thm lthy =
let
  val perm_fn_names = full_ty_names
    |> map Long_Name.base_name
    |> map (prefix "permute_")

  val perm_fn_types = map perm_ty tys
  val perm_fn_frees = map Free (perm_fn_names ~~ perm_fn_types)
  val perm_fn_binds = map (fn s => (Binding.name s, NONE, NoSyn)) perm_fn_names

  val perm_eqs = map (mk_perm_eq (tys ~~ perm_fn_frees)) constrs

  fun tac _ (_, _, simps) =
    Class.intro_classes_tac [] THEN ALLGOALS (resolve_tac simps)
  
  fun morphism phi (fvs, dfs, simps) =
    (map (Morphism.term phi) fvs, 
     map (Morphism.thm phi) dfs, 
     map (Morphism.thm phi) simps);

  val ((perm_funs, perm_eq_thms), lthy') =
    lthy
    |> Local_Theory.exit_global
    |> Class.instantiation (full_ty_names, [], @{sort pt}) 
    |> Primrec.add_primrec perm_fn_binds perm_eqs
    
  val perm_zero_thms = prove_permute_zero induct_thm perm_eq_thms perm_funs lthy'
  val perm_plus_thms = prove_permute_plus induct_thm perm_eq_thms perm_funs lthy' 
in
  lthy'
  |> Class.prove_instantiation_exit_result morphism tac 
       (perm_funs, perm_eq_thms, perm_zero_thms @ perm_plus_thms)
  ||> Named_Target.theory_init
end


end (* structure *)