src/HOLCF/Tools/Domain/domain_constructors.ML
changeset 35481 7bb9157507a9
parent 35476 8e5eb497b042
child 35482 d756837b708d
equal deleted inserted replaced
35480:7a1f285cad25 35481:7bb9157507a9
     7 
     7 
     8 signature DOMAIN_CONSTRUCTORS =
     8 signature DOMAIN_CONSTRUCTORS =
     9 sig
     9 sig
    10   val add_domain_constructors :
    10   val add_domain_constructors :
    11       string
    11       string
    12       -> typ * (binding * (bool * binding option * typ) list * mixfix) list
    12       -> (binding * (bool * binding option * typ) list * mixfix) list
    13       -> term * term
    13       -> Domain_Isomorphism.iso_info
    14       -> thm * thm
       
    15       -> thm
    14       -> thm
    16       -> theory
    15       -> theory
    17       -> { con_consts : term list,
    16       -> { con_consts : term list,
    18            con_betas : thm list,
    17            con_betas : thm list,
    19            exhaust : thm,
    18            exhaust : thm,
   911 (******************************* main function ********************************)
   910 (******************************* main function ********************************)
   912 (******************************************************************************)
   911 (******************************************************************************)
   913 
   912 
   914 fun add_domain_constructors
   913 fun add_domain_constructors
   915     (dname : string)
   914     (dname : string)
   916     (lhsT : typ,
   915     (spec : (binding * (bool * binding option * typ) list * mixfix) list)
   917      spec : (binding * (bool * binding option * typ) list * mixfix) list)
   916     (iso_info : Domain_Isomorphism.iso_info)
   918     (rep_const : term, abs_const : term)
       
   919     (rep_iso_thm : thm, abs_iso_thm : thm)
       
   920     (case_def : thm)
   917     (case_def : thm)
   921     (thy : theory) =
   918     (thy : theory) =
   922   let
   919   let
   923 
   920 
   924     (* prove rep/abs strictness rules *)
   921     (* retrieve facts about rep/abs *)
       
   922     val lhsT = #absT iso_info;
       
   923     val {rep_const, abs_const, ...} = iso_info;
       
   924     val abs_iso_thm = #abs_inverse iso_info;
       
   925     val rep_iso_thm = #rep_inverse iso_info;
   925     val iso_locale = @{thm iso.intro} OF [abs_iso_thm, rep_iso_thm];
   926     val iso_locale = @{thm iso.intro} OF [abs_iso_thm, rep_iso_thm];
   926     val rep_strict = iso_locale RS @{thm iso.rep_strict};
   927     val rep_strict = iso_locale RS @{thm iso.rep_strict};
   927     val abs_strict = iso_locale RS @{thm iso.abs_strict};
   928     val abs_strict = iso_locale RS @{thm iso.abs_strict};
   928     val rep_defined_iff = iso_locale RS @{thm iso.rep_defined_iff};
   929     val rep_defined_iff = iso_locale RS @{thm iso.rep_defined_iff};
   929     val abs_defined_iff = iso_locale RS @{thm iso.abs_defined_iff};
   930     val abs_defined_iff = iso_locale RS @{thm iso.abs_defined_iff};