1. Function package accepts a parameter (default "some_term"), which specifies the functions
behaviour outside its domain.
2. Bugfix: An exception occured when a function in a mutual definition
was declared but no equation was given.

--- a/src/HOL/FunDef.thy	Thu Sep 21 03:17:51 2006 +0200
+++ b/src/HOL/FunDef.thy	Thu Sep 21 12:22:05 2006 +0200
@@ -41,25 +41,45 @@
 
 
 lemma fundef_ex1_existence:
-assumes f_def: "f \<equiv> \<lambda>x. THE_default d (\<lambda>y. (x,y)\<in>G)"
+assumes f_def: "f \<equiv> \<lambda>x. THE_default (d x) (\<lambda>y. (x,y)\<in>G)"
 assumes ex1: "\<exists>!y. (x,y)\<in>G"
 shows "(x, f x)\<in>G"
   by (simp only:f_def, rule THE_defaultI', rule ex1)
 
 lemma fundef_ex1_uniqueness:
-assumes f_def: "f \<equiv> \<lambda>x. THE_default d (\<lambda>y. (x,y)\<in>G)"
+assumes f_def: "f \<equiv> \<lambda>x. THE_default (d x) (\<lambda>y. (x,y)\<in>G)"
 assumes ex1: "\<exists>!y. (x,y)\<in>G"
 assumes elm: "(x, h x)\<in>G"
 shows "h x = f x"
   by (simp only:f_def, rule THE_default1_equality[symmetric], rule ex1, rule elm)
 
 lemma fundef_ex1_iff:
-assumes f_def: "f \<equiv> \<lambda>x. THE_default d (\<lambda>y. (x,y)\<in>G)"
+assumes f_def: "f \<equiv> \<lambda>x. THE_default (d x) (\<lambda>y. (x,y)\<in>G)"
 assumes ex1: "\<exists>!y. (x,y)\<in>G"
 shows "((x, y)\<in>G) = (f x = y)"
   apply (auto simp:ex1 f_def THE_default1_equality)
   by (rule THE_defaultI', rule ex1)
 
+lemma fundef_default_value:
+assumes f_def: "f \<equiv> \<lambda>x. THE_default (d x) (\<lambda>y. (x,y)\<in>G)"
+assumes graph: "\<And>x y. (x,y) \<in> G \<Longrightarrow> x \<in> D"
+assumes "x \<notin> D"
+shows "f x = d x"
+proof -
+  have "\<not>(\<exists>y. (x, y) \<in> G)"
+  proof
+    assume "(\<exists>y. (x, y) \<in> G)"
+    with graph and `x\<notin>D` show False by blast
+  qed
+  hence "\<not>(\<exists>!y. (x, y) \<in> G)" by blast
+  
+  thus ?thesis
+    unfolding f_def
+    by (rule THE_default_none)
+qed
+
+
+
 
 subsection {* Projections *}
 consts

--- a/src/HOL/Tools/function_package/fundef_common.ML	Thu Sep 21 03:17:51 2006 +0200
+++ b/src/HOL/Tools/function_package/fundef_common.ML	Thu Sep 21 12:22:05 2006 +0200
@@ -214,6 +214,54 @@
 val map_fundef_congs = FundefCongs.map 
 val get_fundef_congs = FundefCongs.get
 
+
+(* Configuration management *)
+datatype fundef_opt 
+  = Sequential
+  | Default of string
+  | Preprocessor of string
+
+datatype fundef_config
+  = FundefConfig of
+   {
+    sequential: bool,
+    default: string,
+    preprocessor: string option
+   }
+
+
+val default_config = FundefConfig { sequential=false, default="%x. arbitrary", preprocessor=NONE }
+val fun_config = FundefConfig { sequential=true, default="%x. arbitrary", preprocessor=NONE }
+
+fun apply_opt Sequential (FundefConfig {sequential, default, preprocessor}) = 
+    FundefConfig {sequential=true, default=default, preprocessor=preprocessor }
+  | apply_opt (Default d) (FundefConfig {sequential, default, preprocessor}) = 
+    FundefConfig {sequential=sequential, default=d, preprocessor=preprocessor }
+  | apply_opt (Preprocessor p) (FundefConfig {sequential, default, preprocessor}) = 
+    FundefConfig {sequential=sequential, default=default, preprocessor=SOME p }
+
+    
+local structure P = OuterParse and K = OuterKeyword in
+
+val opt_sequential = Scan.optional ((P.$$$ "(" |-- P.$$$ "sequential" --| P.$$$ ")") >> K true) false
+
+val option_parser = (P.$$$ "sequential" >> K Sequential)
+               || ((P.reserved "default" |-- P.term) >> Default)
+
+val config_parser = (Scan.optional (P.$$$ "(" |-- P.list1 option_parser --| P.$$$ ")") [])
+                      >> (fn opts => fold apply_opt opts default_config)
+end
+
+
+
+
+
+
+
+
+
+
+
 end
 
 

--- a/src/HOL/Tools/function_package/fundef_datatype.ML	Thu Sep 21 03:17:51 2006 +0200
+++ b/src/HOL/Tools/function_package/fundef_datatype.ML	Thu Sep 21 12:22:05 2006 +0200
@@ -192,7 +192,7 @@
   OuterSyntax.command "fun" "define general recursive functions (short version)" K.thy_decl
   ((P.opt_locale_target -- P.fixes --| P.$$$ "where" -- statements_ow)
      >> (fn ((target, fixes), statements) =>
-            Toplevel.print o Toplevel.local_theory NONE (FundefPackage.add_fundef fixes statements true 
+            Toplevel.print o Toplevel.local_theory NONE (FundefPackage.add_fundef fixes statements FundefCommon.fun_config 
                                                                                   #> by_pat_completeness_simp)));
 
 val _ = OuterSyntax.add_parsers [funP];

--- a/src/HOL/Tools/function_package/fundef_package.ML	Thu Sep 21 03:17:51 2006 +0200
+++ b/src/HOL/Tools/function_package/fundef_package.ML	Thu Sep 21 12:22:05 2006 +0200
@@ -11,7 +11,7 @@
 sig
     val add_fundef :  (string * string option * mixfix) list 
                       -> ((bstring * Attrib.src list) * string list) list list
-                      -> bool 
+                      -> FundefCommon.fundef_config 
                       -> local_theory 
                       -> Proof.state
 
@@ -34,6 +34,7 @@
 
 open FundefCommon
 
+(*fn (ctxt,s) => Variable.importT_terms (fst (ProofContext.read_termTs ctxt (K false) (K NONE) (K NONE) [] [s])) ctxt;*)
 
 fun burrow_snd f ps = (* ('a list -> 'b list) -> ('c * 'a) list -> ('c * 'b) list *)
     let val (xs, ys) = split_list ps
@@ -101,14 +102,16 @@
     end
 
 
-fun gen_add_fundef prep_spec fixspec eqnss_flags preprocess lthy =
+fun gen_add_fundef prep_spec fixspec eqnss_flags config lthy =
     let
-      val ((fixes, spec), ctxt') = prep_with_flags prep_spec fixspec eqnss_flags preprocess lthy
+      val FundefConfig {sequential, default, ...} = config
+
+      val ((fixes, spec), ctxt') = prep_with_flags prep_spec fixspec eqnss_flags sequential lthy
       val t_eqns = spec
                      |> flat |> map snd |> flat (* flatten external structure *)
 
       val ((mutual_info, name, prep_result as Prep {goal, goalI, ...}), lthy) = 
-          FundefMutual.prepare_fundef_mutual fixes t_eqns lthy
+          FundefMutual.prepare_fundef_mutual fixes t_eqns default lthy
 
       val afterqed = fundef_afterqed fixes spec mutual_info name prep_result
     in
@@ -198,9 +201,9 @@
 
 val functionP =
   OuterSyntax.command "function" "define general recursive functions" K.thy_goal
-  ((opt_sequential -- P.opt_locale_target -- P.fixes --| P.$$$ "where" -- statements_ow)
-     >> (fn (((sequential, target), fixes), statements) =>
-            Toplevel.print o local_theory_to_proof (add_fundef fixes statements sequential)));
+  ((config_parser -- P.opt_locale_target -- P.fixes --| P.$$$ "where" -- statements_ow)
+     >> (fn (((config, target), fixes), statements) =>
+            Toplevel.print o local_theory_to_proof (add_fundef fixes statements config)));
 
 
 val terminationP =
@@ -211,7 +214,7 @@
 
 val _ = OuterSyntax.add_parsers [functionP];
 val _ = OuterSyntax.add_parsers [terminationP];
-val _ = OuterSyntax.add_keywords ["sequential", "otherwise"]; (* currently unused *)
+val _ = OuterSyntax.add_keywords ["sequential", "otherwise"];
 
 end;
 

--- a/src/HOL/Tools/function_package/fundef_prep.ML	Thu Sep 21 03:17:51 2006 +0200
+++ b/src/HOL/Tools/function_package/fundef_prep.ML	Thu Sep 21 12:22:05 2006 +0200
@@ -12,6 +12,7 @@
     val prepare_fundef : string (* defname *)
                          -> (string * typ * mixfix) (* defined symbol *)
                          -> ((string * typ) list * term list * term * term) list (* specification *)
+                         -> string (* default_value, not parsed yet *)
                          -> local_theory
                          -> FundefCommon.prep_result * term * local_theory
 
@@ -419,10 +420,10 @@
 
 
 
-fun define_function fdefname (fname, mixfix) domT ranT G lthy =
+fun define_function fdefname (fname, mixfix) domT ranT G default lthy =
     let
       val f_def = 
-          Abs ("x", domT, Const ("FunDef.THE_default", ranT --> (ranT --> boolT) --> ranT) $ Const ("arbitrary", ranT) $
+          Abs ("x", domT, Const ("FunDef.THE_default", ranT --> (ranT --> boolT) --> ranT) $ (default $ Bound 0) $
                                 Abs ("y", ranT, mk_relmemT domT ranT (Bound 1, Bound 0) G))
           
       val ((f, (_, f_defthm)), lthy) = LocalTheory.def ((fname ^ "C", mixfix), ((fdefname, []), f_def)) lthy
@@ -486,11 +487,13 @@
 
 
 
-fun prepare_fundef defname (fname, fT, mixfix) abstract_qglrs lthy =
+fun prepare_fundef defname (fname, fT, mixfix) abstract_qglrs default_str lthy =
     let
       val fvar = Free (fname, fT)
       val domT = domain_type fT
       val ranT = range_type fT
+                            
+      val [default] = fst (Variable.importT_terms (fst (ProofContext.read_termTs lthy (K false) (K NONE) (K NONE) [] [(default_str, fT)])) lthy) (* FIXME *)
 
       val congs = get_fundef_congs (Context.Proof lthy)
       val (globals, ctxt') = fix_globals domT ranT fvar lthy
@@ -510,7 +513,7 @@
       val RCss = map find_calls trees
 
       val ((G, GIntro_thms, G_elim), lthy) = define_graph (defname ^ "_graph") fvar domT ranT clauses RCss lthy
-      val ((f, f_defthm), lthy) = define_function (defname ^ "_sum_def") (fname, mixfix) domT ranT G lthy
+      val ((f, f_defthm), lthy) = define_function (defname ^ "_sum_def") (fname, mixfix) domT ranT G default lthy
 
       val RCss = map (map (inst_RC (ProofContext.theory_of lthy) fvar f)) RCss
       val trees = map (FundefCtxTree.inst_tree (ProofContext.theory_of lthy) fvar f) trees

--- a/src/HOL/Tools/function_package/mutual.ML	Thu Sep 21 03:17:51 2006 +0200
+++ b/src/HOL/Tools/function_package/mutual.ML	Thu Sep 21 12:22:05 2006 +0200
@@ -12,6 +12,7 @@
   
   val prepare_fundef_mutual : ((string * typ) * mixfix) list 
                               -> term list 
+                              -> string (* default, unparsed term *)
                               -> local_theory 
                               -> ((FundefCommon.mutual_info * string * FundefCommon.prep_result) * local_theory)
 
@@ -42,7 +43,7 @@
 
 fun check_head fs t =
     if (case t of 
-          (Free (n, _)) => n mem fs
+          (Free (n, _)) => n mem (map fst fs)
         | _ => false)
     then dest_Free t
     else raise ERROR "Head symbol of every left hand side must be the new function." (* FIXME: Output the equation here *)
@@ -54,7 +55,7 @@
 
 
 (* Builds a curried clause description in abstracted form *)
-fun split_def fnames geq =
+fun split_def fs geq arities =
     let
       val (qs, imp) = open_all_all geq
 
@@ -63,7 +64,7 @@
 
       val (f_args, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop eq)
       val (fc, args) = strip_comb f_args
-      val f as (fname, _) = check_head fnames fc
+      val f as (fname, _) = check_head fs fc
 
       fun add_bvs t is = add_loose_bnos (t, 0, is)
       val rhs_only = (add_bvs rhs [] \\ fold add_bvs args [])
@@ -71,8 +72,16 @@
                         |> map (fst o nth (rev qs))
       val _ = if null rhs_only then () 
 	      else raise ERROR "Variables occur on right hand side only." (* FIXME: Output vars *)
+
+      val k = length args
+
+      val arities' = case Symtab.lookup arities fname of
+                   NONE => Symtab.update (fname, k) arities
+                 | SOME i => if (i <> k) 
+                             then raise ERROR ("Function " ^ fname ^ " has different numbers of arguments in different equations")
+                             else arities
     in
-	((f, length args), (fname, qs, gs, args, rhs))
+	((fname, qs, gs, args, rhs), arities')
     end
 
 fun get_part fname =
@@ -89,45 +98,38 @@
     end;
 
 
-fun analyze_eqs ctxt fnames eqs =
+fun analyze_eqs ctxt fs eqs =
     let
-      (* FIXME: Add check for number of arguments
-	fun all_equal ((x as ((n:string,T), k:int))::xs) = if forall (fn ((n',_),k') => n = n' andalso k = k') xs then x
-							   else raise ERROR ("All equations in a block must describe the same "
-									     ^ "function and have the same number of arguments.")
-       *)
-								      
-        val (consts, fqgars) = split_list (map (split_def fnames) eqs)
+        val fnames = map fst fs 
+        val (fqgars, arities) = fold_map (split_def fs) eqs Symtab.empty
 
-        val different_consts = distinct (eq_fst (eq_fst eq_str)) consts
-	val cnames = map (fst o fst) different_consts
-
-	val check_rcs = exists_subterm (fn Free (n, _) => if n mem cnames 
+	val check_rcs = exists_subterm (fn Free (n, _) => if n mem fnames
 						          then raise ERROR "Recursive Calls not allowed in premises." else false
                                          | _ => false)
                         
 	val _ = forall (fn (_, _, gs, _, _) => forall check_rcs gs) fqgars
 
-	fun curried_types ((_,T), k) =
+	fun curried_types (fname, fT) =
 	    let
-		val (caTs, uaTs) = chop k (binder_types T)
+              val k = the_default 1 (Symtab.lookup arities fname)
+	      val (caTs, uaTs) = chop k (binder_types fT)
 	    in 
-		(caTs, uaTs ---> body_type T)
+		(caTs, uaTs ---> body_type fT)
 	    end
 
-	val (caTss, resultTs) = split_list (map curried_types different_consts)
+	val (caTss, resultTs) = split_list (map curried_types fs)
 	val argTs = map (foldr1 HOLogic.mk_prodT) caTss
 
 	val (RST,streeR, pthsR) = SumTools.mk_tree_distinct resultTs
 	val (ST, streeA, pthsA) = SumTools.mk_tree argTs
 
-	val def_name = foldr1 (fn (a,b) => a ^ "_" ^ b) (map Sign.base_name cnames)
+	val def_name = foldr1 (fn (a,b) => a ^ "_" ^ b) (map Sign.base_name fnames)
 	val fsum_type = ST --> RST
 
         val ([fsum_var_name], _) = Variable.add_fixes [ def_name ^ "_sum" ] ctxt
         val fsum_var = (fsum_var_name, fsum_type)
 
-	fun define (fvar as (n, T), _) caTs pthA pthR = 
+	fun define (fvar as (n, T)) caTs pthA pthR = 
 	    let 
 		val vars = map_index (fn (i,T) => Free ("x" ^ string_of_int i, T)) caTs (* FIXME: Bind xs properly *)
 
@@ -139,7 +141,7 @@
 		(MutualPart {fvar=fvar,cargTs=caTs,pthA=pthA,pthR=pthR,f_def=def,f=NONE,f_defthm=NONE}, rew)
 	    end
 
-	val (parts, rews) = split_list (map4 define different_consts caTss pthsA pthsR)
+	val (parts, rews) = split_list (map4 define fs caTss pthsA pthsR)
 
         fun convert_eqs (f, qs, gs, args, rhs) =
             let
@@ -181,17 +183,13 @@
     end
 
 
-
-  
-
-
-fun prepare_fundef_mutual fixes eqss lthy =
+fun prepare_fundef_mutual fixes eqss default lthy =
     let 
-	val mutual = analyze_eqs lthy (map (fst o fst) fixes) eqss
+	val mutual = analyze_eqs lthy (map fst fixes) eqss
 	val Mutual {defname, fsum_var=(n, T), qglrs, ...} = mutual
 
         val (prep_result, fsum, lthy') =
-            FundefPrep.prepare_fundef defname (n, T, NoSyn) qglrs lthy
+            FundefPrep.prepare_fundef defname (n, T, NoSyn) qglrs default lthy
 
         val (mutual', lthy'') = define_projections fixes mutual fsum lthy'
     in

--- a/src/HOL/Tools/function_package/pattern_split.ML	Thu Sep 21 03:17:51 2006 +0200
+++ b/src/HOL/Tools/function_package/pattern_split.ML	Thu Sep 21 12:22:05 2006 +0200
@@ -94,9 +94,6 @@
       val (vs, feq1 as (_ $ (_ $ lhs1 $ _))) = dest_all_all eq1
       val (_,  _ $ (_ $ lhs2 $ _)) = dest_all_all eq2
 
-      val _ = print (cterm_of thy eq1)
-      val _ = print (cterm_of thy eq2)
-
       val substs = pattern_subtract_subst ctx vs lhs1 lhs2
 
       fun instantiate (vs', sigma) =
@@ -105,10 +102,8 @@
           in
             fold_rev mk_forall (map Free (frees_in_term ctx t) inter vs') t
           end
-
-      fun prtrm t = let val _ = print (map (cterm_of thy) t) in t end
     in
-      prtrm (map instantiate substs)
+      map instantiate substs
     end