(*  Title:      nominal_library.ML
    Author:     Christian Urban

  Basic functions for nominal.
*)

signature NOMINAL_LIBRARY =
sig
  val last2: 'a list -> 'a * 'a

  val dest_listT: typ -> typ

  val mk_minus: term -> term
  val mk_plus: term -> term -> term

  val perm_ty: typ -> typ 
  val mk_perm_ty: typ -> term -> term -> term
  val mk_perm: term -> term -> term
  val dest_perm: term -> term * term

  val mk_sort_of: term -> term
  val atom_ty: typ -> typ
  val mk_atom_ty: typ -> term -> term
  val mk_atom: term -> term

  val supp_ty: typ -> typ
  val supp_const: typ -> term
  val mk_supp_ty: typ -> term -> term
  val mk_supp: term -> term

  val mk_equiv: thm -> thm
  val safe_mk_equiv: thm -> thm

  val mk_diff: term * term -> term
  val mk_append: term * term -> term
  val mk_union: term * term -> term
  val fold_union: term list -> term
  val mk_conj: term * term -> term
  val fold_conj: term list -> term

  (* datatype operations *)
  val all_dtyps: Datatype_Aux.descr -> (string * sort) list -> typ list
  val nth_dtyp: Datatype_Aux.descr -> (string * sort) list -> int -> typ
  val all_dtyp_constrs_types: Datatype_Aux.descr -> (string * sort) list -> 
    (term * typ * typ list * bool list) list list
  val nth_dtyp_constrs_types: Datatype_Aux.descr -> (string * sort) list -> int -> 
    (term * typ * typ list * bool list) list
  val prefix_dt_names: Datatype_Aux.descr -> (string * sort) list -> string -> string list

  (* tactics for function package *)
  val pat_completeness_auto: Proof.context -> tactic
  val pat_completeness_simp: thm list -> Proof.context -> tactic
  val prove_termination: Proof.context -> Function.info * local_theory

  (* transformations of premises in inductions *)
  val transform_prem1: Proof.context -> string list -> thm -> thm
  val transform_prem2: Proof.context -> string list -> thm -> thm

  (* transformation into the object logic *)
  val atomize: thm -> thm

end


structure Nominal_Library: NOMINAL_LIBRARY =
struct

fun last2 [] = raise Empty
  | last2 [_] = raise Empty
  | last2 [x, y] = (x, y)
  | last2 (_ :: xs) = last2 xs

fun dest_listT (Type (@{type_name list}, [T])) = T
  | dest_listT T = raise TYPE ("dest_listT: list type expected", [T], [])

fun mk_minus p = @{term "uminus::perm => perm"} $ p;

fun mk_plus p q = @{term "plus::perm => perm => perm"} $ p $ q;

fun perm_ty ty = @{typ "perm"} --> ty --> ty; 
fun mk_perm_ty ty p trm = Const (@{const_name "permute"}, perm_ty ty) $ p $ trm;
fun mk_perm p trm = mk_perm_ty (fastype_of trm) p trm;

fun dest_perm (Const (@{const_name "permute"}, _) $ p $ t) = (p, t)
  | dest_perm t = raise TERM ("dest_perm", [t]);

fun mk_sort_of t = @{term "sort_of"} $ t;

fun atom_ty ty = ty --> @{typ "atom"};
fun mk_atom_ty ty t = Const (@{const_name "atom"}, atom_ty ty) $ t;
fun mk_atom t = mk_atom_ty (fastype_of t) t;


fun supp_ty ty = ty --> @{typ "atom set"};
fun supp_const ty = Const (@{const_name "supp"}, supp_ty ty)
fun mk_supp_ty ty t = supp_const ty $ t;
fun mk_supp t = mk_supp_ty (fastype_of t) t;


fun mk_equiv r = r RS @{thm eq_reflection};
fun safe_mk_equiv r = mk_equiv r handle Thm.THM _ => r;


(* functions that construct differences, appends and unions
   but avoid producing empty atom sets or empty atom lists *)

fun mk_diff (@{term "{}::atom set"}, _) = @{term "{}::atom set"}
  | mk_diff (t1, @{term "{}::atom set"}) = t1
  | mk_diff (t1, t2) = HOLogic.mk_binop @{const_name minus} (t1, t2)

fun mk_append (t1, @{term "[]::atom list"}) = t1
  | mk_append (@{term "[]::atom list"}, t2) = t2
  | mk_append (t1, t2) = HOLogic.mk_binop @{const_name "append"} (t1, t2) 

fun mk_union (t1, @{term "{}::atom set"}) = t1
  | mk_union (@{term "{}::atom set"}, t2) = t2
  | mk_union (t1, t2) = HOLogic.mk_binop @{const_name "sup"} (t1, t2)  
 
fun fold_union trms = fold_rev (curry mk_union) trms @{term "{}::atom set"}

fun mk_conj (t1, @{term "True"}) = t1
  | mk_conj (@{term "True"}, t2) = t2
  | mk_conj (t1, t2) = HOLogic.mk_conj (t1, t2)

