diff -r 41137dc935ff -r 8193bbaa07fe Nominal-General/nominal_library.ML --- a/Nominal-General/nominal_library.ML Sun Nov 14 12:09:14 2010 +0000 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,372 +0,0 @@ -(* Title: nominal_library.ML - Author: Christian Urban - - Basic functions for nominal. -*) - -signature NOMINAL_LIBRARY = -sig - val is_true: term -> bool - - val last2: 'a list -> 'a * 'a - - val dest_listT: typ -> typ - - val size_const: typ -> 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 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 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 - - (* fresh arguments for a term *) - val fresh_args: Proof.context -> term -> term list - - (* 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 - -end - - -structure Nominal_Library: NOMINAL_LIBRARY = -struct - -fun is_true @{term "Trueprop True"} = true - | is_true _ = false - -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 size_const ty = Const (@{const_name size}, ty --> @{typ nat}) - -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 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 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"} - - -(* 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 - - - -(** datatypes **) - -(* constructor infos *) -type cns_info = (term * typ * typ list * bool list) list - -(* 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 - Const (@{const_name prod_size}, [fT_fun, sT_fun, prodT] ---> natT) - end - - fun mk_size_measure T = - case T of - (Type (@{type_name Sum_Type.sum}, [fT, sT])) => - SumTree.mk_sumcase fT sT natT (mk_size_measure fT) (mk_size_measure sT) - | (Type (@{type_name Product_Type.prod}, [fT, sT])) => - prod_size_const fT sT $ (mk_size_measure fT) $ (mk_size_measure sT) - | _ => size_const T - - fun mk_measure_trm T = - HOLogic.dest_setT T - |> fst o HOLogic.dest_prodT - |> mk_size_measure - |> curry (op $) (Const (@{const_name "measure"}, dummyT)) - |> Syntax.check_term ctxt - - val ss = HOL_ss addsimps @{thms in_measure wf_measure sum.cases add_Suc_right add.right_neutral - zero_less_Suc prod.size(1) mult_Suc_right} @ size_simps - val ss' = ss addsimprocs Nat_Numeral_Simprocs.cancel_numerals - in - Function_Relation.relation_tac ctxt mk_measure_trm - THEN_ALL_NEW simp_tac ss' - end - -fun prove_termination size_simps ctxt = - Function.prove_termination NONE - (HEADGOAL (prove_termination_tac size_simps ctxt)) ctxt - -(** 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 (@{const_name "conj"}, _) $ f1 $ _) = - (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 (@{const_name "conj"}, _) $ 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; \ No newline at end of file