Deleted code for axiomatic introduction of datatypes. Instead, the package
authorberghofe
Thu Apr 03 17:52:51 2008 +0200 (2008-04-03)
changeset 26533aeef55a3d1d5
parent 26532 3fc9730403c1
child 26534 a2cb4de2a1aa
Deleted code for axiomatic introduction of datatypes. Instead, the package
now uses SkipProof.prove rather than Goal.prove to do proofs.
src/HOL/Tools/datatype_package.ML
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Thu Apr 03 17:50:50 2008 +0200
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Thu Apr 03 17:52:51 2008 +0200
     1.3 @@ -380,12 +380,8 @@
     1.4  
     1.5  val distinctN = "constr_distinct";
     1.6  
     1.7 -exception ConstrDistinct of term;
     1.8 -
     1.9  fun distinct_rule thy ss tname eq_t = case #distinct (the_datatype thy tname) of
    1.10 -    QuickAndDirty => Thm.invoke_oracle
    1.11 -      (ThyInfo.the_theory "Datatype" thy) distinctN (thy, ConstrDistinct eq_t)
    1.12 -  | FewConstrs thms => Goal.prove (Simplifier.the_context ss) [] [] eq_t (K
    1.13 +    FewConstrs thms => Goal.prove (Simplifier.the_context ss) [] [] eq_t (K
    1.14        (EVERY [rtac eq_reflection 1, rtac iffI 1, rtac notE 1,
    1.15          atac 2, resolve_tac thms 1, etac FalseE 1]))
    1.16    | ManyConstrs (thm, simpset) =>
    1.17 @@ -427,7 +423,6 @@
    1.18  val dist_ss = HOL_ss addsimprocs [distinct_simproc];
    1.19  
    1.20  val simproc_setup =
    1.21 -  Theory.add_oracle (distinctN, fn (_, ConstrDistinct t) => t) #>
    1.22    Simplifier.map_simpset (fn ss => ss addsimprocs [distinct_simproc]);
    1.23  
    1.24  
    1.25 @@ -494,181 +489,9 @@
    1.26      case_cong = case_cong,
    1.27      weak_case_cong = weak_case_cong});
    1.28  
    1.29 -
    1.30 -(********************* axiomatic introduction of datatypes ********************)
    1.31 -
    1.32 -fun add_axiom label t atts thy =
    1.33 -  thy
    1.34 -  |> PureThy.add_axioms_i [((label, t), atts)];
    1.35 -
    1.36 -fun add_axioms label ts atts thy =
    1.37 -  thy
    1.38 -  |> PureThy.add_axiomss_i [((label, ts), atts)];
    1.39 -
    1.40 -fun add_and_get_axioms_atts label tnames ts attss =
    1.41 -  fold_map (fn (tname, (atts, t)) => fn thy =>
    1.42 -    thy
    1.43 -    |> Sign.add_path tname
    1.44 -    |> add_axiom label t atts
    1.45 -    ||> Sign.parent_path
    1.46 -    |-> (fn [ax] => pair ax)) (tnames ~~ (attss ~~ ts));
    1.47 -
    1.48 -fun add_and_get_axioms label tnames ts =
    1.49 -  add_and_get_axioms_atts label tnames ts (replicate (length tnames) []);
    1.50 -
    1.51 -fun add_and_get_axiomss label tnames tss =
    1.52 -  fold_map (fn (tname, ts) => fn thy =>
    1.53 -    thy
    1.54 -    |> Sign.add_path tname
    1.55 -    |> add_axioms label ts []
    1.56 -    ||> Sign.parent_path
    1.57 -    |-> (fn [ax] => pair ax)) (tnames ~~ tss);
    1.58 -
    1.59 -fun gen_specify_consts add args thy =
    1.60 -  let
    1.61 -    val specs = map (fn (c, T, mx) =>
    1.62 -      Const (Sign.full_name thy (Syntax.const_name c mx), T)) args;
    1.63 -  in
    1.64 -    thy
    1.65 -    |> add args
    1.66 -    |> Theory.add_finals_i false specs
    1.67 -  end;
    1.68 -
    1.69 -val specify_consts = gen_specify_consts Sign.add_consts_i;
    1.70 -val specify_consts_authentic = gen_specify_consts (fold (snd oo Sign.declare_const []));
    1.71 -
    1.72  structure DatatypeInterpretation = InterpretationFun(type T = string list val eq = op =);
    1.73  val interpretation = DatatypeInterpretation.interpretation;
    1.74  
    1.75 -fun add_datatype_axm flat_names new_type_names descr sorts types_syntax constr_syntax dt_info
    1.76 -    case_names_induct case_names_exhausts thy =
    1.77 -  let
    1.78 -    val descr' = flat descr;
    1.79 -    val recTs = get_rec_types descr' sorts;
    1.80 -    val used = map fst (fold Term.add_tfreesT recTs []);
    1.81 -    val newTs = Library.take (length (hd descr), recTs);
    1.82 -
    1.83 -    (**** declare new types and constants ****)
    1.84 -
    1.85 -    val tyvars = map (fn (_, (_, Ts, _)) => map dest_DtTFree Ts) (hd descr);
    1.86 -
    1.87 -    val constr_decls = map (fn (((_, (_, _, constrs)), T), constr_syntax') =>
    1.88 -      map (fn ((_, cargs), (cname, mx)) =>
    1.89 -        (cname, map (typ_of_dtyp descr' sorts) cargs ---> T, mx))
    1.90 -          (constrs ~~ constr_syntax')) ((hd descr) ~~ newTs ~~ constr_syntax);
    1.91 -
    1.92 -    val (rec_result_Ts, reccomb_fn_Ts) = DatatypeProp.make_primrec_Ts descr sorts used;
    1.93 -
    1.94 -    val big_reccomb_name = (space_implode "_" new_type_names) ^ "_rec";
    1.95 -    val reccomb_names = if length descr' = 1 then [big_reccomb_name] else
    1.96 -      (map ((curry (op ^) (big_reccomb_name ^ "_")) o string_of_int)
    1.97 -        (1 upto (length descr')));
    1.98 -
    1.99 -    val freeT = TFree (Name.variant used "'t", HOLogic.typeS);
   1.100 -    val case_fn_Ts = map (fn (i, (_, _, constrs)) =>
   1.101 -      map (fn (_, cargs) =>
   1.102 -        let val Ts = map (typ_of_dtyp descr' sorts) cargs
   1.103 -        in Ts ---> freeT end) constrs) (hd descr);
   1.104 -
   1.105 -    val case_names = map (fn s => (s ^ "_case")) new_type_names;
   1.106 -
   1.107 -    val thy2' = thy
   1.108 -
   1.109 -      (** new types **)
   1.110 -      |> fold2 (fn (name, mx) => fn tvs => ObjectLogic.typedecl (name, tvs, mx) #> snd)
   1.111 -           types_syntax tyvars
   1.112 -      |> add_path flat_names (space_implode "_" new_type_names)
   1.113 -
   1.114 -      (** primrec combinators **)
   1.115 -
   1.116 -      |> specify_consts (map (fn ((name, T), T') =>
   1.117 -           (name, reccomb_fn_Ts @ [T] ---> T', NoSyn)) (reccomb_names ~~ recTs ~~ rec_result_Ts))
   1.118 -
   1.119 -      (** case combinators **)
   1.120 -
   1.121 -      |> specify_consts_authentic (map (fn ((name, T), Ts) =>
   1.122 -           (name, Ts @ [T] ---> freeT, NoSyn)) (case_names ~~ newTs ~~ case_fn_Ts));
   1.123 -
   1.124 -    val reccomb_names' = map (Sign.full_name thy2') reccomb_names;
   1.125 -    val case_names' = map (Sign.full_name thy2') case_names;
   1.126 -
   1.127 -    val thy2 = thy2'
   1.128 -
   1.129 -      (** constructors **)
   1.130 -
   1.131 -      |> parent_path flat_names
   1.132 -      |> fold (fn ((((_, (_, _, constrs)), T), tname),
   1.133 -        constr_syntax') =>
   1.134 -          add_path flat_names tname #>
   1.135 -            specify_consts (map (fn ((_, cargs), (cname, mx)) =>
   1.136 -              (cname, map (typ_of_dtyp descr' sorts) cargs ---> T, mx))
   1.137 -                (constrs ~~ constr_syntax')) #>
   1.138 -          parent_path flat_names)
   1.139 -            (hd descr ~~ newTs ~~ new_type_names ~~ constr_syntax);
   1.140 -
   1.141 -    (**** introduction of axioms ****)
   1.142 -
   1.143 -    val rec_axs = DatatypeProp.make_primrecs new_type_names descr sorts thy2;
   1.144 -
   1.145 -    val ((([induct], [rec_thms]), inject), thy3) =
   1.146 -      thy2
   1.147 -      |> Sign.add_path (space_implode "_" new_type_names)
   1.148 -      |> add_axiom "induct" (DatatypeProp.make_ind descr sorts) [case_names_induct]
   1.149 -      ||>> add_axioms "recs" rec_axs []
   1.150 -      ||> Sign.parent_path
   1.151 -      ||>> add_and_get_axiomss "inject" new_type_names
   1.152 -            (DatatypeProp.make_injs descr sorts);
   1.153 -    val (distinct, thy4) = add_and_get_axiomss "distinct" new_type_names
   1.154 -      (DatatypeProp.make_distincts new_type_names descr sorts thy3) thy3;
   1.155 -
   1.156 -    val exhaust_ts = DatatypeProp.make_casedists descr sorts;
   1.157 -    val (exhaustion, thy5) = add_and_get_axioms_atts "exhaust" new_type_names
   1.158 -      exhaust_ts (map single case_names_exhausts) thy4;
   1.159 -    val (case_thms, thy6) = add_and_get_axiomss "cases" new_type_names
   1.160 -      (DatatypeProp.make_cases new_type_names descr sorts thy5) thy5;
   1.161 -    val (split_ts, split_asm_ts) = ListPair.unzip
   1.162 -      (DatatypeProp.make_splits new_type_names descr sorts thy6);
   1.163 -    val (split, thy7) = add_and_get_axioms "split" new_type_names split_ts thy6;
   1.164 -    val (split_asm, thy8) = add_and_get_axioms "split_asm" new_type_names
   1.165 -      split_asm_ts thy7;
   1.166 -    val (nchotomys, thy9) = add_and_get_axioms "nchotomy" new_type_names
   1.167 -      (DatatypeProp.make_nchotomys descr sorts) thy8;
   1.168 -    val (case_congs, thy10) = add_and_get_axioms "case_cong" new_type_names
   1.169 -      (DatatypeProp.make_case_congs new_type_names descr sorts thy9) thy9;
   1.170 -    val (weak_case_congs, thy11) = add_and_get_axioms "weak_case_cong" new_type_names
   1.171 -      (DatatypeProp.make_weak_case_congs new_type_names descr sorts thy10) thy10;
   1.172 -
   1.173 -    val dt_infos = map (make_dt_info NONE descr' sorts induct reccomb_names' rec_thms)
   1.174 -      ((0 upto length (hd descr) - 1) ~~ (hd descr) ~~ case_names' ~~ case_thms ~~
   1.175 -        exhaustion ~~ replicate (length (hd descr)) QuickAndDirty ~~ inject ~~
   1.176 -          nchotomys ~~ case_congs ~~ weak_case_congs);
   1.177 -
   1.178 -    val simps = flat (distinct @ inject @ case_thms) @ rec_thms;
   1.179 -    val split_thms = split ~~ split_asm;
   1.180 -
   1.181 -    val thy12 =
   1.182 -      thy11
   1.183 -      |> add_case_tr' case_names'
   1.184 -      |> Sign.add_path (space_implode "_" new_type_names)
   1.185 -      |> add_rules simps case_thms rec_thms inject distinct
   1.186 -          weak_case_congs Simplifier.cong_add
   1.187 -      |> put_dt_infos dt_infos
   1.188 -      |> add_cases_induct dt_infos induct
   1.189 -      |> Sign.parent_path
   1.190 -      |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)
   1.191 -      |> snd
   1.192 -      |> DatatypeInterpretation.data (map fst dt_infos);
   1.193 -  in
   1.194 -    ({distinct = distinct,
   1.195 -      inject = inject,
   1.196 -      exhaustion = exhaustion,
   1.197 -      rec_thms = rec_thms,
   1.198 -      case_thms = case_thms,
   1.199 -      split_thms = split_thms,
   1.200 -      induction = induct,
   1.201 -      simps = simps}, thy12)
   1.202 -  end;
   1.203 -
   1.204  
   1.205  (******************* definitional introduction of datatypes *******************)
   1.206  
   1.207 @@ -897,7 +720,7 @@
   1.208      val case_names_induct = mk_case_names_induct descr';
   1.209      val case_names_exhausts = mk_case_names_exhausts descr' (map #1 new_dts);
   1.210    in
   1.211 -    (if (!quick_and_dirty) then add_datatype_axm else add_datatype_def)
   1.212 +    add_datatype_def
   1.213        flat_names new_type_names descr sorts types_syntax constr_syntax dt_info
   1.214        case_names_induct case_names_exhausts thy
   1.215    end;