src/HOL/Tools/function_package/mutual.ML
changeset 23189 4574ab8f3b21
parent 22733 0b14bb35be90
child 23203 a5026e73cfcf
     1.1 --- a/src/HOL/Tools/function_package/mutual.ML	Fri Jun 01 15:20:53 2007 +0200
     1.2 +++ b/src/HOL/Tools/function_package/mutual.ML	Fri Jun 01 15:57:45 2007 +0200
     1.3 @@ -13,7 +13,6 @@
     1.4                                -> string (* defname *)
     1.5                                -> ((string * typ) * mixfix) list
     1.6                                -> term list
     1.7 -                              -> string (* default, unparsed term *)
     1.8                                -> local_theory
     1.9                                -> ((thm (* goalstate *)
    1.10                                     * (thm -> FundefCommon.fundef_result) (* proof continuation *)
    1.11 @@ -72,50 +71,6 @@
    1.12      if n < 5 then fst (chop n ["P","Q","R","S"])
    1.13      else map (fn i => "P" ^ string_of_int i) (1 upto n)
    1.14  
    1.15 -
    1.16 -fun open_all_all (Const ("all", _) $ Abs (n, T, b)) = apfst (cons (n, T)) (open_all_all b)
    1.17 -  | open_all_all t = ([], t)
    1.18 -
    1.19 -(* Builds a curried clause description in abstracted form *)
    1.20 -fun split_def ctxt fnames geq arities =
    1.21 -    let
    1.22 -      fun input_error msg = cat_lines [msg, ProofContext.string_of_term ctxt geq]
    1.23 -                            
    1.24 -      val (qs, imp) = open_all_all geq
    1.25 -
    1.26 -      val gs = Logic.strip_imp_prems imp
    1.27 -      val eq = Logic.strip_imp_concl imp
    1.28 -
    1.29 -      val (f_args, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop eq)
    1.30 -      val (head, args) = strip_comb f_args
    1.31 -
    1.32 -      val invalid_head_msg = "Head symbol of left hand side must be " ^ plural "" "one out of " fnames ^ commas_quote fnames
    1.33 -      val fname = fst (dest_Free head)
    1.34 -          handle TERM _ => error (input_error invalid_head_msg)
    1.35 -
    1.36 -      val _ = fname mem fnames orelse error (input_error invalid_head_msg)
    1.37 -
    1.38 -      fun add_bvs t is = add_loose_bnos (t, 0, is)
    1.39 -      val rvs = (add_bvs rhs [] \\ fold add_bvs args [])
    1.40 -                  |> map (fst o nth (rev qs))
    1.41 -                
    1.42 -      val _ = null rvs orelse error (input_error ("Variable" ^ plural " " "s " rvs ^ commas_quote rvs
    1.43 -                                              ^ " occur" ^ plural "s" "" rvs ^ " on right hand side only:"))
    1.44 -
    1.45 -      val _ = forall (forall_aterms (fn Free (n, _) => not (n mem fnames) | _ => true)) gs orelse
    1.46 -                     error (input_error "Recursive Calls not allowed in premises")
    1.47 -
    1.48 -      val k = length args
    1.49 -
    1.50 -      val arities' = case Symtab.lookup arities fname of
    1.51 -                       NONE => Symtab.update (fname, k) arities
    1.52 -                     | SOME i => (i = k orelse
    1.53 -                                  error (input_error ("Function " ^ quote fname ^ " has different numbers of arguments in different equations"));
    1.54 -                                  arities)
    1.55 -    in
    1.56 -      ((fname, qs, gs, args, rhs), arities')
    1.57 -    end
    1.58 -    
    1.59  fun get_part fname =
    1.60      the o find_first (fn (MutualPart {fvar=(n,_), ...}) => n = fname)
    1.61                       
    1.62 @@ -133,7 +88,8 @@
    1.63  fun analyze_eqs ctxt defname fs eqs =
    1.64      let
    1.65          val fnames = map fst fs
    1.66 -        val (fqgars, arities) = fold_map (split_def ctxt fnames) eqs Symtab.empty
    1.67 +        val fqgars = map split_def eqs
    1.68 +        val arities = mk_arities fqgars
    1.69  
    1.70          fun curried_types (fname, fT) =
    1.71              let
    1.72 @@ -325,15 +281,17 @@
    1.73        fun mk_mpsimp fqgar sum_psimp =
    1.74            in_context lthy fqgar (recover_mutual_psimp all_orig_fdefs parts) sum_psimp
    1.75            
    1.76 +      val rew_ss = HOL_basic_ss addsimps all_f_defs
    1.77        val mpsimps = map2 mk_mpsimp fqgars psimps
    1.78        val mtrsimps = map_option (map2 mk_mpsimp fqgars) trsimps
    1.79        val minducts = mutual_induct_rules lthy simple_pinduct all_f_defs m
    1.80 -      val mtermination = full_simplify (HOL_basic_ss addsimps all_f_defs) termination
    1.81 +      val mtermination = full_simplify rew_ss termination
    1.82 +      val mdomintros = map_option (map (full_simplify rew_ss)) domintros
    1.83      in
    1.84        FundefResult { fs=fs, G=G, R=R,
    1.85                       psimps=mpsimps, subset_pinducts=[subset_pinduct], simple_pinducts=minducts,
    1.86                       cases=cases, termination=mtermination,
    1.87 -                     domintros=domintros,
    1.88 +                     domintros=mdomintros,
    1.89                       trsimps=mtrsimps}
    1.90      end
    1.91        
    1.92 @@ -351,13 +309,13 @@
    1.93               |> map (snd #> map snd)                     (* and remove the labels afterwards *)
    1.94  
    1.95  
    1.96 -fun prepare_fundef_mutual config defname fixes eqss default lthy =
    1.97 +fun prepare_fundef_mutual config defname fixes eqss lthy =
    1.98      let
    1.99        val mutual = analyze_eqs lthy defname (map fst fixes) (map Envir.beta_eta_contract eqss)
   1.100        val Mutual {fsum_var=(n, T), qglrs, ...} = mutual
   1.101            
   1.102        val ((fsum, goalstate, cont), lthy') =
   1.103 -          FundefCore.prepare_fundef config defname (n, T, NoSyn) qglrs default lthy
   1.104 +          FundefCore.prepare_fundef config defname [((n, T), NoSyn)] qglrs lthy
   1.105            
   1.106        val (mutual', lthy'') = define_projections fixes mutual fsum lthy'
   1.107