skip proof of induction rule for indirect-recursive domain definitions
authorhuffman
Fri Mar 05 09:09:11 2010 -0800 (2010-03-05)
changeset 35585555f26f00e47
parent 35583 c7ddb7105dde
child 35586 f57de4a9eb9c
skip proof of induction rule for indirect-recursive domain definitions
src/HOLCF/Tools/Domain/domain_theorems.ML
src/HOLCF/ex/Domain_ex.thy
     1.1 --- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Fri Mar 05 10:42:13 2010 +0100
     1.2 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Fri Mar 05 09:09:11 2010 -0800
     1.3 @@ -196,6 +196,278 @@
     1.4          pat_rews @ dist_les @ dist_eqs)
     1.5  end; (* let *)
     1.6  
     1.7 +(******************************************************************************)
     1.8 +(****************************** induction rules *******************************)
     1.9 +(******************************************************************************)
    1.10 +
    1.11 +fun prove_induction
    1.12 +    (comp_dnam, eqs : eq list)
    1.13 +    (take_lemmas : thm list)
    1.14 +    (axs_reach : thm list)
    1.15 +    (take_rews : thm list)
    1.16 +    (thy : theory) =
    1.17 +let
    1.18 +  val dnames = map (fst o fst) eqs;
    1.19 +  val conss  = map  snd        eqs;
    1.20 +  fun dc_take dn = %%:(dn^"_take");
    1.21 +  val x_name = idx_name dnames "x"; 
    1.22 +  val P_name = idx_name dnames "P";
    1.23 +  val pg = pg' thy;
    1.24 +
    1.25 +  local
    1.26 +    fun ga s dn = PureThy.get_thm thy (dn ^ "." ^ s);
    1.27 +    fun gts s dn = PureThy.get_thms thy (dn ^ "." ^ s);
    1.28 +  in
    1.29 +    val axs_chain_take = map (ga "chain_take") dnames;
    1.30 +    val axs_finite_def = map (ga "finite_def") dnames;
    1.31 +    val cases = map (ga  "casedist" ) dnames;
    1.32 +    val con_rews  = maps (gts "con_rews" ) dnames;
    1.33 +  end;
    1.34 +
    1.35 +  fun one_con p (con, args) =
    1.36 +    let
    1.37 +      val P_names = map P_name (1 upto (length dnames));
    1.38 +      val vns = Name.variant_list P_names (map vname args);
    1.39 +      val nonlazy_vns = map snd (filter_out (is_lazy o fst) (args ~~ vns));
    1.40 +      fun ind_hyp arg = %:(P_name (1 + rec_of arg)) $ bound_arg args arg;
    1.41 +      val t1 = mk_trp (%:p $ con_app2 con (bound_arg args) args);
    1.42 +      val t2 = lift ind_hyp (filter is_rec args, t1);
    1.43 +      val t3 = lift_defined (bound_arg vns) (nonlazy_vns, t2);
    1.44 +    in Library.foldr mk_All (vns, t3) end;
    1.45 +
    1.46 +  fun one_eq ((p, cons), concl) =
    1.47 +    mk_trp (%:p $ UU) ===> Logic.list_implies (map (one_con p) cons, concl);
    1.48 +
    1.49 +  fun ind_term concf = Library.foldr one_eq
    1.50 +    (mapn (fn n => fn x => (P_name n, x)) 1 conss,
    1.51 +     mk_trp (foldr1 mk_conj (mapn concf 1 dnames)));
    1.52 +  val take_ss = HOL_ss addsimps (@{thm Rep_CFun_strict1} :: take_rews);
    1.53 +  fun quant_tac ctxt i = EVERY
    1.54 +    (mapn (fn n => fn _ => res_inst_tac ctxt [(("x", 0), x_name n)] spec i) 1 dnames);
    1.55 +
    1.56 +  fun ind_prems_tac prems = EVERY
    1.57 +    (maps (fn cons =>
    1.58 +      (resolve_tac prems 1 ::
    1.59 +        maps (fn (_,args) => 
    1.60 +          resolve_tac prems 1 ::
    1.61 +          map (K(atac 1)) (nonlazy args) @
    1.62 +          map (K(atac 1)) (filter is_rec args))
    1.63 +        cons))
    1.64 +      conss);
    1.65 +  local 
    1.66 +    (* check whether every/exists constructor of the n-th part of the equation:
    1.67 +       it has a possibly indirectly recursive argument that isn't/is possibly 
    1.68 +       indirectly lazy *)
    1.69 +    fun rec_to quant nfn rfn ns lazy_rec (n,cons) = quant (exists (fn arg => 
    1.70 +          is_rec arg andalso not(rec_of arg mem ns) andalso
    1.71 +          ((rec_of arg =  n andalso nfn(lazy_rec orelse is_lazy arg)) orelse 
    1.72 +            rec_of arg <> n andalso rec_to quant nfn rfn (rec_of arg::ns) 
    1.73 +              (lazy_rec orelse is_lazy arg) (n, (List.nth(conss,rec_of arg))))
    1.74 +          ) o snd) cons;
    1.75 +    fun all_rec_to ns  = rec_to forall not all_rec_to  ns;
    1.76 +    fun warn (n,cons) =
    1.77 +      if all_rec_to [] false (n,cons)
    1.78 +      then (warning ("domain "^List.nth(dnames,n)^" is empty!"); true)
    1.79 +      else false;
    1.80 +    fun lazy_rec_to ns = rec_to exists I  lazy_rec_to ns;
    1.81 +
    1.82 +  in
    1.83 +    val n__eqs = mapn (fn n => fn (_,cons) => (n,cons)) 0 eqs;
    1.84 +    val is_emptys = map warn n__eqs;
    1.85 +    val is_finite = forall (not o lazy_rec_to [] false) n__eqs;
    1.86 +  end;
    1.87 +  val _ = trace " Proving finite_ind...";
    1.88 +  val finite_ind =
    1.89 +    let
    1.90 +      fun concf n dn = %:(P_name n) $ (dc_take dn $ %:"n" `%(x_name n));
    1.91 +      val goal = ind_term concf;
    1.92 +
    1.93 +      fun tacf {prems, context} =
    1.94 +        let
    1.95 +          val tacs1 = [
    1.96 +            quant_tac context 1,
    1.97 +            simp_tac HOL_ss 1,
    1.98 +            InductTacs.induct_tac context [[SOME "n"]] 1,
    1.99 +            simp_tac (take_ss addsimps prems) 1,
   1.100 +            TRY (safe_tac HOL_cs)];
   1.101 +          fun arg_tac arg =
   1.102 +                        (* FIXME! case_UU_tac *)
   1.103 +            case_UU_tac context (prems @ con_rews) 1
   1.104 +              (List.nth (dnames, rec_of arg) ^ "_take n$" ^ vname arg);
   1.105 +          fun con_tacs (con, args) = 
   1.106 +            asm_simp_tac take_ss 1 ::
   1.107 +            map arg_tac (filter is_nonlazy_rec args) @
   1.108 +            [resolve_tac prems 1] @
   1.109 +            map (K (atac 1)) (nonlazy args) @
   1.110 +            map (K (etac spec 1)) (filter is_rec args);
   1.111 +          fun cases_tacs (cons, cases) =
   1.112 +            res_inst_tac context [(("y", 0), "x")] cases 1 ::
   1.113 +            asm_simp_tac (take_ss addsimps prems) 1 ::
   1.114 +            maps con_tacs cons;
   1.115 +        in
   1.116 +          tacs1 @ maps cases_tacs (conss ~~ cases)
   1.117 +        end;
   1.118 +    in pg'' thy [] goal tacf
   1.119 +       handle ERROR _ => (warning "Proof of finite_ind failed."; TrueI)
   1.120 +    end;
   1.121 +
   1.122 +(* ----- theorems concerning finiteness and induction ----------------------- *)
   1.123 +
   1.124 +  val global_ctxt = ProofContext.init thy;
   1.125 +
   1.126 +  val _ = trace " Proving finites, ind...";
   1.127 +  val (finites, ind) =
   1.128 +  (
   1.129 +    if is_finite
   1.130 +    then (* finite case *)
   1.131 +      let 
   1.132 +        fun take_enough dn = mk_ex ("n",dc_take dn $ Bound 0 ` %:"x" === %:"x");
   1.133 +        fun dname_lemma dn =
   1.134 +          let
   1.135 +            val prem1 = mk_trp (defined (%:"x"));
   1.136 +            val disj1 = mk_all ("n", dc_take dn $ Bound 0 ` %:"x" === UU);
   1.137 +            val prem2 = mk_trp (mk_disj (disj1, take_enough dn));
   1.138 +            val concl = mk_trp (take_enough dn);
   1.139 +            val goal = prem1 ===> prem2 ===> concl;
   1.140 +            val tacs = [
   1.141 +              etac disjE 1,
   1.142 +              etac notE 1,
   1.143 +              resolve_tac take_lemmas 1,
   1.144 +              asm_simp_tac take_ss 1,
   1.145 +              atac 1];
   1.146 +          in pg [] goal (K tacs) end;
   1.147 +        val _ = trace " Proving finite_lemmas1a";
   1.148 +        val finite_lemmas1a = map dname_lemma dnames;
   1.149 + 
   1.150 +        val _ = trace " Proving finite_lemma1b";
   1.151 +        val finite_lemma1b =
   1.152 +          let
   1.153 +            fun mk_eqn n ((dn, args), _) =
   1.154 +              let
   1.155 +                val disj1 = dc_take dn $ Bound 1 ` Bound 0 === UU;
   1.156 +                val disj2 = dc_take dn $ Bound 1 ` Bound 0 === Bound 0;
   1.157 +              in
   1.158 +                mk_constrainall
   1.159 +                  (x_name n, Type (dn,args), mk_disj (disj1, disj2))
   1.160 +              end;
   1.161 +            val goal =
   1.162 +              mk_trp (mk_all ("n", foldr1 mk_conj (mapn mk_eqn 1 eqs)));
   1.163 +            fun arg_tacs ctxt vn = [
   1.164 +              eres_inst_tac ctxt [(("x", 0), vn)] all_dupE 1,
   1.165 +              etac disjE 1,
   1.166 +              asm_simp_tac (HOL_ss addsimps con_rews) 1,
   1.167 +              asm_simp_tac take_ss 1];
   1.168 +            fun con_tacs ctxt (con, args) =
   1.169 +              asm_simp_tac take_ss 1 ::
   1.170 +              maps (arg_tacs ctxt) (nonlazy_rec args);
   1.171 +            fun foo_tacs ctxt n (cons, cases) =
   1.172 +              simp_tac take_ss 1 ::
   1.173 +              rtac allI 1 ::
   1.174 +              res_inst_tac ctxt [(("y", 0), x_name n)] cases 1 ::
   1.175 +              asm_simp_tac take_ss 1 ::
   1.176 +              maps (con_tacs ctxt) cons;
   1.177 +            fun tacs ctxt =
   1.178 +              rtac allI 1 ::
   1.179 +              InductTacs.induct_tac ctxt [[SOME "n"]] 1 ::
   1.180 +              simp_tac take_ss 1 ::
   1.181 +              TRY (safe_tac (empty_cs addSEs [conjE] addSIs [conjI])) ::
   1.182 +              flat (mapn (foo_tacs ctxt) 1 (conss ~~ cases));
   1.183 +          in pg [] goal tacs end;
   1.184 +
   1.185 +        fun one_finite (dn, l1b) =
   1.186 +          let
   1.187 +            val goal = mk_trp (%%:(dn^"_finite") $ %:"x");
   1.188 +            fun tacs ctxt = [
   1.189 +                        (* FIXME! case_UU_tac *)
   1.190 +              case_UU_tac ctxt take_rews 1 "x",
   1.191 +              eresolve_tac finite_lemmas1a 1,
   1.192 +              step_tac HOL_cs 1,
   1.193 +              step_tac HOL_cs 1,
   1.194 +              cut_facts_tac [l1b] 1,
   1.195 +              fast_tac HOL_cs 1];
   1.196 +          in pg axs_finite_def goal tacs end;
   1.197 +
   1.198 +        val _ = trace " Proving finites";
   1.199 +        val finites = map one_finite (dnames ~~ atomize global_ctxt finite_lemma1b);
   1.200 +        val _ = trace " Proving ind";
   1.201 +        val ind =
   1.202 +          let
   1.203 +            fun concf n dn = %:(P_name n) $ %:(x_name n);
   1.204 +            fun tacf {prems, context} =
   1.205 +              let
   1.206 +                fun finite_tacs (finite, fin_ind) = [
   1.207 +                  rtac(rewrite_rule axs_finite_def finite RS exE)1,
   1.208 +                  etac subst 1,
   1.209 +                  rtac fin_ind 1,
   1.210 +                  ind_prems_tac prems];
   1.211 +              in
   1.212 +                TRY (safe_tac HOL_cs) ::
   1.213 +                maps finite_tacs (finites ~~ atomize global_ctxt finite_ind)
   1.214 +              end;
   1.215 +          in pg'' thy [] (ind_term concf) tacf end;
   1.216 +      in (finites, ind) end (* let *)
   1.217 +
   1.218 +    else (* infinite case *)
   1.219 +      let
   1.220 +        fun one_finite n dn =
   1.221 +          read_instantiate global_ctxt [(("P", 0), dn ^ "_finite " ^ x_name n)] excluded_middle;
   1.222 +        val finites = mapn one_finite 1 dnames;
   1.223 +
   1.224 +        val goal =
   1.225 +          let
   1.226 +            fun one_adm n _ = mk_trp (mk_adm (%:(P_name n)));
   1.227 +            fun concf n dn = %:(P_name n) $ %:(x_name n);
   1.228 +          in Logic.list_implies (mapn one_adm 1 dnames, ind_term concf) end;
   1.229 +        val cont_rules =
   1.230 +            @{thms cont_id cont_const cont2cont_Rep_CFun
   1.231 +                   cont2cont_fst cont2cont_snd};
   1.232 +        val subgoal =
   1.233 +          let fun p n dn = %:(P_name n) $ (dc_take dn $ Bound 0 `%(x_name n));
   1.234 +          in mk_trp (mk_all ("n", foldr1 mk_conj (mapn p 1 dnames))) end;
   1.235 +        val subgoal' = legacy_infer_term thy subgoal;
   1.236 +        fun tacf {prems, context} =
   1.237 +          let
   1.238 +            val subtac =
   1.239 +                EVERY [rtac allI 1, rtac finite_ind 1, ind_prems_tac prems];
   1.240 +            val subthm = Goal.prove context [] [] subgoal' (K subtac);
   1.241 +          in
   1.242 +            map (fn ax_reach => rtac (ax_reach RS subst) 1) axs_reach @ [
   1.243 +            cut_facts_tac (subthm :: take (length dnames) prems) 1,
   1.244 +            REPEAT (rtac @{thm conjI} 1 ORELSE
   1.245 +                    EVERY [etac @{thm admD [OF _ ch2ch_Rep_CFunL]} 1,
   1.246 +                           resolve_tac axs_chain_take 1,
   1.247 +                           asm_simp_tac HOL_basic_ss 1])
   1.248 +            ]
   1.249 +          end;
   1.250 +        val ind = (pg'' thy [] goal tacf
   1.251 +          handle ERROR _ =>
   1.252 +            (warning "Cannot prove infinite induction rule"; TrueI)
   1.253 +                  );
   1.254 +      in (finites, ind) end
   1.255 +  )
   1.256 +      handle THM _ =>
   1.257 +             (warning "Induction proofs failed (THM raised)."; ([], TrueI))
   1.258 +           | ERROR _ =>
   1.259 +             (warning "Cannot prove induction rule"; ([], TrueI));
   1.260 +
   1.261 +val inducts = Project_Rule.projections (ProofContext.init thy) ind;
   1.262 +fun ind_rule (dname, rule) = ((Binding.empty, [rule]), [Induct.induct_type dname]);
   1.263 +val induct_failed = (Thm.prop_of ind = Thm.prop_of TrueI);
   1.264 +
   1.265 +in thy |> Sign.add_path comp_dnam
   1.266 +       |> snd o PureThy.add_thmss [
   1.267 +           ((Binding.name "finites"    , finites     ), []),
   1.268 +           ((Binding.name "finite_ind" , [finite_ind]), []),
   1.269 +           ((Binding.name "ind"        , [ind]       ), [])]
   1.270 +       |> (if induct_failed then I
   1.271 +           else snd o PureThy.add_thmss (map ind_rule (dnames ~~ inducts)))
   1.272 +       |> Sign.parent_path
   1.273 +end; (* prove_induction *)
   1.274 +
   1.275 +(******************************************************************************)
   1.276 +(************************ bisimulation and coinduction ************************)
   1.277 +(******************************************************************************)
   1.278 +
   1.279  fun prove_coinduction
   1.280      (comp_dnam, eqs : eq list)
   1.281      (take_lemmas : thm list)
   1.282 @@ -348,303 +620,62 @@
   1.283  val map_tab = Domain_Take_Proofs.get_map_tab thy;
   1.284  
   1.285  val dnames = map (fst o fst) eqs;
   1.286 -val conss  = map  snd        eqs;
   1.287  val comp_dname = Sign.full_bname thy comp_dnam;
   1.288  
   1.289  val _ = message ("Proving induction properties of domain "^comp_dname^" ...");
   1.290  
   1.291 -val pg = pg' thy;
   1.292 +(* ----- getting the composite axiom and definitions ------------------------ *)
   1.293  
   1.294 -(* ----- getting the composite axiom and definitions ------------------------ *)
   1.295 +(* Test for indirect recursion *)
   1.296 +local
   1.297 +  fun indirect_arg arg =
   1.298 +      rec_of arg = ~1 andalso Datatype_Aux.is_rec_type (dtyp_of arg);
   1.299 +  fun indirect_con (_, args) = exists indirect_arg args;
   1.300 +  fun indirect_eq (_, cons) = exists indirect_con cons;
   1.301 +in
   1.302 +  val is_indirect = exists indirect_eq eqs;
   1.303 +  val _ = if is_indirect
   1.304 +          then message "Definition uses indirect recursion."
   1.305 +          else ();
   1.306 +end;
   1.307 +
   1.308 +(* theorems about take *)
   1.309  
   1.310  local
   1.311    fun ga s dn = PureThy.get_thm thy (dn ^ "." ^ s);
   1.312 -in
   1.313 -  val axs_take_def   = map (ga "take_def"  ) dnames;
   1.314    val axs_chain_take = map (ga "chain_take") dnames;
   1.315    val axs_lub_take   = map (ga "lub_take"  ) dnames;
   1.316 -  val axs_finite_def = map (ga "finite_def") dnames;
   1.317 -end;
   1.318 -
   1.319 -local
   1.320 -  fun gt  s dn = PureThy.get_thm  thy (dn ^ "." ^ s);
   1.321 -  fun gts s dn = PureThy.get_thms thy (dn ^ "." ^ s);
   1.322  in
   1.323 -  val cases = map (gt  "casedist" ) dnames;
   1.324 -  val con_rews  = maps (gts "con_rews" ) dnames;
   1.325 -end;
   1.326 -
   1.327 -fun dc_take dn = %%:(dn^"_take");
   1.328 -val x_name = idx_name dnames "x"; 
   1.329 -val P_name = idx_name dnames "P";
   1.330 -val n_eqs = length eqs;
   1.331 -
   1.332 -(* ----- theorems concerning finite approximation and finite induction ------ *)
   1.333 -
   1.334 -val take_rews =
   1.335 -    maps (fn dn => PureThy.get_thms thy (dn ^ ".take_rews")) dnames;
   1.336 -
   1.337 -local
   1.338 -  fun one_con p (con, args) =
   1.339 -    let
   1.340 -      val P_names = map P_name (1 upto (length dnames));
   1.341 -      val vns = Name.variant_list P_names (map vname args);
   1.342 -      val nonlazy_vns = map snd (filter_out (is_lazy o fst) (args ~~ vns));
   1.343 -      fun ind_hyp arg = %:(P_name (1 + rec_of arg)) $ bound_arg args arg;
   1.344 -      val t1 = mk_trp (%:p $ con_app2 con (bound_arg args) args);
   1.345 -      val t2 = lift ind_hyp (filter is_rec args, t1);
   1.346 -      val t3 = lift_defined (bound_arg vns) (nonlazy_vns, t2);
   1.347 -    in Library.foldr mk_All (vns, t3) end;
   1.348 -
   1.349 -  fun one_eq ((p, cons), concl) =
   1.350 -    mk_trp (%:p $ UU) ===> Logic.list_implies (map (one_con p) cons, concl);
   1.351 -
   1.352 -  fun ind_term concf = Library.foldr one_eq
   1.353 -    (mapn (fn n => fn x => (P_name n, x)) 1 conss,
   1.354 -     mk_trp (foldr1 mk_conj (mapn concf 1 dnames)));
   1.355 -  val take_ss = HOL_ss addsimps (@{thm Rep_CFun_strict1} :: take_rews);
   1.356 -  fun quant_tac ctxt i = EVERY
   1.357 -    (mapn (fn n => fn _ => res_inst_tac ctxt [(("x", 0), x_name n)] spec i) 1 dnames);
   1.358 -
   1.359 -  fun ind_prems_tac prems = EVERY
   1.360 -    (maps (fn cons =>
   1.361 -      (resolve_tac prems 1 ::
   1.362 -        maps (fn (_,args) => 
   1.363 -          resolve_tac prems 1 ::
   1.364 -          map (K(atac 1)) (nonlazy args) @
   1.365 -          map (K(atac 1)) (filter is_rec args))
   1.366 -        cons))
   1.367 -      conss);
   1.368 -  local 
   1.369 -    (* check whether every/exists constructor of the n-th part of the equation:
   1.370 -       it has a possibly indirectly recursive argument that isn't/is possibly 
   1.371 -       indirectly lazy *)
   1.372 -    fun rec_to quant nfn rfn ns lazy_rec (n,cons) = quant (exists (fn arg => 
   1.373 -          is_rec arg andalso not(rec_of arg mem ns) andalso
   1.374 -          ((rec_of arg =  n andalso nfn(lazy_rec orelse is_lazy arg)) orelse 
   1.375 -            rec_of arg <> n andalso rec_to quant nfn rfn (rec_of arg::ns) 
   1.376 -              (lazy_rec orelse is_lazy arg) (n, (List.nth(conss,rec_of arg))))
   1.377 -          ) o snd) cons;
   1.378 -    fun all_rec_to ns  = rec_to forall not all_rec_to  ns;
   1.379 -    fun warn (n,cons) =
   1.380 -      if all_rec_to [] false (n,cons)
   1.381 -      then (warning ("domain "^List.nth(dnames,n)^" is empty!"); true)
   1.382 -      else false;
   1.383 -    fun lazy_rec_to ns = rec_to exists I  lazy_rec_to ns;
   1.384 -
   1.385 -  in
   1.386 -    val n__eqs = mapn (fn n => fn (_,cons) => (n,cons)) 0 eqs;
   1.387 -    val is_emptys = map warn n__eqs;
   1.388 -    val is_finite = forall (not o lazy_rec_to [] false) n__eqs;
   1.389 -  end;
   1.390 -in (* local *)
   1.391 -  val _ = trace " Proving finite_ind...";
   1.392 -  val finite_ind =
   1.393 -    let
   1.394 -      fun concf n dn = %:(P_name n) $ (dc_take dn $ %:"n" `%(x_name n));
   1.395 -      val goal = ind_term concf;
   1.396 -
   1.397 -      fun tacf {prems, context} =
   1.398 -        let
   1.399 -          val tacs1 = [
   1.400 -            quant_tac context 1,
   1.401 -            simp_tac HOL_ss 1,
   1.402 -            InductTacs.induct_tac context [[SOME "n"]] 1,
   1.403 -            simp_tac (take_ss addsimps prems) 1,
   1.404 -            TRY (safe_tac HOL_cs)];
   1.405 -          fun arg_tac arg =
   1.406 -                        (* FIXME! case_UU_tac *)
   1.407 -            case_UU_tac context (prems @ con_rews) 1
   1.408 -              (List.nth (dnames, rec_of arg) ^ "_take n$" ^ vname arg);
   1.409 -          fun con_tacs (con, args) = 
   1.410 -            asm_simp_tac take_ss 1 ::
   1.411 -            map arg_tac (filter is_nonlazy_rec args) @
   1.412 -            [resolve_tac prems 1] @
   1.413 -            map (K (atac 1)) (nonlazy args) @
   1.414 -            map (K (etac spec 1)) (filter is_rec args);
   1.415 -          fun cases_tacs (cons, cases) =
   1.416 -            res_inst_tac context [(("y", 0), "x")] cases 1 ::
   1.417 -            asm_simp_tac (take_ss addsimps prems) 1 ::
   1.418 -            maps con_tacs cons;
   1.419 -        in
   1.420 -          tacs1 @ maps cases_tacs (conss ~~ cases)
   1.421 -        end;
   1.422 -    in pg'' thy [] goal tacf
   1.423 -       handle ERROR _ => (warning "Proof of finite_ind failed."; TrueI)
   1.424 -    end;
   1.425 -
   1.426    val _ = trace " Proving take_lemmas...";
   1.427    val take_lemmas =
   1.428      let
   1.429        fun take_lemma (ax_chain_take, ax_lub_take) =
   1.430 -        Drule.export_without_context
   1.431 -        (@{thm lub_ID_take_lemma} OF [ax_chain_take, ax_lub_take]);
   1.432 +          Drule.export_without_context
   1.433 +            (@{thm lub_ID_take_lemma} OF [ax_chain_take, ax_lub_take]);
   1.434      in map take_lemma (axs_chain_take ~~ axs_lub_take) end;
   1.435 -
   1.436    val axs_reach =
   1.437      let
   1.438        fun reach (ax_chain_take, ax_lub_take) =
   1.439 -        Drule.export_without_context
   1.440 -        (@{thm lub_ID_reach} OF [ax_chain_take, ax_lub_take]);
   1.441 +          Drule.export_without_context
   1.442 +            (@{thm lub_ID_reach} OF [ax_chain_take, ax_lub_take]);
   1.443      in map reach (axs_chain_take ~~ axs_lub_take) end;
   1.444 -
   1.445 -(* ----- theorems concerning finiteness and induction ----------------------- *)
   1.446 -
   1.447 -  val global_ctxt = ProofContext.init thy;
   1.448 -
   1.449 -  val _ = trace " Proving finites, ind...";
   1.450 -  val (finites, ind) =
   1.451 -  (
   1.452 -    if is_finite
   1.453 -    then (* finite case *)
   1.454 -      let 
   1.455 -        fun take_enough dn = mk_ex ("n",dc_take dn $ Bound 0 ` %:"x" === %:"x");
   1.456 -        fun dname_lemma dn =
   1.457 -          let
   1.458 -            val prem1 = mk_trp (defined (%:"x"));
   1.459 -            val disj1 = mk_all ("n", dc_take dn $ Bound 0 ` %:"x" === UU);
   1.460 -            val prem2 = mk_trp (mk_disj (disj1, take_enough dn));
   1.461 -            val concl = mk_trp (take_enough dn);
   1.462 -            val goal = prem1 ===> prem2 ===> concl;
   1.463 -            val tacs = [
   1.464 -              etac disjE 1,
   1.465 -              etac notE 1,
   1.466 -              resolve_tac take_lemmas 1,
   1.467 -              asm_simp_tac take_ss 1,
   1.468 -              atac 1];
   1.469 -          in pg [] goal (K tacs) end;
   1.470 -        val _ = trace " Proving finite_lemmas1a";
   1.471 -        val finite_lemmas1a = map dname_lemma dnames;
   1.472 - 
   1.473 -        val _ = trace " Proving finite_lemma1b";
   1.474 -        val finite_lemma1b =
   1.475 -          let
   1.476 -            fun mk_eqn n ((dn, args), _) =
   1.477 -              let
   1.478 -                val disj1 = dc_take dn $ Bound 1 ` Bound 0 === UU;
   1.479 -                val disj2 = dc_take dn $ Bound 1 ` Bound 0 === Bound 0;
   1.480 -              in
   1.481 -                mk_constrainall
   1.482 -                  (x_name n, Type (dn,args), mk_disj (disj1, disj2))
   1.483 -              end;
   1.484 -            val goal =
   1.485 -              mk_trp (mk_all ("n", foldr1 mk_conj (mapn mk_eqn 1 eqs)));
   1.486 -            fun arg_tacs ctxt vn = [
   1.487 -              eres_inst_tac ctxt [(("x", 0), vn)] all_dupE 1,
   1.488 -              etac disjE 1,
   1.489 -              asm_simp_tac (HOL_ss addsimps con_rews) 1,
   1.490 -              asm_simp_tac take_ss 1];
   1.491 -            fun con_tacs ctxt (con, args) =
   1.492 -              asm_simp_tac take_ss 1 ::
   1.493 -              maps (arg_tacs ctxt) (nonlazy_rec args);
   1.494 -            fun foo_tacs ctxt n (cons, cases) =
   1.495 -              simp_tac take_ss 1 ::
   1.496 -              rtac allI 1 ::
   1.497 -              res_inst_tac ctxt [(("y", 0), x_name n)] cases 1 ::
   1.498 -              asm_simp_tac take_ss 1 ::
   1.499 -              maps (con_tacs ctxt) cons;
   1.500 -            fun tacs ctxt =
   1.501 -              rtac allI 1 ::
   1.502 -              InductTacs.induct_tac ctxt [[SOME "n"]] 1 ::
   1.503 -              simp_tac take_ss 1 ::
   1.504 -              TRY (safe_tac (empty_cs addSEs [conjE] addSIs [conjI])) ::
   1.505 -              flat (mapn (foo_tacs ctxt) 1 (conss ~~ cases));
   1.506 -          in pg [] goal tacs end;
   1.507 +end;
   1.508  
   1.509 -        fun one_finite (dn, l1b) =
   1.510 -          let
   1.511 -            val goal = mk_trp (%%:(dn^"_finite") $ %:"x");
   1.512 -            fun tacs ctxt = [
   1.513 -                        (* FIXME! case_UU_tac *)
   1.514 -              case_UU_tac ctxt take_rews 1 "x",
   1.515 -              eresolve_tac finite_lemmas1a 1,
   1.516 -              step_tac HOL_cs 1,
   1.517 -              step_tac HOL_cs 1,
   1.518 -              cut_facts_tac [l1b] 1,
   1.519 -              fast_tac HOL_cs 1];
   1.520 -          in pg axs_finite_def goal tacs end;
   1.521 -
   1.522 -        val _ = trace " Proving finites";
   1.523 -        val finites = map one_finite (dnames ~~ atomize global_ctxt finite_lemma1b);
   1.524 -        val _ = trace " Proving ind";
   1.525 -        val ind =
   1.526 -          let
   1.527 -            fun concf n dn = %:(P_name n) $ %:(x_name n);
   1.528 -            fun tacf {prems, context} =
   1.529 -              let
   1.530 -                fun finite_tacs (finite, fin_ind) = [
   1.531 -                  rtac(rewrite_rule axs_finite_def finite RS exE)1,
   1.532 -                  etac subst 1,
   1.533 -                  rtac fin_ind 1,
   1.534 -                  ind_prems_tac prems];
   1.535 -              in
   1.536 -                TRY (safe_tac HOL_cs) ::
   1.537 -                maps finite_tacs (finites ~~ atomize global_ctxt finite_ind)
   1.538 -              end;
   1.539 -          in pg'' thy [] (ind_term concf) tacf end;
   1.540 -      in (finites, ind) end (* let *)
   1.541 -
   1.542 -    else (* infinite case *)
   1.543 -      let
   1.544 -        fun one_finite n dn =
   1.545 -          read_instantiate global_ctxt [(("P", 0), dn ^ "_finite " ^ x_name n)] excluded_middle;
   1.546 -        val finites = mapn one_finite 1 dnames;
   1.547 +val take_rews =
   1.548 +    maps (fn dn => PureThy.get_thms thy (dn ^ ".take_rews")) dnames;
   1.549  
   1.550 -        val goal =
   1.551 -          let
   1.552 -            fun one_adm n _ = mk_trp (mk_adm (%:(P_name n)));
   1.553 -            fun concf n dn = %:(P_name n) $ %:(x_name n);
   1.554 -          in Logic.list_implies (mapn one_adm 1 dnames, ind_term concf) end;
   1.555 -        val cont_rules =
   1.556 -            @{thms cont_id cont_const cont2cont_Rep_CFun
   1.557 -                   cont2cont_fst cont2cont_snd};
   1.558 -        val subgoal =
   1.559 -          let fun p n dn = %:(P_name n) $ (dc_take dn $ Bound 0 `%(x_name n));
   1.560 -          in mk_trp (mk_all ("n", foldr1 mk_conj (mapn p 1 dnames))) end;
   1.561 -        val subgoal' = legacy_infer_term thy subgoal;
   1.562 -        fun tacf {prems, context} =
   1.563 -          let
   1.564 -            val subtac =
   1.565 -                EVERY [rtac allI 1, rtac finite_ind 1, ind_prems_tac prems];
   1.566 -            val subthm = Goal.prove context [] [] subgoal' (K subtac);
   1.567 -          in
   1.568 -            map (fn ax_reach => rtac (ax_reach RS subst) 1) axs_reach @ [
   1.569 -            cut_facts_tac (subthm :: take (length dnames) prems) 1,
   1.570 -            REPEAT (rtac @{thm conjI} 1 ORELSE
   1.571 -                    EVERY [etac @{thm admD [OF _ ch2ch_Rep_CFunL]} 1,
   1.572 -                           resolve_tac axs_chain_take 1,
   1.573 -                           asm_simp_tac HOL_basic_ss 1])
   1.574 -            ]
   1.575 -          end;
   1.576 -        val ind = (pg'' thy [] goal tacf
   1.577 -          handle ERROR _ =>
   1.578 -            (warning "Cannot prove infinite induction rule"; TrueI)
   1.579 -                  );
   1.580 -      in (finites, ind) end
   1.581 -  )
   1.582 -      handle THM _ =>
   1.583 -             (warning "Induction proofs failed (THM raised)."; ([], TrueI))
   1.584 -           | ERROR _ =>
   1.585 -             (warning "Cannot prove induction rule"; ([], TrueI));
   1.586 -
   1.587 -end; (* local *)
   1.588 +(* prove induction rules, unless definition is indirect recursive *)
   1.589 +val thy =
   1.590 +    if is_indirect then thy else
   1.591 +    prove_induction (comp_dnam, eqs) take_lemmas axs_reach take_rews thy;
   1.592  
   1.593  val (coind, thy) = prove_coinduction (comp_dnam, eqs) take_lemmas thy;
   1.594  
   1.595 -val inducts = Project_Rule.projections (ProofContext.init thy) ind;
   1.596 -fun ind_rule (dname, rule) = ((Binding.empty, [rule]), [Induct.induct_type dname]);
   1.597 -val induct_failed = (Thm.prop_of ind = Thm.prop_of TrueI);
   1.598 -
   1.599  in thy |> Sign.add_path comp_dnam
   1.600         |> snd o PureThy.add_thmss [
   1.601             ((Binding.name "take_lemmas", take_lemmas ), []),
   1.602             ((Binding.name "reach"      , axs_reach   ), []),
   1.603 -           ((Binding.name "finites"    , finites     ), []),
   1.604 -           ((Binding.name "finite_ind" , [finite_ind]), []),
   1.605 -           ((Binding.name "ind"        , [ind]       ), []),
   1.606             ((Binding.name "coind"      , [coind]     ), [])]
   1.607 -       |> (if induct_failed then I
   1.608 -           else snd o PureThy.add_thmss (map ind_rule (dnames ~~ inducts)))
   1.609         |> Sign.parent_path |> pair take_rews
   1.610  end; (* let *)
   1.611  end; (* struct *)
     2.1 --- a/src/HOLCF/ex/Domain_ex.thy	Fri Mar 05 10:42:13 2010 +0100
     2.2 +++ b/src/HOLCF/ex/Domain_ex.thy	Fri Mar 05 09:09:11 2010 -0800
     2.3 @@ -52,18 +52,18 @@
     2.4  
     2.5  text {*
     2.6    Indirect recusion is allowed for sums, products, lifting, and the
     2.7 -  continuous function space.  However, the domain package currently
     2.8 -  cannot prove the induction rules.  A fix is planned for the next
     2.9 -  release.
    2.10 +  continuous function space.  However, the domain package does not
    2.11 +  generate an induction rule in terms of the constructors.
    2.12  *}
    2.13  
    2.14  domain 'a d7 = d7a "'a d7 \<oplus> int lift" | d7b "'a \<otimes> 'a d7" | d7c (lazy "'a d7 \<rightarrow> 'a")
    2.15  
    2.16 -thm d7.ind -- "currently replaced with dummy theorem"
    2.17 +(* d7.ind is absent *)
    2.18  
    2.19  text {*
    2.20    Indirect recursion using previously-defined datatypes is currently
    2.21 -  not allowed.  This restriction should go away by the next release.
    2.22 +  not allowed.  This restriction does not apply to the new definitional
    2.23 +  domain package.
    2.24  *}
    2.25  (*
    2.26  domain 'a slist = SNil | SCons 'a "'a slist"
    2.27 @@ -167,6 +167,7 @@
    2.28  thm tree.take_take
    2.29  thm tree.deflation_take
    2.30  thm tree.take_lemmas
    2.31 +thm tree.lub_take
    2.32  thm tree.reach
    2.33  thm tree.finite_ind
    2.34  
    2.35 @@ -199,15 +200,14 @@
    2.36    I don't know what is going on here.  The failed proof has to do with
    2.37    the finiteness predicate.
    2.38  *}
    2.39 -(*
    2.40 +
    2.41  domain foo = Foo (lazy "bar") and bar = Bar
    2.42 -  -- "Tactic failed."
    2.43 -*)
    2.44 +  -- "Cannot prove induction rule"
    2.45  
    2.46  text {* Declaring class constraints on the LHS is currently broken. *}
    2.47  (*
    2.48  domain ('a::cpo) box = Box (lazy 'a)
    2.49 -  -- "Malformed YXML encoding: multiple results"
    2.50 +  -- "Proof failed"
    2.51  *)
    2.52  
    2.53  text {*