src/HOLCF/Tools/Domain/domain_axioms.ML
changeset 35486 c91854705b1d
parent 35468 09bc6a2e2296
child 35494 45c9a8278faf
equal deleted inserted replaced
35485:7d7495f5e35e 35486:c91854705b1d
    65     val dnam = Long_Name.base_name dname;
    65     val dnam = Long_Name.base_name dname;
    66 
    66 
    67     val abs_iso_ax = ("abs_iso", mk_trp(dc_rep`(dc_abs`%x_name') === %:x_name'));
    67     val abs_iso_ax = ("abs_iso", mk_trp(dc_rep`(dc_abs`%x_name') === %:x_name'));
    68     val rep_iso_ax = ("rep_iso", mk_trp(dc_abs`(dc_rep`%x_name') === %:x_name'));
    68     val rep_iso_ax = ("rep_iso", mk_trp(dc_abs`(dc_rep`%x_name') === %:x_name'));
    69 
    69 
    70     val when_def = ("when_def",%%:(dname^"_when") == 
       
    71         List.foldr (uncurry /\ ) (/\x_name'((when_body cons (fn (x,y) =>
       
    72           Bound(1+length cons+x-y)))`(dc_rep`Bound 0))) (when_funs cons));
       
    73 
       
    74     val copy_def =
    70     val copy_def =
    75       let fun r i = proj (Bound 0) eqs i;
    71       let fun r i = proj (Bound 0) eqs i;
    76       in
    72       in
    77         ("copy_def", %%:(dname^"_copy") == /\ "f"
    73         ("copy_def", %%:(dname^"_copy") == /\ "f"
    78           (dc_abs oo (copy_of_dtyp map_tab r (dtyp_of_eq eqn)) oo dc_rep))
    74           (dc_abs oo (copy_of_dtyp map_tab r (dtyp_of_eq eqn)) oo dc_rep))
    93             mk_lam(x_name,
    89             mk_lam(x_name,
    94                    mk_ex("n",(%%:(dname^"_take") $ Bound 0)`Bound 1 === Bound 1)));
    90                    mk_ex("n",(%%:(dname^"_take") $ Bound 0)`Bound 1 === Bound 1)));
    95 
    91 
    96   in (dnam,
    92   in (dnam,
    97       (if definitional then [] else [abs_iso_ax, rep_iso_ax, reach_ax]),
    93       (if definitional then [] else [abs_iso_ax, rep_iso_ax, reach_ax]),
    98       (if definitional then [when_def] else [when_def, copy_def]) @
    94       (if definitional then [] else [copy_def]) @
    99       [take_def, finite_def])
    95       [take_def, finite_def])
   100   end; (* let (calc_axioms) *)
    96   end; (* let (calc_axioms) *)
   101 
    97 
   102 
    98 
   103 (* legacy type inference *)
    99 (* legacy type inference *)