# HG changeset patch
# User krauss
# Date 1189801306 -7200
# Node ID 8b5c5eb7df876de85beeff5b98a1fa43ee7b1c56
# Parent  e840872e9c7cb251ffa43a6cb9f8da8ebc11f613
added "<*mlex*>" which lexicographically combines a measure function with a relation

diff -r e840872e9c7c -r 8b5c5eb7df87 src/HOL/Wellfounded_Relations.thy
--- a/src/HOL/Wellfounded_Relations.thy	Fri Sep 14 17:02:34 2007 +0200
+++ b/src/HOL/Wellfounded_Relations.thy	Fri Sep 14 22:21:46 2007 +0200
@@ -124,6 +124,24 @@
   "(((a,b),(a',b')): r <*lex*> s) = ((a,a'): r \<or> (a = a' \<and> (b, b') : s))"
   by (auto simp:lex_prod_def)
 
+text {* lexicographic combinations with measure functions *}
+
+definition 
+  mlex_prod :: "('a \<Rightarrow> nat) \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" (infixr "<*mlex*>" 80)
+where
+  "f <*mlex*> R = inv_image (less_than <*lex*> R) (%x. (f x, x))"
+
+lemma wf_mlex: "wf R \<Longrightarrow> wf (f <*mlex*> R)"
+unfolding mlex_prod_def
+by auto
+
+lemma mlex_less: "f x < f y \<Longrightarrow> (x, y) \<in> f <*mlex*> R"
+unfolding mlex_prod_def by simp
+
+lemma mlex_leq: "f x \<le> f y \<Longrightarrow> (x, y) \<in> R \<Longrightarrow> (x, y) \<in> f <*mlex*> R"
+unfolding mlex_prod_def by auto
+
+
 text{*Transitivity of WF combinators.*}
 lemma trans_lex_prod [intro!]: 
     "[| trans R1; trans R2 |] ==> trans (R1 <*lex*> R2)"