# HG changeset patch
# User krauss
# Date 1229413567 -3600
# Node ID d41182a8135ccebc6d5fa11e4dd48f2a014830e4
# Parent  5a79ec2fedfbf29fdee8746df926dc49c6b39895
method "sizechange" proves termination of functions; added more infrastructure for termination proofs

diff -r 5a79ec2fedfb -r d41182a8135c NEWS
--- a/NEWS	Tue Dec 16 00:19:47 2008 +0100
+++ b/NEWS	Tue Dec 16 08:46:07 2008 +0100
@@ -239,6 +239,9 @@
 mechanisms may be specified (currently, [SML], [code] or [nbe]).  See
 further src/HOL/ex/Eval_Examples.thy.
 
+* New method "sizechange" to automate termination proofs using (a
+modification of) the size-change principle. Requires SAT solver.
+
 * HOL/Orderings: class "wellorder" moved here, with explicit induction
 rule "less_induct" as assumption.  For instantiation of "wellorder" by
 means of predicate "wf", use rule wf_wellorderI.  INCOMPATIBILITY.
diff -r 5a79ec2fedfb -r d41182a8135c src/HOL/FunDef.thy
--- a/src/HOL/FunDef.thy	Tue Dec 16 00:19:47 2008 +0100
+++ b/src/HOL/FunDef.thy	Tue Dec 16 08:46:07 2008 +0100
@@ -3,11 +3,13 @@
     Author:     Alexander Krauss, TU Muenchen
 *)
 
-header {* General recursive function definitions *}
+header {* Function Definitions and Termination Proofs *}
 
 theory FunDef
 imports Wellfounded
 uses
+  "Tools/prop_logic.ML"
+  "Tools/sat_solver.ML"
   ("Tools/function_package/fundef_lib.ML")
   ("Tools/function_package/fundef_common.ML")
   ("Tools/function_package/inductive_wrap.ML")
@@ -22,9 +24,14 @@
   ("Tools/function_package/lexicographic_order.ML")
   ("Tools/function_package/fundef_datatype.ML")
   ("Tools/function_package/induction_scheme.ML")
+  ("Tools/function_package/termination.ML")
+  ("Tools/function_package/decompose.ML")
+  ("Tools/function_package/descent.ML")
+  ("Tools/function_package/scnp_solve.ML")
+  ("Tools/function_package/scnp_reconstruct.ML")
 begin
 
-text {* Definitions with default value. *}
+subsection {* Definitions with default value. *}
 
 definition
   THE_default :: "'a \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a" where
@@ -97,9 +104,6 @@
   "wf R \<Longrightarrow> wfP (in_rel R)"
   by (simp add: wfP_def)
 
-inductive is_measure :: "('a \<Rightarrow> nat) \<Rightarrow> bool"
-where is_measure_trivial: "is_measure f"
-
 use "Tools/function_package/fundef_lib.ML"
 use "Tools/function_package/fundef_common.ML"
 use "Tools/function_package/inductive_wrap.ML"
@@ -110,19 +114,37 @@
 use "Tools/function_package/pattern_split.ML"
 use "Tools/function_package/auto_term.ML"
 use "Tools/function_package/fundef_package.ML"
-use "Tools/function_package/measure_functions.ML"
-use "Tools/function_package/lexicographic_order.ML"
 use "Tools/function_package/fundef_datatype.ML"
 use "Tools/function_package/induction_scheme.ML"
 
 setup {* 
   FundefPackage.setup 
+  #> FundefDatatype.setup
   #> InductionScheme.setup
-  #> MeasureFunctions.setup
-  #> LexicographicOrder.setup 
-  #> FundefDatatype.setup
 *}
 
+subsection {* Measure Functions *}
+
+inductive is_measure :: "('a \<Rightarrow> nat) \<Rightarrow> bool"
+where is_measure_trivial: "is_measure f"
+
+use "Tools/function_package/measure_functions.ML"
+setup MeasureFunctions.setup
+
+lemma measure_size[measure_function]: "is_measure size"
+by (rule is_measure_trivial)
+
+lemma measure_fst[measure_function]: "is_measure f \<Longrightarrow> is_measure (\<lambda>p. f (fst p))"
+by (rule is_measure_trivial)
+lemma measure_snd[measure_function]: "is_measure f \<Longrightarrow> is_measure (\<lambda>p. f (snd p))"
+by (rule is_measure_trivial)
+
+use "Tools/function_package/lexicographic_order.ML"
+setup LexicographicOrder.setup 
+
+
+subsection {* Congruence Rules *}
+
 lemma let_cong [fundef_cong]:
   "M = N \<Longrightarrow> (\<And>x. x = N \<Longrightarrow> f x = g x) \<Longrightarrow> Let M f = Let N g"
   unfolding Let_def by blast
@@ -140,17 +162,7 @@
   "f (g x) = f' (g' x') \<Longrightarrow> (f o g) x = (f' o g') x'"
   unfolding o_apply .
 
-subsection {* Setup for termination proofs *}
-
-text {* Rules for generating measure functions *}
-
-lemma [measure_function]: "is_measure size"
-by (rule is_measure_trivial)
-
-lemma [measure_function]: "is_measure f \<Longrightarrow> is_measure (\<lambda>p. f (fst p))"
-by (rule is_measure_trivial)
-lemma [measure_function]: "is_measure f \<Longrightarrow> is_measure (\<lambda>p. f (snd p))"
-by (rule is_measure_trivial)
+subsection {* Simp rules for termination proofs *}
 
 lemma termination_basic_simps[termination_simp]:
   "x < (y::nat) \<Longrightarrow> x < y + z" 
@@ -166,5 +178,150 @@
   "prod_size f g p = f (fst p) + g (snd p) + Suc 0"
 by (induct p) auto
 
