equal
deleted
inserted
replaced
5 |
5 |
6 header {* Set-theory lemmas and HOL type definitions *} |
6 header {* Set-theory lemmas and HOL type definitions *} |
7 |
7 |
8 theory Typedef = Set |
8 theory Typedef = Set |
9 files "subset.ML" "equalities.ML" "mono.ML" ("Tools/typedef_package.ML"): |
9 files "subset.ML" "equalities.ML" "mono.ML" ("Tools/typedef_package.ML"): |
|
10 |
|
11 (*belongs to theory Set*) |
|
12 declare atomize_ball [symmetric, rulify] |
10 |
13 |
11 (* Courtesy of Stephan Merz *) |
14 (* Courtesy of Stephan Merz *) |
12 lemma Least_mono: |
15 lemma Least_mono: |
13 "mono (f::'a::order => 'b::order) ==> EX x:S. ALL y:S. x <= y |
16 "mono (f::'a::order => 'b::order) ==> EX x:S. ALL y:S. x <= y |
14 ==> (LEAST y. y : f ` S) = f (LEAST x. x : S)" |
17 ==> (LEAST y. y : f ` S) = f (LEAST x. x : S)" |
16 apply (erule_tac P = "%x. x : S" in LeastI2) |
19 apply (erule_tac P = "%x. x : S" in LeastI2) |
17 apply fast |
20 apply fast |
18 apply (rule LeastI2) |
21 apply (rule LeastI2) |
19 apply (auto elim: monoD intro!: order_antisym) |
22 apply (auto elim: monoD intro!: order_antisym) |
20 done |
23 done |
21 |
|
22 |
|
23 (*belongs to theory Set*) |
|
24 setup Rulify.setup |
|
25 |
24 |
26 |
25 |
27 subsection {* HOL type definitions *} |
26 subsection {* HOL type definitions *} |
28 |
27 |
29 constdefs |
28 constdefs |