move take-related definitions and proofs to new module; simplify map_of_typ functions
authorhuffman
Tue Mar 02 13:50:23 2010 -0800 (2010-03-02)
changeset 35514a2cfa413eaab
parent 35513 89eddccbb93d
child 35515 d631dc53ede0
move take-related definitions and proofs to new module; simplify map_of_typ functions
src/HOLCF/Representable.thy
src/HOLCF/Tools/Domain/domain_axioms.ML
src/HOLCF/Tools/Domain/domain_constructors.ML
src/HOLCF/Tools/Domain/domain_isomorphism.ML
src/HOLCF/Tools/Domain/domain_take_proofs.ML
src/HOLCF/Tools/Domain/domain_theorems.ML
     1.1 --- a/src/HOLCF/Representable.thy	Tue Mar 02 13:01:22 2010 -0800
     1.2 +++ b/src/HOLCF/Representable.thy	Tue Mar 02 13:50:23 2010 -0800
     1.3 @@ -9,6 +9,7 @@
     1.4  uses
     1.5    ("Tools/repdef.ML")
     1.6    ("Tools/holcf_library.ML")
     1.7 +  ("Tools/Domain/domain_take_proofs.ML")
     1.8    ("Tools/Domain/domain_isomorphism.ML")
     1.9  begin
    1.10  
    1.11 @@ -778,6 +779,7 @@
    1.12  subsection {* Constructing Domain Isomorphisms *}
    1.13  
    1.14  use "Tools/holcf_library.ML"
    1.15 +use "Tools/Domain/domain_take_proofs.ML"
    1.16  use "Tools/Domain/domain_isomorphism.ML"
    1.17  
    1.18  setup {*
     2.1 --- a/src/HOLCF/Tools/Domain/domain_axioms.ML	Tue Mar 02 13:01:22 2010 -0800
     2.2 +++ b/src/HOLCF/Tools/Domain/domain_axioms.ML	Tue Mar 02 13:50:23 2010 -0800
     2.3 @@ -135,7 +135,7 @@
     2.4      val dom_binds = map (Binding.name o Long_Name.base_name) dnames;
     2.5      val thy =
     2.6          if definitional then thy
     2.7 -        else snd (Domain_Isomorphism.define_take_functions
     2.8 +        else snd (Domain_Take_Proofs.define_take_functions
     2.9                      (dom_binds ~~ map get_iso_info eqs') thy);
    2.10  
    2.11      fun add_one' (dnam, axs, dfs) =
     3.1 --- a/src/HOLCF/Tools/Domain/domain_constructors.ML	Tue Mar 02 13:01:22 2010 -0800
     3.2 +++ b/src/HOLCF/Tools/Domain/domain_constructors.ML	Tue Mar 02 13:50:23 2010 -0800
     3.3 @@ -10,7 +10,7 @@
     3.4    val add_domain_constructors :
     3.5        string
     3.6        -> (binding * (bool * binding option * typ) list * mixfix) list
     3.7 -      -> Domain_Isomorphism.iso_info
     3.8 +      -> Domain_Take_Proofs.iso_info
     3.9        -> theory
    3.10        -> { con_consts : term list,
    3.11             con_betas : thm list,
    3.12 @@ -1011,7 +1011,7 @@
    3.13  fun add_domain_constructors
    3.14      (dname : string)
    3.15      (spec : (binding * (bool * binding option * typ) list * mixfix) list)
    3.16 -    (iso_info : Domain_Isomorphism.iso_info)
    3.17 +    (iso_info : Domain_Take_Proofs.iso_info)
    3.18      (thy : theory) =
    3.19    let
    3.20  
     4.1 --- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Tue Mar 02 13:01:22 2010 -0800
     4.2 +++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Tue Mar 02 13:50:23 2010 -0800
     4.3 @@ -6,37 +6,17 @@
     4.4  
     4.5  signature DOMAIN_ISOMORPHISM =
     4.6  sig
     4.7 -  type iso_info =
     4.8 -    {
     4.9 -      repT : typ,
    4.10 -      absT : typ,
    4.11 -      rep_const : term,
    4.12 -      abs_const : term,
    4.13 -      rep_inverse : thm,
    4.14 -      abs_inverse : thm
    4.15 -    }
    4.16    val domain_isomorphism :
    4.17      (string list * binding * mixfix * typ * (binding * binding) option) list
    4.18 -      -> theory -> iso_info list * theory
    4.19 +      -> theory -> Domain_Take_Proofs.iso_info list * theory
    4.20    val domain_isomorphism_cmd :
    4.21      (string list * binding * mixfix * string * (binding * binding) option) list
    4.22        -> theory -> theory
    4.23    val add_type_constructor :
    4.24      (string * term * string * thm  * thm * thm * thm) -> theory -> theory
    4.25 -  val get_map_tab :
    4.26 -    theory -> string Symtab.table
    4.27 -  val define_take_functions :
    4.28 -    (binding * iso_info) list -> theory ->
    4.29 -    { take_consts : term list,
    4.30 -      take_defs : thm list,
    4.31 -      chain_take_thms : thm list,
    4.32 -      take_0_thms : thm list,
    4.33 -      take_Suc_thms : thm list,
    4.34 -      deflation_take_thms : thm list
    4.35 -    } * theory;
    4.36  end;
    4.37  
    4.38 -structure Domain_Isomorphism :> DOMAIN_ISOMORPHISM =
    4.39 +structure Domain_Isomorphism : DOMAIN_ISOMORPHISM =
    4.40  struct
    4.41  
    4.42  val beta_ss =
    4.43 @@ -53,47 +33,51 @@
    4.44  
    4.45  structure DeflData = Theory_Data
    4.46  (
    4.47 +  (* terms like "foo_defl" *)
    4.48    type T = term Symtab.table;
    4.49    val empty = Symtab.empty;
    4.50    val extend = I;
    4.51    fun merge data = Symtab.merge (K true) data;
    4.52  );
    4.53  
    4.54 -structure MapData = Theory_Data
    4.55 +structure RepData = Theory_Data
    4.56  (
    4.57 -  type T = string Symtab.table;
    4.58 -  val empty = Symtab.empty;
    4.59 -  val extend = I;
    4.60 -  fun merge data = Symtab.merge (K true) data;
    4.61 -);
    4.62 -
    4.63 -structure Thm_List : THEORY_DATA_ARGS =
    4.64 -struct
    4.65 +  (* theorems like "REP('a foo) = foo_defl$REP('a)" *)
    4.66    type T = thm list;
    4.67    val empty = [];
    4.68    val extend = I;
    4.69    val merge = Thm.merge_thms;
    4.70 -end;
    4.71 -
    4.72 -structure RepData = Theory_Data (Thm_List);
    4.73 +);
    4.74  
    4.75 -structure IsodeflData = Theory_Data (Thm_List);
    4.76 +structure MapIdData = Theory_Data
    4.77 +(
    4.78 +  (* theorems like "foo_map$ID = ID" *)
    4.79 +  type T = thm list;
    4.80 +  val empty = [];
    4.81 +  val extend = I;
    4.82 +  val merge = Thm.merge_thms;
    4.83 +);
    4.84  
    4.85 -structure MapIdData = Theory_Data (Thm_List);
    4.86 -
    4.87 -structure DeflMapData = Theory_Data (Thm_List);
    4.88 +structure IsodeflData = Theory_Data
    4.89 +(
    4.90 +  (* theorems like "isodefl d t ==> isodefl (foo_map$d) (foo_defl$t)" *)
    4.91 +  type T = thm list;
    4.92 +  val empty = [];
    4.93 +  val extend = I;
    4.94 +  val merge = Thm.merge_thms;
    4.95 +);
    4.96  
    4.97  fun add_type_constructor
    4.98    (tname, defl_const, map_name, REP_thm,
    4.99     isodefl_thm, map_ID_thm, defl_map_thm) =
   4.100      DeflData.map (Symtab.insert (K true) (tname, defl_const))
   4.101 -    #> MapData.map (Symtab.insert (K true) (tname, map_name))
   4.102 +    #> Domain_Take_Proofs.add_map_function (tname, map_name, defl_map_thm)
   4.103      #> RepData.map (Thm.add_thm REP_thm)
   4.104      #> IsodeflData.map (Thm.add_thm isodefl_thm)
   4.105 -    #> MapIdData.map (Thm.add_thm map_ID_thm)
   4.106 -    #> DeflMapData.map (Thm.add_thm defl_map_thm);
   4.107 +    #> MapIdData.map (Thm.add_thm map_ID_thm);
   4.108  
   4.109 -val get_map_tab = MapData.get;
   4.110 +
   4.111 +(* val get_map_tab = MapData.get; *)
   4.112  
   4.113  
   4.114  (******************************************************************************)
   4.115 @@ -142,17 +126,7 @@
   4.116  (****************************** isomorphism info ******************************)
   4.117  (******************************************************************************)
   4.118  
   4.119 -type iso_info =
   4.120 -  {
   4.121 -    absT : typ,
   4.122 -    repT : typ,
   4.123 -    abs_const : term,
   4.124 -    rep_const : term,
   4.125 -    abs_inverse : thm,
   4.126 -    rep_inverse : thm
   4.127 -  }
   4.128 -
   4.129 -fun deflation_abs_rep (info : iso_info) : thm =
   4.130 +fun deflation_abs_rep (info : Domain_Take_Proofs.iso_info) : thm =
   4.131    let
   4.132      val abs_iso = #abs_inverse info;
   4.133      val rep_iso = #rep_inverse info;
   4.134 @@ -250,22 +224,6 @@
   4.135                    else error ("defl_of_typ: type variable under unsupported type constructor " ^ c);
   4.136    in defl_of T end;
   4.137  
   4.138 -fun map_of_typ
   4.139 -    (tab : string Symtab.table)
   4.140 -    (T : typ) : term =
   4.141 -  let
   4.142 -    fun is_closed_typ (Type (_, Ts)) = forall is_closed_typ Ts
   4.143 -      | is_closed_typ _ = false;
   4.144 -    fun map_of (T as TFree (a, _)) = Free (Library.unprefix "'" a, T ->> T)
   4.145 -      | map_of (T as TVar _) = error ("map_of_typ: TVar")
   4.146 -      | map_of (T as Type (c, Ts)) =
   4.147 -        case Symtab.lookup tab c of
   4.148 -          SOME t => list_ccomb (Const (t, mapT T), map map_of Ts)
   4.149 -        | NONE => if is_closed_typ T
   4.150 -                  then mk_ID T
   4.151 -                  else error ("map_of_typ: type variable under unsupported type constructor " ^ c);
   4.152 -  in map_of T end;
   4.153 -
   4.154  
   4.155  (******************************************************************************)
   4.156  (********************* declaring definitions and theorems *********************)
   4.157 @@ -293,217 +251,6 @@
   4.158      ||> Sign.parent_path;
   4.159  
   4.160  (******************************************************************************)
   4.161 -(************************** defining take functions ***************************)
   4.162 -(******************************************************************************)
   4.163 -
   4.164 -fun define_take_functions
   4.165 -    (spec : (binding * iso_info) list)
   4.166 -    (thy : theory) =
   4.167 -  let
   4.168 -
   4.169 -    (* retrieve components of spec *)
   4.170 -    val dom_binds = map fst spec;
   4.171 -    val iso_infos = map snd spec;
   4.172 -    val dom_eqns = map (fn x => (#absT x, #repT x)) iso_infos;
   4.173 -    val rep_abs_consts = map (fn x => (#rep_const x, #abs_const x)) iso_infos;
   4.174 -    val dnames = map Binding.name_of dom_binds;
   4.175 -
   4.176 -    (* get table of map functions *)
   4.177 -    val map_tab = MapData.get thy;
   4.178 -
   4.179 -    fun mk_projs []      t = []
   4.180 -      | mk_projs (x::[]) t = [(x, t)]
   4.181 -      | mk_projs (x::xs) t = (x, mk_fst t) :: mk_projs xs (mk_snd t);
   4.182 -
   4.183 -    fun mk_cfcomp2 ((rep_const, abs_const), f) =
   4.184 -        mk_cfcomp (abs_const, mk_cfcomp (f, rep_const));
   4.185 -
   4.186 -    (* defining map functions over dtyps *)
   4.187 -    fun copy_of_dtyp recs (T, dt) =
   4.188 -        if Datatype_Aux.is_rec_type dt
   4.189 -        then copy_of_dtyp' recs (T, dt)
   4.190 -        else mk_ID T
   4.191 -    and copy_of_dtyp' recs (T, Datatype_Aux.DtRec i) = nth recs i
   4.192 -      | copy_of_dtyp' recs (T, Datatype_Aux.DtTFree a) = mk_ID T
   4.193 -      | copy_of_dtyp' recs (T, Datatype_Aux.DtType (c, ds)) =
   4.194 -        case Symtab.lookup map_tab c of
   4.195 -          SOME f =>
   4.196 -          list_ccomb
   4.197 -            (Const (f, mapT T),
   4.198 -             map (copy_of_dtyp recs) (snd (dest_Type T) ~~ ds))
   4.199 -        | NONE =>
   4.200 -          (warning ("copy_of_dtyp: unknown type constructor " ^ c); mk_ID T);
   4.201 -
   4.202 -    (* define take functional *)
   4.203 -    val new_dts : (string * string list) list =
   4.204 -      map (apsnd (map (fst o dest_TFree)) o dest_Type o fst) dom_eqns;
   4.205 -    val copy_arg_type = mk_tupleT (map (fn (T, _) => T ->> T) dom_eqns);
   4.206 -    val copy_arg = Free ("f", copy_arg_type);
   4.207 -    val copy_args = map snd (mk_projs dom_binds copy_arg);
   4.208 -    fun one_copy_rhs (rep_abs, (lhsT, rhsT)) =
   4.209 -      let
   4.210 -        val dtyp = Datatype_Aux.dtyp_of_typ new_dts rhsT;
   4.211 -        val body = copy_of_dtyp copy_args (rhsT, dtyp);
   4.212 -      in
   4.213 -        mk_cfcomp2 (rep_abs, body)
   4.214 -      end;
   4.215 -    val take_functional =
   4.216 -        big_lambda copy_arg
   4.217 -          (mk_tuple (map one_copy_rhs (rep_abs_consts ~~ dom_eqns)));
   4.218 -    val take_rhss =
   4.219 -      let
   4.220 -        val i = Free ("i", HOLogic.natT);
   4.221 -        val rhs = mk_iterate (i, take_functional)
   4.222 -      in
   4.223 -        map (Term.lambda i o snd) (mk_projs dom_binds rhs)
   4.224 -      end;
   4.225 -
   4.226 -    (* define take constants *)
   4.227 -    fun define_take_const ((tbind, take_rhs), (lhsT, rhsT)) thy =
   4.228 -      let
   4.229 -        val take_type = HOLogic.natT --> lhsT ->> lhsT;
   4.230 -        val take_bind = Binding.suffix_name "_take" tbind;
   4.231 -        val (take_const, thy) =
   4.232 -          Sign.declare_const ((take_bind, take_type), NoSyn) thy;
   4.233 -        val take_eqn = Logic.mk_equals (take_const, take_rhs);
   4.234 -        val (take_def_thm, thy) =
   4.235 -          thy
   4.236 -          |> Sign.add_path (Binding.name_of tbind)
   4.237 -          |> yield_singleton
   4.238 -              (PureThy.add_defs false o map Thm.no_attributes)
   4.239 -              (Binding.name "take_def", take_eqn)
   4.240 -          ||> Sign.parent_path;
   4.241 -      in ((take_const, take_def_thm), thy) end;
   4.242 -    val ((take_consts, take_defs), thy) = thy
   4.243 -      |> fold_map define_take_const (dom_binds ~~ take_rhss ~~ dom_eqns)
   4.244 -      |>> ListPair.unzip;
   4.245 -
   4.246 -    (* prove chain_take lemmas *)
   4.247 -    fun prove_chain_take (take_const, dname) thy =
   4.248 -      let
   4.249 -        val goal = mk_trp (mk_chain take_const);
   4.250 -        val rules = take_defs @ @{thms chain_iterate ch2ch_fst ch2ch_snd};
   4.251 -        val tac = simp_tac (HOL_basic_ss addsimps rules) 1;
   4.252 -        val chain_take_thm = Goal.prove_global thy [] [] goal (K tac);
   4.253 -      in
   4.254 -        add_qualified_thm "chain_take" (dname, chain_take_thm) thy
   4.255 -      end;
   4.256 -    val (chain_take_thms, thy) =
   4.257 -      fold_map prove_chain_take (take_consts ~~ dnames) thy;
   4.258 -
   4.259 -    (* prove take_0 lemmas *)
   4.260 -    fun prove_take_0 ((take_const, dname), (lhsT, rhsT)) thy =
   4.261 -      let
   4.262 -        val lhs = take_const $ @{term "0::nat"};
   4.263 -        val goal = mk_eqs (lhs, mk_bottom (lhsT ->> lhsT));
   4.264 -        val rules = take_defs @ @{thms iterate_0 fst_strict snd_strict};
   4.265 -        val tac = simp_tac (HOL_basic_ss addsimps rules) 1;
   4.266 -        val take_0_thm = Goal.prove_global thy [] [] goal (K tac);
   4.267 -      in
   4.268 -        add_qualified_thm "take_0" (dname, take_0_thm) thy
   4.269 -      end;
   4.270 -    val (take_0_thms, thy) =
   4.271 -      fold_map prove_take_0 (take_consts ~~ dnames ~~ dom_eqns) thy;
   4.272 -
   4.273 -    (* prove take_Suc lemmas *)
   4.274 -    val i = Free ("i", natT);
   4.275 -    val take_is = map (fn t => t $ i) take_consts;
   4.276 -    fun prove_take_Suc
   4.277 -          (((take_const, rep_abs), dname), (lhsT, rhsT)) thy =
   4.278 -      let
   4.279 -        val lhs = take_const $ (@{term Suc} $ i);
   4.280 -        val dtyp = Datatype_Aux.dtyp_of_typ new_dts rhsT;
   4.281 -        val body = copy_of_dtyp take_is (rhsT, dtyp);
   4.282 -        val rhs = mk_cfcomp2 (rep_abs, body);
   4.283 -        val goal = mk_eqs (lhs, rhs);
   4.284 -        val simps = @{thms iterate_Suc fst_conv snd_conv}
   4.285 -        val rules = take_defs @ simps;
   4.286 -        val tac = simp_tac (beta_ss addsimps rules) 1;
   4.287 -        val take_Suc_thm = Goal.prove_global thy [] [] goal (K tac);
   4.288 -      in
   4.289 -        add_qualified_thm "take_Suc" (dname, take_Suc_thm) thy
   4.290 -      end;
   4.291 -    val (take_Suc_thms, thy) =
   4.292 -      fold_map prove_take_Suc
   4.293 -        (take_consts ~~ rep_abs_consts ~~ dnames ~~ dom_eqns) thy;
   4.294 -
   4.295 -    (* prove deflation theorems for take functions *)
   4.296 -    val deflation_abs_rep_thms = map deflation_abs_rep iso_infos;
   4.297 -    val deflation_take_thm =
   4.298 -      let
   4.299 -        val i = Free ("i", natT);
   4.300 -        fun mk_goal take_const = mk_deflation (take_const $ i);
   4.301 -        val goal = mk_trp (foldr1 mk_conj (map mk_goal take_consts));
   4.302 -        val adm_rules =
   4.303 -          @{thms adm_conj adm_subst [OF _ adm_deflation]
   4.304 -                 cont2cont_fst cont2cont_snd cont_id};
   4.305 -        val bottom_rules =
   4.306 -          take_0_thms @ @{thms deflation_UU simp_thms};
   4.307 -        val deflation_rules =
   4.308 -          @{thms conjI deflation_ID}
   4.309 -          @ deflation_abs_rep_thms
   4.310 -          @ DeflMapData.get thy;
   4.311 -      in
   4.312 -        Goal.prove_global thy [] [] goal (fn _ =>
   4.313 -         EVERY
   4.314 -          [rtac @{thm nat.induct} 1,
   4.315 -           simp_tac (HOL_basic_ss addsimps bottom_rules) 1,
   4.316 -           asm_simp_tac (HOL_basic_ss addsimps take_Suc_thms) 1,
   4.317 -           REPEAT (etac @{thm conjE} 1
   4.318 -                   ORELSE resolve_tac deflation_rules 1
   4.319 -                   ORELSE atac 1)])
   4.320 -      end;
   4.321 -    fun conjuncts [] thm = []
   4.322 -      | conjuncts (n::[]) thm = [(n, thm)]
   4.323 -      | conjuncts (n::ns) thm = let
   4.324 -          val thmL = thm RS @{thm conjunct1};
   4.325 -          val thmR = thm RS @{thm conjunct2};
   4.326 -        in (n, thmL):: conjuncts ns thmR end;
   4.327 -    val (deflation_take_thms, thy) =
   4.328 -      fold_map (add_qualified_thm "deflation_take")
   4.329 -        (map (apsnd Drule.export_without_context)
   4.330 -          (conjuncts dnames deflation_take_thm)) thy;
   4.331 -
   4.332 -    (* prove strictness of take functions *)
   4.333 -    fun prove_take_strict (take_const, dname) thy =
   4.334 -      let
   4.335 -        val goal = mk_trp (mk_strict (take_const $ Free ("i", natT)));
   4.336 -        val tac = rtac @{thm deflation_strict} 1
   4.337 -                  THEN resolve_tac deflation_take_thms 1;
   4.338 -        val take_strict_thm = Goal.prove_global thy [] [] goal (K tac);
   4.339 -      in
   4.340 -        add_qualified_thm "take_strict" (dname, take_strict_thm) thy
   4.341 -      end;
   4.342 -    val (take_strict_thms, thy) =
   4.343 -      fold_map prove_take_strict (take_consts ~~ dnames) thy;
   4.344 -
   4.345 -    (* prove take/take rules *)
   4.346 -    fun prove_take_take ((chain_take, deflation_take), dname) thy =
   4.347 -      let
   4.348 -        val take_take_thm =
   4.349 -            @{thm deflation_chain_min} OF [chain_take, deflation_take];
   4.350 -      in
   4.351 -        add_qualified_thm "take_take" (dname, take_take_thm) thy
   4.352 -      end;
   4.353 -    val (take_take_thms, thy) =
   4.354 -      fold_map prove_take_take
   4.355 -        (chain_take_thms ~~ deflation_take_thms ~~ dnames) thy;
   4.356 -
   4.357 -    val result =
   4.358 -      {
   4.359 -        take_consts = take_consts,
   4.360 -        take_defs = take_defs,
   4.361 -        chain_take_thms = chain_take_thms,
   4.362 -        take_0_thms = take_0_thms,
   4.363 -        take_Suc_thms = take_Suc_thms,
   4.364 -        deflation_take_thms = deflation_take_thms
   4.365 -      };
   4.366 -
   4.367 -  in
   4.368 -    (result, thy)
   4.369 -  end;
   4.370 -
   4.371 -(******************************************************************************)
   4.372  (******************************* main function ********************************)
   4.373  (******************************************************************************)
   4.374  
   4.375 @@ -529,7 +276,7 @@
   4.376      (prep_typ: theory -> 'a -> (string * sort) list -> typ * (string * sort) list)
   4.377      (doms_raw: (string list * binding * mixfix * 'a * (binding * binding) option) list)
   4.378      (thy: theory)
   4.379 -    : iso_info list * theory =
   4.380 +    : Domain_Take_Proofs.iso_info list * theory =
   4.381    let
   4.382      val _ = Theory.requires thy "Representable" "domain isomorphisms";
   4.383  
   4.384 @@ -669,7 +416,7 @@
   4.385        |>> ListPair.unzip;
   4.386  
   4.387      (* collect info about rep/abs *)
   4.388 -    val iso_infos : iso_info list =
   4.389 +    val iso_infos : Domain_Take_Proofs.iso_info list =
   4.390        let
   4.391          fun mk_info (((lhsT, rhsT), (repC, absC)), (rep_iso, abs_iso)) =
   4.392            {
   4.393 @@ -696,19 +443,24 @@
   4.394        fold_map declare_map_const (dom_binds ~~ dom_eqns);
   4.395  
   4.396      (* defining equations for map functions *)
   4.397 -    val map_tab1 = MapData.get thy;
   4.398 -    val map_tab2 =
   4.399 -      Symtab.make (map (fst o dest_Type o fst) dom_eqns
   4.400 -                   ~~ map (fst o dest_Const) map_consts);
   4.401 -    val map_tab' = Symtab.merge (K true) (map_tab1, map_tab2);
   4.402 -    val thy = MapData.put map_tab' thy;
   4.403 -    fun mk_map_spec ((rep_const, abs_const), (lhsT, rhsT)) =
   4.404 -      let
   4.405 -        val lhs = map_of_typ map_tab' lhsT;
   4.406 -        val body = map_of_typ map_tab' rhsT;
   4.407 -        val rhs = mk_cfcomp (abs_const, mk_cfcomp (body, rep_const));
   4.408 -      in mk_eqs (lhs, rhs) end;
   4.409 -    val map_specs = map mk_map_spec (rep_abs_consts ~~ dom_eqns);
   4.410 +    local
   4.411 +      fun unprime a = Library.unprefix "'" a;
   4.412 +      fun mapvar T = Free (unprime (fst (dest_TFree T)), T ->> T);
   4.413 +      fun map_lhs (map_const, lhsT) =
   4.414 +          (lhsT, list_ccomb (map_const, map mapvar (snd (dest_Type lhsT))));
   4.415 +      val tab1 = map map_lhs (map_consts ~~ map fst dom_eqns);
   4.416 +      val Ts = (snd o dest_Type o fst o hd) dom_eqns;
   4.417 +      val tab = (Ts ~~ map mapvar Ts) @ tab1;
   4.418 +      fun mk_map_spec (((rep_const, abs_const), map_const), (lhsT, rhsT)) =
   4.419 +        let
   4.420 +          val lhs = Domain_Take_Proofs.map_of_typ thy tab lhsT;
   4.421 +          val body = Domain_Take_Proofs.map_of_typ thy tab rhsT;
   4.422 +          val rhs = mk_cfcomp (abs_const, mk_cfcomp (body, rep_const));
   4.423 +        in mk_eqs (lhs, rhs) end;
   4.424 +    in
   4.425 +      val map_specs =
   4.426 +          map mk_map_spec (rep_abs_consts ~~ map_consts ~~ dom_eqns);
   4.427 +    end;
   4.428  
   4.429      (* register recursive definition of map functions *)
   4.430      val map_binds = map (Binding.suffix_name "_map") dom_binds;
   4.431 @@ -816,7 +568,7 @@
   4.432          val deflation_rules =
   4.433            @{thms conjI deflation_ID}
   4.434            @ deflation_abs_rep_thms
   4.435 -          @ DeflMapData.get thy;
   4.436 +          @ Domain_Take_Proofs.get_deflation_thms thy;
   4.437        in
   4.438          Goal.prove_global thy [] assms goal (fn {prems, ...} =>
   4.439           EVERY
   4.440 @@ -834,11 +586,22 @@
   4.441      val (deflation_map_thms, thy) = thy |>
   4.442        (PureThy.add_thms o map (Thm.no_attributes o apsnd Drule.export_without_context))
   4.443          (conjuncts deflation_map_binds deflation_map_thm);
   4.444 -    val thy = DeflMapData.map (fold Thm.add_thm deflation_map_thms) thy;
   4.445 +
   4.446 +    (* register map functions in theory data *)
   4.447 +    local
   4.448 +      fun register_map ((dname, map_name), defl_thm) =
   4.449 +          Domain_Take_Proofs.add_map_function (dname, map_name, defl_thm);
   4.450 +      val dnames = map (fst o dest_Type o fst) dom_eqns;
   4.451 +      val map_names = map (fst o dest_Const) map_consts;
   4.452 +    in
   4.453 +      val thy =
   4.454 +          fold register_map (dnames ~~ map_names ~~ deflation_map_thms) thy;
   4.455 +    end;
   4.456  
   4.457      (* definitions and proofs related to take functions *)
   4.458      val (take_info, thy) =
   4.459 -      define_take_functions (dom_binds ~~ iso_infos) thy;
   4.460 +        Domain_Take_Proofs.define_take_functions
   4.461 +          (dom_binds ~~ iso_infos) thy;
   4.462      val {take_consts, take_defs, chain_take_thms, take_0_thms,
   4.463           take_Suc_thms, deflation_take_thms} = take_info;
   4.464  
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOLCF/Tools/Domain/domain_take_proofs.ML	Tue Mar 02 13:50:23 2010 -0800
     5.3 @@ -0,0 +1,391 @@
     5.4 +(*  Title:      HOLCF/Tools/domain/domain_take_proofs.ML
     5.5 +    Author:     Brian Huffman
     5.6 +
     5.7 +Defines take functions for the given domain equation
     5.8 +and proves related theorems.
     5.9 +*)
    5.10 +
    5.11 +signature DOMAIN_TAKE_PROOFS =
    5.12 +sig
    5.13 +  type iso_info =
    5.14 +    {
    5.15 +      absT : typ,
    5.16 +      repT : typ,
    5.17 +      abs_const : term,
    5.18 +      rep_const : term,
    5.19 +      abs_inverse : thm,
    5.20 +      rep_inverse : thm
    5.21 +    }
    5.22 +
    5.23 +  val define_take_functions :
    5.24 +    (binding * iso_info) list -> theory ->
    5.25 +    { take_consts : term list,
    5.26 +      take_defs : thm list,
    5.27 +      chain_take_thms : thm list,
    5.28 +      take_0_thms : thm list,
    5.29 +      take_Suc_thms : thm list,
    5.30 +      deflation_take_thms : thm list
    5.31 +    } * theory
    5.32 +
    5.33 +  val map_of_typ :
    5.34 +    theory -> (typ * term) list -> typ -> term
    5.35 +
    5.36 +  val add_map_function :
    5.37 +    (string * string * thm) -> theory -> theory
    5.38 +
    5.39 +  val get_map_tab : theory -> string Symtab.table
    5.40 +  val get_deflation_thms : theory -> thm list
    5.41 +end;
    5.42 +
    5.43 +structure Domain_Take_Proofs : DOMAIN_TAKE_PROOFS =
    5.44 +struct
    5.45 +
    5.46 +type iso_info =
    5.47 +  {
    5.48 +    absT : typ,
    5.49 +    repT : typ,
    5.50 +    abs_const : term,
    5.51 +    rep_const : term,
    5.52 +    abs_inverse : thm,
    5.53 +    rep_inverse : thm
    5.54 +  };
    5.55 +
    5.56 +val beta_ss =
    5.57 +  HOL_basic_ss
    5.58 +    addsimps simp_thms
    5.59 +    addsimps [@{thm beta_cfun}]
    5.60 +    addsimprocs [@{simproc cont_proc}];
    5.61 +
    5.62 +val beta_tac = simp_tac beta_ss;
    5.63 +
    5.64 +(******************************************************************************)
    5.65 +(******************************** theory data *********************************)
    5.66 +(******************************************************************************)
    5.67 +
    5.68 +structure MapData = Theory_Data
    5.69 +(
    5.70 +  (* constant names like "foo_map" *)
    5.71 +  type T = string Symtab.table;
    5.72 +  val empty = Symtab.empty;
    5.73 +  val extend = I;
    5.74 +  fun merge data = Symtab.merge (K true) data;
    5.75 +);
    5.76 +
    5.77 +structure DeflMapData = Theory_Data
    5.78 +(
    5.79 +  (* theorems like "deflation a ==> deflation (foo_map$a)" *)
    5.80 +  type T = thm list;
    5.81 +  val empty = [];
    5.82 +  val extend = I;
    5.83 +  val merge = Thm.merge_thms;
    5.84 +);
    5.85 +
    5.86 +fun add_map_function (tname, map_name, deflation_map_thm) =
    5.87 +    MapData.map (Symtab.insert (K true) (tname, map_name))
    5.88 +    #> DeflMapData.map (Thm.add_thm deflation_map_thm);
    5.89 +
    5.90 +val get_map_tab = MapData.get;
    5.91 +val get_deflation_thms = DeflMapData.get;
    5.92 +
    5.93 +(******************************************************************************)
    5.94 +(************************** building types and terms **************************)
    5.95 +(******************************************************************************)
    5.96 +
    5.97 +open HOLCF_Library;
    5.98 +
    5.99 +infixr 6 ->>;
   5.100 +infix -->>;
   5.101 +
   5.102 +val deflT = @{typ "udom alg_defl"};
   5.103 +
   5.104 +fun mapT (T as Type (_, Ts)) =
   5.105 +    (map (fn T => T ->> T) Ts) -->> (T ->> T)
   5.106 +  | mapT T = T ->> T;
   5.107 +
   5.108 +fun mk_Rep_of T =
   5.109 +  Const (@{const_name Rep_of}, Term.itselfT T --> deflT) $ Logic.mk_type T;
   5.110 +
   5.111 +fun coerce_const T = Const (@{const_name coerce}, T);
   5.112 +
   5.113 +fun isodefl_const T =
   5.114 +  Const (@{const_name isodefl}, (T ->> T) --> deflT --> HOLogic.boolT);
   5.115 +
   5.116 +fun mk_deflation t =
   5.117 +  Const (@{const_name deflation}, Term.fastype_of t --> boolT) $ t;
   5.118 +
   5.119 +fun mk_lub t =
   5.120 +  let
   5.121 +    val T = Term.range_type (Term.fastype_of t);
   5.122 +    val lub_const = Const (@{const_name lub}, (T --> boolT) --> T);
   5.123 +    val UNIV_const = @{term "UNIV :: nat set"};
   5.124 +    val image_type = (natT --> T) --> (natT --> boolT) --> T --> boolT;
   5.125 +    val image_const = Const (@{const_name image}, image_type);
   5.126 +  in
   5.127 +    lub_const $ (image_const $ t $ UNIV_const)
   5.128 +  end;
   5.129 +
   5.130 +(* splits a cterm into the right and lefthand sides of equality *)
   5.131 +fun dest_eqs t = HOLogic.dest_eq (HOLogic.dest_Trueprop t);
   5.132 +
   5.133 +fun mk_eqs (t, u) = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u));
   5.134 +
   5.135 +(******************************************************************************)
   5.136 +(****************************** isomorphism info ******************************)
   5.137 +(******************************************************************************)
   5.138 +
   5.139 +fun deflation_abs_rep (info : iso_info) : thm =
   5.140 +  let
   5.141 +    val abs_iso = #abs_inverse info;
   5.142 +    val rep_iso = #rep_inverse info;
   5.143 +    val thm = @{thm deflation_abs_rep} OF [abs_iso, rep_iso];
   5.144 +  in
   5.145 +    Drule.export_without_context thm
   5.146 +  end
   5.147 +
   5.148 +(******************************************************************************)
   5.149 +(********************* building map functions over types **********************)
   5.150 +(******************************************************************************)
   5.151 +
   5.152 +fun map_of_typ (thy : theory) (sub : (typ * term) list) (T : typ) : term =
   5.153 +  let
   5.154 +    val map_tab = get_map_tab thy;
   5.155 +    fun auto T = T ->> T;
   5.156 +    fun map_of T =
   5.157 +        case AList.lookup (op =) sub T of
   5.158 +          SOME m => (m, true) | NONE => map_of' T
   5.159 +    and map_of' (T as (Type (c, Ts))) =
   5.160 +        (case Symtab.lookup map_tab c of
   5.161 +          SOME map_name =>
   5.162 +          let
   5.163 +            val map_type = map auto Ts -->> auto T;
   5.164 +            val (ms, bs) = map_split map_of Ts;
   5.165 +          in
   5.166 +            if exists I bs
   5.167 +            then (list_ccomb (Const (map_name, map_type), ms), true)
   5.168 +            else (mk_ID T, false)
   5.169 +          end
   5.170 +        | NONE => (mk_ID T, false))
   5.171 +      | map_of' T = (mk_ID T, false);
   5.172 +  in
   5.173 +    fst (map_of T)
   5.174 +  end;
   5.175 +
   5.176 +
   5.177 +(******************************************************************************)
   5.178 +(********************* declaring definitions and theorems *********************)
   5.179 +(******************************************************************************)
   5.180 +
   5.181 +fun define_const
   5.182 +    (bind : binding, rhs : term)
   5.183 +    (thy : theory)
   5.184 +    : (term * thm) * theory =
   5.185 +  let
   5.186 +    val typ = Term.fastype_of rhs;
   5.187 +    val (const, thy) = Sign.declare_const ((bind, typ), NoSyn) thy;
   5.188 +    val eqn = Logic.mk_equals (const, rhs);
   5.189 +    val def = Thm.no_attributes (Binding.suffix_name "_def" bind, eqn);
   5.190 +    val (def_thm, thy) = yield_singleton (PureThy.add_defs false) def thy;
   5.191 +  in
   5.192 +    ((const, def_thm), thy)
   5.193 +  end;
   5.194 +
   5.195 +fun add_qualified_thm name (path, thm) thy =
   5.196 +    thy
   5.197 +    |> Sign.add_path path
   5.198 +    |> yield_singleton PureThy.add_thms
   5.199 +        (Thm.no_attributes (Binding.name name, thm))
   5.200 +    ||> Sign.parent_path;
   5.201 +
   5.202 +(******************************************************************************)
   5.203 +(************************** defining take functions ***************************)
   5.204 +(******************************************************************************)
   5.205 +
   5.206 +fun define_take_functions
   5.207 +    (spec : (binding * iso_info) list)
   5.208 +    (thy : theory) =
   5.209 +  let
   5.210 +
   5.211 +    (* retrieve components of spec *)
   5.212 +    val dom_binds = map fst spec;
   5.213 +    val iso_infos = map snd spec;
   5.214 +    val dom_eqns = map (fn x => (#absT x, #repT x)) iso_infos;
   5.215 +    val rep_abs_consts = map (fn x => (#rep_const x, #abs_const x)) iso_infos;
   5.216 +    val dnames = map Binding.name_of dom_binds;
   5.217 +
   5.218 +    (* get table of map functions *)
   5.219 +    val map_tab = MapData.get thy;
   5.220 +
   5.221 +    fun mk_projs []      t = []
   5.222 +      | mk_projs (x::[]) t = [(x, t)]
   5.223 +      | mk_projs (x::xs) t = (x, mk_fst t) :: mk_projs xs (mk_snd t);
   5.224 +
   5.225 +    fun mk_cfcomp2 ((rep_const, abs_const), f) =
   5.226 +        mk_cfcomp (abs_const, mk_cfcomp (f, rep_const));
   5.227 +
   5.228 +    (* define take functional *)
   5.229 +    val newTs : typ list = map fst dom_eqns;
   5.230 +    val copy_arg_type = mk_tupleT (map (fn T => T ->> T) newTs);
   5.231 +    val copy_arg = Free ("f", copy_arg_type);
   5.232 +    val copy_args = map snd (mk_projs dom_binds copy_arg);
   5.233 +    fun one_copy_rhs (rep_abs, (lhsT, rhsT)) =
   5.234 +      let
   5.235 +        val body = map_of_typ thy (newTs ~~ copy_args) rhsT;
   5.236 +      in
   5.237 +        mk_cfcomp2 (rep_abs, body)
   5.238 +      end;
   5.239 +    val take_functional =
   5.240 +        big_lambda copy_arg
   5.241 +          (mk_tuple (map one_copy_rhs (rep_abs_consts ~~ dom_eqns)));
   5.242 +    val take_rhss =
   5.243 +      let
   5.244 +        val i = Free ("i", HOLogic.natT);
   5.245 +        val rhs = mk_iterate (i, take_functional)
   5.246 +      in
   5.247 +        map (Term.lambda i o snd) (mk_projs dom_binds rhs)
   5.248 +      end;
   5.249 +
   5.250 +    (* define take constants *)
   5.251 +    fun define_take_const ((tbind, take_rhs), (lhsT, rhsT)) thy =
   5.252 +      let
   5.253 +        val take_type = HOLogic.natT --> lhsT ->> lhsT;
   5.254 +        val take_bind = Binding.suffix_name "_take" tbind;
   5.255 +        val (take_const, thy) =
   5.256 +          Sign.declare_const ((take_bind, take_type), NoSyn) thy;
   5.257 +        val take_eqn = Logic.mk_equals (take_const, take_rhs);
   5.258 +        val (take_def_thm, thy) =
   5.259 +          thy
   5.260 +          |> Sign.add_path (Binding.name_of tbind)
   5.261 +          |> yield_singleton
   5.262 +              (PureThy.add_defs false o map Thm.no_attributes)
   5.263 +              (Binding.name "take_def", take_eqn)
   5.264 +          ||> Sign.parent_path;
   5.265 +      in ((take_const, take_def_thm), thy) end;
   5.266 +    val ((take_consts, take_defs), thy) = thy
   5.267 +      |> fold_map define_take_const (dom_binds ~~ take_rhss ~~ dom_eqns)
   5.268 +      |>> ListPair.unzip;
   5.269 +
   5.270 +    (* prove chain_take lemmas *)
   5.271 +    fun prove_chain_take (take_const, dname) thy =
   5.272 +      let
   5.273 +        val goal = mk_trp (mk_chain take_const);
   5.274 +        val rules = take_defs @ @{thms chain_iterate ch2ch_fst ch2ch_snd};
   5.275 +        val tac = simp_tac (HOL_basic_ss addsimps rules) 1;
   5.276 +        val chain_take_thm = Goal.prove_global thy [] [] goal (K tac);
   5.277 +      in
   5.278 +        add_qualified_thm "chain_take" (dname, chain_take_thm) thy
   5.279 +      end;
   5.280 +    val (chain_take_thms, thy) =
   5.281 +      fold_map prove_chain_take (take_consts ~~ dnames) thy;
   5.282 +
   5.283 +    (* prove take_0 lemmas *)
   5.284 +    fun prove_take_0 ((take_const, dname), (lhsT, rhsT)) thy =
   5.285 +      let
   5.286 +        val lhs = take_const $ @{term "0::nat"};
   5.287 +        val goal = mk_eqs (lhs, mk_bottom (lhsT ->> lhsT));
   5.288 +        val rules = take_defs @ @{thms iterate_0 fst_strict snd_strict};
   5.289 +        val tac = simp_tac (HOL_basic_ss addsimps rules) 1;
   5.290 +        val take_0_thm = Goal.prove_global thy [] [] goal (K tac);
   5.291 +      in
   5.292 +        add_qualified_thm "take_0" (dname, take_0_thm) thy
   5.293 +      end;
   5.294 +    val (take_0_thms, thy) =
   5.295 +      fold_map prove_take_0 (take_consts ~~ dnames ~~ dom_eqns) thy;
   5.296 +
   5.297 +    (* prove take_Suc lemmas *)
   5.298 +    val i = Free ("i", natT);
   5.299 +    val take_is = map (fn t => t $ i) take_consts;
   5.300 +    fun prove_take_Suc
   5.301 +          (((take_const, rep_abs), dname), (lhsT, rhsT)) thy =
   5.302 +      let
   5.303 +        val lhs = take_const $ (@{term Suc} $ i);
   5.304 +        val body = map_of_typ thy (newTs ~~ take_is) rhsT;
   5.305 +        val rhs = mk_cfcomp2 (rep_abs, body);
   5.306 +        val goal = mk_eqs (lhs, rhs);
   5.307 +        val simps = @{thms iterate_Suc fst_conv snd_conv}
   5.308 +        val rules = take_defs @ simps;
   5.309 +        val tac = simp_tac (beta_ss addsimps rules) 1;
   5.310 +        val take_Suc_thm = Goal.prove_global thy [] [] goal (K tac);
   5.311 +      in
   5.312 +        add_qualified_thm "take_Suc" (dname, take_Suc_thm) thy
   5.313 +      end;
   5.314 +    val (take_Suc_thms, thy) =
   5.315 +      fold_map prove_take_Suc
   5.316 +        (take_consts ~~ rep_abs_consts ~~ dnames ~~ dom_eqns) thy;
   5.317 +
   5.318 +    (* prove deflation theorems for take functions *)
   5.319 +    val deflation_abs_rep_thms = map deflation_abs_rep iso_infos;
   5.320 +    val deflation_take_thm =
   5.321 +      let
   5.322 +        val i = Free ("i", natT);
   5.323 +        fun mk_goal take_const = mk_deflation (take_const $ i);
   5.324 +        val goal = mk_trp (foldr1 mk_conj (map mk_goal take_consts));
   5.325 +        val adm_rules =
   5.326 +          @{thms adm_conj adm_subst [OF _ adm_deflation]
   5.327 +                 cont2cont_fst cont2cont_snd cont_id};
   5.328 +        val bottom_rules =
   5.329 +          take_0_thms @ @{thms deflation_UU simp_thms};
   5.330 +        val deflation_rules =
   5.331 +          @{thms conjI deflation_ID}
   5.332 +          @ deflation_abs_rep_thms
   5.333 +          @ DeflMapData.get thy;
   5.334 +      in
   5.335 +        Goal.prove_global thy [] [] goal (fn _ =>
   5.336 +         EVERY
   5.337 +          [rtac @{thm nat.induct} 1,
   5.338 +           simp_tac (HOL_basic_ss addsimps bottom_rules) 1,
   5.339 +           asm_simp_tac (HOL_basic_ss addsimps take_Suc_thms) 1,
   5.340 +           REPEAT (etac @{thm conjE} 1
   5.341 +                   ORELSE resolve_tac deflation_rules 1
   5.342 +                   ORELSE atac 1)])
   5.343 +      end;
   5.344 +    fun conjuncts [] thm = []
   5.345 +      | conjuncts (n::[]) thm = [(n, thm)]
   5.346 +      | conjuncts (n::ns) thm = let
   5.347 +          val thmL = thm RS @{thm conjunct1};
   5.348 +          val thmR = thm RS @{thm conjunct2};
   5.349 +        in (n, thmL):: conjuncts ns thmR end;
   5.350 +    val (deflation_take_thms, thy) =
   5.351 +      fold_map (add_qualified_thm "deflation_take")
   5.352 +        (map (apsnd Drule.export_without_context)
   5.353 +          (conjuncts dnames deflation_take_thm)) thy;
   5.354 +
   5.355 +    (* prove strictness of take functions *)
   5.356 +    fun prove_take_strict (take_const, dname) thy =
   5.357 +      let
   5.358 +        val goal = mk_trp (mk_strict (take_const $ Free ("i", natT)));
   5.359 +        val tac = rtac @{thm deflation_strict} 1
   5.360 +                  THEN resolve_tac deflation_take_thms 1;
   5.361 +        val take_strict_thm = Goal.prove_global thy [] [] goal (K tac);
   5.362 +      in
   5.363 +        add_qualified_thm "take_strict" (dname, take_strict_thm) thy
   5.364 +      end;
   5.365 +    val (take_strict_thms, thy) =
   5.366 +      fold_map prove_take_strict (take_consts ~~ dnames) thy;
   5.367 +
   5.368 +    (* prove take/take rules *)
   5.369 +    fun prove_take_take ((chain_take, deflation_take), dname) thy =
   5.370 +      let
   5.371 +        val take_take_thm =
   5.372 +            @{thm deflation_chain_min} OF [chain_take, deflation_take];
   5.373 +      in
   5.374 +        add_qualified_thm "take_take" (dname, take_take_thm) thy
   5.375 +      end;
   5.376 +    val (take_take_thms, thy) =
   5.377 +      fold_map prove_take_take
   5.378 +        (chain_take_thms ~~ deflation_take_thms ~~ dnames) thy;
   5.379 +
   5.380 +    val result =
   5.381 +      {
   5.382 +        take_consts = take_consts,
   5.383 +        take_defs = take_defs,
   5.384 +        chain_take_thms = chain_take_thms,
   5.385 +        take_0_thms = take_0_thms,
   5.386 +        take_Suc_thms = take_Suc_thms,
   5.387 +        deflation_take_thms = deflation_take_thms
   5.388 +      };
   5.389 +
   5.390 +  in
   5.391 +    (result, thy)
   5.392 +  end;
   5.393 +
   5.394 +end;
     6.1 --- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Tue Mar 02 13:01:22 2010 -0800
     6.2 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Tue Mar 02 13:50:23 2010 -0800
     6.3 @@ -106,7 +106,7 @@
     6.4  let
     6.5  
     6.6  val _ = message ("Proving isomorphism properties of domain "^dname^" ...");
     6.7 -val map_tab = Domain_Isomorphism.get_map_tab thy;
     6.8 +val map_tab = Domain_Take_Proofs.get_map_tab thy;
     6.9  
    6.10  
    6.11  (* ----- getting the axioms and definitions --------------------------------- *)
    6.12 @@ -139,7 +139,7 @@
    6.13  
    6.14  val abs_const = Const(dname^"_abs", rhsT ->> lhsT);
    6.15  
    6.16 -val iso_info : Domain_Isomorphism.iso_info =
    6.17 +val iso_info : Domain_Take_Proofs.iso_info =
    6.18    {
    6.19      absT = lhsT,
    6.20      repT = rhsT,
    6.21 @@ -229,7 +229,7 @@
    6.22  
    6.23  fun comp_theorems (comp_dnam, eqs: eq list) thy =
    6.24  let
    6.25 -val map_tab = Domain_Isomorphism.get_map_tab thy;
    6.26 +val map_tab = Domain_Take_Proofs.get_map_tab thy;
    6.27  
    6.28  val dnames = map (fst o fst) eqs;
    6.29  val conss  = map  snd        eqs;