(* 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+ −
+ −
(* 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+ −
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 (@{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+ −
+ −
+ −
+ −
(** 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+ −
+ −
+ −
+ −
end (* structure *)+ −
+ −
open Nominal_Library;+ −