moved lemma Wellfounded.in_inv_image to Relation.thy
authorkrauss
Mon Aug 31 20:34:48 2009 +0200 (2009-08-31)
changeset 324633a0a65ca2261
parent 32462 c33faa289520
child 32464 5b9731f83569
moved lemma Wellfounded.in_inv_image to Relation.thy
NEWS
src/HOL/Relation.thy
src/HOL/Wellfounded.thy
     1.1 --- a/NEWS	Mon Aug 31 20:34:44 2009 +0200
     1.2 +++ b/NEWS	Mon Aug 31 20:34:48 2009 +0200
     1.3 @@ -112,6 +112,9 @@
     1.4  Suc_eq_add_numeral_1_left -> Suc_eq_plus1_left
     1.5  Suc_plus1 -> Suc_eq_plus1
     1.6  
     1.7 +* Moved theorems:
     1.8 +Wellfounded.in_inv_image -> Relation.in_inv_image
     1.9 +
    1.10  * New sledgehammer option "Full Types" in Proof General settings menu.
    1.11  Causes full type information to be output to the ATPs.  This slows
    1.12  ATPs down considerably but eliminates a source of unsound "proofs"
     2.1 --- a/src/HOL/Relation.thy	Mon Aug 31 20:34:44 2009 +0200
     2.2 +++ b/src/HOL/Relation.thy	Mon Aug 31 20:34:48 2009 +0200
     2.3 @@ -599,6 +599,9 @@
     2.4    apply blast
     2.5    done
     2.6  
     2.7 +lemma in_inv_image[simp]: "((x,y) : inv_image r f) = ((f x, f y) : r)"
     2.8 +  by (auto simp:inv_image_def)
     2.9 +
    2.10  
    2.11  subsection {* Finiteness *}
    2.12  
     3.1 --- a/src/HOL/Wellfounded.thy	Mon Aug 31 20:34:44 2009 +0200
     3.2 +++ b/src/HOL/Wellfounded.thy	Mon Aug 31 20:34:48 2009 +0200
     3.3 @@ -630,9 +630,6 @@
     3.4  apply blast
     3.5  done
     3.6  
     3.7 -lemma in_inv_image[simp]: "((x,y) : inv_image r f) = ((f x, f y) : r)"
     3.8 -  by (auto simp:inv_image_def)
     3.9 -
    3.10  text {* Measure Datatypes into @{typ nat} *}
    3.11  
    3.12  definition measure :: "('a => nat) => ('a * 'a)set"