* Preliminary implementation of tail recursion
authorkrauss
Mon Jan 22 17:29:43 2007 +0100 (2007-01-22)
changeset 221660a50d4db234a
parent 22165 eaec72532dd7
child 22167 c3afded569ea
* Preliminary implementation of tail recursion
* Clarified internal interfaces
src/HOL/FunDef.thy
src/HOL/IsaMakefile
src/HOL/Tools/function_package/fundef_common.ML
src/HOL/Tools/function_package/fundef_core.ML
src/HOL/Tools/function_package/fundef_lib.ML
src/HOL/Tools/function_package/fundef_package.ML
src/HOL/Tools/function_package/fundef_prep.ML
src/HOL/Tools/function_package/fundef_proof.ML
src/HOL/Tools/function_package/inductive_wrap.ML
src/HOL/Tools/function_package/mutual.ML
src/HOL/Tools/function_package/termination.ML
src/HOL/ex/Fundefs.thy
     1.1 --- a/src/HOL/FunDef.thy	Mon Jan 22 16:53:33 2007 +0100
     1.2 +++ b/src/HOL/FunDef.thy	Mon Jan 22 17:29:43 2007 +0100
     1.3 @@ -13,13 +13,11 @@
     1.4  ("Tools/function_package/fundef_lib.ML")
     1.5  ("Tools/function_package/inductive_wrap.ML")
     1.6  ("Tools/function_package/context_tree.ML")
     1.7 -("Tools/function_package/fundef_prep.ML")
     1.8 -("Tools/function_package/fundef_proof.ML")
     1.9 +("Tools/function_package/fundef_core.ML")
    1.10  ("Tools/function_package/termination.ML")
    1.11  ("Tools/function_package/mutual.ML")
    1.12  ("Tools/function_package/pattern_split.ML")
    1.13  ("Tools/function_package/fundef_package.ML")
    1.14 -(*("Tools/function_package/fundef_datatype.ML")*)
    1.15  ("Tools/function_package/auto_term.ML")
    1.16  begin
    1.17  
    1.18 @@ -71,6 +69,27 @@
    1.19    done
    1.20  
    1.21  
    1.22 +lemma not_accP_down:
    1.23 +  assumes na: "\<not> accP R x"
    1.24 +  obtains z where "R z x" and "\<not>accP R z"
    1.25 +proof -
    1.26 +  assume a: "\<And>z. \<lbrakk>R z x; \<not> accP R z\<rbrakk> \<Longrightarrow> thesis"
    1.27 +
    1.28 +  show thesis
    1.29 +  proof (cases "\<forall>z. R z x \<longrightarrow> accP R z")
    1.30 +    case True
    1.31 +    hence "\<And>z. R z x \<Longrightarrow> accP R z" by auto
    1.32 +    hence "accP R x"
    1.33 +      by (rule accPI)
    1.34 +    with na show thesis ..
    1.35 +  next
    1.36 +    case False then obtain z where "R z x" and "\<not>accP R z"
    1.37 +      by auto
    1.38 +    with a show thesis .
    1.39 +  qed
    1.40 +qed
    1.41 +
    1.42 +
    1.43  lemma accP_subset:
    1.44    assumes sub: "\<And>x y. R1 x y \<Longrightarrow> R2 x y"
    1.45    shows "\<And>x. accP R2 x \<Longrightarrow> accP R1 x"
    1.46 @@ -195,8 +214,7 @@
    1.47  use "Tools/function_package/fundef_lib.ML"
    1.48  use "Tools/function_package/inductive_wrap.ML"
    1.49  use "Tools/function_package/context_tree.ML"
    1.50 -use "Tools/function_package/fundef_prep.ML"
    1.51 -use "Tools/function_package/fundef_proof.ML"
    1.52 +use "Tools/function_package/fundef_core.ML"
    1.53  use "Tools/function_package/termination.ML"
    1.54  use "Tools/function_package/mutual.ML"
    1.55  use "Tools/function_package/pattern_split.ML"
     2.1 --- a/src/HOL/IsaMakefile	Mon Jan 22 16:53:33 2007 +0100
     2.2 +++ b/src/HOL/IsaMakefile	Mon Jan 22 17:29:43 2007 +0100
     2.3 @@ -107,8 +107,7 @@
     2.4    Tools/function_package/fundef_datatype.ML					\
     2.5    Tools/function_package/fundef_lib.ML						\
     2.6    Tools/function_package/fundef_package.ML					\
     2.7 -  Tools/function_package/fundef_prep.ML						\
     2.8 -  Tools/function_package/fundef_proof.ML					\
     2.9 +  Tools/function_package/fundef_core.ML						\
    2.10    Tools/function_package/inductive_wrap.ML					\
    2.11    Tools/function_package/lexicographic_order.ML					\
    2.12    Tools/function_package/mutual.ML						\
     3.1 --- a/src/HOL/Tools/function_package/fundef_common.ML	Mon Jan 22 16:53:33 2007 +0100
     3.2 +++ b/src/HOL/Tools/function_package/fundef_common.ML	Mon Jan 22 17:29:43 2007 +0100
     3.3 @@ -12,7 +12,6 @@
     3.4  (* Theory Dependencies *)
     3.5  val acc_const_name = "FunDef.accP"
     3.6  
     3.7 -val domintros = ref true;
     3.8  val profile = ref false;
     3.9  
    3.10  fun PROFILE msg = if !profile then timeap_msg msg else I
    3.11 @@ -20,6 +19,7 @@
    3.12  fun mk_acc domT R =
    3.13      Const (acc_const_name, (fastype_of R) --> domT --> HOLogic.boolT) $ R 
    3.14  
    3.15 +(* FIXME, unused *)
    3.16  val function_name = suffix "C"
    3.17  val graph_name = suffix "_graph"
    3.18  val rel_name = suffix "_rel"
    3.19 @@ -35,163 +35,29 @@
    3.20    | Cong of (term * thm * depgraph * ((string * typ) list * thm list * ctx_tree) list)
    3.21    | RCall of (term * ctx_tree)
    3.22  
    3.23 -type glrs = (term list * term list * term * term) list
    3.24  
    3.25  
    3.26 -datatype globals =
    3.27 -   Globals of { 
    3.28 -         fvar: term, 
    3.29 -         domT: typ, 
    3.30 -         ranT: typ,
    3.31 -         h: term, 
    3.32 -         y: term, 
    3.33 -         x: term, 
    3.34 -         z: term, 
    3.35 -         a:term, 
    3.36 -         P: term, 
    3.37 -         D: term, 
    3.38 -         Pbool:term
    3.39 -}
    3.40 -
    3.41 -
    3.42 -datatype rec_call_info = 
    3.43 -  RCInfo of
    3.44 -  {
    3.45 -   RIvs: (string * typ) list,  (* Call context: fixes and assumes *)
    3.46 -   CCas: thm list,
    3.47 -   rcarg: term,                 (* The recursive argument *)
    3.48 -
    3.49 -   llRI: thm,
    3.50 -   h_assum: term
    3.51 -  } 
    3.52 -
    3.53 -
    3.54 -datatype clause_context =
    3.55 -  ClauseContext of
    3.56 -  {
    3.57 -    ctxt : Proof.context,
    3.58 -
    3.59 -    qs : term list,
    3.60 -    gs : term list,
    3.61 -    lhs: term,
    3.62 -    rhs: term,
    3.63 -
    3.64 -    cqs: cterm list,
    3.65 -    ags: thm list,     
    3.66 -    case_hyp : thm
    3.67 -  }
    3.68 -
    3.69 -
    3.70 -fun transfer_clause_ctx thy (ClauseContext { ctxt, qs, gs, lhs, rhs, cqs, ags, case_hyp }) =
    3.71 -    ClauseContext { ctxt = ProofContext.transfer thy ctxt,
    3.72 -                    qs = qs, gs = gs, lhs = lhs, rhs = rhs, cqs = cqs, ags = ags, case_hyp = case_hyp }
    3.73 -
    3.74 -
    3.75 -datatype clause_info =
    3.76 -  ClauseInfo of 
    3.77 -     {
    3.78 -      no: int,
    3.79 -      qglr : ((string * typ) list * term list * term * term),
    3.80 -      cdata : clause_context,
    3.81 -
    3.82 -      tree: ctx_tree,
    3.83 -      lGI: thm,
    3.84 -      RCs: rec_call_info list
    3.85 -     }
    3.86 -
    3.87 -
    3.88 -
    3.89 -
    3.90 -type qgar = string * (string * typ) list * term list * term list * term
    3.91 -
    3.92 -fun name_of_fqgar (f, _, _, _, _) = f
    3.93 -
    3.94 -datatype mutual_part =
    3.95 -  MutualPart of 
    3.96 -   {
    3.97 -    fvar : string * typ,
    3.98 -    cargTs: typ list,
    3.99 -    pthA: SumTools.sum_path,
   3.100 -    pthR: SumTools.sum_path,
   3.101 -    f_def: term,
   3.102 -
   3.103 -    f: term option,
   3.104 -    f_defthm : thm option
   3.105 -   }
   3.106 -   
   3.107 -
   3.108 -datatype mutual_info =
   3.109 -  Mutual of 
   3.110 -   { 
   3.111 -    defname: string,
   3.112 -    fsum_var : string * typ,
   3.113 -
   3.114 -    ST: typ,
   3.115 -    RST: typ,
   3.116 -    streeA: SumTools.sum_tree,
   3.117 -    streeR: SumTools.sum_tree,
   3.118 -
   3.119 -    parts: mutual_part list,
   3.120 -    fqgars: qgar list,
   3.121 -    qglrs: ((string * typ) list * term list * term * term) list,
   3.122 -
   3.123 -    fsum : term option
   3.124 -   }
   3.125 -
   3.126 -
   3.127 -datatype prep_result =
   3.128 -  Prep of
   3.129 -     {
   3.130 -      globals: globals,
   3.131 -      f: term,
   3.132 -      G: term,
   3.133 -      R: term,
   3.134 - 
   3.135 -      goal: term,
   3.136 -      goalI: thm,
   3.137 -      values: thm list,
   3.138 -      clauses: clause_info list,
   3.139 -
   3.140 -      R_cases: thm,
   3.141 -      ex1_iff: thm
   3.142 -     }
   3.143 -
   3.144  datatype fundef_result =
   3.145    FundefResult of
   3.146       {
   3.147        f: term,
   3.148 -      G : term,
   3.149 -      R : term,
   3.150 -      completeness : thm,
   3.151 -
   3.152 -      psimps : thm list, 
   3.153 -      subset_pinduct : thm, 
   3.154 -      simple_pinduct : thm, 
   3.155 -      total_intro : thm,
   3.156 -      dom_intros : thm list
   3.157 -     }
   3.158 -
   3.159 -datatype fundef_mresult =
   3.160 -  FundefMResult of
   3.161 -     {
   3.162 -      f: term,
   3.163        G: term,
   3.164        R: term,
   3.165  
   3.166        psimps : thm list, 
   3.167 +      trsimps : thm list option, 
   3.168 +
   3.169        subset_pinducts : thm list, 
   3.170        simple_pinducts : thm list, 
   3.171        cases : thm,
   3.172        termination : thm,
   3.173 -      domintros : thm list
   3.174 +      domintros : thm list option
   3.175       }
   3.176  
   3.177  datatype fundef_context_data =
   3.178    FundefCtxData of
   3.179       {
   3.180 -      fixes : ((string * typ) * mixfix) list,
   3.181 -      spec : ((string * Attrib.src list) * term list) list list,
   3.182 -      mutual: mutual_info,
   3.183 +      add_simps : string -> Attrib.src list -> thm list -> local_theory -> thm list * local_theory,
   3.184  
   3.185        f : term,
   3.186        R : term,
   3.187 @@ -261,6 +127,7 @@
   3.188    | Preprocessor of string
   3.189    | Target of xstring
   3.190    | DomIntros
   3.191 +  | Tailrec
   3.192  
   3.193  datatype fundef_config
   3.194    = FundefConfig of
   3.195 @@ -269,23 +136,29 @@
   3.196      default: string,
   3.197      preprocessor: string option,
   3.198      target: xstring option,
   3.199 -    domintros: bool
   3.200 +    domintros: bool,
   3.201 +    tailrec: bool
   3.202     }
   3.203  
   3.204  
   3.205 -val default_config = FundefConfig { sequential=false, default="%x. arbitrary", preprocessor=NONE, target=NONE, domintros=false }
   3.206 -val fun_config = FundefConfig { sequential=true, default="%x. arbitrary", preprocessor=NONE, target=NONE, domintros=false }
   3.207 +val default_config = FundefConfig { sequential=false, default="%x. arbitrary", preprocessor=NONE,
   3.208 +                                    target=NONE, domintros=false, tailrec=false }
   3.209 +
   3.210 +val fun_config = FundefConfig { sequential=true, default="%x. arbitrary", preprocessor=NONE, 
   3.211 +                                target=NONE, domintros=false, tailrec=false }
   3.212  
   3.213 -fun apply_opt Sequential (FundefConfig {sequential, default, preprocessor, target, domintros}) = 
   3.214 -    FundefConfig {sequential=true, default=default, preprocessor=preprocessor, target=target, domintros=domintros }
   3.215 -  | apply_opt (Default d) (FundefConfig {sequential, default, preprocessor, target, domintros}) = 
   3.216 -    FundefConfig {sequential=sequential, default=d, preprocessor=preprocessor, target=target, domintros=domintros }
   3.217 -  | apply_opt (Preprocessor p) (FundefConfig {sequential, default, preprocessor, target, domintros}) = 
   3.218 -    FundefConfig {sequential=sequential, default=default, preprocessor=SOME p, target=target, domintros=domintros }
   3.219 -  | apply_opt (Target t) (FundefConfig {sequential, default, preprocessor, target, domintros }) =
   3.220 -    FundefConfig {sequential=sequential, default=default, preprocessor=preprocessor, target=SOME t, domintros=domintros }
   3.221 -  | apply_opt Domintros (FundefConfig {sequential, default, preprocessor, target, domintros }) =
   3.222 -    FundefConfig {sequential=sequential, default=default, preprocessor=preprocessor, target=target, domintros=true }
   3.223 +fun apply_opt Sequential (FundefConfig {sequential, default, preprocessor, target, domintros,tailrec}) = 
   3.224 +    FundefConfig {sequential=true, default=default, preprocessor=preprocessor, target=target, domintros=domintros, tailrec=tailrec }
   3.225 +  | apply_opt (Default d) (FundefConfig {sequential, default, preprocessor, target, domintros,tailrec}) = 
   3.226 +    FundefConfig {sequential=sequential, default=d, preprocessor=preprocessor, target=target, domintros=domintros, tailrec=tailrec }
   3.227 +  | apply_opt (Preprocessor p) (FundefConfig {sequential, default, preprocessor, target, domintros,tailrec}) = 
   3.228 +    FundefConfig {sequential=sequential, default=default, preprocessor=SOME p, target=target, domintros=domintros, tailrec=tailrec }
   3.229 +  | apply_opt (Target t) (FundefConfig {sequential, default, preprocessor, target, domintros,tailrec }) =
   3.230 +    FundefConfig {sequential=sequential, default=default, preprocessor=preprocessor, target=SOME t, domintros=domintros, tailrec=tailrec }
   3.231 +  | apply_opt DomIntros (FundefConfig {sequential, default, preprocessor, target, domintros,tailrec }) =
   3.232 +    FundefConfig {sequential=sequential, default=default, preprocessor=preprocessor, target=target, domintros=true,tailrec=tailrec }
   3.233 +  | apply_opt Tailrec (FundefConfig {sequential, default, preprocessor, target, domintros,tailrec }) =
   3.234 +    FundefConfig {sequential=sequential, default=default, preprocessor=preprocessor, target=target, domintros=domintros,tailrec=true } 
   3.235  
   3.236  
   3.237  local structure P = OuterParse and K = OuterKeyword in
   3.238 @@ -295,29 +168,18 @@
   3.239  val option_parser = (P.$$$ "sequential" >> K Sequential)
   3.240                 || ((P.reserved "default" |-- P.term) >> Default)
   3.241                 || (P.reserved "domintros" >> K DomIntros)
   3.242 +               || (P.reserved "tailrec" >> K Tailrec)
   3.243                 || ((P.$$$ "in" |-- P.xname) >> Target)
   3.244  
   3.245  fun config_parser def = (Scan.optional (P.$$$ "(" |-- P.list1 option_parser --| P.$$$ ")") [])
   3.246                            >> (fn opts => fold apply_opt opts def)
   3.247 +
   3.248  end
   3.249  
   3.250  
   3.251  
   3.252  
   3.253  
   3.254 -
   3.255 -
   3.256 -
   3.257 -
   3.258 -
   3.259 -
   3.260 -
   3.261 -
   3.262 -
   3.263 -
   3.264 -
   3.265 -
   3.266 -
   3.267  end
   3.268  
   3.269  
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Tools/function_package/fundef_core.ML	Mon Jan 22 17:29:43 2007 +0100
     4.3 @@ -0,0 +1,952 @@
     4.4 +(*  Title:      HOL/Tools/function_package/fundef_core.ML
     4.5 +    ID:         $Id$
     4.6 +    Author:     Alexander Krauss, TU Muenchen
     4.7 +
     4.8 +A package for general recursive function definitions.
     4.9 +Main functionality
    4.10 +*)
    4.11 +
    4.12 +signature FUNDEF_CORE =
    4.13 +sig
    4.14 +    val prepare_fundef : FundefCommon.fundef_config
    4.15 +                         -> string (* defname *)
    4.16 +                         -> (string * typ * mixfix) (* defined symbol *)
    4.17 +                         -> ((string * typ) list * term list * term * term) list (* specification *)
    4.18 +                         -> string (* default_value, not parsed yet *)
    4.19 +                         -> local_theory
    4.20 +
    4.21 +                         -> (term   (* f *)
    4.22 +                             * thm  (* goalstate *)
    4.23 +                             * (thm -> FundefCommon.fundef_result) (* continuation *)
    4.24 +                            ) * local_theory
    4.25 +
    4.26 +end
    4.27 +
    4.28 +structure FundefCore : FUNDEF_CORE =
    4.29 +struct
    4.30 +
    4.31 +
    4.32 +open FundefLib
    4.33 +open FundefCommon
    4.34 +open FundefAbbrev
    4.35 +
    4.36 +datatype globals =
    4.37 +   Globals of { 
    4.38 +         fvar: term, 
    4.39 +         domT: typ, 
    4.40 +         ranT: typ,
    4.41 +         h: term, 
    4.42 +         y: term, 
    4.43 +         x: term, 
    4.44 +         z: term, 
    4.45 +         a: term, 
    4.46 +         P: term, 
    4.47 +         D: term, 
    4.48 +         Pbool:term
    4.49 +}
    4.50 +
    4.51 +
    4.52 +datatype rec_call_info = 
    4.53 +  RCInfo of
    4.54 +  {
    4.55 +   RIvs: (string * typ) list,  (* Call context: fixes and assumes *)
    4.56 +   CCas: thm list,
    4.57 +   rcarg: term,                 (* The recursive argument *)
    4.58 +
    4.59 +   llRI: thm,
    4.60 +   h_assum: term
    4.61 +  } 
    4.62 +
    4.63 +
    4.64 +datatype clause_context =
    4.65 +  ClauseContext of
    4.66 +  {
    4.67 +    ctxt : Proof.context,
    4.68 +
    4.69 +    qs : term list,
    4.70 +    gs : term list,
    4.71 +    lhs: term,
    4.72 +    rhs: term,
    4.73 +
    4.74 +    cqs: cterm list,
    4.75 +    ags: thm list,     
    4.76 +    case_hyp : thm
    4.77 +  }
    4.78 +
    4.79 +
    4.80 +fun transfer_clause_ctx thy (ClauseContext { ctxt, qs, gs, lhs, rhs, cqs, ags, case_hyp }) =
    4.81 +    ClauseContext { ctxt = ProofContext.transfer thy ctxt,
    4.82 +                    qs = qs, gs = gs, lhs = lhs, rhs = rhs, cqs = cqs, ags = ags, case_hyp = case_hyp }
    4.83 +
    4.84 +
    4.85 +datatype clause_info =
    4.86 +  ClauseInfo of 
    4.87 +     {
    4.88 +      no: int,
    4.89 +      qglr : ((string * typ) list * term list * term * term),
    4.90 +      cdata : clause_context,
    4.91 +
    4.92 +      tree: ctx_tree,
    4.93 +      lGI: thm,
    4.94 +      RCs: rec_call_info list
    4.95 +     }
    4.96 +
    4.97 +
    4.98 +(* Theory dependencies. *)
    4.99 +val Pair_inject = thm "Product_Type.Pair_inject";
   4.100 +
   4.101 +val acc_induct_rule = thm "FunDef.accP_induct_rule"
   4.102 +
   4.103 +val ex1_implies_ex = thm "FunDef.fundef_ex1_existence"
   4.104 +val ex1_implies_un = thm "FunDef.fundef_ex1_uniqueness"
   4.105 +val ex1_implies_iff = thm "FunDef.fundef_ex1_iff"
   4.106 +
   4.107 +val acc_downward = thm "FunDef.accP_downward"
   4.108 +val accI = thm "FunDef.accPI"
   4.109 +val case_split = thm "HOL.case_split_thm"
   4.110 +val fundef_default_value = thm "FunDef.fundef_default_value"
   4.111 +val not_accP_down = thm "FunDef.not_accP_down"
   4.112 +
   4.113 +
   4.114 +
   4.115 +fun find_calls tree =
   4.116 +    let
   4.117 +      fun add_Ri (fixes,assumes) (_ $ arg) _ (_, xs) = ([], (fixes, assumes, arg) :: xs)
   4.118 +        | add_Ri _ _ _ _ = raise Match
   4.119 +    in
   4.120 +      rev (FundefCtxTree.traverse_tree add_Ri tree [])
   4.121 +    end
   4.122 +
   4.123 +
   4.124 +(** building proof obligations *)
   4.125 +
   4.126 +fun mk_compat_proof_obligations domT ranT fvar f glrs =
   4.127 +    let
   4.128 +      fun mk_impl ((qs, gs, lhs, rhs),(qs', gs', lhs', rhs')) =
   4.129 +          let
   4.130 +            val shift = incr_boundvars (length qs')
   4.131 +          in
   4.132 +            (implies $ Trueprop (eq_const domT $ shift lhs $ lhs')
   4.133 +                     $ Trueprop (eq_const ranT $ shift rhs $ rhs'))
   4.134 +              |> fold_rev (curry Logic.mk_implies) (map shift gs @ gs')
   4.135 +              |> fold_rev (fn (n,T) => fn b => all T $ Abs(n,T,b)) (qs @ qs')
   4.136 +              |> curry abstract_over fvar
   4.137 +              |> curry subst_bound f
   4.138 +          end
   4.139 +    in
   4.140 +      map mk_impl (unordered_pairs glrs)
   4.141 +    end
   4.142 +
   4.143 +
   4.144 +fun mk_completeness (Globals {x, Pbool, ...}) clauses qglrs =
   4.145 +    let
   4.146 +        fun mk_case (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) =
   4.147 +            Trueprop Pbool
   4.148 +                     |> curry Logic.mk_implies (Trueprop (mk_eq (x, lhs)))
   4.149 +                     |> fold_rev (curry Logic.mk_implies) gs
   4.150 +                     |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
   4.151 +    in
   4.152 +        Trueprop Pbool
   4.153 +                 |> fold_rev (curry Logic.mk_implies o mk_case) (clauses ~~ qglrs)
   4.154 +                 |> mk_forall_rename ("x", x)
   4.155 +                 |> mk_forall_rename ("P", Pbool)
   4.156 +    end
   4.157 +
   4.158 +(** making a context with it's own local bindings **)
   4.159 +
   4.160 +fun mk_clause_context x ctxt (pre_qs,pre_gs,pre_lhs,pre_rhs) =
   4.161 +    let
   4.162 +      val (qs, ctxt') = Variable.variant_fixes (map fst pre_qs) ctxt
   4.163 +                                           |>> map2 (fn (_, T) => fn n => Free (n, T)) pre_qs
   4.164 +
   4.165 +      val thy = ProofContext.theory_of ctxt'
   4.166 +
   4.167 +      fun inst t = subst_bounds (rev qs, t)
   4.168 +      val gs = map inst pre_gs
   4.169 +      val lhs = inst pre_lhs
   4.170 +      val rhs = inst pre_rhs
   4.171 +                
   4.172 +      val cqs = map (cterm_of thy) qs
   4.173 +      val ags = map (assume o cterm_of thy) gs
   4.174 +                  
   4.175 +      val case_hyp = assume (cterm_of thy (Trueprop (mk_eq (x, lhs))))
   4.176 +    in
   4.177 +      ClauseContext { ctxt = ctxt', qs = qs, gs = gs, lhs = lhs, rhs = rhs, 
   4.178 +                      cqs = cqs, ags = ags, case_hyp = case_hyp }
   4.179 +    end
   4.180 +      
   4.181 +
   4.182 +(* lowlevel term function *)
   4.183 +fun abstract_over_list vs body =
   4.184 +  let
   4.185 +    exception SAME;
   4.186 +    fun abs lev v tm =
   4.187 +      if v aconv tm then Bound lev
   4.188 +      else
   4.189 +        (case tm of
   4.190 +          Abs (a, T, t) => Abs (a, T, abs (lev + 1) v t)
   4.191 +        | t $ u => (abs lev v t $ (abs lev v u handle SAME => u) handle SAME => t $ abs lev v u)
   4.192 +        | _ => raise SAME);
   4.193 +  in 
   4.194 +    fold_index (fn (i,v) => fn t => abs i v t handle SAME => t) vs body
   4.195 +  end
   4.196 +
   4.197 +
   4.198 +
   4.199 +fun mk_clause_info globals G f no cdata qglr tree RCs GIntro_thm RIntro_thms =
   4.200 +    let
   4.201 +        val Globals {h, fvar, x, ...} = globals
   4.202 +
   4.203 +        val ClauseContext { ctxt, qs, cqs, ags, ... } = cdata
   4.204 +        val cert = Thm.cterm_of (ProofContext.theory_of ctxt)
   4.205 +
   4.206 +        (* Instantiate the GIntro thm with "f" and import into the clause context. *)
   4.207 +        val lGI = GIntro_thm
   4.208 +                    |> forall_elim (cert f)
   4.209 +                    |> fold forall_elim cqs
   4.210 +                    |> fold implies_elim_swp ags
   4.211 +
   4.212 +        fun mk_call_info (rcfix, rcassm, rcarg) RI =
   4.213 +            let
   4.214 +                val llRI = RI
   4.215 +                             |> fold forall_elim cqs
   4.216 +                             |> fold (forall_elim o cert o Free) rcfix
   4.217 +                             |> fold implies_elim_swp ags
   4.218 +                             |> fold implies_elim_swp rcassm
   4.219 +
   4.220 +                val h_assum =
   4.221 +                    Trueprop (G $ rcarg $ (h $ rcarg))
   4.222 +                              |> fold_rev (curry Logic.mk_implies o prop_of) rcassm
   4.223 +                              |> fold_rev (mk_forall o Free) rcfix
   4.224 +                              |> Pattern.rewrite_term (ProofContext.theory_of ctxt) [(f, h)] []
   4.225 +                              |> abstract_over_list (rev qs)
   4.226 +            in
   4.227 +                RCInfo {RIvs=rcfix, rcarg=rcarg, CCas=rcassm, llRI=llRI, h_assum=h_assum}
   4.228 +            end
   4.229 +
   4.230 +        val RC_infos = map2 mk_call_info RCs RIntro_thms
   4.231 +    in
   4.232 +        ClauseInfo
   4.233 +            {
   4.234 +             no=no,
   4.235 +             cdata=cdata,
   4.236 +             qglr=qglr,
   4.237 +
   4.238 +             lGI=lGI, 
   4.239 +             RCs=RC_infos,
   4.240 +             tree=tree
   4.241 +            }
   4.242 +    end
   4.243 +
   4.244 +
   4.245 +
   4.246 +
   4.247 +
   4.248 +
   4.249 +
   4.250 +(* replace this by a table later*)
   4.251 +fun store_compat_thms 0 thms = []
   4.252 +  | store_compat_thms n thms =
   4.253 +    let
   4.254 +        val (thms1, thms2) = chop n thms
   4.255 +    in
   4.256 +        (thms1 :: store_compat_thms (n - 1) thms2)
   4.257 +    end
   4.258 +
   4.259 +(* expects i <= j *)
   4.260 +fun lookup_compat_thm i j cts =
   4.261 +    nth (nth cts (i - 1)) (j - i)
   4.262 +
   4.263 +(* Returns "Gsi, Gsj, lhs_i = lhs_j |-- rhs_j_f = rhs_i_f" *)
   4.264 +(* if j < i, then turn around *)
   4.265 +fun get_compat_thm thy cts i j ctxi ctxj = 
   4.266 +    let
   4.267 +      val ClauseContext {cqs=cqsi,ags=agsi,lhs=lhsi,...} = ctxi
   4.268 +      val ClauseContext {cqs=cqsj,ags=agsj,lhs=lhsj,...} = ctxj
   4.269 +          
   4.270 +      val lhsi_eq_lhsj = cterm_of thy (Trueprop (mk_eq (lhsi, lhsj)))
   4.271 +    in if j < i then
   4.272 +         let
   4.273 +           val compat = lookup_compat_thm j i cts
   4.274 +         in
   4.275 +           compat         (* "!!qj qi. Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *)
   4.276 +                |> fold forall_elim (cqsj @ cqsi) (* "Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *)
   4.277 +                |> fold implies_elim_swp agsj
   4.278 +                |> fold implies_elim_swp agsi
   4.279 +                |> implies_elim_swp ((assume lhsi_eq_lhsj) RS sym) (* "Gsj, Gsi, lhsi = lhsj |-- rhsj = rhsi" *)
   4.280 +         end
   4.281 +       else
   4.282 +         let
   4.283 +           val compat = lookup_compat_thm i j cts
   4.284 +         in
   4.285 +               compat        (* "!!qi qj. Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *)
   4.286 +                 |> fold forall_elim (cqsi @ cqsj) (* "Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *)
   4.287 +                 |> fold implies_elim_swp agsi
   4.288 +                 |> fold implies_elim_swp agsj
   4.289 +                 |> implies_elim_swp (assume lhsi_eq_lhsj)
   4.290 +                 |> (fn thm => thm RS sym) (* "Gsi, Gsj, lhsi = lhsj |-- rhsj = rhsi" *)
   4.291 +         end
   4.292 +    end
   4.293 +
   4.294 +
   4.295 +
   4.296 +
   4.297 +(* Generates the replacement lemma in fully quantified form. *)
   4.298 +fun mk_replacement_lemma thy h ih_elim clause =
   4.299 +    let
   4.300 +        val ClauseInfo {cdata=ClauseContext {qs, lhs, rhs, cqs, ags, case_hyp, ...}, RCs, tree, ...} = clause
   4.301 +
   4.302 +        val ih_elim_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_elim
   4.303 +
   4.304 +        val Ris = map (fn RCInfo {llRI, ...} => llRI) RCs
   4.305 +        val h_assums = map (fn RCInfo {h_assum, ...} => assume (cterm_of thy (subst_bounds (rev qs, h_assum)))) RCs
   4.306 +
   4.307 +        val ih_elim_case_inst = instantiate' [] [NONE, SOME (cterm_of thy h)] ih_elim_case (* Should be done globally *)
   4.308 +
   4.309 +        val (eql, _) = FundefCtxTree.rewrite_by_tree thy h ih_elim_case_inst (Ris ~~ h_assums) tree
   4.310 +
   4.311 +        val replace_lemma = (eql RS meta_eq_to_obj_eq)
   4.312 +                                |> implies_intr (cprop_of case_hyp)
   4.313 +                                |> fold_rev (implies_intr o cprop_of) h_assums
   4.314 +                                |> fold_rev (implies_intr o cprop_of) ags
   4.315 +                                |> fold_rev forall_intr cqs
   4.316 +                                |> Goal.close_result
   4.317 +    in
   4.318 +      replace_lemma
   4.319 +    end
   4.320 +
   4.321 +
   4.322 +fun mk_uniqueness_clause thy globals f compat_store clausei clausej RLj =
   4.323 +    let
   4.324 +        val Globals {h, y, x, fvar, ...} = globals
   4.325 +        val ClauseInfo {no=i, cdata=cctxi as ClauseContext {ctxt=ctxti, lhs=lhsi, case_hyp, ...}, ...} = clausei
   4.326 +        val ClauseInfo {no=j, qglr=cdescj, RCs=RCsj, ...} = clausej
   4.327 +
   4.328 +        val cctxj as ClauseContext {ags = agsj', lhs = lhsj', rhs = rhsj', qs = qsj', cqs = cqsj', ...} 
   4.329 +            = mk_clause_context x ctxti cdescj
   4.330 +
   4.331 +        val rhsj'h = Pattern.rewrite_term thy [(fvar,h)] [] rhsj'
   4.332 +        val compat = get_compat_thm thy compat_store i j cctxi cctxj
   4.333 +        val Ghsj' = map (fn RCInfo {h_assum, ...} => assume (cterm_of thy (subst_bounds (rev qsj', h_assum)))) RCsj
   4.334 +
   4.335 +        val RLj_import = 
   4.336 +            RLj |> fold forall_elim cqsj'
   4.337 +                |> fold implies_elim_swp agsj'
   4.338 +                |> fold implies_elim_swp Ghsj'
   4.339 +
   4.340 +        val y_eq_rhsj'h = assume (cterm_of thy (Trueprop (mk_eq (y, rhsj'h))))
   4.341 +        val lhsi_eq_lhsj' = assume (cterm_of thy (Trueprop (mk_eq (lhsi, lhsj')))) (* lhs_i = lhs_j' |-- lhs_i = lhs_j' *)
   4.342 +    in
   4.343 +        (trans OF [case_hyp, lhsi_eq_lhsj']) (* lhs_i = lhs_j' |-- x = lhs_j' *)
   4.344 +        |> implies_elim RLj_import (* Rj1' ... Rjk', lhs_i = lhs_j' |-- rhs_j'_h = rhs_j'_f *)
   4.345 +        |> (fn it => trans OF [it, compat]) (* lhs_i = lhs_j', Gj', Rj1' ... Rjk' |-- rhs_j'_h = rhs_i_f *)
   4.346 +        |> (fn it => trans OF [y_eq_rhsj'h, it]) (* lhs_i = lhs_j', Gj', Rj1' ... Rjk', y = rhs_j_h' |-- y = rhs_i_f *)
   4.347 +        |> fold_rev (implies_intr o cprop_of) Ghsj'
   4.348 +        |> fold_rev (implies_intr o cprop_of) agsj' (* lhs_i = lhs_j' , y = rhs_j_h' |-- Gj', Rj1'...Rjk' ==> y = rhs_i_f *)
   4.349 +        |> implies_intr (cprop_of y_eq_rhsj'h)
   4.350 +        |> implies_intr (cprop_of lhsi_eq_lhsj')
   4.351 +        |> fold_rev forall_intr (cterm_of thy h :: cqsj')
   4.352 +    end
   4.353 +
   4.354 +
   4.355 +
   4.356 +fun mk_uniqueness_case thy globals G f ihyp ih_intro G_cases compat_store clauses rep_lemmas clausei =
   4.357 +    let
   4.358 +        val Globals {x, y, ranT, fvar, ...} = globals
   4.359 +        val ClauseInfo {cdata = ClauseContext {lhs, rhs, qs, cqs, ags, case_hyp, ...}, lGI, RCs, ...} = clausei
   4.360 +        val rhsC = Pattern.rewrite_term thy [(fvar, f)] [] rhs
   4.361 +
   4.362 +        val ih_intro_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_intro
   4.363 +
   4.364 +        fun prep_RC (RCInfo {llRI, RIvs, CCas, ...}) = (llRI RS ih_intro_case)
   4.365 +                                                            |> fold_rev (implies_intr o cprop_of) CCas
   4.366 +                                                            |> fold_rev (forall_intr o cterm_of thy o Free) RIvs
   4.367 +
   4.368 +        val existence = fold (curry op COMP o prep_RC) RCs lGI
   4.369 +
   4.370 +        val P = cterm_of thy (mk_eq (y, rhsC))
   4.371 +        val G_lhs_y = assume (cterm_of thy (Trueprop (G $ lhs $ y)))
   4.372 +
   4.373 +        val unique_clauses = map2 (mk_uniqueness_clause thy globals f compat_store clausei) clauses rep_lemmas
   4.374 +
   4.375 +        val uniqueness = G_cases
   4.376 +                           |> forall_elim (cterm_of thy lhs)
   4.377 +                           |> forall_elim (cterm_of thy y)
   4.378 +                           |> forall_elim P
   4.379 +                           |> implies_elim_swp G_lhs_y
   4.380 +                           |> fold implies_elim_swp unique_clauses
   4.381 +                           |> implies_intr (cprop_of G_lhs_y)
   4.382 +                           |> forall_intr (cterm_of thy y)
   4.383 +
   4.384 +        val P2 = cterm_of thy (lambda y (G $ lhs $ y)) (* P2 y := (lhs, y): G *)
   4.385 +
   4.386 +        val exactly_one =
   4.387 +            ex1I |> instantiate' [SOME (ctyp_of thy ranT)] [SOME P2, SOME (cterm_of thy rhsC)]
   4.388 +                 |> curry (op COMP) existence
   4.389 +                 |> curry (op COMP) uniqueness
   4.390 +                 |> simplify (HOL_basic_ss addsimps [case_hyp RS sym])
   4.391 +                 |> implies_intr (cprop_of case_hyp)
   4.392 +                 |> fold_rev (implies_intr o cprop_of) ags
   4.393 +                 |> fold_rev forall_intr cqs
   4.394 +
   4.395 +        val function_value =
   4.396 +            existence
   4.397 +              |> implies_intr ihyp
   4.398 +              |> implies_intr (cprop_of case_hyp)
   4.399 +              |> forall_intr (cterm_of thy x)
   4.400 +              |> forall_elim (cterm_of thy lhs)
   4.401 +              |> curry (op RS) refl
   4.402 +    in
   4.403 +        (exactly_one, function_value)
   4.404 +    end
   4.405 +
   4.406 +
   4.407 +
   4.408 +
   4.409 +fun prove_stuff thy congs globals G f R clauses complete compat compat_store G_elim f_def =
   4.410 +    let
   4.411 +        val Globals {h, domT, ranT, x, ...} = globals
   4.412 +
   4.413 +        (* Inductive Hypothesis: !!z. (z,x):R ==> EX!y. (z,y):G *)
   4.414 +        val ihyp = all domT $ Abs ("z", domT,
   4.415 +                                   implies $ Trueprop (R $ Bound 0 $ x)
   4.416 +                                           $ Trueprop (Const ("Ex1", (ranT --> boolT) --> boolT) $
   4.417 +                                                             Abs ("y", ranT, G $ Bound 1 $ Bound 0)))
   4.418 +                       |> cterm_of thy
   4.419 +
   4.420 +        val ihyp_thm = assume ihyp |> forall_elim_vars 0
   4.421 +        val ih_intro = ihyp_thm RS (f_def RS ex1_implies_ex)
   4.422 +        val ih_elim = ihyp_thm RS (f_def RS ex1_implies_un)
   4.423 +
   4.424 +        val _ = Output.debug (K "Proving Replacement lemmas...")
   4.425 +        val repLemmas = map (mk_replacement_lemma thy h ih_elim) clauses
   4.426 +
   4.427 +        val _ = Output.debug (K "Proving cases for unique existence...")
   4.428 +        val (ex1s, values) = 
   4.429 +            split_list (map (mk_uniqueness_case thy globals G f ihyp ih_intro G_elim compat_store clauses repLemmas) clauses)
   4.430 +
   4.431 +        val _ = Output.debug (K "Proving: Graph is a function") (* FIXME: Rewrite this proof. *)
   4.432 +        val graph_is_function = complete
   4.433 +                                  |> forall_elim_vars 0
   4.434 +                                  |> fold (curry op COMP) ex1s
   4.435 +                                  |> implies_intr (ihyp)
   4.436 +                                  |> implies_intr (cterm_of thy (Trueprop (mk_acc domT R $ x)))
   4.437 +                                  |> forall_intr (cterm_of thy x)
   4.438 +                                  |> (fn it => Drule.compose_single (it, 2, acc_induct_rule)) (* "EX! y. (?x,y):G" *)
   4.439 +                                  |> (fn it => fold (forall_intr o cterm_of thy) (term_vars (prop_of it)) it)
   4.440 +
   4.441 +        val goalstate =  Conjunction.intr graph_is_function complete
   4.442 +                          |> Goal.close_result
   4.443 +                          |> Goal.protect
   4.444 +                          |> fold_rev (implies_intr o cprop_of) compat
   4.445 +                          |> implies_intr (cprop_of complete)
   4.446 +    in
   4.447 +      (goalstate, values)
   4.448 +    end
   4.449 +
   4.450 +
   4.451 +fun define_graph Gname fvar domT ranT clauses RCss lthy =
   4.452 +    let
   4.453 +      val GT = domT --> ranT --> boolT
   4.454 +      val Gvar = Free (the_single (Variable.variant_frees lthy [] [(Gname, GT)]))
   4.455 +
   4.456 +      fun mk_GIntro (ClauseContext {qs, gs, lhs, rhs, ...}) RCs =
   4.457 +          let
   4.458 +            fun mk_h_assm (rcfix, rcassm, rcarg) =
   4.459 +                Trueprop (Gvar $ rcarg $ (fvar $ rcarg))
   4.460 +                          |> fold_rev (curry Logic.mk_implies o prop_of) rcassm
   4.461 +                          |> fold_rev (mk_forall o Free) rcfix
   4.462 +          in
   4.463 +            Trueprop (Gvar $ lhs $ rhs)
   4.464 +                      |> fold_rev (curry Logic.mk_implies o mk_h_assm) RCs
   4.465 +                      |> fold_rev (curry Logic.mk_implies) gs
   4.466 +                      |> fold_rev mk_forall (fvar :: qs)
   4.467 +          end
   4.468 +          
   4.469 +      val G_intros = map2 mk_GIntro clauses RCss
   4.470 +                     
   4.471 +      val (GIntro_thms, (G, G_elim, G_induct, lthy)) = 
   4.472 +          FundefInductiveWrap.inductive_def G_intros ((dest_Free Gvar, NoSyn), lthy)
   4.473 +    in
   4.474 +      ((G, GIntro_thms, G_elim, G_induct), lthy)
   4.475 +    end
   4.476 +
   4.477 +
   4.478 +
   4.479 +fun define_function fdefname (fname, mixfix) domT ranT G default lthy =
   4.480 +    let
   4.481 +      val f_def = 
   4.482 +          Abs ("x", domT, Const ("FunDef.THE_default", ranT --> (ranT --> boolT) --> ranT) $ (default $ Bound 0) $
   4.483 +                                Abs ("y", ranT, G $ Bound 1 $ Bound 0))
   4.484 +              |> Envir.beta_norm (* FIXME: LocalTheory.def does not work if not beta-normal *)
   4.485 +          
   4.486 +      val ((f, (_, f_defthm)), lthy) =
   4.487 +        LocalTheory.def Thm.internalK ((fname ^ "C", mixfix), ((fdefname, []), f_def)) lthy
   4.488 +    in
   4.489 +      ((f, f_defthm), lthy)
   4.490 +    end
   4.491 +
   4.492 +
   4.493 +fun define_recursion_relation Rname domT ranT fvar f qglrs clauses RCss lthy =
   4.494 +    let
   4.495 +
   4.496 +      val RT = domT --> domT --> boolT
   4.497 +      val Rvar = Free (the_single (Variable.variant_frees lthy [] [(Rname, RT)]))
   4.498 +
   4.499 +      fun mk_RIntro (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) (rcfix, rcassm, rcarg) =
   4.500 +          Trueprop (Rvar $ rcarg $ lhs)
   4.501 +                    |> fold_rev (curry Logic.mk_implies o prop_of) rcassm
   4.502 +                    |> fold_rev (curry Logic.mk_implies) gs
   4.503 +                    |> fold_rev (mk_forall o Free) rcfix
   4.504 +                    |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
   4.505 +                    (* "!!qs xs. CS ==> G => (r, lhs) : R" *)
   4.506 +
   4.507 +      val R_intross = map2 (map o mk_RIntro) (clauses ~~ qglrs) RCss
   4.508 +
   4.509 +      val (RIntro_thmss, (R, R_elim, _, lthy)) = 
   4.510 +          fold_burrow FundefInductiveWrap.inductive_def R_intross ((dest_Free Rvar, NoSyn), lthy)
   4.511 +    in
   4.512 +      ((R, RIntro_thmss, R_elim), lthy)
   4.513 +    end
   4.514 +
   4.515 +
   4.516 +fun fix_globals domT ranT fvar ctxt =
   4.517 +    let
   4.518 +      val ([h, y, x, z, a, D, P, Pbool],ctxt') = 
   4.519 +          Variable.variant_fixes ["h_fd", "y_fd", "x_fd", "z_fd", "a_fd", "D_fd", "P_fd", "Pb_fd"] ctxt
   4.520 +    in
   4.521 +      (Globals {h = Free (h, domT --> ranT),
   4.522 +                y = Free (y, ranT),
   4.523 +                x = Free (x, domT),
   4.524 +                z = Free (z, domT),
   4.525 +                a = Free (a, domT),
   4.526 +                D = Free (D, domT --> boolT),
   4.527 +                P = Free (P, domT --> boolT),
   4.528 +                Pbool = Free (Pbool, boolT),
   4.529 +                fvar = fvar,
   4.530 +                domT = domT,
   4.531 +                ranT = ranT
   4.532 +               },
   4.533 +       ctxt')
   4.534 +    end
   4.535 +
   4.536 +
   4.537 +
   4.538 +fun inst_RC thy fvar f (rcfix, rcassm, rcarg) =
   4.539 +    let
   4.540 +      fun inst_term t = subst_bound(f, abstract_over (fvar, t))
   4.541 +    in
   4.542 +      (rcfix, map (assume o cterm_of thy o inst_term o prop_of) rcassm, inst_term rcarg)
   4.543 +    end
   4.544 +
   4.545 +
   4.546 +
   4.547 +(**********************************************************
   4.548 + *                   PROVING THE RULES 
   4.549 + **********************************************************)
   4.550 +
   4.551 +fun mk_psimps thy globals R clauses valthms f_iff graph_is_function =
   4.552 +    let
   4.553 +      val Globals {domT, z, ...} = globals
   4.554 +  
   4.555 +      fun mk_psimp (ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {cqs, lhs, ags, ...}, ...}) valthm =
   4.556 +          let
   4.557 +            val lhs_acc = cterm_of thy (Trueprop (mk_acc domT R $ lhs)) (* "acc R lhs" *)
   4.558 +            val z_smaller = cterm_of thy (Trueprop (R $ z $ lhs)) (* "R z lhs" *)
   4.559 +          in
   4.560 +            ((assume z_smaller) RS ((assume lhs_acc) RS acc_downward))
   4.561 +              |> (fn it => it COMP graph_is_function)
   4.562 +              |> implies_intr z_smaller
   4.563 +              |> forall_intr (cterm_of thy z)
   4.564 +              |> (fn it => it COMP valthm)
   4.565 +              |> implies_intr lhs_acc 
   4.566 +              |> asm_simplify (HOL_basic_ss addsimps [f_iff])
   4.567 +              |> fold_rev (implies_intr o cprop_of) ags
   4.568 +              |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
   4.569 +          end
   4.570 +    in
   4.571 +      map2 mk_psimp clauses valthms
   4.572 +    end
   4.573 +
   4.574 +
   4.575 +(** Induction rule **)
   4.576 +
   4.577 +
   4.578 +val acc_subset_induct = thm "FunDef.accP_subset_induct"
   4.579 +
   4.580 +fun mk_partial_induct_rule thy globals R complete_thm clauses =
   4.581 +    let
   4.582 +      val Globals {domT, x, z, a, P, D, ...} = globals
   4.583 +      val acc_R = mk_acc domT R
   4.584 +                  
   4.585 +      val x_D = assume (cterm_of thy (Trueprop (D $ x)))
   4.586 +      val a_D = cterm_of thy (Trueprop (D $ a))
   4.587 +                
   4.588 +      val D_subset = cterm_of thy (mk_forall x (implies $ Trueprop (D $ x) $ Trueprop (acc_R $ x)))
   4.589 +                     
   4.590 +      val D_dcl = (* "!!x z. [| x: D; (z,x):R |] ==> z:D" *)
   4.591 +                    mk_forall x
   4.592 +                    (mk_forall z (Logic.mk_implies (Trueprop (D $ x),
   4.593 +                                                    Logic.mk_implies (Trueprop (R $ z $ x),
   4.594 +                                                                      Trueprop (D $ z)))))
   4.595 +                    |> cterm_of thy
   4.596 +                    
   4.597 +                    
   4.598 +  (* Inductive Hypothesis: !!z. (z,x):R ==> P z *)
   4.599 +      val ihyp = all domT $ Abs ("z", domT, 
   4.600 +               implies $ Trueprop (R $ Bound 0 $ x)
   4.601 +             $ Trueprop (P $ Bound 0))
   4.602 +           |> cterm_of thy
   4.603 +
   4.604 +      val aihyp = assume ihyp
   4.605 +
   4.606 +  fun prove_case clause =
   4.607 +      let
   4.608 +    val ClauseInfo {cdata = ClauseContext {qs, cqs, ags, gs, lhs, case_hyp, ...}, RCs, 
   4.609 +                    qglr = (oqs, _, _, _), ...} = clause
   4.610 +                       
   4.611 +    val replace_x_ss = HOL_basic_ss addsimps [case_hyp]
   4.612 +    val lhs_D = simplify replace_x_ss x_D (* lhs : D *)
   4.613 +    val sih = full_simplify replace_x_ss aihyp
   4.614 +          
   4.615 +    fun mk_Prec (RCInfo {llRI, RIvs, CCas, rcarg, ...}) =
   4.616 +        sih |> forall_elim (cterm_of thy rcarg)
   4.617 +            |> implies_elim_swp llRI
   4.618 +            |> fold_rev (implies_intr o cprop_of) CCas
   4.619 +            |> fold_rev (forall_intr o cterm_of thy o Free) RIvs
   4.620 +        
   4.621 +    val P_recs = map mk_Prec RCs   (*  [P rec1, P rec2, ... ]  *)
   4.622 +                 
   4.623 +    val step = Trueprop (P $ lhs)
   4.624 +            |> fold_rev (curry Logic.mk_implies o prop_of) P_recs
   4.625 +            |> fold_rev (curry Logic.mk_implies) gs
   4.626 +            |> curry Logic.mk_implies (Trueprop (D $ lhs))
   4.627 +            |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
   4.628 +            |> cterm_of thy
   4.629 +         
   4.630 +    val P_lhs = assume step
   4.631 +           |> fold forall_elim cqs
   4.632 +           |> implies_elim_swp lhs_D 
   4.633 +           |> fold_rev implies_elim_swp ags
   4.634 +           |> fold implies_elim_swp P_recs
   4.635 +          
   4.636 +    val res = cterm_of thy (Trueprop (P $ x))
   4.637 +           |> Simplifier.rewrite replace_x_ss
   4.638 +           |> symmetric (* P lhs == P x *)
   4.639 +           |> (fn eql => equal_elim eql P_lhs) (* "P x" *)
   4.640 +           |> implies_intr (cprop_of case_hyp)
   4.641 +           |> fold_rev (implies_intr o cprop_of) ags
   4.642 +           |> fold_rev forall_intr cqs
   4.643 +      in
   4.644 +        (res, step)
   4.645 +      end
   4.646 +      
   4.647 +  val (cases, steps) = split_list (map prove_case clauses)
   4.648 +                       
   4.649 +  val istep = complete_thm
   4.650 +                |> forall_elim_vars 0
   4.651 +                |> fold (curry op COMP) cases (*  P x  *)
   4.652 +                |> implies_intr ihyp
   4.653 +                |> implies_intr (cprop_of x_D)
   4.654 +                |> forall_intr (cterm_of thy x)
   4.655 +         
   4.656 +  val subset_induct_rule = 
   4.657 +      acc_subset_induct
   4.658 +        |> (curry op COMP) (assume D_subset)
   4.659 +        |> (curry op COMP) (assume D_dcl)
   4.660 +        |> (curry op COMP) (assume a_D)
   4.661 +        |> (curry op COMP) istep
   4.662 +        |> fold_rev implies_intr steps
   4.663 +        |> implies_intr a_D
   4.664 +        |> implies_intr D_dcl
   4.665 +        |> implies_intr D_subset
   4.666 +
   4.667 +  val subset_induct_all = fold_rev (forall_intr o cterm_of thy) [P, a, D] subset_induct_rule
   4.668 +
   4.669 +  val simple_induct_rule =
   4.670 +      subset_induct_rule
   4.671 +        |> forall_intr (cterm_of thy D)
   4.672 +        |> forall_elim (cterm_of thy acc_R)
   4.673 +        |> assume_tac 1 |> Seq.hd
   4.674 +        |> (curry op COMP) (acc_downward
   4.675 +                              |> (instantiate' [SOME (ctyp_of thy domT)]
   4.676 +                                               (map (SOME o cterm_of thy) [R, x, z]))
   4.677 +                              |> forall_intr (cterm_of thy z)
   4.678 +                              |> forall_intr (cterm_of thy x))
   4.679 +        |> forall_intr (cterm_of thy a)
   4.680 +        |> forall_intr (cterm_of thy P)
   4.681 +    in
   4.682 +      (subset_induct_all, simple_induct_rule)
   4.683 +    end
   4.684 +
   4.685 +
   4.686 +
   4.687 +(* FIXME: This should probably use fixed goals, to be more reliable and faster *)
   4.688 +fun mk_domain_intro thy (Globals {domT, ...}) R R_cases clause =
   4.689 +    let
   4.690 +      val ClauseInfo {cdata = ClauseContext {qs, gs, lhs, rhs, cqs, ...}, 
   4.691 +                      qglr = (oqs, _, _, _), ...} = clause
   4.692 +      val goal = Trueprop (mk_acc domT R $ lhs)
   4.693 +                          |> fold_rev (curry Logic.mk_implies) gs
   4.694 +                          |> cterm_of thy
   4.695 +    in
   4.696 +      Goal.init goal 
   4.697 +      |> (SINGLE (resolve_tac [accI] 1)) |> the
   4.698 +      |> (SINGLE (eresolve_tac [forall_elim_vars 0 R_cases] 1))  |> the
   4.699 +      |> (SINGLE (CLASIMPSET auto_tac)) |> the
   4.700 +      |> Goal.conclude
   4.701 +      |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
   4.702 +    end
   4.703 +
   4.704 +
   4.705 +
   4.706 +(** Termination rule **)
   4.707 +
   4.708 +val wf_induct_rule = thm "FunDef.wfP_induct_rule";
   4.709 +val wf_in_rel = thm "FunDef.wf_in_rel";
   4.710 +val in_rel_def = thm "FunDef.in_rel_def";
   4.711 +
   4.712 +fun mk_nest_term_case thy globals R' ihyp clause =
   4.713 +    let
   4.714 +      val Globals {x, z, ...} = globals
   4.715 +      val ClauseInfo {cdata = ClauseContext {qs,cqs,ags,lhs,rhs,case_hyp,...},tree,
   4.716 +                      qglr=(oqs, _, _, _), ...} = clause
   4.717 +          
   4.718 +      val ih_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ihyp
   4.719 +                    
   4.720 +      fun step (fixes, assumes) (_ $ arg) u (sub,(hyps,thms)) = 
   4.721 +          let
   4.722 +            val used = map (fn ((f,a),thm) => FundefCtxTree.export_thm thy (f, map prop_of a) thm) (u @ sub)
   4.723 +                       
   4.724 +            val hyp = Trueprop (R' $ arg $ lhs)
   4.725 +                      |> fold_rev (curry Logic.mk_implies o prop_of) used
   4.726 +                      |> FundefCtxTree.export_term (fixes, map prop_of assumes) 
   4.727 +                      |> fold_rev (curry Logic.mk_implies o prop_of) ags
   4.728 +                      |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
   4.729 +                      |> cterm_of thy
   4.730 +                      
   4.731 +            val thm = assume hyp
   4.732 +                      |> fold forall_elim cqs
   4.733 +                      |> fold implies_elim_swp ags
   4.734 +                      |> FundefCtxTree.import_thm thy (fixes, assumes) (*  "(arg, lhs) : R'"  *)
   4.735 +                      |> fold implies_elim_swp used
   4.736 +                      
   4.737 +            val acc = thm COMP ih_case
   4.738 +                      
   4.739 +            val z_eq_arg = cterm_of thy (Trueprop (HOLogic.mk_eq (z, arg)))
   4.740 +                           
   4.741 +            val arg_eq_z = (assume z_eq_arg) RS sym
   4.742 +                           
   4.743 +            val z_acc = simplify (HOL_basic_ss addsimps [arg_eq_z]) acc (* fragile, slow... *)
   4.744 +                        |> implies_intr (cprop_of case_hyp)
   4.745 +                        |> implies_intr z_eq_arg
   4.746 +
   4.747 +            val z_eq_arg = assume (cterm_of thy (Trueprop (mk_eq (z, arg))))
   4.748 +            val x_eq_lhs = assume (cterm_of thy (Trueprop (mk_eq (x, lhs))))
   4.749 +                           
   4.750 +            val ethm = (z_acc OF [z_eq_arg, x_eq_lhs])
   4.751 +                         |> FundefCtxTree.export_thm thy (fixes, 
   4.752 +                                                          prop_of z_eq_arg :: prop_of x_eq_lhs :: map prop_of (ags @ assumes))
   4.753 +                         |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
   4.754 +
   4.755 +            val sub' = sub @ [(([],[]), acc)]
   4.756 +          in
   4.757 +            (sub', (hyp :: hyps, ethm :: thms))
   4.758 +          end
   4.759 +        | step _ _ _ _ = raise Match
   4.760 +    in
   4.761 +      FundefCtxTree.traverse_tree step tree
   4.762 +    end
   4.763 +    
   4.764 +    
   4.765 +fun mk_nest_term_rule thy globals R R_cases clauses =
   4.766 +    let
   4.767 +      val Globals { domT, x, z, ... } = globals
   4.768 +      val acc_R = mk_acc domT R
   4.769 +                  
   4.770 +      val R' = Free ("R", fastype_of R)
   4.771 +               
   4.772 +      val Rrel = Free ("R", mk_relT (domT, domT))
   4.773 +      val inrel_R = Const ("FunDef.in_rel", mk_relT (domT, domT) --> fastype_of R) $ Rrel
   4.774 +                    
   4.775 +      val wfR' = cterm_of thy (Trueprop (Const ("FunDef.wfP", (domT --> domT --> boolT) --> boolT) $ R')) (* "wf R'" *)
   4.776 +                          
   4.777 +      (* Inductive Hypothesis: !!z. (z,x):R' ==> z : acc R *)
   4.778 +      val ihyp = all domT $ Abs ("z", domT, 
   4.779 +                                 implies $ Trueprop (R' $ Bound 0 $ x)
   4.780 +                                         $ Trueprop (acc_R $ Bound 0))
   4.781 +                     |> cterm_of thy
   4.782 +
   4.783 +      val ihyp_a = assume ihyp |> forall_elim_vars 0
   4.784 +                   
   4.785 +      val R_z_x = cterm_of thy (Trueprop (R $ z $ x)) 
   4.786 +                  
   4.787 +      val (hyps,cases) = fold (mk_nest_term_case thy globals R' ihyp_a) clauses ([],[])
   4.788 +    in
   4.789 +      R_cases
   4.790 +        |> forall_elim (cterm_of thy z)
   4.791 +        |> forall_elim (cterm_of thy x)
   4.792 +        |> forall_elim (cterm_of thy (acc_R $ z))
   4.793 +        |> curry op COMP (assume R_z_x)
   4.794 +        |> fold_rev (curry op COMP) cases
   4.795 +        |> implies_intr R_z_x
   4.796 +        |> forall_intr (cterm_of thy z)
   4.797 +        |> (fn it => it COMP accI)
   4.798 +        |> implies_intr ihyp
   4.799 +        |> forall_intr (cterm_of thy x)
   4.800 +        |> (fn it => Drule.compose_single(it,2,wf_induct_rule))
   4.801 +        |> curry op RS (assume wfR')
   4.802 +        |> fold implies_intr hyps
   4.803 +        |> implies_intr wfR'
   4.804 +        |> forall_intr (cterm_of thy R')
   4.805 +        |> forall_elim (cterm_of thy (inrel_R))
   4.806 +        |> curry op RS wf_in_rel
   4.807 +        |> full_simplify (HOL_basic_ss addsimps [in_rel_def])
   4.808 +        |> forall_intr (cterm_of thy Rrel)
   4.809 +    end
   4.810 +    
   4.811 +
   4.812 +
   4.813 +(* Tail recursion (probably very fragile)
   4.814 + *
   4.815 + * FIXME:
   4.816 + * - Need to do forall_elim_vars on psimps: Unneccesary, if psimps would be taken from the same context.
   4.817 + * - Must we really replace the fvar by f here?
   4.818 + * - Splitting is not configured automatically: Problems with case?
   4.819 + *)
   4.820 +fun mk_trsimps octxt globals f G R f_def R_cases G_induct clauses psimps =
   4.821 +    let
   4.822 +      val Globals {domT, ranT, fvar, ...} = globals
   4.823 +
   4.824 +      val R_cases = forall_elim_vars 0 R_cases (* FIXME: Should be already in standard form. *)
   4.825 +
   4.826 +      val graph_implies_dom = (* "G ?x ?y ==> dom ?x"  *)
   4.827 +          Goal.prove octxt ["x", "y"] [HOLogic.mk_Trueprop (G $ Free ("x", domT) $ Free ("y", ranT))]
   4.828 +                     (HOLogic.mk_Trueprop (mk_acc domT R $ Free ("x", domT)))
   4.829 +                     (fn {prems=[a], ...} => 
   4.830 +                         ((rtac (G_induct OF [a]))
   4.831 +                            THEN_ALL_NEW (rtac accI)
   4.832 +                            THEN_ALL_NEW (etac R_cases)
   4.833 +                            THEN_ALL_NEW (SIMPSET' asm_full_simp_tac)) 1)
   4.834 +
   4.835 +      val default_thm = (forall_intr_vars graph_implies_dom) COMP (f_def COMP fundef_default_value)
   4.836 +
   4.837 +      fun mk_trsimp clause psimp =
   4.838 +          let
   4.839 +            val ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {ctxt, cqs, qs, gs, lhs, rhs, ...}, ...} = clause
   4.840 +            val thy = ProofContext.theory_of ctxt
   4.841 +            val rhs_f = Pattern.rewrite_term thy [(fvar, f)] [] rhs
   4.842 +                        
   4.843 +            val trsimp = Logic.list_implies(gs, HOLogic.mk_Trueprop (HOLogic.mk_eq(f $ lhs, rhs_f))) (* "f lhs = rhs" *)
   4.844 +            val lhs_acc = (mk_acc domT R $ lhs) (* "acc R lhs" *)
   4.845 +          in
   4.846 +            Goal.prove ctxt [] [] trsimp
   4.847 +                       (fn _ =>  
   4.848 +                           rtac (instantiate' [] [SOME (cterm_of thy lhs_acc)] case_split) 1
   4.849 +                                THEN (rtac (forall_elim_vars 0 psimp) THEN_ALL_NEW assume_tac) 1
   4.850 +                                THEN (SIMPSET (fn ss => asm_full_simp_tac (ss addsimps [default_thm]) 1))
   4.851 +                                THEN (etac not_accP_down 1)
   4.852 +                                THEN ((etac R_cases) THEN_ALL_NEW (SIMPSET' (fn ss => asm_full_simp_tac (ss addsimps [default_thm])))) 1)
   4.853 +              |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
   4.854 +          end
   4.855 +    in
   4.856 +      map2 mk_trsimp clauses psimps
   4.857 +    end
   4.858 +
   4.859 +
   4.860 +fun prepare_fundef config defname (fname, fT, mixfix) abstract_qglrs default_str lthy =
   4.861 +    let
   4.862 +      val FundefConfig {domintros, tailrec, ...} = config 
   4.863 +                                                         
   4.864 +      val fvar = Free (fname, fT)
   4.865 +      val domT = domain_type fT
   4.866 +      val ranT = range_type fT
   4.867 +                            
   4.868 +      val [default] = fst (Variable.importT_terms (fst (ProofContext.read_termTs lthy (K false) (K NONE) (K NONE) [] [(default_str, fT)])) lthy) (* FIXME *)
   4.869 +
   4.870 +      val congs = get_fundef_congs (Context.Proof lthy)
   4.871 +      val (globals, ctxt') = fix_globals domT ranT fvar lthy
   4.872 +
   4.873 +      val Globals { x, h, ... } = globals
   4.874 +
   4.875 +      val clauses = map (mk_clause_context x ctxt') abstract_qglrs 
   4.876 +
   4.877 +      val n = length abstract_qglrs
   4.878 +
   4.879 +      val congs_deps = map (fn c => (c, FundefCtxTree.cong_deps c)) (congs @ FundefCtxTree.add_congs) (* FIXME: Save in theory *)
   4.880 +              
   4.881 +      fun build_tree (ClauseContext { ctxt, rhs, ...}) = 
   4.882 +            FundefCtxTree.mk_tree congs_deps (fname, fT) h ctxt rhs
   4.883 +
   4.884 +      val trees = map build_tree clauses
   4.885 +      val RCss = map find_calls trees
   4.886 +
   4.887 +      val ((G, GIntro_thms, G_elim, G_induct), lthy) = 
   4.888 +          PROFILE "def_graph" (define_graph (graph_name defname) fvar domT ranT clauses RCss) lthy
   4.889 +
   4.890 +      val ((f, f_defthm), lthy) = 
   4.891 +          PROFILE "def_fun" (define_function (defname ^ "_sum_def") (fname, mixfix) domT ranT G default) lthy
   4.892 +
   4.893 +      val RCss = map (map (inst_RC (ProofContext.theory_of lthy) fvar f)) RCss
   4.894 +      val trees = map (FundefCtxTree.inst_tree (ProofContext.theory_of lthy) fvar f) trees
   4.895 +
   4.896 +      val ((R, RIntro_thmss, R_elim), lthy) = 
   4.897 +          PROFILE "def_rel" (define_recursion_relation (rel_name defname) domT ranT fvar f abstract_qglrs clauses RCss) lthy
   4.898 +
   4.899 +      val (_, lthy) = 
   4.900 +          LocalTheory.abbrev Syntax.default_mode ((defname ^ "_dom", NoSyn), mk_acc domT R) lthy
   4.901 +
   4.902 +      val newthy = ProofContext.theory_of lthy
   4.903 +      val clauses = map (transfer_clause_ctx newthy) clauses
   4.904 +
   4.905 +      val cert = cterm_of (ProofContext.theory_of lthy)
   4.906 +
   4.907 +      val xclauses = PROFILE "xclauses" (map7 (mk_clause_info globals G f) (1 upto n) clauses abstract_qglrs trees RCss GIntro_thms) RIntro_thmss
   4.908 +
   4.909 +      val complete = mk_completeness globals clauses abstract_qglrs |> cert |> assume
   4.910 +      val compat = mk_compat_proof_obligations domT ranT fvar f abstract_qglrs |> map (cert #> assume)
   4.911 +
   4.912 +      val compat_store = store_compat_thms n compat
   4.913 +
   4.914 +      val (goalstate, values) = PROFILE "prove_stuff" (prove_stuff newthy congs globals G f R xclauses complete compat compat_store G_elim) f_defthm
   4.915 +
   4.916 +      val mk_trsimps = mk_trsimps lthy globals f G R f_defthm R_elim G_induct xclauses
   4.917 +
   4.918 +      fun mk_partial_rules provedgoal =
   4.919 +          let
   4.920 +            val newthy = theory_of_thm provedgoal (*FIXME*) 
   4.921 +
   4.922 +            val (graph_is_function, complete_thm) = 
   4.923 +                provedgoal
   4.924 +                  |> Conjunction.elim
   4.925 +                  |> apfst (forall_elim_vars 0)
   4.926 +                
   4.927 +            val f_iff = graph_is_function RS (f_defthm RS ex1_implies_iff)
   4.928 +                        
   4.929 +            val psimps = PROFILE "Proving simplification rules" (mk_psimps newthy globals R xclauses values f_iff) graph_is_function
   4.930 +                         
   4.931 +            val (subset_pinduct, simple_pinduct) = PROFILE "Proving partial induction rule" 
   4.932 +                                                           (mk_partial_induct_rule newthy globals R complete_thm) xclauses
   4.933 +                                                   
   4.934 +                                                   
   4.935 +            val total_intro = PROFILE "Proving nested termination rule" (mk_nest_term_rule newthy globals R R_elim) xclauses
   4.936 +                              
   4.937 +            val dom_intros = if domintros 
   4.938 +                             then SOME (PROFILE "Proving domain introduction rules" (map (mk_domain_intro newthy globals R R_elim)) xclauses)
   4.939 +                             else NONE
   4.940 +            val trsimps = if tailrec then SOME (mk_trsimps psimps) else NONE
   4.941 +                                                                        
   4.942 +          in 
   4.943 +            FundefResult {f=f, G=G, R=R, cases=complete_thm, 
   4.944 +                          psimps=psimps, subset_pinducts=[subset_pinduct], simple_pinducts=[simple_pinduct], 
   4.945 +                          termination=total_intro, trsimps=trsimps,
   4.946 +                          domintros=dom_intros}
   4.947 +          end
   4.948 +    in
   4.949 +      ((f, goalstate, mk_partial_rules), lthy)
   4.950 +    end
   4.951 +
   4.952 +
   4.953 +
   4.954 +
   4.955 +end
     5.1 --- a/src/HOL/Tools/function_package/fundef_lib.ML	Mon Jan 22 16:53:33 2007 +0100
     5.2 +++ b/src/HOL/Tools/function_package/fundef_lib.ML	Mon Jan 22 17:29:43 2007 +0100
     5.3 @@ -10,14 +10,34 @@
     5.4  
     5.5  structure FundefLib = struct
     5.6  
     5.7 +(* ==> library/string *)
     5.8  fun plural sg pl [x] = sg
     5.9    | plural sg pl _ = pl
    5.10  
    5.11 +
    5.12 +
    5.13 +fun map_option f NONE = NONE 
    5.14 +  | map_option f (SOME x) = SOME (f x);
    5.15 +
    5.16 +fun fold_option f NONE y = y
    5.17 +  | fold_option f (SOME x) y = f x y;
    5.18 +
    5.19 +fun fold_map_option f NONE y = (NONE, y)
    5.20 +  | fold_map_option f (SOME x) y = apfst SOME (f x y);
    5.21 +
    5.22 +
    5.23 +
    5.24 +
    5.25 +
    5.26 +
    5.27 +(* ??? *)
    5.28  fun eq_str (s : string, t) = (s = t) (* monomorphic equality on strings *)
    5.29  
    5.30 +(* ==> logic.ML? *)
    5.31  fun mk_forall v t = all (fastype_of v) $ lambda v t
    5.32  
    5.33 -(* Constructs a tupled abstraction from an arbitrarily nested tuple of variables and a term. *)
    5.34 +(* lambda-abstracts over an arbitrarily nested tuple
    5.35 +  ==> hologic.ML? *)
    5.36  fun tupled_lambda vars t =
    5.37      case vars of
    5.38        (Free v) => lambda (Free v) t
    5.39 @@ -86,16 +106,12 @@
    5.40  
    5.41  
    5.42  (* forms all "unordered pairs": [1, 2, 3] ==> [(1, 1), (1, 2), (1, 3), (2, 2), (2, 3), (3, 3)] *)
    5.43 +(* ==> library *)
    5.44  fun unordered_pairs [] = []
    5.45    | unordered_pairs (x::xs) = map (pair x) (x::xs) @ unordered_pairs xs
    5.46  
    5.47  
    5.48 -(* Replaces Frees by name. Probably quicker than Pattern.rewrite_terms, and works with loose Bounds. *)
    5.49 -fun replace_frees assoc =
    5.50 -    map_aterms (fn c as Free (n, _) => the_default c (AList.lookup (op =) assoc n)
    5.51 -                 | t => t)
    5.52 -
    5.53 -
    5.54 +(* term.ML *)
    5.55  fun forall_aterms P (t $ u) = forall_aterms P t andalso forall_aterms P u
    5.56    | forall_aterms P (Abs (_, _, t)) = forall_aterms P t
    5.57    | forall_aterms P a = P a
    5.58 @@ -104,6 +120,11 @@
    5.59  
    5.60  
    5.61  
    5.62 +(* Replaces Frees by name. Probably quicker than Pattern.rewrite_terms, and works with loose Bounds. *)
    5.63 +fun replace_frees assoc =
    5.64 +    map_aterms (fn c as Free (n, _) => the_default c (AList.lookup (op =) assoc n)
    5.65 +                 | t => t)
    5.66 +
    5.67  
    5.68  fun rename_bound n (Q $ Abs(_, T, b)) = (Q $ Abs(n, T, b))
    5.69    | rename_bound n _ = raise Match
    5.70 @@ -116,7 +137,7 @@
    5.71  fun forall_intr_rename (n, cv) thm =
    5.72      let
    5.73        val allthm = forall_intr cv thm
    5.74 -      val (_, abs) = Logic.dest_all (prop_of allthm)
    5.75 +      val (_ $ abs) = prop_of allthm
    5.76      in
    5.77        Thm.rename_boundvars abs (Abs (n, dummyT, dummy_term)) allthm
    5.78      end
    5.79 @@ -127,11 +148,6 @@
    5.80      Term.add_frees t []
    5.81      |> filter_out (Variable.is_fixed ctxt o fst)
    5.82      |> rev
    5.83 -(*
    5.84 -    rev (fold_aterms (fn  Free (v as (x, _)) =>
    5.85 -                          if Variable.is_fixed ctxt x then I else insert (fn ((x, _),(y, _)) => x = y) v | _ => I) t [])
    5.86 -*)
    5.87 -
    5.88  
    5.89  
    5.90  end
     6.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Mon Jan 22 16:53:33 2007 +0100
     6.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Mon Jan 22 17:29:43 2007 +0100
     6.3 @@ -40,6 +40,8 @@
     6.4  
     6.5  val note_theorem = LocalTheory.note Thm.theoremK
     6.6  
     6.7 +fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_" 
     6.8 +
     6.9  fun burrow_snd f ps = (* ('a list -> 'b list) -> ('c * 'a) list -> ('c * 'b) list *)
    6.10      let val (xs, ys) = split_list ps
    6.11      in xs ~~ f ys end
    6.12 @@ -47,49 +49,46 @@
    6.13  fun restore_spec_structure reps spec =
    6.14      (burrow o burrow_snd o burrow o K) reps spec
    6.15  
    6.16 -fun add_simps label moreatts mutual_info fixes psimps spec lthy =
    6.17 +fun add_simps fixes spec sort label moreatts simps lthy =
    6.18      let
    6.19        val fnames = map (fst o fst) fixes
    6.20  
    6.21 -      val (saved_spec_psimps, lthy) =
    6.22 -        fold_map (fold_map note_theorem) (restore_spec_structure psimps spec) lthy
    6.23 -      val saved_psimps = flat (map snd (flat saved_spec_psimps))
    6.24 +      val (saved_spec_simps, lthy) =
    6.25 +        fold_map (fold_map note_theorem) (restore_spec_structure simps spec) lthy
    6.26 +      val saved_simps = flat (map snd (flat saved_spec_simps))
    6.27  
    6.28 -      val psimps_by_f = FundefMutual.sort_by_function mutual_info fnames saved_psimps
    6.29 +      val simps_by_f = sort saved_simps
    6.30  
    6.31 -      fun add_for_f fname psimps =
    6.32 +      fun add_for_f fname simps =
    6.33          note_theorem
    6.34            ((NameSpace.qualified fname label, Attrib.internal (K Simplifier.simp_add) :: moreatts),
    6.35 -            psimps) #> snd
    6.36 +            simps) #> snd
    6.37      in
    6.38 -      (saved_psimps,
    6.39 -       fold2 add_for_f fnames psimps_by_f lthy)
    6.40 +      (saved_simps,
    6.41 +       fold2 add_for_f fnames simps_by_f lthy)
    6.42      end
    6.43  
    6.44  
    6.45 -fun fundef_afterqed config fixes spec mutual_info defname data [[result]] lthy =
    6.46 +fun fundef_afterqed config fixes spec defname cont sort_cont [[proof]] lthy =
    6.47      let
    6.48 -      val FundefConfig { domintros, ...} = config
    6.49 -      val Prep {f, R, ...} = data
    6.50 -      val fundef_data = FundefMutual.mk_partial_rules_mutual lthy mutual_info data result
    6.51 -      val FundefMResult {psimps, subset_pinducts, simple_pinducts, termination, domintros, cases, ...} = fundef_data
    6.52 +      val FundefResult {f, R, psimps, trsimps, subset_pinducts, simple_pinducts, termination, domintros, cases, ...} = 
    6.53 +          cont (Goal.close_result proof)
    6.54 +
    6.55        val qualify = NameSpace.qualified defname
    6.56 +      val addsimps = add_simps fixes spec sort_cont
    6.57  
    6.58        val (((psimps', pinducts'), (_, [termination'])), lthy) =
    6.59            lthy
    6.60 -            |> PROFILE "adding_psimps" (add_simps "psimps" [] mutual_info fixes psimps spec)
    6.61 -            ||>> PROFILE "adding pinduct"
    6.62 -              (note_theorem ((qualify "pinduct",
    6.63 -                [Attrib.internal (K (InductAttrib.induct_set ""))]), simple_pinducts))
    6.64 -            ||>> PROFILE "adding termination"
    6.65 -              (note_theorem ((qualify "termination", []), [termination]))
    6.66 -            ||> (snd o PROFILE "adding cases" (note_theorem ((qualify "cases", []), [cases])))
    6.67 -            ||> (snd o PROFILE "adding domintros" (note_theorem ((qualify "domintros", []), domintros)))
    6.68 +            |> addsimps "psimps" [] psimps
    6.69 +            ||> fold_option (snd oo addsimps "simps" []) trsimps
    6.70 +            ||>> note_theorem ((qualify "pinduct",
    6.71 +                                [Attrib.internal (K (InductAttrib.induct_set ""))]), simple_pinducts)
    6.72 +            ||>> note_theorem ((qualify "termination", []), [termination])
    6.73 +            ||> (snd o note_theorem ((qualify "cases", []), [cases]))
    6.74 +            ||> fold_option (snd oo curry note_theorem (qualify "domintros", [])) domintros
    6.75  
    6.76 -      val cdata = FundefCtxData { fixes=fixes, spec=spec, mutual=mutual_info, psimps=psimps',
    6.77 +      val cdata = FundefCtxData { add_simps=addsimps, psimps=psimps',
    6.78                                    pinducts=snd pinducts', termination=termination', f=f, R=R }
    6.79 -
    6.80 -
    6.81      in
    6.82        lthy  (* FIXME proper handling of morphism *)
    6.83          |> LocalTheory.declaration (fn phi => add_fundef_data defname cdata) (* save in target *)
    6.84 @@ -117,33 +116,36 @@
    6.85  
    6.86  fun gen_add_fundef prep_spec fixspec eqnss_flags config lthy =
    6.87      let
    6.88 -      val FundefConfig {sequential, default, ...} = config
    6.89 +      val FundefConfig {sequential, default, tailrec, ...} = config
    6.90  
    6.91        val ((fixes, spec), ctxt') = prep_with_flags prep_spec fixspec eqnss_flags sequential lthy
    6.92 +
    6.93 +      val defname = mk_defname fixes
    6.94 +
    6.95        val t_eqns = spec
    6.96                       |> flat |> map snd |> flat (* flatten external structure *)
    6.97  
    6.98 -      val ((mutual_info, name, prep_result as Prep {goal, goalI, ...}), lthy) =
    6.99 -          FundefMutual.prepare_fundef_mutual fixes t_eqns default lthy
   6.100 +      val ((goalstate, cont, sort_cont), lthy) =
   6.101 +          FundefMutual.prepare_fundef_mutual config defname fixes t_eqns default lthy
   6.102  
   6.103 -      val afterqed = fundef_afterqed config fixes spec mutual_info name prep_result
   6.104 +      val afterqed = fundef_afterqed config fixes spec defname cont sort_cont
   6.105      in
   6.106 -      (name, lthy
   6.107 -         |> Proof.theorem_i NONE afterqed [[(goal, [])]]
   6.108 -         |> Proof.refine (Method.primitive_text (fn _ => goalI)) |> Seq.hd)
   6.109 +      (defname, lthy
   6.110 +         |> Proof.theorem_i NONE afterqed [[(Logic.unprotect (concl_of goalstate), [])]]
   6.111 +         |> Proof.refine (Method.primitive_text (fn _ => goalstate)) |> Seq.hd)
   6.112      end
   6.113  
   6.114  
   6.115  fun total_termination_afterqed defname data [[totality]] lthy =
   6.116      let
   6.117 -      val FundefCtxData { fixes, spec, mutual, psimps, pinducts, ... } = data
   6.118 +      val FundefCtxData { add_simps, psimps, pinducts, ... } = data
   6.119  
   6.120 -      val totality = PROFILE "closing" Goal.close_result totality
   6.121 +      val totality = Goal.close_result totality
   6.122  
   6.123        val remove_domain_condition = full_simplify (HOL_basic_ss addsimps [totality, True_implies_equals])
   6.124  
   6.125 -      val tsimps = PROFILE "making tsimps" (map remove_domain_condition) psimps
   6.126 -      val tinduct = PROFILE "making tinduct" (map remove_domain_condition) pinducts
   6.127 +      val tsimps = map remove_domain_condition psimps
   6.128 +      val tinduct = map remove_domain_condition pinducts
   6.129  
   6.130          (* FIXME: How to generate code from (possibly) local contexts*)
   6.131        val has_guards = exists ((fn (Const ("Trueprop", _) $ _) => false | _ => true) o prop_of) tsimps
   6.132 @@ -152,26 +154,26 @@
   6.133        val qualify = NameSpace.qualified defname;
   6.134      in
   6.135        lthy
   6.136 -        |> PROFILE "adding tsimps" (add_simps "simps" allatts mutual fixes tsimps spec) |> snd
   6.137 -        |> PROFILE "adding tinduct" (note_theorem ((qualify "induct", []), tinduct)) |> snd
   6.138 +        |> add_simps "simps" allatts tsimps |> snd
   6.139 +        |> note_theorem ((qualify "induct", []), tinduct) |> snd
   6.140      end
   6.141  
   6.142  
   6.143  fun setup_termination_proof name_opt lthy =
   6.144      let
   6.145 -        val name = the_default (get_last_fundef (Context.Proof lthy)) name_opt
   6.146 -        val data = the (get_fundef_data name (Context.Proof lthy))
   6.147 -                   handle Option.Option => raise ERROR ("No such function definition: " ^ name)
   6.148 +        val defname = the_default (get_last_fundef (Context.Proof lthy)) name_opt
   6.149 +        val data = the (get_fundef_data defname (Context.Proof lthy))
   6.150 +                   handle Option.Option => raise ERROR ("No such function definition: " ^ defname)
   6.151  
   6.152 -        val FundefCtxData {termination, f, R, ...} = data
   6.153 -        val goal = FundefTermination.mk_total_termination_goal f R
   6.154 +        val FundefCtxData {termination, R, ...} = data
   6.155 +        val goal = FundefTermination.mk_total_termination_goal R
   6.156      in
   6.157        lthy
   6.158          |> ProofContext.note_thmss_i ""
   6.159            [(("termination", [ContextRules.intro_query NONE]),
   6.160              [([Goal.norm_result termination], [])])] |> snd
   6.161          |> set_termination_rule termination
   6.162 -        |> Proof.theorem_i NONE (total_termination_afterqed name data) [[(goal, [])]]
   6.163 +        |> Proof.theorem_i NONE (total_termination_afterqed defname data) [[(goal, [])]]
   6.164      end
   6.165  
   6.166  
     7.1 --- a/src/HOL/Tools/function_package/fundef_prep.ML	Mon Jan 22 16:53:33 2007 +0100
     7.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.3 @@ -1,534 +0,0 @@
     7.4 -(*  Title:      HOL/Tools/function_package/fundef_prep.ML
     7.5 -    ID:         $Id$
     7.6 -    Author:     Alexander Krauss, TU Muenchen
     7.7 -
     7.8 -A package for general recursive function definitions.
     7.9 -Preparation step: makes auxiliary definitions and generates
    7.10 -proof obligations.
    7.11 -*)
    7.12 -
    7.13 -signature FUNDEF_PREP =
    7.14 -sig
    7.15 -    val prepare_fundef : string (* defname *)
    7.16 -                         -> (string * typ * mixfix) (* defined symbol *)
    7.17 -                         -> ((string * typ) list * term list * term * term) list (* specification *)
    7.18 -                         -> string (* default_value, not parsed yet *)
    7.19 -                         -> local_theory
    7.20 -                         -> FundefCommon.prep_result * term * local_theory
    7.21 -
    7.22 -end
    7.23 -
    7.24 -structure FundefPrep : FUNDEF_PREP =
    7.25 -struct
    7.26 -
    7.27 -
    7.28 -open FundefLib
    7.29 -open FundefCommon
    7.30 -open FundefAbbrev
    7.31 -
    7.32 -(* Theory dependencies. *)
    7.33 -val Pair_inject = thm "Product_Type.Pair_inject";
    7.34 -
    7.35 -val acc_induct_rule = thm "FunDef.accP_induct_rule"
    7.36 -
    7.37 -val ex1_implies_ex = thm "FunDef.fundef_ex1_existence"
    7.38 -val ex1_implies_un = thm "FunDef.fundef_ex1_uniqueness"
    7.39 -val ex1_implies_iff = thm "FunDef.fundef_ex1_iff"
    7.40 -
    7.41 -val conjunctionI = thm "conjunctionI";
    7.42 -
    7.43 -
    7.44 -
    7.45 -fun find_calls tree =
    7.46 -    let
    7.47 -      fun add_Ri (fixes,assumes) (_ $ arg) _ (_, xs) = ([], (fixes, assumes, arg) :: xs)
    7.48 -        | add_Ri _ _ _ _ = raise Match
    7.49 -    in
    7.50 -      rev (FundefCtxTree.traverse_tree add_Ri tree [])
    7.51 -    end
    7.52 -
    7.53 -
    7.54 -fun mk_compat_proof_obligations domT ranT fvar f glrs =
    7.55 -    let
    7.56 -      fun mk_impl ((qs, gs, lhs, rhs),(qs', gs', lhs', rhs')) =
    7.57 -          let
    7.58 -            val shift = incr_boundvars (length qs')
    7.59 -          in
    7.60 -            (implies $ Trueprop (eq_const domT $ shift lhs $ lhs')
    7.61 -                     $ Trueprop (eq_const ranT $ shift rhs $ rhs'))
    7.62 -              |> fold_rev (curry Logic.mk_implies) (map shift gs @ gs')
    7.63 -              |> fold_rev (fn (n,T) => fn b => all T $ Abs(n,T,b)) (qs @ qs')
    7.64 -              |> curry abstract_over fvar
    7.65 -              |> curry subst_bound f
    7.66 -          end
    7.67 -    in
    7.68 -      map mk_impl (unordered_pairs glrs)
    7.69 -    end
    7.70 -
    7.71 -
    7.72 -fun mk_completeness (Globals {x, Pbool, ...}) clauses qglrs =
    7.73 -    let
    7.74 -        fun mk_case (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) =
    7.75 -            Trueprop Pbool
    7.76 -                     |> curry Logic.mk_implies (Trueprop (mk_eq (x, lhs)))
    7.77 -                     |> fold_rev (curry Logic.mk_implies) gs
    7.78 -                     |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
    7.79 -    in
    7.80 -        Trueprop Pbool
    7.81 -                 |> fold_rev (curry Logic.mk_implies o mk_case) (clauses ~~ qglrs)
    7.82 -                 |> mk_forall_rename ("x", x)
    7.83 -                 |> mk_forall_rename ("P", Pbool)
    7.84 -    end
    7.85 -
    7.86 -
    7.87 -fun mk_clause_context x ctxt (pre_qs,pre_gs,pre_lhs,pre_rhs) =
    7.88 -    let
    7.89 -      val (qs, ctxt') = Variable.variant_fixes (map fst pre_qs) ctxt
    7.90 -                                           |>> map2 (fn (_, T) => fn n => Free (n, T)) pre_qs
    7.91 -
    7.92 -      val thy = ProofContext.theory_of ctxt'
    7.93 -
    7.94 -      fun inst t = subst_bounds (rev qs, t)
    7.95 -      val gs = map inst pre_gs
    7.96 -      val lhs = inst pre_lhs
    7.97 -      val rhs = inst pre_rhs
    7.98 -                
    7.99 -      val cqs = map (cterm_of thy) qs
   7.100 -      val ags = map (assume o cterm_of thy) gs
   7.101 -                  
   7.102 -      val case_hyp = assume (cterm_of thy (Trueprop (mk_eq (x, lhs))))
   7.103 -    in
   7.104 -      ClauseContext { ctxt = ctxt', qs = qs, gs = gs, lhs = lhs, rhs = rhs, 
   7.105 -                      cqs = cqs, ags = ags, case_hyp = case_hyp }
   7.106 -    end
   7.107 -      
   7.108 -
   7.109 -(* lowlevel term function *)
   7.110 -fun abstract_over_list vs body =
   7.111 -  let
   7.112 -    exception SAME;
   7.113 -    fun abs lev v tm =
   7.114 -      if v aconv tm then Bound lev
   7.115 -      else
   7.116 -        (case tm of
   7.117 -          Abs (a, T, t) => Abs (a, T, abs (lev + 1) v t)
   7.118 -        | t $ u => (abs lev v t $ (abs lev v u handle SAME => u) handle SAME => t $ abs lev v u)
   7.119 -        | _ => raise SAME);
   7.120 -  in 
   7.121 -    fold_index (fn (i,v) => fn t => abs i v t handle SAME => t) vs body
   7.122 -  end
   7.123 -
   7.124 -
   7.125 -
   7.126 -fun mk_clause_info globals G f no cdata qglr tree RCs GIntro_thm RIntro_thms =
   7.127 -    let
   7.128 -        val Globals {h, fvar, x, ...} = globals
   7.129 -
   7.130 -        val ClauseContext { ctxt, qs, cqs, ags, ... } = cdata
   7.131 -        val cert = Thm.cterm_of (ProofContext.theory_of ctxt)
   7.132 -
   7.133 -        (* Instantiate the GIntro thm with "f" and import into the clause context. *)
   7.134 -        val lGI = GIntro_thm
   7.135 -                    |> forall_elim (cert f)
   7.136 -                    |> fold forall_elim cqs
   7.137 -                    |> fold implies_elim_swp ags
   7.138 -
   7.139 -        fun mk_call_info (rcfix, rcassm, rcarg) RI =
   7.140 -            let
   7.141 -                val llRI = RI
   7.142 -                             |> fold forall_elim cqs
   7.143 -                             |> fold (forall_elim o cert o Free) rcfix
   7.144 -                             |> fold implies_elim_swp ags
   7.145 -                             |> fold implies_elim_swp rcassm
   7.146 -
   7.147 -                val h_assum =
   7.148 -                    Trueprop (G $ rcarg $ (h $ rcarg))
   7.149 -                              |> fold_rev (curry Logic.mk_implies o prop_of) rcassm
   7.150 -                              |> fold_rev (mk_forall o Free) rcfix
   7.151 -                              |> Pattern.rewrite_term (ProofContext.theory_of ctxt) [(f, h)] []
   7.152 -                              |> abstract_over_list (rev qs)
   7.153 -            in
   7.154 -                RCInfo {RIvs=rcfix, rcarg=rcarg, CCas=rcassm, llRI=llRI, h_assum=h_assum}
   7.155 -            end
   7.156 -
   7.157 -        val RC_infos = map2 mk_call_info RCs RIntro_thms
   7.158 -    in
   7.159 -        ClauseInfo
   7.160 -            {
   7.161 -             no=no,
   7.162 -             cdata=cdata,
   7.163 -             qglr=qglr,
   7.164 -
   7.165 -             lGI=lGI, 
   7.166 -             RCs=RC_infos,
   7.167 -             tree=tree
   7.168 -            }
   7.169 -    end
   7.170 -
   7.171 -
   7.172 -
   7.173 -
   7.174 -
   7.175 -
   7.176 -
   7.177 -(* replace this by a table later*)
   7.178 -fun store_compat_thms 0 thms = []
   7.179 -  | store_compat_thms n thms =
   7.180 -    let
   7.181 -        val (thms1, thms2) = chop n thms
   7.182 -    in
   7.183 -        (thms1 :: store_compat_thms (n - 1) thms2)
   7.184 -    end
   7.185 -
   7.186 -(* expects i <= j *)
   7.187 -fun lookup_compat_thm i j cts =
   7.188 -    nth (nth cts (i - 1)) (j - i)
   7.189 -
   7.190 -(* Returns "Gsi, Gsj, lhs_i = lhs_j |-- rhs_j_f = rhs_i_f" *)
   7.191 -(* if j < i, then turn around *)
   7.192 -fun get_compat_thm thy cts i j ctxi ctxj = 
   7.193 -    let
   7.194 -      val ClauseContext {cqs=cqsi,ags=agsi,lhs=lhsi,...} = ctxi
   7.195 -      val ClauseContext {cqs=cqsj,ags=agsj,lhs=lhsj,...} = ctxj
   7.196 -          
   7.197 -      val lhsi_eq_lhsj = cterm_of thy (Trueprop (mk_eq (lhsi, lhsj)))
   7.198 -    in if j < i then
   7.199 -         let
   7.200 -           val compat = lookup_compat_thm j i cts
   7.201 -         in
   7.202 -           compat         (* "!!qj qi. Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *)
   7.203 -                |> fold forall_elim (cqsj @ cqsi) (* "Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *)
   7.204 -                |> fold implies_elim_swp agsj
   7.205 -                |> fold implies_elim_swp agsi
   7.206 -                |> implies_elim_swp ((assume lhsi_eq_lhsj) RS sym) (* "Gsj, Gsi, lhsi = lhsj |-- rhsj = rhsi" *)
   7.207 -         end
   7.208 -       else
   7.209 -         let
   7.210 -           val compat = lookup_compat_thm i j cts
   7.211 -         in
   7.212 -               compat        (* "!!qi qj. Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *)
   7.213 -                 |> fold forall_elim (cqsi @ cqsj) (* "Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *)
   7.214 -                 |> fold implies_elim_swp agsi
   7.215 -                 |> fold implies_elim_swp agsj
   7.216 -                 |> implies_elim_swp (assume lhsi_eq_lhsj)
   7.217 -                 |> (fn thm => thm RS sym) (* "Gsi, Gsj, lhsi = lhsj |-- rhsj = rhsi" *)
   7.218 -         end
   7.219 -    end
   7.220 -
   7.221 -
   7.222 -
   7.223 -
   7.224 -(* Generates the replacement lemma in fully quantified form. *)
   7.225 -fun mk_replacement_lemma thy h ih_elim clause =
   7.226 -    let
   7.227 -        val ClauseInfo {cdata=ClauseContext {qs, lhs, rhs, cqs, ags, case_hyp, ...}, RCs, tree, ...} = clause
   7.228 -
   7.229 -        val ih_elim_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_elim
   7.230 -
   7.231 -        val Ris = map (fn RCInfo {llRI, ...} => llRI) RCs
   7.232 -        val h_assums = map (fn RCInfo {h_assum, ...} => assume (cterm_of thy (subst_bounds (rev qs, h_assum)))) RCs
   7.233 -
   7.234 -        val ih_elim_case_inst = instantiate' [] [NONE, SOME (cterm_of thy h)] ih_elim_case (* Should be done globally *)
   7.235 -
   7.236 -        val (eql, _) = FundefCtxTree.rewrite_by_tree thy h ih_elim_case_inst (Ris ~~ h_assums) tree
   7.237 -
   7.238 -        val replace_lemma = (eql RS meta_eq_to_obj_eq)
   7.239 -                                |> implies_intr (cprop_of case_hyp)
   7.240 -                                |> fold_rev (implies_intr o cprop_of) h_assums
   7.241 -                                |> fold_rev (implies_intr o cprop_of) ags
   7.242 -                                |> fold_rev forall_intr cqs
   7.243 -                                |> Goal.close_result
   7.244 -    in
   7.245 -      replace_lemma
   7.246 -    end
   7.247 -
   7.248 -
   7.249 -fun mk_uniqueness_clause thy globals f compat_store clausei clausej RLj =
   7.250 -    let
   7.251 -        val Globals {h, y, x, fvar, ...} = globals
   7.252 -        val ClauseInfo {no=i, cdata=cctxi as ClauseContext {ctxt=ctxti, lhs=lhsi, case_hyp, ...}, ...} = clausei
   7.253 -        val ClauseInfo {no=j, qglr=cdescj, RCs=RCsj, ...} = clausej
   7.254 -
   7.255 -        val cctxj as ClauseContext {ags = agsj', lhs = lhsj', rhs = rhsj', qs = qsj', cqs = cqsj', ...} 
   7.256 -            = mk_clause_context x ctxti cdescj
   7.257 -
   7.258 -        val rhsj'h = Pattern.rewrite_term thy [(fvar,h)] [] rhsj'
   7.259 -        val compat = get_compat_thm thy compat_store i j cctxi cctxj
   7.260 -        val Ghsj' = map (fn RCInfo {h_assum, ...} => assume (cterm_of thy (subst_bounds (rev qsj', h_assum)))) RCsj
   7.261 -
   7.262 -        val RLj_import = 
   7.263 -            RLj |> fold forall_elim cqsj'
   7.264 -                |> fold implies_elim_swp agsj'
   7.265 -                |> fold implies_elim_swp Ghsj'
   7.266 -
   7.267 -        val y_eq_rhsj'h = assume (cterm_of thy (Trueprop (mk_eq (y, rhsj'h))))
   7.268 -        val lhsi_eq_lhsj' = assume (cterm_of thy (Trueprop (mk_eq (lhsi, lhsj')))) (* lhs_i = lhs_j' |-- lhs_i = lhs_j' *)
   7.269 -    in
   7.270 -        (trans OF [case_hyp, lhsi_eq_lhsj']) (* lhs_i = lhs_j' |-- x = lhs_j' *)
   7.271 -        |> implies_elim RLj_import (* Rj1' ... Rjk', lhs_i = lhs_j' |-- rhs_j'_h = rhs_j'_f *)
   7.272 -        |> (fn it => trans OF [it, compat]) (* lhs_i = lhs_j', Gj', Rj1' ... Rjk' |-- rhs_j'_h = rhs_i_f *)
   7.273 -        |> (fn it => trans OF [y_eq_rhsj'h, it]) (* lhs_i = lhs_j', Gj', Rj1' ... Rjk', y = rhs_j_h' |-- y = rhs_i_f *)
   7.274 -        |> fold_rev (implies_intr o cprop_of) Ghsj'
   7.275 -        |> fold_rev (implies_intr o cprop_of) agsj' (* lhs_i = lhs_j' , y = rhs_j_h' |-- Gj', Rj1'...Rjk' ==> y = rhs_i_f *)
   7.276 -        |> implies_intr (cprop_of y_eq_rhsj'h)
   7.277 -        |> implies_intr (cprop_of lhsi_eq_lhsj')
   7.278 -        |> fold_rev forall_intr (cterm_of thy h :: cqsj')
   7.279 -    end
   7.280 -
   7.281 -
   7.282 -
   7.283 -fun mk_uniqueness_case thy globals G f ihyp ih_intro G_cases compat_store clauses rep_lemmas clausei =
   7.284 -    let
   7.285 -        val Globals {x, y, ranT, fvar, ...} = globals
   7.286 -        val ClauseInfo {cdata = ClauseContext {lhs, rhs, qs, cqs, ags, case_hyp, ...}, lGI, RCs, ...} = clausei
   7.287 -        val rhsC = Pattern.rewrite_term thy [(fvar, f)] [] rhs
   7.288 -
   7.289 -        val ih_intro_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_intro
   7.290 -
   7.291 -        fun prep_RC (RCInfo {llRI, RIvs, CCas, ...}) = (llRI RS ih_intro_case)
   7.292 -                                                            |> fold_rev (implies_intr o cprop_of) CCas
   7.293 -                                                            |> fold_rev (forall_intr o cterm_of thy o Free) RIvs
   7.294 -
   7.295 -        val existence = fold (curry op COMP o prep_RC) RCs lGI
   7.296 -
   7.297 -        val P = cterm_of thy (mk_eq (y, rhsC))
   7.298 -        val G_lhs_y = assume (cterm_of thy (Trueprop (G $ lhs $ y)))
   7.299 -
   7.300 -        val unique_clauses = map2 (mk_uniqueness_clause thy globals f compat_store clausei) clauses rep_lemmas
   7.301 -
   7.302 -        val uniqueness = G_cases
   7.303 -                           |> forall_elim (cterm_of thy lhs)
   7.304 -                           |> forall_elim (cterm_of thy y)
   7.305 -                           |> forall_elim P
   7.306 -                           |> implies_elim_swp G_lhs_y
   7.307 -                           |> fold implies_elim_swp unique_clauses
   7.308 -                           |> implies_intr (cprop_of G_lhs_y)
   7.309 -                           |> forall_intr (cterm_of thy y)
   7.310 -
   7.311 -        val P2 = cterm_of thy (lambda y (G $ lhs $ y)) (* P2 y := (lhs, y): G *)
   7.312 -
   7.313 -        val exactly_one =
   7.314 -            ex1I |> instantiate' [SOME (ctyp_of thy ranT)] [SOME P2, SOME (cterm_of thy rhsC)]
   7.315 -                 |> curry (op COMP) existence
   7.316 -                 |> curry (op COMP) uniqueness
   7.317 -                 |> simplify (HOL_basic_ss addsimps [case_hyp RS sym])
   7.318 -                 |> implies_intr (cprop_of case_hyp)
   7.319 -                 |> fold_rev (implies_intr o cprop_of) ags
   7.320 -                 |> fold_rev forall_intr cqs
   7.321 -
   7.322 -        val function_value =
   7.323 -            existence
   7.324 -              |> implies_intr ihyp
   7.325 -              |> implies_intr (cprop_of case_hyp)
   7.326 -              |> forall_intr (cterm_of thy x)
   7.327 -              |> forall_elim (cterm_of thy lhs)
   7.328 -              |> curry (op RS) refl
   7.329 -    in
   7.330 -        (exactly_one, function_value)
   7.331 -    end
   7.332 -
   7.333 -
   7.334 -
   7.335 -
   7.336 -fun prove_stuff thy congs globals G f R clauses complete compat compat_store G_elim f_def =
   7.337 -    let
   7.338 -        val Globals {h, domT, ranT, x, ...} = globals
   7.339 -
   7.340 -        val inst_ex1_ex =  f_def RS ex1_implies_ex
   7.341 -        val inst_ex1_un =  f_def RS ex1_implies_un
   7.342 -        val inst_ex1_iff = f_def RS ex1_implies_iff
   7.343 -
   7.344 -        (* Inductive Hypothesis: !!z. (z,x):R ==> EX!y. (z,y):G *)
   7.345 -        val ihyp = all domT $ Abs ("z", domT,
   7.346 -                                   implies $ Trueprop (R $ Bound 0 $ x)
   7.347 -                                           $ Trueprop (Const ("Ex1", (ranT --> boolT) --> boolT) $
   7.348 -                                                             Abs ("y", ranT, G $ Bound 1 $ Bound 0)))
   7.349 -                       |> cterm_of thy
   7.350 -
   7.351 -        val ihyp_thm = assume ihyp |> forall_elim_vars 0
   7.352 -        val ih_intro = ihyp_thm RS inst_ex1_ex
   7.353 -        val ih_elim = ihyp_thm RS inst_ex1_un
   7.354 -
   7.355 -        val _ = Output.debug (fn () => "Proving Replacement lemmas...")
   7.356 -        val repLemmas = map (mk_replacement_lemma thy h ih_elim) clauses
   7.357 -
   7.358 -        val _ = Output.debug (fn () => "Proving cases for unique existence...")
   7.359 -        val (ex1s, values) = 
   7.360 -            split_list (map (mk_uniqueness_case thy globals G f ihyp ih_intro G_elim compat_store clauses repLemmas) clauses)
   7.361 -
   7.362 -        val _ = Output.debug (fn () => "Proving: Graph is a function") (* FIXME: Rewrite this proof. *)
   7.363 -        val graph_is_function = complete
   7.364 -                                  |> forall_elim_vars 0
   7.365 -                                  |> fold (curry op COMP) ex1s
   7.366 -                                  |> implies_intr (ihyp)
   7.367 -                                  |> implies_intr (cterm_of thy (Trueprop (mk_acc domT R $ x)))
   7.368 -                                  |> forall_intr (cterm_of thy x)
   7.369 -                                  |> (fn it => Drule.compose_single (it, 2, acc_induct_rule)) (* "EX! y. (?x,y):G" *)
   7.370 -                                  |> (fn it => fold (forall_intr o cterm_of thy) (term_vars (prop_of it)) it)
   7.371 -
   7.372 -        val goal = complete COMP (graph_is_function COMP conjunctionI)
   7.373 -                            |> Goal.close_result
   7.374 -
   7.375 -        val goalI = Goal.protect goal
   7.376 -                                 |> fold_rev (implies_intr o cprop_of) compat
   7.377 -                                 |> implies_intr (cprop_of complete)
   7.378 -    in
   7.379 -      (prop_of goal, goalI, inst_ex1_iff, values)
   7.380 -    end
   7.381 -
   7.382 -
   7.383 -fun define_graph Gname fvar domT ranT clauses RCss lthy =
   7.384 -    let
   7.385 -      val GT = domT --> ranT --> boolT
   7.386 -      val Gvar = Free (the_single (Variable.variant_frees lthy [] [(Gname, GT)]))
   7.387 -
   7.388 -      fun mk_GIntro (ClauseContext {qs, gs, lhs, rhs, ...}) RCs =
   7.389 -          let
   7.390 -            fun mk_h_assm (rcfix, rcassm, rcarg) =
   7.391 -                Trueprop (Gvar $ rcarg $ (fvar $ rcarg))
   7.392 -                          |> fold_rev (curry Logic.mk_implies o prop_of) rcassm
   7.393 -                          |> fold_rev (mk_forall o Free) rcfix
   7.394 -          in
   7.395 -            Trueprop (Gvar $ lhs $ rhs)
   7.396 -                      |> fold_rev (curry Logic.mk_implies o mk_h_assm) RCs
   7.397 -                      |> fold_rev (curry Logic.mk_implies) gs
   7.398 -                      |> fold_rev mk_forall (fvar :: qs)
   7.399 -          end
   7.400 -          
   7.401 -      val G_intros = map2 mk_GIntro clauses RCss
   7.402 -                     
   7.403 -      val (GIntro_thms, (G, G_elim, lthy)) = 
   7.404 -          FundefInductiveWrap.inductive_def G_intros ((dest_Free Gvar, NoSyn), lthy)
   7.405 -    in
   7.406 -      ((G, GIntro_thms, G_elim), lthy)
   7.407 -    end
   7.408 -
   7.409 -
   7.410 -
   7.411 -fun define_function fdefname (fname, mixfix) domT ranT G default lthy =
   7.412 -    let
   7.413 -      val f_def = 
   7.414 -          Abs ("x", domT, Const ("FunDef.THE_default", ranT --> (ranT --> boolT) --> ranT) $ (default $ Bound 0) $
   7.415 -                                Abs ("y", ranT, G $ Bound 1 $ Bound 0))
   7.416 -              |> Envir.beta_norm (* FIXME: LocalTheory.def does not work if not beta-normal *)
   7.417 -          
   7.418 -      val ((f, (_, f_defthm)), lthy) =
   7.419 -        LocalTheory.def Thm.internalK ((fname ^ "C", mixfix), ((fdefname, []), f_def)) lthy
   7.420 -    in
   7.421 -      ((f, f_defthm), lthy)
   7.422 -    end
   7.423 -
   7.424 -
   7.425 -fun define_recursion_relation Rname domT ranT fvar f qglrs clauses RCss lthy =
   7.426 -    let
   7.427 -
   7.428 -      val RT = domT --> domT --> boolT
   7.429 -      val Rvar = Free (the_single (Variable.variant_frees lthy [] [(Rname, RT)]))
   7.430 -
   7.431 -      fun mk_RIntro (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) (rcfix, rcassm, rcarg) =
   7.432 -          Trueprop (Rvar $ rcarg $ lhs)
   7.433 -                    |> fold_rev (curry Logic.mk_implies o prop_of) rcassm
   7.434 -                    |> fold_rev (curry Logic.mk_implies) gs
   7.435 -                    |> fold_rev (mk_forall o Free) rcfix
   7.436 -                    |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
   7.437 -                    (* "!!qs xs. CS ==> G => (r, lhs) : R" *)
   7.438 -
   7.439 -      val R_intross = map2 (map o mk_RIntro) (clauses ~~ qglrs) RCss
   7.440 -
   7.441 -      val (RIntro_thmss, (R, R_elim, lthy)) = 
   7.442 -          fold_burrow FundefInductiveWrap.inductive_def R_intross ((dest_Free Rvar, NoSyn), lthy)
   7.443 -    in
   7.444 -      ((R, RIntro_thmss, R_elim), lthy)
   7.445 -    end
   7.446 -
   7.447 -
   7.448 -fun fix_globals domT ranT fvar ctxt =
   7.449 -    let
   7.450 -      val ([h, y, x, z, a, D, P, Pbool],ctxt') = 
   7.451 -          Variable.variant_fixes ["h_fd", "y_fd", "x_fd", "z_fd", "a_fd", "D_fd", "P_fd", "Pb_fd"] ctxt
   7.452 -    in
   7.453 -      (Globals {h = Free (h, domT --> ranT),
   7.454 -                y = Free (y, ranT),
   7.455 -                x = Free (x, domT),
   7.456 -                z = Free (z, domT),
   7.457 -                a = Free (a, domT),
   7.458 -                D = Free (D, domT --> boolT),
   7.459 -                P = Free (P, domT --> boolT),
   7.460 -                Pbool = Free (Pbool, boolT),
   7.461 -                fvar = fvar,
   7.462 -                domT = domT,
   7.463 -                ranT = ranT
   7.464 -               },
   7.465 -       ctxt')
   7.466 -    end
   7.467 -
   7.468 -
   7.469 -
   7.470 -fun inst_RC thy fvar f (rcfix, rcassm, rcarg) =
   7.471 -    let
   7.472 -      fun inst_term t = subst_bound(f, abstract_over (fvar, t))
   7.473 -    in
   7.474 -      (rcfix, map (assume o cterm_of thy o inst_term o prop_of) rcassm, inst_term rcarg)
   7.475 -    end
   7.476 -
   7.477 -
   7.478 -
   7.479 -fun prepare_fundef defname (fname, fT, mixfix) abstract_qglrs default_str lthy =
   7.480 -    let
   7.481 -      val fvar = Free (fname, fT)
   7.482 -      val domT = domain_type fT
   7.483 -      val ranT = range_type fT
   7.484 -                            
   7.485 -      val [default] = fst (Variable.importT_terms (fst (ProofContext.read_termTs lthy (K false) (K NONE) (K NONE) [] [(default_str, fT)])) lthy) (* FIXME *)
   7.486 -
   7.487 -      val congs = get_fundef_congs (Context.Proof lthy)
   7.488 -      val (globals, ctxt') = fix_globals domT ranT fvar lthy
   7.489 -
   7.490 -      val Globals { x, h, ... } = globals
   7.491 -
   7.492 -      val clauses = PROFILE "mk_clause_context" (map (mk_clause_context x ctxt')) abstract_qglrs 
   7.493 -
   7.494 -      val n = length abstract_qglrs
   7.495 -
   7.496 -      val congs_deps = map (fn c => (c, FundefCtxTree.cong_deps c)) (congs @ FundefCtxTree.add_congs) (* FIXME: Save in theory *)
   7.497 -              
   7.498 -      fun build_tree (ClauseContext { ctxt, rhs, ...}) = 
   7.499 -            FundefCtxTree.mk_tree congs_deps (fname, fT) h ctxt rhs
   7.500 -
   7.501 -      val trees = PROFILE "making trees" (map build_tree) clauses
   7.502 -      val RCss = PROFILE "finding calls" (map find_calls) trees
   7.503 -
   7.504 -      val ((G, GIntro_thms, G_elim), lthy) = PROFILE "def_graph" (define_graph (graph_name defname) fvar domT ranT clauses RCss) lthy
   7.505 -      val ((f, f_defthm), lthy) = PROFILE "def_fun" (define_function (defname ^ "_sum_def") (fname, mixfix) domT ranT G default) lthy
   7.506 -
   7.507 -      val RCss = PROFILE "inst_RCs" (map (map (inst_RC (ProofContext.theory_of lthy) fvar f))) RCss
   7.508 -      val trees = PROFILE "inst_trees" (map (FundefCtxTree.inst_tree (ProofContext.theory_of lthy) fvar f)) trees
   7.509 -
   7.510 -      val ((R, RIntro_thmss, R_elim), lthy) = 
   7.511 -          PROFILE "def_rel" (define_recursion_relation (rel_name defname) domT ranT fvar f abstract_qglrs clauses RCss) lthy
   7.512 -
   7.513 -      val (_, lthy) = PROFILE "abbrev"
   7.514 -        (LocalTheory.abbrev Syntax.default_mode ((defname ^ "_dom", NoSyn), mk_acc domT R)) lthy
   7.515 -
   7.516 -      val newthy = ProofContext.theory_of lthy
   7.517 -      val clauses = map (transfer_clause_ctx newthy) clauses
   7.518 -
   7.519 -      val cert = cterm_of (ProofContext.theory_of lthy)
   7.520 -
   7.521 -      val xclauses = PROFILE "xclauses" (map7 (mk_clause_info globals G f) (1 upto n) clauses abstract_qglrs trees RCss GIntro_thms) RIntro_thmss
   7.522 -
   7.523 -      val complete = PROFILE "mk_compl" (mk_completeness globals clauses) abstract_qglrs |> cert |> assume
   7.524 -      val compat = PROFILE "mk_compat" (mk_compat_proof_obligations domT ranT fvar f) abstract_qglrs |> map (cert #> assume)
   7.525 -
   7.526 -      val compat_store = store_compat_thms n compat
   7.527 -
   7.528 -      val (goal, goalI, ex1_iff, values) = PROFILE "prove_stuff" (prove_stuff newthy congs globals G f R xclauses complete compat compat_store G_elim) f_defthm
   7.529 -    in
   7.530 -        (Prep {globals = globals, f = f, G = G, R = R, goal = goal, goalI = goalI, values = values, clauses = xclauses, ex1_iff = ex1_iff, R_cases = R_elim}, f,
   7.531 -         lthy)
   7.532 -    end
   7.533 -
   7.534 -
   7.535 -
   7.536 -
   7.537 -end
     8.1 --- a/src/HOL/Tools/function_package/fundef_proof.ML	Mon Jan 22 16:53:33 2007 +0100
     8.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.3 @@ -1,327 +0,0 @@
     8.4 -(*  Title:      HOL/Tools/function_package/fundef_proof.ML
     8.5 -    ID:         $Id$
     8.6 -    Author:     Alexander Krauss, TU Muenchen
     8.7 -
     8.8 -A package for general recursive function definitions. 
     8.9 -Internal proofs.
    8.10 -*)
    8.11 -
    8.12 -
    8.13 -signature FUNDEF_PROOF =
    8.14 -sig
    8.15 -
    8.16 -    val mk_partial_rules : theory -> FundefCommon.prep_result 
    8.17 -         -> thm -> FundefCommon.fundef_result
    8.18 -end
    8.19 -
    8.20 -
    8.21 -structure FundefProof : FUNDEF_PROOF = 
    8.22 -struct
    8.23 -
    8.24 -open FundefLib
    8.25 -open FundefCommon
    8.26 -open FundefAbbrev
    8.27 -
    8.28 -(* Theory dependencies *)
    8.29 -val subsetD = thm "subsetD"
    8.30 -val split_apply = thm "Product_Type.split"
    8.31 -val wf_induct_rule = thm "FunDef.wfP_induct_rule";
    8.32 -val Pair_inject = thm "Product_Type.Pair_inject";
    8.33 -
    8.34 -val wf_in_rel = thm "FunDef.wf_in_rel";
    8.35 -val in_rel_def = thm "FunDef.in_rel_def";
    8.36 -
    8.37 -val acc_induct_rule = thm "FunDef.accP_induct_rule"
    8.38 -val acc_downward = thm "FunDef.accP_downward"
    8.39 -val accI = thm "FunDef.accPI"
    8.40 -
    8.41 -val acc_subset_induct = thm "FunDef.accP_subset_induct"
    8.42 -
    8.43 -val conjunctionD1 = thm "conjunctionD1"
    8.44 -val conjunctionD2 = thm "conjunctionD2"
    8.45 -
    8.46 -
    8.47 -fun mk_psimp thy globals R f_iff graph_is_function clause valthm =
    8.48 -    let
    8.49 -      val Globals {domT, z, ...} = globals
    8.50 -                                   
    8.51 -      val ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {qs, cqs, gs, lhs, rhs, ags, ...}, ...} = clause
    8.52 -      val lhs_acc = cterm_of thy (Trueprop (mk_acc domT R $ lhs)) (* "acc R lhs" *)
    8.53 -      val z_smaller = cterm_of thy (Trueprop (R $ z $ lhs)) (* "R z lhs" *)
    8.54 -    in
    8.55 -      ((assume z_smaller) RS ((assume lhs_acc) RS acc_downward))
    8.56 -        |> (fn it => it COMP graph_is_function)
    8.57 -        |> implies_intr z_smaller
    8.58 -        |> forall_intr (cterm_of thy z)
    8.59 -        |> (fn it => it COMP valthm)
    8.60 -        |> implies_intr lhs_acc 
    8.61 -        |> asm_simplify (HOL_basic_ss addsimps [f_iff])
    8.62 -        |> fold_rev (implies_intr o cprop_of) ags
    8.63 -        |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
    8.64 -    end
    8.65 -
    8.66 -
    8.67 -
    8.68 -fun mk_partial_induct_rule thy globals R complete_thm clauses =
    8.69 -    let
    8.70 -      val Globals {domT, x, z, a, P, D, ...} = globals
    8.71 -      val acc_R = mk_acc domT R
    8.72 -                  
    8.73 -      val x_D = assume (cterm_of thy (Trueprop (D $ x)))
    8.74 -      val a_D = cterm_of thy (Trueprop (D $ a))
    8.75 -                
    8.76 -      val D_subset = cterm_of thy (mk_forall x (implies $ Trueprop (D $ x) $ Trueprop (acc_R $ x)))
    8.77 -                     
    8.78 -      val D_dcl = (* "!!x z. [| x: D; (z,x):R |] ==> z:D" *)
    8.79 -                    mk_forall x
    8.80 -                    (mk_forall z (Logic.mk_implies (Trueprop (D $ x),
    8.81 -                                                    Logic.mk_implies (Trueprop (R $ z $ x),
    8.82 -                                                                      Trueprop (D $ z)))))
    8.83 -                    |> cterm_of thy
    8.84 -                    
    8.85 -                    
    8.86 -  (* Inductive Hypothesis: !!z. (z,x):R ==> P z *)
    8.87 -      val ihyp = all domT $ Abs ("z", domT, 
    8.88 -               implies $ Trueprop (R $ Bound 0 $ x)
    8.89 -             $ Trueprop (P $ Bound 0))
    8.90 -           |> cterm_of thy
    8.91 -
    8.92 -      val aihyp = assume ihyp
    8.93 -
    8.94 -  fun prove_case clause =
    8.95 -      let
    8.96 -    val ClauseInfo {cdata = ClauseContext {qs, cqs, ags, gs, lhs, rhs, case_hyp, ...}, RCs, 
    8.97 -                    qglr = (oqs, _, _, _), ...} = clause
    8.98 -                       
    8.99 -    val replace_x_ss = HOL_basic_ss addsimps [case_hyp]
   8.100 -    val lhs_D = simplify replace_x_ss x_D (* lhs : D *)
   8.101 -    val sih = full_simplify replace_x_ss aihyp
   8.102 -          
   8.103 -    fun mk_Prec (RCInfo {llRI, RIvs, CCas, rcarg, ...}) =
   8.104 -        sih |> forall_elim (cterm_of thy rcarg)
   8.105 -            |> implies_elim_swp llRI
   8.106 -            |> fold_rev (implies_intr o cprop_of) CCas
   8.107 -            |> fold_rev (forall_intr o cterm_of thy o Free) RIvs
   8.108 -        
   8.109 -    val P_recs = map mk_Prec RCs   (*  [P rec1, P rec2, ... ]  *)
   8.110 -                 
   8.111 -    val step = Trueprop (P $ lhs)
   8.112 -            |> fold_rev (curry Logic.mk_implies o prop_of) P_recs
   8.113 -            |> fold_rev (curry Logic.mk_implies) gs
   8.114 -            |> curry Logic.mk_implies (Trueprop (D $ lhs))
   8.115 -            |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
   8.116 -            |> cterm_of thy
   8.117 -         
   8.118 -    val P_lhs = assume step
   8.119 -           |> fold forall_elim cqs
   8.120 -           |> implies_elim_swp lhs_D 
   8.121 -           |> fold_rev implies_elim_swp ags
   8.122 -           |> fold implies_elim_swp P_recs
   8.123 -          
   8.124 -    val res = cterm_of thy (Trueprop (P $ x))
   8.125 -           |> Simplifier.rewrite replace_x_ss
   8.126 -           |> symmetric (* P lhs == P x *)
   8.127 -           |> (fn eql => equal_elim eql P_lhs) (* "P x" *)
   8.128 -           |> implies_intr (cprop_of case_hyp)
   8.129 -           |> fold_rev (implies_intr o cprop_of) ags
   8.130 -           |> fold_rev forall_intr cqs
   8.131 -      in
   8.132 -    (res, step)
   8.133 -      end
   8.134 -
   8.135 -  val (cases, steps) = split_list (map prove_case clauses)
   8.136 -
   8.137 -  val istep = complete_thm
   8.138 -                |> forall_elim_vars 0
   8.139 -                |> fold (curry op COMP) cases (*  P x  *)
   8.140 -                |> implies_intr ihyp
   8.141 -                |> implies_intr (cprop_of x_D)
   8.142 -                |> forall_intr (cterm_of thy x)
   8.143 -         
   8.144 -  val subset_induct_rule = 
   8.145 -      acc_subset_induct
   8.146 -        |> (curry op COMP) (assume D_subset)
   8.147 -        |> (curry op COMP) (assume D_dcl)
   8.148 -        |> (curry op COMP) (assume a_D)
   8.149 -        |> (curry op COMP) istep
   8.150 -        |> fold_rev implies_intr steps
   8.151 -        |> implies_intr a_D
   8.152 -        |> implies_intr D_dcl
   8.153 -        |> implies_intr D_subset
   8.154 -
   8.155 -  val subset_induct_all = fold_rev (forall_intr o cterm_of thy) [P, a, D] subset_induct_rule
   8.156 -
   8.157 -  val simple_induct_rule =
   8.158 -      subset_induct_rule
   8.159 -        |> forall_intr (cterm_of thy D)
   8.160 -        |> forall_elim (cterm_of thy acc_R)
   8.161 -        |> assume_tac 1 |> Seq.hd
   8.162 -        |> (curry op COMP) (acc_downward
   8.163 -                              |> (instantiate' [SOME (ctyp_of thy domT)]
   8.164 -                                               (map (SOME o cterm_of thy) [R, x, z]))
   8.165 -                              |> forall_intr (cterm_of thy z)
   8.166 -                              |> forall_intr (cterm_of thy x))
   8.167 -        |> forall_intr (cterm_of thy a)
   8.168 -        |> forall_intr (cterm_of thy P)
   8.169 -    in
   8.170 -      (subset_induct_all, simple_induct_rule)
   8.171 -    end
   8.172 -
   8.173 -
   8.174 -
   8.175 -(* Does this work with Guards??? *)
   8.176 -fun mk_domain_intro thy globals R R_cases clause =
   8.177 -    let
   8.178 -      val Globals {z, domT, ...} = globals
   8.179 -      val ClauseInfo {cdata = ClauseContext {qs, gs, lhs, rhs, cqs, ...}, 
   8.180 -                      qglr = (oqs, _, _, _), ...} = clause
   8.181 -      val goal = Trueprop (mk_acc domT R $ lhs)
   8.182 -                          |> fold_rev (curry Logic.mk_implies) gs
   8.183 -                          |> cterm_of thy
   8.184 -    in
   8.185 -      Goal.init goal 
   8.186 -      |> (SINGLE (resolve_tac [accI] 1)) |> the
   8.187 -      |> (SINGLE (eresolve_tac [forall_elim_vars 0 R_cases] 1))  |> the
   8.188 -      |> (SINGLE (CLASIMPSET auto_tac)) |> the
   8.189 -      |> Goal.conclude
   8.190 -      |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
   8.191 -    end
   8.192 -
   8.193 -
   8.194 -fun maybe_mk_domain_intro thy =
   8.195 -    if !FundefCommon.domintros then mk_domain_intro thy
   8.196 -    else K (K (K (K refl)))
   8.197 -
   8.198 -
   8.199 -fun mk_nest_term_case thy globals R' ihyp clause =
   8.200 -    let
   8.201 -      val Globals {x, z, ...} = globals
   8.202 -      val ClauseInfo {cdata = ClauseContext {qs,cqs,ags,lhs,rhs,case_hyp,...},tree,
   8.203 -                      qglr=(oqs, _, _, _), ...} = clause
   8.204 -          
   8.205 -      val ih_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ihyp
   8.206 -                    
   8.207 -      fun step (fixes, assumes) (_ $ arg) u (sub,(hyps,thms)) = 
   8.208 -          let
   8.209 -            val used = map (fn ((f,a),thm) => FundefCtxTree.export_thm thy (f, map prop_of a) thm) (u @ sub)
   8.210 -                       
   8.211 -            val hyp = Trueprop (R' $ arg $ lhs)
   8.212 -                      |> fold_rev (curry Logic.mk_implies o prop_of) used
   8.213 -                      |> FundefCtxTree.export_term (fixes, map prop_of assumes) 
   8.214 -                      |> fold_rev (curry Logic.mk_implies o prop_of) ags
   8.215 -                      |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
   8.216 -                      |> cterm_of thy
   8.217 -                      
   8.218 -            val thm = assume hyp
   8.219 -                      |> fold forall_elim cqs
   8.220 -                      |> fold implies_elim_swp ags
   8.221 -                      |> FundefCtxTree.import_thm thy (fixes, assumes) (*  "(arg, lhs) : R'"  *)
   8.222 -                      |> fold implies_elim_swp used
   8.223 -                      
   8.224 -            val acc = thm COMP ih_case
   8.225 -                      
   8.226 -            val z_eq_arg = cterm_of thy (Trueprop (HOLogic.mk_eq (z, arg)))
   8.227 -                           
   8.228 -            val arg_eq_z = (assume z_eq_arg) RS sym
   8.229 -                           
   8.230 -            val z_acc = simplify (HOL_basic_ss addsimps [arg_eq_z]) acc (* fragile, slow... *)
   8.231 -                        |> implies_intr (cprop_of case_hyp)
   8.232 -                        |> implies_intr z_eq_arg
   8.233 -
   8.234 -            val z_eq_arg = assume (cterm_of thy (Trueprop (mk_eq (z, arg))))
   8.235 -            val x_eq_lhs = assume (cterm_of thy (Trueprop (mk_eq (x, lhs))))
   8.236 -                           
   8.237 -            val ethm = (z_acc OF [z_eq_arg, x_eq_lhs])
   8.238 -                         |> FundefCtxTree.export_thm thy (fixes, 
   8.239 -                                                          prop_of z_eq_arg :: prop_of x_eq_lhs :: map prop_of (ags @ assumes))
   8.240 -                         |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
   8.241 -
   8.242 -            val sub' = sub @ [(([],[]), acc)]
   8.243 -          in
   8.244 -            (sub', (hyp :: hyps, ethm :: thms))
   8.245 -          end
   8.246 -        | step _ _ _ _ = raise Match
   8.247 -    in
   8.248 -      FundefCtxTree.traverse_tree step tree
   8.249 -    end
   8.250 -    
   8.251 -    
   8.252 -fun mk_nest_term_rule thy globals R R_cases clauses =
   8.253 -    let
   8.254 -      val Globals { domT, x, z, ... } = globals
   8.255 -      val acc_R = mk_acc domT R
   8.256 -                  
   8.257 -      val R' = Free ("R", fastype_of R)
   8.258 -               
   8.259 -      val Rrel = Free ("R", mk_relT (domT, domT))
   8.260 -      val inrel_R = Const ("FunDef.in_rel", mk_relT (domT, domT) --> fastype_of R) $ Rrel
   8.261 -                    
   8.262 -      val wfR' = cterm_of thy (Trueprop (Const ("FunDef.wfP", (domT --> domT --> boolT) --> boolT) $ R')) (* "wf R'" *)
   8.263 -                          
   8.264 -      (* Inductive Hypothesis: !!z. (z,x):R' ==> z : acc R *)
   8.265 -      val ihyp = all domT $ Abs ("z", domT, 
   8.266 -                                 implies $ Trueprop (R' $ Bound 0 $ x)
   8.267 -                                         $ Trueprop (acc_R $ Bound 0))
   8.268 -                     |> cterm_of thy
   8.269 -
   8.270 -      val ihyp_a = assume ihyp |> forall_elim_vars 0
   8.271 -                   
   8.272 -      val R_z_x = cterm_of thy (Trueprop (R $ z $ x)) 
   8.273 -                  
   8.274 -      val (hyps,cases) = fold (mk_nest_term_case thy globals R' ihyp_a) clauses ([],[])
   8.275 -    in
   8.276 -      R_cases
   8.277 -        |> forall_elim (cterm_of thy z)
   8.278 -        |> forall_elim (cterm_of thy x)
   8.279 -        |> forall_elim (cterm_of thy (acc_R $ z))
   8.280 -        |> curry op COMP (assume R_z_x)
   8.281 -        |> fold_rev (curry op COMP) cases
   8.282 -        |> implies_intr R_z_x
   8.283 -        |> forall_intr (cterm_of thy z)
   8.284 -        |> (fn it => it COMP accI)
   8.285 -        |> implies_intr ihyp
   8.286 -        |> forall_intr (cterm_of thy x)
   8.287 -        |> (fn it => Drule.compose_single(it,2,wf_induct_rule))
   8.288 -        |> curry op RS (assume wfR')
   8.289 -        |> fold implies_intr hyps
   8.290 -        |> implies_intr wfR'
   8.291 -        |> forall_intr (cterm_of thy R')
   8.292 -        |> forall_elim (cterm_of thy (inrel_R))
   8.293 -        |> curry op RS wf_in_rel
   8.294 -        |> full_simplify (HOL_basic_ss addsimps [in_rel_def])
   8.295 -        |> forall_intr (cterm_of thy Rrel)
   8.296 -    end
   8.297 -    
   8.298 -
   8.299 -
   8.300 -
   8.301 -fun mk_partial_rules thy data provedgoal =
   8.302 -    let
   8.303 -      val Prep {globals, G, f, R, clauses, values, R_cases, ex1_iff, ...} = data
   8.304 -                                                                            
   8.305 -      val provedgoal = PROFILE "Closing result" Goal.close_result provedgoal
   8.306 -                       
   8.307 -      val graph_is_function = PROFILE "Getting function theorem" (fn x => (x COMP conjunctionD1) |> forall_elim_vars 0) provedgoal
   8.308 -                              
   8.309 -      val complete_thm = PROFILE "Getting cases" (curry op COMP provedgoal) conjunctionD2
   8.310 -
   8.311 -      val f_iff = PROFILE "Making f_iff" (curry op RS graph_is_function) ex1_iff
   8.312 -                  
   8.313 -      val psimps = PROFILE "Proving simplification rules" (map2 (mk_psimp thy globals R f_iff graph_is_function)) clauses values
   8.314 -                    
   8.315 -      val (subset_pinduct, simple_pinduct) = PROFILE "Proving partial induction rule" 
   8.316 -                                             (mk_partial_induct_rule thy globals R complete_thm) clauses
   8.317 -                                             
   8.318 -      val total_intro = PROFILE "Proving nested termination rule" (mk_nest_term_rule thy globals R R_cases) clauses
   8.319 -                        
   8.320 -      val dom_intros = PROFILE "Proving domain introduction rules" (map (maybe_mk_domain_intro thy globals R R_cases)) clauses
   8.321 -    in 
   8.322 -      FundefResult {f=f, G=G, R=R, completeness=complete_thm, 
   8.323 -                    psimps=psimps, subset_pinduct=subset_pinduct, simple_pinduct=simple_pinduct, total_intro=total_intro,
   8.324 -                    dom_intros=dom_intros}
   8.325 -    end
   8.326 -    
   8.327 -    
   8.328 -end
   8.329 -
   8.330 -
     9.1 --- a/src/HOL/Tools/function_package/inductive_wrap.ML	Mon Jan 22 16:53:33 2007 +0100
     9.2 +++ b/src/HOL/Tools/function_package/inductive_wrap.ML	Mon Jan 22 17:29:43 2007 +0100
     9.3 @@ -11,7 +11,7 @@
     9.4  sig
     9.5    val inductive_def :  term list 
     9.6                         -> ((bstring * typ) * mixfix) * local_theory
     9.7 -                       -> thm list * (term * thm * local_theory)
     9.8 +                       -> thm list * (term * thm * thm * local_theory)
     9.9  end
    9.10  
    9.11  structure FundefInductiveWrap =
    9.12 @@ -40,7 +40,7 @@
    9.13      let
    9.14        val qdefs = map dest_all_all defs
    9.15                    
    9.16 -      val ({intrs = intrs_gen, elims = [elim_gen], preds = [ Rdef ], ...}, lthy) =
    9.17 +      val ({intrs = intrs_gen, elims = [elim_gen], preds = [ Rdef ], induct, ...}, lthy) =
    9.18            InductivePackage.add_inductive_i true (*verbose*)
    9.19                                             "" (* no altname *)
    9.20                                             false (* no coind *)
    9.21 @@ -70,7 +70,7 @@
    9.22                         |> Term.strip_comb |> snd |> hd (* Trueprop *)
    9.23                         |> Term.strip_comb |> fst
    9.24      in
    9.25 -      (intrs, (Rdef_real, elim, lthy))
    9.26 +      (intrs, (Rdef_real, elim, induct, lthy))
    9.27      end
    9.28      
    9.29  end
    10.1 --- a/src/HOL/Tools/function_package/mutual.ML	Mon Jan 22 16:53:33 2007 +0100
    10.2 +++ b/src/HOL/Tools/function_package/mutual.ML	Mon Jan 22 17:29:43 2007 +0100
    10.3 @@ -9,17 +9,16 @@
    10.4  signature FUNDEF_MUTUAL =
    10.5  sig
    10.6  
    10.7 -  val prepare_fundef_mutual : ((string * typ) * mixfix) list
    10.8 +  val prepare_fundef_mutual : FundefCommon.fundef_config
    10.9 +                              -> string (* defname *)
   10.10 +                              -> ((string * typ) * mixfix) list
   10.11                                -> term list
   10.12                                -> string (* default, unparsed term *)
   10.13                                -> local_theory
   10.14 -                              -> ((FundefCommon.mutual_info * string * FundefCommon.prep_result) * local_theory)
   10.15 -
   10.16 -
   10.17 -  val mk_partial_rules_mutual : Proof.context -> FundefCommon.mutual_info -> FundefCommon.prep_result -> thm ->
   10.18 -                                FundefCommon.fundef_mresult
   10.19 -
   10.20 -  val sort_by_function : FundefCommon.mutual_info -> string list -> 'a list -> 'a list list
   10.21 +                              -> ((thm (* goalstate *)
   10.22 +                                   * (thm -> FundefCommon.fundef_result) (* proof continuation *)
   10.23 +                                   * (thm list -> thm list list)         (* sorting continuation *)
   10.24 +                                  ) * local_theory)
   10.25  
   10.26  end
   10.27  
   10.28 @@ -34,6 +33,45 @@
   10.29  val sum_case_rules = thms "Datatype.sum.cases"
   10.30  val split_apply = thm "Product_Type.split"
   10.31  
   10.32 +type qgar = string * (string * typ) list * term list * term list * term
   10.33 +
   10.34 +fun name_of_fqgar (f, _, _, _, _) = f
   10.35 +
   10.36 +datatype mutual_part =
   10.37 +  MutualPart of 
   10.38 +   {
   10.39 +    fvar : string * typ,
   10.40 +    cargTs: typ list,
   10.41 +    pthA: SumTools.sum_path,
   10.42 +    pthR: SumTools.sum_path,
   10.43 +    f_def: term,
   10.44 +
   10.45 +    f: term option,
   10.46 +    f_defthm : thm option
   10.47 +   }
   10.48 +   
   10.49 +
   10.50 +datatype mutual_info =
   10.51 +  Mutual of 
   10.52 +   { 
   10.53 +    fsum_var : string * typ,
   10.54 +
   10.55 +    ST: typ,
   10.56 +    RST: typ,
   10.57 +    streeA: SumTools.sum_tree,
   10.58 +    streeR: SumTools.sum_tree,
   10.59 +
   10.60 +    parts: mutual_part list,
   10.61 +    fqgars: qgar list,
   10.62 +    qglrs: ((string * typ) list * term list * term * term) list,
   10.63 +
   10.64 +    fsum : term option
   10.65 +   }
   10.66 +
   10.67 +
   10.68 +
   10.69 +
   10.70 +
   10.71  
   10.72  
   10.73  fun mutual_induct_Pnames n =
   10.74 @@ -100,7 +138,7 @@
   10.75      end;
   10.76  
   10.77  
   10.78 -fun analyze_eqs ctxt fs eqs =
   10.79 +fun analyze_eqs ctxt defname fs eqs =
   10.80      let
   10.81          val fnames = map fst fs
   10.82          val (fqgars, arities) = fold_map (split_def ctxt fnames) eqs Symtab.empty
   10.83 @@ -119,10 +157,9 @@
   10.84          val (RST,streeR, pthsR) = SumTools.mk_tree_distinct resultTs
   10.85          val (ST, streeA, pthsA) = SumTools.mk_tree argTs
   10.86  
   10.87 -        val def_name = foldr1 (fn (a,b) => a ^ "_" ^ b) (map Sign.base_name fnames)
   10.88          val fsum_type = ST --> RST
   10.89  
   10.90 -        val ([fsum_var_name], _) = Variable.add_fixes [ def_name ^ "_sum" ] ctxt
   10.91 +        val ([fsum_var_name], _) = Variable.add_fixes [ defname ^ "_sum" ] ctxt
   10.92          val fsum_var = (fsum_var_name, fsum_type)
   10.93  
   10.94          fun define (fvar as (n, T)) caTs pthA pthR =
   10.95 @@ -150,7 +187,7 @@
   10.96  
   10.97          val qglrs = map convert_eqs fqgars
   10.98      in
   10.99 -        Mutual {defname=def_name,fsum_var=fsum_var, ST=ST, RST=RST, streeA=streeA, streeR=streeR,
  10.100 +        Mutual {fsum_var=fsum_var, ST=ST, RST=RST, streeA=streeA, streeR=streeR,
  10.101                  parts=parts, fqgars=fqgars, qglrs=qglrs, fsum=NONE}
  10.102      end
  10.103  
  10.104 @@ -171,29 +208,15 @@
  10.105               lthy')
  10.106            end
  10.107            
  10.108 -      val Mutual { defname, fsum_var, ST, RST, streeA, streeR, parts, fqgars, qglrs, ... } = mutual
  10.109 +      val Mutual { fsum_var, ST, RST, streeA, streeR, parts, fqgars, qglrs, ... } = mutual
  10.110        val (parts', lthy') = fold_map def (parts ~~ fixes) lthy
  10.111      in
  10.112 -      (Mutual { defname=defname, fsum_var=fsum_var, ST=ST, RST=RST, streeA=streeA, streeR=streeR, parts=parts',
  10.113 +      (Mutual { fsum_var=fsum_var, ST=ST, RST=RST, streeA=streeA, streeR=streeR, parts=parts',
  10.114                  fqgars=fqgars, qglrs=qglrs, fsum=SOME fsum },
  10.115         lthy')
  10.116      end
  10.117  
  10.118  
  10.119 -fun prepare_fundef_mutual fixes eqss default lthy =
  10.120 -    let
  10.121 -      val mutual = analyze_eqs lthy (map fst fixes) eqss
  10.122 -      val Mutual {defname, fsum_var=(n, T), qglrs, ...} = mutual
  10.123 -          
  10.124 -      val (prep_result, fsum, lthy') =
  10.125 -          FundefPrep.prepare_fundef defname (n, T, NoSyn) qglrs default lthy
  10.126 -          
  10.127 -      val (mutual', lthy'') = define_projections fixes mutual fsum lthy'
  10.128 -    in
  10.129 -      ((mutual', defname, prep_result), lthy'')
  10.130 -    end
  10.131 -      
  10.132 -
  10.133  (* Beta-reduce both sides of a meta-equality *)
  10.134  fun beta_norm_eq thm =
  10.135      let
  10.136 @@ -315,7 +338,7 @@
  10.137  
  10.138  
  10.139  
  10.140 -fun mk_partial_rules_mutual lthy (m as Mutual {RST, parts, streeR, fqgars, ...}) data prep_result =
  10.141 +fun mk_partial_rules_mutual lthy inner_cont (m as Mutual {RST, parts, streeR, fqgars, ...}) proof =
  10.142      let
  10.143        val thy = ProofContext.theory_of lthy
  10.144                                         
  10.145 @@ -323,8 +346,9 @@
  10.146        val expand = Assumption.export false lthy (LocalTheory.target_of lthy)
  10.147        val expand_term = Drule.term_rule thy expand
  10.148                          
  10.149 -      val result = FundefProof.mk_partial_rules thy data prep_result
  10.150 -      val FundefResult {f, G, R, completeness, psimps, subset_pinduct,simple_pinduct,total_intro,dom_intros} = result
  10.151 +      val result = inner_cont proof
  10.152 +      val FundefResult {f, G, R, cases, psimps, trsimps, subset_pinducts=[subset_pinduct],simple_pinducts=[simple_pinduct],
  10.153 +                        termination,domintros} = result
  10.154                                                                                                                 
  10.155        val all_f_defs = map (fn MutualPart {f_defthm = SOME f_def, cargTs, ...} =>
  10.156                                 mk_applied_form lthy cargTs (symmetric (Thm.freezeT f_def)))
  10.157 @@ -333,18 +357,19 @@
  10.158        fun mk_mpsimp fqgar sum_psimp =
  10.159            in_context lthy fqgar (recover_mutual_psimp thy RST streeR all_f_defs parts) sum_psimp
  10.160            
  10.161 -      val mpsimps = PROFILE "making mpsimps" (map2 mk_mpsimp fqgars) psimps
  10.162 -      val minducts = PROFILE "making mpinduct" (mutual_induct_rules thy simple_pinduct all_f_defs) m
  10.163 -      val termination = PROFILE "making mtermination" (full_simplify (HOL_basic_ss addsimps all_f_defs)) total_intro
  10.164 +      val mpsimps = map2 mk_mpsimp fqgars psimps
  10.165 +      val mtrsimps = map_option (map2 mk_mpsimp fqgars) trsimps
  10.166 +      val minducts = mutual_induct_rules thy simple_pinduct all_f_defs m
  10.167 +      val mtermination = full_simplify (HOL_basic_ss addsimps all_f_defs) termination
  10.168      in
  10.169 -      FundefMResult { f=expand_term f, G=expand_term G, R=expand_term R,
  10.170 -                      psimps=map expand mpsimps, subset_pinducts=[expand subset_pinduct], simple_pinducts=map expand minducts,
  10.171 -                      cases=expand completeness, termination=expand termination,
  10.172 -                      domintros=map expand dom_intros }
  10.173 +      FundefResult { f=expand_term f, G=expand_term G, R=expand_term R,
  10.174 +                     psimps=map expand mpsimps, subset_pinducts=[expand subset_pinduct], simple_pinducts=map expand minducts,
  10.175 +                     cases=expand cases, termination=expand mtermination,
  10.176 +                     domintros=map_option (map expand) domintros,
  10.177 +                     trsimps=map_option (map expand) trsimps}
  10.178      end
  10.179        
  10.180 -      
  10.181 -      
  10.182 +
  10.183  (* puts an object in the "right bucket" *)
  10.184  fun store_grouped P x [] = []
  10.185    | store_grouped P x ((l, xs)::bs) =
  10.186 @@ -356,5 +381,23 @@
  10.187               (map (rpair []) names)                (* in the empty buckets labeled with names *)
  10.188               
  10.189               |> map (snd #> map snd)                     (* and remove the labels afterwards *)
  10.190 +
  10.191 +
  10.192 +fun prepare_fundef_mutual config defname fixes eqss default lthy =
  10.193 +    let
  10.194 +      val mutual = analyze_eqs lthy defname (map fst fixes) eqss
  10.195 +      val Mutual {fsum_var=(n, T), qglrs, ...} = mutual
  10.196 +          
  10.197 +      val ((fsum, goalstate, cont), lthy') =
  10.198 +          FundefCore.prepare_fundef config defname (n, T, NoSyn) qglrs default lthy
  10.199 +          
  10.200 +      val (mutual', lthy'') = define_projections fixes mutual fsum lthy'
  10.201 +
  10.202 +      val mutual_cont = mk_partial_rules_mutual lthy'' cont mutual'
  10.203 +      val sort_cont = sort_by_function mutual' (map (fst o fst) fixes)
  10.204 +    in
  10.205 +      ((goalstate, mutual_cont, sort_cont), lthy'')
  10.206 +    end
  10.207 +
  10.208      
  10.209  end
    11.1 --- a/src/HOL/Tools/function_package/termination.ML	Mon Jan 22 16:53:33 2007 +0100
    11.2 +++ b/src/HOL/Tools/function_package/termination.ML	Mon Jan 22 17:29:43 2007 +0100
    11.3 @@ -9,7 +9,7 @@
    11.4  
    11.5  signature FUNDEF_TERMINATION =
    11.6  sig
    11.7 -  val mk_total_termination_goal : term -> term -> term
    11.8 +  val mk_total_termination_goal : term -> term
    11.9  (*  val mk_partial_termination_goal : theory -> FundefCommon.result_with_names -> string -> term * term*)
   11.10  end
   11.11  
   11.12 @@ -21,9 +21,9 @@
   11.13  open FundefCommon
   11.14  open FundefAbbrev
   11.15       
   11.16 -fun mk_total_termination_goal f R =
   11.17 +fun mk_total_termination_goal R =
   11.18      let
   11.19 -      val domT = domain_type (fastype_of f)
   11.20 +      val domT = domain_type (fastype_of R)
   11.21        val x = Free ("x", domT)
   11.22      in
   11.23        mk_forall x (Trueprop (mk_acc domT R $ x))
    12.1 --- a/src/HOL/ex/Fundefs.thy	Mon Jan 22 16:53:33 2007 +0100
    12.2 +++ b/src/HOL/ex/Fundefs.thy	Mon Jan 22 17:29:43 2007 +0100
    12.3 @@ -24,7 +24,6 @@
    12.4  text {* There is also a cases rule to distinguish cases along the definition *}
    12.5  thm fib.cases
    12.6  
    12.7 -thm fib.domintros
    12.8  
    12.9  text {* total simp and induction rules: *}
   12.10  thm fib.simps
   12.11 @@ -172,8 +171,6 @@
   12.12  
   12.13  thm evn_od.pinduct
   12.14  thm evn_od.termination
   12.15 -thm evn_od.domintros
   12.16 -
   12.17  
   12.18  
   12.19