moved most material fron Nominal2_FSet into the Nominal_Base theory
(* Title: nominal_dt_rawfuns.ML Author: Cezary Kaliszyk Author: Christian Urban Definitions of the raw fv and fv_bn functions*)signature NOMINAL_DT_RAWFUNS =sig (* info of raw datatypes *) type dt_info = string list * binding * mixfix * ((binding * typ list * mixfix) list) list (* info of raw binding functions *) type bn_info = term * int * (int * term option) list list (* binding modes and binding clauses *) datatype bmode = Lst | Res | Set datatype bclause = BC of bmode * (term option * int) list * int list 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 mk_atom_set: term -> term val mk_atom_fset: term -> term val setify: Proof.context -> term -> term val listify: Proof.context -> term -> term (* FIXME: should be here - currently in Nominal2.thy val define_raw_bns: string list -> dt_info -> (binding * typ option * mixfix) list -> (Attrib.binding * term) list -> thm list -> thm list -> local_theory -> (term list * thm list * bn_info list * thm list * local_theory) *) val define_raw_fvs: string list -> typ list -> cns_info list -> bn_info list -> bclause list list list -> thm list -> thm list -> Proof.context -> term list * term list * thm list * thm list * local_theory val define_raw_bn_perms: typ list -> bn_info list -> cns_info list -> thm list -> thm list -> local_theory -> (term list * thm list * local_theory) val raw_prove_eqvt: term list -> thm list -> thm list -> Proof.context -> thm listendstructure Nominal_Dt_RawFuns: NOMINAL_DT_RAWFUNS =struct(* string list - type variables of a datatype binding - name of the datatype mixfix - its mixfix (binding * typ list * mixfix) list - datatype constructors of the type*) type dt_info = string list * binding * mixfix * ((binding * typ list * mixfix) list) list(* term - is constant of the bn-function int - is datatype number over which the bn-function is defined int * term option - is number of the corresponding argument with possibly recursive call with bn-function term *) type bn_info = term * int * (int * term option) list listdatatype bmode = Lst | Res | Setdatatype bclause = BC of bmode * (term option * int) list * int listfun lookup xs x = the (AList.lookup (op=) xs x)(* 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", [t, @{typ bool}])) = is_atom ctxt t | is_atom_set _ _ = false;fun is_atom_fset ctxt (Type (@{type_name "fset"}, [t])) = is_atom ctxt t | is_atom_fset _ _ = false;fun is_atom_list ctxt (Type (@{type_name "list"}, [t])) = is_atom ctxt t | is_atom_list _ _ = false(* functions for producing sets, fsets and lists of general atom type out from concrete atom types *)fun mk_atom_set t = let val ty = fastype_of t; val atom_ty = HOLogic.dest_setT ty --> @{typ "atom"}; val img_ty = atom_ty --> ty --> @{typ "atom set"}; in Const (@{const_name image}, img_ty) $ mk_atom_ty atom_ty t endfun dest_fsetT (Type (@{type_name fset}, [T])) = T | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []);fun mk_atom_fset t = let val ty = fastype_of t; val atom_ty = dest_fsetT ty --> @{typ "atom"}; val fmap_ty = atom_ty --> ty --> @{typ "atom fset"}; val fset = @{term "fset :: atom fset => atom set"} in fset $ (Const (@{const_name map_fset}, fmap_ty) $ Const (@{const_name atom}, atom_ty) $ t) end fun mk_atom_list t = let val ty = fastype_of t; val atom_ty = dest_listT ty --> @{typ atom}; val map_ty = atom_ty --> ty --> @{typ "atom list"}; in Const (@{const_name map}, map_ty) $ mk_atom_ty atom_ty t end(* functions that coerces singletons, sets and fsets of concrete atoms into sets of general atoms *)fun setify ctxt t = let val ty = fastype_of t; in if is_atom ctxt ty then HOLogic.mk_set @{typ atom} [mk_atom t] else if is_atom_set ctxt ty then mk_atom_set t else if is_atom_fset ctxt ty then mk_atom_fset t else raise TERM ("setify", [t]) end(* functions that coerces singletons and lists of concrete atoms into lists of general atoms *)fun listify ctxt t = let val ty = fastype_of t; in if is_atom ctxt ty then HOLogic.mk_list @{typ atom} [mk_atom t] else if is_atom_list ctxt ty then mk_atom_set t else raise TERM ("listify", [t]) end(* coerces a list into a set *)fun to_set t = if fastype_of t = @{typ "atom list"} then @{term "set::atom list => atom set"} $ t else t(** functions that construct the equations for fv and fv_bn **)fun mk_fv_rhs lthy fv_map fv_bn_map args (BC (bmode, binders, bodies)) = let fun mk_fv_body fv_map args i = let val arg = nth args i val ty = fastype_of arg in case AList.lookup (op=) fv_map ty of NONE => mk_supp arg | SOME fv => fv $ arg end fun mk_fv_binder lthy fv_bn_map args binders = let fun bind_set lthy args (NONE, i) = (setify lthy (nth args i), @{term "{}::atom set"}) | bind_set _ args (SOME bn, i) = (bn $ (nth args i), if member (op=) bodies i then @{term "{}::atom set"} else lookup fv_bn_map bn $ (nth args i)) fun bind_lst lthy args (NONE, i) = (listify lthy (nth args i), @{term "[]::atom list"}) | bind_lst _ args (SOME bn, i) = (bn $ (nth args i), if member (op=) bodies i then @{term "[]::atom list"} else lookup fv_bn_map bn $ (nth args i)) val (combine_fn, bind_fn) = case bmode of Lst => (fold_append, bind_lst) | Set => (fold_union, bind_set) | Res => (fold_union, bind_set) in binders |> map (bind_fn lthy args) |> split_list |> pairself combine_fn end val t1 = map (mk_fv_body fv_map args) bodies val (t2, t3) = mk_fv_binder lthy fv_bn_map args binders in mk_union (mk_diff (fold_union t1, to_set t2), to_set t3) end(* in case of fv_bn we have to treat the case special, where an "empty" binding clause is given *)fun mk_fv_bn_rhs lthy fv_map fv_bn_map bn_args args bclause = let fun mk_fv_bn_body i = let val arg = nth args i val ty = fastype_of arg in case AList.lookup (op=) bn_args i of NONE => (case (AList.lookup (op=) fv_map ty) of NONE => mk_supp arg | SOME fv => fv $ arg) | SOME (NONE) => @{term "{}::atom set"} | SOME (SOME bn) => lookup fv_bn_map bn $ arg end in case bclause of BC (_, [], bodies) => fold_union (map mk_fv_bn_body bodies) | _ => mk_fv_rhs lthy fv_map fv_bn_map args bclause endfun mk_fv_eq lthy fv_map fv_bn_map (constr, ty, arg_tys, _) bclauses = let val arg_names = Datatype_Prop.make_tnames arg_tys val args = map Free (arg_names ~~ arg_tys) val fv = lookup fv_map ty val lhs = fv $ list_comb (constr, args) val rhs_trms = map (mk_fv_rhs lthy fv_map fv_bn_map args) bclauses val rhs = fold_union rhs_trms in HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) endfun mk_fv_bn_eq lthy bn_trm fv_map fv_bn_map (bn_args, (constr, _, arg_tys, _)) bclauses = let val arg_names = Datatype_Prop.make_tnames arg_tys val args = map Free (arg_names ~~ arg_tys) val fv_bn = lookup fv_bn_map bn_trm val lhs = fv_bn $ list_comb (constr, args) val rhs_trms = map (mk_fv_bn_rhs lthy fv_map fv_bn_map bn_args args) bclauses val rhs = fold_union rhs_trms in HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) endfun mk_fv_bn_eqs lthy fv_map fv_bn_map constrs_info bclausesss (bn_trm, bn_n, bn_argss) = let val nth_constrs_info = nth constrs_info bn_n val nth_bclausess = nth bclausesss bn_n in map2 (mk_fv_bn_eq lthy bn_trm fv_map fv_bn_map) (bn_argss ~~ nth_constrs_info) nth_bclausess endfun define_raw_fvs raw_full_ty_names raw_tys cns_info bn_info bclausesss constr_thms size_simps lthy = let val fv_names = map (prefix "fv_" o Long_Name.base_name) raw_full_ty_names val fv_tys = map (fn ty => ty --> @{typ "atom set"}) raw_tys val fv_frees = map Free (fv_names ~~ fv_tys); val fv_map = raw_tys ~~ fv_frees val (bns, bn_tys) = split_list (map (fn (bn, i, _) => (bn, i)) bn_info) val bn_names = map (fn bn => Long_Name.base_name (fst (dest_Const bn))) bns val fv_bn_names = map (prefix "fv_") bn_names val fv_bn_arg_tys = map (nth raw_tys) bn_tys val fv_bn_tys = map (fn ty => ty --> @{typ "atom set"}) fv_bn_arg_tys val fv_bn_frees = map Free (fv_bn_names ~~ fv_bn_tys) val fv_bn_map = bns ~~ fv_bn_frees val fv_eqs = map2 (map2 (mk_fv_eq lthy fv_map fv_bn_map)) cns_info bclausesss val fv_bn_eqs = map (mk_fv_bn_eqs lthy fv_map fv_bn_map cns_info bclausesss) bn_info val all_fun_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names) val all_fun_eqs = map (pair Attrib.empty_binding) (flat fv_eqs @ flat fv_bn_eqs) val (_, lthy') = Function.add_function all_fun_names all_fun_eqs Function_Common.default_config (pat_completeness_simp constr_thms) lthy val (info, lthy'') = prove_termination size_simps (Local_Theory.restore lthy') val {fs, simps, inducts, ...} = info; val morphism = ProofContext.export_morphism lthy'' lthy val simps_exp = map (Morphism.thm morphism) (the simps) val inducts_exp = map (Morphism.thm morphism) (the inducts) val (fvs', fv_bns') = chop (length fv_frees) fs in (fvs', fv_bns', simps_exp, inducts_exp, lthy'') end(** definition of raw permute_bn functions **)fun mk_perm_bn_eq_rhs p perm_bn_map bn_args (i, arg) = case AList.lookup (op=) bn_args i of NONE => arg | SOME (NONE) => mk_perm p arg | SOME (SOME bn) => (lookup perm_bn_map bn) $ p $ arg fun mk_perm_bn_eq lthy bn_trm perm_bn_map bn_args (constr, _, arg_tys, _) = let val p = Free ("p", @{typ perm}) val arg_names = Datatype_Prop.make_tnames arg_tys val args = map Free (arg_names ~~ arg_tys) val perm_bn = lookup perm_bn_map bn_trm val lhs = perm_bn $ p $ list_comb (constr, args) val rhs = list_comb (constr, map_index (mk_perm_bn_eq_rhs p perm_bn_map bn_args) args) in HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) endfun mk_perm_bn_eqs lthy perm_bn_map cns_info (bn_trm, bn_n, bn_argss) = let val nth_cns_info = nth cns_info bn_n in map2 (mk_perm_bn_eq lthy bn_trm perm_bn_map) bn_argss nth_cns_info endfun define_raw_bn_perms raw_tys bn_info cns_info cns_thms size_thms lthy = if null bn_info then ([], [], lthy) else let val (bns, bn_tys) = split_list (map (fn (bn, i, _) => (bn, i)) bn_info) val bn_names = map (fn bn => Long_Name.base_name (fst (dest_Const bn))) bns val perm_bn_names = map (prefix "permute_") bn_names val perm_bn_arg_tys = map (nth raw_tys) bn_tys val perm_bn_tys = map (fn ty => @{typ "perm"} --> ty --> ty) perm_bn_arg_tys val perm_bn_frees = map Free (perm_bn_names ~~ perm_bn_tys) val perm_bn_map = bns ~~ perm_bn_frees val perm_bn_eqs = map (mk_perm_bn_eqs lthy perm_bn_map cns_info) bn_info val all_fun_names = map (fn s => (Binding.name s, NONE, NoSyn)) perm_bn_names val all_fun_eqs = map (pair Attrib.empty_binding) (flat perm_bn_eqs) val prod_simps = @{thms prod.inject HOL.simp_thms} val (_, lthy') = Function.add_function all_fun_names all_fun_eqs Function_Common.default_config (pat_completeness_simp (prod_simps @ cns_thms)) lthy val (info, lthy'') = prove_termination size_thms (Local_Theory.restore lthy') val {fs, simps, ...} = info; val morphism = ProofContext.export_morphism lthy'' lthy val simps_exp = map (Morphism.thm morphism) (the simps) in (fs, simps_exp, lthy'') end(** equivarance proofs **)val eqvt_apply_sym = @{thm eqvt_apply[symmetric]}fun subproof_tac const_names simps = SUBPROOF (fn {prems, context, ...} => HEADGOAL (simp_tac (HOL_basic_ss addsimps simps) THEN' Nominal_Permeq.eqvt_tac context [] const_names THEN' simp_tac (HOL_basic_ss addsimps (prems @ [eqvt_apply_sym]))))fun prove_eqvt_tac insts ind_thms const_names simps ctxt = HEADGOAL (Object_Logic.full_atomize_tac THEN' (DETERM o (InductTacs.induct_rules_tac ctxt insts ind_thms)) THEN_ALL_NEW subproof_tac const_names simps ctxt)fun mk_eqvt_goal pi const arg = let val lhs = mk_perm pi (const $ arg) val rhs = const $ (mk_perm pi arg) in HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) endfun raw_prove_eqvt consts ind_thms simps ctxt = if null consts then [] else let val ([p], ctxt') = Variable.variant_fixes ["p"] ctxt val p = Free (p, @{typ perm}) val arg_tys = consts |> map fastype_of |> map domain_type val (arg_names, ctxt'') = Variable.variant_fixes (Datatype_Prop.make_tnames arg_tys) ctxt' val args = map Free (arg_names ~~ arg_tys) val goals = map2 (mk_eqvt_goal p) consts args val insts = map (single o SOME) arg_names val const_names = map (fst o dest_Const) consts in Goal.prove_multi ctxt'' [] [] goals (fn {context, ...} => prove_eqvt_tac insts ind_thms const_names simps context) |> ProofContext.export ctxt'' ctxt endend (* structure *)