emerging common infrastructure for datatype and rep_datatype
authorhaftmann
Sun Sep 27 20:58:25 2009 +0200 (2009-09-27)
changeset 32721a5fcc7960681
parent 32720 fc32e6771749
child 32722 ad04cda866be
emerging common infrastructure for datatype and rep_datatype
src/HOL/Tools/Datatype/datatype.ML
     1.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Sun Sep 27 20:43:47 2009 +0200
     1.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Sun Sep 27 20:58:25 2009 +0200
     1.3 @@ -268,37 +268,6 @@
     1.4  
     1.5  end;
     1.6  
     1.7 -(* note rules and interpretations *)
     1.8 -
     1.9 -fun add_rules simps case_thms rec_thms inject distinct
    1.10 -                  weak_case_congs cong_att =
    1.11 -  PureThy.add_thmss [((Binding.name "simps", simps), []),
    1.12 -    ((Binding.empty, flat case_thms @
    1.13 -          flat distinct @ rec_thms), [Simplifier.simp_add]),
    1.14 -    ((Binding.empty, rec_thms), [Code.add_default_eqn_attribute]),
    1.15 -    ((Binding.empty, flat inject), [iff_add]),
    1.16 -    ((Binding.empty, map (fn th => th RS notE) (flat distinct)), [Classical.safe_elim NONE]),
    1.17 -    ((Binding.empty, weak_case_congs), [cong_att])]
    1.18 -  #> snd;
    1.19 -
    1.20 -fun add_cases_induct infos inducts thy =
    1.21 -  let
    1.22 -    fun named_rules (name, {index, exhaust, ...}: info) =
    1.23 -      [((Binding.empty, nth inducts index), [Induct.induct_type name]),
    1.24 -       ((Binding.empty, exhaust), [Induct.cases_type name])];
    1.25 -    fun unnamed_rule i =
    1.26 -      ((Binding.empty, nth inducts i), [Thm.kind_internal, Induct.induct_type ""]);
    1.27 -  in
    1.28 -    thy |> PureThy.add_thms
    1.29 -      (maps named_rules infos @
    1.30 -        map unnamed_rule (length infos upto length inducts - 1)) |> snd
    1.31 -    |> PureThy.add_thmss [((Binding.name "inducts", inducts), [])] |> snd
    1.32 -  end;
    1.33 -
    1.34 -structure DatatypeInterpretation = InterpretationFun
    1.35 -  (type T = config * string list val eq: T * T -> bool = eq_snd op =);
    1.36 -fun interpretation f = DatatypeInterpretation.interpretation (uncurry f);
    1.37 -
    1.38  (* translation rules for case *)
    1.39  
    1.40  fun make_case ctxt = DatatypeCase.make_case
    1.41 @@ -345,23 +314,45 @@
    1.42      in ThyOutput.output (ThyOutput.maybe_pretty_source (K pretty_datatype) src [()]) end);
    1.43  
    1.44  
    1.45 -(** declare existing type as datatype **)
    1.46 +(** abstract theory extensions relative to a datatype characterisation **)
    1.47 +
    1.48 +structure DatatypeInterpretation = InterpretationFun
    1.49 +  (type T = config * string list val eq: T * T -> bool = eq_snd op =);
    1.50 +fun interpretation f = DatatypeInterpretation.interpretation (uncurry f);
    1.51 +
    1.52 +fun add_rules simps case_thms rec_thms inject distinct
    1.53 +                  weak_case_congs cong_att =
    1.54 +  PureThy.add_thmss [((Binding.name "simps", simps), []),
    1.55 +    ((Binding.empty, flat case_thms @
    1.56 +          flat distinct @ rec_thms), [Simplifier.simp_add]),
    1.57 +    ((Binding.empty, rec_thms), [Code.add_default_eqn_attribute]),
    1.58 +    ((Binding.empty, flat inject), [iff_add]),
    1.59 +    ((Binding.empty, map (fn th => th RS notE) (flat distinct)), [Classical.safe_elim NONE]),
    1.60 +    ((Binding.empty, weak_case_congs), [cong_att])]
    1.61 +  #> snd;
    1.62  
    1.63 -fun prove_rep_datatype (config : config) dt_names alt_names descr sorts raw_induct raw_inject half_distinct thy1 =
    1.64 +fun add_cases_induct infos inducts thy =
    1.65    let
    1.66 -    val raw_distinct = (map o maps) (fn thm => [thm, thm RS not_sym]) half_distinct;
    1.67 +    fun named_rules (name, {index, exhaust, ...}: info) =
    1.68 +      [((Binding.empty, nth inducts index), [Induct.induct_type name]),
    1.69 +       ((Binding.empty, exhaust), [Induct.cases_type name])];
    1.70 +    fun unnamed_rule i =
    1.71 +      ((Binding.empty, nth inducts i), [Thm.kind_internal, Induct.induct_type ""]);
    1.72 +  in
    1.73 +    thy |> PureThy.add_thms
    1.74 +      (maps named_rules infos @
    1.75 +        map unnamed_rule (length infos upto length inducts - 1)) |> snd
    1.76 +    |> PureThy.add_thmss [((Binding.name "inducts", inducts), [])] |> snd
    1.77 +  end;
    1.78 +
    1.79 +fun derive_datatype_props config dt_names alt_names descr sorts induct inject distinct thy2 =
    1.80 +  let
    1.81      val new_type_names = map Long_Name.base_name (the_default dt_names alt_names);
    1.82 +    val _ = message config ("Proofs for datatype(s) " ^ commas_quote new_type_names);
    1.83      val (case_names_induct, case_names_exhausts) =
    1.84        (mk_case_names_induct descr, mk_case_names_exhausts descr dt_names);
    1.85 -    val (((inject, distinct), [induct]), thy2) =
    1.86 -      thy1
    1.87 -      |> store_thmss "inject" new_type_names raw_inject
    1.88 -      ||>> store_thmss "distinct" new_type_names raw_distinct
    1.89 -      ||> Sign.add_path (space_implode "_" new_type_names)
    1.90 -      ||>> PureThy.add_thms [((Binding.name "induct", raw_induct), [case_names_induct])];
    1.91 +    val inducts = Project_Rule.projections (ProofContext.init thy2) induct;
    1.92  
    1.93 -    val _ = message config ("Proofs for datatype(s) " ^ commas_quote new_type_names);
    1.94 -    val inducts = Project_Rule.projections (ProofContext.init thy2) induct;
    1.95      val (casedist_thms, thy3) = thy2 |>
    1.96        DatatypeAbsProofs.prove_casedist_thms config new_type_names [descr] sorts induct
    1.97          case_names_exhausts;
    1.98 @@ -397,7 +388,24 @@
    1.99      |> pair dt_names
   1.100    end;
   1.101  
   1.102 -fun gen_rep_datatype prep_term (config : config) after_qed alt_names raw_ts thy =
   1.103 +
   1.104 +(** declare existing type as datatype **)
   1.105 +
   1.106 +fun prove_rep_datatype config dt_names alt_names descr sorts raw_induct raw_inject half_distinct thy1 =
   1.107 +  let
   1.108 +    val raw_distinct = (map o maps) (fn thm => [thm, thm RS not_sym]) half_distinct;
   1.109 +    val new_type_names = map Long_Name.base_name (the_default dt_names alt_names);
   1.110 +    val (case_names_induct, case_names_exhausts) =
   1.111 +      (mk_case_names_induct descr, mk_case_names_exhausts descr dt_names);
   1.112 +    val (((inject, distinct), [induct]), thy2) =
   1.113 +      thy1
   1.114 +      |> store_thmss "inject" new_type_names raw_inject
   1.115 +      ||>> store_thmss "distinct" new_type_names raw_distinct
   1.116 +      ||> Sign.add_path (space_implode "_" new_type_names)
   1.117 +      ||>> PureThy.add_thms [((Binding.name "induct", raw_induct), [case_names_induct])];
   1.118 +  in derive_datatype_props config dt_names alt_names descr sorts induct inject distinct thy2 end;
   1.119 +
   1.120 +fun gen_rep_datatype prep_term config after_qed alt_names raw_ts thy =
   1.121    let
   1.122      fun constr_of_term (Const (c, T)) = (c, T)
   1.123        | constr_of_term t =
   1.124 @@ -468,7 +476,7 @@
   1.125  
   1.126  (** definitional introduction of datatypes **)
   1.127  
   1.128 -fun add_datatype_def (config : config) new_type_names descr sorts types_syntax constr_syntax dt_info
   1.129 +fun add_datatype_def config new_type_names descr sorts types_syntax constr_syntax dt_info
   1.130      case_names_induct case_names_exhausts thy =
   1.131    let
   1.132      val _ = message config ("Proofs for datatype(s) " ^ commas_quote new_type_names);
   1.133 @@ -515,7 +523,7 @@
   1.134        |> DatatypeInterpretation.data (config, map fst dt_infos);
   1.135    in (dt_names, thy12) end;
   1.136  
   1.137 -fun gen_add_datatype prep_typ (config : config) new_type_names dts thy =
   1.138 +fun gen_add_datatype prep_typ config new_type_names dts thy =
   1.139    let
   1.140      val _ = Theory.requires thy "Datatype" "datatype definitions";
   1.141  
   1.142 @@ -582,7 +590,7 @@
   1.143      val case_names_exhausts = mk_case_names_exhausts descr' (map #1 new_dts);
   1.144    in
   1.145      add_datatype_def
   1.146 -      (config : config) new_type_names descr sorts types_syntax constr_syntax dt_info
   1.147 +      config new_type_names descr sorts types_syntax constr_syntax dt_info
   1.148        case_names_induct case_names_exhausts thy
   1.149    end;
   1.150