(*  Title:      nominal_library.ML+
−
    Author:     Christian Urban+
−
+
−
  Basic functions for nominal.+
−
*)+
−
+
−
signature NOMINAL_LIBRARY =+
−
sig+
−
  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+
−
+
−
  (* 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+
−
+
−
end+
−
+
−
+
−
structure Nominal_Library: NOMINAL_LIBRARY =+
−
struct+
−
+
−
(* this function should be in hologic.ML *)+
−
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 (@{term "[]::atom list"}, @{term "[]::atom list"}) = @{term "[]::atom list"}+
−
  | 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 (@{term "{}::atom set"}, @{term "{}::atom set"}) = @{term "{}::atom set"}+
−
  | 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 (curry mk_union) trms @{term "{}::atom set"}+
−
+
−
+
−
+
−
+
−
(** 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+
−
+
−
+
−
end (* structure *)+
−
+
−
open Nominal_Library;+
−