src/HOLCF/Tools/Domain/domain_take_proofs.ML
changeset 40774 0437dbc127b3
parent 40773 6c12f5e24e34
child 40775 ed7a4eadb2f6
     1.1 --- a/src/HOLCF/Tools/Domain/domain_take_proofs.ML	Sat Nov 27 14:34:54 2010 -0800
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,609 +0,0 @@
     1.4 -(*  Title:      HOLCF/Tools/Domain/domain_take_proofs.ML
     1.5 -    Author:     Brian Huffman
     1.6 -
     1.7 -Defines take functions for the given domain equation
     1.8 -and proves related theorems.
     1.9 -*)
    1.10 -
    1.11 -signature DOMAIN_TAKE_PROOFS =
    1.12 -sig
    1.13 -  type iso_info =
    1.14 -    {
    1.15 -      absT : typ,
    1.16 -      repT : typ,
    1.17 -      abs_const : term,
    1.18 -      rep_const : term,
    1.19 -      abs_inverse : thm,
    1.20 -      rep_inverse : thm
    1.21 -    }
    1.22 -  type take_info =
    1.23 -    {
    1.24 -      take_consts : term list,
    1.25 -      take_defs : thm list,
    1.26 -      chain_take_thms : thm list,
    1.27 -      take_0_thms : thm list,
    1.28 -      take_Suc_thms : thm list,
    1.29 -      deflation_take_thms : thm list,
    1.30 -      take_strict_thms : thm list,
    1.31 -      finite_consts : term list,
    1.32 -      finite_defs : thm list
    1.33 -    }
    1.34 -  type take_induct_info =
    1.35 -    {
    1.36 -      take_consts         : term list,
    1.37 -      take_defs           : thm list,
    1.38 -      chain_take_thms     : thm list,
    1.39 -      take_0_thms         : thm list,
    1.40 -      take_Suc_thms       : thm list,
    1.41 -      deflation_take_thms : thm list,
    1.42 -      take_strict_thms    : thm list,
    1.43 -      finite_consts       : term list,
    1.44 -      finite_defs         : thm list,
    1.45 -      lub_take_thms       : thm list,
    1.46 -      reach_thms          : thm list,
    1.47 -      take_lemma_thms     : thm list,
    1.48 -      is_finite           : bool,
    1.49 -      take_induct_thms    : thm list
    1.50 -    }
    1.51 -  val define_take_functions :
    1.52 -    (binding * iso_info) list -> theory -> take_info * theory
    1.53 -
    1.54 -  val add_lub_take_theorems :
    1.55 -    (binding * iso_info) list -> take_info -> thm list ->
    1.56 -    theory -> take_induct_info * theory
    1.57 -
    1.58 -  val map_of_typ :
    1.59 -    theory -> (typ * term) list -> typ -> term
    1.60 -
    1.61 -  val add_rec_type : (string * bool list) -> theory -> theory
    1.62 -  val get_rec_tab : theory -> (bool list) Symtab.table
    1.63 -  val add_deflation_thm : thm -> theory -> theory
    1.64 -  val get_deflation_thms : theory -> thm list
    1.65 -  val map_ID_add : attribute
    1.66 -  val get_map_ID_thms : theory -> thm list
    1.67 -  val setup : theory -> theory
    1.68 -end;
    1.69 -
    1.70 -structure Domain_Take_Proofs : DOMAIN_TAKE_PROOFS =
    1.71 -struct
    1.72 -
    1.73 -type iso_info =
    1.74 -  {
    1.75 -    absT : typ,
    1.76 -    repT : typ,
    1.77 -    abs_const : term,
    1.78 -    rep_const : term,
    1.79 -    abs_inverse : thm,
    1.80 -    rep_inverse : thm
    1.81 -  };
    1.82 -
    1.83 -type take_info =
    1.84 -  { take_consts : term list,
    1.85 -    take_defs : thm list,
    1.86 -    chain_take_thms : thm list,
    1.87 -    take_0_thms : thm list,
    1.88 -    take_Suc_thms : thm list,
    1.89 -    deflation_take_thms : thm list,
    1.90 -    take_strict_thms : thm list,
    1.91 -    finite_consts : term list,
    1.92 -    finite_defs : thm list
    1.93 -  };
    1.94 -
    1.95 -type take_induct_info =
    1.96 -  {
    1.97 -    take_consts         : term list,
    1.98 -    take_defs           : thm list,
    1.99 -    chain_take_thms     : thm list,
   1.100 -    take_0_thms         : thm list,
   1.101 -    take_Suc_thms       : thm list,
   1.102 -    deflation_take_thms : thm list,
   1.103 -    take_strict_thms    : thm list,
   1.104 -    finite_consts       : term list,
   1.105 -    finite_defs         : thm list,
   1.106 -    lub_take_thms       : thm list,
   1.107 -    reach_thms          : thm list,
   1.108 -    take_lemma_thms     : thm list,
   1.109 -    is_finite           : bool,
   1.110 -    take_induct_thms    : thm list
   1.111 -  };
   1.112 -
   1.113 -val beta_rules =
   1.114 -  @{thms beta_cfun cont_id cont_const cont2cont_APP cont2cont_LAM'} @
   1.115 -  @{thms cont2cont_fst cont2cont_snd cont2cont_Pair};
   1.116 -
   1.117 -val beta_ss = HOL_basic_ss addsimps (simp_thms @ beta_rules);
   1.118 -
   1.119 -val beta_tac = simp_tac beta_ss;
   1.120 -
   1.121 -(******************************************************************************)
   1.122 -(******************************** theory data *********************************)
   1.123 -(******************************************************************************)
   1.124 -
   1.125 -structure Rec_Data = Theory_Data
   1.126 -(
   1.127 -  (* list indicates which type arguments allow indirect recursion *)
   1.128 -  type T = (bool list) Symtab.table;
   1.129 -  val empty = Symtab.empty;
   1.130 -  val extend = I;
   1.131 -  fun merge data = Symtab.merge (K true) data;
   1.132 -);
   1.133 -
   1.134 -structure DeflMapData = Named_Thms
   1.135 -(
   1.136 -  val name = "domain_deflation"
   1.137 -  val description = "theorems like deflation a ==> deflation (foo_map$a)"
   1.138 -);
   1.139 -
   1.140 -structure Map_Id_Data = Named_Thms
   1.141 -(
   1.142 -  val name = "domain_map_ID"
   1.143 -  val description = "theorems like foo_map$ID = ID"
   1.144 -);
   1.145 -
   1.146 -fun add_rec_type (tname, bs) =
   1.147 -    Rec_Data.map (Symtab.insert (K true) (tname, bs));
   1.148 -
   1.149 -fun add_deflation_thm thm =
   1.150 -    Context.theory_map (DeflMapData.add_thm thm);
   1.151 -
   1.152 -val get_rec_tab = Rec_Data.get;
   1.153 -fun get_deflation_thms thy = DeflMapData.get (ProofContext.init_global thy);
   1.154 -
   1.155 -val map_ID_add = Map_Id_Data.add;
   1.156 -val get_map_ID_thms = Map_Id_Data.get o ProofContext.init_global;
   1.157 -
   1.158 -val setup = DeflMapData.setup #> Map_Id_Data.setup;
   1.159 -
   1.160 -(******************************************************************************)
   1.161 -(************************** building types and terms **************************)
   1.162 -(******************************************************************************)
   1.163 -
   1.164 -open HOLCF_Library;
   1.165 -
   1.166 -infixr 6 ->>;
   1.167 -infix -->>;
   1.168 -infix 9 `;
   1.169 -
   1.170 -fun mapT (T as Type (_, Ts)) =
   1.171 -    (map (fn T => T ->> T) Ts) -->> (T ->> T)
   1.172 -  | mapT T = T ->> T;
   1.173 -
   1.174 -fun mk_deflation t =
   1.175 -  Const (@{const_name deflation}, Term.fastype_of t --> boolT) $ t;
   1.176 -
   1.177 -fun mk_eqs (t, u) = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u));
   1.178 -
   1.179 -(******************************************************************************)
   1.180 -(****************************** isomorphism info ******************************)
   1.181 -(******************************************************************************)
   1.182 -
   1.183 -fun deflation_abs_rep (info : iso_info) : thm =
   1.184 -  let
   1.185 -    val abs_iso = #abs_inverse info;
   1.186 -    val rep_iso = #rep_inverse info;
   1.187 -    val thm = @{thm deflation_abs_rep} OF [abs_iso, rep_iso];
   1.188 -  in
   1.189 -    Drule.zero_var_indexes thm
   1.190 -  end
   1.191 -
   1.192 -(******************************************************************************)
   1.193 -(********************* building map functions over types **********************)
   1.194 -(******************************************************************************)
   1.195 -
   1.196 -fun map_of_typ (thy : theory) (sub : (typ * term) list) (T : typ) : term =
   1.197 -  let
   1.198 -    val thms = get_map_ID_thms thy;
   1.199 -    val rules = map (Thm.concl_of #> HOLogic.dest_Trueprop #> HOLogic.dest_eq) thms;
   1.200 -    val rules' = map (apfst mk_ID) sub @ map swap rules;
   1.201 -  in
   1.202 -    mk_ID T
   1.203 -    |> Pattern.rewrite_term thy rules' []
   1.204 -    |> Pattern.rewrite_term thy rules []
   1.205 -  end;
   1.206 -
   1.207 -(******************************************************************************)
   1.208 -(********************* declaring definitions and theorems *********************)
   1.209 -(******************************************************************************)
   1.210 -
   1.211 -fun add_qualified_def name (dbind, eqn) =
   1.212 -    yield_singleton (Global_Theory.add_defs false)
   1.213 -     ((Binding.qualified true name dbind, eqn), []);
   1.214 -
   1.215 -fun add_qualified_thm name (dbind, thm) =
   1.216 -    yield_singleton Global_Theory.add_thms
   1.217 -      ((Binding.qualified true name dbind, thm), []);
   1.218 -
   1.219 -fun add_qualified_simp_thm name (dbind, thm) =
   1.220 -    yield_singleton Global_Theory.add_thms
   1.221 -      ((Binding.qualified true name dbind, thm), [Simplifier.simp_add]);
   1.222 -
   1.223 -(******************************************************************************)
   1.224 -(************************** defining take functions ***************************)
   1.225 -(******************************************************************************)
   1.226 -
   1.227 -fun define_take_functions
   1.228 -    (spec : (binding * iso_info) list)
   1.229 -    (thy : theory) =
   1.230 -  let
   1.231 -
   1.232 -    (* retrieve components of spec *)
   1.233 -    val dbinds = map fst spec;
   1.234 -    val iso_infos = map snd spec;
   1.235 -    val dom_eqns = map (fn x => (#absT x, #repT x)) iso_infos;
   1.236 -    val rep_abs_consts = map (fn x => (#rep_const x, #abs_const x)) iso_infos;
   1.237 -
   1.238 -    fun mk_projs []      t = []
   1.239 -      | mk_projs (x::[]) t = [(x, t)]
   1.240 -      | mk_projs (x::xs) t = (x, mk_fst t) :: mk_projs xs (mk_snd t);
   1.241 -
   1.242 -    fun mk_cfcomp2 ((rep_const, abs_const), f) =
   1.243 -        mk_cfcomp (abs_const, mk_cfcomp (f, rep_const));
   1.244 -
   1.245 -    (* define take functional *)
   1.246 -    val newTs : typ list = map fst dom_eqns;
   1.247 -    val copy_arg_type = mk_tupleT (map (fn T => T ->> T) newTs);
   1.248 -    val copy_arg = Free ("f", copy_arg_type);
   1.249 -    val copy_args = map snd (mk_projs dbinds copy_arg);
   1.250 -    fun one_copy_rhs (rep_abs, (lhsT, rhsT)) =
   1.251 -      let
   1.252 -        val body = map_of_typ thy (newTs ~~ copy_args) rhsT;
   1.253 -      in
   1.254 -        mk_cfcomp2 (rep_abs, body)
   1.255 -      end;
   1.256 -    val take_functional =
   1.257 -        big_lambda copy_arg
   1.258 -          (mk_tuple (map one_copy_rhs (rep_abs_consts ~~ dom_eqns)));
   1.259 -    val take_rhss =
   1.260 -      let
   1.261 -        val n = Free ("n", HOLogic.natT);
   1.262 -        val rhs = mk_iterate (n, take_functional);
   1.263 -      in
   1.264 -        map (lambda n o snd) (mk_projs dbinds rhs)
   1.265 -      end;
   1.266 -
   1.267 -    (* define take constants *)
   1.268 -    fun define_take_const ((dbind, take_rhs), (lhsT, rhsT)) thy =
   1.269 -      let
   1.270 -        val take_type = HOLogic.natT --> lhsT ->> lhsT;
   1.271 -        val take_bind = Binding.suffix_name "_take" dbind;
   1.272 -        val (take_const, thy) =
   1.273 -          Sign.declare_const ((take_bind, take_type), NoSyn) thy;
   1.274 -        val take_eqn = Logic.mk_equals (take_const, take_rhs);
   1.275 -        val (take_def_thm, thy) =
   1.276 -            add_qualified_def "take_def" (dbind, take_eqn) thy;
   1.277 -      in ((take_const, take_def_thm), thy) end;
   1.278 -    val ((take_consts, take_defs), thy) = thy
   1.279 -      |> fold_map define_take_const (dbinds ~~ take_rhss ~~ dom_eqns)
   1.280 -      |>> ListPair.unzip;
   1.281 -
   1.282 -    (* prove chain_take lemmas *)
   1.283 -    fun prove_chain_take (take_const, dbind) thy =
   1.284 -      let
   1.285 -        val goal = mk_trp (mk_chain take_const);
   1.286 -        val rules = take_defs @ @{thms chain_iterate ch2ch_fst ch2ch_snd};
   1.287 -        val tac = simp_tac (HOL_basic_ss addsimps rules) 1;
   1.288 -        val thm = Goal.prove_global thy [] [] goal (K tac);
   1.289 -      in
   1.290 -        add_qualified_simp_thm "chain_take" (dbind, thm) thy
   1.291 -      end;
   1.292 -    val (chain_take_thms, thy) =
   1.293 -      fold_map prove_chain_take (take_consts ~~ dbinds) thy;
   1.294 -
   1.295 -    (* prove take_0 lemmas *)
   1.296 -    fun prove_take_0 ((take_const, dbind), (lhsT, rhsT)) thy =
   1.297 -      let
   1.298 -        val lhs = take_const $ @{term "0::nat"};
   1.299 -        val goal = mk_eqs (lhs, mk_bottom (lhsT ->> lhsT));
   1.300 -        val rules = take_defs @ @{thms iterate_0 fst_strict snd_strict};
   1.301 -        val tac = simp_tac (HOL_basic_ss addsimps rules) 1;
   1.302 -        val take_0_thm = Goal.prove_global thy [] [] goal (K tac);
   1.303 -      in
   1.304 -        add_qualified_simp_thm "take_0" (dbind, take_0_thm) thy
   1.305 -      end;
   1.306 -    val (take_0_thms, thy) =
   1.307 -      fold_map prove_take_0 (take_consts ~~ dbinds ~~ dom_eqns) thy;
   1.308 -
   1.309 -    (* prove take_Suc lemmas *)
   1.310 -    val n = Free ("n", natT);
   1.311 -    val take_is = map (fn t => t $ n) take_consts;
   1.312 -    fun prove_take_Suc
   1.313 -          (((take_const, rep_abs), dbind), (lhsT, rhsT)) thy =
   1.314 -      let
   1.315 -        val lhs = take_const $ (@{term Suc} $ n);
   1.316 -        val body = map_of_typ thy (newTs ~~ take_is) rhsT;
   1.317 -        val rhs = mk_cfcomp2 (rep_abs, body);
   1.318 -        val goal = mk_eqs (lhs, rhs);
   1.319 -        val simps = @{thms iterate_Suc fst_conv snd_conv}
   1.320 -        val rules = take_defs @ simps;
   1.321 -        val tac = simp_tac (beta_ss addsimps rules) 1;
   1.322 -        val take_Suc_thm = Goal.prove_global thy [] [] goal (K tac);
   1.323 -      in
   1.324 -        add_qualified_thm "take_Suc" (dbind, take_Suc_thm) thy
   1.325 -      end;
   1.326 -    val (take_Suc_thms, thy) =
   1.327 -      fold_map prove_take_Suc
   1.328 -        (take_consts ~~ rep_abs_consts ~~ dbinds ~~ dom_eqns) thy;
   1.329 -
   1.330 -    (* prove deflation theorems for take functions *)
   1.331 -    val deflation_abs_rep_thms = map deflation_abs_rep iso_infos;
   1.332 -    val deflation_take_thm =
   1.333 -      let
   1.334 -        val n = Free ("n", natT);
   1.335 -        fun mk_goal take_const = mk_deflation (take_const $ n);
   1.336 -        val goal = mk_trp (foldr1 mk_conj (map mk_goal take_consts));
   1.337 -        val adm_rules =
   1.338 -          @{thms adm_conj adm_subst [OF _ adm_deflation]
   1.339 -                 cont2cont_fst cont2cont_snd cont_id};
   1.340 -        val bottom_rules =
   1.341 -          take_0_thms @ @{thms deflation_UU simp_thms};
   1.342 -        val deflation_rules =
   1.343 -          @{thms conjI deflation_ID}
   1.344 -          @ deflation_abs_rep_thms
   1.345 -          @ get_deflation_thms thy;
   1.346 -      in
   1.347 -        Goal.prove_global thy [] [] goal (fn _ =>
   1.348 -         EVERY
   1.349 -          [rtac @{thm nat.induct} 1,
   1.350 -           simp_tac (HOL_basic_ss addsimps bottom_rules) 1,
   1.351 -           asm_simp_tac (HOL_basic_ss addsimps take_Suc_thms) 1,
   1.352 -           REPEAT (etac @{thm conjE} 1
   1.353 -                   ORELSE resolve_tac deflation_rules 1
   1.354 -                   ORELSE atac 1)])
   1.355 -      end;
   1.356 -    fun conjuncts [] thm = []
   1.357 -      | conjuncts (n::[]) thm = [(n, thm)]
   1.358 -      | conjuncts (n::ns) thm = let
   1.359 -          val thmL = thm RS @{thm conjunct1};
   1.360 -          val thmR = thm RS @{thm conjunct2};
   1.361 -        in (n, thmL):: conjuncts ns thmR end;
   1.362 -    val (deflation_take_thms, thy) =
   1.363 -      fold_map (add_qualified_thm "deflation_take")
   1.364 -        (map (apsnd Drule.zero_var_indexes)
   1.365 -          (conjuncts dbinds deflation_take_thm)) thy;
   1.366 -
   1.367 -    (* prove strictness of take functions *)
   1.368 -    fun prove_take_strict (deflation_take, dbind) thy =
   1.369 -      let
   1.370 -        val take_strict_thm =
   1.371 -            Drule.zero_var_indexes
   1.372 -              (@{thm deflation_strict} OF [deflation_take]);
   1.373 -      in
   1.374 -        add_qualified_simp_thm "take_strict" (dbind, take_strict_thm) thy
   1.375 -      end;
   1.376 -    val (take_strict_thms, thy) =
   1.377 -      fold_map prove_take_strict
   1.378 -        (deflation_take_thms ~~ dbinds) thy;
   1.379 -
   1.380 -    (* prove take/take rules *)
   1.381 -    fun prove_take_take ((chain_take, deflation_take), dbind) thy =
   1.382 -      let
   1.383 -        val take_take_thm =
   1.384 -            Drule.zero_var_indexes
   1.385 -              (@{thm deflation_chain_min} OF [chain_take, deflation_take]);
   1.386 -      in
   1.387 -        add_qualified_thm "take_take" (dbind, take_take_thm) thy
   1.388 -      end;
   1.389 -    val (take_take_thms, thy) =
   1.390 -      fold_map prove_take_take
   1.391 -        (chain_take_thms ~~ deflation_take_thms ~~ dbinds) thy;
   1.392 -
   1.393 -    (* prove take_below rules *)
   1.394 -    fun prove_take_below (deflation_take, dbind) thy =
   1.395 -      let
   1.396 -        val take_below_thm =
   1.397 -            Drule.zero_var_indexes
   1.398 -              (@{thm deflation.below} OF [deflation_take]);
   1.399 -      in
   1.400 -        add_qualified_thm "take_below" (dbind, take_below_thm) thy
   1.401 -      end;
   1.402 -    val (take_below_thms, thy) =
   1.403 -      fold_map prove_take_below
   1.404 -        (deflation_take_thms ~~ dbinds) thy;
   1.405 -
   1.406 -    (* define finiteness predicates *)
   1.407 -    fun define_finite_const ((dbind, take_const), (lhsT, rhsT)) thy =
   1.408 -      let
   1.409 -        val finite_type = lhsT --> boolT;
   1.410 -        val finite_bind = Binding.suffix_name "_finite" dbind;
   1.411 -        val (finite_const, thy) =
   1.412 -          Sign.declare_const ((finite_bind, finite_type), NoSyn) thy;
   1.413 -        val x = Free ("x", lhsT);
   1.414 -        val n = Free ("n", natT);
   1.415 -        val finite_rhs =
   1.416 -          lambda x (HOLogic.exists_const natT $
   1.417 -            (lambda n (mk_eq (mk_capply (take_const $ n, x), x))));
   1.418 -        val finite_eqn = Logic.mk_equals (finite_const, finite_rhs);
   1.419 -        val (finite_def_thm, thy) =
   1.420 -            add_qualified_def "finite_def" (dbind, finite_eqn) thy;
   1.421 -      in ((finite_const, finite_def_thm), thy) end;
   1.422 -    val ((finite_consts, finite_defs), thy) = thy
   1.423 -      |> fold_map define_finite_const (dbinds ~~ take_consts ~~ dom_eqns)
   1.424 -      |>> ListPair.unzip;
   1.425 -
   1.426 -    val result =
   1.427 -      {
   1.428 -        take_consts = take_consts,
   1.429 -        take_defs = take_defs,
   1.430 -        chain_take_thms = chain_take_thms,
   1.431 -        take_0_thms = take_0_thms,
   1.432 -        take_Suc_thms = take_Suc_thms,
   1.433 -        deflation_take_thms = deflation_take_thms,
   1.434 -        take_strict_thms = take_strict_thms,
   1.435 -        finite_consts = finite_consts,
   1.436 -        finite_defs = finite_defs
   1.437 -      };
   1.438 -
   1.439 -  in
   1.440 -    (result, thy)
   1.441 -  end;
   1.442 -
   1.443 -fun prove_finite_take_induct
   1.444 -    (spec : (binding * iso_info) list)
   1.445 -    (take_info : take_info)
   1.446 -    (lub_take_thms : thm list)
   1.447 -    (thy : theory) =
   1.448 -  let
   1.449 -    val dbinds = map fst spec;
   1.450 -    val iso_infos = map snd spec;
   1.451 -    val absTs = map #absT iso_infos;
   1.452 -    val {take_consts, ...} = take_info;
   1.453 -    val {chain_take_thms, take_0_thms, take_Suc_thms, ...} = take_info;
   1.454 -    val {finite_consts, finite_defs, ...} = take_info;
   1.455 -
   1.456 -    val decisive_lemma =
   1.457 -      let
   1.458 -        fun iso_locale (info : iso_info) =
   1.459 -            @{thm iso.intro} OF [#abs_inverse info, #rep_inverse info];
   1.460 -        val iso_locale_thms = map iso_locale iso_infos;
   1.461 -        val decisive_abs_rep_thms =
   1.462 -            map (fn x => @{thm decisive_abs_rep} OF [x]) iso_locale_thms;
   1.463 -        val n = Free ("n", @{typ nat});
   1.464 -        fun mk_decisive t =
   1.465 -            Const (@{const_name decisive}, fastype_of t --> boolT) $ t;
   1.466 -        fun f take_const = mk_decisive (take_const $ n);
   1.467 -        val goal = mk_trp (foldr1 mk_conj (map f take_consts));
   1.468 -        val rules0 = @{thm decisive_bottom} :: take_0_thms;
   1.469 -        val rules1 =
   1.470 -            take_Suc_thms @ decisive_abs_rep_thms
   1.471 -            @ @{thms decisive_ID decisive_ssum_map decisive_sprod_map};
   1.472 -        val tac = EVERY [
   1.473 -            rtac @{thm nat.induct} 1,
   1.474 -            simp_tac (HOL_ss addsimps rules0) 1,
   1.475 -            asm_simp_tac (HOL_ss addsimps rules1) 1];
   1.476 -      in Goal.prove_global thy [] [] goal (K tac) end;
   1.477 -    fun conjuncts 1 thm = [thm]
   1.478 -      | conjuncts n thm = let
   1.479 -          val thmL = thm RS @{thm conjunct1};
   1.480 -          val thmR = thm RS @{thm conjunct2};
   1.481 -        in thmL :: conjuncts (n-1) thmR end;
   1.482 -    val decisive_thms = conjuncts (length spec) decisive_lemma;
   1.483 -
   1.484 -    fun prove_finite_thm (absT, finite_const) =
   1.485 -      let
   1.486 -        val goal = mk_trp (finite_const $ Free ("x", absT));
   1.487 -        val tac =
   1.488 -            EVERY [
   1.489 -            rewrite_goals_tac finite_defs,
   1.490 -            rtac @{thm lub_ID_finite} 1,
   1.491 -            resolve_tac chain_take_thms 1,
   1.492 -            resolve_tac lub_take_thms 1,
   1.493 -            resolve_tac decisive_thms 1];
   1.494 -      in
   1.495 -        Goal.prove_global thy [] [] goal (K tac)
   1.496 -      end;
   1.497 -    val finite_thms =
   1.498 -        map prove_finite_thm (absTs ~~ finite_consts);
   1.499 -
   1.500 -    fun prove_take_induct ((ch_take, lub_take), decisive) =
   1.501 -        Drule.export_without_context
   1.502 -          (@{thm lub_ID_finite_take_induct} OF [ch_take, lub_take, decisive]);
   1.503 -    val take_induct_thms =
   1.504 -        map prove_take_induct
   1.505 -          (chain_take_thms ~~ lub_take_thms ~~ decisive_thms);
   1.506 -
   1.507 -    val thy = thy
   1.508 -        |> fold (snd oo add_qualified_thm "finite")
   1.509 -            (dbinds ~~ finite_thms)
   1.510 -        |> fold (snd oo add_qualified_thm "take_induct")
   1.511 -            (dbinds ~~ take_induct_thms);
   1.512 -  in
   1.513 -    ((finite_thms, take_induct_thms), thy)
   1.514 -  end;
   1.515 -
   1.516 -fun add_lub_take_theorems
   1.517 -    (spec : (binding * iso_info) list)
   1.518 -    (take_info : take_info)
   1.519 -    (lub_take_thms : thm list)
   1.520 -    (thy : theory) =
   1.521 -  let
   1.522 -
   1.523 -    (* retrieve components of spec *)
   1.524 -    val dbinds = map fst spec;
   1.525 -    val iso_infos = map snd spec;
   1.526 -    val absTs = map #absT iso_infos;
   1.527 -    val repTs = map #repT iso_infos;
   1.528 -    val {take_consts, take_0_thms, take_Suc_thms, ...} = take_info;
   1.529 -    val {chain_take_thms, deflation_take_thms, ...} = take_info;
   1.530 -
   1.531 -    (* prove take lemmas *)
   1.532 -    fun prove_take_lemma ((chain_take, lub_take), dbind) thy =
   1.533 -      let
   1.534 -        val take_lemma =
   1.535 -            Drule.export_without_context
   1.536 -              (@{thm lub_ID_take_lemma} OF [chain_take, lub_take]);
   1.537 -      in
   1.538 -        add_qualified_thm "take_lemma" (dbind, take_lemma) thy
   1.539 -      end;
   1.540 -    val (take_lemma_thms, thy) =
   1.541 -      fold_map prove_take_lemma
   1.542 -        (chain_take_thms ~~ lub_take_thms ~~ dbinds) thy;
   1.543 -
   1.544 -    (* prove reach lemmas *)
   1.545 -    fun prove_reach_lemma ((chain_take, lub_take), dbind) thy =
   1.546 -      let
   1.547 -        val thm =
   1.548 -            Drule.zero_var_indexes
   1.549 -              (@{thm lub_ID_reach} OF [chain_take, lub_take]);
   1.550 -      in
   1.551 -        add_qualified_thm "reach" (dbind, thm) thy
   1.552 -      end;
   1.553 -    val (reach_thms, thy) =
   1.554 -      fold_map prove_reach_lemma
   1.555 -        (chain_take_thms ~~ lub_take_thms ~~ dbinds) thy;
   1.556 -
   1.557 -    (* test for finiteness of domain definitions *)
   1.558 -    local
   1.559 -      val types = [@{type_name ssum}, @{type_name sprod}];
   1.560 -      fun finite d T = if member (op =) absTs T then d else finite' d T
   1.561 -      and finite' d (Type (c, Ts)) =
   1.562 -          let val d' = d andalso member (op =) types c;
   1.563 -          in forall (finite d') Ts end
   1.564 -        | finite' d _ = true;
   1.565 -    in
   1.566 -      val is_finite = forall (finite true) repTs;
   1.567 -    end;
   1.568 -
   1.569 -    val ((finite_thms, take_induct_thms), thy) =
   1.570 -      if is_finite
   1.571 -      then
   1.572 -        let
   1.573 -          val ((finites, take_inducts), thy) =
   1.574 -              prove_finite_take_induct spec take_info lub_take_thms thy;
   1.575 -        in
   1.576 -          ((SOME finites, take_inducts), thy)
   1.577 -        end
   1.578 -      else
   1.579 -        let
   1.580 -          fun prove_take_induct (chain_take, lub_take) =
   1.581 -              Drule.zero_var_indexes
   1.582 -                (@{thm lub_ID_take_induct} OF [chain_take, lub_take]);
   1.583 -          val take_inducts =
   1.584 -              map prove_take_induct (chain_take_thms ~~ lub_take_thms);
   1.585 -          val thy = fold (snd oo add_qualified_thm "take_induct")
   1.586 -                         (dbinds ~~ take_inducts) thy;
   1.587 -        in
   1.588 -          ((NONE, take_inducts), thy)
   1.589 -        end;
   1.590 -
   1.591 -    val result =
   1.592 -      {
   1.593 -        take_consts         = #take_consts take_info,
   1.594 -        take_defs           = #take_defs take_info,
   1.595 -        chain_take_thms     = #chain_take_thms take_info,
   1.596 -        take_0_thms         = #take_0_thms take_info,
   1.597 -        take_Suc_thms       = #take_Suc_thms take_info,
   1.598 -        deflation_take_thms = #deflation_take_thms take_info,
   1.599 -        take_strict_thms    = #take_strict_thms take_info,
   1.600 -        finite_consts       = #finite_consts take_info,
   1.601 -        finite_defs         = #finite_defs take_info,
   1.602 -        lub_take_thms       = lub_take_thms,
   1.603 -        reach_thms          = reach_thms,
   1.604 -        take_lemma_thms     = take_lemma_thms,
   1.605 -        is_finite           = is_finite,
   1.606 -        take_induct_thms    = take_induct_thms
   1.607 -      };
   1.608 -  in
   1.609 -    (result, thy)
   1.610 -  end;
   1.611 -
   1.612 -end;