HOL/Tools/function_package: Added support for mutual recursive definitions.

--- a/src/HOL/Datatype.thy	Mon Jun 05 14:22:58 2006 +0200
+++ b/src/HOL/Datatype.thy	Mon Jun 05 14:26:07 2006 +0200
@@ -6,8 +6,7 @@
 header {* Datatypes *}
 
 theory Datatype
-imports Datatype_Universe FunDef
-uses ("Tools/function_package/fundef_datatype.ML")
+imports Datatype_Universe
 begin
 
 subsection {* Representing primitive types *}
@@ -316,8 +315,6 @@
     haskell (target_atom "Just")
 
 
-use "Tools/function_package/fundef_datatype.ML"
-setup FundefDatatype.setup
 
 
 end

--- a/src/HOL/FunDef.thy	Mon Jun 05 14:22:58 2006 +0200
+++ b/src/HOL/FunDef.thy	Mon Jun 05 14:26:07 2006 +0200
@@ -1,13 +1,17 @@
 theory FunDef
-imports Accessible_Part
+imports Accessible_Part Datatype Recdef
 uses 
+("Tools/function_package/sum_tools.ML")
 ("Tools/function_package/fundef_common.ML")
 ("Tools/function_package/fundef_lib.ML")
 ("Tools/function_package/context_tree.ML")
 ("Tools/function_package/fundef_prep.ML")
 ("Tools/function_package/fundef_proof.ML")
 ("Tools/function_package/termination.ML")
+("Tools/function_package/mutual.ML")
 ("Tools/function_package/fundef_package.ML")
+("Tools/function_package/fundef_datatype.ML")
+("Tools/function_package/auto_term.ML")
 begin
 
 lemma fundef_ex1_existence:
@@ -34,16 +38,52 @@
   by simp
 
 
+subsection {* Projections *}
+consts
+  lpg::"(('a + 'b) * 'a) set"
+  rpg::"(('a + 'b) * 'b) set"
+
+inductive lpg
+intros
+  "(Inl x, x) : lpg"
+inductive rpg
+intros
+  "(Inr y, y) : rpg"
+definition
+  "lproj x = (THE y. (x,y) : lpg)"
+  "rproj x = (THE y. (x,y) : rpg)"
+
+lemma lproj_inl:
+  "lproj (Inl x) = x"
+  by (auto simp:lproj_def intro: the_equality lpg.intros elim: lpg.cases)
+lemma rproj_inr:
+  "rproj (Inr x) = x"
+  by (auto simp:rproj_def intro: the_equality rpg.intros elim: rpg.cases)
+
+
+
+
+use "Tools/function_package/sum_tools.ML"
 use "Tools/function_package/fundef_common.ML"
 use "Tools/function_package/fundef_lib.ML"
 use "Tools/function_package/context_tree.ML"
 use "Tools/function_package/fundef_prep.ML"
 use "Tools/function_package/fundef_proof.ML"
 use "Tools/function_package/termination.ML"
+use "Tools/function_package/mutual.ML"
 use "Tools/function_package/fundef_package.ML"
 
 setup FundefPackage.setup
 
+use "Tools/function_package/fundef_datatype.ML"
+setup FundefDatatype.setup
+
+use "Tools/function_package/auto_term.ML"
+setup FundefAutoTerm.setup
+
+
+lemmas [fundef_cong] = 
+  let_cong if_cong image_cong INT_cong UN_cong bex_cong ball_cong imp_cong
 
 
 end

--- a/src/HOL/List.thy	Mon Jun 05 14:22:58 2006 +0200
+++ b/src/HOL/List.thy	Mon Jun 05 14:26:07 2006 +0200
@@ -6,7 +6,7 @@
 header {* The datatype of finite lists *}
 
 theory List
-imports PreList
+imports PreList FunDef
 begin
 
 datatype 'a list =
@@ -498,7 +498,7 @@
 lemma map_eq_conv[simp]: "(map f xs = map g xs) = (!x : set xs. f x = g x)"
 by (induct xs) auto
 
-lemma map_cong [recdef_cong]:
+lemma map_cong [fundef_cong, recdef_cong]:
 "xs = ys ==> (!!x. x : set ys ==> f x = g x) ==> map f xs = map g ys"
 -- {* a congruence rule for @{text map} *}
 by simp
@@ -863,7 +863,7 @@
   (\<exists>us vs. ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs)"
 by(auto dest:Cons_eq_filterD)
 
-lemma filter_cong[recdef_cong]:
+lemma filter_cong[fundef_cong, recdef_cong]:
  "xs = ys \<Longrightarrow> (\<And>x. x \<in> set ys \<Longrightarrow> P x = Q x) \<Longrightarrow> filter P xs = filter Q ys"
 apply simp
 apply(erule thin_rl)
@@ -1363,12 +1363,12 @@
 apply(auto)
 done
 
-lemma takeWhile_cong [recdef_cong]:
+lemma takeWhile_cong [fundef_cong, recdef_cong]:
   "[| l = k; !!x. x : set l ==> P x = Q x |] 
   ==> takeWhile P l = takeWhile Q k"
   by (induct k fixing: l, simp_all)
 
-lemma dropWhile_cong [recdef_cong]:
+lemma dropWhile_cong [fundef_cong, recdef_cong]:
   "[| l = k; !!x. x : set l ==> P x = Q x |] 
   ==> dropWhile P l = dropWhile Q k"
   by (induct k fixing: l, simp_all)
@@ -1613,12 +1613,12 @@
 lemma foldr_append[simp]: "foldr f (xs @ ys) a = foldr f xs (foldr f ys a)"
 by (induct xs) auto
 
-lemma foldl_cong [recdef_cong]:
+lemma foldl_cong [fundef_cong, recdef_cong]:
   "[| a = b; l = k; !!a x. x : set l ==> f a x = g a x |] 
   ==> foldl f a l = foldl g b k"
   by (induct k fixing: a b l, simp_all)
 
-lemma foldr_cong [recdef_cong]:
+lemma foldr_cong [fundef_cong, recdef_cong]:
   "[| a = b; l = k; !!a x. x : set l ==> f x a = g x a |] 
   ==> foldr f l a = foldr g k b"
   by (induct k fixing: a b l, simp_all)

--- a/src/HOL/Recdef.thy	Mon Jun 05 14:22:58 2006 +0200
+++ b/src/HOL/Recdef.thy	Mon Jun 05 14:26:07 2006 +0200
@@ -6,7 +6,7 @@
 header {* TFL: recursive function definitions *}
 
 theory Recdef
