# HG changeset patch
# User blanchet
# Date 1390249961 -3600
# Node ID 0e8e4dc558664de0e71ca8cf1c6638af3e5184cd
# Parent  8ee9aabb2bca8e4394e68a43c3e371129dfc45e6
moved 'fundef_cong' attribute (and other basic 'fun' stuff) up the dependency chain

diff -r 8ee9aabb2bca -r 0e8e4dc55866 src/HOL/BNF_Def.thy
--- a/src/HOL/BNF_Def.thy	Mon Jan 20 20:42:43 2014 +0100
+++ b/src/HOL/BNF_Def.thy	Mon Jan 20 21:32:41 2014 +0100
@@ -8,9 +8,7 @@
 header {* Definition of Bounded Natural Functors *}
 
 theory BNF_Def
-imports BNF_Util
-   (*FIXME: register fundef_cong attribute in an interpretation to remove this dependency*)
-  FunDef
+imports BNF_Util Fun_Def_Base
 keywords
   "print_bnfs" :: diag and
   "bnf" :: thy_goal
diff -r 8ee9aabb2bca -r 0e8e4dc55866 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Mon Jan 20 20:42:43 2014 +0100
+++ b/src/HOL/Divides.thy	Mon Jan 20 21:32:41 2014 +0100
@@ -1062,10 +1062,10 @@
    \<Longrightarrow> divmod_nat_rel a (b * c) (q div c, b *(q mod c) + r)"
 by (auto simp add: mult_ac divmod_nat_rel_def add_mult_distrib2 [symmetric] mod_lemma)
 
-lemma div_mult2_eq: "a div (b*c) = (a div b) div (c::nat)"
+lemma div_mult2_eq: "a div (b * c) = (a div b) div (c::nat)"
 by (force simp add: divmod_nat_rel [THEN divmod_nat_rel_mult2_eq, THEN div_nat_unique])
 
-lemma mod_mult2_eq: "a mod (b*c) = b*(a div b mod c) + a mod (b::nat)"
+lemma mod_mult2_eq: "a mod (b * c) = b * (a div b mod c) + a mod (b::nat)"
 by (auto simp add: mult_commute divmod_nat_rel [THEN divmod_nat_rel_mult2_eq, THEN mod_nat_unique])
 
 
@@ -2136,7 +2136,7 @@
   using mod_div_equality [of m n] by arith
 
 
