src/HOL/Tools/datatype_rep_proofs.ML
changeset 8436 8a87fa482baf
parent 8305 93aa21ec5494
child 8479 5d327a46dc61
equal deleted inserted replaced
8435:51a040fd2200 8436:8a87fa482baf
    15 signature DATATYPE_REP_PROOFS =
    15 signature DATATYPE_REP_PROOFS =
    16 sig
    16 sig
    17   val representation_proofs : bool -> DatatypeAux.datatype_info Symtab.table ->
    17   val representation_proofs : bool -> DatatypeAux.datatype_info Symtab.table ->
    18     string list -> (int * (string * DatatypeAux.dtyp list *
    18     string list -> (int * (string * DatatypeAux.dtyp list *
    19       (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
    19       (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
    20         (string * mixfix) list -> (string * mixfix) list list -> theory ->
    20         (string * mixfix) list -> (string * mixfix) list list -> theory attribute
    21           theory * thm list list * thm list list * thm list list *
    21           -> theory -> theory * thm list list * thm list list * thm list list *
    22             DatatypeAux.simproc_dist list * thm
    22             DatatypeAux.simproc_dist list * thm
    23 end;
    23 end;
    24 
    24 
    25 structure DatatypeRepProofs : DATATYPE_REP_PROOFS =
    25 structure DatatypeRepProofs : DATATYPE_REP_PROOFS =
    26 struct
    26 struct
    40   #exhaustion (the (Symtab.lookup (dt_info, tname)));
    40   #exhaustion (the (Symtab.lookup (dt_info, tname)));
    41 
    41 
    42 (******************************************************************************)
    42 (******************************************************************************)
    43 
    43 
    44 fun representation_proofs flat_names (dt_info : datatype_info Symtab.table)
    44 fun representation_proofs flat_names (dt_info : datatype_info Symtab.table)
    45       new_type_names descr sorts types_syntax constr_syntax thy =
    45       new_type_names descr sorts types_syntax constr_syntax case_names_induct thy =
    46   let
    46   let
    47     val Datatype_thy = theory "Datatype";
    47     val Datatype_thy = theory "Datatype";
    48     val node_name = Sign.intern_tycon (Theory.sign_of Datatype_thy) "node";
    48     val node_name = Sign.intern_tycon (Theory.sign_of Datatype_thy) "node";
    49     val [In0_name, In1_name, Scons_name, Leaf_name, Numb_name, Lim_name,
    49     val [In0_name, In1_name, Scons_name, Leaf_name, Numb_name, Lim_name,
    50       Funs_name, o_name, sum_case_name] =
    50       Funs_name, o_name, sum_case_name] =
   229         val rhs = mk_univ_inj r_args n i;
   229         val rhs = mk_univ_inj r_args n i;
   230         val def = equals T $ lhs $ (Const (abs_name, Univ_elT --> T) $ rhs);
   230         val def = equals T $ lhs $ (Const (abs_name, Univ_elT --> T) $ rhs);
   231         val def_name = (Sign.base_name cname) ^ "_def";
   231         val def_name = (Sign.base_name cname) ^ "_def";
   232         val eqn = HOLogic.mk_Trueprop (HOLogic.mk_eq
   232         val eqn = HOLogic.mk_Trueprop (HOLogic.mk_eq
   233           (Const (rep_name, T --> Univ_elT) $ lhs, rhs));
   233           (Const (rep_name, T --> Univ_elT) $ lhs, rhs));
   234         val thy' = thy |>
   234         val (thy', [def_thm]) = thy |>
   235           Theory.add_consts_i [(cname', constrT, mx)] |>
   235           Theory.add_consts_i [(cname', constrT, mx)] |>
   236           (PureThy.add_defs_i o map Thm.no_attributes) [(def_name, def)];
   236           (PureThy.add_defs_i o map Thm.no_attributes) [(def_name, def)];
   237 
   237 
   238       in (thy', defs @ [get_thm thy' def_name], eqns @ [eqn], i + 1)
   238       in (thy', defs @ [def_thm], eqns @ [eqn], i + 1) end;
   239       end;
       
   240 
   239 
   241     (* constructor definitions for datatype *)
   240     (* constructor definitions for datatype *)
   242 
   241 
   243     fun dt_constr_defs ((thy, defs, eqns, rep_congs, dist_lemmas),
   242     fun dt_constr_defs ((thy, defs, eqns, rep_congs, dist_lemmas),
   244         ((((_, (_, _, constrs)), tname), T), constr_syntax)) =
   243         ((((_, (_, _, constrs)), tname), T), constr_syntax)) =
   380         val (fs, eqns, isos) = foldl process_dt (([], [], []), ds);
   379         val (fs, eqns, isos) = foldl process_dt (([], [], []), ds);
   381         val fTs = map fastype_of fs;
   380         val fTs = map fastype_of fs;
   382         val defs = map (fn (rec_name, (T, iso_name)) => ((Sign.base_name iso_name) ^ "_def",
   381         val defs = map (fn (rec_name, (T, iso_name)) => ((Sign.base_name iso_name) ^ "_def",
   383           equals (T --> Univ_elT) $ Const (iso_name, T --> Univ_elT) $
   382           equals (T --> Univ_elT) $ Const (iso_name, T --> Univ_elT) $
   384             list_comb (Const (rec_name, fTs @ [T] ---> Univ_elT), fs))) (rec_names ~~ isos);
   383             list_comb (Const (rec_name, fTs @ [T] ---> Univ_elT), fs))) (rec_names ~~ isos);
   385         val thy' = (PureThy.add_defs_i o map Thm.no_attributes) defs thy;
   384         val (thy', def_thms) = (PureThy.add_defs_i o map Thm.no_attributes) defs thy;
   386         val def_thms = map (get_thm thy') (map fst defs);
       
   387 
   385 
   388         (* prove characteristic equations *)
   386         (* prove characteristic equations *)
   389 
   387 
   390         val rewrites = def_thms @ (map mk_meta_eq rec_rewrites);
   388         val rewrites = def_thms @ (map mk_meta_eq rec_rewrites);
   391         val char_thms' = map (fn eqn => prove_goalw_cterm rewrites
   389         val char_thms' = map (fn eqn => prove_goalw_cterm rewrites
   578 
   576 
   579     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)
   580       ((DatatypeProp.make_injs descr sorts) ~~ constr_rep_thms);
   578       ((DatatypeProp.make_injs descr sorts) ~~ constr_rep_thms);
   581 
   579 
   582     val thy6 = thy5 |> parent_path flat_names |>
   580     val thy6 = thy5 |> parent_path flat_names |>
   583       store_thmss "inject" new_type_names constr_inject |>
   581       (#1 o store_thmss "inject" new_type_names constr_inject) |>
   584       store_thmss "distinct" new_type_names distinct_thms;
   582       (#1 o store_thmss "distinct" new_type_names distinct_thms);
   585 
   583 
   586     (*************************** induction theorem ****************************)
   584     (*************************** induction theorem ****************************)
   587 
   585 
   588     val _ = message "Proving induction rule for datatypes ...";
   586     val _ = message "Proving induction rule for datatypes ...";
   589 
   587 
   636             simp_tac (HOL_basic_ss addsimps ((symmetric r)::Rep_inverse_thms')) 1,
   634             simp_tac (HOL_basic_ss addsimps ((symmetric r)::Rep_inverse_thms')) 1,
   637             DEPTH_SOLVE_1 (ares_tac [prem] 1 ORELSE (EVERY [rewtac o_def,
   635             DEPTH_SOLVE_1 (ares_tac [prem] 1 ORELSE (EVERY [rewtac o_def,
   638               rtac allI 1, dtac FunsD 1, etac CollectD 1]))]))
   636               rtac allI 1, dtac FunsD 1, etac CollectD 1]))]))
   639                 (prems ~~ (constr_defs @ (map mk_meta_eq iso_char_thms))))]);
   637                 (prems ~~ (constr_defs @ (map mk_meta_eq iso_char_thms))))]);
   640 
   638 
   641     val thy7 = thy6 |>
   639     val (thy7, [dt_induct']) = thy6 |>
   642       Theory.add_path big_name |>
   640       Theory.add_path big_name |>
   643       PureThy.add_thms [(("induct", dt_induct), [])] |>
   641       PureThy.add_thms [(("induct", dt_induct), [case_names_induct])] |>>
   644       Theory.parent_path;
   642       Theory.parent_path;
   645 
   643 
   646   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')
   647   end;
   645   end;
   648 
   646 
   649 end;
   647 end;