nominal2: comparison Nominal/nominal_dt

equal deleted inserted replaced

-:72ad4e766acf
+:8aff3f3ce47f
 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 setify: Proof.context -> term -> term
 val listify: Proof.context -> term -> term
-val define_raw_fvs:
+val define_raw_fvs: Datatype_Aux.descr -> (string * sort) list -> bn_info ->
-Datatype_Aux.descr ->
+bclause list list list -> Proof.context -> term list * term list * thm list * local_theory
-(string * sort) list ->
-term list ->
-(term * int * (int * term option) list list) list ->
-bclause list list list -> Proof.context -> term list * term list * thm list * local_theory
 end
 structure Nominal_Dt_RawFuns: NOMINAL_DT_RAWFUNS =
 struct
+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 *)
 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 concrete atoms, sets and fsets into sets
+(* functions that coerces singletons, sets and fsets of concrete atoms
-of general atoms *)
+into sets of general atoms *)
 fun setify ctxt t =
 let
 val ty = fastype_of t;
 in
 if is_atom ctxt ty
 else if is_atom_fset ctxt ty
 then mk_atom_fset t
 else raise TERM ("setify", [t])
 end
-(* functions that coerces concrete atoms and lists into lists of
+(* functions that coerces singletons and lists of concrete atoms
-general atoms  *)
+into lists of general atoms  *)
 fun listify ctxt t =
 let
 val ty = fastype_of t;
 in
 if is_atom ctxt ty
 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 *)
+(** functions that construct the equations for fv and fv_bn **)
-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
-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
 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 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 dt_descr sorts bn_trms bn_funs2 bclausesss lthy =
+fun define_raw_fvs descr sorts bn_info bclausesss lthy =
 let
-val fv_names = prefix_dt_names dt_descr sorts "fv_"
+val fv_names = prefix_dt_names descr sorts "fv_"
-val fv_arg_tys = map (fn (i, _) => nth_dtyp dt_descr sorts i) dt_descr;
+val fv_arg_tys = map (fn (i, _) => nth_dtyp descr sorts i) descr;
 val fv_tys = map (fn ty => ty --> @{typ "atom set"}) fv_arg_tys;
 val fv_frees = map Free (fv_names ~~ fv_tys);
 val fv_map = fv_arg_tys ~~ fv_frees
-val bn_tys2 = map (fn (_, i, _) => i) bn_funs2
+val (bns, bn_tys) = split_list (map (fn (bn, i, _) => (bn, i)) bn_info)
-val fv_bn_names2 = map (fn bn => "fv_" ^ (Long_Name.base_name (fst (dest_Const bn)))) bn_trms
+val bn_names = map (fn bn => Long_Name.base_name (fst (dest_Const bn))) bns
-val fv_bn_arg_tys2 = map (fn i => nth_dtyp dt_descr sorts i) bn_tys2
+val fv_bn_names = map (prefix "fv_") bn_names
-val fv_bn_tys2 = map (fn ty => ty --> @{typ "atom set"}) fv_bn_arg_tys2
+val fv_bn_arg_tys = map (fn i => nth_dtyp descr sorts i) bn_tys
-val fv_bn_frees2 = map Free (fv_bn_names2 ~~ fv_bn_tys2)
+val fv_bn_tys = map (fn ty => ty --> @{typ "atom set"}) fv_bn_arg_tys
-val fv_bn_map = bn_trms ~~ fv_bn_frees2
+val fv_bn_frees = map Free (fv_bn_names ~~ fv_bn_tys)
+val fv_bn_map = bns ~~ fv_bn_frees
-val constrs_info = all_dtyp_constrs_types dt_descr sorts
+val constrs_info = all_dtyp_constrs_types descr sorts
-val fv_eqs2 = map2 (map2 (mk_fv_eq lthy fv_map fv_bn_map)) constrs_info bclausesss
-val fv_bn_eqs2 = map (mk_fv_bn_eqs lthy fv_map fv_bn_map constrs_info bclausesss) bn_funs2
+val fv_eqs = map2 (map2 (mk_fv_eq lthy fv_map fv_bn_map)) constrs_info bclausesss
+val fv_bn_eqs = map (mk_fv_bn_eqs lthy fv_map fv_bn_map constrs_info bclausesss) bn_info
-val all_fv_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names2)
+val all_fun_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names)
-val all_fv_eqs = map (pair Attrib.empty_binding) (flat fv_eqs2 @ flat fv_bn_eqs2)
+val all_fun_eqs = map (pair Attrib.empty_binding) (flat fv_eqs @ flat fv_bn_eqs)
 fun pat_completeness_auto lthy =
 Pat_Completeness.pat_completeness_tac lthy 1
 THEN auto_tac (clasimpset_of lthy)
 fun prove_termination lthy =
 Function.prove_termination NONE
 (Lexicographic_Order.lexicographic_order_tac true lthy) lthy
-val (_, lthy') = Function.add_function all_fv_names all_fv_eqs
+val (_, lthy') = Function.add_function all_fun_names all_fun_eqs
 Function_Common.default_config pat_completeness_auto lthy
 val (info, lthy'') = prove_termination (Local_Theory.restore lthy')
 val {fs, simps, ...} = info;

changeset 2295	8aff3f3ce47f
parent 2294	72ad4e766acf
child 2296	45a69c9cc4cc