1.1 --- a/src/HOLCF/Tools/Domain/domain_axioms.ML	Sat Feb 27 14:04:46 2010 -0800
     1.2 +++ b/src/HOLCF/Tools/Domain/domain_axioms.ML	Sat Feb 27 15:32:42 2010 -0800
     1.3 @@ -78,15 +78,6 @@
     1.4            (dc_abs oo (copy_of_dtyp map_tab r (dtyp_of_eq eqn)) oo dc_rep))
     1.5        end;
     1.6  
     1.7 -(* -- definitions concerning the discriminators - *)
     1.8 -
     1.9 -    val dis_defs = let
    1.10 -      fun ddef (con,_,_) = (dis_name con ^"_def",%%:(dis_name con) == 
    1.11 -                                              list_ccomb(%%:(dname^"_when"),map 
    1.12 -                                                                              (fn (con',_,args) => (List.foldr /\#
    1.13 -      (if con'=con then TT else FF) args)) cons))
    1.14 -    in map ddef cons end;
    1.15 -
    1.16      val mat_defs =
    1.17        let
    1.18          fun mdef (con, _, _) =
    1.19 @@ -134,7 +125,7 @@
    1.20    in (dnam,
    1.21        (if definitional then [] else [abs_iso_ax, rep_iso_ax, reach_ax]),
    1.22        (if definitional then [when_def] else [when_def, copy_def]) @
    1.23 -      dis_defs @ mat_defs @ pat_defs @
    1.24 +      mat_defs @ pat_defs @
    1.25        [take_def, finite_def])
    1.26    end; (* let (calc_axioms) *)
    1.27  

     2.1 --- a/src/HOLCF/Tools/Domain/domain_constructors.ML	Sat Feb 27 14:04:46 2010 -0800
     2.2 +++ b/src/HOLCF/Tools/Domain/domain_constructors.ML	Sat Feb 27 15:32:42 2010 -0800
     2.3 @@ -25,7 +25,8 @@
     2.4             dist_les : thm list,
     2.5             dist_eqs : thm list,
     2.6             cases : thm list,
     2.7 -           sel_rews : thm list
     2.8 +           sel_rews : thm list,
     2.9 +           dis_rews : thm list
    2.10           } * theory;
    2.11  end;
    2.12  
    2.13 @@ -590,7 +591,8 @@
    2.14      (con_betas : thm list)
    2.15      (casedist : thm)
    2.16      (iso_locale : thm)
    2.17 -    (thy : theory) =
    2.18 +    (thy : theory)
    2.19 +    : ((typ -> term) * thm list) * theory =
    2.20    let
    2.21  
    2.22      (* prove rep/abs rules *)
    2.23 @@ -598,16 +600,17 @@
    2.24      val abs_inverse = iso_locale RS @{thm iso.abs_iso};
    2.25  
    2.26      (* calculate function arguments of case combinator *)
    2.27 -    val resultT = TVar (("'a",0), @{sort pcpo});
    2.28 -    val fTs = map (fn (_, args) => map snd args -->> resultT) spec;
    2.29 +    val resultT = TVar (("'t",0), @{sort pcpo});
    2.30 +    fun fTs T = map (fn (_, args) => map snd args -->> T) spec;
    2.31      val fns = Datatype_Prop.indexify_names (map (K "f") spec);
    2.32 -    val fs = map Free (fns ~~ fTs);
    2.33 -    val caseT = fTs -->> (lhsT ->> resultT);
    2.34 +    val fs = map Free (fns ~~ fTs resultT);
    2.35 +    fun caseT T = fTs T -->> (lhsT ->> T);
    2.36  
    2.37      (* TODO: move definition of case combinator here *)
    2.38      val case_bind = Binding.name (dname ^ "_when");
    2.39 -    val case_const = Const (Sign.full_name thy case_bind, caseT);
    2.40 -    val case_app = list_ccomb (case_const, fs);
    2.41 +    val case_name = Sign.full_name thy case_bind;
    2.42 +    fun case_const T = Const (case_name, caseT T);
    2.43 +    val case_app = list_ccomb (case_const resultT, fs);
    2.44  
    2.45      (* prove beta reduction rule for case combinator *)
    2.46      val case_beta = beta_of_def thy case_def;
    2.47 @@ -645,7 +648,7 @@
    2.48      end
    2.49  
    2.50    in
    2.51 -    (case_strict :: case_apps, thy)
    2.52 +    ((case_const, case_strict :: case_apps), thy)
    2.53    end
    2.54  
    2.55  (******************************************************************************)
    2.56 @@ -791,6 +794,52 @@
    2.57    end
    2.58  
    2.59  (******************************************************************************)
    2.60 +(************ definitions and theorems for discriminator functions ************)
    2.61 +(******************************************************************************)
    2.62 +
    2.63 +fun add_discriminators
    2.64 +    (bindings : binding list)
    2.65 +    (spec : (term * (bool * typ) list) list)
    2.66 +    (case_const : typ -> term)
    2.67 +    (thy : theory) =
    2.68 +  let
    2.69 +
    2.70 +    fun vars_of args =
    2.71 +      let
    2.72 +        val Ts = map snd args;
    2.73 +        val ns = Datatype_Prop.make_tnames Ts;
    2.74 +      in
    2.75 +        map Free (ns ~~ Ts)
    2.76 +      end;
    2.77 +
    2.78 +    (* define discriminator functions *)
    2.79 +    local
    2.80 +      fun dis_fun i (j, (con, args)) =
    2.81 +        let
    2.82 +          val Ts = map snd args;
    2.83 +          val ns = Datatype_Prop.make_tnames Ts;
    2.84 +          val vs = map Free (ns ~~ Ts);
    2.85 +          val tr = if i = j then @{term TT} else @{term FF};
    2.86 +        in
    2.87 +          big_lambdas vs tr
    2.88 +        end;
    2.89 +      fun dis_eqn (i, bind) : binding * term * mixfix =
    2.90 +        let
    2.91 +          val dis_bind = Binding.prefix_name "is_" bind;
    2.92 +          val rhs = list_ccomb (case_const trT, map_index (dis_fun i) spec);
    2.93 +        in
    2.94 +          (dis_bind, rhs, NoSyn)
    2.95 +        end;
    2.96 +    in
    2.97 +      val ((dis_consts, dis_defs), thy) =
    2.98 +          define_consts (map_index dis_eqn bindings) thy
    2.99 +    end;
   2.100 +
   2.101 +  in
   2.102 +    (dis_defs, thy)
   2.103 +  end;
   2.104 +
   2.105 +(******************************************************************************)
   2.106  (******************************* main function ********************************)
   2.107  (******************************************************************************)
   2.108  
   2.109 @@ -823,7 +872,7 @@
   2.110      val {con_consts, con_betas, casedist, ...} = con_result;
   2.111  
   2.112      (* define case combinator *)
   2.113 -    val (cases : thm list, thy) =
   2.114 +    val ((case_const : typ -> term, cases : thm list), thy) =
   2.115        let
   2.116          fun prep_arg (lazy, sel, T) = (lazy, T);
   2.117          fun prep_con c (b, args, mx) = (c, map prep_arg args);
   2.118 @@ -836,14 +885,26 @@
   2.119      (* TODO: enable this earlier *)
   2.120      val thy = Sign.add_path dname thy;
   2.121  
   2.122 -    (* replace bindings with terms in constructor spec *)
   2.123 -    val sel_spec : (term * (bool * binding option * typ) list) list =
   2.124 -      map2 (fn con => fn (b, args, mx) => (con, args)) con_consts spec;
   2.125 -
   2.126      (* define and prove theorems for selector functions *)
   2.127      val (sel_thms : thm list, thy : theory) =
   2.128 -      add_selectors sel_spec rep_const
   2.129 -        abs_iso_thm rep_strict rep_defined_iff con_betas thy;
   2.130 +      let
   2.131 +        val sel_spec : (term * (bool * binding option * typ) list) list =
   2.132 +          map2 (fn con => fn (b, args, mx) => (con, args)) con_consts spec;
   2.133 +      in
   2.134 +        add_selectors sel_spec rep_const
   2.135 +          abs_iso_thm rep_strict rep_defined_iff con_betas thy
   2.136 +      end;
   2.137 +
   2.138 +    (* define and prove theorems for discriminator functions *)
   2.139 +    val (dis_thms : thm list, thy : theory) =
   2.140 +      let
   2.141 +        val bindings = map #1 spec;
   2.142 +        fun prep_arg (lazy, sel, T) = (lazy, T);
   2.143 +        fun prep_con c (b, args, mx) = (c, map prep_arg args);
   2.144 +        val dis_spec = map2 prep_con con_consts spec;
   2.145 +      in
   2.146 +        add_discriminators bindings dis_spec case_const thy
   2.147 +      end
   2.148  
   2.149      (* restore original signature path *)
   2.150      val thy = Sign.parent_path thy;
   2.151 @@ -860,7 +921,8 @@
   2.152          dist_les = #dist_les con_result,
   2.153          dist_eqs = #dist_eqs con_result,
   2.154          cases = cases,
   2.155 -        sel_rews = sel_thms };
   2.156 +        sel_rews = sel_thms,
   2.157 +        dis_rews = dis_thms };
   2.158    in
   2.159      (result, thy)
   2.160    end;

     3.1 --- a/src/HOLCF/Tools/Domain/domain_syntax.ML	Sat Feb 27 14:04:46 2010 -0800
     3.2 +++ b/src/HOLCF/Tools/Domain/domain_syntax.ML	Sat Feb 27 15:32:42 2010 -0800
     3.3 @@ -64,15 +64,10 @@
     3.4            | esc []      = []
     3.5        in implode o esc o Symbol.explode end;
     3.6  
     3.7 -      fun dis_name_ con =
     3.8 -          Binding.name ("is_" ^ strip_esc (Binding.name_of con));
     3.9        fun mat_name_ con =
    3.10            Binding.name ("match_" ^ strip_esc (Binding.name_of con));
    3.11        fun pat_name_ con =
    3.12            Binding.name (strip_esc (Binding.name_of con) ^ "_pat");
    3.13 -      fun dis (con,args,mx) =
    3.14 -          (dis_name_ con, dtype->>trT,
    3.15 -           Mixfix(escape ("is_" ^ Binding.name_of con), [], Syntax.max_pri));
    3.16        (* strictly speaking, these constants have one argument,
    3.17         but the mixfix (without arguments) is introduced only
    3.18             to generate parse rules for non-alphanumeric names*)
    3.19 @@ -95,7 +90,6 @@
    3.20               mk_patT (dtype, mk_ctupleT (map (freetvar "t") (1 upto length args))),
    3.21             Mixfix(escape (Binding.name_of con ^ "_pat"), [], Syntax.max_pri));
    3.22      in
    3.23 -    val consts_dis = map dis cons';
    3.24      val consts_mat = map mat cons';
    3.25      val consts_pat = map pat cons';
    3.26      end;
    3.27 @@ -165,7 +159,7 @@
    3.28          if definitional then [] else [const_rep, const_abs, const_copy];
    3.29  
    3.30    in (optional_consts @ [const_when] @ 
    3.31 -      consts_dis @ consts_mat @ consts_pat @
    3.32 +      consts_mat @ consts_pat @
    3.33        [const_take, const_finite],
    3.34        (case_trans false :: case_trans true :: (abscon_trans false @ abscon_trans true @ Case_trans)))
    3.35    end; (* let *)

     4.1 --- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Sat Feb 27 14:04:46 2010 -0800
     4.2 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Sat Feb 27 15:32:42 2010 -0800
     4.3 @@ -156,7 +156,6 @@
     4.4    val ax_rep_iso  = ga "rep_iso"  dname;
     4.5    val ax_when_def = ga "when_def" dname;
     4.6    fun get_def mk_name (con, _, _) = ga (mk_name con^"_def") dname;
     4.7 -  val axs_dis_def = map (get_def dis_name) cons;
     4.8    val axs_mat_def = map (get_def mat_name) cons;
     4.9    val axs_pat_def = map (get_def pat_name) cons;
    4.10    val ax_copy_def = ga "copy_def" dname;
    4.11 @@ -191,6 +190,7 @@
    4.12  val {sel_rews, ...} = result;
    4.13  val when_rews = #cases result;
    4.14  val when_strict = hd when_rews;
    4.15 +val axs_dis_def = #dis_rews result;
    4.16  
    4.17  (* ----- theorems concerning the isomorphism -------------------------------- *)
    4.18