author krauss Thu, 26 Oct 2006 15:12:03 +0200 changeset 21103 367b4ad7c7cc parent 21102 7f2ebe5c5b72 child 21104 b6ab939147eb
Added "measures" combinator for lexicographic combinations of multiple measures.
 src/HOL/List.thy file | annotate | diff | comparison | revisions
```--- 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"```