src/HOL/Tools/inductive.ML
changeset 45647 96af0578571c
parent 45592 8baa0b7f3f66
child 45648 7654f750fb43
     1.1 --- a/src/HOL/Tools/inductive.ML	Sun Nov 27 13:12:42 2011 +0100
     1.2 +++ b/src/HOL/Tools/inductive.ML	Sun Nov 27 14:20:31 2011 +0100
     1.3 @@ -114,6 +114,7 @@
     1.4    [@{thm le_fun_def}, @{thm le_bool_def}, @{thm sup_fun_def}, @{thm sup_bool_def}];
     1.5  
     1.6  
     1.7 +
     1.8  (** context data **)
     1.9  
    1.10  type inductive_result =
    1.11 @@ -133,7 +134,7 @@
    1.12  type inductive_info =
    1.13    {names: string list, coind: bool} * inductive_result;
    1.14  
    1.15 -structure InductiveData = Generic_Data
    1.16 +structure Data = Generic_Data
    1.17  (
    1.18    type T = inductive_info Symtab.table * thm list;
    1.19    val empty = (Symtab.empty, []);
    1.20 @@ -142,7 +143,7 @@
    1.21      (Symtab.merge (K true) (tab1, tab2), Thm.merge_thms (monos1, monos2));
    1.22  );
    1.23  
    1.24 -val get_inductives = InductiveData.get o Context.Proof;
    1.25 +val get_inductives = Data.get o Context.Proof;
    1.26  
    1.27  fun print_inductives ctxt =
    1.28    let
    1.29 @@ -162,15 +163,15 @@
    1.30      NONE => error ("Unknown (co)inductive predicate " ^ quote name)
    1.31    | SOME info => info);
    1.32  
    1.33 -fun put_inductives names info = InductiveData.map
    1.34 -  (apfst (fold (fn name => Symtab.update (name, info)) names));
    1.35 +fun put_inductives names info =
    1.36 +  Data.map (apfst (fold (fn name => Symtab.update (name, info)) names));
    1.37  
    1.38  
    1.39  
    1.40  (** monotonicity rules **)
    1.41  
    1.42  val get_monos = #2 o get_inductives;
    1.43 -val map_monos = InductiveData.map o apsnd;
    1.44 +val map_monos = Data.map o apsnd;
    1.45  
    1.46  fun mk_mono ctxt thm =
    1.47    let
    1.48 @@ -178,13 +179,13 @@
    1.49      fun dest_less_concl thm = dest_less_concl (thm RS @{thm le_funD})
    1.50        handle THM _ => thm RS @{thm le_boolD}
    1.51    in
    1.52 -    case concl_of thm of
    1.53 +    (case concl_of thm of
    1.54        Const ("==", _) $ _ $ _ => eq2mono (thm RS meta_eq_to_obj_eq)
    1.55      | _ $ (Const (@{const_name HOL.eq}, _) $ _ $ _) => eq2mono thm
    1.56      | _ $ (Const (@{const_name Orderings.less_eq}, _) $ _ $ _) =>
    1.57        dest_less_concl (Seq.hd (REPEAT (FIRSTGOAL
    1.58          (resolve_tac [@{thm le_funI}, @{thm le_boolI'}])) thm))
    1.59 -    | _ => thm
    1.60 +    | _ => thm)
    1.61    end handle THM _ => error ("Bad monotonicity theorem:\n" ^ Display.string_of_thm ctxt thm);
    1.62  
    1.63  val mono_add =
    1.64 @@ -199,7 +200,7 @@
    1.65  
    1.66  (** equations **)
    1.67  
    1.68 -structure Equation_Data = Generic_Data
    1.69 +structure Equation_Data = Generic_Data   (* FIXME just one data slot per module *)
    1.70  (
    1.71    type T = thm Item_Net.T;
    1.72    val empty = Item_Net.init (op aconv o pairself Thm.prop_of)
    1.73 @@ -263,7 +264,8 @@
    1.74  
    1.75  fun select_disj 1 1 = []
    1.76    | select_disj _ 1 = [rtac disjI1]
    1.77 -  | select_disj n i = (rtac disjI2)::(select_disj (n - 1) (i - 1));
    1.78 +  | select_disj n i = rtac disjI2 :: select_disj (n - 1) (i - 1);
    1.79 +
    1.80  
    1.81  
    1.82  (** process rules **)
    1.83 @@ -298,17 +300,19 @@
    1.84      val aprems = map (atomize_term (Proof_Context.theory_of ctxt)) prems;
    1.85      val arule = list_all_free (params', Logic.list_implies (aprems, concl));
    1.86  
    1.87 -    fun check_ind err t = case dest_predicate cs params t of
    1.88 +    fun check_ind err t =
    1.89 +      (case dest_predicate cs params t of
    1.90          NONE => err (bad_app ^
    1.91            commas (map (Syntax.string_of_term ctxt) params))
    1.92        | SOME (_, _, ys, _) =>
    1.93            if exists (fn c => exists (fn t => Logic.occs (c, t)) ys) cs
    1.94 -          then err bad_ind_occ else ();
    1.95 +          then err bad_ind_occ else ());
    1.96  
    1.97      fun check_prem' prem t =
    1.98        if member (op =) cs (head_of t) then
    1.99          check_ind (err_in_prem ctxt binding rule prem) t
   1.100 -      else (case t of
   1.101 +      else
   1.102 +        (case t of
   1.103            Abs (_, _, t) => check_prem' prem t
   1.104          | t $ u => (check_prem' prem t; check_prem' prem u)
   1.105          | _ => ());
   1.106 @@ -316,14 +320,16 @@
   1.107      fun check_prem (prem, aprem) =
   1.108        if can HOLogic.dest_Trueprop aprem then check_prem' prem prem
   1.109        else err_in_prem ctxt binding rule prem "Non-atomic premise";
   1.110 -  in
   1.111 -    (case concl of
   1.112 -       Const (@{const_name Trueprop}, _) $ t =>
   1.113 -         if member (op =) cs (head_of t) then
   1.114 +
   1.115 +    val _ =
   1.116 +      (case concl of
   1.117 +        Const (@{const_name Trueprop}, _) $ t =>
   1.118 +          if member (op =) cs (head_of t) then
   1.119             (check_ind (err_in_rule ctxt binding rule') t;
   1.120              List.app check_prem (prems ~~ aprems))
   1.121 -         else err_in_rule ctxt binding rule' bad_concl
   1.122 -     | _ => err_in_rule ctxt binding rule' bad_concl);
   1.123 +          else err_in_rule ctxt binding rule' bad_concl
   1.124 +       | _ => err_in_rule ctxt binding rule' bad_concl);
   1.125 +  in
   1.126      ((binding, att), arule)
   1.127    end;
   1.128  
   1.129 @@ -428,16 +434,19 @@
   1.130  
   1.131     in map prove_elim cs end;
   1.132  
   1.133 +
   1.134  (* prove simplification equations *)
   1.135  
   1.136 -fun prove_eqs quiet_mode cs params intr_ts intrs (elims: (thm * bstring list * int) list) ctxt ctxt'' =
   1.137 +fun prove_eqs quiet_mode cs params intr_ts intrs
   1.138 +    (elims: (thm * bstring list * int) list) ctxt ctxt'' =  (* FIXME ctxt'' ?? *)
   1.139    let
   1.140      val _ = clean_message quiet_mode "  Proving the simplification rules ...";
   1.141 -    
   1.142 +
   1.143      fun dest_intr r =
   1.144        (the (dest_predicate cs params (HOLogic.dest_Trueprop (Logic.strip_assums_concl r))),
   1.145         Logic.strip_assums_hyp r, Logic.strip_params r);
   1.146      val intr_ts' = map dest_intr intr_ts;
   1.147 +
   1.148      fun prove_eq c (elim: thm * 'a * 'b) =
   1.149        let
   1.150          val Ts = arg_types_of (length params) c;
   1.151 @@ -447,53 +456,56 @@
   1.152          fun mk_intr_conj (((_, _, us, _), ts, params'), _) =
   1.153            let
   1.154              fun list_ex ([], t) = t
   1.155 -              | list_ex ((a,T)::vars, t) =
   1.156 -                 (HOLogic.exists_const T) $ (Abs(a, T, list_ex(vars,t)));
   1.157 -            val conjs = map2 (curry HOLogic.mk_eq) frees us @ (map HOLogic.dest_Trueprop ts)
   1.158 +              | list_ex ((a, T) :: vars, t) =
   1.159 +                  HOLogic.exists_const T $ Abs (a, T, list_ex (vars, t));
   1.160 +            val conjs = map2 (curry HOLogic.mk_eq) frees us @ (map HOLogic.dest_Trueprop ts);
   1.161            in
   1.162              list_ex (params', if null conjs then @{term True} else foldr1 HOLogic.mk_conj conjs)
   1.163            end;
   1.164 -        val lhs = list_comb (c, params @ frees)
   1.165 +        val lhs = list_comb (c, params @ frees);
   1.166          val rhs =
   1.167 -          if null c_intrs then @{term False} else foldr1 HOLogic.mk_disj (map mk_intr_conj c_intrs)
   1.168 -        val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
   1.169 +          if null c_intrs then @{term False}
   1.170 +          else foldr1 HOLogic.mk_disj (map mk_intr_conj c_intrs);
   1.171 +        val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
   1.172          fun prove_intr1 (i, _) = Subgoal.FOCUS_PREMS (fn {params, prems, ...} =>
   1.173              let
   1.174 -              val (prems', last_prem) = split_last prems
   1.175 +              val (prems', last_prem) = split_last prems;
   1.176              in
   1.177 -              EVERY1 (select_disj (length c_intrs) (i + 1))
   1.178 -              THEN EVERY (replicate (length params) (rtac @{thm exI} 1))
   1.179 -              THEN EVERY (map (fn prem => (rtac @{thm conjI} 1 THEN rtac prem 1)) prems')
   1.180 -              THEN rtac last_prem 1
   1.181 -            end) ctxt' 1
   1.182 +              EVERY1 (select_disj (length c_intrs) (i + 1)) THEN
   1.183 +              EVERY (replicate (length params) (rtac @{thm exI} 1)) THEN
   1.184 +              EVERY (map (fn prem => (rtac @{thm conjI} 1 THEN rtac prem 1)) prems') THEN
   1.185 +              rtac last_prem 1
   1.186 +            end) ctxt' 1;
   1.187          fun prove_intr2 (((_, _, us, _), ts, params'), intr) =
   1.188 -          EVERY (replicate (length params') (etac @{thm exE} 1))
   1.189 -          THEN EVERY (replicate (length ts + length us - 1) (etac @{thm conjE} 1))
   1.190 -          THEN Subgoal.FOCUS_PREMS (fn {params, prems, ...} =>
   1.191 +          EVERY (replicate (length params') (etac @{thm exE} 1)) THEN
   1.192 +          EVERY (replicate (length ts + length us - 1) (etac @{thm conjE} 1)) THEN
   1.193 +          Subgoal.FOCUS_PREMS (fn {params, prems, ...} =>
   1.194              let
   1.195 -              val (eqs, prems') = chop (length us) prems
   1.196 -              val rew_thms = map (fn th => th RS @{thm eq_reflection}) eqs
   1.197 +              val (eqs, prems') = chop (length us) prems;
   1.198 +              val rew_thms = map (fn th => th RS @{thm eq_reflection}) eqs;
   1.199              in
   1.200 -              rewrite_goal_tac rew_thms 1
   1.201 -              THEN rtac intr 1
   1.202 -              THEN (EVERY (map (fn p => rtac p 1) prems'))              
   1.203 -            end) ctxt' 1 
   1.204 +              rewrite_goal_tac rew_thms 1 THEN
   1.205 +              rtac intr 1 THEN
   1.206 +              EVERY (map (fn p => rtac p 1) prems')
   1.207 +            end) ctxt' 1;
   1.208        in
   1.209 -        Skip_Proof.prove ctxt' [] [] eq (fn {...} =>
   1.210 -          rtac @{thm iffI} 1 THEN etac (#1 elim) 1
   1.211 -          THEN EVERY (map_index prove_intr1 c_intrs)
   1.212 -          THEN (if null c_intrs then etac @{thm FalseE} 1 else
   1.213 +        Skip_Proof.prove ctxt' [] [] eq (fn _ =>
   1.214 +          rtac @{thm iffI} 1 THEN etac (#1 elim) 1 THEN
   1.215 +          EVERY (map_index prove_intr1 c_intrs) THEN
   1.216 +          (if null c_intrs then etac @{thm FalseE} 1
   1.217 +           else
   1.218              let val (c_intrs', last_c_intr) = split_last c_intrs in
   1.219 -              EVERY (map (fn ci => etac @{thm disjE} 1 THEN prove_intr2 ci) c_intrs')
   1.220 -              THEN prove_intr2 last_c_intr
   1.221 +              EVERY (map (fn ci => etac @{thm disjE} 1 THEN prove_intr2 ci) c_intrs') THEN
   1.222 +              prove_intr2 last_c_intr
   1.223              end))
   1.224          |> rulify
   1.225          |> singleton (Proof_Context.export ctxt' ctxt'')
   1.226 -      end;  
   1.227 +      end;
   1.228    in
   1.229      map2 prove_eq cs elims
   1.230    end;
   1.231 -  
   1.232 +
   1.233 +
   1.234  (* derivation of simplified elimination rules *)
   1.235  
   1.236  local
   1.237 @@ -533,6 +545,7 @@
   1.238  
   1.239  end;
   1.240  
   1.241 +
   1.242  (* inductive_cases *)
   1.243  
   1.244  fun gen_inductive_cases prep_att prep_prop args lthy =
   1.245 @@ -560,31 +573,35 @@
   1.246          in Method.erule 0 rules end))
   1.247      "dynamic case analysis on predicates";
   1.248  
   1.249 +
   1.250  (* derivation of simplified equation *)
   1.251  
   1.252  fun mk_simp_eq ctxt prop =
   1.253    let
   1.254 -    val thy = Proof_Context.theory_of ctxt
   1.255 -    val ctxt' = Variable.auto_fixes prop ctxt
   1.256 -    val lhs_of = fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of
   1.257 -    val substs = Item_Net.retrieve (Equation_Data.get (Context.Proof ctxt)) (HOLogic.dest_Trueprop prop) 
   1.258 +    val thy = Proof_Context.theory_of ctxt;
   1.259 +    val ctxt' = Variable.auto_fixes prop ctxt;
   1.260 +    val lhs_of = fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of;
   1.261 +    val substs =
   1.262 +      Item_Net.retrieve (Equation_Data.get (Context.Proof ctxt)) (HOLogic.dest_Trueprop prop)
   1.263        |> map_filter
   1.264          (fn eq => SOME (Pattern.match thy (lhs_of eq, HOLogic.dest_Trueprop prop)
   1.265              (Vartab.empty, Vartab.empty), eq)
   1.266 -          handle Pattern.MATCH => NONE)
   1.267 -    val (subst, eq) = case substs of
   1.268 +          handle Pattern.MATCH => NONE);
   1.269 +    val (subst, eq) =
   1.270 +      (case substs of
   1.271          [s] => s
   1.272        | _ => error
   1.273 -        ("equations matching pattern " ^ Syntax.string_of_term ctxt prop ^ " is not unique")
   1.274 -    val inst = map (fn v => (cterm_of thy (Var v), cterm_of thy (Envir.subst_term subst (Var v))))
   1.275 -      (Term.add_vars (lhs_of eq) [])
   1.276 -   in
   1.277 +        ("equations matching pattern " ^ Syntax.string_of_term ctxt prop ^ " is not unique"));
   1.278 +    val inst =
   1.279 +      map (fn v => (cterm_of thy (Var v), cterm_of thy (Envir.subst_term subst (Var v))))
   1.280 +        (Term.add_vars (lhs_of eq) []);
   1.281 +  in
   1.282      cterm_instantiate inst eq
   1.283 -    |> Conv.fconv_rule (Conv.arg_conv (Conv.arg_conv
   1.284 -      (Simplifier.full_rewrite (simpset_of ctxt))))
   1.285 +    |> Conv.fconv_rule (Conv.arg_conv (Conv.arg_conv (Simplifier.full_rewrite (simpset_of ctxt))))
   1.286      |> singleton (Variable.export ctxt' ctxt)
   1.287    end
   1.288  
   1.289 +
   1.290  (* inductive simps *)
   1.291  
   1.292  fun gen_inductive_simps prep_att prep_prop args lthy =
   1.293 @@ -598,19 +615,20 @@
   1.294  val inductive_simps = gen_inductive_simps Attrib.intern_src Syntax.read_prop;
   1.295  val inductive_simps_i = gen_inductive_simps (K I) Syntax.check_prop;
   1.296  
   1.297 +
   1.298  (* prove induction rule *)
   1.299  
   1.300  fun prove_indrule quiet_mode cs argTs bs xs rec_const params intr_ts mono
   1.301 -    fp_def rec_preds_defs ctxt ctxt''' =
   1.302 +    fp_def rec_preds_defs ctxt ctxt''' =  (* FIXME ctxt''' ?? *)
   1.303    let
   1.304      val _ = clean_message quiet_mode "  Proving the induction rule ...";
   1.305 -    val thy = Proof_Context.theory_of ctxt;
   1.306  
   1.307      (* predicates for induction rule *)
   1.308  
   1.309      val (pnames, ctxt') = Variable.variant_fixes (mk_names "P" (length cs)) ctxt;
   1.310 -    val preds = map2 (curry Free) pnames
   1.311 -      (map (fn c => arg_types_of (length params) c ---> HOLogic.boolT) cs);
   1.312 +    val preds =
   1.313 +      map2 (curry Free) pnames
   1.314 +        (map (fn c => arg_types_of (length params) c ---> HOLogic.boolT) cs);
   1.315  
   1.316      (* transform an introduction rule into a premise for induction rule *)
   1.317  
   1.318 @@ -625,12 +643,12 @@
   1.319                  val P = list_comb (nth preds i, map (incr_boundvars k) ys @ bs);
   1.320                  val Q = list_abs (mk_names "x" k ~~ Ts,
   1.321                    HOLogic.mk_binop inductive_conj_name
   1.322 -                    (list_comb (incr_boundvars k s, bs), P))
   1.323 +                    (list_comb (incr_boundvars k s, bs), P));
   1.324                in (Q, case Ts of [] => SOME (s, P) | _ => NONE) end
   1.325            | NONE =>
   1.326                (case s of
   1.327 -                (t $ u) => (fst (subst t) $ fst (subst u), NONE)
   1.328 -              | (Abs (a, T, t)) => (Abs (a, T, fst (subst t)), NONE)
   1.329 +                t $ u => (fst (subst t) $ fst (subst u), NONE)
   1.330 +              | Abs (a, T, t) => (Abs (a, T, fst (subst t)), NONE)
   1.331                | _ => (s, NONE)));
   1.332  
   1.333          fun mk_prem s prems =
   1.334 @@ -638,9 +656,8 @@
   1.335              (_, SOME (t, u)) => t :: u :: prems
   1.336            | (t, _) => t :: prems);
   1.337  
   1.338 -        val SOME (_, i, ys, _) = dest_predicate cs params
   1.339 -          (HOLogic.dest_Trueprop (Logic.strip_assums_concl r))
   1.340 -
   1.341 +        val SOME (_, i, ys, _) =
   1.342 +          dest_predicate cs params (HOLogic.dest_Trueprop (Logic.strip_assums_concl r));
   1.343        in
   1.344          list_all_free (Logic.strip_params r,
   1.345            Logic.list_implies (map HOLogic.mk_Trueprop (fold_rev mk_prem
   1.346 @@ -654,27 +671,28 @@
   1.347      (* make conclusions for induction rules *)
   1.348  
   1.349      val Tss = map (binder_types o fastype_of) preds;
   1.350 -    val (xnames, ctxt'') =
   1.351 -      Variable.variant_fixes (mk_names "x" (length (flat Tss))) ctxt';
   1.352 -    val mutual_ind_concl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
   1.353 +    val (xnames, ctxt'') = Variable.variant_fixes (mk_names "x" (length (flat Tss))) ctxt';
   1.354 +    val mutual_ind_concl =
   1.355 +      HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
   1.356          (map (fn (((xnames, Ts), c), P) =>
   1.357 -           let val frees = map Free (xnames ~~ Ts)
   1.358 -           in HOLogic.mk_imp
   1.359 -             (list_comb (c, params @ frees), list_comb (P, frees))
   1.360 -           end) (unflat Tss xnames ~~ Tss ~~ cs ~~ preds)));
   1.361 +          let val frees = map Free (xnames ~~ Ts)
   1.362 +          in HOLogic.mk_imp (list_comb (c, params @ frees), list_comb (P, frees)) end)
   1.363 +        (unflat Tss xnames ~~ Tss ~~ cs ~~ preds)));
   1.364  
   1.365  
   1.366      (* make predicate for instantiation of abstract induction rule *)
   1.367  
   1.368 -    val ind_pred = fold_rev lambda (bs @ xs) (foldr1 HOLogic.mk_conj
   1.369 -      (map_index (fn (i, P) => fold_rev (curry HOLogic.mk_imp)
   1.370 -         (make_bool_args HOLogic.mk_not I bs i)
   1.371 -         (list_comb (P, make_args' argTs xs (binder_types (fastype_of P))))) preds));
   1.372 +    val ind_pred =
   1.373 +      fold_rev lambda (bs @ xs) (foldr1 HOLogic.mk_conj
   1.374 +        (map_index (fn (i, P) => fold_rev (curry HOLogic.mk_imp)
   1.375 +           (make_bool_args HOLogic.mk_not I bs i)
   1.376 +           (list_comb (P, make_args' argTs xs (binder_types (fastype_of P))))) preds));
   1.377  
   1.378 -    val ind_concl = HOLogic.mk_Trueprop
   1.379 -      (HOLogic.mk_binrel @{const_name Orderings.less_eq} (rec_const, ind_pred));
   1.380 +    val ind_concl =
   1.381 +      HOLogic.mk_Trueprop
   1.382 +        (HOLogic.mk_binrel @{const_name Orderings.less_eq} (rec_const, ind_pred));
   1.383  
   1.384 -    val raw_fp_induct = (mono RS (fp_def RS @{thm def_lfp_induct}));
   1.385 +    val raw_fp_induct = mono RS (fp_def RS @{thm def_lfp_induct});
   1.386  
   1.387      val induct = Skip_Proof.prove ctxt'' [] ind_prems ind_concl
   1.388        (fn {prems, ...} => EVERY
   1.389 @@ -701,7 +719,7 @@
   1.390              REPEAT (eresolve_tac [@{thm le_funE}, @{thm le_boolE}] 1),
   1.391              atac 1,
   1.392              rewrite_goals_tac simp_thms',
   1.393 -            atac 1])])
   1.394 +            atac 1])]);
   1.395  
   1.396    in singleton (Proof_Context.export ctxt'' ctxt''') (induct RS lemma) end;
   1.397  
   1.398 @@ -717,10 +735,12 @@
   1.399      val argTs = fold (combine (op =) o arg_types_of (length params)) cs [];
   1.400      val k = log 2 1 (length cs);
   1.401      val predT = replicate k HOLogic.boolT ---> argTs ---> HOLogic.boolT;
   1.402 -    val p :: xs = map Free (Variable.variant_frees lthy intr_ts
   1.403 -      (("p", predT) :: (mk_names "x" (length argTs) ~~ argTs)));
   1.404 -    val bs = map Free (Variable.variant_frees lthy (p :: xs @ intr_ts)
   1.405 -      (map (rpair HOLogic.boolT) (mk_names "b" k)));
   1.406 +    val p :: xs =
   1.407 +      map Free (Variable.variant_frees lthy intr_ts
   1.408 +        (("p", predT) :: (mk_names "x" (length argTs) ~~ argTs)));
   1.409 +    val bs =
   1.410 +      map Free (Variable.variant_frees lthy (p :: xs @ intr_ts)
   1.411 +        (map (rpair HOLogic.boolT) (mk_names "b" k)));
   1.412  
   1.413      fun subst t =
   1.414        (case dest_predicate cs params t of
   1.415 @@ -746,23 +766,24 @@
   1.416  
   1.417      fun transform_rule r =
   1.418        let
   1.419 -        val SOME (_, i, ts, (Ts, _)) = dest_predicate cs params
   1.420 -          (HOLogic.dest_Trueprop (Logic.strip_assums_concl r));
   1.421 -        val ps = make_bool_args HOLogic.mk_not I bs i @
   1.422 +        val SOME (_, i, ts, (Ts, _)) =
   1.423 +          dest_predicate cs params (HOLogic.dest_Trueprop (Logic.strip_assums_concl r));
   1.424 +        val ps =
   1.425 +          make_bool_args HOLogic.mk_not I bs i @
   1.426            map HOLogic.mk_eq (make_args' argTs xs Ts ~~ ts) @
   1.427 -          map (subst o HOLogic.dest_Trueprop)
   1.428 -            (Logic.strip_assums_hyp r)
   1.429 +          map (subst o HOLogic.dest_Trueprop) (Logic.strip_assums_hyp r);
   1.430        in
   1.431          fold_rev (fn (x, T) => fn P => HOLogic.exists_const T $ Abs (x, T, P))
   1.432            (Logic.strip_params r)
   1.433            (if null ps then HOLogic.true_const else foldr1 HOLogic.mk_conj ps)
   1.434 -      end
   1.435 +      end;
   1.436  
   1.437      (* make a disjunction of all introduction rules *)
   1.438  
   1.439 -    val fp_fun = fold_rev lambda (p :: bs @ xs)
   1.440 -      (if null intr_ts then HOLogic.false_const
   1.441 -       else foldr1 HOLogic.mk_disj (map transform_rule intr_ts));
   1.442 +    val fp_fun =
   1.443 +      fold_rev lambda (p :: bs @ xs)
   1.444 +        (if null intr_ts then HOLogic.false_const
   1.445 +         else foldr1 HOLogic.mk_disj (map transform_rule intr_ts));
   1.446  
   1.447      (* add definiton of recursive predicates to theory *)
   1.448  
   1.449 @@ -779,16 +800,17 @@
   1.450             fold_rev lambda params
   1.451               (Const (fp_name, (predT --> predT) --> predT) $ fp_fun)))
   1.452        ||> Local_Theory.restore_naming lthy;
   1.453 -    val fp_def' = Simplifier.rewrite (HOL_basic_ss addsimps [fp_def])
   1.454 -      (cterm_of (Proof_Context.theory_of lthy') (list_comb (rec_const, params)));
   1.455 +    val fp_def' =
   1.456 +      Simplifier.rewrite (HOL_basic_ss addsimps [fp_def])
   1.457 +        (cterm_of (Proof_Context.theory_of lthy') (list_comb (rec_const, params)));
   1.458      val specs =
   1.459        if length cs < 2 then []
   1.460        else
   1.461          map_index (fn (i, (name_mx, c)) =>
   1.462            let
   1.463              val Ts = arg_types_of (length params) c;
   1.464 -            val xs = map Free (Variable.variant_frees lthy intr_ts
   1.465 -              (mk_names "x" (length Ts) ~~ Ts))
   1.466 +            val xs =
   1.467 +              map Free (Variable.variant_frees lthy intr_ts (mk_names "x" (length Ts) ~~ Ts));
   1.468            in
   1.469              (name_mx, (apfst Binding.conceal Attrib.empty_binding, fold_rev lambda (params @ xs)
   1.470                (list_comb (rec_const, params @ make_bool_args' bs i @
   1.471 @@ -849,7 +871,7 @@
   1.472          ((rec_qualified true (Binding.name (coind_prefix coind ^ "induct")),
   1.473            map (Attrib.internal o K) (#2 induct)), [rulify (#1 induct)]);
   1.474  
   1.475 -    val (eqs', lthy3) = lthy2 |> 
   1.476 +    val (eqs', lthy3) = lthy2 |>
   1.477        fold_map (fn (name, eq) => Local_Theory.note
   1.478            ((Binding.qualify true (Long_Name.base_name name) (Binding.name "simps"),
   1.479              [Attrib.internal (K add_equation)]), [eq])
   1.480 @@ -913,13 +935,14 @@
   1.481           prove_indrule quiet_mode cs argTs bs xs rec_const params intr_ts mono fp_def
   1.482             rec_preds_defs lthy2 lthy1);
   1.483      val eqs =
   1.484 -      if no_elim then [] else prove_eqs quiet_mode cs params intr_ts intrs elims lthy2 lthy1
   1.485 +      if no_elim then [] else prove_eqs quiet_mode cs params intr_ts intrs elims lthy2 lthy1;
   1.486  
   1.487 -    val elims' = map (fn (th, ns, i) => (rulify th, ns, i)) elims
   1.488 -    val intrs' = map rulify intrs
   1.489 +    val elims' = map (fn (th, ns, i) => (rulify th, ns, i)) elims;
   1.490 +    val intrs' = map rulify intrs;
   1.491  
   1.492 -    val (intrs'', elims'', eqs', induct, inducts, lthy3) = declare_rules rec_name coind no_ind
   1.493 -      cnames preds intrs' intr_names intr_atts elims' eqs raw_induct lthy1;
   1.494 +    val (intrs'', elims'', eqs', induct, inducts, lthy3) =
   1.495 +      declare_rules rec_name coind no_ind
   1.496 +        cnames preds intrs' intr_names intr_atts elims' eqs raw_induct lthy1;
   1.497  
   1.498      val result =
   1.499        {preds = preds,
   1.500 @@ -1033,10 +1056,9 @@
   1.501  (* read off parameters of inductive predicate from raw induction rule *)
   1.502  fun params_of induct =
   1.503    let
   1.504 -    val (_ $ t $ u :: _) =
   1.505 -      HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induct));
   1.506 +    val (_ $ t $ u :: _) = HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induct));
   1.507      val (_, ts) = strip_comb t;
   1.508 -    val (_, us) = strip_comb u
   1.509 +    val (_, us) = strip_comb u;
   1.510    in
   1.511      List.take (ts, length ts - length us)
   1.512    end;
   1.513 @@ -1065,13 +1087,15 @@
   1.514      fun mtch (t, u) =
   1.515        let
   1.516          val params = Logic.strip_params t;
   1.517 -        val vars = map (Var o apfst (rpair 0))
   1.518 -          (Name.variant_list used (map fst params) ~~ map snd params);
   1.519 -        val ts = map (curry subst_bounds (rev vars))
   1.520 -          (List.drop (Logic.strip_assums_hyp t, arity));
   1.521 +        val vars =
   1.522 +          map (Var o apfst (rpair 0))
   1.523 +            (Name.variant_list used (map fst params) ~~ map snd params);
   1.524 +        val ts =
   1.525 +          map (curry subst_bounds (rev vars))
   1.526 +            (List.drop (Logic.strip_assums_hyp t, arity));
   1.527          val us = Logic.strip_imp_prems u;
   1.528 -        val tab = fold (Pattern.first_order_match thy) (ts ~~ us)
   1.529 -          (Vartab.empty, Vartab.empty);
   1.530 +        val tab =
   1.531 +          fold (Pattern.first_order_match thy) (ts ~~ us) (Vartab.empty, Vartab.empty);
   1.532        in
   1.533          map (Envir.subst_term tab) vars
   1.534        end