src/HOL/Tools/Datatype/datatype.ML
changeset 32915 a7a97960054b
parent 32911 5f7386f7cbe6
child 32922 8e40cd05de7a
equal deleted inserted replaced
32912:9fd51a25bd3a 32915:a7a97960054b
   332     val thy2 = thy1 |> Theory.checkpoint;
   332     val thy2 = thy1 |> Theory.checkpoint;
   333     val flat_descr = flat descr;
   333     val flat_descr = flat descr;
   334     val new_type_names = map Long_Name.base_name (the_default dt_names alt_names);
   334     val new_type_names = map Long_Name.base_name (the_default dt_names alt_names);
   335     val _ = message config ("Deriving properties for datatype(s) " ^ commas_quote new_type_names);
   335     val _ = message config ("Deriving properties for datatype(s) " ^ commas_quote new_type_names);
   336 
   336 
   337     val other_distincts = all_distincts thy2 (get_rec_types flat_descr sorts);
       
   338 
       
   339     val (exhaust, thy3) = DatatypeAbsProofs.prove_casedist_thms config new_type_names
   337     val (exhaust, thy3) = DatatypeAbsProofs.prove_casedist_thms config new_type_names
   340       descr sorts induct (mk_case_names_exhausts flat_descr dt_names) thy2;
   338       descr sorts induct (mk_case_names_exhausts flat_descr dt_names) thy2;
   341     val (nchotomys, thy4) = DatatypeAbsProofs.prove_nchotomys config new_type_names
   339     val (nchotomys, thy4) = DatatypeAbsProofs.prove_nchotomys config new_type_names
   342       descr sorts exhaust thy3;
   340       descr sorts exhaust thy3;
   343     val ((rec_names, rec_rewrites), thy5) = DatatypeAbsProofs.prove_primrec_thms
   341     val ((rec_names, rec_rewrites), thy5) = DatatypeAbsProofs.prove_primrec_thms
   344       config new_type_names descr sorts (#inject o the o Symtab.lookup (get_all thy4))
   342       config new_type_names descr sorts (#inject o the o Symtab.lookup (get_all thy4))
   345       inject distinct (Simplifier.theory_context thy4 (HOL_basic_ss addsimps (flat other_distincts)))
   343       inject (distinct, all_distincts thy2 (get_rec_types flat_descr sorts))
   346       induct thy4;
   344       induct thy4;
   347     val ((case_rewrites, case_names), thy6) = DatatypeAbsProofs.prove_case_thms
   345     val ((case_rewrites, case_names), thy6) = DatatypeAbsProofs.prove_case_thms
   348       config new_type_names descr sorts rec_names rec_rewrites thy5;
   346       config new_type_names descr sorts rec_names rec_rewrites thy5;
   349     val (case_congs, thy7) = DatatypeAbsProofs.prove_case_congs new_type_names
   347     val (case_congs, thy7) = DatatypeAbsProofs.prove_case_congs new_type_names
   350       descr sorts nchotomys case_rewrites thy6;
   348       descr sorts nchotomys case_rewrites thy6;