src/HOL/Wellfounded.thy
changeset 36664 6302f9ad7047
parent 36635 080b755377c0
child 37407 61dd8c145da7
equal deleted inserted replaced
36663:f75b13ed4898 36664:6302f9ad7047
   665 apply (erule allE)
   665 apply (erule allE)
   666 apply (erule (1) notE impE)
   666 apply (erule (1) notE impE)
   667 apply blast
   667 apply blast
   668 done
   668 done
   669 
   669 
   670 text {* Measure Datatypes into @{typ nat} *}
   670 text {* Measure functions into @{typ nat} *}
   671 
   671 
   672 definition measure :: "('a => nat) => ('a * 'a)set"
   672 definition measure :: "('a => nat) => ('a * 'a)set"
   673 where "measure == inv_image less_than"
   673 where "measure == inv_image less_than"
   674 
   674 
   675 lemma in_measure[simp]: "((x,y) : measure f) = (f x < f y)"
   675 lemma in_measure[simp]: "((x,y) : measure f) = (f x < f y)"
   705 
   705 
   706 lemma trans_lex_prod [intro!]: 
   706 lemma trans_lex_prod [intro!]: 
   707     "[| trans R1; trans R2 |] ==> trans (R1 <*lex*> R2)"
   707     "[| trans R1; trans R2 |] ==> trans (R1 <*lex*> R2)"
   708 by (unfold trans_def lex_prod_def, blast) 
   708 by (unfold trans_def lex_prod_def, blast) 
   709 
   709 
   710 text {* lexicographic combinations with measure Datatypes *}
   710 text {* lexicographic combinations with measure functions *}
   711 
   711 
   712 definition 
   712 definition 
   713   mlex_prod :: "('a \<Rightarrow> nat) \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" (infixr "<*mlex*>" 80)
   713   mlex_prod :: "('a \<Rightarrow> nat) \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" (infixr "<*mlex*>" 80)
   714 where
   714 where
   715   "f <*mlex*> R = inv_image (less_than <*lex*> R) (%x. (f x, x))"
   715   "f <*mlex*> R = inv_image (less_than <*lex*> R) (%x. (f x, x))"