author krauss Fri, 14 Sep 2007 22:21:46 +0200 changeset 24575 8b5c5eb7df87 parent 24574 e840872e9c7c child 24576 32ddd902b0ad
added "<*mlex*>" which lexicographically combines a measure function with a relation
--- 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)"