(* 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 binding functions *) type bn_info = (term * int * (int * term option) list 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 val define_raw_fvs: Datatype_Aux.descr -> (string * sort) list -> bn_info -> bclause list list list -> thm list -> Proof.context -> term list * term list * thm 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 =structtype bn_info = (term * int * (int * term option) list list) listdatatype bmode = Lst | Res | Setdatatype bclause = BC of bmode * (term option * int) list * int list(* 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 tendfun 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_to_set = @{term "fset_to_set :: atom fset => atom set"}in fset_to_set $ (Const (@{const_name fmap}, fmap_ty) $ Const (@{const_name atom}, atom_ty) $ t)endfun 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 tend(* 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 (_, 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 (bn_option, i) = let val arg = nth args i in case bn_option of NONE => (setify lthy arg, @{term "{}::atom set"}) | SOME bn => (to_set (bn $ arg), the (AList.lookup (op=) fv_bn_map bn) $ arg) end val t1 = map (mk_fv_body fv_map args) bodies val (t2, t3) = split_list (map (mk_fv_binder lthy fv_bn_map args) binders)in fold_union (mk_diff (fold_union t1, fold_union t2)::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 fv_map fv_bn_map bn_args args 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) => the (AList.lookup (op=) fv_bn_map bn) $ arg end in case bclause of BC (_, [], bodies) => fold_union (map (mk_fv_bn_body fv_map fv_bn_map bn_args args) bodies) | _ => mk_fv_rhs lthy fv_map fv_bn_map args bclauseendfun 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 = the (AList.lookup (op=) 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_trmsin 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 = the (AList.lookup (op=) 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_trmsin 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_nin map2 (mk_fv_bn_eq lthy bn_trm fv_map fv_bn_map) (bn_argss ~~ nth_constrs_info) nth_bclausessendfun define_raw_fvs descr sorts bn_info bclausesss constr_thms lthy =let val fv_names = prefix_dt_names descr sorts "fv_" val fv_arg_tys = all_dtyps descr sorts val fv_tys = map (fn ty => ty --> @{typ "atom set"}) fv_arg_tys; val fv_frees = map Free (fv_names ~~ fv_tys); val fv_map = fv_arg_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 (fn i => nth_dtyp descr sorts i) 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 constrs_info = all_dtyp_constrs_types descr sorts val fv_eqs = map2 (map2 (mk_fv_eq lthy fv_map fv_bn_map)) constrs_info bclausesss val fv_bn_eqs = map (mk_fv_bn_eqs lthy fv_map fv_bn_map constrs_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 (Local_Theory.restore lthy') val {fs, simps, inducts, ...} = info; val morphism = ProofContext.export_morphism lthy'' lthy val fs_exp = map (Morphism.term morphism) fs val (fv_frees_exp, fv_bns_exp) = chop (length fv_frees) fs_exp val simps_exp = map (Morphism.thm morphism) (the simps) val fv_bns_inducts_exp = map (Morphism.thm morphism) (the inducts)in (fv_frees_exp, fv_bns_exp, simps_exp, fv_bns_inducts_exp, lthy'')end(** equivarance proofs **)val eqvt_apply_sym = @{thm eqvt_apply[symmetric]}fun subproof_tac const_names simps = Subgoal.FOCUS (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 (eqvt_apply_sym :: prems))))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 *)