src/HOL/Tools/datatype_prop.ML
changeset 8601 8fb3a81b4ccf
parent 8434 5e4bba59bfaa
child 9060 b0dd884b1848
equal deleted inserted replaced
8600:a466c687c726 8601:8fb3a81b4ccf
    30     (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
    30     (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
    31       theory -> (term * term) list
    31       theory -> (term * term) list
    32   val make_case_trrules : string list -> (int * (string * DatatypeAux.dtyp list *
    32   val make_case_trrules : string list -> (int * (string * DatatypeAux.dtyp list *
    33     (string * DatatypeAux.dtyp list) list)) list list -> ast Syntax.trrule list
    33     (string * DatatypeAux.dtyp list) list)) list list -> ast Syntax.trrule list
    34   val make_size : string list -> (int * (string * DatatypeAux.dtyp list *
    34   val make_size : string list -> (int * (string * DatatypeAux.dtyp list *
       
    35     (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
       
    36       theory -> term list
       
    37   val make_weak_case_congs : string list -> (int * (string * DatatypeAux.dtyp list *
    35     (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
    38     (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
    36       theory -> term list
    39       theory -> term list
    37   val make_case_congs : string list -> (int * (string * DatatypeAux.dtyp list *
    40   val make_case_congs : string list -> (int * (string * DatatypeAux.dtyp list *
    38     (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
    41     (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
    39       theory -> term list
    42       theory -> term list
   428       map (make_size_eqn size_const T) constrs) (descr' ~~ size_consts ~~ recTs))
   431       map (make_size_eqn size_const T) constrs) (descr' ~~ size_consts ~~ recTs))
   429   end;
   432   end;
   430 
   433 
   431 (************************* additional rules for TFL ***************************)
   434 (************************* additional rules for TFL ***************************)
   432 
   435 
       
   436 fun make_weak_case_congs new_type_names descr sorts thy =
       
   437   let
       
   438     val case_combs = make_case_combs new_type_names descr sorts thy "f";
       
   439 
       
   440     fun mk_case_cong comb =
       
   441       let 
       
   442         val Type ("fun", [T, _]) = fastype_of comb;
       
   443         val M = Free ("M", T);
       
   444         val M' = Free ("M'", T);
       
   445       in
       
   446         Logic.mk_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (M, M')),
       
   447           HOLogic.mk_Trueprop (HOLogic.mk_eq (comb $ M, comb $ M')))
       
   448       end
       
   449   in
       
   450     map mk_case_cong case_combs
       
   451   end;
       
   452  
       
   453 
   433 (*---------------------------------------------------------------------------
   454 (*---------------------------------------------------------------------------
   434  * Structure of case congruence theorem looks like this:
   455  * Structure of case congruence theorem looks like this:
   435  *
   456  *
   436  *    (M = M') 
   457  *    (M = M') 
   437  *    ==> (!!x1,...,xk. (M' = C1 x1..xk) ==> (f1 x1..xk = g1 x1..xk)) 
   458  *    ==> (!!x1,...,xk. (M' = C1 x1..xk) ==> (f1 x1..xk = g1 x1..xk))