author huffman Fri Mar 05 09:09:11 2010 -0800 (2010-03-05) changeset 35585 555f26f00e47 parent 35583 c7ddb7105dde child 35586 f57de4a9eb9c
skip proof of induction rule for indirect-recursive domain definitions
```     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 {*
```