--- 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
*}
--- 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)) =