# HG changeset patch # User berghofe # Date 1207237971 -7200 # Node ID aeef55a3d1d5c9d910a2a42a00bd1f163fd256b8 # Parent 3fc9730403c1382fa6a187f99e5a49fc4e13cf5f Deleted code for axiomatic introduction of datatypes. Instead, the package now uses SkipProof.prove rather than Goal.prove to do proofs. diff -r 3fc9730403c1 -r aeef55a3d1d5 src/HOL/Tools/datatype_package.ML --- a/src/HOL/Tools/datatype_package.ML Thu Apr 03 17:50:50 2008 +0200 +++ b/src/HOL/Tools/datatype_package.ML Thu Apr 03 17:52:51 2008 +0200 @@ -380,12 +380,8 @@ val distinctN = "constr_distinct"; -exception ConstrDistinct of term; - fun distinct_rule thy ss tname eq_t = case #distinct (the_datatype thy tname) of - QuickAndDirty => Thm.invoke_oracle - (ThyInfo.the_theory "Datatype" thy) distinctN (thy, ConstrDistinct eq_t) - | FewConstrs thms => Goal.prove (Simplifier.the_context ss) [] [] eq_t (K + FewConstrs thms => Goal.prove (Simplifier.the_context ss) [] [] eq_t (K (EVERY [rtac eq_reflection 1, rtac iffI 1, rtac notE 1, atac 2, resolve_tac thms 1, etac FalseE 1])) | ManyConstrs (thm, simpset) => @@ -427,7 +423,6 @@ val dist_ss = HOL_ss addsimprocs [distinct_simproc]; val simproc_setup = - Theory.add_oracle (distinctN, fn (_, ConstrDistinct t) => t) #> Simplifier.map_simpset (fn ss => ss addsimprocs [distinct_simproc]); @@ -494,181 +489,9 @@ case_cong = case_cong, weak_case_cong = weak_case_cong}); - -(********************* axiomatic introduction of datatypes ********************) - -fun add_axiom label t atts thy = - thy - |> PureThy.add_axioms_i [((label, t), atts)]; - -fun add_axioms label ts atts thy = - thy - |> PureThy.add_axiomss_i [((label, ts), atts)]; - -fun add_and_get_axioms_atts label tnames ts attss = - fold_map (fn (tname, (atts, t)) => fn thy => - thy - |> Sign.add_path tname - |> add_axiom label t atts - ||> Sign.parent_path - |-> (fn [ax] => pair ax)) (tnames ~~ (attss ~~ ts)); - -fun add_and_get_axioms label tnames ts = - add_and_get_axioms_atts label tnames ts (replicate (length tnames) []); - -fun add_and_get_axiomss label tnames tss = - fold_map (fn (tname, ts) => fn thy => - thy - |> Sign.add_path tname - |> add_axioms label ts [] - ||> Sign.parent_path - |-> (fn [ax] => pair ax)) (tnames ~~ tss); - -fun gen_specify_consts add args thy = - let - val specs = map (fn (c, T, mx) => - Const (Sign.full_name thy (Syntax.const_name c mx), T)) args; - in - thy - |> add args - |> Theory.add_finals_i false specs - end; - -val specify_consts = gen_specify_consts Sign.add_consts_i; -val specify_consts_authentic = gen_specify_consts (fold (snd oo Sign.declare_const [])); - structure DatatypeInterpretation = InterpretationFun(type T = string list val eq = op =); val interpretation = DatatypeInterpretation.interpretation; -fun add_datatype_axm flat_names new_type_names descr sorts types_syntax constr_syntax dt_info - case_names_induct case_names_exhausts thy = - let - val descr' = flat descr; - val recTs = get_rec_types descr' sorts; - val used = map fst (fold Term.add_tfreesT recTs []); - val newTs = Library.take (length (hd descr), recTs); - - (**** declare new types and constants ****) - - val tyvars = map (fn (_, (_, Ts, _)) => map dest_DtTFree Ts) (hd descr); - - val constr_decls = map (fn (((_, (_, _, constrs)), T), constr_syntax') => - map (fn ((_, cargs), (cname, mx)) => - (cname, map (typ_of_dtyp descr' sorts) cargs ---> T, mx)) - (constrs ~~ constr_syntax')) ((hd descr) ~~ newTs ~~ constr_syntax); - - val (rec_result_Ts, reccomb_fn_Ts) = DatatypeProp.make_primrec_Ts descr sorts used; - - val big_reccomb_name = (space_implode "_" new_type_names) ^ "_rec"; - val reccomb_names = if length descr' = 1 then [big_reccomb_name] else - (map ((curry (op ^) (big_reccomb_name ^ "_")) o string_of_int) - (1 upto (length descr'))); - - val freeT = TFree (Name.variant used "'t", HOLogic.typeS); - val case_fn_Ts = map (fn (i, (_, _, constrs)) => - map (fn (_, cargs) => - let val Ts = map (typ_of_dtyp descr' sorts) cargs - in Ts ---> freeT end) constrs) (hd descr); - - val case_names = map (fn s => (s ^ "_case")) new_type_names; - - val thy2' = thy - - (** new types **) - |> fold2 (fn (name, mx) => fn tvs => ObjectLogic.typedecl (name, tvs, mx) #> snd) - types_syntax tyvars - |> add_path flat_names (space_implode "_" new_type_names) - - (** primrec combinators **) - - |> specify_consts (map (fn ((name, T), T') => - (name, reccomb_fn_Ts @ [T] ---> T', NoSyn)) (reccomb_names ~~ recTs ~~ rec_result_Ts)) - - (** case combinators **) - - |> specify_consts_authentic (map (fn ((name, T), Ts) => - (name, Ts @ [T] ---> freeT, NoSyn)) (case_names ~~ newTs ~~ case_fn_Ts)); - - val reccomb_names' = map (Sign.full_name thy2') reccomb_names; - val case_names' = map (Sign.full_name thy2') case_names; - - val thy2 = thy2' - - (** constructors **) - - |> parent_path flat_names - |> fold (fn ((((_, (_, _, constrs)), T), tname), - constr_syntax') => - add_path flat_names tname #> - specify_consts (map (fn ((_, cargs), (cname, mx)) => - (cname, map (typ_of_dtyp descr' sorts) cargs ---> T, mx)) - (constrs ~~ constr_syntax')) #> - parent_path flat_names) - (hd descr ~~ newTs ~~ new_type_names ~~ constr_syntax); - - (**** introduction of axioms ****) - - val rec_axs = DatatypeProp.make_primrecs new_type_names descr sorts thy2; - - val ((([induct], [rec_thms]), inject), thy3) = - thy2 - |> Sign.add_path (space_implode "_" new_type_names) - |> add_axiom "induct" (DatatypeProp.make_ind descr sorts) [case_names_induct] - ||>> add_axioms "recs" rec_axs [] - ||> Sign.parent_path - ||>> add_and_get_axiomss "inject" new_type_names - (DatatypeProp.make_injs descr sorts); - val (distinct, thy4) = add_and_get_axiomss "distinct" new_type_names - (DatatypeProp.make_distincts new_type_names descr sorts thy3) thy3; - - val exhaust_ts = DatatypeProp.make_casedists descr sorts; - val (exhaustion, thy5) = add_and_get_axioms_atts "exhaust" new_type_names - exhaust_ts (map single case_names_exhausts) thy4; - val (case_thms, thy6) = add_and_get_axiomss "cases" new_type_names - (DatatypeProp.make_cases new_type_names descr sorts thy5) thy5; - val (split_ts, split_asm_ts) = ListPair.unzip - (DatatypeProp.make_splits new_type_names descr sorts thy6); - val (split, thy7) = add_and_get_axioms "split" new_type_names split_ts thy6; - val (split_asm, thy8) = add_and_get_axioms "split_asm" new_type_names - split_asm_ts thy7; - val (nchotomys, thy9) = add_and_get_axioms "nchotomy" new_type_names - (DatatypeProp.make_nchotomys descr sorts) thy8; - val (case_congs, thy10) = add_and_get_axioms "case_cong" new_type_names - (DatatypeProp.make_case_congs new_type_names descr sorts thy9) thy9; - val (weak_case_congs, thy11) = add_and_get_axioms "weak_case_cong" new_type_names - (DatatypeProp.make_weak_case_congs new_type_names descr sorts thy10) thy10; - - val dt_infos = map (make_dt_info NONE descr' sorts induct reccomb_names' rec_thms) - ((0 upto length (hd descr) - 1) ~~ (hd descr) ~~ case_names' ~~ case_thms ~~ - exhaustion ~~ replicate (length (hd descr)) QuickAndDirty ~~ inject ~~ - nchotomys ~~ case_congs ~~ weak_case_congs); - - val simps = flat (distinct @ inject @ case_thms) @ rec_thms; - val split_thms = split ~~ split_asm; - - val thy12 = - thy11 - |> add_case_tr' case_names' - |> Sign.add_path (space_implode "_" new_type_names) - |> add_rules simps case_thms rec_thms inject distinct - weak_case_congs Simplifier.cong_add - |> put_dt_infos dt_infos - |> add_cases_induct dt_infos induct - |> Sign.parent_path - |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms) - |> snd - |> DatatypeInterpretation.data (map fst dt_infos); - in - ({distinct = distinct, - inject = inject, - exhaustion = exhaustion, - rec_thms = rec_thms, - case_thms = case_thms, - split_thms = split_thms, - induction = induct, - simps = simps}, thy12) - end; - (******************* definitional introduction of datatypes *******************) @@ -897,7 +720,7 @@ val case_names_induct = mk_case_names_induct descr'; val case_names_exhausts = mk_case_names_exhausts descr' (map #1 new_dts); in - (if (!quick_and_dirty) then add_datatype_axm else add_datatype_def) + add_datatype_def flat_names new_type_names descr sorts types_syntax constr_syntax dt_info case_names_induct case_names_exhausts thy end;