add_domain_constructors takes iso_info record as argument
authorhuffman
Sun Feb 28 20:56:28 2010 -0800 (2010-02-28)
changeset 354817bb9157507a9
parent 35480 7a1f285cad25
child 35482 d756837b708d
add_domain_constructors takes iso_info record as argument
src/HOLCF/Tools/Domain/domain_constructors.ML
src/HOLCF/Tools/Domain/domain_theorems.ML
     1.1 --- a/src/HOLCF/Tools/Domain/domain_constructors.ML	Sun Feb 28 19:39:50 2010 -0800
     1.2 +++ b/src/HOLCF/Tools/Domain/domain_constructors.ML	Sun Feb 28 20:56:28 2010 -0800
     1.3 @@ -9,9 +9,8 @@
     1.4  sig
     1.5    val add_domain_constructors :
     1.6        string
     1.7 -      -> typ * (binding * (bool * binding option * typ) list * mixfix) list
     1.8 -      -> term * term
     1.9 -      -> thm * thm
    1.10 +      -> (binding * (bool * binding option * typ) list * mixfix) list
    1.11 +      -> Domain_Isomorphism.iso_info
    1.12        -> thm
    1.13        -> theory
    1.14        -> { con_consts : term list,
    1.15 @@ -913,15 +912,17 @@
    1.16  
    1.17  fun add_domain_constructors
    1.18      (dname : string)
    1.19 -    (lhsT : typ,
    1.20 -     spec : (binding * (bool * binding option * typ) list * mixfix) list)
    1.21 -    (rep_const : term, abs_const : term)
    1.22 -    (rep_iso_thm : thm, abs_iso_thm : thm)
    1.23 +    (spec : (binding * (bool * binding option * typ) list * mixfix) list)
    1.24 +    (iso_info : Domain_Isomorphism.iso_info)
    1.25      (case_def : thm)
    1.26      (thy : theory) =
    1.27    let
    1.28  
    1.29 -    (* prove rep/abs strictness rules *)
    1.30 +    (* retrieve facts about rep/abs *)
    1.31 +    val lhsT = #absT iso_info;
    1.32 +    val {rep_const, abs_const, ...} = iso_info;
    1.33 +    val abs_iso_thm = #abs_inverse iso_info;
    1.34 +    val rep_iso_thm = #rep_inverse iso_info;
    1.35      val iso_locale = @{thm iso.intro} OF [abs_iso_thm, rep_iso_thm];
    1.36      val rep_strict = iso_locale RS @{thm iso.rep_strict};
    1.37      val abs_strict = iso_locale RS @{thm iso.abs_strict};
     2.1 --- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Sun Feb 28 19:39:50 2010 -0800
     2.2 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Sun Feb 28 20:56:28 2010 -0800
     2.3 @@ -142,10 +142,19 @@
     2.4  
     2.5  val abs_const = Const(dname^"_abs", rhsT ->> lhsT);
     2.6  
     2.7 +val iso_info : Domain_Isomorphism.iso_info =
     2.8 +  {
     2.9 +    absT = lhsT,
    2.10 +    repT = rhsT,
    2.11 +    abs_const = abs_const,
    2.12 +    rep_const = rep_const,
    2.13 +    abs_inverse = ax_abs_iso,
    2.14 +    rep_inverse = ax_rep_iso
    2.15 +  };
    2.16 +
    2.17  val (result, thy) =
    2.18    Domain_Constructors.add_domain_constructors
    2.19 -    (Long_Name.base_name dname) dom_eqn
    2.20 -    (rep_const, abs_const) (ax_rep_iso, ax_abs_iso) ax_when_def thy;
    2.21 +    (Long_Name.base_name dname) (snd dom_eqn) iso_info ax_when_def thy;
    2.22  
    2.23  val con_appls = #con_betas result;
    2.24  val {exhaust, casedist, ...} = result;