author wenzelm Tue Oct 30 13:43:26 2001 +0100 (2001-10-30) changeset 11982 65e2822d83dd parent 11981 ad67e8d2c75f child 11983 85141af30120
lemma Least_mono moved from Typedef.thy to Set.thy;
 src/HOL/Set.thy file | annotate | diff | revisions src/HOL/Typedef.thy file | annotate | diff | revisions
```     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
```