src/HOLCF/Tools/Domain/domain_theorems.ML
changeset 35481 7bb9157507a9
parent 35468 09bc6a2e2296
child 35482 d756837b708d
equal deleted inserted replaced
35480:7a1f285cad25 35481:7bb9157507a9
   140 
   140 
   141 val rep_const = Const(dname^"_rep", lhsT ->> rhsT);
   141 val rep_const = Const(dname^"_rep", lhsT ->> rhsT);
   142 
   142 
   143 val abs_const = Const(dname^"_abs", rhsT ->> lhsT);
   143 val abs_const = Const(dname^"_abs", rhsT ->> lhsT);
   144 
   144 
       
   145 val iso_info : Domain_Isomorphism.iso_info =
       
   146   {
       
   147     absT = lhsT,
       
   148     repT = rhsT,
       
   149     abs_const = abs_const,
       
   150     rep_const = rep_const,
       
   151     abs_inverse = ax_abs_iso,
       
   152     rep_inverse = ax_rep_iso
       
   153   };
       
   154 
   145 val (result, thy) =
   155 val (result, thy) =
   146   Domain_Constructors.add_domain_constructors
   156   Domain_Constructors.add_domain_constructors
   147     (Long_Name.base_name dname) dom_eqn
   157     (Long_Name.base_name dname) (snd dom_eqn) iso_info ax_when_def thy;
   148     (rep_const, abs_const) (ax_rep_iso, ax_abs_iso) ax_when_def thy;
       
   149 
   158 
   150 val con_appls = #con_betas result;
   159 val con_appls = #con_betas result;
   151 val {exhaust, casedist, ...} = result;
   160 val {exhaust, casedist, ...} = result;
   152 val {con_compacts, con_rews, inverts, injects, dist_les, dist_eqs, ...} = result;
   161 val {con_compacts, con_rews, inverts, injects, dist_les, dist_eqs, ...} = result;
   153 val {sel_rews, ...} = result;
   162 val {sel_rews, ...} = result;