Added "measures" combinator for lexicographic combinations of multiple measures.

--- a/src/HOL/List.thy	Thu Oct 26 10:48:35 2006 +0200
+++ b/src/HOL/List.thy	Thu Oct 26 15:12:03 2006 +0200
@@ -2404,6 +2404,32 @@
   by blast
 
 
+subsection {* Lexicographic combination of measure functions *}
+
+text {* These are useful for termination proofs *}
+
+definition
+  "measures fs = inv_image (lex less_than) (%a. map (%f. f a) fs)"
+
+lemma wf_measures: "wf (measures fs)"
+  unfolding measures_def
+  by blast
+
+lemma in_measures[simp]: 
+  "(x, y) \<in> measures [] = False"
+  "(x, y) \<in> measures (f # fs)
+         = (f x < f y \<or> (f x = f y \<and> (x, y) \<in> measures fs))"  
+  unfolding measures_def
+  by auto
+
+lemma measures_less: "f x < f y ==> (x, y) \<in> measures (f#fs)"
+  by simp
+
+lemma measures_lesseq: "f x <= f y ==> (x, y) \<in> measures fs ==> (x, y) \<in> measures (f#fs)"
+  by auto
+
+
+
 subsubsection{*Lifting a Relation on List Elements to the Lists*}
 
 consts  listrel :: "('a * 'a)set => ('a list * 'a list)set"