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.39 +  trans_less_add1[termination_simp]
    1.40 +  trans_less_add2[termination_simp]
    1.41 +  trans_le_add1[termination_simp]
    1.42 +  trans_le_add2[termination_simp]
    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)"