src/HOL/Fun_Def.thy

 setup {*
   Function.setup
   #> Function_Fun.setup
 *}
 
-subsection {* Measure Functions *}
+
+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"

 *} "termination prover for lexicographic orderings"
 
 setup Lexicographic_Order.setup
 
 
-subsection {* Congruence Rules *}
+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
 

 
 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]
+declare
+  trans_less_add1[termination_simp]
+  trans_less_add2[termination_simp]
+  trans_le_add1[termination_simp]
+  trans_le_add2[termination_simp]
+  less_imp_le_nat[termination_simp]
+  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 wf_no_loop:
   "R O R = {} \<Longrightarrow> wf R"
 by (auto simp add: wf_comp_self[of R])
 
 
-subsection {* Reduction Pairs *}
+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)"