src/HOL/Tools/datatype_rep_proofs.ML
changeset 5661 6ecb6ea25f19
parent 5553 ae42b36a50c2
child 5696 c2c2214f8037
     1.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Fri Oct 16 18:52:17 1998 +0200
     1.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Fri Oct 16 18:54:55 1998 +0200
     1.3 @@ -14,7 +14,7 @@
     1.4  
     1.5  signature DATATYPE_REP_PROOFS =
     1.6  sig
     1.7 -  val representation_proofs : DatatypeAux.datatype_info Symtab.table ->
     1.8 +  val representation_proofs : bool -> DatatypeAux.datatype_info Symtab.table ->
     1.9      string list -> (int * (string * DatatypeAux.dtyp list *
    1.10        (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
    1.11          (string * mixfix) list -> (string * mixfix) list list -> theory ->
    1.12 @@ -41,7 +41,7 @@
    1.13  
    1.14  (******************************************************************************)
    1.15  
    1.16 -fun representation_proofs (dt_info : datatype_info Symtab.table)
    1.17 +fun representation_proofs flat_names (dt_info : datatype_info Symtab.table)
    1.18        new_type_names descr sorts types_syntax constr_syntax thy =
    1.19    let
    1.20      val Univ_thy = the (get_thy "Univ" thy);
    1.21 @@ -56,13 +56,18 @@
    1.22  
    1.23      val descr' = flat descr;
    1.24  
    1.25 -    val big_rec_name = (space_implode "_" new_type_names) ^ "_rep_set";
    1.26 -    val rep_set_names = map (Sign.full_name (sign_of thy))
    1.27 +    val big_name = space_implode "_" new_type_names;
    1.28 +    val thy1 = add_path flat_names big_name thy;
    1.29 +    val big_rec_name = big_name ^ "_rep_set";
    1.30 +    val rep_set_names = map (Sign.full_name (sign_of thy1))
    1.31        (if length descr' = 1 then [big_rec_name] else
    1.32          (map ((curry (op ^) (big_rec_name ^ "_")) o string_of_int)
    1.33            (1 upto (length descr'))));
    1.34  
    1.35 -    val leafTs = get_nonrec_types descr' sorts;
    1.36 +    val tyvars = map (fn (_, (_, Ts, _)) => map dest_DtTFree Ts) (hd descr);
    1.37 +    val leafTs' = get_nonrec_types descr' sorts;
    1.38 +    val unneeded_vars = hd tyvars \\ foldr add_typ_tfree_names (leafTs', []);
    1.39 +    val leafTs = leafTs' @ (map (fn n => TFree (n, the (assoc (sorts, n)))) unneeded_vars);
    1.40      val recTs = get_rec_types descr' sorts;
    1.41      val newTs = take (length (hd descr), recTs);
    1.42      val oldTs = drop (length (hd descr), recTs);
    1.43 @@ -101,7 +106,7 @@
    1.44  
    1.45      (************** generate introduction rules for representing set **********)
    1.46  
    1.47 -    val _ = writeln "Constructing representing sets...";
    1.48 +    val _ = message "Constructing representing sets...";
    1.49  
    1.50      (* make introduction rule for a single constructor *)
    1.51  
    1.52 @@ -130,18 +135,19 @@
    1.53          ((1 upto (length constrs)) ~~ constrs)) (descr' ~~ rep_set_names));
    1.54  
    1.55      val (thy2, {raw_induct = rep_induct, intrs = rep_intrs, ...}) =
    1.56 -      InductivePackage.add_inductive_i false true big_rec_name false true false
    1.57 -        consts intr_ts [] [] thy;
    1.58 +      setmp InductivePackage.quiet_mode (!quiet_mode)
    1.59 +        (InductivePackage.add_inductive_i false true big_rec_name false true false
    1.60 +           consts intr_ts [] []) thy1;
    1.61  
    1.62      (********************************* typedef ********************************)
    1.63  
    1.64 -    val tyvars = map (fn (_, (_, Ts, _)) => map dest_DtTFree Ts) (hd descr);
    1.65 +    (* FIXME: quiet_mode flag for TypedefPackage and BREADTH_FIRST *)
    1.66  
    1.67 -    val thy3 = foldl (fn (thy, ((((name, mx), tvs), c), name')) =>
    1.68 +    val thy3 = add_path flat_names big_name (foldl (fn (thy, ((((name, mx), tvs), c), name')) =>
    1.69        TypedefPackage.add_typedef_i_no_def name' (name, tvs, mx) c [] []
    1.70          (Some (BREADTH_FIRST (has_fewer_prems 1) (resolve_tac rep_intrs 1))) thy)
    1.71 -          (thy2, types_syntax ~~ tyvars ~~ (take (length newTs, consts)) ~~
    1.72 -            new_type_names);
    1.73 +          (parent_path flat_names thy2, types_syntax ~~ tyvars ~~ (take (length newTs, consts)) ~~
    1.74 +            new_type_names));
    1.75  
    1.76      (*********************** definition of constructors ***********************)
    1.77  
    1.78 @@ -149,7 +155,8 @@
    1.79      val rep_names = map (curry op ^ "Rep_") new_type_names;
    1.80      val rep_names' = map (fn i => big_rep_name ^ (string_of_int i))
    1.81        (1 upto (length (flat (tl descr))));
    1.82 -    val all_rep_names = map (Sign.full_name (sign_of thy3)) (rep_names @ rep_names');
    1.83 +    val all_rep_names = map (Sign.intern_const (sign_of thy3)) rep_names @
    1.84 +      map (Sign.full_name (sign_of thy3)) rep_names';
    1.85  
    1.86      (* isomorphism declarations *)
    1.87  
    1.88 @@ -198,20 +205,19 @@
    1.89          val cong' = cterm_instantiate [(cterm_of sg cong_f, rep_const)] arg_cong;
    1.90          val dist = cterm_instantiate [(cterm_of sg distinct_f, rep_const)] distinct_lemma;
    1.91          val (thy', defs', eqns', _) = foldl ((make_constr_def tname T) (length constrs))
    1.92 -          ((if length newTs = 1 then thy else Theory.add_path tname thy, defs, [], 1),
    1.93 -            constrs ~~ constr_syntax)
    1.94 +          ((add_path flat_names tname thy, defs, [], 1), constrs ~~ constr_syntax)
    1.95        in
    1.96 -        (if length newTs = 1 then thy' else Theory.parent_path thy', defs', eqns @ [eqns'],
    1.97 +        (parent_path flat_names thy', defs', eqns @ [eqns'],
    1.98            rep_congs @ [cong'], dist_lemmas @ [dist])
    1.99        end;
   1.100  
   1.101      val (thy4, constr_defs, constr_rep_eqns, rep_congs, dist_lemmas) = foldl dt_constr_defs
   1.102 -      ((Theory.add_consts_i iso_decls thy3, [], [], [], []),
   1.103 +      ((thy3 |> Theory.add_consts_i iso_decls |> parent_path flat_names, [], [], [], []),
   1.104          hd descr ~~ new_type_names ~~ newTs ~~ constr_syntax);
   1.105  
   1.106      (*********** isomorphisms for new types (introduced by typedef) ***********)
   1.107  
   1.108 -    val _ = writeln "Proving isomorphism properties...";
   1.109 +    val _ = message "Proving isomorphism properties...";
   1.110  
   1.111      (* get axioms from theory *)
   1.112  
   1.113 @@ -323,7 +329,8 @@
   1.114  
   1.115        in (thy', char_thms' @ char_thms) end;
   1.116  
   1.117 -    val (thy5, iso_char_thms) = foldr make_iso_defs (tl descr, (thy4, []));
   1.118 +    val (thy5, iso_char_thms) = foldr make_iso_defs
   1.119 +      (tl descr, (add_path flat_names big_name thy4, []));
   1.120  
   1.121      (* prove isomorphism properties *)
   1.122  
   1.123 @@ -423,7 +430,7 @@
   1.124  
   1.125      (******************* freeness theorems for constructors *******************)
   1.126  
   1.127 -    val _ = writeln "Proving freeness of constructors...";
   1.128 +    val _ = message "Proving freeness of constructors...";
   1.129  
   1.130      (* prove theorem  Rep_i (Constr_j ...) = Inj_j ...  *)
   1.131      
   1.132 @@ -470,11 +477,12 @@
   1.133      val constr_inject = map (fn (ts, thms) => map (prove_constr_inj_thm thms) ts)
   1.134        ((DatatypeProp.make_injs descr sorts) ~~ constr_rep_thms);
   1.135  
   1.136 -    val thy6 = store_thmss "inject" new_type_names constr_inject thy5;
   1.137 +    val thy6 = store_thmss "inject" new_type_names
   1.138 +      constr_inject (parent_path flat_names thy5);
   1.139  
   1.140      (*************************** induction theorem ****************************)
   1.141  
   1.142 -    val _ = writeln "Proving induction rule for datatypes...";
   1.143 +    val _ = message "Proving induction rule for datatypes...";
   1.144  
   1.145      val Rep_inverse_thms = (map (fn (_, iso, _) => iso RS subst) newT_iso_axms) @
   1.146        (map (fn r => r RS inv_f_f RS subst) (drop (length newTs, iso_inj_thms)));
   1.147 @@ -526,7 +534,10 @@
   1.148              DEPTH_SOLVE_1 (ares_tac [prem] 1)]))
   1.149                (prems ~~ (constr_defs @ (map mk_meta_eq iso_char_thms))))]);
   1.150  
   1.151 -    val thy7 = PureThy.add_tthms [(("induct", Attribute.tthm_of dt_induct), [])] thy6;
   1.152 +    val thy7 = thy6 |>
   1.153 +      Theory.add_path big_name |>
   1.154 +      PureThy.add_tthms [(("induct", Attribute.tthm_of dt_induct), [])] |>
   1.155 +      Theory.parent_path;
   1.156  
   1.157    in (thy7, constr_inject, dist_rewrites, dt_induct)
   1.158    end;