(* 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 (* 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 -> thmendstructure 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) endin map (map aux) (all_dtyp_constrs_info descr)endfun 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)endfun 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))]endfun 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) thmfun transform_prem2 ctxt names thm = map_thm ctxt (split_conj2 names) (etac conjunct2 1) thmend (* structure *)open Nominal_Library;