src/HOL/HOLCF/Tools/Domain/domain_induction.ML
changeset 40832 4352ca878c41
parent 40774 0437dbc127b3
child 41214 8a341cf54a85
     1.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_induction.ML	Tue Nov 30 14:01:49 2010 -0800
     1.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_induction.ML	Tue Nov 30 14:21:57 2010 -0800
     1.3 @@ -13,20 +13,20 @@
     1.4        Domain_Constructors.constr_info list ->
     1.5        theory -> thm list * theory
     1.6  
     1.7 -  val quiet_mode: bool Unsynchronized.ref;
     1.8 -  val trace_domain: bool Unsynchronized.ref;
     1.9 -end;
    1.10 +  val quiet_mode: bool Unsynchronized.ref
    1.11 +  val trace_domain: bool Unsynchronized.ref
    1.12 +end
    1.13  
    1.14  structure Domain_Induction :> DOMAIN_INDUCTION =
    1.15  struct
    1.16  
    1.17 -val quiet_mode = Unsynchronized.ref false;
    1.18 -val trace_domain = Unsynchronized.ref false;
    1.19 +val quiet_mode = Unsynchronized.ref false
    1.20 +val trace_domain = Unsynchronized.ref false
    1.21  
    1.22 -fun message s = if !quiet_mode then () else writeln s;
    1.23 -fun trace s = if !trace_domain then tracing s else ();
    1.24 +fun message s = if !quiet_mode then () else writeln s
    1.25 +fun trace s = if !trace_domain then tracing s else ()
    1.26  
    1.27 -open HOLCF_Library;
    1.28 +open HOLCF_Library
    1.29  
    1.30  (******************************************************************************)
    1.31  (***************************** proofs about take ******************************)
    1.32 @@ -38,60 +38,60 @@
    1.33      (constr_infos : Domain_Constructors.constr_info list)
    1.34      (thy : theory) : thm list list * theory =
    1.35  let
    1.36 -  val {take_consts, take_Suc_thms, deflation_take_thms, ...} = take_info;
    1.37 -  val deflation_thms = Domain_Take_Proofs.get_deflation_thms thy;
    1.38 +  val {take_consts, take_Suc_thms, deflation_take_thms, ...} = take_info
    1.39 +  val deflation_thms = Domain_Take_Proofs.get_deflation_thms thy
    1.40  
    1.41 -  val n = Free ("n", @{typ nat});
    1.42 -  val n' = @{const Suc} $ n;
    1.43 +  val n = Free ("n", @{typ nat})
    1.44 +  val n' = @{const Suc} $ n
    1.45  
    1.46    local
    1.47 -    val newTs = map (#absT o #iso_info) constr_infos;
    1.48 -    val subs = newTs ~~ map (fn t => t $ n) take_consts;
    1.49 +    val newTs = map (#absT o #iso_info) constr_infos
    1.50 +    val subs = newTs ~~ map (fn t => t $ n) take_consts
    1.51      fun is_ID (Const (c, _)) = (c = @{const_name ID})
    1.52 -      | is_ID _              = false;
    1.53 +      | is_ID _              = false
    1.54    in
    1.55      fun map_of_arg thy v T =
    1.56 -      let val m = Domain_Take_Proofs.map_of_typ thy subs T;
    1.57 -      in if is_ID m then v else mk_capply (m, v) end;
    1.58 +      let val m = Domain_Take_Proofs.map_of_typ thy subs T
    1.59 +      in if is_ID m then v else mk_capply (m, v) end
    1.60    end
    1.61  
    1.62    fun prove_take_apps
    1.63        ((dbind, take_const), constr_info) thy =
    1.64      let
    1.65 -      val {iso_info, con_specs, con_betas, ...} = constr_info;
    1.66 -      val {abs_inverse, ...} = iso_info;
    1.67 +      val {iso_info, con_specs, con_betas, ...} = constr_info
    1.68 +      val {abs_inverse, ...} = iso_info
    1.69        fun prove_take_app (con_const, args) =
    1.70          let
    1.71 -          val Ts = map snd args;
    1.72 -          val ns = Name.variant_list ["n"] (Datatype_Prop.make_tnames Ts);
    1.73 -          val vs = map Free (ns ~~ Ts);
    1.74 -          val lhs = mk_capply (take_const $ n', list_ccomb (con_const, vs));
    1.75 -          val rhs = list_ccomb (con_const, map2 (map_of_arg thy) vs Ts);
    1.76 -          val goal = mk_trp (mk_eq (lhs, rhs));
    1.77 +          val Ts = map snd args
    1.78 +          val ns = Name.variant_list ["n"] (Datatype_Prop.make_tnames Ts)
    1.79 +          val vs = map Free (ns ~~ Ts)
    1.80 +          val lhs = mk_capply (take_const $ n', list_ccomb (con_const, vs))
    1.81 +          val rhs = list_ccomb (con_const, map2 (map_of_arg thy) vs Ts)
    1.82 +          val goal = mk_trp (mk_eq (lhs, rhs))
    1.83            val rules =
    1.84                [abs_inverse] @ con_betas @ @{thms take_con_rules}
    1.85 -              @ take_Suc_thms @ deflation_thms @ deflation_take_thms;
    1.86 -          val tac = simp_tac (HOL_basic_ss addsimps rules) 1;
    1.87 +              @ take_Suc_thms @ deflation_thms @ deflation_take_thms
    1.88 +          val tac = simp_tac (HOL_basic_ss addsimps rules) 1
    1.89          in
    1.90            Goal.prove_global thy [] [] goal (K tac)
    1.91 -        end;
    1.92 -      val take_apps = map prove_take_app con_specs;
    1.93 +        end
    1.94 +      val take_apps = map prove_take_app con_specs
    1.95      in
    1.96        yield_singleton Global_Theory.add_thmss
    1.97          ((Binding.qualified true "take_rews" dbind, take_apps),
    1.98          [Simplifier.simp_add]) thy
    1.99 -    end;
   1.100 +    end
   1.101  in
   1.102    fold_map prove_take_apps
   1.103      (dbinds ~~ take_consts ~~ constr_infos) thy
   1.104 -end;
   1.105 +end
   1.106  
   1.107  (******************************************************************************)
   1.108  (****************************** induction rules *******************************)
   1.109  (******************************************************************************)
   1.110  
   1.111  val case_UU_allI =
   1.112 -    @{lemma "(!!x. x ~= UU ==> P x) ==> P UU ==> ALL x. P x" by metis};
   1.113 +    @{lemma "(!!x. x ~= UU ==> P x) ==> P UU ==> ALL x. P x" by metis}
   1.114  
   1.115  fun prove_induction
   1.116      (comp_dbind : binding)
   1.117 @@ -100,135 +100,135 @@
   1.118      (take_rews : thm list)
   1.119      (thy : theory) =
   1.120  let
   1.121 -  val comp_dname = Binding.name_of comp_dbind;
   1.122 +  val comp_dname = Binding.name_of comp_dbind
   1.123  
   1.124 -  val iso_infos = map #iso_info constr_infos;
   1.125 -  val exhausts = map #exhaust constr_infos;
   1.126 -  val con_rews = maps #con_rews constr_infos;
   1.127 -  val {take_consts, take_induct_thms, ...} = take_info;
   1.128 +  val iso_infos = map #iso_info constr_infos
   1.129 +  val exhausts = map #exhaust constr_infos
   1.130 +  val con_rews = maps #con_rews constr_infos
   1.131 +  val {take_consts, take_induct_thms, ...} = take_info
   1.132  
   1.133 -  val newTs = map #absT iso_infos;
   1.134 -  val P_names = Datatype_Prop.indexify_names (map (K "P") newTs);
   1.135 -  val x_names = Datatype_Prop.indexify_names (map (K "x") newTs);
   1.136 -  val P_types = map (fn T => T --> HOLogic.boolT) newTs;
   1.137 -  val Ps = map Free (P_names ~~ P_types);
   1.138 -  val xs = map Free (x_names ~~ newTs);
   1.139 -  val n = Free ("n", HOLogic.natT);
   1.140 +  val newTs = map #absT iso_infos
   1.141 +  val P_names = Datatype_Prop.indexify_names (map (K "P") newTs)
   1.142 +  val x_names = Datatype_Prop.indexify_names (map (K "x") newTs)
   1.143 +  val P_types = map (fn T => T --> HOLogic.boolT) newTs
   1.144 +  val Ps = map Free (P_names ~~ P_types)
   1.145 +  val xs = map Free (x_names ~~ newTs)
   1.146 +  val n = Free ("n", HOLogic.natT)
   1.147  
   1.148    fun con_assm defined p (con, args) =
   1.149      let
   1.150 -      val Ts = map snd args;
   1.151 -      val ns = Name.variant_list P_names (Datatype_Prop.make_tnames Ts);
   1.152 -      val vs = map Free (ns ~~ Ts);
   1.153 -      val nonlazy = map snd (filter_out (fst o fst) (args ~~ vs));
   1.154 +      val Ts = map snd args
   1.155 +      val ns = Name.variant_list P_names (Datatype_Prop.make_tnames Ts)
   1.156 +      val vs = map Free (ns ~~ Ts)
   1.157 +      val nonlazy = map snd (filter_out (fst o fst) (args ~~ vs))
   1.158        fun ind_hyp (v, T) t =
   1.159            case AList.lookup (op =) (newTs ~~ Ps) T of NONE => t
   1.160 -          | SOME p' => Logic.mk_implies (mk_trp (p' $ v), t);
   1.161 -      val t1 = mk_trp (p $ list_ccomb (con, vs));
   1.162 -      val t2 = fold_rev ind_hyp (vs ~~ Ts) t1;
   1.163 -      val t3 = Logic.list_implies (map (mk_trp o mk_defined) nonlazy, t2);
   1.164 -    in fold_rev Logic.all vs (if defined then t3 else t2) end;
   1.165 +          | SOME p' => Logic.mk_implies (mk_trp (p' $ v), t)
   1.166 +      val t1 = mk_trp (p $ list_ccomb (con, vs))
   1.167 +      val t2 = fold_rev ind_hyp (vs ~~ Ts) t1
   1.168 +      val t3 = Logic.list_implies (map (mk_trp o mk_defined) nonlazy, t2)
   1.169 +    in fold_rev Logic.all vs (if defined then t3 else t2) end
   1.170    fun eq_assms ((p, T), cons) =
   1.171 -      mk_trp (p $ HOLCF_Library.mk_bottom T) :: map (con_assm true p) cons;
   1.172 -  val assms = maps eq_assms (Ps ~~ newTs ~~ map #con_specs constr_infos);
   1.173 +      mk_trp (p $ HOLCF_Library.mk_bottom T) :: map (con_assm true p) cons
   1.174 +  val assms = maps eq_assms (Ps ~~ newTs ~~ map #con_specs constr_infos)
   1.175  
   1.176 -  val take_ss = HOL_ss addsimps (@{thm Rep_cfun_strict1} :: take_rews);
   1.177 +  val take_ss = HOL_ss addsimps (@{thm Rep_cfun_strict1} :: take_rews)
   1.178    fun quant_tac ctxt i = EVERY
   1.179 -    (map (fn name => res_inst_tac ctxt [(("x", 0), name)] spec i) x_names);
   1.180 +    (map (fn name => res_inst_tac ctxt [(("x", 0), name)] spec i) x_names)
   1.181  
   1.182    (* FIXME: move this message to domain_take_proofs.ML *)
   1.183 -  val is_finite = #is_finite take_info;
   1.184 +  val is_finite = #is_finite take_info
   1.185    val _ = if is_finite
   1.186            then message ("Proving finiteness rule for domain "^comp_dname^" ...")
   1.187 -          else ();
   1.188 +          else ()
   1.189  
   1.190 -  val _ = trace " Proving finite_ind...";
   1.191 +  val _ = trace " Proving finite_ind..."
   1.192    val finite_ind =
   1.193      let
   1.194        val concls =
   1.195            map (fn ((P, t), x) => P $ mk_capply (t $ n, x))
   1.196 -              (Ps ~~ take_consts ~~ xs);
   1.197 -      val goal = mk_trp (foldr1 mk_conj concls);
   1.198 +              (Ps ~~ take_consts ~~ xs)
   1.199 +      val goal = mk_trp (foldr1 mk_conj concls)
   1.200  
   1.201        fun tacf {prems, context} =
   1.202          let
   1.203            (* Prove stronger prems, without definedness side conditions *)
   1.204            fun con_thm p (con, args) =
   1.205              let
   1.206 -              val subgoal = con_assm false p (con, args);
   1.207 -              val rules = prems @ con_rews @ simp_thms;
   1.208 -              val simplify = asm_simp_tac (HOL_basic_ss addsimps rules);
   1.209 +              val subgoal = con_assm false p (con, args)
   1.210 +              val rules = prems @ con_rews @ simp_thms
   1.211 +              val simplify = asm_simp_tac (HOL_basic_ss addsimps rules)
   1.212                fun arg_tac (lazy, _) =
   1.213 -                  rtac (if lazy then allI else case_UU_allI) 1;
   1.214 +                  rtac (if lazy then allI else case_UU_allI) 1
   1.215                val tacs =
   1.216                    rewrite_goals_tac @{thms atomize_all atomize_imp} ::
   1.217                    map arg_tac args @
   1.218 -                  [REPEAT (rtac impI 1), ALLGOALS simplify];
   1.219 +                  [REPEAT (rtac impI 1), ALLGOALS simplify]
   1.220              in
   1.221                Goal.prove context [] [] subgoal (K (EVERY tacs))
   1.222 -            end;
   1.223 -          fun eq_thms (p, cons) = map (con_thm p) cons;
   1.224 -          val conss = map #con_specs constr_infos;
   1.225 -          val prems' = maps eq_thms (Ps ~~ conss);
   1.226 +            end
   1.227 +          fun eq_thms (p, cons) = map (con_thm p) cons
   1.228 +          val conss = map #con_specs constr_infos
   1.229 +          val prems' = maps eq_thms (Ps ~~ conss)
   1.230  
   1.231            val tacs1 = [
   1.232              quant_tac context 1,
   1.233              simp_tac HOL_ss 1,
   1.234              InductTacs.induct_tac context [[SOME "n"]] 1,
   1.235              simp_tac (take_ss addsimps prems) 1,
   1.236 -            TRY (safe_tac HOL_cs)];
   1.237 +            TRY (safe_tac HOL_cs)]
   1.238            fun con_tac _ = 
   1.239              asm_simp_tac take_ss 1 THEN
   1.240 -            (resolve_tac prems' THEN_ALL_NEW etac spec) 1;
   1.241 +            (resolve_tac prems' THEN_ALL_NEW etac spec) 1
   1.242            fun cases_tacs (cons, exhaust) =
   1.243              res_inst_tac context [(("y", 0), "x")] exhaust 1 ::
   1.244              asm_simp_tac (take_ss addsimps prems) 1 ::
   1.245 -            map con_tac cons;
   1.246 +            map con_tac cons
   1.247            val tacs = tacs1 @ maps cases_tacs (conss ~~ exhausts)
   1.248          in
   1.249            EVERY (map DETERM tacs)
   1.250 -        end;
   1.251 -    in Goal.prove_global thy [] assms goal tacf end;
   1.252 +        end
   1.253 +    in Goal.prove_global thy [] assms goal tacf end
   1.254  
   1.255 -  val _ = trace " Proving ind...";
   1.256 +  val _ = trace " Proving ind..."
   1.257    val ind =
   1.258      let
   1.259 -      val concls = map (op $) (Ps ~~ xs);
   1.260 -      val goal = mk_trp (foldr1 mk_conj concls);
   1.261 -      val adms = if is_finite then [] else map (mk_trp o mk_adm) Ps;
   1.262 +      val concls = map (op $) (Ps ~~ xs)
   1.263 +      val goal = mk_trp (foldr1 mk_conj concls)
   1.264 +      val adms = if is_finite then [] else map (mk_trp o mk_adm) Ps
   1.265        fun tacf {prems, context} =
   1.266          let
   1.267            fun finite_tac (take_induct, fin_ind) =
   1.268                rtac take_induct 1 THEN
   1.269                (if is_finite then all_tac else resolve_tac prems 1) THEN
   1.270 -              (rtac fin_ind THEN_ALL_NEW solve_tac prems) 1;
   1.271 -          val fin_inds = Project_Rule.projections context finite_ind;
   1.272 +              (rtac fin_ind THEN_ALL_NEW solve_tac prems) 1
   1.273 +          val fin_inds = Project_Rule.projections context finite_ind
   1.274          in
   1.275            TRY (safe_tac HOL_cs) THEN
   1.276            EVERY (map finite_tac (take_induct_thms ~~ fin_inds))
   1.277 -        end;
   1.278 +        end
   1.279      in Goal.prove_global thy [] (adms @ assms) goal tacf end
   1.280  
   1.281    (* case names for induction rules *)
   1.282 -  val dnames = map (fst o dest_Type) newTs;
   1.283 +  val dnames = map (fst o dest_Type) newTs
   1.284    val case_ns =
   1.285      let
   1.286        val adms =
   1.287            if is_finite then [] else
   1.288            if length dnames = 1 then ["adm"] else
   1.289 -          map (fn s => "adm_" ^ Long_Name.base_name s) dnames;
   1.290 +          map (fn s => "adm_" ^ Long_Name.base_name s) dnames
   1.291        val bottoms =
   1.292            if length dnames = 1 then ["bottom"] else
   1.293 -          map (fn s => "bottom_" ^ Long_Name.base_name s) dnames;
   1.294 +          map (fn s => "bottom_" ^ Long_Name.base_name s) dnames
   1.295        fun one_eq bot constr_info =
   1.296 -        let fun name_of (c, args) = Long_Name.base_name (fst (dest_Const c));
   1.297 -        in bot :: map name_of (#con_specs constr_info) end;
   1.298 -    in adms @ flat (map2 one_eq bottoms constr_infos) end;
   1.299 +        let fun name_of (c, args) = Long_Name.base_name (fst (dest_Const c))
   1.300 +        in bot :: map name_of (#con_specs constr_info) end
   1.301 +    in adms @ flat (map2 one_eq bottoms constr_infos) end
   1.302  
   1.303 -  val inducts = Project_Rule.projections (ProofContext.init_global thy) ind;
   1.304 +  val inducts = Project_Rule.projections (ProofContext.init_global thy) ind
   1.305    fun ind_rule (dname, rule) =
   1.306        ((Binding.empty, rule),
   1.307 -       [Rule_Cases.case_names case_ns, Induct.induct_type dname]);
   1.308 +       [Rule_Cases.case_names case_ns, Induct.induct_type dname])
   1.309  
   1.310  in
   1.311    thy
   1.312 @@ -236,7 +236,7 @@
   1.313       ((Binding.qualified true "finite_induct" comp_dbind, finite_ind), []),
   1.314       ((Binding.qualified true "induct"        comp_dbind, ind       ), [])]
   1.315    |> (snd o Global_Theory.add_thms (map ind_rule (dnames ~~ inducts)))
   1.316 -end; (* prove_induction *)
   1.317 +end (* prove_induction *)
   1.318  
   1.319  (******************************************************************************)
   1.320  (************************ bisimulation and coinduction ************************)
   1.321 @@ -249,83 +249,83 @@
   1.322      (take_rews : thm list list)
   1.323      (thy : theory) : theory =
   1.324  let
   1.325 -  val iso_infos = map #iso_info constr_infos;
   1.326 -  val newTs = map #absT iso_infos;
   1.327 +  val iso_infos = map #iso_info constr_infos
   1.328 +  val newTs = map #absT iso_infos
   1.329  
   1.330 -  val {take_consts, take_0_thms, take_lemma_thms, ...} = take_info;
   1.331 +  val {take_consts, take_0_thms, take_lemma_thms, ...} = take_info
   1.332  
   1.333 -  val R_names = Datatype_Prop.indexify_names (map (K "R") newTs);
   1.334 -  val R_types = map (fn T => T --> T --> boolT) newTs;
   1.335 -  val Rs = map Free (R_names ~~ R_types);
   1.336 -  val n = Free ("n", natT);
   1.337 -  val reserved = "x" :: "y" :: R_names;
   1.338 +  val R_names = Datatype_Prop.indexify_names (map (K "R") newTs)
   1.339 +  val R_types = map (fn T => T --> T --> boolT) newTs
   1.340 +  val Rs = map Free (R_names ~~ R_types)
   1.341 +  val n = Free ("n", natT)
   1.342 +  val reserved = "x" :: "y" :: R_names
   1.343  
   1.344    (* declare bisimulation predicate *)
   1.345 -  val bisim_bind = Binding.suffix_name "_bisim" comp_dbind;
   1.346 -  val bisim_type = R_types ---> boolT;
   1.347 +  val bisim_bind = Binding.suffix_name "_bisim" comp_dbind
   1.348 +  val bisim_type = R_types ---> boolT
   1.349    val (bisim_const, thy) =
   1.350 -      Sign.declare_const ((bisim_bind, bisim_type), NoSyn) thy;
   1.351 +      Sign.declare_const ((bisim_bind, bisim_type), NoSyn) thy
   1.352  
   1.353    (* define bisimulation predicate *)
   1.354    local
   1.355      fun one_con T (con, args) =
   1.356        let
   1.357 -        val Ts = map snd args;
   1.358 -        val ns1 = Name.variant_list reserved (Datatype_Prop.make_tnames Ts);
   1.359 -        val ns2 = map (fn n => n^"'") ns1;
   1.360 -        val vs1 = map Free (ns1 ~~ Ts);
   1.361 -        val vs2 = map Free (ns2 ~~ Ts);
   1.362 -        val eq1 = mk_eq (Free ("x", T), list_ccomb (con, vs1));
   1.363 -        val eq2 = mk_eq (Free ("y", T), list_ccomb (con, vs2));
   1.364 +        val Ts = map snd args
   1.365 +        val ns1 = Name.variant_list reserved (Datatype_Prop.make_tnames Ts)
   1.366 +        val ns2 = map (fn n => n^"'") ns1
   1.367 +        val vs1 = map Free (ns1 ~~ Ts)
   1.368 +        val vs2 = map Free (ns2 ~~ Ts)
   1.369 +        val eq1 = mk_eq (Free ("x", T), list_ccomb (con, vs1))
   1.370 +        val eq2 = mk_eq (Free ("y", T), list_ccomb (con, vs2))
   1.371          fun rel ((v1, v2), T) =
   1.372              case AList.lookup (op =) (newTs ~~ Rs) T of
   1.373 -              NONE => mk_eq (v1, v2) | SOME r => r $ v1 $ v2;
   1.374 -        val eqs = foldr1 mk_conj (map rel (vs1 ~~ vs2 ~~ Ts) @ [eq1, eq2]);
   1.375 +              NONE => mk_eq (v1, v2) | SOME r => r $ v1 $ v2
   1.376 +        val eqs = foldr1 mk_conj (map rel (vs1 ~~ vs2 ~~ Ts) @ [eq1, eq2])
   1.377        in
   1.378          Library.foldr mk_ex (vs1 @ vs2, eqs)
   1.379 -      end;
   1.380 +      end
   1.381      fun one_eq ((T, R), cons) =
   1.382        let
   1.383 -        val x = Free ("x", T);
   1.384 -        val y = Free ("y", T);
   1.385 -        val disj1 = mk_conj (mk_eq (x, mk_bottom T), mk_eq (y, mk_bottom T));
   1.386 -        val disjs = disj1 :: map (one_con T) cons;
   1.387 +        val x = Free ("x", T)
   1.388 +        val y = Free ("y", T)
   1.389 +        val disj1 = mk_conj (mk_eq (x, mk_bottom T), mk_eq (y, mk_bottom T))
   1.390 +        val disjs = disj1 :: map (one_con T) cons
   1.391        in
   1.392          mk_all (x, mk_all (y, mk_imp (R $ x $ y, foldr1 mk_disj disjs)))
   1.393 -      end;
   1.394 -    val conjs = map one_eq (newTs ~~ Rs ~~ map #con_specs constr_infos);
   1.395 -    val bisim_rhs = lambdas Rs (Library.foldr1 mk_conj conjs);
   1.396 -    val bisim_eqn = Logic.mk_equals (bisim_const, bisim_rhs);
   1.397 +      end
   1.398 +    val conjs = map one_eq (newTs ~~ Rs ~~ map #con_specs constr_infos)
   1.399 +    val bisim_rhs = lambdas Rs (Library.foldr1 mk_conj conjs)
   1.400 +    val bisim_eqn = Logic.mk_equals (bisim_const, bisim_rhs)
   1.401    in
   1.402      val (bisim_def_thm, thy) = thy |>
   1.403          yield_singleton (Global_Theory.add_defs false)
   1.404 -         ((Binding.qualified true "bisim_def" comp_dbind, bisim_eqn), []);
   1.405 +         ((Binding.qualified true "bisim_def" comp_dbind, bisim_eqn), [])
   1.406    end (* local *)
   1.407  
   1.408    (* prove coinduction lemma *)
   1.409    val coind_lemma =
   1.410      let
   1.411 -      val assm = mk_trp (list_comb (bisim_const, Rs));
   1.412 +      val assm = mk_trp (list_comb (bisim_const, Rs))
   1.413        fun one ((T, R), take_const) =
   1.414          let
   1.415 -          val x = Free ("x", T);
   1.416 -          val y = Free ("y", T);
   1.417 -          val lhs = mk_capply (take_const $ n, x);
   1.418 -          val rhs = mk_capply (take_const $ n, y);
   1.419 +          val x = Free ("x", T)
   1.420 +          val y = Free ("y", T)
   1.421 +          val lhs = mk_capply (take_const $ n, x)
   1.422 +          val rhs = mk_capply (take_const $ n, y)
   1.423          in
   1.424            mk_all (x, mk_all (y, mk_imp (R $ x $ y, mk_eq (lhs, rhs))))
   1.425 -        end;
   1.426 +        end
   1.427        val goal =
   1.428 -          mk_trp (foldr1 mk_conj (map one (newTs ~~ Rs ~~ take_consts)));
   1.429 -      val rules = @{thm Rep_cfun_strict1} :: take_0_thms;
   1.430 +          mk_trp (foldr1 mk_conj (map one (newTs ~~ Rs ~~ take_consts)))
   1.431 +      val rules = @{thm Rep_cfun_strict1} :: take_0_thms
   1.432        fun tacf {prems, context} =
   1.433          let
   1.434 -          val prem' = rewrite_rule [bisim_def_thm] (hd prems);
   1.435 -          val prems' = Project_Rule.projections context prem';
   1.436 -          val dests = map (fn th => th RS spec RS spec RS mp) prems';
   1.437 +          val prem' = rewrite_rule [bisim_def_thm] (hd prems)
   1.438 +          val prems' = Project_Rule.projections context prem'
   1.439 +          val dests = map (fn th => th RS spec RS spec RS mp) prems'
   1.440            fun one_tac (dest, rews) =
   1.441                dtac dest 1 THEN safe_tac HOL_cs THEN
   1.442 -              ALLGOALS (asm_simp_tac (HOL_basic_ss addsimps rews));
   1.443 +              ALLGOALS (asm_simp_tac (HOL_basic_ss addsimps rews))
   1.444          in
   1.445            rtac @{thm nat.induct} 1 THEN
   1.446            simp_tac (HOL_ss addsimps rules) 1 THEN
   1.447 @@ -334,33 +334,33 @@
   1.448          end
   1.449      in
   1.450        Goal.prove_global thy [] [assm] goal tacf
   1.451 -    end;
   1.452 +    end
   1.453  
   1.454    (* prove individual coinduction rules *)
   1.455    fun prove_coind ((T, R), take_lemma) =
   1.456      let
   1.457 -      val x = Free ("x", T);
   1.458 -      val y = Free ("y", T);
   1.459 -      val assm1 = mk_trp (list_comb (bisim_const, Rs));
   1.460 -      val assm2 = mk_trp (R $ x $ y);
   1.461 -      val goal = mk_trp (mk_eq (x, y));
   1.462 +      val x = Free ("x", T)
   1.463 +      val y = Free ("y", T)
   1.464 +      val assm1 = mk_trp (list_comb (bisim_const, Rs))
   1.465 +      val assm2 = mk_trp (R $ x $ y)
   1.466 +      val goal = mk_trp (mk_eq (x, y))
   1.467        fun tacf {prems, context} =
   1.468          let
   1.469 -          val rule = hd prems RS coind_lemma;
   1.470 +          val rule = hd prems RS coind_lemma
   1.471          in
   1.472            rtac take_lemma 1 THEN
   1.473            asm_simp_tac (HOL_basic_ss addsimps (rule :: prems)) 1
   1.474 -        end;
   1.475 +        end
   1.476      in
   1.477        Goal.prove_global thy [] [assm1, assm2] goal tacf
   1.478 -    end;
   1.479 -  val coinds = map prove_coind (newTs ~~ Rs ~~ take_lemma_thms);
   1.480 -  val coind_binds = map (Binding.qualified true "coinduct") dbinds;
   1.481 +    end
   1.482 +  val coinds = map prove_coind (newTs ~~ Rs ~~ take_lemma_thms)
   1.483 +  val coind_binds = map (Binding.qualified true "coinduct") dbinds
   1.484  
   1.485  in
   1.486    thy |> snd o Global_Theory.add_thms
   1.487      (map Thm.no_attributes (coind_binds ~~ coinds))
   1.488 -end; (* let *)
   1.489 +end (* let *)
   1.490  
   1.491  (******************************************************************************)
   1.492  (******************************* main function ********************************)
   1.493 @@ -373,67 +373,67 @@
   1.494      (thy : theory) =
   1.495  let
   1.496  
   1.497 -val comp_dname = space_implode "_" (map Binding.name_of dbinds);
   1.498 -val comp_dbind = Binding.name comp_dname;
   1.499 +val comp_dname = space_implode "_" (map Binding.name_of dbinds)
   1.500 +val comp_dbind = Binding.name comp_dname
   1.501  
   1.502  (* Test for emptiness *)
   1.503  (* FIXME: reimplement emptiness test
   1.504  local
   1.505 -  open Domain_Library;
   1.506 -  val dnames = map (fst o fst) eqs;
   1.507 -  val conss = map snd eqs;
   1.508 +  open Domain_Library
   1.509 +  val dnames = map (fst o fst) eqs
   1.510 +  val conss = map snd eqs
   1.511    fun rec_to ns lazy_rec (n,cons) = forall (exists (fn arg => 
   1.512          is_rec arg andalso not (member (op =) ns (rec_of arg)) andalso
   1.513          ((rec_of arg =  n andalso not (lazy_rec orelse is_lazy arg)) orelse 
   1.514            rec_of arg <> n andalso rec_to (rec_of arg::ns) 
   1.515              (lazy_rec orelse is_lazy arg) (n, (List.nth(conss,rec_of arg))))
   1.516 -        ) o snd) cons;
   1.517 +        ) o snd) cons
   1.518    fun warn (n,cons) =
   1.519      if rec_to [] false (n,cons)
   1.520 -    then (warning ("domain "^List.nth(dnames,n)^" is empty!"); true)
   1.521 -    else false;
   1.522 +    then (warning ("domain "^List.nth(dnames,n)^" is empty!") true)
   1.523 +    else false
   1.524  in
   1.525 -  val n__eqs = mapn (fn n => fn (_,cons) => (n,cons)) 0 eqs;
   1.526 -  val is_emptys = map warn n__eqs;
   1.527 -end;
   1.528 +  val n__eqs = mapn (fn n => fn (_,cons) => (n,cons)) 0 eqs
   1.529 +  val is_emptys = map warn n__eqs
   1.530 +end
   1.531  *)
   1.532  
   1.533  (* Test for indirect recursion *)
   1.534  local
   1.535 -  val newTs = map (#absT o #iso_info) constr_infos;
   1.536 +  val newTs = map (#absT o #iso_info) constr_infos
   1.537    fun indirect_typ (Type (_, Ts)) =
   1.538        exists (fn T => member (op =) newTs T orelse indirect_typ T) Ts
   1.539 -    | indirect_typ _ = false;
   1.540 -  fun indirect_arg (_, T) = indirect_typ T;
   1.541 -  fun indirect_con (_, args) = exists indirect_arg args;
   1.542 -  fun indirect_eq cons = exists indirect_con cons;
   1.543 +    | indirect_typ _ = false
   1.544 +  fun indirect_arg (_, T) = indirect_typ T
   1.545 +  fun indirect_con (_, args) = exists indirect_arg args
   1.546 +  fun indirect_eq cons = exists indirect_con cons
   1.547  in
   1.548 -  val is_indirect = exists indirect_eq (map #con_specs constr_infos);
   1.549 +  val is_indirect = exists indirect_eq (map #con_specs constr_infos)
   1.550    val _ =
   1.551        if is_indirect
   1.552        then message "Indirect recursion detected, skipping proofs of (co)induction rules"
   1.553 -      else message ("Proving induction properties of domain "^comp_dname^" ...");
   1.554 -end;
   1.555 +      else message ("Proving induction properties of domain "^comp_dname^" ...")
   1.556 +end
   1.557  
   1.558  (* theorems about take *)
   1.559  
   1.560  val (take_rewss, thy) =
   1.561 -    take_theorems dbinds take_info constr_infos thy;
   1.562 +    take_theorems dbinds take_info constr_infos thy
   1.563  
   1.564 -val {take_lemma_thms, take_0_thms, take_strict_thms, ...} = take_info;
   1.565 +val {take_lemma_thms, take_0_thms, take_strict_thms, ...} = take_info
   1.566  
   1.567 -val take_rews = take_0_thms @ take_strict_thms @ flat take_rewss;
   1.568 +val take_rews = take_0_thms @ take_strict_thms @ flat take_rewss
   1.569  
   1.570  (* prove induction rules, unless definition is indirect recursive *)
   1.571  val thy =
   1.572      if is_indirect then thy else
   1.573 -    prove_induction comp_dbind constr_infos take_info take_rews thy;
   1.574 +    prove_induction comp_dbind constr_infos take_info take_rews thy
   1.575  
   1.576  val thy =
   1.577      if is_indirect then thy else
   1.578 -    prove_coinduction (comp_dbind, dbinds) constr_infos take_info take_rewss thy;
   1.579 +    prove_coinduction (comp_dbind, dbinds) constr_infos take_info take_rewss thy
   1.580  
   1.581  in
   1.582    (take_rews, thy)
   1.583 -end; (* let *)
   1.584 -end; (* struct *)
   1.585 +end (* let *)
   1.586 +end (* struct *)