--- a/Nominal/Nominal2.thy Mon Jul 11 12:23:24 2011 +0100
+++ b/Nominal/Nominal2.thy Mon Jul 11 12:23:44 2011 +0100
@@ -145,7 +145,7 @@
ML {*
(* definition of the raw datatype *)
-fun define_raw_dts dts bn_funs bn_eqs bclauses lthy =
+fun define_raw_dts dts cnstr_names cnstr_tys bn_funs bn_eqs bclauses lthy =
let
val thy = Local_Theory.exit_global lthy
val thy_name = Context.theory_name thy
@@ -155,8 +155,6 @@
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
@@ -168,37 +166,25 @@
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_full_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 (raw_full_dt_names', thy1) =
+ Datatype.add_datatype Datatype.default_config raw_full_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 dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy0)) raw_dt_names
+ val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy1)) raw_full_dt_names'
val {descr, sorts, ...} = hd dtinfos
val raw_tys = Datatype_Aux.get_rec_types descr sorts
- val tvs = hd raw_tys
+ val raw_ty_args = hd raw_tys
|> snd o dest_Type
- |> map dest_TFree
+ |> map dest_TFree
val raw_cns_info = all_dtyp_constrs_types descr sorts
- val raw_constrs = (map o map) (fn (c, _, _, _) => c) raw_cns_info
+ val raw_all_cns = (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)
@@ -206,41 +192,100 @@
val raw_induct_thms = #inducts (hd dtinfos)
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)
+ val raw_size_thms = Size.size_thms (ProofContext.theory_of lthy1) (hd raw_full_dt_names')
|> `(fn thms => (length thms) div 2)
|> uncurry drop
+
+ val raw_result = RawDtInfo
+ {raw_dt_names = raw_full_dt_names',
+ raw_dts = raw_dts,
+ raw_tys = raw_tys,
+ raw_ty_args = raw_ty_args,
+ raw_cns_info = raw_cns_info,
+ raw_all_cns = raw_all_cns,
+ raw_inject_thms = raw_inject_thms,
+ raw_distinct_thms = raw_distinct_thms,
+ raw_induct_thm = raw_induct_thm,
+ raw_induct_thms = raw_induct_thms,
+ raw_exhaust_thms = raw_exhaust_thms,
+ raw_size_trms = raw_size_trms,
+ raw_size_thms = raw_size_thms}
+in
+ (raw_bclauses, raw_bn_funs, raw_bn_eqs, raw_result, lthy1)
+end
+*}
+
+ML {*
+infix 1 ||>>> |>>>
+
+fun (x |>>> f) =
+ let
+ val (x', y') = f x
+ in
+ ([x'], y')
+ end
+
+fun (([], y) ||>>> f) = ([], y)
+ | ((xs, y) ||>>> f) =
+ let
+ val (x', y') = f y
+ in
+ (xs @ [x'], y')
+ end;
+(op ||>>)
+*}
+
+
+
+ML {*
+fun nominal_datatype2 opt_thms_name dts bn_funs bn_eqs bclauses lthy =
+let
+ val cnstr_names = get_cnstr_strs dts
+ val cnstr_tys = get_typed_cnstrs dts
+
+ val _ = trace_msg (K "Defining raw datatypes...")
+ val (raw_bclauses, raw_bn_funs, raw_bn_eqs, raw_dt_info, lthy0) =
+ define_raw_dts dts cnstr_names cnstr_tys bn_funs bn_eqs bclauses lthy
+
+ val RawDtInfo
+ {raw_dt_names,
+ raw_tys,
+ raw_ty_args,
+ raw_all_cns,
+ raw_inject_thms,
+ raw_distinct_thms,
+ raw_induct_thm,
+ raw_induct_thms,
+ raw_exhaust_thms,
+ raw_size_trms,
+ raw_size_thms, ...} = raw_dt_info
val _ = trace_msg (K "Defining raw permutations...")
- val ((raw_perm_funs, raw_perm_simps, raw_perm_laws), lthy2a) =
- define_raw_perms raw_dt_names raw_tys tvs (flat raw_constrs) raw_induct_thm lthy0
+ val ((raw_perm_funs, raw_perm_simps, raw_perm_laws), lthy2a) = define_raw_perms raw_dt_info lthy0
(* noting the raw permutations as eqvt theorems *)
- val (_, lthy3) = Local_Theory.note ((Binding.empty, [eqvt_attr]), raw_perm_simps) lthy2a
+ val lthy3 = snd (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_inducts, lthy3a) =
- define_raw_bns raw_dt_names raw_dts raw_bn_funs raw_bn_eqs
- (raw_inject_thms @ raw_distinct_thms) raw_size_thms lthy3
+ define_raw_bns raw_dt_info raw_bn_funs raw_bn_eqs 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
+ define_raw_bn_perms raw_dt_info raw_bn_info lthy3a
val (raw_fvs, raw_fv_bns, raw_fv_defs, raw_fv_bns_induct, lthy3c) =
- define_raw_fvs raw_dt_names raw_tys raw_cns_info raw_bn_info raw_bclauses
- (raw_inject_thms @ raw_distinct_thms) raw_size_thms lthy3b
+ define_raw_fvs raw_dt_info raw_bn_info raw_bclauses lthy3b
val _ = trace_msg (K "Defining alpha relations...")
val (alpha_result, lthy4) =
- define_raw_alpha raw_dt_names raw_tys raw_cns_info raw_bn_info raw_bclauses raw_fvs lthy3c
+ define_raw_alpha raw_dt_info raw_bn_info raw_bclauses raw_fvs lthy3c
val _ = trace_msg (K "Proving distinct theorems...")
- val alpha_distincts =
- raw_prove_alpha_distincts lthy4 alpha_result raw_distinct_thms raw_dt_names
+ val alpha_distincts = raw_prove_alpha_distincts lthy4 alpha_result raw_dt_info
val _ = trace_msg (K "Proving eq-iff theorems...")
- val alpha_eq_iff = raw_prove_alpha_eq_iff lthy4 alpha_result raw_distinct_thms raw_inject_thms
+ val alpha_eq_iff = raw_prove_alpha_eq_iff lthy4 alpha_result raw_dt_info
val _ = trace_msg (K "Proving equivariance of bns, fvs, size and alpha...")
val raw_bn_eqvt =
@@ -253,11 +298,15 @@
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 raw_size_eqvt =
+ let
+ val RawDtInfo {raw_size_trms, raw_size_thms, raw_induct_thms, ...} = raw_dt_info
+ in
+ 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})
+ end
val lthy5 = snd (Local_Theory.note ((Binding.empty, [eqvt_attr]), raw_fv_eqvt) lthy_tmp)
@@ -293,7 +342,7 @@
|> map mk_funs_rsp
val raw_constrs_rsp =
- raw_constrs_rsp lthy5 alpha_result (flat raw_constrs) (alpha_bn_imp_thms @ raw_funs_rsp_aux)
+ raw_constrs_rsp lthy5 alpha_result (flat raw_all_cns) (alpha_bn_imp_thms @ raw_funs_rsp_aux)
val alpha_permute_rsp = map mk_alpha_permute_rsp alpha_eqvt
@@ -324,7 +373,7 @@
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
+ (map2 o map2) (fn (b, _, mx) => fn t => (Variable.check_name b, t, mx)) (get_cnstrs dts) raw_all_cns
val qbns_descr =
map2 (fn (b, _, mx) => fn t => (Variable.check_name b, t, mx)) bn_funs raw_bns
@@ -362,10 +411,10 @@
||>> define_qconsts qtys qperm_bn_descr
val lthy9 =
- define_qperms qtys qty_full_names tvs qperm_descr raw_perm_laws lthy8
+ define_qperms qtys qty_full_names raw_ty_args qperm_descr raw_perm_laws lthy8
val lthy9a =
- define_qsizes qtys qty_full_names tvs qsize_descr lthy9
+ define_qsizes qtys qty_full_names raw_ty_args qsize_descr lthy9
val qtrms = (map o map) #qconst qconstrs_infos
val qbns = map #qconst qbns_info
@@ -378,37 +427,34 @@
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), qbn_inducts),
- lthyA) =
+ val ([ qdistincts, qeq_iffs, qfv_defs, qbn_defs, qperm_simps, qfv_qbn_eqvts,
+ qbn_inducts, qsize_eqvt, [qinduct], qexhausts, qsize_simps, qperm_bn_simps,
+ qalpha_refl_thms ], lthyB) =
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)
- ||>> lift_thms qtys [] raw_bn_inducts
-
- 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
+ |>>> 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)
+ ||>>> lift_thms qtys [] raw_bn_inducts
+ ||>>> 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 lthyB qinduct
val _ = trace_msg (K "Proving supp lemmas and fs-instances...")
- val qsupports_thms =
- prove_supports lthyB qperm_simps (flat qtrms)
+ 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 lthyC = fs_instance qtys qty_full_names raw_ty_args qfsupp_thms lthyB
val _ = trace_msg (K "Proving equality between fv and supp...")
val qfv_supp_thms =
@@ -523,6 +569,7 @@
fun prep_dts (tvs, tname, mx, constrs) (constr_trms, dts, sorts) =
let
+
val (constrs', sorts') =
fold prep_constr constrs ([], sorts)
--- a/Nominal/nominal_basics.ML Mon Jul 11 12:23:24 2011 +0100
+++ b/Nominal/nominal_basics.ML Mon Jul 11 12:23:44 2011 +0100
@@ -10,6 +10,7 @@
val trace_msg: (unit -> string) -> unit
val last2: 'a list -> 'a * 'a
+ val split_triples: ('a * 'b * 'c) list -> ('a list * 'b list * 'c list)
val split_last2: 'a list -> 'a list * 'a * 'a
val order: ('a * 'a -> bool) -> 'a list -> ('a * 'b) list -> 'b list
val order_default: ('a * 'a -> bool) -> 'b -> 'a list -> ('a * 'b) list -> 'b list
@@ -68,6 +69,9 @@
then remove_dups eq xs
else x :: remove_dups eq xs
+fun split_triples xs =
+ fold (fn (a, b, c) => fn (axs, bxs, cxs) => (a :: axs, b :: bxs, c :: cxs)) xs ([], [], [])
+
fun last2 [] = raise Empty
| last2 [_] = raise Empty
| last2 [x, y] = (x, y)
--- a/Nominal/nominal_dt_alpha.ML Mon Jul 11 12:23:24 2011 +0100
+++ b/Nominal/nominal_dt_alpha.ML Mon Jul 11 12:23:44 2011 +0100
@@ -9,8 +9,8 @@
sig
val comb_binders: Proof.context -> bmode -> term list -> (term option * int) list -> term
- val define_raw_alpha: string list -> typ list -> cns_info list -> bn_info list ->
- bclause list list list -> term list -> Proof.context -> alpha_result * local_theory
+ val define_raw_alpha: raw_dt_info -> bn_info list -> bclause list list list -> term list ->
+ Proof.context -> alpha_result * local_theory
val induct_prove: typ list -> (typ * (term -> term)) list -> thm ->
(Proof.context -> int -> tactic) -> Proof.context -> thm list
@@ -18,8 +18,8 @@
val alpha_prove: term list -> (term * ((term * term) -> term)) list -> thm ->
(Proof.context -> int -> tactic) -> Proof.context -> thm list
- val raw_prove_alpha_distincts: Proof.context -> alpha_result -> thm list -> string list -> thm list
- val raw_prove_alpha_eq_iff: Proof.context -> alpha_result -> thm list -> thm list -> thm list
+ val raw_prove_alpha_distincts: Proof.context -> alpha_result -> raw_dt_info -> thm list
+ val raw_prove_alpha_eq_iff: Proof.context -> alpha_result -> raw_dt_info -> thm list
val raw_prove_refl: Proof.context -> alpha_result -> thm -> thm list
val raw_prove_sym: Proof.context -> alpha_result -> thm list -> thm list
val raw_prove_trans: Proof.context -> alpha_result -> thm list -> thm list -> thm list
@@ -224,9 +224,11 @@
map2 (mk_alpha_bn_intro lthy bn_trm alpha_map alpha_bn_map) (bn_argss ~~ nth_constrs_info) nth_bclausess
end
-fun define_raw_alpha raw_full_ty_names raw_tys cns_info bn_info bclausesss fvs lthy =
+fun define_raw_alpha raw_dt_info bn_info bclausesss fvs lthy =
let
- val alpha_names = map (prefix "alpha_" o Long_Name.base_name) raw_full_ty_names
+ val RawDtInfo {raw_dt_names, raw_tys, raw_cns_info, ...} = raw_dt_info
+
+ val alpha_names = map (prefix "alpha_" o Long_Name.base_name) raw_dt_names
val alpha_tys = map (fn ty => [ty, ty] ---> @{typ bool}) raw_tys
val alpha_frees = map Free (alpha_names ~~ alpha_tys)
val alpha_map = raw_tys ~~ (alpha_frees ~~ fvs)
@@ -239,8 +241,8 @@
val alpha_bn_frees = map Free (alpha_bn_names ~~ alpha_bn_tys)
val alpha_bn_map = bns ~~ alpha_bn_frees
- val alpha_intros = map2 (map2 (mk_alpha_intros lthy alpha_map alpha_bn_map)) cns_info bclausesss
- val alpha_bn_intros = map (mk_alpha_bn_intros lthy alpha_map alpha_bn_map cns_info bclausesss) bn_info
+ val alpha_intros = map2 (map2 (mk_alpha_intros lthy alpha_map alpha_bn_map)) raw_cns_info bclausesss
+ val alpha_bn_intros = map (mk_alpha_bn_intros lthy alpha_map alpha_bn_map raw_cns_info bclausesss) bn_info
val all_alpha_names = map (fn (a, ty) => ((Binding.name a, ty), NoSyn))
(alpha_names @ alpha_bn_names ~~ alpha_tys @ alpha_bn_tys)
@@ -393,9 +395,10 @@
rtac notI THEN' eresolve_tac cases_thms
THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps distinct_thms)
-fun raw_prove_alpha_distincts ctxt alpha_result raw_distinct_thms raw_dt_names =
+fun raw_prove_alpha_distincts ctxt alpha_result raw_dt_info =
let
val AlphaResult {alpha_names, alpha_cases, ...} = alpha_result
+ val RawDtInfo {raw_dt_names, raw_distinct_thms, ...} = raw_dt_info
val ty_trm_assoc = raw_dt_names ~~ alpha_names
@@ -439,9 +442,10 @@
else HOLogic.mk_Trueprop (HOLogic.mk_eq (concl, list_conj hyps))
end;
-fun raw_prove_alpha_eq_iff ctxt alpha_result raw_distinct_thms raw_inject_thms =
+fun raw_prove_alpha_eq_iff ctxt alpha_result raw_dt_info =
let
val AlphaResult {alpha_intros, alpha_cases, ...} = alpha_result
+ val RawDtInfo {raw_distinct_thms, raw_inject_thms, ...} = raw_dt_info
val ((_, thms_imp), ctxt') = Variable.import false alpha_intros ctxt;
val goals = map mk_alpha_eq_iff_goal thms_imp;
--- a/Nominal/nominal_dt_data.ML Mon Jul 11 12:23:24 2011 +0100
+++ b/Nominal/nominal_dt_data.ML Mon Jul 11 12:23:44 2011 +0100
@@ -5,11 +5,21 @@
signature NOMINAL_DT_DATA =
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
+
type info =
- {inject : thm list,
- distinct : thm list,
- strong_inducts : thm list,
- strong_exhaust : thm list}
+ {inject : thm list,
+ distinct : thm list,
+ strong_inducts : thm list,
+ strong_exhaust : thm list}
val get_all_info: Proof.context -> (string * info) list
val get_info: Proof.context -> string -> info option
@@ -17,6 +27,29 @@
val register_info: (string * info) -> Context.generic -> Context.generic
val mk_infos: string list -> thm list -> thm list -> thm list -> thm list -> (string * info) list
+ datatype user_data = UserData of
+ {dts : dt_info,
+ cn_names : string list,
+ cn_tys : (string * string) list,
+ bn_funs : (binding * typ * mixfix) list,
+ bn_eqs : (Attrib.binding * term) list,
+ bclauses : bclause list list list}
+
+ datatype raw_dt_info = RawDtInfo of
+ {raw_dt_names : string list,
+ raw_dts : dt_info,
+ raw_tys : typ list,
+ raw_ty_args : (string * sort) list,
+ raw_cns_info : cns_info list,
+ raw_all_cns : term list list,
+ raw_inject_thms : thm list,
+ raw_distinct_thms : thm list,
+ raw_induct_thm : thm,
+ raw_induct_thms : thm list,
+ raw_exhaust_thms : thm list,
+ raw_size_trms : term list,
+ raw_size_thms : thm list}
+
datatype alpha_result = AlphaResult of
{alpha_names : string list,
alpha_trms : term list,
@@ -33,6 +66,24 @@
structure Nominal_Dt_Data: NOMINAL_DT_DATA =
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 list
+
+datatype bmode = Lst | Res | Set
+datatype bclause = BC of bmode * (term option * int) list * int list
+
(* information generated by nominal_datatype *)
type info =
@@ -68,6 +119,30 @@
map aux ty_names
end
+
+datatype user_data = UserData of
+ {dts : dt_info,
+ cn_names : string list,
+ cn_tys : (string * string) list,
+ bn_funs : (binding * typ * mixfix) list,
+ bn_eqs : (Attrib.binding * term) list,
+ bclauses : bclause list list list}
+
+datatype raw_dt_info = RawDtInfo of
+ {raw_dt_names : string list,
+ raw_dts : dt_info,
+ raw_tys : typ list,
+ raw_ty_args : (string * sort) list,
+ raw_cns_info : cns_info list,
+ raw_all_cns : term list list,
+ raw_inject_thms : thm list,
+ raw_distinct_thms : thm list,
+ raw_induct_thm : thm,
+ raw_induct_thms : thm list,
+ raw_exhaust_thms : thm list,
+ raw_size_trms : term list,
+ raw_size_thms : thm list}
+
datatype alpha_result = AlphaResult of
{alpha_names : string list,
alpha_trms : term list,
@@ -79,5 +154,4 @@
alpha_cases : thm list,
alpha_raw_induct : thm}
-
end
\ No newline at end of file
--- a/Nominal/nominal_dt_rawfuns.ML Mon Jul 11 12:23:24 2011 +0100
+++ b/Nominal/nominal_dt_rawfuns.ML Mon Jul 11 12:23:44 2011 +0100
@@ -7,59 +7,30 @@
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 get_all_binders: bclause list -> (term option * int) list
val is_recursive_binder: bclause -> bool
- val define_raw_bns: string list -> dt_info -> (binding * typ option * mixfix) list ->
- (Attrib.binding * term) list -> thm list -> thm list -> local_theory ->
+ val define_raw_bns: raw_dt_info -> (binding * typ option * mixfix) list ->
+ (Attrib.binding * term) 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_fvs: raw_dt_info -> bn_info list -> bclause list list 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 define_raw_bn_perms: raw_dt_info -> bn_info list -> local_theory ->
+ (term list * thm list * local_theory)
+
+ val define_raw_perms: raw_dt_info -> local_theory -> (term list * thm list * thm list) * local_theory
val raw_prove_eqvt: term list -> thm list -> thm list -> Proof.context -> thm list
- val define_raw_perms: string list -> typ list -> (string * sort) list -> term list -> thm ->
- local_theory -> (term list * thm list * thm list) * local_theory
end
structure Nominal_Dt_RawFuns: NOMINAL_DT_RAWFUNS =
struct
-open Nominal_Permeq
-
-(* 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 list
-
-
-datatype bmode = Lst | Res | Set
-datatype bclause = BC of bmode * (term option * int) list * int list
+open Nominal_Permeq
fun get_all_binders bclauses =
bclauses
@@ -136,22 +107,25 @@
|> order (op=) bn_funs (* ordered according to bn_functions *)
end
-fun define_raw_bns dt_names dts raw_bn_funs raw_bn_eqs constr_thms size_thms lthy =
+fun define_raw_bns raw_dt_info raw_bn_funs raw_bn_eqs lthy =
if null raw_bn_funs
then ([], [], [], [], lthy)
else
let
+ val RawDtInfo
+ {raw_dt_names, raw_dts, raw_inject_thms, raw_distinct_thms, raw_size_thms, ...} = raw_dt_info
+
val (_, lthy1) = Function.add_function raw_bn_funs raw_bn_eqs
- Function_Common.default_config (pat_completeness_simp constr_thms) lthy
+ Function_Common.default_config (pat_completeness_simp (raw_inject_thms @ raw_distinct_thms)) lthy
- val (info, lthy2) = prove_termination_fun size_thms (Local_Theory.restore lthy1)
+ val (info, lthy2) = prove_termination_fun raw_size_thms (Local_Theory.restore lthy1)
val {fs, simps, inducts, ...} = info
val raw_bn_induct = (the inducts)
val raw_bn_eqs = the simps
val raw_bn_info =
- prep_bn_info lthy dt_names dts fs (map prop_of raw_bn_eqs)
+ prep_bn_info lthy raw_dt_names raw_dts fs (map prop_of raw_bn_eqs)
in
(fs, raw_bn_eqs, raw_bn_info, raw_bn_induct, lthy2)
end
@@ -255,9 +229,13 @@
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 size_simps lthy =
+fun define_raw_fvs raw_dt_info bn_info bclausesss lthy =
let
- val fv_names = map (prefix "fv_" o Long_Name.base_name) raw_full_ty_names
+ val RawDtInfo
+ {raw_dt_names, raw_tys, raw_cns_info, raw_inject_thms, raw_distinct_thms, raw_size_thms, ...} =
+ raw_dt_info
+
+ val fv_names = map (prefix "fv_" o Long_Name.base_name) raw_dt_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
@@ -270,16 +248,16 @@
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 fv_eqs = map2 (map2 (mk_fv_eq lthy fv_map fv_bn_map)) raw_cns_info bclausesss
+ val fv_bn_eqs = map (mk_fv_bn_eqs lthy fv_map fv_bn_map raw_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
+ Function_Common.default_config (pat_completeness_simp (raw_inject_thms @ raw_distinct_thms)) lthy
- val (info, lthy'') = prove_termination_fun size_simps (Local_Theory.restore lthy')
+ val (info, lthy'') = prove_termination_fun raw_size_thms (Local_Theory.restore lthy')
val {fs, simps, inducts, ...} = info;
@@ -325,11 +303,14 @@
map2 (mk_perm_bn_eq lthy bn_trm perm_bn_map) bn_argss nth_cns_info
end
-fun define_raw_bn_perms raw_tys bn_info cns_info cns_thms size_thms lthy =
+fun define_raw_bn_perms raw_dt_info bn_info lthy =
if null bn_info
then ([], [], lthy)
else
let
+ val RawDtInfo
+ {raw_tys, raw_cns_info, raw_inject_thms, raw_distinct_thms, raw_size_thms, ...} = raw_dt_info
+
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
@@ -338,7 +319,7 @@
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 perm_bn_eqs = map (mk_perm_bn_eqs lthy perm_bn_map raw_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)
@@ -346,9 +327,10 @@
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
+ Function_Common.default_config
+ (pat_completeness_simp (prod_simps @ raw_inject_thms @ raw_distinct_thms)) lthy
- val (info, lthy'') = prove_termination_fun size_thms (Local_Theory.restore lthy')
+ val (info, lthy'') = prove_termination_fun raw_size_thms (Local_Theory.restore lthy')
val {fs, simps, ...} = info;
@@ -358,57 +340,6 @@
(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' eqvt_tac context (eqvt_relaxed_config addexcls 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
-
-
-
(*** raw permutation functions ***)
(** proves the two pt-type class properties **)
@@ -483,17 +414,20 @@
end
-fun define_raw_perms full_ty_names tys tvs constrs induct_thm lthy =
+fun define_raw_perms raw_dt_info lthy =
let
- val perm_fn_names = full_ty_names
+ val RawDtInfo
+ {raw_dt_names, raw_tys, raw_ty_args, raw_all_cns, raw_induct_thm, ...} = raw_dt_info
+
+ val perm_fn_names = raw_dt_names
|> map Long_Name.base_name
|> map (prefix "permute_")
- val perm_fn_types = map perm_ty tys
+ val perm_fn_types = map perm_ty raw_tys
val perm_fn_frees = map Free (perm_fn_names ~~ perm_fn_types)
val perm_fn_binds = map (fn s => (Binding.name s, NONE, NoSyn)) perm_fn_names
- val perm_eqs = map (mk_perm_eq (tys ~~ perm_fn_frees)) constrs
+ val perm_eqs = map (mk_perm_eq (raw_tys ~~ perm_fn_frees)) (flat raw_all_cns)
fun tac _ (_, _, simps) =
Class.intro_classes_tac [] THEN ALLGOALS (resolve_tac simps)
@@ -506,11 +440,11 @@
val ((perm_funs, perm_eq_thms), lthy') =
lthy
|> Local_Theory.exit_global
- |> Class.instantiation (full_ty_names, tvs, @{sort pt})
+ |> Class.instantiation (raw_dt_names, raw_ty_args, @{sort pt})
|> Primrec.add_primrec perm_fn_binds perm_eqs
- val perm_zero_thms = prove_permute_zero induct_thm perm_eq_thms perm_funs lthy'
- val perm_plus_thms = prove_permute_plus induct_thm perm_eq_thms perm_funs lthy'
+ val perm_zero_thms = prove_permute_zero raw_induct_thm perm_eq_thms perm_funs lthy'
+ val perm_plus_thms = prove_permute_plus raw_induct_thm perm_eq_thms perm_funs lthy'
in
lthy'
|> Class.prove_instantiation_exit_result morphism tac
@@ -519,5 +453,54 @@
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' eqvt_tac context (eqvt_relaxed_config addexcls 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 *)