-imports Wellfounded_Relations Datatype
+imports Wellfounded_Relations
 uses
   ("../TFL/casesplit.ML")
   ("../TFL/utils.ML")
@@ -18,7 +18,6 @@
   ("../TFL/tfl.ML")
   ("../TFL/post.ML")
   ("Tools/recdef_package.ML")
-  ("Tools/function_package/auto_term.ML")
 begin
 
 lemma tfl_eq_True: "(x = True) --> x"
@@ -97,7 +96,4 @@
 qed
 
 
-use "Tools/function_package/auto_term.ML"
-setup FundefAutoTerm.setup
-
 end

--- a/src/HOL/Tools/function_package/auto_term.ML	Mon Jun 05 14:22:58 2006 +0200
+++ b/src/HOL/Tools/function_package/auto_term.ML	Mon Jun 05 14:26:07 2006 +0200
@@ -32,7 +32,7 @@
 	val {simps, congs, wfs} = RecdefPackage.get_local_hints ctxt
 	val ss = local_simpset_of ctxt addsimps simps
 	    
-	val intro_rule = ProofContext.get_thm ctxt (Name "termination_intro")
+	val intro_rule = ProofContext.get_thm ctxt (Name "termination")
     in
 	Method.RAW_METHOD (K (auto_term_tac
 				  intro_rule

--- a/src/HOL/Tools/function_package/fundef_common.ML	Mon Jun 05 14:22:58 2006 +0200
+++ b/src/HOL/Tools/function_package/fundef_common.ML	Mon Jun 05 14:26:07 2006 +0200
@@ -22,6 +22,7 @@
   | Cong of (term * thm * depgraph * ((string * typ) list * thm list * ctx_tree) list)
   | RCall of (term * ctx_tree)
 
+type glrs = (term list * term list * term * term) list
 
 
 (* A record containing all the relevant symbols and types needed during the proof.
@@ -39,8 +40,18 @@
 
 
 datatype rec_call_info = 
-  RCInfo of {RI: thm, RIvs: (string * typ) list, lRI: thm, lRIq: thm, Gh: thm, Gh': thm} 
-
+  RCInfo 
+  of {
+  RI: thm, 
+  RIvs: (string * typ) list,
+  lRI: thm, 
+  lRIq: thm, 
+  Gh: thm, 
+  Gh': thm,
+  GmAs: term list,
+  rcarg: term
+} 
+     
 datatype clause_info =
   ClauseInfo of 
      {
@@ -73,6 +84,36 @@
 datatype curry_info =
   Curry of { argTs: typ list, curry_ss: simpset }
 
+type inj_proj = ((term -> term) * (term -> term))
+
+type qgar = (string * typ) list * term list * term list * term
+
+datatype mutual_part =
+  MutualPart of 
+	 {
+          f_name: string,
+	  const: string * typ,
+	  cargTs: typ list,
+	  pthA: SumTools.sum_path,
+	  pthR: SumTools.sum_path,
+	  qgars: qgar list,
+	  f_def: thm
+	 }
+	 
+
+datatype mutual_info =
+  Mutual of 
+	 { 
+	  name: string, 
+	  sum_const: string * typ,
+	  ST: typ,
+	  RST: typ,
+	  streeA: SumTools.sum_tree,
+	  streeR: SumTools.sum_tree,
+	  parts: mutual_part list,
+	  qglrss: (term list * term list * term * term) list list
+	 }
+
 
 datatype prep_result =
   Prep of
@@ -99,11 +140,28 @@
       dom_intros : thm list
      }
 
+datatype fundef_mresult =
+  FundefMResult of
+     {
+      f: term,
+      G : term,
+      R : term,
+
+      psimps : thm list list, 
+      subset_pinducts : thm list, 
+      simple_pinducts : thm list, 
+      cases : thm,
+      termination : thm,
+      domintros : thm list
+     }
+
+
+type result_with_names = fundef_mresult * mutual_info * string list list * attribute list list list
 
 structure FundefData = TheoryDataFun
 (struct
   val name = "HOL/function_def/data";
-  type T = string * fundef_result Symtab.table
+  type T = string * result_with_names Symtab.table
 
   val empty = ("", Symtab.empty);
   val copy = I;

--- a/src/HOL/Tools/function_package/fundef_datatype.ML	Mon Jun 05 14:22:58 2006 +0200
+++ b/src/HOL/Tools/function_package/fundef_datatype.ML	Mon Jun 05 14:26:07 2006 +0200
@@ -18,6 +18,7 @@
 structure FundefDatatype : FUNDEF_DATATYPE =
 struct
 
+
 fun mk_argvar i T = Free ("_av" ^ (string_of_int i), T)
 fun mk_patvar i T = Free ("_pv" ^ (string_of_int i), T)
 

--- a/src/HOL/Tools/function_package/fundef_lib.ML	Mon Jun 05 14:22:58 2006 +0200
+++ b/src/HOL/Tools/function_package/fundef_lib.ML	Mon Jun 05 14:26:07 2006 +0200
@@ -62,3 +62,6 @@
 fun upairs [] = []
   | upairs (x::xs) = map (pair x) (x::xs) @ upairs xs
 
+
+fun the_single [x] = x
+  | the_single _ = sys_error "the_single"
\ No newline at end of file

--- a/src/HOL/Tools/function_package/fundef_package.ML	Mon Jun 05 14:22:58 2006 +0200
+++ b/src/HOL/Tools/function_package/fundef_package.ML	Mon Jun 05 14:26:07 2006 +0200
@@ -9,12 +9,13 @@
 
 signature FUNDEF_PACKAGE = 
 sig
-    val add_fundef : ((bstring * Attrib.src list) * string) list -> theory -> Proof.state (* Need an _i variant *)
+    val add_fundef : ((bstring * Attrib.src list) * string) list list -> theory -> Proof.state (* Need an _i variant *)
 
     val cong_add: attribute
     val cong_del: attribute
 							 
     val setup : theory -> theory
+    val get_congs : theory -> thm list
 end
 
 
@@ -26,46 +27,73 @@
 val True_implies = thm "True_implies"
 
 
+fun add_simps label moreatts (MutualPart {f_name, ...}, psimps) (names, attss) thy =
+    let 
+      val thy = thy |> Theory.add_path f_name 
+                
+      val thy = thy |> Theory.add_path label
+      val spsimps = map standard psimps
+      val add_list = (names ~~ spsimps) ~~ attss
+      val (_, thy) = PureThy.add_thms add_list thy
+      val thy = thy |> Theory.parent_path
+                
+      val (_, thy) = PureThy.add_thmss [((label, spsimps), Simplifier.simp_add :: moreatts)] thy
+      val thy = thy |> Theory.parent_path
+    in
+      thy
+    end
+    
+
+
+
+
+
 fun fundef_afterqed congs curry_info name data names atts thmss thy =
     let
 	val (complete_thm :: compat_thms) = map hd thmss
-	val fundef_data = FundefProof.mk_partial_rules_curried thy congs curry_info data (freezeT complete_thm) (map freezeT compat_thms)
-	val FundefResult {psimps, subset_pinduct, simple_pinduct, total_intro, dom_intros, ...} = fundef_data
-
+	val fundef_data = FundefMutual.mk_partial_rules_mutual thy congs curry_info data (freezeT complete_thm) (map freezeT compat_thms)
+	val FundefMResult {psimps, subset_pinducts, simple_pinducts, termination, domintros, ...} = fundef_data
+        val Mutual {parts, ...} = curry_info
 
 	val Prep {names = Names {acc_R=accR, ...}, ...} = data
 	val dom_abbrev = Logic.mk_equals (Free (name ^ "_dom", fastype_of accR), accR)
 	val (_, thy) = LocalTheory.mapping NONE (Specification.abbreviation_i ("", false) [(NONE, dom_abbrev)]) thy
 
-	val thy = thy |> Theory.add_path name 
-
-	val thy = thy |> Theory.add_path "psimps"
-	val (_, thy) = PureThy.add_thms ((names ~~ psimps) ~~ atts) thy;
-	val thy = thy |> Theory.parent_path
+        val thy = fold2 (add_simps "psimps" []) (parts ~~ psimps) (names ~~ atts) thy
 
-	val (_, thy) = PureThy.add_thms [(("cases", complete_thm), [RuleCases.case_names names])] thy
-	val (_, thy) = PureThy.add_thmss [(("domintros", dom_intros), [])] thy
-	val (_, thy) = PureThy.add_thms [(("termination", total_intro), [])] thy
-	val (_,thy) = PureThy.add_thms [(("pinduct", simple_pinduct), [RuleCases.case_names names, InductAttrib.induct_set ""])] thy
-	val (_, thy) = PureThy.add_thmss [(("psimps", psimps), [Simplifier.simp_add])] thy
+	val thy = thy |> Theory.add_path name
+	val (_, thy) = PureThy.add_thms [(("cases", complete_thm), [RuleCases.case_names (flat names)])] thy
+	val (_, thy) = PureThy.add_thmss [(("domintros", domintros), [])] thy
+	val (_, thy) = PureThy.add_thms [(("termination", termination), [])] thy
+	val (_,thy) = PureThy.add_thmss [(("pinduct", map standard simple_pinducts), [RuleCases.case_names (flat names), InductAttrib.induct_set ""])] thy
 	val thy = thy |> Theory.parent_path
     in
-	add_fundef_data name fundef_data thy
+	add_fundef_data name (fundef_data, curry_info, names, atts) thy
     end
 
-fun gen_add_fundef prep_att eqns_atts thy =
+fun gen_add_fundef prep_att eqns_attss thy =
     let
-	val (natts, eqns) = split_list eqns_atts
-	val (names, raw_atts) = split_list natts
+	fun split eqns_atts =
+	    let 
+		val (natts, eqns) = split_list eqns_atts
+		val (names, raw_atts) = split_list natts
+		val atts = map (map (prep_att thy)) raw_atts
+	    in
+		((names, atts), eqns)
+	    end
 
-	val atts = map (map (prep_att thy)) raw_atts
+
+	val (natts, eqns) = split_list (map split_list eqns_attss)
+	val (names, raw_atts) = split_list (map split_list natts)
+
+	val atts = map (map (map (prep_att thy))) raw_atts
 
 	val congs = get_fundef_congs (Context.Theory thy)
 
-	val t_eqns = map (Sign.read_prop thy) eqns
-			 |> map (term_of o cterm_of thy) (* HACK to prevent strange things from happening with abbreviations *)
+	val t_eqns = map (map (Sign.read_prop thy)) eqns
+			 |> map (map (term_of o cterm_of thy)) (* HACK to prevent strange things from happening with abbreviations *)
 
-	val (curry_info, name, (data, thy)) = FundefPrep.prepare_fundef_curried congs t_eqns thy
+	val (curry_info, name, (data, thy)) = FundefMutual.prepare_fundef_mutual congs t_eqns thy
 	val Prep {complete, compat, ...} = data
 
 	val props = (complete :: compat) (*(complete :: fst (chop 110 compat))*)
@@ -76,27 +104,23 @@
     end
 
 
-fun total_termination_afterqed name thmss thy =
+fun total_termination_afterqed name (Mutual {parts, ...}) thmss thy =
     let
 	val totality = hd (hd thmss)
 
-	val FundefResult {psimps, simple_pinduct, ... }
+	val (FundefMResult {psimps, simple_pinducts, ... }, Mutual {parts, ...}, names, atts)
 	  = the (get_fundef_data name thy)
 
 	val remove_domain_condition = full_simplify (HOL_basic_ss addsimps [totality, True_implies])
 
-	val tsimps = map remove_domain_condition psimps
-	val tinduct = remove_domain_condition simple_pinduct
+	val tsimps = map (map remove_domain_condition) psimps
+	val tinduct = map remove_domain_condition simple_pinducts
+
+        val thy = fold2 (add_simps "simps" [RecfunCodegen.add NONE]) (parts ~~ tsimps) (names ~~ atts) thy
 
 	val thy = Theory.add_path name thy
 		  
-		  (* Need the names and attributes. Apply the attributes again? *)
-(*	val thy = thy |> Theory.add_path "simps"
-	val (_, thy) = PureThy.add_thms ((names ~~ tsimps) ~~ atts) thy;
-	val thy = thy |> Theory.parent_path*)
-
-	val (_, thy) = PureThy.add_thms [(("induct", tinduct), [])] thy 
-	val (_, thy) = PureThy.add_thmss [(("simps", tsimps), [Simplifier.simp_add, RecfunCodegen.add NONE])] thy
+	val (_, thy) = PureThy.add_thmss [(("induct", map standard tinduct), [])] thy 
 	val thy = Theory.parent_path thy
     in
 	thy
@@ -135,13 +159,13 @@
 	val name = if name = "" then get_last_fundef thy else name
 	val data = the (get_fundef_data name thy)
 
-	val FundefResult {total_intro, ...} = data
+	val (res as FundefMResult {termination, ...}, mutual, _, _) = data
 	val goal = FundefTermination.mk_total_termination_goal data
     in
 	thy |> ProofContext.init
-	    |> ProofContext.note_thmss_i [(("termination_intro", 
-					    [ContextRules.intro_query NONE]), [([total_intro], [])])] |> snd
-	    |> Proof.theorem_i PureThy.internalK NONE (total_termination_afterqed name) NONE ("", [])
+	    |> ProofContext.note_thmss_i [(("termination", 
+					    [ContextRules.intro_query NONE]), [([termination], [])])] |> snd
+	    |> Proof.theorem_i PureThy.internalK NONE (total_termination_afterqed name mutual) NONE ("", [])
 	    [(("", []), [(goal, [])])]
     end	
   | fundef_setup_termination_proof name (SOME (dom_name, dom)) thy =
@@ -173,6 +197,9 @@
 		[("fundef_cong", Attrib.add_del_args cong_add cong_del, "declaration of congruence rule for function definitions")]
 
 
+val get_congs = FundefCommon.get_fundef_congs o Context.Theory
+
+
 (* outer syntax *)
 
 local structure P = OuterParse and K = OuterKeyword in
@@ -182,8 +209,8 @@
 
 val functionP =
   OuterSyntax.command "function" "define general recursive functions" K.thy_goal
-    (function_decl >> (fn eqns =>
-      Toplevel.print o Toplevel.theory_to_proof (add_fundef eqns)));
+    (P.and_list1 function_decl >> (fn eqnss =>
+      Toplevel.print o Toplevel.theory_to_proof (add_fundef eqnss)));
 
 val terminationP =
   OuterSyntax.command "termination" "prove termination of a recursive function" K.thy_goal

--- a/src/HOL/Tools/function_package/fundef_prep.ML	Mon Jun 05 14:22:58 2006 +0200
+++ b/src/HOL/Tools/function_package/fundef_prep.ML	Mon Jun 05 14:26:07 2006 +0200
@@ -11,6 +11,11 @@
 sig
     val prepare_fundef_curried : thm list -> term list -> theory
 				 -> FundefCommon.curry_info option * xstring * (FundefCommon.prep_result * theory)
+
+    val prepare_fundef_new : theory -> thm list -> string -> term -> FundefCommon.glrs -> string list
+			          -> FundefCommon.prep_result * theory
+
+
 end
 
 
@@ -125,12 +130,17 @@
 		val RI = freezeT RI
 		val lRI = localize RI
 		val lRIq = fold_rev (forall_intr o cterm_of thy o mk_var0) RIvs lRI
+		val plRI = prop_of lRI
+		val GmAs = Logic.strip_imp_prems plRI
+		val rcarg = case Logic.strip_imp_concl plRI of
+				trueprop $ (memb $ (pair $ rcarg $ _) $ R) => rcarg
+			      | _ => raise Match
 			  
 		val Gh_term = Pattern.rewrite_term thy [rw_RI_to_h_assum, rw_f_to_h] [] (prop_of lRIq)
 		val Gh = assume (cterm_of thy Gh_term)
 		val Gh' = assume (cterm_of thy (rename_vars Gh_term))
 	    in
-		RCInfo {RI=RI, RIvs=RIvs, lRI=lRI, lRIq=lRIq, Gh=Gh, Gh'=Gh'}
+		RCInfo {RI=RI, RIvs=RIvs, lRI=lRI, lRIq=lRIq, Gh=Gh, Gh'=Gh', GmAs=GmAs, rcarg=rcarg}
 	    end
 
 	val case_hyp = assume (cterm_of thy (Trueprop (mk_eq (x, lhs))))
@@ -151,7 +161,7 @@
 
 (* Chooses fresh free names, declares G and R, defines f and returns a record
    with all the information *)  
-fun setup_context (f, glrs, used) fname congs thy =
+fun setup_context (f, glrs, used) defname congs thy =
     let
 	val trees = map (build_tree thy f congs) glrs
 	val allused = fold FundefCtxTree.add_context_varnames trees used
@@ -175,8 +185,8 @@
 
 	val GT = mk_relT (domT, ranT)
 	val RT = mk_relT (domT, domT)
-	val G_name = fname ^ "_graph"
-	val R_name = fname ^ "_rel"
+	val G_name = defname ^ "_graph"
+	val R_name = defname ^ "_rel"
 
 	val glrs' = mk_primed_vars thy glrs
 
@@ -292,9 +302,9 @@
  * Defines the function, the graph and the termination relation, synthesizes completeness
  * and comatibility conditions and returns everything.
  *)
-fun prepare_fundef congs eqs fname thy =
+fun prepare_fundef congs eqs defname thy =
     let
-	val (names, thy) = setup_context (analyze_eqs eqs) fname congs thy
+	val (names, thy) = setup_context (analyze_eqs eqs) defname congs thy
 	val Names {G, R, glrs, trees, ...} = names
 
 	val {G_intros, vRiss, R_intross, complete, compat} = extract_conditions thy names trees congs
@@ -310,6 +320,28 @@
     end
 
 
+fun prepare_fundef_new thy congs defname f glrs used =
+    let
+	val (names, thy) = setup_context (f, glrs, used) defname congs thy
+	val Names {G, R, glrs, trees, ...} = names
+
+	val {G_intros, vRiss, R_intross, complete, compat} = extract_conditions thy names trees congs
+
+	val (G_intro_thms, (thy, _)) = inductive_def G_intros (thy, G)
+	val (R_intro_thmss, (thy, _)) = fold_burrow inductive_def R_intross (thy, R)
+
+	val n = length glrs
+	val clauses = map3 (mk_clause_info thy names) ((1 upto n) ~~ glrs) (G_intro_thms ~~ trees) (map2 (curry op ~~) vRiss R_intro_thmss)
+    in
+	(Prep {names = names, complete=complete, compat=compat, clauses = clauses},
+	 thy) 
+    end
+
+
+
+
+
+
 
 
 fun prepare_fundef_curried congs eqs thy =

--- a/src/HOL/Tools/function_package/fundef_proof.ML	Mon Jun 05 14:22:58 2006 +0200
+++ b/src/HOL/Tools/function_package/fundef_proof.ML	Mon Jun 05 14:26:07 2006 +0200
@@ -10,6 +10,9 @@
 signature FUNDEF_PROOF =
 sig
 
+    val mk_partial_rules : theory -> thm list -> FundefCommon.prep_result 
+			   -> thm -> thm list -> FundefCommon.fundef_result
+
     val mk_partial_rules_curried : theory -> thm list -> FundefCommon.curry_info option -> FundefCommon.prep_result 
 				   -> thm -> thm list -> FundefCommon.fundef_result
 end
@@ -42,7 +45,7 @@
 
 
     
-fun mk_simp thy names f_iff graph_is_function clause valthm =
+fun mk_psimp thy names f_iff graph_is_function clause valthm =
     let
 	val Names {R, acc_R, domT, z, ...} = names
 	val ClauseInfo {qs, cqs, gs, lhs, rhs, ...} = clause
@@ -56,10 +59,10 @@
 	    |> (fn it => it COMP valthm)
 	    |> implies_intr lhs_acc 
 	    |> asm_simplify (HOL_basic_ss addsimps [f_iff])
-	    |> fold forall_intr cqs
+(*	    |> fold forall_intr cqs
 	    |> forall_elim_vars 0
 	    |> varifyT
-	    |> Drule.close_derivation
+	    |> Drule.close_derivation*)
     end
 
 
@@ -143,20 +146,23 @@
 		|> implies_intr a_D
 		|> implies_intr D_dcl
 		|> implies_intr D_subset
-		|> forall_intr_frees
-		|> forall_elim_vars 0
+
+	val subset_induct_all = fold_rev (forall_intr o cterm_of thy) [P, a, D] subset_induct_rule
 
 	val simple_induct_rule =
 	    subset_induct_rule
-		|> instantiate' [] [SOME (cterm_of thy acc_R)]
+		|> forall_intr (cterm_of thy D)
+		|> forall_elim (cterm_of thy acc_R)
 		|> (curry op COMP) subset_refl
 		|> (curry op COMP) (acc_downward
 					|> (instantiate' [SOME (ctyp_of thy domT)]
 							 (map (SOME o cterm_of thy) [x, R, z]))
 					|> forall_intr (cterm_of thy z)
 					|> forall_intr (cterm_of thy x))
+		|> forall_intr (cterm_of thy a)
+		|> forall_intr (cterm_of thy P)
     in
-	(varifyT subset_induct_rule, varifyT simple_induct_rule)
+	(subset_induct_all, simple_induct_rule)
     end
 
 
@@ -344,25 +350,13 @@
     let
 	val Names {z, R, acc_R, ...} = names
 	val ClauseInfo {qs, gs, lhs, rhs, ...} = clause
-
-	val z_lhs = cterm_of thy (HOLogic.mk_prod (z,lhs))
-	val z_acc = cterm_of thy (HOLogic.mk_mem (z,acc_R))
-
-	val icases = R_cases 
-			 |> instantiate' [] [SOME z_lhs, SOME z_acc]
-			 |> forall_intr_frees
-			 |> forall_elim_vars 0
-
 	val goal = cterm_of thy (HOLogic.mk_Trueprop (HOLogic.mk_mem (lhs,acc_R)))
     in
 	Goal.init goal 
-		  |> SINGLE (resolve_tac [accI] 1) |> the
-		  |> SINGLE (eresolve_tac [icases] 1)  |> the
-		  |> SINGLE (CLASIMPSET auto_tac) |> the
+		  |> (SINGLE (resolve_tac [accI] 1)) |> print |> the
+		  |> (SINGLE (eresolve_tac [R_cases] 1))  |> print |> the
+		  |> (SINGLE (CLASIMPSET auto_tac)) |> print |> the
 		  |> Goal.conclude
-		  |> forall_intr_frees
-		  |> forall_elim_vars 0
-		  |> varifyT
     end
 
 
@@ -530,7 +524,7 @@
 	val f_iff = (graph_is_function RS inst_ex1_iff)
 
 	val _ = Output.debug "Proving simplification rules"
-	val psimps  = map2 (mk_simp thy names f_iff graph_is_function) clauses values
+	val psimps  = map2 (mk_psimp thy names f_iff graph_is_function) clauses values
 
 	val _ = Output.debug "Proving partial induction rule"
 	val (subset_pinduct, simple_pinduct) = mk_partial_induct_rule thy names complete_thm clauses

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/function_package/mutual.ML	Mon Jun 05 14:26:07 2006 +0200
@@ -0,0 +1,264 @@
+(*  Title:      HOL/Tools/function_package/mutual.ML
+    ID:         $Id$
+    Author:     Alexander Krauss, TU Muenchen
+
+A package for general recursive function definitions. 
+Tools for mutual recursive definitions.
+
+*)
+
+signature FUNDEF_MUTUAL = 
+sig
+  
+  val prepare_fundef_mutual : thm list -> term list list -> theory ->
+                              (FundefCommon.mutual_info * string * (FundefCommon.prep_result * theory))
+
+
+  val mk_partial_rules_mutual : theory -> thm list -> FundefCommon.mutual_info -> FundefCommon.prep_result -> thm -> thm list ->
+                                FundefCommon.fundef_mresult
+end
+
+
+structure FundefMutual: FUNDEF_MUTUAL = 
+struct
+
+open FundefCommon
+
+
+
+fun check_const (Const C) = C
+  | check_const _ = raise ERROR "Head symbol of every left hand side must be a constant." (* FIXME: Output the equation here *)
+
+
+
+
+
+fun split_def geq =
+    let
+	val gs = Logic.strip_imp_prems geq
+	val eq = Logic.strip_imp_concl geq
+	val (f_args, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop eq)
+	val (fc, args) = strip_comb f_args
+	val f = check_const fc
+		    
+	val qs = fold_rev Term.add_frees args []
+		 
+	val rhs_new_vars = (Term.add_frees rhs []) \\ qs
+	val _ = if null rhs_new_vars then () 
+		else raise ERROR "Variables occur on right hand side only: " (* FIXME: Output vars here *)
+    in
+	((f, length args), (qs, gs, args, rhs))
+    end
+
+
+fun analyze_eqs thy eqss =
+    let
+	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 "
+									     ^ "constant and have the same number of arguments.")
+								      
+	val def_infoss = map (split_list o map split_def) eqss
+	val (consts, qgarss) = split_list (map (fn (Cis, eqs) => (all_equal Cis, eqs)) def_infoss)
+
+	val cnames = map (fst o fst) consts
+	val check_rcs = exists_Const (fn (n,_) => if n mem cnames 
+						  then raise ERROR "Recursive Calls not allowed in premises." else false)
+	val _ = forall (forall (fn (_, gs, _, _) => forall check_rcs gs)) qgarss
+
+	fun curried_types ((_,T), k) =
+	    let
+		val (caTs, uaTs) = chop k (binder_types T)
+	    in 
+		(caTs, uaTs ---> body_type T)
+	    end
+
+	val (caTss, resultTs) = split_list (map curried_types consts)
+	val argTs = map (foldr1 HOLogic.mk_prodT) caTss
+
+	val (RST,streeR, pthsR) = SumTools.mk_tree resultTs
+	val (ST, streeA, pthsA) = SumTools.mk_tree argTs
+
+	val def_name = foldr1 (fn (a,b) => a ^ "_" ^ b) (map Sign.base_name cnames)
+	val sfun_xname = def_name ^ "_sum"
+	val sfun_type = ST --> RST
+
+    	val thy = Sign.add_consts_i [(sfun_xname, sfun_type, NoSyn)] thy (* Add the sum function *)
+	val sfun = Const (Sign.intern_const thy sfun_xname, sfun_type)
+
+	fun define (((((n, T), _), caTs), (pthA, pthR)), qgars) (thy, rews) = 
+	    let 
+		val fxname = Sign.extern_const thy n
+		val f = Const (n, T)
+		val vars = map_index (fn (i,T) => Free ("x" ^ string_of_int i, T)) caTs
+
+		val f_exp = SumTools.mk_proj streeR pthR (sfun $ SumTools.mk_inj streeA pthA (foldr1 HOLogic.mk_prod vars))
+		val def = Logic.mk_equals (list_comb (f, vars), f_exp)
+
+		val ([f_def], thy) = PureThy.add_defs_i false [((fxname ^ "_def", def), [])] thy
+		val rews' = (f, fold_rev lambda vars f_exp) :: rews
+	    in
+		(MutualPart {f_name=fxname, const=(n, T),cargTs=caTs,pthA=pthA,pthR=pthR,qgars=qgars,f_def=f_def}, (thy, rews'))
+	    end
+
+	val _ = print pthsA
+	val _ = print pthsR
+
+	val (parts, (thy, rews)) = fold_map define (((consts ~~ caTss)~~ (pthsA ~~ pthsR)) ~~ qgarss) (thy, [])
+
+	fun mk_qglrss (MutualPart {qgars, pthA, pthR, ...}) =
+	    let
+		fun convert_eqs (qs, gs, args, rhs) =
+		    (map Free qs, gs, SumTools.mk_inj streeA pthA (foldr1 HOLogic.mk_prod args), 
+		     SumTools.mk_inj streeR pthR (Pattern.rewrite_term thy rews [] rhs))
+	    in
+		map convert_eqs qgars
+	    end
+	    
+	val qglrss = map mk_qglrss parts
+    in
+	(Mutual {name=def_name,sum_const=dest_Const sfun, ST=ST, RST=RST, streeA=streeA, streeR=streeR, parts=parts, qglrss=qglrss}, thy)
+    end
+
+
+
+
+fun prepare_fundef_mutual congs eqss thy =
+    let 
+	val (mutual, thy) = analyze_eqs thy eqss
+	val Mutual {name, sum_const, qglrss, ...} = mutual
+	val global_glrs = flat qglrss
+	val used = fold (fn (qs, _, _, _) => fold (curry op ins_string o fst o dest_Free) qs) global_glrs []
+    in
+	(mutual, name, FundefPrep.prepare_fundef_new thy congs name (Const sum_const) global_glrs used)
+    end
+
+
+(* Beta-reduce both sides of a meta-equality *)
+fun beta_norm_eq thm = 
+    let
+	val (lhs, rhs) = dest_equals (cprop_of thm)
+	val lhs_conv = beta_conversion false lhs 
+	val rhs_conv = beta_conversion false rhs 
+    in
+	transitive (symmetric lhs_conv) (transitive thm rhs_conv)
+    end
+
+
+
+
+fun map_mutual2 f (Mutual {parts, ...}) =
+    map2 (fn (p as MutualPart {qgars, ...}) => map2 (f p) qgars) parts
+
+
+
+fun recover_mutual_psimp thy RST streeR all_f_defs (MutualPart {f_def, pthR, ...}) (_,_,args,_) sum_psimp =
+    let
+	val [accCond] = cprems_of sum_psimp
+	val plain_eq = implies_elim sum_psimp (assume accCond)
+	val x = Free ("x", RST)
+
+	val f_def_inst = instantiate' [] (map (SOME o cterm_of thy) args) f_def
+    in
+	reflexive (cterm_of thy (lambda x (SumTools.mk_proj streeR pthR x)))  (*  PR(x) == PR(x) *)
+		  |> (fn it => combination it (plain_eq RS eq_reflection))
+		  |> beta_norm_eq (*  PR(S(I(as))) == PR(IR(...)) *)
+		  |> transitive f_def_inst (*  f ... == PR(IR(...)) *)
+		  |> simplify (HOL_basic_ss addsimps [SumTools.projl_inl, SumTools.projr_inr]) (*  f ... == ... *)
+		  |> simplify (HOL_basic_ss addsimps all_f_defs) (*  f ... == ... *)
+		  |> (fn it => it RS meta_eq_to_obj_eq)
+		  |> implies_intr accCond
+    end
+
+
+
+
+
+fun mutual_induct_Pnames n = 
+    if n < 5 then fst (chop n ["P","Q","R","S"])
+    else map (fn i => "P" ^ string_of_int i) (1 upto n)
+	 
+	 
+val sum_case_rules = thms "Datatype.sum.cases"
+val split_apply = thm "Product_Type.split"
+		     
+		     
+fun mutual_induct_rules thy induct all_f_defs (Mutual {qglrss, RST, parts, streeA, ...}) =
+    let
+	fun mk_P (MutualPart {cargTs, ...}) Pname =
+	    let
+		val avars = map_index (fn (i,T) => Var (("a", i), T)) cargTs
+		val atup = foldr1 HOLogic.mk_prod avars
+	    in
+		tupled_lambda atup (list_comb (Free (Pname, cargTs ---> HOLogic.boolT), avars))
+	    end
+	    
+	val Ps = map2 mk_P parts (mutual_induct_Pnames (length parts))
+	val case_exp = SumTools.mk_sumcases streeA HOLogic.boolT Ps
+		       
+	val induct_inst = 
+	    forall_elim (cterm_of thy case_exp) induct
+			|> full_simplify (HOL_basic_ss addsimps (split_apply :: sum_case_rules))
+		        |> full_simplify (HOL_basic_ss addsimps all_f_defs) 
+
+	fun mk_proj rule (MutualPart {cargTs, pthA, ...}) =
+	    let
+		val afs = map_index (fn (i,T) => Free ("a" ^ string_of_int i, T)) cargTs
+		val inj = SumTools.mk_inj streeA pthA (foldr1 HOLogic.mk_prod afs)
+	    in
+		rule 
+		    |> forall_elim (cterm_of thy inj)
+		    |> full_simplify (HOL_basic_ss addsimps (split_apply :: sum_case_rules))
+	    end
+
+    in
+	map (mk_proj induct_inst) parts
+    end
+    
+    
+
+
+
+fun mk_partial_rules_mutual thy congs (m as Mutual {qglrss, RST, parts, streeR, ...}) data complete_thm compat_thms =
+    let
+	val result = FundefProof.mk_partial_rules thy congs data complete_thm compat_thms 
+	val FundefResult {f, G, R, compatibility, completeness, psimps, subset_pinduct,simple_pinduct,total_intro,dom_intros} = result
+
+	val sum_psimps = Library.unflat qglrss psimps
+
+	val all_f_defs = map (fn MutualPart {f_def, ...} => symmetric f_def) parts
+	val mpsimps = map_mutual2 (recover_mutual_psimp thy RST streeR all_f_defs) m sum_psimps
+	val minducts = mutual_induct_rules thy simple_pinduct all_f_defs m
+        val termination = full_simplify (HOL_basic_ss addsimps all_f_defs) total_intro
+    in
+	FundefMResult { f=f, G=G, R=R,
+			psimps=mpsimps, subset_pinducts=[subset_pinduct], simple_pinducts=minducts,
+			cases=completeness, termination=termination, domintros=dom_intros}
+    end
+    
+
+end
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/function_package/sum_tools.ML	Mon Jun 05 14:26:07 2006 +0200
@@ -0,0 +1,109 @@
+(*  Title:      HOL/Tools/function_package/sum_tools.ML
+    ID:         $Id$
+    Author:     Alexander Krauss, TU Muenchen
+
+A package for general recursive function definitions. 
+Tools for mutual recursive definitions. This could actually be useful for other packages, too, but needs
+some cleanup first...
+
+*)
+
+signature SUM_TOOLS =
+sig
+  type sum_tree
+  type sum_path
+
+  val projl_inl: thm
+  val projr_inr: thm
+
+  val mk_tree : typ list -> typ * sum_tree * sum_path list
+
+  val mk_proj: sum_tree -> sum_path -> term -> term
+  val mk_inj: sum_tree -> sum_path -> term -> term
+
+  val mk_sumcases: sum_tree -> typ -> term list -> term
+end
+
+
+structure SumTools: SUM_TOOLS =
+struct
+
+val inlN = "Sum_Type.Inl"
+val inrN = "Sum_Type.Inr"
+val sumcaseN = "Datatype.sum.sum_case"
+
+val projlN = "FunDef.lproj"
+val projrN = "FunDef.rproj"
+val projl_inl = thm "FunDef.lproj_inl"
+val projr_inr = thm "FunDef.rproj_inr"
+
+
+
+fun mk_sumT LT RT = Type ("+", [LT, RT])
+fun mk_sumcase TL TR T l r = Const (sumcaseN, (TL --> T) --> (TR --> T) --> mk_sumT TL TR --> T) $ l $ r
+
+
+datatype sum_tree 
+  = Leaf of typ
+  | Branch of (typ * (typ * sum_tree) * (typ * sum_tree))
+
+type sum_path = bool list (* true: left, false: right *)
+
+fun sum_type_of (Leaf T) = T
+  | sum_type_of (Branch (ST,(LT,_),(RT,_))) = ST
+
+
+fun mk_tree Ts =
+    let 
+	fun mk_tree' 1 [T] = (T, Leaf T, [[]])
+	  | mk_tree' n Ts =
+	    let 
+		val n2 = n div 2
+		val (lTs, rTs) = chop n2 Ts
+		val (TL, ltree, lpaths) = mk_tree' n2 lTs
+		val (TR, rtree, rpaths) = mk_tree' (n - n2) rTs
+		val T = mk_sumT TL TR
+		val pths = map (cons true) lpaths @ map (cons false) rpaths 
+	    in
+		(T, Branch (T, (TL, ltree), (TR, rtree)), pths)
+	    end
+    in
+	mk_tree' (length Ts) Ts
+    end
+
+
+fun mk_inj (Leaf _) [] t = t
+  | mk_inj (Branch (ST, (LT, tr), _)) (true::pth) t = 
+    Const (inlN, LT --> ST) $ mk_inj tr pth t
+  | mk_inj (Branch (ST, _, (RT, tr))) (false::pth) t = 
+    Const (inrN, RT --> ST) $ mk_inj tr pth t
+  | mk_inj _ _ _ = sys_error "mk_inj"
+
+fun mk_proj (Leaf _) [] t = t
+  | mk_proj (Branch (ST, (LT, tr), _)) (true::pth) t = 
+    mk_proj tr pth (Const (projlN, ST --> LT) $ t)
+  | mk_proj (Branch (ST, _, (RT, tr))) (false::pth) t = 
+    mk_proj tr pth (Const (projrN, ST --> RT) $ t)
+  | mk_proj _ _ _ = sys_error "mk_proj"
+
+
+fun mk_sumcases tree T ts =
+    let
+	fun mk_sumcases' (Leaf _) (t::ts) = (t,ts)
+	  | mk_sumcases' (Branch (ST, (LT, ltr), (RT, rtr))) ts =
+	    let
+		val (lcase, ts') = mk_sumcases' ltr ts
+		val (rcase, ts'') = mk_sumcases' rtr ts'
+	    in
+		(mk_sumcase LT RT T lcase rcase, ts'')
+	    end
+	  | mk_sumcases' _ [] = sys_error "mk_sumcases"
+    in
+	fst (mk_sumcases' tree ts)
+    end
+
+end
+
+
+
+

--- a/src/HOL/Tools/function_package/termination.ML	Mon Jun 05 14:22:58 2006 +0200
+++ b/src/HOL/Tools/function_package/termination.ML	Mon Jun 05 14:26:07 2006 +0200
@@ -9,8 +9,8 @@
 
 signature FUNDEF_TERMINATION =
 sig
-    val mk_total_termination_goal : FundefCommon.fundef_result -> term
-    val mk_partial_termination_goal : theory -> FundefCommon.fundef_result -> string -> term * term
+    val mk_total_termination_goal : FundefCommon.result_with_names -> term
+    val mk_partial_termination_goal : theory -> FundefCommon.result_with_names -> string -> term * term
 end
 
 structure FundefTermination : FUNDEF_TERMINATION =
@@ -20,20 +20,16 @@
 open FundefCommon
 open FundefAbbrev
 
-fun mk_total_termination_goal data =
+fun mk_total_termination_goal (FundefMResult {R, f, ... }, _, _, _) =
     let
-	val FundefResult {R, f, ... } = data
-
 	val domT = domain_type (fastype_of f)
 	val x = Free ("x", domT)
     in
 	Trueprop (mk_mem (x, Const (acc_const_name, fastype_of R --> HOLogic.mk_setT domT) $ R))
     end
 
-fun mk_partial_termination_goal thy data dom =
+fun mk_partial_termination_goal thy (FundefMResult {R, f, ... }, _, _, _) dom =
     let
-	val FundefResult {R, f, ... } = data
-
 	val domT = domain_type (fastype_of f)
 	val D = Sign.simple_read_term thy (Type.varifyT (HOLogic.mk_setT domT)) dom
 	val DT = type_of D

--- a/src/HOL/Tools/recdef_package.ML	Mon Jun 05 14:22:58 2006 +0200
+++ b/src/HOL/Tools/recdef_package.ML	Mon Jun 05 14:26:07 2006 +0200
@@ -300,7 +300,7 @@
   LocalRecdefData.init #>
   Attrib.add_attributes
    [(recdef_simpN, Attrib.add_del_args simp_add simp_del, "declaration of recdef simp rule"),
-    (recdef_congN, Attrib.add_del_args (FundefPackage.cong_add o cong_add) (FundefPackage.cong_del o cong_del), "declaration of recdef cong rule"),
+    (recdef_congN, Attrib.add_del_args cong_add cong_del, "declaration of recdef cong rule"),
     (recdef_wfN, Attrib.add_del_args wf_add wf_del, "declaration of recdef wf rule")];
 
 

--- a/src/HOL/ex/Fundefs.thy	Mon Jun 05 14:22:58 2006 +0200
+++ b/src/HOL/ex/Fundefs.thy	Mon Jun 05 14:26:07 2006 +0200
@@ -5,11 +5,10 @@
 Examples of function definitions using the new "function" package.
 *)
 
-theory Fundefs
+theory Fundefs 
 imports Main
 begin
 
-
 section {* Very basic *}
 
 consts fib :: "nat \<Rightarrow> nat"
@@ -22,7 +21,7 @@
 
 text {* we get partial simp and induction rules: *}
 thm fib.psimps
-thm fib.pinduct
+thm pinduct
 
 text {* There is also a cases rule to distinguish cases along the definition *}
 thm fib.cases
@@ -41,6 +40,8 @@
 function
   "add 0 y = y"
   "add (Suc x) y = Suc (add x y)"
+thm add_rel.cases
+
 by pat_completeness auto
 termination
   by (auto_term "measure fst")
@@ -50,7 +51,6 @@
 
 section {* Nested recursion *}
 
-
 consts nz :: "nat \<Rightarrow> nat"
 function
   "nz 0 = 0"
@@ -61,7 +61,9 @@
   assumes trm: "x \<in> nz_dom"
   shows "nz x = 0"
 using trm
-by induct auto
+apply induct 
+apply auto
+done
 
 termination nz
   apply (auto_term "less_than") -- {* Oops, it left us something to prove *}
@@ -70,6 +72,36 @@
 thm nz.simps
 thm nz.induct
 
+text {* Here comes McCarthy's 91-function *}
+
+consts f91 :: "nat => nat"
+function 
+  "f91 n = (if 100 < n then n - 10 else f91 (f91 (n + 11)))"
+by pat_completeness auto
+
+(* Prove a lemma before attempting a termination proof *)
+lemma f91_estimate: 
+  assumes trm: "n : f91_dom" 
+  shows "n < f91 n + 11"
+using trm by induct auto
+
+(* Now go for termination *)
+termination
+proof
+  let ?R = "measure (%x. 101 - x)"
+  show "wf ?R" ..
+
+  fix n::nat assume "~ 100 < n" (* Inner call *)
+  thus "(n + 11, n) : ?R"
+    by simp arith
+
+  assume inner_trm: "n + 11 : f91_dom" (* Outer call *)
+  with f91_estimate have "n + 11 < f91 (n + 11) + 11" .
+  with `~ 100 < n` show "(f91 (n + 11), n) : ?R"
+    by simp arith
+qed
+
+
 
 section {* More general patterns *}
 
@@ -84,7 +116,8 @@
   "gcd2 (Suc x) (Suc y) = (if x < y then gcd2 (Suc x) (y - x)
                                 else gcd2 (x - y) (Suc y))"
 by pat_completeness auto
-termination by (auto_term "measure (\<lambda>(x,y). x + y)")
+termination 
+  by (auto_term "measure (\<lambda>(x,y). x + y)")
 
 thm gcd2.simps
 thm gcd2.induct
@@ -117,4 +150,34 @@
 thm ev.induct
 thm ev.cases
 
+
+section {* Mutual Recursion *}
+
+
+consts
+  evn :: "nat \<Rightarrow> bool"
+  od :: "nat \<Rightarrow> bool"
+
+function
+  "evn 0 = True"
+  "evn (Suc n) = od n"
+and
+  "od 0 = False"
+  "od (Suc n) = evn n"
+  by pat_completeness auto
+
+thm evn.psimps
+thm od.psimps
+
+thm evn_od.pinduct
+thm evn_od.termination
+thm evn_od.domintros
+
+termination
+  by (auto_term "measure (sum_case (%n. n) (%n. n))")
+
+thm evn.simps
+thm od.simps
+
+
 end