+subsection {* Decomposition *}
+
+lemma less_by_empty: 
+  "A = {} \<Longrightarrow> A \<subseteq> B"
+and  union_comp_emptyL:
+  "\<lbrakk> A O C = {}; B O C = {} \<rbrakk> \<Longrightarrow> (A \<union> B) O C = {}"
+and union_comp_emptyR:
+  "\<lbrakk> A O B = {}; A O C = {} \<rbrakk> \<Longrightarrow> A O (B \<union> C) = {}"
+and wf_no_loop: 
+  "R O R = {} \<Longrightarrow> wf R"
+by (auto simp add: wf_comp_self[of R])
+
+
+subsection {* Reduction Pairs *}
+
+definition
+  "reduction_pair P = (wf (fst P) \<and> snd P O fst P \<subseteq> fst P)"
+
+lemma reduction_pairI[intro]: "wf R \<Longrightarrow> S O R \<subseteq> R \<Longrightarrow> reduction_pair (R, S)"
+unfolding reduction_pair_def by auto
+
+lemma reduction_pair_lemma:
+  assumes rp: "reduction_pair P"
+  assumes "R \<subseteq> fst P"
+  assumes "S \<subseteq> snd P"
+  assumes "wf S"
+  shows "wf (R \<union> S)"
+proof -
+  from rp `S \<subseteq> snd P` have "wf (fst P)" "S O fst P \<subseteq> fst P"
+    unfolding reduction_pair_def by auto
+  with `wf S` have "wf (fst P \<union> S)" 
+    by (auto intro: wf_union_compatible)
+  moreover from `R \<subseteq> fst P` have "R \<union> S \<subseteq> fst P \<union> S" by auto
+  ultimately show ?thesis by (rule wf_subset) 
+qed
+
+definition
+  "rp_inv_image = (\<lambda>(R,S) f. (inv_image R f, inv_image S f))"
+
+lemma rp_inv_image_rp:
+  "reduction_pair P \<Longrightarrow> reduction_pair (rp_inv_image P f)"
+  unfolding reduction_pair_def rp_inv_image_def split_def
+  by force
+
+
+subsection {* Concrete orders for SCNP termination proofs *}
+
+definition "pair_less = less_than <*lex*> less_than"
+definition "pair_leq = pair_less^="
+definition "max_strict = max_ext pair_less"
+definition "max_weak = max_ext pair_leq \<union> {({}, {})}"
+definition "min_strict = min_ext pair_less"
+definition "min_weak = min_ext pair_leq \<union> {({}, {})}"
+
+lemma wf_pair_less[simp]: "wf pair_less"
+  by (auto simp: pair_less_def)
+
+text {* Introduction rules for pair_less/pair_leq *}
+lemma pair_leqI1: "a < b \<Longrightarrow> ((a, s), (b, t)) \<in> pair_leq"
+  and pair_leqI2: "a \<le> b \<Longrightarrow> s \<le> t \<Longrightarrow> ((a, s), (b, t)) \<in> pair_leq"
+  and pair_lessI1: "a < b  \<Longrightarrow> ((a, s), (b, t)) \<in> pair_less"
+  and pair_lessI2: "a \<le> b \<Longrightarrow> s < t \<Longrightarrow> ((a, s), (b, t)) \<in> pair_less"
+  unfolding pair_leq_def pair_less_def by auto
+
+text {* Introduction rules for max *}
+lemma smax_emptyI: 
+  "finite Y \<Longrightarrow> Y \<noteq> {} \<Longrightarrow> ({}, Y) \<in> max_strict" 
+  and smax_insertI: 
+  "\<lbrakk>y \<in> Y; (x, y) \<in> pair_less; (X, Y) \<in> max_strict\<rbrakk> \<Longrightarrow> (insert x X, Y) \<in> max_strict"
+  and wmax_emptyI: 
+  "finite X \<Longrightarrow> ({}, X) \<in> max_weak" 
+  and wmax_insertI:
+  "\<lbrakk>y \<in> YS; (x, y) \<in> pair_leq; (XS, YS) \<in> max_weak\<rbrakk> \<Longrightarrow> (insert x XS, YS) \<in> max_weak" 
+unfolding max_strict_def max_weak_def by (auto elim!: max_ext.cases)
+
+text {* Introduction rules for min *}
+lemma smin_emptyI: 
+  "X \<noteq> {} \<Longrightarrow> (X, {}) \<in> min_strict" 
+  and smin_insertI: 
+  "\<lbrakk>x \<in> XS; (x, y) \<in> pair_less; (XS, YS) \<in> min_strict\<rbrakk> \<Longrightarrow> (XS, insert y YS) \<in> min_strict"
+  and wmin_emptyI: 
+  "(X, {}) \<in> min_weak" 
+  and wmin_insertI: 
+  "\<lbrakk>x \<in> XS; (x, y) \<in> pair_leq; (XS, YS) \<in> min_weak\<rbrakk> \<Longrightarrow> (XS, insert y YS) \<in> min_weak" 
+by (auto simp: min_strict_def min_weak_def min_ext_def)
+
+text {* Reduction Pairs *}
+
+lemma max_ext_compat: 
+  assumes "S O R \<subseteq> R"
+  shows "(max_ext S \<union> {({},{})}) O max_ext R \<subseteq> max_ext R"
+using assms 
+apply auto
+apply (elim max_ext.cases)
+apply rule
+apply auto[3]
+apply (drule_tac x=xa in meta_spec)
+apply simp
+apply (erule bexE)
+apply (drule_tac x=xb in meta_spec)
+by auto
+
+lemma max_rpair_set: "reduction_pair (max_strict, max_weak)"
+  unfolding max_strict_def max_weak_def 
+apply (intro reduction_pairI max_ext_wf)
+apply simp
+apply (rule max_ext_compat)
+by (auto simp: pair_less_def pair_leq_def)
+
+lemma min_ext_compat: 
+  assumes "S O R \<subseteq> R"
+  shows "(min_ext S \<union> {({},{})}) O min_ext R \<subseteq> min_ext R"
+using assms 
+apply (auto simp: min_ext_def)
+apply (drule_tac x=ya in bspec, assumption)
+apply (erule bexE)
+apply (drule_tac x=xc in bspec)
+apply assumption
+by auto
+
+lemma min_rpair_set: "reduction_pair (min_strict, min_weak)"
+  unfolding min_strict_def min_weak_def 
+apply (intro reduction_pairI min_ext_wf)
+apply simp
+apply (rule min_ext_compat)
+by (auto simp: pair_less_def pair_leq_def)
+
+
+subsection {* Tool setup *}
+
+use "Tools/function_package/termination.ML"
+use "Tools/function_package/decompose.ML"
+use "Tools/function_package/descent.ML"
+use "Tools/function_package/scnp_solve.ML"
+use "Tools/function_package/scnp_reconstruct.ML"
+
+setup {* ScnpReconstruct.setup *}
+(*
+setup {*
+  Context.theory_map (FundefCommon.set_termination_prover (ScnpReconstruct.decomp_scnp 
+  [ScnpSolve.MAX, ScnpSolve.MIN, ScnpSolve.MS])) 
+*}
+*)
+
+
 
 end
diff -r 5a79ec2fedfb -r d41182a8135c src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Tue Dec 16 00:19:47 2008 +0100
+++ b/src/HOL/IsaMakefile	Tue Dec 16 08:46:07 2008 +0100
@@ -112,6 +112,8 @@
   Tools/dseq.ML \
   Tools/function_package/auto_term.ML \
   Tools/function_package/context_tree.ML \
+  Tools/function_package/decompose.ML \
+  Tools/function_package/descent.ML \
   Tools/function_package/fundef_common.ML \
   Tools/function_package/fundef_core.ML \
   Tools/function_package/fundef_datatype.ML \
@@ -123,8 +125,11 @@
   Tools/function_package/measure_functions.ML \
   Tools/function_package/mutual.ML \
   Tools/function_package/pattern_split.ML \
+  Tools/function_package/scnp_reconstruct.ML \
+  Tools/function_package/scnp_solve.ML \
   Tools/function_package/size.ML \
   Tools/function_package/sum_tree.ML \
+  Tools/function_package/termination.ML \
   Tools/hologic.ML \
   Tools/inductive_codegen.ML \
   Tools/inductive_package.ML \
diff -r 5a79ec2fedfb -r d41182a8135c src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Tue Dec 16 00:19:47 2008 +0100
+++ b/src/HOL/Library/Multiset.thy	Tue Dec 16 08:46:07 2008 +0100
@@ -1481,4 +1481,155 @@
   @{term "{#x+x|x:#M. x<c#}"}.
 *}
 
