Nominal/nominal_dt_rawfuns.ML
changeset 2304 8a98171ba1fc
parent 2297 9ca7b249760e
child 2305 93ab397f5980
equal deleted inserted replaced
2303:c785fff02a8f 2304:8a98171ba1fc
    19   val is_atom_fset: Proof.context -> typ -> bool
    19   val is_atom_fset: Proof.context -> typ -> bool
    20   val is_atom_list: Proof.context -> typ -> bool
    20   val is_atom_list: Proof.context -> typ -> bool
    21   val mk_atom_set: term -> term
    21   val mk_atom_set: term -> term
    22   val mk_atom_fset: term -> term
    22   val mk_atom_fset: term -> term
    23 
    23 
    24 
       
    25   val setify: Proof.context -> term -> term
    24   val setify: Proof.context -> term -> term
    26   val listify: Proof.context -> term -> term
    25   val listify: Proof.context -> term -> term
    27 
    26 
    28   val define_raw_fvs: Datatype_Aux.descr -> (string * sort) list -> bn_info ->
    27   val define_raw_fvs: Datatype_Aux.descr -> (string * sort) list -> bn_info ->
    29     bclause list list list -> Proof.context -> term list * term list * thm list * local_theory
    28     bclause list list list -> thm list -> Proof.context -> term list * term list * thm list * local_theory
    30 end
    29 end
    31 
    30 
    32 
    31 
    33 structure Nominal_Dt_RawFuns: NOMINAL_DT_RAWFUNS =
    32 structure Nominal_Dt_RawFuns: NOMINAL_DT_RAWFUNS =
    34 struct
    33 struct
   198   val nth_bclausess = nth bclausesss bn_n
   197   val nth_bclausess = nth bclausesss bn_n
   199 in
   198 in
   200   map2 (mk_fv_bn_eq lthy bn_trm fv_map fv_bn_map) (bn_argss ~~ nth_constrs_info) nth_bclausess
   199   map2 (mk_fv_bn_eq lthy bn_trm fv_map fv_bn_map) (bn_argss ~~ nth_constrs_info) nth_bclausess
   201 end
   200 end
   202 
   201 
   203 fun define_raw_fvs descr sorts bn_info bclausesss lthy =
   202 fun define_raw_fvs descr sorts bn_info bclausesss constr_thms lthy =
   204 let
   203 let
   205   val fv_names = prefix_dt_names descr sorts "fv_"
   204   val fv_names = prefix_dt_names descr sorts "fv_"
   206   val fv_arg_tys = all_dtyps descr sorts
   205   val fv_arg_tys = all_dtyps descr sorts
   207   val fv_tys = map (fn ty => ty --> @{typ "atom set"}) fv_arg_tys;
   206   val fv_tys = map (fn ty => ty --> @{typ "atom set"}) fv_arg_tys;
   208   val fv_frees = map Free (fv_names ~~ fv_tys);
   207   val fv_frees = map Free (fv_names ~~ fv_tys);
   222   val fv_bn_eqs = map (mk_fv_bn_eqs lthy fv_map fv_bn_map constrs_info bclausesss) bn_info
   221   val fv_bn_eqs = map (mk_fv_bn_eqs lthy fv_map fv_bn_map constrs_info bclausesss) bn_info
   223   
   222   
   224   val all_fun_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names)
   223   val all_fun_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names)
   225   val all_fun_eqs = map (pair Attrib.empty_binding) (flat fv_eqs @ flat fv_bn_eqs)
   224   val all_fun_eqs = map (pair Attrib.empty_binding) (flat fv_eqs @ flat fv_bn_eqs)
   226 
   225 
   227   fun pat_completeness_auto lthy =
       
   228     Pat_Completeness.pat_completeness_tac lthy 1
       
   229       THEN auto_tac (clasimpset_of lthy)
       
   230 
       
   231   fun prove_termination lthy =
       
   232     Function.prove_termination NONE
       
   233       (Lexicographic_Order.lexicographic_order_tac true lthy) lthy
       
   234 
       
   235   val (_, lthy') = Function.add_function all_fun_names all_fun_eqs
   226   val (_, lthy') = Function.add_function all_fun_names all_fun_eqs
   236     Function_Common.default_config pat_completeness_auto lthy
   227     Function_Common.default_config (pat_completeness_simp constr_thms) lthy
   237 
   228 
   238   val (info, lthy'') = prove_termination (Local_Theory.restore lthy')
   229   val (info, lthy'') = prove_termination (Local_Theory.restore lthy')
   239 
   230 
   240   val {fs, simps, ...} = info;
   231   val {fs, simps, ...} = info;
   241 
   232