(* 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: string list -> typ list -> cns_info 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 list+ −
end+ −
+ −
+ −
structure Nominal_Dt_RawFuns: NOMINAL_DT_RAWFUNS =+ −
struct+ −
+ −
(* 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 list) list+ −
+ −
datatype bmode = Lst | Res | Set+ −
datatype 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 t+ −
end+ −
+ −
+ −
fun 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)+ −
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 (_, 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 bclause+ −
end+ −
+ −
fun 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_trms+ −
in+ −
HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))+ −
end+ −
+ −
fun 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_trms+ −
in+ −
HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))+ −
end+ −
+ −
fun 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+ −
end+ −
+ −
fun define_raw_fvs raw_full_ty_names raw_tys cns_info bn_info bclausesss constr_thms 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 (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 = + −
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))+ −
end+ −
+ −
fun 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+ −
end+ −
+ −
end (* structure *)+ −
+ −