src/HOL/Tools/datatype_abs_proofs.ML
changeset 8601 8fb3a81b4ccf
parent 8477 17231d71171a
child 9315 f793f05024f6
equal deleted inserted replaced
8600:a466c687c726 8601:8fb3a81b4ccf
    36     (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
    36     (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
    37       string list -> thm list -> theory -> theory * thm list
    37       string list -> thm list -> theory -> theory * thm list
    38   val prove_nchotomys : string list -> (int * (string * DatatypeAux.dtyp list *
    38   val prove_nchotomys : string list -> (int * (string * DatatypeAux.dtyp list *
    39     (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
    39     (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
    40       thm list -> theory -> theory * thm list
    40       thm list -> theory -> theory * thm list
       
    41   val prove_weak_case_congs : string list -> (int * (string * DatatypeAux.dtyp list *
       
    42     (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
       
    43       theory -> theory * thm list
    41   val prove_case_congs : string list -> (int * (string * DatatypeAux.dtyp list *
    44   val prove_case_congs : string list -> (int * (string * DatatypeAux.dtyp list *
    42     (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
    45     (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
    43       thm list -> thm list list -> theory -> theory * thm list
    46       thm list -> thm list list -> theory -> theory * thm list
    44 end;
    47 end;
    45 
    48 
   459     thy' |> Theory.add_path big_name |>
   462     thy' |> Theory.add_path big_name |>
   460     PureThy.add_thmss [(("size", size_thms), [])] |>>
   463     PureThy.add_thmss [(("size", size_thms), [])] |>>
   461     Theory.parent_path |> apsnd flat
   464     Theory.parent_path |> apsnd flat
   462   end;
   465   end;
   463 
   466 
       
   467 fun prove_weak_case_congs new_type_names descr sorts thy =
       
   468   let
       
   469     fun prove_weak_case_cong t =
       
   470        prove_goalw_cterm [] (cterm_of (Theory.sign_of thy) t)
       
   471          (fn prems => [rtac ((hd prems) RS arg_cong) 1])
       
   472 
       
   473     val weak_case_congs = map prove_weak_case_cong (DatatypeProp.make_weak_case_congs
       
   474       new_type_names descr sorts thy)
       
   475 
       
   476   in thy |> store_thms "weak_case_cong" new_type_names weak_case_congs end;
   464 
   477 
   465 (************************* additional theorems for TFL ************************)
   478 (************************* additional theorems for TFL ************************)
   466 
   479 
   467 fun prove_nchotomys new_type_names descr sorts casedist_thms thy =
   480 fun prove_nchotomys new_type_names descr sorts casedist_thms thy =
   468   let
   481   let