+
+subsection {* Termination proofs with multiset orders *}
+
+lemma multi_member_skip: "x \<in># XS \<Longrightarrow> x \<in># {# y #} + XS"
+  and multi_member_this: "x \<in># {# x #} + XS"
+  and multi_member_last: "x \<in># {# x #}"
+  by auto
+
+definition "ms_strict = mult pair_less"
+definition "ms_weak = ms_strict \<union> Id"
+
+lemma ms_reduction_pair: "reduction_pair (ms_strict, ms_weak)"
+unfolding reduction_pair_def ms_strict_def ms_weak_def pair_less_def
+by (auto intro: wf_mult1 wf_trancl simp: mult_def)
+
+lemma smsI:
+  "(set_of A, set_of B) \<in> max_strict \<Longrightarrow> (Z + A, Z + B) \<in> ms_strict"
+  unfolding ms_strict_def
+by (rule one_step_implies_mult) (auto simp add: max_strict_def pair_less_def elim!:max_ext.cases)
+
+lemma wmsI:
+  "(set_of A, set_of B) \<in> max_strict \<or> A = {#} \<and> B = {#}
+  \<Longrightarrow> (Z + A, Z + B) \<in> ms_weak"
+unfolding ms_weak_def ms_strict_def
+by (auto simp add: pair_less_def max_strict_def elim!:max_ext.cases intro: one_step_implies_mult)
+
+inductive pw_leq
+where
+  pw_leq_empty: "pw_leq {#} {#}"
+| pw_leq_step:  "\<lbrakk>(x,y) \<in> pair_leq; pw_leq X Y \<rbrakk> \<Longrightarrow> pw_leq ({#x#} + X) ({#y#} + Y)"
+
+lemma pw_leq_lstep:
+  "(x, y) \<in> pair_leq \<Longrightarrow> pw_leq {#x#} {#y#}"
+by (drule pw_leq_step) (rule pw_leq_empty, simp)
+
+lemma pw_leq_split:
+  assumes "pw_leq X Y"
+  shows "\<exists>A B Z. X = A + Z \<and> Y = B + Z \<and> ((set_of A, set_of B) \<in> max_strict \<or> (B = {#} \<and> A = {#}))"
+  using assms
+proof (induct)
+  case pw_leq_empty thus ?case by auto
+next
+  case (pw_leq_step x y X Y)
+  then obtain A B Z where
+    [simp]: "X = A + Z" "Y = B + Z" 
+      and 1[simp]: "(set_of A, set_of B) \<in> max_strict \<or> (B = {#} \<and> A = {#})" 
+    by auto
+  from pw_leq_step have "x = y \<or> (x, y) \<in> pair_less" 
+    unfolding pair_leq_def by auto
+  thus ?case
+  proof
+    assume [simp]: "x = y"
+    have
+      "{#x#} + X = A + ({#y#}+Z) 
+      \<and> {#y#} + Y = B + ({#y#}+Z)
+      \<and> ((set_of A, set_of B) \<in> max_strict \<or> (B = {#} \<and> A = {#}))"
+      by (auto simp: add_ac)
+    thus ?case by (intro exI)
+  next
+    assume A: "(x, y) \<in> pair_less"
+    let ?A' = "{#x#} + A" and ?B' = "{#y#} + B"
+    have "{#x#} + X = ?A' + Z"
+      "{#y#} + Y = ?B' + Z"
+      by (auto simp add: add_ac)
+    moreover have 
+      "(set_of ?A', set_of ?B') \<in> max_strict"
+      using 1 A unfolding max_strict_def 
+      by (auto elim!: max_ext.cases)
+    ultimately show ?thesis by blast
+  qed
+qed
+
+lemma 
+  assumes pwleq: "pw_leq Z Z'"
+  shows ms_strictI: "(set_of A, set_of B) \<in> max_strict \<Longrightarrow> (Z + A, Z' + B) \<in> ms_strict"
+  and   ms_weakI1:  "(set_of A, set_of B) \<in> max_strict \<Longrightarrow> (Z + A, Z' + B) \<in> ms_weak"
+  and   ms_weakI2:  "(Z + {#}, Z' + {#}) \<in> ms_weak"
+proof -
+  from pw_leq_split[OF pwleq] 
+  obtain A' B' Z''
+    where [simp]: "Z = A' + Z''" "Z' = B' + Z''"
+    and mx_or_empty: "(set_of A', set_of B') \<in> max_strict \<or> (A' = {#} \<and> B' = {#})"
+    by blast
+  {
+    assume max: "(set_of A, set_of B) \<in> max_strict"
+    from mx_or_empty
+    have "(Z'' + (A + A'), Z'' + (B + B')) \<in> ms_strict"
+    proof
+      assume max': "(set_of A', set_of B') \<in> max_strict"
+      with max have "(set_of (A + A'), set_of (B + B')) \<in> max_strict"
+        by (auto simp: max_strict_def intro: max_ext_additive)
+      thus ?thesis by (rule smsI) 
+    next
+      assume [simp]: "A' = {#} \<and> B' = {#}"
+      show ?thesis by (rule smsI) (auto intro: max)
+    qed
+    thus "(Z + A, Z' + B) \<in> ms_strict" by (simp add:add_ac)
+    thus "(Z + A, Z' + B) \<in> ms_weak" by (simp add: ms_weak_def)
+  }
+  from mx_or_empty
+  have "(Z'' + A', Z'' + B') \<in> ms_weak" by (rule wmsI)
+  thus "(Z + {#}, Z' + {#}) \<in> ms_weak" by (simp add:add_ac)
+qed
+
+lemma empty_idemp: "{#} + x = x" "x + {#} = x"
+and nonempty_plus: "{# x #} + rs \<noteq> {#}"
+and nonempty_single: "{# x #} \<noteq> {#}"
+by auto
+
+setup {*
+let
+  fun msetT T = Type ("Multiset.multiset", [T]);
+
+  fun mk_mset T [] = Const (@{const_name Mempty}, msetT T)
+    | mk_mset T [x] = Const (@{const_name single}, T --> msetT T) $ x
+    | mk_mset T (x :: xs) =
+          Const (@{const_name plus}, msetT T --> msetT T --> msetT T) $
+                mk_mset T [x] $ mk_mset T xs
+
+  fun mset_member_tac m i =
+      (if m <= 0 then
+           rtac @{thm multi_member_this} i ORELSE rtac @{thm multi_member_last} i
+       else
+           rtac @{thm multi_member_skip} i THEN mset_member_tac (m - 1) i)
+
+  val mset_nonempty_tac =
+      rtac @{thm nonempty_plus} ORELSE' rtac @{thm nonempty_single}
+
+  val regroup_munion_conv =
+      FundefLib.regroup_conv @{const_name Multiset.Mempty} @{const_name plus}
+        (map (fn t => t RS eq_reflection) (@{thms union_ac} @ @{thms empty_idemp}))
+
+  fun unfold_pwleq_tac i =
+    (rtac @{thm pw_leq_step} i THEN (fn st => unfold_pwleq_tac (i + 1) st))
+      ORELSE (rtac @{thm pw_leq_lstep} i)
+      ORELSE (rtac @{thm pw_leq_empty} i)
+
+  val set_of_simps = [@{thm set_of_empty}, @{thm set_of_single}, @{thm set_of_union},
+                      @{thm Un_insert_left}, @{thm Un_empty_left}]
+in
+  ScnpReconstruct.multiset_setup (ScnpReconstruct.Multiset 
+  {
+    msetT=msetT, mk_mset=mk_mset, mset_regroup_conv=regroup_munion_conv,
+    mset_member_tac=mset_member_tac, mset_nonempty_tac=mset_nonempty_tac,
+    mset_pwleq_tac=unfold_pwleq_tac, set_of_simps=set_of_simps,
+    smsI'=@{thm ms_strictI}, wmsI2''=@{thm ms_weakI2}, wmsI1=@{thm ms_weakI1},
+    reduction_pair=@{thm ms_reduction_pair}
+  })
 end
+*}
+
+end
diff -r 5a79ec2fedfb -r d41182a8135c src/HOL/Tools/function_package/decompose.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/function_package/decompose.ML	Tue Dec 16 08:46:07 2008 +0100
@@ -0,0 +1,105 @@
+(*  Title:       HOL/Tools/function_package/decompose.ML
+    Author:      Alexander Krauss, TU Muenchen
+
+Graph decomposition using "Shallow Dependency Pairs".
+*)
+
+signature DECOMPOSE =
+sig
+
+  val derive_chains : Proof.context -> tactic
+                      -> (Termination.data -> int -> tactic)
+                      -> Termination.data -> int -> tactic
+
+  val decompose_tac : Proof.context -> tactic
+                      -> Termination.ttac
+
+end
+
+structure Decompose : DECOMPOSE =
+struct
+
+structure TermGraph = GraphFun(type key = term val ord = Term.fast_term_ord);
+
+
+fun derive_chains ctxt chain_tac cont D = Termination.CALLS (fn (cs, i) =>
+  let
+      val thy = ProofContext.theory_of ctxt
+
+      fun prove_chain c1 c2 D =
+          if is_some (Termination.get_chain D c1 c2) then D else
+          let
+            val goal = HOLogic.mk_eq (HOLogic.mk_binop @{const_name "Relation.rel_comp"} (c1, c2),
+                                      Const (@{const_name "{}"}, fastype_of c1))
+                       |> HOLogic.mk_Trueprop (* "C1 O C2 = {}" *)
+
+            val chain = case FundefLib.try_proof (cterm_of thy goal) chain_tac of
+                          FundefLib.Solved thm => SOME thm
+                        | _ => NONE
+          in
+            Termination.note_chain c1 c2 chain D
+          end
+  in
+    cont (fold_product prove_chain cs cs D) i
+  end)
+
+
+fun mk_dgraph D cs =
+    TermGraph.empty
+    |> fold (fn c => TermGraph.new_node (c,())) cs
+    |> fold_product (fn c1 => fn c2 =>
+         if is_none (Termination.get_chain D c1 c2 |> the_default NONE)
+         then TermGraph.add_edge (c1, c2) else I)
+       cs cs
+
+
+fun ucomp_empty_tac T =
+    REPEAT_ALL_NEW (rtac @{thm union_comp_emptyR}
+                    ORELSE' rtac @{thm union_comp_emptyL}
+                    ORELSE' SUBGOAL (fn (_ $ (_ $ (_ $ c1 $ c2) $ _), i) => rtac (T c1 c2) i))
+
+fun regroup_calls_tac cs = Termination.CALLS (fn (cs', i) =>
+   let
+     val is = map (fn c => find_index (curry op aconv c) cs') cs
+   in
+     CONVERSION (Conv.arg_conv (Conv.arg_conv (FundefLib.regroup_union_conv is))) i
+   end)
+
+
+fun solve_trivial_tac D = Termination.CALLS
+(fn ([c], i) =>
+    (case Termination.get_chain D c c of
+       SOME (SOME thm) => rtac @{thm wf_no_loop} i
+                          THEN rtac thm i
+     | _ => no_tac)
+  | _ => no_tac)
+
+fun decompose_tac' ctxt cont err_cont D = Termination.CALLS (fn (cs, i) =>
+    let
+      val G = mk_dgraph D cs
+      val sccs = TermGraph.strong_conn G
+
+      fun split [SCC] i = (solve_trivial_tac D i ORELSE cont D i)
+        | split (SCC::rest) i =
+            regroup_calls_tac SCC i
+            THEN rtac @{thm wf_union_compatible} i
+            THEN rtac @{thm less_by_empty} (i + 2)
+            THEN ucomp_empty_tac (the o the oo Termination.get_chain D) (i + 2)
+            THEN split rest (i + 1)
+            THEN (solve_trivial_tac D i ORELSE cont D i)
+    in
+      if length sccs > 1 then split sccs i
+      else solve_trivial_tac D i ORELSE err_cont D i
+    end)
+
+fun decompose_tac ctxt chain_tac cont err_cont =
+    derive_chains ctxt chain_tac
+    (decompose_tac' ctxt cont err_cont)
+
+fun auto_decompose_tac ctxt =
+    Termination.TERMINATION ctxt
+      (decompose_tac ctxt (auto_tac (local_clasimpset_of ctxt))
+                     (K (K all_tac)) (K (K no_tac)))
+
+
+end
diff -r 5a79ec2fedfb -r d41182a8135c src/HOL/Tools/function_package/descent.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/function_package/descent.ML	Tue Dec 16 08:46:07 2008 +0100
@@ -0,0 +1,44 @@
+(*  Title:       HOL/Tools/function_package/descent.ML
+    Author:      Alexander Krauss, TU Muenchen
+
+Descent proofs for termination
+*)
+
+
+signature DESCENT =
+sig
+
+  val derive_diag : Proof.context -> tactic -> (Termination.data -> int -> tactic)
+                    -> Termination.data -> int -> tactic
+
+  val derive_all  : Proof.context -> tactic -> (Termination.data -> int -> tactic)
+                    -> Termination.data -> int -> tactic
+
+end
+
+
+structure Descent : DESCENT =
+struct
+
+fun gen_descent diag ctxt tac cont D = Termination.CALLS (fn (cs, i) =>
+  let
+    val thy = ProofContext.theory_of ctxt
+    val measures_of = Termination.get_measures D
+
+    fun derive c D =
+      let
+        val (_, p, _, q, _, _) = Termination.dest_call D c
+      in
+        if diag andalso p = q
+        then fold (fn m => Termination.derive_descent thy tac c m m) (measures_of p) D
+        else fold_product (Termination.derive_descent thy tac c)
+               (measures_of p) (measures_of q) D
+      end
+  in
+    cont (FundefCommon.PROFILE "deriving descents" (fold derive cs) D) i
+  end)
+
+val derive_diag = gen_descent true
+val derive_all = gen_descent false
+
+end
diff -r 5a79ec2fedfb -r d41182a8135c src/HOL/Tools/function_package/fundef_lib.ML
--- a/src/HOL/Tools/function_package/fundef_lib.ML	Tue Dec 16 00:19:47 2008 +0100
+++ b/src/HOL/Tools/function_package/fundef_lib.ML	Tue Dec 16 08:46:07 2008 +0100
@@ -130,4 +130,50 @@
     | SOME st => if Thm.no_prems st then Solved (Goal.finish st) else Stuck st
 
 
+fun dest_binop_list cn (t as (Const (n, _) $ a $ b)) = 
+    if cn = n then dest_binop_list cn a @ dest_binop_list cn b else [ t ]
+  | dest_binop_list _ t = [ t ]
+
+
+(* separate two parts in a +-expression:
+   "a + b + c + d + e" --> "(a + b + d) + (c + e)"
+
+   Here, + can be any binary operation that is AC.
+
+   cn - The name of the binop-constructor (e.g. @{const_name "op Un"})
+   ac - the AC rewrite rules for cn
+   is - the list of indices of the expressions that should become the first part
+        (e.g. [0,1,3] in the above example)
+*)
+
+fun regroup_conv neu cn ac is ct =
+ let
+   val mk = HOLogic.mk_binop cn
+   val t = term_of ct
+   val xs = dest_binop_list cn t
+   val js = 0 upto (length xs) - 1 \\ is
+   val ty = fastype_of t
+   val thy = theory_of_cterm ct
+ in
+   Goal.prove_internal []
+     (cterm_of thy
+       (Logic.mk_equals (t,
+          if is = []
+          then mk (Const (neu, ty), foldr1 mk (map (nth xs) js))
+          else if js = []
+            then mk (foldr1 mk (map (nth xs) is), Const (neu, ty))
+            else mk (foldr1 mk (map (nth xs) is), foldr1 mk (map (nth xs) js)))))
+     (K (MetaSimplifier.rewrite_goals_tac ac
+         THEN rtac Drule.reflexive_thm 1))
+ end
+
+(* instance for unions *)
+fun regroup_union_conv t =
+    regroup_conv (@{const_name "{}"})
+                  @{const_name "op Un"}
+       (map (fn t => t RS eq_reflection) (@{thms "Un_ac"} @
+                                          @{thms "Un_empty_right"} @
+                                          @{thms "Un_empty_left"})) t
+
+
 end
diff -r 5a79ec2fedfb -r d41182a8135c src/HOL/Tools/function_package/scnp_reconstruct.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/function_package/scnp_reconstruct.ML	Tue Dec 16 08:46:07 2008 +0100
@@ -0,0 +1,426 @@
+(*  Title:       HOL/Tools/function_package/scnp_reconstruct.ML
+    Author:      Armin Heller, TU Muenchen
+    Author:      Alexander Krauss, TU Muenchen
+
+Proof reconstruction for SCNP
+*)
+
+signature SCNP_RECONSTRUCT =
+sig
+
+  val decomp_scnp : ScnpSolve.label list -> Proof.context -> method
+
+  val setup : theory -> theory
+
+  datatype multiset_setup =
+    Multiset of
+    {
+     msetT : typ -> typ,
+     mk_mset : typ -> term list -> term,
+     mset_regroup_conv : int list -> conv,
+     mset_member_tac : int -> int -> tactic,
+     mset_nonempty_tac : int -> tactic,
+     mset_pwleq_tac : int -> tactic,
+     set_of_simps : thm list,
+     smsI' : thm,
+     wmsI2'' : thm,
+     wmsI1 : thm,
+     reduction_pair : thm
+    }
+
+
+  val multiset_setup : multiset_setup -> theory -> theory
+
+end
+
+structure ScnpReconstruct : SCNP_RECONSTRUCT =
+struct
+
+val PROFILE = FundefCommon.PROFILE
+fun TRACE x = if ! FundefCommon.profile then Output.tracing x else ()
+
+open ScnpSolve
+
+val natT = HOLogic.natT
+val nat_pairT = HOLogic.mk_prodT (natT, natT)
+
+(* Theory dependencies *)
+
+datatype multiset_setup =
+  Multiset of
+  {
+   msetT : typ -> typ,
+   mk_mset : typ -> term list -> term,
+   mset_regroup_conv : int list -> conv,
+   mset_member_tac : int -> int -> tactic,
+   mset_nonempty_tac : int -> tactic,
+   mset_pwleq_tac : int -> tactic,
+   set_of_simps : thm list,
+   smsI' : thm,
+   wmsI2'' : thm,
+   wmsI1 : thm,
+   reduction_pair : thm
+  }
+
+structure MultisetSetup = TheoryDataFun
+(
+  type T = multiset_setup option
+  val empty = NONE
+  val copy = I;
+  val extend = I;
+  fun merge _ (v1, v2) = if is_some v2 then v2 else v1
+)
+
+val multiset_setup = MultisetSetup.put o SOME
+
+fun undef x = error "undef"
+fun get_multiset_setup thy = MultisetSetup.get thy
+  |> the_default (Multiset
+{ msetT = undef, mk_mset=undef,
+  mset_regroup_conv=undef, mset_member_tac = undef,
+  mset_nonempty_tac = undef, mset_pwleq_tac = undef,
+  set_of_simps = [],reduction_pair = refl,
+  smsI'=refl, wmsI2''=refl, wmsI1=refl })
+
+fun order_rpair _ MAX = @{thm max_rpair_set}
+  | order_rpair msrp MS  = msrp
+  | order_rpair _ MIN = @{thm min_rpair_set}
+
+fun ord_intros_max true =
+    (@{thm smax_emptyI}, @{thm smax_insertI})
+  | ord_intros_max false =
+    (@{thm wmax_emptyI}, @{thm wmax_insertI})
+fun ord_intros_min true =
+    (@{thm smin_emptyI}, @{thm smin_insertI})
+  | ord_intros_min false =
+    (@{thm wmin_emptyI}, @{thm wmin_insertI})
+
+fun gen_probl D cs =
+  let
+    val n = Termination.get_num_points D
+    val arity = length o Termination.get_measures D
+    fun measure p i = nth (Termination.get_measures D p) i
+
+    fun mk_graph c =
+      let
+        val (_, p, _, q, _, _) = Termination.dest_call D c
+
+        fun add_edge i j =
+          case Termination.get_descent D c (measure p i) (measure q j)
+           of SOME (Termination.Less _) => cons (i, GTR, j)
+            | SOME (Termination.LessEq _) => cons (i, GEQ, j)
+            | _ => I
+
+        val edges =
+          fold_product add_edge (0 upto arity p - 1) (0 upto arity q - 1) []
+      in
+        G (p, q, edges)
+      end
+  in
+    GP (map arity (0 upto n - 1), map mk_graph cs)
+  end
+
+(* General reduction pair application *)
+fun rem_inv_img ctxt =
+  let
+    val unfold_tac = LocalDefs.unfold_tac ctxt
+  in
+    rtac @{thm subsetI} 1
+    THEN etac @{thm CollectE} 1
+    THEN REPEAT (etac @{thm exE} 1)
+    THEN unfold_tac @{thms inv_image_def}
+    THEN rtac @{thm CollectI} 1
+    THEN etac @{thm conjE} 1
+    THEN etac @{thm ssubst} 1
+    THEN unfold_tac (@{thms split_conv} @ @{thms triv_forall_equality}
+                     @ @{thms Sum_Type.sum_cases})
+  end
+
+(* Sets *)
+
+val setT = HOLogic.mk_setT
+
+fun mk_set T [] = Const (@{const_name "{}"}, setT T)
+  | mk_set T (x :: xs) =
+      Const (@{const_name insert}, T --> setT T --> setT T) $
+            x $ mk_set T xs
+
+fun set_member_tac m i =
+  if m = 0 then rtac @{thm insertI1} i
+  else rtac @{thm insertI2} i THEN set_member_tac (m - 1) i
+
+val set_nonempty_tac = rtac @{thm insert_not_empty}
+
+fun set_finite_tac i =
+  rtac @{thm finite.emptyI} i
+  ORELSE (rtac @{thm finite.insertI} i THEN (fn st => set_finite_tac i st))
+
+
+(* Reconstruction *)
+
+fun reconstruct_tac ctxt D cs (gp as GP (_, gs)) certificate =
+  let
+    val thy = ProofContext.theory_of ctxt
+    val Multiset
+          { msetT, mk_mset,
+            mset_regroup_conv, mset_member_tac,
+            mset_nonempty_tac, mset_pwleq_tac, set_of_simps,
+            smsI', wmsI2'', wmsI1, reduction_pair=ms_rp } 
+        = get_multiset_setup thy
+
+    fun measure_fn p = nth (Termination.get_measures D p)
+
+    fun get_desc_thm cidx m1 m2 bStrict =
+      case Termination.get_descent D (nth cs cidx) m1 m2
+       of SOME (Termination.Less thm) =>
+          if bStrict then thm
+          else (thm COMP (Thm.lift_rule (cprop_of thm) @{thm less_imp_le}))
+        | SOME (Termination.LessEq (thm, _))  =>
+          if not bStrict then thm
+          else sys_error "get_desc_thm"
+        | _ => sys_error "get_desc_thm"
+
+    val (label, lev, sl, covering) = certificate
+
+    fun prove_lev strict g =
+      let
+        val G (p, q, el) = nth gs g
+
+        fun less_proof strict (j, b) (i, a) =
+          let
+            val tag_flag = b < a orelse (not strict andalso b <= a)
+
+            val stored_thm =
+              get_desc_thm g (measure_fn p i) (measure_fn q j)
+                             (not tag_flag)
+              |> Conv.fconv_rule (Thm.beta_conversion true)
+
+            val rule = if strict
+              then if b < a then @{thm pair_lessI2} else @{thm pair_lessI1}
+              else if b <= a then @{thm pair_leqI2} else @{thm pair_leqI1}
+          in
+            rtac rule 1 THEN PRIMITIVE (Thm.elim_implies stored_thm)
+            THEN (if tag_flag then arith_tac ctxt 1 else all_tac)
+          end
+
+        fun steps_tac MAX strict lq lp =
+          let
+            val (empty, step) = ord_intros_max strict
+          in
+            if length lq = 0
+            then rtac empty 1 THEN set_finite_tac 1
+                 THEN (if strict then set_nonempty_tac 1 else all_tac)
+            else
+              let
+                val (j, b) :: rest = lq
+                val (i, a) = the (covering g strict j)
+                fun choose xs = set_member_tac (Library.find_index (curry op = (i, a)) xs) 1
+                val solve_tac = choose lp THEN less_proof strict (j, b) (i, a)
+              in
+                rtac step 1 THEN solve_tac THEN steps_tac MAX strict rest lp
+              end
+          end
+          | steps_tac MIN strict lq lp =
+          let
+            val (empty, step) = ord_intros_min strict
+          in
+            if length lp = 0
+            then rtac empty 1
+                 THEN (if strict then set_nonempty_tac 1 else all_tac)
+            else
+              let
+                val (i, a) :: rest = lp
+                val (j, b) = the (covering g strict i)
+                fun choose xs = set_member_tac (Library.find_index (curry op = (j, b)) xs) 1
+                val solve_tac = choose lq THEN less_proof strict (j, b) (i, a)
+              in
+                rtac step 1 THEN solve_tac THEN steps_tac MIN strict lq rest
+              end
+          end
+          | steps_tac MS strict lq lp =
+          let
+            fun get_str_cover (j, b) =
+              if is_some (covering g true j) then SOME (j, b) else NONE
+            fun get_wk_cover (j, b) = the (covering g false j)
+
+            val qs = lq \\ map_filter get_str_cover lq
+            val ps = map get_wk_cover qs
+
+            fun indices xs ys = map (fn y => Library.find_index (curry op = y) xs) ys
+            val iqs = indices lq qs
+            val ips = indices lp ps
+
+            local open Conv in
+            fun t_conv a C =
+              params_conv ~1 (K ((concl_conv ~1 o arg_conv o arg1_conv o a) C)) ctxt
+            val goal_rewrite =
+                t_conv arg1_conv (mset_regroup_conv iqs)
+                then_conv t_conv arg_conv (mset_regroup_conv ips)
+            end
+          in
+            CONVERSION goal_rewrite 1
+            THEN (if strict then rtac smsI' 1
+                  else if qs = lq then rtac wmsI2'' 1
+                  else rtac wmsI1 1)
+            THEN mset_pwleq_tac 1
+            THEN EVERY (map2 (less_proof false) qs ps)
+            THEN (if strict orelse qs <> lq
+                  then LocalDefs.unfold_tac ctxt set_of_simps
+                       THEN steps_tac MAX true (lq \\ qs) (lp \\ ps)
+                  else all_tac)
+          end
+      in
+        rem_inv_img ctxt
+        THEN steps_tac label strict (nth lev q) (nth lev p)
+      end
+
+    val (mk_set, setT) = if label = MS then (mk_mset, msetT) else (mk_set, setT)
+
+    fun tag_pair p (i, tag) =
+      HOLogic.pair_const natT natT $
+        (measure_fn p i $ Bound 0) $ HOLogic.mk_number natT tag
+
+    fun pt_lev (p, lm) = Abs ("x", Termination.get_types D p,
+                           mk_set nat_pairT (map (tag_pair p) lm))
+
+    val level_mapping =
+      map_index pt_lev lev
+        |> Termination.mk_sumcases D (setT nat_pairT)
+        |> cterm_of thy
+    in
+      PROFILE "Proof Reconstruction"
+        (CONVERSION (Conv.arg_conv (Conv.arg_conv (FundefLib.regroup_union_conv sl))) 1
+         THEN (rtac @{thm reduction_pair_lemma} 1)
+         THEN (rtac @{thm rp_inv_image_rp} 1)
+         THEN (rtac (order_rpair ms_rp label) 1)
+         THEN PRIMITIVE (instantiate' [] [SOME level_mapping])
+         THEN unfold_tac @{thms rp_inv_image_def} (simpset_of thy)
+         THEN LocalDefs.unfold_tac ctxt
+           (@{thms split_conv} @ @{thms fst_conv} @ @{thms snd_conv})
+         THEN REPEAT (SOMEGOAL (resolve_tac [@{thm Un_least}, @{thm empty_subsetI}]))
+         THEN EVERY (map (prove_lev true) sl)
+         THEN EVERY (map (prove_lev false) ((0 upto length cs - 1) \\ sl)))
+    end
+
+
+
+local open Termination in
+fun print_cell (SOME (Less _)) = "<"
+  | print_cell (SOME (LessEq _)) = "\<le>"
+  | print_cell (SOME (None _)) = "-"
+  | print_cell (SOME (False _)) = "-"
+  | print_cell (NONE) = "?"
+
+fun print_error ctxt D = CALLS (fn (cs, i) =>
+  let
+    val np = get_num_points D
+    val ms = map (get_measures D) (0 upto np - 1)
+    val tys = map (get_types D) (0 upto np - 1)
+    fun index xs = (1 upto length xs) ~~ xs
+    fun outp s t f xs = map (fn (x, y) => s ^ Int.toString x ^ t ^ f y ^ "\n") xs
+    val ims = index (map index ms)
+    val _ = Output.tracing (concat (outp "fn #" ":\n" (concat o outp "\tmeasure #" ": " (Syntax.string_of_term ctxt)) ims))
+    fun print_call (k, c) =
+      let
+        val (_, p, _, q, _, _) = dest_call D c
+        val _ = Output.tracing ("call table for call #" ^ Int.toString k ^ ": fn " ^ 
+                                Int.toString (p + 1) ^ " ~> fn " ^ Int.toString (q + 1))
+        val caller_ms = nth ms p
+        val callee_ms = nth ms q
+        val entries = map (fn x => map (pair x) (callee_ms)) (caller_ms)
+        fun print_ln (i : int, l) = concat (Int.toString i :: "   " :: map (enclose " " " " o print_cell o (uncurry (get_descent D c))) l)
+        val _ = Output.tracing (concat (Int.toString (p + 1) ^ "|" ^ Int.toString (q + 1) ^ 
+                                        " " :: map (enclose " " " " o Int.toString) (1 upto length callee_ms)) ^ "\n" 
+                                ^ cat_lines (map print_ln ((1 upto (length entries)) ~~ entries)))
+      in
+        true
+      end
+    fun list_call (k, c) =
+      let
+        val (_, p, _, q, _, _) = dest_call D c
+        val _ = Output.tracing ("call #" ^ (Int.toString k) ^ ": fn " ^
+                                Int.toString (p + 1) ^ " ~> fn " ^ Int.toString (q + 1) ^ "\n" ^ 
+                                (Syntax.string_of_term ctxt c))
+      in true end
+    val _ = forall list_call ((1 upto length cs) ~~ cs)
+    val _ = forall print_call ((1 upto length cs) ~~ cs)
+  in
+    all_tac
+  end)
+end
+
+
+fun single_scnp_tac use_tags orders ctxt cont err_cont D = Termination.CALLS (fn (cs, i) =>
+  let
+    val gp = gen_probl D cs
+(*    val _ = TRACE ("SCNP instance: " ^ makestring gp)*)
+    val certificate = generate_certificate use_tags orders gp
+(*    val _ = TRACE ("Certificate: " ^ makestring certificate)*)
+
+    val ms_configured = is_some (MultisetSetup.get (ProofContext.theory_of ctxt))
+    in
+    case certificate
+     of NONE => err_cont D i
+      | SOME cert =>
+        if not ms_configured andalso #1 cert = MS
+        then err_cont D i
+        else SELECT_GOAL (reconstruct_tac ctxt D cs gp cert) i
+             THEN (rtac @{thm wf_empty} i ORELSE cont D i)
+  end)
+
+fun decomp_scnp_tac orders autom_tac ctxt err_cont =
+  let
+    open Termination
+    val derive_diag = Descent.derive_diag ctxt autom_tac
+    val derive_all = Descent.derive_all ctxt autom_tac
+    val decompose = Decompose.decompose_tac ctxt autom_tac
+    val scnp_no_tags = single_scnp_tac false orders ctxt
+    val scnp_full = single_scnp_tac true orders ctxt
+
+    fun first_round c e =
+        derive_diag (REPEAT scnp_no_tags c e)
+
+    val second_round =
+        REPEAT (fn c => fn e => decompose (scnp_no_tags c c) e)
+
+    val third_round =
+        derive_all oo
+        REPEAT (fn c => fn e =>
+          scnp_full (decompose c c) e)
+
+    fun Then s1 s2 c e = s1 (s2 c c) (s2 c e)
+
+    val strategy = Then (Then first_round second_round) third_round
+
+  in
+    TERMINATION ctxt (strategy err_cont err_cont)
+  end
+
+fun decomp_scnp orders ctxt =
+  let
+    val extra_simps = FundefCommon.TerminationSimps.get ctxt
+    val autom_tac = auto_tac (local_clasimpset_of ctxt addsimps2 extra_simps)
+  in
+    Method.SIMPLE_METHOD
+      (TRY (FundefCommon.apply_termination_rule ctxt 1)
+       THEN TRY Termination.wf_union_tac
+       THEN
+         (rtac @{thm wf_empty} 1
+          ORELSE decomp_scnp_tac orders autom_tac ctxt (print_error ctxt) 1))
+  end
+
+
+(* Method setup *)
+
+val orders =
+  (Scan.repeat1
+    ((Args.$$$ "max" >> K MAX) ||
+     (Args.$$$ "min" >> K MIN) ||
+     (Args.$$$ "ms" >> K MS))
+  || Scan.succeed [MAX, MS, MIN])
+
+val setup = Method.add_method
+  ("sizechange", Method.sectioned_args (Scan.lift orders) clasimp_modifiers decomp_scnp,
+   "termination prover with graph decomposition and the NP subset of size change termination")
+
+end
diff -r 5a79ec2fedfb -r d41182a8135c src/HOL/Tools/function_package/scnp_solve.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/function_package/scnp_solve.ML	Tue Dec 16 08:46:07 2008 +0100
@@ -0,0 +1,257 @@
+(*  Title:       HOL/Tools/function_package/scnp_solve.ML
+    Author:      Armin Heller, TU Muenchen
+    Author:      Alexander Krauss, TU Muenchen
+
+Generate certificates for SCNP using a SAT solver
+*)
+
+
+signature SCNP_SOLVE =
+sig
+
+  datatype edge = GTR | GEQ
+  datatype graph = G of int * int * (int * edge * int) list
+  datatype graph_problem = GP of int list * graph list
+
+  datatype label = MIN | MAX | MS
+
+  type certificate =
+    label                   (* which order *)
+    * (int * int) list list (* (multi)sets *)
+    * int list              (* strictly ordered calls *)
+    * (int -> bool -> int -> (int * int) option) (* covering function *)
+
+  val generate_certificate : bool -> label list -> graph_problem -> certificate option
+
+  val solver : string ref
+end
+
+structure ScnpSolve : SCNP_SOLVE =
+struct
+
+(** Graph problems **)
+
+datatype edge = GTR | GEQ ;
+datatype graph = G of int * int * (int * edge * int) list ;
+datatype graph_problem = GP of int list * graph list ;
+
+datatype label = MIN | MAX | MS ;
+type certificate =
+  label
+  * (int * int) list list
+  * int list
+  * (int -> bool -> int -> (int * int) option)
+
+fun graph_at (GP (_, gs), i) = nth gs i ;
+fun num_prog_pts (GP (arities, _)) = length arities ;
+fun num_graphs (GP (_, gs)) = length gs ;
+fun arity (GP (arities, gl)) i = nth arities i ;
+fun ndigits (GP (arities, _)) = IntInf.log2 (foldl (op +) 0 arities) + 1
+
+
+(** Propositional formulas **)
+
+val Not = PropLogic.Not and And = PropLogic.And and Or = PropLogic.Or
+val BoolVar = PropLogic.BoolVar
+fun Implies (p, q) = Or (Not p, q)
+fun Equiv (p, q) = And (Implies (p, q), Implies (q, p))
+val all = PropLogic.all
+
+(* finite indexed quantifiers:
+
+iforall n f   <==>      /\
+                       /  \  f i
+                      0<=i<n
+ *)
+fun iforall n f = all (map f (0 upto n - 1))
+fun iexists n f = PropLogic.exists (map f (0 upto n - 1))
+fun iforall2 n m f = all (map_product f (0 upto n - 1) (0 upto m - 1))
+
+fun the_one var n x = all (var x :: map (Not o var) ((0 upto n - 1) \\ [x]))
+fun exactly_one n f = iexists n (the_one f n)
+
+(* SAT solving *)
+val solver = ref "auto";
+fun sat_solver x =
+  FundefCommon.PROFILE "sat_solving..." (SatSolver.invoke_solver (!solver)) x
+
+(* "Virtual constructors" for various propositional variables *)
+fun var_constrs (gp as GP (arities, gl)) =
+  let
+    val n = Int.max (num_graphs gp, num_prog_pts gp)
+    val k = foldl Int.max 1 arities
+
+    (* Injective, provided  a < 8, x < n, and i < k. *)
+    fun prod a x i j = ((j * k + i) * n + x) * 8 + a + 1
+
+    fun ES (g, i, j) = BoolVar (prod 0 g i j)
+    fun EW (g, i, j) = BoolVar (prod 1 g i j)
+    fun WEAK g       = BoolVar (prod 2 g 0 0)
+    fun STRICT g     = BoolVar (prod 3 g 0 0)
+    fun P (p, i)     = BoolVar (prod 4 p i 0)
+    fun GAM (g, i, j)= BoolVar (prod 5 g i j)
+    fun EPS (g, i)   = BoolVar (prod 6 g i 0)
+    fun TAG (p, i) b = BoolVar (prod 7 p i b)
+  in
+    (ES,EW,WEAK,STRICT,P,GAM,EPS,TAG)
+  end
+
+
+fun graph_info gp g =
+  let
+    val G (p, q, edgs) = graph_at (gp, g)
+  in
+    (g, p, q, arity gp p, arity gp q, edgs)
+  end
+
+
+(* Order-independent part of encoding *)
+
+fun encode_graphs bits gp =
+  let
+    val ng = num_graphs gp
+    val (ES,EW,_,_,_,_,_,TAG) = var_constrs gp
+
+    fun encode_constraint_strict 0 (x, y) = PropLogic.False
+      | encode_constraint_strict k (x, y) =
+        Or (And (TAG x (k - 1), Not (TAG y (k - 1))),
+            And (Equiv (TAG x (k - 1), TAG y (k - 1)),
+                 encode_constraint_strict (k - 1) (x, y)))
+
+    fun encode_constraint_weak k (x, y) =
+        Or (encode_constraint_strict k (x, y),
+            iforall k (fn i => Equiv (TAG x i, TAG y i)))
+
+    fun encode_graph (g, p, q, n, m, edges) =
+      let
+        fun encode_edge i j =
+          if exists (fn x => x = (i, GTR, j)) edges then
+            And (ES (g, i, j), EW (g, i, j))
+          else if not (exists (fn x => x = (i, GEQ, j)) edges) then
+            And (Not (ES (g, i, j)), Not (EW (g, i, j)))
+          else
+            And (
+              Equiv (ES (g, i, j),
+                     encode_constraint_strict bits ((p, i), (q, j))),
+              Equiv (EW (g, i, j),
+                     encode_constraint_weak bits ((p, i), (q, j))))
+       in
+        iforall2 n m encode_edge
+      end
+  in
+    iforall ng (encode_graph o graph_info gp)
+  end
+
+
+(* Order-specific part of encoding *)
+
+fun encode bits gp mu =
+  let
+    val ng = num_graphs gp
+    val (ES,EW,WEAK,STRICT,P,GAM,EPS,_) = var_constrs gp
+
+    fun encode_graph MAX (g, p, q, n, m, _) =
+        all [
+          Equiv (WEAK g,
+            iforall m (fn j =>
+              Implies (P (q, j),
+                iexists n (fn i =>
+                  And (P (p, i), EW (g, i, j)))))),
+          Equiv (STRICT g,
+            iforall m (fn j =>
+              Implies (P (q, j),
+                iexists n (fn i =>
+                  And (P (p, i), ES (g, i, j)))))),
+          iexists n (fn i => P (p, i))
+        ]
+      | encode_graph MIN (g, p, q, n, m, _) =
+        all [
+          Equiv (WEAK g,
+            iforall n (fn i =>
+              Implies (P (p, i),
+                iexists m (fn j =>
+                  And (P (q, j), EW (g, i, j)))))),
+          Equiv (STRICT g,
+            iforall n (fn i =>
+              Implies (P (p, i),
+                iexists m (fn j =>
+                  And (P (q, j), ES (g, i, j)))))),
+          iexists m (fn j => P (q, j))
+        ]
+      | encode_graph MS (g, p, q, n, m, _) =
+        all [
+          Equiv (WEAK g,
+            iforall m (fn j =>
+              Implies (P (q, j),
+                iexists n (fn i => GAM (g, i, j))))),
+          Equiv (STRICT g,
+            iexists n (fn i =>
+              And (P (p, i), Not (EPS (g, i))))),
+          iforall2 n m (fn i => fn j =>
+            Implies (GAM (g, i, j),
+              all [
+                P (p, i),
+                P (q, j),
+                EW (g, i, j),
+                Equiv (Not (EPS (g, i)), ES (g, i, j))])),
+          iforall n (fn i =>
+            Implies (And (P (p, i), EPS (g, i)),
+              exactly_one m (fn j => GAM (g, i, j))))
+        ]
+  in
+    all [
+      encode_graphs bits gp,
+      iforall ng (encode_graph mu o graph_info gp),
+      iforall ng (fn x => WEAK x),
+      iexists ng (fn x => STRICT x)
+    ]
+  end
+
+
+(*Generieren des level-mapping und diverser output*)
+fun mk_certificate bits label gp f =
+  let
+    val (ES,EW,WEAK,STRICT,P,GAM,EPS,TAG) = var_constrs gp
+    fun assign (PropLogic.BoolVar v) = the_default false (f v)
+    fun assignTag i j =
+      (fold (fn x => fn y => 2 * y + (if assign (TAG (i, j) x) then 1 else 0))
+        (bits - 1 downto 0) 0)
+
+    val level_mapping =
+      let fun prog_pt_mapping p =
+            map_filter (fn x => if assign (P(p, x)) then SOME (x, assignTag p x) else NONE)
+              (0 upto (arity gp p) - 1)
+      in map prog_pt_mapping (0 upto num_prog_pts gp - 1) end
+
+    val strict_list = filter (assign o STRICT) (0 upto num_graphs gp - 1)
+
+    fun covering_pair g bStrict j =
+      let
+        val (_, p, q, n, m, _) = graph_info gp g
+
+        fun cover        MAX j = find_index (fn i => assign (P (p, i))      andalso      assign (EW  (g, i, j))) (0 upto n - 1)
+          | cover        MS  k = find_index (fn i =>                                     assign (GAM (g, i, k))) (0 upto n - 1)
+          | cover        MIN i = find_index (fn j => assign (P (q, j))      andalso      assign (EW  (g, i, j))) (0 upto m - 1)
+        fun cover_strict MAX j = find_index (fn i => assign (P (p, i))      andalso      assign (ES  (g, i, j))) (0 upto n - 1)
+          | cover_strict MS  k = find_index (fn i => assign (GAM (g, i, k)) andalso not (assign (EPS (g, i)  ))) (0 upto n - 1)
+          | cover_strict MIN i = find_index (fn j => assign (P (q, j))      andalso      assign (ES  (g, i, j))) (0 upto m - 1)
+        val i = if bStrict then cover_strict label j else cover label j
+      in
+        find_first (fn x => fst x = i) (nth level_mapping (if label = MIN then q else p))
+      end
+  in
+    (label, level_mapping, strict_list, covering_pair)
+  end
+
+(*interface for the proof reconstruction*)
+fun generate_certificate use_tags labels gp =
+  let
+    val bits = if use_tags then ndigits gp else 0
+  in
+    get_first
+      (fn l => case sat_solver (encode bits gp l) of
+                 SatSolver.SATISFIABLE f => SOME (mk_certificate bits l gp f)
+               | _ => NONE)
+      labels
+  end
+end
diff -r 5a79ec2fedfb -r d41182a8135c 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	Tue Dec 16 08:46:07 2008 +0100
@@ -0,0 +1,324 @@
+(*  Title:       HOL/Tools/function_package/termination_data.ML
+    Author:      Alexander Krauss, TU Muenchen
+
+Context data for termination proofs
+*)
+
+
+signature TERMINATION =
+sig
+
+  type data
+  datatype cell = Less of thm | LessEq of (thm * thm) | None of (thm * thm) | False of thm
+
+  val mk_sumcases : data -> typ -> term list -> term
+
+  val note_measure : int -> term -> data -> data
+  val note_chain   : term -> term -> thm option -> data -> data
+  val note_descent : term -> term -> term -> cell -> data -> data
+
+  val get_num_points : data -> int
+  val get_types      : data -> int -> typ
+  val get_measures   : data -> int -> term list
+
+  (* read from cache *)
+  val get_chain      : data -> term -> term -> thm option option
+  val get_descent    : data -> term -> term -> term -> cell option
+
+  (* writes *)
+  val derive_descent  : theory -> tactic -> term -> term -> term -> data -> data
+  val derive_descents : theory -> tactic -> term -> data -> data
+
+  val dest_call : data -> term -> ((string * typ) list * int * term * int * term * term)
+
+  val CALLS : (term list * int -> tactic) -> int -> tactic
+
+  (* Termination tactics. Sequential composition via continuations. (2nd argument is the error continuation) *)
+  type ttac = (data -> int -> tactic) -> (data -> int -> tactic) -> data -> int -> tactic
+
+  val TERMINATION : Proof.context -> (data -> int -> tactic) -> int -> tactic
+
+  val REPEAT : ttac -> ttac
+
+  val wf_union_tac : tactic
+end
+
+
+
+structure Termination : TERMINATION =
+struct
+
+open FundefLib
+
+val term2_ord = prod_ord Term.fast_term_ord Term.fast_term_ord
+structure Term2tab = TableFun(type key = term * term val ord = term2_ord);
+structure Term3tab = TableFun(type key = term * (term * term) val ord = prod_ord Term.fast_term_ord term2_ord);
+
+(** Analyzing binary trees **)
+
+(* Skeleton of a tree structure *)
+
+datatype skel =
+  SLeaf of int (* index *)
+| SBranch of (skel * skel)
+
+
+(* abstract make and dest functions *)
+fun mk_tree leaf branch =
+  let fun mk (SLeaf i) = leaf i
+        | mk (SBranch (s, t)) = branch (mk s, mk t)
+  in mk end
+
+
+fun dest_tree split =
+  let fun dest (SLeaf i) x = [(i, x)]
+        | dest (SBranch (s, t)) x =
+          let val (l, r) = split x
+          in dest s l @ dest t r end
+  in dest end
+
+
+(* concrete versions for sum types *)
+fun is_inj (Const ("Sum_Type.Inl", _) $ _) = true
+  | is_inj (Const ("Sum_Type.Inr", _) $ _) = true
+  | is_inj _ = false
+
+fun dest_inl (Const ("Sum_Type.Inl", _) $ t) = SOME t
+  | dest_inl _ = NONE
+
+fun dest_inr (Const ("Sum_Type.Inr", _) $ t) = SOME t
+  | dest_inr _ = NONE
+
+
+fun mk_skel ps =
+  let
+    fun skel i ps =
+      if forall is_inj ps andalso not (null ps)
+      then let
+          val (j, s) = skel i (map_filter dest_inl ps)
+          val (k, t) = skel j (map_filter dest_inr ps)
+        in (k, SBranch (s, t)) end
+      else (i + 1, SLeaf i)
+  in
+    snd (skel 0 ps)
+  end
+
+(* compute list of types for nodes *)
+fun node_types sk T = dest_tree (fn Type ("+", [LT, RT]) => (LT, RT)) sk T |> map snd
+
+(* find index and raw term *)
+fun dest_inj (SLeaf i) trm = (i, trm)
+  | dest_inj (SBranch (s, t)) trm =
+    case dest_inl trm of
+      SOME trm' => dest_inj s trm'
+    | _ => dest_inj t (the (dest_inr trm))
+
+
+
+(** Matrix cell datatype **)
+
+datatype cell = Less of thm | LessEq of (thm * thm) | None of (thm * thm) | False of thm;
+
+
+type data =
+  skel                            (* structure of the sum type encoding "program points" *)
+  * (int -> typ)                  (* types of program points *)
+  * (term list Inttab.table)      (* measures for program points *)
+  * (thm option Term2tab.table)   (* which calls form chains? *)
+  * (cell Term3tab.table)         (* local descents *)
+
+
+fun map_measures f (p, T, M, C, D) = (p, T, f M, C, D)
+fun map_chains f   (p, T, M, C, D) = (p, T, M, f C, D)
+fun map_descent f  (p, T, M, C, D) = (p, T, M, C, f D)
+
+fun note_measure p m = map_measures (Inttab.insert_list (op aconv) (p, m))
+fun note_chain c1 c2 res = map_chains (Term2tab.update ((c1, c2), res))
+fun note_descent c m1 m2 res = map_descent (Term3tab.update ((c,(m1, m2)), res))
+
+(* Build case expression *)
+fun mk_sumcases (sk, _, _, _, _) T fs =
+  mk_tree (fn i => (nth fs i, domain_type (fastype_of (nth fs i))))
+          (fn ((f, fT), (g, gT)) => (SumTree.mk_sumcase fT gT T f g, SumTree.mk_sumT fT gT))
+          sk
+  |> fst
+
+fun mk_sum_skel rel =
+  let
+    val cs = FundefLib.dest_binop_list @{const_name "op Un"} rel
+    fun collect_pats (Const ("Collect", _) $ Abs (_, _, c)) =
+      let
+        val (Const ("op &", _) $ (Const ("op =", _) $ _ $ (Const ("Pair", _) $ r $ l)) $ Gam)
+          = Term.strip_qnt_body "Ex" c
+      in cons r o cons l end
+  in
+    mk_skel (fold collect_pats cs [])
+  end
+
+fun create ctxt T rel =
+  let
+    val sk = mk_sum_skel rel
+    val Ts = node_types sk T
+    val M = Inttab.make (map_index (apsnd (MeasureFunctions.get_measure_functions ctxt)) Ts)
+  in
+    (sk, nth Ts, M, Term2tab.empty, Term3tab.empty)
+  end
+
+fun get_num_points (sk, _, _, _, _) =
+  let
+    fun num (SLeaf i) = i + 1
+      | num (SBranch (s, t)) = num t
+  in num sk end
+
+fun get_types (_, T, _, _, _) = T
+fun get_measures (_, _, M, _, _) = Inttab.lookup_list M
+
+fun get_chain (_, _, _, C, _) c1 c2 =
+  Term2tab.lookup C (c1, c2)
+
+fun get_descent (_, _, _, _, D) c m1 m2 =
+  Term3tab.lookup D (c, (m1, m2))
+
+fun dest_call D (Const ("Collect", _) $ Abs (_, _, c)) =
+  let
+    val n = get_num_points D
+    val (sk, _, _, _, _) = D
+    val vs = Term.strip_qnt_vars "Ex" c
+
+    (* FIXME: throw error "dest_call" for malformed terms *)
+    val (Const ("op &", _) $ (Const ("op =", _) $ _ $ (Const ("Pair", _) $ r $ l)) $ Gam)
+      = Term.strip_qnt_body "Ex" c
+    val (p, l') = dest_inj sk l
+    val (q, r') = dest_inj sk r
+  in
+    (vs, p, l', q, r', Gam)
+  end
+  | dest_call D t = error "dest_call"
+
+
+fun derive_desc_aux thy tac c (vs, p, l', q, r', Gam) m1 m2 D =
+  case get_descent D c m1 m2 of
+    SOME _ => D
+  | NONE => let
+    fun cgoal rel =
+      Term.list_all (vs,
+        Logic.mk_implies (HOLogic.mk_Trueprop Gam,
+          HOLogic.mk_Trueprop (Const (rel, @{typ "nat => nat => bool"})
+            $ (m2 $ r') $ (m1 $ l'))))
+      |> cterm_of thy
+    in
+      note_descent c m1 m2
+        (case try_proof (cgoal @{const_name HOL.less}) tac of
+           Solved thm => Less thm
+         | Stuck thm =>
+           (case try_proof (cgoal @{const_name HOL.less_eq}) tac of
+              Solved thm2 => LessEq (thm2, thm)
+            | Stuck thm2 =>
+              if prems_of thm2 = [HOLogic.Trueprop $ HOLogic.false_const]
+              then False thm2 else None (thm2, thm)
+            | _ => raise Match) (* FIXME *)
+         | _ => raise Match) D
+      end
+
+fun derive_descent thy tac c m1 m2 D =
+  derive_desc_aux thy tac c (dest_call D c) m1 m2 D
+
+(* all descents in one go *)
+fun derive_descents thy tac c D =
+  let val cdesc as (vs, p, l', q, r', Gam) = dest_call D c
+  in fold_product (derive_desc_aux thy tac c cdesc)
+       (get_measures D p) (get_measures D q) D
+  end
+
+fun CALLS tac i st =
+  if Thm.no_prems st then all_tac st
+  else case Thm.term_of (Thm.cprem_of st i) of
+    (_ $ (_ $ rel)) => tac (FundefLib.dest_binop_list @{const_name "op Un"} rel, i) st
+  |_ => no_tac st
+
+type ttac = (data -> int -> tactic) -> (data -> int -> tactic) -> data -> int -> tactic
+
+fun TERMINATION ctxt tac =
+  SUBGOAL (fn (_ $ (Const (@{const_name "wf"}, wfT) $ rel), i) =>
+  let
+    val (T, _) = HOLogic.dest_prodT (HOLogic.dest_setT (domain_type wfT))
+  in
+    tac (create ctxt T rel) i
+  end)
+
+
+(* A tactic to convert open to closed termination goals *)
+local
+fun dest_term (t : term) = (* FIXME, cf. Lexicographic order *)
+    let
+      val (vars, prop) = FundefLib.dest_all_all t
+      val (prems, concl) = Logic.strip_horn prop
+      val (lhs, rhs) = concl
+                         |> HOLogic.dest_Trueprop
+                         |> HOLogic.dest_mem |> fst
+                         |> HOLogic.dest_prod
+    in
+      (vars, prems, lhs, rhs)
+    end
+
+fun mk_pair_compr (T, qs, l, r, conds) =
+    let
+      val pT = HOLogic.mk_prodT (T, T)
+      val n = length qs
+      val peq = HOLogic.eq_const pT $ Bound n $ (HOLogic.pair_const T T $ l $ r)
+      val conds' = if null conds then [HOLogic.true_const] else conds
+    in
+      HOLogic.Collect_const pT $
+      Abs ("uu_", pT,
+           (foldr1 HOLogic.mk_conj (peq :: conds')
+            |> fold_rev (fn v => fn t => HOLogic.exists_const (fastype_of v) $ lambda v t) qs))
+    end
+
+in
+
+fun wf_union_tac st =
+    let
+      val thy = theory_of_thm st
+      val cert = cterm_of (theory_of_thm st)
+      val ((trueprop $ (wf $ rel)) :: ineqs) = prems_of st
+
+      fun mk_compr ineq =
+          let
+            val (vars, prems, lhs, rhs) = dest_term ineq
+          in
+            mk_pair_compr (fastype_of lhs, vars, lhs, rhs, map (ObjectLogic.atomize_term thy) prems)
+          end
+
+      val relation =
+          if null ineqs then
+              Const (@{const_name "{}"}, fastype_of rel)
+          else
+              foldr1 (HOLogic.mk_binop @{const_name "op Un"}) (map mk_compr ineqs)
+
+      fun solve_membership_tac i =
+          (EVERY' (replicate (i - 2) (rtac @{thm UnI2}))  (* pick the right component of the union *)
+          THEN' (fn j => TRY (rtac @{thm UnI1} j))
+          THEN' (rtac @{thm CollectI})                    (* unfold comprehension *)
+          THEN' (fn i => REPEAT (rtac @{thm exI} i))      (* Turn existentials into schematic Vars *)
+          THEN' ((rtac @{thm refl})                       (* unification instantiates all Vars *)
+                 ORELSE' ((rtac @{thm conjI})
+                          THEN' (rtac @{thm refl})
+                          THEN' (CLASET' blast_tac)))     (* Solve rest of context... not very elegant *)
+          ) i
+    in
+      ((PRIMITIVE (Drule.cterm_instantiate [(cert rel, cert relation)])
+      THEN ALLGOALS (fn i => if i = 1 then all_tac else solve_membership_tac i))) st
+    end
+
+
+end
+
+
+(* continuation passing repeat combinator *)
+fun REPEAT ttac cont err_cont =
+    ttac (fn D => fn i => (REPEAT ttac cont cont D i)) err_cont
+
+
+
+
+end
diff -r 5a79ec2fedfb -r d41182a8135c src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Tue Dec 16 00:19:47 2008 +0100
+++ b/src/HOL/Wellfounded.thy	Tue Dec 16 08:46:07 2008 +0100
@@ -842,6 +842,11 @@
   qed
 qed
 
+lemma max_ext_additive: 
+ "(A, B) \<in> max_ext R \<Longrightarrow> (C, D) \<in> max_ext R \<Longrightarrow>
+  (A \<union> C, B \<union> D) \<in> max_ext R"
+by (force elim!: max_ext.cases)
+
 
 definition
   min_ext :: "('a \<times> 'a) set \<Rightarrow> ('a set \<times> 'a set) set" 
diff -r 5a79ec2fedfb -r d41182a8135c src/HOL/ex/ExecutableContent.thy
--- a/src/HOL/ex/ExecutableContent.thy	Tue Dec 16 00:19:47 2008 +0100
+++ b/src/HOL/ex/ExecutableContent.thy	Tue Dec 16 08:46:07 2008 +0100
@@ -24,4 +24,11 @@
   "~~/src/HOL/ex/Records"
 begin
 
+text {* However, some aren't executable *}
+
+declare pair_leq_def[code del]
+declare max_weak_def[code del]
+declare min_weak_def[code del]
+declare ms_weak_def[code del]
+
 end