(*  Title:      nominal_library.ML

    Author:     Christian Urban

  Basic functions for nominal.

*)

signature NOMINAL_LIBRARY =

sig

  val last2: 'a list -> 'a * 'a

  val order: ('a * 'a -> bool) -> 'a list -> ('a * 'b) list -> 'b list

  val remove_dups: ('a * 'a -> bool) -> 'a list -> 'a list

  val map4: ('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list -> 'c list -> 'd list -> 'e list

  val split_filter: ('a -> bool) -> 'a list -> 'a list * 'a list

  val fold_left: ('a * 'a -> 'a) -> 'a list -> 'a -> 'a

  val is_true: term -> bool

  val dest_listT: typ -> typ

  val dest_fsetT: typ -> typ

  val mk_id: term -> term

  val mk_all: (string * typ) -> term -> term

  val sum_case_const: typ -> typ -> typ -> term

  val mk_sum_case: term -> term -> term

  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 atom_const: typ -> term

  val mk_atom_ty: typ -> term -> term

  val mk_atom: term -> term

  val mk_atom_set_ty: typ -> term -> term

  val mk_atom_set: term -> term

  val mk_atom_fset_ty: typ -> term -> term

  val mk_atom_fset: term -> term

  val mk_atom_list_ty: typ -> term -> term

  val mk_atom_list: term -> term

  val is_atom: Proof.context -> typ -> bool

  val is_atom_set: Proof.context -> typ -> bool

  val is_atom_fset: Proof.context -> typ -> bool

  val is_atom_list: Proof.context -> typ -> bool

  val to_set_ty: typ -> term -> term

  val to_set: term -> term

  val atomify_ty: Proof.context -> typ -> term -> term

  val atomify: Proof.context -> term -> term

  val setify_ty: Proof.context -> typ -> term -> term

  val setify: Proof.context -> term -> term

  val listify_ty: Proof.context -> typ -> term -> term

  val listify: Proof.context -> term -> term

  val fresh_star_ty: typ -> typ

  val fresh_star_const: typ -> term

  val mk_fresh_star_ty: typ -> term -> term -> term

  val mk_fresh_star: term -> 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 supp_rel_ty: typ -> typ

  val supp_rel_const: typ -> term

  val mk_supp_rel_ty: typ -> term -> term -> term

  val mk_supp_rel: term -> term -> term		       

  val supports_const: typ -> term

  val mk_supports_ty: typ -> term -> term -> term

  val mk_supports: term -> term -> term

  val finite_const: typ -> term

  val mk_finite_ty: typ -> term -> term

  val mk_finite: 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 fold_append: term list -> term

  val mk_conj: term * term -> term

  val fold_conj: term list -> term

  (* functions for de-Bruijn open terms *)

  val mk_binop_env: typ list -> string -> term * term -> term

  val mk_union_env: typ list -> term * term -> term

  val fold_union_env: typ list -> term list -> term

  (* fresh arguments for a term *)

  val fresh_args: Proof.context -> term -> term list

  (* some logic operations *)

  val strip_full_horn: term -> (string * typ) list * term list * term

  val mk_full_horn: (string * typ) list -> term list -> term -> term

  (* datatype operations *)

  type cns_info = (term * typ * typ list * bool list) list

  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 -> cns_info list

  val nth_dtyp_constrs_types: Datatype_Aux.descr -> (string * sort) list -> int -> cns_info

  val prefix_dt_names: Datatype_Aux.descr -> (string * sort) list -> string -> string list

  (* tactics for function package *)

  val pat_completeness_simp: thm list -> Proof.context -> tactic

  val prove_termination: thm list -> 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

  (* applies a tactic to a formula composed of conjunctions *)

  val conj_tac: (int -> tactic) -> int -> tactic

end

structure Nominal_Library: NOMINAL_LIBRARY =

struct

(* orders an AList according to keys *)

fun order eq keys list = 

  map (the o AList.lookup eq list) keys

(* remove duplicates *)

fun remove_dups eq [] = []

  | remove_dups eq (x :: xs) = 

      if member eq xs x 

      then remove_dups eq xs 

      else x :: remove_dups eq xs

fun last2 [] = raise Empty

  | last2 [_] = raise Empty

  | last2 [x, y] = (x, y)

  | last2 (_ :: xs) = last2 xs

fun map4 _ [] [] [] [] = []

  | map4 f (x :: xs) (y :: ys) (z :: zs) (u :: us) = f x y z u :: map4 f xs ys zs us

fun split_filter f [] = ([], [])

  | split_filter f (x :: xs) =

      let 

        val (r, l) = split_filter f xs 

      in 

        if f x 

        then (x :: r, l) 

        else (r, x :: l) 

      end

(* to be used with left-infix binop-operations *)

fun fold_left f [] z = z

  | fold_left f [x] z = x

  | fold_left f (x :: y :: xs) z = fold_left f (f (x, y) :: xs) z

fun is_true @{term "Trueprop True"} = true

  | is_true _ = false 

fun dest_listT (Type (@{type_name list}, [T])) = T

  | dest_listT T = raise TYPE ("dest_listT: list type expected", [T], [])

fun dest_fsetT (Type (@{type_name fset}, [T])) = T

  | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []);

fun mk_id trm = HOLogic.id_const (fastype_of trm) $ trm

fun mk_all (a, T) t =  Term.all T $ Abs (a, T, t)

fun sum_case_const ty1 ty2 ty3 = 

  Const (@{const_name sum_case}, [ty1 --> ty3, ty2 --> ty3, Type (@{type_name sum}, [ty1, ty2])] ---> ty3)

fun mk_sum_case trm1 trm2 =

  let

    val ([ty1], ty3) = strip_type (fastype_of trm1)

    val ty2 = domain_type (fastype_of trm2)

  in

    sum_case_const ty1 ty2 ty3 $ trm1 $ trm2

  end 

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 atom_const ty = Const (@{const_name "atom"}, atom_ty ty)

fun mk_atom_ty ty t = atom_const ty $ t;

fun mk_atom t = mk_atom_ty (fastype_of t) t;

fun mk_atom_set_ty ty t =

  let

    val atom_ty = HOLogic.dest_setT ty 

    val img_ty = (atom_ty --> @{typ atom}) --> ty --> @{typ "atom set"};

  in

    Const (@{const_name image}, img_ty) $ atom_const atom_ty $ t

  end

fun mk_atom_fset_ty ty t =

  let

    val atom_ty = dest_fsetT ty

    val fmap_ty = (atom_ty --> @{typ atom}) --> ty --> @{typ "atom fset"};

  in

    Const (@{const_name map_fset}, fmap_ty) $ atom_const atom_ty $ t

  end

fun mk_atom_list_ty ty t =

  let

    val atom_ty = dest_listT ty

    val map_ty = (atom_ty --> @{typ atom}) --> ty --> @{typ "atom list"}

  in

    Const (@{const_name map}, map_ty) $ atom_const atom_ty $ t

  end

fun mk_atom_set t = mk_atom_set_ty (fastype_of t) t

fun mk_atom_fset t = mk_atom_fset_ty (fastype_of t) t

fun mk_atom_list t = mk_atom_list_ty (fastype_of t) t

(* coerces a list into a set *)

fun to_set_ty ty t =

  case ty of

    @{typ "atom list"} => @{term "set :: atom list => atom set"} $ t

  | @{typ "atom fset"} => @{term "fset :: atom fset => atom set"} $ t

  | _ => t

fun to_set t = to_set_ty (fastype_of t) t

(* testing for concrete atom types *)

fun is_atom ctxt ty =

  Sign.of_sort (ProofContext.theory_of ctxt) (ty, @{sort at_base})

fun is_atom_set ctxt (Type ("fun", [ty, @{typ bool}])) = is_atom ctxt ty

  | is_atom_set _ _ = false;

fun is_atom_fset ctxt (Type (@{type_name "fset"}, [ty])) = is_atom ctxt ty

  | is_atom_fset _ _ = false;

fun is_atom_list ctxt (Type (@{type_name "list"}, [ty])) = is_atom ctxt ty

  | is_atom_list _ _ = false

(* functions that coerce singletons, sets, fsets and lists of concrete 

   atoms into general atoms sets / lists *)

fun atomify_ty ctxt ty t =

  if is_atom ctxt ty

    then  mk_atom_ty ty t

  else if is_atom_set ctxt ty

    then mk_atom_set_ty ty t

  else if is_atom_fset ctxt ty

    then mk_atom_fset_ty ty t

  else if is_atom_list ctxt ty

    then mk_atom_list_ty ty t

  else raise TERM ("atomify", [t])

fun setify_ty ctxt ty t =

  if is_atom ctxt ty

    then  HOLogic.mk_set @{typ atom} [mk_atom_ty ty t]

  else if is_atom_set ctxt ty

    then mk_atom_set_ty ty t

  else if is_atom_fset ctxt ty

    then @{term "fset :: atom fset => atom set"} $ mk_atom_fset_ty ty t

  else if is_atom_list ctxt ty

    then @{term "set :: atom list => atom set"} $ mk_atom_list_ty ty t

  else raise TERM ("setify", [t])

fun listify_ty ctxt ty t =

  if is_atom ctxt ty

    then HOLogic.mk_list @{typ atom} [mk_atom_ty ty t]

  else if is_atom_list ctxt ty

    then mk_atom_list_ty ty t

  else raise TERM ("listify", [t])

fun atomify ctxt t = atomify_ty ctxt (fastype_of t) t

fun setify ctxt t  = setify_ty ctxt (fastype_of t) t

fun listify ctxt t = listify_ty ctxt (fastype_of t) t

fun fresh_star_ty ty = [@{typ "atom set"}, ty] ---> @{typ bool}

fun fresh_star_const ty = Const (@{const_name fresh_star}, fresh_star_ty ty)

fun mk_fresh_star_ty ty t1 t2 = fresh_star_const ty $ t1 $ t2

fun mk_fresh_star t1 t2 = mk_fresh_star_ty (fastype_of t2) t1 t2

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 supp_rel_ty ty = ([ty, ty] ---> @{typ bool}) --> ty --> @{typ "atom set"};

fun supp_rel_const ty = Const (@{const_name supp_rel}, supp_rel_ty ty)

fun mk_supp_rel_ty ty r t = supp_rel_const ty $ r $ t

fun mk_supp_rel r t = mk_supp_rel_ty (fastype_of t) r t

fun supports_const ty = Const (@{const_name supports}, [@{typ "atom set"}, ty] ---> @{typ bool});

fun mk_supports_ty ty t1 t2 = supports_const ty $ t1 $ t2;

fun mk_supports t1 t2 = mk_supports_ty (fastype_of t2) t1 t2;

fun finite_const ty = Const (@{const_name finite}, ty --> @{typ bool})

fun mk_finite_ty ty t = finite_const ty $ t

fun mk_finite t = mk_finite_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 (@{term "set ([]::atom list)"}, _) = @{term "set ([]::atom list)"}

  | mk_diff (t1, @{term "set ([]::atom list)"}) = 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, @{term "set ([]::atom list)"}) = t1

  | mk_union (@{term "set ([]::atom list)"}, 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 fold_append trms = fold_rev (curry mk_append) trms @{term "[]::atom list"}

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"}

(* functions for de-Bruijn open terms *)

fun mk_binop_env tys c (t, u) =

  let 

    val ty = fastype_of1 (tys, t) 

  in

    Const (c, [ty, ty] ---> ty) $ t $ u

  end

fun mk_union_env tys (t1, @{term "{}::atom set"}) = t1

  | mk_union_env tys (@{term "{}::atom set"}, t2) = t2

  | mk_union_env tys (t1, @{term "set ([]::atom list)"}) = t1

  | mk_union_env tys (@{term "set ([]::atom list)"}, t2) = t2

  | mk_union_env tys (t1, t2) = mk_binop_env tys @{const_name "sup"} (t1, t2)  

fun fold_union_env tys trms = fold_left (mk_union_env tys) trms @{term "{}::atom set"} 

(* produces fresh arguments for a term *)

fun fresh_args ctxt f =

    f |> fastype_of

      |> binder_types

      |> map (pair "z")

      |> Variable.variant_frees ctxt [f]

      |> map Free

(** some logic operations **)

(* decompses a formula into params, premises and a conclusion *)

fun strip_full_horn trm =

  let

    fun strip_outer_params (Const ("all", _) $ Abs (a, T, t)) = strip_outer_params t |>> cons (a, T)

    | strip_outer_params B = ([], B)

    val (params, body) = strip_outer_params trm

    val (prems, concl) = Logic.strip_horn body

  in

    (params, prems, concl)

  end

(* composes a formula out of params, premises and a conclusion *)

fun mk_full_horn params prems concl =

  Logic.list_implies (prems, concl)

  |> fold_rev mk_all params

(** datatypes **)

(* constructor infos *)

type cns_info = (term * typ * typ list * bool list) list

(*  - term for constructor constant

    - type of the constructor

    - types of the arguments

    - flags indicating whether the argument is recursive

*)

(* 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_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_tac size_simps ctxt =

  let

    val natT = @{typ nat}

    fun prod_size_const fT sT = 

      let

        val fT_fun = fT --> natT

        val sT_fun = sT --> natT

        val prodT = Type (@{type_name prod}, [fT, sT])

      in