add_datatypes does not yield particular rules any longer
authorhaftmann
Tue Jun 23 15:32:34 2009 +0200 (2009-06-23)
changeset 31783cfbe9609ceb1
parent 31782 2b041d16cc13
child 31784 bd3486c57ba3
add_datatypes does not yield particular rules any longer
src/HOL/Nominal/nominal.ML
src/HOL/Nominal/nominal_atoms.ML
src/HOL/Tools/Datatype/datatype.ML
src/HOL/Tools/inductive_realizer.ML
     1.1 --- a/src/HOL/Nominal/nominal.ML	Tue Jun 23 14:51:21 2009 +0200
     1.2 +++ b/src/HOL/Nominal/nominal.ML	Tue Jun 23 15:32:34 2009 +0200
     1.3 @@ -241,13 +241,12 @@
     1.4          map replace_types cargs, NoSyn)) constrs)) dts';
     1.5  
     1.6      val new_type_names' = map (fn n => n ^ "_Rep") new_type_names;
     1.7 -    val full_new_type_names' = map (Sign.full_bname thy) new_type_names';
     1.8  
     1.9 -    val ((dt_names, {induction, ...}),thy1) =
    1.10 +    val (full_new_type_names',thy1) =
    1.11        Datatype.add_datatype config new_type_names' dts'' thy;
    1.12  
    1.13 -    val SOME {descr, ...} = Symtab.lookup
    1.14 -      (Datatype.get_datatypes thy1) (hd full_new_type_names');
    1.15 +    val {descr, induction, ...} =
    1.16 +      Datatype.the_datatype thy1 (hd full_new_type_names');
    1.17      fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);
    1.18  
    1.19      val big_name = space_implode "_" new_type_names;
     2.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Tue Jun 23 14:51:21 2009 +0200
     2.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Tue Jun 23 15:32:34 2009 +0200
     2.3 @@ -101,9 +101,10 @@
     2.4      val (_,thy1) = 
     2.5      fold_map (fn ak => fn thy => 
     2.6            let val dt = ([], Binding.name ak, NoSyn, [(Binding.name ak, [@{typ nat}], NoSyn)])
     2.7 -              val ((dt_names, {inject,case_thms,...}),thy1) = Datatype.add_datatype
     2.8 -                Datatype.default_config [ak] [dt] thy
     2.9 -              val inject_flat = flat inject
    2.10 +              val (dt_names, thy1) = Datatype.add_datatype
    2.11 +                Datatype.default_config [ak] [dt] thy;
    2.12 +            
    2.13 +              val injects = maps (#inject o Datatype.the_datatype thy1) dt_names;
    2.14                val ak_type = Type (Sign.intern_type thy1 ak,[])
    2.15                val ak_sign = Sign.intern_const thy1 ak 
    2.16                
    2.17 @@ -115,7 +116,7 @@
    2.18                    (Const (@{const_name "inj_on"},inj_on_type) $ 
    2.19                           Const (ak_sign,inj_type) $ HOLogic.mk_UNIV @{typ nat})
    2.20  
    2.21 -              val simp1 = @{thm inj_on_def}::inject_flat
    2.22 +              val simp1 = @{thm inj_on_def} :: injects;
    2.23                
    2.24                val proof1 = fn _ => EVERY [simp_tac (HOL_basic_ss addsimps simp1) 1,
    2.25                                            rtac @{thm ballI} 1,
     3.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Tue Jun 23 14:51:21 2009 +0200
     3.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Tue Jun 23 15:32:34 2009 +0200
     3.3 @@ -8,11 +8,7 @@
     3.4  sig
     3.5    include DATATYPE_COMMON
     3.6    val add_datatype : config -> string list -> (string list * binding * mixfix *
     3.7 -    (binding * typ list * mixfix) list) list -> theory ->
     3.8 -     (string list * {inject : thm list list,
     3.9 -      rec_thms : thm list,
    3.10 -      case_thms : thm list list,
    3.11 -      induction : thm}) * theory
    3.12 +    (binding * typ list * mixfix) list) list -> theory -> string list * theory
    3.13    val datatype_cmd : string list -> (string list * binding * mixfix *
    3.14      (binding * string list * mixfix) list) list -> theory -> theory
    3.15    val rep_datatype : config -> (string list -> Proof.context -> Proof.context)
    3.16 @@ -381,12 +377,7 @@
    3.17        |> Sign.parent_path
    3.18        |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms) |> snd
    3.19        |> DatatypeInterpretation.data (config, map fst dt_infos);
    3.20 -  in
    3.21 -    ((dt_names, {inject = inject,
    3.22 -      rec_thms = rec_thms,
    3.23 -      case_thms = case_thms,
    3.24 -      induction = induct}), thy12)
    3.25 -  end;
    3.26 +  in (dt_names, thy12) end;
    3.27  
    3.28  
    3.29  (*********************** declare existing type as datatype *********************)
     4.1 --- a/src/HOL/Tools/inductive_realizer.ML	Tue Jun 23 14:51:21 2009 +0200
     4.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Tue Jun 23 15:32:34 2009 +0200
     4.3 @@ -305,15 +305,17 @@
     4.4  
     4.5      (** datatype representing computational content of inductive set **)
     4.6  
     4.7 -    val ((dummies, (dt_names_rules)), thy2) =
     4.8 +    val ((dummies, some_dt_names), thy2) =
     4.9        thy1
    4.10        |> add_dummies (Datatype.add_datatype
    4.11             { strict = false, flat_names = false, quiet = false } (map (Binding.name_of o #2) dts))
    4.12             (map (pair false) dts) []
    4.13        ||> Extraction.add_typeof_eqns_i ty_eqs
    4.14        ||> Extraction.add_realizes_eqns_i rlz_eqs;
    4.15 -    val rec_thms = these (Option.map (#rec_thms o snd) dt_names_rules);
    4.16 -    val case_thms = these (Option.map (#case_thms o snd) dt_names_rules);
    4.17 +    val dt_names = these some_dt_names;
    4.18 +    val case_thms = map (#case_rewrites o Datatype.the_datatype thy2) dt_names;
    4.19 +    val rec_thms = if null dt_names then []
    4.20 +      else (#rec_rewrites o Datatype.the_datatype thy2) (hd dt_names);
    4.21      val rec_names = distinct (op =) (map (fst o dest_Const o head_of o fst o
    4.22        HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) rec_thms);
    4.23      val (constrss, _) = fold_map (fn (s, rs) => fn (recs, dummies) =>