src/HOL/Tools/Function/mutual.ML
changeset 34232 36a2a3029fd3
parent 33855 cd8acf137c9c
child 35624 c4e29a0bb8c1
     1.1 --- a/src/HOL/Tools/Function/mutual.ML	Sat Jan 02 23:18:58 2010 +0100
     1.2 +++ b/src/HOL/Tools/Function/mutual.ML	Sat Jan 02 23:18:58 2010 +0100
     1.3 @@ -9,13 +9,13 @@
     1.4  sig
     1.5  
     1.6    val prepare_function_mutual : Function_Common.function_config
     1.7 -                              -> string (* defname *)
     1.8 -                              -> ((string * typ) * mixfix) list
     1.9 -                              -> term list
    1.10 -                              -> local_theory
    1.11 -                              -> ((thm (* goalstate *)
    1.12 -                                   * (thm -> Function_Common.function_result) (* proof continuation *)
    1.13 -                                  ) * local_theory)
    1.14 +    -> string (* defname *)
    1.15 +    -> ((string * typ) * mixfix) list
    1.16 +    -> term list
    1.17 +    -> local_theory
    1.18 +    -> ((thm (* goalstate *)
    1.19 +        * (thm -> Function_Common.function_result) (* proof continuation *)
    1.20 +       ) * local_theory)
    1.21  
    1.22  end
    1.23  
    1.24 @@ -28,282 +28,269 @@
    1.25  
    1.26  type qgar = string * (string * typ) list * term list * term list * term
    1.27  
    1.28 -datatype mutual_part =
    1.29 -  MutualPart of 
    1.30 -   {
    1.31 -    i : int,
    1.32 -    i' : int,
    1.33 -    fvar : string * typ,
    1.34 -    cargTs: typ list,
    1.35 -    f_def: term,
    1.36 +datatype mutual_part = MutualPart of
    1.37 + {i : int,
    1.38 +  i' : int,
    1.39 +  fvar : string * typ,
    1.40 +  cargTs: typ list,
    1.41 +  f_def: term,
    1.42  
    1.43 -    f: term option,
    1.44 -    f_defthm : thm option
    1.45 -   }
    1.46 -   
    1.47 +  f: term option,
    1.48 +  f_defthm : thm option}
    1.49  
    1.50 -datatype mutual_info =
    1.51 -  Mutual of 
    1.52 -   { 
    1.53 -    n : int,
    1.54 -    n' : int,
    1.55 -    fsum_var : string * typ,
    1.56 +datatype mutual_info = Mutual of
    1.57 + {n : int,
    1.58 +  n' : int,
    1.59 +  fsum_var : string * typ,
    1.60  
    1.61 -    ST: typ,
    1.62 -    RST: typ,
    1.63 +  ST: typ,
    1.64 +  RST: typ,
    1.65  
    1.66 -    parts: mutual_part list,
    1.67 -    fqgars: qgar list,
    1.68 -    qglrs: ((string * typ) list * term list * term * term) list,
    1.69 +  parts: mutual_part list,
    1.70 +  fqgars: qgar list,
    1.71 +  qglrs: ((string * typ) list * term list * term * term) list,
    1.72  
    1.73 -    fsum : term option
    1.74 -   }
    1.75 +  fsum : term option}
    1.76  
    1.77  fun mutual_induct_Pnames n =
    1.78 -    if n < 5 then fst (chop n ["P","Q","R","S"])
    1.79 -    else map (fn i => "P" ^ string_of_int i) (1 upto n)
    1.80 +  if n < 5 then fst (chop n ["P","Q","R","S"])
    1.81 +  else map (fn i => "P" ^ string_of_int i) (1 upto n)
    1.82  
    1.83  fun get_part fname =
    1.84 -    the o find_first (fn (MutualPart {fvar=(n,_), ...}) => n = fname)
    1.85 -                     
    1.86 +  the o find_first (fn (MutualPart {fvar=(n,_), ...}) => n = fname)
    1.87 +
    1.88  (* FIXME *)
    1.89  fun mk_prod_abs e (t1, t2) =
    1.90 -    let
    1.91 -      val bTs = rev (map snd e)
    1.92 -      val T1 = fastype_of1 (bTs, t1)
    1.93 -      val T2 = fastype_of1 (bTs, t2)
    1.94 -    in
    1.95 -      HOLogic.pair_const T1 T2 $ t1 $ t2
    1.96 -    end;
    1.97 -
    1.98 +  let
    1.99 +    val bTs = rev (map snd e)
   1.100 +    val T1 = fastype_of1 (bTs, t1)
   1.101 +    val T2 = fastype_of1 (bTs, t2)
   1.102 +  in
   1.103 +    HOLogic.pair_const T1 T2 $ t1 $ t2
   1.104 +  end
   1.105  
   1.106  fun analyze_eqs ctxt defname fs eqs =
   1.107 -    let
   1.108 -      val num = length fs
   1.109 -        val fqgars = map (split_def ctxt) eqs
   1.110 -        val arity_of = map (fn (fname,_,_,args,_) => (fname, length args)) fqgars
   1.111 -                       |> AList.lookup (op =) #> the
   1.112 +  let
   1.113 +    val num = length fs
   1.114 +    val fqgars = map (split_def ctxt) eqs
   1.115 +    val arity_of = map (fn (fname,_,_,args,_) => (fname, length args)) fqgars
   1.116 +      |> AList.lookup (op =) #> the
   1.117  
   1.118 -        fun curried_types (fname, fT) =
   1.119 -            let
   1.120 -              val (caTs, uaTs) = chop (arity_of fname) (binder_types fT)
   1.121 -            in
   1.122 -                (caTs, uaTs ---> body_type fT)
   1.123 -            end
   1.124 +    fun curried_types (fname, fT) =
   1.125 +      let
   1.126 +        val (caTs, uaTs) = chop (arity_of fname) (binder_types fT)
   1.127 +      in
   1.128 +        (caTs, uaTs ---> body_type fT)
   1.129 +      end
   1.130  
   1.131 -        val (caTss, resultTs) = split_list (map curried_types fs)
   1.132 -        val argTs = map (foldr1 HOLogic.mk_prodT) caTss
   1.133 +    val (caTss, resultTs) = split_list (map curried_types fs)
   1.134 +    val argTs = map (foldr1 HOLogic.mk_prodT) caTss
   1.135  
   1.136 -        val dresultTs = distinct (op =) resultTs
   1.137 -        val n' = length dresultTs
   1.138 +    val dresultTs = distinct (op =) resultTs
   1.139 +    val n' = length dresultTs
   1.140  
   1.141 -        val RST = Balanced_Tree.make (uncurry SumTree.mk_sumT) dresultTs
   1.142 -        val ST = Balanced_Tree.make (uncurry SumTree.mk_sumT) argTs
   1.143 +    val RST = Balanced_Tree.make (uncurry SumTree.mk_sumT) dresultTs
   1.144 +    val ST = Balanced_Tree.make (uncurry SumTree.mk_sumT) argTs
   1.145  
   1.146 -        val fsum_type = ST --> RST
   1.147 +    val fsum_type = ST --> RST
   1.148  
   1.149 -        val ([fsum_var_name], _) = Variable.add_fixes [ defname ^ "_sum" ] ctxt
   1.150 -        val fsum_var = (fsum_var_name, fsum_type)
   1.151 +    val ([fsum_var_name], _) = Variable.add_fixes [ defname ^ "_sum" ] ctxt
   1.152 +    val fsum_var = (fsum_var_name, fsum_type)
   1.153  
   1.154 -        fun define (fvar as (n, _)) caTs resultT i =
   1.155 -            let
   1.156 -                val vars = map_index (fn (j,T) => Free ("x" ^ string_of_int j, T)) caTs (* FIXME: Bind xs properly *)
   1.157 -                val i' = find_index (fn Ta => Ta = resultT) dresultTs + 1 
   1.158 +    fun define (fvar as (n, _)) caTs resultT i =
   1.159 +      let
   1.160 +        val vars = map_index (fn (j,T) => Free ("x" ^ string_of_int j, T)) caTs (* FIXME: Bind xs properly *)
   1.161 +        val i' = find_index (fn Ta => Ta = resultT) dresultTs + 1
   1.162  
   1.163 -                val f_exp = SumTree.mk_proj RST n' i' (Free fsum_var $ SumTree.mk_inj ST num i (foldr1 HOLogic.mk_prod vars))
   1.164 -                val def = Term.abstract_over (Free fsum_var, fold_rev lambda vars f_exp)
   1.165 +        val f_exp = SumTree.mk_proj RST n' i' (Free fsum_var $ SumTree.mk_inj ST num i (foldr1 HOLogic.mk_prod vars))
   1.166 +        val def = Term.abstract_over (Free fsum_var, fold_rev lambda vars f_exp)
   1.167  
   1.168 -                val rew = (n, fold_rev lambda vars f_exp)
   1.169 -            in
   1.170 -                (MutualPart {i=i, i'=i', fvar=fvar,cargTs=caTs,f_def=def,f=NONE,f_defthm=NONE}, rew)
   1.171 -            end
   1.172 -            
   1.173 -        val (parts, rews) = split_list (map4 define fs caTss resultTs (1 upto num))
   1.174 +        val rew = (n, fold_rev lambda vars f_exp)
   1.175 +      in
   1.176 +        (MutualPart {i=i, i'=i', fvar=fvar,cargTs=caTs,f_def=def,f=NONE,f_defthm=NONE}, rew)
   1.177 +      end
   1.178 +
   1.179 +    val (parts, rews) = split_list (map4 define fs caTss resultTs (1 upto num))
   1.180  
   1.181 -        fun convert_eqs (f, qs, gs, args, rhs) =
   1.182 -            let
   1.183 -              val MutualPart {i, i', ...} = get_part f parts
   1.184 -            in
   1.185 -              (qs, gs, SumTree.mk_inj ST num i (foldr1 (mk_prod_abs qs) args),
   1.186 -               SumTree.mk_inj RST n' i' (replace_frees rews rhs)
   1.187 -                               |> Envir.beta_norm)
   1.188 -            end
   1.189 +    fun convert_eqs (f, qs, gs, args, rhs) =
   1.190 +      let
   1.191 +        val MutualPart {i, i', ...} = get_part f parts
   1.192 +      in
   1.193 +        (qs, gs, SumTree.mk_inj ST num i (foldr1 (mk_prod_abs qs) args),
   1.194 +         SumTree.mk_inj RST n' i' (replace_frees rews rhs)
   1.195 +         |> Envir.beta_norm)
   1.196 +      end
   1.197  
   1.198 -        val qglrs = map convert_eqs fqgars
   1.199 -    in
   1.200 -        Mutual {n=num, n'=n', fsum_var=fsum_var, ST=ST, RST=RST, 
   1.201 -                parts=parts, fqgars=fqgars, qglrs=qglrs, fsum=NONE}
   1.202 -    end
   1.203 -
   1.204 -
   1.205 -
   1.206 +    val qglrs = map convert_eqs fqgars
   1.207 +  in
   1.208 +    Mutual {n=num, n'=n', fsum_var=fsum_var, ST=ST, RST=RST,
   1.209 +      parts=parts, fqgars=fqgars, qglrs=qglrs, fsum=NONE}
   1.210 +  end
   1.211  
   1.212  fun define_projections fixes mutual fsum lthy =
   1.213 -    let
   1.214 -      fun def ((MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs, f_def, ...}), (_, mixfix)) lthy =
   1.215 -          let
   1.216 -            val ((f, (_, f_defthm)), lthy') =
   1.217 -              Local_Theory.define
   1.218 -                ((Binding.name fname, mixfix),
   1.219 -                  ((Binding.conceal (Binding.name (fname ^ "_def")), []),
   1.220 -                  Term.subst_bound (fsum, f_def))) lthy
   1.221 -          in
   1.222 -            (MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs=cargTs, f_def=f_def,
   1.223 -                         f=SOME f, f_defthm=SOME f_defthm },
   1.224 -             lthy')
   1.225 -          end
   1.226 -          
   1.227 -      val Mutual { n, n', fsum_var, ST, RST, parts, fqgars, qglrs, ... } = mutual
   1.228 -      val (parts', lthy') = fold_map def (parts ~~ fixes) lthy
   1.229 -    in
   1.230 -      (Mutual { n=n, n'=n', fsum_var=fsum_var, ST=ST, RST=RST, parts=parts',
   1.231 -                fqgars=fqgars, qglrs=qglrs, fsum=SOME fsum },
   1.232 -       lthy')
   1.233 -    end
   1.234 +  let
   1.235 +    fun def ((MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs, f_def, ...}), (_, mixfix)) lthy =
   1.236 +      let
   1.237 +        val ((f, (_, f_defthm)), lthy') =
   1.238 +          Local_Theory.define
   1.239 +            ((Binding.name fname, mixfix),
   1.240 +              ((Binding.conceal (Binding.name (fname ^ "_def")), []),
   1.241 +              Term.subst_bound (fsum, f_def))) lthy
   1.242 +      in
   1.243 +        (MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs=cargTs, f_def=f_def,
   1.244 +           f=SOME f, f_defthm=SOME f_defthm },
   1.245 +         lthy')
   1.246 +      end
   1.247  
   1.248 +    val Mutual { n, n', fsum_var, ST, RST, parts, fqgars, qglrs, ... } = mutual
   1.249 +    val (parts', lthy') = fold_map def (parts ~~ fixes) lthy
   1.250 +  in
   1.251 +    (Mutual { n=n, n'=n', fsum_var=fsum_var, ST=ST, RST=RST, parts=parts',
   1.252 +       fqgars=fqgars, qglrs=qglrs, fsum=SOME fsum },
   1.253 +     lthy')
   1.254 +  end
   1.255  
   1.256  fun in_context ctxt (f, pre_qs, pre_gs, pre_args, pre_rhs) F =
   1.257 -    let
   1.258 -      val thy = ProofContext.theory_of ctxt
   1.259 -                
   1.260 -      val oqnames = map fst pre_qs
   1.261 -      val (qs, _) = Variable.variant_fixes oqnames ctxt
   1.262 -        |>> map2 (fn (_, T) => fn n => Free (n, T)) pre_qs
   1.263 -                        
   1.264 -      fun inst t = subst_bounds (rev qs, t)
   1.265 -      val gs = map inst pre_gs
   1.266 -      val args = map inst pre_args
   1.267 -      val rhs = inst pre_rhs
   1.268 +  let
   1.269 +    val thy = ProofContext.theory_of ctxt
   1.270 +
   1.271 +    val oqnames = map fst pre_qs
   1.272 +    val (qs, _) = Variable.variant_fixes oqnames ctxt
   1.273 +      |>> map2 (fn (_, T) => fn n => Free (n, T)) pre_qs
   1.274 +
   1.275 +    fun inst t = subst_bounds (rev qs, t)
   1.276 +    val gs = map inst pre_gs
   1.277 +    val args = map inst pre_args
   1.278 +    val rhs = inst pre_rhs
   1.279  
   1.280 -      val cqs = map (cterm_of thy) qs
   1.281 -      val ags = map (assume o cterm_of thy) gs
   1.282 +    val cqs = map (cterm_of thy) qs
   1.283 +    val ags = map (assume o cterm_of thy) gs
   1.284  
   1.285 -      val import = fold forall_elim cqs
   1.286 -                   #> fold Thm.elim_implies ags
   1.287 +    val import = fold forall_elim cqs
   1.288 +      #> fold Thm.elim_implies ags
   1.289  
   1.290 -      val export = fold_rev (implies_intr o cprop_of) ags
   1.291 -                   #> fold_rev forall_intr_rename (oqnames ~~ cqs)
   1.292 -    in
   1.293 -      F ctxt (f, qs, gs, args, rhs) import export
   1.294 -    end
   1.295 -
   1.296 -fun recover_mutual_psimp all_orig_fdefs parts ctxt (fname, _, _, args, rhs) import (export : thm -> thm) sum_psimp_eq =
   1.297 -    let
   1.298 -      val (MutualPart {f=SOME f, ...}) = get_part fname parts
   1.299 +    val export = fold_rev (implies_intr o cprop_of) ags
   1.300 +      #> fold_rev forall_intr_rename (oqnames ~~ cqs)
   1.301 +  in
   1.302 +    F ctxt (f, qs, gs, args, rhs) import export
   1.303 +  end
   1.304  
   1.305 -      val psimp = import sum_psimp_eq
   1.306 -      val (simp, restore_cond) = case cprems_of psimp of
   1.307 -                                   [] => (psimp, I)
   1.308 -                                 | [cond] => (implies_elim psimp (assume cond), implies_intr cond)
   1.309 -                                 | _ => sys_error "Too many conditions"
   1.310 -    in
   1.311 -      Goal.prove ctxt [] [] 
   1.312 -                 (HOLogic.Trueprop $ HOLogic.mk_eq (list_comb (f, args), rhs))
   1.313 -                 (fn _ => (LocalDefs.unfold_tac ctxt all_orig_fdefs)
   1.314 -                          THEN EqSubst.eqsubst_tac ctxt [0] [simp] 1
   1.315 -                          THEN (simp_tac (simpset_of ctxt addsimps SumTree.proj_in_rules)) 1)
   1.316 -        |> restore_cond 
   1.317 -        |> export
   1.318 -    end
   1.319 +fun recover_mutual_psimp all_orig_fdefs parts ctxt (fname, _, _, args, rhs)
   1.320 +  import (export : thm -> thm) sum_psimp_eq =
   1.321 +  let
   1.322 +    val (MutualPart {f=SOME f, ...}) = get_part fname parts
   1.323 +
   1.324 +    val psimp = import sum_psimp_eq
   1.325 +    val (simp, restore_cond) =
   1.326 +      case cprems_of psimp of
   1.327 +        [] => (psimp, I)
   1.328 +      | [cond] => (implies_elim psimp (assume cond), implies_intr cond)
   1.329 +      | _ => sys_error "Too many conditions"
   1.330  
   1.331 +  in
   1.332 +    Goal.prove ctxt [] []
   1.333 +      (HOLogic.Trueprop $ HOLogic.mk_eq (list_comb (f, args), rhs))
   1.334 +      (fn _ => (LocalDefs.unfold_tac ctxt all_orig_fdefs)
   1.335 +         THEN EqSubst.eqsubst_tac ctxt [0] [simp] 1
   1.336 +         THEN (simp_tac (simpset_of ctxt addsimps SumTree.proj_in_rules)) 1)
   1.337 +    |> restore_cond
   1.338 +    |> export
   1.339 +  end
   1.340  
   1.341 -(* FIXME HACK *)
   1.342  fun mk_applied_form ctxt caTs thm =
   1.343 -    let
   1.344 -      val thy = ProofContext.theory_of ctxt
   1.345 -      val xs = map_index (fn (i,T) => cterm_of thy (Free ("x" ^ string_of_int i, T))) caTs (* FIXME: Bind xs properly *)
   1.346 -    in
   1.347 -      fold (fn x => fn thm => combination thm (reflexive x)) xs thm
   1.348 -           |> Conv.fconv_rule (Thm.beta_conversion true)
   1.349 -           |> fold_rev forall_intr xs
   1.350 -           |> Thm.forall_elim_vars 0
   1.351 -    end
   1.352 -
   1.353 +  let
   1.354 +    val thy = ProofContext.theory_of ctxt
   1.355 +    val xs = map_index (fn (i,T) => cterm_of thy (Free ("x" ^ string_of_int i, T))) caTs (* FIXME: Bind xs properly *)
   1.356 +  in
   1.357 +    fold (fn x => fn thm => combination thm (reflexive x)) xs thm
   1.358 +    |> Conv.fconv_rule (Thm.beta_conversion true)
   1.359 +    |> fold_rev forall_intr xs
   1.360 +    |> Thm.forall_elim_vars 0
   1.361 +  end
   1.362  
   1.363  fun mutual_induct_rules lthy induct all_f_defs (Mutual {n, ST, parts, ...}) =
   1.364 -    let
   1.365 -      val cert = cterm_of (ProofContext.theory_of lthy)
   1.366 -      val newPs = map2 (fn Pname => fn MutualPart {cargTs, ...} => 
   1.367 -                                       Free (Pname, cargTs ---> HOLogic.boolT))
   1.368 -                       (mutual_induct_Pnames (length parts))
   1.369 -                       parts
   1.370 -                       
   1.371 -      fun mk_P (MutualPart {cargTs, ...}) P =
   1.372 -          let
   1.373 -            val avars = map_index (fn (i,T) => Var (("a", i), T)) cargTs
   1.374 -            val atup = foldr1 HOLogic.mk_prod avars
   1.375 -          in
   1.376 -            tupled_lambda atup (list_comb (P, avars))
   1.377 -          end
   1.378 -          
   1.379 -      val Ps = map2 mk_P parts newPs
   1.380 -      val case_exp = SumTree.mk_sumcases HOLogic.boolT Ps
   1.381 -                     
   1.382 -      val induct_inst =
   1.383 -          forall_elim (cert case_exp) induct
   1.384 -                      |> full_simplify SumTree.sumcase_split_ss
   1.385 -                      |> full_simplify (HOL_basic_ss addsimps all_f_defs)
   1.386 -          
   1.387 -      fun project rule (MutualPart {cargTs, i, ...}) k =
   1.388 -          let
   1.389 -            val afs = map_index (fn (j,T) => Free ("a" ^ string_of_int (j + k), T)) cargTs (* FIXME! *)
   1.390 -            val inj = SumTree.mk_inj ST n i (foldr1 HOLogic.mk_prod afs)
   1.391 -          in
   1.392 -            (rule
   1.393 -              |> forall_elim (cert inj)
   1.394 -              |> full_simplify SumTree.sumcase_split_ss
   1.395 -              |> fold_rev (forall_intr o cert) (afs @ newPs),
   1.396 -             k + length cargTs)
   1.397 -          end
   1.398 -    in
   1.399 -      fst (fold_map (project induct_inst) parts 0)
   1.400 -    end
   1.401 -    
   1.402 +  let
   1.403 +    val cert = cterm_of (ProofContext.theory_of lthy)
   1.404 +    val newPs =
   1.405 +      map2 (fn Pname => fn MutualPart {cargTs, ...} =>
   1.406 +          Free (Pname, cargTs ---> HOLogic.boolT))
   1.407 +        (mutual_induct_Pnames (length parts)) parts
   1.408 +
   1.409 +    fun mk_P (MutualPart {cargTs, ...}) P =
   1.410 +      let
   1.411 +        val avars = map_index (fn (i,T) => Var (("a", i), T)) cargTs
   1.412 +        val atup = foldr1 HOLogic.mk_prod avars
   1.413 +      in
   1.414 +        tupled_lambda atup (list_comb (P, avars))
   1.415 +      end
   1.416 +
   1.417 +    val Ps = map2 mk_P parts newPs
   1.418 +    val case_exp = SumTree.mk_sumcases HOLogic.boolT Ps
   1.419 +
   1.420 +    val induct_inst =
   1.421 +      forall_elim (cert case_exp) induct
   1.422 +      |> full_simplify SumTree.sumcase_split_ss
   1.423 +      |> full_simplify (HOL_basic_ss addsimps all_f_defs)
   1.424 +
   1.425 +    fun project rule (MutualPart {cargTs, i, ...}) k =
   1.426 +      let
   1.427 +        val afs = map_index (fn (j,T) => Free ("a" ^ string_of_int (j + k), T)) cargTs (* FIXME! *)
   1.428 +        val inj = SumTree.mk_inj ST n i (foldr1 HOLogic.mk_prod afs)
   1.429 +      in
   1.430 +        (rule
   1.431 +         |> forall_elim (cert inj)
   1.432 +         |> full_simplify SumTree.sumcase_split_ss
   1.433 +         |> fold_rev (forall_intr o cert) (afs @ newPs),
   1.434 +         k + length cargTs)
   1.435 +      end
   1.436 +  in
   1.437 +    fst (fold_map (project induct_inst) parts 0)
   1.438 +  end
   1.439  
   1.440  fun mk_partial_rules_mutual lthy inner_cont (m as Mutual {parts, fqgars, ...}) proof =
   1.441 -    let
   1.442 -      val result = inner_cont proof
   1.443 -      val FunctionResult {G, R, cases, psimps, trsimps, simple_pinducts=[simple_pinduct],
   1.444 -        termination, domintros, ...} = result
   1.445 -                                                                                                               
   1.446 -      val (all_f_defs, fs) = map (fn MutualPart {f_defthm = SOME f_def, f = SOME f, cargTs, ...} =>
   1.447 -                                     (mk_applied_form lthy cargTs (symmetric f_def), f))
   1.448 -                                 parts
   1.449 -                             |> split_list
   1.450 +  let
   1.451 +    val result = inner_cont proof
   1.452 +    val FunctionResult {G, R, cases, psimps, trsimps, simple_pinducts=[simple_pinduct],
   1.453 +      termination, domintros, ...} = result
   1.454 +
   1.455 +    val (all_f_defs, fs) =
   1.456 +      map (fn MutualPart {f_defthm = SOME f_def, f = SOME f, cargTs, ...} =>
   1.457 +        (mk_applied_form lthy cargTs (symmetric f_def), f))
   1.458 +      parts
   1.459 +      |> split_list
   1.460 +
   1.461 +    val all_orig_fdefs =
   1.462 +      map (fn MutualPart {f_defthm = SOME f_def, ...} => f_def) parts
   1.463 +
   1.464 +    fun mk_mpsimp fqgar sum_psimp =
   1.465 +      in_context lthy fqgar (recover_mutual_psimp all_orig_fdefs parts) sum_psimp
   1.466  
   1.467 -      val all_orig_fdefs = map (fn MutualPart {f_defthm = SOME f_def, ...} => f_def) parts
   1.468 -                           
   1.469 -      fun mk_mpsimp fqgar sum_psimp =
   1.470 -          in_context lthy fqgar (recover_mutual_psimp all_orig_fdefs parts) sum_psimp
   1.471 -          
   1.472 -      val rew_ss = HOL_basic_ss addsimps all_f_defs
   1.473 -      val mpsimps = map2 mk_mpsimp fqgars psimps
   1.474 -      val mtrsimps = map_option (map2 mk_mpsimp fqgars) trsimps
   1.475 -      val minducts = mutual_induct_rules lthy simple_pinduct all_f_defs m
   1.476 -      val mtermination = full_simplify rew_ss termination
   1.477 -      val mdomintros = map_option (map (full_simplify rew_ss)) domintros
   1.478 -    in
   1.479 -      FunctionResult { fs=fs, G=G, R=R,
   1.480 -                     psimps=mpsimps, simple_pinducts=minducts,
   1.481 -                     cases=cases, termination=mtermination,
   1.482 -                     domintros=mdomintros,
   1.483 -                     trsimps=mtrsimps}
   1.484 -    end
   1.485 -      
   1.486 +    val rew_ss = HOL_basic_ss addsimps all_f_defs
   1.487 +    val mpsimps = map2 mk_mpsimp fqgars psimps
   1.488 +    val mtrsimps = map_option (map2 mk_mpsimp fqgars) trsimps
   1.489 +    val minducts = mutual_induct_rules lthy simple_pinduct all_f_defs m
   1.490 +    val mtermination = full_simplify rew_ss termination
   1.491 +    val mdomintros = map_option (map (full_simplify rew_ss)) domintros
   1.492 +  in
   1.493 +    FunctionResult { fs=fs, G=G, R=R,
   1.494 +      psimps=mpsimps, simple_pinducts=minducts,
   1.495 +      cases=cases, termination=mtermination,
   1.496 +      domintros=mdomintros, trsimps=mtrsimps}
   1.497 +  end
   1.498 +
   1.499  fun prepare_function_mutual config defname fixes eqss lthy =
   1.500 -    let
   1.501 -      val mutual = analyze_eqs lthy defname (map fst fixes) (map Envir.beta_eta_contract eqss)
   1.502 -      val Mutual {fsum_var=(n, T), qglrs, ...} = mutual
   1.503 -          
   1.504 -      val ((fsum, goalstate, cont), lthy') =
   1.505 -          Function_Core.prepare_function config defname [((n, T), NoSyn)] qglrs lthy
   1.506 -          
   1.507 -      val (mutual', lthy'') = define_projections fixes mutual fsum lthy'
   1.508 +  let
   1.509 +    val mutual as Mutual {fsum_var=(n, T), qglrs, ...} =
   1.510 +      analyze_eqs lthy defname (map fst fixes) (map Envir.beta_eta_contract eqss)
   1.511 +
   1.512 +    val ((fsum, goalstate, cont), lthy') =
   1.513 +      Function_Core.prepare_function config defname [((n, T), NoSyn)] qglrs lthy
   1.514  
   1.515 -      val mutual_cont = mk_partial_rules_mutual lthy'' cont mutual'
   1.516 -    in
   1.517 -      ((goalstate, mutual_cont), lthy'')
   1.518 -    end
   1.519 +    val (mutual', lthy'') = define_projections fixes mutual fsum lthy'
   1.520  
   1.521 -    
   1.522 +    val mutual_cont = mk_partial_rules_mutual lthy'' cont mutual'
   1.523 +  in
   1.524 +    ((goalstate, mutual_cont), lthy'')
   1.525 +  end
   1.526 +
   1.527  end