# 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 \ (a = a' \ (b, b') : s))" by (auto simp:lex_prod_def) +text {* lexicographic combinations with measure functions *} + +definition + mlex_prod :: "('a \ nat) \ ('a \ 'a) set \ ('a \ 'a) set" (infixr "<*mlex*>" 80) +where + "f <*mlex*> R = inv_image (less_than <*lex*> R) (%x. (f x, x))" + +lemma wf_mlex: "wf R \ wf (f <*mlex*> R)" +unfolding mlex_prod_def +by auto + +lemma mlex_less: "f x < f y \ (x, y) \ f <*mlex*> R" +unfolding mlex_prod_def by simp + +lemma mlex_leq: "f x \ f y \ (x, y) \ R \ (x, y) \ 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)"