src/HOL/Fun_Def.thy
 changeset 56643 41d3596d8a64 parent 56248 67dc9549fa15 child 56846 9df717fef2bb
```     1.1 --- a/src/HOL/Fun_Def.thy	Wed Apr 23 10:23:26 2014 +0200
1.2 +++ b/src/HOL/Fun_Def.thy	Wed Apr 23 10:23:27 2014 +0200
1.3 @@ -111,7 +111,8 @@
1.4    #> Function_Fun.setup
1.5  *}
1.6
1.7 -subsection {* Measure Functions *}
1.8 +
1.9 +subsection {* Measure functions *}
1.10
1.11  inductive is_measure :: "('a \<Rightarrow> nat) \<Rightarrow> bool"
1.12  where is_measure_trivial: "is_measure f"
1.13 @@ -137,7 +138,7 @@
1.14  setup Lexicographic_Order.setup
1.15
1.16
1.17 -subsection {* Congruence Rules *}
1.18 +subsection {* Congruence rules *}
1.19
1.20  lemma let_cong [fundef_cong]:
1.21    "M = N \<Longrightarrow> (\<And>x. x = N \<Longrightarrow> f x = g x) \<Longrightarrow> Let M f = Let N g"
1.22 @@ -156,22 +157,22 @@
1.23    "f (g x) = f' (g' x') \<Longrightarrow> (f o g) x = (f' o g') x'"
1.24    unfolding o_apply .
1.25
1.26 +
1.27  subsection {* Simp rules for termination proofs *}
1.28
1.29 -lemma termination_basic_simps[termination_simp]:
1.30 -  "x < (y::nat) \<Longrightarrow> x < y + z"
1.31 -  "x < z \<Longrightarrow> x < y + z"
1.32 -  "x \<le> y \<Longrightarrow> x \<le> y + (z::nat)"
1.33 -  "x \<le> z \<Longrightarrow> x \<le> y + (z::nat)"
1.34 -  "x < y \<Longrightarrow> x \<le> (y::nat)"
1.35 -by arith+
1.36 -
1.37 -declare le_imp_less_Suc[termination_simp]
1.38 +declare
1.43 +  less_imp_le_nat[termination_simp]
1.44 +  le_imp_less_Suc[termination_simp]
1.45
1.46  lemma prod_size_simp[termination_simp]:
1.47    "prod_size f g p = f (fst p) + g (snd p) + Suc 0"
1.48  by (induct p) auto
1.49
1.50 +
1.51  subsection {* Decomposition *}
1.52
1.53  lemma less_by_empty:
1.54 @@ -185,7 +186,7 @@
1.55  by (auto simp add: wf_comp_self[of R])
1.56
1.57
1.58 -subsection {* Reduction Pairs *}
1.59 +subsection {* Reduction pairs *}
1.60
1.61  definition
1.62    "reduction_pair P = (wf (fst P) \<and> fst P O snd P \<subseteq> fst P)"
```