src/HOL/Tools/datatype_rep_proofs.ML
changeset 8479 5d327a46dc61
parent 8436 8a87fa482baf
child 9315 f793f05024f6
equal deleted inserted replaced
8478:6053a5cd2881 8479:5d327a46dc61
   575       end;
   575       end;
   576 
   576 
   577     val constr_inject = map (fn (ts, thms) => map (prove_constr_inj_thm thms) ts)
   577     val constr_inject = map (fn (ts, thms) => map (prove_constr_inj_thm thms) ts)
   578       ((DatatypeProp.make_injs descr sorts) ~~ constr_rep_thms);
   578       ((DatatypeProp.make_injs descr sorts) ~~ constr_rep_thms);
   579 
   579 
   580     val thy6 = thy5 |> parent_path flat_names |>
   580     val (thy6, (constr_inject', distinct_thms'))= thy5 |> parent_path flat_names |>
   581       (#1 o store_thmss "inject" new_type_names constr_inject) |>
   581       store_thmss "inject" new_type_names constr_inject |>>>
   582       (#1 o store_thmss "distinct" new_type_names distinct_thms);
   582       store_thmss "distinct" new_type_names distinct_thms;
   583 
   583 
   584     (*************************** induction theorem ****************************)
   584     (*************************** induction theorem ****************************)
   585 
   585 
   586     val _ = message "Proving induction rule for datatypes ...";
   586     val _ = message "Proving induction rule for datatypes ...";
   587 
   587 
   639     val (thy7, [dt_induct']) = thy6 |>
   639     val (thy7, [dt_induct']) = thy6 |>
   640       Theory.add_path big_name |>
   640       Theory.add_path big_name |>
   641       PureThy.add_thms [(("induct", dt_induct), [case_names_induct])] |>>
   641       PureThy.add_thms [(("induct", dt_induct), [case_names_induct])] |>>
   642       Theory.parent_path;
   642       Theory.parent_path;
   643 
   643 
   644   in (thy7, constr_inject, distinct_thms, dist_rewrites, simproc_dists, dt_induct')
   644   in (thy7, constr_inject', distinct_thms', dist_rewrites, simproc_dists, dt_induct')
   645   end;
   645   end;
   646 
   646 
   647 end;
   647 end;