-subsubsection {* Proving  @{term "a div (b*c) = (a div b) div c"} *}
+subsubsection {* Proving  @{term "a div (b * c) = (a div b) div c"} *}
 
 (*The condition c>0 seems necessary.  Consider that 7 div ~6 = ~2 but
   7 div 2 div ~3 = 3 div ~3 = ~1.  The subcase (a div b) mod c = 0 seems
@@ -2144,7 +2144,7 @@
 
 text{*first, four lemmas to bound the remainder for the cases b<0 and b>0 *}
 
-lemma zmult2_lemma_aux1: "[| (0::int) < c;  b < r;  r \<le> 0 |] ==> b*c < b*(q mod c) + r"
+lemma zmult2_lemma_aux1: "[| (0::int) < c;  b < r;  r \<le> 0 |] ==> b * c < b * (q mod c) + r"
 apply (subgoal_tac "b * (c - q mod c) < r * 1")
  apply (simp add: algebra_simps)
 apply (rule order_le_less_trans)
diff -r 8ee9aabb2bca -r 0e8e4dc55866 src/HOL/FunDef.thy
--- a/src/HOL/FunDef.thy	Mon Jan 20 20:42:43 2014 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,321 +0,0 @@
-(*  Title:      HOL/FunDef.thy
-    Author:     Alexander Krauss, TU Muenchen
-*)
-
-header {* Function Definitions and Termination Proofs *}
-
-theory FunDef
-imports Partial_Function SAT Wellfounded
-keywords "function" "termination" :: thy_goal and "fun" "fun_cases" :: thy_decl
-begin
-
-subsection {* Definitions with default value. *}
-
-definition
-  THE_default :: "'a \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a" where
-  "THE_default d P = (if (\<exists>!x. P x) then (THE x. P x) else d)"
-
-lemma THE_defaultI': "\<exists>!x. P x \<Longrightarrow> P (THE_default d P)"
-  by (simp add: theI' THE_default_def)
-
-lemma THE_default1_equality:
-    "\<lbrakk>\<exists>!x. P x; P a\<rbrakk> \<Longrightarrow> THE_default d P = a"
-  by (simp add: the1_equality THE_default_def)
-
-lemma THE_default_none:
-    "\<not>(\<exists>!x. P x) \<Longrightarrow> THE_default d P = d"
-  by (simp add:THE_default_def)
-
-
-lemma fundef_ex1_existence:
-  assumes f_def: "f == (\<lambda>x::'a. THE_default (d x) (\<lambda>y. G x y))"
-  assumes ex1: "\<exists>!y. G x y"
-  shows "G x (f x)"
-  apply (simp only: f_def)
-  apply (rule THE_defaultI')
-  apply (rule ex1)
-  done
-
-lemma fundef_ex1_uniqueness:
-  assumes f_def: "f == (\<lambda>x::'a. THE_default (d x) (\<lambda>y. G x y))"
-  assumes ex1: "\<exists>!y. G x y"
-  assumes elm: "G x (h x)"
-  shows "h x = f x"
-  apply (simp only: f_def)
-  apply (rule THE_default1_equality [symmetric])
-   apply (rule ex1)
-  apply (rule elm)
-  done
-
-lemma fundef_ex1_iff:
-  assumes f_def: "f == (\<lambda>x::'a. THE_default (d x) (\<lambda>y. G x y))"
-  assumes ex1: "\<exists>!y. G x y"
-  shows "(G x y) = (f x = y)"
-  apply (auto simp:ex1 f_def THE_default1_equality)
-  apply (rule THE_defaultI')
-  apply (rule ex1)
-  done
-
-lemma fundef_default_value:
-  assumes f_def: "f == (\<lambda>x::'a. THE_default (d x) (\<lambda>y. G x y))"
-  assumes graph: "\<And>x y. G x y \<Longrightarrow> D x"
-  assumes "\<not> D x"
-  shows "f x = d x"
-proof -
-  have "\<not>(\<exists>y. G x y)"
-  proof
-    assume "\<exists>y. G x y"
-    hence "D x" using graph ..
-    with `\<not> D x` show False ..
-  qed
-  hence "\<not>(\<exists>!y. G x y)" by blast
-
-  thus ?thesis
-    unfolding f_def
-    by (rule THE_default_none)
-qed
-
-definition in_rel_def[simp]:
-  "in_rel R x y == (x, y) \<in> R"
-
-lemma wf_in_rel:
-  "wf R \<Longrightarrow> wfP (in_rel R)"
-  by (simp add: wfP_def)
-
-ML_file "Tools/Function/function_common.ML"
-ML_file "Tools/Function/context_tree.ML"
-ML_file "Tools/Function/function_core.ML"
-ML_file "Tools/Function/sum_tree.ML"
-ML_file "Tools/Function/mutual.ML"
-ML_file "Tools/Function/pattern_split.ML"
-ML_file "Tools/Function/relation.ML"
-ML_file "Tools/Function/function_elims.ML"
-
-method_setup relation = {*
-  Args.term >> (fn t => fn ctxt => SIMPLE_METHOD' (Function_Relation.relation_infer_tac ctxt t))
-*} "prove termination using a user-specified wellfounded relation"
-
-ML_file "Tools/Function/function.ML"
-ML_file "Tools/Function/pat_completeness.ML"
-
-method_setup pat_completeness = {*
-  Scan.succeed (SIMPLE_METHOD' o Pat_Completeness.pat_completeness_tac)
-*} "prove completeness of datatype patterns"
-
-ML_file "Tools/Function/fun.ML"
-ML_file "Tools/Function/induction_schema.ML"
-
-method_setup induction_schema = {*
-  Scan.succeed (RAW_METHOD o Induction_Schema.induction_schema_tac)
-*} "prove an induction principle"
-
-setup {*
-  Function.setup
-  #> Function_Fun.setup
-*}
-
-subsection {* Measure Functions *}
-
-inductive is_measure :: "('a \<Rightarrow> nat) \<Rightarrow> bool"
-where is_measure_trivial: "is_measure f"
-
-ML_file "Tools/Function/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)
-
-ML_file "Tools/Function/lexicographic_order.ML"
-
-method_setup lexicographic_order = {*
-  Method.sections clasimp_modifiers >>
-  (K (SIMPLE_METHOD o Lexicographic_Order.lexicographic_order_tac false))
-*} "termination prover for lexicographic orderings"
-
-setup Lexicographic_Order.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
-
-lemmas [fundef_cong] =
-  if_cong image_cong INT_cong UN_cong
-  bex_cong ball_cong imp_cong Option.map_cong Option.bind_cong
-
-lemma split_cong [fundef_cong]:
-  "(\<And>x y. (x, y) = q \<Longrightarrow> f x y = g x y) \<Longrightarrow> p = q
-    \<Longrightarrow> split f p = split g q"
-  by (auto simp: split_def)
-
-lemma comp_cong [fundef_cong]:
-  "f (g x) = f' (g' x') \<Longrightarrow> (f o g) x = (f' o g') x'"
-  unfolding o_apply .
-
-subsection {* Simp rules for termination proofs *}
-
-lemma termination_basic_simps[termination_simp]:
-  "x < (y::nat) \<Longrightarrow> x < y + z"
-  "x < z \<Longrightarrow> x < y + z"
-  "x \<le> y \<Longrightarrow> x \<le> y + (z::nat)"
-  "x \<le> z \<Longrightarrow> x \<le> y + (z::nat)"
-  "x < y \<Longrightarrow> x \<le> (y::nat)"
-by arith+
-
-declare le_imp_less_Suc[termination_simp]
-
-lemma prod_size_simp[termination_simp]:
-  "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> fst P O snd P \<subseteq> fst P)"
-
-lemma reduction_pairI[intro]: "wf R \<Longrightarrow> R O S \<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)" "fst P O S \<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 @{text pair_less}/@{text 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 "R O S \<subseteq> R"
-  shows "max_ext R O (max_ext S \<union> {({},{})}) \<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 "R O S \<subseteq> R"
-  shows "min_ext R O  (min_ext S \<union> {({},{})}) \<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 *}
-
-ML_file "Tools/Function/termination.ML"
-ML_file "Tools/Function/scnp_solve.ML"
-ML_file "Tools/Function/scnp_reconstruct.ML"
-ML_file "Tools/Function/fun_cases.ML"
-
-setup ScnpReconstruct.setup
-
-ML_val -- "setup inactive"
-{*
-  Context.theory_map (Function_Common.set_termination_prover
-    (ScnpReconstruct.decomp_scnp_tac [ScnpSolve.MAX, ScnpSolve.MIN, ScnpSolve.MS]))
-*}
-
-end
diff -r 8ee9aabb2bca -r 0e8e4dc55866 src/HOL/Fun_Def.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Fun_Def.thy	Mon Jan 20 21:32:41 2014 +0100
@@ -0,0 +1,319 @@
+(*  Title:      HOL/Fun_Def.thy
+    Author:     Alexander Krauss, TU Muenchen
+*)
+
+header {* Function Definitions and Termination Proofs *}
+
+theory Fun_Def
+imports Partial_Function SAT
+keywords "function" "termination" :: thy_goal and "fun" "fun_cases" :: thy_decl
+begin
+
+subsection {* Definitions with default value *}
+
+definition
+  THE_default :: "'a \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a" where
+  "THE_default d P = (if (\<exists>!x. P x) then (THE x. P x) else d)"
+
+lemma THE_defaultI': "\<exists>!x. P x \<Longrightarrow> P (THE_default d P)"
+  by (simp add: theI' THE_default_def)
+
+lemma THE_default1_equality:
+    "\<lbrakk>\<exists>!x. P x; P a\<rbrakk> \<Longrightarrow> THE_default d P = a"
+  by (simp add: the1_equality THE_default_def)
+
+lemma THE_default_none:
+    "\<not>(\<exists>!x. P x) \<Longrightarrow> THE_default d P = d"
+  by (simp add:THE_default_def)
+
+
+lemma fundef_ex1_existence:
+  assumes f_def: "f == (\<lambda>x::'a. THE_default (d x) (\<lambda>y. G x y))"
+  assumes ex1: "\<exists>!y. G x y"
+  shows "G x (f x)"
+  apply (simp only: f_def)
+  apply (rule THE_defaultI')
+  apply (rule ex1)
+  done
+
+lemma fundef_ex1_uniqueness:
+  assumes f_def: "f == (\<lambda>x::'a. THE_default (d x) (\<lambda>y. G x y))"
+  assumes ex1: "\<exists>!y. G x y"
+  assumes elm: "G x (h x)"
+  shows "h x = f x"
+  apply (simp only: f_def)
+  apply (rule THE_default1_equality [symmetric])
+   apply (rule ex1)
+  apply (rule elm)
+  done
+
+lemma fundef_ex1_iff:
+  assumes f_def: "f == (\<lambda>x::'a. THE_default (d x) (\<lambda>y. G x y))"
+  assumes ex1: "\<exists>!y. G x y"
+  shows "(G x y) = (f x = y)"
+  apply (auto simp:ex1 f_def THE_default1_equality)
+  apply (rule THE_defaultI')
+  apply (rule ex1)
+  done
+
+lemma fundef_default_value:
+  assumes f_def: "f == (\<lambda>x::'a. THE_default (d x) (\<lambda>y. G x y))"
+  assumes graph: "\<And>x y. G x y \<Longrightarrow> D x"
+  assumes "\<not> D x"
+  shows "f x = d x"
+proof -
+  have "\<not>(\<exists>y. G x y)"
+  proof
+    assume "\<exists>y. G x y"
+    hence "D x" using graph ..
+    with `\<not> D x` show False ..
+  qed
+  hence "\<not>(\<exists>!y. G x y)" by blast
+
+  thus ?thesis
+    unfolding f_def
+    by (rule THE_default_none)
+qed
+
+definition in_rel_def[simp]:
+  "in_rel R x y == (x, y) \<in> R"
+
+lemma wf_in_rel:
+  "wf R \<Longrightarrow> wfP (in_rel R)"
+  by (simp add: wfP_def)
+
+ML_file "Tools/Function/function_core.ML"
+ML_file "Tools/Function/sum_tree.ML"
+ML_file "Tools/Function/mutual.ML"
+ML_file "Tools/Function/pattern_split.ML"
+ML_file "Tools/Function/relation.ML"
+ML_file "Tools/Function/function_elims.ML"
+
+method_setup relation = {*
+  Args.term >> (fn t => fn ctxt => SIMPLE_METHOD' (Function_Relation.relation_infer_tac ctxt t))
+*} "prove termination using a user-specified wellfounded relation"
+
+ML_file "Tools/Function/function.ML"
+ML_file "Tools/Function/pat_completeness.ML"
+
+method_setup pat_completeness = {*
+  Scan.succeed (SIMPLE_METHOD' o Pat_Completeness.pat_completeness_tac)
+*} "prove completeness of datatype patterns"
+
+ML_file "Tools/Function/fun.ML"
+ML_file "Tools/Function/induction_schema.ML"
+
+method_setup induction_schema = {*
+  Scan.succeed (RAW_METHOD o Induction_Schema.induction_schema_tac)
+*} "prove an induction principle"
+
+setup {*
+  Function.setup
+  #> Function_Fun.setup
+*}
+
+subsection {* Measure Functions *}
+
+inductive is_measure :: "('a \<Rightarrow> nat) \<Rightarrow> bool"
+where is_measure_trivial: "is_measure f"
+
+ML_file "Tools/Function/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)
+
+ML_file "Tools/Function/lexicographic_order.ML"
+
+method_setup lexicographic_order = {*
+  Method.sections clasimp_modifiers >>
+  (K (SIMPLE_METHOD o Lexicographic_Order.lexicographic_order_tac false))
+*} "termination prover for lexicographic orderings"
+
+setup Lexicographic_Order.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
+
+lemmas [fundef_cong] =
+  if_cong image_cong INT_cong UN_cong
+  bex_cong ball_cong imp_cong Option.map_cong Option.bind_cong
+
+lemma split_cong [fundef_cong]:
+  "(\<And>x y. (x, y) = q \<Longrightarrow> f x y = g x y) \<Longrightarrow> p = q
+    \<Longrightarrow> split f p = split g q"
+  by (auto simp: split_def)
+
+lemma comp_cong [fundef_cong]:
+  "f (g x) = f' (g' x') \<Longrightarrow> (f o g) x = (f' o g') x'"
+  unfolding o_apply .
+
+subsection {* Simp rules for termination proofs *}
+
+lemma termination_basic_simps[termination_simp]:
+  "x < (y::nat) \<Longrightarrow> x < y + z"
+  "x < z \<Longrightarrow> x < y + z"
+  "x \<le> y \<Longrightarrow> x \<le> y + (z::nat)"
+  "x \<le> z \<Longrightarrow> x \<le> y + (z::nat)"
+  "x < y \<Longrightarrow> x \<le> (y::nat)"
+by arith+
+
+declare le_imp_less_Suc[termination_simp]
+
+lemma prod_size_simp[termination_simp]:
+  "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> fst P O snd P \<subseteq> fst P)"
+
+lemma reduction_pairI[intro]: "wf R \<Longrightarrow> R O S \<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)" "fst P O S \<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 @{text pair_less}/@{text 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 "R O S \<subseteq> R"
+  shows "max_ext R O (max_ext S \<union> {({},{})}) \<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 "R O S \<subseteq> R"
+  shows "min_ext R O  (min_ext S \<union> {({},{})}) \<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 *}
+
+ML_file "Tools/Function/termination.ML"
+ML_file "Tools/Function/scnp_solve.ML"
+ML_file "Tools/Function/scnp_reconstruct.ML"
+ML_file "Tools/Function/fun_cases.ML"
+
+setup ScnpReconstruct.setup
+
+ML_val -- "setup inactive"
+{*
+  Context.theory_map (Function_Common.set_termination_prover
+    (ScnpReconstruct.decomp_scnp_tac [ScnpSolve.MAX, ScnpSolve.MIN, ScnpSolve.MS]))
+*}
+
+end
diff -r 8ee9aabb2bca -r 0e8e4dc55866 src/HOL/Fun_Def_Base.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Fun_Def_Base.thy	Mon Jan 20 21:32:41 2014 +0100
@@ -0,0 +1,16 @@
+(*  Title:      HOL/Fun_Def_Base.thy
+    Author:     Alexander Krauss, TU Muenchen
+*)
+
+header {* Function Definition Base *}
+
+theory Fun_Def_Base
+imports Ctr_Sugar Set Wellfounded
+begin
+
+ML_file "Tools/Function/function_lib.ML"
+ML_file "Tools/Function/function_common.ML"
+ML_file "Tools/Function/context_tree.ML"
+setup Function_Ctx_Tree.setup
+
+end
diff -r 8ee9aabb2bca -r 0e8e4dc55866 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Mon Jan 20 20:42:43 2014 +0100
+++ b/src/HOL/Int.thy	Mon Jan 20 21:32:41 2014 +0100
@@ -6,7 +6,7 @@
 header {* The Integers as Equivalence Classes over Pairs of Natural Numbers *} 
 
 theory Int
-imports Equiv_Relations Wellfounded Quotient FunDef
+imports Equiv_Relations Wellfounded Quotient Fun_Def
 begin
 
 subsection {* Definition of integers as a quotient type *}
diff -r 8ee9aabb2bca -r 0e8e4dc55866 src/HOL/Lifting_Product.thy
--- a/src/HOL/Lifting_Product.thy	Mon Jan 20 20:42:43 2014 +0100
+++ b/src/HOL/Lifting_Product.thy	Mon Jan 20 21:32:41 2014 +0100
@@ -17,15 +17,8 @@
   "prod_pred P1 P2 (a, b) \<longleftrightarrow> P1 a \<and> P2 b"
   by (simp add: prod_pred_def)
 
-lemma prod_rel_eq [relator_eq]:
-  shows "prod_rel (op =) (op =) = (op =)"
-  by (simp add: fun_eq_iff)
-
-lemma prod_rel_mono[relator_mono]:
-  assumes "A \<le> C"
-  assumes "B \<le> D"
-  shows "(prod_rel A B) \<le> (prod_rel C D)"
-using assms by (auto simp: prod_rel_def)
+lemmas prod_rel_eq[relator_eq] = prod.rel_eq
+lemmas prod_rel_mono[relator_mono] = prod.rel_mono
 
 lemma prod_rel_OO[relator_distr]:
   "(prod_rel A B) OO (prod_rel C D) = prod_rel (A OO C) (B OO D)"
diff -r 8ee9aabb2bca -r 0e8e4dc55866 src/HOL/Partial_Function.thy
--- a/src/HOL/Partial_Function.thy	Mon Jan 20 20:42:43 2014 +0100
+++ b/src/HOL/Partial_Function.thy	Mon Jan 20 21:32:41 2014 +0100
@@ -5,11 +5,10 @@
 header {* Partial Function Definitions *}
 
 theory Partial_Function
-imports Complete_Partial_Order Option
+imports Complete_Partial_Order Fun_Def_Base Option
 keywords "partial_function" :: thy_decl
 begin
 
-ML_file "Tools/Function/function_lib.ML"
 ML_file "Tools/Function/partial_function.ML"
 setup Partial_Function.setup
 
diff -r 8ee9aabb2bca -r 0e8e4dc55866 src/HOL/Set_Interval.thy
--- a/src/HOL/Set_Interval.thy	Mon Jan 20 20:42:43 2014 +0100
+++ b/src/HOL/Set_Interval.thy	Mon Jan 20 21:32:41 2014 +0100
@@ -827,8 +827,8 @@
 subset is exactly that interval. *}
 
 lemma subset_card_intvl_is_intvl:
-  assumes "A \<subseteq> {k..<k+card A}"
-  shows "A = {k..<k+card A}"
+  assumes "A \<subseteq> {k..<k + card A}"
+  shows "A = {k..<k + card A}"
 proof (cases "finite A")
   case True
   from this and assms show ?thesis
@@ -837,7 +837,7 @@
   next
     case (insert b A)
     hence *: "b \<notin> A" by auto
-    with insert have "A <= {k..<k+card A}" and "b = k+card A"
+    with insert have "A <= {k..<k + card A}" and "b = k + card A"
       by fastforce+
     with insert * show ?case by auto
   qed
diff -r 8ee9aabb2bca -r 0e8e4dc55866 src/HOL/Tools/Function/context_tree.ML
--- a/src/HOL/Tools/Function/context_tree.ML	Mon Jan 20 20:42:43 2014 +0100
+++ b/src/HOL/Tools/Function/context_tree.ML	Mon Jan 20 21:32:41 2014 +0100
@@ -35,6 +35,8 @@
 
   val rewrite_by_tree : Proof.context -> term -> thm -> (thm * thm) list ->
     ctx_tree -> thm * (thm * thm) list
+
+  val setup : theory -> theory
 end
 
 structure Function_Ctx_Tree : FUNCTION_CTXTREE =
@@ -286,4 +288,8 @@
     rewrite_help [] [] x tr
   end
 
+val setup =
+  Attrib.setup @{binding fundef_cong} (Attrib.add_del cong_add cong_del)
+    "declaration of congruence rule for function definitions"
+
 end
diff -r 8ee9aabb2bca -r 0e8e4dc55866 src/HOL/Tools/Function/function.ML
--- a/src/HOL/Tools/Function/function.ML	Mon Jan 20 20:42:43 2014 +0100
+++ b/src/HOL/Tools/Function/function.ML	Mon Jan 20 21:32:41 2014 +0100
@@ -278,10 +278,7 @@
 (* setup *)
 
 val setup =
-  Attrib.setup @{binding fundef_cong}
-    (Attrib.add_del Function_Ctx_Tree.cong_add Function_Ctx_Tree.cong_del)
-    "declaration of congruence rule for function definitions"
-  #> setup_case_cong
+  setup_case_cong
   #> Function_Common.Termination_Simps.setup
 
 val get_congs = Function_Ctx_Tree.get_function_congs
diff -r 8ee9aabb2bca -r 0e8e4dc55866 src/HOL/Tools/Function/function_core.ML
--- a/src/HOL/Tools/Function/function_core.ML	Mon Jan 20 20:42:43 2014 +0100
+++ b/src/HOL/Tools/Function/function_core.ML	Mon Jan 20 21:32:41 2014 +0100
@@ -81,14 +81,14 @@
 (* Theory dependencies. *)
 val acc_induct_rule = @{thm accp_induct_rule}
 
-val ex1_implies_ex = @{thm FunDef.fundef_ex1_existence}
-val ex1_implies_un = @{thm FunDef.fundef_ex1_uniqueness}
-val ex1_implies_iff = @{thm FunDef.fundef_ex1_iff}
+val ex1_implies_ex = @{thm Fun_Def.fundef_ex1_existence}
+val ex1_implies_un = @{thm Fun_Def.fundef_ex1_uniqueness}
+val ex1_implies_iff = @{thm Fun_Def.fundef_ex1_iff}
 
 val acc_downward = @{thm accp_downward}
 val accI = @{thm accp.accI}
 val case_split = @{thm HOL.case_split}
-val fundef_default_value = @{thm FunDef.fundef_default_value}
+val fundef_default_value = @{thm Fun_Def.fundef_default_value}
 val not_acc_down = @{thm not_accp_down}
 
 
@@ -494,7 +494,7 @@
 fun define_function fdefname (fname, mixfix) domT ranT G default lthy =
   let
     val f_def =
-      Abs ("x", domT, Const (@{const_name FunDef.THE_default}, ranT --> (ranT --> boolT) --> ranT)
+      Abs ("x", domT, Const (@{const_name Fun_Def.THE_default}, ranT --> (ranT --> boolT) --> ranT)
         $ (default $ Bound 0) $ Abs ("y", ranT, G $ Bound 1 $ Bound 0))
       |> Syntax.check_term lthy
   in
@@ -718,8 +718,8 @@
 (** Termination rule **)
 
 val wf_induct_rule = @{thm Wellfounded.wfP_induct_rule}
-val wf_in_rel = @{thm FunDef.wf_in_rel}
-val in_rel_def = @{thm FunDef.in_rel_def}
+val wf_in_rel = @{thm Fun_Def.wf_in_rel}
+val in_rel_def = @{thm Fun_Def.in_rel_def}
 
 fun mk_nest_term_case ctxt globals R' ihyp clause =
   let
@@ -780,7 +780,7 @@
     val R' = Free ("R", fastype_of R)
 
     val Rrel = Free ("R", HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)))
-    val inrel_R = Const (@{const_name FunDef.in_rel},
+    val inrel_R = Const (@{const_name Fun_Def.in_rel},
       HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)) --> fastype_of R) $ Rrel
 
     val wfR' = HOLogic.mk_Trueprop (Const (@{const_name Wellfounded.wfP},