added "<*mlex*>" which lexicographically combines a measure function with a relation
authorkrauss
Fri Sep 14 22:21:46 2007 +0200 (2007-09-14)
changeset 245758b5c5eb7df87
parent 24574 e840872e9c7c
child 24576 32ddd902b0ad
added "<*mlex*>" which lexicographically combines a measure function with a relation
src/HOL/Wellfounded_Relations.thy
     1.1 --- a/src/HOL/Wellfounded_Relations.thy	Fri Sep 14 17:02:34 2007 +0200
     1.2 +++ b/src/HOL/Wellfounded_Relations.thy	Fri Sep 14 22:21:46 2007 +0200
     1.3 @@ -124,6 +124,24 @@
     1.4    "(((a,b),(a',b')): r <*lex*> s) = ((a,a'): r \<or> (a = a' \<and> (b, b') : s))"
     1.5    by (auto simp:lex_prod_def)
     1.6  
     1.7 +text {* lexicographic combinations with measure functions *}
     1.8 +
     1.9 +definition 
    1.10 +  mlex_prod :: "('a \<Rightarrow> nat) \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" (infixr "<*mlex*>" 80)
    1.11 +where
    1.12 +  "f <*mlex*> R = inv_image (less_than <*lex*> R) (%x. (f x, x))"
    1.13 +
    1.14 +lemma wf_mlex: "wf R \<Longrightarrow> wf (f <*mlex*> R)"
    1.15 +unfolding mlex_prod_def
    1.16 +by auto
    1.17 +
    1.18 +lemma mlex_less: "f x < f y \<Longrightarrow> (x, y) \<in> f <*mlex*> R"
    1.19 +unfolding mlex_prod_def by simp
    1.20 +
    1.21 +lemma mlex_leq: "f x \<le> f y \<Longrightarrow> (x, y) \<in> R \<Longrightarrow> (x, y) \<in> f <*mlex*> R"
    1.22 +unfolding mlex_prod_def by auto
    1.23 +
    1.24 +
    1.25  text{*Transitivity of WF combinators.*}
    1.26  lemma trans_lex_prod [intro!]: 
    1.27      "[| trans R1; trans R2 |] ==> trans (R1 <*lex*> R2)"