# HG changeset patch
# User krauss
# Date 1146842241 -7200
# Node ID d3e2f532459ad2f19e06c0bc63f91dbfb532ef06
# Parent  ddd36d9e6943a8654a287b848c59dccfae1559e9
First usable version of the new function definition package (HOL/function_packake/...).
Moved Accessible_Part.thy from Library to Main.

diff -r ddd36d9e6943 -r d3e2f532459a etc/isar-keywords-HOL-Nominal.el
--- a/etc/isar-keywords-HOL-Nominal.el	Fri May 05 16:50:58 2006 +0200
+++ b/etc/isar-keywords-HOL-Nominal.el	Fri May 05 17:17:21 2006 +0200
@@ -82,6 +82,7 @@
     "fix"
     "from"
     "full_prf"
+    "function"
     "global"
     "guess"
     "have"
@@ -174,6 +175,7 @@
     "subsubsection"
     "syntax"
     "term"
+    "termination"
     "text"
     "text_raw"
     "then"
@@ -423,11 +425,13 @@
 (defconst isar-keywords-theory-goal
   '("ax_specification"
     "corollary"
+    "function"
     "instance"
     "interpretation"
     "lemma"
     "recdef_tc"
     "specification"
+    "termination"
     "theorem"
     "typedef"))
 
diff -r ddd36d9e6943 -r d3e2f532459a etc/isar-keywords.el
--- a/etc/isar-keywords.el	Fri May 05 16:50:58 2006 +0200
+++ b/etc/isar-keywords.el	Fri May 05 17:17:21 2006 +0200
@@ -49,6 +49,7 @@
     "code_primclass"
     "code_primconst"
     "code_primtyco"
+    "code_purge"
     "code_serialize"
     "code_syntax_const"
     "code_syntax_tyco"
@@ -85,6 +86,7 @@
     "fixrec"
     "from"
     "full_prf"
+    "function"
     "global"
     "guess"
     "have"
@@ -177,6 +179,7 @@
     "subsubsection"
     "syntax"
     "term"
+    "termination"
     "text"
     "text_raw"
     "then"
@@ -382,6 +385,7 @@
     "code_primclass"
     "code_primconst"
     "code_primtyco"
+    "code_purge"
     "code_serialize"
     "code_syntax_const"
     "code_syntax_tyco"
@@ -445,12 +449,14 @@
   '("ax_specification"
     "corollary"
     "cpodef"
+    "function"
     "instance"
     "interpretation"
     "lemma"
     "pcpodef"
     "recdef_tc"
     "specification"
+    "termination"
     "theorem"
     "typedef"))
 
diff -r ddd36d9e6943 -r d3e2f532459a src/HOL/Accessible_Part.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Accessible_Part.thy	Fri May 05 17:17:21 2006 +0200
@@ -0,0 +1,123 @@
+(*  Title:      HOL/Accessible_Part.thy
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1994  University of Cambridge
+*)
+
+header {* The accessible part of a relation *}
+
+theory Accessible_Part
+imports Wellfounded_Recursion
+begin
+
+subsection {* Inductive definition *}
+
+text {*
+ Inductive definition of the accessible part @{term "acc r"} of a
+ relation; see also \cite{paulin-tlca}.
+*}
+
+consts
+  acc :: "('a \<times> 'a) set => 'a set"
+inductive "acc r"
+  intros
+    accI: "(!!y. (y, x) \<in> r ==> y \<in> acc r) ==> x \<in> acc r"
+
+abbreviation
+  termi :: "('a \<times> 'a) set => 'a set"
+  "termi r == acc (r\<inverse>)"
+
+
+subsection {* Induction rules *}
+
+theorem acc_induct:
+  assumes major: "a \<in> acc r"
+  assumes hyp: "!!x. x \<in> acc r ==> \<forall>y. (y, x) \<in> r --> P y ==> P x"
+  shows "P a"
+  apply (rule major [THEN acc.induct])
+  apply (rule hyp)
+   apply (rule accI)
+   apply fast
+  apply fast
+  done
+
+theorems acc_induct_rule = acc_induct [rule_format, induct set: acc]
+
+theorem acc_downward: "b \<in> acc r ==> (a, b) \<in> r ==> a \<in> acc r"
+  apply (erule acc.elims)
+  apply fast
+  done
+
+lemma acc_downwards_aux: "(b, a) \<in> r\<^sup>* ==> a \<in> acc r --> b \<in> acc r"
+  apply (erule rtrancl_induct)
+   apply blast
+  apply (blast dest: acc_downward)
+  done
+
+theorem acc_downwards: "a \<in> acc r ==> (b, a) \<in> r\<^sup>* ==> b \<in> acc r"
+  apply (blast dest: acc_downwards_aux)
+  done
+
+theorem acc_wfI: "\<forall>x. x \<in> acc r ==> wf r"
+  apply (rule wfUNIVI)
+  apply (induct_tac P x rule: acc_induct)
+   apply blast
+  apply blast
+  done
+
+theorem acc_wfD: "wf r ==> x \<in> acc r"
+  apply (erule wf_induct)
+  apply (rule accI)
+  apply blast
+  done
+
+theorem wf_acc_iff: "wf r = (\<forall>x. x \<in> acc r)"
+  apply (blast intro: acc_wfI dest: acc_wfD)
+  done
+
+
+(* Smaller relations have bigger accessible parts: *)
+lemma acc_subset:
+  assumes sub:"R1 \<subseteq> R2"
+  shows "acc R2 \<subseteq> acc R1"
+proof
+  fix x assume "x \<in> acc R2"
+  thus "x \<in> acc R1"
+  proof (induct x) -- "acc-induction"
+    fix x
+    assume ih: "\<And>y. (y, x) \<in> R2 \<Longrightarrow> y \<in> acc R1"
+    
+    with sub show "x \<in> acc R1"
+      by (blast intro:accI)
+  qed
+qed
+
+
+
+(* This is a generalized induction theorem that works on
+    subsets of the accessible part. *)
+lemma acc_subset_induct:
+  assumes subset: "D \<subseteq> acc R"
+  assumes dcl: "\<And>x z. \<lbrakk>x \<in> D; (z, x)\<in>R\<rbrakk> \<Longrightarrow> z \<in> D"
+
+  assumes "x \<in> D"
+  assumes istep: "\<And>x. \<lbrakk>x \<in> D; (\<And>z. (z, x)\<in>R \<Longrightarrow> P z)\<rbrakk> \<Longrightarrow> P x"
+shows "P x"
+proof -
+  from `x \<in> D` and subset 
+  have "x \<in> acc R" ..
+
+  thus "P x" using `x \<in> D`
+  proof (induct x)
+    fix x
+    assume "x \<in> D"
+      and "\<And>y. (y, x) \<in> R \<Longrightarrow> y \<in> D \<Longrightarrow> P y"
+
+    with dcl and istep show "P x" by blast
+  qed
+qed
+
+
+
+
+end
diff -r ddd36d9e6943 -r d3e2f532459a src/HOL/Bali/DeclConcepts.thy
--- a/src/HOL/Bali/DeclConcepts.thy	Fri May 05 16:50:58 2006 +0200
+++ b/src/HOL/Bali/DeclConcepts.thy	Fri May 05 17:17:21 2006 +0200
@@ -1914,12 +1914,12 @@
 	   next
 	     case Some
 	     with dynM
-	     have termination: "?Termination"
+	     have "termination": "?Termination"
 	       by (auto)
 	     with Some dynM
 	     have "?Dynmethd_def dynC sig=Some dynM"
 	      by (auto simp add: dynmethd_dynC_def)
-	     with subclseq_super_statC statM dynM termination
+	     with subclseq_super_statC statM dynM "termination"
 	     show ?thesis
 	       by (auto simp add: dynmethd_def)
 	   qed
diff -r ddd36d9e6943 -r d3e2f532459a src/HOL/Datatype.thy
--- a/src/HOL/Datatype.thy	Fri May 05 16:50:58 2006 +0200
+++ b/src/HOL/Datatype.thy	Fri May 05 17:17:21 2006 +0200
@@ -6,7 +6,8 @@
 header {* Datatypes *}
 
 theory Datatype
-imports Datatype_Universe
+imports Datatype_Universe FunDef
+uses ("Tools/function_package/fundef_datatype.ML")
 begin
 
 subsection {* Representing primitive types *}
@@ -314,4 +315,9 @@
     ml (target_atom "SOME")
     haskell (target_atom "Just")
 
+
+use "Tools/function_package/fundef_datatype.ML"
+setup FundefDatatype.setup
+
+
 end
