Nominal/Nominal2.thy
changeset 2633 d1d09177ec89
parent 2631 e73bd379e839
child 2634 3ce1089cdbf3
equal deleted inserted replaced
2632:e8732350a29f 2633:d1d09177ec89
   129   val dt_names = map (fn (_, s, _, _) => Binding.name_of s) dts
   129   val dt_names = map (fn (_, s, _, _) => Binding.name_of s) dts
   130   val dt_full_names = map (Long_Name.qualify thy_name) dt_names 
   130   val dt_full_names = map (Long_Name.qualify thy_name) dt_names 
   131   val dt_full_names' = add_raws dt_full_names
   131   val dt_full_names' = add_raws dt_full_names
   132   val dts_env = dt_full_names ~~ dt_full_names'
   132   val dts_env = dt_full_names ~~ dt_full_names'
   133 
   133 
   134   val cnstrs = get_cnstr_strs dts
   134   val cnstr_names = get_cnstr_strs dts
   135   val cnstrs_ty = get_typed_cnstrs dts
   135   val cnstr_tys = get_typed_cnstrs dts
   136   val cnstrs_full_names = map (Long_Name.qualify thy_name) cnstrs
   136   val cnstr_full_names = map (Long_Name.qualify thy_name) cnstr_names
   137   val cnstrs_full_names' = map (fn (x, y) => Long_Name.qualify thy_name 
   137   val cnstr_full_names' = map (fn (x, y) => Long_Name.qualify thy_name 
   138     (Long_Name.qualify (add_raw x) (add_raw y))) cnstrs_ty
   138     (Long_Name.qualify (add_raw x) (add_raw y))) cnstr_tys
   139   val cnstrs_env = cnstrs_full_names ~~ cnstrs_full_names'
   139   val cnstrs_env = cnstr_full_names ~~ cnstr_full_names'
   140 
   140 
   141   val bn_fun_strs = get_bn_fun_strs bn_funs
   141   val bn_fun_strs = get_bn_fun_strs bn_funs
   142   val bn_fun_strs' = add_raws bn_fun_strs
   142   val bn_fun_strs' = add_raws bn_fun_strs
   143   val bn_fun_env = bn_fun_strs ~~ bn_fun_strs'
   143   val bn_fun_env = bn_fun_strs ~~ bn_fun_strs'
   144   val bn_fun_full_env = map (pairself (Long_Name.qualify thy_name)) 
   144   val bn_fun_full_env = map (pairself (Long_Name.qualify thy_name)) 
   151   val (raw_dt_full_names, thy1) = 
   151   val (raw_dt_full_names, thy1) = 
   152     Datatype.add_datatype Datatype.default_config raw_dt_names raw_dts thy
   152     Datatype.add_datatype Datatype.default_config raw_dt_names raw_dts thy
   153 
   153 
   154   val lthy1 = Named_Target.theory_init thy1
   154   val lthy1 = Named_Target.theory_init thy1
   155 in
   155 in
   156   (raw_dt_full_names, raw_dts, raw_bclauses, raw_bn_funs, raw_bn_eqs, lthy1)
   156   (raw_dt_full_names, raw_dts, raw_bclauses, raw_bn_funs, raw_bn_eqs, cnstr_names, lthy1)
   157 end
   157 end
   158 *}
   158 *}
   159 
   159 
   160 ML {*
   160 ML {*
   161 (* for testing porposes - to exit the procedure early *)
   161 (* for testing porposes - to exit the procedure early *)
   172 ML {*
   172 ML {*
   173 fun nominal_datatype2 opt_thms_name dts bn_funs bn_eqs bclauses lthy =
   173 fun nominal_datatype2 opt_thms_name dts bn_funs bn_eqs bclauses lthy =
   174 let
   174 let
   175   (* definition of the raw datatypes *)
   175   (* definition of the raw datatypes *)
   176   val _ = warning "Definition of raw datatypes";
   176   val _ = warning "Definition of raw datatypes";
   177   val (raw_dt_names, raw_dts, raw_bclauses, raw_bn_funs, raw_bn_eqs, lthy0) =
   177   val (raw_dt_names, raw_dts, raw_bclauses, raw_bn_funs, raw_bn_eqs, cnstr_names, lthy0) =
   178     if get_STEPS lthy > 0 
   178     if get_STEPS lthy > 0 
   179     then define_raw_dts dts bn_funs bn_eqs bclauses lthy
   179     then define_raw_dts dts bn_funs bn_eqs bclauses lthy
   180     else raise TEST lthy
   180     else raise TEST lthy
   181 
   181 
   182   val dtinfo = Datatype.the_info (ProofContext.theory_of lthy0) (hd raw_dt_names)
   182   val dtinfo = Datatype.the_info (ProofContext.theory_of lthy0) (hd raw_dt_names)
   538 
   538 
   539   (* proving the strong exhausts and induct lemmas *)
   539   (* proving the strong exhausts and induct lemmas *)
   540   val qstrong_exhaust_thms = prove_strong_exhausts lthyC qexhausts bclauses qbn_finite_thms qeq_iffs'
   540   val qstrong_exhaust_thms = prove_strong_exhausts lthyC qexhausts bclauses qbn_finite_thms qeq_iffs'
   541     qfv_qbn_eqvts qpermute_bn_thms qperm_bn_alpha_thms
   541     qfv_qbn_eqvts qpermute_bn_thms qperm_bn_alpha_thms
   542 
   542 
   543   val qstrong_induct_thms = prove_strong_induct lthyC qinduct qstrong_exhaust_thms qsize_simps bclauses
   543   val qstrong_induct_thms =  prove_strong_induct lthyC qinduct qstrong_exhaust_thms qsize_simps bclauses
   544 
   544 
   545 
   545 
   546   (* noting the theorems *)  
   546   (* noting the theorems *)  
   547 
   547 
   548   (* generating the prefix for the theorem names *)
   548   (* generating the prefix for the theorem names *)
   549   val thms_name = 
   549   val thms_name = 
   550     the_default (Binding.name (space_implode "_" qty_names)) opt_thms_name 
   550     the_default (Binding.name (space_implode "_" qty_names)) opt_thms_name 
   551   fun thms_suffix s = Binding.qualified true s thms_name 
   551   fun thms_suffix s = Binding.qualified true s thms_name 
       
   552   val case_names_attr = Attrib.internal (K (Rule_Cases.case_names cnstr_names))
   552 
   553 
   553   val (_, lthy9') = lthyC
   554   val (_, lthy9') = lthyC
   554      |> Local_Theory.note ((thms_suffix "distinct", []), qdistincts) 
   555      |> Local_Theory.note ((thms_suffix "distinct", []), qdistincts) 
   555      ||>> Local_Theory.note ((thms_suffix "eq_iff", []), qeq_iffs')
   556      ||>> Local_Theory.note ((thms_suffix "eq_iff", []), qeq_iffs')
   556      ||>> Local_Theory.note ((thms_suffix "fv_defs", []), qfv_defs) 
   557      ||>> Local_Theory.note ((thms_suffix "fv_defs", []), qfv_defs) 
   557      ||>> Local_Theory.note ((thms_suffix "bn_defs", []), qbn_defs) 
   558      ||>> Local_Theory.note ((thms_suffix "bn_defs", []), qbn_defs) 
   558      ||>> Local_Theory.note ((thms_suffix "perm_simps", [eqvt_attr, simp_attr]), qperm_simps) 
   559      ||>> Local_Theory.note ((thms_suffix "perm_simps", [eqvt_attr, simp_attr]), qperm_simps) 
   559      ||>> Local_Theory.note ((thms_suffix "fv_bn_eqvt", []), qfv_qbn_eqvts) 
   560      ||>> Local_Theory.note ((thms_suffix "fv_bn_eqvt", []), qfv_qbn_eqvts) 
   560      ||>> Local_Theory.note ((thms_suffix "size", []), qsize_simps)
   561      ||>> Local_Theory.note ((thms_suffix "size", []), qsize_simps)
   561      ||>> Local_Theory.note ((thms_suffix "size_eqvt", []), qsize_eqvt)
   562      ||>> Local_Theory.note ((thms_suffix "size_eqvt", []), qsize_eqvt)
   562      ||>> Local_Theory.note ((thms_suffix "induct", []), [qinduct]) 
   563      ||>> Local_Theory.note ((thms_suffix "induct", [case_names_attr]), [qinduct]) 
   563      ||>> Local_Theory.note ((thms_suffix "inducts", []), qinducts)
   564      ||>> Local_Theory.note ((thms_suffix "inducts", [case_names_attr]), qinducts)
   564      ||>> Local_Theory.note ((thms_suffix "exhaust", []), qexhausts)
   565      ||>> Local_Theory.note ((thms_suffix "exhaust", [case_names_attr]), qexhausts)
   565      ||>> Local_Theory.note ((thms_suffix "strong_exhaust", []), qstrong_exhaust_thms)
   566      ||>> Local_Theory.note ((thms_suffix "strong_exhaust", [case_names_attr]), qstrong_exhaust_thms)
   566      ||>> Local_Theory.note ((thms_suffix "strong_induct", []), qstrong_induct_thms)
   567      ||>> Local_Theory.note ((thms_suffix "strong_induct", [case_names_attr]), qstrong_induct_thms)
   567      ||>> Local_Theory.note ((thms_suffix "supports", []), qsupports_thms)
   568      ||>> Local_Theory.note ((thms_suffix "supports", []), qsupports_thms)
   568      ||>> Local_Theory.note ((thms_suffix "fsupp", []), qfsupp_thms)
   569      ||>> Local_Theory.note ((thms_suffix "fsupp", []), qfsupp_thms)
   569      ||>> Local_Theory.note ((thms_suffix "supp", []), qsupp_constrs)
   570      ||>> Local_Theory.note ((thms_suffix "supp", []), qsupp_constrs)
   570      ||>> Local_Theory.note ((thms_suffix "fresh", []), qfresh_constrs)
   571      ||>> Local_Theory.note ((thms_suffix "fresh", []), qfresh_constrs)
   571      ||>> Local_Theory.note ((thms_suffix "raw_alpha", []), alpha_intros)
   572      ||>> Local_Theory.note ((thms_suffix "raw_alpha", []), alpha_intros)