rewrite domain package code for selector functions
authorhuffman
Thu Feb 25 13:16:28 2010 -0800 (2010-02-25)
changeset 35446b719dad322fa
parent 35445 593c184977a4
child 35447 82af95d998e0
rewrite domain package code for selector functions
src/HOLCF/Domain.thy
src/HOLCF/Tools/Domain/domain_axioms.ML
src/HOLCF/Tools/Domain/domain_constructors.ML
src/HOLCF/Tools/Domain/domain_syntax.ML
src/HOLCF/Tools/Domain/domain_theorems.ML
     1.1 --- a/src/HOLCF/Domain.thy	Wed Feb 24 17:37:59 2010 -0800
     1.2 +++ b/src/HOLCF/Domain.thy	Thu Feb 25 13:16:28 2010 -0800
     1.3 @@ -229,6 +229,24 @@
     1.4  lemmas con_eq_iff_rules =
     1.5    sinl_eq sinr_eq sinl_eq_sinr sinr_eq_sinl con_defined_iff_rules
     1.6  
     1.7 +lemmas sel_strict_rules =
     1.8 +  cfcomp2 sscase1 sfst_strict ssnd_strict fup1
     1.9 +
    1.10 +lemma sel_app_extra_rules:
    1.11 +  "sscase\<cdot>ID\<cdot>\<bottom>\<cdot>(sinr\<cdot>x) = \<bottom>"
    1.12 +  "sscase\<cdot>ID\<cdot>\<bottom>\<cdot>(sinl\<cdot>x) = x"
    1.13 +  "sscase\<cdot>\<bottom>\<cdot>ID\<cdot>(sinl\<cdot>x) = \<bottom>"
    1.14 +  "sscase\<cdot>\<bottom>\<cdot>ID\<cdot>(sinr\<cdot>x) = x"
    1.15 +  "fup\<cdot>ID\<cdot>(up\<cdot>x) = x"
    1.16 +by (cases "x = \<bottom>", simp, simp)+
    1.17 +
    1.18 +lemmas sel_app_rules =
    1.19 +  sel_strict_rules sel_app_extra_rules
    1.20 +  ssnd_spair sfst_spair up_defined spair_defined
    1.21 +
    1.22 +lemmas sel_defined_iff_rules =
    1.23 +  cfcomp2 sfst_defined_iff ssnd_defined_iff
    1.24 +
    1.25  use "Tools/cont_consts.ML"
    1.26  use "Tools/cont_proc.ML"
    1.27  use "Tools/Domain/domain_constructors.ML"
     2.1 --- a/src/HOLCF/Tools/Domain/domain_axioms.ML	Wed Feb 24 17:37:59 2010 -0800
     2.2 +++ b/src/HOLCF/Tools/Domain/domain_axioms.ML	Thu Feb 25 13:16:28 2010 -0800
     2.3 @@ -78,7 +78,7 @@
     2.4            (dc_abs oo (copy_of_dtyp map_tab r (dtyp_of_eq eqn)) oo dc_rep))
     2.5        end;
     2.6  
     2.7 -(* -- definitions concerning the discriminators and selectors - *)
     2.8 +(* -- definitions concerning the discriminators - *)
     2.9  
    2.10      val dis_defs = let
    2.11        fun ddef (con,_,_) = (dis_name con ^"_def",%%:(dis_name con) == 
    2.12 @@ -115,13 +115,6 @@
    2.13            end
    2.14        in map pdef cons end;
    2.15  
    2.16 -    val sel_defs = let
    2.17 -      fun sdef con n arg = Option.map (fn sel => (sel^"_def",%%:sel == 
    2.18 -                                                            list_ccomb(%%:(dname^"_when"),map 
    2.19 -                                                                                            (fn (con', _, args) => if con'<>con then UU else
    2.20 -                                                                                                               List.foldr /\# (Bound (length args - n)) args) cons))) (sel_of arg);
    2.21 -    in map_filter I (maps (fn (con, _, args) => mapn (sdef con) 1 args) cons) end;
    2.22 -
    2.23  
    2.24  (* ----- axiom and definitions concerning induction ------------------------- *)
    2.25  
    2.26 @@ -141,7 +134,7 @@
    2.27    in (dnam,
    2.28        (if definitional then [] else [abs_iso_ax, rep_iso_ax, reach_ax]),
    2.29        (if definitional then [when_def] else [when_def, copy_def]) @
    2.30 -      dis_defs @ mat_defs @ pat_defs @ sel_defs @
    2.31 +      dis_defs @ mat_defs @ pat_defs @
    2.32        [take_def, finite_def])
    2.33    end; (* let (calc_axioms) *)
    2.34  
     3.1 --- a/src/HOLCF/Tools/Domain/domain_constructors.ML	Wed Feb 24 17:37:59 2010 -0800
     3.2 +++ b/src/HOLCF/Tools/Domain/domain_constructors.ML	Thu Feb 25 13:16:28 2010 -0800
     3.3 @@ -14,7 +14,8 @@
     3.4        -> thm * thm
     3.5        -> theory
     3.6        -> { con_consts : term list,
     3.7 -           con_defs : thm list }
     3.8 +           con_defs : thm list,
     3.9 +           sel_rews : thm list }
    3.10           * theory;
    3.11  end;
    3.12  
    3.13 @@ -33,6 +34,7 @@
    3.14  fun mk_cfunT (T, U) = Type(@{type_name "->"}, [T, U]);
    3.15  
    3.16  infixr 6 ->>; val (op ->>) = mk_cfunT;
    3.17 +infix -->>; val (op -->>) = Library.foldr mk_cfunT;
    3.18  
    3.19  fun dest_cfunT (Type(@{type_name "->"}, [T, U])) = (T, U)
    3.20    | dest_cfunT T = raise TYPE ("dest_cfunT", [T], []);
    3.21 @@ -64,6 +66,25 @@
    3.22  
    3.23  infix 9 ` ; val (op `) = mk_capply;
    3.24  
    3.25 +val list_ccomb : term * term list -> term = Library.foldl mk_capply;
    3.26 +
    3.27 +fun mk_ID T = Const (@{const_name ID}, T ->> T);
    3.28 +
    3.29 +fun cfcomp_const (T, U, V) =
    3.30 +  Const (@{const_name cfcomp}, (U ->> V) ->> (T ->> U) ->> (T ->> V));
    3.31 +
    3.32 +fun mk_cfcomp (f, g) =
    3.33 +  let
    3.34 +    val (U, V) = dest_cfunT (Term.fastype_of f);
    3.35 +    val (T, U') = dest_cfunT (Term.fastype_of g);
    3.36 +  in
    3.37 +    if U = U'
    3.38 +    then mk_capply (mk_capply (cfcomp_const (T, U, V), f), g)
    3.39 +    else raise TYPE ("mk_cfcomp", [U, U'], [f, g])
    3.40 +  end;
    3.41 +
    3.42 +fun mk_bottom T = Const (@{const_name UU}, T);
    3.43 +
    3.44  
    3.45  (*** Product type ***)
    3.46  
    3.47 @@ -87,10 +108,18 @@
    3.48  
    3.49  fun mk_upT T = Type(@{type_name "u"}, [T]);
    3.50  
    3.51 +fun dest_upT (Type(@{type_name "u"}, [T])) = T
    3.52 +  | dest_upT T = raise TYPE ("dest_upT", [T], []);
    3.53 +
    3.54  fun up_const T = Const(@{const_name up}, T ->> mk_upT T);
    3.55  
    3.56  fun mk_up t = up_const (Term.fastype_of t) ` t;
    3.57  
    3.58 +fun fup_const (T, U) =
    3.59 +  Const(@{const_name fup}, (T ->> U) ->> mk_upT T ->> U);
    3.60 +
    3.61 +fun from_up T = fup_const (T, T) ` mk_ID T;
    3.62 +
    3.63  
    3.64  (*** Strict product type ***)
    3.65  
    3.66 @@ -98,6 +127,9 @@
    3.67  
    3.68  fun mk_sprodT (T, U) = Type(@{type_name "**"}, [T, U]);
    3.69  
    3.70 +fun dest_sprodT (Type(@{type_name "**"}, [T, U])) = (T, U)
    3.71 +  | dest_sprodT T = raise TYPE ("dest_sprodT", [T], []);
    3.72 +
    3.73  fun spair_const (T, U) =
    3.74    Const(@{const_name spair}, T ->> U ->> mk_sprodT (T, U));
    3.75  
    3.76 @@ -110,6 +142,12 @@
    3.77    | mk_stuple (t::[]) = t
    3.78    | mk_stuple (t::ts) = mk_spair (t, mk_stuple ts);
    3.79  
    3.80 +fun sfst_const (T, U) =
    3.81 +  Const(@{const_name sfst}, mk_sprodT (T, U) ->> T);
    3.82 +
    3.83 +fun ssnd_const (T, U) =
    3.84 +  Const(@{const_name ssnd}, mk_sprodT (T, U) ->> U);
    3.85 +
    3.86  
    3.87  (*** Strict sum type ***)
    3.88  
    3.89 @@ -139,6 +177,16 @@
    3.90      fst (inj (ts ~~ Ts))
    3.91    end;
    3.92  
    3.93 +fun sscase_const (T, U, V) =
    3.94 +  Const(@{const_name sscase},
    3.95 +    (T ->> V) ->> (U ->> V) ->> mk_ssumT (T, U) ->> V);
    3.96 +
    3.97 +fun from_sinl (T, U) =
    3.98 +  sscase_const (T, U, T) ` mk_ID T ` mk_bottom (U ->> T);
    3.99 +
   3.100 +fun from_sinr (T, U) =
   3.101 +  sscase_const (T, U, U) ` mk_bottom (T ->> U) ` mk_ID U;
   3.102 +
   3.103  
   3.104  (*** miscellaneous constructions ***)
   3.105  
   3.106 @@ -151,7 +199,7 @@
   3.107      fun argTs (Type (_, Ts)) = Ts | argTs _ = [];
   3.108      fun auto T = T ->> T;
   3.109    in
   3.110 -    Library.foldr mk_cfunT (map auto (argTs T), auto T)
   3.111 +    map auto (argTs T) -->> auto T
   3.112    end;
   3.113  
   3.114  val mk_equals = Logic.mk_equals;
   3.115 @@ -159,6 +207,13 @@
   3.116  val mk_trp = HOLogic.mk_Trueprop;
   3.117  val mk_fst = HOLogic.mk_fst;
   3.118  val mk_snd = HOLogic.mk_snd;
   3.119 +val mk_not = HOLogic.mk_not;
   3.120 +
   3.121 +fun mk_strict t =
   3.122 +  let val (T, U) = dest_cfunT (Term.fastype_of t);
   3.123 +  in mk_eq (t ` mk_bottom T, mk_bottom U) end;
   3.124 +
   3.125 +fun mk_defined t = mk_not (mk_eq (t, mk_bottom (Term.fastype_of t)));
   3.126  
   3.127  fun mk_cont t =
   3.128    let val T = Term.fastype_of t
   3.129 @@ -168,21 +223,6 @@
   3.130    let val (T, _) = dest_cfunT (Term.fastype_of t)
   3.131    in mk_capply (Const(@{const_name fix}, (T ->> T) ->> T), t) end;
   3.132  
   3.133 -fun ID_const T = Const (@{const_name ID}, T ->> T);
   3.134 -
   3.135 -fun cfcomp_const (T, U, V) =
   3.136 -  Const (@{const_name cfcomp}, (U ->> V) ->> (T ->> U) ->> (T ->> V));
   3.137 -
   3.138 -fun mk_cfcomp (f, g) =
   3.139 -  let
   3.140 -    val (U, V) = dest_cfunT (Term.fastype_of f);
   3.141 -    val (T, U') = dest_cfunT (Term.fastype_of g);
   3.142 -  in
   3.143 -    if U = U'
   3.144 -    then mk_capply (mk_capply (cfcomp_const (T, U, V), f), g)
   3.145 -    else raise TYPE ("mk_cfcomp", [U, U'], [f, g])
   3.146 -  end;
   3.147 -
   3.148  fun mk_Rep_of T =
   3.149    Const (@{const_name Rep_of}, Term.itselfT T --> deflT) $ Logic.mk_type T;
   3.150  
   3.151 @@ -196,8 +236,10 @@
   3.152  
   3.153  fun mk_eqs (t, u) = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u));
   3.154  
   3.155 -(*** miscellaneous ***)
   3.156  
   3.157 +(************************** miscellaneous functions ***************************)
   3.158 +
   3.159 +(*
   3.160  fun declare_consts
   3.161      (decls : (binding * typ * mixfix) list)
   3.162      (thy : theory)
   3.163 @@ -208,6 +250,7 @@
   3.164    in
   3.165      (map con decls, thy)
   3.166    end;
   3.167 +*)
   3.168  
   3.169  fun define_consts
   3.170      (specs : (binding * term * mixfix) list)
   3.171 @@ -228,6 +271,16 @@
   3.172      ((consts, def_thms), thy)
   3.173    end;
   3.174  
   3.175 +fun define_const
   3.176 +    (spec : binding * term * mixfix)
   3.177 +    (thy : theory)
   3.178 +    : (term * thm) * theory =
   3.179 +  let
   3.180 +    val ((consts, def_thms), thy) = define_consts [spec] thy;
   3.181 +  in
   3.182 +    ((hd consts, hd def_thms), thy)
   3.183 +  end;
   3.184 +
   3.185  
   3.186  (************** generating beta reduction rules from definitions **************)
   3.187  
   3.188 @@ -243,7 +296,7 @@
   3.189        let
   3.190          val (con, lam) = Logic.dest_equals (concl_of def_thm);
   3.191          val (args, rhs) = arglist lam;
   3.192 -        val lhs = Library.foldl mk_capply (con, args);
   3.193 +        val lhs = list_ccomb (con, args);
   3.194          val goal = mk_equals (lhs, rhs);
   3.195          val cs = ContProc.cont_thms lam;
   3.196          val betas = map (fn c => mk_meta_eq (c RS @{thm beta_cfun})) cs;
   3.197 @@ -255,45 +308,211 @@
   3.198        end;
   3.199  end;
   3.200  
   3.201 -(******************************* main function ********************************)
   3.202 +(******************************************************************************)
   3.203 +(************** definitions and theorems for selector functions ***************)
   3.204 +(******************************************************************************)
   3.205 +
   3.206 +fun add_selectors
   3.207 +    (spec : (term * (bool * binding option * typ) list) list)
   3.208 +    (rep_const : term)
   3.209 +    (abs_inv : thm)
   3.210 +    (rep_strict : thm)
   3.211 +    (rep_strict_iff : thm)
   3.212 +    (con_betas : thm list)
   3.213 +    (thy : theory)
   3.214 +    : thm list * theory =
   3.215 +  let
   3.216 +
   3.217 +    (* define selector functions *)
   3.218 +    val ((sel_consts, sel_defs), thy) =
   3.219 +      let
   3.220 +        fun rangeT s = snd (dest_cfunT (Term.fastype_of s));
   3.221 +        fun mk_outl s = mk_cfcomp (from_sinl (dest_ssumT (rangeT s)), s);
   3.222 +        fun mk_outr s = mk_cfcomp (from_sinr (dest_ssumT (rangeT s)), s);
   3.223 +        fun mk_sfst s = mk_cfcomp (sfst_const (dest_sprodT (rangeT s)), s);
   3.224 +        fun mk_ssnd s = mk_cfcomp (ssnd_const (dest_sprodT (rangeT s)), s);
   3.225 +        fun mk_down s = mk_cfcomp (from_up (dest_upT (rangeT s)), s);
   3.226 +
   3.227 +        fun sels_of_arg s (lazy, NONE,   T) = []
   3.228 +          | sels_of_arg s (lazy, SOME b, T) =
   3.229 +            [(b, if lazy then mk_down s else s, NoSyn)];
   3.230 +        fun sels_of_args s [] = []
   3.231 +          | sels_of_args s (v :: []) = sels_of_arg s v
   3.232 +          | sels_of_args s (v :: vs) =
   3.233 +            sels_of_arg (mk_sfst s) v @ sels_of_args (mk_ssnd s) vs;
   3.234 +        fun sels_of_cons s [] = []
   3.235 +          | sels_of_cons s ((con, args) :: []) = sels_of_args s args
   3.236 +          | sels_of_cons s ((con, args) :: cs) =
   3.237 +            sels_of_args (mk_outl s) args @ sels_of_cons (mk_outr s) cs;
   3.238 +        val sel_eqns : (binding * term * mixfix) list =
   3.239 +            sels_of_cons rep_const spec;
   3.240 +      in
   3.241 +        define_consts sel_eqns thy
   3.242 +      end
   3.243 +
   3.244 +    (* replace bindings with terms in constructor spec *)
   3.245 +    val spec2 : (term * (bool * term option * typ) list) list =
   3.246 +      let
   3.247 +        fun prep_arg (lazy, NONE, T) sels = ((lazy, NONE, T), sels)
   3.248 +          | prep_arg (lazy, SOME _, T) sels =
   3.249 +            ((lazy, SOME (hd sels), T), tl sels);
   3.250 +        fun prep_con (con, args) sels =
   3.251 +            apfst (pair con) (fold_map prep_arg args sels);
   3.252 +      in
   3.253 +        fst (fold_map prep_con spec sel_consts)
   3.254 +      end;
   3.255 +
   3.256 +    (* prove selector strictness rules *)
   3.257 +    val sel_stricts : thm list =
   3.258 +      let
   3.259 +        val rules = rep_strict :: sel_defs @ @{thms sel_strict_rules};
   3.260 +        val tac = simp_tac (HOL_basic_ss addsimps rules) 1;
   3.261 +        fun sel_strict sel =
   3.262 +          let
   3.263 +            val goal = mk_trp (mk_strict sel);
   3.264 +          in
   3.265 +            Goal.prove_global thy [] [] goal (K tac)
   3.266 +          end
   3.267 +      in
   3.268 +        map sel_strict sel_consts
   3.269 +      end
   3.270 +
   3.271 +    (* prove selector application rules *)
   3.272 +    val sel_apps : thm list =
   3.273 +      let
   3.274 +        val rules = @{thms sel_app_rules};
   3.275 +        val simps = simp_thms @ [abs_inv] @ con_betas @ sel_defs @ rules;
   3.276 +        val tac = asm_simp_tac (HOL_basic_ss addsimps simps) 1;
   3.277 +        fun sel_apps_of (i, (con, args)) =
   3.278 +          let
   3.279 +            val Ts : typ list = map #3 args;
   3.280 +            val ns : string list = Datatype_Prop.make_tnames Ts;
   3.281 +            val vs : term list = map Free (ns ~~ Ts);
   3.282 +            val con_app : term = list_ccomb (con, vs);
   3.283 +            val vs' : (bool * term) list = map #1 args ~~ vs;
   3.284 +            fun one_same (n, sel, T) =
   3.285 +              let
   3.286 +                val xs = map snd (filter_out fst (nth_drop n vs'));
   3.287 +                val assms = map (mk_trp o mk_defined) xs;
   3.288 +                val concl = mk_trp (mk_eq (sel ` con_app, nth vs n));
   3.289 +                val goal = Logic.list_implies (assms, concl);
   3.290 +              in
   3.291 +                Goal.prove_global thy [] [] goal (K tac)
   3.292 +              end;
   3.293 +            fun one_diff (n, sel, T) =
   3.294 +              let
   3.295 +                val goal = mk_trp (mk_eq (sel ` con_app, mk_bottom T));
   3.296 +              in
   3.297 +                Goal.prove_global thy [] [] goal (K tac)
   3.298 +              end;
   3.299 +            fun one_con (j, (_, args')) : thm list =
   3.300 +              let
   3.301 +                fun prep (i, (lazy, NONE, T)) = NONE
   3.302 +                  | prep (i, (lazy, SOME sel, T)) = SOME (i, sel, T);
   3.303 +                val sels : (int * term * typ) list =
   3.304 +                  map_filter prep (map_index I args');
   3.305 +              in
   3.306 +                if i = j
   3.307 +                then map one_same sels
   3.308 +                else map one_diff sels
   3.309 +              end
   3.310 +          in
   3.311 +            flat (map_index one_con spec2)
   3.312 +          end
   3.313 +      in
   3.314 +        flat (map_index sel_apps_of spec2)
   3.315 +      end
   3.316 +
   3.317 +  (* prove selector definedness rules *)
   3.318 +    val sel_defins : thm list =
   3.319 +      let
   3.320 +        val rules = @{thms sel_defined_iff_rules};
   3.321 +        val simps = rep_strict_iff :: sel_defs @ rules;
   3.322 +        val tac = simp_tac (HOL_basic_ss addsimps simps) 1;
   3.323 +        fun sel_defin sel =
   3.324 +          let
   3.325 +            val (T, U) = dest_cfunT (Term.fastype_of sel);
   3.326 +            val x = Free ("x", T);
   3.327 +            val lhs = mk_eq (sel ` x, mk_bottom U);
   3.328 +            val rhs = mk_eq (x, mk_bottom T);
   3.329 +            val goal = mk_trp (mk_eq (lhs, rhs));
   3.330 +          in
   3.331 +            Goal.prove_global thy [] [] goal (K tac)
   3.332 +          end
   3.333 +        fun one_arg (false, SOME sel, T) = SOME (sel_defin sel)
   3.334 +          | one_arg _                    = NONE;
   3.335 +      in
   3.336 +        case spec2 of
   3.337 +          [(con, args)] => map_filter one_arg args
   3.338 +        | _             => []
   3.339 +      end;
   3.340 +
   3.341 +  in
   3.342 +    (sel_stricts @ sel_defins @ sel_apps, thy)
   3.343 +  end
   3.344 +
   3.345 +(******************************************************************************)
   3.346 +(************* definitions and theorems for constructor functions *************)
   3.347 +(******************************************************************************)
   3.348  
   3.349  fun add_domain_constructors
   3.350      (dname : string)
   3.351      (lhsT : typ,
   3.352 -     cons : (binding * (bool * binding option * typ) list * mixfix) list)
   3.353 +     spec : (binding * (bool * binding option * typ) list * mixfix) list)
   3.354      (rep_const : term, abs_const : term)
   3.355      (rep_iso_thm : thm, abs_iso_thm : thm)
   3.356      (thy : theory) =
   3.357    let
   3.358 -    (* TODO: re-enable this *)
   3.359 -    (* val thy = Sign.add_path dname thy; *)
   3.360 +
   3.361 +    (* prove rep/abs strictness rules *)
   3.362 +    val iso_locale = @{thm iso.intro} OF [abs_iso_thm, rep_iso_thm];
   3.363 +    val rep_strict = iso_locale RS @{thm iso.rep_strict};
   3.364 +    val abs_strict = iso_locale RS @{thm iso.abs_strict};
   3.365 +    val rep_defined_iff = iso_locale RS @{thm iso.rep_defined_iff};
   3.366 +    val abs_defined_iff = iso_locale RS @{thm iso.abs_defined_iff};
   3.367  
   3.368      (* define constructor functions *)
   3.369      val ((con_consts, con_def_thms), thy) =
   3.370        let
   3.371 -        fun prep_con (bind, args, mx) =
   3.372 -          (bind, args ~~ Datatype_Prop.make_tnames (map #3 args), mx);
   3.373 -        fun var_of ((lazy, sel, T), name) = Free (name, T);
   3.374 -        fun is_lazy ((lazy, sel, T), name) = lazy;
   3.375 -        val cons' = map prep_con cons;
   3.376 -        fun one_arg arg = (if is_lazy arg then mk_up else I) (var_of arg);
   3.377 -        fun one_con (bind, args, mx) = mk_stuple (map one_arg args);
   3.378 +        fun vars_of args =
   3.379 +          let
   3.380 +            val Ts = map (fn (lazy,sel,T) => T) args;
   3.381 +            val ns = Datatype_Prop.make_tnames Ts;
   3.382 +          in
   3.383 +            map Free (ns ~~ Ts)
   3.384 +          end;
   3.385 +        fun one_arg (lazy,_,_) var = if lazy then mk_up var else var;
   3.386 +        fun one_con (_,args,_) = mk_stuple (map2 one_arg args (vars_of args));
   3.387          fun mk_abs t = abs_const ` t;
   3.388 -        val rhss = map mk_abs (mk_sinjects (map one_con cons'));
   3.389 +        val rhss = map mk_abs (mk_sinjects (map one_con spec));
   3.390          fun mk_def (bind, args, mx) rhs =
   3.391 -          (bind, big_lambdas (map var_of args) rhs, mx);
   3.392 +          (bind, big_lambdas (vars_of args) rhs, mx);
   3.393        in
   3.394 -        define_consts (map2 mk_def cons' rhss) thy
   3.395 +        define_consts (map2 mk_def spec rhss) thy
   3.396        end;
   3.397  
   3.398 +    (* prove beta reduction rules for constructors *)
   3.399      val con_beta_thms = map (beta_of_def thy) con_def_thms;
   3.400  
   3.401 -    (* TODO: re-enable this *)
   3.402 -    (* val thy = Sign.parent_path thy; *)
   3.403 +    (* TODO: enable this earlier *)
   3.404 +    val thy = Sign.add_path dname thy;
   3.405 +
   3.406 +    (* replace bindings with terms in constructor spec *)
   3.407 +    val spec2 : (term * (bool * binding option * typ) list) list =
   3.408 +      map2 (fn con => fn (b, args, mx) => (con, args)) con_consts spec;
   3.409 +
   3.410 +    (* define and prove theorems for selector functions *)
   3.411 +    val (sel_thms : thm list, thy : theory) =
   3.412 +      add_selectors spec2 rep_const
   3.413 +        abs_iso_thm rep_strict rep_defined_iff con_beta_thms thy;
   3.414 +
   3.415 +    (* restore original signature path *)
   3.416 +    val thy = Sign.parent_path thy;
   3.417  
   3.418      val result =
   3.419        { con_consts = con_consts,
   3.420 -        con_defs = con_def_thms };
   3.421 +        con_defs = con_def_thms,
   3.422 +        sel_rews = sel_thms };
   3.423    in
   3.424      (result, thy)
   3.425    end;
     4.1 --- a/src/HOLCF/Tools/Domain/domain_syntax.ML	Wed Feb 24 17:37:59 2010 -0800
     4.2 +++ b/src/HOLCF/Tools/Domain/domain_syntax.ML	Thu Feb 25 13:16:28 2010 -0800
     4.3 @@ -86,9 +86,6 @@
     4.4            (mat_name_ con,
     4.5             mk_matT(dtype, map third args, freetvar "t" 1),
     4.6             Mixfix(escape ("match_" ^ Binding.name_of con), [], Syntax.max_pri));
     4.7 -      fun sel1 (_,sel,typ) =
     4.8 -          Option.map (fn s => (s,dtype ->> typ,NoSyn)) sel;
     4.9 -      fun sel (con,args,mx) = map_filter sel1 args;
    4.10        fun mk_patT (a,b)     = a ->> mk_maybeT b;
    4.11        fun pat_arg_typ n arg = mk_patT (third arg, freetvar "t" n);
    4.12        fun pat (con,args,mx) =
    4.13 @@ -101,7 +98,6 @@
    4.14      val consts_dis = map dis cons';
    4.15      val consts_mat = map mat cons';
    4.16      val consts_pat = map pat cons';
    4.17 -    val consts_sel = maps sel cons';
    4.18      end;
    4.19  
    4.20  (* ----- constants concerning induction ------------------------------------- *)
    4.21 @@ -169,7 +165,7 @@
    4.22          if definitional then [] else [const_rep, const_abs, const_copy];
    4.23  
    4.24    in (optional_consts @ [const_when] @ 
    4.25 -      consts_dis @ consts_mat @ consts_pat @ consts_sel @
    4.26 +      consts_dis @ consts_mat @ consts_pat @
    4.27        [const_take, const_finite],
    4.28        (case_trans false :: case_trans true :: (abscon_trans false @ abscon_trans true @ Case_trans)))
    4.29    end; (* let *)
     5.1 --- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Wed Feb 24 17:37:59 2010 -0800
     5.2 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Thu Feb 25 13:16:28 2010 -0800
     5.3 @@ -161,6 +161,7 @@
     5.4    val axs_dis_def = map (get_def dis_name) cons;
     5.5    val axs_mat_def = map (get_def mat_name) cons;
     5.6    val axs_pat_def = map (get_def pat_name) cons;
     5.7 +(*
     5.8    val axs_sel_def =
     5.9      let
    5.10        fun def_of_sel sel = ga (sel^"_def") dname;
    5.11 @@ -169,6 +170,7 @@
    5.12      in
    5.13        maps defs_of_con cons
    5.14      end;
    5.15 +*)
    5.16    val ax_copy_def = ga "copy_def" dname;
    5.17  end; (* local *)
    5.18  
    5.19 @@ -196,6 +198,7 @@
    5.20      (rep_const, abs_const) (ax_rep_iso, ax_abs_iso) thy;
    5.21  
    5.22  val axs_con_def = #con_defs result;
    5.23 +val sel_rews = #sel_rews result;
    5.24  
    5.25  (* ----- theorems concerning the isomorphism -------------------------------- *)
    5.26  
    5.27 @@ -472,79 +475,6 @@
    5.28    val con_compacts = map con_compact cons;
    5.29  end;
    5.30  
    5.31 -local
    5.32 -  fun one_sel sel =
    5.33 -    pg axs_sel_def (mk_trp (strict (%%:sel)))
    5.34 -      (K [simp_tac (HOLCF_ss addsimps when_rews) 1]);
    5.35 -
    5.36 -  fun sel_strict (_, _, args) =
    5.37 -    map_filter (Option.map one_sel o sel_of) args;
    5.38 -in
    5.39 -  val _ = trace " Proving sel_stricts...";
    5.40 -  val sel_stricts = maps sel_strict cons;
    5.41 -end;
    5.42 -
    5.43 -local
    5.44 -  fun sel_app_same c n sel (con, args) =
    5.45 -    let
    5.46 -      val nlas = nonlazy args;
    5.47 -      val vns = map vname args;
    5.48 -      val vnn = List.nth (vns, n);
    5.49 -      val nlas' = filter (fn v => v <> vnn) nlas;
    5.50 -      val lhs = (%%:sel)`(con_app con args);
    5.51 -      val goal = lift_defined %: (nlas', mk_trp (lhs === %:vnn));
    5.52 -      fun tacs1 ctxt =
    5.53 -        if vnn mem nlas
    5.54 -                        (* FIXME! case_UU_tac *)
    5.55 -        then [case_UU_tac ctxt (when_rews @ con_stricts) 1 vnn]
    5.56 -        else [];
    5.57 -      val tacs2 = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
    5.58 -    in pg axs_sel_def goal (fn ctxt => (tacs1 ctxt @ tacs2)) end;
    5.59 -
    5.60 -  fun sel_app_diff c n sel (con, args) =
    5.61 -    let
    5.62 -      val nlas = nonlazy args;
    5.63 -      val goal = mk_trp (%%:sel ` con_app con args === UU);
    5.64 -                        (* FIXME! case_UU_tac *)
    5.65 -      fun tacs1 ctxt = map (case_UU_tac ctxt (when_rews @ con_stricts) 1) nlas;
    5.66 -      val tacs2 = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
    5.67 -    in pg axs_sel_def goal (fn ctxt => (tacs1 ctxt @ tacs2)) end;
    5.68 -
    5.69 -  fun sel_app c n sel (con, _, args) =
    5.70 -    if con = c
    5.71 -    then sel_app_same c n sel (con, args)
    5.72 -    else sel_app_diff c n sel (con, args);
    5.73 -
    5.74 -  fun one_sel c n sel = map (sel_app c n sel) cons;
    5.75 -  fun one_sel' c n arg = Option.map (one_sel c n) (sel_of arg);
    5.76 -  fun one_con (c, _, args) =
    5.77 -    flat (map_filter I (mapn (one_sel' c) 0 args));
    5.78 -in
    5.79 -  val _ = trace " Proving sel_apps...";
    5.80 -  val sel_apps = maps one_con cons;
    5.81 -end;
    5.82 -
    5.83 -local
    5.84 -  fun sel_defin sel =
    5.85 -    let
    5.86 -      val goal = defined (%:x_name) ==> defined (%%:sel`%x_name);
    5.87 -      val tacs = [
    5.88 -        rtac casedist 1,
    5.89 -        contr_tac 1,
    5.90 -        DETERM_UNTIL_SOLVED (CHANGED
    5.91 -          (asm_simp_tac (HOLCF_ss addsimps sel_apps) 1))];
    5.92 -    in pg [] goal (K tacs) end;
    5.93 -in
    5.94 -  val _ = trace " Proving sel_defins...";
    5.95 -  val sel_defins =
    5.96 -    if length cons = 1
    5.97 -    then map_filter (fn arg => Option.map sel_defin (sel_of arg))
    5.98 -                 (filter_out is_lazy (third (hd cons)))
    5.99 -    else [];
   5.100 -end;
   5.101 -
   5.102 -val sel_rews = sel_stricts @ sel_defins @ sel_apps;
   5.103 -
   5.104  val _ = trace " Proving dist_les...";
   5.105  val dist_les =
   5.106    let