fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
theory Nominal2+ −
imports + −
Nominal2_Base Nominal2_Abs+ −
uses ("nominal_dt_rawfuns.ML")+ −
("nominal_dt_alpha.ML")+ −
("nominal_dt_quot.ML")+ −
("nominal_induct.ML")+ −
("nominal_inductive.ML")+ −
("nominal_function_core.ML")+ −
("nominal_mutual.ML")+ −
("nominal_function.ML")+ −
begin+ −
+ −
use "nominal_dt_rawfuns.ML"+ −
ML {* open Nominal_Dt_RawFuns *}+ −
+ −
use "nominal_dt_alpha.ML"+ −
ML {* open Nominal_Dt_Alpha *}+ −
+ −
use "nominal_dt_quot.ML"+ −
ML {* open Nominal_Dt_Quot *}+ −
+ −
(*****************************************)+ −
(* setup for induction principles method *)+ −
use "nominal_induct.ML"+ −
method_setup nominal_induct =+ −
{* NominalInduct.nominal_induct_method *}+ −
{* nominal induction *}+ −
+ −
(****************************************************)+ −
(* inductive definition involving nominal datatypes *)+ −
use "nominal_inductive.ML" + −
+ −
+ −
(***************************************)+ −
(* forked code of the function package *)+ −
(* for defining nominal functions *)+ −
use "nominal_function_core.ML"+ −
use "nominal_mutual.ML"+ −
use "nominal_function.ML"+ −
+ −
ML {*+ −
val eqvt_attr = Attrib.internal (K Nominal_ThmDecls.eqvt_add)+ −
val rsp_attr = Attrib.internal (K Quotient_Info.rsp_rules_add)+ −
val simp_attr = Attrib.internal (K Simplifier.simp_add)+ −
val induct_attr = Attrib.internal (K Induct.induct_simp_add)+ −
*}+ −
+ −
section{* Interface for nominal_datatype *}+ −
+ −
ML {* print_depth 50 *}+ −
+ −
ML {*+ −
fun get_cnstrs dts =+ −
map (fn (_, _, _, constrs) => constrs) dts+ −
+ −
fun get_typed_cnstrs dts =+ −
flat (map (fn (_, bn, _, constrs) => + −
(map (fn (bn', _, _) => (Binding.name_of bn, Binding.name_of bn')) constrs)) dts)+ −
+ −
fun get_cnstr_strs dts =+ −
map (fn (bn, _, _) => Binding.name_of bn) (flat (get_cnstrs dts))+ −
+ −
fun get_bn_fun_strs bn_funs =+ −
map (fn (bn_fun, _, _) => Binding.name_of bn_fun) bn_funs+ −
*}+ −
+ −
+ −
text {* Infrastructure for adding "_raw" to types and terms *}+ −
+ −
ML {*+ −
fun add_raw s = s ^ "_raw"+ −
fun add_raws ss = map add_raw ss+ −
fun raw_bind bn = Binding.suffix_name "_raw" bn+ −
+ −
fun replace_str ss s = + −
case (AList.lookup (op=) ss s) of + −
SOME s' => s'+ −
| NONE => s+ −
+ −
fun replace_typ ty_ss (Type (a, Ts)) = Type (replace_str ty_ss a, map (replace_typ ty_ss) Ts)+ −
| replace_typ ty_ss T = T + −
+ −
fun raw_dts ty_ss dts =+ −
let+ −
fun raw_dts_aux1 (bind, tys, _) =+ −
(raw_bind bind, map (replace_typ ty_ss) tys, NoSyn)+ −
+ −
fun raw_dts_aux2 (ty_args, bind, _, constrs) =+ −
(ty_args, raw_bind bind, NoSyn, map raw_dts_aux1 constrs)+ −
in+ −
map raw_dts_aux2 dts+ −
end+ −
+ −
fun replace_aterm trm_ss (Const (a, T)) = Const (replace_str trm_ss a, T)+ −
| replace_aterm trm_ss (Free (a, T)) = Free (replace_str trm_ss a, T)+ −
| replace_aterm trm_ss trm = trm+ −
+ −
fun replace_term trm_ss ty_ss trm =+ −
trm |> Term.map_aterms (replace_aterm trm_ss) |> map_types (replace_typ ty_ss) + −
*}+ −
+ −
ML {*+ −
fun rawify_dts dt_names dts dts_env =+ −
let+ −
val raw_dts = raw_dts dts_env dts+ −
val raw_dt_names = add_raws dt_names+ −
in+ −
(raw_dt_names, raw_dts)+ −
end + −
*}+ −
+ −
ML {*+ −
fun rawify_bn_funs dts_env cnstrs_env bn_fun_env bn_funs bn_eqs =+ −
let+ −
val bn_funs' = map (fn (bn, ty, _) => + −
(raw_bind bn, SOME (replace_typ dts_env ty), NoSyn)) bn_funs+ −
+ −
val bn_eqs' = map (fn (attr, trm) => + −
(attr, replace_term (cnstrs_env @ bn_fun_env) dts_env trm)) bn_eqs+ −
in+ −
(bn_funs', bn_eqs') + −
end + −
*}+ −
+ −
ML {* + −
fun rawify_bclauses dts_env cnstrs_env bn_fun_env bclauses =+ −
let+ −
fun rawify_bnds bnds = + −
map (apfst (Option.map (replace_term (cnstrs_env @ bn_fun_env) dts_env))) bnds+ −
+ −
fun rawify_bclause (BC (mode, bnds, bdys)) = BC (mode, rawify_bnds bnds, bdys)+ −
in+ −
(map o map o map) rawify_bclause bclauses+ −
end+ −
*}+ −
+ −
+ −
ML {*+ −
fun define_raw_dts dts bn_funs bn_eqs bclauses lthy =+ −
let+ −
val thy = Local_Theory.exit_global lthy+ −
val thy_name = Context.theory_name thy+ −
+ −
val dt_names = map (fn (_, s, _, _) => Binding.name_of s) dts+ −
val dt_full_names = map (Long_Name.qualify thy_name) dt_names + −
val dt_full_names' = add_raws dt_full_names+ −
val dts_env = dt_full_names ~~ dt_full_names'+ −
+ −
val cnstr_names = get_cnstr_strs dts+ −
val cnstr_tys = get_typed_cnstrs dts+ −
val cnstr_full_names = map (Long_Name.qualify thy_name) cnstr_names+ −
val cnstr_full_names' = map (fn (x, y) => Long_Name.qualify thy_name + −
(Long_Name.qualify (add_raw x) (add_raw y))) cnstr_tys+ −
val cnstrs_env = cnstr_full_names ~~ cnstr_full_names'+ −
+ −
val bn_fun_strs = get_bn_fun_strs bn_funs+ −
val bn_fun_strs' = add_raws bn_fun_strs+ −
val bn_fun_env = bn_fun_strs ~~ bn_fun_strs'+ −
val bn_fun_full_env = map (pairself (Long_Name.qualify thy_name)) + −
(bn_fun_strs ~~ bn_fun_strs')+ −
+ −
val (raw_dt_names, raw_dts) = rawify_dts dt_names dts dts_env+ −
val (raw_bn_funs, raw_bn_eqs) = rawify_bn_funs dts_env cnstrs_env bn_fun_env bn_funs bn_eqs + −
val raw_bclauses = rawify_bclauses dts_env cnstrs_env bn_fun_full_env bclauses + −
+ −
val (raw_dt_full_names, thy1) = + −
Datatype.add_datatype Datatype.default_config raw_dt_names raw_dts thy+ −
+ −
val lthy1 = Named_Target.theory_init thy1+ −
in+ −
(raw_dt_full_names, raw_dts, raw_bclauses, raw_bn_funs, raw_bn_eqs, cnstr_names, lthy1)+ −
end+ −
*}+ −
+ −
+ −
ML {*+ −
fun nominal_datatype2 opt_thms_name dts bn_funs bn_eqs bclauses lthy =+ −
let+ −
val _ = trace_msg (K "Defining raw datatypes...")+ −
val (raw_dt_names, raw_dts, raw_bclauses, raw_bn_funs, raw_bn_eqs, cnstr_names, lthy0) =+ −
define_raw_dts dts bn_funs bn_eqs bclauses lthy + −
+ −
val dtinfo = Datatype.the_info (ProofContext.theory_of lthy0) (hd raw_dt_names)+ −
val {descr, sorts, ...} = dtinfo+ −
+ −
val raw_tys = all_dtyps descr sorts+ −
val raw_full_ty_names = map (fst o dest_Type) raw_tys+ −
val tvs = hd raw_tys+ −
|> snd o dest_Type+ −
|> map dest_TFree + −
+ −
val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy0)) raw_full_ty_names + −
+ −
val raw_cns_info = all_dtyp_constrs_types descr sorts+ −
val raw_constrs = (map o map) (fn (c, _, _, _) => c) raw_cns_info+ −
+ −
val raw_inject_thms = flat (map #inject dtinfos)+ −
val raw_distinct_thms = flat (map #distinct dtinfos)+ −
val raw_induct_thm = #induct dtinfo+ −
val raw_induct_thms = #inducts dtinfo+ −
val raw_exhaust_thms = map #exhaust dtinfos+ −
val raw_size_trms = map HOLogic.size_const raw_tys+ −
val raw_size_thms = Size.size_thms (ProofContext.theory_of lthy0) (hd raw_dt_names)+ −
|> `(fn thms => (length thms) div 2)+ −
|> uncurry drop+ −
+ −
val _ = trace_msg (K "Defining raw permutations...")+ −
val ((raw_perm_funs, raw_perm_simps, raw_perm_laws), lthy2a) =+ −
define_raw_perms raw_full_ty_names raw_tys tvs (flat raw_constrs) raw_induct_thm lthy0+ −
+ −
(* noting the raw permutations as eqvt theorems *)+ −
val (_, lthy3) = Local_Theory.note ((Binding.empty, [eqvt_attr]), raw_perm_simps) lthy2a+ −
+ −
val _ = trace_msg (K "Defining raw fv- and bn-functions...")+ −
val (raw_bns, raw_bn_defs, raw_bn_info, raw_bn_induct, lthy3a) =+ −
define_raw_bns raw_full_ty_names raw_dts raw_bn_funs raw_bn_eqs + −
(raw_inject_thms @ raw_distinct_thms) raw_size_thms lthy3+ −
+ −
(* defining the permute_bn functions *)+ −
val (raw_perm_bns, raw_perm_bn_simps, lthy3b) = + −
define_raw_bn_perms raw_tys raw_bn_info raw_cns_info + −
(raw_inject_thms @ raw_distinct_thms) raw_size_thms lthy3a+ −
+ −
val (raw_fvs, raw_fv_bns, raw_fv_defs, raw_fv_bns_induct, lthy3c) = + −
define_raw_fvs raw_full_ty_names raw_tys raw_cns_info raw_bn_info raw_bclauses + −
(raw_inject_thms @ raw_distinct_thms) raw_size_thms lthy3b+ −
+ −
val _ = trace_msg (K "Defining alpha relations...")+ −
val (alpha_trms, alpha_bn_trms, alpha_intros, alpha_cases, alpha_induct, lthy4) =+ −
define_raw_alpha raw_full_ty_names raw_tys raw_cns_info raw_bn_info raw_bclauses raw_fvs lthy3c+ −
+ −
val alpha_tys = map (domain_type o fastype_of) alpha_trms + −
+ −
val _ = trace_msg (K "Proving distinct theorems...")+ −
val alpha_distincts = + −
mk_alpha_distincts lthy4 alpha_cases raw_distinct_thms alpha_trms raw_tys+ −
+ −
val _ = trace_msg (K "Proving eq-iff theorems...")+ −
val alpha_eq_iff = + −
mk_alpha_eq_iff lthy4 alpha_intros raw_distinct_thms raw_inject_thms alpha_cases+ −
+ −
val _ = trace_msg (K "Proving equivariance of bns, fvs, size and alpha...")+ −
val raw_bn_eqvt = + −
raw_prove_eqvt raw_bns raw_bn_induct (raw_bn_defs @ raw_perm_simps) lthy4+ −
+ −
(* noting the raw_bn_eqvt lemmas in a temprorary theory *)+ −
val lthy_tmp = snd (Local_Theory.note ((Binding.empty, [eqvt_attr]), raw_bn_eqvt) lthy4)+ −
+ −
val raw_fv_eqvt = + −
raw_prove_eqvt (raw_fvs @ raw_fv_bns) raw_fv_bns_induct (raw_fv_defs @ raw_perm_simps) + −
(Local_Theory.restore lthy_tmp)+ −
+ −
val raw_size_eqvt = + −
raw_prove_eqvt raw_size_trms raw_induct_thms (raw_size_thms @ raw_perm_simps) + −
(Local_Theory.restore lthy_tmp)+ −
|> map (rewrite_rule @{thms permute_nat_def[THEN eq_reflection]})+ −
|> map (fn thm => thm RS @{thm sym})+ −
+ −
val lthy5 = snd (Local_Theory.note ((Binding.empty, [eqvt_attr]), raw_fv_eqvt) lthy_tmp)+ −
+ −
val (alpha_eqvt, lthy6) =+ −
Nominal_Eqvt.raw_equivariance true (alpha_trms @ alpha_bn_trms) alpha_induct alpha_intros lthy5+ −
+ −
val _ = trace_msg (K "Proving equivalence of alpha...")+ −
val alpha_refl_thms = + −
raw_prove_refl alpha_trms alpha_bn_trms alpha_intros raw_induct_thm lthy6 + −
+ −
val alpha_sym_thms = + −
raw_prove_sym (alpha_trms @ alpha_bn_trms) alpha_intros alpha_induct lthy6 + −
+ −
val alpha_trans_thms = + −
raw_prove_trans (alpha_trms @ alpha_bn_trms) (raw_distinct_thms @ raw_inject_thms) + −
alpha_intros alpha_induct alpha_cases lthy6+ −
+ −
val (alpha_equivp_thms, alpha_bn_equivp_thms) = + −
raw_prove_equivp alpha_trms alpha_bn_trms alpha_refl_thms alpha_sym_thms + −
alpha_trans_thms lthy6+ −
+ −
val _ = trace_msg (K "Proving alpha implies bn...")+ −
val alpha_bn_imp_thms = + −
raw_prove_bn_imp alpha_trms alpha_bn_trms alpha_intros alpha_induct lthy6 + −
+ −
val _ = trace_msg (K "Proving respectfulness...")+ −
val raw_funs_rsp_aux = + −
raw_fv_bn_rsp_aux alpha_trms alpha_bn_trms raw_fvs + −
raw_bns raw_fv_bns alpha_induct (raw_bn_defs @ raw_fv_defs) lthy6+ −
+ −
val raw_funs_rsp = map mk_funs_rsp raw_funs_rsp_aux+ −
+ −
val raw_size_rsp = + −
raw_size_rsp_aux (alpha_trms @ alpha_bn_trms) alpha_induct + −
(raw_size_thms @ raw_size_eqvt) lthy6+ −
|> map mk_funs_rsp+ −
+ −
val raw_constrs_rsp = + −
raw_constrs_rsp (flat raw_constrs) alpha_trms alpha_intros+ −
(alpha_bn_imp_thms @ raw_funs_rsp_aux) lthy6 + −
+ −
val alpha_permute_rsp = map mk_alpha_permute_rsp alpha_eqvt+ −
+ −
val alpha_bn_rsp = + −
raw_alpha_bn_rsp alpha_bn_trms alpha_bn_equivp_thms alpha_bn_imp_thms+ −
+ −
val raw_perm_bn_rsp =+ −
raw_perm_bn_rsp (alpha_trms @ alpha_bn_trms) raw_perm_bns alpha_induct + −
alpha_intros raw_perm_bn_simps lthy6+ −
+ −
(* noting the quot_respects lemmas *)+ −
val (_, lthy6a) = + −
Local_Theory.note ((Binding.empty, [rsp_attr]),+ −
raw_constrs_rsp @ raw_funs_rsp @ raw_size_rsp @ alpha_permute_rsp @ + −
alpha_bn_rsp @ raw_perm_bn_rsp) lthy6+ −
+ −
val _ = trace_msg (K "Defining the quotient types...")+ −
val qty_descr = map (fn (vs, bind, mx, _) => (vs, bind, mx)) dts+ −
+ −
val (qty_infos, lthy7) = + −
define_qtypes qty_descr alpha_tys alpha_trms alpha_equivp_thms lthy6a+ −
+ −
val qtys = map #qtyp qty_infos+ −
val qty_full_names = map (fst o dest_Type) qtys+ −
val qty_names = map Long_Name.base_name qty_full_names + −
+ −
val _ = trace_msg (K "Defining the quotient constants...")+ −
val qconstrs_descrs =+ −
(map2 o map2) (fn (b, _, mx) => fn t => (Variable.check_name b, t, mx)) (get_cnstrs dts) raw_constrs+ −
+ −
val qbns_descr =+ −
map2 (fn (b, _, mx) => fn t => (Variable.check_name b, t, mx)) bn_funs raw_bns+ −
+ −
val qfvs_descr = + −
map2 (fn n => fn t => ("fv_" ^ n, t, NoSyn)) qty_names raw_fvs+ −
+ −
val qfv_bns_descr = + −
map2 (fn (b, _, _) => fn t => ("fv_" ^ Variable.check_name b, t, NoSyn)) bn_funs raw_fv_bns+ −
+ −
val qalpha_bns_descr = + −
map2 (fn (b, _, _) => fn t => ("alpha_" ^ Variable.check_name b, t, NoSyn)) bn_funs alpha_bn_trms+ −
+ −
val qperm_descr =+ −
map2 (fn n => fn t => ("permute_" ^ n, Type.legacy_freeze t, NoSyn)) qty_names raw_perm_funs+ −
+ −
val qsize_descr =+ −
map2 (fn n => fn t => ("size_" ^ n, t, NoSyn)) qty_names raw_size_trms+ −
+ −
val qperm_bn_descr = + −
map2 (fn (b, _, _) => fn t => ("permute_" ^ Variable.check_name b, t, NoSyn)) bn_funs raw_perm_bns+ −
+ −
val ((((((qconstrs_infos, qbns_info), qfvs_info), qfv_bns_info), qalpha_bns_info), qperm_bns_info), + −
lthy8) = + −
lthy7+ −
|> fold_map (define_qconsts qtys) qconstrs_descrs + −
||>> define_qconsts qtys qbns_descr + −
||>> define_qconsts qtys qfvs_descr+ −
||>> define_qconsts qtys qfv_bns_descr+ −
||>> define_qconsts qtys qalpha_bns_descr+ −
||>> define_qconsts qtys qperm_bn_descr+ −
+ −
val lthy9 = + −
define_qperms qtys qty_full_names tvs qperm_descr raw_perm_laws lthy8 + −
+ −
val lthy9a = + −
define_qsizes qtys qty_full_names tvs qsize_descr lthy9+ −
+ −
val qtrms = (map o map) #qconst qconstrs_infos+ −
val qbns = map #qconst qbns_info+ −
val qfvs = map #qconst qfvs_info+ −
val qfv_bns = map #qconst qfv_bns_info+ −
val qalpha_bns = map #qconst qalpha_bns_info+ −
val qperm_bns = map #qconst qperm_bns_info+ −
+ −
val _ = trace_msg (K "Lifting of theorems...") + −
val eq_iff_simps = @{thms alphas permute_prod.simps prod_fv.simps prod_alpha_def prod_rel_def+ −
prod.cases} + −
+ −
val ((((((qdistincts, qeq_iffs), qfv_defs), qbn_defs), qperm_simps), qfv_qbn_eqvts), lthyA) = + −
lthy9a + −
|> lift_thms qtys [] alpha_distincts + −
||>> lift_thms qtys eq_iff_simps alpha_eq_iff + −
||>> lift_thms qtys [] raw_fv_defs+ −
||>> lift_thms qtys [] raw_bn_defs+ −
||>> lift_thms qtys [] raw_perm_simps+ −
||>> lift_thms qtys [] (raw_fv_eqvt @ raw_bn_eqvt)+ −
+ −
val ((((((qsize_eqvt, [qinduct]), qexhausts), qsize_simps), qperm_bn_simps), qalpha_refl_thms), lthyB) = + −
lthyA + −
|> lift_thms qtys [] raw_size_eqvt+ −
||>> lift_thms qtys [] [raw_induct_thm]+ −
||>> lift_thms qtys [] raw_exhaust_thms+ −
||>> lift_thms qtys [] raw_size_thms+ −
||>> lift_thms qtys [] raw_perm_bn_simps+ −
||>> lift_thms qtys [] alpha_refl_thms+ −
+ −
val qinducts = Project_Rule.projections lthyA qinduct+ −
+ −
val _ = trace_msg (K "Proving supp lemmas and fs-instances...")+ −
val qsupports_thms =+ −
prove_supports lthyB qperm_simps (flat qtrms)+ −
+ −
(* finite supp lemmas *)+ −
val qfsupp_thms = prove_fsupp lthyB qtys qinduct qsupports_thms+ −
+ −
(* fs instances *)+ −
val lthyC = fs_instance qtys qty_full_names tvs qfsupp_thms lthyB+ −
+ −
val _ = trace_msg (K "Proving equality between fv and supp...")+ −
val qfv_supp_thms = + −
prove_fv_supp qtys (flat qtrms) qfvs qfv_bns qalpha_bns qfv_defs qeq_iffs + −
qperm_simps qfv_qbn_eqvts qinduct (flat raw_bclauses) lthyC+ −
+ −
(* postprocessing of eq and fv theorems *)+ −
val qeq_iffs' = qeq_iffs+ −
|> map (simplify (HOL_basic_ss addsimps qfv_supp_thms))+ −
|> map (simplify (HOL_basic_ss addsimps @{thms prod_fv_supp prod_alpha_eq Abs_eq_iff[symmetric]}))+ −
+ −
val qsupp_constrs = qfv_defs+ −
|> map (simplify (HOL_basic_ss addsimps (take (length qfvs) qfv_supp_thms)))+ −
+ −
val transform_thm = @{lemma "x = y \<Longrightarrow> a \<notin> x \<longleftrightarrow> a \<notin> y" by simp}+ −
val transform_thms = + −
[ @{lemma "a \<notin> (S \<union> T) \<longleftrightarrow> a \<notin> S \<and> a \<notin> T" by simp}, + −
@{lemma "a \<notin> (S - T) \<longleftrightarrow> a \<notin> S \<or> a \<in> T" by simp}, + −
@{lemma "(lhs = (a \<notin> {})) \<longleftrightarrow> lhs" by simp}, + −
@{thm fresh_def[symmetric]}]+ −
+ −
val qfresh_constrs = qsupp_constrs+ −
|> map (fn thm => thm RS transform_thm) + −
|> map (simplify (HOL_basic_ss addsimps transform_thms))+ −
+ −
(* proving that the qbn result is finite *)+ −
val qbn_finite_thms = prove_bns_finite qtys qbns qinduct qbn_defs lthyC+ −
+ −
(* proving that perm_bns preserve alpha *)+ −
val qperm_bn_alpha_thms = + −
prove_perm_bn_alpha_thms qtys qperm_bns qalpha_bns qinduct qperm_bn_simps qeq_iffs' + −
qalpha_refl_thms lthyC+ −
+ −
(* proving the relationship of bn and permute_bn *)+ −
val qpermute_bn_thms = + −
prove_permute_bn_thms qtys qbns qperm_bns qinduct qperm_bn_simps qbn_defs qfv_qbn_eqvts lthyC+ −
+ −
val _ = trace_msg (K "Proving strong exhaust lemmas...")+ −
val qstrong_exhaust_thms = prove_strong_exhausts lthyC qexhausts bclauses qbn_finite_thms qeq_iffs'+ −
qfv_qbn_eqvts qpermute_bn_thms qperm_bn_alpha_thms+ −
+ −
val _ = trace_msg (K "Proving strong induct lemmas...")+ −
val qstrong_induct_thms = prove_strong_induct lthyC qinduct qstrong_exhaust_thms qsize_simps bclauses+ −
+ −
(* noting the theorems *) + −
+ −
(* generating the prefix for the theorem names *)+ −
val thms_name = + −
the_default (Binding.name (space_implode "_" qty_names)) opt_thms_name + −
fun thms_suffix s = Binding.qualified true s thms_name + −
val case_names_attr = Attrib.internal (K (Rule_Cases.case_names cnstr_names))+ −
+ −
val (_, lthy9') = lthyC+ −
|> Local_Theory.note ((thms_suffix "distinct", [induct_attr, simp_attr]), qdistincts) + −
||>> Local_Theory.note ((thms_suffix "eq_iff", [induct_attr, simp_attr]), qeq_iffs')+ −
||>> Local_Theory.note ((thms_suffix "fv_defs", []), qfv_defs) + −
||>> Local_Theory.note ((thms_suffix "bn_defs", []), qbn_defs) + −
||>> Local_Theory.note ((thms_suffix "perm_simps", [eqvt_attr, simp_attr]), qperm_simps) + −
||>> Local_Theory.note ((thms_suffix "fv_bn_eqvt", []), qfv_qbn_eqvts) + −
||>> Local_Theory.note ((thms_suffix "size", []), qsize_simps)+ −
||>> Local_Theory.note ((thms_suffix "size_eqvt", []), qsize_eqvt)+ −
||>> Local_Theory.note ((thms_suffix "induct", [case_names_attr]), [qinduct]) + −
||>> Local_Theory.note ((thms_suffix "inducts", [case_names_attr]), qinducts)+ −
||>> Local_Theory.note ((thms_suffix "exhaust", [case_names_attr]), qexhausts)+ −
||>> Local_Theory.note ((thms_suffix "strong_exhaust", [case_names_attr]), qstrong_exhaust_thms)+ −
||>> Local_Theory.note ((thms_suffix "strong_induct", [case_names_attr]), qstrong_induct_thms)+ −
||>> Local_Theory.note ((thms_suffix "supports", []), qsupports_thms)+ −
||>> Local_Theory.note ((thms_suffix "fsupp", []), qfsupp_thms)+ −
||>> Local_Theory.note ((thms_suffix "supp", []), qsupp_constrs)+ −
||>> Local_Theory.note ((thms_suffix "fresh", []), qfresh_constrs)+ −
||>> Local_Theory.note ((thms_suffix "raw_alpha", []), alpha_intros)+ −
||>> Local_Theory.note ((thms_suffix "perm_bn_simps", []), qperm_bn_simps)+ −
||>> Local_Theory.note ((thms_suffix "bn_finite", []), qbn_finite_thms)+ −
||>> Local_Theory.note ((thms_suffix "perm_bn_alpha", []), qperm_bn_alpha_thms)+ −
||>> Local_Theory.note ((thms_suffix "permute_bn", []), qpermute_bn_thms)+ −
in+ −
lthy9'+ −
end + −
*}+ −
+ −
+ −
section {* Preparing and parsing of the specification *}+ −
+ −
ML {* + −
(* generates the parsed datatypes and + −
declares the constructors + −
*)+ −
fun prepare_dts dt_strs thy = + −
let+ −
fun inter_fs_sort thy (a, S) = + −
(a, Type.inter_sort (Sign.tsig_of thy) (@{sort fs}, S)) + −
+ −
fun mk_type tname sorts (cname, cargs, mx) =+ −
let+ −
val full_tname = Sign.full_name thy tname+ −
val ty = Type (full_tname, map (TFree o inter_fs_sort thy) sorts)+ −
in+ −
(cname, cargs ---> ty, mx)+ −
end+ −
+ −
fun prep_constr (cname, cargs, mx, _) (constrs, sorts) =+ −
let + −
val (cargs', sorts') = + −
fold_map (Datatype.read_typ thy) (map snd cargs) sorts+ −
|>> map (map_type_tfree (TFree o inter_fs_sort thy)) + −
in + −
(constrs @ [(cname, cargs', mx)], sorts') + −
end+ −
+ −
fun prep_dts (tvs, tname, mx, constrs) (constr_trms, dts, sorts) =+ −
let + −
val (constrs', sorts') = + −
fold prep_constr constrs ([], sorts)+ −
+ −
val constr_trms' = + −
map (mk_type tname (rev sorts')) constrs'+ −
in + −
(constr_trms @ constr_trms', dts @ [(tvs, tname, mx, constrs')], sorts') + −
end+ −
+ −
val (constr_trms, dts, sorts) = fold prep_dts dt_strs ([], [], []);+ −
in+ −
thy+ −
|> Sign.add_consts_i constr_trms+ −
|> pair dts+ −
end+ −
*}+ −
+ −
ML {*+ −
(* parsing the binding function specification and *)+ −
(* declaring the functions in the local theory *)+ −
fun prepare_bn_funs bn_fun_strs bn_eq_strs thy =+ −
let+ −
val lthy = Named_Target.theory_init thy+ −
+ −
val ((bn_funs, bn_eqs), lthy') = + −
Specification.read_spec bn_fun_strs bn_eq_strs lthy+ −
+ −
fun prep_bn_fun ((bn, T), mx) = (bn, T, mx) + −
+ −
val bn_funs' = map prep_bn_fun bn_funs+ −
in+ −
(Local_Theory.exit_global lthy')+ −
|> Sign.add_consts_i bn_funs'+ −
|> pair (bn_funs', bn_eqs) + −
end + −
*}+ −
+ −
text {* associates every SOME with the index in the list; drops NONEs *}+ −
ML {*+ −
fun indexify xs =+ −
let+ −
fun mapp _ [] = []+ −
| mapp i (NONE :: xs) = mapp (i + 1) xs+ −
| mapp i (SOME x :: xs) = (x, i) :: mapp (i + 1) xs+ −
in + −
mapp 0 xs + −
end+ −
+ −
fun index_lookup xs x =+ −
case AList.lookup (op=) xs x of+ −
SOME x => x+ −
| NONE => error ("Cannot find " ^ x ^ " as argument annotation.");+ −
*}+ −
+ −
ML {*+ −
fun prepare_bclauses dt_strs thy = + −
let+ −
val annos_bclauses =+ −
get_cnstrs dt_strs+ −
|> (map o map) (fn (_, antys, _, bns) => (map fst antys, bns))+ −
+ −
fun prep_binder env bn_str =+ −
case (Syntax.read_term_global thy bn_str) of+ −
Free (x, _) => (NONE, index_lookup env x)+ −
| Const (a, T) $ Free (x, _) => (SOME (Const (a, T)), index_lookup env x)+ −
| _ => error ("The term " ^ bn_str ^ " is not allowed as binding function.")+ −
+ −
fun prep_body env bn_str = index_lookup env bn_str+ −
+ −
fun prep_bclause env (mode, binders, bodies) = + −
let+ −
val binders' = map (prep_binder env) binders+ −
val bodies' = map (prep_body env) bodies+ −
in + −
BC (mode, binders', bodies')+ −
end+ −
+ −
fun prep_bclauses (annos, bclause_strs) = + −
let+ −
val env = indexify annos (* for every label, associate the index *)+ −
in+ −
map (prep_bclause env) bclause_strs+ −
end+ −
in+ −
((map o map) prep_bclauses annos_bclauses, thy)+ −
end+ −
*}+ −
+ −
text {* + −
adds an empty binding clause for every argument+ −
that is not already part of a binding clause+ −
*}+ −
+ −
ML {*+ −
fun included i bcs = + −
let+ −
fun incl (BC (_, bns, bds)) = + −
member (op =) (map snd bns) i orelse member (op =) bds i+ −
in+ −
exists incl bcs + −
end+ −
*}+ −
+ −
ML {* + −
fun complete dt_strs bclauses = + −
let+ −
val args = + −
get_cnstrs dt_strs+ −
|> (map o map) (fn (_, antys, _, _) => length antys)+ −
+ −
fun complt n bcs = + −
let+ −
fun add bcs i = (if included i bcs then [] else [BC (Lst, [], [i])]) + −
in+ −
bcs @ (flat (map_range (add bcs) n))+ −
end+ −
in+ −
(map2 o map2) complt args bclauses+ −
end+ −
*}+ −
+ −
ML {*+ −
fun nominal_datatype2_cmd (opt_thms_name, dt_strs, bn_fun_strs, bn_eq_strs) lthy = + −
let+ −
val pre_typs = + −
map (fn (tvs, tname, mx, _) => (tname, length tvs, mx)) dt_strs+ −
+ −
(* this theory is used just for parsing *)+ −
val thy = ProofContext.theory_of lthy + −
val tmp_thy = Theory.copy thy + −
+ −
val (((dts, (bn_funs, bn_eqs)), bclauses), tmp_thy') = + −
tmp_thy+ −
|> Sign.add_types_global pre_typs+ −
|> prepare_dts dt_strs + −
||>> prepare_bn_funs bn_fun_strs bn_eq_strs + −
||>> prepare_bclauses dt_strs + −
+ −
val bclauses' = complete dt_strs bclauses+ −
in+ −
nominal_datatype2 opt_thms_name dts bn_funs bn_eqs bclauses' lthy+ −
end+ −
*}+ −
+ −
ML {* + −
(* nominal datatype parser *)+ −
local+ −
structure P = Parse;+ −
structure S = Scan+ −
+ −
fun triple ((x, y), z) = (x, y, z)+ −
fun tuple1 ((x, y, z), u) = (x, y, z, u)+ −
fun tuple2 (((x, y), z), u) = (x, y, u, z)+ −
fun tuple3 ((x, y), (z, u)) = (x, y, z, u)+ −
in+ −
+ −
val _ = Keyword.keyword "bind"+ −
+ −
val opt_name = Scan.option (P.binding --| Args.colon)+ −
+ −
val anno_typ = S.option (P.name --| P.$$$ "::") -- P.typ+ −
+ −
val bind_mode = P.$$$ "bind" |--+ −
S.optional (Args.parens + −
(Args.$$$ "list" >> K Lst || (Args.$$$ "set" -- Args.$$$ "+") >> K Res || Args.$$$ "set" >> K Set)) Lst+ −
+ −
val bind_clauses = + −
P.enum "," (bind_mode -- S.repeat1 P.term -- (P.$$$ "in" |-- S.repeat1 P.name) >> triple)+ −
+ −
val cnstr_parser =+ −
P.binding -- S.repeat anno_typ -- bind_clauses -- P.opt_mixfix >> tuple2+ −
+ −
(* datatype parser *)+ −
val dt_parser =+ −
(P.type_args -- P.binding -- P.opt_mixfix >> triple) -- + −
(P.$$$ "=" |-- P.enum1 "|" cnstr_parser) >> tuple1+ −
+ −
(* binding function parser *)+ −
val bnfun_parser = + −
S.optional (P.$$$ "binder" |-- P.fixes -- Parse_Spec.where_alt_specs) ([], [])+ −
+ −
(* main parser *)+ −
val main_parser =+ −
opt_name -- P.and_list1 dt_parser -- bnfun_parser >> tuple3+ −
+ −
end+ −
+ −
(* Command Keyword *)+ −
val _ = Outer_Syntax.local_theory "nominal_datatype" "test" Keyword.thy_decl+ −
(main_parser >> nominal_datatype2_cmd)+ −
*}+ −
+ −
(*+ −
ML {*+ −
trace := true+ −
*}+ −
*)+ −
+ −
end+ −
+ −
+ −
+ −