* New attribute "termination_simp": Simp rules for termination proofs
* General lemmas about list_size

--- a/doc-src/IsarAdvanced/Functions/Thy/Functions.thy	Fri Apr 25 15:30:33 2008 +0200
+++ b/doc-src/IsarAdvanced/Functions/Thy/Functions.thy	Fri Apr 25 16:28:06 2008 +0200
@@ -582,7 +582,7 @@
 | "fib2 1 = 1"
 | "fib2 (n + 2) = fib2 n + fib2 (Suc n)"
 
-(*<*)ML "goals_limit := 1"(*>*)
+(*<*)ML_val "goals_limit := 1"(*>*)
 txt {*
   This kind of matching is again justified by the proof of pattern
   completeness and compatibility. 
@@ -599,7 +599,7 @@
   existentials, which can then be soved by the arithmetic decision procedure.
   Pattern compatibility and termination are automatic as usual.
 *}
-(*<*)ML "goals_limit := 10"(*>*)
+(*<*)ML_val "goals_limit := 10"(*>*)
 apply atomize_elim
 apply arith
 apply auto
@@ -1152,14 +1152,11 @@
 text {* \noindent We can define a function which swaps the left and right subtrees recursively, using the 
   list functions @{const rev} and @{const map}: *}
 
-lemma [simp]: "x \<in> set l \<Longrightarrow> f x < Suc (list_size f l)"
-by (induct l) auto
-
-
-fun mirror :: "'a tree \<Rightarrow> 'a tree"
+function mirror :: "'a tree \<Rightarrow> 'a tree"
 where
   "mirror (Leaf n) = Leaf n"
 | "mirror (Branch l) = Branch (rev (map mirror l))"
+by pat_completeness auto
 
 
 text {*

--- a/src/HOL/FunDef.thy	Fri Apr 25 15:30:33 2008 +0200
+++ b/src/HOL/FunDef.thy	Fri Apr 25 16:28:06 2008 +0200
@@ -135,4 +135,10 @@
   "f (g x) = f' (g' x') \<Longrightarrow> (f o g) x = (f' o g') x'"
   unfolding o_apply .
 
+lemma termination_basic_simps[termination_simp]:
+  "x < y \<Longrightarrow> x < Suc y"
+  "x < (y::nat) \<Longrightarrow> x < y + z" 
+  "x < z \<Longrightarrow> x < y + z"
+by arith+
+
 end

--- a/src/HOL/List.thy	Fri Apr 25 15:30:33 2008 +0200
+++ b/src/HOL/List.thy	Fri Apr 25 16:28:06 2008 +0200
@@ -3265,6 +3265,15 @@
 setup StringSyntax.setup
 
 
+subsection {* Size function *}
+
+declare [[measure_function "list_size size"]]
+
+lemma list_size_estimation[termination_simp]:
+  "x \<in> set xs \<Longrightarrow> f x < list_size f xs"
+by (induct xs) auto
+
+
 subsection {* Code generator *}
 
 subsubsection {* Setup *}

--- a/src/HOL/Tools/function_package/fundef_common.ML	Fri Apr 25 15:30:33 2008 +0200
+++ b/src/HOL/Tools/function_package/fundef_common.ML	Fri Apr 25 16:28:06 2008 +0200
@@ -119,6 +119,11 @@
 
 val all_fundef_data = NetRules.rules o FundefData.get
 
+structure TerminationSimps = NamedThmsFun(
+  val name = "termination_simp" 
+  val description = "Simplification rule for termination proofs"
+);
+
 structure TerminationRule = GenericDataFun
 (
   type T = thm list

--- a/src/HOL/Tools/function_package/fundef_package.ML	Fri Apr 25 15:30:33 2008 +0200
+++ b/src/HOL/Tools/function_package/fundef_package.ML	Fri Apr 25 16:28:06 2008 +0200
@@ -184,6 +184,7 @@
       "declaration of congruence rule for function definitions")]
   #> setup_case_cong
   #> FundefRelation.setup
+  #> FundefCommon.TerminationSimps.setup
 
 val get_congs = FundefCtxTree.get_fundef_congs o Context.Theory
 

--- a/src/HOL/Tools/function_package/lexicographic_order.ML	Fri Apr 25 15:30:33 2008 +0200
+++ b/src/HOL/Tools/function_package/lexicographic_order.ML	Fri Apr 25 16:28:06 2008 +0200
@@ -325,7 +325,7 @@
 
 fun lexicographic_order thms ctxt = 
     Method.SIMPLE_METHOD (TRY (FundefCommon.apply_termination_rule ctxt 1)
-                          THEN lexicographic_order_tac ctxt (auto_tac (local_clasimpset_of ctxt)))
+                          THEN lexicographic_order_tac ctxt (auto_tac (local_clasimpset_of ctxt addsimps2 FundefCommon.TerminationSimps.get ctxt)))
 
 val setup = Method.add_methods [("lexicographic_order", Method.bang_sectioned_args clasimp_modifiers lexicographic_order,
                                  "termination prover for lexicographic orderings")]