lemma Least_mono moved from Typedef.thy to Set.thy;
authorwenzelm
Tue Oct 30 13:43:26 2001 +0100 (2001-10-30)
changeset 1198265e2822d83dd
parent 11981 ad67e8d2c75f
child 11983 85141af30120
lemma Least_mono moved from Typedef.thy to Set.thy;
src/HOL/Set.thy
src/HOL/Typedef.thy
     1.1 --- a/src/HOL/Set.thy	Mon Oct 29 17:22:18 2001 +0100
     1.2 +++ b/src/HOL/Set.thy	Tue Oct 30 13:43:26 2001 +0100
     1.3 @@ -893,4 +893,15 @@
     1.4  use "equalities.ML"
     1.5  use "mono.ML"
     1.6  
     1.7 +lemma Least_mono:
     1.8 +  "mono (f::'a::order => 'b::order) ==> EX x:S. ALL y:S. x <= y
     1.9 +    ==> (LEAST y. y : f ` S) = f (LEAST x. x : S)"
    1.10 +    -- {* Courtesy of Stephan Merz *}
    1.11 +  apply clarify
    1.12 +  apply (erule_tac P = "%x. x : S" in LeastI2)
    1.13 +   apply fast
    1.14 +  apply (rule LeastI2)
    1.15 +  apply (auto elim: monoD intro!: order_antisym)
    1.16 +  done
    1.17 +
    1.18  end
     2.1 --- a/src/HOL/Typedef.thy	Mon Oct 29 17:22:18 2001 +0100
     2.2 +++ b/src/HOL/Typedef.thy	Tue Oct 30 13:43:26 2001 +0100
     2.3 @@ -8,18 +8,6 @@
     2.4  theory Typedef = Set
     2.5  files ("Tools/typedef_package.ML"):
     2.6  
     2.7 -lemma Least_mono: 
     2.8 -  "mono (f::'a::order => 'b::order) ==> EX x:S. ALL y:S. x <= y
     2.9 -    ==> (LEAST y. y : f ` S) = f (LEAST x. x : S)"
    2.10 -    -- {* Courtesy of Stephan Merz *}
    2.11 -  apply clarify
    2.12 -  apply (erule_tac P = "%x. x : S" in LeastI2)
    2.13 -   apply fast
    2.14 -  apply (rule LeastI2)
    2.15 -  apply (auto elim: monoD intro!: order_antisym)
    2.16 -  done
    2.17 -
    2.18 -
    2.19  subsection {* HOL type definitions *}
    2.20  
    2.21  constdefs