# HG changeset patch # User Christian Urban # Date 1291813504 0 # Node ID 89c55d36980f8deba4b836379c8ec7472a880894 # Parent ca6b4bc7a871dbaa3692a0a4a3bc66a3ad6b984b moved definition of raw bn-functions into nominal_dt_rawfuns diff -r ca6b4bc7a871 -r 89c55d36980f Nominal/Nominal2.thy --- a/Nominal/Nominal2.thy Wed Dec 08 12:37:25 2010 +0000 +++ b/Nominal/Nominal2.thy Wed Dec 08 13:05:04 2010 +0000 @@ -113,91 +113,6 @@ end *} -(* strip_bn_fun takes a rhs of a bn function: this can only contain unions or - appends of elements; in case of recursive calls it retruns also the applied - bn function *) -ML {* -fun strip_bn_fun lthy args t = -let - fun aux t = - case t of - Const (@{const_name sup}, _) $ l $ r => aux l @ aux r - | Const (@{const_name append}, _) $ l $ r => aux l @ aux r - | Const (@{const_name insert}, _) $ (Const (@{const_name atom}, _) $ (x as Var _)) $ y => - (find_index (equal x) args, NONE) :: aux y - | Const (@{const_name Cons}, _) $ (Const (@{const_name atom}, _) $ (x as Var _)) $ y => - (find_index (equal x) args, NONE) :: aux y - | Const (@{const_name bot}, _) => [] - | Const (@{const_name Nil}, _) => [] - | (f as Const _) $ (x as Var _) => [(find_index (equal x) args, SOME f)] - | _ => error ("Unsupported binding function: " ^ (Syntax.string_of_term lthy t)) -in - aux t -end -*} - -ML {* -(** definition of the raw binding functions **) - -fun prep_bn_info lthy dt_names dts bn_funs eqs = -let - fun process_eq eq = - let - val (lhs, rhs) = eq - |> HOLogic.dest_Trueprop - |> HOLogic.dest_eq - val (bn_fun, [cnstr]) = strip_comb lhs - val (_, ty) = dest_Const bn_fun - val (ty_name, _) = dest_Type (domain_type ty) - val dt_index = find_index (fn x => x = ty_name) dt_names - val (cnstr_head, cnstr_args) = strip_comb cnstr - val cnstr_name = Long_Name.base_name (fst (dest_Const cnstr_head)) - val rhs_elements = strip_bn_fun lthy cnstr_args rhs - in - ((bn_fun, dt_index), (cnstr_name, rhs_elements)) - end - - (* order according to constructor names *) - fun cntrs_order ((bn, dt_index), data) = - let - val dt = nth dts dt_index - val cts = (fn (_, _, _, x) => x) dt - val ct_names = map (Binding.name_of o (fn (x, _, _) => x)) cts - in - (bn, (bn, dt_index, order (op=) ct_names data)) - end - -in - eqs - |> map process_eq - |> AList.group (op=) (* eqs grouped according to bn_functions *) - |> map cntrs_order (* inner data ordered according to constructors *) - |> order (op=) bn_funs (* ordered according to bn_functions *) -end -*} - -ML {* -fun define_raw_bns dt_names dts raw_bn_funs raw_bn_eqs constr_thms size_thms lthy = - if null raw_bn_funs - then ([], [], [], [], lthy) - else - let - val (_, lthy1) = Function.add_function raw_bn_funs raw_bn_eqs - Function_Common.default_config (pat_completeness_simp constr_thms) lthy - - val (info, lthy2) = prove_termination 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) - in - (fs, raw_bn_eqs, raw_bn_info, raw_bn_induct, lthy2) - end - -*} ML {* fun define_raw_dts dts bn_funs bn_eqs bclauses lthy = @@ -646,8 +561,8 @@ ||>> Local_Theory.note ((thms_suffix "perm_bn_alpha", []), qperm_bn_alpha_thms) ||>> Local_Theory.note ((thms_suffix "permute_bn", []), qpermute_bn_thms) in - (0, lthy9') -end handle TEST ctxt => (0, ctxt) + lthy9' +end handle TEST ctxt => ctxt *} @@ -821,7 +736,7 @@ val bclauses' = complete dt_strs bclauses in - timeit (fn () => nominal_datatype2 opt_thms_name dts bn_funs bn_eqs bclauses' lthy |> snd) + timeit (fn () => nominal_datatype2 opt_thms_name dts bn_funs bn_eqs bclauses' lthy) end *} diff -r ca6b4bc7a871 -r 89c55d36980f Nominal/nominal_dt_rawfuns.ML --- a/Nominal/nominal_dt_rawfuns.ML Wed Dec 08 12:37:25 2010 +0000 +++ b/Nominal/nominal_dt_rawfuns.ML Wed Dec 08 13:05:04 2010 +0000 @@ -8,7 +8,7 @@ signature NOMINAL_DT_RAWFUNS = sig (* info of raw datatypes *) - type dt_info = string list * binding * mixfix * ((binding * typ list * mixfix) list) list + 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 @@ -28,11 +28,10 @@ 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 @@ -55,7 +54,7 @@ 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 +type dt_info = (string list * binding * mixfix * ((binding * typ list * mixfix) list)) list (* term - is constant of the bn-function @@ -149,6 +148,88 @@ end +(** functions that define the raw binding functions **) + +(* strip_bn_fun takes a rhs of a bn function: this can only contain unions or + appends of elements; in case of recursive calls it returns also the applied + bn function *) +fun strip_bn_fun lthy args t = +let + fun aux t = + case t of + Const (@{const_name sup}, _) $ l $ r => aux l @ aux r + | Const (@{const_name append}, _) $ l $ r => aux l @ aux r + | Const (@{const_name insert}, _) $ (Const (@{const_name atom}, _) $ (x as Var _)) $ y => + (find_index (equal x) args, NONE) :: aux y + | Const (@{const_name Cons}, _) $ (Const (@{const_name atom}, _) $ (x as Var _)) $ y => + (find_index (equal x) args, NONE) :: aux y + | Const (@{const_name bot}, _) => [] + | Const (@{const_name Nil}, _) => [] + | (f as Const _) $ (x as Var _) => [(find_index (equal x) args, SOME f)] + | _ => error ("Unsupported binding function: " ^ (Syntax.string_of_term lthy t)) +in + aux t +end + +(** definition of the raw binding functions **) + +fun prep_bn_info lthy dt_names dts bn_funs eqs = +let + fun process_eq eq = + let + val (lhs, rhs) = eq + |> HOLogic.dest_Trueprop + |> HOLogic.dest_eq + val (bn_fun, [cnstr]) = strip_comb lhs + val (_, ty) = dest_Const bn_fun + val (ty_name, _) = dest_Type (domain_type ty) + val dt_index = find_index (fn x => x = ty_name) dt_names + val (cnstr_head, cnstr_args) = strip_comb cnstr + val cnstr_name = Long_Name.base_name (fst (dest_Const cnstr_head)) + val rhs_elements = strip_bn_fun lthy cnstr_args rhs + in + ((bn_fun, dt_index), (cnstr_name, rhs_elements)) + end + + (* order according to constructor names *) + fun cntrs_order ((bn, dt_index), data) = + let + val dt = nth dts dt_index + val cts = (fn (_, _, _, x) => x) dt + val ct_names = map (Binding.name_of o (fn (x, _, _) => x)) cts + in + (bn, (bn, dt_index, order (op=) ct_names data)) + end +in + eqs + |> map process_eq + |> AList.group (op=) (* eqs grouped according to bn_functions *) + |> map cntrs_order (* inner data ordered according to constructors *) + |> 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 = + if null raw_bn_funs + then ([], [], [], [], lthy) + else + let + val (_, lthy1) = Function.add_function raw_bn_funs raw_bn_eqs + Function_Common.default_config (pat_completeness_simp constr_thms) lthy + + val (info, lthy2) = prove_termination 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) + in + (fs, raw_bn_eqs, raw_bn_info, raw_bn_induct, lthy2) + end + + + (** 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)) =