fun fold_conj trms = fold_rev (curry mk_conj) trms @{term "True"}

(** datatypes **)


(* returns the type of the nth datatype *)
fun all_dtyps descr sorts = 
  map (fn n => Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec n)) (0 upto (length descr - 1))

fun nth_dtyp descr sorts n = 
  Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec n);

(* returns info about constructors in a datatype *)
fun all_dtyp_constrs_info descr = 
  map (fn (_, (ty, vs, constrs)) => map (pair (ty, vs)) constrs) descr

(* returns the constants of the constructors plus the 
   corresponding type and types of arguments *)
fun all_dtyp_constrs_types descr sorts = 
let
  fun aux ((ty_name, vs), (cname, args)) =
  let
    val vs_tys = map (Datatype_Aux.typ_of_dtyp descr sorts) vs
    val ty = Type (ty_name, vs_tys)
    val arg_tys = map (Datatype_Aux.typ_of_dtyp descr sorts) args
    val is_rec = map Datatype_Aux.is_rec_type args
  in
    (Const (cname, arg_tys ---> ty), ty, arg_tys, is_rec)
  end
in
  map (map aux) (all_dtyp_constrs_info descr)
end

fun nth_dtyp_constrs_types descr sorts n =
  nth (all_dtyp_constrs_types descr sorts) n


(* generates for every datatype a name str ^ dt_name 
   plus and index for multiple occurences of a string *)
fun prefix_dt_names descr sorts str = 
let
  fun get_nth_name (i, _) = 
    Datatype_Aux.name_of_typ (nth_dtyp descr sorts i) 
in
  Datatype_Prop.indexify_names 
    (map (prefix str o get_nth_name) descr)
end



(** function package tactics **)

fun pat_completeness_auto lthy =
  Pat_Completeness.pat_completeness_tac lthy 1
    THEN auto_tac (clasimpset_of lthy)

fun pat_completeness_simp simps lthy =
let
  val simp_set = HOL_basic_ss addsimps (@{thms sum.inject sum.distinct} @ simps)
in
  Pat_Completeness.pat_completeness_tac lthy 1
    THEN ALLGOALS (asm_full_simp_tac simp_set)
end

fun prove_termination lthy =
  Function.prove_termination NONE
    (Lexicographic_Order.lexicographic_order_tac true lthy) lthy


(** transformations of premises (in inductive proofs) **)

(* 
 given the theorem F[t]; proves the theorem F[f t] 

  - F needs to be monotone
  - f returns either SOME for a term it fires on 
    and NONE elsewhere 
*)
fun map_term f t = 
  (case f t of
     NONE => map_term' f t 
   | x => x)
and map_term' f (t $ u) = 
    (case (map_term f t, map_term f u) of
        (NONE, NONE) => NONE
      | (SOME t'', NONE) => SOME (t'' $ u)
      | (NONE, SOME u'') => SOME (t $ u'')
      | (SOME t'', SOME u'') => SOME (t'' $ u''))
  | map_term' f (Abs (s, T, t)) = 
      (case map_term f t of
        NONE => NONE
      | SOME t'' => SOME (Abs (s, T, t'')))
  | map_term' _ _  = NONE;

fun map_thm_tac ctxt tac thm =
let
  val monos = Inductive.get_monos ctxt
  val simps = HOL_basic_ss addsimps @{thms split_def}
in
  EVERY [cut_facts_tac [thm] 1, etac rev_mp 1, 
    REPEAT_DETERM (FIRSTGOAL (simp_tac simps THEN' resolve_tac monos)),
    REPEAT_DETERM (rtac impI 1 THEN (atac 1 ORELSE tac))]
end

fun map_thm ctxt f tac thm =
let
  val opt_goal_trm = map_term f (prop_of thm)
in
  case opt_goal_trm of
    NONE => thm
  | SOME goal =>
     Goal.prove ctxt [] [] goal (fn _ => map_thm_tac ctxt tac thm) 
end

(*
 inductive premises can be of the form
 R ... /\ P ...; split_conj_i picks out
 the part R or P part
*)
fun split_conj1 names (Const ("op &", _) $ f1 $ f2) = 
  (case head_of f1 of
     Const (name, _) => if member (op =) names name then SOME f1 else NONE
   | _ => NONE)
| split_conj1 _ _ = NONE;

fun split_conj2 names (Const ("op &", _) $ f1 $ f2) = 
  (case head_of f1 of
     Const (name, _) => if member (op =) names name then SOME f2 else NONE
   | _ => NONE)
| split_conj2 _ _ = NONE;

fun transform_prem1 ctxt names thm =
  map_thm ctxt (split_conj1 names) (etac conjunct1 1) thm

fun transform_prem2 ctxt names thm =
  map_thm ctxt (split_conj2 names) (etac conjunct2 1) thm


(* transformes a theorem into one of the object logic *)
val atomize = Conv.fconv_rule Object_Logic.atomize o forall_intr_vars

end (* structure *)

open Nominal_Library;