diff -r ddd36d9e6943 -r d3e2f532459a src/HOL/FunDef.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/FunDef.thy	Fri May 05 17:17:21 2006 +0200
@@ -0,0 +1,49 @@
+theory FunDef
+imports Accessible_Part
+uses 
+("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/fundef_package.ML")
+begin
+
+lemma fundef_ex1_existence:
+assumes f_def: "\<And>x. f x \<equiv> THE 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 theI', rule ex1)
+
+lemma fundef_ex1_uniqueness:
+assumes f_def: "\<And>x. f x \<equiv> THE 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 the1_equality[symmetric], rule ex1, rule elm)
+
+lemma fundef_ex1_iff:
+assumes f_def: "\<And>x. f x \<equiv> THE 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 the1_equality)
+  by (rule theI', rule ex1)
+
+lemma True_implies: "(True \<Longrightarrow> PROP P) \<equiv> PROP P"
+  by simp
+
+
+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/fundef_package.ML"
+
+setup FundefPackage.setup
+
+
+
+end
diff -r ddd36d9e6943 -r d3e2f532459a src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri May 05 16:50:58 2006 +0200
+++ b/src/HOL/IsaMakefile	Fri May 05 17:17:21 2006 +0200
@@ -120,7 +120,17 @@
   antisym_setup.ML arith_data.ML blastdata.ML cladata.ML			\
   document/root.tex hologic.ML simpdata.ML ResAtpMethods.thy 			\
   Tools/res_atp_provers.ML Tools/res_atp_methods.ML	\
-  Tools/res_hol_clause.ML
+  Tools/res_hol_clause.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/fundef_package.ML 	\
+  Tools/function_package/auto_term.ML 	\
+  Tools/function_package/fundef_datatype.ML 	\
+  FunDef.thy Accessible_Part.thy 
 	@$(ISATOOL) usedir $(HOL_USEDIR_OPTIONS) -b -g true $(OUT)/Pure HOL
 
 
@@ -184,7 +194,7 @@
 
 HOL-Library: HOL $(LOG)/HOL-Library.gz
 
-$(LOG)/HOL-Library.gz: $(OUT)/HOL Library/Accessible_Part.thy \
+$(LOG)/HOL-Library.gz: $(OUT)/HOL \
   Library/SetsAndFunctions.thy Library/BigO.thy \
   Library/EfficientNat.thy Library/ExecutableSet.thy Library/ExecutableRat.thy \
   Library/FuncSet.thy Library/Library.thy \
@@ -480,7 +490,7 @@
 
 HOL-Lambda: HOL $(LOG)/HOL-Lambda.gz
 
-$(LOG)/HOL-Lambda.gz: $(OUT)/HOL Library/Accessible_Part.thy \
+$(LOG)/HOL-Lambda.gz: $(OUT)/HOL \
   Lambda/Commutation.thy Lambda/Eta.thy Lambda/InductTermi.thy Lambda/Lambda.thy \
   Lambda/ListApplication.thy Lambda/ListBeta.thy Lambda/ListOrder.thy \
   Lambda/ParRed.thy Lambda/StrongNorm.thy Lambda/Type.thy \
@@ -740,7 +750,7 @@
 
 HOL-Nominal-Examples: HOL-Nominal $(LOG)/HOL-Nominal-Examples.gz
 
-$(LOG)/HOL-Nominal-Examples.gz: $(OUT)/HOL-Nominal Library/Accessible_Part.thy	\
+$(LOG)/HOL-Nominal-Examples.gz: $(OUT)/HOL-Nominal 	\
   Nominal/Examples/ROOT.ML Nominal/Examples/CR.thy Nominal/Examples/Class.thy	\
   Nominal/Examples/Fsub.thy Nominal/Examples/Lambda_mu.thy			\
   Nominal/Examples/Iteration.thy Nominal/Examples/Lam_substs.thy		\
diff -r ddd36d9e6943 -r d3e2f532459a src/HOL/Lambda/ListOrder.thy
--- a/src/HOL/Lambda/ListOrder.thy	Fri May 05 16:50:58 2006 +0200
+++ b/src/HOL/Lambda/ListOrder.thy	Fri May 05 17:17:21 2006 +0200
@@ -6,7 +6,7 @@
 
 header {* Lifting an order to lists of elements *}
 
-theory ListOrder imports Accessible_Part begin
+theory ListOrder imports Main begin
 
 text {*
   Lifting an order to lists of elements, relating exactly one
diff -r ddd36d9e6943 -r d3e2f532459a src/HOL/Library/Accessible_Part.thy
--- a/src/HOL/Library/Accessible_Part.thy	Fri May 05 16:50:58 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,78 +0,0 @@
-(*  Title:      HOL/Library/Accessible_Part.thy
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1994  University of Cambridge
-*)
-
-header {* The accessible part of a relation *}
-
-theory Accessible_Part
-imports Main
-begin
-
-subsection {* Inductive definition *}
-
-text {*
- Inductive definition of the accessible part @{term "acc r"} of a
- relation; see also \cite{paulin-tlca}.
-*}
-
-consts
-  acc :: "('a \<times> 'a) set => 'a set"
-inductive "acc r"
-  intros
-    accI: "(!!y. (y, x) \<in> r ==> y \<in> acc r) ==> x \<in> acc r"
-
-abbreviation
-  termi :: "('a \<times> 'a) set => 'a set"
-  "termi r == acc (r\<inverse>)"
-
-
-subsection {* Induction rules *}
-
-theorem acc_induct:
-  assumes major: "a \<in> acc r"
-  assumes hyp: "!!x. x \<in> acc r ==> \<forall>y. (y, x) \<in> r --> P y ==> P x"
-  shows "P a"
-  apply (rule major [THEN acc.induct])
-  apply (rule hyp)
-   apply (rule accI)
-   apply fast
-  apply fast
-  done
-
-theorems acc_induct_rule = acc_induct [rule_format, induct set: acc]
-
-theorem acc_downward: "b \<in> acc r ==> (a, b) \<in> r ==> a \<in> acc r"
-  apply (erule acc.elims)
-  apply fast
-  done
-
-lemma acc_downwards_aux: "(b, a) \<in> r\<^sup>* ==> a \<in> acc r --> b \<in> acc r"
-  apply (erule rtrancl_induct)
-   apply blast
-  apply (blast dest: acc_downward)
-  done
-
-theorem acc_downwards: "a \<in> acc r ==> (b, a) \<in> r\<^sup>* ==> b \<in> acc r"
-  apply (blast dest: acc_downwards_aux)
-  done
-
-theorem acc_wfI: "\<forall>x. x \<in> acc r ==> wf r"
-  apply (rule wfUNIVI)
-  apply (induct_tac P x rule: acc_induct)
-   apply blast
-  apply blast
-  done
-
-theorem acc_wfD: "wf r ==> x \<in> acc r"
-  apply (erule wf_induct)
-  apply (rule accI)
-  apply blast
-  done
-
-theorem wf_acc_iff: "wf r = (\<forall>x. x \<in> acc r)"
-  apply (blast intro: acc_wfI dest: acc_wfD)
-  done
-
-end
diff -r ddd36d9e6943 -r d3e2f532459a src/HOL/Library/Library.thy
--- a/src/HOL/Library/Library.thy	Fri May 05 16:50:58 2006 +0200
+++ b/src/HOL/Library/Library.thy	Fri May 05 17:17:21 2006 +0200
@@ -1,7 +1,6 @@
 (*<*)
 theory Library
 imports
-  Accessible_Part
   BigO
   Continuity
   EfficientNat
diff -r ddd36d9e6943 -r d3e2f532459a src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Fri May 05 16:50:58 2006 +0200
+++ b/src/HOL/Library/Multiset.thy	Fri May 05 17:17:21 2006 +0200
@@ -6,7 +6,7 @@
 header {* Multisets *}
 
 theory Multiset
-imports Accessible_Part
+imports Main
 begin
 
 subsection {* The type of multisets *}
diff -r ddd36d9e6943 -r d3e2f532459a src/HOL/Nominal/Examples/SN.thy
--- a/src/HOL/Nominal/Examples/SN.thy	Fri May 05 16:50:58 2006 +0200
+++ b/src/HOL/Nominal/Examples/SN.thy	Fri May 05 17:17:21 2006 +0200
@@ -1,7 +1,7 @@
 (* $Id$ *)
 
 theory SN
-imports Lam_substs Accessible_Part
+imports Lam_substs
 begin
 
 text {* Strong Normalisation proof from the Proofs and Types book *}
diff -r ddd36d9e6943 -r d3e2f532459a src/HOL/Recdef.thy
--- a/src/HOL/Recdef.thy	Fri May 05 16:50:58 2006 +0200
+++ b/src/HOL/Recdef.thy	Fri May 05 17:17:21 2006 +0200
@@ -18,6 +18,7 @@
   ("../TFL/tfl.ML")
   ("../TFL/post.ML")
   ("Tools/recdef_package.ML")
+  ("Tools/function_package/auto_term.ML")
 begin
 
 lemma tfl_eq_True: "(x = True) --> x"
@@ -95,4 +96,8 @@
   finally show "finite (UNIV :: 'a option set)" .
 qed
 
+
+use "Tools/function_package/auto_term.ML"
+setup FundefAutoTerm.setup
+
 end
diff -r ddd36d9e6943 -r d3e2f532459a src/HOL/Tools/function_package/auto_term.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/function_package/auto_term.ML	Fri May 05 17:17:21 2006 +0200
@@ -0,0 +1,52 @@
+(*  Title:      HOL/Tools/function_package/auto_term.ML
+    ID:         $Id$
+    Author:     Alexander Krauss, TU Muenchen
+
+A package for general recursive function definitions. 
+The auto_term method.
+*)
+
+
+signature FUNDEF_AUTO_TERM =
+sig
+    val setup : theory -> theory
+end
+
+structure FundefAutoTerm : FUNDEF_AUTO_TERM = 
+struct
+
+open FundefCommon
+open FundefAbbrev
+
+
+
+fun auto_term_tac tc_intro_rule relstr wf_rules ss =
+    (resolve_tac [tc_intro_rule] 1)                    (* produce the usual goals *)
+        THEN (instantiate_tac [("R", relstr)])    (* instantiate with the given relation *)
+	THEN (ALLGOALS 
+		  (fn 1 => ares_tac wf_rules 1    (* Solve wellfoundedness *)
+		    | i => asm_simp_tac ss i))    (* Simplify termination conditions *)
+
+fun mk_termination_meth relstr ctxt =
+    let
+	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")
+    in
+	Method.RAW_METHOD (K (auto_term_tac
+				  intro_rule
+				  relstr
+				  wfs
+				  ss))
+    end
+
+
+
+val setup = Method.add_methods [("auto_term", Method.simple_args Args.name mk_termination_meth, "termination prover for recdef compatibility")]
+
+end
+
+
+
+
diff -r ddd36d9e6943 -r d3e2f532459a src/HOL/Tools/function_package/context_tree.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/function_package/context_tree.ML	Fri May 05 17:17:21 2006 +0200
@@ -0,0 +1,240 @@
+(*  Title:      HOL/Tools/function_package/context_tree.ML
+    ID:         $Id$
+    Author:     Alexander Krauss, TU Muenchen
+
+A package for general recursive function definitions. 
+Builds and traverses trees of nested contexts along a term.
+*)
+
+
+signature FUNDEF_CTXTREE =
+sig
+    type ctx_tree
+
+    (* FIXME: This interface is a mess and needs to be cleaned up! *)
+    val cong_deps : thm -> int FundefCommon.IntGraph.T
+    val add_congs : thm list
+
+    val mk_tree: theory -> (thm * FundefCommon.depgraph) list -> term -> term -> FundefCommon.ctx_tree
+
+    val add_context_varnames : FundefCommon.ctx_tree -> string list -> string list
+
+    val export_term : (string * typ) list * term list -> term -> term
+    val export_thm : theory -> (string * typ) list * term list -> thm -> thm
+    val import_thm : theory -> (string * typ) list * thm list -> thm -> thm
+
+
+    val traverse_tree : 
+   ((string * typ) list * thm list -> term ->
+   (((string * typ) list * thm list) * thm) list ->
+   (((string * typ) list * thm list) * thm) list * 'b ->
+   (((string * typ) list * thm list) * thm) list * 'b)
+   -> FundefCommon.ctx_tree -> 'b -> 'b
+
+    val rewrite_by_tree : theory -> 'a -> term -> thm -> (thm * thm) list -> FundefCommon.ctx_tree -> thm * (thm * thm) list
+end
+
+structure FundefCtxTree : FUNDEF_CTXTREE =
+struct
+
+open FundefCommon
+
+
+(* Maps "Trueprop A = B" to "A" *)
+val rhs_of = snd o HOLogic.dest_eq o HOLogic.dest_Trueprop
+(* Maps "A == B" to "B" *)
+val meta_rhs_of = snd o Logic.dest_equals
+
+
+
+(*** Dependency analysis for congruence rules ***)
+
+fun branch_vars t = 
+    let	val (assumes, term) = dest_implies_list (snd (dest_all_all t))
+    in (fold (curry add_term_vars) assumes [], term_vars term)
+    end
+
+fun cong_deps crule =
+    let
+	val branches = map branch_vars (prems_of crule)
+	val num_branches = (1 upto (length branches)) ~~ branches
+    in
+	IntGraph.empty
+	    |> fold (fn (i,_)=> IntGraph.new_node (i,i)) num_branches
+	    |> fold (fn ((i,(c1,_)),(j,(_, t2))) => if i = j orelse null (c1 inter t2) then I else IntGraph.add_edge_acyclic (i,j))
+	    (product num_branches num_branches)
+    end
+    
+val add_congs = map (fn c => c RS eq_reflection) [cong, ext] 
+
+
+
+(* Called on the INSTANTIATED branches of the congruence rule *)
+fun mk_branch t = 
+    let
+	val (fixes, impl) = dest_all_all t
+	val (assumes, term) = dest_implies_list impl
+    in
+	(map dest_Free fixes, assumes, rhs_of term)
+    end
+
+
+
+
+
+exception CTREE_INTERNAL of string
+
+fun find_cong_rule thy ((r,dep)::rs) t =
+    (let
+	val (c, subs) = (meta_rhs_of (concl_of r), prems_of r)
+
+	val subst = Pattern.match thy (c, t) (Vartab.empty, Vartab.empty)
+
+	val branches = map (mk_branch o Envir.beta_norm o Envir.subst_vars subst) subs
+     in
+	 (r, dep, branches)
+     end
+    handle Pattern.MATCH => find_cong_rule thy rs t)
+  | find_cong_rule thy [] _ = raise CTREE_INTERNAL "No cong rule found!" (* Should never happen *)
+
+
+fun matchcall f (a $ b) = if a = f then SOME b else NONE
+  | matchcall f _ = NONE
+
+fun mk_tree thy congs f t =
+    case matchcall f t of
+	SOME arg => RCall (t, mk_tree thy congs f arg)
+      | NONE => 
+	if not (exists_Const (curry op = (dest_Const f)) t) then Leaf t
+	else 
+	    let val (r, dep, branches) = find_cong_rule thy congs t in
+		Cong (t, r, dep, map (fn (fixes, assumes, st) => 
+					 (fixes, map (assume o cterm_of thy) assumes, mk_tree thy congs f st)) branches)
+	    end
+		
+		
+fun add_context_varnames (Leaf _) = I
+  | add_context_varnames (Cong (_, _, _, sub)) = fold (fn (fs, _, st) => fold (curry op ins_string o fst) fs o add_context_varnames st) sub
+  | add_context_varnames (RCall (_,st)) = add_context_varnames st
+    
+
+(* Poor man's contexts: Only fixes and assumes *)
+fun compose (fs1, as1) (fs2, as2) = (fs1 @ fs2, as1 @ as2)
+
+fun export_term (fixes, assumes) =
+    fold_rev (curry Logic.mk_implies) assumes #> fold (mk_forall o Free) fixes
+
+fun export_thm thy (fixes, assumes) =
+    fold_rev (implies_intr o cterm_of thy) assumes
+ #> fold_rev (forall_intr o cterm_of thy o Free) fixes
+
+fun import_thm thy (fixes, athms) =
+    fold (forall_elim o cterm_of thy o Free) fixes
+ #> fold implies_elim_swp athms
+
+fun assume_in_ctxt thy (fixes, athms) prop =
+    let
+	val global_assum = export_term (fixes, map prop_of athms) prop
+    in
+	(global_assum,
+	 assume (cterm_of thy global_assum) |> import_thm thy (fixes, athms))
+    end
+
+
+(* folds in the order of the dependencies of a graph. *)
+fun fold_deps G f x =
+    let
+	fun fill_table i (T, x) =
+	    case Inttab.lookup T i of
+		SOME _ => (T, x)
+	      | NONE => 
+		let
+		    val (T', x') = fold fill_table (IntGraph.imm_succs G i) (T, x)
+		    val (v, x'') = f (the o Inttab.lookup T') i x
+		in
+		    (Inttab.update (i, v) T', x'')
+		end
+
+	val (T, x) = fold fill_table (IntGraph.keys G) (Inttab.empty, x)
+    in
+	(Inttab.fold (cons o snd) T [], x)
+    end
+
+
+fun flatten xss = fold_rev append xss []
+
+fun traverse_tree rcOp tr x =
+    let 
+	fun traverse_help ctx (Leaf _) u x = ([], x)
+	  | traverse_help ctx (RCall (t, st)) u x =
+	    rcOp ctx t u (traverse_help ctx st u x)
+	  | traverse_help ctx (Cong (t, crule, deps, branches)) u x =
+	    let
+		fun sub_step lu i x =
+		    let
+			val (fixes, assumes, subtree) = nth branches (i - 1)
+			val used = fold_rev (append o lu) (IntGraph.imm_succs deps i) u
+			val (subs, x') = traverse_help (compose ctx (fixes, assumes)) subtree used x
+			val exported_subs = map (apfst (compose (fixes, assumes))) subs
+		    in
+			(exported_subs, x')
+		    end
+	    in
+		fold_deps deps sub_step x
+			  |> apfst flatten
+	    end
+    in
+	snd (traverse_help ([], []) tr [] x)
+    end
+
+
+fun is_refl thm = let val (l,r) = Logic.dest_equals (prop_of thm) in l = r end
+
+fun rewrite_by_tree thy f h ih x tr =
+    let
+	fun rewrite_help fix f_as h_as x (Leaf t) = (reflexive (cterm_of thy t), x)
+	  | rewrite_help fix f_as h_as x (RCall (_ $ arg, st)) =
+	    let
+		val (inner, (Ri,ha)::x') = rewrite_help fix f_as h_as x st
+					   
+					   (* Need not use the simplifier here. Can use primitive steps! *)
+		val rew_ha = if is_refl inner then I else simplify (HOL_basic_ss addsimps [inner])
+			     
+		val h_a_eq_h_a' = combination (reflexive (cterm_of thy h)) inner
+		val iRi = import_thm thy (fix, f_as) Ri (* a < lhs *)
+		val iha = import_thm thy (fix, h_as) ha (* (a', h a') : G *)
+				     |> rew_ha
+
+		val inst_ih = instantiate' [] [SOME (cterm_of thy arg)] ih
+		val eq = implies_elim (implies_elim inst_ih iRi) iha
+			 
+		val h_a'_eq_f_a' = eq RS eq_reflection
+		val result = transitive h_a_eq_h_a' h_a'_eq_f_a'
+	    in
+		(result, x')
+	    end
+	  | rewrite_help fix f_as h_as x (Cong (t, crule, deps, branches)) =
+	    let
+		fun sub_step lu i x =
+		    let
+			val (fixes, assumes, st) = nth branches (i - 1)
+			val used = fold_rev (cons o lu) (IntGraph.imm_succs deps i) []
+			val used_rev = map (fn u_eq => (u_eq RS sym) RS eq_reflection) used
+			val assumes' = map (simplify (HOL_basic_ss addsimps (filter_out is_refl used_rev))) assumes
+
+			val (subeq, x') = rewrite_help (fix @ fixes) (f_as @ assumes) (h_as @ assumes') x st
+			val subeq_exp = export_thm thy (fixes, map prop_of assumes) (subeq RS meta_eq_to_obj_eq)
+		    in
+			(subeq_exp, x')
+		    end
+		    
+		val (subthms, x') = fold_deps deps sub_step x
+	    in
+		(fold_rev (curry op COMP) subthms crule, x')
+	    end
+	    
+    in
+	rewrite_help [] [] [] x tr
+    end
+
+end
\ No newline at end of file
diff -r ddd36d9e6943 -r d3e2f532459a src/HOL/Tools/function_package/fundef_common.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/function_package/fundef_common.ML	Fri May 05 17:17:21 2006 +0200
@@ -0,0 +1,182 @@
+(*  Title:      HOL/Tools/function_package/fundef_common.ML
+    ID:         $Id$
+    Author:     Alexander Krauss, TU Muenchen
+
+A package for general recursive function definitions. 
+Common type definitions and other infrastructure.
+*)
+
+structure FundefCommon =
+struct
+
+(* Theory Dependencies *)
+val acc_const_name = "Accessible_Part.acc"
+
+
+
+(* Partial orders to represent dependencies *)
+structure IntGraph = GraphFun(type key = int val ord = int_ord);
+
+type depgraph = int IntGraph.T
+
+
+datatype ctx_tree 
+  = Leaf of term
+  | Cong of (term * thm * depgraph * ((string * typ) list * thm list * ctx_tree) list)
+  | RCall of (term * ctx_tree)
+
+
+
+(* A record containing all the relevant symbols and types needed during the proof.
+   This is set up at the beginning and does not change. *)
+type naming_context =
+     { f: term, fvarname: string, fvar: term, domT: typ, ranT: typ,
+       G: term, R: term, acc_R: term, h: term, y: term, x: term, z: term, a:term, P: term, 
+       D: term, Pbool:term,
+       glrs: (term list * term list * term * term) list,
+       glrs': (term list * term list * term * term) list,
+       f_def: thm,
+       used: string list,
+       trees: ctx_tree list
+     }
+
+
+type rec_call_info = 
+     {RI: thm, RIvs: (string * typ) list, lRI: thm, lRIq: thm, Gh: thm, Gh': thm} 
+
+type clause_info =
+     {
+      no: int,
+
+      qs: term list, 
+      gs: term list,
+      lhs: term,
+      rhs: term,
+
+      cqs: cterm list,
+      cvqs: cterm list,
+      ags: thm list,
+      
+      cqs': cterm list, 
+      ags': thm list,
+      lhs': term,
+      rhs': term,
+      ordcqs': cterm list, 
+
+      GI: thm,
+      lGI: thm,
+      RCs: rec_call_info list,
+
+      tree: ctx_tree,
+      case_hyp: thm
+     }
+
+
+type curry_info =
+     { argTs: typ list, curry_ss: simpset }
+
+
+type prep_result =
+     {
+      names: naming_context, 
+      complete : term,
+      compat : term list,
+      clauses: clause_info list
+     }
+
+type fundef_result =
+     {
+      f: term,
+      G : term,
+      R : term,
+      completeness : thm,
+      compatibility : thm list,
+
+      psimps : thm list, 
+      subset_pinduct : thm, 
+      simple_pinduct : thm, 
+      total_intro : thm,
+      dom_intros : thm list
+     }
+
+
+structure FundefData = TheoryDataFun
+(struct
+  val name = "HOL/function_def/data";
+  type T = string * fundef_result Symtab.table
+
+  val empty = ("", Symtab.empty);
+  val copy = I;
+  val extend = I;
+  fun merge _ ((l1,tab1),(l2,tab2)) = (l1, Symtab.merge (op =) (tab1, tab2))
+
+  fun print _ _ = ();
+end);
+
+
+structure FundefCongs = GenericDataFun
+(struct
+    val name = "HOL/function_def/congs"
+    type T = thm list
+    val empty = []
+    val extend = I
+    fun merge _ (l1, l2) = l1 @ l2
+    fun print  _ _ = ()
+end);
+
+
+fun add_fundef_data name fundef_data =
+    FundefData.map (fn (_,tab) => (name, Symtab.update_new (name, fundef_data) tab))
+
+fun get_fundef_data name thy = Symtab.lookup (snd (FundefData.get thy)) name
+
+fun get_last_fundef thy = fst (FundefData.get thy)
+
+val map_fundef_congs = FundefCongs.map 
+val get_fundef_congs = FundefCongs.get
+
+end
+
+
+
+(* Common Abbreviations *)
+
+structure FundefAbbrev =
+struct
+
+fun implies_elim_swp x y = implies_elim y x
+
+(* Some HOL things frequently used *)
+val boolT = HOLogic.boolT
+val mk_prod = HOLogic.mk_prod
+val mk_mem = HOLogic.mk_mem
+val mk_eq = HOLogic.mk_eq
+val Trueprop = HOLogic.mk_Trueprop
+
+val mk_relT = HOLogic.mk_setT o HOLogic.mk_prodT
+fun mk_relmem (x,y) R = Trueprop (mk_mem (mk_prod (x, y), R))
+
+fun mk_subset T A B = 
+    let val sT = HOLogic.mk_setT T
+    in Const ("Orderings.less_eq", sT --> sT --> boolT) $ A $ B end
+
+
+(* with explicit types: Needed with loose bounds *)
+fun mk_relmemT xT yT (x,y) R = 
+    let 
+	val pT = HOLogic.mk_prodT (xT, yT)
+	val RT = HOLogic.mk_setT pT
+    in
+	Const ("op :", [pT, RT] ---> boolT)
+	      $ (HOLogic.pair_const xT yT $ x $ y)
+	      $ R
+    end
+
+fun free_to_var (Free (v,T)) = Var ((v,0),T)
+  | free_to_var _ = raise Match
+
+fun var_to_free (Var ((v,_),T)) = Free (v,T)
+  | var_to_free _ = raise Match
+
+
+end
diff -r ddd36d9e6943 -r d3e2f532459a src/HOL/Tools/function_package/fundef_datatype.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/function_package/fundef_datatype.ML	Fri May 05 17:17:21 2006 +0200
@@ -0,0 +1,167 @@
+(*  Title:      HOL/Tools/function_package/fundef_datatype.ML
+    ID:         $Id$
+    Author:     Alexander Krauss, TU Muenchen
+
+A package for general recursive function definitions. 
+A tactic to prove completeness of datatype patterns.
+*)
+
+signature FUNDEF_DATATYPE = 
+sig
+    val pat_complete_tac: int -> tactic
+
+    val setup : theory -> theory
+end
+
+
+
+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)
+
+fun inst_free var inst thm =
+    forall_elim inst (forall_intr var thm)
+
+
+fun inst_case_thm thy x P thm =
+    let
+	val [Pv, xv] = term_vars (prop_of thm)
+    in
+	cterm_instantiate [(cterm_of thy xv, cterm_of thy x), (cterm_of thy Pv, cterm_of thy P)] thm
+    end
+
+
+fun invent_vars constr i =
+    let
+	val Ts = binder_types (fastype_of constr)
+	val j = i + length Ts
+	val is = i upto (j - 1)
+	val avs = map2 mk_argvar is Ts
+	val pvs = map2 mk_patvar is Ts
+    in
+	(avs, pvs, j)
+    end
+
+
+fun filter_pats thy cons pvars [] = []
+  | filter_pats thy cons pvars (([], thm) :: pts) = raise Match
+  | filter_pats thy cons pvars ((pat :: pats, thm) :: pts) = 
+    case pat of
+	Free _ => let val inst = list_comb (cons, pvars)
+		 in (inst :: pats, inst_free (cterm_of thy pat) (cterm_of thy inst) thm)
+		    :: (filter_pats thy cons pvars pts) end
+      | _ => if fst (strip_comb pat) = cons
+	     then (pat :: pats, thm) :: (filter_pats thy cons pvars pts)
+	     else filter_pats thy cons pvars pts
+
+
+fun inst_constrs_of thy (T as Type (name, _)) =
+	map (fn (Cn,CT) => Envir.subst_TVars (Type.typ_match (Sign.tsig_of thy) (body_type CT, T) Vartab.empty) (Const (Cn, CT)))
+	    (the (DatatypePackage.get_datatype_constrs thy name))
+  | inst_constrs_of thy _ = raise Match
+
+
+fun transform_pat thy avars c_assum ([] , thm) = raise Match
+  | transform_pat thy avars c_assum (pat :: pats, thm) =
+    let
+	val (_, subps) = strip_comb pat
+	val eqs = map (cterm_of thy o HOLogic.mk_Trueprop o HOLogic.mk_eq) (avars ~~ subps)
+	val a_eqs = map assume eqs
+	val c_eq_pat = simplify (HOL_basic_ss addsimps a_eqs) c_assum
+    in
+	(subps @ pats, fold_rev implies_intr eqs
+				(implies_elim thm c_eq_pat))
+    end
+
+
+exception COMPLETENESS
+
+fun constr_case thy P idx (v :: vs) pats cons =
+    let
+	val (avars, pvars, newidx) = invent_vars cons idx
+	val c_hyp = cterm_of thy (HOLogic.mk_Trueprop (HOLogic.mk_eq (v, list_comb (cons, avars))))
+	val c_assum = assume c_hyp
+	val newpats = map (transform_pat thy avars c_assum) (filter_pats thy cons pvars pats)
+    in
+	o_alg thy P newidx (avars @ vs) newpats
+	      |> implies_intr c_hyp
+	      |> fold_rev (forall_intr o cterm_of thy) avars
+    end
+  | constr_case _ _ _ _ _ _ = raise Match
+and o_alg thy P idx [] (([], Pthm) :: _)  = Pthm
+  | o_alg thy P idx (v :: vs) [] = raise COMPLETENESS
+  | o_alg thy P idx (v :: vs) pts =
+    if forall (is_Free o hd o fst) pts (* Var case *)
+    then o_alg thy P idx vs (map (fn (pv :: pats, thm) =>
+			       (pats, refl RS (inst_free (cterm_of thy pv) (cterm_of thy v) thm))) pts)
+    else (* Cons case *)
+	 let  
+	     val T = fastype_of v
+	     val (tname, _) = dest_Type T
+	     val {exhaustion=case_thm, ...} = DatatypePackage.the_datatype thy tname
+	     val constrs = inst_constrs_of thy T
+	     val c_cases = map (constr_case thy P idx (v :: vs) pts) constrs
+	 in 
+	     inst_case_thm thy v P case_thm
+			   |> fold (curry op COMP) c_cases
+	 end
+  | o_alg _ _ _ _ _ = raise Match
+
+			   
+fun prove_completeness thy x P qss pats =
+    let
+	fun mk_assum qs pat = Logic.mk_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (x,pat)),
+						HOLogic.mk_Trueprop P)
+					       |> fold_rev mk_forall qs
+					       |> cterm_of thy
+
+	val hyps = map2 mk_assum qss pats
+
+	fun inst_hyps hyp qs = fold (forall_elim o cterm_of thy) qs (assume hyp)
+
+	val assums = map2 inst_hyps hyps qss
+    in
+	o_alg thy P 2 [x] (map2 (pair o single) pats assums)
+	      |> fold_rev implies_intr hyps
+	      |> zero_var_indexes
+	      |> forall_intr_frees
+	      |> forall_elim_vars 0 
+    end
+
+
+
+fun pat_complete_tac i thm =
+    let 
+	val subgoal = nth (prems_of thm) (i - 1)
+	val assums = Logic.strip_imp_prems subgoal
+	val _ $ P = Logic.strip_imp_concl subgoal
+		    
+	fun pat_of assum = 
+	    let
+		val (qs, imp) = dest_all_all assum
+	    in
+		case Logic.dest_implies imp of 
+		    (_ $ (_ $ x $ pat), _) => (x, (qs, pat))
+		  | _ => raise COMPLETENESS
+	    end
+
+	val (x, (qss, pats)) = 
+	    case (map pat_of assums) of
+		[] => raise COMPLETENESS
+	      | rs as ((x,_) :: _) 
+		=> (x, split_list (snd (split_list rs)))
+
+	val complete_thm = prove_completeness (theory_of_thm thm) x P qss pats
+    in
+	Seq.single (Drule.compose_single(complete_thm, i, thm))
+    end
+    handle COMPLETENESS => Seq.empty
+
+
+
+val setup = 
+    Method.add_methods [("pat_completeness", Method.no_args (Method.SIMPLE_METHOD (pat_complete_tac 1)), "Completeness prover for datatype patterns")]
+
+end
\ No newline at end of file
diff -r ddd36d9e6943 -r d3e2f532459a src/HOL/Tools/function_package/fundef_lib.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/function_package/fundef_lib.ML	Fri May 05 17:17:21 2006 +0200
@@ -0,0 +1,64 @@
+(*  Title:      HOL/Tools/function_package/lib.ML
+    ID:         $Id$
+    Author:     Alexander Krauss, TU Muenchen
+
+A package for general recursive function definitions. 
+Some fairly general functions that should probably go somewhere else... 
+*)
+
+
+fun mk_forall (var as Free (v,T)) t =
+    all T $ Abs (v,T, abstract_over (var,t))
+  | mk_forall _ _ = raise Match
+
+(* Builds a quantification with a new name for the variable. *)
+fun mk_forall_rename ((v,T),newname) t =
+    all T $ Abs (newname,T, abstract_over (Free (v,T),t))
+
+(* Constructs a tupled abstraction from an arbitrarily nested tuple of variables and a term. *)
+fun tupled_lambda vars t =
+    case vars of
+	(Free v) => lambda (Free v) t
+      | (Var v) => lambda (Var v) t
+      | (Const ("Pair", Type ("fun", [Ta, Type ("fun", [Tb, _])]))) $ us $ vs =>  
+	(HOLogic.split_const (Ta,Tb, fastype_of t)) $ (tupled_lambda us (tupled_lambda vs t))
+      | _ => raise Match
+
+
+fun dest_all (Const ("all", _) $ Abs (a as (_,T,_))) =
+    let
+	val (n, body) = Term.dest_abs a
+    in
+	(Free (n, T), body)
+    end
+  | dest_all _ = raise Match
+
+
+(* Removes all quantifiers from a term, replacing bound variables by frees. *)
+fun dest_all_all (t as (Const ("all",_) $ _)) = 
+    let
+	val (v,b) = dest_all t
+	val (vs, b') = dest_all_all b
+    in
+	(v :: vs, b')
+    end
+  | dest_all_all t = ([],t)
+
+(* unfold *)
+fun unfold P f g b x = if (P x) then ((f x)::(unfold P f g b (g x))) else (b x)
+
+val dest_implies_list = 
+    split_last o (unfold Logic.is_implies (fst o Logic.dest_implies) (snd o Logic.dest_implies) single)
+
+fun implies_elim_swp a b = implies_elim b a
+
+fun map3 _ [] [] [] = []
+  | map3 f (x :: xs) (y :: ys) (z :: zs) = f x y z :: map3 f xs ys zs
+  | map3 _ _ _ _ = raise UnequalLengths;
+
+
+
+(* forms all "unordered pairs": [1, 2, 3] ==> [(1, 1), (1, 2), (1, 3), (2, 2), (2, 3), (3, 3)] *)
+fun upairs [] = []
+  | upairs (x::xs) = map (pair x) (x::xs) @ upairs xs
+
diff -r ddd36d9e6943 -r d3e2f532459a src/HOL/Tools/function_package/fundef_package.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/function_package/fundef_package.ML	Fri May 05 17:17:21 2006 +0200
@@ -0,0 +1,197 @@
+(*  Title:      HOL/Tools/function_package/fundef_package.ML
+    ID:         $Id$
+    Author:     Alexander Krauss, TU Muenchen
+
+A package for general recursive function definitions. 
+Isar commands.
+
+*)
+
+signature FUNDEF_PACKAGE = 
+sig
+    val add_fundef : ((bstring * Attrib.src list) * string) list -> theory -> Proof.state (* Need an _i variant *)
+
+    val cong_add: attribute
+    val cong_del: attribute
+							 
+    val setup : theory -> theory
+end
+
+
+structure FundefPackage : FUNDEF_PACKAGE =
+struct
+
+open FundefCommon
+
+val True_implies = thm "True_implies"
+
+
+(*#> FundefTermination.setup #> FundefDatatype.setup*)
+
+fun fundef_afterqed congs curry_info name data natts 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 {psimps, subset_pinduct, simple_pinduct, total_intro, dom_intros, ...} = fundef_data
+
+	val (names, attsrcs) = split_list natts
+	val atts = map (map (Attrib.attribute thy)) attsrcs
+
+	val accR = (#acc_R(#names(data)))
+	val dom_abbrev = Logic.mk_equals (Free ("dom", fastype_of accR), accR)
+
+	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) = LocalTheory.mapping NONE (Specification.abbreviation_i ("", false) [(NONE, dom_abbrev)]) 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.parent_path
+    in
+	add_fundef_data name fundef_data thy
+    end
+
+fun add_fundef eqns_atts thy =
+    let
+	val (natts, eqns) = split_list eqns_atts
+
+	val congs = get_fundef_congs (Context.Theory thy)
+
+	val (curry_info, name, (data, thy)) = FundefPrep.prepare_fundef_curried congs (map (Sign.read_prop thy) eqns) thy
+	val {complete, compat, ...} = data
+
+	val props = (complete :: compat) (*(complete :: fst (chop 110 compat))*)
+    in
+	thy |> ProofContext.init
+	    |> Proof.theorem_i PureThy.internalK NONE (fundef_afterqed congs curry_info name data natts) NONE ("", [])
+	    (map (fn t => (("", []), [(t, ([], []))])) props)
+    end
+
+
+fun total_termination_afterqed name thmss thy =
+    let
+	val totality = hd (hd thmss)
+
+	val {psimps, simple_pinduct, ... }
+	  = 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 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 = Theory.parent_path thy
+    in
+	thy
+    end
+
+(*
+fun mk_partial_rules name D_name D domT idomT thmss thy =
+    let
+	val [subs, dcl] = (hd thmss)
+
+	val {f_const, f_curried_const, G_const, R_const, G_elims, completeness, f_simps, names_attrs, subset_induct, ... }
+	  = the (Symtab.lookup (FundefData.get thy) name)
+
+	val D_implies_dom = subs COMP (instantiate' [SOME (ctyp_of thy idomT)] 
+						    [SOME (cterm_of thy D)]
+						    subsetD)
+
+	val D_simps = map (curry op RS D_implies_dom) f_simps
+
+	val D_induct = subset_induct
+			   |> cterm_instantiate [(cterm_of thy (Var (("D",0), fastype_of D)) ,cterm_of thy D)]
+			   |> curry op COMP subs
+			   |> curry op COMP (dcl |> forall_intr (cterm_of thy (Var (("z",0), idomT)))
+						 |> forall_intr (cterm_of thy (Var (("x",0), idomT))))
+
+	val ([tinduct'], thy2) = PureThy.add_thms [((name ^ "_" ^ D_name ^ "_induct", D_induct), [])] thy
+	val ([tsimps'], thy3) = PureThy.add_thmss [((name ^ "_" ^ D_name ^ "_simps", D_simps), [])] thy2
+    in
+	thy3
+    end
+*)
+ 
+
+fun fundef_setup_termination_proof name NONE thy = 
+    let
+	val name = if name = "" then get_last_fundef thy else name
+	val data = the (get_fundef_data name thy)
+
+	val {total_intro, ...} = 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 ("", [])
+	    [(("", []), [(goal, ([], []))])]
+    end	
+  | fundef_setup_termination_proof name (SOME (dom_name, dom)) thy =
+    let
+	val name = if name = "" then get_last_fundef thy else name
+	val data = the (get_fundef_data name thy)
+	val (subs, dcl) = FundefTermination.mk_partial_termination_goal thy data dom
+    in
+	thy |> ProofContext.init
+	    |> Proof.theorem_i PureThy.internalK NONE (K I) NONE ("", [])
+	    [(("", []), [(subs, ([], [])), (dcl, ([], []))])]
+    end	
+
+
+
+
+(* congruence rules *)
+
+val cong_add = Thm.declaration_attribute (map_fundef_congs o cons o safe_mk_meta_eq);
+val cong_del = Thm.declaration_attribute (map_fundef_congs o remove (op =) o safe_mk_meta_eq);
+
+
+(* setup *)
+
+val setup = FundefData.init #> FundefCongs.init 
+	#>  Attrib.add_attributes
+		[("fundef_cong", Attrib.add_del_args cong_add cong_del, "declaration of congruence rule for function definitions")]
+
+
+(* outer syntax *)
+
+local structure P = OuterParse and K = OuterKeyword in
+
+val function_decl =
+    Scan.repeat1 (P.opt_thm_name ":" -- P.prop);
+
+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)));
+
+val terminationP =
+  OuterSyntax.command "termination" "prove termination of a recursive function" K.thy_goal
+  ((Scan.optional P.name "" -- Scan.option (P.$$$ "(" |-- Scan.optional (P.name --| P.$$$ ":") "dom" -- P.term --| P.$$$ ")"))
+       >> (fn (name,dom) =>
+	      Toplevel.print o Toplevel.theory_to_proof (fundef_setup_termination_proof name dom)));
+
+val _ = OuterSyntax.add_parsers [functionP];
+val _ = OuterSyntax.add_parsers [terminationP];
+
+
+end;
+
+
+end
\ No newline at end of file
diff -r ddd36d9e6943 -r d3e2f532459a src/HOL/Tools/function_package/fundef_prep.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/function_package/fundef_prep.ML	Fri May 05 17:17:21 2006 +0200
@@ -0,0 +1,355 @@
+(*  Title:      HOL/Tools/function_package/fundef_prep.ML
+    ID:         $Id$
+    Author:     Alexander Krauss, TU Muenchen
+
+A package for general recursive function definitions. 
+Preparation step: makes auxiliary definitions and generates
+proof obligations.
+*)
+
+signature FUNDEF_PREP =
+sig
+    val prepare_fundef_curried : thm list -> term list -> theory
+				 -> FundefCommon.curry_info option * xstring * (FundefCommon.prep_result * theory)
+end
+
+
+
+
+
+structure FundefPrep : FUNDEF_PREP =
+struct
+
+
+open FundefCommon
+open FundefAbbrev 
+
+
+
+
+fun split_list3 [] = ([],[],[])
+  | split_list3 ((x,y,z)::xyzs) = 
+    let
+	val (xs, ys, zs) = split_list3 xyzs
+    in
+	(x::xs,y::ys,z::zs)
+    end
+
+
+fun build_tree thy f congs (qs, gs, lhs, rhs) =
+    let
+	(* FIXME: Save precomputed dependencies in a theory data slot *)
+	val congs_deps = map (fn c => (c, FundefCtxTree.cong_deps c)) (congs @ FundefCtxTree.add_congs)
+    in
+	FundefCtxTree.mk_tree thy congs_deps f rhs
+    end
+
+
+fun analyze_eqs eqs =
+    let
+	fun dest_geq geq = 
+	    let
+		val qs = add_term_frees (geq, [])
+	    in
+		case dest_implies_list geq of
+		    (gs, Const ("Trueprop", _) $ (Const ("op =", _) $ (f $ lhs) $ rhs)) => 
+		    (f, (qs, gs, lhs, rhs))
+		  | _ => raise ERROR "Not a guarded equation"
+	    end
+			       
+	val (fs, glrs) = split_list (map dest_geq eqs)
+			 
+	val f = (hd fs) (* should be equal and a constant... check! *)
+
+	val used = fold (curry add_term_names) eqs [] (* all names in the eqs *)
+		   (* Must check for recursive calls in guards and new vars in rhss *)
+    in
+	(f, glrs, used)
+    end
+
+
+(* maps (qs,gs,lhs,ths) to (qs',gs',lhs',rhs') with primed variables *)
+fun mk_primed_vars thy glrs =
+    let
+	val used = fold (fn (qs,_,_,_) => fold ((insert op =) o fst o dest_Free) qs) glrs []
+
+	fun rename_vars (qs,gs,lhs,rhs) =
+	    let
+		val qs' = map (fn Free (v,T) => Free (variant used (v ^ "'"),T)) qs
+		val rename_vars = Pattern.rewrite_term thy (qs ~~ qs') []
+	    in
+		(qs', map rename_vars gs, rename_vars lhs, rename_vars rhs)
+	    end
+    in
+	map rename_vars glrs
+    end
+
+
+fun mk_clause_info thy (names:naming_context) (no, (qs,gs,lhs,rhs)) (GI,tree) RIs =
+    let
+	val {domT, G, R, h, f, fvar, used, x, ...} = names
+				 
+	val zv = Var (("z",0), domT) (* for generating h_assums *)
+	val xv = Var (("x",0), domT)
+	val rw_RI_to_h_assum = (mk_mem (mk_prod (zv, xv), R),
+				mk_mem (mk_prod (zv, h $ zv), G))
+	val rw_f_to_h = (f, h)
+			
+	val cqs = map (cterm_of thy) qs
+		  
+	val vqs = map free_to_var qs
+	val cvqs = map (cterm_of thy) vqs
+
+	val ags = map (assume o cterm_of thy) gs
+		  
+	val qs' = map (fn Free (v,T) => Free (variant used (v ^ "'"),T)) qs
+	val cqs' = map (cterm_of thy) qs'
+
+	val rename_vars = Pattern.rewrite_term thy (qs ~~ qs') []
+	val ags' = map (assume o cterm_of thy o rename_vars) gs
+	val lhs' = rename_vars lhs
+	val rhs' = rename_vars rhs
+
+	val localize = instantiate ([], cvqs ~~ cqs) 
+					   #> fold implies_elim_swp ags
+
+	val GI = freezeT GI
+	val lGI = localize GI
+
+	val ordcqs' = map (cterm_of thy o Pattern.rewrite_term thy ((fvar,h)::(qs ~~ qs')) [] o var_to_free) (term_vars (prop_of GI))
+			  
+	fun mk_call_info (RIvs, RI) =
+	    let
+		fun mk_var0 (v,T) = Var ((v,0),T)
+
+		val RI = freezeT RI
+		val lRI = localize RI
+		val lRIq = fold_rev (forall_intr o cterm_of thy o mk_var0) RIvs lRI
+			  
+		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
+		{RI=RI, RIvs=RIvs, lRI=lRI, lRIq=lRIq, Gh=Gh, Gh'=Gh'}
+	    end
+
+	val case_hyp = assume (cterm_of thy (Trueprop (mk_eq (x, lhs))))
+    in
+	{
+	 no=no,
+	 qs=qs, gs=gs, lhs=lhs, rhs=rhs,		 
+	 cqs=cqs, cvqs=cvqs, ags=ags,		 
+	 cqs'=cqs', ags'=ags', lhs'=lhs', rhs'=rhs', ordcqs' = ordcqs',
+	 GI=GI, lGI=lGI, RCs=map mk_call_info RIs,
+	 tree=tree, case_hyp = case_hyp
+	}
+    end
+
+
+
+
+(* 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 =
+    let
+	val trees = map (build_tree thy f congs) glrs
+	val allused = fold FundefCtxTree.add_context_varnames trees used
+
+	val Const (f_proper_name, fT) = f
+	val fxname = Sign.extern_const thy f_proper_name
+
+	val domT = domain_type fT 
+	val ranT = range_type fT
+
+	val h = Free (variant allused "h", domT --> ranT)
+	val y = Free (variant allused "y", ranT)
+	val x = Free (variant allused "x", domT)
+	val z = Free (variant allused "z", domT)
+	val a = Free (variant allused "a", domT)
+	val D = Free (variant allused "D", HOLogic.mk_setT domT)
+	val P = Free (variant allused "P", domT --> boolT)
+	val Pbool = Free (variant allused "P", boolT)
+	val fvarname = variant allused "f"
+	val fvar = Free (fvarname, domT --> ranT)
+
+	val GT = mk_relT (domT, ranT)
+	val RT = mk_relT (domT, domT)
+	val G_name = fname ^ "_graph"
+	val R_name = fname ^ "_rel"
+
+	val glrs' = mk_primed_vars thy glrs
+
+	val thy = Sign.add_consts_i [(G_name, GT, NoSyn), (R_name, RT, NoSyn)] thy
+
+	val G = Const (Sign.intern_const thy G_name, GT)
+	val R = Const (Sign.intern_const thy R_name, RT)
+	val acc_R = Const (acc_const_name, (fastype_of R) --> HOLogic.mk_setT domT) $ R
+
+	val f_eq = Logic.mk_equals (f $ x, 
+				    Const ("The", (ranT --> boolT) --> ranT) $
+					  Abs ("y", ranT, mk_relmemT domT ranT (x, Bound 0) G))
+
+	val ([f_def], thy) = PureThy.add_defs_i false [((fxname ^ "_def", f_eq), [])] thy
+    in
+	({f=f, glrs=glrs, glrs'=glrs', fvar=fvar, fvarname=fvarname, domT=domT, ranT=ranT, G=G, R=R, acc_R=acc_R, h=h, x=x, y=y, z=z, a=a, D=D, P=P, Pbool=Pbool, f_def=f_def, used=allused, trees=trees}, thy)
+    end
+
+
+(* Gs ==> Gs' ==> lhs = lhs' ==> rhs = rhs' *)
+fun mk_compat_impl ((qs, gs, lhs, rhs),(qs', gs', lhs', rhs')) =
+    (implies $ Trueprop (mk_eq (lhs, lhs'))
+	     $ Trueprop (mk_eq (rhs, rhs')))
+	|> fold_rev (curry Logic.mk_implies) (gs @ gs')
+
+
+(* all proof obligations *)
+fun mk_compat_proof_obligations glrs glrs' =
+    map (fn ((x,_), (_,y')) => mk_compat_impl (x,y')) (upairs (glrs ~~ glrs'))
+
+
+fun extract_Ris thy congs f R tree (qs, gs, lhs, rhs) =
+    let
+	fun add_Ri2 (fixes,assumes) (_ $ arg) _ (_, x) = ([], (FundefCtxTree.export_term (fixes, map prop_of assumes) (mk_relmem (arg, lhs) R)) :: x)
+	  | add_Ri2 _ _ _ _ = raise Match
+
+	val preRis = rev (FundefCtxTree.traverse_tree add_Ri2 tree [])
+	val (vRis, preRis_unq) = split_list (map dest_all_all preRis)
+
+	val Ris = map (fold_rev (curry Logic.mk_implies) gs) preRis_unq
+    in
+	(map (map dest_Free) vRis, preRis, Ris)
+    end
+
+fun mk_GIntro thy names (qs, gs, lhs, rhs) Ris =
+    let
+	val { domT, R, G, f, fvar, h, y, Pbool, ... } = names
+
+	val z = Var (("z",0), domT)
+	val x = Var (("x",0), domT)
+
+	val rew1 = (mk_mem (mk_prod (z, x), R),
+		    mk_mem (mk_prod (z, fvar $ z), G))
+	val rew2 = (f, fvar)
+
+	val prems = map (Pattern.rewrite_term thy [rew1, rew2] []) Ris
+	val rhs' = Pattern.rewrite_term thy [rew2] [] rhs 
+    in
+	mk_relmem (lhs, rhs') G
+		  |> fold_rev (curry Logic.mk_implies) prems
+		  |> fold_rev (curry Logic.mk_implies) gs
+    end
+
+fun mk_completeness names glrs =
+    let
+	val {domT, x, Pbool, ...} = names
+
+	fun mk_case (qs, gs, lhs, _) = Trueprop Pbool
+						|> curry Logic.mk_implies (Trueprop (mk_eq (x, lhs)))
+						|> fold_rev (curry Logic.mk_implies) gs
+						|> fold_rev mk_forall qs
+    in
+	Trueprop Pbool
+		 |> fold_rev (curry Logic.mk_implies o mk_case) glrs
+    end
+
+
+fun extract_conditions thy names trees congs =
+    let
+	val {f, G, R, acc_R, domT, ranT, f_def, x, z, fvarname, glrs, glrs', ...} = names
+
+	val (vRiss, preRiss, Riss) = split_list3 (map2 (extract_Ris thy congs f R) trees glrs)
+	val Gis = map2 (mk_GIntro thy names) glrs preRiss
+	val complete = mk_completeness names glrs
+	val compat = mk_compat_proof_obligations glrs glrs'
+    in
+	{G_intros = Gis, vRiss = vRiss, R_intross = Riss, complete = complete, compat = compat}
+    end
+
+
+fun inductive_def defs (thy, const) =
+    let
+ 	val (thy, {intrs, elims = [elim], ...}) = 
+	    InductivePackage.add_inductive_i true (*verbose*)
+					     false (*add_consts*)
+					     "" (* no altname *)
+					     false (* no coind *)
+					     false (* elims, please *)
+					     false (* induction thm please *)
+					     [const] (* the constant *)
+					     (map (fn t=>(("", t),[])) defs) (* the intros *)
+					     [] (* no special monos *)
+					     thy
+    in
+	(intrs, (thy, elim))
+    end
+
+
+
+(*
+ * This is the first step in a function definition.
+ *
+ * Defines the function, the graph and the termination relation, synthesizes completeness
+ * and comatibility conditions and returns everything.
+ *)
+fun prepare_fundef congs eqs fname thy =
+    let
+	val (names, thy) = setup_context (analyze_eqs eqs) fname congs thy
+	val {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
+	({names = names, complete=complete, compat=compat, clauses = clauses},
+	 thy) 
+    end
+
+
+
+
+fun prepare_fundef_curried congs eqs thy =
+    let
+	val lhs1 = hd eqs
+		   |> dest_implies_list |> snd
+		   |> HOLogic.dest_Trueprop
+		   |> HOLogic.dest_eq |> fst
+
+	val (f, args) = strip_comb lhs1
+	val Const(fname, fT) = f
+	val fxname = Sign.extern_const thy fname
+    in
+	if (length args < 2)
+	then (NONE, fxname, (prepare_fundef congs eqs fxname thy))
+	else
+	    let
+		val (caTs, uaTs) = chop (length args) (binder_types fT)
+		val newtype = foldr1 HOLogic.mk_prodT caTs --> (uaTs ---> body_type fT)
+		val gxname = fxname ^ "_tupled"
+			     
+    		val thy = Sign.add_consts_i [(gxname, newtype, NoSyn)] thy
+		val gc = Const (Sign.intern_const thy gxname, newtype)
+			 
+		val vars = map2 (fn i => fn T => Free ("x"^(string_of_int i), T))
+				(1 upto (length caTs)) caTs
+
+		val f_lambda = fold_rev lambda vars (gc $ foldr1 HOLogic.mk_prod vars)
+			       
+		val def = Logic.mk_equals (fold (curry ((op $) o Library.swap)) vars f,
+					   gc $ foldr1 HOLogic.mk_prod vars)
+			  
+		val ([f_def], thy) = PureThy.add_defs_i false [((fxname ^ "_def", def), [])] thy
+				      
+		val g_to_f_ss = HOL_basic_ss addsimps [symmetric f_def]
+		val eqs_tupled = map (Pattern.rewrite_term thy [(f, f_lambda)] []) eqs
+	    in
+		(SOME {curry_ss = g_to_f_ss, argTs = caTs}, fxname, prepare_fundef congs eqs_tupled fxname thy)
+	    end
+    end
+
+
+
+end
\ No newline at end of file
diff -r ddd36d9e6943 -r d3e2f532459a src/HOL/Tools/function_package/fundef_proof.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/function_package/fundef_proof.ML	Fri May 05 17:17:21 2006 +0200
@@ -0,0 +1,585 @@
+(*  Title:      HOL/Tools/function_package/fundef_proof.ML
+    ID:         $Id$
+    Author:     Alexander Krauss, TU Muenchen
+
+A package for general recursive function definitions. 
+Internal proofs.
+*)
+
+
+signature FUNDEF_PROOF =
+sig
+
+    val mk_partial_rules_curried : theory -> thm list -> FundefCommon.curry_info option -> FundefCommon.prep_result 
+				   -> thm -> thm list -> FundefCommon.fundef_result
+end
+
+
+structure FundefProof : FUNDEF_PROOF = 
+struct
+
+open FundefCommon
+open FundefAbbrev
+
+(* Theory dependencies *)
+val subsetD = thm "subsetD"
+val subset_refl = thm "subset_refl"
+val split_apply = thm "Product_Type.split"
+val wf_induct_rule = thm "wf_induct_rule";
+val Pair_inject = thm "Product_Type.Pair_inject";
+
+val acc_induct_rule = thm "acc_induct_rule" (* from: Accessible_Part *)
+val acc_downward = thm "acc_downward"
+val accI = thm "accI"
+
+val ex1_implies_ex = thm "fundef_ex1_existence"   (* from: Fundef.thy *) 
+val ex1_implies_un = thm "fundef_ex1_uniqueness"
+val ex1_implies_iff = thm "fundef_ex1_iff"
+val acc_subset_induct = thm "acc_subset_induct"
+
+
+
+
+
+    
+fun mk_simp thy (names:naming_context) f_iff graph_is_function clause valthm =
+    let
+	val {R, acc_R, domT, z, ...} = names
+	val {qs, cqs, gs, lhs, rhs, ...} = clause
+	val lhs_acc = cterm_of thy (Trueprop (mk_mem (lhs, acc_R))) (* "lhs : acc R" *)
+	val z_smaller = cterm_of thy (Trueprop (mk_relmemT domT domT (z, lhs) R)) (* "(z, lhs) : R" *)
+    in
+	((assume z_smaller) RS ((assume lhs_acc) RS acc_downward))
+	    |> (fn it => it COMP graph_is_function)
+	    |> implies_intr z_smaller
+	    |> forall_intr (cterm_of thy z)
+	    |> (fn it => it COMP valthm)
+	    |> implies_intr lhs_acc 
+	    |> asm_simplify (HOL_basic_ss addsimps [f_iff])
+	    |> fold forall_intr cqs
+	    |> forall_elim_vars 0
+	    |> varifyT
+	    |> Drule.close_derivation
+    end
+
+
+
+
+fun mk_partial_induct_rule thy (names:naming_context) complete_thm clauses =
+    let
+	val {domT, R, acc_R, x, z, a, P, D, ...} = names
+
+	val x_D = assume (cterm_of thy (Trueprop (mk_mem (x, D))))
+	val a_D = cterm_of thy (Trueprop (mk_mem (a, D)))
+
+	val D_subset = cterm_of thy (Trueprop (mk_subset domT D acc_R))
+
+	val D_dcl = (* "!!x z. [| x: D; (z,x):R |] ==> z:D" *)
+	    mk_forall x
+		      (mk_forall z (Logic.mk_implies (Trueprop (mk_mem (x, D)),
+						      Logic.mk_implies (mk_relmem (z, x) R,
+									Trueprop (mk_mem (z, D))))))
+		      |> cterm_of thy
+
+
+	(* Inductive Hypothesis: !!z. (z,x):R ==> P z *)
+	val ihyp = all domT $ Abs ("z", domT, 
+				   implies $ Trueprop (mk_relmemT domT domT (Bound 0, x) R)
+					   $ Trueprop (P $ Bound 0))
+		       |> cterm_of thy
+
+	val aihyp = assume ihyp |> forall_elim_vars 0
+
+	fun prove_case clause =
+	    let
+		val {qs, cqs, ags, gs, lhs, rhs, case_hyp, RCs, ...} = clause
+								       
+		val replace_x_ss = HOL_basic_ss addsimps [case_hyp]
+		val lhs_D = simplify replace_x_ss x_D (* lhs : D *)
+		val sih = full_simplify replace_x_ss aihyp
+					
+					(* FIXME: Variable order destroyed by forall_intr_vars *)
+		val P_recs = map (fn {lRI, RIvs, ...} => (lRI RS sih) |> forall_intr_vars) RCs   (*  [P rec1, P rec2, ... ]  *)
+			     
+		val step = Trueprop (P $ lhs)
+				    |> fold_rev (curry Logic.mk_implies o prop_of) P_recs
+				    |> fold_rev (curry Logic.mk_implies) gs
+				    |> curry Logic.mk_implies (Trueprop (mk_mem (lhs, D)))
+				    |> fold_rev mk_forall qs
+				    |> cterm_of thy
+			   
+		val P_lhs = assume step
+				   |> fold forall_elim cqs
+				   |> implies_elim_swp lhs_D 
+				   |> fold_rev implies_elim_swp ags
+				   |> fold implies_elim_swp P_recs
+			    
+		val res = cterm_of thy (Trueprop (P $ x))
+				   |> Simplifier.rewrite replace_x_ss
+				   |> symmetric (* P lhs == P x *)
+				   |> (fn eql => equal_elim eql P_lhs) (* "P x" *)
+				   |> implies_intr (cprop_of case_hyp)
+				   |> fold_rev (implies_intr o cprop_of) ags
+				   |> fold_rev forall_intr cqs
+	    in
+		(res, step)
+	    end
+
+	val (cases, steps) = split_list (map prove_case clauses)
+
+	val istep =  complete_thm
+			 |> fold (curry op COMP) cases (*  P x  *)
+			 |> implies_intr ihyp
+			 |> implies_intr (cprop_of x_D)
+			 |> forall_intr (cterm_of thy x)
+			   
+	val subset_induct_rule = 
+	    acc_subset_induct
+		|> (curry op COMP) (assume D_subset)
+		|> (curry op COMP) (assume D_dcl)
+		|> (curry op COMP) (assume a_D)
+		|> (curry op COMP) istep
+		|> fold_rev implies_intr steps
+		|> implies_intr a_D
+		|> implies_intr D_dcl
+		|> implies_intr D_subset
+		|> forall_intr_frees
+		|> forall_elim_vars 0
+
+	val simple_induct_rule =
+	    subset_induct_rule
+		|> instantiate' [] [SOME (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))
+    in
+	(varifyT subset_induct_rule, varifyT simple_induct_rule)
+    end
+
+
+
+
+
+(***********************************************)
+(* Compat thms are stored in normal form (with vars) *)
+
+(* replace this by a table later*)
+fun store_compat_thms 0 cts = []
+  | store_compat_thms n cts =
+    let
+	val (cts1, cts2) = chop n cts
+    in
+	(cts1 :: store_compat_thms (n - 1) cts2)
+    end
+
+
+(* needs i <= j *)
+fun lookup_compat_thm i j cts =
+    nth (nth cts (i - 1)) (j - i)
+(***********************************************)
+
+
+(* recover the order of Vars *)
+fun get_var_order thy (clauses: clause_info list) =
+    map (fn ({cqs,...}, {cqs',...}) => map (cterm_of thy o free_to_var o term_of) (cqs @ cqs')) (upairs clauses)
+
+
+(* Returns "Gsi, Gsj', lhs_i = lhs_j' |-- rhs_j'_f = rhs_i_f" *)
+(* if j < i, then turn around *)
+fun get_compat_thm thy cts clausei clausej =
+    let 
+	val {no=i, cqs=qsi, ags=gsi, lhs=lhsi, ...} = clausei
+	val {no=j, cqs'=qsj', ags'=gsj', lhs'=lhsj', ...} = clausej
+
+	val lhsi_eq_lhsj' = cterm_of thy (Trueprop (mk_eq (lhsi, lhsj')))
+    in if j < i then
+	   let 
+	       val (var_ord, compat) = lookup_compat_thm j i cts
+	   in
+	       compat         (* "!!qj qi'. Gsj => Gsi' => lhsj = lhsi' ==> rhsj = rhsi'" *)
+		|> instantiate ([],(var_ord ~~ (qsj' @ qsi))) (* "Gsj' => Gsi => lhsj' = lhsi ==> rhsj' = rhsi" *)
+		|> fold implies_elim_swp gsj'
+		|> fold implies_elim_swp gsi
+		|> implies_elim_swp ((assume lhsi_eq_lhsj') RS sym) (* "Gsj', Gsi, lhsi = lhsj' |-- rhsj' = rhsi" *)
+	   end
+       else
+	   let
+	       val (var_ord, compat) = lookup_compat_thm i j cts
+	   in
+	       compat        (* "?Gsi => ?Gsj' => ?lhsi = ?lhsj' ==> ?rhsi = ?rhsj'" *)
+	         |> instantiate ([], (var_ord ~~ (qsi @ qsj'))) (* "Gsi => Gsj' => lhsi = lhsj' ==> rhsi = rhsj'" *)
+		 |> fold implies_elim_swp gsi
+		 |> fold implies_elim_swp gsj'
+		 |> implies_elim_swp (assume lhsi_eq_lhsj')
+		 |> (fn thm => thm RS sym) (* "Gsi, Gsj', lhsi = lhsj' |-- rhsj' = rhsi" *)
+	   end
+    end
+
+
+
+
+
+(* Generates the replacement lemma with primed variables. A problem here is that one should not do
+the complete requantification at the end to replace the variables. One should find a way to be more efficient
+here. *)
+fun mk_replacement_lemma thy (names:naming_context) ih_elim clause = 
+    let 
+	val {fvar, f, x, y, h, Pbool, G, ranT, domT, R, ...} = names 
+	val {qs,cqs,ags,lhs,rhs,cqs',ags',case_hyp, RCs, tree, ...} = clause
+
+	val ih_elim_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_elim
+
+	val Ris = map #lRIq RCs
+	val h_assums = map #Gh RCs
+	val h_assums' = map #Gh' RCs
+
+	val ih_elim_case_inst = instantiate' [] [NONE, SOME (cterm_of thy h)] ih_elim_case (* Should be done globally *)
+
+	val (eql, _) = FundefCtxTree.rewrite_by_tree thy f h ih_elim_case_inst (Ris ~~ h_assums) tree
+
+	val replace_lemma = (eql RS meta_eq_to_obj_eq)
+				|> implies_intr (cprop_of case_hyp)
+				|> fold_rev (implies_intr o cprop_of) h_assums
+				|> fold_rev (implies_intr o cprop_of) ags
+				|> fold_rev forall_intr cqs
+				|> fold forall_elim cqs'
+				|> fold implies_elim_swp ags'
+				|> fold implies_elim_swp h_assums'
+    in
+	replace_lemma
+    end
+
+
+
+
+fun mk_uniqueness_clause thy (names:naming_context) compat_store (clausei:clause_info) (clausej:clause_info) RLj =
+    let
+	val {f, h, y, ...} = names
+	val {no=i, lhs=lhsi, case_hyp, ...} = clausei
+	val {no=j, ags'=gsj', lhs'=lhsj', rhs'=rhsj', RCs=RCsj, ordcqs'=ordcqs'j, ...} = clausej
+
+	val rhsj'h = Pattern.rewrite_term thy [(f,h)] [] rhsj'
+	val compat = get_compat_thm thy compat_store clausei clausej
+	val Ghsj' = map (fn {Gh', ...} => Gh') RCsj
+
+	val y_eq_rhsj'h = assume (cterm_of thy (Trueprop (mk_eq (y, rhsj'h))))
+	val lhsi_eq_lhsj' = assume (cterm_of thy (Trueprop (mk_eq (lhsi, lhsj')))) (* lhs_i = lhs_j' |-- lhs_i = lhs_j'	*)
+
+	val eq_pairs = assume (cterm_of thy (Trueprop (mk_eq (mk_prod (lhsi, y), mk_prod (lhsj',rhsj'h)))))
+    in
+	(trans OF [case_hyp, lhsi_eq_lhsj']) (* lhs_i = lhs_j' |-- x = lhs_j' *)
+        |> implies_elim RLj (* Rj1' ... Rjk', lhs_i = lhs_j' |-- rhs_j'_h = rhs_j'_f *)
+	|> (fn it => trans OF [it, compat]) (* lhs_i = lhs_j', Gj', Rj1' ... Rjk' |-- rhs_j'_h = rhs_i_f *)
+	|> (fn it => trans OF [y_eq_rhsj'h, it]) (* lhs_i = lhs_j', Gj', Rj1' ... Rjk', y = rhs_j_h' |-- y = rhs_i_f *)
+	|> implies_intr (cprop_of y_eq_rhsj'h)
+	|> implies_intr (cprop_of lhsi_eq_lhsj') (* Gj', Rj1' ... Rjk' |-- [| lhs_i = lhs_j', y = rhs_j_h' |] ==> y = rhs_i_f *)
+	|> (fn it => Drule.compose_single(it, 2, Pair_inject)) (* Gj', Rj1' ... Rjk' |-- (lhs_i, y) = (lhs_j', rhs_j_h') ==> y = rhs_i_f *)
+	|> implies_elim_swp eq_pairs
+	|> fold_rev (implies_intr o cprop_of) Ghsj' 
+	|> fold_rev (implies_intr o cprop_of) gsj' (* Gj', Rj1', ..., Rjk' ==> (lhs_i, y) = (lhs_j', rhs_j_h') ==> y = rhs_i_f *)
+	|> implies_intr (cprop_of eq_pairs)
+	|> fold_rev forall_intr ordcqs'j
+    end
+
+
+
+fun mk_uniqueness_case thy (names:naming_context) ihyp ih_intro G_cases compat_store clauses rep_lemmas (clausei:clause_info) =
+    let
+	val {x, y, G, fvar, f, ranT, ...} = names
+	val {lhs, rhs, qs, cqs, ags, case_hyp, lGI, RCs, ...} = clausei
+
+	val ih_intro_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_intro
+
+	fun prep_RC ({lRIq,RIvs, ...} : rec_call_info) = lRIq
+							     |> fold (forall_elim o cterm_of thy o Free) RIvs
+							     |> (fn it => it RS ih_intro_case)
+							     |> fold_rev (forall_intr o cterm_of thy o Free) RIvs
+
+	val existence = lGI |> instantiate ([], [(cterm_of thy (free_to_var fvar), cterm_of thy f)])
+			    |> fold (curry op COMP o prep_RC) RCs 
+
+
+	val a = cterm_of thy (mk_prod (lhs, y))
+	val P = cterm_of thy (mk_eq (y, rhs))
+	val a_in_G = assume (cterm_of thy (Trueprop (mk_mem (term_of a, G))))
+
+	val unique_clauses = map2 (mk_uniqueness_clause thy names compat_store clausei) clauses rep_lemmas
+
+	val uniqueness = G_cases 
+			     |> instantiate' [] [SOME a, SOME P]
+			     |> implies_elim_swp a_in_G
+			     |> fold implies_elim_swp unique_clauses
+			     |> implies_intr (cprop_of a_in_G)
+			     |> forall_intr (cterm_of thy y) 
+
+	val P2 = cterm_of thy (lambda y (mk_mem (mk_prod (lhs, y), G))) (* P2 y := (lhs, y): G *)
+
+	val exactly_one =
+	    ex1I |> instantiate' [SOME (ctyp_of thy ranT)] [SOME P2, SOME (cterm_of thy rhs)]
+		 |> curry (op COMP) existence
+		 |> curry (op COMP) uniqueness
+		 |> simplify (HOL_basic_ss addsimps [case_hyp RS sym])
+		 |> implies_intr (cprop_of case_hyp) 
+		 |> fold_rev (implies_intr o cprop_of) ags
+		 |> fold_rev forall_intr cqs
+	val function_value =
+	    existence 
+		|> fold_rev (implies_intr o cprop_of) ags
+		|> implies_intr ihyp
+		|> implies_intr (cprop_of case_hyp)
+		|> forall_intr (cterm_of thy x)
+		|> forall_elim (cterm_of thy lhs)
+		|> curry (op RS) refl
+    in
+	(exactly_one, function_value)
+    end
+
+
+
+(* Does this work with Guards??? *)
+fun mk_domain_intro thy (names:naming_context) R_cases clause =
+    let
+	val {z, R, acc_R, ...} = names
+	val {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
+		  |> Goal.conclude
+		  |> forall_intr_frees
+		  |> forall_elim_vars 0
+		  |> varifyT
+    end
+
+
+
+
+fun mk_nest_term_case thy (names:naming_context) R' ihyp clause =
+    let
+	val {x, z, ...} = names
+	val {qs,cqs,ags,lhs,rhs,tree,case_hyp,...} = clause
+
+	val ih_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ihyp
+
+	fun step (fixes, assumes) (_ $ arg) u (sub,(hyps,thms)) = 
+	    let
+		val used = map (fn ((f,a),thm) => FundefCtxTree.export_thm thy (f, map prop_of a) thm) (u @ sub)
+
+		val hyp = mk_relmem (arg, lhs) R'
+				    |> fold_rev (curry Logic.mk_implies o prop_of) used
+				    |> FundefCtxTree.export_term (fixes, map prop_of assumes) 
+				    |> fold_rev (curry Logic.mk_implies o prop_of) ags
+				    |> fold_rev mk_forall qs
+				    |> cterm_of thy
+
+		val thm = assume hyp
+				 |> fold forall_elim cqs
+				 |> fold implies_elim_swp ags
+				 |> FundefCtxTree.import_thm thy (fixes, assumes) (*  "(arg, lhs) : R'"  *)
+				 |> fold implies_elim_swp used
+
+		val acc = thm COMP ih_case
+
+		val z_eq_arg = cterm_of thy (Trueprop (HOLogic.mk_eq (z, arg)))
+
+		val arg_eq_z = (assume z_eq_arg) RS sym
+
+		val z_acc = simplify (HOL_basic_ss addsimps [arg_eq_z]) acc (* fragile, slow... *)
+				     |> implies_intr (cprop_of case_hyp)
+				     |> implies_intr z_eq_arg
+
+		val zx_eq_arg_lhs = cterm_of thy (Trueprop (mk_eq (mk_prod (z,x), mk_prod (arg,lhs))))
+
+		val z_acc' = z_acc COMP (assume zx_eq_arg_lhs COMP Pair_inject)
+
+		val ethm = z_acc'
+			       |> FundefCtxTree.export_thm thy (fixes, (term_of zx_eq_arg_lhs) :: map prop_of (ags @ assumes))
+			       |> fold_rev forall_intr cqs
+
+
+		val sub' = sub @ [(([],[]), acc)]
+	    in
+		(sub', (hyp :: hyps, ethm :: thms))
+	    end
+	  | step _ _ _ _ = raise Match
+    in
+	FundefCtxTree.traverse_tree step tree
+    end
+
+
+fun mk_nest_term_rule thy (names:naming_context) clauses =
+    let
+	val { R, acc_R, domT, x, z, ... } = names
+
+	val R_elim = hd (#elims (snd (the (InductivePackage.get_inductive thy (fst (dest_Const R))))))
+
+	val R' = Free ("R", fastype_of R)
+
+	val wfR' = cterm_of thy (Trueprop (Const ("Wellfounded_Recursion.wf", mk_relT (domT, domT) --> boolT) $ R')) (* "wf R'" *)
+
+	(* Inductive Hypothesis: !!z. (z,x):R' ==> z : acc R *)
+	val ihyp = all domT $ Abs ("z", domT, 
+				   implies $ Trueprop (mk_relmemT domT domT (Bound 0, x) R')
+					   $ Trueprop ((Const ("op :", [domT, HOLogic.mk_setT domT] ---> boolT))
+							   $ Bound 0 $ acc_R))
+		       |> cterm_of thy
+
+	val ihyp_a = assume ihyp |> forall_elim_vars 0
+
+	val z_ltR_x = cterm_of thy (mk_relmem (z, x) R) (* "(z, x) : R" *)
+	val z_acc = cterm_of thy (mk_mem (z, acc_R))
+
+	val (hyps,cases) = fold (mk_nest_term_case thy names R' ihyp_a) clauses ([],[])
+    in
+	R_elim
+	    |> freezeT
+	    |> instantiate' [] [SOME (cterm_of thy (mk_prod (z,x))), SOME z_acc]
+	    |> curry op COMP (assume z_ltR_x)
+	    |> fold_rev (curry op COMP) cases
+	    |> implies_intr z_ltR_x
+	    |> forall_intr (cterm_of thy z)
+	    |> (fn it => it COMP accI)
+	    |> implies_intr ihyp
+	    |> forall_intr (cterm_of thy x)
+	    |> (fn it => Drule.compose_single(it,2,wf_induct_rule))
+	    |> implies_elim_swp (assume wfR')
+	    |> fold implies_intr hyps
+	    |> implies_intr wfR'
+	    |> forall_intr (cterm_of thy R')
+	    |> forall_elim_vars 0
+	    |> varifyT
+    end
+
+
+
+
+fun mk_partial_rules thy congs data complete_thm compat_thms =
+    let
+	val {names, clauses, complete, compat, ...} = data
+	val {G, R, acc_R, domT, ranT, f, f_def, x, z, fvarname, ...}:naming_context = names
+
+(*	val _ = Output.debug "closing derivation: completeness"
+	val _ = Output.debug (Proofterm.size_of_proof (proof_of complete_thm))
+	val _ = Output.debug (map (Proofterm.size_of_proof o proof_of) compat_thms)*)
+	val complete_thm = Drule.close_derivation complete_thm
+(*	val _ = Output.debug "closing derivation: compatibility"*)
+	val compat_thms = map Drule.close_derivation compat_thms
+(*	val _ = Output.debug "  done"*)
+
+	val complete_thm_fr = freezeT complete_thm
+	val compat_thms_fr = map freezeT compat_thms
+	val f_def_fr = freezeT f_def
+
+	val instantiate_and_def = (instantiate' [SOME (ctyp_of thy domT), SOME (ctyp_of thy ranT)] 
+						[SOME (cterm_of thy f), SOME (cterm_of thy G)])
+				      #> curry op COMP (forall_intr_vars f_def_fr)
+			  
+	val inst_ex1_ex = instantiate_and_def ex1_implies_ex
+	val inst_ex1_un = instantiate_and_def ex1_implies_un
+	val inst_ex1_iff = instantiate_and_def ex1_implies_iff
+
+	(* Inductive Hypothesis: !!z. (z,x):R ==> EX!y. (z,y):G *)
+	val ihyp = all domT $ Abs ("z", domT, 
+				   implies $ Trueprop (mk_relmemT domT domT (Bound 0, x) R)
+					   $ Trueprop (Const ("Ex1", (ranT --> boolT) --> boolT) $
+							     Abs ("y", ranT, mk_relmemT domT ranT (Bound 1, Bound 0) G)))
+		       |> cterm_of thy
+		   
+	val ihyp_thm = assume ihyp
+			      |> forall_elim_vars 0
+		       
+	val ih_intro = ihyp_thm RS inst_ex1_ex
+	val ih_elim = ihyp_thm RS inst_ex1_un
+
+	val _ = Output.debug "Proving Replacement lemmas..."
+	val repLemmas = map (mk_replacement_lemma thy names ih_elim) clauses
+
+	val n = length clauses
+	val var_order = get_var_order thy clauses
+	val compat_store = store_compat_thms n (var_order ~~ compat_thms_fr)
+
+	val R_cases = hd (#elims (snd (the (InductivePackage.get_inductive thy (fst (dest_Const R)))))) |> freezeT
+	val G_cases = hd (#elims (snd (the (InductivePackage.get_inductive thy (fst (dest_Const G)))))) |> freezeT
+
+	val _ = Output.debug "Proving cases for unique existence..."
+	val (ex1s, values) = split_list (map (mk_uniqueness_case thy names ihyp ih_intro G_cases compat_store clauses repLemmas) clauses)
+
+	val _ = Output.debug "Proving: Graph is a function"
+	val graph_is_function = complete_thm_fr
+				    |> fold (curry op COMP) ex1s
+				    |> implies_intr (ihyp)
+				    |> implies_intr (cterm_of thy (Trueprop (mk_mem (x, acc_R))))
+				    |> forall_intr (cterm_of thy x)
+				    |> (fn it => Drule.compose_single (it, 2, acc_induct_rule)) (* "EX! y. (?x,y):G" *)
+				    |> Drule.close_derivation
+
+	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 _ = Output.debug "Proving partial induction rule"
+	val (subset_pinduct, simple_pinduct) = mk_partial_induct_rule thy names complete_thm clauses
+
+	val _ = Output.debug "Proving nested termination rule"
+	val total_intro = mk_nest_term_rule thy names clauses
+
+	val _ = Output.debug "Proving domain introduction rules"
+	val dom_intros = map (mk_domain_intro thy names R_cases) clauses
+    in 
+	{f=f, G=G, R=R, compatibility=compat_thms, completeness=complete_thm, 
+	 psimps=psimps, subset_pinduct=subset_pinduct, simple_pinduct=simple_pinduct, total_intro=total_intro,
+	 dom_intros=dom_intros}
+    end
+
+
+fun curry_induct_rule thy argTs induct =
+    let
+	val vnums = (1 upto (length argTs))
+	val avars = map2 (fn T => fn i => Var (("a",i), T)) argTs vnums
+	val atup = foldr1 HOLogic.mk_prod avars
+	val Q = Var (("P",1),argTs ---> HOLogic.boolT)
+	val P = tupled_lambda atup (list_comb (Q, avars))
+    in
+	induct |> freezeT
+	       |> instantiate' [] [SOME (cterm_of thy atup), SOME (cterm_of thy P)]
+	       |> zero_var_indexes
+	       |> full_simplify (HOL_basic_ss addsimps [split_apply])
+	       |> varifyT
+    end
+
+
+
+fun mk_partial_rules_curried thy congs NONE data complete_thm compat_thms =
+    mk_partial_rules thy congs data complete_thm compat_thms 
+  | mk_partial_rules_curried thy congs (SOME {curry_ss, argTs}) data complete_thm compat_thms =
+    let
+	val {f, G, R, compatibility, completeness, psimps, subset_pinduct,simple_pinduct,total_intro,dom_intros} =
+	    mk_partial_rules thy congs data complete_thm compat_thms 
+	val cpsimps = map (simplify curry_ss) psimps
+	val cpinduct = full_simplify curry_ss simple_pinduct
+				     |> curry_induct_rule thy argTs
+	val cdom_intros = map (full_simplify curry_ss) dom_intros
+	val ctotal_intro = full_simplify curry_ss total_intro
+    in
+	{f=f, G=G, R=R, compatibility=compat_thms, completeness=complete_thm, 
+	 psimps=cpsimps, subset_pinduct=subset_pinduct, simple_pinduct=cpinduct, total_intro=ctotal_intro, dom_intros=cdom_intros}
+    end
+
+end
+
+
diff -r ddd36d9e6943 -r d3e2f532459a src/HOL/Tools/function_package/termination.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/function_package/termination.ML	Fri May 05 17:17:21 2006 +0200
@@ -0,0 +1,67 @@
+(*  Title:      HOL/Tools/function_package/termination.ML
+    ID:         $Id$
+    Author:     Alexander Krauss, TU Muenchen
+
+A package for general recursive function definitions. 
+Termination goals...
+*)
+
+
+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
+end
+
+structure FundefTermination : FUNDEF_TERMINATION =
+struct
+
+
+open FundefCommon
+open FundefAbbrev
+
+fun mk_total_termination_goal (data: fundef_result) =
+    let
+	val {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: fundef_result) dom =
+    let
+	val {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
+	val idomT = HOLogic.dest_setT DT
+
+	val x = Free ("x", idomT)
+	val z = Free ("z", idomT)
+	val Rname = fst (dest_Const R)
+	val iRT = mk_relT (idomT, idomT)
+	val iR = Const (Rname, iRT)
+		
+
+	val subs = HOLogic.mk_Trueprop 
+			 (Const ("Orderings.less_eq", DT --> DT --> boolT) $ D $
+				(Const (acc_const_name, iRT --> DT) $ iR))
+			 |> Type.freeze
+
+	val dcl = mk_forall x
+			    (mk_forall z (Logic.mk_implies (Trueprop (HOLogic.mk_mem (x, D)),
+							    Logic.mk_implies (mk_relmem (z, x) iR,
+									      Trueprop (mk_mem (z, D))))))
+			    |> Type.freeze
+    in
+	(subs, dcl)
+    end
+
+end
+
+
+
+
diff -r ddd36d9e6943 -r d3e2f532459a src/HOL/Tools/recdef_package.ML
--- a/src/HOL/Tools/recdef_package.ML	Fri May 05 16:50:58 2006 +0200
+++ b/src/HOL/Tools/recdef_package.ML	Fri May 05 17:17:21 2006 +0200
@@ -30,7 +30,7 @@
   val recdef_tc_i: bstring * attribute list -> string -> int option -> theory -> Proof.state
   val setup: theory -> theory
 
-(* HACK: This has to be exported, since the new recdef-package uses the same hints *)
+(* HACK: This has to be exported, since the new fundef-package uses the same hints *)
   val get_local_hints: ProofContext.context -> {simps: thm list, congs: (string * thm) list, wfs: thm list}
   val get_global_hints: theory -> {simps: thm list, congs: (string * thm) list, wfs: thm list}
 end;
@@ -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 cong_add cong_del, "declaration of recdef cong 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_wfN, Attrib.add_del_args wf_add wf_del, "declaration of recdef wf rule")];