Eliminated store_clasimp.
authorberghofe
Wed Mar 15 23:38:19 2000 +0100 (2000-03-15)
changeset 84786053a5cd2881
parent 8477 17231d71171a
child 8479 5d327a46dc61
Eliminated store_clasimp.
src/HOL/Tools/datatype_package.ML
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Wed Mar 15 23:36:46 2000 +0100
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Wed Mar 15 23:38:19 2000 +0100
     1.3 @@ -348,9 +348,6 @@
     1.4         nchotomy = nchotomy,
     1.5         case_cong = case_cong});
     1.6  
     1.7 -fun store_clasimp thy (cla, simp) =
     1.8 -  (claset_ref_of thy := cla; simpset_ref_of thy := simp);
     1.9 -
    1.10  
    1.11  (********************* axiomatic introduction of datatypes ********************)
    1.12  
    1.13 @@ -517,15 +514,13 @@
    1.14  
    1.15      val thy11 = thy10 |>
    1.16        Theory.add_path (space_implode "_" new_type_names) |>
    1.17 -      (#1 o PureThy.add_thmss [(("simps", simps), [])]) |>
    1.18 +      (#1 o PureThy.add_thmss [(("simps", simps), []),
    1.19 +        (("", flat case_thms @ size_thms @ rec_thms), [Simplifier.simp_add_global]),
    1.20 +        (("", flat (inject @ distinct)), [iff_add_global])]) |>
    1.21        put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |>
    1.22        add_cases_induct dt_infos |>
    1.23        Theory.parent_path;
    1.24  
    1.25 -    val _ = store_clasimp thy11 ((claset_of thy11, simpset_of thy11)
    1.26 -      addsimps2 flat case_thms addsimps2 size_thms addsimps2 rec_thms
    1.27 -      addIffs flat (inject @ distinct));
    1.28 -
    1.29    in
    1.30      (thy11,
    1.31       {distinct = distinct,
    1.32 @@ -553,7 +548,7 @@
    1.33  
    1.34      val (thy3, casedist_thms) = DatatypeAbsProofs.prove_casedist_thms new_type_names descr
    1.35        sorts induct case_names_exhausts thy2;
    1.36 -    val (thy4, reccomb_names, rec_thms) = DatatypeAbsProofs.prove_primrec_thms
    1.37 +    val (thy4, (reccomb_names, rec_thms)) = DatatypeAbsProofs.prove_primrec_thms
    1.38        flat_names new_type_names descr sorts dt_info inject dist_rewrites dist_ss induct thy3;
    1.39      val (thy6, (case_thms, case_names)) = DatatypeAbsProofs.prove_case_thms
    1.40        flat_names new_type_names descr sorts reccomb_names rec_thms thy4;
    1.41 @@ -574,15 +569,13 @@
    1.42  
    1.43      val thy11 = thy10 |>
    1.44        Theory.add_path (space_implode "_" new_type_names) |>
    1.45 -      (#1 o PureThy.add_thmss [(("simps", simps), [])]) |>
    1.46 +      (#1 o PureThy.add_thmss [(("simps", simps), []),
    1.47 +        (("", flat case_thms @ size_thms @ rec_thms), [Simplifier.simp_add_global]),
    1.48 +        (("", flat (inject @ distinct)), [iff_add_global])]) |>
    1.49        put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |>
    1.50        add_cases_induct dt_infos |>
    1.51        Theory.parent_path;
    1.52  
    1.53 -    val _ = store_clasimp thy11 ((claset_of thy11, simpset_of thy11)
    1.54 -      addsimps2 flat case_thms addsimps2 size_thms addsimps2 rec_thms
    1.55 -      addIffs flat (inject @ distinct));
    1.56 -
    1.57    in
    1.58      (thy11,
    1.59       {distinct = distinct,
    1.60 @@ -650,7 +643,7 @@
    1.61      val (thy2, casedist_thms) = thy1 |>
    1.62        DatatypeAbsProofs.prove_casedist_thms new_type_names [descr] sorts induction
    1.63          case_names_exhausts;
    1.64 -    val (thy3, reccomb_names, rec_thms) = DatatypeAbsProofs.prove_primrec_thms
    1.65 +    val (thy3, (reccomb_names, rec_thms)) = DatatypeAbsProofs.prove_primrec_thms
    1.66        false new_type_names [descr] sorts dt_info inject distinct dist_ss induction thy2;
    1.67      val (thy4, (case_thms, case_names)) = DatatypeAbsProofs.prove_case_thms false
    1.68        new_type_names [descr] sorts reccomb_names rec_thms thy3;
    1.69 @@ -677,15 +670,13 @@
    1.70        (#1 o store_thmss "distinct" new_type_names distinct) |>
    1.71        Theory.add_path (space_implode "_" new_type_names) |>
    1.72        PureThy.add_thms [(("induct", induction), [case_names_induct])] |>>
    1.73 -      (#1 o PureThy.add_thmss [(("simps", simps), [])]) |>>
    1.74 +      (#1 o PureThy.add_thmss [(("simps", simps), []),
    1.75 +        (("", flat case_thms @ size_thms @ rec_thms), [Simplifier.simp_add_global]),
    1.76 +        (("", flat (inject @ distinct)), [iff_add_global])]) |>>
    1.77        put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |>>
    1.78        add_cases_induct dt_infos |>>
    1.79        Theory.parent_path;
    1.80  
    1.81 -    (* FIXME use attributes *)
    1.82 -    val _ = store_clasimp thy9 ((claset_of thy9, simpset_of thy9)
    1.83 -      addsimps2 flat case_thms addsimps2 size_thms addsimps2 rec_thms
    1.84 -      addIffs flat (inject @ distinct));
    1.85    in
    1.86      (thy9,
    1.87       {distinct = distinct,